Module Normalise

Require Import Coqlib.
Require Import Psatz.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Values_symbolictype.
Require Import NormaliseSpec.
Require Import IntFacts.

This module defines useful properties of the normalise function.

We axiomatise the normalise function, it will be implemented later in Values_symbolic_aux.ml.

Axiom normalise : norm_typ.
Axiom norm_correct : normalise_correct eu eb normalise.
Axiom norm_complete : normalise_complete eu eb normalise.

Definition eq_modulo_normalise (e1 e2:expr_sym) :=
forall resType sz msk, normalise sz msk e1 resType = normalise sz msk e2 resType.

Notation "x == y" := (eq_modulo_normalise x y) (at level 80).

Lemma eq_modulo_normalise_sym : forall x y, x == y -> y == x.

Proof.

  intros.
  intro.
  intros.
  elim H.
  reflexivity.
Qed.

Lemma eq_modulo_normalise_trans : forall x y z, x == y -> y == z -> x == z.

Proof.

  intros.
  intro.
  intros.
  elim H0. elim H.
  reflexivity.
Qed.

Require Import Setoid.

Instance eq_modulo_normalise_equi : Equivalence eq_modulo_normalise.

Proof.

  constructor.
  constructor.
  exact eq_modulo_normalise_sym.
  exact eq_modulo_normalise_trans.
Qed.

Lemma expr_wt :
  forall bound align e r,
    tcheck_expr e <> Some (typ_of_result r) ->
    normalise bound align e r = Vundef.

Proof.

  intros. eapply IsNorm.expr_wt.
  apply norm_correct.
  auto.
Qed.

Ltac destr_wt :=
  match goal with
      |- normalise _ _ ?e ?rt = _ =>
      destruct (tcheck_expr_dec e (typ_of_result rt));
        [|try (repeat rewrite expr_wt; auto; simpl in *; intuition congruence)]
  end.

Section NormSpec.

