| 5489c23 | Pierre-Yves Strub | 29 June 2022, 16:01:28 UTC | Dependent version of the multi-rnd tactic | 29 June 2022, 16:01:28 UTC |
| 34819c4 | Pierre-Yves Strub | 29 June 2022, 14:56:03 UTC | fix merge | 29 June 2022, 14:56:03 UTC |
| b8a1516 | Pierre-Yves Strub | 29 June 2022, 14:23:00 UTC | Merge branch 'main' into deploy-quantum | 29 June 2022, 14:23:00 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 |
| ccf8c79 | Pierre-Yves Strub | 10 June 2022, 09:42:14 UTC | Merge branch 'main' into deploy-quantum | 10 June 2022, 09:42:14 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 |
| 0efc2d9 | Pierre-Yves Strub | 08 June 2022, 12:15:51 UTC | Fix pretty-printing bug (box not closed) fix #209 | 08 June 2022, 12:15:51 UTC |
| d7e3674 | Pierre-Yves Strub | 07 June 2022, 05:25:22 UTC | more on dfun | 07 June 2022, 05:25:22 UTC |
| 9b26d2e | Pierre-Yves Strub | 05 June 2022, 14:58:05 UTC | more results on dfun | 05 June 2022, 15:00:07 UTC |
| eedb32b | Pierre-Yves Strub | 04 June 2022, 11:20:53 UTC | Merge branch 'main' into deploy-quantum | 04 June 2022, 11:20:53 UTC |
| 7fed186 | Pierre-Yves Strub | 04 June 2022, 11:20:29 UTC | new command: exit (stops EasyCrypt) | 04 June 2022, 11:20:29 UTC |
| 1dc6081 | Pierre-Yves Strub | 04 June 2022, 11:01:51 UTC | cleaning + generalizing dprodrDl | 04 June 2022, 11:01:51 UTC |
| ec94eae | Pierre-Yves Strub | 03 June 2022, 20:38:08 UTC | more on dfun | 03 June 2022, 20:38:08 UTC |
| cbbab92 | Pierre-Yves Strub | 03 June 2022, 12:06:47 UTC | Merge branch 'main' into deploy-quantum | 03 June 2022, 12:06:47 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 |
| ce4696e | Pierre-Yves Strub | 03 June 2022, 12:02:28 UTC | [stdlib]: more on dfun | 03 June 2022, 12:02:28 UTC |
| 47dbe8b | Pierre-Yves Strub | 03 June 2022, 11:50:08 UTC | Merge remote-tracking branch 'origin/deploy-quantum-hashbased' into deploy-quantum | 03 June 2022, 11:50:08 UTC |
| 0968b99 | Pierre-Yves Strub | 03 June 2022, 10:42:14 UTC | Merge branch 'main' into deploy-quantum | 03 June 2022, 10:42:14 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 |
| 1fcbf2c | Manuel Barbosa | 25 May 2022, 17:05:51 UTC | getting Word.eca to compile: commented proof* | 25 May 2022, 17:05:51 UTC |
| 1cbf7ed | Manuel Barbosa | 25 May 2022, 16:46:06 UTC | Fixing dune theories | 25 May 2022, 16:46:06 UTC |
| 352d694 | Manuel Barbosa | 25 May 2022, 16:37:30 UTC | Fixing dune theories | 25 May 2022, 16:37:30 UTC |
| 1b6f523 | Manuel Barbosa | 25 May 2022, 16:19:14 UTC | theories/datatypes/Word.eca | 25 May 2022, 16:19:14 UTC |
| dfe6020 | François Dupressoir | 14 December 2021, 12:22:51 UTC | Lemma stating equality of word and list distributions | 25 May 2022, 10:10:00 UTC |
| 45ca6cd | François Dupressoir | 30 March 2022, 12:32:24 UTC | [chore] update theories/dune | 25 May 2022, 10:06:07 UTC |
| c0a80b5 | François Dupressoir | 30 March 2022, 12:32:24 UTC | Merging dune theories | 25 May 2022, 10:05:38 UTC |
| 9d62149 | Manuel Barbosa | 24 May 2022, 18:07:40 UTC | generalized version of dfun_allE | 24 May 2022, 18:07:40 UTC |
| 9989616 | Oskar Goldhahn | 11 March 2022, 21:20:30 UTC | changed name of lemma | 24 May 2022, 17:54:42 UTC |
| 274a36d | Oskar Goldhahn | 11 March 2022, 18:14:23 UTC | added stronger version of dmap1E_can | 24 May 2022, 17:52:58 UTC |
| 44c088f | Pierre-Yves Strub | 14 May 2022, 21:49:26 UTC | merge cherry pick in Distr | 24 May 2022, 17:52:47 UTC |
| eb5164e | Pierre-Yves Strub | 14 May 2022, 21:39:35 UTC | [stdlib] new lemmas around dscalar & dlet. | 24 May 2022, 17:46:55 UTC |
| 019ac2d | 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. | 24 May 2022, 17:46:54 UTC |
| 94a67b4 | 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". | 24 May 2022, 17:44:34 UTC |
| 6175736 | Manuel Barbosa | 24 May 2022, 17:37:33 UTC | Revert "Stuff needed for hashbased" This reverts commit e02ee33759b678e14170830eedc7d8634095acfd. | 24 May 2022, 17:37:33 UTC |
| e02ee33 | Manuel Barbosa | 24 May 2022, 17:03:09 UTC | Stuff needed for hashbased | 24 May 2022, 17:03:09 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 |
| d5df8b2 | Oskar Goldhahn | 11 March 2022, 18:14:23 UTC | added stronger version of dmap1E_can | 12 March 2022, 10:06:23 UTC |
| c98b014 | Kai-Chun Ning | 03 March 2022, 15:26:36 UTC | Extend standard library (IntDiv) with core results. | 03 March 2022, 18:13:54 UTC |
| e22c918 | MM | 13 January 2022, 20:10:45 UTC | Added definition and lemmas for 'put' operator in List.ec. | 03 March 2022, 12:53:02 UTC |
| 8cfa32b | Alley Stoughton | 29 March 2021, 13:09:27 UTC | An axiom-free formalization of well-founded relations, induction and recursion. | 03 March 2022, 09:50:40 UTC |
| 6199997 | Morten Solberg | 01 March 2022, 09:53:41 UTC | Generalize `LorR` theory Generalize the `LorR` theory to make it possible to give some input to `L.main` and `R.main`. Using the theory for procedures without input is still possible by cloning the theory with type `input <- unit`. | 03 March 2022, 09:50:19 UTC |
| b06e700 | Pierre-Yves Strub | 02 March 2022, 16:27:38 UTC | Stdlib: more results on integer division & exponentiation | 02 March 2022, 16:28:09 UTC |
| c316eff | Alley Stoughton | 01 March 2022, 14:04:58 UTC | Removed redundant "rec" in function declaration. | 01 March 2022, 14:04:58 UTC |
| 77aac4b | Pierre-Yves Strub | 24 February 2022, 07:02:59 UTC | Revert "Unfold non-transparent operators in `case` & `elim`." This reverts commit 70662a755d2121ca1c809cf2eef68462bd720d72. | 24 February 2022, 07:02:59 UTC |
| 559910b | Benjamin Gregoire | 22 February 2022, 05:52:41 UTC | Partially fix memory capture in substitutions closes #130 | 22 February 2022, 09:41:14 UTC |
| ce4d8ca | François Dupressoir | 21 February 2022, 17:58:38 UTC | [dune+opam] fix git hash versioning widget | 21 February 2022, 18:24:12 UTC |
| a81d7e8 | Pierre-Yves Strub | 21 February 2022, 08:29:19 UTC | Merge branch 'deploy-cost-1.0-preview' into deploy-quantum | 21 February 2022, 08:29:19 UTC |
| 28c60b4 | Pierre-Yves Strub | 21 February 2022, 08:25:03 UTC | Merge branch '1.0' into deploy-cost-1.0-preview | 21 February 2022, 08:25:03 UTC |
