rocq/spikes/ListSumLogic.v
Spike: spikes/listsum.c through the program logic of Logic.v.
sum gets an Iris Hoare triple that hands the list back and states its result (sum_spec): from lst p xs, its run returns the sum of xs modulo 2^64 (list_sum) and the list is still there. listsum builds the list and calls sum through that triple (wp_call_bind), then drops the list. Each loop is a Löb induction at the point after its head's phis; sum's carries the walked prefix as a list segment (lseg). Every step is taken by its rule from Logic.v, its premises discharged by Symbolic.v's tactics on the premise alone; step is never reduced on a whole configuration.
Integer arithmetic on an unknown stays folded when a premise is computed (Symbolic.v).
The blocks, computed once
Block l of the function f, or an empty one.
sum's entry block.
sum's loop head.
sum's loop body.
sum's exit.
listsum's entry block.
listsum's loop head.
listsum's loop body.
listsum's exit, the call of sum.
sum 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
sum has its loop head.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
sum has its loop body.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
sum has its exit.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
listsum 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
listsum has its loop head.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
listsum has its loop body.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
listsum has its exit.
Explore proof 2 tactics
Initial goal
vm_compute
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
sum returns a long.
Explore proof 2 tactics
listsum returns a long.
Explore proof 2 tactics
Environments
Replace each environment put k v e of the goal, e a variable, by a new variable, with what each name looks up to in it.
Nodes
A node's region: a 16-byte live heap object at b.
p is the own pointer of a node at b: positive, 16-aligned, and fitting the address space.
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 of the module 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.
Sums
The sum of the values xs modulo 2^64, as sum adds longs.
A sum is a 64-bit unsigned integer.
Explore proof 2 tactics
Initial goal
apply Z.mod_pos_bound
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Adding one more value, wrapped as sum's loop adds it.
Explore proof 11 tactics
Initial goal
unfold list_sum
rewrite fold_right_app
cbn [ fold_right ]
assert E : ∀zs a, fold_rightZ.add a zs = fold_rightZ.add 0 zs + a
2 openfocused goal
{induction zs as | z zs IH ; intros a ; cbn [ fold_right ] ; lia |
2 opendeferred goal
rewrite IH
2 opendeferred goal
lia
deferred goal
rewrite E
rewrite <- Zplus_mod
f_equal
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
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.
sum called with the pointer p: its entry frame.
The list from p holds the values xs: null for none; otherwise p is its node's own pointer (node_ok), and the node is live, holds the next pointer at offset 0 and the value at offset 8, and the rest of the list follows from the next pointer.
The list segment from p to q holds the values ys: the nodes of lst, ending at q instead of null.
A list of one value or more, unfolded once.
Explore proof 1 tactics
Source script
A segment to q and the node at q make a segment to the node's next pointer.
Explore proof 12 tactics
Initial goal
intros Hq
revert p
induction ys as | y′ ys IH ; intros p ; cbn [ lseg app ]
2 openfocused goal
–iIntros → Hl Hp Hi
2 opendeferred goal
iExists b, nx
2 opendeferred goal
by iFrame
deferred goal
–iIntros Hs Hl Hp Hi
iDestruct Hs as b′ nx′ (% & Hl′ & Hp′ & Hi′ & Hs)
iExists b′, nx′
iFrame Hl′ Hp′ Hi′
iSplit ; done |
iApply IH with Hs Hl Hp Hi
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A segment to q and the list from q make the list from p.
Explore proof 11 tactics
Initial goal
revert p
induction ys as | y ys IH ; intros p ; cbn [ lseg app ]
2 open–iIntros → Hl
2 opendeferred goal
iExact Hl
deferred goal
–iIntros Hs Hl
iDestruct Hs as b nx (% & Hlv & Hp & Hi & Hs)
cbn [ lst ]
iExists b, nx
iFrame Hlv Hp Hi
iSplit ; done |
iApply IH with Hs Hl
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
The head of a list: its address is in range, and the life of the object its capability names, if any, can be lent out.
Explore proof 16 tactics
Initial goal
destruct xs as | x xs ; cbn [ lst ]
2 openfocused goal
–iIntros →
2 opendeferred goal
cbn
2 opendeferred goal
iSplit ; iPureIntro ; lia |
2 opendeferred goal
iSplit ; done |
2 opendeferred goal
by iIntros _
deferred goal
–iIntros H
iDestruct H as b nx Hn (Hlv & Hp & Hi & Hl)
destruct Hn as → & Hb0 & Hb1 & Hb2
cbn [ ptr_addr ptr_cap live_cap ]
iSplit ; iPureIntro ; lia |
iFrame Hlv
iIntros Hlv
iExists b, nx
iFrame
done
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
sum's loop, from the point after its head's phis, with the walked prefix ys as a segment from p to q, the rest zs as the list from q, pr.1 holding q and pr.2 the prefix's sum: the run returns the whole list's sum and hands the list back. By Löb induction.
Explore proof 43 tactics
Initial goal
iLöb as IH
iIntros e q ys zs Hq Hs Hs Hl HΦ
pose proof list_sum_rangeys
destruct zs as | z zs
2 openfocused goal
–iDestruct Hl as %→
2 opendeferred goal
cbn [ sum_L3 b_insts b_jump ]
2 opendeferred goal
ls_facts
2 opendeferred goal
rewrite app_nil_r
2 opendeferred goal
wp_let_
2 opendeferred goal
wp_let_
2 opendeferred goal
wp_branch_
2 opendeferred goal
wp_enter_
2 opendeferred goal
iApply wp_ret ; first side | iNext
2 opendeferred goal
iApply HΦ
2 opendeferred goal
iDestruct lseg_lst_ _ _ [ ] with Hs [//] as H
2 opendeferred goal
rewrite app_nil_r
2 opendeferred goal
iExact H
deferred goal
–rewrite lst_cons
iDestruct Hl as b nx → & Hb0 & Hb1 & Hb2 (Hlv & Hp & Hi & Hl)
ls_facts
cbn [ sum_L3 b_insts b_jump ]
wp_let_
wp_let_
wp_branch_
wp_enter_
wp_flight_
iApply wp_check with Hlv ; first side | iNext ; iIntros Hlv ; gen_env
iApply wp_raw_load with Hlv Hi ; first side | iNext ; iIntros Hlv Hi ; gen_env
wp_let_
iApply wp_half_check with Hlv ; first side | iNext ; iIntros Hlv ; gen_env
iDestruct lst_cap with Hl as Hnr [Hcap Hl]
iApply wp_raw_load_pointer with Hlv Hp Hcap ; first side | iNext ; iIntros Hlv Hp Hcap ; iSpecialize Hl with Hcap ; gen_env
wp_goto_
wp_enter_
iApply IH $! _ nx ys ++ z zs with [%] [Hs Hlv Hp Hi] Hl [HΦ]
3 openfocused goal
focused goal
+split ; eassumption |
3 opendeferred goal
deferred goal
rewrite list_sum_snoc
3 opendeferred goal
deferred goal
eassumption
2 opendeferred goal
deferred goal
+iApply lseg_snoc with Hs Hlv Hp Hi
2 opendeferred goal
unfold node_ok
2 opendeferred goal
auto
deferred goal
+rewrite - app_assoc
iExact HΦ
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
sum's specification: called with the list from p holding xs, it returns their sum modulo 2^64 and hands the list back.
Explore proof 8 tactics
Initial goal
iIntros Φ !> Hl HΦ
ls_facts
unfold sum_frame
wp_enter_
wp_goto_
wp_enter_
iApply sum_loopp Φ $! _ p [ ] xs with [%] [//] Hl HΦ
split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
A new node's object, split into the pieces a node owns: its life, a null next pointer and a zero value; the other aux slots are dropped.
Explore proof 7 tactics
Initial goal
rewrite / obj / live / pcell / icell
assert E : obj_psbase heap_req16 16 = PLivebase, VLivenode_regbase ++ cellbase 0 0 ++ cellbase 8 0 ++ PAuxbase 0, VAuxCNone ++ λi ⇒ PAuxbase i, VAuxCNone <$> seqZ1 15 by reflexivity
rewrite E ! pts_app
iIntros (Hl & H0 & H8 & Ha & _)
iFrame Hl H8
rewrite pts_app_ cellbase 0 0
iFrame
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
listsum's loop, from the point after its head's phis: with pr.2 an int i in range, pr.1 the list's pointer h and v0 the input n, owning the list, the run is safe. By Löb induction; each iteration allocates a node, stores h and i in it, and the loop goes on with i + 1 and the longer list; at the end sum is called with the list through its triple, and the list it hands back is dropped.
Explore proof 49 tactics
Initial goal
iLöb as IH
iIntros e i h xs Hi & Hir & Hh & Hn Hl
ls_facts
pose proof ls_find_sumR.free
cbn [ ls_L4 b_insts b_jump ]
wp_let_
match goal withH : lookupTAtom"v10" _ = SomeWIntif then 1 else 0 |- _⇒destruct c eqn: Hcend
2 openfocused goal
–assert Hi1 : i + 1 < 2 ^ 31
3 openfocused goal
deferred goal
{apply Z.ltb_lt in Hc
3 opendeferred goal
deferred goal
revert Hc
3 opendeferred goal
deferred goal
destruct 2 ^ 31 ≤? n mod 2 ^ 32 eqn: Hs ; apply Z.leb_le in Hs | apply Z.leb_gt in Hs ; intros ; pose proof Z.mod_pos_boundn 2 ^ 32 ltac:lia ; lia
2 opendeferred goal
deferred goal
wp_branch_
2 opendeferred goal
wp_enter_
2 opendeferred goal
iApply wp_alloc ; first side | iNext ; iIntros base Hb0 & Hb1 & Hb2 Hobj ; gen_env
2 opendeferred goal
change req_alignheap_req16 16 with 16 in Hb1
2 opendeferred goal
change req_extentheap_req16 16 with 16 in Hb2
2 opendeferred goal
iDestruct obj_node with Hobj as (Hlv & Hp & Hi)
2 opendeferred goal
iApply wp_check with Hlv ; first side | iNext ; iIntros Hlv ; gen_env
2 opendeferred goal
iApply wp_raw_store_pointer with Hlv Hp ; first side | iNext ; iIntros Hlv Hp ; gen_env
2 opendeferred goal
wp_flight_
2 opendeferred goal
wp_let_
2 opendeferred goal
iApply wp_half_check with Hlv ; first side | iNext ; iIntros Hlv ; gen_env
2 opendeferred goal
iApply wp_raw_store with Hlv Hi ; first side | iNext ; iIntros Hlv Hi ; gen_env
2 opendeferred goal
wp_let_
2 opendeferred goal
wp_goto_
2 opendeferred goal
wp_enter_
2 opendeferred goal
iApply IH $! _ i + 1 mkPtrbase Objbase i :: xs with [%] [Hlv Hp Hi Hl]
3 openfocused goal
deferred goal
+split ; eassumption |
3 opendeferred goal
deferred goal
split ; lia |
3 opendeferred goal
deferred goal
split ; eassumption
2 opendeferred goal
deferred goal
+rewrite lst_cons
2 opendeferred goal
iExists base, h
2 opendeferred goal
iFrame
2 opendeferred goal
iPureIntro
2 opendeferred goal
unfold node_ok
2 opendeferred goal
auto with zarith
deferred goal
–wp_branch_
wp_enter_
iApply wp_call_bind ; try side
iNext
iApply sum_spec with Hl
iNext
iIntros _
iExists _
2 openshelved goal
iSplit ; iPureIntro ; reflexivity |
iNext
cbn [ fr_fn fr_env fr_locals fr_doomed fr_at ]
gen_env
iApply wp_ret ; first side | done
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
listsum called with the int n is safe.
Explore proof 8 tactics
Initial goal
ls_facts
wp_enter_
wp_goto_
wp_enter_
iApply ls_loopn $! _ 0 null [ ] with [%] [//]
split ; reflexivity |
split ; lia |
split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
The resources the proof uses: invariants and the ghost heap.
lsΣ has invariants.
Explore proof 2 tactics
lsΣ has the ghost heap of pieces.
Explore proof 2 tactics
listsum never panics: for every input whose first word is an int, with any fuel, no state of its run fails, whatever bases its nodes get. Proved by Iris adequacy (heap_never_panics) from listsum_spec.
Explore proof 11 tactics
Initial goal
apply heap_never_panicslsΣ ls_module TAtom"listsum" _ ls_globals ListSum.ls_mem ls_fn"listsum"
4 openfocused goal
–exact ls_initial
3 opendeferred goal
–exact ls_find_listsumR.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 listsum_call_frame |
intros HinvG HheapG
apply listsum_spec
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The theorem for the interpreter's runtime.
listsum.c never panics under the interpreter's runtime.
Explore proof 1 tactics
Initial goal
exact InterpListSumLogic.listsum_never_panics
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.