| 3cef12a | Manuel Barbosa | 10 October 2023, 09:38:20 UTC | Making this branch work with same Why3 version as main | 10 October 2023, 09:38:20 UTC |
| 029e3f4 | Manuel Barbosa | 08 October 2023, 19:43:05 UTC | Merge commit '9f46b97dbeee0cccd37d058721ee4f989a7bbe48' into deploy-quantum-upgrade | 08 October 2023, 19:43:05 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 |
| 8f62037 | François Dupressoir | 20 March 2023, 14:58:02 UTC | Revert "Fix QROM adversarial losslessness condition" This reverts commit b033d8d139740abf9fccf0f60da7764df0e0b851. | 20 March 2023, 14:58:02 UTC |
| b033d8d | François Dupressoir | 20 March 2023, 13:00:00 UTC | Fix QROM adversarial losslessness condition | 20 March 2023, 14:00:10 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 |
| 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 |
| cf77265 | Manuel Barbosa | 08 March 2023, 16:04:09 UTC | Counters for queries | 08 March 2023, 16:04:09 UTC |
| 1603355 | Manuel Barbosa | 05 March 2023, 18:36:14 UTC | Documentation for the qrom axioms in theories | 05 March 2023, 18:36:14 UTC |
| d16b3a3 | Manuel Barbosa | 26 February 2023, 17:45:33 UTC | Fixed bug in unused SRD axiom | 26 February 2023, 17:45:33 UTC |
| 860d4c7 | Manuel Barbosa | 26 February 2023, 13:37:37 UTC | Fixed bug in SC axiom and associated proofs | 26 February 2023, 13:37:37 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 |
| 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 |
| ce73dd0 | Pierre-Yves Strub | 16 February 2023, 15:27:42 UTC | Merge remote-tracking branch 'origin/main' into deploy-quantum-upgrade | 16 February 2023, 15:27:42 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 |
| 015cfcc | Pierre-Yves Strub | 16 February 2023, 09:10:05 UTC | Merge remote-tracking branch 'origin/main' into deploy-quantum-upgrade | 16 February 2023, 09:10:05 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 |
| cba0841 | Pierre-Yves Strub | 15 February 2023, 16:26:30 UTC | Merge branch 'deploy-opsem' into deploy-quantum-upgrade | 15 February 2023, 16:32:10 UTC |
| 7c46a74 | Benjamin Gregoire | 15 February 2023, 14:19:02 UTC | fix printing bug | 15 February 2023, 14:19:02 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 |
| 1b8c6f1 | Benjamin Gregoire | 14 February 2023, 13:48:37 UTC | fix previous merge | 14 February 2023, 13:48:37 UTC |
| a23d049 | Benjamin Gregoire | 14 February 2023, 13:25:09 UTC | remove admit in init_eager | 14 February 2023, 13:25:09 UTC |
| 947fadb | Benjamin Gregoire | 14 February 2023, 10:12:55 UTC | Merge branch 'main' into deploy-quantum-upgrade | 14 February 2023, 10:12:55 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 |
| e3888f9 | Manuel Barbosa | 13 February 2023, 15:45:10 UTC | T_QROM | 13 February 2023, 15:45:10 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 |
| 83cc9d7 | Manuel Barbosa | 13 February 2023, 13:38:46 UTC | Still Collision | 13 February 2023, 13:38:46 UTC |
| b9e4ebe | Manuel Barbosa | 12 February 2023, 21:07:30 UTC | Collision bound almost done | 12 February 2023, 21:07:30 UTC |
| 0a4b96c | Manuel Barbosa | 11 February 2023, 20:21:48 UTC | Tweaking collision in T_QROM | 11 February 2023, 20:21:48 UTC |
| acfb65a | Manuel Barbosa | 10 February 2023, 16:30:46 UTC | Query counting | 10 February 2023, 16:30:46 UTC |
| 1b4df3e | Manuel Barbosa | 10 February 2023, 15:25:08 UTC | Fixed query counting | 10 February 2023, 15:25:08 UTC |
| d7e9a28 | Manuel Barbosa | 08 February 2023, 18:34:38 UTC | error in classical game | 08 February 2023, 18:34:38 UTC |
| 595ad84 | Manuel Barbosa | 07 February 2023, 19:24:01 UTC | QROM now carries its own ROM | 07 February 2023, 19:24:01 UTC |
| 1070702 | Manuel Barbosa | 07 February 2023, 18:21:21 UTC | Classical collision | 07 February 2023, 18:21:21 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 |
| ec7e364 | Manuel Barbosa | 23 January 2023, 13:36:52 UTC | PRFs | 23 January 2023, 13:36:52 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 |
| a2d1e07 | Manuel Barbosa | 16 January 2023, 17:35:30 UTC | Merge branch 'main' into deploy-quantum-upgrade | 16 January 2023, 17:35:30 UTC |
| c299bbd | Pierre-Yves Strub | 11 January 2023, 08:40:38 UTC | proc | 11 January 2023, 08:40:38 UTC |
| b40c051 | Pierre-Yves Strub | 05 January 2023, 13:05:53 UTC | Merge branch 'main' into deploy-opsem | 05 January 2023, 13:05:53 UTC |
| ba37062 | Pierre-Yves Strub | 05 January 2023, 13:05:38 UTC | runtest: ECRJOBS env. variable | 05 January 2023, 13:05:38 UTC |
| d92e5f0 | Pierre-Yves Strub | 05 January 2023, 09:50:54 UTC | Merge branch 'main' into deploy-opsem | 05 January 2023, 09:50:54 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 |
| f2fbbe3 | Pierre-Yves Strub | 04 January 2023, 14:02:24 UTC | Merge branch 'main' into deploy-opsem | 04 January 2023, 14:02:24 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 |
| 1ce8c17 | Pierre-Yves Strub | 04 January 2023, 13:06:50 UTC | Merge branch 'main' into deploy-opsem | 04 January 2023, 13:06:50 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 |
| 4a99e7e | Pierre-Yves Strub | 04 January 2023, 12:47:53 UTC | Merge branch 'main' into deploy-opsem | 04 January 2023, 12:47:53 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 |
| f3b5429 | Pierre-Yves Strub | 23 December 2022, 16:21:40 UTC | . | 23 December 2022, 16:21:40 UTC |
| c776cd5 | Pierre-Yves Strub | 23 December 2022, 16:05:27 UTC | . | 23 December 2022, 16:05:27 UTC |
| e8576a5 | Pierre-Yves Strub | 16 December 2022, 15:13:02 UTC | iteriS_rw | 19 December 2022, 09:02:50 UTC |
| 47dc13a | Manuel Barbosa | 16 December 2022, 14:17:20 UTC | Merge branch 'deploy-quantum-upgrade' of github.com:easycrypt/easycrypt into deploy-quantum-upgrade | 16 December 2022, 14:17:20 UTC |
| 4a9f58f | Manuel Barbosa | 16 December 2022, 14:17:11 UTC | lossless guarantees for B | 16 December 2022, 14:17:11 UTC |
| 0583e0a | Pierre-Yves Strub | 15 December 2022, 14:46:47 UTC | . | 15 December 2022, 14:46:47 UTC |
| 2cbdee6 | Pierre-Yves Strub | 15 December 2022, 14:32:57 UTC | . | 15 December 2022, 14:32:57 UTC |
| b2f0651 | Benjamin Gregoire | 14 December 2022, 10:08:27 UTC | Merge branch 'main' into deploy-quantum-upgrade | 14 December 2022, 10:08:27 UTC |
| dd42a74 | Benjamin Gregoire | 14 December 2022, 09:37:13 UTC | [tactic]: fix t_solve performance issues | 14 December 2022, 10:01:29 UTC |
| f2a1723 | 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, 10:01:28 UTC |
| a0e56b2 | Pierre Boutry | 02 September 2022, 14:10:17 UTC | Remove dependency to oldlibs for Group | 14 December 2022, 10:01:20 UTC |
| dc8494c | Benjamin Gregoire | 09 December 2022, 14:10:57 UTC | Various bug fixes for clones (modules & lemmas) fix #292 | 14 December 2022, 10:00:21 UTC |
| 46d0453 | François Dupressoir | 21 March 2022, 16:15:38 UTC | force delta on convertibility checks Closes #154 | 14 December 2022, 09:59:20 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 |
| db12aa8 | Manuel Barbosa | 13 December 2022, 18:02:14 UTC | QLorR | 13 December 2022, 18:02:14 UTC |
| a168eb2 | Manuel Barbosa | 30 November 2022, 18:33:32 UTC | OW2H | 30 November 2022, 18:33:32 UTC |
| 2225c23 | Pierre-Yves Strub | 28 November 2022, 13:17:16 UTC | . | 28 November 2022, 13:17:16 UTC |
| 430daf6 | Pierre-Yves Strub | 28 November 2022, 06:02:07 UTC | . | 28 November 2022, 06:02:07 UTC |
| ddb653d | Pierre-Yves Strub | 27 November 2022, 11:09:54 UTC | . | 27 November 2022, 11:09:54 UTC |
| 47057ed | Manuel Barbosa | 25 November 2022, 13:29:36 UTC | added ow2h to installation | 25 November 2022, 13:29:36 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 |
| 3c4117a | Manuel Barbosa | 24 November 2022, 12:51:38 UTC | Merge branch 'deploy-quantum-upgrade' of github.com:easycrypt/easycrypt into deploy-quantum-upgrade | 24 November 2022, 12:51:38 UTC |
| 06b0e50 | Manuel Barbosa | 24 November 2022, 12:51:23 UTC | OW2H | 24 November 2022, 12:51:23 UTC |
| 5fbbd9c | Benjamin Gregoire | 22 November 2022, 12:41:00 UTC | cleanup | 22 November 2022, 12:41:00 UTC |
| 39c4e7a | Pierre-Yves Strub | 17 November 2022, 09:58:29 UTC | Merge branch 'main' into deploy-opsem | 17 November 2022, 09:58:29 UTC |
| a841354 | Pierre-Yves Strub | 17 November 2022, 09:58:25 UTC | nits | 17 November 2022, 09:58:25 UTC |
| f098d6e | Benjamin Gregoire | 17 November 2022, 09:08:21 UTC | Merge branch 'main' into deploy-quantum-upgrade | 17 November 2022, 09:08:21 UTC |
| 69c9c2e | Benjamin Gregoire | 11 November 2022, 08:06:12 UTC | add few lemmas on dfun | 16 November 2022, 08:40:22 UTC |
| 367513e | Manuel Barbosa | 15 November 2022, 18:15:46 UTC | Quantum version of Means | 15 November 2022, 18:15:46 UTC |
| 86d9eac | Manuel Barbosa | 15 November 2022, 18:10:42 UTC | Merge branch 'deploy-quantum' into deploy-quantum-upgrade | 15 November 2022, 18:10:42 UTC |
| 6bc9ba8 | Manuel Barbosa | 11 November 2022, 14:10:06 UTC | install theories | 11 November 2022, 14:10:06 UTC |
| 5785ce2 | Manuel Barbosa | 11 November 2022, 13:46:50 UTC | incorporated FunSamplingLib changes | 11 November 2022, 13:46:50 UTC |
