Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.
Require Import VST.progs.object.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Local Open Scope Z.
Local Open Scope logic.

Definition object_invariant := list Z -> val -> mpred.

Definition tobject := tptr (Tstruct _object noattr).

Definition reset_spec (instance: object_invariant) :=
  WITH self: val, history: list Z
  PRE [ _self OF tobject]
          PROP ()
          LOCAL (temp _self self)
          SEP (instance history self)
  POST [ tvoid ]
          PROP() LOCAL () SEP(instance nil self).

Definition twiddle_spec (instance: object_invariant) :=
  WITH self: val, i: Z, history: list Z
  PRE [ _self OF tobject, _i OF tint]
          PROP (0 < i <= Int.max_signed / 4;
                0 <= fold_right Z.add 0 history <= Int.max_signed / 4)
          LOCAL (temp _self self; temp _i (Vint (Int.repr i)))
          SEP (instance history self)
  POST [ tint ]
      EX v: Z, 
          PROP(2* fold_right Z.add 0 history < v <= 2* fold_right Z.add 0 (i::history))
          LOCAL (temp ret_temp (Vint (Int.repr v))) 
          SEP(instance (i::history) self).

Definition object_methods (instance: object_invariant) (mtable: val) : mpred :=
  EX sh: share, EX reset: val, EX twiddle: val,
  !! readable_share sh && 
  func_ptr' (reset_spec instance) reset *
  func_ptr' (twiddle_spec instance) twiddle *
  data_at sh (Tstruct _methods noattr) (reset,twiddle) mtable.

Lemma object_methods_local_facts: forall instance p,
  object_methods instance p |-- !! isptr p.
Proof.
(* Goal: forall (sh : share) (instance : object_invariant) (reset twiddle mtable : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (func_ptr' (reset_spec instance) reset) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) mtable)) (object_methods instance mtable) *)
intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (func_ptr' (reset_spec instance) reset) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) mtable)) (object_methods instance mtable) *)
unfold object_methods.
(* Goal: @derives mpred Nveric (@exp mpred Nveric share (fun sh : share => @exp mpred Nveric val (fun reset : val => @exp mpred Nveric val (fun twiddle : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share sh)) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m))))) (@sepcon mpred Nveric Sveric (@exp mpred Nveric share (fun sh : share => @exp mpred Nveric val (fun reset : val => @exp mpred Nveric val (fun twiddle : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share sh)) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m))))) (@exp mpred Nveric share (fun sh : share => @exp mpred Nveric val (fun reset : val => @exp mpred Nveric val (fun twiddle : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share sh)) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m)))))) *)
Intros sh reset twiddle.
(* 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
entailer!.
Qed.
Hint Resolve object_methods_local_facts : saturate_local.

Definition object_mpred (history: list Z) (self: val) : mpred :=
  EX instance: object_invariant, EX mtable: val, 
       (object_methods instance mtable *
     field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable self*
     instance history self).

Definition foo_invariant : object_invariant :=
  (fun (history: list Z) p =>
    withspacer Ews (sizeof size_t + sizeof tint) (2 * sizeof size_t) (field_at Ews (Tstruct _foo_object noattr) 
            [StructField _data] (Vint (Int.repr (2*fold_right Z.add 0 history)))) p
      *  malloc_token Ews (Tstruct _foo_object noattr) p).

Definition foo_reset_spec :=
 DECLARE _foo_reset (reset_spec foo_invariant).

Definition foo_twiddle_spec :=
 DECLARE _foo_twiddle  (twiddle_spec foo_invariant).

Definition make_foo_spec :=
 DECLARE _make_foo
 WITH gv: globals
 PRE [ ]
    PROP () LOCAL (gvars gv) 
    SEP (mem_mgr gv; object_methods foo_invariant (gv _foo_methods))
 POST [ tobject ]
    EX p: val, PROP () LOCAL (temp ret_temp p)
     SEP (mem_mgr gv; object_mpred nil p; object_methods foo_invariant (gv _foo_methods)).

Definition main_spec :=
 DECLARE _main
  WITH gv: globals
  PRE  [] main_pre prog nil gv
  POST [ tint ]
     EX i:Z, PROP(0<=i<=6) LOCAL (temp ret_temp (Vint (Int.repr i))) SEP(TT).

Definition Gprog : funspecs :=   ltac:(with_library prog [
    foo_reset_spec; foo_twiddle_spec; make_foo_spec; main_spec]).

Lemma object_mpred_i:
  forall (history: list Z) (self: val) (instance: object_invariant) (mtable: val),
    object_methods instance mtable *
     field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable self *
     instance history self 
    |-- object_mpred history self.
Proof.
(* Goal: forall (sh : share) (instance : object_invariant) (reset twiddle mtable : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (func_ptr' (reset_spec instance) reset) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) mtable)) (object_methods instance mtable) *)
intros. unfold object_mpred. Exists instance mtable; auto.
Qed.

Lemma body_foo_reset: semax_body Vprog Gprog f_foo_reset foo_reset_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_foo_reset foo_reset_spec *)
unfold foo_reset_spec, foo_invariant, reset_spec.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _self self) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (withspacer Ews (Z.add (@sizeof (@cenv_cs CompSpecs) size_t) (@sizeof (@cenv_cs CompSpecs) tint)) (Z.mul (Zpos (xO xH)) (@sizeof (@cenv_cs CompSpecs) size_t)) (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history))))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)) (@nil mpred))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _self (tptr (Tstruct _foo_object noattr))) (Tstruct _foo_object noattr)) _data tint) (Econst_int (Int.repr Z0) tint)) MORE_COMMANDS) POSTCONDITION *)
unfold withspacer; simpl; Intros.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward.  (* self->data=0; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward.  (* return; *)
(* 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
all: unfold withspacer; simpl; entailer!.  (* needed if Archi.ptr64=true *)
Qed.

Lemma body_foo_twiddle: semax_body Vprog Gprog f_foo_twiddle foo_twiddle_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_foo_twiddle foo_twiddle_spec *)
unfold foo_twiddle_spec, foo_invariant, twiddle_spec.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
start_function.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) i) (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history))))) self) (withspacer Ews (Zpos (xO (xO (xO xH)))) (Zpos (xO (xO (xO xH)))) (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) i) (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)))))) self) *)
unfold withspacer; simpl.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _self self) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)) (@nil mpred))))) (Ssequence (Sset _d (Efield (Ederef (Etempvar _self (tptr (Tstruct _foo_object noattr))) (Tstruct _foo_object noattr)) _data tint)) MORE_COMMANDS) POSTCONDITION *)
Intros.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward.  (* d = self->data; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward.  (* self -> data = d+2*i; *) 
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) (Z.mul (Zpos (xO xH)) i)))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)) (@prop mpred Nveric (and (Z.le Int.min_signed (Z.add (Int.signed (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)))) (Int.signed (Int.repr i)))) (Z.le (Z.add (Int.signed (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)))) (Int.signed (Int.repr i))) Int.max_signed))) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) (Z.mul (Zpos (xO xH)) i)))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)) (@exp mpred Nveric Z (fun a : Z => @andp mpred Nveric (@prop mpred Nveric (and (and (Z.lt (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) a) (Z.le a (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z i history))))) (@eq val (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) i))) (Vint (Int.repr a))))) (@sepcon mpred Nveric Sveric (withspacer Ews (Z.add (@sizeof (@cenv_cs CompSpecs) size_t) (@sizeof (@cenv_cs CompSpecs) tint)) (Z.mul (Zpos (xO xH)) (@sizeof (@cenv_cs CompSpecs) size_t)) (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z i history)))))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)))) *)
 set (j:= Int.max_signed / 4) in *; compute in j; subst j.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) (Z.mul (Zpos (xO xH)) i)))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)) (@prop mpred Nveric (and (Z.le Int.min_signed (Z.add (Int.signed (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)))) (Int.signed (Int.repr i)))) (Z.le (Z.add (Int.signed (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)))) (Int.signed (Int.repr i))) Int.max_signed))) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) (Z.mul (Zpos (xO xH)) i)))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)) (@exp mpred Nveric Z (fun a : Z => @andp mpred Nveric (@prop mpred Nveric (and (and (Z.lt (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) a) (Z.le a (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z i history))))) (@eq val (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) i))) (Vint (Int.repr a))))) (@sepcon mpred Nveric Sveric (withspacer Ews (Z.add (@sizeof (@cenv_cs CompSpecs) size_t) (@sizeof (@cenv_cs CompSpecs) tint)) (Z.mul (Zpos (xO xH)) (@sizeof (@cenv_cs CompSpecs) size_t)) (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z i history)))))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)))) *)
 forget (fold_right Z.add 0 history) as h.
