e035875 | Cameron Low | 09 February 2023, 17:59:08 UTC | fixed proof. | 09 February 2023, 17:59:08 UTC |
32e0d51 | Cameron Low | 09 February 2023, 17:46:12 UTC | fixed proof. | 09 February 2023, 17:46:12 UTC |
2efbf9b | Cameron Low | 09 February 2023, 17:33:39 UTC | Dropped in rewrite equiv as much as possible. Seems to hold up fairly well. | 09 February 2023, 17:33:39 UTC |
8e047ca | Cameron Low | 09 February 2023, 12:41:21 UTC | Fixed all? the issues we had previously with post/pre conds. Things are smoother. | 09 February 2023, 12:41:21 UTC |
29ede16 | Cameron Low | 09 February 2023, 12:40:30 UTC | Added one sided goal splitting and variable finding | 09 February 2023, 12:40:30 UTC |
14f05c3 | Cameron Low | 19 January 2023, 15:38:55 UTC | Removed pos argument as a simplification before we merge. | 19 January 2023, 15:38:55 UTC |
2e60024 | Cameron Low | 19 December 2022, 16:10:44 UTC | Dropped in rewrite equiv, showcases local lemma use. | 19 December 2022, 16:10:44 UTC |
0a1a721 | Cameron Low | 08 December 2022, 09:41:13 UTC | Added extra example showcasing pre condition carry through | 08 December 2022, 09:41:13 UTC |
bd529ab | Cameron Low | 08 December 2022, 09:37:56 UTC | Added support for local lemma use, also carry the pre condition throughout. | 08 December 2022, 09:37:56 UTC |
6a16de3 | François Dupressoir | 13 June 2022, 15:46:00 UTC | Fiddling with goal generation And getting a proper-ish example through. | 13 June 2022, 15:46:00 UTC |
aef451b | François Dupressoir | 12 April 2022, 11:34:15 UTC | generate goals that work when argument/result types are different | 13 June 2022, 13:55:49 UTC |
6c65bac | François Dupressoir | 11 April 2022, 12:28:05 UTC | Parser: now takes two arg and two res expressions | 13 June 2022, 13:55:49 UTC |
fca183d | François Dupressoir | 05 April 2022, 16:28:33 UTC | Generalise parser and internal proofs slightly | 13 June 2022, 13:55:49 UTC |
9fc3ce2 | François Dupressoir | 14 March 2022, 10:43:37 UTC | Implement right-to-left | 13 June 2022, 13:55:49 UTC |
c5574b8 | François Dupressoir | 01 March 2022, 17:41:53 UTC | WIP and notes | 13 June 2022, 13:55:49 UTC |
2397c47 | François Dupressoir | 01 March 2022, 14:35:45 UTC | Fix: auto can close goals | 13 June 2022, 13:55:48 UTC |
59ffc7c | François Dupressoir | 01 March 2022, 13:55:13 UTC | First full version for {1} Kills all goals that will always be killable without smt. | 13 June 2022, 13:55:48 UTC |
60f6f72 | François Dupressoir | 24 February 2022, 18:37:13 UTC | [wip] a little bit more progress Using higher level tacticals | 13 June 2022, 13:55:48 UTC |
865dffa | François Dupressoir | 22 February 2022, 23:02:06 UTC | more WIP progress/exploration | 13 June 2022, 13:55:48 UTC |
1a224bd | François Dupressoir | 22 February 2022, 18:11:09 UTC | [wip] very minor progress and some notes | 13 June 2022, 13:55:48 UTC |
40eec71 | Pierre-Yves Strub | 22 February 2022, 17:10:40 UTC | WIP | 13 June 2022, 13:55:48 UTC |
cb70908 | François Dupressoir | 22 February 2022, 15:18:57 UTC | WIP | 13 June 2022, 13:55:48 UTC |
752e775 | François Dupressoir | 16 February 2022, 00:24:48 UTC | wip: work the pattern out | 13 June 2022, 13:55:48 UTC |
050ab54 | Pierre-Yves Strub | 15 February 2022, 17:03:24 UTC | wip | 13 June 2022, 13:55:48 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 |
f278e3c | François Dupressoir | 14 December 2021, 12:22:51 UTC | Lemma stating equality of word and list distributions | 18 February 2022, 22:51:52 UTC |
70662a7 | Pierre-Yves Strub | 18 February 2022, 22:18:29 UTC | Unfold non-transparent operators in `case` & `elim`. When `case` or `elim` search for a redex, allows the reduction to unfold non-transparent operators. This does not affect tactics that does case/elim internally (e.g., />). fix #132 | 18 February 2022, 22:18:29 UTC |
03a3fe8 | Pierre-Yves Strub | 18 February 2022, 22:18:29 UTC | Fails gracefully when applying a tactic on a completed proof. fix #133 | 18 February 2022, 22:18:29 UTC |
39b2562 | Pierre-Yves Strub | 16 February 2022, 06:38:28 UTC | Get rid of dune-site dune-site is currently in a very alpha-state and not stable enough. fix #99 fix #115 | 16 February 2022, 06:38:37 UTC |
ce56b10 | François Dupressoir | 19 January 2022, 19:29:05 UTC | Add rdirs option in config file closes #127 | 19 January 2022, 22:45:29 UTC |
46ba308 | Christian Doczkal | 14 December 2021, 09:43:58 UTC | Apply suggestions from code review Co-authored-by: Francois Dupressoir <fdupress@gmail.com> | 05 January 2022, 13:39:35 UTC |
49e768e | Christian Doczkal | 10 November 2021, 11:05:22 UTC | fix theories | 05 January 2022, 13:39:35 UTC |
e77248a | Christian Doczkal | 09 November 2021, 15:40:12 UTC | allow zero queries in Hybrid and SDist | 05 January 2022, 13:39:35 UTC |
49aec58 | Christian Doczkal | 10 December 2021, 15:21:46 UTC | lemmas on FSet, List, and DList | 10 December 2021, 17:02:37 UTC |
7df1de5 | François Dupressoir | 08 December 2021, 19:10:52 UTC | First pass: slices are inclusive | 09 December 2021, 21:39:05 UTC |
32abff2 | Christian Doczkal | 08 December 2021, 16:05:33 UTC | some lemmas on subseq, fmap, and drat | 09 December 2021, 06:26:12 UTC |
799d429 | Christian Doczkal | 08 December 2021, 12:53:47 UTC | add lemma RO_LRO and generalize RO_FinRO_D | 08 December 2021, 13:26:16 UTC |
8e47fe3 | Pierre-Yves Strub | 03 December 2021, 16:11:39 UTC | Fix bug that prevents `rewrite //= in h` to simplify in `h` Fix #68 | 03 December 2021, 16:12:21 UTC |
6a6f3b8 | Pierre-Yves Strub | 03 December 2021, 08:56:41 UTC | Merge pull request #105 from EasyCrypt/deploy-lift-lro lift LRO oracle out of FullEager | 03 December 2021, 08:56:41 UTC |
e77e653 | Christian Doczkal | 02 December 2021, 17:45:41 UTC | lift LRO oracle out of FullEager | 03 December 2021, 08:00:10 UTC |
fe9a171 | Francois Dupressoir | 03 December 2021, 05:08:44 UTC | Update ci.yml | 03 December 2021, 05:09:09 UTC |
541aa08 | Benjamin Gregoire | 02 December 2021, 10:41:39 UTC | fix substitution of modules when cloning. fix #97 | 02 December 2021, 10:41:39 UTC |
4a1ce0d | François Dupressoir | 28 November 2021, 17:26:46 UTC | [docker] Build box base is now an opam image The original base was 5 months out of date. An issue in the build was due to opam running as root. The replacement base image is setup for opam to not run as root while allowing passwordless sudo. | 02 December 2021, 08:09:28 UTC |