Tactic: async while Tactic

The async while tactic applies to probabilistic relational Hoare Logic goals where the programs contains a while loop. Unlike the while tactic, the async while tactic allows to reason on loops which are not in lockstep.

Syntax

The general form of the tactic is:

Syntax

async while [f1,k1] [f2,k2] (L1) (L2) : (I)

Here:

• L1 and L2 are the left and right condition to control if we consider the lockstep case, or the oneside case,

• k1 and k2 are natural number

• f1 and f2 are the unrolling condition, initial by the parameter k1 and k2.

Concretely, the tactic implements the following rule:

I => (b1 <=> b2 /\ (!L1 /\ !L2 => f1 k1 /\ f2 k2)) \/ (L1 /\ b1) \/ (L2 /\ b2)
   equiv[ while (b1 /\ f1 k1) {c1} ~ while (b2 /\ f2 k2) {c2}:
          I /\ b1 <=> b2 /\ !L1 /\ !L2 /\ f1 k1 /\ f2 k2 ==> I ]
                   hoare[ c1: I /\ b1 /\ L1 /\ ==> I ]
                   hoare[ c2: I /\ b2 /\ L2 /\ ==> I ]
              phoare[ while b1 {c1}: I /\ b1 /\ L1 /\ ==> True ]
              phoare[ while b2 {c2}: I /\ b2 /\ L2 /\ ==> True ]
                (Pre => I) /\  (I /\ !b1 /\ !b2  => Post)
-------------------------------------------------------------------------------
             equiv[while b1 {c1} ~ while b2 {c2}:  Pre ==> Post]

The following example shows async while on a prhl goal. The program increments x until it reaches 10.

[easycrypt failed]