Require Import VST.floyd.proofauto. (* Import the Verifiable C system *)
Require Import VST.progs.bin_search. (* Import the AST of this C program *)
(* The next line is "boilerplate", always required after importing an AST. *)
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs.  mk_varspecs prog. Defined.

Fixpoint sorted (l : list Z) : Prop :=
  match l with
  | [] => True
  | x::rest =>
    match rest with [] => True | y::_ =>  x <= y /\ sorted rest end
  end.

(* Beginning of the API spec for the bin_search.c program *)
Definition search_spec :=
 DECLARE _search
  WITH a: val, sh : share, contents : list Z, tgt : Z, lo : Z, hi : Z
  PRE [ _a OF (tptr tint), _tgt OF tint, _lo OF tint, _hi OF tint ]
            PROP  (readable_share sh;
                     0 <= lo <= Int.max_signed; 
                     hi <= Zlength contents <= Int.max_signed;
                     Int.min_signed <= hi <= Int.max_signed / 2;
                     sorted contents;
                     Forall (fun x => Int.min_signed <= x <= Int.max_signed) contents;
                     Int.min_signed <= tgt <= Int.max_signed)
                  LOCAL (temp _a a; temp _tgt (Vint (Int.repr tgt));
                         temp _lo (Vint (Int.repr lo)); temp _hi (Vint (Int.repr hi)))
          SEP   (data_at sh (tarray tint (Zlength contents)) (map Vint (map Int.repr contents)) a)
  POST [ tint ]
    EX i:Z,
         PROP (if in_dec Z.eq_dec tgt (sublist lo hi contents) then Znth i contents = tgt else i = -1)
          LOCAL (temp ret_temp  (Vint (Int.repr i)))
           SEP (data_at sh (tarray tint (Zlength contents)) (map Vint (map Int.repr contents)) a).

(* The spec of "int main(void){}" always looks like this. *)
Definition main_spec :=
 DECLARE _main
  WITH gv: globals
  PRE  [] main_pre prog nil gv
  POST [ tint ] main_post prog nil gv.

(* Packaging the API spec all together. *)
Definition Gprog : funspecs :=
        ltac:(with_library prog [search_spec; main_spec]).

Lemma sublist_nil1 : forall A i j (l : list A), j <= i -> sublist i j l = [].
Proof.
(* Goal: forall (A : Type) (i j : Z) (l : list A) (_ : Z.le j i), @eq (list A) (@sublist A i j l) (@nil A) *)
  intros; destruct (eq_dec i j).
  - subst; apply sublist_nil.
  - unfold sublist; rewrite Z2Nat_neg; auto; omega.
Qed.

Lemma Znth_In : forall A (d: Inhabitant A) i (l : list A) x (Hrange : 0 <= i < Zlength l)
                       (Hnth : Znth i l = x), In x l.
Proof.
(* Goal: forall (A : Type) (d : Inhabitant A) (l : list A) (x : A) (_ : @In A x l), @ex Z (fun i : Z => and (and (Z.le Z0 i) (Z.lt i (@Zlength A l))) (@eq A (@Znth A d i l) x)) *)
  unfold Znth; intros.
(* Goal: @In A x l *)
  destruct (zlt i 0); [omega|].
(* Goal: @In A x l *)
  subst; apply nth_In.
(* Goal: lt (Z.to_nat i) (@Datatypes.length A l) *)
  rewrite Zlength_correct in Hrange; auto.
(* Goal: lt (Z.to_nat i) (@Datatypes.length A l) *)
  rep_omega.
Qed.

Lemma In_Znth : forall A (d: Inhabitant A) (l : list A) x,
    In x l ->
    exists i, 0 <= i < Zlength l /\ Znth i l = x.
Proof.
(* Goal: forall (A : Type) (d : Inhabitant A) (l : list A) (x : A) (_ : @In A x l), @ex Z (fun i : Z => and (and (Z.le Z0 i) (Z.lt i (@Zlength A l))) (@eq A (@Znth A d i l) x)) *)
  unfold Znth; intros.
(* Goal: @ex Z (fun i : Z => and (and (Z.le Z0 i) (Z.lt i (@Zlength A l))) (@eq A (if zlt i Z0 then @default A d else @nth A (Z.to_nat i) l d) x)) *)
  apply In_nth with (d := d) in H; destruct H as (n & ? & ?).
