EasyCrypt: Ticket Query
https://www.easycrypt.info/trac/query?status=assigned&status=new&status=accepted&status=reopened&milestone=1.0&group=status&order=priority
EasyCrypt: Computer-Aided Cryptographic Proofsen-USEasyCrypthttps://www.easycrypt.info/trac/chrome/site/easycrypt.png
https://www.easycrypt.info/trac/query?status=assigned&status=new&status=accepted&status=reopened&milestone=1.0&group=status&order=priority
Trac 1.2
https://www.easycrypt.info/trac/ticket/17378
https://www.easycrypt.info/trac/ticket/17378#17378: Proof of false using smt and Eprover.Sun, 29 Apr 2018 20:18:29 GMTsolvei<pre class="wiki">require import Int Real RealExp.
op n : int.
op q : {int | 0 <> q} as q_.
lemma test1 x : x = n%r / q%r => false.
proof.
smt t=5 p=["Eprover"].
qed.
lemma test2 : false.
proof.
pose x := n%r / q%r.
smt t=5 p=["Eprover"].
qed.
</pre><p>
Tested with Eprover version 1.9.1 and 2.0.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17378#changelog
https://www.easycrypt.info/trac/ticket/17141
https://www.easycrypt.info/trac/ticket/17141#17141: Wrong module type annotations acceptedFri, 19 Dec 2014 18:03:11 GMTDominique Unruh<p>
<code>module M:T = { ... }.</code> does not completely check whether the judgement M:T is correct.
(It overlooks that some functions need to be initializers.)
</p>
<p>
The bug seems to be cosmetic only, because the wrong judgement does not seem to be used for deciding whether a module can be used in a given place.
</p>
<p>
See the example below.
</p>
<pre class="wiki">require import Int.
module type T={
proc * f():unit
}.
(* The typing judgement M:T should not be accepted.
f() does not x, but is declared as an initializer in type T. *)
module M:T = {
var x:int
proc f():unit = {}
}.
(* An example lemma *)
lemma test (N<:T): equiv [ N.f ~ N.f : true ==> ={glob N} ].
proc*.
call (_:true).
auto.
qed.
lemma test2: equiv [ M.f ~ M.f : true ==> ={M.x} ].
(* The following is rejected, fortunately.
(Otherwise we would prove a false lemma.)
But it should be accepted according to the incorrect
typing judgement M:T above. *)
apply (test M).
qed.
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17141#changelog
https://www.easycrypt.info/trac/ticket/17024
https://www.easycrypt.info/trac/ticket/17024#17024: Pattern matching should try to infer memory and module parametersMon, 16 Jun 2014 12:41:15 GMTPierre-Yves StrubResultshttps://www.easycrypt.info/trac/ticket/17024#changelog
https://www.easycrypt.info/trac/ticket/17034
https://www.easycrypt.info/trac/ticket/17034#17034: Generalizing loop fusionTue, 01 Jul 2014 10:11:17 GMTFrançois Dupressoir<p>
Currently, loop fusion tries to syntactically check that the statements that are separated are in fact independent. This is very far from being sufficient when the loops write into arrays: the syntactic check is performed at variable-level, and SMTs may in general be needed to check it in a finer-grained way.
</p>
<p>
The objective is, for example, to be able to prove that the two statements below are equivalent.
</p>
<pre class="wiki">u = set0<:T>;
i = 0;
while (i < n) {
index[i] = $T \ u;
u = u U {index[i]};
m[index[i]] = $T';
i = i + 1;
}
</pre><pre class="wiki">u = set0<:T>;
i = 0;
while (i < n) {
index[i] = $T \u;
u = u U {index[i]};
i = i + 1;
}
i = 0;
while (i < n) {
m[index[i]] = $T';
i = i + 1;
}
</pre><p>
Generalizing, we want to prove
</p>
<pre class="wiki">init
while (i < n) {
c(i)
c'(i)
i = i + 1;
}
</pre><p>
equivalent to
</p>
<pre class="wiki">init
while (i < n) {
c(i)
i = i + 1;
}
init
while (i < n) {
c'(i)
i = i + 1;
}
</pre><p>
To do so, it is sufficient to prove that, for all i, j such that j < i, we have
<code>c(i); c'(j); ~ c'(j); c(i);</code>. This guarantees that we can move <code>c'(i);</code> all the way up through higher iterations of the c-loop to be joined with <code>c(i);</code>.
</p>
<p>
In addition, we of course need to know that neither c nor c' modify the loop index and that nor c or c' modify the effect of init.
</p>
<p>
A quick opinion: the current syntactic check could be replaced with "generating the proof obligation as above and using <code>swap</code> to discharge the proof obligation". If it succeeds, we are happy. If it fails, we give the proof obligation to the user and let her discharge it automatically.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17034#changelog
https://www.easycrypt.info/trac/ticket/17040
https://www.easycrypt.info/trac/ticket/17040#17040: Syntactic sugar for nested if-then-else statements.Sat, 12 Jul 2014 22:07:42 GMTPierre-Yves StrubResultshttps://www.easycrypt.info/trac/ticket/17040#changelog
https://www.easycrypt.info/trac/ticket/17042
https://www.easycrypt.info/trac/ticket/17042#17042: Pattern matching in non-normal form.Mon, 14 Jul 2014 13:38:14 GMTMarkulf Kohlweiss<p>
Support for pattern matching in non-normal form should be added to <a class="missing wiki">EasyCrypt?</a>. This includes: wild pattern matching (_), deep pattern matching (C (C x)), or'ed pattern matching (C x | D x => ...)
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17042#changelog
https://www.easycrypt.info/trac/ticket/17070
https://www.easycrypt.info/trac/ticket/17070#17070: better error message when difference between goal and lemma is tinyThu, 09 Oct 2014 20:29:35 GMTAlley Stoughton<p>
I've had some frustrating experiences with [apply] when the difference between the goal and the statement of the lemma I'm applying is tiny, but the goal is large. At first glance, in fact, it's looked like they were identical. (Once I had "tagLen" in one, and "secLen" in the other, and it took me a while to spot the difference.) Instead of the "unable to apply lemma" message, it would be great to be told something more informative. One possibility is to print the two formulas and assert they are different. This would help one differentiate this situation from one where something else was preventing the lemma from being applied. Even better would be to point out the position of difference in the two formulas. Of course, this only makes sense when they are almost the same.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17070#changelog
https://www.easycrypt.info/trac/ticket/17195
https://www.easycrypt.info/trac/ticket/17195#17195: Swap with 2 args move as far down as possibleTue, 02 Jun 2015 18:44:42 GMTBrent Carmer<p>
It would be convenient for swap to have a default behavior of moving a particular line as far down as its dependencies will allow.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17195#changelog
https://www.easycrypt.info/trac/ticket/17250
https://www.easycrypt.info/trac/ticket/17250#17250: off-by-one error in swapThu, 24 Sep 2015 20:28:22 GMTAlley Stoughton<p>
Here's an off-by-one error involving <code>swap</code>:
</p>
<pre class="wiki">module M = {
var x : bool
proc f() : unit = {
x <- true;
}
}.
lemma X :
equiv[M.f ~ M.f : ={M.x} ==> ={M.x}].
proof.
proc.
swap 1 -1.
(* the above should fail -- seems
to be an off-by-one error;
the corresponding positive
case *does* fail: *)
swap 1 1.
(* error:
invalid position, 1 <= 1 < 2 <= 2 <= 1
perhaps not the best error message, though ;-) *)
</pre><p>
And the following, in my opinion, should also fail:
</p>
<pre class="wiki">module M = {
var x : bool
proc f() : unit = {
}
}.
lemma X :
equiv[M.f ~ M.f : ={M.x} ==> ={M.x}].
proof.
proc.
swap 1 0.
(* I would think the above should
fail, because it seems to
refer to a statement (1) that
doesn't exist;
I've documented swap saying this fails *)
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17250#changelog
https://www.easycrypt.info/trac/ticket/17309
https://www.easycrypt.info/trac/ticket/17309#17309: `rewrite /F` when F is a fixpoint should simplify selected occurence for head-iota reduction.Tue, 12 Apr 2016 08:41:11 GMTtomsib2001Resultshttps://www.easycrypt.info/trac/ticket/17309#changelog
https://www.easycrypt.info/trac/ticket/17392
https://www.easycrypt.info/trac/ticket/17392#17392: problems with glob and delta and matchingSat, 27 Jul 2019 23:28:26 GMTAlley Stoughton<p>
Here is an example where delta infinite-loops:
</p>
<pre class="wiki">type t = [ First | Second of int & int & int ].
module M = {
var x : t
}.
op f (g : glob M) : int =
match g with
First => 2
| Second _ _ _ => 1
end.
lemma ge0_f (g : glob M) : 0 <= f g.
proof.
delta.
</pre><p>
The above infinite-loops:
</p>
<pre class="wiki">Current goal
Type variables: <none>
g : (glob M)
------------------------------------------------------------------------
[error-0-0]anomaly: File "src/ecUtils.ml", line 234, characters 24-30: Assertion failed
0 < [7|check]>
interrupted
</pre><p>
And here is a related example that produces an anomaly:
</p>
<pre class="wiki">type t = [ First | Second of int & int ].
module M = {
var x : t
var y : t
}.
op f (g : glob M) : int =
match g.`1 with
First => 2
| Second _ _ => 1
end.
lemma ge0_f (g : glob M) : 0 <= f g.
proof.
delta.
case g.`1.
(*
g : (glob M)
------------------------------------------------------------------------
0 < match First with | First => 2 | Second (_, _) => 1 end \/
0 = match First with | First => 2 | Second (_, _) => 1 end
*)
trivial.
</pre><p>
The above fails with:
"anomaly: File "src/ecCallbyValue.ml", line 433, characters 14-20: Assertion failed". And the pretty-printing of Second is faulty, as it doesn't take a pair.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17392#changelog
https://www.easycrypt.info/trac/ticket/16113
https://www.easycrypt.info/trac/ticket/16113#16113: <top> in printerMon, 22 Jul 2013 23:53:00 GMTGuillaume Davy<p>The following example generates a printer bug maybe a more internal bug<br/>
</p><p>module type T = { fun f():unit }.<br/>
</p><p>module M(A:T) : T = {<br/>
var b : int<br/>
fun f() : unit = { A.f(); }<br/>
}.<br/>
</p><p>module N(M:T) = {<br/>
</p><p>fun f() : unit = {M.f();}<br/>
}.<br/>
</p><p>equiv eq (A<:T) : A.f ~ A.f : ={glob A} ==> ={res} by fun true=> //.<br/>
</p><p>equiv bug (A<:T) : N(M(A)).f ~ N(M(A)).f : ={glob M,glob A} ==> ={res}.<br/>
fun.<br/>
call (eq (M(A))).<br/>
skip.<br/>
qed.<br/>
</p>Resultshttps://www.easycrypt.info/trac/ticket/16113#changelog
https://www.easycrypt.info/trac/ticket/17181
https://www.easycrypt.info/trac/ticket/17181#17181: slow rewriting for large expressionsWed, 04 Mar 2015 11:36:09 GMTBenedikt Schmidt<p>
In the arithmetica repo, there are some examples of slow rewriting (e.g., Limbs2:216 in rev <a class="missing changeset" rel="nofollow" title="No changeset b06471db76ca00d1e2b99de0437afff03aede512 in the repository">b06471db76ca00d1e2b99de0437afff03aede512</a>). The expressions are large and contain many deeply nested occurrences of a small number of function symbols (e.g., add).
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17181#changelog
https://www.easycrypt.info/trac/ticket/17194
https://www.easycrypt.info/trac/ticket/17194#17194: anomaly: EcHiGoal.LowApply.NoInstance (in byequiv)Mon, 25 May 2015 11:03:53 GMTDominique Unruh<p>
The following code raises <code>anomaly: EcHiGoal.LowApply.NoInstance</code>.
</p>
<pre class="wiki">require import Real.
require import Bool.
module M = {
proc f():bool = {
return true;
}
}.
lemma test &m:
Pr[M.f() @ &m : res]
<=
Pr[M.f() @ &m : res]
+
Pr[M.f() @ &m : true].
byequiv.
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17194#changelog
https://www.easycrypt.info/trac/ticket/17207
https://www.easycrypt.info/trac/ticket/17207#17207: Applicative viewWed, 24 Jun 2015 08:35:11 GMTPierre-Yves Strub<p>
The applicative view <code>/(_ v1 ... vn)</code> applies the top-assumption to <code>v1...vn</code>.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17207#changelog
https://www.easycrypt.info/trac/ticket/17222
https://www.easycrypt.info/trac/ticket/17222#17222: local clones do not disappear from the environment on section endTue, 21 Jul 2015 14:59:57 GMTFrançois Dupressoir<pre class="wiki">theory T.
type t.
op Z: t.
op o: t -> t -> t.
end T.
section S.
local clone T as T1.
end section S.
section S'.
local clone T as T1. (* the symbol T1 already exists *)
end section S'.
</pre><p>
Since nothing about "<code>S.T1</code>" leaves the scope of <code>S</code>, I expect it should be possible to remove "<code>S.T1</code>" from the environment when exiting <code>S</code>.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17222#changelog
https://www.easycrypt.info/trac/ticket/17240
https://www.easycrypt.info/trac/ticket/17240#17240: Syntactic sugar for proc. that reduces to a call to an external proc.Mon, 07 Sep 2015 10:36:21 GMTPierre-Yves Strub<p>
A procedure def. like:
</p>
<pre class="wiki">proc foo(x, y) = {
var aout;
aout <@ bar(x+y, x-y);
return aout;
</pre><p>
should be writable as:
</p>
<pre class="wiki">proc foo(x, y) = bar(x+y, x-y)
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17240#changelog
https://www.easycrypt.info/trac/ticket/17255
https://www.easycrypt.info/trac/ticket/17255#17255: Missing unification in `clone...with...`Thu, 22 Oct 2015 15:15:05 GMTPierre-Yves Strub<p>
The instantiation body of op/pred of clone specs. should be unified with the expected types.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17255#changelog
https://www.easycrypt.info/trac/ticket/17256
https://www.easycrypt.info/trac/ticket/17256#17256: apply/rewrite should work modulo zeta-reduction.Sun, 25 Oct 2015 06:39:14 GMTPierre-Yves StrubResultshttps://www.easycrypt.info/trac/ticket/17256#changelog
https://www.easycrypt.info/trac/ticket/17261
https://www.easycrypt.info/trac/ticket/17261#17261: `rewrite -/(f _)` should not match its own unfoldings.Wed, 04 Nov 2015 10:44:00 GMTPierre-Yves StrubResultshttps://www.easycrypt.info/trac/ticket/17261#changelog
https://www.easycrypt.info/trac/ticket/17262
https://www.easycrypt.info/trac/ticket/17262#17262: Add the possibility to add rewrite hints to rewrite hint databases.Sun, 08 Nov 2015 09:48:31 GMTPierre-Yves Strub<p>
For example:
</p>
<pre class="wiki">hint rewrite ler_add2 : ler_add2l ler_add2r.
hint rewrite ltr_add2 : ltr_add2l ltr_add2r.
hint rewrite lter_add2 : ler_add2 ltr_add2.
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17262#changelog
https://www.easycrypt.info/trac/ticket/17263
https://www.easycrypt.info/trac/ticket/17263#17263: Multiple incompleteness in `apply`Sun, 08 Nov 2015 09:54:03 GMTPierre-Yves Strub<p>
The theory Number.eca contains a bunch of <code>apply</code> that should succeed.
</p>
<p>
See the FIXME in Number.eca.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17263#changelog
https://www.easycrypt.info/trac/ticket/17265
https://www.easycrypt.info/trac/ticket/17265#17265: `goal` vernacular commandWed, 11 Nov 2015 13:57:36 GMTPierre-Yves Strub<p>
Add a <code>goal</code> vernacular command (for unnamed lemmas).
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17265#changelog
https://www.easycrypt.info/trac/ticket/17268
https://www.easycrypt.info/trac/ticket/17268#17268: Add a tactical that fails when no progress is done.Wed, 11 Nov 2015 14:19:21 GMTPierre-Yves Strub<p>
Similar to the Coq <code>progress</code> tactic.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17268#changelog
https://www.easycrypt.info/trac/ticket/17269
https://www.easycrypt.info/trac/ticket/17269#17269: Add notations for >/>=Mon, 16 Nov 2015 18:14:44 GMTPierre-Yves Strub<p>
These notations should be "parsing only"
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17269#changelog
https://www.easycrypt.info/trac/ticket/17270
https://www.easycrypt.info/trac/ticket/17270#17270: `done` should close a goal when `false` is a local hyp.Wed, 18 Nov 2015 11:24:16 GMTPierre-Yves StrubResultshttps://www.easycrypt.info/trac/ticket/17270#changelog
https://www.easycrypt.info/trac/ticket/17271
https://www.easycrypt.info/trac/ticket/17271#17271: Pattern matching should solve problems of the form `?f tj...tn ~ f t1 ... tn`Wed, 18 Nov 2015 11:25:12 GMTPierre-Yves StrubResultshttps://www.easycrypt.info/trac/ticket/17271#changelog
https://www.easycrypt.info/trac/ticket/17308
https://www.easycrypt.info/trac/ticket/17308#17308: `rewrite !(A,B)` loops when `B` is not known aboutMon, 14 Mar 2016 14:46:14 GMTBas SpittersResultshttps://www.easycrypt.info/trac/ticket/17308#changelog
https://www.easycrypt.info/trac/ticket/17319
https://www.easycrypt.info/trac/ticket/17319#17319: Anomaly triggered by `smt`Thu, 07 Jul 2016 09:45:23 GMTPierre-Yves Strub<pre class="wiki">require import Perms.
require import List.
lemma perm_test:
mem (Perms.allperms [1;2;3]) [1;2;3].
proof.
smt.
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17319#changelog
https://www.easycrypt.info/trac/ticket/17334
https://www.easycrypt.info/trac/ticket/17334#17334: this message need more information: cannot infer all placeholdersFri, 26 Aug 2016 11:11:46 GMTBenjamin Grégoire<p>
We need a better localisation of the error.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17334#changelog
https://www.easycrypt.info/trac/ticket/17335
https://www.easycrypt.info/trac/ticket/17335#17335: the formula contains free type variablesFri, 26 Aug 2016 11:14:06 GMTBenjamin Grégoire<p>
We need a better localisation of the error:
</p>
<p>
lemma toto x : true.
---> the formula contains free type variables
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17335#changelog
https://www.easycrypt.info/trac/ticket/17117
https://www.easycrypt.info/trac/ticket/17117#17117: Warning when restrictions over an adversary are emptyTue, 25 Nov 2014 08:45:57 GMTPierre-Yves StrubResultshttps://www.easycrypt.info/trac/ticket/17117#changelog
https://www.easycrypt.info/trac/ticket/17160
https://www.easycrypt.info/trac/ticket/17160#17160: Call SMT in parallels.Mon, 19 Jan 2015 16:24:13 GMTPierre-Yves Strub<p>
On !Windows, the maximum of parallel calls to SMT solvers is <code>1</code>. This restriction should be leverage.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17160#changelog
https://www.easycrypt.info/trac/ticket/17253
https://www.easycrypt.info/trac/ticket/17253#17253: EasyCrypt should fail gracefully when applying a tactic on a solved goal.Thu, 15 Oct 2015 21:23:27 GMTPierre-Yves StrubResultshttps://www.easycrypt.info/trac/ticket/17253#changelog
https://www.easycrypt.info/trac/ticket/17264
https://www.easycrypt.info/trac/ticket/17264#17264: Add the possibility to clear lemmas when closing a theory.Sun, 08 Nov 2015 09:55:46 GMTPierre-Yves Strub<p>
This should allow the hiding of internal results.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17264#changelog
https://www.easycrypt.info/trac/ticket/17310
https://www.easycrypt.info/trac/ticket/17310#17310: Top-level command to print various databases (exact, rewrite, ...)Tue, 19 Apr 2016 08:32:14 GMTPierre-Yves StrubResultshttps://www.easycrypt.info/trac/ticket/17310#changelog
https://www.easycrypt.info/trac/ticket/17347
https://www.easycrypt.info/trac/ticket/17347#17347: Search with notations is broken.Fri, 24 Mar 2017 12:19:23 GMTPierre-Yves Strub<p>
For instance, if <code>abbrev f x := ...</code>, <code>search f</code> will search for <code>fun x => f x</code> and finds nothing.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17347#changelog
https://www.easycrypt.info/trac/ticket/17343
https://www.easycrypt.info/trac/ticket/17343#17343: (Optional) warning for old syntaxTue, 07 Feb 2017 22:03:11 GMTPierre-Yves Strub<p>
E.g. for <code>x = v</code> in place of <code>x <- v</code>.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17343#changelog
https://www.easycrypt.info/trac/ticket/17345
https://www.easycrypt.info/trac/ticket/17345#17345: Bad printingFri, 17 Mar 2017 12:55:05 GMTPierre-Yves Strub<p>
See:
</p>
<pre class="wiki">+ added operator mprod ['a, 'b] :
| ('a -> real) -> ('b -> real) -> 'a * 'b -> real.
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17345#changelog
https://www.easycrypt.info/trac/ticket/17364
https://www.easycrypt.info/trac/ticket/17364#17364: Internals: use Batteries maps instead of Why3 ones.Mon, 19 Feb 2018 13:01:10 GMTPierre-Yves StrubResultshttps://www.easycrypt.info/trac/ticket/17364#changelog
https://www.easycrypt.info/trac/ticket/17077
https://www.easycrypt.info/trac/ticket/17077#17077: No more direct access to stdlib pathsMon, 20 Oct 2014 11:01:55 GMTPierre-Yves Strub<p>
All the path resolution w.r.t. the standard library should go through a dedicated API that check that the enclosing module has been loaded. This should solve all bugs related to the use of paths that cannot be resolved afterward.
</p>
<p>
Regarding checking that a module is loaded, the standard library should resides in a private namespace that cannot be extended by users.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17077#changelog
https://www.easycrypt.info/trac/ticket/17082
https://www.easycrypt.info/trac/ticket/17082#17082: SMT tactic should be interruptable.Sun, 02 Nov 2014 18:45:27 GMTPierre-Yves Strub<p>
Currently, this stops the whole <a class="missing wiki">EasyCrypt?</a> process.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17082#changelog
https://www.easycrypt.info/trac/ticket/17163
https://www.easycrypt.info/trac/ticket/17163#17163: Check that `phoare` tactics are forcing the input bounds to be in [0..1].Wed, 21 Jan 2015 14:38:55 GMTPierre-Yves Strub<p>
See <a class="closed ticket" href="https://www.easycrypt.info/trac/ticket/17120" title="#17120: defect: [rnd] allows to prove false (closed: fixed)">#17120</a> for instance.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17163#changelog
https://www.easycrypt.info/trac/ticket/17298
https://www.easycrypt.info/trac/ticket/17298#17298: Super rndTue, 02 Feb 2016 13:08:33 GMTruette<p>
We would like to have a rule which would help proving an equivalence between :
</p>
<p>
pre : P
</p>
<p>
x <$ d1
y <$ d2 x
~
y <$ dlet d1 d2
</p>
<p>
post : ={y}
</p>
<p>
This without evoking new procedure names (bypr).
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17298#changelog
https://www.easycrypt.info/trac/ticket/16103
https://www.easycrypt.info/trac/ticket/16103#16103: scoping issue with theoriesSun, 21 Jul 2013 23:25:00 GMTAlley Stoughton<p>Consider the following:<br/>
</p><p>module X = {<br/>
var x : int<br/>
}.<br/>
</p><p>theory T.<br/>
</p><p>module X = {<br/>
var x : bool<br/>
}.<br/>
</p><p>end T.<br/>
</p><p>import T.<br/>
</p><p>module Y = {<br/>
fun f() : bool = {<br/>
var b : bool;<br/>
b = X.x;<br/>
return b;<br/>
}<br/>
}.<br/>
</p><p>Here, X.x refers to the one from T, so that the original definition of X was eclipsed.<br/>
</p><p>Perhaps there should be a way to refer to the original X from inside the overall theory?<br/>
</p><p>More importantly, I'm concerned about conflicts between names of components of theories when the theories are imported. Of course, one can always not to do the import, always using T.blah, etc. But I'm thinking that, when importing, one might want to choose new names for the module types, modules, etc., that are being imported.<br/>
</p><p>E.g., if a theory T includes a module type Adv, and there is already a module type Adv in the context into which T is imported, then one certainly doesn't want to render the original Adv inaccessible.<br/>
</p>Resultshttps://www.easycrypt.info/trac/ticket/16103#changelog
https://www.easycrypt.info/trac/ticket/16648
https://www.easycrypt.info/trac/ticket/16648#16648: Make notations and tactics on distributions and functions a bit more uniform.Mon, 18 Nov 2013 12:59:00 GMTFrançois Dupressoir<p>"islossless" should apply to distributions as well as functions.<br/>
</p><p>"isuniform" should be made into a keyword and apply to functions as well as distributions (a pain to prove but powerful once obtained...)<br/>
</p><p>"rewrite Pr" should work with (almost) arbitrary rewriting lemmas on mu<br/>
</p>Resultshttps://www.easycrypt.info/trac/ticket/16648#changelog
https://www.easycrypt.info/trac/ticket/16987
https://www.easycrypt.info/trac/ticket/16987#16987: Move facts from precondition to contextFri, 07 Feb 2014 14:52:00 GMTFrançois Dupressoir<p>The "exists* v; elim* => v0" combination is useful, but it is sometimes necessary to also move facts about the new values in the context from the precondition up.<br/>
For example, on<br/>
</p><p>pre = valid (Mem.var{1})<br/>
</p><p> c ~ c'<br/>
</p><p>post = \Psi<br/>
</p><p>the combination "exists* Mem.var{1} <valid (Mem.var{1})>; elim* => v valid_v." would yield (after checking that the formula between <...> is indeed true in the precondition, and that all the program variables that appear in it are being existentially quantified over)<br/>
</p><p>v : t<br/>
valid_v: valid v<br/>
--------------------------------<br/>
pre = valid (Mem.var{1})<br/>
</p><p>c ~ c'<br/>
</p><p>post = \Psi<br/>
</p>Resultshttps://www.easycrypt.info/trac/ticket/16987#changelog
https://www.easycrypt.info/trac/ticket/17002
https://www.easycrypt.info/trac/ticket/17002#17002: Better section && cloning supportSun, 16 Feb 2014 18:42:04 GMTPierre-Yves Strub<h1 id="Onsectionsanddeclaredentities">On sections and declared entities</h1>
<dl class="wiki"><dt>declared type</dt><dd>
Make <em>lemmas</em> and <em>operators</em> that refer to a declared type polymorphic.
</dd></dl>
<blockquote>
<p>
<em>Module types</em> and <em>non-local modules</em> cannot use the declared type (no polymorphism in modules).
</p>
</blockquote>
<dl class="wiki"><dt>local type</dt><dd>
<em>Local type aliases</em> should be inlined.
</dd></dl>
<blockquote>
<p>
<em>Defined types</em> can only be used in local entities.
</p>
</blockquote>
<dl class="wiki"><dt>declared operator</dt><dd>
<em>universally quantified; declare operators</em> have to be monomorphic (or used in a parametric way, which is not very useful).
</dd></dl>
<blockquote>
<p>
Cannot be used in non-local modules.
</p>
</blockquote>
<dl class="wiki"><dt>local operator</dt><dd>
<em>Fixpoints</em> may only appear in local entities.
</dd></dl>
<blockquote>
<p>
Other local op definitions are inlined on exit.
</p>
</blockquote>
<dl class="wiki"><dt>declared module type</dt><dd>
useless?
</dd></dl>
<dl class="wiki"><dt>local module type</dt><dd>
can only appear in local entities.
</dd></dl>
<dl class="wiki"><dt>declared module</dt><dd>
universally quantified in lemmas.
</dd></dl>
<dl class="wiki"><dt>local modules</dt><dd>
<em>Aliases</em> are inlined on exit.
</dd></dl>
<blockquote>
<p>
Other module definitions may only appear in local entities.
</p>
</blockquote>
<dl class="wiki"><dt>local axioms</dt><dd>
Default behaviour is to turn them into hypotheses on lemmas (with simplifications).
</dd></dl>
<blockquote>
<p>
Axioms marked as global can only mention global entities and are exported by the section.
</p>
</blockquote>
<h1 id="Oncloning">On cloning</h1>
<p>
The final clone is computed from the sequence of cloning instructions, applied to the base theory.
</p>
<h2 id="Wheninstantiatingentities">When instantiating entities</h2>
<p>
We follow the following rules:
</p>
<dl class="wiki"><dt>types, operators and modules</dt><dd>
<ul><li>Abstract entities of those kinds are easy to instantiate by substitution;
</li><li>A concrete entitiy of these kinds can only be instantiated with concrete entities they are convertible to.
</li></ul></dd></dl>
<dl class="wiki"><dt>axioms, lemmas</dt><dd>
<ul><li>Once a lemma has been proved, reproving it yields an error;
</li><li>In proof expressions, the * captures all axioms that have not yet been discharged;
</li><li>When the instance has a proved lemma, we do not need to create a fresh copy of it (to save SMT).
</li></ul></dd></dl>
<h2 id="Whencloninginsideasection">When cloning inside a section</h2>
<ul><li>instantiating an entity with declared symbols yields a local entity;
</li><li>sugar:
<ul><li>we want to be able to mark cloning instructions (clone local) and instantiation instructions (with local op x <- ...) as local (or global). If nothing remains of a theory is global after a clone, it disappears entirely on exiting the section.
</li><li>we want to be able to mark abstract cloned entities as 'declared' (with declared op x).
</li></ul></li></ul>Resultshttps://www.easycrypt.info/trac/ticket/17002#changelog
https://www.easycrypt.info/trac/ticket/17022
https://www.easycrypt.info/trac/ticket/17022#17022: Pattern-matching on variables in judgments and probability expressionsFri, 06 Jun 2014 14:28:15 GMTFrançois Dupressoir<p>
This is a placeholder feature request so I don't forget to craft more examples of what was requested.
</p>
<p>
<code>axiom toto v: equiv[M.f ~ M.f: P v ==> Q v].</code>
</p>
<p>
<code>apply toto.</code> works if the goal is exactly the lemma (with quantification), but fails if the goal is an instance of the lemma.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17022#changelog
https://www.easycrypt.info/trac/ticket/17085
https://www.easycrypt.info/trac/ticket/17085#17085: Generic NotationsMon, 03 Nov 2014 14:48:52 GMTFrançois Dupressoir<p>
Including notations on memories.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17085#changelog
https://www.easycrypt.info/trac/ticket/17086
https://www.easycrypt.info/trac/ticket/17086#17086: Generalize [rewrite Pr]Mon, 03 Nov 2014 14:53:06 GMTFrançois Dupressoir<p>
<code>rewrite Pr</code> should be able to take an almost arbitrary lemma on probabilities and lift it to programs/memories/events.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17086#changelog
https://www.easycrypt.info/trac/ticket/17105
https://www.easycrypt.info/trac/ticket/17105#17105: [transitivity] for phoare and hoareThu, 13 Nov 2014 12:49:16 GMTFrançois Dupressoir<p>
Currently <code>transitivity</code> only applies on <code>equiv</code> judgments. Having it generate <code>equiv</code> judgments on statements when applied in <code>phoare</code> and <code>hoare</code> might be useful. For example, in <code>phoare</code> (similar rules would work for <code>>=</code> and <code>=</code>):
</p>
<pre class="wiki"> {P{1} <=> P{2}} s ~ s' {Q{1} <=> Q{2}} {P} s' {Q} <= d
-------------------------------------------------------------------- transitivity { s' }.
{P} s {Q} <= d
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17105#changelog
https://www.easycrypt.info/trac/ticket/17113
https://www.easycrypt.info/trac/ticket/17113#17113: Decide what to do on rewrite with defined head symbolsTue, 18 Nov 2014 14:44:41 GMTFrançois Dupressoir<pre class="wiki">type 'a set.
op mem: 'a -> 'a set -> bool.
pred (<=) (A B:'a set) = forall x, mem x A => mem x B.
op inter: 'a set -> 'a set -> 'a set.
axiom interGs (A B:'a set): inter A B <= A.
lemma toto (A B:'a set): inter A B <= A.
proof.
rewrite interGs. (* This currently fails. Do we want it to succeed? *)
qed.
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17113#changelog
https://www.easycrypt.info/trac/ticket/17136
https://www.easycrypt.info/trac/ticket/17136#17136: variant of seq to deal with large preconditionsTue, 09 Dec 2014 12:00:27 GMTBenedikt Schmidt<p>
In some proofs, a random sampling followed by an <code>if</code> requires the use of <code>seq</code>. Currently, it is always necessary to specify the full postcondition, even though the required change is small. It would be nice to have a variant, say <code>seq*</code>, that adds a new conjunct to the pre (existentially quantifying modified variables as necessary).
</p>
<pre class="wiki">require import Int.
require import Distr.
module A = {
var x : int
var y : int
proc b() : unit = {
x = $Dinter.dinter 0 10;
if (x = 5) {
y = x;
}
}
}.
op inv : (int * int) -> (int * int) -> bool.
equiv eq_A:
A.b ~ A.b : inv (A.x,A.y){1} (A.x,A.y){2} ==> inv (A.x,A.y){1} (A.x,A.y){2}.
proof.
proc.
seq 1 1: (={A.x} /\ exists x_L x_R, inv (x_L, A.y{1}) (x_R, A.y{2})).
(* It would be very convenient to have something like
seq* 1 1: (={A.x})
to replace the above. *)
admit.
admit.
qed.
</pre><p>
Of course, such a feature is related to a forward variant of <code>rnd</code> or supporting something like <code>@PRE</code> in <code>seq</code>.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17136#changelog
https://www.easycrypt.info/trac/ticket/17140
https://www.easycrypt.info/trac/ticket/17140#17140: Pattern matching should make use of simplification rules.Thu, 18 Dec 2014 14:34:15 GMTPierre-Yves Strub<p>
For instance, <code>1</code> and <code>(?n + 1)</code> should match, leading to <code>?n -> 0</code>.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17140#changelog
https://www.easycrypt.info/trac/ticket/17149
https://www.easycrypt.info/trac/ticket/17149#17149: Expand glob A for concrete moduleTue, 30 Dec 2014 20:26:10 GMTBenedikt Schmidt<p>
The following fails because the module <code>M</code> is local:
</p>
<pre class="wiki">section.
module type T = {}.
local module M : T = {
var a, b, c : int
}.
op foo : glob M -> bool.
(* this works and should be equivalent
op foo : (int * int * int) -> bool.*)
(* fails with: unknown symbol: Top.M *)
end section.
</pre><p>
It would be useful to treat <code>glob M</code> for concrete modules like a type alias, i.e., internally replace <code>glob M</code> by the corresponding tuple type.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17149#changelog
https://www.easycrypt.info/trac/ticket/17156
https://www.easycrypt.info/trac/ticket/17156#17156: New vernacular command: `print axiom`Mon, 05 Jan 2015 20:41:07 GMTPierre-Yves Strub<p>
Print the set of axioms that are reachable in the current context. This command should try to give the origins of axioms (for instance, it should collapse all axioms that are coming from different cloning of the same theory).
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17156#changelog
https://www.easycrypt.info/trac/ticket/17164
https://www.easycrypt.info/trac/ticket/17164#17164: behavior of -check-allWed, 21 Jan 2015 18:31:23 GMTAlley Stoughton<p>
When running the check-all option:
</p>
<p>
(1) It would be good to prune the theory tree at points viewed as "trusted". One option is to draw the line at the EC library. Another, as suggested by Francois, is to let the user label certain requires as trusted:
</p>
<blockquote>
<p>
require [trusted] import Int.
</p>
</blockquote>
<p>
(2) When checking the theory tree, it's important to print status information showing when the checker descends to a new file, and when it exits from that file. At present, everything within a require is opaque.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17164#changelog
https://www.easycrypt.info/trac/ticket/17169
https://www.easycrypt.info/trac/ticket/17169#17169: Anonymous functor arguments: passing procedures to functors directlyFri, 06 Feb 2015 19:05:23 GMTFrançois Dupressoir<p>
Since module types do not mention globals and the granularity of restrictions is fine enough, we could pass oracles and procedures directly to functors in functor applications. This would avoid a lot of the current verbosity, that requires the definition of intermediate modules with explicit procedure aliases for all required procedures even when only one of them is used in practice, and get EasyCrypt syntax slightly closer to standard "cryptographer" notation.
</p>
<p>
(Ideally, we would also allow the definition of functors without having to define a type for its module argument, simply by listing the required procedures...)
</p>
<pre class="wiki">module type Arg = {
proc foo(): unit
}.
module M: Arg = {
var b:bool
proc bar(): unit = {
b = ${0,1};
}
proc check(b':bool): bool = {
return b = b';
}
}.
module A(M:Arg) = {
proc main(b:bool): bool = {
M.foo();
b = M.check(b);
return b;
}
}.
module B = A({foo = M.bar}).
</pre><p>
For the "ideally" extension to anonymous module types, a possible syntax would be <code>module A(M:{foo(): bool;}) = { ... }. </code>
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17169#changelog
https://www.easycrypt.info/trac/ticket/17175
https://www.easycrypt.info/trac/ticket/17175#17175: Direct intro on negative goalsWed, 18 Feb 2015 19:04:00 GMTFrançois Dupressoir<pre class="wiki"> H: a
----------- move=> H. -----------
!a false
</pre><p>
may be useful?
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17175#changelog
https://www.easycrypt.info/trac/ticket/17192
https://www.easycrypt.info/trac/ticket/17192#17192: Problem with `glob` and type inferenceThu, 16 Apr 2015 09:38:51 GMTFrançois Dupressoir<p>
In the following, the statement of lemma <code>bug</code> is parsed and type-checked. However, <code>p</code> is introduced before <code>M</code>, despite the fact that the type of <code>p</code> depends on the value of <code>M</code> (there, I said it).
</p>
<p>
Expected behaviour: type inference should fail (obviously with a cryptic message :)).
</p>
<pre class="wiki">module type T = {
proc func(): unit
}.
lemma bug: forall p (M <: T),
hoare [M.func: p (glob M) ==> p (glob M)].
</pre><p>
yields (modulo unification variable)
</p>
<pre class="wiki">Current goal
Type variables: <none>
------------------------------------------------------------------------
forall (p : (glob M/2036) -> bool) (M <: T),
hoare[ M.func : p (glob M) ==> p (glob M)]
</pre><p>
Quantifying the right way around works as expected.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17192#changelog
https://www.easycrypt.info/trac/ticket/17197
https://www.easycrypt.info/trac/ticket/17197#17197: Asserts in equivalence proofsMon, 15 Jun 2015 14:18:28 GMTmbbarbosa<p>
Our goal is to be able to prove an equivalence between two versions of the same program, one of which is annotated with safety assertions. We attach a file that illustrates this.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17197#changelog
https://www.easycrypt.info/trac/ticket/17202
https://www.easycrypt.info/trac/ticket/17202#17202: Add seq* tacticTue, 16 Jun 2015 12:20:42 GMTineol<p>
It would be nice to have seq* n X, similar to conseq*, which adds to the X the terms of the precondition that are not modified by the instructions 1..n.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17202#changelog
https://www.easycrypt.info/trac/ticket/17210
https://www.easycrypt.info/trac/ticket/17210#17210: Pattern-matching for pairs in operator argumentsWed, 24 Jun 2015 11:10:14 GMTFrançois Dupressoir<p>
<code>fun ((x,y):'a * 'b) => f x</code>
</p>
<p>
is easier to read and write than
</p>
<p>
<code>fun (xy:'a * 'b) => f xy.`1</code>
</p>
<p>
(or even having to use a let expression to destruct the pair).
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17210#changelog
https://www.easycrypt.info/trac/ticket/17215
https://www.easycrypt.info/trac/ticket/17215#17215: Issues with module typing when functor parameters are themselves functorsFri, 26 Jun 2015 13:55:03 GMTFrançois Dupressoir<p>
This is more a discussion than a bug report, although at least improving the error messages for errors in module typing would definitely be a bonus...
</p>
<p>
Consider the following scenario. I have the following module types (for example <code>O</code> might be the type of random oracles, <code>S</code> might be the type of some primitive that uses it, and <code>C</code> might be the type of scheme we are constructing).
</p>
<pre class="wiki">module type O = {
proc toto(): unit
}.
module type S (Or:O) = {
proc titi(): unit
}.
module type C = {
proc tata(): unit
}.
</pre><p>
Now, it might be useful (read, "it is very nice") to sometimes consider the type of "black-box constructions of <code>C</code> from <code>S</code> and <code>O</code>", which we would write as follows:
</p>
<pre class="wiki">module type C_p (Sc:S,OR:O) = {
proc tata(): unit
}.
</pre><p>
EasyCrypt is then very happy to accept that the following module <code>Good</code>, applied to an <code>S</code> and an <code>O</code> does implement module type <code>C</code>:
</p>
<pre class="wiki">module Good(Sc:S,Or:O): C = {
proc tata = Sc(Or).titi
}.
</pre><p>
However, what we really want to know is that <code>Good</code> has type <code>C_p</code>. The following currently fails with an obscure <code>this module body does not meet its interface: the item `tata' does not have a compatible kind/type</code>. (Along the way, note the ugly notation for functor types...)
</p>
<pre class="wiki">module Manimoule(Sc:S,Or:O): C_p(Sc Or) = {
proc tata = Sc(Or).titi
}.
</pre><p>
Intrigued by the failure (and after a couple of hours of swearing while trying to go from the error message above to an idea of what may be going wrong), we <code>print C_p</code> to get the following:
</p>
<pre class="wiki">module type C_p(Sc : S,Or : O) = {
proc tata() : unit {Or.toto}
}.
</pre><p>
This is bad: we are happy for <code>tata</code> to be able to query <code>Or.toto</code>, but we also want <code>tata</code> to be able to query <code>Sc(Or).titi</code>. Obviously, EasyCrypt cannot figure out on its own that this is the case (in general, we might even be taking two different parameters of type <code>O</code> and letting <code>tata</code> query <code>Sc</code> with both!), so we go ahead and modify <code>C_p</code> to let the tool know of our intentions:
</p>
<pre class="wiki">module type C_p' (Sc:S,Or:O) = {
proc tata(): unit { Or.toto Sc(Or).titi }
}.
</pre><p>
This yields a nice <code>parse error</code>, pointing to the <code>O</code> in <code>Sc(Or).titi</code>.
</p>
<p>
Now we're stuck. There is something we would like to do, but no way of doing it. Question: Do we want to fix this? The simplest fix (on the surface) would be to allow functor instantiation in oracle restrictions.
If we don't want to fix this (and I understand that I'm sometimes doing weird things), we should definitely make it clear in the error message so the use doesn't try to fight it for too long.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17215#changelog
https://www.easycrypt.info/trac/ticket/17217
https://www.easycrypt.info/trac/ticket/17217#17217: need better error message when attempting to apply lemma to goal that isn't a judgmentWed, 08 Jul 2015 16:25:11 GMTAlley Stoughton<p>
The error message below isn't helpful. The user has probably meant to use <code>call</code> instead of <code>apply</code>.
</p>
<pre class="wiki">module A = {
proc f() : unit = {
}
proc g() : unit = {
f();
}
}.
lemma Af :
equiv[A.f ~ A.f : true ==> true].
proof.
proc; auto.
qed.
lemma Ag :
equiv[A.g ~ A.g : true ==> true].
proof.
proc.
(*
Current goal
Type variables: <none>
------------------------------------------------------------------------
&1 (left ) : A.g
&2 (right) : A.g
pre = true
A.f() (1) A.f()
post = true
*)
apply Af.
(* error message:
"cannot apply lemma"
This is an unhelpful error message,
because a goal of this form can
never be the conclusion of a lemma.
Maybe:
"goal is not a judgement" *)
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17217#changelog
https://www.easycrypt.info/trac/ticket/17218
https://www.easycrypt.info/trac/ticket/17218#17218: proposal for expressing goal of two-sided PRHL rnd tactic using isomorphism of bijections predicateWed, 08 Jul 2015 20:56:25 GMTAlley Stoughton<pre class="wiki">(* if we introduce a predicate describing an isomorphism between
distributions, then the two-sided PRHL rnd tactic could express its
goal using this predicate, making things clearer and more
modular *)
require import Bool Int Real Distr.
(* isomorphism between distributions *)
pred DistrIso (aDistr : 'a distr, bDistr : 'b distr,
f : 'a -> 'b, g : 'b -> 'a) =
(forall (x : 'a),
in_supp x aDistr =>
mu_x aDistr x = mu_x bDistr (f x) &&
x = g(f x)) &&
(forall (y : 'b),
in_supp y bDistr =>
mu_x bDistr y = mu_x aDistr (g y) &&
y = f(g y)).
(* example use of rnd tactic *)
module G1 = {
proc main() : bool = {
var x : bool;
x <$ Dbool.dbool;
return x;
}
}.
module G2 = {
proc main() : bool = {
var x, y : bool;
x <$ Dbool.dbool;
y <$ Dbool.dbool;
return x ^^ y;
}
}.
lemma G1_G2 : equiv[G1.main ~ G2.main : true ==> ={res}].
proof.
proc.
(* handle choice of x in {2} *)
seq 0 1 : (true).
rnd {2}; auto; smt.
(* goal:
pre = true
x <$ {0,1} (1) y <$ {0,1}
post = x{1} = x{2} ^^ y{2}
*)
rnd (fun u => x{2} ^^ u) (fun v => x{2} ^^ v).
(* goal:
pre = true
post =
(forall (yR : bool), in_supp yR {0,1} => yR = x{2} ^^ (x{2} ^^ yR)) &&
(forall (yR : bool),
in_supp yR {0,1} => mu_x {0,1} yR = mu_x {0,1} (x{2} ^^ yR)) &&
forall (xL : bool),
in_supp xL {0,1} =>
in_supp (x{2} ^^ xL) {0,1} &&
xL = x{2} ^^ (x{2} ^^ xL) && xL = x{2} ^^ (x{2} ^^ xL)
But now, let's see how the postcondition could be expressed using DistrIso: *)
conseq
(_ :
_ ==>
DistrIso Dbool.dbool Dbool.dbool
(fun u => x{2} ^^ u) (fun v => x{2} ^^ v) &&
(forall (b : bool),
in_supp b Dbool.dbool =>
b = x{2} ^^ (fun u => x{2} ^^ u) b));
first smt.
(*
goal:
pre = true
post =
DistrIso {0,1} {0,1}
(fun (u : bool) => x{2} ^^ u)
(fun (v : bool) => x{2} ^^ v) &&
forall (b : bool),
in_supp b {0,1} =>
b = x{2} ^^ (fun (u : bool) => x{2} ^^ u) b
The point is that rnd could generate this itself, making it clear
which part has to do with the isomorphism of bijections, and which
has to do with the postcondition of the equiv. *)
skip.
(* goal:
forall &1 &2,
true =>
DistrIso {0,1} {0,1}
(fun (u : bool) => x{2} ^^ u)
(fun (v : bool) => x{2} ^^ v) &&
forall (b : bool),
in_supp b {0,1} =>
b = x{2} ^^ (fun (u : bool) => x{2} ^^ u) b
*)
move => &1 &2 _.
(* deal with the bijection of distributions part: *)
(split; first smt) => DB b bSup.
(* this leave us with the goal corresponding to the equiv's
postcondition:
DB: DistrIso {0,1} {0,1}
(fun (u : bool) => x{2} ^^ u)
(fun (v : bool) => x{2} ^^ v)
b : bool
bSup: in_supp b {0,1}
------------------------------------------------------------------------
b = x{2} ^^ (fun (u : bool) => x{2} ^^ u) b
*)
smt.
qed.
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17218#changelog
https://www.easycrypt.info/trac/ticket/17225
https://www.easycrypt.info/trac/ticket/17225#17225: Explore reproducible smt callsMon, 27 Jul 2015 16:04:12 GMTBenedikt Schmidt<p>
There seems to be some support for machine-independent resource limits for Z3 and alt-ergo now:
<a class="ext-link" href="https://github.com/Z3Prover/z3/issues/56"><span class="icon"></span>https://github.com/Z3Prover/z3/issues/56</a>
</p>
<p>
This could useful to make replaying proofs less fragile.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17225#changelog
https://www.easycrypt.info/trac/ticket/17239
https://www.easycrypt.info/trac/ticket/17239#17239: Mutual inductive types.Sun, 06 Sep 2015 17:31:12 GMTPierre-Yves StrubResultshttps://www.easycrypt.info/trac/ticket/17239#changelog
https://www.easycrypt.info/trac/ticket/17245
https://www.easycrypt.info/trac/ticket/17245#17245: Formula manipulation commands (for `conseq` and `seq`)Wed, 16 Sep 2015 12:48:17 GMTFrançois Dupressoir<p>
We should extend (the simple variant of) <code>conseq</code> so that
<code>conseq (_: C[_] ==> C'[_])</code>, where <code>C</code> and <code>C'</code> are pre and postcondition contexts simply expands to the same <code>conseq</code> statement where <code>C[_]</code> and <code>C'[_]</code> are replaced with their instantiation with the current pre and post, respectively.
</p>
<p>
For example, on goal <code>{P} c1 ~ c2 {Q}</code>, <code>conseq (_: _ /\ P' ==> _ /\ Q').</code> would act as <code>conseq (_: P /\ P' ==> Q /\ Q').</code> and yield goals <code>P => P /\ P'</code>, <code>Q /\ Q' => Q</code> (+ premise related to the precondition) and <code>{P /\ P'} c1 ~ c2 {Q /\ Q'}</code>.
</p>
<p>
The same could be done for <code>seq</code>, but it involves an inference component that I do not completely understand: <code>conseq</code> can simply syntactically look at the current goal to figure out what to apply the context to, whereas the formula for <code>seq</code> is not immediately clear.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17245#changelog
https://www.easycrypt.info/trac/ticket/17246
https://www.easycrypt.info/trac/ticket/17246#17246: `rewrite`, apply, ... in contractsWed, 16 Sep 2015 14:54:53 GMTFrançois DupressoirResultshttps://www.easycrypt.info/trac/ticket/17246#changelog
https://www.easycrypt.info/trac/ticket/17251
https://www.easycrypt.info/trac/ticket/17251#17251: print SelfMon, 28 Sep 2015 09:02:48 GMTFrançois Dupressoir<p>
Is it possible to make <code>print Self.</code> pretty print the current contents of the current theory? This would be particularly useful when <code>Self</code> contains a <code>clone include</code> command, so the corresponding definitions can be inspected.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17251#changelog
https://www.easycrypt.info/trac/ticket/17257
https://www.easycrypt.info/trac/ticket/17257#17257: `/=` is too weak.Sun, 25 Oct 2015 06:45:17 GMTPierre-Yves Strub<p>
E.g., <code>flatten []</code> should reduce to <code>[]</code>
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17257#changelog
https://www.easycrypt.info/trac/ticket/17259
https://www.easycrypt.info/trac/ticket/17259#17259: Theory of distribution (iso)morphismsMon, 02 Nov 2015 11:09:45 GMTFrançois Dupressoir<p>
A general theory of morphisms on distributions would be good to have to simplify reasoning on equivalences.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17259#changelog
https://www.easycrypt.info/trac/ticket/17267
https://www.easycrypt.info/trac/ticket/17267#17267: `auto` with `call`Wed, 11 Nov 2015 14:18:40 GMTPierre-Yves Strub<p>
Add a new parameter to <code>auto</code> containing invariants for calls, with the option to default to the <code>true</code> invariant.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17267#changelog
https://www.easycrypt.info/trac/ticket/17279
https://www.easycrypt.info/trac/ticket/17279#17279: Improve `invalid goal shape` error messages for variants of `byequiv`Fri, 11 Dec 2015 10:04:51 GMTFrançois Dupressoir<p>
It would be helpful if the error messages gave (at least) the expected goal shape for the variant of <code>byequiv</code> that is being used.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17279#changelog
https://www.easycrypt.info/trac/ticket/17281
https://www.easycrypt.info/trac/ticket/17281#17281: Several problems with `apply` in program logicsMon, 14 Dec 2015 12:10:00 GMTFrançois Dupressoir<p>
Several things would be good on the program logic <code>apply</code> tactic:
</p>
<ul><li>it should use the medium-level apply so useful error messages are returned (l. 298);
</li><li>it should do some inference, at least on values (FIXME).
</li></ul><p>
Examples can be found in SHA3, file old/MyRO.ec, rev. <a class="missing changeset" rel="nofollow" title="No changeset f5583ecdd1563e5a5d59f613c4c16b4255e982ae in the repository">f5583ecdd1563e5a5d59f613c4c16b4255e982ae</a>
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17281#changelog
https://www.easycrypt.info/trac/ticket/17282
https://www.easycrypt.info/trac/ticket/17282#17282: call should not workMon, 14 Dec 2015 15:19:03 GMTruetteResultshttps://www.easycrypt.info/trac/ticket/17282#changelog
https://www.easycrypt.info/trac/ticket/17283
https://www.easycrypt.info/trac/ticket/17283#17283: pattern matching complexity problemMon, 14 Dec 2015 15:35:22 GMTruette<p>
In cs-gossip repository, in Gossip.ec, a complexity problem has to be fixed.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17283#changelog
https://www.easycrypt.info/trac/ticket/17285
https://www.easycrypt.info/trac/ticket/17285#17285: Transitivity on procedures should support inferring contracts from `equiv` lemmas.Wed, 16 Dec 2015 10:11:17 GMTFrançois Dupressoir<p>
Variants (for pRHL) would be:
</p>
<ul><li><code>transitivity <proc> <contract> <contract></code> (current syntax)
</li><li><code>transitivity _ <lemma> <lemma></code>
</li><li><code>transitivity _ <lemma> <contract></code> (and commuted)
</li></ul>Resultshttps://www.easycrypt.info/trac/ticket/17285#changelog
https://www.easycrypt.info/trac/ticket/17286
https://www.easycrypt.info/trac/ticket/17286#17286: pRHL `apply` should have a framing variantTue, 05 Jan 2016 15:20:26 GMTFrançois Dupressoir<p>
Currently, <code>apply</code> in pRHL fails unless pre and postconditions match precisely between goal and lemma. It would be useful to have an <code>apply [conseq]</code> option that applies <code>conseq</code> as needed.
</p>
<p>
Making it an optional behaviour rather than the default one is important for early failure when lemmas change.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17286#changelog
https://www.easycrypt.info/trac/ticket/17287
https://www.easycrypt.info/trac/ticket/17287#17287: Program transformation tactics should not `anomaly` without a side in pRHLSat, 09 Jan 2016 15:58:35 GMTFrançois Dupressoir<p>
In pRHL, <code>splitwhile</code> and other program transformation tactics currently fail badly when not given a side. At the very least, they should report why they are failing. In the best case, they should just work on both programs and generate two subgoals.
</p>
<p>
For example, on
</p>
<pre class="wiki">while (i < j) { ( 1 ) while (i < j) {
i <- i + 1; (1.1) i <- i + 1;
} (---) }
</pre><p>
<code>splitwhile 1: (i < M)</code> should work and produce the subgoal:
</p>
<pre class="wiki">while (i < j /\ i < M) { ( 1 ) while (i < j /\ i < M) {
i <- i + 1; (1.1) i <- i + 1;
} (---) }
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17287#changelog
https://www.easycrypt.info/trac/ticket/17288
https://www.easycrypt.info/trac/ticket/17288#17288: EasyCrypt crashes when printing required abstract theory IterProcTue, 12 Jan 2016 21:59:06 GMTAlley Stoughton<p>
Running <a class="missing wiki">EasyCrypt?</a> on
</p>
<pre class="wiki">require IterProc.
print IterProc.
</pre><p>
results in
</p>
<pre class="wiki">$ easycrypt goo.ec
* In [theories]: % (-1.0B / [frag -1.0B])
[critical] [goo.ec:3] unknown symbol: Top.IterProc.Iter(O/22533)./iter
[/] [0003] 100.0 % (-1.0B / [frag -1.0B])
abstract theory IterProc.
type t.
</pre><p>
...
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17288#changelog
https://www.easycrypt.info/trac/ticket/17290
https://www.easycrypt.info/trac/ticket/17290#17290: `n!->>` should workTue, 19 Jan 2016 15:12:39 GMTFrançois Dupressoir<p>
It really should...
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17290#changelog
https://www.easycrypt.info/trac/ticket/17295
https://www.easycrypt.info/trac/ticket/17295#17295: local opsFri, 22 Jan 2016 14:52:26 GMTFrançois Dupressoir<p>
Benjamin mentioned that local operators would be useful to carry out proofs when invariants get large. As a first step, simply not allowing them to appear in any non-local object would be sufficient for this use.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17295#changelog
https://www.easycrypt.info/trac/ticket/17301
https://www.easycrypt.info/trac/ticket/17301#17301: Applicative view for `if then else`Thu, 04 Feb 2016 15:24:11 GMTFrançois Dupressoir<p>
On goal
</p>
<pre class="wiki">H: if b then c else d
---------------------
b => e
</pre><p>
I would like <code>move=> /H</code> to produce
</p>
<pre class="wiki">H: if b then c else d
---------------------
c => e
</pre><p>
(And obviously, something similar with <code>!b</code> as top assumption.)
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17301#changelog
https://www.easycrypt.info/trac/ticket/17305
https://www.easycrypt.info/trac/ticket/17305#17305: proc* in eager case needlessly assigns result of procedures returning unit to variablesWed, 02 Mar 2016 00:28:49 GMTAlley Stoughton<p>
When the procedures of an eager judgment have return type <code>unit</code>, no need for <code>proc*</code> to assign returned values to variables. If <code>res</code> is used in postcondition despite it having only one possible value, could deal with that case, too.
</p>
<pre class="wiki">module M = {
proc f() : unit = {}
proc g() : unit = {}
}.
lemma foo : eager[M.f();, M.g ~ M.g, M.f(); : true ==> true].
proof.
proc*.
(*
Current goal
Type variables: <none>
------------------------------------------------------------------------
&1 (left ) : M.g
&2 (right) : M.g
pre = true
M.f() (1) r <@ M.g()
r <@ M.g() (2) M.f()
post = true
*)
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17305#changelog
https://www.easycrypt.info/trac/ticket/17311
https://www.easycrypt.info/trac/ticket/17311#17311: `smt (@Self)`Mon, 25 Apr 2016 16:19:10 GMTFrançois Dupressoir<p>
Probably related in some way to <a class="new ticket" href="https://www.easycrypt.info/trac/ticket/17251" title="#17251: enhancement: print Self (new)">#17251</a>, it would be nice to be able to quickly refer to "all lemmas I've just proved in this file" in <code>smt</code> calls.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17311#changelog
https://www.easycrypt.info/trac/ticket/17316
https://www.easycrypt.info/trac/ticket/17316#17316: [smt (@Theory)] should force the use of axioms marked as `nosmt`Fri, 27 May 2016 12:14:19 GMTFrançois DupressoirResultshttps://www.easycrypt.info/trac/ticket/17316#changelog
https://www.easycrypt.info/trac/ticket/17317
https://www.easycrypt.info/trac/ticket/17317#17317: `search` should work somewhat better with abbreviationsMon, 30 May 2016 09:12:01 GMTFrançois Dupressoir<pre class="wiki">type t.
op zero: t.
op (+): t -> t -> t.
abbrev \id (x : t) = x + zero.
axiom addt0 (x : t): \id x = x.
search (\id). (* empty results *)
search (+). (* returns addt0 *)
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17317#changelog
https://www.easycrypt.info/trac/ticket/17322
https://www.easycrypt.info/trac/ticket/17322#17322: use of side with HL version of while tactic should be syntax errorTue, 02 Aug 2016 19:32:28 GMTAlley Stoughton<pre class="wiki">module M = {
proc f() : unit = {
while (true) {
}
}
}.
lemma X : hoare[M.f : true ==> true].
proof.
proc.
(* presumably the use of {1} or {2} for HL version of while should
be a syntax error? *)
while{1} (true).
auto.
auto.
qed.
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17322#changelog
https://www.easycrypt.info/trac/ticket/17325
https://www.easycrypt.info/trac/ticket/17325#17325: syntax marking end of cloning realizationMon, 08 Aug 2016 13:33:25 GMTAlley Stoughton<p>
It would be useful to have syntax marking the end of the realization part, so the reader of a script (as opposed to the tool, or even someone interactively running the tool under Emacs) can see it’s over. E.g.,
</p>
<pre class="wiki">clone import blah as blaah with
. . .
proof *.
realize A. . . . qed.
. . .
realize Z. . . . qed.
end proof.
</pre>Resultshttps://www.easycrypt.info/trac/ticket/17325#changelog
https://www.easycrypt.info/trac/ticket/17337
https://www.easycrypt.info/trac/ticket/17337#17337: substitutions should complain when substituting a locally defined variableWed, 31 Aug 2016 12:27:03 GMTFrançois Dupressoir<p>
In a context where variable <code>x</code> is defined in context (for example, through <code>pose</code>) and an equation of the form <code>x = e</code> (with <code>e</code> an expression) is substituted, we would expect a complaint rather than silent loss of information.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17337#changelog
https://www.easycrypt.info/trac/ticket/17340
https://www.easycrypt.info/trac/ticket/17340#17340: cfold should support variables (and more general terms).Thu, 22 Sep 2016 11:55:53 GMTBas Spitters<p>
cfold should change something like:
</p>
<p>
y <- x
z <- y
</p>
<p>
To:
</p>
<p>
z <- x
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17340#changelog
https://www.easycrypt.info/trac/ticket/17341
https://www.easycrypt.info/trac/ticket/17341#17341: for loopsWed, 25 Jan 2017 12:05:58 GMTBas Spitters<p>
Easycrypt does not seem to support for loops (or does not document them?).
IMO it would be natural to add them.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17341#changelog
https://www.easycrypt.info/trac/ticket/17342
https://www.easycrypt.info/trac/ticket/17342#17342: Better support for rewriting with equivalencesWed, 25 Jan 2017 21:10:26 GMTBas Spitters<p>
Here's one example for concreteness, but there should be many.
</p>
<p>
require import Bool Array List Option <a class="missing wiki">NewDistr?</a> DBool.
</p>
<p>
module Test = {
proc f () : bool = {
</p>
<blockquote>
<p>
var b : bool;
b = $dbool;
return b;
</p>
</blockquote>
<blockquote>
<p>
}
</p>
</blockquote>
<p>
proc g () : bool = {
</p>
<blockquote>
<p>
var b : bool;
b = $dbool;
return !b;
</p>
</blockquote>
<blockquote>
<p>
}
</p>
</blockquote>
<p>
proc h ():bool = {
</p>
<blockquote>
<p>
var b,bf,bg:bool;
b=$dbool;
bf=f();
bg=g();
return (if b then bf else bg );
</p>
</blockquote>
<p>
}}.
</p>
<p>
lemma test: equiv [ Test.f ~ Test.g : true ==> ={res}].
proof.
</p>
<blockquote>
<p>
proc. rnd (fun b => !b). auto. progress; smt.
</p>
</blockquote>
<p>
qed.
</p>
<p>
(* How to prove: *)
</p>
<blockquote>
<p>
lemma test2: equiv [ Test.f ~ Test.h : true ==> ={res}].
</p>
</blockquote>
Resultshttps://www.easycrypt.info/trac/ticket/17342#changelog
https://www.easycrypt.info/trac/ticket/17344
https://www.easycrypt.info/trac/ticket/17344#17344: Trees and polynomialsWed, 15 Mar 2017 15:24:13 GMTBas Spitters<p>
I am trying to define trees ( to define multinomials).
</p>
<p>
However,
type 'a tree = [
| Leaf of 'a
| Cons of (('a tree) list)
].
-- the datatype does not respect the positivity condition
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17344#changelog
https://www.easycrypt.info/trac/ticket/17346
https://www.easycrypt.info/trac/ticket/17346#17346: have access to notation in mlMon, 20 Mar 2017 09:56:00 GMTBenjamin GrégoireResultshttps://www.easycrypt.info/trac/ticket/17346#changelog
https://www.easycrypt.info/trac/ticket/17348
https://www.easycrypt.info/trac/ticket/17348#17348: Intro-pattern `|>` might transform a provable goal to a non-provable oneMon, 10 Apr 2017 11:49:14 GMTPierre-Yves Strub<p>
See mpc-ec/mpc, commit <code>93eb4b45</code>, SSactive.ec, line 627.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17348#changelog
https://www.easycrypt.info/trac/ticket/17349
https://www.easycrypt.info/trac/ticket/17349#17349: call tactic for aequiv conclusionsMon, 29 May 2017 08:47:31 GMTMads Buch<p>
call tactic for aequiv conclusions
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17349#changelog
https://www.easycrypt.info/trac/ticket/17351
https://www.easycrypt.info/trac/ticket/17351#17351: sp for aqeuiv goalsSat, 10 Jun 2017 11:38:07 GMTMads Buch<p>
It would be nice to have the SP tactic for the apRHL logic.
</p>
Resultshttps://www.easycrypt.info/trac/ticket/17351#changelog