Lemma norm_eq'':
  forall (e e' : expr_sym) (r : result) (bound : block -> Z * Z)
         (align : block -> int),
    tcheck_expr e = Some (typ_of_result r) ->
    tcheck_expr e' = Some (typ_of_result r) ->
    (forall alloc em,
       compat alloc bound align ->
       eSexpr alloc em eb eu (typ_of_result r) e =
       eSexpr alloc em eb eu (typ_of_result r) e') ->
    normalise bound align e r = normalise bound align e' r.

Proof.

exact (normalise_eq'' eu eb normalise norm_correct norm_complete).
Qed.

Lemma expr_tc:
  forall e sz msk resType,
    tcheck_expr e <> Some (typ_of_result resType) ->
    normalise sz msk e resType = Vundef.

Proof.

  intros.
  apply expr_wt.
  auto.
Qed.

Lemma norm_correct2: normalise_correct2 eu eb normalise.

Proof.

apply normalise_correct_same.
apply norm_correct.
Qed.

Lemma no_alloc_undef:
  forall bound align e r,
    ~ (exists al, compat al bound align) ->
    normalise bound align e r = Vundef.

Proof.

  intros.
  eapply IsNorm.no_alloc_undef.
  apply norm_correct.
  auto.
Qed.

Lemma norm_gr:
forall bound align e r,
good_result bound e (normalise bound align e r) r.

Proof.

  intros.
  eapply IsNorm.result_wt.
  apply norm_correct.
Qed.

Definition dummy_em : block -> int -> byte := fun _ _ => Byte.zero.

Lemma normalise_undef: forall b a r t i, normalise b a (Eval (Eundef t i)) r = Vundef.

Proof.

  intros.
  destruct (ex_alloc_dec b a) as [(al,Hal)|Hal].
  - generalize (norm_correct2 b a (Eval (Eundef t i)) r); intro H.
    destruct (tcheck_expr_dec (Eval (Eundef t i)) (typ_of_result r)).
    + inversion H.
      specialize (eval_ok e al Hal).
      destruct eval_ok; intuition try congruence.
      generalize (H2 dummy_em).
      generalize (H2 (fun _ _ => Byte.one)).
      intros A B.
      rewrite <- A in B; contradict B; simpl.
      des r; discriminate.
    + apply expr_wt. auto.
  - apply no_alloc_undef; auto.
Qed.

Lemma normalise_zero_ext_and:
  forall e n,
    n >= 0 ->
    Eunop (OpZeroext n) Tint e == Ebinop OpAnd Tint Tint e (Eval (Eint (Int.repr ((two_p n) - 1)))).

Proof.

  intros. intro. intros.
  destr_wt.
  apply (norm_eq'' ); intros; simpl; try tauto.
  simpl_eval'.
  rewrite Int.zero_ext_and.
  reflexivity.
    omega.
Qed.

Section NormaliseFacts.

Variable sz : block -> Z*Z.
Variable msk : block -> int.

Variable alloc : block -> int.
Variable alloc_compat : compat alloc sz msk.

Lemma normalise_not_undef_wt:
  forall e t,
    normalise sz msk e t <> Vundef ->
    tcheck_expr e = Some (typ_of_result t).

Proof.

  intros.
  destruct (tcheck_expr_dec e (typ_of_result t)); auto.
  rewrite expr_tc in H. congruence.
  auto.
Qed.

Lemma normalise_int_type :
  forall v,
    (exists i, normalise sz msk v Int = Vint i) \/
    normalise sz msk v Int = Vundef.

Proof.

  intros.
  generalize (norm_gr sz msk v Int); intro H1.
  unfold good_result in H1.
  revert H1; destr_cond_match; eauto; tauto.
Qed.

Lemma normalise_long_type : forall v, (exists i, normalise sz msk v Long = Vlong i) \/ normalise sz msk v Long = Vundef.

Proof.

  intros.
  generalize (norm_gr sz msk v Long); intro H1.
  unfold good_result in H1.
  revert H1; destr_cond_match; eauto; tauto.
Qed.

Lemma normalise_float_type : forall v, (exists i, normalise sz msk v Float = Vfloat i) \/ normalise sz msk v Float = Vundef.

Proof.

  intros.
  generalize (norm_gr sz msk v Float); intro H1.
  unfold good_result in H1.
  revert H1; destr_cond_match; eauto; tauto.
Qed.

Lemma normalise_single_type : forall v, (exists i, normalise sz msk v Single = Vsingle i) \/ normalise sz msk v Single = Vundef.

Proof.

  intros.
  generalize (norm_gr sz msk v Single); intro H1.
  unfold good_result in H1.
  revert H1; destr_cond_match; eauto; tauto.
Qed.

Lemma normalise_ptr_type : forall v, (exists b ofs, normalise sz msk v Ptr = Vptr b ofs) \/ normalise sz msk v Ptr = Vundef.

Proof.

  intros.
  generalize (norm_gr sz msk v Ptr); intro H1.
  unfold good_result in H1.
  revert H1; destr_cond_match; eauto; tauto.
Qed.

Lemma normalise_int_int : forall v, normalise sz msk (Eval (Eint v)) Int = (Vint v).

Proof.

  intros.
  generalize (norm_correct2 sz msk (Eval (Eint v)) Int); intro H.
  inv H.
  specialize (eval_ok eq_refl alloc alloc_compat).
  simpl in *.
  destruct (normalise_int_type (Eval (Eint v))) as [[i H1]|H1]; rewrite H1 in *; simpl in *.
  - destruct eval_ok. congruence.
    destruct H.
    specialize (H0 dummy_em).
    inv H0; auto.
  - generalize (norm_complete sz msk (Eval (Eint v)) Int (Vint v)).
    intro A.
    rewrite H1 in A.
    assert (Val.lessdef (Vint v) Vundef).
    + apply A.
      constructor; intros; intuition try congruence.
      exists (Vi Int.zero).
      simpl in H2.
      inv H2. simpl; auto.
      exfalso; apply H; exists alloc; auto.
    + inv H.
Qed.

Lemma int_add_eq_l:
  forall a b c,
    Int.add a b = Int.add a c ->
    b = c.

Proof.

  intros.
  generalize (Int.eq_true (Int.add a b)).
  rewrite H at 2.
  rewrite ! (Int.add_commut a).
  rewrite Int.translate_eq.
  intro A.
  generalize (Int.eq_spec b c). rewrite A; auto.
Qed.

Lemma normalise_ptr_ptr :
  forall b ofs,
    in_bound (Int.unsigned ofs) (sz b) ->
    normalise sz msk (Eval (Eptr b ofs)) Ptr = Vptr b ofs.

Proof.

  intros b ofs IB.
  destruct (norm_correct2 sz msk (Eval (Eptr b ofs)) Ptr).
  destruct (normalise_ptr_type (Eval (Eptr b ofs))) as [[b' [ofs' H1]]|H1]; rewrite H1 in *.
  - simpl in *.
    specialize (eval_ok eq_refl alloc alloc_compat ); eauto.
    destruct eval_ok as [|[_ eval_ok]]; try congruence.
    specialize (eval_ok dummy_em).
    apply eq_lval_inj_i in eval_ok; auto.
    inv alloc_compat.
    destruct (peq b b').
    + subst. f_equal.
      apply int_add_eq_l in eval_ok; auto.
    + generalize (overlap _ _ _ _ n IB result_wt).
      rewrite eval_ok.
      congruence.
  - generalize (norm_complete sz msk (Eval (Eptr b ofs)) Ptr (Vptr b ofs)); intro NC.
    rewrite H1 in NC.
    assert ( IsNorm.t eu eb sz msk (Eval (Eptr b ofs)) Ptr (Vptr b ofs)).
    + constructor; simpl; intros; auto.
      inv H2. simpl.
      exists (Vi Int.zero); eauto. congruence.
      exfalso; apply H; exists alloc; auto.
    + specialize (NC H).
      inv NC.
Qed.

Lemma normalise_long_long : forall v, normalise sz msk (Eval (Elong v)) Long = (Vlong v).

Proof.

  intros.
  generalize (norm_correct2 sz msk (Eval (Elong v)) Long); intro H.
  inv H.
  specialize (eval_ok eq_refl alloc alloc_compat).
  simpl in *.
  destruct (normalise_long_type (Eval (Elong v))) as [[i H1]|H1]; rewrite H1 in *; simpl in *.
  - destruct eval_ok. congruence.
    destruct H.
    specialize (H0 dummy_em). inv H0; auto.
  - generalize (norm_complete sz msk (Eval (Elong v)) Long (Vlong v)).
    intro A.
    rewrite H1 in A.
    assert (Val.lessdef (Vlong v) Vundef).
    + apply A.
      constructor; intros; intuition try congruence.
      exists (Vi Int.zero).
      simpl in H2.
      inv H2. simpl; auto.
      exfalso; apply H; exists alloc; auto.
    + inv H.
Qed.

Lemma normalise_float_float : forall v, normalise sz msk (Eval (Efloat v)) Float = (Vfloat v).

Proof.

  intros.
  generalize (norm_correct2 sz msk (Eval (Efloat v)) Float); intro H.
  inv H.
  specialize (eval_ok eq_refl alloc alloc_compat).
  simpl in *.
  destruct (normalise_float_type (Eval (Efloat v))) as [[i H1]|H1]; rewrite H1 in *; simpl in *.
  - destruct eval_ok. congruence.
    destruct H.
    specialize (H0 dummy_em); inv H0; auto.
  - generalize (norm_complete sz msk (Eval (Efloat v)) Float (Vfloat v)).
    intro A.
    rewrite H1 in A.
    assert (Val.lessdef (Vfloat v) Vundef).
    + apply A.
      constructor; intros; intuition try congruence.
      exists (Vi Int.zero).
      simpl in H2.
      inv H2. simpl; auto.
      exfalso; apply H; exists alloc; auto.
    + inv H.
Qed.

Lemma normalise_single_single : forall v, normalise sz msk (Eval (Esingle v)) Single = (Vsingle v).

Proof.

  intros.
  generalize (norm_correct2 sz msk (Eval (Esingle v)) Single); intro H.
  inv H.
  specialize (eval_ok eq_refl alloc alloc_compat).
  simpl in *.
  destruct (normalise_single_type (Eval (Esingle v))) as [[i H1]|H1]; rewrite H1 in *; simpl in *.
  - destruct eval_ok. congruence.
    destruct H; specialize (H0 dummy_em); inv H0; auto.
  - generalize (norm_complete sz msk (Eval (Esingle v)) Single (Vsingle v)).
    intro A.
    rewrite H1 in A.
    assert (Val.lessdef (Vsingle v) Vundef).
    + apply A.
      constructor; intros; intuition try congruence.
      exists (Vi Int.zero).
      simpl in H2.
      inv H2. simpl; auto.
      exfalso; apply H; exists alloc; auto.
    + inv H.
Qed.

Lemma normalise_int_eval_inv:
  forall e e',
    normalise sz msk (Eval e') Int = Vint e ->
    match e' with
        Eint i => i = e
      | Eptr b o => Int.add (alloc b) o = e
      | _ => False
    end.

Proof.

  intros.
  destruct e'; simpl in *; try ( rewrite expr_tc in H; simpl; congruence).
  rewrite normalise_undef in H; congruence.
  rewrite normalise_int_int in H; inv H; auto.
  generalize (norm_correct2 sz msk (Eval (Eptr b i)) Int).
  rewrite H.
  intro A; inv A.
  specialize (eval_ok eq_refl alloc alloc_compat).
  simpl in eval_ok.
  destruct eval_ok; try congruence.
  destruct H0.
  specialize (H1 dummy_em); inv H1; auto.
Qed.

Lemma normalise_long_eval_inv:
  forall e e',
    normalise sz msk (Eval e') Long = Vlong e ->
    e' = Elong e.

Proof.

  intros.
  destruct e'; simpl in *;
  try (rewrite expr_tc in H; simpl; congruence);
  try (rewrite normalise_undef in H; congruence).
  rewrite normalise_long_long in H.
  inv H; auto.
Qed.

Lemma normalise_float_eval_inv:
  forall e e',
    normalise sz msk (Eval e') Float = Vfloat e ->
    e' = Efloat e.

Proof.

  intros.
  destruct e'; simpl in *;
  try (rewrite expr_tc in H; simpl; congruence);
  try (rewrite normalise_undef in H; congruence).
  generalize (norm_correct2 sz msk (Eval (Efloat f)) Float).
  rewrite H;
  intro A; inv A.
  specialize (eval_ok eq_refl alloc alloc_compat). simpl in *.
  destruct eval_ok. congruence.
  destruct H0. specialize (H1 dummy_em); inv H1; auto.
Qed.

Lemma normalise_single_eval_inv:
  forall e e',
    normalise sz msk (Eval e') Single = Vsingle e ->
    e' = Esingle e.

Proof.

  intros.
  destruct e'; simpl in *;
  try (rewrite expr_tc in H; simpl; congruence);
  try (rewrite normalise_undef in H; congruence).
  generalize (norm_correct2 sz msk (Eval (Esingle f)) Single).
  rewrite H;
  intro A; inv A.
  specialize (eval_ok eq_refl alloc alloc_compat). simpl in *.
  destruct eval_ok. congruence.
  destruct H0. specialize (H1 dummy_em); inv H1; auto.
Qed.

Lemma normalise_inv_eval :
  forall em e r v,
    tcheck_expr e = Some (typ_of_result r) ->
    normalise sz msk e r = v ->
    exists v',
      eSexpr alloc em eb eu (typ_of_result r) e =
      eEval alloc v' (typ_of_result r) v.

Proof.

  intros.
  assert (A:= norm_correct2 sz msk e r).
  inv A.
  specialize (eval_ok H alloc alloc_compat).
  destruct eval_ok; intuition try congruence.
  - rewrite H0 in *.
    simpl.
    exists (eSexpr alloc em eb eu (typ_of_result r) e); simpl.
    rewrite wt_lval_cast_id; auto.
    eapply eSexpr_wt; eauto.
  - (exists (Vi Int.zero)).
    rewrite H2; auto.
Qed.

Lemma add_t_commut :
  forall ot v v',
    ot <> Tfloat /\ ot <> Tsingle ->
    add_t ot ot v v' = add_t ot ot v' v.

Proof.

  unfold add_t.
  des ot; intros.
  apply Val.add_commut.
  des v; des v'.
  rewrite Int64.add_commut; reflexivity.
Qed.

Lemma mul_t_commut :
  forall ot
         (Ht : ot <> Tfloat /\ ot <> Tsingle),
    forall v v' : val, mul_t ot ot v v' = mul_t ot ot v' v.

Proof.

  unfold mul_t. des ot.
  apply Val.mul_commut.
  des v; des v';
  rewrite Int64.mul_commut. reflexivity.
Qed.

Lemma norm_eq_not_wt :
  forall sz msk e1 e2 rt,
    tcheck_expr e1 <> Some (typ_of_result rt) ->
    tcheck_expr e2 <> Some (typ_of_result rt) ->
   normalise sz msk e1 rt =
   normalise sz msk e2 rt.

Proof.

intros.
repeat rewrite expr_tc; auto.
Qed.

Lemma norm_eq_not_tc :
  forall sz msk e1 e2 rt,
    tcheck_expr e1 <> Some (typ_of_result rt) ->
    tcheck_expr e2 <> Some (typ_of_result rt) ->
   normalise sz msk e1 rt =
   normalise sz msk e2 rt.

Proof.

intros.
apply norm_eq_not_wt; auto.
Qed.

Lemma normalize_commut :
  forall ot e1 e2 P f g
         (Hp : P ot)
         (Hcomm : forall v v', f ot ot v v' = f ot ot v' v)
         (Heval : forall m env_mem env_undef_unop env_undef_binop x y ,
                    wt_expr x ot ->
                    wt_expr y ot ->
            (eSexpr m env_mem env_undef_unop env_undef_binop ot (g ot x y) =
             ebinop ot ot ot (eSexpr m env_mem env_undef_unop env_undef_binop) (eEval m (Vi Int.zero)) f x y))
         (Hwt : forall x y, wt_expr x ot -> wt_expr y ot -> wt_expr (g ot x y) ot)
         (Hwtdec : forall r x y, wt_expr (g ot x y) r ->
                                 r = ot /\ wt_expr x ot /\ wt_expr y ot)
  ,

    g ot e1 e2 == g ot e2 e1.

Proof.

  intros.
  intro.
  intros.
  destr_wt.

  apply norm_eq''; simpl in *; subst; eauto.
  - apply tcheck_expr_correct in e. apply Hwtdec in e.
    intuition subst.
    apply tcheck_expr_correct. apply Hwt; auto.
  - intros. apply tcheck_expr_correct in e. apply Hwtdec in e. simpl in e; intuition subst.
    repeat rewrite Heval; auto.
    unfold ebinop, binop; simpl.
    rewrite Hcomm.
    auto.
  - apply norm_eq_not_wt ; simpl; auto; intro.
    apply tcheck_expr_correct in H. apply Hwtdec in H.
    apply n. intuition subst. apply tcheck_expr_correct; apply Hwt; auto.
Qed.

Lemma normalize_plus_comm:
  forall ot e1 e2
         (HnFloat : ot <> Tfloat /\ ot <> Tsingle),
    Ebinop OpAdd ot ot e1 e2 == Ebinop OpAdd ot ot e2 e1.

Proof.

  intros.
  apply normalize_commut with (P:= fun ot => ot <> Tfloat ) (f:=add_t); simpl; intuition.
  intros ; apply add_t_commut ; auto.
  unfold ebinop, binop,fun_of_binop, fun_of_binop'; simpl.
  destr.

  revert Heqv.
  generalize (eSexpr_wt m env_mem env_undef_unop env_undef_binop x ot _ eq_refl).
  generalize (eSexpr_wt m env_mem env_undef_unop env_undef_binop y ot _ eq_refl).
  generalize (eSexpr m env_mem env_undef_unop env_undef_binop ot x).
  generalize (eSexpr m env_mem env_undef_unop env_undef_binop ot y).
  clear; intros.
  des l; des l0; des ot.
Qed.

Lemma normalize_mul_comm:
  forall e1 e2 ot
         (Ht : ot <> Tfloat /\ ot <> Tsingle),
    Ebinop OpMul ot ot e1 e2 == Ebinop OpMul ot ot e2 e1.

Proof.

  intros.
  apply normalize_commut with (P:= fun ot => ot <> Tfloat) (f:=mul_t); simpl; intuition.
  intros ; apply mul_t_commut ; auto.
  unfold ebinop, binop,fun_of_binop, fun_of_binop'; simpl.
  destr.

  revert Heqv.
  generalize (eSexpr_wt m env_mem env_undef_unop env_undef_binop x ot _ eq_refl).
  generalize (eSexpr_wt m env_mem env_undef_unop env_undef_binop y ot _ eq_refl).
  generalize (eSexpr m env_mem env_undef_unop env_undef_binop ot x).
  generalize (eSexpr m env_mem env_undef_unop env_undef_binop ot y).
  clear; intros.
  des l; des l0; des ot.
Qed.

Lemma normalise_int_not_int:
  forall a b rt i
    (T:rt <> Int /\ rt <> Ptr),
    normalise b a (Eval (Eint i)) rt = Vundef.

Proof.

  intros.
  apply expr_tc; eauto.
  des rt.
Qed.

Lemma normalise_long_not_long:
  forall a b rt i,
    rt <> Long ->
    normalise b a (Eval (Elong i)) rt = Vundef.

Proof.

  intros.
  apply expr_tc; eauto.
  des rt.
Qed.

Lemma normalise_float_not_float:
  forall a b rt i,
    rt <> Float ->
    normalise b a (Eval (Efloat i)) rt = Vundef.

Proof.

  intros.
  apply expr_wt; eauto.
  des rt.
Qed.

Lemma normalise_ptr_not_ptr:
  forall a bnds rt b ofs,
    rt <> Ptr ->
    rt <> Int ->
    normalise bnds a (Eval (Eptr b ofs)) rt = Vundef.

Proof.

  intros.
  apply expr_wt; eauto.
  des rt.
Qed.

Lemma normalise_type:
  forall bound align v t,
    match v with
        Vptr b ofs => t <> Ptr /\ t <> Int
      | Vfloat f => t <> Float
      | Vsingle f => t <> Single
      | Vint i => t <> Int /\ t <> Ptr
      | Vlong l => t <> Long
      | Vundef => True
    end ->
    normalise bound align (Eval (sval_of_val v)) t = Vundef.

Proof.

  intros.
  destruct v eqn:?; try ( simpl; try destr_cond_match; try apply normalise_undef;
  destruct t; simpl in *; intuition congruence);
  rewrite expr_tc; des t.
Qed.

Lemma long_undef_undef_long:
  forall i i' resType ,
    normalise sz msk (Eval (Elong i)) resType = Vundef ->
    Vundef = normalise sz msk (Eval (Elong i')) resType.

Proof.

  intros; symmetry.
  apply expr_wt; eauto.
  des resType.
  rewrite normalise_long_long in H; congruence.
Qed.

Lemma normalise_plus_zero_trans:
  forall e e2,
    normalise sz msk e Int = Vint Int.zero ->
    normalise sz msk (Ebinop OpAdd Tint Tint e2 e) Int = normalise sz msk e2 Int.

Proof.

  intros.
  assert (tcheck_expr e = Some Tint).
  destruct (tcheck_expr_dec e Tint); auto.
  rewrite expr_tc in H; auto.
  discriminate.
  destruct (tcheck_expr_dec e2 Tint); [|repeat rewrite (expr_tc); simpl; intuition solve_wt].
  - eapply (norm_eq''); eauto.
    + simpl; intuition try congruence.
      rewrite e0; simpl.
      rewrite H0; simpl; auto.
    + generalize (norm_correct2 sz msk e Int); intro A; inv A.
      rewrite H in eval_ok.
      simpl in *.
      intros.
      unfold ebinop, binop, fun_of_binop', fun_of_binop; simpl.
      repeat simpl_eval.
      specialize (H3 alloc0 H1).
      destruct H3; intuition try congruence.
      rewrite H6 in Heql0.
      inv Heql0.
      rewrite Int.add_zero; auto.
  - revert H1; destr.
    apply has_typ_true in Heqb.
    apply n; auto.
Qed.

Lemma typ_eq_refl:
forall A x (y z:A),
(if typ_eq x x then y else z) = y.

Proof.

intros.
destr.
Qed.

Lemma normalize_mul_zero:
  forall e0 e t,
    wt_expr e (typ_of_result t) ->
    normalise sz msk e0 t = Vint Int.zero ->
    normalise sz msk (Ebinop OpMul Tint Tint e0 e) t = Vint Int.zero.

Proof.

  intros.
  assert (t = Int).
  generalize (norm_gr sz msk e0 t); eauto.
  rewrite H0. simpl; destruct t; simpl; intuition try congruence.
  subst.
  assert (tcheck_expr e0 = Some Tint).
  destruct (tcheck_expr_dec e0 Tint); auto.
  rewrite (expr_wt) in H0. congruence.
  solve_wt. simpl; auto.
  assert (tcheck_expr (Ebinop OpMul Tint Tint e0 e) = Some Tint).
  simpl; solve_wt.
  rewrite <- H0.
  eapply (norm_eq''); simpl; try solve_wt.
  intros.
  generalize (norm_correct2 sz msk e0 Int). intro A.
  inv A.
  rewrite H0 in eval_ok.
  specialize (eval_ok H1 alloc0 H3).
  destruct eval_ok; intuition try congruence.
  simpl_eval'.
  rewrite H6 in Heql.
  inv Heql.
  rewrite Int.mul_commut.
  rewrite Int.mul_zero; auto.
Qed.

Lemma normalize_mul_one:
  forall e0 e t,
    wt_expr e (typ_of_result t) ->
    normalise sz msk e0 t = Vint Int.one ->
    normalise sz msk (Ebinop OpMul Tint Tint e e0) t = normalise sz msk e t.

Proof.

  intros.
  assert (t=Int).
  generalize (norm_gr sz msk e0 t); eauto.
  rewrite H0. simpl; destruct t; simpl; intuition try congruence.
  subst.
  assert (tcheck_expr e0 = Some Tint).
  destruct (tcheck_expr_dec e0 Tint); auto.
  rewrite expr_tc in H0; try congruence. auto.
  eapply (norm_eq''); eauto; simpl; solve_wt.
  assert (A:=norm_correct2 sz msk e0 Int).
    inv A.
    intros.
  specialize (eval_ok H1 alloc0 H2).
  rewrite H0 in eval_ok.
  destruct eval_ok; intuition try congruence.
  simpl_eval'.
  rewrite H5 in Heql0.
  inv Heql0.
  rewrite Int.mul_one. reflexivity.
Qed.

Lemma int_sign_ext_diff:
  forall n
         (Hnot0 : n > 0),
    Int.sign_ext n Int.one <> Int.sign_ext n Int.zero.

Proof.

  intros.
  intro.
  apply (f_equal (fun e => Int.testbit e 0)) in H.
  destruct (Z_le_dec n Int.zwordsize).
  repeat rewrite Int.bits_sign_ext in H by lia.
  destruct (zlt 0 n).
  discriminate.
  lia.
  repeat rewrite Int.sign_ext_above in H by lia.
  simpl in H.
  discriminate.
Qed.

Lemma int64_sign_ext_diff:
  forall n
         (Hnot0 : n > 0),
    Int64.sign_ext n (Int64.repr (Int.unsigned Int.one)) <> Int64.sign_ext n Int64.zero.

Proof.

  intros.
  intro.
  apply (f_equal (fun e => Int64.testbit e 0)) in H.
  destruct (Z_le_dec n Int64.zwordsize).
  repeat rewrite Int64.bits_sign_ext in H by lia.
  destruct (zlt 0 n).
  discriminate.
  lia.
  repeat rewrite Int64.sign_ext_above in H by lia.
  simpl in H.
  discriminate.
Qed.

Lemma int_zero_ext_diff:
  forall n
         (Hnot0 : n > 0),
    Int.zero_ext n Int.one <> Int.zero_ext n Int.zero.

Proof.

  intros.
  intro.
  apply Int.sign_ext_equal_if_zero_equal in H ;try lia.
  generalize int_sign_ext_diff; intuition try congruence.
  apply (H0 n); eauto; try lia.
Qed.

Lemma int64_zero_ext_diff:
  forall n
         (Hnot0 : n > 0),
    Int64.zero_ext n (Int64.repr (Int.unsigned Int.one)) <> Int64.zero_ext n Int64.zero.

Proof.

  intros.
  intro.
  apply Int64.sign_ext_equal_if_zero_equal in H ;try lia.
  generalize int64_sign_ext_diff; intuition try congruence.
  apply (H0 n); eauto; try lia.
Qed.

End NormaliseFacts.

Lemma normalise_zero_ext_undef:
  forall n ot t i
         (Hnot0: n >= 8),
    (Eunop (OpZeroext n) ot (Eval (Eundef t i))) == Eval (Eundef t i).

Proof.

  intros; intro; intros.
  destruct (ex_alloc_dec sz msk) as [[alloc alloc_compat]|Hnal].
  destr_wt.
  - simpl in e. des ot.
    + apply norm_eq''; simpl; auto; try tauto.
      intros; simpl; simpl_eval'.
      f_equal. f_equal.
      apply Int.same_bits_eq.
      intros.
      rewrite Int.bits_zero_ext; intuition.
      destr.
      rewrite Int.testbit_repr; intuition.
      rewrite Byte.Ztestbit_above with (n:=Z.to_nat i0); auto.
      generalize (Byte.unsigned_range (em t i)).
      unfold Byte.modulus.
      cut (two_power_nat Byte.wordsize <= two_power_nat (Z.to_nat i0)).
      omega.
      repeat rewrite two_power_nat_two_p.
      rewrite Z2Nat.id; auto.
      apply two_p_monotone.
      intuition.
      unfold Byte.wordsize; simpl.
      omega.
      rewrite Z2Nat.id; auto.
      omega.
  - rewrite normalise_undef.
    rewrite expr_tc; simpl in *; auto.
  - repeat rewrite (no_alloc_undef); auto.
Qed.

Lemma wt_lval_cast:
  forall v t,
    wt_lval v t ->
    cast t v = v.

Proof.

intros.
destruct v; destruct t; simpl in *; intuition try congruence.
Qed.

Lemma normalise_convert_float_float:
  forall sz msk f,
    normalise sz msk (Eunop (OpConvert SESigned (Tfloat, SESigned)) Tfloat (Eval (Efloat f))) Float =
    normalise sz msk (Eval (Efloat f)) Float.

Proof.

  intros.
  destr_wt.
  simpl in *; intuition.
  apply (norm_eq''); simpl in *; intuition try congruence.
Qed.

Lemma ofwords_magic_diff:
  forall i,
    Int64.ofwords (Int.repr (Int64.unsigned Int64.zero)) i <>
    Int64.ofwords (Int.repr (Int64.unsigned Int64.one)) i.

Proof.

  intros; intro H.
  apply (f_equal (fun x => Int64.testbit x 32)) in H.
  repeat rewrite Int64.bits_ofwords in H by (vm_compute; intuition congruence).
  revert H; destr; try (vm_compute in l; congruence).
  vm_compute in H; congruence.
Qed.

Lemma convert_t_subtype_wt_val:
  forall t0 resType s0 t s l
         (w : t0 = typ_of_result resType),
         wt_val (convert_t s (t0, s0) t (val_of_lval_t t (cast t (Vl l))))
                (typ_of_result resType).

Proof.

  intuition.
  des t; des s; des s0; des resType; try rewrite <- w; auto;
    unfold convert_t; simpl; try wt_val_option_map.
Qed.

Definition styp_of_typ (t:typ) : styp :=
  styp_of_ast t.

Definition typ_of_styp (t:styp) : typ :=
  match t with
      Tint => AST.Tint
    | Tlong => AST.Tlong
    | Tfloat => AST.Tfloat
    | Tsingle => AST.Tsingle
  end.

Lemma typ_of_styp_of_typ:
  forall t,
    t <> Tany32 /\ t <> Tany64 ->
    typ_of_styp (styp_of_typ t) = t.

Proof.

des t. Qed.

Lemma styp_of_typ_of_styp:
forall t,
styp_of_typ (typ_of_styp t) = t.

Proof.

des t. Qed.

Lemma normalise_convert_float_type_idem:
  forall e,
    wt_expr e Tfloat ->
    Eunop (OpConvert SESigned (Tfloat, SESigned)) Tfloat e == e.

Proof.

  intros; intro; intros.
  destr_wt.
  simpl in e0.
  revert e0; destr.
  des (tcheck_expr e). des s.
  des resType.
  apply (norm_eq''); simpl; auto; intuition try congruence.
  rewrite Heqo; simpl; auto.
  simpl. simpl_eval'. simpl. simpl_eval'.
  simpl in n. intuition.
  apply norm_eq_not_wt; simpl in *; intuition try congruence.
  apply tcheck_expr_correct in H.
  des resType.
  rewrite H0 in n; simpl in *. congruence.
Qed.

Lemma normalise_convert_single_type_idem:
  forall e,
    wt_expr e Tsingle ->
    Eunop (OpConvert SESigned (Tsingle, SESigned)) Tsingle e == e.

Proof.

  intros; intro; intros.
  destr_wt.
  apply tcheck_expr_correct in H.
  apply norm_eq''; simpl; auto; intuition try congruence.
  simpl in e0.
  rewrite H in e0; simpl in e0. congruence.
  simpl_eval'; simpl; simpl_eval'.
  rewrite H in e0. des resType.
  simpl in n. intuition.
  apply norm_eq_not_wt; simpl in *; intuition try congruence.
  apply tcheck_expr_correct in H.
  rewrite H in n; simpl in n.
  des resType.
Qed.

Lemma normalize_zero_ext_32:
forall e, wt_expr e Tint ->
(Eunop (OpZeroext 32) Tint e) == e.

Proof.

  intros.
  intro; intros.
  destr_wt; solve_wt.
  apply norm_eq''; simpl in *; rewrite H in *; simpl in *; solve_wt; try tauto.
  - intros; simpl. simpl_eval'. inv e0. rewrite Heql.
    rewrite Int.zero_ext_above by (unfold Int.zwordsize; simpl; lia).
    reflexivity.
  - apply norm_eq_not_wt; simpl in *; intuition try congruence.
    rewrite H in H0; inv H0.
    apply n; intuition; try constructor.
    rewrite H; simpl; auto. rewrite H2. reflexivity.
Qed.

Lemma normalize_sign_ext_32:
forall e, wt_expr e Tint ->
(Eunop (OpSignext 32) Tint e) == e.

Proof.

  intros.
  intro; intros.
  destr_wt; solve_wt.
  apply norm_eq''; simpl in *; rewrite H in *; simpl in *; solve_wt; try tauto.
  - intros; simpl. simpl_eval'. inv e0. rewrite Heql.
    rewrite Int.sign_ext_above by (unfold Int.zwordsize; simpl; lia).
    reflexivity.
  - apply norm_eq_not_wt; simpl in *; intuition try congruence.
    rewrite H in H0; inv H0.
    apply n; intuition; try constructor.
    rewrite H; simpl; auto. rewrite H2. reflexivity.
Qed.

Lemma normalize_zero_ext_64:
forall e, wt_expr e Tlong ->
(Eunop (OpZeroext 64) Tlong e) == e.

Proof.

  intros.
  intro; intros.
  destr_wt; solve_wt.
  apply norm_eq''; simpl in *; rewrite H in *; simpl in *; solve_wt; try tauto.
  - intros; simpl. simpl_eval'. inv e0. rewrite Heql.
    rewrite Int64.zero_ext_above by (unfold Int64.zwordsize; simpl; lia).
    reflexivity.
  - apply norm_eq_not_wt; simpl in *; intuition try congruence.
    rewrite H in H0; inv H0.
    apply n; intuition; try constructor.
    rewrite H; simpl; auto. rewrite H2. reflexivity.
Qed.

Lemma normalize_sign_ext_64:
forall e, wt_expr e Tlong ->
(Eunop (OpSignext 64) Tlong e) == e.

Proof.

  intros.
  intro; intros.
  destr_wt; solve_wt.
  apply norm_eq''; simpl in *; rewrite H in *; simpl in *; solve_wt; try tauto.
  - intros; simpl. simpl_eval'. inv e0. rewrite Heql.
    rewrite Int64.sign_ext_above by (unfold Int64.zwordsize; simpl; lia).
    reflexivity.
  - apply norm_eq_not_wt; simpl in *; intuition try congruence.
    rewrite H in H0; inv H0.
    apply n; intuition; try constructor.
    rewrite H; simpl; auto. rewrite H2. reflexivity.
Qed.

Lemma normalise_and_undef_zero:
  forall sz msk e1 e2,
    wt_expr e2 Tint ->
    normalise sz msk e1 Int = Vint Int.zero ->
    normalise sz msk (Ebinop OpAnd Tint Tint e1 e2) Int = Vint Int.zero.

Proof.

  intros.
  destruct (ex_alloc_dec sz msk) as [[al Hal]|Hal].
  destruct (wt_expr_dec (Ebinop OpAnd Tint Tint e1 e2) Tint).
  - simpl in w. intuition.
    rewrite <- (normalise_int_int sz msk al Hal); auto.
    apply norm_eq''; simpl; intuition try congruence; solve_wt.
    + simpl_eval.
      assert (A:= norm_correct2 sz msk e1 Int).
      inv A.
      specialize (eval_ok H1 alloc H5).
      rewrite H0 in eval_ok; destruct eval_ok; intuition try congruence.
      rewrite H11 in Heql.
      simpl in Heql.
      inv Heql.
      rewrite Int.and_zero_l; auto.
  - simpl in n.
    intuition try congruence.
    exfalso; apply H1; intuition; try constructor.
    destruct (wt_expr_dec e1 Tint); auto.
    rewrite (expr_wt) in H0; simpl; try congruence.
    rewrite tcheck_expr_correct. auto.
  - rewrite (no_alloc_undef ) in H0; auto.
    congruence.
Qed.

Lemma ltu_zero_iwordsize :
Int.ltu Int.zero Int.iwordsize = true.

Proof.

reflexivity.
Qed.

Lemma normalise_singleofbits:
forall n,
Eval (Esingle (Float32.of_bits n)) == Eunop OpSingleofbits Tint (Eval (Eint n)).

Proof.

  intros; intro; intros.
  destr_wt.
  simpl in e; intuition.
  apply norm_eq''; simpl; intuition try congruence.
Qed.

Lemma normalise_bitsofsingle:
forall n,
Eval (Eint (Float32.to_bits n)) == Eunop OpBitsofsingle Tsingle (Eval (Esingle n)).

Proof.

  intros; intro; intros.
  destr_wt.
  simpl in *.
  apply norm_eq''; simpl; auto; intuition try congruence.
Qed.

Lemma normalise_doubleofbits:
forall n,
Eval (Efloat (Float.of_bits n)) == Eunop OpDoubleofbits Tlong (Eval (Elong n)).

Proof.

  intros; intro; intros.
  destr_wt.
  simpl in e; intuition.
  apply (norm_eq''); simpl; auto; intuition try congruence.
Qed.

Lemma normalise_bitsofdouble:
forall n,
Eval (Elong (Float.to_bits n)) == Eunop OpBitsofdouble Tfloat (Eval (Efloat n)).

Proof.

  intros; intro; intros.
  destr_wt. simpl in e; intuition.
  apply (norm_eq''); simpl; auto; intuition try congruence.
Qed.

Lemma normalise_sign_ext_sign_ext:
forall e n (Hn : 0 < n),
Eunop (OpSignext n) Tint (Eunop (OpSignext n) Tint e) == Eunop (OpSignext n) Tint e.

Proof.

  intros ; intro ; intros.
  destr_wt.
  apply norm_eq''; simpl in *; solve_wt; intuition try congruence; solve_wt; try congruence.
  des (tcheck_expr e). des s.
  simpl_eval'.
  rewrite Int.sign_ext_widen; auto; lia.
  apply norm_eq_not_wt; auto.
  simpl in *.
  des (tcheck_expr e). des s.
Qed.

Lemma normalise_zero_ext_widen:
  forall n n' e
    (Hn : 0 <= n <= n'),
    Eunop (OpZeroext n') Tint (Eunop (OpZeroext n) Tint e) == Eunop (OpZeroext n) Tint e.

Proof.

  intros ; intro ; intros.
  destr_wt.
  apply norm_eq'';
  simpl in * ; intuition try congruence; solve_wt; try congruence.
  des (tcheck_expr e). des s.
  simpl_eval'.
  rewrite Int.zero_ext_widen ; try lia; reflexivity.
  apply norm_eq_not_wt; auto.
  simpl in *.
  des (tcheck_expr e). des s.
Qed.

Lemma normalise_zero_ext_zero_ext:
  forall e n
    (Hn : 0 < n),
    Eunop (OpZeroext n) Tint (Eunop (OpZeroext n) Tint e) == Eunop (OpZeroext n) Tint e.

Proof.

intros.
apply normalise_zero_ext_widen ; lia.
Qed.

Lemma normalise_sign_ext_zero_ext:
  forall e n ot,
    0 < n ->
    Eunop (OpSignext n) ot (Eunop (OpZeroext n) ot e) == Eunop (OpSignext n) ot e.

Proof.

  intros; intro; intros.
  destr_wt.
  apply norm_eq''; simpl in *; intuition try congruence.
  des (tcheck_expr e). des s; des ot.
  des (tcheck_expr e). des s; des ot; inv e0; simpl; simpl_eval'.
  rewrite Int.sign_ext_zero_ext; auto.
  rewrite Int64.sign_ext_zero_ext; auto.
  apply norm_eq_not_wt; auto.
  simpl in *.
  des (tcheck_expr e). des s; des ot.
Qed.

Lemma normalise_zero_ext_sign_ext:
  forall e n ot,
    0 < n ->
    Eunop (OpZeroext n) ot (Eunop (OpSignext n) ot e) == Eunop (OpZeroext n) ot e.

Proof.

  intros; intro; intros.
  destr_wt.
  apply norm_eq''; simpl in *; intuition try congruence.
  des (tcheck_expr e). des s; des ot.
  des (tcheck_expr e). des s; des ot; inv e0; simpl; simpl_eval'.
  rewrite Int.zero_ext_sign_ext; auto.
  rewrite Int64.zero_ext_sign_ext; auto.
  apply norm_eq_not_wt; auto.
  simpl in *.
  des (tcheck_expr e). des s; des ot.
Qed.

Lemma normalise_sign_ext_widen:
  forall n n' e ot,
    0 < n <= n' ->
    Eunop (OpSignext n') ot (Eunop (OpSignext n) ot e) == Eunop (OpSignext n) ot e .

Proof.

   intros; intro; intros.
  destr_wt.
  apply norm_eq''; simpl in *; intuition try congruence.
  des (tcheck_expr e). des s; des ot.
  des (tcheck_expr e). des s; des ot; inv e0; simpl; simpl_eval'.
  rewrite Int.sign_ext_widen; auto.
  rewrite Int64.sign_ext_widen; auto.
  apply norm_eq_not_wt; auto.
  simpl in *.
  des (tcheck_expr e). des s; des ot.
Qed.

Lemma normalise_sign_zero_ext_widen:
  forall n n' e ot,
    0 <= n < n' ->
    Eunop (OpSignext n') ot (Eunop (OpZeroext n) ot e ) == Eunop (OpZeroext n) ot e.

Proof.

  intros; intro; intros.
  destr_wt.
  apply norm_eq''; simpl in *; intuition try congruence.
  des (tcheck_expr e). des s; des ot.
  des (tcheck_expr e). des s; des ot; inv e0; simpl; simpl_eval'.
  rewrite Int.sign_zero_ext_widen; auto.
  rewrite Int64.sign_zero_ext_widen; auto.
  apply norm_eq_not_wt; auto.
  simpl in *.
  des (tcheck_expr e). des s; des ot.
Qed.

Lemma normalise_zero_ext_narrow:
  forall n n' e ot,
    0 <= n <= n' ->
    Eunop (OpZeroext n) ot (Eunop (OpZeroext n') ot e) == Eunop (OpZeroext n) ot e.

Proof.

  intros; intro; intros.
  destr_wt.
  apply norm_eq''; simpl in *; intuition try congruence.
  des (tcheck_expr e). des s; des ot.
  des (tcheck_expr e). des s; des ot; inv e0; simpl; simpl_eval'.
  rewrite Int.zero_ext_narrow; auto.
  rewrite Int64.zero_ext_narrow; auto.
  apply norm_eq_not_wt; auto.
  simpl in *.
  des (tcheck_expr e). des s; des ot.
Qed.

Lemma normalise_sign_ext_narrow:
  forall n n' e ot,
    0 < n <= n' ->
    Eunop (OpSignext n) ot (Eunop (OpSignext n') ot e) == Eunop (OpSignext n) ot e.

Proof.

  intros; intro; intros.
  destr_wt.
  apply norm_eq''; simpl in *; intuition try congruence.
  des (tcheck_expr e). des s; des ot.
  des (tcheck_expr e). des s; des ot; inv e0; simpl; simpl_eval'.
  rewrite Int.sign_ext_narrow; auto.
  rewrite Int64.sign_ext_narrow; auto.
  apply norm_eq_not_wt; auto.
  simpl in *.
  des (tcheck_expr e). des s; des ot.
Qed.

Lemma normalise_zero_sign_ext_narrow:
  forall n n' e ot,
    0 < n <= n' ->
    Eunop (OpZeroext n) ot (Eunop (OpSignext n') ot e) == Eunop (OpZeroext n) ot e.

Proof.

  intros; intro; intros.
  destr_wt.
  apply norm_eq''; simpl in *; intuition try congruence.
  des (tcheck_expr e). des s; des ot.
  des (tcheck_expr e). des s; des ot; inv e0; simpl; simpl_eval'.
  rewrite Int.zero_sign_ext_narrow; auto.
  rewrite Int64.zero_sign_ext_narrow; auto.
  apply norm_eq_not_wt; auto.
  simpl in *.
  des (tcheck_expr e). des s; des ot.
Qed.

Lemma normalise_sign_ext_int:
forall i n ,
Eunop (OpSignext n) Tint (Eval (Eint i)) == Eval (Eint (Int.sign_ext n i)).

Proof.

  intros; intro; intros.
  destr_wt.
  apply (norm_eq''); simpl in *; intuition try congruence.
Qed.

Lemma normalise_sign_ext_long:
forall i n ,
Eunop (OpSignext n) Tlong (Eval (Elong i)) == Eval (Elong (Int64.sign_ext n i)).

Proof.

  intros; intro; intros.
  destr_wt.
  apply (norm_eq''); simpl in *; intuition try congruence.
Qed.

Lemma normalise_zero_ext_int:
forall e n ,
Eunop (OpZeroext n) Tint (Eval (Eint e)) == Eval (Eint (Int.zero_ext n e)).

Proof.

  intros; intro; intros.
  destr_wt.
  apply (norm_eq''); simpl in *; intuition try congruence.
Qed.

Lemma normalise_zero_ext_long:
forall e n ,
Eunop (OpZeroext n) Tlong (Eval (Elong e)) == Eval (Elong (Int64.zero_ext n e)).

Proof.

  intros; intro; intros.
  destr_wt.
  apply (norm_eq''); simpl in *; intuition try congruence.
Qed.

Lemma ltu_zero_iwordsize':
Int.ltu Int.zero Int64.iwordsize' = true.

Proof.

  unfold Int.ltu.
  unfold Int.zero. unfold Int64.iwordsize'.
  unfold Int64.zwordsize.
  simpl.
  repeat rewrite Int.unsigned_repr by
      (unfold Int.max_unsigned; simpl; omega); auto.
Qed.

Lemma int64_shr'_zero:
forall i,
Int64.shr' i Int.zero = i.

Proof.

  intros; apply Int64.same_bits_eq; intros.
  rewrite Int64.bits_shr'.
  rewrite Int.unsigned_zero. rewrite zlt_true.
  f_equal; omega.
  omega. omega.
Qed.

Lemma int64_shru'_zero:
forall i,
Int64.shru' i Int.zero = i.

Proof.

  intros; apply Int64.same_bits_eq; intros.
  rewrite Int64.bits_shru'.
  rewrite Int.unsigned_zero. rewrite zlt_true.
  f_equal; omega.
  omega. omega.
Qed.

Lemma normalise_shr:
  forall ot sg e e0
         (Ht: is_lval_typ ot)
         (Hwt : tcheck_expr e0 = Some Tint)
         (Ht': tcheck_expr e = Some ot),
    e0 == Eval (Eint Int.zero) ->
    Ebinop (OpShr sg) ot Tint e e0 == e.

Proof.

  intros; intro; intros.
  destr_wt; simpl in *.
  - clear_useless.
    rewrite Ht' in e1. rewrite Hwt in e1. simpl in *.
    rewrite styp_eq_refl in e1.
    rewrite pred_dec_true in e1; auto.
    inv e1.
    apply norm_eq''; simpl. intuition try congruence.
    rewrite ! Ht'. simpl. rewrite styp_eq_refl.
    rewrite Hwt. simpl. rewrite pred_dec_true; auto. auto.
    specialize (H Int sz msk).
    symmetry in H.
    intros.
    apply (same_norm _ _ _ norm_correct) with (alloc:=alloc) (em:=em) in H; solve_wt; auto.
    simpl in H. symmetry in H.
    inv Ht; des sg; intros; simpl; simpl_eval'; simpl; rewrite H; simpl; simpl_int.
    rewrite Int.shr_zero; auto.
    rewrite Int.shru_zero; auto.
    rewrite int64_shr'_zero; auto.
    rewrite int64_shru'_zero; auto.
    rewrite normalise_int_int with (alloc:=alloc) ; auto.
    congruence.
  - simpl in n; intuition.
    apply norm_eq_not_wt; simpl in *; intuition try congruence.
    rewrite Ht' in n; rewrite Hwt in n. simpl in *.
    rewrite styp_eq_refl in n; rewrite pred_dec_true in n; auto.
    rewrite Ht' in H0. inv H0. congruence.
Qed.

Lemma shr_t_zero_id :
  forall v sg t,
    t = Tint \/ t = Tlong ->
    shr_t sg t Tint (val_of_lval_t t v) (Vint Int.zero) = val_of_lval_t t v.

Proof.

  intros.
  unfold shr_t.
  destruct t; destruct sg; intuition try congruence;
  unfold Val.shr, Val.shrl, Val.shru, Val.shrlu;
  destruct v ; simpl ; try tauto; try rewrite ltu_zero_iwordsize;
  try rewrite ltu_zero_iwordsize'.
  rewrite Int.shr_zero; auto.
  rewrite Int.shru_zero; auto.
  rewrite int64_shr'_zero; auto.
  rewrite int64_shru'_zero; auto.
Qed.

Lemma normalise_shr_zero_id:
  forall sg ot e1
         (Ht : forall ty,
                 wt_expr e1 ty ->
                 wt_expr (Ebinop (OpShr sg) ot Tint e1 (Eval (Eint Int.zero))) ty),
    wt_expr e1 ot ->
    Ebinop (OpShr sg) ot Tint e1 (Eval (Eint Int.zero)) == e1.

Proof.

  intros.
  apply normalise_shr; auto.
  specialize (Ht _ H).
  simpl in Ht; intuition.
  solve_wt.
  reflexivity.
Qed.

Lemma int_zero_ext_idem_Z :
  forall (z:Z) e ,
    z > 0 ->
    z < Int.zwordsize ->
    Int.zero_ext z (Int.repr (Int.unsigned e mod two_p z)) =
    Int.zero_ext z e.

Proof.

  intros.
  assert (H1: two_p z > 0) by (apply two_p_gt_ZERO; omega).
  rewrite <- Int.repr_unsigned at 1.
  rewrite Int.zero_ext_mod; try omega.
  rewrite <- Int.repr_unsigned.
  rewrite Int.zero_ext_mod; try omega.
  assert (H2 := Z_mod_lt (Int.unsigned e) (two_p z) H1).
  rewrite Int.unsigned_repr; auto.
  rewrite Zmod_small; auto; reflexivity.
  split; try omega.
  unfold Int.max_unsigned.
  assert (two_p z <= Int.modulus).
  unfold Int.modulus.
  unfold Int.zwordsize in H0.
  simpl in H0.
  rewrite two_power_nat_two_p.
  apply two_p_monotone.
  simpl; omega.
  omega.
Qed.

Lemma two_p_two_power_pos:
  forall n nZ nP,
    (0 < n <= Z.to_nat Int.zwordsize)%nat ->
    Z.of_nat n = nZ ->
    Pos.of_nat n = nP ->
    two_p nZ = two_power_pos nP.

Proof.

  intros; subst.
  rewrite two_power_pos_nat.
  rewrite <- two_power_nat_two_p.
  rewrite Nat2Pos.id; [reflexivity|omega].
Qed.

Lemma int_zero_ext_idem :
  forall (n:nat) e nZ nP,
    (0 < n < (Z.to_nat Int.zwordsize))%nat ->
    (Z.of_nat n) = nZ ->
    (Pos.of_nat n) = nP ->
    Int.zero_ext nZ (Int.repr (Int.unsigned e mod two_power_pos nP)) =
    Int.zero_ext nZ e.

Proof.

  intros.
  erewrite <- two_p_two_power_pos; eauto.
  destruct H.
  apply int_zero_ext_idem_Z.
  omega.
  subst; unfold Int.zwordsize in *.
  rewrite Nat2Z.id in H2.
  apply inj_lt; auto.
  omega.
Qed.

Lemma int_sign_ext_idem :
  forall (n:nat) e nZ nP,
    (0 < n < Z.to_nat Int.zwordsize)%nat ->
    (Z.of_nat n) = nZ ->
    (Pos.of_nat n) = nP ->
    Int.sign_ext nZ (Int.repr (Int.unsigned e mod two_power_pos nP)) =
    Int.sign_ext nZ e.

Proof.

  intros.
  apply Int.sign_ext_equal_if_zero_equal.
  omega.
  apply int_zero_ext_idem with (n:=n); auto.
Qed.

Lemma repr_unsigned_mod32:
forall n,
(Int.repr (Int.unsigned n mod two_power_pos 32)) = n.

Proof.

  intros.
  replace (two_power_pos 32) with (Int.modulus) by auto.
  rewrite <- Int.unsigned_repr_eq.
  repeat rewrite Int.repr_unsigned.
  reflexivity.
Qed.

Lemma repr_unsigned_mod64:
forall n,
(Int64.repr (Int64.unsigned n mod two_power_pos 64)) = n.

Proof.

  intros.
  replace (two_power_pos 64) with (Int64.modulus) by auto.
  rewrite <- Int64.unsigned_repr_eq.
  repeat rewrite Int64.repr_unsigned.
  reflexivity.
Qed.

Lemma normalise_sign_ext:
  forall n p,
    (0 < p < Int.wordsize)%nat ->
    Eval
      (Eint (Int.sign_ext (Z.of_nat p) (Int.repr (Int.unsigned n mod two_power_nat p)))) ==
    Eunop (OpSignext (Z.of_nat p)) Tint (Eval (Eint n)).

Proof.

  intros; intro; intros.
  destr_wt.
  apply norm_eq''; simpl in *; solve_wt; intuition try congruence.
  simpl_eval'.
  f_equal.
  replace (two_power_nat p) with (two_power_pos (Pos.of_nat p)).
  rewrite int_sign_ext_idem with (n:=p) (nP:=Pos.of_nat p); auto.
  rewrite two_power_pos_nat.
  rewrite Nat2Pos.id; auto.
  lia.
Qed.

Lemma normalise_zero_ext:
  forall n p,
    (0 < p < Int.wordsize)%nat ->
    Eval
      (Eint (Int.zero_ext (Z.of_nat p) (Int.repr (Int.unsigned n mod two_power_nat p)))) ==
    Eunop (OpZeroext (Z.of_nat p)) Tint (Eval (Eint n)).

Proof.

  intros; intro; intros.
  destr_wt.
  apply norm_eq''; simpl in *; solve_wt; intuition try congruence.
  simpl_eval'.
  decEq.
  replace (two_power_nat p) with (two_power_pos (Pos.of_nat p)).
  rewrite int_zero_ext_idem with (n:=p) (nP:=Pos.of_nat p); auto.
  rewrite two_power_pos_nat.
  rewrite Nat2Pos.id; auto.
  lia.
Qed.

Lemma normalise_sign_ext_32:
  forall n,
   Eval (Eint (Int.repr (Int.unsigned n mod two_power_nat 32))) ==
   Eunop (OpSignext 32) Tint (Eval (Eint n)).

Proof.

  intros; intro; intros.
  destr_wt.
  apply norm_eq''; simpl in *; solve_wt; intuition try congruence.
  simpl_eval'.
  decEq.
  rewrite Int.sign_ext_above.
  rewrite repr_unsigned_mod32; auto.
  unfold Int.zwordsize, Int.wordsize, Wordsize_32.wordsize; simpl; omega.
Qed.

Lemma normalise_zero_ext_32:
  forall n,
   Eval (Eint (Int.repr (Int.unsigned n mod two_power_nat 32))) ==
   Eunop (OpZeroext 32) Tint (Eval (Eint n)).

Proof.

  intros; intro; intros.
  destr_wt.
  apply norm_eq''; simpl in *; solve_wt; intuition try congruence.
  simpl_eval'.
  decEq.
  rewrite Int.zero_ext_above.
  rewrite repr_unsigned_mod32; auto.
  unfold Int.zwordsize.
  unfold Int.wordsize.
  unfold Wordsize_32.wordsize.
  simpl.
  omega.
Qed.

Lemma normalise_convert_float_float_idem:
  forall n,
    Eval (Efloat n) ==
    Eunop (OpConvert SESigned (Tfloat, SESigned)) Tfloat (Eval (Efloat n)).

Proof.

  intros; intro; intros.
  destr_wt.
  apply norm_eq''; simpl in *; solve_wt; intuition try congruence.
Qed.

Section NormaliseIdem.

Variable sz : block -> Z*Z.
Variable msk : block -> int.

Variable sz2 : block -> Z*Z.
Hypothesis same_bounds : forall b, sz b = sz2 b.
Variable msk2 : block -> int.
Hypothesis same_masks : forall b, msk b = msk2 b.

Lemma compat_same_bounds:
  forall a b c d e,
    (forall f, b f = c f) ->
    (forall f, d f = e f) ->
    compat a b d ->
    compat a c e.

Proof.

  intros.
  destruct H1.
  constructor; intros; eauto.
  apply addr_space; rewrite H; auto.
  apply overlap; auto; rewrite H; auto.
  rewrite <- H0; apply alignment.
Qed.

Lemma good_result_same_bounds:
forall e v r,
good_result sz e v r <-> good_result sz2 e v r.

Proof.

  split; intros;
  unfold good_result in *;
  des v; des r.
Qed.

Lemma normalise_idem_if_bounds_align_idem:
forall e t,
normalise sz msk e t = normalise sz2 msk2 e t.

Proof.

  intros.
  destruct (tcheck_expr_dec e (typ_of_result t)).
  - generalize (norm_correct sz msk e t); intro Ha.
    generalize (norm_correct sz2 msk2 e t); intro Hb.
    assert (IsNorm.t eu eb sz msk e t (normalise sz2 msk2 e t)).
    {
      destruct Hb; econstructor; eauto.
      intros.
      specialize (eval_ok e0 alloc em v').
      apply eval_ok; auto.
      eapply compat_same_bounds; eauto.
      apply good_result_same_bounds. auto.
      intros.
      apply no_alloc_undef0.
      intros [alloc Hcompat].
      eapply compat_same_bounds in Hcompat; eauto.
    }
    assert (IsNorm.t eu eb sz2 msk2 e t (normalise sz msk e t)).
    {
      destruct Ha; econstructor; eauto.
      intros.
      specialize (eval_ok e0 alloc em v').
      apply eval_ok; auto.
      symmetry in same_bounds, same_masks.
      eapply compat_same_bounds; eauto.
      symmetry in same_bounds, same_masks.
      eapply good_result_same_bounds. eauto.
      intros.
      apply no_alloc_undef0.
      intros [alloc Hcompat].
      symmetry in same_bounds, same_masks.
      eapply compat_same_bounds in Hcompat; eauto.
    }
    generalize (norm_complete sz msk e t (normalise sz2 msk2 e t)); intro Hc.
    generalize (norm_complete sz2 msk2 e t (normalise sz msk e t)); intro Hd.
    apply lessdef_antisym ; eauto.
  - repeat (rewrite expr_wt; eauto).
Qed.

End NormaliseIdem.

Lemma normalise_idem_same_bounds:
  forall sz sz2 msk e t,
    (forall b, sz b = sz2 b) ->
    normalise sz msk e t = normalise sz2 msk e t.

Proof.

intros.
apply normalise_idem_if_bounds_align_idem; auto.
Qed.

Lemma normalise_idem_same_align:
  forall sz msk msk2 e t,
    (forall b, msk b = msk2 b) ->
    normalise sz msk e t = normalise sz msk2 e t.

Proof.

intros.
apply normalise_idem_if_bounds_align_idem; auto.
Qed.

End NormSpec.

Lemma normalise_sign_ext_shr_shl:
  forall (n : Z) (e : expr_sym),
  0 < n < Int.zwordsize ->
  let y := Int.repr (Int.zwordsize - n) in
  Eunop (OpSignext n) Tint e == Ebinop (OpShr SESigned) Tint Tint (Ebinop OpShl Tint Tint e (Eval (Eint y))) (Eval (Eint y)).

Proof.

  intros; intro; intros.
  assert (Hltu:Int.ltu y Int.iwordsize = true).
  unfold y.
  unfold Int.iwordsize.
  unfold Int.ltu.
  repeat rewrite Int.unsigned_repr.
  unfold zlt.
  destr_cond_match; try congruence; try omega.
  unfold Int.zwordsize, Int.max_unsigned; simpl; omega.
  split.
  destruct H.
  exploit (Z.sub_lt_le_mono n Int.zwordsize n n H0).
  omega.
  omega.
  cut (Int.zwordsize <= Int.max_unsigned).
  omega.
  unfold Int.zwordsize, Int.max_unsigned; simpl; omega.
  Opaque Z.sub.
  destr_wt.
  apply norm_eq''; simpl in *; intuition try congruence.
  des (tcheck_expr e); des s.
  des (tcheck_expr e); des s. inv e0.
  simpl; simpl_eval'.
  rewrite Int.sign_ext_shr_shl; auto.
  apply norm_eq_not_wt; simpl in *; auto.
  des (tcheck_expr e); des s.
Qed.

Lemma int_zero_ext_rew:
  forall n x,
    0 < n < Int.zwordsize ->
    let y := Int.zwordsize - n in
    Int.zero_ext n x = Int.repr (Int.unsigned (Int.mul x (Int.repr (two_p y))) / two_p y).

Proof.

  intros.
  assert (0 <= Int.zwordsize - n <= Int.max_unsigned).
  {
    change Int.zwordsize with 32 in *.
    change Int.max_unsigned with 4294967295. lia.
  }
  rewrite Int.zero_ext_shru_shl; auto.
  rewrite Int.shru_div_two_p.
  rewrite Int.unsigned_repr; auto.
  rewrite Int.shl_mul_two_p.
  rewrite Int.unsigned_repr; auto.
Qed.

Lemma normalise_zero_ext_shr_shl:
  forall (n : Z) (e : expr_sym),
  0 < n < Int.zwordsize ->
  let y := Int.repr (Int.zwordsize - n) in
  Eunop (OpZeroext n) Tint e == Ebinop (OpShr SEUnsigned) Tint Tint (Ebinop OpShl Tint Tint e (Eval (Eint y))) (Eval (Eint y)).

Proof.

  intros; intro; intros.
  Opaque Z.sub.
  destr_wt.
  apply norm_eq''; simpl in *; intuition try congruence.
  des (tcheck_expr e); des s.
  des (tcheck_expr e); des s; inv e0.
  assert (Int.ltu y Int.iwordsize = true).
  unfold y.
  unfold Int.iwordsize.
  revert H0 H1; clear; intros.
  unfold Int.ltu.
  repeat rewrite Int.unsigned_repr.
  unfold zlt.
  Transparent Z.sub.
  destr_cond_match; try congruence; try omega.
  unfold Int.zwordsize, Int.max_unsigned; simpl; omega.
  split.
  exploit (Z.sub_lt_le_mono n Int.zwordsize n n H1).
  omega.
  omega.
  cut (Int.zwordsize <= Int.max_unsigned).
  omega.
  unfold Int.zwordsize, Int.max_unsigned; simpl; omega.
  simpl_eval'.
  rewrite Int.zero_ext_shru_shl; auto.
  apply norm_eq_not_wt; simpl in *; auto.
  des (tcheck_expr e); des s.
Qed.

Hint Rewrite
     normalise_float_float
     normalise_int_int
     normalise_long_long
     normalise_ptr_ptr
     normalise_sign_ext_sign_ext
     normalise_sign_ext_zero_ext
     normalise_undef
     normalise_zero_ext_and
     normalise_zero_ext_sign_ext
     normalise_zero_ext_undef
     normalise_zero_ext_zero_ext
     normalize_mul_comm
     normalize_mul_one
     normalize_mul_zero
     normalize_plus_comm
     normalise_sign_ext_widen
: norm.