aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly/GF25519.v
diff options
context:
space:
mode:
authorGravatar Robert Sloan <varomodt@google.com>2016-10-25 11:47:06 -0700
committerGravatar Robert Sloan <varomodt@google.com>2016-10-25 11:47:06 -0700
commit85d1e50a35d7003db0c1b1b5e44df7bf5ad211db (patch)
tree7ee4fba02a40fec8f07d537a5ba6f63b86bc790f /src/Assembly/GF25519.v
parent6c29b39c2c0eafdd6f92e7b3d67c451b3c769af5 (diff)
Refactors to remove intermediate conversions in HLConversions
Diffstat (limited to 'src/Assembly/GF25519.v')
-rw-r--r--src/Assembly/GF25519.v5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v
index 2e6329f18..9a9215c4d 100644
--- a/src/Assembly/GF25519.v
+++ b/src/Assembly/GF25519.v
@@ -205,6 +205,11 @@ Module GF25519.
Module Opp := Pipeline OppExpr.
End GF25519.
+Set Printing All.
+Opaque eadd esub emul eshiftr eand toT fromT.
+Eval cbv iota beta delta in GF25519.Add.HL.progZ.
+Eval cbv iota beta delta in GF25519.Add.AST.progZ.
+
Extraction "GF25519Add" GF25519.Add.
Extraction "GF25519Sub" GF25519.Sub.
Extraction "GF25519Mul" GF25519.Mul.