Skip to content

Commit dfe3c0d

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
proof(verifier-spec): ADR-0005 — MkTrustedFixture audit boundary (closes #103)
PR #79 landed total bodies for VerifierSpecAgreement / SourceVerifierAgreement. Issue #103 named the residual: the trust-injection moment (every VADifferential / SADifferential step ultimately routes through `MkTrustedFixture`) needed a load-bearing home, not an inline docstring. Three closure paths were offered; this PR takes path (3): an ADR pinning the audit boundary. Changes: * `docs/decisions/0005-trustedfixture-audit-boundary.adoc` — new ADR (Status: Accepted) pinning three inspection invariants every `MkTrustedFixture m` construction site is audited against: I1 Provenance — (name, id) matches a row in `crates/typed-wasm-verify/tests/cross_compat.rs` I2 Witness fidelity — `trustedWitness : FunctionsAccepted` is the structural witness the harness's ACCEPT verdict establishes; rejected fixtures yield no MkTrustedFixture I3 Module shape — `ModuleSummary` mirrors the harness's reconstruction (function order + decoded ownership intents) Also names the supersession path: WasmCert-Isabelle tie-back or constructive Rust-verifier soundness would each ship as a fresh ADR superseding 0005 by collapsing the audit boundary into a constructive proof. * `docs/decisions/README.adoc` — index row for ADR-0005 + 1-line owner-line header normalisation (hook compliance). * `src/abi/TypedWasm/ABI/VerifierSpec.idr` — 6-line docstring addition near `MkTrustedFixture` cross-referencing ADR-0005 so a reader landing on the record's definition can find the invariants without rediscovering them. Single grep point for trust injections preserved: `git grep MkTrustedFixture`. Same 1-line owner-line normalisation as PR #152's Epistemic.idr (incidental hook compliance — parenthetical removal only; no licence change, no SPDX change; owner-approved via AskUserQuestion mid-session). * `PROOF-NEEDS.md` — new `RECONCILIATION 2026-06-02` banner recording the closure with the I1/I2/I3 summary and the supersession note. Matches the convention of the prior `RECONCILIATION 2026-05-27 (post-A10 items 7 + 8 bodies closed)` banner. Same 3-line owner-line header normalisation already landed on PR #153's branch (incidental hook compliance). Verification: * `src/abi/TypedWasm/ABI/VerifierSpec.idr` — type-checks rc=0 in isolation (`idris2 --check`). The 6-line docstring edit changes no types and no terms. * Whole-package build (`idris2 --build typed-wasm.ipkg`) requires PR #152's fix to `composeWitnessLegacyAgree` in `TypedWasm/ABI/Proofs.idr`. This PR stacks on `proof/epistemic-fresh-pin-102` (#152's branch) so the package build returns to 22/22 on the stacked head. No `believe_me`, `assert_total`, `postulate`, `sorry`, or `assert_smaller` introduced. `%default total` preserved. No soundness-relevant escape hatch in the code paths this PR touches. Closes #103. Refs #79 (statement-level landing of agreement records). Refs #74 (superseded alternative design — `RegisteredFixture` GADT). Refs #102, #152, #153 (companion proof work in flight). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 584cba6 commit dfe3c0d

4 files changed

Lines changed: 351 additions & 2 deletions

File tree

‎PROOF-NEEDS.md‎

Lines changed: 53 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,8 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0
3+
Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
-->
15
# PROOF-NEEDS.md
2-
<!-- SPDX-License-Identifier: MPL-2.0 -->
36

47
**Scope:** handoff document for the Claude instance that will deepen
58
typed-wasm's formal verification. Read this file in full before
@@ -20,6 +23,55 @@ compile time" (true) and "here is a lemma proving it is forbidden"
2023
claims — a reviewer asking _"where is the theorem?"_ currently has no
2124
answer to point at.
2225

26+
## RECONCILIATION 2026-06-02 (audit-boundary half of post-A10 items 7 + 8 promoted to ADR-0005 — read this FIRST)
27+
28+
> **The "Full proof bodies for `VerifierSpecAgreement` /
29+
> `SourceVerifierAgreement`" long-tail item (issue #103) is now
30+
> closed via path (3) — explicit ADR.**
31+
>
32+
> The 2026-05-27 banner below recorded the bodies as TOTAL in PR #79
33+
> (commit `06ec00e`). What remained per issue #103 was a load-bearing
34+
> home for the audit-boundary story: every `VADifferential` /
35+
> `SADifferential` step ultimately routes through a
36+
> `MkTrustedFixture` construction, and the trust-injection moment
37+
> needed a single, named, cross-referenced specification rather than
38+
> an inline docstring.
39+
>
40+
> **ADR-0005**
41+
> (`docs/decisions/0005-trustedfixture-audit-boundary.adoc`,
42+
> 2026-06-02) pins three inspection invariants every
43+
> `MkTrustedFixture m` construction site is audited against:
44+
>
45+
> * **I1 — Provenance.** The pair `(trustedFixtureName,
46+
> trustedFixtureId)` must correspond to an existing row in the
47+
> Rust differential harness
48+
> (`crates/typed-wasm-verify/tests/cross_compat.rs`).
49+
> * **I2 — Witness fidelity.** The `FunctionsAccepted m.functions`
50+
> payload must be the structural witness the harness's ACCEPT
51+
> verdict establishes; rejected fixtures yield no `MkTrustedFixture`.
52+
> * **I3 — Module shape.** The indexing `ModuleSummary` must mirror
53+
> the harness's `ModuleSummary` reconstruction for the same
54+
> fixture bytes (function order + decoded ownership intents).
55+
>
56+
> **What this is not.** ADR-0005 is not a constructive proof of
57+
> Rust-verifier soundness; the Rust verifier remains the trusted
58+
> base for the differential path. The two supersession paths from
59+
> issue #103 — WasmCert-Isabelle tie-back (path 1) or constructive
60+
> Rust-verifier soundness (path 2) — remain valid future upgrades
61+
> and would each ship as a fresh ADR superseding 0005.
62+
>
63+
> **Source-code cross-reference.** A docstring near `MkTrustedFixture`
64+
> in `src/abi/TypedWasm/ABI/VerifierSpec.idr` points at ADR-0005, so
65+
> a reader landing on the record's definition can find the
66+
> invariants without rediscovering them. Single grep point for
67+
> trust injections: `git grep MkTrustedFixture`.
68+
>
69+
> **No `believe_me` / `assert_total` / `postulate` / `sorry` /
70+
> `assert_smaller` introduced; `%default total` preserved across
71+
> the arc. The closure work was an ADR + a docstring cross-reference
72+
> + a proof-debt banner — no new proof obligations, no new code
73+
> behind the lemma bodies that PR #79 already shipped.**
74+
2375
## RECONCILIATION 2026-05-30 (carrier-ABI proposals 0001 + 0002 accepted + ADR'd — read this FIRST)
2476

2577
> **The "verifier L1-L6 + L13-L16 coverage on emitted wasm" long-tail

‎docs/decisions/0005-trustedfixture-audit-boundary.adoc‎

Lines changed: 285 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,285 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
= Architecture Decision Record: 0005-trustedfixture-audit-boundary
4+
<!-- SPDX-License-Identifier: MPL-2.0 -->
5+
<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
6+
7+
# 5. `MkTrustedFixture` is the formal audit boundary for the `VerifierAccepts` / `SourceAccepts` predicates
8+
9+
Date: 2026-06-02
10+
11+
## Status
12+
13+
Accepted
14+
15+
Closes
16+
https://github.com/hyperpolymath/typed-wasm/issues/103[issue #103].
17+
Promotes the audit-boundary half of PR #79's design (commit `06ec00e`
18+
on `main`) from an inline comment in
19+
link:../../src/abi/TypedWasm/ABI/VerifierSpec.idr[`VerifierSpec.idr`]
20+
to a load-bearing architecture decision.
21+
22+
## Context
23+
24+
PR #79 landed TOTAL bodies (`%default total`; no `believe_me`, no
25+
`assert_total`, no `postulate`, no `sorry`, no `Admitted`) for both
26+
post-A10 audit obligations:
27+
28+
* `verifierSpecAgreement : VerifierSpecAgreement` — bundles
29+
`verifierIsSound` (verifier ⇒ spec) and `verifierIsComplete`
30+
(spec ⇒ verifier).
31+
* `sourceVerifierAgreement : SourceVerifierAgreement` — bundles
32+
`sourceImpliesVerifier` and `verifierImpliesSource`.
33+
34+
The lemma bodies are total by case analysis on the constructor of the
35+
input. Both `VerifierAccepts m` constructors — `VAStructural` and
36+
`VADifferential` — surface a `FunctionsAccepted m.functions` payload
37+
that wraps directly into `SpecAccepts`. `SourceAccepts m` mirrors the
38+
shape. The composition lemmas (`sourceImpliesSpec` / `specImpliesSource`)
39+
inherit totality.
40+
41+
What did NOT change in PR #79: the differential constructors
42+
(`VADifferential`, `SADifferential`) still ultimately depend on a
43+
non-Idris-proven step — the Rust differential harness's
44+
accept-verdict. PR #79's design choice was to **package** that
45+
attestation inline, via the `TrustedFixture m` record:
46+
47+
[source,idris2]
48+
----
49+
record TrustedFixture (m : ModuleSummary) where
50+
constructor MkTrustedFixture
51+
trustedFixtureName : String
52+
trustedFixtureId : Nat
53+
trustedWitness : FunctionsAccepted m.functions
54+
----
55+
56+
The structural witness `trustedWitness` is **required** at construction
57+
time. Once a `MkTrustedFixture` value exists, every downstream consumer
58+
operates on a structural Idris2 proof; no further trust is injected
59+
anywhere in the chain. The trust-injection moment is therefore exactly
60+
the act of writing `MkTrustedFixture` in source.
61+
62+
Issue #103 framed the residual obligation:
63+
64+
> Closing this issue means **either** discharging those bodies to
65+
> constructive proofs **or** documenting the trust-injection moment
66+
> formally (single grep point: `MkTrustedFixture` construction).
67+
68+
and listed three closure paths:
69+
70+
. WasmCert-Isabelle tie-back for the Rust-verifier soundness step.
71+
. A constructive proof of the Rust verifier's soundness, in-tree.
72+
. An explicit ADR documenting `MkTrustedFixture` as the audit
73+
boundary.
74+
75+
Paths (1) and (2) are both multi-month external/upstream commitments.
76+
Path (3) is the same audit story PR #79 already implemented as a
77+
docstring; promoting it to an ADR gives the inspection invariants a
78+
load-bearing home and a stable cross-reference target for the proof
79+
code and the proof-debt documents.
80+
81+
## Decision
82+
83+
Adopt `MkTrustedFixture` as the **formal, single, named audit
84+
boundary** for the `VerifierAccepts` / `SourceAccepts` predicates in
85+
link:../../src/abi/TypedWasm/ABI/VerifierSpec.idr[`VerifierSpec.idr`].
86+
87+
### What this means concretely
88+
89+
. The audit-boundary statement is normative: every `VerifierAccepts m`
90+
or `SourceAccepts m` value whose history includes a
91+
`VADifferential` / `SADifferential` step **must** route through a
92+
`MkTrustedFixture` construction. The smart constructors
93+
`differentialAccepted` and `sourceAccepted` enforce this at the
94+
type level (both take a `FunctionsAccepted m.functions` argument
95+
and wrap it into a `MkTrustedFixture` inside the differential
96+
constructor — there is no other surface for differential
97+
acceptance).
98+
. `MkTrustedFixture` is the **single grep point**: a complete
99+
enumeration of trust injections is `git grep MkTrustedFixture` in
100+
the proof code (and its companion in the test/wiring code if a
101+
fixture-table module is added in future work).
102+
. The inspection invariants below (§Inspection invariants) define what
103+
reviewers verify at each `MkTrustedFixture` call site. These
104+
invariants are the spec the ADR pins; they replace the implicit
105+
"trust the harness" reading.
106+
. The closure paths (1) and (2) from issue #103 remain valid future
107+
upgrades. This ADR does NOT preclude them: an Isabelle tie-back or
108+
a constructive verifier-soundness proof would **subsume** the
109+
audit boundary by allowing every `VAStructural`/`SAStructural`
110+
construction to absorb what `VADifferential`/`SADifferential`
111+
currently delegate. Either upgrade would supersede this ADR.
112+
113+
### Inspection invariants
114+
115+
Every `MkTrustedFixture m` construction site is audited against the
116+
following three invariants. Inspection is the load-bearing step the
117+
ADR formalises.
118+
119+
[discrete]
120+
==== I1. Provenance — fixture identity matches a harness row
121+
122+
The pair `(trustedFixtureName, trustedFixtureId)` MUST correspond to
123+
an existing row in the Rust differential harness
124+
(link:../../crates/typed-wasm-verify/tests/cross_compat.rs[`crates/typed-wasm-verify/tests/cross_compat.rs`]).
125+
126+
* `trustedFixtureName` MUST equal the harness fixture's name as it
127+
appears in the `cross_compat` test table.
128+
* `trustedFixtureId` MUST equal the harness row's numeric id (the row
129+
index used by the cross-compat report).
130+
131+
Worked example (PR #79 commit `06ec00e`):
132+
133+
[source,idris2]
134+
----
135+
fixtureCleanLinearConsumerTrusted = MkTrustedFixture
136+
"fixture_clean_linear_consumer" -- name matches harness fixture
137+
1 -- id matches harness row 1
138+
fixtureCleanLinearConsumerWitness -- structural witness — see I2
139+
----
140+
141+
[discrete]
142+
==== I2. Witness fidelity — `trustedWitness` matches the harness's verdict
143+
144+
The `FunctionsAccepted m.functions` payload passed as `trustedWitness`
145+
MUST be the structural witness the harness's ACCEPT verdict
146+
establishes — i.e., the L7+L10 structural acceptance predicate over
147+
`m.functions`. In particular:
148+
149+
* If the harness REJECTS the fixture, no `MkTrustedFixture` may be
150+
constructed for that fixture. (The reviewer should flag any such
151+
attempt; the type system already rules out fabricating a
152+
`FunctionsAccepted` for a fixture that lacks one — see the
153+
`notVerifierStructuralAcceptsBadDoubleConsume` family in
154+
`VerifierSpec.idr` for the negative side.)
155+
* If the harness ACCEPTS the fixture but for a strictly weaker
156+
property than `IntentsLinearAcceptable` (e.g., a partial decode
157+
pass), no `MkTrustedFixture` may be constructed at the full
158+
`FunctionsAccepted` strength. Add a strictly-weaker predicate
159+
instead, in a separate, audited follow-up.
160+
161+
[discrete]
162+
==== I3. Module shape — `ModuleSummary` mirrors the harness's view
163+
164+
The `ModuleSummary` value indexing the `TrustedFixture` MUST mirror
165+
the Rust harness's `ModuleSummary` reconstruction for the same
166+
fixture bytes:
167+
168+
* Function order MUST match the harness's iteration order over the
169+
module's exports.
170+
* `OwnershipIntent` list per function MUST match the harness's
171+
decoded `typedwasm.ownership` carrier section (or its absence —
172+
see the cross-references below).
173+
174+
A mismatch between the Idris2 `ModuleSummary` and the harness's
175+
decoded view is a fixture-wiring bug, not a soundness bug, but it
176+
voids `I2` and therefore voids the `MkTrustedFixture`.
177+
178+
### What this does NOT do
179+
180+
* It does not constitute a constructive proof of Rust-verifier
181+
soundness. The Rust verifier remains the trusted base for the
182+
differential path; the ADR pins the audit story for that trust,
183+
not its discharge.
184+
* It does not change the Idris2 source. The audit-boundary docstring
185+
PR #79 placed near `MkTrustedFixture` already states the same
186+
invariants in narrative form; this ADR is the load-bearing,
187+
cross-referenced version of that statement.
188+
* It does not gate the structural path. `VAStructural` and
189+
`SAStructural` continue to inject zero trust — they only require a
190+
pure Idris2 `FunctionsAccepted m.functions` value. The
191+
`verifierIsComplete` direction (spec ⇒ verifier) routes through
192+
`VAStructural` and therefore is trust-free in both PR #79 and this
193+
ADR.
194+
195+
## Consequences
196+
197+
### Positive
198+
199+
* **Single grep point** — `MkTrustedFixture` is the unique
200+
trust-injection name. `git grep MkTrustedFixture` enumerates every
201+
audit-relevant call site, in proof code and test wiring alike.
202+
* **Total Idris2 chain preserved** — the audit boundary does not add
203+
any escape hatch (no `believe_me`, no `assert_total`, no `postulate`,
204+
no `sorry`, no `Admitted`); the trust budget lives in a record
205+
constructor, not in a soundness lemma.
206+
* **Stable cross-reference for proof-debt docs** — `PROOF-NEEDS.md`
207+
and `docs/proof-debt.md` can now point at ADR-0005 instead of
208+
re-stating the invariants inline.
209+
* **Explicit subsumption path** — a future WasmCert-Isabelle
210+
tie-back or constructive verifier-soundness proof has a named
211+
ADR to supersede, not an inline docstring to argue with.
212+
* **Audit checklist for reviewers** — the I1/I2/I3 invariants give
213+
PR reviewers a concrete, three-bullet checklist for any new
214+
`MkTrustedFixture` site.
215+
216+
### Negative
217+
218+
* **Trust is real and named** — the ADR makes explicit that the Rust
219+
verifier (and the source-side harness) remain the trusted base for
220+
the differential path. Anyone reading `verifierSpecAgreement.idr`
221+
as "no trust anywhere" is wrong; the audit boundary moved to
222+
`MkTrustedFixture`, it did not disappear.
223+
* **Per-fixture review burden** — adding a fixture means a manual
224+
invariant check against the harness; the ADR does not automate
225+
this. (A future CI script that grep-cross-references
226+
`MkTrustedFixture` against `cross_compat.rs` fixture names is a
227+
cheap follow-up.)
228+
229+
### Neutral
230+
231+
* The ADR does not change any Idris2 type. PR #79's record shape
232+
remains canonical.
233+
* The smart constructors `differentialAccepted` / `sourceAccepted`
234+
continue to be the recommended surface for constructing a
235+
fixture-backed acceptance witness; they are documented as the
236+
pre-`MkTrustedFixture` ergonomic wrapper.
237+
238+
## Future work — when this ADR is superseded
239+
240+
The two paths that would supersede this ADR by collapsing the audit
241+
boundary into a constructive proof:
242+
243+
. **WasmCert-Isabelle tie-back** — port the Rust verifier's
244+
acceptance criterion to the WasmCert-Isabelle development and
245+
prove it sound against the WebAssembly spec's typing rules. The
246+
Idris2 side would then receive the Isabelle theorem as an external
247+
trust commit (the trusted base shifts to WasmCert-Isabelle), and
248+
`VADifferential` could be replaced with a constructor that
249+
carries the Isabelle theorem instead of a fixture row.
250+
. **Constructive Rust-verifier soundness** — prove the Rust verifier
251+
sound in a system (Rust + Creusot, Lean, Coq, or Idris2) that can
252+
be checked in the same CI run. The Idris2 side would then receive
253+
the verifier-soundness theorem and absorb the differential
254+
constructor into `VAStructural`.
255+
256+
Either upgrade would land its own ADR that supersedes this one. Until
257+
then, the audit boundary is `MkTrustedFixture` and the inspection
258+
invariants are I1/I2/I3.
259+
260+
## Cross-references
261+
262+
* link:../../src/abi/TypedWasm/ABI/VerifierSpec.idr[`src/abi/TypedWasm/ABI/VerifierSpec.idr`]
263+
— the proof code this ADR pins. PR #79 / commit `06ec00e`.
264+
* link:../../crates/typed-wasm-verify/tests/cross_compat.rs[`crates/typed-wasm-verify/tests/cross_compat.rs`]
265+
— the Rust differential harness. Fixture names and row ids in I1
266+
refer to entries in this file.
267+
* link:../../PROOF-NEEDS.md[`PROOF-NEEDS.md`] — proof-debt handoff.
268+
Long-tail item "Full proof bodies for `VerifierSpecAgreement` /
269+
`SourceVerifierAgreement`" is closed via this ADR (audit-boundary
270+
path). Cross-references back to ADR-0005 from the post-A10 / A13
271+
RECONCILIATION banner.
272+
* https://github.com/hyperpolymath/typed-wasm/issues/103[issue #103] —
273+
this ADR closes #103.
274+
* https://github.com/hyperpolymath/typed-wasm/pull/79[PR #79] — landed
275+
the statement-level records and TOTAL bodies; this ADR formalises
276+
the audit-boundary half of that PR's design.
277+
* https://github.com/hyperpolymath/typed-wasm/pull/74[PR #74] — the
278+
superseded alternative design (Maybe-returning bridges + closed-world
279+
`RegisteredFixture` GADT). PR #79 picked the inline-witness shape
280+
this ADR pins; the `RegisteredFixture` machinery remains available
281+
as a composable add-on if a fixture-table module is added in
282+
future work.
283+
* link:../../PROOF-NEEDS.md[`PROOF-NEEDS.md` RECONCILIATION 2026-05-27
284+
(post-A10 items 7 + 8 bodies closed)] — the prior reconciliation
285+
banner whose audit-boundary claim this ADR backs.

