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
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
ff3e418 Jason Gross 13 May 2020, 00:41:43 UTC Bump coqprime for compat with Coq master 13 May 2020, 00:41:43 UTC
1d21d0c Jason Gross 12 May 2020, 23:39:26 UTC Strip trailing spaces at the end of lines 12 May 2020, 23:39:26 UTC
c8cc226 jadep 11 May 2020, 16:40:43 UTC regenerate bedrock2 files 12 May 2020, 09:17:58 UTC
68bd18a jadep 11 May 2020, 14:15:00 UTC modify Stringification.v to use input/output access sizes when calling bedrock2 translation 12 May 2020, 09:17:58 UTC
4d3eb85 jadep 11 May 2020, 14:13:42 UTC add requirement that width is a multiple of 8 12 May 2020, 09:17:58 UTC
7b301a0 jadep 05 May 2020, 17:08:05 UTC update other test proofs 12 May 2020, 09:17:58 UTC
3641969 jadep 05 May 2020, 16:41:00 UTC fix proofs in X25519_64 test to work with bounds 12 May 2020, 09:17:58 UTC
935e298 jadep 05 May 2020, 12:03:42 UTC update remainder of tests 12 May 2020, 09:17:58 UTC
5025d01 jadep 05 May 2020, 11:48:06 UTC proofs all use equivalence-with-access-size now; 64-bit test updated 12 May 2020, 09:17:58 UTC
7a65df6 jadep 05 May 2020, 11:29:53 UTC WIP: make proofs through LoadStoreList compatible with equivalence in terms of access sizes 12 May 2020, 09:17:58 UTC
8e60515 jadep 01 May 2020, 13:56:06 UTC WIP: equivalence in terms of sizes for in-memory lists 12 May 2020, 09:17:58 UTC
cb3f606 jadep 01 May 2020, 13:55:55 UTC WIP: equivalence in terms of sizes for in-memory lists 12 May 2020, 09:17:58 UTC
b5994fe jadep 01 May 2020, 01:29:01 UTC WIP: make translation take list access sizes 12 May 2020, 09:17:58 UTC
bb3f387 jadep 30 April 2020, 14:45:11 UTC add from_bytes to X25519_64 test 12 May 2020, 09:17:58 UTC
51abc74 Jason Gross 11 May 2020, 05:42:00 UTC Bump rust crate version for new version of code 11 May 2020, 05:42:00 UTC
1776b15 Jason Gross 09 May 2020, 21:46:36 UTC Use Rust docstring comments Addresses part of #785 11 May 2020, 04:54:28 UTC
065f5a2 Jason Gross 09 May 2020, 21:29:55 UTC Add to_montgomery Closes #784, partial work on #785 10 May 2020, 03:24:25 UTC
62978b9 Jason Gross 07 May 2020, 19:26:35 UTC Fix a bug in SPSE 07 May 2020, 19:26:35 UTC
224e8e2 Jason Gross 06 May 2020, 20:07:01 UTC Do more rewriting before emitting bounds-don't-match errors 06 May 2020, 20:07:01 UTC
ed8e316 Jason Gross 06 May 2020, 19:22:38 UTC More informative error messages 06 May 2020, 19:22:38 UTC
bee423c Jason Gross 06 May 2020, 18:52:47 UTC Better error message pretty-printing Previously we'd get claims that the input to bounds analysis was unprintable as C, because some literals were annotated with casts. This change makes annotating a literal with a cast valid in more locations, as long as the literal fits inside the cast bounds. 06 May 2020, 18:52:47 UTC
d6acb3c Jason Gross 06 May 2020, 04:45:06 UTC Work around coq/coq#12258 06 May 2020, 18:08:09 UTC
87f6a00 Jason Gross 06 May 2020, 01:44:07 UTC Add support for comments and stripping annotations After `Import Crypto.Language.PreExtra`, it's now possible to do `dlet _ := ident.comment stuff in ...` and have `stuff` appear in the synthesized code as a comment. There's room for improvement with regards to quoting and handling multi-line comments, but it works for debugging purposes. Note that bounds analysis does not add casts underneath comments, though I believe let-lifting still happens, and the comments are still definitely subject to rewriting. If you want comments whose variable dependencies are eliminated during the very last dead-code-elimination phase of the stringification pipeline, use `ident.comment_no_keep`. Both `ident.comment` and `ident.comment_no_keep` have type `forall {A}, A -> unit`. There are now also passes `StripAnnotations` and `StripAllAnnotations`; the former takes an expression and input bounds, and strips cast annotations which are guaranteed to be no-ops given the bounds; it's proven to preserve `Wf` and `Interp`-relatedness. The `StripAllAnnotations` pass strips *all* cast annotations, even the ones that might be doing necessary truncation or modulo computations, and does not require input bounds. It's proven to preserve `Wf` but has no `Interp` proofs. 06 May 2020, 18:08:09 UTC
e8755ef Hugo Herbelin 04 May 2020, 23:08:34 UTC Adapt to subst now inactive on section variables with indirect dependency in goal. The fix is a priori backward-compatible. 05 May 2020, 16:41:21 UTC
45a64c9 Jason Gross 05 May 2020, 05:06:12 UTC Add lemma missing from Coq 8.9 05 May 2020, 05:06:12 UTC
fdc6aa2 Jason Gross 05 May 2020, 03:17:27 UTC Bump rewriter 05 May 2020, 03:17:27 UTC
4e54578 Jason Gross 05 May 2020, 03:12:00 UTC Fix previous commit 05 May 2020, 03:12:00 UTC
24ee597 Jason Gross 05 May 2020, 03:10:29 UTC Bump rewriter 05 May 2020, 03:10:29 UTC
2de5f15 Jason Gross 05 May 2020, 02:59:51 UTC Bump rewriter 05 May 2020, 03:00:03 UTC
0e577cb Jason Gross 04 May 2020, 23:33:05 UTC Factor out prepare_use_curve_good It should speed things up a bit <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) -------------------------------------------------------------------------------------------------------------------------------------------------------- 8m16.33s | 1816868 ko | Total Time / Peak Mem | 8m29.27s | 1821124 ko || -0m12.93s || -4256 ko | -2.54% | -0.23% -------------------------------------------------------------------------------------------------------------------------------------------------------- 0m41.66s | 937180 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m52.86s | 942172 ko || -0m11.20s || -4992 ko | -21.18% | -0.52% 2m23.94s | 1812196 ko | Fancy/Barrett256.vo | 2m25.27s | 1812196 ko || -0m01.33s || 0 ko | -0.91% | +0.00% 1m25.50s | 1816868 ko | Fancy/Montgomery256.vo | 1m25.74s | 1821124 ko || -0m00.23s || -4256 ko | -0.27% | -0.23% 1m24.40s | 1356144 ko | SlowPrimeSynthesisExamples.vo | 1m23.66s | 1355988 ko || +0m00.74s || 156 ko | +0.88% | +0.01% 0m35.48s | 915844 ko | Bedrock/Tests/Proofs/X25519_32.vo | 0m35.68s | 915840 ko || -0m00.20s || 4 ko | -0.56% | +0.00% 0m22.23s | 1030916 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m22.25s | 1028224 ko || -0m00.01s || 2692 ko | -0.08% | +0.26% 0m18.04s | 795300 ko | Bedrock/Tests/Proofs/X25519_64.vo | 0m18.17s | 795504 ko || -0m00.13s || -204 ko | -0.71% | -0.02% 0m13.71s | 915780 ko | Bedrock/Tests/X25519_32.vo | 0m13.58s | 915396 ko || +0m00.13s || 384 ko | +0.95% | +0.04% 0m08.76s | 769292 ko | Bedrock/Tests/Proofs/X1305_32.vo | 0m08.81s | 769228 ko || -0m00.05s || 64 ko | -0.56% | +0.00% 0m06.24s | 863912 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.34s | 863852 ko || -0m00.09s || 60 ko | -1.57% | +0.00% 0m05.67s | 854912 ko | PushButtonSynthesis/BaseConversion.vo | 0m05.69s | 854872 ko || -0m00.02s || 40 ko | -0.35% | +0.00% 0m04.99s | 785432 ko | Bedrock/Tests/X25519_64.vo | 0m05.03s | 785444 ko || -0m00.04s || -12 ko | -0.79% | -0.00% 0m04.53s | 788144 ko | Bedrock/Tests/X1305_32.vo | 0m04.55s | 788240 ko || -0m00.01s || -96 ko | -0.43% | -0.01% 0m03.49s | 850400 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.50s | 850444 ko || -0m00.00s || -44 ko | -0.28% | -0.00% 0m03.36s | 838884 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.41s | 839760 ko || -0m00.05s || -876 ko | -1.46% | -0.10% 0m02.54s | 722672 ko | CLI.vo | 0m02.57s | 722848 ko || -0m00.02s || -176 ko | -1.16% | -0.02% 0m02.21s | 736724 ko | Rewriter/PerfTesting/Core.vo | 0m02.40s | 737004 ko || -0m00.18s || -280 ko | -7.91% | -0.03% 0m02.00s | 762760 ko | Bedrock/StandaloneHaskellMain.vo | 0m02.03s | 763100 ko || -0m00.02s || -340 ko | -1.47% | -0.04% 0m01.99s | 756156 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.01s | 755988 ko || -0m00.01s || 168 ko | -0.99% | +0.02% 0m01.92s | 762464 ko | Bedrock/StandaloneOCamlMain.vo | 0m01.87s | 763000 ko || +0m00.04s || -536 ko | +2.67% | -0.07% 0m01.87s | 742608 ko | StandaloneOCamlMain.vo | 0m01.93s | 743016 ko || -0m00.05s || -408 ko | -3.10% | -0.05% 0m01.81s | 742564 ko | StandaloneHaskellMain.vo | 0m01.93s | 742312 ko || -0m00.11s || 252 ko | -6.21% | +0.03% ``` </p> 05 May 2020, 00:16:46 UTC
1cf7064 Jason Gross 04 May 2020, 23:40:38 UTC Fix a name qualification issue 04 May 2020, 23:40:38 UTC
8ef6554 Jason Gross 04 May 2020, 23:25:42 UTC Split off ZRange part of abs int for finer grained dependencies 04 May 2020, 23:25:42 UTC
f0f2849 Jason Gross 04 May 2020, 22:56:56 UTC Bump rewriter 04 May 2020, 22:56:56 UTC
12fd2df Jason Gross 04 May 2020, 18:24:58 UTC Add reflect instances for string and ascii 04 May 2020, 18:24:58 UTC
6dbb93a Jason Gross 04 May 2020, 18:21:50 UTC Combine the show_application nodes This should make it easier to extend simple identifiers in the future 04 May 2020, 18:21:50 UTC
3f58bfa Jason Gross 02 May 2020, 17:08:43 UTC Add an inlined version of sat mul 02 May 2020, 17:08:43 UTC
a510d07 Jason Gross 02 May 2020, 16:50:10 UTC Add an example of computing unsat solinas For https://github.com/mit-plv/fiat-crypto/issues/776#issuecomment-622970195 02 May 2020, 16:50:10 UTC
d5b3894 Jason Gross 02 May 2020, 16:49:31 UTC Add more Show instances Useful for debugging pipelines 02 May 2020, 16:49:31 UTC
f423db3 Adam Chlipala 01 May 2020, 12:26:55 UTC Proofreading README 01 May 2020, 12:26:55 UTC
557c5b4 Jason Gross 30 April 2020, 04:08:28 UTC Update README.md Co-Authored-By: jadephilipoom <jade.philipoom@gmail.com> 01 May 2020, 03:10:48 UTC
5779d32 Jason Gross 30 April 2020, 01:45:36 UTC Apply suggestions from code review 01 May 2020, 03:10:48 UTC
9ee04cb Jason Gross 29 April 2020, 21:14:44 UTC Add bedrock2 instructions to README 01 May 2020, 03:10:48 UTC
81aefa3 jadep 30 April 2020, 16:15:51 UTC regenerate fiat-bedrock2 files (TODO on mulhuu was removed after testing, see mit-plv/bedrock2#155 30 April 2020, 22:18:29 UTC
1c209d2 jadep 30 April 2020, 16:14:29 UTC bump bedrock2 30 April 2020, 22:18:29 UTC
99792aa Jason Gross 29 April 2020, 21:51:19 UTC Hopefully emit Coq's version, not ours 29 April 2020, 21:51:19 UTC
ad5026f Jason Gross 21 April 2020, 23:21:21 UTC 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? 24 April 2020, 02:19:56 UTC
fd4738d jadep 21 April 2020, 15:12:05 UTC add zutil file for Z.ltz lemmas 22 April 2020, 21:23:02 UTC
33564a3 jadep 21 April 2020, 14:29:47 UTC add 32-bit poly1305 test for bedrock2 22 April 2020, 20:03:55 UTC
f3a74f9 jadep 22 April 2020, 16:04:08 UTC add support for opp in bedrock2 backend 22 April 2020, 16:04:08 UTC
d8d588f jadep 22 April 2020, 03:14:14 UTC remove upload-timing-info stage from GH actions 22 April 2020, 13:57:45 UTC
9c7958e jadephilipoom 21 April 2020, 06:01:25 UTC remove unnecessary parens Co-Authored-By: Jason Gross <jgross@mit.edu> 21 April 2020, 23:19:58 UTC
f4c144f jadep 21 April 2020, 04:24:06 UTC add no_select_size_opt instance to SlowPrimeSynthesisExamples 21 April 2020, 23:19:58 UTC
9e57208 jadep 21 April 2020, 02:27:06 UTC support new zselect patterns in bedrock2 backend 21 April 2020, 23:19:58 UTC
9b16394 jadep 20 April 2020, 16:31:45 UTC add rewrite rules to translate Z.zselect into non-cmov-requiring expression for bedrock2, and add CLI flag 21 April 2020, 23:19:58 UTC
bcedf4f jadep 21 April 2020, 06:14:35 UTC respond to Jason's review comments and do a little extra cleanup in test files 21 April 2020, 13:08:03 UTC
3a1cfb1 jadep 20 April 2020, 14:24:40 UTC instantiate correctness and wf proofs for 32-bit tests (following 64-bit model) 21 April 2020, 13:08:03 UTC
1cb33d7 jadep 20 April 2020, 14:17:52 UTC prove Wf3 for 64-bit test case using Jason's new tactic 21 April 2020, 13:08:03 UTC
61310cb jadep 20 April 2020, 13:44:47 UTC instantiate correctness proof for 64-bit test 21 April 2020, 13:08:03 UTC
7485bc6 Jason Gross 20 April 2020, 18:46:16 UTC Add poly1305 This was somewhat more annoying than it had to be; I'd like to come up with a more compact format for specifying the primes that we're building by default. ``` Time | Peak Mem | File Name ----------------------------------------------------- 0m02.46s | 20076 ko | Total Time / Peak Mem ----------------------------------------------------- 0m00.34s | 17136 ko | fiat-c/src/poly1305_32.c 0m00.34s | 17552 ko | fiat-rust/src/poly1305_32.rs 0m00.33s | 17152 ko | fiat-java/src/FiatPoly1305.java 0m00.31s | 16884 ko | fiat-go/src/poly1305_32.go 0m00.29s | 17300 ko | fiat-go/src/poly1305_64.go 0m00.27s | 16680 ko | fiat-rust/src/poly1305_64.rs 0m00.26s | 16608 ko | fiat-c/src/poly1305_64.c 0m00.21s | 20076 ko | fiat-bedrock2/src/poly1305_32.c 0m00.12s | 17388 ko | fiat-bedrock2/src/poly1305_64.c ``` 20 April 2020, 22:44:31 UTC
000218d Jason Gross 19 April 2020, 23:11:52 UTC Remove useless tactic aliases generating a warning 19 April 2020, 23:11:52 UTC
b146757 Jason Gross 19 April 2020, 16:12:50 UTC Attempt to be compatible with https://github.com/coq/coq/pull/12073 19 April 2020, 16:12:50 UTC
ad49dd7 Jason Gross 16 April 2020, 21:38:31 UTC Add 32-bit bedrock2 builds Closes #751 19 April 2020, 15:41:42 UTC
c02f8b6 jadep 18 April 2020, 18:52:24 UTC use new upstream Z->string function and use it to prove an admit 19 April 2020, 03:14:06 UTC
2454952 jadep 18 April 2020, 16:49:07 UTC write most of mulmod_correct proof for 64-bit 19 April 2020, 03:14:06 UTC
5236855 jadep 18 April 2020, 14:54:58 UTC factor out common proofs for bedrock2 test cases 19 April 2020, 03:14:06 UTC
f4eeaeb jadep 17 April 2020, 21:59:19 UTC use passed-in machine wordsize instead of hacky temoporary solution 19 April 2020, 03:14:06 UTC
0743563 jadep 17 April 2020, 15:06:58 UTC make hacky temporary wordsize-inference work on looser bounds 19 April 2020, 03:14:06 UTC
8305de0 jadep 17 April 2020, 14:31:26 UTC indentation fixes (no code changes) 19 April 2020, 03:14:06 UTC
c19e801 jadep 17 April 2020, 14:30:44 UTC make Bedrock/Stringification.v generic over machine word size 19 April 2020, 03:14:06 UTC
4adcee9 jadep 17 April 2020, 13:34:33 UTC remove global from instance declarations that are specific to a machine word size 19 April 2020, 03:14:06 UTC
b1969e4 jadep 17 April 2020, 13:32:43 UTC add 32-bit test case 19 April 2020, 03:14:06 UTC
b0b4b0f jadep 16 April 2020, 21:09:22 UTC separate out common parts of Defaults.v, and then put machine-wordsize-dependent parts in two separate files for 32- and 64-bit 19 April 2020, 03:14:06 UTC
092b311 Hugo Herbelin 18 April 2020, 12:44:08 UTC Adapting to Coq PR #12023: atomic form of primitive tactics are in module Ltac. Previously, it was in Coq.Init.Notations. Now in Coq.Init.Ltac. The patch is backward compatible (but a bit less explicit about which etransitivity we are talking about). 18 April 2020, 19:51:58 UTC
692462f Jason Gross 18 April 2020, 14:41:27 UTC Bump rewriter for prove_Wf3 18 April 2020, 14:41:27 UTC
a854dea Jason Gross 18 April 2020, 00:18:16 UTC Remove string cruft that's been upstreamed Since we now no longer support Coq 8.8, we can rely on definitions in the standard library to print and parse strings. The upshot is that now we have many fewer lines of code, and we have a couple more proofs about the fact that `parse ∘ print` is the identity. 18 April 2020, 14:19:58 UTC
17e3c5b Jason Gross 17 April 2020, 15:35:28 UTC Deal with splitting 32x64 mul, not just 64x32 mul We previously only had a rule for the double-width multiplicand on the left; this commit adds a rewrite rule for having the double-width multiplicand on the right. This should allow synthesis of 32-bit carry_square for bedrock2. 17 April 2020, 20:42:16 UTC
ba2b479 Jason Gross 17 April 2020, 15:16:03 UTC Give stringification access to machine_wordsize This will make bedrock2 32-bit support significantly easier. Currently the CLI support is a bit messy, because I couldn't decide whether bitwidth was "owned" by the overall pipeline (in which case it probably shouldn't show up in the header, or should show up uniformly with all the other options in the header, like static and some rewriter options), or whether it's "owned" by individual synthesis pipelines (like m, s, and c) (which allows it to continue showing up as its own line in the header, as it currently does). Probably we should eventually choose the former, but because I haven't really thought out this design decision at this point, I currently preserve the way the output files are currently being generated and do this sort-of mixed support mode. 17 April 2020, 20:41:44 UTC
31c76f8 Jason Gross 16 April 2020, 22:36:05 UTC Add support for Z.lxor Currently bounds analysis only knows how to analyze Z.lxor applied to constants, but it still can be used in post-bounds-analysis rewrite rules. 17 April 2020, 15:57:42 UTC
0884b6d jadep 16 April 2020, 13:03:47 UTC fixes based on review comments from Jason 16 April 2020, 17:30:14 UTC
b392f5d jadep 16 April 2020, 01:33:49 UTC move helper lemmas to util files 16 April 2020, 17:30:14 UTC
5deda65 jadep 15 April 2020, 21:34:38 UTC add and prove rules for sub_get_borrow and sub_with_get_borrow 16 April 2020, 17:30:14 UTC
effaa95 jadep 15 April 2020, 17:27:57 UTC add and prove rule for add_with_get_carry 16 April 2020, 17:30:14 UTC
back to top