(* This file illustrates two approaches to C verification,
  described in Section III of this paper:

 Modular Verification for Computer Security,
 by Andrew W. Appel, in IEEE Computer Security Foundations conference (CSF'16),
 June 2016.
 http://www.cs.princeton.edu/~appel/papers/modsec.pdf
*)

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

Require Import ZArith.
Require Import List.
Import ListNotations.
Open Scope Z.


Theorem fold_min_general:
  forall (al: list Z)(i: Z),
  In i (al) ->
  forall x, List.fold_right Z.min x al <= i.
Proof.
(* Goal: forall (al : list Z) (i : Z) (_ : @In Z i al) (x : Z), Z.le (@fold_right Z Z Z.min x al) i *)
induction al; intros.
(* Goal: Z.le (@fold_right Z Z Z.min x (@nil Z)) i *)
(* Goal: Z.le (@fold_right Z Z Z.min x (@cons Z a al)) i *)
inversion H.
(* Goal: Z.le (@fold_right Z Z Z.min x (@cons Z a al)) i *)
destruct H.
(* Goal: Z.le (@fold_right Z Z Z.min x (@cons Z a al)) i *)
(* Goal: Z.le (@fold_right Z Z Z.min x (@cons Z a al)) i *)
subst a.
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
simpl.
(* Goal: Z.le (Z.min i (@fold_right Z Z Z.min x al)) i *)
(* Goal: Z.le (@fold_right Z Z Z.min x (@cons Z a al)) i *)
apply Z.le_min_l.
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
simpl. rewrite Z.le_min_r.
(* Goal: @eq Z (@fold_right Z Z Z.min x (@app Z al (@cons Z y (@nil Z)))) (Z.min (@fold_right Z Z Z.min x al) y) *)
apply IHal.
(* Goal: @In Z i al *)
apply H.
Qed.

Theorem fold_min:
  forall (al: list Z)(i: Z),
  In i (al) ->
  List.fold_right Z.min (hd 0 al) al <= i.
Proof.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (Inv (Zpos xH) (Z.gt n) i)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a : Z => Inv (Zpos xH) (Z.gt n) a)) *)
intros.
(* Goal: Z.le (@fold_right Z Z Z.min (@hd Z Z0 al) al) i *)
apply fold_min_general.
(* Goal: @In Z i al *)
apply H.
Qed.

Lemma Forall_fold_min:
  forall (f: Z -> Prop) (x: Z) (al: list Z),
    f x -> Forall f al -> f (fold_right Z.min x al).
Proof.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (Inv (Zpos xH) (Z.gt n) i)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a : Z => Inv (Zpos xH) (Z.gt n) a)) *)
 intros.
(* Goal: f (@fold_right Z Z Z.min x al) *)
 induction H0.
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
 simpl. auto.
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
 simpl.
(* Goal: f (Z.min x0 (@fold_right Z Z Z.min x l)) *)
 unfold Z.min at 1.
(* Goal: f x *)
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
 destruct (Z.compare x0 (fold_right Z.min x l)) eqn:?; auto.
Qed.

Lemma fold_min_another:
  forall x al y,
    fold_right Z.min x (al ++ [y]) = Z.min (fold_right Z.min x al) y.
Proof.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (Inv (Zpos xH) (Z.gt n) i)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a : Z => Inv (Zpos xH) (Z.gt n) a)) *)
 intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (Inv (Zpos xH) (Z.gt n) i)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a : Z => Inv (Zpos xH) (Z.gt n) a)) *)
 revert x; induction al; simpl; intros.
(* Goal: @eq Z (Z.min y x) (Z.min x y) *)
(* Goal: @eq Z (Z.min a (@fold_right Z Z Z.min x (@app Z al (@cons Z y (@nil Z))))) (Z.min (Z.min a (@fold_right Z Z Z.min x al)) y) *)
 apply Z.min_comm.
(* Goal: @eq Z (Z.min a (@fold_right Z Z Z.min x (@app Z al (@cons Z y (@nil Z))))) (Z.min (Z.min a (@fold_right Z Z Z.min x al)) y) *)
 rewrite <- Z.min_assoc. f_equal.
