Require Import VST.floyd.proofauto.
Require Import VST.progs.nest2.

Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Local Open Scope logic.

Definition t_struct_b := Tstruct _b noattr.

Definition get_spec :=
 DECLARE _get
  WITH v : reptype' t_struct_b, gv: globals
  PRE  []
        PROP ()
        LOCAL(gvars gv)
        SEP(data_at Ews t_struct_b (repinj _ v) (gv _p))
  POST [ tint ]
         PROP()
         LOCAL (temp 1%positive (Vint (snd (snd v))))
         SEP (data_at Ews t_struct_b (repinj _ v) (gv _p)).

Definition get_spec' :=
 DECLARE _get
  WITH v : (int * (float * int))%type, gv: globals
  PRE  []
        PROP ()
        LOCAL(gvars gv)
        SEP(data_at Ews t_struct_b (repinj t_struct_b v) (gv _p))
  POST [ tint ]
         PROP()
         LOCAL (temp 1%positive (Vint (snd (snd v))))
         SEP (data_at Ews t_struct_b (repinj t_struct_b v) (gv _p)).

Definition update22 (i: int) (v: reptype' t_struct_b) : reptype' t_struct_b :=
   (fst v, (fst (snd v), i)).

Definition set_spec :=
 DECLARE _set
  WITH i : int, v : reptype' t_struct_b, gv: globals
  PRE  [ _i OF tint ]
         PROP  ()
         LOCAL (gvars gv;
                temp _i (Vint i))
         SEP   (data_at Ews t_struct_b (repinj _ v) (gv _p))
  POST [ tvoid ]
         PROP() LOCAL()
        SEP(data_at Ews t_struct_b (repinj _ (update22 i v)) (gv _p)).

Definition Gprog : funspecs :=   ltac:(with_library prog [get_spec; set_spec]).

Lemma body_get:  semax_body Vprog Gprog f_get get_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_set set_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@cons localdef (temp _i (Vint i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@repinj CompSpecs t_struct_b v) (gv _p)) (@nil mpred))))) (Ssequence (Sassign (Efield (Efield (Evar _p (Tstruct _b noattr)) _y2 (Tstruct _a noattr)) _x2 tint) (Etempvar _i tint)) MORE_COMMANDS) POSTCONDITION *)
simpl in v.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@cons localdef (temp _i (Vint i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@repinj CompSpecs t_struct_b v) (gv _p)) (@nil mpred))))) (Ssequence (Sassign (Efield (Efield (Evar _p (Tstruct _b noattr)) _y2 (Tstruct _a noattr)) _x2 tint) (Etempvar _i tint)) MORE_COMMANDS) POSTCONDITION *)
unfold_repinj.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@cons localdef (temp _i (Vint i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (prod val val) (Vint (let (x, _) := v in x)) (@pair val val (Vfloat (let (x, _) := let (_, y) := v in y in x)) (Vint i))) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
Time forward. (* 5.989 sec  -> 2.6 -> 1.5 *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@cons localdef (temp _i (Vint i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (prod val val) (Vint (let (x, _) := v in x)) (@pair val val (Vfloat (let (x, _) := let (_, y) := v in y in x)) (Vint i))) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
Time forward. (* 11.1118 sec -> 7.5 *)
Time Qed.

Lemma body_get':  semax_body Vprog Gprog f_get get_spec'.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_set set_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@cons localdef (temp _i (Vint i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@repinj CompSpecs t_struct_b v) (gv _p)) (@nil mpred))))) (Ssequence (Sassign (Efield (Efield (Evar _p (Tstruct _b noattr)) _y2 (Tstruct _a noattr)) _x2 tint) (Etempvar _i tint)) MORE_COMMANDS) POSTCONDITION *)
simpl in v.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@cons localdef (temp _i (Vint i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@repinj CompSpecs t_struct_b v) (gv _p)) (@nil mpred))))) (Ssequence (Sassign (Efield (Efield (Evar _p (Tstruct _b noattr)) _y2 (Tstruct _a noattr)) _x2 tint) (Etempvar _i tint)) MORE_COMMANDS) POSTCONDITION *)
unfold_repinj.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@cons localdef (temp _i (Vint i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (prod val val) (Vint (let (x, _) := v in x)) (@pair val val (Vfloat (let (x, _) := let (_, y) := v in y in x)) (Vint i))) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
Time forward. (* 5.989 sec  -> 2.6*)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@cons localdef (temp _i (Vint i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (prod val val) (Vint (let (x, _) := v in x)) (@pair val val (Vfloat (let (x, _) := let (_, y) := v in y in x)) (Vint i))) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
Time forward. (* 11.1118 sec -> 7.5 *)
Qed.

Lemma body_set:  semax_body Vprog Gprog f_set set_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_set set_spec *)
 start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@cons localdef (temp _i (Vint i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@repinj CompSpecs t_struct_b v) (gv _p)) (@nil mpred))))) (Ssequence (Sassign (Efield (Efield (Evar _p (Tstruct _b noattr)) _y2 (Tstruct _a noattr)) _x2 tint) (Etempvar _i tint)) MORE_COMMANDS) POSTCONDITION *)
simpl in v.
(*destruct v as [a [b c]]; simpl in *. *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@cons localdef (temp _i (Vint i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@repinj CompSpecs t_struct_b v) (gv _p)) (@nil mpred))))) (Ssequence (Sassign (Efield (Efield (Evar _p (Tstruct _b noattr)) _y2 (Tstruct _a noattr)) _x2 tint) (Etempvar _i tint)) MORE_COMMANDS) POSTCONDITION *)
unfold_repinj.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@cons localdef (temp _i (Vint i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (prod val val) (Vint (let (x, _) := v in x)) (@pair val val (Vfloat (let (x, _) := let (_, y) := v in y in x)) (Vint i))) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
Time forward. (* 1.23 sec *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@cons localdef (temp _i (Vint i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (prod val val) (Vint (let (x, _) := v in x)) (@pair val val (Vfloat (let (x, _) := let (_, y) := v in y in x)) (Vint i))) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
Time forward. (* 8.77  -> 5.25 sec *)
Time Qed.  (*  28 sec -> 3.45 sec *)

