Require Import VST.floyd.proofauto.
Require Import VST.progs.field_loadstore.

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 sub_spec (sub_id: ident) :=
 DECLARE sub_id
  WITH v : val * list (val*val) , gv: globals
  PRE  []
        PROP  (is_int I8 Signed (snd (nth 1%nat (snd v) (Vundef, Vundef))))
        LOCAL (gvars gv)
        SEP   (data_at Ews t_struct_b v (gv _p))
  POST [ tvoid ]
        PROP() LOCAL()
        SEP(data_at Ews t_struct_b (snd (nth 1%nat (snd v) (Vundef, Vundef)), snd v) (gv _p)).

Definition sub_spec' (sub_id: ident) :=
 DECLARE sub_id
  WITH v : reptype t_struct_b, gv: globals
  PRE  []
        PROP  (is_int I8 Signed (proj_reptype _ (DOT _y2 SUB 1 DOT _x2) v))
        LOCAL (gvars gv)
        SEP   (data_at Ews t_struct_b v (gv _p))
  POST [ tvoid ]
        PROP() LOCAL()
        SEP(data_at Ews t_struct_b
           (upd_reptype t_struct_b (DOT _y1) v
             (proj_reptype t_struct_b (StructField _x2 :: ArraySubsc 1 :: StructField _y2 :: nil) v))
           (gv _p)).

Lemma spec_coincide: sub_spec' = sub_spec.
Proof.
(*reflexivity.*)
Abort.

Definition Gprog : funspecs :=   ltac:(with_library prog [
    sub_spec _sub1; sub_spec _sub2; sub_spec _sub3]).

Lemma body_sub1:  semax_body Vprog Gprog f_sub1 (sub_spec _sub1).
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_sub3 (sub_spec _sub3) *)
  unfold sub_spec.
(* Goal: semax_body Vprog Gprog CompSpecs f_sub3 (@pair ident funspec _sub3 (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tvoid) cc_default (prod (prod val (list (prod val val))) globals) (fun x : prod (prod val (list (prod val val))) globals => let (v, gv) := x in PROPx (@cons Prop (is_int I8 Signed (@snd val val (@nth (prod val val) (S O) (@snd val (list (prod val val)) v) (@pair val val Vundef Vundef)))) (@nil Prop)) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b v (gv _p)) (@nil mpred))))) (fun x : prod (prod val (list (prod val val))) globals => let (v, gv) := x in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (@snd val val (@nth (prod val val) (S O) (@snd val (list (prod val val)) v) (@pair val val Vundef Vundef))) (@snd val (list (prod val val)) v)) (gv _p)) (@nil mpred))))))) *)
  start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _i (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _t'1 (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)) (@cons localdef (gvars gv) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (force_val (sem_cast_i2i I8 Signed (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y))) (let (_, y) := v in y)) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
  forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _i (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _t'1 (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)) (@cons localdef (gvars gv) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (force_val (sem_cast_i2i I8 Signed (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y))) (let (_, y) := v in y)) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
  forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _i (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _t'1 (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)) (@cons localdef (gvars gv) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (force_val (sem_cast_i2i I8 Signed (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y))) (let (_, y) := v in y)) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
  forward.
Qed.

Lemma body_sub2:  semax_body Vprog Gprog f_sub2 (sub_spec _sub2).
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_sub3 (sub_spec _sub3) *)
  unfold sub_spec.
(* Goal: semax_body Vprog Gprog CompSpecs f_sub3 (@pair ident funspec _sub3 (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tvoid) cc_default (prod (prod val (list (prod val val))) globals) (fun x : prod (prod val (list (prod val val))) globals => let (v, gv) := x in PROPx (@cons Prop (is_int I8 Signed (@snd val val (@nth (prod val val) (S O) (@snd val (list (prod val val)) v) (@pair val val Vundef Vundef)))) (@nil Prop)) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b v (gv _p)) (@nil mpred))))) (fun x : prod (prod val (list (prod val val))) globals => let (v, gv) := x in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (@snd val val (@nth (prod val val) (S O) (@snd val (list (prod val val)) v) (@pair val val Vundef Vundef))) (@snd val (list (prod val val)) v)) (gv _p)) (@nil mpred))))))) *)
  start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _i (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _t'1 (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)) (@cons localdef (gvars gv) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (force_val (sem_cast_i2i I8 Signed (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y))) (let (_, y) := v in y)) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
  forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _i (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _t'1 (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)) (@cons localdef (gvars gv) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (force_val (sem_cast_i2i I8 Signed (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y))) (let (_, y) := v in y)) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
  forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _i (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _t'1 (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)) (@cons localdef (gvars gv) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (force_val (sem_cast_i2i I8 Signed (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y))) (let (_, y) := v in y)) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
  forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _i (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _t'1 (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)) (@cons localdef (gvars gv) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (force_val (sem_cast_i2i I8 Signed (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y))) (let (_, y) := v in y)) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
  forward.
Qed.

Lemma body_sub3:  semax_body Vprog Gprog f_sub3 (sub_spec _sub3).
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_sub3 (sub_spec _sub3) *)
  unfold sub_spec.
(* Goal: semax_body Vprog Gprog CompSpecs f_sub3 (@pair ident funspec _sub3 (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tvoid) cc_default (prod (prod val (list (prod val val))) globals) (fun x : prod (prod val (list (prod val val))) globals => let (v, gv) := x in PROPx (@cons Prop (is_int I8 Signed (@snd val val (@nth (prod val val) (S O) (@snd val (list (prod val val)) v) (@pair val val Vundef Vundef)))) (@nil Prop)) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b v (gv _p)) (@nil mpred))))) (fun x : prod (prod val (list (prod val val))) globals => let (v, gv) := x in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (@snd val val (@nth (prod val val) (S O) (@snd val (list (prod val val)) v) (@pair val val Vundef Vundef))) (@snd val (list (prod val val)) v)) (gv _p)) (@nil mpred))))))) *)
  start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _i (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _t'1 (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)) (@cons localdef (gvars gv) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (force_val (sem_cast_i2i I8 Signed (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y))) (let (_, y) := v in y)) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
  forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _i (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _t'1 (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)) (@cons localdef (gvars gv) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (force_val (sem_cast_i2i I8 Signed (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y))) (let (_, y) := v in y)) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
  forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _i (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _t'1 (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)) (@cons localdef (gvars gv) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (force_val (sem_cast_i2i I8 Signed (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y))) (let (_, y) := v in y)) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
  forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _i (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _t'1 (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)) (@cons localdef (gvars gv) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (force_val (sem_cast_i2i I8 Signed (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y))) (let (_, y) := v in y)) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
  forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _i (force_val (sem_cast tschar tschar (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)))) (@cons localdef (temp _t'1 (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y)) (@cons localdef (gvars gv) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_b (@pair val (list (prod val val)) (force_val (sem_cast_i2i I8 Signed (let (_, y) := @Znth (prod val val) (@pair val val Vundef Vundef) (Zpos xH) (let (_, y) := v in y) in y))) (let (_, y) := v in y)) (gv _p)) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
  forward.
Qed.
