https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
787383f [C/G]DH-RSR: adapt to changes on main branch 27 June 2022, 15:50:50 UTC
ffb0bb3 AKEM: adapt to changes on main branch 31 May 2022, 11:27:55 UTC
71cc455 AKEM: bound public key collisions 10 May 2022, 14:09:06 UTC
ca2e7c8 fsize and fcoll_bound for PROM 09 May 2022, 14:31:24 UTC
9b703ad fix brittle smt call 27 April 2022, 12:22:33 UTC
4180067 clean up Oracle_PKE (IND-CCA2) 27 April 2022, 12:11:20 UTC
3b14065 update the proof to fit the new axiom for nominal groups 21 April 2022, 14:15:12 UTC
ee0e32a adapt to cost-merge changes 05 April 2022, 11:01:59 UTC
6a925f4 Merge branch 'main' into deploy-cv2ec (syntax changes) 05 April 2022, 09:37:49 UTC
29061b7 [chore] update theories/dune 30 March 2022, 12:32:24 UTC
0b0aa5d [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 License change: CeCILL B/C -> MIT 29 March 2022, 19:39:31 UTC
b229a87 dopt: extend subdistribution to lossless distributions on options 29 March 2022, 14:19:04 UTC
1a754ad [tactic]: in `apply... in...`, check that all variables are instantiated fix #149 29 March 2022, 09:05:09 UTC
7a93224 [build]: [dune]: auto-generation of theories/dune 28 March 2022, 17:07:06 UTC
a9748f7 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 Add lemmas divzMr and divzMl; strenghten and prove modz_pow2_div. 17 March 2022, 20:33:03 UTC
3646dd8 changed name of lemma 12 March 2022, 10:06:23 UTC
d5df8b2 added stronger version of dmap1E_can 12 March 2022, 10:06:23 UTC
c98b014 Extend standard library (IntDiv) with core results. 03 March 2022, 18:13:54 UTC
44211a9 prepare gluing 03 March 2022, 14:18:59 UTC
1305ee1 prepare gluing 03 March 2022, 14:11:52 UTC
e22c918 Added definition and lemmas for 'put' operator in List.ec. 03 March 2022, 12:53:02 UTC
8cfa32b An axiom-free formalization of well-founded relations, induction and recursion. 03 March 2022, 09:50:40 UTC
6199997 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 Stdlib: more results on integer division & exponentiation 02 March 2022, 16:28:09 UTC
c316eff Removed redundant "rec" in function declaration. 01 March 2022, 14:04:58 UTC
26f2dba additional lemmas from IND_CCA2_find_proof 28 February 2022, 13:33:58 UTC
77aac4b Revert "Unfold non-transparent operators in `case` & `elim`." This reverts commit 70662a755d2121ca1c809cf2eef68462bd720d72. 24 February 2022, 07:02:59 UTC
559910b Partially fix memory capture in substitutions closes #130 22 February 2022, 09:41:14 UTC
ce4d8ca [dune+opam] fix git hash versioning widget 21 February 2022, 18:24:12 UTC
f278e3c Lemma stating equality of word and list distributions 18 February 2022, 22:51:52 UTC
70662a7 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 Fails gracefully when applying a tactic on a completed proof. fix #133 18 February 2022, 22:18:29 UTC
60ea9db gather generic lemmas in one file 18 February 2022, 15:36:35 UTC
9c22d15 AKEM: query counting and final theorem 18 February 2022, 08:20:01 UTC
e7e4b62 replace all uses of 'smt.' 16 February 2022, 14:59:03 UTC
39b2562 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
30b796e AKEM: cleanup and comments 15 February 2022, 16:22:34 UTC
7f87ed3 AKEM: finish proof of Lemma 3 (up to absence of pkey collisions) 15 February 2022, 13:51:25 UTC
f7e85af AKEM: assume no public key collisions (WIP) 14 February 2022, 09:40:12 UTC
4ca2786 AKEM: stuck with OidealB_Guv1 02 February 2022, 15:25:54 UTC
2402e66 AKEM: eager/lazy argument for Outsider-2-CCA 28 January 2022, 09:51:59 UTC
d847355 AKEM: OrealB_Guv (up to eager-lazy argument) 27 January 2022, 13:51:26 UTC
c254327 AKEM: first part of lemma3 25 January 2022, 13:33:09 UTC
cd105a8 AKEM: proof Lemma 2 and statement/skeleton of Theorem 11 24 January 2022, 09:41:33 UTC
1e7b210 adapt to changes in Hybrid 21 January 2022, 14:50:35 UTC
fa1cfde add cv2ec proof of GDH-RSR 21 January 2022, 14:04:03 UTC
fef5826 collect cv2ec proofs of CDH-RSR and IND-CCA2 on one branch 21 January 2022, 13:40:04 UTC
ce56b10 Add rdirs option in config file closes #127 19 January 2022, 22:45:29 UTC
46ba308 Apply suggestions from code review Co-authored-by: Francois Dupressoir <fdupress@gmail.com> 05 January 2022, 13:39:35 UTC
49e768e fix theories 05 January 2022, 13:39:35 UTC
e77248a allow zero queries in Hybrid and SDist 05 January 2022, 13:39:35 UTC
49aec58 lemmas on FSet, List, and DList 10 December 2021, 17:02:37 UTC
7df1de5 First pass: slices are inclusive 09 December 2021, 21:39:05 UTC
32abff2 some lemmas on subseq, fmap, and drat 09 December 2021, 06:26:12 UTC
799d429 add lemma RO_LRO and generalize RO_FinRO_D 08 December 2021, 13:26:16 UTC
8e47fe3 Fix bug that prevents `rewrite //= in h` to simplify in `h` Fix #68 03 December 2021, 16:12:21 UTC
6a6f3b8 Merge pull request #105 from EasyCrypt/deploy-lift-lro lift LRO oracle out of FullEager 03 December 2021, 08:56:41 UTC
e77e653 lift LRO oracle out of FullEager 03 December 2021, 08:00:10 UTC
fe9a171 Update ci.yml 03 December 2021, 05:09:09 UTC
541aa08 fix substitution of modules when cloning. fix #97 02 December 2021, 10:41:39 UTC
4a1ce0d [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 PROM: add a ROmap interface for RO + access to the internal map 02 December 2021, 07:48:19 UTC
dda8233 CI / Zulip 02 December 2021, 07:46:33 UTC
f66167f [dune] add abstract theories to install list 26 November 2021, 15:00:50 UTC
b37b762 Prototype implementation of a match statement. 23 November 2021, 16:58:42 UTC
f8514a6 remove ocamlbuild.ml 22 November 2021, 17:48:42 UTC
50dae1b [build] install runtest (as ec-runtest) 21 November 2021, 16:30:31 UTC
3476312 script for graphing a dependency graph for .eco 19 November 2021, 10:53:40 UTC
08ed0c2 New format for eco (v3) Store whether a theory has been directly required or not. 19 November 2021, 07:18:46 UTC
471ea3b foo 19 November 2021, 07:04:08 UTC
a549eb4 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 remove \# files 19 November 2021, 06:09:01 UTC
ffe0656 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 Add the project name in dune-project This is needed by "dune subst" ref #99 18 November 2021, 12:06:45 UTC
5e3929a remove debugging code 18 November 2021, 12:06:09 UTC
17e143c 17 November 2021, 15:41:35 UTC
b38a5aa 17 November 2021, 15:39:37 UTC
dfb413d fix opam package (do not do "dune subst") 17 November 2021, 15:35:07 UTC
0a2d4ad [build] use dune to install & find resources 17 November 2021, 08:23:14 UTC
31ce231 [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 Remove EcFortune 17 November 2021, 06:24:47 UTC
02082bd Update copyright 17 November 2021, 06:22:22 UTC
e7d401f remove the script for creating tarballs 17 November 2021, 06:01:10 UTC
e46ef74 disable warning as errors 17 November 2021, 05:57:03 UTC
a54cec2 remove deprecated functions and reenable warning 3 17 November 2021, 05:52:23 UTC
b7a2ee2 reenable warning 39 17 November 2021, 05:43:59 UTC
4217836 reenable warning 38 17 November 2021, 05:41:36 UTC
061e164 reenable warning 35 17 November 2021, 05:40:28 UTC
43a1b9f reenable warning 34 17 November 2021, 05:39:17 UTC
5b09921 reenable warning 6 17 November 2021, 05:34:48 UTC
003fc41 [build] only consider src/theories/examples are deps 17 November 2021, 05:34:23 UTC
df78b65 .gitignore (.eca at root) 17 November 2021, 05:34:13 UTC
f8d5b79 Merge pull request #31 from ejgallego/1.0+dune [build] Add basic dune support 16 November 2021, 18:32:37 UTC
e39463d .gitignore: cleanup 16 November 2021, 17:37:59 UTC
68bbd4b [nix] update dependencies 16 November 2021, 17:35:05 UTC
f7c671c [build] use dune in Makefile 16 November 2021, 17:35:05 UTC
5334126 [build] do not create an internal EC library we do not currently expose any stable API. 16 November 2021, 17:35:05 UTC
3f13dec Use the old build system in opam. 16 November 2021, 17:35:04 UTC
back to top