text:
Require Export MinBFTprops2.
Require Export MinBFTtacts2.

Section MinBFTsame.

  Local Open Scope eo.
  Local Open Scope proc.

  Context { dtc                 : DTimeContext        }.
  Context { microbft_context    : MinBFT_context      }.
  Context { m_initial_keys      : MinBFT_initial_keys }.
  Context { u_initial_keys      : USIG_initial_keys   }.
  Context { usig_hash           : USIG_hash           }.
  Context { microbft_auth       : MinBFT_auth         }.

  Lemma usig_step_same_id :
    forall {eo : EventOrdering} (e : Event) r t s s1 s2 u u1 u2,
      M_run_ls_on_this_one_event (MinBFTlocalSys_new r s s1 s2) e
      = Some (MinBFTlocalSys_new t u u1 u2)
      -> usig_id s1 = usig_id u1.
  Proof.
    introv h.
    apply map_option_Some in h; exrepnd; rev_Some; simpl in *; minbft_simp.
    unfold M_run_ls_on_input_ls, M_run_ls_on_input in *; simpl in *; autorewrite with minbft in *.

    Time minbft_dest_msg Case;
      repeat(simpl in *; autorewrite with minbft in *; smash_minbft2).
  Qed.

  Lemma usig_step_same_keys :
    forall {eo : EventOrdering} (e : Event) r t s s1 s2 u u1 u2,
      M_run_ls_on_this_one_event (MinBFTlocalSys_new r s s1 s2) e
      = Some (MinBFTlocalSys_new t u u1 u2)
      -> usig_local_keys s1 = usig_local_keys u1.
  Proof.
    introv h.
    apply map_option_Some in h; exrepnd; rev_Some; simpl in *; minbft_simp.
    unfold M_run_ls_on_input_ls, M_run_ls_on_input in *; simpl in *; autorewrite with minbft in *.

    Time minbft_dest_msg Case;
      repeat(simpl in *; autorewrite with minbft in *; smash_minbft2).
  Qed.

  Lemma usig_same_keys :
    forall {eo : EventOrdering} (e : Event) r t s s1 s2,
      M_run_ls_before_event (MinBFTlocalSys r) e
      = Some (MinBFTlocalSys_new t s s1 s2)
      -> usig_local_keys s1 = usig_initial_keys (usig_id s1).
  Proof.
    intros eo e.
    induction e as [e ind] using predHappenedBeforeInd;[]; introv h.
    rewrite M_run_ls_before_event_unroll in h.
    destruct (dec_isFirst e); ginv; auto; smash_minbft2;[].

    apply map_option_Some in h; exrepnd; rev_Some.
    applydup M_run_ls_before_event_ls_is_minbft in h1; exrepnd; subst.
    eapply ind in h1; eauto 3 with eo;[].
    applydup usig_step_same_keys in h0.
    applydup usig_step_same_id in h0.
    try congruence.
  Qed.

  Lemma usig_same_id :
    forall {eo : EventOrdering} (e : Event) r t s s1 s2,
      M_run_ls_before_event (MinBFTlocalSys r) e
      = Some (MinBFTlocalSys_new t s s1 s2)
      -> usig_id s1 = r.
  Proof.
    intros eo e.
    induction e as [e ind] using predHappenedBeforeInd;[]; introv h.
    rewrite M_run_ls_before_event_unroll in h.
    destruct (dec_isFirst e); ginv; auto; smash_minbft2;[].

    apply map_option_Some in h; exrepnd; rev_Some.
    applydup M_run_ls_before_event_ls_is_minbft in h1; exrepnd; subst.
    eapply ind in h1; eauto 3 with eo;[].
    applydup usig_step_same_id in h0.
    try congruence.
  Qed.

  Lemma usig_same_keys_on :
    forall {eo : EventOrdering} (e : Event) r t s s1 s2,
      M_run_ls_on_event (MinBFTlocalSys r) e
      = Some (MinBFTlocalSys_new t s s1 s2)
      -> usig_local_keys s1 = usig_initial_keys (usig_id s1).
  Proof.
    introv h.
    rewrite M_run_ls_on_event_unroll2 in h.
    apply map_option_Some in h; exrepnd; rev_Some.
    applydup M_run_ls_before_event_ls_is_minbft in h1; exrepnd; subst.
    apply usig_same_keys in h1.
    applydup usig_step_same_keys in h0.
    apply usig_step_same_id in h0; try congruence.
  Qed.

  Lemma usig_same_id_on :
    forall {eo : EventOrdering} (e : Event) r t s s1 s2,
      M_run_ls_on_event (MinBFTlocalSys r) e
      = Some (MinBFTlocalSys_new t s s1 s2)
      -> usig_id s1 = r.
  Proof.
    introv h.
    rewrite M_run_ls_on_event_unroll2 in h.
    apply map_option_Some in h; exrepnd; rev_Some.
    applydup M_run_ls_before_event_ls_is_minbft in h1; exrepnd; subst.
    apply usig_same_id in h1.
    apply usig_step_same_id in h0; try congruence.
  Qed.

  (* MOVE to ComponentSM2 *)
  Lemma M_run_ls_on_event_empty_ls :
    forall {eo : EventOrdering} (e : Event) l s ls,
      M_run_ls_on_event (empty_ls l s) e = Some ls
      -> ls = empty_ls l s.
  Proof.
    introv h.
    rewrite M_run_ls_on_event_unroll2 in h.
    apply map_option_Some in h; exrepnd; rev_Some.
    apply M_run_ls_before_event_empty_ls in h1; subst; simpl in *.
    apply map_option_Some in h0; exrepnd; rev_Some; ginv.
    inversion h1; subst; simpl in *; tcsp.
  Qed.

  Lemma state_usig_same_keys :
    forall {eo : EventOrdering} (e : Event) s,
      M_state_sys_on_event MinBFTsys e USIGname = Some s
      -> usig_local_keys s = usig_initial_keys (loc e).
  Proof.
    introv h.
    apply map_option_Some in h; exrepnd; rev_Some.
    remember (loc e) as x; destruct x; simpl in *; tcsp;
      [|apply M_run_ls_on_event_empty_ls in h1; subst; simpl in *; inversion h0];[].
    applydup M_run_ls_on_event_ls_is_minbft in h1; exrepnd; subst.
    applydup usig_same_id_on in h1.
    apply usig_same_keys_on in h1.
    simpl in *.
    unfold state_of_component in h0; simpl in *; ginv.
  Qed.

End MinBFTsame.

author: veri-fit

repo: Asphalion

save_path: github-repos/coq/veri-fit-Asphalion


text:
From Hammer Require Import Hammer.

Require Export Bool.

Section Bool_eq_dec.

Variable A : Set.

Variable beq : A -> A -> bool.

Variable beq_refl : forall x:A, true = beq x x.

Variable beq_eq : forall x y:A, true = beq x y -> x = y.

Definition beq_eq_true : forall x y:A, x = y -> true = beq x y.
Proof. hammer_hook "BoolEq" "BoolEq.beq_eq_true".
intros x y H.
case H.
apply beq_refl.
Defined.

Definition beq_eq_not_false : forall x y:A, x = y -> false <> beq x y.
Proof. hammer_hook "BoolEq" "BoolEq.beq_eq_not_false".
intros x y e.
rewrite <- beq_eq_true; trivial; discriminate.
Defined.

Definition beq_false_not_eq : forall x y:A, false = beq x y -> x <> y.
Proof. hammer_hook "BoolEq" "BoolEq.beq_false_not_eq".
exact
(fun (x y:A) (H:false = beq x y) (e:x = y) => beq_eq_not_false x y e H).
Defined.

Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}.
Proof. hammer_hook "BoolEq" "BoolEq.exists_beq_eq".
intros.
exists (beq x y).
constructor.
Defined.

Definition not_eq_false_beq : forall x y:A, x <> y -> false = beq x y.
Proof. hammer_hook "BoolEq" "BoolEq.not_eq_false_beq".
intros x y H.
symmetry .
apply not_true_is_false.
intro.
apply H.
apply beq_eq.
symmetry .
assumption.
Defined.

Definition eq_dec : forall x y:A, {x = y} + {x <> y}.
Proof. hammer_hook "BoolEq" "BoolEq.eq_dec".
intros x y; case (exists_beq_eq x y).
intros b; case b; intro H.
left; apply beq_eq; assumption.
right; apply beq_false_not_eq; assumption.
Defined.

End Bool_eq_dec.

author: lukaszcz

repo: coqhammer-eval


text:
(************************************************************************)
(* Copyright (c) 2017, Ajay Kumar Eeralla <ae266@mail.missouri.edu>     *)
(*                   University of Missouri-Columbia.                   *)
(*                                                                      *)
(*                                                                      *)
(*                                                                      *)
(************************************************************************)

Load "ex7_7".
(**  This library defines a theorem that states, [if not(b) then x else y = if b then y else x ].
(*<!-- Of course, we use ## (resp. ##) for message (resp. Bool) in lieu of [=]. -->*) *)

Theorem Example16_B :  forall (n:nat) (b1 b2 :Bool), (ifb (notb  (Bvar n)) b1 b2) ## (ifb (Bvar n) b2 b1).
Proof.
intros.
unfold notb.
assert(H1: (ifb (ifb (Bvar n) FAlse TRue) b1 b2) ##
    (ifb (Bvar n) (  ifb FAlse b1 b2) ( ifb TRue b1 b2))).

apply IFMORPH_B2 .
rewrite H1.
rewrite IFFALSE_B.
rewrite IFTRUE_B.
reflexivity.
Qed.
Theorem Example16_M :  forall (n:nat) (m1 m2:message), (ifm (notb  (Bvar n)) m1 m2) # (ifm (Bvar n) m2 m1).
Proof.
intros.
unfold notb.
assert(H1: (ifm (ifb (Bvar n) FAlse TRue) m1 m2) #
    (ifm (Bvar n) (  ifm FAlse m1 m2) ( ifm TRue m1 m2))).

apply IFMORPH_M2 .
rewrite H1.
rewrite IFFALSE_M.
rewrite IFTRUE_M.
reflexivity.
Qed.

author: ajayeeralla

repo: real-or-random-auth-proofs-coq


text:
(* generated by Ott 0.30, locally-nameless lngen from: ../ott/rules.ott *)
Require Import Bool.
Require Import Metalib.Metatheory.
Require Import List.
Require Import syntaxb_ott.
(** syntax *)

(* Parameter label : atom. *)

Inductive exp : Set :=  (*r expressions *)
 | e_var_b (_:nat) (*r variables *)
 | e_var_f (x:var) (*r variables *)
 | e_lit (i5:i) (*r lit *)
 | e_abs (e:exp) (p:var) (b:bool) (*r abstractions *)
 | e_app (e1:exp) (p:var) (b:bool) (e2:exp) (*r applications *)
 | e_anno (e:exp) (p:var) (b:bool) (A:typ) (*r annotation *)
 | e_appv (e1:exp)  (e2:exp) (*r applications *)
 | e_add : exp (*r addition *)
 | e_addl (i5:i) (*r addl *).

Inductive dirflag : Set :=  (*r checking direction *)
 | Inf : dirflag
 | Chk : dirflag.

 Inductive ddirflag2 : Set :=  (*r checking direction *)
 | Inf3 : ddirflag2
 | Chk3 (p:var) (b:bool): ddirflag2.

 Inductive dirflag2 : Set :=  (*r checking direction *)
 | Inf2 : dirflag2
 | Chk2 (p:var) (b:bool) (A:typ): dirflag2.

Definition ctx : Set := list ( atom * typ ).

Definition ls : Set := list st.

(* EXPERIMENTAL *)
(** auxiliary functions on the new list types *)
(** library functions *)
(** subrules *)
(** arities *)
(** opening up abstractions *)
Fixpoint open_exp_wrt_exp_rec (k:nat) (e_5:exp) (e__6:exp) {struct e__6}: exp :=
  match e__6 with
  | (e_var_b nat) =>
      match lt_eq_lt_dec nat k with
        | inleft (left _) => e_var_b nat
        | inleft (right _) => e_5
        | inright _ => e_var_b (nat - 1)
      end
  | (e_var_f x) => e_var_f x
  | (e_lit i5) => e_lit i5
  | (e_abs e l b) => e_abs (open_exp_wrt_exp_rec (S k) e_5 e) l b
  | (e_app e1 p b e2) => e_app (open_exp_wrt_exp_rec k e_5 e1) p b (open_exp_wrt_exp_rec k e_5 e2)
  | (e_anno e p b A) => e_anno (open_exp_wrt_exp_rec k e_5 e) p b A
  | (e_appv e1 e2) => e_appv (open_exp_wrt_exp_rec k e_5 e1) (open_exp_wrt_exp_rec k e_5 e2)
  | e_add => e_add
  | (e_addl i5) => e_addl i5
end.

Definition open_exp_wrt_exp e_5 e__6 := open_exp_wrt_exp_rec 0 e__6 e_5.

(** terms are locally-closed pre-terms *)
(** definitions *)

(* defns LC_exp *)
Inductive lc_exp : exp -> Prop :=    (* defn lc_exp *)
 | lc_e_var_f : forall (x:var),
     (lc_exp (e_var_f x))
 | lc_e_lit : forall (i5:i),
     (lc_exp (e_lit i5))
 | lc_e_abs : forall (e:exp) l b,
      ( forall x , lc_exp  ( open_exp_wrt_exp e (e_var_f x) )  )  ->
     (lc_exp (e_abs e l b))
 | lc_e_app : forall (e1 e2:exp) p b ,
     (lc_exp e1) ->
     (lc_exp e2) ->
     (lc_exp (e_app e1 p b e2))
 | lc_e_anno : forall (e:exp)  (p:var) (A:typ) b,
     (lc_exp e) ->
     (lc_exp (e_anno e p b A))
 | lc_e_appv : forall (e1 e2:exp),
     (lc_exp e1) ->
     (lc_exp e2) ->
     (lc_exp (e_appv e1 e2))
 | lc_e_add :
     (lc_exp e_add)
 | lc_e_addl : forall (i5:i),
     (lc_exp (e_addl i5)).

(** free variables *)
Fixpoint fv_exp (e_5:exp) : vars :=
  match e_5 with
  | (e_var_b nat) => {}
  | (e_var_f x) => {{x}}
  | (e_lit i5) => {}
  | (e_abs e l b) => (fv_exp e)
  | (e_app e1 p b e2) => (fv_exp e1) \u (fv_exp e2)
  | (e_anno e p b A) => (fv_exp e)
  | (e_appv e1 e2) => (fv_exp e1) \u (fv_exp e2)
  | e_add => {}
  | (e_addl i5) => {}
end.

(** substitutions *)
Fixpoint subst_exp (e_5:exp) (x5:var) (e__6:exp) {struct e__6} : exp :=
  match e__6 with
  | (e_var_b nat) => e_var_b nat
  | (e_var_f x) => (if eq_var x x5 then e_5 else (e_var_f x))
  | (e_lit i5) => e_lit i5
  | (e_abs e l b) => e_abs (subst_exp e_5 x5 e) l b
  | (e_app e1 p b e2) => e_app (subst_exp e_5 x5 e1) p b (subst_exp e_5 x5 e2)
  | (e_anno e p b A) => e_anno (subst_exp e_5 x5 e) p b A
  | (e_appv e1 e2) => e_appv (subst_exp e_5 x5 e1) (subst_exp e_5 x5 e2)
  | e_add => e_add
  | (e_addl i5) => (e_addl i5)
end.

(* principal types for values*)
Fixpoint principal_type (v:exp) : typ :=
  match v with
  | (e_lit i5) => t_int
  | (e_anno e p b A) => A
  | (e_abs e l b ) => (t_arrow t_dyn t_dyn)
  | (e_add) => (t_arrow t_int (t_arrow t_int t_int))
  | (e_addl i5) => (t_arrow t_int t_int)
  | _ => t_dyn
  end.

(* defns Values *)
Inductive value : exp -> Prop :=    (* defn value *)
 | value_lit : forall (i5:i),
     value (e_lit i5)
 | value_abs : forall e l b,
     lc_exp (e_abs e l b) ->
     value (e_abs e l b)
 | value_fanno : forall (v:exp) (A B C D:typ) (p:var) b,
     value v ->
      (t_arrow C D)  =   (principal_type   ( v )  )   ->
     value (e_anno v p b (t_arrow A B))
 | value_dyn : forall (v:exp) (p:var) b,
     Ground   (principal_type  v )   ->
     value v ->
     value  ( (e_anno v p b t_dyn) )
 | value_add :
     value e_add
 | value_addl : forall (i5:i),
     value  ( (e_addl i5) ).

Inductive walue : exp -> Prop :=    (* defn value *)
 | walue_lit : forall (i5:i),
     walue (e_lit i5)
 | walue_absd : forall e l b l0 b0,
     lc_exp (e_abs e l0 b0) ->
     walue (e_anno (e_abs e l0 b0) l b t_dyn)
 | walue_absa : forall e l b t1 t2 l0 b0,
     lc_exp (e_abs e l0 b0) ->
     walue (e_anno (e_abs e l0 b0) l b (t_arrow t1 t2))
 | walue_fanno : forall (v:exp) (A B C D:typ) l b,
     walue v ->
      (t_arrow C D)  =   (principal_type   ( v )  )   ->
     walue (e_anno v l b (t_arrow A B))
 | walue_dyn : forall (v:exp) l b,
     Ground   (principal_type  v )   ->
     walue v ->
     walue  ( (e_anno v l b t_dyn) )
 | walue_add :
     walue e_add
 | walue_addl : forall (i5:i),
     walue  ( (e_addl i5) ) .

Definition FLike A := not (A = t_dyn) /\ not (A = (t_arrow t_dyn t_dyn)) /\ (sim A (t_arrow t_dyn t_dyn)).

Inductive pattern : typ -> typ -> Prop :=
 | pa_abs : forall A B,
   pattern (t_arrow A B) (t_arrow A B)
 | pa_dyn:
   pattern t_dyn (t_arrow t_dyn t_dyn).

Inductive nlam : exp -> Prop :=
  | nl_var_b : forall nat,
    nlam (e_var_b nat)
 | nl_var_nat : forall (x:var),
     nlam (e_var_f x)
 | nl_var_f : forall (x:var),
     nlam (e_var_f x)
 | nl_lit : forall (i5:i),
     nlam (e_lit i5)
 | nl_app : forall (e1 e2:exp) l b ,
     nlam (e_app e1 l b e2)
 | nl_anno : forall (e:exp) (A:typ) l b ,
     nlam (e_anno e l b A)
 | nl_appv : forall (e1 e2:exp) ,
     nlam (e_appv e1 e2)
 | nl_add :
     nlam (e_add)
 | nl_addl : forall i,
     nlam (e_addl i).

(* defns Typing *)
Inductive Typing : ctx -> exp -> dirflag -> typ -> Prop :=    (* defn Typing *)
 | Typ_lit : forall (G:ctx) (i5:i),
      uniq  G  ->
     Typing G (e_lit i5) Inf t_int
 | Typ_var : forall (G:ctx) (x:var) (A:typ),
      uniq  G  ->
      binds  x A G  ->
     Typing G (e_var_f x) Inf A
 | Typ_abs : forall (L:vars) (G:ctx) (A:typ) (e:exp) (B:typ) l b,
      ( forall x , x \notin  L  -> Typing  (cons ( x , A )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk B )  ->
     Typing G (e_abs e l b ) Chk (t_arrow A B)
 | Typ_absd : forall (L:vars) (G:ctx) (e:exp) l b,
     ( forall x , x \notin  L  -> Typing  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk t_dyn )  ->
    Typing G (e_abs e l b ) Chk t_dyn
 | Typ_sugar : forall (L:vars) (G:ctx) (e:exp) l b,
    ( forall x , x \notin  L  -> Typing  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk t_dyn )  ->
   Typing G (e_abs e l b) Inf (t_arrow t_dyn t_dyn)
 | Typ_app : forall (G:ctx) (e1 e2:exp) (A1 A2 A:typ) l b,
     pattern A (t_arrow A1 A2) ->
     Typing G e1 Inf A ->
     Typing G e2 Chk A1 ->
     Typing G (e_app e1 l b e2) Inf A2
 | Typ_anno : forall (G:ctx) (e:exp) (p:var) b (A:typ),
     Typing G e Chk A ->
     Typing G  ( (e_anno e p b A) )  Inf A
 | Typ_sim : forall (G:ctx) (e:exp) (B A:typ),
     Typing G e Inf A ->
     sim A B ->
     nlam e ->
     Typing G e Chk B
 | Typ_appv : forall (G:ctx) (e1 e2:exp) (A1 A2:typ),
     Typing G e1 Inf (t_arrow A1 A2) ->
     Typing G e2 Inf A1 ->
     nlam e2 ->
     Typing G (e_appv e1 e2) Inf A2
 | Typ_add : forall (G:ctx),
     uniq  G  ->
     Typing G e_add Inf (t_arrow t_int  (t_arrow t_int t_int) )
 | Typ_addl : forall (G:ctx) (i1:i),
     uniq  G  ->
     Typing G (e_addl i1) Inf (t_arrow t_int t_int).

Fixpoint cal_p (e:exp) (x:var) : var :=
      match e with
      | (e_anno e p b A) => p
      | _ => x
      end.

Fixpoint cal_b (e:exp) : bool :=
      match e with
      | (e_anno e p b A) => b
      | _ => false
      end.

Fixpoint output (e:exp) (t:term) (l:var) (b:bool) (A: typ) (B: typ): term :=
      match e with
      | (e_abs e' l b) => t
      | _ => (trm_cast t l b A B)
      end.

Inductive typing : ctx -> exp -> ddirflag2 -> typ -> term -> Prop :=    (* defn Typing *)
 | typ_lit : forall (G:ctx) (i5:i) ,
      uniq  G  ->
     typing G (e_lit i5) Inf3 t_int (trm_lit i5)
 | typ_var : forall (G:ctx) (x:var) (A:typ),
      uniq  G  ->
      binds  x A G  ->
     typing G (e_var_f x) Inf3 A (trm_var_f x)
 | typ_abs : forall (L:vars) (G:ctx) (A:typ) (e:exp) (B:typ) l b l0 b0 t,
      ( forall x , x \notin  L  -> typing  (cons ( x , A )  G )   ( open_exp_wrt_exp e (e_var_f x) )  (Chk3 l b) B ( open_term_wrt_term t (trm_var_f x) ))  ->
     typing G (e_abs e l0 b0) (Chk3 l b) (t_arrow A B) (trm_abs A t)
 | typ_absd : forall (L:vars) (G:ctx) (e:exp) (t:term) l0 b0 l b,
      ( forall x , x \notin  L  -> typing  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) ) (Chk3 l b) t_dyn ( open_term_wrt_term t (trm_var_f x) ))  ->
     typing G (e_abs e l0 b0) (Chk3 l b) t_dyn (trm_cast (trm_abs t_dyn t) l b (t_arrow t_dyn t_dyn) t_dyn)
 | typ_sugar : forall (L:vars) (G:ctx) (e:exp) (t:term) l b,
     ( forall x , x \notin  L  -> typing  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  (Chk3 l b) t_dyn ( open_term_wrt_term t (trm_var_f x) ))  ->
    typing G (e_abs e l b) Inf3 (t_arrow t_dyn t_dyn) (trm_abs t_dyn t)
 | typ_app : forall (G:ctx) (e1 e2:exp) (B A:typ) (t1 t2:term) (l:var) b,
     typing G e1 Inf3 (t_arrow A B) t1 ->
     typing G e2 (Chk3 l b) A t2 ->
     typing G (e_app e1 l b e2) Inf3 B (trm_app t1 t2)
 | typ_anno : forall (G:ctx) (e:exp) (A:typ) l (t:term) b,
     typing G e (Chk3 l b) A t ->
     typing G  ( (e_anno e l b A) ) Inf3 A t
 | typ_sim : forall (G:ctx) (e:exp) (B A:typ) (t:term) (l:var) b,
     typing G e Inf3 A t ->
     sim A B ->
     nlam e ->
     typing G e (Chk3 l b) B (trm_cast t l b A B)
 | typ_appv : forall (G:ctx) (e1 e2:exp) (A1 A2:typ) t1 t2,
     typing G e1 Inf3 (t_arrow A1 A2) t1 ->
     typing G e2 Inf3 A1 t2 ->
     nlam e2 ->
     typing G (e_appv e1 e2) Inf3 A2 (trm_app t1 t2)
 | typ_appd : forall (G:ctx) (e1 e2:exp) (t1 t2:term) (l:var) b,
     typing G e1 Inf3 t_dyn t1 ->
     typing G e2 (Chk3 l b) t_dyn t2 ->
     typing G (e_app e1 l b e2) Inf3 t_dyn (trm_app (trm_cast t1 l b t_dyn (t_arrow t_dyn t_dyn)) t2)
 | typ_add : forall (G:ctx) ,
     uniq G ->
     typing G (e_add) Inf3 (t_arrow t_int (t_arrow t_int t_int)) (trm_add)
 | typ_addl : forall (G:ctx) i,
     uniq G ->
     typing G (e_addl i) Inf3 (t_arrow t_int t_int) (trm_addl i).

Inductive ttyping : ctx -> exp -> dirflag2 -> typ -> term -> Prop :=    (* defn Typing *)
 | ttyp_lit : forall (G:ctx) (i5:i) ,
      uniq  G  ->
     ttyping G (e_lit i5) Inf2 t_int (trm_lit i5)
 | ttyp_var : forall (G:ctx) (x:var) (A:typ),
      uniq  G  ->
      binds  x A G  ->
     ttyping G (e_var_f x) Inf2 A (trm_var_f x)
 | ttyp_abs : forall (L:vars) (G:ctx) (A:typ) (e:exp) (B:typ) l b t C l0 b0,
    ( forall x , x \notin  L  ->
    ttyping  (cons ( x , A )  G )   ( open_exp_wrt_exp e (e_var_f x) )  (Chk2 l b C) B ( open_term_wrt_term t (trm_var_f x) ))  ->
    nlam e ->
   ttyping G (e_abs e l0 b0) (Chk2 l b (t_arrow A B)) (t_arrow A B) (trm_abs A (trm_cast t l b C B))
 | ttyp_abs2 : forall (L:vars) (G:ctx) (A:typ) (e:exp) (B:typ) l b t C l0 b0,
    ( forall x , x \notin  L  ->
    ttyping  (cons ( x , A )  G )   ( open_exp_wrt_exp e (e_var_f x) )  (Chk2 l b C) B (trm_cast (open_term_wrt_term t (trm_var_f x) ) l b C B) )  ->
    not(nlam e) ->
   ttyping G (e_abs e l0 b0) (Chk2 l b (t_arrow A B)) (t_arrow A B) (trm_abs A (trm_cast t l b C B))
 | ttyp_absd : forall (L:vars) (G:ctx) (e:exp) (t:term) l b B l0 b0,
    ( forall x , x \notin  L  ->
    ttyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) ) (Chk2 l b B) t_dyn (open_term_wrt_term t (trm_var_f x) ))  ->
    nlam e ->
    ttyping G (e_abs e l0 b0  ) (Chk2 l b t_dyn) t_dyn (trm_cast (trm_abs t_dyn (trm_cast t l b B t_dyn)) l b (t_arrow t_dyn t_dyn) t_dyn)
 | ttyp_absd2 : forall (L:vars) (G:ctx) (e:exp) (t:term) l b B l0 b0,
    ( forall x , x \notin  L  ->
    ttyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) ) (Chk2 l b B) t_dyn (trm_cast (open_term_wrt_term t (trm_var_f x)) l b B t_dyn))  ->
    not(nlam e) ->
    ttyping G (e_abs e l0 b0) (Chk2 l b t_dyn) t_dyn (trm_cast (trm_abs t_dyn (trm_cast t l b B t_dyn)) l b (t_arrow t_dyn t_dyn) t_dyn)
 | ttyp_sugar : forall (L:vars) (G:ctx) (e:exp) (t:term) B l b,
   ( forall x , x \notin  L  ->
   ttyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  (Chk2 l b B) t_dyn (open_term_wrt_term t (trm_var_f x))  ) ->
   (nlam e) ->
   ttyping G (e_abs e l b) Inf2 (t_arrow t_dyn t_dyn) (trm_abs t_dyn (trm_cast t l b B t_dyn))
 | ttyp_sugar2 : forall (L:vars) (G:ctx) (e:exp) (t:term) B l b,
    ( forall x , x \notin  L  ->
    ttyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  (Chk2 l b B) t_dyn (trm_cast ( open_term_wrt_term t (trm_var_f x) ) l b B t_dyn) ) ->
    not(nlam e) ->
    ttyping G (e_abs e l b) Inf2 (t_arrow t_dyn t_dyn) (trm_abs t_dyn (trm_cast t l b B t_dyn))
 | ttyp_app : forall (G:ctx) (e1 e2:exp) (C B A:typ) (t1 t2:term) (l:var) b,
     ttyping G e1 Inf2 (t_arrow A B) t1 ->
     ttyping G (e_anno e2 l b A) Inf2 A t2 ->
     ttyping G (e_app e1 l b e2) Inf2 B (trm_app t1 t2)
 | ttyp_appd : forall (G:ctx) (e1 e2:exp) (t1 t2:term) (l:var) b,
     ttyping G e1 Inf2 t_dyn t1 ->
     ttyping G (e_anno e2 l b t_dyn) Inf2 t_dyn t2 ->
     ttyping G (e_app e1 l b e2) Inf2 t_dyn (trm_app (trm_cast t1 l b t_dyn (t_arrow t_dyn t_dyn)) t2)
 | ttyp_anno : forall (G:ctx) (e:exp) (A:typ) l (t:term) b B,
     ttyping G e (Chk2 l b B) A t ->
     nlam e ->
     ttyping G  ( (e_anno e l b A) ) Inf2 A (trm_cast t l b B A)
 | ttyp_anno2 : forall (G:ctx) (e:exp) (A:typ) l (t:term) b B l0 b0,
     ttyping G (e_abs e l0 b0) (Chk2 l b B) A t ->
     ttyping G  ( (e_anno (e_abs e l0 b0) l b A) ) Inf2 A t
 | ttyp_sim : forall (G:ctx) (e:exp) (B A:typ) (t:term) (l:var) b,
     ttyping G e Inf2 A t ->
     sim A B ->
     nlam e ->
     ttyping G e (Chk2 l b A) B t
 | ttyp_appv : forall (G:ctx) (e1 e2:exp) (A1 A2:typ) t1 t2,
     ttyping G e1 Inf2 (t_arrow A1 A2) t1 ->
     ttyping G e2 Inf2 A1 t2 ->
     nlam e2 ->
     ttyping G (e_appv e1 e2) Inf2 A2 (trm_app t1 t2).

Inductive ctx_item : Type :=
     | appCtxL : exp -> var -> bool -> ctx_item
     | appCtxR : exp -> var -> bool -> ctx_item
     | annoCtx : var -> bool -> typ -> ctx_item
     | appvCtxL : exp -> ctx_item
     | appvCtxR : exp -> ctx_item.

Notation Evactx := (list ctx_item).

Inductive wellformed : ctx_item -> Prop :=
     | wf_appCtxL : forall (e : exp) p b,
                   lc_exp e ->
                    wellformed (appCtxL e p b )
     | wf_appCtxR : forall (v : exp) p b A B,
                    principal_type v = (t_arrow A B) ->
                    value v ->
                    wellformed (appCtxR v p b)
     | wf_annoCtx : forall (A : typ)  (p:var) b,
                    wellformed (annoCtx p b A)
     | wf_appvCtxL : forall (e : exp) ,
                    lc_exp e ->
                     wellformed (appvCtxL e )
      | wf_appvCtxR : forall (v : exp) ,
                     value v ->
                     wellformed (appvCtxR v ).

Definition fill (E : ctx_item) (e : exp) : exp :=
     match E with
     | appCtxL e2 p b  => e_app e p b e2
     | appCtxR v1 p b => e_app v1 p b e
     | annoCtx p b A => e_anno e p b A
     | appvCtxL e2   => e_appv e  e2
     | appvCtxR v1  => e_appv v1  e
     end.

Inductive res : Type :=
     | e_exp  : exp -> res
     | e_blame : var -> bool -> res.

