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
e872e22 jadep 19 June 2020, 16:28:42 UTC remove line breaks from notes because github doesn't like them 19 June 2020, 16:28:42 UTC
a22adb8 jadep 19 June 2020, 16:24:11 UTC add notes from a close-read of BoringSSL curve25519 code for later reference 19 June 2020, 16:25:16 UTC
c0dcbb8 jadep 17 June 2020, 09:20:48 UTC fix typo 18 June 2020, 16:31:35 UTC
570ca50 jadep 17 June 2020, 09:17:13 UTC add missing import 18 June 2020, 16:31:35 UTC
72ef67b jadep 16 June 2020, 16:07:54 UTC prove admit in EncodeDecode.v 18 June 2020, 16:31:35 UTC
a115243 jadep 01 June 2020, 11:02:36 UTC replace encode_no_reduce with partition (and use that to prove an admit in Bedrock/Interfaces) 18 June 2020, 16:31:35 UTC
fb68225 jadep 15 June 2020, 09:32:30 UTC update notations in bedrock2 synthesis examples 15 June 2020, 15:14:43 UTC
2ddec0a jadep 12 June 2020, 12:09:45 UTC remove stray print statement 15 June 2020, 15:14:43 UTC
c5873dd jadep 12 June 2020, 11:13:11 UTC use newly exported bounds definitions for UnsaturatedSolinas interface 15 June 2020, 15:14:43 UTC
509a624 jadep 12 June 2020, 09:50:12 UTC use vm_cast_no_check instead of (vm_compute; reflexivity) 15 June 2020, 15:14:43 UTC
b0f3449 jadep 12 June 2020, 09:49:08 UTC move lemmas to String util 15 June 2020, 15:14:43 UTC
a283122 jadep 02 June 2020, 11:20:13 UTC more feedback from Jason: improve tactics and apply fixes to things that cause warnings 15 June 2020, 15:14:43 UTC
cc2ed04 jadep 01 June 2020, 13:51:19 UTC incorporate feedback from Jason (add TODO for a larger lemma-restructure) 15 June 2020, 15:14:43 UTC
5bc81d6 jadep 01 June 2020, 08:58:33 UTC minor fixup after rebase 15 June 2020, 15:14:43 UTC
a8a4897 jadep 31 May 2020, 14:51:35 UTC remove debugging, insert (hopefully) fix for to_bytes issue 15 June 2020, 15:14:43 UTC
25c256b jadep 29 May 2020, 12:40:36 UTC debugging statement, remove comment 15 June 2020, 15:14:43 UTC
58ffa3b jadep 29 May 2020, 12:39:47 UTC separate correctness from funcs/specs to improve performance of straightline_call 15 June 2020, 15:14:43 UTC
e3e8908 jadep 29 May 2020, 09:46:55 UTC nicer specs and naming, straightline_call now super slow but proofs in ladderstep work eventually 15 June 2020, 15:14:43 UTC
d858cb4 jadep 28 May 2020, 11:43:21 UTC remove bounds from operation postconditions, more automation in examples, more debugging for master 15 June 2020, 15:14:43 UTC
b71f321 jadep 28 May 2020, 09:56:22 UTC more debugging for master 15 June 2020, 15:14:43 UTC
de3f508 jadep 27 May 2020, 19:11:41 UTC ladderstep example 15 June 2020, 15:14:43 UTC
eec8025 jadep 27 May 2020, 11:45:10 UTC more debugging 15 June 2020, 15:14:43 UTC
82bd580 jadep 27 May 2020, 11:35:09 UTC restructure API.v into Synthesis/ directory with examples separated out 15 June 2020, 15:14:43 UTC
60212b0 jadep 27 May 2020, 08:44:33 UTC change so 8.11 doesn't error and I can see debugging statement for master 15 June 2020, 15:14:43 UTC
afd7fa0 jadep 26 May 2020, 16:57:37 UTC insert debugging statement to help debug master build 15 June 2020, 15:14:43 UTC
0f8f6af jadep 26 May 2020, 14:25:29 UTC tweak logic for proving output length of to_bytes 15 June 2020, 15:14:43 UTC
45f64b5 jadep 26 May 2020, 11:24:34 UTC add encode/decode test to API 15 June 2020, 15:14:43 UTC
8daf7b7 jadep 26 May 2020, 10:22:28 UTC cleanup 15 June 2020, 15:14:43 UTC
5f84303 jadep 26 May 2020, 10:16:57 UTC add all unsaturated solinas operations to UnsaturatedSolinas.v and API.v 15 June 2020, 15:14:43 UTC
1f49a89 jadep 21 May 2020, 20:02:52 UTC try to fix build on master 15 June 2020, 15:14:43 UTC
9f65cb9 jadep 21 May 2020, 16:33:42 UTC remove Tests/ from _CoqProject 15 June 2020, 15:14:43 UTC
eb9cabb jadep 21 May 2020, 14:22:24 UTC fix API.v 15 June 2020, 15:14:43 UTC
62ce13c jadep 21 May 2020, 14:22:11 UTC remove Tests/ 15 June 2020, 15:14:43 UTC
13d4aba jadep 21 May 2020, 13:51:46 UTC reorganization -- categorize files 15 June 2020, 15:14:43 UTC
fb6058f jadep 21 May 2020, 13:23:46 UTC move UnsaturatedSolinas.v 15 June 2020, 15:14:43 UTC
b5c0b68 jadep 21 May 2020, 13:21:34 UTC factor out generalizable things from UnsaturatedSolinas.v 15 June 2020, 15:14:43 UTC
e872188 jadep 21 May 2020, 11:57:13 UTC more automation in UnsaturatedSolinas.v - all correctness proofs down to one line 15 June 2020, 15:14:43 UTC
9f2c223 jadep 21 May 2020, 11:55:52 UTC more automation in UnsaturatedSolinas.v - all correctness proofs down to a few lines 15 June 2020, 15:14:43 UTC
b6fd680 jadep 21 May 2020, 10:55:55 UTC more automation in UnsaturatedSolinas.v 15 June 2020, 15:14:43 UTC
fb9c6b9 jadep 21 May 2020, 10:46:44 UTC more automation in UnsaturatedSolinas.v 15 June 2020, 15:14:43 UTC
b3982e2 jadep 20 May 2020, 17:44:12 UTC more automation in UnsaturatedSolinas.v 15 June 2020, 15:14:43 UTC
c2503fe jadep 20 May 2020, 16:13:52 UTC fix up API.v 15 June 2020, 15:14:43 UTC
a72d293 jadep 20 May 2020, 15:07:21 UTC undo moving of postcondition and clean up UnsaturatedSolinas interface 15 June 2020, 15:14:43 UTC
50b444e jadep 19 May 2020, 09:08:22 UTC WIP: moving input bounds into postcondition for UnsaturatedSolinas interface 15 June 2020, 15:14:43 UTC
716624f jadep 18 May 2020, 20:42:15 UTC fix typo 15 June 2020, 15:14:43 UTC
c53d477 jadep 18 May 2020, 20:42:03 UTC clean up/automate UnsaturatedSolinas interface 15 June 2020, 15:14:43 UTC
6fe9429 jadep 15 May 2020, 08:28:45 UTC slight arithmetic modification to hopefully fix build for coq master 15 June 2020, 15:14:43 UTC
f60fefd jadep 14 May 2020, 19:49:42 UTC add to_bytes to API 15 June 2020, 15:14:43 UTC
fc8f4f7 jadep 14 May 2020, 19:33:37 UTC add to_bytes to UnsaturatedSolinas (and infrastructure to deal with bytes) 15 June 2020, 15:14:43 UTC
f7a3c56 jadep 14 May 2020, 12:09:10 UTC add add to API.v 15 June 2020, 15:14:43 UTC
554b420 jadep 14 May 2020, 11:57:34 UTC add addition to UnsaturatedSolinas + improve automation 15 June 2020, 15:14:43 UTC
928ba54 jadep 14 May 2020, 11:02:19 UTC more cleanup; move some more lemmas from UnsaturatedSolinas to own files or Util 15 June 2020, 15:14:43 UTC
9477cd6 jadep 14 May 2020, 08:12:37 UTC cleanup; moved some operations like make_names into their own files and simplified the treatment of variable-name generation functions 15 June 2020, 15:14:43 UTC
ad08ae2 jadep 13 May 2020, 11:25:34 UTC update test 15 June 2020, 15:14:43 UTC
c7f48d8 jadep 13 May 2020, 10:51:56 UTC change equivalence to use words, more progress on UnsaturatedSolinas 15 June 2020, 15:14:43 UTC
de1e0b8 jadep 01 May 2020, 00:03:49 UTC state after chat with Andres -- bit of a mess, need to remove word.of_Z from rep.equiv if the rewrite of Bignum is going to work 15 June 2020, 15:14:43 UTC
7dd8d3b jadep 30 April 2020, 05:14:24 UTC try composing API functions 15 June 2020, 15:14:43 UTC
5c5871e jadep 30 April 2020, 03:32:16 UTC add poly1305 test to API 15 June 2020, 15:14:43 UTC
cae2b25 jadep 30 April 2020, 03:26:16 UTC make sure function is fully computed in API 15 June 2020, 15:14:43 UTC
1946b34 jadep 29 April 2020, 22:33:24 UTC clean up API 15 June 2020, 15:14:43 UTC
5107d81 jadep 29 April 2020, 22:10:54 UTC hopefully fix build on master 15 June 2020, 15:14:43 UTC
c2221d7 jadep 29 April 2020, 22:05:46 UTC Add first sketches of an API for bedrock2 synthesis 15 June 2020, 15:14:43 UTC
522e577 jadep 29 April 2020, 17:29:39 UTC clean up parameter selection a bit 15 June 2020, 15:14:43 UTC
a8724ff jadep 29 April 2020, 16:34:34 UTC add Bedrock/UnsaturatedSolinas.v to _CoqProject 15 June 2020, 15:14:43 UTC
a7e13f7 jadep 29 April 2020, 16:33:56 UTC clean up carry_mul correctness proof in Bedrock/UnsaturatedSolinas 15 June 2020, 15:14:43 UTC
2201269 jadep 29 April 2020, 15:31:16 UTC WIP, only bytes<->Bignum left for carry_mul 15 June 2020, 15:14:43 UTC
ddf91dc jadep 29 April 2020, 13:22:30 UTC WIP, only bytes<->Bignum and varname proofs left for carry_mul 15 June 2020, 15:14:43 UTC
3b24ae0 jadep 28 April 2020, 12:56:49 UTC WIP 15 June 2020, 15:14:43 UTC
a9eec83 jadep 27 April 2020, 21:10:54 UTC WIP 15 June 2020, 15:14:43 UTC
64945b3 jadep 27 April 2020, 18:17:01 UTC more work on parameterized carry_mul proof -- full skeleton of proof 15 June 2020, 15:14:43 UTC
270c632 jadep 27 April 2020, 17:36:47 UTC more work on parameterized carry_mul proof 15 June 2020, 15:14:43 UTC
2af880b jadep 27 April 2020, 15:46:43 UTC first sketches of parameterized UnsaturatedSolinas for bedrock2 15 June 2020, 15:14:43 UTC
bdefb56 Jason Gross 03 June 2020, 18:48:33 UTC Improve stringification of correctness conditions This is required for #670. We now do a bit more post-processing of the correctness conditions, including inlining `let '(x, y) := z in ...` expressions, reducing `fst (x, y)` and `snd (x, y)`, and pulling tuples outside of `if` statements. 04 June 2020, 02:40:38 UTC
14f9ea3 Jason Gross 03 June 2020, 17:01:52 UTC Expose various definitions from PushButtonSynthesis, BoundsPipeline This should help with https://github.com/mit-plv/fiat-crypto/pull/808#discussion_r433797764 Also expose `arg_bounds_of_pipeline`, `out_bounds_of_pipeline`, and `possible_values_of_pipeline` from `BoundsPipeline`. 03 June 2020, 17:01:52 UTC
a841138 Jason Gross 29 May 2020, 02:58:45 UTC Add all-except-compiled, pre-standalone-extracted 29 May 2020, 02:58:45 UTC
d1c9486 Jason Gross 20 May 2020, 05:00:49 UTC Better computation of loose bounds We now compute the loose bounds by recording the number of additions and/or balanced subtractions we want to be able to do in a row before we need to multiply and carry. Note that balanced subtraction always takes a bit more overhead than addition. This is a more conservative variant of #799 that doesn't actually change the bounds, and makes the genuine change of #799 easier to see, namely, reducing `headspace_add_count` from `2` to `1`. 28 May 2020, 22:45:35 UTC
890de05 Jason Gross 25 May 2020, 18:27:39 UTC Reorganize generation of files There's a bit more Makefile magic now, but it should hopefully be easier to add new primes and new languages to the Makefile, now that there is less copy-pasting of boilerplate. We also add targets `all-except-generated` and `lite-generated-files` which should help with https://github.com/coq/coq/pull/12405 27 May 2020, 15:34:42 UTC
e525793 Jason Gross 23 May 2020, 23:08:06 UTC Bump coq-scripts 23 May 2020, 23:08:06 UTC
b5d9ba0 Jason Gross 21 May 2020, 20:28:08 UTC Add UnsaturatedSolinasHeuristics/Tests.v <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ------------------------------------------------------------------------------------------------------------------------------------------- 0m25.96s | 566428 ko | Total Time / Peak Mem | 0m00.00s | 0 ko || +0m25.96s || 566428 ko | N/A | ∞ ------------------------------------------------------------------------------------------------------------------------------------------- 0m25.97s | 566428 ko | UnsaturatedSolinasHeuristics/Tests.vo | N/A | N/A || +0m25.96s || 566428 ko | ∞ | ∞ ``` </p> 23 May 2020, 23:05:05 UTC
493b5fd jadep 21 May 2020, 17:43:37 UTC fix limb count heuristics 21 May 2020, 21:38:00 UTC
9ac37a1 Jason Gross 21 May 2020, 04:01:29 UTC Rework argument parsing, add --tight-bounds-mul-by The `--tight-bounds-mul-by` argument allows us to specify the tight bounds multiplier manually. Closes #800 Closes #796 (actually, this had already been implemented, though we now use it for curve25519) Closes #755 (machine_wordsize is now owned by the binary as a whole) Note that the last of these necessitates moving machine_wordsize to come right after curve_description. Invoking the binaries in the old way may result in them hanging for a long time while they try to compute representations for, say, lists of 2^255-19 5-bit-limbs for the "prime" 64. We now use a structured language to describe the command line arguments, based on OCaml's Arg module interface. The error and help messages are now perhaps a tiny bit worse, but it should now be moderately easier to add new optional command line arguments. Note that named arguments now use spaces rather than equals signs to pass values. The old usage message: ``` USAGE: ./src/ExtractionOCaml/unsaturated_solinas [--lang=LANGUAGE] [--static] [--internal-static] [--no-wide-int] [--widen-carry] [--widen-bytes] [--no-select] [--split-multiret] [--no-primitives] [--cmovznz-by-mul] curve_description n s-c machine_wordsize [function_to_synthesize*] Got 0 arguments. LANGUAGE The output language code should be emitted in. Defaults to C if no language is given. Case-sensitive. Valid options are: C, Rust, Go, Java --static Declare the functions as static, i.e., local to the file. --internal-static Declare internal functions as static, i.e., local to the file. --no-wide-int Don't use integers wider than the bitwidth. --widen-carry Widen carry bit integer types to either the byte type, or to the full bitwidth if --widen-bytes is also passed. --widen-bytes Widen byte types to the full bitwidth. --no-select Use expressions that don't require cmov. --split-multiret Don't allow instructions to return two results. This should always be set for bedrock2. --no-primitives Suppress the generation of the bodies of primitive operations such as addcarryx, subborrowx, cmovznz, mulx, etc. --cmovznz-by-mul Use an alternative implementation of cmovznz using multiplication rather than bitwise-and with -1. curve_description A string which will be prefixed to every function name generated n The number of limbs, or the literal '(auto)' or '(autoN)' for a non-negative number N, to automatically guess the number of limbs s-c The prime, which must be expressed as a difference of a power of two and a small field element (e.g., '2^255 - 19', '2^448 - 2^224 - 1') machine_wordsize The machine bitwidth (e.g., 32 or 64) function_to_synthesize A space-separated list of functions that should be synthesized. If no functions are given, all functions are synthesized. Valid options are carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, or 'carry_scmul' followed by a decimal literal Fatal error: exception Failure("Synthesis failed") ``` The new usage message: ``` ./src/ExtractionOCaml/unsaturated_solinas: option 'curve_description' needs an argument. USAGE: ./src/ExtractionOCaml/unsaturated_solinas [OPTS...] curve_description machine_wordsize n s-c [function_to_synthesize...] --lang {C|Rust|Go|Java} The output language code should be emitted in. Defaults to C if no language is given. Case-sensitive. --static Declare the functions as static, i.e., local to the file. --internal-static Declare internal functions as static, i.e., local to the file. --no-wide-int Don't use integers wider than the bitwidth. --widen-carry Widen carry bit integer types to either the byte type, or to the full bitwidth if --widen-bytes is also passed. --widen-bytes Widen byte types to the full bitwidth. --no-select Use expressions that don't require cmov. --split-multiret Don't allow instructions to return two results. This should always be set for bedrock2. --no-primitives Suppress the generation of the bodies of primitive operations such as addcarryx, subborrowx, cmovznz, mulx, etc. --cmovznz-by-mul Use an alternative implementation of cmovznz using multiplication rather than bitwise-and with -1. --only-signed Only allow signed integer types. --tight-bounds-mul-by The (improper) fraction by which the (tight) bounds of each limb are scaled -h, --help Display this list of options curve_description A string which will be prefixed to every function name generated machine_wordsize The machine bitwidth (e.g., 32 or 64) n The number of limbs, or the literal '(auto)' or '(autoN)' for a non-negative number N, to automatically guess the number of limbs s-c The prime, which must be expressed as a difference of a power of two and a small field element (e.g., '2^255 - 19', '2^448 - 2^224 - 1') function_to_synthesize A space-separated list of functions that should be synthesized. If no functions are given, all functions are synthesized. Valid options are carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, or 'carry_scmul' followed by a decimal literal. Fatal error: exception Failure("Synthesis failed") ``` 21 May 2020, 18:37:42 UTC
49f0a50 Automated Publisher 21 May 2020, 06:10:38 UTC Automated Rust Crate Version Bump: Thu May 21 06:10:39 UTC 2020 ccf644f710b931dad8339aa63c1ce6e95d19a623 21 May 2020, 06:10:38 UTC
ccf644f Jason Gross 20 May 2020, 00:02:51 UTC 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> 21 May 2020, 05:37:39 UTC
d43df58 Jason Gross 20 May 2020, 19:14:55 UTC Fix previous commit 20 May 2020, 19:14:55 UTC
2b5c790 Jason Gross 20 May 2020, 18:58:47 UTC Be more lax about newlines in output diff Compatibility with https://github.com/coq/coq/pull/12358 20 May 2020, 18:58:47 UTC
f1c65d2 Jason Gross 19 May 2020, 22:39:49 UTC Test crate-crypto/Ed448-Goldilocks As per private correspondence with `@kevaundray`, https://github.com/crate-crypto/Ed448-Goldilock now supports a fiat-crypto backend, so we add it to our CI. 20 May 2020, 04:47:00 UTC
b1e83d5 Jason Gross 20 May 2020, 03:55:53 UTC Add relax_list_Z_bounded_by 20 May 2020, 03:55:53 UTC
997e7c5 Jason Gross 20 May 2020, 03:03:37 UTC Add a better nth_error_map 20 May 2020, 03:03:37 UTC
8f1b497 Jason Gross 20 May 2020, 02:47:55 UTC Add In_nth_error_iff 20 May 2020, 02:47:55 UTC
99e2ae0 Jason Gross 19 May 2020, 22:35:54 UTC Bump coq-scripts 19 May 2020, 22:35:54 UTC
c1741e1 Jason Gross 18 May 2020, 18:13:27 UTC Try a different diff 19 May 2020, 18:19:55 UTC
1562eea Jason Gross 18 May 2020, 16:21:43 UTC [coq] Backwards-compatible: Adapt to coq/coq#11980 : Improvements on Print Assumptions Backwards compatible version of #793 Closes #793 19 May 2020, 18:19:55 UTC
50fb0d7 Jason Gross 14 May 2020, 19:33:54 UTC Move the fiat-rust-crate-bumper to etc/ci 14 May 2020, 19:33:54 UTC
8ccd326 Automated Publisher 13 May 2020, 23:10:49 UTC Automated Rust Crate Version Bump: Wed May 13 23:10:49 UTC 2020 e83501253736d8403093203c195457de3f7574f4 13 May 2020, 23:10:49 UTC
e835012 Jason Gross 13 May 2020, 23:08:06 UTC Try again to auto-bump crate version 13 May 2020, 23:08:06 UTC
47278b0 Jason Gross 13 May 2020, 23:01:21 UTC Try again to auto-bump crate version 13 May 2020, 23:01:21 UTC
aed3c7d Jason Gross 13 May 2020, 22:53:17 UTC 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
be9371b Jason Gross 10 May 2020, 20:08:56 UTC Adjust computation of nreductions Based on https://github.com/mit-plv/fiat-crypto/issues/776#issuecomment-623043271 <details><summary>Coq code to generate the table</summary> ```bash echo 'prime | *n* (x64) | nreductions (old, x64) | nreductions (new, x64) | *n* (x32) | nreductions (old, x32) | nreductions (new, x32)'; echo '--|--|--|--|--|--|--'; (COQPATH=$(pwd)/coqprime/src:$(pwd)/rewriter/src coqc -q -R src Crypto src/printtable.v | grep '^"' | sed 's/"//g; s/\*/×/g; s,\^\([0-9]\+\),<sup>\1</sup>,g') ``` ```coq Require Export Coq.ZArith.ZArith. Require Import Coq.QArith.QArith_base Coq.QArith.Qround. Require Export Coq.Strings.String. Require Import Coq.Lists.List. Require Import Crypto.Util.Strings.ParseArithmetic. Require Import Crypto.Util.Strings.ParseArithmeticToTaps. Require Import Crypto.Util.Strings.Show. Import ListNotations. Open Scope string_scope. Open Scope list_scope. Open Scope Z_scope. Definition primes : list string := [ (* single-tap: *) "2^127 - 1"; (* "kummer strikes back" *) "2^129 - 25"; "2^130 - 5"; (* poly1305 *) "2^137 - 13"; "2^140 - 27"; "2^141 - 9"; "2^150 - 5"; "2^150 - 3"; "2^152 - 17"; "2^158 - 15"; "2^165 - 25"; "2^166 - 5"; "2^171 - 19"; "2^174 - 17"; "2^174 - 3"; "2^189 - 25"; "2^190 - 11"; "2^191 - 19"; "2^194 - 33"; "2^196 - 15"; "2^198 - 17"; "2^206 - 5"; "2^212 - 29"; "2^213 - 3"; "2^221 - 3"; "2^222 - 117"; "2^226 - 5"; "2^230 - 27"; "2^235 - 15"; "2^243 - 9"; "2^251 - 9"; "2^255 - 765"; "2^255 - 19"; (* curve25519 *) "2^256 - 189"; "2^266 - 3"; "2^285 - 9"; "2^291 - 19"; "2^321 - 9"; "2^336 - 17"; "2^336 - 3"; "2^338 - 15"; "2^369 - 25"; "2^379 - 19"; "2^382 - 105"; "2^383 - 421"; "2^383 - 187"; "2^383 - 31"; "2^384 - 317"; "2^389 - 21"; "2^401 - 31"; "2^413 - 21"; "2^414 - 17"; "2^444 - 17"; "2^452 - 3"; "2^468 - 17"; "2^488 - 17"; "2^489 - 21"; "2^495 - 31"; "2^511 - 481"; "2^511 - 187"; "2^512 - 569"; "2^521 - 1"; (* p512 *) (* two taps, golden ratio: *) "2^192 - 2^64 - 1"; "2^216 - 2^108 - 1"; "2^322 - 2^161 - 1"; "2^416 - 2^208 - 1"; "2^448 - 2^224 - 1"; (* goldilocks *) "2^450 - 2^225 - 1"; "2^480 - 2^240 - 1"; (* ridinghood *) (* two or more taps *) "2^205 - 45*2^198 - 1"; "2^224 - 2^96 + 1"; (* p224 *) "2^256 - 2^224 + 2^192 + 2^96 - 1"; (* p256 *) "2^256 - 2^32 - 977"; (* bitcoin *) "2^256 - 4294968273"; (* bitcoin, for 64-bit impl *) "2^384 - 2^128 - 2^96 + 2^32 - 1"; (* p384 *) (* Montgomery-Friendly *) "2^256 - 88*2^240 - 1"; "2^254 - 127*2^240 - 1"; "2^384 - 79*2^376 - 1"; "2^384 - 5*2^368 - 1"; "2^512 - 491*2^496 - 1"; "2^510 - 290*2^496 - 1" ]. Local Coercion inject_Z : Z >-> Q. Section nreductions. Context (s : Z) (c : list (Z * Z)) (machine_wordsize : Z). Definition n := Z.to_nat (Qceiling (Z.log2_up s / machine_wordsize)). Definition nreductions_old : nat := let i := fold_right Z.max 0 (map (fun t => Z.log2 (fst t) / machine_wordsize) c) in Z.to_nat (Qceiling (Z.of_nat n / (Z.of_nat n - i))). Definition nreductions_new : nat := let i := fold_right Z.max 0 (map (fun t => Z.log2 (fst t) / machine_wordsize) c) in if Z.of_nat n - i <=? 1 then n else Z.to_nat (Qceiling (Z.of_nat n / (Z.of_nat n - i - 1))). End nreductions. Definition make_table_row (p : string) : string * nat (* n_64 *) * nat (* nreductions_old_64 *) * nat (* nreductions_new_64 *) * nat (* n_32 *) * nat (* nreductions_old_32 *) * nat (* nreductions_new_32 *) := match parseZ_arith_to_taps p with | Some (s, c) => (p, n s 64, nreductions_old s c 64, nreductions_new s c 64, n s 32, nreductions_old s c 32, nreductions_new s c 32) | None => ("", 0, 0, 0, 0, 0, 0) end%nat. Definition table := Eval vm_compute in List.map make_table_row primes. Local Open Scope nat_scope. Declare Scope md_scope. Notation "a | b | .. | c" := (pair .. (pair a b) .. c) (at level 10, format "a | b | .. | c") : md_scope. Notation "a b .. c" := (cons a (cons b .. (cons c nil) .. )) (at level 200, format "a '//' b '//' .. '//' c") : md_scope. Undelimit Scope list_scope. Undelimit Scope core_scope. Close Scope core_scope. Close Scope list_scope. Open Scope md_scope. Print table. (* table = "2^127 - 1" | 2 | 1 | 2 | 4 | 1 | 2 "2^129 - 25" | 3 | 1 | 2 | 5 | 1 | 2 "2^130 - 5" | 3 | 1 | 2 | 5 | 1 | 2 "2^137 - 13" | 3 | 1 | 2 | 5 | 1 | 2 "2^140 - 27" | 3 | 1 | 2 | 5 | 1 | 2 "2^141 - 9" | 3 | 1 | 2 | 5 | 1 | 2 "2^150 - 5" | 3 | 1 | 2 | 5 | 1 | 2 "2^150 - 3" | 3 | 1 | 2 | 5 | 1 | 2 "2^152 - 17" | 3 | 1 | 2 | 5 | 1 | 2 "2^158 - 15" | 3 | 1 | 2 | 5 | 1 | 2 "2^165 - 25" | 3 | 1 | 2 | 6 | 1 | 2 "2^166 - 5" | 3 | 1 | 2 | 6 | 1 | 2 "2^171 - 19" | 3 | 1 | 2 | 6 | 1 | 2 "2^174 - 17" | 3 | 1 | 2 | 6 | 1 | 2 "2^174 - 3" | 3 | 1 | 2 | 6 | 1 | 2 "2^189 - 25" | 3 | 1 | 2 | 6 | 1 | 2 "2^190 - 11" | 3 | 1 | 2 | 6 | 1 | 2 "2^191 - 19" | 3 | 1 | 2 | 6 | 1 | 2 "2^194 - 33" | 4 | 1 | 2 | 7 | 1 | 2 "2^196 - 15" | 4 | 1 | 2 | 7 | 1 | 2 "2^198 - 17" | 4 | 1 | 2 | 7 | 1 | 2 "2^206 - 5" | 4 | 1 | 2 | 7 | 1 | 2 "2^212 - 29" | 4 | 1 | 2 | 7 | 1 | 2 "2^213 - 3" | 4 | 1 | 2 | 7 | 1 | 2 "2^221 - 3" | 4 | 1 | 2 | 7 | 1 | 2 "2^222 - 117" | 4 | 1 | 2 | 7 | 1 | 2 "2^226 - 5" | 4 | 1 | 2 | 8 | 1 | 2 "2^230 - 27" | 4 | 1 | 2 | 8 | 1 | 2 "2^235 - 15" | 4 | 1 | 2 | 8 | 1 | 2 "2^243 - 9" | 4 | 1 | 2 | 8 | 1 | 2 "2^251 - 9" | 4 | 1 | 2 | 8 | 1 | 2 "2^255 - 765" | 4 | 1 | 2 | 8 | 1 | 2 "2^255 - 19" | 4 | 1 | 2 | 8 | 1 | 2 "2^256 - 189" | 4 | 1 | 2 | 8 | 1 | 2 "2^266 - 3" | 5 | 1 | 2 | 9 | 1 | 2 "2^285 - 9" | 5 | 1 | 2 | 9 | 1 | 2 "2^291 - 19" | 5 | 1 | 2 | 10 | 1 | 2 "2^321 - 9" | 6 | 1 | 2 | 11 | 1 | 2 "2^336 - 17" | 6 | 1 | 2 | 11 | 1 | 2 "2^336 - 3" | 6 | 1 | 2 | 11 | 1 | 2 "2^338 - 15" | 6 | 1 | 2 | 11 | 1 | 2 "2^369 - 25" | 6 | 1 | 2 | 12 | 1 | 2 "2^379 - 19" | 6 | 1 | 2 | 12 | 1 | 2 "2^382 - 105" | 6 | 1 | 2 | 12 | 1 | 2 "2^383 - 421" | 6 | 1 | 2 | 12 | 1 | 2 "2^383 - 187" | 6 | 1 | 2 | 12 | 1 | 2 "2^383 - 31" | 6 | 1 | 2 | 12 | 1 | 2 "2^384 - 317" | 6 | 1 | 2 | 12 | 1 | 2 "2^389 - 21" | 7 | 1 | 2 | 13 | 1 | 2 "2^401 - 31" | 7 | 1 | 2 | 13 | 1 | 2 "2^413 - 21" | 7 | 1 | 2 | 13 | 1 | 2 "2^414 - 17" | 7 | 1 | 2 | 13 | 1 | 2 "2^444 - 17" | 7 | 1 | 2 | 14 | 1 | 2 "2^452 - 3" | 8 | 1 | 2 | 15 | 1 | 2 "2^468 - 17" | 8 | 1 | 2 | 15 | 1 | 2 "2^488 - 17" | 8 | 1 | 2 | 16 | 1 | 2 "2^489 - 21" | 8 | 1 | 2 | 16 | 1 | 2 "2^495 - 31" | 8 | 1 | 2 | 16 | 1 | 2 "2^511 - 481" | 8 | 1 | 2 | 16 | 1 | 2 "2^511 - 187" | 8 | 1 | 2 | 16 | 1 | 2 "2^512 - 569" | 8 | 1 | 2 | 16 | 1 | 2 "2^521 - 1" | 9 | 1 | 2 | 17 | 1 | 2 "2^192 - 2^64 - 1" | 3 | 2 | 3 | 6 | 2 | 2 "2^216 - 2^108 - 1" | 4 | 2 | 2 | 7 | 2 | 3 "2^322 - 2^161 - 1" | 6 | 2 | 2 | 11 | 2 | 3 "2^416 - 2^208 - 1" | 7 | 2 | 3 | 13 | 2 | 3 "2^448 - 2^224 - 1" | 7 | 2 | 3 | 14 | 2 | 3 "2^450 - 2^225 - 1" | 8 | 2 | 2 | 15 | 2 | 3 "2^480 - 2^240 - 1" | 8 | 2 | 2 | 15 | 2 | 3 "2^205 - 45*2^198 - 1" | 4 | 4 | 4 | 7 | 7 | 7 "2^224 - 2^96 + 1" | 4 | 2 | 2 | 7 | 2 | 3 "2^256 - 2^224 + 2^192 + 2^96 - 1" | 4 | 4 | 4 | 8 | 8 | 8 "2^256 - 2^32 - 977" | 4 | 1 | 2 | 8 | 2 | 2 "2^256 - 4294968273" | 4 | 1 | 2 | 8 | 1 | 2 "2^384 - 2^128 - 2^96 + 2^32 - 1" | 6 | 2 | 2 | 12 | 2 | 2 "2^256 - 88*2^240 - 1" | 4 | 4 | 4 | 8 | 8 | 8 "2^254 - 127*2^240 - 1" | 4 | 4 | 4 | 8 | 8 | 8 "2^384 - 79*2^376 - 1" | 6 | 6 | 6 | 12 | 12 | 12 "2^384 - 5*2^368 - 1" | 6 | 6 | 6 | 12 | 12 | 12 "2^512 - 491*2^496 - 1" | 8 | 8 | 8 | 16 | 16 | 16 "2^510 - 290*2^496 - 1" | 8 | 8 | 8 | 16 | 16 | 16 : list (string * nat * nat * nat * nat * nat * nat) *) ``` </details> prime | *n* (x64) | nreductions (old, x64) | nreductions (new, x64) | *n* (x32) | nreductions (old, x32) | nreductions (new, x32) --|--|--|--|--|--|-- 2<sup>127</sup> - 1 | 2 | 1 | 2 | 4 | 1 | 2 2<sup>129</sup> - 25 | 3 | 1 | 2 | 5 | 1 | 2 2<sup>130</sup> - 5 | 3 | 1 | 2 | 5 | 1 | 2 2<sup>137</sup> - 13 | 3 | 1 | 2 | 5 | 1 | 2 2<sup>140</sup> - 27 | 3 | 1 | 2 | 5 | 1 | 2 2<sup>141</sup> - 9 | 3 | 1 | 2 | 5 | 1 | 2 2<sup>150</sup> - 5 | 3 | 1 | 2 | 5 | 1 | 2 2<sup>150</sup> - 3 | 3 | 1 | 2 | 5 | 1 | 2 2<sup>152</sup> - 17 | 3 | 1 | 2 | 5 | 1 | 2 2<sup>158</sup> - 15 | 3 | 1 | 2 | 5 | 1 | 2 2<sup>165</sup> - 25 | 3 | 1 | 2 | 6 | 1 | 2 2<sup>166</sup> - 5 | 3 | 1 | 2 | 6 | 1 | 2 2<sup>171</sup> - 19 | 3 | 1 | 2 | 6 | 1 | 2 2<sup>174</sup> - 17 | 3 | 1 | 2 | 6 | 1 | 2 2<sup>174</sup> - 3 | 3 | 1 | 2 | 6 | 1 | 2 2<sup>189</sup> - 25 | 3 | 1 | 2 | 6 | 1 | 2 2<sup>190</sup> - 11 | 3 | 1 | 2 | 6 | 1 | 2 2<sup>191</sup> - 19 | 3 | 1 | 2 | 6 | 1 | 2 2<sup>194</sup> - 33 | 4 | 1 | 2 | 7 | 1 | 2 2<sup>196</sup> - 15 | 4 | 1 | 2 | 7 | 1 | 2 2<sup>198</sup> - 17 | 4 | 1 | 2 | 7 | 1 | 2 2<sup>206</sup> - 5 | 4 | 1 | 2 | 7 | 1 | 2 2<sup>212</sup> - 29 | 4 | 1 | 2 | 7 | 1 | 2 2<sup>213</sup> - 3 | 4 | 1 | 2 | 7 | 1 | 2 2<sup>221</sup> - 3 | 4 | 1 | 2 | 7 | 1 | 2 2<sup>222</sup> - 117 | 4 | 1 | 2 | 7 | 1 | 2 2<sup>226</sup> - 5 | 4 | 1 | 2 | 8 | 1 | 2 2<sup>230</sup> - 27 | 4 | 1 | 2 | 8 | 1 | 2 2<sup>235</sup> - 15 | 4 | 1 | 2 | 8 | 1 | 2 2<sup>243</sup> - 9 | 4 | 1 | 2 | 8 | 1 | 2 2<sup>251</sup> - 9 | 4 | 1 | 2 | 8 | 1 | 2 2<sup>255</sup> - 765 | 4 | 1 | 2 | 8 | 1 | 2 2<sup>255</sup> - 19 | 4 | 1 | 2 | 8 | 1 | 2 2<sup>256</sup> - 189 | 4 | 1 | 2 | 8 | 1 | 2 2<sup>266</sup> - 3 | 5 | 1 | 2 | 9 | 1 | 2 2<sup>285</sup> - 9 | 5 | 1 | 2 | 9 | 1 | 2 2<sup>291</sup> - 19 | 5 | 1 | 2 | 10 | 1 | 2 2<sup>321</sup> - 9 | 6 | 1 | 2 | 11 | 1 | 2 2<sup>336</sup> - 17 | 6 | 1 | 2 | 11 | 1 | 2 2<sup>336</sup> - 3 | 6 | 1 | 2 | 11 | 1 | 2 2<sup>338</sup> - 15 | 6 | 1 | 2 | 11 | 1 | 2 2<sup>369</sup> - 25 | 6 | 1 | 2 | 12 | 1 | 2 2<sup>379</sup> - 19 | 6 | 1 | 2 | 12 | 1 | 2 2<sup>382</sup> - 105 | 6 | 1 | 2 | 12 | 1 | 2 2<sup>383</sup> - 421 | 6 | 1 | 2 | 12 | 1 | 2 2<sup>383</sup> - 187 | 6 | 1 | 2 | 12 | 1 | 2 2<sup>383</sup> - 31 | 6 | 1 | 2 | 12 | 1 | 2 2<sup>384</sup> - 317 | 6 | 1 | 2 | 12 | 1 | 2 2<sup>389</sup> - 21 | 7 | 1 | 2 | 13 | 1 | 2 2<sup>401</sup> - 31 | 7 | 1 | 2 | 13 | 1 | 2 2<sup>413</sup> - 21 | 7 | 1 | 2 | 13 | 1 | 2 2<sup>414</sup> - 17 | 7 | 1 | 2 | 13 | 1 | 2 2<sup>444</sup> - 17 | 7 | 1 | 2 | 14 | 1 | 2 2<sup>452</sup> - 3 | 8 | 1 | 2 | 15 | 1 | 2 2<sup>468</sup> - 17 | 8 | 1 | 2 | 15 | 1 | 2 2<sup>488</sup> - 17 | 8 | 1 | 2 | 16 | 1 | 2 2<sup>489</sup> - 21 | 8 | 1 | 2 | 16 | 1 | 2 2<sup>495</sup> - 31 | 8 | 1 | 2 | 16 | 1 | 2 2<sup>511</sup> - 481 | 8 | 1 | 2 | 16 | 1 | 2 2<sup>511</sup> - 187 | 8 | 1 | 2 | 16 | 1 | 2 2<sup>512</sup> - 569 | 8 | 1 | 2 | 16 | 1 | 2 2<sup>521</sup> - 1 | 9 | 1 | 2 | 17 | 1 | 2 2<sup>192</sup> - 2<sup>64</sup> - 1 | 3 | 2 | 3 | 6 | 2 | 2 2<sup>216</sup> - 2<sup>108</sup> - 1 | 4 | 2 | 2 | 7 | 2 | 3 2<sup>322</sup> - 2<sup>161</sup> - 1 | 6 | 2 | 2 | 11 | 2 | 3 2<sup>416</sup> - 2<sup>208</sup> - 1 | 7 | 2 | 3 | 13 | 2 | 3 2<sup>448</sup> - 2<sup>224</sup> - 1 | 7 | 2 | 3 | 14 | 2 | 3 2<sup>450</sup> - 2<sup>225</sup> - 1 | 8 | 2 | 2 | 15 | 2 | 3 2<sup>480</sup> - 2<sup>240</sup> - 1 | 8 | 2 | 2 | 15 | 2 | 3 2<sup>205</sup> - 45×2<sup>198</sup> - 1 | 4 | 4 | 4 | 7 | 7 | 7 2<sup>224</sup> - 2<sup>96</sup> + 1 | 4 | 2 | 2 | 7 | 2 | 3 2<sup>256</sup> - 2<sup>224</sup> + 2<sup>192</sup> + 2<sup>96</sup> - 1 | 4 | 4 | 4 | 8 | 8 | 8 2<sup>256</sup> - 2<sup>32</sup> - 977 | 4 | 1 | 2 | 8 | 2 | 2 2<sup>256</sup> - 4294968273 | 4 | 1 | 2 | 8 | 1 | 2 2<sup>384</sup> - 2<sup>128</sup> - 2<sup>96</sup> + 2<sup>32</sup> - 1 | 6 | 2 | 2 | 12 | 2 | 2 2<sup>256</sup> - 88×2<sup>240</sup> - 1 | 4 | 4 | 4 | 8 | 8 | 8 2<sup>254</sup> - 127×2<sup>240</sup> - 1 | 4 | 4 | 4 | 8 | 8 | 8 2<sup>384</sup> - 79×2<sup>376</sup> - 1 | 6 | 6 | 6 | 12 | 12 | 12 2<sup>384</sup> - 5×2<sup>368</sup> - 1 | 6 | 6 | 6 | 12 | 12 | 12 2<sup>512</sup> - 491×2<sup>496</sup> - 1 | 8 | 8 | 8 | 16 | 16 | 16 2<sup>510</sup> - 290×2<sup>496</sup> - 1 | 8 | 8 | 8 | 16 | 16 | 16 13 May 2020, 22:29:22 UTC
3805ad7 Jason Gross 13 May 2020, 00:18:24 UTC Parenthesize bitwise operators in printing PHOASTs Even though we are nominally printing Gallina identifiers here, we parenthesize bitwise operators much more frequently. See, e.g., https://github.com/mit-plv/fiat-crypto/pull/792#issuecomment-627647069, where Andres makes the point that in C, `+` binds more tightly than `<<`. 13 May 2020, 16:49:47 UTC
8e9e5ec Jason Gross 12 May 2020, 20:57:06 UTC Display definitions for `eval` and `bytes_eval` Closes #791 This should resolve the question of endianess of encoding. 13 May 2020, 16:49:47 UTC
back to top