Skip to content

Commit c2badda

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs+test: A14 catch-up — CHANGELOG / PROOF-NEEDS / LEVEL-STATUS / regression
Documentation reconciliation for the A14 work landed in commits 1d09ef6, 3678d64, and 5adea82 on this branch. CHANGELOG.md: new top-level "Proof-debt pass A14" section above the A13 entry, summarising the design pass (VerifierAccepts / SourceAccepts made inductive with structural + differential constructors), the first concrete structuralAgreement value, the four-OwnershipIntent allocFreeWithBorrowModule witness, the three discrimination proofs, and the ExtendedAgreement constructive bridge. Documents the ~30 new named items and that the open residual is now bounded (populate emptyExtendedAgreement's fixture registry). PROOF-NEEDS.md: new "RECONCILIATION 2026-05-26 (A14 follow-up — read this FIRST)" block above the A13 reconciliation, mirroring the CHANGELOG breakdown. The five-numbered-item structure narrates each of the design pass / structuralAgreement value / concrete inhabitants / discrimination proofs / ExtendedAgreement bridge in turn, and reframes the long-tail residual from "multi-week TODO" to "fixture- registry population, bounded". LEVEL-STATUS.md: VerifierSpec.idr row updated to reflect A14 additions — listing the constructor split, the six structural- direction agreement lemmas, the StructuralAgreement record + concrete value, the inhabitants (empty + alloc/free + four-constructor), the three discrimination proofs, and TrustedFixture / ExtendedAgreement / emptyExtendedAgreement / verifierImpliesSpecExtended / sourceImpliesSpecExtended. Phrasing: "structural sublattice of items 7+8 fully proven; differential case bounded". tests/proof/regression.mjs: 23 new regex assertions covering all the new named items. Layer 1 grep now reports 90 passed (up from 67). Layer 2 idris2 --build failure is pre-existing environment issue unrelated to this branch (asdf wrapper / base-library mismatch when idris2 is invoked without IDRIS2_PREFIX); same failure mode on b585068 baseline. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 5adea82 commit c2badda

4 files changed

Lines changed: 203 additions & 2 deletions

File tree

‎CHANGELOG.md‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,95 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
1010

1111
## [Unreleased]
1212

13+
### Proof-debt pass A14 (2026-05-26, same-day continuation; PR #74)
14+
15+
A13 (same-day, [#72](https://github.com/hyperpolymath/typed-wasm/pull/72))
16+
stated items 7 + 8 as typed obligations but kept the
17+
`VerifierAccepts` / `SourceAccepts` predicates **opaque** (single
18+
constructor carrying only an external-evidence string + fixture id).
19+
That made every agreement direction unprovable without external
20+
trust at every consumer site.
21+
22+
A14 ([#74](https://github.com/hyperpolymath/typed-wasm/pull/74))
23+
reshapes the predicates and lands the first **concrete, total,
24+
no-`believe_me`** agreement value in the codebase between spec /
25+
verifier / source-checker.
26+
27+
- **Design pass.** `VerifierAccepts` / `SourceAccepts` refactored to
28+
inductive types with two constructors each:
29+
- `VAStructural FunctionsAccepted` / `SAStructural FunctionsAccepted`
30+
— backed by the same structural predicate the spec uses. No
31+
trust-injection; introspectable in proofs.
32+
- `VADifferential String Nat` / `SADifferential String Nat` —
33+
external evidence pinned to a fixture row. Single audit point;
34+
grep these constructors to enumerate every trust-injection site.
35+
`SpecAccepts` refactored to wrap the new `FunctionsAccepted`
36+
predicate, so spec / verifier / source-checker now share one
37+
canonical structural witness shape at the L7+L10 layer.
38+
- **First concrete agreement value.** `structuralAgreement :
39+
StructuralAgreement` — total, no `believe_me`, no `postulate`, no
40+
external trust — closes the structural sublattice of items 7 + 8.
41+
Six new total functions:
42+
`functionsAcceptedImpliesSpec` / `specImpliesFunctionsAccepted`
43+
(round-trip), `specImpliesVerifierStructural` /
44+
`specImpliesSourceStructural` (total — uses the structural
45+
constructors directly), `verifierImpliesSpecStructural` /
46+
`sourceImpliesSpecStructural` (return `Maybe`; differential case is
47+
honestly `Nothing`).
48+
- **Concrete inhabitants.** `emptyFunctionsAccepted`,
49+
`emptyModuleSpecAccepts`, `emptyModuleVerifierAccepts`,
50+
`emptyModuleSourceAccepts` — show the predicates aren't vacuously
51+
empty. `allocFreeModule` + `allocFreeSpecAccepts` /
52+
`allocFreeVerifierAccepts` / `allocFreeSourceAccepts` — first
53+
non-empty witness, exercises `ILAProduces` / `ILAConsumes`.
54+
`allocFreeWithBorrowModule` extends to all four
55+
`OwnershipIntent` constructors with three witnesses each.
56+
- **Discrimination — predicate has teeth.** Three rejection paths,
57+
each exercising a distinct `TF*` / `ILA*` constructor combination:
58+
- `notSpecAcceptsBadDoubleConsume` — `[Consumes 0, Consumes 0]`
59+
rejected via `ILAConsumes` / `TFConsumesOther` / `Refl`.
60+
- `notSpecAcceptsBadDoubleProduce` — `[Produces 0, Produces 0]`
61+
rejected via `ILAProduces` / `TFProducesOther` / `Refl`.
62+
- `notSpecAcceptsBadConsumeProduceMix` — `[Consumes 0, Produces 0]`
63+
rejected via `ILAConsumes` / `TFProducesOther` / `Refl`.
64+
Plus `notVerifierStructuralAcceptsBadDoubleConsume` showing the
65+
structural verifier path is symmetric.
66+
- **ExtendedAgreement — constructive bridge for VADifferential.**
67+
`record TrustedFixture m` packages a fixture name + id with the
68+
structural witness it certifies; constructing one IS the
69+
trust-injection moment (auditable by grepping `MkTrustedFixture`).
70+
Projections `trustedToVerifier` / `trustedToSpec` /
71+
`trustedToSource` carry the witness into each acceptance predicate
72+
without further trust at use site. `record ExtendedAgreement`
73+
bundles `StructuralAgreement` with a fixture-lookup, and
74+
`emptyExtendedAgreement` is the concrete inhabitant with an empty
75+
registry. `verifierImpliesSpecExtended` /
76+
`sourceImpliesSpecExtended` are total `Maybe`-returning bridges:
77+
structural witnesses pass through; differential witnesses consult
78+
the fixture registry. Net effect: the multi-week
79+
`VerifierSpecAgreement` / `SourceVerifierAgreement` residual now
80+
has a concrete shape (fixture-registry population) rather than
81+
a "multi-week TODO".
82+
83+
**~30 new named items added** including `FunctionsAccepted`,
84+
`VAStructural` / `VADifferential`, `SAStructural` / `SADifferential`,
85+
six structural-agreement directions + `StructuralAgreement` record +
86+
concrete `structuralAgreement` value, four empty-module inhabitants,
87+
six alloc/free + borrow inhabitants, four discrimination proofs +
88+
their bad modules, `TrustedFixture` record + three projections,
89+
`ExtendedAgreement` record + concrete empty inhabitant + two
90+
extended-bridge functions. Regression: build green 22/22 modules
91+
under Idris2 0.8.0. Zero new `believe_me`, `assert_total`,
92+
`postulate`, `sorry`, `assert_smaller`. `%default total` preserved.
93+
94+
**Open after A14** — full proof bodies for `VerifierSpecAgreement` /
95+
`SourceVerifierAgreement` (now down to: populate
96+
`emptyExtendedAgreement`'s fixture registry from the actual
97+
differential harness, then close the unconditional direction).
98+
Other long-tail items (`LevelAttestation` reindexed-by-witness
99+
redesign; WasmCert-Isabelle tie-back; emitted-wasm byte-equality)
100+
unchanged.
101+
13102
### Proof-debt pass A13 (2026-05-26, same-day continuation)
14103

15104
Per coordinator pre-clearance for items 5 + 7 + 8, this round closes

‎LEVEL-STATUS.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@ toolchain remains future work.
105105
| Tropical.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) |
106106
| 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. |
107107
| Echo.idr | 0 | 0 | 0 | In package (A0, 2026-04-18) |
108-
| VerifierSpec.idr | 0 | 0 | 0 | New module A13 (2026-05-26). Spec-of-record for items 7+8 of the post-A10 audit at the statement level. Exposes the abstract `ModuleSummary` / `FunctionSummary` / `OwnershipIntent` shapes shared by the Rust verifier and the Idris2 spec; the structural L10 single-consumption predicate `IntentsLinearAcceptable` and its `TokenFresh` underpinning; the L7+L10 acceptance predicate `SpecAccepts m`; the opaque `VerifierAccepts m` / `SourceAccepts m` predicates (witnessed only by named fixture ids via `differentialAccepted` / `sourceAccepted` to keep the trust boundary inspectable); the two agreement records `VerifierSpecAgreement` (item 7) / `SourceVerifierAgreement` (item 8) each bundling soundness + completeness directions; and composition lemmas `sourceImpliesSpec` / `specImpliesSource` under both agreements. Statement-only — full proof bodies are multi-week long-tail. |
108+
| 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. 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. Structural sublattice of items 7+8 fully proven; differential case bounded to fixture-registry population. |
109109

110110
## Post-codegen verifier (Rust)
111111

‎PROOF-NEEDS.md‎

Lines changed: 88 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,94 @@ compile time" (true) and "here is a lemma proving it is forbidden"
2020
claims — a reviewer asking _"where is the theorem?"_ currently has no
2121
answer to point at.
2222

23-
## RECONCILIATION 2026-05-26 (A13 follow-up — read this FIRST)
23+
## RECONCILIATION 2026-05-26 (A14 follow-up — read this FIRST)
24+
25+
> **A14 follows A13 in the same calendar day** ([#74](https://github.com/hyperpolymath/typed-wasm/pull/74)).
26+
> A13 stated items 7 + 8 as typed obligations but kept the
27+
> `VerifierAccepts` / `SourceAccepts` predicates **opaque** (a single
28+
> constructor carrying only an external-evidence string + fixture
29+
> id), which made every agreement direction unprovable in Idris2.
30+
> A14 reshapes those predicates and lands the **first concrete,
31+
> total, no-`believe_me` agreement value in the codebase** between
32+
> spec / verifier / source-checker.
33+
>
34+
> 1. **Design pass — `VerifierAccepts` / `SourceAccepts` no longer
35+
> opaque.** Each refactored to two constructors: `VAStructural` /
36+
> `SAStructural` taking a `FunctionsAccepted` witness (the same
37+
> structural predicate the spec uses, fully introspectable) and
38+
> `VADifferential` / `SADifferential` carrying external-evidence
39+
> name + id (the trust-injection escape hatch, single audit
40+
> point). `SpecAccepts` is refactored to wrap `FunctionsAccepted`
41+
> too, so spec / verifier / source share one canonical structural
42+
> witness shape at L7+L10.
43+
>
44+
> 2. **First concrete agreement value.** `structuralAgreement :
45+
> StructuralAgreement` is total, no `believe_me`, no `postulate`,
46+
> no external trust. It closes the structural sublattice of items
47+
> 7 + 8 with six total agreement directions (`functionsAcceptedImpliesSpec`,
48+
> `specImpliesFunctionsAccepted`, `specImpliesVerifierStructural`,
49+
> `specImpliesSourceStructural`, `verifierImpliesSpecStructural`,
50+
> `sourceImpliesSpecStructural` — the latter two return `Maybe`
51+
> because the differential case has no structural information by
52+
> design).
53+
>
54+
> 3. **Concrete inhabitants.** `emptyFunctionsAccepted` plus three
55+
> empty-module variants (`emptyModuleSpecAccepts` /
56+
> `…VerifierAccepts` / `…SourceAccepts`) prove the predicates are
57+
> not vacuously empty. `allocFreeModule` plus spec / verifier /
58+
> source witnesses build the first non-empty case.
59+
> `allocFreeWithBorrowModule` extends to all four
60+
> `OwnershipIntent` constructors with three witnesses each.
61+
>
62+
> 4. **Discrimination — predicate has teeth.** Three rejection
63+
> proofs each exercise a distinct `TF*` / `ILA*` constructor
64+
> combination: `notSpecAcceptsBadDoubleConsume` rules out
65+
> `[Consumes 0, Consumes 0]`, `notSpecAcceptsBadDoubleProduce`
66+
> rules out `[Produces 0, Produces 0]`, and
67+
> `notSpecAcceptsBadConsumeProduceMix` rules out
68+
> `[Consumes 0, Produces 0]`. All discharged by the `Refl`
69+
> pattern against the `Not (0 = 0)` embedded in the relevant
70+
> `TF*` constructor. Plus
71+
> `notVerifierStructuralAcceptsBadDoubleConsume` for the
72+
> structural verifier path.
73+
>
74+
> 5. **ExtendedAgreement — constructive bridge for `VADifferential`.**
75+
> `record TrustedFixture m` pairs a fixture name + id with the
76+
> structural witness it certifies; constructing one IS the
77+
> trust-injection moment (auditable by grepping
78+
> `MkTrustedFixture`). Projections `trustedToVerifier` /
79+
> `trustedToSpec` / `trustedToSource` carry the witness into each
80+
> acceptance predicate. `record ExtendedAgreement` bundles
81+
> `StructuralAgreement` with a fixture-lookup, and
82+
> `emptyExtendedAgreement` is its concrete inhabitant.
83+
> `verifierImpliesSpecExtended` and `sourceImpliesSpecExtended`
84+
> are total `Maybe`-returning bridges: structural witnesses pass
85+
> through; differential witnesses consult the registry. Net
86+
> effect — the multi-week `VerifierSpecAgreement` /
87+
> `SourceVerifierAgreement` residual now has a concrete shape
88+
> (populate the registry from the actual differential harness)
89+
> rather than a "multi-week TODO".
90+
>
91+
> **~30 new named items** including `FunctionsAccepted`, four
92+
> `OwnershipIntent`-flavoured demo modules + witnesses, three
93+
> discrimination proofs + bad modules, `TrustedFixture`,
94+
> `ExtendedAgreement`, `structuralAgreement`,
95+
> `emptyExtendedAgreement`, and the agreement-direction
96+
> total functions. Build green 22/22 modules under Idris2 0.8.0.
97+
> Zero new `believe_me`, `assert_total`, `postulate`, `sorry`,
98+
> `assert_smaller`. `%default total` preserved.
99+
>
100+
> **Open after A14.** Full proof bodies for
101+
> `VerifierSpecAgreement` / `SourceVerifierAgreement` are now
102+
> bounded: populate `emptyExtendedAgreement`'s fixture registry
103+
> from the differential harness (one `MkTrustedFixture` per
104+
> audited fixture row), then close the unconditional direction
105+
> by case analysis. Other long-tail items
106+
> (`LevelAttestation` reindexed-by-witness redesign,
107+
> WasmCert-Isabelle tie-back, emitted-wasm byte-equality, parser
108+
> round-trip in Idris2) unchanged.
109+
110+
## RECONCILIATION 2026-05-26 (A13 follow-up)
24111

25112
> **A13 follows A12 in the same calendar day.** Per coordinator
26113
> pre-clearance for items 5 + 7 + 8 (and the small A12 leave-behind),

‎tests/proof/regression.mjs‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -175,6 +175,31 @@ const EXPECTED = [
175175
["VerifierSpec.idr", /^record\s+SourceVerifierAgreement/m, "Source↔verifier coverage obligation (A13, item 8)"],
176176
["VerifierSpec.idr", /^sourceImpliesSpec\s*:/m, "Source→spec composition under both agreements (A13)"],
177177
["VerifierSpec.idr", /^specImpliesSource\s*:/m, "Spec→source composition under both agreements (A13)"],
178+
179+
// VerifierSpec.idr — A14 design pass + concrete agreement witnesses
180+
["VerifierSpec.idr", /^data\s+FunctionsAccepted/m, "Shared structural walk over the function list (A14)"],
181+
["VerifierSpec.idr", /^record\s+StructuralAgreement/m, "Structural sublattice agreement record (A14)"],
182+
["VerifierSpec.idr", /^structuralAgreement\s*:/m, "Concrete structural agreement value, items 7+8 (A14)"],
183+
["VerifierSpec.idr", /^functionsAcceptedImpliesSpec\s*:/m, "FunctionsAccepted → SpecAccepts (A14)"],
184+
["VerifierSpec.idr", /^specImpliesFunctionsAccepted\s*:/m, "SpecAccepts → FunctionsAccepted (A14)"],
185+
["VerifierSpec.idr", /^specImpliesVerifierStructural\s*:/m, "Spec → verifier structural direction (A14)"],
186+
["VerifierSpec.idr", /^specImpliesSourceStructural\s*:/m, "Spec → source structural direction (A14)"],
187+
["VerifierSpec.idr", /^verifierImpliesSpecStructural\s*:/m, "Verifier → spec structural direction (A14, Maybe)"],
188+
["VerifierSpec.idr", /^sourceImpliesSpecStructural\s*:/m, "Source → spec structural direction (A14, Maybe)"],
189+
["VerifierSpec.idr", /^emptyModuleSpecAccepts\s*:/m, "Empty-module spec inhabitant (A14)"],
190+
["VerifierSpec.idr", /^allocFreeModule\s*:/m, "Concrete alloc/free demo module (A14)"],
191+
["VerifierSpec.idr", /^allocFreeSpecAccepts\s*:/m, "Non-empty spec acceptance witness (A14)"],
192+
["VerifierSpec.idr", /^allocFreeWithBorrowModule\s*:/m, "Four-constructor demo module (A14)"],
193+
["VerifierSpec.idr", /^allocFreeWithBorrowSpecAccepts\s*:/m, "Four-constructor spec witness (A14)"],
194+
["VerifierSpec.idr", /^badDoubleConsumeModule\s*:/m, "Bad-module case (double Consumes) (A14)"],
195+
["VerifierSpec.idr", /^notSpecAcceptsBadDoubleConsume\s*:/m, "L10 discrimination proof (Consumes/Consumes) (A14)"],
196+
["VerifierSpec.idr", /^notSpecAcceptsBadDoubleProduce\s*:/m, "L10 discrimination proof (Produces/Produces) (A14)"],
197+
["VerifierSpec.idr", /^notSpecAcceptsBadConsumeProduceMix\s*:/m, "L10 discrimination proof (Consumes/Produces mix) (A14)"],
198+
["VerifierSpec.idr", /^record\s+TrustedFixture/m, "Fixture-pinned structural witness packaging (A14)"],
199+
["VerifierSpec.idr", /^record\s+ExtendedAgreement/m, "Structural agreement + fixture lookup (A14)"],
200+
["VerifierSpec.idr", /^emptyExtendedAgreement\s*:/m, "Concrete empty-registry ExtendedAgreement (A14)"],
201+
["VerifierSpec.idr", /^verifierImpliesSpecExtended\s*:/m, "Constructive bridge from VADifferential to spec (A14)"],
202+
["VerifierSpec.idr", /^sourceImpliesSpecExtended\s*:/m, "Constructive bridge from SADifferential to spec (A14)"],
178203
];
179204

180205
// ----------------------------------------------------------------------

0 commit comments

Comments
 (0)