Proving the Home operator's opened database

Status: exact design4770bc6 APPROVED by Claude Fable5 (claude-fable-5), explicit verdict with no blockers, stopReason=end_turn and process exit0. Receipt: /tmp/oficina-home-open-design-review/verdict.txt; model-metadata.json and exit.json preserve provenance. This annotation does not approve code, command dispatch or the later platform fd4 delta. Parent contracts: approved home-operator-seed.md and home-provisioner.md at898fe219, approval recorded3945a34; pending-window amendment42529b5 approved and recorded806c4ad. Platform's separately reviewed launch supplement is proposed4605a54, implementation/maintenance-launch.md. This amendment resolves only the native Linux SQLite identity check. It does not claim a maintenance fence, worker implementation, or live operator proof.

Why the pathname is insufficient

The disposable modernc.org/sqlite v1.55.0 experiment in /tmp/oficina-home-open-proof uses two independent synthetic databases. It pins the original inode, replaces the path before SQLite opens it, and restores the original pathname after opening. SELECT returns the replacement's marker while the final pathname again matches the original pin. Thus even matching path checks before and after SQLite open do not identify the database actually opened.

The same experiment inventories actual process descriptors using /proc/self/fd, fstat and FGETFL. Ordinary opening introduces exactly one writable regular descriptor matching the pin. In the replacement-and-restored-path case none of the newly opened writable descriptors matches the pin. Replacement after opening instead fails the final pathname check. A symlink before pinning refuses ONOFOLLOW; a symlink introduced afterward opens a different inode and fails verification. The proc-fd path experiment observes the original database after a rename, but does not establish that SQLite's pathname canonicalization and subsequent opens are race-free. We will not use /proc/self/fd/N as a substitute for verification.

These are read-only marker queries in a synthetic process, not a production connector or proof against a malicious process controlling the worker UID. Source and exact JSON receipts are copied into the review snapshot with hashes. They justify the problem and the candidate mechanism; the tests below still have to establish the full implementation.

Supported boundary

Use a command-only database/sql/driver.Connector around the pinned modernc driver. No dependency fork, private conn-field access, unsafe memory layout, custom VFS or new cryptography is introduced. The supplied modernc fs.FS VFS is read-only; its public FileControl interface exposes PersistWAL and DataVersion, not HAS_MOVED or the underlying descriptor. Those interfaces cannot supply this proof today.

The connector is supported only in the fixed, nonserving native Linux operator process. The worker launches the immutable artifact with only fd0/1/2/3 and the reviewed private environment. Before database construction, this process has no SQLite connections, HTTP server, mailer, background jobs, extension loading, arbitrary UDF hooks or other file writers. Configuration and signature verification do not open a database. The adapter fails if its baseline descriptor inventory includes any writable regular file. Pipe stdio/context and /dev/null are not regular files. An unexpected inherited regular-file stdout is unsupported, not a relaxed exception.

The worker holds the real lifecycle fence and continuously supervises its lease. Same-UID hostile process injection is outside the approved trusted-worker boundary, as in the launch supplement. This check is not protection against a malicious approved artifact that manufactures descriptors to fool itself. File replacement and symlink mistakes are nevertheless tested at controlled barriers. The approved artifact owns all connector construction, and request JSON cannot choose a DSN, URI flag, path or validator.

The native proof relies on Linux /proc and actual file identity. Missing proc access, unsupported fstat/flags, ambiguous candidates, hardlinked database files, descriptor reuse or a driver behavior change fail closed. There is no path-only fallback. Keep the exact modernc1.55.0 pin until this contract is reviewed against a proposed upgrade.

Connection construction

After validating the launch descriptor and signed input, the adapter has the worker's exact expected absolute database path, device and inode. Role, origin and fixed operation allowlist come from the pinned launch environment. Platform request/attempt and the verified Home operation ID remain distinct and bound in private invocation metadata. The worker checks expected artifact/environment/record bindings before creating fd3; Home cannot independently reconstruct a randomized environment-envelope digest or platform registry record. It validates their shape and trusts that checked worker construction. The Home input hash and opened database identity are independently checked here.

