The Lemma body_push in Verif_stack of VC

Using Coq
1

I am now working on proving the Lemma body_push in Verif_stack of VC:
Lemma body_push: semax_body Vprog Gprog f_push push_spec.https://softwarefoundations.cis.upenn.edu/vc-current/Verif_stack.html
But I’m stuck.
Here are my current proofs:

Lemma body_push: semax_body Vprog Gprog f_push push_spec.

Proof.

start_function.

forward_call (Tstruct _cons noattr, gv).

unfold stack. Intros vret q.

forward_if (PROP ( )

LOCAL (temp _q vret; gvars gv; temp _p p; temp _i (Vint (Int.repr i)))

SEP (mem_mgr gv;

if eq_dec vret nullval

then emp

else

malloc_token Ews (Tstruct _cons noattr) vret

* data_at_ Ews (Tstruct _cons noattr) vret;

malloc_token Ews (Tstruct _stack noattr) p;

data_at Ews (Tstruct _stack noattr) q p; listrep il q)).

+destruct vret;simpl;entailer!.

+

(* FILL IN HERE *) Admitted.
2

I’m stuck on it as well, if I manage to get through it I’ll let you know :sweat_smile:

3

I just managed to get through it. The idea is that after if (!q) exit(1); executes, for sure we’ll have an allocated memory chunk to work with. So you want to have

forward_if (PROP ( )
   LOCAL (temp _q vret; gvars gv; temp _p p; temp _i (Vint (Int.repr i)))
   SEP (mem_mgr gv;
    malloc_token Ews (Tstruct _cons noattr) vret
      * data_at_ Ews (Tstruct _cons noattr) vret; stack il p)).

Without the if eq_dec vret nullval then ... else .... Also I recommend not unfolding the stack definition yet.

4

Even better! You can do

forward_if (vret <> nullval)

Instead of putting the whole assertion. The tactic realizes it’s a Prop and adds it to the context.