From 26832aad06bfb39b93219fadde2b29b9ad5e7f2f Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 11:11:15 +0000 Subject: [PATCH 1/3] feat(abi): MinMax joins the grade kernel; tropMax is its sequence Transcribes resource-algebra Instances/MinMax.agda (resource-algebra#4) as ResourceAlgebra/MinMax.idr: minMaxSeq (max, Infinity absorbing) on Loss's carrier with Loss's alternatives. The instance and its dioid, ordered and annihilating layers are named implementations, because ResourceAlgebra LossGrade is already Loss. - Tropical.tropMax = minMaxSeq; tools/grade-kernel.allow is empty and the gate expects exactly one min-max definition, in MinMax.idr. - Nat.idr: minOfLTE, maxDistribLMin, maxDistribRMin. - Separation S-4 bottleneckIsNotSum; new reject MinMaxIsLoss. - Transcription table: MinMax sequence rows (197 rows, 269 equalities) and a fourth wrong row. - resource-algebra pin cf9235c -> 0b338c9 (Core, Loss, MaxPlus, HWM unchanged). occupancy-types needs hyperpolymath/occupancy-types#11 to check against it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- .github/workflows/contract-gate.yml | 4 +- CHANGELOG.adoc | 22 +++ CONTRACT.adoc | 4 +- LEVEL-STATUS.adoc | 61 ++++---- scripts/fetch-siblings.sh | 2 +- src/abi/TypedWasm/ABI/ResourceAlgebra.idr | 3 +- src/abi/TypedWasm/ABI/ResourceAlgebra/HWM.idr | 3 +- .../TypedWasm/ABI/ResourceAlgebra/Loss.idr | 3 +- .../TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr | 3 +- .../TypedWasm/ABI/ResourceAlgebra/MinMax.idr | 139 ++++++++++++++++++ src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr | 32 +++- .../ABI/ResourceAlgebra/Separation.idr | 29 +++- src/abi/TypedWasm/ABI/Tropical.idr | 32 ++-- src/abi/typed-wasm.ipkg | 5 +- tests/proof/regression.mjs | 11 +- tests/reject/MinMaxIsLoss.idr | 19 +++ tests/reject/README.adoc | 3 +- tests/transcription/Explore.idr | 6 +- tests/transcription/README.adoc | 3 +- tests/transcription/gen.sh | 13 +- tests/transcription/ops.tsv | 27 +++- tests/transcription/wrong-rows.tsv | 2 + tools/check-grade-kernel.sh | 11 +- tools/check-kernel-proofs.sh | 3 +- tools/grade-kernel.allow | 1 - 25 files changed, 371 insertions(+), 70 deletions(-) create mode 100644 src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr create mode 100644 tests/reject/MinMaxIsLoss.idr diff --git a/.github/workflows/contract-gate.yml b/.github/workflows/contract-gate.yml index 93ef94e..41157d6 100644 --- a/.github/workflows/contract-gate.yml +++ b/.github/workflows/contract-gate.yml @@ -29,7 +29,7 @@ jobs: - name: Run contract gate run: bash tools/check-contract.sh - # Grade kernel (PWL-01): the one definition of min-plus and of max-plus. + # Grade kernel (PWL-01): the one definition of min-plus, max-plus and min-max. # 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 @@ -48,7 +48,7 @@ jobs: # 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) + # PINNED Agda kernel (resource-algebra at the fetch-siblings.sh pin, 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 source with Chez Scheme, diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 6543e0f..92ec778 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,6 +9,28 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== MinMax joins the grade kernel (2026-10-14) + +* New `ResourceAlgebra/MinMax.idr` transcribes resource-algebra + `Instances/MinMax.agda` (hyperpolymath/resource-algebra#4): the bottleneck + sequence `minMaxSeq` (max, ∞ absorbing) on Loss's carrier, with Loss's + alternatives. The instance and its dioid, ordered and annihilating layers + are named implementations (`@{minMax}`, ...), because Idris2 resolves by + carrier and `ResourceAlgebra LossGrade` is Loss. +* `Tropical.tropMax = minMaxSeq`. It was the one grade operation defined + outside the kernel, so `tools/grade-kernel.allow` is now empty and the gate + names a third single definition (min-max). +* `ResourceAlgebra/Nat.idr`: `minOfLTE`, `maxDistribLMin`, `maxDistribRMin` + (upstream `min-≤`, `max-distribˡ-min`, `max-distribʳ-min`). +* Separation S-4 `bottleneckIsNotSum`. New reject `MinMaxIsLoss`. The + transcription table gains the MinMax sequence: 197 rows, 269 equalities, + and a fourth wrong row. +* resource-algebra pin `cf9235c` → `0b338c9`. Core, Loss, MaxPlus and HWM are + unchanged between the two; the kernel headers cite the new pin. + occupancy-types is checked against this pin and needs + hyperpolymath/occupancy-types#11 (its order lemmas now clash with the new + Prelude's); the occupancy-types pin moves when that merges. + ==== Fixed (2026-10-14) * `Occupancy.WithinMaximum`: `UnderMaximum` now bounds a private memory's diff --git a/CONTRACT.adoc b/CONTRACT.adoc index 7cd9384..46c0f5f 100644 --- a/CONTRACT.adoc +++ b/CONTRACT.adoc @@ -94,8 +94,8 @@ and runnable locally / as a pre-commit step): - *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 one definition of min-plus, of max-plus and of min-max; 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`. diff --git a/LEVEL-STATUS.adoc b/LEVEL-STATUS.adoc index 99f61a9..65e4552 100644 --- a/LEVEL-STATUS.adoc +++ b/LEVEL-STATUS.adoc @@ -374,9 +374,10 @@ predicate. |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+`. +re-derived from `+ResourceAlgebra/Loss.idr+`. 2026-10-14: `+tropMax+` +(the bottleneck) is the kernel's MinMax sequence (`+tropMax = minMaxSeq+`, +`+ResourceAlgebra/MinMax.idr+`), so no grade operation is defined outside +the kernel and `+tools/grade-kernel.allow+` is empty. |Epistemic.idr |0 |0 |0 |In package (A1, 2026-04-18). A10 (2026-05-26): propagation theorems added — `+freshImpliesEqual+`, `+staleImpliesLT+`, @@ -404,20 +405,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 +|ResourceAlgebra.idr + ResourceAlgebra/{Nat,Loss,MaxPlus,HWM,MinMax,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+`); +(max-plus), HWM (high-water-mark) and MinMax (min-max, bottleneck; named +implementations on Loss's carrier) instances, transcribed from +`+hyperpolymath/resource-algebra+` @ `+0b338c9+` (Agda `+--safe +--without-K+`; MinMax added 2026-10-14, the rest unchanged since `+cf9235c+`). 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 +on a 197-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 +4-row negative control refused by both +(`+tools/check-kernel-proofs.sh+`). Separation S-1..S-4 TESTED (computed). Negative controls `+tests/reject/{HWMAnnihilates, -LossWorstCase, DriftExceedsPeak, TropicalIsNotMaxPlus}.idr+` refused -for the intended reason. +LossWorstCase, DriftExceedsPeak, TropicalIsNotMaxPlus, MinMaxIsLoss}.idr+` +refused for the intended reason. |Occupancy.idr |0 |0 |0 |In package (PWL-01 step 3, 2026-10-14). L13 occupancy over the kernel's HWM grade: occupancy-types @@ -641,36 +643,43 @@ rule. 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 +`+hyperpolymath/resource-algebra+` @ `+0b338c9+`, 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 +`+scripts/fetch-siblings.sh+`. It holds the only min-plus (Loss), the only +max-plus (MaxPlus) and the only min-max (MinMax, the bottleneck) 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 +* The interface laws and the four 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. + 197-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 + accepts it by `+Refl+` against the port. Four 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 +* The 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. + opposite ways, S-4 a bottleneck is not a sum (`+ResourceAlgebra/Separation.idr+`, + computed). So L11's latency cost (Loss carrier), its bottleneck (MinMax), 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. +`+tests/reject/TropicalIsNotMaxPlus.idr+` is the checked statement. + +*Resolved 2026-10-14.* The owner ruled to add MinMax upstream +(hyperpolymath/resource-algebra#4, at the pin `+0b338c9+`). +`+ResourceAlgebra/MinMax.idr+` transcribes it, `+tropMax+` is its sequence, +`+tests/reject/MinMaxIsLoss.idr+` refuses reading it as a sum, and +`+tools/grade-kernel.allow+` is empty. Upstream's strict and lax morphisms +(`+Morphism.agda+`) are not ported. Level11BottleneckProof's status does not +move: the bottleneck's laws were already proved; what changed is where its +sequence is defined. No level changes status here: L11 and L12 stay draft. diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh index 3833578..8040cb1 100755 --- a/scripts/fetch-siblings.sh +++ b/scripts/fetch-siblings.sh @@ -21,7 +21,7 @@ set -euo pipefail cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." -RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-cf9235c532712a783a404c359a1055f40134794a}" +RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe}" OCCUPANCY_TYPES_COMMIT="${OCCUPANCY_TYPES_COMMIT:-af957280075699c659de0abd9a3b0defade77309}" CHOREOGRAPHIC_TYPES_COMMIT="${CHOREOGRAPHIC_TYPES_COMMIT:-edb784a7d26c276c2abfa8399b773d346dbb101e}" diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra.idr index 8fe360a..affa889 100644 --- a/src/abi/TypedWasm/ABI/ResourceAlgebra.idr +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra.idr @@ -10,7 +10,8 @@ -- (tools/check-grade-kernel.sh enforces that). -- -- PROVENANCE. Transcribed from hyperpolymath/resource-algebra --- src/ResourceAlgebra/Core.agda @ cf9235c532712a783a404c359a1055f40134794a +-- src/ResourceAlgebra/Core.agda @ 0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe +-- (unchanged since cf9235c, the pin it was first transcribed at) -- (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 diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/HWM.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/HWM.idr index 6335061..df35fd5 100644 --- a/src/abi/TypedWasm/ABI/ResourceAlgebra/HWM.idr +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/HWM.idr @@ -7,7 +7,8 @@ -- (resource-algebra H-2); PROVEN against the definition below. -- -- Transcribed from hyperpolymath/resource-algebra --- src/ResourceAlgebra/Instances/HWM.agda @ cf9235c532712a783a404c359a1055f40134794a +-- src/ResourceAlgebra/Instances/HWM.agda @ 0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe +-- (unchanged since cf9235c, the pin it was first transcribed at) -- 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. diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr index 4cf0917..504435a 100644 --- a/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr @@ -8,7 +8,8 @@ -- loss grade are this carrier, not copies of it. -- -- Transcribed from hyperpolymath/resource-algebra --- src/ResourceAlgebra/Instances/Loss.agda @ cf9235c532712a783a404c359a1055f40134794a +-- src/ResourceAlgebra/Instances/Loss.agda @ 0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe +-- (unchanged since cf9235c, the pin it was first transcribed at) -- which is itself the echo-types loss grade -- (echo-types experimental/echo-additive/Grade.agda). -- Correspondence status: ASSUMED (transcription); operation table TESTED on diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr index f921103..820b97f 100644 --- a/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr @@ -6,7 +6,8 @@ -- 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 +-- src/ResourceAlgebra/Instances/MaxPlus.agda @ 0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe +-- (unchanged since cf9235c, the pin it was first transcribed at) -- 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) diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr new file mode 100644 index 0000000..e1fe363 --- /dev/null +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr @@ -0,0 +1,139 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- ResourceAlgebra/MinMax.idr — the min-max (bottleneck) grade on ℕ ∪ {∞}. +-- +-- THE ONE DEFINITION OF THE BOTTLENECK SEQUENCE IN THIS TREE. +-- TypedWasm.ABI.Tropical's `tropMax` (the L11 bottleneck layer, +-- Level11BottleneckProof) is `minMaxSeq`, not a copy of it. +-- +-- Transcribed from hyperpolymath/resource-algebra +-- src/ResourceAlgebra/Instances/MinMax.agda @ 0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe +-- Correspondence status: ASSUMED (transcription); the sequence's operation +-- table is TESTED on both sides by tests/transcription. +-- +-- Renaming (the only change from the Agda text): _⊔g_ is minMaxSeq; the +-- carrier and the alternatives are Loss's own (Agda imports Loss's Grade, +-- fin / inf and _⊓g_; here LossGrade, Finite / Infinity and lossAlt). +-- Clause order is kept. +-- +-- minMaxSeq = sequence = MAX (the worst hop) — the "⊗", unit Finite 0 +-- lossAlt = alternatives = MIN (the better path) — the "⊕", unit Infinity +-- Infinity absorbs under both: an unreachable hop makes the path unreachable, +-- and an unreachable alternative is never chosen. +-- +-- The carrier is shared with Loss ON PURPOSE (upstream Morphism.agda, +-- `loss-bottleneck`: the identity on the carrier is a lax morphism Loss → +-- MinMax, because a bottleneck never exceeds the sum). Idris2 resolves an +-- interface by its carrier, and `ResourceAlgebra LossGrade` is already Loss, +-- so this instance and its layers are NAMED implementations: use them with +-- `@{minMax}`, `@{minMaxDioid}`, ... . They never take part in search. +-- +-- Neither min-plus (sequence is max, not +) nor max-plus (max is the +-- sequence, not the alternatives, and 𝟘 is ∞, not −∞): Separation.idr S-4 +-- and tests/reject/MinMaxIsLoss.idr are the checked statements. +-- +-- NO believe_me, NO postulate, NO assert_total. %default total. + +module TypedWasm.ABI.ResourceAlgebra.MinMax + +import public Data.Nat +import TypedWasm.ABI.ResourceAlgebra +import TypedWasm.ABI.ResourceAlgebra.Nat +import public TypedWasm.ABI.ResourceAlgebra.Loss + +%default total + +||| Sequence: the worst hop. Agda `_⊔g_`. +public export +minMaxSeq : LossGrade -> LossGrade -> LossGrade +minMaxSeq Infinity _ = Infinity +minMaxSeq (Finite m) Infinity = Infinity +minMaxSeq (Finite m) (Finite n) = Finite (maximum m n) + +-- ============================================================================ +-- Sequence: (minMaxSeq, Finite 0) is a monoid +-- ============================================================================ + +||| Agda `⊔g-assoc`. +public export +minMaxSeqAssoc : (a, b, c : LossGrade) -> + minMaxSeq (minMaxSeq a b) c = minMaxSeq a (minMaxSeq b c) +minMaxSeqAssoc (Finite a) (Finite b) (Finite c) = cong Finite (maxAssoc a b c) +minMaxSeqAssoc (Finite a) (Finite b) Infinity = Refl +minMaxSeqAssoc (Finite a) Infinity c = Refl +minMaxSeqAssoc Infinity b c = Refl + +||| Agda `⊔g-unitˡ`. +public export +minMaxSeqUnitL : (a : LossGrade) -> minMaxSeq (Finite 0) a = a +minMaxSeqUnitL (Finite a) = Refl +minMaxSeqUnitL Infinity = Refl + +||| Agda `⊔g-unitʳ`. +public export +minMaxSeqUnitR : (a : LossGrade) -> minMaxSeq a (Finite 0) = a +minMaxSeqUnitR (Finite a) = cong Finite (maximumZeroNLeft a) +minMaxSeqUnitR Infinity = Refl + +-- ============================================================================ +-- The instance, and its layers +-- ============================================================================ + +||| Agda `MinMax : ResourceAlgebra`. Named: the carrier is Loss's. +public export +[minMax] ResourceAlgebra LossGrade where + oplus = lossAlt + otimes = minMaxSeq + zeroG = Infinity + oneG = Finite 0 + altAssoc = lossAltAssoc + altComm = lossAltComm + altIdem = lossAltIdem + altUnitL = \_ => Refl + seqAssoc = minMaxSeqAssoc + seqUnitL = minMaxSeqUnitL + seqUnitR = minMaxSeqUnitR + +||| Agda `MinMax-dioid` (distribˡ). +public export +minMaxDistribL : (a, b, c : LossGrade) -> + minMaxSeq a (lossAlt b c) = lossAlt (minMaxSeq a b) (minMaxSeq a c) +minMaxDistribL (Finite a) (Finite b) (Finite c) = cong Finite (maxDistribLMin a b c) +minMaxDistribL (Finite a) (Finite b) Infinity = Refl +minMaxDistribL (Finite a) Infinity c = Refl +minMaxDistribL Infinity b c = Refl + +||| Agda `MinMax-dioid` (distribʳ). +public export +minMaxDistribR : (a, b, c : LossGrade) -> + minMaxSeq (lossAlt a b) c = lossAlt (minMaxSeq a c) (minMaxSeq b c) +minMaxDistribR (Finite a) (Finite b) (Finite c) = cong Finite (maxDistribRMin a b c) +minMaxDistribR (Finite a) (Finite b) Infinity = Refl +minMaxDistribR (Finite a) Infinity (Finite c) = Refl +minMaxDistribR (Finite a) Infinity Infinity = Refl +minMaxDistribR Infinity b c = Refl + +||| Agda `MinMax-dioid`. +public export +[minMaxDioid] IsDioid LossGrade using minMax where + distribL = minMaxDistribL + distribR = minMaxDistribR + +||| Agda `MinMax-ordered = IsDioid.ordered MinMax-dioid`. +public export +[minMaxOrdered] IsOrdered LossGrade using minMax where + otimesMonoL = dioidMonoL @{minMaxDioid} + otimesMonoR = dioidMonoR @{minMaxDioid} + +||| Agda `MinMax-annihilating` (annihilʳ). +public export +minMaxAnnihilR : (a : LossGrade) -> minMaxSeq a Infinity = Infinity +minMaxAnnihilR (Finite _) = Refl +minMaxAnnihilR Infinity = Refl + +||| Agda `MinMax-annihilating`. +public export +[minMaxAnnihilating] IsAnnihilating LossGrade using minMax where + annihilL = \_ => Refl + annihilR = minMaxAnnihilR diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr index b1d64ec..17c3a00 100644 --- a/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr @@ -4,7 +4,9 @@ -- ResourceAlgebra/Nat.idr — the ℕ lemmas the grade kernel's instances need. -- -- Transcribed from hyperpolymath/resource-algebra --- src/ResourceAlgebra/Prelude.agda @ cf9235c532712a783a404c359a1055f40134794a +-- src/ResourceAlgebra/Prelude.agda @ 0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe +-- (the max-over-min lemmas at the end came upstream with Instances/MinMax; +-- everything else is unchanged since cf9235c) -- Correspondence status: ASSUMED (transcription). -- -- The Agda development is builtins-only, so it defines its own `max`, `min` @@ -197,3 +199,31 @@ maxLub : {a, b, c : Nat} -> LTE a c -> LTE b c -> LTE (maximum a b) c maxLub LTEZero q = q maxLub (LTESucc p) LTEZero = LTESucc p maxLub (LTESucc p) (LTESucc q) = LTESucc (maxLub p q) + +-- ============================================================================ +-- max over min — Prelude.agda (added upstream with Instances/MinMax) +-- ============================================================================ + +||| Agda `min-≤`: min m n is m once m ≤ n. +public export +minOfLTE : {m, n : Nat} -> LTE m n -> minimum m n = m +minOfLTE {m} {n} le = trans (minimumCommutative m n) (minimumOfLTE le) + +||| Agda `max-distribˡ-min`: max distributes over min, so the min-max +||| instance is a dioid. +public export +maxDistribLMin : (a, b, c : Nat) -> + maximum a (minimum b c) = minimum (maximum a b) (maximum a c) +maxDistribLMin Z b c = Refl +maxDistribLMin (S a) Z c = sym (minOfLTE (maximumLeftUpperBound (S a) c)) +maxDistribLMin (S a) (S b) Z = cong S (sym (minimumOfLTE (maximumLeftUpperBound a b))) +maxDistribLMin (S a) (S b) (S c) = cong S (maxDistribLMin a b c) + +||| Agda `max-distribʳ-min`. +public export +maxDistribRMin : (a, b, c : Nat) -> + maximum (minimum a b) c = minimum (maximum a c) (maximum b c) +maxDistribRMin a b c = + trans (maximumCommutative (minimum a b) c) + (trans (maxDistribLMin c a b) + (cong2 minimum (maximumCommutative c a) (maximumCommutative c b))) diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/Separation.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/Separation.idr index 875f9fd..fd6029d 100644 --- a/src/abi/TypedWasm/ABI/ResourceAlgebra/Separation.idr +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/Separation.idr @@ -9,9 +9,12 @@ -- 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 +-- S-4 a bottleneck is not a sum: MinMax and Loss share carrier and +-- alternatives and differ only in sequence -- -- Transcribed from hyperpolymath/resource-algebra --- src/ResourceAlgebra/Separation.agda @ cf9235c532712a783a404c359a1055f40134794a +-- src/ResourceAlgebra/Separation.agda @ 0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe +-- (S-1..S-3 unchanged since cf9235c; S-4 added with Instances/MinMax) -- Correspondence status: ASSUMED (transcription). -- -- These are the reason typed-wasm does not fold its grades into one: L11's @@ -27,6 +30,7 @@ import TypedWasm.ABI.ResourceAlgebra import TypedWasm.ABI.ResourceAlgebra.Loss import TypedWasm.ABI.ResourceAlgebra.MaxPlus import TypedWasm.ABI.ResourceAlgebra.HWM +import TypedWasm.ABI.ResourceAlgebra.MinMax %default total @@ -96,3 +100,26 @@ maxPlusOrder = Refl public export lossOrderReversed : LeG (Finite 2) (Finite 1) lossOrderReversed = Refl + +-- ============================================================================ +-- S-4 A bottleneck is not a sum. MinMax and Loss share the carrier and the +-- alternatives (both min); sequencing 2 and 3 gives the worst hop, 3, +-- in MinMax and the total, 5, in Loss. A bottleneck bound is not a +-- loss bound, though it is below one (upstream Morphism.agda, +-- `loss-bottleneck`). +-- ============================================================================ + +||| Agda `loss-seq`. +public export +lossSeqSums : lossSeq (Finite 2) (Finite 3) = Finite 5 +lossSeqSums = Refl + +||| Agda `minmax-seq`. +public export +minMaxSeqWorstHop : minMaxSeq (Finite 2) (Finite 3) = Finite 3 +minMaxSeqWorstHop = Refl + +||| Agda `bottleneck-is-not-sum`. +public export +bottleneckIsNotSum : Not (minMaxSeq (Finite 2) (Finite 3) = lossSeq (Finite 2) (Finite 3)) +bottleneckIsNotSum p = threeNotFive (finiteInjective p) diff --git a/src/abi/TypedWasm/ABI/Tropical.idr b/src/abi/TypedWasm/ABI/Tropical.idr index bdb4062..058f80f 100644 --- a/src/abi/TypedWasm/ABI/Tropical.idr +++ b/src/abi/TypedWasm/ABI/Tropical.idr @@ -32,11 +32,11 @@ -- provenance, not parallel definitions. -- -- 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). +-- * parametric_resource_transport — needs resource-algebra homomorphisms. +-- Upstream has them since 0b338c9 (Morphism.agda: strict and lax); they +-- are not ported here. +-- The bottleneck layer (tropMax below) is the kernel's MinMax sequence +-- (ResourceAlgebra/MinMax.idr), so no grade operation is defined here. -- typed-wasm holds one thing the kernel lacks: the Kleene-closure matrix -- layer below (extend-upstream candidate; owner sign-off required). -- ---------------------------------------------------------------------------- @@ -48,6 +48,7 @@ import TypedWasm.ABI.Levels import public TypedWasm.ABI.ResourceAlgebra import public TypedWasm.ABI.ResourceAlgebra.Loss import public TypedWasm.ABI.ResourceAlgebra.MaxPlus +import public TypedWasm.ABI.ResourceAlgebra.MinMax import Data.Nat import Data.Fin import Data.List @@ -421,10 +422,10 @@ tropMulMonoL c ab = otimesMonoR c ab -- -- 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. +-- the SEQUENCE operation, +∞ absorbs, and alternatives stay min. It is the +-- kernel's MinMax instance (ResourceAlgebra/MinMax.idr, transcribed from +-- resource-algebra Instances/MinMax.agda); `tropMax` is its sequence, not a +-- copy of it. ||| min (max m n) m = m : a lower bottleneck absorbs against the route max. private @@ -434,12 +435,10 @@ 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 -||| absorbs. Mirrors canonical MinMax.mul (= max). +||| absorbs. The kernel's MinMax sequence (`minMaxSeq`, Agda `_⊔g_`). public export tropMax : TropCost -> TropCost -> TropCost -tropMax Infinity _ = Infinity -tropMax _ Infinity = Infinity -tropMax (Finite a) (Finite b) = Finite (maximum a b) +tropMax = minMaxSeq ||| Bottleneck composition is commutative. public export @@ -595,9 +594,10 @@ bottleneckCeilsEdges p e el = rewrite p.isBottleneck in hubCeiling e el -- sequence; the bound is `worstCase plan ≼ Val bound`, which is ℕ's ≤. -- DESIGNED as an obligation: no surface syntax, checker or attestation -- uses it yet. --- Level11BottleneckProof MinMax. Not a kernel instance and --- NOT MaxPlus (tests/reject/TropicalIsNotMaxPlus.idr; see the header). --- Left as it is. +-- Level11BottleneckProof MinMax (min-max), the kernel instance +-- ResourceAlgebra/MinMax.idr: `tropMax` is its sequence. NOT MaxPlus +-- (tests/reject/TropicalIsNotMaxPlus.idr) and NOT Loss +-- (tests/reject/MinMaxIsLoss.idr). ||| The L11 numeric bound is the kernel's Loss order: `c ≤ n` as a cost is ||| `Finite n ≼ c` as a grade. diff --git a/src/abi/typed-wasm.ipkg b/src/abi/typed-wasm.ipkg index 34e5178..413892f 100644 --- a/src/abi/typed-wasm.ipkg +++ b/src/abi/typed-wasm.ipkg @@ -23,13 +23,14 @@ modules = TypedWasm.ABI.Region , TypedWasm.ABI.KCut , 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. + -- @ 0b338c9; the one definition of min-plus (Loss), of max-plus + -- (MaxPlus) and of min-max (MinMax) 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.MinMax , TypedWasm.ABI.ResourceAlgebra.Separation -- L13 occupancy (PWL-01 step 3): R-1..R-5 ported from occupancy-types @ af95728 , TypedWasm.ABI.Occupancy diff --git a/tests/proof/regression.mjs b/tests/proof/regression.mjs index 6752278..4a82465 100644 --- a/tests/proof/regression.mjs +++ b/tests/proof/regression.mjs @@ -206,8 +206,9 @@ const EXPECTED = [ ["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. + // hyperpolymath/resource-algebra (pin in scripts/fetch-siblings.sh). Pins + // the interface layers, the four 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"], @@ -230,12 +231,18 @@ const EXPECTED = [ ["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/MinMax.idr", /^minMaxSeq\s*:/m, "MinMax sequence (max) — the one min-max"], + ["ResourceAlgebra/MinMax.idr", /^\[minMax\] ResourceAlgebra LossGrade where/m, "MinMax instance, named (carrier shared with Loss)"], + ["ResourceAlgebra/MinMax.idr", /^minMaxDistribL\s*:/m, "MinMax left distributivity"], + ["ResourceAlgebra/MinMax.idr", /^\[minMaxAnnihilating\] IsAnnihilating LossGrade using minMax where/m, "MinMax annihilating layer"], ["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"], + ["ResourceAlgebra/Separation.idr", /^bottleneckIsNotSum\s*:/m, "S-4 a bottleneck is not a sum"], ["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)"], + ["Tropical.idr", /^tropMax = minMaxSeq$/m, "L11 bottleneck = the kernel's MinMax sequence"], ["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)"], diff --git a/tests/reject/MinMaxIsLoss.idr b/tests/reject/MinMaxIsLoss.idr new file mode 100644 index 0000000..7d86b8d --- /dev/null +++ b/tests/reject/MinMaxIsLoss.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/MinMaxIsLoss.agda @ 0b338c9. +-- +-- The bottleneck sequence keeps the worst hop; it does not add the hops. +-- Accepting this would let a min-max bound (L11's Level11BottleneckProof) be +-- read as a min-plus (loss) bound, the identification Separation S-4 and +-- upstream's lax (not strict) loss-bottleneck morphism exist to forbid. +-- EXPECT: Can.t solve constraint between: plus m n and maximum m n +module MinMaxIsLoss + +import TypedWasm.ABI.ResourceAlgebra.MinMax + +%default total + +invalid : (m, n : Nat) -> minMaxSeq (Finite m) (Finite n) = Finite (m + n) +invalid m n = Refl diff --git a/tests/reject/README.adoc b/tests/reject/README.adoc index c1c5426..d6b0528 100644 --- a/tests/reject/README.adoc +++ b/tests/reject/README.adoc @@ -15,6 +15,7 @@ because then the control proves nothing. | `LossWorstCase` | echo's alternatives read as max, i.e. loss treated as cost (S-2) | `DriftExceedsPeak` | a run ending with more live state than its peak | `TropicalIsNotMaxPlus` | L11's `TropCost` read as max-plus (it is min-plus) +| `MinMaxIsLoss` | L11's bottleneck (the MinMax sequence) read as a sum, i.e. a min-max bound taken for a loss bound (S-4) | `CostIsOccupancy` | an L13 run charged the sum of its peaks, as if the boundary reclaimed nothing (occupancy-types R-6) | `DriftIsPeak` | drift identified with peak: "a boundary never reclaims" (occupancy-types R-6) | `WorstCaseIsCheapest` | L11's MaxPlus worst case charging the cheaper branch @@ -23,7 +24,7 @@ because then the control proves nothing. | `InconsistentCut` | K-CUT-LOSS without the Consistent side-condition (choreographic-types K-7) |=== -`HWMAnnihilates`, `LossWorstCase` and `DriftExceedsPeak` mirror resource-algebra +`HWMAnnihilates`, `LossWorstCase`, `DriftExceedsPeak` and `MinMaxIsLoss` mirror resource-algebra `tests/reject/*.agda`; `CostIsOccupancy` and `DriftIsPeak` mirror occupancy-types `tests/reject/*.agda`; `UnprojectableChoice` and `InconsistentCut` mirror choreographic-types diff --git a/tests/transcription/Explore.idr b/tests/transcription/Explore.idr index 0b261ef..7a99f07 100644 --- a/tests/transcription/Explore.idr +++ b/tests/transcription/Explore.idr @@ -12,13 +12,16 @@ -- 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}. +-- every operation is reached), HWM {(p, n) | n <= p <= 2}. MinMax shares +-- Loss's carrier and alternatives (`lossAlt`, already tabled), so only its +-- sequence `minMaxSeq` is tabled, on the Loss domain. module Main import Data.List import TypedWasm.ABI.ResourceAlgebra.Loss import TypedWasm.ABI.ResourceAlgebra.MaxPlus import TypedWasm.ABI.ResourceAlgebra.HWM +import TypedWasm.ABI.ResourceAlgebra.MinMax %default total @@ -58,3 +61,4 @@ main = traverse_ putStrLn $ ++ rows "MaxPlus" "seq" showM maxPlusSeq maxDom ++ rows "HWM" "alt" showH hwmAlt hwmDom ++ rows "HWM" "seq" showH hwmSeq hwmDom + ++ rows "MinMax" "seq" showL minMaxSeq lossDom diff --git a/tests/transcription/README.adoc b/tests/transcription/README.adoc index 1c90265..d19e960 100644 --- a/tests/transcription/README.adoc +++ b/tests/transcription/README.adoc @@ -10,7 +10,8 @@ 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. + every clause is reached, and HWM on peak ≤ 2. MinMax shares Loss's carrier + and alternatives, so only its sequence is tabled, on the Loss domain. . *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. diff --git a/tests/transcription/gen.sh b/tests/transcription/gen.sh index 4949140..4c911d0 100755 --- a/tests/transcription/gen.sh +++ b/tests/transcription/gen.sh @@ -5,7 +5,8 @@ # 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) +# Agda instances (Loss / MaxPlus / HWM / MinMax at the +# pin in scripts/fetch-siblings.sh) # OUTDIR/MODULE.idr every row as `Refl` against the Idris2 port # (src/abi/TypedWasm/ABI/ResourceAlgebra/*) # @@ -16,6 +17,8 @@ # ops alt (_⊕h_ / hwmAlt), seq (_⊗h_ / hwmSeq); # a result is compared by peak and drift # (the bound proof is irrelevant). +# MinMax values "fin N" | "inf" op seq (_⊔g_ / minMaxSeq); its alternatives +# are Loss's own (_⊓g_ / lossAlt). # 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; } @@ -27,13 +30,13 @@ function lte_agda(n, s, i) { s = "z≤n"; for (i = 0; i < n; i++) s = "(s≤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 == "Loss" || inst == "MinMax") 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 == "Loss" || inst == "MinMax") 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]) ")" } @@ -41,11 +44,13 @@ 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_" + if (inst == "MinMax") return (op == "alt") ? "L._⊓g_" : "MM._⊔g_" } 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" + if (inst == "MinMax") return (op == "alt") ? "lossAlt" : "minMaxSeq" } BEGIN { print "{-# OPTIONS --safe --without-K #-}" > agda @@ -55,6 +60,7 @@ BEGIN { 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 "import ResourceAlgebra.Instances.MinMax as MM" > agda print "open L using (fin; inf)" > agda print "open M using (val; bot)" > agda print "open H using (hwm)" > agda @@ -65,6 +71,7 @@ BEGIN { print "import TypedWasm.ABI.ResourceAlgebra.Loss" > idr print "import TypedWasm.ABI.ResourceAlgebra.MaxPlus" > idr print "import TypedWasm.ABI.ResourceAlgebra.HWM" > idr + print "import TypedWasm.ABI.ResourceAlgebra.MinMax" > idr print "" > idr print "%default total" > idr print "" > idr diff --git a/tests/transcription/ops.tsv b/tests/transcription/ops.tsv index f1f899a..1d84076 100644 --- a/tests/transcription/ops.tsv +++ b/tests/transcription/ops.tsv @@ -1,7 +1,7 @@ # 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. +# resource-algebra @ 0b338c9 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 @@ -174,3 +174,28 @@ 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 +MinMax seq fin 0 fin 0 fin 0 +MinMax seq fin 0 fin 1 fin 1 +MinMax seq fin 0 fin 2 fin 2 +MinMax seq fin 0 fin 3 fin 3 +MinMax seq fin 0 inf inf +MinMax seq fin 1 fin 0 fin 1 +MinMax seq fin 1 fin 1 fin 1 +MinMax seq fin 1 fin 2 fin 2 +MinMax seq fin 1 fin 3 fin 3 +MinMax seq fin 1 inf inf +MinMax seq fin 2 fin 0 fin 2 +MinMax seq fin 2 fin 1 fin 2 +MinMax seq fin 2 fin 2 fin 2 +MinMax seq fin 2 fin 3 fin 3 +MinMax seq fin 2 inf inf +MinMax seq fin 3 fin 0 fin 3 +MinMax seq fin 3 fin 1 fin 3 +MinMax seq fin 3 fin 2 fin 3 +MinMax seq fin 3 fin 3 fin 3 +MinMax seq fin 3 inf inf +MinMax seq inf fin 0 inf +MinMax seq inf fin 1 inf +MinMax seq inf fin 2 inf +MinMax seq inf fin 3 inf +MinMax seq inf inf inf diff --git a/tests/transcription/wrong-rows.tsv b/tests/transcription/wrong-rows.tsv index eef6f08..1492d41 100644 --- a/tests/transcription/wrong-rows.tsv +++ b/tests/transcription/wrong-rows.tsv @@ -5,6 +5,8 @@ # 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 +# MinMax seq read as a sum, the S-4 confusion: the worst hop of 2, 3 is 3 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 +MinMax seq fin 2 fin 3 fin 5 diff --git a/tools/check-grade-kernel.sh b/tools/check-grade-kernel.sh index 9a2b790..4c27646 100755 --- a/tools/check-grade-kernel.sh +++ b/tools/check-grade-kernel.sh @@ -2,7 +2,7 @@ # 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. +# check-grade-kernel.sh — one definition of min-plus, one of max-plus, one of min-max. # # The grade kernel (src/abi/TypedWasm/ABI/ResourceAlgebra.idr and # src/abi/TypedWasm/ABI/ResourceAlgebra/*.idr) is the only place in the tree @@ -140,6 +140,8 @@ 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 ;; + # MinMax's alternatives are Loss's own lossAlt; it defines only its sequence. + */ResourceAlgebra/MinMax.idr) want=1 ;; *) want=0 ;; esac got="$(kernel_count "$kf")" @@ -148,15 +150,16 @@ for kf in $(git ls-files 'src/abi/TypedWasm/ABI/ResourceAlgebra.idr' 'src/abi/Ty kernel_ok=0 fi done -for need in src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr; do +for need in src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr \ + src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.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; } +[ "$kernel_ok" -eq 1 ] || { echo "GRADE-KERNEL GATE FAILED: the kernel does not hold exactly one min-plus, one max-plus and one min-max."; 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" + echo "OK: one definition of min-plus (ResourceAlgebra/Loss.idr), one of max-plus (ResourceAlgebra/MaxPlus.idr) and one of min-max (ResourceAlgebra/MinMax.idr); no grade operation outside the kernel, 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 diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh index 41dc633..8f5757e 100755 --- a/tools/check-kernel-proofs.sh +++ b/tools/check-kernel-proofs.sh @@ -59,7 +59,8 @@ else cat "$OUT/upstream.log"; err "upstream resource-algebra check failed at the pin" fi # occupancy-types (L13's reclamation law), checked against OUR resource-algebra -# pin: its own pin (b2c9f1f) differs from cf9235c only by a CI workflow file. +# pin: its own pin (b2c9f1f) predates Instances/MinMax and Morphism; this pin only +# adds modules and lemmas, so the check below is what shows nothing it uses moved. OCC="_build/dependencies/occupancy-types" [ -d "$OCC/src/OccupancyTypes" ] || die "occupancy-types not fetched — run scripts/fetch-siblings.sh" echo "occupancy-types at $(git -C "$OCC" rev-parse HEAD)" diff --git a/tools/grade-kernel.allow b/tools/grade-kernel.allow index da9e54b..de1aa23 100644 --- a/tools/grade-kernel.allow +++ b/tools/grade-kernel.allow @@ -2,4 +2,3 @@ # 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 8ef6b4ff1dfe46a41cdf59ab73c4a2dc985f733b Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 14 Oct 2026 12:19:06 +0100 Subject: [PATCH 2/3] Update src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr index e1fe363..d3c9b8e 100644 --- a/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr +++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr @@ -19,7 +19,7 @@ -- -- minMaxSeq = sequence = MAX (the worst hop) — the "⊗", unit Finite 0 -- lossAlt = alternatives = MIN (the better path) — the "⊕", unit Infinity --- Infinity absorbs under both: an unreachable hop makes the path unreachable, +-- Infinity absorbs under sequence but is the identity for alternatives: -- and an unreachable alternative is never chosen. -- -- The carrier is shared with Loss ON PURPOSE (upstream Morphism.agda, From 9bf1786dd869b8a56b1f884356a3b3da1cfb1d42 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 14 Oct 2026 12:19:23 +0100 Subject: [PATCH 3/3] Update scripts/fetch-siblings.sh Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- scripts/fetch-siblings.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh index 8040cb1..7c72800 100755 --- a/scripts/fetch-siblings.sh +++ b/scripts/fetch-siblings.sh @@ -22,7 +22,7 @@ set -euo pipefail cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe}" -OCCUPANCY_TYPES_COMMIT="${OCCUPANCY_TYPES_COMMIT:-af957280075699c659de0abd9a3b0defade77309}" +OCCUPANCY_TYPES_COMMIT="${OCCUPANCY_TYPES_COMMIT:-60134839efe2c6f51a31d977a72c1cf94457e71d}" CHOREOGRAPHIC_TYPES_COMMIT="${CHOREOGRAPHIC_TYPES_COMMIT:-edb784a7d26c276c2abfa8399b773d346dbb101e}" fetch() { # fetch