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 can first use the seq tactic (or another tactic such as sp that eliminates the earlier statements) to separate the preceding statements from the conditional.

Variant: if (HL)

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).

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.

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.

Variant: if (eHL)

In expectation Hoare logic, the if tactic behaves similarly to standard Hoare logic. Two subgoals are generated, where the pre-expection is additionally guarded by the branch condition and its negation, respectively. This naturally splits the goal of proving the upper-bound into two cases along the control flow.