diff options
author | Robert Sloan <varomodt@google.com> | 2016-10-25 11:47:06 -0700 |
---|---|---|
committer | Robert Sloan <varomodt@google.com> | 2016-10-25 11:47:06 -0700 |
commit | 85d1e50a35d7003db0c1b1b5e44df7bf5ad211db (patch) | |
tree | 7ee4fba02a40fec8f07d537a5ba6f63b86bc790f /src/Assembly/GF25519.v | |
parent | 6c29b39c2c0eafdd6f92e7b3d67c451b3c769af5 (diff) |
Refactors to remove intermediate conversions in HLConversions
Diffstat (limited to 'src/Assembly/GF25519.v')
-rw-r--r-- | src/Assembly/GF25519.v | 5 |
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. |