Module IdealEnvToMachineEnv

Require Import Utf8.
Require Import Coqlib FastArith.
Require Import AbIdealEnv IdealExpr.
Require Import AbMachineEnv.
Require Import Integers.
Require Import FloatLib FloatIntervals ZIntervals IdealIntervals.
Require Import ZArith.
Require Import Cminor Ctypes.
Require Import AdomLib.
Require Import Maps ShareTree TreeAl Util Hash ToString Sets.
Require Import FactMsgHelpers.

Open Scope Z_scope.

Definition var0 := Cells.cell.

Section Functor.
  Context (abt abt_iter:Type) {IdD : ab_ideal_env_nochan abt abt_iter}.

  Inductive related : mach_num -> ideal_num -> Prop :=
  | rel_int : forall x, related (MNint (Int.repr x)) (INz x)
  | rel_long : forall x, related (MNint64 (Int64.repr x)) (INz x)
  | rel_float : forall x, related (MNfloat x) (INf x)
  | rel_single : forall x, related (MNsingle x) (INf (Float.of_single x)).

  Hint Constructors related.

  Lemma related_unsigned:
    forall x, related (MNint x) (INz (Int.unsigned x)).

  Lemma related_signed:
    forall x, related (MNint x) (INz (Int.signed x)).

  Lemma related_unsigned_long:
    forall x, related (MNint64 x) (INz (Int64.unsigned x)).

  Lemma related_signed_long:
    forall x, related (MNint64 x) (INz (Int64.signed x)).

  Instance gamma_mach : gamma_op abt (var0 -> mach_num) :=
    fun v ρ =>
      ∃ ρ':var -> ideal_num,
        ρ' ∈ γ v ∧ ∀ id, related (ρ id) (ρ' (Real id)).

  Instance gamma_mach_iter : gamma_op abt_iter (var0 -> mach_num) :=
    fun v ρ =>
      ∃ ρ':var -> ideal_num,
        ρ' ∈ γ v ∧ ∀ id, related (ρ id) (ρ' (Real id)).

  Definition typesmap := Cells.ACTree.t (option signedness * mach_num_ty).

  Instance gamma_typs : gamma_op typesmap (var0 -> mach_num) :=
    fun typs ρ =>
      ∀ v t, Cells.ACTree.get v typs = Some t ->
             match snd t with MNTfloat | MNTsingle => fst t = None | _ => True end /\
             ρ v ∈ γ (snd t).

  Record ghosts_info : Type := {
    next_g: positive;
    typs_g: PTree.t ideal_num_ty
  }.

  Definition init_ghost_info := {| next_g := 1; typs_g := PTree.empty _ |}.

  Definition compat_gh (gi:ghosts_info) (ρ1 ρ2:var -> ideal_num) :=
    (∀ id, ρ1 (Real id) = ρ2 (Real id)) /\
    (∀ g, (g < gi.(next_g))%positive -> ρ1 (Ghost g) = ρ2 (Ghost g)).

  Lemma compat_gh_refl:
    ∀ next_g ρ, compat_gh next_g ρ ρ.
  Hint Resolve compat_gh_refl.

  Lemma compat_gh_trans:
    ∀ gi1 gi2 ρ1 ρ2 ρ3,
      (gi1.(next_g) <= gi2.(next_g))%positive ->
      compat_gh gi1 ρ1 ρ2 ->
      compat_gh gi2 ρ2 ρ3 ->
      compat_gh gi1 ρ1 ρ3.
  Hint Resolve compat_gh_trans.

  Instance gamma_gh : gamma_op ghosts_info (var -> ideal_num) :=
    fun gi ρ =>
      ∀ p ty, PTree.get p gi.(typs_g) = Some ty -> ρ (Ghost p) ∈ γ ty.

  Lemma gamma_gh_init:
    ∀ ρ, ρ ∈ γ init_ghost_info.
  Hint Resolve gamma_gh_init.

  Definition signed_itv := ZITV Int.min_signed Int.max_signed.

  Lemma signed_itv_correct:
    ∀ x, Int.signed x ∈ γ signed_itv.

  Definition unsigned_itv :=
    ZITV F0 Int.max_unsigned.

  Lemma unsigned_itv_correct:
    ∀ x, Int.unsigned x ∈ γ unsigned_itv.

  Definition signed64_itv :=
    ZITV Int64.min_signed Int64.max_signed.

  Lemma signed64_itv_correct:
    ∀ x, Int64.signed x ∈ γ signed64_itv.

  Definition unsigned64_itv :=
    ZITV F0 Int64.max_unsigned.

  Lemma unsigned64_itv_correct:
    ∀ x, Int64.unsigned x ∈ γ unsigned64_itv.

  Definition alias_sz : Z := 100000.
  Opaque alias_sz.

  Definition simplify_expr_alias (v:abt+⊥) (e:iexpr) (gi:ghosts_info):
    iexpr*abt+⊥*ghosts_info :=
    let e := simplify_expr e in
    if Z.leb (iexpr_sz e) alias_sz then (e, v, gi)
    else
      (IEvar (iexpr_ty e) (Ghost gi.(next_g)),
       do v <- v;
       idnc_assign (Ghost gi.(next_g)) e v,
       {| next_g := Pos.succ gi.(next_g);
          typs_g := PTree.set gi.(next_g) (iexpr_ty e) gi.(typs_g) |}).

  Lemma simplify_expr_alias_correct:
    ∀ v e gi,
    ∀ e' v' gi', simplify_expr_alias v e gi = (e', v', gi') ->
    ∀ ρ x, ρ ∈ γ v -> ρ ∈ γ gi ->
          (∀ ρ', compat_gh gi ρ ρ' -> eval_iexpr ρ' e x ) ->
    ∃ ρ', compat_gh gi ρ ρ' /\ ρ' ∈ γ v' /\ ρ' ∈ γ gi' /\
          (∀ ρ'', compat_gh gi' ρ' ρ'' -> eval_iexpr ρ'' e' x).

  Lemma simplify_expr_alias_monotone:
    ∀ v e gi,
    ∀ e' v' gi',
      simplify_expr_alias v e gi = (e', v', gi') ->
      (gi.(next_g) <= gi'.(next_g))%positive.

  Definition itv_normalizer (i:zitv+⊤+⊥) (min max:Zfast) (logdiv:Zfast): option Zfast :=
    match i with
    | NotBot (Just (ZITV a b)) =>
      if Zfasteqb (Zfastshr (Zfastsub b a) logdiv) F0 then
        let q := Zfastshr (Zfastsub a min) logdiv in
        if Zfastleb (Zfastsub b (Zfastshl q logdiv)) max
        then Some q
        else None
      else None
    | _ => None
    end.

  Lemma itv_normalizer_correct:
    ∀ i (min max logdiv:Z), 0 < logdiv ->
    ∀ q, itv_normalizer i min max logdiv = Some q ->
    ∀ n, n ∈ γ i -> min <= n - q * 2 ^ logdiv <= max.

  Definition normalize_expr (v:abt+⊥) (e:iexpr) (min max:Zfast)
                            (logdiv:Zfast) (gi:ghosts_info):
    iexpr*abt+⊥*ghosts_info*bool :=
    let '(e, v, gi) := simplify_expr_alias v e gi in
    match v with
    | NotBot v =>
      let itv :=
        do x <- (idnc_get_query_chan v).(AbIdealEnv.get_itv) e;
        in_z x
      in
      match itv_normalizer itv min max logdiv with
      | Some q =>
        let e :=
          if Zfasteqb q F0 then e
          else
            let shift := Zfastshl q logdiv in
            IEbinop IOsub e (IEconst (INz shift))
        in
        (e, NotBot v, gi, true)
      | None => (e, NotBot v, gi, false)
      end
    | Bot => (e, v, gi, false)
    end.

  Lemma normalize_expr_correct:
    ∀ v e (min max logdiv:Z) gi, 0 < logdiv ->
    ∀ e' v' gi' b, normalize_expr v e min max logdiv gi = (e', v', gi', b) ->
    ∀ ρ (x:Z), ρ ∈ γ v -> ρ ∈ γ gi ->
      (∀ ρ', compat_gh gi ρ ρ' -> eval_iexpr ρ' e (INz x)) ->
      ∃ ρ', compat_gh gi ρ ρ' /\ ρ' ∈ γ v' /\ ρ' ∈ γ gi' /\
        if b then
          ∃ (x':Z), min <= x' <= max ∧ Int.eqmod (two_p logdiv) x x' /\
                (∀ ρ'', compat_gh gi' ρ' ρ'' -> eval_iexpr ρ'' e' (INz x'))
        else
          ∀ ρ'', compat_gh gi' ρ' ρ'' -> eval_iexpr ρ'' e' (INz x).

  Lemma normalize_expr_next_g_monotone:
    ∀ v e min max logdiv gi e' v' gi' b,
      normalize_expr v e min max logdiv gi = (e', v', gi', b) ->
      (gi.(next_g) <= gi'.(next_g))%positive.

  Definition intrange := (Int.min_signed:Zfast, Int.max_signed:Zfast).
  Definition intrangeu := (F0:Zfast, Int.max_unsigned:Zfast).
  Definition intzwordsize : Zfast := Int.zwordsize.
  Definition normalize_expr_signedness (v:abt+⊥) (e:iexpr) (f:signedness) (gi:ghosts_info):
    iexpr * abt+⊥ * ghosts_info :=
    let '(min, max) :=
      match f with Signed => intrange | Unsigned => intrangeu end
    in
    match normalize_expr v e min max intzwordsize gi with
    | (e, v, ng, true) => (e, v, ng)
    | _ => (IEZitv (ZITV min max), v, gi)
    end.

  Lemma normalize_expr_signedness_correct:
    ∀ v e f,
    ∀ ρ (x:Z) gi, ρ ∈ γ v -> ρ ∈ γ gi ->
    (∀ ρ', compat_gh gi ρ ρ' -> eval_iexpr ρ' e (INz x)) ->
    ∀ e' v' gi', normalize_expr_signedness v e f gi = (e', v', gi') ->
    ∃ ρ', compat_gh gi ρ ρ' /\ ρ' ∈ γ v' /\ ρ' ∈ γ gi' /\
    ∃ (x':Z),
      x' ∈ γ (match f with Signed => signed_itv | Unsigned => unsigned_itv end) ∧
      Int.eqm x x' ∧
      (∀ ρ'', compat_gh gi' ρ' ρ'' -> eval_iexpr ρ'' e' (INz x')).

  Lemma normalize_expr_signedness_next_g_monotone:
    ∀ v e f gi e' v' gi',
      normalize_expr_signedness v e f gi = (e', v', gi') ->
      (gi.(next_g) <= gi'.(next_g))%positive.

  Definition int64range := (Int64.min_signed:Zfast, Int64.max_signed:Zfast).
  Definition int64rangeu := (F0:Zfast, Int64.max_unsigned:Zfast).
  Definition int64zwordsize : Zfast := Int64.zwordsize.
  Definition normalize_expr_signedness64 (v:abt+⊥) (e:iexpr) (f:signedness) (gi:ghosts_info):
    iexpr * abt+⊥ * ghosts_info :=
    let '(min, max) :=
      match f with Signed => int64range | Unsigned => int64rangeu end
    in
    match normalize_expr v e min max int64zwordsize gi with
    | (e, v, ng, true) => (e, v, ng)
    | _ => (IEZitv (ZITV min max), v, gi)
    end.

  Lemma normalize_expr_signedness64_correct:
    ∀ v e f,
    ∀ ρ (x:Z) gi, ρ ∈ γ v -> ρ ∈ γ gi ->
              (∀ ρ', compat_gh gi ρ ρ' -> eval_iexpr ρ' e (INz x)) ->
    ∀ e' v' gi', normalize_expr_signedness64 v e f gi = (e', v', gi') ->
    ∃ ρ', compat_gh gi ρ ρ' /\ ρ' ∈ γ v' /\ ρ' ∈ γ gi' /\
    ∃ (x':Z),
      x' ∈ γ (match f with Signed => signed64_itv | Unsigned => unsigned64_itv end) ∧
      Int64.eqm x x' ∧
      (∀ ρ'', compat_gh gi' ρ' ρ'' -> eval_iexpr ρ'' e' (INz x')).

  Lemma normalize_expr_signedness64_next_g_monotone:
    ∀ v e f gi e' v' gi',
      normalize_expr_signedness64 v e f gi = (e', v', gi') ->
      (gi.(next_g) <= gi'.(next_g))%positive.

  Definition assume_cmp (c:comparison) (e:iexpr) (z:Zfast) (v:abt+⊥): abt+⊥ :=
    do v <- v;
    idnc_assume (IEbinop (IOcmp c) e (IEconst (INz z))) true v.

  Lemma assume_cmp_correct:
    ∀ c e (x:Z) z ρ ab,
      ρ ∈ γ ab ->
      INz x ∈ eval_iexpr ρ e ->
      Zcmp c x z = true ->
      ρ ∈ γ (assume_cmp c e z ab).

  Definition check_finitef (e:iexpr) (v:abt+⊥): bool :=
    match v with
    | Bot => true
    | NotBot v =>
      is_bot (idnc_assume
                (IEbinop (IOcmpf Cgt) e (IEconst (INf (B754_infinity true)))) false v) &&
      is_bot (idnc_assume
                (IEbinop (IOcmpf Clt) e (IEconst (INf (B754_infinity false)))) false v)
    end.

  Lemma check_finitef_correct:
    ∀ e x ρ ab,
      check_finitef e ab = true ->
      ρ ∈ γ ab ->
      INf x ∈ eval_iexpr ρ e ->
      is_finite x = true.

  Fixpoint convert_expr (e:mexpr var0) (v:abt+⊥) (nerr:bool) (gi:ghosts_info) :
    (iexpr * abt+⊥ * bool * ghosts_info) :=
    match e with
    | MEvar (MNTint | MNTint64) x => (IEvar INTz (Real x), v, nerr, gi)
    | MEvar (MNTfloat | MNTsingle) x => (IEvar INTf (Real x), v, nerr, gi)
    | MEconst (MNint i) => (IEconst (INz (Int.signed i)), v, nerr, gi)
    | MEconst (MNint64 i) => (IEconst (INz (Int64.signed i)), v, nerr, gi)
    | MEconst (MNfloat f) => (IEconst (INf f), v, nerr, gi)
    | MEconst (MNsingle f) => (IEconst (INf (Float.of_single f)), v, nerr, gi)

    | MEunop op e =>
      let '(e, v, nerr, gi) := convert_expr e v nerr gi in
      match op with
      | Ocast8unsigned =>
        match normalize_expr v e F0 F255 F8 gi with
          | (e, v, gi, true) => (e, v, nerr, gi)
          | _ => (IEZitv (ZITV F0 F255), v, nerr, gi)
        end
      | Ocast8signed =>
        match normalize_expr v e (-128) 127 F8 gi with
          | (e, v, gi, true) => (e, v, nerr, gi)
          | _ => (IEZitv (ZITV (-128) 127), v, nerr, gi)
        end
      | Ocast16unsigned =>
        match normalize_expr v e F0 65535 F16 gi with
          | (e, v, gi, true) => (e, v, nerr, gi)
          | _ => (IEZitv (ZITV F0 65535), v, nerr, gi)
        end
      | Ocast16signed =>
        match normalize_expr v e (-32768) 32767 F16 gi with
          | (e, v, gi, true) => (e, v, nerr, gi)
          | _ => (IEZitv (ZITV (-32768) 32767), v, nerr, gi)
        end
      | Olongofint =>
        let '(e, v, gi) := normalize_expr_signedness v e Signed gi in
        (e, v, nerr, gi)
      | Olongofintu =>
        let '(e, v, gi) := normalize_expr_signedness v e Unsigned gi in
        (e, v, nerr, gi)
      | Ointoflong => (e, v, nerr, gi)

      | Onegint => (IEunop IOneg e, v, nerr, gi)
      | Onotint => (IEunop IOnot e, v, nerr, gi)

      | Onegl => (IEunop IOneg e, v, nerr, gi)
      | Onotl => (IEunop IOnot e, v, nerr, gi)

      | Onegf | Onegfs => (IEunop IOnegf e, v, nerr, gi)
      | Oabsf | Oabsfs => (IEunop IOabsf e, v, nerr, gi)
      | Ofloatofsingle => (e, v, nerr, gi)
      | Osingleoffloat => (IEunop IOsingleoffloat e, v, nerr, gi)
      | Ointoffloat | Ointofsingle =>
        let '(e, v, gi) := simplify_expr_alias v e gi in
        let e' := IEunop IOzoffloat e in
        let nerr := nerr &&
          check_finitef e v &&
          is_bot (assume_cmp Clt e' (fst intrange) v) &&
          is_bot (assume_cmp Cgt e' (snd intrange) v)
        in
        (e', v, nerr, gi)
      | Ointuoffloat | Ointuofsingle =>
        let '(e, v, gi) := simplify_expr_alias v e gi in
        let e' := IEunop IOzoffloat e in
        let nerr := nerr &&
          check_finitef e v &&
          is_bot (assume_cmp Clt e' F0 v) &&
          is_bot (assume_cmp Cgt e' (snd intrangeu) v)
        in
        (e', v, nerr, gi)
      | Ofloatofint =>
        let '(e, v, gi) := normalize_expr_signedness v e Signed gi in
        (IEunop IOfloatofz e, v, nerr, gi)
      | Osingleofint =>
        let '(e, v, gi) := normalize_expr_signedness v e Signed gi in
        (IEunop IOsingleofz e, v, nerr, gi)
      | Ofloatofintu =>
        let '(e, v, gi) := normalize_expr_signedness v e Unsigned gi in
        (IEunop IOfloatofz e, v, nerr, gi)
      | Osingleofintu =>
        let '(e, v, gi) := normalize_expr_signedness v e Unsigned gi in
        (IEunop IOsingleofz e, v, nerr, gi)
      | Olongoffloat | Olongofsingle =>
        let '(e, v, gi) := simplify_expr_alias v e gi in
        let e' := IEunop IOzoffloat e in
        let nerr := nerr &&
          check_finitef e v &&
          is_bot (assume_cmp Clt e' (fst int64range) v) &&
          is_bot (assume_cmp Cgt e' (snd int64range) v)
        in
        (e', v, nerr, gi)
      | Olonguoffloat | Olonguofsingle =>
        let '(e, v, gi) := simplify_expr_alias v e gi in
        let e' := IEunop IOzoffloat e in
        let nerr := nerr &&
          check_finitef e v &&
          is_bot (assume_cmp Clt e' F0 v) &&
          is_bot (assume_cmp Cgt e' (snd int64rangeu) v)
        in
        (e', v, nerr, gi)
      | Ofloatoflong =>
        let '(e, v, gi) := normalize_expr_signedness64 v e Signed gi in
        (IEunop IOfloatofz e, v, nerr, gi)
      | Ofloatoflongu =>
        let '(e, v, gi) := normalize_expr_signedness64 v e Unsigned gi in
        (IEunop IOfloatofz e, v, nerr, gi)
      | Osingleoflong =>
        let '(e, v, gi) := normalize_expr_signedness64 v e Signed gi in
        (IEunop IOsingleofz e, v, nerr, gi)
      | Osingleoflongu =>
        let '(e, v, gi) := normalize_expr_signedness64 v e Unsigned gi in
        (IEunop IOsingleofz e, v, nerr, gi)
      end

    | MEbinop op e1 e2 =>
      let '(e1, v, nerr, gi) := convert_expr e1 v nerr gi in
      let '(e2, v, nerr, gi) := convert_expr e2 v nerr gi in
      match op with
      | Ocmp c =>
        let '(e1, v, gi) := normalize_expr_signedness v e1 Signed gi in
        let '(e2, v, gi) := normalize_expr_signedness v e2 Signed gi in
        (IEbinop (IOcmp c) e1 e2, v, nerr, gi)
      | Ocmpu c =>
        let '(e1, v, gi) := normalize_expr_signedness v e1 Unsigned gi in
        let '(e2, v, gi) := normalize_expr_signedness v e2 Unsigned gi in
        (IEbinop (IOcmp c) e1 e2, v, nerr, gi)
      | Ocmpl c =>
        let '(e1, v, gi) := normalize_expr_signedness64 v e1 Signed gi in
        let '(e2, v, gi) := normalize_expr_signedness64 v e2 Signed gi in
        (IEbinop (IOcmp c) e1 e2, v, nerr, gi)
      | Ocmplu c =>
        let '(e1, v, gi) := normalize_expr_signedness64 v e1 Unsigned gi in
        let '(e2, v, gi) := normalize_expr_signedness64 v e2 Unsigned gi in
        (IEbinop (IOcmp c) e1 e2, v, nerr, gi)

      | Oaddf => (IEbinop IOaddf e1 e2, v, nerr, gi)
      | Oaddfs => (IEunop IOsingleoffloat (IEbinop IOaddf e1 e2), v, nerr, gi)
      | Osubf => (IEbinop IOsubf e1 e2, v, nerr, gi)
      | Osubfs => (IEunop IOsingleoffloat (IEbinop IOsubf e1 e2), v, nerr, gi)
      | Omulf => (IEbinop IOmulf e1 e2, v, nerr, gi)
      | Omulfs => (IEunop IOsingleoffloat (IEbinop IOmulf e1 e2), v, nerr, gi)
      | Odivf => (IEbinop IOdivf e1 e2, v, nerr, gi)
      | Odivfs => (IEunop IOsingleoffloat (IEbinop IOdivf e1 e2), v, nerr, gi)
      | Ocmpf c | Ocmpfs c => (IEbinop (IOcmpf c) e1 e2, v, nerr, gi)
      | Oadd | Oaddl => (IEbinop IOadd e1 e2, v, nerr, gi)
      | Osub | Osubl => (IEbinop IOsub e1 e2, v, nerr, gi)
      | Omul | Omull => (IEbinop IOmul e1 e2, v, nerr, gi)

      | Odiv =>
        let '(e1, v, gi) := normalize_expr_signedness v e1 Signed gi in
        let '(e2, v, gi) := normalize_expr_signedness v e2 Signed gi in
        let nerr := nerr && is_bot (assume_cmp Ceq e2 F0 v) &&
          is_bot (assume_cmp Cle e1 (fst intrange) (assume_cmp Ceq e2 Fm1 v))
        in
        (IEbinop IOdiv e1 e2, v, nerr, gi)
      | Odivl =>
        let '(e1, v, gi) := normalize_expr_signedness64 v e1 Signed gi in
        let '(e2, v, gi) := normalize_expr_signedness64 v e2 Signed gi in
        let nerr := nerr && is_bot (assume_cmp Ceq e2 F0 v) &&
          is_bot (assume_cmp Cle e1 (fst int64range) (assume_cmp Ceq e2 Fm1 v))
        in
        (IEbinop IOdiv e1 e2, v, nerr, gi)
      | Odivu =>
        let '(e1, v, gi) := normalize_expr_signedness v e1 Unsigned gi in
        let '(e2, v, gi) := normalize_expr_signedness v e2 Unsigned gi in
        let nerr := nerr && is_bot (assume_cmp Ceq e2 F0 v) in
        (IEbinop IOdiv e1 e2, v, nerr, gi)
      | Odivlu =>
        let '(e1, v, gi) := normalize_expr_signedness64 v e1 Unsigned gi in
        let '(e2, v, gi) := normalize_expr_signedness64 v e2 Unsigned gi in
        let nerr := nerr && is_bot (assume_cmp Ceq e2 F0 v) in
        (IEbinop IOdiv e1 e2, v, nerr, gi)
      | Omod =>
        let '(e1, v, gi) := normalize_expr_signedness v e1 Signed gi in
        let '(e2, v, gi) := normalize_expr_signedness v e2 Signed gi in
        let nerr := nerr && is_bot (assume_cmp Ceq e2 F0 v) &&
          is_bot (assume_cmp Cle e1 (fst intrange) (assume_cmp Ceq e2 Fm1 v))
        in
        (IEbinop IOmod e1 e2, v, nerr, gi)
      | Omodl =>
        let '(e1, v, gi) := normalize_expr_signedness64 v e1 Signed gi in
        let '(e2, v, gi) := normalize_expr_signedness64 v e2 Signed gi in
        let nerr := nerr && is_bot (assume_cmp Ceq e2 F0 v) &&
          is_bot (assume_cmp Cle e1 (fst int64range) (assume_cmp Ceq e2 Fm1 v))
        in
        (IEbinop IOmod e1 e2, v, nerr, gi)
      | Omodu =>
        let '(e1, v, gi) := normalize_expr_signedness v e1 Unsigned gi in
        let '(e2, v, gi) := normalize_expr_signedness v e2 Unsigned gi in
        let nerr := nerr && is_bot (assume_cmp Ceq e2 F0 v) in
        (IEbinop IOmod e1 e2, v, nerr, gi)
      | Omodlu =>
        let '(e1, v, gi) := normalize_expr_signedness64 v e1 Unsigned gi in
        let '(e2, v, gi) := normalize_expr_signedness64 v e2 Unsigned gi in
        let nerr := nerr && is_bot (assume_cmp Ceq e2 F0 v) in
        (IEbinop IOmod e1 e2, v, nerr, gi)

      | Oand | Oandl => (IEbinop IOand e1 e2, v, nerr, gi)
      | Oor | Oorl => (IEbinop IOor e1 e2, v, nerr, gi)
      | Oxor | Oxorl => (IEbinop IOxor e1 e2, v, nerr, gi)
      | Oshl =>
        let '(e2, v, gi) := normalize_expr_signedness v e2 Unsigned gi in
        let nerr := nerr && is_bot (assume_cmp Cge e2 intzwordsize v) in
        (IEbinop IOshl e1 e2, v, nerr, gi)
      | Oshll =>
        let '(e2, v, gi) := normalize_expr_signedness v e2 Unsigned gi in
        let nerr := nerr && is_bot (assume_cmp Cge e2 int64zwordsize v) in
        (IEbinop IOshl e1 e2, v, nerr, gi)
      | Oshr =>
        let '(e1, v, gi) := normalize_expr_signedness v e1 Signed gi in
        let '(e2, v, gi) := normalize_expr_signedness v e2 Unsigned gi in
        let nerr := nerr && is_bot (assume_cmp Cge e2 intzwordsize v) in
        (IEbinop IOshr e1 e2, v, nerr, gi)
      | Oshrl =>
        let '(e1, v, gi) := normalize_expr_signedness64 v e1 Signed gi in
        let '(e2, v, gi) := normalize_expr_signedness v e2 Unsigned gi in
        let nerr := nerr && is_bot (assume_cmp Cge e2 int64zwordsize v) in
        (IEbinop IOshr e1 e2, v, nerr, gi)
      | Oshru =>
        let '(e1, v, gi) := normalize_expr_signedness v e1 Unsigned gi in
        let '(e2, v, gi) := normalize_expr_signedness v e2 Unsigned gi in
        let nerr := nerr && is_bot (assume_cmp Cge e2 intzwordsize v) in
        (IEbinop IOshr e1 e2, v, nerr, gi)
      | Oshrlu =>
        let '(e1, v, gi) := normalize_expr_signedness64 v e1 Unsigned gi in
        let '(e2, v, gi) := normalize_expr_signedness v e2 Unsigned gi in
        let nerr := nerr && is_bot (assume_cmp Cge e2 int64zwordsize v) in
        (IEbinop IOshr e1 e2, v, nerr, gi)
      end
    end.

  Lemma convert_expr_next_g_monotone:
    ∀ e v nerr gi e' v' nerr' gi',
      convert_expr e v nerr gi = (e', v', nerr', gi') ->
      (gi.(next_g) <= gi'.(next_g))%positive.

  Lemma convert_expr_ok:
    ∀ e ρ x, eval_mexpr ρ e x ->
    ∀ v ρ'1 gi, ρ'1 ∈ γ v -> ρ'1 ∈ γ gi -> (∀ id, related (ρ id) (ρ'1 (Real id))) ->
    ∀ nerr e' v' nerr' gi', convert_expr e v nerr gi = (e', v', nerr', gi') ->
    ∃ ρ'2,
      ρ'2 ∈ γ v' /\ ρ'2 ∈ γ gi' /\
      compat_gh gi ρ'1 ρ'2 /\
    ∃ x',
      (∀ ρ'3, compat_gh gi' ρ'2 ρ'3 -> eval_iexpr ρ'3 e' x') ∧
      related x x'.

  Lemma convert_expr_nerr_monotone:
    ∀ e v gi e' v' gi',
      ~convert_expr e v false gi = (e', v', true, gi').

  Ltac leb_case H :=
    match type of H with
    | context [?A <=? ?B] => pose proof Zle_cases A B; destruct (A <=? B)
    end.

  Lemma convert_expr_noerror:
    ∀ ρ e v ρ'1 gi, ρ'1 ∈ γ v -> ρ'1 ∈ γ gi ->
      (∀ id, related (ρ id) (ρ'1 (Real id))) ->
    ∀ e' v' gi', convert_expr e v true gi = (e', v', true, gi') ->
      ¬error_mexpr ρ e.

  Definition forget_temps (v:abt) (gi:ghosts_info) : abt+⊥ :=
    positive_rec _ (NotBot v)
      (fun x v => do v <- v; idnc_forget (Ghost x) v)
      gi.(next_g).

  Lemma forget_temps_correct:
    ∀ ab (ρ:var -> ideal_num) gi, ρ ∈ γ ab ->
    ρ ∈ γ (forget_temps ab gi).

  Definition get_itv (e:mexpr var0) (v:abt * typesmap) : mach_num_itv+⊥ :=
    let '(ie, v, _, gi) := convert_expr e (NotBot (fst v)) false init_ghost_info in
    do v <- v;
    do itv <- (idnc_get_query_chan v).(AbIdealEnv.get_itv) (simplify_expr ie);
      match itv, mexpr_ty e with
      | Just (Az ((ZITV a b) as itv')), MNTint =>
        NotBot (MNIint
           (match itv_normalizer (NotBot (Just itv'))
                                 (fst intrange) (snd intrangeu) intzwordsize with
           | Some q => Just (ZITV (Zfastsub a (Zfastshl q intzwordsize))
                                  (Zfastsub b (Zfastshl q intzwordsize)))
           | None => All
           end))
      | All, MNTint => NotBot (MNIint All)
      | Just (Az ((ZITV a b) as itv')), MNTint64 =>
        NotBot (MNIint64
           (match itv_normalizer (NotBot (Just itv'))
                                 (fst int64range) (snd int64rangeu) int64zwordsize with
           | Some q => Just (ZITV (Zfastsub a (Zfastshl q int64zwordsize))
                                  (Zfastsub b (Zfastshl q int64zwordsize)))
           | None => All
           end))
      | All, MNTint64 => ret (MNIint64 All)
      | Just (Af itv), MNTfloat => ret (MNIfloat (Just itv))
      | Just (Af itv), MNTsingle => ret (MNIsingle (Just itv))
      | All, MNTfloat => ret (MNIfloat All)
      | All, MNTsingle => ret (MNIsingle All)
      | _, _ => Bot
      end.

  Lemma get_itv_correct:
    ∀ e ρ ab, ρ ∈ γ ab -> eval_mexpr ρ e ⊆ γ (get_itv e ab).

  Definition forget (x:var0) (v:abt * typesmap) : (abt * typesmap)+⊥ :=
    do fstres <- idnc_forget (Real x) (fst v);
    ret (fstres, Cells.ACTree.remove x (snd v)).

  Lemma forget_correct:
    ∀ x ρ, ∀ n ab,
      ρ ∈ γ ab ->
      (upd ρ x n) ∈ γ (forget x ab).

  Fixpoint infer_var_types (e:mexpr var0) (ctx:option signedness) (typs:typesmap)
  : typesmap :=
    match e with
    | MEvar nvt x =>
      match ctx with
      | None =>
        match Cells.ACTree.get x typs with
        | None =>
          match nvt with
          | MNTfloat | MNTsingle => typs
          | _ => Cells.ACTree.set x (None, nvt) typs
          end
        | Some _ => typs
        end
      | Some _ => Cells.ACTree.set x (ctx, nvt) typs
      end
    | MEconst _ => typs
    | MEunop op e =>
      let ctx :=
        match op with
        | (Ofloatofint | Ofloatoflong | Olongofint | Osingleofint | Osingleoflong |
           Ocast16signed | Ocast8signed) => Some Signed
        | (Ofloatofintu | Ofloatoflongu | Olongofintu | Osingleofintu | Osingleoflongu |
           Ocast16unsigned | Ocast8unsigned) => Some Unsigned
        | _ => None
        end
      in
      infer_var_types e ctx typs
    | MEbinop op e1 e2 =>
      let ctx1 :=
        match op with
        | (Odiv | Omod | Odivl | Omodl | Ocmp _ | Ocmpl _ | Oshr | Oshrl) =>
          Some Signed
        | (Odivu | Omodu | Odivlu | Omodlu | Ocmpu _ | Ocmplu _ | Oshru | Oshrlu) =>
          Some Unsigned
        | _ => None
        end
      in
      let ctx2 :=
        match op with
        | (Odiv | Omod | Odivl | Omodl | Ocmp _ | Ocmpl _) => Some Signed
        | (Odivu | Omodu | Odivlu | Omodlu | Ocmpu _ | Ocmplu _ |
           Oshl | Oshr | Oshru | Oshll | Oshrl | Oshrlu) => Some Unsigned
        | _ => None
        end
      in
      (infer_var_types e2 ctx2 (infer_var_types e1 ctx1 typs))
    end.

  Lemma infer_var_types_consistent :
    ∀ ρ e nv ctx typs,
      eval_mexpr ρ e nv ->
      ρ ∈ γ typs ->
      (match nv with MNfloat _ | MNsingle _ => ctx = None | _ => True end) ->
      ρ ∈ γ (infer_var_types e ctx typs).

  Definition assign_vars_to_top (e:mexpr var0) (v:abt * typesmap) : (abt * typesmap)+⊥ :=
    let types := infer_var_types e None (Cells.ACTree.empty _) in
    Cells.ACTree.fold (fun ab v sty =>
      do (ab, typs) <- ab;
      match sty with
      | (Some s, ty) =>
        let typs := Cells.ACTree.set v sty typs in
        match get_itv (MEvar ty v) (ab, typs) with
        | NotBot (MNIint All) | NotBot (MNIint64 All) =>
          do ab <- (idnc_assign (Real v) (IEZitv
                 (match s, ty with
                  | Signed, MNTint => signed_itv
                  | Unsigned, MNTint => unsigned_itv
                  | Signed, MNTint64 => signed64_itv
                  | Unsigned, MNTint64 => unsigned64_itv
                  | _, _ => signed_itv
                  end)) ab);
          ret (ab, typs)
        | _ => ret (ab, typs)
        end
      | (None, _) =>
        let typs :=
          match Cells.ACTree.get v typs with
          | None => Cells.ACTree.set v sty typs
          | Some _ => typs
          end
        in
        ret (ab, typs)
      end)
     types (NotBot v).

  Lemma assign_vars_to_top_correct:
    forall ab e ρ v,
      eval_mexpr ρ e v ->
      γ ab ρ -> γ (assign_vars_to_top e ab) ρ.

  Definition assign (x:var0) (e:mexpr var0) (v:abt*typesmap) : (abt*typesmap)+⊥ :=
    let v := assign_vars_to_top e v in
    do (v, typs) <- v;
    let '(e', v, _, gi) := convert_expr e (NotBot v) false init_ghost_info in
    do v <- v;
    let ty := mexpr_ty e in
    let typs := Cells.ACTree.set x (None, ty) typs in
    let '(v, gi) :=
    match ty with
    | MNTint =>
      match normalize_expr (NotBot v) e'
                           (fst intrange) (snd intrangeu) intzwordsize gi with
      | (e, v, gi, true) =>
        (do v <- v; idnc_assign (Real x) e v, gi)
      | _ =>
        (idnc_forget (Real x) v, gi)
      end
    | MNTint64 =>
      match normalize_expr (NotBot v) e'
                           (fst int64range) (snd int64rangeu) int64zwordsize gi with
      | (e, v, gi, true) =>
        (do v <- v; idnc_assign (Real x) e v, gi)
      | _ =>
        (idnc_forget (Real x) v, gi)
      end
    | MNTfloat | MNTsingle =>
      (let e := simplify_expr e' in idnc_assign (Real x) e v, gi)
    end
    in
    do v <- v;
    do v <- forget_temps v gi;
    ret (v, typs).

  Lemma assign_correct:
    ∀ x e ρ, ∀ n ab,
      ρ ∈ γ ab ->
      n ∈ eval_mexpr ρ e ->
      (upd ρ x n) ∈ γ (assign x e ab).

  Definition assume (e:mexpr var0) (b:bool) (v:abt * typesmap) : (abt*typesmap)+⊥ :=
    let v := assign_vars_to_top e v in
    do (v, typs) <- v;
    let '(e, v, _, gi) := convert_expr e (NotBot v) false init_ghost_info in
    do v <- v;
    match normalize_expr (NotBot v) e (fst intrange) (snd intrangeu) intzwordsize gi with
    | (e, v, gi, true) =>
      do v <- v;
      do v <- idnc_assume e b v;
      do v <- forget_temps v gi;
      ret (v, typs)
    | _ =>
      do v <- forget_temps v gi;
      ret (v, typs)
    end.

  Lemma assume_correct:
    ∀ e ρ ab b,
      ρ ∈ γ ab ->
      of_bool b ∈ eval_mexpr ρ e ->
      ρ ∈ γ (assume e b ab).

  Definition noerror (e:mexpr var0) (v:abt * typesmap) : bool :=
    let '(_, _, nerr, _) := convert_expr e (NotBot (fst v)) true init_ghost_info in
    nerr.

  Lemma noerror_correct:
    ∀ e ρ ab,
      ρ ∈ γ ab ->
      noerror e ab = true ->
      error_mexpr ρ e ->
      False.

  Function zitv_concretize_int_aux (from: Z) (nb: N) (acc: ZSet.t) {measure N.to_nat nb} : ZSet.t :=
    match nb with
    | N0 => acc
    | Npos p =>
      let nb' := Pos.pred_N p in
      zitv_concretize_int_aux (Z.succ from) nb' (ZSet.add from acc)
    end.

  Definition zitv_concretize_int (max: Nfast) (i: zitv) : ZSet.t+⊤+⊥ :=
    match i with
    | ZITV m M =>
      if Zfastleb m M then
        let n := Nfast_of_Zfast (Zfastsub M m) in
        if Nfastleb n max
        then NotBot (Just (zitv_concretize_int_aux m (N.succ n) ZSet.empty))
        else NotBot All
      else Bot
    end.

  Lemma zitv_concretize_int_correct:
    ∀ itv max z, γ itv z ->
      match zitv_concretize_int max itv with
      | NotBot (Just ab) => ZSet.mem z ab
      | NotBot All => True
      | Bot => False
      end.

  Definition concretize_int (max: N) (e: mexpr var0) (ab: abt*typesmap) : ZSet.t+⊤+⊥ :=
    let ab := fst ab in
    let '(e, ab, _, gi) := convert_expr e (NotBot ab) false init_ghost_info in
    do ab <- ab;
    let e := simplify_expr e in
    let c := idnc_get_query_chan ab in
    do cong <- c.(get_congr) e;
    let '{| ZCongruences_defs.zc_rem := rem; ZCongruences_defs.zc_mod := modn |} := cong in
    let modz := Zfast_of_Nfast modn in
    if Nfastleb modn F0 then ret (Just (ZSetOp.singleton (Int.unsigned (Int.repr rem))))
    else
      do itv <- c.(AbIdealEnv.get_itv) e;
      do itv <- in_z itv;
      match itv with
      | All => ret All
      | Just (ZITV a b) =>
        let modn := Zfast_of_Nfast modn in
        let itvdiv := ZITV (Zfastopp (Zfastdiv (Zfastsub rem a) modn))
                           (Zfastdiv (Zfastsub b rem) modn) in
        do set <- zitv_concretize_int max itvdiv;
        ret (fmap (ZSetOp.map
           (fun x => Int.unsigned (Int.repr (Zfastadd (Zfastmul x modn) rem)))) set)
      end.

  Lemma concretize_int_correct :
    ∀ max e ρ ab, ρ ∈ γ ab ->
      (eval_mexpr ρ e ∘ MNint) ⊆ γ (concretize_int max e ab).

  Program Definition transfer_types (v2:abt) (typs1 typs2:typesmap) : abt :=
    let typs := Cells.ACTree.shcombine_diff (fun _ s1 s2 =>
      match s1, s2 return _ with
      | Some (Some s, MNTint), Some (None, MNTint) =>
        Some (Some s, MNTint)
      | Some (Some s, MNTint64), Some (None, MNTint64) =>
        Some (Some s, MNTint64)
      | _, _ => None
      end) _ typs1 typs2
    in
    Cells.ACTree.fold (fun ab x sty =>
              match sty return _ with
              | (Some s, ty) =>
                match get_itv (MEvar ty x) (ab, typs2) return _ with
                | (NotBot (MNIint All)) | NotBot (MNIint64 All) =>
                  match idnc_assign (Real x) (IEZitv
                               (match s, ty return _ with
                                | Signed, MNTint => signed_itv
                                | Unsigned, MNTint => unsigned_itv
                                | Signed, MNTint64 => signed64_itv
                                | Unsigned, MNTint64 => unsigned64_itv
                                | _, _ => signed_itv
                                end)) ab
                        return _
                  with Bot => ab
                  | NotBot ab => ab
                  end
                | _ => ab
                end
              | _ => ab
              end)
           typs v2.

  Lemma transfer_types_correct:
    ∀ typs1 typs2 v2 (ρ:var0 -> mach_num),
      ρ ∈ γ (v2, typs2) ->
      ρ ∈ γ (transfer_types v2 typs1 typs2).

  Program Definition join_typs (typs1 typs2:typesmap) : typesmap :=
    Cells.ACTree.shcombine (fun _ s1 s2 =>
      match s1, s2 return _ with
      | Some (Some Signed, MNTint), Some (Some Signed | None, MNTint)
      | Some (Some Signed, MNTint64), Some (Some Signed | None, MNTint64)
      | Some (Some Unsigned, MNTint), Some (Some Unsigned | None, MNTint)
      | Some (Some Unsigned, MNTint64), Some (Some Unsigned | None, MNTint64)
        => s1
      | Some (None, MNTint), Some (Some Signed, MNTint)
      | Some (None, MNTint64), Some (Some Signed, MNTint64)
      | Some (None, MNTint), Some (Some Unsigned, MNTint)
      | Some (None, MNTint64), Some (Some Unsigned, MNTint64)
        => s2
      | Some (Some _, MNTfloat), Some (Some _, MNTfloat)
      | Some (Some _, MNTsingle), Some (Some _, MNTsingle)
      | Some (None, MNTint), Some (None, MNTint)
      | Some (None, MNTint64), Some (None, MNTint64)
      | Some (None, MNTfloat), Some (None, MNTfloat)
      | Some (None, MNTsingle), Some (None, MNTsingle)
        => s1
      | _, _ => None
      end) _ typs1 typs2.

  Lemma join_typs_correct:
    ∀ a b, γ a ∪ γ b ⊆ γ (join_typs a b).

  Instance top_ietme : top_op ((abt * typesmap)+⊥) :=
    do t <- top;
    ret (t, Cells.ACTree.empty _).

  Program Instance leb_ietme : leb_op (abt * typesmap) := fun ab1 ab2 =>
    (fst ab1) ⊑ (fst ab2) &&
    Cells.ACTree.shforall2 (fun _ s1 s2 =>
                   match s1, s2 return _ with
                   | _, None
                   | Some (_, MNTint), Some (_, MNTint)
                   | Some (_, MNTint64), Some (_, MNTint64)
                   | Some (_, MNTsingle), Some (None, MNTsingle)
                   | Some (_, MNTfloat), Some (None, MNTfloat)
                   | Some (Some _, MNTsingle), Some (Some _, MNTsingle)
                   | Some (Some _, MNTfloat), Some (Some _, MNTfloat) => true
                   | _, _ => false
                   end) _
      (snd ab1) (snd ab2).

  Instance join_ietme : join_op (abt * typesmap) ((abt * typesmap)+⊥) := fun ab1 ab2 =>
    let ab1' := transfer_types (fst ab1) (snd ab2) (snd ab1) in
    let ab2' := transfer_types (fst ab2) (snd ab1) (snd ab2) in
    do j <- ab1' ⊔ ab2';
    ret (j, join_typs (snd ab1) (snd ab2)).

  Instance widen_ietme : widen_op (abt_iter * typesmap+⊥) ((abt * typesmap)+⊥) :=
    {| widen ab1 ab2 :=
         let '(w1, w2) := fst ab1 ▽ do (ab2, _) <- ab2; ret (ab2) in
         let typs :=
           match ab1 with
           | (_, Bot) => do (_, typs2) <- ab2; ret typs2
           | (_, NotBot typs1) =>
             match ab2 with
             | Bot => NotBot typs1
             | NotBot (_, typs2) => NotBot (join_typs typs1 typs2)
             end
           end
         in
         ((w1, typs),
          do w <- w2;
          do typs <- typs;
          ret (w, typs));
       init_iter x :=
         match x with
         | Bot => (init_iter Bot, Bot)
         | NotBot x => (init_iter (NotBot (fst x)), NotBot (snd x))
        end |}.

  Instance top_ietme_correct : top_op_correct ((abt * typesmap)+⊥) (var0->mach_num).

  Instance leb_ietme_correct : leb_op_correct (abt * typesmap) (var0->mach_num).

  Instance join_ietme_correct : join_op_correct (abt * typesmap) ((abt * typesmap)+⊥) (var0->mach_num).

  Instance widen_ietme_correct :
    widen_op_correct (abt_iter * typesmap+⊥) ((abt * typesmap)+⊥) (var0->mach_num).

  Instance idealenv_to_machineenv:
    ab_machine_env (var:=var0) (abt * typesmap) (abt_iter * typesmap+⊥) :=
    { assign := assign
    ; forget := forget
    ; assume := assume
    ; get_itv := fun e v => do v <- assign_vars_to_top e v; get_itv e v
    ; concretize_int := concretize_int
    ; noerror := noerror }.

End Functor.

Instance typesmap_TS : ToString typesmap :=
  fun _ => ""%string.

Existing Instances idealenv_to_machineenv.