diff options
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | src/Experiments/Ed25519Extraction.v | 14 |
2 files changed, 13 insertions, 7 deletions
@@ -91,16 +91,18 @@ src/Experiments/Ed25519_noimports.hs: src/Experiments/Ed25519Extraction.vo src/E src/Experiments/Ed25519.hs: src/Experiments/Ed25519_noimports.hs src/Experiments/Ed25519_imports.hs ( cd src/Experiments && \ - < Ed25519_noimports.hs \ + ( < Ed25519_noimports.hs \ sed "/import qualified Prelude/r Ed25519_imports.hs" | \ sed 's/ Ed25519_noimports / Ed25519 /g' \ + && echo -e '{-# INLINE mul1 #-} \n{-# INLINE add2 #-} \n{-# INLINE sub3 #-}' ) \ > Ed25519.hs ) src/Experiments/X25519.hs: src/Experiments/X25519_noimports.hs src/Experiments/Ed25519_imports.hs ( cd src/Experiments && \ - < X25519_noimports.hs \ + ( < X25519_noimports.hs \ sed "/import qualified Prelude/r Ed25519_imports.hs" | \ sed 's/ X25519_noimports / X25519 /g' \ + && echo -e '{-# INLINE mul #-} \n{-# INLINE sub0 #-} \n{-# INLINE add #-}' ) \ > X25519.hs ) src/Experiments/Ed25519.o: src/Experiments/Ed25519.hs diff --git a/src/Experiments/Ed25519Extraction.v b/src/Experiments/Ed25519Extraction.v index 5b12abad9..b498a8c4e 100644 --- a/src/Experiments/Ed25519Extraction.v +++ b/src/Experiments/Ed25519Extraction.v @@ -256,11 +256,11 @@ Extract Inlined Constant Word64.mul => "(Prelude.*)". Extract Inlined Constant Word64.sub => "(Prelude.-)". Extract Inlined Constant Word64.land => "(Data.Bits..&.)". Extract Inlined Constant Word64.lor => "(Data.Bits..|.)". -Extract Constant Word64.neg => "(\_ w -> Prelude.negate w)". (* FIXME: reification: drop arg1 *) -Extract Constant Word64.shr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))". -Extract Constant Word64.shl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))". -Extract Constant Word64.cmovle => "(\x y r1 r2 -> if x Prelude.<= y then r1 else r2)". -Extract Constant Word64.cmovne => "(\x y r1 r2 -> if x Prelude.== y then r1 else r2)". +Extract Inlined Constant Word64.neg => "(\_ w -> Prelude.negate w)". (* FIXME: reification: drop arg1 *) +Extract Inlined Constant Word64.shr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))". +Extract Inlined Constant Word64.shl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))". +Extract Inlined Constant Word64.cmovle => "(\x y r1 r2 -> if x Prelude.<= y then r1 else r2)". +Extract Inlined Constant Word64.cmovne => "(\x y r1 r2 -> if x Prelude.== y then r1 else r2)". (* inlining, primarily to reduce polymorphism *) Extraction Inline dec_eq_Z dec_eq_N dec_eq_sig_hprop. @@ -275,6 +275,10 @@ Extraction Inline GF25519BoundedCommon.proj_word GF25519BoundedCommon.Build_boun Extraction Inline GF25519BoundedCommon.app_wire_digits GF25519BoundedCommon.wire_digit_bounds_exp. Extraction Inline Crypto.Util.HList.mapt' Crypto.Util.HList.mapt Crypto.Util.Tuple.map. +Extraction Inline GF25519BoundedCommon.exist_fe25519 GF25519BoundedCommon.exist_fe25519W GF25519BoundedCommon.proj1_fe25519W. +Extraction Inline Crypto.Specific.GF25519Bounded.mulW Crypto.Specific.GF25519Bounded.addW Crypto.Specific.GF25519Bounded.subW. +(*done-at-haskell-level: Extraction Inline Crypto.Specific.GF25519Bounded.mul Crypto.Specific.GF25519Bounded.add Crypto.Specific.GF25519Bounded.sub Crypto.Specific.GF25519Bounded.inv Crypto.Specific.GF25519Bounded.sqrt. *) + Extraction Implicit Ed25519.SHA512 [ 1 ]. Extract Constant Ed25519.SHA512 => "let { b2i b = case b of { Prelude.True -> 1 ; Prelude.False -> 0 } } in |