(** Heavily annotated for a tutorial introduction. *)

(** First, import the entire Floyd proof automation system, which includes
 ** the VeriC program logic and the MSL theory of separation logic**)
Require Import VST.floyd.proofauto.

(** Import the [reverse.v] file, which is produced by CompCert's clightgen
 ** from reverse.c.   The file reverse.v defines abbreviations for identifiers
 ** (variable names, etc.) of the C program, such as _head, _reverse.
 ** It also defines "prog", which is the entire abstract syntax tree
 ** of the C program *)
Require Import VST.progs.reverse.

(* The C programming language has a special namespace for struct
** and union identifiers, e.g., "struct foo {...}".  Some type-based operators
** in the program logic need access to an interpretation of this namespace,
** i.e., the meaning of each struct-identifier such as "foo".  The next
** line (which looks identical for any program) builds this
** interpretation, called "CompSpecs" *)
Instance CompSpecs : compspecs. make_compspecs prog. Defined.

(** Calculate the "types-of-global-variables" specification
 ** directly from the program *)
Definition Vprog : varspecs. mk_varspecs prog. Defined.

(** A convenience definition *)
Definition t_struct_list := Tstruct _list noattr.

(** Inductive definition of linked lists *)
Fixpoint listrep (sigma: list val) (x: val) : mpred :=
 match sigma with
 | h::hs => 
    EX y:val, 
      data_at Tsh t_struct_list (h,y) x  *  listrep hs y
 | nil => 
    !! (x = nullval) && emp
 end.

Arguments listrep sigma x : simpl never.

(** Whenever you define a new spatial operator, such as
 ** [listrep] here, it's useful to populate two hint databases.
 ** The [saturate_local] hint is a lemma that extracts
 ** pure propositional facts from a spatial fact.
 ** The [valid_pointer] hint is a lemma that extracts a
 ** valid-pointer fact from a spatial lemma.
 **)

Lemma listrep_local_facts:
  forall sigma p,
   listrep sigma p |--
   !! (is_pointer_or_null p /\ (p=nullval <-> sigma=nil)).
Proof.
(* Goal: forall (sigma : list val) (p : val), @derives mpred Nveric (listrep sigma p) (@prop mpred Nveric (and (is_pointer_or_null p) (iff (@eq val p nullval) (@eq (list val) sigma (@nil val))))) *)
intros.
revert p; induction sigma; 
  unfold listrep; fold listrep; intros; normalize.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@prop mpred Nveric (and (is_pointer_or_null nullval) (iff (@eq val nullval nullval) (@eq (list val) (@nil val) (@nil val))))) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val a y) p) (listrep sigma y)) (@prop mpred Nveric (and (is_pointer_or_null p) (iff (@eq val p nullval) (@eq (list val) (@cons val a sigma) (@nil val))))) *)
apply prop_right; split; simpl; auto. intuition.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (listrep s1 w) (@andp mpred Nveric (@prop mpred Nveric (@eq val nullval nullval)) (@emp mpred Nveric Sveric))) (listrep (@rev val (@app val (@rev val s1) (@nil val))) w) *)
entailer!.
(* Goal: iff (@eq val p nullval) (@eq (list val) (@cons val a sigma) (@nil val)) *)
split; intro. subst p. destruct H; contradiction. inv H2.
Qed.

Hint Resolve listrep_local_facts : saturate_local.

Lemma listrep_valid_pointer:
  forall sigma p,
   listrep sigma p |-- valid_pointer p.
Proof.
 destruct sigma; unfold listrep; fold listrep;
 intros; normalize.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (valid_pointer nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val v y) p) (listrep sigma y)) (valid_pointer p) *)
 auto with valid_pointer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val v y) p) (listrep sigma y)) (valid_pointer p) *)
 apply sepcon_valid_pointer1.
(* Goal: @derives mpred Nveric (@data_at CompSpecs Tsh t_struct_list (@pair val val v y) p) (valid_pointer p) *)
 apply data_at_valid_ptr; auto.
 simpl;  computable.
Qed.

Hint Resolve listrep_valid_pointer : valid_pointer.

(** Specification of the [reverse] function.  It characterizes
 ** the precondition required for calling the function,
 ** and the postcondition guaranteed by the function.
 **)
Definition reverse_spec :=
 DECLARE _reverse
  WITH sigma : list val, p: val
  PRE  [ _p OF (tptr t_struct_list) ]
     PROP ()
     LOCAL (temp _p p)
     SEP (listrep sigma p)
  POST [ (tptr t_struct_list) ]
    EX q:val,
     PROP () LOCAL (temp ret_temp q)
     SEP (listrep(rev sigma) q).

(** The global function spec, characterizing the
 ** preconditions/postconditions of all the functions
 ** that your proved-correct program will call. 
 ** Normally you include all the functions here, but
 ** in this tutorial example we include only one. *)
Definition Gprog : funspecs :=
         ltac:(with_library prog [ reverse_spec ]).

(** For each function definition in the C program, prove that the
 ** function-body (in this case, f_reverse) satisfies its specification
 ** (in this case, reverse_spec).
 **)
Lemma body_reverse: semax_body Vprog Gprog
                                    f_reverse reverse_spec.
Proof.
(** The start_function tactic "opens up" a semax_body
 ** proof goal into a Hoare triple. *)
(* Goal: semax_body Vprog Gprog CompSpecs f_reverse reverse_spec *)
start_function.
(** For each assignment statement, "symbolically execute" it
 ** using the forward tactic *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _w w) (@cons localdef (temp _v v) (@nil localdef))) (SEPx (@cons mpred (listrep s1 w) (@cons mpred (listrep s2 v) (@nil mpred)))))) (Sreturn (@Some expr (Etempvar _w (tptr (Tstruct _list noattr))))) POSTCONDITION *)
forward.  (* w = NULL; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _w w) (@cons localdef (temp _v v) (@nil localdef))) (SEPx (@cons mpred (listrep s1 w) (@cons mpred (listrep s2 v) (@nil mpred)))))) (Sreturn (@Some expr (Etempvar _w (tptr (Tstruct _list noattr))))) POSTCONDITION *)
forward.  (* v = p; *)
(** To prove a while-loop, you must supply a loop invariant,
 ** in this case (EX s1  PROP(...)LOCAL(...)(SEP(...)).  *)
forward_while
   (EX s1: list val, EX s2 : list val, 
    EX w: val, EX v: val,
     PROP (sigma = rev s1 ++ s2)
     LOCAL (temp _w w; temp _v v)
     SEP (listrep s1 w; listrep s2 v)).
(** The forward_while tactic leaves four subgoals,
 ** which we mark with * (the Coq "bullet") *)
* (* Prove that precondition implies loop invariant *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _v p) (@cons localdef (temp _w (Vint (Int.repr Z0))) (@cons localdef (temp _p p) (@nil localdef)))) (SEPx (@cons mpred (listrep sigma p) (@nil mpred)))))) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (list val) (fun s1 : list val => @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (list val) (fun s2 : list val => @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun w : val => @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun v : val => PROPx (@cons Prop (@eq (list val) sigma (@app val (@rev val s1) s2)) (@nil Prop)) (LOCALx (@cons localdef (temp _w w) (@cons localdef (temp _v v) (@nil localdef))) (SEPx (@cons mpred (listrep s1 w) (@cons mpred (listrep s2 v) (@nil mpred)))))))))) *)
Exists (@nil val) sigma nullval p.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (listrep s1 w) (@andp mpred Nveric (@prop mpred Nveric (@eq val nullval nullval)) (@emp mpred Nveric Sveric))) (listrep (@rev val (@app val (@rev val s1) (@nil val))) w) *)
entailer!.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (listrep (@nil val) nullval) *)
unfold listrep.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (listrep s1 w) (@andp mpred Nveric (@prop mpred Nveric (@eq val nullval nullval)) (@emp mpred Nveric Sveric))) (listrep (@rev val (@app val (@rev val s1) (@nil val))) w) *)
entailer!.
* (* Prove that loop invariant implies typechecking of loop condition *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (listrep s1 w) (@andp mpred Nveric (@prop mpred Nveric (@eq val nullval nullval)) (@emp mpred Nveric Sveric))) (listrep (@rev val (@app val (@rev val s1) (@nil val))) w) *)
entailer!.
* (* Prove that loop body preserves invariant *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _w w) (@cons localdef (temp _v v) (@nil localdef))) (SEPx (@cons mpred (listrep s1 w) (@cons mpred (listrep s2 v) (@nil mpred)))))) (Ssequence (Sset _t (Efield (Ederef (Etempvar _v (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
destruct s2 as [ | h r].
 - unfold listrep at 2. 
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _w w) (@cons localdef (temp _v v) (@nil localdef))) (SEPx (@cons mpred (listrep s1 w) (@cons mpred (@andp mpred Nveric (@prop mpred Nveric (@eq val v nullval)) (@emp mpred Nveric Sveric)) (@nil mpred)))))) (Ssequence (Sset _t (Efield (Ederef (Etempvar _v (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   Intros. subst. contradiction.
 - unfold listrep at 2; fold listrep.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _w w) (@cons localdef (temp _v v) (@nil localdef))) (SEPx (@cons mpred (listrep s1 w) (@cons mpred (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val h y) v) (listrep r y))) (@nil mpred)))))) (Ssequence (Sset _t (Efield (Ederef (Etempvar _v (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   Intros y.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _w w) (@cons localdef (temp _v v) (@nil localdef))) (SEPx (@cons mpred (listrep s1 w) (@cons mpred (listrep s2 v) (@nil mpred)))))) (Sreturn (@Some expr (Etempvar _w (tptr (Tstruct _list noattr))))) POSTCONDITION *)
   forward. (* t = v->tail *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _w w) (@cons localdef (temp _v v) (@nil localdef))) (SEPx (@cons mpred (listrep s1 w) (@cons mpred (listrep s2 v) (@nil mpred)))))) (Sreturn (@Some expr (Etempvar _w (tptr (Tstruct _list noattr))))) POSTCONDITION *)
   forward. (* v->tail = w; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _w w) (@cons localdef (temp _v v) (@nil localdef))) (SEPx (@cons mpred (listrep s1 w) (@cons mpred (listrep s2 v) (@nil mpred)))))) (Sreturn (@Some expr (Etempvar _w (tptr (Tstruct _list noattr))))) POSTCONDITION *)
   forward. (* w = v; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _w w) (@cons localdef (temp _v v) (@nil localdef))) (SEPx (@cons mpred (listrep s1 w) (@cons mpred (listrep s2 v) (@nil mpred)))))) (Sreturn (@Some expr (Etempvar _w (tptr (Tstruct _list noattr))))) POSTCONDITION *)
   forward. (* v = t; *)
   (* At end of loop body; reestablish invariant *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (listrep s1 w) (@andp mpred Nveric (@prop mpred Nveric (@eq val nullval nullval)) (@emp mpred Nveric Sveric))) (listrep (@rev val (@app val (@rev val s1) (@nil val))) w) *)
   entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (listrep s1 w) (@data_at CompSpecs Tsh t_struct_list (@pair val val h w) v)) (listrep r y)) (@exp mpred Nveric (prod (prod (prod (list val) (list val)) val) val) (fun a : prod (prod (prod (list val) (list val)) val) val => @andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@app val (@rev val s1) (@cons val h r)) (@app val (@rev val (@fst (list val) (list val) (@fst (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val a)))) (@snd (list val) (list val) (@fst (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val a))))) (and (@eq val (@snd (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val a)) v) (@eq val (@snd (prod (prod (list val) (list val)) val) val a) y)))) (@sepcon mpred Nveric Sveric (listrep (@fst (list val) (list val) (@fst (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val a))) (@snd (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val a))) (listrep (@snd (list val) (list val) (@fst (prod (list val) (list val)) val (@fst (prod (prod (list val) (list val)) val) val a))) (@snd (prod (prod (list val) (list val)) val) val a))))) *)
   Exists (h::s1,r,v,y).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (listrep s1 w) (@andp mpred Nveric (@prop mpred Nveric (@eq val nullval nullval)) (@emp mpred Nveric Sveric))) (listrep (@rev val (@app val (@rev val s1) (@nil val))) w) *)
   entailer!.
   + simpl. rewrite app_ass. auto.
   + unfold listrep at 3; fold listrep.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (listrep s1 w) (@andp mpred Nveric (@prop mpred Nveric (@eq val nullval nullval)) (@emp mpred Nveric Sveric))) (listrep (@rev val (@app val (@rev val s1) (@nil val))) w) *)
     Exists w. entailer!.