(* Goal: @eq Z (@fold_right Z Z Z.min x (@app Z al (@cons Z y (@nil Z)))) (Z.min (@fold_right Z Z Z.min x al) y) *)
 apply IHal.
Qed.

Lemma is_int_I32_Znth_map_Vint:
 forall i s al,
  0 <= i < Zlength al ->
  is_int I32 s (Znth i (map Vint al)).
Proof.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (Inv (Zpos xH) (Z.gt n) i)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a : Z => Inv (Zpos xH) (Z.gt n) a)) *)
intros. rewrite Znth_map; auto.
Qed.
Hint Extern 3 (is_int I32 _ (Znth _ (map Vint _))) =>
  (apply  is_int_I32_Znth_map_Vint; rewrite ?Zlength_map; omega).

Definition minimum_spec :=
 DECLARE _minimum
  WITH a: val, n: Z, al: list Z
  PRE [ _a OF tptr tint , _n OF tint ]
    PROP  (1 <= n <= Int.max_signed; Forall repable_signed al)
    LOCAL (temp _a a; temp _n (Vint (Int.repr n)))
    SEP   (data_at Ews (tarray tint n) (map Vint (map Int.repr al)) a)
  POST [ tint ]
    PROP ()
    LOCAL(temp ret_temp  (Vint (Int.repr (fold_right Z.min (hd 0 al) al))))
    SEP   (data_at Ews (tarray tint n) (map Vint (map Int.repr al)) a).

Definition Gprog : funspecs :=
      ltac:(with_library prog [minimum_spec]).

(* First approach from "Modular Verification for Computer Security",
  proved using forward_for_simple_bound *)
Lemma body_min: semax_body Vprog Gprog f_minimum minimum_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_minimum minimum_spec2 *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Ssequence (Sset _min (Ederef (Ebinop Oadd (Etempvar _a (tptr tint)) (Econst_int (Int.repr Z0) tint) (tptr tint)) tint)) MORE_COMMANDS) POSTCONDITION *)
assert_PROP (Zlength al = n). {
(* Goal: f x *)
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
  entailer!. autorewrite with sublist; auto.
}
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
forward.  (* min = a[0]; *)
forward_for_simple_bound n
  (EX i:Z,
    PROP()
    LOCAL(temp _min (Vint (Int.repr (fold_right Z.min (Znth 0 al) (sublist 0 i al))));
          temp _a a;
          temp _n (Vint (Int.repr n)))
    SEP(data_at Ews (tarray tint n) (map Vint (map Int.repr al)) a)).
* (* Prove that the precondition implies the loop invariant *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@andp mpred Nveric (@prop mpred Nveric (and (@In Z x al) (and (@Forall Z (fun x0 : Z => Z.le x x0) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr x)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a)) *)
  entailer!.
* (* Prove that the loop body preserves the loop invariant *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
 forward. (* j = a[i]; *)
 assert (repable_signed (Znth i al))
     by (apply Forall_Znth; auto; omega).
 assert (repable_signed (fold_right Z.min (Znth 0 al) (sublist 0 i al)))
   by (apply Forall_fold_min;
          [apply Forall_Znth; auto; omega
          |apply Forall_sublist; auto]).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip) POSTCONDITION *)
 autorewrite with sublist.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (Inv (Zpos xH) (Z.gt n) i)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a : Z => Inv (Zpos xH) (Z.gt n) a)) *)
 subst POSTCONDITION; unfold abbreviate.
(* Goal: @Forall Z (Z.le j) (@sublist Z Z0 (Z.add i (Zpos xH)) al) *)
 rewrite (sublist_split 0 i (i+1)) by omega.
