https://github.com/mit-plv/fiat-crypto
Tip revision: 0b1ebe16c40ae1bb3a37ee4b09a88ac177df1dc7 authored by Jason Gross on 28 June 2021, 17:28:42 UTC
Fix perf.csv generation
Fix perf.csv generation
Tip revision: 0b1ebe1
Crypto.Fancy.Montgomery256.Prod.MontRed256.expected
= fun lo hi y t t0 scratch RegPInv : register =>
MUL128LL y lo RegPInv;
MUL128UL t lo RegPInv;
ADD 128 y y t;
MUL128LU t lo RegPInv;
ADD 128 y y t;
MUL128LL t y RegMod;
MUL128UU t0 y RegMod;
MUL128UL scratch y RegMod;
ADD 128 t t scratch;
ADDC (-128) t0 t0 scratch;
MUL128LU scratch y RegMod;
ADD 128 t t scratch;
ADDC (-128) t0 t0 scratch;
ADD 0 lo lo t;
ADDC 0 hi hi t0;
SELC y RegMod RegZero;
SUB 0 lo hi y;
ADDM lo lo RegZero RegMod;
Ret lo
: forall lo hi y t t0 scratch RegPInv : register, expr
