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
df77590 Andres Erbsen 02 March 2022, 15:14:07 UTC admit riscv_word_ok instance 02 March 2022, 15:14:07 UTC
168bcc9 Andres Erbsen 02 March 2022, 12:43:24 UTC X25519: use specs of from_wrod,cswap,copy 02 March 2022, 13:18:35 UTC
e53e02b Jade Philipoom 05 December 2021, 18:19:53 UTC finish proof about compiler output and factor out remaining admits WIP, working on compiler proof compiler proof statement wip separating proof WIP wip, changed ext_spec in field25519 to be parameterized wip finish proof about compiler output and factor out remaining admits 02 March 2022, 12:47:00 UTC
514951e Andres Erbsen 02 March 2022, 01:26:54 UTC update output-tests/Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.montladder_body.expected 02 March 2022, 12:05:52 UTC
01b94d9 Andres Erbsen 23 February 2022, 21:00:42 UTC rm src/Bedrock/Field/Interface/Compilation.v 02 March 2022, 12:05:52 UTC
433c56e Andres Erbsen 22 February 2022, 19:57:12 UTC integrate from_word and cswap with montledder 02 March 2022, 12:05:52 UTC
33af4d1 Andres Erbsen 17 January 2022, 00:26:20 UTC thread through admitted fe25519_copy 02 March 2022, 12:05:52 UTC
46dbcef Andres Erbsen 15 January 2022, 20:29:54 UTC Hint Rewrite @eval_cons weight_multiples : push_eval 02 March 2022, 12:05:52 UTC
4390cb9 dependabot[bot] 28 February 2022, 21:42:57 UTC Bump actions/setup-python from 2.3.2 to 3 (#1144) 28 February 2022, 21:42:57 UTC
72a46b7 dependabot[bot] 28 February 2022, 20:02:02 UTC Bump actions/setup-go from 2.2.0 to 3 (#1143) 28 February 2022, 20:02:02 UTC
c9172da Jason Gross 25 February 2022, 18:57:19 UTC Finish SymbolicProofs proof of shlx 28 February 2022, 00:25:04 UTC
1607562 Joel 21 February 2022, 23:01:52 UTC added import to Tactics.WarnIfGoalsRemain. 28 February 2022, 00:25:04 UTC
5e92f66 Joel 21 February 2022, 21:37:45 UTC Update src/Assembly/WithBedrock/SymbolicProofs.v Co-authored-by: Jason Gross <jasongross9@gmail.com> 28 February 2022, 00:25:04 UTC
aa7d354 Joel 21 February 2022, 04:33:58 UTC adding `Show.` 28 February 2022, 00:25:04 UTC
d191296 Joel 21 February 2022, 00:00:10 UTC adding Unshelve, to see the remaining goals in the CI 28 February 2022, 00:25:04 UTC
05d1f6f Joel 18 February 2022, 06:21:07 UTC simplify 28 February 2022, 00:25:04 UTC
6f7f38d Joel 18 February 2022, 06:11:52 UTC 'most' infix... 28 February 2022, 00:25:04 UTC
b25d3f1 Joel 18 February 2022, 06:05:28 UTC negb rather than Z.z2b 28 February 2022, 00:25:04 UTC
0c700c3 Joel 18 February 2022, 05:01:52 UTC z2b'ing it back to be able to call SetFlag 28 February 2022, 00:25:04 UTC
44ed466 Joel 18 February 2022, 04:25:29 UTC using B2z to convert bool -> Z 28 February 2022, 00:25:04 UTC
ae98890 Joel 17 February 2022, 23:58:08 UTC remove space 28 February 2022, 00:25:04 UTC
970f3b4 Joel 17 February 2022, 23:29:45 UTC adding `shl,_` and `shlx,_` in DenoteNormalInstruction 28 February 2022, 00:25:04 UTC
6739378 Joel 17 February 2022, 20:57:45 UTC xor -> lxor Co-authored-by: Jason Gross <jasongross9@gmail.com> 28 February 2022, 00:25:04 UTC
6bac53a Joel 17 February 2022, 03:33:25 UTC showcasing shlx-by-2 to multiply-by-2-twice 28 February 2022, 00:25:04 UTC
25bcfb8 Joel 17 February 2022, 03:29:20 UTC fix correctness. x10 was missing 28 February 2022, 00:25:04 UTC
d278fb7 Joel 17 February 2022, 03:18:42 UTC moving shift to mul before flatten assoc 28 February 2022, 00:25:04 UTC
48917a3 Joel 17 February 2022, 03:15:22 UTC amending existing file fo showcase shlx/shl to mul 28 February 2022, 00:25:04 UTC
e93e29a Joel 17 February 2022, 03:10:00 UTC move showcase (*2*2 != *4) to existing file 28 February 2022, 00:25:04 UTC
59af4d4 Joel 17 February 2022, 03:06:08 UTC moving to other PR 28 February 2022, 00:25:04 UTC
4937bbb Joel 17 February 2022, 01:51:21 UTC resolve syntax err. Co-authored-by: Jason Gross <jasongross9@gmail.com> 28 February 2022, 00:25:04 UTC
7fb8749 Joel 17 February 2022, 01:45:28 UTC remove space Co-authored-by: Jason Gross <jasongross9@gmail.com> 28 February 2022, 00:25:04 UTC
8182d88 Joel 17 February 2022, 01:44:20 UTC Update src/Assembly/Syntax.v Co-authored-by: Jason Gross <jasongross9@gmail.com> 28 February 2022, 00:25:04 UTC
49727ae Joel 17 February 2022, 01:44:13 UTC Update src/Assembly/Parse.v Co-authored-by: Jason Gross <jasongross9@gmail.com> 28 February 2022, 00:25:04 UTC
46b1cf3 Joel 17 February 2022, 01:51:41 UTC using cnt' instead of cnt 28 February 2022, 00:25:04 UTC
2a5e8f6 Jason Gross 17 February 2022, 01:11:44 UTC Fix shift_to_mul definition and proof We need to truncate the expression when there's a bitwidth to truncate it to 28 February 2022, 00:25:04 UTC
3c1358e Joel 16 February 2022, 23:46:21 UTC adding shl->mul rewrite 28 February 2022, 00:25:04 UTC
e5498cb Joel 16 February 2022, 23:46:04 UTC reverting MEM-changes to focus on shl-mul rewrite 28 February 2022, 00:25:04 UTC
f81e5a3 Joel 14 February 2022, 07:05:47 UTC shl, shlx into Semantics.v for bedrock 28 February 2022, 00:25:04 UTC
3a28184 Joel 14 February 2022, 07:05:22 UTC lea z*reg 28 February 2022, 00:25:04 UTC
5174d20 Joel 10 February 2022, 06:38:04 UTC showcase a * 2 * 2 !== a*4 28 February 2022, 00:25:04 UTC
af52382 Joel 10 February 2022, 02:33:36 UTC added shl and shlx to parser and symbolic 28 February 2022, 00:25:04 UTC
0d92c08 Joel 10 February 2022, 02:32:52 UTC added two files, showcasing other instr. to mul * imm 28 February 2022, 00:25:04 UTC
92bd843 Jason Gross 24 February 2022, 23:16:16 UTC Add ListUtil.StdlibCompat All the lemmas in Coq.Lists.List and Coq.Sorting.Permutation present in current master (8.16?) but not in 8.11. 25 February 2022, 17:26:23 UTC
eebdaad Jason Gross 24 February 2022, 02:05:47 UTC Add groupBy and groupAllBy 25 February 2022, 17:26:23 UTC
9251ed6 dependabot[bot] 24 February 2022, 21:38:12 UTC Bump rupicola from `fb8c808` to `48820b7` (#1142) 24 February 2022, 21:38:12 UTC
bc8b294 dependabot[bot] 24 February 2022, 20:45:44 UTC Bump actions/setup-java from 2.5.0 to 3.0.0 (#1141) 24 February 2022, 20:45:44 UTC
23d85fd Ashley Lin 23 February 2022, 06:27:52 UTC reverse argument order in AdditionChains 23 February 2022, 06:27:52 UTC
1549d5a Jason Gross 22 February 2022, 21:06:23 UTC Add ListUtil.span for groupBy (#1137) 22 February 2022, 21:06:23 UTC
982f14d Jason Gross 21 February 2022, 23:50:15 UTC Include the operation when explaining the final error messages in asm 22 February 2022, 15:57:11 UTC
cfe296f Jason Gross 21 February 2022, 21:22:44 UTC Better error messages Probably if the lists are the same lengths, then we want to compare them element-wise rather than all at once. It's way too verbose to keep expanding them, so we only do that when lists are not the same length. We now get error messages such as ``` Unable to unify: [inr [378, 381, 384]] == [inr [101, 106, 108]] Could not unify the values at index 0: [#378, #381, #384] != [#101, #106, #108] index 0: #378 != #101 (slice 0 44, [#377]) != (slice 0 44, [#98]) index 0: #377 != #98 (add 64, [#345, #375]) != (add 64, [#57, #96]) index 0: #345 != #57 (slice 0 44, [#337]) != (slice 0 44, [#44]) index 0: #337 != #44 (add 64, [#41, #334]) != (add 64, [#25, #41]) index 1: #334 != #25 (mul 64, [#1, #331]) != (mul 64, [#0, #1, #22]) [(add 64, [#329, #329])] != [#0, (const 20, [])] [(add 64, [(mul 64, [#7, #328]), (mul 64, [#7, #328])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, #327])]), (mul 64, [(const 2, []), (add 64, [#0, #327])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, #326])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, #326])])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])])])] != [(old 64 0, []), (const 20, [])] ``` The second to last line is generally the one to look at; the last line adds a bit more detail to it. Perhaps we should instead list out the values of indices rather than expanding one additional level? 22 February 2022, 15:57:11 UTC
1b8c820 Jason Gross 21 February 2022, 20:26:40 UTC Prefix dag indices with more # 22 February 2022, 15:57:11 UTC
a41e08c Jason Gross 21 February 2022, 17:20:37 UTC Better explanation of unification error messages 22 February 2022, 15:57:11 UTC
8ca4f01 Jason Gross 22 February 2022, 00:24:11 UTC Export FixCoqMistakes 22 February 2022, 00:24:11 UTC
e21d65a Jason Gross 21 February 2022, 23:51:29 UTC Add Util.MSetN a la MSetPositive (#1135) 21 February 2022, 23:51:29 UTC
c1d9a8d Jason Gross 21 February 2022, 19:01:30 UTC Add warn_if_goals_remain, fail_if_goals_remain 21 February 2022, 19:01:30 UTC
0fc8a3f Jason Gross 21 February 2022, 18:00:47 UTC Add List.combine_extend 21 February 2022, 18:00:47 UTC
d394fb1 Jason Gross 16 February 2022, 22:33:04 UTC Minor progress towards finishing asm equiv proof The way that we're dealing with load state needs to be rethought :-( 17 February 2022, 06:27:41 UTC
9ba2af1 Jason Gross 16 February 2022, 08:59:40 UTC More progress on assembly equivalence proof The only thing that remains to be proven is that the runtime output values that we get are the ones we expect to get. I need to figure out where to propogate this information from, but this proof is almost done! 17 February 2022, 06:27:41 UTC
3e3fcf2 Jason Gross 15 February 2022, 17:48:12 UTC Add ClearHead 15 February 2022, 17:48:12 UTC
d925881 Dustin Jamner 14 February 2022, 20:26:21 UTC Fix equivalence proofs to work w/ current cswap 15 February 2022, 03:51:47 UTC
b467760 Dustin Jamner 14 February 2022, 17:05:26 UTC Fix breakage in end2end due to moved function name 15 February 2022, 03:51:47 UTC
3735655 Dustin Jamner 10 February 2022, 21:54:25 UTC Move context to top of file 15 February 2022, 03:51:47 UTC
a8e5684 Dustin Jamner 10 February 2022, 21:47:05 UTC Integrate cswap and montladder 15 February 2022, 03:51:47 UTC
b18204d Dustin Jamner 09 February 2022, 18:29:23 UTC Add CSwap implementation 15 February 2022, 03:51:47 UTC
f6d4db0 dependabot[bot] 14 February 2022, 20:15:14 UTC Bump rupicola from `e8651e8` to `fb8c808` (#1129) 14 February 2022, 20:15:14 UTC
af618d3 Jason Gross 14 February 2022, 00:18:48 UTC More WIP on asm equiv (#1124) 14 February 2022, 00:18:48 UTC
e77a9f6 Jason Gross 11 February 2022, 06:49:55 UTC Fix for Coq master 13 February 2022, 03:49:10 UTC
b44327e Jason Gross 03 February 2022, 19:00:10 UTC Finish proving/using that SymexLines scribles only over known memory What remains is doing the reverse of the final symex goal to deal with the different representations of memory specs, splitting apart input and output values via `++` (not 100% sure how to do this yet), and showing that the outputs are mapped to the right values (also need to figure out how to do this). 13 February 2022, 03:49:10 UTC
59600ae Jason Gross 10 February 2022, 23:58:59 UTC Enable const folding for mul asm (#1127) c.f. https://github.com/mit-plv/fiat-crypto/pull/1123#issuecomment-1035216542 10 February 2022, 23:58:59 UTC
90a33fc dependabot[bot] 10 February 2022, 22:32:30 UTC Bump rewriter from `2bd8776` to `5ca81b1` (#1126) 10 February 2022, 22:32:30 UTC
e151e21 Jason Gross 10 February 2022, 07:44:59 UTC Better coherence in describing commutative errors We now report correct array indices (at least on the left side) 10 February 2022, 16:20:40 UTC
ac1b073 Jason Gross 10 February 2022, 07:30:44 UTC Give better error messages on length mismatch 10 February 2022, 16:20:40 UTC
23c8a75 Jason Gross 10 February 2022, 07:16:07 UTC Report equiv errors modulo commutativity Should give a better error message for https://github.com/mit-plv/fiat-crypto/pull/1123#issuecomment-1034554480 10 February 2022, 16:20:40 UTC
ba344c5 dependabot[bot] 10 February 2022, 11:13:28 UTC Bump actions/setup-go from 2.1.5 to 2.2.0 (#1122) 10 February 2022, 11:13:28 UTC
4a89282 dependabot[bot] 10 February 2022, 10:06:50 UTC Bump coqprime from `f0eb59e` to `b984180` (#1121) 10 February 2022, 10:06:50 UTC
77731c4 dependabot[bot] 10 February 2022, 05:20:44 UTC Bump rewriter from `73192bd` to `2bd8776` (#1120) 10 February 2022, 05:20:44 UTC
e612a32 dependabot[bot] 05 February 2022, 00:08:45 UTC Bump rupicola from `a55c99f` to `e8651e8` (#1119) 05 February 2022, 00:08:45 UTC
e14021a dependabot[bot] 04 February 2022, 22:32:15 UTC Bump actions/setup-python from 2.3.1 to 2.3.2 (#1118) 04 February 2022, 22:32:15 UTC
b61ebb1 Jason Gross 04 February 2022, 15:46:07 UTC Don't fail-fast This allows us to still get the generated file updates when one job fails and the other succeeds. It's not particularly bad to do this, since now we're only testing two versions in coq.yml 04 February 2022, 15:46:07 UTC
680a5aa Jason Gross 04 February 2022, 15:34:39 UTC Add a lemma about list split (#1116) 04 February 2022, 15:34:39 UTC
fe19dfc Jason Gross 03 February 2022, 01:44:41 UTC Insert a probably-useful revgoals 03 February 2022, 19:00:43 UTC
7975cee Jason Gross 03 February 2022, 00:49:48 UTC Remove dead comment What remains is to replace the TODO in `Forall2_rets_of_R_mem` with something like `(??? * R_list_scalar_or_array runtime_rets asm_args_out)%sep` (shouldn't be too bad), and then to prove that `SymexLines` preserves the memory cells that are mapped. 03 February 2022, 19:00:43 UTC
4af4ccf Jason Gross 03 February 2022, 00:06:22 UTC Moderate progress on output goal 03 February 2022, 19:00:43 UTC
721a9d9 Jason Gross 25 January 2022, 17:37:46 UTC Update asm equiv to finish all but output goal 03 February 2022, 19:00:43 UTC
90e0c05 Jason Gross 03 February 2022, 00:13:47 UTC Add eq_filter_nil_Forall_iff 03 February 2022, 00:13:47 UTC
8d316e5 dependabot[bot] 28 January 2022, 20:19:10 UTC Bump rupicola from `8c23e8f` to `a55c99f` (#1112) 28 January 2022, 20:19:10 UTC
27e8fde dependabot[bot] 27 January 2022, 20:52:45 UTC Bump rewriter from `629c4f4` to `73192bd` (#1111) 27 January 2022, 20:52:45 UTC
607d27a Jason Gross 27 January 2022, 15:41:01 UTC Add some Forall lemmas (#1110) 27 January 2022, 15:41:01 UTC
731ed9f Jason Gross 26 January 2022, 19:48:41 UTC Keep Tactics.v up to date 26 January 2022, 19:48:41 UTC
15bf6e7 Jason Gross 26 January 2022, 19:40:18 UTC Add Tactics.FindHyp, fix bug in unique pose Work around https://github.com/coq/coq/issues/15554 26 January 2022, 19:40:57 UTC
083a3ef Jason Gross 26 January 2022, 16:27:20 UTC Remove duplicate file 26 January 2022, 16:27:20 UTC
e47a33e Jason Gross 25 January 2022, 15:20:37 UTC More assembly equivalence WIP (#1109) Only two subgoals remain: ```coq R_runtime_output frame runtime_rets (type_spec_of_runtime (word_args_to_Z_args word_runtime_inputs)) (Datatypes.length x) stack_base asm_args_out asm_args_in callee_saved_registers runtime_callee_saved_registers m' ``` and ```coq R (frame ⋆ R_list_scalar_or_array x0 asm_args_out ⋆ R_list_scalar_or_array (word_args_to_Z_args word_runtime_inputs) asm_args_in ⋆ array cell64 (word.of_Z 8) stack_base x)%sep x1 (update_dag_with (init_symbolic_state d) (fun _ : dag => d0)) m -> R_mem frame G_final dag_state1 (rev (List.combine x4 x5) ++ rev (flat_map (fun pat : (idx + idx * list idx) * (idx + list idx) => match pat with | (inl _, _) => [] | (inr (_, addrs'), inl _) => [] | (inr (_, addrs'), inr items) => List.combine addrs' items end) (List.combine x3 (l4 ++ inputs))) ++ init_symbolic_state d) m ``` The first goal is that we must connect everything from the final symbolic evaluation with our output spec. The second goal is that we must connect the memory predicate from before SymexLines (post-initialization) with the desired memory predicate, by showing that we've updated symbolic memory as desired. Note that we'll probably want some `iff` statements around `R_mem`, because what we do in one direction in the first goal we do in the other direction in the second goal. 25 January 2022, 15:20:37 UTC
1e2c36e dependabot[bot] 24 January 2022, 20:36:04 UTC Bump rupicola from `f9df34b` to `8c23e8f` (#1108) 24 January 2022, 20:36:04 UTC
2af2296 Jason Gross 22 January 2022, 20:15:03 UTC Add option `--emit-all-casts` and use it in JSON (#1107) We now emit all inferred casts, without trying to do any clever adjustment. Fixes #1099 <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- 96m53.43s | 2625152 ko | Total Time / Peak Mem | 95m53.88s | 2462932 ko || +0m59.55s || 162220 ko | +1.03% | +6.58% ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- 7m42.70s | 1068504 ko | fiat-go/32/p384/p384.go | 7m15.67s | 1016432 ko || +0m27.02s || 52072 ko | +6.20% | +5.12% 7m15.76s | 1160712 ko | fiat-bedrock2/src/p384_32.c | 7m01.45s | 1081268 ko || +0m14.31s || 79444 ko | +3.39% | +7.34% 8m14.89s | 917796 ko | fiat-c/src/p384_32.c | 8m00.98s | 1084016 ko || +0m13.90s || -166220 ko | +2.89% | -15.33% 8m13.67s | 990128 ko | fiat-rust/src/p384_32.rs | 8m08.88s | 1128700 ko || +0m04.79s || -138572 ko | +0.97% | -12.27% 1m37.50s | 1487292 ko | SlowPrimeSynthesisExamples.vo | 1m39.95s | 1466444 ko || -0m02.45s || 20848 ko | -2.45% | +1.42% 0m27.25s | 202704 ko | fiat-rust/src/p256_32.rs | 0m29.28s | 217964 ko || -0m02.03s || -15260 ko | -6.93% | -7.00% 0m24.51s | 171172 ko | fiat-bedrock2/src/p434_64.c | 0m22.45s | 155804 ko || +0m02.06s || 15368 ko | +9.17% | +9.86% 7m49.82s | 1114728 ko | fiat-json/src/p384_32.json | 7m47.92s | 1051532 ko || +0m01.89s || 63196 ko | +0.40% | +6.00% 7m47.22s | 1051556 ko | fiat-java/src/FiatP384.java | 7m49.09s | 1051212 ko || -0m01.87s || 344 ko | -0.39% | +0.03% 0m31.97s | 221720 ko | fiat-json/src/secp256k1_32.json | 0m30.61s | 230568 ko || +0m01.35s || -8848 ko | +4.44% | -3.83% 0m31.90s | 1408184 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m33.45s | 1407148 ko || -0m01.55s || 1036 ko | -4.63% | +0.07% 0m31.31s | 196800 ko | fiat-c/src/secp256k1_32.c | 0m29.86s | 218048 ko || +0m01.44s || -21248 ko | +4.85% | -9.74% 0m28.82s | 1226428 ko | ExtractionOCaml/base_conversion | 0m29.95s | 1240312 ko || -0m01.12s || -13884 ko | -3.77% | -1.11% 0m28.22s | 209892 ko | fiat-java/src/FiatSecp256K1.java | 0m29.55s | 215616 ko || -0m01.33s || -5724 ko | -4.50% | -2.65% 0m27.50s | 1233668 ko | ExtractionOCaml/saturated_solinas | 0m28.69s | 1233804 ko || -0m01.19s || -136 ko | -4.14% | -0.01% 0m22.74s | 157592 ko | fiat-zig/src/p434_64.zig | 0m20.99s | 136588 ko || +0m01.75s || 21004 ko | +8.33% | +15.37% 7m31.83s | 1034496 ko | fiat-zig/src/p384_32.zig | 7m31.32s | 925468 ko || +0m00.50s || 109028 ko | +0.11% | +11.78% 1m46.12s | 1376176 ko | Fancy/Barrett256.vo | 1m46.30s | 1375784 ko || -0m00.17s || 392 ko | -0.16% | +0.02% 1m41.53s | 1057688 ko | Bedrock/Field/Synthesis/Examples/X25519_64.vo | 1m41.32s | 1057792 ko || +0m00.21s || -104 ko | +0.20% | -0.00% 1m13.71s | 1185408 ko | Bedrock/End2End/X25519/Field25519.vo | 1m13.07s | 1185336 ko || +0m00.64s || 72 ko | +0.87% | +0.00% 1m01.31s | 1328760 ko | Bedrock/Field/Synthesis/Examples/p224_64.vo | 1m00.95s | 1328624 ko || +0m00.35s || 136 ko | +0.59% | +0.01% 0m59.56s | 1302544 ko | Bedrock/Field/Synthesis/Examples/p256_64.vo | 0m59.47s | 1302584 ko || +0m00.09s || -40 ko | +0.15% | -0.00% 0m53.81s | 2462848 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m54.33s | 2462484 ko || -0m00.51s || 364 ko | -0.95% | +0.01% 0m48.97s | 2625152 ko | ExtractionOCaml/word_by_word_montgomery | 0m49.78s | 2462932 ko || -0m00.81s || 162220 ko | -1.62% | +6.58% 0m47.10s | 1273040 ko | Fancy/Montgomery256.vo | 0m46.80s | 1277188 ko || +0m00.30s || -4148 ko | +0.64% | -0.32% 0m45.27s | 940228 ko | Assembly/WithBedrock/SymbolicProofs.vo | 0m45.22s | 939756 ko || +0m00.05s || 472 ko | +0.11% | +0.05% 0m40.11s | 2335372 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m40.27s | 2340268 ko || -0m00.16s || -4896 ko | -0.39% | -0.20% 0m39.01s | 2231488 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m38.98s | 2218968 ko || +0m00.03s || 12520 ko | +0.07% | +0.56% 0m36.42s | 1742648 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m36.57s | 1742908 ko || -0m00.14s || -260 ko | -0.41% | -0.01% 0m34.44s | 211996 ko | fiat-bedrock2/src/secp256k1_32.c | 0m33.57s | 213748 ko || +0m00.86s || -1752 ko | +2.59% | -0.81% 0m33.67s | 1144732 ko | Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo | 0m33.67s | 1145460 ko || +0m00.00s || -728 ko | +0.00% | -0.06% 0m33.34s | 1403940 ko | ExtractionOCaml/bedrock2_base_conversion | 0m33.43s | 1402028 ko || -0m00.08s || 1912 ko | -0.26% | +0.13% 0m33.24s | 913272 ko | Assembly/WithBedrock/Proofs.vo | 0m33.10s | 913344 ko || +0m00.14s || -72 ko | +0.42% | -0.00% 0m32.94s | 1086560 ko | Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo | 0m33.16s | 1087712 ko || -0m00.21s || -1152 ko | -0.66% | -0.10% 0m32.82s | 214696 ko | fiat-bedrock2/src/p256_32.c | 0m32.19s | 227932 ko || +0m00.63s || -13236 ko | +1.95% | -5.80% 0m31.60s | 189840 ko | fiat-zig/src/secp256k1_32.zig | 0m31.24s | 192512 ko || +0m00.36s || -2672 ko | +1.15% | -1.38% 0m31.47s | 1721020 ko | ExtractionOCaml/unsaturated_solinas | 0m31.50s | 1727952 ko || -0m00.03s || -6932 ko | -0.09% | -0.40% 0m30.51s | 218052 ko | fiat-go/32/secp256k1/secp256k1.go | 0m30.44s | 217028 ko || +0m00.07s || 1024 ko | +0.22% | +0.47% 0m30.45s | 219476 ko | fiat-go/32/p256/p256.go | 0m29.47s | 211972 ko || +0m00.98s || 7504 ko | +3.32% | +3.54% 0m30.38s | 218752 ko | fiat-rust/src/secp256k1_32.rs | 0m30.33s | 205732 ko || +0m00.05s || 13020 ko | +0.16% | +6.32% 0m29.97s | 216340 ko | fiat-json/src/p256_32.json | 0m29.99s | 200256 ko || -0m00.01s || 16084 ko | -0.06% | +8.03% 0m29.70s | 1233408 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m29.96s | 1233332 ko || -0m00.26s || 76 ko | -0.86% | +0.00% 0m29.36s | 214036 ko | fiat-zig/src/p256_32.zig | 0m29.57s | 210932 ko || -0m00.21s || 3104 ko | -0.71% | +1.47% 0m28.87s | 208136 ko | fiat-c/src/p256_32.c | 0m29.03s | 192676 ko || -0m00.16s || 15460 ko | -0.55% | +8.02% 0m28.25s | 849252 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m28.36s | 848072 ko || -0m00.10s || 1180 ko | -0.38% | +0.13% 0m28.01s | 192640 ko | fiat-java/src/FiatP256.java | 0m28.08s | 231864 ko || -0m00.06s || -39224 ko | -0.24% | -16.91% 0m27.48s | 1233336 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m27.43s | 1233380 ko || +0m00.05s || -44 ko | +0.18% | -0.00% 0m25.55s | 1707316 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m25.42s | 1706088 ko || +0m00.12s || 1228 ko | +0.51% | +0.07% 0m24.34s | 865636 ko | Bedrock/Field/Synthesis/Examples/LadderStep.vo | 0m24.27s | 865984 ko || +0m00.07s || -348 ko | +0.28% | -0.04% 0m24.11s | 1726360 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m23.88s | 1694844 ko || +0m00.23s || 31516 ko | +0.96% | +1.85% 0m23.17s | 832528 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m23.19s | 832092 ko || -0m00.01s || 436 ko | -0.08% | +0.05% 0m23.09s | 156324 ko | fiat-go/64/p434/p434.go | 0m23.18s | 151052 ko || -0m00.08s || 5272 ko | -0.38% | +3.49% 0m23.09s | 163028 ko | fiat-json/src/p434_64.json | 0m22.86s | 143576 ko || +0m00.23s || 19452 ko | +1.00% | +13.54% 0m22.88s | 161972 ko | fiat-rust/src/p434_64.rs | 0m23.16s | 162884 ko || -0m00.28s || -912 ko | -1.20% | -0.55% 0m22.20s | 149984 ko | fiat-c/src/p434_64.c | 0m22.77s | 135908 ko || -0m00.57s || 14076 ko | -2.50% | +10.35% 0m21.01s | 1665436 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m20.94s | 1666380 ko || +0m00.07s || -944 ko | +0.33% | -0.05% 0m20.74s | 1669652 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m20.99s | 1670756 ko || -0m00.25s || -1104 ko | -1.19% | -0.06% 0m20.17s | 1843672 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m20.17s | 1827544 ko || +0m00.00s || 16128 ko | +0.00% | +0.88% 0m19.76s | 1615100 ko | ExtractionOCaml/base_conversion.ml | 0m19.61s | 1615232 ko || +0m00.15s || -132 ko | +0.76% | -0.00% 0m18.93s | 824252 ko | Bedrock/Field/Synthesis/Examples/X1305_32.vo | 0m18.84s | 824020 ko || +0m00.08s || 232 ko | +0.47% | +0.02% 0m18.82s | 1621096 ko | ExtractionOCaml/saturated_solinas.ml | 0m19.68s | 1604964 ko || -0m00.85s || 16132 ko | -4.36% | +1.00% 0m18.64s | 1738884 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m18.61s | 1740672 ko || +0m00.03s || -1788 ko | +0.16% | -0.10% 0m17.95s | 1761132 ko | ExtractionHaskell/word_by_word_montgomery.hs | 0m17.10s | 1760444 ko || +0m00.84s || 688 ko | +4.97% | +0.03% 0m17.34s | 1927676 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs | 0m18.10s | 1941556 ko || -0m00.76s || -13880 ko | -4.19% | -0.71% 0m16.81s | 780772 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m16.89s | 780368 ko || -0m00.08s || 404 ko | -0.47% | +0.05% 0m16.37s | 802384 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m16.34s | 802500 ko || +0m00.03s || -116 ko | +0.18% | -0.01% 0m15.91s | 924888 ko | StandaloneDebuggingExamples.vo | 0m15.55s | 910316 ko || +0m00.35s || 14572 ko | +2.31% | +1.60% 0m15.13s | 134564 ko | fiat-bedrock2/src/p224_32.c | 0m15.42s | 144212 ko || -0m00.28s || -9648 ko | -1.88% | -6.69% 0m14.52s | 794884 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m14.51s | 794712 ko || +0m00.00s || 172 ko | +0.06% | +0.02% 0m14.11s | 143288 ko | fiat-json/src/p224_32.json | 0m13.59s | 147428 ko || +0m00.51s || -4140 ko | +3.82% | -2.80% 0m14.01s | 140976 ko | fiat-java/src/FiatP224.java | 0m14.22s | 127540 ko || -0m00.21s || 13436 ko | -1.47% | +10.53% 0m13.86s | 139932 ko | fiat-go/32/p224/p224.go | 0m13.65s | 129588 ko || +0m00.20s || 10344 ko | +1.53% | +7.98% 0m13.84s | 1480060 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs | 0m13.86s | 1492508 ko || -0m00.01s || -12448 ko | -0.14% | -0.83% 0m13.69s | 136040 ko | fiat-rust/src/p224_32.rs | 0m14.01s | 139460 ko || -0m00.32s || -3420 ko | -2.28% | -2.45% 0m13.63s | 1430500 ko | ExtractionHaskell/unsaturated_solinas.hs | 0m13.75s | 1431204 ko || -0m00.11s || -704 ko | -0.87% | -0.04% 0m13.61s | 133008 ko | fiat-zig/src/p224_32.zig | 0m13.53s | 135168 ko || +0m00.08s || -2160 ko | +0.59% | -1.59% 0m13.58s | 128228 ko | fiat-c/src/p224_32.c | 0m13.65s | 132132 ko || -0m00.07s || -3904 ko | -0.51% | -2.95% 0m12.37s | 1382164 ko | ExtractionHaskell/saturated_solinas.hs | 0m12.32s | 1381884 ko || +0m00.04s || 280 ko | +0.40% | +0.02% 0m12.20s | 1356512 ko | ExtractionHaskell/base_conversion.hs | 0m12.31s | 1352812 ko || -0m00.11s || 3700 ko | -0.89% | +0.27% 0m11.99s | 97416 ko | fiat-bedrock2/src/p384_64.c | 0m12.20s | 94244 ko || -0m00.20s || 3172 ko | -1.72% | +3.36% 0m11.93s | 858012 ko | PushButtonSynthesis/SmallExamples.vo | 0m11.76s | 857716 ko || +0m00.16s || 296 ko | +1.44% | +0.03% 0m11.76s | 1381096 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs | 0m12.30s | 1386120 ko || -0m00.54s || -5024 ko | -4.39% | -0.36% 0m11.65s | 1380672 ko | ExtractionHaskell/bedrock2_base_conversion.hs | 0m11.57s | 1379576 ko || +0m00.08s || 1096 ko | +0.69% | +0.07% 0m10.91s | 772120 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m10.88s | 772016 ko || +0m00.02s || 104 ko | +0.27% | +0.01% 0m10.86s | 589532 ko | Stringification/IR.vo | 0m10.66s | 589148 ko || +0m00.19s || 384 ko | +1.87% | +0.06% 0m10.81s | 88648 ko | fiat-go/64/p384/p384.go | 0m10.94s | 87320 ko || -0m00.12s || 1328 ko | -1.18% | +1.52% 0m10.81s | 94888 ko | fiat-json/src/p384_64.json | 0m10.52s | 97052 ko || +0m00.29s || -2164 ko | +2.75% | -2.22% 0m10.56s | 100488 ko | fiat-rust/src/p384_64.rs | 0m10.53s | 103028 ko || +0m00.03s || -2540 ko | +0.28% | -2.46% 0m10.42s | 97896 ko | fiat-zig/src/p384_64.zig | 0m10.03s | 97292 ko || +0m00.39s || 604 ko | +3.88% | +0.62% 0m10.41s | 99904 ko | fiat-c/src/p384_64.c | 0m10.43s | 96588 ko || -0m00.01s || 3316 ko | -0.19% | +3.43% 0m08.73s | 105440 ko | fiat-json/src/p448_solinas_32.json | 0m08.48s | 51280 ko || +0m00.25s || 54160 ko | +2.94% | +105.61% 0m08.34s | 44380 ko | fiat-zig/src/p448_solinas_32.zig | 0m08.34s | 46620 ko || +0m00.00s || -2240 ko | +0.00% | -4.80% 0m08.27s | 45448 ko | fiat-rust/src/p448_solinas_32.rs | 0m08.28s | 46412 ko || -0m00.00s || -964 ko | -0.12% | -2.07% 0m08.24s | 44248 ko | fiat-c/src/p448_solinas_32.c | 0m08.19s | 47432 ko || +0m00.05s || -3184 ko | +0.61% | -6.71% 0m08.23s | 751040 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m08.27s | 750848 ko || -0m00.03s || 192 ko | -0.48% | +0.02% 0m08.21s | 688480 ko | PushButtonSynthesis/BaseConversion.vo | 0m08.38s | 688756 ko || -0m00.16s || -276 ko | -2.02% | -0.04% 0m06.93s | 691472 ko | PushButtonSynthesis/Primitives.vo | 0m07.02s | 689956 ko || -0m00.08s || 1516 ko | -1.28% | +0.21% 0m05.37s | 733708 ko | Bedrock/Field/Synthesis/Examples/EncodeDecode.vo | 0m05.41s | 734284 ko || -0m00.04s || -576 ko | -0.73% | -0.07% 0m05.23s | 638624 ko | BoundsPipeline.vo | 0m05.24s | 638220 ko || -0m00.00s || 404 ko | -0.19% | +0.06% 0m04.80s | 679684 ko | PushButtonSynthesis/BarrettReduction.vo | 0m04.55s | 679588 ko || +0m00.25s || 96 ko | +5.49% | +0.01% 0m03.85s | 39396 ko | fiat-bedrock2/src/p521_64.c | 0m03.89s | 39664 ko || -0m00.04s || -268 ko | -1.02% | -0.67% 0m03.73s | 31024 ko | fiat-go/64/p521/p521.go | 0m03.83s | 33072 ko || -0m00.10s || -2048 ko | -2.61% | -6.19% 0m03.65s | 740564 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m03.63s | 740392 ko || +0m00.02s || 172 ko | +0.55% | +0.02% 0m03.45s | 721632 ko | Bedrock/Field/Synthesis/Examples/MulTwice.vo | 0m03.38s | 721452 ko || +0m00.07s || 180 ko | +2.07% | +0.02% 0m03.23s | 688560 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.22s | 688660 ko || +0m00.00s || -100 ko | +0.31% | -0.01% 0m03.21s | 27044 ko | fiat-zig/src/p521_64.zig | 0m03.25s | 27048 ko || -0m00.04s || -4 ko | -1.23% | -0.01% 0m03.20s | 25648 ko | fiat-rust/src/p521_64.rs | 0m03.16s | 26996 ko || +0m00.04s || -1348 ko | +1.26% | -4.99% 0m03.07s | 45200 ko | fiat-bedrock2/src/secp256k1_64.c | 0m03.07s | 46472 ko || +0m00.00s || -1272 ko | +0.00% | -2.73% 0m03.06s | 705168 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m03.06s | 704904 ko || +0m00.00s || 264 ko | +0.00% | +0.03% 0m02.98s | 38308 ko | fiat-json/src/p521_64.json | 0m02.93s | 29156 ko || +0m00.04s || 9152 ko | +1.70% | +31.38% 0m02.93s | 686628 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m02.89s | 686832 ko || +0m00.04s || -204 ko | +1.38% | -0.02% 0m02.89s | 27044 ko | fiat-c/src/p521_64.c | 0m02.84s | 26884 ko || +0m00.05s || 160 ko | +1.76% | +0.59% 0m02.84s | 709872 ko | CLI.vo | 0m02.88s | 710820 ko || -0m00.04s || -948 ko | -1.38% | -0.13% 0m02.77s | 41836 ko | fiat-go/64/secp256k1/secp256k1.go | 0m02.64s | 44612 ko || +0m00.12s || -2776 ko | +4.92% | -6.22% 0m02.72s | 42708 ko | fiat-bedrock2/src/p448_solinas_64.c | 0m02.54s | 41632 ko || +0m00.18s || 1076 ko | +7.08% | +2.58% 0m02.69s | 33084 ko | fiat-go/64/p448solinas/p448solinas.go | 0m02.76s | 35392 ko || -0m00.06s || -2308 ko | -2.53% | -6.52% 0m02.62s | 51844 ko | fiat-json/src/secp256k1_64.json | 0m02.59s | 41700 ko || +0m00.03s || 10144 ko | +1.15% | +24.32% 0m02.60s | 38624 ko | fiat-bedrock2/src/curve25519_32.c | 0m02.65s | 37148 ko || -0m00.04s || 1476 ko | -1.88% | +3.97% 0m02.59s | 44504 ko | fiat-zig/src/secp256k1_64.zig | 0m02.57s | 41456 ko || +0m00.02s || 3048 ko | +0.77% | +7.35% 0m02.55s | 42268 ko | fiat-rust/src/secp256k1_64.rs | 0m02.55s | 40072 ko || +0m00.00s || 2196 ko | +0.00% | +5.48% 0m02.45s | 41412 ko | fiat-c/src/secp256k1_64.c | 0m02.53s | 40504 ko || -0m00.07s || 908 ko | -3.16% | +2.24% 0m02.42s | 49824 ko | fiat-bedrock2/src/p224_64.c | 0m02.36s | 42792 ko || +0m00.06s || 7032 ko | +2.54% | +16.43% 0m02.24s | 46188 ko | fiat-bedrock2/src/p256_64.c | 0m02.33s | 43988 ko || -0m00.08s || 2200 ko | -3.86% | +5.00% 0m02.18s | 26812 ko | fiat-go/32/curve25519/curve25519.go | 0m02.18s | 25160 ko || +0m00.00s || 1652 ko | +0.00% | +6.56% 0m02.09s | 38928 ko | fiat-json/src/p448_solinas_64.json | 0m02.03s | 27476 ko || +0m00.06s || 11452 ko | +2.95% | +41.68% 0m02.03s | 42628 ko | fiat-go/64/p224/p224.go | 0m02.03s | 39108 ko || +0m00.00s || 3520 ko | +0.00% | +9.00% 0m02.03s | 44152 ko | fiat-go/64/p256/p256.go | 0m02.02s | 42852 ko || +0m00.00s || 1300 ko | +0.49% | +3.03% 0m02.01s | 25624 ko | fiat-zig/src/p448_solinas_64.zig | 0m02.01s | 25772 ko || +0m00.00s || -148 ko | +0.00% | -0.57% 0m01.99s | 48988 ko | fiat-json/src/p256_64.json | 0m01.86s | 42908 ko || +0m00.12s || 6080 ko | +6.98% | +14.16% 0m01.98s | 25504 ko | fiat-rust/src/p448_solinas_64.rs | 0m01.99s | 25652 ko || -0m00.01s || -148 ko | -0.50% | -0.57% 0m01.97s | 25456 ko | fiat-c/src/p448_solinas_64.c | 0m01.96s | 26928 ko || +0m00.01s || -1472 ko | +0.51% | -5.46% 0m01.96s | 49372 ko | fiat-json/src/p224_64.json | 0m01.96s | 39872 ko || +0m00.00s || 9500 ko | +0.00% | +23.82% 0m01.95s | 43548 ko | fiat-zig/src/p224_64.zig | 0m01.82s | 44616 ko || +0m00.12s || -1068 ko | +7.14% | -2.39% 0m01.94s | 39292 ko | fiat-json/src/curve25519_32.json | 0m01.87s | 27144 ko || +0m00.06s || 12148 ko | +3.74% | +44.75% 0m01.94s | 40268 ko | fiat-rust/src/p224_64.rs | 0m01.90s | 43584 ko || +0m00.04s || -3316 ko | +2.10% | -7.60% 0m01.90s | 42200 ko | fiat-zig/src/p256_64.zig | 0m01.93s | 38124 ko || -0m00.03s || 4076 ko | -1.55% | +10.69% 0m01.88s | 43232 ko | fiat-c/src/p224_64.c | 0m01.93s | 41848 ko || -0m00.05s || 1384 ko | -2.59% | +3.30% 0m01.87s | 25296 ko | fiat-java/src/FiatCurve25519.java | 0m01.84s | 25740 ko || +0m00.03s || -444 ko | +1.63% | -1.72% 0m01.84s | 640576 ko | Bedrock/Field/Translation/Cmd.vo | 0m01.82s | 639320 ko || +0m00.02s || 1256 ko | +1.09% | +0.19% 0m01.84s | 40064 ko | fiat-rust/src/p256_64.rs | 0m01.78s | 44444 ko || +0m00.06s || -4380 ko | +3.37% | -9.85% 0m01.84s | 25864 ko | fiat-zig/src/curve25519_32.zig | 0m01.77s | 25244 ko || +0m00.07s || 620 ko | +3.95% | +2.45% 0m01.83s | 589212 ko | CompilersTestCases.vo | 0m01.83s | 589832 ko || +0m00.00s || -620 ko | +0.00% | -0.10% 0m01.82s | 38612 ko | fiat-c/src/p256_64.c | 0m01.83s | 43068 ko || -0m00.01s || -4456 ko | -0.54% | -10.34% 0m01.81s | 24308 ko | fiat-rust/src/curve25519_32.rs | 0m01.76s | 23796 ko || +0m00.05s || 512 ko | +2.84% | +2.15% 0m01.79s | 25376 ko | fiat-c/src/curve25519_32.c | 0m01.78s | 24584 ko || +0m00.01s || 792 ko | +0.56% | +3.22% 0m01.55s | 532812 ko | Stringification/Language.vo | 0m01.61s | 533020 ko || -0m00.06s || -208 ko | -3.72% | -0.03% 0m01.54s | 719172 ko | Rewriter/PerfTesting/Core.vo | 0m01.53s | 719192 ko || +0m00.01s || -20 ko | +0.65% | -0.00% 0m01.52s | 633916 ko | Bedrock/Field/Translation/Func.vo | 0m01.57s | 633736 ko || -0m00.05s || 180 ko | -3.18% | +0.02% 0m01.27s | 527856 ko | Stringification/Go.vo | 0m01.26s | 527528 ko || +0m00.01s || 328 ko | +0.79% | +0.06% 0m01.24s | 688748 ko | Bedrock/Field/Stringification/Stringification.vo | 0m01.29s | 688736 ko || -0m00.05s || 12 ko | -3.87% | +0.00% 0m01.14s | 711912 ko | Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.vo | 0m01.21s | 712128 ko || -0m00.07s || -216 ko | -5.78% | -0.03% 0m01.12s | 743720 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m01.14s | 743556 ko || -0m00.01s || 164 ko | -1.75% | +0.02% 0m01.10s | 696888 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m01.08s | 696836 ko || +0m00.02s || 52 ko | +1.85% | +0.00% 0m01.09s | 581084 ko | Assembly/Equivalence.vo | 0m01.08s | 581040 ko || +0m00.01s || 44 ko | +0.92% | +0.00% 0m01.09s | 694508 ko | Bedrock/Field/Synthesis/Generic/Operation.vo | 0m01.09s | 694572 ko || +0m00.00s || -64 ko | +0.00% | -0.00% 0m01.07s | 693036 ko | Bedrock/Field/Synthesis/Specialized/Tactics.vo | 0m01.00s | 693004 ko || +0m00.07s || 32 ko | +7.00% | +0.00% 0m01.06s | 725488 ko | Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.vo | 0m01.21s | 725576 ko || -0m00.14s || -88 ko | -12.39% | -0.01% 0m01.05s | 730628 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m00.99s | 730772 ko || +0m00.06s || -144 ko | +6.06% | -0.01% 0m01.04s | 706760 ko | StandaloneOCamlMain.vo | 0m01.00s | 706608 ko || +0m00.04s || 152 ko | +4.00% | +0.02% 0m01.03s | 707500 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m00.99s | 707524 ko || +0m00.04s || -24 ko | +4.04% | -0.00% 0m01.02s | 693140 ko | Bedrock/Field/Synthesis/Generic/Tactics.vo | 0m00.92s | 693144 ko || +0m00.09s || -4 ko | +10.86% | -0.00% 0m01.02s | 743928 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m01.00s | 743960 ko || +0m00.02s || -32 ko | +2.00% | -0.00% 0m01.00s | 706500 ko | StandaloneHaskellMain.vo | 0m01.06s | 706448 ko || -0m00.06s || 52 ko | -5.66% | +0.00% 0m00.98s | 525328 ko | Stringification/JSON.vo | 0m01.00s | 525164 ko || -0m00.02s || 164 ko | -2.00% | +0.03% 0m00.95s | 649284 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m00.98s | 649236 ko || -0m00.03s || 48 ko | -3.06% | +0.00% 0m00.93s | 699120 ko | Bedrock/Field/Synthesis/Specialized/ReifiedOperation.vo | 0m01.03s | 699080 ko || -0m00.09s || 40 ko | -9.70% | +0.00% 0m00.93s | 528320 ko | Stringification/C.vo | 0m00.89s | 528272 ko || +0m00.04s || 48 ko | +4.49% | +0.00% 0m00.92s | 649300 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m00.96s | 649116 ko || -0m00.03s || 184 ko | -4.16% | +0.02% 0m00.91s | 644524 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m00.82s | 644540 ko || +0m00.09s || -16 ko | +10.97% | -0.00% 0m00.87s | 525128 ko | Stringification/Zig.vo | 0m00.87s | 524968 ko || +0m00.00s || 160 ko | +0.00% | +0.03% 0m00.85s | 524524 ko | Stringification/Rust.vo | 0m00.90s | 524608 ko || -0m00.05s || -84 ko | -5.55% | -0.01% 0m00.82s | 524732 ko | Stringification/Java.vo | 0m00.88s | 524648 ko || -0m00.06s || 84 ko | -6.81% | +0.01% 0m00.70s | 531472 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo | 0m00.67s | 531556 ko || +0m00.02s || -84 ko | +4.47% | -0.01% 0m00.68s | 536180 ko | Bedrock/Field/Stringification/FlattenVarData.vo | 0m00.74s | 536444 ko || -0m00.05s || -264 ko | -8.10% | -0.04% 0m00.64s | 26336 ko | fiat-bedrock2/src/curve25519_64.c | 0m00.64s | 26296 ko || +0m00.00s || 40 ko | +0.00% | +0.15% 0m00.64s | 23696 ko | fiat-go/64/curve25519/curve25519.go | 0m00.64s | 23716 ko || +0m00.00s || -20 ko | +0.00% | -0.08% 0m00.50s | 26012 ko | fiat-json/src/curve25519_64.json | 0m00.44s | 22916 ko || +0m00.06s || 3096 ko | +13.63% | +13.51% 0m00.49s | 20724 ko | fiat-rust/src/curve25519_64.rs | 0m00.48s | 21332 ko || +0m00.01s || -608 ko | +2.08% | -2.85% 0m00.47s | 20712 ko | fiat-c/src/curve25519_64.c | 0m00.46s | 20332 ko || +0m00.00s || 380 ko | +2.17% | +1.86% 0m00.47s | 21088 ko | fiat-zig/src/curve25519_64.zig | 0m00.48s | 21140 ko || -0m00.01s || -52 ko | -2.08% | -0.24% 0m00.35s | 24268 ko | fiat-bedrock2/src/poly1305_32.c | 0m00.34s | 24720 ko || +0m00.00s || -452 ko | +2.94% | -1.82% 0m00.28s | 20124 ko | fiat-go/32/poly1305/poly1305.go | 0m00.28s | 20720 ko || +0m00.00s || -596 ko | +0.00% | -2.87% 0m00.23s | 19996 ko | fiat-java/src/FiatPoly1305.java | 0m00.23s | 20060 ko || +0m00.00s || -64 ko | +0.00% | -0.31% 0m00.23s | 24240 ko | fiat-json/src/poly1305_32.json | 0m00.20s | 20700 ko || +0m00.03s || 3540 ko | +15.00% | +17.10% 0m00.22s | 19680 ko | fiat-zig/src/poly1305_32.zig | 0m00.22s | 19332 ko || +0m00.00s || 348 ko | +0.00% | +1.80% 0m00.21s | 19792 ko | fiat-c/src/poly1305_32.c | 0m00.21s | 20164 ko || +0m00.00s || -372 ko | +0.00% | -1.84% 0m00.21s | 19840 ko | fiat-rust/src/poly1305_32.rs | 0m00.21s | 20040 ko || +0m00.00s || -200 ko | +0.00% | -0.99% 0m00.19s | 20640 ko | fiat-go/64/poly1305/poly1305.go | 0m00.20s | 20724 ko || -0m00.01s || -84 ko | -5.00% | -0.40% 0m00.15s | 22028 ko | fiat-json/src/poly1305_64.json | 0m00.12s | 20404 ko || +0m00.03s || 1624 ko | +25.00% | +7.95% 0m00.14s | 22240 ko | fiat-bedrock2/src/poly1305_64.c | 0m00.16s | 22184 ko || -0m00.01s || 56 ko | -12.49% | +0.25% 0m00.13s | 19356 ko | fiat-rust/src/poly1305_64.rs | 0m00.10s | 19176 ko || +0m00.03s || 180 ko | +30.00% | +0.93% 0m00.13s | 18956 ko | fiat-zig/src/poly1305_64.zig | 0m00.12s | 19156 ko || +0m00.01s || -200 ko | +8.33% | -1.04% 0m00.12s | 19376 ko | fiat-c/src/poly1305_64.c | 0m00.11s | 19376 ko || +0m00.00s || 0 ko | +9.09% | +0.00% ``` </p> </details> 22 January 2022, 20:15:03 UTC
e100e42 Jason Gross 20 January 2022, 15:35:54 UTC More WIP (#1105) 20 January 2022, 15:35:54 UTC
1d94565 Jason Gross 20 January 2022, 15:35:08 UTC `List.rev l` -> `List.rev_append l []` (#1106) Unfortunately, `List.rev` is quadratic in the length of the list. This is a bottleneck in some generated code, so we use the linear-time `List.rev_append _ []`. <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ----------------------------------------------------------------------------------------------------------------------------------------------------------------------- 97m13.31s | 2628008 ko | Total Time / Peak Mem | 100m32.50s | 2631112 ko || -3m19.19s || -3104 ko | -3.30% | -0.11% ----------------------------------------------------------------------------------------------------------------------------------------------------------------------- 6m33.67s | 1081244 ko | fiat-bedrock2/src/p384_32.c | 7m46.00s | 1001716 ko || -1m12.32s || 79528 ko | -15.52% | +7.93% 7m53.66s | 1051572 ko | fiat-json/src/p384_32.json | 8m25.80s | 1142468 ko || -0m32.14s || -90896 ko | -6.35% | -7.95% 0m08.23s | 51328 ko | fiat-json/src/p448_solinas_32.json | 0m32.16s | 66288 ko || -0m23.92s || -14960 ko | -74.40% | -22.56% 0m30.86s | 230648 ko | fiat-json/src/secp256k1_32.json | 0m49.78s | 181408 ko || -0m18.92s || 49240 ko | -38.00% | +27.14% 8m10.16s | 1128908 ko | fiat-rust/src/p384_32.rs | 7m55.11s | 1143724 ko || +0m15.05s || -14816 ko | +3.16% | -1.29% 0m27.89s | 200292 ko | fiat-json/src/p256_32.json | 0m43.79s | 194596 ko || -0m15.89s || 5696 ko | -36.30% | +2.92% 0m10.99s | 1081948 ko | Assembly/Parse/TestAsm.vo | 0m26.40s | 1154020 ko || -0m15.40s || -72072 ko | -58.37% | -6.24% 8m05.89s | 1016344 ko | fiat-go/32/p384/p384.go | 7m52.52s | 1019884 ko || +0m13.37s || -3540 ko | +2.82% | -0.34% 0m22.99s | 143656 ko | fiat-json/src/p434_64.json | 0m34.91s | 161632 ko || -0m11.91s || -17976 ko | -34.14% | -11.12% 6m49.10s | 925644 ko | fiat-zig/src/p384_32.zig | 6m40.11s | 1017248 ko || +0m08.99s || -91604 ko | +2.24% | -9.00% 0m13.53s | 147208 ko | fiat-json/src/p224_32.json | 0m21.45s | 142152 ko || -0m07.92s || 5056 ko | -36.92% | +3.55% 0m33.74s | 213812 ko | fiat-bedrock2/src/secp256k1_32.c | 0m39.30s | 211076 ko || -0m05.55s || 2736 ko | -14.14% | +1.29% 0m10.54s | 97136 ko | fiat-json/src/p384_64.json | 0m16.26s | 98252 ko || -0m05.72s || -1116 ko | -35.17% | -1.13% 0m32.51s | 227552 ko | fiat-bedrock2/src/p256_32.c | 0m35.24s | 215936 ko || -0m02.73s || 11616 ko | -7.74% | +5.37% 0m21.41s | 150904 ko | fiat-go/64/p434/p434.go | 0m23.83s | 153580 ko || -0m02.41s || -2676 ko | -10.15% | -1.74% 0m03.31s | 28980 ko | fiat-json/src/p521_64.json | 0m05.45s | 30756 ko || -0m02.14s || -1776 ko | -39.26% | -5.77% 0m01.80s | 27284 ko | fiat-json/src/curve25519_32.json | 0m04.25s | 30760 ko || -0m02.45s || -3476 ko | -57.64% | -11.30% 0m30.95s | 1725368 ko | ExtractionOCaml/unsaturated_solinas | 0m32.28s | 1730696 ko || -0m01.33s || -5328 ko | -4.12% | -0.30% 0m15.34s | 144072 ko | fiat-bedrock2/src/p224_32.c | 0m17.24s | 134840 ko || -0m01.89s || 9232 ko | -11.02% | +6.84% 0m12.71s | 135076 ko | fiat-zig/src/p224_32.zig | 0m14.00s | 132136 ko || -0m01.28s || 2940 ko | -9.21% | +2.22% 0m12.15s | 94228 ko | fiat-bedrock2/src/p384_64.c | 0m13.15s | 105940 ko || -0m01.00s || -11712 ko | -7.60% | -11.05% 0m02.59s | 41680 ko | fiat-json/src/secp256k1_64.json | 0m04.23s | 44748 ko || -0m01.64s || -3068 ko | -38.77% | -6.85% 0m01.96s | 27332 ko | fiat-json/src/p448_solinas_64.json | 0m03.91s | 28960 ko || -0m01.95s || -1628 ko | -49.87% | -5.62% 0m01.88s | 42944 ko | fiat-json/src/p256_64.json | 0m03.19s | 40536 ko || -0m01.31s || 2408 ko | -41.06% | +5.94% 0m01.83s | 39792 ko | fiat-json/src/p224_64.json | 0m03.27s | 42840 ko || -0m01.43s || -3048 ko | -44.03% | -7.11% 8m01.73s | 1084084 ko | fiat-c/src/p384_32.c | 8m00.81s | 1012692 ko || +0m00.92s || 71392 ko | +0.19% | +7.04% 7m43.65s | 919980 ko | fiat-java/src/FiatP384.java | 7m43.61s | 990208 ko || +0m00.03s || -70228 ko | +0.00% | -7.09% 1m46.30s | 1376280 ko | Fancy/Barrett256.vo | 1m47.03s | 1376168 ko || -0m00.73s || 112 ko | -0.68% | +0.00% 1m41.27s | 1058136 ko | Bedrock/Field/Synthesis/Examples/X25519_64.vo | 1m41.38s | 1057976 ko || -0m00.10s || 160 ko | -0.10% | +0.01% 1m39.42s | 1534200 ko | SlowPrimeSynthesisExamples.vo | 1m39.28s | 1595764 ko || +0m00.14s || -61564 ko | +0.14% | -3.85% 1m15.10s | 1131812 ko | UnsaturatedSolinasHeuristics/Tests.vo | 1m14.96s | 1131736 ko || +0m00.13s || 76 ko | +0.18% | +0.00% 1m13.46s | 1185228 ko | Bedrock/End2End/X25519/Field25519.vo | 1m13.07s | 1184996 ko || +0m00.39s || 232 ko | +0.53% | +0.01% 1m01.05s | 1328624 ko | Bedrock/Field/Synthesis/Examples/p224_64.vo | 1m00.88s | 1328812 ko || +0m00.16s || -188 ko | +0.27% | -0.01% 0m59.23s | 1301292 ko | Bedrock/Field/Synthesis/Examples/p256_64.vo | 0m59.13s | 1301396 ko || +0m00.09s || -104 ko | +0.16% | -0.00% 0m52.97s | 2462464 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m52.36s | 2462316 ko || +0m00.60s || 148 ko | +1.16% | +0.00% 0m49.34s | 2628008 ko | ExtractionOCaml/word_by_word_montgomery | 0m49.66s | 2631112 ko || -0m00.31s || -3104 ko | -0.64% | -0.11% 0m46.76s | 1277196 ko | Fancy/Montgomery256.vo | 0m47.13s | 1277420 ko || -0m00.37s || -224 ko | -0.78% | -0.01% 0m44.90s | 939548 ko | Assembly/WithBedrock/SymbolicProofs.vo | 0m45.17s | 939488 ko || -0m00.27s || 60 ko | -0.59% | +0.00% 0m40.16s | 2333444 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m39.57s | 2331288 ko || +0m00.58s || 2156 ko | +1.49% | +0.09% 0m39.05s | 2217188 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m38.82s | 2217536 ko || +0m00.22s || -348 ko | +0.59% | -0.01% 0m34.61s | 1739412 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m35.07s | 1741292 ko || -0m00.46s || -1880 ko | -1.31% | -0.10% 0m33.06s | 913448 ko | Assembly/WithBedrock/Proofs.vo | 0m32.97s | 913500 ko || +0m00.09s || -52 ko | +0.27% | -0.00% 0m32.88s | 1145092 ko | Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo | 0m32.94s | 1145040 ko || -0m00.05s || 52 ko | -0.18% | +0.00% 0m32.59s | 1407024 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m32.54s | 1420004 ko || +0m00.05s || -12980 ko | +0.15% | -0.91% 0m32.16s | 1402252 ko | ExtractionOCaml/bedrock2_base_conversion | 0m32.49s | 1402328 ko || -0m00.33s || -76 ko | -1.01% | -0.00% 0m31.85s | 1088792 ko | Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo | 0m31.77s | 1089044 ko || +0m00.08s || -252 ko | +0.25% | -0.02% 0m31.59s | 192420 ko | fiat-zig/src/secp256k1_32.zig | 0m31.35s | 220292 ko || +0m00.23s || -27872 ko | +0.76% | -12.65% 0m31.50s | 215508 ko | fiat-java/src/FiatSecp256K1.java | 0m31.26s | 232040 ko || +0m00.23s || -16532 ko | +0.76% | -7.12% 0m30.70s | 216860 ko | fiat-go/32/secp256k1/secp256k1.go | 0m31.56s | 211696 ko || -0m00.85s || 5164 ko | -2.72% | +2.43% 0m30.47s | 205812 ko | fiat-rust/src/secp256k1_32.rs | 0m30.43s | 214660 ko || +0m00.03s || -8848 ko | +0.13% | -4.12% 0m30.23s | 211036 ko | fiat-zig/src/p256_32.zig | 0m30.04s | 232456 ko || +0m00.19s || -21420 ko | +0.63% | -9.21% 0m30.08s | 217912 ko | fiat-c/src/secp256k1_32.c | 0m30.41s | 213544 ko || -0m00.33s || 4368 ko | -1.08% | +2.04% 0m29.98s | 1240368 ko | ExtractionOCaml/base_conversion | 0m29.40s | 1223744 ko || +0m00.58s || 16624 ko | +1.97% | +1.35% 0m29.59s | 218024 ko | fiat-rust/src/p256_32.rs | 0m29.56s | 223756 ko || +0m00.03s || -5732 ko | +0.10% | -2.56% 0m29.54s | 212092 ko | fiat-go/32/p256/p256.go | 0m30.22s | 218336 ko || -0m00.67s || -6244 ko | -2.25% | -2.85% 0m29.36s | 1233276 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m29.42s | 1233416 ko || -0m00.06s || -140 ko | -0.20% | -0.01% 0m29.32s | 192216 ko | fiat-c/src/p256_32.c | 0m29.30s | 181852 ko || +0m00.01s || 10364 ko | +0.06% | +5.69% 0m28.94s | 1233756 ko | ExtractionOCaml/saturated_solinas | 0m29.66s | 1280124 ko || -0m00.71s || -46368 ko | -2.42% | -3.62% 0m27.65s | 231692 ko | fiat-java/src/FiatP256.java | 0m28.29s | 221764 ko || -0m00.64s || 9928 ko | -2.26% | +4.47% 0m27.53s | 843616 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m27.54s | 843840 ko || -0m00.00s || -224 ko | -0.03% | -0.02% 0m26.69s | 1233172 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m26.77s | 1233276 ko || -0m00.07s || -104 ko | -0.29% | -0.00% 0m25.44s | 1707472 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m25.16s | 1707444 ko || +0m00.28s || 28 ko | +1.11% | +0.00% 0m24.76s | 156092 ko | fiat-bedrock2/src/p434_64.c | 0m25.18s | 150240 ko || -0m00.41s || 5852 ko | -1.66% | +3.89% 0m24.68s | 865452 ko | Bedrock/Field/Synthesis/Examples/LadderStep.vo | 0m24.80s | 865464 ko || -0m00.12s || -12 ko | -0.48% | -0.00% 0m24.15s | 1693768 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m24.08s | 1693724 ko || +0m00.07s || 44 ko | +0.29% | +0.00% 0m23.32s | 162920 ko | fiat-rust/src/p434_64.rs | 0m23.09s | 136092 ko || +0m00.23s || 26828 ko | +0.99% | +19.71% 0m23.05s | 136500 ko | fiat-zig/src/p434_64.zig | 0m22.86s | 143812 ko || +0m00.19s || -7312 ko | +0.83% | -5.08% 0m22.57s | 145960 ko | fiat-c/src/p434_64.c | 0m22.61s | 160852 ko || -0m00.03s || -14892 ko | -0.17% | -9.25% 0m21.52s | 841508 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m21.49s | 841584 ko || +0m00.03s || -76 ko | +0.13% | -0.00% 0m20.98s | 1666096 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m21.08s | 1666132 ko || -0m00.09s || -36 ko | -0.47% | -0.00% 0m20.79s | 1670640 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m20.88s | 1670448 ko || -0m00.08s || 192 ko | -0.43% | +0.01% 0m20.07s | 1841684 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m19.96s | 1843676 ko || +0m00.10s || -1992 ko | +0.55% | -0.10% 0m19.78s | 1614952 ko | ExtractionOCaml/base_conversion.ml | 0m19.85s | 1614764 ko || -0m00.07s || 188 ko | -0.35% | +0.01% 0m19.41s | 1604808 ko | ExtractionOCaml/saturated_solinas.ml | 0m19.52s | 1604704 ko || -0m00.10s || 104 ko | -0.56% | +0.00% 0m18.86s | 824252 ko | Bedrock/Field/Synthesis/Examples/X1305_32.vo | 0m18.87s | 824340 ko || -0m00.01s || -88 ko | -0.05% | -0.01% 0m18.55s | 1941360 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs | 0m18.62s | 1941136 ko || -0m00.07s || 224 ko | -0.37% | +0.01% 0m18.54s | 1740824 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m18.69s | 1740444 ko || -0m00.15s || 380 ko | -0.80% | +0.02% 0m17.96s | 1778524 ko | ExtractionHaskell/word_by_word_montgomery.hs | 0m17.95s | 1778672 ko || +0m00.01s || -148 ko | +0.05% | -0.00% 0m16.64s | 780392 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m16.67s | 780456 ko || -0m00.03s || -64 ko | -0.17% | -0.00% 0m16.30s | 802308 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m16.30s | 802372 ko || +0m00.00s || -64 ko | +0.00% | -0.00% 0m15.68s | 910168 ko | StandaloneDebuggingExamples.vo | 0m15.87s | 910920 ko || -0m00.18s || -752 ko | -1.19% | -0.08% 0m14.46s | 794764 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m14.47s | 794656 ko || -0m00.00s || 108 ko | -0.06% | +0.01% 0m14.44s | 127640 ko | fiat-java/src/FiatP224.java | 0m13.88s | 143460 ko || +0m00.55s || -15820 ko | +4.03% | -11.02% 0m14.17s | 1492216 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs | 0m13.98s | 1492216 ko || +0m00.18s || 0 ko | +1.35% | +0.00% 0m14.17s | 139556 ko | fiat-rust/src/p224_32.rs | 0m13.88s | 147852 ko || +0m00.28s || -8296 ko | +2.08% | -5.61% 0m13.79s | 129584 ko | fiat-go/32/p224/p224.go | 0m14.05s | 133732 ko || -0m00.26s || -4148 ko | -1.85% | -3.10% 0m13.65s | 132008 ko | fiat-c/src/p224_32.c | 0m13.94s | 138228 ko || -0m00.28s || -6220 ko | -2.08% | -4.49% 0m13.11s | 1430580 ko | ExtractionHaskell/unsaturated_solinas.hs | 0m13.26s | 1430484 ko || -0m00.15s || 96 ko | -1.13% | +0.00% 0m12.66s | 1379452 ko | ExtractionHaskell/bedrock2_base_conversion.hs | 0m12.59s | 1379652 ko || +0m00.07s || -200 ko | +0.55% | -0.01% 0m12.57s | 1385972 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs | 0m12.71s | 1385880 ko || -0m00.14s || 92 ko | -1.10% | +0.00% 0m12.26s | 1352904 ko | ExtractionHaskell/base_conversion.hs | 0m12.37s | 1352756 ko || -0m00.10s || 148 ko | -0.88% | +0.01% 0m12.06s | 1381888 ko | ExtractionHaskell/saturated_solinas.hs | 0m11.40s | 1381992 ko || +0m00.66s || -104 ko | +5.78% | -0.00% 0m11.68s | 857572 ko | PushButtonSynthesis/SmallExamples.vo | 0m11.73s | 857624 ko || -0m00.05s || -52 ko | -0.42% | -0.00% 0m11.53s | 608184 ko | Assembly/Symbolic.vo | 0m11.60s | 608320 ko || -0m00.07s || -136 ko | -0.60% | -0.02% 0m10.88s | 589096 ko | Stringification/IR.vo | 0m10.90s | 589004 ko || -0m00.01s || 92 ko | -0.18% | +0.01% 0m10.86s | 87512 ko | fiat-go/64/p384/p384.go | 0m10.82s | 90840 ko || +0m00.03s || -3328 ko | +0.36% | -3.66% 0m10.76s | 772068 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m10.84s | 771972 ko || -0m00.08s || 96 ko | -0.73% | +0.01% 0m10.72s | 103140 ko | fiat-rust/src/p384_64.rs | 0m10.67s | 91100 ko || +0m00.05s || 12040 ko | +0.46% | +13.21% 0m10.71s | 97196 ko | fiat-zig/src/p384_64.zig | 0m10.75s | 94688 ko || -0m00.03s || 2508 ko | -0.37% | +2.64% 0m10.49s | 96236 ko | fiat-c/src/p384_64.c | 0m10.59s | 96520 ko || -0m00.09s || -284 ko | -0.94% | -0.29% 0m08.33s | 750552 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m08.29s | 750608 ko || +0m00.04s || -56 ko | +0.48% | -0.00% 0m08.31s | 47320 ko | fiat-c/src/p448_solinas_32.c | 0m08.42s | 47668 ko || -0m00.10s || -348 ko | -1.30% | -0.73% 0m08.20s | 46316 ko | fiat-zig/src/p448_solinas_32.zig | 0m08.14s | 46484 ko || +0m00.05s || -168 ko | +0.73% | -0.36% 0m08.17s | 688468 ko | PushButtonSynthesis/BaseConversion.vo | 0m08.18s | 688300 ko || -0m00.00s || 168 ko | -0.12% | +0.02% 0m08.16s | 46276 ko | fiat-rust/src/p448_solinas_32.rs | 0m08.10s | 44208 ko || +0m00.06s || 2068 ko | +0.74% | +4.67% 0m06.62s | 688800 ko | PushButtonSynthesis/Primitives.vo | 0m06.72s | 688680 ko || -0m00.09s || 120 ko | -1.48% | +0.01% 0m05.42s | 733912 ko | Bedrock/Field/Synthesis/Examples/EncodeDecode.vo | 0m05.44s | 734144 ko || -0m00.02s || -232 ko | -0.36% | -0.03% 0m05.17s | 638172 ko | BoundsPipeline.vo | 0m05.40s | 638088 ko || -0m00.23s || 84 ko | -4.25% | +0.01% 0m04.80s | 679740 ko | PushButtonSynthesis/BarrettReduction.vo | 0m04.71s | 679500 ko || +0m00.08s || 240 ko | +1.91% | +0.03% 0m03.93s | 39472 ko | fiat-bedrock2/src/p521_64.c | 0m04.04s | 39720 ko || -0m00.10s || -248 ko | -2.72% | -0.62% 0m03.74s | 740320 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m03.73s | 740560 ko || +0m00.01s || -240 ko | +0.26% | -0.03% 0m03.67s | 32888 ko | fiat-go/64/p521/p521.go | 0m04.16s | 33012 ko || -0m00.49s || -124 ko | -11.77% | -0.37% 0m03.46s | 721284 ko | Bedrock/Field/Synthesis/Examples/MulTwice.vo | 0m03.55s | 721488 ko || -0m00.08s || -204 ko | -2.53% | -0.02% 0m03.18s | 26784 ko | fiat-c/src/p521_64.c | 0m02.89s | 25464 ko || +0m00.29s || 1320 ko | +10.03% | +5.18% 0m03.15s | 26756 ko | fiat-rust/src/p521_64.rs | 0m02.92s | 26776 ko || +0m00.23s || -20 ko | +7.87% | -0.07% 0m03.11s | 688320 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.18s | 688624 ko || -0m00.07s || -304 ko | -2.20% | -0.04% 0m03.09s | 46776 ko | fiat-bedrock2/src/secp256k1_64.c | 0m03.32s | 43576 ko || -0m00.23s || 3200 ko | -6.92% | +7.34% 0m03.01s | 705260 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m02.97s | 705228 ko || +0m00.03s || 32 ko | +1.34% | +0.00% 0m02.86s | 710548 ko | CLI.vo | 0m02.77s | 710484 ko || +0m00.08s || 64 ko | +3.24% | +0.00% 0m02.82s | 26760 ko | fiat-zig/src/p521_64.zig | 0m02.90s | 25500 ko || -0m00.08s || 1260 ko | -2.75% | +4.94% 0m02.79s | 686496 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m02.85s | 686600 ko || -0m00.06s || -104 ko | -2.10% | -0.01% 0m02.78s | 41652 ko | fiat-bedrock2/src/p448_solinas_64.c | 0m02.94s | 42496 ko || -0m00.16s || -844 ko | -5.44% | -1.98% 0m02.70s | 44612 ko | fiat-go/64/secp256k1/secp256k1.go | 0m02.72s | 45080 ko || -0m00.02s || -468 ko | -0.73% | -1.03% 0m02.66s | 37188 ko | fiat-bedrock2/src/curve25519_32.c | 0m02.81s | 38160 ko || -0m00.14s || -972 ko | -5.33% | -2.54% 0m02.63s | 41296 ko | fiat-zig/src/secp256k1_64.zig | 0m02.58s | 40992 ko || +0m00.04s || 304 ko | +1.93% | +0.74% 0m02.58s | 39944 ko | fiat-rust/src/secp256k1_64.rs | 0m02.60s | 44500 ko || -0m00.02s || -4556 ko | -0.76% | -10.23% 0m02.55s | 40488 ko | fiat-c/src/secp256k1_64.c | 0m02.61s | 41436 ko || -0m00.06s || -948 ko | -2.29% | -2.28% 0m02.55s | 35304 ko | fiat-go/64/p448solinas/p448solinas.go | 0m02.77s | 33140 ko || -0m00.22s || 2164 ko | -7.94% | +6.52% 0m02.41s | 42840 ko | fiat-bedrock2/src/p224_64.c | 0m02.61s | 41404 ko || -0m00.19s || 1436 ko | -7.66% | +3.46% 0m02.31s | 43652 ko | fiat-bedrock2/src/p256_64.c | 0m02.46s | 46180 ko || -0m00.14s || -2528 ko | -6.09% | -5.47% 0m02.14s | 25184 ko | fiat-go/32/curve25519/curve25519.go | 0m02.16s | 24720 ko || -0m00.02s || 464 ko | -0.92% | +1.87% 0m02.05s | 39216 ko | fiat-go/64/p224/p224.go | 0m02.09s | 41476 ko || -0m00.04s || -2260 ko | -1.91% | -5.44% 0m02.03s | 43028 ko | fiat-go/64/p256/p256.go | 0m02.00s | 41476 ko || +0m00.02s || 1552 ko | +1.49% | +3.74% 0m01.97s | 26788 ko | fiat-c/src/p448_solinas_64.c | 0m02.01s | 25484 ko || -0m00.03s || 1304 ko | -1.99% | +5.11% 0m01.96s | 42060 ko | fiat-c/src/p224_64.c | 0m01.98s | 41180 ko || -0m00.02s || 880 ko | -1.01% | +2.13% 0m01.96s | 25428 ko | fiat-rust/src/p448_solinas_64.rs | 0m02.00s | 25584 ko || -0m00.04s || -156 ko | -2.00% | -0.60% 0m01.94s | 43456 ko | fiat-rust/src/p224_64.rs | 0m01.98s | 44756 ko || -0m00.04s || -1300 ko | -2.02% | -2.90% 0m01.88s | 42792 ko | fiat-c/src/p256_64.c | 0m01.95s | 42096 ko || -0m00.07s || 696 ko | -3.58% | +1.65% 0m01.88s | 44288 ko | fiat-rust/src/p256_64.rs | 0m01.81s | 37416 ko || +0m00.06s || 6872 ko | +3.86% | +18.36% 0m01.88s | 44600 ko | fiat-zig/src/p224_64.zig | 0m01.95s | 43472 ko || -0m00.07s || 1128 ko | -3.58% | +2.59% 0m01.88s | 25624 ko | fiat-zig/src/p448_solinas_64.zig | 0m02.00s | 24608 ko || -0m00.12s || 1016 ko | -6.00% | +4.12% 0m01.82s | 639300 ko | Bedrock/Field/Translation/Cmd.vo | 0m01.85s | 639372 ko || -0m00.03s || -72 ko | -1.62% | -0.01% 0m01.81s | 38076 ko | fiat-zig/src/p256_64.zig | 0m01.93s | 43296 ko || -0m00.11s || -5220 ko | -6.21% | -12.05% 0m01.79s | 23716 ko | fiat-rust/src/curve25519_32.rs | 0m01.79s | 24644 ko || +0m00.00s || -928 ko | +0.00% | -3.76% 0m01.78s | 24432 ko | fiat-c/src/curve25519_32.c | 0m01.85s | 24132 ko || -0m00.07s || 300 ko | -3.78% | +1.24% 0m01.77s | 25356 ko | fiat-java/src/FiatCurve25519.java | 0m01.85s | 24648 ko || -0m00.08s || 708 ko | -4.32% | +2.87% 0m01.77s | 25340 ko | fiat-zig/src/curve25519_32.zig | 0m01.84s | 25944 ko || -0m00.07s || -604 ko | -3.80% | -2.32% 0m01.76s | 532812 ko | Stringification/Language.vo | 0m01.66s | 533108 ko || +0m00.10s || -296 ko | +6.02% | -0.05% 0m01.75s | 589800 ko | CompilersTestCases.vo | 0m01.78s | 589528 ko || -0m00.03s || 272 ko | -1.68% | +0.04% 0m01.50s | 633952 ko | Bedrock/Field/Translation/Func.vo | 0m01.50s | 633716 ko || +0m00.00s || 236 ko | +0.00% | +0.03% 0m01.50s | 718848 ko | Rewriter/PerfTesting/Core.vo | 0m01.49s | 718916 ko || +0m00.01s || -68 ko | +0.67% | -0.00% 0m01.42s | 468988 ko | Assembly/Parse.vo | 0m01.43s | 468876 ko || -0m00.01s || 112 ko | -0.69% | +0.02% 0m01.27s | 527636 ko | Stringification/Go.vo | 0m01.28s | 527480 ko || -0m00.01s || 156 ko | -0.78% | +0.02% 0m01.22s | 688684 ko | Bedrock/Field/Stringification/Stringification.vo | 0m01.24s | 688568 ko || -0m00.02s || 116 ko | -1.61% | +0.01% 0m01.19s | 581076 ko | Assembly/Equivalence.vo | 0m01.22s | 581008 ko || -0m00.03s || 68 ko | -2.45% | +0.01% 0m01.13s | 743416 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m01.06s | 743444 ko || +0m00.06s || -28 ko | +6.60% | -0.00% 0m01.11s | 711800 ko | Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.vo | 0m01.18s | 711860 ko || -0m00.06s || -60 ko | -5.93% | -0.00% 0m01.10s | 730332 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m01.12s | 730484 ko || -0m00.02s || -152 ko | -1.78% | -0.02% 0m01.09s | 694460 ko | Bedrock/Field/Synthesis/Generic/Operation.vo | 0m01.07s | 694264 ko || +0m00.02s || 196 ko | +1.86% | +0.02% 0m01.09s | 725344 ko | Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.vo | 0m01.16s | 725412 ko || -0m00.06s || -68 ko | -6.03% | -0.00% 0m01.08s | 743680 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m01.12s | 743404 ko || -0m00.04s || 276 ko | -3.57% | +0.03% 0m01.07s | 693280 ko | Bedrock/Field/Synthesis/Generic/Tactics.vo | 0m01.07s | 692968 ko || +0m00.00s || 312 ko | +0.00% | +0.04% 0m01.04s | 699028 ko | Bedrock/Field/Synthesis/Specialized/ReifiedOperation.vo | 0m01.08s | 699152 ko || -0m00.04s || -124 ko | -3.70% | -0.01% 0m01.04s | 706628 ko | StandaloneOCamlMain.vo | 0m01.12s | 706540 ko || -0m00.08s || 88 ko | -7.14% | +0.01% 0m01.02s | 697000 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m01.13s | 697012 ko || -0m00.10s || -12 ko | -9.73% | -0.00% 0m01.00s | 707464 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m01.13s | 707508 ko || -0m00.12s || -44 ko | -11.50% | -0.00% 0m01.00s | 692764 ko | Bedrock/Field/Synthesis/Specialized/Tactics.vo | 0m00.85s | 693076 ko || +0m00.15s || -312 ko | +17.64% | -0.04% 0m01.00s | 706284 ko | StandaloneHaskellMain.vo | 0m01.01s | 706196 ko || -0m00.01s || 88 ko | -0.99% | +0.01% 0m00.95s | 649016 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m00.88s | 649052 ko || +0m00.06s || -36 ko | +7.95% | -0.00% 0m00.95s | 525208 ko | Stringification/JSON.vo | 0m00.94s | 525212 ko || +0m00.01s || -4 ko | +1.06% | -0.00% 0m00.89s | 649240 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m00.95s | 649268 ko || -0m00.05s || -28 ko | -6.31% | -0.00% 0m00.86s | 528164 ko | Stringification/C.vo | 0m00.94s | 528260 ko || -0m00.07s || -96 ko | -8.51% | -0.01% 0m00.83s | 644608 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m00.94s | 644528 ko || -0m00.10s || 80 ko | -11.70% | +0.01% 0m00.82s | 524472 ko | Stringification/Java.vo | 0m00.81s | 524636 ko || +0m00.00s || -164 ko | +1.23% | -0.03% 0m00.78s | 524652 ko | Stringification/Rust.vo | 0m00.83s | 524508 ko || -0m00.04s || 144 ko | -6.02% | +0.02% 0m00.78s | 525028 ko | Stringification/Zig.vo | 0m00.89s | 525024 ko || -0m00.10s || 4 ko | -12.35% | +0.00% 0m00.73s | 536444 ko | Bedrock/Field/Stringification/FlattenVarData.vo | 0m00.72s | 536220 ko || +0m00.01s || 224 ko | +1.38% | +0.04% 0m00.68s | 531384 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo | 0m00.68s | 531412 ko || +0m00.00s || -28 ko | +0.00% | -0.00% 0m00.64s | 26312 ko | fiat-bedrock2/src/curve25519_64.c | 0m00.66s | 26228 ko || -0m00.02s || 84 ko | -3.03% | +0.32% 0m00.62s | 23372 ko | fiat-go/64/curve25519/curve25519.go | 0m00.66s | 23228 ko || -0m00.04s || 144 ko | -6.06% | +0.61% 0m00.59s | 420680 ko | Util/Strings/ParseArithmetic.vo | 0m00.61s | 420668 ko || -0m00.02s || 12 ko | -3.27% | +0.00% 0m00.56s | 432300 ko | Util/Arg.vo | 0m00.60s | 432416 ko || -0m00.03s || -116 ko | -6.66% | -0.02% 0m00.47s | 20296 ko | fiat-c/src/curve25519_64.c | 0m00.48s | 20956 ko || -0m00.01s || -660 ko | -2.08% | -3.14% 0m00.47s | 21536 ko | fiat-rust/src/curve25519_64.rs | 0m00.49s | 21004 ko || -0m00.02s || 532 ko | -4.08% | +2.53% 0m00.47s | 21208 ko | fiat-zig/src/curve25519_64.zig | 0m00.48s | 21280 ko || -0m00.01s || -72 ko | -2.08% | -0.33% 0m00.46s | 23068 ko | fiat-json/src/curve25519_64.json | 0m00.90s | 23324 ko || -0m00.44s || -256 ko | -48.88% | -1.09% 0m00.45s | 431200 ko | Util/Strings/NamingConventions.vo | 0m00.45s | 431132 ko || +0m00.00s || 68 ko | +0.00% | +0.01% 0m00.44s | 455136 ko | Util/MSetPositive/Show.vo | 0m00.43s | 455088 ko || +0m00.01s || 48 ko | +2.32% | +0.01% 0m00.40s | 415744 ko | Util/Strings/ParseArithmeticToTaps.vo | 0m00.51s | 415732 ko || -0m00.10s || 12 ko | -21.56% | +0.00% 0m00.40s | 430304 ko | Util/Strings/Show.vo | 0m00.42s | 430256 ko || -0m00.01s || 48 ko | -4.76% | +0.01% 0m00.34s | 24848 ko | fiat-bedrock2/src/poly1305_32.c | 0m00.39s | 24072 ko || -0m00.04s || 776 ko | -12.82% | +3.22% 0m00.30s | 411096 ko | Util/Strings/String.vo | 0m00.24s | 411196 ko || +0m00.06s || -100 ko | +25.00% | -0.02% 0m00.29s | 20520 ko | fiat-go/32/poly1305/poly1305.go | 0m00.31s | 20192 ko || -0m00.02s || 328 ko | -6.45% | +1.62% 0m00.23s | 317528 ko | Util/ZRange/Show.vo | 0m00.18s | 317392 ko || +0m00.05s || 136 ko | +27.77% | +0.04% 0m00.22s | 319836 ko | Util/MSets/Show.vo | 0m00.25s | 319960 ko || -0m00.03s || -124 ko | -12.00% | -0.03% 0m00.22s | 19892 ko | fiat-java/src/FiatPoly1305.java | 0m00.23s | 19668 ko || -0m00.01s || 224 ko | -4.34% | +1.13% 0m00.21s | 299052 ko | Bedrock/Field/Common/Names/VarnameGenerator.vo | 0m00.23s | 298832 ko || -0m00.02s || 220 ko | -8.69% | +0.07% 0m00.21s | 285648 ko | Util/Strings/Parse/Common.vo | 0m00.22s | 285692 ko || -0m00.01s || -44 ko | -4.54% | -0.01% 0m00.21s | 20636 ko | fiat-json/src/poly1305_32.json | 0m00.43s | 21280 ko || -0m00.22s || -644 ko | -51.16% | -3.02% 0m00.21s | 19288 ko | fiat-zig/src/poly1305_32.zig | 0m00.21s | 19852 ko || +0m00.00s || -564 ko | +0.00% | -2.84% 0m00.20s | 19908 ko | fiat-rust/src/poly1305_32.rs | 0m00.23s | 19872 ko || -0m00.03s || 36 ko | -13.04% | +0.18% 0m00.18s | 319112 ko | Util/ErrorT/Show.vo | 0m00.19s | 319084 ko || -0m00.01s || 28 ko | -5.26% | +0.00% 0m00.18s | 20536 ko | fiat-go/64/poly1305/poly1305.go | 0m00.18s | 20384 ko || +0m00.00s || 152 ko | +0.00% | +0.74% 0m00.17s | 22008 ko | fiat-bedrock2/src/poly1305_64.c | 0m00.17s | 21912 ko || +0m00.00s || 96 ko | +0.00% | +0.43% 0m00.17s | 19884 ko | fiat-c/src/poly1305_32.c | 0m00.21s | 19936 ko || -0m00.03s || -52 ko | -19.04% | -0.26% 0m00.13s | 19356 ko | fiat-c/src/poly1305_64.c | 0m00.14s | 19152 ko || -0m00.01s || 204 ko | -7.14% | +1.06% 0m00.12s | 18760 ko | fiat-rust/src/poly1305_64.rs | 0m00.12s | 19184 ko || +0m00.00s || -424 ko | +0.00% | -2.21% 0m00.11s | 19024 ko | fiat-zig/src/poly1305_64.zig | 0m00.13s | 18752 ko || -0m00.02s || 272 ko | -15.38% | +1.45% 0m00.10s | 20380 ko | fiat-json/src/poly1305_64.json | 0m00.21s | 20240 ko || -0m00.10s || 140 ko | -52.38% | +0.69% ``` </p> </details> 20 January 2022, 15:35:08 UTC
b67ab7f Jason Gross 19 January 2022, 22:27:27 UTC Add `encode_word` and `copy` to PushButtonSynthesis (#1103) * Add `encode_word` and `copy` to PushButtonSynthesis * Add copy_correct * Fix unfolding 19 January 2022, 22:27:27 UTC
5f31580 Jason Gross 19 January 2022, 21:46:00 UTC Enable native compute profiling in UnsaturatedSolinasHeuristics/Tests 19 January 2022, 21:46:00 UTC
4145a70 Jason Gross 19 January 2022, 21:09:12 UTC Empty commit for timing info <details><summary>Timing Diff</summary> <p> ``` Time | Peak Mem | File Name --------------------------------------------------------------------------------------------------------------------------------- 193m08.18s | 3686620 ko | Total Time / Peak Mem --------------------------------------------------------------------------------------------------------------------------------- 9m19.30s | 1142192 ko | fiat-json/src/p384_32.json 8m07.07s | 1012840 ko | fiat-c/src/p384_32.c 7m51.23s | 1143352 ko | fiat-rust/src/p384_32.rs 7m49.14s | 1019984 ko | fiat-go/32/p384/p384.go 7m43.54s | 990316 ko | fiat-java/src/FiatP384.java 7m42.78s | 1001920 ko | fiat-bedrock2/src/p384_32.c 7m12.20s | 1017308 ko | fiat-zig/src/p384_32.zig 7m11.67s | 2055812 ko | Curves/Weierstrass/AffineProofs.vo 4m19.48s | 3686620 ko | Curves/EdwardsMontgomery.vo 4m18.92s | 1388544 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo 3m08.22s | 1862356 ko | Rewriter/Passes/ArithWithCasts.vo 3m05.32s | 807520 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.vo 2m59.55s | 1479820 ko | Curves/Weierstrass/Projective.vo 2m58.66s | 1499584 ko | Curves/Montgomery/XZProofs.vo 2m38.03s | 1109872 ko | Fancy/Compiler.vo 2m35.17s | 1305828 ko | Curves/Montgomery/AffineProofs.vo 2m26.60s | 1647472 ko | Rewriter/Passes/NBE.vo 2m19.10s | 1042220 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.vo 2m09.63s | 1239244 ko | Rewriter/Rewriter/Wf.vo 2m05.89s | 1627864 ko | Rewriter/Passes/ToFancyWithCasts.vo 2m02.80s | 2711008 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.vo 1m55.30s | 905496 ko | AbstractInterpretation/Wf.vo 1m46.58s | 1375916 ko | Fancy/Barrett256.vo 1m40.24s | 1058108 ko | Bedrock/Field/Synthesis/Examples/X25519_64.vo 1m36.91s | 1595780 ko | SlowPrimeSynthesisExamples.vo 1m24.89s | 922556 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/Softmul.vo 1m18.68s | 438948 ko | Spec/Test/X25519.vo 1m18.43s | 720168 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/MMIO.vo 1m16.68s | 1587848 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.vo 1m14.13s | 1131864 ko | UnsaturatedSolinasHeuristics/Tests.vo 1m13.32s | 1196448 ko | Bedrock/End2End/X25519/Field25519.vo 1m03.89s | 752752 ko | Rewriter/Language/UnderLetsProofs.vo 1m03.78s | 965964 ko | Curves/Weierstrass/Jacobian.vo 0m59.53s | 1328880 ko | Bedrock/Field/Synthesis/Examples/p224_64.vo 0m59.24s | 842844 ko | AbstractInterpretation/ZRangeProofs.vo 0m58.31s | 1301320 ko | Bedrock/Field/Synthesis/Examples/p256_64.vo 0m58.08s | 970024 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo 0m57.01s | 725600 ko | AbstractInterpretation/Proofs.vo 0m55.83s | 729492 ko | Rewriter/RulesProofs.vo 0m53.98s | 970928 ko | Rewriter/Rewriter/InterpProofs.vo 0m53.58s | 1082876 ko | Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo 0m52.37s | 2462444 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery 0m51.06s | 939168 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.vo 0m50.02s | 181180 ko | fiat-json/src/secp256k1_32.json 0m49.94s | 1103760 ko | Rewriter/Passes/MultiRetSplit.vo 0m49.77s | 2631236 ko | ExtractionOCaml/word_by_word_montgomery 0m49.50s | 795920 ko | Rewriter/Rewriter/ProofsCommon.vo 0m48.12s | 1070936 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo 0m47.50s | 581308 ko | Demo.vo 0m47.34s | 638640 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/Spilling.vo 0m46.70s | 934668 ko | Assembly/WithBedrock/SymbolicProofs.vo 0m46.02s | 1272196 ko | Fancy/Montgomery256.vo 0m45.41s | 1156052 ko | Rewriter/Passes/Arith.vo 0m44.19s | 194688 ko | fiat-json/src/p256_32.json 0m43.97s | 558944 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricSane.vo 0m39.43s | 2339364 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml 0m38.53s | 211044 ko | fiat-bedrock2/src/secp256k1_32.c 0m38.06s | 2223084 ko | ExtractionOCaml/word_by_word_montgomery.ml 0m36.65s | 1100044 ko | Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo 0m35.11s | 1741412 ko | ExtractionOCaml/bedrock2_unsaturated_solinas 0m34.33s | 215688 ko | fiat-bedrock2/src/p256_32.c 0m33.06s | 1729984 ko | ExtractionOCaml/unsaturated_solinas 0m32.70s | 909532 ko | Assembly/WithBedrock/Proofs.vo 0m32.55s | 602636 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvLiterals.vo 0m32.47s | 1407932 ko | ExtractionOCaml/bedrock2_saturated_solinas 0m32.34s | 1402268 ko | ExtractionOCaml/bedrock2_base_conversion 0m32.27s | 66544 ko | fiat-json/src/p448_solinas_32.json 0m31.74s | 1145180 ko | Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo 0m31.69s | 161488 ko | fiat-json/src/p434_64.json 0m31.43s | 924252 ko | Rewriter/Passes/MulSplit.vo 0m31.36s | 232084 ko | fiat-java/src/FiatSecp256K1.java 0m31.21s | 211636 ko | fiat-go/32/secp256k1/secp256k1.go 0m31.15s | 220188 ko | fiat-zig/src/secp256k1_32.zig 0m31.08s | 530848 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeBound.vo 0m30.63s | 1088588 ko | Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo 0m30.59s | 221996 ko | fiat-java/src/FiatP256.java 0m30.52s | 213496 ko | fiat-c/src/secp256k1_32.c 0m30.20s | 232412 ko | fiat-zig/src/p256_32.zig 0m30.19s | 1280300 ko | ExtractionOCaml/saturated_solinas 0m30.02s | 783592 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/RegRename.vo 0m29.85s | 218580 ko | fiat-go/32/p256/p256.go 0m29.65s | 1223664 ko | ExtractionOCaml/base_conversion 0m29.54s | 223720 ko | fiat-rust/src/p256_32.rs 0m29.22s | 181748 ko | fiat-c/src/p256_32.c 0m29.19s | 1233324 ko | ExtractionOCaml/perf_word_by_word_montgomery 0m28.77s | 882476 ko | Rewriter/Rewriter/Examples.vo 0m28.42s | 214704 ko | fiat-rust/src/secp256k1_32.rs 0m28.26s | 961868 ko | PushButtonSynthesis/BYInversionReificationCache.vo 0m27.68s | 845540 ko | PushButtonSynthesis/UnsaturatedSolinas.vo 0m27.68s | 150160 ko | fiat-bedrock2/src/p434_64.c 0m27.49s | 918568 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo 0m26.81s | 1233224 ko | ExtractionOCaml/perf_unsaturated_solinas 0m26.63s | 1154076 ko | Assembly/Parse/TestAsm.vo 0m26.29s | 870600 ko | Rewriter/Rewriter/Examples/PrefixSums.vo 0m26.00s | 685080 ko | Rewriter/Language/Wf.vo 0m25.66s | 1734780 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml 0m25.65s | 499196 ko | Arithmetic/Saturated.vo 0m24.66s | 865512 ko | Bedrock/Field/Synthesis/Examples/LadderStep.vo 0m23.89s | 799260 ko | Bedrock/Field/Translation/Proofs/Expr.vo 0m23.80s | 153616 ko | fiat-go/64/p434/p434.go 0m23.34s | 871328 ko | Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo 0m23.11s | 1703768 ko | ExtractionOCaml/unsaturated_solinas.ml 0m23.08s | 136040 ko | fiat-rust/src/p434_64.rs 0m22.74s | 143448 ko | fiat-zig/src/p434_64.zig 0m21.78s | 839512 ko | PushButtonSynthesis/WordByWordMontgomery.vo 0m21.41s | 142148 ko | fiat-json/src/p224_32.json 0m21.23s | 1670340 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml 0m21.18s | 744060 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo 0m20.94s | 160716 ko | fiat-c/src/p434_64.c 0m20.86s | 1665312 ko | ExtractionOCaml/bedrock2_base_conversion.ml 0m19.68s | 1597384 ko | ExtractionOCaml/base_conversion.ml 0m19.06s | 1825436 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml 0m18.65s | 1585784 ko | ExtractionOCaml/saturated_solinas.ml 0m18.44s | 824264 ko | Bedrock/Field/Synthesis/Examples/X1305_32.vo 0m18.33s | 1921456 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs 0m18.30s | 583724 ko | Rewriter/Language/Inversion.vo 0m18.27s | 1780864 ko | ExtractionOCaml/perf_unsaturated_solinas.ml 0m17.78s | 1777620 ko | ExtractionHaskell/word_by_word_montgomery.hs 0m17.61s | 491748 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/RunInstruction.vo 0m17.50s | 98268 ko | fiat-json/src/p384_64.json 0m16.99s | 618720 ko | Util/ZUtil/ArithmeticShiftr.vo 0m16.81s | 1935596 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPreconditionProperties.vo 0m16.81s | 134432 ko | fiat-bedrock2/src/p224_32.c 0m16.80s | 834780 ko | Curves/Edwards/XYZT/Basic.vo 0m16.72s | 535444 ko | Arithmetic/WordByWordMontgomery.vo 0m16.68s | 788712 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo 0m16.54s | 731832 ko | Curves/Edwards/AffineProofs.vo 0m16.50s | 767704 ko | Language/IdentifiersGENERATED.vo 0m16.34s | 690024 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo 0m16.02s | 515852 ko | Arithmetic/BarrettReduction.vo 0m15.95s | 802608 ko | Bedrock/Field/Translation/Proofs/Cmd.vo 0m15.83s | 780420 ko | Bedrock/Field/Translation/Proofs/Func.vo 0m15.76s | 569888 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_SB.vo 0m15.49s | 722088 ko | Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo 0m15.44s | 911004 ko | StandaloneDebuggingExamples.vo 0m14.91s | 515740 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_66.vo 0m14.86s | 457860 ko | Algebra/Field.vo 0m14.76s | 426412 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/TestGoals.vo 0m14.58s | 569668 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA.vo 0m14.39s | 794592 ko | Bedrock/End2End/Poly1305/Field1305.vo 0m14.28s | 487088 ko | Arithmetic/Core.vo 0m14.21s | 655304 ko | Bedrock/Group/AdditionChains.vo 0m14.11s | 573684 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatImp.vo 0m14.04s | 596160 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI64.vo 0m13.99s | 590752 ko | Bedrock/Field/Common/Util.vo 0m13.88s | 147740 ko | fiat-rust/src/p224_32.rs 0m13.85s | 143368 ko | fiat-java/src/FiatP224.java 0m13.83s | 133844 ko | fiat-go/32/p224/p224.go 0m13.52s | 595588 ko | Util/ZRange/LandLorBounds.vo 0m13.45s | 598972 ko | Language/IdentifiersGENERATEDProofs.vo 0m13.44s | 482216 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.vo 0m13.37s | 649468 ko | Bedrock/Group/ScalarMult/LadderStep.vo 0m13.30s | 1477264 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs 0m13.13s | 1394912 ko | ExtractionHaskell/unsaturated_solinas.hs 0m13.09s | 543904 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA64.vo 0m12.95s | 138336 ko | fiat-c/src/p224_32.c 0m12.86s | 132156 ko | fiat-zig/src/p224_32.zig 0m12.80s | 105716 ko | fiat-bedrock2/src/p384_64.c 0m12.05s | 642144 ko | Rewriter/Demo.vo 0m11.93s | 1345788 ko | ExtractionHaskell/base_conversion.hs 0m11.82s | 1382968 ko | ExtractionHaskell/bedrock2_base_conversion.hs 0m11.80s | 857824 ko | PushButtonSynthesis/SmallExamples.vo 0m11.73s | 1398988 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs 0m11.54s | 608588 ko | Assembly/Symbolic.vo 0m11.47s | 1322896 ko | ExtractionHaskell/saturated_solinas.hs 0m11.41s | 654352 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/SpillingMapGoals.vo 0m11.01s | 607836 ko | Bedrock/Field/Translation/Proofs/Flatten.vo 0m11.00s | 547084 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM.vo 0m10.84s | 589060 ko | Stringification/IR.vo 0m10.80s | 90756 ko | fiat-go/64/p384/p384.go 0m10.80s | 91296 ko | fiat-rust/src/p384_64.rs 0m10.74s | 772064 ko | Bedrock/Field/Synthesis/New/Signature.vo 0m10.72s | 503160 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_UJ.vo 0m10.51s | 94444 ko | fiat-zig/src/p384_64.zig 0m10.47s | 505592 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/RegAlloc.vo 0m10.45s | 96512 ko | fiat-c/src/p384_64.c 0m10.25s | 476312 ko | Primitives/MxDHRepChange.vo 0m10.09s | 447704 ko | Algebra/Ring.vo 0m10.05s | 553316 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ToplevelLoop.vo 0m09.97s | 871992 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.vo 0m09.23s | 502084 ko | Arithmetic/BarrettReduction/Generalized.vo 0m08.88s | 504968 ko | Rewriter/Language/IdentifiersLibraryProofs.vo 0m08.56s | 785644 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.vo 0m08.50s | 46396 ko | fiat-zig/src/p448_solinas_32.zig 0m08.44s | 904344 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo 0m08.38s | 47604 ko | fiat-c/src/p448_solinas_32.c 0m08.37s | 609068 ko | Language/IdentifiersBasicGENERATED.vo 0m08.36s | 44408 ko | fiat-rust/src/p448_solinas_32.rs 0m08.21s | 750780 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo 0m08.18s | 688248 ko | PushButtonSynthesis/BaseConversion.vo 0m07.86s | 714304 ko | Assembly/Syntax.vo 0m07.82s | 595408 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo 0m07.66s | 461740 ko | Util/ZRange/CornersMonotoneBounds.vo 0m07.49s | 467488 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_S.vo 0m07.14s | 484012 ko | Util/ZUtil/Modulo.vo 0m06.95s | 711056 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.vo 0m06.92s | 688752 ko | PushButtonSynthesis/Primitives.vo 0m06.89s | 464132 ko | Arithmetic/FancyMontgomeryReduction.vo 0m06.86s | 440748 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Minimal.vo 0m06.57s | 477844 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ExprImp.vo 0m06.33s | 603176 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo 0m06.33s | 572768 ko | Rewriter/Passes/NoSelect.vo 0m06.32s | 673024 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.vo 0m06.30s | 457696 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_Fence.vo 0m06.23s | 508436 ko | Arithmetic/BYInv.vo 0m06.19s | 458064 ko | Util/MSets/Sum.vo 0m06.18s | 458504 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R_atomic.vo 0m06.18s | 459468 ko | Rewriter/Util/ListUtil.vo 0m06.17s | 667736 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.vo 0m06.15s | 456928 ko | Util/ListUtil.vo 0m05.80s | 833792 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo 0m05.79s | 486724 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/EmitsValid.vo 0m05.52s | 469972 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM64.vo 0m05.49s | 30756 ko | fiat-json/src/p521_64.json 0m05.47s | 529448 ko | Fancy/Prod.vo 0m05.46s | 638172 ko | BoundsPipeline.vo 0m05.38s | 579124 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Properties.vo 0m05.37s | 470800 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Loops.vo 0m05.35s | 455960 ko | Util/FsatzAutoLemmas.vo 0m05.14s | 733972 ko | Bedrock/Field/Synthesis/Examples/EncodeDecode.vo 0m05.14s | 490440 ko | COperationSpecifications.vo 0m04.95s | 429048 ko | Util/ZUtil/ZSimplify/Autogenerated.vo 0m04.82s | 433516 ko | Spec/Curve25519.vo 0m04.80s | 679552 ko | PushButtonSynthesis/BarrettReduction.vo 0m04.79s | 431892 ko | Arithmetic/MontgomeryReduction/Proofs.vo 0m04.76s | 503488 ko | Curves/Edwards/Pre.vo 0m04.64s | 547132 ko | Language/InversionExtra.vo 0m04.57s | 560284 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRFile.vo 0m04.51s | 460544 ko | Util/ZRange/BasicLemmas.vo 0m04.42s | 445096 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_57.vo 0m04.40s | 444852 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R.vo 0m04.34s | 475580 ko | Algebra/Field_test.vo 0m04.31s | 469540 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/LowerPipeline.vo 0m04.26s | 474012 ko | Rewriter/Language/IdentifiersBasicLibrary.vo 0m04.22s | 444684 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_FenceI.vo 0m04.22s | 461536 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Core.vo 0m04.21s | 44504 ko | fiat-json/src/secp256k1_64.json 0m04.19s | 32992 ko | fiat-go/64/p521/p521.go 0m04.13s | 561872 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.vo 0m04.05s | 444532 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I.vo 0m03.97s | 30624 ko | fiat-json/src/curve25519_32.json 0m03.93s | 459140 ko | UnsaturatedSolinasHeuristics.vo 0m03.86s | 450164 ko | Util/ZUtil/LandLorBounds.vo 0m03.85s | 486688 ko | Curves/Montgomery/Affine.vo 0m03.80s | 442640 ko | Arithmetic/BarrettReduction/HAC.vo 0m03.70s | 413900 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SlowGoals.vo 0m03.68s | 452280 ko | CastLemmas.vo 0m03.62s | 28892 ko | fiat-json/src/p448_solinas_64.json 0m03.58s | 456424 ko | Arithmetic/UniformWeight.vo 0m03.57s | 741664 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo 0m03.56s | 664376 ko | Bedrock/Group/ScalarMult/ScalarMult.vo 0m03.56s | 39428 ko | fiat-bedrock2/src/p521_64.c 0m03.48s | 721344 ko | Bedrock/Field/Synthesis/Examples/MulTwice.vo 0m03.40s | 442512 ko | Util/ZUtil/LandLorShiftBounds.vo 0m03.38s | 434648 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/ident_of_string.vo 0m03.37s | 447396 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO.vo 0m03.32s | 25468 ko | fiat-c/src/p521_64.c 0m03.31s | 396060 ko | Algebra/Group.vo 0m03.30s | 42728 ko | fiat-json/src/p224_64.json 0m03.29s | 588348 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo 0m03.28s | 43560 ko | fiat-bedrock2/src/secp256k1_64.c 0m03.27s | 435880 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_system.vo 0m03.23s | 25588 ko | fiat-zig/src/p521_64.zig 0m03.21s | 40336 ko | fiat-json/src/p256_64.json 0m03.20s | 464988 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/Pipeline.vo 0m03.18s | 566068 ko | PushButtonSynthesis/BaseConversionReificationCache.vo 0m03.10s | 445592 ko | Util/MSets/Iso.vo 0m03.05s | 705328 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo 0m03.04s | 615768 ko | Bedrock/Field/Interface/Compilation2.vo 0m03.02s | 688396 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo 0m03.00s | 539960 ko | Rewriter/Passes/AddAssocLeft.vo 0m02.99s | 468696 ko | MiscCompilerPassesProofs.vo 0m02.98s | 437604 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Properties.vo 0m02.97s | 522552 ko | Rewriter/Passes/Test.vo 0m02.95s | 686600 ko | PushButtonSynthesis/SaturatedSolinas.vo 0m02.94s | 413360 ko | Coqprime/PrimalityTest/PocklingtonCertificat.vo 0m02.92s | 26908 ko | fiat-rust/src/p521_64.rs 0m02.90s | 430816 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_U.vo 0m02.90s | 42596 ko | fiat-bedrock2/src/p448_solinas_64.c 0m02.76s | 429628 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/List.vo 0m02.76s | 32924 ko | fiat-go/64/p448solinas/p448solinas.go 0m02.74s | 38236 ko | fiat-bedrock2/src/curve25519_32.c 0m02.73s | 45140 ko | fiat-go/64/secp256k1/secp256k1.go 0m02.69s | 425268 ko | Util/Bool/Reflect.vo 0m02.66s | 439364 ko | Arithmetic/Primitives.vo 0m02.66s | 537352 ko | Rewriter/Passes/FlattenThunkedRects.vo 0m02.64s | 40940 ko | fiat-zig/src/secp256k1_64.zig 0m02.63s | 532420 ko | Bedrock/Field/Translation/Expr.vo 0m02.59s | 710536 ko | CLI.vo 0m02.59s | 41548 ko | fiat-bedrock2/src/p224_64.c 0m02.59s | 41288 ko | fiat-c/src/secp256k1_64.c 0m02.57s | 44588 ko | fiat-rust/src/secp256k1_64.rs 0m02.56s | 425932 ko | Rewriter/Util/Bool/Reflect.vo 0m02.51s | 429488 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/MulTrapHandler.vo 0m02.45s | 466108 ko | Util/ZUtil/Morphisms.vo 0m02.45s | 46312 ko | fiat-bedrock2/src/p256_64.c 0m02.40s | 457760 ko | Spec/MontgomeryCurve.vo 0m02.34s | 591252 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo 0m02.30s | 437656 ko | Util/ZUtil/Shift.vo 0m02.27s | 431604 ko | Arithmetic/BarrettReduction/RidiculousFish.vo 0m02.26s | 611596 ko | Bedrock/Field/Interface/Compilation.vo 0m02.21s | 430924 ko | Util/ZUtil/TwosComplement.vo 0m02.14s | 458288 ko | Arithmetic/Freeze.vo 0m02.12s | 455572 ko | Arithmetic/ModOps.vo 0m02.12s | 24696 ko | fiat-go/32/curve25519/curve25519.go 0m02.07s | 41664 ko | fiat-go/64/p224/p224.go 0m02.06s | 444228 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Arrays.vo 0m02.02s | 24556 ko | fiat-zig/src/p448_solinas_64.zig 0m02.01s | 431788 ko | Util/ZUtil/Testbit.vo 0m02.01s | 41592 ko | fiat-go/64/p256/p256.go 0m01.98s | 44632 ko | fiat-rust/src/p224_64.rs 0m01.96s | 416952 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/AbsintWordToZ.vo 0m01.96s | 41148 ko | fiat-c/src/p224_64.c 0m01.96s | 25532 ko | fiat-rust/src/p448_solinas_64.rs 0m01.95s | 432516 ko | Util/ZUtil/ModInv.vo 0m01.95s | 37392 ko | fiat-rust/src/p256_64.rs 0m01.94s | 25428 ko | fiat-c/src/p448_solinas_64.c 0m01.94s | 43480 ko | fiat-zig/src/p224_64.zig 0m01.93s | 43236 ko | fiat-zig/src/p256_64.zig 0m01.92s | 457468 ko | Arithmetic/BaseConversion.vo 0m01.91s | 388812 ko | Util/Wf2.vo 0m01.91s | 426104 ko | Util/ZUtil/Div.vo 0m01.88s | 24724 ko | fiat-java/src/FiatCurve25519.java 0m01.87s | 639212 ko | Bedrock/Field/Translation/Cmd.vo 0m01.85s | 589552 ko | CompilersTestCases.vo 0m01.85s | 535208 ko | Rewriter/Passes/StripLiteralCasts.vo 0m01.85s | 24192 ko | fiat-c/src/curve25519_32.c 0m01.85s | 42140 ko | fiat-c/src/p256_64.c 0m01.84s | 24720 ko | fiat-rust/src/curve25519_32.rs 0m01.84s | 25968 ko | fiat-zig/src/curve25519_32.zig 0m01.82s | 439484 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/WMMFree.vo 0m01.79s | 532024 ko | Stringification/Language.vo 0m01.77s | 534756 ko | Rewriter/Passes/UnfoldValueBarrier.vo 0m01.75s | 449028 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/GoFlatToRiscv.vo 0m01.75s | 451248 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/load_save_regs_correct.vo 0m01.71s | 433032 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/SeparationLogic.vo 0m01.71s | 626392 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo 0m01.65s | 431016 ko | Util/Tuple.vo 0m01.63s | 601296 ko | Bedrock/Field/Common/Names/MakeNames.vo 0m01.62s | 533440 ko | Rewriter/Passes/ToFancy.vo 0m01.61s | 462564 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/CompilerInvariant.vo 0m01.60s | 437876 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/ControlFlow/DownTo.vo 0m01.59s | 412348 ko | Util/ListUtil/Forall.vo 0m01.57s | 444348 ko | Arithmetic/ModularArithmeticTheorems.vo 0m01.55s | 434640 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Loops.vo 0m01.53s | 412184 ko | Rewriter/Util/ListUtil/Forall.vo 0m01.52s | 633704 ko | Bedrock/Field/Translation/Func.vo 0m01.51s | 431124 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Fib.vo 0m01.51s | 468896 ko | Assembly/Parse.vo 0m01.49s | 455624 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.vo 0m01.48s | 510816 ko | AbstractInterpretation/AbstractInterpretation.vo 0m01.46s | 437056 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/InlineTables.vo 0m01.46s | 455556 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised.vo 0m01.45s | 436624 ko | Spec/WeierstrassCurve.vo 0m01.43s | 513704 ko | AbstractInterpretation/ZRange.vo 0m01.43s | 454892 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.vo 0m01.41s | 437432 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Compiler.vo 0m01.41s | 718984 ko | Rewriter/PerfTesting/Core.vo 0m01.38s | 453320 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FitsStack.vo 0m01.38s | 417732 ko | Algebra/ScalarMult.vo 0m01.36s | 413540 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/MapEauto.vo 0m01.36s | 412932 ko | Coqprime/Z/Pmod.vo 0m01.36s | 527704 ko | Stringification/Go.vo 0m01.36s | 416444 ko | Util/ZUtil/Rshi.vo 0m01.33s | 431748 ko | Util/ZUtil/Pow2Mod.vo 0m01.31s | 411264 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness.vo 0m01.29s | 445296 ko | Util/ZRange/SplitRangeBounds.vo 0m01.28s | 435080 ko | Util/ZUtil/Bitwise.vo 0m01.26s | 428008 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRs.vo 0m01.25s | 470296 ko | Rewriter/Language/IdentifiersLibrary.vo 0m01.23s | 429640 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.vo 0m01.23s | 688724 ko | Bedrock/Field/Stringification/Stringification.vo 0m01.20s | 725512 ko | Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.vo 0m01.20s | 432232 ko | Util/ZUtil/TruncatingShiftl.vo 0m01.18s | 427164 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/InstructionSetOrder.vo 0m01.17s | 470156 ko | Arithmetic/PrimeFieldTheorems.vo 0m01.15s | 711988 ko | Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.vo 0m01.14s | 581008 ko | Assembly/Equivalence.vo 0m01.13s | 410772 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/PropSet.vo 0m01.12s | 694388 ko | Bedrock/Field/Synthesis/Generic/Operation.vo 0m01.12s | 696836 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo 0m01.11s | 447296 ko | Arithmetic/Partition.vo 0m01.11s | 441040 ko | Util/ZRange/SplitBounds.vo 0m01.10s | 432600 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimalMMIO.vo 0m01.09s | 441764 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/ControlFlow/CondSwap.vo 0m01.09s | 616864 ko | Bedrock/Specs/Field.vo 0m01.09s | 435732 ko | Util/ZUtil/Quot.vo 0m01.08s | 743344 ko | Bedrock/Standalone/StandaloneHaskellMain.vo 0m01.08s | 410624 ko | Coqprime/PrimalityTest/LucasLehmer.vo 0m01.08s | 730324 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo 0m01.07s | 602888 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo 0m01.07s | 414248 ko | Coqprime/PrimalityTest/EGroup.vo 0m01.06s | 413464 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Map/SeparationLogic.vo 0m01.06s | 419644 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/LittleEndianList.vo 0m01.06s | 693024 ko | Bedrock/Field/Synthesis/Specialized/Tactics.vo 0m01.06s | 451876 ko | Fancy/Spec.vo 0m01.06s | 417348 ko | Util/ZUtil/AddGetCarry.vo 0m01.05s | 593904 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo 0m01.04s | 706504 ko | StandaloneOCamlMain.vo 0m01.02s | 692868 ko | Bedrock/Field/Synthesis/Generic/Tactics.vo 0m01.02s | 359632 ko | Util/Wf1.vo 0m01.00s | 427488 ko | Util/ZUtil/OnesFrom.vo 0m00.99s | 707420 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo 0m00.98s | 518176 ko | Bedrock/Field/Translation/LoadStoreList.vo 0m00.97s | 442344 ko | Curves/Edwards/XYZT/Precomputed.vo 0m00.97s | 468504 ko | Rewriter/Rewriter/Rewriter.vo 0m00.96s | 525256 ko | Stringification/JSON.vo 0m00.93s | 743492 ko | Bedrock/Standalone/StandaloneOCamlMain.vo 0m00.93s | 528188 ko | Stringification/C.vo 0m00.93s | 415612 ko | Util/NatUtil.vo 0m00.92s | 706096 ko | StandaloneHaskellMain.vo 0m00.91s | 698984 ko | Bedrock/Field/Synthesis/Specialized/ReifiedOperation.vo 0m00.91s | 649040 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo 0m00.91s | 468460 ko | Rewriter/Rewriter/Reify.vo 0m00.90s | 644680 ko | Bedrock/Field/Translation/Parameters/Defaults.vo 0m00.90s | 649060 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo 0m00.90s | 611012 ko | Bedrock/Group/Point.vo 0m00.90s | 416572 ko | Rewriter/Util/NatUtil.vo 0m00.89s | 447724 ko | Rewriter/Language/Language.vo 0m00.89s | 23292 ko | fiat-json/src/curve25519_64.json 0m00.88s | 608956 ko | Bedrock/Field/Interface/Representation.vo 0m00.88s | 430016 ko | Util/ZUtil/Ones.vo 0m00.84s | 518292 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo 0m00.83s | 423032 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ptsto_bytes.vo 0m00.83s | 411684 ko | Coqprime/PrimalityTest/Pocklington.vo 0m00.83s | 409100 ko | Coqprime/Z/ZCAux.vo 0m00.83s | 524588 ko | Stringification/Rust.vo 0m00.83s | 524848 ko | Stringification/Zig.vo 0m00.82s | 503524 ko | Language/APINotations.vo 0m00.82s | 488088 ko | Rewriter/Rewriter/AllTactics.vo 0m00.81s | 587896 ko | Bedrock/Field/Common/Tactics.vo 0m00.81s | 517360 ko | Bedrock/Field/Common/Types.vo 0m00.81s | 428928 ko | Curves/Montgomery/AffineInstances.vo 0m00.81s | 418740 ko | Util/Strings/String_as_OT.vo 0m00.80s | 524444 ko | Stringification/Java.vo 0m00.77s | 411200 ko | Rewriter/Rewriter/Examples/PerfTesting/Sample.vo 0m00.75s | 416732 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/BigEndian.vo 0m00.75s | 513444 ko | Bedrock/Field/Translation/Flatten.vo 0m00.74s | 443860 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/ExprCompiler.vo 0m00.73s | 430596 ko | Arithmetic/BarrettReduction/Wikipedia.vo 0m00.72s | 552560 ko | Rewriter/All.vo 0m00.71s | 429784 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlattenExprSimulation.vo 0m00.71s | 445052 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/RiscvEventLoop.vo 0m00.71s | 418552 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/LittleEndian.vo 0m00.71s | 531456 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo 0m00.71s | 412352 ko | Coqprime/PrimalityTest/Root.vo 0m00.71s | 382688 ko | Util/Decidable.vo 0m00.68s | 439088 ko | Rewriter/Rules.vo 0m00.68s | 23348 ko | fiat-go/64/curve25519/curve25519.go 0m00.67s | 424188 ko | Util/CPSUtil.vo 0m00.67s | 436312 ko | Util/NumTheoryUtil.vo 0m00.67s | 326156 ko | Util/PartiallyReifiedProp.vo 0m00.66s | 422864 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Array.vo 0m00.66s | 415544 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/BitOps.vo 0m00.66s | 513340 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo 0m00.66s | 413372 ko | Coqprime/PrimalityTest/Cyclic.vo 0m00.65s | 536300 ko | Bedrock/Field/Stringification/FlattenVarData.vo 0m00.65s | 382768 ko | Rewriter/Util/Decidable.vo 0m00.65s | 26220 ko | fiat-bedrock2/src/curve25519_64.c 0m00.64s | 423452 ko | Algebra/IntegralDomain.vo 0m00.64s | 517416 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo 0m00.63s | 441400 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/SepLocals.vo 0m00.63s | 411116 ko | Coqprime/PrimalityTest/PGroup.vo 0m00.63s | 496904 ko | PushButtonSynthesis/ReificationCache.vo 0m00.62s | 496228 ko | Language/API.vo 0m00.62s | 420780 ko | Util/Strings/ParseArithmetic.vo 0m00.61s | 411236 ko | Coqprime/Z/ZSum.vo 0m00.60s | 435648 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/ArrayCasts.vo 0m00.60s | 447620 ko | Assembly/Equality.vo 0m00.60s | 451664 ko | Bedrock/Specs/Group.vo 0m00.60s | 501232 ko | Language/WfExtra.vo 0m00.60s | 503192 ko | Rewriter/AllTacticsExtra.vo 0m00.60s | 386956 ko | Util/Structures/Orders/Sum.vo 0m00.59s | 427232 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/SMTVerif.vo 0m00.59s | 441860 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/ExprReflection.vo 0m00.59s | 436848 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/NoExprReflection.vo 0m00.59s | 505780 ko | AbstractInterpretation/WfExtra.vo 0m00.59s | 459096 ko | MiscCompilerPasses.vo 0m00.59s | 474896 ko | Rewriter/Rewriter/ProofsCommonTactics.vo 0m00.58s | 501316 ko | Language/UnderLetsProofsExtra.vo 0m00.58s | 500936 ko | MiscCompilerPassesProofsExtra.vo 0m00.58s | 459524 ko | Rewriter/Language/IdentifiersGenerate.vo 0m00.58s | 480220 ko | Rewriter/Util/plugins/RewriterBuild.vo 0m00.57s | 412616 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedList.vo 0m00.57s | 421312 ko | Algebra/SubsetoidRing.vo 0m00.57s | 479768 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports.vo 0m00.57s | 432392 ko | Util/Arg.vo 0m00.57s | 440436 ko | Util/ZRange/OperationsBounds.vo 0m00.55s | 415000 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ZLemmas.vo 0m00.55s | 414096 ko | Coqprime/PrimalityTest/Zp.vo 0m00.54s | 420648 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/Registers.vo 0m00.54s | 466340 ko | ArithmeticCPS/WordByWordMontgomery.vo 0m00.54s | 452216 ko | Bedrock/Group/Loops.vo 0m00.53s | 417632 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/DivisibleBy4.vo 0m00.53s | 460512 ko | Rewriter/Language/IdentifiersGenerateProofs.vo 0m00.53s | 409112 ko | Util/OptionList.vo 0m00.53s | 359484 ko | Util/Wf.vo 0m00.53s | 410384 ko | Util/ZUtil/Modulo/PullPush.vo 0m00.52s | 411608 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/ListSet.vo 0m00.52s | 460888 ko | ArithmeticCPS/Freeze.vo 0m00.52s | 481620 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings.vo 0m00.52s | 408160 ko | Util/Loops.vo 0m00.52s | 440720 ko | Util/QUtil.vo 0m00.51s | 423988 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/FE310CSemantics.vo 0m00.51s | 413452 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/bitblast.vo 0m00.51s | 480112 ko | Rewriter/Util/plugins/RewriterBuildRegistry.vo 0m00.50s | 421300 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeProver.vo 0m00.49s | 453416 ko | ArithmeticCPS/Saturated.vo 0m00.49s | 21016 ko | fiat-rust/src/curve25519_64.rs 0m00.48s | 435260 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/SepReflection.vo 0m00.48s | 457204 ko | ArithmeticCPS/ModOps.vo 0m00.48s | 415796 ko | Util/Strings/ParseArithmeticToTaps.vo 0m00.48s | 430440 ko | Util/ZUtil/Stabilization.vo 0m00.48s | 20996 ko | fiat-c/src/curve25519_64.c 0m00.48s | 21284 ko | fiat-zig/src/curve25519_64.zig 0m00.47s | 422972 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Memory.vo 0m00.47s | 406528 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/PushPullMod.vo 0m00.47s | 420972 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRGetSet.vo 0m00.46s | 424564 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/StringNameGen.vo 0m00.46s | 421224 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/OfListWord.vo 0m00.46s | 350576 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Monads.vo 0m00.46s | 436436 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Alloc.vo 0m00.46s | 470772 ko | Arithmetic/FLia.vo 0m00.46s | 431236 ko | Util/Strings/NamingConventions.vo 0m00.45s | 460808 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ExprImpEventLoopSpec.vo 0m00.45s | 417632 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/ZifyLittleEndian.vo 0m00.45s | 422904 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Example64Literal.vo 0m00.45s | 425244 ko | Util/Decidable/Decidable2Bool.vo 0m00.45s | 454756 ko | Util/MSetPositive/Show.vo 0m00.44s | 434392 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatImpSepLog.vo 0m00.44s | 437316 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvDef.vo 0m00.44s | 442688 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ForeverSafe.vo 0m00.44s | 426852 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/UniqueSepLog.vo 0m00.44s | 462696 ko | ArithmeticCPS/BaseConversion.vo 0m00.44s | 434608 ko | Rewriter/Language/IdentifiersBasicGenerate.vo 0m00.44s | 384884 ko | Util/Sum.vo 0m00.44s | 429196 ko | Util/ZUtil/CC.vo 0m00.43s | 414524 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Naive.vo 0m00.43s | 437968 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Conditionals.vo 0m00.43s | 464708 ko | Assembly/WithBedrock/Semantics.vo 0m00.43s | 430328 ko | Util/Strings/Show.vo 0m00.42s | 407952 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/ZLib.vo 0m00.42s | 432500 ko | Arithmetic/ModularArithmeticPre.vo 0m00.41s | 427300 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/MetricPrimitives.vo 0m00.41s | 422672 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Monads.vo 0m00.41s | 412040 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/ToCString.vo 0m00.41s | 450632 ko | ArithmeticCPS/Core.vo 0m00.40s | 430656 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO_Post.vo 0m00.40s | 426208 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Primitives.vo 0m00.40s | 386384 ko | Coqprime/List/UList.vo 0m00.40s | 427816 ko | Util/ZBounded.vo 0m00.39s | 431956 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatImpUniqueSepLog.vo 0m00.39s | 365400 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimal.vo 0m00.39s | 423000 ko | Util/HList.vo 0m00.39s | 432100 ko | Util/ZUtil/Lxor.vo 0m00.38s | 412476 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ToCString.vo 0m00.38s | 416200 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/util/Result.vo 0m00.38s | 351272 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/FE310ExtSpec.vo 0m00.38s | 361140 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Tactics.vo 0m00.38s | 384756 ko | Rewriter/Util/Sum.vo 0m00.38s | 424836 ko | Util/Level.vo 0m00.38s | 394868 ko | Util/Strings/String_as_OT_old.vo 0m00.38s | 411976 ko | Util/ZUtil/CPS.vo 0m00.38s | 415116 ko | Util/ZUtil/Ltz.vo 0m00.38s | 433360 ko | Util/ZUtil/SignBit.vo 0m00.37s | 410320 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Decode.vo 0m00.37s | 422360 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI.vo 0m00.37s | 385884 ko | Coqprime/List/Permutation.vo 0m00.37s | 404328 ko | Language/IdentifierParameters.vo 0m00.37s | 389456 ko | Language/PreExtra.vo 0m00.37s | 424268 ko | Util/ZUtil/Log2.vo 0m00.37s | 24268 ko | fiat-bedrock2/src/poly1305_32.c 0m00.37s | 21344 ko | fiat-json/src/poly1305_32.json 0m00.36s | 373820 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/MemoryLayout.vo 0m00.36s | 356092 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalLogging.vo 0m00.36s | 426228 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Sane.vo 0m00.36s | 409500 ko | Coqprime/Z/ZCmisc.vo 0m00.36s | 425152 ko | Curves/Weierstrass/Affine.vo 0m00.36s | 415208 ko | Rewriter/Util/Strings/ParseArithmetic.vo 0m00.36s | 427372 ko | Util/ZRange.vo 0m00.35s | 415944 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/OfFunc.vo 0m00.35s | 414980 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/prove_Zeq_bitwise.vo 0m00.35s | 400568 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRsDet.vo 0m00.35s | 410048 ko | Coqprime/PrimalityTest/Euler.vo 0m00.35s | 398656 ko | Rewriter/TestRules.vo 0m00.35s | 408944 ko | Util/Strings/String.vo 0m00.35s | 393280 ko | Util/ZUtil/Divide.vo 0m00.34s | 370164 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlattenExprDef.vo 0m00.34s | 421088 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Memory.vo 0m00.34s | 365336 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Api.vo 0m00.34s | 375280 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Notations.vo 0m00.34s | 363872 ko | Util/ZUtil.vo 0m00.34s | 428500 ko | Util/ZUtil/Land.vo 0m00.33s | 413004 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/MapKeys.vo 0m00.33s | 350844 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/AtomicMinimal.vo 0m00.33s | 360380 ko | Rewriter/TestRulesProofs.vo 0m00.33s | 376152 ko | Rewriter/Util/MSetPositive/Facts.vo 0m00.33s | 377380 ko | Util/Strings/Sorting.vo 0m00.33s | 350684 ko | Util/ZUtil/Tactics/SolveRange.vo 0m00.32s | 339900 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ProgramLogic.vo 0m00.32s | 421384 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/footpr.vo 0m00.32s | 375216 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Invariants.vo 0m00.32s | 424116 ko | Spec/CompleteEdwardsCurve.vo 0m00.32s | 331328 ko | Spec/ModularArithmetic.vo 0m00.31s | 377228 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA64.vo 0m00.31s | 385048 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Encode.vo 0m00.31s | 354228 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/WordNotations.vo 0m00.31s | 410044 ko | Coqprime/PrimalityTest/IGroup.vo 0m00.31s | 369776 ko | Curves/Montgomery/XZ.vo 0m00.31s | 352892 ko | Util/ZUtil/Lor.vo 0m00.30s | 336360 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatImpConstraints.vo 0m00.30s | 341928 ko | Rewriter/Util/MSetPositive/Equality.vo 0m00.30s | 388872 ko | Util/ZUtil/EquivModulo.vo 0m00.30s | 20168 ko | fiat-go/32/poly1305/poly1305.go 0m00.29s | 342568 ko | Util/MSetPositive/Equality.vo 0m00.29s | 376488 ko | Util/MSetPositive/Facts.vo 0m00.29s | 336460 ko | Util/ZUtil/Le.vo 0m00.29s | 348172 ko | Util/ZUtil/Tactics/SolveTestbit.vo 0m00.29s | 342860 ko | Util/ZUtil/Tactics/Ztestbit.vo 0m00.28s | 350316 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPrecondition.vo 0m00.28s | 378888 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA.vo 0m00.28s | 386536 ko | Algebra/Monoid.vo 0m00.28s | 315852 ko | Algebra/Nsatz.vo 0m00.28s | 326704 ko | Arithmetic/MontgomeryReduction/Definition.vo 0m00.28s | 408660 ko | Coqprime/PrimalityTest/Lagrange.vo 0m00.28s | 374404 ko | Util/Listable.vo 0m00.27s | 332180 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedListWord.vo 0m00.27s | 333668 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MaterializeRiscvProgram.vo 0m00.27s | 336616 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/RiscvMachine.vo 0m00.27s | 298828 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Run.vo 0m00.27s | 374140 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteCSR.vo 0m00.27s | 386312 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/StringRecords.vo 0m00.27s | 298688 ko | Bedrock/Field/Common/Names/VarnameGenerator.vo 0m00.27s | 386468 ko | Coqprime/List/Iterator.vo 0m00.27s | 385248 ko | Coqprime/List/ListAux.vo 0m00.27s | 409616 ko | Coqprime/List/ZProgression.vo 0m00.27s | 392268 ko | Rewriter/Language/UnderLets.vo 0m00.27s | 376032 ko | Rewriter/Util/Strings/String.vo 0m00.27s | 342424 ko | Util/NUtil/WithoutReferenceToZ.vo 0m00.27s | 315028 ko | Util/Option.vo 0m00.26s | 390980 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/NotationsCustomEntry.vo 0m00.26s | 295340 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringStackallocLoopTest.vo 0m00.26s | 298404 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/util/Common.vo 0m00.26s | 330884 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/DebugWordEq.vo 0m00.26s | 314992 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI64.vo 0m00.26s | 357564 ko | Util/AdditionChainExponentiation.vo 0m00.26s | 299264 ko | Util/ZUtil/Nat2Z.vo 0m00.25s | 327420 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/BasicC32Semantics.vo 0m00.25s | 343508 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ZnWords.vo 0m00.25s | 306932 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/regs_initialized.vo 0m00.25s | 382148 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/SimplWordExpr.vo 0m00.25s | 311180 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/SoftmulInsts.vo 0m00.25s | 276756 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Execute.vo 0m00.25s | 324524 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Machine.vo 0m00.25s | 315000 ko | Rewriter/Util/Option.vo 0m00.25s | 316288 ko | Util/IdfunWithAlt.vo 0m00.25s | 337624 ko | Util/ListUtil/Permutation.vo 0m00.25s | 346692 ko | Util/ListUtil/SetoidList.vo 0m00.25s | 319664 ko | Util/MSets/Show.vo 0m00.25s | 292932 ko | Util/SideConditions/ModInvPackage.vo 0m00.25s | 361060 ko | Util/ZRange/Operations.vo 0m00.25s | 270120 ko | Util/ZUtil/Hints/PullPush.vo 0m00.25s | 363016 ko | Util/ZUtil/Pow.vo 0m00.25s | 310336 ko | Util/ZUtil/ZSimplify/Simple.vo 0m00.25s | 19780 ko | fiat-java/src/FiatPoly1305.java 0m00.24s | 392304 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Semantics.vo 0m00.24s | 321360 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ZNameGen.vo 0m00.24s | 331084 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/mod4_0.vo 0m00.24s | 340344 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/LogInstructionTrace.vo 0m00.24s | 288904 ko | Util/ZUtil/Definitions.vo 0m00.24s | 292524 ko | Util/ZUtil/N2Z.vo 0m00.24s | 335540 ko | Util/ZUtil/Peano.vo 0m00.24s | 273652 ko | Util/ZUtil/Sorting.vo 0m00.24s | 316600 ko | Util/ZUtil/Tactics.vo 0m00.24s | 319432 ko | Util/ZUtil/Tactics/SimplifyFractionsLe.vo 0m00.24s | 19820 ko | fiat-zig/src/poly1305_32.zig 0m00.23s | 329044 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/BasicC64Semantics.vo 0m00.23s | 285080 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringExprTypecheckingTest.vo 0m00.23s | 285940 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/RiscvWordProperties.vo 0m00.23s | 261884 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Bitwidth32.vo 0m00.23s | 250148 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricLogging.vo 0m00.23s | 280236 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRSpec.vo 0m00.23s | 294480 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Utility.vo 0m00.23s | 309336 ko | Rewriter/Util/FMapPositive/Equality.vo 0m00.23s | 317272 ko | Util/ZRange/Show.vo 0m00.23s | 280976 ko | Util/ZUtil/Sgn.vo 0m00.23s | 263956 ko | Util/ZUtil/Tactics/DivModToQuotRem.vo 0m00.23s | 314952 ko | Util/ZUtil/Tactics/RewriteModSmall.vo 0m00.23s | 316832 ko | Util/ZUtil/Tactics/ZeroBounds.vo 0m00.23s | 20412 ko | fiat-json/src/poly1305_64.json 0m00.23s | 19852 ko | fiat-rust/src/poly1305_32.rs 0m00.22s | 301644 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/div10.vo 0m00.22s | 262016 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Bitwidth64.vo 0m00.22s | 261488 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/HexNotation.vo 0m00.22s | 288380 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/InstructionNotations.vo 0m00.22s | 308888 ko | Rewriter/Language/PreLemmas.vo 0m00.22s | 346408 ko | Rewriter/Util/ListUtil/SetoidList.vo 0m00.22s | 281584 ko | TAPSort.vo 0m00.22s | 283452 ko | Util/Factorize.vo 0m00.22s | 338896 ko | Util/ZUtil/Combine.vo 0m00.22s | 276504 ko | Util/ZUtil/DistrIf.vo 0m00.22s | 264724 ko | Util/ZUtil/Div/Bootstrap.vo 0m00.22s | 264852 ko | Util/ZUtil/Hints/Core.vo 0m00.22s | 263224 ko | Util/ZUtil/Mul.vo 0m00.22s | 287160 ko | Util/ZUtil/Odd.vo 0m00.22s | 261180 ko | Util/ZUtil/Tactics/CompareToSgn.vo 0m00.22s | 261492 ko | Util/ZUtil/Tactics/DivideExistsMul.vo 0m00.22s | 282968 ko | Util/ZUtil/Tactics/LinearSubstitute.vo 0m00.22s | 267692 ko | Util/ZUtil/Tactics/PullPush/Modulo.vo 0m00.22s | 279788 ko | Util/ZUtil/Zselect.vo 0m00.22s | 19844 ko | fiat-c/src/poly1305_32.c 0m00.21s | 311156 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/SepLogAddrArith.vo 0m00.21s | 314820 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Byte.vo 0m00.21s | 273280 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Solver.vo 0m00.21s | 288612 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Z_keyed_SortedListMap.vo 0m00.21s | 307804 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteM.vo 0m00.21s | 280784 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/PseudoInstructions.vo 0m00.21s | 263980 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/VirtualMemory.vo 0m00.21s | 295624 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/DefaultMemImpl32.vo 0m00.21s | 296172 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/DefaultMemImpl64.vo 0m00.21s | 272668 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/RegisterNames.vo 0m00.21s | 250508 ko | Algebra/Hierarchy.vo 0m00.21s | 343752 ko | Coqprime/PrimalityTest/FGroup.vo 0m00.21s | 265524 ko | PushButtonSynthesis/InvertHighLow.vo 0m00.21s | 318968 ko | Util/ErrorT/Show.vo 0m00.21s | 285524 ko | Util/Strings/Parse/Common.vo 0m00.21s | 268076 ko | Util/Strings/StringMap.vo 0m00.21s | 258916 ko | Util/Structures/Equalities/Sum.vo 0m00.21s | 265872 ko | Util/ZUtil/Lnot.vo 0m00.21s | 282452 ko | Util/ZUtil/Pow2.vo 0m00.20s | 234692 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/MetricsToRiscv.vo 0m00.20s | 288200 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/AtomicRiscvMachine.vo 0m00.20s | 301752 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncode.vo 0m00.20s | 297856 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSR.vo 0m00.20s | 300548 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteM64.vo 0m00.20s | 263308 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Words32Naive.vo 0m00.20s | 227176 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/IdentParsing.vo 0m00.20s | 270888 ko | Algebra/NsatzTactic.vo 0m00.20s | 309668 ko | Util/FMapPositive/Equality.vo 0m00.20s | 264164 ko | Util/NUtil/Sorting.vo 0m00.20s | 280248 ko | Util/NUtil/Testbit.vo 0m00.20s | 266420 ko | Util/SideConditions/RingPackage.vo 0m00.20s | 270448 ko | Util/ZUtil/AddModulo.vo 0m00.20s | 265988 ko | Util/ZUtil/Hints.vo 0m00.20s | 262848 ko | Util/ZUtil/Hints/Ztestbit.vo 0m00.20s | 277248 ko | Util/ZUtil/Modulo/Bootstrap.vo 0m00.20s | 267164 ko | Util/ZUtil/Opp.vo 0m00.20s | 20712 ko | fiat-go/64/poly1305/poly1305.go 0m00.19s | 249784 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Map/Separation.vo 0m00.19s | 264292 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/groundcbv.vo 0m00.19s | 284996 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Funext.vo 0m00.19s | 246500 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedListString.vo 0m00.19s | 240084 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd_list_hints.vo 0m00.19s | 248212 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd_map_hints.vo 0m00.19s | 271152 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRField.vo 0m00.19s | 271644 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/nat_div_mod_to_quot_rem.vo 0m00.19s | 216732 ko | Spec/MxDH.vo 0m00.19s | 264536 ko | Util/ZUtil/Hints/ZArith.vo 0m00.19s | 270864 ko | Util/ZUtil/ModExp.vo 0m00.19s | 299300 ko | Util/ZUtil/MulSplit.vo 0m00.19s | 263784 ko | Util/ZUtil/Tactics/PeelLe.vo 0m00.19s | 266424 ko | Util/ZUtil/Tactics/ReplaceNegWithPos.vo 0m00.19s | 262112 ko | Util/ZUtil/Tactics/SplitMinMax.vo 0m00.18s | 250816 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/MetricLogging.vo 0m00.18s | 239100 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Structs.vo 0m00.18s | 239872 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/NameGen.vo 0m00.18s | 254924 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Empty_set_keyed_map.vo 0m00.18s | 290516 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Interface.vo 0m00.18s | 263212 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/Simp.vo 0m00.18s | 314252 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Interface.vo 0m00.18s | 288908 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricRiscvMachine.vo 0m00.18s | 302628 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MkMachineWidth.vo 0m00.18s | 261320 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Tactics.vo 0m00.18s | 269780 ko | Rewriter/Util/Prod.vo 0m00.18s | 255372 ko | Rewriter/Util/Strings/Decimal.vo 0m00.18s | 306000 ko | Util/ListUtil/FoldBool.vo 0m00.18s | 269244 ko | Util/SideConditions/Autosolve.vo 0m00.18s | 283428 ko | Util/ZUtil/Ge.vo 0m00.18s | 317052 ko | Util/ZUtil/Tactics/LtbToLt.vo 0m00.18s | 266432 ko | Util/ZUtil/ZSimplify/Core.vo 0m00.18s | 21812 ko | fiat-bedrock2/src/poly1305_64.c 0m00.17s | 275196 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedListString_test.vo 0m00.17s | 243872 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/SafeSimpl.vo 0m00.17s | 265488 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/Tactics.vo 0m00.17s | 246976 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd.vo 0m00.17s | 261884 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/Lia.vo 0m00.17s | 258852 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/InstructionCoercions.vo 0m00.17s | 263428 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Words64Naive.vo 0m00.17s | 271692 ko | Rewriter/Util/Strings/Parse/Common.vo 0m00.17s | 190220 ko | Util/ParseTaps.vo 0m00.17s | 312340 ko | Util/PointedProp.vo 0m00.17s | 214416 ko | Util/Strings/Ascii.vo 0m00.17s | 308608 ko | Util/ZUtil/Z2Nat.vo 0m00.16s | 246540 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Decidable.vo 0m00.16s | 201824 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Macros/ident_to_string.vo 0m00.16s | 261892 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Bitwidth.vo 0m00.16s | 184884 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/div_mod_to_equations.vo 0m00.16s | 255456 ko | Util/Strings/Decimal.vo 0m00.16s | 270088 ko | Util/ZUtil/LnotModulo.vo 0m00.16s | 235484 ko | Util/ZUtil/Tactics/PullPush.vo 0m00.15s | 221392 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Bytedump.vo 0m00.15s | 217112 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Syntax.vo 0m00.15s | 259584 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/TracePredicate.vo 0m00.15s | 331288 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/String.vo 0m00.15s | 190888 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd_arith_hints.vo 0m00.15s | 216792 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MonadTests.vo 0m00.15s | 254992 ko | Coqprime/N/NatAux.vo 0m00.15s | 179688 ko | Util/ListUtil/PermutationCompat.vo 0m00.15s | 193156 ko | Util/SideConditions/ReductionPackages.vo 0m00.15s | 231264 ko | Util/ZUtil/Tactics/PrimeBound.vo 0m00.14s | 217888 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd_core.vo 0m00.14s | 211292 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/FreeMonad.vo 0m00.14s | 212608 ko | Rewriter/Util/Strings/Ascii.vo 0m00.13s | 193760 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Variables.vo 0m00.13s | 196668 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/destr.vo 0m00.13s | 261792 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/rewr.vo 0m00.13s | 189256 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MMIOTrace.vo 0m00.13s | 198760 ko | Rewriter/Util/PrimitiveProd.vo 0m00.13s | 210800 ko | Util/ListUtil/NthExt.vo 0m00.13s | 274948 ko | Util/Prod.vo 0m00.13s | 230388 ko | Util/Sigma.vo 0m00.13s | 256708 ko | Util/Telescope/Equality.vo 0m00.13s | 19216 ko | fiat-c/src/poly1305_64.c 0m00.13s | 19232 ko | fiat-rust/src/poly1305_64.rs 0m00.12s | 150052 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/HList.vo 0m00.12s | 189200 ko | /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Gensym.vo 0m00.12s | 270248 ko | Rewriter/Util/OptionList.vo 0m00.12s | 154460 ko | Util/Bool.vo 0m00.12s | 236580 ko | Util/Decidable/Bool2Prop.vo 0m00.12s | 243548 ko | Util/LetInMonad.vo 0m00.12s | 192112 ko | Util/Telescope/Instances.vo 0m00.12s | 240692 ko | Util/ZUtil/ZSimplify.vo 0m00.12s | 18852 ko | fiat-zig/src/poly1305_64.zig 0m00.11s | 177276 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/div_to_equations.vo 0m00.11s | 178288 ko | Util/ListUtil/IndexOf.vo 0m00.11s | 204224 ko | Util/PrimitiveProd.vo 0m00.10s | 133704 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/ExtensibleRecords.vo 0m00.10s | 167684 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MonadT.vo 0m00.10s | 113372 ko | Rewriter/Language/Pre.vo 0m00.10s | 224804 ko | Rewriter/Util/Sigma.vo 0m00.10s | 143240 ko | Util/Equality.vo 0m00.10s | 112328 ko | Util/ListUtil/FoldMap.vo 0m00.10s | 175816 ko | Util/ListUtil/ForallIn.vo 0m00.10s | 179720 ko | Util/ZUtil/Notations.vo 0m00.09s | 122648 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Lift1Prop.vo 0m00.09s | 121696 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/Simulation.vo 0m00.09s | 145092 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/JMonad.vo 0m00.09s | 162700 ko | Rewriter/Util/PrimitiveSigma.vo 0m00.09s | 188696 ko | Util/Relations.vo 0m00.08s | 118688 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/Records.vo 0m00.08s | 112792 ko | Rewriter/Language/PreCommon.vo 0m00.08s | 133752 ko | Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.vo 0m00.08s | 137976 ko | Rewriter/Util/Equality.vo 0m00.08s | 84628 ko | Rewriter/Util/Logic/ProdForall.vo 0m00.08s | 108000 ko | Util/DynList.vo 0m00.08s | 113532 ko | Util/PrimitiveHList.vo 0m00.08s | 168520 ko | Util/PrimitiveSigma.vo 0m00.08s | 120420 ko | Util/Structures/Equalities/Iso.vo 0m00.08s | 108612 ko | Util/Structures/Orders/Iso.vo 0m00.08s | 108940 ko | Util/Tactics/AllInstances.vo 0m00.08s | 108368 ko | Util/Tactics/AllSuccesses.vo 0m00.08s | 114688 ko | Util/TagList.vo 0m00.07s | 85808 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Hexdump.vo 0m00.07s | 104140 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ReversedListNotations.vo 0m00.07s | 78700 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/ParamRecords.vo 0m00.07s | 86568 ko | Rewriter/Util/IffT.vo 0m00.07s | 113320 ko | Rewriter/Util/PrimitiveHList.vo 0m00.07s | 71976 ko | Util/ChangeInAll.vo 0m00.07s | 102012 ko | Util/HProp.vo 0m00.07s | 105752 ko | Util/Logic/ExistsEqAnd.vo 0m00.07s | 94064 ko | Util/Structures/Orders.vo 0m00.07s | 114988 ko | Util/Tactics.vo 0m00.07s | 103420 ko | Util/Telescope/Core.vo 0m00.07s | 81144 ko | tests/coqpl_2021.vo 0m00.06s | 68408 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Markers.vo 0m00.06s | 82760 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/eplace.vo 0m00.06s | 112144 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MonadNotations.vo 0m00.06s | 82816 ko | Rewriter/Util/CPSNotations.vo 0m00.06s | 96920 ko | Rewriter/Util/HProp.vo 0m00.06s | 104372 ko | Rewriter/Util/LetIn.vo 0m00.06s | 114640 ko | Rewriter/Util/Sigma/Related.vo 0m00.06s | 94924 ko | Rewriter/Util/Tactics/RewriteHyp.vo 0m00.06s | 67128 ko | Rewriter/Util/Tactics/WarnIfGoalsRemain.vo 0m00.06s | 93592 ko | Util/AutoRewrite.vo 0m00.06s | 81316 ko | Util/Bool/Equality.vo 0m00.06s | 81608 ko | Util/Bool/LeCompat.vo 0m00.06s | 104752 ko | Util/Compose.vo 0m00.06s | 134492 ko | Util/ErrorT.vo 0m00.06s | 91760 ko | Util/IffT.vo 0m00.06s | 91848 ko | Util/Logic.vo 0m00.06s | 79996 ko | Util/Logic/ImplAnd.vo 0m00.06s | 93460 ko | Util/Pointed.vo 0m00.06s | 76264 ko | Util/Tactics/AppendUnderscores.vo 0m00.06s | 72348 ko | Util/Tactics/ChangeInAll.vo 0m00.06s | 80876 ko | Util/Tactics/DebugPrint.vo 0m00.06s | 88280 ko | Util/Tactics/DestructHead.vo 0m00.06s | 72104 ko | Util/Tactics/SubstEvars.vo 0m00.06s | 73132 ko | Util/Tactics/TransparentAssert.vo 0m00.06s | 112188 ko | tests/ListNotationTests.vo 0m00.06s | 116764 ko | tests/RecordSetTests.vo 0m00.05s | 85424 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/GenericForeverSafe.vo 0m00.05s | 113164 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/Option.vo 0m00.05s | 76316 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Ltac2Lib/Log.vo 0m00.05s | 76948 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Macros/symmetry.vo 0m00.05s | 66720 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/rdelta.vo 0m00.05s | 132344 ko | Rewriter/Util/Bool.vo 0m00.05s | 99520 ko | Rewriter/Util/Logic/ExistsEqAnd.vo 0m00.05s | 88200 ko | Rewriter/Util/Pointed.vo 0m00.05s | 75584 ko | Rewriter/Util/Tactics/DebugPrint.vo 0m00.05s | 82320 ko | Rewriter/Util/Tactics/DestructHead.vo 0m00.05s | 75560 ko | Rewriter/Util/Tactics/DoWithHyp.vo 0m00.05s | 66996 ko | Rewriter/Util/Tactics/EvarNormalize.vo 0m00.05s | 70980 ko | Rewriter/Util/Tactics/Head.vo 0m00.05s | 71096 ko | Rewriter/Util/Tactics/HeadUnderBinders.vo 0m00.05s | 75460 ko | Rewriter/Util/Tactics/SpecializeAllWays.vo 0m00.05s | 80284 ko | Util/PER.vo 0m00.05s | 72348 ko | Util/Tactics/ClearAll.vo 0m00.05s | 72740 ko | Util/Tactics/ConvoyDestruct.vo 0m00.05s | 72632 ko | Util/Tactics/Forward.vo 0m00.05s | 84668 ko | Util/Tactics/MoveLetIn.vo 0m00.05s | 71976 ko | Util/Tactics/OnSubterms.vo 0m00.05s | 100708 ko | Util/Tactics/RewriteHyp.vo 0m00.05s | 72716 ko | Util/Tactics/UnfoldArg.vo 0m00.05s | 74560 ko | tests/SimpleRecordUpdate.vo 0m00.04s | 68488 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/on_hyp_containing.vo 0m00.04s | 67820 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/util/LogGoal.vo 0m00.04s | 80556 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/util/Misc.vo 0m00.04s | 76196 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Ltac2Lib/Msg.vo 0m00.04s | 66392 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Macros/unique.vo 0m00.04s | 66620 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/autoforward.vo 0m00.04s | 70956 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/forward.vo 0m00.04s | 67744 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/simpl_rewrite.vo 0m00.04s | 66724 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/dlet.vo 0m00.04s | 72940 ko | RecordSet.vo 0m00.04s | 66240 ko | RecordUpdate.vo 0m00.04s | 70200 ko | Rewriter/Util/InductiveHList.vo 0m00.04s | 67916 ko | Rewriter/Util/Isomorphism.vo 0m00.04s | 71008 ko | Rewriter/Util/Tactics/AssertSucceedsPreserveError.vo 0m00.04s | 68840 ko | Rewriter/Util/Tactics/CPSId.vo 0m00.04s | 72204 ko | Rewriter/Util/Tactics/DestructHyps.vo 0m00.04s | 71196 ko | Rewriter/Util/Tactics/RunTacticAsConstr.vo 0m00.04s | 66892 ko | Rewriter/Util/Tactics/SetEvars.vo 0m00.04s | 68008 ko | Rewriter/Util/Tactics/SetoidSubst.vo 0m00.04s | 71696 ko | Rewriter/Util/Tactics/SpecializeBy.vo 0m00.04s | 66612 ko | Rewriter/Util/Tactics/Test.vo 0m00.04s | 67532 ko | Rewriter/Util/Tactics/TransparentAssert.vo 0m00.04s | 71692 ko | Rewriter/Util/Tactics/UniquePose.vo 0m00.04s | 73876 ko | Util/Bool/IsTrue.vo 0m00.04s | 88728 ko | Util/CPSNotations.vo 0m00.04s | 72316 ko | Util/DefaultedTypes.vo 0m00.04s | 82328 ko | Util/FixCoqMistakes.vo 0m00.04s | 72616 ko | Util/FueledLUB.vo 0m00.04s | 71648 ko | Util/GlobalSettings.vo 0m00.04s | 81796 ko | Util/Logic/Forall.vo 0m00.04s | 90052 ko | Util/Notations.vo 0m00.04s | 80564 ko | Util/SideConditions/CorePackages.vo 0m00.04s | 90496 ko | Util/Sigma/Lift.vo 0m00.04s | 120280 ko | Util/Sigma/Related.vo 0m00.04s | 84752 ko | Util/Tactics/BreakMatch.vo 0m00.04s | 74384 ko | Util/Tactics/CacheTerm.vo 0m00.04s | 72076 ko | Util/Tactics/ClearDuplicates.vo 0m00.04s | 76896 ko | Util/Tactics/CountBinders.vo 0m00.04s | 77572 ko | Util/Tactics/DestructHyps.vo 0m00.04s | 72156 ko | Util/Tactics/ESpecialize.vo 0m00.04s | 71980 ko | Util/Tactics/GetGoal.vo 0m00.04s | 72144 ko | Util/Tactics/Not.vo 0m00.04s | 72064 ko | Util/Tactics/PrintContext.vo 0m00.04s | 72032 ko | Util/Tactics/Revert.vo 0m00.04s | 76596 ko | Util/Tactics/RunTacticAsConstr.vo 0m00.04s | 81368 ko | Util/Tactics/SpecializeAllWays.vo 0m00.04s | 77200 ko | Util/Tactics/SpecializeBy.vo 0m00.04s | 77672 ko | Util/Tactics/SplitInContext.vo 0m00.04s | 77668 ko | Util/Unit.vo 0m00.04s | 69576 ko | tests/ReadmeExampleTests.vo 0m00.03s | 67388 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Notations.vo 0m00.03s | 68120 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/eqexact.vo 0m00.03s | 69424 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/util/Learning.vo 0m00.03s | 68104 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/PrimitivePair.vo 0m00.03s | 99780 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/Prod.vo 0m00.03s | 76828 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Ltac2Lib/Constr.vo 0m00.03s | 66784 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/eabstract.vo 0m00.03s | 68904 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/syntactic_unify.vo 0m00.03s | 79752 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/runsToNonDet.vo 0m00.03s | 69660 ko | Lens.vo 0m00.03s | 76192 ko | Rewriter/Util/Bool/Equality.vo 0m00.03s | 76964 ko | Rewriter/Util/FixCoqMistakes.vo 0m00.03s | 66452 ko | Rewriter/Util/GlobalSettings.vo 0m00.03s | 84400 ko | Rewriter/Util/Notations.vo 0m00.03s | 78964 ko | Rewriter/Util/Tactics/BreakMatch.vo 0m00.03s | 69012 ko | Rewriter/Util/Tactics/CacheTerm.vo 0m00.03s | 66992 ko | Rewriter/Util/Tactics/Contains.vo 0m00.03s | 67196 ko | Rewriter/Util/Tactics/PrintGoal.vo 0m00.03s | 84548 ko | Util/Comparison.vo 0m00.03s | 75468 ko | Util/Curry.vo 0m00.03s | 103676 ko | Util/LetIn.vo 0m00.03s | 79772 ko | Util/Logic/Exists.vo 0m00.03s | 90204 ko | Util/Logic/ProdForall.vo 0m00.03s | 94432 ko | Util/Sumbool.vo 0m00.03s | 74280 ko | Util/Tactics/CPSId.vo 0m00.03s | 71920 ko | Util/Tactics/ConstrFail.vo 0m00.03s | 72232 ko | Util/Tactics/DestructTrivial.vo 0m00.03s | 81492 ko | Util/Tactics/DoWithHyp.vo 0m00.03s | 72212 ko | Util/Tactics/EvarExists.vo 0m00.03s | 72108 ko | Util/Tactics/EvarNormalize.vo 0m00.03s | 76224 ko | Util/Tactics/Head.vo 0m00.03s | 72372 ko | Util/Tactics/PoseTermWithName.vo 0m00.03s | 72060 ko | Util/Tactics/SetEvars.vo 0m00.03s | 73296 ko | Util/Tactics/SetoidSubst.vo 0m00.03s | 73092 ko | Util/Tactics/UnifyAbstractReflexivity.vo 0m00.03s | 76928 ko | Util/Tactics/UniquePose.vo 0m00.03s | 69080 ko | tests/LensTests.vo 0m00.03s | 74856 ko | tests/RegressionTests.vo 0m00.02s | 65992 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Macros/subst.vo 0m00.02s | 67144 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/letexists.vo 0m00.02s | 66976 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/sanity.vo 0m00.02s | 68144 ko | Coqprime/Tactic/Tactic.vo 0m00.02s | 66904 ko | Rewriter/Util/Tactics/GetGoal.vo 0m00.02s | 66896 ko | Rewriter/Util/Tactics/Not.vo 0m00.02s | 67044 ko | Rewriter/Util/Tactics/PrintContext.vo 0m00.02s | 72240 ko | Rewriter/Util/Tactics/SplitInContext.vo 0m00.02s | 67008 ko | Rewriter/Util/Tactics/SubstEvars.vo 0m00.02s | 72184 ko | Util/Tactics/ClearbodyAll.vo 0m00.02s | 75868 ko | Util/Tactics/ETransitivity.vo 0m00.02s | 71936 ko | Util/Tactics/HasBody.vo 0m00.02s | 72188 ko | Util/Tactics/NormalizeCommutativeIdentifier.vo 0m00.02s | 72560 ko | Util/Tactics/PrintGoal.vo 0m00.02s | 73076 ko | Util/Tactics/SimplifyProjections.vo 0m00.02s | 72488 ko | Util/Tactics/SimplifyRepeatedIfs.vo 0m00.02s | 72104 ko | Util/Tactics/SubstLet.vo 0m00.02s | 71872 ko | Util/Tactics/Test.vo 0m00.02s | 72896 ko | Util/Tactics/VM.vo 0m00.02s | 88676 ko | Util/Tower.vo 0m00.02s | 72740 ko | tests/PrintingTests.vo 0m00.01s | 68216 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd_bool_hints.vo 0m00.01s | 76328 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/PowerFunc.vo 0m00.01s | 79404 ko | Rewriter/Util/Comparison.vo 0m00.01s | 66696 ko | Rewriter/Util/Tactics/ConstrFail.vo 0m00.01s | 68728 ko | Rewriter/Util/TypeList.vo 0m00.01s | 66836 ko | Rewriter/Util/plugins/StrategyTactic.vo 0m00.01s | 72984 ko | Util/Isomorphism.vo 0m00.01s | 73372 ko | Util/Pos.vo 0m00.01s | 76532 ko | Util/Tactics/HeadUnderBinders.vo 0m00.01s | 72144 ko | Util/Tactics/SideConditionsBeforeToAfter.vo 0m00.00s | 74492 ko | Util/Sigma/Associativity.vo 0m00.00s | 73956 ko | Util/Sigma/MapProjections.vo 0m00.00s | 72172 ko | Util/Tactics/Contains.vo ``` </p> </details> 19 January 2022, 21:09:12 UTC
4785bb9 Jason Gross 19 January 2022, 19:38:40 UTC Add relevant bedrock2 files to pre-standalone 19 January 2022, 19:38:40 UTC
back to top