‎docs/decisions/README.adoc‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
23
= Architecture Decision Records (ADRs)
34

45
Accepted decisions that shape typed-wasm's architecture. Proposals
@@ -30,6 +31,11 @@ proposals still under discussion live in link:../proposals/[`docs/proposals/`].
3031
| Classify maa-framework's `absolute-zero/` as a stale vendor copy (sibling-estate)
3132
| 2026-05-30
3233
| Accepted
34+
35+
| link:0005-trustedfixture-audit-boundary.adoc[0005]
36+
| `MkTrustedFixture` is the formal audit boundary for `VerifierAccepts` / `SourceAccepts`
37+
| 2026-06-02
38+
| Accepted
3339
|===
3440

3541
== Authoring an ADR

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

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
-- SPDX-License-Identifier: MPL-2.0
2-
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
2+
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
33
--
44
-- VerifierSpec.idr — Spec-of-record for the post-codegen Rust verifier
55
-- and the source-side checker, with TOTAL bodies for both agreement
@@ -153,6 +153,12 @@ data FunctionsAccepted : List FunctionSummary -> Type where
153153
||| id) with the structural witness the fixture is claimed to certify.
154154
||| Constructing one is the trust-injection moment. Search for
155155
||| `MkTrustedFixture` to enumerate every fixture trust-injection.
156+
|||
157+
||| The audit boundary, the I1/I2/I3 inspection invariants every
158+
||| construction site is audited against, and the supersession path
159+
||| (WasmCert-Isabelle tie-back or constructive Rust-verifier
160+
||| soundness) are pinned by ADR-0005
161+
||| (`docs/decisions/0005-trustedfixture-audit-boundary.adoc`).
156162
public export
157163
record TrustedFixture (m : ModuleSummary) where
158164
constructor MkTrustedFixture

0 commit comments

Comments
 (0)