Provable non-corruption: the foundations of syn verify (v1.0)

Executive summary

Every integrity system in the literature proves one of three things: (A) content integrity: this artifact is the one attested (hash/signature); (B) history integrity: the append-only log was not reordered, truncated, or rewritten (consistency proof); (C) derived-state integrity: the output was reproducibly derived from the input (deterministic rebuild). Synapse is uniquely positioned to prove all three at once, offline, per-fact, because the truth is the user’s Markdown in their git and the SQLite index is a pure function of it. A hosted competitor structurally cannot offer (C); there is no user-side source to reproduce from. syn verify operationalises the brand line “provable, not estimated” into a command that emits a signed, reproducible attestation. The governing discipline, inherited from the ADRs: borrow the invariant, refuse the engine (no servers, no heavy deps, deterministic over ML, tamper-evident not tamper-proof).

1. Theory → adoption verdict (condensed)

2. The invariants syn verify proves (the catalogue)

Each is deterministic (recomputable, no ML/judge) and contributes a line to the signed report.

1. INV-1 Disposability / reindex fixpoint: digest(reindex(markdown)) == digest(live index) over a canonical logical dump (ordered rows; rowids/FTS-internal/float-vectors excluded or pinned to model@precision). The keystone; the index is a reproducible build of the files.
2. INV-2 Content integrity: every fact’s payload_sha256 matches the Markdown blob at the commit that introduced it; no orphan facts, no orphan audit rows.
3. INV-3 History integrity: hash-chain (seq/prev) + ed25519 signed checkpoint intact (Tier-2), or git DAG intact + per-author monotonic segments (Tier-1). (Shipped as audit verify; formalise.)
4. INV-4 Reversibility: replaying the audit reconstructs the current store state (frontmatter-generic). (Riskiest: see §4.)
5. INV-5 No silent corruption: no fact’s value changed without a recorded x-supersedes + an appended interval close (invalidation-not-deletion). The HaluMem <26%-auto-update failure made a provable invariant, the headline differentiator.
6. INV-6 Port parity: CLI ≡ MCP for every read (metamorphic; the AGENTS.md “two doors, one core” rule as a test).
7. INV-7 Temporal correctness: at <ref> -- search --as-of <date> reconstructs the state that held. (Seeded by SYN-258.)
8. INV-8 (opt) Round-trip: import(export(w)) ≅ w.

Proof artifact: a signed synapse.verify-report/1 (in-toto-shaped): {subject:{workspace, git_ref, inputs_hash}, predicate:{tool_version, invariants:[{id,status,evidence}], checkpoint, witness_status, ts}, sig, pubkey}. Reproducible: anyone with the repo at git_ref re-runs syn verify and gets a bit-identical inputs_hash + the same verdicts.

3. Opportunities (white space, ranked)

• O1: syn verify (headline). All three integrity classes, offline, exit-coded, signed report. Mostly assembly of shipped primitives (audit verify + reindex + at/--as-of) reframed as proofs → low new code, category-defining claim.
• O2: Verifiable-rebuild attestation (--rebuild). “Your memory is a reproducible build of your files; delete the index, rebuild it, get the same bits: if you can’t, syn verify tells you which fact.” Literally true, and uncopyable by a hosted store.
• O3: Offline consistency proof + publishable witness (syn audit witness + syn verify --since <ref>). Cache a signed tree-head; prove the current history is an append-only extension (git ancestry + segment-prefix hash) → catches history-rewrite locally, no remote. A published checkpoint lets a third party hold the owner to their history (recovers part of the witness property ADR-030 says only a remote gives).
• O4: git as the trust root. Export identity → .synapse/allowed_signers (git-native verify), gix verify_checksum for the DAG. Resolves ADR-030’s open allowlist; no reinvention.
• O5: The invariant harness (CI). proptest (already a dev-dep) + metamorphic + differential (CLI≡MCP) + fuzz the untrusted boundary. The “test-suite half” of SYN-253. Only new dep: cargo-fuzz (opt-in, own ADR).

4. Critical caveats / risks (be honest)

• Honest ceiling: tamper-evident, not tamper-proof. A lone local clone cannot detect its own owner’s rewrite (no witness). syn verify must print the trust-root caveat (local-only vs remote-witnessed vs checkpoint-witnessed). The Memoir lesson: be specific where competitors hand-wave “cryptographically secure.”
• Canonicalisation is the one real prerequisite. The index isn’t byte-deterministic (rowids, FTS internals, float vectors). Verify against a canonical logical manifest; spike it first (SYN-262).
• Replay (INV-4) rests on an unverified ADR-027 assumption (generic frontmatter reconstruction + supersession-close-as-append). Verify that before claiming --deep replay; else a frontmatter-generic replay refactor is needed first.
• Don’t over-engineer. Reject Rekor/Fulcio/OIDC, Trillian/witness-nets, runtime model-checking, RDF/OWL, IPFS/CID. Borrow the invariant, refuse the engine.

5. Proposed v1.0 issues (next free SYN-262)

Whitepaper/positioning (separate doc): “Provable non-corruption”: the invariants, the proof artifact, and a SLSA-style ladder (L1 audited → L2 hash-chained → L3 git-witnessed → L4 signed-identity).

6. Cross-check vs prior hypotheses