PROVEN
Finding · authorise
A limit on what an agent may do was proved to hold no matter how concurrent operations interleave.
§ 1
The record
FINDING · concurrent-capability-bound-over-interleavingsauthorise
A limit on what an agent may do was proved to hold no matter how concurrent operations interleave.
- Claim
- 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.
- Status
- PROVEN Follows from stated premises inside a named frame.
- Subject
- A Rocq/Iris model of a concurrent capability meter (model). built for the study
- Frame
- Any cap, any finite list of charge operations, every interleaving; terminal-observation safety only.
- Method
- Adequacy over every reachable configuration in Iris concurrent separation logic.
- Oracle
- The Rocq kernel; Print Assumptions committed and diffed in CI.
- Negative control
- Present Floor E: an explicit counterexample showing per-key safety does not certify a tighter cross-key aggregate bound.
- Limitation
- 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.
- Source
- repowazdogz-droid/capctl-iris @ 5e9284a0
- Reproduce
eval $(opam env --switch=capctl-iris) && make verify
- Independent reproduction
- None known.
§ 2
Where this sits
This finding answers Individually compliant is not collectively safe and supports the AUTHORISE stage of the operating method.