diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 6bdfc8a..99dd37e 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -2,14 +2,14 @@ # CODEOWNERS - Define code review assignments # See: https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-code-owners # -# Replace {{OWNER}} with your GitHub username or team +# Repository owner: hyperpolymath # Default owners for everything -* @{{OWNER}} +* @hyperpolymath # Security-sensitive files require explicit review -SECURITY.md @{{OWNER}} -.github/workflows/ @{{OWNER}} -.machine_readable/contractiles/trust/ @{{OWNER}} -*_chora.deed @{{OWNER}} -.machine_readable/ @{{OWNER}} +SECURITY.md @hyperpolymath +.github/workflows/ @hyperpolymath +.machine_readable/contractiles/trust/ @hyperpolymath +*_chora.deed @hyperpolymath +.machine_readable/ @hyperpolymath diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index f0aea84..73a77cc 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -57,6 +57,8 @@ workflows: - 'actions/deploy-pages@v5.0.1' - 'actions/upload-pages-artifact@v5.0.0' - 'haskell-actions/setup@v2.12.0' + '.github/workflows/proofs.yml': + - 'actions/checkout@v7.0.1' '.github/workflows/push-email-notify.yml': - 'hyperpolymath/smtp-notify-action@v0.3.0' '.github/workflows/quality.yml': diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 842b74d..5277e9d 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -20,8 +20,10 @@ jobs: run: | apt-get update apt-get install --no-install-recommends -y ca-certificates git agda-bin=2.6.4.3-1+b2 - - uses: actions/checkout@v6.0.3 + - uses: actions/checkout@v7.0.1 + with: + persist-credentials: false - name: Verify the checked Agda version run: test "$(agda --version)" = 'Agda version 2.6.4.3' - name: Core proofs and expected rejections - run: bash scripts/check.sh + run: bash scripts/check-agda.sh diff --git a/.machine_readable/descriptiles/anchors/README.adoc b/.machine_readable/descriptiles/anchors/README.adoc index 9d2f62f..c943bef 100644 --- a/.machine_readable/descriptiles/anchors/README.adoc +++ b/.machine_readable/descriptiles/anchors/README.adoc @@ -10,7 +10,7 @@ anchor file lives in this directory, and no `.a2ml` file may be created here. - `(anchor)` - Project recalibration, scope intervention, canonical authority -Read a field with `scripts/deed-field.sh rsr-template-repo_chora.deed anchor `. +Read a field with `scripts/deed-field.sh resource-algebra_chora.deed anchor `. ## Multiple Versions diff --git a/.machine_readable/root-allow.txt b/.machine_readable/root-allow.txt index 3bb68f2..e98fc5f 100644 --- a/.machine_readable/root-allow.txt +++ b/.machine_readable/root-allow.txt @@ -32,12 +32,13 @@ LICENSE LICENSES/ # REUSE licence texts, dual-licence model (code MPL-2.0 / docs CC-BY-SA-4.0) CHANGELOG.adoc # AsciiDoc is the estate-standard documentation format CITATION.cff # citation metadata; GitHub reads it from the root of the default branch only -rsr-template-repo_chora.deed # the repo deed: universal AI entry point; family-7 allocation manifest + ply tree folded in (standards#837 pilot). Filename carries the repo slug (deed dispatch _chora.deed), so repo-init renames it at mint +resource-algebra_chora.deed # repository deed; Canon lockstep reads _chora.deed at the PR head CLAUDE.md # generated arrival pack; the generator, pre-commit and Claude Code all read it from the ROOT (do not hand-edit; edit the repo deed) ?GEMINI.md # pointer to CLAUDE.md for repos without AGENTS.md yet Justfile # thin; delegates phases to build/just/*.just launcher.sh # --setup/--doctor/--heal/--ai-setup (launcher-standard 0.6.0); the one file a newcomer runs first coordination.k9.ncl # repo-local session binding (template-mandated) +resource-algebra.agda-lib # Agda library manifest; Agda discovers it at the library root and resolves src/ relative to it # ─── Conventional dotfiles (tool-required at root) ─────────────────────────── .editorconfig diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 7772d90..64f181c 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -1,6 +1,29 @@ == Changelog +== 2026-10-14 — MinMax and morphisms (resource-algebra#3) + +* `Instances/MinMax.agda`: the min-max (bottleneck) instance on the Loss + carrier, with dioid, ordered and annihilating layers. +* `Morphism.agda`: strict (`Hom`) and lax (`LaxHom`) morphisms with + identities and composition; `peak-lax` (HWM → MaxPlus); no strict + morphism out of HWM; exactly two strict morphisms Loss → MaxPlus and + exactly one MaxPlus → Loss; `loss-bottleneck` (Loss → MinMax, lax). +* `Separation.agda`: S-4 (a bottleneck is not a sum). +* Five more expected rejections: `MinMaxIsLoss`, `PeakIsStrict`, + `BottleneckBoundReversed`, `MinMaxInfinityIsIdentity`, `PeakPreservesZero`; + unit tests in `tests/unit/`. +* `scripts/check-agda.sh` now requires each rejection to carry the message + its `-- EXPECT:` line names (a refusal for another reason fails), and + typechecks the unit tests. +* The proof ledger moved to `docs/status/PROOF-STATUS.adoc`, the template's + home for it, replacing the unfilled template stub there (`just` read the + stub first). The root allowlist keeps only `resource-algebra.agda-lib`. +* Fixed: `proofs.yml` called a non-existent `scripts/check.sh`, so CI had + never checked the proofs; it now runs `scripts/check-agda.sh`. The + workflow had no `actions.lock` key and an unlocked checkout ref (Lock Sync + Gate); it now uses the locked `actions/checkout@v7.0.1`. + == 2026-10-12 — initial development * `ResourceAlgebra` record with `IsOrdered`, `IsDioid` (⇒ ordered) and diff --git a/CITATION.cff b/CITATION.cff index 1ec9ea5..0871c55 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -1,4 +1,5 @@ cff-version: 1.2.0 +message: "If you use this software, please cite it using the metadata in this file." title: "resource-algebra: the parametric grade algebra of the hyperpolymath type family" type: software authors: diff --git a/CLAUDE.md b/CLAUDE.md index 39dde1b..63bf9ad 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -6,7 +6,7 @@ SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell - + # You are in the hyperpolymath estate — orient before acting @@ -38,7 +38,7 @@ The descriptive family (working name *descriptiles*) describes what-is; the **co | File | Answers | |---|---| -| `rsr-template-repo_chora.deed` | **CHORA**, the repo deed. Its `(identity)` `(clade)` `(lineage)` clauses say what this repo IS (registers into `gv-clade-index`); `(meta)` the architecture axes; `(agentic)` *may I act now?*; `(ecosystem)` where it sits and what it is not; `(status)` and `(maturity)` where it is now. Read fields with `scripts/deed-field.sh`. | +| `resource-algebra_chora.deed` | **CHORA**, the repo deed. Its `(identity)` `(clade)` `(lineage)` clauses say what this repo IS (registers into `gv-clade-index`); `(meta)` the architecture axes; `(agentic)` *may I act now?*; `(ecosystem)` where it sits and what it is not; `(status)` and `(maturity)` where it is now. Read fields with `scripts/deed-field.sh`. | | `(anchor)` | *Semantic authority + golden path* — what downstream may extend-not-redefine; if a recognised-drift / re-anchor marker is present, it **supersedes** accumulated context — read it first. | | `(neurosym)` | *Meaning* of operations — proof obligations. | | `(playbook)` | *How* permitted actions run. | @@ -57,17 +57,17 @@ Use plain JavaScript when this tooling is needed. TypeScript and ReScript migrat --- -# This repo: `rsr-template-repo` · clade `rm-rsr-template-repo` +# This repo: `resource-algebra` · clade `UNASSIGNED-resource-algebra` -- **Identity** — uuid `a5ea1382-a34c-5334-8a46-a2ebe904c810`; clade `rm` (secondary ``); born 2026-03-16; forge `hyperpolymath/rsr-template-repo`. -- **IS** — Canonical RSR-compliant repository template: scaffolding (CI/CD, AI manifests, ABI/FFI standards, container ecosystem, governance) that new hyperpolymath projects are instantiated from. -- **IS-NOT** — a project in its own right · Scaffoldia (the full-featured repo designer) · standards (the canon source this template operationalises) -- **Where it sits** — pipeline position **foundation**; chain `standards → rsr-template-repo → (every estate repo)`; coordination = `standards`. +- **Identity** — uuid `241f1c29-0838-5033-b654-7f4c5e279ebc`; clade `UNASSIGNED` (secondary ``); born 2026-10-12; forge `hyperpolymath/resource-algebra`. +- **IS** — Parametric resource algebra in Agda, with Loss, MaxPlus, HWM and MinMax instances and strict/lax morphisms. +- **IS-NOT** — a repository template · the K-CUT statement, which belongs in choreographic-types · occupancy-types' own algebra, for which HWM is a proposal +- **Where it sits** — pipeline position **kernel**; chain `resource-algebra → hyperpolymath type family`; coordination = ``. - **Constraints here** (AGENTIC) — fail-closed; evidence-per-step; no-silent-skip; rerun-after-fix; release-claim-requires-hard-pass. Never: banned langs (above), secrets, state files in repo root, AGPL. Details: the deed's `(bot-directives (methodology) (coverage) (debt))` clauses. - **Golden path** (ANCHOR) — `just test && just quality` → Core tests pass; Quality gates pass; No unresolved critical security findings. -- **State** — phase active; maturity production. Milestones and next actions: `docs/status/ROADMAP.adoc`. +- **State** — phase active; maturity experimental. Milestones and next actions: `docs/status/ROADMAP.adoc`. - + ## Estate-Wide Format Migration Directives diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc deleted file mode 100644 index 2a50bcd..0000000 --- a/PROOF-STATUS.adoc +++ /dev/null @@ -1,66 +0,0 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -= resource-algebra — Proof Status -:revdate: 2026-10-12 - -Statuses follow the estate taxonomy: PROVEN / TESTED / ASSUMED / DESIGNED / -OPEN. Every PROVEN line names the module that discharges it under -`--safe --without-K --no-libraries --double-check`. - -== Build invariant - -* All modules carry `{-# OPTIONS --safe --without-K #-}`; no postulates, no - holes, no standard library. — PROVEN by `just check` (All.agda). -* Three expected rejections fail at their invalid declaration and for the - intended reason (`min m n != max m n`, `p != zero`, `suc _ != zero`). — - TESTED by `scripts/check.sh`. - -== Core (Core.agda) - -[cols="1,3,1",options="header"] -|=== -| ID | Claim | Status -| C-1 | `ResourceAlgebra`: alternatives an idempotent commutative monoid, sequence a monoid | PROVEN (definition + derived `unitʳ`) -| C-2 | The ⊕-induced relation `≼` is a partial order with `𝟘` least and `⊕` its join | PROVEN (`≼-refl`, `≼-trans`, `≼-antisym`, `𝟘-least`, `⊕-upperˡ/ʳ`) -| C-3 | Every dioid is ordered: distributivity ⇒ `⊗` monotone on both sides | PROVEN (`IsDioid.ordered`) -| C-4 | `IsAnnihilating` is independent of `IsDioid` (an instance can be one without the other) | TESTED (HWM is a dioid; `tests/reject/HWMAnnihilates.agda` refuses the zero) -|=== - -== Instances - -[cols="1,3,1",options="header"] -|=== -| ID | Claim | Status -| L-1 | `Loss` is a `ResourceAlgebra`, `IsDioid`, `IsOrdered`, `IsAnnihilating` with ⊕ = min, ⊗ = +, 𝟘 = inf, 𝟙 = fin 0 | PROVEN (Instances/Loss.agda) -| L-2 | `Loss` is textually the echo-types definition (`experimental/echo-additive/Grade.agda`: `_⊓g_`, `_+g_`) | ASSUMED — transcription reviewed by eye; direction of future import (echo → here or here → echo) OPEN -| M-1 | `MaxPlus` is a `ResourceAlgebra`, `IsDioid`, `IsOrdered`, `IsAnnihilating` with ⊕ = max, ⊗ = +, 𝟘 = bot, 𝟙 = val 0 | PROVEN (Instances/MaxPlus.agda) -| M-2 | `MaxPlus` agrees with tropical-types `instance : CommSemiring Tropical` (Lean 4) | OPEN — cross-prover; port-and-reprove, named bridge obligation, no mechanical link exists or is claimed -| H-1 | `HWM` (peak, drift, drift ≤ peak) is a `ResourceAlgebra`, `IsDioid`, `IsOrdered`; 𝟘 ≡ 𝟙 | PROVEN against the definition in Instances/HWM.agda -| H-2 | `HWM` is occupancy-types' occupancy algebra | DESIGNED — occupancy defines none yet (its v0 counts live bytes; the algebra is R2–R3); signed drift (consuming terms) not modelled -| H-3 | `HWM` has no annihilating zero | TESTED (`tests/reject/HWMAnnihilates.agda`) -|=== - -== Separation (Separation.agda) - -[cols="1,3,1",options="header"] -|=== -| ID | Claim | Status -| S-1 | Sequencing peaks 2 and 3 gives 3 under HWM and 5 under MaxPlus: an occupancy bound is not a cost bound | TESTED (computed; `occupancy-is-not-cost`) -| S-2 | On the same numbers, Loss alternatives give `fin 2` and MaxPlus alternatives give `val 3`: echo's join is min, tropical's is max | TESTED (computed; `alternatives-differ`) -| S-3 | `val 1 ≼ val 2` in MaxPlus and `fin 2 ≼ fin 1` in Loss: the induced order runs the opposite way | TESTED (computed) -|=== - -== Open (honest — NOT proved) - -* K-CUT-LOSS itself. It is not stated here; this repository supplies the - algebra it will be parametric in. Expectation (DESIGNED): only the core - record is needed for the equality; `IsOrdered` is needed for the - K-CUT-WARRANT bound. -* L-2 import direction; M-2 Lean bridge; H-2 supersession by occupancy. -* Homomorphisms between instances are not defined. The separation - witnesses show no grade-preserving identification of the three exists on - the embedded naturals; a general non-existence theorem is not claimed. - -== Discipline - -Prose, citation and artefact must agree before any status moves. A status -moves only with a named module or a named log line. diff --git a/README.adoc b/README.adoc index 6eb94c1..4327202 100644 --- a/README.adoc +++ b/README.adoc @@ -4,10 +4,6 @@ = resource-algebra — the parametric grade algebra shared by the type family :toc: left -// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -= Resource Algebra — the parametric grade algebra shared by the type family -:toc: left - == Overview One Agda record, `ResourceAlgebra`, states what a grade algebra is for the @@ -17,7 +13,7 @@ monoid `(⊕, 𝟘)`, sequence forms a monoid `(⊗, 𝟙)`. Optional layers add (`IsDioid`, which yields `IsOrdered` by a proof, not a second obligation), and an annihilating zero (`IsAnnihilating`). -Three instances are checked against it: +Four instances are checked against it: [cols="1,2,2,1",options="header"] |=== @@ -25,6 +21,7 @@ Three instances are checked against it: | `Instances.Loss` | echo-types `experimental/echo-additive/Grade.agda`, transcribed | min / + on ℕ ∪ {∞} | transcribed, PROVEN | `Instances.MaxPlus` | tropical-types `TropicalSessionTypes.lean`, transcribed | max / + on ℕ ∪ {−∞} | transcribed, PROVEN; Lean bridge OPEN | `Instances.HWM` | occupancy-types operational model, *proposed* (its R2–R3 algebra is not yet defined) | componentwise max / peak-and-drift | DESIGNED, PROVEN against this definition +| `Instances.MinMax` | typed-wasm L11 bottleneck (`Tropical.tropMax`), which defined it locally | min / max on ℕ ∪ {∞} | PROVEN; typed-wasm adoption DESIGNED |=== This repository is a kernel module of the family, not a family of its own. @@ -32,6 +29,13 @@ It exists so that K-CUT-LOSS (choreographic-types) can be stated once, parametrically, and discharged three times, instead of being proved against a single concrete algebra that bakes in one repo's vocabulary. +`Morphism.agda` defines strict (`Hom`) and lax (`LaxHom`) maps between +instances and says which exist: `peak` is lax HWM → MaxPlus and nothing +strict leaves HWM; Loss → MaxPlus has exactly two strict maps and +MaxPlus → Loss exactly one, and none of them separates two positive +grades; the identity is lax Loss → MinMax. Transport of K-CUT-LOSS along these maps is +not proved here (link:docs/status/PROOF-STATUS.adoc[], Open). + == What is standard and what is ours *Standard:* idempotent semirings (dioids), the max-plus and min-plus @@ -41,16 +45,16 @@ multiplication for the natural order. *Ours:* the layering (what K-CUT-LOSS needs versus what K-CUT-WARRANT needs), the three estate instances held against one record, the high-water-mark proposal, and the checked separation witnesses -(`Separation.agda`) that turn three boundary sentences of the family map into +(`Separation.agda`) that turn four boundary sentences into `refl`-plus-inequality facts: an occupancy bound is not a cost bound; echo alternatives are min while tropical alternatives are max; the induced order -runs opposite ways in the two. +runs opposite ways in the two; a bottleneck bound is not a loss bound. == What this is not * Not an import of echo-types or tropical-types. The instances are transcriptions; the correspondence is a review obligation recorded in - link:PROOF-STATUS.adoc[]. + link:docs/status/PROOF-STATUS.adoc[]. * Not the K-CUT statement. Global/local types, projection and cuts live in choreographic-types; this repository supplies the algebra they are parametric in. @@ -61,29 +65,33 @@ runs opposite ways in the two. [source,bash] ---- -just check # core proofs under --safe --without-K --double-check, - # then every tests/reject/*.agda must be refused at its - # invalid declaration +just check-agda # core proofs and unit tests under --safe --without-K + # --double-check, then every tests/reject/*.agda must be + # refused at its invalid declaration with the message + # its `-- EXPECT:` line names ---- -Builtins only (`--no-libraries`): the development checks under the Debian -`agda-bin` package the estate CI pins and under Ubuntu's 2.6.3. +Builtins only (`--no-libraries`). It checks locally under Agda 2.6.3. CI +(`proofs.yml`) pins the Debian `agda-bin` 2.6.4.3 package; until 2026-10-14 +that workflow called a script that does not exist, so a CI check is evidence +only from its first green run. == Repository layout ---- src/ResourceAlgebra/Prelude.agda ℕ lemmas (+, max, min, ≤), proved here src/ResourceAlgebra/Core.agda the record and its layers -src/ResourceAlgebra/Instances/*.agda Loss, MaxPlus, HWM +src/ResourceAlgebra/Instances/*.agda Loss, MaxPlus, HWM, MinMax src/ResourceAlgebra/Separation.agda checked separation witnesses +src/ResourceAlgebra/Morphism.agda strict and lax morphisms, classifications tests/reject/*.agda expected rejections (must fail) docs/pre-registration.adoc intent, provenance ledger, obligations -PROOF-STATUS.adoc every claim with its status and artefact +docs/status/PROOF-STATUS.adoc every claim with its status and artefact ---- == Documentation -* link:PROOF-STATUS.adoc[Proof status] +* link:docs/status/PROOF-STATUS.adoc[Proof status] * link:docs/pre-registration.adoc[Pre-registration and obligations] * Family map: `nextgen-typing/docs/TYPE-CONNECTIONS.adoc` @@ -209,7 +217,7 @@ maintainers can brief an AI with `just ai-warmup dev` / `just ai-warmup maintain * *Machine-readable metadata* (`.machine_readable/descriptiles/`) — `STATE`, `META`, `ECOSYSTEM`, `PLAYBOOK`, `AGENTIC`, `NEUROSYM`, `CLADE`, and `anchors/ANCHOR`, in deed, so tools and agents can read the project's state and boundaries. -* *AI gatekeeper protocol* — `rsr-template-repo_chora.deed` (the repo deed) is the +* *AI gatekeeper protocol* — `resource-algebra_chora.deed` (the repo deed) is the universal entry point that tells an AI agent how to work in this repo before it touches anything; it carries the AI allocation policy and the ply directory tree. * *Typed ABI/FFI seam* — `src/interface/Abi/` (Idris2 type + layout proofs) over diff --git a/docs/MAINTAINERS.adoc b/docs/MAINTAINERS.adoc index 458fc55..3f1fad4 100644 --- a/docs/MAINTAINERS.adoc +++ b/docs/MAINTAINERS.adoc @@ -12,9 +12,9 @@ earlier duplicates at `.github/MAINTAINERS` and `docs/attribution/MAINTAINERS.ad |=== | Name | Role | Contact -| {{AUTHOR}} +| Jonathan D.A. Jewell | Lead Maintainer -| https://github.com/{{OWNER}}[@{{OWNER}}] +| https://github.com/hyperpolymath[@hyperpolymath] |=== == Responsibilities diff --git a/docs/architecture/REPOSITORY-MAP.adoc b/docs/architecture/REPOSITORY-MAP.adoc index ff28fb0..5b92b52 100644 --- a/docs/architecture/REPOSITORY-MAP.adoc +++ b/docs/architecture/REPOSITORY-MAP.adoc @@ -113,6 +113,10 @@ predecessors did. | yes | REUSE licence texts, dual-licence model (code MPL-2.0 / docs CC-BY-SA-4.0) +| `PROOF-STATUS.adoc` +| yes +| project proof ledger, linked by README.adoc and docs/pre-registration.adoc + | `README.adoc` | yes | - @@ -161,9 +165,13 @@ predecessors did. | yes | the toolchain: every tool at latest (PROVISIONING-STANDARD §4) -| `rsr-template-repo_chora.deed` +| `resource-algebra.agda-lib` +| yes +| Agda library manifest; Agda discovers it at the library root and resolves src/ relative to it + +| `resource-algebra_chora.deed` | yes -| the repo deed: universal AI entry point; family-7 allocation manifest + ply tree folded in (standards#837 pilot). Filename carries the repo slug (deed dispatch _chora.deed), so repo-init renames it at mint +| repository deed; Canon lockstep reads _chora.deed at the PR head | `scripts/` | yes diff --git a/docs/onboarding/llm-warmup-user.adoc b/docs/onboarding/llm-warmup-user.adoc index 8da8ba4..80b95f6 100644 --- a/docs/onboarding/llm-warmup-user.adoc +++ b/docs/onboarding/llm-warmup-user.adoc @@ -13,7 +13,7 @@ rsr-template-repo (https://github.com/hyperpolymath/rsr-template-repo) is a libr It is not a project in its own right: it is the template every new hyperpolymath repository is created from. It ships CI/CD, machine-readable metadata (`.machine_readable/descriptiles/`), an AI gatekeeper deed -(`rsr-template-repo_chora.deed`), a typed ABI/FFI seam (Idris2 over Zig), Guix and +(`resource-algebra_chora.deed`), a typed ABI/FFI seam (Idris2 over Zig), Guix and mise toolchains, and governance files, all passing the RSR validators before you add a line of your own. diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index aca702c..6792964 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -1,101 +1,97 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -// Template: rsr-template-repo/docs/status/PROOF-STATUS.adoc -// Tracks proof completion. Requirements defined in PROOF-NEEDS.adoc -= Proof Status — {{PROJECT}} - -== Summary - -[cols="2,1,1,1,1,1", options="header"] += resource-algebra — Proof Status +:revdate: 2026-10-14 + +Statuses follow the estate taxonomy: PROVEN / TESTED / ASSUMED / DESIGNED / +OPEN. Every PROVEN line names the module that discharges it under +`--safe --without-K --no-libraries --double-check`. + +== Build invariant + +* All modules carry `{-# OPTIONS --safe --without-K #-}`; no postulates, no + holes, no standard library. — PROVEN by `just check-agda` (All.agda). +* Eight expected rejections fail at their invalid declaration, each with the + message its `-- EXPECT:` line names (`min m n != max m n`, `p != zero`, + `suc _ != zero`, `max m n != m + n`, `max p₁ (n₁ + p₂) != p₁ + p₂`, + `3 != 5`, `inf != fin 3`, `… != bot`); a refusal with any other message + fails the gate. The unit tests in `tests/unit/AllTests.agda` typecheck. — + TESTED by `scripts/check-agda.sh`, which CI (`proofs.yml`) runs. Until + 2026-10-14 the workflow called a `scripts/check.sh` that does not exist, so + no CI run had checked these proofs. The first CI run, on the pinned Agda + 2.6.4.3, passed on 2026-10-14 (resource-algebra#4). + +== Core (Core.agda) + +[cols="1,3,1",options="header"] |=== -| Category | Total | Done | In Progress | Blocked | Remaining - -| ABI/FFI (ABI) | 5 | 0 | 0 | 0 | 5 -| Typing (TP) | 2 | 0 | 0 | 0 | 2 -| Invariant (INV) | 0 | 0 | 0 | 0 | 0 -| Security (SEC) | 0 | 0 | 0 | 0 | 0 -| Concurrency (CONC) | 0 | 0 | 0 | 0 | 0 -| Algorithm (ALG) | 0 | 0 | 0 | 0 | 0 -| Domain (DOM) | 0 | 0 | 0 | 0 | 0 -| *Total* | *7* | *0* | *0* | *0* | *7* +| ID | Claim | Status +| C-1 | `ResourceAlgebra`: alternatives an idempotent commutative monoid, sequence a monoid | PROVEN (definition + derived `unitʳ`) +| C-2 | The ⊕-induced relation `≼` is a partial order with `𝟘` least and `⊕` its join | PROVEN (`≼-refl`, `≼-trans`, `≼-antisym`, `𝟘-least`, `⊕-upperˡ/ʳ`) +| C-3 | Every dioid is ordered: distributivity ⇒ `⊗` monotone on both sides | PROVEN (`IsDioid.ordered`) +| C-4 | `IsAnnihilating` is independent of `IsDioid` (an instance can be one without the other) | TESTED (HWM is a dioid; `tests/reject/HWMAnnihilates.agda` refuses the zero) |=== -*Overall*: 0% proven - -== Proofs Done +== Instances -// Format: -// | ID | Proof | Prover | File | Date | Verified By | -// | ABI-1 | Non-null pointer proofs | Idris2 | verification/proofs/idris2/ABI/Pointers.idr | 2026-XX-XX | idris2 --check | - -[cols="1,3,1,3,1,2", options="header"] +[cols="1,3,1",options="header"] |=== -| ID | Proof | Prover | File | Date | Verified By - -| — | No proofs completed yet | — | — | — | — +| ID | Claim | Status +| L-1 | `Loss` is a `ResourceAlgebra`, `IsDioid`, `IsOrdered`, `IsAnnihilating` with ⊕ = min, ⊗ = +, 𝟘 = inf, 𝟙 = fin 0 | PROVEN (Instances/Loss.agda) +| L-2 | `Loss` is textually the echo-types definition (`experimental/echo-additive/Grade.agda`: `_⊓g_`, `_+g_`) | ASSUMED — transcription reviewed by eye; direction of future import (echo → here or here → echo) OPEN +| M-1 | `MaxPlus` is a `ResourceAlgebra`, `IsDioid`, `IsOrdered`, `IsAnnihilating` with ⊕ = max, ⊗ = +, 𝟘 = bot, 𝟙 = val 0 | PROVEN (Instances/MaxPlus.agda) +| M-2 | `MaxPlus` agrees with tropical-types `instance : CommSemiring Tropical` (Lean 4) | OPEN — cross-prover; port-and-reprove, named bridge obligation, no mechanical link exists or is claimed +| H-1 | `HWM` (peak, drift, drift ≤ peak) is a `ResourceAlgebra`, `IsDioid`, `IsOrdered`; 𝟘 ≡ 𝟙 | PROVEN against the definition in Instances/HWM.agda +| H-2 | `HWM` is occupancy-types' occupancy algebra | DESIGNED — occupancy defines none yet (its v0 counts live bytes; the algebra is R2–R3); signed drift (consuming terms) not modelled +| H-3 | `HWM` has no annihilating zero | TESTED (`tests/reject/HWMAnnihilates.agda`) +| N-1 | `MinMax` (bottleneck) is a `ResourceAlgebra`, `IsDioid`, `IsOrdered`, `IsAnnihilating` on the Loss carrier with ⊕ = min, ⊗ = max (`_⊔g_`, `inf` absorbing), 𝟘 = inf, 𝟙 = fin 0 | PROVEN (Instances/MinMax.agda) +| N-2 | `MinMax` is the bottleneck sequence typed-wasm's `Tropical.tropMax` defines locally | DESIGNED — typed-wasm still defines it locally; moves when typed-wasm's kernel port carries it and its transcription table lists it |=== -== Proofs In Progress +== Morphisms (Morphism.agda) -[cols="1,3,1,2,1,2", options="header"] -|=== -| ID | Proof | Prover | Assignee | Started | Blocker +`Hom A B` preserves 𝟘, 𝟙, ⊕ and ⊗ (what transporting a grade equality +needs). `LaxHom A B` preserves 𝟙 and ⊕, hence is monotone, and maps ⊗ to at +most ⊗ (what transporting a bound needs). -| — | — | — | — | — | — +[cols="1,3,1",options="header"] |=== - -== Proofs Blocked - -[cols="1,3,2,3", options="header"] +| ID | Claim | Status +| F-1 | Both notions have identities and compose; every strict morphism is lax | PROVEN (`id-hom`, `_∘h_`, `id-lax`, `_∘l_`, `lax`) +| F-2 | `peak : HWM → MaxPlus` is lax: the peak of a sequence never exceeds the sum of the peaks | PROVEN (`peak-lax`) +| F-3 | `peak` is not strict | TESTED (`tests/reject/PeakIsStrict.agda`) +| F-4 | No strict morphism leaves HWM for any algebra with 𝟘 ≢ 𝟙; in particular none to MaxPlus or Loss | PROVEN (`no-strict-from-HWM`, `no-strict-HWM→MaxPlus`, `no-strict-HWM→Loss`) +| F-5 | Exactly two strict morphisms Loss → MaxPlus exist, `zero-test` and `support`, and neither distinguishes `fin 1` from `fin 2` | PROVEN (`zero-test-hom`, `support-hom`, `Loss→MaxPlus`, `Loss→MaxPlus-collapses`, `no-injective-Loss→MaxPlus`) +| F-6 | Exactly one strict morphism MaxPlus → Loss exists, `support′` (resource-algebra#3 sketched this direction as "symmetric" to Loss → MaxPlus; it is not: one map, not two. Its other claim, that every positive grade goes to a single point, holds) | PROVEN (`support′-hom`, `MaxPlus→Loss`) +| F-7 | The identity on the carrier is a lax morphism Loss → MinMax: a bottleneck never exceeds the sum | PROVEN (`loss-bottleneck`) |=== -| ID | Proof | Blocked By | Notes -| — | — | — | — -|=== +== Separation (Separation.agda) -== Proofs Remaining - -[cols="1,3,1,1,1,1", options="header"] +[cols="1,3,1",options="header"] |=== -| ID | Proof | Category | Prover | Priority | Est. Effort - -| ABI-1 | Non-null pointer proofs | ABI | Idris2 | P1 | 2h -| ABI-2 | Memory layout correctness | ABI | Idris2 | P1 | 4h -| ABI-3 | Platform type size proofs | ABI | Idris2 | P1 | 2h -| ABI-4 | FFI function return type proofs | ABI | Idris2 | P1 | 2h -| ABI-5 | C ABI compliance | ABI | Idris2 | P1 | 4h -| TP-1 | Core data type well-formedness | TP | Idris2 | P1 | 4h -| TP-2 | Public API type safety | TP | Lean4 | P2 | 4h +| ID | Claim | Status +| S-1 | Sequencing peaks 2 and 3 gives 3 under HWM and 5 under MaxPlus: an occupancy bound is not a cost bound | TESTED (computed; `occupancy-is-not-cost`) +| S-2 | On the same numbers, Loss alternatives give `fin 2` and MaxPlus alternatives give `val 3`: echo's join is min, tropical's is max | TESTED (computed; `alternatives-differ`) +| S-3 | `val 1 ≼ val 2` in MaxPlus and `fin 2 ≼ fin 1` in Loss: the induced order runs the opposite way | TESTED (computed) +| S-4 | Sequencing 2 then 3 gives `fin 5` under Loss and `fin 3` under MinMax: a bottleneck bound is not a loss bound | TESTED (computed; `bottleneck-is-not-sum`; `tests/reject/MinMaxIsLoss.agda` refuses the general identification) |=== -== Verification Commands - -[source,bash] ----- -# Check all Idris2 proofs -just proof-check-idris2 - -# Check all Lean4 proofs -just proof-check-lean4 - -# Check all Agda proofs -just proof-check-agda - -# Check all Coq proofs -just proof-check-coq - -# Run all proof checks -just proof-check-all - -# Scan for dangerous patterns -panic-attack assail --proofs-only ----- - -== Changelog - -[cols="1,3,1", options="header"] -|=== -| Date | Change | By - -| 2026-04-04 | Initial proof status tracking | Template -|=== +== Open (honest — NOT proved) + +* K-CUT-LOSS itself. It is not stated here; this repository supplies the + algebra it will be parametric in. Expectation (DESIGNED): only the core + record is needed for the equality; `IsOrdered` is needed for the + K-CUT-WARRANT bound. +* L-2 import direction; M-2 Lean bridge; H-2 supersession by occupancy; + N-2 typed-wasm adoption. +* Transport of K-CUT-LOSS along a morphism. F-1..F-7 supply the maps and + say which exist; no theorem here states that a strict morphism carries a + cut-loss equality, or a lax one a cut-loss bound. That theorem belongs + with K-CUT-LOSS (choreographic-types), and is OPEN. +* Morphisms out of or into MinMax other than `loss-bottleneck` are not + classified. + +== Discipline + +Prose, citation and artefact must agree before any status moves. A status +moves only with a named module or a named log line. diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index 8597095..90483f3 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -7,7 +7,7 @@ A repo minted from the template does not inherit it: `just repo-init` replaces this file with `build/templates/ROADMAP.adoc.in`. Phase and maturity are not recorded here. They live in the repo deed, -`rsr-template-repo_chora.deed`, in the `(status …)` and `(maturity …)` +`resource-algebra_chora.deed`, in the `(status …)` and `(maturity …)` clauses (`just state-phase` prints both). This file took over the journal half of the retired STATE record diff --git a/rsr-template-repo_chora.deed b/resource-algebra_chora.deed similarity index 92% rename from rsr-template-repo_chora.deed rename to resource-algebra_chora.deed index ab6d329..3ea6799 100644 --- a/rsr-template-repo_chora.deed +++ b/resource-algebra_chora.deed @@ -1,6 +1,6 @@ ;; SPDX-License-Identifier: MPL-2.0 ; -; The repo deed of rsr-template-repo: one-deed-per-repo doctrine (standards#837, +; The repo deed of resource-algebra: one-deed-per-repo doctrine (standards#837, ; owner ruling 2026-09-19, Option A). Folds the former ply manifest tree ; (82 per-directory manifests) and the family-7 AI allocation manifest ; into deed clauses. @@ -16,9 +16,9 @@ ; field; scripts/deed-clause.sh is the one writer. (repo-deed :schema-version "1.0.0" - :canonical-name "rsr-template-repo" + :canonical-name "resource-algebra" :beholding-chora #u5"estate/chora" - :repo-uuid #u5"github.com/hyperpolymath/rsr-template-repo" + :repo-uuid #u5"github.com/hyperpolymath/resource-algebra" ; The canon pin: which release of hyperpolymath/standards canon.lock this ; repo implements. It is the ONLY canon pin in this deed (deed_canon ; refuses zero or two); the (rsr-profile) clause below declares @@ -38,37 +38,30 @@ ; ORDER, not a rejected change: land the spine's adoption first, then the ; canon change is a one-line bump. :order "spine-adopts-then-canon-releases") - ; >>> repo-identity (repo-init replaces this block at mint) - ; The template's OWN identity. `just repo-init` swaps everything between - ; these two markers for build/templates/identity.deed.in, filled for the - ; new repo. Before that swap existed every minted repo inherited this - ; block's uuid and canonical-name and told arriving agents it WAS the - ; template (corrected in chronicles-of-slavia and scaffoldia 2026-07-16). - ; The uuid is not stored: it is uuid5(URL namespace, the header - ; :repo-uuid name), a5ea1382-a34c-5334-8a46-a2ebe904c810 here. - ; Identity, clade, forges, lineage, status: mapping clade-to-repo-deed. + ; >>> repo-identity + ; Repository identity follows the GitHub repository and the Agda library + ; described in README.adoc. Clade assignment remains an owner decision, + ; as in build/templates/identity.deed.in. (identity :primary-forge github :owner "hyperpolymath" - :prefixed-name "rm-rsr-template-repo") + :prefixed-name "UNASSIGNED-resource-algebra") (clade - :primary rm - :primary-name "Repo Management & Tooling" + :primary UNASSIGNED + :primary-name "UNASSIGNED" :secondary () - :assigned "2026-03-16" - :rationale "Repo Management & Tooling (`rm`): the core value proposition is scaffolding repositories — CI/CD, AI manifests, ABI/FFI seams, governance — that other projects are instantiated from. `gv` was previously claimed as a secondary and is dropped: the template SHIPS governance files, but shipping them is not being a governance project. That authority lives in `standards` and `metadatastician-governance`. The inherited [\"gv\"] propagated into every repo created from this template, where it was even less meant.") + :rationale "Clade not yet assigned for resource-algebra.") (forges - :github "hyperpolymath/rsr-template-repo" - :gitlab "hyperpolymath/rsr-template-repo" - :bitbucket "hyperpolymath/rsr-template-repo") + :github "hyperpolymath/resource-algebra") (lineage :type standalone :parent "" - :born "2026-03-16" - :previous-names ()) + :born "2026-10-12" + :previous-names () + :instantiated-from "rsr-template-repo") (status :phase active - :since "2026-03-16" + :since "2026-10-12" :present #t :aliases () :merged-into "" @@ -76,33 +69,22 @@ :successors () :ended "" (history - (entry :phase active :since "2026-03-16" :note "the estate's canonical repository template; in production use"))) - ; Maturity has its own clause (owner decision 2026-10-02; standards - ; 1-formats/deed/vocabulary/maturity.adoc). No :since: the date the - ; template reached production was never recorded. Milestones, next actions - ; and blockers live in docs/status/ROADMAP.adoc. + (entry :phase active :since "2026-10-12" :note "Agda resource-algebra library, created from rsr-template-repo"))) + ; Proofs and remaining adoption obligations are recorded in PROOF-STATUS.adoc. (maturity - :level production) + :level experimental) ; Ecosystem: mapping meta-ecosystem-to-repo-deed. (ecosystem - :project "rsr-template-repo" + :project "resource-algebra" :ecosystem "hyperpolymath" - :position-type "repository-template" - :purpose "Canonical RSR-compliant repository template: scaffolding (CI/CD, AI manifests, ABI/FFI standards, container ecosystem, governance) that new hyperpolymath projects are instantiated from." - :not ("a project in its own right" - "Scaffoldia (the full-featured repo designer)" - "standards (the canon source this template operationalises)") - :pipeline-position "foundation" - :chain "standards → rsr-template-repo → (every estate repo)" - :pipeline-notes "rsr-template-repo turns the RSR standard into runnable scaffolding. New repos are created from it via `just repo-init`, which substitutes the {{PLACEHOLDER}} tokens." - :coordination standards - (related :name "standards" :relationship standard-source :notes "Defines the RSR standard, contractile canon, and policies that this template operationalises.") - (related :name "stapeln" :relationship build-tooling :notes "Layer-based container build system; the template ships stapeln.toml scaffolding.") - (related :name "selur-compose" :relationship build-tooling :notes "Service composition; the template ships selur-compose.toml scaffolding.") - (related :name "k9-svc" :relationship validation-tooling :notes "Runs the self-validating k9.ncl checks (.machine_readable/self-validating/).") - (related :name "cerro-torre" :relationship signing-tooling :notes "Container/image signing provider referenced by the container scaffolding.") - (related :name "svalinn" :relationship verification-tooling :notes "Supply-chain verification referenced by the container scaffolding.") - (related :name "vordr" :relationship verification-tooling :notes "Build/artifact verification referenced by the container scaffolding.")) + :position-type "library" + :purpose "Parametric resource algebra in Agda, with Loss, MaxPlus, HWM and MinMax instances and strict/lax morphisms." + :not ("a repository template" + "the K-CUT statement, which belongs in choreographic-types" + "occupancy-types' own algebra, for which HWM is a proposal") + :pipeline-position "kernel" + :chain "resource-algebra → hyperpolymath type family" + (related :name "rsr-template-repo" :relationship minted-from :notes "Source of the inherited repository scaffolding.")) ; <<< repo-identity ; Meta: mapping meta-ecosystem-to-repo-deed. A minted repo keeps this ; clause (self-name pass applied) and edits it as its own. @@ -167,9 +149,9 @@ (methodology :instructions-clause "bot-directives" :default-mode hybrid)) (manifest :version "0.1.0" - :last-updated "{{CURRENT_DATE}}" - :project "[YOUR-REPO-NAME]" - :purpose "Canonical RSR (Rhodium Standard Repository) template — governance, CI/CD, machine-readable metadata, ABI/FFI seam and formal-verification scaffolding that hyperpolymath projects are instantiated from." + :last-updated "2026-10-14" + :project "resource-algebra" + :purpose "Parametric resource algebra in Agda, with checked instances, separation witnesses and strict/lax morphism classifications." (agent :name CLAUDE :role "proofs, compilers, repo-local implementation, CI/CD, formal verification, Rust/Idris2/Zig") (agent :name CHATGPT :role "prose, papers, publication review, standards docs, outreach drafts, letters") (agent :name GEMINI :role "estate audits, cross-repo sweeps, long-context triage, pattern detection") @@ -183,8 +165,8 @@ (ply (directory :ply 1 :path ".github") (directory :id "machine-readable-pillar" :ply 1 :path ".machine_readable" :description "Registry for all machine-readable metadata, policies, and internal\nautomation scripts." - (canonical-locations :ai_configs "ai/" :anchor "rsr-template-repo_chora.deed (anchor)" :compliance "compliance/" :neurosym "rsr-template-repo_chora.deed (neurosym)" :playbook "rsr-template-repo_chora.deed (playbook)" :policies "rsr-template-repo_chora.deed (policies)" :scripts "scripts/") - :invariants ("Repo metadata MUST live in the repo deed (rsr-template-repo_chora.deed) and follow the DEED grammar" "Internal automation MUST live in scripts/ subfolder") + (canonical-locations :ai_configs "ai/" :anchor "resource-algebra_chora.deed (anchor)" :compliance "compliance/" :neurosym "resource-algebra_chora.deed (neurosym)" :playbook "resource-algebra_chora.deed (playbook)" :policies "resource-algebra_chora.deed (policies)" :scripts "scripts/") + :invariants ("Repo metadata MUST live in the repo deed (resource-algebra_chora.deed) and follow the DEED grammar" "Internal automation MUST live in scripts/ subfolder") (directory :id "ai-registry" :ply 2 :path ".machine_readable/ai" :description "Sub-registry for ai metadata.") (directory :id "configs-registry" :ply 2 :path ".machine_readable/configs" :description "Sub-registry for configs metadata.") (directory :ply 0 :path ".machine_readable/descriptiles" :description "This manifest declares the AI-assistant context for the descriptiles machine-readable metadata directory." @@ -306,7 +288,7 @@ ; and the golden path. The CLAUDE.md arrival pack reads anchor/golden-path and hashes this clause (ANCHOR@…). (anchor :schema "hyperpolymath.anchor/1" - :repo "{{OWNER}}/{{REPO}}" + :repo "hyperpolymath/resource-algebra" :authority "upstream-canonical" :purpose ( "Define canonical semantics and policy boundaries for this repository." @@ -315,13 +297,13 @@ ) (metadata :version "1.0.0" - :last-updated "{{CURRENT_DATE}}") + :last-updated "2026-10-14") (identity - :project "{{PROJECT_NAME}}" + :project "Resource Algebra" ; language | library | service | tool - :kind "{{PROJECT_KIND}}" - :one-sentence "{{PROJECT_PURPOSE}}" - :domain "{{PROJECT_DOMAIN}}") + :kind "library" + :one-sentence "Parametric resource algebra in Agda with checked instances and strict/lax morphisms." + :domain "formal-methods") (semantic-authority :policy "canonical" :owns ( @@ -476,7 +458,7 @@ (methodology (metadata :version "1.0.0" - :last-updated "{{CURRENT_DATE}}" + :last-updated "2026-10-14" :spec "https://github.com/hyperpolymath/standards/blob/main/1-formats/a2ml/agentic/docs/ADR-002-methodology-layer.adoc") ; ============================================================================ ; MODE SELECTION @@ -520,7 +502,7 @@ ; What makes this project special. Agents should DEEPEN this, not broaden it. ; Customise this per project — the template default is generic. (unique-strength - :description "{{PROJECT_UNIQUE_STRENGTH}}" + :description "Checked separation witnesses and classifications of strict and lax morphisms between resource algebras." :deepen-not-broaden #t) ; ============================================================================ ; DIVERGENT INVARIANTS @@ -559,7 +541,7 @@ ; These rules detect corrupt/template/stale state files. (state-validation ; A regex, not a literal list. The list form named the exact strings it was - ; meant to catch ("{{PROJECT}}"), so `just repo-init` substituted the detector along + ; meant to catch (an upper-snake brace token), so `just repo-init` substituted the detector along ; with everything else and shipped reject-if-contains = ["MY_PROJECT", ...] — ; a guard against unfilled tokens that had been eaten by the filling. The ; escaped pattern below contains no token for init to match, and covers every @@ -578,7 +560,7 @@ (coverage (metadata :version "1.0.0" - :last-updated "{{CURRENT_DATE}}") + :last-updated "2026-10-14") ; ============================================================================ ; COVERAGE STATE ; ============================================================================ @@ -596,7 +578,7 @@ (debt (metadata :version "1.0.0" - :last-updated "{{CURRENT_DATE}}")) + :last-updated "2026-10-14")) ; rra — directives for Robot Repo Automaton (RRA) enforcing the Platonic Ideal root. (rra :target "robot-repo-automaton" @@ -611,7 +593,7 @@ ; The pattern ".*" allows hidden dotfiles implicitly; RRA checks specific ; dotfile rules below. (allow-list - :files ("README.adoc" "CHANGELOG.adoc" "Justfile" "LICENSE" "rsr-template-repo_chora.deed" "CITATION.cff" "CLAUDE.md") + :files ("README.adoc" "CHANGELOG.adoc" "Justfile" "LICENSE" "resource-algebra_chora.deed" "CITATION.cff" "CLAUDE.md") :patterns (".*")) ; Relocation rules: move heavy prose out of the root (relocations @@ -709,8 +691,8 @@ ; See: https://github.com/hyperpolymath/standards/tree/main/groove-protocol (groove :version "1.0" - ; Service identity — replace {{REPO}} with your project name - :service "{{REPO}}" + ; Service identity — replace resource-algebra with your project name + :service "resource-algebra" :service-version "0.1.0" ; Primary port — MUST be unique across the ecosystem. Check PORT-REGISTRY.md ; in the standards repo before assigning: @@ -739,7 +721,7 @@ (maintenance-axes (metadata :version "1.0.0" - :last-updated "{{CURRENT_DATE}}" + :last-updated "2026-10-14" :scope "repo") (discovery :human-entrypoints ( diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh index 3697a16..61d5e46 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -8,6 +8,9 @@ prover="${AGDA:-agda}" "$prover" --version flags=(--safe --without-K --no-libraries --ignore-interfaces --double-check -i src) "$prover" "${flags[@]}" src/ResourceAlgebra/All.agda +# Unit tests (closed computations and small lemmas over the instances). +"$prover" "${flags[@]}" -i tests/unit tests/unit/AllTests.agda +echo "PASS: unit tests (tests/unit/AllTests.agda)" mkdir -p _build/check-logs shopt -s nullglob rejects=(tests/reject/*.agda) @@ -18,6 +21,13 @@ if (( ${#rejects[@]} == 0 )); then fi for file in "${rejects[@]}"; do name="$(basename -- "$file" .agda)" + # The refusal must carry the message the fixture names: failing at the + # declaration for some other reason must not pass. + expect="$(sed -n 's/^-- EXPECT: //p' "$file" | head -1)" + if [ -z "$expect" ]; then + echo "ERROR: $name has no '-- EXPECT: ' line" >&2 + exit 1 + fi log="_build/check-logs/$name.log" if "$prover" "${flags[@]}" -i tests/reject "$file" >"$log" 2>&1; then cat "$log" @@ -31,6 +41,11 @@ for file in "${rejects[@]}"; do echo "ERROR: unexpected failure while checking $name" >&2 exit 1 fi - echo "PASS: rejected $name at its invalid declaration" + if ! grep -Eq -- "$expect" "$log"; then + cat "$log" + echo "ERROR: $name was refused, but not with: $expect" >&2 + exit 1 + fi + echo "PASS: rejected $name at its invalid declaration ($expect)" done -echo "PASS: core proofs and all ${#rejects[@]} expected rejections" +echo "PASS: core proofs, unit tests and all ${#rejects[@]} expected rejections" diff --git a/src/ResourceAlgebra/All.agda b/src/ResourceAlgebra/All.agda index ecdbe11..0ef472b 100644 --- a/src/ResourceAlgebra/All.agda +++ b/src/ResourceAlgebra/All.agda @@ -9,4 +9,6 @@ import ResourceAlgebra.Core import ResourceAlgebra.Instances.Loss import ResourceAlgebra.Instances.MaxPlus import ResourceAlgebra.Instances.HWM +import ResourceAlgebra.Instances.MinMax import ResourceAlgebra.Separation +import ResourceAlgebra.Morphism diff --git a/src/ResourceAlgebra/Instances/MinMax.agda b/src/ResourceAlgebra/Instances/MinMax.agda new file mode 100644 index 0000000..66d5e34 --- /dev/null +++ b/src/ResourceAlgebra/Instances/MinMax.agda @@ -0,0 +1,87 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- The min-max (bottleneck) grade: the Loss carrier ℕ ∪ {∞} with +-- _⊓g_ = alternatives = MIN (the better path) — the semiring "⊕", unit inf +-- _⊔g_ = sequence = MAX (the worst hop) — the semiring "⊗", unit fin 0 +-- inf absorbs under both: an unreachable hop makes the path unreachable, +-- and an unreachable alternative is never chosen. +-- +-- Consumer: typed-wasm L11's bottleneck reading (Tropical.tropMax, its +-- Level11BottleneckProof), which until now defined this sequence locally +-- and was the one allowlisted exception to its one-min-plus/one-max-plus +-- gate. It shares Loss's carrier and alternatives on purpose: the +-- identity on the carrier is a lax morphism Loss → MinMax (Morphism.agda, +-- `loss-bottleneck`), because a bottleneck never exceeds the sum. +-- +-- It is neither min-plus (sequence is max, not +) nor max-plus (max is the +-- sequence, not the alternatives, and 𝟘 is inf, not −∞): Separation.agda +-- S-4 and tests/reject/MinMaxIsLoss.agda are the checked statements. +module ResourceAlgebra.Instances.MinMax where + +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Core +open import ResourceAlgebra.Instances.Loss + using (Grade; fin; inf; _⊓g_; ⊓g-assoc; ⊓g-comm; ⊓g-idem) + +infixl 7 _⊔g_ +_⊔g_ : Grade → Grade → Grade +inf ⊔g _ = inf +fin m ⊔g inf = inf +fin m ⊔g fin n = fin (max m n) + +---------------------------------------------------------------------- +-- Sequence: (⊔g, fin 0) is a monoid +⊔g-assoc : ∀ a b c → (a ⊔g b) ⊔g c ≡ a ⊔g (b ⊔g c) +⊔g-assoc (fin a) (fin b) (fin c) = cong fin (max-assoc a b c) +⊔g-assoc (fin a) (fin b) inf = refl +⊔g-assoc (fin a) inf c = refl +⊔g-assoc inf b c = refl + +⊔g-unitˡ : ∀ a → fin 0 ⊔g a ≡ a +⊔g-unitˡ (fin a) = refl +⊔g-unitˡ inf = refl + +⊔g-unitʳ : ∀ a → a ⊔g fin 0 ≡ a +⊔g-unitʳ (fin a) = cong fin (max-zeroʳ a) +⊔g-unitʳ inf = refl + +---------------------------------------------------------------------- +-- The instance, and its layers +MinMax : ResourceAlgebra +MinMax = record + { Grade = Grade + ; _⊕_ = _⊓g_ + ; _⊗_ = _⊔g_ + ; 𝟘 = inf + ; 𝟙 = fin 0 + ; alt = record { assoc = ⊓g-assoc ; comm = ⊓g-comm ; idem = ⊓g-idem ; unitˡ = λ _ → refl } + ; seq = record { assoc = ⊔g-assoc ; unitˡ = ⊔g-unitˡ ; unitʳ = ⊔g-unitʳ } + } + +MinMax-dioid : IsDioid MinMax +MinMax-dioid = record { distribˡ = distribˡ ; distribʳ = distribʳ } + where + distribˡ : ∀ a b c → a ⊔g (b ⊓g c) ≡ (a ⊔g b) ⊓g (a ⊔g c) + distribˡ (fin a) (fin b) (fin c) = cong fin (max-distribˡ-min a b c) + distribˡ (fin a) (fin b) inf = refl + distribˡ (fin a) inf c = refl + distribˡ inf b c = refl + + distribʳ : ∀ a b c → (a ⊓g b) ⊔g c ≡ (a ⊔g c) ⊓g (b ⊔g c) + distribʳ (fin a) (fin b) (fin c) = cong fin (max-distribʳ-min a b c) + distribʳ (fin a) (fin b) inf = refl + distribʳ (fin a) inf (fin c) = refl + distribʳ (fin a) inf inf = refl + distribʳ inf b c = refl + +MinMax-ordered : IsOrdered MinMax +MinMax-ordered = IsDioid.ordered MinMax-dioid + +MinMax-annihilating : IsAnnihilating MinMax +MinMax-annihilating = record { annihilˡ = λ _ → refl ; annihilʳ = annihilʳ } + where + annihilʳ : ∀ a → a ⊔g inf ≡ inf + annihilʳ (fin _) = refl + annihilʳ inf = refl diff --git a/src/ResourceAlgebra/Morphism.agda b/src/ResourceAlgebra/Morphism.agda new file mode 100644 index 0000000..a1f0423 --- /dev/null +++ b/src/ResourceAlgebra/Morphism.agda @@ -0,0 +1,305 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- Morphisms between resource algebras (resource-algebra#3). +-- +-- Hom A B strict: preserves 𝟘, 𝟙, ⊕ and ⊗. What transport of a grade +-- *equality* (K-CUT-LOSS) across instances needs. +-- LaxHom A B preserves 𝟙 and ⊕ (hence is monotone) and maps ⊗ to at most +-- ⊗: h (a ⊗ b) ≼ h a ⊗ h b. What transport of a *bound* +-- needs. 𝟘 is not asked for: B's 𝟘 is least, so B.𝟘 ≼ h A.𝟘 +-- holds for free (`LaxHom.map-𝟘`). +-- +-- Both compose and have identities. The instances below are the maps the +-- typed-wasm levels actually use, and the classifications show which maps +-- cannot exist: +-- +-- peak-lax HWM → MaxPlus is lax (occupancy never exceeds cost; +-- occupancy-types R-3), and there is no strict map out +-- of HWM into any algebra with 𝟘 ≢ 𝟙 (no-strict-from-HWM). +-- Loss→MaxPlus exactly two strict maps, zero-test and support; neither +-- tells fin 1 from fin 2. +-- MaxPlus→Loss exactly one strict map, support′. +-- loss-bottleneck the identity on the carrier is lax Loss → MinMax +-- (a bottleneck never exceeds the sum); it is not strict +-- (Separation S-4). +module ResourceAlgebra.Morphism where + +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Core +open import ResourceAlgebra.Instances.Loss as L using (Loss; fin; inf; _⊓g_; _+g_) +open import ResourceAlgebra.Instances.MaxPlus as M using (MaxPlus; Tropical; val; bot; tAdd; tMul) +open import ResourceAlgebra.Instances.HWM as H using (HWM; hwm; peak; _⊕h_; _⊗h_) +open import ResourceAlgebra.Instances.MinMax as N using (MinMax; _⊔g_) + +---------------------------------------------------------------------- +-- The two notions +module _ (A B : ResourceAlgebra) where + private + module A = ResourceAlgebra A + module B = ResourceAlgebra B + + record Hom : Set where + field + map : A.Grade → B.Grade + map-𝟘 : map A.𝟘 ≡ B.𝟘 + map-𝟙 : map A.𝟙 ≡ B.𝟙 + map-⊕ : ∀ a b → map (a A.⊕ b) ≡ map a B.⊕ map b + map-⊗ : ∀ a b → map (a A.⊗ b) ≡ map a B.⊗ map b + + record LaxHom : Set where + field + map : A.Grade → B.Grade + map-𝟙 : map A.𝟙 ≡ B.𝟙 + map-⊕ : ∀ a b → map (a A.⊕ b) ≡ map a B.⊕ map b + map-⊗ : ∀ a b → map (a A.⊗ b) B.≼ (map a B.⊗ map b) + + -- Preserving ⊕ is already monotonicity for the induced order. + mono : ∀ {a b} → a A.≼ b → map a B.≼ map b + mono {a} {b} p = trans (sym (map-⊕ a b)) (cong map p) + + map-𝟘 : B.𝟘 B.≼ map A.𝟘 + map-𝟘 = B.𝟘-least (map A.𝟘) + + -- Every strict morphism is lax. + lax : Hom → LaxHom + lax h = record + { map = Hom.map h + ; map-𝟙 = Hom.map-𝟙 h + ; map-⊕ = Hom.map-⊕ h + ; map-⊗ = λ a b → + subst (λ x → x B.≼ (Hom.map h a B.⊗ Hom.map h b)) + (sym (Hom.map-⊗ h a b)) + (B.≼-refl (Hom.map h a B.⊗ Hom.map h b)) + } + +---------------------------------------------------------------------- +-- Identities and composition +id-hom : (A : ResourceAlgebra) → Hom A A +id-hom A = record + { map = λ a → a ; map-𝟘 = refl ; map-𝟙 = refl + ; map-⊕ = λ _ _ → refl ; map-⊗ = λ _ _ → refl } + +infixr 9 _∘h_ +_∘h_ : {A B C : ResourceAlgebra} → Hom B C → Hom A B → Hom A C +g ∘h f = record + { map = λ a → Hom.map g (Hom.map f a) + ; map-𝟘 = trans (cong (Hom.map g) (Hom.map-𝟘 f)) (Hom.map-𝟘 g) + ; map-𝟙 = trans (cong (Hom.map g) (Hom.map-𝟙 f)) (Hom.map-𝟙 g) + ; map-⊕ = λ a b → trans (cong (Hom.map g) (Hom.map-⊕ f a b)) + (Hom.map-⊕ g (Hom.map f a) (Hom.map f b)) + ; map-⊗ = λ a b → trans (cong (Hom.map g) (Hom.map-⊗ f a b)) + (Hom.map-⊗ g (Hom.map f a) (Hom.map f b)) + } + +id-lax : (A : ResourceAlgebra) → LaxHom A A +id-lax A = lax A A (id-hom A) + +infixr 9 _∘l_ +_∘l_ : {A B C : ResourceAlgebra} → LaxHom B C → LaxHom A B → LaxHom A C +_∘l_ {C = C} g f = record + { map = λ a → LaxHom.map g (LaxHom.map f a) + ; map-𝟙 = trans (cong (LaxHom.map g) (LaxHom.map-𝟙 f)) (LaxHom.map-𝟙 g) + ; map-⊕ = λ a b → trans (cong (LaxHom.map g) (LaxHom.map-⊕ f a b)) + (LaxHom.map-⊕ g (LaxHom.map f a) (LaxHom.map f b)) + ; map-⊗ = λ a b → ResourceAlgebra.≼-trans C + (LaxHom.mono g (LaxHom.map-⊗ f a b)) + (LaxHom.map-⊗ g (LaxHom.map f a) (LaxHom.map f b)) + } + +---------------------------------------------------------------------- +-- HWM → MaxPlus: the peak is a lax morphism, never a strict one +peak-lax : LaxHom HWM MaxPlus +peak-lax = record + { map = λ g → val (peak g) + ; map-𝟙 = refl + ; map-⊕ = ⊕-case + ; map-⊗ = ⊗-case + } + where + ⊕-case : ∀ a b → val (peak (a ⊕h b)) ≡ tAdd (val (peak a)) (val (peak b)) + ⊕-case (hwm p n _) (hwm p' n' _) = refl + + -- max p₁ (n₁ + p₂) ≤ p₁ + p₂, because the drift n₁ is at most the peak p₁. + ⊗-case : ∀ a b → tAdd (val (peak (a ⊗h b))) (tMul (val (peak a)) (val (peak b))) + ≡ tMul (val (peak a)) (val (peak b)) + ⊗-case (hwm p₁ n₁ b₁) (hwm p₂ n₂ b₂) = + cong val (max-≤ (max-lub (≤-+ʳ p₁ p₂) (+-monoˡ-≤ p₂ b₁))) + +-- HWM's 𝟘 is its 𝟙, so a strict map out of HWM would identify B's 𝟘 and 𝟙. +no-strict-from-HWM : (B : ResourceAlgebra) + → ResourceAlgebra.𝟘 B ≢ ResourceAlgebra.𝟙 B + → Hom HWM B → ⊥ +no-strict-from-HWM B 𝟘≢𝟙 h = 𝟘≢𝟙 (trans (sym (Hom.map-𝟘 h)) (Hom.map-𝟙 h)) + +no-strict-HWM→MaxPlus : Hom HWM MaxPlus → ⊥ +no-strict-HWM→MaxPlus = no-strict-from-HWM MaxPlus (λ ()) + +no-strict-HWM→Loss : Hom HWM Loss → ⊥ +no-strict-HWM→Loss = no-strict-from-HWM Loss (λ ()) + +---------------------------------------------------------------------- +-- Loss → MaxPlus: exactly two strict morphisms +zero-test : L.Grade → Tropical +zero-test (fin zero) = val 0 +zero-test (fin (suc _)) = bot +zero-test inf = bot + +support : L.Grade → Tropical +support (fin _) = val 0 +support inf = bot + +zero-test-hom : Hom Loss MaxPlus +zero-test-hom = record + { map = zero-test ; map-𝟘 = refl ; map-𝟙 = refl ; map-⊕ = ⊕-case ; map-⊗ = ⊗-case } + where + ⊕-case : ∀ a b → zero-test (a ⊓g b) ≡ tAdd (zero-test a) (zero-test b) + ⊕-case (fin zero) (fin zero) = refl + ⊕-case (fin zero) (fin (suc n)) = refl + ⊕-case (fin (suc m)) (fin zero) = refl + ⊕-case (fin (suc m)) (fin (suc n)) = refl + ⊕-case (fin zero) inf = refl + ⊕-case (fin (suc m)) inf = refl + ⊕-case inf b = refl + + ⊗-case : ∀ a b → zero-test (a +g b) ≡ tMul (zero-test a) (zero-test b) + ⊗-case (fin zero) (fin zero) = refl + ⊗-case (fin zero) (fin (suc n)) = refl + ⊗-case (fin (suc m)) (fin n) = refl + ⊗-case (fin zero) inf = refl + ⊗-case (fin (suc m)) inf = refl + ⊗-case inf b = refl + +support-hom : Hom Loss MaxPlus +support-hom = record + { map = support ; map-𝟘 = refl ; map-𝟙 = refl ; map-⊕ = ⊕-case ; map-⊗ = ⊗-case } + where + ⊕-case : ∀ a b → support (a ⊓g b) ≡ tAdd (support a) (support b) + ⊕-case (fin m) (fin n) = refl + ⊕-case (fin m) inf = refl + ⊕-case inf b = refl + + ⊗-case : ∀ a b → support (a +g b) ≡ tMul (support a) (support b) + ⊗-case (fin m) (fin n) = refl + ⊗-case (fin m) inf = refl + ⊗-case inf b = refl + +val-injective : ∀ {m n} → val m ≡ val n → m ≡ n +val-injective refl = refl + +-- Every strict morphism Loss → MaxPlus is zero-test or support, pointwise. +-- fin 0 ⊓g fin 1 = fin 0 forces h (fin 1) ∈ {bot, val 0}; every fin n is +-- fin 1 sequenced n times, so h (fin 1) decides the rest. +Loss→MaxPlus : (h : Hom Loss MaxPlus) + → (∀ a → Hom.map h a ≡ zero-test a) ⊎ (∀ a → Hom.map h a ≡ support a) +Loss→MaxPlus h = go (Hom.map h (fin 1)) refl + where + f = Hom.map h + + step : ∀ n → f (fin (suc n)) ≡ tMul (f (fin 1)) (f (fin n)) + step n = Hom.map-⊗ h (fin 1) (fin n) + + -- val 0 ≡ tAdd (val 0) (f (fin 1)) + pin : val 0 ≡ tAdd (val 0) (f (fin 1)) + pin = trans (sym (Hom.map-𝟙 h)) + (trans (Hom.map-⊕ h (fin 0) (fin 1)) + (cong (λ z → tAdd z (f (fin 1))) (Hom.map-𝟙 h))) + + go : (x : Tropical) → f (fin 1) ≡ x + → (∀ a → f a ≡ zero-test a) ⊎ (∀ a → f a ≡ support a) + go bot e = inj₁ pointwise + where + pointwise : ∀ a → f a ≡ zero-test a + pointwise (fin zero) = Hom.map-𝟙 h + pointwise (fin (suc n)) = trans (step n) (cong (λ z → tMul z (f (fin n))) e) + pointwise inf = Hom.map-𝟘 h + go (val c) e = inj₂ pointwise + where + c≡0 : c ≡ 0 + c≡0 = sym (val-injective (trans pin (cong (tAdd (val 0)) e))) + + fin-val0 : ∀ n → f (fin n) ≡ val 0 + fin-val0 zero = Hom.map-𝟙 h + fin-val0 (suc n) = + trans (step n) + (trans (cong (λ z → tMul z (f (fin n))) (trans e (cong val c≡0))) + (cong (tMul (val 0)) (fin-val0 n))) + + pointwise : ∀ a → f a ≡ support a + pointwise (fin n) = fin-val0 n + pointwise inf = Hom.map-𝟘 h + +-- So no strict morphism Loss → MaxPlus tells fin 1 from fin 2: the +-- separation witnesses, stated for every morphism rather than for one. +Loss→MaxPlus-collapses : (h : Hom Loss MaxPlus) → Hom.map h (fin 1) ≡ Hom.map h (fin 2) +Loss→MaxPlus-collapses h with Loss→MaxPlus h +... | inj₁ z = trans (z (fin 1)) (sym (z (fin 2))) +... | inj₂ s = trans (s (fin 1)) (sym (s (fin 2))) + +no-injective-Loss→MaxPlus : (h : Hom Loss MaxPlus) + → (∀ a b → Hom.map h a ≡ Hom.map h b → a ≡ b) → ⊥ +no-injective-Loss→MaxPlus h inj with inj (fin 1) (fin 2) (Loss→MaxPlus-collapses h) +... | () + +---------------------------------------------------------------------- +-- MaxPlus → Loss: exactly one strict morphism +support′ : Tropical → L.Grade +support′ (val _) = fin 0 +support′ bot = inf + +support′-hom : Hom MaxPlus Loss +support′-hom = record + { map = support′ ; map-𝟘 = refl ; map-𝟙 = refl ; map-⊕ = ⊕-case ; map-⊗ = ⊗-case } + where + ⊕-case : ∀ a b → support′ (tAdd a b) ≡ support′ a ⊓g support′ b + ⊕-case (val m) (val n) = refl + ⊕-case (val m) bot = refl + ⊕-case bot b = refl + + ⊗-case : ∀ a b → support′ (tMul a b) ≡ support′ a +g support′ b + ⊗-case (val m) (val n) = refl + ⊗-case (val m) bot = refl + ⊗-case bot b = refl + +fin-injective : ∀ {m n} → fin m ≡ fin n → m ≡ n +fin-injective refl = refl + +-- val 0 ⊕ val 1 = val 1 forces h (val 1) = fin 0 ⊓g h (val 1), which rules +-- out inf and pins every finite value to fin 0. +MaxPlus→Loss : (h : Hom MaxPlus Loss) → ∀ a → Hom.map h a ≡ support′ a +MaxPlus→Loss h = pointwise + where + f = Hom.map h + + absorb : f (val 1) ≡ fin 0 ⊓g f (val 1) + absorb = trans (Hom.map-⊕ h (val 0) (val 1)) + (cong (λ z → z ⊓g f (val 1)) (Hom.map-𝟙 h)) + + one : (x : L.Grade) → f (val 1) ≡ x → f (val 1) ≡ fin 0 + one (fin c) e = trans absorb (cong (λ z → fin 0 ⊓g z) e) + one inf e with trans (sym e) (trans absorb (cong (λ z → fin 0 ⊓g z) e)) + ... | () + + val-fin0 : ∀ n → f (val n) ≡ fin 0 + val-fin0 zero = Hom.map-𝟙 h + val-fin0 (suc n) = + trans (Hom.map-⊗ h (val 1) (val n)) + (trans (cong (λ z → z +g f (val n)) (one (f (val 1)) refl)) + (cong (fin 0 +g_) (val-fin0 n))) + + pointwise : ∀ a → f a ≡ support′ a + pointwise (val n) = val-fin0 n + pointwise bot = Hom.map-𝟘 h + +---------------------------------------------------------------------- +-- Loss → MinMax: the identity on the carrier is lax +loss-bottleneck : LaxHom Loss MinMax +loss-bottleneck = record + { map = λ a → a ; map-𝟙 = refl ; map-⊕ = λ _ _ → refl ; map-⊗ = ⊗-case } + where + -- (a +g b) ≼ (a ⊔g b) in MinMax: the bottleneck is at most the sum. + ⊗-case : ∀ a b → (a +g b) ⊓g (a ⊔g b) ≡ a ⊔g b + ⊗-case (fin m) (fin n) = cong fin (min-≥ (max-≤-+ m n)) + ⊗-case (fin m) inf = refl + ⊗-case inf b = refl diff --git a/src/ResourceAlgebra/Prelude.agda b/src/ResourceAlgebra/Prelude.agda index 59b31dd..6cd0744 100644 --- a/src/ResourceAlgebra/Prelude.agda +++ b/src/ResourceAlgebra/Prelude.agda @@ -182,3 +182,67 @@ max-mono-≤ : ∀ {a a' b b'} → a ≤ a' → b ≤ b' → max a b ≤ max a' max-mono-≤ {a' = a'} z≤n q = ≤-trans q (≤-max-right a' _) max-mono-≤ {a' = a'} {b' = b'} (s≤s p) z≤n = ≤-trans (s≤s p) (≤-max-left a' b') max-mono-≤ (s≤s p) (s≤s q) = s≤s (max-mono-≤ p q) + +---------------------------------------------------------------------- +-- Disjoint sum (for the morphism classifications) +infixr 1 _⊎_ +data _⊎_ (A B : Set) : Set where + inj₁ : A → A ⊎ B + inj₂ : B → A ⊎ B + +---------------------------------------------------------------------- +-- More of the usual order, for the min-max instance and the morphisms +suc-injective : ∀ {m n} → suc m ≡ suc n → m ≡ n +suc-injective refl = refl + ++-cancelˡ : ∀ k {m n} → k + m ≡ k + n → m ≡ n ++-cancelˡ zero p = p ++-cancelˡ (suc k) p = +-cancelˡ k (suc-injective p) + +≤-+ʳ : ∀ m n → m ≤ m + n +≤-+ʳ zero n = z≤n +≤-+ʳ (suc m) n = s≤s (≤-+ʳ m n) + +≤-+ˡ : ∀ m n → n ≤ m + n +≤-+ˡ m n = subst (λ x → n ≤ x) (+-comm n m) (≤-+ʳ n m) + ++-monoˡ-≤ : ∀ {m n} p → m ≤ n → m + p ≤ n + p ++-monoˡ-≤ {m} {n} p q = + subst (λ x → x ≤ n + p) (+-comm p m) + (subst (λ y → p + m ≤ y) (+-comm p n) (+-monoʳ-≤ p q)) + +max-lub : ∀ {a b c} → a ≤ c → b ≤ c → max a b ≤ c +max-lub {zero} _ q = q +max-lub {suc a} {zero} p _ = p +max-lub {suc a} {suc b} (s≤s p) (s≤s q) = s≤s (max-lub p q) + +-- max m n is n once m ≤ n; min m n is m once m ≤ n. +max-≤ : ∀ {m n} → m ≤ n → max m n ≡ n +max-≤ z≤n = refl +max-≤ (s≤s p) = cong suc (max-≤ p) + +min-≤ : ∀ {m n} → m ≤ n → min m n ≡ m +min-≤ z≤n = refl +min-≤ (s≤s p) = cong suc (min-≤ p) + +min-≥ : ∀ {m n} → n ≤ m → min m n ≡ n +min-≥ {m} {n} p = trans (min-comm m n) (min-≤ p) + +-- A bottleneck never exceeds the sum: max m n ≤ m + n. +max-≤-+ : ∀ m n → max m n ≤ m + n +max-≤-+ m n = max-lub (≤-+ʳ m n) (≤-+ˡ m n) + +-- max distributes over min: the min-max instance is a dioid. +max-distribˡ-min : ∀ a b c → max a (min b c) ≡ min (max a b) (max a c) +max-distribˡ-min zero b c = refl +max-distribˡ-min (suc a) zero c = + sym (min-≤ (≤-max-left (suc a) c)) +max-distribˡ-min (suc a) (suc b) zero = + cong suc (sym (min-≥ (≤-max-left a b))) +max-distribˡ-min (suc a) (suc b) (suc c) = cong suc (max-distribˡ-min a b c) + +max-distribʳ-min : ∀ a b c → max (min a b) c ≡ min (max a c) (max b c) +max-distribʳ-min a b c = + trans (max-comm (min a b) c) + (trans (max-distribˡ-min c a b) + (cong₂ min (max-comm c a) (max-comm c b))) diff --git a/src/ResourceAlgebra/Separation.agda b/src/ResourceAlgebra/Separation.agda index 476d28b..16dfe48 100644 --- a/src/ResourceAlgebra/Separation.agda +++ b/src/ResourceAlgebra/Separation.agda @@ -2,15 +2,17 @@ -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -- --- Computed witnesses that the three instances are not interchangeable. +-- Computed witnesses that the four 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. They discharge, as checked --- facts, three boundary sentences the family map currently states only in +-- facts, four boundary sentences the family map currently states only in -- words: -- S-1 "an occupancy bound is not a cost bound" (nextgen-typing) -- S-2 "an informal loss number cannot stand in for the -- structure" — echo alternatives are MIN, tropical MAX (nextgen-typing) -- 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 module ResourceAlgebra.Separation where open import ResourceAlgebra.Prelude @@ -18,6 +20,7 @@ open import ResourceAlgebra.Core open import ResourceAlgebra.Instances.Loss as L open import ResourceAlgebra.Instances.MaxPlus as M open import ResourceAlgebra.Instances.HWM as H +open import ResourceAlgebra.Instances.MinMax as MM using (_⊔g_) ---------------------------------------------------------------------- -- S-1 Sequencing peaks 2 and 3 (nothing held between them): @@ -64,3 +67,20 @@ maxplus-order = refl loss-order-reversed : ResourceAlgebra._≼_ Loss (fin 2) (fin 1) loss-order-reversed = refl + +---------------------------------------------------------------------- +-- S-4 Same carrier, same alternatives, different sequence: Loss adds the +-- hops (2 then 3 costs 5), MinMax keeps the worst hop (3). A +-- bottleneck bound is not a loss bound, though it is below one +-- (Morphism.loss-bottleneck). +loss-seq : fin 2 +g fin 3 ≡ fin 5 +loss-seq = refl + +minmax-seq : fin 2 ⊔g fin 3 ≡ fin 3 +minmax-seq = refl + +bottleneck-is-not-sum : (fin 2 ⊔g fin 3) ≢ (fin 2 +g fin 3) +bottleneck-is-not-sum p = 3≢5 (fin-inj p) + where + fin-inj : ∀ {m n} → fin m ≡ fin n → m ≡ n + fin-inj refl = refl diff --git a/tests/reject/BottleneckBoundReversed.agda b/tests/reject/BottleneckBoundReversed.agda new file mode 100644 index 0000000..cddf890 --- /dev/null +++ b/tests/reject/BottleneckBoundReversed.agda @@ -0,0 +1,15 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +module BottleneckBoundReversed where +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Core +open import ResourceAlgebra.Instances.Loss using (fin) +open import ResourceAlgebra.Instances.MinMax using (MinMax) + +-- Must fail: the Loss → MinMax lax bound is 5 ≼ 3, since the induced +-- order reverses the numeric order. Reversing it would validate a bound +-- that the bottleneck map does not provide. +-- EXPECT: 3 != 5 of type Nat +invalid : ResourceAlgebra._≼_ MinMax (fin 3) (fin 5) +invalid = refl diff --git a/tests/reject/DriftExceedsPeak.agda b/tests/reject/DriftExceedsPeak.agda index 8f24d0a..de88a36 100644 --- a/tests/reject/DriftExceedsPeak.agda +++ b/tests/reject/DriftExceedsPeak.agda @@ -7,5 +7,6 @@ open import ResourceAlgebra.Instances.HWM -- Must fail: 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: suc .* != zero of type Nat invalid : Grade invalid = hwm 1 2 (s≤s (s≤s z≤n)) diff --git a/tests/reject/HWMAnnihilates.agda b/tests/reject/HWMAnnihilates.agda index 04696d8..e1cd00d 100644 --- a/tests/reject/HWMAnnihilates.agda +++ b/tests/reject/HWMAnnihilates.agda @@ -9,5 +9,6 @@ open import ResourceAlgebra.Instances.HWM -- Must fail: in the high-water-mark algebra the ⊕-unit is also the -- ⊗-unit, so sequencing with it returns the other grade, not 𝟘. Accepting -- this would smuggle an annihilating zero into an algebra that has none. +-- EXPECT: p != zero of type Nat invalid : ∀ g → (𝟘h ⊗h g) ≡ 𝟘h invalid (hwm p n b) = refl diff --git a/tests/reject/LossWorstCase.agda b/tests/reject/LossWorstCase.agda index 6c13d7f..0f8e59a 100644 --- a/tests/reject/LossWorstCase.agda +++ b/tests/reject/LossWorstCase.agda @@ -9,5 +9,6 @@ open import ResourceAlgebra.Instances.Loss -- Must fail: 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 — the "informal loss number" the family map forbids. +-- EXPECT: min m n != max m n of type Nat invalid : ∀ m n → (fin m ⊓g fin n) ≡ fin (max m n) invalid m n = refl diff --git a/tests/reject/MinMaxInfinityIsIdentity.agda b/tests/reject/MinMaxInfinityIsIdentity.agda new file mode 100644 index 0000000..0f259b6 --- /dev/null +++ b/tests/reject/MinMaxInfinityIsIdentity.agda @@ -0,0 +1,13 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +module MinMaxInfinityIsIdentity where +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Instances.Loss using (fin; inf) +open import ResourceAlgebra.Instances.MinMax using (_⊔g_) + +-- Must fail: an unreachable sequential hop absorbs, even though infinity +-- is the identity for alternatives on the same carrier. +-- EXPECT: inf != fin 3 of type +invalid : inf ⊔g fin 3 ≡ fin 3 +invalid = refl diff --git a/tests/reject/MinMaxIsLoss.agda b/tests/reject/MinMaxIsLoss.agda new file mode 100644 index 0000000..720a9a8 --- /dev/null +++ b/tests/reject/MinMaxIsLoss.agda @@ -0,0 +1,15 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +module MinMaxIsLoss where +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Instances.Loss using (fin) +open import ResourceAlgebra.Instances.MinMax + +-- Must fail: the bottleneck sequence keeps the worst hop; it does not add +-- the hops. Accepting this would let a min-max bound be read as a +-- min-plus (loss) bound, which is the identification Separation S-4 and +-- the lax (not strict) loss-bottleneck morphism exist to forbid. +-- EXPECT: max m n != m \+ n of type Nat +invalid : ∀ m n → (fin m ⊔g fin n) ≡ fin (m + n) +invalid m n = refl diff --git a/tests/reject/PeakIsStrict.agda b/tests/reject/PeakIsStrict.agda new file mode 100644 index 0000000..84fab46 --- /dev/null +++ b/tests/reject/PeakIsStrict.agda @@ -0,0 +1,15 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +module PeakIsStrict where +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Instances.HWM +open import ResourceAlgebra.Instances.MaxPlus using (val; tMul) + +-- Must fail: the peak of a sequence is max (peak a) (drift a + peak b), +-- not peak a + peak b. Peak is only a LAX morphism HWM → MaxPlus +-- (Morphism.peak-lax: occupancy never exceeds cost); accepting this would +-- make it strict and let an occupancy bound stand in for a cost bound. +-- EXPECT: max p₁ \(n₁ \+ p₂\) != p₁ \+ p₂ of type Nat +invalid : ∀ a b → val (peak (a ⊗h b)) ≡ tMul (val (peak a)) (val (peak b)) +invalid (hwm p₁ n₁ b₁) (hwm p₂ n₂ b₂) = refl diff --git a/tests/reject/PeakPreservesZero.agda b/tests/reject/PeakPreservesZero.agda new file mode 100644 index 0000000..3ae0700 --- /dev/null +++ b/tests/reject/PeakPreservesZero.agda @@ -0,0 +1,15 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +module PeakPreservesZero where +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Core +open import ResourceAlgebra.Instances.HWM using (HWM) +open import ResourceAlgebra.Instances.MaxPlus using (MaxPlus) +open import ResourceAlgebra.Morphism using (LaxHom; peak-lax) + +-- Must fail: LaxHom only provides a bound for zero, not strict zero +-- preservation. The zero HWM grade maps to val 0, not MaxPlus's bot. +-- EXPECT: != ResourceAlgebra\.Instances\.MaxPlus\.bot of type +invalid : LaxHom.map peak-lax (ResourceAlgebra.𝟘 HWM) ≡ ResourceAlgebra.𝟘 MaxPlus +invalid = refl diff --git a/tests/unit/AllTests.agda b/tests/unit/AllTests.agda new file mode 100644 index 0000000..18e9084 --- /dev/null +++ b/tests/unit/AllTests.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +module AllTests where + +import MinMaxTest +import MorphismTest +import PreludeTest diff --git a/tests/unit/MinMaxTest.agda b/tests/unit/MinMaxTest.agda new file mode 100644 index 0000000..b337cbc --- /dev/null +++ b/tests/unit/MinMaxTest.agda @@ -0,0 +1,123 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +module MinMaxTest where + +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Core +open import ResourceAlgebra.Instances.Loss using (fin; inf; _+g_) +open import ResourceAlgebra.Instances.MinMax +import ResourceAlgebra.Separation as S + +module MM = ResourceAlgebra MinMax + +-- Use the public record as well as the sequence operator: the record's +-- choice of units and operations is part of the consumer contract. +zero-is-unreachable : MM.𝟘 ≡ inf +zero-is-unreachable = refl + +one-is-no-cost : MM.𝟙 ≡ fin 0 +one-is-no-cost = refl + +alternative-chooses-smaller : fin 2 MM.⊕ fin 7 ≡ fin 2 +alternative-chooses-smaller = refl + +alternative-chooses-smaller-reversed : fin 7 MM.⊕ fin 2 ≡ fin 2 +alternative-chooses-smaller-reversed = refl + +unreachable-alternative-left : ∀ n → inf MM.⊕ fin n ≡ fin n +unreachable-alternative-left n = refl + +unreachable-alternative-right : ∀ n → fin n MM.⊕ inf ≡ fin n +unreachable-alternative-right n = refl + +both-alternatives-unreachable : inf MM.⊕ inf ≡ inf +both-alternatives-unreachable = refl + +sequence-chooses-larger : fin 2 MM.⊗ fin 7 ≡ fin 7 +sequence-chooses-larger = refl + +sequence-chooses-larger-reversed : fin 7 MM.⊗ fin 2 ≡ fin 7 +sequence-chooses-larger-reversed = refl + +repeated-hop-does-not-accumulate : fin 4 MM.⊗ fin 4 ≡ fin 4 +repeated-hop-does-not-accumulate = refl + +zero-hop-left : ∀ n → fin 0 ⊔g fin n ≡ fin n +zero-hop-left n = refl + +zero-hop-right : ∀ n → fin n ⊔g fin 0 ≡ fin n +zero-hop-right n = cong fin (max-zeroʳ n) + +unreachable-hop-left : ∀ n → inf ⊔g fin n ≡ inf +unreachable-hop-left n = refl + +unreachable-hop-right : ∀ n → fin n ⊔g inf ≡ inf +unreachable-hop-right n = refl + +both-hops-unreachable : inf ⊔g inf ≡ inf +both-hops-unreachable = refl + +unreachable-after-no-cost : fin 0 MM.⊗ inf ≡ inf +unreachable-after-no-cost = refl + +no-cost-after-unreachable : inf MM.⊗ fin 0 ≡ inf +no-cost-after-unreachable = refl + +three-hop-bottleneck : (fin 2 MM.⊗ fin 7) MM.⊗ fin 3 ≡ fin 7 +three-hop-bottleneck = refl + +unreachable-middle-hop : (fin 2 MM.⊗ inf) MM.⊗ fin 3 ≡ inf +unreachable-middle-hop = refl + +-- Exercise both distribution laws through the exported dioid layer. +distribute-left-with-unreachable : + fin 4 MM.⊗ (inf MM.⊕ fin 2) ≡ + (fin 4 MM.⊗ inf) MM.⊕ (fin 4 MM.⊗ fin 2) +distribute-left-with-unreachable = IsDioid.distribˡ MinMax-dioid (fin 4) inf (fin 2) + +distribute-right-with-unreachable : + (fin 2 MM.⊕ inf) MM.⊗ fin 4 ≡ + (fin 2 MM.⊗ fin 4) MM.⊕ (inf MM.⊗ fin 4) +distribute-right-with-unreachable = IsDioid.distribʳ MinMax-dioid (fin 2) inf (fin 4) + +choice-between-bottlenecks : + (fin 4 MM.⊗ fin 2) MM.⊕ (fin 4 MM.⊗ fin 7) ≡ fin 4 +choice-between-bottlenecks = refl + +annihilate-left : inf MM.⊗ fin 0 ≡ inf +annihilate-left = IsAnnihilating.annihilˡ MinMax-annihilating (fin 0) + +annihilate-right : fin 0 MM.⊗ inf ≡ inf +annihilate-right = IsAnnihilating.annihilʳ MinMax-annihilating (fin 0) + +-- The induced order reverses the usual numeric order, including infinity. +smaller-bottleneck-is-above : fin 7 MM.≼ fin 2 +smaller-bottleneck-is-above = refl + +unreachable-is-least : inf MM.≼ fin 0 +unreachable-is-least = refl + +sequence-monotone-left : (fin 4 MM.⊗ fin 7) MM.≼ (fin 4 MM.⊗ fin 2) +sequence-monotone-left = IsOrdered.⊗-monoˡ MinMax-ordered (fin 4) + {a = fin 7} {b = fin 2} refl + +sequence-monotone-right : (inf MM.⊗ fin 4) MM.≼ (fin 2 MM.⊗ fin 4) +sequence-monotone-right = IsOrdered.⊗-monoʳ MinMax-ordered (fin 4) + {a = inf} {b = fin 2} refl + +-- S-4's public witnesses, and a new boundary where adding repeats a hop. +separation-loss-result : fin 2 +g fin 3 ≡ fin 5 +separation-loss-result = S.loss-seq + +separation-bottleneck-result : fin 2 ⊔g fin 3 ≡ fin 3 +separation-bottleneck-result = S.minmax-seq + +separation-witness : fin 2 ⊔g fin 3 ≢ fin 2 +g fin 3 +separation-witness = S.bottleneck-is-not-sum + +repeated-hop-is-not-a-sum : fin 4 ⊔g fin 4 ≢ fin 4 +g fin 4 +repeated-hop-is-not-a-sum () + +numeric-order-is-not-induced-order : ¬ (fin 2 MM.≼ fin 7) +numeric-order-is-not-induced-order () diff --git a/tests/unit/MorphismTest.agda b/tests/unit/MorphismTest.agda new file mode 100644 index 0000000..ba1ccda --- /dev/null +++ b/tests/unit/MorphismTest.agda @@ -0,0 +1,252 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +module MorphismTest where + +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Core +open import ResourceAlgebra.Morphism +open import ResourceAlgebra.Instances.Loss as L using (Loss; fin; inf) +open import ResourceAlgebra.Instances.MaxPlus using (MaxPlus; val; bot) +open import ResourceAlgebra.Instances.HWM as H using (HWM; hwm; 𝟘h; _⊗h_; _⊕h_) +open import ResourceAlgebra.Instances.MinMax using (MinMax) + +module MP = ResourceAlgebra MaxPlus +module MM = ResourceAlgebra MinMax + +-- The two Loss maps agree at zero and infinity, but disagree at EVERY +-- positive finite grade. Test the functions via their exported records. +zero-test-at-zero : Hom.map zero-test-hom (fin 0) ≡ val 0 +zero-test-at-zero = refl + +zero-test-at-positive : ∀ n → Hom.map zero-test-hom (fin (suc n)) ≡ bot +zero-test-at-positive n = refl + +zero-test-at-infinity : Hom.map zero-test-hom inf ≡ bot +zero-test-at-infinity = refl + +support-at-finite : ∀ n → Hom.map support-hom (fin n) ≡ val 0 +support-at-finite n = refl + +support-at-infinity : Hom.map support-hom inf ≡ bot +support-at-infinity = refl + +maps-disagree-at-positive : ∀ n → zero-test (fin (suc n)) ≢ support (fin (suc n)) +maps-disagree-at-positive n () + +reverse-support-at-finite : ∀ n → Hom.map support′-hom (val n) ≡ fin 0 +reverse-support-at-finite n = refl + +reverse-support-at-bottom : Hom.map support′-hom bot ≡ inf +reverse-support-at-bottom = refl + +-- The new classifiers compute the correct branch, including on maps +-- built by composition rather than just their canonical inhabitants. +branch : {A B : Set} → A ⊎ B → Nat +branch (inj₁ _) = 0 +branch (inj₂ _) = 1 + +classify-zero-test : branch (Loss→MaxPlus zero-test-hom) ≡ 0 +classify-zero-test = refl + +classify-support : branch (Loss→MaxPlus support-hom) ≡ 1 +classify-support = refl + +classify-composed-support : + branch (Loss→MaxPlus (zero-test-hom ∘h support′-hom ∘h support-hom)) ≡ 1 +classify-composed-support = refl + +unique-reverse-map-finite : ∀ n → Hom.map support′-hom (val n) ≡ fin 0 +unique-reverse-map-finite n = MaxPlus→Loss support′-hom (val n) + +unique-reverse-map-bottom : Hom.map support′-hom bot ≡ inf +unique-reverse-map-bottom = MaxPlus→Loss support′-hom bot + +zero-test-collapses-witnesses : + Hom.map zero-test-hom (fin 1) ≡ Hom.map zero-test-hom (fin 2) +zero-test-collapses-witnesses = Loss→MaxPlus-collapses zero-test-hom + +support-collapses-witnesses : + Hom.map support-hom (fin 1) ≡ Hom.map support-hom (fin 2) +support-collapses-witnesses = Loss→MaxPlus-collapses support-hom + +-- A client cannot recover distinct positive grades through either map. +cannot-recover-positive-loss : (h : Hom Loss MaxPlus) + → (∀ a b → Hom.map h a ≡ Hom.map h b → a ≡ b) → ⊥ +cannot-recover-positive-loss = no-injective-Loss→MaxPlus + +strict-round-trip-zero : Hom.map (support′-hom ∘h zero-test-hom) (fin 0) ≡ fin 0 +strict-round-trip-zero = refl + +strict-round-trip-positive : + Hom.map (support′-hom ∘h zero-test-hom) (fin 3) ≡ inf +strict-round-trip-positive = refl + +support-round-trip-positive : + Hom.map (support′-hom ∘h support-hom) (fin 3) ≡ fin 0 +support-round-trip-positive = refl + +strict-round-trip-infinity : Hom.map (support′-hom ∘h zero-test-hom) inf ≡ inf +strict-round-trip-infinity = refl + +reverse-round-trip-positive : + Hom.map (zero-test-hom ∘h support′-hom) (val 3) ≡ val 0 +reverse-round-trip-positive = refl + +reverse-round-trip-bottom : Hom.map (zero-test-hom ∘h support′-hom) bot ≡ bot +reverse-round-trip-bottom = refl + +-- Pointwise category laws avoid function extensionality and test every +-- grade, including the sentinel grades, of every compatible algebra. +strict-identity : (A : ResourceAlgebra) (a : ResourceAlgebra.Grade A) + → Hom.map (id-hom A) a ≡ a +strict-identity A a = refl + +strict-left-identity : {A B : ResourceAlgebra} (h : Hom A B) + (a : ResourceAlgebra.Grade A) → Hom.map (id-hom B ∘h h) a ≡ Hom.map h a +strict-left-identity h a = refl + +strict-right-identity : {A B : ResourceAlgebra} (h : Hom A B) + (a : ResourceAlgebra.Grade A) → Hom.map (h ∘h id-hom A) a ≡ Hom.map h a +strict-right-identity h a = refl + +strict-associativity : {A B C D : ResourceAlgebra} + (f : Hom A B) (g : Hom B C) (h : Hom C D) (a : ResourceAlgebra.Grade A) + → Hom.map ((h ∘h g) ∘h f) a ≡ Hom.map (h ∘h (g ∘h f)) a +strict-associativity f g h a = refl + +lax-identity : (A : ResourceAlgebra) (a : ResourceAlgebra.Grade A) + → LaxHom.map (id-lax A) a ≡ a +lax-identity A a = refl + +lax-left-identity : {A B : ResourceAlgebra} (h : LaxHom A B) + (a : ResourceAlgebra.Grade A) → LaxHom.map (id-lax B ∘l h) a ≡ LaxHom.map h a +lax-left-identity h a = refl + +lax-right-identity : {A B : ResourceAlgebra} (h : LaxHom A B) + (a : ResourceAlgebra.Grade A) → LaxHom.map (h ∘l id-lax A) a ≡ LaxHom.map h a +lax-right-identity h a = refl + +lax-associativity : {A B C D : ResourceAlgebra} + (f : LaxHom A B) (g : LaxHom B C) (h : LaxHom C D) (a : ResourceAlgebra.Grade A) + → LaxHom.map ((h ∘l g) ∘l f) a ≡ LaxHom.map (h ∘l (g ∘l f)) a +lax-associativity f g h a = refl + +strict-to-lax-keeps-map : (A B : ResourceAlgebra) (h : Hom A B) + (a : ResourceAlgebra.Grade A) → LaxHom.map (lax A B h) a ≡ Hom.map h a +strict-to-lax-keeps-map A B h a = refl + +-- Multiplication and monotonicity of a converted non-identity map. +converted-zero-test-sequence : + LaxHom.map (lax Loss MaxPlus zero-test-hom) (fin 3) MP.≼ bot +converted-zero-test-sequence = + LaxHom.map-⊗ (lax Loss MaxPlus zero-test-hom) (fin 1) (fin 2) + +converted-support-monotone : val 0 MP.≼ val 0 +converted-support-monotone = LaxHom.mono (lax Loss MaxPlus support-hom) + {a = fin 7} {b = fin 2} refl + +-- Peaks need not preserve zero. Released state yields a strict bound; +-- retaining the full peak makes the bound an equality. +released-two released-three retained-two partial-four : H.Grade +released-two = hwm 2 0 z≤n +released-three = hwm 3 0 z≤n +retained-two = hwm 2 2 (≤-refl 2) +partial-four = hwm 4 1 (s≤s z≤n) + +peak-of-zero : LaxHom.map peak-lax 𝟘h ≡ val 0 +peak-of-zero = refl + +peak-zero-is-not-bottom : LaxHom.map peak-lax 𝟘h ≢ bot +peak-zero-is-not-bottom () + +peak-zero-bound : bot MP.≼ LaxHom.map peak-lax 𝟘h +peak-zero-bound = LaxHom.map-𝟘 peak-lax + +peak-ignores-drift : LaxHom.map peak-lax retained-two ≡ val 2 +peak-ignores-drift = refl + +peak-of-alternatives : LaxHom.map peak-lax (released-two ⊕h released-three) ≡ val 3 +peak-of-alternatives = refl + +released-sequence-peak : + LaxHom.map peak-lax (released-two ⊗h released-three) ≡ val 3 +released-sequence-peak = refl + +released-sequence-bound : val 3 MP.≼ val 5 +released-sequence-bound = LaxHom.map-⊗ peak-lax released-two released-three + +retained-sequence-peak : + LaxHom.map peak-lax (retained-two ⊗h released-three) ≡ val 5 +retained-sequence-peak = refl + +retained-sequence-tight-bound : val 5 MP.≼ val 5 +retained-sequence-tight-bound = LaxHom.map-⊗ peak-lax retained-two released-three + +first-peak-dominates : LaxHom.map peak-lax (partial-four ⊗h released-two) ≡ val 4 +first-peak-dominates = refl + +peak-is-monotone : val 2 MP.≼ val 3 +peak-is-monotone = LaxHom.mono peak-lax + {a = released-two} {b = released-three} (H.hwm-≡ refl refl) + +-- HWM's equal units rule out strict maps even to the new MinMax instance. +no-strict-HWM-to-MinMax : Hom HWM MinMax → ⊥ +no-strict-HWM-to-MinMax = no-strict-from-HWM MinMax (λ ()) + +-- The bottleneck map preserves all grades but weakens an additive bound +-- in the REVERSED order induced by min. Infinity must remain unreachable. +bottleneck-keeps-finite : ∀ n → LaxHom.map loss-bottleneck (fin n) ≡ fin n +bottleneck-keeps-finite n = refl + +bottleneck-keeps-infinity : LaxHom.map loss-bottleneck inf ≡ inf +bottleneck-keeps-infinity = refl + +bottleneck-positive-bound : fin 5 MM.≼ fin 3 +bottleneck-positive-bound = LaxHom.map-⊗ loss-bottleneck (fin 2) (fin 3) + +bottleneck-zero-bound : fin 3 MM.≼ fin 3 +bottleneck-zero-bound = LaxHom.map-⊗ loss-bottleneck (fin 0) (fin 3) + +bottleneck-infinite-left-bound : inf MM.≼ inf +bottleneck-infinite-left-bound = LaxHom.map-⊗ loss-bottleneck inf (fin 3) + +bottleneck-infinite-right-bound : inf MM.≼ inf +bottleneck-infinite-right-bound = LaxHom.map-⊗ loss-bottleneck (fin 3) inf + +bottleneck-both-infinite-bound : inf MM.≼ inf +bottleneck-both-infinite-bound = LaxHom.map-⊗ loss-bottleneck inf inf + +bottleneck-monotone : fin 7 MM.≼ fin 2 +bottleneck-monotone = LaxHom.mono loss-bottleneck {a = fin 7} {b = fin 2} refl + +bottleneck-zero-bound-is-least : inf MM.≼ inf +bottleneck-zero-bound-is-least = LaxHom.map-𝟘 loss-bottleneck + +-- Composition must retain a strict inequality when it passes through an +-- identity, including the reversed inequality in the MinMax target. +composed-peak-keeps-loose-bound : val 3 MP.≼ val 5 +composed-peak-keeps-loose-bound = + LaxHom.map-⊗ (id-lax MaxPlus ∘l peak-lax) released-two released-three + +composed-bottleneck-keeps-loose-bound : fin 5 MM.≼ fin 3 +composed-bottleneck-keeps-loose-bound = + LaxHom.map-⊗ (id-lax MinMax ∘l loss-bottleneck) (fin 2) (fin 3) + +-- A genuinely lax composition crosses three instances. This also tests +-- that strict-to-lax conversion interoperates with both lax maps. +peak-bottleneck : LaxHom HWM MinMax +peak-bottleneck = loss-bottleneck ∘l lax MaxPlus Loss support′-hom ∘l peak-lax + +composed-lax-map : LaxHom.map peak-bottleneck retained-two ≡ fin 0 +composed-lax-map = refl + +composed-lax-unit : LaxHom.map peak-bottleneck 𝟘h ≡ fin 0 +composed-lax-unit = LaxHom.map-𝟙 peak-bottleneck + +composed-lax-sequence : fin 0 MM.≼ fin 0 +composed-lax-sequence = LaxHom.map-⊗ peak-bottleneck released-two released-three + +composed-lax-monotone : fin 0 MM.≼ fin 0 +composed-lax-monotone = LaxHom.mono peak-bottleneck + {a = released-two} {b = released-three} (H.hwm-≡ refl refl) diff --git a/tests/unit/PreludeTest.agda b/tests/unit/PreludeTest.agda new file mode 100644 index 0000000..443f020 --- /dev/null +++ b/tests/unit/PreludeTest.agda @@ -0,0 +1,90 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +module PreludeTest where + +open import ResourceAlgebra.Prelude + +-- Concrete clients of the new lemmas cover zero, equal bounds, strict +-- bounds, and the recursive positive cases without a standard library. +cancel-zero-prefix : ∀ {m n} → 0 + m ≡ 0 + n → m ≡ n +cancel-zero-prefix = +-cancelˡ 0 + +cancel-positive-prefix : ∀ {m n} → 3 + m ≡ 3 + n → m ≡ n +cancel-positive-prefix = +-cancelˡ 3 + +cancel-successor : ∀ {m n} → suc m ≡ suc n → m ≡ n +cancel-successor = suc-injective + +left-summand-zero : 0 ≤ 0 + 5 +left-summand-zero = ≤-+ʳ 0 5 + +left-summand-positive : 3 ≤ 3 + 2 +left-summand-positive = ≤-+ʳ 3 2 + +right-summand-zero : 5 ≤ 0 + 5 +right-summand-zero = ≤-+ˡ 0 5 + +right-summand-positive : 5 ≤ 3 + 5 +right-summand-positive = ≤-+ˡ 3 5 + +adding-preserves-strict-bound : 2 + 3 ≤ 5 + 3 +adding-preserves-strict-bound = +-monoˡ-≤ {m = 2} {n = 5} 3 (s≤s (s≤s z≤n)) + +adding-zero-preserves-equal-bound : 3 + 0 ≤ 3 + 0 +adding-zero-preserves-equal-bound = +-monoˡ-≤ {m = 3} {n = 3} 0 (≤-refl 3) + +max-bound-left-zero : max 0 3 ≤ 5 +max-bound-left-zero = max-lub z≤n (s≤s (s≤s (s≤s z≤n))) + +max-bound-right-zero : max 3 0 ≤ 5 +max-bound-right-zero = max-lub (s≤s (s≤s (s≤s z≤n))) z≤n + +max-bound-positive : max 2 3 ≤ 4 +max-bound-positive = max-lub (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) + +max-of-zero-and-positive : max 0 5 ≡ 5 +max-of-zero-and-positive = max-≤ z≤n + +max-at-equal-bound : max 3 3 ≡ 3 +max-at-equal-bound = max-≤ (≤-refl 3) + +max-at-strict-bound : max 2 5 ≡ 5 +max-at-strict-bound = max-≤ (s≤s (s≤s z≤n)) + +min-at-zero-bound : min 0 5 ≡ 0 +min-at-zero-bound = min-≤ {m = 0} {n = 5} z≤n + +min-at-strict-bound : min 2 5 ≡ 2 +min-at-strict-bound = min-≤ {m = 2} {n = 5} (s≤s (s≤s z≤n)) + +min-at-reversed-bound : min 5 2 ≡ 2 +min-at-reversed-bound = min-≥ {m = 5} {n = 2} (s≤s (s≤s z≤n)) + +bottleneck-bound-zero-left : max 0 5 ≤ 0 + 5 +bottleneck-bound-zero-left = max-≤-+ 0 5 + +bottleneck-bound-zero-right : max 5 0 ≤ 5 + 0 +bottleneck-bound-zero-right = max-≤-+ 5 0 + +bottleneck-bound-positive : max 2 3 ≤ 2 + 3 +bottleneck-bound-positive = max-≤-+ 2 3 + +-- Each base case and the recursive case of the new distributivity lemma. +distribute-zero-sequence : max 0 (min 2 5) ≡ min (max 0 2) (max 0 5) +distribute-zero-sequence = max-distribˡ-min 0 2 5 + +distribute-zero-first-choice : max 3 (min 0 5) ≡ min (max 3 0) (max 3 5) +distribute-zero-first-choice = max-distribˡ-min 3 0 5 + +distribute-zero-second-choice : max 3 (min 5 0) ≡ min (max 3 5) (max 3 0) +distribute-zero-second-choice = max-distribˡ-min 3 5 0 + +distribute-positive-choices : max 3 (min 2 5) ≡ min (max 3 2) (max 3 5) +distribute-positive-choices = max-distribˡ-min 3 2 5 + +distribute-right-positive-choices : max (min 2 5) 3 ≡ min (max 2 3) (max 5 3) +distribute-right-positive-choices = max-distribʳ-min 2 5 3 + +distribute-right-zero-choice : max (min 5 0) 3 ≡ min (max 5 3) (max 0 3) +distribute-right-zero-choice = max-distribʳ-min 5 0 3 diff --git a/tests/unit/resource_algebra_test.sh b/tests/unit/resource_algebra_test.sh new file mode 100644 index 0000000..a28b431 --- /dev/null +++ b/tests/unit/resource_algebra_test.sh @@ -0,0 +1,17 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# Run from any directory: bash tests/unit/resource_algebra_test.sh +# Mirrors scripts/check-agda.sh's proof flags and honors its AGDA override. +set -euo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../.." +export LC_ALL="${LC_ALL:-C.UTF-8}" +prover="${AGDA:-agda}" +"$prover" --version +"$prover" --safe --without-K --no-libraries --ignore-interfaces --double-check \ + -i src -i tests/unit tests/unit/AllTests.agda +echo 'PASS: MinMax, morphism, and Prelude unit tests' + +# Keep the expected failures in the existing harness, which verifies that +# they fail at their declarations rather than at parsing/import resolution. +bash scripts/check-agda.sh