(* 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
 entailer!.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward.  (* return d+i; *)
(* Goal: and (and (Z.lt Z0 (Zpos (xI xH))) (Z.le (Zpos (xI xH)) (Z.div Int.max_signed (Zpos (xO (xO xH)))))) (and (Z.le Z0 (@fold_right Z Z Z.add Z0 (@nil Z))) (Z.le (@fold_right Z Z Z.add Z0 (@nil Z)) (Z.div Int.max_signed (Zpos (xO (xO xH)))))) *)
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun vret : Z => PROPx (@cons Prop (and (Z.lt (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@nil Z))) vret) (Z.le vret (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z (Zpos (xI xH)) (@nil Z)))))) (@nil Prop)) (LOCALx (@cons localdef (temp _i (Vint (Int.repr vret))) (@cons localdef (temp _p_twiddle t0) (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))))) (SEPx (@cons mpred (instance (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (func_ptr' (reset_spec instance) r0) (@cons mpred (func_ptr' (twiddle_spec instance) t0) (@cons mpred (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val r0 t0) mtable0) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred)))))))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
simpl.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) (Z.mul (Zpos (xO xH)) i)))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)) (@prop mpred Nveric (and (Z.le Int.min_signed (Z.add (Int.signed (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)))) (Int.signed (Int.repr i)))) (Z.le (Z.add (Int.signed (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)))) (Int.signed (Int.repr i))) Int.max_signed))) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) (Z.mul (Zpos (xO xH)) i)))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)) (@exp mpred Nveric Z (fun a : Z => @andp mpred Nveric (@prop mpred Nveric (and (and (Z.lt (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) a) (Z.le a (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z i history))))) (@eq val (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) i))) (Vint (Int.repr a))))) (@sepcon mpred Nveric Sveric (withspacer Ews (Z.add (@sizeof (@cenv_cs CompSpecs) size_t) (@sizeof (@cenv_cs CompSpecs) tint)) (Z.mul (Zpos (xO xH)) (@sizeof (@cenv_cs CompSpecs) size_t)) (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z i history)))))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)))) *)
 set (j:= Int.max_signed / 4) in *; compute in j; subst j.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) (Z.mul (Zpos (xO xH)) i)))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)) (@prop mpred Nveric (and (Z.le Int.min_signed (Z.add (Int.signed (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)))) (Int.signed (Int.repr i)))) (Z.le (Z.add (Int.signed (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)))) (Int.signed (Int.repr i))) Int.max_signed))) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) (Z.mul (Zpos (xO xH)) i)))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)) (@exp mpred Nveric Z (fun a : Z => @andp mpred Nveric (@prop mpred Nveric (and (and (Z.lt (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) a) (Z.le a (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z i history))))) (@eq val (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) i))) (Vint (Int.repr a))))) (@sepcon mpred Nveric Sveric (withspacer Ews (Z.add (@sizeof (@cenv_cs CompSpecs) size_t) (@sizeof (@cenv_cs CompSpecs) tint)) (Z.mul (Zpos (xO xH)) (@sizeof (@cenv_cs CompSpecs) size_t)) (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z i history)))))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)))) *)
 forget (fold_right Z.add 0 history) as h.
