| 1e4e582 | Christian Doczkal | 14 June 2023, 14:00:26 UTC | Variant of FMap where get samples randomly | 14 June 2023, 14:00:26 UTC |
| b0eeedc | Yi Lee | 10 June 2023, 12:55:36 UTC | Take PolyReduce theory from Kyber project Add choice-based inverses and fix broken proofs from subtype changes Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> | 13 June 2023, 09:09:31 UTC |
| dfec6be | François Dupressoir | 27 March 2023, 08:59:03 UTC | restore name | 13 June 2023, 07:53:12 UTC |
| a4a0332 | François Dupressoir | 24 March 2022, 15:55:56 UTC | Tighten the ROM bad call results | 13 June 2023, 07:53:12 UTC |
| d481338 | François Dupressoir | 05 June 2023, 14:21:42 UTC | [lib] FSet: fcard_eq1 Co-authored-by: Christian Doczkal <christian.doczkal@mpi-sp.org> | 13 June 2023, 07:30:41 UTC |
| c73033b | François Dupressoir | 05 June 2023, 21:54:01 UTC | [lib] List: remove all raw smt calls | 13 June 2023, 07:14:59 UTC |
| ab21d3a | Pierre-Yves Strub | 12 June 2023, 11:53:09 UTC | New rewrite-pr lemma: Pr[muE] Transform a Pr[...] statement into its pointwise summation. | 12 June 2023, 12:22:39 UTC |
| 16747c7 | François Dupressoir | 04 May 2023, 10:24:24 UTC | properly fail early if one SMT returns `Invalid` This was seemingly intended, but racy | 10 June 2023, 22:35:56 UTC |
| cf55a7c | François Dupressoir | 04 May 2023, 10:22:26 UTC | warn on `Invalid` SMT results | 10 June 2023, 22:35:56 UTC |
| eaba09c | Christian Doczkal | 24 February 2023, 16:42:30 UTC | [theories]: p_max (maximum probability for atomic events) Co-authored-by: Ethan Lee <ylee1228@umd.edu> | 05 June 2023, 14:39:42 UTC |
| 4650947 | Cameron Low | 19 May 2023, 10:58:37 UTC | Removed Smart constructors for types, expressions, formulae, paths, and statements. | 05 June 2023, 06:53:24 UTC |
| dc50f44 | Pierre-Yves Strub | 26 May 2023, 09:54:58 UTC | Forbid the usage of [declare] for concrete modules. Fix #328 | 26 May 2023, 12:06:42 UTC |
| 8f15fcb | Pierre-Yves Strub | 25 May 2023, 14:14:03 UTC | Fix datatype comparisons for theory replays We do not need to check the inductive schemas: - if the constructors are compatible, so are the schemas, - anyway, they are going to be checked right after, and - at that point, they are not convertible because they come from incomaptible enclosing theories. Fix #381 | 25 May 2023, 14:30:11 UTC |
| 926927a | Pierre-Yves Strub | 25 May 2023, 14:06:49 UTC | Accept non-printed variable only abbreviations. fix #382 | 25 May 2023, 14:23:31 UTC |
| 242e996 | Pierre-Yves Strub | 25 May 2023, 13:58:07 UTC | New command: proc op. This command generates an operator that computes the output distribution of a stateless proc. The command is in beta-mode. It misses: - a support for a larger set of instructions, - better error messages, - a registry of generated proc ops, and - a hoare/phoare statement that links the operator to the procedure. | 25 May 2023, 14:16:01 UTC |
| cf79f50 | Christian Doczkal | 26 April 2023, 13:15:46 UTC | [theories] FunRO: RO for FinType using dfun for init | 23 May 2023, 10:49:03 UTC |
| 860dc3f | Christian Doczkal | 16 May 2023, 10:13:08 UTC | use polymorpic wrapper to enable theory cloning | 17 May 2023, 04:25:30 UTC |
| d77676c | Christian Doczkal | 15 May 2023, 15:27:15 UTC | clean up SubType theory | 17 May 2023, 04:25:30 UTC |
| a672c38 | Dominique Unruh | 14 May 2023, 15:50:01 UTC | Updated examples to match new Subtype. | 17 May 2023, 04:25:30 UTC |
| 957afc7 | Dominique Unruh | 14 May 2023, 15:20:56 UTC | New Subtype theory. Updated stdlib to match. | 17 May 2023, 04:25:30 UTC |
| ee26cc5 | Alley Stoughton | 15 May 2023, 19:51:42 UTC | Commit b2106aa suppressed additional parentheses around match ... end in all circumstances, even though on the left and right of applications the parser requires parentheses, the theory being this makes it easier for humans to scan. So this commit inserts parentheses around matches in applications, but not elsewhere (e.g., not in infix operators). See below for examples. [The pretty printer needs a major redesign, so this is another stopgap measure.] require import AllCore List. type t = [ A of int | B of bool]. (* the following formulas now parse and pretty-print the same *) lemma foo1 (f : int -> bool) : f (match A 3 with | A a => a | B b => if b then 1 else 2 end). proof. abort. lemma foo2 : (match A 3 with | A a => fun _ => a | B b => fun _ => 2 end) 3 = 4. proof. abort. lemma foo3 (f : (int -> int) -> (int -> int)) : f (match A 3 with | A a => fun _ => a | B b => fun _ => 2 end) 3 = 4. proof. abort. lemma foo4 (f : int -> bool) : f (1 + match A 3 with | A a => a | B b => if b then 1 else 2 end). proof. abort. lemma foo5 (f : int -> bool) : f (match A 3 with | A a => a | B b => if b then 1 else 2 end + 1). proof. abort. lemma foo6 (f : int -> bool) : f (3 + match A 3 with | A a => a | B b => if b then 1 else 2 end + 1). proof. abort. | 16 May 2023, 07:04:10 UTC |
| 94538c5 | François Dupressoir | 16 March 2023, 19:08:33 UTC | [ci] update actions to avoid node deprecation | 02 May 2023, 09:38:51 UTC |
| bde8af8 | Cameron Low | 28 March 2023, 16:09:16 UTC | Track the argument variables as well. Also update ROM proof. | 02 May 2023, 09:38:19 UTC |
| f626259 | Cameron Low | 21 March 2023, 14:35:30 UTC | [tactic] Rewrite Equiv | 24 March 2023, 13:44:07 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 69c9c2e | Benjamin Gregoire | 11 November 2022, 08:06:12 UTC | add few lemmas on dfun | 16 November 2022, 08:40:22 UTC |
| 1b369f9 | Benjamin Gregoire | 10 November 2022, 07:39:43 UTC | add theory Dfun_sub + backport many lemma from deploy-quantum | 10 November 2022, 10:06:28 UTC |
| 9f4a2f7 | Pierre-Yves Strub | 03 November 2022, 05:50:59 UTC | [ec-runtest]: add the possibility to exclude file based on the name The entry is `file_exclude`. It is a space-separated list of globs. A file is excluded if its basename matches any of the glob. See `fnmatch.fnmatch` of the standard Python libraries to get a description of which glob patterns are supported. Fix #303 | 07 November 2022, 20:30:11 UTC |
| 8d4e67d | ahuelsing | 02 November 2022, 11:35:35 UTC | added lemma assoc_none. (#304) trivial proof by rewrite assocTP mem_map_fst. but smt(assocTP mem_map_fst) fails. | 02 November 2022, 11:35:35 UTC |
| 5834e92 | Benjamin Gregoire | 28 October 2022, 05:05:43 UTC | add lemma mu_dlet_le : mu (dlet d F1) P1 <= mu (dlet d F2) P2 | 28 October 2022, 05:31:26 UTC |
| 9c54096 | Pierre-Yves Strub | 27 October 2022, 09:14:38 UTC | generalize big_pow lemmas | 27 October 2022, 12:04:41 UTC |
| f2011a3 | Benjamin Gregoire | 27 October 2022, 07:19:12 UTC | telescoping_sum + sum p^i + sum i*p^i | 27 October 2022, 12:04:41 UTC |
| 6593a9e | Benjamin Gregoire | 26 October 2022, 19:06:35 UTC | add cnvC cnv_pow | 26 October 2022, 20:11:44 UTC |
| 2df1d51 | Benjamin Gregoire | 26 October 2022, 15:36:01 UTC | lim (x^n) = 0 | 26 October 2022, 17:24:14 UTC |
| 024aa82 | Pierre-Yves Strub | 26 October 2022, 10:46:54 UTC | [stdlib] limit of a sequence of distributions | 26 October 2022, 13:11:02 UTC |
| f36307f | Pierre-Yves Strub | 26 October 2022, 09:54:52 UTC | [stdlib]: extra properties on lim | 26 October 2022, 10:47:29 UTC |
| d3da5af | Pierre-Yves Strub | 21 October 2022, 15:19:36 UTC | Fix bug in theory replay for modules. When checking for module convertibility, check the computed module flat expression (i.e. all module aliases have been resolved), not the module expression. Fix #292 | 26 October 2022, 10:47:29 UTC |
| c8bea89 | Pierre-Yves Strub | 21 October 2022, 11:55:39 UTC | Register for the pretty-printer | 26 October 2022, 07:43:45 UTC |
| d277b49 | Christian Doczkal | 21 October 2022, 15:19:28 UTC | remove admits in Ideal.ec | 21 October 2022, 16:16:34 UTC |
| 56054fd | oskgo | 18 October 2022, 22:05:21 UTC | Fix typos in user messages | 19 October 2022, 06:41:28 UTC |
| 2a75df5 | Christian Doczkal | 28 July 2022, 14:55:15 UTC | port Dexcepted to dresrict and deprecate Dfilter fixes #233 | 18 October 2022, 09:01:45 UTC |
| 147daa0 | Benjamin Gregoire | 17 October 2022, 07:51:05 UTC | tactic [byupto] add missing restriction in the case of adversary. | 18 October 2022, 07:19:47 UTC |
| 638229b | Pierre-Yves Strub | 17 October 2022, 13:37:47 UTC | Fix a bug when replaying a removed user reduction rule A local exception was raised but was not properly catched. Fix #268 | 17 October 2022, 13:50:21 UTC |
| 1dd5130 | Christian Doczkal | 12 May 2022, 08:35:59 UTC | [stdlib] bound collisions for ROmap | 17 October 2022, 13:31:22 UTC |
| fc2bfba | Christian Doczkal | 12 May 2022, 08:22:30 UTC | [stdlib] SmtMap: fsize and fcoll + some lemmas - #non-backward-compatible: May need to disambiguate SmtMap.mem_filter and List.mem_filter. | 17 October 2022, 13:31:22 UTC |
| 86472e0 | bgregoir | 16 October 2022, 23:52:10 UTC | add syntaxic upto tactic (#287) The tactic name is `byupto`. | 16 October 2022, 23:52:10 UTC |
| 9154d9a | Benjamin Gregoire | 13 October 2022, 14:38:45 UTC | lossless for equiv | 13 October 2022, 14:58:18 UTC |
| 3d0f508 | Sofía Celi | 10 October 2022, 11:27:22 UTC | Fix new link | 10 October 2022, 12:07:27 UTC |
| 8e046e1 | Pierre-Yves Strub | 09 October 2022, 06:11:02 UTC | Fix pretty-printing of high-order postfix operators | 09 October 2022, 06:24:47 UTC |
| ddb2336 | Pierre-Yves Strub | 08 October 2022, 11:10:02 UTC | Add postfix notations. Postfix operators are named "(%x)" where x is a low-ident. This generalizes the %r notation. | 08 October 2022, 11:41:17 UTC |
| 58d5547 | Pierre-Yves Strub | 07 October 2022, 15:27:31 UTC | Fix pretty-printing of %r | 07 October 2022, 15:27:40 UTC |
| b2d6b7e | Yi Lee | 29 July 2022, 06:47:55 UTC | [stdlib]: core theory conditional distributions | 07 October 2022, 10:27:08 UTC |
| 1198d07 | Benjamin Gregoire | 07 October 2022, 10:06:23 UTC | doCheck = false, for merlin (solve a pb with ld warning on mac) | 07 October 2022, 10:26:51 UTC |
| 63e4ead | Pierre-Yves Strub | 20 September 2022, 14:58:45 UTC | [conv]: add case for program variables & globals | 22 September 2022, 15:45:34 UTC |
| 80dba47 | Pierre-Yves Strub | 07 September 2022, 15:56:54 UTC | [while (phl, >=)]: be more restrictive on the variant delta lower-bound The lower-bound should be independent from the variables written by the loop body. | 07 September 2022, 16:10:30 UTC |
| f43464a | Yi Lee | 05 September 2022, 18:47:23 UTC | Allow quotient ring elements to be matrix entries | 05 September 2022, 20:15:21 UTC |
| 97dc179 | Ethan Lee | 05 September 2022, 15:16:34 UTC | Add camlp-streams dependency to nix build | 05 September 2022, 16:48:27 UTC |
