diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index de5db0d..0785b45 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,37 +9,41 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] -==== Access sites carry ADR-0003 byte offsets; wire counts are bounded (2026-11-09) - -* `verify_access_typing_from_module` now reads `instruction_byte_offset` - as ADR-0003 defines it: the byte offset of the access opcode within the - function body, counted from the start of the locals vector. Before, both - the verifier and `typed-wasm-codegen` used an operator index in that - slot, which contradicted the ADR and made the gate reject every Ephapax - module (Ephapax follows the ADR). `emit` now writes the byte offset of - each pinned instruction (read from `Function::byte_len` while encoding). - New `AccessTypingError` variants: `AccessSiteOffsetOutOfRange` (replaces - `AccessSiteIndexOutOfRange`) and `AccessSiteNotAnInstructionBoundary`; - `AccessSiteNotAMemoryOp` now reports `byte_offset`. -* Every `typedwasm.*` codec bounds its wire counts and length prefixes by - the bytes remaining before allocating. A count the payload cannot hold - is `CarrierError::CountExceedsPayload`, surfaced by the verifier passes - as `VerifyError::MalformedCarrier`. Before, an ownership payload with - count `0xFFFF_FFFF` requested a ~137 GB allocation and aborted the - process. `parse_ownership_section_payload` now returns a `Result`; the - versioned codecs gain `try_parse_*` variants (the `parse_*` forms keep - returning `Option`, `None` also for a malformed payload). Departure from - OCaml parity: a count larger than the payload can encode is rejected, - not zero-filled; truncation *within* an entry stays lenient. -* Docs: removed claims that a `verify_regions_from_module` pass exists, - that Ephapax compiles to WasmGC, that Ephapax emits the ownership section - on every compile, and that ephapax#251 is pending; documented that - `Layout.Types.stringLayout` models `(array i32)`, not `(array i8)`; marked - `generated/abi/` and `stdlib/` as not created; and stated that the - `VerifierSpecAgreement` / `SourceVerifierAgreement` inhabitants are true - by construction rather than a proof about the Rust verifier. -* New proposal 0007 (PROPOSED, not adopted): an `Affine` usage grade, a - `typedwasm.mode` module mode record and a separate borrow axis. +==== 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 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 + `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) diff --git a/LEVEL-STATUS.adoc b/LEVEL-STATUS.adoc index bef4f92..c9a4a4f 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 fe74664..0acc0f9 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..e14beb2 --- /dev/null +++ b/src/abi/TypedWasm/ABI/Certified.idr @@ -0,0 +1,351 @@ +-- 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 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. +-- +-- `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..81c511b --- /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 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 + +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 a region with a different schema. +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..9e2b09f 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 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 |=== `HWMAnnihilates`, `LossWorstCase`, `DriftExceedsPeak` and `MinMaxIsLoss` mirror resource-algebra