Skip to main content

Browse the archive

https://github.com/mit-plv/fiat-crypto
12 July 2022, 18:24:35 UTC
Revision 72fe0dddee5e6dceeab0b8a2e6a745abf5287d3e authored by Jason Gross on 15 July 2021, 00:27:45 UTC, committed by Jason Gross on 15 July 2021, 00:28:57 UTC 
make perf csv
 
```
make COQBIN="$HOME/.local64/coq/coq-8.11.1/bin/" SKIP_BEDROCK2=1 TIMED=1 --output-sync perf-csv
```
1 parent f020c4e
Raw File
Tip revision: 72fe0dddee5e6dceeab0b8a2e6a745abf5287d3e authored by Jason Gross on 15 July 2021, 00:27:45 UTC
make perf csv
Tip revision: 72fe0dd
Crypto.Fancy.Montgomery256.Prod.MontRed256.expected 
     = fun lo hi y t1 t2 scratch RegPInv : register =>
       MUL128LL y lo RegPInv;
       MUL128UL t1 lo RegPInv;
       ADD 128 y y t1;
       MUL128LU t1 lo RegPInv;
       ADD 128 y y t1;
       MUL128LL t1 y RegMod;
       MUL128UU t2 y RegMod;
       MUL128UL scratch y RegMod;
       ADD 128 t1 t1 scratch;
       ADDC (-128) t2 t2 scratch;
       MUL128LU scratch y RegMod;
       ADD 128 t1 t1 scratch;
       ADDC (-128) t2 t2 scratch;
       ADD 0 lo lo t1;
       ADDC 0 hi hi t2;
       SELC y RegMod RegZero;
       SUB 0 lo hi y;
       ADDM lo lo RegZero RegMod;
       Ret lo
     : register ->
       register ->
       register -> register -> register -> register -> register -> expr
back to top