sort by:
Revision Author Date Message Commit Date
9d08a76 fix #154 24 November 2022, 16:10:02 UTC
69c9c2e add few lemmas on dfun 16 November 2022, 08:40:22 UTC
1b369f9 add theory Dfun_sub + backport many lemma from deploy-quantum 10 November 2022, 10:06:28 UTC
9f4a2f7 [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 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 add lemma mu_dlet_le : mu (dlet d F1) P1 <= mu (dlet d F2) P2 28 October 2022, 05:31:26 UTC
9c54096 generalize big_pow lemmas 27 October 2022, 12:04:41 UTC
f2011a3 telescoping_sum + sum p^i + sum i*p^i 27 October 2022, 12:04:41 UTC
6593a9e add cnvC cnv_pow 26 October 2022, 20:11:44 UTC
2df1d51 lim (x^n) = 0 26 October 2022, 17:24:14 UTC
024aa82 [stdlib] limit of a sequence of distributions 26 October 2022, 13:11:02 UTC
f36307f [stdlib]: extra properties on lim 26 October 2022, 10:47:29 UTC
d3da5af 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 Register for the pretty-printer 26 October 2022, 07:43:45 UTC
d277b49 remove admits in 21 October 2022, 16:16:34 UTC
56054fd Fix typos in user messages 19 October 2022, 06:41:28 UTC
2a75df5 port Dexcepted to dresrict and deprecate Dfilter fixes #233 18 October 2022, 09:01:45 UTC
147daa0 tactic [byupto] add missing restriction in the case of adversary. 18 October 2022, 07:19:47 UTC
638229b 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 [stdlib] bound collisions for ROmap 17 October 2022, 13:31:22 UTC
fc2bfba [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 add syntaxic upto tactic (#287) The tactic name is `byupto`. 16 October 2022, 23:52:10 UTC
9154d9a lossless for equiv 13 October 2022, 14:58:18 UTC
3d0f508 Fix new link 10 October 2022, 12:07:27 UTC
8e046e1 Fix pretty-printing of high-order postfix operators 09 October 2022, 06:24:47 UTC
ddb2336 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 Fix pretty-printing of %r 07 October 2022, 15:27:40 UTC
b2d6b7e [stdlib]: core theory conditional distributions 07 October 2022, 10:27:08 UTC
1198d07 doCheck = false, for merlin (solve a pb with ld warning on mac) 07 October 2022, 10:26:51 UTC
63e4ead [conv]: add case for program variables & globals 22 September 2022, 15:45:34 UTC
80dba47 [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 Allow quotient ring elements to be matrix entries 05 September 2022, 20:15:21 UTC
97dc179 Add camlp-streams dependency to nix build 05 September 2022, 16:48:27 UTC
be40298 [stdlib]: Matrix: coeffs in a comm. ring instead of an ID. 05 September 2022, 14:49:50 UTC
750a491 [build]: use camlp-streams This resolves the deprecation warning about the Stream module. Fix #186 05 September 2022, 08:46:47 UTC
70ac960 [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/ (starting line 299, including the conseq) and examples/ (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 <> co-authored-by: François Dupressoir <> 05 September 2022, 08:27:00 UTC
38fb166 In tactic apply[alpha]: instiantiate type-varaibles. Fix #255 05 September 2022, 08:25:14 UTC
f8c2cac Fix MEE-CBC example failing smt call 31 August 2022, 16:50:48 UTC
94be874 Remove unused PF-WP 31 August 2022, 09:58:51 UTC
7f37e97 Lemmas on dprod and djoin 30 August 2022, 09:20:18 UTC
af067ba In `cloning ... with lemma...`, disable inference for `apply` Ref #247 30 August 2022, 07:26:44 UTC
0aeaa74 Distinction between modules & module types path in the hi-level subst. Ref #247 30 August 2022, 07:26:44 UTC
c7fb3d9 Relate dbiased and dmap 29 August 2022, 13:03:15 UTC
b2273f0 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 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 Enforce section restrictions on the types of declared modules. Fix #245 23 August 2022, 12:07:34 UTC
644ddc2 Fix a typing annotation bug in distribution tags' axioms fix #241 09 August 2022, 09:00:42 UTC
1587d64 Fix unprecise/invalid error message 09 August 2022, 07:53:49 UTC
c8d3d6c [theories]: Add scalar-vector multiplication 23 July 2022, 07:07:55 UTC
fec4d5f [build]: add option -f to codesign 23 July 2022, 06:12:54 UTC
aee8bfe CI: mechanism for checking external developments Currently, this mechanism is configured to check the Jasmin ECLib 22 July 2022, 12:34:18 UTC
b184b1d theories: add back "oldlibs" in the CI + fix 19 July 2022, 14:08:51 UTC
ea77e0e add looptransform 15 July 2022, 08:36:36 UTC
53f3e84 slightly reduce reliance on trivial SMT calls 12 July 2022, 16:44:15 UTC
bef5649 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 strip out code related to proc * 12 July 2022, 16:38:49 UTC
df8a2f9 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 Hakyber jasmin eclib 12 July 2022, 09:10:25 UTC
5524b72 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 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 Dependent version of the multi-rnd tactic 29 June 2022, 16:17:08 UTC
9d00961 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 remove "rnd := f" syntax 29 June 2022, 14:12:18 UTC
dafa224 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
cec6716 In loop fusion/fission, add more constraints on the epilog Loops' epilogs must now be deterministic and loop/calls-free. This forbids the following unsoundness: ``` require import AllCore DBool. module E = { var i,j : int proc foo () = { var c; i <- 0; j <- 0; c <- false; while (!c) { i <- i + 1; j <- j + 1; c <$ {0,1}; } return i = j; } proc bar () = { var c; i <- 0; j <- 0; c <- false; while (!c) { i <- i + 1; c <$ {0,1}; } c <- false; while (!c) { j <- j + 1; c <$ {0,1}; } return i = j; } }. equiv bad : ~ : true ==> ={res}. proof. proc. fission{1} 4!1 @1,2. by sim. qed. ``` Fix #210 11 June 2022, 06:10:21 UTC
1f8da33 Add an option that allows EasyCrypt to connect to an external Why3 server The option is -why3server and takes the unix domain socket path as argument. 11 June 2022, 06:02:38 UTC
38c4947 Clear the blocked signals mask on startup. In some circumstances, the inherited mask disturbs Why3 server. 10 June 2022, 09:40:59 UTC
7fed186 new command: exit (stops EasyCrypt) 04 June 2022, 11:20:29 UTC
4e97480 [runtest]: use all cores by default 03 June 2022, 12:06:38 UTC
0ea3d99 rename depext to opam-depext The `depext` package fails to install with recent versions of opam. The fix suggested in the package information is to use the renamed package `opam-depext` instead. 02 June 2022, 11:26:56 UTC
d083fc5 [dune]: (re)-codesign promoted binaries Dune substitution breaks the initial code-signing. The problem has been acknowledge by the dune team and should be fixed on their side at some point. 01 June 2022, 06:32:41 UTC
e45a54c smt option to dump a smt query to a file 20 May 2022, 14:00:39 UTC
90826b1 default.nix: use why3 1.5.0 19 May 2022, 08:16:49 UTC
b44893a [runtest]: exit with a non-zero exit status in case of failure. 18 May 2022, 05:22:28 UTC
168c6d7 [runtest]: do not display warnings/infos as errors Fix #198 18 May 2022, 05:22:28 UTC
3c1476b Fix pretty-printing of projections. Former printer was using an invalid priority for projections. Fixes #200 17 May 2022, 14:43:37 UTC
24b0ce7 Updating README for current why3 requirements. 17 May 2022, 08:36:55 UTC
762988d mark `transpose` as parse-only We have suffered long enough 16 May 2022, 09:27:43 UTC
b44bcba [stdlib]: more lemmas around dfun. Main result is the equivalence between sampling a function and sampling a function in the same function space, but for one point that is sample a posteriori. 14 May 2022, 21:58:53 UTC
2e5cc0e [stdlib] new lemmas around dscalar & dlet. 14 May 2022, 21:58:53 UTC
b66eb5c [stdlib]: new operator for updating a function at one point. Notation is "f.[x <- v]" for the function that is equal to "f" but at value "x" where it returns "v". 14 May 2022, 21:58:45 UTC
b6f7335 New `runtest` script - more readable output (for tty / no-tty) - more readable report 14 May 2022, 21:49:14 UTC
c629679 Fix pretty-printing of mixfix notations. The notation was not printed when the operators was over-applied. E.g., f.[x <- v] y was printed "_.[_<-_]" f x v y. 14 May 2022, 21:32:09 UTC
164a167 README: remove "make PREFIX=" 13 May 2022, 07:23:39 UTC
a76ddc7 README: configuration Why3 using EasyCrypt 13 May 2022, 07:23:18 UTC
5ff9d70 When configuring Why3, create the configuration file destination directory first 13 May 2022, 07:18:32 UTC
92941b1 [stdlib]: link Finite & FinType. 12 May 2022, 07:12:12 UTC
1e12363 error on potential procedure call in RHS of <- If the RHS of a <- fails to typecheck as an expression but could be a procedure call, mention <@ as an alternative 12 May 2022, 06:49:18 UTC
5d030a1 Enforce separation between <- and <@ more strictly This removes the error message when the RHS is a procedure call. This allows us to accept things that were rejected before, when a procedure and operator share their name. A follow-up may re-enable it. Fix #189 12 May 2022, 06:49:18 UTC
cdc065e [stdlib]: add various small lemmas (Logic, FSet, Distr, DInterval, Bigop) - #non-backward-compatible: this commits generalizes `Bigop.reindex` to restrict the cancellation property to the index list. 12 May 2022, 06:43:29 UTC
de42d06 Change configuration file resolution Do not consider locations that point to non-existing files. The configuration file location is now printing by the `config` command. 10 May 2022, 12:14:09 UTC
f1ce5ae Finite.to_seq: now have a body based on choiceb Co-authored-by: Christian Doczkal <> 09 May 2022, 11:54:13 UTC
a49a0ac Bump Why3 version from 1.4.x to 1.5.0 fix #184 05 May 2022, 13:58:12 UTC
a1eeaf0 [github-action]: do not start as root This requires a modification of the docker image s.t. the user UID is compatible with the one used by Github Action 05 May 2022, 13:14:49 UTC
aab2ca4 Use local configuration file in priority 27 April 2022, 12:46:45 UTC
dbdca26 Fic computation of source root for local builds 27 April 2022, 12:46:13 UTC
577c882 Fix the license announced in the banner 27 April 2022, 09:48:51 UTC
8f314e4 Makefile 26 April 2022, 08:49:07 UTC
89df8ee move cost axioms in abstract theories (fix #175) 26 April 2022, 08:43:31 UTC
9c03562 Reject `x <- RHS` when `RHS` is a procedure call 22 April 2022, 11:13:38 UTC
back to top