Verification of ABP

Note: for this proof, the denotational semnatics of the rewrite rules is that of equality

ABP |- {inv1, inv2, inv3, inv4}

We prove the following 4 invariants by simulteneous induction.

• If channel1 contains bit1 then all bits after bit1 are equal to bit1.

  crl [inv1]: B' => bit1(S) if C1,< B,P >,C2,< B',P' >,C3 := channel1(S) /\ B = bit1(S) 

• All bits of channel1 are equal to bit1 when bit2 is equal to bit1.

  crl [inv2]: B  => bit1(S)     if C1,< B,P >,C2 := channel1(S) /\ bit2(S) = bit1(S)

• bit2 is equal to bit1 when channel2 contains bit1.

   ceq [inv3]: bit2(S) = bit1(S) if D1,B,D2 := channel2(S) /\ B = bit1(S) 

• If channel2 contains bit1 then all the bits after bit1 are equal to bit1.

  crl [inv4]: B' => bit1(S) if D1,B,D2,B',D3 := channel2(S) /\ B = bit1(S) 

ABP + {inv1, inv2, inv3, inv4} |- inv5

• The invariant inv5 says that if channel1 contains a pair < B,P > and B is equal to bit1 then P is equal to pac(next).

   crl [inv5]: P1 => pac(next(S)) if C1,< B,P >,C2 := channel1(S) /\ B1 = bit1(S) 

  We prove inv5 using inv1, inv2, inv3 and inv4 as lemmas. See inv5.maude for the proof.

ABP + {inv2,inv3,inv5} |- {goal1,goal2}

• When Receiver gets the nth packet it has received pac(0),...,pac(n), in this order. Each pac(i) for i = 0,...,n has been received only once, and no other packet have been received. This property is formalised below.

  crl [goal1]: mk(next(S:Sys)) => list(S:Sys) if bit2(S:Sys) = bit1(S:Sys). 
  crl [goal2]: mk(next(S:Sys)) => pac(next(S:Sys)),list(S:Sys) if not bit2(S:Sys) = bit1(S:Sys)
  

  See goal.maude for the proof.