proof: total bodies for VerifierSpecAgreement + SourceVerifierAgreement (items 7 + 8)

[hyperpolymath]

Summary

Closes the multi-week residual flagged by PR #74's design-pass: the two agreement records introduced by PR #72 (VerifierSpecAgreement, SourceVerifierAgreement) now have concrete inhabitants with totally proven bodies in every direction. Zero believe_me, zero postulate, %default total preserved.

This is an alternative-design PR to the stacked chain #72 → #74. It does not depend on either landing; it builds straight off main with a single new module (src/abi/TypedWasm/ABI/VerifierSpec.idr).

Design choice that unblocks the full bodies

VADifferential / SADifferential now carry the structural witness the differential harness attested — packaged inline via an embedded TrustedFixture m:

data VerifierAccepts : ModuleSummary -> Type where
  VAStructural   : FunctionsAccepted m.functions -> VerifierAccepts m
  VADifferential : (fixture : TrustedFixture m)  -> VerifierAccepts m

record TrustedFixture (m : ModuleSummary) where
  constructor MkTrustedFixture
  trustedFixtureName : String
  trustedFixtureId   : Nat
  trustedWitness     : FunctionsAccepted m.functions

differentialAccepted :
     (fixtureName : String) -> (fixtureId : Nat)
  -> FunctionsAccepted m.functions
  -> VerifierAccepts m

The trust-injection moment is exactly the act of constructing one — fixture name + id never travel without the structural witness the harness's accept-verdict establishes. Every MkTrustedFixture is a single grep point for audit.

Consequence: all four agreement lemmas become total by case analysis. Both VAStructural and VADifferential surface a FunctionsAccepted m.functions payload that wraps directly into SpecAccepts; the spec-to-verifier direction lifts via VAStructural; source ↔ verifier mirror the same pattern.

verifierIsSound : (m : ModuleSummary) -> VerifierAccepts m -> SpecAccepts m
verifierIsSound _ (VAStructural   fa) = MkSpecAccepts fa
verifierIsSound _ (VADifferential tf) = trustedToSpec tf

verifierIsComplete : (m : ModuleSummary) -> SpecAccepts m -> VerifierAccepts m
verifierIsComplete _ (MkSpecAccepts fa) = VAStructural fa

Comparison with PR #74 (Maybe-returning bridges)

PR #74 keeps VADifferential opaque (string + nat only) and exposes Maybe-returning bridges plus a closed-world RegisteredFixture GADT. Soundness/completeness for the unparameterised agreement records remain unprovable in that design — explicitly noted in #74 as "multi-week residual".

This PR refactors the data type instead. The audit story is preserved (every MkTrustedFixture is a single grep point), but the agreement records cease to be obligations and become inhabited records like any other.

The two designs are mutually exclusive at the data-type level (VADifferential's payload differs). If both PRs are wanted in evolved form, #74's RegisteredFixture machinery composes cleanly on top of this PR's witness-carrying ctors as a tighter audit layer.

What's in the module

Single file (~620 LOC, zero banned patterns):

• OwnershipIntent / FunctionSummary / ModuleSummary — shared spec surface
• TokenFresh / IntentsLinearAcceptable / FunctionsAccepted — structural acceptance predicates the three sides share at L7+L10
• TrustedFixture m — packaged differential-harness attestation
• SpecAccepts / VerifierAccepts / SourceAccepts — three predicates; the latter two have a *Differential ctor carrying a TrustedFixture
• differentialAccepted / sourceAccepted — smart constructors that thread the structural witness through
• trustedToSpec / trustedToVerifier / trustedToSource — projections
• The four agreement lemmas, total bodies: verifierIsSound, verifierIsComplete, sourceImpliesVerifier, verifierImpliesSource
• record VerifierSpecAgreement / record SourceVerifierAgreement — record shapes match PR proof: A10 + A11 + A12 — close 2 named + 6 untracked proof-debt items (19 theorems, 50/50 regression) #72
• verifierSpecAgreement / sourceVerifierAgreement — concrete inhabitants, the first total no-believe_me such values in the codebase
• sourceImpliesSpec / specImpliesSource + *Concrete specialisations — end-to-end composition lemmas
• Concrete instances: empty module, allocFreeModule, plus fixtureCleanLinearConsumerModule mirrored from cross_compat row 1 — exercises the differential path end-to-end through the agreement record
• Discrimination: notSpecAcceptsBadDoubleConsume, notVerifierAcceptsBadDoubleConsume (both ctors), notSourceAcceptsBadDoubleConsume (both ctors), notSpecAcceptsBadDoubleProduce — show L10 has teeth and the differential escape hatch can't smuggle a bad module past the verifier

Regression

tests/proof/regression.mjs gains 33 Layer 1 grep assertions covering every new top-level name (data ctors, lemmas, records, concrete witnesses, discrimination proofs). Layer 2 (Idris2 --build of the ipkg) verified locally.

While here, fixed a pre-existing latent bug: Layer 2 invoked idris2 --check typed-wasm.ipkg, which the Idris2 0.8.0 CLI rejects (--check takes a single .idr path, not an ipkg). Changed to --build. CI was unaffected because it skips Layer 2 (idris2 not on PATH in e2e.yml); local strict runs now actually exercise it.

Build oracle

IDRIS2_PREFIX=$IDRIS2/0.8.0 idris2 --build src/abi/typed-wasm.ipkg

22/22 modules, rc=0, no warnings from the new module.

PATH=$IDRIS2/0.8.0/bin:$PATH \
IDRIS2_PREFIX=$IDRIS2/0.8.0 \
  node tests/proof/regression.mjs --strict
# 59 passed, 0 failed, 0 skipped

Test plan

• CI E2E build green (Idris2 + regression)
• CI cargo build green
• CI governance + dogfood + scanners green
• Owner review of the design choice (witness-carrying ctor vs PR proof: items 7+8 — design pass + first concrete structural agreement witnesses (stacked on #72) #74's Maybe bridges)

🤖 Generated with Claude Code