Module SelectOpproof


Correctness of instruction selection for operators

Require Import Coqlib.
Require Import AST Integers Floats.
Require Import Values Memory Builtins Globalenvs.
Require Import Cminor Op CminorSel.
Require Import SelectOp.
Require Import OpHelpers OpHelpersproof.
Require ExtValues.

Local Open Scope cminorsel_scope.
Local Transparent Archi.ptr64.

Useful lemmas and tactics


The following are trivial lemmas and custom tactics that help perform backward (inversion) and forward reasoning over the evaluation of operator applications.

Ltac EvalOp := eapply eval_Eop; eauto with evalexpr.

Ltac InvEval1 :=
  match goal with
  | [ H: (eval_expr _ _ _ _ _ (Eop _ Enil) _) |- _ ] =>
      inv H; InvEval1
  | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: Enil)) _) |- _ ] =>
      inv H; InvEval1
  | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: _ ::: Enil)) _) |- _ ] =>
      inv H; InvEval1
  | [ H: (eval_exprlist _ _ _ _ _ Enil _) |- _ ] =>
      inv H; InvEval1
  | [ H: (eval_exprlist _ _ _ _ _ (_ ::: _) _) |- _ ] =>
      inv H; InvEval1
  | _ =>
      idtac
  end.

Ltac InvEval2 :=
  match goal with
  | [ H: (eval_operation _ _ _ nil _ = Some _) |- _ ] =>
      simpl in H; inv H
  | [ H: (eval_operation _ _ _ (_ :: nil) _ = Some _) |- _ ] =>
      simpl in H; FuncInv
  | [ H: (eval_operation _ _ _ (_ :: _ :: nil) _ = Some _) |- _ ] =>
      simpl in H; FuncInv
  | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) _ = Some _) |- _ ] =>
      simpl in H; FuncInv
  | _ =>
      idtac
  end.

Ltac InvEval := InvEval1; InvEval2; InvEval2.

Ltac TrivialExists :=
  match goal with
  | [ |- exists v, _ /\ Val.lessdef ?a v ] => exists a; split; [EvalOp | auto]
  end.

Correctness of the smart constructors


Section CMCONSTR.
Variable prog: program.
Variable hf: helper_functions.
Hypothesis HELPERS: helper_functions_declared prog hf.
Let ge := Genv.globalenv prog.
Variable sp: val.
Variable e: env.
Variable m: mem.

We now show that the code generated by "smart constructor" functions such as Selection.notint behaves as expected. Continuing the notint example, we show that if the expression e evaluates to some integer value Vint n, then Selection.notint e evaluates to a value Vint (Int.not n) which is indeed the integer negation of the value of e. All proofs follow a common pattern:

Definition unary_constructor_sound (cstr: expr -> expr) (sem: val -> val) : Prop :=
  forall le a x,
  eval_expr ge sp e m le a x ->
  exists v, eval_expr ge sp e m le (cstr a) v /\ Val.lessdef (sem x) v.

Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> val -> val) : Prop :=
  forall le a x b y,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef (sem x y) v.

Theorem eval_addrsymbol:
  forall le id ofs,
  exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v.
Proof.
  intros. unfold addrsymbol. econstructor; split.
  EvalOp. simpl; eauto.
  auto.
Qed.

Theorem eval_addrstack:
  forall le ofs,
  exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.offset_ptr sp ofs) v.
Proof.
  intros. unfold addrstack. econstructor; split.
  EvalOp. simpl; eauto.
  auto.
Qed.

Theorem eval_notint: unary_constructor_sound notint Val.notint.
Proof.
  unfold notint; red; intros until x; case (notint_match a); intros; InvEval.
  TrivialExists.
  subst x. TrivialExists.
  exists v1; split; auto. subst. destruct v1; simpl; auto. rewrite Int.not_involutive; auto.
  exists (eval_shift s v1); split. EvalOp. subst x. destruct (eval_shift s v1); simpl; auto. rewrite Int.not_involutive; auto.
  subst x. rewrite Val.not_xor. rewrite Val.xor_assoc. TrivialExists.
  TrivialExists.
Qed.

Theorem eval_addimm:
  forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)).
Proof.
  red; unfold addimm; intros until x.
  predSpec Int.eq Int.eq_spec n Int.zero.
  { subst n. intros. exists x; split; auto.
    destruct x; simpl; auto.
    rewrite Int.add_zero. auto. rewrite Ptrofs.add_zero. auto. }
  case (addimm_match a); intros; InvEval; simpl.
  - TrivialExists; simpl. rewrite Int.add_commut. auto.
  - destruct (Compopts.optim_globaladdroffset tt).
    + TrivialExists; simpl. unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Ptrofs.add_commut; auto.
  + TrivialExists; simpl.
    repeat econstructor. reflexivity.
  - TrivialExists; simpl. destruct sp; simpl; auto. rewrite Ptrofs.add_assoc. do 3 f_equal. apply Ptrofs.add_commut.
  - TrivialExists; simpl. subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
  - TrivialExists; simpl.
Qed.

Lemma val_add_mul_neg_zero_eq:
  forall a b c,
    Val.add (Val.mul (Val.sub Vzero a) b) c = Val.sub c (Val.mul a b).
Proof.
  intros a b c.
  destruct a, b, c; cbn; auto.
  - f_equal. rewrite Int.sub_zero_r, <- Int.neg_mul_distr_l.
    rewrite Int.add_commut, <- Int.sub_add_opp. reflexivity.
  - f_equal. rewrite Int.sub_zero_r, <- Int.neg_mul_distr_l.
    rewrite Ptrofs.sub_add_opp. f_equal.
    apply Ptrofs.agree32_of_int_eq.
    apply Ptrofs.agree32_neg. reflexivity.
    apply Ptrofs.agree32_of_int. reflexivity.
Qed.

Lemma eval_match_neg:
  forall le ex t v,
    match_neg ex = Some t ->
    eval_expr ge sp e m le ex v ->
    exists v', eval_expr ge sp e m le t v' /\ v = Val.sub Vzero v'.
Proof.
  intros le0 ex t v MN EV.
  unfold match_neg in MN.
  destruct ex as [|op args| | | | | |]; try discriminate.
  destruct op; try discriminate.
  destruct args as [|arg1 args1tail]; try discriminate.
  destruct args1tail; try discriminate.
  destruct (Int.eq i Int.zero) eqn:Hi; try discriminate.
  inv MN.
  apply Int.same_if_eq in Hi. subst i.
  inv EV. inv H2. inv H6. simpl in H4. inv H4.
  exists v1; split; auto.
Qed.

Lemma eval_mls_or_mla:
  forall le e1 e2 e3 v1 v2 v3,
    eval_expr ge sp e m le e1 v1 ->
    eval_expr ge sp e m le e2 v2 ->
    eval_expr ge sp e m le e3 v3 ->
    exists v,
      eval_expr ge sp e m le (mls_or_mla e1 e2 e3) v
      /\ Val.lessdef (Val.add (Val.mul v1 v2) v3) v.
Proof.
  intros le e1 e2 e3 v1 v2 v3 EV1 EV2 EV3.
  assert (DEFAULT: exists v,
            eval_expr ge sp e m le (Eop Omla (e1:::e2:::e3:::Enil)) v
            /\ Val.lessdef (Val.add (Val.mul v1 v2) v3) v).
  { econstructor; split.
    repeat (econstructor; eauto). apply Val.lessdef_refl. }
  unfold mls_or_mla.
  destruct Archi.thumb2_support; [| exact DEFAULT].
  destruct (match_neg e1) as [t1|] eqn:MN1.
  - eapply eval_match_neg in MN1; eauto.
    destruct MN1 as (v1' & EV1' & ->).
    econstructor; split.
    repeat (econstructor; eauto).
    rewrite val_add_mul_neg_zero_eq. apply Val.lessdef_refl.
  - destruct (match_neg e2) as [t2|] eqn:MN2; [|exact DEFAULT].
    eapply eval_match_neg in MN2; eauto.
    destruct MN2 as (v2' & EV2' & ->).
    econstructor; split.
    repeat (econstructor; eauto).
    rewrite Val.mul_commut.
    rewrite val_add_mul_neg_zero_eq. apply Val.lessdef_refl.
Qed.

Theorem eval_add: binary_constructor_sound add Val.add.
Proof.
  red; intros until y.
  unfold add; case (add_match a b); intros; InvEval.
  rewrite Val.add_commut. apply eval_addimm; auto.
  apply eval_addimm; auto.
  subst.
  replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2)))
     with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))).
  apply eval_addimm. EvalOp.
  repeat rewrite Val.add_assoc. decEq. apply Val.add_permut.
  subst.
  replace (Val.add (Val.add v1 (Vint n1)) y)
     with (Val.add (Val.add v1 y) (Vint n1)).
  apply eval_addimm. EvalOp.
  repeat rewrite Val.add_assoc. decEq. apply Val.add_commut.
  subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp.
  subst. rewrite Val.add_commut. TrivialExists.
  subst. TrivialExists.
  (* case Eop Omul (t1:::t2:::Enil), t3 *)
  subst. apply eval_mls_or_mla; auto.
  (* case t1, Eop Omul (t2:::t3:::Enil) *)
  subst. rewrite Val.add_commut. apply eval_mls_or_mla; auto.
  TrivialExists.
Qed.

Theorem eval_rsubimm: forall n, unary_constructor_sound (rsubimm n) (fun v => Val.sub (Vint n) v).
Proof.
  red; intros until x. unfold rsubimm; case (rsubimm_match a); intros.
  InvEval. TrivialExists.
  InvEval. subst x. econstructor; split. EvalOp. unfold eval_operation; eauto.
  destruct v1; simpl; auto. rewrite Int.sub_add_r. rewrite <- Int.sub_add_opp.
  auto.
  InvEval. subst x. econstructor; split. EvalOp. simpl; eauto.
  fold (Val.sub (Vint m0) v1). destruct v1; simpl; auto.
  rewrite ! Int.sub_add_opp. rewrite Int.neg_add_distr. rewrite Int.neg_involutive.
  rewrite (Int.add_permut i). rewrite (Int.add_commut i). auto.
  TrivialExists.
Qed.

Theorem eval_sub: binary_constructor_sound sub Val.sub.
Proof.
  red; intros until y.
  unfold sub; case (sub_match a b); intros; InvEval.
  rewrite Val.sub_add_opp. apply eval_addimm; auto.
  subst. rewrite Val.sub_add_l. rewrite Val.sub_add_r.
    rewrite Val.add_assoc. simpl. rewrite Int.add_commut. rewrite <- Int.sub_add_opp.
  - apply eval_addimm; EvalOp.
  - subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp.
  - subst. rewrite Val.sub_add_r. apply eval_addimm; EvalOp.
  - apply eval_rsubimm; auto.
  - subst. TrivialExists.
  - subst. TrivialExists.
  - subst. destruct Archi.thumb2_support.
    + TrivialExists.
    + repeat econstructor; eassumption.
  - TrivialExists.
Qed.

Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v).
Proof.
  red; intros. unfold negint. apply eval_rsubimm; auto.
Qed.

Theorem eval_shlimm:
  forall n, unary_constructor_sound (fun a => shlimm a n)
                                    (fun x => Val.shl x (Vint n)).
Proof.
Opaque mk_shift_amount.
  red; intros until x. unfold shlimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shl_zero; auto.
  destruct (Int.ltu n Int.iwordsize) eqn:?; simpl.
  destruct (shlimm_match a); intros.
  InvEval. simpl; rewrite Heqb. TrivialExists.
  destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
  InvEval. subst x. exists (Val.shl v1 (Vint (Int.add n n1))); split. EvalOp.
  simpl. rewrite mk_shift_amount_eq; auto.
  destruct v1; simpl; auto. rewrite s_range. simpl. rewrite Heqb. rewrite Heqb0.
  rewrite Int.add_commut. rewrite Int.shl_shl; auto. apply s_range. rewrite Int.add_commut; auto.
  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto.
  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto.
  intros; TrivialExists. simpl. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto.
Qed.

 Theorem eval_shrimm:
  forall n, unary_constructor_sound (fun a => shrimm a n)
                                    (fun x => Val.shr x (Vint n)).
Proof.
  red; intros until x. unfold shrimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
  destruct (Int.ltu n Int.iwordsize) eqn:?; simpl.
  destruct (shrimm_match a); intros.
  - InvEval. simpl; rewrite Heqb. TrivialExists.
  - destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
    InvEval. subst x. exists (Val.shr v1 (Vint (Int.add n n1))); split. EvalOp.
    simpl. rewrite mk_shift_amount_eq; auto.
    destruct v1; simpl; auto. rewrite s_range. simpl. rewrite Heqb. rewrite Heqb0.
    rewrite Int.add_commut. rewrite Int.shr_shr; auto. apply s_range. rewrite Int.add_commut; auto.
    TrivialExists. simpl. rewrite mk_shift_amount_eq; auto.
  - destruct (_ && _) eqn:SPECIAL; cycle 1.
    { TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. }
    repeat rewrite andb_true_iff in SPECIAL.
    rewrite negb_true_iff in SPECIAL.
    destruct SPECIAL as [[THUMB LTU_n1] LTU_n_n1].
    InvEval. TrivialExists. simpl. f_equal. subst x.
    destruct v1; cbn; try reflexivity.
    rewrite LTU_n1. cbn.
    rewrite Heqb.
    rewrite Int.shr_shl2 by assumption. rewrite LTU_n_n1.
    unfold Int.ltu in *.
    destruct (zlt (Int.unsigned n) (Int.unsigned Int.iwordsize)) as [less1 | ]; [clear Heqb | discriminate].
    destruct (zlt (Int.unsigned n1) (Int.unsigned Int.iwordsize)) as [less2 | ]; [clear LTU_n1 | discriminate].
    destruct (zlt (Int.unsigned n) (Int.unsigned n1)) as [| less3]; [discriminate | clear LTU_n_n1].
    pose proof (Int.unsigned_range n) as n_RANGE.
    pose proof (Int.unsigned_range n1) as n1_RANGE.
    change Int.modulus with 4294967296 in *.
    change (Int.unsigned Int.iwordsize) with 32 in *.
    destruct zlt; cycle 1.
    { unfold Int.sub in g.
       rewrite Int.unsigned_repr in g by (change Int.max_unsigned with 4294967295 in * ; lia).
       lia.
    }
    unfold Int.sub in l.
    rewrite Int.unsigned_repr in l by (change Int.max_unsigned with 4294967295 in * ; lia).
    Opaque Z.sub. cbn. f_equal. f_equal.
    unfold Int.sub.
    rewrite Int.unsigned_repr.
    all: change (Int.unsigned Int.iwordsize) with 32 in *.
    all: change Int.max_unsigned with 4294967295 in *.
    all: lia.
  - TrivialExists. simpl. rewrite mk_shift_amount_eq; auto.
  - intros; TrivialExists. simpl. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto.
