remove dead code

1 files changed, 0 insertions, 1283 deletions

diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v
index 754db6d5a..0475f0451 100644
--- a/src/Experiments/NewPipeline/Toplevel2.v
+++ b/src/Experiments/NewPipeline/Toplevel2.v
@@ -371,1210 +371,6 @@ mulmod = fun var : type -> Type => λ x x0 : var (type.base (base.type.list (bas
 
 End P192_64.
 
-(*
-(* TODO : delete *)
-Module PreFancy.
-  Section with_wordmax.
-    Context (log2wordmax : Z) (log2wordmax_pos : 1 < log2wordmax) (log2wordmax_even : log2wordmax mod 2 = 0).
-    Let wordmax := 2 ^ log2wordmax.
-    Lemma wordmax_gt_2 : 2 < wordmax.
-    Proof.
-      apply Z.le_lt_trans with (m:=2 ^ 1); [ reflexivity | ].
-      apply Z.pow_lt_mono_r; omega.
-    Qed.
-
-    Lemma wordmax_even : wordmax mod 2 = 0.
-    Proof.
-      replace 2 with (2 ^ 1) by reflexivity.
-      subst wordmax. apply Z.mod_same_pow; omega.
-    Qed.
-
-    Let half_bits := log2wordmax / 2.
-
-    Lemma half_bits_nonneg : 0 <= half_bits.
-    Proof. subst half_bits; Z.zero_bounds. Qed.
-
-    Let wordmax_half_bits := 2 ^ half_bits.
-
-    Lemma wordmax_half_bits_pos : 0 < wordmax_half_bits.
-    Proof. subst wordmax_half_bits half_bits. Z.zero_bounds. Qed.
-
-    Lemma half_bits_squared : (wordmax_half_bits - 1) * (wordmax_half_bits - 1) <= wordmax - 1.
-    Proof.
-      pose proof wordmax_half_bits_pos.
-      subst wordmax_half_bits.
-      transitivity (2 ^ (half_bits + half_bits) - 2 * 2 ^ half_bits + 1).
-      { rewrite Z.pow_add_r by (subst half_bits; Z.zero_bounds).
-        autorewrite with push_Zmul; omega. }
-      { transitivity (wordmax - 2 * 2 ^ half_bits + 1); [ | lia].
-        subst wordmax.
-        apply Z.add_le_mono_r.
-        apply Z.sub_le_mono_r.
-        apply Z.pow_le_mono_r; [ omega | ].
-        rewrite Z.add_diag; subst half_bits.
-        apply BinInt.Z.mul_div_le; omega. }
-    Qed.
-
-    Lemma wordmax_half_bits_le_wordmax : wordmax_half_bits <= wordmax.
-    Proof.
-      subst wordmax half_bits wordmax_half_bits.
-      apply Z.pow_le_mono_r; [lia|].
-      apply Z.div_le_upper_bound; lia.
-    Qed.
-
-    Lemma ones_half_bits : wordmax_half_bits - 1 = Z.ones half_bits.
-    Proof.
-      subst wordmax_half_bits. cbv [Z.ones].
-      rewrite Z.shiftl_mul_pow2, <-Z.sub_1_r by auto using half_bits_nonneg.
-      lia.
-    Qed.
-
-    Lemma wordmax_half_bits_squared : wordmax_half_bits * wordmax_half_bits = wordmax.
-    Proof.
-      subst wordmax half_bits wordmax_half_bits.
-      rewrite <-Z.pow_add_r by Z.zero_bounds.
-      rewrite Z.add_diag, Z.mul_div_eq by omega.
-      f_equal; lia.
-    Qed.
-
-(*
-    Section interp.
-      Context {interp_cast : zrange -> Z -> Z}.
-      Local Notation interp_scalar := (interp_scalar (interp_cast:=interp_cast)).
-      Local Notation interp_cast2 := (interp_cast2 (interp_cast:=interp_cast)).
-      Local Notation low x := (Z.land x (wordmax_half_bits - 1)).
-      Local Notation high x := (x >> half_bits).
-      Local Notation shift x imm := ((x << imm) mod wordmax).
-
-      Definition interp_ident {s d} (idc : ident s d) : type.interp s -> type.interp d :=
-        match idc with
-        | add imm => fun x => Z.add_get_carry_full wordmax (fst x) (shift (snd x) imm)
-        | addc imm => fun x => Z.add_with_get_carry_full wordmax (fst (fst x)) (snd (fst x)) (shift (snd x) imm)
-        | sub imm => fun x => Z.sub_get_borrow_full wordmax (fst x) (shift (snd x) imm)
-        | subb imm => fun x => Z.sub_with_get_borrow_full wordmax (fst (fst x)) (snd (fst x)) (shift (snd x) imm)
-        | mulll => fun x => low (fst x) * low (snd x)
-        | mullh => fun x => low (fst x) * high (snd x)
-        | mulhl => fun x => high (fst x) * low (snd x)
-        | mulhh => fun x => high (fst x) * high (snd x)
-        | rshi n => fun x => Z.rshi wordmax (fst x) (snd x) n
-        | selc => fun x => Z.zselect (fst (fst x)) (snd (fst x)) (snd x)
-        | selm => fun x => Z.zselect (Z.cc_m wordmax (fst (fst x))) (snd (fst x)) (snd x)
-        | sell => fun x => Z.zselect (Z.land (fst (fst x)) 1) (snd (fst x)) (snd x)
-        | addm => fun x => Z.add_modulo (fst (fst x)) (snd (fst x)) (snd x)
-        end.
-
-      Fixpoint interp {t} (e : @expr type.interp ident t) : type.interp t :=
-        match e with
-        | Scalar t s => interp_scalar s
-        | LetInAppIdentZ s d r idc x f =>
-          interp (f (interp_cast r (interp_ident idc (interp_scalar x))))
-        | LetInAppIdentZZ s d r idc x f =>
-          interp (f (interp_cast2 r (interp_ident idc (interp_scalar x))))
-        end.
-    End interp.
-
-    Section proofs.
-      Context (dummy_arrow : forall s d, type.interp (s -> d)%ctype) (consts : list Z)
-              (consts_ok : forall x, In x consts -> 0 <= x <= wordmax - 1).
-      Context {interp_cast : zrange -> Z -> Z} {interp_cast_correct : forall r x, lower r <= x <= upper r -> interp_cast r x = x}.
-      Local Notation interp_scalar := (interp_scalar (interp_cast:=interp_cast)).
-      Local Notation interp_cast2 := (interp_cast2 (interp_cast:=interp_cast)).
-
-      Local Notation word_range := (r[0~>wordmax-1])%zrange.
-      Local Notation half_word_range := (r[0~>wordmax_half_bits-1])%zrange.
-      Local Notation flag_range := (r[0~>1])%zrange.
-
-      Definition in_word_range (r : zrange) := is_tighter_than_bool r word_range = true.
-      Definition in_flag_range (r : zrange) := is_tighter_than_bool r flag_range = true.
-
-      Fixpoint get_range_var (t : type) : type.interp t -> range_type t :=
-        match t with
-        | type.type_primitive type.Z =>
-          fun x => {| lower := x; upper := x |}
-        | type.prod a b =>
-          fun x => (get_range_var a (fst x), get_range_var b (snd x))
-        | _ => fun _ => tt
-        end.
-
-      Fixpoint get_range {t} (x : @scalar type.interp t) : range_type t :=
-        match x with
-        | Var t v => get_range_var t v
-        | TT => tt
-        | Nil _ => tt
-        | Pair _ _ x y => (get_range x, get_range y)
-        | Cast r _ => r
-        | Cast2 r _ => r
-        | Fst _ _ p => fst (get_range p)
-        | Snd _ _ p => snd (get_range p)
-        | Shiftr n x => ZRange.map (fun y => Z.shiftr y n) (get_range x)
-        | Shiftl n x => ZRange.map (fun y => Z.shiftl y n) (get_range x)
-        | Land n x => r[0~>n]%zrange
-        | CC_m n x => ZRange.map (Z.cc_m n) (get_range x)
-        | Primitive type.Z x => {| lower := x; upper := x |}
-        | Primitive p x => tt
-        end.
-
-      Fixpoint has_range {t} : range_type t -> type.interp t -> Prop :=
-        match t with
-        | type.type_primitive type.Z =>
-          fun r x =>
-            lower r <= x <= upper r
-        | type.prod a b =>
-          fun r x =>
-            has_range (fst r) (fst x) /\ has_range (snd r) (snd x)
-        | _ => fun _ _ => True
-        end.
-
-      Inductive ok_scalar : forall {t}, @scalar type.interp t -> Prop :=
-      | sc_ok_var : forall t v, ok_scalar (Var t v)
-      | sc_ok_unit : ok_scalar TT
-      | sc_ok_nil : forall t, ok_scalar (Nil t)
-      | sc_ok_pair : forall A B x y,
-          @ok_scalar A x ->
-          @ok_scalar B y ->
-          ok_scalar (Pair x y)
-      | sc_ok_cast : forall r (x : scalar type.Z),
-          ok_scalar x ->
-          is_tighter_than_bool (get_range x) r = true ->
-          ok_scalar (Cast r x)
-      | sc_ok_cast2 : forall r (x : scalar (type.prod type.Z type.Z)),
-          ok_scalar x ->
-          is_tighter_than_bool (fst (get_range x)) (fst r) = true ->
-          is_tighter_than_bool (snd (get_range x)) (snd r) = true ->
-          ok_scalar (Cast2 r x)
-      | sc_ok_fst :
-          forall A B p, @ok_scalar (A * B) p -> ok_scalar (Fst p)
-      | sc_ok_snd :
-          forall A B p, @ok_scalar (A * B) p -> ok_scalar (Snd p)
-      | sc_ok_shiftr :
-          forall n x, 0 <= n -> ok_scalar x -> ok_scalar (Shiftr n x)
-      | sc_ok_shiftl :
-          forall n x, 0 <= n -> 0 <= lower (@get_range type.Z x) -> ok_scalar x -> ok_scalar (Shiftl n x)
-      | sc_ok_land :
-          forall n x, 0 <= n -> 0 <= lower (@get_range type.Z x) -> ok_scalar x -> ok_scalar (Land n x)
-      | sc_ok_cc_m :
-          forall x, ok_scalar x -> ok_scalar (CC_m wordmax x)
-      | sc_ok_prim : forall p x, ok_scalar (@Primitive _ p x)
-      .
-
-      Inductive is_halved : scalar type.Z -> Prop :=
-      | is_halved_lower :
-          forall x : scalar type.Z,
-            in_word_range (get_range x) ->
-            is_halved (Cast half_word_range (Land (wordmax_half_bits - 1) x))
-      | is_halved_upper :
-          forall x : scalar type.Z,
-            in_word_range (get_range x) ->
-            is_halved (Cast half_word_range (Shiftr half_bits x))
-      | is_halved_constant :
-          forall y z,
-            constant_to_scalar consts z = Some y ->
-            is_halved y ->
-            is_halved (Primitive (t:=type.Z) z)
-      .
-
-      Inductive ok_ident : forall s d, scalar s -> range_type d -> ident.ident s d -> Prop :=
-      | ok_add :
-          forall x y : scalar type.Z,
-            in_word_range (get_range x) ->
-            in_word_range (get_range y) ->
-            ok_ident _
-                     (type.prod type.Z type.Z)
-                     (Pair x y)
-                     (word_range, flag_range)
-                     (ident.Z.add_get_carry_concrete wordmax)
-      | ok_addc :
-          forall (c x y : scalar type.Z) outr,
-            in_flag_range (get_range c) ->
-            in_word_range (get_range x) ->
-            in_word_range (get_range y) ->
-            lower outr = 0 ->
-            (0 <= upper (get_range c) + upper (get_range x) + upper (get_range y) <= upper outr \/ outr = word_range) ->
-            ok_ident _
-                     (type.prod type.Z type.Z)
-                     (Pair (Pair c x) y)
-                     (outr, flag_range)
-                     (ident.Z.add_with_get_carry_concrete wordmax)
-      | ok_sub :
-          forall x y : scalar type.Z,
-            in_word_range (get_range x) ->
-            in_word_range (get_range y) ->
-            ok_ident _
-                     (type.prod type.Z type.Z)
-                     (Pair x y)
-                     (word_range, flag_range)
-                     (ident.Z.sub_get_borrow_concrete wordmax)
-      | ok_subb :
-          forall b x y : scalar type.Z,
-            in_flag_range (get_range b) ->
-            in_word_range (get_range x) ->
-            in_word_range (get_range y) ->
-            ok_ident _
-                     (type.prod type.Z type.Z)
-                     (Pair (Pair b x) y)
-                     (word_range, flag_range)
-                     (ident.Z.sub_with_get_borrow_concrete wordmax)
-      | ok_rshi :
-          forall (x : scalar (type.prod type.Z type.Z)) n outr,
-            in_word_range (fst (get_range x)) ->
-            in_word_range (snd (get_range x)) ->
-            (* note : using [outr] rather than [word_range] allows for cases where the result has been put in a smaller word size. *)
-            lower outr = 0 ->
-            0 <= n ->
-            ((0 <= (upper (snd (get_range x)) + upper (fst (get_range x)) * wordmax) / 2^n <= upper outr)
-              \/ outr = word_range) ->
-            ok_ident (type.prod type.Z type.Z) type.Z x outr (ident.Z.rshi_concrete wordmax n)
-      | ok_selc :
-          forall (x : scalar (type.prod type.Z type.Z)) (y z : scalar type.Z),
-            in_flag_range (snd (get_range x)) ->
-            in_word_range (get_range y) ->
-            in_word_range (get_range z) ->
-            ok_ident _
-                     type.Z
-                     (Pair (Pair (Cast flag_range (Snd x)) y) z)
-                     word_range
-                     ident.Z.zselect
-      | ok_selm :
-          forall x y z : scalar type.Z,
-            in_word_range (get_range x) ->
-            in_word_range (get_range y) ->
-            in_word_range (get_range z) ->
-            ok_ident _
-                     type.Z
-                     (Pair (Pair (Cast flag_range (CC_m wordmax x)) y) z)
-                     word_range
-                     ident.Z.zselect
-      | ok_sell :
-          forall x y z : scalar type.Z,
-            in_word_range (get_range x) ->
-            in_word_range (get_range y) ->
-            in_word_range (get_range z) ->
-            ok_ident _
-                     type.Z
-                     (Pair (Pair (Cast flag_range (Land 1 x)) y) z)
-                     word_range
-                     ident.Z.zselect
-      | ok_addm :
-          forall (x : scalar (type.prod (type.prod type.Z type.Z) type.Z)),
-            in_word_range (fst (fst (get_range x))) ->
-            in_word_range (snd (fst (get_range x))) ->
-            in_word_range (snd (get_range x)) ->
-            upper (fst (fst (get_range x))) + upper (snd (fst (get_range x))) - lower (snd (get_range x)) < wordmax ->
-            ok_ident _
-                     type.Z
-                     x
-                     word_range
-                     ident.Z.add_modulo
-      | ok_mul :
-          forall x y : scalar type.Z,
-            is_halved x ->
-            is_halved y ->
-            ok_ident (type.prod type.Z type.Z)
-                     type.Z
-                     (Pair x y)
-                     word_range
-                     ident.Z.mul
-      .
-
-      Inductive ok_expr : forall {t}, @expr type.interp ident.ident t -> Prop :=
-      | ok_of_scalar : forall t s, ok_scalar s -> @ok_expr t (Scalar s)
-      | ok_letin_z : forall s d r idc x f,
-          ok_ident _ type.Z x r idc ->
-          (r <=? word_range)%zrange = true ->
-          ok_scalar x ->
-          (forall y, has_range (t:=type.Z) r y -> ok_expr (f y)) ->
-          ok_expr (@LetInAppIdentZ _ _ s d r idc x f)
-      | ok_letin_zz : forall s d r idc x f,
-          ok_ident _ (type.prod type.Z type.Z) x (r, flag_range) idc ->
-          (r <=? word_range)%zrange = true ->
-          ok_scalar x ->
-          (forall y, has_range (t:=type.Z * type.Z) (r, flag_range) y -> ok_expr (f y)) ->
-          ok_expr (@LetInAppIdentZZ _ _ s d (r, flag_range) idc x f)
-      .
-
-      Ltac invert H :=
-        inversion H; subst;
-        repeat match goal with
-               | H : existT _ _ _ = existT _ _ _ |- _ => apply (Eqdep_dec.inj_pair2_eq_dec _ type.type_eq_dec) in H; subst
-               end.
-
-      Lemma has_range_get_range_var {t} (v : type.interp t) :
-        has_range (get_range_var _ v) v.
-      Proof.
-        induction t; cbn [get_range_var has_range fst snd]; auto.
-        destruct p; auto; cbn [upper lower]; omega.
-      Qed.
-
-      Lemma has_range_loosen r1 r2 (x : Z) :
-        @has_range type.Z r1 x ->
-        is_tighter_than_bool r1 r2 = true ->
-        @has_range type.Z r2 x.
-      Proof.
-        cbv [is_tighter_than_bool has_range]; intros;
-          match goal with H : _ && _ = true |- _ => rewrite andb_true_iff in H; destruct H end;
-          Z.ltb_to_lt; omega.
-      Qed.
-
-      Lemma interp_cast_noop x r :
-        @has_range type.Z r x ->
-        interp_cast r x = x.
-      Proof. cbv [has_range]; intros; auto. Qed.
-
-      Lemma interp_cast2_noop x r :
-        @has_range (type.prod type.Z type.Z) r x ->
-        interp_cast2 r x = x.
-      Proof.
-        cbv [has_range interp_cast2]; intros.
-        rewrite !interp_cast_correct by tauto.
-        destruct x; reflexivity.
-      Qed.
-
-      Lemma has_range_shiftr n (x : scalar type.Z) :
-        0 <= n ->
-        has_range (get_range x) (interp_scalar x) ->
-        @has_range type.Z (ZRange.map (fun y : Z => y >> n) (get_range x)) (interp_scalar x >> n).
-      Proof. cbv [has_range]; intros; cbn. auto using Z.shiftr_le with omega. Qed.
-      Hint Resolve has_range_shiftr : has_range.
-
-      Lemma has_range_shiftl n r x :
-        0 <= n -> 0 <= lower r ->
-        @has_range type.Z r x ->
-        @has_range type.Z (ZRange.map (fun y : Z => y << n) r) (x << n).
-      Proof. cbv [has_range]; intros; cbn. auto using Z.shiftl_le_mono with omega. Qed.
-      Hint Resolve has_range_shiftl : has_range.
-
-      Lemma has_range_land n (x : scalar type.Z) :
-        0 <= n -> 0 <= lower (get_range x) ->
-        has_range (get_range x) (interp_scalar x) ->
-        @has_range type.Z (r[0~>n])%zrange (Z.land (interp_scalar x) n).
-      Proof.
-        cbv [has_range]; intros; cbn.
-        split; [ apply Z.land_nonneg | apply Z.land_upper_bound_r ]; omega.
-      Qed.
-      Hint Resolve has_range_land : has_range.
-
-      Lemma has_range_interp_scalar {t} (x : scalar t) :
-        ok_scalar x ->
-        has_range (get_range x) (interp_scalar x).
-      Proof.
-        induction 1; cbn [interp_scalar get_range];
-          auto with has_range;
-          try solve [try inversion IHok_scalar; cbn [has_range];
-                     auto using has_range_get_range_var]; [ | | | ].
-        { rewrite interp_cast_noop by eauto using has_range_loosen.
-          eapply has_range_loosen; eauto. }
-        { inversion IHok_scalar.
-          rewrite interp_cast2_noop;
-            cbn [has_range]; split; eapply has_range_loosen; eauto. }
-        { cbn. cbv [has_range] in *.
-          pose proof wordmax_gt_2.
-          rewrite !Z.cc_m_eq by omega.
-          split; apply Z.div_le_mono; Z.zero_bounds; omega. }
-        { destruct p; cbn [has_range upper lower]; auto; omega. }
-      Qed.
-      Hint Resolve has_range_interp_scalar : has_range.
-
-      Lemma has_word_range_interp_scalar (x : scalar type.Z) :
-        ok_scalar x ->
-        in_word_range (get_range x) ->
-        @has_range type.Z word_range (interp_scalar x).
-      Proof. eauto using has_range_loosen, has_range_interp_scalar. Qed.
-
-      Lemma in_word_range_nonneg r : in_word_range r -> 0 <= lower r.
-      Proof.
-        cbv [in_word_range is_tighter_than_bool].
-        rewrite andb_true_iff; intuition.
-      Qed.
-
-      Lemma in_word_range_upper_nonneg r x : @has_range type.Z r x -> in_word_range r -> 0 <= upper r.
-      Proof.
-        cbv [in_word_range is_tighter_than_bool]; cbn.
-        rewrite andb_true_iff; intuition.
-        Z.ltb_to_lt. omega.
-      Qed.
-
-      Lemma has_word_range_shiftl n r x :
-        0 <= n -> upper r * 2 ^ n <= wordmax - 1 ->
-        @has_range type.Z r x ->
-        in_word_range r ->
-        @has_range type.Z word_range (x << n).
-      Proof.
-        intros.
-        eapply has_range_loosen;
-          [ apply has_range_shiftl; eauto using in_word_range_nonneg with has_range; omega | ].
-        cbv [is_tighter_than_bool]. cbn.
-        apply andb_true_iff; split; apply Z.leb_le;
-          [ apply Z.shiftl_nonneg; solve [auto using in_word_range_nonneg] | ].
-        rewrite Z.shiftl_mul_pow2 by omega.
-        auto.
-      Qed.
-
-      Lemma has_range_rshi r n x y :
-        0 <= n ->
-        0 <= x ->
-        0 <= y ->
-        lower r = 0 ->
-        (0 <= (y + x * wordmax) / 2^n <= upper r \/ r = word_range) ->
-        @has_range type.Z r (Z.rshi wordmax x y n).
-      Proof.
-        pose proof wordmax_gt_2.
-        intros. cbv [has_range].
-        rewrite Z.rshi_correct by omega.
-        match goal with |- context [?x mod ?m] =>
-                        pose proof (Z.mod_pos_bound x m ltac:(omega)) end.
-        split; [lia|].
-        intuition.
-        { destruct (Z_lt_dec (upper r) wordmax); [ | lia].
-          rewrite Z.mod_small by (split; Z.zero_bounds; omega).
-          omega. }
-        { subst r. cbn [upper]. omega. }
-      Qed.
-
-      Lemma in_word_range_spec r :
-        (0 <= lower r /\ upper r <= wordmax - 1)
-        <-> in_word_range r.
-      Proof.
-        intros; cbv [in_word_range is_tighter_than_bool].
-        rewrite andb_true_iff.
-        intuition; apply Z.leb_le; cbn [upper lower]; try omega.
-      Qed.
-
-      Ltac destruct_scalar :=
-        match goal with
-        | x : scalar (type.prod (type.prod _ _) _) |- _ =>
-          match goal with |- context [interp_scalar x] =>
-            destruct (interp_scalar x) as [ [? ?] ?];
-            destruct (get_range x) as [ [? ?] ?]
-          end
-        | x : scalar (type.prod _ _) |- _ =>
-          match goal with |- context [interp_scalar x] =>
-            destruct (interp_scalar x) as [? ?]; destruct (get_range x) as [? ?]
-          end
-        end.
-
-      Ltac extract_ok_scalar' level x :=
-        match goal with
-        | H : ok_scalar (Pair (Pair (?f (?g x)) _) _) |- _ =>
-          match (eval compute in (4 <=? level)) with
-          | true => invert H; extract_ok_scalar' 3 x
-          | _ => fail
-          end
-        | H : ok_scalar (Pair (?f (?g x)) _) |- _ =>
-          match (eval compute in (3 <=? level)) with
-          | true => invert H; extract_ok_scalar' 2 x
-          | _ => fail
-          end
-        | H : ok_scalar (Pair _ (?f (?g x))) |- _ =>
-          match (eval compute in (3 <=? level)) with
-          | true => invert H; extract_ok_scalar' 2 x
-          | _ => fail
-          end
-        | H : ok_scalar (?f (?g x)) |- _ =>
-          match (eval compute in (2 <=? level)) with
-          | true => invert H; extract_ok_scalar' 1 x
-          | _ => fail
-          end
-        | H : ok_scalar (Pair (Pair x _) _) |- _ =>
-          match (eval compute in (2 <=? level)) with
-          | true => invert H; extract_ok_scalar' 1 x
-          | _ => fail
-          end
-        | H : ok_scalar (Pair (Pair _ x) _) |- _ =>
-          match (eval compute in (2 <=? level)) with
-          | true => invert H; extract_ok_scalar' 1 x
-          | _ => fail
-          end
-        | H : ok_scalar (?g x) |- _ => invert H
-        | H : ok_scalar (Pair x _) |- _ => invert H
-        | H : ok_scalar (Pair _ x) |- _ => invert H
-        end.
-
-      Ltac extract_ok_scalar :=
-        match goal with |- ok_scalar ?x => extract_ok_scalar' 4 x; assumption end.
-
-      Lemma has_half_word_range_shiftr r x :
-        in_word_range r ->
-        @has_range type.Z r x ->
-        @has_range type.Z half_word_range (x >> half_bits).
-      Proof.
-        cbv [in_word_range is_tighter_than_bool].
-        rewrite andb_true_iff.
-        cbn [has_range upper lower]; intros; intuition; Z.ltb_to_lt.
-        { apply Z.shiftr_nonneg. omega. }
-        { pose proof half_bits_nonneg.
-          pose proof half_bits_squared.
-          assert (x >> half_bits < wordmax_half_bits); [|omega].
-          rewrite Z.shiftr_div_pow2 by auto.
-          apply Z.div_lt_upper_bound; Z.zero_bounds.
-          subst wordmax_half_bits half_bits.
-          rewrite <-Z.pow_add_r by omega.
-          rewrite Z.add_diag, Z.mul_div_eq, log2wordmax_even by omega.
-          autorewrite with zsimplify_fast. subst wordmax. omega. }
-      Qed.
-
-      Lemma has_half_word_range_land r x :
-        in_word_range r ->
-        @has_range type.Z r x ->
-        @has_range type.Z half_word_range (x &' (wordmax_half_bits - 1)).
-      Proof.
-        pose proof wordmax_half_bits_pos.
-        cbv [in_word_range is_tighter_than_bool].
-        rewrite andb_true_iff.
-        cbn [has_range upper lower]; intros; intuition; Z.ltb_to_lt.
-        { apply Z.land_nonneg; omega. }
-        { apply Z.land_upper_bound_r; omega. }
-      Qed.
-
-      Section constant_to_scalar.
-        Lemma constant_to_scalar_single_correct s x z :
-            0 <= x <= wordmax - 1 ->
-            constant_to_scalar_single x z = Some s -> interp_scalar s = z.
-        Proof.
-          cbv [constant_to_scalar_single].
-          break_match; try discriminate; intros; Z.ltb_to_lt; subst;
-            try match goal with H : Some _ = Some _ |- _ => inversion H; subst end;
-            cbn [interp_scalar]; apply interp_cast_noop.
-          { apply has_half_word_range_shiftr with (r:=r[x~>x]%zrange);
-            cbv [in_word_range is_tighter_than_bool upper lower has_range]; try omega.
-            apply andb_true_iff; split; apply Z.leb_le; omega. }
-          { apply has_half_word_range_land with (r:=r[x~>x]%zrange);
-            cbv [in_word_range is_tighter_than_bool upper lower has_range]; try omega.
-            apply andb_true_iff; split; apply Z.leb_le; omega. }
-        Qed.
-
-        Lemma constant_to_scalar_correct s z :
-          constant_to_scalar consts z = Some s -> interp_scalar s = z.
-        Proof.
-          cbv [constant_to_scalar].
-          apply fold_right_invariant; try discriminate.
-          intros until 2; break_match; eauto using constant_to_scalar_single_correct.
-        Qed.
-
-        Lemma constant_to_scalar_single_cases x y z :
-          @constant_to_scalar_single type.interp x z = Some y ->
-          (y = Cast half_word_range (Land (wordmax_half_bits - 1) (Primitive (t:=type.Z) x)))
-          \/ (y = Cast half_word_range (Shiftr half_bits (Primitive (t:=type.Z) x))).
-        Proof.
-          cbv [constant_to_scalar_single].
-          break_match; try discriminate; intros; Z.ltb_to_lt; subst;
-            try match goal with H : Some _ = Some _ |- _ => inversion H; subst end;
-            tauto.
-        Qed.
-
-        Lemma constant_to_scalar_cases y z :
-          @constant_to_scalar type.interp consts z = Some y ->
-          (exists x,
-              @has_range type.Z word_range x
-              /\ y = Cast half_word_range (Land (wordmax_half_bits - 1) (Primitive x)))
-          \/ (exists x,
-                 @has_range type.Z word_range x
-                 /\ y = Cast half_word_range (Shiftr half_bits (Primitive x))).
-        Proof.
-          cbv [constant_to_scalar].
-          apply fold_right_invariant; try discriminate.
-          intros until 2; break_match; eauto; intros.
-          match goal with H : constant_to_scalar_single _ _ = _ |- _ =>
-                          destruct (constant_to_scalar_single_cases _ _ _ H); subst end.
-          { left; eexists; split; eauto.
-            apply consts_ok; auto. }
-          { right; eexists; split; eauto.
-            apply consts_ok; auto. }
-        Qed.
-
-        Lemma ok_scalar_constant_to_scalar y z : constant_to_scalar consts z = Some y -> ok_scalar y.
-        Proof.
-          pose proof wordmax_half_bits_pos. pose proof half_bits_nonneg.
-          let H := fresh in
-          intro H; apply constant_to_scalar_cases in H; destruct H as [ [? ?] | [? ?] ]; intuition; subst;
-            cbn [has_range lower upper] in *; repeat constructor; cbn [lower get_range]; try apply Z.leb_refl; try omega.
-          assert (in_word_range r[x~>x]) by (apply in_word_range_spec; cbn [lower upper]; omega).
-          pose proof (has_half_word_range_shiftr r[x~>x] x ltac:(assumption) ltac:(cbv [has_range lower upper]; omega)).
-          cbn [has_range ZRange.map is_tighter_than_bool lower upper] in *.
-          apply andb_true_iff; cbn [lower upper]; split; apply Z.leb_le; omega.
-        Qed.
-      End constant_to_scalar.
-      Hint Resolve ok_scalar_constant_to_scalar.
-
-      Lemma is_halved_has_range x :
-        ok_scalar x ->
-        is_halved x ->
-        @has_range type.Z half_word_range (interp_scalar x).
-      Proof.
-        intro; pose proof (has_range_interp_scalar x ltac:(assumption)).
-        induction 1; cbn [interp_scalar] in *; intros; try assumption; [ ].
-        rewrite <-(constant_to_scalar_correct y z) by assumption.
-        eauto using has_range_interp_scalar.
-      Qed.
-
-      Lemma ident_interp_has_range s d x r idc:
-        ok_scalar x ->
-        ok_ident s d x r idc ->
-        has_range r (ident.interp idc (interp_scalar x)).
-      Proof.
-        intro.
-        pose proof (has_range_interp_scalar x ltac:(assumption)).
-        pose proof wordmax_gt_2.
-        induction 1; cbn [ident.interp ident.gen_interp]; intros; try destruct_scalar;
-          repeat match goal with
-                 | H : _ && _ = true |- _ => rewrite andb_true_iff in H; destruct H; Z.ltb_to_lt
-                 |  H : _ /\ _ |- _ => destruct H
-                 | H : is_halved _ |- _ => apply is_halved_has_range in H; [ | extract_ok_scalar ]
-                 | _ => progress subst
-                 | _ => progress (cbv [in_word_range in_flag_range is_tighter_than_bool] in * )
-                 | _ => progress (cbn [interp_scalar get_range has_range upper lower fst snd] in * )
-                 end.
-        {
-          autorewrite with to_div_mod.
-          match goal with |- context[?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end.
-          rewrite Z.div_between_0_if by omega.
-          split; break_match; lia. }
-        {
-          autorewrite with to_div_mod.
-          match goal with |- context[?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end.
-          rewrite Z.div_between_0_if by omega.
-          match goal with H : _ \/ _ |- _ => destruct H; subst end.
-          { split; break_match; try lia.
-            destruct (Z_lt_dec (upper outr) wordmax).
-            { match goal with |- _ <= ?y mod _ <= ?u =>
-                              assert (y <= u) by nia end.
-              rewrite Z.mod_small by omega. omega. }
-            { match goal with|- context [?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end.
-              omega. } }
-          { split; break_match; cbn; lia. } }
-        {
-          autorewrite with to_div_mod.
-          match goal with |- context[?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end.
-          rewrite Z.div_sub_small by omega.
-          split; break_match; lia. }
-        {
-          autorewrite with to_div_mod.
-          match goal with |- context [?a - ?b - ?c] => replace (a - b - c) with (a - (b + c)) by ring end.
-          match goal with |- context[?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end.
-          rewrite Z.div_sub_small by omega.
-          split; break_match; lia. }
-        { apply has_range_rshi; try nia; [ ].
-          match goal with H : context [upper ?ra + upper ?rb * wordmax] |- context [?a + ?b * wordmax] =>
-                          assert ((a + b * wordmax) / 2^n <= (upper ra + upper rb * wordmax) / 2^n) by (apply Z.div_le_mono; Z.zero_bounds; nia)
-          end.
-          match goal with H : _ \/ ?P |- _ \/ ?P => destruct H; [left|tauto] end.
-          split; Z.zero_bounds; nia. }
-        { rewrite Z.zselect_correct. break_match; omega. }
-        { cbn [interp_scalar fst snd get_range] in *.
-          rewrite Z.zselect_correct. break_match; omega. }
-        { cbn [interp_scalar fst snd get_range] in *.
-          rewrite Z.zselect_correct. break_match; omega. }
-        { rewrite Z.add_modulo_correct.
-          break_match; Z.ltb_to_lt; omega. }
-        { cbn [interp_scalar has_range fst snd get_range upper lower] in *.
-          pose proof half_bits_squared. nia. }
-      Qed.
-
-      Lemma has_flag_range_cc_m r x :
-        @has_range type.Z r x ->
-        in_word_range r ->
-        @has_range type.Z flag_range (Z.cc_m wordmax x).
-      Proof.
-        cbv [has_range in_word_range is_tighter_than_bool].
-        cbn [upper lower]; rewrite andb_true_iff; intros.
-        match goal with H : _ /\ _ |- _ => destruct H; Z.ltb_to_lt end.
-        pose proof wordmax_gt_2. pose proof wordmax_even.
-        pose proof (Z.cc_m_small wordmax x). omega.
-      Qed.
-
-      Lemma has_flag_range_cc_m' (x : scalar type.Z) :
-        ok_scalar x ->
-        in_word_range (get_range x) ->
-        @has_range type.Z flag_range (Z.cc_m wordmax (interp_scalar x)).
-      Proof. eauto using has_flag_range_cc_m with has_range. Qed.
-
-      Lemma has_flag_range_land r x :
-        @has_range type.Z r x ->
-        in_word_range r ->
-        @has_range type.Z flag_range (Z.land x 1).
-      Proof.
-        cbv [has_range in_word_range is_tighter_than_bool].
-        cbn [upper lower]; rewrite andb_true_iff; intuition; Z.ltb_to_lt.
-        { apply Z.land_nonneg. left; omega. }
-        { apply Z.land_upper_bound_r; omega. }
-      Qed.
-
-      Lemma has_flag_range_land' (x : scalar type.Z) :
-        ok_scalar x ->
-        in_word_range (get_range x) ->
-        @has_range type.Z flag_range (Z.land (interp_scalar x) 1).
-      Proof. eauto using has_flag_range_land with has_range. Qed.
-
-      Ltac rewrite_cast_noop_in_mul :=
-        repeat match goal with
-               | _ => rewrite interp_cast_noop with (r:=half_word_range) in *
-                   by (eapply has_range_loosen; auto using has_range_land, has_range_interp_scalar)
-               | _ => rewrite interp_cast_noop with (r:=half_word_range) in *
-                   by (eapply has_range_loosen; try apply has_range_shiftr; auto using has_range_interp_scalar;
-                       cbn [ZRange.map get_range] in *; auto)
-               | _ => rewrite interp_cast_noop by assumption
-               end.
-
-      Lemma is_halved_cases x :
-        is_halved x ->
-        ok_scalar x ->
-        (exists y,
-            invert_lower consts x = Some y
-            /\ invert_upper consts x = None
-            /\ interp_scalar y &' (wordmax_half_bits - 1) = interp_scalar x)
-        \/ (exists y,
-               invert_lower consts x = None
-               /\ invert_upper consts x = Some y
-               /\ interp_scalar y >> half_bits = interp_scalar x).
-      Proof.
-        induction 1; intros; cbn; rewrite ?Z.eqb_refl; cbn.
-        { left. eexists; repeat split; auto.
-          rewrite interp_cast_noop; [ reflexivity | ].
-          apply has_half_word_range_land with (r:=get_range x); auto.
-          apply has_range_interp_scalar; extract_ok_scalar. }
-        { right. eexists; repeat split; auto.
-          rewrite interp_cast_noop; [ reflexivity | ].
-          apply has_half_word_range_shiftr with (r:=get_range x); auto.
-          apply has_range_interp_scalar; extract_ok_scalar. }
-        { match goal with H : constant_to_scalar _ _ = Some _ |- _ =>
-                          rewrite H;
-                            let P := fresh in
-                            destruct (constant_to_scalar_cases _ _ H) as [ [? [? ?] ] | [? [? ?] ] ];
-                              subst; cbn; rewrite ?Z.eqb_refl; cbn
-          end.
-          { left; eexists; repeat split; auto.
-            erewrite <-constant_to_scalar_correct by eassumption.
-            subst. cbn.
-            rewrite interp_cast_noop; [ reflexivity | ].
-            eapply has_half_word_range_land with (r:=word_range); auto.
-            cbv [in_word_range is_tighter_than_bool].
-            rewrite !Z.leb_refl; reflexivity. }
-          { right; eexists; repeat split; auto.
-            erewrite <-constant_to_scalar_correct by eassumption.
-            subst. cbn.
-            rewrite interp_cast_noop; [ reflexivity | ].
-            eapply has_half_word_range_shiftr with (r:=word_range); auto.
-            cbv [in_word_range is_tighter_than_bool].
-            rewrite !Z.leb_refl; reflexivity. } }
-      Qed.
-
-      Lemma halved_mul_range x y :
-        ok_scalar (Pair x y) ->
-        is_halved x ->
-        is_halved y ->
-        0 <= interp_scalar x * interp_scalar y < wordmax.
-      Proof.
-        intro Hok; invert Hok. intros.
-        repeat match goal with H : _ |- _ => apply is_halved_has_range in H; [|assumption] end.
-        cbv [has_range lower upper] in *.
-        pose proof half_bits_squared. nia.
-      Qed.
-
-      Lemma of_straightline_ident_mul_correct r t x y g :
-        is_halved x ->
-        is_halved y ->
-        ok_scalar (Pair x y) ->
-        (word_range <=? r)%zrange = true ->
-        @has_range type.Z word_range (ident.interp ident.Z.mul (interp_scalar (Pair x y))) ->
-        @interp interp_cast _ (of_straightline_ident dummy_arrow consts ident.Z.mul t r (Pair x y) g) =
-        @interp interp_cast _ (g (ident.interp ident.Z.mul (interp_scalar (Pair x y)))).
-      Proof.
-        intros Hx Hy Hok ? ?; invert Hok; cbn [interp_scalar of_straightline_ident];
-        destruct (is_halved_cases x Hx ltac:(assumption)) as [ [? [Pxlow [Pxhigh Pxi] ] ] | [? [Pxlow [Pxhigh Pxi] ] ] ];
-          rewrite ?Pxlow, ?Pxhigh;
-          destruct (is_halved_cases y Hy ltac:(assumption)) as [ [? [Pylow [Pyhigh Pyi] ] ] | [? [Pylow [Pyhigh Pyi] ] ] ];
-          rewrite ?Pylow, ?Pyhigh;
-          cbn; rewrite Pxi, Pyi; assert (0 <= interp_scalar x * interp_scalar y < wordmax) by (auto using halved_mul_range);
-            rewrite interp_cast_noop by (cbv [is_tighter_than_bool] in *; cbn [has_range upper lower] in *; rewrite andb_true_iff in *; intuition; Z.ltb_to_lt; lia); reflexivity.
-      Qed.
-
-      Lemma has_word_range_mod_small x:
-        @has_range type.Z word_range x ->
-        x mod wordmax = x.
-      Proof.
-        cbv [has_range upper lower].
-        intros. apply Z.mod_small; omega.
-      Qed.
-
-      Lemma half_word_range_le_word_range r :
-        upper r = wordmax_half_bits - 1 ->
-        lower r = 0 ->
-        (r <=? word_range)%zrange = true.
-      Proof.
-        pose proof wordmax_half_bits_le_wordmax.
-        destruct r; cbv [is_tighter_than_bool ZRange.lower ZRange.upper].
-        intros; subst.
-        apply andb_true_iff; split; Z.ltb_to_lt; lia.
-      Qed.
-
-      Lemma and_shiftl_half_bits_eq x :
-        (x &' (wordmax_half_bits - 1)) << half_bits = x << half_bits mod wordmax.
-      Proof.
-        rewrite ones_half_bits.
-        rewrite Z.land_ones, !Z.shiftl_mul_pow2 by auto using half_bits_nonneg.
-        rewrite <-wordmax_half_bits_squared.
-        subst wordmax_half_bits.
-        rewrite Z.mul_mod_distr_r_full.
-        reflexivity.
-      Qed.
-
-      Lemma in_word_range_word_range : in_word_range word_range.
-      Proof.
-        cbv [in_word_range is_tighter_than_bool].
-        rewrite !Z.leb_refl; reflexivity.
-      Qed.
-
-      Lemma invert_shift_correct (s : scalar type.Z) x imm :
-        ok_scalar s ->
-        invert_shift consts s = Some (x, imm) ->
-        interp_scalar s = (interp_scalar x << imm) mod wordmax.
-      Proof.
-        intros Hok ?; invert Hok;
-          try match goal with H : ok_scalar ?x, H' : context[Cast _ ?x] |- _ =>
-                          invert H end;
-          try match goal with H : ok_scalar ?x, H' : context[Shiftl _ ?x] |- _ =>
-                          invert H end;
-          try match goal with H : ok_scalar ?x, H' : context[Shiftl _ (Cast _ ?x)] |- _ =>
-                          invert H end;
-          try (cbn [invert_shift invert_upper invert_upper'] in *; discriminate);
-          repeat match goal with
-                 | _ => progress (cbn [invert_shift invert_lower invert_lower' invert_upper invert_upper' interp_scalar fst snd] in * )
-                 | _ => rewrite interp_cast_noop by eauto using has_half_word_range_land, has_half_word_range_shiftr, in_word_range_word_range, has_range_loosen
-                 | H : ok_scalar (Shiftr _ _) |- _ => apply has_range_interp_scalar in H
-                 | H : ok_scalar (Shiftl _ _) |- _ => apply has_range_interp_scalar in H
-                 | H : ok_scalar (Land _ _) |- _ => apply has_range_interp_scalar in H
-                 | H : context [if ?x then _ else _] |- _ =>
-                   let Heq := fresh in case_eq x; intro Heq; rewrite Heq in H
-                 | H : context [match @constant_to_scalar ?v ?consts ?x with _ => _ end] |- _ =>
-                   let Heq := fresh in
-                   case_eq (@constant_to_scalar v consts x); intros until 0; intro Heq; rewrite Heq in *; [|discriminate];
-                     destruct (constant_to_scalar_cases _ _ Heq) as [ [? [? ?] ] | [? [? ?] ] ]; subst;
-                       pose proof (ok_scalar_constant_to_scalar _ _ Heq)
-                 | H : constant_to_scalar _ _ = Some _ |- _ => erewrite <-(constant_to_scalar_correct _ _ H)
-                 | H : _ |- _ => rewrite andb_true_iff in H; destruct H; Z.ltb_to_lt
-                 | H : Some _ = Some _ |- _ => progress (invert H)
-                 | _ => rewrite has_word_range_mod_small by eauto using has_range_loosen, half_word_range_le_word_range
-                 | _ => rewrite has_word_range_mod_small by
-                       (eapply has_range_loosen with (r1:=half_word_range);
-                        [ eapply has_half_word_range_shiftr with (r:=word_range) | ];
-                        eauto using in_word_range_word_range, half_word_range_le_word_range)
-                 | _ => rewrite and_shiftl_half_bits_eq
-                 | _ => progress subst
-                 | _ => reflexivity
-                 | _ => discriminate
-                 end.
-      Qed.
-
-      Local Ltac solve_commutative_replace :=
-        match goal with
-               | |- @eq (_ * _) ?x ?y =>
-                 replace x with (fst x, snd x) by (destruct x; reflexivity);
-                 replace y with (fst y, snd y) by (destruct y; reflexivity)
-        end; autorewrite with to_div_mod; solve [repeat (f_equal; try ring)].
-
-      Fixpoint is_tighter_than_bool_range_type t : range_type t -> range_type t -> bool :=
-        match t with
-        | type.type_primitive type.Z => (fun r1 r2 => (r1 <=? r2)%zrange)
-        | type.prod a b => fun r1 r2 =>
-                             (is_tighter_than_bool_range_type a (fst r1) (fst r2))
-                               && (is_tighter_than_bool_range_type b (snd r1) (snd r2))
-        | _ => fun _ _ => true
-        end.
-
-      Definition range_ok {t} : range_type t -> Prop :=
-        match t with
-        | type.type_primitive type.Z => fun r => in_word_range r
-        | type.prod type.Z type.Z => fun r => in_word_range (fst r) /\ snd r = flag_range
-        | _ => fun _ => False
-        end.
-
-      Lemma of_straightline_ident_correct s d t x r r' (idc : ident.ident s d) g :
-        ok_ident s d x r idc ->
-        range_ok r' ->
-        is_tighter_than_bool_range_type d r r' = true ->
-        ok_scalar x ->
-        @interp interp_cast _ (of_straightline_ident dummy_arrow consts idc t r' x g) =
-        @interp interp_cast _ (g (ident.interp idc (interp_scalar x))).
-      Proof.
-        intros.
-        pose proof wordmax_half_bits_pos.
-        pose proof (ident_interp_has_range _ _ x r idc ltac:(assumption) ltac:(assumption)).
-        match goal with H : ok_ident _ _ _ _ _ |- _ => induction H end;
-          try solve [auto using of_straightline_ident_mul_correct];
-          cbv [is_tighter_than_bool_range_type is_tighter_than_bool range_ok] in *;
-          cbn [of_straightline_ident ident.interp ident.gen_interp
-                                     invert_selm invert_sell] in *;
-            intros; rewrite ?Z.eqb_refl; cbn [andb];
-            try match goal with |- context [invert_shift] => break_match end;
-            cbn [interp interp_ident]; try destruct_scalar;
-          repeat match goal with
-                   | _ => progress (cbn [fst snd interp_scalar] in * )
-                   | _ => progress break_match; [ ]
-                   | _ => progress autorewrite with zsimplify_fast
-                   | _ => progress Z.ltb_to_lt
-                   | H : _ /\ _ |- _ => destruct H
-                   | _ => rewrite andb_true_iff in *
-                   | _ => rewrite interp_cast_noop with (r:=flag_range) in *
-                       by (apply has_flag_range_cc_m'; auto; extract_ok_scalar)
-                   | _ => rewrite interp_cast_noop with (r:=flag_range) in *
-                       by (apply has_flag_range_land'; auto; extract_ok_scalar)
-                   | H : _ = (_,_) |- _ => progress (inversion H; subst)
-                   | H : invert_shift _ _ = Some _ |- _ =>
-                     apply invert_shift_correct in H; [|extract_ok_scalar];
-                       rewrite <-H
-                   | H : has_range ?r  (?f ?x ?y) |- context [?f ?y ?x] =>
-                     replace (f y x) with (f x y) by solve_commutative_replace
-                   | _ => rewrite has_word_range_mod_small
-                       by (eapply has_range_loosen;
-                           [apply has_range_interp_scalar; extract_ok_scalar|];
-                           assumption)
-                   | _ => rewrite interp_cast_noop by (cbn [has_range fst snd] in *; split; lia)
-                   | _ => rewrite interp_cast2_noop by (cbn [has_range fst snd] in *; split; lia)
-                   | _ => reflexivity
-                 end.
-      Qed.
-
-      Lemma of_straightline_correct {t} (e : expr t) :
-        ok_expr e ->
-        @interp interp_cast _ (of_straightline dummy_arrow consts e)
-        = Straightline.expr.interp (interp_ident:=@ident.interp) (interp_cast:=interp_cast) e.
-      Proof.
-        induction 1; cbn [of_straightline]; intros;
-          repeat match goal with
-                 | _ => progress cbn [Straightline.expr.interp]
-                 | _ => erewrite of_straightline_ident_correct
-                     by (cbv [range_ok is_tighter_than_bool_range_type];
-                         eauto using in_word_range_word_range;
-                         try apply andb_true_iff; auto)
-                 | _ => rewrite interp_cast_noop by eauto using has_range_loosen, ident_interp_has_range
-                 | _ => rewrite interp_cast2_noop by eauto using has_range_loosen, ident_interp_has_range
-                 | H : forall y, has_range _ y -> interp _ = _ |- _ => rewrite H by eauto using has_range_loosen, ident_interp_has_range
-                 | _ => reflexivity
-        end.
-      Qed.
-    End proofs.
-
-   Section no_interp_cast.
-      Context (dummy_arrow : forall s d, type.interp (s -> d)%ctype) (consts : list Z)
-              (consts_ok : forall x, In x consts -> 0 <= x <= wordmax - 1).
-
-      Local Arguments interp _ {_} _.
-      Local Arguments interp_scalar _ {_} _.
-
-      Local Ltac tighter_than_to_le :=
-        repeat match goal with
-               | _ => progress (cbv [is_tighter_than_bool] in * )
-               | _ => rewrite andb_true_iff in *
-               | H : _ /\ _ |- _ => destruct H
-               end; Z.ltb_to_lt.
-
-      Lemma replace_interp_cast_scalar {t} (x : scalar t) interp_cast interp_cast'
-        (interp_cast_correct : forall r x, lower r <= x <= upper r -> interp_cast r x = x)
-        (interp_cast'_correct : forall r x, lower r <= x <= upper r -> interp_cast' r x = x) :
-        ok_scalar x ->
-        interp_scalar interp_cast x = interp_scalar interp_cast' x.
-      Proof.
-        induction 1; cbn [interp_scalar Straightline.expr.interp_scalar];
-          repeat match goal with
-                 | _ => progress (cbv [has_range interp_cast2] in * )
-                 | _ => progress tighter_than_to_le
-                 | H : ok_scalar _ |- _ => apply (has_range_interp_scalar (interp_cast_correct:=interp_cast_correct)) in H
-                 | _ => rewrite <-IHok_scalar
-                 | _ => rewrite interp_cast_correct by omega
-                 | _ => rewrite interp_cast'_correct by omega
-                 | _ => congruence
-                 end.
-      Qed.
-
-      Lemma replace_interp_cast {t} (e : expr t) interp_cast interp_cast'
-        (interp_cast_correct : forall r x, lower r <= x <= upper r -> interp_cast r x = x)
-        (interp_cast'_correct : forall r x, lower r <= x <= upper r -> interp_cast' r x = x) :
-        ok_expr consts e ->
-        interp interp_cast (of_straightline dummy_arrow consts e) =
-        interp interp_cast' (of_straightline dummy_arrow consts e).
-      Proof.
-        induction 1; intros; cbn [of_straightline interp].
-        { apply replace_interp_cast_scalar; auto. }
-        { erewrite !of_straightline_ident_correct by (eauto; cbv [range_ok]; apply in_word_range_word_range).
-          rewrite replace_interp_cast_scalar with (interp_cast'0:=interp_cast') by auto.
-          eauto using ident_interp_has_range. }
-        { erewrite !of_straightline_ident_correct by
-              (eauto; try solve [cbv [range_ok]; split; auto using in_word_range_word_range];
-               cbv [is_tighter_than_bool_range_type]; apply andb_true_iff; split; auto).
-          rewrite replace_interp_cast_scalar with (interp_cast'0:=interp_cast') by auto.
-          eauto using ident_interp_has_range. }
-      Qed.
-    End no_interp_cast.
-*)
-  End with_wordmax.
-(*
-  Definition of_Expr {s d} (log2wordmax : Z) (consts : list Z) (e : Expr (s -> d))
-             (var : type -> Type) (x : var s) dummy_arrow : @Straightline.expr.expr var ident d :=
-    @of_straightline log2wordmax var dummy_arrow consts _ (Straightline.of_Expr e var x dummy_arrow).
-*)
-  Definition interp_cast_mod w r x := if (lower r =? 0)
-                                      then if (upper r =? 2^w - 1)
-                                           then x mod (2^w)
-                                           else if (upper r =? 1)
-                                                then x mod 2
-                                                else x
-                                      else x.
-
-  Lemma interp_cast_mod_correct w r x :
-    lower r <= x <= upper r ->
-    interp_cast_mod w r x = x.
-  Proof.
-    cbv [interp_cast_mod].
-    intros; break_match; rewrite ?andb_true_iff in *; intuition; Z.ltb_to_lt;
-      apply Z.mod_small; omega.
-  Qed.
-(*
-  Lemma of_Expr_correct {s d} (log2wordmax : Z) (consts : list Z) (e : Expr (s -> d))
-        (e' : (type.interp s -> Uncurried.expr.expr d))
-        (x : type.interp s) dummy_arrow :
-    e type.interp = Abs e' ->
-    1 < log2wordmax ->
-    log2wordmax mod 2 = 0 ->
-    Straightline.expr.ok_expr (e' x) ->
-    (forall x0 : Z, In x0 consts -> 0 <= x0 <= 2 ^ log2wordmax - 1) ->
-    ok_expr log2wordmax consts
-            (of_uncurried (dummy_arrow:=dummy_arrow) (depth (fun _ : type => unit) (fun _ : type => tt) (e _)) (e' x)) ->
-    (depth type.interp (@DefaultValue.type.default) (e' x) <= depth (fun _ : type => unit) (fun _ : type => tt) (e _))%nat ->
-    @interp log2wordmax (interp_cast_mod log2wordmax) _ (of_Expr log2wordmax consts e type.interp x dummy_arrow) = @Uncurried.expr.interp _ (@ident.interp) _ (e type.interp) x.
-  Proof.
-    intro He'; intros; cbv [of_Expr Straightline.of_Expr].
-    rewrite He'; cbn [invert_Abs expr.interp].
-    assert (forall r z, lower r <= z <= upper r -> ident.cast ident.cast_outside_of_range r z = z) as interp_cast_correct.
-    { cbv [ident.cast]; intros; break_match; rewrite ?andb_true_iff, ?andb_false_iff in *; intuition; Z.ltb_to_lt; omega. }
-    erewrite replace_interp_cast with (interp_cast':=ident.cast ident.cast_outside_of_range) by auto using interp_cast_mod_correct.
-    rewrite of_straightline_correct by auto.
-    erewrite Straightline.expr.of_uncurried_correct by eassumption.
-    reflexivity.
-  Qed.
-*)
-  Notation LetInAppIdentZ S D r eidc x f
-    := (expr.LetIn
-          (A:=type.base (base.type.type_base base.type.Z))
-          (B:=type.base D)
-          (expr.App
-             (s:=type.base (base.type.type_base base.type.Z))
-             (d:=type.base (base.type.type_base base.type.Z))
-             (expr.Ident (ident.Z_cast r))
-             (expr.App
-                (s:=type.base S)
-                (d:=type.base (base.type.type_base base.type.Z))
-                eidc
-                x))
-          f).
-  Notation LetInAppIdentZZ S D r eidc x f
-    := (expr.LetIn
-          (A:=type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)))
-          (B:=type.base D)
-          (expr.App
-             (s:=type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)))
-             (d:=type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)))
-             (expr.Ident (ident.Z_cast2 r))
-             (expr.App
-                (s:=type.base S)
-                (d:=type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)))
-                eidc
-                x))
-          f).
-  Module Notations.
-    Import PrintingNotations.
-    (*Import Straightline.expr.*)
-
-    Local Open Scope expr_scope.
-    Local Notation "'tZ'" := (base.type.type_base base.type.Z).
-    Notation "'RegZero'" := (expr.Ident (ident.Literal 0)).
-    Notation "$ x" := (#(ident.Z_cast uint256) @ (#ident.fst @ (#(ident.Z_cast2 (uint256,bool)%core) @ (expr.Var x)))) (at level 10, format "$ x").
-    Notation "$ x" := (#(ident.Z_cast uint128) @ (#ident.fst @ (#(ident.Z_cast2 (uint128,bool)%core) @ (expr.Var x)))) (at level 10, format "$ x").
-    Notation "$ x ₁" := (#(ident.Z_cast uint256) @ (#ident.fst @ (expr.Var x))) (at level 10, format "$ x ₁").
-    Notation "$ x ₂" := (#(ident.Z_cast uint256) @ (#ident.snd @ (expr.Var x))) (at level 10, format "$ x ₂").
-    Notation "$ x" := (#(ident.Z_cast uint256) @ (expr.Var x)) (at level 10, format "$ x").
-    Notation "$ x" := (#(ident.Z_cast uint128) @ (expr.Var x)) (at level 10, format "$ x").
-    Notation "$ x" := (#(ident.Z_cast bool) @ (expr.Var x)) (at level 10, format "$ x").
-    Notation "carry{ $ x }" := (#(ident.Z_cast bool) @ (#ident.snd @ (#(ident.Z_cast2 (uint256, bool)%core) @ (expr.Var x))))
-                                 (at level 10, format "carry{ $ x }").
-    Notation "Lower{ x }" := (#(ident.Z_cast uint128) @ (#(ident.Z_land 340282366920938463463374607431768211455) @ x))
-                               (at level 10, format "Lower{ x }").
-    Notation "f @( y , x1 , x2 ); g "
-      := (LetInAppIdentZZ _ _ (uint256, bool)%core f (x1, x2) (fun y => g))
-           (at level 10, g at level 200, format "f @( y ,  x1 ,  x2 ); '//' g ").
-    Notation "f @( y , x1 , x2 , x3 ); g "
-      := (LetInAppIdentZZ _ _ (uint256, bool)%core f (#ident.pair @ (#ident.pair @ x1 @ x2) @ x3) (fun y => g))
-           (at level 10, g at level 200, format "f @( y ,  x1 ,  x2 ,  x3 ); '//' g ").
-    Notation "f @( y , x1 , x2 , x3 ); '#128' g "
-      := (LetInAppIdentZZ _ _ (uint128, bool)%core f (#ident.pair @ (#ident.pair @ x1 @ x2) @ x3) (fun y => g))
-           (at level 10, g at level 200, format "f @( y ,  x1 ,  x2 ,  x3 );  '#128' '//' g ").
-    Notation "f @( y , x1 , x2 ); g "
-      := (LetInAppIdentZ _ _ uint256 f (#ident.pair @ x1 @ x2) (fun y => g))
-           (at level 10, g at level 200, format "f @( y ,  x1 ,  x2 ); '//' g ").
-    Notation "f @( y , x1 , x2 , x3 ); g "
-      := (LetInAppIdentZ _ _ uint256 f (#ident.pair @ (#ident.pair @ x1 x2) x3) (fun y => g))
-           (at level 10, g at level 200, format "f @( y ,  x1 ,  x2 ,  x3 ); '//' g ").
-    (* special cases for when the ident constructor takes a constant argument *)
-    Notation "add@( y , x1 , x2 , n ); g"
-      := (LetInAppIdentZZ _ _ (uint256, bool) (#(ident.fancy_add 256 n)) (#ident.pair @ x1 x2) (fun y => g))
-           (at level 10, g at level 200, format "add@( y ,  x1 ,  x2 ,  n ); '//' g").
-    Notation "addc@( y , x1 , x2 , x3 , n ); g"
-      := (LetInAppIdentZZ _ _ (uint256, bool) (#(ident.fancy_addc 256 n)) (#ident.pair @ (#ident.pair @ x1 x2) x3) (fun y => g))
-           (at level 10, g at level 200, format "addc@( y ,  x1 ,  x2 ,  x3 ,  n ); '//' g").
-    Notation "addc@( y , x1 , x2 , x3 , n ); '#128' g"
-      := (LetInAppIdentZZ _ _ (uint128, bool) (#(ident.fancy_addc 256 n)) (#ident.pair @ (#ident.pair @ x1 x2) x3) (fun y => g))
-           (at level 10, g at level 200, format "addc@( y ,  x1 ,  x2 ,  x3 ,  n );  '#128' '//' g").
-    Notation "sub@( y , x1 , x2 , n ); g"
-      := (LetInAppIdentZZ _ _ (uint256, bool) (#(ident.fancy_sub 256 n)) (#ident.pair @ x1 x2) (fun y => g))
-           (at level 10, g at level 200, format "sub@( y ,  x1 ,  x2 ,  n ); '//' g").
-    Notation "subb@( y , x1 , x2 , x3 , n ); g"
-      := (LetInAppIdentZZ _ _ (uint256, bool) (#(ident.fancy_subb 256 n)) (#ident.pair @ (#ident.pair @ x1 x2) x3) (fun y => g))
-           (at level 10, g at level 200, format "subb@( y ,  x1 ,  x2 ,  x3 ,  n ); '//' g").
-    Notation "rshi@( y , x1 , x2 , n ); g"
-      := (LetInAppIdentZ _ _ _ (#(ident.fancy_rshi 256 n)) (#ident.pair @ x1 x2) (fun y => g))
-           (at level 10, g at level 200, format "rshi@( y ,  x1 ,  x2 , n ); '//' g ").
-    (*Notation "'ret' $ x" := (Scalar (expr.Var x)) (at level 10, format "'ret'  $ x").*)
-    Notation "( x , y )" := (#ident.pair @ x @ y) (at level 10, left associativity).
-  End Notations.
-(*
-  Module Tactics.
-    Ltac ok_expr_step' :=
-      match goal with
-      | _ => assumption
-      | |- _ <= _ <= _ \/ @eq zrange _ _ =>
-        right; lazy; try split; congruence
-      | |- _ <= _ <= _ \/ @eq zrange _ _ =>
-        left; lazy; try split; congruence
-      | |- context [PreFancy.ok_ident] => constructor
-      | |- context [PreFancy.ok_scalar] => constructor; try omega
-      | |- context [PreFancy.is_halved] => eapply PreFancy.is_halved_constant; [lazy; reflexivity | ]
-      | |- context [PreFancy.is_halved] => constructor
-      | |- context [PreFancy.in_word_range] => lazy; reflexivity
-      | |- context [PreFancy.in_flag_range] => lazy; reflexivity
-      | |- context [PreFancy.get_range] =>
-        cbn [PreFancy.get_range lower upper fst snd ZRange.map]
-      | x : type.interp (type.prod _ _) |- _ => destruct x
-      | |- (_ <=? _)%zrange = true =>
-        match goal with
-        | |- context [PreFancy.get_range_var] =>
-          cbv [is_tighter_than_bool PreFancy.has_range fst snd upper lower] in *; cbn;
-          apply andb_true_iff; split; apply Z.leb_le
-        | _ => lazy
-        end; omega || reflexivity
-      | |- @eq zrange _ _ => lazy; reflexivity
-      | |- _ <= _ => omega
-      | |- _ <= _ <= _ => omega
-      end; intros.
-
-    Ltac ok_expr_step :=
-      match goal with
-      | |- context [PreFancy.ok_expr] => constructor; cbn [fst snd]; repeat ok_expr_step'
-      end; intros; cbn [Nat.max].
-  End Tactics.
- *)
-  Notation interp w := (@expr.interp base.type ident.ident base.interp (@ident.gen_interp (PreFancy.interp_cast_mod w))).
-  Notation Interp w := (@expr.Interp base.type ident.ident base.interp (@ident.gen_interp (PreFancy.interp_cast_mod w))).
-End PreFancy.
- *)
-
 Module Fancy.
 
   Module CC.
@@ -3299,85 +2095,6 @@ Module ProdEquiv.
     end.
 End ProdEquiv.
 
-(* TODO : delete
-(* Lemmas to help prove that a fancy and prefancy expression have the
-same meaning -- should be replaced eventually with a proof of fancy
-passes in general. *)
-
-Module Fancy_PreFancy_Equiv.
-  Import LanguageWf.Compilers.
-  Import ZRange.Operations.
-  Import Fancy.Registers.
-
-  Lemma interp_cast_mod_eq w u x: 1 <= 2^w -> u = 2^w - 1 -> ident.cast (PreFancy.interp_cast_mod w) r[0 ~> u] x = x mod 2^w.
-  Proof.
-    cbv [PreFancy.interp_cast_mod]; intros.
-    rewrite ident.cast_out_of_bounds_simple_0; cbn [lower upper]; subst;
-      rewrite ?Z.eqb_refl; intros.
-    all: Z.rewrite_mod_small; Z.div_mod_to_quot_rem; auto with zarith.
-  Qed.
-  Lemma interp_cast_mod_flag w x: ident.cast (PreFancy.interp_cast_mod w) r[0 ~> 1] x = x mod 2.
-  Proof.
-    cbv [PreFancy.interp_cast_mod].
-    rewrite ident.cast_out_of_bounds_simple_0_mod; cbn [lower upper]; subst;
-      rewrite ?Z.eqb_refl; intros.
-    all: break_match; Bool.split_andb; Z.ltb_to_lt; Z.rewrite_mod_small; subst; try omega.
-    replace (2^w) with 2 by omega.
-    Z.rewrite_mod_small; reflexivity.
-  Qed.
-
-  Lemma interp_equivZ {s} w u (Hw : 1 <= 2^w) (Hu : u = 2^w-1) i rd regs e cc ctx idc args f :
-    (Fancy.spec i (Tuple.map ctx regs) cc
-     = ident.gen_interp (PreFancy.interp_cast_mod w) (t:=type.arrow _ base.type.Z) idc (PreFancy.interp w args)) ->
-    ( let r := Fancy.spec i (Tuple.map ctx regs) cc in
-      Fancy.interp reg_eqb (2 ^ w) Fancy.cc_spec e
-                 (Fancy.CC.update (Fancy.writes_conditions i) r Fancy.cc_spec cc)
-                 (fun n : register => if reg_eqb n rd then r mod 2 ^ w else ctx n) =
-    @PreFancy.interp w base.type.Z (f (r mod 2 ^ w))) ->
-    Fancy.interp reg_eqb (2^w) Fancy.cc_spec (Fancy.Instr i rd regs e) cc ctx
-    = @PreFancy.interp w base.type.Z
-                      (@PreFancy.LetInAppIdentZ s _ (r[0~>2^w-1])%zrange (#idc) args f).
-  Proof.
-    cbv zeta; intros spec_eq next_eq.
-    cbn [Fancy.interp PreFancy.interp].
-    cbv [Let_In].
-    rewrite next_eq.
-    cbn in *.
-    rewrite <-spec_eq.
-    rewrite interp_cast_mod_eq by omega.
-    reflexivity.
-  Qed.
-
-  Lemma interp_equivZZ {s} w (Hw : 2 < 2 ^ w) u (Hu : u = 2^w - 1) i rd regs e cc ctx idc args f :
-    ((Fancy.spec i (Tuple.map ctx regs) cc) mod 2 ^ w
-     = fst (ident.gen_interp (PreFancy.interp_cast_mod w) (t:=type.arrow _ (base.type.Z*base.type.Z)) idc (PreFancy.interp w args))) ->
-    ((if Fancy.cc_spec Fancy.CC.C(Fancy.spec i (Tuple.map ctx regs) cc) then 1 else 0)
-     = snd (ident.gen_interp (PreFancy.interp_cast_mod w) (t:=type.arrow _ (base.type.Z*base.type.Z)) idc (PreFancy.interp w args)) mod 2) ->
-    ( let r := Fancy.spec i (Tuple.map ctx regs) cc in
-      Fancy.interp reg_eqb (2 ^ w) Fancy.cc_spec e
-                 (Fancy.CC.update (Fancy.writes_conditions i) r Fancy.cc_spec cc)
-                 (fun n : register => if reg_eqb n rd then r mod 2 ^ w else ctx n) =
-     @PreFancy.interp w base.type.Z
-                     (f (r mod 2 ^ w, if (Fancy.cc_spec Fancy.CC.C r) then 1 else 0))) ->
-    Fancy.interp reg_eqb (2^w) Fancy.cc_spec (Fancy.Instr i rd regs e) cc ctx
-    = @PreFancy.interp w base.type.Z
-                      (@PreFancy.LetInAppIdentZZ s _ (r[0~>u], r[0~>1])%zrange (#idc) args f).
-  Proof.
-    cbv zeta; intros spec_eq1 spec_eq2 next_eq.
-    cbn [Fancy.interp PreFancy.interp].
-    cbv [Let_In].
-    cbn [ident.gen_interp]; Prod.eta_expand.
-    rewrite next_eq.
-    rewrite interp_cast_mod_eq by omega.
-    rewrite interp_cast_mod_flag by omega.
-    cbn -[Fancy.cc_spec] in *.
-    rewrite <-spec_eq1, <-spec_eq2.
-    rewrite Z.mod_mod by omega.
-    reflexivity.
-  Qed.
-End Fancy_PreFancy_Equiv.
-*)
-
 Module Barrett256.
   Import LanguageWf.Compilers.