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 |
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 |
b386764 | Pierre-Yves Strub | 18 February 2022, 22:23:17 UTC | fix merge | 18 February 2022, 22:23:17 UTC |
721cc18 | Pierre-Yves Strub | 18 February 2022, 22:23:00 UTC | Merge branch 'deploy-cost-1.0-preview' into deploy-quantum | 18 February 2022, 22:23:00 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 |
b71782f | Adrien Koutsos | 18 February 2022, 10:27:03 UTC | minor | 18 February 2022, 10:27:03 UTC |
c3251b6 | Adrien Koutsos | 18 February 2022, 08:59:35 UTC | fixed example | 18 February 2022, 08:59:35 UTC |
53150bb | Adrien Koutsos | 17 February 2022, 17:15:48 UTC | fixed parser | 17 February 2022, 17:15:48 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 |
76d410e | Adrien Koutsos | 14 February 2022, 17:35:58 UTC | 1.0 version of SDist with fixed syntax | 14 February 2022, 17:35:58 UTC |
222efc5 | Adrien Koutsos | 14 February 2022, 16:49:04 UTC | 1.0 versions of Hybird.ec and Indist.ec, with updated syntax | 14 February 2022, 16:49:04 UTC |
5532145 | Adrien Koutsos | 14 February 2022, 16:37:06 UTC | new syntax | 14 February 2022, 16:37:06 UTC |
56084f8 | Adrien Koutsos | 14 February 2022, 16:32:50 UTC | change Ideal.ec to the version in 1.0 | 14 February 2022, 16:32:50 UTC |
ec7f718 | Adrien Koutsos | 14 February 2022, 16:27:02 UTC | [WIP] merge | 14 February 2022, 16:27:02 UTC |
f933dd7 | Adrien Koutsos | 11 February 2022, 16:18:14 UTC | minor | 11 February 2022, 16:18:14 UTC |
d123580 | Adrien Koutsos | 11 February 2022, 15:43:31 UTC | [WIP] fixing examples and theories | 11 February 2022, 15:43:31 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 |
1235685 | Benjamin Gregoire | 13 December 2021, 08:56:53 UTC | add lemma on dfun + remove admit | 13 December 2021, 08:56:53 UTC |
459d7f3 | Benjamin Gregoire | 13 December 2021, 08:50:20 UTC | add lemma on dfun | 13 December 2021, 08:50:20 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 |
664aa8b | Pierre-Yves Strub | 09 December 2021, 16:00:07 UTC | Merge branch '1.0' into deploy-cost-1.0-preview | 09 December 2021, 16:00:07 UTC |
a725928 | Pierre-Yves Strub | 09 December 2021, 15:27:54 UTC | Merge branch '1.0' into deploy-cost-1.0-preview | 09 December 2021, 15:27:54 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 |
2e815c5 | Pierre-Yves Strub | 02 December 2021, 06:15:54 UTC | PROM: add a ROmap interface for RO + access to the internal map | 02 December 2021, 07:48:19 UTC |
dda8233 | Pierre-Yves Strub | 02 December 2021, 07:45:45 UTC | CI / Zulip | 02 December 2021, 07:46:33 UTC |
f66167f | François Dupressoir | 26 November 2021, 11:56:31 UTC | [dune] add abstract theories to install list | 26 November 2021, 15:00:50 UTC |
b37b762 | Pierre-Yves Strub | 23 November 2021, 16:58:42 UTC | Prototype implementation of a match statement. | 23 November 2021, 16:58:42 UTC |
f5c749c | Benjamin Gregoire | 23 November 2021, 07:49:01 UTC | fix default.nix | 23 November 2021, 07:49:25 UTC |
f8514a6 | Pierre-Yves Strub | 22 November 2021, 17:48:42 UTC | remove ocamlbuild.ml | 22 November 2021, 17:48:42 UTC |
50dae1b | Pierre-Yves Strub | 21 November 2021, 16:30:31 UTC | [build] install runtest (as ec-runtest) | 21 November 2021, 16:30:31 UTC |
3476312 | Pierre-Yves Strub | 19 November 2021, 10:53:40 UTC | script for graphing a dependency graph for .eco | 19 November 2021, 10:53:40 UTC |
08ed0c2 | Pierre-Yves Strub | 19 November 2021, 07:18:43 UTC | New format for eco (v3) Store whether a theory has been directly required or not. | 19 November 2021, 07:18:46 UTC |
471ea3b | Pierre-Yves Strub | 19 November 2021, 07:03:57 UTC | foo | 19 November 2021, 07:04:08 UTC |
a549eb4 | Pierre-Yves Strub | 19 November 2021, 06:23:34 UTC | Add an option to define opaque operators This can be done by adding the "opaque" tag, e.g.: op [opaque] myop = ... solve #94 | 19 November 2021, 06:27:09 UTC |
10e1563 | Pierre-Yves Strub | 19 November 2021, 06:09:01 UTC | remove \# files | 19 November 2021, 06:09:01 UTC |
ffe0656 | Pierre-Yves Strub | 18 November 2021, 14:23:49 UTC | New command: locate [partial-qualid] This command allows to locate and print the fullname & shortest name of an operator, a lemma or a type declaration. fix #82 | 18 November 2021, 14:23:49 UTC |
92f23db | Pierre-Yves Strub | 18 November 2021, 12:06:18 UTC | Add the project name in dune-project This is needed by "dune subst" ref #99 | 18 November 2021, 12:06:45 UTC |
5e3929a | Pierre-Yves Strub | 18 November 2021, 12:06:09 UTC | remove debugging code | 18 November 2021, 12:06:09 UTC |
17e143c | Pierre-Yves Strub | 17 November 2021, 15:41:35 UTC | | 17 November 2021, 15:41:35 UTC |
b38a5aa | Pierre-Yves Strub | 17 November 2021, 15:39:37 UTC | | 17 November 2021, 15:39:37 UTC |
dfb413d | Pierre-Yves Strub | 17 November 2021, 15:35:07 UTC | fix opam package (do not do "dune subst") | 17 November 2021, 15:35:07 UTC |
0a2d4ad | Pierre-Yves Strub | 17 November 2021, 07:42:42 UTC | [build] use dune to install & find resources | 17 November 2021, 08:23:14 UTC |
31ce231 | François Dupressoir | 06 November 2019, 20:46:14 UTC | [SmtMap] add has, find and some lemmas these are focused on a specific proof and deserve expanding, fleshing out and cleaning up | 17 November 2021, 07:51:50 UTC |
229ac7a | Pierre-Yves Strub | 17 November 2021, 06:24:47 UTC | Remove EcFortune | 17 November 2021, 06:24:47 UTC |
02082bd | Pierre-Yves Strub | 17 November 2021, 06:22:22 UTC | Update copyright | 17 November 2021, 06:22:22 UTC |
e7d401f | Pierre-Yves Strub | 17 November 2021, 05:59:48 UTC | remove the script for creating tarballs | 17 November 2021, 06:01:10 UTC |
e46ef74 | Pierre-Yves Strub | 17 November 2021, 05:57:03 UTC | disable warning as errors | 17 November 2021, 05:57:03 UTC |
a54cec2 | Pierre-Yves Strub | 17 November 2021, 05:52:23 UTC | remove deprecated functions and reenable warning 3 | 17 November 2021, 05:52:23 UTC |
b7a2ee2 | Pierre-Yves Strub | 17 November 2021, 05:43:59 UTC | reenable warning 39 | 17 November 2021, 05:43:59 UTC |
4217836 | Pierre-Yves Strub | 17 November 2021, 05:41:36 UTC | reenable warning 38 | 17 November 2021, 05:41:36 UTC |
061e164 | Pierre-Yves Strub | 17 November 2021, 05:40:28 UTC | reenable warning 35 | 17 November 2021, 05:40:28 UTC |
43a1b9f | Pierre-Yves Strub | 17 November 2021, 05:39:00 UTC | reenable warning 34 | 17 November 2021, 05:39:17 UTC |
5b09921 | Pierre-Yves Strub | 17 November 2021, 05:34:48 UTC | reenable warning 6 | 17 November 2021, 05:34:48 UTC |
003fc41 | Pierre-Yves Strub | 17 November 2021, 05:34:23 UTC | [build] only consider src/theories/examples are deps | 17 November 2021, 05:34:23 UTC |
df78b65 | Pierre-Yves Strub | 17 November 2021, 05:34:13 UTC | .gitignore (.eca at root) | 17 November 2021, 05:34:13 UTC |