(* defns type precision *)
Inductive tpre : typ -> typ -> Prop :=    (* defn tpre *)
 | tp_i :
     tpre t_int t_int
 | tp_dyn : forall (A:typ),
     tpre A t_dyn
 | tp_abs : forall (A B C D:typ),
     tpre A C ->
     tpre B D ->
     tpre (t_arrow A B) (t_arrow C D).

(* defns Semantics *)
Inductive TypedReduce : exp -> var -> bool -> typ -> res -> Prop :=    (* defn TypedReduce *)
 | TReduce_abs: forall v A B C D p b,
   sim (t_arrow C D) (t_arrow A B) ->
   principal_type v = (t_arrow C D) ->
   TypedReduce v p b (t_arrow A B) (e_exp (e_anno v p b (t_arrow A B)))
  | TReduce_v : forall (v:exp)  (p:var) b,
   Ground(principal_type v) ->
   TypedReduce v p b t_dyn (e_exp (e_anno v p b t_dyn))
 | TReduce_lit : forall (i5:i) b (p:var),
     TypedReduce (e_lit i5) p b t_int (e_exp (e_lit i5))
 | TReduce_dd : forall (v:exp) (p:var) (q:var) b1 b2,
     lc_exp v ->
     TypedReduce  ( (e_anno v q b1 t_dyn) ) p b2 t_dyn  (e_exp  (e_anno v q b1 t_dyn) )
 | TReduce_anyd : forall (v:exp) (p:var) b,
      FLike (principal_type  v )  ->
     TypedReduce v p b t_dyn  (e_exp (e_anno  ( (e_anno v p b (t_arrow t_dyn t_dyn)) ) p b t_dyn) )
 | TReduce_adyn : forall e (A:typ) l1 b1 l2 b2 l0 b0,
     FLike A ->
     TypedReduce  ( (e_anno (e_abs e l0 b0) l1 b1 t_dyn) ) l2 b2 A  (e_exp (e_anno (e_anno (e_abs e l0 b0) l1 b1 (t_arrow t_dyn t_dyn)) l2 b2 A))
 | TReduce_absd : forall e l1 b1 l2 b2 l0 b0,
     TypedReduce  ( (e_anno (e_abs e l0 b0) l1 b1 t_dyn) )  l2 b2 (t_arrow t_dyn t_dyn)  (e_exp (e_anno (e_abs e l0 b0) l1 b1 (t_arrow t_dyn t_dyn)))
 | TReduce_dyna : forall (v:exp) (A:typ) (p:var) b1 b2 (q:var),
      FLike A ->
     sim (principal_type v) A ->
     nlam v ->
    TypedReduce  ( (e_anno v q b1 t_dyn) ) p b2 A  (e_exp (e_anno v p b2 A) )
 | TReduce_vany : forall (v:exp) (p:var)  (q:var) b1 b2,
    nlam v ->
   TypedReduce (e_anno v q b1 t_dyn) p b2 (principal_type  v) (e_exp v)
 | TReduce_blame : forall (v:exp) (A:typ) (p:var) b1 b2 (q:var),
      not (sim A (principal_type  v ))  ->
     TypedReduce (e_anno v q b1 t_dyn) p b2 A (e_blame p b2).