(* 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
 entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) (Z.mul (Zpos (xO xH)) i)))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)) (@exp mpred Nveric Z (fun a : Z => @andp mpred Nveric (@prop mpred Nveric (and (and (Z.lt (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) a) (Z.le a (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z i history))))) (@eq val (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) i))) (Vint (Int.repr a))))) (@sepcon mpred Nveric Sveric (withspacer Ews (Z.add (@sizeof (@cenv_cs CompSpecs) size_t) (@sizeof (@cenv_cs CompSpecs) tint)) (Z.mul (Zpos (xO xH)) (@sizeof (@cenv_cs CompSpecs) size_t)) (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z i history)))))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)))) *)
Exists (2 * fold_right Z.add 0 history + i).
simpl;
(* 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
entailer!.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)) (Z.mul (Zpos (xO xH)) i)))) self) (withspacer Ews (Zpos (xO (xO (xO xH)))) (Zpos (xO (xO (xO xH)))) (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.mul (Zpos (xO xH)) (Z.add i (@fold_right Z Z Z.add Z0 history)))))) self) *)
rewrite Z.mul_add_distr_l, Z.add_comm.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) i) (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history))))) self) (withspacer Ews (Zpos (xO (xO (xO xH)))) (Zpos (xO (xO (xO xH)))) (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) i) (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)))))) self) *)
unfold withspacer; simpl.
(* 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
entailer!.
Qed.

Lemma split_object_methods:
  forall instance m, 
    object_methods instance m |-- object_methods instance m * object_methods instance m.
Proof.
(* Goal: forall (sh : share) (instance : object_invariant) (reset twiddle mtable : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (func_ptr' (reset_spec instance) reset) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) mtable)) (object_methods instance mtable) *)
intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (func_ptr' (reset_spec instance) reset) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) mtable)) (object_methods instance mtable) *)
unfold object_methods.
(* Goal: @derives mpred Nveric (@exp mpred Nveric share (fun sh : share => @exp mpred Nveric val (fun reset : val => @exp mpred Nveric val (fun twiddle : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share sh)) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m))))) (@sepcon mpred Nveric Sveric (@exp mpred Nveric share (fun sh : share => @exp mpred Nveric val (fun reset : val => @exp mpred Nveric val (fun twiddle : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share sh)) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m))))) (@exp mpred Nveric share (fun sh : share => @exp mpred Nveric val (fun reset : val => @exp mpred Nveric val (fun twiddle : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share sh)) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m)))))) *)
Intros sh reset twiddle.

(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (func_ptr' (reset_spec instance) reset) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m)) (@sepcon mpred Nveric Sveric (@exp mpred Nveric share (fun sh : share => @exp mpred Nveric val (fun reset : val => @exp mpred Nveric val (fun twiddle : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share sh)) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m))))) (@exp mpred Nveric share (fun sh : share => @exp mpred Nveric val (fun reset : val => @exp mpred Nveric val (fun twiddle : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share sh)) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m)))))) *)
Exists (fst (slice.cleave sh)) reset twiddle.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (func_ptr' (reset_spec instance) reset) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share (@fst Share.t Share.t (slice.cleave sh)))) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs (@fst Share.t Share.t (slice.cleave sh)) (Tstruct _methods noattr) (@pair val val reset twiddle) m)) (@exp mpred Nveric share (fun sh : share => @exp mpred Nveric val (fun reset : val => @exp mpred Nveric val (fun twiddle : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share sh)) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m)))))) *)
Exists (snd (slice.cleave sh)) reset twiddle.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (func_ptr' (reset_spec instance) reset) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share (@fst Share.t Share.t (slice.cleave sh)))) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs (@fst Share.t Share.t (slice.cleave sh)) (Tstruct _methods noattr) (@pair val val reset twiddle) m)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share (@snd Share.t Share.t (slice.cleave sh)))) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs (@snd Share.t Share.t (slice.cleave sh)) (Tstruct _methods noattr) (@pair val val reset twiddle) m))) *)
rewrite (split_func_ptr' (reset_spec instance) reset) at 1.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (func_ptr' (reset_spec instance) reset) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share (@fst Share.t Share.t (slice.cleave sh)))) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs (@fst Share.t Share.t (slice.cleave sh)) (Tstruct _methods noattr) (@pair val val reset twiddle) m)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share (@snd Share.t Share.t (slice.cleave sh)))) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs (@snd Share.t Share.t (slice.cleave sh)) (Tstruct _methods noattr) (@pair val val reset twiddle) m))) *)
rewrite (split_func_ptr' (twiddle_spec instance) twiddle) at 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
entailer!.
(* Goal: and (readable_share (@fst Share.t Share.t (slice.cleave sh))) (readable_share (@snd Share.t Share.t (slice.cleave sh))) *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@sepcon mpred Nveric Sveric (@data_at CompSpecs (@fst Share.t Share.t (slice.cleave sh)) (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@data_at CompSpecs (@snd Share.t Share.t (slice.cleave sh)) (Tstruct _methods noattr) (@pair val val reset twiddle) m)) *)
split.
(* Goal: readable_share (@fst Share.t Share.t (slice.cleave sh)) *)
(* Goal: readable_share (@snd Share.t Share.t (slice.cleave sh)) *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@sepcon mpred Nveric Sveric (@data_at CompSpecs (@fst Share.t Share.t (slice.cleave sh)) (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@data_at CompSpecs (@snd Share.t Share.t (slice.cleave sh)) (Tstruct _methods noattr) (@pair val val reset twiddle) m)) *)
apply slice.cleave_readable1; auto.
(* Goal: readable_share (@snd Share.t Share.t (slice.cleave sh)) *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@sepcon mpred Nveric Sveric (@data_at CompSpecs (@fst Share.t Share.t (slice.cleave sh)) (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@data_at CompSpecs (@snd Share.t Share.t (slice.cleave sh)) (Tstruct _methods noattr) (@pair val val reset twiddle) m)) *)
apply slice.cleave_readable2; auto.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@sepcon mpred Nveric Sveric (@data_at CompSpecs (@fst Share.t Share.t (slice.cleave sh)) (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@data_at CompSpecs (@snd Share.t Share.t (slice.cleave sh)) (Tstruct _methods noattr) (@pair val val reset twiddle) m)) *)
rewrite (data_at_share_join (fst (slice.cleave sh)) (snd (slice.cleave sh)) sh).
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) *)
(* Goal: @sepalg.join Share.t Share.Join_ba (@fst Share.t Share.t (slice.cleave sh)) (@snd Share.t Share.t (slice.cleave sh)) sh *)
auto.
(* Goal: @sepalg.join Share.t Share.Join_ba (@fst Share.t Share.t (slice.cleave sh)) (@snd Share.t Share.t (slice.cleave sh)) sh *)
apply slice.cleave_join.
Qed.

