-
Notifications
You must be signed in to change notification settings - Fork 143
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Rework equivalence checker proofs to be based on remove #1173
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
JasonGross
force-pushed
the
more-asm
branch
2 times, most recently
from
March 26, 2022 01:16
d02927f
to
73f4614
Compare
This gets us almost all the way to the end of the proof. The primary remaining issue is the fact that the current spec constrains the registers holding the input and output values to not change across the proof. We need to rework how we're handling registers in the spec a bit. Ensure that we can prove goals not about register equality After chatting with Andres, the way to spec these is to add asm_in/out arguments that track only the arrays, and have these be the arguments that are passed to both inputs and outputs. Then both the inputs and the outputs can mandate that there exist asm_in/out arguments which also apply to scalar arguments, and spec the rest in terms of these. <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 193m13.13s | 4088604 ko | Total Time / Peak Mem | 188m56.89s | 4088744 ko || +4m16.24s || -140 ko | +2.26% | -0.00% -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 5m36.38s | 3054028 ko | Assembly/WithBedrock/Proofs.vo | 0m49.93s | 993444 ko || +4m46.44s || 2060584 ko | +573.70% | +207.41% 7m08.11s | 964412 ko | fiat-go/32/p384/p384.go | 7m58.16s | 1030768 ko || -0m50.04s || -66356 ko | -10.46% | -6.43% 0m57.88s | 1016920 ko | Assembly/EquivalenceProofs.vo | 0m42.19s | 981188 ko || +0m15.69s || 35732 ko | +37.18% | +3.64% 2m23.75s | 1632616 ko | Rewriter/Passes/NBE.vo | 2m36.85s | 1609124 ko || -0m13.09s || 23492 ko | -8.35% | +1.45% 7m53.10s | 1011348 ko | fiat-c/src/p384_32.c | 7m42.05s | 992272 ko || +0m11.05s || 19076 ko | +2.39% | +1.92% 4m21.97s | 1390132 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 4m14.80s | 1397512 ko || +0m07.17s || -7380 ko | +2.81% | -0.52% 7m48.63s | 965904 ko | fiat-java/src/FiatP384.java | 7m43.82s | 942416 ko || +0m04.81s || 23488 ko | +1.03% | +2.49% 7m48.03s | 1198288 ko | fiat-json/src/p384_32.json | 7m44.86s | 1131728 ko || +0m03.16s || 66560 ko | +0.68% | +5.88% 7m15.14s | 1125288 ko | fiat-zig/src/p384_32.zig | 7m19.06s | 992304 ko || -0m03.92s || 132984 ko | -0.89% | +13.40% 7m13.06s | 1084172 ko | fiat-bedrock2/src/p384_32.c | 7m10.54s | 990920 ko || +0m02.51s || 93252 ko | +0.58% | +9.41% 0m31.13s | 255036 ko | fiat-json/src/secp256k1_32.json | 0m28.86s | 207112 ko || +0m02.26s || 47924 ko | +7.86% | +23.13% 0m30.24s | 189332 ko | fiat-c/src/secp256k1_32.c | 0m27.51s | 208784 ko || +0m02.72s || -19452 ko | +9.92% | -9.31% 0m27.64s | 212428 ko | fiat-go/32/p256/p256.go | 0m29.89s | 227992 ko || -0m02.25s || -15564 ko | -7.52% | -6.82% 2m59.73s | 789248 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.vo | 3m01.25s | 788988 ko || -0m01.52s || 260 ko | -0.83% | +0.03% 2m01.32s | 1591124 ko | Rewriter/Passes/ToFancyWithCasts.vo | 2m02.47s | 1591164 ko || -0m01.15s || -40 ko | -0.93% | -0.00% 1m56.71s | 2413724 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 1m54.96s | 2413440 ko || +0m01.75s || 284 ko | +1.52% | +0.01% 1m33.39s | 1596664 ko | SlowPrimeSynthesisExamples.vo | 1m34.44s | 1596504 ko || -0m01.04s || 160 ko | -1.11% | +0.01% 0m30.56s | 217712 ko | fiat-java/src/FiatSecp256K1.java | 0m31.86s | 199004 ko || -0m01.30s || 18708 ko | -4.08% | +9.40% 0m30.46s | 218356 ko | fiat-zig/src/secp256k1_32.zig | 0m31.60s | 222192 ko || -0m01.14s || -3836 ko | -3.60% | -1.72% 0m27.44s | 1233240 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m26.25s | 1155756 ko || +0m01.19s || 77484 ko | +4.53% | +6.70% 0m23.61s | 1736432 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m24.64s | 1732968 ko || -0m01.03s || 3464 ko | -4.18% | +0.19% 0m16.39s | 1887428 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs | 0m17.62s | 1889036 ko || -0m01.23s || -1608 ko | -6.98% | -0.08% 0m15.51s | 134808 ko | fiat-bedrock2/src/p224_32.c | 0m14.09s | 145772 ko || +0m01.41s || -10964 ko | +10.07% | -7.52% 7m49.67s | 1063652 ko | fiat-rust/src/p384_32.rs | 7m50.04s | 1081104 ko || -0m00.37s || -17452 ko | -0.07% | -1.61% 6m57.85s | 2075164 ko | Curves/Weierstrass/AffineProofs.vo | 6m58.31s | 2081684 ko || -0m00.45s || -6520 ko | -0.10% | -0.31% 4m14.13s | 4088604 ko | Curves/EdwardsMontgomery.vo | 4m14.55s | 4088744 ko || -0m00.42s || -140 ko | -0.16% | -0.00% 3m11.62s | 1778848 ko | Rewriter/Passes/ArithWithCasts.vo | 3m11.53s | 1778888 ko || +0m00.09s || -40 ko | +0.04% | -0.00% 2m56.32s | 1448332 ko | Curves/Weierstrass/Projective.vo | 2m56.51s | 1404040 ko || -0m00.18s || 44292 ko | -0.10% | +3.15% 2m47.02s | 1441796 ko | Curves/Montgomery/XZProofs.vo | 2m47.55s | 1447212 ko || -0m00.53s || -5416 ko | -0.31% | -0.37% 2m36.49s | 1231416 ko | Curves/Montgomery/AffineProofs.vo | 2m36.51s | 1231432 ko || -0m00.01s || -16 ko | -0.01% | -0.00% 2m31.48s | 1115940 ko | Fancy/Compiler.vo | 2m31.68s | 1119736 ko || -0m00.20s || -3796 ko | -0.13% | -0.33% 2m15.81s | 1030820 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.vo | 2m15.69s | 1030824 ko || +0m00.12s || -4 ko | +0.08% | -0.00% 2m08.08s | 1193704 ko | Rewriter/Rewriter/Wf.vo | 2m08.81s | 1193664 ko || -0m00.72s || 40 ko | -0.56% | +0.00% 2m01.88s | 2785816 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.vo | 2m01.94s | 2785760 ko || -0m00.06s || 56 ko | -0.04% | +0.00% 1m50.27s | 901316 ko | AbstractInterpretation/Wf.vo | 1m50.36s | 901316 ko || -0m00.08s || 0 ko | -0.08% | +0.00% 1m42.59s | 1346872 ko | Fancy/Barrett256.vo | 1m42.33s | 1346192 ko || +0m00.26s || 680 ko | +0.25% | +0.05% 1m41.07s | 1048152 ko | Bedrock/Field/Synthesis/Examples/X25519_64.vo | 1m40.24s | 1048008 ko || +0m00.82s || 144 ko | +0.82% | +0.01% 1m19.07s | 1208384 ko | Bedrock/End2End/X25519/Field25519.vo | 1m19.14s | 1208488 ko || -0m00.07s || -104 ko | -0.08% | -0.00% 1m18.08s | 745944 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/MMIO.vo | 1m18.29s | 745948 ko || -0m00.20s || -4 ko | -0.26% | -0.00% 1m17.05s | 435240 ko | Spec/Test/X25519.vo | 1m17.15s | 435276 ko || -0m00.10s || -36 ko | -0.12% | -0.00% 1m15.79s | 1046156 ko | UnsaturatedSolinasHeuristics/Tests.vo | 1m15.57s | 1046108 ko || +0m00.21s || 48 ko | +0.29% | +0.00% 1m14.11s | 1578696 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.vo | 1m14.23s | 1578676 ko || -0m00.12s || 20 ko | -0.16% | +0.00% 1m02.38s | 943344 ko | Curves/Weierstrass/Jacobian.vo | 1m02.25s | 943240 ko || +0m00.13s || 104 ko | +0.20% | +0.01% 1m02.31s | 1335652 ko | Bedrock/Field/Synthesis/Examples/p224_64.vo | 1m01.86s | 1335560 ko || +0m00.45s || 92 ko | +0.72% | +0.00% 1m01.62s | 729280 ko | Rewriter/Language/UnderLetsProofs.vo | 1m01.82s | 729232 ko || -0m00.20s || 48 ko | -0.32% | +0.00% 0m59.66s | 975008 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m59.89s | 974848 ko || -0m00.23s || 160 ko | -0.38% | +0.01% 0m59.30s | 1272772 ko | Bedrock/Field/Synthesis/Examples/p256_64.vo | 0m58.87s | 1272872 ko || +0m00.42s || -100 ko | +0.73% | -0.00% 0m56.82s | 635744 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/Spilling.vo | 0m56.75s | 635680 ko || +0m00.07s || 64 ko | +0.12% | +0.01% 0m56.70s | 843772 ko | AbstractInterpretation/ZRangeProofs.vo | 0m56.77s | 844460 ko || -0m00.07s || -688 ko | -0.12% | -0.08% 0m55.88s | 723056 ko | AbstractInterpretation/Proofs.vo | 0m55.73s | 723564 ko || +0m00.15s || -508 ko | +0.26% | -0.07% 0m54.99s | 2462412 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m55.10s | 2462596 ko || -0m00.10s || -184 ko | -0.19% | -0.00% 0m54.54s | 694904 ko | Rewriter/RulesProofs.vo | 0m54.82s | 694060 ko || -0m00.28s || 844 ko | -0.51% | +0.12% 0m53.28s | 1025948 ko | Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo | 0m53.14s | 1025904 ko || +0m00.14s || 44 ko | +0.26% | +0.00% 0m51.41s | 944972 ko | Rewriter/Rewriter/InterpProofs.vo | 0m51.37s | 944996 ko || +0m00.03s || -24 ko | +0.07% | -0.00% 0m50.18s | 1048308 ko | Rewriter/Passes/MultiRetSplit.vo | 0m50.19s | 1048504 ko || -0m00.00s || -196 ko | -0.01% | -0.01% 0m50.16s | 957260 ko | Assembly/WithBedrock/SymbolicProofs.vo | 0m50.48s | 957440 ko || -0m00.32s || -180 ko | -0.63% | -0.01% 0m49.16s | 937444 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.vo | 0m49.18s | 937380 ko || -0m00.02s || 64 ko | -0.04% | +0.00% 0m48.69s | 2145732 ko | ExtractionOCaml/word_by_word_montgomery | 0m49.34s | 2145532 ko || -0m00.65s || 200 ko | -1.31% | +0.00% 0m48.14s | 792992 ko | Rewriter/Rewriter/ProofsCommon.vo | 0m48.05s | 792968 ko || +0m00.09s || 24 ko | +0.18% | +0.00% 0m46.75s | 1112048 ko | Rewriter/Passes/Arith.vo | 0m46.77s | 1112112 ko || -0m00.02s || -64 ko | -0.04% | -0.00% 0m46.59s | 1076312 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo | 0m47.37s | 1076452 ko || -0m00.77s || -140 ko | -1.64% | -0.01% 0m44.87s | 577176 ko | Demo.vo | 0m44.94s | 577156 ko || -0m00.07s || 20 ko | -0.15% | +0.00% 0m43.85s | 1326816 ko | Fancy/Montgomery256.vo | 0m43.27s | 1324368 ko || +0m00.57s || 2448 ko | +1.34% | +0.18% 0m39.77s | 567524 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricSane.vo | 0m39.81s | 567312 ko || -0m00.03s || 212 ko | -0.10% | +0.03% 0m38.33s | 2347268 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m38.53s | 2359096 ko || -0m00.20s || -11828 ko | -0.51% | -0.50% 0m37.26s | 1862916 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m37.34s | 1862948 ko || -0m00.08s || -32 ko | -0.21% | -0.00% 0m36.90s | 2242368 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m37.12s | 2218472 ko || -0m00.21s || 23896 ko | -0.59% | +1.07% 0m35.20s | 1650584 ko | ExtractionOCaml/unsaturated_solinas | 0m35.59s | 1650372 ko || -0m00.39s || 212 ko | -1.09% | +0.01% 0m34.59s | 1072932 ko | Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo | 0m34.66s | 1073056 ko || -0m00.06s || -124 ko | -0.20% | -0.01% 0m33.72s | 1410252 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m33.93s | 1430984 ko || -0m00.21s || -20732 ko | -0.61% | -1.44% 0m33.62s | 1409276 ko | ExtractionOCaml/bedrock2_base_conversion | 0m33.56s | 1422496 ko || +0m00.05s || -13220 ko | +0.17% | -0.92% 0m33.14s | 228364 ko | fiat-bedrock2/src/secp256k1_32.c | 0m33.53s | 220936 ko || -0m00.39s || 7428 ko | -1.16% | +3.36% 0m32.08s | 225244 ko | fiat-bedrock2/src/p256_32.c | 0m32.30s | 222652 ko || -0m00.21s || 2592 ko | -0.68% | +1.16% 0m30.90s | 898584 ko | Rewriter/Passes/MulSplit.vo | 0m30.66s | 898356 ko || +0m00.23s || 228 ko | +0.78% | +0.02% 0m30.68s | 218588 ko | fiat-go/32/secp256k1/secp256k1.go | 0m30.84s | 217548 ko || -0m00.16s || 1040 ko | -0.51% | +0.47% 0m30.68s | 192712 ko | fiat-java/src/FiatP256.java | 0m30.97s | 218100 ko || -0m00.28s || -25388 ko | -0.93% | -11.64% 0m30.43s | 598344 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvLiterals.vo | 0m30.67s | 598168 ko || -0m00.24s || 176 ko | -0.78% | +0.02% 0m30.36s | 194132 ko | fiat-rust/src/secp256k1_32.rs | 0m30.14s | 217280 ko || +0m00.21s || -23148 ko | +0.72% | -10.65% 0m30.14s | 235172 ko | fiat-json/src/p256_32.json | 0m30.21s | 226308 ko || -0m00.07s || 8864 ko | -0.23% | +3.91% 0m29.95s | 215276 ko | fiat-zig/src/p256_32.zig | 0m30.20s | 215876 ko || -0m00.25s || -600 ko | -0.82% | -0.27% 0m29.65s | 528308 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeBound.vo | 0m29.48s | 528064 ko || +0m00.16s || 244 ko | +0.57% | +0.04% 0m29.58s | 1154380 ko | Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo | 0m29.30s | 1155644 ko || +0m00.27s || -1264 ko | +0.95% | -0.10% 0m29.55s | 1233348 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m30.09s | 1233332 ko || -0m00.53s || 16 ko | -1.79% | +0.00% 0m29.37s | 218388 ko | fiat-rust/src/p256_32.rs | 0m29.90s | 217936 ko || -0m00.52s || 452 ko | -1.77% | +0.20% 0m29.28s | 218320 ko | fiat-c/src/p256_32.c | 0m28.92s | 198000 ko || +0m00.35s || 20320 ko | +1.24% | +10.26% 0m29.26s | 916216 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo | 0m29.31s | 916064 ko || -0m00.04s || 152 ko | -0.17% | +0.01% 0m29.21s | 953928 ko | PushButtonSynthesis/BYInversionReificationCache.vo | 0m29.17s | 954144 ko || +0m00.03s || -216 ko | +0.13% | -0.02% 0m29.05s | 1234908 ko | ExtractionOCaml/base_conversion | 0m29.27s | 1233792 ko || -0m00.21s || 1116 ko | -0.75% | +0.09% 0m28.98s | 1233556 ko | ExtractionOCaml/saturated_solinas | 0m29.01s | 1235808 ko || -0m00.03s || -2252 ko | -0.10% | -0.18% 0m27.92s | 1085444 ko | Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo | 0m28.62s | 1086312 ko || -0m00.69s || -868 ko | -2.44% | -0.07% 0m27.61s | 879320 ko | Rewriter/Rewriter/Examples.vo | 0m27.71s | 879392 ko || -0m00.10s || -72 ko | -0.36% | -0.00% 0m27.34s | 914916 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m27.38s | 914916 ko || -0m00.03s || 0 ko | -0.14% | +0.00% 0m26.97s | 848176 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m26.76s | 848004 ko || +0m00.20s || 172 ko | +0.78% | +0.02% 0m25.98s | 679452 ko | Rewriter/Language/Wf.vo | 0m26.22s | 679228 ko || -0m00.23s || 224 ko | -0.91% | +0.03% 0m25.41s | 496364 ko | Arithmetic/Saturated.vo | 0m25.51s | 496112 ko || -0m00.10s || 252 ko | -0.39% | +0.05% 0m25.25s | 840144 ko | Rewriter/Rewriter/Examples/PrefixSums.vo | 0m25.20s | 840272 ko || +0m00.05s || -128 ko | +0.19% | -0.01% 0m24.79s | 161720 ko | fiat-bedrock2/src/p434_64.c | 0m24.45s | 160508 ko || +0m00.33s || 1212 ko | +1.39% | +0.75% 0m24.51s | 749724 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/RegRename.vo | 0m24.65s | 749784 ko || -0m00.13s || -60 ko | -0.56% | -0.00% 0m23.27s | 860088 ko | Bedrock/Field/Synthesis/Examples/LadderStep.vo | 0m23.08s | 860492 ko || +0m00.19s || -404 ko | +0.82% | -0.04% 0m23.23s | 154380 ko | fiat-go/64/p434/p434.go | 0m23.26s | 154688 ko || -0m00.03s || -308 ko | -0.12% | -0.19% 0m23.19s | 143704 ko | fiat-zig/src/p434_64.zig | 0m22.84s | 155548 ko || +0m00.35s || -11844 ko | +1.53% | -7.61% 0m23.09s | 171980 ko | fiat-json/src/p434_64.json | 0m23.13s | 166400 ko || -0m00.03s || 5580 ko | -0.17% | +3.35% 0m23.08s | 145104 ko | fiat-rust/src/p434_64.rs | 0m22.98s | 142824 ko || +0m00.09s || 2280 ko | +0.43% | +1.59% 0m22.89s | 783268 ko | Bedrock/Field/Translation/Proofs/Expr.vo | 0m22.63s | 783300 ko || +0m00.26s || -32 ko | +1.14% | -0.00% 0m22.71s | 1679396 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m23.11s | 1703648 ko || -0m00.39s || -24252 ko | -1.73% | -1.42% 0m22.55s | 138676 ko | fiat-c/src/p434_64.c | 0m22.27s | 149828 ko || +0m00.28s || -11152 ko | +1.25% | -7.44% 0m22.10s | 854936 ko | Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo | 0m22.06s | 855036 ko || +0m00.04s || -100 ko | +0.18% | -0.01% 0m20.73s | 807068 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m20.73s | 807072 ko || +0m00.00s || -4 ko | +0.00% | -0.00% 0m20.63s | 732620 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo | 0m19.83s | 732368 ko || +0m00.80s || 252 ko | +4.03% | +0.03% 0m20.05s | 1679792 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m20.21s | 1682344 ko || -0m00.16s || -2552 ko | -0.79% | -0.15% 0m19.53s | 1664260 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m20.39s | 1668252 ko || -0m00.85s || -3992 ko | -4.21% | -0.23% 0m18.75s | 1622948 ko | ExtractionOCaml/base_conversion.ml | 0m19.39s | 1607864 ko || -0m00.64s || 15084 ko | -3.30% | +0.93% 0m18.68s | 1594048 ko | ExtractionOCaml/saturated_solinas.ml | 0m18.92s | 1602896 ko || -0m00.24s || -8848 ko | -1.26% | -0.55% 0m18.60s | 1833352 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m18.69s | 1831936 ko || -0m00.08s || 1416 ko | -0.48% | +0.07% 0m18.32s | 808128 ko | Bedrock/Field/Synthesis/Examples/X1305_32.vo | 0m18.27s | 807988 ko || +0m00.05s || 140 ko | +0.27% | +0.01% 0m18.03s | 1114624 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m18.07s | 1114660 ko || -0m00.03s || -36 ko | -0.22% | -0.00% 0m17.19s | 580008 ko | Rewriter/Language/Inversion.vo | 0m17.26s | 579736 ko || -0m00.07s || 272 ko | -0.40% | +0.04% 0m17.07s | 831256 ko | Curves/Edwards/XYZT/Basic.vo | 0m17.09s | 831384 ko || -0m00.01s || -128 ko | -0.11% | -0.01% 0m17.06s | 907288 ko | StandaloneDebuggingExamples.vo | 0m17.07s | 907212 ko || -0m00.01s || 76 ko | -0.05% | +0.00% 0m17.03s | 1808088 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m17.43s | 1807948 ko || -0m00.39s || 140 ko | -2.29% | +0.00% 0m16.96s | 614488 ko | Util/ZUtil/ArithmeticShiftr.vo | 0m16.97s | 614396 ko || -0m00.00s || 92 ko | -0.05% | +0.01% 0m16.94s | 755036 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo | 0m16.70s | 754868 ko || +0m00.24s || 168 ko | +1.43% | +0.02% 0m16.91s | 1876404 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPreconditionProperties.vo | 0m17.01s | 1876420 ko || -0m00.10s || -16 ko | -0.58% | -0.00% 0m16.78s | 666748 ko | Assembly/Symbolic.vo | 0m16.81s | 666904 ko || -0m00.02s || -156 ko | -0.17% | -0.02% 0m16.55s | 531296 ko | Arithmetic/WordByWordMontgomery.vo | 0m16.62s | 531124 ko || -0m00.07s || 172 ko | -0.42% | +0.03% 0m16.17s | 796320 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m15.76s | 796180 ko || +0m00.41s || 140 ko | +2.60% | +0.01% 0m15.95s | 752088 ko | Language/IdentifiersGENERATED.vo | 0m15.88s | 752120 ko || +0m00.06s || -32 ko | +0.44% | -0.00% 0m15.68s | 486504 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/RunInstruction.vo | 0m15.71s | 486368 ko || -0m00.03s || 136 ko | -0.19% | +0.02% 0m15.65s | 779256 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m16.13s | 778948 ko || -0m00.47s || 308 ko | -2.97% | +0.03% 0m15.61s | 1810056 ko | ExtractionHaskell/word_by_word_montgomery.hs | 0m15.59s | 1818656 ko || +0m00.01s || -8600 ko | +0.12% | -0.47% 0m15.23s | 573772 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_SB.vo | 0m15.13s | 573784 ko || +0m00.09s || -12 ko | +0.66% | -0.00% 0m15.10s | 726436 ko | Curves/Edwards/AffineProofs.vo | 0m15.00s | 726160 ko || +0m00.09s || 276 ko | +0.66% | +0.03% 0m14.99s | 514772 ko | Arithmetic/BarrettReduction.vo | 0m14.94s | 514192 ko || +0m00.05s || 580 ko | +0.33% | +0.11% 0m14.66s | 785452 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m14.66s | 785424 ko || +0m00.00s || 28 ko | +0.00% | +0.00% 0m14.57s | 422128 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/TestGoals.vo | 0m14.80s | 422124 ko || -0m00.23s || 4 ko | -1.55% | +0.00% 0m14.49s | 460208 ko | Algebra/Field.vo | 0m14.49s | 460528 ko || +0m00.00s || -320 ko | +0.00% | -0.06% 0m14.48s | 512676 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_66.vo | 0m14.41s | 512792 ko || +0m00.07s || -116 ko | +0.48% | -0.02% 0m14.36s | 706744 ko | Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo | 0m14.37s | 706712 ko || -0m00.00s || 32 ko | -0.06% | +0.00% 0m14.19s | 562732 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA.vo | 0m14.11s | 562584 ko || +0m00.08s || 148 ko | +0.56% | +0.02% 0m13.95s | 480456 ko | Arithmetic/Core.vo | 0m14.02s | 480536 ko || -0m00.07s || -80 ko | -0.49% | -0.01% 0m13.76s | 594340 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI64.vo | 0m13.72s | 594392 ko || +0m00.03s || -52 ko | +0.29% | -0.00% 0m13.75s | 135240 ko | fiat-go/32/p224/p224.go | 0m13.74s | 129076 ko || +0m00.00s || 6164 ko | +0.07% | +4.77% 0m13.71s | 594428 ko | Language/IdentifiersGENERATEDProofs.vo | 0m13.62s | 594192 ko || +0m00.09s || 236 ko | +0.66% | +0.03% 0m13.70s | 138104 ko | fiat-zig/src/p224_32.zig | 0m13.00s | 138088 ko || +0m00.69s || 16 ko | +5.38% | +0.01% 0m13.56s | 584684 ko | Bedrock/Field/Common/Util.vo | 0m13.53s | 584784 ko || +0m00.03s || -100 ko | +0.22% | -0.01% 0m13.54s | 557484 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatImp.vo | 0m13.58s | 557628 ko || -0m00.04s || -144 ko | -0.29% | -0.02% 0m13.45s | 143240 ko | fiat-rust/src/p224_32.rs | 0m13.81s | 134244 ko || -0m00.36s || 8996 ko | -2.60% | +6.70% 0m13.43s | 132436 ko | fiat-c/src/p224_32.c | 0m13.09s | 141264 ko || +0m00.33s || -8828 ko | +2.59% | -6.24% 0m13.30s | 653748 ko | Bedrock/Group/AdditionChains.vo | 0m13.57s | 653968 ko || -0m00.26s || -220 ko | -1.98% | -0.03% 0m13.03s | 133060 ko | fiat-json/src/p224_32.json | 0m13.94s | 150044 ko || -0m00.91s || -16984 ko | -6.52% | -11.31% 0m12.95s | 146448 ko | fiat-java/src/FiatP224.java | 0m13.90s | 141984 ko || -0m00.95s || 4464 ko | -6.83% | +3.14% 0m12.90s | 647192 ko | Bedrock/Group/ScalarMult/LadderStep.vo | 0m12.97s | 647116 ko || -0m00.07s || 76 ko | -0.53% | +0.01% 0m12.63s | 540816 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA64.vo | 0m12.68s | 540600 ko || -0m00.04s || 216 ko | -0.39% | +0.03% 0m12.46s | 1446936 ko | ExtractionHaskell/unsaturated_solinas.hs | 0m12.27s | 1449476 ko || +0m00.19s || -2540 ko | +1.54% | -0.17% 0m12.41s | 105600 ko | fiat-bedrock2/src/p384_64.c | 0m12.21s | 109020 ko || +0m00.19s || -3420 ko | +1.63% | -3.13% 0m12.35s | 1512072 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs | 0m12.82s | 1511508 ko || -0m00.47s || 564 ko | -3.66% | +0.03% 0m12.12s | 478328 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.vo | 0m12.17s | 478424 ko || -0m00.05s || -96 ko | -0.41% | -0.02% 0m12.01s | 1083092 ko | Assembly/Parse/TestAsm.vo | 0m11.72s | 1083280 ko || +0m00.28s || -188 ko | +2.47% | -0.01% 0m11.85s | 704252 ko | Util/ZRange/LandLorBounds.vo | 0m11.94s | 710768 ko || -0m00.08s || -6516 ko | -0.75% | -0.91% 0m11.83s | 1444260 ko | ExtractionHaskell/bedrock2_base_conversion.hs | 0m11.15s | 1444976 ko || +0m00.67s || -716 ko | +6.09% | -0.04% 0m11.56s | 616532 ko | Rewriter/Demo.vo | 0m11.51s | 616680 ko || +0m00.05s || -148 ko | +0.43% | -0.02% 0m11.55s | 829672 ko | PushButtonSynthesis/SmallExamples.vo | 0m11.55s | 829764 ko || +0m00.00s || -92 ko | +0.00% | -0.01% 0m11.05s | 1449268 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs | 0m11.71s | 1447492 ko || -0m00.66s || 1776 ko | -5.63% | +0.12% 0m11.03s | 1326800 ko | ExtractionHaskell/saturated_solinas.hs | 0m11.03s | 1326804 ko || +0m00.00s || -4 ko | +0.00% | -0.00% 0m10.99s | 651332 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/SpillingMapGoals.vo | 0m10.85s | 651460 ko || +0m00.14s || -128 ko | +1.29% | -0.01% 0m10.97s | 1365584 ko | ExtractionHaskell/base_conversion.hs | 0m10.94s | 1332792 ko || +0m00.03s || 32792 ko | +0.27% | +2.46% 0m10.82s | 97544 ko | fiat-go/64/p384/p384.go | 0m10.92s | 97136 ko || -0m00.09s || 408 ko | -0.91% | +0.42% 0m10.77s | 101016 ko | fiat-json/src/p384_64.json | 0m10.65s | 111348 ko || +0m00.11s || -10332 ko | +1.12% | -9.27% 0m10.67s | 539820 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM.vo | 0m10.61s | 539860 ko || +0m00.06s || -40 ko | +0.56% | -0.00% 0m10.58s | 786952 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m10.49s | 786388 ko || +0m00.08s || 564 ko | +0.85% | +0.07% 0m10.56s | 97940 ko | fiat-zig/src/p384_64.zig | 0m10.44s | 97852 ko || +0m00.12s || 88 ko | +1.14% | +0.08% 0m10.52s | 96952 ko | fiat-c/src/p384_64.c | 0m09.90s | 102812 ko || +0m00.61s || -5860 ko | +6.26% | -5.69% 0m10.46s | 604532 ko | Bedrock/Field/Translation/Proofs/Flatten.vo | 0m10.54s | 604552 ko || -0m00.07s || -20 ko | -0.75% | -0.00% 0m10.38s | 473080 ko | Primitives/MxDHRepChange.vo | 0m10.29s | 473000 ko || +0m00.09s || 80 ko | +0.87% | +0.01% 0m10.30s | 582964 ko | Stringification/IR.vo | 0m10.28s | 583004 ko || +0m00.02s || -40 ko | +0.19% | -0.00% 0m10.21s | 504468 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/RegAlloc.vo | 0m10.25s | 504480 ko || -0m00.03s || -12 ko | -0.39% | -0.00% 0m10.12s | 505216 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_UJ.vo | 0m10.21s | 505368 ko || -0m00.09s || -152 ko | -0.88% | -0.03% 0m09.93s | 91068 ko | fiat-rust/src/p384_64.rs | 0m10.58s | 96060 ko || -0m00.65s || -4992 ko | -6.14% | -5.19% 0m09.83s | 447432 ko | Algebra/Ring.vo | 0m09.84s | 447508 ko || -0m00.00s || -76 ko | -0.10% | -0.01% 0m09.73s | 551904 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ToplevelLoop.vo | 0m09.76s | 551956 ko || -0m00.02s || -52 ko | -0.30% | -0.00% 0m09.32s | 637232 ko | Bedrock/Group/ScalarMult/CSwap.vo | 0m09.43s | 637200 ko || -0m00.10s || 32 ko | -1.16% | +0.00% 0m09.14s | 867948 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.vo | 0m09.15s | 867840 ko || -0m00.00s || 108 ko | -0.10% | +0.01% 0m08.83s | 105964 ko | fiat-json/src/p448_solinas_32.json | 0m08.72s | 104548 ko || +0m00.10s || 1416 ko | +1.26% | +1.35% 0m08.59s | 505520 ko | Rewriter/Language/IdentifiersLibraryProofs.vo | 0m08.48s | 505512 ko || +0m00.10s || 8 ko | +1.29% | +0.00% 0m08.37s | 44580 ko | fiat-zig/src/p448_solinas_32.zig | 0m08.35s | 47676 ko || +0m00.01s || -3096 ko | +0.23% | -6.49% 0m08.28s | 47976 ko | fiat-rust/src/p448_solinas_32.rs | 0m08.25s | 44228 ko || +0m00.02s || 3748 ko | +0.36% | +8.47% 0m08.25s | 48156 ko | fiat-c/src/p448_solinas_32.c | 0m07.87s | 44324 ko || +0m00.37s || 3832 ko | +4.82% | +8.64% 0m08.17s | 900220 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo | 0m08.19s | 900160 ko || -0m00.01s || 60 ko | -0.24% | +0.00% 0m08.09s | 679932 ko | PushButtonSynthesis/BaseConversion.vo | 0m08.04s | 679748 ko || +0m00.05s || 184 ko | +0.62% | +0.02% 0m08.05s | 594508 ko | Language/IdentifiersBasicGENERATED.vo | 0m08.01s | 594540 ko || +0m00.04s || -32 ko | +0.49% | -0.00% 0m07.84s | 782012 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.vo | 0m07.73s | 782044 ko || +0m00.10s || -32 ko | +1.42% | -0.00% 0m07.81s | 587180 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo | 0m07.74s | 587092 ko || +0m00.06s || 88 ko | +0.90% | +0.01% 0m07.51s | 696672 ko | Assembly/Syntax.vo | 0m07.48s | 696764 ko || +0m00.02s || -92 ko | +0.40% | -0.01% 0m07.32s | 458304 ko | Util/ZRange/CornersMonotoneBounds.vo | 0m07.34s | 458500 ko || -0m00.01s || -196 ko | -0.27% | -0.04% 0m07.16s | 466564 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_S.vo | 0m07.17s | 466384 ko || -0m00.00s || 180 ko | -0.13% | +0.03% 0m06.83s | 682160 ko | PushButtonSynthesis/Primitives.vo | 0m06.74s | 682212 ko || +0m00.08s || -52 ko | +1.33% | -0.00% 0m06.73s | 473952 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ExprImp.vo | 0m06.73s | 474124 ko || +0m00.00s || -172 ko | +0.00% | -0.03% 0m06.62s | 436720 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Minimal.vo | 0m06.69s | 436920 ko || -0m00.07s || -200 ko | -1.04% | -0.04% 0m06.57s | 461396 ko | Arithmetic/FancyMontgomeryReduction.vo | 0m06.48s | 461236 ko || +0m00.08s || 160 ko | +1.38% | +0.03% 0m06.38s | 600516 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m06.31s | 600460 ko || +0m00.07s || 56 ko | +1.10% | +0.00% 0m06.23s | 828944 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo | 0m06.10s | 829180 ko || +0m00.13s || -236 ko | +2.13% | -0.02% 0m06.21s | 456172 ko | Util/ListUtil.vo | 0m06.17s | 455860 ko || +0m00.04s || 312 ko | +0.64% | +0.06% 0m06.17s | 702500 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.vo | 0m06.22s | 702464 ko || -0m00.04s || 36 ko | -0.80% | +0.00% 0m06.11s | 564092 ko | Rewriter/Passes/NoSelect.vo | 0m06.22s | 564032 ko || -0m00.10s || 60 ko | -1.76% | +0.01% 0m06.08s | 455768 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_Fence.vo | 0m05.99s | 455596 ko || +0m00.08s || 172 ko | +1.50% | +0.03% 0m06.03s | 454952 ko | Rewriter/Util/ListUtil.vo | 0m06.09s | 454680 ko || -0m00.05s || 272 ko | -0.98% | +0.05% 0m06.02s | 455140 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R_atomic.vo | 0m06.07s | 455148 ko || -0m00.05s || -8 ko | -0.82% | -0.00% 0m05.87s | 478160 ko | Util/ZUtil/Modulo.vo | 0m05.87s | 477880 ko || +0m00.00s || 280 ko | +0.00% | +0.05% 0m05.70s | 671228 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.vo | 0m05.75s | 671024 ko || -0m00.04s || 204 ko | -0.86% | +0.03% 0m05.70s | 453928 ko | Util/MSets/Sum.vo | 0m05.80s | 453856 ko || -0m00.09s || 72 ko | -1.72% | +0.01% 0m05.65s | 480568 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/EmitsValid.vo | 0m05.55s | 480464 ko || +0m00.10s || 104 ko | +1.80% | +0.02% 0m05.62s | 663932 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.vo | 0m05.56s | 663864 ko || +0m00.06s || 68 ko | +1.07% | +0.01% 0m05.59s | 523872 ko | Fancy/Prod.vo | 0m05.55s | 523656 ko || +0m00.04s || 216 ko | +0.72% | +0.04% 0m05.46s | 628212 ko | BoundsPipeline.vo | 0m05.39s | 627912 ko || +0m00.07s || 300 ko | +1.29% | +0.04% 0m05.43s | 576296 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Properties.vo | 0m05.37s | 576076 ko || +0m00.05s || 220 ko | +1.11% | +0.03% 0m05.40s | 500184 ko | Arithmetic/BYInv.vo | 0m05.40s | 500496 ko || +0m00.00s || -312 ko | +0.00% | -0.06% 0m05.37s | 466732 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM64.vo | 0m05.34s | 466900 ko || +0m00.03s || -168 ko | +0.56% | -0.03% 0m05.30s | 724352 ko | Bedrock/Field/Synthesis/Examples/EncodeDecode.vo | 0m05.42s | 724516 ko || -0m00.12s || -164 ko | -2.21% | -0.02% 0m05.23s | 467376 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Loops.vo | 0m05.22s | 467476 ko || +0m00.01s || -100 ko | +0.19% | -0.02% 0m05.10s | 490588 ko | COperationSpecifications.vo | 0m05.08s | 490496 ko || +0m00.01s || 92 ko | +0.39% | +0.01% 0m04.96s | 430160 ko | Spec/Curve25519.vo | 0m04.96s | 430296 ko || +0m00.00s || -136 ko | +0.00% | -0.03% 0m04.93s | 459736 ko | Util/FsatzAutoLemmas.vo | 0m04.95s | 459640 ko || -0m00.02s || 96 ko | -0.40% | +0.02% 0m04.82s | 545324 ko | Language/InversionExtra.vo | 0m04.91s | 545332 ko || -0m00.08s || -8 ko | -1.83% | -0.00% 0m04.79s | 500796 ko | Curves/Edwards/Pre.vo | 0m04.85s | 500768 ko || -0m00.05s || 28 ko | -1.23% | +0.00% 0m04.61s | 671700 ko | PushButtonSynthesis/BarrettReduction.vo | 0m04.70s | 671660 ko || -0m00.08s || 40 ko | -1.91% | +0.00% 0m04.57s | 429152 ko | Arithmetic/MontgomeryReduction/Proofs.vo | 0m04.57s | 429128 ko || +0m00.00s || 24 ko | +0.00% | +0.00% 0m04.48s | 472764 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/LowerPipeline.vo | 0m04.50s | 472612 ko || -0m00.01s || 152 ko | -0.44% | +0.03% 0m04.33s | 458704 ko | Util/ZRange/BasicLemmas.vo | 0m04.38s | 458720 ko || -0m00.04s || -16 ko | -1.14% | -0.00% 0m04.28s | 441536 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R.vo | 0m04.23s | 441536 ko || +0m00.04s || 0 ko | +1.18% | +0.00% 0m04.26s | 547908 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRFile.vo | 0m04.26s | 547852 ko || +0m00.00s || 56 ko | +0.00% | +0.01% 0m04.19s | 441516 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_57.vo | 0m04.22s | 441528 ko || -0m00.02s || -12 ko | -0.71% | -0.00% 0m04.18s | 31108 ko | fiat-go/64/p521/p521.go | 0m03.76s | 31108 ko || +0m00.41s || 0 ko | +11.17% | +0.00% 0m04.17s | 468056 ko | Rewriter/Language/IdentifiersBasicLibrary.vo | 0m04.11s | 467792 ko || +0m00.05s || 264 ko | +1.45% | +0.05% 0m04.08s | 442436 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I.vo | 0m04.00s | 442248 ko || +0m00.08s || 188 ko | +2.00% | +0.04% 0m04.08s | 474804 ko | Algebra/Field_test.vo | 0m04.09s | 474804 ko || -0m00.00s || 0 ko | -0.24% | +0.00% 0m04.07s | 442312 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_FenceI.vo | 0m04.11s | 442244 ko || -0m00.04s || 68 ko | -0.97% | +0.01% 0m03.89s | 452624 ko | UnsaturatedSolinasHeuristics.vo | 0m03.87s | 452732 ko || +0m00.02s || -108 ko | +0.51% | -0.02% 0m03.89s | 43892 ko | fiat-bedrock2/src/p521_64.c | 0m03.49s | 40668 ko || +0m00.39s || 3224 ko | +11.46% | +7.92% 0m03.86s | 484156 ko | Curves/Montgomery/Affine.vo | 0m03.83s | 484128 ko || +0m00.02s || 28 ko | +0.78% | +0.00% 0m03.84s | 460308 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Core.vo | 0m03.84s | 460252 ko || +0m00.00s || 56 ko | +0.00% | +0.01% 0m03.79s | 559560 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.vo | 0m03.81s | 559600 ko || -0m00.02s || -40 ko | -0.52% | -0.00% 0m03.62s | 734040 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m03.69s | 733860 ko || -0m00.06s || 180 ko | -1.89% | +0.02% 0m03.57s | 446520 ko | Arithmetic/BarrettReduction/Generalized.vo | 0m03.54s | 446656 ko || +0m00.02s || -136 ko | +0.84% | -0.03% 0m03.55s | 411908 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SlowGoals.vo | 0m03.58s | 412004 ko || -0m00.03s || -96 ko | -0.83% | -0.02% 0m03.53s | 452752 ko | Arithmetic/UniformWeight.vo | 0m03.55s | 452712 ko || -0m00.02s || 40 ko | -0.56% | +0.00% 0m03.42s | 448052 ko | CastLemmas.vo | 0m03.49s | 448100 ko || -0m00.07s || -48 ko | -2.00% | -0.01% 0m03.38s | 422240 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/ident_of_string.vo | 0m03.38s | 422216 ko || +0m00.00s || 24 ko | +0.00% | +0.00% 0m03.35s | 711840 ko | Bedrock/Field/Synthesis/Examples/MulTwice.vo | 0m03.22s | 711944 ko || +0m00.12s || -104 ko | +4.03% | -0.01% 0m03.34s | 439820 ko | Util/ZUtil/LandLorShiftBounds.vo | 0m03.29s | 439684 ko || +0m00.04s || 136 ko | +1.51% | +0.03% 0m03.30s | 433500 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalNoMul.vo | 0m03.32s | 433436 ko || -0m00.02s || 64 ko | -0.60% | +0.01% 0m03.27s | 440028 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO.vo | 0m03.24s | 439920 ko || +0m00.02s || 108 ko | +0.92% | +0.02% 0m03.26s | 564952 ko | PushButtonSynthesis/BaseConversionReificationCache.vo | 0m03.23s | 564760 ko || +0m00.02s || 192 ko | +0.92% | +0.03% 0m03.26s | 27064 ko | fiat-zig/src/p521_64.zig | 0m02.91s | 26824 ko || +0m00.34s || 240 ko | +12.02% | +0.89% 0m03.23s | 392780 ko | Algebra/Group.vo | 0m03.23s | 392668 ko || +0m00.00s || 112 ko | +0.00% | +0.02% 0m03.23s | 443740 ko | Util/ZUtil/LandLorBounds.vo | 0m03.24s | 443512 ko || -0m00.01s || 228 ko | -0.30% | +0.05% 0m03.23s | 26944 ko | fiat-rust/src/p521_64.rs | 0m03.18s | 25740 ko || +0m00.04s || 1204 ko | +1.57% | +4.67% 0m03.20s | 432564 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_system.vo | 0m03.20s | 432792 ko || +0m00.00s || -228 ko | +0.00% | -0.05% 0m03.20s | 439772 ko | Arithmetic/BarrettReduction/HAC.vo | 0m03.26s | 439880 ko || -0m00.05s || -108 ko | -1.84% | -0.02% 0m03.19s | 598172 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo | 0m03.21s | 598220 ko || -0m00.02s || -48 ko | -0.62% | -0.00% 0m03.13s | 679816 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.15s | 679856 ko || -0m00.02s || -40 ko | -0.63% | -0.00% 0m03.11s | 653740 ko | Bedrock/Group/ScalarMult/ScalarMult.vo | 0m03.01s | 653740 ko || +0m00.10s || 0 ko | +3.32% | +0.00% 0m03.09s | 46548 ko | fiat-bedrock2/src/secp256k1_64.c | 0m03.04s | 41768 ko || +0m00.04s || 4780 ko | +1.64% | +11.44% 0m03.07s | 462952 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/Pipeline.vo | 0m03.02s | 462896 ko || +0m00.04s || 56 ko | +1.65% | +0.01% 0m03.04s | 38324 ko | fiat-json/src/p521_64.json | 0m03.33s | 38320 ko || -0m00.29s || 4 ko | -8.70% | +0.01% 0m02.99s | 464536 ko | MiscCompilerPassesProofs.vo | 0m03.02s | 464532 ko || -0m00.02s || 4 ko | -0.99% | +0.00% 0m02.99s | 514468 ko | Rewriter/Passes/Test.vo | 0m02.95s | 514388 ko || +0m00.04s || 80 ko | +1.35% | +0.01% 0m02.94s | 411368 ko | Coqprime/PrimalityTest/PocklingtonCertificat.vo | 0m02.94s | 411456 ko || +0m00.00s || -88 ko | +0.00% | -0.02% 0m02.93s | 532408 ko | Rewriter/Passes/AddAssocLeft.vo | 0m02.90s | 532476 ko || +0m00.03s || -68 ko | +1.03% | -0.01% 0m02.92s | 430468 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Properties.vo | 0m02.94s | 430764 ko || -0m00.02s || -296 ko | -0.68% | -0.06% 0m02.91s | 696072 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m02.90s | 696152 ko || +0m00.01s || -80 ko | +0.34% | -0.01% 0m02.89s | 606684 ko | Bedrock/Field/Interface/Compilation2.vo | 0m02.98s | 606636 ko || -0m00.08s || 48 ko | -3.02% | +0.00% 0m02.89s | 678700 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m02.90s | 678680 ko || -0m00.00s || 20 ko | -0.34% | +0.00% 0m02.87s | 25412 ko | fiat-c/src/p521_64.c | 0m03.17s | 25180 ko || -0m00.29s || 232 ko | -9.46% | +0.92% 0m02.77s | 426736 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_U.vo | 0m02.77s | 426508 ko || +0m00.00s || 228 ko | +0.00% | +0.05% 0m02.76s | 35212 ko | fiat-go/64/p448solinas/p448solinas.go | 0m02.77s | 33020 ko || -0m00.01s || 2192 ko | -0.36% | +6.63% 0m02.71s | 436380 ko | Arithmetic/Primitives.vo | 0m02.71s | 436244 ko || +0m00.00s || 136 ko | +0.00% | +0.03% 0m02.70s | 434284 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/List.vo | 0m02.64s | 434396 ko || +0m00.06s || -112 ko | +2.27% | -0.02% 0m02.70s | 43976 ko | fiat-bedrock2/src/p448_solinas_64.c | 0m02.68s | 43764 ko || +0m00.02s || 212 ko | +0.74% | +0.48% 0m02.69s | 41792 ko | fiat-go/64/secp256k1/secp256k1.go | 0m02.70s | 45244 ko || -0m00.01s || -3452 ko | -0.37% | -7.62% 0m02.64s | 52116 ko | fiat-json/src/secp256k1_64.json | 0m02.67s | 52444 ko || -0m00.02s || -328 ko | -1.12% | -0.62% 0m02.62s | 40232 ko | fiat-bedrock2/src/curve25519_32.c | 0m02.59s | 39884 ko || +0m00.03s || 348 ko | +1.15% | +0.87% 0m02.62s | 44520 ko | fiat-zig/src/secp256k1_64.zig | 0m02.61s | 42560 ko || +0m00.01s || 1960 ko | +0.38% | +4.60% 0m02.60s | 703184 ko | CLI.vo | 0m02.70s | 703008 ko || -0m00.10s || 176 ko | -3.70% | +0.02% 0m02.58s | 42084 ko | fiat-rust/src/secp256k1_64.rs | 0m02.54s | 44504 ko || +0m00.04s || -2420 ko | +1.57% | -5.43% 0m02.56s | 528432 ko | Bedrock/Field/Translation/Expr.vo | 0m02.54s | 528460 ko || +0m00.02s || -28 ko | +0.78% | -0.00% 0m02.55s | 422912 ko | Util/Bool/Reflect.vo | 0m02.54s | 422836 ko || +0m00.00s || 76 ko | +0.39% | +0.01% 0m02.54s | 42752 ko | fiat-c/src/secp256k1_64.c | 0m02.50s | 43268 ko || +0m00.04s || -516 ko | +1.60% | -1.19% 0m02.51s | 530012 ko | Rewriter/Passes/FlattenThunkedRects.vo | 0m02.45s | 530016 ko || +0m00.05s || -4 ko | +2.44% | -0.00% 0m02.51s | 423120 ko | Rewriter/Util/Bool/Reflect.vo | 0m02.50s | 423044 ko || +0m00.00s || 76 ko | +0.39% | +0.01% 0m02.51s | 421536 ko | Util/ZUtil/ZSimplify/Autogenerated.vo | 0m02.54s | 421548 ko || -0m00.03s || -12 ko | -1.18% | -0.00% 0m02.48s | 444144 ko | Util/MSets/Iso.vo | 0m02.50s | 444224 ko || -0m00.02s || -80 ko | -0.80% | -0.01% 0m02.45s | 432772 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/MulTrapHandler.vo | 0m02.42s | 432952 ko || +0m00.03s || -180 ko | +1.23% | -0.04% 0m02.41s | 463948 ko | Util/ZUtil/Morphisms.vo | 0m02.33s | 463972 ko || +0m00.08s || -24 ko | +3.43% | -0.00% 0m02.39s | 42920 ko | fiat-bedrock2/src/p224_64.c | 0m02.39s | 43876 ko || +0m00.00s || -956 ko | +0.00% | -2.17% 0m02.37s | 460120 ko | Spec/MontgomeryCurve.vo | 0m02.31s | 460076 ko || +0m00.06s || 44 ko | +2.59% | +0.00% 0m02.32s | 442392 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/SepAutoArray.vo | 0m02.33s | 442460 ko || -0m00.01s || -68 ko | -0.42% | -0.01% 0m02.30s | 45680 ko | fiat-bedrock2/src/p256_64.c | 0m02.24s | 44508 ko || +0m00.05s || 1172 ko | +2.67% | +2.63% 0m02.25s | 454636 ko | Arithmetic/Freeze.vo | 0m02.18s | 454636 ko || +0m00.06s || 0 ko | +3.21% | +0.00% 0m02.23s | 584688 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo | 0m02.28s | 584628 ko || -0m00.04s || 60 ko | -2.19% | +0.01% 0m02.23s | 427044 ko | Util/ZUtil/TwosComplement.vo | 0m02.19s | 427068 ko || +0m00.04s || -24 ko | +1.82% | …
It's just too slow, at least for now :-(
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This gets us almost all the way to the end of the proof.
The primary remaining issue is the fact that the current spec constrains
the registers holding the input and output values to not change across
the proof. We need to rework how we're handling registers in the spec a
bit.
After chatting with @andres-erbsen , the way to spec these is to add asm_in/out
arguments that track only the arrays, and have these be the arguments
that are passed to both inputs and outputs. Then both the inputs and
the outputs can mandate that there exist asm_in/out arguments which also
apply to scalar arguments, and spec the rest in terms of these.
Timing Diff