https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
27c52db Try out a non-branching version of core ROM This makes post-skip proofs a lot smoother (avoiding a lot of duplication in proofs). However, it requires some mental gymnastics to deal with no-op updates. 07 July 2020, 16:39:45 UTC
d750dc3 Fix merge problem 15 June 2020, 15:10:39 UTC
66c830f Clean up the ROM libraries Now reduced to PROM as core, with ROM as a simpler interface. PROM is concrete to allow reuse of its flag type. Its internal theories, and ROM, are abstract to avoid growing forests of clones when using eager arguments. ROM now aligns with PROM in cloning interface: additional types `d_in_t` and `d_out_t` specify the distinguisher's interface. (This simplifies instantiation.) Some changes to type and oracle names to make them more explicit. Notably: - `from` is now `in_t`, - `to` is now `out_t`, (with associated change on name of distribution). 15 June 2020, 14:55:33 UTC
734e5bb Do no search for rewriting patterns modulo conversion. 10 June 2020, 17:03:25 UTC
41d0d08 Theory on square matrices (up to ring structure) `unit` predicate is still abstract. The link with the determinant has still to be done. 10 June 2020, 14:44:03 UTC
4b965ee Fix compilation 10 June 2020, 14:13:50 UTC
c9641e4 Revert "Add user reductions for iteri" This reverts commit f693233ec9a7b33ba350d7b17e1d223f33d7fb56. 10 June 2020, 09:53:35 UTC
bacb90b in rewrite find occurences using alpha conversion first. 10 June 2020, 09:41:40 UTC
ab61883 add reduction for -i = i' 10 June 2020, 07:47:46 UTC
19c6c50 remove duplicate declaration 10 June 2020, 07:47:46 UTC
6965ea6 binomial law + basic lemmas (full / support) 10 June 2020, 07:46:26 UTC
2064617 "search" now works with notations [fix #17317] 10 June 2020, 07:28:49 UTC
763732a smt: do not filter wanted lemma 09 June 2020, 15:43:43 UTC
f693233 Add user reductions for iteri 09 June 2020, 15:39:58 UTC
23b938a Refactor & merge min/max & integer/real pow. Co-Authored-By: Benjamin Gregoire <benjamin.gregoire@inria.fr> Co-Authored-By: Pierre-Yves Strub <pierre-yves@strub.nu> 09 June 2020, 11:33:32 UTC
f71bd6c Some extra lemmas on Ring.expr Co-Authored-By: Benjamin Gregoire <benjamin.gregoire@inria.fr> Co-Authored-By: Pierre-Yves Strub <pierre-yves@strub.nu> 08 June 2020, 17:14:32 UTC
00ffc11 add lemmas on bigi 27 May 2020, 13:11:27 UTC
53ed919 Allows nosmt with all operators other than pure, abstract ones - i.e., with plain, axiomatized (including : {t | phi} as ax) and cases operators. When cloning, [op nosmt x = ...] is allowed, but nosmt can't be used with inlining mode. 26 May 2020, 08:38:14 UTC
170c443 fix default.nix 27 April 2020, 12:23:05 UTC
58aaed4 Merge pull request #42 from AntoineSere/eqvquo Added two useful lemmas to Quotient.ec 20 April 2020, 17:02:04 UTC
ce4d827 Added two useful lemmas to Quotient.ec 20 April 2020, 15:04:39 UTC
acfd4ea Definition of quotient types w.r.t. a equivalence relation 16 April 2020, 14:56:46 UTC
60a7d34 Finite groups, cyclic groups, Bezout. 16 April 2020, 13:19:53 UTC
cdb2e6f Use arrow-based assignments This is to align standard libraries with 1.0-preview, which forbids '=' 16 April 2020, 10:45:54 UTC
f44260c stdlib: distributions: dmap1E_can 16 April 2020, 09:41:06 UTC
94786bc stdlib: List: nth_default 16 April 2020, 09:40:44 UTC
136b237 lemma: fun_ext2 15 April 2020, 09:39:30 UTC
5eba66b allow writing m.[i, j] in place of m.[(i, j)] 15 April 2020, 09:31:23 UTC
4882379 views: allow application of induction principle as a view 15 April 2020, 08:28:48 UTC
64d592d elim: search quantifier modulo reduction 15 April 2020, 08:19:54 UTC
3b8b038 Fixed unclosed box. (#41) Co-authored-by: Adrien Koutsos <akoutsos@users.noreply.github.com> 14 April 2020, 15:08:58 UTC
f3581d5 binomial coefficients 10 April 2020, 09:56:42 UTC
21e8fce CI: move to slack notification 09 April 2020, 16:21:20 UTC
d41a34d Matching for *hoareF & Pr 09 April 2020, 13:44:05 UTC
4062085 Merge pull request #40 from CohenCyril/nixfix default.nix: adding installFlags 09 April 2020, 13:39:11 UTC
21354f7 default.nix: adding installFlags 08 April 2020, 15:23:25 UTC
149b09f User error message for map-style lvalue on unsupported assignment [fix #17412] 28 March 2020, 08:13:21 UTC
b1b35e6 Internal: remove LvMap lvalue. 26 March 2020, 19:52:54 UTC
1a8d60a Revert "better conversion + simplify reduction algorithm." This reverts commit 11a875951d0f94381b22b362ddf8b0cc18f77886. 26 March 2020, 18:26:21 UTC
2a5b4f6 Only accepts Alt-Ergo from version 2.3.1 26 March 2020, 07:42:17 UTC
22799f1 In `rewrite`, use a keyed matching algorithm for finding occurences. 28 February 2020, 06:49:27 UTC
10b9097 drop python2 support 15 February 2020, 09:20:51 UTC
44b23b5 Allow operators of the form 'n where n is a *fixed* natural number 15 February 2020, 07:19:25 UTC
11a8759 better conversion + simplify reduction algorithm. 14 February 2020, 08:36:31 UTC
4f587f3 "hint simplify [reduce]" does one head reduction for finding the quantifers 13 February 2020, 09:06:03 UTC
2bbf3d3 Add new options to 'hint simplify': - reduce: equations are found up-to reduction - eqtrue: if no equations can be found, add a equation of the form (e = true) 13 February 2020, 08:38:38 UTC
2efb9e7 Consolidate PRP and PRF libraries Including weak PRP-PRF switching lemma, but not its strong version Squashed commit of the following: commit 005342f19a55b0ae01c88c0c729fdbad3f2519ff Merge: 5407570b 7325ae6d Author: François Dupressoir <fdupress@gmail.com> Date: Mon Feb 10 09:48:54 2020 +0000 Merge branch '1.0' into deploy-simpler-rp commit 5407570bbdeaee7b725f57fcdbbf764ff301ac9e Author: François Dupressoir <fdupress@gmail.com> Date: Fri Jan 24 12:00:21 2020 +0000 move towards merging PRF and RO also clean assignment notation commit 65e0c4eb8c702729500148e34900dc5971e583a7 Author: François Dupressoir <fdupress@gmail.com> Date: Tue Jan 21 14:14:29 2020 +0000 Integrate PRP-PRF switching lemma into PRP lib Not done for the strong version yet commit 456a7c96e40fa6827d92fbc36d8cd75fdd8abab1 Author: François Dupressoir <fdupress@gmail.com> Date: Tue Jan 21 09:40:25 2020 +0000 Simplifying the PRF interface No keys are needed for the ideal RP, The raw interface can be defined separately as needed. commit e7dea73e6eae21f192efc45f42e9cdc9e5ec4eb8 Author: François Dupressoir <fdupress@gmail.com> Date: Tue Jan 21 09:19:04 2020 +0000 Some nits commit 8bb90549b6084ea8189e3a4067a155f977ccd34a Author: François Dupressoir <fdupress@gmail.com> Date: Mon Jan 20 16:38:30 2020 +0000 Cleanup PRP/PRF and PRP-PRF 10 February 2020, 09:50:13 UTC
7325ae6 Refactor PlugAndPray 10 February 2020, 09:45:08 UTC
9e11412 Generalize arguments about sampling in dexcepted This pushes several complex low-level arguments related to sampling in restricted distributions into the related distribution file. This also generalizes these arguments, so that: - TwoStepSampling no longer requires a full distribution, - WhileSampling takes distributions and tests as procedure arguments rather than clone parameters. Specialized versions of theories and lemmas that reproduce the old behaviours are also included. The Dice_Sampling theory is removed, replaced with Dexcepted.WhileSamplingFixedTest (an abstract theory). Squashed commit of the following: commit e4bf1725f2a327bc58dda51d0079acb8dbb8fb1a Author: François Dupressoir <fdupress@gmail.com> Date: Thu Jan 16 20:40:23 2020 +0000 trailing white space in modified files commit 12d5ff0ae8607be10f7e925d1f0d44dd8e78dbde Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 19 15:49:41 2019 +0000 minor cleanup commit 7921a24e13e9f6d19ad02c0a22e8efb49bc37184 Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 19 13:47:19 2019 +0000 More general ways of sampling out of a predicate TwoStep no longer requires losslessness. More sharing of proof could be obtained commit 393700f85b47b9d373be983b1451b08ae3d3be94 Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 5 21:40:16 2019 +0000 PRP<->PRF uses generic resampling commit 74b9aef924cc313e358510ab9f83bc7410489db4 Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 5 21:27:12 2019 +0000 Slight generalization: no longer need a full distribution commit 0853fc0e313bb6adac0ad956417480ebd70f512f Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 5 18:34:43 2019 +0000 Dexcepted: equivalence between two ways of sampling used in PRP<->PRF, but also in a current proof TODO: make PRP<->PRF use this 16 January 2020, 20:48:25 UTC
cd341ca [done] solves context of the form [false |- G] [fix 17270] 18 December 2019, 09:52:45 UTC
050cada Remove dead code in 't_solve' 18 December 2019, 09:52:45 UTC
1ec24f8 Improve />. Be sure that tactic crush (|>, />) does not transform the goal into umprovable one. 18 December 2019, 07:48:19 UTC
eb9d7e3 fix DHIES 10 December 2019, 17:19:16 UTC
7c400bd fixing examples 10 December 2019, 15:36:45 UTC
943b847 Merge remote-tracking branch 'origin/1.0' into deploy-simple-stuff 10 December 2019, 14:36:33 UTC
3acf93f fixing some examples 10 December 2019, 14:35:50 UTC
47c0851 Fix parser 10 December 2019, 14:34:52 UTC
0d33668 Printers for rewrite & solve databases 10 December 2019, 14:00:13 UTC
0b1128e add lemma in "random" database 10 December 2019, 12:38:29 UTC
babbac3 Rename internal tactic t_auto into t_solve 10 December 2019, 12:33:05 UTC
e6c9905 improve automatic simplification of rnd rule for equiv 10 December 2019, 12:29:05 UTC
5d09cc2 improve t_auto internal tactic 10 December 2019, 12:28:10 UTC
2b2b5b8 automatically remove lossless condition in rnd{i} 09 December 2019, 15:43:32 UTC
fa8b38b add simplification rule for oget_some, oget_none 07 December 2019, 09:46:33 UTC
89e35d1 Compiles with OCaml 4.07 -> 4.09 (tested) 05 December 2019, 19:54:02 UTC
132968e remove failing SMT 02 December 2019, 10:06:01 UTC
60cfeb4 More results on dlet / dprod 02 December 2019, 09:16:55 UTC
de1d4dc Fix bug in eager if 29 November 2019, 07:56:52 UTC
78e8f6e Work of Roberto Metere on Sigma Protocols: - formalisation of the discrete logarithm assumption - formalisation of generic commitment schemes - formal verification of the Pedersen commitment scheme - formalisation of generic Sigma protocols - Sigma Protocol example: the Schnorr proof of knowledge Co-authored-by: Roberto Metere <r.metere2@ncl.ac.uk> 26 November 2019, 13:31:58 UTC
add72dc Squashed commit of the following: [closes #17403] commit 55d4c60f675f8baf509682dd12e817377ba682e9 Author: Pierre-Yves Strub <pierre-yves@strub.nu> Date: Thu Nov 14 10:30:54 2019 +0100 Regeneralization of unspecified arguments in applicative views 14 November 2019, 10:15:31 UTC
e58c36a add the full PRG tutorial from FOSAD (#35) 07 November 2019, 16:19:02 UTC
e53aab7 Check .eco after the loader has been configured [fix #17400] 25 October 2019, 15:59:33 UTC
6489ade Make ECO handling more robust - do not fail when an .eco file is invalid - fix the reading of the `version' flag - erase staled .eco file - do not accept to compile files not handing with .ec or .eca - API: .mli file for EcEco [fix #17398] 25 October 2019, 06:46:13 UTC
10b2ab0 Add EC hash to .eco 18 October 2019, 08:36:08 UTC
51f8ab0 .gitignore: .eco 18 October 2019, 08:11:34 UTC
f38226c Generate and use .eco files. Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> Co-authored-by: Benjamin Gregoire <benjamin.gregoire@inria.fr> 17 October 2019, 10:08:11 UTC
1c35db0 Fix t_auto. (was pruning opened goals) 16 October 2019, 09:09:32 UTC
2139beb CI: test 1.0-preview 15 October 2019, 07:46:58 UTC
2f6587f In `case`, normalized 'glob' when searching for an inductive type. [fix #17391] 15 October 2019, 07:09:54 UTC
74207ab Remove debugging infos 14 October 2019, 15:22:16 UTC
e023995 New option from inline: [tuple]. Allows no to not use tuple assignments. 14 October 2019, 12:27:51 UTC
a38b2e9 Fix handling of abstract theories imports. 14 October 2019, 12:05:09 UTC
e12e2c2 This commit introduces two major features. - call by value reduction strategy. - user defined reduction rules. Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> Co-authored-by: Benjamin Gregoire <benjamin.gregoire@inria.fr> 14 October 2019, 08:39:46 UTC
651df3f Solve tactic: apply is now done modulo delta 14 October 2019, 08:24:30 UTC
e77d659 Misc. in SmtMap.ec 14 October 2019, 07:45:06 UTC
297f528 Add interleave tactic 14 October 2019, 07:10:05 UTC
ce9380d Add transitivity * (transivity with generation of VC) 14 October 2019, 06:42:35 UTC
3b9667b Pragmas for printing pre/post as a list of their resp. conjunctions Pragmas are: PrPo:{pr,po}:{raw,ands} (Pragma system has been revamped by this commit) 14 October 2019, 06:27:33 UTC
66e7f99 Add decimal literals 14 October 2019, 05:55:27 UTC
115229e New intro pattern: [#|]. [#|] is a multi-case i-p (like [#]) that works also on on disjunctions. 14 October 2019, 05:19:52 UTC
1f45fde refactor flagged map && PROM (#22) 10 October 2019, 11:50:05 UTC
da0b25a Some extra lemmas on nseq (#26) 10 October 2019, 07:49:06 UTC
408d1b0 Add a more general version of dmap_uni (#30, #33) 10 October 2019, 07:19:29 UTC
e9598be Add lemmas to filter noncontributing list items in bigops (#29) 10 October 2019, 06:50:06 UTC
8eb2491 Critical bugfix on dot-product (#34) * Critical bugfix on dot-product * CauchySchwarz is now an abstract theory 09 October 2019, 19:14:57 UTC
c8257d3 Namespace for libraries and th. renaming 02 October 2019, 06:23:52 UTC
f2bcd42 README: add a note about installing external deps for provers 01 October 2019, 20:12:36 UTC
b6a4d3a Docker: bump Z3 version 01 October 2019, 19:49:59 UTC
4860685 Fetch more up-to-date smt binaries & compress unnecessary layers 01 October 2019, 10:54:42 UTC
88ded1b Fix "n?" intro pattern. 17 September 2019, 11:28:41 UTC
back to top