(* Goal: @ex Z (fun i : Z => and (and (Z.le Z0 i) (Z.lt i (@Zlength A l))) (@eq A (if zlt i Z0 then @default A d else @nth A (Z.to_nat i) l d) x)) *)
  exists (Z.of_nat n); split.
  - rewrite Zlength_correct; omega.
  - destruct (zlt (Z.of_nat n) 0); [omega|].
(* Goal: @eq A (@nth A (Z.to_nat (Z.of_nat n)) l d) x *)
    rewrite Nat2Z.id; auto.
Qed.

Lemma sublist_of_nil : forall A i j, sublist i j (nil : list A) = [].
Proof.
(* Goal: forall (A : Type) (i j : Z), @eq (list A) (@sublist A i j (@nil A : list A)) (@nil A) *)
  intros; unfold sublist.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub j i)) (@skipn A (Z.to_nat i) (@nil A))) (@nil A) *)
  rewrite skipn_nil, firstn_nil; auto.
Qed.

Fixpoint sorted2 l :=
  match l with
  | [] => True
  | x :: rest => Forall (fun y => x <= y) rest /\ sorted2 rest
  end.

Lemma sorted_equiv : forall l, sorted l <-> sorted2 l.
Proof.
(* Goal: forall l : list Z, iff (sorted l) (sorted2 l) *)
  induction l; simpl.
  - reflexivity.
  - destruct l.
    + simpl; split; auto.
    + rewrite IHl; simpl; split; intros (? & Hall & ?); split3; auto.
       * constructor; auto.
          rewrite Forall_forall in *; intros ? Hin.
(* Goal: Z.le a x *)
          specialize (Hall _ Hin); omega.
       * inversion H. auto.
Qed.

Lemma sorted_mono : forall l i j (Hsort : sorted l) (Hi : 0 <= i <= j)
                           (Hj : j < Zlength l),
    Znth i l <= Znth j l.
Proof.
(* Goal: forall (l : list Z) (i j : Z) (_ : sorted l) (_ : and (Z.le Z0 i) (Z.le i j)) (_ : Z.lt j (@Zlength Z l)), Z.le (@Znth Z Inhabitant_Z i l) (@Znth Z Inhabitant_Z j l) *)
induction l; intros.
* rewrite !Znth_nil. omega.
* 
(* Goal: Z.le (@Znth Z Inhabitant_Z i (@cons Z a l)) (@Znth Z Inhabitant_Z j (@cons Z a l)) *)
 rewrite sorted_equiv in Hsort. destruct Hsort as [H9 Hsort].
 rewrite <- sorted_equiv in Hsort. rewrite Forall_forall in H9.
(* Goal: Z.le (@Znth Z Inhabitant_Z i (@cons Z a l)) (@Znth Z Inhabitant_Z j (@cons Z a l)) *)
 rewrite Zlength_cons in Hj.
(* Goal: Z.le (@Znth Z Inhabitant_Z i (@cons Z a l)) (@Znth Z Inhabitant_Z j (@cons Z a l)) *)
 destruct (zeq i 0).
 +
(* Goal: Z.le (@Znth Z Inhabitant_Z i (@cons Z a l)) (@Znth Z Inhabitant_Z j (@cons Z a l)) *)
   subst i; rewrite Znth_0_cons. 
(* Goal: Z.le a (@Znth Z Inhabitant_Z j (@cons Z a l)) *)
   destruct (zeq j 0).
   - subst j. rewrite Znth_0_cons. omega.
   - rewrite Znth_pos_cons by omega.
(* Goal: Z.le a (@Znth Z Inhabitant_Z (Z.sub j (Zpos xH)) l) *)
      apply H9.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
      eapply Znth_In; [ | reflexivity]; omega.
 +
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
    rewrite !Znth_pos_cons by omega.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
    apply IHl; auto; omega.
Qed.

Lemma In_sorted_range : forall lo hi x l (Hsort : sorted l) (Hlo : 0 <= lo <= hi)
                              (Hhi : hi <= Zlength l)
                              (Hin : In x (sublist lo hi l)),
    Znth lo l <= x <= Znth (hi - 1) l.
Proof.
(* Goal: forall (A : Type) (l : list A) (x : A) (lo hi lo' hi' : Z) (_ : and (Z.le Z0 lo) (Z.le lo lo')) (_ : Z.le hi' hi) (_ : @In A x (@sublist A lo' hi' l)), @In A x (@sublist A lo hi l) *)
  intros.
(* Goal: and (Z.le (@Znth Z Inhabitant_Z lo l) x) (Z.le x (@Znth Z Inhabitant_Z (Z.sub hi (Zpos xH)) l)) *)
  generalize (In_Znth _ _ _ _ Hin); intros (i & Hrange & Hi).
(* Goal: readable_share Ews *)
(* Goal: and (and (Z.le Z0 Z0) (Z.le Z0 Int.max_signed)) (and (and (Z.le (Zpos (xO (xO xH))) (@Zlength Z four_contents)) (Z.le (@Zlength Z four_contents) Int.max_signed)) (and (and (Z.le Int.min_signed (Zpos (xO (xO xH)))) (Z.le (Zpos (xO (xO xH))) (Z.div Int.max_signed (Zpos (xO xH))))) (and (sorted four_contents) (and (@Forall Z (fun x : Z => and (Z.le Int.min_signed x) (Z.le x Int.max_signed)) four_contents) (and (Z.le Int.min_signed (Zpos (xI xH))) (Z.le (Zpos (xI xH)) Int.max_signed)))))) *)
  rewrite Zlength_sublist in Hrange by auto.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
  rewrite Znth_sublist in Hi by omega.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
  subst; split; apply sorted_mono; auto; omega.
Qed.

Lemma In_sorted_gt : forall x i n l lo hi (Hsort : sorted l) (Hlo : lo >= 0)
                            (Hhi : hi <= Zlength l)
                            (Hin : In x (sublist lo hi l))
                            (Hi : lo <= i < hi) (Hn : Znth i l = n)
                            (Hgt : n < x),
    In x (sublist (i + 1) hi l).
Proof.
(* Goal: forall (A : Type) (l : list A) (x : A) (lo hi lo' hi' : Z) (_ : and (Z.le Z0 lo) (Z.le lo lo')) (_ : Z.le hi' hi) (_ : @In A x (@sublist A lo' hi' l)), @In A x (@sublist A lo hi l) *)
  intros.
  rewrite sublist_split with (mid := i + 1) in Hin; try omega.
(* Goal: readable_share Ews *)
(* Goal: and (and (Z.le Z0 Z0) (Z.le Z0 Int.max_signed)) (and (and (Z.le (Zpos (xO (xO xH))) (@Zlength Z four_contents)) (Z.le (@Zlength Z four_contents) Int.max_signed)) (and (and (Z.le Int.min_signed (Zpos (xO (xO xH)))) (Z.le (Zpos (xO (xO xH))) (Z.div Int.max_signed (Zpos (xO xH))))) (and (sorted four_contents) (and (@Forall Z (fun x : Z => and (Z.le Int.min_signed x) (Z.le x Int.max_signed)) four_contents) (and (Z.le Int.min_signed (Zpos (xI xH))) (Z.le (Zpos (xI xH)) Int.max_signed)))))) *)
  rewrite in_app in Hin; destruct Hin; auto.
  generalize (In_sorted_range lo (i + 1) x _ Hsort); intro X.
(* Goal: @In Z x (@sublist Z lo i l) *)
  repeat (lapply X; [clear X; intro X | omega]).
  replace (i + 1 - 1) with i in X by omega.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
  specialize (X H); subst; omega.
Qed.

Lemma In_sorted_lt : forall x i n l lo hi (Hsort : sorted l) (Hlo : lo >= 0)
                            (Hhi : hi <= Zlength l)
                            (Hin : In x (sublist lo hi l))
                            (Hi : lo <= i < hi) (Hn : Znth i l = n)
                            (Hgt : x < n),
    In x (sublist lo i l).
Proof.
(* Goal: forall (A : Type) (l : list A) (x : A) (lo hi lo' hi' : Z) (_ : and (Z.le Z0 lo) (Z.le lo lo')) (_ : Z.le hi' hi) (_ : @In A x (@sublist A lo' hi' l)), @In A x (@sublist A lo hi l) *)
  intros.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
  rewrite sublist_split with (mid := i) in Hin; try omega.
(* Goal: readable_share Ews *)
(* Goal: and (and (Z.le Z0 Z0) (Z.le Z0 Int.max_signed)) (and (and (Z.le (Zpos (xO (xO xH))) (@Zlength Z four_contents)) (Z.le (@Zlength Z four_contents) Int.max_signed)) (and (and (Z.le Int.min_signed (Zpos (xO (xO xH)))) (Z.le (Zpos (xO (xO xH))) (Z.div Int.max_signed (Zpos (xO xH))))) (and (sorted four_contents) (and (@Forall Z (fun x : Z => and (Z.le Int.min_signed x) (Z.le x Int.max_signed)) four_contents) (and (Z.le Int.min_signed (Zpos (xI xH))) (Z.le (Zpos (xI xH)) Int.max_signed)))))) *)
  rewrite in_app in Hin; destruct Hin; auto.
(* Goal: @In Z x (@sublist Z lo i l) *)
  generalize (In_sorted_range i hi x _ Hsort); intro X.
(* Goal: @In Z x (@sublist Z lo i l) *)
  repeat (lapply X; [clear X; intro X | omega]).
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
  specialize (X H); subst; omega.
Qed.

Lemma Znth_In_sublist : forall A (d: Inhabitant A) i (l : list A) lo hi
  (Hlo : 0 <= lo <= i) (Hhi : i < hi <= Zlength l),
  In (Znth i l) (sublist lo hi l).
Proof.
(* Goal: forall (A : Type) (l : list A) (x : A) (lo hi lo' hi' : Z) (_ : and (Z.le Z0 lo) (Z.le lo lo')) (_ : Z.le hi' hi) (_ : @In A x (@sublist A lo' hi' l)), @In A x (@sublist A lo hi l) *)
  intros.
  apply Znth_In with (i := i - lo)(d := d).
  - rewrite Zlength_sublist; omega.
  - rewrite <- (Z.sub_simpl_r i lo) at 2.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
    apply Znth_sublist; omega.
Qed.

Lemma sublist_In_sublist : forall A (l : list A) x lo hi lo' hi' (Hlo : 0 <= lo <= lo')
  (Hhi : hi' <= hi), In x (sublist lo' hi' l) -> In x (sublist lo hi l).
Proof.
(* Goal: forall (A : Type) (l : list A) (x : A) (lo hi lo' hi' : Z) (_ : and (Z.le Z0 lo) (Z.le lo lo')) (_ : Z.le hi' hi) (_ : @In A x (@sublist A lo' hi' l)), @In A x (@sublist A lo hi l) *)
  intros.
  apply sublist_In with (lo0 := lo' - lo)(hi0 := hi' - lo); rewrite sublist_sublist;
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
    try split; try omega.
  - repeat rewrite Z.sub_simpl_r; auto.
  - destruct (Z_le_dec hi' lo'); try omega.
    rewrite sublist_nil1 in *; auto; simpl in *; contradiction.
Qed.

Lemma body_search: semax_body Vprog Gprog f_search search_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 (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo))) (@cons localdef (temp _hi (Vint (Int.repr hi))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Swhile (Ebinop Olt (Etempvar _lo tint) (Etempvar _hi tint) tint) LOOP_BODY) MORE_COMMANDS) POSTCONDITION *)
 destruct H0.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo))) (@cons localdef (temp _hi (Vint (Int.repr hi))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Swhile (Ebinop Olt (Etempvar _lo tint) (Etempvar _hi tint) tint) LOOP_BODY) MORE_COMMANDS) POSTCONDITION *)
 assert (H6 := Int.min_signed_neg).
 forward_while (EX lo' : Z, EX hi' : Z,
    PROP  (0 <= lo' <= Int.max_signed; 
           Int.min_signed <= hi' <= Int.max_signed / 2;
           hi' <= Zlength contents;
           In tgt (sublist lo hi contents) <-> In tgt (sublist lo' hi' contents))
    LOCAL (temp _a a; temp _tgt (Vint (Int.repr tgt));
           temp _lo (Vint (Int.repr lo')); temp _hi (Vint (Int.repr hi')))
    SEP   (data_at sh (tarray tint (Zlength contents))
                   (map Vint (map Int.repr contents)) a)).
 * Exists lo; Exists hi; entailer!.
 * entailer!.
 *
  match goal with H : _ <-> _ |- _ => rename H into H_tgt_sublist end.
  forward.  (* mid =  (lo + hi) >> 1; *) {
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _hi (Vint (Int.repr mid))) (@cons localdef (temp _val (Vint (Int.repr (@Znth Z Inhabitant_Z mid contents)))) (@cons localdef (temp _mid (Vint (Int.repr mid))) (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo'))) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred)))))) (PROPx (@cons Prop (and (Z.le Z0 lo') (Z.le lo' Int.max_signed)) (@cons Prop (and (Z.le Int.min_signed mid) (Z.le mid (Z.div Int.max_signed (Zpos (xO xH))))) (@cons Prop (Z.le mid (@Zlength Z contents)) (@cons Prop (iff (@In Z tgt (@sublist Z lo hi contents)) (@In Z tgt (@sublist Z lo' mid contents))) (@nil Prop))))) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo'))) (@cons localdef (temp _hi (Vint (Int.repr mid))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) *)
   entailer!.
   clear - H8 HRE H7.
   set (j := Int.max_signed / 2) in *; compute in j; subst j.
   set (j := Int.max_signed) in *; compute in j; subst j.
   set (j := Int.min_signed) in *; compute in j; subst j.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
   omega.
 }
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _mid (Vint (Int.shr (Int.add (Int.repr lo') (Int.repr hi')) (Int.repr (Zpos xH))))) (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo'))) (@cons localdef (temp _hi (Vint (Int.repr hi'))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Sset _val (Ederef (Ebinop Oadd (Etempvar _a (tptr tint)) (Etempvar _mid tint) (tptr tint)) tint)) MORE_COMMANDS) POSTCONDITION *)
  rewrite add_repr, Int.shr_div_two_p.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _mid (Vint (Int.repr (Z.div (Int.signed (Int.repr (Z.add lo' hi'))) (two_p (Int.unsigned (Int.repr (Zpos xH)))))))) (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo'))) (@cons localdef (temp _hi (Vint (Int.repr hi'))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Sset _val (Ederef (Ebinop Oadd (Etempvar _a (tptr tint)) (Etempvar _mid tint) (tptr tint)) tint)) MORE_COMMANDS) POSTCONDITION *)
  change (two_p (Int.unsigned (Int.repr 1))) with 2. 
  assert (Hlo'hi':  lo' + hi' <= Int.max_signed). {
   transitivity (Int.max_signed / 2 + Int.max_signed / 2).
   - apply Zplus_le_compat; omega.
   - rewrite Zplus_diag_eq_mult_2, Z.mul_comm. apply Z_mult_div_ge; omega.
  }
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
  rewrite !Int.signed_repr by omega.
  set (mid := (lo' + hi') / 2) in *.
  assert (H13: 0 <= mid < Zlength contents)
    by (subst; split; [apply Z_div_pos | apply Zdiv_lt_upper_bound]; omega).
  assert (H15: lo' <= mid < hi')
    by (split; [apply Zdiv_le_lower_bound | apply Zdiv_lt_upper_bound]; omega).
  assert (H16: Int.min_signed <= Znth mid contents <= Int.max_signed)
    by (rewrite Forall_forall in H3; apply H3; eapply Znth_In; eauto).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _mid (Vint (Int.repr mid))) (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo'))) (@cons localdef (temp _hi (Vint (Int.repr hi'))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Sset _val (Ederef (Ebinop Oadd (Etempvar _a (tptr tint)) (Etempvar _mid tint) (tptr tint)) tint)) MORE_COMMANDS) POSTCONDITION *)
  clear H3 Hlo'hi' H H0 H1.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _mid (Vint (Int.repr mid))) (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo'))) (@cons localdef (temp _hi (Vint (Int.repr hi'))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Sset _val (Ederef (Ebinop Oadd (Etempvar _a (tptr tint)) (Etempvar _mid tint) (tptr tint)) tint)) MORE_COMMANDS) POSTCONDITION *)
  clearbody mid.
  forward. (* val = a[mid]; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _val (Vint (Int.repr (@Znth Z Inhabitant_Z mid contents)))) (@cons localdef (temp _mid (Vint (Int.repr mid))) (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo'))) (@cons localdef (temp _hi (Vint (Int.repr hi'))) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sifthenelse (Ebinop Oeq (Etempvar _val tint) (Etempvar _tgt tint) tint) (Sreturn (@Some expr (Etempvar _mid tint))) (Sifthenelse (Ebinop Olt (Etempvar _val tint) (Etempvar _tgt tint) tint) (Sset _lo (Ebinop Oadd (Etempvar _mid tint) (Econst_int (Int.repr (Zpos xH)) tint) tint)) (Sset _hi (Etempvar _mid tint)))) POSTCONDITION *)
  autorewrite with sublist.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _val (Vint (Int.repr (@Znth Z Inhabitant_Z mid contents)))) (@cons localdef (temp _mid (Vint (Int.repr mid))) (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo'))) (@cons localdef (temp _hi (Vint (Int.repr hi'))) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sifthenelse (Ebinop Olt (Etempvar _val tint) (Etempvar _tgt tint) tint) (Sset _lo (Ebinop Oadd (Etempvar _mid tint) (Econst_int (Int.repr (Zpos xH)) tint) tint)) (Sset _hi (Etempvar _mid tint))) (normal_ret_assert (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (prod Z Z) (fun a0 : prod Z Z => PROPx (@cons Prop (and (Z.le Z0 (@fst Z Z a0)) (Z.le (@fst Z Z a0) Int.max_signed)) (@cons Prop (and (Z.le Int.min_signed (@snd Z Z a0)) (Z.le (@snd Z Z a0) (Z.div Int.max_signed (Zpos (xO xH))))) (@cons Prop (Z.le (@snd Z Z a0) (@Zlength Z contents)) (@cons Prop (iff (@In Z tgt (@sublist Z lo hi contents)) (@In Z tgt (@sublist Z (@fst Z Z a0) (@snd Z Z a0) contents))) (@nil Prop))))) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr (@fst Z Z a0)))) (@cons localdef (temp _hi (Vint (Int.repr (@snd Z Z a0)))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))))) *)
  forward_if.
  - forward. (* return mid; *)
(* 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 _hi (Vint (Int.repr mid))) (@cons localdef (temp _val (Vint (Int.repr (@Znth Z Inhabitant_Z mid contents)))) (@cons localdef (temp _mid (Vint (Int.repr mid))) (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo'))) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred)))))) (PROPx (@cons Prop (and (Z.le Z0 lo') (Z.le lo' Int.max_signed)) (@cons Prop (and (Z.le Int.min_signed mid) (Z.le mid (Z.div Int.max_signed (Zpos (xO xH))))) (@cons Prop (Z.le mid (@Zlength Z contents)) (@cons Prop (iff (@In Z tgt (@sublist Z lo hi contents)) (@In Z tgt (@sublist Z lo' mid contents))) (@nil Prop))))) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo'))) (@cons localdef (temp _hi (Vint (Int.repr mid))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) *)
    Exists mid; entailer!.
(* Goal: readable_share Ews *)
(* Goal: and (and (Z.le Z0 Z0) (Z.le Z0 Int.max_signed)) (and (and (Z.le (Zpos (xO (xO xH))) (@Zlength Z four_contents)) (Z.le (@Zlength Z four_contents) Int.max_signed)) (and (and (Z.le Int.min_signed (Zpos (xO (xO xH)))) (Z.le (Zpos (xO (xO xH))) (Z.div Int.max_signed (Zpos (xO xH))))) (and (sorted four_contents) (and (@Forall Z (fun x : Z => and (Z.le Int.min_signed x) (Z.le x Int.max_signed)) four_contents) (and (Z.le Int.min_signed (Zpos (xI xH))) (Z.le (Zpos (xI xH)) Int.max_signed)))))) *)
    rewrite if_true; auto. 
