Skip to main content
https://github.com/EasyCrypt/easycrypt
04 July 2025, 20:56:38 UTC
sort by:
RevisionAuthorDateMessageCommit Date
d583086 Antoine Séré01 March 2021, 09:56:16 UTCCRT prooved modulo some easy admits01 March 2021, 09:56:16 UTC
a6d9801 Antoine Séré27 February 2021, 11:42:50 UTCadditive and multiplicative left in CRT27 February 2021, 11:42:50 UTC
4e72a78 Antoine Séré26 February 2021, 23:06:36 UTCAdvanced proof26 February 2021, 23:06:36 UTC
be9057b Antoine Séré25 February 2021, 22:39:02 UTCMerge branch 'deploy-crt' of https://github.com/EasyCrypt/easycrypt into deploy-crt25 February 2021, 22:39:02 UTC
98b4558 Antoine Séré25 February 2021, 22:38:54 UTCAdvanced proof in CRT25 February 2021, 22:38:54 UTC
d31ba9a Pierre-Yves Strub23 February 2021, 14:50:04 UTCcleanup23 February 2021, 14:50:04 UTC
b650e9f Antoine Séré23 February 2021, 13:03:59 UTCAdvancing proof of CRT23 February 2021, 13:03:59 UTC
607b6cc Antoine Séré19 February 2021, 14:36:31 UTCAdvanced crt19 February 2021, 14:36:31 UTC
9e43e60 Pierre-Yves Strub19 February 2021, 11:22:30 UTCBachet Bezout in euclidean domains The proof only use principality of ideals and could be ported to principal rings easily.19 February 2021, 11:22:30 UTC
02763c8 Pierre-Yves Strub19 February 2021, 11:22:17 UTC[trivial]: the tactic now tries to do a [solve] first19 February 2021, 11:22:17 UTC
9898669 Pierre-Yves Strub18 February 2021, 11:01:16 UTCCRT: spec (add missing preconditions)18 February 2021, 11:01:16 UTC
d8fbd62 Pierre-Yves Strub18 February 2021, 10:59:19 UTCCRT: spec18 February 2021, 10:59:19 UTC
a7ca8c7 Pierre-Yves Strub02 February 2021, 14:18:43 UTCLib: uniform distributions over finite functions02 February 2021, 14:18:43 UTC
708e88c Pierre-Yves Strub16 January 2021, 08:38:18 UTCLosslessness axioms are now added to the "rnd" database16 January 2021, 08:38:18 UTC
9dcb1a4 Pierre-Yves Strub16 January 2021, 07:53:24 UTCRenaming: XXX_full -> XXX_fu16 January 2021, 07:53:35 UTC
7314a12 Benjamin Gregoire16 January 2021, 05:42:38 UTCprinting added lemma by operator declaration16 January 2021, 05:43:39 UTC
f7e2b19 Pierre-Yves Strub15 January 2021, 14:03:21 UTCBasic results on dvector/dmatrix15 January 2021, 14:03:21 UTC
b5f65bc Pierre-Yves Strub15 January 2021, 09:29:53 UTCBasic results on dvector/dmatrix15 January 2021, 09:29:53 UTC
844e61b Pierre-Yves Strub15 January 2021, 08:11:01 UTCMore results on dlet/dmap15 January 2021, 08:11:01 UTC
bb0a97a Pierre-Yves Strub13 January 2021, 15:15:47 UTCAxiomatized operators are now forcibly unfoldable13 January 2021, 15:15:47 UTC
88e05a0 Benjamin Gregoire12 January 2021, 14:55:42 UTCt_subst not in the trusted base + some improvement to />.12 January 2021, 14:55:42 UTC
5583bca Benjamin Gregoire12 January 2021, 14:15:46 UTCpragma -oldip become the default12 January 2021, 14:15:46 UTC
6feb5d7 Benjamin Gregoire05 January 2021, 11:47:23 UTCfix quadratic behavior of ecCallbyValue05 January 2021, 11:47:23 UTC
999561c Pierre-Yves Strub04 January 2021, 13:24:41 UTCremove deprecated "cut" tactic04 January 2021, 13:24:41 UTC
f4f3f94 Pierre-Yves Strub04 January 2021, 10:26:56 UTCimplement -R flag04 January 2021, 10:26:56 UTC
3671d46 Pierre-Yves Strub18 December 2020, 20:07:48 UTCTravis -> CircleCI18 December 2020, 20:07:48 UTC
35e59d1 Pierre-Yves Strub04 December 2020, 14:05:15 UTC`apply` is now using product-compatible matching04 December 2020, 14:05:15 UTC
6504b04 Pierre-Yves Strub03 December 2020, 13:54:55 UTCremove debug infos03 December 2020, 13:55:10 UTC
3c14f4d Benjamin Gregoire03 December 2020, 07:08:30 UTCsmall refactoring03 December 2020, 07:08:30 UTC
177f61d Benjamin Gregoire03 December 2020, 05:53:30 UTCadd trivial lemma03 December 2020, 05:53:30 UTC
e7ca052 Benjamin Gregoire02 December 2020, 15:08:03 UTCstack based conversion02 December 2020, 15:08:03 UTC
93748b3 Pierre-Yves Strub01 December 2020, 09:41:56 UTCDecimal numbers are now translated to irreducible fractions01 December 2020, 09:41:56 UTC
de9fdea Pierre-Yves Strub01 December 2020, 08:48:33 UTCIn pose/trivial: use less conversion, cleanup chain of trivial calls.01 December 2020, 08:48:33 UTC
68b3ffa Benjamin Gregoire27 November 2020, 16:47:34 UTCmake congr less costly27 November 2020, 16:47:34 UTC
ea13c71 Benjamin Gregoire27 November 2020, 16:46:54 UTCsimplify t_split27 November 2020, 16:46:54 UTC
2363562 Benjamin Gregoire24 November 2020, 19:47:13 UTCfix cbv user_red24 November 2020, 19:47:13 UTC
6857723 Benjamin Gregoire24 November 2020, 13:48:55 UTCsimplify user reduction24 November 2020, 13:49:28 UTC
fcdfcbd Pierre-Yves Strub21 November 2020, 12:11:49 UTCCore theory for univariate polynomials21 November 2020, 12:11:49 UTC
a08bc34 Pierre-Yves Strub21 November 2020, 08:29:35 UTCStdlib: more results on Rn + bigops on Rn21 November 2020, 08:29:35 UTC
7a42484 Pierre-Yves Strub21 November 2020, 00:14:50 UTCMANIFEST21 November 2020, 00:14:50 UTC
07b937c Pierre-Yves Strub20 November 2020, 22:16:40 UTCSmall addititions on distributions20 November 2020, 22:16:40 UTC
6f68e27 Pierre-Yves Strub20 November 2020, 14:45:54 UTCMore results on distributions (conditional exp, Jensen (finite))20 November 2020, 14:45:54 UTC
27ff637 Pierre-Yves Strub18 November 2020, 06:00:50 UTCintegrating more results on distributions18 November 2020, 06:00:50 UTC
8d01a80 Benjamin Gregoire17 November 2020, 17:48:08 UTCfix CBC17 November 2020, 17:48:08 UTC
ed25190 Benjamin Gregoire16 November 2020, 10:58:31 UTCsmall generalization of PRP16 November 2020, 10:58:31 UTC
8cb3e88 Benjamin Gregoire13 November 2020, 11:33:30 UTCextend conseq rules: equivF => hoareF => hoareF and equivF => phoareF => phoareF13 November 2020, 11:33:47 UTC
4391b04 Pierre-Yves Strub12 November 2020, 11:00:16 UTCbasic results about minr12 November 2020, 11:00:16 UTC
61de4b9 Pierre-Yves Strub12 November 2020, 08:24:07 UTCFix "smt debug"12 November 2020, 08:24:20 UTC
b360fa8 Benjamin Gregoire11 November 2020, 05:55:58 UTCFix bug in conseq11 November 2020, 05:56:42 UTC
ffad375 Pierre-Yves Strub03 November 2020, 09:04:00 UTCNew option for SMT: "debug"03 November 2020, 09:04:00 UTC
4ef4286 Pierre-Yves Strub21 October 2020, 08:49:24 UTCFix dfold s.t. the functor takes the index21 October 2020, 08:49:24 UTC
19c7285 Pierre-Yves Strub20 October 2020, 09:34:40 UTCNew operator: dfold20 October 2020, 09:40:14 UTC
fa3853d Pierre-Yves Strub15 October 2020, 10:30:04 UTCREADME (nix)15 October 2020, 10:30:04 UTC
bc4f6df Pierre-Yves Strub15 October 2020, 08:39:16 UTC"={_}" now supports the construction "glob M \ { p1, p2, ... }" It stands for "glob M" without "p1, p2, ..."15 October 2020, 08:39:16 UTC
22a8b51 Pierre-Yves Strub14 October 2020, 09:10:10 UTCbetter printing of modules bodies w.r.t. "import var"14 October 2020, 09:10:10 UTC
ca1f0d2 Pierre-Yves Strub14 October 2020, 07:08:46 UTCThe command "import var" is now allowed at top-level14 October 2020, 07:08:46 UTC
b34c174 Pierre-Yves Strub14 October 2020, 06:55:56 UTCadd alias "include var" that stands for "include" then "import var"14 October 2020, 06:55:56 UTC
c3114bd Pierre-Yves Strub14 October 2020, 06:52:22 UTC"import var" now takes a space-separated list of modules14 October 2020, 06:52:22 UTC
4268b0f Pierre-Yves Strub14 October 2020, 06:33:40 UTCNew command in modules: import var M This imports the variables of M in the active module scope.14 October 2020, 06:34:14 UTC
7ba9ba4 Pierre-Yves Strub11 October 2020, 07:27:44 UTCDocker image: bump provers versions11 October 2020, 07:27:44 UTC
7d8a513 François Dupressoir10 October 2020, 11:22:49 UTCHelp smt along in brittle proofs These SMT fail when using: - Why3 1.3.1 - Z3 4.8.9 - CVC4 1.9 - Alt-Ergo 1.3.3 This appears to be bad interplay between the provers and this version of Why3: the proofs work with Why3 1.210 October 2020, 12:08:14 UTC
469a12a François Dupressoir09 October 2020, 16:20:54 UTCeasycrypt why3config uses --full-config09 October 2020, 16:20:54 UTC
ef6f0ba Pierre-Yves Strub09 October 2020, 15:44:59 UTCREADME: add --full-config option (why3 config)09 October 2020, 15:44:59 UTC
6d31cc5 Pierre-Yves Strub09 October 2020, 15:44:32 UTCUpdate Dockerfile w.r.t new EasyCrypt repo layout09 October 2020, 15:44:32 UTC
e664da3 Pierre-Yves Strub09 October 2020, 11:02:44 UTCDocker: do not use easycrypt remote anymore09 October 2020, 11:02:44 UTC
ce70fa4 Pierre-Yves Strub09 October 2020, 10:23:24 UTCopam: change post-install message09 October 2020, 10:23:24 UTC
6c03840 Pierre-Yves Strub09 October 2020, 10:21:16 UTCFix travis configuration file w.r.t recent changes09 October 2020, 10:21:16 UTC
44a728a Pierre-Yves Strub09 October 2020, 10:16:24 UTCUpdate README (no more external opam repo) & add missing opam fields09 October 2020, 10:16:58 UTC
e37a10c Pierre-Yves Strub09 October 2020, 08:12:15 UTCImport opam file s.t. travis can use it to update its dependencies09 October 2020, 08:41:05 UTC
c436fd4 Pierre-Yves Strub09 October 2020, 07:16:05 UTCTravis: update EasyCrypt dependencies before running tests09 October 2020, 08:41:05 UTC
730f329 Pierre-Yves Strub09 October 2020, 08:02:28 UTCdefault.nix: remove restriction on Why3 version09 October 2020, 08:41:05 UTC
8f33b95 Stephane Graham-Lengrand07 October 2020, 23:19:47 UTCFirst attempt at handling Why3 1.3.X09 October 2020, 08:41:05 UTC
3007982 Benjamin Gregoire14 September 2020, 13:36:41 UTCfix default.nix14 September 2020, 13:36:41 UTC
d750dc3 François Dupressoir15 June 2020, 15:10:39 UTCFix merge problem15 June 2020, 15:10:39 UTC
66c830f François Dupressoir15 June 2020, 14:55:33 UTCClean 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 Pierre-Yves Strub10 June 2020, 17:03:25 UTCDo no search for rewriting patterns modulo conversion.10 June 2020, 17:03:25 UTC
41d0d08 Pierre-Yves Strub10 June 2020, 14:44:03 UTCTheory 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 Pierre-Yves Strub10 June 2020, 14:13:50 UTCFix compilation10 June 2020, 14:13:50 UTC
c9641e4 Pierre-Yves Strub10 June 2020, 09:53:25 UTCRevert "Add user reductions for iteri" This reverts commit f693233ec9a7b33ba350d7b17e1d223f33d7fb56.10 June 2020, 09:53:35 UTC
bacb90b Benjamin Gregoire10 June 2020, 08:02:11 UTCin rewrite find occurences using alpha conversion first.10 June 2020, 09:41:40 UTC
ab61883 Benjamin Gregoire10 June 2020, 07:46:56 UTCadd reduction for -i = i'10 June 2020, 07:47:46 UTC
19c6c50 Benjamin Gregoire10 June 2020, 07:45:48 UTCremove duplicate declaration10 June 2020, 07:47:46 UTC
6965ea6 Pierre-Yves Strub10 June 2020, 07:46:26 UTCbinomial law + basic lemmas (full / support)10 June 2020, 07:46:26 UTC
2064617 Pierre-Yves Strub10 June 2020, 07:28:45 UTC"search" now works with notations [fix #17317]10 June 2020, 07:28:49 UTC
763732a Benjamin Gregoire09 June 2020, 15:43:37 UTCsmt: do not filter wanted lemma09 June 2020, 15:43:43 UTC
f693233 Pierre-Yves Strub09 June 2020, 15:39:58 UTCAdd user reductions for iteri09 June 2020, 15:39:58 UTC
23b938a Pierre-Yves Strub09 June 2020, 11:32:57 UTCRefactor & 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 Pierre-Yves Strub08 June 2020, 17:14:32 UTCSome 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 Benjamin Gregoire27 May 2020, 13:08:56 UTCadd lemmas on bigi27 May 2020, 13:11:27 UTC
53ed919 Alley Stoughton22 May 2020, 22:12:19 UTCAllows 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 Benjamin Gregoire27 April 2020, 12:23:05 UTCfix default.nix27 April 2020, 12:23:05 UTC
58aaed4 AntoineSere20 April 2020, 17:02:04 UTCMerge pull request #42 from AntoineSere/eqvquo Added two useful lemmas to Quotient.ec20 April 2020, 17:02:04 UTC
ce4d827 Antoine Séré20 April 2020, 15:04:39 UTCAdded two useful lemmas to Quotient.ec20 April 2020, 15:04:39 UTC
acfd4ea Pierre-Yves Strub16 April 2020, 14:56:46 UTCDefinition of quotient types w.r.t. a equivalence relation16 April 2020, 14:56:46 UTC
60a7d34 Pierre-Yves Strub16 April 2020, 13:19:34 UTCFinite groups, cyclic groups, Bezout.16 April 2020, 13:19:53 UTC
cdb2e6f François Dupressoir16 April 2020, 10:45:54 UTCUse arrow-based assignments This is to align standard libraries with 1.0-preview, which forbids '='16 April 2020, 10:45:54 UTC
f44260c Pierre-Yves Strub16 April 2020, 09:41:06 UTCstdlib: distributions: dmap1E_can16 April 2020, 09:41:06 UTC
94786bc Pierre-Yves Strub16 April 2020, 09:40:44 UTCstdlib: List: nth_default16 April 2020, 09:40:44 UTC
136b237 Pierre-Yves Strub15 April 2020, 09:39:30 UTClemma: fun_ext215 April 2020, 09:39:30 UTC
5eba66b Pierre-Yves Strub15 April 2020, 09:31:23 UTCallow writing m.[i, j] in place of m.[(i, j)]15 April 2020, 09:31:23 UTC