Lemma body_make_foo: semax_body Vprog Gprog f_make_foo make_foo_spec.
Proof.
unfold make_foo_spec.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
start_function.
forward_call (Tstruct _foo_object noattr, gv).
   split3; simpl; auto; computable.
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun vret : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p vret) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (object_mpred (@nil Z) vret) (@cons mpred (object_methods foo_invariant (gv _foo_methods)) (@nil mpred)))))))) (Ssequence (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_reset (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default)))) (Ssequence (Scall (@None ident) (Etempvar _p_reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@nil expr))) (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint))))))))) MORE_COMMANDS) POSTCONDITION *)
Intros p.
forward_if
  (PROP ( )
   LOCAL (temp _p p; gvars gv)
   SEP (mem_mgr gv;
          malloc_token Ews (Tstruct _foo_object noattr) p;
          data_at_ Ews (Tstruct _foo_object noattr) p;
          object_methods foo_invariant (gv _foo_methods))).
*
change (Memory.EqDec_val p nullval) with (eq_dec p nullval).
(* 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
if_tac; entailer!.
*
forward_call tt.
contradiction.
*
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) *)
(* Goal: @sepalg.join Share.t Share.Join_ba (@fst Share.t Share.t (slice.cleave sh)) (@snd Share.t Share.t (slice.cleave sh)) sh *)
rewrite if_false by auto.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _self self) (@cons localdef (temp _i (Vint (Int.repr i))) (@nil localdef))) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)))) self) (@malloc_token CompSpecs Ews (Tstruct _foo_object noattr) self)) (@nil mpred))))) (Ssequence (Sset _d (Efield (Ederef (Etempvar _self (tptr (Tstruct _foo_object noattr))) (Tstruct _foo_object noattr)) _data tint)) MORE_COMMANDS) POSTCONDITION *)
Intros.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward.  (*  /*skip*/;  *)
(* 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
entailer!.
*
(* Goal: and (and (Z.lt Z0 (Zpos (xI xH))) (Z.le (Zpos (xI xH)) (Z.div Int.max_signed (Zpos (xO (xO xH)))))) (and (Z.le Z0 (@fold_right Z Z Z.add Z0 (@nil Z))) (Z.le (@fold_right Z Z Z.add Z0 (@nil Z)) (Z.div Int.max_signed (Zpos (xO (xO xH)))))) *)
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun vret : Z => PROPx (@cons Prop (and (Z.lt (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@nil Z))) vret) (Z.le vret (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z (Zpos (xI xH)) (@nil Z)))))) (@nil Prop)) (LOCALx (@cons localdef (temp _i (Vint (Int.repr vret))) (@cons localdef (temp _p_twiddle t0) (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))))) (SEPx (@cons mpred (instance (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (func_ptr' (reset_spec instance) r0) (@cons mpred (func_ptr' (twiddle_spec instance) t0) (@cons mpred (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val r0 t0) mtable0) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred)))))))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
unfold data_at_, field_at_, default_val; simpl.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward. (* p->mtable = &foo_methods; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward. (* p->data = 0; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward. (* return (struct object * ) p; *)
Exists p.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@nil Z) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint)))))) MORE_COMMANDS) POSTCONDITION *)
unfold object_mpred.
Exists foo_invariant (gv _foo_methods).
sep_apply (split_object_methods foo_invariant (gv _foo_methods)).
unfold foo_invariant at 4.
(* 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
entailer!.
(* Goal: and (and (Z.lt Z0 (Zpos (xI xH))) (Z.le (Zpos (xI xH)) (Z.div Int.max_signed (Zpos (xO (xO xH)))))) (and (Z.le Z0 (@fold_right Z Z Z.add Z0 (@nil Z))) (Z.le (@fold_right Z Z Z.add Z0 (@nil Z)) (Z.div Int.max_signed (Zpos (xO (xO xH)))))) *)
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun vret : Z => PROPx (@cons Prop (and (Z.lt (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@nil Z))) vret) (Z.le vret (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z (Zpos (xI xH)) (@nil Z)))))) (@nil Prop)) (LOCALx (@cons localdef (temp _i (Vint (Int.repr vret))) (@cons localdef (temp _p_twiddle t0) (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))))) (SEPx (@cons mpred (instance (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (func_ptr' (reset_spec instance) r0) (@cons mpred (func_ptr' (twiddle_spec instance) t0) (@cons mpred (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val r0 t0) mtable0) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred)))))))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
simpl.
unfold_data_at (field_at _ _ nil _ p).
cancel.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) i) (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history))))) self) (withspacer Ews (Zpos (xO (xO (xO xH)))) (Zpos (xO (xO (xO xH)))) (@field_at CompSpecs Ews (Tstruct _foo_object noattr) (@cons gfield (StructField _data) (@nil gfield)) (Vint (Int.repr (Z.add (Z.mul (Zpos (xO xH)) i) (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 history)))))) self) *)
unfold withspacer; simpl.
rewrite !field_at_data_at.
(* Goal: and (and (Z.lt Z0 (Zpos (xI xH))) (Z.le (Zpos (xI xH)) (Z.div Int.max_signed (Zpos (xO (xO xH)))))) (and (Z.le Z0 (@fold_right Z Z Z.add Z0 (@nil Z))) (Z.le (@fold_right Z Z Z.add Z0 (@nil Z)) (Z.div Int.max_signed (Zpos (xO (xO xH)))))) *)
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun vret : Z => PROPx (@cons Prop (and (Z.lt (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@nil Z))) vret) (Z.le vret (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z (Zpos (xI xH)) (@nil Z)))))) (@nil Prop)) (LOCALx (@cons localdef (temp _i (Vint (Int.repr vret))) (@cons localdef (temp _p_twiddle t0) (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))))) (SEPx (@cons mpred (instance (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (func_ptr' (reset_spec instance) r0) (@cons mpred (func_ptr' (twiddle_spec instance) t0) (@cons mpred (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val r0 t0) mtable0) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred)))))))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
simpl.
apply derives_refl'.
rewrite <- ?sepcon_assoc. (* needed if Archi.ptr64=true *)
rewrite !field_compatible_field_address; auto with field_compatible.
clear - H.
(* TODO: simplify the following proof. *)
destruct p; try contradiction.
destruct H as [AL SZ].
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) *)
(* Goal: @sepalg.join Share.t Share.Join_ba (@fst Share.t Share.t (slice.cleave sh)) (@snd Share.t Share.t (slice.cleave sh)) sh *)
repeat split; auto.
simpl in *; omega.
eapply align_compatible_rec_Tstruct; [reflexivity |].
(* Goal: forall (sh : share) (instance : object_invariant) (reset twiddle mtable : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (func_ptr' (reset_spec instance) reset) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) mtable)) (object_methods instance mtable) *)
simpl co_members; intros.
simpl in H.
if_tac in H; [| inv H].
inv H. inv H0.
eapply align_compatible_rec_by_value.
reflexivity.
rewrite Z.add_0_r.
(* Goal: and (and (Z.lt Z0 (Zpos (xI xH))) (Z.le (Zpos (xI xH)) (Z.div Int.max_signed (Zpos (xO (xO xH)))))) (and (Z.le Z0 (@fold_right Z Z Z.add Z0 (@nil Z))) (Z.le (@fold_right Z Z Z.add Z0 (@nil Z)) (Z.div Int.max_signed (Zpos (xO (xO xH)))))) *)
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun vret : Z => PROPx (@cons Prop (and (Z.lt (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@nil Z))) vret) (Z.le vret (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z (Zpos (xI xH)) (@nil Z)))))) (@nil Prop)) (LOCALx (@cons localdef (temp _i (Vint (Int.repr vret))) (@cons localdef (temp _p_twiddle t0) (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))))) (SEPx (@cons mpred (instance (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (func_ptr' (reset_spec instance) r0) (@cons mpred (func_ptr' (twiddle_spec instance) t0) (@cons mpred (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val r0 t0) mtable0) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred)))))))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
simpl.
unfold natural_alignment in AL.
eapply Z.divide_trans; [ | apply AL].
apply prove_Zdivide.
reflexivity.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) *)
(* Goal: @sepalg.join Share.t Share.Join_ba (@fst Share.t Share.t (slice.cleave sh)) (@snd Share.t Share.t (slice.cleave sh)) sh *)
left; auto.
Qed.