Qed.

Theorem eval_shruimm:
  forall n, unary_constructor_sound (fun a => shruimm a n)
                                    (fun x => Val.shru x (Vint n)).
Proof.
  red; intros until x. unfold shruimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto.
  destruct (Int.ltu n Int.iwordsize) eqn:?; simpl.
  destruct (shruimm_match a); intros.
  - InvEval. simpl; rewrite Heqb. TrivialExists.
  - destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
  InvEval. subst x. exists (Val.shru v1 (Vint (Int.add n n1))); split. EvalOp.
  simpl. rewrite mk_shift_amount_eq; auto.
  destruct v1; simpl; auto. destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto.
  rewrite Heqb; rewrite Heqb0. rewrite Int.add_commut. rewrite Int.shru_shru; auto. rewrite Int.add_commut; auto.
  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto.
  - destruct (_ && _) eqn:SPECIAL; cycle 1.
    { TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. }
    repeat rewrite andb_true_iff in SPECIAL.
    rewrite negb_true_iff in SPECIAL.
    destruct SPECIAL as [[THUMB LTU_n1] LTU_n_n1].
    InvEval. TrivialExists. simpl. f_equal. subst x.
    destruct v1; cbn; try reflexivity.
    rewrite LTU_n1. cbn.
    rewrite Heqb.
    rewrite Int.shru_shl by assumption. rewrite LTU_n_n1.
    unfold Int.ltu in *.
    destruct (zlt (Int.unsigned n) (Int.unsigned Int.iwordsize)) as [less1 | ]; [clear Heqb | discriminate].
    destruct (zlt (Int.unsigned n1) (Int.unsigned Int.iwordsize)) as [less2 | ]; [clear LTU_n1 | discriminate].
    destruct (zlt (Int.unsigned n) (Int.unsigned n1)) as [| less3]; [discriminate | clear LTU_n_n1].
    pose proof (Int.unsigned_range n) as n_RANGE.
    pose proof (Int.unsigned_range n1) as n1_RANGE.
    change Int.modulus with 4294967296 in *.
    change (Int.unsigned Int.iwordsize) with 32 in *.
    destruct zlt; cycle 1.
    { unfold Int.sub in g.
       rewrite Int.unsigned_repr in g by (change Int.max_unsigned with 4294967295 in * ; lia).
       lia.
    }
    unfold Int.sub in l.
    rewrite Int.unsigned_repr in l by (change Int.max_unsigned with 4294967295 in * ; lia).
    Opaque Z.sub. cbn. f_equal. f_equal.
    unfold Int.sub.
    rewrite Int.unsigned_repr.
    all: change (Int.unsigned Int.iwordsize) with 32 in *.
    all: change Int.max_unsigned with 4294967295 in *.
    all: lia.
  - TrivialExists. simpl. rewrite mk_shift_amount_eq; auto.
  - intros; TrivialExists. simpl. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto.
Qed.

Lemma eval_mulimm_base:
  forall n, unary_constructor_sound (mulimm_base n) (fun x => Val.mul x (Vint n)).
