Module MemCsharpminorproof

Require
  OnMem
  MemCsharpminor.

Import
  Utf8
  Coqlib
  AST
  Maps
  Globalenvs
  Values
  Integers
  Floats
  Memory
  Csharpminorannot

  Util
  AssocList
  ListAdom
  ToString
  AdomLib
  AlarmMon
  AbMachineEnv
  Cells
  Sets
  PExpr
  AbMemSignatureCsharpminor
  PointsTo
  OnMem
  MemCsharpminor.

Set Implicit Arguments.

Section num.

  Context
    {num num_iter: Type}
    `{numToString: ToString num}
    `{numIterToString: ToString num_iter}
    (NumDom: ab_machine_env (var:=cell) num num_iter).

  Variable ge : genv.
  Variable max_concretize : N.

  Existing Instances t_leb_correct t_join_correct widen_mem_correct.

  Local Instance t_gamma : gamma_op (@t num) concrete_state := t_gamma NumDom ge.
  Local Instance iter_t_gamma : gamma_op (@iter_t num_iter) concrete_state := iter_t_gamma NumDom ge.
  Local Instance mem_cshm_dom : mem_dom _ _ _ := mem_cshm_dom NumDom ge max_concretize.

  Lemma read_cell_upd t e σ m x v c:
    c ≠ ACtemp (plength σ) x →
    read_cell ge ((PTree.set x v t, e) :: σ, m) c =
    read_cell ge ((t, e) :: σ, m) c.

  Lemma validate_volatile_ptr_in sz ptr nes b :
    ∀ stk m,
      sizes_gamma ge stk sz m →
      validate_volatile_ptr ge sz ptr nes b = true →
      ∀ blk,
        BlockSet.mem blk ptr →
        ∃ g b, blk = ABglobal b ∧ Genv.find_symbol ge g = Some b ∧ Senv.block_is_volatile ge b.

  Lemma forget_all_correct
        {A V: Type} (P: A → (cell → V) → Prop)
        (P_ext: ∀ ρ ρ', (∀ x, ρ(x) = ρ'(x)) → ∀ m, ρ ∈ P m → ρ' ∈ P m)
        (F: A → cell → A)
        (PF: ∀ m ρ ρ' x, ρ ∈ P m → (∀ y, y ≠ x → ρ'(y) = ρ(y)) → ρ' ∈ P (F m x))
        l :
    ∀ m : A,
    ∀ ρ ρ' : cell → V,
      ρ ∈ P m →
      (∀ c, ρ c = ρ' c ∨ In c l) →
      ρ' ∈ P (fold_left F l m).

  Opaque ACTreeDom.set.
  Lemma ct_forget_all_get {A} l : ∀ m c,
    ACTreeDom.get c (@ct_forget_all A l m) =
    if in_dec eq_dec c l
    then All
    else ACTreeDom.get c m.

  Lemma pt_forget_all_correct stk l :
    ∀ m : points_to,
    ∀ ρ ρ' : cell → val,
      ρ ∈ points_to_gamma ge stk m →
      (∀ c, ρ c = ρ' c ∨ In c l) →
      ρ' ∈ points_to_gamma ge stk (ct_forget_all l m).

  Definition loose_upd_spec {B} (f: cell → B) (x: cell) (v: B) (f': cell → B) : Prop :=
    f'(x) = v ∧ ∀ y, y ∈ cells_disjoint(x) → f'(y) = f(y).

  Lemma nm_upd_correct nm c e n (ρ ρ': cell → mach_num) :
    ρ ∈ γ(nm) →
    n ∈ eval_mexpr ρ e →
    ρ' ∈ loose_upd_spec ρ c n →
    ρ' ∈ γ (nm_upd NumDom nm c e).

  Lemma nm_upd_not_bot nm c e n (ρ: cell → mach_num) :
    ρ ∈ γ(nm) →
    n ∈ eval_mexpr ρ e →
    nm_upd NumDom nm c e ≠ Bot.

  Lemma tp_upd_correct (val:Type) (Γ: gamma_op type val)
        (HJ: join_op_correct type (type+⊤) val) tp ρ cells ty c v :
    v ∈ γ(ty) →
    In c cells →
    ρ ∈ γ tp →
    loose_upd_spec ρ c v ⊆ γ (tp_upd_cells tp cells ty).

  Lemma cell_in_bounds_range_perm κ (ab: @t num) c:
    am_get (cell_in_bounds ge κ ab c) = Some tt →
    ∀ m σ b,
      m ∈ sizes_gamma ge σ (ab_sz ab) →
      block_of_ablock ge σ (ablock_of_cell c) = Some b →
      Mem.range_perm m b (fst (range_of_cell c)) (fst (range_of_cell c) + size_chunk (proj1_sig κ)) Cur Writable.
  Arguments cell_in_bounds_range_perm [κ] [ab] [c] _ [m] [σ] [b] _ _ _ _.
  Opaque cell_in_bounds.

  Lemma nassume_correct b nm F el :
    ∀ ρ,
      ρ ∈ γ(nm) →
      ∀ e, In e el → eval_mexpr ρ (F e) (of_bool b) →
      ρ ∈ γ (nassume NumDom b nm F el).

  Lemma env_ok (ε: lvarset) (e: env) :
    (∀ x, PSet.mem x ε = dom x e) →
    ∀ i, is_local ε i = true ↔ e ! i ≠ None.

  Remark bind_parameters_zip formals : ∀ args te,
    bind_parameters formals args te =
    fold_left2 (λ acc id v, do te <- acc; ret (PTree.set id v te))
               (λ _ _ , None) (λ _ _, None)
               formals args (Some te).

  Lemma set_local_sizes_get μ vars sz b :
    list_norepet (map fst vars) →
    ABTreeDom.get b (set_local_sizes μ vars sz) =
    match b with
    | ABlocal μ' x => if peq μ' μ
                      then match assoc x vars with
                           | Some hi => Just (hi, (Freeable, false))
                           | None => ABTreeDom.get b sz
                           end
                      else ABTreeDom.get b sz
    | _ => ABTreeDom.get b sz
    end.

  Lemma clear_local_sizes_get μ ε b sz :
    ABTreeDom.get b (clear_local_sizes μ ε sz) =
    match b with
    | ABlocal μ' x => if peq μ μ' && PSet.mem x ε then All else ABTreeDom.get b sz
    | _ => ABTreeDom.get b sz
    end.

  Lemma read_perm_non_volatile {V} (gv: globvar V) :
    perm_order (Genv.perm_globvar gv) Readable →
    gvar_volatile gv = false.

  Arguments ab_sz _ _/.
  Arguments ab_num _ _/.
  Arguments ab_tp _ _/.

  Lemma ab_alloc_global_ok:
    ∀ prog m, ge = Genv.globalenv prog ->
              Genv.init_mem prog = Some m ->
    ∀ b gv ab ab' id log,
      Genv.find_var_info ge b = Some gv ->
      Genv.invert_symbol ge b = Some id ->
      ab_alloc_global NumDom ge (Genv.perm_globvar gv) (gvar_volatile gv) b (gvar_init gv) (NotBot ab) = (ab', (nil, log)) ->
    m ∈ sizes_gamma ge nil (ab_sz ab) ->
    ab_stk ab = Just nil ->
    mem_as_fun ge (nil, m) ∈ tnum_gamma _ ge nil (ab_nm ab) ->
    match ab' with
      | Bot => False
      | NotBot ab' =>
        m ∈ sizes_gamma ge nil (ab_sz ab') /\
        ab_stk ab' = Just nil /\
        mem_as_fun ge (nil, m) ∈ tnum_gamma _ ge nil (ab_nm ab')
    end.

  Lemma ab_alloc_globals_ok:
    ∀ prog m, ge = Genv.globalenv prog ->
              Genv.init_mem prog = Some m ->
      list_norepet (map fst prog.(prog_defs)) ->
    ∀ b ab log,
      ab_alloc_globals NumDom ge prog.(prog_defs) = ((b, ab), (nil, log)) ->
      b = plength prog.(prog_defs) /\
    match ab with
      | Bot => False
      | NotBot ab =>
        m ∈ sizes_gamma ge nil (ab_sz ab) /\
        ab_stk ab = Just nil /\
        mem_as_fun ge (nil, m) ∈ tnum_gamma _ ge nil (ab_nm ab)
    end.

  Lemma check_volatile_sound {tgt κ ab} :
    ∀ μ log, check_volatile NumDom ge max_concretize tgt κ ab = (μ, (nil, log)) →
         match ab_stk ab with Just ( _ :: σ ) => μ = plength σ | _ => False end ∧
         match tgt with
         | inl (g, ofs) =>
           ∃ b, Genv.find_symbol ge g = Some b ∧
           ∃ hi perm, ABTreeDom.get (ABglobal b) (ab_sz ab) = Just (hi, (perm, true))
         | inr addr =>
           ∃ tn ty ne, am_get (ab_eval_expr NumDom ge max_concretize ab addr) = Some (NotBot (tn, Just ty, ne)) ∧
           ∃ ptr,
             ty = TyPtr (Just ptr) ∧
              validate_volatile_ptr ge (ab_sz ab) ptr ne true
         end.

  Lemma only_global_pointer_iff aptr :
    only_global_pointer ge aptr →
    ∃ ptr, aptr = Just ptr ∧
           ∀ p, BlockSet.mem p ptr → ∃ b, p = ABglobal b ∧ ∃ g, Genv.invert_symbol ge b = Some g ∧ Senv.public_symbol ge g.

  Definition alloc_variables' e m v :=
    List.fold_left (λ e_m id_sz,
                    let '(e, m) := e_m in
                    let '(id, sz) := id_sz in
                    let '(m₁, b₁) := Mem.alloc m 0 sz in
                    (PTree.set id (b₁, sz) e, m₁)) v (e, m).

  Lemma alloc_variables_alt v:
    ∀ e m e' m',
      alloc_variables e m v e' m' ↔ alloc_variables' e m v = (e', m').

  Definition alloc_var := alloc_variables' empty_env.
  Lemma alloc_var_alt m v e' m' :
    alloc_variables empty_env m v e' m' ↔ alloc_var m v = (e', m').

  Lemma alloc_var_snoc m v id sz :
    alloc_var m (v ++ (id, sz) :: nil)%list =
    let '(e, m') := alloc_var m v in
    let '(m₁, b₁) := Mem.alloc m' 0 sz in
    (PTree.set id (b₁, sz) e, m₁).

  Lemma alloc_var_guts m v:
    ∀ e' m',
    alloc_var m v = (e', m') →
    ∀ b,
      Mem.valid_block m b →
      Mem.valid_block m' b ∧
      (Mem.mem_contents m') !! b = (Mem.mem_contents m) !! b ∧
      (Mem.mem_access m') !! b = (Mem.mem_access m) !! b.

  Corollary alloc_var_load m v:
    ∀ e' m',
    alloc_var m v = (e', m') →
    ∀ b,
      Mem.valid_block m b →
      ∀ κ o,
        Mem.load κ m' b o = Mem.load κ m b o.

  Lemma alloc_variables_dom e m v e' m' :
    alloc_variables e m v e' m' →
    ∀ x, dom x e' = dom x e || in_dec peq x (List.map fst v).

  Lemma in_elements_set {A} e x y (v: A):
    In x (PTree.elements (PTree.set y v e)) →
    x = (y, v) ∨ In x (PTree.elements e) ∧ fst x ≠ y.

  Lemma alloc_variables_perm_mono m e v e' m':
    alloc_variables e m v e' m' →
    ∀ b o p,
      Mem.perm m b o Cur p → Mem.perm m' b o Cur p.

  Lemma alloc_variables_perm' e m v e' m':
    alloc_variables e m v e' m' →
  ∀ b hi, In (b, 0, hi) (blocks_of_env e') →
          In (b, 0, hi) (blocks_of_env e) ∨ Mem.range_perm m' b 0 hi Cur Freeable.

  Corollary alloc_variables_perm m v e m':
    alloc_variables empty_env m v e m' →
    ∀ b hi, In (b, 0, hi) (blocks_of_env e) →
            Mem.range_perm m' b 0 hi Cur Freeable.

  Lemma alloc_variables_env' e m v e' m':
    alloc_variables e m v e' m' →
    list_norepet (List.map fst v) →
    ∀ x y, PTree.get x e' = Some y →
           PTree.get x e = Some y ∨ assoc x v = Some (snd y).

  Corollary alloc_variables_env m v e m':
    alloc_variables empty_env m v e m' →
    list_norepet (List.map fst v) →
    ∀ x y, PTree.get x e = Some y →
           assoc x v = Some (snd y).

  Lemma alloc_variables_load' e m v :
    ∀ e' m',
      alloc_variables e m v e' m' →
      ∀ x y,
        e' ! x = Some y →
        e ! x = Some y ∨ Mem.valid_block m' (fst y) ∧ ∀ o, ZMap.get o (Mem.mem_contents m') !! (fst y) = Undef.

  Corollary alloc_variables_load m v e m':
    alloc_variables empty_env m v e m' →
    ∀ x y, e ! x = Some y →
           Mem.valid_block m' (fst y) ∧ ∀ o, ZMap.get o (Mem.mem_contents m') !! (fst y) = Undef.

  Lemma alloc_var_inj m v :
    ∀ e' m', alloc_var m v = (e', m') →
             (Mem.valid_block m ⊆ Mem.valid_block m') ∧
             (∀ x y, e' ! x = Some y → Mem.valid_block m' (fst y) ∧ ¬ Mem.valid_block m (fst y)) ∧
             injective_map (λ x, fmap fst (e' ! x)).

  Lemma alloc_variables_build vars m m' :
    ∀e',
      alloc_variables empty_env m vars e' m' →
      ∀ x : PSet.elt,
        PSet.mem x (PSetOp.build (rev_map fst vars)) = dom x e'.

  Remark create_undef_temps_undef l x :
    extend (λ x, (create_undef_temps l) ! x) x = Vundef.

  Lemma push_frame_invariant vars :
    ∀ σ m tmp e m',
      alloc_variables empty_env m vars e m' →
      invariant ge (σ, m) →
      invariant ge ((tmp, e) :: σ, m').

  Lemma push_frame_sizes σ sz vars m t' e' m' :
    invariant ge ((t', e') :: σ, m') →
    list_norepet (map fst vars) →
    alloc_variables empty_env m vars e' m' →
    m ∈ sizes_gamma ge σ sz →
    m' ∈ sizes_gamma ge ((t', e') :: σ) (set_local_sizes (plength σ) vars sz).

  Lemma push_frame_pt σ tmp e' ty :
    type_gamma (ptset_gamma ge σ) ty ⊆ type_gamma (ptset_gamma ge ((tmp, e') :: σ)) ty.

  Section ARGS_MATCH.
    Local Set Elimination Schemes.
    Variables (f: ident) (en : env) (tmp: temp_env) (σ: list (temp_env * env)) (m: mem) (ρn: cell → mach_num).
    Inductive args_match : list expr → list val → list (type+⊤ * list (mexpr cell)) → Prop :=
    | AMnil : args_match nil nil nil
    | AMcons eargs vargs aargs e v ty ln me n :
        v ≠ Vundef →
        v ∈ eval_expr ge en tmp m (expr_erase e) →
        v ∈ toplift_gamma (type_gamma (ptset_gamma ge ((tmp, en) :: σ))) ty →
        In me ln →
        n ∈ N.ncompat v → n ∈ eval_mexpr ρn me →
        (∀ x y, ACtemp x y ∈ me_free_var me → (x < Pos.succ (plength σ))%positive) →
        args_match eargs vargs aargs →
        args_match (e :: eargs) (v :: vargs) ((ty, ln) :: aargs)
    .

    Lemma am_a_cons_inv eargs vargs a aargs :
      args_match eargs vargs (a :: aargs) →
      ∃ e eargs' v vargs' ty ln me n,
        eargs = e :: eargs' ∧
        vargs = v :: vargs' ∧
        a = (ty, ln) ∧
        v ≠ Vundef ∧
        v ∈ eval_expr ge en tmp m (expr_erase e) ∧
        v ∈ toplift_gamma (type_gamma (ptset_gamma ge ((tmp, en) :: σ))) ty ∧
        In me ln ∧
        n ∈ (N.ncompat v ∩ eval_mexpr ρn me) ∧
        (∀ x y, ACtemp x y ∈ me_free_var me → (x < Pos.succ (plength σ))%positive) ∧
        args_match eargs' vargs' aargs.
  End ARGS_MATCH.


  Lemma load_undef {m b} :
    (∀ o, ZMap.get o (Mem.mem_contents m) !! b = Undef) →
    ∀ κ o, extend (Mem.load κ m b) o = Vundef.


  Lemma ab_bind_parameters_sound e t σ m vars e' m' :
    invariant ge ((t, e) :: σ, m) →
    alloc_variables empty_env m vars e' m' →
    ∀ params eargs aargs vargs ρn,
    args_match e t σ m ρn eargs vargs aargs →
    ∀ tmp tmp',
    bind_parameters params vargs tmp = Some tmp' →
    ∀ ab ab',
    am_get (ab_bind_parameters NumDom (Pos.succ (plength σ)) params aargs (ret (NotBot ab))) = Some ab' →
    mem_as_fun ge ((tmp, e') :: (t, e) :: σ, m) ∈ points_to_gamma ge ((tmp, e') :: (t, e) :: σ) (ab_tp ab) →
    ρn ∈ (compat (mem_as_fun ge ((tmp, e') :: (t, e) :: σ, m)) ∩ γ(ab_num ab)) →
    ∃ q,
      ab' = NotBot q ∧
      ab_stk q = ab_stk ab ∧
      ab_sz q = ab_sz ab ∧
      mem_as_fun ge ((tmp', e') :: (t, e) :: σ, m') ∈ points_to_gamma ge ((tmp', e') :: (t, e) :: σ) (ab_tp q) ∧
      ∃ ρn', ρn' ∈ (compat (mem_as_fun ge ((tmp', e') :: (t, e) :: σ, m')) ∩ γ (ab_num q)).

  Definition valid_block (stk: list (temp_env * env)) b : Prop :=
     (∃ s, Genv.invert_symbol ge b = Some s)
   ∨ (∃ t e x sz, In (t, e) stk ∧ e ! x = Some (b, sz)).

  Lemma valid_block_tmp stk stk' :
    stacks_tmp stk stk' →
    valid_block stk' ⊆ valid_block stk.

  Lemma pop_local_pt_get μ pt c :
    ACTree.get c (pop_local_pt μ pt) = do ty <- ACTree.get c pt;
    if if is_local_cell μ c
       then false
       else match ty with
            | (TyPtr (Just bs) | TyZPtr (Just bs)) =>
              negb (BSO.existsb (is_local_block μ) bs)
            | TyPtr All | TyZPtr All
            | TyFloat | TySingle | TyLong | TyInt | TyZero | TyIntPtr => true
            end
    then Some ty
    else None.

  Lemma pop_frame_pt τ₀ ε₀ σ m m' (tp: points_to) c:
    (∀ b, b ∈ valid_block σ →
          (∀ κ o, Mem.load κ m b o = Mem.load κ m' b o)
    ) →
    mem_as_fun ge ((τ₀, ε₀) :: σ, m) c ∈
               toplift_gamma (type_gamma (ptset_gamma ge ((τ₀, ε₀) :: σ))) (ACTreeDom.get c tp) →
    mem_as_fun ge (σ, m') c ∈
               toplift_gamma (type_gamma (ptset_gamma ge σ))
               (ACTreeDom.get c (pop_local_pt (plength σ) tp)).

  Lemma pop_frame_compat τ₀ ε₀ σ m m' :
    (∀ b, b ∈ valid_block σ →
          (∀ κ o, Mem.load κ m b o = Mem.load κ m' b o)
    ) →
    compat (mem_as_fun ge ((τ₀, ε₀) :: σ, m)) ⊆
    compat (mem_as_fun ge (σ, m')).

  Lemma pop_frame_invariant τ₀ ε₀ σ m m':
    invariant ge ((τ₀, ε₀) :: σ, m) →
    (∀ b, b ∈ valid_block σ →
          (∀ lo hi p, Mem.range_perm m b lo hi Cur p → Mem.range_perm m' b lo hi Cur p) ∧
          (b ∈ Mem.valid_block m → b ∈ Mem.valid_block m')
    ) →
    Mem.mem_contents m = Mem.mem_contents m' →
    invariant ge (σ, m').

  Lemma pop_frame_sizes τ₀ (ε₀: env) σ m m' (sz: sizes) ε':
    invariant ge ((τ₀, ε₀) :: σ, m) →
    (∀ b, b ∈ valid_block σ →
          (∀ lo hi p, Mem.range_perm m b lo hi Cur p → Mem.range_perm m' b lo hi Cur p)
    ) →
    m ∈ sizes_gamma ge ((τ₀, ε₀) :: σ) sz →
    m' ∈ sizes_gamma ge σ (clear_local_sizes (plength σ) ε' sz).

  Lemma free_list_ex tmp env stk m :
    invariant ge ((tmp, env) :: stk, m) →
    ∃ m', Mem.free_list m (blocks_of_env env) = Some m' ∧
          ∀ b, valid_block stk b →
               (∀ κ ofs, Mem.load κ m b ofs = Mem.load κ m' b ofs) ∧
               (∀ lo hi p, Mem.range_perm m b lo hi Cur p → Mem.range_perm m' b lo hi Cur p) ∧
               (b ∈ Mem.valid_block m → b ∈ Mem.valid_block m').

  Lemma nm_forget_all_weaken cells nm :
    γ(nm) ⊆ γ(nm_forget_all NumDom cells nm).

  Lemma pop_local_num_correct μ ε τ sz nm:
    γ nm ⊆ γ(pop_local_num NumDom μ ε τ sz (NotBot nm)).

  Lemma ab_alloc_global_ex:
    ∀ ab gv id m ab' log,
      ab_alloc_global NumDom ge (Genv.perm_globvar gv) (gvar_volatile gv) (Mem.nextblock m) gv.(gvar_init) ab = (ab', (nil, log)) ->
      ∃ m', Genv.alloc_global ge m (id, Gvar gv) = Some m'.

  Lemma ab_alloc_globals_ex:
    ∀ gl b ab log, ab_alloc_globals NumDom ge gl = ((b, ab), (nil, log)) ->
    ∃ m, Genv.alloc_globals ge Mem.empty gl = Some m /\
         Mem.nextblock m = b.

  Lemma init_mem_sound :
   ∀ (defs : list (ident * globdef fundef unit)) (a : option concrete_state),
   Init_Mem ge defs a → γ (AbMemSignatureCsharpminor.init_mem _ defs) a.

  Ltac ung :=
  repeat
  match goal with
  | G : γ _ _ |- _ => unfold γ in G
  | G : t_gamma ?a ?b |- _ =>
    let STK := fresh "STK" in
    let INV := fresh "INV" in
    let SZ := fresh "SZ" in
    let TPNM := fresh "TPNM" in
    destruct G as [STK INV SZ TPNM]
  | G : ?NOTALL ≠ All → _ |- _ =>
    let HH := fresh "HH" in
    assert (HH:NOTALL ≠ All) by discriminate;
    specialize (G HH);
    clear HH
  | G : stack_elt_gamma _ (_, _) |- _ =>
    destruct G
  | G : stack_elt_gamma _ ?a |- _ =>
    destruct a as (? & ?);
    destruct G
  | G : list_gamma _ _ (_ :: _) |- _ =>
    apply gamma_cons_inv in G;
    destruct G as (? & ? & ? & ? & G)
  | G : list_gamma _ (_ :: _) _ |- _ =>
    apply gamma_cons_inv_r in G;
    destruct G as (? & ? & ? & ? & G)
  | G : list_gamma _ nil _ |- _ =>
    apply gamma_nil_r in G
  | G : list_gamma _ _ nil |- _ =>
    apply gamma_nil_l in G
  | G : MemCsharpminor.tnum_gamma _ _ _ _ _ |- _ =>
    let TP := fresh "TP" in
    let ρn := fresh "ρn" in
    let CPT := fresh "CPT" in
    let NM := fresh "NM" in
    destruct G as (TP & ρn & CPT & NM)
  end.

  Lemma forget_temp_sound x t e stk m σ ab :
    ((t, e) :: stk, m) ∈ γ (Just σ, ab) →
    ∀ v, ((PTree.set x v t, e) :: stk, m) ∈ γ (forget_cell NumDom (Just σ, ab) (ACtemp (plength stk) x)).

  Lemma list_gamma_len {t B} {G: gamma_op t B} {x y} :
    list_gamma G x y → plength x = plength y.

  Lemma noerror_correct e ab :
    match am_get (noerror NumDom ge max_concretize e ab) with
    | Some tt => ∀ tmp env stk m, ((tmp, env) :: stk, m) ∈ γ(ab) →
                                    ∃ v, eval_expr ge env tmp m (expr_erase e) v ∧ v ≠ Vundef
    | None => True
    end.

  Existing Instance UnitGamma.
  Lemma noerror_sound: ∀ e ab, Noerror ge e (γ ab) ⊆ γ (noerror NumDom ge max_concretize e ab).

  Existing Instance boolean_partitionning.

  Lemma assume_sound :
   ∀ (e : expr) (ab : t) (a : option (bool * concrete_state)),
   Assume ge e (γ ab) a → γ (assume _ ge max_concretize e ab) a.

  Ltac ssubst :=
    repeat
    match goal with
    | H : ?a = ?b |- _ => first [subst a | subst b]
    end.

  Lemma ab_eval_expr_correct (ab: @t num) stk m (G: (stk, m) ∈ γ ab) e :
    match am_get (ab_eval_expr _ ge max_concretize ab e) with
    | Some res =>
        match res with
        | NotBot (tn, ty, ln) =>
          tnum_mono NumDom ge stk (ab_nm ab) tn ∧
          ∃ env tmp stk',
          stk = (tmp, env) :: stk' ∧
          ∀ ρ',
           ρ' ∈ compat (mem_as_fun ge (stk, m)) →
          ρ' ∈ γ(snd tn) →
          ∃ v, eval_expr ge env tmp m (expr_erase e) v ∧ v ≠ Vundef ∧
               v ∈ (toplift_gamma (type_gamma (ptset_gamma ge stk)) ty) ∧
               ∃ me n, In me ln ∧
                       N.ncompat v n ∧
                       (∀ x y : ident, me_free_var me (ACtemp x y) → (x < Pos.succ (plength stk'))%positive) ∧
                       eval_mexpr ρ' me n
          | Bot => False
       end
    | None => True
    end.

  Lemma ab_eval_exprlist_correct ε τ σ m :
    ∀ eargs (ab: @t num) (Hstk: ab_stk ab ≠ All) (G: ((τ, ε) :: σ, m) ∈ γ ab),
      match am_get (ab_eval_exprlist NumDom ge max_concretize ab eargs) with
      | None => True
      | Some Bot => False
      | Some (NotBot (ab', aargs)) =>
        ab_stk ab = ab_stk ab' ∧
        ab_sz ab = ab_sz ab' ∧
        tnum_mono NumDom ge ((τ,ε) :: σ) (ab_nm ab) (ab_nm ab')
        ∧
        ∀ ρn,
          ρn ∈ compat (mem_as_fun ge ((τ, ε) :: σ, m)) →
          ρn ∈ γ (ab_num ab) →
            ∃ vargs,
              eval_exprlist ge ε τ m (List.map expr_erase eargs) vargs ∧
              args_match ε τ σ m ρn eargs vargs aargs
      end.
  Global Opaque ab_eval_exprlist.

  Existing Instance stack_elt_gamma.
  Lemma assign_in_correct (μ: fname) (x: ident) (a: expr) (ab: t) stk m :
    (stk, m) ∈ γ(ab) →
    match am_get (assign_in NumDom ge max_concretize μ x a ab) with
    | Some ab' =>
        match ab' with
        | Bot => False
        | NotBot ab' =>
          ab_stk ab = ab_stk ab' ∧
          ab_sz ab = ab_sz ab' ∧
          ∃ env tmp stk',
          stk = (tmp, env) :: stk' ∧
          match get_stk_dep μ stk with
          | inleft H =>
            let 'exist ((pre, (tmp', env')), post) _ := H in
            ∃ v, eval_expr ge env tmp m (expr_erase a) v ∧ v ≠ Vundef ∧
                 (pre ++ (PTree.set x v tmp', env') :: post, m)%list ∈ γ(ab')
          | inright _ => True
          end
        end
    | None => True
    end.

  Lemma assign_sound :
   ∀ (x : ident) (e : expr) (ab : t) (a : option concrete_state),
   Assign ge x e (γ ab) a → γ (assign NumDom ge max_concretize x e ab) a.

  Lemma assign_any_sound :
   ∀ (x : ident) (ty: typ) (ab : t) (a : option concrete_state),
   AssignAny x ty (γ ab) a → γ (assign_any NumDom x ty ab) a.

  Lemma vload_sound : ∀ rettemp gofs κ args ab,
    VLoad ge rettemp gofs κ args (γ ab) ⊆ γ (vload NumDom ge max_concretize rettemp gofs κ args ab).

  Lemma store_sound α :
   ∀ (κ : memory_chunk) (dst src : expr) (ab : t)
   (a : option concrete_state),
   Store ge κ dst src (γ ab) a
   → γ (store NumDom ge max_concretize α κ dst src ab) a.

  Lemma vstore_sound : ∀ rettemp gofs κ args ab,
    VStore ge rettemp gofs κ args (γ ab) ⊆ γ (vstore NumDom ge max_concretize rettemp gofs κ args ab).

  Lemma push_frame_sound :
   ∀ (f : function) (args : list expr)
   (ab : t) (a : option concrete_state),
   PushFrame ge f args (γ ab) a → γ (push_frame NumDom ge max_concretize f args ab) a.

  Lemma pop_frame_sound :
   ∀ (ret : option expr) (rettemp : option ident) (ab : t)
   (a : option concrete_state),
   PopFrame ge ret rettemp (γ ab) a
   → γ (AbMemSignatureCsharpminor.pop_frame _ ret rettemp ab) a.

  Existing Instance ListIncl.
  Lemma deref_fun_sound :
   ∀ (e : expr) (ab : t) (a : option (ident * fundef)),
   DerefFun ge e (γ ab) a → γ (deref_fun NumDom ge max_concretize e ab) a.

  Instance widen_mem_correct:
    widen_op_correct (iter_t +⊥) (t +⊥) concrete_state.

  Lemma mem_cshm_dom_correct:
    mem_dom_spec _ ge mem_cshm_dom t_gamma (gamma_bot iter_t_gamma).

End num.