Skip to main content

Browse the archive

https://github.com/mit-plv/fiat-crypto
12 July 2022, 18:24:35 UTC
sort by:
Revision Author Date Message Commit Date
cfaa85b jadep 07 September 2020, 00:27:24 UTC Bignum_to_bytes proved; representation working 07 September 2020, 00:27:24 UTC
3b9beb9 jadep 06 September 2020, 23:50:09 UTC WIP: Bignum_from_bytes proved 06 September 2020, 23:50:09 UTC
85cc562 jadep 06 September 2020, 22:22:23 UTC WIP: scalarmult correctness proven, field representation instantiation not fixed 06 September 2020, 22:22:23 UTC
f2184b7 jadep 23 August 2020, 22:28:30 UTC WIP 23 August 2020, 22:28:30 UTC
3c09ecd jadep 23 August 2020, 15:53:07 UTC add from_bytes to field 23 August 2020, 15:53:07 UTC
3e0f8b5 jadep 20 August 2020, 19:46:18 UTC use stackalloc in scmul implementation 23 August 2020, 13:36:28 UTC
18d4e66 jadep 20 August 2020, 15:34:58 UTC add TODO 21 August 2020, 16:24:47 UTC
def7104 jadep 17 August 2020, 16:12:57 UTC start proving implementation 21 August 2020, 16:24:47 UTC
2b89ccc jadep 17 August 2020, 16:02:26 UTC prove montgomery group parameters are valid 21 August 2020, 16:24:47 UTC
86420ca jadep 17 August 2020, 15:50:08 UTC add #bits to ScalarFieldParameters and define Montgomery point representation 21 August 2020, 16:24:47 UTC
748eeda jadep 17 August 2020, 14:10:36 UTC prove equivalence of Curves version of montladder and rupicola-translated version 21 August 2020, 16:24:45 UTC
11775fb jadep 17 August 2020, 12:40:48 UTC use number of scalar bits as montladder bound 21 August 2020, 16:20:47 UTC
d87ec31 jadep 21 August 2020, 10:43:39 UTC bump rupicola version 21 August 2020, 16:17:11 UTC
630a2e3 jadep 20 August 2020, 19:56:30 UTC use lib target for rupicola for faster builds 21 August 2020, 16:17:11 UTC
e5b914e jadep 20 August 2020, 19:48:40 UTC bump rupicola version 21 August 2020, 16:17:11 UTC
93b5796 jadep 15 August 2020, 14:52:50 UTC update Specs/Group.v to match F-style scalar representation 20 August 2020, 08:23:42 UTC
8aa931d jadep 15 August 2020, 14:52:12 UTC minor tactic tweak 20 August 2020, 08:23:42 UTC
52b22f4 jadep 15 August 2020, 14:06:02 UTC remove fevals from postconditions 20 August 2020, 08:23:42 UTC
42be15f jadep 15 August 2020, 12:02:21 UTC switch scalar field to use F 20 August 2020, 08:23:42 UTC
5b23371 jadep 15 August 2020, 11:58:48 UTC change field specs to use F 20 August 2020, 08:23:42 UTC
b9974f0 Jason Gross 19 August 2020, 18:05:58 UTC Remove useless requires resulting in needless axioms The only remaining axioms we require are now the ones of the real numbers, transitively loaded by Nsatz 19 August 2020, 18:05:58 UTC
acc220f Jason Gross 19 August 2020, 15:59:28 UTC Update README.md 19 August 2020, 15:59:28 UTC
5bbdb0d jadep 17 August 2020, 13:47:59 UTC change Definition back to Instance to preserve notation 19 August 2020, 11:50:31 UTC
32dcffb jadep 17 August 2020, 08:53:34 UTC improve comments in spec parameter classes 19 August 2020, 11:50:31 UTC
bf19fee jadep 17 August 2020, 08:52:08 UTC change Instances to Definitions 19 August 2020, 11:50:31 UTC
9d50fde jadep 14 August 2020, 13:57:27 UTC fix missing argument 19 August 2020, 11:50:31 UTC
091d282 jadep 14 August 2020, 12:50:56 UTC create Bedrock/Field/Interface and put compilation lemmas there 19 August 2020, 11:50:31 UTC
eacf7df jadep 14 August 2020, 12:23:25 UTC renaming: bignum -> felem 19 August 2020, 11:50:31 UTC
cac93a8 jadep 14 August 2020, 11:52:27 UTC add Field/Representation.v and instantiate BignumRepresentation; remove outdated comments 19 August 2020, 11:50:31 UTC
d05c81c jadep 14 August 2020, 11:50:56 UTC add Specs/Group.v 19 August 2020, 11:50:31 UTC
d7a7244 jadep 11 August 2020, 10:38:05 UTC Copy over ECC content from rupicola 19 August 2020, 11:50:31 UTC
bab6168 Jason Gross 19 August 2020, 02:49:35 UTC Include bounds in the generated JSON As requested 19 August 2020, 02:49:35 UTC
081ac50 dderjoel 18 August 2020, 07:36:14 UTC added info on dependencies package Apparently, the package `ocamlfind` has been renamed to `ocaml-findlib` Added convenience cmd lines to install the required dependencies. (Checked package names in brew / pacman and apt package-lists) 19 August 2020, 00:46:20 UTC
3abdd27 Jason Gross 17 August 2020, 21:40:11 UTC Play some tricks to remove axioms from coqchk We provide dummy definitions locked inside opaque modules rather than using axioms for constants to be extracted as stateful primitives. Since all we care about with coqchk is that we cannot prove False, it does not really matter if the model we provide for these constants does not match their semantics. We only use them for interaction with the system in any case. 18 August 2020, 02:42:54 UTC
8b334e6 Jason Gross 17 August 2020, 21:45:56 UTC Remove the axiom in Curves/Edwards/AffineProofs 18 August 2020, 02:42:34 UTC
8e00fa7 Jason Gross 17 August 2020, 23:34:44 UTC Don't Require Psatz It brings in axioms that we don't want to depend on, c.f. https://github.com/mit-plv/fiat-crypto/issues/736 17 August 2020, 23:34:44 UTC
9428f47 Jason Gross 17 August 2020, 21:42:30 UTC Remove an Admitted that we didn't need to have 17 August 2020, 21:42:30 UTC
dc69e17 Jason Gross 12 August 2020, 16:38:39 UTC Add some documentation of the JSON format 17 August 2020, 20:53:42 UTC
65105b8 Jason Gross 12 August 2020, 02:04:08 UTC Add a JSON output format Note that we need to keep the individual lines of each function separate so as to not stack-overflow when joining strings before printing, because JSON has many, many more lines than most of the other languages. 17 August 2020, 20:53:42 UTC
4844fa0 Jason Gross 16 August 2020, 23:20:07 UTC Bump the rewriter to remove funext There were two insights that went into making it possible to remove functional extensionaliy. 1. The insight that went into 4d7999ebb66c1497222d024a1d9f9d0f1ecb2356: interp-relatedness implies equivalence. 2. Requiring `f x = v` in the `App`/`LetIn` case of `interp_related_gen` et al is essentially saying that, in order to prove `interp_related_gen`, we need to materialize an interpretation of the function part of applications. Since interpretation is in general highly non-trivial (for `rawexpr`s, `value`s, etc), we must weaken this condition. By instead only requiring `f x == v`, we only require being able to manifest *some* function which interprets to `v`, a much easier task. This weakening allows us to prove for each interpretation-relation `R` that `(exists e, R e v1 /\ R e v2) <-> v1 == v2`, i.e., that two interpreted values are equivalent iff there is some uninterpreted value which is related to both of them. Unfortunately this is not a full specification of interpretation-relatedness (we still need to say what it means for a particular uninterpreted value to be related to a particular interpreted value), and so we still end up doing a lot of work to prove various properties. I'm confused why synthesis of p384 x32 is a full minute faster in C and Rust but not any other language ... probably a glitch in timing? The changes in `Rewriter/Language/UnderLetsProofs` and `Rewriter/Rewriter/ProofsCommon` seem real, and the slight increases in the `Passes/` files also seem likely to be real, but almost everything else is probably mostly noise. <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 149m11.81s | 2370428 ko | Total Time / Peak Mem | 149m40.94s | 2369520 ko || -0m29.12s || 908 ko | -0.32% | +0.03% ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 6m47.98s | 996696 ko | fiat-c/src/p384_32.c | 7m47.01s | 996704 ko || -0m59.02s || -8 ko | -12.63% | -0.00% 6m46.71s | 996728 ko | fiat-rust/src/p384_32.rs | 7m45.38s | 996772 ko || -0m58.67s || -44 ko | -12.60% | -0.00% 1m14.86s | 867156 ko | Rewriter/Language/UnderLetsProofs | 0m46.79s | 774576 ko || +0m28.07s || 92580 ko | +59.99% | +11.95% 3m25.60s | 1443464 ko | Fancy/Compiler.vo | 3m17.64s | 1443264 ko || +0m07.96s || 200 ko | +4.02% | +0.01% 0m56.19s | 874216 ko | Rewriter/Rewriter/ProofsCommon | 0m49.05s | 867820 ko || +0m07.14s || 6396 ko | +14.55% | +0.73% 2m30.19s | 2285532 ko | Fancy/Barrett256.vo | 2m25.11s | 2285712 ko || +0m05.07s || -180 ko | +3.50% | -0.00% 7m24.25s | 1072480 ko | fiat-bedrock2/src/p384_32.c | 7m20.19s | 1072476 ko || +0m04.06s || 4 ko | +0.92% | +0.00% 3m14.52s | 1450412 ko | Rewriter/Passes/NBE.vo | 3m10.13s | 1444696 ko || +0m04.39s || 5716 ko | +2.30% | +0.39% 1m57.34s | 958504 ko | Rewriter/Rewriter/Wf | 1m52.52s | 955660 ko || +0m04.81s || 2844 ko | +4.28% | +0.29% 1m19.14s | 1071228 ko | Curves/Weierstrass/Jacobian.vo | 1m15.04s | 1070856 ko || +0m04.10s || 372 ko | +5.46% | +0.03% 7m46.25s | 1028476 ko | fiat-java/src/FiatP384.java | 7m43.03s | 1028592 ko || +0m03.22s || -116 ko | +0.69% | -0.01% 1m28.84s | 1910576 ko | Fancy/Montgomery256.vo | 1m25.52s | 1933348 ko || +0m03.32s || -22772 ko | +3.88% | -1.17% 1m12.42s | 1118960 ko | Rewriter/Passes/MultiRetSplit.vo | 1m09.27s | 1124872 ko || +0m03.15s || -5912 ko | +4.54% | -0.52% 0m29.51s | 929128 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m33.17s | 930700 ko || -0m03.66s || -1572 ko | -11.03% | -0.16% 0m24.94s | 216076 ko | fiat-rust/src/secp256k1_32.rs | 0m28.07s | 216112 ko || -0m03.12s || -36 ko | -11.15% | -0.01% 3m35.65s | 1608212 ko | Rewriter/Passes/ArithWithCasts.vo | 3m33.30s | 1608012 ko || +0m02.34s || 200 ko | +1.10% | +0.01% 1m42.39s | 580312 ko | Spec/Test/X25519.vo | 1m45.11s | 580516 ko || -0m02.71s || -204 ko | -2.58% | -0.03% 0m44.64s | 1594996 ko | ExtractionOCaml/word_by_word_montgomery | 0m42.57s | 1594880 ko || +0m02.07s || 116 ko | +4.86% | +0.00% 0m27.98s | 215924 ko | fiat-go/src/secp256k1_32.go | 0m24.99s | 216036 ko || +0m02.99s || -112 ko | +11.96% | -0.05% 0m24.69s | 644612 ko | Rewriter/Language/Wf | 0m22.54s | 633384 ko || +0m02.15s || 11228 ko | +9.53% | +1.77% 7m53.18s | 1066948 ko | fiat-go/src/p384_32.go | 7m54.71s | 1066864 ko || -0m01.52s || 84 ko | -0.32% | +0.00% 1m14.22s | 967412 ko | AbstractInterpretation/Proofs.vo | 1m12.40s | 967344 ko || +0m01.81s || 68 ko | +2.51% | +0.00% 1m04.06s | 942748 ko | Rewriter/Rewriter/InterpProofs | 1m02.79s | 956060 ko || +0m01.27s || -13312 ko | +2.02% | -1.39% 0m51.17s | 981596 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m52.57s | 1029132 ko || -0m01.39s || -47536 ko | -2.66% | -4.61% 0m41.74s | 927116 ko | Rewriter/Passes/MulSplit.vo | 0m40.69s | 921708 ko || +0m01.05s || 5408 ko | +2.58% | +0.58% 0m33.06s | 1251244 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m34.47s | 1251344 ko || -0m01.40s || -100 ko | -4.09% | -0.00% 0m30.60s | 1250952 ko | ExtractionOCaml/unsaturated_solinas | 0m32.19s | 1250820 ko || -0m01.58s || 132 ko | -4.93% | +0.01% 0m29.91s | 1054016 ko | ExtractionOCaml/base_conversion | 0m28.37s | 1053736 ko || +0m01.53s || 280 ko | +5.42% | +0.02% 0m29.78s | 1090076 ko | ExtractionOCaml/bedrock2_base_conversion | 0m30.91s | 1090208 ko || -0m01.12s || -132 ko | -3.65% | -0.01% 0m29.52s | 1941812 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m27.93s | 1955200 ko || +0m01.58s || -13388 ko | +5.69% | -0.68% 0m28.52s | 1053720 ko | ExtractionOCaml/saturated_solinas | 0m30.00s | 1053752 ko || -0m01.48s || -32 ko | -4.93% | -0.00% 0m24.76s | 820360 ko | Curves/Edwards/AffineProofs.vo | 0m22.86s | 820332 ko || +0m01.90s || 28 ko | +8.31% | +0.00% 0m16.29s | 137656 ko | fiat-go/src/p434_64.go | 0m14.34s | 137708 ko || +0m01.94s || -52 ko | +13.59% | -0.03% 0m15.74s | 130600 ko | fiat-c/src/p434_64.c | 0m13.85s | 130528 ko || +0m01.89s || 72 ko | +13.64% | +0.05% 0m12.18s | 130500 ko | fiat-go/src/p224_32.go | 0m10.97s | 130444 ko || +0m01.20s || 56 ko | +11.03% | +0.04% 0m12.08s | 118664 ko | fiat-bedrock2/src/p224_32.c | 0m13.41s | 118548 ko || -0m01.33s || 116 ko | -9.91% | +0.09% 9m00.53s | 2370428 ko | Curves/Weierstrass/AffineProofs.vo | 9m00.97s | 2369520 ko || -0m00.44s || 908 ko | -0.08% | +0.03% 4m25.11s | 2281892 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 4m25.91s | 2029560 ko || -0m00.80s || 252332 ko | -0.30% | +12.43% 3m55.52s | 2288204 ko | Curves/Montgomery/XZProofs.vo | 3m55.71s | 2288968 ko || -0m00.18s || -764 ko | -0.08% | -0.03% 3m42.64s | 1365004 ko | Curves/Weierstrass/Projective.vo | 3m43.33s | 1364812 ko || -0m00.68s || 192 ko | -0.30% | +0.01% 3m06.01s | 1246912 ko | Curves/Montgomery/AffineProofs.vo | 3m06.68s | 1247008 ko || -0m00.67s || -96 ko | -0.35% | -0.00% 2m33.72s | 1479492 ko | Rewriter/Passes/ToFancyWithCasts.vo | 2m33.11s | 1477876 ko || +0m00.60s || 1616 ko | +0.39% | +0.10% 2m33.20s | 1247780 ko | Bedrock/Field/Synthesis/Examples/X25519_64.vo | 2m32.72s | 1246024 ko || +0m00.47s || 1756 ko | +0.31% | +0.14% 2m17.93s | 960828 ko | AbstractInterpretation/Wf.vo | 2m18.00s | 960820 ko || -0m00.06s || 8 ko | -0.05% | +0.00% 1m52.89s | 1632656 ko | Bedrock/Field/Synthesis/Examples/p224_64.vo | 1m53.43s | 1632744 ko || -0m00.54s || -88 ko | -0.47% | -0.00% 1m49.72s | 1469608 ko | Bedrock/Field/Synthesis/Examples/p256_64.vo | 1m49.42s | 1469564 ko || +0m00.29s || 44 ko | +0.27% | +0.00% 1m27.77s | 1314596 ko | SlowPrimeSynthesisExamples.vo | 1m27.61s | 1314340 ko || +0m00.15s || 256 ko | +0.18% | +0.01% 1m20.55s | 1620180 ko | Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo | 1m20.74s | 1558860 ko || -0m00.18s || 61320 ko | -0.23% | +3.93% 1m16.59s | 1552908 ko | Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo | 1m16.60s | 1538380 ko || -0m00.00s || 14528 ko | -0.01% | +0.94% 1m16.47s | 984720 ko | UnsaturatedSolinasHeuristics/Tests.vo | 1m16.75s | 984760 ko || -0m00.28s || -40 ko | -0.36% | -0.00% 1m14.14s | 1131868 ko | AbstractInterpretation/ZRangeProofs.vo | 1m14.12s | 1124580 ko || +0m00.01s || 7288 ko | +0.02% | +0.64% 1m02.20s | 1194176 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo | 1m01.91s | 1184924 ko || +0m00.29s || 9252 ko | +0.46% | +0.78% 1m01.60s | 1049272 ko | Rewriter/RulesProofs.vo | 1m01.79s | 1048168 ko || -0m00.18s || 1104 ko | -0.30% | +0.10% 0m58.68s | 1067216 ko | Rewriter/Passes/Arith.vo | 0m58.42s | 1066656 ko || +0m00.25s || 560 ko | +0.44% | +0.05% 0m53.88s | 920492 ko | Demo.vo | 0m53.77s | 920360 ko || +0m00.10s || 132 ko | +0.20% | +0.01% 0m49.09s | 975332 ko | Bedrock/Field/Synthesis/Examples/LadderStep.vo | 0m49.12s | 976208 ko || -0m00.02s || -876 ko | -0.06% | -0.08% 0m48.95s | 1832580 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m48.41s | 1832688 ko || +0m00.54s || -108 ko | +1.11% | -0.00% 0m38.68s | 972092 ko | Rewriter/Rewriter/Examples/SieveOfEratosthenes | 0m38.28s | 888524 ko || +0m00.39s || 83568 ko | +1.04% | +9.40% 0m34.83s | 811224 ko | Rewriter/Rewriter/Examples | 0m34.63s | 811504 ko || +0m00.19s || -280 ko | +0.57% | -0.03% 0m34.62s | 784240 ko | Arithmetic/Saturated.vo | 0m34.55s | 783824 ko || +0m00.07s || 416 ko | +0.20% | +0.05% 0m34.35s | 996676 ko | Bedrock/Field/Synthesis/Examples/X1305_32.vo | 0m34.38s | 997184 ko || -0m00.03s || -508 ko | -0.08% | -0.05% 0m33.16s | 1053572 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m33.01s | 1053364 ko || +0m00.14s || 208 ko | +0.45% | +0.01% 0m32.51s | 171608 ko | fiat-bedrock2/src/secp256k1_32.c | 0m32.52s | 171536 ko || -0m00.01s || 72 ko | -0.03% | +0.04% 0m32.50s | 811088 ko | Rewriter/Rewriter/Examples/PrefixSums | 0m31.82s | 811164 ko || +0m00.67s || -76 ko | +2.13% | -0.00% 0m31.73s | 1090704 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m31.41s | 1090724 ko || +0m00.32s || -20 ko | +1.01% | -0.00% 0m30.32s | 217800 ko | fiat-bedrock2/src/p256_32.c | 0m30.02s | 217868 ko || +0m00.30s || -68 ko | +0.99% | -0.03% 0m29.91s | 1054604 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m29.57s | 1054468 ko || +0m00.33s || 136 ko | +1.14% | +0.01% 0m28.64s | 183780 ko | fiat-java/src/FiatSecp256K1.java | 0m28.30s | 183736 ko || +0m00.33s || 44 ko | +1.20% | +0.02% 0m28.21s | 216020 ko | fiat-java/src/FiatP256.java | 0m28.10s | 216160 ko || +0m00.10s || -140 ko | +0.39% | -0.06% 0m28.03s | 1873684 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m28.54s | 1828316 ko || -0m00.50s || 45368 ko | -1.78% | +2.48% 0m27.85s | 190592 ko | fiat-c/src/p256_32.c | 0m27.70s | 190536 ko || +0m00.15s || 56 ko | +0.54% | +0.02% 0m27.74s | 191240 ko | fiat-go/src/p256_32.go | 0m27.84s | 191280 ko || -0m00.10s || -40 ko | -0.35% | -0.02% 0m27.71s | 190480 ko | fiat-c/src/secp256k1_32.c | 0m27.78s | 190752 ko || -0m00.07s || -272 ko | -0.25% | -0.14% 0m25.10s | 193596 ko | fiat-rust/src/p256_32.rs | 0m24.83s | 193812 ko || +0m00.27s || -216 ko | +1.08% | -0.11% 0m24.31s | 881228 ko | Bedrock/Field/Common/Util.vo | 0m24.99s | 881912 ko || -0m00.67s || -684 ko | -2.72% | -0.07% 0m23.75s | 1107364 ko | Bedrock/Field/Translation/Proofs/Expr.vo | 0m23.72s | 1101928 ko || +0m00.03s || 5436 ko | +0.12% | +0.49% 0m22.54s | 871768 ko | Arithmetic/BarrettReduction.vo | 0m22.44s | 871808 ko || +0m00.09s || -40 ko | +0.44% | -0.00% 0m22.48s | 865944 ko | Arithmetic/WordByWordMontgomery.vo | 0m22.60s | 865972 ko || -0m00.12s || -28 ko | -0.53% | -0.00% 0m22.26s | 1065268 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m21.93s | 1063888 ko || +0m00.33s || 1380 ko | +1.50% | +0.12% 0m21.34s | 1540048 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m21.07s | 1508676 ko || +0m00.26s || 31372 ko | +1.28% | +2.07% 0m20.76s | 1647768 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m20.68s | 1542440 ko || +0m00.08s || 105328 ko | +0.38% | +6.82% 0m20.08s | 1040192 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo | 0m20.06s | 1035360 ko || +0m00.01s || 4832 ko | +0.09% | +0.46% 0m20.05s | 994728 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m19.80s | 983628 ko || +0m00.25s || 11100 ko | +1.26% | +1.12% 0m19.34s | 698100 ko | Rewriter/Rewriter/Examples/LiftLetsMap | 0m19.01s | 695816 ko || +0m00.32s || 2284 ko | +1.73% | +0.32% 0m19.07s | 613156 ko | Rewriter/Language/Inversion | 0m18.76s | 612440 ko || +0m00.30s || 716 ko | +1.65% | +0.11% 0m18.96s | 1522484 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m18.23s | 1492188 ko || +0m00.73s || 30296 ko | +4.00% | +2.03% 0m18.91s | 811004 ko | Curves/Edwards/XYZT/Basic.vo | 0m19.47s | 811332 ko || -0m00.55s || -328 ko | -2.87% | -0.04% 0m18.83s | 823944 ko | Arithmetic/Core.vo | 0m18.48s | 823508 ko || +0m00.34s || 436 ko | +1.89% | +0.05% 0m18.72s | 1514728 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m18.67s | 1498072 ko || +0m00.04s || 16656 ko | +0.26% | +1.11% 0m18.44s | 813408 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo | 0m18.26s | 816284 ko || +0m00.17s || -2876 ko | +0.98% | -0.35% 0m18.38s | 747140 ko | Language/IdentifiersGENERATED.vo | 0m17.93s | 747868 ko || +0m00.44s || -728 ko | +2.50% | -0.09% 0m18.36s | 1781612 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m19.01s | 1763764 ko || -0m00.65s || 17848 ko | -3.41% | +1.01% 0m18.13s | 1483480 ko | ExtractionOCaml/base_conversion.ml | 0m18.01s | 1463764 ko || +0m00.11s || 19716 ko | +0.66% | +1.34% 0m18.10s | 132852 ko | fiat-bedrock2/src/p434_64.c | 0m17.74s | 132956 ko || +0m00.36s || -104 ko | +2.02% | -0.07% 0m17.86s | 1479096 ko | ExtractionOCaml/saturated_solinas.ml | 0m17.71s | 1472784 ko || +0m00.14s || 6312 ko | +0.84% | +0.42% 0m17.79s | 1698056 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m17.83s | 1812412 ko || -0m00.03s || -114356 ko | -0.22% | -6.30% 0m16.55s | 567492 ko | Algebra/Field.vo | 0m16.90s | 567672 ko || -0m00.34s || -180 ko | -2.07% | -0.03% 0m16.30s | 654900 ko | Stringification/IR.vo | 0m15.32s | 649772 ko || +0m00.98s || 5128 ko | +6.39% | +0.78% 0m15.94s | 642888 ko | Language/IdentifiersGENERATEDProofs.vo | 0m15.78s | 640752 ko || +0m00.16s || 2136 ko | +1.01% | +0.33% 0m15.71s | 122496 ko | fiat-rust/src/p434_64.rs | 0m15.54s | 122336 ko || +0m00.17s || 160 ko | +1.09% | +0.13% 0m15.65s | 880424 ko | Util/ZRange/LandLorBounds.vo | 0m15.02s | 880216 ko || +0m00.63s || 208 ko | +4.19% | +0.02% 0m15.49s | 994900 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m15.44s | 993968 ko || +0m00.05s || 932 ko | +0.32% | +0.09% 0m15.28s | 1689280 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs | 0m15.19s | 1661224 ko || +0m00.08s || 28056 ko | +0.59% | +1.68% 0m15.11s | 689144 ko | Rewriter/Rewriter/Examples/Plus0Tree | 0m15.03s | 684720 ko || +0m00.08s || 4424 ko | +0.53% | +0.64% 0m14.99s | 1626748 ko | ExtractionHaskell/word_by_word_montgomery.hs | 0m14.12s | 1569720 ko || +0m00.87s || 57028 ko | +6.16% | +3.63% 0m14.50s | 688788 ko | Rewriter/Rewriter/Examples/UnderLetsPlus0 | 0m14.37s | 684648 ko || +0m00.13s || 4140 ko | +0.90% | +0.60% 0m14.31s | 729944 ko | Rewriter/Demo | 0m14.41s | 741344 ko || -0m00.09s || -11400 ko | -0.69% | -1.53% 0m13.15s | 635692 ko | Rewriter/Language/IdentifiersLibraryProofs | 0m13.26s | 640652 ko || -0m00.10s || -4960 ko | -0.82% | -0.77% 0m12.53s | 1466612 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs | 0m11.91s | 1470460 ko || +0m00.61s || -3848 ko | +5.20% | -0.26% 0m12.33s | 115512 ko | fiat-java/src/FiatP224.java | 0m12.24s | 115652 ko || +0m00.08s || -140 ko | +0.73% | -0.12% 0m12.13s | 115628 ko | fiat-rust/src/p224_32.rs | 0m12.06s | 115572 ko || +0m00.07s || 56 ko | +0.58% | +0.04% 0m12.00s | 583940 ko | Primitives/MxDHRepChange.vo | 0m12.58s | 584248 ko || -0m00.58s || -308 ko | -4.61% | -0.05% 0m11.96s | 808372 ko | Arithmetic/FancyMontgomeryReduction.vo | 0m11.93s | 808456 ko || +0m00.03s || -84 ko | +0.25% | -0.01% 0m11.96s | 106712 ko | fiat-c/src/p224_32.c | 0m11.92s | 106688 ko || +0m00.04s || 24 ko | +0.33% | +0.02% 0m11.89s | 1432548 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs | 0m11.50s | 1361004 ko || +0m00.39s || 71544 ko | +3.39% | +5.25% 0m11.73s | 1420776 ko | ExtractionHaskell/bedrock2_base_conversion.hs | 0m11.49s | 1356016 ko || +0m00.24s || 64760 ko | +2.08% | +4.77% 0m11.49s | 1417948 ko | ExtractionHaskell/unsaturated_solinas.hs | 0m11.97s | 1410428 ko || -0m00.48s || 7520 ko | -4.01% | +0.53% 0m11.40s | 1354852 ko | ExtractionHaskell/base_conversion.hs | 0m11.20s | 1370652 ko || +0m00.20s || -15800 ko | +1.78% | -1.15% 0m11.25s | 1355376 ko | ExtractionHaskell/saturated_solinas.hs | 0m10.60s | 1371336 ko || +0m00.65s || -15960 ko | +6.13% | -1.16% 0m10.67s | 500848 ko | Algebra/Ring.vo | 0m11.07s | 500884 ko || -0m00.40s || -36 ko | -3.61% | -0.00% 0m10.05s | 984696 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m10.47s | 984868 ko || -0m00.41s || -172 ko | -4.01% | -0.01% 0m09.80s | 791468 ko | PushButtonSynthesis/SmallExamples.vo | 0m09.60s | 788984 ko || +0m00.20s || 2484 ko | +2.08% | +0.31% 0m09.34s | 715912 ko | Util/ZRange/CornersMonotoneBounds.vo | 0m09.37s | 715836 ko || -0m00.02s || 76 ko | -0.32% | +0.01% 0m09.23s | 753776 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m09.19s | 750876 ko || +0m00.04s || 2900 ko | +0.43% | +0.38% 0m09.08s | 949412 ko | Bedrock/Field/Translation/Proofs/Flatten.vo | 0m08.91s | 947388 ko || +0m00.16s || 2024 ko | +1.90% | +0.21% 0m08.73s | 1057796 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo | 0m08.76s | 1065860 ko || -0m00.02s || -8064 ko | -0.34% | -0.75% 0m08.44s | 629000 ko | Language/IdentifiersBasicGENERATED.vo | 0m08.90s | 627456 ko || -0m00.46s || 1544 ko | -5.16% | +0.24% 0m07.85s | 656224 ko | Rewriter/Passes/NoSelect.vo | 0m07.40s | 653324 ko || +0m00.44s || 2900 ko | +6.08% | +0.44% 0m07.76s | 917092 ko | PushButtonSynthesis/BarrettReduction.vo | 0m07.73s | 920724 ko || +0m00.02s || -3632 ko | +0.38% | -0.39% 0m07.57s | 89432 ko | fiat-bedrock2/src/p384_64.c | 0m07.58s | 89344 ko || -0m00.00s || 88 ko | -0.13% | +0.09% 0m07.54s | 39660 ko | fiat-rust/src/p448_solinas_32.rs | 0m07.20s | 39624 ko || +0m00.33s || 36 ko | +4.72% | +0.09% 0m07.51s | 39884 ko | fiat-c/src/p448_solinas_32.c | 0m07.52s | 39856 ko || -0m00.00s || 28 ko | -0.13% | +0.07% 0m07.45s | 693700 ko | Util/ListUtil.vo | 0m07.44s | 693520 ko || +0m00.00s || 180 ko | +0.13% | +0.02% 0m07.29s | 1244276 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo | 0m07.24s | 1245116 ko || +0m00.04s || -840 ko | +0.69% | -0.06% 0m07.07s | 676404 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m06.78s | 673516 ko || +0m00.29s || 2888 ko | +4.27% | +0.42% 0m06.90s | 920240 ko | PushButtonSynthesis/BaseConversion.vo | 0m06.54s | 920320 ko || +0m00.36s || -80 ko | +5.50% | -0.00% 0m06.83s | 503108 ko | Rewriter/Util/ListUtil | 0m06.55s | 501576 ko || +0m00.28s || 1532 ko | +4.27% | +0.30% 0m06.64s | 94052 ko | fiat-rust/src/p384_64.rs | 0m06.04s | 93920 ko || +0m00.59s || 132 ko | +9.93% | +0.14% 0m06.62s | 502564 ko | Util/MSets/Sum.vo | 0m06.72s | 502956 ko || -0m00.09s || -392 ko | -1.48% | -0.07% 0m06.54s | 749172 ko | Util/ZUtil/Modulo.vo | 0m06.60s | 749296 ko || -0m00.05s || -124 ko | -0.90% | -0.01% 0m06.46s | 81268 ko | fiat-c/src/p384_64.c | 0m05.93s | 81212 ko || +0m00.53s || 56 ko | +8.93% | +0.06% 0m06.32s | 964408 ko | Bedrock/Field/Synthesis/Examples/EncodeDecode.vo | 0m06.37s | 964896 ko || -0m00.04s || -488 ko | -0.78% | -0.05% 0m06.31s | 82212 ko | fiat-go/src/p384_64.go | 0m06.83s | 82240 ko || -0m00.52s || -28 ko | -7.61% | -0.03% 0m06.26s | 804636 ko | COperationSpecifications.vo | 0m06.18s | 804412 ko || +0m00.08s || 224 ko | +1.29% | +0.02% 0m06.13s | 731360 ko | Util/ZUtil/ZSimplify/Autogenerated.vo | 0m06.33s | 730924 ko || -0m00.20s || 436 ko | -3.15% | +0.05% 0m06.10s | 707744 ko | Util/ZRange/BasicLemmas.vo | 0m06.23s | 708104 ko || -0m00.13s || -360 ko | -2.08% | -0.05% 0m05.99s | 800004 ko | Fancy/Prod.vo | 0m06.05s | 797560 ko || -0m00.05s || 2444 ko | -0.99% | +0.30% 0m05.99s | 919180 ko | PushButtonSynthesis/Primitives.vo | 0m06.00s | 914104 ko || -0m00.00s || 5076 ko | -0.16% | +0.55% 0m05.92s | 699284 ko | BoundsPipeline.vo | 0m05.76s | 696844 ko || +0m00.16s || 2440 ko | +2.77% | +0.35% 0m05.87s | 607780 ko | Curves/Edwards/Pre.vo | 0m05.57s | 607760 ko || +0m00.29s || 20 ko | +5.38% | +0.00% 0m05.71s | 717532 ko | Arithmetic/MontgomeryReduction/Proofs.vo | 0m05.77s | 717680 ko || -0m00.05s || -148 ko | -1.03% | -0.02% 0m05.51s | 567556 ko | Util/FsatzAutoLemmas.vo | 0m05.53s | 567580 ko || -0m00.02s || -24 ko | -0.36% | -0.00% 0m05.31s | 606340 ko | Language/InversionExtra.vo | 0m05.16s | 604280 ko || +0m00.14s || 2060 ko | +2.90% | +0.34% 0m05.26s | 795968 ko | UnsaturatedSolinasHeuristics.vo | 0m05.52s | 795544 ko || -0m00.25s || 424 ko | -4.71% | +0.05% 0m05.13s | 584412 ko | Algebra/Field_test.vo | 0m05.05s | 584372 ko || +0m00.08s || 40 ko | +1.58% | +0.00% 0m04.91s | 780436 ko | Util/ZUtil/Morphisms.vo | 0m04.95s | 780412 ko || -0m00.04s || 24 ko | -0.80% | +0.00% 0m04.79s | 710164 ko | CastLemmas.vo | 0m04.71s | 709620 ko || +0m00.08s || 544 ko | +1.69% | +0.07% 0m04.69s | 789232 ko | Arithmetic/UniformWeight.vo | 0m04.94s | 789544 ko || -0m00.25s || -312 ko | -5.06% | -0.03% 0m04.64s | 527420 ko | Rewriter/Language/IdentifiersBasicLibrary | 0m04.60s | 527288 ko || +0m00.04s || 132 ko | +0.86% | +0.02% 0m04.62s | 734812 ko | Arithmetic/BarrettReduction/Generalized.vo | 0m04.65s | 735076 ko || -0m00.03s || -264 ko | -0.64% | -0.03% 0m04.34s | 730192 ko | Util/ZUtil/LandLorShiftBounds.vo | 0m04.42s | 730372 ko || -0m00.08s || -180 ko | -1.80% | -0.02% 0m04.24s | 590952 ko | Curves/Montgomery/Affine.vo | 0m04.47s | 590612 ko || -0m00.22s || 340 ko | -5.14% | +0.05% 0m04.17s | 737572 ko | Util/ZUtil/LandLorBounds.vo | 0m04.19s | 738172 ko || -0m00.02s || -600 ko | -0.47% | -0.08% 0m04.10s | 719208 ko | Arithmetic/BarrettReduction/HAC.vo | 0m03.97s | 719400 ko || +0m00.12s || -192 ko | +3.27% | -0.02% 0m03.97s | 768568 ko | Bedrock/Field/Synthesis/Examples/MulTwice.vo | 0m04.00s | 768340 ko || -0m00.02s || 228 ko | -0.74% | +0.02% 0m03.81s | 907100 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.97s | 909484 ko || -0m00.16s || -2384 ko | -4.03% | -0.26% 0m03.66s | 661992 ko | PushButtonSynthesis/BaseConversionReificationCache.vo | 0m03.77s | 659136 ko || -0m00.10s || 2856 ko | -2.91% | +0.43% 0m03.56s | 416408 ko | Algebra/Group.vo | 0m03.53s | 416552 ko || +0m00.03s || -144 ko | +0.84% | -0.03% 0m03.53s | 619436 ko | Rewriter/Passes/AddAssocLeft.vo | 0m03.49s | 616188 ko || +0m00.03s || 3248 ko | +1.14% | +0.52% 0m03.49s | 899560 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.44s | 892324 ko || +0m00.05s || 7236 ko | +1.45% | +0.81% 0m03.38s | 580012 ko | Rewriter/Passes/Test.vo | 0m03.36s | 578660 ko || +0m00.02s || 1352 ko | +0.59% | +0.23% 0m03.38s | 33768 ko | fiat-bedrock2/src/p521_64.c | 0m03.01s | 34108 ko || +0m00.37s || -340 ko | +12.29% | -0.99% 0m03.27s | 930012 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo | 0m03.00s | 925480 ko || +0m00.27s || 4532 ko | +9.00% | +0.48% 0m03.25s | 27476 ko | fiat-go/src/p521_64.go | 0m03.21s | 27620 ko || +0m00.04s || -144 ko | +1.24% | -0.52% 0m03.04s | 788484 ko | Arithmetic/Freeze.vo | 0m02.99s | 788604 ko || +0m00.04s || -120 ko | +1.67% | -0.01% 0m03.04s | 686904 ko | Arithmetic/Primitives.vo | 0m03.07s | 687072 ko || -0m00.02s || -168 ko | -0.97% | -0.02% 0m03.02s | 726732 ko | Util/ZUtil/Shift.vo | 0m03.02s | 726668 ko || +0m00.00s || 64 ko | +0.00% | +0.00% 0m02.98s | 22360 ko | fiat-rust/src/p521_64.rs | 0m02.96s | 22260 ko || +0m00.02s || 100 ko | +0.67% | +0.44% 0m02.93s | 488820 ko | Util/MSets/Iso.vo | 0m02.96s | 488860 ko || -0m00.02s || -40 ko | -1.01% | -0.00% 0m02.86s | 560308 ko | Spec/MontgomeryCurve.vo | 0m02.71s | 560860 ko || +0m00.14s || -552 ko | +5.53% | -0.09% 0m02.85s | 934092 ko | Bedrock/Field/Common/Names/MakeNames.vo | 0m02.90s | 932456 ko || -0m00.04s || 1636 ko | -1.72% | +0.17% 0m02.81s | 521072 ko | MiscCompilerPassesProofs.vo | 0m02.74s | 520280 ko || +0m00.06s || 792 ko | +2.55% | +0.15% 0m02.75s | 714628 ko | Arithmetic/BarrettReduction/RidiculousFish.vo | 0m02.56s | 714860 ko || +0m00.18s || -232 ko | +7.42% | -0.03% 0m02.67s | 22952 ko | fiat-c/src/p521_64.c | 0m02.95s | 22984 ko || -0m00.28s || -32 ko | -9.49% | -0.13% 0m02.61s | 922484 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo | 0m02.55s | 918888 ko || +0m00.06s || 3596 ko | +2.35% | +0.39% 0m02.53s | 713944 ko | Util/ZUtil/Div.vo | 0m02.54s | 713864 ko || -0m00.01s || 80 ko | -0.39% | +0.01% 0m02.51s | 742400 ko | Arithmetic/BaseConversion.vo | 0m02.38s | 742440 ko || +0m00.12s || -40 ko | +5.46% | -0.00% 0m02.45s | 741008 ko | CLI.vo | 0m02.55s | 737092 ko || -0m00.09s || 3916 ko | -3.92% | +0.53% 0m02.44s | 782848 ko | Arithmetic/ModOps.vo | 0m02.49s | 783076 ko || -0m00.05s || -228 ko | -2.00% | -0.02% 0m02.42s | 744852 ko | Rewriter/PerfTesting/Core.vo | 0m02.39s | 743584 ko || +0m00.02s || 1268 ko | +1.25% | +0.17% 0m02.37s | 761416 ko | Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.vo | 0m02.31s | 759568 ko || +0m00.06s || 1848 ko | +2.59% | +0.24% 0m02.35s | 605744 ko | Rewriter/Passes/StripLiteralCasts.vo | 0m02.32s | 604180 ko || +0m00.03s || 1564 ko | +1.29% | +0.25% 0m02.35s | 35992 ko | fiat-bedrock2/src/p448_solinas_64.c | 0m02.34s | 36040 ko || +0m00.01s || -48 ko | +0.42% | -0.13% 0m02.28s | 713848 ko | Arithmetic/ModularArithmeticTheorems.vo | 0m02.35s | 714008 ko || -0m00.07s || -160 ko | -2.97% | -0.02% 0m02.27s | 746572 ko | Bedrock/Standalone/Stringification.vo | 0m02.02s | 745628 ko || +0m00.25s || 944 ko | +12.37% | +0.12% 0m02.26s | 34248 ko | fiat-bedrock2/src/curve25519_32.c | 0m02.19s | 34104 ko || +0m00.06s || 144 ko | +3.19% | +0.42% 0m02.25s | 609580 ko | Rewriter/Passes/UnfoldValueBarrier.vo | 0m02.38s | 606484 ko || -0m00.12s || 3096 ko | -5.46% | +0.51% 0m02.25s | 664572 ko | Util/ZUtil/Testbit.vo | 0m02.28s | 664268 ko || -0m00.02s || 304 ko | -1.31% | +0.04% 0m02.24s | 653004 ko | CompilersTestCases.vo | 0m02.20s | 652508 ko || +0m00.04s || 496 ko | +1.81% | +0.07% 0m02.21s | 696056 ko | Util/NatUtil.vo | 0m02.23s | 695800 ko || -0m00.02s || 256 ko | -0.89% | +0.03% 0m02.21s | 688292 ko | Util/ZUtil/Bitwise.vo | 0m02.23s | 688092 ko || -0m00.02s || 200 ko | -0.89% | +0.02% 0m02.17s | 752944 ko | AbstractInterpretation/ZRange.vo | 0m02.05s | 750316 ko || +0m00.12s || 2628 ko | +5.85% | +0.35% 0m02.17s | 768552 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.10s | 764088 ko || +0m00.06s || 4464 ko | +3.33% | +0.58% 0m02.16s | 779928 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m02.18s | 775356 ko || -0m00.02s || 4572 ko | -0.91% | +0.58% 0m02.15s | 29084 ko | fiat-go/src/p448_solinas_64.go | 0m02.10s | 29128 ko || +0m00.04s || -44 ko | +2.38% | -0.15% 0m02.14s | 772044 ko | Stringification/Language.vo | 0m02.11s | 771780 ko || +0m00.03s || 264 ko | +1.42% | +0.03% 0m02.11s | 757992 ko | Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.vo | 0m02.09s | 754268 ko || +0m00.02s || 3724 ko | +0.95% | +0.49% 0m02.10s | 779540 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m02.06s | 775164 ko || +0m00.04s || 4376 ko | +1.94% | +0.56% 0m02.09s | 607584 ko | Rewriter/Passes/ToFancy.vo | 0m02.13s | 604552 ko || -0m00.04s || 3032 ko | -1.87% | +0.50% 0m02.09s | 657728 ko | Util/Tuple.vo | 0m02.08s | 657760 ko || +0m00.00s || -32 ko | +0.48% | -0.00% 0m02.08s | 745428 ko | Bedrock/Field/Synthesis/Generic/Operation.vo | 0m02.09s | 744864 ko || -0m00.00s || 564 ko | -0.47% | +0.07% 0m02.05s | 716352 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m01.96s | 714736 ko || +0m00.08s || 1616 ko | +4.59% | +0.22% 0m02.03s | 749816 ko | StandaloneHaskellMain.vo | 0m02.03s | 747468 ko || +0m00.00s || 2348 ko | +0.00% | +0.31% 0m02.02s | 739548 ko | Bedrock/Field/Synthesis/Generic/Tactics.vo | 0m02.01s | 737892 ko || +0m00.01s || 1656 ko | +0.49% | +0.22% 0m02.02s | 740760 ko | Bedrock/Field/Synthesis/Specialized/ReifiedOperation.vo | 0m01.95s | 737644 ko || +0m00.07s || 3116 ko | +3.58% | +0.42% 0m02.01s | 745704 ko | Bedrock/Field/Synthesis/Specialized/Tactics.vo | 0m01.79s | 743324 ko || +0m00.21s || 2380 ko | +12.29% | +0.32% 0m01.99s | 721372 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.01s | 719832 ko || -0m00.01s || 1540 ko | -0.99% | +0.21% 0m01.97s | 842928 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo | 0m02.26s | 840868 ko || -0m00.28s || 2060 ko | -12.83% | +0.24% 0m01.97s | 687852 ko | Bedrock/Field/Translation/Cmd.vo | 0m01.90s | 684932 ko || +0m00.07s || 2920 ko | +3.68% | +0.42% 0m01.96s | 563392 ko | AbstractInterpretation/AbstractInterpretation.vo | 0m02.11s | 562712 ko || -0m00.14s || 680 ko | -7.10% | +0.12% 0m01.95s | 732148 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo | 0m01.94s | 730500 ko || +0m00.01s || 1648 ko | +0.51% | +0.22% 0m01.91s | 740256 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m01.97s | 737572 ko || -0m00.06s || 2684 ko | -3.04% | +0.36% 0m01.89s | 586496 ko | Bedrock/Field/Translation/Expr.vo | 0m02.01s | 582668 ko || -0m00.11s || 3828 ko | -5.97% | +0.65% 0m01.89s | 721528 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m01.98s | 719716 ko || -0m00.09s || 1812 ko | -4.54% | +0.25% 0m01.89s | 750208 ko | StandaloneOCamlMain.vo | 0m02.01s | 747844 ko || -0m00.11s || 2364 ko | -5.97% | +0.31% 0m01.88s | 579764 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness | 0m01.84s | 578572 ko || +0m00.03s || 1192 ko | +2.17% | +0.20% 0m01.85s | 719604 ko | Bedrock/Field/Translation/Parameters/SelectParameters.vo | 0m01.88s | 717428 ko || -0m00.02s || 2176 ko | -1.59% | +0.30% 0m01.83s | 22184 ko | fiat-c/src/p448_solinas_64.c | 0m01.85s | 22028 ko || -0m00.02s || 156 ko | -1.08% | +0.70% 0m01.80s | 640124 ko | Algebra/ScalarMult.vo | 0m01.85s | 640776 ko || -0m00.05s || -652 ko | -2.70% | -0.10% 0m01.80s | 697128 ko | Util/ZRange/SplitRangeBounds.vo | 0m01.80s | 697036 ko || +0m00.00s || 92 ko | +0.00% | +0.01% 0m01.79s | 714200 ko | Util/ZUtil/Quot.vo | 0m01.79s | 714020 ko || +0m00.00s || 180 ko | +0.00% | +0.02% 0m01.78s | 22244 ko | fiat-java/src/FiatCurve25519.java | 0m01.79s | 22156 ko || -0m00.01s || 88 ko | -0.55% | +0.39% 0m01.76s | 731112 ko | Util/ZRange/SplitBounds.vo | 0m01.90s | 731080 ko || -0m00.13s || 32 ko | -7.36% | +0.00% 0m01.76s | 22924 ko | fiat-rust/src/p448_solinas_64.rs | 0m01.84s | 22964 ko || -0m00.08s || -40 ko | -4.34% | -0.17% 0m01.75s | 724660 ko | Arithmetic/Partition.vo | 0m01.73s | 724360 ko || +0m00.02s || 300 ko | +1.15% | +0.04% 0m01.74s | 717332 ko | Arithmetic/PrimeFieldTheorems.vo | 0m01.89s | 717476 ko || -0m00.14s || -144 ko | -7.93% | -0.02% 0m01.74s | 525124 ko | Spec/WeierstrassCurve.vo | 0m01.74s | 525288 ko || +0m00.00s || -164 ko | +0.00% | -0.03% 0m01.74s | 663924 ko | Util/ZUtil/Pow2Mod.vo | 0m01.65s | 663816 ko || +0m00.09s || 108 ko | +5.45% | +0.01% 0m01.73s | 21496 ko | fiat-rust/src/curve25519_32.rs | 0m01.75s | 21144 ko || -0m00.02s || 352 ko | -1.14% | +1.66% 0m01.70s | 457864 ko | Rewriter/Util/NatUtil | 0m01.71s | 457604 ko || -0m00.01s || 260 ko | -0.58% | +0.05% 0m01.68s | 22112 ko | fiat-c/src/curve25519_32.c | 0m01.73s | 22204 ko || -0m00.05s || -92 ko | -2.89% | -0.41% 0m01.68s | 22160 ko | fiat-go/src/curve25519_32.go | 0m01.72s | 22328 ko || -0m00.04s || -168 ko | -2.32% | -0.75% 0m01.66s | 705624 ko | Util/ZUtil/Rshi.vo | 0m01.71s | 705236 ko || -0m00.05s || 388 ko | -2.92% | +0.05% 0m01.64s | 709448 ko | Util/ZUtil/AddGetCarry.vo | 0m01.69s | 709652 ko || -0m00.05s || -204 ko | -2.95% | -0.02% 0m01.62s | 653896 ko | Bedrock/Field/Common/Tactics.vo | 0m01.45s | 652432 ko || +0m00.17s || 1464 ko | +11.72% | +0.22% 0m01.62s | 681072 ko | Bedrock/Field/Translation/Func.vo | 0m01.68s | 679372 ko || -0m00.05s || 1700 ko | -3.57% | +0.25% 0m01.62s | 521076 ko | Rewriter/Language/IdentifiersLibrary | 0m01.51s | 519436 ko || +0m00.11s || 1640 ko | +7.28% | +0.31% 0m01.53s | 659012 ko | Util/ZUtil/Ones.vo | 0m01.55s | 659092 ko || -0m00.02s || -80 ko | -1.29% | -0.01% 0m01.47s | 532768 ko | Curves/Edwards/XYZT/Precomputed.vo | 0m01.43s | 532360 ko || +0m00.04s || 408 ko | +2.79% | +0.07% 0m01.47s | 632288 ko | Util/ListUtil/Forall.vo | 0m01.50s | 632548 ko || -0m00.03s || -260 ko | -2.00% | -0.04% 0m01.44s | 34204 ko | fiat-bedrock2/src/secp256k1_64.c | 0m01.44s | 34260 ko || +0m00.00s || -56 ko | +0.00% | -0.16% 0m01.42s | 571640 ko | Stringification/Go.vo | 0m01.40s | 571488 ko || +0m00.02s || 152 ko | +1.42% | +0.02% 0m01.41s | 517708 ko | Rewriter/Rewriter/Rewriter | 0m01.31s | 516220 ko || +0m00.09s || 1488 ko | +7.63% | +0.28% 0m01.39s | 34024 ko | fiat-go/src/secp256k1_64.go | 0m01.37s | 33952 ko || +0m00.01s || 72 ko | +1.45% | +0.21% 0m01.38s | 38068 ko | fiat-bedrock2/src/p224_64.c | 0m01.35s | 38000 ko || +0m00.02s || 68 ko | +2.22% | +0.17% 0m01.36s | 573552 ko | Stringification/C.vo | 0m01.36s | 571396 ko || +0m00.00s || 2156 ko | +0.00% | +0.37% 0m01.34s | 570412 ko | Stringification/Java.vo | 0m01.46s | 569240 ko || -0m00.11s || 1172 ko | -8.21% | +0.20% 0m01.34s | 569616 ko | Stringification/Rust.vo | 0m01.45s | 568380 ko || -0m00.10s || 1236 ko | -7.58% | +0.21% 0m01.34s | 33860 ko | fiat-go/src/p224_64.go | 0m01.31s | 34268 ko || +0m00.03s || -408 ko | +2.29% | -1.19% 0m01.32s | 523224 ko | Curves/Montgomery/AffineInstances.vo | 0m01.29s | 523412 ko || +0m00.03s || -188 ko | +2.32% | -0.03% 0m01.31s | 577376 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo | 0m01.31s | 575144 ko || +0m00.00s || 2232 ko | +0.00% | +0.38% 0m01.31s | 630612 ko | Rewriter/All.vo | 0m01.27s | 628928 ko || +0m00.04s || 1684 ko | +3.14% | +0.26% 0m01.31s | 35192 ko | fiat-bedrock2/src/p256_64.c | 0m01.32s | 35128 ko || -0m00.01s || 64 ko | -0.75% | +0.18% 0m01.29s | 33120 ko | fiat-rust/src/secp256k1_64.rs | 0m01.22s | 33120 ko || +0m00.07s || 0 ko | +5.73% | +0.00% 0m01.28s | 489276 ko | Fancy/Spec.vo | 0m01.32s | 489452 ko || -0m00.04s || -176 ko | -3.03% | -0.03% 0m01.27s | 576996 ko | Bedrock/Field/Common/Types.vo | 0m01.20s | 573200 ko || +0m00.07s || 3796 ko | +5.83% | +0.66% 0m01.27s | 34912 ko | fiat-c/src/secp256k1_64.c | 0m01.28s | 34928 ko || -0m00.01s || -16 ko | -0.78% | -0.04% 0m01.27s | 33984 ko | fiat-go/src/p256_64.go | 0m01.27s | 33996 ko || +0m00.00s || -12 ko | +0.00% | -0.03% 0m01.26s | 574248 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo | 0m01.16s | 573000 ko || +0m00.10s || 1248 ko | +8.62% | +0.21% 0m01.23s | 518604 ko | Rewriter/Rewriter/Reify | 0m01.29s | 517904 ko || -0m00.06s || 700 ko | -4.65% | +0.13% 0m01.21s | 34948 ko | fiat-rust/src/p256_64.rs | 0m01.11s | 34956 ko || +0m00.09s || -8 ko | +9.00% | -0.02% 0m01.20s | 660408 ko | Arithmetic/BarrettReduction/Wikipedia.vo | 0m01.11s | 660496 ko || +0m00.08s || -88 ko | +8.10% | -0.01% 0m01.20s | 34940 ko | fiat-c/src/p224_64.c | 0m01.20s | 35076 ko || +0m00.00s || -136 ko | +0.00% | -0.38% 0m01.18s | 575920 ko | Bedrock/Field/Translation/Flatten.vo | 0m01.29s | 574000 ko || -0m00.11s || 1920 ko | -8.52% | +0.33% 0m01.18s | 576956 ko | Bedrock/Field/Translation/LoadStoreList.vo | 0m01.30s | 575552 ko || -0m00.12s || 1404 ko | -9.23% | +0.24% 0m01.18s | 556964 ko | Language/APINotations.vo | 0m01.16s | 553944 ko || +0m00.02s || 3020 ko | +1.72% | +0.54% 0m01.18s | 33832 ko | fiat-c/src/p256_64.c | 0m01.17s | 33728 ko || +0m00.01s || 104 ko | +0.85% | +0.30% 0m01.17s | 670196 ko | Util/NumTheoryUtil.vo | 0m01.10s | 670448 ko || +0m00.06s || -252 ko | +6.36% | -0.03% 0m01.16s | 33944 ko | fiat-rust/src/p224_64.rs | 0m01.22s | 33880 ko || -0m00.06s || 64 ko | -4.91% | +0.18% 0m01.15s | 478124 ko | Rewriter/Language/Language | 0m01.20s | 476752 ko || -0m00.05s || 1372 ko | -4.16% | +0.28% 0m01.15s | 444216 ko | Rewriter/Util/ListUtil/Forall | 0m01.01s | 445400 ko || +0m00.13s || -1184 ko | +13.86% | -0.26% 0m01.13s | 548480 ko | ArithmeticCPS/Freeze.vo | 0m01.02s | 548816 ko || +0m00.10s || -336 ko | +10.78% | -0.06% 0m01.13s | 551232 ko | Language/WfExtra.vo | 0m01.13s | 550136 ko || +0m00.00s || 1096 ko | +0.00% | +0.19% 0m01.12s | 556432 ko | AbstractInterpretation/WfExtra.vo | 0m01.18s | 555212 ko || -0m00.05s || 1220 ko | -5.08% | +0.21% 0m01.11s | 549688 ko | Language/API.vo | 0m01.03s | 547860 ko || +0m00.08s || 1828 ko | +7.76% | +0.33% 0m01.11s | 551644 ko | MiscCompilerPassesProofsExtra.vo | 0m01.09s | 549704 ko || +0m00.02s || 1940 ko | +1.83% | +0.35% 0m01.11s | 538548 ko | Rewriter/Rewriter/AllTactics | 0m01.13s | 537856 ko || -0m00.01s || 692 ko | -1.76% | +0.12% 0m01.11s | 709160 ko | Util/ZUtil/CC.vo | 0m01.08s | 708948 ko || +0m00.03s || 212 ko | +2.77% | +0.02% 0m01.10s | 575236 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo | 0m01.19s | 574120 ko || -0m00.08s || 1116 ko | -7.56% | +0.19% 0m01.09s | 555040 ko | PushButtonSynthesis/ReificationCache.vo | 0m01.05s | 553440 ko || +0m00.04s || 1600 ko | +3.80% | +0.28% 0m01.08s | 726664 ko | Util/QUtil.vo | 0m01.17s | 726908 ko || -0m00.08s || -244 ko | -7.69% | -0.03% 0m01.07s | 462100 ko | Util/Bool/Reflect.vo | 0m01.05s | 461700 ko || +0m00.02s || 400 ko | +1.90% | +0.08% 0m01.06s | 507572 ko | Algebra/IntegralDomain.vo | 0m01.02s | 507504 ko || +0m00.04s || 68 ko | +3.92% | +0.01% 0m01.02s | 551300 ko | Language/UnderLetsProofsExtra.vo | 0m00.95s | 550128 ko || +0m00.07s || 1172 ko | +7.36% | +0.21% 0m01.02s | 644224 ko | Util/Decidable/Decidable2Bool.vo | 0m00.98s | 644376 ko || +0m00.04s || -152 ko | +4.08% | -0.02% 0m01.00s | 542504 ko | ArithmeticCPS/ModOps.vo | 0m00.95s | 542472 ko || +0m00.05s || 32 ko | +5.26% | +0.00% 0m01.00s | 557108 ko | Rewriter/AllTacticsExtra.vo | 0m00.98s | 556036 ko || +0m00.02s || 1072 ko | +2.04% | +0.19% 0m00.99s | 651656 ko | Util/ZUtil/Modulo/PullPush.vo | 0m01.03s | 651480 ko || -0m00.04s || 176 ko | -3.88% | +0.02% 0m00.94s | 662812 ko | Util/ZUtil/Stabilization.vo | 0m00.92s | 662892 ko || +0m00.01s || -80 ko | +2.17% | -0.01% 0m00.93s | 504444 ko | MiscCompilerPasses.vo | 0m00.90s | 503724 ko || +0m00.03s || 720 ko | +3.33% | +0.14% 0m00.93s | 685792 ko | Util/ZUtil/Ltz.vo | 0m00.87s | 685812 ko || +0m00.06s || -20 ko | +6.89% | -0.00% 0m00.91s | 479764 ko | Rewriter/Rules.vo | 0m01.00s | 479396 ko || -0m00.08s || 368 ko | -8.99% | +0.07% 0m00.89s | 626768 ko | Util/Loops.vo | 0m00.91s | 626748 ko || -0m00.02s || 20 ko | -2.19% | +0.00% 0m00.88s | 540832 ko | ArithmeticCPS/WordByWordMontgomery.vo | 0m00.99s | 540592 ko || -0m00.10s || 240 ko | -11.11% | +0.04% 0m00.88s | 523472 ko | Rewriter/Rewriter/ProofsCommonTactics | 0m00.99s | 519808 ko || -0m00.10s || 3664 ko | -11.11% | +0.70% 0m00.86s | 507220 ko | Rewriter/Language/IdentifiersGenerateProofs | 0m00.80s | 506648 ko || +0m00.05s || 572 ko | +7.49% | +0.11% 0m00.86s | 532684 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings | 0m00.87s | 535264 ko || -0m00.01s || -2580 ko | -1.14% | -0.48% 0m00.85s | 558188 ko | Rewriter/Rewriter/Examples/PerfTesting/All | 0m00.88s | 560420 ko || -0m00.03s || -2232 ko | -3.40% | -0.39% 0m00.84s | 549580 ko | ArithmeticCPS/BaseConversion.vo | 0m00.88s | 548988 ko || -0m00.04s || 592 ko | -4.54% | +0.10% 0m00.83s | 506824 ko | Rewriter/Language/IdentifiersGenerate | 0m00.82s | 506616 ko || +0m00.01s || 208 ko | +1.21% | +0.04% 0m00.83s | 531224 ko | Rewriter/Util/plugins/RewriterBuild | 0m00.81s | 529616 ko || +0m00.01s || 1608 ko | +2.46% | +0.30% 0m00.83s | 530180 ko | Rewriter/Util/plugins/RewriterBuildRegistry | 0m00.82s | 529304 ko || +0m00.01s || 876 ko | +1.21% | +0.16% 0m00.83s | 533408 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports | 0m00.79s | 531416 ko || +0m00.03s || 1992 ko | +5.06% | +0.37% 0m00.82s | 630896 ko | Util/ZUtil/Log2.vo | 0m00.73s | 630488 ko || +0m00.08s || 408 ko | +12.32% | +0.06% 0m00.81s | 459588 ko | Util/CPSUtil.vo | 0m00.73s | 459320 ko || +0m00.08s || 268 ko | +10.95% | +0.05% 0m00.80s | 531376 ko | ArithmeticCPS/Core.vo | 0m00.86s | 531484 ko || -0m00.05s || -108 ko | -6.97% | -0.02% 0m00.79s | 322228 ko | Util/PartiallyReifiedProp.vo | 0m00.83s | 322184 ko || -0m00.03s || 44 ko | -4.81% | +0.01% 0m00.78s | 621048 ko | Util/Strings/String_as_OT.vo | 0m00.82s | 621180 ko || -0m00.03s || -132 ko | -4.87% | -0.02% 0m00.78s | 493584 ko | Util/ZRange/OperationsBounds.vo | 0m00.81s | 493820 ko || -0m00.03s || -236 ko | -3.70% | -0.04% 0m00.75s | 527012 ko | ArithmeticCPS/Saturated.vo | 0m00.84s | 527160 ko || -0m00.08s || -148 ko | -10.71% | -0.02% 0m00.73s | 461268 ko | Algebra/SubsetoidRing.vo | 0m00.78s | 461176 ko || -0m00.05s || 92 ko | -6.41% | +0.01% 0m00.73s | 458336 ko | Rewriter/Util/Bool/Reflect | 0m00.74s | 457608 ko || -0m00.01s || 728 ko | -1.35% | +0.15% 0m00.73s | 469020 ko | Util/Arg.vo | 0m00.73s | 469076 ko || +0m00.00s || -56 ko | +0.00% | -0.01% 0m00.72s | 689172 ko | Util/ZUtil/Combine.vo | 0m00.73s | 689204 ko || -0m00.01s || -32 ko | -1.36% | -0.00% 0m00.72s | 666060 ko | Util/ZUtil/Divide.vo | 0m00.68s | 666116 ko || +0m00.03s || -56 ko | +5.88% | -0.00% 0m00.69s | 400324 ko | Util/Structures/Orders/Sum.vo | 0m00.68s | 400376 ko || +0m00.00s || -52 ko | +1.47% | -0.01% 0m00.68s | 670276 ko | Util/ZUtil/Tactics/RewriteModSmall.vo | 0m00.70s | 669948 ko || -0m00.01s || 328 ko | -2.85% | +0.04% 0m00.66s | 508128 ko | Curves/Montgomery/XZ.vo | 0m00.63s | 507744 ko || +0m00.03s || 384 ko | +4.76% | +0.07% 0m00.64s | 625504 ko | Util/Strings/String.vo | 0m00.66s | 625968 ko || -0m00.02s || -464 ko | -3.03% | -0.07% 0m00.63s | 503744 ko | Curves/Weierstrass/Affine.vo | 0m00.67s | 504028 ko || -0m00.04s || -284 ko | -5.97% | -0.05% 0m00.62s | 449400 ko | Util/Strings/ParseArithmeticToTaps.vo | 0m00.65s | 449280 ko || -0m00.03s || 120 ko | -4.61% | +0.02% 0m00.62s | 609812 ko | Util/ZUtil/Pow.vo | 0m00.61s | 609964 ko || +0m00.01s || -152 ko | +1.63% | -0.02% 0m00.61s | 500440 ko | Spec/CompleteEdwardsCurve.vo | 0m00.64s | 500456 ko || -0m00.03s || -16 ko | -4.68% | -0.00% 0m00.60s | 605792 ko | Util/ZUtil/Le.vo | 0m00.63s | 605920 ko || -0m00.03s || -128 ko | -4.76% | -0.02% 0m00.59s | 574180 ko | Util/ZUtil/Peano.vo | 0m00.61s | 574044 ko || -0m00.02s || 136 ko | -3.27% | +0.02% 0m00.59s | 626580 ko | Util/ZUtil/Tactics/LtbToLt.vo | 0m00.62s | 626580 ko || -0m00.03s || 0 ko | -4.83% | +0.00% 0m00.58s | 602148 ko | Util/ZUtil/Opp.vo | 0m00.57s | 601952 ko || +0m00.01s || 196 ko | +1.75% | +0.03% 0m00.57s | 487516 ko | Algebra/Nsatz.vo | 0m00.57s | 487748 ko || +0m00.00s || -232 ko | +0.00% | -0.04% 0m00.57s | 20424 ko | fiat-go/src/curve25519_64.go | 0m00.56s | 20552 ko || +0m00.00s || -128 ko | +1.78% | -0.62% 0m00.56s | 474340 ko | Rewriter/Language/IdentifiersBasicGenerate | 0m00.55s | 474180 ko || +0m00.01s || 160 ko | +1.81% | +0.03% 0m00.56s | 459264 ko | Util/ZBounded.vo | 0m00.51s | 459140 ko || +0m00.05s || 124 ko | +9.80% | +0.02% 0m00.55s | 478140 ko | Arithmetic/ModularArithmeticPre.vo | 0m00.57s | 478224 ko || -0m00.01s || -84 ko | -3.50% | -0.01% 0m00.55s | 397324 ko | Util/Decidable.vo | 0m00.56s | 397348 ko || -0m00.01s || -24 ko | -1.78% | -0.00% 0m00.55s | 455856 ko | Util/HList.vo | 0m00.55s | 455784 ko || +0m00.00s || 72 ko | +0.00% | +0.01% 0m00.55s | 569184 ko | Util/ZUtil/Odd.vo | 0m00.58s | 568712 ko || -0m00.02s || 472 ko | -5.17% | +0.08% 0m00.53s | 470092 ko | Util/MSetPositive/Show.vo | 0m00.54s | 470024 ko || -0m00.01s || 68 ko | -1.85% | +0.01% 0m00.53s | 564236 ko | Util/ZUtil/Tactics/LinearSubstitute.vo | 0m00.58s | 563876 ko || -0m00.04s || 360 ko | -8.62% | +0.06% 0m00.53s | 23648 ko | fiat-bedrock2/src/curve25519_64.c | 0m00.52s | 23392 ko || +0m00.01s || 256 ko | +1.92% | +1.09% 0m00.51s | 448752 ko | Util/MSetPositive/Facts.vo | 0m00.50s | 448856 ko || +0m00.01s || -104 ko | +2.00% | -0.02% 0m00.51s | 456816 ko | Util/ZRange.vo | 0m00.52s | 456608 ko || -0m00.01s || 208 ko | -1.92% | +0.04% 0m00.49s | 457600 ko | Util/ZRange/Operations.vo | 0m00.49s | 457296 ko || +0m00.00s || 304 ko | +0.00% | +0.06% 0m00.48s | 463388 ko | Rewriter/Language/UnderLets | 0m00.44s | 462668 ko || +0m00.03s || 720 ko | +9.09% | +0.15% 0m00.48s | 448820 ko | Rewriter/Util/MSetPositive/Facts | 0m00.45s | 448876 ko || +0m00.02s || -56 ko | +6.66% | -0.01% 0m00.48s | 447924 ko | Util/Strings/ParseArithmetic.vo | 0m00.42s | 447752 ko || +0m00.06s || 172 ko | +14.28% | +0.03% 0m00.48s | 399312 ko | Util/Sum.vo | 0m00.44s | 399236 ko || +0m00.03s || 76 ko | +9.09% | +0.01% 0m00.48s | 461668 ko | Util/ZUtil/Land.vo | 0m00.49s | 461648 ko || -0m00.01s || 20 ko | -2.04% | +0.00% 0m00.48s | 457784 ko | Util/ZUtil/ZSimplify/Simple.vo | 0m00.47s | 457944 ko || +0m00.01s || -160 ko | +2.12% | -0.03% 0m00.47s | 466976 ko | Language/PreExtra.vo | 0m00.43s | 466108 ko || +0m00.03s || 868 ko | +9.30% | +0.18% 0m00.47s | 467192 ko | Rewriter/TestRules.vo | 0m00.52s | 466692 ko || -0m00.05s || 500 ko | -9.61% | +0.10% 0m00.47s | 433340 ko | Spec/ModularArithmetic.vo | 0m00.45s | 432964 ko || +0m00.01s || 376 ko | +4.44% | +0.08% 0m00.46s | 467108 ko | Language/IdentifierParameters.vo | 0m00.49s | 467132 ko || -0m00.02s || -24 ko | -6.12% | -0.00% 0m00.46s | 442756 ko | Util/ZUtil/CPS.vo | 0m00.46s | 442392 ko || +0m00.00s || 364 ko | +0.00% | +0.08% 0m00.46s | 18624 ko | fiat-rust/src/curve25519_64.rs | 0m00.46s | 18668 ko || +0m00.00s || -44 ko | +0.00% | -0.23% 0m00.45s | 426612 ko | Util/MSetPositive/Equality.vo | 0m00.43s | 426676 ko || +0m00.02s || -64 ko | +4.65% | -0.01% 0m00.45s | 448700 ko | Util/Strings/Show.vo | 0m00.46s | 448700 ko || -0m00.01s || 0 ko | -2.17% | +0.00% 0m00.45s | 466180 ko | Util/ZUtil/EquivModulo.vo | 0m00.39s | 465912 ko || +0m00.06s || 268 ko | +15.38% | +0.05% 0m00.44s | 19088 ko | fiat-c/src/curve25519_64.c | 0m00.47s | 19112 ko || -0m00.02s || -24 ko | -6.38% | -0.12% 0m00.43s | 456472 ko | Util/AdditionChainExponentiation.vo | 0m00.43s | 456456 ko || +0m00.00s || 16 ko | +0.00% | +0.00% 0m00.42s | 489944 ko | Util/ZUtil.vo | 0m00.47s | 490408 ko || -0m00.04s || -464 ko | -10.63% | -0.09% 0m00.42s | 434532 ko | Util/ZUtil/Tactics/Ztestbit.vo | 0m00.45s | 434156 ko || -0m00.03s || 376 ko | -6.66% | +0.08% 0m00.41s | 468136 ko | Rewriter/TestRulesProofs.vo | 0m00.46s | 467840 ko || -0m00.05s || 296 ko | -10.86% | +0.06% 0m00.41s | 444612 ko | Util/Strings/StringMap.vo | 0m00.35s | 444700 ko || +0m00.06s || -88 ko | +17.14% | -0.01% 0m00.40s | 409472 ko | Util/ZUtil/Tactics.vo | 0m00.40s | 409456 ko || +0m00.00s || 16 ko | +0.00% | +0.00% 0m00.39s | 441504 ko | Util/NUtil/WithoutReferenceToZ.vo | 0m00.38s | 441556 ko || +0m00.01s || -52 ko | +2.63% | -0.01% 0m00.38s | 399680 ko | Algebra/Monoid.vo | 0m00.32s | 399440 ko || +0m00.06s || 240 ko | +18.75% | +0.06% 0m00.38s | 381368 ko | Util/ZUtil/Hints/Core.vo | 0m00.33s | 381528 ko || +0m00.04s || -160 ko | +15.15% | -0.04% 0m00.38s | 390940 ko | Util/ZUtil/Modulo/Bootstrap.vo | 0m00.35s | 390800 ko || +0m00.03s || 140 ko | +8.57% | +0.03% 0m00.38s | 413740 ko | Util/ZUtil/N2Z.vo | 0m00.36s | 414024 ko || +0m00.02s || -284 ko | +5.55% | -0.06% 0m00.37s | 403856 ko | Arithmetic/MontgomeryReduction/Definition.vo | 0m00.36s | 403972 ko || +0m00.01s || -116 ko | +2.77% | -0.02% 0m00.37s | 409928 ko | Util/Factorize.vo | 0m00.37s | 409748 ko || +0m00.00s || 180 ko | +0.00% | +0.04% 0m00.37s | 412560 ko | Util/IdfunWithAlt.vo | 0m00.33s | 412476 ko || +0m00.03s || 84 ko | +12.12% | +0.02% 0m00.37s | 381024 ko | Util/ZUtil/Hints.vo | 0m00.31s | 381084 ko || +0m00.06s || -60 ko | +19.35% | -0.01% 0m00.37s | 397340 ko | Util/ZUtil/Lor.vo | 0m00.40s | 397208 ko || -0m00.03s || 132 ko | -7.50% | +0.03% 0m00.37s | 395548 ko | Util/ZUtil/MulSplit.vo | 0m00.35s | 395928 ko || +0m00.02s || -380 ko | +5.71% | -0.09% 0m00.37s | 393360 ko | Util/ZUtil/Tactics/SimplifyFractionsLe.vo | 0m00.36s | 393388 ko || +0m00.01s || -28 ko | +2.77% | -0.00% 0m00.37s | 389948 ko | Util/ZUtil/Tactics/ZeroBounds.vo | 0m00.33s | 389884 ko || +0m00.03s || 64 ko | +12.12% | +0.01% 0m00.36s | 386508 ko | Bedrock/Field/Common/Names/VarnameGenerator.vo | 0m00.37s | 386720 ko || -0m00.01s || -212 ko | -2.70% | -0.05% 0m00.36s | 421340 ko | Util/ZRange/Show.vo | 0m00.39s | 421284 ko || -0m00.03s || 56 ko | -7.69% | +0.01% 0m00.36s | 378176 ko | Util/ZUtil/Div/Bootstrap.vo | 0m00.32s | 378420 ko || +0m00.03s || -244 ko | +12.49% | -0.06% 0m00.35s | 375992 ko | Util/MSets/Show.vo | 0m00.32s | 376044 ko || +0m00.02s || -52 ko | +9.37% | -0.01% 0m00.35s | 393164 ko | Util/ZUtil/DistrIf.vo | 0m00.36s | 392936 ko || -0m00.01s || 228 ko | -2.77% | +0.05% 0m00.35s | 412936 ko | Util/ZUtil/Sgn.vo | 0m00.37s | 413028 ko || -0m00.02s || -92 ko | -5.40% | -0.02% 0m00.35s | 377836 ko | Util/ZUtil/Tactics/PeelLe.vo | 0m00.35s | 377804 ko || +0m00.00s || 32 ko | +0.00% | +0.00% 0m00.35s | 383336 ko | Util/ZUtil/Tactics/PullPush/Modulo.vo | 0m00.35s | 383356 ko || +0m00.00s || -20 ko | +0.00% | -0.00% 0m00.34s | 378684 ko | Util/ZUtil/Tactics/DivModToQuotRem.vo | 0m00.35s | 378540 ko || -0m00.00s || 144 ko | -2.85% | +0.03% 0m00.34s | 383376 ko | Util/ZUtil/ZSimplify/Core.vo | 0m00.33s | 383204 ko || +0m00.01s || 172 ko | +3.03% | +0.04% 0m00.33s | 403064 ko | Rewriter/Language/PreLemmas | 0m00.31s | 400760 ko || +0m00.02s || 2304 ko | +6.45% | +0.57% 0m00.33s | 354496 ko | Util/ListUtil/SetoidList.vo | 0m00.29s | 354628 ko || +0m00.04s || -132 ko | +13.79% | -0.03% 0m00.33s | 387204 ko | Util/ZUtil/Hints/PullPush.vo | 0m00.34s | 386988 ko || -0m00.01s || 216 ko | -2.94% | +0.05% 0m00.33s | 376964 ko | Util/ZUtil/Hints/Ztestbit.vo | 0m00.35s | 376984 ko || -0m00.01s || -20 ko | -5.71% | -0.00% 0m00.33s | 349020 ko | Util/ZUtil/Lnot.vo | 0m00.30s | 348928 ko || +0m00.03s || 92 ko | +10.00% | +0.02% 0m00.33s | 369308 ko | Util/ZUtil/Pow2.vo | 0m00.34s | 369268 ko || -0m00.01s || 40 ko | -2.94% | +0.01% 0m00.33s | 341952 ko | Util/ZUtil/Tactics/SplitMinMax.vo | 0m00.29s | 342220 ko || +0m00.04s || -268 ko | +13.79% | -0.07% 0m00.33s | 382628 ko | Util/ZUtil/TruncatingShiftl.vo | 0m00.33s | 382584 ko || +0m00.00s || 44 ko | +0.00% | +0.01% 0m00.33s | 353940 ko | Util/ZUtil/ZSimplify.vo | 0m00.28s | 353788 ko || +0m00.04s || 152 ko | +17.85% | +0.04% 0m00.32s | 366280 ko | Util/ErrorT/Show.vo | 0m00.31s | 366704 ko || +0m00.01s || -424 ko | +3.22% | -0.11% 0m00.32s | 378836 ko | Util/ZUtil/Hints/ZArith.vo | 0m00.36s | 379152 ko || -0m00.03s || -316 ko | -11.11% | -0.08% 0m00.32s | 347740 ko | Util/ZUtil/Tactics/ReplaceNegWithPos.vo | 0m00.26s | 347612 ko || +0m00.06s || 128 ko | +23.07% | +0.03% 0m00.31s | 364064 ko | TAPSort.vo | 0m00.28s | 364028 ko || +0m00.02s || 36 ko | +10.71% | +0.00% 0m00.31s | 357148 ko | Util/ZUtil/Sorting.vo | 0m00.29s | 357164 ko || +0m00.02s || -16 ko | +6.89% | -0.00% 0m00.31s | 347952 ko | Util/ZUtil/Tactics/PullPush.vo | 0m00.36s | 347892 ko || -0m00.04s || 60 ko | -13.88% | +0.01% 0m00.30s | 312496 ko | Util/Option.vo | 0m00.26s | 312220 ko || +0m00.03s || 276 ko | +15.38% | +0.08% 0m00.30s | 352648 ko | Util/Strings/Parse/Common.vo | 0m00.30s | 352500 ko || +0m00.00s || 148 ko | +0.00% | +0.04% 0m00.30s | 401844 ko | Util/ZUtil/Z2Nat.vo | 0m00.34s | 401896 ko || -0m00.04s || -52 ko | -11.76% | -0.01% 0m00.28s | 373832 ko | Util/FMapPositive/Equality.vo | 0m00.27s | 373904 ko || +0m00.01s || -72 ko | +3.70% | -0.01% 0m00.28s | 344304 ko | Util/ZUtil/Mul.vo | 0m00.31s | 344004 ko || -0m00.02s || 300 ko | -9.67% | +0.08% 0m00.28s | 22008 ko | fiat-bedrock2/src/poly1305_32.c | 0m00.24s | 22360 ko || +0m00.04s || -352 ko | +16.66% | -1.57% 0m00.27s | 328148 ko | Util/ZUtil/Definitions.vo | 0m00.29s | 328260 ko || -0m00.01s || -112 ko | -6.89% | -0.03% 0m00.26s | 298284 ko | Util/SideConditions/ModInvPackage.vo | 0m00.25s | 298240 ko || +0m00.01s || 44 ko | +4.00% | +0.01% 0m00.26s | 321216 ko | Util/ZUtil/Zselect.vo | 0m00.26s | 321356 ko || +0m00.00s || -140 ko | +0.00% | -0.04% 0m00.25s | 311368 ko | Algebra/Hierarchy.vo | 0m00.23s | 311448 ko || +0m00.01s || -80 ko | +8.69% | -0.02% 0m00.25s | 328216 ko | Util/Structures/Equalities/Sum.vo | 0m00.23s | 328136 ko || +0m00.01s || 80 ko | +8.69% | +0.02% 0m00.25s | 340968 ko | Util/ZUtil/Tactics/DivideExistsMul.vo | 0m00.28s | 340960 ko || -0m00.03s || 8 ko | -10.71% | +0.00% 0m00.25s | 306328 ko | Util/ZUtil/Tactics/PrimeBound.vo | 0m00.25s | 306264 ko || +0m00.00s || 64 ko | +0.00% | +0.02% 0m00.24s | 312052 ko | Rewriter/Util/Option | 0m00.28s | 312008 ko || -0m00.04s || 44 ko | -14.28% | +0.01% 0m00.24s | 299600 ko | Util/SideConditions/RingPackage.vo | 0m00.24s | 299988 ko || +0m00.00s || -388 ko | +0.00% | -0.12% 0m00.24s | 306480 ko | Util/Strings/Decimal.vo | 0m00.24s | 306464 ko || +0m00.00s || 16 ko | +0.00% | +0.00% 0m00.24s | 311448 ko | Util/ZUtil/AddModulo.vo | 0m00.25s | 311524 ko || -0m00.01s || -76 ko | -4.00% | -0.02% 0m00.24s | 313680 ko | Util/ZUtil/Ge.vo | 0m00.28s | 313672 ko || -0m00.04s || 8 ko | -14.28% | +0.00% 0m00.24s | 306856 ko | Util/ZUtil/ModInv.vo | 0m00.24s | 306520 ko || +0m00.00s || 336 ko | +0.00% | +0.10% 0m00.24s | 18128 ko | fiat-java/src/FiatPoly1305.java | 0m00.23s | 18144 ko || +0m00.00s || -16 ko | +4.34% | -0.08% 0m00.23s | 18224 ko | fiat-rust/src/poly1305_32.rs | 0m00.21s | 18048 ko || +0m00.02s || 176 ko | +9.52% | +0.97% 0m00.22s | 296724 ko | PushButtonSynthesis/InvertHighLow.vo | 0m00.21s | 296844 ko || +0m00.01s || -120 ko | +4.76% | -0.04% 0m00.21s | 312000 ko | Util/PointedProp.vo | 0m00.22s | 312052 ko || -0m00.01s || -52 ko | -4.54% | -0.01% 0m00.21s | 279216 ko | Util/SideConditions/Autosolve.vo | 0m00.20s | 279412 ko || +0m00.00s || -196 ko | +4.99% | -0.07% 0m00.21s | 291692 ko | Util/ZUtil/Tactics/CompareToSgn.vo | 0m00.25s | 292044 ko || -0m00.04s || -352 ko | -16.00% | -0.12% 0m00.21s | 18068 ko | fiat-c/src/poly1305_32.c | 0m00.21s | 18156 ko || +0m00.00s || -88 ko | +0.00% | -0.48% 0m00.20s | 277664 ko | Spec/MxDH.vo | 0m00.21s | 277676 ko || -0m00.00s || -12 ko | -4.76% | -0.00% 0m00.20s | 264748 ko | Util/Decidable/Bool2Prop.vo | 0m00.22s | 264932 ko || -0m00.01s || -184 ko | -9.09% | -0.06% 0m00.20s | 304908 ko | Util/LetInMonad.vo | 0m00.17s | 304932 ko || +0m00.03s || -24 ko | +17.64% | -0.00% 0m00.20s | 353260 ko | Util/OptionList.vo | 0m00.21s | 353396 ko || -0m00.00s || -136 ko | -4.76% | -0.03% 0m00.20s | 250280 ko | Util/SideConditions/ReductionPackages.vo | 0m00.18s | 250464 ko || +0m00.02s || -184 ko | +11.11% | -0.07% 0m00.20s | 280072 ko | Util/Strings/Ascii.vo | 0m00.22s | 279800 ko || -0m00.01s || 272 ko | -9.09% | +0.09% 0m00.20s | 18244 ko | fiat-go/src/poly1305_32.go | 0m00.21s | 18208 ko || -0m00.00s || 36 ko | -4.76% | +0.19% 0m00.18s | 341096 ko | Rewriter/Util/OptionList | 0m00.20s | 341044 ko || -0m00.02s || 52 ko | -10.00% | +0.01% 0m00.17s | 306428 ko | Util/ListUtil/FoldBool.vo | 0m00.20s | 306476 ko || -0m00.03s || -48 ko | -15.00% | -0.01% 0m00.16s | 242032 ko | Util/Sigma.vo | 0m00.18s | 242080 ko || -0m00.01s || -48 ko | -11.11% | -0.01% 0m00.16s | 231268 ko | Util/ZUtil/Notations.vo | 0m00.15s | 230928 ko || +0m00.01s || 340 ko | +6.66% | +0.14% 0m00.15s | 242284 ko | Util/ParseTaps.vo | 0m00.16s | 242028 ko || -0m00.01s || 256 ko | -6.25% | +0.10% 0m00.15s | 18204 ko | fiat-go/src/poly1305_64.go | 0m00.15s | 17960 ko || +0m00.00s || 244 ko | +0.00% | +1.35% 0m00.14s | 221024 ko | Util/ListUtil/ForallIn.vo | 0m00.14s | 220872 ko || +0m00.00s || 152 ko | +0.00% | +0.06% 0m00.13s | 17164 ko | fiat-c/src/poly1305_64.c | 0m00.11s | 17440 ko || +0m00.02s || -276 ko | +18.18% | -1.58% 0m00.13s | 17160 ko | fiat-rust/src/poly1305_64.rs | 0m00.12s | 17356 ko || +0m00.01s || -196 ko | +8.33% | -1.12% 0m00.12s | 191024 ko | Util/Relations.vo | 0m00.11s | 191048 ko || +0m00.00s || -24 ko | +9.09% | -0.01% 0m00.12s | 19448 ko | fiat-bedrock2/src/poly1305_64.c | 0m00.12s | 19424 ko || +0m00.00s || 24 ko | +0.00% | +0.12% 0m00.11s | 194124 ko | Util/Prod.vo | 0m00.10s | 194228 ko || +0m00.00s || -104 ko | +9.99% | -0.05% 0m00.10s | 204472 ko | Rewriter/Util/ListUtil/SetoidList | 0m00.12s | 204308 ko || -0m00.01s || 164 ko | -16.66% | +0.08% 0m00.10s | 158600 ko | Util/PrimitiveHList.vo | 0m00.11s | 158756 ko || -0m00.00s || -156 ko | -9.09% | -0.09% 0m00.10s | 199408 ko | Util/PrimitiveProd.vo | 0m00.12s | 199296 ko || -0m00.01s || 112 ko | -16.66% | +0.05% 0m00.10s | 166896 ko | Util/PrimitiveSigma.vo | 0m00.12s | 167204 ko || -0m00.01s || -308 ko | -16.66% | -0.18% 0m00.09s | 147140 ko | Util/Equality.vo | 0m00.08s | 147316 ko || +0m00.00s || -176 ko | +12.49% | -0.11% 0m00.09s | 158592 ko | Util/TagList.vo | 0m00.10s | 158664 ko || -0m00.01s || -72 ko | -10.00% | -0.04% 0m00.08s | 135808 ko | Rewriter/Util/Bool | 0m00.07s | 118980 ko || +0m00.00s || 16828 ko | +14.28% | +14.14% 0m00.08s | 119876 ko | Util/Structures/Equalities/Iso.vo | 0m00.08s | 119912 ko || +0m00.00s || -36 ko | +0.00% | -0.03% 0m00.07s | 123196 ko | Util/Bool.vo | 0m00.08s | 123348 ko || -0m00.00s || -152 ko | -12.49% | -0.12% 0m00.07s | 119880 ko | Util/Sigma/Related.vo | 0m00.08s | 119684 ko || -0m00.00s || 196 ko | -12.49% | +0.16% 0m00.07s | 107652 ko | Util/Structures/Orders/Iso.vo | 0m00.05s | 107736 ko || +0m00.02s || -84 ko | +40.00% | -0.07% 0m00.07s | 76340 ko | Util/Tactics/BreakMatch.vo | 0m00.05s | 76416 ko || +0m00.02s || -76 ko | +40.00% | -0.09% 0m00.07s | 91756 ko | Util/Tactics/RewriteHyp.vo | 0m00.05s | 91720 ko || +0m00.02s || 36 ko | +40.00% | +0.03% 0m00.06s | 95556 ko | Util/HProp.vo | 0m00.06s | 95364 ko || +0m00.00s || 192 ko | +0.00% | +0.20% 0m00.06s | 94868 ko | Util/LetIn.vo | 0m00.06s | 94964 ko || +0m00.00s || -96 ko | +0.00% | -0.10% 0m00.06s | 75736 ko | Util/Logic/Exists.vo | 0m00.05s | 75752 ko || +0m00.00s || -16 ko | +19.99% | -0.02% 0m00.06s | 103632 ko | Util/Logic/ExistsEqAnd.vo | 0m00.04s | 103452 ko || +0m00.01s || 180 ko | +49.99% | +0.17% 0m00.06s | 89324 ko | Util/Pointed.vo | 0m00.06s | 89228 ko || +0m00.00s || 96 ko | +0.00% | +0.10% 0m00.05s | 60864 ko | Rewriter/Util/Tactics/SetoidSubst | N/A | N/A || +0m00.05s || 60864 ko | ∞ | ∞ 0m00.05s | 84512 ko | Util/AutoRewrite.vo | 0m00.05s | 84580 ko || +0m00.00s || -68 ko | +0.00% | -0.08% 0m00.05s | 78408 ko | Util/ErrorT.vo | 0m00.05s | 78544 ko || +0m00.00s || -136 ko | +0.00% | -0.17% 0m00.05s | 85792 ko | Util/IffT.vo | 0m00.05s | 85876 ko || +0m00.00s || -84 ko | +0.00% | -0.09% 0m00.05s | 66152 ko | Util/Isomorphism.vo | 0m00.04s | 66004 ko || +0m00.01s || 148 ko | +25.00% | +0.22% 0m00.05s | 88632 ko | Util/Logic.vo | 0m00.04s | 88616 ko || +0m00.01s || 16 ko | +25.00% | +0.01% 0m00.05s | 84968 ko | Util/Notations.vo | 0m00.06s | 84712 ko || -0m00.00s || 256 ko | -16.66% | +0.30% 0m00.05s | 67276 ko | Util/Sigma/Associativity.vo | 0m00.05s | 67432 ko || +0m00.00s || -156 ko | +0.00% | -0.23% 0m00.05s | 84860 ko | Util/Sigma/Lift.vo | 0m00.06s | 84796 ko || -0m00.00s || 64 ko | -16.66% | +0.07% 0m00.05s | 93300 ko | Util/Structures/Orders.vo | 0m00.04s | 93036 ko || +0m00.01s || 264 ko | +25.00% | +0.28% 0m00.05s | 89652 ko | Util/Sumbool.vo | 0m00.05s | 89492 ko || +0m00.00s || 160 ko | +0.00% | +0.17% 0m00.05s | 83980 ko | Util/Tactics.vo | 0m00.05s | 83844 ko || +0m00.00s || 136 ko | +0.00% | +0.16% 0m00.05s | 67684 ko | Util/Tactics/CacheTerm.vo | 0m00.04s | 67732 ko || +0m00.01s || -48 ko | +25.00% | -0.07% 0m00.05s | 72532 ko | Util/Tactics/DebugPrint.vo | 0m00.05s | 72636 ko || +0m00.00s || -104 ko | +0.00% | -0.14% 0m00.05s | 72148 ko | Util/Tactics/RunTacticAsConstr.vo | 0m00.04s | 72360 ko || +0m00.01s || -212 ko | +25.00% | -0.29% 0m00.05s | 72132 ko | Util/Tactics/SpecializeAllWays.vo | 0m00.03s | 72336 ko || +0m00.02s || -204 ko | +66.66% | -0.28% 0m00.05s | 72732 ko | Util/Tactics/UniquePose.vo | 0m00.04s | 72788 ko || +0m00.01s || -56 ko | +25.00% | -0.07% 0m00.05s | 85432 ko | Util/Tower.vo | 0m00.05s | 85656 ko || +0m00.00s || -224 ko | +0.00% | -0.26% 0m00.04s | 75260 ko | Util/Bool/Equality.vo | 0m00.05s | 75536 ko || -0m00.01s || -276 ko | -20.00% | -0.36% 0m00.04s | 79324 ko | Util/CPSNotations.vo | 0m00.05s | 79172 ko || -0m00.01s || 152 ko | -20.00% | +0.19% 0m00.04s | 79036 ko | Util/Comparison.vo | 0m00.05s | 78824 ko || -0m00.01s || 212 ko | -20.00% | +0.26% 0m00.04s | 102732 ko | Util/Compose.vo | 0m00.07s | 102824 ko || -0m00.03s || -92 ko | -42.85% | -0.08% 0m00.04s | 78808 ko | Util/FixCoqMistakes.vo | 0m00.06s | 78540 ko || -0m00.01s || 268 ko | -33.33% | +0.34% 0m00.04s | 65548 ko | Util/FueledLUB.vo | 0m00.03s | 65640 ko || +0m00.01s || -92 ko | +33.33% | -0.14% 0m00.04s | 77960 ko | Util/Logic/Forall.vo | 0m00.04s | 77776 ko || +0m00.00s || 184 ko | +0.00% | +0.23% 0m00.04s | 72304 ko | Util/Logic/ImplAnd.vo | 0m00.04s | 72240 ko || +0m00.00s || 64 ko | +0.00% | +0.08% 0m00.04s | 85456 ko | Util/Logic/ProdForall.vo | 0m00.04s | 85556 ko || +0m00.00s || -100 ko | +0.00% | -0.11% 0m00.04s | 76140 ko | Util/PER.vo | 0m00.04s | 76444 ko || +0m00.00s || -304 ko | +0.00% | -0.39% 0m00.04s | 74064 ko | Util/SideConditions/CorePackages.vo | 0m00.05s | 73972 ko || -0m00.01s || 92 ko | -20.00% | +0.12% 0m00.04s | 66984 ko | Util/Sigma/MapProjections.vo | 0m00.02s | 66896 ko || +0m00.02s || 88 ko | +100.00% | +0.13% 0m00.04s | 64764 ko | Util/Tactics/ClearAll.vo | 0m00.03s | 64880 ko || +0m00.01s || -116 ko | +33.33% | -0.17% 0m00.04s | 64688 ko | Util/Tactics/ClearbodyAll.vo | 0m00.04s | 64796 ko || +0m00.00s || -108 ko | +0.00% | -0.16% 0m00.04s | 64840 ko | Util/Tactics/Contains.vo | 0m00.03s | 64752 ko || +0m00.01s || 88 ko | +33.33% | +0.13% 0m00.04s | 65852 ko | Util/Tactics/ConvoyDestruct.vo | 0m00.03s | 65884 ko || +0m00.01s || -32 ko | +33.33% | -0.04% 0m00.04s | 80636 ko | Util/Tactics/DestructHead.vo | 0m00.05s | 80696 ko || -0m00.01s || -60 ko | -20.00% | -0.07% 0m00.04s | 64920 ko | Util/Tactics/DestructTrivial.vo | 0m00.03s | 64916 ko || +0m00.01s || 4 ko | +33.33% | +0.00% 0m00.04s | 72504 ko | Util/Tactics/DoWithHyp.vo | 0m00.05s | 72588 ko || -0m00.01s || -84 ko | -20.00% | -0.11% 0m00.04s | 64612 ko | Util/Tactics/ESpecialize.vo | 0m00.04s | 64644 ko || +0m00.00s || -32 ko | +0.00% | -0.04% 0m00.04s | 64896 ko | Util/Tactics/EvarNormalize.vo | 0m00.03s | 64924 ko || +0m00.01s || -28 ko | +33.33% | -0.04% 0m00.04s | 64508 ko | Util/Tactics/GetGoal.vo | 0m00.03s | 64724 ko || +0m00.01s || -216 ko | +33.33% | -0.33% 0m00.04s | 64732 ko | Util/Tactics/HasBody.vo | 0m00.03s | 64520 ko || +0m00.01s || 212 ko | +33.33% | +0.32% 0m00.04s | 72232 ko | Util/Tactics/Head.vo | 0m00.04s | 72188 ko || +0m00.00s || 44 ko | +0.00% | +0.06% 0m00.04s | 72660 ko | Util/Tactics/HeadUnderBinders.vo | 0m00.05s | 72676 ko || -0m00.01s || -16 ko | -20.00% | -0.02% 0m00.04s | 65236 ko | Util/Tactics/NormalizeCommutativeIdentifier.vo | 0m00.05s | 65096 ko || -0m00.01s || 140 ko | -20.00% | +0.21% 0m00.04s | 64884 ko | Util/Tactics/Not.vo | 0m00.03s | 64796 ko || +0m00.01s || 88 ko | +33.33% | +0.13% 0m00.04s | 64928 ko | Util/Tactics/PoseTermWithName.vo | 0m00.04s | 65156 ko || +0m00.00s || -228 ko | +0.00% | -0.34% 0m00.04s | 64788 ko | Util/Tactics/SetEvars.vo | 0m00.04s | 64780 ko || +0m00.00s || 8 ko | +0.00% | +0.01% 0m00.04s | 65124 ko | Util/Tactics/SideConditionsBeforeToAfter.vo | 0m00.04s | 65044 ko || +0m00.00s || 80 ko | +0.00% | +0.12% 0m00.04s | 64876 ko | Util/Tactics/SubstEvars.vo | 0m00.03s | 64828 ko || +0m00.01s || 48 ko | +33.33% | +0.07% 0m00.04s | 64688 ko | Util/Tactics/SubstLet.vo | 0m00.04s | 64844 ko || +0m00.00s || -156 ko | +0.00% | -0.24% 0m00.04s | 64620 ko | Util/Tactics/Test.vo | 0m00.04s | 64780 ko || +0m00.00s || -160 ko | +0.00% | -0.24% 0m00.04s | 65740 ko | Util/Tactics/VM.vo | 0m00.04s | 65724 ko || +0m00.00s || 16 ko | +0.00% | +0.02% 0m00.04s | 73192 ko | Util/Unit.vo | 0m00.03s | 73336 ko || +0m00.01s || -144 ko | +33.33% | -0.19% 0m00.03s | 59656 ko | Rewriter/Util/Tactics/Contains | N/A | N/A || +0m00.03s || 59656 ko | ∞ | ∞ 0m00.03s | 66852 ko | Util/Bool/IsTrue.vo | 0m00.05s | 66956 ko || -0m00.02s || -104 ko | -40.00% | -0.15% 0m00.03s | 68620 ko | Util/Curry.vo | 0m00.03s | 68652 ko || +0m00.00s || -32 ko | +0.00% | -0.04% 0m00.03s | 64912 ko | Util/DefaultedTypes.vo | 0m00.04s | 64964 ko || -0m00.01s || -52 ko | -25.00% | -0.08% 0m00.03s | 64156 ko | Util/GlobalSettings.vo | 0m00.03s | 64432 ko || +0m00.00s || -276 ko | +0.00% | -0.42% 0m00.03s | 66872 ko | Util/Pos.vo | 0m00.04s | 66736 ko || -0m00.01s || 136 ko | -25.00% | +0.20% 0m00.03s | 67260 ko | Util/Tactics/CPSId.vo | 0m00.03s | 67148 ko || +0m00.00s || 112 ko | +0.00% | +0.16% 0m00.03s | 64936 ko | Util/Tactics/ChangeInAll.vo | 0m00.03s | 65048 ko || +0m00.00s || -112 ko | +0.00% | -0.17% 0m00.03s | 64740 ko | Util/Tactics/ConstrFail.vo | 0m00.04s | 64888 ko || -0m00.01s || -148 ko | -25.00% | -0.22% 0m00.03s | 74172 ko | Util/Tactics/DestructHyps.vo | 0m00.05s | 74004 ko || -0m00.02s || 168 ko | -40.00% | +0.22% 0m00.03s | 64980 ko | Util/Tactics/EvarExists.vo | 0m00.04s | 64996 ko || -0m00.01s || -16 ko | -25.00% | -0.02% 0m00.03s | 65752 ko | Util/Tactics/Forward.vo | 0m00.03s | 65496 ko || +0m00.00s || 256 ko | +0.00% | +0.39% 0m00.03s | 76596 ko | Util/Tactics/MoveLetIn.vo | 0m00.06s | 76700 ko || -0m00.03s || -104 ko | -50.00% | -0.13% 0m00.03s | 64952 ko | Util/Tactics/OnSubterms.vo | 0m00.04s | 64712 ko || -0m00.01s || 240 ko | -25.00% | +0.37% 0m00.03s | 65040 ko | Util/Tactics/PrintContext.vo | 0m00.03s | 65036 ko || +0m00.00s || 4 ko | +0.00% | +0.00% 0m00.03s | 65332 ko | Util/Tactics/PrintGoal.vo | 0m00.02s | 65228 ko || +0m00.00s || 104 ko | +49.99% | +0.15% 0m00.03s | 65008 ko | Util/Tactics/Revert.vo | 0m00.04s | 64832 ko || -0m00.01s || 176 ko | -25.00% | +0.27% 0m00.03s | 66268 ko | Util/Tactics/SetoidSubst.vo | 0m00.05s | 66592 ko || -0m00.02s || -324 ko | -40.00% | -0.48% 0m00.03s | 65964 ko | Util/Tactics/SimplifyProjections.vo | 0m00.03s | 65832 ko || +0m00.00s || 132 ko | +0.00% | +0.20% 0m00.03s | 73564 ko | Util/Tactics/SplitInContext.vo | 0m00.05s | 73456 ko || -0m00.02s || 108 ko | -40.00% | +0.14% 0m00.03s | 65724 ko | Util/Tactics/TransparentAssert.vo | 0m00.02s | 65432 ko || +0m00.00s || 292 ko | +49.99% | +0.44% 0m00.03s | 65360 ko | Util/Tactics/UnfoldArg.vo | 0m00.04s | 65432 ko || -0m00.01s || -72 ko | -25.00% | -0.11% 0m00.03s | 66392 ko | Util/Tactics/UnifyAbstractReflexivity.vo | 0m00.05s | 66432 ko || -0m00.02s || -40 ko | -40.00% | -0.06% 0m00.02s | 65188 ko | Util/Tactics/ClearDuplicates.vo | 0m00.04s | 65024 ko || -0m00.02s || 164 ko | -50.00% | +0.25% 0m00.02s | 70432 ko | Util/Tactics/ETransitivity.vo | 0m00.03s | 70404 ko || -0m00.00s || 28 ko | -33.33% | +0.03% 0m00.02s | 65388 ko | Util/Tactics/SimplifyRepeatedIfs.vo | 0m00.04s | 65448 ko || -0m00.02s || -60 ko | -50.00% | -0.09% 0m00.02s | 73068 ko | Util/Tactics/SpecializeBy.vo | 0m00.03s | 73016 ko || -0m00.00s || 52 ko | -33.33% | +0.07% 0m00.01s | 65004 ko | Util/ChangeInAll.vo | 0m00.06s | 64676 ko || -0m00.05s || 328 ko | -83.33% | +0.50% ``` </p> 17 August 2020, 20:53:15 UTC
741066c Jason Gross 12 August 2020, 17:56:39 UTC Improve bedrock2 rewrite rules We now handle the case of carry/borrow being 0 specially, so we now no longer need `-Wno-error=tautological-compare` Fixes #769 16 August 2020, 23:07:28 UTC
af78b89 Jason Gross 12 August 2020, 17:05:55 UTC Reindent to minimize diff in the next commit 16 August 2020, 23:07:28 UTC
2111394 jadep 14 August 2020, 10:16:47 UTC comment out two admitted, unused lemmas 15 August 2020, 09:22:39 UTC
aaa359f jadep 14 August 2020, 10:14:08 UTC remove two admitted, unused lemmas 15 August 2020, 09:22:39 UTC
486738b jadep 11 August 2020, 09:50:53 UTC use Syntax.func instead of bedrock_func notation 14 August 2020, 12:56:46 UTC
d5b5206 Jason Gross 13 August 2020, 16:18:50 UTC Move Forall lemmas to Forall.v 13 August 2020, 16:18:50 UTC
c0afb99 Jason Gross 13 August 2020, 16:13:28 UTC Add some Forall2 lemmas 13 August 2020, 16:13:28 UTC
9f08fb6 jadep 12 August 2020, 15:05:19 UTC update rupicola version 12 August 2020, 19:09:17 UTC
484cc36 jadep 12 August 2020, 09:06:52 UTC use bedrock2 prelude 12 August 2020, 19:09:17 UTC
882b1e8 jadep 12 August 2020, 08:15:26 UTC new bedrock2 printing-as-C structure 12 August 2020, 19:09:17 UTC
2e1d7a3 jadep 11 August 2020, 19:44:48 UTC revert change to CI deps task 12 August 2020, 19:09:17 UTC
d78c2c9 jadep 11 August 2020, 19:43:01 UTC bump rupicola version 12 August 2020, 19:09:17 UTC
7aa44f1 jadep 11 August 2020, 08:49:06 UTC update LadderStep.v to match latest bedrock2 version 12 August 2020, 19:09:17 UTC
e34cec1 jadep 10 August 2020, 18:34:36 UTC remove to_c_parameters (to match bedrock2 updates) 12 August 2020, 19:09:17 UTC
c2d85d1 jadep 10 August 2020, 14:40:22 UTC add rupicola to dir-locals.el 12 August 2020, 19:09:17 UTC
9d85558 jadep 10 August 2020, 12:24:20 UTC add rupicola to COQPATH 12 August 2020, 19:09:17 UTC
4750d38 jadep 07 August 2020, 14:53:41 UTC make deps task run regular make (instead of make with timing and git diff) 12 August 2020, 19:09:17 UTC
3aa9274 jadep 07 August 2020, 11:25:55 UTC update rupicola to get compatible bedrock2 version 12 August 2020, 19:09:17 UTC
3d9ba25 jadep 07 August 2020, 11:13:26 UTC point to rupicola's bedrock2 submodule 12 August 2020, 19:09:17 UTC
a5f302c jadep 07 August 2020, 11:11:48 UTC remove bedrock2 direct submodule 12 August 2020, 19:09:17 UTC
3b0c948 jadep 07 August 2020, 11:05:56 UTC add rupicola targets to Makefile 12 August 2020, 19:09:17 UTC
98b4520 jadep 07 August 2020, 11:01:42 UTC add rupicola submodule 12 August 2020, 19:09:17 UTC
580a5b1 Jason Gross 12 August 2020, 18:19:36 UTC Update README.md Mention ocamlfind. The text could possibly be better. Closes #781 12 August 2020, 18:19:36 UTC
fbd1a1f Jason Gross 12 August 2020, 18:11:19 UTC Update README.md We now document how to increase the stack size, fixing #825 12 August 2020, 18:11:19 UTC
67b7762 Jason Gross 12 August 2020, 17:18:06 UTC Test for --output-sync on CI Mac OS apparently doesn't support it 12 August 2020, 17:18:06 UTC
aae3116 Jason Gross 09 August 2020, 17:35:50 UTC Also test Coq 8.12 09 August 2020, 17:35:50 UTC
c290142 Andres Erbsen 08 August 2020, 21:09:18 UTC Merge branch 'reorganize-bedrock2_2' into master 08 August 2020, 21:09:18 UTC
2b7d738 Andres Erbsen 08 August 2020, 21:09:11 UTC bedrock2 translation readme: minor rewording 08 August 2020, 21:09:11 UTC
7617a09 Jason Gross 07 August 2020, 19:10:17 UTC Generalize the nth_default proof of encode_distributed 08 August 2020, 02:21:20 UTC
942fa68 Jason Gross 07 August 2020, 16:40:23 UTC Revert revert revert get_balances.expected file 08 August 2020, 02:21:20 UTC
cb1364a Jason Gross 07 August 2020, 16:39:19 UTC Revert "Revert "Use the redistributive algorithm for balance"" This reverts commit a3b5e8d0937f6864eef92d9ea4c457797c28276a. With the new commit, things should work fine. 08 August 2020, 02:21:20 UTC
8dafdfc jadep 06 August 2020, 10:57:12 UTC fix index order in distribute_balance 08 August 2020, 02:21:20 UTC
0321c27 Jason Gross 05 August 2020, 18:51:52 UTC Revert "Use the redistributive algorithm for balance" This reverts commit eb8346049efe2a5b4244152b691aaa68b287ed91. It was computing incorrect balance for some primes. 08 August 2020, 02:21:20 UTC
1c7d5fe Jason Gross 05 August 2020, 18:09:13 UTC Use the redistributive algorithm for balance As per the consenus of the group meeting. Unfortunately, this algorithm computes incorrect balance for some primes (leaving over negative limbs), as seen in the changes to the test-suite. If the algorithm worked as expected, I believe the two algorithms would give exactly the same answer in all cases where their evaluation is equal and the input does not exceed the maximum of the weight and lower-bound in any limb except possibly the highest one. (This last condition morally says that we have not already rebalanced for a larger minimum value.) Here is my argument: The specification of the algorithm of #857 (henceforth algorithm (1)) is that it computes the minimum value that each limb can have subject to the following constraints: 1. the overall evaluation must equal that of the input 2. each limb must be greater than or equal to the specified lower bound 3. each limb remains unchanged iff, after borrowing what's necessary for the lower limbs from the current limb, the current limb is already above the minimum value. The specification of the algorithm of #860 (henceforth algorithm (2)) is that it computes limbwise the number: ``` partition (eval (input - minvalues) mod p) + minvalues ``` The intuition is that both algorithms in fact compute the minimum possible borrow for each limb. The argument: Note that if both algorithms give results that evaluate to the same value, then both algorithms can be expressed as borrowing some amount from each non-lowest-limb to add into the next-lower-limb, by the properties of modular arithmetic (in particular that `x = x / d + x mod d` for every `x` and any positive `d`). Then the two algorithms compute different limbs iff they borrow different amounts from some limb to add to the next-lower-limb. Suppose, for contradiction, that there is a such a limb. Say that the lowest such limb has index `i+1`, and that (1) borrows `b1` from limb `i+1` for limb `i`, while (2) borrows `b2` from limb `i+1` to add to limb `i`. Let us compute the output limbs of (2). By the specification of `partition`, limb `i` of the output of (2) is equal to ``` minvalues[i] + (eval(input - minvalues) mod p) mod (weight(i+1)) / weight i ``` The assumption that the evaluations of (1) and (2) are equal is the assumption that `eval(input - minvalues)` is already reduced modulo `p`. Hence we have that limb `i` of the output of (2) is equal to ``` minvalues[i] + eval(input - minvalues) mod (weight(i+1)) / weight i ``` Since `(x mod weight(i+1)) / weight i` is less than `weight(i+1) / weight i`, we have that the amount we add to `minvalues[i]` is at most 1 more than we would need to borrow to get exactly `minvalues[i]`. Furthermore, if we can get exactly `minvalues[i]` by borrowing some amount, then we borrow exactly that amount, and not more, because the remainder will be smaller than `weight i` in that case. Hence if we borrowed any less than `b2`, then we'd end up with something less than `minvalues[i]`. By the constraints on (1), `b1 ≤ b2`. Hence `b1 = b2`, in violation of our assumption that they differ in this limb. Qed 08 August 2020, 02:21:20 UTC
2ca8318 Jason Gross 05 August 2020, 17:18:27 UTC Add Jade's version of redistributing balance From #857 08 August 2020, 02:21:20 UTC
21d12e0 Jason Gross 05 August 2020, 17:05:31 UTC Move encode_distributed to UnsaturatedSolinasHeuristics As per Jade's request 08 August 2020, 02:21:20 UTC
b76a81d Jason Gross 03 August 2020, 21:19:32 UTC Generalized sub/opp balance for unsaturated solinas Alternative to #857. Rather than redistributing an existing encoding, this version simply encodes a number using `partition` that, when added to the relevant bounds on a limb-by-limb basis without carrying, gives something which evaluates to the desired result. The limb-by-limb addition ensures the bounds we want, and the encoding scheme ensures the correct value. Furthermore, we don't need to know ahead-of-time how many copies of the prime we need to add. This is pleasingly simple to me. Additionally, as in #857, the tweak to make `to_bytes` work for p224 (and other primes with low limbs) and unsaturated solinas. The tweak here is a bit uglier than in #857, because balancing here doesn't guarantee the same value under `eval`, only something congruent to that value. So we need to ensure that we're encoding at least one copy of the prime. 08 August 2020, 02:21:20 UTC
2f09403 jadep 06 August 2020, 13:28:47 UTC fix references in WordByWordMontgomery.v 07 August 2020, 11:00:05 UTC
e8d66da jadep 06 August 2020, 10:26:06 UTC fix path in Makefile 07 August 2020, 11:00:05 UTC
7d84a7a jadep 04 August 2020, 10:54:19 UTC update READMEs 07 August 2020, 11:00:05 UTC
53f3cfb jadep 04 August 2020, 07:50:20 UTC fix imports 07 August 2020, 11:00:05 UTC
79414a0 jadep 04 August 2020, 07:39:12 UTC move Bedrock/Proofs and Bedrock/Parameters to Bedrock/Field/Translation 07 August 2020, 11:00:05 UTC
4e7848b jadep 04 August 2020, 07:35:58 UTC add and populate Bedrock/Field/Common 07 August 2020, 11:00:05 UTC
cefa5ae jadep 04 August 2020, 07:31:54 UTC make Bedrock/Field/Synthesis 07 August 2020, 11:00:05 UTC
3427cc5 jadep 04 August 2020, 07:29:12 UTC update-_CoqProject 07 August 2020, 11:00:05 UTC
eabfff3 jadep 04 August 2020, 07:28:53 UTC move Bedrock/Synthesis -> Bedrock/Field/Specialized and Bedrock/Synthesis/Examples -> Bedrock/Field/Examples 07 August 2020, 11:00:05 UTC
e775a75 jadep 23 July 2020, 11:00:30 UTC update _CoqProject 07 August 2020, 11:00:05 UTC
bfcf251 jadep 22 July 2020, 15:28:35 UTC move Translation/ and Generic/ to Field and fix imports 07 August 2020, 11:00:05 UTC
087ea49 jadep 22 July 2020, 15:22:20 UTC rename Bedrock/Field 07 August 2020, 11:00:05 UTC
1c74e32 jadep 22 July 2020, 15:20:53 UTC create Standalone/ directory and move some files 07 August 2020, 11:00:05 UTC
3ed760e Jason Gross 05 August 2020, 17:30:55 UTC Factor out definition of weight in UnsaturatedSolinasHeuristics 05 August 2020, 17:30:55 UTC
74547cc Jason Gross 05 August 2020, 17:22:03 UTC Don't unfold balance in tight_bounds_tighter 05 August 2020, 17:24:05 UTC
99e92eb Jason Gross 03 August 2020, 21:19:32 UTC Move some length lemmas to UnsaturatedSolinasHeuristics Also add them to a hint db 05 August 2020, 15:16:07 UTC
038f554 Jason Gross 03 August 2020, 21:17:49 UTC Add nth_default_partition_full to hintdb This requires adjusting a proof that relied on the absence of this rewriting 05 August 2020, 15:15:38 UTC
16d02ed Jason Gross 03 August 2020, 21:15:12 UTC Add some lemmas to NatUtil and ListUtil 05 August 2020, 15:15:38 UTC
98cb402 Jason Gross 29 July 2020, 16:03:26 UTC Update .mailmap 29 July 2020, 16:03:26 UTC
e9ff2d0 Jason Gross 28 July 2020, 18:29:39 UTC Fix unintentional catch-all cases in Rust, Go, and Java 28 July 2020, 18:29:39 UTC
a297577 Jason Gross 28 July 2020, 01:35:41 UTC Generate value_barrier wrappers for cmovznz code This is significant progress towards #748 Note that rather than checking for whether or not `OPENSSL_NO_ASM` is defined, we instead check for the definition of a curve-specific `*_NO_ASM` variable, where the prefix is the uppercased prefix of the curve description. This lets us not be tied to OpenSSL. (I presume that BoringSSL can do something like ```c #ifdef OPENSSL_NO_ASM #define FIAT_25519_NO_ASM #define FIAT_P256_NO_ASM [...] #endif ``` ) 28 July 2020, 17:29:56 UTC
9a54a82 Jason Gross 27 July 2020, 19:15:36 UTC Update README.md 27 July 2020, 19:15:36 UTC
27beeb1 jadep 24 July 2020, 17:58:06 UTC update possible limbs output test 27 July 2020, 09:20:58 UTC
back to top