Skip to content

FOUNDATION_CONTRACT.md

Latest commit

 

History

History
147 lines (115 loc) · 6.56 KB

FOUNDATION_CONTRACT.md

File metadata and controls

147 lines (115 loc) · 6.56 KB
Raw

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.