From 778c1906711f68bed5760710712bb16eeb9c2365 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 13 Oct 2016 14:00:42 -0400 Subject: Eta-expand pairs in Eta.v --- src/BoundedArithmetic/Eta.v | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/src/BoundedArithmetic/Eta.v b/src/BoundedArithmetic/Eta.v index b48b8cff1..bc9b0e940 100644 --- a/src/BoundedArithmetic/Eta.v +++ b/src/BoundedArithmetic/Eta.v @@ -2,30 +2,33 @@ (** This is useful for allowing us to refold the projections. *) Require Import Crypto.BoundedArithmetic.Interface. +Local Notation eta x := (fst x, snd x). +Local Notation eta3 x := (fst x, eta (snd x)). + 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_shrdf (x : shift_right_doubleword_immediate_with_CF W) := {| shrdf a b c := eta (shrdf a b c) |}. Definition eta_shl (x : shift_left_immediate W) := {| shl := shl |}. - Definition eta_shlf (x : shift_left_immediate_with_CF W) := {| shlf := shlf |}. + Definition eta_shlf (x : shift_left_immediate_with_CF W) := {| shlf a b := eta (shlf a b) |}. 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_shrf (x : shift_right_immediate_with_CF W) := {| shrf a b := eta (shrf a b) |}. + Definition eta_sprl (x : spread_left_immediate W) := {| sprl a b := eta (sprl a b) |}. 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_andf (x : bitwise_and_with_CF W) := {| andf a b := eta (andf a b) |}. 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_orf (x : bitwise_or_with_CF W) := {| orf a b := eta (orf a b) |}. + Definition eta_adc (x : add_with_carry W) := {| adc a b c := eta (adc a b c) |}. + Definition eta_subc (x : sub_with_carry W) := {| subc a b c := eta (subc a b c) |}. 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_muldw (x : multiply_double W) := {| muldw a b := eta (muldw a b) |}. + Definition eta_muldwf (x : multiply_double_with_CF W) := {| muldwf a b := eta3 (muldwf a b) |}. Definition eta_selc (x : select_conditional W) := {| selc := selc |}. Definition eta_addm (x : add_modulo W) := {| addm := addm |}. End InstructionGallery. -- cgit v1.2.3