diff --git a/doc/tactics/if.rst b/doc/tactics/if.rst new file mode 100644 index 000000000..b39cfe715 --- /dev/null +++ b/doc/tactics/if.rst @@ -0,0 +1,227 @@ +======================================================================== +Tactic: ``if`` +======================================================================== + +In EasyCrypt, the ``if`` tactic is a way of reasoning about program(s) +that use conditionals. When a program begins with an if statement, +execution will follow one path if the condition is ``true`` and another +path if it is ``false``. The tactic says that to prove the program is +correct, you must consider both cases: you assume the condition holds +and show that the *then* branch establishes the desired result, and you +assume the condition does not hold and show that the *else* branch +establishes the same result. EasyCrypt allows you to apply this rule +only when the program starts with an if, so the proof can split immediately +from the initial state. If the conditional appears deeper in the code, +you must first use the ``seq`` tactic to separate the earlier commands +from the conditional. + +.. contents:: + :local: + +------------------------------------------------------------------------ +Variant: ``if`` (HL) +------------------------------------------------------------------------ + +.. ecproof:: + :title: Hoare logic example + + require import AllCore. + + module M = { + proc f(x : int) = { + var y : int; + + if (x < 0) { + y <- -x; + } else { + y <- x; + } + + return y; + } + }. + + pred p : glob M. + + lemma L : hoare[M.f : p (glob M) ==> 0 <= res]. + proof. + proc. + (*$*) if. + (* First goal: (x < 0) holds *) + - wp. skip. smt(). + (* Second goal: (x < 0) does not hold *) + - wp. skip. smt(). + qed. + +------------------------------------------------------------------------ +Variant: ``if`` (pRHL) +------------------------------------------------------------------------ + +In probabilistic relational Hoare logic, the ``if`` tactic is applied +in a lock-step manner, meaning that the two programs being compared must +proceed through the conditional in sync. This requires that their guards +evaluate to the same boolean value in the related states, so that either +both programs take the *then* branch or both take the *else* branch. + +As a result, using the ``if`` tactic involves establishing that the two +conditions are equal under the current relational invariant before +splitting into the two synchronized cases. + +Although synchronization ensures both guards take the same value, the +implementation splits only on the left guard (rather than explicitly +stating both are true or both are false). + +.. ecproof:: + :title: Relational Hoare logic example (2-sided) + + require import AllCore. + + module M = { + proc f(x : int) = { + var y : int; + + if (x < 0) { + y <- -x; + } else { + y <- x; + } + + return y; + } + }. + + lemma L : equiv[M.f ~ M.f: x{1} = x{2} ==> res{1} = res{2}]. + proof. + proc. + (*$*) if. + (* First goal: we prove that the guards are in sync. *) + - smt(). + (* First goal: (x < 0) holds *) + - wp; skip. smt(). + (* Second goal: (x < 0) does not hold *) + - wp; skip. smt(). + qed. + + +------------------------------------------------------------------------ +Variant: ``if {side}`` (pRHL) +------------------------------------------------------------------------ + +In the one-sided ``if`` tactic used in pRHL, the user specifies whether +the conditional reasoning should be applied to the left or the right +program. The tactic then performs a case analysis only on the ``if`` +statement at the top of that chosen program, generating separate goals +for the ``true`` and ``false`` branches on that side. Unlike the lock-step +relational ``if`` tactic, no synchronization of guards is required, and +the other program is not constrained to take the same branch or even to +have a similar structure. + +.. ecproof:: + :title: Relational Hoare logic example (1-sided) + + require import AllCore. + + module M = { + proc f(x : int) = { + var y : int; + + if (x < 0) { + y <- -x; + } else { + y <- x; + } + + return y; + } + + proc g(x : int) = { + return `|x|; + } + }. + + lemma L : equiv[M.f ~ M.g: x{1} = x{2} ==> res{1} = res{2}]. + proof. + proc. + (*$*) if{1}. + (* First goal: (x < 0) holds (left program) *) + - wp; skip. smt(). + (* Second goal: (x < 0) does not hold (left program) *) + - wp; skip. smt(). + qed. + +------------------------------------------------------------------------ +Variant: ``if`` (pHL) +------------------------------------------------------------------------ + +In probabilistic Hoare logic, the ``if`` tactic behaves much like in +standard Hoare logic, except that the postcondition is expressed in terms +of a probability bound. Since the if statement is the first command of +the program, its guard is evaluated immediately in the initial state and +therefore deterministically takes either the ``true`` or the ``false`` +value, with probability 1. As a result, the program execution splits into +one of the two branches without introducing any additional probabilistic +choice at the level of control flow, and the probability bound is preserved +by reasoning separately about each branch under the corresponding +assumption on the guard. + +.. ecproof:: + :title: Probabilistic Hoare logic example + + require import AllCore. + + module M = { + proc f(x : int) = { + var y : int; + + if (x < 0) { + y <- -x; + } else { + y <- x; + } + + return y; + } + }. + + lemma L : phoare[M.f : true ==> 0 <= res] = 1%r. + proof. + proc. + (*$*) if. + (* First goal: (x < 0) holds *) + - wp; skip. smt(). + (* Second goal: (x < 0) does not hold *) + - wp; skip. smt(). + qed. + +------------------------------------------------------------------------ +Variant: ``if`` (eHL) +------------------------------------------------------------------------ + +.. ecproof:: + :title: Expectation Hoare logic example + + require import AllCore Xreal. + + module M = { + proc f(x : int) = { + var y : int; + + if (x < 0) { + y <- -x; + } else { + y <- x; + } + + return y; + } + }. + + lemma L : ehoare[M.f : 0%xr ==> (0 <= res)%xr]. + proof. + proc. + (*$*) if. + (* First goal: (x < 0) holds *) + - wp; skip. admit. (* FIXME *) + (* Second goal: (x < 0) does not hold *) + - wp; skip. admit. (* FIXME *) + qed.