1 files changed, 74 insertions, 0 deletions
diff --git a/src/BoundedArithmetic/StripCF.v b/src/BoundedArithmetic/StripCF.v
new file mode 100644
index 000000000..f44b1b7f7
--- /dev/null
+++ b/src/BoundedArithmetic/StripCF.v
@@ -0,0 +1,74 @@
+(** * Strip CF for Interface for bounded arithmetic *)
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.BoundedArithmetic.Interface.
+
+Local Open Scope type_scope.
+Local Open Scope Z_scope.
+
+Section strip_CF.
+  Context (n : Z) (* bit-width of width of [W] *)
+          {W : Type} (* bounded type, [W] for word *)
+          (Wdecoder : decoder n W).
+  Local Notation imm := Z (only parsing). (* immediate (compile-time) argument *)
+
+  Global Instance shift_right_doubleword_immediate_strip_CF
+         {shrdf : shift_right_doubleword_immediate_with_CF W}
+    : shift_right_doubleword_immediate W
+    := { shrd x y z := snd (shrdf x y z) }.
+  Global Instance is_shift_right_doubleword_immediate_strip_CF
+         {shrdf : shift_right_doubleword_immediate_with_CF W}
+         {shift_right_doubleword_immediate_with_CF : is_shift_right_doubleword_immediate_with_CF shrdf}
+    : is_shift_right_doubleword_immediate shift_right_doubleword_immediate_strip_CF
+    := shift_right_doubleword_immediate_with_CF.
+
+  Global Instance shift_left_immediate_strip_CF
+         {shlf : shift_left_immediate_with_CF W}
+    : shift_left_immediate W
+    := { shl x y := snd (shlf x y) }.
+  Global Instance is_shift_left_immediate_strip_CF
+         {shlf : shift_left_immediate_with_CF W}
+         {shift_left_immediate_with_CF : is_shift_left_immediate_with_CF shlf}
+    : is_shift_left_immediate shift_left_immediate_strip_CF
+    := shift_left_immediate_with_CF.
+
+  Global Instance shift_right_immediate_strip_CF
+         {shrf : shift_right_immediate_with_CF W}
+    : shift_right_immediate W
+    := { shr x y := snd (shrf x y) }.
+  Global Instance is_shift_right_immediate_strip_CF
+         {shrf : shift_right_immediate_with_CF W}
+         {shift_right_immediate_with_CF : is_shift_right_immediate_with_CF shrf}
+    : is_shift_right_immediate shift_right_immediate_strip_CF
+    := shift_right_immediate_with_CF.
+
+  Global Instance bitwise_and_strip_CF
+         {andf : bitwise_and_with_CF W}
+    : bitwise_and W
+    := { and x y := snd (andf x y) }.
+  Global Instance is_bitwise_and_strip_CF
+         {andf : bitwise_and_with_CF W}
+         {bitwise_and_with_CF : is_bitwise_and_with_CF andf}
+    : is_bitwise_and bitwise_and_strip_CF
+    := { decode_bitwise_and := @decode_snd_bitwise_and_with_CF _ _ _ _ bitwise_and_with_CF }.
+
+  Global Instance bitwise_or_strip_CF
+         {orf : bitwise_or_with_CF W}
+    : bitwise_or W
+    := { or x y := snd (orf x y) }.
+  Global Instance is_bitwise_or_strip_CF
+         {orf : bitwise_or_with_CF W}
+         {bitwise_or_with_CF : is_bitwise_or_with_CF orf}
+    : is_bitwise_or bitwise_or_strip_CF
+    := { decode_bitwise_or := @decode_snd_bitwise_or_with_CF _ _ _ _ bitwise_or_with_CF }.
+
+  Global Instance multiply_double_strip_CF
+         {muldwf : multiply_double_with_CF W}
+    : multiply_double W
+    := { muldw x y := snd (muldwf x y) }.
+  Global Instance is_mul_double_strip_CF
+         {muldwf : multiply_double_with_CF W}
+         {multiply_double_with_CF : is_mul_double_with_CF muldwf}
+    : is_mul_double multiply_double_strip_CF
+    := { decode_fst_mul_double := @decode_fst_mul_double_with_CF _ _ _ _ multiply_double_with_CF;
+         decode_snd_mul_double := @decode_snd_mul_double_with_CF _ _ _ _ multiply_double_with_CF}.
+End strip_CF.