| index dbb6f7b..b109684 100644 |
| --- a/implementation/compatibility-checker/proposal.json |
| +++ b/implementation/compatibility-checker/proposal.json |
| @@ -1,6 +1,6 @@ |
| { |
| - "version": 3, |
| - "status": "UNAPPROVED revision3 after Fable R2; all original blockers resolved, replication schema correction pending rereview", |
| + "version": 4, |
| + "status": "UNAPPROVED revision4: pinned-library cleanup proof addresses PERSIST_WAL handoff blocker; design rereview required", |
| "home_revision": "7e282e2a363b9cc90cd74dd97809e6613a699af8", |
| "audit": "audit.json", |
| "audit_sha256": "0625d33bb795c1cf415e1e213d8e572e65f8ae4ebcf71ab52adf264c076e8b60", |
| @@ -91,7 +91,7 @@ |
| "directory_set": "migrate.Merge(directorySchema, directorydata.OperatorSchema, operator.DirectorySchema) from selected release. directorySchema = sessions.Schema + oficina_handoff migrations + directorydata.Schema + directorydata.RosterSchema. Operator bindings namespace oficina_directory_operator_bindings; DirectorySchema namespace oficina_directory_operator with0001_operator,0002_owner_receipts,0003_operator_key_identity.", |
| "current_gap": "Runtime.Schema currently omits operator.CredentialSchema/operator.DirectorySchema and directorydata.OperatorSchema. Checker never fixes that. Separately reviewed additive deployment must install required sets before the checker can succeed.", |
| "ledger": "Use Set.All plus migrate.Checksum of exact embedded SQL. Read rastrillo_migrations through pinned connection; every expected ID and checksum must match and no extra ID is accepted. Go migrations, if introduced, require explicit release profile rather than empty-checksum inference. Never call Apply.", |
| - "structure": "Build expected normalized sqlite_schema/table/index/FK/trigger/view shape at build/test time by replaying exact reviewed migration sets into a scratch DB; freeze expected descriptor in release. Compare actual structure read-only, including constraints/index expressions/triggers/views; migrate.Read alone lacks complete CHECK/FK/trigger semantics and is insufficient. Normalize only SQLite-stable metadata/formatting defined by fixture generation, not SQL semantics through regex. Generated internal sqlite tables and ledger are explicitly included or excluded by fixed rule. Exact expected sqlite_schema SQL from the same migration execution is acceptable conservative first profile; harmless divergent DDL may refuse. The frozen descriptor includes exactly the pinned replication-owned objects specified below, generated by executing their exact upstream DDL in the scratch build/test fixture; this does not create or repair objects on the real DB.", |
| + "structure": "Build expected normalized sqlite_schema/table/index/FK/trigger/view shape at build/test time by replaying exact reviewed migration sets into a scratch DB; freeze expected descriptor in release. Compare actual structure read-only, including constraints/index expressions/triggers/views; migrate.Read alone lacks complete CHECK/FK/trigger semantics and is insufficient. Normalize only SQLite-stable metadata/formatting defined by fixture generation, not SQL semantics through regex. Generated internal sqlite tables and ledger are explicitly included or excluded by fixed rule. Exact expected sqlite_schema SQL from the same migration execution is acceptable conservative first profile; harmless divergent DDL may refuse. The frozen descriptor includes exactly the pinned replication-owned objects specified below, generated by executing their exact upstream DDL in the scratch build/test fixture; this does not create or repair objects on the real DB. Compare as a SET keyed by sqlite_schema type,name,tbl_name and normalized stored SQL (SQLite-produced spelling from exact fixture DDL), never row order, rowid or rootpage. Replication tables may predate app/operator migrations; physical page placement and creation order do not affect accepted identity. Structural field/SQL normalization must not erase constraints or expressions.", |
| "credential_identity": "No directory/team/roster namespace; people refs and blind indexes retain their current shape. If operator_state exists, exact origin/installation/registry/device/key identity must match trusted enrollment and sequence/head/completion must match approved expected state constraints. Do not infer app identity from table names alone. The exact two replication-owned tables are shared infrastructure and explicitly allowed; they do not establish Home role identity.", |
| "directory_identity": "No people/signin/passkey credential namespace; exact operator origin/installation/registry/device/key identity when initialized; generation and existing owner/team memberships agree with trusted baseline expectations. Validate team sqid/label, purpose-bound name, bounded epochs, and existing registry/provisioning references using current pure validators. No new generation, team or owner creation. The exact two replication-owned tables are shared infrastructure and explicitly allowed; they do not establish Home role identity.", |
| "empty_policy": "No default empty DB success. Missing file, empty schema, missing ledger or untrusted role binding always refuse. A schema-complete but authority-empty initial role is accepted ONLY with a separately enrolled explicit baseline profile binding exact DB identity, role/origins, required schema, expected absence of operator state/generation/teams/people and key fingerprints. This permits planned first initialization without inventing ownership, but that baseline profile must be reviewed/enrolled; a caller boolean or just current count=0 is insufficient. Initialized profile requires exact expected state presence and at least its enrolled durable identity witnesses; zero rows unexpectedly refuses.", |
| @@ -115,11 +115,13 @@ |
| "worker_order": [ |
| "Verify exact approved resume operation, exclusive operation execution and same primary/artifact/environment/DB identities. Install durable/local admission fence. Obtain checked old main+sidecar death, cgroup emptiness and old replication Close evidence BEFORE acquiring the maintenance Held lease.", |
| "Under the same retained healthy Held lease and exclusive worker execution, invoke the separately proposed Held.Checkpoint protocol: temporary replica store SyncAndWait then checked Close; final lease health check. No Release or second owner. All store/SQLite handles used by checkpoint must be closed. Failure or uncertain close refuses handoff.", |
| - "Checkpoint receipt alone does not prove filesystem state. Verify main exists, one link and exact pinned identity, and WAL/SHM/rollback-journal are ABSENT by nofollow relative inspection of pinned parent directory. Any sidecar including zero-length WAL/SHM refuses; never delete sidecars to make the check pass. Normal closed checkpoint is the supported positive state. If actual checkpoint leaves sidecars, remain fenced/unavailable until a separately reviewed preparation path exists.", |
| - "Run the platform non-serving integrity check against the exact closed DB under the same retained lease before the prelaunch byte-hash step; check/close its handle and recheck all sidecars absent afterward. Bind its fresh successful result into handoff evidence. This ordering is an explicit proposed refinement of maintenance-exec P1, not an assertion that an integrity receipt obtained only after the checker already exists. Failure or sidecar creation leaves handoff unavailable; no checker repair.", |
| + "This preparation is permitted only after fresh approval/fence/old writer and replica death under retained Held, never side-effect-free preflight. Litestream0.5.14 deliberately retains WAL/SHM via PERSIST_WAL1; do not require absence immediately after its Close. Open exactly one ordinary existing-only mode=rw SQLite connection through reviewed pinned DB and sidecar identity verification, with no global hooks or background jobs. This is worker preparation, not the readonly checker. Require one pool connection and no other SQLite/replication handle on the DB.", |
| + "On that ordinary connection, use the pinned modernc FileControl interface to set FileControlPersistWAL(\"main\",0), verify returned/readback0, run integrity_check requiring exactly ok, then PRAGMA wal_checkpoint(TRUNCATE) requiring busy=0,log=0,checkpointed=0. Unsupported file control, busy/incomplete checkpoint, integrity error, deadline/lease loss or uncertain identity refuses. Check all failures; no fallback/manual unlink or ignoring busy result. Return connection then checked DB.Close to perform last-connection SQLite cleanup. This close-time deletion is an explicitly proposed worker preparation effect under retained authority, never a checker mutation.", |
| + "After checked ordinary last close verify main one-link identity and actual ABSENCE of WAL/SHM/rollback-journal. Any remaining file, including zero-byte sidecar, refuses; never delete it to manufacture proof. Check lease health and exclusive executor still current. If actual pinned driver cannot complete cleanup, remain fenced/unavailable. Bind this fresh preparation+integrity receipt with Held.Checkpoint receipt into launch evidence; the exact receipt must identify source, operation and same lease rather than a free-standing success boolean.", |
| "After closure and before checker launch, bind main length and SHA256 from an exact bounded scan to fresh attempt-specific private handoff evidence, alongside checkpoint receipt, old-writer/replica stop evidence, retained lease identity and current guard generation. Recheck absence/identity and healthy lease before dispatch.", |
| "Launch only the exact selected checker artifact under immutable protected environment and reviewed read-only data namespace. Verify fresh handoff evidence through the platform launch verifier. The checker cannot mint evidence from a path, env flag, lease timestamp or its own observation.", |
| - "No writer, checkpoint, replication reopen, adoption or other checker may overlap this handoff interval. Worker retains lease/exclusive execution through checker closure, final evidence and resume transition. Any failure remains fenced. Existing ResumeFenced still owns subsequent compatible serving/replication handoff; checker never releases ownership." |
| + "No writer, checkpoint, replication reopen, adoption or other checker may overlap this handoff interval. Worker retains lease/exclusive execution through checker closure, final evidence and resume transition. Any failure remains fenced. Existing ResumeFenced still owns subsequent compatible serving/replication handoff; checker never releases ownership.", |
| + "Preserve the protocol-required POST-checker independent integrity/checkpoint/restore and final serving handoff checks. This new pre-checker preparation supplies immutable-opening conditions only; it does not replace those checks, clear the fence or approve serving. Any post-checker checkpoint may recreate sidecars; that is outside the closed checker interval and must be handled by existing reviewed resume protocol." |
| ], |
| "executor_recovery": "A fresh lease, empty app cgroup or RecoverClaim alone does not prove an earlier maintenance executor is dead. Paused workerA could later checkpoint/reopen/publish while B checks immutable state. Takeover unavailable unless independently reviewed exclusive operation execution and predecessor executor quiescence/death/exclusion proof hold. No automatic timeout-based recovery or reuse of old handoff receipt.", |
| "identity": "Retain existing nofollow ancestor walk, pinned parent and one-hardlink main device/inode, actual driver-open descriptor inventory, checks before/after every query/row and close. Expected driver main descriptor must be O_RDONLY and match the retained main identity. URI built by code with only fixed mode=ro,immutable=1,defaultVFS; no caller query params/hooks/extensions. Refuse O_RDWR/O_WRONLY, extra database, unexpected file descriptor, reconnect overlap, changed path or unlinked main. Immutable is safe only because separately proved ownership excludes ALL writers; it is not evidence that no writers exist. After pin acquisition and before driver open, freeze FD baseline. Require exactly ONE new O_RDONLY descriptor matching main device/inode in post-open FD delta; retained pin is already in baseline and cannot satisfy this test. Refuse no delta, multiple matching new FDs, writable/unlinked/temp regular descriptors or loss/reuse of a baseline FD. Apply same identity/descriptor checks across operation lifetime. Do not reuse mutable connector writable-only classification.", |
| @@ -129,9 +131,9 @@ |
| "descriptor_lifetime": "Checker acquires and retains read-only pinned main descriptor before driver construction; prehash via that descriptor before SQL open and posthash via the SAME descriptor only after all SQLite connections close. Never open/close a second main-file descriptor while SQLite locks may exist. Use ReadAt/Seek on retained descriptor rather than reopening path. Keep it until hash/identity/sidecar checks finish. Close failure, partial scan, unexpected EOF/growth, deadline or mismatch prevents success. Worker independent observer holds its own stable descriptor and closes outside any local SQLite active connection.", |
| "deadline": "Entire invocation including both checker hashes and SQL scan is bounded by min(verified launch deadline,30seconds) and conservative retained-lease deadline. Check context between64KiB reads; blocking kernel IO is supervised by platform containment/deadline and failure cannot be reported as checked stop. No success emitted if cleanup/posthash cannot finish within deadline. Larger/slower DB refuses, never sampling or extending lease authority.", |
| "postcondition": "Before emitting any success bytes, verify driver close succeeded, exact pre/post main hashes match the fresh worker handoff hash, identity/size still match and all three sidecars remain absent. Worker accepts result only for exact live attempt with retained healthy lease and exclusive ownership, and independently rechecks identity/absence before resume. A hash is byte evidence under the no-writer protocol, not proof against a hostile trusted worker that changes and restores bytes.", |
| - "actual_driver_gate": "Required empirical positive: exact pinned modernc/native Linux, WAL-mode header but cleanly checkpointed/closed main with no sidecars, actual mode=ro&immutable=1 O_RDONLY inode descriptor, byte preservation and no sidecar creation. Negative: current mode=rw+query_only housekeeping probe, missing handoff, hot/empty WAL, SHM, journal, stale lease/worker, inode replacement and >256MiB all refuse. No VFS/unsafe introspection/dependency fork; failure means unsupported, not fallback.", |
| + "actual_driver_gate": "Required empirical positive: exact pinned modernc/native Linux, WAL-mode header but cleanly checkpointed/closed main with no sidecars, actual mode=ro&immutable=1 O_RDONLY inode descriptor, byte preservation and no sidecar creation. Negative: current mode=rw+query_only housekeeping probe, missing handoff, hot/empty WAL, SHM, journal, stale lease/worker, inode replacement and >256MiB all refuse. No VFS/unsafe introspection/dependency fork; failure means unsupported, not fallback. Enforce temp-file prohibition through actual descriptor inventory (including unlinked writable temp files), not merely temp_store readback: SQLITE_TEMP_STORE compile options may override pragma. Test forced spill/refusal on actual build; bound memory and fail closed. Positive local library proof is in probe/closed-checkpoint-proof.json, separate from future actual pinned-descriptor checker proof.", |
| "root_probe": "Historical probe/observation.json demonstrates current mutable connector changes main/removes WAL+SHM despite only SELECT/query_only. It remains a negative control; it does not prove the proposed immutable connector or worker handoff exists.", |
| - "approval_provenance": "maintenance-exec.md P1 names the desired retained-lease checkpoint/stop protocol, but its file retains pending-approval status text. Treat those dependencies as separately proposed/reviewed artifacts whose exact approval and implementation receipts must be verified at integration. Neither this checker design nor references to parent work approve or supply checkpoint/launch/executor capability. Explicit immutable exception and integrity-before-hash ordering are requests for this dependency contract." |
| + "approval_provenance": "maintenance-exec.md P1 names the desired retained-lease checkpoint/stop protocol, but its file retains pending-approval status text. Treat those dependencies as separately proposed/reviewed artifacts whose exact approval and implementation receipts must be verified at integration. Neither this checker design nor references to parent work approve or supply checkpoint/launch/executor capability. Explicit immutable exception and integrity-before-hash ordering are requests for this dependency contract. Protocol owner confirms the pre-checker sequence is an additive app/worker-preparation dependency under the same approved operation, not preflight or a new wire/state transition; actual implementation still needs review. Local pinned-library proof establishes mechanics only, not deployed containment, file binding, namespace isolation or authority." |
| }, |
| "launch_and_result": { |
| "required_input_binding": "Verified platform launch pins request/attempt/guard generation, account/app/primary host, selected immutable executable digest, immutable config snapshot binding, existing DB device/inode, role/origin and enrolled expected-state digest. Exact fields/API come from reviewed launch contract; application cannot self-authorize or accept raw env equivalents. Additionally require fresh verified closed-checkpoint handoff evidence binding main identity/length/SHA256, absent WAL/SHM/journal, old writer/replica stop proof and same retained lease/exclusive executor. Evidence format belongs to reviewed platform launch adapter; this checker design requests required semantics, not a new self-signed authorization.", |
| @@ -181,7 +183,11 @@ |
| "Remove immutable restriction-to-verified-handoff, sidecar absence, final byte comparison or handoff ciphertext checks in meaningful mutations: each must be killed.", |
| "Actual replicated synthetic Home fixture after pinned Litestream open/checkpoint/close passes exact2-table profile; application ledger remains unchanged and no repair writes occur. Missing table, extra prefix object, added trigger/index, seq id!=1/NULL/noninteger/out-of-range/second row and nonempty lock all refuse.", |
| "Mutations skipping replication row checks, excluding replication metadata from byte hashes, accepting retained pin as driver FD, omitting temp_store=MEMORY, or allowing wrong cross-runtime expected key equality must fail tests.", |
| - "Platform integrity must complete and close before hash/handoff. A stale/after-checker integrity receipt cannot satisfy prelaunch requirement." |
| + "Platform integrity must complete and close before hash/handoff. A stale/after-checker integrity receipt cannot satisfy prelaunch requirement.", |
| + "Pinned actual Held/Litestream/modernc proof: after Held.Checkpoint sidecars remain; ordinary FileControlPersistWAL0 + integrity + TRUNCATE + checkedlastclose removes them without unlink; same renewer/lease remains healthy, peer acquisition refused, replica restores unchanged logical data, immutable read preserves main hash/absence.", |
| + "Negative PERSIST_WAL1 on preparation connection retains sidecars and prevents success. Also test busy TRUNCATE, unsupported control, failedclose, lease loss and wrong inode: no checker launch. Synthetic proof does not substitute for integration tests of these failure cases.", |
| + "Run preparation only after fresh authorized execution and fence, never preflight. Mandatory independent post-checker integrity/checkpoint/restore remains executed; mutation skipping it must fail.", |
| + "Descriptor profile accepts replication tables created before additive migrations with changed rootpages/order, but refuses changed constraints/indexes/triggers/contents; actual temp spill is refused even when pragma readback reports memory." |
| ], |
| "unresolved_review_dependencies": [ |
| "Checker-only exception to approved mutable operator mode=rw contract, reviewed immutable readonly descriptor connector and verified closed-checkpoint launch evidence are required. No existing Checkpoint receipt alone asserts absent sidecars or exclusive predecessor executor death; integrations must implement and prove those facts. Unsupported state remains unavailable.", |
| @@ -416,5 +422,5 @@ |
| "sha256": "6ab9ea1dd6c63916f8d1984cf4a7c3a7cdf05e4705e807a34c58f7da5e537824" |
| } |
| ], |
| - "review_note": "R3 resolves concrete replication-owned schema blocker and clarifies R2 nonblocking findings. No runtime implementation or dependency approval inferred." |
| + "review_note": "R4 addresses R3 PERSIST_WAL blocker using actual pinned-library/local Held proof. This is a complete proposed preparation dependency with post-checker checks preserved; runtime authority and deployment not inferred." |
| } |
amadan