diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc new file mode 100644 index 0000000..1c0a7a6 --- /dev/null +++ b/ARCHITECTURE.adoc @@ -0,0 +1,48 @@ +== Architecture + +=== Overview + +This repository follows a modular, maintainable architecture designed +for clarity, scalability, and long-term sustainability. + +=== Directory Structure + +.... +. +├── src/ # Source code +├── tests/ # Test suites +├── docs/ # Documentation +├── scripts/ # Utility scripts +├── config/ # Configuration files +├── LICENSE # License file +├── LICENSES/ # Full license texts +└── README.adoc # Project documentation +.... + +=== Design Principles + +* *Separation of Concerns*: Each module has a single responsibility +* *Testability*: Code is written to be easily testable +* *Documentation*: All public APIs are documented +* *Configuration*: Environment-specific settings are externalized + +=== Dependencies + +* External dependencies are minimized and clearly declared +* Version pinning is used for reproducibility + +=== Security Considerations + +* Sensitive data is never committed to the repository +* Secrets are managed through environment variables or secure vaults +* Regular dependency audits are performed + +=== Maintainability + +* Code follows consistent style guidelines +* Pull requests require review and CI checks +* Issues and discussions are tracked transparently + +''''' + +_Last updated: 2026-07-18_ diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md deleted file mode 100644 index 607e3d8..0000000 --- a/ARCHITECTURE.md +++ /dev/null @@ -1,47 +0,0 @@ -# Architecture - -## Overview - -This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability. - -## Directory Structure - -``` -. -├── src/ # Source code -├── tests/ # Test suites -├── docs/ # Documentation -├── scripts/ # Utility scripts -├── config/ # Configuration files -├── LICENSE # License file -├── LICENSES/ # Full license texts -└── README.adoc # Project documentation -``` - -## Design Principles - -- **Separation of Concerns**: Each module has a single responsibility -- **Testability**: Code is written to be easily testable -- **Documentation**: All public APIs are documented -- **Configuration**: Environment-specific settings are externalized - -## Dependencies - -- External dependencies are minimized and clearly declared -- Version pinning is used for reproducibility - -## Security Considerations - -- Sensitive data is never committed to the repository -- Secrets are managed through environment variables or secure vaults -- Regular dependency audits are performed - -## Maintainability - -- Code follows consistent style guidelines -- Pull requests require review and CI checks -- Issues and discussions are tracked transparently - ---- - -*Last updated: 2026-07-18* diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc new file mode 100644 index 0000000..c196a4c --- /dev/null +++ b/CHANGELOG.adoc @@ -0,0 +1,133 @@ +== Changelog + +All notable changes to `+tropical-resource-typing+` will be documented +in this file. + +This file is generated from conventional commits by the +https://github.com/hyperpolymath/standards/blob/main/.github/workflows/changelog-reusable.yml[`+changelog-reusable.yml+`] +workflow (`+hyperpolymath/standards#206+`). Adopt the workflow in this +repo’s CI to keep this file in sync automatically — see +https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml[`+templates/cliff.toml+`] +for the canonical config. + +The format follows https://keepachangelog.com/en/1.1.0/[Keep a +Changelog]; this project aims to follow +https://semver.org/spec/v2.0.0.html[Semantic Versioning]. + +=== [Unreleased] + +==== Added + +* feat(lean4): bridge the two original twins onto the resource-grade +axis (`+Resource.Bridge+`) — max-plus session grading shown +resource-algebra-structured (`+grade_spec_par = ⊞+`, +`+grade_send = val 1 ⊠ ·+`) with the QTT refinement restated in the +resource order (`+grade_le_sequential+`); the bounded bottleneck algebra +embedded into `+Resource.Instances.MinMax+`, with +`+embed_tcZero_ne_zero+` exposing the finite-`+∞+` approximation and +`+hub_ceiling_le+` restating `+hub_ceiling+` in `+⊑+`. Closes the +standing "`construct a functor / state the QTT quotient morphism`" open +items +* feat(lean4): add the *resource-grade axis* — `+Resource.*+` library +exporting a reusable resource-algebra interface (`+ResourceSemiring+` + +ordered `+ResourceAlgebra+`, no Mathlib), the canonical dioid-order +builder, concrete instances (Linear/Affine `+{0,1,ω}+`, MaxPlus, +MinPlus, MinMax), and the parametric transport theorem +`+parametric_resource_transport+` (alias +`+resource_laws_sufficient_for_consumers+`) over `+ConsumerLawBundle+`; +aggregator `+Resource.lean+`; `+lake build+` green, new theorems depend +only on propext/Quot.sound (or nothing) +* feat(lean4): prove tropical carriers are infinite +(`+Resource.Stress+`: `+infinite_maxPlus/minPlus/minMax+`) — the +infinite-carrier stress test that the abstraction is not a finite +`+{0,1,ω}+` reification +* feat(lean4): add `+Resource.EchoBridge+` — abstract `+ResidueMeasure+` +showing a resource algebra may measure (opaque) Echo residues, direction +`+E → R+`, with a compiling max-plus witness; no `+echo-types+` +dependency +* docs: add `+FOUNDATION_CONTRACT.md+`, `+docs/RESOURCE-ALGEBRA.adoc+`, +`+docs/ECHO-RESIDUE-BRIDGE.adoc+` (resource grade vs resource algebra vs +tropical instance vs residue measure; the "`tropical is not Echo`" +boundary invariant) +* ci(lean4): extend `+lean.yml+` axiom audit to the new `+Resource.*+` +headline theorems and instances +* feat(lean4): migrate the min-max transport semiring +(TropicalAdapterPath) in beside the max-plus twin; pin Lean 4.13.0 via +lean-toolchain; add lakefile + lake-manifest; `+lake build+` green +* feat(lean4): prove the De Morgan duality bridge — dualGrade_invol, +dual_tcAdd_is_max (dual of min = max), dual_tcMul_is_min (dual of max = +min) +* docs(lean4): add docs/LEAN-FORMALIZATION.adoc (authoritative Lean +reference: build/verify recipe, theorem index, axiom audit, provenance) ++ README section +* ci(lean4): add lean.yml — lake build + axiom audit (propext/Quot.sound +only, no sorry) on push/PR +* feat(isabelle): close all sorries in Tropical_Kleene and +Tropical_Matrices_Clean +* feat(isabelle): close all sorries in Tropical_CNO.thy +* feat(determinants): add Tropical_Determinants.thy — optimal assignment +theorem +* feat(isabelle): close bellman_ford OFFICIAL SORRY 2 — min-plus +Bellman-Ford proved +* feat(isabelle): extend Tropical_Matrices_Full.thy +* feat(afp): create AFP submission files for Tropical_Semirings +* feat(isabelle): recover Tropical_Matrices_Full, Kleene, CNO, and Clean +* feat(isabelle,lean4): recover Tropical_v2.thy and +TropicalSessionTypes.lean v6.0 +* feat(lean4): add tropical session types formalisation +* feat(isabelle): add verified tropical semiring formalisation + +==== Fixed + +* fix(lean4): repair TropicalSessionTypes + TropicalAdapterPath to +compile clean under core Lean 4.13.0 — import ordering, Mathlib-only +`+push_neg+`→core tactics, `+AdapterPath+` def→abbrev, local `+One+` +shim (4.13.0 core lacks One), +`+pathCost_append+`/`+pathCost_le_sequential+` reproved; the inherited +"`Verified`" headers were never true +* fix(lean4): replace the FALSE `+dual_tcMul_bounded+` +(`+dual(max m n)=dual m+dual n−maxGrade+`, wrong at m=1,n=2) with the +correct De Morgan dual `+dual_tcMul_is_min+` +* fix(ci): sync hypatia-scan.yml to canonical (413: +env.HOME+Phase-2+SARIF) (#1) +* fix(Tropical_Semirings): close all 16 sites + ~10 doc drifts — session +GREEN under Isabelle 2025-1 +* fix(Tropical_CNO): close 4 more sites — triangle NegInf cases, CNO +close conditional, ge_id 1=Fin0 +* fix(Tropical_Semirings): close most CNO drift, hoist sum_le_const + +trop_mat_pow_n_le_star +* fix(Tropical_Semirings): close Det/Kleene/Matrices/CNO regressions, +add ordered_ab_semigroup_add +* fix(Tropical_Determinants): close type-class regression at 153/207 +* fix(matrices): close cycle-excise root + use-before-define + 5 +supporting fixes +* fix(isabelle2025): Permutations import + less_tropical definition +fixes + +==== Documentation + +* docs(lean4): note that docs/FORMAL-PROOFS.adoc’s code listings predate +the v6.0 source (illustrative API); point to LEAN-FORMALIZATION.adoc as +authoritative +* docs(swarm): SWARM-SESSION 2026-04-26 + 6a2 sextet completion + STATE +update +* docs(afp): update HANDOVER_v2 — all sorries closed, AFP submission +ready +* docs: add arXiv paper outline for Rigorous Tropical Session Types +* docs: add TROPICAL-ESTATE-MAP.adoc +* docs(ecosystem): add ECOSYSTEM.a2ml with pipeline and tropical +connection +* docs: add HANDOVER_v2.adoc from Claude.ai session +* docs: add formal proof document and handover guide +* docs: add TOPOLOGY.md +* docs: substantive CRG C annotation (EXPLAINME.adoc) + +=== Pre-history + +Prior commits to this file’s introduction are recorded in git history +but not formally classified into Keep-a-Changelog sections. To backfill, +run `+git cliff -o CHANGELOG.md+` locally using the canonical +https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml[`+cliff.toml+`] +— this is one-shot mechanical work. + +''''' diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 index 4742e40..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,76 +0,0 @@ - - -# Changelog - -All notable changes to `tropical-resource-typing` will be documented in this file. - -This file is generated from conventional commits by the -[`changelog-reusable.yml`](https://github.com/hyperpolymath/standards/blob/main/.github/workflows/changelog-reusable.yml) -workflow (`hyperpolymath/standards#206`). Adopt the workflow in this repo's CI to keep this file in sync automatically — see -[`templates/cliff.toml`](https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml) -for the canonical config. - -The format follows [Keep a Changelog](https://keepachangelog.com/en/1.1.0/); -this project aims to follow [Semantic Versioning](https://semver.org/spec/v2.0.0.html). - -## [Unreleased] - -### Added - -- feat(lean4): bridge the two original twins onto the resource-grade axis (`Resource.Bridge`) — max-plus session grading shown resource-algebra-structured (`grade_spec_par = ⊞`, `grade_send = val 1 ⊠ ·`) with the QTT refinement restated in the resource order (`grade_le_sequential`); the bounded bottleneck algebra embedded into `Resource.Instances.MinMax`, with `embed_tcZero_ne_zero` exposing the finite-`∞` approximation and `hub_ceiling_le` restating `hub_ceiling` in `⊑`. Closes the standing "construct a functor / state the QTT quotient morphism" open items -- feat(lean4): add the **resource-grade axis** — `Resource.*` library exporting a reusable resource-algebra interface (`ResourceSemiring` + ordered `ResourceAlgebra`, no Mathlib), the canonical dioid-order builder, concrete instances (Linear/Affine `{0,1,ω}`, MaxPlus, MinPlus, MinMax), and the parametric transport theorem `parametric_resource_transport` (alias `resource_laws_sufficient_for_consumers`) over `ConsumerLawBundle`; aggregator `Resource.lean`; `lake build` green, new theorems depend only on propext/Quot.sound (or nothing) -- feat(lean4): prove tropical carriers are infinite (`Resource.Stress`: `infinite_maxPlus/minPlus/minMax`) — the infinite-carrier stress test that the abstraction is not a finite `{0,1,ω}` reification -- feat(lean4): add `Resource.EchoBridge` — abstract `ResidueMeasure` showing a resource algebra may measure (opaque) Echo residues, direction `E → R`, with a compiling max-plus witness; no `echo-types` dependency -- docs: add `FOUNDATION_CONTRACT.md`, `docs/RESOURCE-ALGEBRA.adoc`, `docs/ECHO-RESIDUE-BRIDGE.adoc` (resource grade vs resource algebra vs tropical instance vs residue measure; the "tropical is not Echo" boundary invariant) -- ci(lean4): extend `lean.yml` axiom audit to the new `Resource.*` headline theorems and instances -- feat(lean4): migrate the min-max transport semiring (TropicalAdapterPath) in beside the max-plus twin; pin Lean 4.13.0 via lean-toolchain; add lakefile + lake-manifest; `lake build` green -- feat(lean4): prove the De Morgan duality bridge — dualGrade_invol, dual_tcAdd_is_max (dual of min = max), dual_tcMul_is_min (dual of max = min) -- docs(lean4): add docs/LEAN-FORMALIZATION.adoc (authoritative Lean reference: build/verify recipe, theorem index, axiom audit, provenance) + README section -- ci(lean4): add lean.yml — lake build + axiom audit (propext/Quot.sound only, no sorry) on push/PR -- feat(isabelle): close all sorries in Tropical_Kleene and Tropical_Matrices_Clean -- feat(isabelle): close all sorries in Tropical_CNO.thy -- feat(determinants): add Tropical_Determinants.thy — optimal assignment theorem -- feat(isabelle): close bellman_ford OFFICIAL SORRY 2 — min-plus Bellman-Ford proved -- feat(isabelle): extend Tropical_Matrices_Full.thy -- feat(afp): create AFP submission files for Tropical_Semirings -- feat(isabelle): recover Tropical_Matrices_Full, Kleene, CNO, and Clean -- feat(isabelle,lean4): recover Tropical_v2.thy and TropicalSessionTypes.lean v6.0 -- feat(lean4): add tropical session types formalisation -- feat(isabelle): add verified tropical semiring formalisation - -### Fixed - -- fix(lean4): repair TropicalSessionTypes + TropicalAdapterPath to compile clean under core Lean 4.13.0 — import ordering, Mathlib-only `push_neg`→core tactics, `AdapterPath` def→abbrev, local `One` shim (4.13.0 core lacks One), `pathCost_append`/`pathCost_le_sequential` reproved; the inherited "Verified" headers were never true -- fix(lean4): replace the FALSE `dual_tcMul_bounded` (`dual(max m n)=dual m+dual n−maxGrade`, wrong at m=1,n=2) with the correct De Morgan dual `dual_tcMul_is_min` -- fix(ci): sync hypatia-scan.yml to canonical (413: env.HOME+Phase-2+SARIF) (#1) -- fix(Tropical_Semirings): close all 16 sites + ~10 doc drifts — session GREEN under Isabelle 2025-1 -- fix(Tropical_CNO): close 4 more sites — triangle NegInf cases, CNO close conditional, ge_id 1=Fin0 -- fix(Tropical_Semirings): close most CNO drift, hoist sum_le_const + trop_mat_pow_n_le_star -- fix(Tropical_Semirings): close Det/Kleene/Matrices/CNO regressions, add ordered_ab_semigroup_add -- fix(Tropical_Determinants): close type-class regression at 153/207 -- fix(matrices): close cycle-excise root + use-before-define + 5 supporting fixes -- fix(isabelle2025): Permutations import + less_tropical definition fixes - -### Documentation - -- docs(lean4): note that docs/FORMAL-PROOFS.adoc's code listings predate the v6.0 source (illustrative API); point to LEAN-FORMALIZATION.adoc as authoritative -- docs(swarm): SWARM-SESSION 2026-04-26 + 6a2 sextet completion + STATE update -- docs(afp): update HANDOVER_v2 — all sorries closed, AFP submission ready -- docs: add arXiv paper outline for Rigorous Tropical Session Types -- docs: add TROPICAL-ESTATE-MAP.adoc -- docs(ecosystem): add ECOSYSTEM.a2ml with pipeline and tropical connection -- docs: add HANDOVER_v2.adoc from Claude.ai session -- docs: add formal proof document and handover guide -- docs: add TOPOLOGY.md -- docs: substantive CRG C annotation (EXPLAINME.adoc) - -## Pre-history - -Prior commits to this file's introduction are recorded in git history but not formally classified into Keep-a-Changelog sections. To backfill, run `git cliff -o CHANGELOG.md` locally using the canonical [`cliff.toml`](https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml) — this is one-shot mechanical work. - ---- - - diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..f801aef --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,42 @@ +== Code of Conduct + +This project adopts the +https://www.contributor-covenant.org/version/2/1/code_of_conduct/[Contributor +Covenant 2.1]. The key obligations are summarised inline so they are +enforceable directly from this repository. + +=== Our Pledge + +We pledge to make participation a *harassment*-free experience for +everyone, regardless of age, body size, visible or invisible disability, +ethnicity, sex characteristics, gender identity and expression, level of +experience, education, socio-economic status, nationality, personal +appearance, race, religion, or sexual identity and orientation. + +=== Unacceptable Behaviour + +Unacceptable behaviour includes *harassment* in any form, public or +private; trolling, insulting or derogatory comments; personal or +political attacks; publishing others’ private information without +permission; and other conduct reasonably considered inappropriate in a +professional setting. + +=== Enforcement + +Instances of abusive, harassing, or otherwise unacceptable behaviour may +be reported confidentially to the maintainer at +`+j.d.a.jewell@open.ac.uk+`. All complaints will be reviewed and +investigated promptly and fairly; reports are confidential by default. + +==== Enforcement procedures + +Maintainers follow these Community Impact Guidelines: + +[arabic] +. *Correction* — a private, written warning. +. *Warning* — consequences for continued behaviour; no interaction for a +set period. +. *Temporary ban* — a temporary ban from interaction or public +communication. +. *Permanent ban* — a permanent ban from public interaction within the +community. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index d5563aa..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,25 +0,0 @@ - -# Code of Conduct - -This project adopts the [Contributor Covenant 2.1](https://www.contributor-covenant.org/version/2/1/code_of_conduct/). The key obligations are summarised inline so they are enforceable directly from this repository. - -## Our Pledge - -We pledge to make participation a **harassment**-free experience for everyone, regardless of age, body size, visible or invisible disability, ethnicity, sex characteristics, gender identity and expression, level of experience, education, socio-economic status, nationality, personal appearance, race, religion, or sexual identity and orientation. - -## Unacceptable Behaviour - -Unacceptable behaviour includes **harassment** in any form, public or private; trolling, insulting or derogatory comments; personal or political attacks; publishing others' private information without permission; and other conduct reasonably considered inappropriate in a professional setting. - -## Enforcement - -Instances of abusive, harassing, or otherwise unacceptable behaviour may be reported confidentially to the maintainer at `j.d.a.jewell@open.ac.uk`. All complaints will be reviewed and investigated promptly and fairly; reports are confidential by default. - -### Enforcement procedures - -Maintainers follow these Community Impact Guidelines: - -1. **Correction** — a private, written warning. -2. **Warning** — consequences for continued behaviour; no interaction for a set period. -3. **Temporary ban** — a temporary ban from interaction or public communication. -4. **Permanent ban** — a permanent ban from public interaction within the community. diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..016e06b --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,39 @@ +== Contributing + +Contributions are welcome! Please: + +[arabic] +. Fork the repository +. Create a feature branch from `+main+` +. Ensure all CI checks pass +. Submit a pull request + +=== Standards + +This project follows the +https://github.com/hyperpolymath/standards[Rhodium Standard Repository +(RSR)] conventions. + +=== Contribution model — Tri-Perimeter Contribution Framework (TPCF) + +This repo follows the estate-wide *Tri-Perimeter Contribution Framework +(TPCF)* — graduated trust without gatekeeping: + +* *Perimeter 1 — Core Systems (maintainers only).* The proof kernel: the +Lean `+Resource/+` axis + `+Tropical*.lean+`, the Isabelle `+*.thy+` +theories, and the build/CI tooling. Direct commits by maintainers only +(see `+MAINTAINERS.adoc+`). +* *Perimeter 2 — Expert Extensions (trusted contributors).* New semiring +instances, lemmas, and transport theorems. Apply via issue → review → +merge, with `+lake build+` (Lean) / `+just isabelle-build+` (Isabelle) +green. +* *Perimeter 3 — Community Sandbox (open to all).* Docs (`+.adoc+`), +`+.well-known/+`, and spec proposals. + +The fork-and-PR workflow above applies to all three perimeters; proofs +must type-check and `+just check-sorry+` must be clean before review. + +=== License + +By contributing, you agree that your contributions will be licensed +under MPL-2.0 (with MPL-2.0 as automatic legal fallback). diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index 8472250..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,27 +0,0 @@ - -# Contributing - -Contributions are welcome! Please: - -1. Fork the repository -2. Create a feature branch from `main` -3. Ensure all CI checks pass -4. Submit a pull request - -## Standards - -This project follows the [Rhodium Standard Repository (RSR)](https://github.com/hyperpolymath/standards) conventions. - -## Contribution model — Tri-Perimeter Contribution Framework (TPCF) - -This repo follows the estate-wide **Tri-Perimeter Contribution Framework (TPCF)** — graduated trust without gatekeeping: - -- **Perimeter 1 — Core Systems (maintainers only).** The proof kernel: the Lean `Resource/` axis + `Tropical*.lean`, the Isabelle `*.thy` theories, and the build/CI tooling. Direct commits by maintainers only (see `MAINTAINERS.adoc`). -- **Perimeter 2 — Expert Extensions (trusted contributors).** New semiring instances, lemmas, and transport theorems. Apply via issue → review → merge, with `lake build` (Lean) / `just isabelle-build` (Isabelle) green. -- **Perimeter 3 — Community Sandbox (open to all).** Docs (`.adoc`), `.well-known/`, and spec proposals. - -The fork-and-PR workflow above applies to all three perimeters; proofs must type-check and `just check-sorry` must be clean before review. - -## License - -By contributing, you agree that your contributions will be licensed under MPL-2.0 (with MPL-2.0 as automatic legal fallback). diff --git a/FOUNDATIONS_BRIDGE.adoc b/FOUNDATIONS_BRIDGE.adoc new file mode 100644 index 0000000..2cf86ef --- /dev/null +++ b/FOUNDATIONS_BRIDGE.adoc @@ -0,0 +1,203 @@ +== Foundations bridge — consuming `+echo-types+` and `+tropical-resource-typing+` + +This is a downstream integration brief for `+my-lang+` or any other +consumer of the two foundations. It coordinates their outputs; it *adds +no new proofs*. Every theorem named below is already mechanised upstream +— this document only tells a downstream language _how to depend on the +two foundations without collapsing them into each other_. + +Source of truth: + +[width="100%",cols="25%,25%,25%,25%",options="header",] +|=== +|Foundation |Axis exported |Contract |Machine-checked in +|`+tropical-resource-typing+` |resource-grade axis +|`+FOUNDATION_CONTRACT.md+` |Lean 4 `+Resource.*+` + +|`+echo-types+` |residual-modality axis |`+FOUNDATION_CONTRACT.md+` +|Agda `+Echo.*+` (`+--safe --without-K+`) +|=== + +''''' + +=== 1. Two independent axes + +A consumer tracks *two orthogonal things*. They are not refinements of +one another and they meet only at the one-directional seam in §2. + +____ +The numbering (`+1+`, `+3+`) follows the upstream axis taxonomy. Only +these two axes are in scope for this brief; they are mutually +independent at the core. +____ + +==== Axis 1 — Resource algebra (`+tropical-resource-typing+`) + +* *What it is:* binder/resource _quantities_ — usage, cost, latency, +critical path, bottleneck — living in an ordered-semiring / +usage-algebra interface. +* *Interface:* `+Resource.ResourceAlgebra+` (= +`+Resource.ResourceSemiring+` + an order). `+⊞+` = choice/alternative, +`+⊠+` = sequential composition. +* *Instances:* +`+Resource.Instances.{Linear, Affine, MaxPlus, MinPlus, MinMax}+` — +i.e. linear / affine usage and the tropical (max-plus / min-plus / +min-max) algebras. The tropical instances double as an *infinite-carrier +stress test* (`+Resource.Stress+`, `+Resource.Infinite+`). +* *Used by:* QTT-style / quantitative *resource soundness*. Prove +soundness _parametrically_ over the interface via +`+Resource.ConsumerLawBundle+` (`+parametric_resource_transport+`, alias +`+resource_laws_sufficient_for_consumers+`), then instantiate at any +algebra above with no algebraic re-proof. + +==== Axis 3 — Echo modality (`+echo-types+`) + +* *What it is:* structured *residue / loss / forgetting / projection* — +the remainder of an information-losing map, +`+Echo f y := Σ (x : A), (f x ≡ y)+`. +* *Indexed by a thin poset:* `+Echo.Index.ThinPoset+`; the canonical +index is the three-point loss order `+keep ≤ residue ≤ forget+` +(`+grade-thinPoset+`). Thinness (order proofs are propositional) is +load-bearing, not cosmetic. +* *Proves residual metatheory:* `+Echo.Modality.Core+` / +`+Echo.Modality.Interface+` give `+degrade+`, the unit law +`+degrade-id+`, the path-independence law `+degrade-compose+`, and the +no-section theorem `+no-section-of-collapsing-map+`; the +downstream-instantiable record is `+EchoModality+` (canonical witness +`+grade-echoModality+`). +* *Independent of the resource algebra at the core:* +`+Echo.Modality.Core+`, `+Echo.Modality.Interface+`, and +`+Echo.Index.ThinPoset+` import *no* semiring / resource-algebra +machinery. The proof-relevant content of `+degrade+` is carried by the +thin order of the index, not by any semiring-valued grade. + +''''' + +=== 2. The seam + +The only sanctioned connection between the axes is a *measure*, pointing +in exactly one direction: + +.... +ResidueMeasure : Echo residue ──▶ ResourceAlgebra carrier +.... + +* *Direction:* a resource algebra is _consumed as a measure by_ Echo. +The residue carrier is opaque; only the codomain is a resource algebra. +* *Never the reverse:* Echo is *not* produced as a resource instance, +nor as a `+Soundness(R)+` instance. + +The seam is mechanised on both sides — pick whichever framing matches +your downstream proof obligation; both fix the same `+E → R+` direction: + +*echo-types side (order-monotone view)* — `+Echo.Measure.Interface+`: + +[source,agda] +---- +record ResidueMeasure (E : EchoModality P ℓc) (R : OrderedCarrier ℓm ℓo) where + field + measure : ∀ {i} → ⟦ i ⟧ → Carrier R + monotone : ∀ {i j} (p : i ≤ j) (x : ⟦ i ⟧) → + measure x ≤R measure (degrade p x) +---- + +*tropical side (monoid-homomorphism view)* — `+Resource.EchoBridge+`: + +[source,lean] +---- +structure ResidueMeasure (E : Type) (R : Type) [ResourceAlgebra R] where + combine : E → E → E -- Echo-side residue accumulation (opaque) + empty : E + measure : E → R -- the measurement into a resource grade + measure_empty : measure empty = one + measure_combine : ∀ e₁ e₂, measure (combine e₁ e₂) = measure e₁ ⊠ measure e₂ +---- + +In both, the residue carrier `+E+` carries *no* `+ResourceAlgebra+` +instance and nothing gives it one. `+echo-types+` and +`+tropical-resource-typing+` have *no dependency on each other*; the +seam is supplied downstream. + +''''' + +=== 3. Downstream import pattern + +A consuming language (e.g. `+my-lang+`) should expose: + +.... +Resource parameter R : ResourceAlgebra -- Axis 1 +Echo parameter E : EchoModality -- Axis 3 +Optional seam M : ResidueMeasure E R -- §2, only if you measure residues +.... + +Prove resource soundness against `+R+` parametrically (quote +`+Resource.ConsumerLawBundle+`), instantiate Echo at your own fibration +via `+EchoModality+`, and reach for `+M+` _only_ when you genuinely +measure residues. + +It should *not* introduce any of: + +* ✗ Echo as an instance of `+ResourceAlgebra+` +* ✗ Echo as an instance of `+Soundness(R)+` (resource soundness) +* ✗ Tropical (any of the resource instances) as an Echo modality + +These three are exactly the collapses the foundations are built to +prevent. + +''''' + +=== 4. Vocabulary + +Use these three terms precisely — they name three orthogonal things: + +[width="100%",cols="50%,50%",options="header",] +|=== +|Use |Meaning +|*resource grade* |a binder/resource quantity on the resource-algebra +axis (Axis 1) + +|*echo index* |an inhabitant of the thin-poset index of the Echo +modality, e.g. `+keep ≤ residue ≤ forget+` (Axis 3) + +|*residue measure* |a resource-algebra-valued _observation_ of an Echo +residue (the §2 seam) +|=== + +*Avoid / deprecate `+echo-grade+`.* It ambiguously fuses the _echo +index_ (the retention axis of the modality) with the _resource grade_ +(the semiring axis) — which is precisely the collapse this bridge +forbids. If the term must be explained, explain it as that ambiguity. + +''''' + +=== 5. Boundary invariants + +These hold as mechanised upstream results; downstream code must not +violate them. + +[arabic] +. *Echo IS-NOT a resource instance.* Do not model Echo as a +`+Soundness(S)+` / resource-algebra instance. (Upstream: +`+Echo.Separation.NotResourceInstance+`; the proof-relevant Echo +structure is carried by thinness of the index, not by any semiring +grade.) +. *Tropical IS a resource-algebra instance.* Max-plus / min-plus / +min-max are instances of `+Resource.ResourceAlgebra+` and belong on the +resource-grade axis — they are not Echo modalities. +. *Residue measures are observations, not definitions of Echo.* A +`+ResidueMeasure+` is a lossy, one-directional read-out; +`+Echo.Modality.Core+` never depends on it, and never may. +. *Equal residue measure does not imply equal Echo.* A measure can send +two genuinely-distinct Echo residues to the same value while the +modality keeps them apart — so no measure is the identity criterion of +Echo. (Upstream: `+equal-measure-does-not-imply-equal-echo+`, and the +sharper informative-measure witness +`+equal-informative-measure-does-not-imply-equal-echo+`.) + +''''' + +_This brief restates the two `+FOUNDATION_CONTRACT.md+` files for the +downstream direction and adds nothing to them. For the full contracts +and the parametric transport / anti-collapse theorems, read each +foundation’s `+FOUNDATION_CONTRACT.md+` and (tropical) +`+docs/ECHO-RESIDUE-BRIDGE.adoc+`._ diff --git a/FOUNDATIONS_BRIDGE.md b/FOUNDATIONS_BRIDGE.md deleted file mode 100644 index 014a24e..0000000 --- a/FOUNDATIONS_BRIDGE.md +++ /dev/null @@ -1,179 +0,0 @@ - - -# Foundations bridge — consuming `echo-types` and `tropical-resource-typing` - -This is a downstream integration brief for `my-lang` or any other consumer of -the two foundations. It coordinates their outputs; it **adds no new proofs**. -Every theorem named below is already mechanised upstream — this document only -tells a downstream language *how to depend on the two foundations without -collapsing them into each other*. - -Source of truth: - -| Foundation | Axis exported | Contract | Machine-checked in | -|---|---|---|---| -| `tropical-resource-typing` | resource-grade axis | `FOUNDATION_CONTRACT.md` | Lean 4 `Resource.*` | -| `echo-types` | residual-modality axis | `FOUNDATION_CONTRACT.md` | Agda `Echo.*` (`--safe --without-K`) | - ---- - -## 1. Two independent axes - -A consumer tracks **two orthogonal things**. They are not refinements of one -another and they meet only at the one-directional seam in §2. - -> The numbering (`1`, `3`) follows the upstream axis taxonomy. Only these two -> axes are in scope for this brief; they are mutually independent at the core. - -### Axis 1 — Resource algebra (`tropical-resource-typing`) - -- **What it is:** binder/resource *quantities* — usage, cost, latency, critical - path, bottleneck — living in an ordered-semiring / usage-algebra interface. -- **Interface:** `Resource.ResourceAlgebra` (= `Resource.ResourceSemiring` + an - order). `⊞` = choice/alternative, `⊠` = sequential composition. -- **Instances:** `Resource.Instances.{Linear, Affine, MaxPlus, MinPlus, MinMax}` - — i.e. linear / affine usage and the tropical (max-plus / min-plus / min-max) - algebras. The tropical instances double as an **infinite-carrier stress test** - (`Resource.Stress`, `Resource.Infinite`). -- **Used by:** QTT-style / quantitative **resource soundness**. Prove soundness - *parametrically* over the interface via `Resource.ConsumerLawBundle` - (`parametric_resource_transport`, alias `resource_laws_sufficient_for_consumers`), - then instantiate at any algebra above with no algebraic re-proof. - -### Axis 3 — Echo modality (`echo-types`) - -- **What it is:** structured **residue / loss / forgetting / projection** — the - remainder of an information-losing map, `Echo f y := Σ (x : A), (f x ≡ y)`. -- **Indexed by a thin poset:** `Echo.Index.ThinPoset`; the canonical index is the - three-point loss order `keep ≤ residue ≤ forget` (`grade-thinPoset`). Thinness - (order proofs are propositional) is load-bearing, not cosmetic. -- **Proves residual metatheory:** `Echo.Modality.Core` / - `Echo.Modality.Interface` give `degrade`, the unit law `degrade-id`, the - path-independence law `degrade-compose`, and the no-section theorem - `no-section-of-collapsing-map`; the downstream-instantiable record is - `EchoModality` (canonical witness `grade-echoModality`). -- **Independent of the resource algebra at the core:** `Echo.Modality.Core`, - `Echo.Modality.Interface`, and `Echo.Index.ThinPoset` import **no** - semiring / resource-algebra machinery. The proof-relevant content of `degrade` - is carried by the thin order of the index, not by any semiring-valued grade. - ---- - -## 2. The seam - -The only sanctioned connection between the axes is a **measure**, pointing in -exactly one direction: - -``` -ResidueMeasure : Echo residue ──▶ ResourceAlgebra carrier -``` - -- **Direction:** a resource algebra is *consumed as a measure by* Echo. The - residue carrier is opaque; only the codomain is a resource algebra. -- **Never the reverse:** Echo is **not** produced as a resource instance, nor as - a `Soundness(R)` instance. - -The seam is mechanised on both sides — pick whichever framing matches your -downstream proof obligation; both fix the same `E → R` direction: - -**echo-types side (order-monotone view)** — `Echo.Measure.Interface`: - -```agda -record ResidueMeasure (E : EchoModality P ℓc) (R : OrderedCarrier ℓm ℓo) where - field - measure : ∀ {i} → ⟦ i ⟧ → Carrier R - monotone : ∀ {i j} (p : i ≤ j) (x : ⟦ i ⟧) → - measure x ≤R measure (degrade p x) -``` - -**tropical side (monoid-homomorphism view)** — `Resource.EchoBridge`: - -```lean -structure ResidueMeasure (E : Type) (R : Type) [ResourceAlgebra R] where - combine : E → E → E -- Echo-side residue accumulation (opaque) - empty : E - measure : E → R -- the measurement into a resource grade - measure_empty : measure empty = one - measure_combine : ∀ e₁ e₂, measure (combine e₁ e₂) = measure e₁ ⊠ measure e₂ -``` - -In both, the residue carrier `E` carries **no** `ResourceAlgebra` instance and -nothing gives it one. `echo-types` and `tropical-resource-typing` have **no -dependency on each other**; the seam is supplied downstream. - ---- - -## 3. Downstream import pattern - -A consuming language (e.g. `my-lang`) should expose: - -``` -Resource parameter R : ResourceAlgebra -- Axis 1 -Echo parameter E : EchoModality -- Axis 3 -Optional seam M : ResidueMeasure E R -- §2, only if you measure residues -``` - -Prove resource soundness against `R` parametrically (quote -`Resource.ConsumerLawBundle`), instantiate Echo at your own fibration via -`EchoModality`, and reach for `M` *only* when you genuinely measure residues. - -It should **not** introduce any of: - -- ✗ Echo as an instance of `ResourceAlgebra` -- ✗ Echo as an instance of `Soundness(R)` (resource soundness) -- ✗ Tropical (any of the resource instances) as an Echo modality - -These three are exactly the collapses the foundations are built to prevent. - ---- - -## 4. Vocabulary - -Use these three terms precisely — they name three orthogonal things: - -| Use | Meaning | -|---|---| -| **resource grade** | a binder/resource quantity on the resource-algebra axis (Axis 1) | -| **echo index** | an inhabitant of the thin-poset index of the Echo modality, e.g. `keep ≤ residue ≤ forget` (Axis 3) | -| **residue measure** | a resource-algebra-valued *observation* of an Echo residue (the §2 seam) | - -**Avoid / deprecate `echo-grade`.** It ambiguously fuses the *echo index* (the -retention axis of the modality) with the *resource grade* (the semiring axis) — -which is precisely the collapse this bridge forbids. If the term must be -explained, explain it as that ambiguity. - ---- - -## 5. Boundary invariants - -These hold as mechanised upstream results; downstream code must not violate them. - -1. **Echo IS-NOT a resource instance.** Do not model Echo as a `Soundness(S)` / - resource-algebra instance. (Upstream: `Echo.Separation.NotResourceInstance`; - the proof-relevant Echo structure is carried by thinness of the index, not by - any semiring grade.) -2. **Tropical IS a resource-algebra instance.** Max-plus / min-plus / min-max are - instances of `Resource.ResourceAlgebra` and belong on the resource-grade axis - — they are not Echo modalities. -3. **Residue measures are observations, not definitions of Echo.** A - `ResidueMeasure` is a lossy, one-directional read-out; `Echo.Modality.Core` - never depends on it, and never may. -4. **Equal residue measure does not imply equal Echo.** A measure can send two - genuinely-distinct Echo residues to the same value while the modality keeps - them apart — so no measure is the identity criterion of Echo. (Upstream: - `equal-measure-does-not-imply-equal-echo`, and the sharper informative-measure - witness `equal-informative-measure-does-not-imply-equal-echo`.) - ---- - -*This brief restates the two `FOUNDATION_CONTRACT.md` files for the downstream -direction and adds nothing to them. For the full contracts and the parametric -transport / anti-collapse theorems, read each foundation's `FOUNDATION_CONTRACT.md` -and (tropical) `docs/ECHO-RESIDUE-BRIDGE.adoc`.* diff --git a/FOUNDATION_CONTRACT.adoc b/FOUNDATION_CONTRACT.adoc new file mode 100644 index 0000000..ee09ca8 --- /dev/null +++ b/FOUNDATION_CONTRACT.adoc @@ -0,0 +1,152 @@ +== Tropical Resource Typing Foundation Contract + +Tropical Resource Typing exports the *resource-grade axis*: a reusable +ordered-semiring / resource-algebra interface, with tropical instances +serving as serious infinite-carrier stress tests. + +This file is the stable contract. The machine-checked source of truth is +the `+Resource.*+` Lean 4 library (aggregator: `+Resource.lean+`), built +dependency-free on the pinned `+leanprover/lean4:v4.13.0+` (no Mathlib). + +=== Vocabulary + +* *Resource grade* — a binder/resource _quantity_: usage, cost, latency, +critical path, bottleneck, residue measure. Grades are the things +resource typing tracks on binders. +* *Resource algebra* — the generic _interface_ a grade algebra must +satisfy: an ordered semiring / usage algebra +(`+Resource.ResourceAlgebra+`). +* *Tropical instance* — a concrete resource algebra whose operations are +`+max+`/`+min+`/`+++`: max-plus, min-plus, min-max (bottleneck). +* *Residue measure* — a _downstream consumer_ that uses a resource +algebra to measure Echo residues. The residue carrier is opaque; only +the codomain is a resource algebra. + +These are four distinct things. A _grade_ is a value; a _resource +algebra_ is the interface those values live in; a _tropical instance_ is +one such interface implementation; a _residue measure_ is a consumer +that maps some external carrier _into_ a resource algebra. + +=== Resource grade + +Binder/resource quantities such as usage, cost, latency, critical path, +and bottleneck. In this repository they are the elements of a +resource-algebra carrier `+R+`. + +=== Resource algebra + +A generic ordered semiring / usage-algebra interface +(`+Resource.ResourceAlgebra+`, layered as `+Resource.ResourceSemiring+` ++ an order). It requires only what generic quantitative/resource +consumers actually use: + +.... +carrier R +zero one : R -- additive identity / multiplicative identity +add mul : R → R → R -- ⊞ choice/alternative ; ⊠ sequential composition +le : R → R → Prop -- ⊑ grade subsumption + +add associative, commutative, identity (zero) +mul associative, identity (one) +zero annihilates mul +left/right distributivity +⊑ reflexive and transitive (a preorder) +add and mul monotone with respect to ⊑ +.... + +Deliberately *not* required by the interface: a finite carrier, additive +idempotence, non-idempotence, multiplicative commutativity, totality, +decidable equality, or any `+destruct+`/reflexivity proof strategy. +Antisymmetry is offered as an _optional_ refinement +(`+PartialOrderedResourceAlgebra+`), not the core. + +*Linear, affine, max-plus, min-plus, and min-max are instances.* + +[width="100%",cols="48%,18%,15%,10%,9%",options="header",] +|=== +|instance |carrier |`+⊞+` choice |`+⊠+` seq |finite +|`+Resource.Instances.Linear+` |`+{0,1,ω}+` |usage-add |scale |yes +|`+Resource.Instances.Affine+` |`+{0,1,ω}+` |usage-add |scale |yes +|`+Resource.Instances.MaxPlus+` |`+ℕ ∪ {−∞}+` |`+max+` |`+++` |no +|`+Resource.Instances.MinPlus+` |`+ℕ ∪ {+∞}+` |`+min+` |`+++` |no +|`+Resource.Instances.MinMax+` |`+ℕ ∪ {+∞}+` |`+min+` |`+max+` |no +|=== + +Tropical conventions are stated precisely at each instance and +summarised in `+docs/RESOURCE-ALGEBRA.adoc+` (which operation is choice, +which is sequential composition, what `+zero+`/`+one+` are, and which +order direction means "`better / cheaper / more available`"). + +=== Tropical + +Tropical instances are semantically different from finite usage +quantities and serve as *infinite-carrier stress tests* of the +abstraction. `+Resource.Stress+` proves `+Resource.Infinite+` for the +max-plus, min-plus, and min-max carriers, and checks that the single +generic transport theorem instantiates at each of them. If the interface +only ever had to model `+{0,1,ω}+`, a finite lookup table would suffice; +because the _same_ interface and the _same_ parametric theorem also +serve the infinite tropical carriers — and the generic proofs never +case-split a carrier — the abstraction is doing real work and is not a +finite `+{0,1,ω}+` reification. + +=== Boundary invariant + +* *Tropical is a resource-algebra foundation.* It belongs to the +resource-grade axis. +* *Tropical is not the Echo modality.* It is not an Echo instance, and +Echo is not a tropical/resource instance. +* *Echo may consume tropical values as residue measures, but Echo is not +a resource / soundness instance.* The only sanctioned direction is ++ +.... +resource algebra ──consumed by──▶ residue measure +.... ++ +never ++ +.... +Echo ──is an instance of──▶ resource / soundness (forbidden) +.... ++ +This is machine-checked in `+Resource.EchoBridge+`: the residue carrier +`+E+` there is an opaque type with _no_ `+ResourceAlgebra+` instance, +and the measure maps `+E → R+` into a resource algebra. This repository +imports no `+echo-types+` dependency. + +=== Consumer rule + +Downstream languages (e.g. `+my-lang+`) should prove resource soundness +*parametrically over the resource-algebra interface*, then instantiate +it with concrete algebras. The exported obligation bundle is +`+Resource.ConsumerLawBundle+`, discharged for every resource algebra by + +.... +theorem parametric_resource_transport (R) [ResourceAlgebra R] : ConsumerLawBundle R +.... + +(stable alias `+resource_laws_sufficient_for_consumers+`). A proof that +quotes only `+ConsumerLawBundle+` can be instantiated at linear, affine, +max-plus, min-plus, or min-max *without re-proving any algebraic fact* — +the transport theorem is proved abstractly from the interface and never +inspects a carrier, which is exactly why it survives instantiation at +the infinite tropical carriers. + +=== Axiom hygiene + +`+lake build+` is green. Every new headline theorem depends on no +axioms, or only on `+propext+` (and `+Quot.sound+`) — the project’s +accepted standard. No `+sorry+`, no `+Classical.choice+`. CI +(`+.github/workflows/lean.yml+`) re-runs the build and the +`+#print axioms+` audit. + +=== Isabelle/HOL status + +The Isabelle development (`+ROOT+`, `+Tropical*.thy+`) is a _separate_, +heavyweight matrix-algebra treatment and is *not* part of this +contract’s green claim. It is *RED* and was *not re-run* here (no +Isabelle on this toolchain): per `+docs/BUILD-STATUS-2026-04-26.adoc+` +it has 16 proof-failure sites across 4 theories, superseding the earlier +"`AFP-ready / zero-sorries`" claims in `+docs/FORMAL-PROOFS.adoc+` and +`+docs/HANDOVER_v2.adoc+`. Treat the Lean `+Resource.*+` library as the +authoritative, re-verifiable foundation. diff --git a/FOUNDATION_CONTRACT.md b/FOUNDATION_CONTRACT.md deleted file mode 100644 index 025d28d..0000000 --- a/FOUNDATION_CONTRACT.md +++ /dev/null @@ -1,147 +0,0 @@ - - -# Tropical Resource Typing Foundation Contract - -Tropical Resource Typing exports the **resource-grade axis**: a reusable -ordered-semiring / resource-algebra interface, with tropical instances serving as -serious infinite-carrier stress tests. - -This file is the stable contract. The machine-checked source of truth is the -`Resource.*` Lean 4 library (aggregator: `Resource.lean`), built dependency-free -on the pinned `leanprover/lean4:v4.13.0` (no Mathlib). - -## Vocabulary - -- **Resource grade** — a binder/resource *quantity*: usage, cost, latency, - critical path, bottleneck, residue measure. Grades are the things resource - typing tracks on binders. -- **Resource algebra** — the generic *interface* a grade algebra must satisfy: an - ordered semiring / usage algebra (`Resource.ResourceAlgebra`). -- **Tropical instance** — a concrete resource algebra whose operations are - `max`/`min`/`+`: max-plus, min-plus, min-max (bottleneck). -- **Residue measure** — a *downstream consumer* that uses a resource algebra to - measure Echo residues. The residue carrier is opaque; only the codomain is a - resource algebra. - -These are four distinct things. A *grade* is a value; a *resource algebra* is the -interface those values live in; a *tropical instance* is one such interface -implementation; a *residue measure* is a consumer that maps some external carrier -*into* a resource algebra. - -## Resource grade - -Binder/resource quantities such as usage, cost, latency, critical path, and -bottleneck. In this repository they are the elements of a resource-algebra -carrier `R`. - -## Resource algebra - -A generic ordered semiring / usage-algebra interface (`Resource.ResourceAlgebra`, -layered as `Resource.ResourceSemiring` + an order). It requires only what generic -quantitative/resource consumers actually use: - -``` -carrier R -zero one : R -- additive identity / multiplicative identity -add mul : R → R → R -- ⊞ choice/alternative ; ⊠ sequential composition -le : R → R → Prop -- ⊑ grade subsumption - -add associative, commutative, identity (zero) -mul associative, identity (one) -zero annihilates mul -left/right distributivity -⊑ reflexive and transitive (a preorder) -add and mul monotone with respect to ⊑ -``` - -Deliberately **not** required by the interface: a finite carrier, additive -idempotence, non-idempotence, multiplicative commutativity, totality, decidable -equality, or any `destruct`/reflexivity proof strategy. Antisymmetry is offered as -an *optional* refinement (`PartialOrderedResourceAlgebra`), not the core. - -**Linear, affine, max-plus, min-plus, and min-max are instances.** - -| instance | carrier | `⊞` choice | `⊠` seq | finite | -| ----------------------------- | ------------ | ---------- | ------- | ------ | -| `Resource.Instances.Linear` | `{0,1,ω}` | usage-add | scale | yes | -| `Resource.Instances.Affine` | `{0,1,ω}` | usage-add | scale | yes | -| `Resource.Instances.MaxPlus` | `ℕ ∪ {−∞}` | `max` | `+` | no | -| `Resource.Instances.MinPlus` | `ℕ ∪ {+∞}` | `min` | `+` | no | -| `Resource.Instances.MinMax` | `ℕ ∪ {+∞}` | `min` | `max` | no | - -Tropical conventions are stated precisely at each instance and summarised in -`docs/RESOURCE-ALGEBRA.adoc` (which operation is choice, which is sequential -composition, what `zero`/`one` are, and which order direction means "better / -cheaper / more available"). - -## Tropical - -Tropical instances are semantically different from finite usage quantities and -serve as **infinite-carrier stress tests** of the abstraction. `Resource.Stress` -proves `Resource.Infinite` for the max-plus, min-plus, and min-max carriers, and -checks that the single generic transport theorem instantiates at each of them. If -the interface only ever had to model `{0,1,ω}`, a finite lookup table would -suffice; because the *same* interface and the *same* parametric theorem also serve -the infinite tropical carriers — and the generic proofs never case-split a carrier -— the abstraction is doing real work and is not a finite `{0,1,ω}` reification. - -## Boundary invariant - -- **Tropical is a resource-algebra foundation.** It belongs to the resource-grade - axis. -- **Tropical is not the Echo modality.** It is not an Echo instance, and Echo is - not a tropical/resource instance. -- **Echo may consume tropical values as residue measures, but Echo is not a - resource / soundness instance.** The only sanctioned direction is - - ``` - resource algebra ──consumed by──▶ residue measure - ``` - - never - - ``` - Echo ──is an instance of──▶ resource / soundness (forbidden) - ``` - - This is machine-checked in `Resource.EchoBridge`: the residue carrier `E` there - is an opaque type with *no* `ResourceAlgebra` instance, and the measure maps - `E → R` into a resource algebra. This repository imports no `echo-types` - dependency. - -## Consumer rule - -Downstream languages (e.g. `my-lang`) should prove resource soundness -**parametrically over the resource-algebra interface**, then instantiate it with -concrete algebras. The exported obligation bundle is `Resource.ConsumerLawBundle`, -discharged for every resource algebra by - -``` -theorem parametric_resource_transport (R) [ResourceAlgebra R] : ConsumerLawBundle R -``` - -(stable alias `resource_laws_sufficient_for_consumers`). A proof that quotes only -`ConsumerLawBundle` can be instantiated at linear, affine, max-plus, min-plus, or -min-max **without re-proving any algebraic fact** — the transport theorem is -proved abstractly from the interface and never inspects a carrier, which is -exactly why it survives instantiation at the infinite tropical carriers. - -## Axiom hygiene - -`lake build` is green. Every new headline theorem depends on no axioms, or only on -`propext` (and `Quot.sound`) — the project's accepted standard. No `sorry`, no -`Classical.choice`. CI (`.github/workflows/lean.yml`) re-runs the build and the -`#print axioms` audit. - -## Isabelle/HOL status - -The Isabelle development (`ROOT`, `Tropical*.thy`) is a *separate*, heavyweight -matrix-algebra treatment and is **not** part of this contract's green claim. It is -**RED** and was **not re-run** here (no Isabelle on this toolchain): per -`docs/BUILD-STATUS-2026-04-26.adoc` it has 16 proof-failure sites across 4 -theories, superseding the earlier "AFP-ready / zero-sorries" claims in -`docs/FORMAL-PROOFS.adoc` and `docs/HANDOVER_v2.adoc`. Treat the Lean `Resource.*` -library as the authoritative, re-verifiable foundation. diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc new file mode 100644 index 0000000..9b836fb --- /dev/null +++ b/GOVERNANCE.adoc @@ -0,0 +1,60 @@ +== Governance + +=== Overview + +This project is governed by the following principles and structures to +ensure transparent, inclusive, and effective decision-making. + +=== Roles and Responsibilities + +==== Maintainers + +Maintainers are responsible for: - Reviewing and merging pull requests - +Managing releases and versioning - Ensuring code quality and standards - +Triaging issues and bug reports - Community engagement and support + +==== Contributors + +Contributors are expected to: - Follow the code of conduct - Submit +well-documented pull requests - Write tests for new functionality - +Maintain existing tests - Update documentation as needed + +=== Decision Making + +==== Minor Changes + +* Can be made by any maintainer +* Include bug fixes, documentation updates, dependency updates + +==== Major Changes + +* Require discussion in issues or pull requests +* Include new features, architectural changes, API changes +* Need approval from at least 2 maintainers + +==== Breaking Changes + +* Require RFC (Request for Comments) process +* Need approval from majority of maintainers +* Must include migration guide + +=== Code of Conduct + +All participants are expected to follow our Code of Conduct. Violations +can be reported to the maintainers. + +=== Communication + +* *Issues*: For bug reports and feature requests +* *Discussions*: For questions and general discussion +* *Pull Requests*: For code contributions + +=== Licensing + +All contributions are made under the terms of the repository’s LICENSE +file. By submitting a pull request, you agree to license your +contributions accordingly. + +''''' + +_Last updated: 2026-07-18_ diff --git a/GOVERNANCE.md b/GOVERNANCE.md deleted file mode 100644 index e27364c..0000000 --- a/GOVERNANCE.md +++ /dev/null @@ -1,60 +0,0 @@ -# Governance - -## Overview - -This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making. - -## Roles and Responsibilities - -### Maintainers - -Maintainers are responsible for: -- Reviewing and merging pull requests -- Managing releases and versioning -- Ensuring code quality and standards -- Triaging issues and bug reports -- Community engagement and support - -### Contributors - -Contributors are expected to: -- Follow the code of conduct -- Submit well-documented pull requests -- Write tests for new functionality -- Maintain existing tests -- Update documentation as needed - -## Decision Making - -### Minor Changes -- Can be made by any maintainer -- Include bug fixes, documentation updates, dependency updates - -### Major Changes -- Require discussion in issues or pull requests -- Include new features, architectural changes, API changes -- Need approval from at least 2 maintainers - -### Breaking Changes -- Require RFC (Request for Comments) process -- Need approval from majority of maintainers -- Must include migration guide - -## Code of Conduct - -All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers. - -## Communication - -- **Issues**: For bug reports and feature requests -- **Discussions**: For questions and general discussion -- **Pull Requests**: For code contributions - -## Licensing - -All contributions are made under the terms of the repository's LICENSE file. -By submitting a pull request, you agree to license your contributions accordingly. - ---- - -*Last updated: 2026-07-18* diff --git a/SECURITY.adoc b/SECURITY.adoc new file mode 100644 index 0000000..3081ece --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,16 @@ +== Security Policy + +=== Reporting a Vulnerability + +If you discover a security vulnerability, please report it responsibly: + +* *Email:* j.d.a.jewell@open.ac.uk +* *Do NOT* open a public issue for security vulnerabilities + +We will acknowledge receipt within 48 hours and provide a detailed +response within 7 days. + +=== Supported Versions + +Only the latest release on the `+main+` branch is supported with +security updates. diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index b2dacab..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,15 +0,0 @@ - -# Security Policy - -## Reporting a Vulnerability - -If you discover a security vulnerability, please report it responsibly: - -- **Email:** j.d.a.jewell@open.ac.uk -- **Do NOT** open a public issue for security vulnerabilities - -We will acknowledge receipt within 48 hours and provide a detailed response within 7 days. - -## Supported Versions - -Only the latest release on the `main` branch is supported with security updates. diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc new file mode 100644 index 0000000..ee1737f --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,39 @@ +== Test Requirements — Tropical Resource Typing For Protocols + +=== CRG Grade: C — ACHIEVED 2026-04-04 + +This is a documentation/PDF repository (no compiled source code). CRG +Grade C for this category means validating artefact integrity and +content conventions. + +[width="100%",cols="34%,19%,22%,25%",options="header",] +|=== +|Category |File |Tests |Status +|Unit |`+tests/validate.test.ts+` |3 file existence checks |PASS + +|Smoke |`+tests/validate.test.ts+` |4 content/size checks |PASS + +|P2P / property |`+tests/validate.test.ts+` |UTF-8 validity + PDF magic +bytes |PASS + +|E2E |`+tests/validate.test.ts+` |3 full validation chains |PASS + +|Contract |`+tests/validate.test.ts+` |2 content convention checks |PASS + +|Aspect |`+tests/validate.test.ts+` |2 no-placeholder + filename checks +|PASS + +|Benchmark |`+tests/validate.test.ts+` |text-file scan timing baseline +|PASS (0.4ms) +|=== + +Total: 17 tests, 0 failures. + +=== Running Tests + +[source,bash] +---- +deno task test +# or directly: +deno test --allow-read tests/ +---- diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md deleted file mode 100644 index 3c1ab92..0000000 --- a/TEST-NEEDS.md +++ /dev/null @@ -1,26 +0,0 @@ -# Test Requirements — Tropical Resource Typing For Protocols - -## CRG Grade: C — ACHIEVED 2026-04-04 - -This is a documentation/PDF repository (no compiled source code). CRG Grade C -for this category means validating artefact integrity and content conventions. - -| Category | File | Tests | Status | -|----------|------|-------|--------| -| Unit | `tests/validate.test.ts` | 3 file existence checks | PASS | -| Smoke | `tests/validate.test.ts` | 4 content/size checks | PASS | -| P2P / property | `tests/validate.test.ts` | UTF-8 validity + PDF magic bytes | PASS | -| E2E | `tests/validate.test.ts` | 3 full validation chains | PASS | -| Contract | `tests/validate.test.ts` | 2 content convention checks | PASS | -| Aspect | `tests/validate.test.ts` | 2 no-placeholder + filename checks | PASS | -| Benchmark | `tests/validate.test.ts` | text-file scan timing baseline | PASS (0.4ms) | - -Total: 17 tests, 0 failures. - -## Running Tests - -```bash -deno task test -# or directly: -deno test --allow-read tests/ -``` diff --git a/TOPOLOGY.md b/TOPOLOGY.adoc similarity index 52% rename from TOPOLOGY.md rename to TOPOLOGY.adoc index ef95464..41ef033 100644 --- a/TOPOLOGY.md +++ b/TOPOLOGY.adoc @@ -1,15 +1,16 @@ - - +== TOPOLOGY.md — tropical-resource-typing -# TOPOLOGY.md — tropical-resource-typing +=== Purpose -## Purpose +Research project exploring tropical mathematics and resource-aware type +systems for functional programming. Investigates linear and +substructural types through the lens of tropical algebra, enabling novel +optimizations and resource management strategies. Part of +nextgen-languages ecosystem’s type system research. -Research project exploring tropical mathematics and resource-aware type systems for functional programming. Investigates linear and substructural types through the lens of tropical algebra, enabling novel optimizations and resource management strategies. Part of nextgen-languages ecosystem's type system research. +=== Module Map -## Module Map - -``` +.... tropical-resource-typing/ ├── src/ # Research implementation │ ├── tropical/ # Tropical algebra foundations @@ -19,19 +20,19 @@ tropical-resource-typing/ ├── papers/ # Academic papers and proofs ├── examples/ # Case studies and applications └── tests/ # Validation suite -``` +.... -## Data Flow +=== Data Flow -``` +.... [Source Program] ──► [Parser] ──► [Tropical Type Inference] ──► [Resource Analysis] ↓ [Optimization] ──► [Compiled Output] -``` +.... -## Research Areas +=== Research Areas -- Tropical algebraic semantics for resource types -- Substructural type systems with multiplicative intuitionistic logic -- Resource consumption prediction and optimization -- Integration with formal verification frameworks +* Tropical algebraic semantics for resource types +* Substructural type systems with multiplicative intuitionistic logic +* Resource consumption prediction and optimization +* Integration with formal verification frameworks diff --git a/audits/audit-pa021-comment-text-fp-2026-05-26.adoc b/audits/audit-pa021-comment-text-fp-2026-05-26.adoc new file mode 100644 index 0000000..81f2f5a --- /dev/null +++ b/audits/audit-pa021-comment-text-fp-2026-05-26.adoc @@ -0,0 +1,64 @@ +== Audit: PA021 ProofDrift comment-text false positives + +*Auditor*: Jonathan D.A. Jewell *Date*: 2026-05-26 *Scope*: 4 +`+panic-attack assail+` PA021 ProofDrift findings flagging `+sorry+` / +`+oops+` inside Isabelle `+\...\+` or `+@{text ...}+` +comment-text blocks. *Cross-reference*: campaign tracker +https://github.com/hyperpolymath/panic-attack/issues/32[hyperpolymath/panic-attack#32], +detector bug +https://github.com/hyperpolymath/panic-attack/issues/43[hyperpolymath/panic-attack#43]. +*Registry*: `+audits/assail-classifications.a2ml+`. + +=== Detector bug + +PA021 scans for the Isabelle keywords `+sorry+` (unfinished proof) and +`+oops+` (abandoned proof). The detector reads the raw text and counts +every occurrence, including those inside `+\...\+` comment +antiquotations and `+@{text ...}+` markup. This produces false positives +on files whose header docstrings _assert the absence_ of those keywords. + +`+grep -nE '\bsorry\b'+` against each of the 4 flagged files shows the +keyword exists *only* inside comment text. There are no `+sorry+` or +`+oops+` tactics in any actual proof. + +=== §1 — "`All proofs are complete — zero `+sorry+``" headers + +* `+Tropical_Kleene.thy:663+`: +`+All proofs are complete — zero @{text sorry}.+` +* `+Tropical_Matrices_Clean.thy:24+`: +`+All proofs are complete — zero @{text sorry}.+` + +Both files use the same documentation idiom. PA021 counted the literal +keyword inside the `+@{text ...}+` antiquotation as a real `+sorry+`. + +=== §2 — Echidna oops-handoff marker + +`+Tropical_Ordinal.thy:15+`: +`+with \oops\ are the ones we want ECHIDNA to evaluate: each is either closeable by direct automation or surfaces a missing piece of the design.+` + +This is documentation describing the file’s _intended workflow_ (echidna +evaluates each oops). The detector matched the keyword inside the +`+\...\+` block. + +=== §3 — Closure-completion attestation + +`+Tropical_CNO.thy:29+`: `+All sorry placeholders have been closed.+` + +Plain prose attesting that the file has been cleaned up. Detector +matched the keyword in plain text. + +=== Verification + +`+grep -nE '\bsorry\b' +` and `+grep -nE '\boops\b' +` for +all 4 files returns only comment-context lines. `+isabelle build+` is +not exercised here (proof source unchanged); the classifications are +pure metadata. + +=== Anti-gameability + +The registry is a separate file from the .thy proof source. Adding a +real `+sorry+` or `+oops+` to a proof in any of these files would NOT be +classified by this audit — only the specific comment-text matches above +are suppressed. Real proof debts (if introduced) remain visible. + +Refs hyperpolymath/panic-attack#32, hyperpolymath/panic-attack#43. diff --git a/audits/audit-pa021-comment-text-fp-2026-05-26.md b/audits/audit-pa021-comment-text-fp-2026-05-26.md deleted file mode 100644 index 4a5a695..0000000 --- a/audits/audit-pa021-comment-text-fp-2026-05-26.md +++ /dev/null @@ -1,47 +0,0 @@ - - -# Audit: PA021 ProofDrift comment-text false positives - -**Auditor**: Jonathan D.A. Jewell -**Date**: 2026-05-26 -**Scope**: 4 `panic-attack assail` PA021 ProofDrift findings flagging `sorry` / `oops` inside Isabelle `\...\` or `@{text ...}` comment-text blocks. -**Cross-reference**: campaign tracker [hyperpolymath/panic-attack#32](https://github.com/hyperpolymath/panic-attack/issues/32), detector bug [hyperpolymath/panic-attack#43](https://github.com/hyperpolymath/panic-attack/issues/43). -**Registry**: `audits/assail-classifications.a2ml`. - -## Detector bug - -PA021 scans for the Isabelle keywords `sorry` (unfinished proof) and `oops` (abandoned proof). The detector reads the raw text and counts every occurrence, including those inside `\...\` comment antiquotations and `@{text ...}` markup. This produces false positives on files whose header docstrings *assert the absence* of those keywords. - -`grep -nE '\bsorry\b'` against each of the 4 flagged files shows the keyword exists **only** inside comment text. There are no `sorry` or `oops` tactics in any actual proof. - -## §1 — "All proofs are complete — zero `sorry`" headers - -- `Tropical_Kleene.thy:663`: `All proofs are complete — zero @{text sorry}.` -- `Tropical_Matrices_Clean.thy:24`: `All proofs are complete — zero @{text sorry}.` - -Both files use the same documentation idiom. PA021 counted the literal keyword inside the `@{text ...}` antiquotation as a real `sorry`. - -## §2 — Echidna oops-handoff marker - -`Tropical_Ordinal.thy:15`: `with \oops\ are the ones we want ECHIDNA to evaluate: each is either closeable by direct automation or surfaces a missing piece of the design.` - -This is documentation describing the file's *intended workflow* (echidna evaluates each oops). The detector matched the keyword inside the `\...\` block. - -## §3 — Closure-completion attestation - -`Tropical_CNO.thy:29`: `All sorry placeholders have been closed.` - -Plain prose attesting that the file has been cleaned up. Detector matched the keyword in plain text. - -## Verification - -`grep -nE '\bsorry\b' ` and `grep -nE '\boops\b' ` for all 4 files returns only comment-context lines. `isabelle build` is not exercised here (proof source unchanged); the classifications are pure metadata. - -## Anti-gameability - -The registry is a separate file from the .thy proof source. Adding a real `sorry` or `oops` to a proof in any of these files would NOT be classified by this audit — only the specific comment-text matches above are suppressed. Real proof debts (if introduced) remain visible. - -Refs hyperpolymath/panic-attack#32, hyperpolymath/panic-attack#43. diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc new file mode 100644 index 0000000..6d8b4d1 --- /dev/null +++ b/docs/tech-debt-2026-05-26.adoc @@ -0,0 +1,71 @@ +== Tech-Debt Audit — tropical-resource-typing — 2026-05-26 + +*Source:* estate-wide automated scan 2026-05-26. *Companion:* +https://github.com/hyperpolymath/standards/tree/main/docs/audits[`+hyperpolymath/standards+` +2026-05-26-estate-*-debt audits]. *Combined severity:* `+LOW+`. + +This file records the _raw findings_ — it does not by itself fix the +debt. Each section ends with a '`Recommended next move`' line; closing +the debt is follow-up work. + +=== 1. Proof debt + +No proof-bearing files (`+*.v+`, `+*.lean+`, `+*.agda+`, `+*.idr+`, +`+*.idr2+`, `+*.fst+`, `+*.dfy+`, `+*.tla+`, `+*.ads+`, `+*.adb+`) found +in this repo. + +*Recommended next move:* none. + +=== 2. Licence debt + +[cols=",",options="header",] +|=== +|Field |Value +|LICENSE file |`+LICENSE+` +|SPDX header |`+MPL-2.0+` +|Manifest licence |`+NONE+` +|Body classifier |`+Palimp-MPL-2.0+` +|Severity |`+ok+` +|=== + +*Recommended next move:* none for licence. + +=== 3. Documentation debt + +[cols=",",options="header",] +|=== +|Field |Value +|README lines |5 +|`+docs/+` files |9 +|`+docs/+` LoC |2573 +|CHANGELOG.md |N +|CONTRIBUTING.md |Y +|CODE_OF_CONDUCT.md |N +|SECURITY.md |Y +|Severity |`+LOW+` +|=== + +*Recommended next move:* `+docs/+` has only 9 file(s). Aim for ≥10 +organised docs (architecture, usage, contributing-guide, +troubleshooting, design-decisions). The user’s bar for a +"`heavily-developed and well-organised wiki`" is ≥10 files with topical +organisation. + +Additionally: *CHANGELOG.md is missing.* 65% of estate repos lack one — +adopting a CHANGELOG (or auto-generating via `+git-cliff+`) is a +recommended estate-wide follow-up. + +=== Cross-references + +* Estate proof-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md+` +* Estate licence-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md+` +* Estate documentation-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md+` + +''''' + +🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). +This file is informational — closing the debt is follow-up work owned by +the maintainer. diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md deleted file mode 100644 index cb8b4ab..0000000 --- a/docs/tech-debt-2026-05-26.md +++ /dev/null @@ -1,57 +0,0 @@ - - -# Tech-Debt Audit — tropical-resource-typing — 2026-05-26 - -**Source:** estate-wide automated scan 2026-05-26. -**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits). -**Combined severity:** `LOW`. - -This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work. - -## 1. Proof debt - -No proof-bearing files (`*.v`, `*.lean`, `*.agda`, `*.idr`, `*.idr2`, `*.fst`, `*.dfy`, `*.tla`, `*.ads`, `*.adb`) found in this repo. - -**Recommended next move:** none. - -## 2. Licence debt - -| Field | Value | -|---|---| -| LICENSE file | `LICENSE` | -| SPDX header | `MPL-2.0` | -| Manifest licence | `NONE` | -| Body classifier | `Palimp-MPL-2.0` | -| Severity | `ok` | - -**Recommended next move:** none for licence. - -## 3. Documentation debt - -| Field | Value | -|---|---| -| README lines | 5 | -| `docs/` files | 9 | -| `docs/` LoC | 2573 | -| CHANGELOG.md | N | -| CONTRIBUTING.md | Y | -| CODE_OF_CONDUCT.md | N | -| SECURITY.md | Y | -| Severity | `LOW` | - -**Recommended next move:** `docs/` has only 9 file(s). Aim for ≥10 organised docs (architecture, usage, contributing-guide, troubleshooting, design-decisions). The user's bar for a "heavily-developed and well-organised wiki" is ≥10 files with topical organisation. - -Additionally: **CHANGELOG.md is missing.** 65% of estate repos lack one — adopting a CHANGELOG (or auto-generating via `git-cliff`) is a recommended estate-wide follow-up. - -## Cross-references - -- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` -- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` -- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` - ---- - -🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer.