From 0504d0f31022e21b44a2ef4716dd1987e73c107a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:20:20 +0000 Subject: [PATCH 1/2] feat(abi): certificates about one access (Certified.idr) Every witness in a ProgressiveW chain hides what it is about in an implicit argument, so one chain could hold witnesses about unrelated things, and L1 (any Schema), L3 (TypeCompat at one type), L5 (zeroInBounds) and L6 (any value) hold of any program. witnessAchievedEntails therefore returned a witness for some object, not for the access the certificate was meant to describe. Subject names the access (schema, field, field type, access type, pointer, index and count) and the function- and program-level facts of L8-L15. Attest s n is a level-n witness about s and Certified s n a chain of them, so every level of one certificate speaks about the same access. L2 fixes the field's declared type and L3 relates it to the access type. Theorems: certMonotone, certMonotoneForget, certFieldTyped, certPointer, certInBounds, certResult, and simpleReadCertifiedForget (forgetting the subject gives simpleReadChain). exampleCertified inhabits the type. New rejections: AccessAtWrongType, ForeignPointer, CertifiedOutOfBounds. Not changed: each level is as strong as its witness type, and the legacy and ProgressiveW forms keep the gap. Not proved: that a Subject describes the program; that is the producer's claim. PROOF-NEEDS gains a dated current-state banner over the 2026-04-13 summary it supersedes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- CHANGELOG.adoc | 35 +++ LEVEL-STATUS.adoc | 26 +- PROOF-NEEDS.adoc | 31 +++ src/abi/TypedWasm/ABI/Certified.idr | 349 ++++++++++++++++++++++++++ src/abi/typed-wasm.ipkg | 1 + tests/proof/regression.mjs | 19 ++ tests/reject/AccessAtWrongType.idr | 33 +++ tests/reject/CertifiedOutOfBounds.idr | 33 +++ tests/reject/ForeignPointer.idr | 36 +++ tests/reject/README.adoc | 3 + 10 files changed, 565 insertions(+), 1 deletion(-) create mode 100644 src/abi/TypedWasm/ABI/Certified.idr create mode 100644 tests/reject/AccessAtWrongType.idr create mode 100644 tests/reject/CertifiedOutOfBounds.idr create mode 100644 tests/reject/ForeignPointer.idr diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index d2c5d68..7299413 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,6 +9,41 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Certificates about one access (2026-11-09) + +* New module `Certified.idr`. Every witness in a `ProgressiveW` chain hides + what it is about in an implicit argument, so one chain could hold + witnesses about unrelated things, and L1 (any `Schema`), L3 (`TypeCompat` + at one type), L5 (`zeroInBounds`) and L6 (any value) hold of any program. + `witnessAchievedEntails` therefore returned a witness for *some* object. +* `Subject` names the access (schema, field, field type, access type, + pointer kind and lifetime, index and count) and the function- and + program-level facts of L8-L15. `Attest s n` is a level-n witness about + `s`; `Certified s n` is a chain of them, so every level of one certificate + speaks about the same access. L2 fixes the field's declared type and L3 + relates it to the access type. +* Theorems: `certMonotone`, `certMonotoneForget` (agrees with + `levelMonotoneW` after forgetting), and what a certificate says about its + access: `certFieldTyped` (from level 3: the access reads a field of its + schema at that field's declared type), `certPointer`, `certInBounds`, + `certResult`. `forget` / `forgetChain` give back the `LevelAttestationW` / + `ProgressiveW` forms, and `simpleReadCertifiedForget` shows the + simple-read certificate forgets to `simpleReadChain`. `exampleCertified` + inhabits the type. +* New expected rejections: `AccessAtWrongType` (an I32 field read at F64), + `ForeignPointer` (an L4 pointer into another region), + `CertifiedOutOfBounds` (instance 1 of a one-instance region). +* Not changed: each level is as strong as its witness type. L7 + (`ExclusiveWitness`, a scope name) and L10 (`CompletedProtocol`, any + `FreeResult`) stay weak, and L12 and L13 are not indexed by the subject. + The legacy and `ProgressiveW` certificates are unchanged and keep the gap. +* Not proved: that a `Subject` describes the program. That its schema is the + region's and its count the region's instance count is the claim of whoever + builds it (producer or verifier); `Certified.idr` checks the certificate + against the subject, not the subject against the program. +* `PROOF-NEEDS.adoc`: a dated banner replaces the 2026-04-13 summary as the + current state. + ==== L15-C at the front-end: a caller's caps contain its callee's (2026-10-27) * The canonical Rust front-end (`typed-wasm-codegen`, ADR-0006) now parses diff --git a/LEVEL-STATUS.adoc b/LEVEL-STATUS.adoc index ff6aa36..839d548 100644 --- a/LEVEL-STATUS.adoc +++ b/LEVEL-STATUS.adoc @@ -372,7 +372,31 @@ subsuming the A9 family. *`+WitnessCertificate+` lift 2026-05-27 (PR `+record WitnessCertificate+` mirror of `+ProofCertificate+` with witness-carrying levels, `+witnessToLegacy+` bridge, `+composeWitness+` mirror, `+composeWitnessLegacyAgree+` compat lemma, `+WitnessAchieved+` -predicate. +predicate. *`+ProgressiveW+` 2026-10-26 (#279)*: a chain holding a witness for +every level 1..n in order (`+levelMonotoneW+`, `+witnessAchievedEntails+`). +*Limit, found 2026-11-09:* every witness in these certificates hides what +it is about, so one certificate can mix witnesses about unrelated things, +and L1 (any `+Schema+`), L3 (`+TypeCompat+` at one type), L5 +(`+zeroInBounds+`) and L6 (any value) hold of any program. "Cannot be +constructed without real proof artefacts" holds; the artefacts need not +be about one access. `+Certified.idr+` is the form without that gap; +the legacy and `+ProgressiveW+` forms keep it. + +|Certified.idr |0 |0 |0 |In package (2026-11-09). Certificates about one +access: `+Attest s n+` is a level-n witness about the `+Subject+` s +(schema, field, field type, access type, pointer, index and count, and +the function- and program-level facts of L8-L15), and `+Certified s n+` a +chain of them. PROVEN (`+idris2 --build+`): `+certMonotone+`, +`+certMonotoneForget+`, `+certFieldTyped+` (a level-3 certificate says the +access reads a field of its schema at that field's declared type), +`+certPointer+`, `+certInBounds+`, `+certResult+`, and +`+simpleReadCertifiedForget+` (forgetting the subject gives +`+simpleReadChain+`). `+exampleCertified+` inhabits the type. TESTED: +`+tests/reject/{AccessAtWrongType,ForeignPointer,CertifiedOutOfBounds}.idr+`. +Unchanged: each level is as strong as its witness type (L7 a scope name, +L10 any `+FreeResult+`; L12 and L13 are not indexed by the subject). +Not proved: that a `+Subject+` describes the program (its schema is the +region's, its count the instance count); that is the producer's claim. |Tropical.idr |0 |0 |0 |In package (A1, 2026-04-18). PWL-01 (2026-10-14): min-plus drawn from the grade kernel (`+TropCost = LossGrade+`); laws diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 5b8f329..28bfacd 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -5,6 +5,37 @@ typed-wasm’s formal verification. Read this file in full before touching `+src/abi/TypedWasm/ABI/*.idr+`. Written 2026-04-13 by the dual-AST / parser-panic cleanup Claude after a targeted audit. +=== CURRENT STATE 2026-11-09 (read this first; supersedes the 2026-04-13 summary below) + +____ +*The ledger is `LEVEL-STATUS.adoc`.* This file is a handoff log: the +dated banners below record what each session found, and the oldest +summary no longer describes the tree. + +* *Certificates.* The 2026-04-13 finding that `Proofs.idr` "rubber-stamps + attestations without using their witnesses" is closed in three steps: + witness-carrying `LevelAttestationW` (A7-A12, PR #80), the `ProgressiveW` + chain with a witness for every level 1..n (#279), and `Certified.idr` + (2026-11-09), where every witness is about one `Subject` (the access) so + a certificate says something about its access (`certFieldTyped`, + `certPointer`, `certInBounds`, `certResult`). The legacy and + `ProgressiveW` forms remain and keep the gap `Certified.idr` closes. +* *Since the last banner (2026-06-16):* the PWL-01 grade kernel + (`ResourceAlgebra*.idr`, transcribed from resource-algebra), L13 + occupancy (`Occupancy.idr`, from occupancy-types), L16 K-CUT-LOSS + (`KCut.idr`, from choreographic-types), and L15-A/B/C in the Rust + front-end (#281). The re-proofs are PROVEN in Idris2; their + correspondence to the Agda sources is ASSUMED (port-and-reprove), and the + kernel's operation tables are TESTED against Agda by `refl`. +* *Gate:* `tools/check-kernel-proofs.sh` (build, every + `tests/reject/*.idr` refused at its `invalid` declaration with its + expected message, the transcription table, negative controls) and + `tests/proof/regression.mjs --strict`. +* *Open, as recorded:* the L13 binding is not linked to `memory.grow`; + the T4 layout lemma and the T5a/T5b verifier tie-backs are as the + 2026-06-16 banner left them (not rechecked in this pass). +____ + === The one-line honest summary typed-wasm has *eleven Idris2 files encoding a safety protocol using QTT diff --git a/src/abi/TypedWasm/ABI/Certified.idr b/src/abi/TypedWasm/ABI/Certified.idr new file mode 100644 index 0000000..6f7fc45 --- /dev/null +++ b/src/abi/TypedWasm/ABI/Certified.idr @@ -0,0 +1,349 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Certificates about one access. +-- +-- `LevelAttestationW n` (Proofs.idr) carries a witness for level n, but the +-- thing each witness is about is hidden in an implicit argument. A +-- `ProgressiveW n` chain can therefore be assembled from witnesses about +-- unrelated things, and some levels are inhabited for any program: +-- +-- AttestL1W [] -- any schema +-- AttestL3W (TypeCompat {ty = U8}) -- reflexivity, U8 against U8 +-- AttestL5W zeroInBounds -- index 0 of some non-empty region +-- AttestL6W (MkAccessResult v) -- any value of any type +-- +-- So `witnessAchievedEntails` returns a witness for *some* object, not for +-- the access the certificate was meant to describe. +-- +-- `Subject` names that access: the schema it reads, the field, the type it +-- reads at, the pointer's kind and lifetime, the index and instance count, +-- and the function- and program-level facts levels 8 to 15 talk about. +-- `Attest subj n` is a level-n witness *about subj*, and `Certified subj n` +-- is a chain of them. Every level of one certificate therefore speaks about +-- the same access: +-- +-- * L2 binds the field to the schema and fixes its declared type +-- (`subjFieldTy`), and L3 relates that type to the access type +-- (`subjAccessTy`). Reading an I32 field at F64 has no L3 witness +-- (tests/reject/AccessAtWrongType.idr). +-- * L4 and L7 are about the subject's schema: a pointer into another +-- region does not fit (tests/reject/ForeignPointer.idr). +-- * L5 is about the subject's index and count (tests/reject/ +-- CertifiedOutOfBounds.idr), and L6 returns the subject's access type. +-- +-- `forget` and `forgetChain` drop the subject and give back the +-- `LevelAttestationW` / `ProgressiveW` forms, so this is a strengthening of +-- those, not a different object. +-- +-- What this does not change: each level's witness is as strong as its type +-- in the module that defines it. `ExclusiveWitness` (L7) is a scope name, +-- `CompletedProtocol` (L10) any `FreeResult`, and `Level12Proof` (L12) and +-- `IsolatedModule` (L13) are not indexed by anything a `Subject` can name. +-- Indexing ties the levels to one access; it does not make a weak level +-- stronger. L1 has no predicate of its own (parse-time validity); its +-- attestation is the subject's schema. +-- +-- What this does not prove: that the subject describes the program. A +-- certificate is about its `Subject`; that `subjSchema` is the region's +-- schema and `subjCount` its instance count is the claim of whoever builds +-- the subject (the producer, or the verifier reading its carrier sections), +-- not something this module checks. +-- +-- No `believe_me`, `assert_total` or `postulate`; `%default total`. +module TypedWasm.ABI.Certified + +import Data.Nat +import TypedWasm.ABI.Region +import TypedWasm.ABI.TypedAccess +import TypedWasm.ABI.Levels +import TypedWasm.ABI.Pointer +import TypedWasm.ABI.Effects +import TypedWasm.ABI.Lifetime +import TypedWasm.ABI.Linear +import TypedWasm.ABI.MultiModule +import TypedWasm.ABI.Tropical +import TypedWasm.ABI.Epistemic +import TypedWasm.ABI.ModuleIsolation +import TypedWasm.ABI.SessionProtocol +import TypedWasm.ABI.ResourceCapabilities +import TypedWasm.ABI.Proofs + +%default total + +-- ============================================================================ +-- The subject of a certificate +-- ============================================================================ + +||| The access a certificate is about, and the function and program around +||| it. Levels 1-7 talk about the access, 8-10 about the enclosing function, +||| 11-15 about the program. +public export +record Subject where + constructor MkSubject + ||| The region schema the access reads (L1, L2, L4, L7). + subjSchema : Schema + ||| The field the access names (L2). + subjField : String + ||| The field's declared type in `subjSchema` (fixed by L2). + subjFieldTy : WasmType + ||| The type the access reads or writes at (L3, L6). + subjAccessTy : WasmType + ||| The pointer's kind and lifetime (L4). + subjPtrKind : PtrKind + subjPtrLife : Levels.Lifetime + ||| The instance index and the region's instance count (L5). + subjIndex : Nat + subjCount : Nat + ||| Declared and actual effects of the enclosing function (L8). + subjDeclared : EffectSet + subjActual : EffectSet + ||| The reference's lifetime and the scope it is used in (L9). + subjRefLife : Lifetime.Lifetime + subjScopeLife : Lifetime.Lifetime + ||| The allocation token the function must free (L10). + subjToken : Nat + ||| The size of the cost matrix (L11). + subjCostN : Nat + ||| The session protocol (L14). + subjProtocol : Protocol + ||| The module whose capabilities the function draws on (L15). + subjCaps : ModuleCaps + +-- ============================================================================ +-- Attestations about a subject +-- ============================================================================ + +||| A level-`n` witness about the subject `s`. +public export +data Attest : (s : Subject) -> (n : Nat) -> Type where + ||| L1: the subject's schema is the instruction's schema. + AttS1 : Attest s 1 + ||| L2: the field is in the schema, and its declared type is `subjFieldTy`. + AttS2 : (fi : FieldIn (subjField s) (subjSchema s)) + -> fieldType (lookupField fi) = subjFieldTy s + -> Attest s 2 + ||| L3: the access type is compatible with the field's declared type. + AttS3 : WasmTypeCompat (subjFieldTy s) (subjAccessTy s) -> Attest s 3 + ||| L4: a non-null pointer into the subject's schema. + AttS4 : Pointer.Ptr (subjPtrKind s) (subjSchema s) (subjPtrLife s) NonNull + -> Attest s 4 + ||| L5: the index is in bounds of the instance count. + AttS5 : InBounds (subjIndex s) (subjCount s) -> Attest s 5 + ||| L6: the access returns a value of the access type. + AttS6 : AccessResult (subjAccessTy s) -> Attest s 6 + ||| L7: no other pointer to the subject's schema is live. + AttS7 : ExclusiveWitness (subjSchema s) -> Attest s 7 + ||| L8: the function's actual effects are among its declared ones. + AttS8 : EffectSubsumes (subjDeclared s) (subjActual s) -> Attest s 8 + ||| L9: the reference outlives the scope it is used in. + AttS9 : Lifetime.Outlives (subjRefLife s) (subjScopeLife s) -> Attest s 9 + ||| L10: the function's allocation token is freed. + AttS10 : CompletedProtocol (subjToken s) -> Attest s 10 + ||| L11: every access route is cost-bounded. + AttS11 : AllPairsCosts (subjCostN s) -> Attest s 11 + ||| L12: epistemic freshness (not indexed by the subject; see header). + AttS12 : Level12Proof -> Attest s 12 + ||| L13: module isolation (not indexed by the subject; see header). + AttS13 : IsolatedModule -> Attest s 13 + ||| L14: the subject's protocol is well formed. + AttS14 : WellFormedProtocol (subjProtocol s) -> Attest s 14 + ||| L15: the function's capabilities are contained in its module's. + AttS15 : FunctionCaps (subjCaps s) -> Attest s 15 + +||| Drop the subject: the witness-carrying attestation of `Proofs.idr`. +public export +forget : {s : Subject} -> Attest s n -> LevelAttestationW n +forget {s} AttS1 = AttestL1W (subjSchema s) +forget (AttS2 fi _) = AttestL2W fi +forget (AttS3 w) = AttestL3W w +forget (AttS4 w) = AttestL4W w +forget (AttS5 w) = AttestL5W w +forget (AttS6 w) = AttestL6W w +forget (AttS7 w) = AttestL7W w +forget (AttS8 w) = AttestL8W w +forget (AttS9 w) = AttestL9W w +forget (AttS10 w) = AttestL10W w +forget (AttS11 w) = AttestL11W w +forget (AttS12 w) = AttestL12W w +forget (AttS13 w) = AttestL13W w +forget (AttS14 w) = AttestL14W w +forget (AttS15 w) = AttestL15W w + +-- ============================================================================ +-- Certificates: a chain of attestations about one subject +-- ============================================================================ + +||| A witness about `s` for every level from 1 up to `n`, in order. +public export +data Certified : (s : Subject) -> (n : Nat) -> Type where + StartS : Attest s 1 -> Certified s 1 + AdvanceS : {n : Nat} -> Certified s n -> Attest s (S n) -> Certified s (S n) + +||| Drop the subject from every link: the `ProgressiveW` chain. +public export +forgetChain : {s : Subject} -> Certified s n -> ProgressiveW n +forgetChain (StartS a) = StartW (forget a) +forgetChain (AdvanceS c a) = AdvanceW (forgetChain c) (forget a) + +||| The witness about `s` for the chain's top level. +public export +certTop : Certified s n -> Attest s n +certTop (StartS a) = a +certTop (AdvanceS _ a) = a + +||| Level monotonicity about one subject: a certificate that reaches `n` +||| holds a witness about the same `s` for every level `m`, `1 <= m <= n`. +public export +certMonotone : Certified s n + -> (m : Nat) + -> LTE 1 m + -> LTE m n + -> Attest s m +certMonotone (StartS _) Z one _ = absurd one +certMonotone (StartS a) (S Z) _ _ = a +certMonotone (StartS _) (S (S _)) _ (LTESucc le) = absurd le +certMonotone (AdvanceS prev a) m one le = + case lteSuccSplit le of + Left le' => certMonotone prev m one le' + Right eq => rewrite eq in a + +||| Monotonicity commutes with forgetting the subject: the witness the +||| subject-free chain gives for level `m` is the one this chain gives, +||| forgotten. +public export +certMonotoneForget : {s : Subject} + -> (c : Certified s n) + -> (m : Nat) + -> (one : LTE 1 m) + -> (le : LTE m n) + -> levelMonotoneW (forgetChain c) m one le + = forget (certMonotone c m one le) +certMonotoneForget (StartS _) Z one _ = absurd one +certMonotoneForget (StartS a) (S Z) _ _ = Refl +certMonotoneForget (StartS _) (S (S _)) _ (LTESucc le) = absurd le +certMonotoneForget (AdvanceS prev a) m one le with (lteSuccSplit le) + _ | Left le' = certMonotoneForget prev m one le' + _ | Right eq = rewrite eq in Refl + +-- ============================================================================ +-- What a certificate says about its access +-- ============================================================================ + +||| `FieldTyped name ty schema`: the schema has a field called `name` +||| whose declared type is `ty`. +public export +data FieldTyped : (name : String) -> (ty : WasmType) -> (schema : Schema) -> Type where + MkFieldTyped : (fi : FieldIn name schema) + -> fieldType (lookupField fi) = ty + -> FieldTyped name ty schema + +||| Compatible wasm types are equal (`WasmTypeCompat` has one constructor). +public export +compatEq : WasmTypeCompat a b -> a = b +compatEq TypeCompat = Refl + +||| A certificate at level 3 or above says the access reads a field of its +||| schema at that field's declared type. This is the statement the +||| subject-free chain cannot make: there, L2's field and L3's types are +||| about unrelated things. +public export +certFieldTyped : {s : Subject} + -> Certified s n + -> LTE 3 n + -> FieldTyped (subjField s) (subjAccessTy s) (subjSchema s) +certFieldTyped c le = + case (certMonotone c 2 (LTESucc LTEZero) (lteSuccLeft le), certMonotone c 3 (LTESucc LTEZero) le) of + (AttS2 fi eq, AttS3 w) => MkFieldTyped fi (trans eq (compatEq w)) + +||| A certificate at level 4 or above holds a non-null pointer into the +||| access's own schema. +public export +certPointer : Certified s n + -> LTE 4 n + -> Pointer.Ptr (subjPtrKind s) (subjSchema s) (subjPtrLife s) NonNull +certPointer c le with (certMonotone c 4 (LTESucc LTEZero) le) + _ | AttS4 p = p + +||| A certificate at level 5 or above says the access's index is in bounds. +public export +certInBounds : Certified s n -> LTE 5 n -> InBounds (subjIndex s) (subjCount s) +certInBounds c le with (certMonotone c 5 (LTESucc LTEZero) le) + _ | AttS5 b = b + +||| A certificate at level 6 or above returns a value of the access type. +public export +certResult : Certified s n -> LTE 6 n -> AccessResult (subjAccessTy s) +certResult c le with (certMonotone c 6 (LTESucc LTEZero) le) + _ | AttS6 r = r + +-- ============================================================================ +-- The simple-read certificate about one access +-- ============================================================================ + +||| `simpleReadChain` (Proofs.idr) with every witness about the same access. +public export +simpleReadCertified : {s : Subject} + -> (fi : FieldIn (subjField s) (subjSchema s)) + -> (fieldTy : fieldType (lookupField fi) = subjFieldTy s) + -> (compat : WasmTypeCompat (subjFieldTy s) (subjAccessTy s)) + -> (ptr : Pointer.Ptr (subjPtrKind s) (subjSchema s) (subjPtrLife s) NonNull) + -> (bounds : InBounds (subjIndex s) (subjCount s)) + -> (result : AccessResult (subjAccessTy s)) + -> Certified s 6 +simpleReadCertified fi fieldTy compat ptr bounds result = + AdvanceS (AdvanceS (AdvanceS (AdvanceS (AdvanceS + (StartS AttS1) + (AttS2 fi fieldTy)) (AttS3 compat)) (AttS4 ptr)) (AttS5 bounds)) (AttS6 result) + +||| Forgetting the subject of `simpleReadCertified` gives `simpleReadChain` +||| on the same witnesses, so its legacy projection is `simpleReadCert`. +||| Stated for a subject whose field type and access type are one `ty`: +||| `WasmTypeCompat` admits no other case, and `simpleReadChain` asks for +||| `WasmTypeCompat ty ty`. +public export +simpleReadCertifiedForget : + {sch : Schema} -> {f : String} -> {ty : WasmType} + -> {k : PtrKind} -> {pl : Levels.Lifetime} + -> {i, cnt : Nat} + -> {d, a : EffectSet} -> {rl, sl : Lifetime.Lifetime} + -> {tok, cn : Nat} -> {p : Protocol} -> {caps : ModuleCaps} + -> (fi : FieldIn f sch) + -> (fieldTy : fieldType (lookupField fi) = ty) + -> (compat : WasmTypeCompat ty ty) + -> (ptr : Pointer.Ptr k sch pl NonNull) + -> (bounds : InBounds i cnt) + -> (result : AccessResult ty) + -> forgetChain (simpleReadCertified + {s = MkSubject sch f ty ty k pl i cnt d a rl sl tok cn p caps} + fi fieldTy compat ptr bounds result) + = simpleReadChain sch fi compat ptr bounds result +simpleReadCertifiedForget _ _ _ _ _ _ = Refl + +-- ============================================================================ +-- A concrete certificate +-- ============================================================================ +-- +-- The type is inhabited: instance 0 of a one-instance region with an I32 +-- field "x", read at I32. `exampleFieldTyped` reads the typing fact back +-- out of the certificate. + +||| The access: field "x" (I32) of a one-instance region, read at I32. +public export +exampleSubject : Subject +exampleSubject = + MkSubject [MkField "x" I32] "x" I32 I32 Owning Levels.Static 0 1 + [] [] Lifetime.Static Lifetime.Static 0 0 + (MkProtocol (MkSessionId "example") [] [] Nothing) emptyModuleCaps + +||| A level-6 certificate about `exampleSubject`. +public export +exampleCertified : Certified Certified.exampleSubject 6 +exampleCertified = + simpleReadCertified FieldHere Refl TypeCompat (MkPtr 64) zeroInBounds + (MkAccessResult 7) + +||| What the certificate says about its access. +public export +exampleFieldTyped : FieldTyped "x" I32 [MkField "x" I32] +exampleFieldTyped = certFieldTyped exampleCertified (LTESucc (LTESucc (LTESucc LTEZero))) diff --git a/src/abi/typed-wasm.ipkg b/src/abi/typed-wasm.ipkg index 413892f..80043c7 100644 --- a/src/abi/typed-wasm.ipkg +++ b/src/abi/typed-wasm.ipkg @@ -41,6 +41,7 @@ modules = TypedWasm.ABI.Region , TypedWasm.ABI.PackedLayout , TypedWasm.ABI.AccessTypingSpec , TypedWasm.ABI.Proofs + , TypedWasm.ABI.Certified , TypedWasm.ABI.VerifierSpec -- Cross-language layout contracts (aggregate library role, ADR-004). -- Restored 2026-04-18 after fixing the Idris2 0.8 reduction + parsing diff --git a/tests/proof/regression.mjs b/tests/proof/regression.mjs index 71cb535..7fcb1f9 100644 --- a/tests/proof/regression.mjs +++ b/tests/proof/regression.mjs @@ -361,6 +361,25 @@ const EXPECTED = [ ["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"], + + // Certified.idr — certificates about one access. Every level of a + // `Certified s n` is a witness about the same `Subject`, so a certificate + // says something about its access (`certFieldTyped`), which a + // subject-free `ProgressiveW` cannot. + ["Certified.idr", /^record\s+Subject/m, "The access a certificate is about"], + ["Certified.idr", /^data\s+Attest\s/m, "Subject-indexed attestation"], + ["Certified.idr", /^forget\s*:/m, "Attestation forgets its subject"], + ["Certified.idr", /^data\s+Certified/m, "Subject-indexed certificate chain"], + ["Certified.idr", /^forgetChain\s*:/m, "Certificate forgets to ProgressiveW"], + ["Certified.idr", /^certMonotone\s*:/m, "Every level 1..n has a witness about the subject"], + ["Certified.idr", /^certMonotoneForget\s*:/m, "Monotonicity commutes with forgetting"], + ["Certified.idr", /^certFieldTyped\s*:/m, "Certified access reads a field at its declared type"], + ["Certified.idr", /^certPointer\s*:/m, "Certified access holds a pointer into its own schema"], + ["Certified.idr", /^certInBounds\s*:/m, "Certified access index is in bounds"], + ["Certified.idr", /^certResult\s*:/m, "Certified access returns its access type"], + ["Certified.idr", /^simpleReadCertified\s*:/m, "simpleReadCert about one access"], + ["Certified.idr", /^simpleReadCertifiedForget\s*:/m, "Forgetting gives simpleReadChain"], + ["Certified.idr", /^exampleCertified\s*:/m, "A concrete certificate (the type is inhabited)"], ]; // ---------------------------------------------------------------------- diff --git a/tests/reject/AccessAtWrongType.idr b/tests/reject/AccessAtWrongType.idr new file mode 100644 index 0000000..5f0016f --- /dev/null +++ b/tests/reject/AccessAtWrongType.idr @@ -0,0 +1,33 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- MUST FAIL (tools/check-kernel-proofs.sh). +-- +-- An access that reads the I32 field "x" at F64. Its L3 attestation must +-- relate the field's declared type to the access type; the subject-free +-- `AttestL3W` accepted `TypeCompat` at any one type, so a chain could carry +-- L3 for a read at the wrong width. +-- EXPECT: Mismatch between: F64 and I32 +module AccessAtWrongType + +import TypedWasm.ABI.Region +import TypedWasm.ABI.TypedAccess +import TypedWasm.ABI.Levels +import TypedWasm.ABI.Pointer +import TypedWasm.ABI.Effects +import TypedWasm.ABI.Lifetime +import TypedWasm.ABI.SessionProtocol +import TypedWasm.ABI.ResourceCapabilities +import TypedWasm.ABI.MultiModule +import TypedWasm.ABI.Certified + +%default total + +||| One I32 field, "x", read at F64, instance 0 of 1. +subject : Subject +subject = MkSubject [MkField "x" I32] "x" I32 F64 Owning Levels.Static 0 1 + [] [] Lifetime.Static Lifetime.Static 0 0 + (MkProtocol (MkSessionId "p") [] [] Nothing) emptyModuleCaps + +invalid : Attest AccessAtWrongType.subject 3 +invalid = AttS3 TypeCompat diff --git a/tests/reject/CertifiedOutOfBounds.idr b/tests/reject/CertifiedOutOfBounds.idr new file mode 100644 index 0000000..649b104 --- /dev/null +++ b/tests/reject/CertifiedOutOfBounds.idr @@ -0,0 +1,33 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- MUST FAIL (tools/check-kernel-proofs.sh). +-- +-- Instance 1 of a region with one instance, certified as in bounds. The +-- subject-free `AttestL5W` took `zeroInBounds` for any region; here the +-- index and count are the access's own. +-- EXPECT: Mismatch between: S \?right and 0 +module CertifiedOutOfBounds + +import Data.Nat +import TypedWasm.ABI.Region +import TypedWasm.ABI.TypedAccess +import TypedWasm.ABI.Levels +import TypedWasm.ABI.Pointer +import TypedWasm.ABI.Effects +import TypedWasm.ABI.Lifetime +import TypedWasm.ABI.SessionProtocol +import TypedWasm.ABI.ResourceCapabilities +import TypedWasm.ABI.MultiModule +import TypedWasm.ABI.Certified + +%default total + +||| One I32 field, "x", read at I32, instance 1 of 1. +subject : Subject +subject = MkSubject [MkField "x" I32] "x" I32 I32 Owning Levels.Static 1 1 + [] [] Lifetime.Static Lifetime.Static 0 0 + (MkProtocol (MkSessionId "p") [] [] Nothing) emptyModuleCaps + +invalid : Attest CertifiedOutOfBounds.subject 5 +invalid = AttS5 (MkInBounds (LTESucc (LTESucc LTEZero))) diff --git a/tests/reject/ForeignPointer.idr b/tests/reject/ForeignPointer.idr new file mode 100644 index 0000000..7cce2d8 --- /dev/null +++ b/tests/reject/ForeignPointer.idr @@ -0,0 +1,36 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- MUST FAIL (tools/check-kernel-proofs.sh). +-- +-- A non-null pointer into a different region (one F32 field "y") offered as +-- the L4 witness for an access to the region with the I32 field "x". The +-- subject-free `AttestL4W` took a pointer into any schema. +-- EXPECT: Mismatch between: F32 and I32 +module ForeignPointer + +import TypedWasm.ABI.Region +import TypedWasm.ABI.TypedAccess +import TypedWasm.ABI.Levels +import TypedWasm.ABI.Pointer +import TypedWasm.ABI.Effects +import TypedWasm.ABI.Lifetime +import TypedWasm.ABI.SessionProtocol +import TypedWasm.ABI.ResourceCapabilities +import TypedWasm.ABI.MultiModule +import TypedWasm.ABI.Certified + +%default total + +||| One I32 field, "x", read at I32, instance 0 of 1. +subject : Subject +subject = MkSubject [MkField "x" I32] "x" I32 I32 Owning Levels.Static 0 1 + [] [] Lifetime.Static Lifetime.Static 0 0 + (MkProtocol (MkSessionId "p") [] [] Nothing) emptyModuleCaps + +||| A pointer into another region. +other : Pointer.Ptr Owning [MkField "y" F32] Levels.Static NonNull +other = MkPtr 64 + +invalid : Attest ForeignPointer.subject 4 +invalid = AttS4 other diff --git a/tests/reject/README.adoc b/tests/reject/README.adoc index e462bf0..07bf2de 100644 --- a/tests/reject/README.adoc +++ b/tests/reject/README.adoc @@ -24,6 +24,9 @@ because then the control proves nothing. | `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 +| `AccessAtWrongType` | a certificate about one access whose L3 lets it read the I32 field "x" at F64 +| `ForeignPointer` | a certificate about one access whose L4 pointer points into a different region +| `CertifiedOutOfBounds` | a certificate about one access whose L5 calls instance 1 of a one-instance region in bounds |=== `HWMAnnihilates`, `LossWorstCase`, `DriftExceedsPeak` and `MinMaxIsLoss` mirror resource-algebra From d962835ab05f08e581f855d9aea24f4d3f809a4e Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:40:26 +0000 Subject: [PATCH 2/2] docs(certified): L4 and L7 are indexed by the schema, not the region The header, changelog, ForeignPointer fixture and rejects README said a pointer "into another region" does not fit L4. The index is the schema: a pointer whose schema differs is refused, but two regions with the same schema are not told apart. Say that instead. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- CHANGELOG.adoc | 3 ++- src/abi/TypedWasm/ABI/Certified.idr | 6 ++++-- tests/reject/ForeignPointer.idr | 8 ++++---- tests/reject/README.adoc | 2 +- 4 files changed, 11 insertions(+), 8 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 7299413..0785b45 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -31,7 +31,8 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. simple-read certificate forgets to `simpleReadChain`. `exampleCertified` inhabits the type. * New expected rejections: `AccessAtWrongType` (an I32 field read at F64), - `ForeignPointer` (an L4 pointer into another region), + `ForeignPointer` (an L4 pointer into a region with a different schema; + regions that share a schema are not told apart), `CertifiedOutOfBounds` (instance 1 of a one-instance region). * Not changed: each level is as strong as its witness type. L7 (`ExclusiveWitness`, a scope name) and L10 (`CompletedProtocol`, any diff --git a/src/abi/TypedWasm/ABI/Certified.idr b/src/abi/TypedWasm/ABI/Certified.idr index 6f7fc45..e14beb2 100644 --- a/src/abi/TypedWasm/ABI/Certified.idr +++ b/src/abi/TypedWasm/ABI/Certified.idr @@ -27,8 +27,10 @@ -- (`subjFieldTy`), and L3 relates that type to the access type -- (`subjAccessTy`). Reading an I32 field at F64 has no L3 witness -- (tests/reject/AccessAtWrongType.idr). --- * L4 and L7 are about the subject's schema: a pointer into another --- region does not fit (tests/reject/ForeignPointer.idr). +-- * L4 and L7 are indexed by the subject's schema: a pointer whose schema +-- differs does not fit (tests/reject/ForeignPointer.idr). The index is +-- the schema, not the region, so two regions with the same schema are +-- not told apart. -- * L5 is about the subject's index and count (tests/reject/ -- CertifiedOutOfBounds.idr), and L6 returns the subject's access type. -- diff --git a/tests/reject/ForeignPointer.idr b/tests/reject/ForeignPointer.idr index 7cce2d8..81c511b 100644 --- a/tests/reject/ForeignPointer.idr +++ b/tests/reject/ForeignPointer.idr @@ -3,9 +3,9 @@ -- -- MUST FAIL (tools/check-kernel-proofs.sh). -- --- A non-null pointer into a different region (one F32 field "y") offered as --- the L4 witness for an access to the region with the I32 field "x". The --- subject-free `AttestL4W` took a pointer into any schema. +-- A non-null pointer into a region with a different schema (one F32 field +-- "y") offered as the L4 witness for an access to the region with the I32 +-- field "x". The subject-free `AttestL4W` took a pointer into any schema. -- EXPECT: Mismatch between: F32 and I32 module ForeignPointer @@ -28,7 +28,7 @@ subject = MkSubject [MkField "x" I32] "x" I32 I32 Owning Levels.Static 0 1 [] [] Lifetime.Static Lifetime.Static 0 0 (MkProtocol (MkSessionId "p") [] [] Nothing) emptyModuleCaps -||| A pointer into another region. +||| A pointer into a region with a different schema. other : Pointer.Ptr Owning [MkField "y" F32] Levels.Static NonNull other = MkPtr 64 diff --git a/tests/reject/README.adoc b/tests/reject/README.adoc index 07bf2de..9e2b09f 100644 --- a/tests/reject/README.adoc +++ b/tests/reject/README.adoc @@ -25,7 +25,7 @@ because then the control proves nothing. | `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 | `AccessAtWrongType` | a certificate about one access whose L3 lets it read the I32 field "x" at F64 -| `ForeignPointer` | a certificate about one access whose L4 pointer points into a different region +| `ForeignPointer` | a certificate about one access whose L4 pointer points into a region with a different schema (the index is the schema, not the region) | `CertifiedOutOfBounds` | a certificate about one access whose L5 calls instance 1 of a one-instance region in bounds |===