Repository navigation
feat(abi): resource-algebra as the grade kernel — one min-plus, one max-plus (PWL-01, PR A) - #271
Merged
hyperpolymath merged 4 commits intoOct 14, 2026
Conversation
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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
…ELOG 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
Contributor
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 56 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
|
hyperpolymath
marked this pull request as ready for review
October 14, 2026 01:04
hyperpolymath
added this pull request to stack #272
October 14, 2026 01:05
hyperpolymath
pushed a commit
that referenced
this pull request
Oct 14, 2026
…uash merges) #270 and #271 were squash-merged into main, so their commits on this branch are not ancestors of main. Merging main back in (rather than force-pushing a rebased branch) keeps the branch's published history; the trees agree except for the SPDX header commit, which is not yet on main. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
11 of 12 tasks
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
…-2 at a boundary (PWL-01, PR B) (#273) ## Summary PWL-01 steps 2–3, on top of the kernel from #271 (merged). L11 and L12 obligations are restated against the grade kernel, and L13 gets the occupancy reading: occupancy-types' reclamation law (R-2), ported and re-proved, then bound to `private_memory` and `boundary`. **No row moves to achieved**; L11/L12 stay draft. One correction carried from PR A: the issue asks for "`Level11BottleneckProof` as MaxPlus", but the bottleneck is MinMax, not MaxPlus. Restating it as MaxPlus would change its meaning at an unreachable (+∞) edge. So the bottleneck stays as it is, and MaxPlus goes where max-plus is the right algebra: a worst case over branches. Pins: resource-algebra `cf9235c`, occupancy-types `af957280075699c659de0abd9a3b0defade77309` (both in `scripts/fetch-siblings.sh`). ## Changes - **L11** (`Tropical.idr`): - `CostBounded c n` is proved to *be* the Loss order `Finite n ≼ c` (`costBoundedIsLossOrder` / `lossOrderIsCostBounded`). - Path bounds compose by the kernel's `otimesMono` (`costBoundedSeq`). - New `Level11WorstCaseProof` grades a branching `AccessPlan` in MaxPlus, with `worstCaseThen` / `worstCaseOneOf` from `otimesMono` / `oplusMono` and `worstCaseFinite` / `worstCaseWithin`. The obligation is **DESIGNED**: no surface syntax or attestation uses it. - **L12** (`Epistemic.idr`, additive): `stalenessGrade` is the reader's lag as a Loss grade. - Fresh = 𝟙 (`freshHasNoStaleness`), stale ≠ 𝟙 (`staleHasStaleness`), never synced = 𝟘 (`neverSyncedIsCollapse`). - 𝟙 is the top (`freshIsTop`), and relayed lag = ⊗ (`stalenessRelay`). - `syncGrade` gets a note: it holds a version, not a loss. - **L13** (new `Occupancy.idr`): occupancy-types R-1..R-5 ported and re-proved over the kernel's HWM (`cutFactor`, `reclaimLaw`, `occupancyAtCut`, `occupancyLeCost`, `noReclaim`, `reclaimed`, `witness*`). - Binding, **DESIGNED**: `OccupancyGradedMemory` (an HWM grade per private memory, within its declared maximum) and `BoundaryCut` / `boundaryFrees` = peak − drift / `boundaryOccupancy` / `fitsAcrossBoundary` (the budget rule across a boundary). - `striated` occupancy stays OPEN: it's a surface-only construct. - **Kernel additions**, typed-wasm's own and labelled (no operation changes, so the transcription table is unchanged): each instance's order read in ℕ (`lossLeOfLTE`, `maxPlusLeOfLTE` + inverses); `maxLub` and min/max-vs-`LTE` lemmas in `ResourceAlgebra/Nat.idr`. - **Rejects**: `CostIsOccupancy`, `DriftIsPeak` (occupancy-types R-6), `WorstCaseIsCheapest`. `tools/check-kernel-proofs.sh` also runs occupancy-types' own Agda check at its pin, against our resource-algebra pin. - `LEVEL-STATUS` rows 11–13 name the kernel artefacts; new inventory row; `CHANGELOG`; 18 names pinned in `regression.mjs`. - **CI repair, own commit** (`e080ef6`): `Cargo.lock` listed `wasmparser` twice. Three concurrent Dependabot bumps (#231–#233) caused it, and it was invisible while E2E was `startup_failure`. Once #270 landed, **E2E Validation / cargo-verify went red on `main`** with `package wasmparser is specified twice in the lockfile`. The lock was rewritten by cargo itself: one edge 0.255.0 → 0.256.0, the stale and duplicate entries removed, nothing upgraded. `cargo build --workspace --locked` and `cargo test --workspace --locked` pass. Branch note: this is the designated branch after #271's squash merge. `main` was merged back in (`bb2380b`) instead of force-pushing; the tree equals a clean rebase on `main`. ## Status rows (artefact for each) | Row | Claim | Status | Artefact | |---|---|---|---| | 11 | bound = Loss order; bounds compose | PROVEN | `costBoundedIsLossOrder`, `costBoundedSeq` | | 11 | worst-case obligation (MaxPlus) | PROVEN lemmas, obligation DESIGNED | `Level11WorstCaseProof`, `worstCaseThen/OneOf`; `tests/reject/WorstCaseIsCheapest.idr` | | 12 | staleness as Loss | PROVEN | `freshHasNoStaleness`, `staleHasStaleness`, `stalenessRelay` | | 13 | R-1..R-5 (occupancy-types `Reclaim`/`Timeline`/`Witness`) | PROVEN in Idris2; correspondence ASSUMED (port-and-reprove) | `Occupancy.idr`; upstream check at `af95728` in the gate | | 13 | R-6 | TESTED | `tests/reject/{CostIsOccupancy,DriftIsPeak}.idr` | | 13 | binding to `private_memory` / `boundary` | DESIGNED | `OccupancyGradedMemory`, `BoundaryCut` | | 13 | `striated` occupancy | OPEN | none | ## RSR Quality Checklist ### Required - [x] Tests pass (see Testing) - [x] Code is formatted - [x] Linter is clean (no new warnings) - [x] No banned language patterns - [x] No `unsafe` blocks without `// SAFETY:` comments - [x] No banned functions (gate checks zero `believe_me` / `assert_total` in the kernel) - [x] SPDX license headers present on all new/modified source files (incl. `CHANGELOG.adoc`, which had none) - [x] No secrets, credentials, or `.env` files included ### As Applicable - [ ] `.machine_readable/descriptiles/STATE.a2ml` not updated (stale since 2026-05-27; hand-written figures; owner's call) - [x] Documentation updated - [x] `CHANGELOG` updated - [x] ABI changes validated: `contract.abi.sha256` unchanged (I3 anchors are the wire format only) ## Testing ``` tools/check-contract.sh OK: contract gate — I1 + I3 hold tools/check-grade-kernel.sh OK: one definition of min-plus (ResourceAlgebra/Loss.idr) and one of max-plus (ResourceAlgebra/MaxPlus.idr); no Nat min/max outside base tools/check-kernel-proofs.sh OK: kernel proofs — build, 7 rejection(s), table, and 3 negative control row(s) PASS: upstream: PASS: core proofs and all 3 expected rejections PASS: upstream occupancy-types: PASS: core proofs and all 2 expected rejections PASS: idris2 --build typed-wasm.ipkg: 31 module(s) built, 0 errors node tests/proof/regression.mjs --strict 190 passed, 0 failed, 0 skipped E2E_BUILD=0 bash tests/e2e.sh 47 passed, 0 failed, 7 skipped cargo build/test --workspace --locked ok (all test binaries) ``` 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- _Generated by [Claude Code](https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
This was referenced Oct 14, 2026
Merged
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
## Summary This answers decision 1 from #271 ("MinMax has no kernel instance. Should one be added upstream?"). The owner said add it, and it is now upstream as hyperpolymath/resource-algebra#4, merged at `0b338c9`. This PR transcribes it into the Idris2 grade kernel. `Tropical.tropMax` becomes the kernel's MinMax sequence, which empties the grade-kernel allowlist. **Blocked on hyperpolymath/occupancy-types#11.** The kernel-proofs gate checks occupancy-types against this repo's resource-algebra pin. At `0b338c9`, occupancy-types' `Order.agda` clashes with four lemmas the new Prelude adds (`Multiple definitions of ≤-+ˡ`). occupancy-types#11 fixes it at source. Until it merges, CI's `kernel-proofs` job is expected to fail on that step alone. After the merge I'll move the occupancy-types pin here to the merge commit. ## Changes - **`ResourceAlgebra/MinMax.idr` (new)**, clause-for-clause from `Instances/MinMax.agda`: - `minMaxSeq` (Agda `_⊔g_`) on Loss's carrier, with Loss's alternatives (`lossAlt`). - Monoid, dioid and annihilation laws. - The instance and its layers are **named implementations** (`[minMax]`, `[minMaxDioid]`, `[minMaxOrdered]`, `[minMaxAnnihilating]`). Idris2 resolves an interface by its carrier, and `ResourceAlgebra LossGrade` is already Loss. Upstream shares the carrier on purpose (its lax morphism `loss-bottleneck` is the identity). - **`Tropical.idr`:** `tropMax = minMaxSeq`. Its existing proofs (`tropMaxComm`, `tropMaxUpperL/R`, `hubCeiling`, `Level11BottleneckProof`) go through unchanged. - **Grade-kernel gate:** - `tools/grade-kernel.allow` is now empty. - `check-grade-kernel.sh` expects exactly one min-max definition, in `MinMax.idr`, and requires the file to exist. - Negative control: restoring the old local `tropMax` fails the gate (R2). - **`Nat.idr`:** `minOfLTE`, `maxDistribLMin` and `maxDistribRMin` (upstream `min-≤`, `max-distribˡ-min`, `max-distribʳ-min`). - **`Separation.idr`:** S-4 `bottleneckIsNotSum`. - **New reject `tests/reject/MinMaxIsLoss.idr`**, mirroring upstream's. It is refused with `Can't solve constraint between: plus m n and maximum m n`. - **Transcription table:** - the MinMax sequence is tabled on the Loss domain: 197 rows (was 172) and 269 equalities, accepted by Agda against the pin and by Idris2 against the port; - the alternatives are Loss's own and already tabled; - a fourth wrong row (bottleneck read as a sum) is refused by both. - **resource-algebra pin `cf9235c` → `0b338c9`:** - Core, Loss, MaxPlus and HWM are byte-identical between the two pins. Their headers cite the new pin and say so. - The upstream check now reports `core proofs, unit tests and all 8 expected rejections`. - **Docs and pins:** - `LEVEL-STATUS`: kernel inventory row, Tropical row, Grade kernel section, and a *Resolved 2026-10-14* note; - `CONTRACT`, `ipkg`, `contract-gate.yml` comments, the reject and transcription READMEs, and `CHANGELOG`; - six new names pinned in `regression.mjs`. **No status row moves.** L11 stays draft, and `Level11BottleneckProof`'s laws were already proved; only where its sequence is defined changed. Upstream's strict and lax morphisms (`Morphism.agda`) are **not** ported here. ## RSR Quality Checklist ### Required - [x] Tests pass (see Testing) - [x] Code is formatted - [x] Linter is clean: shellcheck clean on the changed scripts; no new Idris2 build errors - [x] No banned language patterns - [x] No `unsafe` blocks without `// SAFETY:` comments - [x] No banned functions (the gate checks zero `believe_me` / `assert_total` in the kernel) - [x] SPDX license headers present on all new/modified source files - [x] No secrets, credentials, or `.env` files included ### As Applicable - [x] Documentation updated - [x] `CHANGELOG` updated - [x] ABI changes validated: `tools/check-contract.sh` OK; `contract.abi.sha256` unchanged (its anchors are the wire format) ## Testing Run locally with occupancy-types at occupancy-types#11's head (`6013483`): ``` tools/check-kernel-proofs.sh OK: kernel proofs — build, 11 rejection(s), table, and 4 negative control row(s) PASS: upstream: PASS: core proofs, unit tests and all 8 expected rejections PASS: upstream occupancy-types: PASS: core proofs and all 2 expected rejections PASS: idris2 --build typed-wasm.ipkg: 33 module(s) built, 0 errors PASS: rejected MinMaxIsLoss at line 19 (Can.t solve constraint between: plus m n and maximum m n) PASS: explorer: the port reproduces ops.tsv (197 rows) PASS: Agda (pinned resource-algebra) accepts the table by refl: 269 equalities PASS: Idris2 (port) accepts the table by Refl: 269 equalities PASS: control: Agda refuses MinMax seq fin 2 fin 3 fin 5 PASS: control: Idris2 refuses MinMax seq fin 2 fin 3 fin 5 tools/check-grade-kernel.sh 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 tools/check-grade-kernel.sh --self-test 8/8 seeded duplicates caught; 0 false positives tools/check-contract.sh OK: contract gate — I1 + I3 hold node tests/proof/regression.mjs --strict 208 passed, 0 failed, 0 skipped E2E_BUILD=0 bash tests/e2e.sh E2E validation PASSED ``` With occupancy-types at its current pin (`af95728`), only one step fails: `FAIL: upstream occupancy-types check failed at the pin`, caused by the `Multiple definitions of ≤-+ˡ` clash above. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- _Generated by [Claude Code](https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t)_ --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
PWL-01 step 1. This ports hyperpolymath/resource-algebra
Core.agdaand its three instances to Idris2 as the ABI's grade kernel.Tropical.idrandEcho.idrnow draw their grades from it, and a grep gate enforces one definition of min-plus and one of max-plus in the tree.Stacked on #270, the CI unblock. Without it, E2E Validation can't start. Pin: resource-algebra
cf9235c532712a783a404c359a1055f40134794a, fetched byscripts/fetch-siblings.sh.One correction to the issue text.
Tropical.idrwas never max-plus. ItsTropCostis min-plus, the same algebra as Loss. Its bottleneck layer (tropMax) is min-max, which is neither min-plus nor max-plus. So bothTropical.TropCostandEcho.EchoGradebecame the Loss carrier. MaxPlus is in the kernel, but no L11 obligation uses it yet.tests/reject/TropicalIsNotMaxPlus.idris the checked statement.Changes
src/abi/TypedWasm/ABI/ResourceAlgebra.idr: theResourceAlgebrainterface.IsOrdered,IsDioidandIsAnnihilatingare separate interfaces, as in Agda. "Every dioid is ordered" is a proof:dioidMonoL/Rand the named implementationdioidOrdered. A transcription map is in the header.ResourceAlgebra/{Loss,MaxPlus,HWM}.idr: clause-for-clause transcriptions. Constructors are renamedfin/inf→Finite/Infinityandval/bot→Val/Bot; clause order is kept.Separation.idrhas S-1..S-3.Nat.idrholds only the lemmas base lacks: base'sData.Nat.minimum/maximum/LTEare the Agda Prelude'smin/max/≤, so the tree declares no Nat min/max at all.Tropical.idr:TropCost = LossGrade. The 12 axioms and the order layer are derived from the kernel, andtropMin/natMaxare deleted. Every public name is kept, soEpistemic/Proofscompile unchanged.Echo.idr:EchoGrade = LossGrade.tools/check-grade-kernel.shis the grep gate. Its--self-testis the negative control: 8 seeded duplicates are caught, 0 false positives. Run onmain'sTropical.idr, it fails.tools/grade-kernel.allowholds the one exception (tropMax, MinMax) with its reason.tools/check-kernel-proofs.shruns the falsifiers. A missing toolchain fails the gate; it never skips:check-agda.shat the pin;idris2 --build;tests/reject/*.idr, each refused at itsinvalidline with itsEXPECTmessage;tests/transcription/ops.tsv: 172 rows, Agdareflagainst the pinned sources and Idris2Reflagainst the port, withwrong-rows.tsvrefused by both.contract-gate.yml. They go there, not in a new workflow, becauseactions.lockis keyed by path. Idris2 0.8.0 is built from its tag because there are no binaries.LEVEL-STATUSrow 11, the inventory and a new "Grade kernel" section;CONTRACTEnforcement; the spec's L11 sentence;CHANGELOG.regression.mjspins 31 kernel names.Status rows (artefact for each)
ResourceAlgebra*.idr,idris2 --buildtools/check-kernel-proofs.shstep 4ResourceAlgebra/Separation.idrtests/reject/HWMAnnihilates.idrRSR Quality Checklist
Required
main, none newunsafeblocks without// SAFETY:commentsbelieve_me/assert_total(checked by the gate).envfiles includedAs Applicable
.machine_readable/descriptiles/STATE.a2mlnot updated: last updated 2026-05-27, and its completion figures are hand-written; left for the ownerCHANGELOGupdatedcontract.abi.sha256is unchanged: the I3 anchors coversection.rs's wire format, notsrc/abi/(now stated inCONTRACT.adoc). Re-sealing without anabi_versionbump would be wrong.Testing
Mutation check: hand-corrupting one row of
ops.tsvfails the gate three ways (explorer drift, Agda refusal, Idris2 refusal) and exits 1.Decisions for the owner:
🤖 Generated with Claude Code
https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
Generated by Claude Code