Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[high-level tactic] pHL call justified by equiv #741

Open
fdupress opened this issue Mar 7, 2025 · 0 comments
Open

[high-level tactic] pHL call justified by equiv #741

fdupress opened this issue Mar 7, 2025 · 0 comments

Comments

@fdupress
Copy link
Member

fdupress commented Mar 7, 2025

The following pattern, which fills a gap between logics, could be usefully turned into a high-level tactic. I do not expect it to be used a lot (the gaps between logics are there because we don't often need to jump over them), but not having to rediscover the subtleties of bypr every time one faces a similar issue would be a good improvement here.

type in_t.

module type T = {
  proc f(x:in_t): bool
}.

module W (M : T) = {
  var r : bool

  proc f(x) = {
    r <@ M.f(x);
  }
}.

lemma toto (M <: T {-W}) &m a:
  phoare [W(M).f: arg = a /\ (glob M) = (glob M){m} ==> W.r] = Pr[M.f(a) @ &m : res].
proof.
proc.
call (: (glob M) = (glob M){m} /\ arg = a ==> res).
+ bypr=> &0 [] eq_glob_M ->; byequiv (: ={glob M, arg} ==> ={res})=> //.
  by sim.
by auto.
qed.

This can be generalised slightly: the output type does not have to be bool, the equiv does not have to be trivial, the program does not have to be only the procedure call...

Implementing this would ideally be accompanied with documentation for call beyond just this extension.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant