Require Import VST.floyd.proofauto.
Require Import VST.progs.load_demo.

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

Definition pair_pair_t := (Tstruct _pair_pair noattr).

Definition array_size := 100.

Definition get22_spec :=
 DECLARE _get22
  WITH pps: val, i: Z, x11: int, x12: int, x21: int, x22: int, sh : share
  PRE [ _pps OF (tptr pair_pair_t), _i OF tint ]
    PROP  (readable_share sh; 0 <= i < array_size)
    LOCAL (temp _pps pps; temp _i (Vint (Int.repr i)))
    SEP   (field_at sh (tarray pair_pair_t array_size) [ArraySubsc i]
                    ((Vint x11, Vint x12), (Vint x21, Vint x22)) pps)
  POST [ tint ]
        PROP () LOCAL (temp ret_temp (Vint x22))
    SEP   (field_at sh (tarray pair_pair_t array_size) [ArraySubsc i]
                    ((Vint x11, Vint x12), (Vint x21, Vint x22)) pps).

Definition uint_sum (contents : list Z) : int :=
  fold_right (fun el sum => Int.add sum (Int.repr el)) Int.zero contents.

Definition fiddle_spec :=
 DECLARE _fiddle
  WITH p: val, n: Z, tag: Z, contents: list Z
  PRE [ _p OF tptr tuint ]
          PROP  (Int.unsigned (Int.shru (Int.repr tag) (Int.repr 10)) = n)
          LOCAL (temp _p p)
          SEP (data_at Ews (tarray tuint (1+n)) 
                      (map Vint (map Int.repr (tag::contents)))
                      (offset_val (-sizeof tuint) p))
  POST [ tint ]
          PROP ( )
          LOCAL (temp ret_temp (Vint (Int.add (Int.repr (Z.land tag 255)) (uint_sum contents))))
          SEP (data_at Ews (tarray tuint (1+n)) 
                      (map Vint (map Int.repr (tag::contents)))
                      (offset_val (-sizeof tuint) p)).

Definition get_uint32_le (arr: list Z) : int :=
 (Int.or (Int.or (Int.or
            (Int.repr (Znth 0 arr))
   (Int.shl (Int.repr (Znth 1 arr)) (Int.repr  8)))
   (Int.shl (Int.repr (Znth 2 arr)) (Int.repr 16)))
   (Int.shl (Int.repr (Znth 3 arr)) (Int.repr 24))).

Definition get_little_endian_spec :=
  DECLARE _get_little_endian
  WITH input : val, in_sh : share, arr : list Z
  PRE [ _input OF (tptr tuchar) ]
    PROP (Zlength arr = 4;
          readable_share in_sh;
          forall i, 0 <= i < 4 -> 0 <= Znth i arr <= Byte.max_unsigned)
    LOCAL (temp _input input)
    SEP (data_at in_sh (tarray tuchar 4) (map Vint (map Int.repr arr)) input)
  POST [ tuint ]
    PROP() LOCAL(temp ret_temp (Vint (get_uint32_le arr)))
    SEP (data_at in_sh (tarray tuchar 4) (map Vint (map Int.repr arr)) input).

Definition Gprog : funspecs := ltac:(with_library prog
  [get22_spec; fiddle_spec; get_little_endian_spec]).


Ltac solve_arr_range H := 
 match goal with |- context [Znth ?i _] => 
   specialize (H i); spec H; [ computable | ];
   rewrite Int.unsigned_repr; rep_omega
 end.