(* Goal: and (@In Z (@Znth Z Inhabitant_Z i al) (@app Z (@sublist Z Z0 i al) (@sublist Z i (Z.add i (Zpos xH)) al))) (@Forall Z (Z.le (@Znth Z Inhabitant_Z i al)) (@app Z (@sublist Z Z0 i al) (@sublist Z i (Z.add i (Zpos xH)) al))) *)
 rewrite (sublist_one i (i+1) al) by omega.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _min (Vint (Int.repr (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@sublist Z Z0 i al))))) (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip) (normal_ret_assert (PROPx (@cons Prop (and (Z.le Z0 i) (Z.le i n)) (@cons Prop (Z.gt n i) (@nil Prop))) (LOCALx (@cons localdef (temp _min (Vint (Int.repr (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@app Z (@sublist Z Z0 i al) (@cons Z (@Znth Z Inhabitant_Z i al) (@nil Z))))))) (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred)))))) *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (Inv (Zpos xH) (Z.gt n) i)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a : Z => Inv (Zpos xH) (Z.gt n) a)) *)
 rewrite fold_min_another.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip) POSTCONDITION *)
 forward_if.
 +
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
 forward. (* min = j; *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@andp mpred Nveric (@prop mpred Nveric (and (@In Z x al) (and (@Forall Z (fun x0 : Z => Z.le x x0) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr x)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a)) *)
 entailer!.
(* Goal: @eq val (Vint (Int.repr (Z.min (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@sublist Z Z0 i al)) (@Znth Z Inhabitant_Z i al)))) (Vint (Int.repr (@Znth Z Inhabitant_Z i al))) *)
 rewrite Z.min_r; auto; omega.
 +
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
 forward. (* skip; *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@andp mpred Nveric (@prop mpred Nveric (and (@In Z x al) (and (@Forall Z (fun x0 : Z => Z.le x x0) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr x)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a)) *)
 entailer!.
(* Goal: @eq val (Vint (Int.repr (Z.min (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@sublist Z Z0 i al)) (@Znth Z Inhabitant_Z i al)))) (Vint (Int.repr (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@sublist Z Z0 i al)))) *)
 rewrite Z.min_l; auto; omega.
* (* After the loop *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
 forward. (* return *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@andp mpred Nveric (@prop mpred Nveric (and (@In Z x al) (and (@Forall Z (fun x0 : Z => Z.le x x0) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr x)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a)) *)
 entailer!.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip) POSTCONDITION *)
 autorewrite with sublist.
(* Goal: f x *)
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
 destruct al; simpl; auto.
Qed.

(* Demonstration of the same theorem, but using
    forward_for  instead of forward_for_simple_bound *)
Lemma body_min': semax_body Vprog Gprog f_minimum minimum_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_minimum minimum_spec2 *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Ssequence (Sset _min (Ederef (Ebinop Oadd (Etempvar _a (tptr tint)) (Econst_int (Int.repr Z0) tint) (tptr tint)) tint)) MORE_COMMANDS) POSTCONDITION *)
assert_PROP (Zlength al = n). {
(* Goal: f x *)
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
  entailer!. autorewrite with sublist; auto.
}
revert POSTCONDITION;
 replace (hd 0 al) with (Znth 0 al) by (destruct al; reflexivity);
 intro POSTCONDITION.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
forward.  (* min = a[0]; *)
pose (Inv d (f: Z->Prop) (i: Z) :=
    PROP(0 <= i <= n; f i)
    LOCAL(temp _min (Vint (Int.repr (fold_right Z.min (Znth 0 al) (sublist 0 (i+d) al))));
          temp _a a; temp _i (Vint (Int.repr i));
          temp _n (Vint (Int.repr n)))
    SEP(data_at Ews (tarray tint n) (map Vint (map Int.repr al)) a)).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _min (Vint (Int.repr (@Znth Z Inhabitant_Z Z0 al)))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Etempvar _n tint) tint) (Ssequence (Sset _j (Ederef (Ebinop Oadd (Etempvar _a (tptr tint)) (Etempvar _i tint) (tptr tint)) tint)) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip)) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
forward_for (Inv 0 (fun _ => True)) continue: (Inv 1 (Z.gt n)).
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
forward.
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@andp mpred Nveric (@prop mpred Nveric (and (@In Z x al) (and (@Forall Z (fun x0 : Z => Z.le x x0) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr x)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a)) *)
Exists 0. unfold Inv; entailer!.
*
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@andp mpred Nveric (@prop mpred Nveric (and (@In Z x al) (and (@Forall Z (fun x0 : Z => Z.le x x0) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr x)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a)) *)
entailer!.
*
match goal with
| P := @abbreviate ret_assert _ |- _ => unfold abbreviate in P; subst P
end.
match goal with
| |- semax _ _ ?c ?P =>
    tryif (is_sequential false false c)
    then (apply sequential; simpl_ret_assert;
          match goal with |- semax _ _ _ ?Q =>
             abbreviate Q : ret_assert as POSTCONDITION
          end)
    else abbreviate P : ret_assert as POSTCONDITION
