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 |
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 |
cec6716 | Pierre-Yves Strub | 11 June 2022, 06:10:21 UTC | 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 | Pierre-Yves Strub | 11 June 2022, 06:01:44 UTC | 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 | Pierre-Yves Strub | 10 June 2022, 09:40:59 UTC | Clear the blocked signals mask on startup. In some circumstances, the inherited mask disturbs Why3 server. | 10 June 2022, 09:40:59 UTC |
7fed186 | Pierre-Yves Strub | 04 June 2022, 11:20:29 UTC | new command: exit (stops EasyCrypt) | 04 June 2022, 11:20:29 UTC |
4e97480 | Pierre-Yves Strub | 03 June 2022, 12:06:31 UTC | [runtest]: use all cores by default | 03 June 2022, 12:06:38 UTC |
0ea3d99 | Quentin Carbonneaux | 02 June 2022, 08:54:48 UTC | 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 | Pierre-Yves Strub | 01 June 2022, 06:32:41 UTC | [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 | Adrien Koutsos | 20 May 2022, 13:26:31 UTC | smt option to dump a smt query to a file | 20 May 2022, 14:00:39 UTC |
90826b1 | Vincent Laporte | 18 May 2022, 22:23:30 UTC | default.nix: use why3 1.5.0 | 19 May 2022, 08:16:49 UTC |
b44893a | Pierre-Yves Strub | 17 May 2022, 15:17:18 UTC | [runtest]: exit with a non-zero exit status in case of failure. | 18 May 2022, 05:22:28 UTC |
168c6d7 | Pierre-Yves Strub | 17 May 2022, 15:16:35 UTC | [runtest]: do not display warnings/infos as errors Fix #198 | 18 May 2022, 05:22:28 UTC |
3c1476b | Alley Stoughton | 17 May 2022, 13:54:38 UTC | Fix pretty-printing of projections. Former printer was using an invalid priority for projections. Fixes #200 | 17 May 2022, 14:43:37 UTC |
24b0ce7 | Alley Stoughton | 16 May 2022, 17:16:29 UTC | Updating README for current why3 requirements. | 17 May 2022, 08:36:55 UTC |
762988d | François Dupressoir | 16 May 2022, 09:27:43 UTC | mark `transpose` as parse-only We have suffered long enough | 16 May 2022, 09:27:43 UTC |
b44bcba | Pierre-Yves Strub | 14 May 2022, 21:49:26 UTC | [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 | Pierre-Yves Strub | 14 May 2022, 21:39:35 UTC | [stdlib] new lemmas around dscalar & dlet. | 14 May 2022, 21:58:53 UTC |
b66eb5c | Pierre-Yves Strub | 14 May 2022, 21:38:13 UTC | [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 | Pierre-Yves Strub | 09 May 2022, 12:13:47 UTC | New `runtest` script - more readable output (for tty / no-tty) - more readable report | 14 May 2022, 21:49:14 UTC |
c629679 | Pierre-Yves Strub | 14 May 2022, 21:32:09 UTC | 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 | Pierre-Yves Strub | 13 May 2022, 07:23:39 UTC | README: remove "make PREFIX=" | 13 May 2022, 07:23:39 UTC |
a76ddc7 | Pierre-Yves Strub | 13 May 2022, 07:23:18 UTC | README: configuration Why3 using EasyCrypt | 13 May 2022, 07:23:18 UTC |
5ff9d70 | Pierre-Yves Strub | 13 May 2022, 07:18:32 UTC | When configuring Why3, create the configuration file destination directory first | 13 May 2022, 07:18:32 UTC |
92941b1 | Pierre-Yves Strub | 12 May 2022, 06:59:09 UTC | [stdlib]: link Finite & FinType. | 12 May 2022, 07:12:12 UTC |
1e12363 | François Dupressoir | 11 May 2022, 13:32:14 UTC | 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 | François Dupressoir | 12 May 2022, 06:47:58 UTC | 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 | Christian Doczkal | 11 May 2022, 08:47:50 UTC | [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 | Pierre-Yves Strub | 10 May 2022, 12:14:09 UTC | 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 | Pierre-Yves Strub | 09 May 2022, 10:46:10 UTC | Finite.to_seq: now have a body based on choiceb Co-authored-by: Christian Doczkal <christian.doczkal@mpi-sp.org> | 09 May 2022, 11:54:13 UTC |
a49a0ac | Pierre-Yves Strub | 05 May 2022, 06:55:44 UTC | Bump Why3 version from 1.4.x to 1.5.0 fix #184 | 05 May 2022, 13:58:12 UTC |
a1eeaf0 | Pierre-Yves Strub | 05 May 2022, 08:02:38 UTC | [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 | Pierre-Yves Strub | 27 April 2022, 12:46:45 UTC | Use local configuration file in priority | 27 April 2022, 12:46:45 UTC |
dbdca26 | Pierre-Yves Strub | 27 April 2022, 12:46:13 UTC | Fic computation of source root for local builds | 27 April 2022, 12:46:13 UTC |
577c882 | Pierre-Yves Strub | 27 April 2022, 09:41:00 UTC | Fix the license announced in the banner | 27 April 2022, 09:48:51 UTC |
8f314e4 | Pierre-Yves Strub | 26 April 2022, 08:49:07 UTC | Makefile | 26 April 2022, 08:49:07 UTC |
89df8ee | Adrien Koutsos | 25 April 2022, 15:42:10 UTC | move cost axioms in abstract theories (fix #175) | 26 April 2022, 08:43:31 UTC |
9c03562 | François Dupressoir | 11 January 2022, 16:03:51 UTC | Reject `x <- RHS` when `RHS` is a procedure call | 22 April 2022, 11:13:38 UTC |
7b70089 | François Dupressoir | 14 December 2021, 15:43:15 UTC | Improve parser for anonymous proc parameters Anonymous and named parameters can be mixed for abstract procedures. Corner cases are not exercised by test suites and may crop up. Resolves #108. | 22 April 2022, 10:53:46 UTC |
74a4d02 | Pierre-Yves Strub | 30 March 2022, 09:20:02 UTC | Fixing list of authors | 22 April 2022, 06:59:36 UTC |
2c53183 | Pierre-Yves Strub | 07 April 2022, 16:12:18 UTC | [env]: fully head-norm the type before fetching its top-level decl. This commit involves a lot of code motion. partially address #121 | 22 April 2022, 06:59:22 UTC |
bfd4f84 | Pierre-Yves Strub | 07 April 2022, 15:11:17 UTC | [reduction]: in cbv, fix handling of stack arguments The API was s.t. it was possibly to detect a non-empty stack as an empty one. Partially address #121 | 22 April 2022, 06:59:22 UTC |
ecb156d | Adrien Koutsos | 08 April 2022, 08:53:32 UTC | error message if cost information are missing in the call tactic | 08 April 2022, 19:27:18 UTC |
4dec70e | Adrien Koutsos | 07 April 2022, 09:18:51 UTC | Fix typing of modules expressions fix #171 | 07 April 2022, 09:47:53 UTC |
ae4fe92 | Pierre-Yves Strub | 05 April 2022, 10:25:31 UTC | [reduction]: use symmetric "and" when reducing tuples equality fix #171 | 05 April 2022, 10:59:53 UTC |
d5941d0 | Adrien Koutsos | 31 March 2022, 13:49:34 UTC | pretty printer improvements for module restrs + local memtypes | 31 March 2022, 15:38:14 UTC |
3491166 | Alley Stoughton | 31 March 2022, 13:16:44 UTC | Remove superflous renamings fixes #146 | 31 March 2022, 13:49:22 UTC |
98fbc44 | Pierre-Yves Strub | 31 March 2022, 06:36:38 UTC | [tactic]: [proc*]: fix procedure's arguments substitution Instead of introduce a single variable for the arguments tuple, introduce all the procedure's arguments as single program variables. Fix #166 | 31 March 2022, 07:49:56 UTC |
29061b7 | François Dupressoir | 30 March 2022, 12:32:24 UTC | [chore] update theories/dune | 30 March 2022, 12:32:24 UTC |
0b0aa5d | Pierre-Yves Strub | 29 March 2022, 18:47:14 UTC | [tactic]: [rewrite]: support for multi-rules `rewrite h` with `h : eq1 /\ eq2 /\ ... /\ eqn` is equivalent to `rewrite ?(h1, h2, ..., hn)` with `hi : eqi` address #155 | 30 March 2022, 08:50:08 UTC |
f876954 | Pierre-Yves Strub | 29 March 2022, 08:01:08 UTC | License change: CeCILL B/C -> MIT | 29 March 2022, 19:39:31 UTC |
b229a87 | Christian Doczkal | 24 March 2022, 12:11:19 UTC | dopt: extend subdistribution to lossless distributions on options | 29 March 2022, 14:19:04 UTC |
1a754ad | Pierre-Yves Strub | 29 March 2022, 08:23:24 UTC | [tactic]: in `apply... in...`, check that all variables are instantiated fix #149 | 29 March 2022, 09:05:09 UTC |
7a93224 | Pierre-Yves Strub | 28 March 2022, 16:59:08 UTC | [build]: [dune]: auto-generation of theories/dune | 28 March 2022, 17:07:06 UTC |
a9748f7 | Adrien Koutsos | 28 March 2022, 09:19:38 UTC | New logic to upper-bound the worst-case complexity of programs ** Breaking change: - to be consistent with oracle calls restrictions, negative memory restrictions are now set using a minus symbol (e.g. `(M <: T {-H})` instead of `(M <: T {H})`). - use `pragma +old_mem_restr` to retrieve old behaviour on memory restrictions ** Additions: - added a new hoare logic for cost, using predicates of the form `choare [H.f: pre ==> post] time [c]`, meaning: from any initial memory satisfying `pre`, the final memory obtained after the execution of `H.f` satisfies `post`, in time at most `c` - in choare predicates, the cost `c` is a cost-vector, comprising: + a concrete cost of type `xint`, where `xint` is a algebraic data-type with two constructors, `N of int` (for bounded running times) and `Inf` (for potentially unbounded running times). + a list of abstract procedures together with an integer indicated the number of times they can be called (e.g. `ROM.o : 42`). - complexity restrictions can be attached to module types procedures, restricting their instantiations. - added a new predicate, `cost`, to establish the cost of evaluating an expression (while `choare` upper-bound the cost of a statement). - (small) examples showing how to use the cost hoare logic can be found in the sub-directory `examples/cost/` - more advanced examples, using a new UC framework in EasyCrypt, can be found in `examples/UC/composition_cost.ec` `examples/UC/dh_enc_cost.ec` | 28 March 2022, 10:45:44 UTC |
b13fb54 | MM | 15 March 2022, 09:19:03 UTC | Add lemmas divzMr and divzMl; strenghten and prove modz_pow2_div. | 17 March 2022, 20:33:03 UTC |
3646dd8 | Oskar Goldhahn | 11 March 2022, 21:20:30 UTC | changed name of lemma | 12 March 2022, 10:06:23 UTC |