swh:1:snp:a9ad9db76f3bcf80967da2f1daef656b759b09e1

sort by:
Revision Author Date Message Commit Date
6890aca fix small bug in reduction of projection 04 February 2023, 10:59:08 UTC
472c8db 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 Unify created variables correctly. 23 January 2023, 15:43:55 UTC
2f98c08 [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 [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 runtest: ECRJOBS env. variable 05 January 2023, 13:05:38 UTC
e034e6c [internal]: fix detection of empty expression-level substitutions. 05 January 2023, 09:50:08 UTC
b1fe56d remove unused dependency (cmdliner) 04 January 2023, 14:01:27 UTC
c7ceb4f [runtest]: better display of multi-line error messages 04 January 2023, 14:01:09 UTC
ff6a4bb [runtest]: append scenarios to the CLI 04 January 2023, 13:06:36 UTC
36e617d [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 [tactic]: fix t_solve performance issues 14 December 2022, 09:49:19 UTC
f180466 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 Remove dependency to oldlibs for Group 14 December 2022, 09:46:38 UTC
d1dc434 Various bug fixes for clones (modules & lemmas) fix #292 14 December 2022, 09:23:39 UTC
ee7c5ff force delta on convertibility checks Closes #154 24 November 2022, 16:39:53 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 Ideal.ec 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/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 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 : E.foo ~ E.bar : 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
back to top