From d52729598bd93bdd0271b790291ec5d2337a8e14 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 00:59:20 +0000 Subject: [PATCH 1/4] 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 2/4] 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 3/4] 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 4/4] 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