feat(abi): certificates about one access (Certified.idr)

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)
 

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

PROOF-NEEDS.adoc

@@ -1,3 +1,3 @@
 == PROOF-NEEDS.md
 
 *Scope:* handoff document for the Claude instance that will deepen
@@ -5,6 +5,37 @@
 `+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