| 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 |
| 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 |
| 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 |
| be40298 | Pierre-Yves Strub | 05 September 2022, 14:19:50 UTC | [stdlib]: Matrix: coeffs in a comm. ring instead of an ID. | 05 September 2022, 14:49:50 UTC |
| 750a491 | Pierre-Yves Strub | 05 September 2022, 08:35:21 UTC | [build]: use camlp-streams This resolves the deprecation warning about the Stream module. Fix #186 | 05 September 2022, 08:46:47 UTC |
| 70ac960 | Pierre-Yves Strub | 19 June 2022, 19:47:35 UTC | [breaking] Fix unsound pHL while rule This fixes #212 and implements a version of the pHL while rule which does have a(n unpublished) pen-and-paper proof. This (obviously) makes using the pHL while rule generally less simple, but particularly so when the loop condition itself is probabilistically modified by the loop body (as, for example, in rejection sampling). In general, the bound given to the `while` tactic in those cases will need to be conditional. (Essentially capturing control-flow conditions in the bound itself.) Examples of proofs illustrating this case can be found in theories/distributions/Dexcepted.ec (starting line 299, including the conseq) and examples/PIR.ec (starting line 202, including also the conseq). Upper-bounds should be unaffected. On lower bounds, one can no longer apply the upper bound rule. On equalities, we have now added the lower-bound exit check (that if the loop is not entered and the event is true, then the probability should be 1), and further missing checks. In all cases, the inductive reasoning case was simplified to remove duplicated control-flow. co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr> co-authored-by: François Dupressoir <fdupress@gmail.com> | 05 September 2022, 08:27:00 UTC |
| 38fb166 | Pierre-Yves Strub | 05 September 2022, 08:14:39 UTC | In tactic apply[alpha]: instiantiate type-varaibles. Fix #255 | 05 September 2022, 08:25:14 UTC |
| f8c2cac | Pierre-Yves Strub | 31 August 2022, 09:35:29 UTC | Fix MEE-CBC example failing smt call | 31 August 2022, 16:50:48 UTC |
| 94be874 | Pierre-Yves Strub | 31 August 2022, 09:22:43 UTC | Remove unused PF-WP | 31 August 2022, 09:58:51 UTC |
| 7f37e97 | Christian Doczkal | 10 August 2022, 10:00:03 UTC | Lemmas on dprod and djoin | 30 August 2022, 09:20:18 UTC |
| af067ba | Pierre-Yves Strub | 26 August 2022, 06:02:12 UTC | In `cloning ... with lemma...`, disable inference for `apply` Ref #247 | 30 August 2022, 07:26:44 UTC |
| 0aeaa74 | Pierre-Yves Strub | 26 August 2022, 06:01:22 UTC | Distinction between modules & module types path in the hi-level subst. Ref #247 | 30 August 2022, 07:26:44 UTC |
| c7fb3d9 | Yi Lee | 11 August 2022, 23:15:39 UTC | Relate dbiased and dmap | 29 August 2022, 13:03:15 UTC |
| b2273f0 | Pierre-Yves Strub | 29 August 2022, 12:34:54 UTC | Add a warning for useless delta-unfolding The option name is `und_delta`. It is disabled by default. The mechanism can emit false positive, e.g. in: `try rewrite /foo.` | 29 August 2022, 13:02:25 UTC |
| f9d2bf6 | Pierre-Yves Strub | 23 August 2022, 15:09:17 UTC | When replaying a reduction rule, check that the rule does still exists. Currently, when the reduction rule does not exist anymore (because it has been removed by the inlining mechanism), the cloning fails with a lookup error. Ref #247 | 23 August 2022, 16:00:41 UTC |
| 6d0e464 | Pierre-Yves Strub | 23 August 2022, 11:30:30 UTC | Enforce section restrictions on the types of declared modules. Fix #245 | 23 August 2022, 12:07:34 UTC |
| 644ddc2 | Pierre-Yves Strub | 09 August 2022, 07:51:07 UTC | Fix a typing annotation bug in distribution tags' axioms fix #241 | 09 August 2022, 09:00:42 UTC |
| 1587d64 | Pierre-Yves Strub | 09 August 2022, 07:53:49 UTC | Fix unprecise/invalid error message | 09 August 2022, 07:53:49 UTC |
| c8d3d6c | Ethan Lee | 18 July 2022, 17:11:20 UTC | [theories]: Add scalar-vector multiplication | 23 July 2022, 07:07:55 UTC |
| fec4d5f | Pierre-Yves Strub | 23 July 2022, 05:43:55 UTC | [build]: add option -f to codesign | 23 July 2022, 06:12:54 UTC |
| aee8bfe | Pierre-Yves Strub | 19 July 2022, 06:18:57 UTC | CI: mechanism for checking external developments Currently, this mechanism is configured to check the Jasmin ECLib | 22 July 2022, 12:34:18 UTC |
| b184b1d | Pierre-Yves Strub | 19 July 2022, 13:46:58 UTC | theories: add back "oldlibs" in the CI + fix | 19 July 2022, 14:08:51 UTC |
| ea77e0e | Benjamin Gregoire | 15 July 2022, 07:47:48 UTC | add looptransform | 15 July 2022, 08:36:36 UTC |
| 53f3e84 | François Dupressoir | 11 July 2022, 09:31:07 UTC | slightly reduce reliance on trivial SMT calls | 12 July 2022, 16:44:15 UTC |
| bef5649 | François Dupressoir | 12 May 2022, 13:34:34 UTC | unify meaning of `by []` `lemma ... by [].` is now short for `lemma ... by (by []).` (instead of `by smt.`) Fixes #191. | 12 July 2022, 16:44:15 UTC |
| 57be028 | François Dupressoir | 02 July 2022, 08:57:59 UTC | strip out code related to proc * | 12 July 2022, 16:38:49 UTC |
| df8a2f9 | François Dupressoir | 30 June 2022, 20:39:24 UTC | Remove parser support for `proc *` in module sigs A deeper removal is still needed to fully address #206. | 12 July 2022, 16:38:43 UTC |
| c954ae0 | Antoine Séré | 25 April 2022, 14:53:39 UTC | Hakyber jasmin eclib | 12 July 2022, 09:10:25 UTC |
| 5524b72 | Pierre-Yves Strub | 09 July 2022, 05:54:47 UTC | Fix ordering of variables in `rndsem` The chosen ordering is the order of appearance as a left-value in the program. fix #220 | 09 July 2022, 06:08:59 UTC |
| ca3d10a | Pierre-Yves Strub | 09 July 2022, 05:15:03 UTC | Fix naming issue for the [#] intro-pattern When having a conclusion of the form "forall x, E[x]", the intro-pattern [#] was renaming `x` as `_`. Internal: low-level intro tactic that returns the generated intro name fix #221 | 09 July 2022, 05:29:53 UTC |
| 878cd49 | Pierre-Yves Strub | 29 June 2022, 16:01:28 UTC | Dependent version of the multi-rnd tactic | 29 June 2022, 16:17:08 UTC |
| 9d00961 | Pierre-Yves Strub | 29 June 2022, 14:02:08 UTC | Extend `rnd` tactic s.t. it can handle multiple samplings / assignments Syntax is `rnd ... : pos1 pos2` and is only evailable for the pRHL variant. The tactic will first collapse all the instructions after `pos1` / `pos2` (in the left/right programs) before applying the `rnd` tactic. It is also possible to access this collapse phase with the new `rndsem` tactic. The syntax is: `rndsem side? codepos` | 29 June 2022, 14:12:18 UTC |
| f6ca7bf | Pierre-Yves Strub | 29 June 2022, 09:13:11 UTC | remove "rnd := f" syntax | 29 June 2022, 14:12:18 UTC |
| dafa224 | Alley Stoughton | 28 June 2022, 16:48:30 UTC | Switched from x <> y being expanded by the parser to ! (x = y), and consequently having several explicit parsing rules (including one involving using it as a constructor in a match, which was buggy) to removing the special parsing treatment and adding it as an abbreviation. fixes #217 | 28 June 2022, 17:03:43 UTC |
