| 418eb6a | Jason Gross | 09 April 2021, 22:11:04 UTC | Infer the stack size from the code | 26 May 2021, 18:32:39 UTC |
| 41d5df5 | Jason Gross | 20 May 2021, 01:17:42 UTC | Regenerate files | 25 May 2021, 18:04:59 UTC |
| 2aa891b | Jason Gross | 19 May 2021, 14:26:25 UTC | Fix Zig casing | 25 May 2021, 18:04:59 UTC |
| 3302d83 | Jason Gross | 19 May 2021, 02:02:21 UTC | Improve Go code | 25 May 2021, 18:04:59 UTC |
| 468489d | Jason Gross | 18 May 2021, 20:38:23 UTC | Fix for Coq 8.9 | 25 May 2021, 18:04:59 UTC |
| d3638c4 | Jason Gross | 18 May 2021, 19:53:35 UTC | Add Zig typedefs | 25 May 2021, 18:04:59 UTC |
| 11af3c5 | Jason Gross | 18 May 2021, 15:52:20 UTC | Add synthesis of relax Now it makes sense, since we're using typedefs | 25 May 2021, 18:04:59 UTC |
| aafdb40 | Jason Gross | 14 May 2021, 00:21:04 UTC | Add named typedefs Questions: - [ ] Which divstep things belong in the montgomery domain? - [ ] What should we do about the various other kinds of bounds (saturated, bytes, etc)? - [x] Should we synthesize relax? (Current answer: Yes) - [ ] What should we do about selectznz? (should it take tight fe, loose fe, saturated fe; should we have a variant of saturated_relax that goes from loose to saturated?) | 25 May 2021, 18:04:59 UTC |
| 7602507 | Jason Gross | 19 May 2021, 19:02:48 UTC | Work around Coq Haskell Extraction issue https://github.com/coq/coq/issues/14256 | 20 May 2021, 17:34:46 UTC |
| fb05f2b | Jason Gross | 04 May 2021, 15:29:27 UTC | Switch to latest version of Haskell and Cabal Mainly to silence warnings/annotations. Also switch from an unmaintained action to a maintained one. | 20 May 2021, 17:34:46 UTC |
| 098fd23 | Jason Gross | 20 May 2021, 14:32:40 UTC | Add more rewrite_mod_small tactics | 20 May 2021, 14:32:40 UTC |
| 7086309 | Jason Gross | 20 May 2021, 13:25:28 UTC | Add some Wf facts from Fiat | 20 May 2021, 13:25:28 UTC |
| 431b450 | Jason Gross | 20 May 2021, 00:04:46 UTC | Fix a typo and improve doc comment | 20 May 2021, 00:48:37 UTC |
| c4237de | Jason Gross | 20 May 2021, 00:13:44 UTC | Remove trailing whitespace | 20 May 2021, 00:13:44 UTC |
| f555159 | Jason Gross | 19 May 2021, 02:09:59 UTC | Test that gofmt is a no-op on Go code | 19 May 2021, 12:32:59 UTC |
| 9525e9d | Jason Gross | 18 May 2021, 18:47:36 UTC | Bump coqprime | 19 May 2021, 01:47:52 UTC |
| 4a0b8d1 | Automated Publisher | 18 May 2021, 18:44:42 UTC | Automated Rust Crate Version Bump: Tue May 18 18:44:42 UTC 2021 2d76718a2be2b05e22c57c2c0dd6dadd72134f05 | 18 May 2021, 18:44:42 UTC |
| 2d76718 | Jason Gross | 17 May 2021, 22:48:10 UTC | Update fancy machine to use the new curve_good requests | 17 May 2021, 22:48:10 UTC |
| e7c20b5 | Jason Gross | 17 May 2021, 21:34:59 UTC | Add map_ranges utility functions | 17 May 2021, 21:34:59 UTC |
| 21fa689 | Jason Gross | 06 May 2021, 21:21:10 UTC | Make `prime_bytes_bounds` not an `option` This makes things more uniform | 17 May 2021, 21:33:39 UTC |
| 13ac664 | Jason Gross | 17 May 2021, 21:23:09 UTC | Fix a missing argument | 17 May 2021, 21:23:09 UTC |
| f028939 | Jason Gross | 17 May 2021, 14:08:43 UTC | Add tactics for getting all instances of a class | 17 May 2021, 14:08:43 UTC |
| d50398f | Jason Gross | 15 May 2021, 15:55:06 UTC | Bump rewriter | 15 May 2021, 15:55:06 UTC |
| f6f2278 | Jason Gross | 15 May 2021, 01:48:46 UTC | Compatibility with bumped rewriter This is in preparation for having typedefs based on bounds info. If this passes CI, then we can merge https://github.com/mit-plv/rewriter/pull/28. | 15 May 2021, 15:47:42 UTC |
| 32f9f0b | Jason Gross | 15 May 2021, 01:46:25 UTC | Bump rewriter | 15 May 2021, 15:47:42 UTC |
| afbc55a | Jason Gross | 15 May 2021, 01:43:40 UTC | Bump rewriter for compat with Coq master | 15 May 2021, 01:43:40 UTC |
| 4dd8dba | Jason Gross | 13 May 2021, 18:28:53 UTC | Remove useless require | 13 May 2021, 18:28:53 UTC |
| cfa7106 | Jason Gross | 13 May 2021, 17:30:01 UTC | Add list_beq_hetero lemmas | 13 May 2021, 17:30:01 UTC |
| 78fff68 | Jason Gross | 13 May 2021, 17:19:38 UTC | Rename forall2b into list_beq_hetero | 13 May 2021, 17:19:38 UTC |
| 31d4637 | Jason Gross | 13 May 2021, 17:17:48 UTC | Add some utility functions | 13 May 2021, 17:17:58 UTC |
| 7235aa9 | Jason Gross | 12 May 2021, 20:25:48 UTC | Include newlines in -h output Fixes #979 | 12 May 2021, 20:25:48 UTC |
| f4fa385 | Jason Gross | 12 May 2021, 14:02:45 UTC | Revert "TEMP DO NOT MERGE Remove other CI files Also test opam package on PR" This reverts commit aee63da68811951357adb8e3ee66e816fce0160b. | 12 May 2021, 17:08:17 UTC |
| 9be7e28 | Jason Gross | 12 May 2021, 14:06:27 UTC | Update coq-opam-package.yml Now that https://github.com/avsm/setup-ocaml/pull/77 has been merged | 12 May 2021, 17:08:17 UTC |
| 66f003a | Jason Gross | 11 May 2021, 15:39:59 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| ecc3e5c | Jason Gross | 11 May 2021, 14:32:59 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 0ca45b5 | Jason Gross | 11 May 2021, 01:27:05 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| a9b3a3a | Jason Gross | 11 May 2021, 01:24:35 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 5e99331 | Jason Gross | 10 May 2021, 16:31:02 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 0d8630c | Jason Gross | 10 May 2021, 13:53:09 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| f79425c | Jason Gross | 10 May 2021, 12:52:16 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 94c1d9c | Jason Gross | 07 May 2021, 22:30:00 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| ccdd066 | Jason Gross | 07 May 2021, 18:27:50 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| bc3847a | Jason Gross | 06 May 2021, 20:46:09 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 841ac8f | Jason Gross | 06 May 2021, 20:32:18 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 47ac106 | Jason Gross | 06 May 2021, 03:13:27 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 80622d5 | Jason Gross | 06 May 2021, 00:38:29 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| b6e86e0 | Jason Gross | 06 May 2021, 00:28:01 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 4cb4c51 | Jason Gross | 06 May 2021, 00:17:42 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 7c9daf2 | Jason Gross | 05 May 2021, 21:33:12 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 711adfc | Jason Gross | 05 May 2021, 21:32:27 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| b2b288f | Jason Gross | 05 May 2021, 18:54:47 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 225b6c7 | Jason Gross | 05 May 2021, 17:11:07 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 617b23e | Jason Gross | 05 May 2021, 16:13:55 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 50edef8 | Jason Gross | 04 May 2021, 20:10:12 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| c080a0a | Jason Gross | 04 May 2021, 15:03:14 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 4195a8e | Jason Gross | 04 May 2021, 15:02:37 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 10fb11a | Jason Gross | 06 May 2021, 20:40:34 UTC | TEMP DO NOT MERGE Remove other CI files Also test opam package on PR | 12 May 2021, 17:08:17 UTC |
| b960bfb | Jason Gross | 03 May 2021, 15:25:39 UTC | Add a CI test of our opam package | 12 May 2021, 17:08:17 UTC |
| 13b506a | Frank Denis | 09 May 2021, 13:57:19 UTC | Update Zig tests after std.testing.* changes A breaking change was just introduced in the Zig testing framework. This updates the Zig tests for it. | 11 May 2021, 14:27:39 UTC |
| 5e9d9a2 | Jason Gross | 03 May 2021, 20:26:49 UTC | Allow check_args to discriminate on requested ops Fixes #962 Now we can potentially implement different versions of `to_bytes` with different requirements, as per https://github.com/mit-plv/fiat-crypto/issues/960#issuecomment-830662847 | 10 May 2021, 19:56:31 UTC |
| e12be1d | Jason Gross | 07 May 2021, 22:07:17 UTC | Revert "TEMP DO NOT MERGE Remove other files" This reverts commit 794fb277cace5657baae7ae83f4c3e46e63d3a93. | 07 May 2021, 22:07:27 UTC |
| 1bdcbca | Jason Gross | 07 May 2021, 18:14:43 UTC | Update coq-windows.yml | 07 May 2021, 22:07:27 UTC |
| 3e2aa6b | Jason Gross | 07 May 2021, 02:23:24 UTC | Update coq-windows.yml | 07 May 2021, 22:07:27 UTC |
| 3c7ba03 | Jason Gross | 07 May 2021, 02:14:39 UTC | Update coq-windows.yml | 07 May 2021, 22:07:27 UTC |
| 6785434 | Jason Gross | 06 May 2021, 20:50:09 UTC | Update coq-windows.yml | 07 May 2021, 22:07:27 UTC |
| 4dc3227 | Jason Gross | 06 May 2021, 20:47:17 UTC | TEMP DO NOT MERGE Remove other files | 07 May 2021, 22:07:27 UTC |
| 17f0ce3 | Jason Gross | 06 May 2021, 20:39:23 UTC | Update coq-windows.yml | 07 May 2021, 22:07:27 UTC |
| f6a249b | Jason Gross | 06 May 2021, 20:36:54 UTC | Update coq-windows.yml | 07 May 2021, 22:07:27 UTC |
| 81bdcab | Jason Gross | 06 May 2021, 03:08:55 UTC | Update coq-windows.yml | 07 May 2021, 22:07:27 UTC |
| 8115787 | Jason Gross | 06 May 2021, 00:25:26 UTC | Update coq-windows.yml | 07 May 2021, 22:07:27 UTC |
| 8504bc1 | Jason Gross | 05 May 2021, 21:35:36 UTC | Update coq-windows.yml | 07 May 2021, 22:07:27 UTC |
| 4ad1406 | Jason Gross | 05 May 2021, 18:48:13 UTC | Update coq-windows.yml | 07 May 2021, 22:07:27 UTC |
| 224b8eb | Jason Gross | 04 May 2021, 21:14:46 UTC | Update coq-windows.yml | 07 May 2021, 22:07:27 UTC |
| 4d14264 | Jason Gross | 04 May 2021, 16:59:26 UTC | Update coq-windows.yml | 07 May 2021, 22:07:27 UTC |
| 33c95c3 | Jason Gross | 03 May 2021, 19:33:12 UTC | Update coq-windows.yml | 07 May 2021, 22:07:27 UTC |
| d46f9be | Jason Gross | 03 May 2021, 12:29:39 UTC | Use setup-ocaml for Windows CI | 07 May 2021, 22:07:27 UTC |
| 70daaef | jadep | 06 May 2021, 21:42:20 UTC | fix imports after move | 07 May 2021, 07:07:23 UTC |
| 9a0a053 | jadep | 06 May 2021, 21:31:58 UTC | move bedrock2 new-pipeline files | 07 May 2021, 07:07:23 UTC |
| c3cea10 | jadep | 06 May 2021, 21:30:12 UTC | address code review comments | 07 May 2021, 07:07:23 UTC |
| e7f6be2 | Jason Gross | 30 April 2021, 16:37:27 UTC | Rip out `Wf3` from new bedrock2 pipeline We no longer need to compute `Wf` at the output, and can instead prove it once and for all. | 07 May 2021, 07:07:23 UTC |
| 5ef134b | jadep | 27 April 2021, 09:58:43 UTC | update scalarmult proof to match new from_bytes precondition | 07 May 2021, 07:07:23 UTC |
| 712a608 | jadep | 27 April 2021, 08:46:20 UTC | update _CoqProject, remove outdated comment | 07 May 2021, 07:07:23 UTC |
| 425d6b7 | jadep | 21 February 2021, 20:18:56 UTC | factor out computed_op | 07 May 2021, 07:07:23 UTC |
| 3c73d42 | jadep | 21 February 2021, 20:10:13 UTC | all unsat solinas operations | 07 May 2021, 07:07:23 UTC |
| 4a7a287 | jadep | 21 February 2021, 18:08:36 UTC | to_bytes | 07 May 2021, 07:07:23 UTC |
| 99fb34d | jadep | 15 February 2021, 20:53:28 UTC | to_bytes wip | 07 May 2021, 07:07:23 UTC |
| 619a5b8 | jadep | 14 February 2021, 15:57:30 UTC | full prototype of from_bytes | 07 May 2021, 07:07:23 UTC |
| 749ff4e | jadep | 30 January 2021, 15:40:16 UTC | fixed from_bytes proof | 07 May 2021, 07:07:23 UTC |
| 39e038c | jadep | 02 January 2021, 21:28:42 UTC | WIP | 07 May 2021, 07:07:23 UTC |
| e96d6dc | jadep | 02 January 2021, 19:20:38 UTC | WIP: prototype of generic synthesis infrastructure | 07 May 2021, 07:07:23 UTC |
| a9c0a1d | jadep | 11 October 2020, 15:31:50 UTC | WIP comment | 07 May 2021, 07:07:23 UTC |
| 76a623e | jadep | 11 October 2020, 14:50:51 UTC | proofs of bedrock2-translated functions by signature for list-based binary opreations (list Z -> list Z -> list Z) and list-based unary operations (list Z -> list Z) | 07 May 2021, 07:07:23 UTC |
| 4abb766 | Jason Gross | 06 May 2021, 20:19:34 UTC | Fix -native-compiler ondemand logic Previously we were always setting native-compiler ondemand, even when it wasn't supported (I have no idea how the 8.9 build was succeeding, but it breaks on opam, maybe because then we're not in git?). Now we handle older versions of Coq correctly. | 06 May 2021, 20:19:36 UTC |
| 95ed951 | Jason Gross | 06 May 2021, 19:28:17 UTC | When `-h` or `--help` is passed, exit with 0 We now also print the usage to stdout rather than stderr, when requested by the user, following the majority at https://stackoverflow.com/a/2199698/377022 | 06 May 2021, 19:28:17 UTC |
| c076f35 | Jason Gross | 04 May 2021, 14:30:22 UTC | Add more paren wrappers | 04 May 2021, 21:07:32 UTC |
| 91c7792 | Jason Gross | 04 May 2021, 13:36:36 UTC | Add lookup_lvl, lookup_assoc | 04 May 2021, 21:07:32 UTC |
| 11832a4 | Jason Gross | 03 May 2021, 20:51:03 UTC | Work around extraction issues | 04 May 2021, 21:06:47 UTC |
| c86d782 | Jason Gross | 01 May 2021, 01:48:37 UTC | Add `ShowLevel`, rip out `with_parens` from `Show` Now `show` and `show_lines` no longer take a `with_parens` argument, and instead that functionality is generalized into `ShowLevel` / `show_lvl`. This is the first step towards having more flexibility in parenthesizing printed expressions, in a more principled way. It's sort-of a test-drive of a more uniform way of level-based printing. | 04 May 2021, 21:06:47 UTC |
| 56032cd | Jason Gross | 03 May 2021, 20:51:03 UTC | Work around extraction issues | 04 May 2021, 21:06:47 UTC |
| c456e07 | Jason Gross | 28 April 2021, 22:06:52 UTC | Implement some cosmetic Go changes Part of #949 Indent Go code and adjust spacing Minor spacing changes Add `--doc-newline-before-package-declaration` Now we have package docs back for Go code, when we want them. Add `--doc-prepend-header{,-raw}`, use `--doc-text-before-function-name` Fixes #958 | 04 May 2021, 20:59:40 UTC |
