Skip to content

Commit a1b205e

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
proof(p3.2): A16 — typed ProgressiveCheckW + progressive-order monotonicity
PROOF-NEEDS §P3.2 (A8) reframed the level-monotonicity claim under the operational (untyped) `ProgressiveCheck`, leaving the stronger "progressive-order" claim — achieving level N implies levels 1..N were all visited — explicitly deferred: > the stronger "progressive-order" claim requires redesigning > `ProgressiveCheck` with a typed `level = S prevLevel` index and > is left as future work. A16 closes that deferred half. What lands in src/abi/TypedWasm/ABI/Proofs.idr (~150 LOC appended, no existing definition touched): * `ProgressiveCheckW : (highestLevel : Nat) -> Type` — typed chain built on top of the standards#130 `LevelAttestationW` family (already in tree). Constructors enforce that each attestation attest the exact level it sits at: StartL1W : LevelAttestationW 1 -> ProgressiveCheckW 1 AdvanceW : (n : Nat) -> ProgressiveCheckW n -> LevelAttestationW (S n) -> ProgressiveCheckW (S n) Skipping levels (advancing L1 → L5 in one step) and out-of-order attestations (attaching `AttestL3W` to a `ProgressiveCheckW 5`) are now type errors — they cannot construct. * `VisitedAt : (m : Nat) -> ProgressiveCheckW n -> Type` — sub- derivation witness with three constructors (StartW / HeadW / TailW shift). * `lteSuccCases : {m, n : Nat} -> LTE m (S n) -> Either (m = S n) (LTE m n)` — decidable case-split helper used by the recursion. * `progressiveOrderW : (check : ProgressiveCheckW n) -> (m : Nat) -> LT 0 m -> LTE m n -> VisitedAt m check` — the progressive-order theorem. By induction on the check and one LTE branch at each `AdvanceW` layer. Total. * `chainAlwaysVisitsL1` — specialised corollary for the common "L1 is the entry point" guarantee. * `forgetProgressiveCheckW : ProgressiveCheckW n -> ProgressiveCheck` — index-erasing bridge to the legacy untyped chain, so downstream consumers can still feed `buildCertificate` via the typed API. What lands in PROOF-NEEDS.md: * New `RECONCILIATION 2026-06-03 (A16 — P3.2 progressive-order half closed)` banner at the top. * §P3.2 itself now records the closure with the typed-chain signature, the bridge, and the "Purely additive" / "Zero escape hatches" disclaimers. * 3-line owner-line header normalisation (incidental hook compliance — same micro-pattern as PR #153 / #155). Purely additive arc. The legacy `ProgressiveCheck`, `LevelAchievedIn`, `composeAchievedL/R`, and the entire `buildCertificate` pipeline are untouched. No external caller of `ProgressiveCheck` / `StartL1` / `Advance` exists in src/ / examples/ / tests/ (grep-verified before landing), so the additivity preserves the typed-wasm public surface. Verification: * Whole-package build rc=0, 22/22 modules, 0 errors (only pre- existing shadowing warnings in unrelated modules — Epistemic, Tropical, Choreography). * `idris2 --check src/abi/TypedWasm/ABI/Proofs.idr` clean. No `believe_me`, `assert_total`, `postulate`, `sorry`, `Admitted`, or `assert_smaller` introduced. `%default total` preserved across the arc. Stacks on `proof/epistemic-fresh-pin-102` (#152) — same reason as PR #155 (the HEAD build break PR #152 fixes is required for the package build to pass). Refs PROOF-NEEDS §P3.2 (the deferred half). Refs #102, #152, #153, #155 (companion proof work in flight). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent aa7ee25 commit a1b205e

2 files changed

Lines changed: 262 additions & 7 deletions

File tree

‎PROOF-NEEDS.md‎

