Revision 503d035509bd518c18a45b04244b317c75204d7e authored by Pierre Boutry on 19 March 2024, 10:29:37 UTC, committed by Pierre-Yves Strub on 05 April 2024, 18:16:56 UTC
1 parent 30bfa95
rwequiv.ec
(* -------------------------------------------------------------------- *)
require import AllCore.
(* -------------------------------------------------------------------- *)
module M = {
proc foo(x : int, y : int) : bool = {
var r <- true;
if (x < y) {
r <- false;
}
return r;
}
proc bar(x : int, y : int) : bool = {
var r <- false;
if (y <= x) {
r <- true;
}
return r;
}
}.
module N = {
proc baz(x : int, y : int) : bool = {
var r1, r2;
r1 <@ M.bar(x, y);
r2 <@ M.foo(x, y);
return r1 = r2;
}
}.
(* -------------------------------------------------------------------- *)
equiv foo_bar_eq: M.foo ~ M.bar: ={arg} ==> ={res}.
proof.
proc.
by auto=> /#.
qed.
(* -------------------------------------------------------------------- *)
equiv test1: M.foo ~ M.bar: ={arg} ==> ={res}.
proof.
proc*.
rewrite equiv[{1} 1 foo_bar_eq].
by sim.
qed.
(* -------------------------------------------------------------------- *)
equiv test2: M.foo ~ M.bar: ={arg} ==> ={res}.
proof.
proc*.
rewrite equiv[{2} 1 -foo_bar_eq].
by sim.
qed.
(* -------------------------------------------------------------------- *)
equiv test3: M.foo ~ M.bar: ={arg} ==> ={res}.
proof.
proc*.
rewrite equiv[{1} 1 foo_bar_eq (x, y :@ r)].
by sim.
qed.
(* -------------------------------------------------------------------- *)
equiv test4: N.baz ~ N.baz: ={arg} ==> ={res}.
proof.
proc.
rewrite equiv[{1} 2 foo_bar_eq].
rewrite equiv[{2} 1 -foo_bar_eq].
rewrite equiv[{2} 2 foo_bar_eq].
rewrite equiv[{1} 1 -foo_bar_eq].
by sim.
qed.
Computing file changes ...