Findings · Agent control
A capability meter never exceeds its cap over every concurrent interleaving of charge operations, proved in Iris concurrent separation logic for any cap and any finite list of operations.
Evidence
The property is stated as adequacy of a program that forks one compare-and-swap charge thread per element of the list onto a single shared cell. Adequacy quantifies over every configuration reachable by stepping, which is every thread schedule, so “over all interleavings” is the statement, not a gloss on it. The theorem closes with Qed and the audited theorems report no axioms of any kind, stronger than “no added axioms,” since it means no foundational axiom either.
Sample. Universal over the cap, any finite operation list, any initial state, and all thread schedules. The 29 audited theorems are closed under the global context: no user axioms and no foundational axioms.
Boundary
It is terminal-observation safety, the value the driver reads is within the cap, not an all-intermediate-state invariant, and it carries no liveness or wait-freedom. The kernel check was not re-run in this pass; axiom-freedom rests on the committed assumptions audit plus a live search finding no admitted goals.
Independent reproduction. None known.
Reproduction
eval $(opam env --switch=capctl-iris) && make verify- Toolchain
- The Rocq Prover rocq-core 9.2.0, rocq-iris 4.5.0, rocq-stdpp 1.13.0, OCaml 5.2.0
- Expected output
- all files compile to Qed; the assumptions audit diffs clean (29 lines, each 'Closed under the global context')
- Claim stated at
- repowazdogz-droid/capctl-iris · iris/theories/MeterConcSafety.v:32-39
- Verified at
- repowazdogz-droid/capctl-iris@5e9284a0 (2026-07-20)
This pass. Confirmed by source read at 5e9284a0 (theorem, Qed, committed assumptions audit, and a live grep finding no admitted goals); the Rocq kernel was not re-run this pass.
Artifact: repowazdogz-droid/capctl-iris