Lines changed: 115 additions & 7 deletions
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,71 @@ 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-03 (A16 — P3.2 progressive-order half closed — read this FIRST)
27+
28+
> **The deferred half of PROOF-NEEDS §P3.2 — progressive-order
29+
> monotonicity under a typed `ProgressiveCheck` — is now closed.**
30+
>
31+
> The 2026-04-18 (A8) banner below recorded the composition-form of
32+
> level monotonicity (`achievedAppendL` / `achievedAppendR` /
33+
> `composeAchievedL` / `composeAchievedR`) and explicitly deferred
34+
> the stronger "progressive-order" claim with the note:
35+
>
36+
> > the stronger "progressive-order" claim requires redesigning
37+
> > `ProgressiveCheck` with a typed `level = S prevLevel` index and
38+
> > is left as future work.
39+
>
40+
> A16 lands that redesign as a purely additive `ProgressiveCheckW`
41+
> alongside the legacy `ProgressiveCheck`, built on top of the
42+
> standards#130 `LevelAttestationW` family (already in tree):
43+
>
44+
> data ProgressiveCheckW : (highestLevel : Nat) -> Type where
45+
> StartL1W : LevelAttestationW 1 -> ProgressiveCheckW 1
46+
> AdvanceW : (n : Nat)
47+
> -> ProgressiveCheckW n
48+
> -> LevelAttestationW (S n)
49+
> -> ProgressiveCheckW (S n)
50+
>
51+
> Skipping levels (advancing L1 → L5 in one step) and out-of-order
52+
> attestations are now type errors — they cannot construct.
53+
>
54+
> **The progressive-order theorem** is constructive:
55+
>
56+
> progressiveOrderW : (check : ProgressiveCheckW n)
57+
> -> (m : Nat) -> LT 0 m -> LTE m n
58+
> -> VisitedAt m check
59+
>
60+
> Plus a specialised corollary `chainAlwaysVisitsL1` (every
61+
> non-trivial chain visits L1) and an index-erasing bridge
62+
> `forgetProgressiveCheckW : ProgressiveCheckW n -> ProgressiveCheck`
63+
> for downstream consumers still wanting to feed the legacy
64+
> `buildCertificate` pipeline.
65+
>
66+
> **Module: `src/abi/TypedWasm/ABI/Proofs.idr` §A16 (~150 LOC
67+
> appended).** Zero `believe_me` / `assert_total` / `postulate` /
68+
> `sorry` / `Admitted`; `%default total` preserved. Build verified
69+
> 22/22 modules, rc=0, only pre-existing shadowing warnings. Legacy
70+
> `ProgressiveCheck`, `LevelAchievedIn`, `composeAchievedL/R`, and
71+
> the entire `buildCertificate` pipeline are untouched.
72+
>
73+
> **What remains open in the long-tail** (post-A16): same as
74+
> 2026-05-30 banner below — producer-side-gated parser/emitter
75+
> items, WasmCert-Isabelle tie-back, L13/L15-C carrier proposals,
76+
> emitted-wasm byte-equality (P3.1(a)). No purely-Idris2-proof
77+
> residual obligation visible in PROOF-NEEDS.md is currently
78+
> tractable without owner direction or external dependency.
79+
80+
## RECONCILIATION 2026-06-02 (audit-boundary half of post-A10 items 7 + 8 promoted to ADR-0005 — read this FIRST)
81+
82+
> **PR #155** — the audit-boundary half of post-A10 items 7 + 8
83+
> (PROOF-NEEDS §VerifierSpec) is now closed via ADR-0005. See the
84+
> 2026-05-27 (post-A10 items 7 + 8 bodies closed) banner below for
85+
> the bodies; ADR-0005 is at
86+
> `docs/decisions/0005-trustedfixture-audit-boundary.adoc` and pins
87+
> three inspection invariants (I1 provenance / I2 witness fidelity /
88+
> I3 module shape) every `MkTrustedFixture m` construction site is
89+
> audited against.
90+
2391
## RECONCILIATION 2026-05-30 (carrier-ABI proposals 0001 + 0002 accepted + ADR'd — read this FIRST)
2492