Proof.
  intros; red; intros; unfold mulimm_base.
  assert (DFL: exists v, eval_expr ge sp e m le (Eop Omul (Eop (Ointconst n) Enil ::: a ::: Enil)) v /\ Val.lessdef (Val.mul x (Vint n)) v).
  TrivialExists. econstructor. EvalOp. simpl; eauto. econstructor. eauto. constructor.
  rewrite Val.mul_commut. auto.
  assert (RSB: forall k, Int.one_bits (Int.add n Int.one) = k :: nil ->
    Int.ltu k Int.iwordsize = true ->
    exists v, eval_expr ge sp e m le
      (Elet a (Eop (Orsubshift (Slsl (mk_shift_amount k))) (Eletvar 0 ::: Eletvar 0 ::: Enil))) v
      /\ Val.lessdef (Val.mul x (Vint n)) v).
  { intros k HBITS HLTU.
    generalize (Int.one_bits_decomp (Int.add n Int.one)).
    rewrite HBITS. simpl. rewrite Int.add_zero. intros HDECOMP.
    assert (HN: n = Int.sub (Int.shl Int.one k) Int.one).
    { assert (Int.add n Int.one = Int.shl Int.one k) as HADD by exact HDECOMP.
      apply (f_equal (fun y => Int.add y (Int.neg Int.one))) in HADD.
      rewrite Int.add_assoc in HADD. rewrite Int.add_neg_zero in HADD.
      rewrite Int.add_zero in HADD. rewrite Int.sub_add_opp. auto. }
    exists (Val.sub (Val.shl x (Vint k)) x).
    split;
    [ eapply eval_Elet; eauto;
      apply eval_Eop with (vl := x :: x :: nil);
      [apply eval_Econs; [apply eval_Eletvar; reflexivity |
       apply eval_Econs; [apply eval_Eletvar; reflexivity |
       apply eval_Enil]] |
       assert (HLTU': Int.ltu k Int.iwordsize = true) by
         (apply (Int.one_bits_range (Int.add n Int.one));
          rewrite HBITS; auto with coqlib);
       simpl; unfold eval_shift;
       rewrite (mk_shift_amount_eq k HLTU'); reflexivity]
    | rewrite HN;
      assert (HLTU': Int.ltu k Int.iwordsize = true) by
        (apply (Int.one_bits_range (Int.add n Int.one));
         rewrite HBITS; auto with coqlib);
      destruct x; simpl; auto;
      rewrite HLTU'; simpl; f_equal;
      rewrite Int.sub_add_opp; rewrite Int.sub_add_opp;
      rewrite Int.mul_add_distr_r;
      rewrite <- Int.shl_mul;
      rewrite <- Int.neg_mul_distr_r; rewrite Int.mul_one;
      rewrite <- Int.sub_add_opp; apply Val.lessdef_refl ]. }
  assert (SUB: forall k, Int.one_bits (Int.add (Int.neg n) Int.one) = k :: nil ->
    Int.ltu k Int.iwordsize = true ->
    exists v, eval_expr ge sp e m le
      (Elet a (Eop (Osubshift (Slsl (mk_shift_amount k))) (Eletvar 0 ::: Eletvar 0 ::: Enil))) v
      /\ Val.lessdef (Val.mul x (Vint n)) v).
  { intros k HBITS HLTU.
    generalize (Int.one_bits_decomp (Int.add (Int.neg n) Int.one)).
    rewrite HBITS. simpl. rewrite Int.add_zero. intros HDECOMP.
    assert (HN: n = Int.sub Int.one (Int.shl Int.one k)).
    { apply (f_equal Int.neg) in HDECOMP.
      rewrite Int.neg_add_distr in HDECOMP.
      rewrite Int.neg_involutive in HDECOMP.
      apply (f_equal (fun y => Int.add y Int.one)) in HDECOMP.
      rewrite Int.add_assoc in HDECOMP.
      rewrite (Int.add_commut (Int.neg Int.one) Int.one) in HDECOMP.
      rewrite Int.add_neg_zero in HDECOMP.
      rewrite Int.add_zero in HDECOMP.
      rewrite HDECOMP.
      rewrite Int.add_commut.
      symmetry. apply Int.sub_add_opp. }
    exists (Val.sub x (Val.shl x (Vint k))).
    split;
    [ eapply eval_Elet; eauto;
      apply eval_Eop with (vl := x :: x :: nil);
      [apply eval_Econs; [apply eval_Eletvar; reflexivity |
       apply eval_Econs; [apply eval_Eletvar; reflexivity |
       apply eval_Enil]] |
       simpl; unfold eval_shift;
       rewrite (mk_shift_amount_eq k HLTU); reflexivity]
    | rewrite HN;
      destruct x; simpl; auto;
      rewrite HLTU; simpl; f_equal;
      rewrite Int.sub_add_opp; rewrite Int.sub_add_opp;
      rewrite Int.mul_add_distr_r;
      rewrite Int.mul_one;
      rewrite <- Int.neg_mul_distr_r;
      rewrite <- Int.shl_mul;
      apply Val.lessdef_refl ]. }
  (* Common tactic for the [Int.one_bits n] = nil or 3+ bits cases:
     the inner [match Int.one_bits (Int.add n Int.one) with ...] is fully
     handled by RSB on the [k :: nil] branch and SUB on the empty/2+ branches. *)
  assert (TRY_BOTH:
    exists v, eval_expr ge sp e m le
      (match Int.one_bits (Int.add n Int.one) with
       | k :: nil =>
           if Int.ltu k Int.iwordsize then
             Elet a (Eop (Orsubshift (Slsl (mk_shift_amount k)))
                         (Eletvar 0 ::: Eletvar 0 ::: Enil))
           else Eop Omul (Eop (Ointconst n) Enil ::: a ::: Enil)
       | _ =>
           match Int.one_bits (Int.add (Int.neg n) Int.one) with
           | k :: nil =>
               if Int.ltu k Int.iwordsize then
                 Elet a (Eop (Osubshift (Slsl (mk_shift_amount k)))
                             (Eletvar 0 ::: Eletvar 0 ::: Enil))
               else Eop Omul (Eop (Ointconst n) Enil ::: a ::: Enil)
           | _ => Eop Omul (Eop (Ointconst n) Enil ::: a ::: Enil)
           end
       end) v
      /\ Val.lessdef (Val.mul x (Vint n)) v).
  { destruct (Int.one_bits (Int.add n Int.one)) as [|k [| ? ?]] eqn:HBITS.
    - destruct (Int.one_bits (Int.add (Int.neg n) Int.one)) as [|k2 [| ? ?]] eqn:HBITS2;
        [auto | | auto].
      destruct (Int.ltu k2 Int.iwordsize) eqn:HLTU2; [| auto].
      apply SUB; auto.
    - destruct (Int.ltu k Int.iwordsize) eqn:HLTU; [| auto].
      apply RSB; auto.
    - destruct (Int.one_bits (Int.add (Int.neg n) Int.one)) as [|k2 [| ? ?]] eqn:HBITS2;
        [auto | | auto].
      destruct (Int.ltu k2 Int.iwordsize) eqn:HLTU2; [| auto].
      apply SUB; auto. }
  generalize (Int.one_bits_decomp n).
  generalize (Int.one_bits_range n).
  destruct (Int.one_bits n) as [|i [|j [|? ?]]].
- (* nil *)
  intros _ _. exact TRY_BOTH.
- (* i :: nil *)
  intros. rewrite H1. simpl.
  rewrite Int.add_zero.
  replace (Vint (Int.shl Int.one i)) with (Val.shl Vone (Vint i)). rewrite Val.shl_mul.
  apply eval_shlimm. auto. simpl. rewrite H0; auto with coqlib.
- (* i :: j :: nil *)
  intros. rewrite H1. simpl.
  exploit (eval_shlimm i (x :: le) (Eletvar 0) x). constructor; auto. intros [v1 [A1 B1]].
  exploit (eval_shlimm j (x :: le) (Eletvar 0) x). constructor; auto. intros [v2 [A2 B2]].
  exploit (eval_add (x :: le)). eexact A1. eexact A2. intros [v [A B]].
  exists v; split. econstructor; eauto.
  rewrite Int.add_zero.
  replace (Vint (Int.add (Int.shl Int.one i) (Int.shl Int.one j)))
     with (Val.add (Val.shl Vone (Vint i)) (Val.shl Vone (Vint j))).
  rewrite Val.mul_add_distr_r.
  repeat rewrite Val.shl_mul. eapply Val.lessdef_trans. 2: eauto. apply Val.add_lessdef; auto.
  simpl. repeat rewrite H0; auto with coqlib.
- (* 3+ bits *)
  intros _ _. exact TRY_BOTH.
Qed.


Theorem eval_mulimm:
  forall n, unary_constructor_sound (mulimm n) (fun x => Val.mul x (Vint n)).
Proof.
  intros; red; intros until x; unfold mulimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  intros. exists (Vint Int.zero); split. EvalOp.
  destruct x; simpl; auto. subst n. rewrite Int.mul_zero. auto.
  predSpec Int.eq Int.eq_spec n Int.one.
  intros. exists x; split; auto.
  destruct x; simpl; auto. subst n. rewrite Int.mul_one. auto.
  case (mulimm_match a); intros; InvEval.
  TrivialExists. simpl. rewrite Int.mul_commut; auto.
  subst. rewrite Val.mul_add_distr_l.
  exploit eval_mulimm_base; eauto. instantiate (1 := n). intros [v' [A1 B1]].
  exploit (eval_addimm (Int.mul n n2) le (mulimm_base n t2) v'). auto. intros [v'' [A2 B2]].
  exists v''; split; auto. eapply Val.lessdef_trans. eapply Val.add_lessdef; eauto.
  rewrite Val.mul_commut; auto.
  apply eval_mulimm_base; auto.
Qed.

Theorem eval_mul: binary_constructor_sound mul Val.mul.
Proof.
  red; intros until y.
  unfold mul; case (mul_match a b); intros; InvEval.
  rewrite Val.mul_commut. apply eval_mulimm. auto.
  apply eval_mulimm. auto.
  TrivialExists.
Qed.

Theorem eval_mulhs: binary_constructor_sound mulhs Val.mulhs.
Proof.
  unfold mulhs; red; intros; TrivialExists.
Qed.
  
Theorem eval_mulhu: binary_constructor_sound mulhu Val.mulhu.
Proof.
  unfold mulhu; red; intros; TrivialExists.
Qed.

Lemma ones_max_range:
  forall h ma (RANGE : 0 <= h <= ma),
    0 <= Z.ones h < 2^ma.
Proof.
  intros. rewrite Z.ones_equiv.
  assert (0 < 2^h).
  { apply Z.pow_pos_nonneg; lia. }
  assert (2^h <= 2^ma).
  { apply Z.pow_le_mono_r; lia. }
  lia.
Qed.

Lemma ones_max_range32:
  forall h (RANGE : 0 <= h <= 32),
    0 <= Z.ones h <= Int.max_unsigned.
Proof.
  intros.
  pose proof (ones_max_range h 32 RANGE).
  change (Int.max_unsigned) with (2^32-1).
  lia.
Qed.

Lemma and_max_unsigned:
  forall i, (Int.and i (Int.repr 4294967295)) = i.
Proof.
  intros.
  replace (Int.repr 4294967295) with Int.mone.
  apply Int.and_mone.
  unfold Int.mone.
  change 4294967295 with (Int.unsigned Int.mone).
  rewrite Int.repr_unsigned.
  reflexivity.
Qed.
  
Theorem eval_andimm:
  forall n, unary_constructor_sound (andimm n) (fun x => Val.and x (Vint n)).
Proof.
  intros; red; intros until x. unfold andimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  { intros. exists (Vint Int.zero); split. EvalOp.
  destruct x; simpl; auto. subst n. rewrite Int.and_zero. auto. }
  predSpec Int.eq Int.eq_spec n Int.mone.
  { intros. exists x; split; auto.
    subst. destruct x; simpl; auto. rewrite Int.and_mone; auto. }
  case (andimm_match a); intros.
  - (* Eop (Ointconst n2) Enil — both constants, fold immediately. *)
    InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto.
  - (* Eop (Oandimm n2) (t2:::Enil) — chained mask, fold the masks. *)
    InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists.
  - (* Eload Mint8unsigned — load already zero-extends to byte; if mask
       covers the whole byte the [Oandimm] is identity. *)
    predSpec Int.eq Int.eq_spec n (Int.repr 255).
    { subst n. exists x; split; [assumption|].
      match goal with [HE: eval_expr _ _ _ _ _ (Eload _ _ _) _ |- _] => inv HE end.
      unfold Mem.loadv in *. destruct vaddr; try discriminate.
      exploit Mem.load_cast; eauto. simpl. intros HX.
      rewrite <- Val.cast8unsigned_and. rewrite <- HX. apply Val.lessdef_refl. }
    TrivialExists.
  - (* Eload Mint16unsigned — same idea for halfword. *)
    predSpec Int.eq Int.eq_spec n (Int.repr 65535).
    { subst n. exists x; split; [assumption|].
      match goal with [HE: eval_expr _ _ _ _ _ (Eload _ _ _) _ |- _] => inv HE end.
      unfold Mem.loadv in *. destruct vaddr; try discriminate.
      exploit Mem.load_cast; eauto. simpl. intros HX.
      rewrite <- Val.cast16unsigned_and. rewrite <- HX. apply Val.lessdef_refl. }
    TrivialExists.
  - (* Eop (Oshift (Slsr lsb)) (e3:::Enil) — `(e3 >> lsb) & n` *)
    unfold andimm_lsr_to_ubfx.
    destruct (Archi.thumb2_support && Compopts.bitfield_ops tt) eqn:OPT;
      [| TrivialExists].
    destruct (Int.is_power2 (Int.add n Int.one)) as [sz|] eqn:POW2;
      [| TrivialExists].
    destruct (negb (Int.ltu Int.iwordsize (Int.add lsb sz))) eqn:RANGE;
      [| TrivialExists].
    (* Emit [Eop (Oubfx lsb sz) (e3:::Enil)]. *)
    InvEval. subst x.
    pose proof (Int.is_power2_correct _ _ POW2) as Pcorr.
    pose proof (Int.is_power2_range _ _ POW2) as Prange.
    apply Int.ltu_iwordsize_inv in Prange.
    change Int.zwordsize with 32 in Prange.
    pose proof (Int.two_p_range (Int.unsigned sz)) as Tprange.
    change Int.zwordsize with 32 in Tprange.
    specialize (Tprange ltac:(lia)).
    change Int.max_unsigned with 4294967295 in Tprange.
    pose proof (Int.unsigned_range n) as Hnr.
    change Int.modulus with 4294967296 in Hnr.
    pose proof (two_p_gt_ZERO (Int.unsigned sz)) as TPpos.
    assert (UN: Int.unsigned n = two_p (Int.unsigned sz) - 1).
    { rewrite Int.add_unsigned in Pcorr.
      change (Int.unsigned Int.one) with 1 in Pcorr.
      rewrite Int.unsigned_repr_eq in Pcorr.
      change Int.modulus with 4294967296 in Pcorr.
      destruct (Z_lt_dec (Int.unsigned n + 1) 4294967296) as [LT|GE].
      - rewrite Z.mod_small in Pcorr by lia. lia.
      - assert (HE: Int.unsigned n + 1 = 4294967296) by lia.
        rewrite HE in Pcorr.
        rewrite Z.mod_same in Pcorr by lia. lia. }
    assert (NMASK: n = Int.repr (two_p (Int.unsigned sz) - 1)).
    { rewrite <- UN. symmetry. apply Int.repr_unsigned. }
    eexists; split.
    + (* eval Oubfx *)
      eapply eval_Eop. econstructor; [eassumption|econstructor]. cbn. reflexivity.
    + (* lessdef Val.and x (Vint n) ⇐ Val.zero_ext (unsigned sz) x *)
      rewrite NMASK.
      destruct (Val.shru v1 (Vint lsb)) eqn:?; cbn; auto.
      apply Val.lessdef_same. f_equal.
      rewrite Int.zero_ext_and by lia.
      reflexivity.
  - (* default arm — fall through to bfc/ubfx fast paths or final
       [Oandimm] emission.  The GADT case split introduced a fresh [e2]
       (also bound as [a] in the lemma); use [e2] in the body. *)
  destruct (_ && _) eqn:CHOICE.
  { rewrite andb_true_iff in CHOICE.
    destruct CHOICE as [_ CHOICE].
    pose proof (Int.same_if_eq _ _ CHOICE) as EQn.
    intros. unfold ubfx.
    pose proof (ExtValues.int_highest_bit_range n) as HIGH_RANGE.
    destruct (ubfx_match e2).
    { InvEval. subst. TrivialExists. cbn. f_equal.
      destruct v1; cbn; trivial.
      unfold Int.ltu.
      destruct zlt as [LT | GE]; cbn; trivial.
      change (Int.unsigned Int.iwordsize) with 32 in *.
      f_equal.
      rewrite Int.unsigned_repr; cycle 1.
      { change Int.max_unsigned with 4294967295. lia. }
      rewrite EQn at 2. unfold ExtValues.zbitfield_mask.
      rewrite Int.zero_ext_and by lia.
      rewrite Z.sub_1_r. rewrite Z.sub_0_r.
      rewrite Z.shiftl_0_r.
      replace (two_p
          (Z.min (Z.succ (ExtValues.int_highest_bit n))
                 (32 - Int.unsigned lsb))) with
        (1 * (two_p (Z.min (Z.succ (ExtValues.int_highest_bit n))
                 (32 - Int.unsigned lsb)))) by ring.
      rewrite <- Zbits.Zshiftl_mul_two_p by lia.
      fold (Z.ones (Z.min (Z.succ (ExtValues.int_highest_bit n))
                          (32 - Int.unsigned lsb))).
      Int.bit_solve.
      rewrite Int.testbit_repr by assumption.
      rewrite Int.testbit_repr by assumption.
      rewrite Z.testbit_ones_nonneg by lia.
      rewrite Z.testbit_ones_nonneg by lia.
      change Int.zwordsize with 32 in *.
      destruct (Z_lt_ge_dec (i0 + Int.unsigned lsb) 32) as [LT' | GE']; cycle 1.
      { rewrite zlt_false by assumption. reflexivity. }
      rewrite zlt_true by assumption.
      f_equal. lia.
    }
    InvEval.
    destruct zlt; cycle 1.
    { exists x. split. assumption. rewrite EQn.
      replace (ExtValues.int_highest_bit n) with 31 by lia.
      change (ExtValues.zbitfield_mask 31 0) with 4294967295.
      destruct x; cbn; trivial.
      rewrite and_max_unsigned. constructor.
    }
    TrivialExists. cbn. f_equal.
    unfold ExtValues.clearf, ExtValues.is_bitfield.
    rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia).
    rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia).
    replace ((Z.succ (ExtValues.int_highest_bit n) +
                (32 - Z.succ (ExtValues.int_highest_bit n)))) with 32 by lia.
    rewrite Z.leb_refl.
    destruct x; trivial. cbn. f_equal.
    unfold ExtValues.bitfield_mask.
    rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia).
    Int.bit_solve.
    rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia).
    unfold ExtValues.zbitfield_mask.
    destruct (Z_lt_ge_dec i0 (Z.succ (ExtValues.int_highest_bit n))) as [LT | GE].
    { rewrite zlt_true by lia. cbn. rewrite andb_true_r.
      rewrite EQn.
      unfold ExtValues.zbitfield_mask.
      rewrite Int.testbit_repr by lia.
      rewrite Z.sub_0_r. rewrite Z.shiftl_0_r.
      rewrite Z.ones_spec_low.
      { rewrite andb_true_r. reflexivity. }
      lia.
    }
    rewrite zlt_false by lia.
    rewrite Int.testbit_repr by lia.
    rewrite Z.testbit_ones_nonneg by lia.
    replace (i0 - Z.succ (ExtValues.int_highest_bit n) <?
               32 - Z.succ (ExtValues.int_highest_bit n)) with true by (change Int.zwordsize with 32 in *; lia).
    cbn. rewrite andb_false_r.
    replace (Int.testbit n i0) with false.
    { rewrite andb_false_r. reflexivity. }
    rewrite EQn.
    rewrite Int.testbit_repr by lia.
    unfold ExtValues.zbitfield_mask.
    rewrite Z.sub_0_r. rewrite Z.shiftl_0_r.
    rewrite Z.ones_spec_high. reflexivity.
    lia.
  }
  clear CHOICE.
  destruct (_ && _) eqn:CHOICE.
  { rewrite andb_true_iff in CHOICE.
    destruct CHOICE as [_ CHOICE].
    pose proof (Int.same_if_eq _ _ CHOICE) as EQn.
    intros. TrivialExists. simpl. f_equal.
    unfold ExtValues.clearf, ExtValues.is_bitfield, ExtValues.bitfield_mask.
    pose proof (ExtValues.int_highest_bit_range (Int.not n)) as HIGH.
    pose proof (ExtValues.int_lowest_bit_range (Int.not n)) as LOW.
    pose proof (ExtValues.int_lowest_highest_bit (Int.not n)) as LEQ.
    replace (_ <=? _) with true; cycle 1.
    { repeat rewrite Int.unsigned_repr by
        (change Int.max_unsigned with 4294967295; lia).
      symmetry.
      apply Zle_imp_le_bool.
      lia.
    }
    rewrite EQn at 4. f_equal. simpl. f_equal. f_equal.
    unfold ExtValues.zbitfield_mask. unfold Int.shl.
    f_equal. f_equal.
    rewrite Int.unsigned_repr; cycle 1.
    { apply ones_max_range32.
      rewrite Int.unsigned_repr by
        (change Int.max_unsigned with 4294967295; lia).
      lia.
    }
    rewrite Int.unsigned_repr by
      (change Int.max_unsigned with 4294967295; lia).
    reflexivity.
    apply Int.unsigned_repr.
    change Int.max_unsigned with 4294967295; lia.
  }
  TrivialExists.
Qed.

Theorem eval_and: binary_constructor_sound and Val.and.
Proof.
  red; intros until y; unfold and; case (and_match a b); intros; InvEval.
  TrivialExists.
  rewrite Val.and_commut. apply eval_andimm; auto.
  apply eval_andimm; auto.
  subst. rewrite Val.and_commut. TrivialExists.
  subst. TrivialExists.
  subst. rewrite Val.and_commut. TrivialExists.
  subst. TrivialExists.
  subst. rewrite Val.and_commut. TrivialExists.
  subst. TrivialExists.
  TrivialExists.
Qed.


Theorem eval_orimm:
  forall n, unary_constructor_sound (orimm n) (fun x => Val.or x (Vint n)).
Proof.
  intros; red; intros until x. unfold orimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  intros. subst. exists x; split; auto.
  destruct x; simpl; auto. rewrite Int.or_zero; auto.
  predSpec Int.eq Int.eq_spec n Int.mone.
  intros. exists (Vint Int.mone); split. EvalOp.
  destruct x; simpl; auto. subst n. rewrite Int.or_mone. auto.
  destruct (orimm_match a); intros; InvEval.
  TrivialExists. simpl. rewrite Int.or_commut; auto.
  subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists.
  TrivialExists.
Qed.

Scheme expr_ind2 := Induction for expr Sort Prop
  with exprlist_ind2 := Induction for exprlist Sort Prop
  with condexpr_ind2 := Induction for condexpr Sort Prop.

Remark eval_same_expr:
  forall a1 a2 le v1 v2,
  same_expr_pure a1 a2 = true ->
  eval_expr ge sp e m le a1 v1 ->
  eval_expr ge sp e m le a2 v2 ->
  a1 = a2 /\ v1 = v2.
Proof.
  intros a1.
  apply (expr_ind2
    (fun a1 => forall a2 le v1 v2,
      same_expr_pure a1 a2 = true ->
      eval_expr ge sp e m le a1 v1 ->
      eval_expr ge sp e m le a2 v2 ->
      a1 = a2 /\ v1 = v2)
    (fun es1 => forall es2 le vs1 vs2,
      same_exprlist_pure es1 es2 = true ->
      eval_exprlist ge sp e m le es1 vs1 ->
      eval_exprlist ge sp e m le es2 vs2 ->
      es1 = es2 /\ vs1 = vs2)
    (fun _ => True)); intros; auto.
  - (* Evar v *)
    destruct a2; simpl in H; try discriminate.
    destruct (ident_eq i i0); try discriminate.
    subst i0. inv H0. inv H1. split; congruence.
  - (* Eop op args *)
    destruct a2; simpl in H0; try discriminate.
    destruct (eq_operation o o0); try discriminate. subst o0.
    inv H1. inv H2.
    exploit H; eauto. intros [Es Evs]. subst e0 vl0.
    split; [reflexivity | congruence].
  - (* Eload chunk addr args *)
    destruct a2; simpl in H0; try discriminate.
    destruct (chunk_eq m0 m1); try discriminate.
    destruct (eq_addressing a a0); try discriminate. subst m1 a0.
    inv H1. inv H2.
    exploit H; eauto. intros [Es Evs]. subst e0 vl0.
    split; [reflexivity | congruence].
  - (* Econdition *) destruct a2; simpl in H1; discriminate.
  - (* Elet *) destruct a2; simpl in H1; discriminate.
  - (* Eletvar *) destruct a2; simpl in H; discriminate.
  - (* Ebuiltin *) destruct a2; simpl in H0; discriminate.
  - (* Eexternal *) destruct a2; simpl in H0; discriminate.
  - (* Enil *)
    destruct es2; simpl in H; try discriminate.
    inv H0. inv H1. split; reflexivity.
  - (* Econs *)
    destruct es2 as [|e2 es2']; simpl in H1; try discriminate.
    destruct (same_expr_pure e0 e2) eqn:Sa; try discriminate.
    inv H2. inv H3.
    exploit H; eauto. intros [Ea Eva]. subst e2 v0.
    exploit H0; eauto. intros [Es Evs]. subst es2' vl0.
    split; reflexivity.
Qed.

Lemma shifted_masks:
  forall sz, 0 <= sz <= 32 ->
  Int.shl (Int.repr (Z.ones sz)) Int.zero =
    Int.not (Int.shl (Int.repr (Z.ones (32 - sz))) (Int.repr sz)).
Proof.
  intros. apply Int.same_bits_eq. intros.
  rewrite Int.bits_shl by assumption.
  change (Int.unsigned Int.zero) with 0.
  rewrite zlt_false by lia.
  rewrite Z.sub_0_r.
  rewrite Int.bits_not by assumption.
  rewrite Int.bits_shl by assumption.
  unfold Int.testbit.
  rewrite Int.unsigned_repr by
    (apply ones_max_range32; assumption).
  rewrite Int.unsigned_repr by
    (change Int.max_unsigned with 4294967295; lia).
  rewrite Z.testbit_ones_nonneg by lia.
  unfold zlt.
  rewrite Int.unsigned_repr by
    (apply ones_max_range32; lia).
  change Int.zwordsize with 32 in *.
  destruct Z_lt_dec; cbn. lia.
  rewrite Z.testbit_ones_nonneg by lia.
  lia.
Qed.

Lemma val_or_shru_shl_ror_lessdef:
  forall v vn,
  Val.lessdef
    (Val.or (Val.shru v vn)
            (Val.shl v (Val.sub (Vint Int.iwordsize) vn)))
    (Val.ror v vn).
Proof.
  intros. destruct vn as [|n| | | |]; simpl; try (destruct v; simpl; auto; fail).
  destruct v; simpl; auto.
  destruct (Int.ltu n Int.iwordsize) eqn:LT; cycle 1.
  { simpl. auto. }
  destruct (Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize) eqn:LT'; cycle 1.
  { simpl. auto. }
  simpl. apply Val.lessdef_same. f_equal.
  rewrite Int.or_commut. symmetry. apply Int.or_ror; auto.
  rewrite Int.sub_add_opp. rewrite Int.add_assoc.
  rewrite (Int.add_commut (Int.neg n) n). rewrite Int.add_neg_zero.
  apply Int.add_zero.
Qed.

Lemma val_or_shl_shru_ror_lessdef:
  forall v vn,
  Val.lessdef
    (Val.or (Val.shl v (Val.sub (Vint Int.iwordsize) vn))
            (Val.shru v vn))
    (Val.ror v vn).
Proof.
  intros. rewrite Val.or_commut. apply val_or_shru_shl_ror_lessdef.
Qed.

Lemma val_or_shl_shru_rolimm_lessdef:
  forall v vn,
  Val.lessdef
    (Val.or (Val.shl v vn)
            (Val.shru v (Val.sub (Vint Int.iwordsize) vn)))
    (Val.ror v (Val.sub (Vint Int.iwordsize) vn)).
Proof.
  intros. destruct vn as [|n| | | |]; cbn; try (destruct v; cbn; auto; fail).
  destruct v; cbn; auto.
  destruct (Int.ltu n Int.iwordsize) eqn:LT; cycle 1.
  { cbn. auto. }
  destruct (Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize) eqn:LT'; cycle 1.
  { cbn. auto. }
  cbn. apply Val.lessdef_same. f_equal.
  symmetry. apply Int.or_ror; auto.
  rewrite Int.add_commut.
  rewrite Int.sub_add_opp. rewrite Int.add_assoc.
  rewrite (Int.add_commut (Int.neg n) n). rewrite Int.add_neg_zero.
  apply Int.add_zero.
Qed.

Theorem eval_or: binary_constructor_sound or Val.or.
Proof.
  red; intros until y; unfold or; case (or_match a b); intros; InvEval.
  - TrivialExists.
  - rewrite Val.or_commut. apply eval_orimm; auto.
  - apply eval_orimm; auto.
(* bswap32 idiom *)
  - destruct (Int.eq s8 (Int.repr 8) && Int.eq s24a (Int.repr 24) &&
              Int.eq s8a (Int.repr 8) && Int.eq s24b (Int.repr 24) &&
              Int.eq c1 (Int.repr 65280) && Int.eq c2 (Int.repr 16711680) &&
              Int.eq cFF (Int.repr 255) &&
              Int.eq cFF000000 (Int.repr 4278190080) &&
              same_expr_pure x1 x2 && same_expr_pure x2 x3 && same_expr_pure x3 x4)
             eqn:GUARD; cycle 1.
    { (* fall-through *)
      exists (Val.or x y); split; [|apply Val.lessdef_refl].
      repeat (try eassumption; econstructor); cbn; eauto.
      cbn in H6, H7. inv H6. inv H7. reflexivity. }
    InvBooleans.
    exploit (eval_same_expr x1 x2); eauto. intros [_ Eq12].
    exploit (eval_same_expr x2 x3); eauto. intros [_ Eq23].
    exploit (eval_same_expr x3 x4); eauto. intros [_ Eq34].
    subst v5 v7 v9.
    apply Int.same_if_eq in H10, H22, H21, H20, H19, H18, H17, H16.
    eexists; split.
    { eapply eval_Eop;
        [eapply eval_Econs; [eassumption | apply eval_Enil] | cbn; reflexivity]. }
    cbn in H6, H7, H9, H11, H13, H14.
    inv H6. inv H7. inv H9. inv H11. inv H13. inv H14.
    destruct s8 as [s8 ?]; destruct s24a as [s24a ?];
    destruct s8a as [s8a ?]; destruct s24b as [s24b ?]; cbn in *.
    subst s8 s24a s8a s24b.
    destruct v3; cbn; auto.
(* shl - shru *)
  - destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) eqn:?.
    destruct (andb_prop _ _ Heqb0).
    generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros.
    exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst.
    exists (Val.ror v0 (Vint n2)); split. EvalOp.
    destruct v0; simpl; auto.
    destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto.
    destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto.
    simpl. rewrite <- Int.or_ror; auto.
    subst. TrivialExists.
    econstructor. EvalOp. simpl; eauto. econstructor; eauto. constructor.
    simpl. auto.
(* shru - shr *)
  - destruct (Int.eq (Int.add n2 n1) Int.iwordsize && same_expr_pure t1 t2) eqn:?.
    destruct (andb_prop _ _ Heqb0).
    generalize (Int.eq_spec (Int.add n2 n1) Int.iwordsize); rewrite H1; intros.
    exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst.
    exists (Val.ror v0 (Vint n1)); split. EvalOp.
    destruct v0; simpl; auto.
    destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto.
    destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto.
    simpl. rewrite Int.or_commut. rewrite <- Int.or_ror; auto.
    subst. TrivialExists.
    econstructor. EvalOp. simpl; eauto. econstructor; eauto. constructor.
    simpl. auto.
(* variable right rotate: (t >>u n) | (t << (32 - n)) *)
  - destruct (Int.eq c32 Int.iwordsize && same_expr_pure t1 t2 && same_expr_pure n1 n2) eqn:GUARD.
    + destruct (andb_prop _ _ GUARD) as [GUARD' SP_n].
      destruct (andb_prop _ _ GUARD') as [HEQ SP_t].
      generalize (Int.eq_spec c32 Int.iwordsize); rewrite HEQ; intros C32EQ.
      subst c32.
      exploit (eval_same_expr t1 t2); eauto. intros [_ EQT].
      exploit (eval_same_expr n1 n2); eauto. intros [_ EQN].
      subst v2; subst v4.
      eexists; split.
      { eapply eval_Eop.
        eapply eval_Econs. exact H2.
        eapply eval_Econs. exact H3.
        apply eval_Enil.
        cbn. reflexivity. }
      subst x.
      replace v3 with (Val.sub (Vint Int.iwordsize) v0)
        by (destruct v0; cbn in H |- *; auto).
      cbn in H6. inv H6.
      apply val_or_shru_shl_ror_lessdef.
    + subst x.
      eexists; split; [|apply Val.lessdef_refl].
      eapply eval_Eop.
      eapply eval_Econs.
      { eapply eval_Eop. eapply eval_Econs. exact H2.
        eapply eval_Econs. exact H3. apply eval_Enil. cbn. reflexivity. }
      eapply eval_Econs.
      { eapply eval_Eop. eapply eval_Econs. exact H5.
        eapply eval_Econs.
        { eapply eval_Eop. eapply eval_Econs. exact H4. apply eval_Enil.
          cbn. f_equal. }
        apply eval_Enil. rewrite H. exact H6. }
      apply eval_Enil. cbn. reflexivity.
(* variable left rotate: (t << n) | (t >>u (32 - n)) *)
  - destruct (Int.eq c32 Int.iwordsize && same_expr_pure t1 t2 && same_expr_pure n1 n2) eqn:GUARD.
    + destruct (andb_prop _ _ GUARD) as [GUARD' SP_n].
      destruct (andb_prop _ _ GUARD') as [HEQ SP_t].
      generalize (Int.eq_spec c32 Int.iwordsize); rewrite HEQ; intros C32EQ.
      subst c32.
      exploit (eval_same_expr t1 t2); eauto. intros [_ EQT].
      exploit (eval_same_expr n1 n2); eauto. intros [_ EQN].
      subst v2; subst v4.
      eexists; split.
      { eapply eval_Eop.
        eapply eval_Econs. exact H2.
        eapply eval_Econs.
        { eapply eval_Eop. eapply eval_Econs. exact H3. apply eval_Enil.
          cbn. reflexivity. }
        apply eval_Enil.
        cbn. reflexivity. }
      subst x.
      replace v3 with (Val.sub (Vint Int.iwordsize) v0)
        by (destruct v0; cbn in H |- *; auto).
      cbn in H6. inv H6.
      apply val_or_shl_shru_rolimm_lessdef.
    + subst x.
      eexists; split; [|apply Val.lessdef_refl].
      eapply eval_Eop.
      eapply eval_Econs.
      { eapply eval_Eop. eapply eval_Econs. exact H2.
        eapply eval_Econs. exact H3. apply eval_Enil. cbn. reflexivity. }
      eapply eval_Econs.
      { eapply eval_Eop. eapply eval_Econs. exact H5.
        eapply eval_Econs.
        { eapply eval_Eop. eapply eval_Econs. exact H4. apply eval_Enil.
          cbn. f_equal. }
        apply eval_Enil. rewrite H. exact H6. }
      apply eval_Enil. cbn. reflexivity.
(* bfi: shift-ubfx | bfc (case C, swapped of D) *)
  - destruct DecBoolOps.and_dec as [[[ZERO LSB] SZ] | ]; cycle 1.
    { TrivialExists. repeat (try eassumption; econstructor).
      cbn in *; congruence. }
    subst usz. subst ulsb.
    TrivialExists. cbn. rewrite Val.or_commut. f_equal. cbn in H6.
    unfold ExtValues.insf, ExtValues.clearf in H6 |- *.
    destruct (ExtValues.is_bitfield lsb sz) eqn:IBF; cycle 1.
    { (* not a bitfield: y = Vundef *)
      injection H6. clear H6. intros HY. subst y.
      rewrite <- H0. cbn. reflexivity. }
    injection H6. clear H6. intros HY. subst y.
    rewrite <- H0. rewrite <- H.
    pose proof (Int.unsigned_range sz) as Hsz.
    pose proof (Int.unsigned_range lsb) as Hlsb.
    unfold ExtValues.is_bitfield in IBF.
    apply Z.leb_le in IBF.
    assert (Int.ltu lsb2 Int.iwordsize = true) as LTU2.
    { destruct lsb2 as [a' Ha']. cbn. exact Ha'. }
    assert (Int.ltu lsb Int.iwordsize = true) as LTU.
    { rewrite LSB. exact LTU2. }
    f_equal.
    destruct v0; cbn; try reflexivity.
    change (Int.ltu Int.zero Int.iwordsize) with true. cbn.
    rewrite Int.shru_zero.
    rewrite LTU2. rewrite LTU.
    cbn. f_equal.
    rewrite <- LSB.
    unfold ExtValues.bitfield_mask.
    rewrite Int.and_shl.
    rewrite (Int.zero_ext_and (Int.unsigned sz)) by lia.
    do 3 f_equal.
    rewrite Z.ones_equiv. rewrite two_p_equiv. lia.
(* bfi: bfc | shift-ubfx (case D) *)
  - destruct DecBoolOps.and_dec as [[[ZERO LSB] SZ] | ]; cycle 1.
    { TrivialExists. repeat (try eassumption; econstructor).
      cbn in *; congruence. }
    subst usz. subst ulsb.
    TrivialExists. cbn. f_equal. cbn in H6.
    unfold ExtValues.insf, ExtValues.clearf in H0 |- *.
    destruct (ExtValues.is_bitfield lsb sz) eqn:IBF; cycle 1.
    { (* not a bitfield: x = Vundef so Val.or Vundef y = Vundef *)
      subst x. cbn. reflexivity. }
    subst x.
    pose proof (Int.unsigned_range sz) as Hsz.
    pose proof (Int.unsigned_range lsb) as Hlsb.
    unfold ExtValues.is_bitfield in IBF.
    apply Z.leb_le in IBF.
    assert (Int.ltu lsb2 Int.iwordsize = true) as LTU2.
    { destruct lsb2 as [a' Ha']. cbn. exact Ha'. }
    assert (Int.ltu lsb Int.iwordsize = true) as LTU.
    { rewrite LSB. exact LTU2. }
    f_equal.
    cbn in H6.
    injection H6. clear H6. intros HY. subst y.
    rewrite <- H.
    destruct v2; cbn; try reflexivity.
    change (Int.ltu Int.zero Int.iwordsize) with true. cbn.
    rewrite Int.shru_zero.
    rewrite LTU2. rewrite LTU.
    cbn. f_equal.
    rewrite <- LSB.
    unfold ExtValues.bitfield_mask.
    rewrite Int.and_shl.
    rewrite (Int.zero_ext_and (Int.unsigned sz)) by lia.
    do 3 f_equal.
    rewrite Z.ones_equiv. rewrite two_p_equiv. lia.
(* bfi: shift-(Obfc clear-high) | bfc (case 7) *)
  - destruct DecBoolOps.and_dec as [[[LSB CLLSB] [CLSUM CLBF1]] | ]; cycle 1.
    { TrivialExists. repeat (try eassumption; econstructor).
      cbn in *; congruence. }
    TrivialExists. cbn. rewrite Val.or_commut. f_equal. cbn in H6.
    unfold ExtValues.insf, ExtValues.clearf in H6 |- *.
    destruct (ExtValues.is_bitfield lsb sz) eqn:IBF; cycle 1.
    { (* not a bitfield: y = Vundef *)
      injection H6. clear H6. intros HY. subst y.
      rewrite <- H0. cbn. reflexivity. }
    injection H6. clear H6. intros HY. subst y.
    rewrite <- H0. rewrite <- H.
    pose proof (Int.unsigned_range sz) as Hsz.
    pose proof (Int.unsigned_range lsb) as Hlsb.
    unfold ExtValues.is_bitfield in IBF.
    apply Z.leb_le in IBF.
    assert (Int.ltu lsb2 Int.iwordsize = true) as LTU2.
    { destruct lsb2 as [a' Ha']. cbn. exact Ha'. }
    assert (Int.ltu lsb Int.iwordsize = true) as LTU.
    { rewrite LSB. exact LTU2. }
    f_equal.
    unfold ExtValues.clearf, ExtValues.is_bitfield, ExtValues.bitfield_mask.
    assert (CLBF: (Int.unsigned cl_lsb + Int.unsigned cl_sz <=? 32) = true)
      by (apply Z.leb_le; exact CLBF1).
    rewrite CLBF.
    destruct v0; cbn; try reflexivity.
    rewrite LTU2. rewrite LTU. cbn. f_equal.
    rewrite <- LSB.
    rewrite Int.and_shl.
    rewrite CLLSB.
    f_equal.
    (* Int.and i (Int.not (Int.shl (Z.ones cl_sz) sz)) = Int.and i (Int.repr (Z.ones sz)) *)
    apply Int.same_bits_eq. intros i_idx Hi.
    rewrite ! Int.bits_and by lia.
    rewrite Int.bits_not by lia.
    rewrite Int.bits_shl by lia.
    rewrite Int.testbit_repr by lia.
    rewrite Z.testbit_ones_nonneg by (pose proof (Int.unsigned_range sz); lia).
    assert (CLEQ: Int.unsigned cl_sz = 32 - Int.unsigned sz).
    { assert (CLA: Int.unsigned (Int.add cl_lsb cl_sz) = 32) by (rewrite CLSUM; reflexivity).
      unfold Int.add in CLA.
      pose proof (Int.unsigned_range cl_lsb).
      pose proof (Int.unsigned_range cl_sz).
      rewrite Int.unsigned_repr in CLA by (change Int.max_unsigned with 4294967295; lia).
      rewrite CLLSB in CLA. lia. }
    destruct (zlt i_idx (Int.unsigned sz)) as [Hi_lt | Hi_ge].
    + assert ((i_idx <? Int.unsigned sz)%Z = true) as -> by (apply Z.ltb_lt; lia).
      cbn. reflexivity.
    + rewrite Int.testbit_repr by lia.
      rewrite Z.testbit_ones_nonneg by (pose proof (Int.unsigned_range cl_sz); lia).
      assert ((i_idx <? Int.unsigned sz)%Z = false) as -> by (apply Z.ltb_ge; lia).
      cbn.
      assert ((i_idx - Int.unsigned sz <? Int.unsigned cl_sz)%Z = true) as ->.
      { apply Z.ltb_lt. rewrite CLEQ.
        change Int.zwordsize with 32 in Hi. lia. }
      rewrite ! andb_false_r. reflexivity.
(* bfi: bfc | shift-(Obfc clear-high) (case 8) *)
  - destruct DecBoolOps.and_dec as [[[LSB CLLSB] [CLSUM CLBF1]] | ]; cycle 1.
    { TrivialExists. repeat (try eassumption; econstructor).
      cbn in *; congruence. }
    TrivialExists. cbn. f_equal. cbn in H6.
    unfold ExtValues.insf, ExtValues.clearf in H0 |- *.
    destruct (ExtValues.is_bitfield lsb sz) eqn:IBF; cycle 1.
    { subst x. cbn. reflexivity. }
    subst x.
    pose proof (Int.unsigned_range sz) as Hsz.
    pose proof (Int.unsigned_range lsb) as Hlsb.
    unfold ExtValues.is_bitfield in IBF.
    apply Z.leb_le in IBF.
    assert (Int.ltu lsb2 Int.iwordsize = true) as LTU2.
    { destruct lsb2 as [a' Ha']. cbn. exact Ha'. }
    assert (Int.ltu lsb Int.iwordsize = true) as LTU.
    { rewrite LSB. exact LTU2. }
    f_equal.
    cbn in H6.
    injection H6. clear H6. intros HY. subst y.
    rewrite <- H.
    unfold ExtValues.clearf, ExtValues.is_bitfield, ExtValues.bitfield_mask.
    assert (CLBF: (Int.unsigned cl_lsb + Int.unsigned cl_sz <=? 32) = true)
      by (apply Z.leb_le; exact CLBF1).
    rewrite CLBF.
    destruct v2; cbn; try reflexivity.
    rewrite LTU2. rewrite LTU. cbn. f_equal.
    rewrite <- LSB.
    rewrite Int.and_shl.
    rewrite CLLSB.
    f_equal.
    apply Int.same_bits_eq. intros i_idx Hi.
    rewrite ! Int.bits_and by lia.
    rewrite Int.bits_not by lia.
    rewrite Int.bits_shl by lia.
    rewrite Int.testbit_repr by lia.
    rewrite Z.testbit_ones_nonneg by (pose proof (Int.unsigned_range sz); lia).
    assert (CLEQ: Int.unsigned cl_sz = 32 - Int.unsigned sz).
    { assert (CLA: Int.unsigned (Int.add cl_lsb cl_sz) = 32) by (rewrite CLSUM; reflexivity).
      unfold Int.add in CLA.
      pose proof (Int.unsigned_range cl_lsb).
      pose proof (Int.unsigned_range cl_sz).
      rewrite Int.unsigned_repr in CLA by (change Int.max_unsigned with 4294967295; lia).
      rewrite CLLSB in CLA. lia. }
    destruct (zlt i_idx (Int.unsigned sz)) as [Hi_lt | Hi_ge].
    + assert ((i_idx <? Int.unsigned sz)%Z = true) as -> by (apply Z.ltb_lt; lia).
      cbn. reflexivity.
    + rewrite Int.testbit_repr by lia.
      rewrite Z.testbit_ones_nonneg by (pose proof (Int.unsigned_range cl_sz); lia).
      assert ((i_idx <? Int.unsigned sz)%Z = false) as -> by (apply Z.ltb_ge; lia).
      cbn.
      assert ((i_idx - Int.unsigned sz <? Int.unsigned cl_sz)%Z = true) as ->.
      { apply Z.ltb_lt. rewrite CLEQ.
        change Int.zwordsize with 32 in Hi. lia. }
      rewrite ! andb_false_r. reflexivity.
(* bfi: Slsl(Oandimm m fld) | Obfc lsb sz prev — case A *)
  - destruct DecBoolOps.and_dec as [[LSB VAL]| ]; cycle 1.
    { TrivialExists. repeat (try eassumption; econstructor).
      cbn. congruence. }
    TrivialExists. cbn. f_equal. cbn in H6.
    unfold ExtValues.insf, ExtValues.clearf in *.
    destruct (ExtValues.is_bitfield lsb sz); inv H6; cycle 1.
    { rewrite Val.or_commut. reflexivity. }
    rewrite Val.or_commut.
    f_equal.
    unfold ExtValues.bitfield_mask.
    destruct v0; cbn; auto.
    pose proof (s_range lsb2) as Hsr.
    rewrite Hsr. cbn. f_equal.
    rewrite Int.and_shl. reflexivity.
(* bfi: Obfc lsb sz prev | Slsl(Oandimm m fld) — case B (mirror) *)
  - destruct DecBoolOps.and_dec as [[LSB VAL]| ]; cycle 1.
    { TrivialExists. repeat (try eassumption; econstructor).
      cbn in *; congruence. }
    TrivialExists. cbn. f_equal. cbn in H6.
    unfold ExtValues.insf, ExtValues.clearf in *.
    destruct (ExtValues.is_bitfield lsb sz); inv H6; cycle 1.
    { reflexivity. }
    f_equal.
    unfold ExtValues.bitfield_mask.
    destruct v2; cbn; auto.
    pose proof (s_range lsb2) as Hsr.
    rewrite Hsr. cbn. f_equal.
    rewrite Int.and_shl. reflexivity.
(* orshift *)
  - subst. rewrite Val.or_commut. TrivialExists.
  - subst. TrivialExists.
  - destruct DecBoolOps.and_dec as [[LSB VAL]| ]; cycle 1.
    { TrivialExists. repeat (try eassumption; econstructor).
      cbn. congruence. }
    TrivialExists. cbn. f_equal. cbn in H6.
    unfold ExtValues.insf, ExtValues.clearf in *.
    destruct (ExtValues.is_bitfield lsb sz); inv H6; cycle 1.
    { rewrite Val.or_commut. reflexivity. }
    rewrite Val.or_commut. reflexivity.
(* bfi: bfc | Oandimm-shift (case B, symmetric of A) *)
  - destruct DecBoolOps.and_dec as [[LSB VAL]| ]; cycle 1.
    { TrivialExists. repeat (try eassumption; econstructor).
      cbn in *; congruence. }
    TrivialExists. cbn. f_equal. cbn in H6.
    unfold ExtValues.insf, ExtValues.clearf in *.
    destruct (ExtValues.is_bitfield lsb sz); inv H6; cycle 1.
    { reflexivity. }
    reflexivity.
  - destruct DecBoolOps.and_dec as [[[EQ1 EQ2] EQ3]| ]; cycle 1.
    { TrivialExists. repeat (try eassumption; econstructor).
      cbn. congruence. }
    unfold ExtValues.insf, ExtValues.clearf, ExtValues.is_bitfield in *.
    destruct (Int.unsigned rest_lsb + Int.unsigned rest_sz <=? 32) eqn:LEQ1; cycle 1.
    { subst x. cbn. eexists. split.
      repeat (try eassumption; econstructor). constructor. }
    destruct (Int.unsigned lsb + Int.unsigned sz <=? 32) eqn:LEQ2; cycle 1.
    { subst y. rewrite Val.or_commut. cbn. eexists. split.
      repeat (try eassumption; econstructor). constructor. }
    TrivialExists. cbn. unfold ExtValues.insf, ExtValues.is_bitfield.
    unfold ExtValues.bitfield_mask in *.
    subst lsb. subst rest_lsb.
    rewrite LEQ2.
    rewrite Val.or_commut. f_equal.
    f_equal.
    { subst x. destruct v1; cbn; try reflexivity.
      unfold Int.ltu.
      rewrite zlt_true; cycle 1.
      { change (Int.unsigned Int.zero) with 0.
        change (Int.unsigned Int.iwordsize) with 32.
        lia.
      }
      change (Int.unsigned Int.zero) with 0 in LEQ2.
      rewrite Z.add_0_l in LEQ2.
      rewrite Int.shl_zero. cbn. f_equal. f_equal.
      rewrite shifted_masks; cycle 1.
      { pose proof (Int.unsigned_range sz). lia. }
      rewrite Int.repr_unsigned.
      f_equal. f_equal. f_equal. f_equal.
      replace sz with (Int.sub (Int.add sz rest_sz) rest_sz); cycle 1.
      { rewrite Int.sub_add_opp.
        rewrite Int.add_assoc.
        rewrite <- Int.sub_add_opp.
        rewrite Int.sub_idem.
        apply Int.add_zero.
      }
      rewrite EQ3. unfold Int.sub.
      change (Int.unsigned (Int.repr 32)) with 32.
      rewrite Int.unsigned_repr. ring.
      replace rest_sz with (Int.sub (Int.add sz rest_sz) sz); cycle 1.
      { rewrite Int.sub_add_opp.
        rewrite (Int.add_commut sz rest_sz).
        rewrite Int.add_assoc.
        rewrite <- Int.sub_add_opp.
        rewrite Int.sub_idem.
        apply Int.add_zero.
      }
      rewrite EQ3.
      unfold Int.sub.
      change (Int.unsigned (Int.repr 32)) with 32.
      pose proof (Int.unsigned_range sz).
      rewrite Int.unsigned_repr; cycle 1.
      { change Int.modulus with 4294967296 in *.
        change Int.max_unsigned with 4294967295 in *.
        lia.
      }
      change Int.modulus with 4294967296 in *.
      change Int.max_unsigned with 4294967295 in *.
      lia.
    }
    assumption.
(* default *)
  - TrivialExists.
Qed.

Theorem eval_xorimm:
  forall n, unary_constructor_sound (xorimm n) (fun x => Val.xor x (Vint n)).
Proof.
  intros; red; intros until x. unfold xorimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  intros. exists x; split. auto.
  destruct x; simpl; auto. subst n. rewrite Int.xor_zero. auto.
  predSpec Int.eq Int.eq_spec n Int.mone.
  intros. subst n. rewrite <- Val.not_xor. apply eval_notint; auto.
  intros. destruct (xorimm_match a); intros; InvEval.
  TrivialExists. simpl. rewrite Int.xor_commut; auto.
  subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists.
  subst x. rewrite Val.not_xor. rewrite Val.xor_assoc.
  rewrite (Val.xor_commut (Vint Int.mone)). TrivialExists.
  TrivialExists.
Qed.

Theorem eval_xor: binary_constructor_sound xor Val.xor.
Proof.
  red; intros until y; unfold xor; case (xor_match a b); intros; InvEval.
  TrivialExists.
  rewrite Val.xor_commut. apply eval_xorimm; auto.
  apply eval_xorimm; auto.
  subst. rewrite Val.xor_commut. TrivialExists.
  subst. TrivialExists.
  TrivialExists.
Qed.

Lemma eval_mod_aux:
  forall divop semdivop,
  (forall sp x y m, eval_operation ge sp divop (x :: y :: nil) m = semdivop x y) ->
  forall le a b x y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  semdivop x y = Some z ->
  exists v,
  eval_expr ge sp e m le (mod_aux divop a b) v /\
  Val.lessdef (Val.sub x (Val.mul z y)) v.
Proof.
  intros divop semdivop Hdiv le a b x y z Ha Hb Hsem.
  unfold mod_aux.
  set (le2 := y :: x :: le).
  assert (E1: eval_expr ge sp e m le2 (Eletvar 1) x).
  { apply eval_Eletvar. reflexivity. }
  assert (E0: eval_expr ge sp e m le2 (Eletvar 0) y).
  { apply eval_Eletvar. reflexivity. }
  assert (Ediv: eval_expr ge sp e m le2
              (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil)) z).
  { eapply eval_Eop.
    eapply eval_Econs. exact E1.
    eapply eval_Econs. exact E0.
    apply eval_Enil.
    rewrite Hdiv. exact Hsem. }
  assert (Emul: eval_expr ge sp e m le2
              (Eop Omul (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) ::: Eletvar 0 ::: Enil))
              (Val.mul z y)).
  { eapply eval_Eop.
    eapply eval_Econs. exact Ediv.
    eapply eval_Econs. exact E0.
    apply eval_Enil.
    reflexivity. }
  exploit eval_sub. exact E1. exact Emul.
  intros [v [V L]].
  exists v; split; [|exact L].
  eapply eval_Elet. eexact Ha.
  eapply eval_Elet. apply eval_lift. eexact Hb.
  exact V.
Qed.

Theorem eval_divs_base:
  forall le a b x y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.divs x y = Some z ->
  exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v.
Proof.
  intros. unfold divs_base. exists z; split. EvalOp. auto.
Qed.

Theorem eval_mods_base:
  forall le a b x y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.mods x y = Some z ->
  exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v.
Proof.
  intros; unfold mods_base.
  exploit Val.mods_divs; eauto. intros [v [A B]].
  subst.
  eapply eval_mod_aux with (semdivop := Val.divs); eauto.
Qed.

Theorem eval_divu_base:
  forall le a x b y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.divu x y = Some z ->
  exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v.
Proof.
  intros. unfold divu_base. exists z; split. EvalOp. auto.
Qed.

Theorem eval_modu_base:
  forall le a x b y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.modu x y = Some z ->
  exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
Proof.
  intros; unfold modu_base.
  exploit Val.modu_divu; eauto. intros [v [A B]].
  subst.
  eapply eval_mod_aux with (semdivop := Val.divu); eauto.
Qed.

Theorem eval_shrximm:
  forall le a n x z,
  eval_expr ge sp e m le a x ->
  Val.shrx x (Vint n) = Some z ->
  exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v.
Proof.
  intros. unfold shrximm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  subst n. exists x; split; auto.
  destruct x; simpl in H0; try discriminate.
  destruct (Int.ltu Int.zero (Int.repr 31)); inv H0.
  replace (Int.shrx i Int.zero) with i. auto.
  unfold Int.shrx, Int.divs. rewrite Int.shl_zero.
  change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
  econstructor; split. EvalOp. auto.
Qed.

Theorem eval_shl: binary_constructor_sound shl Val.shl.
Proof.
  red; intros until y; unfold shl; case (shl_match b); intros.
  InvEval. apply eval_shlimm; auto.
  TrivialExists.
Qed.

Theorem eval_shr: binary_constructor_sound shr Val.shr.
Proof.
  red; intros until y; unfold shr; case (shr_match b); intros.
  InvEval. apply eval_shrimm; auto.
  TrivialExists.
Qed.

Theorem eval_shru: binary_constructor_sound shru Val.shru.
Proof.
  red; intros until y; unfold shru; case (shru_match b); intros.
  InvEval. apply eval_shruimm; auto.
  TrivialExists.
Qed.


Theorem eval_negf: unary_constructor_sound negf Val.negf.
Proof.
  red; intros. TrivialExists.
Qed.

Theorem eval_absf: unary_constructor_sound absf Val.absf.
Proof.
  red; intros. TrivialExists.
Qed.

Theorem eval_addf: binary_constructor_sound addf Val.addf.
Proof.
  intro. intros e1 v1 e2 v2 He1 He2.
  unfold addf. destruct (addf_match e1 e2).
  - InvEval. subst.
    TrivialExists.
  - TrivialExists.
Qed.

Theorem eval_subf: binary_constructor_sound subf Val.subf.
Proof.
  intro. intros e1 v1 e2 v2 He1 He2.
  unfold subf. destruct (subf_match e1 e2).
  - InvEval. subst.
    TrivialExists.
  - TrivialExists.
Qed.

Theorem eval_mulf: binary_constructor_sound mulf Val.mulf.
Proof.
  red; intros; TrivialExists.
Qed.

Theorem eval_sqrtf:
  forall expr expr' le x
  (EVAL : sqrtf expr = Some expr')
  (EXPR : eval_expr ge sp e m le expr x),
  exists v, eval_expr ge sp e m le expr' v /\ Val.lessdef (Val.sqrtf x) v.
Proof.
  unfold sqrtf in *. intros. inv EVAL. eexists. split.
  repeat econstructor. exact EXPR. constructor.
Qed.

Theorem eval_bswap32:
  forall expr expr' le x
  (EVAL : bswap32 expr = Some expr')
  (EXPR : eval_expr ge sp e m le expr x),
  exists v, eval_expr ge sp e m le expr' v
         /\ Val.lessdef (ExtValues.val_bswap32 x) v.
Proof.
  unfold bswap32 in *. intros. inv EVAL. eexists. split.
  repeat econstructor. exact EXPR. constructor.
Qed.

Theorem eval_negfs: unary_constructor_sound negfs Val.negfs.
Proof.
  red; intros. TrivialExists.
Qed.

Theorem eval_absfs: unary_constructor_sound absfs Val.absfs.
Proof.
  red; intros. TrivialExists.
Qed.


Theorem eval_addfs: binary_constructor_sound addfs Val.addfs.
Proof.
  intro. intros e1 v1 e2 v2 He1 He2.
  unfold addfs. destruct (addfs_match e1 e2).
  - InvEval. subst.
    TrivialExists.
  - TrivialExists.
Qed.

Theorem eval_subfs: binary_constructor_sound subfs Val.subfs.
Proof.
  intro. intros e1 v1 e2 v2 He1 He2.
  unfold subfs. destruct (subfs_match e1 e2).
  - InvEval. subst.
    TrivialExists.
  - TrivialExists.
Qed.

Theorem eval_mulfs: binary_constructor_sound mulfs Val.mulfs.
Proof.
  red; intros; TrivialExists.
Qed.

Theorem eval_sqrtfs:
  forall expr expr' le x
  (EVAL : sqrtfs expr = Some expr')
  (EXPR : eval_expr ge sp e m le expr x),
  exists v, eval_expr ge sp e m le expr' v /\ Val.lessdef (Val.sqrtfs x) v.
Proof.
  unfold sqrtfs in *. intros. inv EVAL. eexists. split.
  repeat econstructor. exact EXPR. constructor.
Qed.

Bit-test identity: if mask is the single-bit power-of-two 2^k, then (i & mask) != 0 is exactly (i >> k) & 1.
Lemma is_power2_bit_test_int:
  forall i mask k,
  Int.is_power2 mask = Some k ->
  Int.zero_ext 1 (Int.shru i k) =
  (if Int.eq (Int.and i mask) Int.zero then Int.zero else Int.one).
Proof.
  intros i mask k Hp.
  pose proof (Int.is_power2_correct _ _ Hp) as Hcor.
  pose proof (Int.is_power2_rng _ _ Hp) as Hrng.
  apply Int.same_bits_eq; intros j Hj.
  rewrite Int.bits_zero_ext by lia.
  rewrite Int.bits_shru by lia.
  predSpec Int.eq Int.eq_spec (Int.and i mask) Int.zero.
  - (* and = 0 *)
    rewrite Int.bits_zero.
    apply (f_equal (fun y => Int.testbit y (Int.unsigned k))) in H.
    rewrite Int.bits_and in H by lia.
    assert (HBitM_k: Int.testbit mask (Int.unsigned k) = true).
    { rewrite <- (Int.repr_unsigned mask) at 1.
      rewrite Hcor. rewrite Int.testbit_repr by lia.
      rewrite two_p_equiv. rewrite Z.pow2_bits_eqb by lia.
      apply Z.eqb_refl. }
    rewrite HBitM_k in H. rewrite andb_true_r in H.
    rewrite Int.bits_zero in H.
    destruct (zlt j 1); [|reflexivity].
    assert (j = 0) by lia; subst j. rewrite Z.add_0_l.
    destruct (zlt (Int.unsigned k) Int.zwordsize); [|lia]. exact H.
  - (* and != 0 *)
    rewrite Int.bits_one.
    assert (HBitI: Int.testbit i (Int.unsigned k) = true).
    { destruct (Int.testbit i (Int.unsigned k)) eqn:HBI; auto.
      exfalso. apply H. apply Int.same_bits_eq; intros j' Hj'.
      rewrite Int.bits_and by lia. rewrite Int.bits_zero.
      destruct (Z.eq_dec j' (Int.unsigned k)).
      - subst j'. rewrite HBI. reflexivity.
      - rewrite <- (Int.repr_unsigned mask) at 1.
        rewrite Hcor. rewrite Int.testbit_repr by lia.
        rewrite two_p_equiv. rewrite Z.pow2_bits_eqb by lia.
        assert (Int.unsigned k =? j' = false) by (apply Z.eqb_neq; lia).
        rewrite H0. apply andb_false_r. }
    destruct (zlt j 1).
    + assert (j = 0) by lia; subst j. rewrite Z.add_0_l.
      destruct (zlt (Int.unsigned k) Int.zwordsize); [|lia].
      rewrite HBitI. simpl. reflexivity.
    + destruct (zeq j 0); [lia|reflexivity].
Qed.

Section COMP_IMM.

Variable default: comparison -> int -> condition.
Variable intsem: comparison -> int -> int -> bool.
Variable sem: comparison -> val -> val -> val.

Hypothesis sem_int: forall c x y, sem c (Vint x) (Vint y) = Val.of_bool (intsem c x y).
Hypothesis sem_undef: forall c v, sem c Vundef v = Vundef.
Hypothesis sem_eq: forall x y, sem Ceq (Vint x) (Vint y) = Val.of_bool (Int.eq x y).
Hypothesis sem_ne: forall x y, sem Cne (Vint x) (Vint y) = Val.of_bool (negb (Int.eq x y)).
Hypothesis sem_default: forall c v n, sem c v (Vint n) = Val.of_optbool (eval_condition (default c n) (v :: nil) m).

Lemma eval_compimm:
  forall le c a n2 x,
  eval_expr ge sp e m le a x ->
  exists v, eval_expr ge sp e m le (compimm default intsem c a n2) v
         /\ Val.lessdef (sem c x (Vint n2)) v.
Proof.
  intros until x.
  unfold compimm; case (compimm_match c a); intros.
(* constant *)
  InvEval. rewrite sem_int. TrivialExists. simpl. destruct (intsem c0 n1 n2); auto.
(* eq cmp *)
  InvEval. inv H. simpl in H5. inv H5.
  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists.
  simpl. rewrite eval_negate_condition.
  destruct (eval_condition c0 vl m); simpl.
  unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto.
  rewrite sem_undef; auto.
  destruct (Int.eq_dec n2 Int.one). subst n2. TrivialExists.
  simpl. destruct (eval_condition c0 vl m); simpl.
  unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto.
  rewrite sem_undef; auto.
  exists (Vint Int.zero); split. EvalOp.
  destruct (eval_condition c0 vl m); simpl.
  unfold Vtrue, Vfalse. destruct b; rewrite sem_eq; rewrite Int.eq_false; auto.
  rewrite sem_undef; auto.
(* ne cmp *)
  InvEval. inv H. simpl in H5. inv H5.
  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists.
  simpl. destruct (eval_condition c0 vl m); simpl.
  unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto.
  rewrite sem_undef; auto.
  destruct (Int.eq_dec n2 Int.one). subst n2. TrivialExists.
  simpl. rewrite eval_negate_condition. destruct (eval_condition c0 vl m); simpl.
  unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto.
  rewrite sem_undef; auto.
  exists (Vint Int.one); split. EvalOp.
  destruct (eval_condition c0 vl m); simpl.
  unfold Vtrue, Vfalse. destruct b; rewrite sem_ne; rewrite Int.eq_false; auto.
  rewrite sem_undef; auto.
(* Cmaskzero (and) *)
  predSpec Int.eq Int.eq_spec n2 Int.zero.
  subst n2. InvEval; subst x.
  econstructor; split.
  eapply eval_Eop; [ repeat econstructor; eauto | reflexivity ].
  simpl. destruct v1; simpl; try (rewrite sem_undef; auto).
  rewrite sem_eq. destruct (Int.eq (Int.and i m0) Int.zero); auto.
  TrivialExists. simpl. rewrite sem_default. auto.
(* andimm_ne_zero_to_bool (and) *)
  predSpec Int.eq Int.eq_spec n2 Int.zero.
  { subst n2. InvEval; subst x. unfold andimm_ne_zero_to_bool.
    destruct (Int.is_power2 m0) as [k|] eqn:HP2.
    - (* Some k: emit Oubfx k 1 on Thumb-2, else fall back to Cmasknotzero. *)
      destruct (Archi.thumb2_support && Compopts.bitfield_ops tt) eqn:GUARD.
      + (* Thumb-2 path: Oubfx k 1 *)
        econstructor; split.
        { eapply eval_Eop; [ repeat econstructor; eauto | reflexivity ]. }
        simpl. destruct v1; simpl; try (rewrite sem_undef; auto).
        pose proof (Int.is_power2_range _ _ HP2) as Hrange.
        change (Int.unsigned Int.one) with 1.
        rewrite Hrange. simpl.
        rewrite sem_ne.
        rewrite (is_power2_bit_test_int i m0 k HP2).
        destruct (Int.eq (Int.and i m0) Int.zero) eqn:HE; apply Val.lessdef_refl.
      + (* Non-Thumb-2 path: Cmasknotzero m0 *)
        econstructor; split.
        { eapply eval_Eop; [ repeat econstructor; eauto | reflexivity ]. }
        simpl. destruct v1; simpl; try (rewrite sem_undef; auto).
        rewrite sem_ne. destruct (Int.eq (Int.and i m0) Int.zero); auto.
    - (* None: emit Cmasknotzero m0 *)
      econstructor; split.
      { eapply eval_Eop; [ repeat econstructor; eauto | reflexivity ]. }
      simpl. destruct v1; simpl; try (rewrite sem_undef; auto).
      rewrite sem_ne. destruct (Int.eq (Int.and i m0) Int.zero); auto. }
  TrivialExists. simpl. rewrite sem_default. auto.
(* Cmaskzero (bfc) *)
  predSpec Int.eq Int.eq_spec n2 Int.zero.
  subst n2. InvEval; subst x.
  econstructor; split.
  eapply eval_Eop; [ repeat econstructor; eauto | reflexivity ].
  simpl. unfold ExtValues.clearf.
  destruct (ExtValues.is_bitfield lsb sz); [| rewrite sem_undef; auto].
  destruct v1; simpl; try (rewrite sem_undef; auto).
  rewrite sem_eq.
  destruct (Int.eq (Int.and i (Int.not (ExtValues.bitfield_mask lsb sz))) Int.zero); auto.
  TrivialExists. simpl. rewrite sem_default. auto.
(* Cmasknotzero (bfc) *)
  predSpec Int.eq Int.eq_spec n2 Int.zero.
  subst n2. InvEval; subst x.
  econstructor; split.
  eapply eval_Eop; [ repeat econstructor; eauto | reflexivity ].
  simpl. unfold ExtValues.clearf.
  destruct (ExtValues.is_bitfield lsb sz); [| rewrite sem_undef; auto].
  destruct v1; simpl; try (rewrite sem_undef; auto).
  rewrite sem_ne.
  destruct (Int.eq (Int.and i (Int.not (ExtValues.bitfield_mask lsb sz))) Int.zero); auto.
  TrivialExists. simpl. rewrite sem_default. auto.
(* Cmaskzero (ubfx) *)
  predSpec Int.eq Int.eq_spec n2 Int.zero.
  subst n2. InvEval; subst x.
  econstructor; split.
  eapply eval_Eop; [ repeat econstructor; eauto | reflexivity ].
  simpl. destruct v1; simpl; try (rewrite sem_undef; auto).
  destruct (Int.ltu lsb Int.iwordsize) eqn:Hlsb; simpl;
    [| rewrite sem_undef; auto].
  rewrite sem_eq.
  rewrite ExtValues.zero_ext_shru_and_bitfield_mask_zero by exact Hlsb.
  destruct (Int.eq (Int.and i (ExtValues.bitfield_mask lsb sz)) Int.zero); auto.
  TrivialExists. simpl. rewrite sem_default. auto.
(* Cmasknotzero (ubfx) *)
  predSpec Int.eq Int.eq_spec n2 Int.zero.
  subst n2. InvEval; subst x.
  econstructor; split.
  eapply eval_Eop; [ repeat econstructor; eauto | reflexivity ].
  simpl. destruct v1; simpl; try (rewrite sem_undef; auto).
  destruct (Int.ltu lsb Int.iwordsize) eqn:Hlsb; simpl;
    [| rewrite sem_undef; auto].
  rewrite sem_ne.
  rewrite ExtValues.zero_ext_shru_and_bitfield_mask_zero by exact Hlsb.
  destruct (Int.eq (Int.and i (ExtValues.bitfield_mask lsb sz)) Int.zero); auto.
  TrivialExists. simpl. rewrite sem_default. auto.
(* Cmaskzero (sbfx) *)
  predSpec Int.eq Int.eq_spec n2 Int.zero.
  subst n2. InvEval; subst x.
  econstructor; split.
  eapply eval_Eop; [ repeat econstructor; eauto | reflexivity ].
  simpl. destruct v1; simpl; try (rewrite sem_undef; auto).
  destruct (Int.ltu lsb Int.iwordsize) eqn:Hlsb; simpl;
    [| rewrite sem_undef; auto].
  rewrite sem_eq.
  rewrite ExtValues.sign_ext_shru_and_bitfield_mask_zero by exact Hlsb.
  destruct (Int.eq (Int.and i (ExtValues.bitfield_mask lsb sz)) Int.zero); auto.
  TrivialExists. simpl. rewrite sem_default. auto.
(* Cmasknotzero (sbfx) *)
  predSpec Int.eq Int.eq_spec n2 Int.zero.
  subst n2. InvEval; subst x.
  econstructor; split.
  eapply eval_Eop; [ repeat econstructor; eauto | reflexivity ].
  simpl. destruct v1; simpl; try (rewrite sem_undef; auto).
  destruct (Int.ltu lsb Int.iwordsize) eqn:Hlsb; simpl;
    [| rewrite sem_undef; auto].
  rewrite sem_ne.
  rewrite ExtValues.sign_ext_shru_and_bitfield_mask_zero by exact Hlsb.
  destruct (Int.eq (Int.and i (ExtValues.bitfield_mask lsb sz)) Int.zero); auto.
  TrivialExists. simpl. rewrite sem_default. auto.
(* default *)
  TrivialExists. simpl. rewrite sem_default. auto.
Qed.

Hypothesis sem_swap:
  forall c x y, sem (swap_comparison c) x y = sem c y x.

Lemma eval_compimm_swap:
  forall le c a n2 x,
  eval_expr ge sp e m le a x ->
  exists v, eval_expr ge sp e m le (compimm default intsem (swap_comparison c) a n2) v
         /\ Val.lessdef (sem c (Vint n2) x) v.
Proof.
  intros. rewrite <- sem_swap. eapply eval_compimm; eauto.
Qed.

End COMP_IMM.

Theorem eval_comp:
  forall c, binary_constructor_sound (comp c) (Val.cmp c).
Proof.
  intros; red; intros until y. unfold comp; case (comp_match a b); intros; InvEval.
  - (* Ointconst n1, t2 *)
    eapply eval_compimm_swap; eauto.
    intros. unfold Val.cmp. rewrite Val.swap_cmp_bool; auto.
  - (* t1, Ointconst n2 *)
    eapply eval_compimm; eauto.
  - (* t1, Eop (Oshift s) (t2:::Enil) *)
    subst. TrivialExists.
  - (* Eop (Oshift s) (t1:::Enil), t2 *)
    subst. TrivialExists. simpl. unfold Val.cmp. rewrite Val.swap_cmp_bool. reflexivity.
  - (* default *)
    TrivialExists.
Qed.

Theorem eval_compu:
  forall c, binary_constructor_sound (compu c) (Val.cmpu (Mem.valid_pointer m) c).
Proof.
  intros; red; intros until y. unfold compu; case (compu_match a b); intros; InvEval.
  - eapply eval_compimm_swap; eauto.
    intros. unfold Val.cmpu. rewrite Val.swap_cmpu_bool; auto.
  - eapply eval_compimm; eauto.
  - (* t1, Eop (Oshift s) (t2:::Enil) *)
    subst. TrivialExists.
  - (* Eop (Oshift s) (t1:::Enil), t2 *)
    subst. TrivialExists. simpl. unfold Val.cmpu. rewrite Val.swap_cmpu_bool. reflexivity.
  - TrivialExists.
Qed.

Theorem eval_compf:
  forall c, binary_constructor_sound (compf c) (Val.cmpf c).
Proof.
  intros; red; intros. unfold compf. TrivialExists.
Qed.

Theorem eval_compfs:
  forall c, binary_constructor_sound (compfs c) (Val.cmpfs c).
Proof.
  intros; red; intros. unfold compfs. TrivialExists.
Qed.

Lemma select_swap:
  forall ob v1 v2,
  Val.select (option_map negb ob) v2 v1 = Val.select ob v1 v2.
Proof.
  intros. destruct ob as [[]|]; reflexivity.
Qed.

Lemma eval_Osel_default:
  forall le cond al vl a1 v1 a2 v2 ty,
  eval_exprlist ge sp e m le al vl ->
  eval_expr ge sp e m le a1 v1 ->
  eval_expr ge sp e m le a2 v2 ->
  exists v,
     eval_expr ge sp e m le (Eop (Osel cond) (a1 ::: a2 ::: al)) v
  /\ Val.lessdef (Val.normalize (Val.select (eval_condition cond vl m) v1 v2) ty) v.
Proof.
  intros. eexists; split.
  - EvalOp. simpl. eauto.
  - apply Val.lessdef_normalize.
Qed.

Lemma eval_selectimm:
  forall le cond al vl e1 v1 imm v2,
  eval_exprlist ge sp e m le al vl ->
  eval_expr ge sp e m le e1 v1 ->
  v2 = Vint imm ->
  exists v,
     eval_expr ge sp e m le (selectimm cond al e1 imm) v
  /\ Val.lessdef (Val.normalize (Val.select (eval_condition cond vl m) v1 v2) Tint) v.
Proof.
  intros; subst. unfold selectimm.
  destruct (is_immed_arith CONST imm) eqn:?.
  - eexists; split; [EvalOp; simpl; eauto | apply Val.lessdef_normalize].
  - eapply eval_Osel_default; eauto. EvalOp.
Qed.

Lemma eval_selimmn:
  forall le cond al vl imm v1 e2 v2,
  eval_exprlist ge sp e m le al vl ->
  v1 = Vint imm ->
  eval_expr ge sp e m le e2 v2 ->
  exists v,
     eval_expr ge sp e m le (selimmn cond al imm e2) v
  /\ Val.lessdef (Val.normalize (Val.select (eval_condition cond vl m) v1 v2) Tint) v.
Proof.
  intros; subst. unfold selimmn.
  destruct (is_immed_arith CONST imm) eqn:?.
  - eexists; split.
    + EvalOp. simpl. rewrite eval_negate_condition. eauto.
    + rewrite select_swap. apply Val.lessdef_normalize.
  - edestruct (eval_Osel_default le cond al vl (Eop (Ointconst imm) Enil) (Vint imm) e2 v2 Tint)
      as (v & EV & LD); eauto.
    EvalOp.
Qed.

Lemma eval_selectimm2:
  forall le cond al vl imm1 imm2 v1 v2,
  eval_exprlist ge sp e m le al vl ->
  v1 = Vint imm1 ->
  v2 = Vint imm2 ->
  exists v,
     eval_expr ge sp e m le (selectimm2 cond al imm1 imm2) v
  /\ Val.lessdef (Val.normalize (Val.select (eval_condition cond vl m) v1 v2) Tint) v.
Proof.
  intros; subst. unfold selectimm2.
  destruct (Int.eq imm1 Int.one && Int.eq imm2 Int.zero) eqn:HEQ10.
  { (* select cond 1 0 = Ocmp cond *)
    apply andb_true_iff in HEQ10. destruct HEQ10 as [HE1 HE2].
    apply Int.same_if_eq in HE1, HE2. subst imm1 imm2.
    exists (Val.of_optbool (eval_condition cond vl m)). split.
    - eapply eval_Eop. eassumption. simpl. reflexivity.
    - destruct (eval_condition cond vl m) as [[|]|]; simpl; auto. }
  destruct (Int.eq imm1 Int.zero && Int.eq imm2 Int.one) eqn:HEQ01.
  { (* select cond 0 1 = Ocmp (negate cond) *)
    apply andb_true_iff in HEQ01. destruct HEQ01 as [HE1 HE2].
    apply Int.same_if_eq in HE1, HE2. subst imm1 imm2.
    exists (Val.of_optbool (eval_condition (negate_condition cond) vl m)). split.
    - eapply eval_Eop. eassumption. simpl. reflexivity.
    - rewrite eval_negate_condition.
      destruct (eval_condition cond vl m) as [[|]|]; simpl; auto. }
  destruct (is_immed_arith CONST imm1 && is_immed_arith CONST imm2) eqn:?.
  - eexists; split; [EvalOp; simpl; eauto | apply Val.lessdef_normalize].
  - destruct (is_immed_arith CONST imm2) eqn:?.
    + eapply eval_selectimm; eauto. EvalOp.
    + eapply eval_selimmn; eauto. EvalOp.
Qed.

Ltac select_default := solve [eapply eval_Osel_default; eauto].

Theorem eval_select:
  forall le ty cond al vl a1 v1 a2 v2,
  select_supported ty = true ->
  eval_exprlist ge sp e m le al vl ->
  eval_expr ge sp e m le a1 v1 ->
  eval_expr ge sp e m le a2 v2 ->
  exists v,
     eval_expr ge sp e m le (select ty cond al a1 a2) v
  /\ Val.lessdef (Val.normalize (Val.select (eval_condition cond vl m) v1 v2) ty) v.
Proof.
  unfold select; intros.
  destruct ty; try select_default.
  (* Tint *)
  destruct a1 as [ | o e0 | | | | | | ];
    try (destruct a2 as [ | o' e0' | | | | | | ]; try select_default;
         destruct o'; try select_default;
         destruct e0'; try select_default;
         InvEval; subst; eapply eval_selectimm; eauto).
  (* a1 = Eop o e0 *)
  destruct o;
    try (destruct a2 as [ | o' e0' | | | | | | ]; try select_default;
         destruct o'; try select_default;
         destruct e0'; try select_default;
         InvEval; subst; eapply eval_selectimm; eauto).
  (* a1 = Eop (Ointconst i) e0 *)
  destruct e0;
    try (destruct a2 as [ | o' e0' | | | | | | ]; try select_default;
         destruct o'; try select_default;
         destruct e0'; try select_default;
         InvEval; subst; eapply eval_selectimm; eauto).
  (* a1 = Eop (Ointconst i) Enil *)
  destruct a2; try (InvEval; subst; eapply eval_selimmn; eauto).
  destruct o; try (InvEval; subst; eapply eval_selimmn; eauto).
  destruct e0; try (InvEval; subst; eapply eval_selimmn; eauto).
  (* both Ointconst Enil *)
  InvEval. subst. eapply eval_selectimm2; eauto.
Qed.

Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
Proof.
  red; intros until x. unfold cast8signed; case (cast8signed_match a); intros.
  InvEval. TrivialExists.
  TrivialExists.
Qed.

Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
Proof.
  red; intros until x. unfold cast8unsigned.
  destruct (cast8unsigned_match a) as [c el | addr args | a'].
- (* Eop (Ocmp c) el — result is already in [0,1]. *)
  exists x; split; [exact H|].
  inv H.
  match goal with [ H: eval_operation _ _ _ _ _ = Some _ |- _ ] => simpl in H; inv H end.
  destruct (eval_condition _ _ m) as [[]|]; simpl; auto using Val.lessdef_refl.
- (* Eload Mint8unsigned addr args — load already zero-extends to byte. *)
  exists x; split; [exact H|].
  inv H.
  unfold Mem.loadv in *.
  destruct vaddr; try discriminate.
  exploit Mem.load_cast; eauto. simpl. intros HX.
  rewrite <- HX. apply Val.lessdef_refl.
- (* default — fall back to [andimm 255]. *)
  rewrite Val.zero_ext_and. apply eval_andimm. lia.
Qed.

Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
Proof.
  red; intros until x. unfold cast16signed; case (cast16signed_match a); intros.
  InvEval. TrivialExists.
  TrivialExists.
Qed.

Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
Proof.
  red; intros until x. unfold cast16unsigned.
  destruct (cast16unsigned_match a) as [c el | addr args | a'].
- (* Eop (Ocmp c) el — result is already in [0,1]. *)
  exists x; split; [exact H|].
  inv H.
  match goal with [ H: eval_operation _ _ _ _ _ = Some _ |- _ ] => simpl in H; inv H end.
  destruct (eval_condition _ _ m) as [[]|]; simpl; auto using Val.lessdef_refl.
- (* Eload Mint16unsigned addr args — load already zero-extends to halfword. *)
  exists x; split; [exact H|].
  inv H.
  unfold Mem.loadv in *.
  destruct vaddr; try discriminate.
  exploit Mem.load_cast; eauto. simpl. intros HX.
  rewrite <- HX. apply Val.lessdef_refl.
- (* default — fall back to [andimm 65535]. *)
  rewrite Val.zero_ext_and. apply eval_andimm. lia.
Qed.

Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat.
Proof.
  red; intros. unfold singleoffloat. TrivialExists.
Qed.

Theorem eval_floatofsingle: unary_constructor_sound floatofsingle Val.floatofsingle.
Proof.
  red; intros. unfold floatofsingle. TrivialExists.
Qed.

Theorem eval_intoffloat:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.intoffloat x = Some y ->
  exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v.
Proof.
  intros; unfold intoffloat. TrivialExists.
Qed.

Theorem eval_floatofint:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.floatofint x = Some y ->
  exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v.
Proof.
  intros until y; unfold floatofint. case (floatofint_match a); intros.
  InvEval. simpl in H0. TrivialExists.
  TrivialExists.
Qed.

Theorem eval_intuoffloat:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.intuoffloat x = Some y ->
  exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v.
Proof.
  intros; unfold intuoffloat. TrivialExists.
Qed.

Theorem eval_floatofintu:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.floatofintu x = Some y ->
  exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v.
Proof.
  intros until y; unfold floatofintu. case (floatofintu_match a); intros.
  InvEval. simpl in H0. TrivialExists.
  TrivialExists.
Qed.

Theorem eval_intofsingle:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.intofsingle x = Some y ->
  exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v.
Proof.
  intros; unfold intofsingle. TrivialExists.
Qed.

Theorem eval_singleofint:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.singleofint x = Some y ->
  exists v, eval_expr ge sp e m le (singleofint a) v /\ Val.lessdef y v.
Proof.
  intros until y; unfold singleofint. case (singleofint_match a); intros.
  InvEval. simpl in H0. TrivialExists.
  TrivialExists.
Qed.

Theorem eval_intuofsingle:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.intuofsingle x = Some y ->
  exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v.
Proof.
  intros; unfold intuofsingle. TrivialExists.
Qed.

Theorem eval_singleofintu:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.singleofintu x = Some y ->
  exists v, eval_expr ge sp e m le (singleofintu a) v /\ Val.lessdef y v.
Proof.
  intros until y; unfold singleofintu. case (singleofintu_match a); intros.
  InvEval. simpl in H0. TrivialExists.
  TrivialExists.
Qed.

Theorem eval_addressing:
  forall le chunk a v b ofs,
  eval_expr ge sp e m le a v ->
  v = Vptr b ofs ->
  match addressing chunk a with (mode, args) =>
    exists vl,
    eval_exprlist ge sp e m le args vl /\
    eval_addressing ge sp mode vl = Some v
  end.
Proof.
  intros until v. unfold addressing; case (addressing_match a); intros; InvEval.
  exists (@nil val). split. eauto with evalexpr. simpl. auto.
  exists (v1 :: nil); split. eauto with evalexpr. simpl. congruence.
  destruct (can_use_Aindexed2shift chunk); simpl.
  exists (v1 :: v0 :: nil); split. eauto with evalexpr. congruence.
  exists (Vptr b ofs :: nil); split. constructor. EvalOp. simpl. congruence. constructor.
  simpl. rewrite Ptrofs.add_zero; auto.
  destruct (can_use_Aindexed2 chunk); simpl.
  exists (v1 :: v0 :: nil); split. eauto with evalexpr. congruence.
  exists (Vptr b ofs :: nil); split. constructor. EvalOp. simpl. congruence. constructor.
  simpl. rewrite Ptrofs.add_zero; auto.
  exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto.
Qed.

Theorem eval_builtin_arg:
  forall a v,
  eval_expr ge sp e m nil a v ->
  CminorSel.eval_builtin_arg ge sp e m (builtin_arg a) v.
Proof.
  intros until v. unfold builtin_arg; case (builtin_arg_match a); intros; InvEval.
- constructor.
- constructor.
- constructor.
- simpl in H5. inv H5. constructor.
- subst v. constructor; auto.
- inv H. InvEval. simpl in H6; inv H6. constructor; auto.
- inv H. InvEval. simpl in H6. rewrite <- Genv.shift_symbol_address_32 in H6 by auto.
  inv H6. constructor; auto.
- inv H. repeat constructor; auto.
- constructor; auto.
Qed.

Theorem eval_divf_base:
  forall le a b x y,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v.
Proof.
  intros; unfold divf_base.
  TrivialExists.
Qed.

Theorem eval_divfs_base:
  forall le a b x y,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v.
Proof.
  intros; unfold divfs_base.
  TrivialExists.
Qed.

Platform-specific known builtins

Theorem eval_platform_builtin:
  forall bf al a vl v le,
  platform_builtin bf al = Some a ->
  eval_exprlist ge sp e m le al vl ->
  platform_builtin_sem bf vl = Some v ->
  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
Proof.
  destruct bf; intros until le; intro Heval.
  1-3: inversion Heval; subst a; clear Heval;
       exists v; split; trivial;
       repeat (try econstructor; try eassumption).
  - (* BI_ctz *)
    inv Heval. intros Hexl Hsem.
    destruct vl as [|v1 [|? ?]]; try discriminate.
    destruct v1; simpl in Hsem; try discriminate; inv Hsem;
    (eexists; split;
      [eapply eval_Eop;
        [econstructor;
          [eapply eval_Eop; [eassumption | reflexivity]
          | econstructor]
        | reflexivity]
      | auto]).
  - (* BI_reverse_bits *)
    inversion Heval; subst a; clear Heval;
    exists v; split; trivial;
    repeat (try econstructor; try eassumption).
Qed.


Lemma eval_fast_isfinitef: forall le a a' m
    (GEN : fast_isfinitef a = Some a') v
    (EVAL : eval_expr ge sp e m le a v),
    exists v' : val,
      eval_expr ge sp e m le a' v' /\
        Val.lessdef (Val.of_optbool (Val.isfinitef v)) v'.
Proof.
  intros. rewrite <- ExtValues.fast_isfinitef2_correct.
  unfold ExtValues.fast_isfinitef2, fast_isfinitef in *.
  destruct (Archi.thumb2_support && Compopts.optim_fast_isfinite_int tt); inv GEN.
  eexists. split.
  { repeat econstructor. eassumption. }
  apply Val.lessdef_refl.
Qed.

Lemma eval_fast_isfinite: forall le a a' m
    (GEN : fast_isfinite a = Some a') v
    (EVAL : eval_expr ge sp e m le a v),
    exists v' : val,
      eval_expr ge sp e m le a' v' /\
        Val.lessdef (Val.of_optbool (Val.isfinite v)) v'.
Proof.
  intros. rewrite <- ExtValues.fast_isfinite_correct.
  unfold ExtValues.fast_isfinite, fast_isfinite in *.
  destruct (Archi.thumb2_support && Compopts.optim_fast_isfinite_int tt); inv GEN.
  eexists. split.
  { repeat econstructor. eassumption. }
  apply Val.lessdef_refl.
Qed.
End CMCONSTR.
Generated by coq2html