(* Goal: iff (@In Z tgt (@sublist Z lo hi contents)) (@In Z tgt (@sublist Z lo' mid contents)) *)
    rewrite H_tgt_sublist.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
    apply Znth_In_sublist; omega.
  - forward_if.
    + forward. (*  lo = mid + 1; *)
      Exists ((mid + 1), hi'); simpl fst; simpl snd; entailer!.
(* Goal: iff (@In Z tgt (@sublist Z lo hi contents)) (@In Z tgt (@sublist Z lo' mid contents)) *)
      rewrite H_tgt_sublist.
(* Goal: iff (@In Z tgt (@sublist Z lo' hi' contents)) (@In Z tgt (@sublist Z lo' mid contents)) *)
      split; intro Hin'.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
      eapply In_sorted_gt; eauto; omega.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
      eapply sublist_In_sublist; try apply Hin'; omega.
    + forward. (* hi=mid; *)
(* 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 _hi (Vint (Int.repr mid))) (@cons localdef (temp _val (Vint (Int.repr (@Znth Z Inhabitant_Z mid contents)))) (@cons localdef (temp _mid (Vint (Int.repr mid))) (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo'))) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred)))))) (PROPx (@cons Prop (and (Z.le Z0 lo') (Z.le lo' Int.max_signed)) (@cons Prop (and (Z.le Int.min_signed mid) (Z.le mid (Z.div Int.max_signed (Zpos (xO xH))))) (@cons Prop (Z.le mid (@Zlength Z contents)) (@cons Prop (iff (@In Z tgt (@sublist Z lo hi contents)) (@In Z tgt (@sublist Z lo' mid contents))) (@nil Prop))))) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo'))) (@cons localdef (temp _hi (Vint (Int.repr mid))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) *)
      Exists (lo',mid). simpl fst. simpl snd. entailer!.
(* Goal: iff (@In Z tgt (@sublist Z lo hi contents)) (@In Z tgt (@sublist Z lo' mid contents)) *)
      rewrite H_tgt_sublist.
(* Goal: iff (@In Z tgt (@sublist Z lo' hi' contents)) (@In Z tgt (@sublist Z lo' mid contents)) *)
      split; intro Hin'.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
      eapply In_sorted_lt; eauto; omega.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
      eapply sublist_In_sublist; try apply Hin'; omega.
 *
    forward.  (* return -1; *)
    Exists (-1); entailer!.
(* Goal: readable_share Ews *)
(* Goal: and (and (Z.le Z0 Z0) (Z.le Z0 Int.max_signed)) (and (and (Z.le (Zpos (xO (xO xH))) (@Zlength Z four_contents)) (Z.le (@Zlength Z four_contents) Int.max_signed)) (and (and (Z.le Int.min_signed (Zpos (xO (xO xH)))) (Z.le (Zpos (xO (xO xH))) (Z.div Int.max_signed (Zpos (xO xH))))) (and (sorted four_contents) (and (@Forall Z (fun x : Z => and (Z.le Int.min_signed x) (Z.le x Int.max_signed)) four_contents) (and (Z.le Int.min_signed (Zpos (xI xH))) (Z.le (Zpos (xI xH)) Int.max_signed)))))) *)
    rewrite if_false; auto.
    match goal with H : _ <-> _ |- _ => rewrite H end.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Z.add lo' hi')) (Z.le (Z.add lo' hi') (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) *)
    rewrite sublist_nil1 by omega.
(* Goal: readable_share Ews *)
(* Goal: and (and (Z.le Z0 Z0) (Z.le Z0 Int.max_signed)) (and (and (Z.le (Zpos (xO (xO xH))) (@Zlength Z four_contents)) (Z.le (@Zlength Z four_contents) Int.max_signed)) (and (and (Z.le Int.min_signed (Zpos (xO (xO xH)))) (Z.le (Zpos (xO (xO xH))) (Z.div Int.max_signed (Zpos (xO xH))))) (and (sorted four_contents) (and (@Forall Z (fun x : Z => and (Z.le Int.min_signed x) (Z.le x Int.max_signed)) four_contents) (and (Z.le Int.min_signed (Zpos (xI xH))) (Z.le (Zpos (xI xH)) Int.max_signed)))))) *)
    clear; simpl; tauto.
Qed.

(* Contents of the extern global initialized array "_four" *)
Definition four_contents := [1; 2; 3; 4].

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 (@data_at CompSpecs Ews (tarray tint (Zpos (xO (xO xH)))) (@map Int.int val Vint (@cons Int.int (Int.repr (Zpos xH)) (@cons Int.int (Int.repr (Zpos (xO xH))) (@cons Int.int (Int.repr (Zpos (xI xH))) (@cons Int.int (Int.repr (Zpos (xO (xO xH)))) (@nil Int.int)))))) (gv _four)) (@nil mpred))))) (Ssequence (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _search (Tfunction (Tcons (tptr tint) (Tcons tint (Tcons tint (Tcons tint Tnil)))) tint cc_default)) (@cons expr (Evar _four (tarray tint (Zpos (xO (xO xH))))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@cons expr (Econst_int (Int.repr Z0) tint) (@cons expr (Econst_int (Int.repr (Zpos (xO (xO xH)))) tint) (@nil expr)))))) (Sset _s (Etempvar _t'1 tint))) (Sreturn (@Some expr (Etempvar _s tint)))) MORE_COMMANDS) POSTCONDITION *)
  forward_call (gv _four,Ews,four_contents,3,0,4).
(* Goal: readable_share Ews *)
(* Goal: and (and (Z.le Z0 Z0) (Z.le Z0 Int.max_signed)) (and (and (Z.le (Zpos (xO (xO xH))) (@Zlength Z four_contents)) (Z.le (@Zlength Z four_contents) Int.max_signed)) (and (and (Z.le Int.min_signed (Zpos (xO (xO xH)))) (Z.le (Zpos (xO (xO xH))) (Z.div Int.max_signed (Zpos (xO xH))))) (and (sorted four_contents) (and (@Forall Z (fun x : Z => and (Z.le Int.min_signed x) (Z.le x Int.max_signed)) four_contents) (and (Z.le Int.min_signed (Zpos (xI xH))) (Z.le (Zpos (xI xH)) Int.max_signed)))))) *)
  { split. auto.
(* Goal: and (and (Z.le Z0 Z0) (Z.le Z0 Int.max_signed)) (and (and (Z.le (Zpos (xO (xO xH))) (@Zlength Z four_contents)) (Z.le (@Zlength Z four_contents) Int.max_signed)) (and (and (Z.le Int.min_signed (Zpos (xO (xO xH)))) (Z.le (Zpos (xO (xO xH))) (Z.div Int.max_signed (Zpos (xO xH))))) (and (sorted four_contents) (and (@Forall Z (fun x : Z => and (Z.le Int.min_signed x) (Z.le x Int.max_signed)) four_contents) (and (Z.le Int.min_signed (Zpos (xI xH))) (Z.le (Zpos (xI xH)) Int.max_signed)))))) *)
    change (Zlength four_contents) with 4.
(* Goal: and (and (Z.le Z0 Z0) (Z.le Z0 Int.max_signed)) (and (and (Z.le (Zpos (xO (xO xH))) (Zpos (xO (xO xH)))) (Z.le (Zpos (xO (xO xH))) Int.max_signed)) (and (and (Z.le Int.min_signed (Zpos (xO (xO xH)))) (Z.le (Zpos (xO (xO xH))) (Z.div Int.max_signed (Zpos (xO xH))))) (and (sorted four_contents) (and (@Forall Z (fun x : Z => and (Z.le Int.min_signed x) (Z.le x Int.max_signed)) four_contents) (and (Z.le Int.min_signed (Zpos (xI xH))) (Z.le (Zpos (xI xH)) Int.max_signed)))))) *)
    repeat constructor; computable.
  }
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo'))) (@cons localdef (temp _hi (Vint (Int.repr hi'))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sreturn (@Some expr (Eunop Oneg (Econst_int (Int.repr (Zpos xH)) tint) tint))) POSTCONDITION *)
  Intro r; forward.
Qed.

Existing Instance NullExtension.Espec.

Lemma prog_correct:
  semax_prog prog Vprog Gprog.
Proof.
(* Goal: semax_prog NullExtension.Espec CompSpecs prog Vprog Gprog *)
prove_semax_prog.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _search (@Internal function f_search)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function))))) (@cons (prod ident funspec) (@pair ident funspec _search (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _a (tptr tint)) (@cons (prod ident type) (@pair ident type _tgt tint) (@cons (prod ident type) (@pair ident type _lo tint) (@cons (prod ident type) (@pair ident type _hi tint) (@nil (prod ident type)))))) tint) cc_default (prod (prod (prod (prod (prod val share) (list Z)) Z) Z) Z) (fun x : prod (prod (prod (prod (prod val share) (list Z)) Z) Z) Z => let (p, hi) := x in let (p0, lo) := p in let (p1, tgt) := p0 in let (p2, contents) := p1 in let (a, sh) := p2 in PROPx (@cons Prop (readable_share sh) (@cons Prop (and (Z.le Z0 lo) (Z.le lo Int.max_signed)) (@cons Prop (and (Z.le hi (@Zlength Z contents)) (Z.le (@Zlength Z contents) Int.max_signed)) (@cons Prop (and (Z.le Int.min_signed hi) (Z.le hi (Z.div Int.max_signed (Zpos (xO xH))))) (@cons Prop (sorted contents) (@cons Prop (@Forall Z (fun x0 : Z => and (Z.le Int.min_signed x0) (Z.le x0 Int.max_signed)) contents) (@cons Prop (and (Z.le Int.min_signed tgt) (Z.le tgt Int.max_signed)) (@nil Prop)))))))) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _tgt (Vint (Int.repr tgt))) (@cons localdef (temp _lo (Vint (Int.repr lo))) (@cons localdef (temp _hi (Vint (Int.repr hi))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (fun x : prod (prod (prod (prod (prod val share) (list Z)) Z) Z) Z => let (p, hi) := x in let (p0, lo) := p in let (p1, tgt) := p0 in let (p2, contents) := p1 in let (a, sh) := p2 in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun i : Z => PROPx (@cons Prop (if @in_dec Z Z.eq_dec tgt (@sublist Z lo hi contents) then @eq Z (@Znth Z Inhabitant_Z i contents) tgt else @eq Z i (Zneg xH)) (@nil Prop)) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr i))) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred)))))))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun gv : globals => main_post prog (@nil Type) gv))) (@nil (prod ident funspec)))) *)
semax_func_cons body_search.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function)))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun gv : globals => main_post prog (@nil Type) gv))) (@nil (prod ident funspec))) *)
semax_func_cons body_main.
Qed.
