rocq/theories/BufferLogic.v
rocq/programs/buffer.c through the program logic of Logic.v.
Buffer.v proves buffer never panics by an assertion at each of its 32 points, checked one symbolic step at a time. This file proves the same theorem (buffer_never_panics) in Iris: the allocation hands the program the new object's pieces (obj), which obj_buf splits into its life and four 8-byte cells (cells); each loop is a Löb induction at the point after its head's phis, carrying the life and the cells; each check lends the life back for one step, and each access takes the one cell it reaches (cells_at). The values the cells hold play no part. Every step is taken by its rule from Logic.v, its premises discharged by Symbolic.v's tactics on the premise alone.
Integer arithmetic on an unknown stays folded when a premise is computed (Symbolic.v).
The blocks, computed once
Block l of buffer, or an empty one.
The entry block, which allocates the buffer.
The fill loop's head.
The fill loop's body.
The sum loop's head.
The sum loop's body.
The exit.
buffer has its entry block.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
buffer has the fill loop's head.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
buffer has the fill loop's body.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
buffer has the sum loop's head.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
buffer has the sum loop's body.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
buffer has its exit.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 2 tactics
Environments
The buffer
The buffer's region: a 32-byte live heap object at b.
Taking a step
Prove an address premise: an alignment to 1 holds at once; the wraps of raw_address are dropped where arithmetic proves them the identity, then arithmetic.
Unfold the blocks that a frame's point names.
Prove one pure premise of a rule of Logic.v: by computation for the op's classes, by a fact for a block and a return class, by addr for an address, by compute_premise for a word, trivially for what the world interpretation must keep (there is no world), and by arithmetic for a bound.
Over any runtime
The proof over the runtime R.
The genv of the module, whose free is R's.
The expressions of its language.
The rules as tactics
A let of an op that reads no memory, by wp_let.
A branch, by wp_branch, its target computed.
Entering a block, by wp_enter, its body unfolded.
A goto, by wp_goto.
The buffer's four 8-byte cells at b, holding any values.
The cell at offset 8 k, for k from 0 to 3, can be taken from the cells and given back holding anything.
Explore proof 3 tactics
Initial goal
intros Hk
iIntros (%v0 & %v1 & %v2 & %v3 & H0 & H1 & H2 & H3)
assert k = 0 ∨ k = 1 ∨ k = 2 ∨ k = 3 as → | → | → | → by lia ; cbn [ Z.mul ] ; iExists v0 ; iFrame H0 | iExists v1 ; iFrame H1 | iExists v2 ; iFrame H2 | iExists v3 ; iFrame H3 ; iIntros w Hw ; rewrite / cells ; iExists _, _, _, _ ; iFrame
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A new 32-byte object, split into its life and its four cells, which hold zero; the aux slots are dropped.
Explore proof 7 tactics
Initial goal
rewrite / obj / live / cells / icell
assert E : obj_psbase heap_req16 32 = PLivebase, VLivebuf_regbase ++ cellbase 0 0 ++ cellbase 8 0 ++ cellbase 16 0 ++ cellbase 24 0 ++ λi ⇒ PAuxbase i, VAuxCNone <$> seqZ0 32 by reflexivity
rewrite E ! pts_app
iIntros (Hl & H0 & H8 & H16 & H24 & _)
iFrame Hl
iExists 0, 0, 0, 0
iFrame
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
What both loops know of the environment e: v4 holds the buffer's own pointer, its base b positive, 16-aligned and ending within the address space.
The sum loop, from the point after its head's phis: with pr.3 an int j from 0 below 2^31, pr.2 any long, v0 the input n, owning the buffer, the run is safe. By Löb induction; each iteration reads the cell j mod 4.
Proof 29 steps Qed
The fill loop, from the point after its head's phi: with pr.1 an int i from 0 to 4 and v0 the input n, owning the buffer, the run is safe. By Löb induction; each iteration writes the cell i; when i reaches 4 the sum loop starts with j and the sum 0.
Proof 27 steps Qed
buffer called with the int n is safe.
Explore proof 10 tactics
Initial goal
buf_facts
wp_enter_
iApply wp_alloc ; first side | iNext ; iIntros base Hb0 & Hb1 & Hb2 Hobj ; gen_env
change req_alignheap_req16 32 with 16 in Hb1
change req_extentheap_req16 32 with 32 in Hb2
iDestruct obj_buf with Hobj as [Hlv Hc]
wp_goto_
wp_enter_
iApply fill_loopn base $! _ 0 with [%] Hlv Hc
repeat split ; try eassumption ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The resources the proof uses: invariants and the ghost heap.
bufΣ has invariants.
Explore proof 2 tactics
bufΣ has the ghost heap of pieces.
Explore proof 2 tactics
buffer never panics: for every input whose first word is an int, with any fuel, no state of its run fails, whatever base its buffer gets. Proved by Iris adequacy (heap_never_panics) from buffer_spec.
Explore proof 11 tactics
Initial goal
apply heap_never_panicsbufΣ buffer_module TAtom"buffer" _ buffer_globals buffer_mem buffer_fn
4 openfocused goal
–exact buffer_initial
3 opendeferred goal
–exact buffer_findR.free
2 opendeferred goal
–intros b1 r1 b2 r2 E _
2 openvm_compute in E
2 opendiscriminate E
–intros xs n & rest & →
eexists
2 opensplit ; apply buffer_call_frame |
intros HinvG HheapG
apply buffer_spec
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The theorem for the interpreter's runtime.
buffer.c never panics under the interpreter's runtime, by the program logic.
Explore proof 1 tactics
Initial goal
exact InterpBufferLogic.buffer_never_panics
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.