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
32b3d8f jadep 28 July 2020, 11:34:51 UTC add length/eval lemmas so build works, fix up comments 28 July 2020, 11:34:51 UTC
1823a19 jadep 24 July 2020, 17:15:04 UTC WIP : add add_balance operation and use it in carry; try an algorithm for reduce_balance coefficient 28 July 2020, 10:59:11 UTC
d8b1e61 jadep 24 July 2020, 11:48:25 UTC WIP: generalize distribute_balance over lower bounds 27 July 2020, 09:24:28 UTC
49779ee jadep 23 July 2020, 15:11:45 UTC tweak balance-distribution algorithm 27 July 2020, 09:24:28 UTC
63aaa01 jadep 23 July 2020, 14:45:11 UTC generalize definition of distribute_balance and use it to distribute m_enc for freeze 27 July 2020, 09:24:28 UTC
7295086 jadep 23 July 2020, 13:00:07 UTC remove comment 27 July 2020, 09:24:28 UTC
7e7b2d7 jadep 23 July 2020, 12:56:58 UTC opp bounds fixed, carry and to_bytes still broken 27 July 2020, 09:24:28 UTC
eeb832c jadep 23 July 2020, 10:59:27 UTC WIP: first stab at new balance algorithm 27 July 2020, 09:24:28 UTC
27beeb1 jadep 24 July 2020, 17:58:06 UTC update possible limbs output test 27 July 2020, 09:20:58 UTC
a6de05c jadep 24 July 2020, 16:00:28 UTC regenerate bedrock2 files 27 July 2020, 09:20:58 UTC
a169681 jadep 24 July 2020, 14:36:15 UTC regenerate rust and java files 27 July 2020, 09:20:58 UTC
ed08034 jadep 24 July 2020, 14:16:17 UTC regenerate go files 27 July 2020, 09:20:58 UTC
7ca572d jadep 24 July 2020, 12:22:31 UTC change tight bounds computation 27 July 2020, 09:20:58 UTC
be3db06 Jason Gross 26 July 2020, 21:58:08 UTC Regenerate generated files 26 July 2020, 21:58:08 UTC
37daa2d Jason Gross 26 July 2020, 21:02:04 UTC Add some constant-folding rules for Z.{land,lor} 26 July 2020, 21:02:23 UTC
abd0a4b jadep 24 July 2020, 11:49:58 UTC remove extra space after 1s 24 July 2020, 14:33:16 UTC
f71bd4f jadep 22 July 2020, 13:42:12 UTC [ci] skip bedrock2 for 8.10 targets (bedrock2 does not support 8.10 and recent updates break it 24 July 2020, 14:33:16 UTC
e570217 jadep 22 July 2020, 11:31:28 UTC update bedrock2 and replace uses of Bedrock/Util lemmas that have been upstreamed to coqutil 24 July 2020, 14:33:16 UTC
091377d Jason Gross 22 July 2020, 19:10:50 UTC Parameterize sub over balance, not coef This is the infrastructure work towards dealing with issues like #554 (at least the part involving balance in sub and opp). Still to come is the more general way of computing balance. 23 July 2020, 14:08:49 UTC
4436097 jadep 21 July 2020, 16:09:56 UTC regenerate bedrock2 files 22 July 2020, 11:28:50 UTC
43c1da0 jadep 21 July 2020, 15:59:05 UTC regenerate rust files 22 July 2020, 11:28:50 UTC
0c3959d jadep 21 July 2020, 15:56:46 UTC regenerate go files 22 July 2020, 11:28:50 UTC
9442e0f jadep 21 July 2020, 15:33:25 UTC regenerate java files 22 July 2020, 11:28:50 UTC
56d032f jadep 21 July 2020, 15:06:48 UTC regenerate c files 22 July 2020, 11:28:50 UTC
8cf2437 jadep 21 July 2020, 10:09:12 UTC incorporate feedback from Jason 22 July 2020, 11:28:50 UTC
508758c jadep 10 July 2020, 10:38:32 UTC change Columns.flatten to add the last column's carry first, which helps keep sum accumulator small 22 July 2020, 11:28:50 UTC
3351c4d jadep 09 July 2020, 17:31:10 UTC reverse columns so small numbers are added first, reducing the need for truncation 22 July 2020, 11:28:50 UTC
9d9b8f8 jadep 09 July 2020, 15:51:09 UTC WIP: new land bounds 22 July 2020, 11:28:50 UTC
0d5afd8 jadep 08 July 2020, 12:04:45 UTC remove now-unneeded nth_default proofs and chained_carries_no_reduce from Core.v 22 July 2020, 11:28:50 UTC
5563ab6 jadep 08 July 2020, 11:48:35 UTC fix let-inlining to match new convert_bases definition, and add a rewrite rule to remove no-op masks 22 July 2020, 11:28:50 UTC
0045c8e jadep 06 July 2020, 13:40:26 UTC parameterize Columns.flatten over add_split 22 July 2020, 11:28:50 UTC
2ba1f31 jadep 06 July 2020, 10:38:48 UTC prettify convert_bases definition 22 July 2020, 11:28:50 UTC
73f8a58 jadep 24 June 2020, 17:05:45 UTC change definition of convert_bases to use Columns 22 July 2020, 11:28:50 UTC
0d6df21 Jason Gross 20 July 2020, 20:25:13 UTC Add Zulip Chat badge to README 20 July 2020, 20:25:13 UTC
6b64e96 Jason Gross 13 July 2020, 22:21:13 UTC Use `s` rather than `weight n` in `n_bytes` As per https://github.com/mit-plv/fiat-crypto/issues/706#issuecomment-657787914, this allows us to deal with unsaturated WBW Montgomery implementations without allocating more bytes than we should. Note for the future: we should possibly move the definition of `bytes_n` out of `Freeze.v`, it seems like a slightly weird location for it. 16 July 2020, 16:03:43 UTC
4c54bbb Jason Gross 08 July 2020, 18:39:28 UTC Add a theory of bitlists and bitwise This is important for proving a tighter bound on the bitwise zrange operations. 14 July 2020, 15:34:44 UTC
254f120 Jason Gross 13 July 2020, 23:33:28 UTC Fix the comment on WBW Mont {from,to}_bytes As per https://github.com/mit-plv/fiat-crypto/issues/706#issuecomment-657787914 14 July 2020, 15:21:58 UTC
0a77905 Jason Gross 13 July 2020, 19:16:51 UTC Don't widen carries in Go, define wrappers Unfortunately, there's not really a good way currently to widen carries to bytes, as some parts of the codebase see the bytes/no-bytes as a function-local destinction, and there's no way to widen carries to bytes while widening things wider than carries to bitwidth. See also https://github.com/mit-plv/fiat-crypto/issues/846 So instead, for Go, we don't widen either, and define types for carries. Additionally, we wrap bits.{Add,Sub}{32,64} so that the outputs and inputs have the right sizes. 14 July 2020, 15:17:48 UTC
6c70313 Jason Gross 13 July 2020, 17:30:00 UTC Revert "Synthesize primitives witout the bytes size" This reverts commit c7302d2343146b385e94cac6fd615b24f005a118. It doesn't actually work, see https://github.com/mit-plv/fiat-crypto/issues/706#issuecomment-657157869 14 July 2020, 15:17:48 UTC
2fe87d6 Jason Gross 12 July 2020, 00:42:16 UTC Synthesize primitives witout the bytes size As per https://github.com/mit-plv/fiat-crypto/issues/706#issuecomment-657154861 We've been synthesizing `cmovznz` and telling it that the `bytes` size is allowed at https://github.com/mit-plv/fiat-crypto/blob/e5751ea93dd729d55c83eb0896d7f321975bcd2c/src/PushButtonSynthesis/Primitives.v#L842-L850, but when we synthesize, e.g., `opp` at https://github.com/mit-plv/fiat-crypto/blob/e5751ea93dd729d55c83eb0896d7f321975bcd2c/src/PushButtonSynthesis/WordByWordMontgomery.v#L347-L355 we tell it that the `bytes` size is not allowed. This hasn't caused issues before, because I don't think I have any other examples where carries should be widened to something wider than bytes. 14 July 2020, 15:17:48 UTC
c6edbbf Jason Gross 11 July 2020, 23:41:50 UTC Don't --widen-bytes in Go As per https://github.com/mit-plv/fiat-crypto/issues/706#issuecomment-657147516 I'm not sure why this doesn't result in too-tight integer ranges for the outputs of `bits.Add{32,64}`, but apparently it doesn't. I should probably look into this sometime, if only to understand it... 14 July 2020, 15:17:48 UTC
ebbcd66 Jason Gross 13 July 2020, 17:25:23 UTC Add some more helper lemmas From developing a theory of bitwise bounds 14 July 2020, 00:32:50 UTC
611908f Jason Gross 13 July 2020, 18:06:48 UTC Use --output-sync This fixes issues like https://github.com/mit-plv/fiat-crypto/runs/866199735 13 July 2020, 18:06:48 UTC
ce7b545 Jason Gross 12 July 2020, 00:02:41 UTC [ci] Try using the latest version of Homebrew This should fix #842, I hope 13 July 2020, 17:27:27 UTC
e5751ea Jason Gross 11 July 2020, 23:16:08 UTC Fix bits.Mul64 Go code As per https://github.com/mit-plv/fiat-crypto/issues/706#issuecomment-657134217 11 July 2020, 23:35:03 UTC
a26d5d4 Jason Gross 10 July 2020, 01:48:34 UTC Add some proofs about apply_to_n_split_range 10 July 2020, 16:34:01 UTC
1f2e302 Jason Gross 10 July 2020, 01:47:36 UTC Add some ZRange operations These will be useful for tighter bitwise bounds, as they let us apply zrange functions separately on the different components of a range. 10 July 2020, 01:47:36 UTC
ec16a20 Jason Gross 10 July 2020, 01:46:08 UTC Add ListUtil lemmas 10 July 2020, 01:46:08 UTC
be867af Jason Gross 10 July 2020, 01:45:51 UTC Remove dead legacy code 10 July 2020, 01:45:51 UTC
a6af08f Jason Gross 09 July 2020, 22:43:55 UTC make update-_CoqProject 09 July 2020, 22:43:55 UTC
7a46295 Jason Gross 09 July 2020, 18:34:25 UTC Bump rewriter for compat with coq/coq#11836 09 July 2020, 18:34:25 UTC
bcc5086 Jason Gross 08 July 2020, 04:32:52 UTC Generalize abstract interpretation over cast assum It's now possible to pass in an argument at a higher level specifying whether or not casts are assumed to truncate. This should help with https://github.com/mit-plv/fiat-crypto/issues/833#issuecomment-655088557 08 July 2020, 18:43:41 UTC
3b0b815 jadep 03 July 2020, 11:40:41 UTC update bedrock2 generated files 08 July 2020, 08:46:09 UTC
fe351ce jadep 02 July 2020, 18:10:36 UTC WIP: change bedrock2 output/input order (update examples) 08 July 2020, 08:46:09 UTC
abb21a4 jadep 02 July 2020, 18:02:07 UTC WIP: change argument order for bedrock2 backend to put output pointers first (compiler proofs/synthesis tactics now work, examples and bedrock2 output files not updated) 08 July 2020, 08:46:09 UTC
dc55596 Jason Gross 07 July 2020, 20:33:36 UTC Speed up UnsaturatedSolinas Work around COQBUG(https://github.com/coq/coq/issues/9286) <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ---------------------------------------------------------------------------------------------------------------------------------------------------- 7m09.83s | 1395540 ko | Total Time / Peak Mem | 7m22.48s | 1395768 ko || -0m12.64s || -228 ko | -2.85% | -0.01% ---------------------------------------------------------------------------------------------------------------------------------------------------- 0m15.24s | 919600 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m27.23s | 925848 ko || -0m11.99s || -6248 ko | -44.03% | -0.67% 3m02.54s | 1309692 ko | Bedrock/Synthesis/Examples/X25519_64.vo | 3m02.63s | 1309552 ko || -0m00.09s || 140 ko | -0.04% | +0.01% 1m23.41s | 1395540 ko | SlowPrimeSynthesisExamples.vo | 1m23.95s | 1395768 ko || -0m00.54s || -228 ko | -0.64% | -0.01% 0m43.85s | 966464 ko | Bedrock/Synthesis/Examples/LadderStep.vo | 0m43.91s | 966612 ko || -0m00.05s || -148 ko | -0.13% | -0.01% 0m39.44s | 1155944 ko | Bedrock/Field/UnsaturatedSolinas.vo | 0m39.53s | 1155788 ko || -0m00.09s || 156 ko | -0.22% | +0.01% 0m39.00s | 997060 ko | Bedrock/Synthesis/Examples/X1305_32.vo | 0m38.80s | 997256 ko || +0m00.20s || -196 ko | +0.51% | -0.01% 0m06.13s | 916548 ko | Bedrock/Synthesis/Examples/EncodeDecode.vo | 0m06.16s | 916320 ko || -0m00.03s || 228 ko | -0.48% | +0.02% 0m03.69s | 766228 ko | Bedrock/Synthesis/Examples/MulTwice.vo | 0m03.71s | 766084 ko || -0m00.02s || 144 ko | -0.53% | +0.01% 0m02.30s | 733164 ko | CLI.vo | 0m02.45s | 733080 ko || -0m00.15s || 84 ko | -6.12% | +0.01% 0m02.27s | 740368 ko | Rewriter/PerfTesting/Core.vo | 0m02.11s | 740376 ko || +0m00.16s || -8 ko | +7.58% | -0.00% 0m02.09s | 771992 ko | Bedrock/StandaloneHaskellMain.vo | 0m02.06s | 772080 ko || +0m00.02s || -88 ko | +1.45% | -0.01% 0m02.09s | 772016 ko | Bedrock/StandaloneOCamlMain.vo | 0m02.10s | 772036 ko || -0m00.01s || -20 ko | -0.47% | -0.00% 0m02.03s | 761352 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.04s | 761372 ko || -0m00.01s || -20 ko | -0.49% | -0.00% 0m01.95s | 752476 ko | Bedrock/Synthesis/UnsaturatedSolinas.vo | 0m01.97s | 752544 ko || -0m00.02s || -68 ko | -1.01% | -0.00% 0m01.91s | 744820 ko | StandaloneHaskellMain.vo | 0m01.89s | 744884 ko || +0m00.02s || -64 ko | +1.05% | -0.00% 0m01.90s | 744980 ko | StandaloneOCamlMain.vo | 0m01.94s | 744976 ko || -0m00.04s || 4 ko | -2.06% | +0.00% ``` </p> 07 July 2020, 20:44:30 UTC
3454813 Jason Gross 07 July 2020, 18:58:50 UTC Adjust some spacing 07 July 2020, 18:58:50 UTC
a70c8ea Jason Gross 07 July 2020, 18:28:02 UTC Add a test pass to the rewriter This should help with https://github.com/mit-plv/fiat-crypto/issues/833#issuecomment-654807764 07 July 2020, 18:43:00 UTC
20e6900 Jason Gross 02 July 2020, 21:15:38 UTC Fix `make bedrock2-files` Fixes #830 03 July 2020, 04:01:46 UTC
73364e5 jadep 24 June 2020, 08:08:28 UTC import Bignum in bedrock synthesis examples 02 July 2020, 18:10:17 UTC
e6914b8 jadep 23 June 2020, 15:02:47 UTC add wbw montgomery examples 02 July 2020, 18:10:17 UTC
d02412a jadep 23 June 2020, 14:46:36 UTC add Synthesis/WordByWordMontgomery.v 02 July 2020, 18:10:17 UTC
2ed31b8 jadep 23 June 2020, 14:40:12 UTC remove trailing space 02 July 2020, 18:10:17 UTC
2b859cf jadep 23 June 2020, 14:39:48 UTC add opp to valid_expr 02 July 2020, 18:10:17 UTC
1e0813f jadep 23 June 2020, 12:00:08 UTC add Field file for wbw montgomery 02 July 2020, 18:10:17 UTC
6361ab7 jadep 23 June 2020, 11:30:43 UTC separate bignums into their own file 02 July 2020, 18:10:17 UTC
920f3df jadep 22 June 2020, 20:03:11 UTC remove reqt that inputs use separate parts of memory 02 July 2020, 18:10:10 UTC
a62076f jadep 22 June 2020, 12:50:30 UTC Move length assertion inside Bignum predicate to simplify specifications 02 July 2020, 11:28:25 UTC
d6252e6 Jason Gross 29 June 2020, 19:09:50 UTC Move C delcarations up to the top of C code This is needed for ISO C90 compliance. Fixes #824 30 June 2020, 20:26:15 UTC
e1e258d Jason Gross 30 June 2020, 04:41:11 UTC Suppress warning about instantiate, add it to list of errors 30 June 2020, 20:25:15 UTC
17992e8 Jason Gross 30 June 2020, 04:37:49 UTC Fix for Coq <= 8.9 30 June 2020, 20:25:15 UTC
560e30f Jason Gross 30 June 2020, 03:38:20 UTC Fixes for Coq master 30 June 2020, 20:25:15 UTC
fe39507 Jason Gross 29 June 2020, 16:41:48 UTC Replace omega with lia The `omega` tactic is deprecated in new versions of Coq. Time difference in AffineProofs is probably due to `par:` interfering with other processes. <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 76m03.23s | 2386204 ko | Total Time / Peak Mem | 74m43.81s | 2385024 ko || +1m19.41s || 1180 ko | +1.77% | +0.04% -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 3m11.65s | 1243992 ko | Curves/Montgomery/AffineProofs.vo | 1m47.33s | 1122852 ko || +1m24.32s || 121140 ko | +78.56% | +10.78% 4m13.26s | 2029864 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 4m25.80s | 2030388 ko || -0m12.54s || -524 ko | -4.71% | -0.02% 2m15.16s | 960984 ko | AbstractInterpretation/Wf.vo | 2m21.93s | 960956 ko || -0m06.77s || 28 ko | -4.76% | +0.00% 0m49.76s | 1034196 ko | Arithmetic/Core.vo | 0m43.40s | 1035596 ko || +0m06.35s || -1400 ko | +14.65% | -0.13% 1m19.40s | 1071248 ko | Curves/Weierstrass/Jacobian.vo | 1m15.95s | 1071260 ko || +0m03.45s || -12 ko | +4.54% | -0.00% 0m49.29s | 1063212 ko | Rewriter/Passes/Arith.vo | 0m45.35s | 1063048 ko || +0m03.93s || 164 ko | +8.68% | +0.01% 0m28.51s | 926840 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m31.77s | 927860 ko || -0m03.25s || -1020 ko | -10.26% | -0.10% 0m05.55s | 658624 ko | Util/ZRange/BasicLemmas.vo | 0m08.60s | 741412 ko || -0m03.04s || -82788 ko | -35.46% | -11.16% 3m44.75s | 1313120 ko | Curves/Weierstrass/Projective.vo | 3m42.28s | 1301252 ko || +0m02.46s || 11868 ko | +1.11% | +0.91% 3m29.49s | 1429900 ko | Fancy/Compiler.vo | 3m26.53s | 1438184 ko || +0m02.96s || -8284 ko | +1.43% | -0.57% 2m50.20s | 1483688 ko | Rewriter/Passes/ArithWithCasts.vo | 2m48.08s | 1482296 ko || +0m02.12s || 1392 ko | +1.26% | +0.09% 0m59.94s | 1058392 ko | Rewriter/Passes/MultiRetSplit.vo | 1m02.16s | 1058200 ko || -0m02.21s || 192 ko | -3.57% | +0.01% 0m22.48s | 820464 ko | Curves/Edwards/AffineProofs.vo | 0m25.07s | 821284 ko || -0m02.58s || -820 ko | -10.33% | -0.09% 9m08.61s | 2386204 ko | Curves/Weierstrass/AffineProofs.vo | 9m07.23s | 2385024 ko || +0m01.37s || 1180 ko | +0.25% | +0.04% 2m46.58s | 1444704 ko | Rewriter/Passes/NBE.vo | 2m45.09s | 1444628 ko || +0m01.48s || 76 ko | +0.90% | +0.00% 2m31.89s | 1474996 ko | Rewriter/Passes/ToFancyWithCasts.vo | 2m33.43s | 1610420 ko || -0m01.54s || -135424 ko | -1.00% | -8.40% 1m11.13s | 908660 ko | AbstractInterpretation/Proofs.vo | 1m12.22s | 911060 ko || -0m01.09s || -2400 ko | -1.50% | -0.26% 1m01.60s | 964420 ko | Rewriter/RulesProofs.vo | 1m00.18s | 964404 ko || +0m01.42s || 16 ko | +2.35% | +0.00% 0m28.12s | 904748 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m29.68s | 904636 ko || -0m01.55s || 112 ko | -5.25% | +0.01% 0m14.86s | 647720 ko | Stringification/IR.vo | 0m16.57s | 647860 ko || -0m01.71s || -140 ko | -10.31% | -0.02% 3m53.62s | 2025944 ko | Curves/Montgomery/XZProofs.vo | 3m54.04s | 2026300 ko || -0m00.41s || -356 ko | -0.17% | -0.01% 3m04.09s | 1312064 ko | Bedrock/Synthesis/Examples/X25519_64.vo | 3m04.43s | 1312052 ko || -0m00.34s || 12 ko | -0.18% | +0.00% 2m23.96s | 2028736 ko | Fancy/Barrett256.vo | 2m24.64s | 1812732 ko || -0m00.67s || 216004 ko | -0.47% | +11.91% 1m45.31s | 580316 ko | Spec/Test/X25519.vo | 1m45.90s | 580228 ko || -0m00.59s || 88 ko | -0.55% | +0.01% 1m28.51s | 1866156 ko | Fancy/Montgomery256.vo | 1m29.05s | 1932396 ko || -0m00.53s || -66240 ko | -0.60% | -3.42% 1m23.63s | 1396068 ko | SlowPrimeSynthesisExamples.vo | 1m22.83s | 1392368 ko || +0m00.79s || 3700 ko | +0.96% | +0.26% 1m16.45s | 1076268 ko | AbstractInterpretation/ZRangeProofs.vo | 1m16.55s | 1076552 ko || -0m00.09s || -284 ko | -0.13% | -0.02% 1m04.93s | 1075548 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 1m04.27s | 1075680 ko || +0m00.66s || -132 ko | +1.02% | -0.01% 0m59.21s | 1189340 ko | Bedrock/Proofs/ValidComputable/Expr.vo | 0m58.75s | 1188736 ko || +0m00.46s || 604 ko | +0.78% | +0.05% 0m53.51s | 877052 ko | Demo.vo | 0m53.89s | 665580 ko || -0m00.38s || 211472 ko | -0.70% | +31.77% 0m45.70s | 971176 ko | Bedrock/Synthesis/Examples/LadderStep.vo | 0m45.20s | 970452 ko || +0m00.50s || 724 ko | +1.10% | +0.07% 0m40.59s | 926616 ko | Rewriter/Passes/MulSplit.vo | 0m40.47s | 925888 ko || +0m00.12s || 728 ko | +0.29% | +0.07% 0m40.48s | 566680 ko | UnsaturatedSolinasHeuristics/Tests.vo | 0m40.55s | 566592 ko || -0m00.07s || 88 ko | -0.17% | +0.01% 0m39.20s | 997212 ko | Bedrock/Synthesis/Examples/X1305_32.vo | 0m39.35s | 997088 ko || -0m00.14s || 124 ko | -0.38% | +0.01% 0m37.98s | 1132692 ko | Bedrock/Field/UnsaturatedSolinas.vo | 0m37.69s | 1133528 ko || +0m00.28s || -836 ko | +0.76% | -0.07% 0m31.76s | 737800 ko | Arithmetic/Saturated.vo | 0m30.88s | 735360 ko || +0m00.88s || 2440 ko | +2.84% | +0.33% 0m26.57s | 844300 ko | Bedrock/Util.vo | 0m26.37s | 842948 ko || +0m00.19s || 1352 ko | +0.75% | +0.16% 0m23.79s | 824116 ko | Arithmetic/BarrettReduction.vo | 0m24.41s | 825164 ko || -0m00.62s || -1048 ko | -2.53% | -0.12% 0m23.33s | 1047112 ko | Bedrock/Proofs/Expr.vo | 0m23.25s | 1049044 ko || +0m00.07s || -1932 ko | +0.34% | -0.18% 0m22.07s | 816800 ko | Arithmetic/WordByWordMontgomery.vo | 0m21.68s | 817052 ko || +0m00.39s || -252 ko | +1.79% | -0.03% 0m20.84s | 1015720 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m20.18s | 1014652 ko || +0m00.66s || 1068 ko | +3.27% | +0.10% 0m20.46s | 914892 ko | Curves/Edwards/XYZT/Basic.vo | 0m19.61s | 915908 ko || +0m00.85s || -1016 ko | +4.33% | -0.11% 0m20.09s | 994264 ko | Bedrock/Proofs/LoadStoreList.vo | 0m20.16s | 993816 ko || -0m00.07s || 448 ko | -0.34% | +0.04% 0m18.19s | 740248 ko | Language/IdentifiersGENERATED.vo | 0m17.59s | 739904 ko || +0m00.60s || 344 ko | +3.41% | +0.04% 0m16.96s | 787568 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo | 0m17.06s | 787420 ko || -0m00.09s || 148 ko | -0.58% | +0.01% 0m16.00s | 639668 ko | Language/IdentifiersGENERATEDProofs.vo | 0m16.02s | 639544 ko || -0m00.01s || 124 ko | -0.12% | +0.01% 0m15.89s | 567736 ko | Algebra/Field.vo | 0m16.04s | 567496 ko || -0m00.14s || 240 ko | -0.93% | +0.04% 0m14.01s | 951320 ko | Bedrock/Proofs/Cmd.vo | 0m14.34s | 951160 ko || -0m00.33s || 160 ko | -2.30% | +0.01% 0m12.99s | 778608 ko | Util/ZRange/LandLorBounds.vo | 0m13.14s | 777628 ko || -0m00.15s || 980 ko | -1.14% | +0.12% 0m11.91s | 584600 ko | Primitives/MxDHRepChange.vo | 0m12.48s | 585064 ko || -0m00.57s || -464 ko | -4.56% | -0.07% 0m11.58s | 767500 ko | Arithmetic/FancyMontgomeryReduction.vo | 0m11.44s | 768396 ko || +0m00.14s || -896 ko | +1.22% | -0.11% 0m10.98s | 501392 ko | Algebra/Ring.vo | 0m10.49s | 476276 ko || +0m00.49s || 25116 ko | +4.67% | +5.27% 0m09.75s | 789176 ko | PushButtonSynthesis/SmallExamples.vo | 0m09.71s | 789672 ko || +0m00.03s || -496 ko | +0.41% | -0.06% 0m09.62s | 941236 ko | Bedrock/Proofs/Func.vo | 0m09.51s | 940744 ko || +0m00.10s || 492 ko | +1.15% | +0.05% 0m09.53s | 681608 ko | Util/ZRange/CornersMonotoneBounds.vo | 0m09.86s | 682416 ko || -0m00.33s || -808 ko | -3.34% | -0.11% 0m08.83s | 630672 ko | Language/IdentifiersBasicGENERATED.vo | 0m08.95s | 631476 ko || -0m00.11s || -804 ko | -1.34% | -0.12% 0m08.74s | 746812 ko | Bedrock/Proofs/ValidComputable/Cmd.vo | 0m08.80s | 747104 ko || -0m00.06s || -292 ko | -0.68% | -0.03% 0m07.62s | 880868 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.64s | 879984 ko || +0m00.98s || 884 ko | +14.75% | +0.10% 0m07.32s | 650200 ko | Util/ListUtil.vo | 0m06.71s | 651976 ko || +0m00.61s || -1776 ko | +9.09% | -0.27% 0m07.28s | 653408 ko | Rewriter/Passes/NoSelect.vo | 0m07.31s | 652964 ko || -0m00.02s || 444 ko | -0.41% | +0.06% 0m07.27s | 1050324 ko | Bedrock/Proofs/EquivalenceProperties.vo | 0m07.76s | 1049288 ko || -0m00.49s || 1036 ko | -6.31% | +0.09% 0m07.14s | 675760 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m07.25s | 675820 ko || -0m00.11s || -60 ko | -1.51% | -0.00% 0m06.77s | 502624 ko | Util/MSets/Sum.vo | 0m06.75s | 501516 ko || +0m00.01s || 1108 ko | +0.29% | +0.22% 0m06.59s | 897452 ko | Bedrock/Proofs/Flatten.vo | 0m06.81s | 897004 ko || -0m00.21s || 448 ko | -3.23% | +0.04% 0m06.41s | 709560 ko | Util/ZUtil/Modulo.vo | 0m06.37s | 713884 ko || +0m00.04s || -4324 ko | +0.62% | -0.60% 0m06.38s | 917936 ko | Bedrock/Synthesis/Examples/EncodeDecode.vo | 0m06.35s | 917344 ko || +0m00.03s || 592 ko | +0.47% | +0.06% 0m06.24s | 764628 ko | COperationSpecifications.vo | 0m05.96s | 764684 ko || +0m00.28s || -56 ko | +4.69% | -0.00% 0m06.09s | 687888 ko | Util/ZUtil/ZSimplify/Autogenerated.vo | 0m05.86s | 685608 ko || +0m00.22s || 2280 ko | +3.92% | +0.33% 0m06.02s | 1193688 ko | Bedrock/Proofs/UsedVarnames.vo | 0m06.44s | 1193688 ko || -0m00.42s || 0 ko | -6.52% | +0.00% 0m06.02s | 870368 ko | PushButtonSynthesis/BaseConversion.vo | 0m05.95s | 870188 ko || +0m00.06s || 180 ko | +1.17% | +0.02% 0m05.82s | 759720 ko | Fancy/Prod.vo | 0m06.07s | 753356 ko || -0m00.25s || 6364 ko | -4.11% | +0.84% 0m05.80s | 607996 ko | Curves/Edwards/Pre.vo | 0m05.44s | 608376 ko || +0m00.35s || -380 ko | +6.61% | -0.06% 0m05.79s | 866512 ko | PushButtonSynthesis/Primitives.vo | 0m05.61s | 866116 ko || +0m00.17s || 396 ko | +3.20% | +0.04% 0m05.52s | 676628 ko | Arithmetic/MontgomeryReduction/Proofs.vo | 0m06.51s | 693376 ko || -0m00.99s || -16748 ko | -15.20% | -2.41% 0m05.49s | 567564 ko | Util/FsatzAutoLemmas.vo | 0m05.47s | 567500 ko || +0m00.02s || 64 ko | +0.36% | +0.01% 0m05.35s | 603124 ko | Language/InversionExtra.vo | 0m05.26s | 602952 ko || +0m00.08s || 172 ko | +1.71% | +0.02% 0m05.34s | 690328 ko | BoundsPipeline.vo | 0m05.40s | 690316 ko || -0m00.06s || 12 ko | -1.11% | +0.00% 0m04.99s | 584360 ko | Algebra/Field_test.vo | 0m04.98s | 584860 ko || +0m00.00s || -500 ko | +0.20% | -0.08% 0m04.90s | 739200 ko | Util/ZUtil/Morphisms.vo | 0m04.67s | 735740 ko || +0m00.23s || 3460 ko | +4.92% | +0.47% 0m04.80s | 749168 ko | Arithmetic/UniformWeight.vo | 0m04.66s | 747912 ko || +0m00.13s || 1256 ko | +3.00% | +0.16% 0m04.79s | 693200 ko | Arithmetic/BarrettReduction/Generalized.vo | 0m05.01s | 698732 ko || -0m00.21s || -5532 ko | -4.39% | -0.79% 0m04.70s | 668536 ko | CastLemmas.vo | 0m04.68s | 668840 ko || +0m00.02s || -304 ko | +0.42% | -0.04% 0m04.26s | 590952 ko | Curves/Montgomery/Affine.vo | 0m04.26s | 590812 ko || +0m00.00s || 140 ko | +0.00% | +0.02% 0m04.11s | 678352 ko | Arithmetic/BarrettReduction/HAC.vo | 0m03.97s | 680704 ko || +0m00.14s || -2352 ko | +3.52% | -0.34% 0m04.09s | 700980 ko | Util/ZUtil/LandLorBounds.vo | 0m04.03s | 700148 ko || +0m00.05s || 832 ko | +1.48% | +0.11% 0m04.00s | 687172 ko | Util/ZUtil/LandLorShiftBounds.vo | 0m03.36s | 681172 ko || +0m00.64s || 6000 ko | +19.04% | +0.88% 0m03.64s | 765496 ko | Bedrock/Synthesis/Examples/MulTwice.vo | 0m03.69s | 765648 ko || -0m00.04s || -152 ko | -1.35% | -0.01% 0m03.54s | 615644 ko | Rewriter/Passes/AddAssocLeft.vo | 0m03.54s | 615580 ko || +0m00.00s || 64 ko | +0.00% | +0.01% 0m03.47s | 867384 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.70s | 867648 ko || -0m00.23s || -264 ko | -6.21% | -0.03% 0m03.46s | 854904 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.43s | 854916 ko || +0m00.02s || -12 ko | +0.87% | -0.00% 0m03.38s | 658856 ko | PushButtonSynthesis/BaseConversionReificationCache.vo | 0m03.62s | 657664 ko || -0m00.24s || 1192 ko | -6.62% | +0.18% 0m03.31s | 881200 ko | Bedrock/Arrays/MakeAccessSizes.vo | 0m03.11s | 880880 ko || +0m00.20s || 320 ko | +6.43% | +0.03% 0m02.96s | 488408 ko | Util/MSets/Iso.vo | 0m02.94s | 487624 ko || +0m00.02s || 784 ko | +0.68% | +0.16% 0m02.94s | 747564 ko | Arithmetic/Freeze.vo | 0m03.11s | 751868 ko || -0m00.16s || -4304 ko | -5.46% | -0.57% 0m02.88s | 645712 ko | Arithmetic/Primitives.vo | 0m03.06s | 648972 ko || -0m00.18s || -3260 ko | -5.88% | -0.50% 0m02.74s | 520344 ko | MiscCompilerPassesProofs.vo | 0m02.66s | 520148 ko || +0m00.08s || 196 ko | +3.00% | +0.03% 0m02.71s | 560436 ko | Spec/MontgomeryCurve.vo | 0m02.66s | 560628 ko || +0m00.04s || -192 ko | +1.87% | -0.03% 0m02.56s | 673892 ko | Arithmetic/BarrettReduction/RidiculousFish.vo | 0m02.66s | 674368 ko || -0m00.10s || -476 ko | -3.75% | -0.07% 0m02.55s | 733140 ko | CLI.vo | 0m02.40s | 730552 ko || +0m00.14s || 2588 ko | +6.24% | +0.35% 0m02.53s | 741784 ko | Arithmetic/ModOps.vo | 0m02.58s | 742876 ko || -0m00.05s || -1092 ko | -1.93% | -0.14% 0m02.52s | 886336 ko | Bedrock/Names/MakeNames.vo | 0m02.69s | 885996 ko || -0m00.16s || 340 ko | -6.31% | +0.03% 0m02.50s | 678208 ko | Util/ZUtil/Shift.vo | 0m02.78s | 682612 ko || -0m00.27s || -4404 ko | -10.07% | -0.64% 0m02.42s | 673068 ko | Util/ZUtil/Div.vo | 0m02.40s | 672244 ko || +0m00.02s || 824 ko | +0.83% | +0.12% 0m02.41s | 603364 ko | Rewriter/Passes/StripLiteralCasts.vo | 0m02.31s | 603036 ko || +0m00.10s || 328 ko | +4.32% | +0.05% 0m02.37s | 880792 ko | Bedrock/Arrays/MaxBounds.vo | 0m02.20s | 880608 ko || +0m00.16s || 184 ko | +7.72% | +0.02% 0m02.30s | 741012 ko | Rewriter/PerfTesting/Core.vo | 0m02.35s | 740656 ko || -0m00.05s || 356 ko | -2.12% | +0.04% 0m02.25s | 551480 ko | Arithmetic/BaseConversion.vo | 0m02.36s | 551088 ko || -0m00.10s || 392 ko | -4.66% | +0.07% 0m02.24s | 673016 ko | Arithmetic/ModularArithmeticTheorems.vo | 0m02.20s | 676344 ko || +0m00.04s || -3328 ko | +1.81% | -0.49% 0m02.23s | 730972 ko | Stringification/Language.vo | 0m02.14s | 730648 ko || +0m00.08s || 324 ko | +4.20% | +0.04% 0m02.19s | 709412 ko | AbstractInterpretation/ZRange.vo | 0m01.91s | 558272 ko || +0m00.28s || 151140 ko | +14.65% | +27.07% 0m02.17s | 740640 ko | Bedrock/Stringification.vo | 0m02.05s | 739828 ko || +0m00.12s || 812 ko | +5.85% | +0.10% 0m02.13s | 648804 ko | CompilersTestCases.vo | 0m02.10s | 649108 ko || +0m00.02s || -304 ko | +1.42% | -0.04% 0m02.11s | 771896 ko | Bedrock/StandaloneHaskellMain.vo | 0m02.05s | 776016 ko || +0m00.06s || -4120 ko | +2.92% | -0.53% 0m02.07s | 655372 ko | Util/NatUtil.vo | 0m01.53s | 509224 ko || +0m00.53s || 146148 ko | +35.29% | +28.70% 0m02.05s | 772016 ko | Bedrock/StandaloneOCamlMain.vo | 0m02.10s | 776312 ko || -0m00.05s || -4296 ko | -2.38% | -0.55% 0m02.05s | 760792 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.09s | 760216 ko || -0m00.04s || 576 ko | -1.91% | +0.07% 0m02.04s | 717304 ko | Bedrock/Parameters/Defaults32.vo | 0m02.04s | 716964 ko || +0m00.00s || 340 ko | +0.00% | +0.04% 0m02.03s | 717468 ko | Bedrock/Parameters/Defaults64.vo | 0m01.99s | 717172 ko || +0m00.03s || 296 ko | +2.01% | +0.04% 0m02.01s | 618160 ko | Util/Tuple.vo | 0m01.73s | 472940 ko || +0m00.27s || 145220 ko | +16.18% | +30.70% 0m02.00s | 603876 ko | Rewriter/Passes/ToFancy.vo | 0m01.99s | 603872 ko || +0m00.01s || 4 ko | +0.50% | +0.00% 0m01.97s | 737492 ko | Bedrock/Field/Tactics.vo | 0m01.79s | 737128 ko || +0m00.17s || 364 ko | +10.05% | +0.04% 0m01.96s | 711880 ko | Bedrock/Parameters/Defaults.vo | 0m01.93s | 711536 ko || +0m00.03s || 344 ko | +1.55% | +0.04% 0m01.96s | 751928 ko | Bedrock/Synthesis/UnsaturatedSolinas.vo | 0m02.10s | 751648 ko || -0m00.14s || 280 ko | -6.66% | +0.03% 0m01.96s | 744532 ko | StandaloneHaskellMain.vo | 0m01.93s | 747008 ko || +0m00.03s || -2476 ko | +1.55% | -0.33% 0m01.94s | 745124 ko | StandaloneOCamlMain.vo | 0m01.94s | 747332 ko || +0m00.00s || -2208 ko | +0.00% | -0.29% 0m01.93s | 682236 ko | Bedrock/Translation/Cmd.vo | 0m01.82s | 681776 ko || +0m00.10s || 460 ko | +6.04% | +0.06% 0m01.92s | 799488 ko | Bedrock/Arrays/ByteBounds.vo | 0m02.01s | 799256 ko || -0m00.08s || 232 ko | -4.47% | +0.02% 0m01.89s | 583016 ko | Bedrock/Translation/Expr.vo | 0m01.94s | 583084 ko || -0m00.05s || -68 ko | -2.57% | -0.01% 0m01.88s | 561788 ko | AbstractInterpretation/AbstractInterpretation.vo | 0m01.95s | 561924 ko || -0m00.07s || -136 ko | -3.58% | -0.02% 0m01.88s | 741864 ko | Bedrock/Field/Operation.vo | 0m01.82s | 741888 ko || +0m00.05s || -24 ko | +3.29% | -0.00% 0m01.87s | 741268 ko | Bedrock/Synthesis/Tactics.vo | 0m01.95s | 740668 ko || -0m00.07s || 600 ko | -4.10% | +0.08% 0m01.82s | 715372 ko | Bedrock/Parameters/SelectParameters.vo | 0m01.97s | 715140 ko || -0m00.14s || 232 ko | -7.61% | +0.03% 0m01.82s | 734260 ko | Bedrock/Proofs/ValidComputable/Func.vo | 0m02.01s | 734424 ko || -0m00.18s || -164 ko | -9.45% | -0.02% 0m01.80s | 676764 ko | Arithmetic/PrimeFieldTheorems.vo | 0m01.38s | 525752 ko || +0m00.42s || 151012 ko | +30.43% | +28.72% 0m01.80s | 729652 ko | Bedrock/Synthesis/ReifiedOperation.vo | 0m01.87s | 729620 ko || -0m00.07s || 32 ko | -3.74% | +0.00% 0m01.70s | 673020 ko | Util/ZUtil/Quot.vo | 0m01.63s | 670320 ko || +0m00.07s || 2700 ko | +4.29% | +0.40% 0m01.68s | 598564 ko | Algebra/ScalarMult.vo | 0m01.42s | 451052 ko || +0m00.26s || 147512 ko | +18.30% | +32.70% 0m01.67s | 525288 ko | Spec/WeierstrassCurve.vo | 0m01.70s | 525580 ko || -0m00.03s || -292 ko | -1.76% | -0.05% 0m01.67s | 684192 ko | Util/ZRange/SplitBounds.vo | 0m01.62s | 683792 ko || +0m00.04s || 400 ko | +3.08% | +0.05% 0m01.66s | 683444 ko | Arithmetic/Partition.vo | 0m01.70s | 684036 ko || -0m00.04s || -592 ko | -2.35% | -0.08% 0m01.63s | 675756 ko | Bedrock/Translation/Func.vo | 0m01.66s | 675508 ko || -0m00.03s || 248 ko | -1.80% | +0.03% 0m01.61s | 668724 ko | Util/ZUtil/AddGetCarry.vo | 0m01.55s | 668840 ko || +0m00.06s || -116 ko | +3.87% | -0.01% 0m01.58s | 652872 ko | Bedrock/Tactics.vo | 0m01.64s | 652876 ko || -0m00.05s || -4 ko | -3.65% | -0.00% 0m01.57s | 664364 ko | Util/ZUtil/Rshi.vo | 0m01.58s | 664912 ko || -0m00.01s || -548 ko | -0.63% | -0.08% 0m01.51s | 532620 ko | Curves/Edwards/XYZT/Precomputed.vo | 0m01.50s | 533596 ko || +0m00.01s || -976 ko | +0.66% | -0.18% 0m01.49s | 622664 ko | Util/ZUtil/Pow2Mod.vo | 0m01.57s | 624052 ko || -0m00.08s || -1388 ko | -5.09% | -0.22% 0m01.41s | 569740 ko | Stringification/Go.vo | 0m01.50s | 569480 ko || -0m00.09s || 260 ko | -6.00% | +0.04% 0m01.39s | 618416 ko | Util/ZUtil/Ones.vo | 0m01.44s | 618844 ko || -0m00.05s || -428 ko | -3.47% | -0.06% 0m01.34s | 571032 ko | Stringification/C.vo | 0m01.42s | 571212 ko || -0m00.07s || -180 ko | -5.63% | -0.03% 0m01.32s | 586940 ko | UnsaturatedSolinasHeuristics.vo | 0m01.42s | 586676 ko || -0m00.09s || 264 ko | -7.04% | +0.04% 0m01.31s | 567656 ko | Stringification/Rust.vo | 0m01.36s | 567768 ko || -0m00.05s || -112 ko | -3.67% | -0.01% 0m01.29s | 572908 ko | Bedrock/Types.vo | 0m01.25s | 572736 ko || +0m00.04s || 172 ko | +3.20% | +0.03% 0m01.29s | 568888 ko | Stringification/Java.vo | 0m01.42s | 568516 ko || -0m00.12s || 372 ko | -9.15% | +0.06% 0m01.28s | 489368 ko | Fancy/Spec.vo | 0m01.23s | 489472 ko || +0m00.05s || -104 ko | +4.06% | -0.02% 0m01.26s | 576664 ko | Bedrock/Translation/LoadStoreList.vo | 0m01.15s | 576688 ko || +0m00.11s || -24 ko | +9.56% | -0.00% 0m01.25s | 522644 ko | Curves/Montgomery/AffineInstances.vo | 0m01.22s | 523172 ko || +0m00.03s || -528 ko | +2.45% | -0.10% 0m01.23s | 574760 ko | Bedrock/Proofs/Equivalence.vo | 0m01.35s | 575132 ko || -0m00.12s || -372 ko | -8.88% | -0.06% 0m01.22s | 572516 ko | Bedrock/Proofs/VarnameSet.vo | 0m01.11s | 572784 ko || +0m00.10s || -268 ko | +9.90% | -0.04% 0m01.22s | 626204 ko | Rewriter/All.vo | 0m01.15s | 625996 ko || +0m00.07s || 208 ko | +6.08% | +0.03% 0m01.21s | 572500 ko | Bedrock/Arrays/MakeListLengths.vo | 0m01.26s | 572132 ko || -0m00.05s || 368 ko | -3.96% | +0.06% 0m01.19s | 553820 ko | Language/APINotations.vo | 0m01.24s | 553708 ko || -0m00.05s || 112 ko | -4.03% | +0.02% 0m01.19s | 620804 ko | Util/ZUtil/Testbit.vo | 0m01.16s | 620920 ko || +0m00.03s || -116 ko | +2.58% | -0.01% 0m01.16s | 549968 ko | Language/WfExtra.vo | 0m01.14s | 550004 ko || +0m00.02s || -36 ko | +1.75% | -0.00% 0m01.16s | 549592 ko | MiscCompilerPassesProofsExtra.vo | 0m01.20s | 549660 ko || -0m00.04s || -68 ko | -3.33% | -0.01% 0m01.12s | 553188 ko | PushButtonSynthesis/ReificationCache.vo | 0m01.16s | 552784 ko || -0m00.03s || 404 ko | -3.44% | +0.07% 0m01.11s | 573332 ko | Bedrock/Translation/Flatten.vo | 0m01.21s | 573136 ko || -0m00.09s || 196 ko | -8.26% | +0.03% 0m01.10s | 685496 ko | Util/QUtil.vo | 0m00.75s | 536812 ko || +0m00.35s || 148684 ko | +46.66% | +27.69% 0m01.09s | 619572 ko | Arithmetic/BarrettReduction/Wikipedia.vo | 0m01.10s | 620492 ko || -0m00.01s || -920 ko | -0.90% | -0.14% 0m01.08s | 507512 ko | Algebra/IntegralDomain.vo | 0m01.13s | 507292 ko || -0m00.04s || 220 ko | -4.42% | +0.04% 0m01.08s | 547800 ko | Language/API.vo | 0m01.10s | 551048 ko || -0m00.02s || -3248 ko | -1.81% | -0.58% 0m01.08s | 461608 ko | Util/Bool/Reflect.vo | 0m01.06s | 461344 ko || +0m00.02s || 264 ko | +1.88% | +0.05% 0m01.07s | 550108 ko | Language/UnderLetsProofsExtra.vo | 0m01.11s | 550132 ko || -0m00.04s || -24 ko | -3.60% | -0.00% 0m01.06s | 548140 ko | ArithmeticCPS/Freeze.vo | 0m01.08s | 547880 ko || -0m00.02s || 260 ko | -1.85% | +0.04% 0m01.06s | 628976 ko | Util/NumTheoryUtil.vo | 0m00.90s | 480052 ko || +0m00.16s || 148924 ko | +17.77% | +31.02% 0m01.05s | 555908 ko | Rewriter/AllTacticsExtra.vo | 0m01.03s | 555720 ko || +0m00.02s || 188 ko | +1.94% | +0.03% 0m01.04s | 555292 ko | AbstractInterpretation/WfExtra.vo | 0m01.12s | 555192 ko || -0m00.08s || 100 ko | -7.14% | +0.01% 0m01.04s | 667724 ko | Util/ZUtil/CC.vo | 0m00.97s | 667608 ko || +0m00.07s || 116 ko | +7.21% | +0.01% 0m00.97s | 478128 ko | Rewriter/Rules.vo | 0m00.98s | 478432 ko || -0m00.01s || -304 ko | -1.02% | -0.06% 0m00.94s | 542976 ko | ArithmeticCPS/WordByWordMontgomery.vo | 0m00.95s | 542884 ko || -0m00.01s || 92 ko | -1.05% | +0.01% 0m00.87s | 548792 ko | ArithmeticCPS/BaseConversion.vo | 0m00.85s | 548580 ko || +0m00.02s || 212 ko | +2.35% | +0.03% 0m00.87s | 529668 ko | ArithmeticCPS/Saturated.vo | 0m00.82s | 529012 ko || +0m00.05s || 656 ko | +6.09% | +0.12% 0m00.85s | 542280 ko | ArithmeticCPS/ModOps.vo | 0m00.95s | 542116 ko || -0m00.09s || 164 ko | -10.52% | +0.03% 0m00.84s | 604876 ko | Util/Decidable/Decidable2Bool.vo | 0m00.64s | 458280 ko || +0m00.19s || 146596 ko | +31.24% | +31.98% 0m00.84s | 621912 ko | Util/ZUtil/Stabilization.vo | 0m00.86s | 622768 ko || -0m00.02s || -856 ko | -2.32% | -0.13% 0m00.83s | 531272 ko | ArithmeticCPS/Core.vo | 0m00.86s | 531164 ko || -0m00.03s || 108 ko | -3.48% | +0.02% 0m00.82s | 610816 ko | Util/ZUtil/Modulo/PullPush.vo | 0m00.85s | 610968 ko || -0m00.03s || -152 ko | -3.52% | -0.02% 0m00.81s | 503828 ko | MiscCompilerPasses.vo | 0m00.89s | 503808 ko || -0m00.07s || 20 ko | -8.98% | +0.00% 0m00.81s | 489480 ko | Util/ZRange/OperationsBounds.vo | 0m00.83s | 489448 ko || -0m00.01s || 32 ko | -2.40% | +0.00% 0m00.79s | 656712 ko | Util/ZUtil/Ltz.vo | 0m00.84s | 658388 ko || -0m00.04s || -1676 ko | -5.95% | -0.25% 0m00.78s | 461120 ko | Algebra/SubsetoidRing.vo | 0m00.67s | 436856 ko || +0m00.10s || 24264 ko | +16.41% | +5.55% 0m00.78s | 587892 ko | Util/Loops.vo | 0m00.54s | 412440 ko || +0m00.24s || 175452 ko | +44.44% | +42.54% 0m00.77s | 459556 ko | Util/CPSUtil.vo | 0m00.79s | 462280 ko || -0m00.02s || -2724 ko | -2.53% | -0.58% 0m00.73s | 580824 ko | Util/Strings/String_as_OT.vo | 0m00.46s | 417076 ko || +0m00.26s || 163748 ko | +58.69% | +39.26% 0m00.70s | 468760 ko | Util/Arg.vo | 0m00.76s | 469144 ko || -0m00.06s || -384 ko | -7.89% | -0.08% 0m00.69s | 658768 ko | Util/ZUtil/Combine.vo | 0m00.73s | 658776 ko || -0m00.04s || -8 ko | -5.47% | -0.00% 0m00.67s | 508000 ko | Curves/Montgomery/XZ.vo | 0m00.65s | 508288 ko || +0m00.02s || -288 ko | +3.07% | -0.05% 0m00.67s | 659996 ko | Util/ZUtil/Divide.vo | 0m00.48s | 509772 ko || +0m00.19s || 150224 ko | +39.58% | +29.46% 0m00.67s | 611960 ko | Util/ZUtil/Log2.vo | 0m00.72s | 611952 ko || -0m00.04s || 8 ko | -6.94% | +0.00% 0m00.66s | 638600 ko | Util/ZUtil/Tactics/RewriteModSmall.vo | 0m00.46s | 505328 ko || +0m00.20s || 133272 ko | +43.47% | +26.37% 0m00.64s | 449464 ko | Util/Strings/ParseArithmeticToTaps.vo | 0m00.62s | 440228 ko || +0m00.02s || 9236 ko | +3.22% | +2.09% 0m00.62s | 503708 ko | Curves/Weierstrass/Affine.vo | 0m00.69s | 503588 ko || -0m00.06s || 120 ko | -10.14% | +0.02% 0m00.62s | 500304 ko | Spec/CompleteEdwardsCurve.vo | 0m00.62s | 501248 ko || +0m00.00s || -944 ko | +0.00% | -0.18% 0m00.62s | 609016 ko | Util/ZUtil/Pow.vo | 0m00.58s | 599576 ko || +0m00.04s || 9440 ko | +6.89% | +1.57% 0m00.60s | 609644 ko | Util/ZUtil/Le.vo | 0m00.59s | 609632 ko || +0m00.01s || 12 ko | +1.69% | +0.00% 0m00.57s | 580212 ko | Util/ZUtil/Tactics/LtbToLt.vo | 0m00.30s | 374944 ko || +0m00.26s || 205268 ko | +89.99% | +54.74% 0m00.55s | 470112 ko | Util/MSetPositive/Show.vo | 0m00.47s | 457548 ko || +0m00.08s || 12564 ko | +17.02% | +2.74% 0m00.54s | 477964 ko | Arithmetic/ModularArithmeticPre.vo | 0m00.66s | 468528 ko || -0m00.12s || 9436 ko | -18.18% | +2.01% 0m00.54s | 579184 ko | Util/Strings/String.vo | 0m00.39s | 420956 ko || +0m00.15s || 158228 ko | +38.46% | +37.58% 0m00.52s | 459044 ko | Util/ZBounded.vo | 0m00.56s | 458976 ko || -0m00.04s || 68 ko | -7.14% | +0.01% 0m00.52s | 456588 ko | Util/ZRange.vo | 0m00.49s | 456920 ko || +0m00.03s || -332 ko | +6.12% | -0.07% 0m00.51s | 466004 ko | Language/PreExtra.vo | 0m00.46s | 467048 ko || +0m00.04s || -1044 ko | +10.86% | -0.22% 0m00.51s | 455856 ko | Util/HList.vo | 0m00.51s | 454808 ko || +0m00.00s || 1048 ko | +0.00% | +0.23% 0m00.50s | 524508 ko | Util/ZUtil/Odd.vo | 0m00.32s | 372296 ko || +0m00.18s || 152212 ko | +56.25% | +40.88% 0m00.49s | 442104 ko | Util/ZUtil/CPS.vo | 0m00.43s | 417064 ko || +0m00.06s || 25040 ko | +13.95% | +6.00% 0m00.49s | 466296 ko | Util/ZUtil/EquivModulo.vo | 0m00.47s | 466072 ko || +0m00.02s || 224 ko | +4.25% | +0.04% 0m00.49s | 536824 ko | Util/ZUtil/Opp.vo | 0m00.37s | 385776 ko || +0m00.12s || 151048 ko | +32.43% | +39.15% 0m00.48s | 467068 ko | Language/IdentifierParameters.vo | 0m00.51s | 466808 ko || -0m00.03s || 260 ko | -5.88% | +0.05% 0m00.46s | 447704 ko | Util/Strings/ParseArithmetic.vo | 0m00.40s | 438008 ko || +0m00.06s || 9696 ko | +15.00% | +2.21% 0m00.46s | 457420 ko | Util/ZRange/Operations.vo | 0m00.47s | 457396 ko || -0m00.00s || 24 ko | -2.12% | +0.00% 0m00.46s | 489108 ko | Util/ZUtil.vo | 0m00.46s | 488600 ko || +0m00.00s || 508 ko | +0.00% | +0.10% 0m00.45s | 432876 ko | Spec/ModularArithmetic.vo | 0m00.41s | 432944 ko || +0m00.04s || -68 ko | +9.75% | -0.01% 0m00.45s | 525904 ko | Util/ZUtil/Tactics/LinearSubstitute.vo | 0m00.27s | 339332 ko || +0m00.18s || 186572 ko | +66.66% | +54.98% 0m00.43s | 448560 ko | Util/Strings/Show.vo | 0m00.43s | 433816 ko || +0m00.00s || 14744 ko | +0.00% | +3.39% 0m00.43s | 433792 ko | Util/ZUtil/Tactics/Ztestbit.vo | 0m00.38s | 433600 ko || +0m00.04s || 192 ko | +13.15% | +0.04% 0m00.42s | 457796 ko | Util/ZUtil/ZSimplify/Simple.vo | 0m00.44s | 457804 ko || -0m00.02s || -8 ko | -4.54% | -0.00% 0m00.41s | 456436 ko | Util/AdditionChainExponentiation.vo | 0m00.45s | 455724 ko || -0m00.04s || 712 ko | -8.88% | +0.15% 0m00.41s | 408588 ko | Util/ZUtil/Tactics.vo | 0m00.40s | 408316 ko || +0m00.00s || 272 ko | +2.49% | +0.06% 0m00.40s | 444592 ko | Util/Strings/StringMap.vo | 0m00.33s | 423268 ko || +0m00.07s || 21324 ko | +21.21% | +5.03% 0m00.38s | 393240 ko | Util/ZUtil/DistrIf.vo | 0m00.37s | 393296 ko || +0m00.01s || -56 ko | +2.70% | -0.01% 0m00.38s | 414712 ko | Util/ZUtil/N2Z.vo | 0m00.34s | 413976 ko || +0m00.03s || 736 ko | +11.76% | +0.17% 0m00.37s | 404068 ko | Arithmetic/MontgomeryReduction/Definition.vo | 0m00.38s | 403772 ko || -0m00.01s || 296 ko | -2.63% | +0.07% 0m00.37s | 412060 ko | Util/IdfunWithAlt.vo | 0m00.34s | 410312 ko || +0m00.02s || 1748 ko | +8.82% | +0.42% 0m00.37s | 441568 ko | Util/NUtil/WithoutReferenceToZ.vo | 0m00.39s | 442664 ko || -0m00.02s || -1096 ko | -5.12% | -0.24% 0m00.37s | 420960 ko | Util/ZRange/Show.vo | 0m00.38s | 420664 ko || -0m00.01s || 296 ko | -2.63% | +0.07% 0m00.37s | 378896 ko | Util/ZUtil/Tactics/DivModToQuotRem.vo | 0m00.39s | 379040 ko || -0m00.02s || -144 ko | -5.12% | -0.03% 0m00.37s | 378064 ko | Util/ZUtil/Tactics/PeelLe.vo | 0m00.34s | 378024 ko || +0m00.02s || 40 ko | +8.82% | +0.01% 0m00.36s | 377428 ko | Util/ZUtil/Hints/Ztestbit.vo | 0m00.33s | 377160 ko || +0m00.02s || 268 ko | +9.09% | +0.07% 0m00.36s | 391208 ko | Util/ZUtil/Modulo/Bootstrap.vo | 0m00.32s | 391236 ko || +0m00.03s || -28 ko | +12.49% | -0.00% 0m00.36s | 383472 ko | Util/ZUtil/Tactics/PullPush/Modulo.vo | 0m00.35s | 383536 ko || +0m00.01s || -64 ko | +2.85% | -0.01% 0m00.36s | 393404 ko | Util/ZUtil/Tactics/SimplifyFractionsLe.vo | 0m00.38s | 393416 ko || -0m00.02s || -12 ko | -5.26% | -0.00% 0m00.36s | 390532 ko | Util/ZUtil/Tactics/ZeroBounds.vo | 0m00.38s | 389972 ko || -0m00.02s || 560 ko | -5.26% | +0.14% 0m00.36s | 383752 ko | Util/ZUtil/ZSimplify/Core.vo | 0m00.38s | 384152 ko || -0m00.02s || -400 ko | -5.26% | -0.10% 0m00.35s | 379212 ko | Util/ZUtil/Hints/ZArith.vo | 0m00.34s | 379288 ko || +0m00.00s || -76 ko | +2.94% | -0.02% 0m00.35s | 413648 ko | Util/ZUtil/Sgn.vo | 0m00.36s | 398524 ko || -0m00.01s || 15124 ko | -2.77% | +3.79% 0m00.34s | 378448 ko | Util/ZUtil/Div/Bootstrap.vo | 0m00.34s | 378772 ko || +0m00.00s || -324 ko | +0.00% | -0.08% 0m00.34s | 395740 ko | Util/ZUtil/MulSplit.vo | 0m00.33s | 395892 ko || +0m00.01s || -152 ko | +3.03% | -0.03% 0m00.34s | 342840 ko | Util/ZUtil/Tactics/SplitMinMax.vo | 0m00.26s | 300596 ko || +0m00.08s || 42244 ko | +30.76% | +14.05% 0m00.33s | 386992 ko | Bedrock/Names/VarnameGenerator.vo | 0m00.30s | 357836 ko || +0m00.03s || 29156 ko | +10.00% | +8.14% 0m00.33s | 376396 ko | Util/MSets/Show.vo | 0m00.28s | 348860 ko || +0m00.04s || 27536 ko | +17.85% | +7.89% 0m00.33s | 381820 ko | Util/ZUtil/Hints.vo | 0m00.35s | 381680 ko || -0m00.01s || 140 ko | -5.71% | +0.03% 0m00.33s | 387668 ko | Util/ZUtil/Hints/PullPush.vo | 0m00.33s | 387640 ko || +0m00.00s || 28 ko | +0.00% | +0.00% 0m00.33s | 348284 ko | Util/ZUtil/Tactics/PullPush.vo | 0m00.31s | 348272 ko || +0m00.02s || 12 ko | +6.45% | +0.00% 0m00.32s | 366712 ko | Util/ErrorT/Show.vo | 0m00.29s | 339052 ko || +0m00.03s || 27660 ko | +10.34% | +8.15% 0m00.32s | 382268 ko | Util/ZUtil/Hints/Core.vo | 0m00.34s | 411900 ko || -0m00.02s || -29632 ko | -5.88% | -7.19% 0m00.31s | 369924 ko | Util/ZUtil/Pow2.vo | 0m00.32s | 366632 ko || -0m00.01s || 3292 ko | -3.12% | +0.89% 0m00.31s | 348324 ko | Util/ZUtil/Tactics/ReplaceNegWithPos.vo | 0m00.26s | 299640 ko || +0m00.04s || 48684 ko | +19.23% | +16.24% 0m00.31s | 354148 ko | Util/ZUtil/ZSimplify.vo | 0m00.36s | 354100 ko || -0m00.04s || 48 ko | -13.88% | +0.01% 0m00.30s | 364384 ko | TAPSort.vo | 0m00.22s | 319388 ko || +0m00.07s || 44996 ko | +36.36% | +14.08% 0m00.29s | 357960 ko | Util/ZUtil/Sorting.vo | 0m00.30s | 357668 ko || -0m00.01s || 292 ko | -3.33% | +0.08% 0m00.27s | 352664 ko | Util/Strings/Parse/Common.vo | 0m00.26s | 322876 ko || +0m00.01s || 29788 ko | +3.84% | +9.22% 0m00.27s | 307032 ko | Util/ZUtil/Tactics/PrimeBound.vo | 0m00.24s | 292168 ko || +0m00.03s || 14864 ko | +12.50% | +5.08% 0m00.25s | 341620 ko | Util/ZUtil/Tactics/DivideExistsMul.vo | 0m00.24s | 292856 ko || +0m00.01s || 48764 ko | +4.16% | +16.65% ``` </p> 30 June 2020, 20:25:15 UTC
d0de37a Jason Gross 29 June 2020, 19:16:25 UTC Bump rewriter 29 June 2020, 19:19:43 UTC
a587b4d Jason Gross 29 June 2020, 18:15:06 UTC Bump rewriter 29 June 2020, 18:15:06 UTC
184b333 Jason Gross 29 June 2020, 16:25:20 UTC Bump rewriter for coq/coq#12372 29 June 2020, 16:25:20 UTC
679ece1 Jason Gross 29 June 2020, 16:24:16 UTC Add debugging symbols to generated ocaml binaries 29 June 2020, 16:24:16 UTC
e63c696 Jason Gross 24 June 2020, 18:22:12 UTC Allow the bedrock2 BoringSSL test to fail 24 June 2020, 18:44:25 UTC
0e15af9 Jason Gross 24 June 2020, 16:21:09 UTC Test C and bedrock2 code with BoringSSL Significant work on #708 24 June 2020, 18:44:25 UTC
f4e03fb jadep 22 June 2020, 20:42:15 UTC update commented-out printing statement in X25519_64.v 23 June 2020, 15:04:24 UTC
b3d6630 jadep 22 June 2020, 20:41:28 UTC update bedrock2 backend readme 23 June 2020, 15:04:24 UTC
d9ada86 jadep 22 June 2020, 12:51:55 UTC bedrock2 backend cleanup: fix lingering import with wrong name 23 June 2020, 11:50:45 UTC
77fefc0 jadep 22 June 2020, 12:00:14 UTC bedrock2 backend cleanup: rename Interfaces/ to Field/ 23 June 2020, 11:50:45 UTC
f964caa jadep 22 June 2020, 11:53:27 UTC bedrock2 backend cleanup: split up Varnames.v 23 June 2020, 11:50:45 UTC
dcd7217 jadep 22 June 2020, 11:32:19 UTC bedrock2 backend cleanup: split up Types.v 23 June 2020, 11:50:45 UTC
d5cfd78 Jason Gross 21 June 2020, 03:59:41 UTC Fix w.r.t. coq/coq#12532 With coq/coq#12532, `eauto` shelves more arguments, and therefore solves more goals. But we don't want `eauto` leaving over shelved goals here, so we prefix it with `unshelve`. Closes #814 21 June 2020, 03:59:41 UTC
0b402f7 Jason Gross 21 June 2020, 02:44:01 UTC Quiet a warning We no longer support Coq 8.7, so we don't need to reserve this notation, and it was giving: Warning: Notation "{ _ & _ }" was already defined with a different format. [notation-incompatible-format,parsing] 21 June 2020, 02:44:01 UTC
afd4506 Jason Gross 21 June 2020, 02:25:05 UTC Remove a suspicious ??? tactic 21 June 2020, 02:25:05 UTC
d3cc84d Jason Gross 21 June 2020, 00:22:18 UTC Add status badges for MacOS and Windows 21 June 2020, 00:22:18 UTC
71ece0a Jason Gross 20 June 2020, 17:26:21 UTC Try to fix Windows CI 20 June 2020, 17:26:21 UTC
e872e22 jadep 19 June 2020, 16:28:42 UTC remove line breaks from notes because github doesn't like them 19 June 2020, 16:28:42 UTC
a22adb8 jadep 19 June 2020, 16:24:11 UTC add notes from a close-read of BoringSSL curve25519 code for later reference 19 June 2020, 16:25:16 UTC
c0dcbb8 jadep 17 June 2020, 09:20:48 UTC fix typo 18 June 2020, 16:31:35 UTC
570ca50 jadep 17 June 2020, 09:17:13 UTC add missing import 18 June 2020, 16:31:35 UTC
72ef67b jadep 16 June 2020, 16:07:54 UTC prove admit in EncodeDecode.v 18 June 2020, 16:31:35 UTC
a115243 jadep 01 June 2020, 11:02:36 UTC replace encode_no_reduce with partition (and use that to prove an admit in Bedrock/Interfaces) 18 June 2020, 16:31:35 UTC
fb68225 jadep 15 June 2020, 09:32:30 UTC update notations in bedrock2 synthesis examples 15 June 2020, 15:14:43 UTC
2ddec0a jadep 12 June 2020, 12:09:45 UTC remove stray print statement 15 June 2020, 15:14:43 UTC
c5873dd jadep 12 June 2020, 11:13:11 UTC use newly exported bounds definitions for UnsaturatedSolinas interface 15 June 2020, 15:14:43 UTC
509a624 jadep 12 June 2020, 09:50:12 UTC use vm_cast_no_check instead of (vm_compute; reflexivity) 15 June 2020, 15:14:43 UTC
back to top