PROOFS.adoc

Ochránce — Proof Campaign Ledger

This is the authoritative, dependency-sorted plan for driving the formal verification of the Ochránce estate to completion. It is the durable source of truth for the proof thread: it survives context compaction, so each working window starts from this file rather than from chat memory.

Table of Contents

• 1. Scope & estate map
• 2. Decisions on record
• 3. Current proof state (ochrance, canonical)
• 4. The remaining proof program (dependency-sorted)
  • 4.1. Stage 1 — Merkle closure + crypto-binding interface [model: Opus]
  • 4.2. Stage 2 — Verify + Validator soundness [model: Opus → Sonnet if mechanical]
  • 4.3. Stage 3 — Repair correctness (L3, linear types) [model: Opus]
  • 4.4. Stage 4 — Completeness, binding discharge, write-up [model: Sonnet; Opus if binding is hard]
• 5. The IO↔pure bridge (estate-wide spine)
• 6. Build-with-proofs discipline
• 7. Optimisation ledger (against the proven backdrop)
• 8. Honestly-bounded items (NOT failures — boundaries by design)
• 9. Disposed tracks (handoff briefs)
  • 9.1. svalinn — migrate ReScript → Ephapax, then verify [model: Sonnet]
  • 9.2. ochrance-framework — retire core, harvest Interface, keep docs [model: Sonnet]
  • 9.3. ochrance ABI / Zig FFI hardening [model: Sonnet/Haiku]
  • 9.4. CI watch — PR #32 [model: Haiku/Sonnet]
• 10. Model guidance (per the thread’s operating model)

1. Scope & estate map

Three repositories are in scope. "Verification" means something different in each.

Repo	What "verified" means	This thread executes?
ochrance	Idris2 dependent-type proofs (the canonical core).	Yes — primary focus.
ochrance-framework	Architecture + docs. Its ochrance-core is a weaker, type-incompatible duplicate and is being retired (see Decision D1).	Docs/Interface harvest only — core is deleted, not proven.
svalinn	ReScript edge gateway → migrating to Ephapax (replaces all ReScript). Type-safety and schema/property tests, not dependent types.	No — disposed to a delegated session (see Disposed Tracks). Specs tracked here.

2. Decisions on record

ID	Decision
D1 — Converge on ochrance	ochrance/ochrance-core is the single source of proof truth. ochrance-framework/ochrance-core is retired. Its one genuinely better idea — the mode-indexed, subsystem-parameterised VerifiedSubsystem Interface (VerificationProof mode SubState SubManifest) — is harvested into ochrance. Framework keeps its real value: the docs (A2ML-SPEC, FFI-CONTRACT, THREAT-MODEL, WHITEPAPER, ROADMAP, L4-POLICIES) and architecture.
D2 — Crypto binding as a typed interface	The security half of the Merkle argument (collision resistance) is modelled as an Idris hypothesis CollisionResistant h, and the binding theorem is discharged against it — not left as prose. Stubbed in Stage 1, discharged in the final stage.
D3 — svalinn: migrate before proving	Prove where the language is final; migrate-then-prove where it is changing. svalinn migrates ReScript → Ephapax — Ephapax replaces all the ReScript. Its linear/exactly-once types make JWT/JTI single-use & revocation, OAuth nonce/PKCE, and session/container lifecycle compile-time guarantees, and typed boundary decoders eliminate the 20+ Obj.magic. Its specifications are captured now (Disposed Tracks); its proofs come after migration. Proving the about-to-be-deleted ReScript is waste. (AffineScript is not the target — it surfaced only as a format exemplar for the migration map.)

3. Current proof state (ochrance, canonical)

The core is clean: all 19 ochrance-core modules carry %default total (the src/abi/ tree adds the ABI modules separately); zero believe_me / assert_* / postulate / holes / partial on any proof symbol.

Table 1. Proven, machine-checked (axiom-free)

