Add dummy version of IdWithAlt to compilers

Currently, it doesn't do anything special

8 files changed, 32 insertions, 0 deletions

diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v
index a1775011d..8da303f4b 100644
--- a/src/Compilers/Z/ArithmeticSimplifier.v
+++ b/src/Compilers/Z/ArithmeticSimplifier.v
@@ -332,6 +332,7 @@ Section language.
          | Lor _ _ _ as opc
          | OpConst _ _ as opc
          | Opp _ _ as opc
+         | IdWithAlt _ _ _ as opc
          | Zselect _ _ _ _ as opc
          | AddWithCarry _ _ _ _ as opc
          | AddWithGetCarry _ _ _ _ _ _ as opc
diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v
index 882cbde3a..c574d3fb1 100644
--- a/src/Compilers/Z/Bounds/Interpretation.v
+++ b/src/Compilers/Z/Bounds/Interpretation.v
@@ -150,6 +150,10 @@ Module Import Bounds.
          {| lower := Z.min lr1 lr2 ; upper := Z.max ur1 ur2 |}.
     Definition cmovle (x y r1 r2 : t) : t
       := truncation_bounds (cmovle' r1 r2).
+
+    (** TODO(jgross): swap to other bounds here *)
+    Definition id_with_alt (x y : t) : t
+      := truncation_bounds x.
   End with_bitwidth.
   Section with_bitwidth2.
     Context (bit_width1 bit_width2 : option Z)
@@ -203,6 +207,7 @@ Module Import Bounds.
        | Land _ _ T => fun xy => land (bit_width_of_base_type T) (fst xy) (snd xy)
        | Lor _ _ T => fun xy => lor (bit_width_of_base_type T) (fst xy) (snd xy)
        | Opp _ T => fun x => opp (bit_width_of_base_type T) x
+       | IdWithAlt _ _ T => fun xy => id_with_alt (bit_width_of_base_type T) (fst xy) (snd xy)
        | Zselect _ _ _ T => fun cxy => let '(c, x, y) := eta3 cxy in zselect (bit_width_of_base_type T) c x y
        | AddWithCarry _ _ _ T => fun cxy => let '(c, x, y) := eta3 cxy in add_with_carry (bit_width_of_base_type T) c x y
        | AddWithGetCarry carry_boundary_bit_width _ _ _ T1 T2
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
index 68cc13d98..169c59d96 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
@@ -390,6 +390,7 @@ Proof.
                  | progress simpl in *
                  | progress split_min_max
                  | omega ]. }
