Require Import VST.floyd.proofauto.
Require Import VST.progs.store_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 set22_spec :=
 DECLARE _set22
  WITH pps: val, i: Z, v: int, x11: int, x12: int, x21: int, x22: int, sh : share
  PRE [ _pps OF (tptr pair_pair_t), _i OF tint, _v OF tint]
    PROP  (writable_share sh; 0 <= i < array_size)
    LOCAL (temp _pps pps; temp _i (Vint (Int.repr i)); temp _v (Vint v))
    SEP   (field_at sh (tarray pair_pair_t array_size) [ArraySubsc i] 
                    ((Vint x11, Vint x12), (Vint x21, Vint x22)) pps)
  POST [ tvoid ]
    PROP () LOCAL ()
    SEP   (field_at sh (tarray pair_pair_t array_size) [ArraySubsc i]
                    ((Vint x11, Vint x12), (Vint x21, Vint v)) pps).

Definition fiddle_spec :=
 DECLARE _fiddle
  WITH p: val, n: Z, tag: Z, contents: list Z
  PRE [ _p OF tptr tuint ]
          PROP  (Zlength contents = 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 [ tvoid ]
          PROP () LOCAL ()
          SEP (data_at Ews (tarray tuint (1+n)) 
                      (map Vint (map Int.repr (3::contents)))
                      (offset_val (-sizeof tuint) p)).

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

Lemma body_fiddle: semax_body Vprog Gprog f_fiddle fiddle_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_set22 set22_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 (Sassign (Ederef (Ebinop Oadd (Etempvar _p (tptr tuint)) (Eunop Oneg (Econst_int (Int.repr (Zpos xH)) tint) tint) (tptr tuint)) tuint) (Econst_int (Int.repr (Zpos (xI xH))) tint)) MORE_COMMANDS) POSTCONDITION *)
rename H into LEN.
(* 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 (Sassign (Ederef (Ebinop Oadd (Etempvar _p (tptr tuint)) (Eunop Oneg (Econst_int (Int.repr (Zpos xH)) tint) tint) (tptr tuint)) tuint) (Econst_int (Int.repr (Zpos (xI xH))) tint)) MORE_COMMANDS) POSTCONDITION *)
assert (Zlength (tag :: contents) = 1 + n) as LEN1. {
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (tarray tuint (Z.add (Zpos xH) (@Zlength Z contents))) (@nil gfield) (@cons val (Vint (Int.repr (Zpos (xI xH)))) (@sublist val Z0 (Z.sub (@Zlength val (@cons val (Vint (Int.repr tag)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)))) (Zpos xH)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)))) (offset_val (Z.opp (@sizeof (@cenv_cs CompSpecs) tuint)) p)) (@data_at CompSpecs Ews (tarray tuint (Z.add (Zpos xH) (@Zlength Z contents))) (@cons val (Vint (Int.repr (Zpos (xI xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr contents))) (offset_val (Z.opp (@sizeof (@cenv_cs CompSpecs) tuint)) p)) *)
  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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) pps) (@nil mpred))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint) (Etempvar _v tint)) MORE_COMMANDS) POSTCONDITION *)
