https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
ce01988 allow cost precondition in rcondf, rcondt and if tactics 19 June 2020, 11:54:46 UTC
aac1558 additional simplifications of cost 12 June 2020, 15:52:02 UTC
92a2cd9 simplification of cost judgments for datatypes and tuples. 12 June 2020, 15:43:12 UTC
88200ac Fix cloning of user reduction (put the correct mode) 02 June 2020, 14:51:20 UTC
556c55d small fixes 02 June 2020, 14:50:06 UTC
8133669 small fixes 02 June 2020, 14:16:53 UTC
b9abebe cloning now supports schemas 02 June 2020, 14:13:38 UTC
8a3eafb Merge branch '1.0' into deploy-cost 28 May 2020, 07:57:19 UTC
3e8c6b5 fix bug 27 May 2020, 13:14:25 UTC
6e5bd45 add lemmas on bigi 27 May 2020, 13:14:25 UTC
6bc158c improved restr. printing 27 May 2020, 08:53:50 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
096de75 example of a section in the small tutorial. Also removed the debugging info when printing choare judgements. 28 April 2020, 13:14:33 UTC
974c7fb cleanup some old comments 28 April 2020, 13:08:08 UTC
fe1193a memory printing printed in a better order. 28 April 2020, 13:02:37 UTC
eee8d28 minor pretty printer improvements. 28 April 2020, 12:55:46 UTC
be2bf40 import BIA for shorter paths, + minor change. 28 April 2020, 12:55:15 UTC
1311f7b short syntax for abs. calls with invariant when there is no oracle. 28 April 2020, 12:30:38 UTC
b7463b6 Fixed shift/reduce conflicts 28 April 2020, 12:01:53 UTC
0ce118f bugs 28 April 2020, 11:13:08 UTC
c55ebb4 Merge remote-tracking branch 'origin/1.0' into deploy-cost 28 April 2020, 11:05:08 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
b8e9ba6 renamed files 20 April 2020, 10:49:51 UTC
a3cd411 work on FO. 16 April 2020, 15:36:20 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
56b5594 FO 14 April 2020, 14:28:52 UTC
f3581d5 binomial coefficients 10 April 2020, 09:56:42 UTC
eb9b026 CI: move to slack notification 09 April 2020, 16:22:07 UTC
21e8fce CI: move to slack notification 09 April 2020, 16:21:20 UTC
ffe2fd6 Matching issue 09 April 2020, 14:45:34 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
ad74e06 minor printing change 09 April 2020, 12:24:40 UTC
cb5a4f9 fixed BR example. 09 April 2020, 12:22:30 UTC
1eca4b1 Proof obligation generated only if necessary + error message. 09 April 2020, 11:52:57 UTC
39d94f3 bug fix for free variables and pretty printing. 09 April 2020, 10:44:27 UTC
e0898d5 bug fix 09 April 2020, 08:58:38 UTC
589e509 splitted proof obligations 09 April 2020, 08:30:25 UTC
2fd58e3 Matching for choaref 09 April 2020, 08:30:09 UTC
75af940 matching for Pr 09 April 2020, 08:08:11 UTC
a9eb399 matching for *hoareF 09 April 2020, 08:08:11 UTC
21354f7 default.nix: adding installFlags 08 April 2020, 15:23:25 UTC
c331657 cleanup 08 April 2020, 15:20:57 UTC
9c85231 examples changes 08 April 2020, 13:03:17 UTC
daeacbd Alternative simpler syntax for cost judgement with true ==> true. 08 April 2020, 11:45:55 UTC
35475fa Bug fx + updated examples. 08 April 2020, 11:04:05 UTC
87273a4 printing improvement 08 April 2020, 10:37:25 UTC
952baf6 Apply on module with restrictions. 07 April 2020, 15:54:32 UTC
0e73f5c Proof obligation when applying a forall on a restricted module. 07 April 2020, 10:31:37 UTC
4193812 Merge remote-tracking branch 'origin/1.0' into deploy-cost 06 April 2020, 16:18:19 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
ea602f8 Changed oracle restrictions in module type. Default to zero. 26 March 2020, 16:40:42 UTC
2a5b4f6 Only accepts Alt-Ergo from version 2.3.1 26 March 2020, 07:42:17 UTC
098adb2 Fix previous merge 25 March 2020, 09:09:46 UTC
ab9b383 Merge remote-tracking branch 'origin/1.0' into deploy-cost 24 March 2020, 17:45:32 UTC
c5c3324 instantiation rule for choare judgement 24 March 2020, 14:20:23 UTC
285fdb7 started implementing choare instantiation rule 23 March 2020, 17:07:05 UTC
e7dfa75 progress for choare judgement: remains to update apply 23 March 2020, 15:21:01 UTC
99a37b4 decreasing quantity in while tactic: cost.ec fix 23 March 2020, 15:20:37 UTC
61ef975 choare are only for abstract calls. 23 March 2020, 14:12:14 UTC
fa4d0e4 small cleanup 23 March 2020, 09:01:10 UTC
29fd288 Correct parsing of memory restrictions. 19 March 2020, 17:02:04 UTC
9bc4cf8 Bug fix, empty restrictions were not properly handled. 19 March 2020, 16:45:59 UTC
3601773 while with decreasing quantity 19 March 2020, 16:30:59 UTC
f3b1f7f Small precision improvement. Added the invariant to the cost of while loop conditions 19 March 2020, 15:59:54 UTC
79619e4 Rnd tactic fix: lossless precondition was forgotten. 19 March 2020, 15:57:37 UTC
928a0fa use max for cost of if statements 19 March 2020, 15:45:56 UTC
7f9f6f8 Minor 19 March 2020, 15:06:49 UTC
0106a13 small parser improvement + bug fix 18 March 2020, 12:58:39 UTC
b694564 parser bug fix + updated examples. 18 March 2020, 11:40:29 UTC
aaf4070 Added memory predicate variables in schemata 18 March 2020, 11:32:24 UTC
e182b0c Adding memory predicate variables in schemata + better reduce_user 17 March 2020, 17:33:24 UTC
980d84b Bug fix. 17 March 2020, 12:17:23 UTC
f9c15b9 examples + br93 done + small fix in while tactic. 17 March 2020, 11:50:46 UTC
309e263 find as while 16 March 2020, 18:13:28 UTC
b0f81e3 started replacing the list by a while. 16 March 2020, 15:01:02 UTC
cbab513 Added an optional precondition to the wp tactic. 16 March 2020, 13:24:18 UTC
9127e98 Revert "To be reverted." This reverts commit c12ce5a9d6a461c2345f2cd76aaf676d1a6ea4e3. 16 March 2020, 09:08:58 UTC
22799f1 In `rewrite`, use a keyed matching algorithm for finding occurences. 28 February 2020, 06:49:27 UTC
c12ce5a To be reverted. 27 February 2020, 13:18:44 UTC
ad1aa95 Minor 26 February 2020, 18:23:24 UTC
ad8432b Can use hint simplify with schema containing costs. Note that this is somehow limited (no matching in cost judgements' precondition). 26 February 2020, 17:26:13 UTC
c28125a Corrected a bug with schema instantiations. Expression variable in cost judgemement's preconditions were not substituted. 26 February 2020, 14:31:32 UTC
38e6067 Printing improvement. 26 February 2020, 14:30:37 UTC
f9ad123 Simplify automatically free costs. 25 February 2020, 18:07:51 UTC
71fded7 Various bugfix. 25 February 2020, 14:26:12 UTC
8b59df9 Fleshing out the BR93 example. 20 February 2020, 17:18:16 UTC
back to top