end.

(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _min (Vint (Int.repr (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@sublist Z Z0 (Z.add a0 Z0) al))))) (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr a0))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Ssequence (Sset _j (Ederef (Ebinop Oadd (Etempvar _a (tptr tint)) (Etempvar _i tint) (tptr tint)) tint)) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip)) POSTCONDITION *)
force_sequential.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _min (Vint (Int.repr (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@sublist Z Z0 (Z.add a0 Z0) al))))) (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr a0))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Ssequence (Sset _j (Ederef (Ebinop Oadd (Etempvar _a (tptr tint)) (Etempvar _i tint) (tptr tint)) tint)) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip)) POSTCONDITION *)
abbreviate_semax.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _min (Vint (Int.repr (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@sublist Z Z0 (Z.add a0 (Zpos xH)) al))))) (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr a0))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint)) (normal_ret_assert (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a0 : Z => PROPx (@cons Prop (and (Z.le Z0 a0) (Z.le a0 n)) (@cons Prop True (@nil Prop))) (LOCALx (@cons localdef (temp _min (Vint (Int.repr (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@sublist Z Z0 (Z.add a0 Z0) al))))) (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr a0))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))))) *)
rename a0 into i.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
 forward. (* j = a[i]; *)
 assert (repable_signed (Znth i al))
     by (apply Forall_Znth; auto; omega).
 assert (repable_signed (fold_right Z.min (Znth 0 al) (sublist 0 i al)))
   by (apply Forall_fold_min;
          [apply Forall_Znth; auto; omega
          |apply Forall_sublist; auto]).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip) POSTCONDITION *)
 autorewrite with sublist.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _min (Vint (Int.repr (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@sublist Z Z0 i al))))) (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip) POSTCONDITION *)
 apply semax_post_flipped' with (Inv 1 (Z.gt n) i).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _min (Vint (Int.repr (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@sublist Z Z0 i al))))) (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip) (normal_ret_assert (Inv (Zpos xH) (Z.gt n) i)) *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (Inv (Zpos xH) (Z.gt n) i)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a : Z => Inv (Zpos xH) (Z.gt n) a)) *)
 unfold Inv.
(* Goal: @Forall Z (Z.le j) (@sublist Z Z0 (Z.add i (Zpos xH)) al) *)
 rewrite (sublist_split 0 i (i+1)) by omega.
