https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
14a56f1 add lemma RO_LRO and generalize RO_FinRO_D 08 December 2021, 12:53 UTC
2f12998 renamings 03 December 2021, 13:59 UTC
4d4db24 cleanup and simplifications 03 December 2021, 13:59 UTC
7c93409 adapt to generalzed section mechanism 03 December 2021, 13:59 UTC
7a88ce3 nominal groups 03 December 2021, 13:59 UTC
6c65d07 cleanup 03 December 2021, 13:59 UTC
bac9061 version of the ideal CCA with sampling 03 December 2021, 13:59 UTC
6fe4da4 try to weaken ICCA assumptions 03 December 2021, 13:59 UTC
0931c93 rename ICCA into ICCA_Oracle 03 December 2021, 13:59 UTC
086af0d useless pk bis 03 December 2021, 13:59 UTC
412a153 useless pk 03 December 2021, 13:59 UTC
d4be3de fix clone import of CCA 03 December 2021, 13:59 UTC
eeab4a1 use local clone to remove restriction 03 December 2021, 13:59 UTC
cc46ec6 close section and theory 03 December 2021, 13:59 UTC
d82785d weaken AB_bound 03 December 2021, 13:59 UTC
3ca12a5 done? 03 December 2021, 13:59 UTC
94a269b only AB_bound left 03 December 2021, 13:59 UTC
1938f58 prove Real'_CCA_L (fix B) 03 December 2021, 13:59 UTC
25f8ab8 fix definitions, Real_Real 03 December 2021, 13:59 UTC
1500e2c forgot to inline one equiv 03 December 2021, 13:59 UTC
6a73e19 fix ICCA_CCALR statement and prove it 03 December 2021, 13:59 UTC
a43f264 finish stating lemmas 03 December 2021, 13:59 UTC
916f3ca first part of Real/Ideal formulation of IND-CCA2 03 December 2021, 13:59 UTC
81bd4ac inline some lemmas 03 December 2021, 13:59 UTC
210ab7a done? 03 December 2021, 13:59 UTC
980e2fc finish proof of A_bound' 03 December 2021, 13:59 UTC
8e1c76c split CCA counting out of Wrap (WIP: problems with write restrictions) 03 December 2021, 13:59 UTC
c05d6a1 stuck with A'_call (A_bound too weak?) 03 December 2021, 13:59 UTC
2deaba7 islossless lemmas 03 December 2021, 13:59 UTC
b72702b second half of CCA_1n 03 December 2021, 13:59 UTC
ebae1d2 first part of CCA_1n 03 December 2021, 13:59 UTC
a7059bb indentation and stuff 03 December 2021, 13:59 UTC
7205fd8 WIP on CCA_1n 03 December 2021, 13:59 UTC
5873df5 reorder 03 December 2021, 13:59 UTC
ae8fede finish proof of B_bound 03 December 2021, 13:59 UTC
c916ea0 changes from Benjamin 03 December 2021, 13:59 UTC
8069350 inital draft of oracle_PKE 03 December 2021, 13:59 UTC
6a6f3b8 Merge pull request #105 from EasyCrypt/deploy-lift-lro lift LRO oracle out of FullEager 03 December 2021, 08:56 UTC
e77e653 lift LRO oracle out of FullEager 03 December 2021, 08:00 UTC
fe9a171 Update ci.yml 03 December 2021, 05:09 UTC
541aa08 fix substitution of modules when cloning. fix #97 02 December 2021, 10:41 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 UTC
2e815c5 PROM: add a ROmap interface for RO + access to the internal map 02 December 2021, 07:48 UTC
dda8233 CI / Zulip 02 December 2021, 07:46 UTC
f66167f [dune] add abstract theories to install list 26 November 2021, 15:00 UTC
b37b762 Prototype implementation of a match statement. 23 November 2021, 16:58 UTC
f8514a6 remove ocamlbuild.ml 22 November 2021, 17:48 UTC
50dae1b [build] install runtest (as ec-runtest) 21 November 2021, 16:30 UTC
3476312 script for graphing a dependency graph for .eco 19 November 2021, 10:53 UTC
08ed0c2 New format for eco (v3) Store whether a theory has been directly required or not. 19 November 2021, 07:18 UTC
471ea3b foo 19 November 2021, 07:04 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 UTC
10e1563 remove \# files 19 November 2021, 06:09 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 UTC
92f23db Add the project name in dune-project This is needed by "dune subst" ref #99 18 November 2021, 12:06 UTC
5e3929a remove debugging code 18 November 2021, 12:06 UTC
17e143c 17 November 2021, 15:41 UTC
b38a5aa 17 November 2021, 15:39 UTC
dfb413d fix opam package (do not do "dune subst") 17 November 2021, 15:35 UTC
0a2d4ad [build] use dune to install & find resources 17 November 2021, 08:23 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 UTC
229ac7a Remove EcFortune 17 November 2021, 06:24 UTC
02082bd Update copyright 17 November 2021, 06:22 UTC
e7d401f remove the script for creating tarballs 17 November 2021, 06:01 UTC
e46ef74 disable warning as errors 17 November 2021, 05:57 UTC
a54cec2 remove deprecated functions and reenable warning 3 17 November 2021, 05:52 UTC
b7a2ee2 reenable warning 39 17 November 2021, 05:43 UTC
4217836 reenable warning 38 17 November 2021, 05:41 UTC
061e164 reenable warning 35 17 November 2021, 05:40 UTC
43a1b9f reenable warning 34 17 November 2021, 05:39 UTC
5b09921 reenable warning 6 17 November 2021, 05:34 UTC
003fc41 [build] only consider src/theories/examples are deps 17 November 2021, 05:34 UTC
df78b65 .gitignore (.eca at root) 17 November 2021, 05:34 UTC
f8d5b79 Merge pull request #31 from ejgallego/1.0+dune [build] Add basic dune support 16 November 2021, 18:32 UTC
e39463d .gitignore: cleanup 16 November 2021, 17:37 UTC
68bbd4b [nix] update dependencies 16 November 2021, 17:35 UTC
f7c671c [build] use dune in Makefile 16 November 2021, 17:35 UTC
5334126 [build] do not create an internal EC library we do not currently expose any stable API. 16 November 2021, 17:35 UTC
3f13dec Use the old build system in opam. 16 November 2021, 17:35 UTC
fd804d6 [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 UTC
743a247 [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 UTC
4b604bf renamings: dletE[_swap] -> dlet_muE[_swap] and dletE_mu -> dletE 16 November 2021, 17:35 UTC
ab62416 adapt to consistent use of mu1 16 November 2021, 17:35 UTC
15946aa use mu1 instead of mass in in Distr 16 November 2021, 17:35 UTC
5a0238b [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 UTC
ec1f979 Merge pull request #88 from EasyCrypt/deploy-mu1 Consistently use `mu1` instead of `mass`. 09 November 2021, 16:32 UTC
e770f0f Refactor & generalize the section mechanism the section mechanism has been refactored s.t. it provides a more uniform interface where any kind of declaration can be marked as local / declared and erased / generalized when the section is closed. Co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr> Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> 09 November 2021, 15:36 UTC
b0e609d Fix the pretty printing of \ as a binop fix #93 05 November 2021, 15:08 UTC
b37085c renamings: dletE[_swap] -> dlet_muE[_swap] and dletE_mu -> dletE 04 November 2021, 14:56 UTC
d5d3d94 adapt to consistent use of mu1 04 November 2021, 12:09 UTC
6676710 use mu1 instead of mass in in Distr 04 November 2021, 12:06 UTC
b9c7685 comments, renaming, proof* 04 November 2021, 10:00 UTC
4da60d2 allow sdist-distinguishers for ROs to call sample and set 04 November 2021, 10:00 UTC
8a26fe5 some more simplifications 04 November 2021, 10:00 UTC
6851729 remove weight equality side conditions 04 November 2021, 10:00 UTC
a21c135 implement feedback from review 04 November 2021, 10:00 UTC
570f090 fix compilation 04 November 2021, 10:00 UTC
7fcfa1d move lemmas from SDist to RealSeries and Distr, rename summableM 04 November 2021, 10:00 UTC
f1d2f19 use PROM rather than ROM 04 November 2021, 10:00 UTC
051cb1d sdist for ROM distinguishers and N distinct queries 04 November 2021, 10:00 UTC
back to top