From 13d26a5ee48d86847e85352572f84de5dbe63144 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 00:55:01 +0000 Subject: [PATCH 01/13] =?UTF-8?q?fix(ci):=20revert=20#268's=20workflow=20b?= =?UTF-8?q?umps=20=E2=80=94=20they=20drifted=20off=20actions.lock=20again?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit E2E Validation and Static Analysis Gate have been `startup_failure` on main since 554345c (#268): Dependabot bumped setup-node 7.0.0 -> 7.1.0, upload-artifact 7.0.1 -> 7.0.2, download-artifact 8.0.1 -> 8.0.2 and setup-ocaml 3.8.0 -> 3.9.0 without a lock refresh, the same failure #266 fixed two commits earlier. A ref absent from .github/workflows/actions.lock is a ref the organisation does not allow, so the workflow is rejected before any job runs. This reverses exactly #268's four workflow edits, back to the refs the lock declares. It does not prevent recurrence: the next grouped actions bump will drift again unless the lock is regenerated with it (owner decision). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- .github/workflows/c5-regenerate.yml | 2 +- .github/workflows/e2e.yml | 4 ++-- .github/workflows/release.yml | 2 +- .github/workflows/static-analysis-gate.yml | 14 +++++++------- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/.github/workflows/c5-regenerate.yml b/.github/workflows/c5-regenerate.yml index 2b1b44d..0655035 100644 --- a/.github/workflows/c5-regenerate.yml +++ b/.github/workflows/c5-regenerate.yml @@ -51,7 +51,7 @@ jobs: path: affinescript - name: Install OCaml - uses: ocaml/setup-ocaml@v3.9.0 + uses: ocaml/setup-ocaml@v3.8.0 with: ocaml-compiler: '4.14.2' diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml index eee3880..a6ec77b 100644 --- a/.github/workflows/e2e.yml +++ b/.github/workflows/e2e.yml @@ -53,7 +53,7 @@ jobs: uses: actions/checkout@v7.0.1 - name: Set up Node.js - uses: actions/setup-node@v7.1.0 + uses: actions/setup-node@v7.0.0 with: node-version: '25' @@ -158,7 +158,7 @@ jobs: # ---- Node (for smoke test within E2E script) ---- - name: Set up Node.js - uses: actions/setup-node@v7.1.0 + uses: actions/setup-node@v7.0.0 with: node-version: '25' diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 3841579..4939a2d 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -77,7 +77,7 @@ jobs: git cliff --output CHANGELOG.md - name: Upload updated CHANGELOG.md - uses: actions/upload-artifact@v7.0.2 + uses: actions/upload-artifact@v7.0.1 with: name: changelog path: CHANGELOG.md diff --git a/.github/workflows/static-analysis-gate.yml b/.github/workflows/static-analysis-gate.yml index 280523b..c1e67b8 100644 --- a/.github/workflows/static-analysis-gate.yml +++ b/.github/workflows/static-analysis-gate.yml @@ -117,7 +117,7 @@ jobs: echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload panic-attack findings - uses: actions/upload-artifact@v7.0.2 + uses: actions/upload-artifact@v7.0.1 with: name: panic-attack-findings path: panic-attack-findings.json @@ -251,7 +251,7 @@ jobs: echo "Skipped: Hypatia scanner not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload hypatia findings - uses: actions/upload-artifact@v7.0.2 + uses: actions/upload-artifact@v7.0.1 with: name: hypatia-findings path: hypatia-findings.json @@ -341,7 +341,7 @@ jobs: echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload bridge report - uses: actions/upload-artifact@v7.0.2 + uses: actions/upload-artifact@v7.0.1 with: name: bridge-report path: bridge-report.json @@ -365,19 +365,19 @@ jobs: steps: - name: Download panic-attack findings - uses: actions/download-artifact@v8.0.2 + uses: actions/download-artifact@v8.0.1 with: name: panic-attack-findings path: findings/ - name: Download hypatia findings - uses: actions/download-artifact@v8.0.2 + uses: actions/download-artifact@v8.0.1 with: name: hypatia-findings path: findings/ - name: Download bridge report - uses: actions/download-artifact@v8.0.2 + uses: actions/download-artifact@v8.0.1 with: name: bridge-report path: findings/ @@ -439,7 +439,7 @@ jobs: echo "low=$LOW" >> "$GITHUB_OUTPUT" - name: Upload unified findings (fleet scanner picks these up) - uses: actions/upload-artifact@v7.0.2 + uses: actions/upload-artifact@v7.0.1 with: name: unified-findings path: findings/unified-findings.json From 145d84b122a1eef469b416ee984f12776ccf520a Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:00:36 +0000 Subject: [PATCH 02/13] fix(test): follow the .md -> .adoc and .well-known -> www/ moves With E2E Validation able to start again, its structural and smoke jobs fail on paths that moved without the tests following (pre-existing on main, masked by the startup_failure): tests/e2e.sh LEVEL-STATUS.md -> LEVEL-STATUS.adoc, and the row pattern "| N |" (Markdown) -> "^|N |" (AsciiDoc), so all 12 rows are really checked tests/aspect/claim-envelope LEVEL-STATUS / PROOF-NEEDS / TEST-NEEDS .md -> .adoc in the RSR list and the L11/L12 cross-check tests/aspect/security-envelope .well-known/security.txt -> www/.well-known/security.txt README.adoc, ROADMAP.adoc docs/WHITEPAPER.md -> docs/WHITEPAPER.adoc Locally: tests/e2e.sh (E2E_BUILD=0) 47 passed / 0 failed (was 35 / 1), claim-envelope 57 / 0 (was 51 / 5), security-envelope 10 / 0 (was 9 / 1). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- README.adoc | 4 ++-- ROADMAP.adoc | 2 +- tests/aspect/claim-envelope.mjs | 10 +++++----- tests/aspect/security-envelope.mjs | 12 ++++++------ tests/e2e.sh | 14 +++++++------- 5 files changed, 21 insertions(+), 21 deletions(-) diff --git a/README.adoc b/README.adoc index 49c3e33..ab420f8 100644 --- a/README.adoc +++ b/README.adoc @@ -223,7 +223,7 @@ PROOF-NEEDS.md # Outstanding proof obligations TEST-NEEDS.md # Outstanding test coverage docs/PRODUCTION-PATH.adoc # 6-phase plan to production-ready docs/onboarding/README.adoc # New here? Start here. -docs/WHITEPAPER.md # Full academic treatment +docs/WHITEPAPER.adoc # Full academic treatment AUDIT.adoc # Hard rules and audit posture ---- @@ -267,7 +267,7 @@ The post-codegen verifier's `verify_access_sites_from_module` pass shipped in PR GraalVM's Truffle framework has the same multi-language shared state problem. typed-wasm's approach could give GraalVM **compile-time guarantees** for cross-language interop, replacing runtime `InteropLibrary` dispatch with -compile-time schema agreement. See `docs/WHITEPAPER.md` for details. +compile-time schema agreement. See `docs/WHITEPAPER.adoc` for details. == License diff --git a/ROADMAP.adoc b/ROADMAP.adoc index f044194..8fbf15c 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -47,7 +47,7 @@ Key capabilities delivered: * `.twasm` grammar (spec/grammar.ebnf) -- EBNF surface syntax * 10-level spec (spec/type-safety-levels-for-wasm.adoc) -- checked DB-to-WASM core mapping * Example `.twasm` files for the checked core, plus draft higher-level examples -* Whitepaper drafts (docs/WHITEPAPER.md + docs/arxiv/typed-wasm.tex) under audit +* Whitepaper drafts (docs/WHITEPAPER.adoc + docs/arxiv/typed-wasm.tex) under audit * No unsound escape hatches in the checked Idris2 core (`believe_me`, `assert_total`) * Estate-axis accommodation (A15/A16, 2026-06-16): L11/L12/Echo now cross-document and mirror the canonical estate repos -- `tropical-resource-typing` (Lean4 diff --git a/tests/aspect/claim-envelope.mjs b/tests/aspect/claim-envelope.mjs index 856db59..ff8892a 100644 --- a/tests/aspect/claim-envelope.mjs +++ b/tests/aspect/claim-envelope.mjs @@ -5,7 +5,7 @@ // Claim-envelope aspect test. // // Every claim this repo makes in human-readable docs (README.adoc, -// ROADMAP.adoc, LEVEL-STATUS.md, EXPLAINME.adoc) is also a contract with +// ROADMAP.adoc, LEVEL-STATUS.adoc, EXPLAINME.adoc) is also a contract with // the artefacts it ships (src/abi/typed-wasm.ipkg, src/parser/*, Rust // crate constants, CI toolchain pins). When docs and artefacts drift, // nobody notices until an audit week later. @@ -106,7 +106,7 @@ function assertDocsAgreeOnL11L12(path, regex) { const stalePattern = /L11.{0,4}L12[^\n]{0,180}?(not part of|not in.*(?:package|ipkg)|standalone.*fail)/i; assertDocsAgreeOnL11L12("ROADMAP.adoc", stalePattern); -assertDocsAgreeOnL11L12("LEVEL-STATUS.md", stalePattern); +assertDocsAgreeOnL11L12("LEVEL-STATUS.adoc", stalePattern); assertDocsAgreeOnL11L12("README.adoc", stalePattern); // ---------------------------------------------------------------------- @@ -318,10 +318,10 @@ const rsrFiles = [ "LICENSE", "Justfile", "0-AI-MANIFEST.a2ml", - "LEVEL-STATUS.md", + "LEVEL-STATUS.adoc", "ROADMAP.adoc", - "PROOF-NEEDS.md", - "TEST-NEEDS.md", + "PROOF-NEEDS.adoc", + "TEST-NEEDS.adoc", "docs/PRODUCTION-PATH.adoc", // canonical strategic plan (added 2026-05-24) "docs/onboarding/README.adoc", // RSR taxonomy (added 2026-05-25) "docs/status/README.adoc", // RSR taxonomy (added 2026-05-25) diff --git a/tests/aspect/security-envelope.mjs b/tests/aspect/security-envelope.mjs index 743c249..27d1377 100644 --- a/tests/aspect/security-envelope.mjs +++ b/tests/aspect/security-envelope.mjs @@ -8,7 +8,7 @@ // checks that human-readable doc claims match shipped artefacts in // general, this file specifically checks SECURITY claims: // -// - SECURITY.md contact email matches .well-known/security.txt +// - SECURITY.md contact email matches www/.well-known/security.txt // - SPDX-License-Identifier headers present on all source files // - "believe_me: 0" README badge matches actual code (not comments) // - No committed secrets / private keys @@ -58,15 +58,15 @@ function maybeRead(rel) { } // ---------------------------------------------------------------------- -// 1. SECURITY.md ↔ .well-known/security.txt — contact alignment +// 1. SECURITY.md ↔ www/.well-known/security.txt — contact alignment // ---------------------------------------------------------------------- -section("1. SECURITY.md and .well-known/security.txt agree on contact"); +section("1. SECURITY.md and www/.well-known/security.txt agree on contact"); const securityMd = maybeRead("SECURITY.md"); -const securityTxt = maybeRead(".well-known/security.txt"); +const securityTxt = maybeRead("www/.well-known/security.txt"); if (!securityMd) bad("SECURITY.md missing"); -if (!securityTxt) bad(".well-known/security.txt missing"); +if (!securityTxt) bad("www/.well-known/security.txt missing"); if (securityMd && securityTxt) { const mdEmail = (securityMd.match(/[\w._%+-]+@[\w.-]+\.[A-Za-z]{2,}/) || [])[0]; @@ -74,7 +74,7 @@ if (securityMd && securityTxt) { || (securityTxt.match(/[\w._%+-]+@[\w.-]+\.[A-Za-z]{2,}/) || [])[0]; if (!mdEmail) bad("SECURITY.md has no contact email"); - else if (!txtEmail) bad(".well-known/security.txt has no Contact: line"); + else if (!txtEmail) bad("www/.well-known/security.txt has no Contact: line"); else if (mdEmail.toLowerCase() !== txtEmail.toLowerCase()) { bad(`Contact email mismatch: SECURITY.md=${mdEmail} vs security.txt=${txtEmail}`); } else { diff --git a/tests/e2e.sh b/tests/e2e.sh index c9f329a..e826725 100755 --- a/tests/e2e.sh +++ b/tests/e2e.sh @@ -11,7 +11,7 @@ # 4. Zig FFI implementation files are present # 5. ReScript parser source files are present # 6. JSON/TOML/IPKG configuration files are well-formed -# 7. LEVEL-STATUS.md documents all 12 levels +# 7. LEVEL-STATUS.adoc documents all 12 levels # 8. Grammar document is non-trivial # 9. SPDX licence headers are present on key files # @@ -65,17 +65,17 @@ else fail "Missing: spec/type-safety-levels-for-wasm.adoc" fi -# LEVEL-STATUS.md documents all 12 levels -if [ -f "LEVEL-STATUS.md" ]; then +# LEVEL-STATUS.adoc documents all 12 levels (AsciiDoc table rows read "|N |...") +if [ -f "LEVEL-STATUS.adoc" ]; then for lvl in $(seq 1 12); do - if grep -q "| $lvl |" "LEVEL-STATUS.md" 2>/dev/null; then - pass "LEVEL-STATUS.md contains level $lvl" + if grep -qE "^\|${lvl} \|" "LEVEL-STATUS.adoc" 2>/dev/null; then + pass "LEVEL-STATUS.adoc contains level $lvl" else - fail "LEVEL-STATUS.md missing entry for level $lvl" + fail "LEVEL-STATUS.adoc missing entry for level $lvl" fi done else - fail "Missing: LEVEL-STATUS.md" + fail "Missing: LEVEL-STATUS.adoc" fi # Grammar document From d52729598bd93bdd0271b790291ec5d2337a8e14 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 00:59:20 +0000 Subject: [PATCH 03/13] feat(abi): port the resource-algebra grade kernel to Idris2 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit src/abi/TypedWasm/ABI/ResourceAlgebra.idr transcribes hyperpolymath/resource-algebra Core.agda @ cf9235c: the ResourceAlgebra interface (alternatives an idempotent commutative monoid, sequence a monoid), the induced order and its lemmas, and IsOrdered / IsDioid / IsAnnihilating as separate interfaces, as in Agda, with "every dioid is ordered" as dioidMonoL/R and the named implementation dioidOrdered. ResourceAlgebra/{Loss,MaxPlus,HWM}.idr transcribe Instances/*.agda clause for clause (constructors renamed fin/inf -> Finite/Infinity, val/bot -> Val/Bot, hwm -> MkHWM; clause order kept, so both sides reduce alike). Separation.idr carries the S-1..S-3 witnesses. ResourceAlgebra/Nat.idr holds only the Nat lemmas Idris2's base lacks: base's Data.Nat.minimum / maximum / LTE are the Agda Prelude's min / max / ≤ clause for clause, so they are used rather than declared again. scripts/fetch-siblings.sh fetches resource-algebra at the pin into _build/dependencies (the residual-evidence-types pattern). All laws re-proved under %default total with no believe_me / assert_total; the package builds clean under Idris2 0.8.0 (30 modules). Correspondence to the Agda source: ASSUMED (transcription). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- scripts/fetch-siblings.sh | 39 ++++ src/abi/TypedWasm/ABI/ResourceAlgebra.idr | 202 ++++++++++++++++++ src/abi/TypedWasm/ABI/ResourceAlgebra/HWM.idr | 179 ++++++++++++++++ .../TypedWasm/ABI/ResourceAlgebra/Loss.idr | 177 +++++++++++++++ .../TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr | 178 +++++++++++++++ src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr | 154 +++++++++++++ .../ABI/ResourceAlgebra/Separation.idr | 98 +++++++++ src/abi/typed-wasm.ipkg | 9 + 8 files changed, 1036 insertions(+) create mode 100755 scripts/fetch-siblings.sh create mode 100644 src/abi/TypedWasm/ABI/ResourceAlgebra.idr create mode 100644 src/abi/TypedWasm/ABI/ResourceAlgebra/HWM.idr create mode 100644 src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr create mode 100644 src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr create mode 100644 src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr create mode 100644 src/abi/TypedWasm/ABI/ResourceAlgebra/Separation.idr diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh new file mode 100755 index 0000000..20704dc --- /dev/null +++ b/scripts/fetch-siblings.sh @@ -0,0 +1,39 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Fetch the sibling proof repositories at their pinned commits +# (pattern: residual-evidence-types / choreographic-types). +# +# typed-wasm consumes these by pin, never by re-declaring their definitions: +# resource-algebra — the grade kernel; src/abi/TypedWasm/ABI/ResourceAlgebra* +# is its Idris2 transcription, and tests/transcription +# checks the operation tables against this tree in Agda. +# +# Re-pin deliberately, one commit per pin, and update the module headers that +# cite the pin in the same commit. Override for a local experiment with +# RESOURCE_ALGEBRA_COMMIT= scripts/fetch-siblings.sh +set -euo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." + +RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-cf9235c532712a783a404c359a1055f40134794a}" + +fetch() { # fetch + local name="$1" commit="$2" dir="_build/dependencies/$1" + mkdir -p _build/dependencies + if [ ! -d "$dir/.git" ]; then + git clone --quiet "https://github.com/hyperpolymath/${name}.git" "$dir" + fi + if ! git -C "$dir" cat-file -e "${commit}^{commit}" 2>/dev/null; then + git -C "$dir" fetch --quiet origin + fi + git -C "$dir" checkout --quiet --detach "$commit" + local got + got="$(git -C "$dir" rev-parse HEAD)" + case "$got" in + "$commit"*) echo "${name} at ${got}" ;; + *) echo "ERROR: ${name} resolved to ${got}, expected ${commit}" >&2; exit 1 ;; + esac +} + +fetch resource-algebra "$RESOURCE_ALGEBRA_COMMIT" diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra.idr new file mode 100644 index 0000000..8fe360a --- /dev/null +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra.idr @@ -0,0 +1,202 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- ResourceAlgebra.idr — the grade kernel of the typed-wasm ABI. +-- +-- One parametric resource algebra, three instances (Loss, MaxPlus, HWM), +-- and the witnesses that say why they must stay three. Every grade the ABI +-- carries (L11 cost, L12 staleness, L13 occupancy, L16 choreography) is +-- drawn from here; no other module defines a min-plus or max-plus algebra +-- (tools/check-grade-kernel.sh enforces that). +-- +-- PROVENANCE. Transcribed from hyperpolymath/resource-algebra +-- src/ResourceAlgebra/Core.agda @ cf9235c532712a783a404c359a1055f40134794a +-- (fetched by scripts/fetch-siblings.sh). Agda --safe --without-K is the +-- proof kernel; this Idris2 module is the ABI layer and re-proves the same +-- laws. Correspondence status: ASSUMED (transcription). The instance +-- operation tables are additionally checked on both sides, by Agda `refl` +-- against the pinned sources and by Idris2 `Refl` against this port +-- (tests/transcription). Nothing mechanical relates the two proofs. +-- +-- Transcription map (Agda -> Idris2): +-- record ResourceAlgebra (Grade field) -> interface ResourceAlgebra g +-- _⊕_ / _⊗_ / 𝟘 / 𝟙 -> oplus / otimes / zeroG / oneG +-- alt : IsAltMonoid (assoc comm idem unitˡ) -> altAssoc altComm altIdem altUnitL +-- seq : IsSeqMonoid (assoc unitˡ unitʳ) -> seqAssoc seqUnitL seqUnitR +-- _≼_ -> LeG +-- IsOrdered / IsDioid / IsAnnihilating -> interfaces of the same names +-- IsDioid.ordered -> dioidMonoL / dioidMonoR (+ the +-- named implementation dioidOrdered) +-- The two monoid records are flattened into the one interface (Idris2 has no +-- convenient way to parameterise an interface by its own operations); the +-- fields and their directions are unchanged. +-- +-- Layering, from weakest to strongest (as in Core.agda): +-- ResourceAlgebra alternatives an idempotent commutative monoid (⊕, 𝟘), +-- sequence a monoid (⊗, 𝟙). All K-CUT-LOSS needs. +-- IsOrdered ⊗ monotone for the ⊕-induced order; what a bound needs. +-- IsDioid ⊗ distributes over ⊕; every dioid is ordered (proved). +-- IsAnnihilating 𝟘 absorbs under ⊗. Separate on purpose: HWM is a dioid +-- with 𝟘 = 𝟙, so it cannot be annihilating. +-- +-- NO believe_me, NO postulate, NO assert_total. %default total. + +module TypedWasm.ABI.ResourceAlgebra + +%default total + +-- ============================================================================ +-- The algebra +-- ============================================================================ + +||| A grade algebra: alternatives form an idempotent commutative monoid +||| (`oplus`, `zeroG`); sequence forms a monoid (`otimes`, `oneG`). +public export +interface ResourceAlgebra g where + ||| Alternatives (⊕). + oplus : g -> g -> g + ||| Sequence (⊗). + otimes : g -> g -> g + ||| Unit of alternatives (𝟘). + zeroG : g + ||| Unit of sequence (𝟙). + oneG : g + -- IsAltMonoid oplus zeroG + altAssoc : (a, b, c : g) -> oplus (oplus a b) c = oplus a (oplus b c) + altComm : (a, b : g) -> oplus a b = oplus b a + altIdem : (a : g) -> oplus a a = a + altUnitL : (a : g) -> oplus zeroG a = a + -- IsSeqMonoid otimes oneG + seqAssoc : (a, b, c : g) -> otimes (otimes a b) c = otimes a (otimes b c) + seqUnitL : (a : g) -> otimes oneG a = a + seqUnitR : (a : g) -> otimes a oneG = a + +||| Agda `IsAltMonoid.unitʳ`. +public export +altUnitR : ResourceAlgebra g => (a : g) -> oplus a (zeroG {g}) = a +altUnitR a = trans (altComm a zeroG) (altUnitL a) + +-- ============================================================================ +-- The induced order: a ≼ b when b absorbs a +-- ============================================================================ +-- +-- Which way it runs numerically is instance-specific (Separation.idr): in +-- MaxPlus 1 ≼ 2; in Loss the numerically smaller grade is ABOVE. + +||| Agda `_≼_`. +public export +LeG : ResourceAlgebra g => g -> g -> Type +LeG a b = oplus a b = b + +||| Agda `≼-refl`. +public export +leRefl : ResourceAlgebra g => (a : g) -> LeG a a +leRefl a = altIdem a + +||| Agda `≼-trans`. +public export +leTrans : ResourceAlgebra g => {a, b, c : g} -> LeG a b -> LeG b c -> LeG a c +leTrans {a} {b} {c} p q = + trans (cong (oplus a) (sym q)) + (trans (sym (altAssoc a b c)) + (trans (cong (\x => oplus x c) p) q)) + +||| Agda `≼-antisym`. +public export +leAntisym : ResourceAlgebra g => {a, b : g} -> LeG a b -> LeG b a -> a = b +leAntisym {a} {b} p q = trans (sym q) (trans (altComm b a) p) + +||| Agda `𝟘-least`. +public export +zeroLeast : ResourceAlgebra g => (a : g) -> LeG (zeroG {g}) a +zeroLeast a = altUnitL a + +||| Agda `⊕-upperˡ`. +public export +oplusUpperL : ResourceAlgebra g => (a, b : g) -> LeG a (oplus a b) +oplusUpperL a b = + trans (sym (altAssoc a a b)) (cong (\x => oplus x b) (altIdem a)) + +||| Agda `⊕-upperʳ`. +public export +oplusUpperR : ResourceAlgebra g => (a, b : g) -> LeG b (oplus a b) +oplusUpperR a b = + trans (cong (oplus b) (altComm a b)) + (trans (sym (altAssoc b b a)) + (trans (cong (\x => oplus x a) (altIdem b)) + (altComm b a))) + +||| Agda `⊕-interchange`. +public export +oplusInterchange : ResourceAlgebra g => (a, b, c, d : g) -> + oplus (oplus a b) (oplus c d) = oplus (oplus a c) (oplus b d) +oplusInterchange a b c d = + trans (altAssoc a b (oplus c d)) + (trans (cong (oplus a) + (trans (sym (altAssoc b c d)) + (trans (cong (\x => oplus x d) (altComm b c)) + (altAssoc c b d)))) + (sym (altAssoc a c (oplus b d)))) + +||| Alternatives are monotone in every resource algebra. Agda `⊕-mono`. +public export +oplusMono : ResourceAlgebra g => {a, a', b, b' : g} -> + LeG a a' -> LeG b b' -> LeG (oplus a b) (oplus a' b') +oplusMono {a} {a'} {b} {b'} p q = + trans (oplusInterchange a b a' b') (cong2 oplus p q) + +-- ============================================================================ +-- IsOrdered — sequencing is monotone +-- ============================================================================ + +||| Agda `IsOrdered`. +public export +interface ResourceAlgebra g => IsOrdered g where + otimesMonoL : (c : g) -> {a, b : g} -> LeG a b -> LeG (otimes c a) (otimes c b) + otimesMonoR : (c : g) -> {a, b : g} -> LeG a b -> LeG (otimes a c) (otimes b c) + +||| Agda `IsOrdered.⊗-mono`. +public export +otimesMono : IsOrdered g => {a, a', b, b' : g} -> + LeG a a' -> LeG b b' -> LeG (otimes a b) (otimes a' b') +otimesMono {a} {a'} {b} {b'} p q = leTrans (otimesMonoR b p) (otimesMonoL a' q) + +-- ============================================================================ +-- IsDioid — distributivity, and hence order +-- ============================================================================ + +||| Agda `IsDioid`. +public export +interface ResourceAlgebra g => IsDioid g where + distribL : (a, b, c : g) -> otimes a (oplus b c) = oplus (otimes a b) (otimes a c) + distribR : (a, b, c : g) -> otimes (oplus a b) c = oplus (otimes a c) (otimes b c) + +||| Distributivity gives left monotonicity outright. Agda `IsDioid.ordered` +||| (its ⊗-monoˡ field). +public export +dioidMonoL : IsDioid g => (c : g) -> {a, b : g} -> LeG a b -> LeG (otimes c a) (otimes c b) +dioidMonoL c {a} {b} p = trans (sym (distribL c a b)) (cong (otimes c) p) + +||| Agda `IsDioid.ordered` (its ⊗-monoʳ field). +public export +dioidMonoR : IsDioid g => (c : g) -> {a, b : g} -> LeG a b -> LeG (otimes a c) (otimes b c) +dioidMonoR c {a} {b} p = trans (sym (distribR a b c)) (cong (\x => otimes x c) p) + +||| Every dioid is ordered — Agda `IsDioid.ordered : IsOrdered R`, as a named +||| implementation (so it is available with `using`, but never competes with +||| an instance's own `IsOrdered` during search). +public export +[dioidOrdered] IsDioid g => IsOrdered g where + otimesMonoL = dioidMonoL + otimesMonoR = dioidMonoR + +-- ============================================================================ +-- IsAnnihilating — 𝟘 absorbs under ⊗ +-- ============================================================================ + +||| Agda `IsAnnihilating`. Independent of IsDioid: Instances/HWM is a dioid +||| with no annihilating zero (tests/reject/HWMAnnihilates.idr is the control). +public export +interface ResourceAlgebra g => IsAnnihilating g where + annihilL : (a : g) -> otimes (zeroG {g}) a = zeroG {g} + annihilR : (a : g) -> otimes a (zeroG {g}) = zeroG {g} diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/HWM.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/HWM.idr new file mode 100644 index 0000000..6335061 --- /dev/null +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/HWM.idr @@ -0,0 +1,179 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- ResourceAlgebra/HWM.idr — the occupancy grade: high-water mark (peak, drift). +-- +-- STATUS (inherited from the source): DESIGNED as occupancy-types' algebra +-- (resource-algebra H-2); PROVEN against the definition below. +-- +-- Transcribed from hyperpolymath/resource-algebra +-- src/ResourceAlgebra/Instances/HWM.agda @ cf9235c532712a783a404c359a1055f40134794a +-- Correspondence status: ASSUMED (transcription); operation table TESTED on +-- both sides by tests/transcription. occupancy-types @ af95728 builds its +-- reclamation law (OccupancyTypes/Reclaim.agda) on that same Agda module. +-- +-- The model: a grade records the peak live state reached during a run and +-- the drift (live state still held at the end). Sequencing b after a starts +-- b from a's drift, so the peak of a;b is max (peak a) (drift a + peak b) — +-- this is where an occupancy bound stops being a cost bound (a cost would add +-- the peaks). Drift is non-negative (drift ≤ peak is a field); a signed drift +-- is a recorded extension upstream (H-2). +-- +-- Renaming: constructor hwm is MkHWM; _⊗h_ / _⊕h_ / 𝟘h are hwmSeq / hwmAlt / +-- hwmZero. +-- +-- NO believe_me, NO postulate, NO assert_total. %default total. + +module TypedWasm.ABI.ResourceAlgebra.HWM + +-- Re-exported so a consumer can REDUCE these grades at type level (the +-- definitions below unfold to Data.Nat and to ResourceAlgebra.Nat's lemmas). +import public Data.Nat +import TypedWasm.ABI.ResourceAlgebra +import public TypedWasm.ABI.ResourceAlgebra.Nat + +%default total + +||| A high-water-mark grade. Agda `record Grade` (constructor `hwm`). +public export +record HWMGrade where + constructor MkHWM + ||| Peak live state reached during the run. + peak : Nat + ||| Live state still held at the end of the run. + drift : Nat + ||| A run cannot end holding more than its peak. + bounded : LTE drift peak + +||| A grade is determined by peak and drift. Agda `hwm-≡`. +public export +hwmEq : {p, p', n, n' : Nat} -> {b : LTE n p} -> {b' : LTE n' p'} -> + p = p' -> n = n' -> MkHWM p n b = MkHWM p' n' b' +hwmEq {b} {b'} Refl Refl = cong (MkHWM _ _) (lteIrrelevant b b') + +-- ============================================================================ +-- Operations +-- ============================================================================ + +||| Sequence: the suffix starts from the prefix's drift. Agda `_⊗h_`. +public export +hwmSeq : HWMGrade -> HWMGrade -> HWMGrade +hwmSeq (MkHWM p1 n1 b1) (MkHWM p2 n2 b2) = + MkHWM (maximum p1 (n1 + p2)) (n1 + n2) + (lteTrans (plusMonoRLTE n1 b2) (maximumRightUpperBound p1 (n1 + p2))) + +||| Alternatives: componentwise max. Agda `_⊕h_`. +public export +hwmAlt : HWMGrade -> HWMGrade -> HWMGrade +hwmAlt (MkHWM p1 n1 b1) (MkHWM p2 n2 b2) = + MkHWM (maximum p1 p2) (maximum n1 n2) (maxMonoLTE b1 b2) + +||| Nothing allocated, nothing held: both units. Agda `𝟘h`. +public export +hwmZero : HWMGrade +hwmZero = MkHWM 0 0 LTEZero + +-- ============================================================================ +-- Alternatives: componentwise max +-- ============================================================================ + +||| Agda `⊕h-assoc`. +public export +hwmAltAssoc : (a, b, c : HWMGrade) -> hwmAlt (hwmAlt a b) c = hwmAlt a (hwmAlt b c) +hwmAltAssoc (MkHWM p n _) (MkHWM p' n' _) (MkHWM p'' n'' _) = + hwmEq (maxAssoc p p' p'') (maxAssoc n n' n'') + +||| Agda `⊕h-comm`. +public export +hwmAltComm : (a, b : HWMGrade) -> hwmAlt a b = hwmAlt b a +hwmAltComm (MkHWM p n _) (MkHWM p' n' _) = + hwmEq (maximumCommutative p p') (maximumCommutative n n') + +||| Agda `⊕h-idem`. +public export +hwmAltIdem : (a : HWMGrade) -> hwmAlt a a = a +hwmAltIdem (MkHWM p n _) = hwmEq (maximumIdempotent p) (maximumIdempotent n) + +||| Agda `⊕h-unitˡ`. +public export +hwmAltUnitL : (a : HWMGrade) -> hwmAlt HWM.hwmZero a = a +hwmAltUnitL (MkHWM p n _) = hwmEq Refl Refl + +-- ============================================================================ +-- Sequence +-- ============================================================================ + +||| Agda `⊗h-assoc`. +public export +hwmSeqAssoc : (a, b, c : HWMGrade) -> hwmSeq (hwmSeq a b) c = hwmSeq a (hwmSeq b c) +hwmSeqAssoc (MkHWM p1 n1 _) (MkHWM p2 n2 _) (MkHWM p3 n3 _) = + hwmEq + (trans (cong (maximum (maximum p1 (n1 + p2))) (plusAssoc n1 n2 p3)) + (trans (maxAssoc p1 (n1 + p2) (n1 + (n2 + p3))) + (cong (maximum p1) (sym (plusDistribLMax n1 p2 (n2 + p3)))))) + (plusAssoc n1 n2 n3) + +||| Agda `⊗h-unitˡ`. +public export +hwmSeqUnitL : (a : HWMGrade) -> hwmSeq HWM.hwmZero a = a +hwmSeqUnitL (MkHWM p n _) = hwmEq Refl Refl + +||| Agda `⊗h-unitʳ`. +public export +hwmSeqUnitR : (a : HWMGrade) -> hwmSeq a HWM.hwmZero = a +hwmSeqUnitR (MkHWM p n b) = + hwmEq (trans (cong (maximum p) (plusZeroRightNeutral n)) (maxAbsorbLTE b)) + (plusZeroRightNeutral n) + +-- ============================================================================ +-- The instance, and its layers +-- ============================================================================ + +||| Agda `HWM : ResourceAlgebra`. 𝟘 and 𝟙 are the same grade. +public export +ResourceAlgebra HWMGrade where + oplus = hwmAlt + otimes = hwmSeq + zeroG = hwmZero + oneG = hwmZero + altAssoc = hwmAltAssoc + altComm = hwmAltComm + altIdem = hwmAltIdem + altUnitL = hwmAltUnitL + seqAssoc = hwmSeqAssoc + seqUnitL = hwmSeqUnitL + seqUnitR = hwmSeqUnitR + +||| Agda `HWM-dioid` (distribˡ). +public export +hwmDistribL : (a, b, c : HWMGrade) -> + hwmSeq a (hwmAlt b c) = hwmAlt (hwmSeq a b) (hwmSeq a c) +hwmDistribL (MkHWM p n _) (MkHWM p2 n2 _) (MkHWM p3 n3 _) = + hwmEq (trans (cong (maximum p) (plusDistribLMax n p2 p3)) + (sym (maxDup p (n + p2) (n + p3)))) + (plusDistribLMax n n2 n3) + +||| Agda `HWM-dioid` (distribʳ). +public export +hwmDistribR : (a, b, c : HWMGrade) -> + hwmSeq (hwmAlt a b) c = hwmAlt (hwmSeq a c) (hwmSeq b c) +hwmDistribR (MkHWM p2 n2 _) (MkHWM p3 n3 _) (MkHWM p n _) = + hwmEq (trans (cong (maximum (maximum p2 p3)) (plusDistribRMax n2 n3 p)) + (maxInterchange p2 p3 (n2 + p) (n3 + p))) + (plusDistribRMax n2 n3 n) + +||| Agda `HWM-dioid`. +public export +IsDioid HWMGrade where + distribL = hwmDistribL + distribR = hwmDistribR + +||| Agda `HWM-ordered = IsDioid.ordered HWM-dioid`. +public export +IsOrdered HWMGrade where + otimesMonoL = dioidMonoL + otimesMonoR = dioidMonoR + +-- There is NO `IsAnnihilating HWMGrade`: hwmZero is also the sequence unit, +-- so hwmSeq hwmZero a = a, not hwmZero. +-- tests/reject/HWMAnnihilates.idr is the negative control. diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr new file mode 100644 index 0000000..8d97bca --- /dev/null +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr @@ -0,0 +1,177 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- ResourceAlgebra/Loss.idr — the loss grade: min-plus on ℕ ∪ {∞}. +-- +-- THE ONE DEFINITION OF MIN-PLUS IN THIS TREE (tools/check-grade-kernel.sh). +-- TypedWasm.ABI.Tropical's latency cost (TropCost) and TypedWasm.ABI.Echo's +-- loss grade are this carrier, not copies of it. +-- +-- Transcribed from hyperpolymath/resource-algebra +-- src/ResourceAlgebra/Instances/Loss.agda @ cf9235c532712a783a404c359a1055f40134794a +-- which is itself the echo-types loss grade +-- (echo-types experimental/echo-additive/Grade.agda). +-- Correspondence status: ASSUMED (transcription); operation table TESTED on +-- both sides by tests/transcription. +-- +-- Renaming (the only change from the Agda text): constructors fin / inf are +-- Finite / Infinity, the names typed-wasm's L11/L12 code already uses; +-- _⊓g_ / _+g_ are lossAlt / lossSeq. Clause order is kept, so the two +-- definitions reduce the same way on the same arguments. +-- +-- Grade = ℕ ∪ {∞}; Finite 0 = no loss (echo `keep`); Infinity = total collapse. +-- lossSeq = sequence (loss accumulates, ∞ absorbs) — the "⊗" +-- lossAlt = alternatives = MIN (the less lossy option) — the "⊕" +-- +-- NO believe_me, NO postulate, NO assert_total. %default total. + +module TypedWasm.ABI.ResourceAlgebra.Loss + +-- Re-exported so a consumer can REDUCE these grades at type level (the +-- definitions below unfold to Data.Nat's minimum / maximum and +). +import public Data.Nat +import TypedWasm.ABI.ResourceAlgebra +import TypedWasm.ABI.ResourceAlgebra.Nat + +%default total + +||| ℕ ∪ {∞}. Agda `Grade` (fin / inf). +public export +data LossGrade : Type where + ||| A finite loss (Agda `fin`). + Finite : (n : Nat) -> LossGrade + ||| Total collapse / unreachable (Agda `inf`). + Infinity : LossGrade + +||| Sequence: loss accumulates. Agda `_+g_`. +public export +lossSeq : LossGrade -> LossGrade -> LossGrade +lossSeq (Finite m) (Finite n) = Finite (m + n) +lossSeq (Finite _) Infinity = Infinity +lossSeq Infinity _ = Infinity + +||| Alternatives: the less lossy option. Agda `_⊓g_`. +public export +lossAlt : LossGrade -> LossGrade -> LossGrade +lossAlt (Finite m) (Finite n) = Finite (minimum m n) +lossAlt (Finite m) Infinity = Finite m +lossAlt Infinity g = g + +||| `Finite` is injective. +public export +finiteInjective : {m, n : Nat} -> Finite m = Finite n -> m = n +finiteInjective Refl = Refl + +-- ============================================================================ +-- Alternatives: (lossAlt, Infinity) is an idempotent commutative monoid +-- ============================================================================ + +||| Agda `⊓g-assoc`. +public export +lossAltAssoc : (a, b, c : LossGrade) -> + lossAlt (lossAlt a b) c = lossAlt a (lossAlt b c) +lossAltAssoc (Finite a) (Finite b) (Finite c) = cong Finite (minAssoc a b c) +lossAltAssoc (Finite a) (Finite b) Infinity = Refl +lossAltAssoc (Finite a) Infinity c = Refl +lossAltAssoc Infinity b c = Refl + +||| Agda `⊓g-comm`. +public export +lossAltComm : (a, b : LossGrade) -> lossAlt a b = lossAlt b a +lossAltComm (Finite a) (Finite b) = cong Finite (minimumCommutative a b) +lossAltComm (Finite a) Infinity = Refl +lossAltComm Infinity (Finite b) = Refl +lossAltComm Infinity Infinity = Refl + +||| Agda `⊓g-idem`. +public export +lossAltIdem : (a : LossGrade) -> lossAlt a a = a +lossAltIdem (Finite a) = cong Finite (minimumIdempotent a) +lossAltIdem Infinity = Refl + +-- ============================================================================ +-- Sequence: (lossSeq, Finite 0) is a monoid +-- ============================================================================ + +||| Agda `+g-assoc`. +public export +lossSeqAssoc : (a, b, c : LossGrade) -> + lossSeq (lossSeq a b) c = lossSeq a (lossSeq b c) +lossSeqAssoc (Finite a) (Finite b) (Finite c) = cong Finite (plusAssoc a b c) +lossSeqAssoc (Finite a) (Finite b) Infinity = Refl +lossSeqAssoc (Finite a) Infinity c = Refl +lossSeqAssoc Infinity b c = Refl + +||| Agda `+g-unitˡ`. +public export +lossSeqUnitL : (a : LossGrade) -> lossSeq (Finite 0) a = a +lossSeqUnitL (Finite a) = Refl +lossSeqUnitL Infinity = Refl + +||| Agda `+g-unitʳ`. +public export +lossSeqUnitR : (a : LossGrade) -> lossSeq a (Finite 0) = a +lossSeqUnitR (Finite a) = cong Finite (plusZeroRightNeutral a) +lossSeqUnitR Infinity = Refl + +-- ============================================================================ +-- The instance, and its layers +-- ============================================================================ + +||| Agda `Loss : ResourceAlgebra`. +public export +ResourceAlgebra LossGrade where + oplus = lossAlt + otimes = lossSeq + zeroG = Infinity + oneG = Finite 0 + altAssoc = lossAltAssoc + altComm = lossAltComm + altIdem = lossAltIdem + altUnitL = \_ => Refl + seqAssoc = lossSeqAssoc + seqUnitL = lossSeqUnitL + seqUnitR = lossSeqUnitR + +||| Agda `Loss-dioid` (distribˡ). +public export +lossDistribL : (a, b, c : LossGrade) -> + lossSeq a (lossAlt b c) = lossAlt (lossSeq a b) (lossSeq a c) +lossDistribL (Finite a) (Finite b) (Finite c) = cong Finite (plusDistribLMin a b c) +lossDistribL (Finite a) (Finite b) Infinity = Refl +lossDistribL (Finite a) Infinity c = Refl +lossDistribL Infinity b c = Refl + +||| Agda `Loss-dioid` (distribʳ). +public export +lossDistribR : (a, b, c : LossGrade) -> + lossSeq (lossAlt a b) c = lossAlt (lossSeq a c) (lossSeq b c) +lossDistribR (Finite a) (Finite b) (Finite c) = cong Finite (plusDistribRMin a b c) +lossDistribR (Finite a) (Finite b) Infinity = Refl +lossDistribR (Finite a) Infinity (Finite c) = Refl +lossDistribR (Finite a) Infinity Infinity = Refl +lossDistribR Infinity b c = Refl + +||| Agda `Loss-dioid`. +public export +IsDioid LossGrade where + distribL = lossDistribL + distribR = lossDistribR + +||| Agda `Loss-ordered = IsDioid.ordered Loss-dioid`. +public export +IsOrdered LossGrade where + otimesMonoL = dioidMonoL + otimesMonoR = dioidMonoR + +||| Agda `Loss-annihilating` (annihilʳ). +public export +lossAnnihilR : (a : LossGrade) -> lossSeq a Infinity = Infinity +lossAnnihilR (Finite _) = Refl +lossAnnihilR Infinity = Refl + +||| Agda `Loss-annihilating`. +public export +IsAnnihilating LossGrade where + annihilL = \_ => Refl + annihilR = lossAnnihilR diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr new file mode 100644 index 0000000..5a85c42 --- /dev/null +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr @@ -0,0 +1,178 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- ResourceAlgebra/MaxPlus.idr — the worst-case cost grade: max-plus on ℕ ∪ {−∞}. +-- +-- THE ONE DEFINITION OF MAX-PLUS IN THIS TREE (tools/check-grade-kernel.sh). +-- +-- Transcribed from hyperpolymath/resource-algebra +-- src/ResourceAlgebra/Instances/MaxPlus.agda @ cf9235c532712a783a404c359a1055f40134794a +-- which is itself the tropical-types grade (TropicalSessionTypes.lean). +-- Correspondence status: ASSUMED (transcription); operation table TESTED on +-- both sides by tests/transcription. The Lean bridge (resource-algebra M-2) +-- stays OPEN: nothing mechanical links Lean, Agda and this module. +-- +-- Renaming: constructors val / bot are Val / Bot; tAdd / tMul are +-- maxPlusAlt / maxPlusSeq. Clause order is kept. +-- +-- Grade = ℕ ∪ {−∞}; Bot = −∞ +-- maxPlusAlt = max with Bot as identity — alternatives, the "⊕" +-- maxPlusSeq = + with Bot absorbing — sequence, the "⊗", unit Val 0 +-- +-- NO believe_me, NO postulate, NO assert_total. %default total. + +module TypedWasm.ABI.ResourceAlgebra.MaxPlus + +-- Re-exported so a consumer can REDUCE these grades at type level (the +-- definitions below unfold to Data.Nat's minimum / maximum and +). +import public Data.Nat +import TypedWasm.ABI.ResourceAlgebra +import TypedWasm.ABI.ResourceAlgebra.Nat + +%default total + +||| ℕ ∪ {−∞}. Agda `Tropical` (val / bot). +public export +data MaxPlusGrade : Type where + ||| A finite cost (Agda `val`). + Val : (n : Nat) -> MaxPlusGrade + ||| −∞: no run (Agda `bot`). + Bot : MaxPlusGrade + +||| Alternatives: the more expensive branch. Agda `tAdd`. +public export +maxPlusAlt : MaxPlusGrade -> MaxPlusGrade -> MaxPlusGrade +maxPlusAlt Bot b = b +maxPlusAlt (Val m) Bot = Val m +maxPlusAlt (Val m) (Val n) = Val (maximum m n) + +||| Sequence: costs add. Agda `tMul`. +public export +maxPlusSeq : MaxPlusGrade -> MaxPlusGrade -> MaxPlusGrade +maxPlusSeq Bot _ = Bot +maxPlusSeq (Val m) Bot = Bot +maxPlusSeq (Val m) (Val n) = Val (m + n) + +||| `Val` is injective. +public export +valInjective : {m, n : Nat} -> Val m = Val n -> m = n +valInjective Refl = Refl + +-- ============================================================================ +-- Alternatives: (maxPlusAlt, Bot) is an idempotent commutative monoid +-- ============================================================================ + +||| Agda `tAdd-assoc`. +public export +maxPlusAltAssoc : (a, b, c : MaxPlusGrade) -> + maxPlusAlt (maxPlusAlt a b) c = maxPlusAlt a (maxPlusAlt b c) +maxPlusAltAssoc (Val a) (Val b) (Val c) = cong Val (maxAssoc a b c) +maxPlusAltAssoc (Val a) (Val b) Bot = Refl +maxPlusAltAssoc (Val a) Bot c = Refl +maxPlusAltAssoc Bot b c = Refl + +||| Agda `tAdd-comm`. +public export +maxPlusAltComm : (a, b : MaxPlusGrade) -> maxPlusAlt a b = maxPlusAlt b a +maxPlusAltComm (Val a) (Val b) = cong Val (maximumCommutative a b) +maxPlusAltComm (Val a) Bot = Refl +maxPlusAltComm Bot (Val b) = Refl +maxPlusAltComm Bot Bot = Refl + +||| Agda `tAdd-idem`. +public export +maxPlusAltIdem : (a : MaxPlusGrade) -> maxPlusAlt a a = a +maxPlusAltIdem (Val a) = cong Val (maximumIdempotent a) +maxPlusAltIdem Bot = Refl + +-- ============================================================================ +-- Sequence: (maxPlusSeq, Val 0) is a monoid +-- ============================================================================ + +||| Agda `tMul-assoc`. +public export +maxPlusSeqAssoc : (a, b, c : MaxPlusGrade) -> + maxPlusSeq (maxPlusSeq a b) c = maxPlusSeq a (maxPlusSeq b c) +maxPlusSeqAssoc (Val a) (Val b) (Val c) = cong Val (plusAssoc a b c) +maxPlusSeqAssoc (Val a) (Val b) Bot = Refl +maxPlusSeqAssoc (Val a) Bot c = Refl +maxPlusSeqAssoc Bot b c = Refl + +||| Agda `tMul-unitˡ`. +public export +maxPlusSeqUnitL : (a : MaxPlusGrade) -> maxPlusSeq (Val 0) a = a +maxPlusSeqUnitL (Val a) = Refl +maxPlusSeqUnitL Bot = Refl + +||| Agda `tMul-unitʳ`. +public export +maxPlusSeqUnitR : (a : MaxPlusGrade) -> maxPlusSeq a (Val 0) = a +maxPlusSeqUnitR (Val a) = cong Val (plusZeroRightNeutral a) +maxPlusSeqUnitR Bot = Refl + +-- ============================================================================ +-- The instance, and its layers +-- ============================================================================ + +||| Agda `MaxPlus : ResourceAlgebra`. +public export +ResourceAlgebra MaxPlusGrade where + oplus = maxPlusAlt + otimes = maxPlusSeq + zeroG = Bot + oneG = Val 0 + altAssoc = maxPlusAltAssoc + altComm = maxPlusAltComm + altIdem = maxPlusAltIdem + altUnitL = \_ => Refl + seqAssoc = maxPlusSeqAssoc + seqUnitL = maxPlusSeqUnitL + seqUnitR = maxPlusSeqUnitR + +||| Agda `MaxPlus-dioid` (distribˡ). +public export +maxPlusDistribL : (a, b, c : MaxPlusGrade) -> + maxPlusSeq a (maxPlusAlt b c) + = maxPlusAlt (maxPlusSeq a b) (maxPlusSeq a c) +maxPlusDistribL (Val a) (Val b) (Val c) = cong Val (plusDistribLMax a b c) +maxPlusDistribL (Val a) (Val b) Bot = Refl +maxPlusDistribL (Val a) Bot (Val c) = Refl +maxPlusDistribL (Val a) Bot Bot = Refl +maxPlusDistribL Bot b c = Refl + +||| Agda `MaxPlus-dioid` (distribʳ). +public export +maxPlusDistribR : (a, b, c : MaxPlusGrade) -> + maxPlusSeq (maxPlusAlt a b) c + = maxPlusAlt (maxPlusSeq a c) (maxPlusSeq b c) +maxPlusDistribR (Val a) (Val b) (Val c) = cong Val (plusDistribRMax a b c) +maxPlusDistribR (Val a) (Val b) Bot = Refl +maxPlusDistribR (Val a) Bot (Val c) = Refl +maxPlusDistribR (Val a) Bot Bot = Refl +maxPlusDistribR Bot (Val b) (Val c) = Refl +maxPlusDistribR Bot (Val b) Bot = Refl +maxPlusDistribR Bot Bot c = Refl + +||| Agda `MaxPlus-dioid`. +public export +IsDioid MaxPlusGrade where + distribL = maxPlusDistribL + distribR = maxPlusDistribR + +||| Agda `MaxPlus-ordered = IsDioid.ordered MaxPlus-dioid`. +public export +IsOrdered MaxPlusGrade where + otimesMonoL = dioidMonoL + otimesMonoR = dioidMonoR + +||| Agda `MaxPlus-annihilating` (annihilʳ). +public export +maxPlusAnnihilR : (a : MaxPlusGrade) -> maxPlusSeq a Bot = Bot +maxPlusAnnihilR (Val _) = Refl +maxPlusAnnihilR Bot = Refl + +||| Agda `MaxPlus-annihilating`. +public export +IsAnnihilating MaxPlusGrade where + annihilL = \_ => Refl + annihilR = maxPlusAnnihilR diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr new file mode 100644 index 0000000..85d5761 --- /dev/null +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr @@ -0,0 +1,154 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- ResourceAlgebra/Nat.idr — the ℕ lemmas the grade kernel's instances need. +-- +-- Transcribed from hyperpolymath/resource-algebra +-- src/ResourceAlgebra/Prelude.agda @ cf9235c532712a783a404c359a1055f40134794a +-- Correspondence status: ASSUMED (transcription). +-- +-- The Agda development is builtins-only, so it defines its own `max`, `min` +-- and `_≤_`. Idris2's base library already has the same definitions, clause +-- for clause: `Data.Nat.maximum`, `Data.Nat.minimum` (structural on Z/S) and +-- `LTE` (LTEZero/LTESucc). They are used here instead of being declared a +-- second time, together with base's associativity / commutativity / +-- idempotence / upper-bound lemmas. This module holds only what base lacks. +-- +-- Direction note: base states associativity as l ∘ (c ∘ r) = (l ∘ c) ∘ r, +-- the Agda Prelude as (m ∘ n) ∘ p ≡ m ∘ (n ∘ p). `maxAssoc` below is the +-- Agda direction, so the proofs that follow read line-for-line like Agda's. +-- +-- NO believe_me, NO postulate, NO assert_total. %default total. + +module TypedWasm.ABI.ResourceAlgebra.Nat + +import Data.Nat + +%default total + +-- ============================================================================ +-- Order on ℕ — Prelude.agda §order +-- ============================================================================ + +||| Agda `≤-refl`. +public export +lteRefl : (n : Nat) -> LTE n n +lteRefl Z = LTEZero +lteRefl (S n) = LTESucc (lteRefl n) + +||| Agda `≤-trans`. +public export +lteTrans : {m, n, p : Nat} -> LTE m n -> LTE n p -> LTE m p +lteTrans LTEZero _ = LTEZero +lteTrans (LTESucc q) (LTESucc r) = LTESucc (lteTrans q r) + +||| Agda `+-monoʳ-≤`. +public export +plusMonoRLTE : (m : Nat) -> {n, p : Nat} -> LTE n p -> LTE (m + n) (m + p) +plusMonoRLTE Z q = q +plusMonoRLTE (S m) q = LTESucc (plusMonoRLTE m q) + +||| Proofs of m ≤ n are unique. Agda `≤-irrelevant` (Instances/HWM.agda). +public export +lteIrrelevant : {m, n : Nat} -> (p, q : LTE m n) -> p = q +lteIrrelevant LTEZero LTEZero = Refl +lteIrrelevant (LTESucc p) (LTESucc q) = cong LTESucc (lteIrrelevant p q) + +-- ============================================================================ +-- max (the join of the usual order on ℕ) — Prelude.agda §max +-- ============================================================================ + +||| Agda `max-assoc` (Agda's direction; base's `maximumAssociative` reversed). +public export +maxAssoc : (m, n, p : Nat) -> maximum (maximum m n) p = maximum m (maximum n p) +maxAssoc m n p = sym (maximumAssociative m n p) + +||| A join absorbs its duplicate. Agda `max-dup`. +public export +maxDup : (p, x, y : Nat) -> + maximum (maximum p x) (maximum p y) = maximum p (maximum x y) +maxDup p x y = + trans (maxAssoc p x (maximum p y)) + (trans (cong (maximum p) (sym (maxAssoc x p y))) + (trans (cong (\z => maximum p (maximum z y)) (maximumCommutative x p)) + (trans (cong (maximum p) (maxAssoc p x y)) + (trans (sym (maxAssoc p p (maximum x y))) + (cong (\z => maximum z (maximum x y)) (maximumIdempotent p)))))) + +||| Agda `max-interchange`. +public export +maxInterchange : (a, b, c, d : Nat) -> + maximum (maximum a b) (maximum c d) + = maximum (maximum a c) (maximum b d) +maxInterchange a b c d = + trans (maxAssoc a b (maximum c d)) + (trans (cong (maximum a) + (trans (sym (maxAssoc b c d)) + (trans (cong (\z => maximum z d) (maximumCommutative b c)) + (maxAssoc c b d)))) + (sym (maxAssoc a c (maximum b d)))) + +||| Agda `+-distribˡ-max`. +public export +plusDistribLMax : (a, b, c : Nat) -> a + maximum b c = maximum (a + b) (a + c) +plusDistribLMax Z b c = Refl +plusDistribLMax (S a) b c = cong S (plusDistribLMax a b c) + +||| Agda `+-distribʳ-max`. +public export +plusDistribRMax : (a, b, c : Nat) -> maximum a b + c = maximum (a + c) (b + c) +plusDistribRMax a b c = + trans (plusCommutative (maximum a b) c) + (trans (plusDistribLMax c a b) + (trans (cong (\z => maximum z (c + b)) (plusCommutative c a)) + (cong (maximum (a + c)) (plusCommutative c b)))) + +||| Agda `max-mono-≤`. +public export +maxMonoLTE : {a, a', b, b' : Nat} -> LTE a a' -> LTE b b' -> + LTE (maximum a b) (maximum a' b') +maxMonoLTE {a' = a'} LTEZero q = + lteTrans q (maximumRightUpperBound a' _) +maxMonoLTE {a' = S k} {b' = b'} (LTESucc p) LTEZero = + lteTrans (LTESucc p) (maximumLeftUpperBound (S k) b') +maxMonoLTE (LTESucc p) (LTESucc q) = LTESucc (maxMonoLTE p q) + +||| A bounded argument is absorbed by max. Agda `max-absorb-≤` +||| (Instances/HWM.agda). +public export +maxAbsorbLTE : {n, p : Nat} -> LTE n p -> maximum p n = p +maxAbsorbLTE {p} LTEZero = maximumZeroNLeft p +maxAbsorbLTE (LTESucc q) = cong S (maxAbsorbLTE q) + +-- ============================================================================ +-- min (the meet of the usual order on ℕ) — Prelude.agda §min +-- ============================================================================ + +||| Agda `min-assoc` (Agda's direction). +public export +minAssoc : (m, n, p : Nat) -> minimum (minimum m n) p = minimum m (minimum n p) +minAssoc m n p = sym (minimumAssociative m n p) + +||| Agda `+-distribˡ-min`. +public export +plusDistribLMin : (a, b, c : Nat) -> a + minimum b c = minimum (a + b) (a + c) +plusDistribLMin Z b c = Refl +plusDistribLMin (S a) b c = cong S (plusDistribLMin a b c) + +||| Agda `+-distribʳ-min`. +public export +plusDistribRMin : (a, b, c : Nat) -> minimum a b + c = minimum (a + c) (b + c) +plusDistribRMin a b c = + trans (plusCommutative (minimum a b) c) + (trans (plusDistribLMin c a b) + (trans (cong (\z => minimum z (c + b)) (plusCommutative c a)) + (cong (minimum (a + c)) (plusCommutative c b)))) + +-- ============================================================================ +-- Addition — Prelude.agda §addition (Agda's direction for associativity) +-- ============================================================================ + +||| Agda `+-assoc`. +public export +plusAssoc : (m, n, p : Nat) -> (m + n) + p = m + (n + p) +plusAssoc m n p = sym (plusAssociative m n p) diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/Separation.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/Separation.idr new file mode 100644 index 0000000..875f9fd --- /dev/null +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/Separation.idr @@ -0,0 +1,98 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- ResourceAlgebra/Separation.idr — why the three grades must stay three. +-- +-- Computed witnesses that the instances are not interchangeable. Each is +-- `Refl` plus a decidable inequality on ℕ, so each is TESTED by the +-- typechecker's evaluator, not argued in prose: +-- S-1 an occupancy bound is not a cost bound (HWM vs MaxPlus) +-- S-2 echo alternatives are MIN, tropical alternatives MAX (Loss vs MaxPlus) +-- S-3 the ⊕-induced order runs opposite ways in Loss and MaxPlus +-- +-- Transcribed from hyperpolymath/resource-algebra +-- src/ResourceAlgebra/Separation.agda @ cf9235c532712a783a404c359a1055f40134794a +-- Correspondence status: ASSUMED (transcription). +-- +-- These are the reason typed-wasm does not fold its grades into one: L11's +-- cost (MaxPlus / the Loss carrier), L12's staleness (Loss) and L13's +-- occupancy (HWM) answer different questions. +-- +-- NO believe_me, NO postulate, NO assert_total. %default total. + +module TypedWasm.ABI.ResourceAlgebra.Separation + +import Data.Nat +import TypedWasm.ABI.ResourceAlgebra +import TypedWasm.ABI.ResourceAlgebra.Loss +import TypedWasm.ABI.ResourceAlgebra.MaxPlus +import TypedWasm.ABI.ResourceAlgebra.HWM + +%default total + +-- ============================================================================ +-- S-1 Sequencing peaks 2 and 3 (nothing held between them): +-- occupancy gives 3, cost gives 5. +-- ============================================================================ + +public export +two : HWMGrade +two = MkHWM 2 0 LTEZero + +public export +three : HWMGrade +three = MkHWM 3 0 LTEZero + +public export +hwmSeqPeak : peak (hwmSeq Separation.two Separation.three) = 3 +hwmSeqPeak = Refl + +public export +maxPlusSeqCost : maxPlusSeq (Val 2) (Val 3) = Val 5 +maxPlusSeqCost = Refl + +public export +threeNotFive : Not (the Nat 3 = 5) +threeNotFive Refl impossible + +||| Agda `occupancy-is-not-cost`. +public export +occupancyIsNotCost : Not (peak (hwmSeq Separation.two Separation.three) = 5) +occupancyIsNotCost = threeNotFive + +-- ============================================================================ +-- S-2 Alternatives: echo picks the less lossy branch (min), tropical the +-- most expensive (max). Same numbers, different grade. +-- ============================================================================ + +public export +lossAltPicksMin : lossAlt (Finite 2) (Finite 3) = Finite 2 +lossAltPicksMin = Refl + +public export +maxPlusAltPicksMax : maxPlusAlt (Val 2) (Val 3) = Val 3 +maxPlusAltPicksMax = Refl + +public export +twoNotThree : Not (the Nat 2 = 3) +twoNotThree Refl impossible + +||| Agda `alternatives-differ`. +public export +alternativesDiffer : Not (lossAlt (Finite 2) (Finite 3) = Finite 3) +alternativesDiffer p = twoNotThree (finiteInjective p) + +-- ============================================================================ +-- S-3 The induced order: in MaxPlus 1 is below 2; in Loss 2 is below 1 +-- (the numerically smaller loss is the one that absorbs). +-- ============================================================================ + +||| Agda `maxplus-order`. +public export +maxPlusOrder : LeG (Val 1) (Val 2) +maxPlusOrder = Refl + +||| Agda `loss-order-reversed`. +public export +lossOrderReversed : LeG (Finite 2) (Finite 1) +lossOrderReversed = Refl diff --git a/src/abi/typed-wasm.ipkg b/src/abi/typed-wasm.ipkg index 31f2b70..9b52812 100644 --- a/src/abi/typed-wasm.ipkg +++ b/src/abi/typed-wasm.ipkg @@ -20,6 +20,15 @@ modules = TypedWasm.ABI.Region , TypedWasm.ABI.SessionProtocol , TypedWasm.ABI.ResourceCapabilities , TypedWasm.ABI.Choreography + -- Grade kernel (PWL-01): transcribed from hyperpolymath/resource-algebra + -- @ cf9235c; the one definition of min-plus (Loss) and of max-plus + -- (MaxPlus) in the tree — tools/check-grade-kernel.sh. + , TypedWasm.ABI.ResourceAlgebra + , TypedWasm.ABI.ResourceAlgebra.Nat + , TypedWasm.ABI.ResourceAlgebra.Loss + , TypedWasm.ABI.ResourceAlgebra.MaxPlus + , TypedWasm.ABI.ResourceAlgebra.HWM + , TypedWasm.ABI.ResourceAlgebra.Separation , TypedWasm.ABI.Echo , TypedWasm.ABI.Tropical , TypedWasm.ABI.Epistemic From 5cd9cde69ac8eb20f29b9a3ae68e1cd3150d220c Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 00:59:20 +0000 Subject: [PATCH 04/13] refactor(abi): L11 Tropical and Echo draw their grade from the kernel Tropical.TropCost is now the kernel's Loss carrier (TropCost = LossGrade; tropAdd = lossAlt, tropMul = lossSeq). The twelve semiring axioms and the dioid-order layer are derived from the kernel's instance proofs instead of re-proved over a private copy; the local tropMin and natMax are deleted (base's minimum / maximum serve the bottleneck layer). Every public name and direction is kept, so Epistemic.idr and Proofs.idr compile unchanged. The header no longer says max-plus tracks the bottleneck: TropCost is min-plus and tropMax is min-max (choice min, sequence max, +inf absorbing), which is neither min-plus nor max-plus. tropMax stays local because the kernel has no MinMax instance. Echo.idr names its loss grade from the same kernel instance (EchoGrade, echoKeep = oneG, echoCollapse = zeroG) and defines no grade operation. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- src/abi/TypedWasm/ABI/Echo.idr | 52 ++++- src/abi/TypedWasm/ABI/Tropical.idr | 362 ++++++++++------------------- 2 files changed, 169 insertions(+), 245 deletions(-) diff --git a/src/abi/TypedWasm/ABI/Echo.idr b/src/abi/TypedWasm/ABI/Echo.idr index 873af2d..f9479fc 100644 --- a/src/abi/TypedWasm/ABI/Echo.idr +++ b/src/abi/TypedWasm/ABI/Echo.idr @@ -37,9 +37,13 @@ -- Estate cross-reference (audit 2026-06-16) — canonical axis: Agda -- hyperpolymath/echo-types @ 2bbdb49 (proofs/agda/{Echo,EchoResidue,EchoGraded, -- EchoGradedComonadInterface}.agda; experimental/ for the R0-R4 variance line). --- The min-plus grade IS the sibling TypedWasm.ABI.Tropical.TropCost; the loss --- of an echo residue is MEASURED into it via Tropical.ResidueMeasure --- (accumulation mu = tropMul = +). +-- The loss grade is the grade kernel's Loss instance (min-plus on ℕ ∪ {∞}, +-- TypedWasm.ABI.ResourceAlgebra.Loss, transcribed from resource-algebra +-- Instances/Loss.agda @ cf9235c, which is itself echo-types' +-- experimental/echo-additive/Grade.agda). `EchoGrade` below names it; +-- TypedWasm.ABI.Tropical.TropCost is the same carrier, so the loss of an echo +-- residue is MEASURED into it via Tropical.ResidueMeasure (accumulation +-- mu = lossSeq = +). This module defines no grade operation of its own. -- -- WHAT THIS FILE MIRRORS (the SETTLED, machine-checked core): -- * the exact-on-a-fiber recoverable subobject: Echo (= Sigma-fiber), @@ -49,7 +53,9 @@ -- * the irreversible-relegation step: EchoR + echoToResidue -- (~ EchoResidue.agda EchoR / echo-to-residue) — an attestation is exactly -- a retained residue of a forgotten witness. --- WHAT IT DEFERS: the numeric min-plus graded CARRIER and the (co)monad / +-- WHAT IT NAMES: the numeric min-plus graded CARRIER, as the kernel's Loss +-- instance (`EchoGrade`, `echoKeep`, `echoCollapse` at the end of this file). +-- WHAT IT DEFERS: the graded modality D_r itself and its (co)monad / -- adjunction laws are live research in echo-types/experimental and are NOT -- reproduced here (deferring per caveat 2; do not bake in a variance). -- @@ -69,6 +75,9 @@ module TypedWasm.ABI.Echo +import TypedWasm.ABI.ResourceAlgebra +import public TypedWasm.ABI.ResourceAlgebra.Loss + %default total -- Shadow the prelude's trans with a definition that reduces on the first @@ -295,3 +304,38 @@ echoToResidue : -> Echo f y -> EchoR C Cert y echoToResidue f kappa sound (MkEcho x pf) = MkEchoR (kappa x) (replace {p = \v => Cert (kappa x) v} pf (sound x)) + +-- ============================================================================ +-- The loss grade — the kernel's Loss instance +-- ============================================================================ +-- +-- echo-types grades loss by ℕ ∪ {∞}: `Finite 0` is `keep` (nothing lost), +-- `Infinity` is total collapse; sequence adds loss, alternatives keep the +-- less lossy branch. That algebra is TypedWasm.ABI.ResourceAlgebra.Loss; it +-- is named here, not redefined. + +||| The echo loss grade. The kernel's Loss carrier. +public export +EchoGrade : Type +EchoGrade = LossGrade + +||| `keep`: no information lost. The unit of sequence. +public export +echoKeep : EchoGrade +echoKeep = oneG + +||| Total collapse: nothing recoverable. The unit of alternatives. +public export +echoCollapse : EchoGrade +echoCollapse = zeroG + +||| Losing nothing then losing `r` loses `r`. Kernel `seqUnitL`. +public export +echoKeepThen : (r : EchoGrade) -> otimes Echo.echoKeep r = r +echoKeepThen r = seqUnitL r + +||| Total collapse absorbs every later loss. Kernel `annihilL` +||| (IsAnnihilating LossGrade). +public export +echoCollapseAbsorbs : (r : EchoGrade) -> otimes Echo.echoCollapse r = Echo.echoCollapse +echoCollapseAbsorbs r = annihilL r diff --git a/src/abi/TypedWasm/ABI/Tropical.idr b/src/abi/TypedWasm/ABI/Tropical.idr index 8350115..e803bde 100644 --- a/src/abi/TypedWasm/ABI/Tropical.idr +++ b/src/abi/TypedWasm/ABI/Tropical.idr @@ -3,45 +3,50 @@ -- -- Tropical.idr — Level 11: Tropical cost-tracking for memory access -- --- Every memory access operation carries a cost in a tropical semiring. --- The min-plus semiring tracks latency (cheapest path), the max-plus --- semiring tracks throughput (bottleneck path). The type checker proves --- that any access path through shared memory has bounded total cost. +-- Every memory access operation carries a cost. Three cost models live +-- here, and they are three different algebras (do not conflate them): +-- * sequential path cost and all-pairs CHEAPEST path (Level11Proof, +-- Level11KleeneProof): min-plus — the grade kernel's Loss carrier; +-- * the BOTTLENECK (worst step) of a path (Level11BottleneckProof): +-- min-max — choice by min, sequence by max, +inf absorbing. It is not +-- max-plus and has no kernel instance (resource-algebra has no MinMax); +-- * worst-case cost over alternatives would be max-plus +-- (ResourceAlgebra/MaxPlus.idr); no L11 obligation uses it yet. +-- The type checker proves that an access path through shared memory has +-- bounded cost. -- -- This is the "how expensive is this access pattern?" question answered -- at compile time. It prevents pathological access patterns (e.g. a -- tight loop doing random access across cache lines) from compiling -- without an explicit cost annotation acknowledging the expense. -- --- The tropical semiring algebra is adapted from 007's TropicalSemiring.idr. --- -- ---------------------------------------------------------------------------- --- Estate cross-reference (audit 2026-06-16) — canonical axis: Lean4 --- hyperpolymath/tropical-resource-typing @ 2e35229. --- --- This module's (TropCost, tropAdd = min, tropMul = +, Infinity, Finite 0) is --- the Idris2 analogue of the canonical Resource.Instances.MinPlus instance, --- and the twelve axioms below correspond to the canonical ResourceSemiring --- fields. It is a DELIBERATE Idris2 mirror, not a literal import: the --- canonical repo is Lean4/Isabelle and there is no Lean->Idris proof-transport --- path, so the algebra above is sourced from 007's TropicalSemiring.idr. +-- Grade kernel (PWL-01, 2026-10-14). TropCost IS the kernel's Loss carrier +-- (TypedWasm.ABI.ResourceAlgebra.Loss, transcribed from hyperpolymath/ +-- resource-algebra Instances/Loss.agda @ cf9235c): tropAdd = lossAlt (min), +-- tropMul = lossSeq (+), Infinity = 𝟘, Finite 0 = 𝟙. The twelve semiring +-- axioms and the dioid-order layer below are DERIVED from the kernel's +-- instance proofs; nothing here re-defines min-plus. 007-lang's +-- TropicalSemiring.idr (the source of the A2 port, 2026-04-18) and +-- tropical-resource-typing @ 2e35229 (Lean4, the earlier canonical axis) are +-- provenance, not parallel definitions. -- --- Mirrored: min-plus semiring + Kleene/Floyd-Warshall all-pairs closure. --- NOT yet mirrored (debt, tracked for owner decision): --- * ResourceAlgebra/Ordered interface (the dioid order a |+| b = b), --- * parametric_resource_transport (one-shot law transport to all instances), --- * the MinMax / Bridge.hub_ceiling BOTTLENECK instance, --- * the MaxPlus worst-case-budget instance, --- * Resource.EchoBridge.ResidueMeasure (E -> R residue measure; would wire --- the sibling TypedWasm.ABI.Echo into this grade). --- typed-wasm holds one thing the canonical Lean axis lacks: the Kleene-closure --- matrix layer below (extend-upstream candidate; owner sign-off required). +-- Still NOT mirrored (debt, owner decision): +-- * parametric_resource_transport — needs resource-algebra homomorphisms, +-- which are OPEN upstream; +-- * a MinMax kernel instance for the bottleneck layer (tropMax below is the +-- one grade operation defined outside the kernel; it is listed, with this +-- reason, in tools/grade-kernel.allow). +-- typed-wasm holds one thing the kernel lacks: the Kleene-closure matrix +-- layer below (extend-upstream candidate; owner sign-off required). -- ---------------------------------------------------------------------------- module TypedWasm.ABI.Tropical import TypedWasm.ABI.Region import TypedWasm.ABI.Levels +import public TypedWasm.ABI.ResourceAlgebra +import public TypedWasm.ABI.ResourceAlgebra.Loss import Data.Nat import Data.Fin import Data.List @@ -50,48 +55,26 @@ import Data.List.Elem %default total -- ============================================================================ --- Tropical Semiring +-- Tropical Semiring — the kernel's Loss instance -- ============================================================================ -||| A tropical semiring value. In the min-plus semiring, addition is min -||| and multiplication is plus. Infinity is the zero element. +||| A min-plus cost: `Finite n` or `Infinity` (unreachable / unbounded). +||| This is the kernel's Loss carrier; addition is min, multiplication is +||| plus, Infinity is the zero element and `Finite 0` the unit. public export -data TropCost : Type where - ||| Finite cost value (non-negative). - Finite : (cost : Nat) -> TropCost - ||| Infinite cost — unreachable or unbounded. - Infinity : TropCost +TropCost : Type +TropCost = LossGrade -||| Structural minimum for Nat (proof-friendly). -||| -||| Idris2 0.8's Prelude.min is defined via comparison -||| (`if x < y then x else y`) and does not reduce under pattern matching -||| on variables in proofs. This equivalent definition by structural -||| recursion does, which is what makes the semiring proofs below go -||| through without holes. -||| -||| Extensionally equal to Prelude.min on Nat (ported from -||| 007-lang/proofs/idris2/TropicalSemiring.idr). -private -tropMin : Nat -> Nat -> Nat -tropMin Z _ = Z -tropMin (S _) Z = Z -tropMin (S m) (S n) = S (tropMin m n) - -||| Tropical addition: min of two costs. Uses structural `tropMin` so -||| the semiring laws below reduce cleanly. +||| Tropical addition: min of two costs. The kernel's `lossAlt`. public export tropAdd : TropCost -> TropCost -> TropCost -tropAdd Infinity b = b -tropAdd a Infinity = a -tropAdd (Finite a) (Finite b) = Finite (tropMin a b) +tropAdd = lossAlt -||| Tropical multiplication: sum of two costs (path composition). +||| Tropical multiplication: sum of two costs (path composition). The +||| kernel's `lossSeq`. public export tropMul : TropCost -> TropCost -> TropCost -tropMul Infinity _ = Infinity -tropMul _ Infinity = Infinity -tropMul (Finite a) (Finite b) = Finite (a + b) +tropMul = lossSeq -- ============================================================================ -- Cost-Annotated Access @@ -148,179 +131,108 @@ record Level11Proof where bounded : CostBounded totalCost bound -- ============================================================================ --- Tropical semiring laws — all twelve axioms +-- Tropical semiring laws — all twelve axioms, derived from the kernel -- ============================================================================ -- --- Ported 2026-04-18 from 007-lang/proofs/idris2/TropicalSemiring.idr. --- (TropCost, tropAdd, tropMul, Infinity, Finite 0) is a proven commutative --- semiring. Zero dangerous patterns, %default total, mechanically checked --- by idris2 --check. - --- ---- Private Nat lemmas (structural, used to close the Finite cases) ---- - -||| Right identity for Nat addition. -private -plusZeroRightNeutral' : (n : Nat) -> n + 0 = n -plusZeroRightNeutral' Z = Refl -plusZeroRightNeutral' (S k) = cong S (plusZeroRightNeutral' k) - -||| Nat addition: m + S n = S (m + n). -private -plusSuccRight' : (m, n : Nat) -> m + S n = S (m + n) -plusSuccRight' Z n = Refl -plusSuccRight' (S k) n = cong S (plusSuccRight' k n) - -||| Nat addition is commutative. -private -plusComm' : (m, n : Nat) -> m + n = n + m -plusComm' Z Z = Refl -plusComm' Z (S k) = cong S (plusComm' Z k) -plusComm' (S k) Z = cong S (plusComm' k Z) -plusComm' (S k) (S j) = - rewrite plusSuccRight' k j in - rewrite plusSuccRight' j k in - cong S (cong S (plusComm' k j)) - -||| Nat addition is associative. -private -plusAssoc' : (m, n, p : Nat) -> m + (n + p) = (m + n) + p -plusAssoc' Z n p = Refl -plusAssoc' (S m) n p = cong S (plusAssoc' m n p) - -||| Structural minimum is commutative. -private -tropMinComm : (m, n : Nat) -> tropMin m n = tropMin n m -tropMinComm Z Z = Refl -tropMinComm Z (S _) = Refl -tropMinComm (S _) Z = Refl -tropMinComm (S m) (S n) = cong S (tropMinComm m n) - -||| Structural minimum is associative. -private -tropMinAssoc : (m, n, p : Nat) -> tropMin m (tropMin n p) = tropMin (tropMin m n) p -tropMinAssoc Z _ _ = Refl -tropMinAssoc (S _) Z _ = Refl -tropMinAssoc (S _) (S _) Z = Refl -tropMinAssoc (S m) (S n) (S p) = cong S (tropMinAssoc m n p) - -||| Addition distributes over structural minimum from the left: -||| a + tropMin m n = tropMin (a + m) (a + n). -private -plusDistribOverTropMin : (a, m, n : Nat) -> a + tropMin m n = tropMin (a + m) (a + n) -plusDistribOverTropMin Z m n = Refl -plusDistribOverTropMin (S a) m n = cong S (plusDistribOverTropMin a m n) +-- Each law below is the kernel's Loss-instance proof +-- (TypedWasm.ABI.ResourceAlgebra.Loss), restated in this module's historic +-- names and directions so existing consumers keep compiling. The one law +-- the kernel does not carry — commutativity of sequence — is a fact about +-- this instance (ℕ addition commutes), proved here from base's +-- plusCommutative; it is not a re-definition of the algebra. -- ---- Additive monoid: (TropCost, tropAdd, Infinity) ---- -||| Left identity: tropAdd Infinity a = a. +||| Left identity: tropAdd Infinity a = a. Kernel `altUnitL`. public export tropAddLeftId : (a : TropCost) -> tropAdd Infinity a = a -tropAddLeftId Infinity = Refl -tropAddLeftId (Finite _) = Refl +tropAddLeftId a = altUnitL a -||| Right identity: tropAdd a Infinity = a. +||| Right identity: tropAdd a Infinity = a. Kernel `altUnitR`. public export tropAddRightId : (a : TropCost) -> tropAdd a Infinity = a -tropAddRightId Infinity = Refl -tropAddRightId (Finite _) = Refl +tropAddRightId a = altUnitR a -||| Commutativity: tropAdd a b = tropAdd b a. +||| Commutativity: tropAdd a b = tropAdd b a. Kernel `lossAltComm`. ||| ||| The order of two branch alternatives does not affect which one wins. public export tropAddComm : (a, b : TropCost) -> tropAdd a b = tropAdd b a -tropAddComm Infinity Infinity = Refl -tropAddComm Infinity (Finite _) = Refl -tropAddComm (Finite _) Infinity = Refl -tropAddComm (Finite m) (Finite n) = cong Finite (tropMinComm m n) +tropAddComm = lossAltComm ||| Associativity: tropAdd a (tropAdd b c) = tropAdd (tropAdd a b) c. +||| Kernel `lossAltAssoc`, read right to left. ||| ||| Grouping three branch alternatives does not affect the minimum outcome. public export tropAddAssoc : (a, b, c : TropCost) -> tropAdd a (tropAdd b c) = tropAdd (tropAdd a b) c -tropAddAssoc Infinity _ _ = Refl -tropAddAssoc (Finite _) Infinity _ = Refl -tropAddAssoc (Finite _) (Finite _) Infinity = Refl -tropAddAssoc (Finite m) (Finite n) (Finite p) = cong Finite (tropMinAssoc m n p) +tropAddAssoc a b c = sym (lossAltAssoc a b c) -- ---- Multiplicative monoid: (TropCost, tropMul, Finite 0) ---- -||| Left identity: tropMul (Finite 0) a = a. +||| Left identity: tropMul (Finite 0) a = a. Kernel `lossSeqUnitL`. public export tropMulLeftId : (a : TropCost) -> tropMul (Finite 0) a = a -tropMulLeftId Infinity = Refl -tropMulLeftId (Finite _) = Refl +tropMulLeftId = lossSeqUnitL -||| Right identity: tropMul a (Finite 0) = a. +||| Right identity: tropMul a (Finite 0) = a. Kernel `lossSeqUnitR`. public export tropMulRightId : (a : TropCost) -> tropMul a (Finite 0) = a -tropMulRightId Infinity = Refl -tropMulRightId (Finite n) = cong Finite (plusZeroRightNeutral' n) +tropMulRightId = lossSeqUnitR -||| Commutativity: tropMul a b = tropMul b a. +||| Commutativity: tropMul a b = tropMul b a. Instance fact (ℕ + commutes); +||| the kernel's sequence is only a monoid. ||| ||| Sequential costs compose the same in either order. public export tropMulComm : (a, b : TropCost) -> tropMul a b = tropMul b a -tropMulComm Infinity Infinity = Refl -tropMulComm Infinity (Finite _) = Refl -tropMulComm (Finite _) Infinity = Refl -tropMulComm (Finite m) (Finite n) = cong Finite (plusComm' m n) +tropMulComm Infinity Infinity = Refl +tropMulComm Infinity (Finite _) = Refl +tropMulComm (Finite _) Infinity = Refl +tropMulComm (Finite m) (Finite n) = cong Finite (plusCommutative m n) ||| Associativity: tropMul a (tropMul b c) = tropMul (tropMul a b) c. +||| Kernel `lossSeqAssoc`, read right to left. ||| ||| Parenthesisation does not affect the cost of a sequential chain. public export tropMulAssoc : (a, b, c : TropCost) -> tropMul a (tropMul b c) = tropMul (tropMul a b) c -tropMulAssoc Infinity _ _ = Refl -tropMulAssoc (Finite _) Infinity _ = Refl -tropMulAssoc (Finite _) (Finite _) Infinity = Refl -tropMulAssoc (Finite m) (Finite n) (Finite p) = cong Finite (plusAssoc' m n p) +tropMulAssoc a b c = sym (lossSeqAssoc a b c) -- ---- Annihilation: Infinity annihilates tropMul ---- -||| Left annihilation: tropMul Infinity a = Infinity. +||| Left annihilation: tropMul Infinity a = Infinity. Kernel `annihilL`. public export tropMulLeftAnn : (a : TropCost) -> tropMul Infinity a = Infinity -tropMulLeftAnn _ = Refl +tropMulLeftAnn a = annihilL a -||| Right annihilation: tropMul a Infinity = Infinity. +||| Right annihilation: tropMul a Infinity = Infinity. Kernel `lossAnnihilR`. public export tropMulRightAnn : (a : TropCost) -> tropMul a Infinity = Infinity -tropMulRightAnn Infinity = Refl -tropMulRightAnn (Finite _) = Refl +tropMulRightAnn = lossAnnihilR -- ---- Distributivity ---- ||| Left distributivity: ||| tropMul a (tropAdd b c) = tropAdd (tropMul a b) (tropMul a c). +||| Kernel `lossDistribL`. ||| ||| A constant sequential prefix does not change which branch is cheaper. public export tropMulDistrib : (a, b, c : TropCost) -> tropMul a (tropAdd b c) = tropAdd (tropMul a b) (tropMul a c) -tropMulDistrib Infinity _ _ = Refl -tropMulDistrib (Finite _) Infinity _ = Refl -tropMulDistrib (Finite _) (Finite _) Infinity = Refl -tropMulDistrib (Finite m) (Finite n) (Finite p) = - cong Finite (plusDistribOverTropMin m n p) +tropMulDistrib = lossDistribL -||| Right distributivity (derived from left distributivity + tropMulComm): +||| Right distributivity: ||| tropMul (tropAdd a b) c = tropAdd (tropMul a c) (tropMul b c). +||| Kernel `lossDistribR` (formerly derived here from left distributivity + +||| tropMulComm; the kernel proves it directly). public export tropMulDistribR : (a, b, c : TropCost) -> tropMul (tropAdd a b) c = tropAdd (tropMul a c) (tropMul b c) -tropMulDistribR a b c = - let step1 = tropMulComm (tropAdd a b) c - step2 = tropMulDistrib c a b - swapA = tropMulComm c a - swapB = tropMulComm c b - rwA = cong (\x => tropAdd x (tropMul c b)) swapA - rwB = cong (\x => tropAdd (tropMul a c) x) swapB - in trans step1 (trans step2 (trans rwA rwB)) +tropMulDistribR = lossDistribR -- ---- Legacy aliases (kept so earlier consumers keep compiling) ---- @@ -444,112 +356,80 @@ record Level11KleeneProof (n : Nat) where inBound : EntryBounded pathCost (costs.pathBound) -- ============================================================================ --- Ordered layer — the canonical dioid order (Resource.Algebra.Ordered) +-- Ordered layer — the kernel's dioid order -- ============================================================================ -- --- Mirrors hyperpolymath/tropical-resource-typing Resource/Algebra/Ordered.lean --- @ 2e35229. The canonical resource order is the dioid order --- a |<=| b := tropAdd a b = b (canonical: a |+| b = b) --- For this MinPlus instance |+| = min, so the order is the REVERSE of numeric --- <=: Finite m |<=| Finite n iff n <= m, and Infinity (the additive zero / --- +inf) is the LEAST element. Smaller cost sits higher. - -||| Structural minimum is idempotent. -private -tropMinIdem : (m : Nat) -> tropMin m m = m -tropMinIdem Z = Refl -tropMinIdem (S k) = cong S (tropMinIdem k) +-- The kernel order (TypedWasm.ABI.ResourceAlgebra.LeG, Agda `_≼_`) is +-- a ≼ b := oplus a b = b +-- For this Loss instance oplus = min, so the order is the REVERSE of numeric +-- <=: Finite m ≼ Finite n iff n <= m, and Infinity (the additive zero / +-- +inf) is the LEAST element. Smaller cost sits higher (resource-algebra +-- Separation S-3; ResourceAlgebra/Separation.idr `lossOrderReversed`). +-- Every lemma here is the kernel's generic one at TropCost. -||| The canonical dioid order: a refines b iff combining them is b. +||| The dioid order: a refines b iff combining them is b. Kernel `LeG`. public export tropLe : TropCost -> TropCost -> Type -tropLe a b = tropAdd a b = b +tropLe a b = LeG a b -||| TropCost addition is idempotent (the dioid property). +||| TropCost addition is idempotent (the dioid property). Kernel `lossAltIdem`. public export tropAddIdem : (a : TropCost) -> tropAdd a a = a -tropAddIdem Infinity = Refl -tropAddIdem (Finite n) = cong Finite (tropMinIdem n) +tropAddIdem = lossAltIdem -||| |<=| is reflexive (canonical ResourceAlgebra.le_refl). +||| ≼ is reflexive. Kernel `leRefl`. public export tropLeRefl : (a : TropCost) -> tropLe a a -tropLeRefl = tropAddIdem +tropLeRefl a = leRefl a -||| |<=| is transitive (canonical ResourceAlgebra.le_trans): -||| a|+|c = a|+|(b|+|c) = (a|+|b)|+|c = b|+|c = c. +||| ≼ is transitive. Kernel `leTrans`. public export tropLeTrans : {a, b, c : TropCost} -> tropLe a b -> tropLe b c -> tropLe a c -tropLeTrans {a} {b} {c} ab bc = - rewrite sym bc in - rewrite tropAddAssoc a b c in - rewrite ab in Refl +tropLeTrans ab bc = leTrans ab bc -||| |+| is monotone in its right argument (canonical add_le_add_left): -||| (c|+|a)|+|(c|+|b) = c|+|b when a|+|b = b. +||| oplus is monotone in its right argument. Kernel `oplusMono` with the +||| left argument fixed. public export tropAddMonoR : {a, b : TropCost} -> (c : TropCost) -> tropLe a b -> tropLe (tropAdd c a) (tropAdd c b) -tropAddMonoR {a} {b} c ab = - let eMid : (tropAdd (tropAdd c a) c = tropAdd c a) - eMid = trans (sym (tropAddAssoc c a c)) - (trans (cong (tropAdd c) (tropAddComm a c)) - (trans (tropAddAssoc c c a) - (cong (\x => tropAdd x a) (tropAddIdem c)))) - in trans (tropAddAssoc (tropAdd c a) c b) - (trans (cong (\x => tropAdd x b) eMid) - (trans (sym (tropAddAssoc c a b)) - (cong (tropAdd c) ab))) - -||| |x| is monotone in its right argument (canonical mul_le_mul_left): -||| (c|x|a)|+|(c|x|b) = c|x|(a|+|b) = c|x|b. +tropAddMonoR c ab = oplusMono (leRefl c) ab + +||| otimes is monotone in its right argument. Kernel `otimesMonoL` +||| (IsOrdered LossGrade, obtained from IsDioid by `dioidMonoL`). public export tropMulMonoR : {a, b : TropCost} -> (c : TropCost) -> tropLe a b -> tropLe (tropMul c a) (tropMul c b) -tropMulMonoR {a} {b} c ab = - rewrite sym (tropMulDistrib c a b) in cong (tropMul c) ab +tropMulMonoR c ab = otimesMonoL c ab -||| |x| is monotone in its left argument (canonical mul_le_mul_right). +||| otimes is monotone in its left argument. Kernel `otimesMonoR`. public export tropMulMonoL : {a, b : TropCost} -> (c : TropCost) -> tropLe a b -> tropLe (tropMul a c) (tropMul b c) -tropMulMonoL {a} {b} c ab = - rewrite sym (tropMulDistribR a b c) in cong (\x => tropMul x c) ab +tropMulMonoL c ab = otimesMonoR c ab -- ============================================================================ -- Min-max / bottleneck layer (Resource.Instances.MinMax + Bridge.hub_ceiling) -- ============================================================================ -- --- Mirrors Resource/Instances/MinMax.lean + Resource/Bridge.lean @ 2e35229. --- The min-max (bottleneck) semiring shares the choice operation |+| = min --- (tropAdd) but composes sequentially by the WORST step (max) rather than by --- sum. Memory fact: MinMax / hub_ceiling = the bottleneck axis; one shared hub --- caps fidelity. Infinity (+inf) absorbs under max (an unreachable step makes --- the whole route unreachable). - -private -natMax : Nat -> Nat -> Nat -natMax Z n = n -natMax (S m) Z = S m -natMax (S m) (S n) = S (natMax m n) - -private -natMaxComm : (m, n : Nat) -> natMax m n = natMax n m -natMaxComm Z Z = Refl -natMaxComm Z (S n) = Refl -natMaxComm (S m) Z = Refl -natMaxComm (S m) (S n) = cong S (natMaxComm m n) - -private -tropMinZeroRight : (k : Nat) -> tropMin k Z = Z -tropMinZeroRight Z = Refl -tropMinZeroRight (S k) = Refl +-- Mirrors tropical-resource-typing Resource/Instances/MinMax.lean + +-- Resource/Bridge.lean @ 2e35229. The min-max (bottleneck) semiring shares +-- the choice operation with Loss (oplus = min) but composes sequentially by +-- the WORST step (max) rather than by sum. One shared hub caps fidelity. +-- Infinity (+inf) absorbs under max (an unreachable step makes the whole +-- route unreachable). +-- +-- This is NOT max-plus: max-plus takes max over ALTERNATIVES and sums along +-- a path, with −∞ as its zero (ResourceAlgebra/MaxPlus.idr); here max is +-- the SEQUENCE operation, +∞ absorbs, and alternatives stay min. The kernel +-- has no MinMax instance, so `tropMax` is the one grade operation defined +-- outside it (tools/grade-kernel.allow records why). Nat's max is base's +-- `Data.Nat.maximum`, not a local copy. ||| min (max m n) m = m : a lower bottleneck absorbs against the route max. private -tropMinMaxAbsorbL : (m, n : Nat) -> tropMin (natMax m n) m = m -tropMinMaxAbsorbL Z n = tropMinZeroRight n -tropMinMaxAbsorbL (S m) Z = cong S (tropMinIdem m) +tropMinMaxAbsorbL : (m, n : Nat) -> minimum (maximum m n) m = m +tropMinMaxAbsorbL Z n = minimumZeroZeroLeft n +tropMinMaxAbsorbL (S m) Z = cong S (minimumIdempotent m) tropMinMaxAbsorbL (S m) (S n) = cong S (tropMinMaxAbsorbL m n) ||| Bottleneck sequential composition: the worse (bottleneck) step. Infinity @@ -558,7 +438,7 @@ public export tropMax : TropCost -> TropCost -> TropCost tropMax Infinity _ = Infinity tropMax _ Infinity = Infinity -tropMax (Finite a) (Finite b) = Finite (natMax a b) +tropMax (Finite a) (Finite b) = Finite (maximum a b) ||| Bottleneck composition is commutative. public export @@ -566,7 +446,7 @@ tropMaxComm : (a, b : TropCost) -> tropMax a b = tropMax b a tropMaxComm Infinity Infinity = Refl tropMaxComm Infinity (Finite n) = Refl tropMaxComm (Finite m) Infinity = Refl -tropMaxComm (Finite m) (Finite n) = cong Finite (natMaxComm m n) +tropMaxComm (Finite m) (Finite n) = cong Finite (maximumCommutative m n) ||| The bottleneck of two grades is no better (in |<=|) than the left one. public export From 8fcd981f82c691fe2b78730b3e3a9b7a60291452 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 00:59:37 +0000 Subject: [PATCH 05/13] test(abi): grade-kernel gate and the falsifiers behind the kernel tools/check-grade-kernel.sh is the grep gate for "one definition of min-plus and one of max-plus": no tracked .idr file may define a Nat min/max (base's are the one definition), no file outside the kernel may define a grade operation (op (C x) (C y) = C (min/max/+ ...)), and the kernel must hold exactly the two in Loss.idr and the two in MaxPlus.idr. --self-test is its negative control (8 seeded duplicates caught, kernel shapes and near-misses not). Run against main's Tropical.idr it fails on tropMin / natMax / tropAdd / tropMul, as it should. tools/grade-kernel.allow lists the one exception, Tropical.tropMax (MinMax bottleneck), with why it is neither algebra. tools/check-kernel-proofs.sh runs, failing (never skipping) without idris2 0.8.0 and agda: - resource-algebra's own check at the pin (Agda --safe --without-K --no-libraries --double-check, 3 rejects); - a clean idris2 --build of the ABI, exit 0 AND no Error line; - tests/reject/*.idr: each refused at its invalid declaration with its EXPECT message, not for a scope/parse/path reason; - tests/transcription: the port, evaluated by Explore.idr, reproduces ops.tsv (172 rows); Agda accepts every row by refl against the PINNED instances and Idris2 by Refl against the port (244 equalities each); every row of wrong-rows.tsv is refused by both. Both run in contract-gate.yml (new jobs grade-kernel and kernel-proofs): actions.lock is keyed by workflow path, so a new workflow file would be rejected at startup; this one already holds the only action used. Idris2 0.8.0 is built from its tag (no binaries are published). tests/proof/regression.mjs pins 31 kernel names. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- .github/workflows/contract-gate.yml | 51 ++++++++ tests/proof/regression.mjs | 34 +++++ tests/reject/DriftExceedsPeak.idr | 17 +++ tests/reject/HWMAnnihilates.idr | 19 +++ tests/reject/LossWorstCase.idr | 17 +++ tests/reject/README.adoc | 21 +++ tests/reject/TropicalIsNotMaxPlus.idr | 18 +++ tests/transcription/Explore.idr | 60 +++++++++ tests/transcription/README.adoc | 26 ++++ tests/transcription/gen.sh | 90 +++++++++++++ tests/transcription/ops.tsv | 176 ++++++++++++++++++++++++++ tests/transcription/wrong-rows.tsv | 10 ++ tools/check-grade-kernel.sh | 163 ++++++++++++++++++++++++ tools/check-kernel-proofs.sh | 173 +++++++++++++++++++++++++ tools/grade-kernel.allow | 5 + 15 files changed, 880 insertions(+) create mode 100644 tests/reject/DriftExceedsPeak.idr create mode 100644 tests/reject/HWMAnnihilates.idr create mode 100644 tests/reject/LossWorstCase.idr create mode 100644 tests/reject/README.adoc create mode 100644 tests/reject/TropicalIsNotMaxPlus.idr create mode 100644 tests/transcription/Explore.idr create mode 100644 tests/transcription/README.adoc create mode 100755 tests/transcription/gen.sh create mode 100644 tests/transcription/ops.tsv create mode 100644 tests/transcription/wrong-rows.tsv create mode 100755 tools/check-grade-kernel.sh create mode 100755 tools/check-kernel-proofs.sh create mode 100644 tools/grade-kernel.allow diff --git a/.github/workflows/contract-gate.yml b/.github/workflows/contract-gate.yml index f4c7fe7..ffe2029 100644 --- a/.github/workflows/contract-gate.yml +++ b/.github/workflows/contract-gate.yml @@ -4,6 +4,9 @@ # direction + I3 shared-ABI drift) that keep this repo composable with the rest # of the stack. See CONTRACT.adoc. Self-contained (no reusable); runnable # locally as tools/check-contract.sh. +# Also gates the grade kernel (I2, extend don't redefine, applied to grades): +# tools/check-grade-kernel.sh and tools/check-kernel-proofs.sh, both runnable +# locally. name: Contract Gate on: pull_request: @@ -25,3 +28,51 @@ jobs: uses: actions/checkout@v7.0.1 - name: Run contract gate run: bash tools/check-contract.sh + + # Grade kernel (PWL-01): the one definition of min-plus and of max-plus. + # Checkout-only and toolchain-free, so it runs on every PR in seconds. + # It lives in this workflow because actions.lock is keyed by workflow path: + # a new workflow file would be rejected at startup until the lock is + # regenerated, and this one already holds the only action it needs. + grade-kernel: + name: Grade kernel (one min-plus, one max-plus) + runs-on: ubuntu-latest + timeout-minutes: 5 + steps: + - name: Checkout + uses: actions/checkout@v7.0.1 + - name: Gate self-test (negative control — seeded duplicates must be caught) + run: bash tools/check-grade-kernel.sh --self-test + - name: Grep gate + run: bash tools/check-grade-kernel.sh + + # The mechanical falsifiers behind the kernel: Idris2 0.8.0 builds the ABI, + # refuses tests/reject/*.idr for the intended reasons, and agrees with the + # PINNED Agda kernel (resource-algebra @ cf9235c, Agda --safe --without-K) + # on tests/transcription/ops.tsv; both provers refuse the wrong rows. + # Idris2 publishes no binaries and its release-tarball URL 404s (see + # e2e.yml build-e2e), so 0.8.0 is built from its tag with Chez Scheme. + kernel-proofs: + name: Grade kernel proofs (Idris2 0.8.0 + Agda) + runs-on: ubuntu-latest + timeout-minutes: 40 + steps: + - name: Checkout + uses: actions/checkout@v7.0.1 + - name: Install Chez Scheme, GMP and Agda + run: | + sudo apt-get update -qq + sudo apt-get install -y -qq chezscheme libgmp-dev agda-bin + agda --version + - name: Build Idris2 0.8.0 from source + run: | + git clone --quiet --depth 1 --branch v0.8.0 https://github.com/idris-lang/Idris2 "$RUNNER_TEMP/idris2-src" + make -C "$RUNNER_TEMP/idris2-src" bootstrap SCHEME=scheme -j"$(nproc)" > "$RUNNER_TEMP/idris2-build.log" 2>&1 \ + || { tail -60 "$RUNNER_TEMP/idris2-build.log"; exit 1; } + make -C "$RUNNER_TEMP/idris2-src" install > "$RUNNER_TEMP/idris2-install.log" 2>&1 \ + || { tail -60 "$RUNNER_TEMP/idris2-install.log"; exit 1; } + echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" + - name: Fetch siblings at their pins + run: bash scripts/fetch-siblings.sh + - name: Kernel proofs + run: bash tools/check-kernel-proofs.sh diff --git a/tests/proof/regression.mjs b/tests/proof/regression.mjs index 03a0116..1e6c794 100644 --- a/tests/proof/regression.mjs +++ b/tests/proof/regression.mjs @@ -205,6 +205,40 @@ const EXPECTED = [ ["VerifierSpec.idr", /^fixtureCleanLinearConsumerTrusted\s*:/m, "cross_compat row 1 trusted fixture"], ["VerifierSpec.idr", /^fixtureCleanLinearConsumerSpecAccepts\s*:/m, "Spec accepts row 1 via VerifierSpecAgreement"], + // ResourceAlgebra*.idr — the grade kernel (PWL-01), transcribed from + // hyperpolymath/resource-algebra @ cf9235c. Pins the interface layers, + // the three instances' operations and laws, and the separation witnesses. + ["ResourceAlgebra.idr", /^interface ResourceAlgebra g where/m, "ResourceAlgebra interface (Agda record)"], + ["ResourceAlgebra.idr", /^interface ResourceAlgebra g => IsOrdered g where/m, "IsOrdered layer"], + ["ResourceAlgebra.idr", /^interface ResourceAlgebra g => IsDioid g where/m, "IsDioid layer"], + ["ResourceAlgebra.idr", /^interface ResourceAlgebra g => IsAnnihilating g where/m, "IsAnnihilating layer (separate, as in Agda)"], + ["ResourceAlgebra.idr", /^leTrans\s*:/m, "Induced order transitivity (Agda ≼-trans)"], + ["ResourceAlgebra.idr", /^leAntisym\s*:/m, "Induced order antisymmetry (Agda ≼-antisym)"], + ["ResourceAlgebra.idr", /^oplusMono\s*:/m, "Alternatives monotone (Agda ⊕-mono)"], + ["ResourceAlgebra.idr", /^dioidMonoL\s*:/m, "Every dioid is ordered, left (Agda IsDioid.ordered)"], + ["ResourceAlgebra.idr", /^dioidMonoR\s*:/m, "Every dioid is ordered, right (Agda IsDioid.ordered)"], + ["ResourceAlgebra/Loss.idr", /^data\s+LossGrade/m, "Loss carrier ℕ ∪ {∞} — the one min-plus"], + ["ResourceAlgebra/Loss.idr", /^lossAlt\s*:/m, "Loss alternatives (min)"], + ["ResourceAlgebra/Loss.idr", /^lossSeq\s*:/m, "Loss sequence (+)"], + ["ResourceAlgebra/Loss.idr", /^lossDistribR\s*:/m, "Loss right distributivity"], + ["ResourceAlgebra/Loss.idr", /^lossAnnihilR\s*:/m, "Loss right annihilation"], + ["ResourceAlgebra/MaxPlus.idr", /^data\s+MaxPlusGrade/m, "MaxPlus carrier ℕ ∪ {−∞} — the one max-plus"], + ["ResourceAlgebra/MaxPlus.idr", /^maxPlusAlt\s*:/m, "MaxPlus alternatives (max)"], + ["ResourceAlgebra/MaxPlus.idr", /^maxPlusSeq\s*:/m, "MaxPlus sequence (+)"], + ["ResourceAlgebra/MaxPlus.idr", /^maxPlusDistribR\s*:/m, "MaxPlus right distributivity"], + ["ResourceAlgebra/HWM.idr", /^record\s+HWMGrade/m, "HWM carrier (peak, drift, drift ≤ peak)"], + ["ResourceAlgebra/HWM.idr", /^hwmSeq\s*:/m, "HWM sequence (suffix starts from drift)"], + ["ResourceAlgebra/HWM.idr", /^hwmSeqAssoc\s*:/m, "HWM sequence associativity"], + ["ResourceAlgebra/HWM.idr", /^hwmDistribL\s*:/m, "HWM left distributivity"], + ["ResourceAlgebra/Separation.idr", /^occupancyIsNotCost\s*:/m, "S-1 occupancy is not cost"], + ["ResourceAlgebra/Separation.idr", /^alternativesDiffer\s*:/m, "S-2 echo min vs tropical max"], + ["ResourceAlgebra/Separation.idr", /^lossOrderReversed\s*:/m, "S-3 induced order reversed in Loss"], + ["Tropical.idr", /^TropCost\s*:/m, "TropCost = the kernel's Loss carrier"], + ["Tropical.idr", /^tropMulDistribR\s*:/m, "L11 right distributivity (kernel lossDistribR)"], + ["Tropical.idr", /^hubCeiling\s*:/m, "L11 hub_ceiling (bottleneck)"], + ["Echo.idr", /^EchoGrade\s*:/m, "Echo loss grade = the kernel's Loss carrier"], + ["Echo.idr", /^echoCollapseAbsorbs\s*:/m, "Total collapse absorbs later loss (kernel annihilL)"], + // Proofs.idr — LevelAttestationW (standards#130 long-tail closure): // witness-indexed attestation GADT with per-level smart ctors, // extractors ("entails-semantic-property" lemmas), legacy bridge, diff --git a/tests/reject/DriftExceedsPeak.idr b/tests/reject/DriftExceedsPeak.idr new file mode 100644 index 0000000..b37aa40 --- /dev/null +++ b/tests/reject/DriftExceedsPeak.idr @@ -0,0 +1,17 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- MUST FAIL (tools/check-kernel-proofs.sh). Mirrors resource-algebra +-- tests/reject/DriftExceedsPeak.agda @ cf9235c. +-- +-- A run cannot end holding more live state than its peak. The invariant is +-- a field of the grade, so no such grade can be written down. +-- EXPECT: Mismatch between: S \?right and 0 +module DriftExceedsPeak + +import TypedWasm.ABI.ResourceAlgebra.HWM + +%default total + +invalid : HWMGrade +invalid = MkHWM 1 2 (LTESucc (LTESucc LTEZero)) diff --git a/tests/reject/HWMAnnihilates.idr b/tests/reject/HWMAnnihilates.idr new file mode 100644 index 0000000..0bed84d --- /dev/null +++ b/tests/reject/HWMAnnihilates.idr @@ -0,0 +1,19 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- MUST FAIL (tools/check-kernel-proofs.sh). Mirrors resource-algebra +-- tests/reject/HWMAnnihilates.agda @ cf9235c. +-- +-- In the high-water-mark algebra the alternatives unit is also the sequence +-- unit, so sequencing with it returns the other grade, not the unit. +-- Accepting this would smuggle an annihilating zero into an algebra that has +-- none (resource-algebra C-4 / H-3). +-- EXPECT: Mismatch between: 0 and n +module HWMAnnihilates + +import TypedWasm.ABI.ResourceAlgebra.HWM + +%default total + +invalid : (g : HWMGrade) -> hwmSeq HWM.hwmZero g = HWM.hwmZero +invalid (MkHWM p n b) = Refl diff --git a/tests/reject/LossWorstCase.idr b/tests/reject/LossWorstCase.idr new file mode 100644 index 0000000..145b660 --- /dev/null +++ b/tests/reject/LossWorstCase.idr @@ -0,0 +1,17 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- MUST FAIL (tools/check-kernel-proofs.sh). Mirrors resource-algebra +-- tests/reject/LossWorstCase.agda @ cf9235c. +-- +-- Echo's alternatives are MIN (the less lossy branch), not MAX. Reading them +-- as worst-case would identify the loss grade with a cost grade. +-- EXPECT: Can't solve constraint between: maximum m n and minimum m n +module LossWorstCase + +import TypedWasm.ABI.ResourceAlgebra.Loss + +%default total + +invalid : (m, n : Nat) -> lossAlt (Finite m) (Finite n) = Finite (maximum m n) +invalid m n = Refl diff --git a/tests/reject/README.adoc b/tests/reject/README.adoc new file mode 100644 index 0000000..6f508ba --- /dev/null +++ b/tests/reject/README.adoc @@ -0,0 +1,21 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Expected rejections (Idris2) + +Every `*.idr` here is a negative control: it states something the grade kernel +must refuse. `tools/check-kernel-proofs.sh` checks each one against the built +`src/abi` package. It passes only if the file is refused, the error sits at +its `invalid` declaration, and the message matches the file's `-- EXPECT:` +line. A refusal for a scoping, parsing or path reason counts as a failure, +because then the control proves nothing. + +[cols="1,3",options="header"] +|=== +| Fixture | What it would smuggle in +| `HWMAnnihilates` | an annihilating zero in the occupancy algebra (resource-algebra C-4 / H-3) +| `LossWorstCase` | echo's alternatives read as max, i.e. loss treated as cost (S-2) +| `DriftExceedsPeak` | a run ending with more live state than its peak +| `TropicalIsNotMaxPlus` | L11's `TropCost` read as max-plus (it is min-plus) +|=== + +The first three mirror resource-algebra `tests/reject/*.agda` at the pin in +`scripts/fetch-siblings.sh`. diff --git a/tests/reject/TropicalIsNotMaxPlus.idr b/tests/reject/TropicalIsNotMaxPlus.idr new file mode 100644 index 0000000..62fce13 --- /dev/null +++ b/tests/reject/TropicalIsNotMaxPlus.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). typed-wasm's own control. +-- +-- L11's TropCost is the kernel's Loss carrier (min-plus), not MaxPlus: its +-- alternatives keep the CHEAPER branch. If this were accepted, the reading +-- "Tropical.idr is the MaxPlus instance" would be true, and it is not +-- (LEVEL-STATUS row 11; ResourceAlgebra/Separation.idr S-2). +-- EXPECT: Can't solve constraint between: maximum m n and minimum m n +module TropicalIsNotMaxPlus + +import TypedWasm.ABI.Tropical + +%default total + +invalid : (m, n : Nat) -> tropAdd (Finite m) (Finite n) = Finite (maximum m n) +invalid m n = Refl diff --git a/tests/transcription/Explore.idr b/tests/transcription/Explore.idr new file mode 100644 index 0000000..0b261ef --- /dev/null +++ b/tests/transcription/Explore.idr @@ -0,0 +1,60 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Explore.idr — the EXPLORER side of the transcription check. +-- +-- Evaluates the Idris2 kernel's operations on a fixed finite domain and prints +-- one TSV row per (instance, operation, left, right): +-- TAB TAB TAB TAB +-- tests/transcription/gen.sh renders those rows into an Agda module that the +-- pinned resource-algebra sources must accept by `refl`, and into an Idris2 +-- module this port must accept by `Refl`. If the port and the Agda source +-- disagree on any tabled input, the Agda side refuses. +-- +-- Domain: Loss {fin 0..3, inf}, MaxPlus {val 0..3, bot} (every clause of +-- every operation is reached), HWM {(p, n) | n <= p <= 2}. +module Main + +import Data.List +import TypedWasm.ABI.ResourceAlgebra.Loss +import TypedWasm.ABI.ResourceAlgebra.MaxPlus +import TypedWasm.ABI.ResourceAlgebra.HWM + +%default total + +showL : LossGrade -> String +showL (Finite n) = "fin " ++ show n +showL Infinity = "inf" + +showM : MaxPlusGrade -> String +showM (Val n) = "val " ++ show n +showM Bot = "bot" + +showH : HWMGrade -> String +showH g = "hwm " ++ show g.peak ++ " " ++ show g.drift + +lossDom : List LossGrade +lossDom = [Finite 0, Finite 1, Finite 2, Finite 3, Infinity] + +maxDom : List MaxPlusGrade +maxDom = [Val 0, Val 1, Val 2, Val 3, Bot] + +hwmDom : List HWMGrade +hwmDom = + [ MkHWM 0 0 LTEZero, MkHWM 1 0 LTEZero, MkHWM 1 1 (LTESucc LTEZero) + , MkHWM 2 0 LTEZero, MkHWM 2 1 (LTESucc LTEZero) + , MkHWM 2 2 (LTESucc (LTESucc LTEZero)) ] + +rows : String -> String -> (a -> String) -> (a -> a -> a) -> List a -> List String +rows inst op sh f dom = + [ inst ++ "\t" ++ op ++ "\t" ++ sh x ++ "\t" ++ sh y ++ "\t" ++ sh (f x y) + | x <- dom, y <- dom ] + +main : IO () +main = traverse_ putStrLn $ + rows "Loss" "alt" showL lossAlt lossDom + ++ rows "Loss" "seq" showL lossSeq lossDom + ++ rows "MaxPlus" "alt" showM maxPlusAlt maxDom + ++ rows "MaxPlus" "seq" showM maxPlusSeq maxDom + ++ rows "HWM" "alt" showH hwmAlt hwmDom + ++ rows "HWM" "seq" showH hwmSeq hwmDom diff --git a/tests/transcription/README.adoc b/tests/transcription/README.adoc new file mode 100644 index 0000000..1c90265 --- /dev/null +++ b/tests/transcription/README.adoc @@ -0,0 +1,26 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Transcription check: the Idris2 grade kernel against its Agda source + +The grade kernel (`src/abi/TypedWasm/ABI/ResourceAlgebra*`) is a +transcription of hyperpolymath/resource-algebra (Agda), pinned in +`scripts/fetch-siblings.sh`. Nothing proves the two equal, so the +correspondence is ASSUMED. On the table below it is checked mechanically, in +the checker-matches-explorer pattern: + +. *Explorer.* `Explore.idr` evaluates the Idris2 port on a fixed finite domain + and prints `ops.tsv`: one row per (instance, operation, left, right, + result). The domain is Loss and MaxPlus on 0..3 plus the infinite point, so + every clause is reached, and HWM on peak ≤ 2. +. *Checkers.* `gen.sh` renders the table into an Agda module and an Idris2 + module. Agda must accept every row by `refl` against the *pinned* Agda + instances. Idris2 must accept it by `Refl` against the port. +. *Negative control.* Each row of `wrong-rows.tsv` is rendered on its own and + must be refused by both provers. + +`tools/check-kernel-proofs.sh` runs all three and also fails if the port no +longer reproduces `ops.tsv`. After an intended change to the kernel, run +`tools/check-kernel-proofs.sh --regen`, commit the new table and let Agda judge +it. + +Scope: agreement on the tabled inputs is TESTED. Agreement everywhere else is +not claimed. diff --git a/tests/transcription/gen.sh b/tests/transcription/gen.sh new file mode 100755 index 0000000..4949140 --- /dev/null +++ b/tests/transcription/gen.sh @@ -0,0 +1,90 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# gen.sh TABLE OUTDIR MODULE — render a transcription table into two checkers. +# +# OUTDIR/MODULE.agda every row as `refl` against the PINNED resource-algebra +# Agda instances (Loss / MaxPlus / HWM @ cf9235c) +# OUTDIR/MODULE.idr every row as `Refl` against the Idris2 port +# (src/abi/TypedWasm/ABI/ResourceAlgebra/*) +# +# TABLE rows: TAB TAB TAB TAB , with +# Loss values "fin N" | "inf" ops alt (_⊓g_ / lossAlt), seq (_+g_ / lossSeq) +# MaxPlus values "val N" | "bot" ops alt (tAdd / maxPlusAlt), seq (tMul / maxPlusSeq) +# HWM values "hwm P N" (peak, drift; N <= P) +# ops alt (_⊕h_ / hwmAlt), seq (_⊗h_ / hwmSeq); +# a result is compared by peak and drift +# (the bound proof is irrelevant). +# The rendering is purely syntactic; neither prover's answer is computed here. +set -euo pipefail +[ $# -eq 3 ] || { echo "usage: $0 TABLE OUTDIR MODULE" >&2; exit 2; } +table="$1"; out="$2"; mod="$3" +mkdir -p "$out" + +awk -F'\t' -v mod="$mod" -v agda="$out/$mod.agda" -v idr="$out/$mod.idr" ' +function lte_agda(n, s, i) { s = "z≤n"; for (i = 0; i < n; i++) s = "(s≤s " s ")"; return s } +function lte_idr(n, s, i) { s = "LTEZero"; for (i = 0; i < n; i++) s = "(LTESucc " s ")"; return s } +function va(inst, v, f) { + split(v, f, " ") + if (inst == "Loss") return (f[1] == "inf") ? "inf" : "(fin " f[2] ")" + if (inst == "MaxPlus") return (f[1] == "bot") ? "bot" : "(val " f[2] ")" + if (inst == "HWM") return "(hwm " f[2] " " f[3] " " lte_agda(f[3]) ")" +} +function vi(inst, v, f) { + split(v, f, " ") + if (inst == "Loss") return (f[1] == "inf") ? "Infinity" : "(Finite " f[2] ")" + if (inst == "MaxPlus") return (f[1] == "bot") ? "Bot" : "(Val " f[2] ")" + if (inst == "HWM") return "(MkHWM " f[2] " " f[3] " " lte_idr(f[3]) ")" +} +function opa(inst, op) { + if (inst == "Loss") return (op == "alt") ? "L._⊓g_" : "L._+g_" + if (inst == "MaxPlus") return (op == "alt") ? "M.tAdd" : "M.tMul" + if (inst == "HWM") return (op == "alt") ? "H._⊕h_" : "H._⊗h_" +} +function opi(inst, op) { + if (inst == "Loss") return (op == "alt") ? "lossAlt" : "lossSeq" + if (inst == "MaxPlus") return (op == "alt") ? "maxPlusAlt" : "maxPlusSeq" + if (inst == "HWM") return (op == "alt") ? "hwmAlt" : "hwmSeq" +} +BEGIN { + print "{-# OPTIONS --safe --without-K #-}" > agda + print "-- GENERATED by tests/transcription/gen.sh — do not edit." > agda + print "module " mod " where" > agda + print "open import ResourceAlgebra.Prelude" > agda + print "import ResourceAlgebra.Instances.Loss as L" > agda + print "import ResourceAlgebra.Instances.MaxPlus as M" > agda + print "import ResourceAlgebra.Instances.HWM as H" > agda + print "open L using (fin; inf)" > agda + print "open M using (val; bot)" > agda + print "open H using (hwm)" > agda + print "" > agda + print "-- GENERATED by tests/transcription/gen.sh — do not edit." > idr + print "module " mod > idr + print "" > idr + print "import TypedWasm.ABI.ResourceAlgebra.Loss" > idr + print "import TypedWasm.ABI.ResourceAlgebra.MaxPlus" > idr + print "import TypedWasm.ABI.ResourceAlgebra.HWM" > idr + print "" > idr + print "%default total" > idr + print "" > idr +} +NF == 0 || $1 ~ /^#/ { next } +NF != 5 { printf "gen.sh: %s:%d: expected 5 fields, got %d\n", FILENAME, NR, NF > "/dev/stderr"; bad = 1; exit 1 } +{ + k++; inst = $1; op = $2 + if (inst == "HWM") { + split($5, r, " ") + ea = "(" opa(inst, op) " " va(inst, $3) " " va(inst, $4) ")" + ei = "(" opi(inst, op) " " vi(inst, $3) " " vi(inst, $4) ")" + printf "row%d-peak : H.peak %s ≡ %s\nrow%d-peak = refl\n", k, ea, r[2], k > agda + printf "row%d-drift : H.drift %s ≡ %s\nrow%d-drift = refl\n", k, ea, r[3], k > agda + printf "row%dPeak : peak %s = %s\nrow%dPeak = Refl\n", k, ei, r[2], k > idr + printf "row%dDrift : drift %s = %s\nrow%dDrift = Refl\n", k, ei, r[3], k > idr + } else { + printf "row%d : %s %s %s ≡ %s\nrow%d = refl\n", k, opa(inst, op), va(inst, $3), va(inst, $4), va(inst, $5), k > agda + printf "row%d : %s %s %s = %s\nrow%d = Refl\n", k, opi(inst, op), vi(inst, $3), vi(inst, $4), vi(inst, $5), k > idr + } +} +END { if (!bad) printf "gen.sh: %d row(s) -> %s.{agda,idr}\n", k, mod > "/dev/stderr" } +' "$table" diff --git a/tests/transcription/ops.tsv b/tests/transcription/ops.tsv new file mode 100644 index 0000000..f1f899a --- /dev/null +++ b/tests/transcription/ops.tsv @@ -0,0 +1,176 @@ +# SPDX-License-Identifier: MPL-2.0 +# GENERATED by tools/check-kernel-proofs.sh --regen from tests/transcription/Explore.idr +# (the Idris2 port evaluated on the domain below). Checked by Agda refl against +# resource-algebra @ cf9235c and by Idris2 Refl against the port. Do not hand-edit. +Loss alt fin 0 fin 0 fin 0 +Loss alt fin 0 fin 1 fin 0 +Loss alt fin 0 fin 2 fin 0 +Loss alt fin 0 fin 3 fin 0 +Loss alt fin 0 inf fin 0 +Loss alt fin 1 fin 0 fin 0 +Loss alt fin 1 fin 1 fin 1 +Loss alt fin 1 fin 2 fin 1 +Loss alt fin 1 fin 3 fin 1 +Loss alt fin 1 inf fin 1 +Loss alt fin 2 fin 0 fin 0 +Loss alt fin 2 fin 1 fin 1 +Loss alt fin 2 fin 2 fin 2 +Loss alt fin 2 fin 3 fin 2 +Loss alt fin 2 inf fin 2 +Loss alt fin 3 fin 0 fin 0 +Loss alt fin 3 fin 1 fin 1 +Loss alt fin 3 fin 2 fin 2 +Loss alt fin 3 fin 3 fin 3 +Loss alt fin 3 inf fin 3 +Loss alt inf fin 0 fin 0 +Loss alt inf fin 1 fin 1 +Loss alt inf fin 2 fin 2 +Loss alt inf fin 3 fin 3 +Loss alt inf inf inf +Loss seq fin 0 fin 0 fin 0 +Loss seq fin 0 fin 1 fin 1 +Loss seq fin 0 fin 2 fin 2 +Loss seq fin 0 fin 3 fin 3 +Loss seq fin 0 inf inf +Loss seq fin 1 fin 0 fin 1 +Loss seq fin 1 fin 1 fin 2 +Loss seq fin 1 fin 2 fin 3 +Loss seq fin 1 fin 3 fin 4 +Loss seq fin 1 inf inf +Loss seq fin 2 fin 0 fin 2 +Loss seq fin 2 fin 1 fin 3 +Loss seq fin 2 fin 2 fin 4 +Loss seq fin 2 fin 3 fin 5 +Loss seq fin 2 inf inf +Loss seq fin 3 fin 0 fin 3 +Loss seq fin 3 fin 1 fin 4 +Loss seq fin 3 fin 2 fin 5 +Loss seq fin 3 fin 3 fin 6 +Loss seq fin 3 inf inf +Loss seq inf fin 0 inf +Loss seq inf fin 1 inf +Loss seq inf fin 2 inf +Loss seq inf fin 3 inf +Loss seq inf inf inf +MaxPlus alt val 0 val 0 val 0 +MaxPlus alt val 0 val 1 val 1 +MaxPlus alt val 0 val 2 val 2 +MaxPlus alt val 0 val 3 val 3 +MaxPlus alt val 0 bot val 0 +MaxPlus alt val 1 val 0 val 1 +MaxPlus alt val 1 val 1 val 1 +MaxPlus alt val 1 val 2 val 2 +MaxPlus alt val 1 val 3 val 3 +MaxPlus alt val 1 bot val 1 +MaxPlus alt val 2 val 0 val 2 +MaxPlus alt val 2 val 1 val 2 +MaxPlus alt val 2 val 2 val 2 +MaxPlus alt val 2 val 3 val 3 +MaxPlus alt val 2 bot val 2 +MaxPlus alt val 3 val 0 val 3 +MaxPlus alt val 3 val 1 val 3 +MaxPlus alt val 3 val 2 val 3 +MaxPlus alt val 3 val 3 val 3 +MaxPlus alt val 3 bot val 3 +MaxPlus alt bot val 0 val 0 +MaxPlus alt bot val 1 val 1 +MaxPlus alt bot val 2 val 2 +MaxPlus alt bot val 3 val 3 +MaxPlus alt bot bot bot +MaxPlus seq val 0 val 0 val 0 +MaxPlus seq val 0 val 1 val 1 +MaxPlus seq val 0 val 2 val 2 +MaxPlus seq val 0 val 3 val 3 +MaxPlus seq val 0 bot bot +MaxPlus seq val 1 val 0 val 1 +MaxPlus seq val 1 val 1 val 2 +MaxPlus seq val 1 val 2 val 3 +MaxPlus seq val 1 val 3 val 4 +MaxPlus seq val 1 bot bot +MaxPlus seq val 2 val 0 val 2 +MaxPlus seq val 2 val 1 val 3 +MaxPlus seq val 2 val 2 val 4 +MaxPlus seq val 2 val 3 val 5 +MaxPlus seq val 2 bot bot +MaxPlus seq val 3 val 0 val 3 +MaxPlus seq val 3 val 1 val 4 +MaxPlus seq val 3 val 2 val 5 +MaxPlus seq val 3 val 3 val 6 +MaxPlus seq val 3 bot bot +MaxPlus seq bot val 0 bot +MaxPlus seq bot val 1 bot +MaxPlus seq bot val 2 bot +MaxPlus seq bot val 3 bot +MaxPlus seq bot bot bot +HWM alt hwm 0 0 hwm 0 0 hwm 0 0 +HWM alt hwm 0 0 hwm 1 0 hwm 1 0 +HWM alt hwm 0 0 hwm 1 1 hwm 1 1 +HWM alt hwm 0 0 hwm 2 0 hwm 2 0 +HWM alt hwm 0 0 hwm 2 1 hwm 2 1 +HWM alt hwm 0 0 hwm 2 2 hwm 2 2 +HWM alt hwm 1 0 hwm 0 0 hwm 1 0 +HWM alt hwm 1 0 hwm 1 0 hwm 1 0 +HWM alt hwm 1 0 hwm 1 1 hwm 1 1 +HWM alt hwm 1 0 hwm 2 0 hwm 2 0 +HWM alt hwm 1 0 hwm 2 1 hwm 2 1 +HWM alt hwm 1 0 hwm 2 2 hwm 2 2 +HWM alt hwm 1 1 hwm 0 0 hwm 1 1 +HWM alt hwm 1 1 hwm 1 0 hwm 1 1 +HWM alt hwm 1 1 hwm 1 1 hwm 1 1 +HWM alt hwm 1 1 hwm 2 0 hwm 2 1 +HWM alt hwm 1 1 hwm 2 1 hwm 2 1 +HWM alt hwm 1 1 hwm 2 2 hwm 2 2 +HWM alt hwm 2 0 hwm 0 0 hwm 2 0 +HWM alt hwm 2 0 hwm 1 0 hwm 2 0 +HWM alt hwm 2 0 hwm 1 1 hwm 2 1 +HWM alt hwm 2 0 hwm 2 0 hwm 2 0 +HWM alt hwm 2 0 hwm 2 1 hwm 2 1 +HWM alt hwm 2 0 hwm 2 2 hwm 2 2 +HWM alt hwm 2 1 hwm 0 0 hwm 2 1 +HWM alt hwm 2 1 hwm 1 0 hwm 2 1 +HWM alt hwm 2 1 hwm 1 1 hwm 2 1 +HWM alt hwm 2 1 hwm 2 0 hwm 2 1 +HWM alt hwm 2 1 hwm 2 1 hwm 2 1 +HWM alt hwm 2 1 hwm 2 2 hwm 2 2 +HWM alt hwm 2 2 hwm 0 0 hwm 2 2 +HWM alt hwm 2 2 hwm 1 0 hwm 2 2 +HWM alt hwm 2 2 hwm 1 1 hwm 2 2 +HWM alt hwm 2 2 hwm 2 0 hwm 2 2 +HWM alt hwm 2 2 hwm 2 1 hwm 2 2 +HWM alt hwm 2 2 hwm 2 2 hwm 2 2 +HWM seq hwm 0 0 hwm 0 0 hwm 0 0 +HWM seq hwm 0 0 hwm 1 0 hwm 1 0 +HWM seq hwm 0 0 hwm 1 1 hwm 1 1 +HWM seq hwm 0 0 hwm 2 0 hwm 2 0 +HWM seq hwm 0 0 hwm 2 1 hwm 2 1 +HWM seq hwm 0 0 hwm 2 2 hwm 2 2 +HWM seq hwm 1 0 hwm 0 0 hwm 1 0 +HWM seq hwm 1 0 hwm 1 0 hwm 1 0 +HWM seq hwm 1 0 hwm 1 1 hwm 1 1 +HWM seq hwm 1 0 hwm 2 0 hwm 2 0 +HWM seq hwm 1 0 hwm 2 1 hwm 2 1 +HWM seq hwm 1 0 hwm 2 2 hwm 2 2 +HWM seq hwm 1 1 hwm 0 0 hwm 1 1 +HWM seq hwm 1 1 hwm 1 0 hwm 2 1 +HWM seq hwm 1 1 hwm 1 1 hwm 2 2 +HWM seq hwm 1 1 hwm 2 0 hwm 3 1 +HWM seq hwm 1 1 hwm 2 1 hwm 3 2 +HWM seq hwm 1 1 hwm 2 2 hwm 3 3 +HWM seq hwm 2 0 hwm 0 0 hwm 2 0 +HWM seq hwm 2 0 hwm 1 0 hwm 2 0 +HWM seq hwm 2 0 hwm 1 1 hwm 2 1 +HWM seq hwm 2 0 hwm 2 0 hwm 2 0 +HWM seq hwm 2 0 hwm 2 1 hwm 2 1 +HWM seq hwm 2 0 hwm 2 2 hwm 2 2 +HWM seq hwm 2 1 hwm 0 0 hwm 2 1 +HWM seq hwm 2 1 hwm 1 0 hwm 2 1 +HWM seq hwm 2 1 hwm 1 1 hwm 2 2 +HWM seq hwm 2 1 hwm 2 0 hwm 3 1 +HWM seq hwm 2 1 hwm 2 1 hwm 3 2 +HWM seq hwm 2 1 hwm 2 2 hwm 3 3 +HWM seq hwm 2 2 hwm 0 0 hwm 2 2 +HWM seq hwm 2 2 hwm 1 0 hwm 3 2 +HWM seq hwm 2 2 hwm 1 1 hwm 3 3 +HWM seq hwm 2 2 hwm 2 0 hwm 4 2 +HWM seq hwm 2 2 hwm 2 1 hwm 4 3 +HWM seq hwm 2 2 hwm 2 2 hwm 4 4 diff --git a/tests/transcription/wrong-rows.tsv b/tests/transcription/wrong-rows.tsv new file mode 100644 index 0000000..eef6f08 --- /dev/null +++ b/tests/transcription/wrong-rows.tsv @@ -0,0 +1,10 @@ +# SPDX-License-Identifier: MPL-2.0 +# NEGATIVE CONTROL for the transcription check: every row below is WRONG, +# and each must be refused by BOTH provers (tools/check-kernel-proofs.sh +# renders each row into its own module). One per instance: +# Loss alt read as worst case (max), the S-2 confusion: min 2 3 is 2 +# MaxPlus seq off by one: 2 + 3 is 5 +# HWM seq read as cost, the S-1 confusion: occupancy peak is 3, not 5 +Loss alt fin 2 fin 3 fin 3 +MaxPlus seq val 2 val 3 val 6 +HWM seq hwm 2 0 hwm 3 0 hwm 5 0 diff --git a/tools/check-grade-kernel.sh b/tools/check-grade-kernel.sh new file mode 100755 index 0000000..9a2b790 --- /dev/null +++ b/tools/check-grade-kernel.sh @@ -0,0 +1,163 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-grade-kernel.sh — one definition of min-plus and one of max-plus. +# +# The grade kernel (src/abi/TypedWasm/ABI/ResourceAlgebra.idr and +# src/abi/TypedWasm/ABI/ResourceAlgebra/*.idr) is the only place in the tree +# allowed to define a grade algebra's operations. Everything else draws its +# grades from it. This gate fails on any tracked .idr file that: +# +# R1 defines a structural min or max on Nat — a clause of the shape +# f (S x) (S y) = S (f x y) +# or a signature : Nat -> Nat -> Nat. +# No file may do this, kernel included: base's Data.Nat.minimum / +# maximum are the one definition, used by the kernel. +# R2 defines a grade operation outside the kernel — a clause that matches +# two values of the same constructor and rebuilds that constructor from +# a min, a max or a sum of their payloads: +# op (C x) (C y) = C (minimum x y) | C (maximum x y) | C (x + y) +# (any function name containing min/max counts as a min/max). +# +# A hit listed in tools/grade-kernel.allow (one "pathnamereason" +# per line) is reported as allowed, with its reason, instead of failing. +# The list is for operations that are provably neither min-plus nor +# max-plus; every entry must say which algebra it belongs to. +# +# Usage: tools/check-grade-kernel.sh # gate the tree +# tools/check-grade-kernel.sh --self-test # negative control: the +# # gate must REJECT seeded +# # duplicates and ACCEPT the +# # kernel's own shapes +set -euo pipefail +cd "$(dirname "$0")/.." + +KERNEL_RE='^src/abi/TypedWasm/ABI/ResourceAlgebra(\.idr|/[A-Za-z]+\.idr)$' +ALLOW_FILE="tools/grade-kernel.allow" + +ID="[A-Za-z_][A-Za-z0-9_']*" +# A grade-carrier constructor: any capitalised name except Nat's own S (R1 covers S). +CON="[A-RT-Z][A-Za-z0-9_']*|S[A-Za-z0-9_']+" +WS="[[:space:]]" +# A min/max-like name: tropMin, natMax, minimum, maxNat, ... (but not maxMonoLTE). +MINMAX="[A-Za-z0-9_']*([Mm]in|[Mm]ax)(imum|Nat|N)?" +# R1a: f (S x) (S y) = S (f x y) (backreference \1 = the function name) +R1A="^${WS}*(${ID})${WS}+\(S${WS}+${ID}\)${WS}+\(S${WS}+${ID}\)${WS}*=${WS}*S${WS}*\(${WS}*\1${WS}" +# R1b: <..min../..max..> : Nat -> Nat -> Nat +R1B="^${WS}*(private${WS}+|export${WS}+|public${WS}+export${WS}+)?${MINMAX}${WS}*:${WS}*Nat${WS}*->${WS}*Nat${WS}*->${WS}*Nat${WS}*$" +# R2: op (C x) (C y) = C (minlike x y | maxlike x y | x + y) +R2="^${WS}*(${ID})${WS}+\((${CON})${WS}+(${ID})\)${WS}+\(\2${WS}+(${ID})\)${WS}*=${WS}*\2${WS}*\((${MINMAX}${WS}+\3${WS}+\4|\3${WS}*\+${WS}*\4)${WS}*\)" + +# scan FILE... — print "rulefilelinenametext" per hit +scan() { + local f + for f in "$@"; do + { grep -nE "$R1A" "$f" 2>/dev/null || true; } | while IFS=: read -r ln text; do + name="$(printf '%s' "$text" | sed -E "s/^${WS}*(${ID}).*/\1/")" + printf 'R1\t%s\t%s\t%s\t%s\n' "$f" "$ln" "$name" "$text" + done + { grep -nE "$R1B" "$f" 2>/dev/null || true; } | while IFS=: read -r ln text; do + name="$(printf '%s' "$text" | sed -E "s/^${WS}*(private${WS}+|export${WS}+|public${WS}+export${WS}+)?(${ID}).*/\2/")" + printf 'R1\t%s\t%s\t%s\t%s\n' "$f" "$ln" "$name" "$text" + done + if ! printf '%s\n' "$f" | grep -qE "$KERNEL_RE"; then + { grep -nE "$R2" "$f" 2>/dev/null || true; } | while IFS=: read -r ln text; do + name="$(printf '%s' "$text" | sed -E "s/^${WS}*(${ID}).*/\1/")" + printf 'R2\t%s\t%s\t%s\t%s\n' "$f" "$ln" "$name" "$text" + done + fi + done +} + +# judge — read scan output on stdin; print verdicts; exit 1 on any non-allowed hit +judge() { + local bad=0 rule f ln name text reason + while IFS=$'\t' read -r rule f ln name text; do + [ -z "$rule" ] && continue + reason="" + if [ -f "$ALLOW_FILE" ]; then + reason="$(awk -F'\t' -v p="$f" -v n="$name" '$1==p && $2==n {print $3; exit}' "$ALLOW_FILE")" + fi + if [ -n "$reason" ]; then + printf 'allowed %s %s:%s %s — %s\n' "$rule" "$f" "$ln" "$name" "$reason" + else + printf 'ERROR %s %s:%s %s\n %s\n' "$rule" "$f" "$ln" "$name" "$text" + bad=1 + fi + done + return "$bad" +} + +if [ "${1:-}" = "--self-test" ]; then + tmp="$(mktemp -d)"; trap 'rm -rf "$tmp"' EXIT + mkdir -p "$tmp/src/abi/TypedWasm/ABI/ResourceAlgebra" + # Seeded duplicates — every one must be caught. + cat > "$tmp/dup.idr" <<'EOF' +tropMin : Nat -> Nat -> Nat +tropMin Z _ = Z +tropMin (S m) (S n) = S (tropMin m n) +private +natMax : Nat -> Nat -> Nat +natMax (S m) (S n) = S (natMax m n) +tropAdd (Finite a) (Finite b) = Finite (tropMin a b) +tropMul (Finite a) (Finite b) = Finite (a + b) +minNat : Nat -> Nat -> Nat +myMax (Val m) (Val n) = Val (maximum m n) +EOF + # The kernel's own shapes — R2 must accept them inside the kernel path. + cat > "$tmp/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr" <<'EOF' +lossSeq (Finite m) (Finite n) = Finite (m + n) +lossAlt (Finite m) (Finite n) = Finite (minimum m n) +EOF + # Neighbours that are not min/max/plus definitions — must not be caught. + cat > "$tmp/clean.idr" <<'EOF' +lte (S k) (S j) = lte k j +minimumCommutative (S k) (S j) = cong S $ minimumCommutative k j +tropMax (Finite a) Infinity = Infinity +pathBottleneck (x :: xs) = tropMax x (pathBottleneck xs) +maxMonoLTE (LTESucc p) (LTESucc q) = LTESucc (maxMonoLTE p q) +EOF + dup_hits="$(cd "$tmp" && scan dup.idr | wc -l)" + kern_hits="$(cd "$tmp" && scan src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr | wc -l)" + clean_hits="$(cd "$tmp" && scan clean.idr | wc -l)" + status=0 + # dup.idr: 2 R1a clauses + 3 R1b signatures + 3 R2 clauses = 8 + if [ "$dup_hits" -eq 8 ]; then echo "PASS: seeded duplicates caught (8/8)" + else echo "FAIL: seeded duplicates caught ${dup_hits}/8"; (cd "$tmp" && scan dup.idr); status=1; fi + if [ "$kern_hits" -eq 0 ]; then echo "PASS: kernel's own grade operations accepted inside the kernel" + else echo "FAIL: ${kern_hits} false hit(s) inside the kernel"; status=1; fi + if [ "$clean_hits" -eq 0 ]; then echo "PASS: non-definitions not caught (0 false positives)" + else echo "FAIL: ${clean_hits} false positive(s)"; (cd "$tmp" && scan clean.idr); status=1; fi + exit "$status" +fi + +# The positive half of "exactly one": inside the kernel, R2's shape must occur +# exactly twice in Loss.idr (lossSeq, lossAlt), exactly twice in MaxPlus.idr +# (maxPlusAlt, maxPlusSeq), and nowhere else. +kernel_count() { { grep -cE "$R2" "$1" 2>/dev/null || true; } | head -1; } +kernel_ok=1 +for kf in $(git ls-files 'src/abi/TypedWasm/ABI/ResourceAlgebra.idr' 'src/abi/TypedWasm/ABI/ResourceAlgebra/*.idr'); do + case "$kf" in + */ResourceAlgebra/Loss.idr|*/ResourceAlgebra/MaxPlus.idr) want=2 ;; + *) want=0 ;; + esac + got="$(kernel_count "$kf")" + if [ "$got" -ne "$want" ]; then + echo "ERROR kernel ${kf}: ${got} grade-operation definition(s), expected ${want}" + kernel_ok=0 + fi +done +for need in src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr; do + git ls-files --error-unmatch "$need" >/dev/null 2>&1 || { echo "ERROR kernel file missing: ${need}"; kernel_ok=0; } +done +[ "$kernel_ok" -eq 1 ] || { echo "GRADE-KERNEL GATE FAILED: the kernel does not hold exactly one min-plus and one max-plus."; exit 1; } + +mapfile -t files < <(git ls-files '*.idr') +echo "grade-kernel gate: ${#files[@]} tracked .idr file(s); kernel = ${KERNEL_RE}" +if scan "${files[@]}" | judge; then + echo "OK: one definition of min-plus (ResourceAlgebra/Loss.idr) and one of max-plus (ResourceAlgebra/MaxPlus.idr); no Nat min/max outside base" +else + echo "GRADE-KERNEL GATE FAILED: a grade operation is defined outside the kernel (see CONTRACT.adoc / LEVEL-STATUS.adoc)." + exit 1 +fi diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh new file mode 100755 index 0000000..2257d5f --- /dev/null +++ b/tools/check-kernel-proofs.sh @@ -0,0 +1,173 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-kernel-proofs.sh — the mechanical falsifiers behind the grade kernel. +# +# 1. upstream resource-algebra's own check at the pin (Agda --safe +# --without-K --no-libraries --double-check + its 3 rejects) +# 2. build idris2 --build src/abi/typed-wasm.ipkg: exit 0 AND no +# `Error:` line (idris2 can exit 0 while printing an error) +# 3. rejects every tests/reject/*.idr must FAIL, at its `invalid` +# declaration, with the message in its `-- EXPECT:` line, and +# not for a scoping/parsing/path reason +# 4. table the Idris2 port, evaluated by tests/transcription/Explore.idr, +# must reproduce tests/transcription/ops.tsv exactly; the table +# must be accepted row by row by Agda `refl` against the PINNED +# Agda instances and by Idris2 `Refl` against the port +# 5. control every row of tests/transcription/wrong-rows.tsv must be +# REFUSED by both provers +# +# A missing toolchain is a failure, never a skip. +# +# Usage: tools/check-kernel-proofs.sh # check +# tools/check-kernel-proofs.sh --regen # rewrite ops.tsv from the port, +# # then check (commit the diff) +set -uo pipefail +cd "$(dirname "$0")/.." +ROOT="$(pwd)" +REGEN=0; [ "${1:-}" = "--regen" ] && REGEN=1 + +RA="_build/dependencies/resource-algebra" +OUT="_build/kernel-proofs" +TTC="$ROOT/src/abi/build/ttc" +AGDA_FLAGS=(--safe --without-K --no-libraries --double-check --ignore-interfaces) +WRONG_REASON='Undefined name|Couldn.t parse|Parse error|not in the source directory|Can.t find import|Module .* not found|INTERNAL ERROR|Not in scope|Failed to find' + +fail=0 +pass() { printf 'PASS: %s\n' "$1"; } +err() { printf 'FAIL: %s\n' "$1"; fail=1; } +die() { printf 'FAIL: %s\n' "$1"; exit 1; } + +command -v idris2 >/dev/null || die "idris2 not on PATH (a gate that cannot run must not report OK)" +command -v agda >/dev/null || die "agda not on PATH (a gate that cannot run must not report OK)" +iv="$(idris2 --version)"; av="$(agda --version | head -1)" +echo "$iv"; echo "$av" +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 +[ -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" + +# 1 — upstream at the pin ----------------------------------------------------- +if (cd "$RA" && AGDA=agda bash scripts/check-agda.sh) > "$OUT/upstream.log" 2>&1; then + pass "upstream: $(tail -1 "$OUT/upstream.log")" +else + cat "$OUT/upstream.log"; err "upstream resource-algebra check failed at the pin" +fi + +# 2 — the ABI package --------------------------------------------------------- +# From clean, so a stale TTC cannot mask an error. +rm -rf src/abi/build +(cd src/abi && idris2 --build typed-wasm.ipkg) > "$OUT/build.log" 2>&1 +st=$? +if [ "$st" -eq 0 ] && ! grep -q '^Error' "$OUT/build.log"; then + pass "idris2 --build typed-wasm.ipkg: $(grep -c ': Building ' "$OUT/build.log") module(s) built, 0 errors" +else + grep -A12 '^Error' "$OUT/build.log" | head -40; err "idris2 --build typed-wasm.ipkg (exit $st)" +fi +dangerous="$(grep -rnE '\b(believe_me|assert_total|assert_smaller|idris_crash)\b|%unsafe' \ + src/abi/TypedWasm/ABI/ResourceAlgebra.idr src/abi/TypedWasm/ABI/ResourceAlgebra/ \ + | grep -vE '^[^:]+:[0-9]+:[[:space:]]*(--|\|\|\|)' || true)" +if [ -z "$dangerous" ]; then pass "kernel: zero believe_me / assert_total / assert_smaller / idris_crash" +else printf '%s\n' "$dangerous"; err "kernel contains a dangerous pattern"; fi + +# 3 — expected rejections ----------------------------------------------------- +n_rej=0 +for f in tests/reject/*.idr; do + [ -e "$f" ] || { err "no tests/reject/*.idr fixtures"; break; } + n_rej=$((n_rej + 1)) + name="$(basename "$f" .idr)" + expect="$(sed -n 's/^-- EXPECT: //p' "$f" | head -1)" + decl="$(grep -nE '^invalid[[:space:]]*:' "$f" | head -1 | cut -d: -f1)" + log="$OUT/reject-$name.log" + (cd tests/reject && IDRIS2_PATH="$TTC" idris2 --build-dir "$ROOT/$OUT/reject-build" --check "$name.idr") > "$log" 2>&1 + loc="$(grep -oE "^${name}:[0-9]+:" "$log" | head -1 | cut -d: -f2)" + if [ -z "$expect" ] || [ -z "$decl" ]; then + err "reject $name: fixture lacks an '-- EXPECT:' line or an 'invalid :' declaration" + elif ! grep -q '^Error' "$log"; then + cat "$log"; err "reject $name: ACCEPTED — an invalid proof typechecked" + elif grep -qE "$WRONG_REASON" "$log"; then + cat "$log"; err "reject $name: refused for the WRONG reason (scope/parse/path), so the control proves nothing" + elif [ -z "$loc" ] || [ "$loc" -lt "$decl" ]; then + cat "$log"; err "reject $name: error not located at its invalid declaration (line ${decl})" + elif ! grep -qE -- "$expect" "$log"; then + cat "$log"; err "reject $name: refused, but not with the expected message: ${expect}" + else + pass "rejected $name at line ${loc} (${expect})" + fi +done + +# 4 — the transcription table ------------------------------------------------- +(cd tests/transcription && IDRIS2_PATH="$TTC" idris2 --build-dir "$ROOT/$OUT/explore-build" --exec main Explore.idr) \ + > "$OUT/ops.explored.tsv" 2> "$OUT/explore.err" +if grep -qE 'Error|error' "$OUT/explore.err" || [ ! -s "$OUT/ops.explored.tsv" ]; then + cat "$OUT/explore.err"; err "explorer did not run (tests/transcription/Explore.idr)" +else + if [ "$REGEN" -eq 1 ]; then + { sed -n '1,/^# resource-algebra @/p' tests/transcription/ops.tsv | grep '^#' + cat "$OUT/ops.explored.tsv"; } > tests/transcription/ops.tsv.new + mv tests/transcription/ops.tsv.new tests/transcription/ops.tsv + echo "regenerated tests/transcription/ops.tsv ($(wc -l < "$OUT/ops.explored.tsv") rows)" + fi + if diff <(grep -v '^#' tests/transcription/ops.tsv) "$OUT/ops.explored.tsv" > "$OUT/table.diff"; then + pass "explorer: the port reproduces ops.tsv ($(wc -l < "$OUT/ops.explored.tsv") rows)" + else + head -20 "$OUT/table.diff" + err "the port no longer reproduces tests/transcription/ops.tsv — if the change is intended, run --regen and let Agda judge the new table" + fi +fi + +check_agda() { # check_agda DIR MODULE LOG + agda "${AGDA_FLAGS[@]}" -i "$RA/src" -i "$1" "$1/$2.agda" > "$3" 2>&1 +} +check_idris() { # check_idris DIR MODULE LOG — exit 0 and no Error line means accepted + (cd "$1" && IDRIS2_PATH="$TTC" idris2 --build-dir "$ROOT/$OUT/tc-build" --check "$2.idr") > "$3" 2>&1 + local st=$? + [ "$st" -eq 0 ] && ! grep -q '^Error' "$3" +} + +bash tests/transcription/gen.sh tests/transcription/ops.tsv "$OUT/table" TranscriptionCheck 2> "$OUT/gen.log" \ + || { cat "$OUT/gen.log"; err "gen.sh failed on ops.tsv"; } +rows="$(grep -c '^row' "$OUT/table/TranscriptionCheck.agda" 2>/dev/null || echo 0)" +if check_agda "$OUT/table" TranscriptionCheck "$OUT/agda-table.log"; then + pass "Agda (pinned resource-algebra) accepts the table by refl: $((rows / 2)) equalities" +else + grep -B2 -A8 'TranscriptionCheck.agda:[0-9]' "$OUT/agda-table.log" | head -30 + err "Agda refuses the table: the port and the pinned Agda instances DISAGREE" +fi +if check_idris "$OUT/table" TranscriptionCheck "$OUT/idris-table.log"; then + pass "Idris2 (port) accepts the table by Refl: $(grep -c '= Refl$' "$OUT/table/TranscriptionCheck.idr") equalities" +else + grep -A10 '^Error' "$OUT/idris-table.log" | head -30; err "Idris2 refuses the table" +fi + +# 5 — negative control: every wrong row refused by both ----------------------- +i=0 +while IFS= read -r line; do + case "$line" in ''|'#'*) continue ;; esac + i=$((i + 1)); m="WrongRow$i"; d="$OUT/wrong/$m"; mkdir -p "$d" + printf '%s\n' "$line" > "$d/row.tsv" + bash tests/transcription/gen.sh "$d/row.tsv" "$d" "$m" 2>/dev/null + if check_agda "$d" "$m" "$d/agda.log"; then + err "control: Agda ACCEPTED a wrong row: $(printf '%s' "$line" | tr '\t' ' ')" + elif grep -qE "$WRONG_REASON" "$d/agda.log" || ! grep -q "$m.agda:[0-9]" "$d/agda.log"; then + cat "$d/agda.log"; err "control: Agda refused $m for the wrong reason" + else + pass "control: Agda refuses $(printf '%s' "$line" | tr '\t' ' ')" + fi + if check_idris "$d" "$m" "$d/idris.log"; then + err "control: Idris2 ACCEPTED a wrong row: $(printf '%s' "$line" | tr '\t' ' ')" + elif grep -qE "$WRONG_REASON" "$d/idris.log" || ! grep -qE "^$m:[0-9]+:" "$d/idris.log"; then + cat "$d/idris.log"; err "control: Idris2 refused $m for the wrong reason" + else + pass "control: Idris2 refuses $(printf '%s' "$line" | tr '\t' ' ')" + fi +done < tests/transcription/wrong-rows.tsv +[ "$i" -gt 0 ] || err "control: tests/transcription/wrong-rows.tsv has no rows" + +echo +if [ "$fail" -ne 0 ]; then echo "KERNEL PROOFS FAILED"; exit 1; fi +echo "OK: kernel proofs — build, ${n_rej} rejection(s), table, and ${i} negative control row(s)" diff --git a/tools/grade-kernel.allow b/tools/grade-kernel.allow new file mode 100644 index 0000000..da9e54b --- /dev/null +++ b/tools/grade-kernel.allow @@ -0,0 +1,5 @@ +# SPDX-License-Identifier: MPL-2.0 +# Grade operations allowed outside the kernel by tools/check-grade-kernel.sh. +# One per line: \t\t. The reason must name the algebra +# the operation belongs to and why it is neither min-plus nor max-plus. +src/abi/TypedWasm/ABI/Tropical.idr tropMax min-max (bottleneck) SEQUENCE on the Loss carrier: max along a path with +inf absorbing, alternatives stay min. Not min-plus (sequence is max, not +) and not max-plus (max is sequence, not alternatives; zero is +inf, not -inf). resource-algebra @ cf9235c has no MinMax instance; adding one is an upstream decision (LEVEL-STATUS L11). From 6d39c322fdbe484db8fd85ff3d9ac81634d90ca5 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 00:59:37 +0000 Subject: [PATCH 06/13] docs: name the grade kernel in LEVEL-STATUS, CONTRACT, spec and CHANGELOG LEVEL-STATUS row 11 and the proof inventory say what the code now does (TropCost = LossGrade; tropMin / natMax deleted); a new inventory row and a "Grade kernel (PWL-01)" section give the kernel's statuses with their artefacts: laws PROVEN in Idris2; correspondence to the Agda source ASSUMED, TESTED on the 172-row table; separation TESTED. It records the correction that Tropical.idr was never max-plus. No level changes status. CONTRACT.adoc: the grade gates under Enforcement, and why contract.abi.sha256 does not change (the I3 anchors cover section.rs's wire format, not src/abi). spec: the L11 sentence no longer claims max-plus for throughput. Also replaces one stray NBSP in LEVEL-STATUS. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- CHANGELOG.adoc | 26 +++++++++++ CONTRACT.adoc | 12 +++++ LEVEL-STATUS.adoc | 66 +++++++++++++++++++++++++-- spec/type-safety-levels-for-wasm.adoc | 13 ++++-- 4 files changed, 109 insertions(+), 8 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index e2b9071..63fa599 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -8,6 +8,32 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Grade kernel: resource-algebra ported as the ABI's one source of grades (PWL-01, 2026-10-14) + +`src/abi/TypedWasm/ABI/ResourceAlgebra.idr` and `ResourceAlgebra/{Nat,Loss, +MaxPlus,HWM,Separation}.idr` transcribe hyperpolymath/resource-algebra @ +`cf9235c` (Agda `--safe --without-K`): the `ResourceAlgebra` / `IsOrdered` / +`IsDioid` / `IsAnnihilating` interfaces, the Loss (min-plus), MaxPlus +(max-plus) and HWM (occupancy) instances, and the S-1..S-3 separation +witnesses. + +* `Tropical.TropCost` is now the kernel's Loss carrier; the twelve semiring + axioms and the dioid-order layer are derived from the kernel, and the local + `tropMin` / `natMax` copies are deleted. Every public name is kept. +* `Echo.EchoGrade` names the same Loss carrier. +* `tools/check-grade-kernel.sh` (with `--self-test`) enforces one min-plus and + one max-plus in the tree. `tools/check-kernel-proofs.sh` runs the + falsifiers: the Idris2 0.8.0 build, `tests/reject/*.idr` refused for the + intended reason, and a 172-row operation table accepted by Agda `refl` against + the pinned sources and by Idris2 `Refl` against the port, with wrong rows + refused by both. Both run in `contract-gate.yml`. +* Correction: `Tropical.idr` was never max-plus. Its cost is min-plus and its + bottleneck is min-max (`tests/reject/TropicalIsNotMaxPlus.idr`). + +No level changes status; L11 and L12 stay draft. `contract.abi.sha256` is +unchanged: the I3 anchors cover the wire format in `section.rs`, not +`src/abi/`. + ==== Machine-readable substrate: retired `6a2` layout migrated to `descriptiles` (2026-10-10) `0-canon/CANONICAL-NAMES.adoc` (owner mandate of 2026-06-30) deprecates the diff --git a/CONTRACT.adoc b/CONTRACT.adoc index f2ff648..7cd9384 100644 --- a/CONTRACT.adoc +++ b/CONTRACT.adoc @@ -91,6 +91,18 @@ and runnable locally / as a pre-commit step): `section.rs` against sealed digests in `contract.abi.sha256`; any change fails until you bump `abi_version`, cite an ADR, and `--reseal`. - *I4 (advisory):* role-purity greps (none for a target). +- *I2 for grades (blocking):* `tools/check-grade-kernel.sh` — the grade kernel + (`src/abi/TypedWasm/ABI/ResourceAlgebra*`, transcribed from + hyperpolymath/resource-algebra at the pin in `scripts/fetch-siblings.sh`) + holds the one definition of min-plus and of max-plus; no other `.idr` file + may define a grade operation or a Nat min/max. `tools/check-kernel-proofs.sh` + holds the mechanical falsifiers behind it (Idris2 build, `tests/reject`, + the Agda/Idris2 transcription table). Both run in `contract-gate.yml`. + +The I3 digests cover only the anchored wire-format regions of `section.rs`. +The Idris2 level proofs under `src/abi/` are not anchors: changing them never +re-seals `contract.abi.sha256`, and re-sealing to "record" such a change would +be wrong (`--reseal` is for an `abi_version` bump only). To change the ABI (the *only* correct way): open a coordinated ADR across typed-wasm + AffineScript + ephapax, bump `CONTRACT_ABI_VERSION`, edit the diff --git a/LEVEL-STATUS.adoc b/LEVEL-STATUS.adoc index c57cc7d..88868f6 100644 --- a/LEVEL-STATUS.adoc +++ b/LEVEL-STATUS.adoc @@ -142,7 +142,10 @@ proof-term, behavioural lemmas `+loadSafeOffset+` and |11 |Tropical cost-tracking |Tropical.idr |Not yet |None |*In package (A1, 2026-04-18). Commutative-semiring closure PROVEN (A2, 2026-04-18): -all 12 axioms. Uses structural `+tropMin+` (007-lang template). Zero +all 12 axioms. PWL-01 (2026-10-14): the algebra is the grade kernel's +Loss instance (`+TropCost = LossGrade+`, `+ResourceAlgebra/Loss.idr+`); +the 12 axioms and the order layer are derived from it, and the local +`+tropMin+` / `+natMax+` copies are deleted (`+tools/check-grade-kernel.sh+`). Zero dangerous patterns. A16 (2026-06-16) estate accommodation: added the canonical dioid ORDER layer (`+tropLe+` refl/trans + add/mul monotonicity, mirrors `+tropical-resource-typing+` @@ -187,7 +190,7 @@ L16-C (payload primitive/declared region ref), L16-D (exact *[sfap]* = "`so far as possible`" — proofs are machine-checked in Idris2 with zero dangerous patterns. They are as complete as the Idris2 type checker can verify. Full mechanical verification against a formal Wasm -operational semantics (e.g. WasmCert-Isabelle) remains future work. +operational semantics (e.g. WasmCert-Isabelle) remains future work. === What "`proven, erased`" means @@ -322,7 +325,11 @@ witness-carrying levels, `+witnessToLegacy+` bridge, `+composeWitness+` mirror, `+composeWitnessLegacyAgree+` compat lemma, `+WitnessAchieved+` predicate. -|Tropical.idr |0 |0 |0 |In package (A1, 2026-04-18) +|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 +re-derived from `+ResourceAlgebra/Loss.idr+`; `+tropMax+` (MinMax +bottleneck) is the one grade operation outside the kernel, allowlisted +with its reason in `+tools/grade-kernel.allow+`. |Epistemic.idr |0 |0 |0 |In package (A1, 2026-04-18). A10 (2026-05-26): propagation theorems added — `+freshImpliesEqual+`, `+staleImpliesLT+`, @@ -350,6 +357,21 @@ RETRACTION R-2026-05-18 + experimental R0–R4). Added `+EchoR+` + attestation = a retained residue). Categorical base remains the settled fiber/slice structure. +|ResourceAlgebra.idr + ResourceAlgebra/{Nat,Loss,MaxPlus,HWM,Separation}.idr |0 |0 |0 |In package (PWL-01, 2026-10-14). The *grade +kernel*: `+ResourceAlgebra+` / `+IsOrdered+` / `+IsDioid+` / +`+IsAnnihilating+` interfaces and the Loss (min-plus), MaxPlus +(max-plus) and HWM (high-water-mark) instances, transcribed from +`+hyperpolymath/resource-algebra+` @ `+cf9235c+` (Agda `+--safe +--without-K+`). Laws re-proved in Idris2 (PROVEN, `+idris2 --build+`); +correspondence to the Agda source ASSUMED (transcription) and TESTED +on a 172-row operation table, accepted by Agda `+refl+` against the +pinned sources and by Idris2 `+Refl+` against the port, with a +3-row negative control refused by both +(`+tools/check-kernel-proofs.sh+`). Separation S-1..S-3 TESTED +(computed). Negative controls `+tests/reject/{HWMAnnihilates, +LossWorstCase, DriftExceedsPeak, TropicalIsNotMaxPlus}.idr+` refused +for the intended reason. + |VerifierSpec.idr |0 |0 |0 |Introduced A13 (2026-05-26, PR #72) as statement-level spec-of-record for post-A10 items 7+8. *Promoted to total bodies 2026-05-27 (PR #79)*: same `+ModuleSummary+` / @@ -561,3 +583,41 @@ comonad claims). `+--safe+`, closed. Nothing pushed or PR’d — drafts are for owner review per the stop-first rule. + +=== Grade kernel (PWL-01 — 2026-10-14) + +The "same object" above is now one definition. The grade kernel +(`+src/abi/TypedWasm/ABI/ResourceAlgebra*+`) is the Idris2 transcription of +`+hyperpolymath/resource-algebra+` @ `+cf9235c+`, the estate's Agda +(`+--safe --without-K+`) proof kernel for grades, fetched by +`+scripts/fetch-siblings.sh+`. It holds the only min-plus (Loss) and the only +max-plus (MaxPlus) in the tree, plus the high-water-mark occupancy grade +(HWM). `+tools/check-grade-kernel.sh+` fails the build if anything else defines +one. `+Tropical.TropCost+`, `+Echo.EchoGrade+` and (through `+TropCost+`) +`+Epistemic.syncGrade+` all draw their grade from Loss. + +What is proved, and how: + +* The interface laws and the three instances are re-proved in Idris2 + (`+idris2 --build+`, zero dangerous patterns). PROVEN against the Idris2 + definitions. +* That those definitions are the Agda ones is a transcription: ASSUMED. On a + 172-row operation table (every clause of every operation), it is TESTED. + Agda accepts each row by `+refl+` against the pinned sources and Idris2 + accepts it by `+Refl+` against the port. Three wrong rows are refused by + both (`+tools/check-kernel-proofs.sh+`, in CI as `+contract-gate.yml+` / + `+kernel-proofs+`). +* The three grades are not one: S-1 occupancy is not cost, S-2 echo + alternatives are min while tropical alternatives are max, S-3 the order runs + opposite ways (`+ResourceAlgebra/Separation.idr+`, computed). So L11's + latency cost (Loss carrier), a worst-case cost (MaxPlus) and L13's occupancy + (HWM) are kept apart. + +One correction to earlier prose. `+Tropical.idr+` was never max-plus: its +`+TropCost+` is min-plus (the Loss algebra), and its bottleneck layer +(`+tropMax+`) is min-max, which is neither min-plus nor max-plus. +`+tests/reject/TropicalIsNotMaxPlus.idr+` is the checked statement. The +kernel has no MinMax instance, so `+tropMax+` stays local, allowlisted with +that reason. Whether to add MinMax upstream is an owner decision. + +No level changes status here: L11 and L12 stay draft. diff --git a/spec/type-safety-levels-for-wasm.adoc b/spec/type-safety-levels-for-wasm.adoc index 74624e3..6efc4f5 100644 --- a/spec/type-safety-levels-for-wasm.adoc +++ b/spec/type-safety-levels-for-wasm.adoc @@ -76,11 +76,14 @@ _reference_ level. **Levels 11-12** (Frontier) are unique to typed-wasm: * **Level 11 — Tropical Cost-Tracking**: Memory access operations carry - semiring costs (min-plus for latency, max-plus for throughput). The - type checker proves that any access path through shared memory has - bounded total cost. Uses the tropical semiring algebra formalised in - 007's `TropicalSemiring.idr`. This is the "how expensive is this - access pattern?" question answered at compile time. + semiring costs (min-plus for latency and cheapest path, min-max for the + bottleneck step; a max-plus worst-case grade is available but not yet + used). The type checker proves that any access path through shared + memory has bounded total cost. The grades come from the ABI's grade + kernel (`ResourceAlgebra`, transcribed from hyperpolymath/resource-algebra; + 007's `TropicalSemiring.idr` is the provenance of the first port). This + is the "how expensive is this access pattern?" question answered at + compile time. * **Level 12 — Epistemic Safety**: Tracks which module _knows_ what about shared memory state. Module A writes field X; Module B's knowledge of From 417745d5cc3fc42e30954e908abf67ee521aa57f Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:12:06 +0000 Subject: [PATCH 07/13] docs: SPDX header on CHANGELOG.adoc CHANGELOG.adoc never carried one; this branch is the first to touch it since the licence-consistency check started looking at changed docs, so add the CC-BY-SA-4.0 identifier the other .adoc files use. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- CHANGELOG.adoc | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 63fa599..9a0973c 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == Changelog All notable changes to this project will be documented in this file. From 91f5dcbf29a6f9cb09761a552c7a9c9368bbacd3 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:11:53 +0000 Subject: [PATCH 08/13] feat(abi): L11 and L12 obligations read through the grade kernel MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit L11 (Tropical.idr). The numeric bound CostBounded c n is proved to BE the kernel's Loss order, Finite n ≼ c (costBoundedIsLossOrder / lossOrderIsCostBounded), so path bounds compose by the kernel's otimesMono (costBoundedSeq) rather than by a new argument. A new Level11WorstCaseProof grades a branching access plan in MaxPlus (worst case: + along Then, max at OneOf) with worstCaseThen / worstCaseOneOf from otimesMono / oplusMono and worstCaseFinite / worstCaseWithin reading the bound in ℕ. The obligation is DESIGNED (no surface syntax or attestation uses it). Level11BottleneckProof is MinMax and is left as it is; it is not MaxPlus (tests/reject/TropicalIsNotMaxPlus.idr), and tests/reject/WorstCaseIsCheapest.idr refuses reading MaxPlus's choice as the cheaper branch. L12 (Epistemic.idr, additive). stalenessGrade is a reader's lag as a Loss grade: fresh is the kernel's 𝟙 (freshHasNoStaleness), stale is not (staleHasStaleness), never synced is 𝟘 (neverSyncedIsCollapse), 𝟙 is the top (freshIsTop), and a relayed lag is the kernel's ⊗ (stalenessRelay). syncGrade gains a note: its number is a version, not a loss. Kernel additions (typed-wasm's own, labelled; not transcription): each instance's order read in ℕ (Loss: Finite n ≼ Finite k iff k ≤ n; MaxPlus: Val m ≼ Val n iff m ≤ n), and min/max-vs-LTE lemmas plus maxLub in ResourceAlgebra/Nat.idr. No operation changes, so the transcription table is unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- src/abi/TypedWasm/ABI/Epistemic.idr | 84 +++++++++++++ .../TypedWasm/ABI/ResourceAlgebra/Loss.idr | 36 ++++++ .../TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr | 17 +++ src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr | 45 +++++++ src/abi/TypedWasm/ABI/Tropical.idr | 115 ++++++++++++++++++ tests/reject/WorstCaseIsCheapest.idr | 17 +++ 6 files changed, 314 insertions(+) create mode 100644 tests/reject/WorstCaseIsCheapest.idr diff --git a/src/abi/TypedWasm/ABI/Epistemic.idr b/src/abi/TypedWasm/ABI/Epistemic.idr index 76e2d3a..cc1731b 100644 --- a/src/abi/TypedWasm/ABI/Epistemic.idr +++ b/src/abi/TypedWasm/ABI/Epistemic.idr @@ -397,6 +397,10 @@ observedHasProvenance (Observed {oldVer} sync) = Just (oldVer ** sync) -- indexed modality. Adopting the shared grade is vocabulary alignment, NOT a -- claim that this layer instantiates the canonical AccessibleModality. +||| NOTE (PWL-01): the number in `syncGrade` is a VERSION, not a loss. Under the +||| kernel's Loss order (`LeG`, smaller is higher) comparing two syncGrades +||| ranks the OLDER version higher, so do not order them with `LeG`. The +||| Loss reading of staleness is `stalenessGrade` below (the lag). ||| The tropical sync-grade of a knowledge state, read as irrecoverability: ||| never-observed (`Unknown`) relegates to `Infinity` (infeasible / unreachable ||| knowledge); knowledge observed at version `v` has finite grade `Finite v`. @@ -422,3 +426,83 @@ public export observedNotInfeasible : (s : Sync mod field old ver) -> Not (syncGrade (Observed {oldVer = old} s) = Infinity) observedNotInfeasible _ Refl impossible + +-- ============================================================================ +-- Staleness as a Loss grade (PWL-01 step 2, 2026-10-14 — ADDITIVE) +-- ============================================================================ +-- +-- L12 staleness, graded in the kernel's Loss instance +-- (TypedWasm.ABI.ResourceAlgebra.Loss): a reader's loss is its LAG, the +-- number of versions it is behind. Fresh knowledge loses nothing (𝟙 = +-- Finite 0, the top of the Loss order); never-synced knowledge is total +-- collapse (𝟘 = Infinity, the bottom). Lag accumulates along a relay of +-- readers by the kernel's sequence (⊗ = +), `stalenessRelay`. Nothing +-- above is re-indexed; the A10–A14 proofs are untouched. + +||| Staleness of knowing version `known` when the field is at `current`: +||| the lag, as a Loss grade. +public export +stalenessGrade : (known, current : Nat) -> LossGrade +stalenessGrade known current = Finite (minus current known) + +||| Staleness of a knowledge state against the field's current version. +||| Never observed is total collapse. +public export +knowledgeStaleness : {ver : Nat} -> Knowledge mod field ver -> (current : Nat) -> LossGrade +knowledgeStaleness {ver} (Observed _) current = stalenessGrade ver current +knowledgeStaleness Unknown _ = Infinity + +||| Fresh knowledge loses nothing: its staleness is the kernel's 𝟙. +public export +freshHasNoStaleness : Fresh mod field known current -> + stalenessGrade known current = oneG {g = LossGrade} +freshHasNoStaleness (MkFresh _ _ _ eq) = + rewrite eq in cong Finite (sym (minusZeroN current)) + +||| Stale knowledge loses something: its staleness is not 𝟙. +public export +staleHasStaleness : Stale mod field known current -> + Not (stalenessGrade known current = oneG {g = LossGrade}) +staleHasStaleness (MkStale lt) prf = + succNotLTEzero (replace {p = \x => LT 0 x} (finiteInjective prf) (minusPos lt)) + +||| Never-synced knowledge is the kernel's 𝟘 (total collapse). +public export +neverSyncedIsCollapse : (current : Nat) -> + knowledgeStaleness {mod} {field} Unknown current = zeroG {g = LossGrade} +neverSyncedIsCollapse _ = Refl + +||| Every staleness is at or below fresh in the Loss order: 𝟙 is the top. +public export +freshIsTop : (known, current : Nat) -> LeG (stalenessGrade known current) (oneG {g = LossGrade}) +freshIsTop known current = lossLeOne (stalenessGrade known current) + +||| A Level-12 proof is a proof of zero staleness. +public export +level12NoStaleness : (p : Level12Proof) -> + stalenessGrade p.knownVersion p.currentVersion = oneG {g = LossGrade} +level12NoStaleness p = freshHasNoStaleness p.freshness + +private +minusPlusCancel : (x, r : Nat) -> minus (x + r) r = x +minusPlusCancel x r = rewrite plusCommutative x r in minusPlus r + +private +lagSplits : {r, i, t : Nat} -> LTE r i -> LTE i t -> + minus t r = minus t i + minus i r +lagSplits {r} {i} {t} ri it = + -- t = ((t − i) + (i − r)) + r, by (t − i) + i = t and (i − r) + r = i; + -- subtract r from both sides. + trans (cong (\z => minus z r) + (trans (sym (plusMinusLte i t it)) + (trans (cong (\z => minus t i + z) (sym (plusMinusLte r i ri))) + (plusAssociative (minus t i) (minus i r) r)))) + (minusPlusCancel (minus t i + minus i r) r) + +||| Relayed knowledge: a reader at version r who learned from a reader at i, +||| itself behind the truth t, lags t by the SEQUENCE of the two lags — the +||| kernel's ⊗ in Loss. (r ≤ i ≤ t: knowledge only flows forward.) +public export +stalenessRelay : {r, i, t : Nat} -> LTE r i -> LTE i t -> + stalenessGrade r t = otimes (stalenessGrade i t) (stalenessGrade r i) +stalenessRelay ri it = cong Finite (lagSplits ri it) diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr index 8d97bca..4cf0917 100644 --- a/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr @@ -175,3 +175,39 @@ public export IsAnnihilating LossGrade where annihilL = \_ => Refl annihilR = lossAnnihilR + +-- ============================================================================ +-- typed-wasm additions (NOT in the Agda source): the order, read in ℕ +-- ============================================================================ +-- +-- Separation S-3 says the Loss order runs opposite to ℕ's. Precisely: +-- Finite n ≼ Finite k iff k ≤ n, +-- and Infinity (𝟘) is below everything, Finite 0 (𝟙) above everything. +-- L11 uses this to read a numeric cost bound as the kernel order. + +||| `Finite` is never `Infinity`. +public export +finiteNotInfinity : {n : Nat} -> Not (Finite n = Infinity) +finiteNotInfinity Refl impossible + +||| k ≤ n gives Finite n ≼ Finite k. +public export +lossLeOfLTE : {k, n : Nat} -> LTE k n -> LeG (Finite n) (Finite k) +lossLeOfLTE le = cong Finite (minimumOfLTE le) + +||| Finite n ≼ Finite k gives k ≤ n. +public export +lteOfLossLe : (n, k : Nat) -> LeG (Finite n) (Finite k) -> LTE k n +lteOfLossLe n k prf = lteOfMinimum n k (finiteInjective prf) + +||| Infinity is the least grade, so no finite grade sits below it: +||| Finite n ≼ Infinity is false. +public export +finiteNotLeInfinity : {n : Nat} -> Not (LeG (Finite n) Infinity) +finiteNotLeInfinity prf = finiteNotInfinity prf + +||| 𝟙 (= Finite 0, no loss) is the top of the Loss order. +public export +lossLeOne : (g : LossGrade) -> LeG g (Finite 0) +lossLeOne (Finite n) = cong Finite (minimumZeroZeroLeft n) +lossLeOne Infinity = Refl diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr index 5a85c42..f921103 100644 --- a/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr @@ -176,3 +176,20 @@ public export IsAnnihilating MaxPlusGrade where annihilL = \_ => Refl annihilR = maxPlusAnnihilR + +-- ============================================================================ +-- typed-wasm additions (NOT in the Agda source): the order, read in ℕ +-- ============================================================================ +-- +-- The MaxPlus order IS ℕ's on finite grades: Val m ≼ Val n iff m ≤ n. +-- L11's worst-case bound uses it to read a numeric bound as the kernel order. + +||| m ≤ n gives Val m ≼ Val n. +public export +maxPlusLeOfLTE : {m, n : Nat} -> LTE m n -> LeG (Val m) (Val n) +maxPlusLeOfLTE le = cong Val (maximumOfLTE le) + +||| Val m ≼ Val n gives m ≤ n. +public export +lteOfMaxPlusLe : (m, n : Nat) -> LeG (Val m) (Val n) -> LTE m n +lteOfMaxPlusLe m n prf = lteOfMaximum m n (valInjective prf) diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr index 85d5761..b1d64ec 100644 --- a/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr @@ -152,3 +152,48 @@ plusDistribRMin a b c = public export plusAssoc : (m, n, p : Nat) -> (m + n) + p = m + (n + p) plusAssoc m n p = sym (plusAssociative m n p) + +-- ============================================================================ +-- typed-wasm additions (NOT in the Agda source): min / max against ℕ's order +-- ============================================================================ +-- +-- Used to read the instances' induced orders as ℕ's order (Loss.idr, +-- MaxPlus.idr) and by the occupancy theorems (TypedWasm.ABI.Occupancy). + +||| `S` is injective. +public export +succInj : {m, n : Nat} -> S m = S n -> m = n +succInj Refl = Refl + +||| A bounded argument is what min returns. +public export +minimumOfLTE : {k, n : Nat} -> LTE k n -> minimum n k = k +minimumOfLTE {n} LTEZero = minimumZeroZeroLeft n +minimumOfLTE (LTESucc q) = cong S (minimumOfLTE q) + +||| If min returns its right argument, that argument is the smaller. +public export +lteOfMinimum : (n, k : Nat) -> minimum n k = k -> LTE k n +lteOfMinimum n Z _ = LTEZero +lteOfMinimum Z (S k) prf = absurd prf +lteOfMinimum (S n) (S k) prf = LTESucc (lteOfMinimum n k (succInj prf)) + +||| A smaller argument is absorbed by max. +public export +maximumOfLTE : {m, n : Nat} -> LTE m n -> maximum m n = n +maximumOfLTE LTEZero = Refl +maximumOfLTE (LTESucc q) = cong S (maximumOfLTE q) + +||| If max returns its right argument, the left one is the smaller. +public export +lteOfMaximum : (m, n : Nat) -> maximum m n = n -> LTE m n +lteOfMaximum Z n _ = LTEZero +lteOfMaximum (S m) Z prf = absurd prf +lteOfMaximum (S m) (S n) prf = LTESucc (lteOfMaximum m n (succInj prf)) + +||| max is the least upper bound. occupancy-types `max-lub` (Order.agda). +public export +maxLub : {a, b, c : Nat} -> LTE a c -> LTE b c -> LTE (maximum a b) c +maxLub LTEZero q = q +maxLub (LTESucc p) LTEZero = LTESucc p +maxLub (LTESucc p) (LTESucc q) = LTESucc (maxLub p q) diff --git a/src/abi/TypedWasm/ABI/Tropical.idr b/src/abi/TypedWasm/ABI/Tropical.idr index e803bde..bdb4062 100644 --- a/src/abi/TypedWasm/ABI/Tropical.idr +++ b/src/abi/TypedWasm/ABI/Tropical.idr @@ -47,6 +47,7 @@ import TypedWasm.ABI.Region import TypedWasm.ABI.Levels import public TypedWasm.ABI.ResourceAlgebra import public TypedWasm.ABI.ResourceAlgebra.Loss +import public TypedWasm.ABI.ResourceAlgebra.MaxPlus import Data.Nat import Data.Fin import Data.List @@ -577,3 +578,117 @@ public export bottleneckCeilsEdges : (p : Level11BottleneckProof) -> (e : TropCost) -> Elem e p.edges -> tropLe p.bottleneck e bottleneckCeilsEdges p e el = rewrite p.isBottleneck in hubCeiling e el + +-- ============================================================================ +-- Level 11 obligations as kernel instantiations (PWL-01 step 2) +-- ============================================================================ +-- +-- Each L11 obligation below is read through the grade kernel, so promoting +-- L11 is a matter of instantiating kernel lemmas, not of a new algebra: +-- +-- Level11Proof / Level11KleeneProof Loss (min-plus). The numeric bound +-- `CostBounded c n` IS the kernel order `Finite n ≼ c` (Loss's order is +-- ℕ's reversed: the cost sits above its bound), and bounds compose +-- along a path by the kernel's `otimesMono` (IsOrdered LossGrade). +-- Level11WorstCaseProof MaxPlus (max-plus). A branching +-- access plan's worst case: max over alternatives, sum along a +-- sequence; the bound is `worstCase plan ≼ Val bound`, which is ℕ's ≤. +-- DESIGNED as an obligation: no surface syntax, checker or attestation +-- uses it yet. +-- Level11BottleneckProof MinMax. Not a kernel instance and +-- NOT MaxPlus (tests/reject/TropicalIsNotMaxPlus.idr; see the header). +-- Left as it is. + +||| The L11 numeric bound is the kernel's Loss order: `c ≤ n` as a cost is +||| `Finite n ≼ c` as a grade. +public export +costBoundedIsLossOrder : {c : TropCost} -> {n : Nat} -> CostBounded c n -> LeG (Finite n) c +costBoundedIsLossOrder (BoundedFinite le) = lossLeOfLTE le + +||| ...and back: a grade above `Finite n` in the Loss order is a cost +||| bounded by n (in particular it is finite). +public export +lossOrderIsCostBounded : {n : Nat} -> (c : TropCost) -> LeG (Finite n) c -> CostBounded c n +lossOrderIsCostBounded (Finite k) prf = BoundedFinite (lteOfLossLe n k prf) +lossOrderIsCostBounded Infinity prf = absurd (finiteNotLeInfinity prf) + +||| Path bounds compose: bounded steps give a bounded path, with the bounds +||| added. Kernel `otimesMono` (IsOrdered LossGrade), not a new proof. +public export +costBoundedSeq : {c1, c2 : TropCost} -> {n1, n2 : Nat} -> + CostBounded c1 n1 -> CostBounded c2 n2 -> + CostBounded (tropMul c1 c2) (n1 + n2) +costBoundedSeq b1 b2 = + lossOrderIsCostBounded (tropMul c1 c2) + (otimesMono (costBoundedIsLossOrder b1) (costBoundedIsLossOrder b2)) + +-- ---- MaxPlus: the worst case over alternatives ---- + +||| A branching access plan: a single access of known cost, one plan after +||| another, or one of two plans (which one runs is not known statically). +public export +data AccessPlan : Type where + ||| One access of the given cost. + Step : (cost : Nat) -> AccessPlan + ||| `p` then `q`. + Then : AccessPlan -> AccessPlan -> AccessPlan + ||| Either `p` or `q`. + OneOf : AccessPlan -> AccessPlan -> AccessPlan + +||| The worst-case cost of a plan, graded in the kernel's MaxPlus instance: +||| costs add along `Then`, the dearer branch counts at `OneOf`. +public export +worstCase : AccessPlan -> MaxPlusGrade +worstCase (Step c) = Val c +worstCase (Then p q) = maxPlusSeq (worstCase p) (worstCase q) +worstCase (OneOf p q) = maxPlusAlt (worstCase p) (worstCase q) + +||| A plan's worst case is always finite (never −∞): every plan does at +||| least its cheapest branch. +public export +worstCaseFinite : (p : AccessPlan) -> (w : Nat ** worstCase p = Val w) +worstCaseFinite (Step c) = (c ** Refl) +worstCaseFinite (Then p q) = + let (a ** pa) = worstCaseFinite p + (b ** qb) = worstCaseFinite q + in (a + b ** rewrite pa in rewrite qb in Refl) +worstCaseFinite (OneOf p q) = + let (a ** pa) = worstCaseFinite p + (b ** qb) = worstCaseFinite q + in (maximum a b ** rewrite pa in rewrite qb in Refl) + +||| Level 11 worst-case obligation: the plan's worst case is within +||| `planBound` in the MaxPlus order (ℕ's ≤ on finite grades). +public export +record Level11WorstCaseProof where + constructor MkLevel11WorstCase + ||| The branching access plan. + plan : AccessPlan + ||| The declared worst-case bound. + planBound : Nat + ||| The plan's worst case does not exceed the bound. + planBounded : LeG (worstCase plan) (Val planBound) + +||| The bound read as a number: the worst case is `Val w` with w ≤ bound. +public export +worstCaseWithin : (prf : Level11WorstCaseProof) -> + (w : Nat ** (worstCase prf.plan = Val w, LTE w prf.planBound)) +worstCaseWithin prf = + let (w ** eq) = worstCaseFinite prf.plan + in (w ** (eq, lteOfMaxPlusLe w prf.planBound + (replace {p = \g => LeG g (Val prf.planBound)} eq prf.planBounded))) + +||| Sequenced plans: the bounds add. Kernel `otimesMono` (IsOrdered +||| MaxPlusGrade). +public export +worstCaseThen : {p, q : AccessPlan} -> {a, b : Nat} -> + LeG (worstCase p) (Val a) -> LeG (worstCase q) (Val b) -> + LeG (worstCase (Then p q)) (Val (a + b)) +worstCaseThen pa qb = otimesMono pa qb + +||| Alternative plans: the larger bound covers both. Kernel `oplusMono`. +public export +worstCaseOneOf : {p, q : AccessPlan} -> {a, b : Nat} -> + LeG (worstCase p) (Val a) -> LeG (worstCase q) (Val b) -> + LeG (worstCase (OneOf p q)) (Val (maximum a b)) +worstCaseOneOf pa qb = oplusMono pa qb diff --git a/tests/reject/WorstCaseIsCheapest.idr b/tests/reject/WorstCaseIsCheapest.idr new file mode 100644 index 0000000..bf9c1c4 --- /dev/null +++ b/tests/reject/WorstCaseIsCheapest.idr @@ -0,0 +1,17 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- MUST FAIL (tools/check-kernel-proofs.sh). typed-wasm's own control. +-- +-- L11's worst-case grade (MaxPlus) charges the DEARER branch of a choice. +-- If this were accepted, `Level11WorstCaseProof` would bound the cheapest +-- path, which is what the min-plus Kleene closure already does. +-- EXPECT: Mismatch between: 0 and 1 +module WorstCaseIsCheapest + +import TypedWasm.ABI.Tropical + +%default total + +invalid : worstCase (OneOf (Step 2) (Step 3)) = Val 2 +invalid = Refl From 23887272a9f83b5859a28d08c259aaad58e19787 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:11:53 +0000 Subject: [PATCH 09/13] =?UTF-8?q?feat(abi):=20L13=20occupancy=20=E2=80=94?= =?UTF-8?q?=20HWM=20grade=20per=20private=20memory,=20R-2=20at=20a=20bound?= =?UTF-8?q?ary?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit src/abi/TypedWasm/ABI/Occupancy.idr ports and re-proves occupancy-types @ af95728 (Order / Timeline / Reclaim / Witness .agda) over the kernel's HWM instance: R-1 cutFactor (the grade factors at every cut, in any resource algebra), R-2 reclaimLaw / occupancyAtCut (the suffix starts from the prefix's drift), R-3 occupancyLeCost / protocolOccupancyLeCost, R-4 noReclaim / reclaimed, R-5 the occupancy-4 / cost-7 witness. R-6 is tests/reject/{CostIsOccupancy,DriftIsPeak}.idr. Statement correspondence: ASSUMED (port-and-reprove). L13 binding, DESIGNED (no operational semantics or checker behind it): OccupancyGradedMemory carries a private memory's run and proof that its peak fits the declared maximum; BoundaryCut is a run cut at a declared boundary, boundaryFrees = peak − drift of the prefix, boundaryOccupancy is R-2 there, and fitsAcrossBoundary is the budget rule (the run after the boundary fits in what the boundary left). striated regions are surface syntax only, so their occupancy is OPEN. scripts/fetch-siblings.sh pins occupancy-types at af95728; tools/check-kernel-proofs.sh runs its own Agda check (core + 2 rejects) against our resource-algebra pin (its own, b2c9f1f, differs from cf9235c only by a workflow file). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- scripts/fetch-siblings.sh | 6 +- src/abi/TypedWasm/ABI/Occupancy.idr | 243 ++++++++++++++++++++++++++++ src/abi/typed-wasm.ipkg | 2 + tests/reject/CostIsOccupancy.idr | 17 ++ tests/reject/DriftIsPeak.idr | 17 ++ tools/check-kernel-proofs.sh | 14 +- 6 files changed, 296 insertions(+), 3 deletions(-) create mode 100644 src/abi/TypedWasm/ABI/Occupancy.idr create mode 100644 tests/reject/CostIsOccupancy.idr create mode 100644 tests/reject/DriftIsPeak.idr diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh index 20704dc..5d2b313 100755 --- a/scripts/fetch-siblings.sh +++ b/scripts/fetch-siblings.sh @@ -9,14 +9,17 @@ # resource-algebra — the grade kernel; src/abi/TypedWasm/ABI/ResourceAlgebra* # is its Idris2 transcription, and tests/transcription # checks the operation tables against this tree in Agda. +# occupancy-types — the reclamation law (R-1..R-6) that +# src/abi/TypedWasm/ABI/Occupancy.idr ports for L13. # # Re-pin deliberately, one commit per pin, and update the module headers that # cite the pin in the same commit. Override for a local experiment with -# RESOURCE_ALGEBRA_COMMIT= scripts/fetch-siblings.sh +# RESOURCE_ALGEBRA_COMMIT= OCCUPANCY_TYPES_COMMIT= scripts/fetch-siblings.sh set -euo pipefail cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-cf9235c532712a783a404c359a1055f40134794a}" +OCCUPANCY_TYPES_COMMIT="${OCCUPANCY_TYPES_COMMIT:-af957280075699c659de0abd9a3b0defade77309}" fetch() { # fetch local name="$1" commit="$2" dir="_build/dependencies/$1" @@ -37,3 +40,4 @@ fetch() { # fetch } fetch resource-algebra "$RESOURCE_ALGEBRA_COMMIT" +fetch occupancy-types "$OCCUPANCY_TYPES_COMMIT" diff --git a/src/abi/TypedWasm/ABI/Occupancy.idr b/src/abi/TypedWasm/ABI/Occupancy.idr new file mode 100644 index 0000000..e47e53c --- /dev/null +++ b/src/abi/TypedWasm/ABI/Occupancy.idr @@ -0,0 +1,243 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Occupancy.idr — L13 occupancy: the high-water-mark grade of private memory +-- and what a module-isolation boundary reclaims. +-- +-- L13 (ModuleIsolation.idr) proves ACCESS isolation. This module adds the +-- OCCUPANCY reading: a private memory's run is graded in the kernel's HWM +-- instance (peak live state, drift still held at the end), and a declared +-- boundary is a cut in that run. The reclamation law says what the cut +-- frees: the suffix after it starts from the prefix's DRIFT, not its PEAK, +-- so peak − drift is reclaimed at the boundary. +-- +-- PROVENANCE. Ported and re-proved from hyperpolymath/occupancy-types +-- src/OccupancyTypes/{Order,Timeline,Reclaim,Witness}.agda @ af957280075699c659de0abd9a3b0defade77309 +-- (fetched by scripts/fetch-siblings.sh), which states them over +-- resource-algebra's Instances/HWM.agda, the source of +-- TypedWasm.ABI.ResourceAlgebra.HWM. Agda is the proof kernel; these Idris2 +-- proofs are the ABI layer's own. Statement correspondence: ASSUMED +-- (port-and-reprove). Map: Timeline (Agda data) -> List; grade -> timelineGrade; +-- cut-factor -> cutFactor (R-1); reclaim-law / occupancy-at-cut -> +-- reclaimLaw / occupancyAtCut (R-2); occupancy≤cost / protocol-occupancy≤cost +-- -> occupancyLeCost / protocolOccupancyLeCost (R-3); no-reclaim / reclaimed +-- -> noReclaim / reclaimed (R-4); Witness -> witness* (R-5); the R-6 rejects +-- are tests/reject/{CostIsOccupancy,DriftIsPeak}.idr. +-- +-- WHAT IS DESIGNED, NOT PROVED. That the HWM unit is a WebAssembly page of +-- the private memory, that a module's run is the sequence of its phases, and +-- that a declared L13 boundary is where the run is cut: no operational +-- semantics links the grade to `memory.grow` or to actual frees, and no +-- surface checker emits these grades. `striated` regions are surface syntax +-- only (no ABI type), so their occupancy is OPEN. +-- +-- NO believe_me, NO postulate, NO assert_total. %default total. + +module TypedWasm.ABI.Occupancy + +import Data.List +import Data.List.Elem +import Data.Nat + +import TypedWasm.ABI.ResourceAlgebra +import public TypedWasm.ABI.ResourceAlgebra.HWM +import TypedWasm.ABI.ResourceAlgebra.MaxPlus +import TypedWasm.ABI.ModuleIsolation + +%default total + +-- ============================================================================ +-- Order lemmas — occupancy-types Order.agda (beyond what base provides) +-- ============================================================================ + +||| Agda `<-+ʳ`: a positive summand makes the sum strictly bigger. +private +ltPlusPositive : (m : Nat) -> {n : Nat} -> LT 0 n -> LT m (m + n) +ltPlusPositive m {n = S k} _ = + rewrite sym (plusSuccRightSucc m k) in LTESucc (lteAddRight m) + +-- ============================================================================ +-- R-1 A run as the sequence of its phases; the grade factors at every cut +-- (occupancy-types Timeline.agda, parametric in the algebra) +-- ============================================================================ + +||| The grade of a run: its phases in sequence. Agda `Timeline.grade`. +public export +timelineGrade : ResourceAlgebra g => List g -> g +timelineGrade [] = oneG +timelineGrade (x :: xs) = otimes x (timelineGrade xs) + +||| Cutting a run anywhere factors its grade, in any resource algebra. +||| Agda `cut-factor` (R-1). +public export +cutFactor : ResourceAlgebra g => (xs, ys : List g) -> + timelineGrade (xs ++ ys) = otimes (timelineGrade xs) (timelineGrade ys) +cutFactor [] ys = sym (seqUnitL (timelineGrade ys)) +cutFactor (x :: xs) ys = + trans (cong (otimes x) (cutFactor xs ys)) + (sym (seqAssoc x (timelineGrade xs) (timelineGrade ys))) + +-- ============================================================================ +-- R-2 .. R-4 Reclamation at a cut — occupancy-types Reclaim.agda +-- ============================================================================ + +||| The reclamation law: the suffix sees the prefix's drift. Agda +||| `reclaim-law` (R-2). +public export +reclaimLaw : (a, b : HWMGrade) -> + peak (hwmSeq a b) = maximum (peak a) (drift a + peak b) +reclaimLaw (MkHWM _ _ _) (MkHWM _ _ _) = Refl + +||| Occupancy never exceeds cost. Agda `occupancy≤cost` (R-3). +public export +occupancyLeCost : (a, b : HWMGrade) -> LTE (peak (hwmSeq a b)) (peak a + peak b) +occupancyLeCost (MkHWM p1 n1 b1) (MkHWM p2 n2 b2) = + maxLub (lteAddRight p1) (plusLteMonotoneRight p2 n1 p1 b1) + +||| Nothing reclaimed (drift = peak): occupancy IS cost. Agda `no-reclaim` (R-4). +public export +noReclaim : (a : HWMGrade) -> peak a = drift a -> (c : HWMGrade) -> + peak (hwmSeq a c) = peak a + peak c +noReclaim (MkHWM p n b) eq (MkHWM p2 n2 b2) = + rewrite sym eq in + trans (maximumCommutative p (p + p2)) (maxAbsorbLTE (lteAddRight p)) + +||| Strict reclamation: something is released at the cut and the suffix does +||| something, so occupancy is strictly below cost. Agda `reclaimed` (R-4). +public export +reclaimed : (a, c : HWMGrade) -> LT (drift a) (peak a) -> LT 0 (peak c) -> + LT (peak (hwmSeq a c)) (peak a + peak c) +reclaimed (MkHWM p1 n1 b1) (MkHWM p2 n2 b2) lt pos = + maxLub (ltPlusPositive p1 pos) (plusLteMonotoneRight p2 (S n1) p1 lt) + +||| At the level of runs: the cut factorisation plus the law. Agda +||| `occupancy-at-cut` (R-2). +public export +occupancyAtCut : (xs, ys : List HWMGrade) -> + peak (timelineGrade (xs ++ ys)) + = maximum (peak (timelineGrade xs)) + (drift (timelineGrade xs) + peak (timelineGrade ys)) +occupancyAtCut xs ys = + trans (cong peak (cutFactor xs ys)) (reclaimLaw (timelineGrade xs) (timelineGrade ys)) + +||| Agda `protocol-occupancy≤cost` (R-3). +public export +protocolOccupancyLeCost : (xs, ys : List HWMGrade) -> + LTE (peak (timelineGrade (xs ++ ys))) + (peak (timelineGrade xs) + peak (timelineGrade ys)) +protocolOccupancyLeCost xs ys = + rewrite cutFactor xs ys in occupancyLeCost (timelineGrade xs) (timelineGrade ys) + +-- ============================================================================ +-- R-5 Two readings of one run — occupancy-types Witness.agda (computed) +-- ============================================================================ +-- +-- Phase 1 allocates 4 and releases 3 (drift 1); phase 2 allocates 3 and +-- holds it. Occupancy 4 (3 reclaimed at the cut), cost 7. + +public export +witnessA : HWMGrade +witnessA = MkHWM 4 1 (LTESucc LTEZero) + +public export +witnessB : HWMGrade +witnessB = MkHWM 3 3 (LTESucc (LTESucc (LTESucc LTEZero))) + +||| Agda `Witness.occupancy`. +public export +witnessOccupancy : peak (timelineGrade [Occupancy.witnessA, Occupancy.witnessB]) = 4 +witnessOccupancy = Refl + +||| Agda `Witness.cost`. +public export +witnessCost : timelineGrade [Val 4, Val 3] = Val 7 +witnessCost = Refl + +||| Agda `Witness.strict`. +public export +witnessStrict : LT (peak (hwmSeq Occupancy.witnessA Occupancy.witnessB)) + (peak Occupancy.witnessA + peak Occupancy.witnessB) +witnessStrict = + reclaimed witnessA witnessB (LTESucc (LTESucc LTEZero)) (LTESucc LTEZero) + +-- ============================================================================ +-- L13 binding — private memory and boundaries (DESIGNED; see header) +-- ============================================================================ + +||| What a cut reclaims: peak − drift. +public export +reclaimedAt : HWMGrade -> Nat +reclaimedAt g = minus (peak g) (drift g) + +||| What is reclaimed and what is still held make up the peak exactly. +public export +reclaimedPlusDrift : (g : HWMGrade) -> reclaimedAt g + drift g = peak g +reclaimedPlusDrift (MkHWM p n b) = plusMinusLte n p b + +||| A private memory's run stays within its declared maximum (in pages). +public export +data WithinMaximum : PrivateMemory -> HWMGrade -> Type where + ||| No maximum declared. + NoMaximum : {pm : PrivateMemory} -> {g : HWMGrade} -> + pm.maximum = Nothing -> WithinMaximum pm g + ||| The peak does not exceed the declared maximum. + UnderMaximum : {pm : PrivateMemory} -> {g : HWMGrade} -> {m : Nat} -> + pm.maximum = Just m -> LTE (peak g) m -> WithinMaximum pm g + +||| A private memory graded by occupancy: its run, phase by phase, and the +||| proof that the run's high-water mark fits the declaration. +public export +record OccupancyGradedMemory where + constructor MkOccupancyGraded + ||| The L13 private memory. + memory : PrivateMemory + ||| Its run, as consecutive phases. + phases : List HWMGrade + ||| The run's peak fits the declared maximum. + fits : WithinMaximum memory (timelineGrade phases) + +||| A run of an isolated module, cut at one of its declared boundaries. +public export +record BoundaryCut (m : IsolatedModule) where + constructor MkBoundaryCut + ||| The boundary the run crosses. + boundary : Boundary + ||| It is one the module declared (L13 well-formedness applies to it). + declared : Elem boundary m.boundaries + ||| Phases before the boundary. + before : List HWMGrade + ||| Phases after it. + after : List HWMGrade + +||| What the boundary frees: the prefix's peak − drift. +public export +boundaryFrees : BoundaryCut m -> Nat +boundaryFrees c = reclaimedAt (timelineGrade c.before) + +||| R-2 at an L13 boundary: the run after the boundary starts from what the +||| run before it still holds. +public export +boundaryOccupancy : (c : BoundaryCut m) -> + peak (timelineGrade (c.before ++ c.after)) + = maximum (peak (timelineGrade c.before)) + (drift (timelineGrade c.before) + peak (timelineGrade c.after)) +boundaryOccupancy c = occupancyAtCut c.before c.after + +||| R-3 at an L13 boundary: occupancy across a boundary never exceeds the +||| cost of the two sides. +public export +boundaryOccupancyLeCost : (c : BoundaryCut m) -> + LTE (peak (timelineGrade (c.before ++ c.after))) + (peak (timelineGrade c.before) + peak (timelineGrade c.after)) +boundaryOccupancyLeCost c = protocolOccupancyLeCost c.before c.after + +||| The budget rule a checker would apply at a boundary: if the run before +||| fits in `m`, and the run after fits in what the boundary left (m minus +||| the drift), the whole run fits in `m`. +public export +fitsAcrossBoundary : {m : Nat} -> (xs, ys : List HWMGrade) -> + LTE (peak (timelineGrade xs)) m -> + LTE (drift (timelineGrade xs) + peak (timelineGrade ys)) m -> + LTE (peak (timelineGrade (xs ++ ys))) m +fitsAcrossBoundary xs ys before after = + rewrite occupancyAtCut xs ys in maxLub before after diff --git a/src/abi/typed-wasm.ipkg b/src/abi/typed-wasm.ipkg index 9b52812..101afcb 100644 --- a/src/abi/typed-wasm.ipkg +++ b/src/abi/typed-wasm.ipkg @@ -29,6 +29,8 @@ modules = TypedWasm.ABI.Region , TypedWasm.ABI.ResourceAlgebra.MaxPlus , TypedWasm.ABI.ResourceAlgebra.HWM , TypedWasm.ABI.ResourceAlgebra.Separation + -- L13 occupancy (PWL-01 step 3): R-1..R-5 ported from occupancy-types @ af95728 + , TypedWasm.ABI.Occupancy , TypedWasm.ABI.Echo , TypedWasm.ABI.Tropical , TypedWasm.ABI.Epistemic diff --git a/tests/reject/CostIsOccupancy.idr b/tests/reject/CostIsOccupancy.idr new file mode 100644 index 0000000..8fd9afc --- /dev/null +++ b/tests/reject/CostIsOccupancy.idr @@ -0,0 +1,17 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- MUST FAIL (tools/check-kernel-proofs.sh). Mirrors occupancy-types +-- tests/reject/CostIsOccupancy.agda @ af95728 (R-6). +-- +-- Occupancy of a sequence is not the sum of the peaks. Reading it as cost +-- would charge an L13 run for memory its boundary has already reclaimed. +-- EXPECT: Can't solve constraint between: plus .* and maximum p \(n \+ p'\) +module CostIsOccupancy + +import TypedWasm.ABI.ResourceAlgebra.HWM + +%default total + +invalid : (a, c : HWMGrade) -> peak (hwmSeq a c) = peak a + peak c +invalid (MkHWM p n b) (MkHWM p' n' b') = Refl diff --git a/tests/reject/DriftIsPeak.idr b/tests/reject/DriftIsPeak.idr new file mode 100644 index 0000000..82f10ef --- /dev/null +++ b/tests/reject/DriftIsPeak.idr @@ -0,0 +1,17 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- MUST FAIL (tools/check-kernel-proofs.sh). Mirrors occupancy-types +-- tests/reject/DriftIsPeak.agda @ af95728 (R-6). +-- +-- What is live at a cut is not the peak reached before it; identifying them +-- is exactly "an L13 boundary never reclaims anything". +-- EXPECT: Mismatch between: p and n +module DriftIsPeak + +import TypedWasm.ABI.ResourceAlgebra.HWM + +%default total + +invalid : (a : HWMGrade) -> drift a = peak a +invalid (MkHWM p n b) = Refl diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh index 2257d5f..b112a7f 100755 --- a/tools/check-kernel-proofs.sh +++ b/tools/check-kernel-proofs.sh @@ -4,8 +4,8 @@ # # check-kernel-proofs.sh — the mechanical falsifiers behind the grade kernel. # -# 1. upstream resource-algebra's own check at the pin (Agda --safe -# --without-K --no-libraries --double-check + its 3 rejects) +# 1. upstream resource-algebra's and occupancy-types' own checks at the pins (Agda --safe +# --without-K --no-libraries --double-check + their rejects) # 2. build idris2 --build src/abi/typed-wasm.ipkg: exit 0 AND no # `Error:` line (idris2 can exit 0 while printing an error) # 3. rejects every tests/reject/*.idr must FAIL, at its `invalid` @@ -57,6 +57,16 @@ if (cd "$RA" && AGDA=agda bash scripts/check-agda.sh) > "$OUT/upstream.log" 2>&1 else cat "$OUT/upstream.log"; err "upstream resource-algebra check failed at the pin" fi +# occupancy-types (L13's reclamation law), checked against OUR resource-algebra +# pin: its own pin (b2c9f1f) differs from cf9235c only by a CI workflow file. +OCC="_build/dependencies/occupancy-types" +[ -d "$OCC/src/OccupancyTypes" ] || die "occupancy-types not fetched — run scripts/fetch-siblings.sh" +echo "occupancy-types at $(git -C "$OCC" rev-parse HEAD)" +if (cd "$OCC" && AGDA=agda RESOURCE_ALGEBRA_SRC="$ROOT/$RA/src" bash scripts/check-agda.sh) > "$OUT/upstream-occupancy.log" 2>&1; then + pass "upstream occupancy-types: $(tail -1 "$OUT/upstream-occupancy.log")" +else + cat "$OUT/upstream-occupancy.log"; err "upstream occupancy-types check failed at the pin" +fi # 2 — the ABI package --------------------------------------------------------- # From clean, so a stale TTC cannot mask an error. From 84e1427cb163f50b38d0fe9224ad01b6cfa544ad Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:11:53 +0000 Subject: [PATCH 10/13] =?UTF-8?q?docs:=20LEVEL-STATUS=20rows=2011=E2=80=93?= =?UTF-8?q?13=20name=20the=20kernel=20artefacts?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rows 11, 12 and 13 now say which kernel artefact each obligation draws on and with what status: PROVEN for the Idris2 theorems, ASSUMED for the port's correspondence to occupancy-types, DESIGNED for the worst-case obligation and the L13 binding, OPEN for striated occupancy. No row moves to achieved; L11 and L12 stay draft. New inventory row for Occupancy.idr, CHANGELOG entry, reject README rows, and 18 names pinned in tests/proof/regression.mjs. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- CHANGELOG.adoc | 22 ++++++++++++++++++++ LEVEL-STATUS.adoc | 42 +++++++++++++++++++++++++++++++++----- tests/proof/regression.mjs | 20 ++++++++++++++++++ tests/reject/README.adoc | 7 ++++++- 4 files changed, 85 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 9a0973c..356a2c7 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,6 +9,28 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== L11 / L12 / L13 read through the grade kernel (PWL-01 steps 2–3, 2026-10-14) + +* *L11.* `CostBounded c n` is proved equal to the kernel's Loss order + `Finite n ≼ c`, and path bounds compose by the kernel's `otimesMono` + (`costBoundedSeq`). New `Level11WorstCaseProof` grades a branching access + plan in MaxPlus (`worstCaseThen`, `worstCaseOneOf`). It is DESIGNED: no + surface syntax or attestation uses it. The bottleneck stays MinMax. +* *L12.* `stalenessGrade` is the reader's lag as a Loss grade: fresh = 𝟙, + stale ≠ 𝟙, never synced = 𝟘, and relayed lag = ⊗ (`stalenessRelay`). + `syncGrade` now carries a note that its number is a version, not a loss. +* *L13.* New `Occupancy.idr` ports occupancy-types @ `af95728` R-1..R-5 + (reclamation law, occupancy ≤ cost, strict reclamation, the 4-vs-7 witness) + over the kernel's HWM. It binds them to `private_memory` (an HWM grade within + the declared maximum) and to `boundary` (the cut that frees peak − drift). + The binding is DESIGNED. +* Kernel additions: each instance's order read in ℕ (`lossLeOfLTE`, + `maxPlusLeOfLTE` and inverses); `ResourceAlgebra/Nat.idr` gains `maxLub` + and min/max-vs-`LTE` lemmas. These are typed-wasm's own, labelled as such. +* New rejects: `CostIsOccupancy`, `DriftIsPeak` (occupancy-types R-6) and + `WorstCaseIsCheapest`. `tools/check-kernel-proofs.sh` also runs + occupancy-types' own Agda check at its pin. + ==== Grade kernel: resource-algebra ported as the ABI's one source of grades (PWL-01, 2026-10-14) `src/abi/TypedWasm/ABI/ResourceAlgebra.idr` and `ResourceAlgebra/{Nat,Loss, diff --git a/LEVEL-STATUS.adoc b/LEVEL-STATUS.adoc index 88868f6..aa243e8 100644 --- a/LEVEL-STATUS.adoc +++ b/LEVEL-STATUS.adoc @@ -154,7 +154,16 @@ monotonicity, mirrors `+tropical-resource-typing+` `+Bridge.hub_ceiling_le+`), `+ResidueMeasure+` (E→R, mirrors `+Resource.EchoBridge+`), and `+Level11BottleneckProof+` + `+bottleneckCeilsEdges+` wired into -`+Proofs.attestL11_Bottleneck+`/`+_Sound+`.* +`+Proofs.attestL11_Bottleneck+`/`+_Sound+`. PWL-01 step 2: the +obligations read through the kernel — `+CostBounded c n+` IS the Loss +order `+Finite n ≼ c+` (`+costBoundedIsLossOrder+` / +`+lossOrderIsCostBounded+`, PROVEN) and path bounds compose by the +kernel's `+otimesMono+` (`+costBoundedSeq+`, PROVEN); +`+Level11WorstCaseProof+` grades a branching plan in MaxPlus with +`+worstCaseThen+` / `+worstCaseOneOf+` from `+otimesMono+` / +`+oplusMono+` (PROVEN; the obligation itself DESIGNED — no surface or +attestation uses it). `+Level11BottleneckProof+` is MinMax, not MaxPlus, +and stays as it is (`+tests/reject/TropicalIsNotMaxPlus.idr+`).* |12 |Epistemic safety |Epistemic.idr |Not yet |None |*In package (A1, 2026-04-18); A10 (2026-05-26) closes the "`freshness propagation under @@ -165,11 +174,28 @@ sibling `+Tropical.TropCost+` (∞ = never-synced) + `+neverSyncedInfeasible+`/`+observedFeasible+`/`+observedNotInfeasible+` — extant Nat-indexed proofs untouched. Header IS-NOT note: this read-consistency model is a DIFFERENT problem from canonical -`+epistemic-types+`’ standpoint-indexed modality.* - -|13 |Module isolation |ModuleIsolation.idr |(per-module handles, future) +`+epistemic-types+`’ standpoint-indexed modality. PWL-01 step 2: +staleness graded in the kernel's Loss — `+stalenessGrade+` is the lag; +fresh is 𝟙 (`+freshHasNoStaleness+`), stale is not (`+staleHasStaleness+`), +never-synced is 𝟘 (`+neverSyncedIsCollapse+`), and a relayed lag is the +kernel's ⊗ (`+stalenessRelay+`), all PROVEN. `+syncGrade+` is kept but +holds a version, not a loss: ordering it with the kernel order would rank +older versions higher.* + +|13 |Module isolation |ModuleIsolation.idr + Occupancy.idr |(per-module handles, future) |12 parser/Checker tests |*v1.2 — Idris2 proof + surface checker live; -007 lowering DONE (task #5)* +007 lowering DONE (task #5). PWL-01 step 3: occupancy graded in the +kernel's HWM — R-1..R-5 of occupancy-types @ `+af95728+` re-proved in +Idris2 (`+cutFactor+`, `+reclaimLaw+`, `+occupancyAtCut+`, +`+occupancyLeCost+`, `+noReclaim+`, `+reclaimed+`, `+witness*+`: PROVEN; +statement correspondence ASSUMED, port-and-reprove), R-6 as +`+tests/reject/{CostIsOccupancy,DriftIsPeak}.idr+` (TESTED). The L13 +binding — an HWM grade per `+private_memory+` within its declared +maximum (`+OccupancyGradedMemory+`), a declared `+boundary+` as the cut +that frees peak − drift (`+BoundaryCut+`, `+boundaryOccupancy+`, +`+fitsAcrossBoundary+`) — is DESIGNED: nothing links the grade to +`+memory.grow+` and no checker emits it. `+striated+` occupancy OPEN +(surface-only construct).* |14 |Session protocols |SessionProtocol.idr |(typed-state handles, future) |13 parser/Checker tests |*v1.3 — Idris2 proof + surface checker @@ -372,6 +398,12 @@ pinned sources and by Idris2 `+Refl+` against the port, with a LossWorstCase, DriftExceedsPeak, TropicalIsNotMaxPlus}.idr+` refused for the intended reason. +|Occupancy.idr |0 |0 |0 |In package (PWL-01 step 3, 2026-10-14). L13 +occupancy over the kernel's HWM grade: occupancy-types +(`+Reclaim.agda+` / `+Timeline.agda+` / `+Witness.agda+` @ `+af95728+`) +R-1..R-5 ported and re-proved; L13 binding (`+OccupancyGradedMemory+`, +`+BoundaryCut+`, `+boundaryFrees+`, `+fitsAcrossBoundary+`) DESIGNED. + |VerifierSpec.idr |0 |0 |0 |Introduced A13 (2026-05-26, PR #72) as statement-level spec-of-record for post-A10 items 7+8. *Promoted to total bodies 2026-05-27 (PR #79)*: same `+ModuleSummary+` / diff --git a/tests/proof/regression.mjs b/tests/proof/regression.mjs index 1e6c794..6a0c52d 100644 --- a/tests/proof/regression.mjs +++ b/tests/proof/regression.mjs @@ -239,6 +239,26 @@ const EXPECTED = [ ["Echo.idr", /^EchoGrade\s*:/m, "Echo loss grade = the kernel's Loss carrier"], ["Echo.idr", /^echoCollapseAbsorbs\s*:/m, "Total collapse absorbs later loss (kernel annihilL)"], + // PWL-01 step 2-3: L11 / L12 obligations read through the kernel, L13 occupancy. + ["Tropical.idr", /^costBoundedIsLossOrder\s*:/m, "L11 bound = kernel Loss order"], + ["Tropical.idr", /^lossOrderIsCostBounded\s*:/m, "L11 kernel Loss order = bound"], + ["Tropical.idr", /^costBoundedSeq\s*:/m, "L11 path bounds compose (kernel otimesMono)"], + ["Tropical.idr", /^record\s+Level11WorstCaseProof/m, "L11 MaxPlus worst-case obligation"], + ["Tropical.idr", /^worstCaseThen\s*:/m, "L11 worst case: sequence bounds add"], + ["Tropical.idr", /^worstCaseOneOf\s*:/m, "L11 worst case: choice takes the larger bound"], + ["Epistemic.idr", /^stalenessGrade\s*:/m, "L12 staleness as a Loss grade"], + ["Epistemic.idr", /^freshHasNoStaleness\s*:/m, "L12 fresh = kernel 𝟙"], + ["Epistemic.idr", /^staleHasStaleness\s*:/m, "L12 stale ≠ kernel 𝟙"], + ["Epistemic.idr", /^stalenessRelay\s*:/m, "L12 relayed lag = kernel ⊗"], + ["Occupancy.idr", /^cutFactor\s*:/m, "R-1 grade factors at every cut"], + ["Occupancy.idr", /^reclaimLaw\s*:/m, "R-2 reclamation law"], + ["Occupancy.idr", /^occupancyAtCut\s*:/m, "R-2 at the level of runs"], + ["Occupancy.idr", /^occupancyLeCost\s*:/m, "R-3 occupancy ≤ cost"], + ["Occupancy.idr", /^reclaimed\s*:/m, "R-4 strict reclamation"], + ["Occupancy.idr", /^witnessOccupancy\s*:/m, "R-5 occupancy 4 / cost 7"], + ["Occupancy.idr", /^boundaryOccupancy\s*:/m, "L13 boundary frees peak − drift"], + ["Occupancy.idr", /^fitsAcrossBoundary\s*:/m, "L13 budget rule across a boundary"], + // Proofs.idr — LevelAttestationW (standards#130 long-tail closure): // witness-indexed attestation GADT with per-level smart ctors, // extractors ("entails-semantic-property" lemmas), legacy bridge, diff --git a/tests/reject/README.adoc b/tests/reject/README.adoc index 6f508ba..be1dd71 100644 --- a/tests/reject/README.adoc +++ b/tests/reject/README.adoc @@ -15,7 +15,12 @@ because then the control proves nothing. | `LossWorstCase` | echo's alternatives read as max, i.e. loss treated as cost (S-2) | `DriftExceedsPeak` | a run ending with more live state than its peak | `TropicalIsNotMaxPlus` | L11's `TropCost` read as max-plus (it is min-plus) +| `CostIsOccupancy` | an L13 run charged the sum of its peaks, as if the boundary reclaimed nothing (occupancy-types R-6) +| `DriftIsPeak` | drift identified with peak: "a boundary never reclaims" (occupancy-types R-6) +| `WorstCaseIsCheapest` | L11's MaxPlus worst case charging the cheaper branch |=== -The first three mirror resource-algebra `tests/reject/*.agda` at the pin in +`HWMAnnihilates`, `LossWorstCase` and `DriftExceedsPeak` mirror resource-algebra +`tests/reject/*.agda`; `CostIsOccupancy` and `DriftIsPeak` mirror occupancy-types +`tests/reject/*.agda`, both at the pins in `scripts/fetch-siblings.sh`. From e080ef6121e14eac2f5902b9e491c6a990647a27 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:15:01 +0000 Subject: [PATCH 11/13] =?UTF-8?q?fix(deps):=20repair=20Cargo.lock=20?= =?UTF-8?q?=E2=80=94=20wasmparser=20listed=20twice=20since=20#231=E2=80=93?= =?UTF-8?q?#233?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit cargo-verify (E2E Validation) fails before compiling anything: error: failed to parse lock file ... package `wasmparser` is specified twice in the lockfile Three Dependabot PRs (#231 wasm-encoder, #232 wasmprinter, #233 wasmparser), each moving to 0.256.0, merged on top of each other and left two `wasmparser 0.256.0` entries plus a stale 0.255.0 one that a crate still pointed at. It went unseen because E2E Validation was startup_failure until #270. The lock was rewritten by cargo itself (`cargo metadata` after dropping the duplicated entry), not by hand: one dependency edge 0.255.0 -> 0.256.0, the 0.255.0 entry and the duplicate removed, nothing upgraded. `cargo build --workspace --locked` and `cargo test --workspace --locked` pass (all test binaries ok). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- Cargo.lock | 24 +----------------------- 1 file changed, 1 insertion(+), 23 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 447e750..1f6077d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -224,7 +224,7 @@ version = "0.1.0" dependencies = [ "thiserror", "wasm-encoder 0.256.0", - "wasmparser 0.255.0", + "wasmparser 0.256.0", ] [[package]] @@ -320,17 +320,6 @@ dependencies = [ "indexmap", ] -[[package]] -name = "wasmparser" -version = "0.255.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e8e329ef4b5d46e73b91d3ac6924417cad55a8cbbf869c199283383427c3320b" -dependencies = [ - "bitflags", - "indexmap", - "semver", -] - [[package]] name = "wasmparser" version = "0.256.0" @@ -344,17 +333,6 @@ dependencies = [ "serde", ] -[[package]] -name = "wasmparser" -version = "0.256.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "60bd825ffedc6cba8a642924ba7ae424afbc47811cffbcb7b92031ec24e59b4c" -dependencies = [ - "bitflags", - "indexmap", - "semver", -] - [[package]] name = "wasmprinter" version = "0.256.0" From eec5e50824ffad7a72999cc43a59fc9b168f9ad7 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:28:36 +0000 Subject: [PATCH 12/13] style(abi): bind module/field implicits in the L12 staleness layer The four staleness lemmas auto-bound `mod` and `field`, adding four "implicitly bind ... shadowing Prelude.Num.mod / FieldVersion.field" warnings to the build (28 against main's 24). Binding them explicitly as `{0 m : ModuleId} -> {0 f : String}` returns the build to main's 24 warnings, none from this PR. No statement changes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- src/abi/TypedWasm/ABI/Epistemic.idr | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/abi/TypedWasm/ABI/Epistemic.idr b/src/abi/TypedWasm/ABI/Epistemic.idr index cc1731b..57753ab 100644 --- a/src/abi/TypedWasm/ABI/Epistemic.idr +++ b/src/abi/TypedWasm/ABI/Epistemic.idr @@ -448,28 +448,31 @@ stalenessGrade known current = Finite (minus current known) ||| Staleness of a knowledge state against the field's current version. ||| Never observed is total collapse. public export -knowledgeStaleness : {ver : Nat} -> Knowledge mod field ver -> (current : Nat) -> LossGrade +knowledgeStaleness : {0 m : ModuleId} -> {0 f : String} -> {ver : Nat} -> + Knowledge m f ver -> (current : Nat) -> LossGrade knowledgeStaleness {ver} (Observed _) current = stalenessGrade ver current knowledgeStaleness Unknown _ = Infinity ||| Fresh knowledge loses nothing: its staleness is the kernel's 𝟙. public export -freshHasNoStaleness : Fresh mod field known current -> +freshHasNoStaleness : {0 m : ModuleId} -> {0 f : String} -> {known, current : Nat} -> + Fresh m f known current -> stalenessGrade known current = oneG {g = LossGrade} freshHasNoStaleness (MkFresh _ _ _ eq) = rewrite eq in cong Finite (sym (minusZeroN current)) ||| Stale knowledge loses something: its staleness is not 𝟙. public export -staleHasStaleness : Stale mod field known current -> +staleHasStaleness : {0 m : ModuleId} -> {0 f : String} -> {known, current : Nat} -> + Stale m f known current -> Not (stalenessGrade known current = oneG {g = LossGrade}) staleHasStaleness (MkStale lt) prf = succNotLTEzero (replace {p = \x => LT 0 x} (finiteInjective prf) (minusPos lt)) ||| Never-synced knowledge is the kernel's 𝟘 (total collapse). public export -neverSyncedIsCollapse : (current : Nat) -> - knowledgeStaleness {mod} {field} Unknown current = zeroG {g = LossGrade} +neverSyncedIsCollapse : {0 m : ModuleId} -> {0 f : String} -> (current : Nat) -> + knowledgeStaleness {m} {f} Unknown current = zeroG {g = LossGrade} neverSyncedIsCollapse _ = Refl ||| Every staleness is at or below fresh in the Loss order: 𝟙 is the top. From 921f00ae71fd86b0b8b9619ed5be6cd3b5de6d1a Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:31:22 +0000 Subject: [PATCH 13/13] =?UTF-8?q?fix(ci):=20revert=20#265's=20smtp-notify-?= =?UTF-8?q?action=20bump=20=E2=80=94=20off=20actions.lock?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit governance / Actions lockfile verify fails on main and on every PR: workflow uses ref "v0.5.0" but lockfile pins "v0.3.0" (.github/workflows/push-email-notify.yml) Dependabot #265 bumped hyperpolymath/smtp-notify-action v0.3.0 -> v0.5.0 without a lock refresh, the same drift #266 and #270 reverted elsewhere (#270 left this one alone because #268 did not cause it). Back to the locked v0.3.0; recurrence needs the lock refreshed with the bump (owner decision, as in #270). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- .github/workflows/push-email-notify.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/push-email-notify.yml b/.github/workflows/push-email-notify.yml index f4765e1..438d01a 100644 --- a/.github/workflows/push-email-notify.yml +++ b/.github/workflows/push-email-notify.yml @@ -40,7 +40,7 @@ jobs: timeout-minutes: 5 steps: - name: Send push notification email - uses: hyperpolymath/smtp-notify-action@v0.5.0 + uses: hyperpolymath/smtp-notify-action@v0.3.0 with: server_address: ${{ secrets.SMTP_HOST }} server_port: ${{ secrets.SMTP_PORT }}