Require Import VST.floyd.proofauto.
Require Import VST.progs.libglob.

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

Local Open Scope logic.

(*  The LG module has two global variables of its own:
<<
int LG_n = 3;
struct foo {  int initialized;  int m; } LG_foo = {0};
>>
From the client's point of view, these variables are hidden
away in a separating conjuct of the form [LG.data n gv],
where [LG.data] is the name of the abstraction,
[n] is a client-visible parameter, and [gv] is the
global-variables table.

In Coq, the LG module defines three things:
 - [LG.data], of type [globals -> mpred] (possibly with some other parameters, in this case [n:Z])
 - [initialized_globals : globals -> mpred]
     This definition is supposed to match the extern initialized
     global variables, as processed by CompCert clightgen,
     for the initial state of LG's variables  [LG_n] and [LG_foo].
 - [initial],  which is a lemma showing that the extern 
      initialized global variables of the C-language LG module do 
      indeed form a legitimate initial state of the [LG.data _ gv]
      abstraction.
*)

Module Type LG_TYPE.
  Parameter data: Z -> globals -> mpred.
  Parameter initialized_globals: globals -> mpred.
  Axiom initial: forall gv, 
     initialized_globals gv |-- data 3 gv.
End LG_TYPE.

(* And here is an implementation of the LG module, satisfying
   this module type. *)

Module LG <: LG_TYPE. 

(* This is an _internal_ definition, not meant to be mentioned
    in proofs about _clients_ of the LG module.  It describes
    "known to be initialized" global LG data. *)
  Definition data_ok (n: Z) (gv: globals) : mpred :=
  !! (0 <= n <= Int.max_signed) &&
  data_at Ews tint (Vint (Int.repr n)) (gv _LG_n) *
  data_at Ews (Tstruct _foo noattr) (Vint Int.one, Vint (Int.repr n)) (gv _LG_foo).

(* This is an externally visible definition, describing global
    LG data whether initialized or not. *)
Definition data (n: Z) (gv: globals) : mpred :=
  data_ok n gv || 
   (!! (n=3) && 
    data_at Ews tint (Vint (Int.repr n)) (gv _LG_n) *
    data_at Ews (Tstruct _foo noattr) (Vint Int.zero, Vundef) (gv _LG_foo)).

(*  This describes the extern global variables of the LG.c file,
    as they would appear as processed by CompCert and Floyd. *)
Definition initialized_globals (gv: globals) := 
   !! (headptr (gv _LG_n)) &&
   !! (headptr (gv _LG_foo)) &&
   mapsto Ews tuint (offset_val 4 (gv _LG_foo))
          (Vint (Int.repr 0)) *
   data_at Ews tuint (Vint (Int.repr 0)) (gv _LG_foo) *
   data_at Ews tuint (Vint (Int.repr 3)) (gv _LG_n).

(*  This lemma packages up the extern global variables of LG.c
   into the client-visible [data] abstraction.  It's a bit clumsy
   and verbose; it would be better to have better proof automation
   support for this kind of thing. *)
Lemma initial:
  forall gv, initialized_globals gv |-- data 3 gv.
Proof.
(* Goal: forall (A : Type) (NA : NatDed A) (P Q : A), @eq A (@orp A NA P Q) (@exp A NA bool (fun b : bool => if b then P else Q)) *)
intros.
(* Goal: @derives mpred Nveric (initialized_globals gv) (data (Zpos (xI xH)) gv) *)
unfold initialized_globals.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (Z.le Z0 n) (Z.le n Int.max_signed))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) *)
entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mapsto Ews tuint (offset_val (Zpos (xO (xO xH))) (gv _LG_foo)) (Vint (Int.repr Z0))) (@data_at CompSpecs Ews tuint (Vint (Int.repr Z0)) (gv _LG_foo))) (@data_at CompSpecs Ews tuint (Vint (Int.repr (Zpos (xI xH)))) (gv _LG_n))) (data (Zpos (xI xH)) gv) *)
unfold data.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mapsto Ews tuint (offset_val (Zpos (xO (xO xH))) (gv _LG_foo)) (Vint (Int.repr Z0))) (@data_at CompSpecs Ews tuint (Vint (Int.repr Z0)) (gv _LG_foo))) (@data_at CompSpecs Ews tuint (Vint (Int.repr (Zpos (xI xH)))) (gv _LG_n))) (@orp mpred Nveric (data_ok (Zpos (xI xH)) gv) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (@eq Z (Zpos (xI xH)) (Zpos (xI xH)))) (@data_at CompSpecs Ews tint (Vint (Int.repr (Zpos (xI xH)))) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.zero) Vundef) (gv _LG_foo)))) *)
apply orp_right2.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (Z.le Z0 n) (Z.le n Int.max_signed))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) *)
entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mapsto Ews tuint (offset_val (Zpos (xO (xO xH))) (gv _LG_foo)) (Vint (Int.repr Z0))) (@data_at CompSpecs Ews tuint (Vint (Int.repr Z0)) (gv _LG_foo))) (@data_at CompSpecs Ews tuint (Vint (Int.repr (Zpos (xI xH)))) (gv _LG_n))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr (Zpos (xI xH)))) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.zero) Vundef) (gv _LG_foo))) *)
rewrite !data_at_tuint_tint.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) (Vint (Int.repr Z0)) (gv _LG_foo)) (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) Vundef (gv _LG_foo)) *)
cancel.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (mapsto Ews tuint (offset_val (Zpos (xO (xO xH))) (gv _LG_foo)) (Vint (Int.repr Z0))) (@data_at CompSpecs Ews tint (Vint (Int.repr Z0)) (gv _LG_foo))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.zero) Vundef) (gv _LG_foo)) *)
unfold_data_at (data_at _ (Tstruct _foo _) _ _).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (mapsto Ews tuint (offset_val (Zpos (xO (xO xH))) (gv _LG_foo)) (Vint (Int.repr Z0))) (@data_at CompSpecs Ews tint (Vint (Int.repr Z0)) (gv _LG_foo))) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _initialized) (@nil gfield)) (Vint Int.zero) (gv _LG_foo)) (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) Vundef (gv _LG_foo))) *)
rewrite sepcon_comm.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr Z0)) (gv _LG_foo)) (mapsto Ews tuint (offset_val (Zpos (xO (xO xH))) (gv _LG_foo)) (Vint (Int.repr Z0)))) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _initialized) (@nil gfield)) (Vint Int.zero) (gv _LG_foo)) (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) Vundef (gv _LG_foo))) *)
apply sepcon_derives.
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews tint (Vint (Int.repr Z0)) (gv _LG_foo)) (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _initialized) (@nil gfield)) (Vint Int.zero) (gv _LG_foo)) *)
(* Goal: @derives mpred Nveric (mapsto Ews tuint (offset_val (Zpos (xO (xO xH))) (gv _LG_foo)) (Vint (Int.repr Z0))) (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) Vundef (gv _LG_foo)) *)
rewrite field_at_data_at.
(* Goal: @derives mpred Nveric (mapsto Ews tuint (offset_val (Zpos (xO (xO xH))) (gv _LG_foo)) (Vint (Int.repr Z0))) (mapsto Ews tint (offset_val (@nested_field_offset CompSpecs (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield))) (gv _LG_foo)) (Vint (Int.repr Z0))) *)
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) (Vint (Int.repr Z0)) (gv _LG_foo)) (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) Vundef (gv _LG_foo)) *)
simpl.
rewrite field_compatible_field_address
  by auto with field_compatible.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) (Vint (Int.repr Z0)) (gv _LG_foo)) (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) Vundef (gv _LG_foo)) *)
simpl. normalize. cancel.
pose (x :=
field_at Ews (Tstruct _foo noattr) [
      StructField _m] (Vint (Int.repr 0)) (gv _LG_foo)).
(* Goal: @derives mpred Nveric (mapsto Ews tuint (offset_val (Zpos (xO (xO xH))) (gv _LG_foo)) (Vint (Int.repr Z0))) (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) Vundef (gv _LG_foo)) *)
apply derives_trans with x; subst x.
erewrite <- mapsto_field_at
  by auto with field_compatible.
(* Goal: @derives mpred Nveric (mapsto Ews tuint (offset_val (Zpos (xO (xO xH))) (gv _LG_foo)) (Vint (Int.repr Z0))) (mapsto Ews tint (offset_val (@nested_field_offset CompSpecs (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield))) (gv _LG_foo)) (Vint (Int.repr Z0))) *)
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) (Vint (Int.repr Z0)) (gv _LG_foo)) (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) Vundef (gv _LG_foo)) *)
simpl.
rewrite field_compatible_field_address
  by auto with field_compatible.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) (Vint (Int.repr Z0)) (gv _LG_foo)) (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) Vundef (gv _LG_foo)) *)
simpl. cancel.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) (Vint (Int.repr Z0)) (gv _LG_foo)) (@field_at CompSpecs Ews (Tstruct _foo noattr) (@cons gfield (StructField _m) (@nil gfield)) Vundef (gv _LG_foo)) *)
cancel.
Qed.

End LG.

(* The [init] function is not meant to be called from clients directly.
    Thus it can use an _internal_ abstraction, LG.data_ok,
    in its specification. *)
Definition init_spec :=
 DECLARE _LG_init
  WITH n: Z, gv: globals
  PRE  []
        PROP ()
        LOCAL(gvars gv)
        SEP(LG.data n gv)
  POST [ tvoid ]
         PROP()
         LOCAL ()
         SEP (LG.data_ok n gv).

(* The [bump] and [get] functions are meant to be called from
    client modules.  *)
Definition bump_spec :=
 DECLARE _LG_bump
  WITH n: Z, gv: globals
  PRE  []
        PROP (n < Int.max_signed)
        LOCAL(gvars gv)
        SEP(LG.data n gv)
  POST [ tvoid ]
         PROP()
         LOCAL ()
         SEP (LG.data (n+1) gv).

Definition get_spec :=
 DECLARE _LG_get
  WITH n: Z, gv: globals
  PRE  []
        PROP ()
        LOCAL(gvars gv)
        SEP(LG.data n gv)
  POST [ tint ]
         PROP()
         LOCAL (temp ret_temp (Vint (Int.repr n)))
         SEP (LG.data n gv).

Definition client_spec :=
 DECLARE _client
  WITH n: Z, gv: globals
  PRE  []
        PROP (n < 1000000000)
        LOCAL(gvars gv)
        SEP(LG.data n gv)
  POST [ tint ]
         PROP()
         LOCAL (temp ret_temp (Vint (Int.repr (n+2))))
         SEP (LG.data (n+2) gv).

Definition main_spec :=
  DECLARE _main
  WITH gv : globals
  PRE  [] main_pre prog nil gv
  POST [ tint ]  
     PROP() 
     LOCAL (temp ret_temp (Vint (Int.repr 5))) 
     SEP(TT).
  
Definition Gprog : funspecs :=
    ltac:(with_library prog [
    init_spec; bump_spec; get_spec; client_spec; main_spec]).

Lemma orp_if_bool:
 forall {A} {NA: NatDed A} (P Q: A),
   orp P Q = EX b: bool, if b then P else Q.
Proof.
(* Goal: forall (A : Type) (NA : NatDed A) (P Q : A), @eq A (@orp A NA P Q) (@exp A NA bool (fun b : bool => if b then P else Q)) *)
intros.
(* Goal: @eq A (@orp A NA P Q) (@exp A NA bool (fun b : bool => if b then P else Q)) *)
apply pred_ext.
(* Goal: @derives A NA (@orp A NA P Q) (@exp A NA bool (fun b : bool => if b then P else Q)) *)
(* Goal: @derives A NA (@exp A NA bool (fun b : bool => if b then P else Q)) (@orp A NA P Q) *)
apply orp_left.
(* Goal: @derives A NA P (@exp A NA bool (fun b : bool => if b then P else Q)) *)
(* Goal: @derives A NA Q (@exp A NA bool (fun b : bool => if b then P else Q)) *)
(* Goal: @derives A NA (@exp A NA bool (fun b : bool => if b then P else Q)) (@orp A NA P Q) *)
Exists true; auto.
(* Goal: @derives A NA Q (@exp A NA bool (fun b : bool => if b then P else Q)) *)
(* Goal: @derives A NA (@exp A NA bool (fun b : bool => if b then P else Q)) (@orp A NA P Q) *)
Exists false; auto.
(* Goal: @derives A NA (@exp A NA bool (fun b : bool => if b then P else Q)) (@orp A NA P Q) *)
Intros b.
(* Goal: @derives A NA (if b then P else Q) (@orp A NA P Q) *)
destruct b.
(* Goal: @derives A NA P (@orp A NA P Q) *)
(* Goal: @derives A NA Q (@orp A NA P Q) *)
apply orp_right1; auto.
(* Goal: @derives A NA Q (@orp A NA P Q) *)
apply orp_right2; auto.
Qed.

Lemma body_init:  semax_body Vprog Gprog f_LG_init init_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
start_function.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (LG.data n gv) *)
unfold LG.data.
(* Goal: @derives A NA (if b then P else Q) (@orp A NA P Q) *)
rewrite orp_if_bool; Intros b; destruct b.
*
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (LG.data_ok n gv) *)
unfold LG.data_ok.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@cons Prop False (@nil Prop)) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@cons mpred (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo)) (@nil mpred))))))) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)) (@stackframe_of CompSpecs f_LG_get)) *)
Intros.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint Int.zero)) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@cons mpred (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.zero) Vundef) (gv _LG_foo)) (@nil mpred)))))) (Ssequence (Sifthenelse (Eunop Onotbool (Etempvar _t'1 tint) tint) (Ssequence (Sassign (Efield (Evar _LG_foo (Tstruct _foo noattr)) _m tint) (Econst_int (Int.repr (Zpos (xI xH))) tint)) (Sassign (Efield (Evar _LG_foo (Tstruct _foo noattr)) _initialized tint) (Econst_int (Int.repr (Zpos xH)) tint))) Sskip) MORE_COMMANDS) POSTCONDITION *)
forward_if (PROP() LOCAL() SEP(LG.data_ok n gv)).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (Z.le Z0 n) (Z.le n Int.max_signed))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) *)
entailer!.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (Z.le Z0 n) (Z.le n Int.max_signed))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) *)
entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (LG.data_ok n gv) *)
unfold LG.data_ok.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (Z.le Z0 n) (Z.le n Int.max_signed))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) *)
entailer!.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
*
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@cons Prop False (@nil Prop)) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@cons mpred (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo)) (@nil mpred))))))) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)) (@stackframe_of CompSpecs f_LG_get)) *)
Intros.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint Int.zero)) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@cons mpred (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.zero) Vundef) (gv _LG_foo)) (@nil mpred)))))) (Ssequence (Sifthenelse (Eunop Onotbool (Etempvar _t'1 tint) tint) (Ssequence (Sassign (Efield (Evar _LG_foo (Tstruct _foo noattr)) _m tint) (Econst_int (Int.repr (Zpos (xI xH))) tint)) (Sassign (Efield (Evar _LG_foo (Tstruct _foo noattr)) _initialized tint) (Econst_int (Int.repr (Zpos xH)) tint))) Sskip) MORE_COMMANDS) POSTCONDITION *)
forward_if (PROP() LOCAL() SEP(LG.data_ok n gv)).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (Z.le Z0 n) (Z.le n Int.max_signed))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) *)
entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (LG.data_ok n gv) *)
unfold LG.data_ok.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (Z.le Z0 n) (Z.le n Int.max_signed))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) *)
entailer!.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (LG.data_ok n gv) *)
unfold LG.data_ok.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (Z.le Z0 n) (Z.le n Int.max_signed))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) *)
entailer!.
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.zero) Vundef) (gv _LG_foo)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr (Zpos (xI xH))))) (gv _LG_foo)) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (LG.data_ok n gv) (@nil mpred))))) (Sreturn (@None expr)) POSTCONDITION *)
inv H0.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
Qed.

Lemma body_bump:  semax_body Vprog Gprog f_LG_bump bump_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 (LG.data n gv) (@nil mpred))))) (Ssequence (Scall (@None ident) (Evar _LG_bump (Tfunction Tnil tvoid cc_default)) (@nil expr)) MORE_COMMANDS) POSTCONDITION *)
forward_call (n,gv).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (LG.data_ok n gv) *)
unfold LG.data_ok.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@cons Prop False (@nil Prop)) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@cons mpred (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo)) (@nil mpred))))))) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)) (@stackframe_of CompSpecs f_LG_get)) *)
Intros.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (LG.data n gv) *)
unfold LG.data.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@orp mpred Nveric (LG.data_ok n gv) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (@eq Z n (Zpos (xI xH)))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.zero) Vundef) (gv _LG_foo)))) *)
apply orp_right1.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (LG.data_ok n gv) *)
unfold LG.data_ok.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (Z.le Z0 n) (Z.le n Int.max_signed))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) *)
entailer!.
Qed.