+  { split; assumption. }
   { destruct_head Bounds.t; cbv [Bounds.zselect' Z.zselect].
     break_innermost_match; split_min_max; omega. }
   { apply (@monotone_eight_corners true true true _ _ _); split; auto. }
diff --git a/src/Compilers/Z/CommonSubexpressionElimination.v b/src/Compilers/Z/CommonSubexpressionElimination.v
index d545d9b47..e1f506c15 100644
--- a/src/Compilers/Z/CommonSubexpressionElimination.v
+++ b/src/Compilers/Z/CommonSubexpressionElimination.v
@@ -20,6 +20,7 @@ Inductive symbolic_op :=
 | SLand
 | SLor
 | SOpp
+| SIdWithAlt
 | SZselect
 | SAddWithCarry
 | SAddWithGetCarry (bitwidth : Z)
@@ -50,6 +51,8 @@ Definition symbolic_op_leb (x y : symbolic_op) : bool
      | _, SLor => false
      | SOpp, _ => true
      | _, SOpp => false
+     | SIdWithAlt, _ => true
+     | _, SIdWithAlt => false
      | SZselect, _ => true
      | _, SZselect => false
      | SAddWithCarry, _ => true
@@ -77,6 +80,7 @@ Definition symbolize_op s d (opc : op s d) : symbolic_op
      | Land T1 T2 Tout => SLand
      | Lor T1 T2 Tout => SLor
      | Opp T Tout => SOpp
+     | IdWithAlt T1 T2 Tout => SIdWithAlt
      | Zselect T1 T2 T3 Tout => SZselect
      | AddWithCarry T1 T2 T3 Tout => SAddWithCarry
      | AddWithGetCarry bitwidth T1 T2 T3 Tout1 Tout2 => SAddWithGetCarry bitwidth
@@ -95,6 +99,7 @@ Definition denote_symbolic_op s d (opc : symbolic_op) : option (op s d)
      | SLand, Prod (Tbase _) (Tbase _), Tbase _ => Some (Land _ _ _)
      | SLor, Prod (Tbase _) (Tbase _), Tbase _ => Some (Lor _ _ _)
      | SOpp, Tbase _, Tbase _ => Some (Opp _ _)
+     | SIdWithAlt, Prod (Tbase _) (Tbase _), Tbase _ => Some (IdWithAlt _ _ _)
      | SZselect, Prod (Prod (Tbase _) (Tbase _)) (Tbase _), Tbase _ => Some (Zselect _ _ _ _)
      | SAddWithCarry, Prod (Prod (Tbase _) (Tbase _)) (Tbase _), Tbase _ => Some (AddWithCarry _ _ _ _)
      | SAddWithGetCarry bitwidth, Prod (Prod (Tbase _) (Tbase _)) (Tbase _), Prod (Tbase _) (Tbase _)
@@ -111,6 +116,7 @@ Definition denote_symbolic_op s d (opc : symbolic_op) : option (op s d)
      | SLor, _, _
      | SOpp, _, _
      | SOpConst _, _, _
+     | SIdWithAlt, _, _
      | SZselect, _, _
      | SAddWithCarry, _, _
      | SAddWithGetCarry _, _, _
@@ -183,6 +189,7 @@ Definition normalize_symbolic_expr_mod_c (opc : symbolic_op) (args : symbolic_ex
      | SShl
      | SShr
      | SOpp
+     | SIdWithAlt
      | SZselect
      | SAddWithCarry
      | SAddWithGetCarry _
diff --git a/src/Compilers/Z/Reify.v b/src/Compilers/Z/Reify.v
index d3a86dde1..66a10a882 100644
--- a/src/Compilers/Z/Reify.v
+++ b/src/Compilers/Z/Reify.v
@@ -8,6 +8,7 @@ Require Import Crypto.Compilers.Reify.
 Require Import Crypto.Compilers.Eta.
 Require Import Crypto.Compilers.EtaInterp.
 Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.IdfunWithAlt.
 
 Ltac base_reify_op op op_head extra ::=
      lazymatch op_head with
@@ -23,6 +24,16 @@ Ltac base_reify_op op op_head extra ::=
      | @Z.zselect => constr:(reify_op op op_head 3 (Zselect TZ TZ TZ TZ))
      | @Z.add_with_carry => constr:(reify_op op op_head 3 (AddWithCarry TZ TZ TZ TZ))
      | @Z.sub_with_borrow => constr:(reify_op op op_head 3 (SubWithBorrow TZ TZ TZ TZ))
+     | @id_with_alt
+       => lazymatch extra with
+          | @id_with_alt Z _ _
+            => constr:(reify_op op op_head 2 (IdWithAlt TZ TZ TZ))
+          | @id_with_alt ?T _ _
+            => let c := uconstr:(@id_with_alt) in
+               let uZ := uconstr:(Z) in
+               fail 100 "Error: In Reflection.Z.base_reify_op: can only reify" c "applied to" uZ "not" T
+          | _ => fail 100 "Anomaly: In Reflection.Z.base_reify_op: head is id_with_alt but body is wrong:" extra
+          end
      | @Z.add_with_get_carry
        => lazymatch extra with
           | @Z.add_with_get_carry ?bit_width _ _ _
diff --git a/src/Compilers/Z/Syntax.v b/src/Compilers/Z/Syntax.v
index 5bfa1168c..53fb60c95 100644
--- a/src/Compilers/Z/Syntax.v
+++ b/src/Compilers/Z/Syntax.v
@@ -7,6 +7,7 @@ Require Import Crypto.Compilers.TypeUtil.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.IdfunWithAlt.
 Require Import Crypto.Util.NatUtil. (* for nat_beq for equality schemes *)
 Export Syntax.Notations.
 
@@ -27,6 +28,7 @@ Inductive op : flat_type base_type -> flat_type base_type -> Type :=
 | Land T1 T2 Tout : op (Tbase T1 * Tbase T2) (Tbase Tout)
 | Lor T1 T2 Tout : op (Tbase T1 * Tbase T2) (Tbase Tout)
 | Opp T Tout : op (Tbase T) (Tbase Tout)
+| IdWithAlt T1 T2 Tout : op (Tbase T1 * Tbase T2) (Tbase Tout)
 | Zselect T1 T2 T3 Tout : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout)
 | AddWithCarry T1 T2 T3 Tout : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout)
 | AddWithGetCarry (bitwidth : Z) T1 T2 T3 Tout1 Tout2 : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout1 * Tbase Tout2)
