https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
221e1b2 Merge branch '1.0' into 1.0-preview 10 October 2020, 10:47:31 UTC
933e315 Merge branch '1.0' into 1.0-preview 10 October 2020, 10:34:11 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
d3fc323 Fix merge problem 16 June 2020, 09:51:05 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
25bcf42 Merge branch '1.0' into 1.0-preview 10 June 2020, 17:05:57 UTC
86a9bf3 Merge branch 'deploy-rewrite' into 1.0-preview 10 June 2020, 17:05:33 UTC
734e5bb Do no search for rewriting patterns modulo conversion. 10 June 2020, 17:03:25 UTC
7c9f3ad Merge branch '1.0' into deploy-rewrite 10 June 2020, 16:51:38 UTC
13b70b3 10 June 2020, 16:28:11 UTC
433e5ba 10 June 2020, 15:06:40 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
9909f4d 10 June 2020, 14:43:30 UTC
e6a9d11 Merge branch 'deploy-rewrite' into 1.0-preview 10 June 2020, 14:34:02 UTC
502db3d change behavior of rewrite !? 10 June 2020, 14:33:42 UTC
2e45603 Merge branch 'deploy-rewrite' into 1.0-preview 10 June 2020, 14:16:36 UTC
65f0514 Merge branch 'deploy-theory-matrix-ring' into deploy-rewrite 10 June 2020, 14:14:30 UTC
74142f2 Merge branch '1.0' into deploy-theory-matrix-ring 10 June 2020, 14:14:07 UTC
4b965ee Fix compilation 10 June 2020, 14:13:50 UTC
8057e61 Merge branch '1.0' into deploy-theory-matrix-ring 10 June 2020, 14:10:55 UTC
2558d8a 10 June 2020, 14:09:28 UTC
21da82c test 10 June 2020, 12:40:16 UTC
9a1afd8 Merge branch '1.0' into 1.0-preview 10 June 2020, 09:53:55 UTC
c9641e4 Revert "Add user reductions for iteri" This reverts commit f693233ec9a7b33ba350d7b17e1d223f33d7fb56. 10 June 2020, 09:53:35 UTC
bcb430c Merge branch '1.0' into 1.0-preview 10 June 2020, 09:44:14 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
c595f3c Merge branch '1.0' into 1.0-preview 10 June 2020, 07:46:49 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
b915e29 Merge branch 'deploy-theory-matrix-ring' into 1.0-preview 09 June 2020, 16:09:22 UTC
3a942c7 fix compilation 09 June 2020, 16:09:00 UTC
4a33a26 Merge branch '1.0' into deploy-theory-matrix-ring 09 June 2020, 16:05:23 UTC
3090828 Merge branch '1.0' into 1.0-preview 09 June 2020, 16:05:14 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
03d203a 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:34:24 UTC
63b4818 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> 09 June 2020, 11:34:24 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
6018240 Merge branch '1.0' into 1.0-preview 09 June 2020, 05:28:48 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
d143056 Merge branch '1.0' into 1.0-preview 26 May 2020, 12:22:58 UTC
ad888b8 Make nosmt operator change on get_as_ operators. 26 May 2020, 12:18:55 UTC
f6e775f 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, 12:18:55 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
286df20 Merge branch 'deploy-theory-matrix-ring' into 1.0-preview 16 May 2020, 07:09:16 UTC
4f38720 more results on matrices 16 May 2020, 06:57:58 UTC
bcc7239 Merge branch '1.0' into deploy-theory-matrix-ring 14 May 2020, 12:45:40 UTC
170c443 fix default.nix 27 April 2020, 12:23:05 UTC
7fa0fc1 Merge branch 'deploy-new-rom' into 1.0-preview 23 April 2020, 14:46:50 UTC
27fcbdc Merge branch '1.0' into 1.0-preview 21 April 2020, 14:45:19 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
c620224 leverage PROM in ROM 16 April 2020, 11:09:05 UTC
43f5e2c New PROM to serve as foundation for all ROM proofs 16 April 2020, 11:08:27 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
c2e1b8f Merge branch 'deploy-theory-matrix-ring' into 1.0-preview 16 April 2020, 09:54:20 UTC
e05cb75 Merge branch '1.0' into 1.0-preview 16 April 2020, 09:54:14 UTC
43d84a5 Matrix.eca: kill admits 16 April 2020, 09:53:57 UTC
09eb21d Merge branch '1.0' into deploy-theory-matrix-ring 16 April 2020, 09:52:51 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
05e3caf Merge branch 'deploy-theory-matrix-ring' into 1.0-preview 16 April 2020, 06:34:14 UTC
f21502a vector/matrix & matrix/vector multiplication + L/R-module lemmas 16 April 2020, 06:33:53 UTC
e71f5fe Merge branch 'deploy-theory-matrix-ring' into 1.0-preview 15 April 2020, 19:08:08 UTC
40ed14d dmatrix 15 April 2020, 19:07:39 UTC
557fc21 square matrices from a non-commutative ring 15 April 2020, 12:39:10 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
88814a4 Merge branch '1.0' into 1.0-preview 10 April 2020, 09:57:07 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
bafcc56 Merge branch '1.0' into 1.0-preview 08 April 2020, 07:28:44 UTC
149b09f User error message for map-style lvalue on unsupported assignment [fix #17412] 28 March 2020, 08:13:21 UTC
527749b fix SecureChannel 27 March 2020, 08:11:36 UTC
f7f2a54 kill admits 27 March 2020, 08:10:49 UTC
13eeceb Merge branch '1.0' into 1.0-preview 26 March 2020, 19:56:08 UTC
b1b35e6 Internal: remove LvMap lvalue. 26 March 2020, 19:52:54 UTC
back to top