3f4a0bd | 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 | 13 June 2022, 09:22:31 UTC |
b9af81d | 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. | 13 June 2022, 09:22:31 UTC |
83417f0 | 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. | 13 June 2022, 08:33:47 UTC |
d44bc68 | Pierre-Yves Strub | 04 June 2022, 11:20:29 UTC | new command: exit (stops EasyCrypt) | 13 June 2022, 08:33:47 UTC |
ddf82fe | Pierre-Yves Strub | 03 June 2022, 12:06:31 UTC | [runtest]: use all cores by default | 13 June 2022, 08:33:47 UTC |
963c9e3 | 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. | 13 June 2022, 08:33:47 UTC |
f7adef3 | 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. | 13 June 2022, 08:33:47 UTC |
e717abd | Adrien Koutsos | 20 May 2022, 13:26:31 UTC | smt option to dump a smt query to a file | 13 June 2022, 08:33:47 UTC |
b4dc5af | Vincent Laporte | 18 May 2022, 22:23:30 UTC | default.nix: use why3 1.5.0 | 13 June 2022, 08:33:47 UTC |
30da1ec | Pierre-Yves Strub | 17 May 2022, 15:17:18 UTC | [runtest]: exit with a non-zero exit status in case of failure. | 13 June 2022, 08:33:47 UTC |
50b36d0 | Pierre-Yves Strub | 17 May 2022, 15:16:35 UTC | [runtest]: do not display warnings/infos as errors Fix #198 | 13 June 2022, 08:33:47 UTC |
38e640d | 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 | 13 June 2022, 08:33:47 UTC |
f5ea865 | Alley Stoughton | 16 May 2022, 17:16:29 UTC | Updating README for current why3 requirements. | 13 June 2022, 08:33:47 UTC |
12c9168 | François Dupressoir | 16 May 2022, 09:27:43 UTC | mark `transpose` as parse-only We have suffered long enough | 13 June 2022, 08:33:47 UTC |
86a6ffb | 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. | 13 June 2022, 08:33:47 UTC |
90b7c63 | Pierre-Yves Strub | 14 May 2022, 21:39:35 UTC | [stdlib] new lemmas around dscalar & dlet. | 13 June 2022, 08:33:47 UTC |
c79e18e | 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". | 13 June 2022, 08:33:47 UTC |
a5633b1 | Pierre-Yves Strub | 09 May 2022, 12:13:47 UTC | New `runtest` script - more readable output (for tty / no-tty) - more readable report | 13 June 2022, 08:33:47 UTC |
611f991 | 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. | 13 June 2022, 08:33:47 UTC |
75c489d | Pierre-Yves Strub | 13 May 2022, 07:23:39 UTC | README: remove "make PREFIX=" | 13 June 2022, 08:33:47 UTC |
3e364fa | Pierre-Yves Strub | 13 May 2022, 07:23:18 UTC | README: configuration Why3 using EasyCrypt | 13 June 2022, 08:33:47 UTC |
d1dfe94 | Pierre-Yves Strub | 13 May 2022, 07:18:32 UTC | When configuring Why3, create the configuration file destination directory first | 13 June 2022, 08:33:47 UTC |
d0b1178 | Pierre-Yves Strub | 12 May 2022, 06:59:09 UTC | [stdlib]: link Finite & FinType. | 13 June 2022, 08:33:47 UTC |
909cfa1 | 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 | 13 June 2022, 08:33:45 UTC |
96cdc83 | 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 | 13 June 2022, 08:30:51 UTC |
194eca8 | 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. | 13 June 2022, 08:29:57 UTC |
058aeeb | Adrien Koutsos | 12 May 2022, 17:14:27 UTC | progress in composition cost | 12 May 2022, 17:14:27 UTC |
1f7d4a7 | Adrien Koutsos | 12 May 2022, 16:19:56 UTC | cleaned-up various cost (in particular epoch-related) todos | 12 May 2022, 16:19:56 UTC |
e8473ba | Adrien Koutsos | 12 May 2022, 10:08:50 UTC | simplification rules of cost comparison based on epochs | 12 May 2022, 10:19:49 UTC |
f4b4c0f | Adrien Koutsos | 11 May 2022, 17:11:58 UTC | [WIP] cost simplification using epochs | 11 May 2022, 17:11:58 UTC |
af6a0ed | Adrien Koutsos | 11 May 2022, 16:03:59 UTC | fix subtyping bug | 11 May 2022, 16:03:59 UTC |
2fdc6e1 | Adrien Koutsos | 11 May 2022, 15:45:31 UTC | fixed: refresh module instead of module substitution | 11 May 2022, 15:45:31 UTC |
0853556 | Adrien Koutsos | 11 May 2022, 15:08:17 UTC | check that CHoare is loaded before generating proof obligation. | 11 May 2022, 15:08:17 UTC |
163c0a0 | Adrien Koutsos | 11 May 2022, 10:05:32 UTC | added epoch in local declarations | 11 May 2022, 10:05:32 UTC |
b6602ec | 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, 13:34:29 UTC |
eedf9d2 | 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> | 10 May 2022, 13:34:29 UTC |
c7851aa | Pierre-Yves Strub | 05 May 2022, 06:55:44 UTC | Bump Why3 version from 1.4.x to 1.5.0 fix #184 | 10 May 2022, 13:34:29 UTC |
b753c9f | 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 | 10 May 2022, 13:34:29 UTC |
f1093b8 | Pierre-Yves Strub | 27 April 2022, 12:46:45 UTC | Use local configuration file in priority | 10 May 2022, 13:34:29 UTC |
260f326 | Pierre-Yves Strub | 27 April 2022, 12:46:13 UTC | Fic computation of source root for local builds | 10 May 2022, 13:34:29 UTC |
1368273 | Pierre-Yves Strub | 27 April 2022, 09:41:00 UTC | Fix the license announced in the banner | 10 May 2022, 13:34:29 UTC |
f3071a1 | Adrien Koutsos | 09 May 2022, 16:45:49 UTC | refactoring: local declarations are now records | 09 May 2022, 16:45:49 UTC |
65e3be8 | Adrien Koutsos | 05 May 2022, 16:44:46 UTC | tentative new technique to make complexity proof obligation still work in progress | 05 May 2022, 16:44:46 UTC |
8352f49 | Adrien Koutsos | 05 May 2022, 14:49:26 UTC | add test file for cost | 05 May 2022, 14:49:26 UTC |
28c4bf8 | Adrien Koutsos | 05 May 2022, 14:46:47 UTC | destruct_cost using hypothesis | 05 May 2022, 14:46:47 UTC |
d411922 | Adrien Koutsos | 05 May 2022, 13:39:01 UTC | started to adapt the composition cost proof | 05 May 2022, 13:39:01 UTC |
4335cc5 | Adrien Koutsos | 05 May 2022, 13:06:40 UTC | fixed bad implicit arguments for cost call rule | 05 May 2022, 13:06:40 UTC |
94dcd47 | Adrien Koutsos | 05 May 2022, 11:36:12 UTC | fixed issue with infinite intrinsic cost infinite intrinsic cost was absorbing oracle call constraints | 05 May 2022, 11:36:12 UTC |
c13099e | Adrien Koutsos | 04 May 2022, 10:18:31 UTC | rules to prove subcond side-conditions | 04 May 2022, 11:30:55 UTC |
2312419 | Adrien Koutsos | 04 May 2022, 09:19:19 UTC | removed projection over concrete cost, which is unsound. | 04 May 2022, 09:22:07 UTC |
29b926f | Adrien Koutsos | 04 May 2022, 07:49:37 UTC | added additional opacity check in LowGoal | 04 May 2022, 07:49:37 UTC |
4015176 | Adrien Koutsos | 03 May 2022, 15:22:13 UTC | abstract module now have an opacity, giving their cost when called The opacity of a module is either Opaque (default) or Open. Essentially, the opacity tells what is the intrinsic cost of an abstract module when it is called. If `A` has type `M[f : [c, ...]]` then: - if A module type is opaque, then calling A.f costs `[A.f : '1]` - if A module type is open, then calling A.f costs `c` Opacity is denoted by adding the `open` or `opaque` keyword in a module complexity restriction, e.g. `M[open f : ...]`. No explicit opacity means Opaque. | 03 May 2022, 15:22:13 UTC |
17ae2d3 | Adrien Koutsos | 29 April 2022, 15:32:59 UTC | better printing + work on costs | 29 April 2022, 15:32:59 UTC |
f37b697 | Adrien Koutsos | 29 April 2022, 12:35:53 UTC | bigcost morphism rule added to reduce_logic | 29 April 2022, 12:41:50 UTC |
163abd8 | Adrien Koutsos | 29 April 2022, 09:31:14 UTC | printing: better alignement in cost vectors | 29 April 2022, 09:31:14 UTC |
6ab4890 | Adrien Koutsos | 29 April 2022, 08:43:58 UTC | simplifications of choare statements | 29 April 2022, 08:43:58 UTC |
f37eff5 | Adrien Koutsos | 28 April 2022, 16:54:57 UTC | removed projection over abstract procedures, which is unsound | 28 April 2022, 16:54:57 UTC |
e399dc5 | Adrien Koutsos | 27 April 2022, 23:09:11 UTC | new cost axiom | 27 April 2022, 23:09:11 UTC |
2055e8f | Adrien Koutsos | 27 April 2022, 17:08:08 UTC | minor | 27 April 2022, 17:08:08 UTC |
c3146c2 | Adrien Koutsos | 27 April 2022, 17:08:03 UTC | cleanup | 27 April 2022, 17:08:03 UTC |
3a46371 | Adrien Koutsos | 27 April 2022, 17:07:53 UTC | fixed cost librairies | 27 April 2022, 17:07:53 UTC |
db88428 | Adrien Koutsos | 27 April 2022, 14:27:46 UTC | fix projection printing | 27 April 2022, 14:27:46 UTC |
89f954e | Adrien Koutsos | 27 April 2022, 14:05:40 UTC | can parse projections | 27 April 2022, 14:05:40 UTC |
753f746 | Adrien Koutsos | 27 April 2022, 09:59:18 UTC | fixed `hint simplify` usage for cost theory also moved axiom out of pervasive | 27 April 2022, 09:59:18 UTC |
91761d1 | Adrien Koutsos | 27 April 2022, 09:49:14 UTC | better form dumping | 27 April 2022, 09:49:14 UTC |
324ba73 | Pierre-Yves Strub | 26 April 2022, 08:49:07 UTC | Makefile | 26 April 2022, 16:46:37 UTC |
2dabde1 | Adrien Koutsos | 25 April 2022, 15:42:10 UTC | move cost axioms in abstract theories (fix #175) | 26 April 2022, 16:46:15 UTC |
5d283f2 | François Dupressoir | 11 January 2022, 16:03:51 UTC | Reject `x <- RHS` when `RHS` is a procedure call | 26 April 2022, 16:42:47 UTC |
7e0f6ba | 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. | 26 April 2022, 16:42:12 UTC |
20564b5 | Pierre-Yves Strub | 30 March 2022, 09:20:02 UTC | Fixing list of authors | 26 April 2022, 16:35:39 UTC |
716f354 | 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 | 26 April 2022, 16:35:39 UTC |
8abdc7d | 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 | 26 April 2022, 16:35:39 UTC |
3aee866 | Adrien Koutsos | 08 April 2022, 08:53:32 UTC | error message if cost information are missing in the call tactic | 26 April 2022, 16:35:18 UTC |
44a632c | Adrien Koutsos | 07 April 2022, 09:18:51 UTC | Fix typing of modules expressions fix #171 | 26 April 2022, 16:33:30 UTC |
a5de7bc | Pierre-Yves Strub | 05 April 2022, 10:25:31 UTC | [reduction]: use symmetric "and" when reducing tuples equality fix #171 | 26 April 2022, 16:33:30 UTC |
1c52e78 | Adrien Koutsos | 31 March 2022, 13:49:34 UTC | pretty printer improvements for module restrs + local memtypes | 26 April 2022, 16:33:17 UTC |
75f6941 | Alley Stoughton | 31 March 2022, 13:16:44 UTC | Remove superflous renamings fixes #146 | 26 April 2022, 16:30:56 UTC |
312ac25 | 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 | 26 April 2022, 16:30:56 UTC |
86b62e5 | François Dupressoir | 30 March 2022, 12:32:24 UTC | [chore] update theories/dune | 26 April 2022, 16:30:56 UTC |
7dbdbe0 | 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 | 26 April 2022, 16:30:56 UTC |
32578da | Pierre-Yves Strub | 29 March 2022, 08:01:08 UTC | License change: CeCILL B/C -> MIT | 26 April 2022, 16:30:22 UTC |
a307890 | Christian Doczkal | 24 March 2022, 12:11:19 UTC | dopt: extend subdistribution to lossless distributions on options | 26 April 2022, 16:29:04 UTC |
47a2f63 | Pierre-Yves Strub | 29 March 2022, 08:23:24 UTC | [tactic]: in `apply... in...`, check that all variables are instantiated fix #149 | 26 April 2022, 16:29:04 UTC |
53651e1 | Pierre-Yves Strub | 28 March 2022, 16:59:08 UTC | [build]: [dune]: auto-generation of theories/dune | 26 April 2022, 16:29:04 UTC |
5dd9a9c | Adrien Koutsos | 11 April 2022, 09:12:40 UTC | improved substitution API for module idents | 11 April 2022, 09:12:40 UTC |
50961c7 | Adrien Koutsos | 08 April 2022, 09:39:43 UTC | fix: use the functor to retrieve the cost information and not the applied module | 08 April 2022, 09:41:52 UTC |
6cabd84 | Adrien Koutsos | 16 March 2022, 09:45:03 UTC | comments + assert | 16 March 2022, 09:45:03 UTC |
3466266 | Adrien Koutsos | 15 March 2022, 17:44:34 UTC | minor | 15 March 2022, 17:44:34 UTC |
905023b | Adrien Koutsos | 15 March 2022, 17:09:54 UTC | Merge branch 'deploy-cost-1.0-preview' into deploy-new-cost | 15 March 2022, 17:09:54 UTC |
45559bb | Adrien Koutsos | 15 March 2022, 15:38:15 UTC | [WIP] | 15 March 2022, 15:43:37 UTC |
9108d72 | Adrien Koutsos | 15 March 2022, 15:12:18 UTC | [WIP] | 15 March 2022, 15:12:18 UTC |
c3be289 | Adrien Koutsos | 15 March 2022, 12:49:19 UTC | [WIP] | 15 March 2022, 12:49:19 UTC |
a0fed93 | Adrien Koutsos | 14 March 2022, 18:57:39 UTC | [WIP] | 14 March 2022, 18:57:39 UTC |
928152b | Adrien Koutsos | 14 March 2022, 17:18:57 UTC | subst: distinguish between refreshing module and instantiating | 14 March 2022, 17:18:57 UTC |
b93754a | Adrien Koutsos | 14 March 2022, 15:02:48 UTC | fixed hashed elgamal | 14 March 2022, 15:02:48 UTC |
aa86882 | Oskar Goldhahn | 11 March 2022, 21:20:30 UTC | changed name of lemma | 14 March 2022, 13:40:02 UTC |
c502b6b | Oskar Goldhahn | 11 March 2022, 18:14:23 UTC | added stronger version of dmap1E_can | 14 March 2022, 13:40:02 UTC |
6f177e1 | Adrien Koutsos | 14 March 2022, 13:38:34 UTC | pragma to retrieve the old behaviour on memory restrictions | 14 March 2022, 13:40:02 UTC |
2a9c1a7 | Adrien Koutsos | 13 March 2022, 07:40:36 UTC | smart constructors for module type and module sigs | 13 March 2022, 07:40:36 UTC |
15d9859 | Adrien Koutsos | 10 March 2022, 14:38:50 UTC | [WIP] substitution in module types | 10 March 2022, 14:38:50 UTC |