* (* after the loop *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _w w) (@cons localdef (temp _v v) (@nil localdef))) (SEPx (@cons mpred (listrep s1 w) (@cons mpred (listrep s2 v) (@nil mpred)))))) (Sreturn (@Some expr (Etempvar _w (tptr (Tstruct _list noattr))))) POSTCONDITION *)
forward.  (* return w; *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (listrep s1 w) (@andp mpred Nveric (@prop mpred Nveric (@eq val nullval nullval)) (@emp mpred Nveric Sveric))) (listrep (@rev val (@app val (@rev val s1) (@nil val))) w) *)
Exists w; entailer!.
(* Goal: @derives mpred Nveric (listrep s1 w) (listrep s1 w) *)
rewrite (proj1 H1) by auto.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (listrep s1 w) (listrep (@nil val) nullval)) (listrep (@rev val (@app val (@rev val s1) (@nil val))) w) *)
unfold listrep at 2; fold listrep.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (listrep s1 w) (@andp mpred Nveric (@prop mpred Nveric (@eq val nullval nullval)) (@emp mpred Nveric Sveric))) (listrep (@rev val (@app val (@rev val s1) (@nil val))) w) *)
entailer!.
rewrite <- app_nil_end, rev_involutive.
(* Goal: @derives mpred Nveric (listrep s1 w) (listrep s1 w) *)
auto.
Qed.

(** See the file [progs/verif_reverse.v] for an alternate
 ** proof of this function, using a general theory of
 ** list segments.  That file also has proofs of the
 ** sumlist function, the main function, and the
 ** [semax_func] theorem that ties all the functions together
 **)

