https://github.com/EasyCrypt/easycrypt
Tip revision: a2c11f189da68d291d48547461aff2432662e9e8 authored by François Dupressoir on 05 September 2024, 14:37:36 UTC
[ci] diversified external CI selects a valid branch
[ci] diversified external CI selects a valid branch
Tip revision: a2c11f1
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.