diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-11-14 11:57:22 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-11-14 11:57:22 -0500 |
| commit | 08e4be46e6de3dbb596c8f31d37235489bcd6bc4 (patch) | |
| tree | adfd1234ed78723d7c5f8a43a6f63795c3cbeed8 /src/Experiments | |
| parent | 4cd3cf5521c2c2bf29ec8db127b1fbb59805d242 (diff) | |
extraction: inline field operations into group operations
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/Ed25519Extraction.v | 14 |
1 files changed, 9 insertions, 5 deletions
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 |