capctl-iris

A machine-checked concurrent capability meter in Iris / Rocq (Coq) — a shared counter that governs cumulative resource consumption against a cap and never exceeds it: sequentially, concurrently (over all thread interleavings), logically atomically, and across a finite family of independently-capped resources. Every headline result is a closed, axiom-free theorem about the HeapLang operational semantics (Closed under the global context; no Admitted, no project-authored axioms).

Layout

• iris/ — the complete Iris/Rocq development: 15 theory files, the Print Assumptions audit, build gates, and the reviewer documentation. Start at iris/README.md.
• tla/ — the TLA+ model (AuthRace.tla + two configs) that the Iris project's make verify re-checks, to exhibit the concurrent TOCTOU race the Iris proof excludes.
• lean/ — the sequential Lean 4 proof (Trajectory.lean, core Lean only: no Mathlib, no lake) with its toolchain pin. Three theorems, each kernel-checked and axiom-free.

The Lean, TLA+ and Iris developments are three separate formalisations of related properties in three tools. Each is re-checked independently in CI; no machine-checked correspondence between them is claimed (see iris/BRIDGE.md).

Build & verify

Requires the pinned toolchain (see iris/environment.lock: the Rocq Prover 9.2.0 / rocq-iris 4.5.0 / rocq-stdpp 1.13.0), from inside its opam switch:

cd iris
make clean && make verify

Expected final line: FLOOR A+B+C VERIFY (+D logatom +E multi) : all applicable checks PASSED. The TLA+ step downloads the pinned TLA+ Tools (v1.7.4) on demand, verifies its SHA-256 against tla/tla2tools.jar.sha256, and re-checks the bundled tla/ model; it skips cleanly if there is no network or no JDK.

Reviewer entry points

iris/SCOPE.md (what is and isn't claimed) → iris/THEOREM-INDEX.md (every theorem + dependencies) → iris/CLAIMS-AUDIT.md → iris/TCB.md (trusted base) → iris/ARCHITECTURE.md.

Verifying the Lean leg

cd lean && lean Trajectory.lean

with the toolchain pinned in lean/lean-toolchain (install via elan). Expected output — three lines, one per theorem:

'CapabilityControl.per_step_insufficient' does not depend on any axioms
'CapabilityControl.cap_does_not_bound_aggregate' does not depend on any axioms
'CapabilityControl.cumulative_monitor_sound' does not depend on any axioms

Author

Warren Smith — repowazdogz@gmail.com (GitHub @repowazdogz-droid).

Provenance & licence

Extracted from a larger, private capability-control research workspace — see PROVENANCE.md for exactly what is and isn't included. Licensed under the MIT License (LICENSE). The TLA+ Tools jar is not committed here; the verification step downloads the pinned official release (v1.7.4, © Microsoft Research, MIT-licensed) and verifies its SHA-256 (tla/tla2tools.jar.sha256).