https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
4e84f9c Make CI useful again 14 May 2020, 11:59:26 UTC
d64dafd finished linear bound 13 May 2020, 10:40:53 UTC
4db3868 step4 bad1 : bad1 -> lbad1 finished 12 May 2020, 14:16:57 UTC
7808e26 skeleton for bad1 07 May 2020, 13:19:40 UTC
bf8fd21 Merge branch 'deploy-chachapoly' of https://github.com/EasyCrypt/easycrypt into deploy-chachapoly 05 May 2020, 09:29:34 UTC
f552073 bound on (bad2 \/ forged): quadratic => linear; bound on (bad1) : still quadratic. 05 May 2020, 09:27:32 UTC
7b8526e ax. for polynomials 03 May 2020, 22:03:20 UTC
67b7c16 WIP 30 April 2020, 16:10:49 UTC
dc90870 Merge branch 'deploy-theory-monalg' into deploy-chachapoly 30 April 2020, 13:18:45 UTC
40fa163 fix default.nix 30 April 2020, 10:29:13 UTC
f1f2a80 Added two useful lemmas to Quotient.ec 30 April 2020, 10:29:13 UTC
dc24144 Definition of quotient types w.r.t. a equivalence relation 30 April 2020, 10:29:13 UTC
7bd64ee Finite groups, cyclic groups, Bezout. 30 April 2020, 10:29:13 UTC
c32f928 Use arrow-based assignments This is to align standard libraries with 1.0-preview, which forbids '=' 30 April 2020, 10:29:13 UTC
e7c6ffd stdlib: distributions: dmap1E_can 30 April 2020, 10:29:13 UTC
dffbae5 stdlib: List: nth_default 30 April 2020, 10:29:13 UTC
7fddd6b lemma: fun_ext2 30 April 2020, 10:29:13 UTC
b7990e8 allow writing m.[i, j] in place of m.[(i, j)] 30 April 2020, 10:29:13 UTC
fa624e2 views: allow application of induction principle as a view 30 April 2020, 10:29:13 UTC
293a64a elim: search quantifier modulo reduction 30 April 2020, 10:29:13 UTC
2967938 Fixed unclosed box. (#41) Co-authored-by: Adrien Koutsos <akoutsos@users.noreply.github.com> 30 April 2020, 10:29:13 UTC
26ee572 binomial coefficients 30 April 2020, 10:29:13 UTC
dd27af4 CI: move to slack notification 30 April 2020, 10:29:13 UTC
c872631 Matching for *hoareF & Pr 30 April 2020, 10:29:13 UTC
b66875f default.nix: adding installFlags 30 April 2020, 10:29:13 UTC
9c29f3f User error message for map-style lvalue on unsupported assignment [fix #17412] 30 April 2020, 10:29:13 UTC
95c5e0c Internal: remove LvMap lvalue. 30 April 2020, 10:29:13 UTC
87aa55c Revert "better conversion + simplify reduction algorithm." This reverts commit 11a875951d0f94381b22b362ddf8b0cc18f77886. 30 April 2020, 10:29:13 UTC
da17086 Only accepts Alt-Ergo from version 2.3.1 30 April 2020, 10:29:13 UTC
84126ec In `rewrite`, use a keyed matching algorithm for finding occurences. 30 April 2020, 10:29:13 UTC
71ecd2d drop python2 support 30 April 2020, 10:29:13 UTC
e24a389 Allow operators of the form 'n where n is a *fixed* natural number 30 April 2020, 10:29:13 UTC
a5351ba better conversion + simplify reduction algorithm. 30 April 2020, 10:29:13 UTC
8ac25f2 "hint simplify [reduce]" does one head reduction for finding the quantifers 30 April 2020, 10:29:13 UTC
f382eaf 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) 30 April 2020, 10:29:13 UTC
8eafa35 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 30 April 2020, 10:29:13 UTC
a610ed2 Refactor PlugAndPray 30 April 2020, 10:29:13 UTC
b599b94 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 30 April 2020, 10:29:13 UTC
786d6da [done] solves context of the form [false |- G] [fix 17270] 30 April 2020, 10:29:13 UTC
29a5adc Remove dead code in 't_solve' 30 April 2020, 10:29:13 UTC
329ace3 Improve />. Be sure that tactic crush (|>, />) does not transform the goal into umprovable one. 30 April 2020, 10:29:13 UTC
263d871 fix DHIES 30 April 2020, 10:29:13 UTC
e6385c5 fixing examples 30 April 2020, 10:29:13 UTC
b90a4ab fixing some examples 30 April 2020, 10:29:13 UTC
5a03071 Fix parser 30 April 2020, 10:29:13 UTC
fbd92e4 Printers for rewrite & solve databases 30 April 2020, 10:29:13 UTC
2cd0c9d add lemma in "random" database 30 April 2020, 10:29:13 UTC
efcc818 Rename internal tactic t_auto into t_solve 30 April 2020, 10:29:13 UTC
996ee58 improve automatic simplification of rnd rule for equiv 30 April 2020, 10:29:13 UTC
414eaa6 improve t_auto internal tactic 30 April 2020, 10:29:13 UTC
dc0468c automatically remove lossless condition in rnd{i} 30 April 2020, 10:29:13 UTC
e59c8de add simplification rule for oget_some, oget_none 30 April 2020, 10:29:13 UTC
ed7fb27 Compiles with OCaml 4.07 -> 4.09 (tested) 30 April 2020, 10:29:13 UTC
401f557 remove failing SMT 30 April 2020, 10:29:13 UTC
c8d4ed8 More results on dlet / dprod 30 April 2020, 10:29:13 UTC
c431557 bound bad1 alone, separate loop for forged vs bad2 29 April 2020, 20:10:44 UTC
94bccea simplify EncRnd 09 December 2019, 15:09:04 UTC
e0ca112 simplify axiom 06 December 2019, 18:48:35 UTC
5ce7541 clean up 06 December 2019, 18:47:53 UTC
a614d3b lemma on has and filter 06 December 2019, 18:47:27 UTC
492b952 add lemma on mu d (fun r => has (P r) s) 06 December 2019, 16:30:40 UTC
568f5fc end proof 06 December 2019, 08:03:49 UTC
ee5cf07 add files 06 December 2019, 08:03:20 UTC
e72e33d Split random oracle 06 December 2019, 08:01:56 UTC
c5b400a almost done 05 December 2019, 19:24:04 UTC
fc4f410 Merge remote-tracking branch 'origin/deploy-prod-fintype' into deploy-chachapoly 29 November 2019, 13:19:27 UTC
ec03a3c 29 November 2019, 13:19:00 UTC
bd9daac Merge remote-tracking branch 'origin/deploy-prod-fintype' into deploy-chachapoly 29 November 2019, 13:13:32 UTC
4778cea 29 November 2019, 13:12:51 UTC
d48df4e Merge remote-tracking branch 'origin/deploy-prod-fintype' into deploy-chachapoly 29 November 2019, 13:02:16 UTC
09c8cd7 missing files 29 November 2019, 13:01:53 UTC
f466e76 Merge remote-tracking branch 'origin/deploy-prod-fintype' into deploy-chachapoly 29 November 2019, 13:01:33 UTC
3ab8e94 Lazy Eager on FinType 29 November 2019, 12:59:59 UTC
5217cee FinType for products 29 November 2019, 12:58:25 UTC
759e168 Merge branch '1.0' into myske 29 November 2019, 07:57:32 UTC
de1d4dc Fix bug in eager if 29 November 2019, 07:56:52 UTC
f1937c1 Merge branch '1.0' into myske 29 November 2019, 07:52:47 UTC
894cfee remove 29 November 2019, 07:50:02 UTC
1a27b20 progress 28 November 2019, 07:04:53 UTC
209749b Fix bug in eager if 27 November 2019, 21:10:03 UTC
7bc397a some progress 27 November 2019, 14:47:07 UTC
c41c28f start proof 27 November 2019, 12:55:18 UTC
52bdbac some tests 27 November 2019, 11:59:10 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
1b160da 14 November 2019, 06:59:17 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
516917b 16 October 2019, 06:39:11 UTC
9300a3a pseudo-ring (minus assoc) 15 October 2019, 19:19:51 UTC
ab40fa2 Fix monalg.ec 15 October 2019, 10:44:47 UTC
d926d20 Merge branch '1.0' into deploy-theory-monalg 15 October 2019, 10:20:17 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
back to top