Require Import VST.floyd.proofauto.
Require Import VST.progs.sumarray.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs.  mk_varspecs prog. Defined.
Definition Gprog: funspecs := nil.
Definition Delta1 : tycontext :=
  ltac:(let x := constr:(func_tycontext f_sumarray Vprog Gprog nil)
         in let y := eval hnf in x
         in exact y).

(* This example is from the "EX, Intros, Exists" chapter of the Verifiable C Reference Manual *)
Lemma exercise1:
 let Delta := @abbreviate _ Delta1 in 
 forall sh p,
 ENTAIL Delta,
   EX x:Z,
    PROP(0<=x) LOCAL(temp _i (Vint (Int.repr x)))
    SEP (EX y:Z, !!(x<y) && data_at sh tint (Vint (Int.repr y)) p)
|-- EX u: Z,
     PROP(0<u) LOCAL()
     SEP (data_at sh tint (Vint (Int.repr u)) p).
Proof.
(* Goal: let Delta := @abbreviate tycontext Delta1 in forall (sh : Share.t) (p : val), @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun x : Z => PROPx (@cons Prop (Z.le Z0 x) (@nil Prop)) (LOCALx (@cons localdef (temp _i (Vint (Int.repr x))) (@nil localdef)) (SEPx (@cons mpred (@exp mpred Nveric Z (fun y : Z => @andp mpred Nveric (@prop mpred Nveric (Z.lt x y)) (@data_at CompSpecs sh tint (Vint (Int.repr y)) p))) (@nil mpred))))))) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun u : Z => PROPx (@cons Prop (Z.lt Z0 u) (@nil Prop)) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at CompSpecs sh tint (Vint (Int.repr u)) p) (@nil mpred)))))) *)
Intros a b.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr a))) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs sh tint (Vint (Int.repr b)) p) (@nil mpred)))))) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun u : Z => PROPx (@cons Prop (Z.lt Z0 u) (@nil Prop)) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at CompSpecs sh tint (Vint (Int.repr u)) p) (@nil mpred)))))) *)
Exists b.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
entailer!.
Qed.

(* These examples of [rep_omega] are from is from the "Integers: nat, Z, int" chapter of the Verifiable C Reference Manual *)
Lemma exercise2:
  forall x,
  Int.min_signed <= x <= Int.max_signed ->
  Int.signed (Int.repr x) = x.
Proof.
(* Goal: forall (x : Z) (_ : and (Z.le Int.min_signed x) (Z.le x Int.max_signed)), @eq Z (Int.signed (Int.repr x)) x *)
intros x H.
(* Notice that the premise H is needed for the next line *)
(* Goal: @eq Z (Int.signed (Int.repr x)) x *)
rewrite Int.signed_repr by rep_omega.
(* Goal: @eq Z x x *)
auto.
Qed.

Lemma exercise3: 
  forall n, 0 <= n <= Int.max_signed ->
  Int.min_signed <= 0 <= n.
