We are hiring ! See our job offers.
https://github.com/EasyCrypt/easycrypt
14 August 2022, 19:57:04 UTC
sort by:
Revision Author Date Message Commit Date
56a393d Pierre-Yves Strub 06 May 2022, 06:44:04 UTC [github-action]: push docker images 06 May 2022, 14:42:43 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
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
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
f8d5b79 Pierre-Yves Strub 16 November 2021, 18:32:37 UTC Merge pull request #31 from ejgallego/1.0+dune [build] Add basic dune support 16 November 2021, 18:32:37 UTC
e39463d Pierre-Yves Strub 16 November 2021, 17:37:59 UTC .gitignore: cleanup 16 November 2021, 17:37:59 UTC
68bbd4b Pierre-Yves Strub 16 November 2021, 14:59:38 UTC [nix] update dependencies 16 November 2021, 17:35:05 UTC
f7c671c Pierre-Yves Strub 16 November 2021, 14:14:36 UTC [build] use dune in Makefile 16 November 2021, 17:35:05 UTC
5334126 Pierre-Yves Strub 16 November 2021, 13:38:29 UTC [build] do not create an internal EC library we do not currently expose any stable API. 16 November 2021, 17:35:05 UTC
3f13dec Pierre-Yves Strub 16 November 2021, 13:29:42 UTC Use the old build system in opam. 16 November 2021, 17:35:04 UTC
fd804d6 Emilio Jesus Gallego Arias 22 August 2019, 15:33:19 UTC [build] Add basic dune support Add experimental support for buidling `ec` using dune. Use ``` dune build ``` We don't add support for building the stdlib yet. 16 November 2021, 17:35:04 UTC
743a247 Pierre-Yves Strub 16 November 2021, 16:53:15 UTC [ci] do not send a slack message for PR from forked repo These PR do not have access to the webhook.t 16 November 2021, 17:35:04 UTC
4b604bf Christian Doczkal 04 November 2021, 14:52:23 UTC renamings: dletE[_swap] -> dlet_muE[_swap] and dletE_mu -> dletE 16 November 2021, 17:35:04 UTC
ab62416 Christian Doczkal 24 October 2021, 10:45:16 UTC adapt to consistent use of mu1 16 November 2021, 17:35:04 UTC
15946aa Christian Doczkal 24 October 2021, 09:36:02 UTC use mu1 instead of mass in in Distr 16 November 2021, 17:35:04 UTC
5a0238b Pierre-Yves Strub 16 November 2021, 16:53:15 UTC [ci] do not send a slack message for PR from forked repo These PR do not have access to the webhook.t 16 November 2021, 16:56:20 UTC
ec1f979 Pierre-Yves Strub 09 November 2021, 16:32:05 UTC Merge pull request #88 from EasyCrypt/deploy-mu1 Consistently use `mu1` instead of `mass`. 09 November 2021, 16:32:05 UTC
back to top