Inductive step : exp -> res -> Prop :=    (* defn step *)
  | do_step E e1 e2 :
       wellformed E ->
       step e1 (e_exp e2 ) ->
      step (fill E e1) (e_exp (fill E e2))
  | blame_step E e1 l b:
      wellformed E ->
      step e1 (e_blame l b) ->
      step (fill E e1) (e_blame l b)
 | Step_beta : forall (A:typ) (e:exp) (B:typ) (v : exp) l0 b0 l1 b1,
    lc_exp (e_abs e l0 b0) ->
    walue v ->
    step (e_appv (e_anno (e_abs e l0 b0) l1 b1 (t_arrow A B)) v)  (e_exp (e_anno  (  (open_exp_wrt_exp  e v )  )  l1 b1 B) )
 | Step_betap : forall (A:typ) (e:exp) (B:typ) v1 v2  l1 b1,
    value v1 ->
    value v2 ->
    principal_type (v1) = (t_arrow A B) ->
    TypedReduce v2 l1 b1 A (e_blame l1 b1) ->
    step (e_app v1 l1 b1 v2)  (e_blame l1 b1)
 | Step_annov : forall (v:exp) (A:typ) (v':res) (l:var) b,
     value v ->
     TypedReduce v l b A v' ->
     not (value (e_anno v l b A)) ->
     step (e_anno v l b A) v'
 | Step_abeta : forall (v1:exp) (A B:typ) (v2 :exp) l1 b1 C D,
     walue  ( (e_anno v1 l1 b1 (t_arrow A B)) )  ->
     walue v1 ->
     walue v2 ->
     principal_type v1 = (t_arrow C D) ->
     step (e_appv (e_anno v1 l1 b1 (t_arrow A B)) v2) (e_exp (e_anno (e_appv v1 (e_anno v2 l1 (negb b1) C)) l1 b1 B))
 | Step_equal : forall (v1:exp) (A B:typ) (v2 v2':exp) l b,
     value v1  ->
     value v2 ->
     principal_type (v1) = (t_arrow A B) ->
     TypedReduce v2 l b A (e_exp v2') ->
     step (e_app v1 l b v2) (e_exp (e_appv v1 v2'))
 | Step_betad : forall (v1:exp) (v2:exp) l1 b1 l2 b2 ,
    value  ( (e_anno v1 l1 b1 t_dyn) )  ->
    lc_exp v2 ->
    step (e_app (e_anno v1 l1 b1 t_dyn) l2 b2 v2) (e_exp (e_app (e_anno (e_anno v1 l1 b1 t_dyn) l2 b2 (t_arrow t_dyn t_dyn)) l2 b2 v2))
 | Step_add : forall (i1:i),
     step (e_appv (e_add)  (e_lit i1))  (e_exp (e_addl i1 ))
 | Step_addl : forall (i1:i) (i2:i),
     step (e_appv (e_addl i1)  (e_lit i2))  (e_exp (e_lit ( i1  +  i2 )))
 | Step_nbeta : forall (e:exp) (v : exp) l b,
    lc_exp (e_abs e l b) ->
    walue v ->
    step (e_appv (e_abs e l b) v)  (e_exp (e_anno (open_exp_wrt_exp  e v ) l b t_dyn) ).

Inductive sstep : exp -> res -> Prop :=    (* defn step *)
  | sdo_step E e1 e2 :
       wellformed E ->
       sstep e1 (e_exp e2 ) ->
      sstep (fill E e1) (e_exp (fill E e2))
  | sblame_step E e1 l b:
      wellformed E ->
      sstep e1 (e_blame l b) ->
      sstep (fill E e1) (e_blame l b)
 | sStep_beta : forall (A:typ) (e:exp) (B:typ) (v : exp) l1 b1 l2 b2 v' l0 b0,
    lc_exp (e_abs e l0 b0) ->
    value v ->
    TypedReduce v l2 b2 A (e_exp v') ->
    sstep (e_app (e_anno (e_abs e l0 b0) l1 b1 (t_arrow A B)) l2 b2 v)  (e_exp (e_anno  (  (open_exp_wrt_exp  e v' )  )  l1 b1 B) )
 | sStep_betap : forall (A:typ) (e:exp) (B:typ) v1 v2  l1 b1,
    value v1 ->
    value v2 ->
    principal_type (v1) = (t_arrow A B) ->
    TypedReduce v2 l1 b1 A (e_blame l1 b1) ->
    sstep (e_app v1 l1 b1 v2)  (e_blame l1 b1)
 | sStep_annov : forall (v:exp) (A:typ) (v':res) (l:var) b,
     value v ->
     TypedReduce v l b A v' ->
     not (value (e_anno v l b A)) ->
     sstep (e_anno v l b A) v'
 | sStep_abeta : forall (v1:exp) (A B:typ) (v2 :exp) l1 b1 C D v2' l b,
     walue  ( (e_anno v1 l1 b1 (t_arrow A B)) )  ->
     walue v1 ->
     value v2 ->
     principal_type v1 = (t_arrow C D) ->
     TypedReduce v2 l b A (e_exp v2') ->
     sstep (e_app (e_anno v1 l1 b1 (t_arrow A B)) l b v2) (e_exp (e_anno (e_app v1 l1 (negb b1) v2' ) l1 b1 B))
 | sStep_betad : forall (v1:exp) (v2:exp) l1 b1 l2 b2 ,
    value  ( (e_anno v1 l1 b1 t_dyn) )  ->
    lc_exp v2 ->
    sstep (e_app (e_anno v1 l1 b1 t_dyn) l2 b2 v2) (e_exp (e_app (e_anno (e_anno v1 l1 b1 t_dyn) l2 b2 (t_arrow t_dyn t_dyn)) l2 b2 v2))
 | sStep_add : forall (i1:i) l b v,
      value v ->
     TypedReduce v l b t_int (e_exp (e_lit i1)) ->
     sstep (e_app (e_add)  l b v)  (e_exp (e_addl i1 ))
 | sStep_addl : forall (i1:i) (i2:i) l b v,
       value v ->
      TypedReduce v l b t_int (e_exp (e_lit i2)) ->
     sstep (e_app (e_addl i1) l b v)  (e_exp (e_lit ( i1  +  i2 )))
 | sStep_nbeta : forall (e:exp) (v : exp) l b v' l0 b0,
    lc_exp (e_abs e l0 b0) ->
    value v ->
    TypedReduce v l b t_dyn (e_exp v') ->
    sstep (e_app (e_abs e l0 b0) l b v)  (e_exp (e_anno (open_exp_wrt_exp  e v') l0 b0 t_dyn) ).

Inductive precision : exp -> exp -> Prop :=    (* defn epre *)
 | epr_var : forall (x:var),
    precision (e_var_f x) (e_var_f x)
 |  epr_i i:
    precision (e_lit i) (e_lit i)
 |  epr_abs : forall (e1 e2:exp) (L:vars) l1 b1 l2 b2,
     ( forall x , x \notin  L  ->
      precision ( open_exp_wrt_exp e1 (e_var_f x) )   ( open_exp_wrt_exp e2 (e_var_f x) )  )  ->
      precision (e_abs e1 l1 b1) (e_abs e2 l2 b2)
 |  epr_app : forall (e1 e2 e1' e2':exp) l1 b1 l2 b2,
     precision e1 e1' ->
     precision e2 e2' ->
     precision (e_app e1 l1 b1 e2) (e_app e1' l2 b2 e2')
 |  epr_anno : forall (A B:typ) (e1 e2:exp) l1 b1 l2 b2,
     tpre A B ->
     precision e1 e2 ->
     precision (e_anno e1 l1 b1 A) (e_anno e2 l2 b2 B)
  | epr_add :
     precision e_add e_add
  | epr_addl : forall i,
     precision (e_addl i) (e_addl i).

Inductive steps : exp -> res -> Prop :=
  | step_refl e:
    steps e (e_exp e)

  | step_n e t' e':
    step e (e_exp e') ->
    steps e' (e_exp t') ->
    steps e  (e_exp t')

  | step_nb e e' l b:
    step e (e_exp e') ->
    steps e' (e_blame l b) ->
    steps e  (e_blame l b)

  | step_b e l b:
    step e (e_blame l b) ->
    steps e (e_blame l b).

Inductive epre_sz : ctx -> ctx -> exp -> exp -> nat -> Prop :=
 | eps_var : forall (x:var) G1 G2,
    epre_sz G1 G2 (e_var_f x) (e_var_f x) 1
 | eps_i i:forall G1 G2,
    epre_sz G1 G2 (e_lit i) (e_lit i) 1
 | eps_abs : forall (e1 e2:exp) (L:vars) G1 G2 n l1 b1 l2 b2,
    ( forall x , x \notin  L  ->
    epre_sz (cons ( x , t_dyn )  G1 )  (cons ( x , t_dyn )  G2 ) ( open_exp_wrt_exp e1 (e_var_f x) )   ( open_exp_wrt_exp e2 (e_var_f x) )  n )  ->
     epre_sz G1 G2 ((e_abs e1 l1 b1)) ((e_abs e2 l2 b2)) (n+1)
 | eps_app : forall (e1 e2 e1' e2':exp) l1 b1 l2 b2 G1 G2 n1 n2,
     epre_sz G1 G2 e1 e1' n1 ->
     epre_sz G1 G2 e2 e2' n2 ->
     epre_sz G1 G2 (e_app e1 l1 b1 e2) (e_app e1' l2 b2 e2') (n1+n2+1)
 | eps_anno : forall (A B:typ) (e1 e2:exp) l1 b1 l2 b2 G1 G2 n,
     tpre A B ->
     epre_sz G1 G2 e1 e2 n ->
     nlam e1 ->
     epre_sz G1 G2 (e_anno e1 l1 b1 A) (e_anno e2 l2 b2 B) (n+1)
 | eps_absn : forall (e1 e2:exp) (L:vars) G1 G2 A1 A2 B1 B2 A B l1 b1 l2 b2 ll1 bb1 ll2 bb2 n,
    ( forall x , x \notin  L  ->
     epre_sz (cons ( x , A1 )  G1 )  (cons ( x , B1 )  G2 ) ( open_exp_wrt_exp e1 (e_var_f x) )   ( open_exp_wrt_exp e2 (e_var_f x) )  n )  ->
     pattern A (t_arrow A1 A2) ->
     pattern B (t_arrow B1 B2) ->
     tpre A B ->
    epre_sz G1 G2 (e_anno (e_abs e1 ll1 bb1) l1 b1 A) (e_anno (e_abs e2 ll2 bb2) l2 b2 B) (n+1)
 | eps_annor : forall (A:typ) (e1 e2:exp) B1 B2 l b G1 G2 n,
   Typing G1 e1 Inf B1 ->
   Typing G2 e2 Inf B2 ->
   epre_sz G1 G2 e1 e2 n ->
   tpre B1 A ->
   tpre B1 B2 ->
   nlam e1 ->
   epre_sz G1 G2 e1 (e_anno e2 l b A) (n+1)
 | eps_annol : forall (A:typ) (e1 e2:exp) B1 B2 l b G1 G2 n,
   Typing G1 e1 Inf B1 ->
   Typing G2 e2 Inf B2 ->
   epre_sz G1 G2 e1 e2 n ->
   tpre A B2 ->
   tpre B1 B2 ->
   nlam e2 ->
   epre_sz G1 G2 (e_anno e1 l b A) e2 (n+1)
 | eps_appv : forall (e1 e2 e1' e2':exp) G1 G2 n1 n2,
     epre_sz G1 G2 e1 e1' n1 ->
     epre_sz G1 G2 e2 e2' n2 ->
     epre_sz G1 G2 (e_appv e1 e2) (e_appv e1' e2') (n1+n2+1)
  | eps_add : forall G1 G2 ,
     epre_sz G1 G2 e_add e_add 1
  | eps_addl : forall i G1 G2,
     epre_sz G1 G2 (e_addl i) (e_addl i) 1.

Inductive epre : ctx -> ctx -> exp -> exp -> Prop :=
 | ep_var : forall (x:var) G1 G2,
    uniq G1 ->
    uniq G2 ->
    epre G1 G2 (e_var_f x) (e_var_f x)
 | ep_i i:forall G1 G2,
    uniq G1 ->
    uniq G2 ->
    epre G1 G2 (e_lit i) (e_lit i)
 | ep_abs : forall (e1 e2:exp) (L:vars) G1 G2 l1 b1 l2 b2,
    ( forall x , x \notin  L  ->
     epre (cons ( x , t_dyn )  G1 )  (cons ( x , t_dyn )  G2 ) (e_anno (open_exp_wrt_exp e1 (e_var_f x)) l1 b1 t_dyn)   (e_anno (open_exp_wrt_exp e2 (e_var_f x)) l2 b2 t_dyn))  ->
    epre G1 G2 ((e_abs e1 l1 b1)) ((e_abs e2 l2 b2))
 | ep_app : forall (e1 e2 e1' e2':exp) l1 b1 l2 b2 G1 G2,
     epre G1 G2 e1 e1' ->
     epre G1 G2 e2 e2' ->
     nlam e2 ->
     epre G1 G2 (e_app e1 l1 b1 e2) (e_app e1' l2 b2 e2')
 | ep_anno : forall (A B:typ) (e1 e2:exp) l1 b1 l2 b2 G1 G2,
     tpre A B ->
     epre G1 G2 e1 e2 ->
     nlam e1 ->
     epre G1 G2 (e_anno e1 l1 b1 A) (e_anno e2 l2 b2 B)
 | ep_absn : forall (e1 e2:exp) (L:vars) G1 G2 A1 A2 B1 B2 A B l1 b1 l2 b2 ll1 bb1 ll2 bb2,
    ( forall x , x \notin  L  ->
     epre (cons ( x , A1 )  G1 )  (cons ( x , B1 )  G2 ) (e_anno (open_exp_wrt_exp e1 (e_var_f x)) l1 b1 A2)   (e_anno (open_exp_wrt_exp e2 (e_var_f x) ) l2 b2 B2)  )  ->
     pattern A (t_arrow A1 A2) ->
     pattern B (t_arrow B1 B2) ->
     tpre A B ->
    epre G1 G2 (e_anno (e_abs e1 ll1 bb1) l1 b1 A) (e_anno (e_abs e2 ll2 bb2) l2 b2 B)
 | ep_annor : forall (A:typ) (e1 e2:exp) B1 B2 l b G1 G2,
   Typing G1 e1 Inf B1 ->
   Typing G2 e2 Inf B2 ->
   epre G1 G2 e1 e2 ->
   tpre B1 A ->
   tpre B1 B2 ->
   nlam e1 ->
   epre G1 G2 e1 (e_anno e2 l b A)
 | ep_annol : forall (A:typ) (e1 e2:exp) B1 B2 l b G1 G2,
   Typing G1 e1 Inf B1 ->
   Typing G2 e2 Inf B2 ->
   epre G1 G2 e1 e2 ->
   tpre A B2 ->
   tpre B1 B2 ->
   nlam e2 ->
   epre G1 G2 (e_anno e1 l b A) e2
 | ep_appv : forall (e1 e2 e1' e2':exp) G1 G2,
     epre G1 G2 e1 e1' ->
     epre G1 G2 e2 e2' ->
     epre G1 G2 (e_appv e1 e2) (e_appv e1' e2')
  | ep_add : forall G1 G2,
      uniq G1 ->
    uniq G2 ->
     epre G1 G2 e_add e_add
  | ep_addl : forall i G1 G2,
   uniq G1 ->
    uniq G2 ->
     epre G1 G2 (e_addl i) (e_addl i)
  | ep_appa : forall (e1 e2 e1' e2':exp) l1 b1 l2 b2 G1 G2 A B A1 A2 B1 B2 ll1 bb1 ll2 bb2,
     Typing G1 e1 Inf A ->
     Typing G2 e1' Inf B ->
     pattern A (t_arrow A1 A2) ->
     pattern B (t_arrow B1 B2) ->
     epre G1 G2 e1 e1' ->
     epre G1 G2 (e_anno (e_abs e2 ll1 bb1) l1 b1 A1) (e_anno (e_abs e2' ll2 bb2) l2 b2 B1) ->
     epre G1 G2 (e_app e1 l1 b1 (e_abs e2 ll1 bb1)) (e_app e1' l2 b2 (e_abs e2' ll2 bb2)).

Inductive cpre : ctx -> ctx -> Prop :=
  | cp_nil:
      cpre nil nil
  | cp_cons: forall E F x A1 A2,
      tpre A1 A2 ->
      cpre E F ->
      cpre (cons ( x , A1 )  E) (cons ( x , A2 )  F).

Inductive elaborate : exp -> term -> Prop :=    (* defn Typing *)
 | el_lit : forall (i5:i),
     elaborate (e_lit i5) (trm_lit i5)
 | el_var : forall (x:var),
     elaborate (e_var_f x) (trm_var_f x)
 | el_abs : forall (L:vars) (e:exp) (t:term) A B l b l0 b0,
      ( forall x , x \notin  L  -> elaborate (e_anno (open_exp_wrt_exp e (e_var_f x)) l b B) (open_term_wrt_term t (trm_var_f x)))  ->
     elaborate (e_anno (e_abs e l0 b0) l b (t_arrow A B)) (trm_abs A t)
 | el_absd : forall (L:vars) (e:exp) (t:term) l b l0 b0,
      ( forall x , x \notin  L  -> elaborate (e_anno ( open_exp_wrt_exp e (e_var_f x) ) l b t_dyn)  ( open_term_wrt_term t (trm_var_f x) ))  ->
      elaborate (e_anno (e_abs e l0 b0) l b t_dyn) (trm_cast (trm_abs t_dyn t) l b (t_arrow t_dyn t_dyn) t_dyn)
 | el_app : forall (e1 e2:exp) (B A:typ) (t1 t2:term) l b,
     Typing nil e1 Inf (t_arrow A B) ->
     elaborate e1 t1 ->
     elaborate (e_anno e2 l b A) t2 ->
     elaborate (e_app e1 l b e2) (trm_app t1 t2)
 | el_anno : forall (e:exp) (A:typ) B (t:term) l b ,
     Typing nil e Inf A ->
     elaborate e t ->
     nlam e ->
     elaborate (e_anno e l b B) (trm_cast t l b A B)
 | el_appv : forall (v1 v2:exp) t1 t2 A B,
     Typing nil v1 Inf A ->
     Typing nil v2 Inf B ->
     elaborate v1 t1 ->
     elaborate v2 t2 ->
     value v1 ->
     walue v2 ->
     elaborate (e_appv v1 v2) (trm_app t1 t2)
 | el_sugar : forall (L:vars) (e:exp) (t:term) l b,
      ( forall x , x \notin  L  -> elaborate (e_anno (open_exp_wrt_exp e (e_var_f x)) l b t_dyn) (open_term_wrt_term t (trm_var_f x)))  ->
     elaborate (e_abs e l b) (trm_abs t_dyn t)
 | el_appd : forall (e1 e2:exp) (t1 t2:term) l b,
     Typing nil e1 Inf t_dyn ->
     elaborate e1 t1 ->
     elaborate (e_anno e2 l b t_dyn) t2 ->
     elaborate (e_app e1 l b e2) (trm_app (trm_cast t1 l b t_dyn (t_arrow t_dyn t_dyn)) t2).

 Inductive sub : typ -> typ -> Prop :=
  | sub_i :
      sub t_int t_int
  | sub_arr : forall (A B C D:typ),
      sub C A ->
      sub B D ->
      sub (t_arrow A B) (t_arrow C D)
  | sub_dyn :
      sub t_dyn t_dyn
  | sub_g : forall A B,
      Ground B ->
      sub A B ->
      sub A t_dyn.

Inductive suba : typ -> typ -> Prop :=
  | suba_i :
      suba t_int t_int
  | suba_arr : forall (A B C D:typ),
      subb C A ->
      suba B D ->
      suba (t_arrow A B) (t_arrow C D)
  | suba_dynr : forall (A:typ),
      suba A t_dyn
with subb : typ -> typ -> Prop :=
  | subb_i :
      subb t_int t_int
  | subb_arr : forall (A B C D:typ),
      suba C A ->
      subb B D ->
      subb (t_arrow A B) (t_arrow C D)
  | subb_dynl : forall (A:typ),
      subb t_dyn A
  | subd_g : forall A B C,
      Ground B ->
      subb A B ->
      subb A C.

 Inductive ssub : typ -> typ -> Prop :=
  | ssub_i :
      ssub t_int t_int
  | ssub_arr : forall (A B C D:typ),
      ssub C A ->
      ssub B D ->
      ssub (t_arrow A B) (t_arrow C D)
  | ssub_dyn :
      ssub t_dyn t_dyn
  | ssub_id :
      ssub t_int t_dyn
 | ssub_ad :
      ssub (t_arrow t_dyn t_dyn) t_dyn.

Inductive ssuba : typ -> typ -> Prop :=
  | ssuba_i :
      ssuba t_int t_int
  | ssuba_arr : forall (A B C D:typ),
      ssubb C A ->
      ssuba B D ->
      ssuba (t_arrow A B) (t_arrow C D)
  | ssuba_dynr : forall (A:typ),
      ssuba A t_dyn
with ssubb : typ -> typ -> Prop :=
  | ssubb_i :
      ssubb t_int t_int
  | ssubb_arr : forall (A B C D:typ),
      ssuba C A ->
      ssubb B D ->
      ssubb (t_arrow A B) (t_arrow C D)
  | ssubb_dynl : forall (A:typ),
      ssubb t_dyn A
  | ssubd_fg : forall C,
      ssubb (t_arrow t_dyn t_dyn) C
  | ssubd_ig : forall C,
      ssubb t_int C.

Inductive Safe : ctx -> exp -> var -> bool -> Prop :=
 | Safe_var : forall (x:var) l b G,
    uniq G ->
    Safe G (e_var_f x) l b
 | Safe_i: forall i l b G,
    uniq G ->
    Safe G (e_lit i) l b
 | Safe_abs : forall (e:exp) A B l1 b1 l2 b2 L G,
  ( forall x , x \notin  L  ->
    Safe (cons (x, A) G) (e_anno ( open_exp_wrt_exp e (e_var_f x) ) l1 b1 B) l2 b2 )  ->
    Safe G (e_anno (e_abs e l1 b1) l1 b1 (t_arrow A B)) l2 b2
 | Safe_absn : forall (e:exp) l2 b2 L G l b,
  ( forall x , x \notin  L  ->
    Safe (cons (x, t_dyn) G) (e_anno (open_exp_wrt_exp e (e_var_f x) ) l b t_dyn) l2 b2 )  ->
    Safe G ((e_abs e l b)) l2 b2
 | Safe_absd : forall (e:exp) l1 b1 l2 b2 L G,
  ( forall x , x \notin  L  ->
    Safe (cons (x, t_dyn) G) (e_anno ( open_exp_wrt_exp e (e_var_f x) ) l1 b1 t_dyn) l2 b2 )  ->
    Safe G (e_anno (e_abs e l1 b1) l1 b1 t_dyn) l2 b2
 | Safe_appd : forall (e1 e2 :exp) l1 b1 l2 b2 G,
    Typing G e1 Inf t_dyn ->
     Safe G (e_anno e1 l1 b1 (t_arrow t_dyn t_dyn)) l2 b2 ->
     Safe G (e_anno e2 l1 b1 t_dyn) l2 b2 ->
     Safe G (e_app e1 l1 b1 e2) l2 b2
 | Safe_app : forall (e1 e2 :exp) l1 b1 l2 b2 A1 A2 G,
    Typing G e1 Inf (t_arrow A1 A2) ->
     Safe G e1 l2 b2 ->
     Safe G (e_anno e2 l1 b1 A1) l2 b2 ->
     Safe G (e_app e1 l1 b1 e2) l2 b2
 | Safe_annoeq : forall (A:typ) B (e:exp) l b G,
     Typing G e Inf B ->
     suba B A ->
     Safe G e l b ->
     nlam e ->
     Safe G (e_anno e l b A) l b
 | Safe_annoeqn : forall (A:typ) B (e:exp) l b G ,
     Typing G e Inf B ->
     subb B A ->
     Safe G e l b ->
     nlam e ->
     Safe G (e_anno e l (negb b) A) l b
 | Safe_anno : forall (A:typ) (e:exp) l1 b1 l2 b2 G,
     Safe G e l2 b2 ->
     not(l1 = l2) ->
     not(b1 = b2) ->
     not((negb b1) = b2) ->
     nlam e ->
     Safe G (e_anno e l1 b1 A) l2 b2
 | Safe_appv : forall (e1 e2:exp) l b G,
     Safe G e1 l b  ->
     Safe G e2 l b  ->
     Safe G (e_appv e1 e2) l b
 | Safe_add : forall l b G ,
    uniq G ->
    Safe G e_add l b
 | Safe_addl : forall i l b G,
    uniq G ->
    Safe G (e_addl i) l b.

Inductive btyping : ctx -> term -> typ -> exp -> Prop :=    (* defn Btyping *)
 | btyp_lit : forall (G:ctx) (i5:i),
      uniq  G  ->
     btyping G (trm_lit i5) t_int (e_lit i5)
 | btyp_var : forall (G:ctx) (x:var) (A:typ),
      uniq  G  ->
      binds  x A G  ->
     btyping G (trm_var_f x) A (e_var_f x)
 | btyp_abs : forall (L:vars) (G:ctx) (A:typ) (t:term) (B:typ) e l b,
      ( forall x , x \notin  L  -> btyping  (cons ( x , A )  G )
      ( open_term_wrt_term t (trm_var_f x) )  B (e_anno ( open_exp_wrt_exp e (e_var_f x) ) l b B))  ->
     btyping G (trm_abs A t) (t_arrow A B) (e_anno (e_abs e l b) l b (t_arrow A B))
 | btyp_app : forall (G:ctx) (t1 t2:term) (B A:typ) e1 e2,
     btyping G t1 (t_arrow A B) e1 ->
     btyping G t2 A e2 ->
     btyping G (trm_app t1 t2) B (e_appv e1 e2)
 | btyp_add : forall (G:ctx),
     uniq  G  ->
     btyping G trm_add (t_arrow t_int  (t_arrow t_int t_int) ) e_add
 | btyp_addl : forall (G:ctx) (i1:i),
    uniq  G  ->
     btyping G (trm_addl i1) (t_arrow t_int t_int) (e_addl i1)
 | btyp_cast : forall (G:ctx) (t:term) (A B:typ) (p:var) b e,
     btyping G t A e ->
     sim A B ->
     btyping G  ( (trm_cast t p b A B) )  B (e_anno e p b B).

Inductive etyping : ctx -> exp -> dirflag -> typ -> exp -> Prop :=    (* defn Typing *)
 | etyp_lit : forall (G:ctx) (i5:i) ,
      uniq  G  ->
     etyping G (e_lit i5) Inf t_int (e_lit i5)
 | etyp_var : forall (G:ctx) (x:var) (A:typ),
      uniq  G  ->
      binds  x A G  ->
     etyping G (e_var_f x) Inf A (e_var_f x)
 | etyp_abs : forall (L:vars) (G:ctx) (A:typ) (e:exp) e1 (B:typ) l b,
      ( forall x , x \notin  L  -> etyping  (cons ( x , A )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk B ( open_exp_wrt_exp e1 (e_var_f x) ) )  ->
     etyping G (e_abs e l b) Chk (t_arrow A B) (e_abs e1 l b)
 | etyp_absd : forall (L:vars) (G:ctx) (e:exp) (t:term) e1 l b,
      ( forall x , x \notin  L  -> etyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) ) Chk t_dyn ( open_exp_wrt_exp e1 (e_var_f x) ) )  ->
     etyping G (e_abs e l b) Chk t_dyn (e_abs e1 l b)
 | etyp_sugar : forall (L:vars) (G:ctx) (e:exp) (t:term) e1 l b,
     ( forall x , x \notin  L  -> etyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk t_dyn  ( open_exp_wrt_exp e1 (e_var_f x) ))  ->
    etyping G (e_abs e l b) Inf (t_arrow t_dyn t_dyn) (e_abs e1 l b)
 | etyp_app : forall (G:ctx) (e1 e2:exp) (A1 A2 A:typ) (t1 t2:term) (l:var) b t1 t2,
     pattern A (t_arrow A1 A2) ->
     etyping G e1 Inf A t1 ->
     etyping G e2 Chk A1 t2 ->
     etyping G (e_app e1 l b e2) Inf A2 (e_app t1 l b t2)
 | etyp_appv : forall (G:ctx) (e1 e2:exp) (A1 A2:typ) (t1 t2:term) (l:var) b t1 t2,
     etyping G e1 Inf (t_arrow A1 A2) t1 ->
     etyping G e2 Inf A1 t2 ->
     nlam e2 ->
     nlam t2 ->
     etyping G (e_app e1 l b e2) Inf A2 (e_appv t1 t2)
 | etyp_anno : forall (G:ctx) (e:exp) (A:typ) l (t:term) b t,
     etyping G e Chk A t ->
     etyping G  ( (e_anno e l b A) ) Inf A  ( (e_anno t l b A) )
 | etyp_sim : forall (G:ctx) (e:exp) (B A:typ) t,
     etyping G e Inf A t ->
     sim A B ->
     nlam e ->
     nlam t ->
     etyping G e Chk B t
 | etyp_add : forall (G:ctx) ,
     uniq G ->
     etyping G (e_add) Inf (t_arrow t_int (t_arrow t_int t_int)) (e_add)
 | etyp_addl : forall (G:ctx) i,
     uniq G ->
     etyping G (e_addl i) Inf (t_arrow t_int t_int) (e_addl i).

Inductive atyping : ctx -> exp -> dirflag -> typ -> exp -> Prop :=    (* defn Typing *)
 | atyp_lit : forall (G:ctx) (i5:i) ,
      uniq  G  ->
      atyping G (e_lit i5) Inf t_int (e_lit i5)
 | atyp_var : forall (G:ctx) (x:var) (A:typ),
      uniq  G  ->
      binds  x A G  ->
      atyping G (e_var_f x) Inf A (e_var_f x)
 | atyp_abs : forall (L:vars) (G:ctx) (A:typ) (e:exp) e1 (B:typ) l b,
      ( forall x , x \notin  L  -> atyping  (cons ( x , A )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk B ( open_exp_wrt_exp e1 (e_var_f x) ) )  ->
      atyping G (e_abs e l b) Chk (t_arrow A B) (e_abs e1 l b)
 | atyp_absd : forall (L:vars) (G:ctx) (e:exp) e1 l b,
      ( forall x , x \notin  L  -> atyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) ) Chk t_dyn ( open_exp_wrt_exp e1 (e_var_f x) ) )  ->
      atyping G (e_abs e l b) Chk t_dyn (e_abs e1 l b)
 | atyp_sugar : forall (L:vars) (G:ctx) (e:exp) e1 l b,
     ( forall x , x \notin  L  -> atyping  (cons ( x , t_dyn )  G )   ( open_exp_wrt_exp e (e_var_f x) )  Chk t_dyn  ( open_exp_wrt_exp e1 (e_var_f x) ))  ->
    atyping G (e_abs e l b) Inf (t_arrow t_dyn t_dyn) (e_abs e1 l b)
 | atyp_appv : forall (G:ctx) (e1 e2:exp) (A1 A2:typ) (l:var) b t1 t2,
     atyping G e1 Inf (t_arrow A1 A2) t1 ->
     atyping G e2 Chk A1 t2 ->
     atyping G (e_app e1 l b e2) Inf A2 (e_appv t1 (e_anno t2 l b A1))
 | atyp_anno : forall (G:ctx) (e:exp) (A:typ) l t b,
     atyping G e Chk A t ->
     atyping G  ( (e_anno e l b A) ) Inf A  ( (e_anno t l b A) )
 | atyp_sim : forall (G:ctx) (e:exp) (B A:typ) t,
     atyping G e Inf A t ->
     sim A B ->
     nlam e ->
     atyping G e Chk B t
 | atyp_add : forall (G:ctx) ,
     uniq G ->
     atyping G (e_add) Inf (t_arrow t_int (t_arrow t_int t_int)) (e_add)
 | atyp_addl : forall (G:ctx) i,
     uniq G ->
     atyping G (e_addl i) Inf (t_arrow t_int t_int) (e_addl i)
 | atyp_app : forall (G:ctx) (e1 e2:exp) (A1 A2 A:typ)  (l:var) b t1 t2,
     pattern A (t_arrow A1 A2) ->
     atyping G e1 Inf A t1 ->
     atyping G e2 Chk A1 t2 ->
     atyping G (e_app e1 l b e2) Inf A2 (e_app t1 l b t2).

     Inductive ssteps : exp -> res -> Prop :=
     | sstep_refl e e':
       step e (e_exp e') ->
       ssteps e (e_exp e')

     | sstep_n e t' e':
       step e (e_exp e') ->
       ssteps e' (e_exp t') ->
       ssteps e  (e_exp t')

     | sstep_nb e e' l b:
       step e (e_exp e') ->
       ssteps e' (e_blame l b) ->
       ssteps e  (e_blame l b)

     | sstep_b e l b:
       step e (e_blame l b) ->
       ssteps e (e_blame l b).

Inductive stepss : exp -> res -> Prop :=
  | steps_refl e:
    stepss e (e_exp e)

  | steps_n e t' e':
    sstep e (e_exp e') ->
    stepss e' (e_exp t') ->
    stepss e  (e_exp t')

  | steps_nb e e' l b:
    sstep e (e_exp e') ->
    stepss e' (e_blame l b) ->
    stepss e  (e_blame l b)

  | steps_b e l b:
    sstep e (e_blame l b) ->
    stepss e (e_blame l b).

Inductive sstep_sz : exp -> res -> nat -> Prop :=
  | ssteps_refl e:
    sstep_sz e (e_exp e) 0

  | ssteps_n e t' e':  forall n,
    step e (e_exp e') ->
    sstep_sz e' (e_exp t') n ->
    sstep_sz e  (e_exp t') (1+n)

  | ssteps_nb e e' p b:forall n,
    step e (e_exp e') ->
    sstep_sz e' (e_blame p b) n ->
    sstep_sz e  (e_blame p b) (1+n)

  | ssteps_b e p b:
    step e (e_blame p b) ->
    sstep_sz e (e_blame p b) 1.

(** infrastructure *)
Hint Constructors sstep_sz stepss etyping ttyping ssub ssuba ssubb suba subb sub Safe pattern elaborate typing atyping sstep
precision epre epre_sz tpre cpre nlam Ground walue value sim TypedReduce step steps ssteps wellformed Typing typing lc_exp btyping: core.

author: YeWenjia

repo: TypedDirectedGradualTypingWithBlame


text:
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)

Require Import ssreflect.
Require Import ssrfun ssrbool TestSuite.ssr_mini_mathcomp.

Lemma ltn_leq_trans : forall n m p : nat, m < n -> n <= p -> m < p.
move=> n m p Hmn Hnp; rewrite -ltnS.
Fail rewrite (_ : forall n0 m0 p0 : nat, m0 <= n0 -> n0 < p0 -> m0 < p0).
Fail rewrite leq_ltn_trans.
Admitted.

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


text:
Inductive list (X:Type) : Type :=
  | nil : list X
  | cons : X -> list X -> list X.

Arguments nil {X}.
Arguments cons {X} _ _.

Notation "x :: y" := (cons x y)
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y)
                     (at level 60, right associativity).

author: FengZiGG

repo: coqlf

save_path: github-repos/coq/FengZiGG-coqlf


text:
Require Import Coq.omega.Omega.
Require Import Coq.Arith.Arith Platform.AutoSep Platform.Bags Platform.Malloc Platform.Queue Platform.Misc.
Import W_W_Bag.

Set Implicit Arguments.

Record tq_args (world : Type) := {
  World : world;
  Pointer : W;
  Settings : settings;
  Mem : smem
}.

Module Type S.
  Variable world : Type.

  Variable evolve : world -> world -> Prop.
  Axiom evolve_refl : forall w, evolve w w.
  Axiom evolve_trans : forall w1 w2 w3, evolve w1 w2 -> evolve w2 w3 -> evolve w1 w3.

  Variable globalInv : world -> W -> hpropB (tq_args world :: nil).
End S.

Definition localsInvariantExit (pre : vals -> W -> qspec) (rpStashed : bool) (adjustSp : W -> W)
  (ns : list string) (_ : nat) : assert :=
  st ~> let sp := adjustSp st#Sp in
    [| sp <> 0 |]
    /\ Ex vs, let res := wordToNat (sel vs "ss") - S (length ns) in
      [| freeable sp (wordToNat (sel vs "ss")) |]
      /\ qspecOut (pre (sel vs) st#Rv) (fun pre =>
        ![ locals ("rp" :: ns) vs res sp * pre ] st).

Notation "'PREexit' [ vs ] pre" := (localsInvariantExit (fun vs _ => pre%qspec%Sep))
  (at level 89).

Notation "'PREexit' [ vs , rv ] pre" := (localsInvariantExit (fun vs rv => pre%qspec%Sep))
  (at level 89).

Module Make(M : S).
Import M.

(* What does it mean for a program counter to be valid for a suspended thread? *)

Definition susp (w : world) (sc pc sp : W) : HProp := fun s m =>
  (Ex pc_tq : W, [| s.(Labels) ("threadq"!"ADT")%SP = Some pc_tq |]
    /\ ExX (* tq *) : tq_args world, Cptr pc_tq (_ ~> PropX.Forall #0)
    /\ ExX (* pre *) : settings * state, Cptr pc #0
    /\ ExX (* inv *) : settings * smem, #0 (s, m)
    /\ Al st : state, Al w' : world,
    [| evolve w w' |]
    /\ ![ #0 * (fun x y => Lift (Lift (Var0 {| World := w';
                                               Pointer := sc;
                                               Settings := x;
                                               Mem := y |})))
      * (fun x y => Lift (Lift (globalInv w' sc x y)))
      * ^[mallocHeap 0] ] (s, st)
    /\ [| Regs st Sp = sp |]
    ---> #1 (s, st))%PropX.

Lemma susp_intro : forall specs w sc pc sp P stn st,
  (exists pc_tq, stn.(Labels) ("threadq"!"ADT")%SP = Some pc_tq
    /\ exists tq, specs pc_tq = Some (fun _ => PropX.Forall tq)
      /\ exists pre, specs pc = Some (fun x => pre x)
        /\ exists inv, interp specs (![ inv * P ] (stn, st))
          /\ forall st' w', interp specs ([| evolve w w' |]
            /\ ![ inv
              * (fun x y => tq {| World := w';
                                  Pointer := sc;
                                  Settings := x;
                                  Mem := y |})
              * substH (globalInv w' sc) tq * mallocHeap 0 ] (stn, st')
            /\ [| Regs st' Sp = sp |]
            ---> pre (stn, st'))%PropX)
  -> interp specs (![ susp w sc pc sp * P ] (stn, st)).
  cptr.
Qed.

Lemma susp_elim : forall specs w sc pc sp P stn st,
  interp specs (![ susp w sc pc sp * P ] (stn, st))
  -> (exists pc_tq, stn.(Labels) ("threadq"!"ADT")%SP = Some pc_tq
    /\ exists tq, specs pc_tq = Some (fun _ => PropX.Forall tq)
      /\ exists pre, specs pc = Some (fun x => pre x)
        /\ exists inv, interp specs (![ inv * P ] (stn, st))
          /\ forall st' w', interp specs ([| evolve w w' |]
            /\ ![ inv * (fun x y => tq {| World := w';
                                          Pointer := sc;
                                          Settings := x;
                                          Mem := y |}) * substH (globalInv w' sc) tq * mallocHeap 0 ] (stn, st')
            /\ [| Regs st' Sp = sp |]
            ---> pre (stn, st'))%PropX).
  cptr.
  propxFo; eauto.
  descend; eauto.
  rewrite <- sepFormula_eq; descend.
  step auto_ext.
  eauto.
  make_Himp.
  apply Himp_refl.
Qed.

Inductive mergeSusp : Prop := MS.
Inductive splitSusp : Prop := SS.

Hint Constructors mergeSusp splitSusp.

Module Type TQ.
  Parameter susps : world -> bag -> W -> HProp.
  Parameter tq : world -> W -> HProp.

  Axiom tq_extensional : forall w sc, HProp_extensional (tq w sc).

  Axiom susps_empty_bwd : forall w sc, Emp ===> susps w empty sc.
  Axiom susps_add_bwd : forall w sc b pc sp, pc = pc -> mergeSusp -> susp w sc pc sp * susps w b sc ===> susps w (b %+ (pc, sp)) sc.
  Axiom susps_del_fwd : forall w sc b pc sp, (pc, sp) %in b -> susps w b sc ===> susp w sc pc sp * susps w (b %- (pc, sp)) sc.

  (* Below, the extra [locals] is a temporary stack for the threadq to use during sensitive
   * stack manipulations when the threads' own stacks may not be safe to touch. *)

  Axiom tq_fwd : forall w sc, tq w sc ===> Ex b, Ex p, Ex sp, Ex vs, (sc ==*> p, sp) * (sc ^+ $8) =?> 2
    * locals ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil) vs 14 sp
    * queue b p * susps w b sc.

  Axiom tq_bwd : forall w sc, (Ex b, Ex p, Ex sp, Ex vs, (sc ==*> p, sp) * (sc ^+ $8) =?> 2
    * locals ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil) vs 14 sp
    * queue b p * susps w b sc) ===> tq w sc.

  Axiom tq_weaken : forall w w' sc,
    evolve w w'
    -> tq w sc ===>* tq w' sc.
End TQ.

Module Tq : TQ.
  Open Scope Sep_scope.

  Definition susps (w : world) (b : bag) (sc : W) : HProp :=
    starB (fun p => susp w sc (fst p) (snd p)) b.

  Theorem susps_empty_bwd : forall w sc, Emp ===> susps w empty sc.
    intros; apply starB_empty_bwd.
  Qed.

  Theorem susps_add_bwd : forall w sc b pc sp, pc = pc -> mergeSusp -> susp w sc pc sp * susps w b sc ===> susps w (b %+ (pc, sp)) sc.
    intros; eapply Himp_trans; [ | apply starB_add_bwd ].
    unfold susps; simpl.
    apply Himp_star_comm.
  Qed.

  Theorem susps_del_fwd : forall w sc b pc sp, (pc, sp) %in b -> susps w b sc ===> susp w sc pc sp * susps w (b %- (pc, sp)) sc.
    intros; eapply Himp_trans; [ apply starB_del_fwd; eauto | apply Himp_refl ].
  Qed.

  Definition tq (w : world) (sc : W) : HProp :=
    Ex b, Ex p, Ex sp, Ex vs, (sc ==*> p, sp) * (sc ^+ $8) =?> 2
      * locals ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil) vs 14 sp
      * queue b p * susps w b sc.

  Theorem tq_extensional : forall w sc, HProp_extensional (tq w sc).
    reflexivity.
  Qed.

  Theorem tq_fwd : forall w sc, tq w sc ===> Ex b, Ex p, Ex sp, Ex vs, (sc ==*> p, sp) * (sc ^+ $8) =?> 2
    * locals ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil) vs 14 sp
    * queue b p * susps w b sc.
    unfold tq; sepLemma.
  Qed.

  Theorem tq_bwd : forall w sc, (Ex b, Ex p, Ex sp, Ex vs, (sc ==*> p, sp) * (sc ^+ $8) =?> 2
    * locals ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil) vs 14 sp
    * queue b p * susps w b sc) ===> tq w sc.
    unfold tq; sepLemma.
  Qed.

  Theorem into_ex : forall A (P P' : A -> _),
    (forall x, P x ===>* P' x)
    -> exB P ===>* exB P'.
    unfold HimpWeak; propxFo.
    apply H in H0; eauto.
  Qed.

  Theorem into_star : forall P P' Q Q',
    P ===>* P'
    -> Q ===>* Q'
    -> P * Q ===>* P' * Q'.
    unfold HimpWeak; propxFo.
    apply H in H1; apply H0 in H4; eauto.
  Qed.

  Theorem weak_refl : forall P,
    P ===>* P.
    unfold HimpWeak; auto.
  Qed.

  Theorem tq_weaken : forall w w' sc,
    evolve w w'
    -> tq w sc ===>* tq w' sc.
    unfold tq; intros; repeat match goal with
                                | [ |- exB _ ===>* exB _ ] => apply into_ex; intro
                                | [ |- (_ * _ ===>* _ * _)%Sep ] => apply into_star; try apply weak_refl
                              end.
    apply starB_weaken_weak; intros.
    unfold HimpWeak; propxFo; descend; eauto.
    eapply Imply_trans; [ | apply H5 ]; clear H5.
    descend.
    apply andL; apply injL; intro.
    apply andR; [ apply injR | ].
    eapply evolve_trans; eauto.
    apply Imply_refl.
  Qed.
End Tq.

Import Tq.
Export Tq.
Hint Immediate tq_extensional.

Definition locals_expose ns vs ss sp := locals ns vs ss sp.

Lemma expose_stack : forall ns vs ss sp,
  locals_expose ns vs ss sp ===> sp =?> (length ns + ss).
  unfold locals_expose, locals; intros; eapply Himp_trans; [ | apply allocated_join ].
  instantiate (1 := length ns).
  2: omega.
  Opaque mult.
  sepLemma.
  eapply Himp_trans; [ apply Himp_star_comm | ].
  eapply Himp_star_frame.
  eapply Himp_trans; [ apply ptsto32m_allocated | ].
  rewrite length_toArray; apply Himp_refl.
  apply allocated_shift_base.
  Require Import Coq.Arith.Arith.
  unfold natToW; rewrite mult_comm; words.
  omega.
  Transparent mult.
Qed.

Definition hints : TacPackage.
  prepare (tq_fwd, create_stack, expose_stack) (tq_bwd, susps_empty_bwd, susps_add_bwd).
Defined.

(* What is a valid initial code pointer for a thread, given the requested stack size? *)

Definition ginv w sc := substH (globalInv w sc) (fun x => tq (World x) (Pointer x) (Settings x) (Mem x)).

Definition starting (w : world) (sc pc : W) (ss : nat) : HProp := fun s m =>
  (ExX (* pre *) : settings * state, Cptr pc #0
    /\ [| semp m |]
    /\ Al st : state, Al vs, Al w',
      [| evolve w w' |]
      /\ [| Regs st Sp <> 0 /\ freeable (Regs st Sp) (1 + ss) |]
      /\ ![ ^[locals ("rp" :: nil) vs ss (Regs st Sp) * tq w' sc * ginv w' sc * mallocHeap 0] ] (s, st)
      ---> #0 (s, st))%PropX.

Local Hint Resolve split_a_semp_a semp_smem_emp.

Lemma starting_intro : forall specs sc w pc ss P stn st,
  (exists pre, specs pc = Some (fun x => pre x)
    /\ interp specs (![ P ] (stn, st))
    /\ forall st' vs w', interp specs ([| evolve w w' |]
      /\ [| Regs st' Sp <> 0 /\ freeable (Regs st' Sp) (1 + ss) |]
      /\ ![ locals ("rp" :: nil) vs ss (Regs st' Sp)
      * tq w' sc * ginv w' sc * mallocHeap 0 ] (stn, st')
    ---> pre (stn, st'))%PropX)
  -> interp specs (![ starting w sc pc ss * P ] (stn, st)).
  cptr.
Qed.

Lemma starting_elim : forall specs w sc pc ss P stn st,
  interp specs (![ starting w sc pc ss * P ] (stn, st))
  -> (exists pre, specs pc = Some (fun x => pre x)
    /\ interp specs (![ P ] (stn, st))
    /\ forall st' vs w', interp specs ([| evolve w w' |]
      /\ [| Regs st' Sp <> 0 /\ freeable (Regs st' Sp) (1 + ss) |]
      /\ ![ locals ("rp" :: nil) vs ss (Regs st' Sp)
      * tq w' sc * ginv w' sc * mallocHeap 0 ] (stn, st')
    ---> pre (stn, st'))%PropX).
  cptr.
  generalize (split_semp _ _ _ H0 H); intros; subst; auto.
  rewrite <- sepFormula_eq; descend; step auto_ext.
  eauto.
  eauto.
  make_Himp.
  apply Himp_refl.
Qed.

Definition susp' (w : world) (sc pc sp : W) : HProp := fun s m =>
  (ExX (* pre *) : settings * state, Cptr pc #0
    /\ ExX (* inv *) : settings * smem, #0 (s, m)
    /\ Al st : state, Al w' : world,
    [| evolve w w' |]
    /\ ![ #0 * ^[tq w' sc * ginv w' sc * mallocHeap 0] ] (s, st)
    /\ [| Regs st Sp = sp |]
    ---> #1 (s, st))%PropX.

Lemma susp_convert : forall specs w sc pc sp P stn st pc_tq,
  interp specs (![ susp' w sc pc sp * P ] (stn, st))
  -> Labels stn (labl "threadq" "ADT") = Some pc_tq
  -> specs pc_tq = Some (fun _ => PropX.Forall (fun x => tq (World x) (Pointer x) (Settings x) (Mem x)))
  -> interp specs (![ susp w sc pc sp * P ] (stn, st)).
  cptr.
  descend; step auto_ext.
  eauto.
  step auto_ext.
Qed.

Lemma susp'_intro : forall specs w sc pc sp P stn st,
  (exists pre, specs pc = Some (fun x => pre x)
    /\ exists inv, interp specs (![ inv * P ] (stn, st))
      /\ forall st' w', interp specs ([| evolve w w' |]
        /\ ![ inv * tq w' sc * ginv w' sc * mallocHeap 0 ] (stn, st')
        /\ [| Regs st' Sp = sp |]
        ---> pre (stn, st'))%PropX)
  -> interp specs (![ susp' w sc pc sp * P ] (stn, st)).
  cptr.
  descend; step auto_ext.
  eauto.
  descend; step auto_ext.
Qed.

Definition initS : spec := SPEC reserving 12
  Al w,
  PRE[_] mallocHeap 0
  POST[R] tq w R * mallocHeap 0.

Definition isEmptyS : spec := SPEC("sc") reserving 4
  Al w,
  PRE[V] tq w (V "sc") * mallocHeap 0
  POST[_] tq w (V "sc") * mallocHeap 0.

Definition spawnWithStackS : spec := SPEC("sc", "pc", "sp") reserving 14
  Al w,
  PRE[V] tq w (V "sc") * susp' w (V "sc") (V "pc") (V "sp") * mallocHeap 0
  POST[_] tq w (V "sc") * mallocHeap 0.

Definition spawnS : spec := SPEC("sc", "pc", "ss") reserving 18
  Al w,
  PRE[V] [| V "ss" >= $2 |] * tq w (V "sc") * starting w (V "sc") (V "pc") (wordToNat (V "ss") - 1) * mallocHeap 0
  POST[_] tq w (V "sc") * mallocHeap 0.

Definition localsInvariantExit' (pre : vals -> W -> qspec) (rpStashed : bool) (adjustSp : W -> W)
  (ns : list string) (_ : nat) : assert :=
  st ~> let sp := adjustSp st#Sp in
    Ex vs, qspecOut (pre (sel vs) st#Rv) (fun pre =>
      ![ locals ("rp" :: ns) vs 14 sp * pre ] st).

Local Notation "'PREexit'' [ vs ] pre" := (localsInvariantExit' (fun vs _ => pre%qspec%Sep))
  (at level 89).

Local Notation "'PREexit'' [ vs , rv ] pre" := (localsInvariantExit' (fun vs rv => pre%qspec%Sep))
  (at level 89).

Definition exitS : spec := SPEC("sc", "ss") reserving 0
  Al w,
  PREexit[V] [| V "ss" >= $3 |] * tq w (V "sc") * ginv w (V "sc") * mallocHeap 0.

Local Notation "'bexit' name ( x1 , .. , xN ) [ p ] b 'end'" :=
  (let p' := p in
   let vars := cons x1 (.. (cons xN nil) ..) in
    {| FName := name;
      FPrecondition := Precondition p' None;
      FBody := b%SP;
      FVars := vars;
      FReserved := Reserved p' |})
  (no associativity, at level 95, name at level 0, p at level 0, only parsing) : SPfuncs_scope.

Definition yieldS : spec := SPEC("sc") reserving 19
  Al w,
  PRE[V] tq w (V "sc") * ginv w (V "sc") * mallocHeap 0
  POST[_] Ex w', [| evolve w w' |] * tq w' (V "sc") * ginv w' (V "sc") * mallocHeap 0.

(* Next, some hijinks to prevent unnecessary unfolding of distinct memory cells for the threadq's stack. *)

Definition stackSize := 21.

Lemma stackSize_bound : natToW stackSize >= natToW 2.
  unfold stackSize; auto.
Qed.

Hint Immediate stackSize_bound.

Lemma stackSize_split : stackSize = length ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil) + 14.
  reflexivity.
Qed.

Opaque stackSize.

Definition yieldInvariantCont (pre : vals -> W -> qspec) (rpStashed : bool) (adjustSp : W -> W)
  (ns : list string) (res : nat) : assert :=
  st ~> let sp := adjustSp st#Sp in
    Ex vs, qspecOut (pre (sel vs) st#Rv) (fun pre =>
      ![ ^[locals ("rp" :: ns) vs res sp * pre] ] st).

Local Notation "'PREy' [ vs ] pre" := (yieldInvariantCont (fun vs _ => pre%qspec%Sep))
  (at level 89).

Notation "'badt' name p 'end'" :=
  {| FName := name;
    FPrecondition := (fun _ => PropX.Forall p);
    FBody := Diverge;
    FVars := nil;
    FReserved := 0 |}
  (no associativity, at level 95, name at level 0, p at level 0, only parsing) : SPfuncs_scope.

Definition m := bimport [[ "malloc"!"malloc" @ [mallocS], "malloc"!"free" @ [freeS],
    "queue"!"init" @ [Queue.initS], "queue"!"isEmpty" @ [Queue.isEmptyS],
    "queue"!"enqueue" @ [enqueueS], "queue"!"dequeue" @ [dequeueS] ]]
  bmodule "threadq" {{
    badt "ADT"
      (fun x => tq (World x) (Pointer x) (Settings x) (Mem x))
    end with bfunction "init"("q", "sp", "r") [initS]
      "q" <-- Call "queue"!"init"()
      [PRE[_, R] mallocHeap 0
       POST[R'] Ex sp, Ex vs, (R' ==*> R, sp) * (R' ^+ $8) =?> 2
         * locals ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil) vs 14 sp
         * mallocHeap 0];;

      "sp" <-- Call "malloc"!"malloc"(0, stackSize)
      [PRE[V, R] R =?> stackSize * mallocHeap 0
        POST[R'] Ex vs, (R' ==*> V "q", R) * (R' ^+ $8) =?> 2 * mallocHeap 0
         * locals ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil) vs 14 R];;

      Assert [PRE[V] mallocHeap 0
        POST[R] (R ==*> V "q", V "sp") * (R ^+ $8) =?> 2 * mallocHeap 0];;

      "r" <-- Call "malloc"!"malloc"(0, 4)
      [PRE[V, R] R =?> 4
       POST[R'] [| R' = R |] * (R ==*> V "q", V "sp") * (R ^+ $8) =?> 2 ];;
      "r" *<- "q";;
      "r" + 4 *<- "sp";;
      Return "r"
    end with bfunction "isEmpty"("sc") [isEmptyS]
      "sc" <-* "sc";;
      "sc" <-- Call "queue"!"isEmpty"("sc")
      [PRE[_, R] Emp
       POST[R'] [| R' = R |] ];;
      Return "sc"
    end with bfunction "spawnWithStack"("sc", "pc", "sp") [spawnWithStackS]
      Assert* [("threadq","ADT")] [Al w,
        PRE[V] tq w (V "sc") * susp w (V "sc") (V "pc") (V "sp") * mallocHeap 0
        POST[_] tq w (V "sc") * mallocHeap 0];;

      "sc" <-* "sc";;
      Note [mergeSusp];;
      Call "queue"!"enqueue"("sc", "pc", "sp")
      [Al w, Al b, Al sc,
        PRE[V] susps w (b %+ (V "pc", V "sp")) sc
         POST[_] susps w (b %+ (V "pc", V "sp")) sc];;
      Return 0
    end with bfunction "spawn"("sc", "pc", "ss") [spawnS]
      "ss" <-- Call "malloc"!"malloc"(0, "ss")
      [Al w, Al ss,
        PRE[V, R] tq w (V "sc") * starting w (V "sc") (V "pc") (ss - 1) * mallocHeap 0
          * R =?> ss * [| (ss >= 2)%nat |] * [| R <> 0 |] * [| freeable R ss |]
        POST[_] tq w (V "sc") * mallocHeap 0];;

      Assert [Al w, Al ss, Al vs,
        PRE[V] tq w (V "sc") * starting w (V "sc") (V "pc") ss * mallocHeap 0
          * locals ("rp" :: nil) vs ss (V "ss") * [| V "ss" <> 0 |] * [| freeable (V "ss") (1 + ss) |]
        POST[_] tq w (V "sc") * mallocHeap 0];;

      Assert* [("threadq","ADT")]
      [Al w,
        PRE[V] tq w (V "sc") * susp' w (V "sc") (V "pc") (V "ss") * mallocHeap 0
        POST[_] tq w (V "sc") * mallocHeap 0];;

      Call "threadq"!"spawnWithStack"("sc", "pc", "ss")
      [PRE[_] Emp
       POST[_] Emp];;
      Return 0
    end with bexit "exit"("sc", "ss", "curPc", "curSp", "newPc", "newSp") [exitS]
      Rp <-* "sc" + 4;;
      Rp + 4 *<- "sc";;
      Rp + 8 *<- "ss";;
      Rp + 12 *<- Sp;;
      Sp <- Rp;;

      Call "malloc"!"free"(0, "curPc", "ss")
      [Al w, Al q, Al qp, Al tsp,
        PREexit'[V] (V "sc" ==*> qp, tsp) * queue q qp * (V "sc" ^+ $8) =?> 2
          * susps w q (V "sc") * ginv w (V "sc") * mallocHeap 0];;

      "curPc" <-* "sc";;
      "curSp" <-- Call "queue"!"isEmpty"("curPc")
      [Al w, Al q, Al tsp,
        PREexit'[V, R] [| (q %= empty) \is R |]
          * queue q (V "curPc") * (V "sc" ==*> V "curPc", tsp)
          * (V "sc" ^+ $8) =?> 2 * susps w q (V "sc") * ginv w (V "sc") * mallocHeap 0];;

      If ("curSp" = 1) {
        (* No threads left to run.  Let's loop forever! *)
        Diverge
      } else {
        (* Pick a thread to switch to. *)

        "curSp" <- "sc" + 8;;
        Call "queue"!"dequeue"("curPc", "curSp")
        [Al w, Al q, Al tsp, Al pc, Al sp,
          PREexit'[V] [| (pc, sp) %in q |] * queue (q %- (pc, sp)) (V "curPc")
            * susps w (q %- (pc, sp)) (V "sc") * susp w (V "sc") pc sp
            * (V "sc" ==*> V "curPc", tsp, pc, sp) * ginv w (V "sc") * mallocHeap 0];;

        "sc" + 4 *<- Sp;;
        Rp <-* "sc" + 8;;
        Sp <-* "sc" + 12;;
        IGoto* [("threadq","ADT")] Rp
      }
    end with bfunction "yield"("sc", "ss", "curPc", "curSp", "newPc", "newSp") [yieldS]
      "ss" <-* "sc";;
      (* Using "curPc" as a temporary before getting to its primary use... *)
      "curPc" <-- Call "queue"!"isEmpty"("ss")
      [Al w, Al q, Al tsp, Al vs,
        PRE[V, R] [| (q %= empty) \is R |]
          * queue q (V "ss") * (V "sc" ==*> V "ss", tsp) * (V "sc" ^+ $8) =?> 2 * susps w q (V "sc")
          * ginv w (V "sc") * mallocHeap 0
          * locals ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil) vs 14 tsp
        POST[_] Ex w', [| evolve w w' |] * tq w' (V "sc") * ginv w' (V "sc") * mallocHeap 0];;

      If ("curPc" = 1) {
        (* No other threads to run.  Simply returning to caller acts like a yield. *)
        Rp <- $[Sp+0];;
        IGoto* [("threadq","ADT")] Rp
      } else {
        (* Pick a thread to switch to. *)
        "curPc" <- "sc" + 8;;
        Call "queue"!"dequeue"("ss", "curPc")
        [Al w, Al q, Al tsp, Al vs, Al pc, Al sp,
          PRE[V] [| (pc, sp) %in q |] * queue (q %- (pc, sp)) (V "ss")
            * susps w (q %- (pc, sp)) (V "sc") * susp w (V "sc") pc sp
            * (V "sc" ==*> V "ss", tsp, pc, sp) * ginv w (V "sc") * mallocHeap 0
            * locals ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil) vs 14 tsp
          POST[_] Ex w', [| evolve w w' |] * tq w' (V "sc") * ginv w' (V "sc") * mallocHeap 0];;
        "newPc" <-* "sc" + 8;;
        "newSp" <-* "sc" + 12;;

        Assert [Al w,
          PRE[V] susp w (V "sc") (V "newPc") (V "newSp") * tq w (V "sc") * ginv w (V "sc") * mallocHeap 0
          POST[_] Ex w', [| evolve w w' |] * tq w' (V "sc") * ginv w' (V "sc") * mallocHeap 0];;

        (* Initialize the temporary stack with data we will need, then switch to using it as our stack. *)
        "curPc" <-* "sc" + 4;;
        "ss" <-* "sc";;
        "curPc" + 4 *<- "sc";;
        "curPc" + 8 *<- "ss";;
        "curPc" + 12 *<- $[Sp+0];;
        "curPc" + 16 *<- Sp;;
        "curPc" + 20 *<- "newPc";;
        "curPc" + 24 *<- "newSp";;
        Sp <- "curPc";;

        Assert* [("threadq","ADT")]
        [PREy[V] Ex w, Ex sp, Ex b, (V "sc" ==*> V "ss", sp) * (V "sc" ^+ $8) =?> 2
          * queue b (V "ss") * susps w b (V "sc") * ginv w (V "sc") * mallocHeap 0
          * susp w (V "sc") (V "newPc") (V "newSp") * susp w (V "sc") (V "curPc") (V "curSp")];;

        Note [mergeSusp];;

        (* Enqueue current thread; note that variable references below resolve in the temporary stack. *)
        Call "queue"!"enqueue"("ss", "curPc", "curSp")
        [PREy[V] Ex w, Ex b, Ex p, Ex sp, (V "sc" ==*> p, sp) * (V "sc" ^+ $8) =?> 2
          * queue b p * susps w b (V "sc") * ginv w (V "sc")
          * mallocHeap 0 * susp w (V "sc") (V "newPc") (V "newSp")];;

        (* Jump to dequeued thread. *)
        "sc" + 4 *<- Sp;;
        Rp <- "newPc";;
        Sp <- "newSp";;
        IGoto* [("threadq","ADT")] Rp
      }
    end
  }}.

Local Hint Extern 1 (@eq W _ _) => words.

Ltac t := abstract (sep hints;
  try (apply himp_star_frame; [ reflexivity | apply susps_del_fwd; assumption ]);
    eauto).

Lemma wordBound : forall w : W,
  natToW 2 <= w
  -> (wordToNat w >= 2)%nat.
  intros; pre_nomega;
    rewrite wordToNat_natToWord_idempotent in * by reflexivity; assumption.
Qed.

Local Hint Immediate wordBound.

Hint Rewrite <- minus_n_O : sepFormula.

Theorem ok : moduleOk m.
  vcgen.

  t.

  t.
  t.
  t.
  t.
  t.
  t.
  t.
  t.
  t.

  post.
  rewrite stackSize_split in H0.
  assert (NoDup ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil)) by NoDup.
  evaluate hints; descend; repeat (step hints; descend); auto.

  t.
  t.
  t.
  t.
  t.

  t.
  t.
  t.
  t.
  t.
  t.
  t.
  t.

  t.
  t.
  t.

  post.
  toFront ltac:(fun P => match P with
                           | susp' _ _ _ _ => idtac
                         end) H0.
  eapply susp_convert in H0; eauto.
  t.

  t.
  t.
  t.
  t.
  t.
  t.
  t.

  t.
  t.
  t.
  t.
  t.
  t.

  post.
  match goal with
    | [ H : context[?X - 1] |- _ ] =>
      replace X with (length ("rp" :: nil) + (X - length ("rp" :: nil))) in H
  end.
  assert (NoDup ("rp" :: nil)) by NoDup.
  evaluate hints; sep hints; auto.
  evaluate hints; simpl; omega.

  post; evaluate auto_ext.
  match goal with
    | [ H : interp _ _ |- _ ] =>
      toFront ltac:(fun P => match P with
                               | starting _ _ _ _ => idtac
                             end) H;
      apply starting_elim in H; post; descend
  end.
  toFront_conc ltac:(fun P => match P with
                                | susp' _ _ _ _ => idtac
                              end);
  apply susp'_intro; descend.
  2: instantiate (5 := locals ("rp" :: nil) x2 x1 (sel x4 "ss")); sep_auto.
  eauto.
  eapply Imply_trans; [ | apply H6 ]; clear H6.
  descend; step auto_ext.
  step auto_ext.
  eauto.
  rewrite H6; auto.
  step auto_ext.
  step auto_ext.
  sep_auto.

  t.
  sep_auto; auto.
  t.
  t.
  t.

  t.

  post.

  Transparent evalInstrs.

  Theorem evalInstrs_app_fwd_None : forall stn is1 is2 st,
    evalInstrs stn st (is1 ++ is2) = None
    -> evalInstrs stn st is1 = None
    \/ exists st', evalInstrs stn st is1 = Some st' /\ evalInstrs stn st' is2 = None.
    induction is1; simpl; intuition eauto.
    destruct (evalInstr stn st a); eauto.
  Qed.

  Theorem evalInstrs_app_fwd_Some : forall stn is1 is2 st st',
    evalInstrs stn st (is1 ++ is2) = Some st'
    -> exists st'', evalInstrs stn st is1 = Some st'' /\ evalInstrs stn st'' is2 = Some st'.
    induction is1; simpl; intuition eauto.
    destruct (evalInstr stn st a); eauto.
    discriminate.
  Qed.

  Opaque evalInstrs.

  change (evalInstrs stn st
    ((Binop Rv (LvMem (Sp + 4)%loc) Plus 4
      :: Assign Rp (LvMem Rv)
      :: Binop Rv Rp Plus 4
      :: Assign (LvMem Rv) (LvMem (Sp + 4)%loc)
      :: Binop Rv Rp Plus 8
      :: Assign (LvMem Rv) (LvMem (Sp + 8)%loc)
      :: Binop Rv Rp Plus 12
      :: Assign (LvMem Rv) Sp
      :: Assign Sp Rp :: nil)
      ++ (Binop Rv Sp Plus 28
      :: Assign (LvMem (Rv + 4)%loc) 0
      :: Binop Rv Sp Plus 28
      :: Assign (LvMem (Rv + 8)%loc) (LvMem (Sp + 12)%loc)
      :: Binop Rv Sp Plus 28
      :: Assign (LvMem (Rv + 12)%loc) (LvMem (Sp + 8)%loc)
      :: Binop Sp Sp Plus 28 :: nil)) = None) in H0.

  apply evalInstrs_app_fwd_None in H0.
  destruct H0 as [ | [ ? [ ] ] ].
  evaluate hints.
  generalize dependent H0; evaluate hints; intro.

  change (locals ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil)
    (upd (upd (upd x4 "sc" (sel x0 "sc")) "ss" (sel x0 "ss")) "curPc" (Regs st Sp))
    14 x5)
    with (locals_call ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil)
      (upd (upd (upd x4 "sc" (sel x0 "sc")) "ss" (sel x0 "ss")) "curPc" (Regs st Sp))
      14 x5
      ("rp" :: "base" :: "p" :: "n" :: nil) 0 28) in H5.
  assert (ok_call ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil)
    ("rp" :: "base" :: "p" :: "n" :: nil)
    14 0 28)
  by (split; [ simpl; omega
    | split; [ simpl; omega
      | split; [ NoDup
        | reflexivity ] ] ]).
  evaluate hints.

  propxFo.
  change (evalInstrs stn x
    ((Binop Rv (LvMem (Sp + 4)%loc) Plus 4
      :: Assign Rp (LvMem Rv)
      :: Binop Rv Rp Plus 4
      :: Assign (LvMem Rv) (LvMem (Sp + 4)%loc)
      :: Binop Rv Rp Plus 8
      :: Assign (LvMem Rv) (LvMem (Sp + 8)%loc)
      :: Binop Rv Rp Plus 12
      :: Assign (LvMem Rv) Sp
      :: Assign Sp Rp :: nil)
      ++ (Binop Rv Sp Plus 28
      :: Assign (LvMem (Rv + 4)%loc) 0
      :: Binop Rv Sp Plus 28
      :: Assign (LvMem (Rv + 8)%loc) (LvMem (Sp + 12)%loc)
      :: Binop Rv Sp Plus 28
      :: Assign (LvMem (Rv + 12)%loc) (LvMem (Sp + 8)%loc)
      :: Binop Sp Sp Plus 28 :: nil)) = Some st) in H2.

  apply evalInstrs_app_fwd_Some in H2.
  destruct H2 as [ ? [ ] ].
  generalize dependent H2; evaluate hints; intro.
  change (locals ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil)
    (upd (upd (upd x5 "sc" (sel x1 "sc")) "ss" (sel x1 "ss")) "curPc" (Regs x Sp))
    14 x6)
    with (locals_call ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil)
      (upd (upd (upd x5 "sc" (sel x1 "sc")) "ss" (sel x1 "ss")) "curPc" (Regs x Sp))
      14 x6
      ("rp" :: "base" :: "p" :: "n" :: nil) 2 28) in H6.
  assert (ok_call ("rp" :: "sc" :: "ss" :: "curPc" :: "curSp" :: "newPc" :: "newSp" :: nil)
    ("rp" :: "base" :: "p" :: "n" :: nil)
    14 2 28)
  by (split; [ simpl; omega
    | split; [ simpl; omega
      | split; [ NoDup
        | reflexivity ] ] ]).
  change (locals ("rp" :: "sc" :: "ss" :: nil) x1 (wordToNat (sel x1 "ss") - 3) (Regs x Sp))
  with (locals_expose ("rp" :: "sc" :: "ss" :: nil) x1 (wordToNat (sel x1 "ss") - 3) (Regs x Sp)) in H6.
  evaluate hints.
  replace (S (S (S (wordToNat (sel x1 "ss") - 3)))) with (wordToNat (sel x1 "ss")) in H12.
  descend.
  step hints.
  step hints.
  step hints.
  unfold localsInvariantExit'; descend; step hints.
  descend; step hints.
  descend; step hints.
  generalize H9; clear.
  intros; pre_nomega.
  rewrite wordToNat_natToWord_idempotent in H9 by reflexivity; omega.

  t.
  t.
  unfold localsInvariantExit'; t.
  t.
  t.
  t.

  unfold localsInvariantExit'; post; evaluate hints.
  descend.
  step hints.
  2: step hints.
  eauto.
  step hints.
  descend; step hints.
  descend; step hints.
  apply susps_del_fwd; assumption.

  t.
  t.

  post; evaluate hints.
  match goal with
    | [ H : interp _ _ |- _ ] =>
      toFront ltac:(fun P => match P with
                               | susp _ _ _ _ => idtac
                             end) H;
      apply susp_elim in H; post
  end.
  descend.
  step auto_ext.
  match goal with
    | [ H : _ |- _ ] => eapply (Imply_sound (H _ _)); clear H; eauto
  end.
  propxFo.
  apply evolve_refl.
  unfold labl in H7; rewrite H1 in H7; injection H7; clear H1 H7; intros; subst.
  rewrite H9 in H2; injection H2; clear H2 H9; intros; subst.
  apply (f_equal (fun f => f (stn, st))) in H.

  Require Import Coq.Logic.Eqdep.
  injection H; clear H; intros; subst.
  do 2 apply inj_pair2 in H; subst; simpl.
  change (fun x y => tq x2 (sel x7 "sc") x y) with (tq x2 (sel x7 "sc")).
  change (fun st m => subst (globalInv x2 (sel x7 "sc") st m)
    (fun x : tq_args world => tq (World x) (Pointer x) (Settings x) (Mem x)))
    with (ginv x2 (sel x7 "sc")).
  step hints.

  t.
  t.
  t.
  t.

  post.
  evaluate hints.
  descend.
  step hints.
  step hints.
  step hints.
  descend; step hints.
  instantiate (2 := x8).
  instantiate (3 := upd x2 "ss" x9).
  descend; cancel hints.
  sep hints.
  sep hints.
  sep hints; auto.

  t.
  t.
  t.

  Hint Immediate evolve_refl.

  t.
  t.

  post; evaluate hints; descend.
  step hints.
  2: step hints.
  eauto.
  step hints.
  descend; step hints.
  instantiate (2 := x3).
  instantiate (3 := upd (upd x6 "curPc" (Regs x0 Rv)) "curPc" (sel x6 "sc" ^+ $8)).
  descend; cancel hints.
  step hints.
  apply himp_star_frame; [ reflexivity | apply susps_del_fwd; assumption ].
  step hints.
  sep hints; auto.

  t.
  t.
  t.
  t.

  post; evaluate hints.
  descend.
  instantiate (1 := upd (upd (upd (upd (upd (upd x7 "sc" (sel x3 "sc")) "ss" x9) "curPc"
    (sel x3 "rp")) "curSp" (Regs x0 Sp)) "newPc" (sel x3 "newPc")) "newSp" (sel x3 "newSp")); descend.
  toFront_conc ltac:(fun P => match P with
                                | susp _ _ (sel _ "rp") _ => idtac
                              end).
  apply susp_intro; descend; eauto.
  match goal with
    | [ _ : context[locals ?ns ?v ?a (Regs ?st Sp)] |- interp specs (![?P * _] _) ] =>
      equate P (locals ns v a (Regs st Sp) * (fun x y => x2 (x, y)))%Sep
  end.
  step hints.
  step auto_ext.
  step auto_ext.
  change (fun (x11 : ST.settings) (y : smem) => tq w' (sel x3 "sc") x11 y)
    with (tq w' (sel x3 "sc")).
  change (fun (st : ST.settings) (m0 : smem) =>
    subst (globalInv w' (sel x3 "sc") st m0)
      (fun x11 : tq_args world =>
        tq (World x11) (Pointer x11) (Settings x11) (Mem x11))) with (ginv w' (sel x3 "sc")).
  step auto_ext.

  t.
  t.

  post; evaluate hints; descend.
  instantiate (3 := x3).
  step hints.
  step hints.
  step hints.
  unfold yieldInvariantCont; descend; step hints.
  instantiate (8 := x3 %+ (sel x0 "curPc", sel x0 "curSp")).
  descend; step hints.

  t.
  t.

  post; evaluate hints.
  match goal with
    | [ H : interp _ _ |- _ ] =>
      toFront ltac:(fun P => match P with
                               | susp _ _ _ _ => idtac
                             end) H;
      apply susp_elim in H; post
  end.
  descend.
  step auto_ext.
  match goal with
    | [ H : _ |- _ ] => eapply (Imply_sound (H _ _)); eauto
  end.
  unfold labl in H7; rewrite H1 in H7; injection H7; clear H1 H7; intros; subst.
  rewrite H8 in H2; injection H2; clear H2 H8; intros; subst.
  apply (f_equal (fun f => f (stn, st))) in H1.
  injection H1; clear H1; intros; subst.
  do 2 apply inj_pair2 in H1; subst; simpl.
  instantiate (1 := x3).
  change (fun x y => tq x3 (sel x2 "sc") x y) with (tq x3 (sel x2 "sc")).
  change (fun st m => subst (globalInv x3 (sel x2 "sc") st m)
    (fun x : tq_args world => tq (World x) (Pointer x) (Settings x) (Mem x)))
    with (ginv x3 (sel x2 "sc")).
  propxFo.
  step hints.
Qed.

Transparent stackSize.

End Make.

author: JasonGross


text:
(*|
################################
How to do induction differently?
################################

:Link: https://stackoverflow.com/q/43011411
|*)

(*|
Question
********

I am doing an exercise in Coq and trying to prove if a list equals to
its reverse, it's a palindrome. Here is how I define palindromes:
|*)

Require Import List. (* .none *)
Import ListNotations. (* .none *)
Inductive pal {X : Type} : list X -> Prop :=
| emptypal : pal []
| singlpal : forall x, pal [x]
| inducpal : forall x l, pal l -> pal (x :: l ++ [x]).

(*| Here is the theorem: |*)

Theorem palindrome3 : forall {X : Type} (l : list X),
    l = rev l -> pal l.

(*|
According to my definition, I will need to do the induction my
extracting the front and tail element but apparently coq won't let me
do it, and if I force it to do so, it gives an induction result that
definitely doesn't make any sense:
|*)

Proof.
  intros X l H. remember (rev l) as rl. induction l, rl.
  - apply emptypal.
  - inversion H.
  - inversion H.
  - (* stuck *)

(*| context: |*)

    Show. (* .unfold .messages *)
Abort. (* .none *)

(*|
apparently the inductive context is terribly wrong. is there any way I
can fix the induction?
|*)

(*|
Answer
******

The solution I propose here is probably not the shortest one, but I
think it is rather natural.

My solution consists in defining an induction principle on ``list``
specialized to your problem.

Consider natural numbers. There is not only the standard induction
``nat_ind`` where you prove ``P 0`` and ``forall n, P n -> P (S n)``.
But there are other induction schemes, e.g., the strong induction
`lt_wf_ind
<https://coq.inria.fr/library/Coq.Arith.Wf_nat.html#lt_wf_ind>`__, or
the two-step induction where you prove ``P 0``, ``P 1`` and ``forall
n, P n -> P (S (S n))``. If the standard induction scheme is not
strong enough to prove the property you want, you can try another one.

We can do the same for lists. If the standard induction scheme
``list_ind`` is not enough, we can write another one that works. In
this idea, we define for lists an induction principle similar to the
two-step induction on ``nat`` (and we will prove the validity of this
induction scheme using the two-step induction on ``nat``), where we
need to prove three cases: ``P []``, ``forall x, P [x]`` and ``forall
x l x', P l -> P (x :: l ++ [x'])``. The proof of this scheme is the
difficult part. Applying it to deduce your theorem is quite
straightforward.

I don't know if the two-step induction scheme is part of the standard
library, so I introduce it as an axiom.
|*)

Axiom nat_ind2 : forall P : nat -> Prop,
    P 0 -> P 1 -> (forall n : nat, P n -> P (S (S n))) -> forall n : nat, P n.

(*| Then we prove the induction scheme we want. |*)

Lemma list_ind2 :
  forall {A} (P : list A -> Prop)
         (P_nil : P [])
         (P_single : forall x, P [x])
         (P_cons_snoc : forall x l x', P l -> P (x :: l ++ [x'])),
  forall l, P l.
Proof.
  intros. remember (length l) as n. symmetry in Heqn. revert dependent l.
  induction n using nat_ind2; intros.
  - apply length_zero_iff_nil in Heqn. subst l. apply P_nil.
  - destruct l; [discriminate|]. simpl in Heqn. inversion Heqn; subst.
    apply length_zero_iff_nil in H0. subst l. apply P_single.
  - destruct l; [discriminate|]. simpl in Heqn.
    inversion Heqn; subst. pose proof (rev_involutive l) as Hinv.
    destruct (rev l). destruct l; discriminate. simpl in Hinv. subst l.
    rewrite app_length in H0.
    rewrite PeanoNat.Nat.add_comm in H0. simpl in H0. inversion H0.
    apply P_cons_snoc. apply IHn. assumption.
Qed.

(*|
You should be able to conclude quite easily using this induction
principle.
|*)

Theorem palindrome3 : forall {X : Type} (l : list X),
    l = rev l -> pal l.
Admitted. (* .none *)

(*|
----

**A:** Yes, there is that induction principle in the standard library,
see `pair_induction
<https://coq.inria.fr/library/Coq.Numbers.Natural.Abstract.NBase.html#NBaseProp.pair_induction>`__.
|*)

author: vonavi

repo: coq-examples

save_path: github-repos/coq/vonavi-coq-examples


text:
Require Import String.
Import List.
Import ListNotations.

Require Import List_Properties.

Require Import Input_Properties.
Require Import Flood_Properties.
Require Import Flood_Box.

Require Import add_message_to_all_properties.
Require Import extract_port_buffer_message_properties.

Lemma resume_run_concats_trace:
  forall inp inp' buf buf' buf'' trace trace',
  execute_flood_rec inp buf = (trace, buf') ->
  execute_flood_rec inp' buf' = (trace', buf'') ->
  execute_flood_rec (inp ++ inp') buf = (trace ++ trace', buf'').
Proof.
  intros inp.
  induction inp;
  intros inp' buf buf' buf'' trace trace';
  intros H_first_run H_second_run.
  - simpl in * |- *.
    inversion H_first_run.
    subst. simpl.
    assumption.
  - destruct a;
    simpl.
    + destruct p.
      simpl in H_first_run.
      destruct (execute_flood_rec inp (add_message_to_all buf n s n0)) eqn:first_run_rem in H_first_run.
      inversion H_first_run. subst. clear H_first_run.
      rewrite IHinp with inp' (add_message_to_all buf n s n0) buf' buf'' f trace';
      try assumption.
      simpl. reflexivity.
    + simpl in H_first_run.
      destruct p.
      destruct (extract_port_buffer buf n0 n n0 s n1).
      destruct o;
      try (do 3 destruct p);
      destruct (execute_flood_rec inp i) eqn:first_run_rem in H_first_run;
      inversion H_first_run; subst; clear H_first_run;
      rewrite IHinp with inp' i buf' buf'' f trace';
      try assumption;
      simpl; reflexivity.
Qed.

Lemma concat_inp_concats_trace_split:
  forall inp inp' buf buf'' trace,
  execute_flood_rec (inp ++ inp') buf = (trace, buf'') ->
    exists buf' trace_head trace_tail,
      trace = trace_head ++ trace_tail /\
      execute_flood_rec inp buf = (trace_head, buf') /\
      execute_flood_rec inp' buf' = (trace_tail, buf'').
Proof.
  intros inp.
  induction inp;
  intros inp' buf buf'' trace;
  intros H_exec.
  - simpl in H_exec.
    exists buf, [], trace.
    repeat split. (* splits /\ and also fixes goal 1 and 2 *)
    assumption.
  - simpl in H_exec.
    destruct a.
    + destruct p.
      destruct (execute_flood_rec (inp ++ inp') (add_message_to_all buf n s n0)) eqn:rem.
      inversion H_exec.
      subst. clear H_exec.
      assert (exists (buf' : In_transit_buffer) (trace_head trace_tail : Flood_Trace),
          f = trace_head ++ trace_tail /\
          execute_flood_rec inp (add_message_to_all buf n s n0) = (trace_head, buf') /\
          execute_flood_rec inp' buf' = (trace_tail, buf'')).
      * apply IHinp.
        assumption.
      * do 4 destruct H.
        destruct H0.
        exists x.
        exists (Flood_Input n (s, n0) :: Flood_Leak n (s, n0) :: x0).
        exists x1.
        repeat split.
        -- simpl.
           rewrite H.
           reflexivity.
        -- simpl.
           rewrite H0.
           reflexivity.
        -- assumption.
    + destruct p.
      destruct (extract_port_buffer buf n0 n n0 s n1) eqn:buf_rem in H_exec.
      destruct o.
      * do 3 destruct p.
        destruct (execute_flood_rec (inp ++ inp') i) eqn:rem.
        assert (exists (buf' : In_transit_buffer) (trace_head trace_tail : Flood_Trace),
                  f = trace_head ++ trace_tail /\
                  execute_flood_rec inp i = (trace_head, buf') /\
                  execute_flood_rec inp' buf' = (trace_tail, i0)).
        -- apply IHinp.
           assumption.
        -- do 4 destruct H.
           destruct H0.
           exists x.
           exists (Flood_Deliver n4 n3 (s0, n2) :: Flood_Output n4 n3 (s0, n2) :: x0).
           exists x1.
           repeat split.
           ++ simpl.
              rewrite H in H_exec.
              inversion H_exec.
              reflexivity.
           ++ simpl.
              rewrite buf_rem.
              rewrite H0.
              reflexivity.
           ++ inversion H_exec.
              subst.
              assumption.
      * destruct (execute_flood_rec (inp ++ inp') i) eqn:rem.
        assert (exists (buf' : In_transit_buffer) (trace_head trace_tail : Flood_Trace),
                  f = trace_head ++ trace_tail /\
                  execute_flood_rec inp i = (trace_head, buf') /\
                  execute_flood_rec inp' buf' = (trace_tail, i0)).
        -- apply IHinp.
           assumption.
        -- do 4 destruct H.
           destruct H0.
           exists x.
           exists (Flood_Deliver n n0 (s, n1) :: x0).
           exists x1.
           repeat split.
           ++ simpl.
              rewrite H in H_exec.
              inversion H_exec.
              reflexivity.
           ++ simpl.
              rewrite buf_rem.
              rewrite H0.
              reflexivity.
           ++ inversion H_exec.
              subst.
              assumption.
Qed.

Lemma input_in_trace_implies_send_in_inp:
  forall inp trace buf buf' t1 i m c,
  execute_flood_rec inp buf = (trace, buf') ->
  nth_error trace t1 = Some (Flood_Input i (m, c)) ->
  exists t1', nth_error inp t1' = Some (Send i (m, c)).
Proof.
  intros inp.
  induction inp;
  intros trace buf buf' t1 i m c;
  intros H_exec H_nth_input;
  unfold execute_flood in H_exec;
  simpl in H_exec.
  - inversion H_exec.
    subst.
    destruct t1;
    simpl in H_nth_input;
    discriminate.
  - destruct a.
    + destruct p.
      destruct (execute_flood_rec inp (add_message_to_all buf n s n0)) eqn:exec_tail.
      inversion H_exec.
      subst. clear H_exec.
      destruct t1;
      simpl in H_nth_input.
      * inversion H_nth_input.
        subst.
        exists 0.
        simpl.
        reflexivity.
      * destruct t1;
        simpl in H_nth_input.
        -- inversion H_nth_input.
        -- assert (exists t1', nth_error inp t1' = Some (Send i (m, c)))
             as H_send_in_tail
             by (eapply IHinp;
                 eassumption).
           destruct H_send_in_tail as [t1' H_send_in_tail].
           exists (S t1').
           simpl.
           assumption.
    + destruct p.
      destruct (extract_port_buffer buf n0 n n0 s n1).  (* This has to be shortable *)
      destruct o.
      * do 3 destruct p.
        destruct (execute_flood_rec inp i0) eqn:exec_tail.
        inversion H_exec.
        subst. clear H_exec.
        destruct t1;
        simpl in H_nth_input.
        -- inversion H_nth_input.
        -- destruct t1;
           simpl in H_nth_input.
           ++ inversion H_nth_input.
           ++ assert (exists t1', nth_error inp t1' = Some (Send i (m, c)))
                as H_send_in_tail
                by (eapply IHinp;
                    eassumption).
              destruct H_send_in_tail as [t1' H_send_in_tail].
              exists (S t1').
              simpl.
              assumption.
      * destruct (execute_flood_rec inp i0) eqn:exec_tail.
        inversion H_exec.
        subst. clear H_exec.
        destruct t1;
        simpl in H_nth_input.
        -- inversion H_nth_input.
        -- assert (exists t1', nth_error inp t1' = Some (Send i (m, c)))
             as H_send_in_tail
             by (eapply IHinp;
                 eassumption).
           destruct H_send_in_tail as [t1' H_send_in_tail].
           exists (S t1').
           simpl.
           assumption.
Qed.

Lemma input_in_trace_implies_late_send_in_inp:
  forall inp trace buf buf' t1 i m c,
  execute_flood_rec inp buf = (trace, buf') ->
  nth_error trace t1 = Some (Flood_Input i (m, c)) ->
  exists t1', nth_error inp t1' = Some (Send i (m, c))
    /\ no_late_specific_send inp t1' i m c.
Proof.
  intros inp trace buf buf' t1 i m c.
  intros H_exec H_nth_input.
  assert (exists t1', nth_error inp t1' = Some (Send i (m, c)))
    as H_send_in_inp
    by (eapply input_in_trace_implies_send_in_inp;
        eassumption).
  destruct H_send_in_inp as [t1' H_send_in_inp].
  assert ((exists t, nth_error inp t = Some (Send i (m, c))
            /\ no_late_specific_send inp t i m c)
            \/ (forall t, nth_error inp t <> Some (Send i (m, c))))
    as H_send_late_or_not
    by (apply send_late_or_not_in_inp).
  destruct H_send_late_or_not as [H_send_late | H_no_send].
  - assumption.
  - specialize (H_no_send t1').
    contradiction.
Qed.

Lemma execute_flood_aux_rec_deliver_no_input_trace:
  forall i j m c trace buf buf' i' m' c',
  execute_flood_rec [Deliver i j (m, c)] buf = (trace, buf') ->
  ~ In (Flood_Input i' (m', c')) trace.
Proof.
  intros i j m c trace buf buf' i' m' c'.
  unfold not.
  intros H_exec H_in.
  simpl in H_exec.
  destruct (extract_port_buffer buf j i j m c).
  destruct o.
  - do 3 destruct p.
    inversion H_exec.
    subst. clear H_exec.
    inversion H_in.
    + discriminate.
    + inversion H.
      * discriminate.
      * inversion H0.
  - inversion H_exec.
    subst. clear H_exec.
    inversion H_in.
    + discriminate.
    + inversion H.
Qed.

Lemma send_in_inp_head_implies_send_in_trace_head:
  forall inp action t t' i m c trace_head trace_tail buf' buf'',
  nth_error inp t = Some (Send i (m, c)) ->
  no_late_specific_send (inp ++ [action]) t i m c ->
  execute_flood_rec [action] buf' = (trace_tail, buf'') ->
  nth_error (trace_head ++ trace_tail) t' = Some (Flood_Input i (m, c)) ->
  nth_error trace_head t' = Some (Flood_Input i (m, c)).
Proof.
  intros inp action t t' i m c trace_head trace_tail buf' buf''.
  intros H_inp_send H_inp_no_late_send H_exec_action H_trace_input.
  apply nth_error_concat_not_in_tail_implies_head with trace_tail.
  - assumption.
  - unfold not.
    intros H_in.
    destruct action.
    + simpl in H_exec_action.
      destruct p.
      inversion H_exec_action.
      subst. clear H_exec_action.
      inversion H_in.
      * inversion H.
        subst. clear H.
        unfold no_late_specific_send in H_inp_no_late_send.
        specialize (H_inp_no_late_send (Datatypes.length inp) i m c).
        apply H_inp_no_late_send.
        -- apply nth_error_Some.
           unfold not.
           intros H_is_none.
           rewrite H_is_none in H_inp_send.
           discriminate.
        -- rewrite nth_error_app2.
           ++ rewrite PeanoNat.Nat.sub_diag.
              simpl.
              reflexivity.
           ++ apply PeanoNat.Nat.le_refl.
        -- reflexivity.
      * inversion H;
        inversion H0.
    + simpl in H_exec_action.
      destruct p.
      destruct (extract_port_buffer buf' n0 n n0 s n1).
      destruct o.
      * do 3 destruct p.
        inversion H_exec_action.
        subst. clear H_exec_action.
        inversion H_in;
        inversion H;
        inversion H0.
      * inversion H_exec_action.
        subst. clear H_exec_action.
        inversion H_in;
        inversion H.
Qed.

Lemma length_of_flood_init_is_param:
  forall n,
  Datatypes.length (Flood_Box_init n) = n.
Proof.
  intros n.
  induction n;
  simpl.
  - reflexivity.
  - rewrite IHn.
    reflexivity.
Qed.

Lemma execute_inp_preserves_buffer_length:
  forall inp buf buf' trace,
  execute_flood_rec inp buf = (trace, buf') ->
  Datatypes.length buf = Datatypes.length buf'.
Proof.
  intros inp.
  induction inp;
  intros buf buf' trace;
  intros H_exec;
  simpl in H_exec.
  - inversion H_exec.
    reflexivity.
  - destruct a.
    + destruct p.
      destruct (execute_flood_rec inp (add_message_to_all buf n s n0)) eqn:exec.
      inversion H_exec.
      subst. clear H_exec.
      rewrite <- IHinp with (add_message_to_all buf n s n0) buf' f.
      * apply add_message_to_all_preserves_length.
      * assumption.
    + destruct p.
      destruct (extract_port_buffer buf n0 n n0 s n1) eqn:extract.
      destruct o;
      try do 3 destruct p;
      destruct (execute_flood_rec inp i) eqn:exec;
      inversion H_exec;
      subst; clear H_exec;
      rewrite <- IHinp with i buf' f;
      try (eapply extract_port_buffer_preserves_length;
           eassumption);
      assumption.
Qed.

author: Crowton

repo: FloodingNetworkSafeAndLive