Lemma body_get_little_endian: semax_body Vprog Gprog f_get_little_endian get_little_endian_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_get22 get22_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _input input) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs in_sh (tarray tuchar (Zpos (xO (xO xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr arr)) input) (@nil mpred))))) (Ssequence (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _input (tptr tuchar)) (Econst_int (Int.repr Z0) tint) (tptr tuchar)) tuchar)) (Sset _b0 (Ecast (Etempvar _t'2 tuchar) tuint))) MORE_COMMANDS) POSTCONDITION *)
assert (BMU: Byte.max_unsigned=255) by reflexivity.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
entailer!. solve_arr_range H0.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
entailer!. solve_arr_range H0.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
entailer!. solve_arr_range H0.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
entailer!. solve_arr_range H0.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
Qed.

Lemma uint_sum_app: forall a b, uint_sum (a++b) = Int.add (uint_sum a) (uint_sum b).
Proof.
(* Goal: forall a b : list Z, @eq Int.int (uint_sum (@app Z a b)) (Int.add (uint_sum a) (uint_sum b)) *)
  intros. induction a; simpl.
  - symmetry. apply Int.add_zero_l.
  - rewrite IHa. rewrite !Int.add_assoc. f_equal. apply Int.add_commut.
Qed.

Lemma body_fiddle: semax_body Vprog Gprog f_fiddle fiddle_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_get22 get22_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Z.add (Zpos xH) n)) (@map Int.int val Vint (@map Z Int.int Int.repr (@cons Z tag contents))) (offset_val (Z.opp (@sizeof (@cenv_cs CompSpecs) tuint)) p)) (@nil mpred))))) (Ssequence (Sset _tagword (Ederef (Ebinop Oadd (Etempvar _p (tptr tuint)) (Eunop Oneg (Econst_int (Int.repr (Zpos xH)) tint) tint) (tptr tuint)) tuint)) MORE_COMMANDS) POSTCONDITION *)
rename H into Htag.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Z.add (Zpos xH) n)) (@map Int.int val Vint (@map Z Int.int Int.repr (@cons Z tag contents))) (offset_val (Z.opp (@sizeof (@cenv_cs CompSpecs) tuint)) p)) (@nil mpred))))) (Ssequence (Sset _tagword (Ederef (Ebinop Oadd (Etempvar _p (tptr tuint)) (Eunop Oneg (Econst_int (Int.repr (Zpos xH)) tint) tint) (tptr tuint)) tuint)) MORE_COMMANDS) POSTCONDITION *)
assert_PROP (Zlength contents = n) as LEN. {
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
  entailer!.
(* Goal: @eq Z (@Zlength Z contents) (Int.unsigned (Int.shru (Int.repr tag) (Int.repr (Zpos (xO (xI (xO xH))))))) *)
  forget (Int.unsigned (Int.shru (Int.repr tag) (Int.repr 10))) as n.
  clear - H0.
(* Goal: @eq Z (@Zlength Z contents) n *)
  rewrite !Zlength_map in H0.
(* Goal: @eq Z (@Zlength Z contents) n *)
  rewrite Zlength_cons in H0.
(* Goal: @eq Z (@Zlength Z contents) n *)
  destruct (zlt n 0); [elimtype False | ].
(* Goal: False *)
(* Goal: @eq Z (@Zlength Z contents) n *)
  rewrite Z.max_l in H0 by omega.
(* Goal: Z.le Z0 n *)
  pose proof (Zlength_nonneg contents).
(* Goal: @eq Z (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xI xH))))) (Z.add (Z.add (Z.add Z0 (Z.mul (Zpos (xO (xO (xO (xO xH))))) i)) (Zpos (xO (xO (xO xH))))) (Zpos (xO (xO xH)))) *)
  omega.
(* Goal: @eq Z (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xI xH))))) (Z.add (Z.add (Z.add Z0 (Z.mul (Zpos (xO (xO (xO (xO xH))))) i)) (Zpos (xO (xO (xO xH))))) (Zpos (xO (xO xH)))) *)
  rewrite Z.max_r in H0 by omega. omega.  
}
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Ssequence (Sset _res (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint)) MORE_COMMANDS) POSTCONDITION *)
assert (Zlength (tag :: contents) = 1 + n) as LEN1. {
(* Goal: @eq Z (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xI xH))))) (Z.add (Z.add (Z.add Z0 (Z.mul (Zpos (xO (xO (xO (xO xH))))) i)) (Zpos (xO (xO (xO xH))))) (Zpos (xO (xO xH)))) *)
  rewrite Zlength_cons. omega.
}
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Ssequence (Sset _res (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint)) MORE_COMMANDS) POSTCONDITION *)
assert (N0: 0 <= n). {
(* Goal: Z.le Z0 n *)
  pose proof (Zlength_nonneg contents). omega.
}
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
assert_PROP (isptr p) as P by entailer!.

