| 14a56f1 | Christian Doczkal | 08 December 2021, 12:53:47 UTC | add lemma RO_LRO and generalize RO_FinRO_D | 08 December 2021, 12:53:47 UTC |
| 2f12998 | Christian Doczkal | 18 November 2021, 15:54:55 UTC | renamings | 03 December 2021, 13:59:53 UTC |
| 4d4db24 | Christian Doczkal | 15 November 2021, 16:46:50 UTC | cleanup and simplifications | 03 December 2021, 13:59:53 UTC |
| 7c93409 | Christian Doczkal | 15 November 2021, 13:04:20 UTC | adapt to generalzed section mechanism | 03 December 2021, 13:59:53 UTC |
| 7a88ce3 | Christian Doczkal | 06 July 2021, 15:27:24 UTC | nominal groups | 03 December 2021, 13:59:53 UTC |
| 6c65d07 | Pierre Boutry | 06 July 2021, 05:31:34 UTC | cleanup | 03 December 2021, 13:59:53 UTC |
| bac9061 | Pierre Boutry | 03 July 2021, 17:01:43 UTC | version of the ideal CCA with sampling | 03 December 2021, 13:59:53 UTC |
| 6fe4da4 | Pierre Boutry | 29 June 2021, 13:17:52 UTC | try to weaken ICCA assumptions | 03 December 2021, 13:59:53 UTC |
| 0931c93 | Pierre Boutry | 23 June 2021, 15:33:34 UTC | rename ICCA into ICCA_Oracle | 03 December 2021, 13:59:53 UTC |
| 086af0d | Pierre Boutry | 23 June 2021, 15:30:57 UTC | useless pk bis | 03 December 2021, 13:59:53 UTC |
| 412a153 | Pierre Boutry | 23 June 2021, 15:30:04 UTC | useless pk | 03 December 2021, 13:59:53 UTC |
| d4be3de | Pierre Boutry | 23 June 2021, 14:24:54 UTC | fix clone import of CCA | 03 December 2021, 13:59:53 UTC |
| eeab4a1 | Benjamin Gregoire | 21 June 2021, 09:50:10 UTC | use local clone to remove restriction | 03 December 2021, 13:59:53 UTC |
| cc46ec6 | Pierre Boutry | 21 June 2021, 07:01:42 UTC | close section and theory | 03 December 2021, 13:59:53 UTC |
| d82785d | Pierre Boutry | 17 June 2021, 19:18:35 UTC | weaken AB_bound | 03 December 2021, 13:59:53 UTC |
| 3ca12a5 | Pierre Boutry | 17 June 2021, 19:01:01 UTC | done? | 03 December 2021, 13:59:53 UTC |
| 94a269b | Pierre Boutry | 17 June 2021, 17:11:44 UTC | only AB_bound left | 03 December 2021, 13:59:53 UTC |
| 1938f58 | Christian Doczkal | 17 June 2021, 16:52:47 UTC | prove Real'_CCA_L (fix B) | 03 December 2021, 13:59:53 UTC |
| 25f8ab8 | Christian Doczkal | 17 June 2021, 16:05:31 UTC | fix definitions, Real_Real | 03 December 2021, 13:59:52 UTC |
| 1500e2c | Pierre Boutry | 17 June 2021, 15:29:10 UTC | forgot to inline one equiv | 03 December 2021, 13:59:52 UTC |
| 6a73e19 | Pierre Boutry | 17 June 2021, 15:12:07 UTC | fix ICCA_CCALR statement and prove it | 03 December 2021, 13:59:52 UTC |
| a43f264 | Pierre Boutry | 17 June 2021, 14:47:31 UTC | finish stating lemmas | 03 December 2021, 13:59:52 UTC |
| 916f3ca | Christian Doczkal | 16 June 2021, 16:47:45 UTC | first part of Real/Ideal formulation of IND-CCA2 | 03 December 2021, 13:59:52 UTC |
| 81bd4ac | Pierre Boutry | 15 June 2021, 12:20:18 UTC | inline some lemmas | 03 December 2021, 13:59:52 UTC |
| 210ab7a | Pierre Boutry | 15 June 2021, 11:08:57 UTC | done? | 03 December 2021, 13:59:52 UTC |
| 980e2fc | Christian Doczkal | 14 June 2021, 08:47:15 UTC | finish proof of A_bound' | 03 December 2021, 13:59:52 UTC |
| 8e1c76c | Christian Doczkal | 11 June 2021, 20:06:20 UTC | split CCA counting out of Wrap (WIP: problems with write restrictions) | 03 December 2021, 13:59:52 UTC |
| c05d6a1 | Christian Doczkal | 11 June 2021, 11:54:15 UTC | stuck with A'_call (A_bound too weak?) | 03 December 2021, 13:59:52 UTC |
| 2deaba7 | Pierre Boutry | 10 June 2021, 17:45:40 UTC | islossless lemmas | 03 December 2021, 13:59:52 UTC |
| b72702b | Christian Doczkal | 10 June 2021, 15:06:24 UTC | second half of CCA_1n | 03 December 2021, 13:59:52 UTC |
| ebae1d2 | Christian Doczkal | 09 June 2021, 14:44:40 UTC | first part of CCA_1n | 03 December 2021, 13:59:52 UTC |
| a7059bb | Pierre Boutry | 09 June 2021, 11:44:57 UTC | indentation and stuff | 03 December 2021, 13:59:52 UTC |
| 7205fd8 | Christian Doczkal | 08 June 2021, 15:55:03 UTC | WIP on CCA_1n | 03 December 2021, 13:59:52 UTC |
| 5873df5 | Pierre Boutry | 08 June 2021, 12:44:44 UTC | reorder | 03 December 2021, 13:59:52 UTC |
| ae8fede | Christian Doczkal | 07 June 2021, 11:52:33 UTC | finish proof of B_bound | 03 December 2021, 13:59:52 UTC |
| c916ea0 | Christian Doczkal | 04 June 2021, 11:57:19 UTC | changes from Benjamin | 03 December 2021, 13:59:52 UTC |
| 8069350 | Christian Doczkal | 04 June 2021, 11:54:19 UTC | inital draft of oracle_PKE | 03 December 2021, 13:59:52 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 |
| e770f0f | Pierre-Yves Strub | 09 November 2021, 15:36:49 UTC | 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:49 UTC |
| b0e609d | Pierre-Yves Strub | 05 November 2021, 15:07:43 UTC | Fix the pretty printing of \ as a binop fix #93 | 05 November 2021, 15:08:07 UTC |
| b37085c | Christian Doczkal | 04 November 2021, 14:52:23 UTC | renamings: dletE[_swap] -> dlet_muE[_swap] and dletE_mu -> dletE | 04 November 2021, 14:56:36 UTC |
| d5d3d94 | Christian Doczkal | 24 October 2021, 10:45:16 UTC | adapt to consistent use of mu1 | 04 November 2021, 12:09:30 UTC |
| 6676710 | Christian Doczkal | 24 October 2021, 09:36:02 UTC | use mu1 instead of mass in in Distr | 04 November 2021, 12:06:45 UTC |
| b9c7685 | Christian Doczkal | 03 November 2021, 15:28:23 UTC | comments, renaming, proof* | 04 November 2021, 10:00:49 UTC |
| 4da60d2 | Christian Doczkal | 03 November 2021, 15:06:57 UTC | allow sdist-distinguishers for ROs to call sample and set | 04 November 2021, 10:00:49 UTC |
| 8a26fe5 | Christian Doczkal | 03 November 2021, 12:25:10 UTC | some more simplifications | 04 November 2021, 10:00:49 UTC |
| 6851729 | Christian Doczkal | 01 November 2021, 10:09:10 UTC | remove weight equality side conditions | 04 November 2021, 10:00:49 UTC |
| a21c135 | Christian Doczkal | 22 October 2021, 14:33:38 UTC | implement feedback from review | 04 November 2021, 10:00:49 UTC |
| 570f090 | Christian Doczkal | 21 October 2021, 15:48:19 UTC | fix compilation | 04 November 2021, 10:00:49 UTC |
| 7fcfa1d | Christian Doczkal | 21 October 2021, 14:21:07 UTC | move lemmas from SDist to RealSeries and Distr, rename summableM | 04 November 2021, 10:00:49 UTC |
| f1d2f19 | Christian Doczkal | 21 October 2021, 09:05:24 UTC | use PROM rather than ROM | 04 November 2021, 10:00:49 UTC |
| 051cb1d | Christian Doczkal | 20 October 2021, 15:24:05 UTC | sdist for ROM distinguishers and N distinct queries | 04 November 2021, 10:00:49 UTC |