(* Goal: and (@In Z (@Znth Z Inhabitant_Z i al) (@app Z (@sublist Z Z0 i al) (@sublist Z i (Z.add i (Zpos xH)) al))) (@Forall Z (Z.le (@Znth Z Inhabitant_Z i al)) (@app Z (@sublist Z Z0 i al) (@sublist Z i (Z.add i (Zpos xH)) al))) *)
 rewrite (sublist_one i (i+1) al) by omega.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _min (Vint (Int.repr (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@sublist Z Z0 i al))))) (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip) (normal_ret_assert (PROPx (@cons Prop (and (Z.le Z0 i) (Z.le i n)) (@cons Prop (Z.gt n i) (@nil Prop))) (LOCALx (@cons localdef (temp _min (Vint (Int.repr (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@app Z (@sublist Z Z0 i al) (@cons Z (@Znth Z Inhabitant_Z i al) (@nil Z))))))) (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred)))))) *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (Inv (Zpos xH) (Z.gt n) i)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a : Z => Inv (Zpos xH) (Z.gt n) a)) *)
 rewrite fold_min_another.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip) POSTCONDITION *)
 forward_if.
 +
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
 forward. (* min = j; *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@andp mpred Nveric (@prop mpred Nveric (and (@In Z x al) (and (@Forall Z (fun x0 : Z => Z.le x x0) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr x)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a)) *)
 entailer!. rewrite Z.min_r; auto; omega.
 +
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
 forward. (* skip; *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@andp mpred Nveric (@prop mpred Nveric (and (@In Z x al) (and (@Forall Z (fun x0 : Z => Z.le x x0) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr x)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a)) *)
 entailer!. rewrite Z.min_l; auto; omega.
 +
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (Inv (Zpos xH) (Z.gt n) i)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a : Z => Inv (Zpos xH) (Z.gt n) a)) *)
 intros.
 subst POSTCONDITION; unfold abbreviate. (* TODO: some of these lines should all be done by forward_if *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (Inv (Zpos xH) (Z.gt n) i)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a : Z => Inv (Zpos xH) (Z.gt n) a)) *)
 simpl_ret_assert.
 (* TODO: entailer! fails here with a misleading error message *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (Inv (Zpos xH) (Z.gt n) i)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a : Z => Inv (Zpos xH) (Z.gt n) a)) *)
 Exists i. apply andp_left2. normalize.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _min (Vint (Int.repr (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@sublist Z Z0 (Z.add a0 (Zpos xH)) al))))) (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr a0))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint)) (normal_ret_assert (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a0 : Z => PROPx (@cons Prop (and (Z.le Z0 a0) (Z.le a0 n)) (@cons Prop True (@nil Prop))) (LOCALx (@cons localdef (temp _min (Vint (Int.repr (@fold_right Z Z Z.min (@Znth Z Inhabitant_Z Z0 al) (@sublist Z Z0 (Z.add a0 Z0) al))))) (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr a0))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))))) *)
 rename a0 into i.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
 forward.
 Exists (i+1).
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@andp mpred Nveric (@prop mpred Nveric (and (@In Z x al) (and (@Forall Z (fun x0 : Z => Z.le x x0) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr x)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a)) *)
 entailer!.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip) POSTCONDITION *)
 autorewrite with sublist.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
 forward.
Qed.

Definition minimum_spec2 :=
 DECLARE _minimum
  WITH a: val, n: Z, al: list Z
  PRE [ _a OF tptr tint , _n OF tint ]
    PROP  (1 <= n <= Int.max_signed; Forall repable_signed al)
    LOCAL (temp _a a; temp _n (Vint (Int.repr n)))
    SEP   (data_at Ews (tarray tint n) (map Vint (map Int.repr al)) a)
  POST [ tint ]
   EX j: Z,
    PROP (In j al; Forall (fun x => j<=x) al)
    LOCAL(temp ret_temp  (Vint (Int.repr j)))
    SEP   (data_at Ews (tarray tint n) (map Vint (map Int.repr al)) a).


(* Second approach from "Modular Verification for Computer Security",
  proved using forward_for_simple_bound *)
Lemma body_min2: semax_body Vprog Gprog f_minimum minimum_spec2.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_minimum minimum_spec2 *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Ssequence (Sset _min (Ederef (Ebinop Oadd (Etempvar _a (tptr tint)) (Econst_int (Int.repr Z0) tint) (tptr tint)) tint)) MORE_COMMANDS) POSTCONDITION *)
assert_PROP (Zlength al = n). {
(* Goal: f x *)
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
  entailer!. autorewrite with sublist; auto.
}
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
forward.  (* min = a[0]; *)
forward_for_simple_bound n
  (EX i:Z, EX j:Z,
    PROP(
         In j (sublist 0 (Z.max 1 i) al);
         Forall (Z.le j) (sublist 0 i al))
    LOCAL(
          temp _min (Vint (Int.repr j));
          temp _a a;
          temp _n (Vint (Int.repr n)))
    SEP(data_at Ews (tarray tint n) (map Vint (map Int.repr al)) a)).