(* forward fails, but tells us to prove this: *)
assert_PROP (force_val (sem_add_ptr_int tuint Signed p (eval_unop Oneg tint (Vint (Int.repr 1)))) 
  = field_address (tarray tuint (1+n)) [ArraySubsc 0] (offset_val (-sizeof tuint) p)). {
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
  entailer!.
(* Goal: @eq val (offset_val (Z.mul (@sizeof (@cenv_cs CompSpecs) tuint) i) p) (@field_address CompSpecs (tarray tuint (Z.add (Zpos xH) (Int.unsigned (Int.shru (Int.repr tag) (Int.repr (Zpos (xO (xI (xO xH))))))))) (@cons gfield (ArraySubsc (Z.add (Zpos xH) i)) (@nil gfield)) (offset_val (Z.opp (@sizeof (@cenv_cs CompSpecs) tuint)) p)) *)
  destruct p; inversion P. simpl.
(* Goal: @eq val (offset_val (Z.add (Z.mul (@sizeof (@cenv_cs CompSpecs) (Tstruct _pair_pair noattr)) i) (Zpos (xO (xO (xO xH))))) pps) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps) *)
  rewrite field_compatible_field_address by auto with field_compatible.
(* Goal: @eq val (offset_val (Z.add (Z.mul (@sizeof (@cenv_cs CompSpecs) (Tstruct _pair_pair noattr)) i) (Zpos (xO (xO (xO xH))))) pps) (offset_val (@nested_field_offset CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield)))) pps) *)
  simpl.
(* Goal: @eq val (Vptr b (Ptrofs.add i (Ptrofs.mul (Ptrofs.repr (Zpos (xO (xO xH)))) (Ptrofs.of_ints (Int.neg (Int.repr (Zpos xH))))))) (Vptr b (Ptrofs.add (Ptrofs.add i (Ptrofs.repr (Zneg (xO (xO xH))))) (Ptrofs.repr Z0))) *)
  rewrite ptrofs_add_repr_0_r. reflexivity.
}
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
(* sum = tagword & 0xff; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
(* size = tagword >> 10; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
(* rewrite !Znth_0_cons. *)
forward_for_simple_bound (Int.unsigned (Int.shru (Int.repr tag) (Int.repr 10))) (EX i: Z,
  PROP ( )
  LOCAL (
    temp _size (Vint (Int.shru (Int.repr tag) (Int.repr 10)));
    temp _sum (Vint (Int.add (Int.and (Int.repr tag) (Int.repr 255))
                             (uint_sum (sublist 0 i contents))));
    temp _tagword (Vint (Int.repr tag));
    temp _p p
  )
  SEP (data_at Ews (tarray tuint (1 + n)) (map Vint (map Int.repr (tag :: contents)))
          (offset_val (- sizeof tuint) p))).
- (* precondition implies 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
  entailer!.
- (* body preserves invariant: *)
  (* forward fails, but tells us to prove this: *)
  assert_PROP (force_val (sem_add_ptr_int tuint Unsigned p (Vint (Int.repr i)))
    = field_address (tarray tuint (1 + n)) [ArraySubsc (1 + i)] (offset_val (- sizeof tuint) p)). {
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
    entailer!.
(* Goal: @eq val (offset_val (Z.mul (@sizeof (@cenv_cs CompSpecs) tuint) i) p) (@field_address CompSpecs (tarray tuint (Z.add (Zpos xH) (Int.unsigned (Int.shru (Int.repr tag) (Int.repr (Zpos (xO (xI (xO xH))))))))) (@cons gfield (ArraySubsc (Z.add (Zpos xH) i)) (@nil gfield)) (offset_val (Z.opp (@sizeof (@cenv_cs CompSpecs) tuint)) p)) *)
    destruct p; inversion P. simpl.
(* Goal: @eq val (offset_val (Z.add (Z.mul (@sizeof (@cenv_cs CompSpecs) (Tstruct _pair_pair noattr)) i) (Zpos (xO (xO (xO xH))))) pps) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps) *)
    rewrite field_compatible_field_address by auto with field_compatible.
(* Goal: @eq val (offset_val (Z.add (Z.mul (@sizeof (@cenv_cs CompSpecs) (Tstruct _pair_pair noattr)) i) (Zpos (xO (xO (xO xH))))) pps) (offset_val (@nested_field_offset CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield)))) pps) *)
    simpl.
(* Goal: @eq val (Vptr b (Ptrofs.add i0 (Ptrofs.repr (Z.mul (Zpos (xO (xO xH))) i)))) (Vptr b (Ptrofs.add (Ptrofs.add i0 (Ptrofs.repr (Zneg (xO (xO xH))))) (Ptrofs.repr (Z.add Z0 (Z.mul (Zpos (xO (xO xH))) (Z.add (Zpos xH) i)))))) *)
    rewrite Ptrofs.add_assoc, ptrofs_add_repr. 
