diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 1d6417e..c68b9ed 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -25,5 +25,5 @@ permissions: jobs: hypatia: - uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@97df762107501909f50bb770e9bc200b6c415600 + uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@915139d73560e65a8240b8fc7768698658502c89 secrets: inherit diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 488532b..7c879d3 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -6,9 +6,9 @@ [metadata] project = "typed-wasm" version = "0.1.0" -last-updated = "2026-05-25" +last-updated = "2026-05-27" status = "active" # active | paused | archived -session = "2026-05-24/25 — Phase 0 closure pass. 11 PRs landed (#46 CI triage, #47 PRODUCTION-PATH doc, #55 cargo-audit CI, #57 Track C complete +64 assertions and 2 real bugs fixed, #58 tree-sitter scaffold, #59 CI hardening non-blocking, #60 ROADMAP truthfulness audit + drift-detection aspect §8, #61 wiki source-of-truth + STATE.a2ml comprehensive, #62 tree-sitter v1 parses example 01 end-to-end with 0 ERROR, #63 repo tidy RSR-aligned + smoke fix + duplication scrub). Phase 0 gates 1 + 3 met; gate 2 (codegen v0) is the terminal Phase-1-handoff item." +session = "2026-05-26/27 — Proof-debt pass A10+A11+A12+A13 (PR #72) + A14+A15+A16+A17 (PR #74). A10 closes the last 2 NAMED deferred items from PROOF-NEEDS (L12 freshness propagation under concurrent writes via 8 theorems incl. `freshnessPropagatesUnderWrites` + `epistemicFreshness` projector; `compatCommute` mutual-subschema case + `noSpoofingBidir` corollary + 2nd worked example). Also fixed `tests/proof/regression.mjs` Layer 2 from silent no-op `--check` to real `--build`. A11 closes 3 of 8 untracked debts: (1) `Sync.WriteSync` now requires a `FieldVersion` witness; (2) `Knowledge.Observed` grounded in a `Sync` event; (4-partial) first algebraic laws for `composeCertificates`. A12 closes 3 MORE untracked items: item 4 FULL; item 6; item 3 (L8↔L15). A13 closes the rest: items 5a/5b cross-level, leave-behind, items 7+8 stated as typed obligations in new `TypedWasm.ABI.VerifierSpec`. A14 (PR #74) reshapes the items 7+8 predicates non-opaque (VAStructural/VADifferential split), adds `structuralAgreement` + `emptyExtendedAgreement` + `TrustedFixture` + `ExtendedAgreement` + 6 structural agreement directions + 4 discrimination proofs + `verifierImpliesSpecExtended` / `sourceImpliesSpecExtended` Maybe-returning bridges. A15 extends fixture coverage with `fixtureExtractExportsTrusted` (cross_compat row 9) + `fixtureRealisticCleanTrusted` (row 10). A16 builds the first non-empty `ExtendedAgreement` via manual `DecEq OwnershipIntent`/`FunctionSummary`/`ModuleSummary` + `liftTrustedFixture` + `fixtureLookupDispatching` + `firstExtendedAgreement`. A17 adds closed-world evidence track: `data RegisteredFixture : ModuleSummary -> Type` GADT + `fixtureFromEvidence` + 6 projector Refl round-trips + Maybe-FREE `verifierImpliesSpecEvidence` / `sourceImpliesSpecEvidence` bridges. Build green 22/22 modules under Idris2 0.8.0, regression 68→118. CI infrastructure fix: orphan-SHA repin (97df762 → 915139d7) for hypatia-scan reusable, swept across ~99 estate repos (PR #75 + estate sweep + standards#220 audit doc). Previous session (2026-05-24/25): Phase 0 closure pass landed 11 PRs (#46..#63)." [project-context] name = "typed-wasm" @@ -51,11 +51,28 @@ milestones = [ { name = "Wiki source-of-truth at docs/wiki/", completion = 100 }, # 2026-05-25 (PR #61) { name = "RSR-template taxonomy alignment (AUDIT.adoc + onboarding/status/proposals stubs)", completion = 100 }, # 2026-05-25 (PR #63) { name = "Parser migration ReScript -> AffineScript -> Idris2", completion = 50 }, # ReScript->AffineScript landed; AffineScript->Idris2 still ahead + { name = "L12 (Epistemic) freshness propagation proof", completion = 100 }, # 2026-05-26 (A10, PR #72) — closes PROOF-NEEDS §P1.2 + { name = "MultiModule mutual-subschema commutativity (compatCommute)", completion = 100 }, # 2026-05-26 (A10, PR #72) + { name = "Sync/Knowledge constructor provenance tightening", completion = 100 }, # 2026-05-26 (A11, PR #72) — closes post-A10 audit items 1 + 2 + { name = "composeCertificates algebraic laws", completion = 100 }, # 2026-05-26 — A11 list-side + A12 full assoc/comm (PR #72) — switched to Data.Nat.minimum, closes audit item 4 + { name = "Region byte-disjointness predicate + symmetry", completion = 100 }, # 2026-05-26 (A12, PR #72) — closes audit item 6; L7/L10 cross-level theorem deferred + { name = "L8 ↔ L15 joint budget composition theorem", completion = 100 }, # 2026-05-26 (A12, PR #72) — closes audit item 3 via jointBudgetCompose + { name = "L13 × L10 cross-level (linear handle across boundary)", completion = 100 }, # 2026-05-26 (A13, PR #72) — closes audit item 5a via LinearAcrossBoundary + linearTransferRequiresBoundary + { name = "L14 × L13 cross-level (session handle across boundary)", completion = 100 }, # 2026-05-26 (A13, PR #72) — closes audit item 5b via SessionAcrossBoundary + sessionAcrossPreservesState + sessionTransferRequiresBoundary + { name = "RegionDisjoint → byte non-overlap theorem (L7/L10 cross-level)", completion = 100 }, # 2026-05-26 (A13, PR #72) — A12 leave-behind via RegionsOverlap + disjointImpliesNoOverlap + { name = "Verifier ↔ Idris2 spec equivalence — STATEMENT", completion = 50 }, # 2026-05-26 (A13, PR #72) — VerifierSpec.idr: VerifierSpecAgreement obligation typed; full bodies multi-week + { name = "Source-checker ↔ verifier coverage agreement — STATEMENT", completion = 50 }, # 2026-05-26 (A13, PR #72) — VerifierSpec.idr: SourceVerifierAgreement obligation typed; full bodies multi-week + { name = "Items 7+8 STRUCTURAL agreement — first concrete value", completion = 100 }, # 2026-05-26 (A14, PR #74) — StructuralAgreement total + structuralAgreement concrete value + 6 agreement directions + 4 discrimination proofs + 4 empty-module inhabitants + allocFreeModule + allocFreeWithBorrowModule + { name = "TrustedFixture / ExtendedAgreement constructive bridge (differential case)", completion = 100 }, # 2026-05-26 (A14, PR #74) — record TrustedFixture + 3 projections + record ExtendedAgreement + emptyExtendedAgreement + verifierImpliesSpecExtended + sourceImpliesSpecExtended + { name = "Fixture coverage — cross_compat rows 1/9/10 as TrustedFixtures", completion = 100 }, # 2026-05-26 (A14+A15, PR #74) — fixtureCleanLinearConsumerTrusted (row 1, A14) + fixtureExtractExportsTrusted (row 9, A15) + fixtureRealisticCleanTrusted (row 10, A15); rows 2-8 out-of-scope for summary-level spec + { name = "First non-empty ExtendedAgreement (decEq dispatch)", completion = 100 }, # 2026-05-26 (A16, PR #74) — manual DecEq OwnershipIntent/FunctionSummary/ModuleSummary + liftTrustedFixture + fixtureLookupDispatching + firstExtendedAgreement; round-trip-to-named-fixture lemmas blocked by decEq String asymmetric reduction + { name = "RegisteredFixture GADT + Maybe-free evidence bridges", completion = 100 }, # 2026-05-27 (A17, PR #74) — data RegisteredFixture : ModuleSummary -> Type + fixtureFromEvidence + 6 projector Refl round-trips (name/id for rows 1/9/10) + verifierImpliesSpecEvidence + sourceImpliesSpecEvidence + { name = "CI infrastructure — hypatia-scan orphan-SHA fix", completion = 100 }, # 2026-05-26 (PR #75, sweep) — repin reusable from 97df762 (orphaned PR-branch SHA) to 915139d7 (merge-commit); estate sweep ~99 repos; standards#220 closure audit ] [blockers-and-issues] issues = [ - "L11-L12 research modules are not part of the checked package and currently fail standalone type-checking.", + "L11 (Tropical) remains research-only at the spec level; theorems live in-package but no surface or FFI exposure. L12 (Epistemic) is now spec-complete for freshness propagation (A10, 2026-05-26) but still lacks surface/FFI exposure.", "Venue-facing paper and benchmark claims still outrun the evidence present in-repo (now caught by tests/aspect/claim-envelope §8 drift detection).", "generated/abi/ C header pipeline not yet implemented (milestone at 0%).", "HostType F32 = Double in TypedAccess.idr — Idris2 lacks Float32; documented limitation.", @@ -80,15 +97,15 @@ actions = [ ] [maintenance-status] -last-run-utc = "2026-05-25T20:00:00Z" -last-report = "docs/PRODUCTION-PATH.adoc" # the canonical strategic doc supersedes one-off audit reports +last-run-utc = "2026-05-27T00:00:00Z" +last-report = "PROOF-NEEDS.md (RECONCILIATION 2026-05-26 A15/A16/A17 banner)" # A14+A15+A16+A17 are the active record; A17 GADT-evidence is the youngest layer last-result = "pass" # unknown | pass | warn | fail open-warnings = 4 # Build+E2E + A2ML + K9 non-blocking advisories (PR #59) + anti-pattern policy (fixed by Track A's ReScript cut) open-failures = 0 # all gating CI is green; previously-red jobs are explicitly advisory now [test-surface] # Test surface as of 2026-05-24; ~545 assertions across 11 surfaces. -total-assertions = 545 +total-assertions = 613 # 545→613: proof-regression bumped 50→68 by A13 (PR #72), 68→118 by A14+A15+A16+A17 (PR #74) surfaces = [ { name = "ParserTests.res", assertions = 88, file = "tests/parser/ParserTests.res" }, { name = "typed-wasm-verify (Rust)", assertions = 53, file = "crates/typed-wasm-verify/" }, # 43 unit + 10 cross-compat @@ -96,7 +113,7 @@ surfaces = [ { name = "claim-envelope aspect", assertions = 53, file = "tests/aspect/claim-envelope.mjs" }, # bumped 49→53 in PR #60 (new section 8 drift detection) { name = "security-envelope aspect", assertions = 10, file = "tests/aspect/security-envelope.mjs" }, # added 2026-05-24 (PR #57) { name = "property tests", assertions = 29, file = "tests/property/property_test.mjs" }, # added 2026-05-24 (PR #57) - { name = "proof regression", assertions = 25, file = "tests/proof/regression.mjs" }, # added 2026-05-24 (PR #57) + { name = "proof regression", assertions = 118, file = "tests/proof/regression.mjs" }, # 25→44 (A10+A11) → 50 (A12) → 68 (A13, PR #72) → ~92 (A14, PR #74) → 105 (A16, PR #74) → 118 (A17, PR #74): A14 added 2-ctor VerifierAccepts/SourceAccepts (VAStructural/VADifferential, SAStructural/SADifferential) + StructuralAgreement + emptyExtendedAgreement + TrustedFixture + first concrete fixture (row 1); A15 added rows 9+10 fixtures; A16 added DecEq machinery + fixtureLookupDispatching + firstExtendedAgreement; A17 added RegisteredFixture GADT + fixtureFromEvidence + 6 projector Refl round-trips + 2 Maybe-free constructive bridges { name = "smoke E2E", assertions = 40, file = "tests/smoke/e2e-smoke.mjs" }, { name = "structural E2E", assertions = 53, file = "tests/e2e.sh" }, { name = "integration (airborne-step)", assertions = 14, file = "tests/contracts/airborne-step-state-contract.mjs" }, diff --git a/CHANGELOG.md b/CHANGELOG.md index 4647415..c30169f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,6 +10,328 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +### Proof-debt pass A14 (2026-05-26, same-day continuation; PR #74) + +A13 (same-day, [#72](https://github.com/hyperpolymath/typed-wasm/pull/72)) +stated items 7 + 8 as typed obligations but kept the +`VerifierAccepts` / `SourceAccepts` predicates **opaque** (single +constructor carrying only an external-evidence string + fixture id). +That made every agreement direction unprovable without external +trust at every consumer site. + +A14 ([#74](https://github.com/hyperpolymath/typed-wasm/pull/74)) +reshapes the predicates and lands the first **concrete, total, +no-`believe_me`** agreement value in the codebase between spec / +verifier / source-checker. + +- **Design pass.** `VerifierAccepts` / `SourceAccepts` refactored to + inductive types with two constructors each: + - `VAStructural FunctionsAccepted` / `SAStructural FunctionsAccepted` + — backed by the same structural predicate the spec uses. No + trust-injection; introspectable in proofs. + - `VADifferential String Nat` / `SADifferential String Nat` — + external evidence pinned to a fixture row. Single audit point; + grep these constructors to enumerate every trust-injection site. + `SpecAccepts` refactored to wrap the new `FunctionsAccepted` + predicate, so spec / verifier / source-checker now share one + canonical structural witness shape at the L7+L10 layer. +- **First concrete agreement value.** `structuralAgreement : + StructuralAgreement` — total, no `believe_me`, no `postulate`, no + external trust — closes the structural sublattice of items 7 + 8. + Six new total functions: + `functionsAcceptedImpliesSpec` / `specImpliesFunctionsAccepted` + (round-trip), `specImpliesVerifierStructural` / + `specImpliesSourceStructural` (total — uses the structural + constructors directly), `verifierImpliesSpecStructural` / + `sourceImpliesSpecStructural` (return `Maybe`; differential case is + honestly `Nothing`). +- **Concrete inhabitants.** `emptyFunctionsAccepted`, + `emptyModuleSpecAccepts`, `emptyModuleVerifierAccepts`, + `emptyModuleSourceAccepts` — show the predicates aren't vacuously + empty. `allocFreeModule` + `allocFreeSpecAccepts` / + `allocFreeVerifierAccepts` / `allocFreeSourceAccepts` — first + non-empty witness, exercises `ILAProduces` / `ILAConsumes`. + `allocFreeWithBorrowModule` extends to all four + `OwnershipIntent` constructors with three witnesses each. +- **Discrimination — predicate has teeth.** Three rejection paths, + each exercising a distinct `TF*` / `ILA*` constructor combination: + - `notSpecAcceptsBadDoubleConsume` — `[Consumes 0, Consumes 0]` + rejected via `ILAConsumes` / `TFConsumesOther` / `Refl`. + - `notSpecAcceptsBadDoubleProduce` — `[Produces 0, Produces 0]` + rejected via `ILAProduces` / `TFProducesOther` / `Refl`. + - `notSpecAcceptsBadConsumeProduceMix` — `[Consumes 0, Produces 0]` + rejected via `ILAConsumes` / `TFProducesOther` / `Refl`. + Plus `notVerifierStructuralAcceptsBadDoubleConsume` showing the + structural verifier path is symmetric. +- **ExtendedAgreement — constructive bridge for VADifferential.** + `record TrustedFixture m` packages a fixture name + id with the + structural witness it certifies; constructing one IS the + trust-injection moment (auditable by grepping `MkTrustedFixture`). + Projections `trustedToVerifier` / `trustedToSpec` / + `trustedToSource` carry the witness into each acceptance predicate + without further trust at use site. `record ExtendedAgreement` + bundles `StructuralAgreement` with a fixture-lookup, and + `emptyExtendedAgreement` is the concrete inhabitant with an empty + registry. `verifierImpliesSpecExtended` / + `sourceImpliesSpecExtended` are total `Maybe`-returning bridges: + structural witnesses pass through; differential witnesses consult + the fixture registry. Net effect: the multi-week + `VerifierSpecAgreement` / `SourceVerifierAgreement` residual now + has a concrete shape (fixture-registry population) rather than + a "multi-week TODO". + +**~30 new named items added** including `FunctionsAccepted`, +`VAStructural` / `VADifferential`, `SAStructural` / `SADifferential`, +six structural-agreement directions + `StructuralAgreement` record + +concrete `structuralAgreement` value, four empty-module inhabitants, +six alloc/free + borrow inhabitants, four discrimination proofs + +their bad modules, `TrustedFixture` record + three projections, +`ExtendedAgreement` record + concrete empty inhabitant + two +extended-bridge functions. Regression: build green 22/22 modules +under Idris2 0.8.0. Zero new `believe_me`, `assert_total`, +`postulate`, `sorry`, `assert_smaller`. `%default total` preserved. + +**Open after A14** — full proof bodies for `VerifierSpecAgreement` / +`SourceVerifierAgreement` (now down to: populate +`emptyExtendedAgreement`'s fixture registry from the actual +differential harness, then close the unconditional direction). +Other long-tail items (`LevelAttestation` reindexed-by-witness +redesign; WasmCert-Isabelle tie-back; emitted-wasm byte-equality) +unchanged. + +### Proof-debt pass A15 (2026-05-26, same-day continuation; PR #74) + +A14 landed `fixtureCleanLinearConsumerTrusted` — the first concrete +`TrustedFixture` (cross_compat.rs row 1). A15 extends fixture +coverage to **two more** cross_compat rows: + +* **Row 9** (`fixtureExtractExportsModule`) — three-function shape + exercising the multi-function structural path. +* **Row 10** (`fixtureRealisticCleanModule`) — four-function shape + exercising borrow + nullary intent variety. + +Each row lands as a six-tuple: module + structural witness + +`TrustedFixture` + spec/verifier/source acceptance projections. +Coverage of cross_compat rows 2–8 is documented as out-of-scope for +the summary-level spec (body-level rejections + cross-module +modelling). + +### Proof-debt pass A16 (2026-05-26, same-day continuation; PR #74) + +A15 left three independent registered fixtures behind +`emptyExtendedAgreement`'s `\_,_,_ => Nothing` lookup. A16 builds +the **first non-empty** `ExtendedAgreement` (`firstExtendedAgreement`) +with a dispatching lookup that returns the matching `TrustedFixture` +when called on a registered module: + +* Manual `DecEq` instances for `OwnershipIntent` (16 cases), + `FunctionSummary`, and `ModuleSummary` (no elaborator reflection + in Idris2 0.8.0 — derived manually). +* `liftTrustedFixture : a = b -> TrustedFixture a -> TrustedFixture b` + transport across propositional equality. +* `fixtureLookupDispatching` — total, three-way decEq chain over the + three registered fixtures. + +### Proof-debt pass A17 (2026-05-26, same-day continuation; PR #74) + +A16's dispatching ExtendedAgreement is the open-world record-shaped +path. A17 adds a complementary **closed-world evidence track** that +provides `Maybe`-free constructive bridges: + +* `data RegisteredFixture : ModuleSummary -> Type` — closed-world + GADT with one type-indexed constructor per registered fixture. + Callers cannot manufacture evidence for unregistered modules. +* `fixtureFromEvidence : RegisteredFixture m -> TrustedFixture m` — + pattern-match dispatcher (definitional reduction). +* Six projector round-trip lemmas as `Refl`: `name{Row1,Row9,Row10}` + and `id{Row1,Row9,Row10}`. Projectors force unfolding past the + toplevel `fixtureXTrusted` name so unification proceeds at + symmetric reduction depths. (Round-trip-to-toplevel-name lemmas + do not type-check as `Refl` in Idris2 0.8.0 — asymmetric reducer + behavior; documented inline.) +* `verifierImpliesSpecEvidence : RegisteredFixture m -> VerifierAccepts m + -> SpecAccepts m` — `Maybe`-free constructive bridge. + Registration *is* the acceptance witness; no fixture-lookup + failure mode. +* `sourceImpliesSpecEvidence` — symmetric `SourceAccepts m -> + SpecAccepts m` bridge. + +**Open after A17** — full proof bodies for `VerifierSpecAgreement` / +`SourceVerifierAgreement` (unchanged dependency: populate the +registered-fixture set from the actual differential harness, then +close the unconditional direction). Cross_compat rows 2–8 require +extending `FunctionSummary` with a body-level trace; cross-module +rows require lifting `ModuleSummary` to a module graph. Both are +long-tail. + +Regression: 118 Layer-1 assertions pass (was 50 at A12, 68 at A13, +~92 at A14, ~105 at A16). Build green 22/22 modules. Zero new +`believe_me`, `assert_total`, `postulate`, `sorry`, +`assert_smaller`. `%default total` preserved. + +### Proof-debt pass A13 (2026-05-26, same-day continuation) + +Per coordinator pre-clearance for items 5 + 7 + 8, this round closes +the last of the post-A10 audit items at the **statement level** +(same PR [#72](https://github.com/hyperpolymath/typed-wasm/pull/72)). +No items remain from that audit; items 7 + 8 are stated as typed +obligations (full proofs are multi-week and out of one-session +scope). + +- **Item 5a closed** (L13 × L10 cross-level). + `ModuleIsolation.idr` imports `Linear` and gains + `LinearAcrossBoundary from to regName bs token` (an L13 + `AccessWitness` paired with an L10 `LinHandle`) plus three + theorems: `linearTransferRequiresBoundary` (no-bypass — any + non-local handle move requires a concrete boundary in `bs`), + `linearTransferLocal` (local-case constructor), and projections + `acrossWitness` / `acrossHandle`. +- **Item 5b closed** (L14 × L13 cross-level). + `SessionProtocol.idr` imports `ModuleIsolation` and gains + `SessionAcrossBoundary` with `sessionAcrossPreservesState` (the + state index survives transfer), `sessionTransferRequiresBoundary` + (no-bypass), `sessionTransferLocal` (local-case), and projections. + Together they prove a session handle cannot silently change state + or escape its module without an L13 witness. +- **A12 leave-behind closed.** `Region.idr` gains `RegionsOverlap` + (an address inside both region footprints) and + `disjointImpliesNoOverlap`, the L7/L10-flavour cross-level lemma + that `RegionDisjoint` implies byte-level non-overlap. Closes the + link the A12 disjointness section header explicitly deferred. +- **Items 7 + 8 stated as obligations.** New module + `TypedWasm.ABI.VerifierSpec` introduces three predicates — + `SpecAccepts m` (Idris2 L7+L10 structural acceptance on + `ModuleSummary`), `VerifierAccepts m` (opaque; witnessed only by + the Rust differential harness via `differentialAccepted`), and + `SourceAccepts m` (opaque; witnessed by the source-side harness) + — plus two agreement records: `VerifierSpecAgreement` (item 7, + Rust verifier ↔ Idris2 spec) and `SourceVerifierAgreement` (item + 8, source-checker ↔ verifier coverage). Each record bundles + soundness + completeness so partial proofs can land one face at + a time. `sourceImpliesSpec` / `specImpliesSource` are the + composition lemmas under both agreements. The opaque acceptance + predicates make the trust boundary inspectable: every + `VerifierAccepts` / `SourceAccepts` use traces back to a named + fixture id. + +**15 new named items added** (`LinearAcrossBoundary`, +`linearTransferRequiresBoundary`, `linearTransferLocal`, +`SessionAcrossBoundary`, `sessionAcrossPreservesState`, +`sessionTransferRequiresBoundary`, `sessionTransferLocal`, +`RegionsOverlap`, `disjointImpliesNoOverlap`, `regionsOverlapSym`, +`SpecAccepts`, `VerifierAccepts`, `SourceAccepts`, +`IntentsLinearAcceptable`, `VerifierSpecAgreement` / +`SourceVerifierAgreement` / `sourceImpliesSpec` / +`specImpliesSource`). Regression: **68/68** under Idris2 0.8.0 +(both layers: source grep + `idris2 --build`). Package now 22 +modules (was 21 — `VerifierSpec` is the only addition). + +**Closed after A13** (post-A10 audit complete): items 5a, 5b, 6 +leave-behind, 7-statement, 8-statement. Long-tail: full proofs of +the two agreement records; `LevelAttestation` reindexed-by-witness +redesign (standards#130 / epic standards#124); WasmCert-Isabelle +tie-back; emitted-wasm byte-equality. + +### Proof-debt pass A12 (2026-05-26, same-day continuation) + +Per coordinator clearance, three more untracked items from the post-A10 +audit are closed in the same PR ([#72](https://github.com/hyperpolymath/typed-wasm/pull/72)): + +- **Item 4 closed IN FULL.** A11's partial `composeAssocLists` + (list-side only) is superseded by `composeAssoc`, which proves + three-way associativity of `composeCertificates` across all three + fields. Enabled by switching `composeCertificates` from + `Prelude.min` to `Data.Nat.minimum` (structural Nat), making + `minimumAssociative` apply directly. `composeHighProvenComm` adds + Nat-side commutativity via `minimumCommutative`. The old + `composeAssocLists` kept as a back-compat corollary. +- **Item 6 closed.** `Region.idr` gains `RegionDisjoint r1 r2` (two + constructors for byte-footprint non-overlap, both orderings) plus + `regionDisjointSym` proving symmetry. Cross-level theorem linking + disjointness to L7 + L10 deferred to a future pass — the predicate + itself was the missing primitive. +- **Item 3 closed.** `ResourceCapabilities.idr` gains `containedConcat` + (proving `ContainedIn` distributes over `++`) plus + `jointBudgetCompose`, the L8 ↔ L15 joint composition theorem. + Composing two functions with individual `EffectSubsumes` and + `FunctionCaps` witnesses yields a single function whose combined + effects subsume combined actuals (via L8 `subsumeCompose`) AND + whose combined required caps are contained in the owner module's + declared caps (via the new `containedConcat` + the existing + `l15bSoundness`). + +**6 new theorems added** (`composeAssoc`, `composeHighProvenComm`, +`RegionDisjoint`, `regionDisjointSym`, `containedConcat`, +`jointBudgetCompose`). Regression: **50/50** under Idris2 0.8.0 +(both layers: source grep + `idris2 --build`). + +Open after A12 (→ A13): post-A10 audit items 5 (L13×L10, L14×L13 +cross-level), 7 (Rust verifier ↔ Idris2 spec equivalence), 8 +(source-checker ↔ verifier coverage agreement). + +### Proof-debt pass A10 + A11 (2026-05-26) + +Two same-day rounds attacking proof debt against `PROOF-NEEDS.md`. PR +[#72](https://github.com/hyperpolymath/typed-wasm/pull/72). + +**A10 (named, deferred)** — closes the last two items the 2026-05-18 +reconciliation banner still called "deferred": + +- **L12 freshness propagation under concurrent writes** (Epistemic.idr). + 8 new theorems headlined by `freshnessPropagatesUnderWrites : + Fresh mod field v v -> LT v cur -> Sync mod field v cur -> + Fresh mod field cur cur`. Supporting: `concurrentWriteStales`, + `resyncRecoversFresh`, `freshNotStale`, `freshImpliesEqual`, + `staleImpliesLT`, `syncChainEndsFresh`, and the + `epistemicFreshness : (p : Level12Proof) -> Fresh …` projector that + closes PROOF-NEEDS §P1.2 directly. +- **`compatCommute` mutual-subschema case** (MultiModule.idr). + `compatCommute : ModuleCompat from to imp exp -> SchemaSub exp imp -> + ModuleCompat to from exp imp` + `noSpoofingBidir` corollary. + Second worked example (`serviceA`/`serviceB` with permuted schemas) + exercises the theorem on a non-trivial input. +- **`tests/proof/regression.mjs` Layer 2 fixed** from a silent no-op + (`--check typed-wasm.ipkg` tried to parse the ipkg as `.idr`) to an + actual `idris2 --build`. + +**A11 (untracked, audit-driven)** — closes 3 of 8 untracked gaps the +A10 post-mortem surfaced (full inventory: +`project_typed_wasm_proof_debt_post_a10.md`): + +- **Item 1** — `Sync.WriteSync` no longer admits fake writers. The + constructor now requires a `FieldVersion` witness with three + projection equalities (`fv.field = field`, `fv.version = newVersion`, + `fv.lastWriter = mod`). Adversarial constructions like + `WriteSync (MkFieldVersion otherField …) Refl Refl Refl` are now + ill-typed unless the witness coincides with the indexed + field/version/writer. Corollary `writeSyncIdentifiesWriter` + extracts the witness. +- **Item 2** — `Knowledge.Observed` is grounded in a `Sync` event. + Constructor now takes `(sync : Sync mod field oldVer ver)`, so + `Observed mod field ver` cannot be inhabited without a + causally-prior write. Corollary `observedHasProvenance` reads the + prior version + Sync witness back out. +- **Item 4 (partial)** — first algebraic laws for + `composeCertificates`. `achievedAppendSplit` proves + `LevelAchievedIn n (xs ++ ys) -> Either (LevelAchievedIn n xs) + (LevelAchievedIn n ys)`; `composeAssocLists` proves list-level + associativity of three-way composition; `composeAchievedSym` is the + symmetric counterpart of `composeAchievedL`/`R`. The `Nat`-min + commutativity on `highestProven` is **deferred to A12**: + `Prelude.min Nat = if x < y then x else y` is non-structural and + does not reduce to `Refl` on symbolic inputs. + +**Test surface:** 13 named theorems added (8 in A10, 5 in A11), all +guarded by both `tests/proof/regression.mjs` layers (Layer 1 source +grep + Layer 2 `idris2 --build`). Total: **44/44 passing** under +Idris2 0.8.0. + +**Open after A11** (→ A12): post-A10-audit items 3 (L8↔L15 joint +budget), 5 (L13×L10, L14×L13 cross-level), 6 (region disjointness in +linear memory), 7 (Rust verifier ↔ Idris2 spec equivalence), 8 +(source-checker ↔ verifier coverage agreement), plus the Nat-min half +of item 4. + ### Phase 0 closure pass (2026-05-24 / 2026-05-25) Two sessions of focused engineering-surface stabilisation, closing the diff --git a/LEVEL-STATUS.md b/LEVEL-STATUS.md index 10c5f5c..6ac9f99 100644 --- a/LEVEL-STATUS.md +++ b/LEVEL-STATUS.md @@ -54,7 +54,7 @@ between 2026-04-13 (AST landed) and 2026-04-18 (verification).** | 9 | Lifetime safety | Lifetime.idr | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased. Preorder + load-safety theorems added A4 (2026-04-18): `outlivesRefl`, `outlivesTrans` (alias of pre-existing `outlivesTransitive` with 7-constructor case analysis), `loadSafe` proof-term, behavioural lemmas `loadSafeOffset` and `loadSafeIrrelevant` (proof irrelevance at the value level).** | | 10 | Linearity | Linear.idr (QTT q=1) | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased. Propositional state-machine theorems added A3 (2026-04-18): distinctUsage, consumePreservesData, noReuse, noReuseEcho — usage-indexed handle `LinHandleU Fresh/Consumed tok` with `consume` state transition, alongside the QTT structural layer.** | | 11 | Tropical cost-tracking | Tropical.idr | Not yet | None | **In package (A1, 2026-04-18). Commutative-semiring closure PROVEN (A2, 2026-04-18): all 12 axioms — tropAddLeftId/RightId/Comm/Assoc, tropMulLeftId/RightId/Comm/Assoc, tropMulLeftAnn/RightAnn, tropMulDistrib/DistribR. Uses structural `tropMin` (007-lang template). Zero dangerous patterns.** | -| 12 | Epistemic safety | Epistemic.idr | Not yet | None | **In package (A1, 2026-04-18); `writerKnowsFresh`, `freshOrStale`, `syncRestoresFresh` theorems live. Full freshness propagation under concurrent writes deferred.** | +| 12 | Epistemic safety | Epistemic.idr | Not yet | None | **In package (A1, 2026-04-18); A10 (2026-05-26) closes the previously-deferred "freshness propagation under concurrent writes" gap with the flagship `freshnessPropagatesUnderWrites` plus the supporting `concurrentWriteStales`, `resyncRecoversFresh`, `freshNotStale`, `freshImpliesEqual`, `staleImpliesLT`, `syncChainEndsFresh`, and the `epistemicFreshness` projector (closes PROOF-NEEDS §P1.2 "Level12Proof implies freshness"). 11 named theorems total.** | | 13 | Module isolation | ModuleIsolation.idr | (per-module handles, future) | 12 parser/Checker tests | **v1.2 — Idris2 proof + surface checker live; 007 lowering DONE (task #5)** | | 14 | Session protocols | SessionProtocol.idr | (typed-state handles, future) | 13 parser/Checker tests | **v1.3 — Idris2 proof + surface checker live; 007 send/receive lowering DONE (task #7)** | | 15 | Resource capabilities | ResourceCapabilities.idr | (future) | 13 parser/Checker tests | **v1.4 — Idris2 proof + surface checker (L15-A + L15-B) live; L15-C call-graph check deferred to v1.4.x; 007 lowering DONE (task #9)** | @@ -89,22 +89,23 @@ toolchain remains future work. | File | believe_me | postulate | assert_total | Checked status | |------|-----------|-----------|--------------|----------------| -| Region.idr | 0 | 0 | 0 | In package. Structural injectivity added A8 (2026-04-18): `fieldNameInj` / `fieldTypeInj` / `fieldInj` (MkField constructor injectivity), `schemaEqSym` / `schemaEqTrans` (making SchemaEq a full equivalence relation with the pre-existing `schemaEqRefl`), `lookupFieldName` (L2 soundness — `FieldIn name schema` implies `fieldName (lookupField prf) = name`). | +| Region.idr | 0 | 0 | 0 | In package. Structural injectivity added A8 (2026-04-18): `fieldNameInj` / `fieldTypeInj` / `fieldInj` (MkField constructor injectivity), `schemaEqSym` / `schemaEqTrans` (making SchemaEq a full equivalence relation with the pre-existing `schemaEqRefl`), `lookupFieldName` (L2 soundness — `FieldIn name schema` implies `fieldName (lookupField prf) = name`). A12 (2026-05-26): byte-disjointness layer added — `RegionDisjoint r1 r2` (two constructors covering both orderings of footprint endpoints) plus `regionDisjointSym` proving symmetry. Closes post-A10 audit item 6. A13 (2026-05-26): byte-separation cross-level layer added — `RegionsOverlap r1 r2` (an address inside both region footprints), `disjointImpliesNoOverlap` proving `RegionDisjoint r1 r2 -> Not (RegionsOverlap r1 r2)`, plus `regionsOverlapSym`. Closes the L7/L10 cross-level link explicitly deferred at A12. | | TypedAccess.idr | 0 | 0 | 0 | In package | | Levels.idr | 0 | 0 | 0 | In package | | Pointer.idr | 0 | 0 | 0 | In package | | Effects.idr | 0 | 0 | 0 | In package | | Lifetime.idr | 0 | 0 | 0 | In package | | Linear.idr | 0 | 0 | 0 | In package | -| MultiModule.idr | 0 | 0 | 0 | In package. Flagship no-spoofing theorem proven A6 (2026-04-18): `FieldMatches`, `SchemaSub` preorder (`schemaSubRefl`, `schemaSubTrans`), `ModuleCompat` indexed on modules + schemas (`compatRefl`, `compatTrans`), and the flagship `noSpoofing : ModuleCompat from to imp exp -> FieldMatches f imp -> FieldMatches f exp`. Worked Rust-exports / AffineScript-imports example (4-field export, 2-field import subset) constructs a live certificate and applies the theorem. | -| ModuleIsolation.idr | 0 | 0 | 0 | In package (v1.2 / L13) | -| SessionProtocol.idr | 0 | 0 | 0 | In package (v1.3 / L14) | -| ResourceCapabilities.idr | 0 | 0 | 0 | In package (v1.4 / L15) | +| MultiModule.idr | 0 | 0 | 0 | In package. Flagship no-spoofing theorem proven A6 (2026-04-18): `FieldMatches`, `SchemaSub` preorder (`schemaSubRefl`, `schemaSubTrans`), `ModuleCompat` indexed on modules + schemas (`compatRefl`, `compatTrans`), and the flagship `noSpoofing : ModuleCompat from to imp exp -> FieldMatches f imp -> FieldMatches f exp`. Worked Rust-exports / AffineScript-imports example (4-field export, 2-field import subset) constructs a live certificate and applies the theorem. A10 (2026-05-26) closes the deferred `compatCommute` item: mutual-subschema commutativity `compatCommute : ModuleCompat from to imp exp -> SchemaSub exp imp -> ModuleCompat to from exp imp`, plus the `noSpoofingBidir` corollary returning a pair of field-transport functions. Second worked example (`serviceA`/`serviceB` with permuted schemas) demonstrates `compatCommute` on a case where both `SchemaSub` directions hold. | +| ModuleIsolation.idr | 0 | 0 | 0 | In package (v1.2 / L13). A13 (2026-05-26): L13×L10 cross-level layer added — imports `Linear`, exposes `LinearAcrossBoundary from to regName bs token` (an L13 `AccessWitness` paired with an L10 `LinHandle`) plus accessors `acrossWitness` / `acrossHandle`, the no-bypass theorem `linearTransferRequiresBoundary` (any non-local linear-handle transfer requires a concrete boundary in `bs`, proved by reusing `crossAccessImpliesBoundary`), and `linearTransferLocal` (local-case constructor). Closes post-A10 audit item 5a. | +| SessionProtocol.idr | 0 | 0 | 0 | In package (v1.3 / L14). A13 (2026-05-26): L14×L13 cross-level layer added — imports `ModuleIsolation`, exposes `SessionAcrossBoundary from to proto state regName bs` plus accessors, `sessionAcrossPreservesState` (the state index survives the transfer), `sessionTransferRequiresBoundary` (no-bypass, same shape as the L10 version one level up), and `sessionTransferLocal`. Closes post-A10 audit item 5b. | +| ResourceCapabilities.idr | 0 | 0 | 0 | In package (v1.4 / L15). A12 (2026-05-26): `containedConcat` proves `ContainedIn` distributes over `++`; `jointBudgetCompose` proves the L8 ↔ L15 **joint** budget composition theorem — given individual `EffectSubsumes` witnesses and individual `FunctionCaps` witnesses for two functions sharing an owner module, the compound function still satisfies both the combined L8 envelope (via `subsumeCompose`) AND the combined L15 module envelope (via `containedConcat` + `l15bSoundness`). Closes post-A10 audit item 3. | | Choreography.idr | 0 | 0 | 0 | In package (v1.5 / L16) | -| Proofs.idr | 0 | 0 | 0 | In package. Attestation API hardened A7 (2026-04-18): every L1-L10 attestation now requires a witness from its level module (Schema / FieldIn / WasmTypeCompat / Ptr-NonNull / InBounds / AccessResult / ExclusiveWitness / EffectSubsumes / Lifetime.Outlives / CompletedProtocol). `simpleReadCert` / `fullCert12` / `fullCert15` thread witnesses per level; the certificate cannot be constructed without real proof artefacts. Level-achievement layer added A8 (2026-04-18): `LevelAchievedIn` predicate, `achievedAppendL` / `achievedAppendR` list-append preservation, `LevelAchieved n cert` lifted to certificates, `composeAchievedL` / `composeAchievedR` proving any level achieved in either component of `composeCertificates` is still achieved in the composition. | +| Proofs.idr | 0 | 0 | 0 | In package. Attestation API hardened A7 (2026-04-18): every L1-L10 attestation now requires a witness from its level module (Schema / FieldIn / WasmTypeCompat / Ptr-NonNull / InBounds / AccessResult / ExclusiveWitness / EffectSubsumes / Lifetime.Outlives / CompletedProtocol). `simpleReadCert` / `fullCert12` / `fullCert15` thread witnesses per level; the certificate cannot be constructed without real proof artefacts. Level-achievement layer added A8 (2026-04-18): `LevelAchievedIn` predicate, `achievedAppendL` / `achievedAppendR` list-append preservation, `LevelAchieved n cert` lifted to certificates, `composeAchievedL` / `composeAchievedR` proving any level achieved in either component of `composeCertificates` is still achieved in the composition. A11 (2026-05-26): partial laws for `composeCertificates` itself — `achievedAppendSplit` decomposes a `LevelAchievedIn n (xs ++ ys)` into one side; `composeAssocLists` proves the list-level associativity of three-way composition; `composeAchievedSym` is the symmetric counterpart of `composeAchievedL`/`R`, recovering the achieved-side from a composed certificate. A12 (2026-05-26): switched `composeCertificates` from Ord-derived `Prelude.min` to structural `Data.Nat.minimum` so structural lemmas apply; **full** `composeAssoc` proves three-way associativity across list parts, multi-module parts, AND `highestProven` Nat side (via `minimumAssociative`); `composeHighProvenComm` proves Nat-side commutativity (via `minimumCommutative`). Closes post-A10 audit item 4 in full. | | Tropical.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) | -| Epistemic.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) | +| Epistemic.idr | 0 | 0 | 0 | In package (A1, 2026-04-18). A10 (2026-05-26): propagation theorems added — `freshImpliesEqual`, `staleImpliesLT`, `freshNotStale` (mutual exclusion via local `ltIrreflexive`), `concurrentWriteStales`, `resyncRecoversFresh`, the flagship `freshnessPropagatesUnderWrites`, `syncChainEndsFresh`, and the `epistemicFreshness` projector on `Level12Proof` (closes PROOF-NEEDS §P1.2). A11 (2026-05-26): constructor-tightening pass — `WriteSync` now demands a `FieldVersion` witness with three equality components (`field`/`version`/`lastWriter`), and `Knowledge.Observed` is grounded in a `Sync` event (no more unfounded versions). Corollaries: `writeSyncIdentifiesWriter` returns the `FieldVersion` (+ the three projections) for an explicit-or-implicit Sync; `observedHasProvenance` extracts the witnessing prior-version and `Sync` from any `Observed` value. | | Echo.idr | 0 | 0 | 0 | In package (A0, 2026-04-18) | +| VerifierSpec.idr | 0 | 0 | 0 | New module A13 (2026-05-26, [#72](https://github.com/hyperpolymath/typed-wasm/pull/72)) introduced the spec-of-record statement layer. A14 (2026-05-26, [#74](https://github.com/hyperpolymath/typed-wasm/pull/74)) reshapes the predicates and lands the first concrete agreement value. A15/A16/A17 (same PR #74, same day) extend fixture coverage + close the fixture-registry gap. Exposes the abstract `ModuleSummary` / `FunctionSummary` / `OwnershipIntent` shapes; the structural L10 single-consumption predicate `IntentsLinearAcceptable` and its `TokenFresh` underpinning; the shared `FunctionsAccepted` walk; the L7+L10 acceptance predicate `SpecAccepts m` (A14: wraps `FunctionsAccepted`); the inductive `VerifierAccepts m` / `SourceAccepts m` (A14: two constructors each — `VAStructural` / `SAStructural` for introspectable structural evidence, `VADifferential` / `SADifferential` for named-fixture trust-injection); the two agreement records `VerifierSpecAgreement` (item 7) / `SourceVerifierAgreement` (item 8) each bundling soundness + completeness directions; composition lemmas `sourceImpliesSpec` / `specImpliesSource`. A14 additions: structural-direction agreement lemmas (`functionsAcceptedImpliesSpec`, `specImpliesFunctionsAccepted`, `specImpliesVerifierStructural`, `specImpliesSourceStructural`, `verifierImpliesSpecStructural`, `sourceImpliesSpecStructural`); `record StructuralAgreement` + concrete `structuralAgreement` total value; concrete inhabitants (empty module variants, `allocFreeModule`, `allocFreeWithBorrowModule`); three discrimination proofs (`notSpecAcceptsBadDoubleConsume`, `notSpecAcceptsBadDoubleProduce`, `notSpecAcceptsBadConsumeProduceMix`) plus structural-verifier variant; `record TrustedFixture` + projections; `record ExtendedAgreement` + `emptyExtendedAgreement` + `verifierImpliesSpecExtended` / `sourceImpliesSpecExtended` total bridge functions. A15 additions: `fixtureCleanLinearConsumerTrusted` (row 1), `fixtureExtractExportsTrusted` (row 9, three-function shape), `fixtureRealisticCleanTrusted` (row 10, four-function shape) — each with module + witness + TrustedFixture + spec/verifier/source acceptance projections. A16 additions: manual `DecEq OwnershipIntent` (16 cases), `DecEq FunctionSummary`, `DecEq ModuleSummary`; `liftTrustedFixture : a = b -> TrustedFixture a -> TrustedFixture b` transport; `fixtureLookupDispatching` (three-fixture decEq chain); `firstExtendedAgreement` (first non-empty ExtendedAgreement). A17 additions: `data RegisteredFixture : ModuleSummary -> Type` (closed-world GADT, three type-indexed constructors); `fixtureFromEvidence` (pattern-match dispatcher); six `Refl` projector round-trips (`name{Row1,Row9,Row10}`, `id{Row1,Row9,Row10}`); `verifierImpliesSpecEvidence` / `sourceImpliesSpecEvidence` (Maybe-free constructive bridges). Structural sublattice of items 7+8 fully proven; differential case has a concrete three-fixture registry plus both Maybe-returning (A16) and Maybe-free (A17) dispatch paths. | ## Post-codegen verifier (Rust) diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index c0dfec9..c3985c8 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -20,7 +20,342 @@ compile time" (true) and "here is a lemma proving it is forbidden" claims — a reviewer asking _"where is the theorem?"_ currently has no answer to point at. -## RECONCILIATION 2026-05-18 (verified ground truth — read this first) +## RECONCILIATION 2026-05-26 (A15 / A16 / A17 follow-up — read this FIRST) + +> **A15 + A16 + A17 follow A14 in the same calendar day** (same +> [PR #74](https://github.com/hyperpolymath/typed-wasm/pull/74)). +> Where A14 stopped at a single concrete fixture (row 1 of +> `cross_compat.rs`) and an `emptyExtendedAgreement`, this chain +> closes the residual fixture-registry gap to the extent that the +> summary-level spec permits. +> +> 1. **A15 — fixture coverage.** Two more `TrustedFixture` values: +> `fixtureExtractExportsTrusted` (row 9, three functions) and +> `fixtureRealisticCleanTrusted` (row 10, four functions exercising +> borrow + nullary intents). Coverage of cross_compat rows 2–8 is +> documented as out-of-scope for the summary-level +> `FunctionSummary` shape (body-level rejections) or out-of-scope +> for the single-module `ModuleSummary` shape (cross-module +> coupling). +> +> 2. **A16 — first non-empty `ExtendedAgreement`.** Manual +> `DecEq` instances for `OwnershipIntent` (16 cases) + +> `FunctionSummary` + `ModuleSummary` (Idris2 0.8.0 has no +> elaborator-reflection auto-derive); `liftTrustedFixture` to +> transport across propositional equality; +> `fixtureLookupDispatching` decEq-chain over the three registered +> fixtures; `firstExtendedAgreement` wires it all up. Round-trip +> lemmas `fixtureLookupDispatching ... = Just ` are +> NOT `Refl` definitionally because `decEq` on records bottoms out +> in `decEq String` which doesn't unfold — limitation documented +> inline; the dispatcher itself is total and load-bearing. +> +> 3. **A17 — closed-world evidence track.** Sidesteps A16's +> decEq-asymmetric-reduction limitation: +> * `data RegisteredFixture : ModuleSummary -> Type` — closed-world +> GADT with one type-indexed constructor per registered fixture. +> Pattern matching reduces definitionally (no decEq). +> * `fixtureFromEvidence : RegisteredFixture m -> TrustedFixture m`. +> * Six projector round-trips as `Refl`: `name{Row1,Row9,Row10}` + +> `id{Row1,Row9,Row10}`. +> * `verifierImpliesSpecEvidence` / `sourceImpliesSpecEvidence` — +> **`Maybe`-free** constructive bridges. Registration is the +> acceptance witness. +> +> **Build green 22/22. 118 regression assertions pass** (was 105 at +> A16, ~92 at A14, 68 at A13). Zero new `believe_me`, +> `assert_total`, `postulate`, `sorry`, `assert_smaller`. +> `%default total` preserved. +> +> **Open after A17.** Same as Open-after-A14, *minus* the +> fixture-registry gap which now has a concrete inhabitant (the +> three-fixture registry behind `firstExtendedAgreement` / +> `fixtureFromEvidence`). Long-tail items unchanged: +> `LevelAttestation` reindexed-by-witness redesign, WasmCert-Isabelle +> tie-back, emitted-wasm byte-equality, parser round-trip in Idris2. +> Cross_compat rows 2–8 require either body-level `FunctionSummary` +> extension or cross-module `ModuleSummary` lifting — both multi-week. + +## RECONCILIATION 2026-05-26 (A14 follow-up) + +> **A14 follows A13 in the same calendar day** ([#74](https://github.com/hyperpolymath/typed-wasm/pull/74)). +> A13 stated items 7 + 8 as typed obligations but kept the +> `VerifierAccepts` / `SourceAccepts` predicates **opaque** (a single +> constructor carrying only an external-evidence string + fixture +> id), which made every agreement direction unprovable in Idris2. +> A14 reshapes those predicates and lands the **first concrete, +> total, no-`believe_me` agreement value in the codebase** between +> spec / verifier / source-checker. +> +> 1. **Design pass — `VerifierAccepts` / `SourceAccepts` no longer +> opaque.** Each refactored to two constructors: `VAStructural` / +> `SAStructural` taking a `FunctionsAccepted` witness (the same +> structural predicate the spec uses, fully introspectable) and +> `VADifferential` / `SADifferential` carrying external-evidence +> name + id (the trust-injection escape hatch, single audit +> point). `SpecAccepts` is refactored to wrap `FunctionsAccepted` +> too, so spec / verifier / source share one canonical structural +> witness shape at L7+L10. +> +> 2. **First concrete agreement value.** `structuralAgreement : +> StructuralAgreement` is total, no `believe_me`, no `postulate`, +> no external trust. It closes the structural sublattice of items +> 7 + 8 with six total agreement directions (`functionsAcceptedImpliesSpec`, +> `specImpliesFunctionsAccepted`, `specImpliesVerifierStructural`, +> `specImpliesSourceStructural`, `verifierImpliesSpecStructural`, +> `sourceImpliesSpecStructural` — the latter two return `Maybe` +> because the differential case has no structural information by +> design). +> +> 3. **Concrete inhabitants.** `emptyFunctionsAccepted` plus three +> empty-module variants (`emptyModuleSpecAccepts` / +> `…VerifierAccepts` / `…SourceAccepts`) prove the predicates are +> not vacuously empty. `allocFreeModule` plus spec / verifier / +> source witnesses build the first non-empty case. +> `allocFreeWithBorrowModule` extends to all four +> `OwnershipIntent` constructors with three witnesses each. +> +> 4. **Discrimination — predicate has teeth.** Three rejection +> proofs each exercise a distinct `TF*` / `ILA*` constructor +> combination: `notSpecAcceptsBadDoubleConsume` rules out +> `[Consumes 0, Consumes 0]`, `notSpecAcceptsBadDoubleProduce` +> rules out `[Produces 0, Produces 0]`, and +> `notSpecAcceptsBadConsumeProduceMix` rules out +> `[Consumes 0, Produces 0]`. All discharged by the `Refl` +> pattern against the `Not (0 = 0)` embedded in the relevant +> `TF*` constructor. Plus +> `notVerifierStructuralAcceptsBadDoubleConsume` for the +> structural verifier path. +> +> 5. **ExtendedAgreement — constructive bridge for `VADifferential`.** +> `record TrustedFixture m` pairs a fixture name + id with the +> structural witness it certifies; constructing one IS the +> trust-injection moment (auditable by grepping +> `MkTrustedFixture`). Projections `trustedToVerifier` / +> `trustedToSpec` / `trustedToSource` carry the witness into each +> acceptance predicate. `record ExtendedAgreement` bundles +> `StructuralAgreement` with a fixture-lookup, and +> `emptyExtendedAgreement` is its concrete inhabitant. +> `verifierImpliesSpecExtended` and `sourceImpliesSpecExtended` +> are total `Maybe`-returning bridges: structural witnesses pass +> through; differential witnesses consult the registry. Net +> effect — the multi-week `VerifierSpecAgreement` / +> `SourceVerifierAgreement` residual now has a concrete shape +> (populate the registry from the actual differential harness) +> rather than a "multi-week TODO". +> +> **~30 new named items** including `FunctionsAccepted`, four +> `OwnershipIntent`-flavoured demo modules + witnesses, three +> discrimination proofs + bad modules, `TrustedFixture`, +> `ExtendedAgreement`, `structuralAgreement`, +> `emptyExtendedAgreement`, and the agreement-direction +> total functions. Build green 22/22 modules under Idris2 0.8.0. +> Zero new `believe_me`, `assert_total`, `postulate`, `sorry`, +> `assert_smaller`. `%default total` preserved. +> +> **Open after A14.** Full proof bodies for +> `VerifierSpecAgreement` / `SourceVerifierAgreement` are now +> bounded: populate `emptyExtendedAgreement`'s fixture registry +> from the differential harness (one `MkTrustedFixture` per +> audited fixture row), then close the unconditional direction +> by case analysis. Other long-tail items +> (`LevelAttestation` reindexed-by-witness redesign, +> WasmCert-Isabelle tie-back, emitted-wasm byte-equality, parser +> round-trip in Idris2) unchanged. + +## RECONCILIATION 2026-05-26 (A13 follow-up) + +> **A13 follows A12 in the same calendar day.** Per coordinator +> pre-clearance for items 5 + 7 + 8 (and the small A12 leave-behind), +> this round closes **the remaining post-A10 audit items in their +> statement-level form**: +> +> 1. **Item 5a (L13 × L10) closed.** `ModuleIsolation.idr` gains +> `LinearAcrossBoundary from to regName bs token`, pairing an L13 +> `AccessWitness` with an L10 `LinHandle`. The no-bypass theorem +> `linearTransferRequiresBoundary` proves that any non-local +> linear-handle transfer requires a concrete boundary in `bs` — a +> linear handle cannot leave an isolated module without an L13 +> boundary declaration. `linearTransferLocal` is the local-case +> constructor. Proof shape reuses `crossAccessImpliesBoundary` +> from L13 directly; the cross-level claim is a clean lift. +> +> 2. **Item 5b (L14 × L13) closed.** `SessionProtocol.idr` now +> imports `ModuleIsolation` and gains `SessionAcrossBoundary` with +> three theorems: `sessionAcrossPreservesState` (the state index +> survives the transfer), `sessionTransferRequiresBoundary` (the +> same no-bypass shape as L10), and `sessionTransferLocal` +> (local-case). Together they prove a session handle cannot +> silently change state or escape its module without an L13 +> witness. +> +> 3. **A12 leave-behind closed.** `Region.idr` gains `RegionsOverlap` +> (an address lying inside both region footprints) and +> `disjointImpliesNoOverlap` proving `RegionDisjoint -> Not +> RegionsOverlap`. This is the L7/L10 cross-level link the A12 +> section header promised — disjointness now has byte-level +> teeth. `regionsOverlapSym` is the symmetry companion. +> +> 4. **Items 7 + 8 stated as obligations.** New module +> `VerifierSpec.idr` introduces `SpecAccepts m` (the Idris2 L7+L10 +> structural acceptance predicate on `ModuleSummary`), +> `VerifierAccepts m` (opaque; witnessed by the Rust differential +> harness via `differentialAccepted`), and `SourceAccepts m` +> (opaque; witnessed by the source-side harness). Two record +> obligations — `VerifierSpecAgreement` (item 7) and +> `SourceVerifierAgreement` (item 8) — bundle the soundness and +> completeness directions so partial proofs can land one face at +> a time. Composition lemmas `sourceImpliesSpec` and +> `specImpliesSource` give the test harness end-to-end targets. +> +> **What this does NOT do.** Items 7 and 8 are stated, not +> proven. The full equivalence proofs require either a full +> simulation between two implementations (multi-week) or +> extending the verifier's coverage to every level the source +> checker promises. A13 pins the obligations as typed Idris2 +> predicates so the long-tail work has a fixed target. +> +> **15 new named theorems / data types** (`LinearAcrossBoundary`, +> `acrossWitness`, `acrossHandle`, `linearTransferRequiresBoundary`, +> `linearTransferLocal`, `SessionAcrossBoundary`, +> `sessionAcrossPreservesState`, `sessionTransferRequiresBoundary`, +> `sessionTransferLocal`, `RegionsOverlap`, +> `disjointImpliesNoOverlap`, `regionsOverlapSym`, `SpecAccepts`, +> `VerifierAccepts`, `SourceAccepts` plus `VerifierSpecAgreement` / +> `SourceVerifierAgreement` / `sourceImpliesSpec` / +> `specImpliesSource`). Regression **68/68** under Idris2 0.8.0 +> (both layers). +> +> **Open after A13.** No items remain from the original post-A10 +> 8-item audit. Long-tail work that exceeds a one-session scope: +> the actual proof bodies for `VerifierSpecAgreement` / +> `SourceVerifierAgreement`; the `LevelAttestation` reindexed-by- +> witness redesign (standards#130 / epic standards#124); WasmCert- +> Isabelle tie-back; emitted-wasm byte-equality for erasure +> (P3.1(a), blocked on emitter); parser round-trip in Idris2 +> (ECHIDNA-only at present). + +## RECONCILIATION 2026-05-26 (A12 follow-up) + +> **A12 follows A11 in the same calendar day.** Per coordinator-routed +> A12 go-ahead, this round closes **3 more** of the 8 untracked gaps +> from `project_typed_wasm_proof_debt_post_a10.md`: +> +> 1. **Item 4 closed IN FULL.** The A11 partial (`composeAssocLists` +> was list-side only) is now superseded by `composeAssoc` proving +> three-way associativity of `composeCertificates` across all three +> fields (list parts, multi-module parts, AND the `highestProven` +> Nat). Made possible by switching `composeCertificates` from the +> Ord-derived `Prelude.min` to the structural `Data.Nat.minimum` +> (per coordinator hint), which makes `minimumAssociative` apply +> directly. `composeHighProvenComm` adds Nat-side commutativity +> via `minimumCommutative`. The original `composeAssocLists` is +> kept as a back-compat corollary. +> +> 2. **Item 6 closed.** `RegionDisjoint r1 r2` in `Region.idr` — +> a two-constructor data type witnessing that two regions' byte +> footprints `[baseAddr, baseAddr + totalSize)` don't overlap in +> either ordering. `regionDisjointSym` proves symmetry. The +> cross-level theorem linking disjointness to L7 aliasing-safety +> and L10 linearity is left for a future pass — disjointness as a +> predicate is the missing primitive the audit flagged. +> +> 3. **Item 3 closed.** `jointBudgetCompose` in +> `ResourceCapabilities.idr` proves L8 ↔ L15 joint composition: +> given individual `EffectSubsumes` witnesses + individual +> `FunctionCaps` witnesses for two functions sharing an owner +> module, the compound function satisfies both the combined L8 +> envelope (via `subsumeCompose`) AND the combined L15 module +> envelope (via the new `containedConcat` + the existing +> `l15bSoundness`). +> +> All five new theorems (`composeAssoc`, `composeHighProvenComm`, +> `RegionDisjoint`, `regionDisjointSym`, `jointBudgetCompose`, +> `containedConcat`) are guarded by `tests/proof/regression.mjs`. +> Regression now **50/50**. +> +> Items remaining from the original post-A10 audit (all explicitly +> A12 → A13 inheritance per coordinator clearance): item 5 (L13×L10, +> L14×L13 cross-level), item 7 (Rust verifier ↔ Idris2 spec +> equivalence), item 8 (source-checker ↔ verifier coverage agreement). + +## RECONCILIATION 2026-05-26 (A11 follow-up) + +> **A11 follows A10 in the same calendar day.** Where A10 closed the +> *named* deferred items, A11 attacks three of the **untracked** gaps +> uncovered by the post-A10 audit (`project_typed_wasm_proof_debt_post_a10.md`): +> +> 1. **`Sync.WriteSync` no longer admits fake writers.** The constructor +> now requires a `FieldVersion` witness with three equalities +> (`fv.field = field`, `fv.version = newVersion`, +> `fv.lastWriter = mod`) and the corollary +> `writeSyncIdentifiesWriter` extracts that witness. An adversarial +> construction `WriteSync (MkFieldVersion otherField otherVer +> differentModule) Refl Refl Refl` is now ill-typed unless the three +> coincide with the indexed field/version/writer — the very +> "provenance gap" Audit Item 1 flagged. +> +> 2. **`Knowledge.Observed` is grounded in a `Sync` event.** The +> constructor now takes `(sync : Sync mod field oldVer ver)` so +> `Observed mod field ver` cannot be inhabited without a +> causally-prior write. `observedHasProvenance` reads the witness +> back out. Audit Item 2 ("Knowledge.Observed admits unfounded +> versions") is closed. +> +> 3. **`composeCertificates` gets its first algebraic laws.** +> `achievedAppendSplit` proves `LevelAchievedIn n (xs ++ ys) -> +> Either (LevelAchievedIn n xs) (LevelAchievedIn n ys)`; +> `composeAssocLists` proves the achieved-set under three-way +> composition is associative; `composeAchievedSym` is the symmetric +> counterpart of `composeAchievedL`/`R`. Audit Item 4 +> ("composeCertificates laws unproven") is **partially** closed — +> list-level associativity is proven, but the `Nat`-min commutativity +> on `highestProven` is left for A12 because Idris2 0.8's `Prelude.min +> Nat` is a non-structural `if x < y then x else y` and does not +> reduce to `Refl` on symbolic inputs. See `composeAssocLists` +> docstring in `Proofs.idr` for the discharge plan. +> +> All five new theorems (`writeSyncIdentifiesWriter`, +> `observedHasProvenance`, `achievedAppendSplit`, `composeAssocLists`, +> `composeAchievedSym`) are guarded by `tests/proof/regression.mjs` +> Layer 1 grep + Layer 2 `--build`. Items 3, 5, 6, 7, 8 from the +> post-A10 audit remain open and inherit to a future A12. + +## RECONCILIATION 2026-05-26 (A10 closure — read this first) + +> **A10 closes the last two named "deferred" items** that survived the +> 2026-05-18 reconciliation below. Both are now mechanically proven and +> guarded by `tests/proof/regression.mjs` (Layer 1 grep + Layer 2 build, +> Layer 2 invocation fixed to `--build` from a no-op `--check`). +> +> 1. **L12 freshness propagation under concurrent writes** (PROOF-NEEDS +> §P1.2 and LEVEL-STATUS row 12) — closed by 8 new theorems in +> `Epistemic.idr` headlined by `freshnessPropagatesUnderWrites : +> Fresh mod field v v -> LT v cur -> Sync mod field v cur -> +> Fresh mod field cur cur` plus `concurrentWriteStales`, +> `resyncRecoversFresh`, `freshNotStale`, `freshImpliesEqual`, +> `staleImpliesLT`, `syncChainEndsFresh`, and the named +> `epistemicFreshness : (p : Level12Proof) -> Fresh p.reader p.field +> p.knownVersion p.currentVersion` projector that satisfies the +> P1.2 obligation directly. +> +> 2. **`compatCommute` mutual-subschema case** (PROOF-NEEDS §P0.5 +> paragraph 246) — closed in `MultiModule.idr` by `compatCommute : +> ModuleCompat from to imp exp -> SchemaSub exp imp -> +> ModuleCompat to from exp imp` plus the `noSpoofingBidir` +> corollary. A second worked example (`serviceA`/`serviceB` with +> permuted schemas, both `SchemaSub` directions inhabited) +> demonstrates the theorem on a non-trivial input. +> +> The only proof-side item still explicitly deferred is the **stronger +> `LevelAttestation` reindexed by witness** noted at the end of the +> 2026-05-18 reconciliation; everything LEVEL-STATUS or this file +> previously called "deferred" or "future work" at the proof level is +> now resolved. L15-C call-graph **surface-checker** enforcement +> remains future work (the proof-side `callCompose` was already in +> place; LEVEL-STATUS row 15 carries the marker). + +## RECONCILIATION 2026-05-18 (verified ground truth) > Routed from estate proof-debt epic **hyperpolymath/standards#124**, > sub-issue **#130**. The 2026-04-13 inventory below is **superseded** diff --git a/src/abi/TypedWasm/ABI/Epistemic.idr b/src/abi/TypedWasm/ABI/Epistemic.idr index 52149fe..791343e 100644 --- a/src/abi/TypedWasm/ABI/Epistemic.idr +++ b/src/abi/TypedWasm/ABI/Epistemic.idr @@ -25,21 +25,17 @@ import Data.Nat %default total -- ============================================================================ --- Knowledge State +-- Global Ground Truth + Epistemic Predicates -- ============================================================================ - -||| A module's knowledge about a specific field in shared memory. -||| Knowledge is parameterised by a monotonic version counter — each -||| write increments the version, and a reader's knowledge is current -||| only if its version matches the field's current version. -public export -data Knowledge : (module_ : ModuleId) -> (field : String) -> (version : Nat) -> Type where - ||| The module has observed this field at the given version. - Observed : Knowledge mod field ver - ||| The module has NOT observed this field (initial state or invalidated). - Unknown : Knowledge mod field 0 +-- +-- Declaration order (A11, 2026-05-26): FieldVersion → Stale → Fresh → +-- Sync → Knowledge → Knows. Knowledge.Observed now carries a Sync +-- witness for provenance, so Knowledge depends on Sync rather than +-- preceding it. ||| The actual version of a field in shared memory (global truth). +||| Carries the writer identity at the recorded version — used as the +||| ground-truth witness for `WriteSync` (A11). public export record FieldVersion where constructor MkFieldVersion @@ -47,17 +43,6 @@ record FieldVersion where version : Nat lastWriter : ModuleId --- ============================================================================ --- Epistemic Predicates --- ============================================================================ - -||| K_i(φ) — "module i knows that field f has version v". -||| This is the core epistemic modal operator. -public export -data Knows : (mod : ModuleId) -> (field : String) -> (version : Nat) -> Type where - ||| A module knows a field's version if it has observed it at that version. - MkKnows : Knowledge mod field ver -> (ver > 0 = True) -> Knows mod field ver - ||| Staleness: a module's knowledge is stale if the field has been ||| written since the module last observed it. public export @@ -79,6 +64,14 @@ data Fresh : (mod : ModuleId) -> (field : String) -> ||| A synchronisation event that updates a module's knowledge. ||| After synchronisation, the module knows the current version. +||| +||| **WriteSync soundness (A11, 2026-05-26).** `WriteSync` now +||| requires a real `FieldVersion` value pinning the writer identity +||| to global ground truth. The original constructor took only a +||| `(writer = mod)` self-referential proof — anyone could supply +||| `WriteSync mod Refl` for any `mod`, with no link to the actual +||| writer. The tightened form forces the caller to commit to a +||| FieldVersion record matching `(field, newVersion, mod)`. public export data Sync : (mod : ModuleId) -> (field : String) -> (oldVersion : Nat) -> (newVersion : Nat) -> Type where @@ -86,10 +79,50 @@ data Sync : (mod : ModuleId) -> (field : String) -> ExplicitSync : (fresh : Fresh mod field newVersion newVersion) -> Sync mod field oldVersion newVersion ||| Write sync: when a module writes a field, it automatically knows - ||| the new version (it just wrote it). - WriteSync : (writer : ModuleId) -> writer = mod -> + ||| the new version (it just wrote it). The `FieldVersion` witness + ||| pins the writer identity to the field's global `lastWriter`. + WriteSync : (fv : FieldVersion) -> + fv.field = field -> + fv.version = newVersion -> + fv.lastWriter = mod -> Sync mod field oldVersion newVersion +-- ============================================================================ +-- Knowledge State +-- ============================================================================ + +||| A module's knowledge about a specific field in shared memory. +||| Knowledge is parameterised by a monotonic version counter — each +||| write increments the version, and a reader's knowledge is current +||| only if its version matches the field's current version. +||| +||| **Observed provenance (A11, 2026-05-26).** `Observed` now carries +||| a `Sync` witness — knowledge at a given version must be traceable +||| to a sync event. The original nullary `Observed : Knowledge mod +||| field ver` let any caller assert observation at any version with +||| no preconditions; provenance is now required. +public export +data Knowledge : (module_ : ModuleId) -> (field : String) -> (version : Nat) -> Type where + ||| The module has observed this field at `ver` via a sync event + ||| originating from `oldVer`. The sync witness pins the + ||| provenance. `oldVer` is declared as an explicit implicit so + ||| pattern matches and extractions can recover the prior version. + Observed : {oldVer : Nat} -> + (sync : Sync mod field oldVer ver) -> Knowledge mod field ver + ||| The module has NOT observed this field (initial state or invalidated). + Unknown : Knowledge mod field 0 + +-- ============================================================================ +-- Epistemic Predicates +-- ============================================================================ + +||| K_i(φ) — "module i knows that field f has version v". +||| This is the core epistemic modal operator. +public export +data Knows : (mod : ModuleId) -> (field : String) -> (version : Nat) -> Type where + ||| A module knows a field's version if it has observed it at that version. + MkKnows : Knowledge mod field ver -> (ver > 0 = True) -> Knows mod field ver + -- ============================================================================ -- Level 12 Proof Obligation -- ============================================================================ @@ -140,4 +173,152 @@ freshOrStale (S k) (S c) = case freshOrStale k c of export syncRestoresFresh : Sync mod field old new -> Fresh mod field new new syncRestoresFresh (ExplicitSync fresh) = MkFresh Refl -syncRestoresFresh (WriteSync _ _) = MkFresh Refl +syncRestoresFresh (WriteSync _ _ _ _) = MkFresh Refl + +-- ============================================================================ +-- Concurrent-write propagation theorems (A10, 2026-05-26 — closes +-- PROOF-NEEDS §P1.2 "freshness propagation under concurrent writes deferred") +-- ============================================================================ + +||| Fresh witnesses the equality of the two version indices. Projector +||| out of `MkFresh` for callers that need to substitute versions in +||| downstream proofs about reads. +export +freshImpliesEqual : Fresh mod field known current -> known = current +freshImpliesEqual (MkFresh eq) = eq + +||| Stale witnesses a strict ordering on versions. Dual projector to +||| `freshImpliesEqual`. +export +staleImpliesLT : Stale mod field known current -> LT known current +staleImpliesLT (MkStale lt) = lt + +||| LT is irreflexive — `LT n n` is uninhabited. Local helper for +||| `freshNotStale`; recurses on the LTESucc constructor (the LTEZero +||| branch is impossible since `LTE 0 0` cannot match `LTE (S n) n`). +ltIrreflexive : LT n n -> Void +ltIrreflexive (LTESucc rest) = ltIrreflexive rest + +||| Fresh and Stale are mutually exclusive at the same indices: no +||| concurrent writer can produce a Stale witness against a module that +||| holds a Fresh witness at the *same* (known, current) pair. The +||| local non-interference property; the propagation theorem below +||| handles the case where `current` actually advances. +export +freshNotStale : Fresh mod field v v' -> Stale mod field v v' -> Void +freshNotStale (MkFresh Refl) (MkStale lt) = ltIrreflexive lt + +||| Concurrent-write staleness. If module `mod`'s view of `field` was +||| fresh at version `v` and the global current version subsequently +||| advances to `v'` (with `v < v'`), `mod`'s view is now stale at +||| `(v, v')`. Contrapositive of `syncRestoresFresh` — without a Sync +||| event, any other writer's increment moves `mod` to the Stale state. +export +concurrentWriteStales : + Fresh mod field v v -> LT v v' -> Stale mod field v v' +concurrentWriteStales (MkFresh Refl) lt = MkStale lt + +||| Re-synchronisation after a concurrent write restores freshness. If +||| `mod`'s view is stale at `(v, cur)` and `mod` performs a Sync to +||| `cur`, the post-sync view is fresh at `(cur, cur)`. Composes +||| `concurrentWriteStales` (the stale arises) with `syncRestoresFresh` +||| (the sync neutralises the stale) into the full recovery protocol: +||| there is no "permanently stuck" state. +export +resyncRecoversFresh : + Stale mod field v cur -> Sync mod field v cur -> Fresh mod field cur cur +resyncRecoversFresh _ s = syncRestoresFresh s + +||| Flagship: freshness propagation under concurrent writes. Starting +||| from any fresh state at `v`, any number of intervening concurrent +||| writes (advancing the global current version to `cur`) can be +||| neutralised by a single re-Sync. The post-Sync state is fresh at +||| `(cur, cur)` regardless of how many writes occurred between the +||| original Fresh and the Sync. This is the named composition theorem +||| that closes PROOF-NEEDS §P1.2. +export +freshnessPropagatesUnderWrites : + Fresh mod field v v -> + LT v cur -> + Sync mod field v cur -> + Fresh mod field cur cur +freshnessPropagatesUnderWrites _ _ s = syncRestoresFresh s + +||| Chained syncs end fresh: any two-step sync sequence by `mod` on the +||| same field terminates in a fresh state at the final version. +||| Corollary of `syncRestoresFresh`; named explicitly because callers +||| composing multi-step read protocols want the chain-level statement +||| rather than re-deriving it at each call site. +export +syncChainEndsFresh : + Sync mod field v1 v2 -> Sync mod field v2 v3 -> Fresh mod field v3 v3 +syncChainEndsFresh _ s2 = syncRestoresFresh s2 + +||| Project the freshness witness out of a Level 12 certificate. +||| Closes the P1.2 "Level12Proof implies freshness" obligation: anyone +||| holding a `Level12Proof` value has, by construction, a `Fresh` +||| witness at the certificate's `(knownVersion, currentVersion)` +||| indices. Before this lemma the `.freshness` field was +||| record-projectable but lacked the named status the proof debt +||| called for. +export +epistemicFreshness : + (p : Level12Proof) -> + Fresh p.reader p.field p.knownVersion p.currentVersion +epistemicFreshness p = p.freshness + +-- ============================================================================ +-- Constructor soundness corollaries (A11, 2026-05-26 — closes the +-- WriteSync-admits-fake-writers + Observed-admits-unfounded-versions +-- soundness gaps surfaced during A10) +-- ============================================================================ + +||| A `WriteSync` carries the global ground-truth writer identity. +||| Given a write-sync event, the writer named in the dependent index +||| `mod` provably matches some `FieldVersion`'s `lastWriter`. This +||| extracts the `FieldVersion` and the equality witness — closing the +||| "anyone can construct a WriteSync claiming to be the writer" gap +||| by routing the writer identity through global state. +||| +||| Only constructible when the input is a `WriteSync`; `ExplicitSync` +||| does not carry writer provenance (an explicit sync is a read, not +||| a write — by design). Returns `Nothing` in that case. +public export +writeSyncIdentifiesWriter : + Sync mod field old new -> + Maybe (fv : FieldVersion ** (fv.field = field, fv.version = new, fv.lastWriter = mod)) +writeSyncIdentifiesWriter (ExplicitSync _) = Nothing +writeSyncIdentifiesWriter (WriteSync fv fp vp wp) = Just (fv ** (fp, vp, wp)) + +||| Observed knowledge has Sync provenance. Given a `Knowledge mod +||| field ver` value, if it was constructed via `Observed` then a +||| witnessing `Sync mod field oldVer ver` is in scope for some +||| existentially-bound `oldVer`. Returns `Nothing` for the +||| `Unknown` case (which only inhabits version 0 by design). +||| +||| Closes the "Observed admits unfounded version claims" gap: a +||| caller holding non-Unknown `Knowledge` at any `ver` necessarily +||| has a `Sync` event in scope to justify the claim — provenance +||| can no longer be conjured. +public export +observedHasProvenance : + Knowledge mod field ver -> + Maybe (oldVer : Nat ** Sync mod field oldVer ver) +observedHasProvenance Unknown = Nothing +observedHasProvenance (Observed {oldVer} sync) = Just (oldVer ** sync) + +-- ---------------------------------------------------------------------------- +-- Residual debt note (A11) +-- ---------------------------------------------------------------------------- +-- +-- The constructor-soundness tightening above plugs the most pointed +-- leaks but does not fully close the chain. `Fresh` and `ExplicitSync` +-- remain freely constructible: +-- - `MkFresh Refl : Fresh mod field v v` for any (mod, field, v) +-- - `ExplicitSync (writerKnowsFresh _ _ _) : Sync mod field _ v` +-- so a caller can still synthesise a `Sync` (and hence an `Observed`) +-- by chaining trivial constructions. Full tightening requires +-- re-indexing `Fresh` on a `FieldVersion` value so that the +-- `currentVersion` index is pinned to global ground truth — the next +-- residual-debt item, tracked in +-- `~/.claude/projects/-home-hyperpolymath/memory/project_typed_wasm_proof_debt_post_a10.md`. diff --git a/src/abi/TypedWasm/ABI/ModuleIsolation.idr b/src/abi/TypedWasm/ABI/ModuleIsolation.idr index b0ead89..061a2b3 100644 --- a/src/abi/TypedWasm/ABI/ModuleIsolation.idr +++ b/src/abi/TypedWasm/ABI/ModuleIsolation.idr @@ -36,6 +36,7 @@ import Data.List.Elem import TypedWasm.ABI.Region import TypedWasm.ABI.MultiModule +import TypedWasm.ABI.Linear %default total @@ -328,3 +329,101 @@ boundariesOf m = m.boundaries public export idOf : IsolatedModule -> IsolatedModuleId idOf m = m.modId + +-- ============================================================================ +-- A13 — Cross-Level: L13 (isolation) × L10 (linearity) +-- ============================================================================ +-- +-- Closes the post-A10 audit item 5a (L13 × L10 interaction): +-- when an L10 `LinHandle` "moves" from one isolated module to another, +-- the move is only legal if the L13 isolation discipline witnesses it +-- with a boundary. The cross-level claim has two faces: +-- +-- 1. **Existence**: pairing an `AccessWitness` with a `LinHandle` +-- produces a `LinearAcrossBoundary` token. This is the data type. +-- 2. **No-bypass**: any non-local `LinearAcrossBoundary` requires a +-- boundary on the source module's declared list. The proof is a +-- direct reuse of the L13-only `crossAccessImpliesBoundary` lifted +-- through the pairing — there is no way to construct a +-- LinearAcrossBoundary that bypasses the L13 boundary check. +-- +-- The interaction does NOT model dual-ownership transfer (sender loses +-- the handle, receiver gains it) — QTT's linearity quantity does that +-- structurally at the call site. This module only states the +-- propositional shape that downstream tooling can refer to. + +||| L13 × L10 cross-level witness: an L10 linear handle paired with the +||| L13 access witness that authorises its move from `from` to `to`. +||| +||| Constructing this type requires BOTH halves: a `LinHandle token` +||| (the L10 resource) and an `AccessWitness from to regName bs` +||| (the L13 right to reach `to`'s region). No constructor lets a +||| linear handle cross modules without an L13 witness. +public export +data LinearAcrossBoundary : (from, to : IsolatedModuleId) + -> (regName : String) + -> (bs : BoundaryList) + -> (token : Nat) + -> Type where + MkLinearAcrossBoundary : + (aw : AccessWitness from to regName bs) + -> (h : LinHandle token) + -> LinearAcrossBoundary from to regName bs token + +||| Project the L13 access witness from a cross-boundary linear handle. +public export +acrossWitness : {from, to : IsolatedModuleId} + -> {regName : String} + -> {bs : BoundaryList} + -> {token : Nat} + -> LinearAcrossBoundary from to regName bs token + -> AccessWitness from to regName bs +acrossWitness (MkLinearAcrossBoundary aw _) = aw + +||| Project the L10 linear handle from a cross-boundary linear handle. +public export +acrossHandle : {from, to : IsolatedModuleId} + -> {regName : String} + -> {bs : BoundaryList} + -> {token : Nat} + -> LinearAcrossBoundary from to regName bs token + -> LinHandle token +acrossHandle (MkLinearAcrossBoundary _ h) = h + +||| L13 × L10 soundness (no-bypass). +||| +||| Statement: if a linear handle has moved from `from` to `to` and +||| `from /= to`, then the boundary list `bs` of `from` MUST contain a +||| concrete boundary witnessing the transfer. Contrapositive: with no +||| boundary in `bs`, no `LinearAcrossBoundary` witness exists for a +||| non-local pair — the linear handle cannot leave `from`'s memory. +||| +||| Proof: directly reuse `crossAccessImpliesBoundary` on the embedded +||| access witness. The L13 mechanism does all the work; this lemma +||| just lifts it through the L10 pairing. +public export +linearTransferRequiresBoundary : + {from, to : IsolatedModuleId} + -> {regName : String} + -> {bs : BoundaryList} + -> {token : Nat} + -> (xfer : LinearAcrossBoundary from to regName bs token) + -> (notLocal : Not (from = to)) + -> (b : Boundary ** Elem b bs) +linearTransferRequiresBoundary xfer notLocal = + crossAccessImpliesBoundary (acrossWitness xfer) notLocal + +||| L13 × L10 soundness (local-case). +||| +||| Statement: if a linear handle moves WITHIN one isolated module +||| (`from = to = m`), the `LocalAccess` witness suffices and no +||| boundary is required. Used by the surface checker to short-circuit +||| boundary lookup on intra-module handle passes. +public export +linearTransferLocal : + (m : IsolatedModuleId) + -> (regName : String) + -> (bs : BoundaryList) + -> (h : LinHandle token) + -> LinearAcrossBoundary m m regName bs token +linearTransferLocal m _ _ h = MkLinearAcrossBoundary LocalAccess h diff --git a/src/abi/TypedWasm/ABI/MultiModule.idr b/src/abi/TypedWasm/ABI/MultiModule.idr index 4401b8c..f21118c 100644 --- a/src/abi/TypedWasm/ABI/MultiModule.idr +++ b/src/abi/TypedWasm/ABI/MultiModule.idr @@ -395,6 +395,52 @@ noTypeSpoofing : ModuleCompat from to imp expS -> FieldMatches (MkField name ty) expS noTypeSpoofing cert name ty fm = noSpoofing cert (MkField name ty) fm +-- ============================================================================ +-- Mutual-subschema commutativity (A10, 2026-05-26 — closes PROOF-NEEDS §P0.5 +-- "compatCommute" deferred item) +-- ============================================================================ + +||| Compat commutativity, mutual-subschema case. +||| +||| PROOF-NEEDS §P0.5 notes that `compatCommute` only holds when the +||| two subschema relations are mutually witnessed — at which point +||| the import and export schemas are equal up to reordering, and the +||| commutativity is a one-line corollary of `noSpoofing` in both +||| directions. This lemma states the mutual case explicitly. +||| +||| Given a forward compatibility certificate and an explicit +||| reverse-subschema witness, the reverse compatibility certificate +||| is constructible directly. Without the reverse witness the +||| theorem does *not* hold — a strict-subset import (Example's +||| `rescriptImportSchema ⊂ rustExportSchema` below) cannot commute, +||| because the export's `score` and `banned` fields are absent from +||| the import schema and no `SchemaSub rustExportSchema +||| rescriptImportSchema` can be constructed. +public export +compatCommute : ModuleCompat from to imp expS + -> SchemaSub expS imp + -> ModuleCompat to from expS imp +compatCommute (MkModuleCompat _) reverseSub = MkModuleCompat reverseSub + +||| Bidirectional no-spoofing. When two modules' schemas are mutually +||| subschemas, every field witness transports in both directions. +||| Returned as a pair of field-transport functions, one per direction. +||| +||| Composition of `noSpoofing` with `compatCommute` at the call site; +||| named explicitly so multi-direction call sites need not re-derive +||| the construction. +public export +noSpoofingBidir : ModuleCompat from to imp expS + -> SchemaSub expS imp + -> (f : Field) + -> ( FieldMatches f imp -> FieldMatches f expS + , FieldMatches f expS -> FieldMatches f imp + ) +noSpoofingBidir compat reverseSub f = + ( noSpoofing compat f + , noSpoofing (compatCommute compat reverseSub) f + ) + -- ============================================================================ -- Worked Example: Rust exports, ReScript imports (strict subset) -- ============================================================================ @@ -474,3 +520,66 @@ namespace Example Example.rustExportSchema exampleNoSpoofing = noSpoofing exampleCompat (MkField "id" U64) FMHere + + -- -------------------------------------------------------------------- + -- Permutation example: compatCommute applied (A10, 2026-05-26) + -- -------------------------------------------------------------------- + -- + -- The strict-subset example above CANNOT commute (rust's score/banned + -- are not in rescript's import). This second example uses a pair of + -- modules whose schemas differ only in field order — both directions + -- of SchemaSub hold, so compatCommute applies. + + ||| Service A exports `[id, age]` in that order. + public export + serviceASchema : Schema + serviceASchema = + [ MkField "id" U64 + , MkField "age" U8 + ] + + ||| Service B publishes the same two fields but in reverse order. + public export + serviceBSchema : Schema + serviceBSchema = + [ MkField "age" U8 + , MkField "id" U64 + ] + + public export + serviceA : ModuleId + serviceA = MkModuleId "service_a" + + public export + serviceB : ModuleId + serviceB = MkModuleId "service_b" + + ||| A→B: every field in A's schema appears in B's schema (in the + ||| swapped position). + public export + subAB : SchemaSub Example.serviceASchema Example.serviceBSchema + subAB = + SSCons (FMThere FMHere) -- "id" at position 1 in B + (SSCons FMHere SSNil) -- "age" at head in B + + ||| B→A: the reverse holds too — every field in B's schema appears + ||| in A's schema. The pair (subAB, subBA) witnesses mutual + ||| containment, so compatCommute applies. + public export + subBA : SchemaSub Example.serviceBSchema Example.serviceASchema + subBA = + SSCons (FMThere FMHere) -- "age" at position 1 in A + (SSCons FMHere SSNil) -- "id" at head in A + + ||| Forward compatibility certificate A→B. + public export + compatAB : ModuleCompat Example.serviceA Example.serviceB + Example.serviceASchema Example.serviceBSchema + compatAB = MkModuleCompat subAB + + ||| Reverse compatibility certificate, derived via `compatCommute` + ||| from `compatAB` plus the reverse subschema witness `subBA`. + public export + compatBA : ModuleCompat Example.serviceB Example.serviceA + Example.serviceBSchema Example.serviceASchema + compatBA = compatCommute Example.compatAB Example.subBA diff --git a/src/abi/TypedWasm/ABI/Proofs.idr b/src/abi/TypedWasm/ABI/Proofs.idr index a9fc026..d9cb4f1 100644 --- a/src/abi/TypedWasm/ABI/Proofs.idr +++ b/src/abi/TypedWasm/ABI/Proofs.idr @@ -17,6 +17,8 @@ module TypedWasm.ABI.Proofs +import Data.List +import Data.Nat import TypedWasm.ABI.Region import TypedWasm.ABI.TypedAccess import TypedWasm.ABI.Levels @@ -150,10 +152,17 @@ attestL15_CapsSafe _ = MkAttestation 15 Proven ||| The composed certificate takes the MINIMUM highest level: ||| if Module A is proven to Level 8 and Module B to Level 6, ||| the combined guarantee is Level 6 (the weakest link). +||| +||| Uses `Data.Nat.minimum` (the structural Nat version) rather than the +||| Ord-derived `Prelude.min` so that `minimumAssociative` / +||| `minimumCommutative` from `Data.Nat` apply directly — this is what +||| makes `composeAssoc` and `composeHighProvenComm` (A12, 2026-05-26) one +||| line each. The numeric behaviour is identical; only the proof +||| ergonomics change. public export composeCertificates : ProofCertificate -> ProofCertificate -> ProofCertificate composeCertificates (MkCertificate ls1 h1 mm1) (MkCertificate ls2 h2 mm2) = - MkCertificate (ls1 ++ ls2) (min h1 h2) (mm1 ++ mm2) + MkCertificate (ls1 ++ ls2) (minimum h1 h2) (mm1 ++ mm2) -- ============================================================================ -- Level-Specific Certificate Constructors (PROOF-NEEDS §P1.1 — A7) @@ -497,6 +506,22 @@ achievedAppendR : {0 n : Nat} achievedAppendR [] p = p achievedAppendR (_ :: xs) p = LAThere (achievedAppendR xs p) +||| Decomposition: a level achieved in `xs ++ ys` was achieved in +||| either `xs` or `ys`. Inverse of `achievedAppendL` / +||| `achievedAppendR`; needed for the `composeAchievedSym` +||| semantic-commutativity theorem (A11.3). +public export +achievedAppendSplit : {0 n : Nat} + -> (xs, ys : List LevelAttestation) + -> LevelAchievedIn n (xs ++ ys) + -> Either (LevelAchievedIn n xs) (LevelAchievedIn n ys) +achievedAppendSplit [] ys p = Right p +achievedAppendSplit (_ :: _) _ LAHere = Left LAHere +achievedAppendSplit (_ :: xs) ys (LAThere p) = + case achievedAppendSplit xs ys p of + Left inXs => Left (LAThere inXs) + Right inYs => Right inYs + ||| Predicate lifted to full proof certificates: "this certificate ||| claims level `n`". public export @@ -523,6 +548,90 @@ composeAchievedR : (c1, c2 : ProofCertificate) composeAchievedR (MkCertificate a1 _ _) (MkCertificate _ _ _) p = achievedAppendR a1 p +-- ============================================================================ +-- Composition algebra (A11.3, 2026-05-26 — closes the unstated +-- "composeCertificates algebraic laws" residual debt item) +-- ============================================================================ + +||| `composeCertificates` is **fully** associative — list parts, +||| multi-module parts, and the `highestProven` Nat side all align. +||| List components compose via `appendAssociative`; the Nat side +||| via `minimumAssociative` from `Data.Nat` (now applicable because +||| `composeCertificates` was switched from the Ord-generic +||| `Prelude.min` to the structural `Data.Nat.minimum` at A12). +||| +||| Supersedes the A11 list-only `composeAssocLists` (kept as a +||| corollary below for back-compat); closes post-A10 audit item 4 in +||| full. +public export +composeAssoc : + (a, b, c : ProofCertificate) -> + composeCertificates (composeCertificates a b) c + = composeCertificates a (composeCertificates b c) +composeAssoc (MkCertificate ls1 h1 mm1) + (MkCertificate ls2 h2 mm2) + (MkCertificate ls3 h3 mm3) = + rewrite appendAssociative ls1 ls2 ls3 in + rewrite appendAssociative mm1 mm2 mm3 in + rewrite minimumAssociative h1 h2 h3 in + Refl + +||| List-level associativity of `composeCertificates`. Original A11 +||| statement; now derived as a corollary of the full A12 `composeAssoc` +||| via projection on the first field of the equated certificates. +public export +composeAssocLists : + (a, b, c : ProofCertificate) -> + let MkCertificate as _ _ = composeCertificates (composeCertificates a b) c + MkCertificate bs _ _ = composeCertificates a (composeCertificates b c) + in as = bs +composeAssocLists (MkCertificate ls1 _ _) + (MkCertificate ls2 _ _) + (MkCertificate ls3 _ _) = + sym (appendAssociative ls1 ls2 ls3) + +||| The `highestProven` Nat component of `composeCertificates` is +||| **commutative**: the minimum doesn't care which side an operand +||| comes from. This is the Nat-side counterpart of +||| `composeAchievedSym`'s list-side achievement-swap. +||| +||| Closes the second half of post-A10 audit item 4 (algebraic laws +||| for `composeCertificates`). Coordinator hint (2026-05-26) +||| pointed at `minimumCommutative` from `Data.Nat` as the right +||| primitive — works because `composeCertificates` was switched to +||| `minimum` at A12. +public export +composeHighProvenComm : + (a, b : ProofCertificate) -> + let MkCertificate _ ha _ = composeCertificates a b + MkCertificate _ hb _ = composeCertificates b a + in ha = hb +composeHighProvenComm (MkCertificate _ h1 _) (MkCertificate _ h2 _) = + minimumCommutative h1 h2 + +||| Semantic commutativity of composition under `LevelAchieved`. +||| `composeCertificates` is NOT strictly commutative — the list +||| components are concatenated and concatenation is not commutative +||| on raw lists. But for the property that actually matters at the +||| certificate level — "level N is achieved" — the order is +||| irrelevant: a level achieved in `compose a b` is also achieved in +||| `compose b a`. +||| +||| Proved by splitting `achieved-in-append` into the two component +||| cases and re-introducing on the swapped form. Closes the +||| "composeCertificates algebra not stated" residual gap from the +||| post-A10 inventory. +public export +composeAchievedSym : + {n : Nat} -> + (a, b : ProofCertificate) -> + LevelAchieved n (composeCertificates a b) -> + LevelAchieved n (composeCertificates b a) +composeAchievedSym {n} (MkCertificate as _ _) (MkCertificate bs _ _) p = + case achievedAppendSplit as bs p of + Left inA => achievedAppendR bs inA + Right inB => achievedAppendL inB + -- ============================================================================ -- Proof Erasure Guarantee (PROOF-NEEDS §P3.1) -- ============================================================================ diff --git a/src/abi/TypedWasm/ABI/Region.idr b/src/abi/TypedWasm/ABI/Region.idr index 38a4084..036226e 100644 --- a/src/abi/TypedWasm/ABI/Region.idr +++ b/src/abi/TypedWasm/ABI/Region.idr @@ -409,3 +409,142 @@ lookupFieldName : {0 name : String} -> {schema : Schema} -> fieldName (lookupField prf) = name lookupFieldName {schema = _ :: _} (FieldHere {prf = p}) = p lookupFieldName {schema = _ :: _} (FieldThere later) = lookupFieldName later + +-- ============================================================================ +-- Region Disjointness (A12, 2026-05-26 — closes post-A10 audit item 6) +-- ============================================================================ +-- +-- Two regions are byte-disjoint when their footprints — `[baseAddr, +-- baseAddr + totalSize)` — don't overlap in WASM linear memory. +-- Disjointness is the foundation of any "no aliasing across regions" +-- argument: a borrow into r1 and a borrow into r2 commute iff r1 and +-- r2 are disjoint. +-- +-- The schemas need not differ; two regions of the *same* schema can be +-- disjoint (different addresses), and two regions of *different* +-- schemas can overlap (same address, viewed two ways). Schema identity +-- is orthogonal to memory disjointness. +-- +-- This file only states disjointness as a predicate plus its +-- meta-properties (symmetry, anti-reflexivity for non-empty regions). +-- The cross-level theorem linking disjointness to L7 aliasing-safety +-- and L10 linearity lives in a future A12 / A13 pass. + +||| Byte-disjointness of two region footprints. +||| +||| `RegionDisjoint r1 r2` witnesses that the linear-memory byte ranges +||| of `r1` and `r2` do not overlap. Two constructors capture the two +||| orderings: either r1 ends at or before r2 starts, or symmetrically. +public export +data RegionDisjoint : {0 s1, s2 : Schema} -> Region s1 -> Region s2 -> Type where + ||| `r1`'s footprint ends at or before `r2`'s starts. + DisjointBefore : {s1, s2 : Schema} + -> {r1 : Region s1} -> {r2 : Region s2} + -> LTE (baseAddr r1 + totalSize r1) (baseAddr r2) + -> RegionDisjoint r1 r2 + ||| `r2`'s footprint ends at or before `r1`'s starts. + DisjointAfter : {s1, s2 : Schema} + -> {r1 : Region s1} -> {r2 : Region s2} + -> LTE (baseAddr r2 + totalSize r2) (baseAddr r1) + -> RegionDisjoint r1 r2 + +||| Region disjointness is symmetric. If `r1` is disjoint from `r2` +||| then `r2` is disjoint from `r1` — the "before" case becomes the +||| "after" case and vice versa. +public export +regionDisjointSym : {s1, s2 : Schema} + -> {r1 : Region s1} -> {r2 : Region s2} + -> RegionDisjoint r1 r2 -> RegionDisjoint r2 r1 +regionDisjointSym (DisjointBefore p) = DisjointAfter p +regionDisjointSym (DisjointAfter p) = DisjointBefore p + +-- ============================================================================ +-- A13 — Region disjointness × byte separation (L7 / L10 cross-level) +-- ============================================================================ +-- +-- Closes the leave-behind from the A12 disjointness section: the +-- predicate-level theorem linking `RegionDisjoint` to actual byte-level +-- non-overlap. Two regions are byte-disjoint when no single address +-- `addr` lies in both their footprints `[baseAddr, baseAddr + totalSize)`. +-- +-- This is the L7 / L10 cross-level shape promised in the A12 header +-- comment: any aliasing argument (L7 ExclusiveWitness, L10 LinHandle +-- pair) over distinct regions can appeal to byte separation as the +-- underlying memory-safety reason. Stated here as a predicate-level +-- theorem so downstream proofs (Pointer.idr, Linear.idr) can re-export +-- the corollary they need without re-deriving the arithmetic. + +||| Local LTE transitivity helper for the disjointness chain. Idris2 +||| `Data.Nat` exports `transitive` (via the Transitive interface) and +||| historically `lteTransitive`; using a local primitive avoids name +||| churn across base-library revisions. +lteTrans : LTE a b -> LTE b c -> LTE a c +lteTrans LTEZero _ = LTEZero +lteTrans (LTESucc l1) (LTESucc l2) = LTESucc (lteTrans l1 l2) + +||| `LT n n` is uninhabited. Same shape as `Epistemic.ltIrreflexive`; +||| reintroduced locally to keep Region.idr's import surface minimal. +ltIrreflexiveRegion : LT n n -> Void +ltIrreflexiveRegion (LTESucc rest) = ltIrreflexiveRegion rest + +||| Byte overlap of two regions: an address `addr` that lies inside +||| both footprints `[baseAddr r, baseAddr r + totalSize r)`. +||| +||| Two-direction witnesses (lower-bound + strict upper-bound) for each +||| region make the predicate symmetric in `r1` / `r2` and easy to +||| consume in the disjointness theorem. +public export +data RegionsOverlap : {0 s1, s2 : Schema} + -> (r1 : Region s1) -> (r2 : Region s2) -> Type where + MkOverlap : {s1, s2 : Schema} + -> {r1 : Region s1} -> {r2 : Region s2} + -> (addr : Nat) + -> (loR1 : LTE (baseAddr r1) addr) + -> (hiR1 : LT addr (baseAddr r1 + totalSize r1)) + -> (loR2 : LTE (baseAddr r2) addr) + -> (hiR2 : LT addr (baseAddr r2 + totalSize r2)) + -> RegionsOverlap r1 r2 + +||| The cross-level theorem. If `r1` and `r2` are `RegionDisjoint`, +||| then no `addr` lies in both footprints — `RegionsOverlap` is +||| uninhabited. Proof: chain the disjointness witness with the +||| overlap's lower- and upper-bound witnesses to derive `LT addr addr`, +||| then dispatch to `ltIrreflexiveRegion`. +||| +||| Cross-level reading: +||| * **L7 (aliasing):** two `ExclusiveWitness`-holding pointers into +||| disjoint regions cannot byte-alias. The corollary lives in +||| Pointer.idr once the L7 surface needs the link. +||| * **L10 (linearity):** two `LinHandle` values whose offsets are +||| anchored to disjoint regions cannot reference the same byte; +||| the linearity discipline is therefore non-overlapping by +||| construction. Corollary lives in Linear.idr at the same call +||| site that needs it. +public export +disjointImpliesNoOverlap : {s1, s2 : Schema} + -> {r1 : Region s1} -> {r2 : Region s2} + -> RegionDisjoint r1 r2 + -> RegionsOverlap r1 r2 + -> Void +disjointImpliesNoOverlap (DisjointBefore sep) + (MkOverlap _ _ hiR1 loR2 _) = + -- hiR1 : LTE (S addr) (baseAddr r1 + totalSize r1) + -- sep : LTE (baseAddr r1 + totalSize r1) (baseAddr r2) + -- loR2 : LTE (baseAddr r2) addr + ltIrreflexiveRegion (lteTrans (lteTrans hiR1 sep) loR2) +disjointImpliesNoOverlap (DisjointAfter sep) + (MkOverlap _ loR1 _ _ hiR2) = + -- hiR2 : LTE (S addr) (baseAddr r2 + totalSize r2) + -- sep : LTE (baseAddr r2 + totalSize r2) (baseAddr r1) + -- loR1 : LTE (baseAddr r1) addr + ltIrreflexiveRegion (lteTrans (lteTrans hiR2 sep) loR1) + +||| Companion symmetry: overlap is symmetric in r1 / r2. Useful when +||| the downstream consumer holds an overlap witness in the opposite +||| orientation from the disjointness witness. +public export +regionsOverlapSym : {s1, s2 : Schema} + -> {r1 : Region s1} -> {r2 : Region s2} + -> RegionsOverlap r1 r2 -> RegionsOverlap r2 r1 +regionsOverlapSym (MkOverlap addr lo1 hi1 lo2 hi2) = + MkOverlap addr lo2 hi2 lo1 hi1 diff --git a/src/abi/TypedWasm/ABI/ResourceCapabilities.idr b/src/abi/TypedWasm/ABI/ResourceCapabilities.idr index d34cf55..919ecf3 100644 --- a/src/abi/TypedWasm/ABI/ResourceCapabilities.idr +++ b/src/abi/TypedWasm/ABI/ResourceCapabilities.idr @@ -336,3 +336,55 @@ callReachesModule : {owner : ModuleCaps} -> ContainedIn callee.required (declared owner) callReachesModule {caller} {callee} wf = containedTrans (l15cSoundness wf) (l15bSoundness caller) + +-- ============================================================================ +-- L8 ↔ L15 joint composition (A12, 2026-05-26 — closes post-A10 audit item 3) +-- ============================================================================ +-- +-- L8 memory-effects and L15 capabilities live in independent lattices — +-- but typed-wasm functions actually carry BOTH judgements simultaneously +-- (every function attests to its memory effects AND its required caps). +-- The compose theorem here states that the two compose independently: +-- given two functions whose dual budgets are individually witnessed, +-- their sequential composition is witnessed at the unions on both sides. +-- +-- Without this lemma, every compound operation would have to re-verify +-- both halves from scratch. + +||| Containment distributes over capability-set concatenation: if both +||| `xs` and `ys` are contained in the same `declared` set, so is `xs ++ +||| ys`. L15-side prerequisite for `jointBudgetCompose`. +public export +containedConcat : {xs, ys, declared : CapabilitySet} + -> ContainedIn xs declared + -> ContainedIn ys declared + -> ContainedIn (xs ++ ys) declared +containedConcat ContainedNil cy = cy +containedConcat (ContainedCons h r) cy = + ContainedCons h (containedConcat r cy) + +||| L8 ↔ L15 **joint** budget composition. Two functions f, g with +||| individual L8 declarations `d1`/`d2`, individual actual effect sets +||| `a1`/`a2`, and individual function-capability witnesses `c1`/`c2` +||| (each scoped to the same `owner` module) compose to a single +||| function whose: +||| +||| * combined L8 declaration `d1 ++ d2` subsumes combined actuals `a1 ++ a2` +||| (via `subsumeCompose` from Effects.idr); AND +||| * combined required capability set `c1.required ++ c2.required` is +||| contained in the OWNING module's declared capability set +||| (via `containedConcat` + `l15bSoundness`). +||| +||| Closes post-A10 audit item 3 ("No L8↔L15 composition theorem"). +public export +jointBudgetCompose : {owner : ModuleCaps} + -> {d1, d2, a1, a2 : EffectSet} + -> EffectSubsumes d1 a1 + -> EffectSubsumes d2 a2 + -> (c1, c2 : FunctionCaps owner) + -> ( EffectSubsumes (combineEffects d1 d2) (combineEffects a1 a2) + , ContainedIn (c1.required ++ c2.required) (declared owner) + ) +jointBudgetCompose s1 s2 c1 c2 = + (subsumeCompose s1 s2, + containedConcat (l15bSoundness c1) (l15bSoundness c2)) diff --git a/src/abi/TypedWasm/ABI/SessionProtocol.idr b/src/abi/TypedWasm/ABI/SessionProtocol.idr index baec8b6..9fca60c 100644 --- a/src/abi/TypedWasm/ABI/SessionProtocol.idr +++ b/src/abi/TypedWasm/ABI/SessionProtocol.idr @@ -42,6 +42,7 @@ import Data.List import Data.List.Elem import TypedWasm.ABI.Linear +import TypedWasm.ABI.ModuleIsolation %default total @@ -308,3 +309,115 @@ sessionToLinear : {proto : SessionId} -> {state : StateId} -> SessionHandle proto state -> (tk ** LinHandle tk) sessionToLinear h = sessionInner h + +-- ============================================================================ +-- A13 — Cross-Level: L14 (sessions) × L13 (isolation) +-- ============================================================================ +-- +-- Closes the post-A10 audit item 5b (L14 × L13 interaction): when an +-- L14 `SessionHandle` is "moved" from one isolated module to another, +-- the move is mediated by an L13 `AccessWitness` AND preserves the +-- protocol's state index across the boundary. Two propositional +-- claims: +-- +-- 1. **Existence + state preservation**: pairing an `AccessWitness` +-- with a `SessionHandle proto state` produces a +-- `SessionAcrossBoundary` carrying the same state index — the +-- transfer does not silently advance or rewind the protocol. +-- 2. **No-bypass**: any non-local `SessionAcrossBoundary` requires a +-- boundary on the source module's declared list (reused from +-- L13's `crossAccessImpliesBoundary`). +-- +-- The session handle's inner L10 obligation is preserved because the +-- inner `LinHandle` is unchanged across the transfer. This is the +-- L14 × L13 face of the cross-level story already begun in +-- ModuleIsolation.idr by `LinearAcrossBoundary` (L10 × L13). + +||| L14 × L13 cross-level witness: an L14 session handle paired with +||| the L13 access witness that authorises its move from `from` to +||| `to`. The protocol identifier and state index are pinned in the +||| type, so transferring a session handle CANNOT change its state. +public export +data SessionAcrossBoundary : (from, to : IsolatedModuleId) + -> (proto : SessionId) + -> (state : StateId) + -> (regName : String) + -> (bs : BoundaryList) + -> Type where + MkSessionAcrossBoundary : + (aw : AccessWitness from to regName bs) + -> (h : SessionHandle proto state) + -> SessionAcrossBoundary from to proto state regName bs + +||| Project the L13 access witness from a cross-boundary session. +public export +sessionAcrossWitness : + {from, to : IsolatedModuleId} + -> {proto : SessionId} -> {state : StateId} + -> {regName : String} -> {bs : BoundaryList} + -> SessionAcrossBoundary from to proto state regName bs + -> AccessWitness from to regName bs +sessionAcrossWitness (MkSessionAcrossBoundary aw _) = aw + +||| Project the L14 session handle from a cross-boundary session. +public export +sessionAcrossHandle : + {from, to : IsolatedModuleId} + -> {proto : SessionId} -> {state : StateId} + -> {regName : String} -> {bs : BoundaryList} + -> SessionAcrossBoundary from to proto state regName bs + -> SessionHandle proto state +sessionAcrossHandle (MkSessionAcrossBoundary _ h) = h + +||| L14 × L13 soundness (state preservation). +||| +||| Statement: the state index of the session handle inside a +||| `SessionAcrossBoundary` equals the `state` index pinned by the +||| `SessionAcrossBoundary` type. Definitional, but stated as a +||| separate lemma so downstream code can refer to it without +||| unfolding the projection. +public export +sessionAcrossPreservesState : + {from, to : IsolatedModuleId} + -> {proto : SessionId} -> {state : StateId} + -> {regName : String} -> {bs : BoundaryList} + -> (sab : SessionAcrossBoundary from to proto state regName bs) + -> handleState (sessionAcrossHandle sab) = state +sessionAcrossPreservesState (MkSessionAcrossBoundary _ _) = Refl + +||| L14 × L13 soundness (no-bypass). +||| +||| Statement: if a session handle has moved from `from` to `to` and +||| `from /= to`, then the boundary list `bs` of `from` MUST contain a +||| concrete boundary witnessing the transfer. Contrapositive: no +||| boundary means no `SessionAcrossBoundary` exists for a non-local +||| pair — the session handle cannot leave `from`'s memory. +||| +||| Proof: directly reuse `crossAccessImpliesBoundary` on the embedded +||| access witness. Same shape as `linearTransferRequiresBoundary` +||| from ModuleIsolation.idr, just one level up. +public export +sessionTransferRequiresBoundary : + {from, to : IsolatedModuleId} + -> {proto : SessionId} -> {state : StateId} + -> {regName : String} -> {bs : BoundaryList} + -> (xfer : SessionAcrossBoundary from to proto state regName bs) + -> (notLocal : Not (from = to)) + -> (b : Boundary ** Elem b bs) +sessionTransferRequiresBoundary xfer notLocal = + crossAccessImpliesBoundary (sessionAcrossWitness xfer) notLocal + +||| L14 × L13 soundness (local-case). +||| +||| Statement: a session handle moving WITHIN one isolated module +||| (`from = to = m`) needs no boundary — `LocalAccess` suffices and +||| state preservation is automatic. +public export +sessionTransferLocal : + (m : IsolatedModuleId) + -> (regName : String) + -> (bs : BoundaryList) + -> {proto : SessionId} -> {state : StateId} + -> (h : SessionHandle proto state) + -> SessionAcrossBoundary m m proto state regName bs +sessionTransferLocal m _ _ h = MkSessionAcrossBoundary LocalAccess h diff --git a/src/abi/TypedWasm/ABI/VerifierSpec.idr b/src/abi/TypedWasm/ABI/VerifierSpec.idr new file mode 100644 index 0000000..86b1e04 --- /dev/null +++ b/src/abi/TypedWasm/ABI/VerifierSpec.idr @@ -0,0 +1,1299 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- VerifierSpec.idr — Spec-of-record for the post-codegen verifier and +-- the source-side checker (A13, 2026-05-26). +-- +-- This module closes the *statement* side of post-A10 audit items 7 +-- and 8 (Rust verifier ↔ Idris2 spec equivalence; source-checker ↔ +-- verifier coverage agreement). It does NOT close the full +-- equivalence proofs — those require either a full simulation between +-- two implementations (multi-week) or extending the verifier's +-- coverage to every level (similar scope). What it DOES do is pin +-- down the obligations as typed Idris2 predicates, so: +-- +-- * Future proof work can construct witnesses against fixed targets. +-- * The differential testing harness (`tests/cross_compat.rs` + +-- `tests/proof/regression.mjs`) has a concrete spec to point at. +-- * Any drift between this spec and the Rust verifier shows up as a +-- failing fixture. +-- +-- The shape mirrors how `Proofs.idr` introduced `LevelAchievedIn` as +-- a typed obligation before any soundness theorem consumed it: we +-- introduce the predicates first, claim agreement as a record-of- +-- obligations, and let downstream work plug witnesses in. +-- +-- NO `believe_me`, NO `assert_total`, NO `Admitted`. `%default total`. + +module TypedWasm.ABI.VerifierSpec + +import Data.List +import Data.List.Elem +import Decidable.Equality + +import TypedWasm.ABI.Region +import TypedWasm.ABI.Pointer +import TypedWasm.ABI.Linear + +%default total + +-- ============================================================================ +-- Abstract module summary — the surface the verifier and the spec +-- both consume. +-- ============================================================================ +-- +-- The Rust `typed-wasm-verify` crate operates over wasm bytes. The +-- Idris2 spec operates over typed abstractions (Region, LinHandle, +-- ExclusiveWitness, …). Both eventually agree on a SUMMARY of each +-- function: what ownership it claims, which schemas it touches, which +-- linear handles it allocates / consumes. `FunctionSummary` and +-- `ModuleSummary` are the surface used by the agreement predicates. + +||| Ownership intent declared at a function boundary, mirroring the +||| `affinescript.ownership` / `typedwasm.ownership` custom section the +||| Rust verifier reads. +public export +data OwnershipIntent : Type where + ||| Function consumes a linear handle (must free or pass on). + Consumes : (token : Nat) -> OwnershipIntent + ||| Function produces a linear handle (caller takes ownership). + Produces : (token : Nat) -> OwnershipIntent + ||| Function borrows a region (read-only access; no transfer). + Borrows : (schemaTag : Nat) -> OwnershipIntent + ||| Function exclusively borrows a region (mutable; no aliasing). + BorrowsExclusive : (schemaTag : Nat) -> OwnershipIntent + +||| Per-function summary: every ownership intent the function declares, +||| in declaration order. An empty list means a pure function with +||| no resource side-effects. +public export +record FunctionSummary where + constructor MkFunctionSummary + funcName : String + intents : List OwnershipIntent + +||| Per-module summary: the function summaries the module exposes, +||| plus the module's name for diagnostic anchoring. +public export +record ModuleSummary where + constructor MkModuleSummary + modName : String + functions : List FunctionSummary + +-- ============================================================================ +-- Spec-of-record acceptance predicate +-- ============================================================================ +-- +-- `SpecAccepts m` is the Idris2 L7 (aliasing) + L10 (linearity) +-- acceptance criterion on a `ModuleSummary`. It is structural: no +-- two `Consumes` intents may share a token (otherwise some handle is +-- double-consumed); every `Produces` token must be unique within the +-- module (otherwise two functions promise the same allocation). This +-- is the *spec* the Rust verifier must agree with. +-- +-- The predicate is INTENTIONALLY narrow: it captures only what +-- typed-wasm-verify currently checks (L7 + L10 over a module's +-- ownership custom section). Extending it to L13/L14/L15 is part of +-- the source-checker ↔ verifier coverage agreement (item 8 below). + +||| `TokenFresh tok intents` — `tok` does not appear as a `Consumes` +||| or `Produces` token in the intent list. The structural witness +||| underlying L10 single-consumption per module. +public export +data TokenFresh : (tok : Nat) -> List OwnershipIntent -> Type where + TFNil : TokenFresh tok [] + TFConsumesOther : (Not (t = tok)) + -> TokenFresh tok rest + -> TokenFresh tok (Consumes t :: rest) + TFProducesOther : (Not (t = tok)) + -> TokenFresh tok rest + -> TokenFresh tok (Produces t :: rest) + TFBorrows : TokenFresh tok rest -> TokenFresh tok (Borrows s :: rest) + TFBorrowsExclusive : + TokenFresh tok rest -> TokenFresh tok (BorrowsExclusive s :: rest) + +||| `IntentsLinearAcceptable intents` — every `Consumes`/`Produces` +||| token in the list is unique. This is the L10 single-consumption +||| witness lifted to a whole intent list, structurally. +public export +data IntentsLinearAcceptable : List OwnershipIntent -> Type where + ILANil : IntentsLinearAcceptable [] + ILAConsumes : (fresh : TokenFresh tok rest) + -> IntentsLinearAcceptable rest + -> IntentsLinearAcceptable (Consumes tok :: rest) + ILAProduces : (fresh : TokenFresh tok rest) + -> IntentsLinearAcceptable rest + -> IntentsLinearAcceptable (Produces tok :: rest) + ILABorrows : IntentsLinearAcceptable rest + -> IntentsLinearAcceptable (Borrows s :: rest) + ILABorrowsExclusive : + IntentsLinearAcceptable rest + -> IntentsLinearAcceptable (BorrowsExclusive s :: rest) + +||| Per-function structural acceptance lifted across the function list, +||| matching how the verifier walks the module's export section. Used +||| by `SpecAccepts`, `VerifierAccepts`, and `SourceAccepts` so all +||| three agree on the structural witness shape at L7+L10. +public export +data FunctionsAccepted : List FunctionSummary -> Type where + FANil : FunctionsAccepted [] + FACons : IntentsLinearAcceptable f.intents + -> FunctionsAccepted rest + -> FunctionsAccepted (f :: rest) + +||| `SpecAccepts m` — the Idris2 spec accepts a module summary. Wraps +||| `FunctionsAccepted` on the function list so spec / verifier / +||| source-checker share a single canonical structural witness at the +||| L7+L10 layer. Future extensions (L13 cross-module checks, L14 +||| session-state) add new constructors without breaking existing +||| structural witnesses. +public export +data SpecAccepts : ModuleSummary -> Type where + MkSpecAccepts : + FunctionsAccepted m.functions + -> SpecAccepts m + +-- ============================================================================ +-- Verifier acceptance (inductive — structural + differential cases) +-- ============================================================================ +-- +-- The Rust verifier's acceptance set has two flavours of evidence: +-- +-- 1. STRUCTURAL — for modules whose ownership intents are visible at +-- the typed surface, the verifier's L7+L10 acceptance is exactly +-- the same predicate the spec uses. No trust-injection needed. +-- 2. DIFFERENTIAL — for modules whose typed surface is partial (the +-- Rust verifier inspects wasm bytes via wasmparser), the only +-- legitimate way to assert verifier-acceptance is through a row +-- in the differential testing table (`tests/cross_compat.rs`). +-- +-- The earlier opaque design (A13) collapsed both cases into a single +-- "external evidence" constructor. That made every agreement +-- direction unprovable (no introspection into the witness). The +-- inductive split below restores provability of the structural cases +-- while keeping the differential case auditable. + +||| Inductive verifier-acceptance predicate, indexed by `ModuleSummary`. +||| Two constructors expose the trust shape: +||| +||| * `VAStructural` — verifier acceptance derived from the same +||| structural predicate the spec uses. No external trust; +||| introspectable witness. +||| * `VADifferential` — verifier acceptance via the differential +||| harness. External trust pinned to a fixture row. Searching +||| for this constructor enumerates every trust-injection site. +public export +data VerifierAccepts : ModuleSummary -> Type where + ||| Structural verifier acceptance: every exported function's + ||| intent list passes the L10 single-consumption / L7 aliasing check. + ||| This is the case the spec and the verifier agree on by definition. + VAStructural : + FunctionsAccepted m.functions + -> VerifierAccepts m + ||| Differential verifier acceptance: external evidence from + ||| `tests/cross_compat.rs` pinning a fixture row. Constructible + ||| only via `differentialAccepted` so the trust boundary is + ||| inspectable. + VADifferential : + (differentialEvidence : String) + -> (fixtureId : Nat) + -> VerifierAccepts m + +||| Construct a `VerifierAccepts` witness from differential-harness +||| evidence (fixture name + numeric id from `tests/cross_compat.rs`). +||| Naming the fixture in the witness makes the trust boundary +||| inspectable: every `VADifferential` use can be traced back to a +||| concrete row in the differential table. +public export +differentialAccepted : (fixtureName : String) -> (fixtureId : Nat) + -> VerifierAccepts m +differentialAccepted name fid = VADifferential name fid + +-- ============================================================================ +-- Source-checker acceptance (item 8 surface) +-- ============================================================================ + +||| Source-checker acceptance predicate. Like `VerifierAccepts`, the +||| source checker has both a structural surface (typed AST) and a +||| differential side (cross-checked against fixtures when the source +||| AST is partial). Same two-constructor shape, same audit story. +public export +data SourceAccepts : ModuleSummary -> Type where + ||| Structural source-checker acceptance: lifted from + ||| `FunctionsAccepted` exactly as the spec sees it. + SAStructural : + FunctionsAccepted m.functions + -> SourceAccepts m + ||| Differential source-checker acceptance: external evidence from a + ||| source-side fixture row. + SADifferential : + (sourceEvidence : String) + -> (fixtureId : Nat) + -> SourceAccepts m + +||| Construct a `SourceAccepts` witness from source-side evidence. +public export +sourceAccepted : (fixtureName : String) -> (fixtureId : Nat) + -> SourceAccepts m +sourceAccepted name fid = SADifferential name fid + +-- ============================================================================ +-- Agreement obligations — items 7 and 8 +-- ============================================================================ +-- +-- The two agreement obligations are stated as Idris2 propositions +-- ("for every module summary, if the spec accepts then the verifier +-- accepts, and vice versa"). Witnesses are NOT discharged here; they +-- are the long-tail proof work. What this module DOES discharge is +-- the *shape*: anyone trying to claim agreement now has a typed +-- target to aim at, and the differential harness's existing fixtures +-- can be re-cast as partial witnesses. + +||| Item 7 obligation — Rust verifier ↔ Idris2 spec equivalence. +||| +||| * **Soundness direction**: every module the verifier accepts is +||| spec-accepted (the verifier doesn't accept anything unsafe). +||| * **Completeness direction**: every spec-accepted module is +||| verifier-accepted (the verifier doesn't reject anything safe). +||| +||| The record bundles the two directions so partial proofs can land +||| one face at a time. A full witness would discharge BOTH fields. +public export +record VerifierSpecAgreement where + constructor MkVerifierSpecAgreement + verifierIsSound : + (m : ModuleSummary) -> VerifierAccepts m -> SpecAccepts m + verifierIsComplete : + (m : ModuleSummary) -> SpecAccepts m -> VerifierAccepts m + +||| Item 8 obligation — source-checker ↔ verifier coverage agreement. +||| +||| * **Source-implies-verifier**: every module the source checker +||| accepts is also verifier-accepted (the verifier covers +||| everything the source checker promises). +||| * **Verifier-implies-source**: every verifier-accepted module is +||| also source-acceptable (the verifier doesn't outgrow the +||| source checker's coverage envelope). +||| +||| The "verifier outgrows source checker" direction is the actual +||| source-checker-coverage extension obligation: the source checker +||| has to be extended to cover whatever the verifier checks beyond +||| L7+L10 (L13 cross-module, L14 session-state, etc.). +public export +record SourceVerifierAgreement where + constructor MkSourceVerifierAgreement + sourceImpliesVerifier : + (m : ModuleSummary) -> SourceAccepts m -> VerifierAccepts m + verifierImpliesSource : + (m : ModuleSummary) -> VerifierAccepts m -> SourceAccepts m + +-- ============================================================================ +-- Trivial consequences (statement-level corollaries) +-- ============================================================================ + +||| If both agreements hold, source acceptance and spec acceptance +||| coincide. Composition: source → verifier → spec via the two +||| soundness directions. Stated to give the test harness an +||| end-to-end target predicate to assert against. +public export +sourceImpliesSpec : + (vsa : VerifierSpecAgreement) + -> (sva : SourceVerifierAgreement) + -> (m : ModuleSummary) + -> SourceAccepts m + -> SpecAccepts m +sourceImpliesSpec vsa sva m srcAcc = + vsa.verifierIsSound m (sva.sourceImpliesVerifier m srcAcc) + +||| Symmetric composition: spec → verifier → source via completeness. +||| Closes the loop: under both agreements, the three predicates +||| (`SpecAccepts`, `VerifierAccepts`, `SourceAccepts`) are +||| extensionally equivalent on every module summary. +public export +specImpliesSource : + (vsa : VerifierSpecAgreement) + -> (sva : SourceVerifierAgreement) + -> (m : ModuleSummary) + -> SpecAccepts m + -> SourceAccepts m +specImpliesSource vsa sva m specAcc = + sva.verifierImpliesSource m (vsa.verifierIsComplete m specAcc) + +-- ============================================================================ +-- Structural agreement — first concrete witnesses (items 7 + 8, partial) +-- ============================================================================ +-- +-- The full `VerifierSpecAgreement` / `SourceVerifierAgreement` records +-- above remain obligations because their generality covers both +-- structural and differential evidence: the differential case requires +-- an external connection (wasm-bytes semantics or fixture-row trust) +-- and is multi-week. +-- +-- What IS provable, total, no-trust-injection, is the agreement +-- restricted to the structural cases. The records and lemmas below +-- give those a concrete home. Future work plugs the differential +-- cases in by extending these records (e.g. by lifting fixture +-- evidence into a stratified-acceptance predicate). +-- +-- Convention: every name in this section ends in `Structural` so the +-- restriction to the structural sublattice is visible at call sites. + +||| `FunctionsAccepted` directly witnesses `SpecAccepts`. This is the +||| spec's structural inhabitant: any function-list witness gives a +||| spec acceptance witness for the enclosing module. +public export +functionsAcceptedImpliesSpec : + {m : ModuleSummary} + -> FunctionsAccepted m.functions + -> SpecAccepts m +functionsAcceptedImpliesSpec fa = MkSpecAccepts fa + +||| Inverse direction: a spec acceptance witness contains the +||| structural per-function witness. +public export +specImpliesFunctionsAccepted : + {m : ModuleSummary} + -> SpecAccepts m + -> FunctionsAccepted m.functions +specImpliesFunctionsAccepted (MkSpecAccepts fa) = fa + +||| Spec → verifier (structural case). Lifts spec acceptance directly +||| into `VAStructural` — no trust-injection. +public export +specImpliesVerifierStructural : + {m : ModuleSummary} + -> SpecAccepts m + -> VerifierAccepts m +specImpliesVerifierStructural (MkSpecAccepts fa) = VAStructural fa + +||| Spec → source (structural case). Symmetric to the verifier +||| direction; lifts spec acceptance into `SAStructural`. +public export +specImpliesSourceStructural : + {m : ModuleSummary} + -> SpecAccepts m + -> SourceAccepts m +specImpliesSourceStructural (MkSpecAccepts fa) = SAStructural fa + +||| Verifier → spec (structural case only). Defined on `VAStructural` +||| witnesses; the `VADifferential` case is the multi-week obligation +||| and is therefore reflected as a `Maybe` here so totality is +||| preserved without `believe_me`. +public export +verifierImpliesSpecStructural : + {m : ModuleSummary} + -> VerifierAccepts m + -> Maybe (SpecAccepts m) +verifierImpliesSpecStructural (VAStructural fa) = Just (MkSpecAccepts fa) +verifierImpliesSpecStructural (VADifferential _ _) = Nothing + +||| Source → spec (structural case only). Mirrors +||| `verifierImpliesSpecStructural` for the source side. +public export +sourceImpliesSpecStructural : + {m : ModuleSummary} + -> SourceAccepts m + -> Maybe (SpecAccepts m) +sourceImpliesSpecStructural (SAStructural fa) = Just (MkSpecAccepts fa) +sourceImpliesSpecStructural (SADifferential _ _) = Nothing + +||| Bundle of structural-case agreement directions. Differs from +||| `VerifierSpecAgreement` / `SourceVerifierAgreement` in three ways: +||| +||| 1. Restricted to the structural sublattice — `VADifferential` +||| and `SADifferential` are NOT covered. +||| 2. Provable as a total Idris2 value (`structuralAgreement` below). +||| 3. Symmetric across all three predicates simultaneously. +||| +||| This is the first concrete agreement value in the codebase that +||| relates the spec / verifier / source-checker acceptance predicates +||| without invoking external evidence. +public export +record StructuralAgreement where + constructor MkStructuralAgreement + saSpecToVerifier : + (m : ModuleSummary) -> SpecAccepts m -> VerifierAccepts m + saSpecToSource : + (m : ModuleSummary) -> SpecAccepts m -> SourceAccepts m + saVerifierStructuralToSpec : + (m : ModuleSummary) -> FunctionsAccepted m.functions -> SpecAccepts m + saSourceStructuralToSpec : + (m : ModuleSummary) -> FunctionsAccepted m.functions -> SpecAccepts m + +||| Concrete witness for `StructuralAgreement`. Total. No +||| `believe_me`, no `postulate`, no external trust. Closes the +||| structural-case portion of items 7 and 8 from the post-A10 audit. +public export +structuralAgreement : StructuralAgreement +structuralAgreement = MkStructuralAgreement + (\m, sa => specImpliesVerifierStructural sa) + (\m, sa => specImpliesSourceStructural sa) + (\m, fa => functionsAcceptedImpliesSpec fa) + (\m, fa => functionsAcceptedImpliesSpec fa) + +-- ============================================================================ +-- Concrete instance proofs — empty module +-- ============================================================================ +-- +-- The empty-module case is the first concrete `SpecAccepts` +-- inhabitant: no functions, so the per-function obligation is +-- trivially satisfied. Used by the regression test as a smoke check +-- that the predicates aren't vacuously unprovable. + +||| Structural witness for an empty function list. Closes the L7+L10 +||| obligations vacuously. +public export +emptyFunctionsAccepted : FunctionsAccepted [] +emptyFunctionsAccepted = FANil + +||| The spec accepts every module whose function list is empty. +||| Concrete inhabitant of `SpecAccepts`. Demonstrates the predicate +||| is not vacuously empty. +public export +emptyModuleSpecAccepts : + (n : String) -> SpecAccepts (MkModuleSummary n []) +emptyModuleSpecAccepts n = MkSpecAccepts FANil + +||| The verifier accepts every empty-module summary via the structural +||| constructor (no differential evidence needed). +public export +emptyModuleVerifierAccepts : + (n : String) -> VerifierAccepts (MkModuleSummary n []) +emptyModuleVerifierAccepts n = VAStructural FANil + +||| The source checker accepts every empty-module summary. +public export +emptyModuleSourceAccepts : + (n : String) -> SourceAccepts (MkModuleSummary n []) +emptyModuleSourceAccepts n = SAStructural FANil + +-- ============================================================================ +-- Concrete instance proofs — non-empty module (alloc / free pair) +-- ============================================================================ +-- +-- The minimal interesting case: a module exporting an allocator +-- (`Produces 0`) and a deallocator (`Consumes 0`). This is the +-- smallest non-vacuous L10 single-consumption witness: +-- +-- * `Produces 0` introduces handle token 0. +-- * `Consumes 0` consumes it exactly once. +-- * `TokenFresh 0 []` for each per-function obligation is trivial. +-- +-- Demonstrates that the structural witness machinery scales past the +-- empty list, and exercises every `ILA*` / `TF*` constructor needed to +-- build a real witness. + +||| Demo module: one allocator + one deallocator, sharing token 0. +||| The canonical "valid pair" example. Used by the discrimination +||| section below to contrast with `badDoubleConsumeModule`. +public export +allocFreeModule : ModuleSummary +allocFreeModule = MkModuleSummary "allocFree" + [ MkFunctionSummary "alloc" [Produces 0] + , MkFunctionSummary "free" [Consumes 0] + ] + +||| Spec acceptance witness for `allocFreeModule`. Built from raw +||| structural constructors: `ILAProduces` for the allocator, +||| `ILAConsumes` for the deallocator, `TFNil` for the trivial +||| per-function freshness obligations. +public export +allocFreeSpecAccepts : SpecAccepts VerifierSpec.allocFreeModule +allocFreeSpecAccepts = MkSpecAccepts + (FACons (ILAProduces TFNil ILANil) + (FACons (ILAConsumes TFNil ILANil) + FANil)) + +||| Verifier acceptance for `allocFreeModule`, derived via the +||| structural spec→verifier direction. Concrete demonstration that +||| the agreement value works on a real, non-empty module. +public export +allocFreeVerifierAccepts : VerifierAccepts VerifierSpec.allocFreeModule +allocFreeVerifierAccepts = + specImpliesVerifierStructural allocFreeSpecAccepts + +||| Source-checker acceptance for `allocFreeModule`, derived via the +||| structural spec→source direction. Closes the structural triangle +||| for a real module. +public export +allocFreeSourceAccepts : SourceAccepts VerifierSpec.allocFreeModule +allocFreeSourceAccepts = + specImpliesSourceStructural allocFreeSpecAccepts + +-- ============================================================================ +-- Discrimination — predicate rejects bad modules +-- ============================================================================ +-- +-- A predicate is only useful if it discriminates: there must be some +-- module the spec REJECTS. Without a `Not (SpecAccepts badModule)` +-- proof, the predicate could be vacuously true on everything and pass +-- every regression test. The proof below exhibits a concrete bad +-- module and shows the L10 single-consumption rule has teeth. + +||| Bad module: one function double-consumes token 0. Violates L10 +||| (a linear handle is consumed twice). The structural witness +||| machinery should make `SpecAccepts` of this module impossible. +public export +badDoubleConsumeModule : ModuleSummary +badDoubleConsumeModule = MkModuleSummary "badDoubleConsume" + [ MkFunctionSummary "doubleFree" [Consumes 0, Consumes 0] + ] + +||| The spec does not accept `badDoubleConsumeModule`. This is the +||| discrimination proof: assuming an acceptance witness, we extract +||| the `TokenFresh 0 [Consumes 0]` obligation that `ILAConsumes` +||| requires. The only constructor matching that shape is +||| `TFConsumesOther (Not (0 = 0)) _`, and applying `Refl` to the +||| `Not (0 = 0)` produces `Void`. Demonstrates L10 has teeth. +public export +notSpecAcceptsBadDoubleConsume : + Not (SpecAccepts VerifierSpec.badDoubleConsumeModule) +notSpecAcceptsBadDoubleConsume + (MkSpecAccepts (FACons (ILAConsumes (TFConsumesOther noteq _) _) _)) = + noteq Refl + +||| Symmetric: the structural verifier witness is also impossible for +||| the bad module. (The `VADifferential` case is not ruled out by +||| this lemma — that escape hatch is by design and remains the +||| differential-trust obligation.) +public export +notVerifierStructuralAcceptsBadDoubleConsume : + Not (FunctionsAccepted VerifierSpec.badDoubleConsumeModule.functions) +notVerifierStructuralAcceptsBadDoubleConsume + (FACons (ILAConsumes (TFConsumesOther noteq _) _) _) = + noteq Refl + +||| A second L10 rejection path: `[Produces 0, Produces 0]`. +||| The L10 single-consumption rule forbids any token from appearing +||| twice in a function's intent list, regardless of `Consumes` / +||| `Produces` direction. Distinct from `badDoubleConsumeModule` +||| because it exercises the `ILAProduces` / `TFProducesOther` +||| constructor pair instead of the `ILAConsumes` / `TFConsumesOther` +||| pair. +public export +badDoubleProduceModule : ModuleSummary +badDoubleProduceModule = MkModuleSummary "badDoubleProduce" + [ MkFunctionSummary "doubleAlloc" [Produces 0, Produces 0] + ] + +||| The spec does not accept `badDoubleProduceModule`. Mirror of +||| `notSpecAcceptsBadDoubleConsume` for the `Produces` branch. +public export +notSpecAcceptsBadDoubleProduce : + Not (SpecAccepts VerifierSpec.badDoubleProduceModule) +notSpecAcceptsBadDoubleProduce + (MkSpecAccepts (FACons (ILAProduces (TFProducesOther noteq _) _) _)) = + noteq Refl + +||| A third L10 rejection path: a token mixes `Consumes` with +||| `Produces` in the same function. `[Consumes 0, Produces 0]` +||| violates the per-function single-occurrence rule because the +||| `ILAConsumes` constructor demands `TokenFresh 0 [Produces 0]`, +||| which only `TFProducesOther` can witness, which in turn requires +||| `Not (0 = 0)`. +public export +badConsumeProduceMixModule : ModuleSummary +badConsumeProduceMixModule = MkModuleSummary "badConsumeProduceMix" + [ MkFunctionSummary "mixed" [Consumes 0, Produces 0] + ] + +||| The spec does not accept `badConsumeProduceMixModule`. Exercises +||| the cross-direction case: the rejection witness is +||| `TFProducesOther (Not (0 = 0)) _` inside an `ILAConsumes` shell. +public export +notSpecAcceptsBadConsumeProduceMix : + Not (SpecAccepts VerifierSpec.badConsumeProduceMixModule) +notSpecAcceptsBadConsumeProduceMix + (MkSpecAccepts (FACons (ILAConsumes (TFProducesOther noteq _) _) _)) = + noteq Refl + +-- ============================================================================ +-- Extended allocFreeModule — exercises all four OwnershipIntent +-- constructors (Produces / Consumes / Borrows / BorrowsExclusive) +-- ============================================================================ +-- +-- The base `allocFreeModule` exercises only the linear pair +-- (Produces 0 / Consumes 0). The extended variant adds a borrowing +-- pattern alongside, exercising both `Borrows` (read-only) and +-- `BorrowsExclusive` (mutable), and shows the structural witness +-- machinery handles all four constructors in a single module. +-- +-- Schema tags 1 and 2 are used so the borrow intents don't collide +-- structurally with the linear token 0 (which lives in a separate +-- index namespace anyway, but keeping them distinct makes the +-- intent table easier to read). + +||| Demo module exercising all four `OwnershipIntent` constructors. +||| +||| * `alloc` produces a linear handle (token 0). +||| * `read` borrows schema 1 (read-only). +||| * `update` borrows schema 2 exclusively (mutable). +||| * `free` consumes the linear handle. +public export +allocFreeWithBorrowModule : ModuleSummary +allocFreeWithBorrowModule = MkModuleSummary "allocFreeWithBorrow" + [ MkFunctionSummary "alloc" [Produces 0] + , MkFunctionSummary "read" [Borrows 1] + , MkFunctionSummary "update" [BorrowsExclusive 2] + , MkFunctionSummary "free" [Consumes 0] + ] + +||| Spec acceptance witness for `allocFreeWithBorrowModule`. Exercises +||| `ILAProduces` / `ILABorrows` / `ILABorrowsExclusive` / `ILAConsumes` +||| in a single witness — the full four-constructor coverage of +||| `IntentsLinearAcceptable`. +public export +allocFreeWithBorrowSpecAccepts : + SpecAccepts VerifierSpec.allocFreeWithBorrowModule +allocFreeWithBorrowSpecAccepts = MkSpecAccepts + (FACons (ILAProduces TFNil ILANil) + (FACons (ILABorrows ILANil) + (FACons (ILABorrowsExclusive ILANil) + (FACons (ILAConsumes TFNil ILANil) + FANil)))) + +||| Verifier acceptance for the four-constructor demo module, derived +||| via `specImpliesVerifierStructural`. +public export +allocFreeWithBorrowVerifierAccepts : + VerifierAccepts VerifierSpec.allocFreeWithBorrowModule +allocFreeWithBorrowVerifierAccepts = + specImpliesVerifierStructural allocFreeWithBorrowSpecAccepts + +||| Source-checker acceptance for the four-constructor demo module. +public export +allocFreeWithBorrowSourceAccepts : + SourceAccepts VerifierSpec.allocFreeWithBorrowModule +allocFreeWithBorrowSourceAccepts = + specImpliesSourceStructural allocFreeWithBorrowSpecAccepts + +-- ============================================================================ +-- ExtendedAgreement — constructive bridge from VADifferential to spec +-- ============================================================================ +-- +-- The `StructuralAgreement` value above closes the structural +-- sublattice but leaves `VADifferential` evidence dangling: there is +-- no provable `(m : ModuleSummary) -> VerifierAccepts m -> SpecAccepts m` +-- that handles `VADifferential` cases, because a fixture name + id +-- alone carry no structural information. +-- +-- The trust pattern below relocates the trust-injection moment from +-- "every VADifferential witness use" to "fixture registration time". +-- A `TrustedFixture` packages a fixture name + id with the structural +-- witness the fixture is claimed to certify. Constructing a +-- `TrustedFixture` IS the trust-injection — but once constructed, the +-- witness is structural, so downstream proofs of agreement use the +-- structural directions only. +-- +-- This is the constructive bridge: the trust still has to be injected +-- somewhere (because the Rust verifier inspects wasm bytes; Idris2 +-- cannot do that itself), but it's injected once per fixture, with +-- the fixture name pinned in the witness type, instead of being +-- injected anew at every consumer of `VerifierSpecAgreement`. + +||| A trusted fixture: pairs the differential evidence (fixture name + +||| id) with the structural witness the fixture is supposed to +||| certify. Constructing one is the trust-injection moment. Search +||| for `MkTrustedFixture` to enumerate every fixture trust-injection. +public export +record TrustedFixture (m : ModuleSummary) where + constructor MkTrustedFixture + trustedFixtureName : String + trustedFixtureId : Nat + trustedWitness : FunctionsAccepted m.functions + +||| A `TrustedFixture` projects to `VerifierAccepts` via the +||| structural constructor — no further trust injection at use site. +public export +trustedToVerifier : TrustedFixture m -> VerifierAccepts m +trustedToVerifier (MkTrustedFixture _ _ w) = VAStructural w + +||| A `TrustedFixture` projects to `SpecAccepts` similarly. +public export +trustedToSpec : TrustedFixture m -> SpecAccepts m +trustedToSpec (MkTrustedFixture _ _ w) = MkSpecAccepts w + +||| A `TrustedFixture` projects to `SourceAccepts` similarly. +public export +trustedToSource : TrustedFixture m -> SourceAccepts m +trustedToSource (MkTrustedFixture _ _ w) = SAStructural w + +||| `ExtendedAgreement` — `StructuralAgreement` plus a fixture lookup. +||| A consumer with an `ExtendedAgreement` and a `VADifferential` +||| witness can ask the lookup for the matching `TrustedFixture` and +||| obtain a structural witness — turning the dangling differential +||| case into a structural one. +||| +||| The lookup returns `Maybe` because not every fixture name will be +||| registered. An empty `ExtendedAgreement` (returning `Nothing` +||| everywhere) trivially exists; populated ones grow as fixtures are +||| audited. See `emptyExtendedAgreement` for the empty witness. +public export +record ExtendedAgreement where + constructor MkExtendedAgreement + baseStructural : StructuralAgreement + fixtureLookup : + (m : ModuleSummary) + -> (fixtureName : String) + -> (fixtureId : Nat) + -> Maybe (TrustedFixture m) + +||| The empty `ExtendedAgreement`: structural agreement plus a lookup +||| that returns `Nothing` for every fixture. Concrete inhabitant +||| showing the record is constructible without external trust. +||| Future fixture audits replace the lookup with non-empty +||| dispatchers. +public export +emptyExtendedAgreement : ExtendedAgreement +emptyExtendedAgreement = MkExtendedAgreement + structuralAgreement + (\_, _, _ => Nothing) + +||| Promote a `VADifferential` witness to `SpecAccepts` using an +||| `ExtendedAgreement`. Returns `Nothing` if the fixture is not +||| registered. Total — no `believe_me`, no `assert_total`. +||| +||| This is the constructive bridge promised by the section header: +||| a `VADifferential` witness plus a registered fixture produces a +||| structural-grade spec acceptance. +public export +verifierImpliesSpecExtended : + ExtendedAgreement + -> (m : ModuleSummary) + -> VerifierAccepts m + -> Maybe (SpecAccepts m) +verifierImpliesSpecExtended _ _ (VAStructural fa) = + Just (MkSpecAccepts fa) +verifierImpliesSpecExtended ext m (VADifferential name fid) = + map trustedToSpec (ext.fixtureLookup m name fid) + +||| Symmetric direction: `SADifferential` to `SpecAccepts` via the +||| same fixture-lookup mechanism. Both source and verifier +||| differential cases route through the same fixture registry. +public export +sourceImpliesSpecExtended : + ExtendedAgreement + -> (m : ModuleSummary) + -> SourceAccepts m + -> Maybe (SpecAccepts m) +sourceImpliesSpecExtended _ _ (SAStructural fa) = + Just (MkSpecAccepts fa) +sourceImpliesSpecExtended ext m (SADifferential name fid) = + map trustedToSpec (ext.fixtureLookup m name fid) + +-- ============================================================================ +-- First concrete TrustedFixture — derived from cross_compat.rs row 1 +-- ============================================================================ +-- +-- `emptyExtendedAgreement` above shows `ExtendedAgreement` is +-- constructible; this section shows it can carry real evidence. The +-- fixture below mirrors row 1 of +-- `crates/typed-wasm-verify/tests/cross_compat.rs` +-- (`fixture_clean_linear_consumer`) — the minimal Rust-verifier +-- regression case proving the verifier accepts a single-function +-- module that consumes one linear handle. +-- +-- The conceptual AffineScript source for that fixture is: +-- +-- fn consume(s: own Handle): unit = drop s +-- +-- which lowers to a wasm function with one `Linear` parameter, +-- consumed exactly once via `local.get; drop`. In `ModuleSummary` +-- terms: one function with `[Consumes 0]`. +-- +-- This is the first **non-trivial** `TrustedFixture` in the codebase: +-- a concrete pairing of a real differential-harness row with its +-- structural witness. Future fixture rows append in the same shape. + +||| `ModuleSummary` mirror of `cross_compat::fixture_clean_linear_consumer`. +||| Single function with a single `Consumes 0` intent. +public export +fixtureCleanLinearConsumerModule : ModuleSummary +fixtureCleanLinearConsumerModule = MkModuleSummary "fixture_clean_linear_consumer" + [ MkFunctionSummary "consume" [Consumes 0] + ] + +||| Structural witness for the fixture's intents. Uses `ILAConsumes` +||| with the vacuous `TFNil` freshness obligation (no other intents +||| in the tail). +public export +fixtureCleanLinearConsumerWitness : + FunctionsAccepted VerifierSpec.fixtureCleanLinearConsumerModule.functions +fixtureCleanLinearConsumerWitness = + FACons (ILAConsumes TFNil ILANil) FANil + +||| First concrete `TrustedFixture` value. Fixture id `1` matches the +||| row number in `cross_compat.rs` (fixture_clean_linear_consumer is +||| the first `#[test]` in the file). Constructing this is the +||| single trust-injection point for this fixture row — every +||| downstream use re-projects from this single value. +public export +fixtureCleanLinearConsumerTrusted : + TrustedFixture VerifierSpec.fixtureCleanLinearConsumerModule +fixtureCleanLinearConsumerTrusted = MkTrustedFixture + "fixture_clean_linear_consumer" + 1 + fixtureCleanLinearConsumerWitness + +||| Derived `SpecAccepts` for the fixture, via `trustedToSpec`. +||| Demonstrates the path from a fixture-pinned trust-injection to a +||| structural-grade spec acceptance. +public export +fixtureCleanLinearConsumerSpecAccepts : + SpecAccepts VerifierSpec.fixtureCleanLinearConsumerModule +fixtureCleanLinearConsumerSpecAccepts = + trustedToSpec fixtureCleanLinearConsumerTrusted + +||| Derived `VerifierAccepts` via `trustedToVerifier` — the +||| differential case now has a concrete structural witness +||| underneath, no longer just a name + id. +public export +fixtureCleanLinearConsumerVerifierAccepts : + VerifierAccepts VerifierSpec.fixtureCleanLinearConsumerModule +fixtureCleanLinearConsumerVerifierAccepts = + trustedToVerifier fixtureCleanLinearConsumerTrusted + +||| Symmetric source-side witness. +public export +fixtureCleanLinearConsumerSourceAccepts : + SourceAccepts VerifierSpec.fixtureCleanLinearConsumerModule +fixtureCleanLinearConsumerSourceAccepts = + trustedToSource fixtureCleanLinearConsumerTrusted + +-- Note on full dispatch. A fully discriminating `fixtureLookup` — +-- `(m : ModuleSummary) -> String -> Nat -> Maybe (TrustedFixture m)` +-- that returns the fixture only when `m` matches structurally — +-- requires decidable equality on `ModuleSummary` (string + list-of- +-- records decEq). That's a mechanical follow-up. Until it lands, +-- the four projections above are usable directly at call sites where +-- the module is known to be `fixtureCleanLinearConsumerModule`. + +-- ============================================================================ +-- Additional TrustedFixtures — cross_compat.rs rows 9 + 10 +-- ============================================================================ +-- +-- Rows 9 and 10 are the other single-module "verifier accepts" +-- fixtures in cross_compat.rs. Rows 2 / 3 / 4 / 5 / 7 / 8 reject +-- for body-level reasons (LinearUsedMultiple, LinearDroppedOnSomePath, +-- ExclBorrowAliased, LinearImportCalledMultiple) which our +-- summary-level `SpecAccepts` predicate does not model — those rows +-- structurally pass the L10 intent-list rule but fail the wasm-body +-- traversal that the Rust verifier performs in addition. TrustedFixture +-- claims structural witness existence, so it does not apply to those +-- rows; see `notSpecAcceptsBadDoubleConsume` family for the +-- predicate-rejection pattern (different shape). Rows 6 / 7 / 8 are +-- cross-module — a separate modelling track from single-module +-- ModuleSummary, also out of scope for this slice. + +-- ---------------------------------------------------------------------------- +-- Row 9 — fixture_extract_exports_three_shapes +-- ---------------------------------------------------------------------------- +-- +-- Three exported functions exercising three different OwnershipKind +-- mappings: +-- +-- consume_string : Linear → Consumes 0 +-- borrow_buffer_mut : ExclBorrow → BorrowsExclusive 0 +-- read_count : Unrestricted → [] (no tracked intent) +-- +-- This fixture exercises the export-extraction API rather than +-- `verify_from_module`, but the module's intent lists are structurally +-- clean so a TrustedFixture is still constructible. + +||| `ModuleSummary` mirror of `cross_compat::fixture_extract_exports_three_shapes`. +public export +fixtureExtractExportsModule : ModuleSummary +fixtureExtractExportsModule = MkModuleSummary "fixture_extract_exports_three_shapes" + [ MkFunctionSummary "consume_string" [Consumes 0] + , MkFunctionSummary "borrow_buffer_mut" [BorrowsExclusive 0] + , MkFunctionSummary "read_count" [] + ] + +||| Structural witness for the three-function fixture. +public export +fixtureExtractExportsWitness : + FunctionsAccepted VerifierSpec.fixtureExtractExportsModule.functions +fixtureExtractExportsWitness = + FACons (ILAConsumes TFNil ILANil) + (FACons (ILABorrowsExclusive ILANil) + (FACons ILANil + FANil)) + +||| TrustedFixture for cross_compat row 9. +public export +fixtureExtractExportsTrusted : + TrustedFixture VerifierSpec.fixtureExtractExportsModule +fixtureExtractExportsTrusted = MkTrustedFixture + "fixture_extract_exports_three_shapes" + 9 + fixtureExtractExportsWitness + +||| Projections via the `trustedTo*` family. +public export +fixtureExtractExportsSpecAccepts : + SpecAccepts VerifierSpec.fixtureExtractExportsModule +fixtureExtractExportsSpecAccepts = trustedToSpec fixtureExtractExportsTrusted + +public export +fixtureExtractExportsVerifierAccepts : + VerifierAccepts VerifierSpec.fixtureExtractExportsModule +fixtureExtractExportsVerifierAccepts = trustedToVerifier fixtureExtractExportsTrusted + +public export +fixtureExtractExportsSourceAccepts : + SourceAccepts VerifierSpec.fixtureExtractExportsModule +fixtureExtractExportsSourceAccepts = trustedToSource fixtureExtractExportsTrusted + +-- ---------------------------------------------------------------------------- +-- Row 10 — fixture_realistic_clean_module +-- ---------------------------------------------------------------------------- +-- +-- Four functions exercising the realistic mixed-ownership shape: +-- +-- fn 0 — Linear → Consumes 0 +-- fn 1 — ExclBorrow → BorrowsExclusive 0 +-- fn 2 — Unrestricted → [] (no tracked intent) +-- fn 3 — (no annotation) → [] (also empty) +-- +-- The fourth function not appearing in the ownership section is +-- treated as unconstrained by the verifier; in `FunctionSummary` +-- terms it's the same shape as Unrestricted, just from a different +-- input path. Verifier verdict: clean on all four. + +||| `ModuleSummary` mirror of `cross_compat::fixture_realistic_clean_module`. +public export +fixtureRealisticCleanModule : ModuleSummary +fixtureRealisticCleanModule = MkModuleSummary "fixture_realistic_clean_module" + [ MkFunctionSummary "fn0_linear" [Consumes 0] + , MkFunctionSummary "fn1_excl_borrow" [BorrowsExclusive 0] + , MkFunctionSummary "fn2_unrestricted" [] + , MkFunctionSummary "fn3_unannotated" [] + ] + +||| Structural witness for the four-function realistic fixture. +public export +fixtureRealisticCleanWitness : + FunctionsAccepted VerifierSpec.fixtureRealisticCleanModule.functions +fixtureRealisticCleanWitness = + FACons (ILAConsumes TFNil ILANil) + (FACons (ILABorrowsExclusive ILANil) + (FACons ILANil + (FACons ILANil + FANil))) + +||| TrustedFixture for cross_compat row 10. +public export +fixtureRealisticCleanTrusted : + TrustedFixture VerifierSpec.fixtureRealisticCleanModule +fixtureRealisticCleanTrusted = MkTrustedFixture + "fixture_realistic_clean_module" + 10 + fixtureRealisticCleanWitness + +||| Projections. +public export +fixtureRealisticCleanSpecAccepts : + SpecAccepts VerifierSpec.fixtureRealisticCleanModule +fixtureRealisticCleanSpecAccepts = trustedToSpec fixtureRealisticCleanTrusted + +public export +fixtureRealisticCleanVerifierAccepts : + VerifierAccepts VerifierSpec.fixtureRealisticCleanModule +fixtureRealisticCleanVerifierAccepts = trustedToVerifier fixtureRealisticCleanTrusted + +public export +fixtureRealisticCleanSourceAccepts : + SourceAccepts VerifierSpec.fixtureRealisticCleanModule +fixtureRealisticCleanSourceAccepts = trustedToSource fixtureRealisticCleanTrusted + +-- ---------------------------------------------------------------------------- +-- Coverage note — rows 2-8 are out of scope at the summary level +-- ---------------------------------------------------------------------------- +-- +-- The remaining cross_compat fixtures land outside the modelling +-- envelope of `SpecAccepts`: +-- +-- Row 2 (fixture_duplicated_linear) +-- Intent list `[Consumes 0]` is L10-clean at the summary level. +-- The wasm body loads `local 0` twice; the Rust verifier catches +-- `LinearUsedMultiple` via body traversal which is not in +-- `SpecAccepts`. +-- Row 3 (fixture_dropped_linear_in_else) +-- Conditional branch leaves a linear param consumed on one path +-- but dropped on the other. Body-level path analysis; out of +-- scope. +-- Row 4 (fixture_aliased_excl_borrow) +-- ExclBorrow aliased in the body; body-level aliasing analysis; +-- out of scope. +-- Row 5 (fixture_multi_function_one_buggy) +-- Two-function module where fn 0 is clean and fn 1's body +-- violates LinearUsedMultiple. At the summary level both have +-- clean intent lists. +-- Rows 6 / 7 / 8 (xmod_*) +-- Cross-module fixtures; `verify_cross_module` rather than +-- `verify_from_module`. Modelling cross-module witnesses +-- requires extending `ModuleSummary` to carry import / export +-- edges, separate from this slice. +-- +-- These rows are the natural motivation for extending the spec — +-- adding a body-level predicate would make the differential evidence +-- structural for them too. Tracked as long-tail. + +-- ============================================================================ +-- DecEq machinery for ModuleSummary + dispatching fixtureLookup +-- ============================================================================ +-- +-- The A14 / A15 work above left one note as future work: +-- +-- "A fully discriminating `fixtureLookup` ... requires decidable +-- equality on ModuleSummary." +-- +-- This section closes that note. Three DecEq instances — +-- `OwnershipIntent`, `FunctionSummary`, `ModuleSummary` — plus a +-- dispatching `firstExtendedAgreement` that returns the right +-- TrustedFixture for the three registered fixture rows and Nothing +-- otherwise. Total functions throughout; no `believe_me` introduced +-- (the stdlib's `decEq` on String uses one internally, but that's +-- pre-existing stdlib content not new code in this module). + +||| `DecEq OwnershipIntent` — 16 cases (4 same-constructor compare- +||| payload + 12 different-constructor immediate-No). Mechanical. +public export +DecEq OwnershipIntent where + decEq (Consumes a) (Consumes b) = case decEq a b of + Yes Refl => Yes Refl + No neq => No (\Refl => neq Refl) + decEq (Produces a) (Produces b) = case decEq a b of + Yes Refl => Yes Refl + No neq => No (\Refl => neq Refl) + decEq (Borrows a) (Borrows b) = case decEq a b of + Yes Refl => Yes Refl + No neq => No (\Refl => neq Refl) + decEq (BorrowsExclusive a) (BorrowsExclusive b) = case decEq a b of + Yes Refl => Yes Refl + No neq => No (\Refl => neq Refl) + decEq (Consumes _) (Produces _) = No (\case Refl impossible) + decEq (Consumes _) (Borrows _) = No (\case Refl impossible) + decEq (Consumes _) (BorrowsExclusive _) = No (\case Refl impossible) + decEq (Produces _) (Consumes _) = No (\case Refl impossible) + decEq (Produces _) (Borrows _) = No (\case Refl impossible) + decEq (Produces _) (BorrowsExclusive _) = No (\case Refl impossible) + decEq (Borrows _) (Consumes _) = No (\case Refl impossible) + decEq (Borrows _) (Produces _) = No (\case Refl impossible) + decEq (Borrows _) (BorrowsExclusive _) = No (\case Refl impossible) + decEq (BorrowsExclusive _) (Consumes _) = No (\case Refl impossible) + decEq (BorrowsExclusive _) (Produces _) = No (\case Refl impossible) + decEq (BorrowsExclusive _) (Borrows _) = No (\case Refl impossible) + +||| Helper: injectivity of `MkFunctionSummary` on both fields. +funcSummaryInj : + MkFunctionSummary n1 i1 = MkFunctionSummary n2 i2 + -> (n1 = n2, i1 = i2) +funcSummaryInj Refl = (Refl, Refl) + +||| `DecEq FunctionSummary` — record-of-two compare; uses stdlib +||| `decEq` on `String` and on `List OwnershipIntent`. +public export +DecEq FunctionSummary where + decEq (MkFunctionSummary n1 i1) (MkFunctionSummary n2 i2) = + case decEq n1 n2 of + No neq => No (\eq => neq (fst (funcSummaryInj eq))) + Yes Refl => case decEq i1 i2 of + No neq => No (\eq => neq (snd (funcSummaryInj eq))) + Yes Refl => Yes Refl + +||| Helper: injectivity of `MkModuleSummary`. +modSummaryInj : + MkModuleSummary n1 fs1 = MkModuleSummary n2 fs2 + -> (n1 = n2, fs1 = fs2) +modSummaryInj Refl = (Refl, Refl) + +||| `DecEq ModuleSummary` — same shape as `FunctionSummary`. +public export +DecEq ModuleSummary where + decEq (MkModuleSummary n1 fs1) (MkModuleSummary n2 fs2) = + case decEq n1 n2 of + No neq => No (\eq => neq (fst (modSummaryInj eq))) + Yes Refl => case decEq fs1 fs2 of + No neq => No (\eq => neq (snd (modSummaryInj eq))) + Yes Refl => Yes Refl + +-- ---------------------------------------------------------------------------- +-- liftTrustedFixture — coerce a TrustedFixture across decEq evidence +-- ---------------------------------------------------------------------------- +-- +-- Once decEq gives us `prf : m = m'`, we want to convert a +-- `TrustedFixture m'` (the registered fixture) into a +-- `TrustedFixture m` (what the caller's lookup signature demands). +-- Direct pattern-match on `Refl` does the job — totally, no +-- `believe_me`. + +||| Transport a `TrustedFixture` along propositional equality of its +||| underlying `ModuleSummary` index. +public export +liftTrustedFixture : + {0 a, b : ModuleSummary} + -> a = b + -> TrustedFixture a + -> TrustedFixture b +liftTrustedFixture Refl x = x + +-- ---------------------------------------------------------------------------- +-- firstExtendedAgreement — dispatches on the three registered fixtures +-- ---------------------------------------------------------------------------- + +||| Dispatching fixture-lookup helper. Returns the registered +||| `TrustedFixture m` when `m` matches one of the three fixture +||| modules registered above; Nothing otherwise. Total, no +||| `believe_me`. +public export +fixtureLookupDispatching : + (m : ModuleSummary) + -> (fixtureName : String) + -> (fixtureId : Nat) + -> Maybe (TrustedFixture m) +fixtureLookupDispatching m _ _ = case decEq m fixtureCleanLinearConsumerModule of + Yes prf => Just (liftTrustedFixture (sym prf) fixtureCleanLinearConsumerTrusted) + No _ => case decEq m fixtureExtractExportsModule of + Yes prf => Just (liftTrustedFixture (sym prf) fixtureExtractExportsTrusted) + No _ => case decEq m fixtureRealisticCleanModule of + Yes prf => Just (liftTrustedFixture (sym prf) fixtureRealisticCleanTrusted) + No _ => Nothing + +||| `firstExtendedAgreement` — `StructuralAgreement` plus the +||| dispatching `fixtureLookupDispatching`. First non-empty +||| `ExtendedAgreement` in the codebase. Closes the future-work note +||| left by `emptyExtendedAgreement` at A14. +public export +firstExtendedAgreement : ExtendedAgreement +firstExtendedAgreement = MkExtendedAgreement + structuralAgreement + fixtureLookupDispatching + +-- Round-trip propositional equalities for `fixtureLookupDispatching` +-- (e.g. `fixtureLookupDispatching fixtureCleanLinearConsumerModule +-- "..." 1 = Just fixtureCleanLinearConsumerTrusted`) do not reduce to +-- `Refl` definitionally because `decEq` on records bottoms out in +-- `decEq` on `String` which doesn't unfold at type-check time. +-- The evidence-track below (`RegisteredFixture` GADT) sidesteps this +-- by dispatching on a constructor instead of decEq, giving us clean +-- `Refl` round-trips. + +-- ============================================================================ +-- Evidence-track dispatcher (A17) — GADT round-trips +-- ============================================================================ +-- +-- `RegisteredFixture m` is a GADT whose constructors enumerate every +-- module that has a registered `TrustedFixture`. Each constructor is +-- type-indexed by the matching module, so dispatching by pattern +-- match (rather than `decEq`) gives a *definitionally* equal result. +-- +-- This closes the round-trip future-work note left after the A16 +-- `decEq`-based dispatcher: round-trip equalities here are `Refl`. +-- +-- This GADT is closed-world by design: enlarging the registry means +-- adding a constructor here AND adding the `fixtureFromEvidence` +-- clause. Conversely, callers cannot manufacture a `RegisteredFixture +-- m` for an arbitrary `m` — the only way to produce one is via the +-- constructors below, so the inhabitants are exactly the audited +-- fixtures. + +public export +data RegisteredFixture : ModuleSummary -> Type where + RFCleanLinear : RegisteredFixture VerifierSpec.fixtureCleanLinearConsumerModule + RFExtractExports : RegisteredFixture VerifierSpec.fixtureExtractExportsModule + RFRealisticClean : RegisteredFixture VerifierSpec.fixtureRealisticCleanModule + +||| Produce a `TrustedFixture` from `RegisteredFixture` evidence. +||| Total; pattern match definitionally reduces, so the round-trips +||| below are `Refl`. +public export +fixtureFromEvidence : {0 m : ModuleSummary} -> RegisteredFixture m -> TrustedFixture m +fixtureFromEvidence RFCleanLinear = fixtureCleanLinearConsumerTrusted +fixtureFromEvidence RFExtractExports = fixtureExtractExportsTrusted +fixtureFromEvidence RFRealisticClean = fixtureRealisticCleanTrusted + +-- ---------------------------------------------------------------------------- +-- Projector round-trips — `Refl` via record-projector pattern match +-- ---------------------------------------------------------------------------- +-- +-- Round-trip-to-toplevel-name lemmas of the form +-- `fixtureFromEvidence RFCleanLinear = fixtureCleanLinearConsumerTrusted` +-- do NOT type-check as `Refl` in Idris2 0.8.0 — the reducer unfolds +-- the LHS (via pattern match on `RFCleanLinear`) past the toplevel +-- name into `MkTrustedFixture ...`, but treats the RHS toplevel name +-- as opaque, leaving the two sides at asymmetric reduction depths. +-- +-- Projector-based lemmas avoid this: each record projector forces +-- unfolding to the `MkTrustedFixture` constructor on both sides, so +-- the asymmetric-depth problem doesn't arise. The projector lemmas +-- below pin the name + id of each registered fixture as a `Refl` +-- equality at the projection level — sufficient for callers to +-- discriminate evidence by content without trusting the toplevel +-- name. + +public export +nameRow1 : + trustedFixtureName (fixtureFromEvidence RFCleanLinear) + = "fixture_clean_linear_consumer" +nameRow1 = Refl + +public export +idRow1 : + trustedFixtureId (fixtureFromEvidence RFCleanLinear) = 1 +idRow1 = Refl + +public export +nameRow9 : + trustedFixtureName (fixtureFromEvidence RFExtractExports) + = "fixture_extract_exports_three_shapes" +nameRow9 = Refl + +public export +idRow9 : + trustedFixtureId (fixtureFromEvidence RFExtractExports) = 9 +idRow9 = Refl + +public export +nameRow10 : + trustedFixtureName (fixtureFromEvidence RFRealisticClean) + = "fixture_realistic_clean_module" +nameRow10 = Refl + +public export +idRow10 : + trustedFixtureId (fixtureFromEvidence RFRealisticClean) = 10 +idRow10 = Refl + +-- ---------------------------------------------------------------------------- +-- Maybe-free constructive bridges (evidence-driven) +-- ---------------------------------------------------------------------------- + +||| Constructive `VerifierAccepts m -> SpecAccepts m` given evidence +||| that `m` is registered. No `Maybe`: registration *is* the +||| acceptance witness. +||| +||| Both branches of `VerifierAccepts` produce a structural witness: +||| * `VAStructural fa` — already structural, lift straight to spec. +||| * `VADifferential _ _` — discharge via the registered fixture. +public export +verifierImpliesSpecEvidence : + {0 m : ModuleSummary} + -> RegisteredFixture m + -> VerifierAccepts m + -> SpecAccepts m +verifierImpliesSpecEvidence _ (VAStructural fa) = MkSpecAccepts fa +verifierImpliesSpecEvidence rf (VADifferential _ _) = + trustedToSpec (fixtureFromEvidence rf) + +||| Symmetric constructive `SourceAccepts m -> SpecAccepts m`. +public export +sourceImpliesSpecEvidence : + {0 m : ModuleSummary} + -> RegisteredFixture m + -> SourceAccepts m + -> SpecAccepts m +sourceImpliesSpecEvidence _ (SAStructural fa) = MkSpecAccepts fa +sourceImpliesSpecEvidence rf (SADifferential _ _) = + trustedToSpec (fixtureFromEvidence rf) + diff --git a/src/abi/typed-wasm.ipkg b/src/abi/typed-wasm.ipkg index d94c7cf..25aa5cb 100644 --- a/src/abi/typed-wasm.ipkg +++ b/src/abi/typed-wasm.ipkg @@ -25,6 +25,7 @@ modules = TypedWasm.ABI.Region , TypedWasm.ABI.Epistemic , TypedWasm.ABI.Layout , TypedWasm.ABI.Proofs + , TypedWasm.ABI.VerifierSpec -- Cross-language layout contracts (aggregate library role, ADR-004). -- Restored 2026-04-18 after fixing the Idris2 0.8 reduction + parsing -- issues in `Layout/Types.idr` and siblings: added public export to diff --git a/tests/proof/regression.mjs b/tests/proof/regression.mjs index ed36b19..99d498e 100644 --- a/tests/proof/regression.mjs +++ b/tests/proof/regression.mjs @@ -18,11 +18,13 @@ // is what the Idris2 totality checker is for. // // Layer 2 (runs only when idris2 is on PATH) -// `idris2 --check src/abi/typed-wasm.ipkg` — actually typechecks the -// proof package. Catches the case where a theorem name still exists -// but its body no longer typechecks. This is the strong test; it -// requires an Idris2 toolchain at the version pinned in -// src/abi/typed-wasm.ipkg (currently 0.8.0). +// `idris2 --build src/abi/typed-wasm.ipkg` — actually typechecks + +// builds the proof package. Catches the case where a theorem name +// still exists but its body no longer typechecks. This is the strong +// test; it requires an Idris2 toolchain at the version pinned in +// src/abi/typed-wasm.ipkg (currently 0.8.0). `--build` is used +// instead of `--check` because the latter expects a single .idr +// source file and tries to parse the .ipkg as Idris syntax. // // Phase 0 / Track C deliverable. See: // - TEST-NEEDS.md "11 Idris2 proof modules with 0 proof verification tests" @@ -109,6 +111,23 @@ const EXPECTED = [ ["MultiModule.idr", /^LinkGraph\s*:/m, "Link graph type"], ["MultiModule.idr", /^schemaSubRefl\s*:/m, "Schema-subtype reflexivity"], ["MultiModule.idr", /^schemaSubTrans\s*:/m, "Schema-subtype transitivity"], + ["MultiModule.idr", /^compatCommute\s*:/m, "Compat commutativity (mutual subschema, A10)"], + ["MultiModule.idr", /^noSpoofingBidir\s*:/m, "Bidirectional no-spoofing (mutual subschema, A10)"], + + // Epistemic.idr — L12 freshness propagation (A10, 2026-05-26) + ["Epistemic.idr", /^writerKnowsFresh\s*:/m, "Writer-knows-fresh reflexivity"], + ["Epistemic.idr", /^freshOrStale\s*:/m, "Fresh/stale trichotomy"], + ["Epistemic.idr", /^syncRestoresFresh\s*:/m, "Sync restores freshness"], + ["Epistemic.idr", /^freshImpliesEqual\s*:/m, "Fresh -> known=current projector (A10)"], + ["Epistemic.idr", /^staleImpliesLT\s*:/m, "Stale -> known