* (* Show that the precondition entails the loop invariant *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _min (Vint (Int.repr (@Znth Z Inhabitant_Z Z0 al)))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred)))))) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun j : Z => PROPx (@cons Prop (@In Z j (@sublist Z Z0 (Z.max (Zpos xH) Z0) al)) (@cons Prop (@Forall Z (Z.le j) (@sublist Z Z0 Z0 al)) (@nil Prop))) (LOCALx (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred)))))) *)
Exists (Znth 0 al).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip) POSTCONDITION *)
autorewrite with sublist.
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@andp mpred Nveric (@prop mpred Nveric (and (@In Z x al) (and (@Forall Z (fun x0 : Z => Z.le x x0) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr x)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a)) *)
entailer!.
(* Goal: @Forall Z (Z.le j) (@sublist Z i (Z.add i (Zpos xH)) al) *)
rewrite sublist_one by omega.
(* Goal: f x *)
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
constructor; auto.
* (* Show that the loop body preserves the loop invariant *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@cons Prop (@In Z j (@sublist Z Z0 (Z.max (Zpos xH) i) al)) (@cons Prop (@Forall Z (Z.le j) (@sublist Z Z0 i al)) (@nil Prop))) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Ssequence (Sset _j (Ederef (Ebinop Oadd (Etempvar _a (tptr tint)) (Etempvar _i tint) (tptr tint)) tint)) MORE_COMMANDS) POSTCONDITION *)
Intros.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
forward. (* j = a[i]; *)
assert (repable_signed (Znth i al))
   by (apply Forall_Znth; auto; omega).
assert (repable_signed j)
   by (eapply Forall_forall; [ | eassumption]; apply Forall_sublist; auto).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip) POSTCONDITION *)
autorewrite with sublist.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Etempvar _min tint) tint) (Sset _min (Etempvar _j tint)) Sskip) POSTCONDITION *)
forward_if.
 + (* Then clause *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
 forward. (* min = j; *)
(* 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 _min (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred)))))) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun j : Z => PROPx (@cons Prop (@In Z j (@sublist Z Z0 (Z.max (Zpos xH) (Z.add i (Zpos xH))) al)) (@cons Prop (@Forall Z (Z.le j) (@sublist Z Z0 (Z.add i (Zpos xH)) al)) (@nil Prop))) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred)))))) *)
 Exists (Znth i al).
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@andp mpred Nveric (@prop mpred Nveric (and (@In Z x al) (and (@Forall Z (fun x0 : Z => Z.le x x0) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr x)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a)) *)
 entailer!.
(* Goal: and (@In Z j (@sublist Z Z0 (Z.max (Zpos xH) (Z.add i (Zpos xH))) al)) (@Forall Z (Z.le j) (@sublist Z Z0 (Z.add i (Zpos xH)) al)) *)
 rewrite Z.max_r by omega.
(* Goal: @Forall Z (Z.le j) (@sublist Z Z0 (Z.add i (Zpos xH)) al) *)
 rewrite (sublist_split 0 i (i+1)) by omega.
(* Goal: and (@In Z (@Znth Z Inhabitant_Z i al) (@app Z (@sublist Z Z0 i al) (@sublist Z i (Z.add i (Zpos xH)) al))) (@Forall Z (Z.le (@Znth Z Inhabitant_Z i al)) (@app Z (@sublist Z Z0 i al) (@sublist Z i (Z.add i (Zpos xH)) al))) *)
 rewrite (sublist_one i (i+1) al) by omega.
(* Goal: and (@In Z j (@sublist Z Z0 (Z.add i (Zpos xH)) al)) (@Forall Z (Z.le j) (@sublist Z Z0 (Z.add i (Zpos xH)) al)) *)
 split.
(* Goal: f x *)
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
 apply in_app; right; constructor; auto.
(* Goal: and (@In Z j (@sublist Z Z0 (Z.add i (Zpos xH)) al)) (@Forall Z (Z.le j) (@sublist Z Z0 (Z.add i (Zpos xH)) al)) *)
 apply Forall_app; split.
(* Goal: @Forall Z (Z.le (@Znth Z Inhabitant_Z i al)) (@sublist Z Z0 i al) *)
(* Goal: @Forall Z (Z.le (@Znth Z Inhabitant_Z i al)) (@cons Z (@Znth Z Inhabitant_Z i al) (@nil Z)) *)
 eapply Forall_impl; try apply H4.
(* Goal: forall (a : Z) (_ : Z.le j a), Z.le (@Znth Z Inhabitant_Z i al) a *)
(* Goal: @Forall Z (Z.le (@Znth Z Inhabitant_Z i al)) (@cons Z (@Znth Z Inhabitant_Z i al) (@nil Z)) *)
 intros; omega.
(* Goal: f x *)
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
 constructor; auto. omega.
 + (* Else clause *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) 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 (temp _j (Vint (Int.repr (@Znth Z Inhabitant_Z i al)))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred)))))) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun j : Z => PROPx (@cons Prop (@In Z j (@sublist Z Z0 (Z.max (Zpos xH) (Z.add i (Zpos xH))) al)) (@cons Prop (@Forall Z (Z.le j) (@sublist Z Z0 (Z.add i (Zpos xH)) al)) (@nil Prop))) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred)))))) *)
 Exists j.
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@andp mpred Nveric (@prop mpred Nveric (and (@In Z x al) (and (@Forall Z (fun x0 : Z => Z.le x x0) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr x)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a)) *)
 entailer!.
(* Goal: and (@In Z j (@sublist Z Z0 (Z.max (Zpos xH) (Z.add i (Zpos xH))) al)) (@Forall Z (Z.le j) (@sublist Z Z0 (Z.add i (Zpos xH)) al)) *)
 rewrite Z.max_r by omega.
(* Goal: and (@In Z j (@sublist Z Z0 (Z.add i (Zpos xH)) al)) (@Forall Z (Z.le j) (@sublist Z Z0 (Z.add i (Zpos xH)) al)) *)
 split.
(* Goal: @In Z j (@sublist Z Z0 (Z.add i (Zpos xH)) al) *)
(* Goal: @Forall Z (Z.le j) (@sublist Z Z0 (Z.add i (Zpos xH)) al) *)
 destruct (zlt 1 i).
(* Goal: Z.le j (@Znth Z Inhabitant_Z i al) *)
 rewrite Z.max_r in H3 by omega.
(* Goal: @Forall Z (Z.le j) (@sublist Z Z0 (Z.add i (Zpos xH)) al) *)
 rewrite (sublist_split 0 i (i+1)) by omega.
(* Goal: f x *)
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
 apply in_app; left; auto.
(* Goal: Z.le j (@Znth Z Inhabitant_Z i al) *)
 rewrite Z.max_l in H3 by omega.
 rewrite (sublist_split 0 1 (i+1)) by omega.
(* Goal: f x *)
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
 apply in_app; left; auto.
(* Goal: @Forall Z (Z.le j) (@sublist Z Z0 (Z.add i (Zpos xH)) al) *)
 rewrite (sublist_split 0 i (i+1)) by omega.
(* Goal: f x *)
(* Goal: f (@fold_right Z Z Z.min x (@cons Z x0 l)) *)
 apply Forall_app. split; auto.
(* Goal: @Forall Z (Z.le j) (@sublist Z i (Z.add i (Zpos xH)) al) *)
 rewrite sublist_one by omega.
(* Goal: Z.le j (@Znth Z Inhabitant_Z i al) *)
 repeat constructor. omega.
* (* After the loop *)
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun j : Z => PROPx (@cons Prop (@In Z j (@sublist Z Z0 (Z.max (Zpos xH) n) al)) (@cons Prop (@Forall Z (Z.le j) (@sublist Z Z0 n al)) (@nil Prop))) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr j))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred)))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
 Intros x.
 autorewrite with sublist in *.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr n))) (@cons localdef (temp _min (Vint (Int.repr x))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tint n) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _min tint))) POSTCONDITION *)
 forward. (* return *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@exp mpred Nveric Z (fun a0 : Z => @andp mpred Nveric (@prop mpred Nveric (and (@In Z a0 al) (and (@Forall Z (fun x : Z => Z.le a0 x) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr a0)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a))) *)
 Exists x.
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a) (@andp mpred Nveric (@prop mpred Nveric (and (@In Z x al) (and (@Forall Z (fun x0 : Z => Z.le x x0) al) (@eq val (Vint (Int.repr x)) (Vint (Int.repr x)))))) (@data_at CompSpecs Ews (tarray tint (@Zlength Z al)) (@map Int.int val Vint (@map Z Int.int Int.repr al)) a)) *)
 entailer!.
Qed.