(* Goal: @eq val (offset_val (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xI xH))))) pps) (offset_val (Z.add (Z.add (Z.add Z0 (Z.mul (Zpos (xO (xO (xO (xO xH))))) i)) (Zpos (xO (xO (xO xH))))) (Zpos (xO (xO xH)))) pps) *)
    f_equal. f_equal. f_equal. omega.
  }
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
  forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
  forward.
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
  entailer!.
(* Goal: @eq Z (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xI xH))))) (Z.add (Z.add (Z.add Z0 (Z.mul (Zpos (xO (xO (xO (xO xH))))) i)) (Zpos (xO (xO (xO xH))))) (Zpos (xO (xO xH)))) *)
  rewrite Znth_pos_cons by omega.
(* Goal: @eq val (offset_val (Z.add (Z.mul (@sizeof (@cenv_cs CompSpecs) (Tstruct _pair_pair noattr)) i) (Zpos (xO (xO (xO xH))))) pps) (offset_val (@nested_field_offset CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield)))) pps) *)
  autorewrite with sublist. simpl.  
(* Goal: @eq val (offset_val (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xI xH))))) pps) (offset_val (Z.add (Z.add (Z.add Z0 (Z.mul (Zpos (xO (xO (xO (xO xH))))) i)) (Zpos (xO (xO (xO xH))))) (Zpos (xO (xO xH)))) pps) *)
  f_equal. rewrite Int.add_assoc. f_equal.
(* Goal: @eq Z (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xI xH))))) (Z.add (Z.add (Z.add Z0 (Z.mul (Zpos (xO (xO (xO (xO xH))))) i)) (Zpos (xO (xO (xO xH))))) (Zpos (xO (xO xH)))) *)
  rewrite (sublist_split 0 i (i+1)) by omega.
(* Goal: @eq Z (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xI xH))))) (Z.add (Z.add (Z.add Z0 (Z.mul (Zpos (xO (xO (xO (xO xH))))) i)) (Zpos (xO (xO (xO xH))))) (Zpos (xO (xO xH)))) *)
  rewrite sublist_len_1 by omega.
  replace (1 + i - 1) with i by omega.
(* Goal: @eq Int.int (Int.add Int.zero (Int.repr (@Znth Z Inhabitant_Z i contents))) (Int.repr (@Znth Z Inhabitant_Z i contents)) *)
  rewrite uint_sum_app. f_equal. simpl. apply Int.add_zero_l.
