| 3787dc9 | Pierre Boutry | 02 June 2023, 13:47:12 UTC | scaled_monicM is provable for polynomials over fields but not over any integral domain | 02 June 2023, 13:47:12 UTC |
| a374108 | Pierre Boutry | 26 May 2023, 11:38:14 UTC | only scaled_monicM left | 26 May 2023, 11:38:14 UTC |
| 53f42b1 | Pierre Boutry | 26 May 2023, 08:11:27 UTC | proofs of the remaining lemmas about polynomial divison for integral domain | 26 May 2023, 08:11:27 UTC |
| 093903b | Antoine Séré | 04 May 2023, 12:56:08 UTC | abstracted some theories that needed to be | 04 May 2023, 12:56:08 UTC |
| f78e70f | Antoine Séré | 02 May 2023, 20:56:59 UTC | Removed error examples, added plan for unicity of finite fields if needed | 02 May 2023, 20:56:59 UTC |
| 05a9fea | Antoine Séré | 26 April 2023, 18:17:14 UTC | Finite field existence proven, up to admits in Perms and one PolyDiv admit | 26 April 2023, 18:17:14 UTC |
| 9cfe9a8 | Antoine Séré | 25 April 2023, 18:23:16 UTC | eqn half done | 25 April 2023, 18:23:16 UTC |
| d993761 | Antoine Séré | 24 April 2023, 21:31:26 UTC | working on ffexistence | 24 April 2023, 21:31:26 UTC |
| a984329 | Antoine Séré | 24 April 2023, 16:32:28 UTC | All but FFexistence fixed | 24 April 2023, 16:32:28 UTC |
| c73c7ab | Antoine Séré | 19 April 2023, 08:48:44 UTC | PY TODOS in examples/cloning | 19 April 2023, 08:48:44 UTC |
| 6bfbcfe | Antoine Séré | 19 April 2023, 08:09:38 UTC | PolyFF being fixed | 19 April 2023, 08:09:38 UTC |
| e611676 | Antoine Séré | 13 April 2023, 21:32:21 UTC | Almost fixed FiniteRing | 13 April 2023, 21:32:21 UTC |
| d24c834 | Antoine Séré | 13 April 2023, 11:42:00 UTC | FiniteRing half done | 13 April 2023, 11:42:00 UTC |
| 3fcde14 | Antoine Séré | 12 April 2023, 19:24:21 UTC | RingModule OK | 12 April 2023, 19:24:21 UTC |
| 056b39c | Antoine Séré | 12 April 2023, 17:42:56 UTC | RingStruct, RingMorph and SubRing OK | 12 April 2023, 17:42:56 UTC |
| 5865a36 | Antoine Séré | 12 April 2023, 12:45:45 UTC | RingMorph ok | 12 April 2023, 12:45:45 UTC |
| 7518f5f | Antoine Séré | 11 April 2023, 20:31:28 UTC | RingStruct stabilized | 11 April 2023, 20:31:28 UTC |
| 799979f | Antoine Séré | 10 April 2023, 23:57:03 UTC | Still broken, but getting there | 10 April 2023, 23:57:03 UTC |
| db7f901 | Antoine Séré | 09 April 2023, 23:01:46 UTC | Broken, use previous commit or next | 09 April 2023, 23:01:46 UTC |
| e6eaea1 | Antoine Séré | 07 April 2023, 10:13:57 UTC | FIXMEs for PY | 07 April 2023, 10:13:57 UTC |
| 072df4c | Antoine Séré | 07 April 2023, 08:14:58 UTC | clone name changed | 07 April 2023, 08:14:58 UTC |
| 9787b78 | Antoine Séré | 07 April 2023, 07:41:02 UTC | done up to clone issue | 07 April 2023, 07:41:02 UTC |
| c086c7e | Antoine Séré | 05 April 2023, 19:06:24 UTC | equality of n lemma and some admits remain | 05 April 2023, 19:06:24 UTC |
| 968f589 | Antoine Séré | 04 April 2023, 19:43:12 UTC | Made exerything work up to examples smt failures | 04 April 2023, 19:43:12 UTC |
| db27238 | Antoine Séré | 04 April 2023, 18:36:04 UTC | Done up to int equalities in FFexistence | 04 April 2023, 18:36:04 UTC |
| 5e937ad | Antoine Séré | 03 April 2023, 20:05:19 UTC | Quotient by an irreducible polynomial is a field | 03 April 2023, 20:05:19 UTC |
| b6dacb7 | Antoine Séré | 31 March 2023, 16:42:54 UTC | merged wit main | 31 March 2023, 16:42:54 UTC |
| e8216e0 | Antoine Séré | 31 March 2023, 15:39:08 UTC | pre merge to fix or identify clone issue | 31 March 2023, 15:39:08 UTC |
| a1ad207 | Antoine Séré | 30 March 2023, 17:42:01 UTC | Interface in Perms is now complete, all done in core up to the last FF clone | 30 March 2023, 17:42:01 UTC |
| 783c8e9 | Antoine Séré | 30 March 2023, 08:06:23 UTC | Perms should have all the required admits | 30 March 2023, 08:06:23 UTC |
| ba674de | Antoine Séré | 29 March 2023, 18:22:42 UTC | Proof advanced | 29 March 2023, 18:22:42 UTC |
| 87d1750 | Antoine Séré | 27 March 2023, 17:47:25 UTC | Some changes to Perms | 27 March 2023, 17:47:25 UTC |
| f626259 | Cameron Low | 21 March 2023, 14:35:30 UTC | [tactic] Rewrite Equiv | 24 March 2023, 13:44:07 UTC |
| 4a81710 | Antoine Séré | 22 March 2023, 18:23:38 UTC | Proof done up to admits and some minor lemma changes in FFexistence | 22 March 2023, 18:23:38 UTC |
| 91553de | Antoine Séré | 21 March 2023, 20:54:13 UTC | counting lemmas | 21 March 2023, 20:54:13 UTC |
| b2106aa | Alley Stoughton | 08 March 2023, 00:26:51 UTC | An attempt at fixing pretty printing bugs in which formulas that end with implications, conditionals or quantifiers and appear to the left of binary operators have their scopes extended to include those following binary operators. E.g., (3 :: 4 :: let x = 1 in [x]) = ys. incorrectly pretty prints as 3 :: 4 :: let x = 1 in [x] = ys | 21 March 2023, 10:59:33 UTC |
| ee4c20e | François Dupressoir | 16 March 2023, 20:56:12 UTC | [chore] update dependency versions in README | 20 March 2023, 16:28:35 UTC |
| ed96ecf | François Dupressoir | 16 March 2023, 16:21:06 UTC | fix a failing proof in MEE-CBC this aligns the top-level proof with earlier changes to a leaf theory | 20 March 2023, 16:28:35 UTC |
| ad96b3d | Pierre-Yves Strub | 16 March 2023, 15:39:37 UTC | simplify some smt calls | 20 March 2023, 16:28:35 UTC |
| 7a00b11 | François Dupressoir | 16 March 2023, 15:21:40 UTC | Remove raw smt in MEE-CBC | 20 March 2023, 16:28:35 UTC |
| 472a2d4 | François Dupressoir | 14 March 2023, 14:34:41 UTC | bump Why3 version in .nix files | 20 March 2023, 16:28:35 UTC |
| 9f46b97 | Pierre-Yves Strub | 10 March 2023, 18:18:12 UTC | Bump Why3 supported version (1.5 -> 1.6) This makes EC compatible with OCaml 5. Close #350 | 20 March 2023, 16:28:35 UTC |
| 1365cea | François Dupressoir | 16 March 2023, 16:34:50 UTC | drop unused and obsolete theory files | 17 March 2023, 13:57:32 UTC |
| 28b21dd | Antoine Séré | 17 March 2023, 12:25:11 UTC | Intermediaries for enumeration of polynomials added | 17 March 2023, 12:25:11 UTC |
| 189283a | Pierre-Yves Strub | 15 March 2023, 06:59:34 UTC | Move to github docker repository | 15 March 2023, 07:41:31 UTC |
| bc97ee6 | Manuel Barbosa | 08 March 2023, 17:44:34 UTC | Extend definition of PKE to ROM from Kyber spec | 14 March 2023, 14:39:11 UTC |
| c7500bd | Francois Dupressoir | 14 March 2023, 14:26:40 UTC | [nix] pin the Why3 version (#353) * [nix] pin the Why3 version This makes it easier to bump versions and rely on CI even if out of sync with nixpkgs PRs. | 14 March 2023, 14:26:40 UTC |
| d70e42f | Antoine Séré | 09 March 2023, 20:14:34 UTC | Merged | 09 March 2023, 20:14:34 UTC |
| 3ae3a55 | Antoine Séré | 09 March 2023, 19:57:36 UTC | one annoying admit in PolyDiv should be adressed | 09 March 2023, 19:57:36 UTC |
| 4ef8183 | Pierre Boutry | 09 March 2023, 16:21:19 UTC | add admitted version of the remaining lemmas about polynomial divison for integral domain | 09 March 2023, 16:21:19 UTC |
| 1c5d848 | Antoine Séré | 08 March 2023, 14:32:21 UTC | PolyDiv mods | 08 March 2023, 14:32:21 UTC |
| 9fd32ce | Antoine Séré | 05 March 2023, 19:57:14 UTC | in progress | 05 March 2023, 19:57:14 UTC |
| 472ee70 | Antoine Séré | 01 March 2023, 18:14:18 UTC | Core of proof has advanced | 01 March 2023, 18:14:18 UTC |
| 8393681 | Antoine Séré | 01 March 2023, 17:47:38 UTC | Merge branch 'theory_finite_field' of github:EasyCrypt/easycrypt into theory_finite_field | 01 March 2023, 17:47:38 UTC |
| 155a193 | Antoine Séré | 01 March 2023, 17:47:13 UTC | Pre merge | 01 March 2023, 17:47:13 UTC |
| 032d3c9 | Pierre Boutry | 01 March 2023, 17:45:22 UTC | the version of Gauss that Antoine deserves | 01 March 2023, 17:45:22 UTC |
| 3494436 | Antoine Séré | 27 February 2023, 10:13:37 UTC | All but irreducible poly cardinal double counting done | 27 February 2023, 10:13:37 UTC |
| 00590a4 | Antoine Séré | 25 February 2023, 17:52:47 UTC | Merge branch 'theory_finite_field' of github:EasyCrypt/easycrypt into theory_finite_field | 25 February 2023, 17:52:47 UTC |
| bad6b21 | Antoine Séré | 25 February 2023, 17:51:40 UTC | Limits of poly | 25 February 2023, 17:51:40 UTC |
| be0a303 | Antoine Séré | 24 February 2023, 22:35:26 UTC | Added bigO, smallo and relevant lemmas | 24 February 2023, 22:35:26 UTC |
| 4d19d94 | Pierre Boutry | 24 February 2023, 16:25:57 UTC | proof of comp_polyM | 24 February 2023, 16:25:57 UTC |
| 5cd9d5d | Antoine Séré | 23 February 2023, 17:37:06 UTC | Core of the exist proof continued | 23 February 2023, 17:37:06 UTC |
| ad13f30 | Christian Doczkal | 21 February 2023, 16:17:11 UTC | [theories]: add various individual lemmas | 21 February 2023, 16:33:42 UTC |
| a347ecb | Christian Doczkal | 21 February 2023, 14:32:59 UTC | [theories]: port "lock" from MathComp | 21 February 2023, 14:47:31 UTC |
| 5072789 | Christian Doczkal | 21 February 2023, 13:17:16 UTC | [theories]: finite expectation (Jensen_fin_concave) | 21 February 2023, 14:16:50 UTC |
| 1ccf46b | Christian Doczkal | 20 February 2023, 16:56:15 UTC | [theories]: lemmas for dcond and dbiased | 21 February 2023, 11:29:39 UTC |
| 961a3ea | Pierre Boutry | 17 February 2023, 13:50:34 UTC | only comp_polyM left | 17 February 2023, 13:50:34 UTC |
| cc31629 | François Dupressoir | 22 July 2022, 14:34:38 UTC | [ci]: workflow to compile with nix | 17 February 2023, 12:12:25 UTC |
| d401307 | François Dupressoir | 19 July 2022, 16:24:35 UTC | [nix]: shell.nix + default.nix | 17 February 2023, 12:12:25 UTC |
| ae4a816 | Pierre-Yves Strub | 16 February 2023, 14:10:41 UTC | default.nix: option to install provers + install Python3 deps | 16 February 2023, 15:21:56 UTC |
| a9f3453 | Christian Doczkal | 16 February 2023, 09:14:19 UTC | mention dune3/alt-ergo-2.4.2 issue | 16 February 2023, 09:19:39 UTC |
| d47a0cd | Pierre-Yves Strub | 16 February 2023, 08:11:31 UTC | kill dead code | 16 February 2023, 08:11:31 UTC |
| 8eca6c7 | Pierre-Yves Strub | 16 February 2023, 07:59:20 UTC | default.nix: update dependencies | 16 February 2023, 07:59:20 UTC |
| 294e2a6 | Pierre-Yves Strub | 15 February 2023, 12:11:06 UTC | [dune]: auto-generate the list of EC files to be installed This requires dune >= 3.6 | 15 February 2023, 12:11:09 UTC |
| efab580 | oskgo | 14 February 2023, 14:59:30 UTC | matrix library with support for arbitrary dynamic size (#267) | 14 February 2023, 15:25:42 UTC |
| 6f695ba | Pierre-Yves Strub | 08 February 2023, 16:47:48 UTC | Fix encoding of Why3 fixpoint containing higher-order calls to itself Fix #334 | 14 February 2023, 10:12:50 UTC |
| 94ccd48 | Pierre-Yves Strub | 10 February 2023, 10:42:21 UTC | Implement a naive termination checker Termination is done via a simple subterm check on the last inductive argument. Ref #62, #144 | 14 February 2023, 10:12:41 UTC |
| a4e43d1 | Benjamin Gregoire | 31 January 2023, 11:38:24 UTC | remove admitted proof in DJoin | 14 February 2023, 10:10:22 UTC |
| 88928de | Pierre-Yves Strub | 23 January 2023, 10:23:53 UTC | [theories]: ring with generic (choice based) inverse | 13 February 2023, 15:20:47 UTC |
| 2803f66 | Yi Lee | 24 January 2023, 10:18:25 UTC | Attempt to implement `RingQuotientDflInv` | 13 February 2023, 15:06:56 UTC |
| 6890aca | Benjamin Gregoire | 04 February 2023, 10:56:31 UTC | fix small bug in reduction of projection | 04 February 2023, 10:59:08 UTC |
| 472c8db | Alley Stoughton | 30 January 2023, 19:45:47 UTC | Added cancellation variant for ofword that uses mkseq to Word.eca, and added lemmas about the integer values of onew and zerow to BitWord.eca. | 31 January 2023, 13:42:57 UTC |
| 701f4f0 | Cameron Low | 20 January 2023, 18:18:02 UTC | Unify created variables correctly. | 23 January 2023, 15:43:55 UTC |
| 2f98c08 | Pierre-Yves Strub | 19 January 2023, 08:42:37 UTC | [tactic]: add the ability to create a memory from thin air. The syntax is `pose &m`. Close #320 | 20 January 2023, 09:28:31 UTC |
| 7f08941 | Cameron Low | 19 January 2023, 18:14:06 UTC | [tactic]: added hoare variant for `match` Here is an example of use: ``` require import AllCore. type t = [ A of int | B of bool | C ]. module M = { proc f(x : t) : int = { var y : int <- 0; match x with | A v => y <- `|v|; | B _ => y <- 1; | C => y <- 2; end; return y; } }. lemma L : hoare[M.f : true ==> 0 <= res]. proof. by proc; sp; match => [v|b|]; auto=> /> /#. qed. ``` | 19 January 2023, 21:44:41 UTC |
| 4a7a9c1 | Pierre Boutry | 06 January 2023, 17:59:57 UTC | polynomial Euclidean division done for rings | 06 January 2023, 18:10:34 UTC |
| ba37062 | Pierre-Yves Strub | 05 January 2023, 13:05:38 UTC | runtest: ECRJOBS env. variable | 05 January 2023, 13:05:38 UTC |
| e034e6c | Pierre-Yves Strub | 05 January 2023, 09:29:25 UTC | [internal]: fix detection of empty expression-level substitutions. | 05 January 2023, 09:50:08 UTC |
| b1fe56d | Pierre-Yves Strub | 04 January 2023, 14:01:27 UTC | remove unused dependency (cmdliner) | 04 January 2023, 14:01:27 UTC |
| c7ceb4f | Pierre-Yves Strub | 04 January 2023, 14:01:09 UTC | [runtest]: better display of multi-line error messages | 04 January 2023, 14:01:09 UTC |
| ff6a4bb | Pierre-Yves Strub | 04 January 2023, 13:04:49 UTC | [runtest]: append scenarios to the CLI | 04 January 2023, 13:06:36 UTC |
| 36e617d | Pierre-Yves Strub | 07 October 2022, 11:31:14 UTC | [CLI]: ec-runtest is now accessible via a CLI subcommand - the subcommand is named `runtest` - the real script is now in `<libexec>/easycrypt/commands/` | 04 January 2023, 12:46:39 UTC |
| 796cc2d | Benjamin Gregoire | 14 December 2022, 09:37:13 UTC | [tactic]: fix t_solve performance issues | 14 December 2022, 09:49:19 UTC |
| f180466 | Oskar Goldhahn | 15 March 2022, 16:24:16 UTC | operator to get maximal element in list use predicates formatting and replacing abstract theory with section disambiguate max operator patch smt failure | 14 December 2022, 09:48:07 UTC |
| 9656af6 | Pierre Boutry | 02 September 2022, 14:10:17 UTC | Remove dependency to oldlibs for Group | 14 December 2022, 09:46:38 UTC |
| d1dc434 | Benjamin Gregoire | 09 December 2022, 14:10:57 UTC | Various bug fixes for clones (modules & lemmas) fix #292 | 14 December 2022, 09:23:39 UTC |
| 65f1233 | Antoine Séré | 29 November 2022, 17:23:07 UTC | Added admitted lemmas in Perms | 29 November 2022, 17:23:07 UTC |
| ee7c5ff | François Dupressoir | 21 March 2022, 16:15:38 UTC | force delta on convertibility checks Closes #154 | 24 November 2022, 16:39:53 UTC |
| 68c075b | Antoine Séré | 17 November 2022, 19:23:03 UTC | Proof of existence of finite fields continuing | 17 November 2022, 19:24:04 UTC |
| 69c9c2e | Benjamin Gregoire | 11 November 2022, 08:06:12 UTC | add few lemmas on dfun | 16 November 2022, 08:40:22 UTC |
