Skip to content

Commit 5adea82

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
proof: extended allocFreeModule + ExtendedAgreement constructive bridge
Two additions on top of the structural agreement work in 1d09ef6 + 3678d64. 1. Extended allocFreeModule exercising all four OwnershipIntent constructors in a single witness. allocFreeWithBorrowModule has four functions exercising the full constructor set: * alloc : [Produces 0] * read : [Borrows 1] * update : [BorrowsExclusive 2] * free : [Consumes 0] Witnesses constructed: allocFreeWithBorrowSpecAccepts, allocFreeWithBorrowVerifierAccepts, allocFreeWithBorrowSourceAccepts. Confirms the structural witness machinery handles ILAProduces, ILABorrows, ILABorrowsExclusive, ILAConsumes in a single FunctionsAccepted spine. Two further discrimination paths now exist alongside the Consumes/Consumes case in 3678d64: * badDoubleProduceModule — [Produces 0, Produces 0] rejected via TFProducesOther / Refl pattern. * badConsumeProduceMixModule — [Consumes 0, Produces 0] rejected via TFProducesOther inside an ILAConsumes shell. These exercise distinct constructor combinations in the rejection witness, showing the L10 single-occurrence rule applies regardless of intent direction. 2. ExtendedAgreement — constructive bridge from VADifferential to structural acceptance. The structuralAgreement value (commit 1d09ef6) closes the structural sublattice but leaves VADifferential witnesses dangling: no provable VerifierAccepts → SpecAccepts function exists for the differential case because a fixture name + id alone carry no structural information. ExtendedAgreement relocates the trust-injection from "every VADifferential consumer" to "fixture registration time": * record TrustedFixture m — pairs a fixture name + id with the structural witness the fixture is claimed to certify. Constructing one IS the trust-injection moment. Grep MkTrustedFixture to enumerate every fixture trust-injection in the codebase. * trustedToVerifier / trustedToSpec / trustedToSource — project a TrustedFixture to each of the three acceptance predicates via the structural constructor. No further trust at use site. * record ExtendedAgreement — StructuralAgreement plus a fixtureLookup mapping (module, name, id) to Maybe TrustedFixture. * emptyExtendedAgreement — concrete inhabitant with the empty lookup; future fixture audits replace the lookup with non-empty dispatchers. * verifierImpliesSpecExtended / sourceImpliesSpecExtended — total functions promoting VerifierAccepts / SourceAccepts to Maybe SpecAccepts via the extended agreement. Structural witnesses pass through; differential witnesses consult the fixture registry. Net effect: the VerifierSpecAgreement / SourceVerifierAgreement records (still obligations for the unconditional case) now have a constructive sibling that's provable up to fixture registration — a concrete shape for the multi-week residual rather than a "multi-week TODO". Idris2 0.8.0 build green: 22/22 modules. Zero new believe_me, assert_total, postulate, sorry, assert_smaller. %default total preserved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 3678d64 commit 5adea82

1 file changed

Lines changed: 218 additions & 0 deletions

File tree

‎src/abi/TypedWasm/ABI/VerifierSpec.idr‎

Lines changed: 218 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -561,3 +561,221 @@ notVerifierStructuralAcceptsBadDoubleConsume :
561561
notVerifierStructuralAcceptsBadDoubleConsume
562562
(FACons (ILAConsumes (TFConsumesOther noteq _) _) _) =
563563
noteq Refl
564+
565+
||| A second L10 rejection path: `[Produces 0, Produces 0]`.
566+
||| The L10 single-consumption rule forbids any token from appearing
567+
||| twice in a function's intent list, regardless of `Consumes` /
568+
||| `Produces` direction. Distinct from `badDoubleConsumeModule`
569+
||| because it exercises the `ILAProduces` / `TFProducesOther`
570+
||| constructor pair instead of the `ILAConsumes` / `TFConsumesOther`
571+
||| pair.
572+
public export
573+
badDoubleProduceModule : ModuleSummary
574+
badDoubleProduceModule = MkModuleSummary "badDoubleProduce"
575+
[ MkFunctionSummary "doubleAlloc" [Produces 0, Produces 0]
576+
]
577+
578+
||| The spec does not accept `badDoubleProduceModule`. Mirror of
579+
||| `notSpecAcceptsBadDoubleConsume` for the `Produces` branch.
580+
public export
581+
notSpecAcceptsBadDoubleProduce :
582+
Not (SpecAccepts VerifierSpec.badDoubleProduceModule)
583+
notSpecAcceptsBadDoubleProduce
584+
(MkSpecAccepts (FACons (ILAProduces (TFProducesOther noteq _) _) _)) =
585+
noteq Refl
586+
587+
||| A third L10 rejection path: a token mixes `Consumes` with
588+
||| `Produces` in the same function. `[Consumes 0, Produces 0]`
589+
||| violates the per-function single-occurrence rule because the
590+
||| `ILAConsumes` constructor demands `TokenFresh 0 [Produces 0]`,
591+
||| which only `TFProducesOther` can witness, which in turn requires
592+
||| `Not (0 = 0)`.
593+
public export
594+
badConsumeProduceMixModule : ModuleSummary
595+
badConsumeProduceMixModule = MkModuleSummary "badConsumeProduceMix"
596+
[ MkFunctionSummary "mixed" [Consumes 0, Produces 0]
597+
]
598+
599+
||| The spec does not accept `badConsumeProduceMixModule`. Exercises
600+
||| the cross-direction case: the rejection witness is
601+
||| `TFProducesOther (Not (0 = 0)) _` inside an `ILAConsumes` shell.
602+
public export
603+
notSpecAcceptsBadConsumeProduceMix :
604+
Not (SpecAccepts VerifierSpec.badConsumeProduceMixModule)
605+
notSpecAcceptsBadConsumeProduceMix
606+
(MkSpecAccepts (FACons (ILAConsumes (TFProducesOther noteq _) _) _)) =
607+
noteq Refl
608+
609+
-- ============================================================================
610+
-- Extended allocFreeModule — exercises all four OwnershipIntent
611+
-- constructors (Produces / Consumes / Borrows / BorrowsExclusive)
612+
-- ============================================================================
613+
--
614+
-- The base `allocFreeModule` exercises only the linear pair
615+
-- (Produces 0 / Consumes 0). The extended variant adds a borrowing
616+
-- pattern alongside, exercising both `Borrows` (read-only) and
617+
-- `BorrowsExclusive` (mutable), and shows the structural witness
618+
-- machinery handles all four constructors in a single module.
619+
--
620+
-- Schema tags 1 and 2 are used so the borrow intents don't collide
621+
-- structurally with the linear token 0 (which lives in a separate
622+
-- index namespace anyway, but keeping them distinct makes the
623+
-- intent table easier to read).
624+
625+
||| Demo module exercising all four `OwnershipIntent` constructors.
626+
|||
627+
||| * `alloc` produces a linear handle (token 0).
628+
||| * `read` borrows schema 1 (read-only).
629+
||| * `update` borrows schema 2 exclusively (mutable).
630+
||| * `free` consumes the linear handle.
631+
public export
632+
allocFreeWithBorrowModule : ModuleSummary
633+
allocFreeWithBorrowModule = MkModuleSummary "allocFreeWithBorrow"
634+
[ MkFunctionSummary "alloc" [Produces 0]
635+
, MkFunctionSummary "read" [Borrows 1]
636+
, MkFunctionSummary "update" [BorrowsExclusive 2]
637+
, MkFunctionSummary "free" [Consumes 0]
638+
]
639+
640+
||| Spec acceptance witness for `allocFreeWithBorrowModule`. Exercises
641+
||| `ILAProduces` / `ILABorrows` / `ILABorrowsExclusive` / `ILAConsumes`
642+
||| in a single witness — the full four-constructor coverage of
643+
||| `IntentsLinearAcceptable`.
644+
public export
645+
allocFreeWithBorrowSpecAccepts :
646+
SpecAccepts VerifierSpec.allocFreeWithBorrowModule
647+
allocFreeWithBorrowSpecAccepts = MkSpecAccepts
648+
(FACons (ILAProduces TFNil ILANil)
649+
(FACons (ILABorrows ILANil)
650+
(FACons (ILABorrowsExclusive ILANil)
651+
(FACons (ILAConsumes TFNil ILANil)
652+
FANil))))
653+
654+
||| Verifier acceptance for the four-constructor demo module, derived
655+
||| via `specImpliesVerifierStructural`.
656+
public export
657+
allocFreeWithBorrowVerifierAccepts :
658+
VerifierAccepts VerifierSpec.allocFreeWithBorrowModule
659+
allocFreeWithBorrowVerifierAccepts =
660+
specImpliesVerifierStructural allocFreeWithBorrowSpecAccepts
661+
662+
||| Source-checker acceptance for the four-constructor demo module.
663+
public export
664+
allocFreeWithBorrowSourceAccepts :
665+
SourceAccepts VerifierSpec.allocFreeWithBorrowModule
666+
allocFreeWithBorrowSourceAccepts =
667+
specImpliesSourceStructural allocFreeWithBorrowSpecAccepts
668+
669+
-- ============================================================================
670+
-- ExtendedAgreement — constructive bridge from VADifferential to spec
671+
-- ============================================================================
672+
--
673+
-- The `StructuralAgreement` value above closes the structural
674+
-- sublattice but leaves `VADifferential` evidence dangling: there is
675+
-- no provable `(m : ModuleSummary) -> VerifierAccepts m -> SpecAccepts m`
676+
-- that handles `VADifferential` cases, because a fixture name + id
677+
-- alone carry no structural information.
678+
--
679+
-- The trust pattern below relocates the trust-injection moment from
680+
-- "every VADifferential witness use" to "fixture registration time".
681+
-- A `TrustedFixture` packages a fixture name + id with the structural
682+
-- witness the fixture is claimed to certify. Constructing a
683+
-- `TrustedFixture` IS the trust-injection — but once constructed, the
684+
-- witness is structural, so downstream proofs of agreement use the
685+
-- structural directions only.
686+
--
687+
-- This is the constructive bridge: the trust still has to be injected
688+
-- somewhere (because the Rust verifier inspects wasm bytes; Idris2
689+
-- cannot do that itself), but it's injected once per fixture, with
690+
-- the fixture name pinned in the witness type, instead of being
691+
-- injected anew at every consumer of `VerifierSpecAgreement`.
692+
693+
||| A trusted fixture: pairs the differential evidence (fixture name +
694+
||| id) with the structural witness the fixture is supposed to
695+
||| certify. Constructing one is the trust-injection moment. Search
696+
||| for `MkTrustedFixture` to enumerate every fixture trust-injection.
697+
public export
698+
record TrustedFixture (m : ModuleSummary) where
699+
constructor MkTrustedFixture
700+
trustedFixtureName : String
701+
trustedFixtureId : Nat
702+
trustedWitness : FunctionsAccepted m.functions
703+
704+
||| A `TrustedFixture` projects to `VerifierAccepts` via the
705+
||| structural constructor — no further trust injection at use site.
706+
public export
707+
trustedToVerifier : TrustedFixture m -> VerifierAccepts m
708+
trustedToVerifier (MkTrustedFixture _ _ w) = VAStructural w
709+
710+
||| A `TrustedFixture` projects to `SpecAccepts` similarly.
711+
public export
712+
trustedToSpec : TrustedFixture m -> SpecAccepts m
713+
trustedToSpec (MkTrustedFixture _ _ w) = MkSpecAccepts w
714+
715+
||| A `TrustedFixture` projects to `SourceAccepts` similarly.
716+
public export
717+
trustedToSource : TrustedFixture m -> SourceAccepts m
718+
trustedToSource (MkTrustedFixture _ _ w) = SAStructural w
719+
720+
||| `ExtendedAgreement` — `StructuralAgreement` plus a fixture lookup.
721+
||| A consumer with an `ExtendedAgreement` and a `VADifferential`
722+
||| witness can ask the lookup for the matching `TrustedFixture` and
723+
||| obtain a structural witness — turning the dangling differential
724+
||| case into a structural one.
725+
|||
726+
||| The lookup returns `Maybe` because not every fixture name will be
727+
||| registered. An empty `ExtendedAgreement` (returning `Nothing`
728+
||| everywhere) trivially exists; populated ones grow as fixtures are
729+
||| audited. See `emptyExtendedAgreement` for the empty witness.
730+
public export
731+
record ExtendedAgreement where
732+
constructor MkExtendedAgreement
733+
baseStructural : StructuralAgreement
734+
fixtureLookup :
735+
(m : ModuleSummary)
736+
-> (fixtureName : String)
737+
-> (fixtureId : Nat)
738+
-> Maybe (TrustedFixture m)
739+
740+
||| The empty `ExtendedAgreement`: structural agreement plus a lookup
741+
||| that returns `Nothing` for every fixture. Concrete inhabitant
742+
||| showing the record is constructible without external trust.
743+
||| Future fixture audits replace the lookup with non-empty
744+
||| dispatchers.
745+
public export
746+
emptyExtendedAgreement : ExtendedAgreement
747+
emptyExtendedAgreement = MkExtendedAgreement
748+
structuralAgreement
749+
(\_, _, _ => Nothing)
750+
751+
||| Promote a `VADifferential` witness to `SpecAccepts` using an
752+
||| `ExtendedAgreement`. Returns `Nothing` if the fixture is not
753+
||| registered. Total — no `believe_me`, no `assert_total`.
754+
|||
755+
||| This is the constructive bridge promised by the section header:
756+
||| a `VADifferential` witness plus a registered fixture produces a
757+
||| structural-grade spec acceptance.
758+
public export
759+
verifierImpliesSpecExtended :
760+
ExtendedAgreement
761+
-> (m : ModuleSummary)
762+
-> VerifierAccepts m
763+
-> Maybe (SpecAccepts m)
764+
verifierImpliesSpecExtended _ _ (VAStructural fa) =
765+
Just (MkSpecAccepts fa)
766+
verifierImpliesSpecExtended ext m (VADifferential name fid) =
767+
map trustedToSpec (ext.fixtureLookup m name fid)
768+
769+
||| Symmetric direction: `SADifferential` to `SpecAccepts` via the
770+
||| same fixture-lookup mechanism. Both source and verifier
771+
||| differential cases route through the same fixture registry.
772+
public export
773+
sourceImpliesSpecExtended :
774+
ExtendedAgreement
775+
-> (m : ModuleSummary)
776+
-> SourceAccepts m
777+
-> Maybe (SpecAccepts m)
778+
sourceImpliesSpecExtended _ _ (SAStructural fa) =
779+
Just (MkSpecAccepts fa)
780+
sourceImpliesSpecExtended ext m (SADifferential name fid) =
781+
map trustedToSpec (ext.fixtureLookup m name fid)

0 commit comments

Comments
 (0)