assert (N0: 0 <= n). {
(* Goal: @eq Z (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xI xH))))) (Z.add (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xO xH))))) (Zpos (xO (xO xH)))) *)
  pose proof (Zlength_nonneg contents). omega.
}
(* 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 (Sassign (Ederef (Ebinop Oadd (Etempvar _p (tptr tuint)) (Eunop Oneg (Econst_int (Int.repr (Zpos xH)) tint) tint) (tptr tuint)) tuint) (Econst_int (Int.repr (Zpos (xI xH))) tint)) MORE_COMMANDS) POSTCONDITION *)
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)))) 
(* 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) pps) (@nil mpred))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint) (Etempvar _v tint)) MORE_COMMANDS) POSTCONDITION *)
  = 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) 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 (force_val (@sem_add_ptr_int CompSpecs tuint Signed p (force_val (sem_unary_operation Oneg tint (Vint (Int.repr (Zpos xH))))))) (@field_address CompSpecs (tarray tuint (Z.add (Zpos xH) (@Zlength Z contents))) (@cons gfield (ArraySubsc Z0) (@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) (Z.add (Zpos (xO (xO (xO xH)))) (Zpos (xO (xO xH))))) pps) (offset_val (@nested_field_offset CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _snd) (@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.
}

(* Now "forward" succeeds, but leaves a goal open to be proved manually: *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) pps) (@nil mpred))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint) (Etempvar _v tint)) MORE_COMMANDS) POSTCONDITION *)
{ entailer!.
  change (eval_unop Oneg tint (Vint (Int.repr 1))) with (Vint (Int.neg (Int.repr 1))) in H.
  rewrite H0.
  apply isptr_field_address_lemma.
  auto with field_compatible.
}
*)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (tarray tuint (Z.add (Zpos xH) (@Zlength Z contents))) (@nil gfield) (@cons val (Vint (Int.repr (Zpos (xI xH)))) (@sublist val Z0 (Z.sub (@Zlength val (@cons val (Vint (Int.repr tag)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)))) (Zpos xH)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)))) (offset_val (Z.opp (@sizeof (@cenv_cs CompSpecs) tuint)) p)) (@data_at CompSpecs Ews (tarray tuint (Z.add (Zpos xH) (@Zlength Z contents))) (@cons val (Vint (Int.repr (Zpos (xI xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr contents))) (offset_val (Z.opp (@sizeof (@cenv_cs CompSpecs) tuint)) p)) *)
rewrite upd_Znth0. rewrite sublist_1_cons. rewrite Zlength_cons.
(* Goal: @eq Z (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xI xH))))) (Z.add (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xO xH))))) (Zpos (xO (xO xH)))) *)
rewrite ?Zlength_map. replace (Z.succ (Zlength contents) - 1) with (Zlength contents) by omega.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (tarray tuint (Z.add (Zpos xH) (@Zlength Z contents))) (@nil gfield) (@cons val (Vint (Int.repr (Zpos (xI xH)))) (@sublist val Z0 (@Zlength Z contents) (@map Int.int val Vint (@map Z Int.int Int.repr contents)))) (offset_val (Z.opp (@sizeof (@cenv_cs CompSpecs) tuint)) p)) (@data_at CompSpecs Ews (tarray tuint (Z.add (Zpos xH) (@Zlength Z contents))) (@cons val (Vint (Int.repr (Zpos (xI xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr contents))) (offset_val (Z.opp (@sizeof (@cenv_cs CompSpecs) tuint)) p)) *)
rewrite sublist_same by (rewrite ?Zlength_map; reflexivity).
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (tarray tuint (Z.add (Zpos xH) (@Zlength Z contents))) (@nil gfield) (@cons val (Vint (Int.repr (Zpos (xI xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr contents))) (offset_val (Z.opp (@sizeof (@cenv_cs CompSpecs) tuint)) p)) (@data_at CompSpecs Ews (tarray tuint (Z.add (Zpos xH) (@Zlength Z contents))) (@cons val (Vint (Int.repr (Zpos (xI xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr contents))) (offset_val (Z.opp (@sizeof (@cenv_cs CompSpecs) tuint)) p)) *)
apply derives_refl.
Qed.

Lemma body_set22_root_expr: semax_body Vprog Gprog f_set22 set22_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_set22 set22_spec *)
start_function.
(* pps[i].right.snd = 0; // simple: the whole path is exposed in the syntax *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
(* int_pair_t* p = &pps[i].right; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) pps) (@nil mpred))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint) (Etempvar _v 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) pps) (@nil mpred))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint) (Etempvar _v 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) 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) (Z.add (Zpos (xO (xO (xO xH)))) (Zpos (xO (xO xH))))) pps) (offset_val (@nested_field_offset CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _snd) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield))))) pps) *)
  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) (offset_val (@nested_field_offset CompSpecs (tarray pair_pair_t array_size) (@cons gfield (StructField _right) (@cons gfield (ArraySubsc i) (@nil gfield)))) pps) *)
  normalize.
}
(* p->snd = v; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
Qed.

Lemma body_set22_full_expr: semax_body Vprog Gprog f_set22 set22_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_set22 set22_spec *)
start_function.
(* pps[i].right.snd = 0; // simple: the whole path is exposed in the syntax *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
(* int_pair_t* p = &pps[i].right; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) pps) (@nil mpred))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint) (Etempvar _v 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) pps) (@nil mpred))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint) (Etempvar _v 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) 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 Z (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xI xH))))) (Z.add (Z.add (Z.mul (Zpos (xO (xO (xO (xO xH))))) i) (Zpos (xO (xO (xO xH))))) (Zpos (xO (xO xH)))) *)
  simpl. normalize.  f_equal. omega.
}
(* int res = p->snd; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
(* return res; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
Qed.

Lemma body_set22_alt: semax_body Vprog Gprog f_set22 set22_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_set22 set22_spec *)
start_function.
(* pps[i].right.snd = 0; // simple: the whole path is exposed in the syntax *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
(* int_pair_t* p = &pps[i].right; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) pps) (@nil mpred))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint) (Etempvar _v 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) pps) (@nil mpred))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint) (Etempvar _v 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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) 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) *)
  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))) (@cons localdef (temp _v (Vint v)) (@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 (Int.repr Z0)))) pps) (@nil mpred))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _int_pair noattr))) (Tstruct _int_pair noattr)) _snd tint) (Etempvar _v tint)) MORE_COMMANDS) POSTCONDITION *)
rewrite E. clear E.
(* int res = p->snd; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
(* return res; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@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))) (@cons localdef (temp _v (Vint v)) (@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 v))) pps) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
Qed.