Lemma make_object_methods:
  forall sh instance reset twiddle mtable,
  readable_share sh ->
  func_ptr' (reset_spec instance) reset *
  func_ptr' (twiddle_spec instance) twiddle *
  data_at sh (Tstruct _methods noattr) (reset, twiddle) mtable
  |-- object_methods instance mtable.
Proof.
(* Goal: forall (sh : share) (instance : object_invariant) (reset twiddle mtable : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (func_ptr' (reset_spec instance) reset) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) mtable)) (object_methods instance mtable) *)
  intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (func_ptr' (reset_spec instance) reset) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) mtable)) (object_methods instance mtable) *)
  unfold object_methods.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (func_ptr' (reset_spec instance) reset) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) mtable)) (@exp mpred Nveric share (fun sh : share => @exp mpred Nveric val (fun reset : val => @exp mpred Nveric val (fun twiddle : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share sh)) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) mtable))))) *)
  Exists sh reset twiddle.
(* 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
  entailer!.
Qed.

Ltac method_call witness hist' result :=
repeat apply seq_assoc1;
match goal with 
   |- semax _ (PROPx _ (LOCALx ?Q (SEPx ?R))) 
            (Ssequence (Sset ?mt (Efield (Ederef (Etempvar ?x _)  _) _ _))
                 _) _  =>
    match Q with context [temp ?x ?x'] =>
     match R with context [object_mpred _ x'] =>
          let instance := fresh "instance" in let mtable := fresh "mtable" in
          unfold object_mpred; Intros instance mtable;
          forward;
          unfold object_methods at 1; 
          let sh := fresh "sh" in let r := fresh "r" in let t := fresh "t" in
          Intros sh r t;
          forward;
          forward_call witness;
          [ .. | try Intros result;
                  sep_apply (make_object_methods sh instance r t mtable); [ auto .. | ];
                  sep_apply (object_mpred_i hist' x' instance mtable);
                  deadvars; try clear dependent sh; try clear r; try clear t
           ]
    end end
end.

Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH (mk_attr false (@None N))) (mk_attr false (@None N))) (Tcons (Tint I32 Signed (mk_attr false (@None N))) Tnil)) (Tint I32 Signed (mk_attr false (@None N))) (mkcallconv false false false)) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@cons mpred (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH (mk_attr false (@None N))) (mk_attr false (@None N))) Tnil) Tvoid (mkcallconv false false false)) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods)) (@nil mpred)))))) (Ssequence (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _make_foo (Tfunction Tnil (tptr (Tstruct _object noattr)) cc_default)) (@nil expr)) (Sset _p (Etempvar _t'1 (tptr (Tstruct _object noattr))))) (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_reset (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default)))) (Ssequence (Scall (@None ident) (Etempvar _p_reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@nil expr))) (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint)))))))))) MORE_COMMANDS) POSTCONDITION *)
sep_apply (create_mem_mgr gv).
(* assert_gvar _foo_methods. (* TODO: this is needed for a field_compatible later on *) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH (mk_attr false (@None N))) (mk_attr false (@None N))) (Tcons (Tint I32 Signed (mk_attr false (@None N))) Tnil)) (Tint I32 Signed (mk_attr false (@None N))) (mkcallconv false false false)) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@cons mpred (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH (mk_attr false (@None N))) (mk_attr false (@None N))) Tnil) Tvoid (mkcallconv false false false)) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods)) (@nil mpred))))))) (Ssequence (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _make_foo (Tfunction Tnil (tptr (Tstruct _object noattr)) cc_default)) (@nil expr)) (Sset _p (Etempvar _t'1 (tptr (Tstruct _object noattr))))) (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_reset (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default)))) (Ssequence (Scall (@None ident) (Etempvar _p_reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@nil expr))) (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint)))))))))) MORE_COMMANDS) POSTCONDITION *)
fold noattr cc_default.

(* 0. This part should be handled automatically by start_function *)
gather_SEP 1 2; 
replace_SEP 0 (data_at Ews (Tstruct _methods noattr) 
(* 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods)) (@cons mpred (mem_mgr gv) (@nil mpred)))))) (Ssequence (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _make_foo (Tfunction Tnil (tptr (Tstruct _object noattr)) cc_default)) (@nil expr)) (Sset _p (Etempvar _t'1 (tptr (Tstruct _object noattr))))) (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_reset (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default)))) (Ssequence (Scall (@None ident) (Etempvar _p_reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@nil expr))) (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint)))))))))) MORE_COMMANDS) POSTCONDITION *)
   (gv _foo_reset, gv _foo_twiddle) (gv _foo_methods)). {
(* 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
  entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (gv _foo_twiddle)) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (gv _foo_reset) (gv _foo_methods))) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods)) *)
  unfold_data_at (data_at _ (Tstruct _methods _) _ (gv _foo_methods)).
  rewrite <- mapsto_field_at with (gfs := [StructField _twiddle]) (v:= (gv _foo_twiddle))
  by  auto with field_compatible.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (gv _foo_twiddle)) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (gv _foo_reset) (gv _foo_methods))) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _methods noattr) (@cons gfield (StructField _reset) (@nil gfield)) (gv _foo_reset) (gv _foo_methods)) (mapsto Ews (@nested_field_type CompSpecs (Tstruct _methods noattr) (@cons gfield (StructField _twiddle) (@nil gfield))) (@field_address CompSpecs (Tstruct _methods noattr) (@cons gfield (StructField _twiddle) (@nil gfield)) (gv _foo_methods)) (gv _foo_twiddle))) *)
  rewrite field_at_data_at.  rewrite !field_compatible_field_address by auto with field_compatible.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) *)
(* Goal: @sepalg.join Share.t Share.Join_ba (@fst Share.t Share.t (slice.cleave sh)) (@snd Share.t Share.t (slice.cleave sh)) sh *)
  rewrite !isptr_offset_val_zero by auto.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (gv _foo_twiddle)) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (gv _foo_reset) (gv _foo_methods))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews (@nested_field_type CompSpecs (Tstruct _methods noattr) (@cons gfield (StructField _reset) (@nil gfield))) (gv _foo_reset) (gv _foo_methods)) (mapsto Ews (@nested_field_type CompSpecs (Tstruct _methods noattr) (@cons gfield (StructField _twiddle) (@nil gfield))) (offset_val (@nested_field_offset CompSpecs (Tstruct _methods noattr) (@cons gfield (StructField _twiddle) (@nil gfield))) (gv _foo_methods)) (gv _foo_twiddle))) *)
  rewrite sepcon_comm.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (gv _foo_reset) (gv _foo_methods)) (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (gv _foo_twiddle))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews (@nested_field_type CompSpecs (Tstruct _methods noattr) (@cons gfield (StructField _reset) (@nil gfield))) (gv _foo_reset) (gv _foo_methods)) (mapsto Ews (@nested_field_type CompSpecs (Tstruct _methods noattr) (@cons gfield (StructField _twiddle) (@nil gfield))) (offset_val (@nested_field_offset CompSpecs (Tstruct _methods noattr) (@cons gfield (StructField _twiddle) (@nil gfield))) (gv _foo_methods)) (gv _foo_twiddle))) *)
  apply derives_refl.
}

(* 1. Prove that [mtable] is a proper method-table for foo-objects *)

(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods)) (@cons mpred (mem_mgr gv) (@nil mpred)))))) (Ssequence (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _make_foo (Tfunction Tnil (tptr (Tstruct _object noattr)) cc_default)) (@nil expr)) (Sset _p (Etempvar _t'1 (tptr (Tstruct _object noattr))))) (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_reset (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default)))) (Ssequence (Scall (@None ident) (Etempvar _p_reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@nil expr))) (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint)))))))))) MORE_COMMANDS) POSTCONDITION *)
make_func_ptr _foo_twiddle.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (func_ptr' (twiddle_spec foo_invariant) (gv _foo_twiddle)) (@cons mpred (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods)) (@cons mpred (mem_mgr gv) (@nil mpred))))))) (Ssequence (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _make_foo (Tfunction Tnil (tptr (Tstruct _object noattr)) cc_default)) (@nil expr)) (Sset _p (Etempvar _t'1 (tptr (Tstruct _object noattr))))) (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_reset (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default)))) (Ssequence (Scall (@None ident) (Etempvar _p_reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@nil expr))) (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint)))))))))) MORE_COMMANDS) POSTCONDITION *)
make_func_ptr _foo_reset.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) *)
(* Goal: @sepalg.join Share.t Share.Join_ba (@fst Share.t Share.t (slice.cleave sh)) (@snd Share.t Share.t (slice.cleave sh)) sh *)
sep_apply (make_object_methods Ews foo_invariant(gv _foo_reset) (gv _foo_twiddle) (gv _foo_methods)); auto.

(* 2. Build an instance of class [foo], called [p] *)
forward_call (* p = make_foo(); *)
        gv.
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun vret : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p vret) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (object_mpred (@nil Z) vret) (@cons mpred (object_methods foo_invariant (gv _foo_methods)) (@nil mpred)))))))) (Ssequence (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_reset (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default)))) (Ssequence (Scall (@None ident) (Etempvar _p_reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@nil expr))) (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint))))))))) MORE_COMMANDS) POSTCONDITION *)
Intros p.

(* 3. Done with object_methods for the foreseeable future *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (Freezer.FRZL MT) (@cons mpred (mem_mgr gv) (@cons mpred (object_mpred (@nil Z) p) (@nil mpred))))))) (Ssequence (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_reset (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default)))) (Ssequence (Scall (@None ident) (Etempvar _p_reset (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) Tnil) tvoid cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@nil expr))) (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint))))))))) MORE_COMMANDS) POSTCONDITION *)
freeze [2]  MT. gather_SEP 1.

(* Illustration of an alternate method to prove the method calls.
   Method 1:  comment out lines AA and BB and the entire range CC-DD.
   Method 2:  comment out lines AA-BB, inclusive.
*)

(* AA *) try (tryif 
  (method_call (p, @nil Z) (@nil Z) whatever;
   method_call (p, 3, @nil Z) [3%Z] i;
     [simpl; computable | ])
(* BB *)  then fail else fail 99)
  .

(* CC *)
(* 4. first method-call *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@nil Z) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint)))))) MORE_COMMANDS) POSTCONDITION *)
unfold object_mpred.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@exp mpred Nveric object_invariant (fun instance : object_invariant => @exp mpred Nveric val (fun mtable : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (object_methods instance mtable) (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable p)) (instance (@nil Z) p)))) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint)))))) MORE_COMMANDS) POSTCONDITION *)
Intros instance mtable0.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward. (*  mtable = p->mtable; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (object_methods instance mtable0) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@cons mpred (instance (@nil Z) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))))) (Ssequence (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint))))) MORE_COMMANDS) POSTCONDITION *)
unfold object_methods at 1.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (@exp mpred Nveric share (fun sh : share => @exp mpred Nveric val (fun reset : val => @exp mpred Nveric val (fun twiddle : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share sh)) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) mtable0))))) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@cons mpred (instance (@nil Z) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))))) (Ssequence (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint))))) MORE_COMMANDS) POSTCONDITION *)
Intros sh r0 t0.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward. (* p_reset = mtable->reset; *)
forward_call (* p_reset(p); *)
      (p, @nil Z).
