Add src/BoundedArithmetic/Eta.v

1 files changed, 65 insertions, 0 deletions

diff --git a/src/BoundedArithmetic/Eta.v b/src/BoundedArithmetic/Eta.v
new file mode 100644
index 000000000..b68112e50
--- /dev/null
+++ b/src/BoundedArithmetic/Eta.v
@@ -0,0 +1,65 @@
+(** * Bounded arithmetic η expansion *)
+(** This is useful for allowing us to refold the projections. *)
+Require Import Crypto.BoundedArithmetic.Interface.
+
+Definition eta_decode {n W} (x : decoder n W) : decoder n W := {| decode := decode |}.
+Section InstructionGallery.
+  Context {n W} {Wdecoder : decoder n W}.
+  Definition eta_ldi (x : load_immediate W) := {| ldi := ldi |}.
+  Definition eta_shrd (x : shift_right_doubleword_immediate W) := {| shrd := shrd |}.
+  Definition eta_shrdf (x : shift_right_doubleword_immediate_with_CF W) := {| shrdf := shrdf |}.
+  Definition eta_shl (x : shift_left_immediate W) := {| shl := shl |}.
+  Definition eta_shlf (x : shift_left_immediate_with_CF W) := {| shlf := shlf |}.
+  Definition eta_shr (x : shift_right_immediate W) := {| shr := shr |}.
+  Definition eta_shrf (x : shift_right_immediate_with_CF W) := {| shrf := shrf |}.
+  Definition eta_sprl (x : spread_left_immediate W) := {| sprl := sprl |}.
+  Definition eta_mkl (x : mask_keep_low W) := {| mkl := mkl |}.
+  Definition eta_and (x : bitwise_and W) := {| and := and |}.
+  Definition eta_andf (x : bitwise_and_with_CF W) := {| andf := andf |}.
+  Definition eta_or (x : bitwise_or W) := {| or := or |}.
+  Definition eta_orf (x : bitwise_or_with_CF W) := {| orf := orf |}.
+  Definition eta_adc (x : add_with_carry W) := {| adc := adc |}.
+  Definition eta_subc (x : sub_with_carry W) := {| subc := subc |}.
+  Definition eta_mul (x : multiply W) := {| mul := mul |}.
+  Definition eta_mulhwll (x : multiply_low_low W) := {| mulhwll := mulhwll |}.
+  Definition eta_mulhwhl (x : multiply_high_low W) := {| mulhwhl := mulhwhl |}.
+  Definition eta_mulhwhh (x : multiply_high_high W) := {| mulhwhh := mulhwhh |}.
+  Definition eta_muldw (x : multiply_double W) := {| muldw := muldw |}.
+  Definition eta_muldwf (x : multiply_double_with_CF W) := {| muldwf := muldwf |}.
+  Definition eta_selc (x : select_conditional W) := {| selc := selc |}.
+  Definition eta_addm (x : add_modulo W) := {| addm := addm |}.
+End InstructionGallery.
+
+Module fancy_machine.
+  Import Interface.fancy_machine.
+  Definition eta_instructions {n} (x : fancy_machine.instructions n) : fancy_machine.instructions n
+    := {| W := W;
+          decode := eta_decode decode;
+          ldi := eta_ldi ldi;
+          shrd := eta_shrd shrd;
+          shl := eta_shl shl;
+          shr := eta_shr shr;
+          adc := eta_adc adc;
+          subc := eta_subc subc;
+          mulhwll := eta_mulhwll mulhwll;
+          mulhwhl := eta_mulhwhl mulhwhl;
+          mulhwhh := eta_mulhwhh mulhwhh;
+          selc := eta_selc selc;
+          addm := eta_addm addm |}.
+End fancy_machine.
+
+Module x86.
+  Import Interface.x86.
+  Definition eta_instructions {n} (x : x86.instructions n) : x86.instructions n
+    := {| W := W;
+          decode := eta_decode decode;
+          ldi := eta_ldi ldi;
+          shrdf := eta_shrdf shrdf;
+          shlf := eta_shlf shlf;
+          shrf := eta_shrf shrf;
+          adc := eta_adc adc;
+          subc := eta_subc subc;
+          muldwf := eta_muldwf muldwf;
+          selc := eta_selc selc;
+          orf := eta_orf orf |}.
+End x86.