From 2efb573272c18901bd709d5f1dd6227932d0de5f Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 22:20:22 +0000 Subject: [PATCH 1/5] feat(abi): certificates whose level is their witnesses (ProgressiveW) WitnessCertificate carried a witness per attestation, but its highest level was a free Nat: MkWitnessCert [] 15 [] reported 15 while holding no attestation. And A8 left the "progressive-order" claim (no level without the ones below it) as future work, pending a chain indexed by level = S prevLevel. ProgressiveW n is that chain. StartW takes a level-1 witness and AdvanceW only the next level's, so the type has no inhabitant without a witness for every level 1..n. - levelMonotoneW: a chain at level n yields the witness for every m with 1 <= m <= n (PROOF-NEEDS P3.2's levelMonotone, over witnesses). - chainCert sets the certificate's highest level to the chain index (chainCertHighest); chainAchievedIn / chainCertAchieves show the certificate claims every such level. - witnessAchievedEntails: any level a WitnessCertificate claims gives that level's LevelAttestationW back. - simpleReadChain, fullChain12, fullChain15 keep the witnesses the legacy certificates discard; *Legacy lemmas (Refl) show each projects to simpleReadCert, fullCert12 and fullCert15. - Rejects SkippedLevel and ClaimWithoutWitness; regression inventory gains the 16 new names. Legacy ProofCertificate is unchanged and still exposes MkAttestation, so a legacy claim proves nothing about witnesses. The chain does not model NotApplicable. No believe_me, assert_total or postulate; %default total. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- CHANGELOG.adoc | 26 ++ src/abi/TypedWasm/ABI/Proofs.idr | 348 ++++++++++++++++++++++++++- tests/proof/regression.mjs | 21 ++ tests/reject/ClaimWithoutWitness.idr | 18 ++ tests/reject/README.adoc | 2 + tests/reject/SkippedLevel.idr | 21 ++ 6 files changed, 431 insertions(+), 5 deletions(-) create mode 100644 tests/reject/ClaimWithoutWitness.idr create mode 100644 tests/reject/SkippedLevel.idr diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 834cca1..4a4406c 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,6 +9,32 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Certificates whose level is their witnesses (2026-10-26) + +* `Proofs.idr`: `ProgressiveW n`, a chain holding a witness for every + level from 1 to `n` in order. `StartW` takes level 1 and `AdvanceW` + only the next level, so no chain reaches a level while skipping one. + `WitnessCertificate`'s highest level was a free `Nat` + (`MkWitnessCert [] 15 []` reported 15 while holding no attestation); + `chainCert` sets it to the chain's index (`chainCertHighest`). +* `levelMonotoneW`: a chain at level `n` yields the witness for every + level `m` with `1 <= m <= n`. This is PROOF-NEEDS §P3.2's + `levelMonotone`, over witnesses, and the "progressive-order" claim A8 + left as future work. +* `chainAchievedIn` / `chainCertAchieves`: a chain's certificate claims + every such level. `witnessAchievedEntails`: any level a + `WitnessCertificate` claims gives that level's `LevelAttestationW` + back, so the claim is evidence, not a label. +* `simpleReadChain`, `fullChain12`, `fullChain15` take the witnesses + `simpleReadCert`, `fullCert12` and `fullCert15` take, and keep them. + `*Legacy` lemmas (`Refl`) show each projects to the legacy certificate. +* New rejects `SkippedLevel` (a chain from level 1 to level 3) and + `ClaimWithoutWitness` (a claim of level 7 in a certificate with no + attestations). +* Not changed: legacy `ProofCertificate` still exposes `MkAttestation`, + so a legacy claim can be written without a witness. The chain does not + model `NotApplicable`; a certificate that waives a level stays legacy. + ==== occupancy-types pin `6013483` → `8f09c0b` (2026-10-14) * `scripts/fetch-siblings.sh` pins occupancy-types at `8f09c0b`, the merge of diff --git a/src/abi/TypedWasm/ABI/Proofs.idr b/src/abi/TypedWasm/ABI/Proofs.idr index fa2e99d..ca84c21 100644 --- a/src/abi/TypedWasm/ABI/Proofs.idr +++ b/src/abi/TypedWasm/ABI/Proofs.idr @@ -477,9 +477,9 @@ fullCert15 l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 costProof epistemicProof isoMod wfProt -- concrete attestation list — and proves the monotonicity *under -- certificate composition*: composing two certificates preserves any -- level achieved in either component. This is the structural --- monotonicity relevant to the current design; the stronger --- "progressive-order" claim requires redesigning `ProgressiveCheck` --- with a typed `level = S prevLevel` index and is left as future work. +-- monotonicity relevant to the legacy design. The stronger +-- "progressive-order" claim, over a chain indexed by `level = S +-- prevLevel`, is `levelMonotoneW` on `ProgressiveW` (end of this module). ||| `LevelAchievedIn n atts` — level `n` appears in the attestation list ||| with status `Proven`. This is the concrete propositional form of @@ -737,8 +737,9 @@ dropCertErases = MkErases Proofs.dropCert -- bridge for all fifteen levels, witness-consuming at the type level. -- Like the A8 reframing, this is the honest incremental theorem; the -- stronger "attestation entails the level's semantic property" claim --- needs `LevelAttestation` reindexed by the witness and is left as --- tracked future work (standards#130 / epic standards#124). +-- needs the attestation reindexed by the witness: `LevelAttestationW` +-- below, with `witnessAchievedEntails` and the `ProgressiveW` chain at +-- the end of this module (standards#130 / epic standards#124). -- -- These declarations are purely additive: no existing definition is -- touched, so no prior proof can regress. `%default total` (module @@ -1561,3 +1562,340 @@ emptyWitnessToLegacy : witnessToLegacy (MkWitnessCert [] 0 []) = MkCertificate [] 0 [] emptyWitnessToLegacy = Refl + +-- ============================================================================ +-- ProgressiveW — certificates whose level is their witnesses +-- ============================================================================ +-- +-- `WitnessCertificate` carries one witness per attestation, but its +-- `witnessHighestProven` is a free `Nat`, and nothing ties it to the +-- witnesses it sits beside: `MkWitnessCert [] 15 []` reports 15 as its +-- highest level while holding no attestation at all. A8 recorded the matching gap for `ProgressiveCheck`: +-- the "progressive-order" claim (you cannot reach level N without levels +-- 1..N-1) needed a chain indexed by `level = S prevLevel` and was left +-- as future work. +-- +-- `ProgressiveW n` is that chain. Its index is the highest level, and +-- each step must supply the witness for exactly the next level, so the +-- type cannot be inhabited without a witness for every level 1..n. +-- Three theorems state what that buys: +-- +-- levelMonotoneW — every level m with 1 <= m <= n has a +-- witness in the chain (PROOF-NEEDS §P3.2's +-- original `levelMonotone`, over witnesses). +-- chainAchievedIn — the chain's certificate claims every such m. +-- witnessAchievedEntails — any claim a WitnessCertificate makes +-- yields the witness for that level. +-- +-- The chain does not model `NotApplicable`: a level without a witness +-- cannot appear in it. Certificates that waive a level stay on the +-- legacy `ProofCertificate` path, where `MkAttestation` is still a public +-- constructor and a claim therefore proves nothing about witnesses. +-- +-- Purely additive: no existing definition changes. + +||| A witness for every level from 1 up to the index `n`, in order. +||| `StartW` takes level 1; `AdvanceW` takes the next level's witness. +public export +data ProgressiveW : (n : Nat) -> Type where + StartW : LevelAttestationW 1 -> ProgressiveW 1 + AdvanceW : {n : Nat} + -> ProgressiveW n + -> LevelAttestationW (S n) + -> ProgressiveW (S n) + +||| The witness for the chain's top level. +public export +chainTop : ProgressiveW n -> LevelAttestationW n +chainTop (StartW a) = a +chainTop (AdvanceW _ a) = a + +||| A chain always starts at level 1, so its index is at least 1. +public export +chainLevelPositive : ProgressiveW n -> LTE 1 n +chainLevelPositive (StartW _) = LTESucc LTEZero +chainLevelPositive (AdvanceW _ _) = LTESucc LTEZero + +||| `m <= S n` splits into `m <= n` or `m = S n`. +public export +lteSuccSplit : {m, n : Nat} -> LTE m (S n) -> Either (LTE m n) (m = S n) +lteSuccSplit {m = Z} _ = Left LTEZero +lteSuccSplit {m = S _} {n = Z} (LTESucc LTEZero) = Right Refl +lteSuccSplit {m = S _} {n = Z} (LTESucc (LTESucc _)) impossible +lteSuccSplit {m = S _} {n = S _} (LTESucc p) = + case lteSuccSplit p of + Left q => Left (LTESucc q) + Right eq => Right (cong S eq) + +||| Level monotonicity over witnesses: a chain that reaches level `n` +||| holds the witness for every level `m` with `1 <= m <= n`. +||| +||| This is PROOF-NEEDS §P3.2's `levelMonotone`, stated over witnesses +||| rather than over a bare "achieved" predicate: the result is the +||| level-`m` attestation itself, so the matching `attestLmW_Entails*` +||| extractor recovers the level's safety evidence. +public export +levelMonotoneW : ProgressiveW n + -> (m : Nat) + -> LTE 1 m + -> LTE m n + -> LevelAttestationW m +levelMonotoneW (StartW _) Z one _ = absurd one +levelMonotoneW (StartW a) (S Z) _ _ = a +levelMonotoneW (StartW _) (S (S _)) _ (LTESucc le) = absurd le +levelMonotoneW (AdvanceW prev a) m one le = + case lteSuccSplit le of + Left le' => levelMonotoneW prev m one le' + Right eq => rewrite eq in a + +||| The chain's attestations, lowest level first. +public export +chainLevels : ProgressiveW n -> List SomeAttestationW +chainLevels (StartW a) = [MkSomeAttW a] +chainLevels (AdvanceW {n} p a) = chainLevels p ++ [MkSomeAttW {n = S n} a] + +||| The witness certificate a chain denotes. Its highest level is the +||| chain's index, not a free `Nat`. +public export +chainCert : {n : Nat} -> ProgressiveW n -> WitnessCertificate +chainCert {n} c = MkWitnessCert (chainLevels c) n [] + +||| The certificate's highest level is the chain's index. +public export +chainCertHighest : {n : Nat} + -> (c : ProgressiveW n) + -> witnessHighestProven (chainCert c) = n +chainCertHighest _ = Refl + +||| A chain's attestation list claims every level from 1 up to its index. +public export +chainAchievedIn : (c : ProgressiveW n) + -> (m : Nat) + -> LTE 1 m + -> LTE m n + -> LevelAchievedIn m (witnessLevelsToLegacy (chainLevels c)) +chainAchievedIn (StartW _) Z one _ = absurd one +chainAchievedIn (StartW _) (S Z) _ _ = LAHere +chainAchievedIn (StartW _) (S (S _)) _ (LTESucc le) = absurd le +chainAchievedIn (AdvanceW {n} p a) m one le = + rewrite witnessLevelsToLegacyAppend (chainLevels p) [MkSomeAttW {n = S n} a] in + case lteSuccSplit le of + Left le' => achievedAppendL (chainAchievedIn p m one le') + Right eq => rewrite eq in achievedAppendR (witnessLevelsToLegacy (chainLevels p)) LAHere + +||| The chain's certificate claims every level from 1 up to its index. +public export +chainCertAchieves : {n : Nat} + -> (c : ProgressiveW n) + -> (m : Nat) + -> LTE 1 m + -> LTE m n + -> WitnessAchieved m (chainCert c) +chainCertAchieves c m one le = chainAchievedIn c m one le + +-- ---------------------------------------------------------------------------- +-- Achievement entails the witness +-- ---------------------------------------------------------------------------- +-- +-- `LevelAchievedIn n` over a legacy list proves only that some entry +-- reads `MkAttestation n Proven`, which anyone can write. Over the +-- projection of a `WitnessCertificate` it proves more: every entry came +-- from a `LevelAttestationW`, so the entry the claim points at gives the +-- level-`n` witness back. + +||| A claim of level `n` in a projected witness list yields the level-`n` +||| witness attestation. +public export +witnessLevelsEntail : (ls : List SomeAttestationW) + -> LevelAchievedIn n (witnessLevelsToLegacy ls) + -> LevelAttestationW n +witnessLevelsEntail [] LAHere impossible +witnessLevelsEntail [] (LAThere _) impossible +witnessLevelsEntail (MkSomeAttW att :: _) LAHere = att +witnessLevelsEntail (_ :: xs) (LAThere p) = witnessLevelsEntail xs p + +||| Any level a witness certificate claims comes with its witness: +||| `WitnessAchieved n c` is evidence of level `n`'s safety property, +||| recovered by the matching `attestLnW_Entails*` extractor. +public export +witnessAchievedEntails : (c : WitnessCertificate) + -> WitnessAchieved n c + -> LevelAttestationW n +witnessAchievedEntails (MkWitnessCert ls _ _) p = witnessLevelsEntail ls p + +-- ---------------------------------------------------------------------------- +-- The existing certificates as witness chains +-- ---------------------------------------------------------------------------- +-- +-- `simpleReadCert`, `fullCert12` and `fullCert15` take one witness per +-- level and then discard them into a legacy `ProofCertificate`. The +-- chains below take the same witnesses and keep them; the `*Legacy` +-- lemmas show that projecting each chain's certificate gives exactly the +-- legacy certificate, so the chain is a strengthening, not a different +-- object. + +||| `simpleReadCert` as a chain to level 6. +public export +simpleReadChain : {nameL2 : String} -> {schemaL2 : Schema} + -> {tyL3 : WasmType} + -> {kindL4 : PtrKind} -> {schemaL4 : Schema} -> {lifeL4 : Levels.Lifetime} + -> {idxL5 : Nat} -> {countL5 : Nat} + -> {tyL6 : WasmType} + -> (l1 : Schema) + -> (l2 : FieldIn nameL2 schemaL2) + -> (l3 : WasmTypeCompat tyL3 tyL3) + -> (l4 : Pointer.Ptr kindL4 schemaL4 lifeL4 NonNull) + -> (l5 : InBounds idxL5 countL5) + -> (l6 : AccessResult tyL6) + -> ProgressiveW 6 +simpleReadChain l1 l2 l3 l4 l5 l6 = + AdvanceW (AdvanceW (AdvanceW (AdvanceW (AdvanceW + (StartW (AttestL1W l1)) + (AttestL2W l2)) (AttestL3W l3)) (AttestL4W l4)) (AttestL5W l5)) (AttestL6W l6) + +||| Projecting `simpleReadChain`'s certificate gives `simpleReadCert`. +public export +simpleReadChainLegacy : + {nameL2 : String} -> {schemaL2 : Schema} + -> {tyL3 : WasmType} + -> {kindL4 : PtrKind} -> {schemaL4 : Schema} -> {lifeL4 : Levels.Lifetime} + -> {idxL5 : Nat} -> {countL5 : Nat} + -> {tyL6 : WasmType} + -> (l1 : Schema) + -> (l2 : FieldIn nameL2 schemaL2) + -> (l3 : WasmTypeCompat tyL3 tyL3) + -> (l4 : Pointer.Ptr kindL4 schemaL4 lifeL4 NonNull) + -> (l5 : InBounds idxL5 countL5) + -> (l6 : AccessResult tyL6) + -> witnessToLegacy (chainCert (simpleReadChain l1 l2 l3 l4 l5 l6)) + = simpleReadCert l1 l2 l3 l4 l5 l6 +simpleReadChainLegacy _ _ _ _ _ _ = Refl + +||| `fullCert12` as a chain to level 12. +public export +fullChain12 : {nameL2 : String} -> {schemaL2 : Schema} + -> {tyL3 : WasmType} + -> {kindL4 : PtrKind} -> {schemaL4 : Schema} -> {lifeL4 : Levels.Lifetime} + -> {idxL5 : Nat} -> {countL5 : Nat} + -> {tyL6 : WasmType} + -> {schemaL7 : Schema} + -> {declared, actual : EffectSet} + -> {rl, sl : Lifetime.Lifetime} + -> {tokL10 : Nat} + -> {n : Nat} + -> (l1 : Schema) + -> (l2 : FieldIn nameL2 schemaL2) + -> (l3 : WasmTypeCompat tyL3 tyL3) + -> (l4 : Pointer.Ptr kindL4 schemaL4 lifeL4 NonNull) + -> (l5 : InBounds idxL5 countL5) + -> (l6 : AccessResult tyL6) + -> (l7 : ExclusiveWitness schemaL7) + -> (l8 : EffectSubsumes declared actual) + -> (l9 : Lifetime.Outlives rl sl) + -> (l10 : CompletedProtocol tokL10) + -> (costProof : AllPairsCosts n) + -> (epistemicProof : Level12Proof) + -> ProgressiveW 12 +fullChain12 l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 costProof epistemicProof = + AdvanceW (AdvanceW (AdvanceW (AdvanceW (AdvanceW (AdvanceW + (simpleReadChain l1 l2 l3 l4 l5 l6) + (AttestL7W l7)) (AttestL8W l8)) (AttestL9W l9)) (AttestL10W l10)) + (AttestL11W costProof)) (AttestL12W epistemicProof) + +||| Projecting `fullChain12`'s certificate gives `fullCert12`. +public export +fullChain12Legacy : + {nameL2 : String} -> {schemaL2 : Schema} + -> {tyL3 : WasmType} + -> {kindL4 : PtrKind} -> {schemaL4 : Schema} -> {lifeL4 : Levels.Lifetime} + -> {idxL5 : Nat} -> {countL5 : Nat} + -> {tyL6 : WasmType} + -> {schemaL7 : Schema} + -> {declared, actual : EffectSet} + -> {rl, sl : Lifetime.Lifetime} + -> {tokL10 : Nat} + -> {n : Nat} + -> (l1 : Schema) + -> (l2 : FieldIn nameL2 schemaL2) + -> (l3 : WasmTypeCompat tyL3 tyL3) + -> (l4 : Pointer.Ptr kindL4 schemaL4 lifeL4 NonNull) + -> (l5 : InBounds idxL5 countL5) + -> (l6 : AccessResult tyL6) + -> (l7 : ExclusiveWitness schemaL7) + -> (l8 : EffectSubsumes declared actual) + -> (l9 : Lifetime.Outlives rl sl) + -> (l10 : CompletedProtocol tokL10) + -> (costProof : AllPairsCosts n) + -> (epistemicProof : Level12Proof) + -> witnessToLegacy (chainCert (fullChain12 l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 costProof epistemicProof)) + = fullCert12 l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 costProof epistemicProof +fullChain12Legacy _ _ _ _ _ _ _ _ _ _ _ _ = Refl + +||| `fullCert15` as a chain to level 15. +public export +fullChain15 : {nameL2 : String} -> {schemaL2 : Schema} + -> {tyL3 : WasmType} + -> {kindL4 : PtrKind} -> {schemaL4 : Schema} -> {lifeL4 : Levels.Lifetime} + -> {idxL5 : Nat} -> {countL5 : Nat} + -> {tyL6 : WasmType} + -> {schemaL7 : Schema} + -> {declared, actual : EffectSet} + -> {rl, sl : Lifetime.Lifetime} + -> {tokL10 : Nat} + -> {n : Nat} + -> {p : Protocol} + -> {owner : ModuleCaps} + -> (l1 : Schema) + -> (l2 : FieldIn nameL2 schemaL2) + -> (l3 : WasmTypeCompat tyL3 tyL3) + -> (l4 : Pointer.Ptr kindL4 schemaL4 lifeL4 NonNull) + -> (l5 : InBounds idxL5 countL5) + -> (l6 : AccessResult tyL6) + -> (l7 : ExclusiveWitness schemaL7) + -> (l8 : EffectSubsumes declared actual) + -> (l9 : Lifetime.Outlives rl sl) + -> (l10 : CompletedProtocol tokL10) + -> (costProof : AllPairsCosts n) + -> (epistemicProof : Level12Proof) + -> (isoMod : IsolatedModule) + -> (wfProto : WellFormedProtocol p) + -> (fc : FunctionCaps owner) + -> ProgressiveW 15 +fullChain15 l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 costProof epistemicProof isoMod wfProto fc = + AdvanceW (AdvanceW (AdvanceW + (fullChain12 l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 costProof epistemicProof) + (AttestL13W isoMod)) (AttestL14W wfProto)) (AttestL15W fc) + +||| Projecting `fullChain15`'s certificate gives `fullCert15`. +public export +fullChain15Legacy : + {nameL2 : String} -> {schemaL2 : Schema} + -> {tyL3 : WasmType} + -> {kindL4 : PtrKind} -> {schemaL4 : Schema} -> {lifeL4 : Levels.Lifetime} + -> {idxL5 : Nat} -> {countL5 : Nat} + -> {tyL6 : WasmType} + -> {schemaL7 : Schema} + -> {declared, actual : EffectSet} + -> {rl, sl : Lifetime.Lifetime} + -> {tokL10 : Nat} + -> {n : Nat} + -> {p : Protocol} + -> {owner : ModuleCaps} + -> (l1 : Schema) + -> (l2 : FieldIn nameL2 schemaL2) + -> (l3 : WasmTypeCompat tyL3 tyL3) + -> (l4 : Pointer.Ptr kindL4 schemaL4 lifeL4 NonNull) + -> (l5 : InBounds idxL5 countL5) + -> (l6 : AccessResult tyL6) + -> (l7 : ExclusiveWitness schemaL7) + -> (l8 : EffectSubsumes declared actual) + -> (l9 : Lifetime.Outlives rl sl) + -> (l10 : CompletedProtocol tokL10) + -> (costProof : AllPairsCosts n) + -> (epistemicProof : Level12Proof) + -> (isoMod : IsolatedModule) + -> (wfProto : WellFormedProtocol p) + -> (fc : FunctionCaps owner) + -> witnessToLegacy (chainCert (fullChain15 l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 costProof epistemicProof isoMod wfProto fc)) + = fullCert15 l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 costProof epistemicProof isoMod wfProto fc +fullChain15Legacy _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = Refl diff --git a/tests/proof/regression.mjs b/tests/proof/regression.mjs index 4a82465..71cb535 100644 --- a/tests/proof/regression.mjs +++ b/tests/proof/regression.mjs @@ -340,6 +340,27 @@ const EXPECTED = [ ["Proofs.idr", /^emptyWitnessCertificate\s*:/m, "Empty witness certificate (concrete inhabitant)"], ["Proofs.idr", /^singletonWitnessCertificate\s*:/m, "Singleton witness certificate smart ctor"], ["Proofs.idr", /^emptyWitnessToLegacy\s*:/m, "Empty round-trip Refl"], + + // Proofs.idr — ProgressiveW: a certificate chain whose level is its + // witnesses (levels 1..n, in order), with the theorems that make a + // claimed level evidence. Pins the names so a refactor cannot + // silently drop the chain or weaken a theorem to a label. + ["Proofs.idr", /^data\s+ProgressiveW/m, "Level-indexed witness chain"], + ["Proofs.idr", /^chainTop\s*:/m, "Top-level witness of a chain"], + ["Proofs.idr", /^lteSuccSplit\s*:/m, "m <= S n splits (helper)"], + ["Proofs.idr", /^levelMonotoneW\s*:/m, "Every level 1..n has a witness (PROOF-NEEDS P3.2)"], + ["Proofs.idr", /^chainCert\s*:/m, "Chain to witness certificate"], + ["Proofs.idr", /^chainCertHighest\s*:/m, "Certificate level is the chain index"], + ["Proofs.idr", /^chainAchievedIn\s*:/m, "Chain claims every level 1..n"], + ["Proofs.idr", /^chainCertAchieves\s*:/m, "Chain certificate claims every level 1..n"], + ["Proofs.idr", /^witnessLevelsEntail\s*:/m, "Claim in a witness list yields the witness"], + ["Proofs.idr", /^witnessAchievedEntails\s*:/m, "Claimed level entails its witness"], + ["Proofs.idr", /^simpleReadChain\s*:/m, "simpleReadCert as a chain"], + ["Proofs.idr", /^simpleReadChainLegacy\s*:/m, "simpleReadChain projects to simpleReadCert"], + ["Proofs.idr", /^fullChain12\s*:/m, "fullCert12 as a chain"], + ["Proofs.idr", /^fullChain12Legacy\s*:/m, "fullChain12 projects to fullCert12"], + ["Proofs.idr", /^fullChain15\s*:/m, "fullCert15 as a chain"], + ["Proofs.idr", /^fullChain15Legacy\s*:/m, "fullChain15 projects to fullCert15"], ]; // ---------------------------------------------------------------------- diff --git a/tests/reject/ClaimWithoutWitness.idr b/tests/reject/ClaimWithoutWitness.idr new file mode 100644 index 0000000..cc96a2f --- /dev/null +++ b/tests/reject/ClaimWithoutWitness.idr @@ -0,0 +1,18 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- MUST FAIL (tools/check-kernel-proofs.sh). +-- +-- A witness certificate that sets its highest level to 7 but holds no +-- attestations. `WitnessAchieved` reads the attestations, not the +-- highest-level field, so the claim has nothing to point at. +-- EXPECT: Mismatch between: MkAttestation \?n Proven :: \?rest and \[\] +module ClaimWithoutWitness + +import TypedWasm.ABI.MultiModule +import TypedWasm.ABI.Proofs + +%default total + +invalid : WitnessAchieved 7 (MkWitnessCert [] 7 []) +invalid = LAHere diff --git a/tests/reject/README.adoc b/tests/reject/README.adoc index d6b0528..e462bf0 100644 --- a/tests/reject/README.adoc +++ b/tests/reject/README.adoc @@ -22,6 +22,8 @@ because then the control proves nothing. | `InitialOverMaximum` | an L13 private memory certified by an empty run although its initial allocation is unbounded by its maximum | `UnprojectableChoice` | K-CUT-LOSS without the Projectable side-condition (choreographic-types K-7) | `InconsistentCut` | K-CUT-LOSS without the Consistent side-condition (choreographic-types K-7) +| `SkippedLevel` | a certificate chain that jumps from level 1 to level 3, skipping level 2 +| `ClaimWithoutWitness` | a witness certificate claiming level 7 with no attestations, on the strength of its highest-level field alone |=== `HWMAnnihilates`, `LossWorstCase`, `DriftExceedsPeak` and `MinMaxIsLoss` mirror resource-algebra diff --git a/tests/reject/SkippedLevel.idr b/tests/reject/SkippedLevel.idr new file mode 100644 index 0000000..ea70b1d --- /dev/null +++ b/tests/reject/SkippedLevel.idr @@ -0,0 +1,21 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- MUST FAIL (tools/check-kernel-proofs.sh). +-- +-- A witness chain that jumps from level 1 to level 3. `AdvanceW` on a +-- chain at level 1 needs a level-2 witness; a level-3 one does not fit, +-- so a certificate cannot reach a level while skipping the one below it. +-- Idris2 reports the clash of LevelAttestationW 3 with LevelAttestationW 2 +-- after peeling the common successors, as 1 against 0. +-- EXPECT: Mismatch between: 1 and 0 +module SkippedLevel + +import TypedWasm.ABI.Region +import TypedWasm.ABI.MultiModule +import TypedWasm.ABI.Proofs + +%default total + +invalid : ProgressiveW 2 +invalid = AdvanceW (StartW (AttestL1W [])) (AttestL3W (TypeCompat {ty = U8})) From 1a504c1acf7e47cee9e0a24b357aad6147c13e97 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 26 Oct 2026 22:46:16 +0000 Subject: [PATCH 2/5] docs(abi): Clarify chain certificate contents and witness evidence requirements --- src/abi/TypedWasm/ABI/Proofs.idr | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/abi/TypedWasm/ABI/Proofs.idr b/src/abi/TypedWasm/ABI/Proofs.idr index ca84c21..7f2f8df 100644 --- a/src/abi/TypedWasm/ABI/Proofs.idr +++ b/src/abi/TypedWasm/ABI/Proofs.idr @@ -1656,6 +1656,8 @@ chainLevels (AdvanceW {n} p a) = chainLevels p ++ [MkSomeAttW {n = S n} a] ||| The witness certificate a chain denotes. Its highest level is the ||| chain's index, not a free `Nat`. +||| Retains the chain's attestations in ascending level order and has +||| no multi-module compatibility entries. public export chainCert : {n : Nat} -> ProgressiveW n -> WitnessCertificate chainCert {n} c = MkWitnessCert (chainLevels c) n [] @@ -1717,6 +1719,8 @@ witnessLevelsEntail (_ :: xs) (LAThere p) = witnessLevelsEntail xs p ||| Any level a witness certificate claims comes with its witness: ||| `WitnessAchieved n c` is evidence of level `n`'s safety property, ||| recovered by the matching `attestLnW_Entails*` extractor. +||| The claim must identify an attestation in `c`'s projected level list; +||| `witnessHighestProven` alone supplies no such evidence. public export witnessAchievedEntails : (c : WitnessCertificate) -> WitnessAchieved n c From 0705c0d6876826301fb2e4294f676acac3396997 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 23:01:11 +0000 Subject: [PATCH 3/5] ci(kernel-proofs): pin the runner and require Agda 2.6.3 ubuntu-latest moved to Ubuntu 26.04 on 2026-10-19. The kernel-proofs job installs Agda from apt, so it got Agda 2.8.0, which prints error locations as file:11.38 where 2.6.3 printed file:11,38. occupancy-types' own reject check only accepts the old form, so it reported CostIsOccupancy as an unexpected failure even though Agda refused it correctly. Every PR now fails the job; main last ran it on 2026-10-17, before the move. The job runs on ubuntu-24.04, whose agda-bin is 2.6.3, and check-kernel-proofs.sh refuses any other Agda (ALLOW_ANY_AGDA=1 to override), as it already refuses any Idris2 but 0.8.0. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- .github/workflows/contract-gate.yml | 6 +++++- CHANGELOG.adoc | 12 ++++++++++++ tools/check-kernel-proofs.sh | 7 +++++++ 3 files changed, 24 insertions(+), 1 deletion(-) diff --git a/.github/workflows/contract-gate.yml b/.github/workflows/contract-gate.yml index 41157d6..7d27b61 100644 --- a/.github/workflows/contract-gate.yml +++ b/.github/workflows/contract-gate.yml @@ -56,7 +56,11 @@ jobs: # cannot). kernel-proofs: name: Grade kernel proofs (Idris2 0.8.0 + Agda) - runs-on: ubuntu-latest + # Pinned: the job installs Agda from apt, so the image decides the Agda + # version, and the reject checks need 2.6.3 (tools/check-kernel-proofs.sh + # refuses any other). ubuntu-latest moved to 26.04 (Agda 2.8.0) on + # 2026-10-19. + runs-on: ubuntu-24.04 timeout-minutes: 40 env: IDRIS2_COMMIT: 15a3e4e70843f7a34100f6470c04b791330788df # v0.8.0 diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 4a4406c..03ad9cd 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -35,6 +35,18 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. so a legacy claim can be written without a witness. The chain does not model `NotApplicable`; a certificate that waives a level stays legacy. +==== Kernel proofs pinned to Agda 2.6.3 (2026-10-26) + +* `ubuntu-latest` moved to Ubuntu 26.04 on 2026-10-19, so the Contract + Gate's kernel-proofs job, which installs Agda from apt, got Agda 2.8.0. + 2.8.0 prints error locations as `file:11.38` where 2.6.3 printed + `file:11,38`, and occupancy-types' own reject check accepts only the old + form, so it reported `CostIsOccupancy` as an unexpected failure although + Agda refused it correctly. +* The job now runs on `ubuntu-24.04`, whose `agda-bin` is 2.6.3, and + `tools/check-kernel-proofs.sh` refuses any other Agda (as it already + refuses any Idris2 but 0.8.0), unless `ALLOW_ANY_AGDA=1` is set. + ==== occupancy-types pin `6013483` → `8f09c0b` (2026-10-14) * `scripts/fetch-siblings.sh` pins occupancy-types at `8f09c0b`, the merge of diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh index 8f5757e..e005cfa 100755 --- a/tools/check-kernel-proofs.sh +++ b/tools/check-kernel-proofs.sh @@ -48,6 +48,13 @@ case "$iv" in *"version 0.8.0"*) ;; *) [ -n "${ALLOW_ANY_IDRIS2:-}" ] || die "Idris2 0.8.0 required (src/abi targets 0.8.0; EXPECT messages are 0.8.0's). Set ALLOW_ANY_IDRIS2=1 to try another." ;; esac +# The rejection checks match prover messages and locations, and both change +# between Agda releases: 2.8.0 prints `file:11.38` where 2.6.3 printed +# `file:11,38`, which occupancy-types' own reject check does not accept. +case "$av" in + *"version 2.6.3"*) ;; + *) [ -n "${ALLOW_ANY_AGDA:-}" ] || die "Agda 2.6.3 required (the pinned siblings' reject checks expect 2.6.3's messages). Set ALLOW_ANY_AGDA=1 to try another." ;; +esac [ -d "$RA/src/ResourceAlgebra" ] || die "resource-algebra not fetched — run scripts/fetch-siblings.sh" echo "resource-algebra at $(git -C "$RA" rev-parse HEAD)" rm -rf "$OUT"; mkdir -p "$OUT" From efd88639b823528f89b04d0a03b11ea32ea62ceb Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 23:04:56 +0000 Subject: [PATCH 4/5] ci(kernel-proofs): use [[ ]] in the Agda version check SonarCloud (shell rule: prefer [[ over [) on the line added in 1b98e5d. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- tools/check-kernel-proofs.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh index e005cfa..a5aec39 100755 --- a/tools/check-kernel-proofs.sh +++ b/tools/check-kernel-proofs.sh @@ -53,7 +53,7 @@ esac # `file:11,38`, which occupancy-types' own reject check does not accept. case "$av" in *"version 2.6.3"*) ;; - *) [ -n "${ALLOW_ANY_AGDA:-}" ] || die "Agda 2.6.3 required (the pinned siblings' reject checks expect 2.6.3's messages). Set ALLOW_ANY_AGDA=1 to try another." ;; + *) [[ -n "${ALLOW_ANY_AGDA:-}" ]] || die "Agda 2.6.3 required (the pinned siblings' reject checks expect 2.6.3's messages). Set ALLOW_ANY_AGDA=1 to try another." ;; esac [ -d "$RA/src/ResourceAlgebra" ] || die "resource-algebra not fetched — run scripts/fetch-siblings.sh" echo "resource-algebra at $(git -C "$RA" rev-parse HEAD)" From dfdc603f77b15348a840c8ddb962d2ef3516863f Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 23:10:10 +0000 Subject: [PATCH 5/5] ci(kernel-proofs): match the whole Agda version line The glob *"version 2.6.3"* also accepted 2.6.3.1 or 2.6.30. The check now requires the line to be exactly "Agda version 2.6.3". Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- tools/check-kernel-proofs.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh index a5aec39..043c403 100755 --- a/tools/check-kernel-proofs.sh +++ b/tools/check-kernel-proofs.sh @@ -52,7 +52,7 @@ esac # between Agda releases: 2.8.0 prints `file:11.38` where 2.6.3 printed # `file:11,38`, which occupancy-types' own reject check does not accept. case "$av" in - *"version 2.6.3"*) ;; + "Agda version 2.6.3") ;; # the whole line: 2.6.3.1 is another release *) [[ -n "${ALLOW_ANY_AGDA:-}" ]] || die "Agda 2.6.3 required (the pinned siblings' reject checks expect 2.6.3's messages). Set ALLOW_ANY_AGDA=1 to try another." ;; esac [ -d "$RA/src/ResourceAlgebra" ] || die "resource-algebra not fetched — run scripts/fetch-siblings.sh"