(* Finish the method-call by regathering the object p back together *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) *)
(* Goal: @sepalg.join Share.t Share.Join_ba (@fst Share.t Share.t (slice.cleave sh)) (@snd Share.t Share.t (slice.cleave sh)) sh *)
sep_apply (make_object_methods sh instance r0 t0 mtable0); auto.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p_reset r0) (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef))))) (SEPx (@cons mpred (object_methods instance mtable0) (@cons mpred (instance (@nil Z) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@nil mpred))))))))) (Ssequence (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint)))))) MORE_COMMANDS) POSTCONDITION *)
sep_apply (object_mpred_i [] p instance mtable0).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _p_twiddle t0) (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
deadvars!. clear.

(* 5. second method-call *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@nil Z) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint)))))) MORE_COMMANDS) POSTCONDITION *)
unfold object_mpred.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@exp mpred Nveric object_invariant (fun instance : object_invariant => @exp mpred Nveric val (fun mtable : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (object_methods instance mtable) (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable p)) (instance (@nil Z) p)))) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Ssequence (Sset _mtable (Efield (Ederef (Etempvar _p (tptr (Tstruct _object noattr))) (Tstruct _object noattr)) _mtable (tptr (Tstruct _methods noattr)))) (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint)))))) MORE_COMMANDS) POSTCONDITION *)
Intros instance mtable0.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward.  (* mtable = p->mtable; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (object_methods instance mtable0) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@cons mpred (instance (@nil Z) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))))) (Ssequence (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint))))) MORE_COMMANDS) POSTCONDITION *)
unfold object_methods at 1.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (@exp mpred Nveric share (fun sh : share => @exp mpred Nveric val (fun reset : val => @exp mpred Nveric val (fun twiddle : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (readable_share sh)) (func_ptr' (reset_spec instance) reset)) (func_ptr' (twiddle_spec instance) twiddle)) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) mtable0))))) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@cons mpred (instance (@nil Z) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))))) (Ssequence (Ssequence (Sset _p_twiddle (Efield (Ederef (Etempvar _mtable (tptr (Tstruct _methods noattr))) (Tstruct _methods noattr)) _twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'2) (Etempvar _p_twiddle (tptr (Tfunction (Tcons (tptr (Tstruct _object noattr)) (Tcons tint Tnil)) tint cc_default))) (@cons expr (Etempvar _p (tptr (Tstruct _object noattr))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr)))) (Sset _i (Etempvar _t'2 tint))) (Sreturn (@Some expr (Etempvar _i tint))))) MORE_COMMANDS) POSTCONDITION *)
Intros sh r0 t0.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward.   (* p_twiddle = mtable->twiddle; *)
forward_call (* i = p_twiddle(p,3); *)
      (p, 3, @nil Z).
(* Goal: and (and (Z.lt Z0 (Zpos (xI xH))) (Z.le (Zpos (xI xH)) (Z.div Int.max_signed (Zpos (xO (xO xH)))))) (and (Z.le Z0 (@fold_right Z Z Z.add Z0 (@nil Z))) (Z.le (@fold_right Z Z Z.add Z0 (@nil Z)) (Z.div Int.max_signed (Zpos (xO (xO xH)))))) *)
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun vret : Z => PROPx (@cons Prop (and (Z.lt (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@nil Z))) vret) (Z.le vret (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z (Zpos (xI xH)) (@nil Z)))))) (@nil Prop)) (LOCALx (@cons localdef (temp _i (Vint (Int.repr vret))) (@cons localdef (temp _p_twiddle t0) (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))))) (SEPx (@cons mpred (instance (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (func_ptr' (reset_spec instance) r0) (@cons mpred (func_ptr' (twiddle_spec instance) t0) (@cons mpred (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val r0 t0) mtable0) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred)))))))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
  simpl. computable.
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun vret : Z => PROPx (@cons Prop (and (Z.lt (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@nil Z))) vret) (Z.le vret (Z.mul (Zpos (xO xH)) (@fold_right Z Z Z.add Z0 (@cons Z (Zpos (xI xH)) (@nil Z)))))) (@nil Prop)) (LOCALx (@cons localdef (temp _i (Vint (Int.repr vret))) (@cons localdef (temp _p_twiddle t0) (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))))) (SEPx (@cons mpred (instance (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (func_ptr' (reset_spec instance) r0) (@cons mpred (func_ptr' (twiddle_spec instance) t0) (@cons mpred (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val r0 t0) mtable0) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred)))))))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
Intros i.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _p_twiddle t0) (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))))) (SEPx (@cons mpred (instance (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (func_ptr' (reset_spec instance) r0) (@cons mpred (func_ptr' (twiddle_spec instance) t0) (@cons mpred (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val r0 t0) mtable0) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
simpl in H0.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) (@data_at CompSpecs sh (Tstruct _methods noattr) (@pair val val reset twiddle) m) *)
(* Goal: @sepalg.join Share.t Share.Join_ba (@fst Share.t Share.t (slice.cleave sh)) (@snd Share.t Share.t (slice.cleave sh)) sh *)
sep_apply (make_object_methods sh instance r0 t0 mtable0); auto.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _p_twiddle t0) (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))))) (SEPx (@cons mpred (object_methods instance mtable0) (@cons mpred (instance (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (@field_at CompSpecs Ews (Tstruct _object noattr) (@cons gfield (StructField _mtable) (@nil gfield)) mtable0 p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
sep_apply (object_mpred_i [3] p instance mtable0).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _p_twiddle t0) (@cons localdef (temp _mtable mtable0) (@cons localdef (temp _p p) (@cons localdef (gvars gv) (@nil localdef)))))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
deadvars!. clear - H0.

(* DD *)

(* 6. return *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (object_mpred (@cons Z (Zpos (xI xH)) (@nil Z)) p) (@cons mpred (mem_mgr gv) (@cons mpred (Freezer.FRZL MT) (@nil mpred))))))) (Ssequence (Sreturn (@Some expr (Etempvar _i tint))) MORE_COMMANDS) POSTCONDITION *)
forward.  (* return 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 (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (mapsto Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) (Tcons (Tint I32 Signed noattr) Tnil)) (Tint I32 Signed noattr) cc_default) noattr) (offset_val (Zpos (xO (xO xH))) (gv _foo_methods)) (offset_val Z0 (gv _foo_twiddle))) (@data_at CompSpecs Ews (Tpointer (Tfunction (Tcons (Tpointer (Tstruct xH noattr) noattr) Tnil) Tvoid cc_default) noattr) (offset_val Z0 (gv _foo_reset)) (gv _foo_methods))) (@nil mpred)))))) (@liftx (LiftEnviron mpred) (@data_at CompSpecs Ews (Tstruct _methods noattr) (@pair val val (gv _foo_reset) (gv _foo_twiddle)) (gv _foo_methods))) *)
Exists i; entailer!.
Qed.