Proof.
(* Goal: let Delta := @abbreviate tycontext Delta1 in forall (sh : Share.t) (p : val), @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
intros.
(* Goal: Z.le Z0 (Z.sub N (Zpos (xO xH))) *)
rep_omega.
Qed.

Lemma exercise3b: 
  forall al: list Z ,  Zlength al < 50 ->
         0 <= Zlength al < Int.max_signed.
Proof.
(* Goal: let Delta := @abbreviate tycontext Delta1 in forall (sh : Share.t) (p : val), @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
intros.
(* Goal: Z.le Z0 (Z.sub N (Zpos (xO xH))) *)
rep_omega.
Qed.

Lemma exercise3c: 
  forall i,
         0 <= Int.unsigned (Int.repr i) <= Int.max_unsigned.
Proof.
(* Goal: let Delta := @abbreviate tycontext Delta1 in forall (sh : Share.t) (p : val), @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
intros.
(* Goal: Z.le Z0 (Z.sub N (Zpos (xO xH))) *)
rep_omega.
Qed.


(* Goal: Z.le Z0 (Z.sub N (Zpos (xO xH))) *)
(**  How to manage semi-opaque constants, using Hint Rewrite : rep_omega. *)
(* Suppose you have an uninitialized array of size N: *)

Definition N : Z := 20.

Lemma exercise4:
 let Delta := @abbreviate _ Delta1 in 
 forall sh p,
    data_at sh (tarray tint N) (Vint (Int.repr 1) :: Vint (Int.repr 2) :: list_repeat (Z.to_nat (N-2)) Vundef) p
 |--  !! (0 <= Zlength (list_repeat (Z.to_nat (N-2)) Vundef) < Int.max_signed).
Proof.
(* Goal: let Delta := @abbreviate tycontext Delta1 in forall (sh : Share.t) (p : val), @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
intros.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
simpl.
(* It's not nice that [simpl] unfolded the list_repeat. *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
entailer!.
repeat rewrite Zlength_cons. rewrite Zlength_nil. 
(* Goal: Z.le Z0 (Z.sub N (Zpos (xO xH))) *)
rep_omega.
Abort.

(* To avoid unfolding of the list_repeat, let us make N opaque. *)

Global Opaque N.

Lemma exercise4b:
 let Delta := @abbreviate _ Delta1 in 
 forall sh p,
    data_at sh (tarray tint N) (Vint (Int.repr 1) :: Vint (Int.repr 2) :: list_repeat (Z.to_nat (N-2)) Vundef) p
 |--  !! (0 <= Zlength (list_repeat (Z.to_nat (N-2)) Vundef) < Int.max_signed).
Proof.
(* Goal: let Delta := @abbreviate tycontext Delta1 in forall (sh : Share.t) (p : val), @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
intros.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
simpl.
(* That's better; the data_at is more concise.  But now, unfortunately: *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
entailer!.
(* Goal: and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed) *)
rewrite Zlength_list_repeat.
(* Goal: Z.le Z0 (Z.sub N (Zpos (xO xH))) *)
Fail rep_omega.
(* now rep_omega does not know that N=20. *)
Abort.

(* To tell rep_omega that N=20, just add a hint to the rep_omega database: *)

Lemma N_eq: N=20.
Proof. reflexivity. Qed.
(* Goal: Z.le Z0 (Z.sub N (Zpos (xO xH))) *)
Hint Rewrite N_eq : rep_omega.

Lemma exercise4c:
 let Delta := @abbreviate _ Delta1 in 
 forall sh p,
    data_at sh (tarray tint N) (Vint (Int.repr 1) :: Vint (Int.repr 2) :: list_repeat (Z.to_nat (N-2)) Vundef) p
 |--  !! (0 <= Zlength (list_repeat (Z.to_nat (N-2)) Vundef) < Int.max_signed).
Proof.
(* Goal: let Delta := @abbreviate tycontext Delta1 in forall (sh : Share.t) (p : val), @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
intros.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
simpl.
(* That's still good; the data_at is more concise.  *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tint N) (@cons val (Vint (Int.repr (Zpos xH))) (@cons val (Vint (Int.repr (Zpos (xO xH)))) (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) p) (@prop mpred Nveric (and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed))) *)
entailer!.
(* Goal: and (Z.le Z0 (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef))) (Z.lt (@Zlength val (@list_repeat val (Z.to_nat (Z.sub N (Zpos (xO xH)))) Vundef)) Int.max_signed) *)
rewrite Zlength_list_repeat.
(* Goal: Z.le Z0 (Z.sub N (Zpos (xO xH))) *)
rep_omega.
(* Goal: Z.le Z0 (Z.sub N (Zpos (xO xH))) *)
rep_omega.
Qed.

(* Summary: Make your constant Global Opaque, but add a Hint Rewrite rule to the rep_omega database. *)








