Projects · Agent control · Research prototype · PROVEN
capctl-iris
What this establishes
That a capability meter never exceeds its cap over every concurrent interleaving of charge operations, in Iris concurrent separation logic, for any cap and any finite operation list.
What this does not establish
It is terminal-observation safety, the value the driver reads is within the cap, not an all-intermediate-state invariant, and carries no liveness or wait-freedom. Floor E shows per-key safety does not certify a tighter cross-key aggregate bound. There is no machine-checked link to the TLA+ model or the Lean parent.
Trusted base
The Rocq kernel (rocq-core 9.2.0). The 29 audited theorems are each closed under the global context: no user axioms and no foundational axioms, which is stronger than 'no added axioms'. The proofs are stated over a few Iris and heap_lang definitions, the operational semantics and the adequacy bridge, which are kernel-checked, not axiomatic.
Method
The concurrent driver forks one compare-and-swap charge thread per element onto a single shared cell; safety is stated as adequacy, which quantifies over every reachable configuration, that is, every thread schedule.
Result
The headline theorem conc_meter_never_exceeds_cap closes with Qed; the assumptions audit reports 29 theorems each closed under the global context; a live search finds no admitted goals. The kernel was not re-run in the evidence pass, so axiom-freedom rests on the committed audit.
Negative controls. Floor E per_key_misses_tight_global_bound is an existential counterexample: per-key caps alone cannot certify a separately chosen tighter global budget.
Reproduce
eval $(opam env --switch=capctl-iris) && make verify- Toolchain
- The Rocq Prover rocq-core 9.2.0, rocq-iris 4.5.0, rocq-iris-heap-lang 4.5.0, rocq-stdpp 1.13.0, OCaml 5.2.0
- Verified at
- repowazdogz-droid/capctl-iris@5e9284a0 (2026-07-20)
This pass. Confirmed by source read at 5e9284a0 (theorem statement, Qed, the committed assumptions audit, and a live grep finding no admitted goals); the Rocq kernel was not re-run this pass.
Independent reproduction
None known.
Prior art and positioning
Iris concurrent separation logic and its adequacy theorem; capability and authority bounds. The contribution is the concurrent meter bound and the audited axiom-free trusted base.