2593
> **The "verifier L1-L6 + L13-L16 coverage on emitted wasm" long-tail
@@ -852,12 +920,52 @@ composeAchievedR : LevelAchieved n c2 -> LevelAchieved n (composeCertificates c1
852920
```
853921

854922
A level achieved in either component of a `composeCertificates`
855-
combination is still achieved in the composition. The stronger
856-
"progressive-order" claim — achieving level N implies all lower
857-
levels hold — would require redesigning `ProgressiveCheck` with a
858-
typed `level = S prevLevel` invariant. That redesign is left as
859-
future work; the composition monotonicity above is the useful
860-
structural claim at the current design.
923+
combination is still achieved in the composition.
924+
925+
**The "progressive-order" claim — achieving level N implies all
926+
lower levels were visited — is now ALSO closed (A16, 2026-06-03).**
927+
The deferred half cited above ("would require redesigning
928+
`ProgressiveCheck` with a typed `level = S prevLevel` invariant")
929+
landed as a purely additive typed redesign in `Proofs.idr` §A16:
930+
931+
```
932+
data ProgressiveCheckW : (highestLevel : Nat) -> Type where
933+
StartL1W : LevelAttestationW 1 -> ProgressiveCheckW 1
934+
AdvanceW : (n : Nat)
935+
-> ProgressiveCheckW n
936+
-> LevelAttestationW (S n)
937+
-> ProgressiveCheckW (S n)
938+
939+
data VisitedAt : (m : Nat) -> ProgressiveCheckW n -> Type where
940+
VAStartW : (att : LevelAttestationW 1) -> VisitedAt 1 (StartL1W att)
941+
VAHeadW : (n : Nat) -> (prev : ProgressiveCheckW n)
942+
-> (att : LevelAttestationW (S n))
943+
-> VisitedAt (S n) (AdvanceW n prev att)
944+
VATailW : VisitedAt m prev -> VisitedAt m (AdvanceW n prev att)
945+
946+
progressiveOrderW : (check : ProgressiveCheckW n)
947+
-> (m : Nat) -> LT 0 m -> LTE m n
948+
-> VisitedAt m check
949+
```
950+
951+
`ProgressiveCheckW` is built on top of the standards#130 `LevelAttestationW`
952+
family (already in tree), so each attestation in a typed chain is
953+
required to attest the exact level it sits at — skipping levels
954+
(advancing L1 → L5 in one step) and out-of-order attestations
955+
(attaching `AttestL3W` to a `ProgressiveCheckW 5`) are now type
956+
errors. The proof is by induction on the chain + LTE case split via
957+
a fresh `lteSuccCases` helper (also in §A16). Bridge to the legacy
958+
untyped `ProgressiveCheck` via `forgetProgressiveCheckW`.
959+
960+
**Purely additive.** A16 does NOT replace the operational
961+
`ProgressiveCheck` or the `LevelAchievedIn` composition lemmas above
962+
— legacy consumers (e.g. `buildCertificate`) are unchanged. Same
963+
pattern as `LevelAttestationW` vs `LevelAttestation`.
964+
965+
**Zero escape hatches.** No `believe_me` / `assert_total` /
966+
`postulate` / `sorry` / `Admitted`; `%default total` preserved across
967+
the arc. Build verified: 22/22 modules, rc=0, only pre-existing
968+
shadowing warnings.
861969

862970
**Original task description preserved for history:** If a program achieves
863971
Level N, it achieves all levels 1..N. Stated as:

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

Lines changed: 147 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1548,3 +1548,150 @@ emptyWitnessToLegacy :
15481548
witnessToLegacy (MkWitnessCert [] 0 [])
15491549
= MkCertificate [] 0 []
15501550
emptyWitnessToLegacy = Refl
1551+
1552+
-- ============================================================================
1553+
-- A16 — Typed ProgressiveCheckW (PROOF-NEEDS §P3.2 progressive-order closure)
1554+
-- ============================================================================
1555+
--
1556+
-- PROOF-NEEDS §P3.2 (A8) reframed the level-monotonicity claim under
1557+
-- the operational (untyped) `ProgressiveCheck`, leaving the stronger
1558+
-- "progressive-order" claim — achieving level N implies levels 1..N
1559+
-- were all visited — explicitly deferred:
1560+
--
1561+
-- > the stronger "progressive-order" claim requires redesigning
1562+
-- > `ProgressiveCheck` with a typed `level = S prevLevel` index and
1563+
-- > is left as future work.
1564+
--
1565+
-- A16 closes that deferred half by adding a TYPED `ProgressiveCheckW`
1566+
-- alongside (not replacing) the legacy `ProgressiveCheck`. Like
1567+
-- `LevelAttestationW` vs `LevelAttestation`, the W-variant is purely
1568+
-- additive: no existing definition is touched; legacy consumers are
1569+
-- unaffected.
1570+
--
1571+
-- The redesign:
1572+
--
1573+
-- * `ProgressiveCheckW : (highestLevel : Nat) -> Type` carries the
1574+
-- highest level as a type-level index.
1575+
-- * `StartL1W` requires a level-1 witness attestation
1576+
-- (`LevelAttestationW 1`).
1577+
-- * `AdvanceW` requires the input to be at level `n` and the new
1578+
-- attestation to be at level `S n`. Skipping levels (e.g.
1579+
-- advancing from L1 to L5 in one step) and out-of-order
1580+
-- attestations (e.g. attaching an `AttestL3W` to a
1581+
-- `ProgressiveCheckW 5`) are now type errors.
1582+
--
1583+
-- The progressive-order theorem becomes constructive: every level
1584+
-- 1..n was visited (in the typed sense — there is a sub-derivation
1585+
-- whose attestation is at that level). Proof is by induction on the
1586+
-- check and case analysis on the LTE budget, with one `decEq`
1587+
-- branch on (m, S n) at the head of each `AdvanceW`.
1588+
1589+
||| Typed progressive level check. Index `n` is the highest level
1590+
||| visited; the constructors enforce that the chain visits levels
1591+
||| 1, 2, ..., n in order (no skipping, no out-of-order
1592+
||| attestations).
1593+
|||
1594+
||| Purely additive — the legacy `ProgressiveCheck` is untouched.
1595+
public export
1596+
data ProgressiveCheckW : (highestLevel : Nat) -> Type where
1597+
||| Start at level 1 with a witness attestation for L1.
1598+
StartL1W : LevelAttestationW 1 -> ProgressiveCheckW 1
1599+
||| Advance from level `n` to level `S n` with a matching
1600+
||| attestation. `n` is runtime-available so the index can be
1601+
||| inspected; this matches the `LevelAttestationW` pattern.
1602+
AdvanceW : (n : Nat)
1603+
-> ProgressiveCheckW n
1604+
-> LevelAttestationW (S n)
1605+
-> ProgressiveCheckW (S n)
1606+
1607+
||| Visited-at relation: there is a sub-derivation of `check` whose
1608+
||| attestation is at level `m`. By construction, every
1609+
||| `ProgressiveCheckW n` visits levels 1..n. This is the typed
1610+
||| analogue of `LevelAchievedIn` from A8, lifted to typed chains.
1611+
public export
1612+
data VisitedAt : (m : Nat) -> ProgressiveCheckW n -> Type where
1613+
||| Level 1 is at the start of every chain.
1614+
VAStartW : (att : LevelAttestationW 1) -> VisitedAt 1 (StartL1W att)
1615+
||| The current head of an `AdvanceW` is visited at level `S n`.
1616+
VAHeadW : (n : Nat) -> (prev : ProgressiveCheckW n)
1617+
-> (att : LevelAttestationW (S n))
1618+
-> VisitedAt (S n) (AdvanceW n prev att)
1619+
||| Any level visited deeper in the chain is still visited at the
1620+
||| head — the witness shifts past the new attestation.
1621+
VATailW : {n : Nat}
1622+
-> {0 prev : ProgressiveCheckW n}
1623+
-> {0 att : LevelAttestationW (S n)}
1624+
-> VisitedAt m prev
1625+
-> VisitedAt m (AdvanceW n prev att)
1626+
1627+
||| `lteSuccCases` — every `LTE m (S n)` either witnesses `m = S n`
1628+
||| or strict `LTE m n`. Decidable case-split on the LTE budget
1629+
||| needed by `progressiveOrderW`'s `AdvanceW` recursive step.
1630+
public export
1631+
lteSuccCases : {m, n : Nat} -> LTE m (S n) -> Either (m = S n) (LTE m n)
1632+
lteSuccCases {m = Z} _ = Right LTEZero
1633+
lteSuccCases {m = S Z} {n = Z} (LTESucc LTEZero) = Left Refl
1634+
lteSuccCases {m = S (S _)} {n = Z} (LTESucc lte) = absurd lte
1635+
lteSuccCases {m = S k} {n = S j} (LTESucc lte) =
1636+
case lteSuccCases {m = k} {n = j} lte of
1637+
Left eq => Left (cong S eq)
1638+
Right l => Right (LTESucc l)
1639+
1640+
||| Progressive-order monotonicity (PROOF-NEEDS §P3.2 progressive-order
1641+
||| closure). Every level `m` with `1 <= m <= n` was visited in the
1642+
||| chain.
1643+
|||
1644+
||| Proof: induction on `check`, case analysis on the LTE budget at
1645+
||| the head, single `decEq` branch on (m, S n) at each `AdvanceW`
1646+
||| layer. The `StartL1W` base case discharges the `m = 1` case
1647+
||| directly; impossible `m > 1` budgets fall into the `absurd`
1648+
||| branch of `lteSuccCases`.
1649+
public export
1650+
progressiveOrderW :
1651+
{0 n : Nat}
1652+
-> (check : ProgressiveCheckW n)
1653+
-> (m : Nat)
1654+
-> LT 0 m
1655+
-> LTE m n
1656+
-> VisitedAt m check
1657+
progressiveOrderW (StartL1W att) (S Z) _ _ = VAStartW att
1658+
progressiveOrderW (StartL1W _) (S (S _)) _ (LTESucc lte) = absurd lte
1659+
progressiveOrderW (AdvanceW k prev att) m mPos mLE =
1660+
case lteSuccCases mLE of
1661+
Left Refl => VAHeadW k prev att
1662+
Right lteK => VATailW (progressiveOrderW prev m mPos lteK)
1663+
1664+
-- ----------------------------------------------------------------------------
1665+
-- Index-erasing bridge to the legacy ProgressiveCheck
1666+
-- ----------------------------------------------------------------------------
1667+
--
1668+
-- Downstream consumers that hold a typed `ProgressiveCheckW n` and
1669+
-- want to feed it into the legacy `buildCertificate : ProgressiveCheck
1670+
-- -> ...` pipeline forget the index via this bridge. The legacy
1671+
-- `LevelAttestation` corresponding to each `LevelAttestationW k` is
1672+
-- already available as `toLegacy` (defined earlier in this module);
1673+
-- here we walk the typed chain and reuse `StartL1` / `Advance` to
1674+
-- rebuild the untyped form.
1675+
1676+
||| Forget the typed index — drop a `ProgressiveCheckW n` to the
1677+
||| legacy `ProgressiveCheck`. The visited-level structure is
1678+
||| preserved; only the type-level guarantee is erased. Useful for
1679+
||| feeding into `buildCertificate` while still constructing the
1680+
||| chain through the typed API.
1681+
public export
1682+
forgetProgressiveCheckW : ProgressiveCheckW n -> ProgressiveCheck
1683+
forgetProgressiveCheckW (StartL1W att) = StartL1 (toLegacy att)
1684+
forgetProgressiveCheckW (AdvanceW _ prev att) =
1685+
Advance (forgetProgressiveCheckW prev) (toLegacy att)
1686+
1687+
||| Specialised progressive-order corollary at level 1: every
1688+
||| non-trivial chain visits level 1. Independent of `n` so callers
1689+
||| who only care about the structural "L1 was the entry point"
1690+
||| guarantee don't have to pick an `n`.
1691+
public export
1692+
chainAlwaysVisitsL1 :
1693+
{0 n : Nat}
1694+
-> (check : ProgressiveCheckW (S n))
1695+
-> VisitedAt 1 check
1696+
chainAlwaysVisitsL1 {n} check =
1697+
progressiveOrderW check 1 (LTESucc LTEZero) (LTESucc LTEZero)

0 commit comments

Comments
 (0)