Theorem	Statement (shape)
merkleCorrect / merkleCorrectWith	inclusion-proof soundness; generic over the hash combiner h (XOR & BLAKE3 are instances). reconstructWith h leaf prf = rootHashWith h t.
verifyProofReconstructs(With)	verifyProofWith h root leaf prf = (root == reconstructWith h leaf prf).
reconstructAppendWith, powerTwoSucc, justInj	supporting lemmas.
buildGetLeaf (Stage 1.1)	constructor round-trip: getLeafHash (buildMerkleTree hs) (finToNat i) = Just (index i hs).
Ochrance.Util.VectLemmas (×5)	reusable transport/append lemmas: indexAppendLeft / indexAppendRight, indexReplace, finToNatReplace, splitAtConcat.
roundtripManifest + sub-codecs (algoRT, modeRT, refsRT, mpolRT, …)	grammar invertibility: decodeManifest (encodeManifest m) = Just m.
SatisfiesMinimum / attestedSatisfiesLax	progressive-assurance threshold witness.
ABI Handle / createHandle	So (ptr /= 0) non-null invariant discharged via choose.

4. The remaining proof program (dependency-sorted)

Each stage is sized to roughly one context window; the thread compacts at each boundary with this file as the hand-off. Watch-fors are things that may force a design change or a model downshift mid-stage.

4.1. Stage 1 — Merkle closure + crypto-binding interface [model: Opus]

1. [DONE — 1.1] buildMerkleTree ↔ getLeafHash round-trip: getLeafHash (buildMerkleTree hs) (finToNat i) = Just (index i hs) (buildGetLeaf in Ochrance.Filesystem.MerkleBuild, on the reusable Ochrance.Util.VectLemmas lemmas). Machine-checked, axiom-free, on main.

2. [1.2] Root-fold law: characterise rootHashWith h (buildMerkleTree hs) as a deterministic fold over hs — "the root is a function of the leaves". Pure; prerequisite of the binding argument.

3. [1.3] IO↔pure bridge: prove verifyProofIO / rootHashBytesIO compute the …With (hashPairBlake3 …) spec modulo the Either allocation-failure plumbing, against a typed combiner-equality hypothesis — connecting the proven theorem to the production crypto path. (The estate-wide spine; see "The IO↔pure bridge".)

4. [1.4] D2: introduce CollisionResistant h and state merkleBinding (typed hypothesis / interface; discharged in Stage 4).

   RESOLVED (was WATCH-FOR): the replace-by-powerTwoSucc transport in buildMerkleTree was discharged without reshaping the builder — via the indexReplace / finToNatReplace / splitAtConcat transport-cancellation lemmas in VectLemmas. No API change was forced.

4.2. Stage 2 — Verify + Validator soundness [model: Opus → Sonnet if mechanical]

1. Validator: validated manifest ⇒ structural invariants hold.

2. verifyState agrees with the manifest, wired to merkleCorrect.

3. Hex codec: hexStringToBytes (bytesToHex bs) = Just bs and the length law.

   WATCH-FOR: Verify and Hex likely rest on primitive String/Bits8 comparison — the same wall as the lexer round-trip. If so the honest theorem is propositional-over-decidable (document the boundary; do not reach for believe_me). This can shorten Stage 2 and justify a Sonnet downshift.

4.3. Stage 3 — Repair correctness (L3, linear types) [model: Opus]

PRECONDITION (surfaced at Compaction 2): repair is currently a stub — repairBlock (Repair.idr) updates the hash map but does not read or write block data. Proving verify (repair s) = Valid against a no-op would be vacuous or false. DECISION (recommended): introduce a pure repairPure : FSState → Manifest → FSState that genuinely reconstructs the hash map, prove correctness over that, and make the IO repair a proven-equivalent shell (the IO↔pure pattern). Alternative: leave repair honestly-bounded until real block-I/O lands (defers the linear-type theorem).

1. verifyPure (repairPure s m) m = True — the meaty (now well-founded) theorem.

2. Repair idempotence as a proof (today only a property test).