@@ -85,6 +87,7 @@ Definition Zinterp_op src dst (f : op src dst)
      | Lor _ _ _ => fun xy => Z.lor (fst xy) (snd xy)
      | Opp _ _ => fun x => Z.opp x
      | Zselect _ _ _ _ => fun ctf => let '(c, t, f) := eta3 ctf in Z.zselect c t f
+     | IdWithAlt _ _ _ => fun xy => id_with_alt (fst xy) (snd xy)
      | AddWithCarry _ _ _ _ => fun cxy => let '(c, x, y) := eta3 cxy in Z.add_with_carry c x y
      | AddWithGetCarry bitwidth _ _ _ _ _ => fun cxy => let '(c, x, y) := eta3 cxy in Z.add_with_get_carry bitwidth c x y
      | SubWithBorrow _ _ _ _ => fun cxy => let '(c, x, y) := eta3 cxy in Z.sub_with_borrow c x y
diff --git a/src/Compilers/Z/Syntax/Equality.v b/src/Compilers/Z/Syntax/Equality.v
index a9003d354..900121456 100644
--- a/src/Compilers/Z/Syntax/Equality.v
+++ b/src/Compilers/Z/Syntax/Equality.v
@@ -41,6 +41,8 @@ Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : bool
        => base_type_beq T1 T1' && base_type_beq T2 T2' && base_type_beq Tout Tout'
      | Opp Tin Tout, Opp Tin' Tout'
        => base_type_beq Tin Tin' && base_type_beq Tout Tout'
+     | IdWithAlt T1 T2 Tout, IdWithAlt T1' T2' Tout'
+       => base_type_beq T1 T1' && base_type_beq T2 T2' && base_type_beq Tout Tout'
      | Zselect T1 T2 T3 Tout, Zselect T1' T2' T3' Tout'
        => base_type_beq T1 T1' && base_type_beq T2 T2' && base_type_beq T3 T3' && base_type_beq Tout Tout'
      | AddWithCarry T1 T2 T3 Tout, AddWithCarry T1' T2' T3' Tout'
@@ -65,6 +67,7 @@ Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : bool
      | AddWithGetCarry _ _ _ _ _ _, _
      | SubWithBorrow _ _ _ _, _
      | SubWithGetBorrow _ _ _ _ _ _, _
+     | IdWithAlt _ _ _, _
        => false
      end%bool.
 
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v
index 2338efc48..d85226c98 100644
--- a/src/Compilers/Z/Syntax/Util.v
+++ b/src/Compilers/Z/Syntax/Util.v
@@ -68,6 +68,7 @@ Definition genericize_op {var' src dst} (opc : op src dst) {f}
      | Land _ _ _ => fun _ _ => Land _ _ _
      | Lor _ _ _ => fun _ _ => Lor _ _ _
      | Opp _ _ => fun _ _ => Opp _ _
+     | IdWithAlt _ _ _ => fun _ _ => IdWithAlt _ _ _
      | Zselect _ _ _ _ => fun _ _ => Zselect _ _ _ _
      | AddWithCarry _ _ _ _ => fun _ _ => AddWithCarry _ _ _ _
      | AddWithGetCarry bitwidth _ _ _ _ _ => fun _ _ => AddWithGetCarry bitwidth _ _ _ _ _