https://github.com/mit-plv/fiat-crypto
Name Target Message Date
HEAD a4bdf47 Bump rupicola from `e504468` to `34b7686` (#1323) 08 July 2022, 05:38:58 UTC
refs/heads/F_lia 657eb50 Implement F_lia tactic for solving goals on field elements 27 October 2021, 16:36:14 UTC
refs/heads/PhD-Dissertation-2021-perf-data 0b1ebe1 Fix perf.csv generation 28 June 2021, 17:28:42 UTC
refs/heads/asm-boring-ssl 230e572 WIP bounds 26 April 2022, 18:59:33 UTC
refs/heads/bedrock2inlinetable 16dd2bb bump rupicola/bedrock2 and adapt to expr.inlinetable feature 05 December 2020, 07:38:20 UTC
refs/heads/ci-on-upstream-ubuntu 20ff71d Update coq.yml 10 October 2021, 19:29:49 UTC
refs/heads/compile-x25519-and-inversion-fix-function-name 135cab8 compiler returned None because fe25519_inv was misnamed "exp_5789...", while caller (montladder) used "fe25519_inv" to call it To find in which phase the compilation fails, one can debug as follows: Goal compile (compile_ext_call (funname_env:=SortedListString.map)) (map.of_list (skipn 2 funcs)) = None. Proof. unfold compile, compose_phases. match goal with | |- match ?x with _ => _ end = None => let x' := eval vm_compute in x in change_no_check x with x' end. cbv beta iota. match goal with | |- match ?x with _ => _ end = None => let x' := eval vm_compute in x in change_no_check x with x' end. cbv beta iota. match goal with | |- match ?x with _ => _ end = None => let x' := eval vm_compute in x in change_no_check x with x' end. cbv beta iota. cbv [LowerPipeline.riscvPhase]. match goal with | |- match ?x with _ => _ end = None => let x' := eval vm_compute in x in change_no_check x with x' end. This shows that everything goes well until `riscvPhase`, which calls `compiler.FitsStack.stack_usage`, which returns `None`, which should only happen if there's a stackalloc whose number of bytes is not divisible by bytes_per_word, or if a function calls a non-existent function, which was the problem here. 08 December 2021, 05:39:00 UTC
refs/heads/compiler-integration b64e689 do not use a precomputed table in ed25519 sign - this patch was tested on an older copy of signer_main.c - untested here - we may want to revert this later for almost 4x speedup 14 December 2020, 19:06:44 UTC
refs/heads/dependabot/github_actions/actions/setup-java-3.4.1 9a340a1 Bump actions/setup-java from 3.4.0 to 3.4.1 Bumps [actions/setup-java](https://github.com/actions/setup-java) from 3.4.0 to 3.4.1. - [Release notes](https://github.com/actions/setup-java/releases) - [Commits](https://github.com/actions/setup-java/compare/v3.4.0...v3.4.1) --- updated-dependencies: - dependency-name: actions/setup-java dependency-type: direct:production update-type: version-update:semver-patch ... Signed-off-by: dependabot[bot] <support@github.com> 11 July 2022, 16:29:29 UTC
refs/heads/fe25519_inv 189ce92 unify inv interface 07 March 2022, 23:06:50 UTC
refs/heads/fermat 0c8a2a2 finish removing dependency on old fermat_little (but still need coqprime for euler criterion and build fails because new fermat_little is not computable) 08 October 2019, 14:47:39 UTC
refs/heads/generic-montgomery abb9768 Add a WIP version of WBW Montgomery that is generic over prime 20 May 2021, 00:11:17 UTC
refs/heads/karatsuba 641088f Merge branch 'karatsuba' 16 March 2017, 01:56:17 UTC
refs/heads/lattice 0df26cd change q_nbits to nat, make helper for mapping on matrices 05 February 2019, 18:17:38 UTC
refs/heads/lean 4a5bb46 Better examples 22 November 2019, 22:21:11 UTC
refs/heads/master a4bdf47 Bump rupicola from `e504468` to `34b7686` (#1323) 08 July 2022, 05:38:58 UTC
refs/heads/montladder-integration 4ba8ecc integrate from_word and cswap with montledder 22 February 2022, 19:57:12 UTC
refs/heads/more-general-balance2 32b3d8f add length/eval lemmas so build works, fix up comments 28 July 2020, 11:34:51 UTC
refs/heads/perf-testing-data-2021-01-24-rewriting 6966564 Add temp logs (build of csv doesn't quite work :-( ) From The Coq Proof Assistant, version 8.12.2 (December 2020) compiled on Dec 29 2020 22:22:37 with OCaml 4.06.1 24 January 2021, 17:36:07 UTC
refs/heads/perf-testing-data-ITP-2022-rewriting 72fe0dd make perf csv ``` make COQBIN="$HOME/.local64/coq/coq-8.11.1/bin/" SKIP_BEDROCK2=1 TIMED=1 --output-sync perf-csv ``` 15 July 2021, 00:27:45 UTC
refs/heads/perf-testing-data-PLDI-2020-rewriting e38849f Fix lingering xargs 28 June 2021, 20:45:50 UTC
refs/heads/perf-testing-data-POPL-2020-rewriting 84c89e7 Add new .txt files 01 November 2019, 19:47:56 UTC
refs/heads/perf-testing-data-POPL-2022-rewriting 72fe0dd make perf csv ``` make COQBIN="$HOME/.local64/coq/coq-8.11.1/bin/" SKIP_BEDROCK2=1 TIMED=1 --output-sync perf-csv ``` 15 July 2021, 00:27:45 UTC
refs/heads/poly1305 c59a5ee make update-_CoqProject 01 April 2017, 18:15:53 UTC
refs/heads/rewrite-if 7d2fe91 Rewriter.Rules: simplify if true, if false 05 July 2022, 19:47:13 UTC
refs/heads/scalarmult 24490e9 add TODO 20 August 2020, 15:34:58 UTC
refs/heads/scalarmult2 1943880 use stackalloc in scmul implementation 20 August 2020, 19:46:18 UTC
refs/heads/scalarmult3 cfaa85b Bignum_to_bytes proved; representation working 07 September 2020, 00:27:24 UTC
refs/heads/sp2019latest 6fea450 Merge pull request #1310 from JasonGross/sp2019latest+strict-hints [sp2019latest] Adaptation w.r.t. coq/coq#16004 03 July 2022, 02:52:06 UTC
refs/heads/top-level-proof-1 df77590 admit riscv_word_ok instance 02 March 2022, 15:14:07 UTC
refs/heads/v8.10 764cca8 Bump rupicola for coqutil compat with Coq 8.1{1,2} 21 September 2021, 18:59:27 UTC
refs/heads/v8.6 1636b68 Add some more things to basesystem_partial_evaluation_unfolder 18 October 2017, 04:13:52 UTC
refs/heads/v8.8 269fe7a Fixes #392 Issue had been hanging around for a while 27 September 2019, 19:02:25 UTC
refs/heads/vector 589baa4 new instruction vpaddq; vector registers added 01 July 2022, 17:56:39 UTC
refs/heads/x25519-printing e9eafb5 printing for demo 21 April 2022, 17:21:05 UTC
refs/origin/sp2019latest 6eadbf4 Merge remote-tracking branch 'origin/fix_fancy4' 07 January 2019, 07:38:13 UTC
refs/tags/v0.0.1-alpha 6b70efd copy the licence, etc files to fiat-rust in make 04 February 2020, 04:30:37 UTC
refs/tags/v0.0.10 c92bed3 Update generated Rust files 13 December 2021, 08:37:54 UTC
refs/tags/v0.0.11 25ce137 Autogenerate fiat-rust/src/lib.rs Fixes #1089, exposing poly1305 27 December 2021, 23:39:37 UTC
refs/tags/v0.0.12 6ccc663 Fix `app_consts` Roughly the issue is that app_consts leaves over spurious x * 1 that don't get removed by subsequent passes. c.f. https://github.com/mit-plv/fiat-crypto/pull/1134#issuecomment-1074461171 22 March 2022, 01:49:47 UTC
refs/tags/v0.0.13 36ef68f Add support for SKIP_COQSCRIPTS_INCLUDE=1 29 March 2022, 22:51:08 UTC
refs/tags/v0.0.2-alpha ad5026f Generate all functions for all bedrock2 files Note that we need to set `-Wno-error=tautological-compare`. It's unfortunate that the rewriter can't yet deal with non-linear patterns to optimize away self-comparisons, though it's possible we could be more clever in the initial rewrite rules to avoid this case? 21 April 2020, 23:21:21 UTC
refs/tags/v0.0.2-beta f423db3 Proofreading README 01 May 2020, 12:26:55 UTC
refs/tags/v0.0.3-alpha 1776b15 Use Rust docstring comments Addresses part of #785 09 May 2020, 21:46:36 UTC
refs/tags/v0.0.3-beta 51abc74 Bump rust crate version for new version of code 11 May 2020, 05:42:00 UTC
refs/tags/v0.0.3-beta2 aed3c7d Automatically bump rust crate version on release This way we don't forget to do it in future releases. 13 May 2020, 22:53:17 UTC
refs/tags/v0.0.3-beta3 47278b0 Try again to auto-bump crate version 13 May 2020, 23:01:21 UTC
refs/tags/v0.0.3-beta4 e835012 Try again to auto-bump crate version 13 May 2020, 23:08:06 UTC
refs/tags/v0.0.4 ccf644f Add p448_32 Disable p448 x32 on backends w/o int128 support It doesn't work due to #797 <details><summary>Timing Diff</summary> <p> ``` Time | Peak Mem | File Name ---------------------------------------------------------------------------- 63m03.86s | 1916264 ko | Total Time / Peak Mem ---------------------------------------------------------------------------- 7m48.59s | 812688 ko | fiat-rust/src/p384_32.rs 7m43.34s | 930444 ko | fiat-go/src/p384_32.go 7m37.87s | 1071224 ko | fiat-bedrock2/src/p384_32.c 7m37.37s | 1065336 ko | fiat-java/src/FiatP384.java 7m37.03s | 1074936 ko | fiat-c/src/p384_32.c 0m52.25s | 63728 ko | fiat-bedrock2/src/p521_64.c 0m50.72s | 69828 ko | fiat-go/src/p521_64.go 0m50.68s | 62288 ko | fiat-c/src/p521_64.c 0m50.59s | 62252 ko | fiat-rust/src/p521_64.rs 0m43.59s | 1594940 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery 0m42.99s | 1594780 ko | ExtractionOCaml/word_by_word_montgomery 0m36.77s | 75096 ko | fiat-bedrock2/src/p448_solinas_32.c 0m31.68s | 1252444 ko | ExtractionOCaml/bedrock2_unsaturated_solinas 0m31.39s | 45904 ko | fiat-java/src/FiatP448Solinas.java 0m31.30s | 1213388 ko | ExtractionOCaml/unsaturated_solinas 0m30.60s | 50876 ko | fiat-go/src/p448_solinas_32.go 0m30.28s | 190236 ko | fiat-bedrock2/src/p256_32.c 0m30.13s | 46416 ko | fiat-c/src/p448_solinas_32.c 0m29.76s | 1053884 ko | ExtractionOCaml/perf_word_by_word_montgomery 0m29.46s | 51052 ko | fiat-rust/src/p448_solinas_32.rs 0m29.26s | 190512 ko | fiat-bedrock2/src/secp256k1_32.c 0m29.02s | 1053672 ko | ExtractionOCaml/bedrock2_base_conversion 0m28.70s | 196588 ko | fiat-java/src/FiatSecp256K1.java 0m28.08s | 217476 ko | fiat-java/src/FiatP256.java 0m27.73s | 198524 ko | fiat-rust/src/secp256k1_32.rs 0m27.69s | 1916264 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml 0m27.62s | 1086056 ko | ExtractionOCaml/bedrock2_saturated_solinas 0m27.26s | 189608 ko | fiat-c/src/secp256k1_32.c 0m27.26s | 215472 ko | fiat-go/src/p256_32.go 0m27.13s | 1089140 ko | ExtractionOCaml/base_conversion 0m26.96s | 1787860 ko | ExtractionOCaml/word_by_word_montgomery.ml 0m26.82s | 190440 ko | fiat-rust/src/p256_32.rs 0m26.65s | 189664 ko | fiat-c/src/p256_32.c 0m26.25s | 1054328 ko | ExtractionOCaml/saturated_solinas 0m25.68s | 1086780 ko | ExtractionOCaml/perf_unsaturated_solinas 0m25.54s | 209344 ko | fiat-go/src/secp256k1_32.go 0m23.53s | 52116 ko | fiat-bedrock2/src/p448_solinas_64.c 0m22.64s | 118728 ko | fiat-bedrock2/src/p434_64.c 0m22.43s | 46136 ko | fiat-go/src/p448_solinas_64.go 0m22.15s | 46056 ko | fiat-rust/src/p448_solinas_64.rs 0m22.05s | 45892 ko | fiat-c/src/p448_solinas_64.c 0m20.98s | 1585224 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml 0m20.27s | 123684 ko | fiat-rust/src/p434_64.rs 0m19.23s | 131440 ko | fiat-c/src/p434_64.c 0m19.17s | 1531960 ko | ExtractionOCaml/unsaturated_solinas.ml 0m18.86s | 123072 ko | fiat-go/src/p434_64.go 0m17.83s | 1729860 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml 0m17.82s | 1490644 ko | ExtractionOCaml/bedrock2_base_conversion.ml 0m16.85s | 1507296 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml 0m16.79s | 1762800 ko | ExtractionOCaml/perf_unsaturated_solinas.ml 0m16.59s | 1512576 ko | ExtractionOCaml/saturated_solinas.ml 0m16.46s | 1483712 ko | ExtractionOCaml/base_conversion.ml 0m12.39s | 129480 ko | fiat-go/src/p224_32.go 0m12.38s | 116660 ko | fiat-bedrock2/src/p224_32.c 0m12.38s | 115040 ko | fiat-java/src/FiatP224.java 0m12.22s | 115064 ko | fiat-rust/src/p224_32.rs 0m12.03s | 115652 ko | fiat-c/src/p224_32.c 0m10.38s | 82772 ko | fiat-bedrock2/src/p384_64.c 0m08.92s | 79460 ko | fiat-rust/src/p384_64.rs 0m08.64s | 78952 ko | fiat-c/src/p384_64.c 0m08.55s | 79640 ko | fiat-go/src/p384_64.go 0m04.12s | 33240 ko | fiat-bedrock2/src/curve25519_32.c 0m03.54s | 25924 ko | fiat-java/src/FiatCurve25519.java 0m03.49s | 25636 ko | fiat-go/src/curve25519_32.go 0m03.49s | 24396 ko | fiat-rust/src/curve25519_32.rs 0m03.47s | 25820 ko | fiat-c/src/curve25519_32.c 0m02.37s | 25400 ko | fiat-bedrock2/src/curve25519_64.c 0m02.33s | 23336 ko | fiat-go/src/curve25519_64.go 0m02.24s | 24212 ko | fiat-rust/src/curve25519_64.rs 0m02.23s | 24088 ko | fiat-c/src/curve25519_64.c 0m02.05s | 771148 ko | Bedrock/StandaloneOCamlMain.vo 0m02.03s | 34112 ko | fiat-bedrock2/src/secp256k1_64.c 0m02.00s | 759356 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo 0m01.97s | 33988 ko | fiat-bedrock2/src/p224_64.c 0m01.94s | 32776 ko | fiat-go/src/secp256k1_64.go 0m01.92s | 32964 ko | fiat-go/src/p224_64.go 0m01.90s | 31848 ko | fiat-bedrock2/src/p256_64.c 0m01.86s | 33052 ko | fiat-rust/src/secp256k1_64.rs 0m01.84s | 32692 ko | fiat-go/src/p256_64.go 0m01.82s | 32744 ko | fiat-c/src/secp256k1_64.c 0m01.82s | 33900 ko | fiat-rust/src/p224_64.rs 0m01.79s | 33916 ko | fiat-c/src/p224_64.c 0m01.72s | 34012 ko | fiat-rust/src/p256_64.rs 0m01.70s | 745148 ko | StandaloneOCamlMain.vo 0m01.62s | 35656 ko | fiat-c/src/p256_64.c 0m00.43s | 20536 ko | fiat-bedrock2/src/poly1305_32.c 0m00.38s | 16816 ko | fiat-java/src/FiatPoly1305.java 0m00.37s | 16936 ko | fiat-go/src/poly1305_32.go 0m00.37s | 17920 ko | fiat-rust/src/poly1305_32.rs 0m00.35s | 18024 ko | fiat-c/src/poly1305_32.c 0m00.31s | 17700 ko | fiat-go/src/poly1305_64.go 0m00.29s | 18852 ko | fiat-bedrock2/src/poly1305_64.c 0m00.26s | 16880 ko | fiat-c/src/poly1305_64.c 0m00.26s | 16816 ko | fiat-rust/src/poly1305_64.rs ``` </p> 20 May 2020, 00:02:51 UTC
refs/tags/v0.0.5 5eb8a89 Regenerate bedrock2 files 09 November 2020, 01:44:28 UTC
refs/tags/v0.0.6 5eb8a89 Regenerate bedrock2 files 09 November 2020, 01:44:28 UTC
refs/tags/v0.0.7 3f4581b Update .gitignore with https://github.com/github/gitignore/pull/3701 27 April 2021, 13:18:54 UTC
refs/tags/v0.0.8 2d76718 Update fancy machine to use the new curve_good requests 17 May 2021, 22:48:10 UTC
refs/tags/v0.0.9 23d2dbc Factor utility lemmas from x86 out of asm files Also add some lemmas for compat of x86 branch with 8.11 <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 61m30.85s | 1990484 ko | Total Time / Peak Mem | 61m25.90s | 1991316 ko || +0m04.94s || -832 ko | +0.13% | -0.04% -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 1m28.11s | 1516788 ko | SlowPrimeSynthesisExamples.vo | 1m25.30s | 1516872 ko || +0m02.81s || -84 ko | +3.29% | -0.00% 3m18.24s | 1702064 ko | Curves/Montgomery/XZProofs.vo | 3m16.75s | 1640968 ko || +0m01.49s || 61096 ko | +0.75% | +3.72% 4m21.92s | 1350984 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 4m21.95s | 1370208 ko || -0m00.02s || -19224 ko | -0.01% | -1.40% 3m49.43s | 1990484 ko | Rewriter/Passes/ArithWithCasts.vo | 3m49.56s | 1991316 ko || -0m00.12s || -832 ko | -0.05% | -0.04% 3m04.56s | 1609256 ko | Rewriter/Passes/NBE.vo | 3m04.56s | 1609184 ko || +0m00.00s || 72 ko | +0.00% | +0.00% 2m51.21s | 1176040 ko | Fancy/Compiler.vo | 2m51.21s | 1176784 ko || +0m00.00s || -744 ko | +0.00% | -0.06% 2m27.09s | 1765524 ko | Rewriter/Passes/ToFancyWithCasts.vo | 2m27.13s | 1621832 ko || -0m00.03s || 143692 ko | -0.02% | +8.85% 2m18.79s | 933052 ko | AbstractInterpretation/Wf.vo | 2m18.92s | 934624 ko || -0m00.13s || -1572 ko | -0.09% | -0.16% 2m00.23s | 1042084 ko | Bedrock/Field/Synthesis/Examples/X25519_64.vo | 1m59.90s | 1042060 ko || +0m00.32s || 24 ko | +0.27% | +0.00% 1m49.43s | 1213588 ko | Bedrock/Group/ScalarMult/LadderStep.vo | 1m49.31s | 1285028 ko || +0m00.12s || -71440 ko | +0.10% | -5.55% 1m38.44s | 434576 ko | Spec/Test/X25519.vo | 1m38.41s | 434468 ko || +0m00.03s || 108 ko | +0.03% | +0.02% 1m37.11s | 1434840 ko | Fancy/Barrett256.vo | 1m37.05s | 1397932 ko || +0m00.06s || 36908 ko | +0.06% | +2.64% 1m15.51s | 1130132 ko | UnsaturatedSolinasHeuristics/Tests.vo | 1m15.22s | 1130096 ko || +0m00.29s || 36 ko | +0.38% | +0.00% 1m14.09s | 1317332 ko | Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo | 1m14.29s | 1317232 ko || -0m00.19s || 100 ko | -0.26% | +0.00% 1m12.98s | 791080 ko | AbstractInterpretation/Proofs.vo | 1m12.87s | 797516 ko || +0m00.10s || -6436 ko | +0.15% | -0.80% 1m11.33s | 1285096 ko | Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo | 1m11.37s | 1288764 ko || -0m00.04s || -3668 ko | -0.05% | -0.28% 1m08.57s | 856328 ko | AbstractInterpretation/ZRangeProofs.vo | 1m08.90s | 855948 ko || -0m00.33s || 380 ko | -0.47% | +0.04% 1m04.54s | 1436764 ko | Bedrock/Field/Synthesis/Examples/p224_64.vo | 1m04.53s | 1436720 ko || +0m00.01s || 44 ko | +0.01% | +0.00% 1m02.97s | 1406988 ko | Bedrock/Field/Synthesis/Examples/p256_64.vo | 1m03.14s | 1406892 ko || -0m00.17s || 96 ko | -0.26% | +0.00% 1m01.76s | 1327100 ko | Fancy/Montgomery256.vo | 1m01.74s | 1345380 ko || +0m00.01s || -18280 ko | +0.03% | -1.35% 1m00.99s | 928944 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 1m00.86s | 928892 ko || +0m00.13s || 52 ko | +0.21% | +0.00% 1m00.84s | 1120888 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo | 1m00.54s | 1120708 ko || +0m00.30s || 180 ko | +0.49% | +0.01% 1m00.79s | 1038612 ko | Rewriter/Passes/MultiRetSplit.vo | 1m00.69s | 1036692 ko || +0m00.10s || 1920 ko | +0.16% | +0.18% 0m54.44s | 776008 ko | Rewriter/RulesProofs.vo | 0m54.41s | 771220 ko || +0m00.03s || 4788 ko | +0.05% | +0.62% 0m53.67s | 1123148 ko | Rewriter/Passes/Arith.vo | 0m53.57s | 1123208 ko || +0m00.10s || -60 ko | +0.18% | -0.00% 0m46.61s | 622308 ko | Demo.vo | 0m47.43s | 624428 ko || -0m00.82s || -2120 ko | -1.72% | -0.33% 0m42.36s | 854840 ko | Bedrock/Field/Synthesis/Examples/LadderStep.vo | 0m42.49s | 855052 ko || -0m00.13s || -212 ko | -0.30% | -0.02% 0m36.57s | 891372 ko | Rewriter/Passes/MulSplit.vo | 0m36.54s | 890896 ko || +0m00.03s || 476 ko | +0.08% | +0.05% 0m31.19s | 880480 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m31.04s | 880640 ko || +0m00.15s || -160 ko | +0.48% | -0.01% 0m31.08s | 523240 ko | Arithmetic/Saturated.vo | 0m31.15s | 523384 ko || -0m00.07s || -144 ko | -0.22% | -0.02% 0m30.39s | 934236 ko | PushButtonSynthesis/BYInversionReificationCache.vo | 0m30.38s | 934176 ko || +0m00.01s || 60 ko | +0.03% | +0.00% 0m28.85s | 852056 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m28.82s | 851796 ko || +0m00.03s || 260 ko | +0.10% | +0.03% 0m28.16s | 891892 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m28.11s | 891756 ko || +0m00.05s || 136 ko | +0.17% | +0.01% 0m26.24s | 1071932 ko | Assembly/Parse/TestAsm.vo | 0m26.14s | 1071820 ko || +0m00.09s || 112 ko | +0.38% | +0.01% 0m23.15s | 872612 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m23.21s | 871584 ko || -0m00.06s || 1028 ko | -0.25% | +0.11% 0m21.01s | 794684 ko | Bedrock/Field/Translation/Proofs/Expr.vo | 0m20.89s | 788616 ko || +0m00.12s || 6068 ko | +0.57% | +0.76% 0m20.13s | 831868 ko | Bedrock/Field/Synthesis/Examples/X1305_32.vo | 0m19.99s | 831944 ko || +0m00.14s || -76 ko | +0.70% | -0.00% 0m17.61s | 544676 ko | Arithmetic/BarrettReduction.vo | 0m17.43s | 543440 ko || +0m00.17s || 1236 ko | +1.03% | +0.22% 0m17.31s | 576056 ko | Arithmetic/WordByWordMontgomery.vo | 0m17.25s | 570092 ko || +0m00.05s || 5964 ko | +0.34% | +1.04% 0m17.14s | 853912 ko | Curves/Edwards/XYZT/Basic.vo | 0m16.96s | 853168 ko || +0m00.17s || 744 ko | +1.06% | +0.08% 0m17.04s | 709932 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo | 0m17.15s | 709848 ko || -0m00.10s || 84 ko | -0.64% | +0.01% 0m16.87s | 648496 ko | Util/ZUtil/ArithmeticShiftr.vo | 0m16.81s | 648796 ko || +0m00.06s || -300 ko | +0.35% | -0.04% 0m16.70s | 515116 ko | Arithmetic/Core.vo | 0m16.56s | 515192 ko || +0m00.14s || -76 ko | +0.84% | -0.01% 0m16.69s | 795996 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo | 0m16.43s | 802952 ko || +0m00.26s || -6956 ko | +1.58% | -0.86% 0m16.58s | 772104 ko | Language/IdentifiersGENERATED.vo | 0m16.52s | 772196 ko || +0m00.05s || -92 ko | +0.36% | -0.01% 0m16.05s | 631640 ko | Bedrock/Field/Common/Util.vo | 0m15.91s | 631508 ko || +0m00.14s || 132 ko | +0.87% | +0.02% 0m15.91s | 717092 ko | Curves/Edwards/AffineProofs.vo | 0m15.86s | 717008 ko || +0m00.05s || 84 ko | +0.31% | +0.01% 0m15.21s | 584124 ko | Stringification/IR.vo | 0m15.17s | 583972 ko || +0m00.04s || 152 ko | +0.26% | +0.02% 0m14.51s | 871992 ko | StandaloneDebuggingExamples.vo | 0m14.60s | 871788 ko || -0m00.08s || 204 ko | -0.61% | +0.02% 0m13.44s | 597140 ko | Language/IdentifiersGENERATEDProofs.vo | 0m13.91s | 596824 ko || -0m00.47s || 316 ko | -3.37% | +0.05% 0m13.38s | 774580 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m13.46s | 774652 ko || -0m00.08s || -72 ko | -0.59% | -0.00% 0m12.85s | 753740 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m12.86s | 753808 ko || -0m00.00s || -68 ko | -0.07% | -0.00% 0m12.14s | 684432 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m12.09s | 684092 ko || +0m00.05s || 340 ko | +0.41% | +0.04% 0m12.13s | 610120 ko | Util/ZRange/LandLorBounds.vo | 0m12.04s | 609660 ko || +0m00.09s || 460 ko | +0.74% | +0.07% 0m11.66s | 862584 ko | PushButtonSynthesis/SmallExamples.vo | 0m11.25s | 862320 ko || +0m00.41s || 264 ko | +3.64% | +0.03% 0m11.13s | 478384 ko | Primitives/MxDHRepChange.vo | 0m11.18s | 478448 ko || -0m00.04s || -64 ko | -0.44% | -0.01% 0m09.27s | 496716 ko | Arithmetic/FancyMontgomeryReduction.vo | 0m09.29s | 495060 ko || -0m00.01s || 1656 ko | -0.21% | +0.33% 0m09.11s | 748216 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m08.97s | 746784 ko || +0m00.13s || 1432 ko | +1.56% | +0.19% 0m08.94s | 599776 ko | Language/IdentifiersBasicGENERATED.vo | 0m09.01s | 599956 ko || -0m00.07s || -180 ko | -0.77% | -0.03% 0m08.91s | 598964 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo | 0m08.92s | 598940 ko || -0m00.00s || 24 ko | -0.11% | +0.00% 0m08.01s | 919520 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo | 0m07.99s | 919420 ko || +0m00.01s || 100 ko | +0.25% | +0.01% 0m07.96s | 486892 ko | Util/ZRange/CornersMonotoneBounds.vo | 0m07.99s | 486792 ko || -0m00.03s || 100 ko | -0.37% | +0.02% 0m07.90s | 620364 ko | Bedrock/Field/Translation/Proofs/Flatten.vo | 0m07.97s | 620296 ko || -0m00.06s || 68 ko | -0.87% | +0.01% 0m07.85s | 694052 ko | PushButtonSynthesis/BaseConversion.vo | 0m07.97s | 693928 ko || -0m00.12s || 124 ko | -1.50% | +0.01% 0m07.64s | 614616 ko | Bedrock/Group/ScalarMult/ScalarMult.vo | 0m07.70s | 614484 ko || -0m00.06s || 132 ko | -0.77% | +0.02% 0m07.01s | 569692 ko | Rewriter/Passes/NoSelect.vo | 0m06.93s | 569096 ko || +0m00.08s || 596 ko | +1.15% | +0.10% 0m06.66s | 706040 ko | PushButtonSynthesis/Primitives.vo | 0m06.64s | 706056 ko || +0m00.02s || -16 ko | +0.30% | -0.00% 0m06.50s | 600068 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m06.41s | 599968 ko || +0m00.08s || 100 ko | +1.40% | +0.01% 0m06.38s | 939028 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo | 0m06.44s | 939032 ko || -0m00.06s || -4 ko | -0.93% | -0.00% 0m05.83s | 499848 ko | Util/ZUtil/Modulo.vo | 0m05.73s | 499632 ko || +0m00.09s || 216 ko | +1.74% | +0.04% 0m05.81s | 541936 ko | Arithmetic/BYInv.vo | 0m05.84s | 541648 ko || -0m00.03s || 288 ko | -0.51% | +0.05% 0m05.61s | 738192 ko | Bedrock/Field/Synthesis/Examples/EncodeDecode.vo | 0m05.59s | 738220 ko || +0m00.02s || -28 ko | +0.35% | -0.00% 0m05.52s | 548784 ko | Language/InversionExtra.vo | 0m05.34s | 545900 ko || +0m00.17s || 2884 ko | +3.37% | +0.52% 0m05.49s | 624900 ko | BoundsPipeline.vo | 0m05.46s | 624776 ko || +0m00.03s || 124 ko | +0.54% | +0.01% 0m05.40s | 520816 ko | COperationSpecifications.vo | 0m05.42s | 520772 ko || -0m00.01s || 44 ko | -0.36% | +0.00% 0m05.17s | 558312 ko | Fancy/Prod.vo | 0m05.24s | 558392 ko || -0m00.07s || -80 ko | -1.33% | -0.01% 0m04.98s | 631904 ko | Assembly/Syntax.vo | 0m04.98s | 631380 ko || +0m00.00s || 524 ko | +0.00% | +0.08% 0m04.74s | 462548 ko | Arithmetic/MontgomeryReduction/Proofs.vo | 0m04.79s | 462520 ko || -0m00.04s || 28 ko | -1.04% | +0.00% 0m04.73s | 688060 ko | PushButtonSynthesis/BarrettReduction.vo | 0m04.78s | 687720 ko || -0m00.04s || 340 ko | -1.04% | +0.04% 0m04.57s | 490360 ko | UnsaturatedSolinasHeuristics.vo | 0m04.58s | 489520 ko || -0m00.00s || 840 ko | -0.21% | +0.17% 0m04.34s | 491352 ko | Util/ZRange/BasicLemmas.vo | 0m04.42s | 491136 ko || -0m00.08s || 216 ko | -1.80% | +0.04% 0m03.80s | 479516 ko | Arithmetic/UniformWeight.vo | 0m03.82s | 478644 ko || -0m00.02s || 872 ko | -0.52% | +0.18% 0m03.74s | 478744 ko | Arithmetic/BarrettReduction/Generalized.vo | 0m03.78s | 478724 ko || -0m00.03s || 20 ko | -1.05% | +0.00% 0m03.70s | 702764 ko | Bedrock/Field/Synthesis/Examples/MulTwice.vo | 0m03.77s | 702796 ko || -0m00.06s || -32 ko | -1.85% | -0.00% 0m03.67s | 476992 ko | CastLemmas.vo | 0m03.58s | 476964 ko || +0m00.08s || 28 ko | +2.51% | +0.00% 0m03.46s | 558456 ko | PushButtonSynthesis/BaseConversionReificationCache.vo | 0m03.43s | 558280 ko || +0m00.02s || 176 ko | +0.87% | +0.03% 0m03.37s | 701092 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.48s | 701000 ko || -0m00.10s || 92 ko | -3.16% | +0.01% 0m03.31s | 508260 ko | Assembly/Semantics.vo | 0m03.21s | 508316 ko || +0m00.10s || -56 ko | +3.11% | -0.01% 0m03.31s | 522400 ko | Rewriter/Passes/Test.vo | 0m03.31s | 522408 ko || +0m00.00s || -8 ko | +0.00% | -0.00% 0m03.31s | 481420 ko | Util/ZUtil/LandLorBounds.vo | 0m03.32s | 481828 ko || -0m00.00s || -408 ko | -0.30% | -0.08% 0m03.27s | 685920 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.29s | 685724 ko || -0m00.02s || 196 ko | -0.60% | +0.02% 0m03.21s | 533872 ko | Rewriter/Passes/AddAssocLeft.vo | 0m03.18s | 533704 ko || +0m00.02s || 168 ko | +0.94% | +0.03% 0m03.13s | 471776 ko | Util/ZUtil/LandLorShiftBounds.vo | 0m03.17s | 472456 ko || -0m00.04s || -680 ko | -1.26% | -0.14% 0m03.11s | 471740 ko | Arithmetic/BarrettReduction/HAC.vo | 0m03.09s | 471264 ko || +0m00.02s || 476 ko | +0.64% | +0.10% 0m02.89s | 696520 ko | CLI.vo | 0m02.92s | 696384 ko || -0m00.02s || 136 ko | -1.02% | +0.01% 0m02.81s | 533152 ko | Rewriter/Passes/FlattenThunkedRects.vo | 0m02.92s | 533304 ko || -0m00.10s || -152 ko | -3.76% | -0.02% 0m02.63s | 503896 ko | Util/ZUtil/Morphisms.vo | 0m02.63s | 503864 ko || +0m00.00s || 32 ko | +0.00% | +0.00% 0m02.57s | 464304 ko | Arithmetic/Primitives.vo | 0m02.59s | 464028 ko || -0m00.02s || 276 ko | -0.77% | +0.05% 0m02.37s | 480652 ko | Arithmetic/Freeze.vo | 0m02.33s | 479460 ko || +0m00.04s || 1192 ko | +1.71% | +0.24% 0m02.31s | 465796 ko | Util/ZUtil/TwosComplement.vo | 0m02.31s | 465692 ko || +0m00.00s || 104 ko | +0.00% | +0.02% 0m02.28s | 468932 ko | Util/ZUtil/Shift.vo | 0m02.26s | 468988 ko || +0m00.02s || -56 ko | +0.88% | -0.01% 0m02.27s | 620024 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo | 0m02.30s | 620032 ko || -0m00.02s || -8 ko | -1.30% | -0.00% 0m02.17s | 472028 ko | Arithmetic/BaseConversion.vo | 0m02.12s | 471888 ko || +0m00.04s || 140 ko | +2.35% | +0.02% 0m02.17s | 530996 ko | Rewriter/Passes/UnfoldValueBarrier.vo | 0m02.25s | 530896 ko || -0m00.08s || 100 ko | -3.55% | +0.01% 0m02.12s | 535208 ko | Bedrock/Field/Translation/Expr.vo | 0m02.15s | 535144 ko || -0m00.02s || 64 ko | -1.39% | +0.01% 0m02.07s | 530948 ko | Rewriter/Passes/StripLiteralCasts.vo | 0m02.02s | 530792 ko || +0m00.04s || 156 ko | +2.47% | +0.02% 0m02.04s | 458040 ko | Util/ZUtil/Testbit.vo | 0m02.07s | 458036 ko || -0m00.02s || 4 ko | -1.44% | +0.00% 0m02.00s | 454608 ko | Util/ZUtil/ModInv.vo | 0m02.11s | 457112 ko || -0m00.10s || -2504 ko | -5.21% | -0.54% 0m01.96s | 457568 ko | Util/ZUtil/Div.vo | 0m01.96s | 457820 ko || +0m00.00s || -252 ko | +0.00% | -0.05% 0m01.94s | 554116 ko | Stringification/Language.vo | 0m02.00s | 554072 ko || -0m00.06s || 44 ko | -3.00% | +0.00% 0m01.92s | 456528 ko | Arithmetic/BarrettReduction/RidiculousFish.vo | 0m01.93s | 456388 ko || -0m00.01s || 140 ko | -0.51% | +0.03% 0m01.89s | 476704 ko | Arithmetic/ModOps.vo | 0m01.92s | 476780 ko || -0m00.03s || -76 ko | -1.56% | -0.01% 0m01.83s | 581544 ko | CompilersTestCases.vo | 0m01.85s | 584836 ko || -0m00.02s || -3292 ko | -1.08% | -0.56% 0m01.80s | 466128 ko | Arithmetic/ModularArithmeticTheorems.vo | 0m01.94s | 466236 ko || -0m00.13s || -108 ko | -7.21% | -0.02% 0m01.76s | 454524 ko | Util/Tuple.vo | 0m01.76s | 455292 ko || +0m00.00s || -768 ko | +0.00% | -0.16% 0m01.74s | 506628 ko | AbstractInterpretation/AbstractInterpretation.vo | 0m01.76s | 506536 ko || -0m00.02s || 92 ko | -1.13% | +0.01% 0m01.73s | 529296 ko | Rewriter/Passes/ToFancy.vo | 0m01.83s | 529176 ko || -0m00.10s || 120 ko | -5.46% | +0.02% 0m01.71s | 536504 ko | AbstractInterpretation/ZRange.vo | 0m01.75s | 536588 ko || -0m00.04s || -84 ko | -2.28% | -0.01% 0m01.62s | 619728 ko | Bedrock/Field/Common/Names/MakeNames.vo | 0m01.67s | 619760 ko || -0m00.04s || -32 ko | -2.99% | -0.00% 0m01.61s | 494640 ko | Bedrock/Field/Interface/Compilation.vo | 0m01.60s | 494616 ko || +0m00.01s || 24 ko | +0.62% | +0.00% 0m01.61s | 697828 ko | Rewriter/PerfTesting/Core.vo | 0m01.62s | 697864 ko || -0m00.01s || -36 ko | -0.61% | -0.00% 0m01.54s | 521944 ko | Stringification/Go.vo | 0m01.49s | 522556 ko || +0m00.05s || -612 ko | +3.35% | -0.11% 0m01.53s | 457796 ko | Util/ZUtil/Pow2Mod.vo | 0m01.51s | 457856 ko || +0m00.02s || -60 ko | +1.32% | -0.01% 0m01.52s | 630524 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo | 0m01.44s | 629852 ko || +0m00.08s || 672 ko | +5.55% | +0.10% 0m01.52s | 537472 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo | 0m01.48s | 537464 ko || +0m00.04s || 8 ko | +2.70% | +0.00% 0m01.51s | 465372 ko | Assembly/Parse.vo | 0m01.59s | 465668 ko || -0m00.08s || -296 ko | -5.03% | -0.06% 0m01.45s | 471620 ko | Util/ZRange/SplitRangeBounds.vo | 0m01.46s | 471604 ko || -0m00.01s || 16 ko | -0.68% | +0.00% 0m01.42s | 704852 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m01.39s | 704764 ko || +0m00.03s || 88 ko | +2.15% | +0.01% 0m01.41s | 502200 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo | 0m01.51s | 502060 ko || -0m00.10s || 140 ko | -6.62% | +0.02% 0m01.41s | 464600 ko | Util/ZUtil/Bitwise.vo | 0m01.45s | 464460 ko || -0m00.04s || 140 ko | -2.75% | +0.03% 0m01.35s | 503408 ko | Arithmetic/PrimeFieldTheorems.vo | 0m01.25s | 503744 ko || +0m00.10s || -336 ko | +8.00% | -0.06% 0m01.29s | 617364 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo | 0m01.37s | 617436 ko || -0m00.08s || -72 ko | -5.83% | -0.01% 0m01.28s | 468428 ko | Util/ZUtil/Quot.vo | 0m01.28s | 468296 ko || +0m00.00s || 132 ko | +0.00% | +0.02% 0m01.23s | 461340 ko | Arithmetic/Partition.vo | 0m01.23s | 461124 ko || +0m00.00s || 216 ko | +0.00% | +0.04% 0m01.18s | 455968 ko | Util/ZUtil/Ones.vo | 0m01.09s | 455832 ko || +0m00.08s || 136 ko | +8.25% | +0.02% 0m01.17s | 444308 ko | Fancy/Spec.vo | 0m01.15s | 444352 ko || +0m00.02s || -44 ko | +1.73% | -0.00% 0m01.14s | 635044 ko | Bedrock/Field/Interface/Representation.vo | 0m01.06s | 634616 ko || +0m00.07s || 428 ko | +7.54% | +0.06% 0m01.14s | 680088 ko | Bedrock/Field/Stringification/Stringification.vo | 0m01.15s | 680040 ko || -0m00.01s || 48 ko | -0.86% | +0.00% 0m01.13s | 671752 ko | Bedrock/Field/Synthesis/Generic/Tactics.vo | 0m01.06s | 671640 ko || +0m00.06s || 112 ko | +6.60% | +0.01% 0m01.13s | 703676 ko | Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.vo | 0m01.14s | 703560 ko || -0m00.01s || 116 ko | -0.87% | +0.01% 0m01.12s | 692472 ko | Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.vo | 0m01.12s | 692268 ko || +0m00.00s || 204 ko | +0.00% | +0.02% 0m01.12s | 473096 ko | Util/ZRange/SplitBounds.vo | 0m01.14s | 473104 ko || -0m00.01s || -8 ko | -1.75% | -0.00% 0m01.12s | 449856 ko | Util/ZUtil/AddGetCarry.vo | 0m01.15s | 450052 ko || -0m00.02s || -196 ko | -2.60% | -0.04% 0m01.11s | 611772 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo | 0m01.05s | 611932 ko || +0m00.06s || -160 ko | +5.71% | -0.02% 0m01.10s | 676524 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m01.12s | 676356 ko || -0m00.02s || 168 ko | -1.78% | +0.02% 0m01.10s | 712464 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m01.09s | 712620 ko || +0m00.01s || -156 ko | +0.91% | -0.02% 0m01.09s | 672372 ko | Bedrock/Field/Synthesis/Specialized/Tactics.vo | 0m00.91s | 672380 ko || +0m00.18s || -8 ko | +19.78% | -0.00% 0m01.08s | 675140 ko | Bedrock/Field/Synthesis/Generic/Operation.vo | 0m01.07s | 675244 ko || +0m00.01s || -104 ko | +0.93% | -0.01% 0m01.08s | 618104 ko | Bedrock/Field/Translation/Cmd.vo | 0m01.20s | 618396 ko || -0m00.11s || -292 ko | -9.99% | -0.04% 0m01.05s | 424760 ko | Util/ZUtil/OnesFrom.vo | 0m01.07s | 424684 ko || -0m00.02s || 76 ko | -1.86% | +0.01% 0m01.04s | 712232 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m01.04s | 712140 ko || +0m00.00s || 92 ko | +0.00% | +0.01% 0m01.04s | 437920 ko | Curves/Edwards/XYZT/Precomputed.vo | 0m01.21s | 438028 ko || -0m00.16s || -108 ko | -14.04% | -0.02% 0m01.04s | 689692 ko | StandaloneOCamlMain.vo | 0m01.05s | 689504 ko || -0m00.01s || 188 ko | -0.95% | +0.02% 0m01.03s | 520256 ko | Stringification/JSON.vo | 0m01.19s | 519884 ko || -0m00.15s || 372 ko | -13.44% | +0.07% 0m01.02s | 632612 ko | Bedrock/Field/Translation/Parameters/SelectParameters.vo | 0m00.96s | 632620 ko || +0m00.06s || -8 ko | +6.25% | -0.00% 0m01.01s | 688788 ko | StandaloneHaskellMain.vo | 0m01.05s | 688876 ko || -0m00.04s || -88 ko | -3.80% | -0.01% 0m01.00s | 681844 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m01.09s | 681808 ko || -0m00.09s || 36 ko | -8.25% | +0.00% 0m00.97s | 682240 ko | Bedrock/Field/Synthesis/Specialized/ReifiedOperation.vo | 0m01.01s | 682068 ko || -0m00.04s || 172 ko | -3.96% | +0.02% 0m00.97s | 631772 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m00.99s | 631568 ko || -0m00.02s || 204 ko | -2.02% | +0.03% 0m00.96s | 617480 ko | Bedrock/Field/Translation/Func.vo | 0m00.92s | 617356 ko || +0m00.03s || 124 ko | +4.34% | +0.02% 0m00.96s | 631492 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m00.96s | 631584 ko || +0m00.00s || -92 ko | +0.00% | -0.01% 0m00.95s | 519120 ko | Stringification/C.vo | 0m00.99s | 519080 ko || -0m00.04s || 40 ko | -4.04% | +0.00% 0m00.94s | 550372 ko | Assembly/Equivalence.vo | 0m01.02s | 550652 ko || -0m00.08s || -280 ko | -7.84% | -0.05% 0m00.92s | 520072 ko | Stringification/Zig.vo | 0m00.93s | 520032 ko || -0m00.01s || 40 ko | -1.07% | +0.00% 0m00.89s | 629652 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m00.95s | 629328 ko || -0m00.05s || 324 ko | -6.31% | +0.05% 0m00.86s | 519424 ko | Stringification/Rust.vo | 0m00.91s | 519212 ko || -0m00.05s || 212 ko | -5.49% | +0.04% 0m00.86s | 456284 ko | Util/ZUtil/TruncatingShiftl.vo | 0m00.81s | 456092 ko || +0m00.04s || 192 ko | +6.17% | +0.04% 0m00.85s | 519164 ko | Stringification/Java.vo | 0m00.90s | 519208 ko || -0m00.05s || -44 ko | -5.55% | -0.00% 0m00.83s | 580632 ko | Bedrock/Field/Common/Tactics.vo | 0m00.76s | 580504 ko || +0m00.06s || 128 ko | +9.21% | +0.02% 0m00.83s | 522380 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo | 0m00.72s | 522256 ko || +0m00.10s || 124 ko | +15.27% | +0.02% 0m00.81s | 524152 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo | 0m00.82s | 523904 ko || -0m00.00s || 248 ko | -1.21% | +0.04% 0m00.80s | 524288 ko | Bedrock/Field/Translation/LoadStoreList.vo | 0m00.75s | 524268 ko || +0m00.05s || 20 ko | +6.66% | +0.00% 0m00.78s | 529496 ko | Bedrock/Field/Stringification/FlattenVarData.vo | 0m00.77s | 529492 ko || +0m00.01s || 4 ko | +1.29% | +0.00% 0m00.76s | 498324 ko | Language/APINotations.vo | 0m00.78s | 498232 ko || -0m00.02s || 92 ko | -2.56% | +0.01% 0m00.75s | 490512 ko | Bedrock/ScalarField/Interface/Compilation.vo | 0m00.76s | 490564 ko || -0m00.01s || -52 ko | -1.31% | -0.01% 0m00.75s | 495092 ko | MiscCompilerPassesProofsExtra.vo | 0m00.69s | 494996 ko || +0m00.06s || 96 ko | +8.69% | +0.01% 0m00.74s | 523384 ko | Bedrock/Field/Common/Types.vo | 0m00.70s | 523416 ko || +0m00.04s || -32 ko | +5.71% | -0.00% 0m00.74s | 546124 ko | Rewriter/All.vo | 0m00.73s | 546132 ko || +0m00.01s || -8 ko | +1.36% | -0.00% 0m00.73s | 454756 ko | Arithmetic/BarrettReduction/Wikipedia.vo | 0m00.76s | 454916 ko || -0m00.03s || -160 ko | -3.94% | -0.03% 0m00.73s | 522316 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo | 0m00.69s | 522172 ko || +0m00.04s || 144 ko | +5.79% | +0.02% 0m00.73s | 460424 ko | Util/NumTheoryUtil.vo | 0m00.64s | 460604 ko || +0m00.08s || -180 ko | +14.06% | -0.03% 0m00.69s | 522344 ko | Bedrock/Field/Translation/Flatten.vo | 0m00.67s | 522400 ko || +0m00.01s || -56 ko | +2.98% | -0.01% 0m00.69s | 435656 ko | Rewriter/Rules.vo | 0m00.74s | 435660 ko || -0m00.05s || -4 ko | -6.75% | -0.00% 0m00.66s | 511652 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo | 0m00.69s | 511520 ko || -0m00.02s || 132 ko | -4.34% | +0.02% 0m00.66s | 497080 ko | Language/WfExtra.vo | 0m00.64s | 497008 ko || +0m00.02s || 72 ko | +3.12% | +0.01% 0m00.65s | 494840 ko | Language/UnderLetsProofsExtra.vo | 0m00.64s | 495132 ko || +0m00.01s || -292 ko | +1.56% | -0.05% 0m00.65s | 497424 ko | Rewriter/AllTacticsExtra.vo | 0m00.60s | 497524 ko || +0m00.05s || -100 ko | +8.33% | -0.02% 0m00.64s | 499412 ko | AbstractInterpretation/WfExtra.vo | 0m00.71s | 499360 ko || -0m00.06s || 52 ko | -9.85% | +0.01% 0m00.64s | 509520 ko | PushButtonSynthesis/ReificationCache.vo | 0m00.67s | 509416 ko || -0m00.03s || 104 ko | -4.47% | +0.02% 0m00.63s | 490496 ko | Language/API.vo | 0m00.66s | 490452 ko || -0m00.03s || 44 ko | -4.54% | +0.00% 0m00.61s | 437524 ko | Util/ZRange/OperationsBounds.vo | 0m00.58s | 437376 ko || +0m00.03s || 148 ko | +5.17% | +0.03% 0m00.60s | 470064 ko | Util/QUtil.vo | 0m00.46s | 470032 ko || +0m00.13s || 32 ko | +30.43% | +0.00% 0m00.59s | 454756 ko | Util/ZUtil/Stabilization.vo | 0m00.56s | 454792 ko || +0m00.02s || -36 ko | +5.35% | -0.00% 0m00.58s | 431820 ko | ArithmeticCPS/WordByWordMontgomery.vo | 0m00.56s | 431584 ko || +0m00.01s || 236 ko | +3.57% | +0.05% 0m00.56s | 429368 ko | ArithmeticCPS/Freeze.vo | 0m00.54s | 429284 ko || +0m00.02s || 84 ko | +3.70% | +0.01% 0m00.56s | 421348 ko | Util/CPSUtil.vo | 0m00.62s | 421360 ko || -0m00.05s || -12 ko | -9.67% | -0.00% 0m00.55s | 460104 ko | Util/ZUtil/CC.vo | 0m00.55s | 460032 ko || +0m00.00s || 72 ko | +0.00% | +0.01% 0m00.54s | 443144 ko | Assembly/Equality.vo | 0m00.60s | 443240 ko || -0m00.05s || -96 ko | -9.99% | -0.02% 0m00.53s | 434684 ko | Bedrock/Specs/Field.vo | 0m00.53s | 434564 ko || +0m00.00s || 120 ko | +0.00% | +0.02% 0m00.52s | 413800 ko | Bedrock/Group/Point.vo | 0m00.48s | 413664 ko || +0m00.04s || 136 ko | +8.33% | +0.03% 0m00.52s | 433812 ko | Bedrock/Specs/Group.vo | 0m00.46s | 433808 ko || +0m00.06s || 4 ko | +13.04% | +0.00% 0m00.51s | 454632 ko | ArithmeticCPS/ModOps.vo | 0m00.45s | 454436 ko || +0m00.06s || 196 ko | +13.33% | +0.04% 0m00.51s | 449912 ko | Util/Decidable/Decidable2Bool.vo | 0m00.47s | 449908 ko || +0m00.04s || 4 ko | +8.51% | +0.00% 0m00.47s | 440884 ko | Bedrock/Specs/ScalarField.vo | 0m00.60s | 440816 ko || -0m00.13s || 68 ko | -21.66% | +0.01% 0m00.45s | 440700 ko | ArithmeticCPS/BaseConversion.vo | 0m00.41s | 440240 ko || +0m00.04s || 460 ko | +9.75% | +0.10% 0m00.45s | 450104 ko | ArithmeticCPS/Saturated.vo | 0m00.46s | 450096 ko || -0m00.01s || 8 ko | -2.17% | +0.00% 0m00.44s | 447832 ko | ArithmeticCPS/Core.vo | 0m00.41s | 447832 ko || +0m00.03s || 0 ko | +7.31% | +0.00% 0m00.43s | 445164 ko | Util/ZUtil/Ltz.vo | 0m00.38s | 445268 ko || +0m00.04s || -104 ko | +13.15% | -0.02% 0m00.42s | 453284 ko | Util/ZUtil/EquivModulo.vo | 0m00.38s | 453060 ko || +0m00.03s || 224 ko | +10.52% | +0.04% 0m00.41s | 420456 ko | Util/HList.vo | 0m00.44s | 420108 ko || -0m00.03s || 348 ko | -6.81% | +0.08% 0m00.41s | 448896 ko | Util/ZUtil/Log2.vo | 0m00.46s | 448852 ko || -0m00.05s || 44 ko | -10.86% | +0.00% 0m00.40s | 457528 ko | Util/ZUtil/SignBit.vo | 0m00.41s | 457556 ko || -0m00.00s || -28 ko | -2.43% | -0.00% 0m00.39s | 456680 ko | Util/ZUtil/Divide.vo | 0m00.39s | 456560 ko || +0m00.00s || 120 ko | +0.00% | +0.02% 0m00.38s | 413784 ko | Language/IdentifierParameters.vo | 0m00.35s | 413788 ko || +0m00.03s || -4 ko | +8.57% | -0.00% 0m00.38s | 453164 ko | Util/ZUtil/Land.vo | 0m00.40s | 452980 ko || -0m00.02s || 184 ko | -5.00% | +0.04% 0m00.37s | 424472 ko | Util/ZRange.vo | 0m00.40s | 424412 ko || -0m00.03s || 60 ko | -7.50% | +0.01% 0m00.36s | 396768 ko | Language/PreExtra.vo | 0m00.32s | 396744 ko || +0m00.03s || 24 ko | +12.49% | +0.00% 0m00.35s | 405464 ko | Rewriter/TestRules.vo | 0m00.37s | 405440 ko || -0m00.02s || 24 ko | -5.40% | +0.00% 0m00.35s | 365772 ko | Rewriter/TestRulesProofs.vo | 0m00.35s | 365476 ko || +0m00.00s || 296 ko | +0.00% | +0.08% 0m00.34s | 424696 ko | Util/ZBounded.vo | 0m00.45s | 424692 ko || -0m00.10s || 4 ko | -24.44% | +0.00% 0m00.32s | 429692 ko | Arithmetic/ModularArithmeticPre.vo | 0m00.36s | 429536 ko || -0m00.03s || 156 ko | -11.11% | +0.03% 0m00.32s | 324964 ko | Util/ZUtil/Tactics/SimplifyFractionsLe.vo | 0m00.27s | 324844 ko || +0m00.04s || 120 ko | +18.51% | +0.03% 0m00.31s | 331912 ko | Arithmetic/MontgomeryReduction/Definition.vo | 0m00.26s | 331780 ko || +0m00.04s || 132 ko | +19.23% | +0.03% 0m00.30s | 335636 ko | Spec/ModularArithmetic.vo | 0m00.32s | 335728 ko || -0m00.02s || -92 ko | -6.25% | -0.02% 0m00.30s | 359368 ko | Util/ZUtil/Lor.vo | 0m00.29s | 359240 ko || +0m00.01s || 128 ko | +3.44% | +0.03% 0m00.30s | 320064 ko | Util/ZUtil/Tactics.vo | 0m00.27s | 320140 ko || +0m00.02s || -76 ko | +11.11% | -0.02% 0m00.30s | 355936 ko | Util/ZUtil/Tactics/SolveRange.vo | 0m00.34s | 355864 ko || -0m00.04s || 72 ko | -11.76% | +0.02% 0m00.30s | 352844 ko | Util/ZUtil/Tactics/SolveTestbit.vo | 0m00.31s | 353120 ko || -0m00.01s || -276 ko | -3.22% | -0.07% 0m00.29s | 347632 ko | Util/ZUtil/Tactics/Ztestbit.vo | 0m00.26s | 347400 ko || +0m00.02s || 232 ko | +11.53% | +0.06% 0m00.27s | 322968 ko | Util/IdfunWithAlt.vo | 0m00.23s | 322844 ko || +0m00.04s || 124 ko | +17.39% | +0.03% 0m00.27s | 332116 ko | Util/ListUtil/Permutation.vo | N/A | N/A || +0m00.27s || 332116 ko | ∞ | ∞ 0m00.26s | 369152 ko | Util/ZUtil.vo | 0m00.30s | 368620 ko || -0m00.03s || 532 ko | -13.33% | +0.14% 0m00.25s | 368968 ko | Util/ZRange/Operations.vo | 0m00.32s | 368944 ko || -0m00.07s || 24 ko | -21.87% | +0.00% 0m00.25s | 321652 ko | Util/ZRange/Show.vo | 0m00.22s | 321460 ko || +0m00.03s || 192 ko | +13.63% | +0.05% 0m00.24s | 291664 ko | Util/SideConditions/Autosolve.vo | 0m00.30s | 291564 ko || -0m00.06s || 100 ko | -20.00% | +0.03% 0m00.23s | 297052 ko | Util/SideConditions/ModInvPackage.vo | 0m00.22s | 296832 ko || +0m00.01s || 220 ko | +4.54% | +0.07% 0m00.23s | 321912 ko | Util/ZUtil/Tactics/ZeroBounds.vo | 0m00.26s | 321496 ko || -0m00.03s || 416 ko | -11.53% | +0.12% 0m00.21s | 339904 ko | Util/ZUtil/Tactics/RewriteModSmall.vo | 0m00.25s | 340112 ko || -0m00.04s || -208 ko | -16.00% | -0.06% 0m00.20s | 268368 ko | Util/ZUtil/Hints.vo | 0m00.21s | 268548 ko || -0m00.00s || -180 ko | -4.76% | -0.06% 0m00.20s | 267548 ko | Util/ZUtil/Hints/ZArith.vo | 0m00.23s | 267636 ko || -0m00.03s || -88 ko | -13.04% | -0.03% 0m00.18s | 313444 ko | Util/NUtil/Testbit.vo | N/A | N/A || +0m00.18s || 313444 ko | ∞ | ∞ 0m00.12s | 182880 ko | Util/ListUtil/PermutationCompat.vo | N/A | N/A || +0m00.12s || 182880 ko | ∞ | ∞ 0m00.04s | 82988 ko | Util/Bool/LeCompat.vo | 0m00.05s | 74072 ko || -0m00.01s || 8916 ko | -20.00% | +12.03% ``` </p> </details> 28 September 2021, 21:46:56 UTC
back to top