Lemma body_get:  semax_body Vprog Gprog f_LG_get get_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 (LG.data n gv) (@nil mpred))))) (Ssequence (Scall (@None ident) (Evar _LG_bump (Tfunction Tnil tvoid cc_default)) (@nil expr)) MORE_COMMANDS) POSTCONDITION *)
forward_call (n,gv).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (LG.data_ok n gv) *)
unfold LG.data_ok.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@cons Prop False (@nil Prop)) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@cons mpred (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo)) (@nil mpred))))))) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)) (@stackframe_of CompSpecs f_LG_get)) *)
Intros.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@cons mpred (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo)) (@nil mpred)))))) (Sifthenelse (Ebinop Oand (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint) (Sreturn (@Some expr (Etempvar _i tint))) (Ssequence (Sset _t'1 (Efield (Evar _LG_foo (Tstruct _foo noattr)) _m tint)) (Sreturn (@Some expr (Etempvar _t'1 tint))))) POSTCONDITION *)
forward_if False.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (LG.data n gv) *)
unfold LG.data.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@orp mpred Nveric (LG.data_ok n gv) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (@eq Z n (Zpos (xI xH)))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.zero) Vundef) (gv _LG_foo)))) *)
apply orp_right1.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (LG.data_ok n gv) *)
unfold LG.data_ok.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (Z.le Z0 n) (Z.le n Int.max_signed))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) *)
entailer!.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (LG.data n gv) *)
unfold LG.data.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@orp mpred Nveric (LG.data_ok n gv) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (@eq Z n (Zpos (xI xH)))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.zero) Vundef) (gv _LG_foo)))) *)
apply orp_right1.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (LG.data_ok n gv) *)
unfold LG.data_ok.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (Z.le Z0 n) (Z.le n Int.max_signed))) (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n))) (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo))) *)
entailer!.
*
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@cons Prop False (@nil Prop)) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews tint (Vint (Int.repr n)) (gv _LG_n)) (@cons mpred (@data_at CompSpecs Ews (Tstruct _foo noattr) (@pair val val (Vint Int.one) (Vint (Int.repr n))) (gv _LG_foo)) (@nil mpred))))))) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)) (@stackframe_of CompSpecs f_LG_get)) *)
Intros. contradiction.
Qed.


Lemma body_client: semax_body Vprog Gprog f_client client_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 (LG.data n gv) (@nil mpred))))) (Ssequence (Scall (@None ident) (Evar _LG_bump (Tfunction Tnil tvoid cc_default)) (@nil expr)) MORE_COMMANDS) POSTCONDITION *)
forward_call (n,gv).
(* Goal: Z.lt (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xI (xO (xI (xO (xO (xI (xI (xO (xI (xO (xI (xI (xO (xO (xI (xI (xI (xO (xI (xI xH)))))))))))))))))))))))))))))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
rep_omega.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (LG.data (Z.add n (Zpos xH)) gv) (@nil mpred))))) (Ssequence (Scall (@None ident) (Evar _LG_bump (Tfunction Tnil tvoid cc_default)) (@nil expr)) MORE_COMMANDS) POSTCONDITION *)
forward_call (n+1,gv).
(* Goal: Z.lt (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xI (xO (xI (xO (xO (xI (xI (xO (xI (xO (xI (xI (xO (xO (xI (xI (xI (xO (xI (xI xH)))))))))))))))))))))))))))))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
rep_omega.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (LG.data (Z.add (Z.add n (Zpos xH)) (Zpos xH)) gv) (@nil mpred))))) (Ssequence (Scall (@Some ident _t'1) (Evar _LG_get (Tfunction Tnil tint cc_default)) (@nil expr)) MORE_COMMANDS) POSTCONDITION *)
replace (n+1+1) with (n+2) by omega.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (LG.data (Z.add n (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Scall (@Some ident _t'1) (Evar _LG_get (Tfunction Tnil tint cc_default)) (@nil expr)) MORE_COMMANDS) POSTCONDITION *)
forward_call (n+2,gv).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
Qed.

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 tuint (offset_val (Zpos (xO (xO xH))) (gv _LG_foo)) (Vint (Int.repr Z0))) (@cons mpred (@data_at CompSpecs Ews tuint (Vint (Int.repr Z0)) (gv _LG_foo)) (@cons mpred (@data_at CompSpecs Ews tuint (Vint (Int.repr (Zpos (xI xH)))) (gv _LG_n)) (@nil mpred))))))) (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _client (Tfunction Tnil tint cc_default)) (@nil expr)) (Sreturn (@Some expr (Etempvar _t'1 tint)))) MORE_COMMANDS) POSTCONDITION *)
sep_apply (LG.initial gv); auto.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (LG.data (Zpos (xI xH)) gv) (@nil mpred))))) (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _client (Tfunction Tnil tint cc_default)) (@nil expr)) (Sreturn (@Some expr (Etempvar _t'1 tint)))) MORE_COMMANDS) POSTCONDITION *)
forward_call (3,gv).
(* Goal: Z.lt (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xI (xO (xI (xO (xO (xI (xI (xO (xI (xO (xI (xI (xO (xO (xI (xI (xI (xO (xI (xI xH)))))))))))))))))))))))))))))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
rep_omega.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (LG.data (Z.add (Zpos (xI xH)) (Zpos (xO xH))) gv) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _t'1 tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
Qed.

