-
Notifications
You must be signed in to change notification settings - Fork 50
[Program Logic] Expectation Logic (eHoare)
Expectation Hoare Logic (eHoare) is a logic for reasoning about judgments of the form
ehoare [ p : f ==> g ]
for procedures p and expressions f,g of type
xreal (see theories/datatypes/xreal.ec), the type of non-negative real numbers extended by a top element oo.
The meaning of such a judgment is that the expected value of g on output distributions is bounded by the value of f applied on the initial memory.
As such, f and g can refer to globally declared variables, the arguments of p can occur in f and an extra res, referring to
the result of the procedure application, can occur in g.
Following the literature we call f and g the pre- and post-expectations.
When g is a predicate, i.e. {0,1} valued function on memories, then f gives an upper-bound,
on the probability that p halts in a state state satisfying g, as a function in the initial memory.
This way, eHoare can be used to reason about probabilities
of events. Since it shares many rules, eHoare can be seen as a a generalisation of conventional, classical Hoare logic,
to a probabilistic setting.
In Easycrypt, an eHoare judgment for a procedure proc is proven following the syntax
ehoare proc vars : proc : f ==> g.
proof.
[tactics]
qed.
In what follows, we provide a synopsis on those tactics implemented within Easycrypt to carry out an eHoare proof.
Many of the tactics work similar to that of standard (probabilistic) Hoare tactics, but operate on an auxiliary judgments
ehoare [ C : f ==> g ]
where
C is a program statement, and pre-/post-expectations f,g are xreal expressions
over the program variables. By slight abuse of notation, this judgment is valid
if
forall m : mem, Ep [C]_m g <= f m
for [C]_m the output (sub)distribution of memories given by running C on initial memory m, and where Ep : 'a distr -> ('a -> xreal) -> xreal computes the expectation of an extended
real function on the given distribution.
A variety of the rules make use of the operator (`|` : bool -> xreal -> xreal) to combine
classical and probabilistic reasoning.
Specifically, ehoare [ C : (P `|` f) ==> (Q `|` g) ] should be understood
as a judgment ehoare [ C : f ==> g ] restricted to initial memories satisfying
the pre-condition P, and simultaneously establishing post-condition Q.
As in probabilistic Hoare logic, the proc tactic is used to show that a procedure judgment
ehoare [ p : f ==> g ] is correct, by lifting the judgment to one on the procedures body.
It is usually the entry point in a proof. Assuming proc p(args) : ty = { C ; return E },
the tactic proc implements the rule
ehoare[ C : f ==> g[ret/E] ]
----------------------------
ehoare[ p : f ==> g ]
Tactic skip proves ehoare[ C : f ==> f ] for all f
For simple program fragments D not involving loops or procedure calls, a weakest (i.e. smallest)
pre-expectation wp(D,g) given post-expectation g can be computed automatically. Specifically,
wp(skip, g) := g
wp(x <- E,g) := g[x/E]
wp(x <$ S,g) := Ep S (fun v => g[x/v])
wp(if b then C else D,g) := (b `|` ft) + (!b `|` ff)
where wp(C,g) = ft
and wp(D,g) = ff
Tactic wp implements notion in conjunction with an application of the seq rule:
ehoare[ C : f ==> wp(D,g) ]
---------------------------
ehoare[ C; D : f ==> g ]
Tactic seq [n] splits a sequence of program statements according to the rule
ehoare[ C : f ==> h ] ehoare[ C : h ==> g ]
---------------------------------------------
ehoare [ C; D : f ==> g ]
The optional integer n defines at which point a sequence of commands is split
Tactic if eliminates conditionals according to the rule
ehoare[ C : (b `|` f) ==> g ] ehoare[ C : (!b `|` f) ==> g ]
--------------------------------------------------------------
ehoare [ if b then C else D : f ==> g ]
Unlike for the probabilistic Hoare logic, the rule for while-loops in eHoare resembles closely the one of conventional Hoare logic:
ehoare [ C : (b `|` f) ==> f ]
-------------------------------------------
ehoare [ while b { C } : f ==> (!b `|` f) ]
In an application of this rule, the (upper) invariant f has to be specifically provided. The corresponding
tactic is while f.
[TODO]
[TODO]
See [TODO]