Module Mconvert

Require DebugAbMachineEnv NoError PointsTo.
Import
  Utf8
  String
  Coqlib
  AST
  Integers
  Floats
  Values
  Globalenvs
  Memory
  Cminor
  Csharpminorannot
  ToString
  Util
  AssocList
  ShareTree
  AdomLib
  AbMachineEnv
  AlarmMon
  PExpr
  NoError
  Cells
  PointsTo.

Section LOG.

Context (L: Type).

Definition nconvert_t A : Type := alarm_mon L (list A).

Section FMA.
  Context {A B} (f: A → nconvert_t B).

  Definition flat_map_a (q: nconvert_t A) : nconvert_t B :=
    do q <- (q: alarm_mon L (list A));
    (fix rec (q: list A) :=
       match q with
       | nil => ret nil
       | a :: a' =>
         do b <- (f a : alarm_mon L (list B));
       do b' <- rec a';
       ret (b ++ b')%list
       end
    ) q.

    Inductive flat_map_a_spec : list A → list B → Prop :=
    | FMA_nil : flat_map_a_spec nil nil
    | FMA_app
        a bs
        `(am_get (f a) = Some bs)
        q r
        `(flat_map_a_spec q r)
        : flat_map_a_spec (a :: q) (bs ++ r)
    .

    Definition flat_map_a_spec_nil_inv (r: list B) :
      flat_map_a_spec nil r →
      r = nil :=
      λ H,
      match H in flat_map_a_spec x r
            return match x return Prop
                   with _ :: _ => True
                   | nil => r = nil
                   end
      with
      | FMA_app _ _ _ _ _ _ => I
      | FMA_nil => eq_refl
      end.

    Definition flat_map_a_spec_cons_inv (a: A) (q: list A) (r: list B) :
      flat_map_a_spec (a :: q) r →
      ∃ bs r', am_get (f a) = Some bs ∧ r = app bs r' ∧ flat_map_a_spec q r'.

    Lemma flat_map_a_spec_nil_r (r: list A) :
      flat_map_a_spec r nil →
      r = nil ∨ r ≠ nil ∧ ∀ a, In a r → am_get (f a) = Some nil.
    
    Lemma flat_map_a_correct (q: nconvert_t A) (bs: list B) :
      am_get (flat_map_a q) = Some bs →
      ∃ q' : list A, am_get q = Some q' ∧ flat_map_a_spec q' bs.

      Lemma fma_in q bs :
        flat_map_a_spec q bs →
        ∀ b, In b bs → ∃ a, In a q ∧ ∃ r, am_get (f a) = Some r ∧ In b r.

      Lemma fma_in' q bs :
        flat_map_a_spec q bs →
        ∀ a, In a q → ∃ b, am_get (f a) = Some b ∧ ∀ x, In x b → In x bs.

      Lemma fma_app a b c d :
        flat_map_a_spec a b →
        flat_map_a_spec c d →
        flat_map_a_spec (a ++ c) (b ++ d).

End FMA.

Global Arguments flat_map_a_correct {A B} [f q bs] _.

Global
Instance nconvert_monad : monad nconvert_t :=
  {
    ret A := λ a, ret (a :: nil);
    bind A B m f := flat_map_a f m
  }.

Definition assert (b: bool) err :=
  if b then ret tt else ((tt :: nil, (err :: nil, nil)): (nconvert_t unit)).

Lemma fma_bind {A B C} (e: nconvert_t B) (f: A → B → nconvert_t C) a c :
  flat_map_a_spec (λ x, do y <- e; f x y) a c →
  a ≠ nil →
  ∃ b : list B,
    am_get e = Some b ∧
    flat_map_a_spec (curry f) (pair_list a b) c.

Lemma flat_map_a_spec_assoc {A B C} (f: A → nconvert_t B) (g: B → nconvert_t C) (ma: list A) (mc: list C) :
  flat_map_a_spec (λ a, flat_map_a g (f a)) ma mc →
  ∃ mb,
    flat_map_a_spec f ma mb ∧ flat_map_a_spec g mb mc.

Lemma flat_map_a_spec_assert {A B} (f: A → nconvert_t B) (b: A → bool) (e: _) ma mb :
  flat_map_a_spec (λ a, do _ <- assert (b a) (e a); f a) ma mb →
  (∀ a, In a ma → b a = true) ∧
  flat_map_a_spec f ma mb.

End LOG.

Local Unset Elimination Schemes.

Local Open Scope string_scope.

Module Nconvert(T:SHARETREE).

Module Import PT := PT T.

  Section nconvert.
    Variable L: Type.
    Variable ge: genv.
    Variable m: Mem.mem.
    Variable μ: ident.
    Variable ε: env.
    Variable tmp: temp_env.
    Variable σ : list (temp_env * env).
    Hypothesis Hμ : μ = plength σ.

    Variable var : Type.
    Variable var_dec : EqDec var.
    Variable elt2p: T.elt -> var.
    Variables num iter_num : Type.
    Variable NumDom : ab_machine_env (var := var) num iter_num.

    Definition convert_constant (cst: constant) : mexpr var :=
      match cst with
        | Ointconst n => MEconst _ (MNint n)
        | Olongconst n => MEconst _ (MNint64 n)
        | Ofloatconst f => MEconst _ (MNfloat f)
        | Osingleconst f => MEconst _ (MNsingle f)
        | Oaddrsymbol _ ofs => MEconst _ (MNint ofs)
      end.

    Inductive nconvert_msg_kind : Set :=
    | MSG_ILL_TYPED_UNOP
    | MSG_ILL_TYPED_BINOP
    | MSG_LARGE_PTSET
    | MSG_UNSAFE_NUM
    | MSG_VALID_PTR
    | MSG_EQ_BLOCKS
    | MSG_CMP_BLK_DK
    | MSG_CMP_OP
    | MSG_NULL
    .

    Definition nconvert_msg_type (k: nconvert_msg_kind) : Type :=
      match k with
      | MSG_LARGE_PTSET => Cminor.binary_operation → type+⊤ → type+⊤ → string
      | MSG_NULL
      | MSG_UNSAFE_NUM
        => mexpr var → string
      | MSG_EQ_BLOCKS
      | MSG_CMP_BLK_DK
        => BlockSet.t → BlockSet.t → string
      | MSG_ILL_TYPED_UNOP => Cminor.unary_operation → typ → string
      | MSG_ILL_TYPED_BINOP => Cminor.binary_operation → typ → typ → string
      | MSG_VALID_PTR => bool → BlockSet.t → mexpr var → string
      | MSG_CMP_OP => comparison → string
      end.

    Section STRING_OF_MEXPR.

    Import DebugAbMachineEnv DebugCminor.
 
    Local Instance AblockToString : ToString ablock := AblockToString ge.
    Local Instance string_of_type : ToString type := string_of_type ge.
    Existing Instances MN_ToString MNI_ToString.

    Context (nm: num).

    Fixpoint string_of_mexpr (e: mexpr var) {struct e} : string :=
      match e with
      | MEvar ty v => to_string (get_itv (MEvar ty v) nm)
      | MEconst c => to_string c
      | MEunop op e' => string_of_unop op ++ string_of_mexpr e'
      | MEbinop op x y => "(" ++ string_of_mexpr x ++ string_of_binop op ++ string_of_mexpr y ++ ")"
      end.

    Definition nconvert_msg (k: nconvert_msg_kind) : nconvert_msg_type k :=
      match k return nconvert_msg_type k with
      | MSG_ILL_TYPED_UNOP => λ op ty, "ill-typed op: " ++ to_string op ++ to_string ty
      | MSG_ILL_TYPED_BINOP => λ op ty₁ ty₂, "ill-typed op: " ++ to_string ty₁ ++ to_string op ++ to_string ty₂
      | MSG_LARGE_PTSET => λ op ty₁ ty₂, "too large points-to set in subtraction or comparison: " ++ to_string ty₁ ++ to_string op ++ to_string ty₂
      | MSG_UNSAFE_NUM=> λ me, "cannot prove safe a numerical expression: " ++ string_of_mexpr me
      | MSG_VALID_PTR => λ weak bs me, "cannot prove pointer " ++ (if weak then "weakly " else "") ++ "valid: " ++ to_string bs ++ " " ++ string_of_mexpr me
      | MSG_EQ_BLOCKS => λ bs₁ bs₂, "cannot prove blocks equal in subtraction " ++ to_string bs₁ ++ " and " ++ to_string bs₂
      | MSG_CMP_BLK_DK => λ bs₁ bs₂, "cannot compare points-to sets " ++ to_string bs₁ ++ " and " ++ to_string bs₂
      | MSG_CMP_OP => λ c, "bad comparison operator: " ++ to_string c
      | MSG_NULL => λ me, "cannot prove definitely null: " ++ string_of_mexpr me
      end.
    Global Opaque nconvert_msg.

    End STRING_OF_MEXPR.

    Definition well_typed_unop (op: unary_operation) (ty: typ) : bool :=
      match op with
      | Ocast8unsigned
      | Ocast8signed
      | Ocast16unsigned
      | Ocast16signed
      | Onegint
      | Onotint
      | Ofloatofint
      | Ofloatofintu
      | Osingleofint
      | Osingleofintu
      | Olongofint
      | Olongofintu
          => eq_dec VI ty
      | Onegf
      | Oabsf
      | Osingleoffloat
      | Ointoffloat
      | Ointuoffloat
      | Olongoffloat
      | Olonguoffloat
          => eq_dec VF ty
      | Onegfs
      | Oabsfs
      | Ofloatofsingle
      | Ointofsingle
      | Ointuofsingle
      | Olongofsingle
      | Olonguofsingle
          => eq_dec VS ty
      | Onegl
      | Onotl
      | Ointoflong
      | Ofloatoflong
      | Ofloatoflongu
      | Osingleoflong
      | Osingleoflongu
          => eq_dec VL ty
      end.

    Inductive nconvert_binop_cases : Type :=
    | NBC_normal
    | NBC_ptr_sub
    | NBC_ptr_ptr_cmp `(comparison)
    | NBC_ptr_int_cmp `(bool) `(comparison)
    | NBC_wrong
    .

    Definition nbc_classify (op: binary_operation) (ty₁ ty₂: typ) : nconvert_binop_cases :=
      match ty₁, ty₂, op with
      | VI, (VIP | VP), Oadd | (VIP | VP), VI, Oadd
      | (VIP | VP), VI, Osub
      | VI, VI,
        (Oadd | Osub | Omul | Odiv | Odivu | Omod | Omodu | Oand
         | Oor | Oxor | Oshl | Oshr | Oshru | Ocmp _ | Ocmpu _)
      | VL, VL,
        (Oaddl | Osubl | Omull | Odivl | Odivlu | Omodl | Omodlu
         | Oandl | Oorl | Oxorl | Ocmpl _ | Ocmplu _)
      | VL, VI, (Oshll | Oshrl | Oshrlu)
      | VF, VF, (Oaddf | Osubf | Omulf | Odivf | Ocmpf _)
      | VS, VS, (Oaddfs | Osubfs | Omulfs | Odivfs | Ocmpfs _) =>
        NBC_normal
      | VP, VP, Osub => NBC_ptr_sub
      | VP, VP, Ocmpu c => NBC_ptr_ptr_cmp c
      | VP, VI, Ocmpu c => NBC_ptr_int_cmp false c
      | VI, VP, Ocmpu c => NBC_ptr_int_cmp true c
      | _, _, _ => NBC_wrong
      end.

    Lemma nbc_classify_intro :
      forall P : binary_operation -> typ -> typ -> nconvert_binop_cases -> Prop,

        (forall o x y, P o x y NBC_wrong) ->

        P Oadd VI VIP NBC_normal ->
        P Oadd VI VP NBC_normal ->
        P Oadd VIP VI NBC_normal ->
        P Oadd VP VI NBC_normal ->

        P Osub VIP VI NBC_normal ->
        P Osub VP VI NBC_normal ->

        P Oadd VI VI NBC_normal ->
        P Osub VI VI NBC_normal ->
        P Omul VI VI NBC_normal ->
        P Odiv VI VI NBC_normal ->
        P Odivu VI VI NBC_normal ->
        P Omod VI VI NBC_normal ->
        P Omodu VI VI NBC_normal ->
        P Oand VI VI NBC_normal ->
        P Oor VI VI NBC_normal ->
        P Oxor VI VI NBC_normal ->
        P Oshl VI VI NBC_normal ->
        P Oshr VI VI NBC_normal ->
        P Oshru VI VI NBC_normal ->
        (forall c, P (Ocmp c) VI VI NBC_normal) ->
        (forall c, P (Ocmpu c) VI VI NBC_normal) ->

        P Oaddl VL VL NBC_normal ->
        P Osubl VL VL NBC_normal ->
        P Omull VL VL NBC_normal ->
        P Odivl VL VL NBC_normal ->
        P Odivlu VL VL NBC_normal ->
        P Omodl VL VL NBC_normal ->
        P Omodlu VL VL NBC_normal ->
        P Oandl VL VL NBC_normal ->
        P Oorl VL VL NBC_normal ->
        P Oxorl VL VL NBC_normal ->
        (forall c, P (Ocmpl c) VL VL NBC_normal) ->
        (forall c, P (Ocmplu c) VL VL NBC_normal) ->

        P Oshll VL VI NBC_normal ->
        P Oshrl VL VI NBC_normal ->
        P Oshrlu VL VI NBC_normal ->

        P Oaddf VF VF NBC_normal ->
        P Osubf VF VF NBC_normal ->
        P Omulf VF VF NBC_normal ->
        P Odivf VF VF NBC_normal ->
        (forall c, P (Ocmpf c) VF VF NBC_normal) ->

        P Oaddfs VS VS NBC_normal ->
        P Osubfs VS VS NBC_normal ->
        P Omulfs VS VS NBC_normal ->
        P Odivfs VS VS NBC_normal ->
        (forall c, P (Ocmpfs c) VS VS NBC_normal) ->

        P Osub VP VP NBC_ptr_sub ->
        (forall c, P (Ocmpu c) VP VP (NBC_ptr_ptr_cmp c)) ->
        (forall c, P (Ocmpu c) VP VI (NBC_ptr_int_cmp false c)) ->
        (forall c, P (Ocmpu c) VI VP (NBC_ptr_int_cmp true c)) ->

        forall o x y, P o x y (nbc_classify o x y).

    Context {MD: Type} (sz : ABTree.t (Z * MD)).
    Hypothesis SZ :
      ∀ b hi md b',
        ABTreeDom.get b sz = Just (hi, md) →
        block_of_ablock ge ((tmp, ε) :: σ) b = Some b' →
        Mem.range_perm m b' 0 hi Cur Nonempty.
    
    Variable nm : num.

    Definition is_valid_ptr (weak: bool) (bs: BlockSet.t) (off: mexpr var) : bool :=
      match min_size sz bs MaxSize with
      | MaxSize => false
      | Size (Zpos min) =>
        let i := Int.repr (Zpos (if weak then Pos.succ min else min)) in
        Pos.ltb min (Z.to_pos Int.max_unsigned) &&
                is_bot (assume (MEbinop (Ocmpu Clt) off (me_const_i _ i)) false nm)
      | Size _
      | MinSize => false
      end.

    Let is_null := is_null NumDom nm.

    Notation "'error' e" := (do _ <- alarm_am e; ret nil) (at level 50).
    Local Notation am_assert b err :=
      (assert L b (λ _, err)).

    Fixpoint nconvert (pt: points_to) (e:pexpr T.elt) : nconvert_t L (mexpr var) :=
      match e with
        | PEvar c ty =>
          match ty with
            | VI|VP|VIP => ret (MEvar MNTint (elt2p c))
            | VL => ret (MEvar MNTint64 (elt2p c))
            | VF => ret (MEvar MNTfloat (elt2p c))
            | VS => ret (MEvar MNTsingle (elt2p c))
          end
        | PElocal _ => ret (MEconst _ (MNint Int.zero))
        | PEconst cst _ _ => ret (convert_constant cst)

        | PEunop op e _ _ =>
          let ty := pexpr_get_ty e in
          do _ <- am_assert (well_typed_unop op ty)
             (nconvert_msg nm MSG_ILL_TYPED_UNOP op ty);
          do e' <- nconvert pt e;
            ret (MEunop op e')

        | PEbinop op e1 e2 _ _ =>
          let ty₁ := pexpr_get_ty e1 in
          let ty₂ := pexpr_get_ty e2 in
          match nbc_classify op ty₁ ty₂ with

          | NBC_normal =>
            do e1' <- nconvert pt e1;
            do e2' <- nconvert pt e2;
            ret (MEbinop op e1' e2')

          | NBC_ptr_sub =>
            do nx <- nconvert pt e1;
            do ny <- nconvert pt e2;
            match pt_eval_pexpr ge μ pt e1, pt_eval_pexpr ge μ pt e2 with
            | Just (TyPtr (Just xb)), Just (TyPtr (Just yb)) =>
              let res := MEbinop op nx ny in
              match cmp_blockset xb yb with
              | Equal b => ret res
              | _ => error (nconvert_msg nm MSG_EQ_BLOCKS xb yb)
              end
            | ty₁, ty₂ =>
              error (nconvert_msg nm MSG_LARGE_PTSET Osub ty₁ ty₂)
            end

          | NBC_ptr_ptr_cmp c =>
            do nx <- nconvert pt e1;
            do ny <- nconvert pt e2;
            match pt_eval_pexpr ge μ pt e1, pt_eval_pexpr ge μ pt e2 with
            | Just (TyPtr (Just xb)), Just (TyPtr (Just yb)) =>
              match cmp_blockset xb yb with
              | Equal b =>
                let res := MEbinop (Ocmpu c) nx ny in
                do _ <- am_assert (is_valid_ptr true xb nx)
                   (nconvert_msg nm MSG_VALID_PTR true xb nx);
                do _ <- am_assert (is_valid_ptr true yb ny)
                   (nconvert_msg nm MSG_VALID_PTR true yb ny);
                 ret res
              | Disjoint =>
                do _ <- am_assert (noerror nx nm)
                   (nconvert_msg nm MSG_UNSAFE_NUM nx);
                do _ <- am_assert (noerror ny nm)
                   (nconvert_msg nm MSG_UNSAFE_NUM ny);
                do _ <- am_assert (is_valid_ptr false xb nx)
                   (nconvert_msg nm MSG_VALID_PTR false xb nx);
                do _ <- am_assert (is_valid_ptr false yb ny)
                   (nconvert_msg nm MSG_VALID_PTR false yb ny);
                match c with
                | Ceq => ret (MEconst _ (MNint Int.zero))
                | Cne => ret (MEconst _ (MNint Int.one))
                | _ => error (nconvert_msg nm MSG_CMP_OP c)
                end
              | DontKnow =>
                do _ <- am_assert (noerror nx nm)
                   (nconvert_msg nm MSG_UNSAFE_NUM nx);
                do _ <- am_assert (noerror ny nm)
                   (nconvert_msg nm MSG_UNSAFE_NUM ny);
                do _ <- am_assert (is_valid_ptr false xb nx)
                   (nconvert_msg nm MSG_VALID_PTR false xb nx);
                do _ <- am_assert (is_valid_ptr false yb ny)
                   (nconvert_msg nm MSG_VALID_PTR false yb ny);
                match c with
                | (Ceq | Cne) =>
                  (MEconst _ (MNint Int.zero) :: MEconst _ (MNint Int.one) :: nil, (nil, nil))
                | _ => error (nconvert_msg nm MSG_CMP_BLK_DK xb yb)
                end
              | Contradiction =>
                do _ <- am_assert (noerror nx nm)
                   (nconvert_msg nm MSG_UNSAFE_NUM nx);
                do _ <- am_assert (noerror ny nm)
                   (nconvert_msg nm MSG_UNSAFE_NUM ny);
                ret (MEconst _ (MNint Int.one))
              end
            | ty₁, ty₂ =>
              error (nconvert_msg nm MSG_LARGE_PTSET (Ocmpu c) ty₁ ty₂)
            end

          | NBC_ptr_int_cmp swapped c =>
            do nx <- nconvert pt e1;
            do ny <- nconvert pt e2;
            do _ <- am_assert (noerror nx nm)
               (nconvert_msg nm MSG_UNSAFE_NUM nx);
            do _ <- am_assert (noerror ny nm)
               (nconvert_msg nm MSG_UNSAFE_NUM ny);
            do _ <- am_assert (is_null (if swapped then nx else ny))
               (nconvert_msg nm MSG_NULL (if swapped then nx else ny));
            match pt_eval_pexpr ge μ pt (if swapped then e2 else e1) with
            | Just (TyPtr (Just bs)) =>
              match c with
              | (Ceq | Cne) =>
                let res := MEconst _ (MNint match c with Ceq => Int.zero | _ => Int.one end) in
                do _ <- am_assert (is_valid_ptr true bs (if swapped then ny else nx))
                   (nconvert_msg nm MSG_VALID_PTR true bs (if swapped then ny else nx));
                ret res
              | _ => error (nconvert_msg nm MSG_CMP_OP c)
              end
            | ty =>
              error (nconvert_msg nm MSG_LARGE_PTSET (Ocmpu c)
                                  (if swapped then All else ty)
                                  (if swapped then ty else All))
            end

          | NBC_wrong => error (nconvert_msg nm MSG_ILL_TYPED_BINOP op ty₁ ty₂)
          end
      end.

    Local
    Ltac clarify :=
      repeat (eq_some_inv; match goal with
             | NE : ?x ≠ ?y, OR: ?x = ?y ∨ _ |- _ =>
               destruct OR as [ OR | OR ]; [ elim (NE OR); fail | ]
             | NEx : ?x ≠ nil, NEy : ?y ≠ nil, OR: pair_list ?x ?y = nil ∨ _ |- _ =>
               destruct OR as [ OR | OR ]; [ elim (pair_list_not_nil NEx NEy OR); fail | ]
             | H : ?x = ?y |- _ => subst y || subst x
             | H : am_get (_, (nil, _)) = Some _ |- _ => apply some_eq_inv in H
             | H : am_get (_, (_ :: _, _)) = Some _ |- _ => exact (None_not_Some H _)
             | H : am_get (flat_map_a _ _ _) = Some _ |- _ =>
               apply flat_map_a_correct in H; hsplit
             | H : am_get (do _ <- _; _) = Some _ |- _ =>
               let K := fresh in
               rename H into K;
               pose proof (flat_map_a_correct _ K) as H; clear K
                                                        
             | H : am_get match ?x with All => _ | _ => _ end = Some _ |- _ =>
               destruct x eqn: ?
             | H : am_get match ?x with TyFloat => _ | _ => _ end = Some _ |- _ =>
               destruct x eqn: ?
             | H : am_get match cmp_blockset ?x ?y with _ => _ end = Some _ |- _ =>
               pose proof (cmp_blockset_correct x y);
                 destruct (cmp_blockset x y)
             | H : am_get match ?x with Ceq => _ | _ => _ end = Some _ |- _ =>
               destruct x
             | H : am_get (am_assert (noerror ?x ?y) _) = Some _, NM : mach_gamma ?y _ |- _ =>
               let K := fresh in
               destruct (noerror x y) eqn: K; [
                   pose proof (noerror_correct y NM K)
                 | ]; simpl in H
             | H : am_get (am_assert (noerror ?x ?y) _) = Some _ |- _ =>
               destruct (noerror x y) eqn: ?; simpl in H
             | H : am_get (am_assert (is_valid_ptr ?x ?y ?z) _) = Some _ |- _ =>
               destruct (is_valid_ptr x y z) eqn: ?; simpl in H
             | H : am_get (am_assert (is_null ?x) _) = Some _ |- _ =>
               destruct (is_null x) eqn: ?; simpl in H

             | H : flat_map_a_spec _ _ (_ :: _) _ |- _ =>
               apply flat_map_a_spec_cons_inv in H; hsplit
             | H : flat_map_a_spec _ _ nil _ |- _ =>
               apply flat_map_a_spec_nil_inv in H; hsplit
             | H : flat_map_a_spec _ _ _ nil |- _ =>
               apply flat_map_a_spec_nil_r in H
             | H : flat_map_a_spec _ _ ?a _, Ha: ?a ≠ nil |- _ =>
               let K := fresh in
               rename H into K;
               pose proof (fma_bind _ _ _ _ _ K Ha) as H; clear K

             | H : In _ (_ ++ nil) |- _ =>
               apply in_app in H; destruct H as [ H | () ]
             | H : In _ nil |- _ =>
               destruct H as ()
             | H : In _ (_ :: nil) |- _ =>
               destruct H as [ H | () ]
             | H : In _ (_ :: _ :: nil) |- _ =>
               destruct H as [ H | [ H | () ] ]

             | H : ∀ x, In x (_ :: nil) → _ |- _ =>
               specialize (H _ (or_introl _ eq_refl))
             | H : ∀ x, In x (_ ++ nil) → _ |- _ =>
               repeat rewrite app_nil_r in H
             end).

    Local
    Ltac forward :=
      repeat match goal with
             | H : ∀ _, _ → _, K : _ |- _ => specialize (H _ K)
    end.

    Lemma nconvert_fv pt pe :
      ∀ lme, am_get (nconvert pt pe) = Some lme →
      ∀ me, In me lme →
      ∀ x, x ∈ me_free_var me → ∃ y, y ∈ pe_free_var pe ∧ x = elt2p y.

    Definition ncompat : val -> mach_num -> Prop :=
      λ v, match v with
             | Vint i | Vptr _ i => eq (MNint i)
             | Vlong l => eq (MNint64 l)
             | Vsingle f => eq (MNsingle f)
             | Vfloat f => eq (MNfloat f)
             | Vundef => λ _, True
           end.

    Lemma ncompat_inv_int v i :
      ncompat v (MNint i) →
      v = Vint i ∨ (∃ b, v = Vptr b i) ∨ v = Vundef.

    Lemma ncompat_inv_int64 v i :
      ncompat v (MNint64 i) →
      v = Vlong i ∨ v = Vundef.

    Lemma ncompat_inv_float v f :
      ncompat v (MNfloat f) →
      v = Vfloat f ∨ v = Vundef.

    Lemma ncompat_inv_single v f :
      ncompat v (MNsingle f) →
      v = Vsingle f ∨ v = Vundef.

    Definition compat_fun (v:val) : mach_num :=
      match v with
      | Vptr _ i | Vint i => MNint i
      | Vlong l => MNint64 l
      | Vundef => MNint Int.zero
      | Vfloat f => MNfloat f
      | Vsingle f => MNsingle f
      end.

    Lemma ncompat_compat_fun v :
      ncompat v (compat_fun v).

    Ltac ncompat_inv H :=
      match type of H with
             | ncompat ?v (MNint ?i) =>
               destruct (ncompat_inv_int v i H) as [?|[(? & ?)|?]];
               clear H
             | ncompat ?v (MNint64 ?i) =>
               destruct (ncompat_inv_int64 v i H) as [?|?];
               clear H
             | ncompat ?v (MNfloat ?i) =>
               destruct (ncompat_inv_float v i H) as [?|?];
               clear H
             | ncompat ?v (MNsingle ?i) =>
               destruct (ncompat_inv_single v i H) as [?|?];
               clear H
             end.

    Definition wtype_num (v:mach_num) (tp: typ) : Prop :=
      match v, tp with
        | MNint _, (VI|VP|VIP)
        | MNint64 _, VL
        | MNfloat _, VF
        | MNsingle _, VS => True
        | _, _ => False
      end.

    Definition compat (ρC:T.elt -> val) (ρ:var -> mach_num) : Prop :=
      forall c, ncompat (ρC c) (ρ (elt2p c)).

    Variable ρC: T.elt -> val.
    Variable ρ: var -> mach_num.

    Variable Hcompat: compat ρC ρ.
    Hint Constructors is_bool.

    Lemma val_cmp_exists_int: forall c i1 i2,
      exists i,
        Val.cmp c (Vint i1) (Vint i2) = Vint i /\
        of_bool (Int.cmp c i1 i2) = (MNint i).

    Lemma val_cmpu_exists_int: forall f c i1 i2,
      exists i,
        Val.cmpu f c (Vint i1) (Vint i2) = Vint i /\
        of_bool (Int.cmpu c i1 i2) = MNint i.

    Lemma val_cmpf_exists_int: forall c f1 f2,
      exists i,
        Val.cmpf c (Vfloat f1) (Vfloat f2) = Vint i /\
        of_bool (Float.cmp c f1 f2) = MNint i.

    Lemma val_cmpfs_exists_int: forall c f1 f2,
      exists i,
        Val.cmpfs c (Vsingle f1) (Vsingle f2) = Vint i /\
        of_bool (Float32.cmp c f1 f2) = MNint i.

    Lemma val_of_bool_exists_int: forall b,
      exists i,
        Val.of_bool b = Vint i /\
        of_bool b = MNint i.

    Lemma ncompat_Vundef: forall n, ncompat Vundef n.
    Hint Resolve ncompat_Vundef.

    Lemma exist_ncompat_Vundef: forall P,
      (exists n, P n) ->
      exists n : mach_num, ncompat Vundef n /\ P n.

    Lemma exist_ncompat_Vint: forall (P:mach_num -> Prop) i,
      P (MNint i) ->
      exists n : mach_num, ncompat (Vint i) n /\ P n.

    Lemma exist_ncompat_Vptr: forall (P:mach_num -> Prop) b i,
      P (MNint i) ->
      exists n : mach_num, ncompat (Vptr b i) n /\ P n.

    Lemma exist_ncompat_Vlong: forall (P:mach_num -> Prop) l,
      P (MNint64 l) ->
      exists n : mach_num, ncompat (Vlong l) n /\ P n.

    Lemma exist_ncompat_Vfloat: forall (P:mach_num -> Prop) f,
      P (MNfloat f) ->
      exists n : mach_num, ncompat (Vfloat f) n /\ P n.

    Lemma exist_ncompat_Vsingle: forall (P:mach_num -> Prop) f,
      P (MNsingle f) ->
      exists n : mach_num, ncompat (Vsingle f) n /\ P n.

    Lemma of_bool_MNint : forall b,
      exists i, of_bool b = MNint i.

    Hypothesis block_of_ablock_inj :
      ∀ ab₁ b₁ ab₂ b₂,
        block_of_ablock ge ((tmp, ε) :: σ) ab₁ = Some b₁ →
        block_of_ablock ge ((tmp, ε) :: σ) ab₂ = Some b₂ →
        ab₁ ≠ ab₂ →
        b₁ ≠ b₂.

    Lemma nconvert_correct: ∀ e,
      ∀ v, eval_pexpr ge m ρC ε e v ->
      ∀ pt (PT: ρC ∈ points_to_gamma ge ((tmp, ε) :: σ) pt) lme,
        am_get (nconvert pt e) = Some lme →
      v ≠ Vundef →
      ∃ e', In e' lme ∧
      exists n, ncompat v n /\
                eval_mexpr ρ e' n /\
                wtype_num n (pexpr_get_ty e).

    Lemma is_valid_ptr_valid (NM: ρ ∈ γ nm) weak bs off :
      is_valid_ptr weak bs off = true →
      ∀ ab, BlockSet.mem ab bs = true →
      ∀ b, block_of_ablock ge ((tmp, ε) :: σ) ab = Some b →
      ∀ i, eval_mexpr ρ off (MNint i) →
           (if weak
           then Mem.weak_valid_pointer m b (Int.unsigned i)
           else Mem.valid_pointer m b (Int.unsigned i)) = true.

    Fixpoint nconvert_def_pre (pe: pexpr T.elt) : Prop :=
      match pe with
      | PEvar v ty => ρC(v) ∈ γ ty
      | PElocal i => ε(i) ≠ None
      | PEconst (Oaddrsymbol i _) _ _ => Genv.find_symbol ge i ≠ None
      | PEconst _ _ _ => True
      | PEunop u pe' _ _ =>
        nconvert_def_pre pe'
      | PEbinop b pe1 pe2 _ _ =>
        nconvert_def_pre pe1 ∧
        nconvert_def_pre pe2
      end.

    Lemma wtype_num_VI {n} :
      wtype_num n VI → ∃ i, n = MNint i.

    Lemma wtype_num_VP {n} :
      wtype_num n VP → ∃ i, n = MNint i.

    Lemma wtype_num_VIP {n} :
      wtype_num n VIP → ∃ i, n = MNint i.

    Lemma wtype_num_VF {n} :
      wtype_num n VF → ∃ f, n = MNfloat f.

    Lemma wtype_num_VS {n} :
      wtype_num n VS → ∃ s, n = MNsingle s.

    Lemma wtype_num_VL {n} :
      wtype_num n VL → ∃ l, n = MNint64 l.

    Ltac wtype_num_inv :=
      repeat match goal with
             | H : wtype_num _ VI |- _ => apply wtype_num_VI in H
             | H : wtype_num _ VP |- _ => apply wtype_num_VP in H
             | H : wtype_num _ VIP |- _ => apply wtype_num_VIP in H
             | H : wtype_num _ VF |- _ => apply wtype_num_VF in H
             | H : wtype_num _ VS |- _ => apply wtype_num_VS in H
             | H : wtype_num _ VL |- _ => apply wtype_num_VL in H
             end.

    Lemma wtype_of_bool {b} :
      wtype_num (of_bool b) VI.
    Local Hint Resolve wtype_of_bool.

    Lemma nconvert_eval_mexpr (NM: ρ ∈ γ nm) pt (PT: ρC ∈ points_to_gamma ge ((tmp, ε) :: σ) pt) pe :
      nconvert_def_pre pe →
      ∀ lme, am_get (nconvert pt pe) = Some lme →
      lme ≠ nil ∧
      ∀ ne, In ne lme → ¬ error_mexpr ρ ne →
      ∃ n, n ∈ eval_mexpr ρ ne ∧ wtype_num n (pexpr_get_ty pe).

    Lemma nconvert_def (NM: ρ ∈ γ nm) pt (PT: ρC ∈ points_to_gamma ge ((tmp, ε) :: σ) pt) pe :
      nconvert_def_pre pe →
      ∀ lme,
        am_get (nconvert pt pe) = Some lme →
        (∀ ne, In ne lme → ¬ error_mexpr ρ ne) →
        ¬ error_pexpr ge m ρC ε pe.

  End nconvert.

  Import Utf8.

  Local Instance TeltEqDec : EqDec T.elt := T.elt_eq.
  Lemma compat_upd var `{EQ: EqDec var} f ρC ρ :
    (∀ x y, x ≠ y → f x ≠ f y) →
    compat var f ρC ρ →
    ∀ x v n ρC',
      ncompat v n →
      ρC' ∈ upd_spec ρC x v →
      compat var f ρC' (upd ρ (f x) n).

End Nconvert.