-
Notifications
You must be signed in to change notification settings - Fork 53
Labels
Description
This means that writing to globals that are not used directly is ignored, even if those writes may be read by subsequent procedures.
Weaponization:
module M = {
var d: bool
}.
module type PT = {
proc p(): bool
}.
module Wt(P:PT) = {
proc p(): bool = {
var r;
M.d <- true;
r <@ P.p();
return r;
}
}.
module Wf(P:PT) = {
proc p(): bool = {
var r;
M.d <- false;
r <@ P.p();
return r;
}
}.
equiv Wt_eq_Wf (P<:PT): Wt(P).p ~ Wf(P).p: ={glob P} ==> ={res}.
proof. proc; sim. qed.
module PC = {
proc p() = {
return M.d;
}
}.
require import Real.
lemma pr_PCt &m: Pr[Wt(PC).p()@&m: res] = 1%r.
proof.
byphoare => //.
proc; inline PC; auto.
qed.
lemma pr_PCf &m: Pr[Wf(PC).p()@&m: res] = 0%r.
proof.
byphoare => //; hoare.
proc; inline PC; auto.
qed.
(* We need the existence of a memory here,
but this already allows us to prove every
program logic statement *)
lemma bad &m: false.
suff//: 1%r = 0%r.
rewrite -(pr_PCf &m).
rewrite -(pr_PCt &m).
byequiv (: ={glob PC} ==> ={res}) => //.
apply (Wt_eq_Wf PC).
qed.
wp
and sp
already handle things correctly, so the fix could amount to importing whatever logic is used there.