Forall construction in code for ghost binding
Sometimes when we want to prove such functions:
let f x : result
ensures { forall y. P(x,y) -> Q(x,y) }
We need to prove with a ghost variable, for easing the proof
let f' x (ghost y) : result
requires { P(x,y) }
ensures { Q(x,y) }
However it is not possible to prove the first function using the second. We propose to add a new construction which allows it.
let f x : result
ensures { forall y. P(x,y) -> Q(x,y) }
=
forall y requires { P(x,y) } in
f' x y
The semantic of this function is not completely clear:
- should a VC be generated to check that it exists such
y
- what if the result contains a ghost
- what if there are ghost effect