https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
63acd50 prelude 21 November 2020, 08:36:44 UTC
005b915 removing trash 21 November 2020, 08:33:24 UTC
6b5f126 Merge branch '1.0' into deploy-sem 21 November 2020, 08:32:07 UTC
a08bc34 Stdlib: more results on Rn + bigops on Rn 21 November 2020, 08:29:35 UTC
aa23a23 Merge branch '1.0' into deploy-sem 21 November 2020, 00:14:56 UTC
7a42484 MANIFEST 21 November 2020, 00:14:50 UTC
f1c7e6c 21 November 2020, 00:04:19 UTC
41fc92c Merge branch 'deploy-Rn-norm' into deploy-sem 20 November 2020, 22:20:42 UTC
e6f1612 Merge branch '1.0' into deploy-Rn-norm 20 November 2020, 22:20:28 UTC
564138c fix compilation 20 November 2020, 22:20:12 UTC
d7b7663 Merge branch '1.0' into deploy-sem 20 November 2020, 22:16:50 UTC
07b937c Small addititions on distributions 20 November 2020, 22:16:40 UTC
553c47e fix sem w.r.t. non-constant bounds 20 November 2020, 22:15:00 UTC
357b1ac Merge branch 'deploy-Rn-norm' into deploy-sem 20 November 2020, 21:48:16 UTC
dffed1c BigRn 20 November 2020, 21:47:25 UTC
bba08b8 Merge branch '1.0' into deploy-Rn-norm 20 November 2020, 15:00:08 UTC
bc2e009 Merge branch '1.0' into deploy-sem 20 November 2020, 14:47:28 UTC
6f68e27 More results on distributions (conditional exp, Jensen (finite)) 20 November 2020, 14:45:54 UTC
bd805ad Merge branch 'deploy-stdlib' into deploy-sem 20 November 2020, 13:38:29 UTC
fb2bb00 bigops 20 November 2020, 13:36:51 UTC
d053425 Merge branch 'deploy-stdlib' into deploy-sem 20 November 2020, 12:59:45 UTC
5487ca0 20 November 2020, 12:59:26 UTC
b28b522 Merge branch 'deploy-stdlib' into deploy-sem 20 November 2020, 12:57:44 UTC
13dedd4 more on distributions 20 November 2020, 12:56:47 UTC
b41cd3b 20 November 2020, 12:34:13 UTC
21dfae2 Merge branch 'deploy-Rn-norm' into deploy-sem 18 November 2020, 08:36:56 UTC
0e53475 fixing admits 18 November 2020, 08:35:45 UTC
2ec6a2b Merge branch '1.0' into deploy-Rn-norm 18 November 2020, 06:02:07 UTC
27ff637 integrating more results on distributions 18 November 2020, 06:00:50 UTC
75d479c Merge branch 'deploy-Rn-norm' into deploy-sem 17 November 2020, 20:24:28 UTC
c98e650 17 November 2020, 20:24:18 UTC
a299ef5 Merge remote-tracking branch 'origin/1.0' into deploy-Rn-norm 17 November 2020, 20:22:54 UTC
8d01a80 fix CBC 17 November 2020, 17:48:08 UTC
25f0ae3 reallim 17 November 2020, 16:12:12 UTC
8fb9e9b Merge branch 'deploy-Rn-norm' into deploy-sem 17 November 2020, 14:37:01 UTC
09988f6 more result on the Rn norm 17 November 2020, 14:36:35 UTC
3633c58 Merge branch 'deploy-stdlib-distr' into deploy-sem 17 November 2020, 14:31:33 UTC
415a437 integrating more results on distributions 17 November 2020, 14:31:11 UTC
aa70a2d 17 November 2020, 14:10:44 UTC
25bf1c2 Merge branch '1.0' into deploy-sem 17 November 2020, 12:21:23 UTC
ed25190 small generalization of PRP 16 November 2020, 10:58:31 UTC
8cb3e88 extend conseq rules: equivF => hoareF => hoareF and equivF => phoareF => phoareF 13 November 2020, 11:33:47 UTC
4391b04 basic results about minr 12 November 2020, 11:00:16 UTC
61de4b9 Fix "smt debug" 12 November 2020, 08:24:20 UTC
b360fa8 Fix bug in conseq 11 November 2020, 05:56:42 UTC
ffad375 New option for SMT: "debug" 03 November 2020, 09:04:00 UTC
4ef4286 Fix dfold s.t. the functor takes the index 21 October 2020, 08:49:24 UTC
d0a9c09 remove notations for mget/mset 21 October 2020, 04:14:33 UTC
19c7285 New operator: dfold 20 October 2020, 09:40:14 UTC
1a75b3b name + red 20 October 2020, 09:29:06 UTC
5c251d1 Fsem constructor 19 October 2020, 09:01:38 UTC
fa3853d README (nix) 15 October 2020, 10:30:04 UTC
bc4f6df "={_}" now supports the construction "glob M \ { p1, p2, ... }" It stands for "glob M" without "p1, p2, ..." 15 October 2020, 08:39:16 UTC
22a8b51 better printing of modules bodies w.r.t. "import var" 14 October 2020, 09:10:10 UTC
ca1f0d2 The command "import var" is now allowed at top-level 14 October 2020, 07:08:46 UTC
b34c174 add alias "include var" that stands for "include" then "import var" 14 October 2020, 06:55:56 UTC
c3114bd "import var" now takes a space-separated list of modules 14 October 2020, 06:52:22 UTC
4268b0f New 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 Docker image: bump provers versions 11 October 2020, 07:27:44 UTC
7d8a513 Help 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.2 10 October 2020, 12:08:14 UTC
469a12a easycrypt why3config uses --full-config 09 October 2020, 16:20:54 UTC
ef6f0ba README: add --full-config option (why3 config) 09 October 2020, 15:44:59 UTC
6d31cc5 Update Dockerfile w.r.t new EasyCrypt repo layout 09 October 2020, 15:44:32 UTC
e664da3 Docker: do not use easycrypt remote anymore 09 October 2020, 11:02:44 UTC
ce70fa4 opam: change post-install message 09 October 2020, 10:23:24 UTC
6c03840 Fix travis configuration file w.r.t recent changes 09 October 2020, 10:21:16 UTC
44a728a Update README (no more external opam repo) & add missing opam fields 09 October 2020, 10:16:58 UTC
e37a10c Import opam file s.t. travis can use it to update its dependencies 09 October 2020, 08:41:05 UTC
c436fd4 Travis: update EasyCrypt dependencies before running tests 09 October 2020, 08:41:05 UTC
730f329 default.nix: remove restriction on Why3 version 09 October 2020, 08:41:05 UTC
8f33b95 First attempt at handling Why3 1.3.X 09 October 2020, 08:41:05 UTC
3007982 fix default.nix 14 September 2020, 13:36:41 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
back to top