| 16dd2bb | Samuel Gruetter | 05 December 2020, 07:38:20 UTC | bump rupicola/bedrock2 and adapt to expr.inlinetable feature | 05 December 2020, 07:38:20 UTC |
| 4f56d30 | Jason Gross | 24 November 2020, 19:21:48 UTC | Bump rewriter | 24 November 2020, 19:21:48 UTC |
| ed18175 | Jason Gross | 24 November 2020, 19:19:06 UTC | Update c.yml Fix for https://github.blog/changelog/2020-10-01-github-actions-deprecating-set-env-and-add-path-commands/ | 24 November 2020, 19:19:06 UTC |
| 8ff9736 | Jason Gross | 24 November 2020, 19:17:46 UTC | Update go.yml Fix for https://github.blog/changelog/2020-10-01-github-actions-deprecating-set-env-and-add-path-commands/ | 24 November 2020, 19:17:46 UTC |
| 5a18e11 | Jason Gross | 09 November 2020, 01:01:06 UTC | Fix cast argument for lnot_modulo | 13 November 2020, 21:47:01 UTC |
| f580889 | Jason Gross | 12 November 2020, 01:03:29 UTC | Add unthunk_bool rewrite db | 12 November 2020, 01:03:29 UTC |
| 2b2420f | Jason Gross | 12 November 2020, 00:56:14 UTC | Fix for 8.9 | 12 November 2020, 00:56:14 UTC |
| 858f121 | Jason Gross | 12 November 2020, 00:09:10 UTC | Use thunked definitions for bool that actually delay computation correctly | 12 November 2020, 00:09:10 UTC |
| 01cb061 | Jason Gross | 11 November 2020, 23:19:05 UTC | Massive dependency shortcut in Bedrock | 11 November 2020, 23:19:05 UTC |
| b8fb061 | Jason Gross | 11 November 2020, 23:08:00 UTC | More thunked bool | 11 November 2020, 23:08:00 UTC |
| 5694f4b | Jason Gross | 11 November 2020, 22:53:02 UTC | Add some thunked boolean operations | 11 November 2020, 22:53:02 UTC |
| 0592f00 | jadep | 08 November 2020, 22:42:52 UTC | add lnot_modulo to valid_expr_bool | 09 November 2020, 04:50:06 UTC |
| c569afb | Jason Gross | 08 November 2020, 00:04:09 UTC | Partial work on adding lnot_modulo support For #888 I still haven't updated the computable version of valid | 09 November 2020, 04:50:06 UTC |
| 4be7fee | Jason Gross | 09 November 2020, 00:33:35 UTC | Add induction_fold_left_orb_true | 09 November 2020, 00:33:35 UTC |
| f1e539d | Jason Gross | 08 November 2020, 19:16:17 UTC | Add a FoldBool lemma | 08 November 2020, 19:16:23 UTC |
| 12a0ada | Jason Gross | 06 November 2020, 01:17:41 UTC | A hopefully more readable translate_cmd | 08 November 2020, 04:58:13 UTC |
| 9aef716 | Jason Gross | 05 November 2020, 00:47:04 UTC | Make translate_cmd handle pairs This allows things like `fun (x y : Z) => (x, y)` and `fun (x y : Z) (z : list Z) => (x, y, z)` to synthesize correctly. This is partial work towards #886 and making bedrock2 output handle divstep. | 08 November 2020, 04:58:13 UTC |
| 683ddc2 | Jason Gross | 05 November 2020, 17:42:19 UTC | Revert "Fix some bedrock2 synthesis" This reverts commit eeec762f7b32283ce977d422c2e94b1fa6a79a1e. | 08 November 2020, 04:58:13 UTC |
| a890d97 | Jason Gross | 04 November 2020, 21:10:33 UTC | Fix some bedrock2 synthesis We now correctly synthesize on `(fun (x1 x2 : Z) => (x1, x2))`, by handling pairs without casts in front correctly. | 08 November 2020, 04:58:13 UTC |
| 1879a34 | Jason Gross | 07 November 2020, 23:28:10 UTC | Fix for Coq 8.11 and earlier | 08 November 2020, 03:28:14 UTC |
| 9c939fa | Jason Gross | 08 November 2020, 01:06:13 UTC | Add is_None, is_nil, and some reflect instances | 08 November 2020, 01:06:13 UTC |
| b44f239 | Jason Gross | 08 November 2020, 00:03:16 UTC | Add Ztestbit and lnot_modulo lemmas/hints | 08 November 2020, 00:03:16 UTC |
| 1c38b6c | Jason Gross | 07 November 2020, 23:30:40 UTC | Bump rewriter for _CoqProject.in update | 07 November 2020, 23:30:40 UTC |
| 780cd7b | Jason Gross | 07 November 2020, 23:29:30 UTC | Fix not-truly-recursive fixpoints warning, and make it an error with +non-recursive | 07 November 2020, 23:29:30 UTC |
| c3cc28a | Jason Gross | 06 November 2020, 01:12:32 UTC | Bump rewriter for a more convenient type.domain | 06 November 2020, 01:12:32 UTC |
| 10baf7e | Jason Gross | 05 November 2020, 00:48:31 UTC | Bump rewriter | 05 November 2020, 00:48:42 UTC |
| 6c87758 | Jason Gross | 04 November 2020, 21:43:01 UTC | Suppress 'Not a truly recursive fixpoint.' warning | 04 November 2020, 21:43:01 UTC |
| 24f51e8 | Jason Gross | 04 November 2020, 20:36:38 UTC | Suppress 'Not a truly recursive fixpoint.' warning | 04 November 2020, 20:36:38 UTC |
| d079d8a | Jason Gross | 02 November 2020, 02:30:01 UTC | Bump rewriter | 02 November 2020, 02:30:01 UTC |
| b363810 | Jason Gross | 02 November 2020, 00:38:30 UTC | echo on Mac has no -n; thread_siblings_list doesn't exist | 02 November 2020, 00:38:30 UTC |
| 92d99d0 | Jason Gross | 01 November 2020, 23:36:11 UTC | TEMP disable error redirection so we can see error messages on Mac | 01 November 2020, 23:36:11 UTC |
| cb45939 | Jason Gross | 01 November 2020, 23:33:59 UTC | TEMP disable error redirection so we can see error messages on Windows | 01 November 2020, 23:33:59 UTC |
| ffa0c05 | Jason Gross | 01 November 2020, 22:22:39 UTC | Update .gitignore | 01 November 2020, 22:22:39 UTC |
| 5436eb7 | Jason Gross | 01 November 2020, 22:21:44 UTC | Move back to f? parser notation We can do this with the resolution of https://github.com/coq/coq/issues/13281 by putting the notation at a higher level. | 01 November 2020, 22:21:44 UTC |
| 30d0e16 | Jason Gross | 29 October 2020, 03:00:36 UTC | Improve parsing Mostly so that we don't get out of sync with the rewriter | 29 October 2020, 03:00:36 UTC |
| 84eba63 | Benjamin Salling Hvass | 15 October 2020, 13:39:36 UTC | changed divstep to use Z.add_carry instead of Z.add to avoid using uint128 where unnecessary (fixes generated go-files) | 27 October 2020, 15:27:07 UTC |
| e192cb4 | Benjamin Salling Hvass | 15 October 2020, 10:30:26 UTC | added inversion templates | 27 October 2020, 15:27:07 UTC |
| a19f129 | Benjamin Salling Hvass | 15 October 2020, 10:26:26 UTC | disabled by-inversion for bedrock2 synthesis | 27 October 2020, 15:27:07 UTC |
| 458de59 | Benjamin Salling Hvass | 30 September 2020, 08:14:45 UTC | regenerated files | 27 October 2020, 15:27:07 UTC |
| a1bdae4 | Benjamin Salling Hvass | 30 September 2020, 07:37:42 UTC | fixed conflict with boringSSL and added comment on definitino of 2s-complement | 27 October 2020, 15:27:07 UTC |
| 3faa0f6 | Benjamin Salling Hvass | 30 September 2020, 07:29:26 UTC | recgenerated go, java, json and rust | 27 October 2020, 15:27:07 UTC |
| 13032b1 | Benjamin Salling Hvass | 07 September 2020, 12:25:59 UTC | refactored and added inversion for more primes (also linked inversion-c/ to fiat-c/src/) | 27 October 2020, 15:27:07 UTC |
| 3164d04 | Benjamin Salling Hvass | 23 August 2020, 23:58:35 UTC | renamed and removed synthesis of precomp (now it just uses the synthesis of encodemod) | 27 October 2020, 15:27:07 UTC |
| f3d91cd | Benjamin Salling Hvass | 07 August 2020, 13:22:58 UTC | fixed for 8.10 | 27 October 2020, 15:27:07 UTC |
| f22a429 | Benjamin Salling Hvass | 07 August 2020, 12:32:30 UTC | removed admitted from Pow.v | 27 October 2020, 15:27:07 UTC |
| 27fd0cd | Benjamin Salling Hvass | 07 August 2020, 07:59:53 UTC | generated updated example of inversoin | 27 October 2020, 15:27:07 UTC |
| f5298c9 | Benjamin Salling Hvass | 08 July 2020, 16:06:51 UTC | fixed for 8.9 | 27 October 2020, 15:27:07 UTC |
| 9e57f1e | Benjamin Salling Hvass | 08 July 2020, 14:52:30 UTC | further refacotring and removal of omega | 27 October 2020, 15:27:07 UTC |
| 4967def | Benjamin Salling Hvass | 08 July 2020, 11:42:24 UTC | refactored/shortened proofs and updated for 8.12 | 27 October 2020, 15:27:07 UTC |
| 5bbda78 | Benjamin Salling Hvass | 05 July 2020, 19:34:42 UTC | updated to newest version of fiat | 27 October 2020, 15:27:07 UTC |
| 9cb0fc6 | Benjamin Salling Hvass | 10 June 2020, 16:57:00 UTC | fixed rebase mistake | 27 October 2020, 15:27:07 UTC |
| 3f1b7a0 | Benjamin Salling Hvass | 05 March 2020, 10:10:20 UTC | Bernstein-Yang inversion using word-by-word-montgomery strategy | 27 October 2020, 15:27:07 UTC |
| 90fc0d0 | jadep | 11 October 2020, 21:42:02 UTC | remove notations from bedrock2 output checks | 18 October 2020, 17:12:18 UTC |
| 8b7b15c | jadep | 11 October 2020, 19:58:05 UTC | fix appending syntax for new output files in Makefile | 18 October 2020, 17:12:18 UTC |
| 4bfc801 | jadep | 11 October 2020, 17:38:15 UTC | don't run bedrock2 output tests if SKIP_BEDROCK2 is true | 18 October 2020, 17:12:18 UTC |
| 77c278e | jadep | 11 October 2020, 16:23:48 UTC | move ladderstep_body and montladder_body print statements to automatically-checked output files | 18 October 2020, 17:12:18 UTC |
| fc77101 | jadep | 03 October 2020, 16:50:16 UTC | reprint ladderstep_body | 18 October 2020, 17:12:18 UTC |
| bfedefd | jadep | 03 October 2020, 16:44:01 UTC | change field specs to have output argument first | 18 October 2020, 17:12:18 UTC |
| d359dac | jadep | 07 September 2020, 18:53:41 UTC | WIP | 18 October 2020, 17:12:18 UTC |
| 58d539b | jadep | 07 September 2020, 19:03:44 UTC | update _CoqProject | 18 October 2020, 17:12:18 UTC |
| 1930388 | jadep | 07 September 2020, 18:54:58 UTC | add missing import | 18 October 2020, 17:12:18 UTC |
| be892af | jadep | 07 September 2020, 16:24:06 UTC | clean up Bedrock/Specs | 18 October 2020, 17:12:18 UTC |
| a4a5c14 | Jason Gross | 14 October 2020, 19:19:44 UTC | Slightly better printing | 14 October 2020, 19:19:44 UTC |
| d285a64 | Jason Gross | 14 October 2020, 19:19:32 UTC | Bump rewriter | 14 October 2020, 19:19:32 UTC |
| 3d15041 | Pierre-Marie Pédrot | 05 October 2020, 13:53:52 UTC | Adapt w.r.t. coq/coq#13139. | 05 October 2020, 18:15:35 UTC |
| 902c79a | Jason Gross | 22 September 2020, 18:56:22 UTC | Multi-license under MIT OR Apache-2.0 OR BSD-1-Clause Hopefully this will satisfy the Go team and might come closer to getting us into OpenSSL. We follow https://github.com/rust-lang/rust/tree/e0bc267512fc0cb49c86978192857e8187017f0b#license and https://github.com/rust-lang/rust/blob/e0bc267512fc0cb49c86978192857e8187017f0b/COPYRIGHT for wording. | 25 September 2020, 21:17:56 UTC |
| ac4da36 | Jason Gross | 23 September 2020, 22:19:51 UTC | Bump rewriter | 23 September 2020, 22:19:51 UTC |
| 3b2016f | Jason Gross | 23 September 2020, 21:32:56 UTC | Bump zarith dependency on Mac CI | 23 September 2020, 21:32:56 UTC |
| 9a701cd | Jason Gross | 23 September 2020, 21:06:57 UTC | aspell -c README.md | 23 September 2020, 21:06:57 UTC |
| 7486009 | Jason Gross | 19 September 2020, 03:06:42 UTC | Add some utility definitions | 19 September 2020, 03:06:42 UTC |
| 01bc458 | jadep | 07 September 2020, 15:10:05 UTC | add missing import | 10 September 2020, 02:10:58 UTC |
| a93ace1 | jadep | 07 September 2020, 14:48:34 UTC | separate montgomery-equivalence proofs into their own file, cleanup | 10 September 2020, 02:10:58 UTC |
| 792119a | jadep | 07 September 2020, 00:27:24 UTC | Bignum_to_bytes proved; representation working | 10 September 2020, 02:10:58 UTC |
| f632bf3 | jadep | 06 September 2020, 23:50:09 UTC | WIP: Bignum_from_bytes proved | 10 September 2020, 02:10:58 UTC |
| b751269 | jadep | 06 September 2020, 22:22:23 UTC | WIP: scalarmult correctness proven, field representation instantiation not fixed | 10 September 2020, 02:10:58 UTC |
| 29e152f | jadep | 23 August 2020, 22:28:30 UTC | WIP | 10 September 2020, 02:10:58 UTC |
| 33a7846 | jadep | 23 August 2020, 15:53:07 UTC | add from_bytes to field | 10 September 2020, 02:10:58 UTC |
| 3e3b1d8 | jadep | 20 August 2020, 19:46:18 UTC | use stackalloc in scmul implementation | 10 September 2020, 02:10:58 UTC |
| bb22bf9 | jadep | 20 August 2020, 15:34:58 UTC | add TODO | 10 September 2020, 02:10:58 UTC |
| 4b93f60 | jadep | 17 August 2020, 16:12:57 UTC | start proving implementation | 10 September 2020, 02:10:58 UTC |
| d5846f8 | jadep | 17 August 2020, 16:02:26 UTC | prove montgomery group parameters are valid | 10 September 2020, 02:10:58 UTC |
| 249b174 | jadep | 17 August 2020, 15:50:08 UTC | add #bits to ScalarFieldParameters and define Montgomery point representation | 10 September 2020, 02:10:58 UTC |
| e3eb299 | jadep | 17 August 2020, 14:10:36 UTC | prove equivalence of Curves version of montladder and rupicola-translated version | 10 September 2020, 02:10:58 UTC |
| 48d1094 | jadep | 17 August 2020, 12:40:48 UTC | use number of scalar bits as montladder bound | 10 September 2020, 02:10:58 UTC |
| 6ef489d | Jason Gross | 01 September 2020, 21:05:15 UTC | Wrap bedrock2 C functions for BoringSSL | 06 September 2020, 17:43:34 UTC |
| 78d0c3f | Jason Gross | 19 August 2020, 19:33:13 UTC | Remove dependencies on the real numbers By copying over the implementation of nsatz, we can drop the dependencies on the real axioms. Together with https://github.com/coq/coq/issues/12845, this should eliminate the last axioms reported by coqchk, allowing us to be done with #736 (maybe modulo adding a CI job to check that no axioms creep back in). Not clear to me if this is worth it... | 02 September 2020, 20:44:28 UTC |
| ea994f4 | Jason Gross | 01 September 2020, 21:52:51 UTC | Fix CI for update to Coq master | 01 September 2020, 21:52:51 UTC |
| d87ec31 | jadep | 21 August 2020, 10:43:39 UTC | bump rupicola version | 21 August 2020, 16:17:11 UTC |
| 630a2e3 | jadep | 20 August 2020, 19:56:30 UTC | use lib target for rupicola for faster builds | 21 August 2020, 16:17:11 UTC |
| e5b914e | jadep | 20 August 2020, 19:48:40 UTC | bump rupicola version | 21 August 2020, 16:17:11 UTC |
| 93b5796 | jadep | 15 August 2020, 14:52:50 UTC | update Specs/Group.v to match F-style scalar representation | 20 August 2020, 08:23:42 UTC |
| 8aa931d | jadep | 15 August 2020, 14:52:12 UTC | minor tactic tweak | 20 August 2020, 08:23:42 UTC |
| 52b22f4 | jadep | 15 August 2020, 14:06:02 UTC | remove fevals from postconditions | 20 August 2020, 08:23:42 UTC |
| 42be15f | jadep | 15 August 2020, 12:02:21 UTC | switch scalar field to use F | 20 August 2020, 08:23:42 UTC |
| 5b23371 | jadep | 15 August 2020, 11:58:48 UTC | change field specs to use F | 20 August 2020, 08:23:42 UTC |
| b9974f0 | Jason Gross | 19 August 2020, 18:05:58 UTC | Remove useless requires resulting in needless axioms The only remaining axioms we require are now the ones of the real numbers, transitively loaded by Nsatz | 19 August 2020, 18:05:58 UTC |
| acc220f | Jason Gross | 19 August 2020, 15:59:28 UTC | Update README.md | 19 August 2020, 15:59:28 UTC |
| 5bbdb0d | jadep | 17 August 2020, 13:47:59 UTC | change Definition back to Instance to preserve notation | 19 August 2020, 11:50:31 UTC |
| 32dcffb | jadep | 17 August 2020, 08:53:34 UTC | improve comments in spec parameter classes | 19 August 2020, 11:50:31 UTC |
| bf19fee | jadep | 17 August 2020, 08:52:08 UTC | change Instances to Definitions | 19 August 2020, 11:50:31 UTC |
