diff options
Diffstat (limited to 'src/Experiments/Ed25519Extraction.v')
| -rw-r--r-- | src/Experiments/Ed25519Extraction.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Experiments/Ed25519Extraction.v b/src/Experiments/Ed25519Extraction.v index 47cf4f791..20a76f17f 100644 --- a/src/Experiments/Ed25519Extraction.v +++ b/src/Experiments/Ed25519Extraction.v @@ -292,4 +292,8 @@ Extraction "src/Experiments/Ed25519_noimports.hs" Ed25519.sign (* Ed25519.verify True *Ed25519 Prelude> eRepEnc ((sRepERepMul l eRepB) `erepAdd` eRepB) == eRepEnc eRepB True -*)
\ No newline at end of file +*) + +Import Crypto.Spec.MxDH. +Extraction Inline MxDH.ladderstep MxDH.montladder. +Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519.
\ No newline at end of file |