- (* return sum; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
  forward. rewrite sublist_same by auto. entailer!.
Qed.

Lemma body_get22_root_expr: semax_body Vprog Gprog f_get22 get22_spec.
 Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_get22 get22_spec *)
 start_function.
 (* int_pair_t* p = &pps[i].right; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
 forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p (offset_val (align (Z.add (align Z0 (@alignof (@cenv_cs CompSpecs) (Tstruct _int_pair noattr))) (@sizeof (@cenv_cs CompSpecs) (Tstruct _int_pair noattr))) (@alignof (@cenv_cs CompSpecs) (Tstruct _int_pair noattr))) (@eval_binop CompSpecs Oadd (tptr (Tstruct _pair_pair noattr)) tint pps (Vint (Int.repr i))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Ssequence (Sset _res (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint)) MORE_COMMANDS) POSTCONDITION *)
 simpl (temp _p _).
 (* Assert_PROP what forward asks us for (only for the root expression "p"):  *)
 assert_PROP (offset_val 8 (force_val (sem_add_ptr_int (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Ssequence (Sset _res (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint)) MORE_COMMANDS) POSTCONDITION *)
   = field_address (tarray pair_pair_t array_size) [StructField _right; ArraySubsc i] pps) as E. {
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
   entailer!. rewrite field_compatible_field_address by auto with field_compatible.
(* Goal: @eq val (offset_val (Z.add (Z.mul (@sizeof (@cenv_cs CompSpecs) (Tstruct _pair_pair noattr)) i) (Zpos (xO (xO (xO xH))))) pps) (offset_val (@nested_field_offset CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield)))) pps) *)
  simpl. normalize.
 }
 (* int res = p->snd; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
 forward.
 (* return res; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
 forward.
 Qed.
 

Lemma body_get22_full_expr: semax_body Vprog Gprog f_get22 get22_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_get22 get22_spec *)
start_function.
(* int_pair_t* p = &pps[i].right; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p (offset_val (align (Z.add (align Z0 (@alignof (@cenv_cs CompSpecs) (Tstruct _int_pair noattr))) (@sizeof (@cenv_cs CompSpecs) (Tstruct _int_pair noattr))) (@alignof (@cenv_cs CompSpecs) (Tstruct _int_pair noattr))) (@eval_binop CompSpecs Oadd (tptr (Tstruct _pair_pair noattr)) tint pps (Vint (Int.repr i))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Ssequence (Sset _res (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint)) MORE_COMMANDS) POSTCONDITION *)
simpl (temp _p _).

(* Assert_PROP what forward asks us for (for the full expression "p->snd"): *)
assert_PROP (
  offset_val 4 (offset_val 8 (force_val
    (sem_add_ptr_int (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))
  = (field_address (tarray pair_pair_t array_size)
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Ssequence (Sset _res (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint)) MORE_COMMANDS) POSTCONDITION *)
                   [StructField _snd; StructField _right; ArraySubsc i] pps)). {
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
  entailer!. rewrite field_compatible_field_address by auto with field_compatible.
(* Goal: @eq val (offset_val (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xI xH))))) pps) (offset_val (Z.add (Z.add (Z.add Z0 (Z.mul (Zpos (xO (xO (xO (xO xH))))) i)) (Zpos (xO (xO (xO xH))))) (Zpos (xO (xO xH)))) pps) *)
  simpl. f_equal. omega.
}
(* int res = p->snd; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
(* return res; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
Qed.

Lemma body_get22_alt: semax_body Vprog Gprog f_get22 get22_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_get22 get22_spec *)
start_function.
(* int_pair_t* p = &pps[i].right; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p (offset_val (align (Z.add (align Z0 (@alignof (@cenv_cs CompSpecs) (Tstruct _int_pair noattr))) (@sizeof (@cenv_cs CompSpecs) (Tstruct _int_pair noattr))) (@alignof (@cenv_cs CompSpecs) (Tstruct _int_pair noattr))) (@eval_binop CompSpecs Oadd (tptr (Tstruct _pair_pair noattr)) tint pps (Vint (Int.repr i))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Ssequence (Sset _res (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint)) MORE_COMMANDS) POSTCONDITION *)
simpl (temp _p _).

(* Alternative: Make p nice enough so that no hint is required: *)
assert_PROP (offset_val 8 (force_val (sem_add_ptr_int (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Ssequence (Sset _res (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint)) MORE_COMMANDS) POSTCONDITION *)
  = field_address (tarray pair_pair_t array_size) [StructField _right; ArraySubsc i] pps) as E. {
(* 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 _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))) (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps))) *)
  entailer!. rewrite field_compatible_field_address by auto with field_compatible.
(* Goal: @eq val (offset_val (Z.add (Z.mul (@sizeof (@cenv_cs CompSpecs) (Tstruct _pair_pair noattr)) i) (Zpos (xO (xO (xO xH))))) pps) (offset_val (@nested_field_offset CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield)))) pps) *)
  simpl.
(* Goal: @eq val (offset_val (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xO xH))))) pps) (offset_val (Z.add (Z.add Z0 (Z.mul (Zpos (xO (xO (xO (xO xH))))) i)) (Zpos (xO (xO (xO xH))))) pps) *)
  normalize.
}
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p (offset_val (Zpos (xO (xO (xO xH)))) (force_val (@sem_add_ptr_int CompSpecs (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Ssequence (Sset _res (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint)) MORE_COMMANDS) POSTCONDITION *)
rewrite E. clear E.
(* int res = p->snd; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
(* return res; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x22)) (@cons localdef (temp _p (@field_address CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))) pps)) (@cons localdef (temp _pps pps) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs sh (tarray pair_pair_t array_size) (@cons gfield (ArraySubsc i) (@nil gfield)) (@pair (prod val val) (prod val val) (@pair val val (Vint x11) (Vint x12)) (@pair val val (Vint x21) (Vint x22))) pps) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _res tint))) POSTCONDITION *)
forward.
Qed.
