rocq/theories/Cycle.v
A loop whose trip count is the input, proved never to panic: rocq/programs/cycle.c, the sum of n longs read in turn from a read-only global array of four, xs[i % 4] for i from 0 while i < n, for every int n (CycleCode.v, checked current by rocq/programs.sh). The loop runs up to 2^31 - 1 times, so no list of runs covers it, as Prefix.v's six runs cover its loop.
The proof is Floyd's: an assertion at each point of the function (cycle_assert) says what the temporaries hold there, and one step from any configuration where the assertion holds reaches a point where its assertion holds, or ends without a failure (cycle_safe). Each step is taken by its rule from StepRules.v (Symbolic.v's take_step): the rule of the instruction at the point, with its premises (a temporary's value, an op on words, an access check) proved one by one. The loop's assertion is that its index i is between 0 and 2^31 - 1: then i % 4 is between 0 and 3, the access is in bounds, and i + 1 does not wrap. The index stays below 2^31 because the loop continues only while i < n, and no int n is above 2^31 - 1. Panics.v's never_panics_by_invariant turns that into never_panics.
Decisions
| Decision | Why |
|---|---|
| assertions at every point, not only at the loop's head | the machine's invariant must hold in every state a run reaches, and the safepoint at the poll edge may act in the middle of the loop |
| an assertion names only the temporaries read later, each with a range | the environment stays abstract, so the proof holds whatever else it holds, in the first iteration and in every later one |
| the input is any list whose first word is an integer | the model reads an int parameter modulo 2^32, so no range on the word is needed; a pointer there is outside the C type |
memory as in Sum.v's mem_ok | the array is laid out where sum.c's is, and the program only reads it |
Integer arithmetic on an unknown stays folded when a step is computed (Symbolic.v).
The program
The checked module, decoded from the fixture cycle_term (cycle_decodes).
The fixture decodes to cycle_module.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The function cycle, the module's first item.
The module's globals: the array xs, laid out as in Sum.v, and the function cycle.
The module's initial memory.
Laying out the module succeeds, with cycle_globals and cycle_mem.
Explore proof 3 tactics
Initial goal
assert H : option_mapfst initial_memorycycle_module = Somecycle_globals by vm_compute ; reflexivity
unfold cycle_mem
destruct initial_memorycycle_module as g m | ; inversion H ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The genv of the module with any free; the program calls none.
cycle is a function of the core subset in the module.
Explore proof 3 tactics
Initial goal
intros free
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Any arguments whose first word is the integer n start cycle at its entry block with n as its parameter v0.
Explore proof 1 tactics
The points
Block l of cycle after its first j instructions.
Every point of cycle, numbered: the entry block start; the loop's head L4 (entered from start or from the body, then its comparison of i with n, then its branch); the loop's body L5, before each of its nine instructions and before its jump back, which polls; and the exit L7, which returns the sum.
The assertions
The temporary x holds a pointer into xs with 8 bytes after it: an address from the array's start to its last long, with the array's read-only capability.
What holds after the first j instructions of the body: the sum pr.1, the index pr.2 with room to add one, and each temporary the body has assigned and reads later: the array's pointer v12, i % 4 (v14, then v15 as a long), the offset v16, the pointer v17 and its checked proof chk0, the long loaded v18, the new sum v19 and the next index v21.
What holds at point k of cycle_points, besides the input. At the loop's head entered from the body, the next index and sum; before the comparison, the index i and the sum; at the branch, also the comparison's answer, and where it is true, that i + 1 does not reach 2^31, since i < n; in the body, body_assert; at the exit, the sum.
A configuration of cycle where the assertions hold: at point k, with no caller, the input v0 an integer, the assertion of k, and a memory that is mem_ok for the array.
Each step
Unfold the assertion at a known point.
Unfold the assertion at a known point in the hypothesis H.
The point of the next configuration is point n of cycle_points or a later one: find it by computing each in turn.
The next configuration is in cycle_inv: at its point, with the memory unchanged, and the facts shown.
One point of cycle_safe: the point from Hk, an index into the points pts, the assertion Ha taken apart, the step taken by its rule (take_step), and its result shown safe.
One step from a configuration where the assertions hold is safe_step for them.
Proof 18 steps Qed
A call with an integer first argument starts where the assertions hold, with any fuel.
Explore proof 6 tactics
Initial goal
intros n fuel
exists O, EnterTAtom"start" None, TAtom"v0", WIntn
split ; reflexivity |
split ; vm_compute ; reflexivity |
split ; split ; reflexivity | vm_compute ; reflexivity |
split ; exists n ; split ; reflexivity | exact I | exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Over any runtime
cycle never panics under the runtime R.
What R does at a safepoint keeps the assertions: it changes only the memory, and keeps mem_ok (Sum.v's mem_ok_safepoint).
Explore proof 8 tactics
Initial goal
intros c s s′ m′ k & pt & e & Ec & Hk & Hm & Hin & Ha Hsp
exists k, pt, e
rewrite Ec at 1
unfold P.RM.with_mem ; cbn [ c_frame c_callers c_mem c_fuel ]
split ; reflexivity |
split ; exact Hk |
split ; | split ; assumption
eapply S.mem_ok_safepoint ; eassumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
cycle never panics: for every input whose first word is an integer, under the runtime R, with any fuel, no state of its run fails, however many times the loop runs.
Explore proof 12 tactics
Initial goal
apply P.never_panics_by_invariant_ _ _ cycle_globals cycle_mem cycle_fn cycle_inv
5 openfocused goal
focused goal
focused goal
focused goal
–exact cycle_initial
4 opendeferred goal
deferred goal
deferred goal
deferred goal
–apply cycle_find
3 opendeferred goal
deferred goal
deferred goal
–intros xs n & rest & →
3 opendeferred goal
deferred goal
eexists
4 opendeferred goal
deferred goal
split ; apply cycle_call_frame |
3 opendeferred goal
deferred goal
intros fuel
3 opendeferred goal
deferred goal
apply cycle_start
2 opendeferred goal
deferred goal
–intros c s Hc _
2 opendeferred goal
apply cycle_safe , Hc
deferred goal
–intros c s s′ m′ Hc _ _ Hsp
eapply cycle_safepoint ; eassumption
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The theorem for the interpreter's runtime.