| 77802af | Pierre-Yves Strub | 16 February 2023, 15:28:03 UTC | Merge remote-tracking branch 'origin/main' into deploy-expected-cost | 16 February 2023, 15:28:03 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 |
| dc7e65a | Pierre-Yves Strub | 15 February 2023, 12:12:21 UTC | Merge branch 'main' into deploy-expected-cost | 15 February 2023, 12:12:21 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 |
| a5b9b87 | oskgo | 14 February 2023, 14:59:30 UTC | matrix library with support for arbitrary dynamic size (#267) | 15 February 2023, 09:41:15 UTC |
| dfee727 | Pierre-Yves Strub | 08 February 2023, 16:47:48 UTC | Fix encoding of Why3 fixpoint containing higher-order calls to itself Fix #334 | 15 February 2023, 09:41:15 UTC |
| 7157047 | 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 | 15 February 2023, 09:41:15 UTC |
| d39b2b4 | Benjamin Gregoire | 31 January 2023, 11:38:24 UTC | remove admitted proof in DJoin | 15 February 2023, 09:41:15 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 |
| c758c50 | Pierre-Yves Strub | 14 February 2023, 08:11:39 UTC | gendune | 14 February 2023, 08:11:39 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 |
| f01d22c | Pierre-Yves Strub | 13 February 2023, 15:07:12 UTC | Merge branch 'main' into deploy-expected-cost | 13 February 2023, 15:07:12 UTC |
| 2803f66 | Yi Lee | 24 January 2023, 10:18:25 UTC | Attempt to implement `RingQuotientDflInv` | 13 February 2023, 15:06:56 UTC |
| 544ee3d | Yi Lee | 24 January 2023, 10:18:25 UTC | Attempt to implement `RingQuotientDflInv` | 13 February 2023, 15:04:43 UTC |
| 5818999 | Pierre-Yves Strub | 23 January 2023, 10:23:53 UTC | [theories]: ring with generic (choice based) inverse | 13 February 2023, 15:04:43 UTC |
| 5be6185 | Benjamin Gregoire | 04 February 2023, 11:00:06 UTC | Merge branch 'main' into deploy-expected-cost | 04 February 2023, 11:00:06 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 |
| c0cdd0f | Benjamin Gregoire | 29 January 2023, 15:32:43 UTC | add usefull lemma | 29 January 2023, 15:32:43 UTC |
| d648f35 | Benjamin Gregoire | 27 January 2023, 08:29:34 UTC | conseq ehore prhl ehore + small fixes | 27 January 2023, 08:29:34 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 |
| 605d9cf | Benjamin Gregoire | 14 December 2022, 10:06:31 UTC | Merge branch 'main' into deploy-expected-cost | 14 December 2022, 10:06:31 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 |
| f1527b7 | Benjamin Gregoire | 14 December 2022, 09:25:27 UTC | Merge branch 'main' into deploy-expected-cost | 14 December 2022, 09:25:27 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 |
| d64fa9e | Benjamin Gregoire | 13 December 2022, 15:47:58 UTC | restore variable order in exists* | 13 December 2022, 15:47:58 UTC |
| 5c8cb85 | Pierre-Yves Strub | 24 November 2022, 16:40:50 UTC | Merge branch 'main' into deploy-expected-cost | 24 November 2022, 16:40:50 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 |
| 4334a9a | Benjamin Gregoire | 08 November 2022, 07:56:14 UTC | Merge branch 'deploy-fix-292' into deploy-expected-cost | 08 November 2022, 07:56:14 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 |
| 2b54cca | Benjamin Gregoire | 29 October 2022, 06:29:51 UTC | add local module during conversion | 29 October 2022, 06:29:51 UTC |
| 2a239ce | Benjamin Gregoire | 29 October 2022, 04:13:52 UTC | Merge branch 'main' into deploy-fix-292 | 29 October 2022, 04:13:52 UTC |
| 4d742dd | Benjamin Gregoire | 28 October 2022, 05:52:03 UTC | Merge branch 'main' into deploy-expected-cost | 28 October 2022, 05:52:03 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 |
| b4ab6a3 | Benjamin Gregoire | 27 October 2022, 19:13:21 UTC | Merge branch 'main' into deploy-expected-cost | 27 October 2022, 19:13:21 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 |
| 971b141 | Benjamin Gregoire | 27 October 2022, 03:48:30 UTC | Merge branch 'main' into deploy-expected-cost | 27 October 2022, 03:48:30 UTC |
| 6593a9e | Benjamin Gregoire | 26 October 2022, 19:06:35 UTC | add cnvC cnv_pow | 26 October 2022, 20:11:44 UTC |
| 538e486 | Benjamin Gregoire | 26 October 2022, 18:24:26 UTC | Merge branch 'main' into deploy-expected-cost | 26 October 2022, 18:24:26 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 |
| b87594c | Benjamin Gregoire | 25 October 2022, 13:10:47 UTC | add t_ehoare_zero tactic | 25 October 2022, 13:10:47 UTC |
| 49125a7 | Benjamin Gregoire | 24 October 2022, 23:30:32 UTC | add reduction/conversion rules for ehoare | 24 October 2022, 23:30:32 UTC |
| d277b49 | Christian Doczkal | 21 October 2022, 15:19:28 UTC | remove admits in Ideal.ec | 21 October 2022, 16:16:34 UTC |
| 9e7229c | 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 | 21 October 2022, 15:19:36 UTC |
| 91b756a | Benjamin Gregoire | 21 October 2022, 11:25:38 UTC | fix Xreal | 21 October 2022, 11:25:38 UTC |
| db5728e | Benjamin Gregoire | 19 October 2022, 09:47:16 UTC | Merge branch 'main' into deploy-expected-cost | 19 October 2022, 09:47:16 UTC |
| b74e275 | Benjamin Gregoire | 19 October 2022, 09:45:10 UTC | WIP | 19 October 2022, 09:45:10 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 |
| 5b37c16 | Benjamin Gregoire | 18 October 2022, 08:38:58 UTC | Merge branch 'main' into deploy-expected-cost | 18 October 2022, 08:38:58 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 |
| b15ebcf | Benjamin Gregoire | 13 October 2022, 13:03:27 UTC | WIP | 13 October 2022, 13:03:27 UTC |
| 8e7c41b | Benjamin Gregoire | 12 October 2022, 07:03:08 UTC | exlim for ehoare | 12 October 2022, 07:03:08 UTC |
| d23b8c0 | Benjamin Gregoire | 12 October 2022, 04:48:02 UTC | add byehoare, fix if/rcond/case tactics for ehoare | 12 October 2022, 04:48:02 UTC |
| 3d0f508 | Sofía Celi | 10 October 2022, 11:27:22 UTC | Fix new link | 10 October 2022, 12:07:27 UTC |
| 1acf588 | Benjamin Gregoire | 09 October 2022, 19:48:16 UTC | fix proc inv for ehoare | 09 October 2022, 19:48:16 UTC |
| e295a0d | Benjamin Gregoire | 09 October 2022, 19:31:16 UTC | ehoare : add tactic call + call / + conseq / | 09 October 2022, 19:31:16 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 |
| 2596309 | Benjamin Gregoire | 08 October 2022, 12:28:54 UTC | use post-fix notations | 08 October 2022, 12:28:54 UTC |
| f77725d | Benjamin Gregoire | 08 October 2022, 11:47:06 UTC | Merge branch 'main' into deploy-expected-cost | 08 October 2022, 11:47:06 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 |
| 49f0390 | Benjamin Gregoire | 08 October 2022, 11:34:52 UTC | Merge branch 'main' into deploy-expected-cost | 08 October 2022, 11:34:52 UTC |
| b4a04b3 | Benjamin Gregoire | 08 October 2022, 11:33:09 UTC | stop using bool | xreal for ehoare | 08 October 2022, 11:33:09 UTC |
| d9ded91 | Benjamin Gregoire | 08 October 2022, 04:36:09 UTC | add inv/div, Rp.(<=) become an abbrev | 08 October 2022, 04:36:09 UTC |
| 675d3e3 | Benjamin Gregoire | 07 October 2022, 16:03:34 UTC | start adding call and proc rule | 07 October 2022, 16:03:34 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 |
| 6b5afaa | Benjamin Gregoire | 07 October 2022, 10:01:32 UTC | Merge branch 'main' into deploy-expected-cost | 07 October 2022, 10:01:32 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 |
