From 5d1a4189db37607ac9687d9f717f74814f19a041 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 13 Oct 2016 13:42:17 -0400 Subject: Add src/BoundedArithmetic/Eta.v --- src/BoundedArithmetic/Eta.v | 65 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 65 insertions(+) create mode 100644 src/BoundedArithmetic/Eta.v (limited to 'src') 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. -- cgit v1.2.3