3. Harvest framework’s mode-indexed Interface; state the VerifiedSubsystem law verify (repair s m) m = Right … and prove the FSState instance satisfies it.

   WATCH-FOR: may need proof witnesses threaded through the 1-quantified API — possible signature changes to Repair.idr.

4.4. Stage 4 — Completeness, binding discharge, write-up [model: Sonnet; Opus if binding is hard]

1. Merkle completeness (converse of soundness): in-range leaf ⇒ a proof exists.

2. D2 discharge: prove the binding argument against CollisionResistant.

3. Progressive monotonicity: the remaining SatisfiesMinimum cases (all Refl).

4. Final ledger pass; thesis-aligned summary (ICFP/PLDI/SOSP framing).

CLEAR = every intended theorem proven or honestly bounded (primitive walls documented, never faked), disposed tracks handed off, PRs landed.

5. The IO↔pure bridge (estate-wide spine)

The same device recurs at every IO boundary — Merkle (1.3), Verify (2.2), Repair (3), signatures (4 / bounded). The shape is always:

pure spec (proven) --[extensional-equality lemma]--> IO production path
                                                     (modulo `Either`
                                                      allocation-failure +
                                                      a typed crypto hypothesis)

Treating this as one architectural pattern — not four ad-hoc stage items — is what lets the proven backdrop reach production code without ever faking the FFI. The typed crypto hypotheses (CollisionResistant h; hashPairBlake3 a b equals the spec combiner) are introduced in Stage 1.4 and discharged-or-assumed explicitly, never silently. It is also the mechanism that licenses optimisation (below).

6. Build-with-proofs discipline

The invariant: code never outstrips proofs. Operationally —

1. A correctness-claiming public export symbol lands only when (a) it carries its lemma in the same PR, or (b) it is explicitly -- UNPROVEN:-marked with a tracking issue, or (c) it is a documented honestly-bounded wall. No silent (d).

2. The --total CI build is the totality proof (already enforced) — a green build is the floor, not the ceiling.

3. No proving stubs. If an implementation is a placeholder (Repair today), make it real or model it purely first — never point a theorem at a no-op.

4. This ledger’s proven-surface table is the source of truth; README / TOPOLOGY must not claim beyond it.

7. Optimisation ledger (against the proven backdrop)

Governing principle: the proven surface is exactly the code you may optimise — the proof is the optimisation’s regression contract. Keep the simple reference R (proven), introduce optimised F, discharge F x = R x, and every theorem about R transports to F by rewrite. Never optimise unproven code (nothing guards it).

Target	Optimisation	Guard	Status
buildMerkleTree	bottom-up O(n) fold from the flat vector (vs. per-level replace/splitAt)	buildFast hs = buildMerkleTree hs ⇒ buildGetLeaf transports	unlocked now
getLeafHash	thread a Fin index; drop Nat minus/<	getLeafFast t i = getLeafHash t (finToNat i)	unlocked now
generateProof / reconstruct	difference-list / vector path (vs. List append per step)	reconstructAppendWith + merkleCorrectWith	unlocked now
root combiner	real BLAKE3 in IO (vs. abstract h)	the Stage 1.3 bridge lemma	after 1.3
A2ML production parser	any fast String parser	roundtripManifest + runtime roundtripProperty net	bounded (prim. wall)
Repair (incremental / CoW)	touch only broken blocks	verify (repair s) = Valid	after Stage 3

8. Honestly-bounded items (NOT failures — boundaries by design)

• Production-pipeline round-trip (parse . lex . serialize = Right m) cannot carry a compile-time theorem: pack/unpack/parseInteger are primitives with no equational theory. The honest guarantee is roundtripManifest over a reference token codec, complemented by roundtripProperty at runtime.

• root == root Bool step in merkleCorrect: the propositional digest equality is the strongest honest statement; discharging the residual primitive-Bits8 == would need an unsafe reflexivity axiom.

9. Disposed tracks (handoff briefs)

These are not this thread’s work. Each is a brief for a delegated session, disposed at Compaction 1. Specs live here so nothing is lost.

9.1. svalinn — migrate ReScript → Ephapax, then verify [model: Sonnet]

PRECONDITION: language migration precedes proof (Decision D3). The first deliverable is a migration map (the critical chain of blockers) — handed to an offline Claude with hyperpolymath/ephapax access, targeting svalinn/docs/ephapax-migration/BLOCKER-LINEAGE.adoc. ROOT of that chain, and the one thing this session could not settle (ephapax is out of scope here): whether Ephapax is yet an implementable application language (compiler, runtime, HTTP/async I/O, JSON, fetch, crypto, FFI) or still a proof-level calculus.

1. Migrate ReScript → Ephapax (gateway, auth, policy, validation, MCP, vörðr, compose; ~27 src/ modules + the ui/ ReScript frontend). Typed boundary decoders make the 20+ Obj.magic casts in security paths impossible.

2. Ephapax linear tokens for exactly-once resources: JWT/JTI single-use + the revocation ledger (fixes the hasRevocationList = false // TODO hazard by construction), OAuth nonce/PKCE, session/container lifecycle, vörðr delegation.

3. Unblock CI: the 53 ReScript unit/security tests don’t execute under Deno (@rescript/core resolution) — they vanish with the migration; ensure the Ephapax suite runs in CI. (svalinn main CI is currently red on pre-existing ReScript breakage — do not fix it in ReScript; it is being replaced.)

4. Specs to discharge after migration (language-agnostic): policy determinism; allow ∩ deny composition + monotonicity; JWT single-use & revocation; no unchecked boundary casts; JSON-Schema conformance of all 9 gateway types.

5. Planned SPARK properties (cerro-torre-integration.adoc §6.2): attestation sig, key lookup, threshold sig, log inclusion, policy eval.

   DEPENDENCY: Ephapax has 3 Admitted (Coq) — svalinn’s linear guarantees inherit those holes until closed. Track upstream.

   DISCHARGES: svalinn security issue #13 (19 Critical/High panic-attack findings — decodeJwt() without jwtVerify(), JSON.parseExn) is addressed structurally by this migration (verified JWT + typed deserialisation), not by patching ReScript.

   RE-ENTRY: the outbound charter now lives at svalinn/docs/ephapax-migration/HANDOFF.adoc; when this track returns, read docs/AFTER-MIGRATION.adoc (the round-trip closure) before resuming the campaign.

9.2. ochrance-framework — retire core, harvest Interface, keep docs [model: Sonnet]

1. Delete ochrance-framework/ochrance-core; make the repo depend on / reference the canonical ochrance core.

2. Harvest the mode-indexed VerifiedSubsystem Interface into ochrance (Stage 3).

3. Fix the weak spots that should not be carried over: decodeSnapshot always returns Nothing (repair unreachable); signatureValid : Bool and allPresent : Bool are unguarded runtime flags; no totality gate in CI.

4. Keep and maintain the docs — they are the framework repo’s real value.

9.3. ochrance ABI / Zig FFI hardening [model: Sonnet/Haiku]

1. blake3Hash in src/abi/Ochrance/ABI/Foreign.idr is covering + a stub returning replicate 32 0 — wire it to the real Zig libochrance BLAKE3.

2. ECHIDNA FFI is entirely stubbed (echidnaProve returns Left "FFI not yet implemented").

9.4. CI watch — PR #32 [model: Haiku/Sonnet]

Keep PR #32 (combiner generalisation) shepherded to green; it is subscribed.

10. Model guidance (per the thread’s operating model)

Model	Use
Opus 4.8	Proof discovery — "is this provable, what is the shape": Stages 1, 3, and any novel theorem or structural-wall reasoning.
Sonnet 4.6	Proof mechanisation (known shape), refactors, tests, and the disposed-track application work (svalinn Ephapax migration, framework, ABI).
Haiku 4.5	Grunt sweeps — suites, grep, SPDX/format, CI watch.

RULE: when a stage’s remaining work is all mechanical, downshift this thread to Sonnet to conserve Opus budget; when a research-grade wall appears, pause for the design conversation rather than pushing proofs.