1. Traverse the exact absolute database path with directory-relative opens and ONOFOLLOW on every component. Require a regular existing final file, nonzero device/inode, one hard link and exact worker identity. Hold a read-only close-on-exec descriptor to that file for the entire command. Never use OCREAT. URI encoding is performed by code, using only mode=rw and the fixed default VFS; no request query string or _pragma executes during opening.
2. Snapshot all regular descriptors and flags immediately before driver.Open. Refuse pre-existing writable regular files other than none: the read-only pin is deliberately not an eligible SQLite candidate. The implementation owns its /proc enumeration descriptor and excludes only that nonregular directory descriptor. It cannot ignore arbitrary user-supplied descriptor numbers.
3. Call a dedicated modernc Driver with no registered hooks/modules/extensions. Its source and tests must establish that this constructor opens exactly one main SQLite connection. Do not call the general web db.Open, migrator or schema repair path. No persistent PRAGMA or operator mutation executes before identity verification. If a metadata query is necessary to materialize the main descriptor, it is fixed read-only SQL and separately tested for zero application-data changes; do not claim opening SQLite can never touch its own auxiliary files.
4. Inventory actual descriptors again and fstat every new writable regular candidate. Require exactly one candidate for the main database's pinned device/inode, no candidate that is a different main database, and no ambiguity about whether an existing descriptor was reused. Expected WAL/SHM descriptors may only be accepted after their fixed sibling identities/names are established; unknown writable regular files refuse. Verify PRAGMA database_list contains only main at the exact expected canonical pathname, with no attachment, as a supplemental check rather than the inode proof.
5. Capture the matched descriptor number and identity in a private wrapper for this exact driver.Conn, then re-open/recheck the normal pathname without following symlinks. Do not duplicate or independently close SQLite's descriptor: doing so can affect POSIX inode locks. The retained read-only pin is independently owned and closed only at command end.
6. Return this verified wrapper to database/sql. Set MaxOpenConns=1 and MaxIdleConns=1. Every future Connect repeats the complete proof; no raw/global modernc registration or alternate DB pool is available to the command. A reconnect cannot inherit another connection's proof.

The implementation must make candidate classification executable and testable. It may not merely assert that a matching inode somewhere in the process belongs to SQLite. The proof depends on the clean pre-open process inventory, the dedicated one-connection constructor, the newly introduced descriptors and their actual flags/identities. If these assumptions cannot be established on the pinned source, this design refuses dispatch; adding a supported driver API would require a separate reviewed change.

Operation and error boundaries

The private wrapper checks the borrowed descriptor remains open with the same identity/flags, the retained pin still matches, and the normal path still names that file before each fixed query, execution and transaction boundary. It also checks the bounded execution deadline. The engine uses that one verified connection for its immediate transaction, FK readback, schema/role checks, idempotency and mutation. Every prepared statement or transaction object must remain behind the same wrapper; an implementation may refuse unsupported Prepare rather than accidentally return an unguarded statement. Direct context query/exec are sufficient for the current engine, but this must be proven by its tests.

Check identity again after execution and before reporting success. A mismatch after an operation may have committed is unavailable/ambiguous, never a claim of rollback or a successful result. No identity/deadline failure returns driver.ErrBadConn: database/sql can automatically retry that error, which is unacceptable for a possibly executed mutation. Cleanup Close and rollback remain available on the already opened connection; they do not follow a new path or mint authority. The worker keeps its fence on any ambiguous outcome and independently checks identity after the child dies.

A path or descriptor check is not a lease extension. The worker's independent supervisor can terminate the command before lease loss. No app field says fenced or approved, and no boolean bypass reaches the engine. The connector is constructed only after valid inherited context, never from a body struct. Tests with a synthetic fd3 are local consumer proofs only.

Required tests before wiring

• Actual pinned modernc connection: ordinary existing WAL database permits the expected mutation and preserves all unrelated rows and sessions. Descriptor inventory shows the verified main inode belongs to the newly opened driver connection. No DB creation, migration, alternate VFS or hidden writer is reachable.
• Controlled replacement before open with pathname restored afterward, replacement after open, symlink before pin and after pin, symlinked ancestor, unlink/recreate, multiple hardlinks, missing proc, wrong flags, unexpected inherited writable descriptor, ambiguous candidates, descriptor close/reuse and an attempted second connection all refuse without an operator mutation.
• Reconnect and statement/transaction paths cannot skip checks. Deadline and identity failures return fixed errors rather than ErrBadConn. A failure after a deliberately committed synthetic operation reports ambiguity and leaves no success receipt; rollback/Close still release the owned connection.
• Repeat tests in actual subprocesses with only the specified inherited descriptors. Test all controlled barriers around pin, driver open, candidate capture and pre-commit checks. Preserve failures as evidence rather than weakening guards to make the fixture run.
• Extend the existing privacy gate: private stdin, context digest and owner material stay out of errors/logs; current role migrations and canonical origins still apply. Run full make/CI and Fable whole worker plus consumer review. The eventual real canary must demonstrate cgroup/lease/fence behavior separately.

Approval of this amendment allows implementing and testing the connector. It does not authorize mounting the Home command before the concrete worker launch contract, private configuration schema and whole-code review are complete.

Recorded review obligations

Fable's nonblocking implementation notes remain acceptance requirements: audit package-global registration as well as the dedicated Driver receiver; verify exact nofollow one-link WAL/SHM siblings; prove mode=rw suppresses the driver's hardwired CREATE flag; refuse unlinked temp descriptors and an unexpected temp database; fail closed on reconnect baseline overlap; and classify OWRONLY as writable in addition to ORDWR. The source audit after review confirms modernc vtab.go registerModules reads global d.modules. The serving-path secure-delete registration must not be mistaken for proof of a clean operator startup; the eventual command call graph and package initializers require review.

Platform proposed caf47fb adds a read-only artifact fd4 and self-executable binding after this frozen review. Its delta did not obtain a verdict before provider quota exhaustion. That layout needs explicit alignment before dispatch; this document's4770bc6 approval is not approval of a silently modified launch contract. Further Fable review attempts wait for the provider reset without model substitution or extra credits.