Module MemCsharpminor

Require ArithLib.
Require ListAdom.
Require Mconvert.
Require Pun.
Require AbMemSignatureCsharpminor.
Require DebugCshm DebugAbMachineEnv.

Import
  Utf8
  String
  Coqlib
  Maps
  Integers
  Floats
  Values
  Memory
  Globalenvs
  AST
  Cminor
  Csharpminor
  Util
  AssocList
  ToString
  Sets
  AdomLib
  AlarmMon
  ListAdom
  AbMemSignatureCsharpminor
  AbMachineEnv
  PExpr
  TypesDomain
  MemChunkTree
  Cells
  Pun
  NoError
  PointsTo
  Mconvert
  FastArith.

Open Scope string.

Set Implicit Arguments.
Unset Elimination Schemes.


Definition injective_map {A B} (m: A → option B) : Prop :=
  ∀ x x' a,
    m(x) = Some a → m(x') = Some a →
    x = x'.

Definition stacks_tmp (stk stk': list (temp_env * env)) : Prop :=
  map snd stk =
  map snd stk'.

Lemma stacks_tmp_in : ∀ stk stk',
  stacks_tmp stk stk' →
  ∀ t e,
    In (t, e) stk' →
    ∃ t', In (t', e) stk.

Lemma get_stk_tmp : ∀ stk stk',
  stacks_tmp stk stk' →
  ∀ f,
  option_map snd (get_stk f stk) =
  option_map snd (get_stk f stk').

Remark block_of_ablock_tmp ge : ∀ stk stk',
  stacks_tmp stk stk' →
  ∀ ab, block_of_ablock ge stk ab = block_of_ablock ge stk' ab.

Module N := Nconvert ACTree.
Module PT := N.PT.
Export PT.
Definition types : Type := ACTreeDom.t AbTy.t.

Definition lvarset : Type := PSet.t.
Definition tvarset : Type := PSet.t.
Definition stack : Type := list (lvarset * tvarset).

Instance fname_leb : leb_op fname := flat_leb_op Pos.eqb.
Instance fname_join : join_op fname (fname+⊤) := flat_join_op Pos.eqb.
Instance lvarset_leb : leb_op lvarset := flat_leb_op PSet.beq.
Instance lvarset_join : join_op lvarset (lvarset+⊤) := flat_join_op PSet.beq.

Instance types_leb : leb_op types :=
  ACTreeDom.leb_tree _ _.

Instance types_join : join_op types types :=
  ACTreeDom.join_tree _ _.

Definition types_widen : types -> types -> types := join.

Definition sizes : Type := ABTreeDom.t (Z * (permission * bool)).
Definition sizes_gamma ge stk : gamma_op sizes mem :=
  λ sz m,
  ∀ b hi perm vol b',
    ABTreeDom.get b sz = Just (hi, (perm, vol)) →
    block_of_ablock ge stk b = Some b' →
    Mem.range_perm m b' 0 hi Cur perm
 ∧ Bool.leb vol (Senv.block_is_volatile ge b').

Instance BoolEqDec : EqDec bool := eq_dec_of_beq _ Bool.eqb_true_iff.
Definition permission_beq (x y: permission) : bool :=
  match x, y with
  | Freeable, Freeable
  | Writable, Writable
  | Readable, Readable
  | Nonempty, Nonempty
    => true
  | _, _ => false
  end.

Lemma permission_beq_iff x y : permission_beq x y = true ↔ x = y.
Instance PermissionEqDec : EqDec permission := eq_dec_of_beq _ permission_beq_iff.

Instance PermissionToString : ToString permission :=
  λ perm,
  match perm with
  | Freeable => "Freeable"
  | Writable => "Writable"
  | Readable => "Readable"
  | Nonempty => "Nonempty"
  end%string.

Instance sizes_leb : leb_op sizes :=
  leb (leb_op:=ABTreeDom.leb_tree (flat_leb_op eq_dec) _).

Instance sizes_join : join_op sizes sizes := ABTreeDom.join_tree (flat_join_op eq_dec) _.

Definition sizes_widen : sizes -> sizes -> sizes := join.

Instance sizes_top_correct ge stk : top_op_correct sizes mem (G:=sizes_gamma ge stk).

Instance sizes_leb_correct ge stk : leb_op_correct sizes mem (G:=sizes_gamma ge stk).

Instance sizes_join_correct ge stk : join_op_correct sizes sizes mem
                            (GA:=sizes_gamma ge stk) (GB:=sizes_gamma ge stk).

Lemma ptset_gamma_tmp ge : ∀ stk stk',
  stacks_tmp stk stk' →
  ∀ bs, ptset_gamma ge stk bs ⊆ ptset_gamma ge stk' bs.

Lemma points_to_gamma_tmp ge : ∀ stk stk',
  stacks_tmp stk stk' →
  ∀ ptr, points_to_gamma ge stk ptr ⊆ points_to_gamma ge stk' ptr.

Lemma sizes_gamma_tmp ge stk stk' :
  stacks_tmp stk stk' →
  ∀ sz, sizes_gamma ge stk sz ⊆ sizes_gamma ge stk' sz.

Section num.

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

  Lemma gamma_num_ext :
   ∀ ρ ρ' : cell → mach_num,
   (∀ x : cell, ρ x = ρ' x) → ∀ m : num +⊥, γ m ρ → γ m ρ'.

  Definition compat := (λ ρ ρn, N.compat _ (λ x, x) ρ ρn).

  Variable ge : genv.
  Local Instance AblockToString : ToString ablock := AblockToString ge.
  Local Instance CellToString : ToString cell := CellToString ge.

  Record invariant (cs: concrete_state) : Prop :=
    { localFreeable :
        ∀ t e, In (t, e) (fst cs) →
          ∀ b hi, In (b, 0, hi) (blocks_of_env e) →
                  Mem.range_perm (snd cs) b 0 hi Cur Freeable
    ; localNotGlobal :
        ∀ t e, In (t, e) (fst cs) →
             ∀ x b y b' z,
               Genv.find_symbol ge x = Some b →
               e ! y = Some (b', z) →
               b ≠ b'
    ; localInj :
   injective_map (λ x_v,
                  do t_e <- get_stk (fst x_v) (fst cs);
                  fmap fst ((snd t_e) ! (snd x_v)))
   ; globalValid:
   ∀ x b, Genv.find_symbol ge x = Some b →
          b ∈ Mem.valid_block (snd cs)
   ; localValid:
       ∀ t e, In (t, e) (fst cs) →
                ∀ x b z,
               e ! x = Some (b, z) →
               b ∈ Mem.valid_block (snd cs)
   ; noIntFragment:
       ∀ ab b,
         block_of_ablock ge (fst cs) ab = Some b →
         ∀ o, match ZMap.get o (Mem.mem_contents (snd cs)) !! b with Fragment (Vint _) _ _ => False | _ => True end
   }.

  Lemma invariant_tmp : ∀ stk stk',
    stacks_tmp stk stk' →
    ∀ m, invariant (stk, m) → invariant (stk', m).

  Lemma invariant_block_of_ablock_inj stk m :
    (stk, m) ∈ invariant →
    ∀ ab₁ b₁ ab₂ b₂,
      block_of_ablock ge stk ab₁ = Some b₁ →
      block_of_ablock ge stk ab₂ = Some b₂ →
      ab₁ ≠ ab₂ →
      b₁ ≠ b₂.

  Lemma assign_const c i (nm : num) :
    ∀ ρ, ρ ∈ γ(nm) →
    match AbMachineEnv.assign c (me_const_i _ i) nm with
    | Bot => False
    | NotBot nm' => (upd ρ c (MNint i)) ∈ γ(nm')
    end.

  Definition tnum : Type := (types * num)%type.
  Definition tnum_iter : Type := (types * num_iter)%type.

  Instance tnum_gamma : gamma_op tnum (cell → val) :=
    λ τ_ν ρ,
    let '(τ, ν) := τ_ν in
    ρ ∈ γ(τ) ∧
    ∃ ρ',
      ρ' ∈ (compat ρ ∩ γ ν).

  Instance tnum_iter_gamma : gamma_op tnum_iter (cell → val) :=
    λ τ_ν ρ,
    let '(τ, ν) := τ_ν in
    ρ ∈ γ(τ) ∧
    ∃ ρ',
      ρ' ∈ (compat ρ ∩ γ ν).

  Instance tnum_leb_correct : leb_op_correct (types * num) (cell -> val).

  Instance tnum_top_correct : top_op_correct ((types * num)+⊥) (cell -> val).

  Instance tnum_join_correct : join_op_correct (types * num) ((types * num)+⊥) (cell -> val).

  Section REALIZATION.


    Definition is_int (tp: types) (c: cell) : bool :=
      ACTreeDom.get c tp ⊑ Just VI.

    Lemma is_int_intro (tp: types) (ρ: cell → val) (TP: ρ ∈ γ tp) (c: cell) (P: bool → Prop):
      (P false) →
      (ρ c ∈ γ VI → P true) →
      P (is_int tp c).
    Global Opaque is_int.

    Definition realize_u8_from_κ (κ: typed_memory_chunk) (ab: ablock) (base: Z) (shift: Z) (tp: types) (nm: num) : tnum+⊥ :=
      let uc : cell := cell_from ab (base + shift, exist _ Mint8unsigned I) in
      let c : cell := cell_from ab (base, κ) in
      do nm' <- assign uc (MEbinop Oand (MEbinop Oshru (MEvar MNTint c) (MEconst _ (MNint (Int.repr (8 * shift))))) (MEconst _ (MNint (Int.repr 255)))) nm;
      NotBot (ACTreeDom.set tp uc (Just VI), nm').

    Definition tnum_mono (x y: tnum) : Prop :=
      ∀ ρ, Pun.pun_u8 ρ →
           ρ ∈ γ x →
           ρ ∈ γ (fst y) ∧
           ∀ ρ',
             compat ρ ρ' →
             ρ' ∈ γ (snd x) → ρ' ∈ γ (snd y).

    Lemma tnum_m_stronger :
      ∀ x y, tnum_mono x y →
          Pun.pun_u8 ∩ γ (x) ⊆ γ (y).

    Lemma tnum_mono_refl x : tnum_mono x x.

    Lemma tnum_mono_trans y x z :
      tnum_mono x y → tnum_mono y z →
      tnum_mono x z.

    Definition tnum_mono' (x: tnum) (y': tnum+⊥) : Prop :=
      ∀ ρ, Pun.pun_u8 ρ →
           ρ ∈ γ x →
           match y' with
           | Bot => False
           | NotBot y =>
             ρ ∈ γ (fst y) ∧
             ∀ ρ',
               compat ρ ρ' →
               ρ' ∈ γ (snd x) → ρ' ∈ γ (snd y)
           end.

    Lemma realize_u8_from_κ_sound (κ: typed_memory_chunk) ab base shift (tp: types) (nm: num) :
      (Archi.big_endian = false) →
      (align_chunk (proj1_sig κ) | base) →
      0 <= shift < size_chunk (proj1_sig κ) ∧ size_chunk (proj1_sig κ) <= 4 →
      let c : cell := cell_from ab (base, κ) in
      is_int tp c →
      tnum_mono' (tp, nm) (realize_u8_from_κ κ ab base shift tp nm).

    Definition cell_mem_rect {T: Type} :
      T →
      (ablock → Z → typed_memory_chunk → T) →
      cell → T :=
      λ b r c,
      match c with
      | AClocal f x ofs κ => r (ABlocal f x) ofs κ
      | ACglobal g ofs κ => r (ABglobal g) ofs κ
      | ACtemp _ _ => b
      end.

    Definition cell_mem_rect_intro {T: Type} (P: cell → T → Prop) :
      ∀ b r,
        (∀ f r, P (ACtemp f r) b) →
        (∀ ab ofs κ, P (cell_from ab (ofs, κ)) (r ab ofs κ)) →
        ∀ c, P c (cell_mem_rect b r c) :=
      λ b r B R c,
      match c with
      | AClocal f x ofs κ => R (ABlocal f x) ofs κ
      | ACglobal g ofs κ => R (ABglobal g) ofs κ
      | ACtemp f r => B f r
      end.
    Global Opaque cell_mem_rect.

    Definition optimistic_realization_one (c: cell) (tn: tnum) : tnum+⊥ :=
      let '(tp, nm) := tn in
      match ACTreeDom.get c tp with
      | Just _ => NotBot tn
      | All =>
        cell_mem_rect
          (NotBot tn)
          (λ ab ofs κ,
           match κ with
           | exist Mint8unsigned _ =>
             let (base, shift) := Z.div_eucl ofs 4 in
             let base := 4 * base in
             let c32 := cell_from ab (base, exist _ Mint32 I) in
             if is_int tp c32
             then realize_u8_from_κ (exist _ Mint32 I) ab base shift tp nm
             else
               let (base, shift) := Z.div_eucl ofs 2 in
               let base := 2 * base in
               let c16u := cell_from ab (base, exist _ Mint16unsigned I) in
               if is_int tp c16u
               then realize_u8_from_κ (exist _ Mint16unsigned I) ab base shift tp nm
               else
               let c16s := cell_from ab (base, exist _ Mint16signed I) in
               if is_int tp c16s
               then realize_u8_from_κ (exist _ Mint16signed I) ab base shift tp nm
               else
               let c8s := cell_from ab (ofs, exist _ Mint8signed I) in
               if is_int tp c8s
               then realize_u8_from_κ (exist _ Mint8signed I) ab ofs 0 tp nm
               else NotBot tn
           | exist Mint32 _ =>
             if ArithLib.divide ofs F4 then
             let c := cell_from ab (ofs, κ) in
             let c8 shift := cell_from ab (ofs + shift, exist _ Mint8unsigned I) in
             if is_int tp (c8 0) then
             if is_int tp (c8 1) then
             if is_int tp (c8 2) then
             if is_int tp (c8 3) then
               do nm' <- assign c
                   (MEbinop Oadd (MEvar MNTint (c8 0))
                   (MEbinop Oadd (MEbinop Oshl (MEvar MNTint (c8 1)) (MEconst _ (MNint (Int.repr 8))))
                   (MEbinop Oadd (MEbinop Oshl (MEvar MNTint (c8 2)) (MEconst _ (MNint (Int.repr 16))))
                   (MEbinop Oshl (MEvar MNTint (c8 3)) (MEconst _ (MNint (Int.repr 24)))))))
                   nm;
               NotBot (ACTreeDom.set tp c (Just VI), nm')
             else NotBot tn
             else NotBot tn
             else NotBot tn
             else NotBot tn
             else NotBot tn
           | _ => NotBot tn
           end)
          c
      end.

    Lemma optimistic_realization_one_sound (c: cell) (tn: tnum) :
      tnum_mono' tn (optimistic_realization_one c tn).
    Global Opaque optimistic_realization_one.

    Definition optimistic_realization (cells: CellSet.t) (tn: tnum) : tnum+⊥ :=
      CellSet.fold (λ c tn, bind tn (optimistic_realization_one c)) cells (NotBot tn).

    Lemma optimistic_realization_sound cells tn:
      tnum_mono' tn (optimistic_realization cells tn).
    Global Opaque optimistic_realization.

  End REALIZATION.

  Variable max_concretize : N.

  Section CONVERT.

  Variable μ : fname.

  Variable ε : lvarset.

  Definition is_local (v: ident) : bool := PSet.mem v ε.

  Definition addr_of (v: ident) : BlockSet.t :=
    if is_local v
    then BSO.singleton (ABlocal μ v)
    else match Genv.find_symbol ge v with
         | Some b => BSO.singleton (ABglobal b)
         | None => BlockSet.empty
         end.

  Variable sz : sizes.
  Variable pt : points_to.

  Definition me_of_pe (nm: num) (pe: pexpr cell) : am_map_t (mexpr cell) :=
    match N.nconvert ge μ _ _ (λ x, x) _ _ NumDom sz nm pt pe with
    | inl me =>
      if AbMachineEnv.noerror me nm
      then Result me
      else Error (Some me)
                 ("me_of_pe(" ++ to_string pe ++ "): error")
    | inr (res, msg) => Error res
                    ("me_of_pe(" ++ to_string pe ++ "): conversion failed: " ++ msg)
    end.

  Definition check_align (nm: num) (sz: Z) (me: mexpr cell) : bool :=
    match is_one sz with
    | false =>
           is_bot (AbMachineEnv.assume
              (MEbinop (Ocmp Cne)
                 (MEbinop Omodu me (me_const_i _ (Int.repr sz)))
                 (me_const_i _ Int.zero))
              true nm)
    | e => e
    end.

  Definition deref_pexpr (nm: num) κ (lpe: list (pexpr cell)) : alarm_mon (CellSet.t+⊤) :=
    let al := align_chunk (proj1_sig κ) in
    am_fold
      (λ acc pe,
       do offs <-
          match pexpr_get_ty pe with
          | VP =>
            match me_of_pe nm pe with
            | Result me =>
              do _ <- am_assert (check_align nm al me)
                 ("bad align (" ++ to_string (proj1_sig κ) ++ "): " ++ to_string me);
              ret (concretize_int max_concretize me nm)
            | Errorc me e =>
              do _ <- alarm_am (e tt);
              ret match me with
                  | Some me => concretize_int max_concretize me nm
                  | None => NotBot All
                  end
            end
          | ty =>
            do _ <- alarm_am ("deref_pexpr: maybe not a pointer (" ++ to_string ty ++ ")");
            ret (NotBot All)
          end;
       ret match acc with
           | All => All
           | Just acc =>
             match pt_eval_pexpr ge μ pt pe with
             | All => All
             | Just ptr => fmap (CellSet.union acc) (set_product ptr κ offs)
             end
           end)
      lpe
      (Just CellSet.empty).

  Lemma deref_pexpr_inv nm κ lpe :
    match am_get (deref_pexpr nm κ lpe) with
    | Some cells =>
      let al := align_chunk (proj1_sig κ) in
    ∀ pe, In pe lpe →
          pexpr_get_ty pe = VP ∧
          ∃ me,
            me_of_pe nm pe = Result me ∧
            check_align nm al me = true ∧
            let ofs := concretize_int max_concretize me nm in
            match cells with All => True | Just cells =>
            ofs ≠ NotBot All ∧
            ∃ ptr, pt_eval_pexpr ge μ pt pe = Just ptr ∧
            ∀ b i,
              BlockSet.mem b ptr →
              i ∈ γ(ofs) →
              CellSet.mem (cell_from b (Int.unsigned i, κ)) cells
            end
    | None => True
    end.

  Definition constant_of_constant (c: Csharpminor.constant) : constant :=
    match c with
    | Csharpminor.Ointconst i => Ointconst i
    | Csharpminor.Olongconst i => Olongconst i
    | Csharpminor.Ofloatconst f => Ofloatconst f
    | Csharpminor.Osingleconst f => Osingleconst f
    end.

  Definition convert_err (e:expr) msg :=
    ("convert(" ++ to_string e ++ "): " ++ msg ++ new_line ++
     "Function: " ++ to_string μ ++ new_line ++
     "Locals: " ++ to_string ε ++ new_line ).
  Opaque convert_err.

  Definition convert_t A := tnum -> alarm_mon (tnum * A).
  Local Instance convert_monad : monad convert_t :=
    {
      ret A := λ a tn, ret (tn, a);
      bind A B := λ m f tn, do (tn', a) <- m tn; f a tn'
    }.

  Let get_tnum : convert_t tnum := λ tn, ret (tn, tn).
  Let lift {A} (m: alarm_mon A) : convert_t A :=
    λ tn, fmap (λ x, (tn, x)) m.

  Local Notation "'alarm' e" := ((λ tn, (((tn, tt), (λ _, e) :: nil))):(convert_t _)) (at level 100).

  Let convert_var (e: expr) (c: cell) : convert_t (list (pexpr cell)) :=
    λ tn,
    let '(tp, nm) := tn in
    match ACTreeDom.get c tp with
    | Just ty => ret (PEvar c ty :: nil) tn
    | All => (do _ <- alarm (convert_err e ("bad temp in " ++ to_string μ)); ret nil) tn
    end.

  Let realize (cells: CellSet.t) : convert_t (list cell) :=
    λ tn,
    match optimistic_realization cells tn with
    | Bot => ret nil tn
    | NotBot tn' => ret (CellSet.elements cells) tn'
    end.

  Fixpoint convert (e: expr) : convert_t (list (pexpr cell)) :=
    let err := convert_err e in
    match e with
    | Evar v => convert_var e (ACtemp μ v)
    | Eaddrof i =>
      if is_local i
      then ret (PElocal _ i :: nil)
      else match Genv.find_symbol ge i with
           | Some _ => ret (PEconst _ (Some (Oaddrsymbol i Int.zero)) VP :: nil)
           | None => do _ <- alarm (err "bad global variable");
                     ret nil
           end
    | Econst cst =>
      let cst := constant_of_constant cst in
      ret (PEconst _ (Some cst) (AbTy.eval_constant cst) :: nil)
    | Eunop op e1 =>
      do e1' <- convert e1;
      ret (rev_map (fun e => PEunop op e (AbTy.eval_unop op (pexpr_get_ty e))) e1')
    | Ebinop op e1 e2 =>
      do e1' <- convert e1;
      do e2' <- convert e2;
      ret (map2 (λ e1 e2,
                 PEbinop op e1 e2
                         (AbTy.eval_binop op (pexpr_get_ty e1) (pexpr_get_ty e2))
                ) e1' e2')

    | Eload κ e1 =>
      do e1' <- convert e1;
      do κ <-
        match κ return convert_t (option typed_memory_chunk) with
          | Many32 | Many64 =>
            do _ <- alarm (err "Many32 or Many64"); ret None
          | κ => ret (Some (exist _ κ I:typed_memory_chunk))
        end;
      do (tp, nm) <- get_tnum;
      do cells <- match κ with Some κ => lift (deref_pexpr nm κ e1') | None => ret All end;
      match cells with
      | All => do _ <- alarm (err "too many cells"); ret nil
      | Just cells =>
        do cells <- realize cells;
        λ tn,
        let '(tp, nm) := tn in
        lift (
      am_map' (λ c, match ACTreeDom.get c tp with
                    | All => Error None (err ("bad cell: " ++ to_string c))
                    | Just ty => Result (PEvar c ty)
                    end)
              cells
          )
             tn
      end
    end.

  Definition me_of_pe_list nm := am_map' (me_of_pe nm).

  Definition nconvert (e:expr) : convert_t (list (mexpr cell)) :=
    do lpe <- convert e;
    λ tn, lift (me_of_pe_list (snd tn) lpe) tn.

  Definition deref_expr_err (nm: num) (e: expr) (κ: typed_memory_chunk) (lpe: list (pexpr cell)) :=
    ("deref_expr(" ++ to_string e ++ ", " ++ to_string (proj1_sig κ) ++ ") " ++ to_string lpe )%string.
  Opaque deref_expr_err.

  Definition deref_expr κ (e: expr) : convert_t (list cell) :=
    do lpe <- convert e;
    λ tn,
      let '(tp, nm) := tn in
      lift (
      do cells <- deref_pexpr nm κ lpe;
      match cells with
      | All => do _ <- alarm_am (deref_expr_err nm e κ lpe);
                ret nil
      | Just cell_set => ret (CellSet.elements cell_set)
      end
      ) tn.

  Section CONVERT_CORRECT.
    Context (e: env) (tmp: temp_env) (m: mem).
    Context (stk: list (temp_env * env)).
    Context (Hstk: μ = plength stk).
    Let ρ := mem_as_fun ge ((tmp, e) :: stk, m).
    Local Instance pt_gamma : gamma_op points_to _ := points_to_gamma ge ((tmp, e) :: stk).
    Hypothesis E: ∀ i, is_local i = true ↔ e ! i ≠ None.
    Hypothesis INV : invariant ((tmp, e) :: stk, m).
    Hypothesis SZ: m ∈ sizes_gamma ge ((tmp, e) :: stk) sz.
    Hypothesis PT: ρ ∈ γ(pt).

    Lemma Tmp: ∀ i v, tmp ! i = Some v → ρ (ACtemp μ i) = v.
    Hint Resolve Tmp.

    Lemma me_of_pe_correct (nm: num) (ρn: cell → mach_num) (NM: ρn ∈ γ(nm)) pe :
      match me_of_pe nm pe with
      | Result me => N.nconvert ge μ _ _ (λ x, x) _ _ NumDom sz nm pt pe = inl me ∧ ¬ error_mexpr ρn me
      | Errorc _ _ => True
      end.

    Ltac with_me_of_pe q :=
      repeat match goal with
      | H : appcontext[ me_of_pe ?nm ?pe ] |- _ =>
        generalize (me_of_pe_correct pe);
        destruct (me_of_pe nm pe); q
      end.

    Lemma me_of_pe_list_noerror (nm: num) (ρn: cell → mach_num) (NM: ρn ∈ γ(nm)) lpe :
      match am_get (me_of_pe_list nm lpe) with
      | Some lme => (∀ me, In me lme → ¬ error_mexpr ρn me)
                  ∧ (∀ pe, In pe lpe → ∃ me, In me lme ∧
                     N.nconvert ge μ _ _ (λ x, x) _ _ NumDom sz nm pt pe = inl me)
      | None => True
      end.

    Lemma pexpr_get_ty_ok (pe: pexpr cell) v :
      eval_pexpr ge m ρ e pe v → v ≠ Vundef → v ∈ γ(pexpr_get_ty pe).

    Lemma check_align_correct (nm: num) (ρn: cell → mach_num) (NM: ρn ∈ γ(nm)) al me :
      al = 1 ∨ al = 2 ∨ al = 4 ∨ al = 8 →
      check_align nm al me = true →
      ∀ n, eval_mexpr ρn me (MNint n) →
           Int.unsigned n = al * Int.unsigned (Int.divu n (Int.repr al)).

    Ltac subs := repeat match goal with H : ?a = ?b |- _ => subst a || subst b end.

    Let Hpun : ρ ∈ pun_u8 := mem_as_fun_pun_u8 _ _ INV.(noIntFragment).

    Lemma convert_wf (q: expr):
      ∀ (tn: tnum) (TN: ρ ∈ γ tn),
      match am_get (convert q tn) with
      | Some (tn', lp) =>
        tnum_mono tn tn'
        ∧
        ∀ pe, In pe lp → N.nconvert_def_pre ge e ρ pe
      | None => True
      end.

    Lemma convert_free_def (q: expr) :
      ∀ (tn: tnum) (TN: ρ ∈ γ tn),
      match am_get (convert q tn) with
      | Some (tn', lp) =>
          ∀ pe, In pe lp ->
          ∀ x, pe_free_var pe x -> ρ x ≠ Vundef
      | None => True
      end.

    Remark align_chunk_4_cases (κ: memory_chunk) :
      align_chunk κ = 1 ∨ align_chunk κ = 2 ∨ align_chunk κ = 4 ∨ align_chunk κ = 8.

    Lemma convert_correct (q: expr) :
      ∀ (tn: tnum) (TN: ρ ∈ γ tn),
      match am_get (convert q tn) with
      | Some (tn', lp) =>
        ∀ v, eval_expr ge e tmp m q v →
             ∃ a, In a lp ∧ eval_pexpr ge m ρ e a v
      | None => True
      end.

    Lemma SZ' :
      ∀ (b : ABTree.elt) (hi : Z) (md : permission * bool)
        (b' : block),
        ABTreeDom.get b sz = Just (hi, md)
        → block_of_ablock ge ((tmp, e) :: stk) b = Some b'
        → Mem.range_perm m b' 0 hi Cur Nonempty.

    Lemma convert_noerror (q: expr) :
      ∀ (tn: tnum) (TN: ρ ∈ γ tn),
      match am_get (convert q tn) with
      | Some (tn', lp) => (∀ pe, In pe lp → ¬ error_pexpr ge m ρ e pe) → ¬ error_expr ge e tmp m q
      | None => True
      end.

    Lemma deref_expr_correct (tn: tnum) (TN: ρ ∈ γ tn) κ q :
      match am_get (deref_expr κ q tn) with
      | Some (tn', cells) =>
        tnum_mono tn tn' ∧
        ¬ error_expr ge e tmp m q ∧
        ∀ v, eval_expr ge e tmp m q v →
        ∃ ab b i, v = Vptr b i ∧
                  In (cell_from ab (Int.unsigned i, κ)) cells ∧
                  block_of_ablock ge ((tmp, e) :: stk) ab = Some b ∧
                  (align_chunk (proj1_sig κ) | Int.unsigned i)
      | None => True
      end.

    Lemma nconvert_sound (tn: tnum) (TN: ρ ∈ γ tn) (q: expr) :
      match am_get (nconvert q tn) with
      | Some (tn', _) =>
        tnum_mono tn tn' ∧
        ¬ error_expr ge e tmp m q
      | None => True
      end.

    Lemma nconvert_ex (tn: tnum) (TN: ρ ∈ γ(tn)) (q: expr) :
      match am_get (nconvert q tn) with
      | Some ((tp', nm'), lme) =>
        tnum_mono tn (tp', nm') ∧
        ∃ lpe, am_get (convert q tn) = Some ((tp', nm'), lpe) ∧
        ∀ v, eval_expr ge e tmp m q v →
             v ≠ Vundef →
        ∀ (TP: ρ ∈ γ tp') (ρn: cell → mach_num) (Nc: compat ρ ρn) (NM: ρn ∈ γ nm'),
             ∃ pe me n,
               In pe lpe ∧
               eval_pexpr ge m ρ e pe v ∧
               N.nconvert ge μ _ _ (λ x, x) _ _ NumDom sz nm' pt pe = inl me ∧
               In me lme ∧
               N.ncompat v n ∧
               N.wtype_num n (pexpr_get_ty pe) ∧
               eval_mexpr ρn me n
      | None => True
      end.

    Lemma convert_to_me (tn: tnum) (TN: ρ ∈ γ(tn)) (q: expr) :
      match am_get (convert q tn) with
      | Some ((tp', nm'), lpe) =>
        match am_get (me_of_pe_list nm' lpe) with
        | Some lme =>
          tnum_mono tn (tp', nm') ∧
          ∃ v, eval_expr ge e tmp m q v ∧ v ≠ Vundef
          ∧ ∀ (TP: ρ ∈ γ tp') (ρn: cell → mach_num) (Nc: compat ρ ρn) (NM: ρn ∈ γ nm'),
            ∃ pe me n,
                 In pe lpe ∧
                 eval_pexpr ge m ρ e pe v ∧
                 N.nconvert ge μ _ _ (λ x, x) _ _ NumDom sz nm' pt pe = inl me ∧
                 In me lme ∧
                 N.ncompat v n ∧
                 N.wtype_num n (pexpr_get_ty pe) ∧
                 eval_mexpr ρn me n
        | None => True
        end
      | None => True
      end.

  End CONVERT_CORRECT.

  End CONVERT.

  Definition t : Type := (stack+⊤ * (sizes * (points_to * tnum)))%type.
  Definition iter_t : Type := (stack+⊤ * (sizes * (points_to * (types * num_iter))))%type.

  Definition AbMem stk sz pt tp nm : t := (stk, (sz, (pt, (tp, nm)))).
  Definition ab_stk (ab: t) : stack+⊤ := fst ab.
  Definition ab_sz (ab: t) : sizes := fst (snd ab).
  Definition ab_pt (ab: t) : points_to := fst (snd (snd ab)).
  Definition ab_nm (ab: t) : tnum := snd (snd (snd ab)).
  Definition ab_tp (ab: t) : types := fst (snd (snd (snd ab))).
  Definition ab_num (ab: t) : num := snd (snd (snd (snd ab))).

  Arguments ab_stk ab /.
  Arguments ab_sz ab /.
  Arguments ab_pt ab /.
  Arguments ab_nm ab /.
  Arguments ab_tp ab /.
  Arguments ab_num ab /.

  Definition ab_stk_iter (ab: iter_t) : stack+⊤ := fst ab.
  Definition ab_sz_iter (ab: iter_t) : sizes := fst (snd ab).
  Definition ab_pt_iter (ab: iter_t) : points_to := fst (snd (snd ab)).
  Definition ab_nm_iter (ab: iter_t) : tnum_iter := snd (snd (snd ab)).
  Definition ab_tp_iter (ab: iter_t) : types := fst (snd (snd (snd ab))).
  Definition ab_num_iter (ab: iter_t) : num_iter := snd (snd (snd (snd ab))).

  Definition with_stk (f: stack+⊤ → stack+⊤) (ab: t) : t :=
    AbMem (f (ab_stk ab)) (ab_sz ab) (ab_pt ab) (ab_tp ab) (ab_num ab).

  Definition with_sz (f: sizes → sizes) (ab: t) : t :=
    AbMem (ab_stk ab) (f (ab_sz ab)) (ab_pt ab) (ab_tp ab) (ab_num ab).

  Definition with_pt (f: points_to → points_to) (ab: t) : t :=
    AbMem (ab_stk ab) (ab_sz ab) (f (ab_pt ab)) (ab_tp ab) (ab_num ab).

  Definition with_tp (f: types → types) (ab: t) : t :=
    AbMem (ab_stk ab) (ab_sz ab) (ab_pt ab) (f (ab_tp ab)) (ab_num ab).

  Definition with_num (f: num → num) (ab: t) : t :=
    AbMem (ab_stk ab) (ab_sz ab) (ab_pt ab) (ab_tp ab) (f (ab_num ab)).

  Definition with_tnum (f: tnum → tnum) (ab: t) : t :=
    (ab_stk ab, (ab_sz ab, (ab_pt ab, f (ab_nm ab)))).

  Definition dom {A} (x: positive) (m: PTree.t A) : bool :=
    match PTree.get x m with
    | Some _ => true
    | None => false
    end.

  Remark dom_set {A} x m y (a: A) : dom x (PTree.set y a m) = peq x y || dom x m.

  Instance stack_elt_gamma : gamma_op (lvarset * tvarset) (temp_env * env) :=
    λ ltv te_e,
    ∀ x, PSet.mem x (fst ltv) = dom x (snd te_e).

  Instance join_stack_elt_correct :
    join_op_correct (lvarset*tvarset) ((lvarset * tvarset)+⊤) (temp_env * env).

  Instance leb_stack_elt_correct :
    leb_op_correct (lvarset * tvarset) (temp_env * env).

  Record gamma (ab: t) (cs: concrete_state) : Prop :=
  { _ : fst cs ∈ γ(ab_stk ab)
  ; _ : ab_stk ab ≠ All → invariant cs
  ; _ : snd cs ∈ sizes_gamma ge (fst cs) (ab_sz ab)
  ; _ : mem_as_fun ge cs ∈ (points_to_gamma ge (fst cs) (ab_pt ab) ∩ γ(ab_nm ab))
  }.
  Instance t_gamma : gamma_op t concrete_state := gamma.

  Record iter_gamma (ab: iter_t) (cs: concrete_state) : Prop :=
  { _ : fst cs ∈ γ(ab_stk_iter ab)
  ; _ : ab_stk_iter ab ≠ All → invariant cs
  ; _ : snd cs ∈ sizes_gamma ge (fst cs) (ab_sz_iter ab)
  ; _ : mem_as_fun ge cs ∈ (points_to_gamma ge (fst cs) (ab_pt_iter ab) ∩ γ(ab_nm_iter ab))
  }.
  Instance iter_t_gamma : gamma_op iter_t concrete_state := iter_gamma.

  Definition split_t (ab:t) : option (ident * lvarset * tvarset * stack * sizes * points_to * tnum) :=
    match ab_stk ab with
    | All | Just nil => None
    | Just ((ε, τ) :: σ) =>
      let '(sz, (pt, tn)) := (snd ab) in
      Some (plength σ, ε, τ, σ, sz, pt, tn)
    end.

  Definition noerror (exp: expr) (ab: t) : alarm_mon unit :=
    match split_t ab with
    | Some (μ, ε, τ, σ, sz, pt, tn) =>
      do _ <- nconvert μ ε sz pt exp tn;
      ret tt
    | None => do _ <- alarm_am "anomaly (noerror)"; ret tt
    end.

  Definition ab_eval_expr (ab: t) (a: expr)
  : alarm_mon ((tnum * PTSet * AbTy.t+⊤ * list (mexpr cell)) +⊥) :=
    match split_t ab with
    | Some (μ, ε, τ, σ, sz, pt, tn) =>
      do (tn', lp) <- convert μ ε sz pt a tn;
      let '(tp', nm') := tn' in
      do ln <- me_of_pe_list μ sz pt nm' lp;
      match lp with nil => ret Bot | _ =>
      let '(a', ty) := union_list_map (λ e, (pt_eval_pexpr ge μ pt e, Just (pexpr_get_ty e))) (All, All) lp in
      ret (NotBot (tn', a', ty, ln))
      end
    | None => do _ <- alarm_am "ab_eval_expr failed"; ret Bot
    end.

  Fixpoint ab_eval_exprlist (ab: t) (e: list expr) : alarm_mon ((t * list (PTSet * AbTy.t+⊤ * list (mexpr cell)))+⊥) :=
    match e with
    | nil => ret (NotBot (ab, nil))
    | e :: e' =>
      do r <- ab_eval_expr ab e;
      match r with
      | Bot => ret Bot
      | NotBot (tn, pt, ty, me) =>
        do m <- ab_eval_exprlist (with_tnum (λ _, tn) ab) e';
        match m with
        | Bot => ret Bot
        | NotBot (ab, y) => ret (NotBot (ab, (pt, ty, me) :: y))
        end
      end
    end.

  Definition nm_forget_all :=
    fold_left (λ m c, bind m (AbMachineEnv.forget c)).

  Definition nm_upd (nm:num) (c:cell) (e:(mexpr cell)) : num+⊥ :=
    let nm' := AbMachineEnv.assign c e nm in
    nm_forget_all (overlap c) nm'.

  Definition nm_upd_cells (nm:num) (l:list cell) (e:(mexpr cell)) : num+⊥ :=
    union_list_map (λ c, nm_upd nm c e) (NotBot nm) l.

  Definition ct_forget_all {A: Type} := fold_left (λ (m: ACTreeDom.t A) c, ACTreeDom.set m c All).

  Definition ct_upd {A} (m:ACTreeDom.t A) (c:cell) (a:A+⊤) : ACTreeDom.t A :=
    ACTreeDom.set (ct_forget_all (overlap c) m) c a.

  Definition pt_upd (pt:points_to) (l:list cell) (s:BlockSet.t+⊤) : points_to :=
    union_list_map (λ c, ct_upd pt c s) pt l.

  Definition tp_upd_cells (tp:types) (l:list cell) (tt:AbTy.t+⊤) : types :=
    union_list_map (λ c, ct_upd tp c tt) tp l.


  Definition chunk_type (κ: typed_memory_chunk) (ty: AbTy.t+⊤) : bool :=
    match ty with
    | All => false
    | Just ty' =>
      match κ, ty' with
      | exist (Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned) _, VI
      | exist Mint32 _, (VI | VP | VIP)
      | exist Mint64 _, VL
      | exist Mfloat64 _, VF
      | exist Mfloat32 _, VS
        => true
      | _, _ => false
      end
    end.

  Definition assign_cells (κ: option typed_memory_chunk) (c: list cell) (a:expr) (ab:t) : alarm_mon (t+⊥) :=
    do res <- ab_eval_expr ab a;
    match res with
    | NotBot ((tp, nm), ptr, ty, ln) =>
        do _ <- am_assert match κ with Some κ => chunk_type κ ty | None => true end
                             ("bad type: " ++ to_string ty);
        ret (
            do nm' <- union_list_map (nm_upd_cells nm c) (NotBot nm) ln;
            let tp' := tp_upd_cells tp c ty in
            ret (AbMem (ab_stk ab) (ab_sz ab) (pt_upd (ab_pt ab) c ptr) tp' nm')
        )
    | Bot => ret Bot
    end.

  Definition assign_in (μ: fname) (x: ident) (a: expr) (ab: t) : alarm_mon (t+⊥) :=
    (assign_cells None (ACtemp μ x :: nil) a ab).

  Definition assign (x:ident) (a:expr) (ab:t) : alarm_mon (t+⊥) :=
    match ab_stk ab with
    | Just (_::σ) => assign_in (plength σ) x a ab
    | _ => do _ <- alarm_am "assign failed"; ret Bot
    end.

  Definition assign_any (x: ident) (ty: AbTy.t) (ab: t) : alarm_mon (t+⊥) :=
    match split_t ab with
    | Some (μ, ε, τ, σ, sz, pt, tn) =>
      let '(tp, nm) := tn in
      let c := ACtemp μ x in
      do nm' <-
            match ty with
            | VI | VL | VF | VS => ret (AbMachineEnv.forget c nm)
            | _ => do _ <- alarm_am ("assign_any: bad type " ++ to_string ty); ret Bot
            end;
        ret (
        do nm' <- nm';
        ret (with_num (λ _, nm')
                      (with_pt (λ pt, ACTreeDom.set pt c (Just BlockSet.empty))
                               (with_tp (λ tp, ACTreeDom.set tp c (Just ty)) ab))))
    | None => do _ <- alarm_am "assign_any failed"; ret Bot
    end.

  Definition permission_can_write (p: permission) : bool :=
    match p with
    | (Freeable | Writable) => true
    | (Readable | Nonempty) => false
    end.

  Definition cell_in_bounds (κ:typed_memory_chunk) (ab: t) (c: cell) : alarm_mon unit :=
    let b := ablock_of_cell c in
    let '(ofs, _) := range_of_cell c in
    match ABTreeDom.get b (ab_sz ab) with
    | All => do _ <- alarm_am ("block of unknown size: " ++ to_string b); ret tt
    | Just (hi, (perm, vol)) =>
      if permission_can_write perm then
      if zle 0 ofs && zle (ofs + size_chunk (proj1_sig κ)) hi
      then ret tt
      else do _ <- alarm_am ("cell out of range("++ to_string hi ++"): " ++ to_string c); ret tt
      else do _ <- alarm_am ("read-only cell: " ++ to_string c); ret tt
    end.

  Definition expr_has_cast_for_chunk (e: expr) (κ: typed_memory_chunk) : bool :=
    match κ, e with
    | exist Mint8signed _, Eunop Ocast8signed _
    | exist Mint8unsigned _, Eunop Ocast8unsigned _
    | exist Mint16signed _, Eunop Ocast16signed _
    | exist Mint16unsigned _, Eunop Ocast16unsigned _
    | exist Mint32 _, _
    | exist Mint64 _, _
    | exist Mfloat32 _, _
    | exist Mfloat64 _, _
      => true
    | _, _ => false
    end.

  Definition store (κ: memory_chunk) (a e: expr) (ab: t) : alarm_mon (t+⊥) :=
    let κ : option typed_memory_chunk :=
        match κ with
          | Many32 | Many64 => None
          | κ => Some (exist _ κ I)
        end
    in
    match κ with
      | None =>
        do _ <- alarm_am "invalid store memory chunk"; ret Bot
      | Some κ =>
        match split_t ab with
          | Some (μ, ε, τ, σ, sz, pt, tn) =>
            do _ <- am_assert (expr_has_cast_for_chunk e κ)
                  ("Uncasted expr for " ++ to_string (proj1_sig κ) ++ ": " ++ to_string e);
            do (tn', cells) <- deref_expr μ ε sz pt κ a tn;
            let ab := with_tnum (λ _, tn') ab in
            match cells with nil => ret Bot | _ =>
              do _ <- am_rev_map (cell_in_bounds κ ab) cells;
              assign_cells (Some κ) cells e ab
            end
          | None => do _ <- alarm_am "store failed"; ret Bot
        end
    end.

  Definition nassume b nm (F: mexpr cell → mexpr cell) e : num+⊥ :=
    union_list_map (λ me, AbMachineEnv.assume (F me) b nm) (NotBot nm) e.

  Definition bool_expr (e: expr) : expr :=
    match e with
    | Ebinop (Ocmp _| Ocmpu _| Ocmpf _| Ocmpfs _| Ocmpl _| Ocmplu _) _ _ => e
    | _ => Ebinop (Ocmp Cne) e (Econst (Csharpminor.Ointconst Int.zero))
    end.

  Definition assume (b: expr) (ab: t) : alarm_mon (t+⊥ * t+⊥) :=
    match split_t ab with
    | Some (μ, ε, τ, σ, sz, pt, tn) =>
      let b := bool_expr b in
      do (tn', b') <- nconvert μ ε sz pt b tn;
      let '(tp, nm) := tn' in
      ret
        (do nz <- nassume true nm id b'; ret (AbMem (Just ((ε,τ)::σ)) sz pt tp nz),
         do z <- nassume false nm id b'; ret (AbMem (Just ((ε,τ)::σ)) sz pt tp z))
    | None => do _ <- alarm_am "assume failed"; ret (Bot, Bot)
    end.

  Definition deref_fun (e: expr) (ab: t) : alarm_mon (list (ident * fundef)) :=
    match split_t ab with
    | Some (μ, ε, τ, σ, sz, pt, tn) =>
      do (tn, cells) <- deref_expr μ ε sz pt (exist _ Mint32 I) e tn;
      am_map' (λ c,
              match c with
              | ACglobal b 0 (exist Mint32 _) =>
                match Genv.find_funct_ptr ge b with
                | Some f =>
                  match Genv.invert_symbol ge b with
                  | Some i => Result (i,f)
                  | None => Error None "unknown function"
                  end
                | None => Error None ("bad function pointer " ++ to_string b)
                end
              | _ => Error None ("bad function pointer (2)")
              end) cells
    | None => do _ <- alarm_am "anomaly: deref_fun";
              ret nil
    end.

  Definition ab_bind_parameters (μ: ident)
             (formals: list ident) (args: list (PTSet * AbTy.t+⊤ * list (mexpr cell)))
             : alarm_mon (t+⊥) → alarm_mon (t+⊥) :=
    fold_left2
      (λ acc id v,
       do ab' <- acc;
       ret (
           do ab' <- ab';
           let c := ACtemp μ id in
           let '(ptr, ty, ln) := v in
           do nm' <- union_list_map (λ me, AbMachineEnv.assign c me (ab_num ab')) (NotBot (ab_num ab')) ln;
           ret (AbMem (ab_stk ab') (ab_sz ab')
                      (ct_upd (ab_pt ab') c ptr) (ct_upd (ab_tp ab') c ty)
                      nm'))
      )
      (λ _ _, do _ <- alarm_am "ab_bind_parameters: too many formals"; ret Bot)
      (λ _ _, do _ <- alarm_am "ab_bind_parameters: too many arguments"; ret Bot)
      formals args.

  Definition set_local_sizes μ vars : sizes → sizes :=
    fold_left (λ sz x_hi, ABTreeDom.set sz (ABlocal μ (fst x_hi)) (Just (snd x_hi, (Freeable, false))))
              vars.

  Definition push_frame (μ_def: function) (args: list expr) (ab:t) : alarm_mon (t+⊥) :=
    do σ' <- match ab_stk ab with
                | All => do _ <- alarm_am "no stack"; ret nil
                | Just σ' => ret σ'
                end;
      let μ := plength σ' in
      do res <- ab_eval_exprlist ab args;
      match res with
      | Bot => ret Bot
      | NotBot (ab, eargs) =>
      let ε := PSetOp.build (rev_map fst μ_def.(fn_vars)) in
      let τ := PSetOp.build (μ_def.(fn_temps) ++ μ_def.(fn_params)) in
      let σ := (ε, τ) :: σ' in
      let ab' := with_stk (λ _, Just σ) (with_sz (set_local_sizes μ μ_def.(fn_vars)) ab) in
      ab_bind_parameters μ μ_def.(fn_params) eargs (ret (NotBot ab'))
      end.

  Definition is_local_cell (μ: fname) (c: cell) : bool :=
    match c with
    | AClocal μ' _ _ _
    | ACtemp μ' _ => eq_dec μ μ'
    | ACglobal _ _ _ => false
    end.

  Definition is_local_block (μ: fname) (ab: ablock) : bool :=
    match ab with
    | ABlocal μ' _ => eq_dec μ μ'
    | ABglobal _ => false
    end.

  Definition pop_local_tp (μ: fname) : types → types :=
    ACTreeDom.SP.filter (λ c _, negb (is_local_cell μ c)).

  Definition pop_local_pt (μ: fname) : points_to → points_to :=
    ACTreeDom.SP.filter (λ c bs, negb (is_local_cell μ c) && negb (BSO.existsb (is_local_block μ) bs)).

  Definition clear_local_sizes μ ε : sizes → sizes :=
    PSet.fold (λ x, ABTree.remove (ABlocal μ x)) ε.

  Definition all_local_cells (μ: ident) (ε: lvarset) (sz: sizes) : list cell :=
    PSet.fold (λ x,
         let z := match ABTree.get (ABlocal μ x) sz with Some (z, _) => z | None => Z0 end in
         memory_chunk_fold (λ acc κ,
           let k := align_chunk (proj1_sig κ) in
           N.peano_rect _
             acc
             (λ n, cons (AClocal μ x (Z.of_N n * k) κ))
             (Z.to_N (z / k))
         )
    ) ε nil.

  Definition pop_local_num (μ: ident) (ε: lvarset) (τ: tvarset) (sz: sizes) : num+⊥ → num+⊥ :=
    (nm_forget_all (all_local_cells μ ε sz)) ∘ (nm_forget_all (List.map (ACtemp μ) (PSet.elements τ))).

  Definition pop_frame (res: option (expr)) (temp : option (ident)) (ab: t) : alarm_mon (t+⊥) :=
    match ab_stk ab, res, temp with
    | Just ((ε₀, τ₀)::(ε,τ)::σ), Some r, Some x =>
      let μ := plength σ in
      let μ₀ := Pos.succ μ in
(
      do ab' <- assign_in μ x r ab;
      match ab' with
      | NotBot ab'' =>
        ret (
            do nm' <- pop_local_num μ₀ ε₀ τ₀ (ab_sz ab'') (NotBot (ab_num ab''));
            ret (with_sz (clear_local_sizes μ₀ ε₀)
                (with_tp (pop_local_tp μ₀)
                (with_pt (pop_local_pt μ₀)
                (with_stk (λ _, Just ((ε,τ)::σ))
                (with_num (λ _, nm') ab''))))))
      | Bot => ret Bot
      end
      )
    | Just ((ε,τ)::nil), Some r, _ =>
      let μ := xH in
      do ret' <- ab_eval_expr ab r;
      match ret' with
      | Bot => ret Bot
      | NotBot (_, ty, _) =>
        match ty with
        | Just VI =>
          ret (NotBot (with_sz (clear_local_sizes μ ε)
                           (with_tp (pop_local_tp μ)
                           (with_pt (pop_local_pt μ)
                           (with_stk (λ _, Just nil) ab)))))
        | _ => do _ <- alarm_am "main ret not an int"; ret Bot
        end
      end
    | Just (_::nil), _, _ =>
      do _ <- alarm_am "pop_frame failed at main"; ret Bot
    | Just ((ε,τ)::σ), None, None =>
      let μ := plength σ in
        ret (
            do nm' <- pop_local_num μ ε τ (ab_sz ab) (NotBot (ab_num ab));
            ret (with_sz (clear_local_sizes μ ε)
                (with_tp (pop_local_tp μ)
                (with_pt (pop_local_pt μ)
                (with_stk (λ _, Just σ)
                (with_num (λ _, nm') ab))))))
    | Just ((ε,τ)::σ), Some r, None =>
      let μ := plength σ in
      do _ <- noerror r ab;
        ret (
            do nm' <- pop_local_num μ ε τ (ab_sz ab) (NotBot (ab_num ab));
            ret (with_sz (clear_local_sizes μ ε)
                (with_tp (pop_local_tp μ)
                (with_pt (pop_local_pt μ)
                (with_stk (λ _, Just σ)
                (with_num (λ _, nm') ab))))))
    | _, _, _ => do _ <- alarm_am ("pop_frame failed: " ++ to_string temp ++ " := " ++ to_string res ); ret Bot
    end.

  Let bad_align {T} (r: T) := do _ <- alarm_am "misaligned init data"; ret r.
  Instance InitDataToString : ToString init_data :=
    λ id,
    match id with
    | Init_int8 i => "int8: " ++ to_string i
    | Init_int16 i => "int16: " ++ to_string i
    | Init_int32 i => "int32: " ++ to_string i
    | Init_int64 i => "int64: " ++ to_string i
    | Init_float32 f => "float32: " ++ to_string f
    | Init_float64 f => "float64: " ++ to_string f
    | Init_space n => "space: " ++ to_string n
    | Init_addrof i o => "&" ++ to_string i ++ " + " ++ to_string o
    end.

  Definition type_of_chunk (κ: typed_memory_chunk) : AbTy.t :=
    match κ with
    | exist (Mint8signed | Mint8unsigned |
             Mint16signed | Mint16unsigned |
             Mint32) _
      => VI
    | exist Mint64 _ => VL
    | exist Mfloat64 _ => VF
    | exist Mfloat32 _ => VS
    | exist _ H => match H with end
    end.

  Definition permission_can_read (p: permission) : { perm_order p Readable } + { p = Nonempty } :=
    match p with
    | Freeable => left (perm_F_any Readable)
    | Writable => left perm_W_R
    | Readable => left (perm_refl Readable)
    | Nonempty => right eq_refl
    end.

  Definition zero_all_cells (b: block) (base: Z) (sz: Z) (ab: t): t+⊥ :=
    N.peano_rect
      (λ _, t+⊥)
      (NotBot ab)
      (λ ofs ab,
       memory_chunk_fold
         (λ ab κ,
          let ofs' := base + Z.of_N ofs in
          if Zdivide_dec (align_chunk (proj1_sig κ)) ofs' (align_chunk_pos (proj1_sig κ))
          && zle (Z.of_N ofs + size_chunk (proj1_sig κ)) sz then
            do ab <- ab;
              let c := ACglobal b ofs' κ in
              do nm <- AbMachineEnv.assign c
                (match κ with
                   | exist (Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned | Mint32) _
                     => me_const_i _ Int.zero
                   | exist Mint64 _ => me_const_l _ Int64.zero
                   | exist (Mfloat32) _ => me_const_s _ Float32.zero
                   | exist (Mfloat64) _ => me_const_f _ Float.zero
                   | exist _ H => match H with end
                 end)
                (ab_num ab);
              ret
                (with_tp (ACTree.set c (type_of_chunk κ))
                (with_pt (ACTree.set c BlockSet.empty)
                (with_num (λ _, nm) ab)))
          else ab
         ) ab)
      (Z.to_N sz).

  Definition ab_alloc_global perm vol b (gv: list init_data) ab : alarm_mon (t+⊥) :=
    do sz_ab' <- am_fold
      (λ (acc:_*(_+⊥)) id,
       let '(ofs, ab) := acc in
       let ofs' := ofs + Genv.init_data_size id in
       let c κ H := ACglobal b ofs (exist _ κ H) in
       if match id with
          | Init_space _
          | Init_int8 _ => true
          | Init_int16 _ => Zdivide_dec (align_chunk Mint16signed) ofs eq_refl
          | Init_int32 _
          | Init_addrof _ _ => Zdivide_dec (align_chunk Mint32) ofs eq_refl
          | Init_int64 _ => Zdivide_dec (align_chunk Mint64) ofs eq_refl
          | Init_float32 _ => Zdivide_dec (align_chunk Mfloat32) ofs eq_refl
          | Init_float64 _ => Zdivide_dec (align_chunk Mfloat64) ofs eq_refl
          end then
       match id return alarm_mon (Z*t+⊥) with
       | Init_int32 n =>
          ret (ofs',
                  if permission_can_read perm
                  then
                  do ab' <- ab;
                  do nm <- AbMachineEnv.assign (c Mint32 I) (me_const_i _ n) (ab_num ab');
                  ret (with_tp (ACTree.set (c Mint32 I) VI)
                      (with_pt (ACTree.set (c Mint32 I) BlockSet.empty)
                      (with_num (λ _, nm) ab')))
                  else ab)
       | Init_int64 n =>
          ret (ofs',
                  if permission_can_read perm
                  then
                  do ab' <- ab;
                  do nm <- AbMachineEnv.assign (c Mint64 I) (me_const_l _ n) (ab_num ab');
                  ret (with_tp (ACTree.set (c Mint64 I) VL)
                      (with_pt (ACTree.set (c Mint64 I) BlockSet.empty)
                      (with_num (λ _, nm) ab')))
                  else ab)
       | Init_addrof s o =>
         match Genv.find_symbol ge s with
         | Some b' => ret (ofs',
                              if permission_can_read perm
                              then
                              do ab' <- ab;
                              do nm <- AbMachineEnv.assign (c Mint32 I) (me_const_i _ o) (ab_num ab');
                              ret (with_tp (ACTree.set (c Mint32 I) VP)
                                  (with_pt (ACTree.set (c Mint32 I) (BSO.singleton (ABglobal b')))
                                  (with_num (λ _, nm) ab')))
                              else ab)
         | None => do _ <- alarm_am ("ab_alloc_globals: not a symbol ("
                                        ++ to_string s ++ ")"); ret (ofs', ab)
         end
       | Init_space s =>
         ret (ofs',
                 if negb (permission_can_read perm)
                 then ab else do ab' <- ab; zero_all_cells b ofs s ab')
       | Init_float64 f =>
         ret (ofs',
           if negb (permission_can_read perm)
           then ab
           else
             do ab' <- ab;
             do nm <- AbMachineEnv.assign (c Mfloat64 I) (MEconst _ (MNfloat f)) (ab_num ab');
             ret (with_tp (ACTree.set (c Mfloat64 I) VF)
                 (with_pt (ACTree.set (c Mfloat64 I) BlockSet.empty)
                 (with_num (λ _, nm) ab'))))
       | Init_float32 f =>
         ret (ofs',
           if negb (permission_can_read perm)
           then ab
           else
             do ab' <- ab;
             do nm <- AbMachineEnv.assign (c Mfloat32 I) (MEconst _ (MNsingle f)) (ab_num ab');
             ret (with_tp (ACTree.set (c Mfloat32 I) VS)
                 (with_pt (ACTree.set (c Mfloat32 I) BlockSet.empty)
                 (with_num (λ _, nm) ab'))))
       | Init_int8 i =>
         ret (ofs',
                 if permission_can_read perm
                 then
                 do ab' <- ab;
                 do nm <- AbMachineEnv.assign (c Mint8unsigned I) (MEunop Ocast8unsigned (me_const_i _ i)) (ab_num ab');
                 ret (with_tp (ACTree.set (c Mint8unsigned I) VI)
                     (with_pt (ACTree.set (c Mint8unsigned I) BlockSet.empty)
                     (with_num (λ _, nm) ab')))
                 else ab)
       | Init_int16 i =>
         ret (ofs',
                 if permission_can_read perm
                 then
                 do ab' <- ab;
                 do nm <- AbMachineEnv.assign (c Mint16unsigned I) (MEunop Ocast16unsigned (me_const_i _ i)) (ab_num ab');
                 ret (with_tp (ACTree.set (c Mint16unsigned I) VI)
                     (with_pt (ACTree.set (c Mint16unsigned I) BlockSet.empty)
                     (with_num (λ _, nm) ab')))
                 else ab)
       end
       else bad_align acc)
      gv
      (0, ab);
    let '(sz, ab') := sz_ab' in
    ret (do ab'' <- ab'; ret (with_sz (ABTree.set (ABglobal b) (sz, (perm, vol))) ab'')).

  Definition ab_alloc_globals (gl: list (ident * globdef fundef unit)) : alarm_mon (block * t+⊥) :=
    (am_fold
       (λ acc ig,
        let '(b, ab) := acc in
        let b' := Pos.succ b in
        match ig with
        | (_, Gfun _) => ret (b', fmap (with_sz (ABTree.set (ABglobal b) (1, (Nonempty, false)))) ab)
        | (_, Gvar gv) =>
            do ab' <- ab_alloc_global (Genv.perm_globvar gv) (gvar_volatile gv) b gv.(gvar_init) ab;
            ret (b', ab')
        end)
       gl
       (xH, do t <- ⊤; ret (Just nil, t))).

  Definition init_mem (defs:list (ident * globdef fundef unit)) : alarm_mon (t+⊥) :=
    do _ <- am_assert (norepet_map fst defs) ("duplicate name in globals");
    do ab <- ab_alloc_globals defs;
    ret (snd ab).

  Definition validate_volatile_ptr (sz: sizes) (ptr: BlockSet.t) (lne: list (mexpr cell)) : bool → bool :=
    BlockSet.fold
      (λ blk (acc: bool),
       if acc
       then
         match blk with
         | ABlocal _ _ => false
         | ABglobal b =>
           match Genv.invert_symbol ge b with
           | None => false
           | Some g =>
             match ABTreeDom.get blk sz with
             | Just (hi, (perm, vol)) =>
               vol
             | All => false
             end
           end
         end
       else acc)
      ptr.

  Definition check_volatile (tgt: (ident * int) + expr) (κ: memory_chunk) (ab: t) : alarm_mon ident :=
    do _ <-
    match tgt with
    | inl (g, ofs) =>
      match Genv.find_symbol ge g with
      | None => alarm_am "check_volatile: bad global"
      | Some b =>
        let b := ABglobal b in
        match ABTreeDom.get b (ab_sz ab) with
        | Just (hi, (perm, vol)) =>
          am_assert vol ("check_volatile: not volatile")
        | All => alarm_am "check_volatile: unknown size"
        end
      end
    | inr addr =>
      do z <- ab_eval_expr ab addr;
      match z with
      | NotBot (tn, Just ptr, Just VP, ne) =>
        am_assert (validate_volatile_ptr (ab_sz ab) ptr ne true) ("check_volatile: bad pointer")
      | _ => alarm_am "check_volatile: unresolved expression"
      end
    end;
    match ab_stk ab with
    | Just ( _ :: σ ) => ret (plength σ)
    | _ => do _ <- alarm_am "check_volatile: no stack"; ret xH
    end.

  Definition forget_cell (ab: t) (c: cell) : t+⊥ :=
    do nm' <- AbMachineEnv.forget c (ab_num ab);
    NotBot (with_pt (λ pt, ACTreeDom.set pt c All)
           (with_tp (λ tp, ACTreeDom.set tp c (⊤))
           (with_num (λ _, nm') ab))).

  Definition vload (rettemp: option ident) (g_ofs: option (ident * int)) (κ: memory_chunk) (args: list expr) (ab: t) : alarm_mon (t+⊥) :=
    do _ <- am_assert match κ with Mint64 | Mint32 | Mfloat32 | Mfloat64 => true | _ => false end "vload: bad chunk";
    match
    match g_ofs, args with
    | Some q, nil => Some (inl q)
    | None, addr :: nil => Some (inr addr)
    | _, _ => None
    end
    with
    | None => do _ <- alarm_am "vload: bad arguments"; ret Bot
    | Some tgt =>
    do μ <- check_volatile tgt κ ab;
    match rettemp with
    | None => ret (NotBot ab)
    | Some r =>
      match κ with
      | Mint64 => assign_any r VL ab
      | Mfloat64 => assign_any r VF ab
      | Mfloat32 => assign_any r VS ab
      | _ => ret (forget_cell ab (ACtemp μ r))
      end
    end
    end.

  Definition only_global_pointer (aptr: BlockSet.t+⊤) : bool :=
    match aptr with
    | All => false
    | Just ptr =>
      negb (BSO.existsb (λ p,
                             match p with
                             | ABglobal b => match Genv.invert_symbol ge b with Some g => negb (Senv.public_symbol ge g) | None => true end
                             | ABlocal _ _ => true
                             end) ptr)
    end.

  Definition vstore (rettemp: option ident) (g_ofs: option (ident * int)) (κ: memory_chunk) (args: list expr) (ab: t) : alarm_mon (t+⊥) :=
    match
    match g_ofs, args with
    | Some q, arg :: nil => Some (inl q, arg)
    | None, addr :: arg :: nil => Some (inr addr, arg)
    | _, _ => None
    end
    with
    | None => do _ <- alarm_am "vstore: bad arguments"; ret Bot
    | Some (tgt, arg) =>
    do μ <- check_volatile tgt κ ab;
    do v <- ab_eval_expr ab arg;
    match v with
    | Bot => ret Bot
    | NotBot (tn, ptr, oty, lne) =>
      do _ <- am_assert
            match oty with
            | Just ty =>
              match ty, κ with
              | VL, Mint64
              | VS, Mfloat32
              | VF, Mfloat64
              | VI, ( Mint32 | Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned )
                => true
              | (VIP|VP), Mint32 => only_global_pointer ptr
              | _, _ => false
              end
            | All => false
            end
            ("vstore: cannot prove that the argument " ++ to_string arg ++ " is well-typed " ++ to_string oty);
      let ab := with_tnum (λ _, tn) ab in
      match rettemp with
      | None => ret (NotBot ab)
      | Some r => ret (forget_cell ab (ACtemp μ r))
      end
    end
    end.

  Instance widen_mem : widen_op (iter_t+⊥) (t+⊥) :=
    {| widen A B :=
         let '(NUM_it_ret, NUM_ret) :=
           match A with
           | Bot => init_iter Bot
           | NotBot (_, (_, (_, (_, NUM)))) => NUM
           end ▽
           match B with
           | Bot => Bot
           | NotBot (_, (_, (_, (_, NUM)))) => NotBot NUM
           end
         in
         match B with
         | Bot =>
           match A with
           | Bot => (Bot, Bot)
           | NotBot (STK, (SZ, (PT, (TP, _)))) =>
             (NotBot (STK, (SZ, (PT, (TP, NUM_it_ret)))),
              do NUM_ret <- NUM_ret;
              ret (STK, (SZ, (PT, (TP, NUM_ret)))))
           end
         | NotBot (STK', (SZ', (PT', (TP', _)))) =>
           match A with
           | Bot =>
             (NotBot (STK', (SZ', (PT', (TP', NUM_it_ret)))),
              do NUM_ret <- NUM_ret;
              ret (STK', (SZ', (PT', (TP', NUM_ret)))))
           | NotBot (STK, (SZ, (PT, (TP, NUM)))) =>
             let STK_ret :=
               match STK, STK' with
               | Just STK, Just STK' => list_widen join STK STK'
               | _, _ => All
               end
             in
             let SZ_ret := sizes_widen SZ SZ' in
             let PT_ret := points_to_widen PT PT' in
             let TP_ret := types_widen TP TP' in
             (NotBot (STK_ret, (SZ_ret, (PT_ret, (TP_ret, NUM_it_ret)))),
              do NUM_ret <- NUM_ret;
              ret (STK_ret, (SZ_ret, (PT_ret, (TP_ret, NUM_ret)))))
           end
         end;
       init_iter x :=
         do x <- x;
         ret (ab_stk x, (ab_sz x, (ab_pt x, (ab_tp x, init_iter (NotBot (ab_num x))))))
    |}.

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

  Instance mem_cshm_dom : mem_dom t (iter_t+⊥) :=
    {| assign := assign
     ; assign_any := assign_any
     ; store := store
     ; assume := assume

     ; noerror := noerror
     ; deref_fun := deref_fun

     ; ab_vload := vload
     ; ab_vstore := vstore

     ; push_frame := push_frame
     ; pop_frame := pop_frame

     ; ab_malloc sz dst ab := do _ <- alarm_am "malloc"; ret (⊤)
     ; ab_free e ab := do _ <- alarm_am "free"; ret (⊤)
     ; ab_memcpy sz al dst src ab :=
         do _ <- alarm_am ("memcpy(" ++ to_string sz ++ ", " ++ to_string al ++ ", " ++ to_string dst ++ ", " ++ to_string src ++ ")");
         ret (⊤)

     ; init_mem := init_mem
    |}.

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

  Instance t_join_correct : join_op_correct t (t+⊥) concrete_state.

  Instance t_leb_correct : leb_op_correct t concrete_state.

  Instance TToString : ToString t :=
    (λ x,
    "Mem { " ++ "stack : " ++ to_string (ab_stk x) ++ new_line
             ++ "blocks: " ++ to_string (ab_sz x) ++ new_line
             ++ "points: " ++ to_string (ab_pt x) ++ new_line
             ++ "types : " ++ to_string (ab_tp x) ++ new_line
             ++ "num : " ++ to_string (ab_num x) ++ new_line
             ++ "}" ++ new_line ).

  Instance IterTToString : ToString iter_t :=
      (λ x,
       "Mem { " ++ "stack : " ++ to_string (ab_stk_iter x) ++ new_line
                ++ "blocks: " ++ to_string (ab_sz_iter x) ++ new_line
                ++ "points: " ++ to_string (ab_pt_iter x) ++ new_line
                ++ "types : " ++ to_string (ab_tp_iter x) ++ new_line
                ++ "num : " ++ to_string (ab_num_iter x) ++ new_line
                ++ "}" ++ new_line ).

End num.