Proof bodies for VerifierSpecAgreement / SourceVerifierAgreement (statements landed in #79; bodies are long-tail)

[hyperpolymath]

Context

PR #79 ("proof: total bodies for VerifierSpecAgreement + SourceVerifierAgreement (items 7 + 8)") landed statement-level records for both agreements in src/abi/TypedWasm/ABI/VerifierSpec.idr. Each is a bundle of soundness + completeness, with composition lemmas sourceImpliesSpec / specImpliesSource connecting them.

Per the A13 follow-up note in the audit memory:

Long-tail tracked elsewhere (NOT in this audit anymore):

• Full proof bodies for VerifierSpecAgreement / SourceVerifierAgreement

This issue tracks that long-tail explicitly so it doesn't get lost when the audit memory archives.

What's needed

Full proof bodies (not statement-level records) for:

1. VerifierSpecAgreement — bridges SpecAccepts m (Idris2 L7+L10 acceptance over ModuleSummary / FunctionSummary / OwnershipIntent) and VerifierAccepts m (opaque, witnessed by Rust differential harness via differentialAccepted).
2. SourceVerifierAgreement — bridges SourceAccepts m (opaque, witnessed by source-side harness) and VerifierAccepts m.

The current bodies are total by case analysis on the bundled VADifferential / SADifferential structural witnesses (TrustedFixture m). Closing this issue means either discharging those bodies to constructive proofs or documenting the trust-injection moment formally (single grep point: MkTrustedFixture construction).

Why this is multi-session

• Requires either WasmCert-Isabelle tie-back (separate long-tail item) for one of the two directions, OR
• A constructive proof of the Rust verifier's soundness, OR
• An explicit ADR documenting TrustedFixture as the audit boundary.

This is design work, not refactoring. Owner-prioritised, not auto-discharge-able.

Cross-references

• PR proof: total bodies for VerifierSpecAgreement + SourceVerifierAgreement (items 7 + 8) #79 (statement-level landing): commit 06ec00e in main.
• Mutually-exclusive design alternative at proof: items 7+8 — design pass + first concrete structural agreement witnesses (stacked on #72) #74 (Maybe-returning bridges + RegisteredFixture GADT). Owner picks one shape; the other's machinery can compose on top if both ideas wanted.
• Memory entry: project_typed_wasm_proof_debt_post_a10 — long-tail section.
• Discovered as still-outstanding during paired-review of proposal 0001 (ephapax#165 + affinescript#402, 2026-05-30).

Refs #48