Safety of causal broadcast algorithm (and implementation) in Agda

cbcast.agda

open import Data.Nat using (ℕ)

-- the whole module is parameterized over the number of processes n
module cbcast (n : ℕ) where

open import Data.Bool using (Bool; true; false; _∧_)
open import Data.Nat using (_+_; _≤_; _<_; _≟_; _≤?_)
open import Data.Nat.Properties using (≤-trans; 1+n≰n; +-comm)
open import Data.Fin as Fin using (Fin)
open import Data.Vec using (Vec; []; _∷_; lookup; allFin; map; foldr)
open import Data.Vec.Properties using (∷-injectiveˡ;  ∷-injectiveʳ)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Empty using (⊥-elim)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using (True; False; toWitness; fromWitnessFalse)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; trans; sym; subst)

open import iter using (iterDec)

VectorClock : Set
VectorClock = Vec ℕ n

_[_] : VectorClock → Fin n → ℕ
vc [ k ] = lookup vc k

record Message : Set where
  constructor Msg
  field
    id : Fin n
    vc : VectorClock

record Process : Set where
  constructor Proc
  field
    id : Fin n
    vc : VectorClock

deliverableK : Message → Process → Fin n → Set
deliverableK (Msg senderId vcₘ) (Proc _ vcₚ) k =   (k ≡ senderId → vcₘ [ k ] ≡ vcₚ [ k ] + 1)
                                                 × (k ≢ senderId → vcₘ [ k ] ≤ vcₚ [ k ])

deliverable : Message → Process → Set
deliverable m p = ∀ k → deliverableK m p k

causallyBeforeK : Message → Message → Fin n → Set
causallyBeforeK (Msg _ vc₁) (Msg _ vc₂) k =   vc₁ [ k ] ≤ vc₂ [ k ]
                                            × vc₁ ≢ vc₂ -- we compare vc₁ and vc₂ for every k just to make deliverable and _causallyBefore uniform

_causallyBefore_ : Message → Message → Set
m₁ causallyBefore m₂ = ∀ k → causallyBeforeK m₁ m₂ k

postulate processOrder : ∀ (m₁ m₂ : Message) → let (Msg senderId₁ vc₁) = m₁
                                                   (Msg senderId₂ vc₂) = m₂
                                               in senderId₁ ≡ senderId₂ → vc₁ [ senderId₁ ] ≢ vc₂ [ senderId₂ ]

safety : ∀ (p : Process) (m₁ m₂ : Message)
         → deliverable m₁ p
         → m₁ causallyBefore m₂
         → ¬ (deliverable m₂ p)
safety (Proc _ vcₚ) m₁@(Msg senderId₁ vc₁) m₂@(Msg senderId₂ vc₂)
       m₁dp m₁beforem₂ m₂dp with senderId₁ Fin.≟ senderId₂
...                            | (yes refl)   = let vc₁[senderId₁]≡vcₚ[senderId₁]+1 = (proj₁ (m₁dp senderId₁)) refl
                                                    vc₂[senderId₁]≡vcₚ[senderId₁]+1 = (proj₁ (m₂dp senderId₂)) refl
                                                    vc₁[senderId₁]≡vc₂[senderId₁]   = trans vc₁[senderId₁]≡vcₚ[senderId₁]+1 (sym vc₂[senderId₁]≡vcₚ[senderId₁]+1)
                                                in processOrder m₁ m₂ refl vc₁[senderId₁]≡vc₂[senderId₁]
...                            | (no notSame) = let vc₁[senderId₁]≡vcₚ[senderId₁]+1 = (proj₁ (m₁dp senderId₁)) refl
                                                    vc₂[senderId₁]≤vcₚ[senderId₁]   = (proj₂ (m₂dp senderId₁)) notSame
                                                    vc₁[senderId₁]≤vc₂[senderId₁]   = proj₁ (m₁beforem₂ senderId₁)
                                                    vc₁[senderId₁]≤vcₚ[senderId₁]   = ≤-trans vc₁[senderId₁]≤vc₂[senderId₁] vc₂[senderId₁]≤vcₚ[senderId₁]
                                                in lemma vc₁[senderId₁]≡vcₚ[senderId₁]+1 vc₁[senderId₁]≤vcₚ[senderId₁]
  where
    lemma : ∀ {i j : ℕ} → (i ≡ j + 1) → ¬ (i ≤ j)
    lemma {i} {j} i≡j+1 rewrite i≡j+1 | +-comm j 1 = 1+n≰n

-- implementation

deliverableImplK : ∀ (m : Message) → (p : Process) → (k : Fin n) → Dec (deliverableK m p k)
deliverableImplK (Msg senderId vcₘ) (Proc _ vcₚ) k with k Fin.≟ senderId
...                                                   | (yes ev) with vcₘ [ k ] ≟ vcₚ [ k ] + 1
...                                                                | (yes ev') = yes ((λ x → ev') , λ x → ⊥-elim (x ev))
...                                                                | (no  ev') = no  λ x → ev' ((proj₁ x) ev)
deliverableImplK (Msg senderId vcₘ) (Proc _ vcₚ) k    | (no  ev) with vcₘ [ k ] ≤? vcₚ [ k ]
...                                                                | (yes ev') = yes ((λ x → ⊥-elim (ev x)) , λ x → ev')
...                                                                | (no  ev') = no  λ x → ev' (proj₂ x ev)

_vec≡?_ : ∀ {n} (vec₁ vec₂ : Vec ℕ n) → Dec (vec₁ ≡ vec₂)
[]       vec≡? []       = yes refl
(x ∷ xs) vec≡? (y ∷ ys) with x ≟ y
...                        | (yes ev) with xs vec≡? ys
...                                      | (yes ev') = yes (helper ev ev')
  where helper : x ≡ y → xs ≡ ys → x ∷ xs ≡ y ∷ ys
        helper refl refl = refl
...                                      | (no  ev') = no  λ z → ev' (∷-injectiveʳ z)
(x ∷ xs) vec≡? (y ∷ ys)    | (no  ev) = no λ z → ev (∷-injectiveˡ z)

causallyBeforeImplK : ∀ (m₁ : Message) → (m₂ : Message) → (k : Fin n) → Dec (causallyBeforeK m₁ m₂ k)
causallyBeforeImplK (Msg _ vc₁) (Msg _ vc₂) k with vc₁ [ k ] ≤? vc₂ [ k ] | vc₁ vec≡? vc₂
...                                              | (yes ev₁)              | (yes ev₂)  = no  λ x → (proj₂ x) ev₂
...                                              | (yes ev₁)              | (no  ev₂)  = yes (ev₁ , ev₂)
...                                              | (no  ev₁)              | (yes ev₂)  = no  λ x → proj₂ x ev₂
...                                              | (no  ev₁)              | (no  ev₂)  = no  λ x → ev₁ (proj₁ x)

deliverableImpl : ∀ (m : Message) → (p : Process) → Dec (deliverable m p)
deliverableImpl m p = iterDec (deliverableImplK m p)

_causallyBeforeImpl_ : ∀ (m₁ m₂ : Message) → Dec (m₁ causallyBefore m₂)
m₁ causallyBeforeImpl m₂ = iterDec (causallyBeforeImplK m₁ m₂)

safetyImpl : ∀ (p : Process) (m₁ m₂ : Message)
           → True (deliverableImpl m₁ p)
           → True (m₁ causallyBeforeImpl m₂)
           → False (deliverableImpl m₂ p)
safetyImpl p m₁ m₂ m₁dp m₁beforem₂ = fromWitnessFalse (safety p m₁ m₂ (toWitness m₁dp) (toWitness m₁beforem₂))

iter.agda

module iter where

open import Function using (_∘_)
open import Data.Bool using (Bool; true; false; _∧_; T)
open import Data.Nat as ℕ using (ℕ; zero; suc)
open import Data.Fin using (Fin)
open import Data.Vec using (Vec; []; _∷_; foldr; map; allFin; lookup)
open import Data.Vec.Properties using (lookup-map; lookup-allFin)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (isYes; toWitness; fromWitness)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst; inspect; [_])

-- iterate over every element in Fin n and apply f, then and the results together
-- it has the effect as forall in logic
iter : ∀ {n} → (Fin n → Bool) → Bool
iter {n} f = foldr (λ _ → Bool) _∧_ true (map f (allFin n))

≡-distrib-∧ : ∀ {x y} → x ∧ y ≡ true → (x ≡ true) × (y ≡ true)
≡-distrib-∧ {true} {true} x∧y≡true = refl , refl

T→∧ : ∀ {a b} → T (a ∧ b) → T a × T b
T→∧ {true} {true} _ = tt , tt

∧→T : ∀ {a b} → T a × T b → T (a ∧ b)
∧→T {true} {true} _ = tt

fold→lookup : ∀ {n} {v : Vec Bool n}
              → T (foldr (λ _ → Bool) _∧_ true v)
              → ∀ (k) → T (lookup v k)
fold→lookup {_} {[]}     Tfold ()
fold→lookup {_} {x ∷ xs} Tfold Fin.zero    = proj₁ (T→∧ Tfold)
fold→lookup {_} {x ∷ xs} Tfold (Fin.suc k) = fold→lookup {v = xs} (proj₂ (T→∧ Tfold)) k

iter→forall : ∀ {n} {f : Fin n → Bool} {P : Fin n → Set}
              → (∀ k → T (f k) → P k)
              → T (iter f)
              → ∀ k → P k
iter→forall {n} {f} {_} f[k]→P[k] Titer k = f[k]→P[k] k helper
  where
    helper : T (f k)
    helper rewrite sym (lookup-allFin k) | sym (lookup-map k f (allFin n)) = fold→lookup {v = map f (allFin n)} Titer k

lookup→fold : ∀ {n} {v : Vec Bool n}
              → (∀ k → T (lookup v k))
              → T (foldr (λ _ → Bool) _∧_ true v)
lookup→fold {_} {[]}     Tlookup = tt
lookup→fold {_} {x ∷ xs} Tlookup = ∧→T {x} (Tlookup Fin.zero , lookup→fold {v = xs} λ k → Tlookup (Fin.suc k))

forall→iter : ∀ {n} {f : Fin n → Bool} {P : Fin n → Set}
              → (∀ k → P k → T (f k))
              → (∀ k → P k)
              → T (iter f)
forall→iter {n} {f} {_} P[k]→f[k] P[k] = lookup→fold {v = map f (allFin n)} helper
  where
    helper : (k : Fin n) → T (lookup (map f (allFin n)) k)
    helper k rewrite lookup-map k f (allFin n) | lookup-allFin k = P[k]→f[k] k (P[k] k)

-- calculate the same result as the above iter with additional proof
iterDec : ∀ {n} {P : Fin n → Set} → (∀ k → Dec (P k)) → Dec (∀ k → P k)
iterDec {_} {P} f with iter (isYes ∘ f) | inspect iter (isYes ∘ f)
...                  | true             | [ iter≡true ]            = yes (iter→forall (λ _ x → toWitness x) (subst T (sym iter≡true) tt))
...                  | false            | [ iter≡false ]           = no  λ x → subst T iter≡false (forall→iter (λ _ x → fromWitness x) x)

tickSameAsCombine.agda

open import Data.Nat using (ℕ)

module tickSameAsCombine (n : ℕ)  where

open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.Nat using (_+_; _≤ᵇ_; _≤_; _≰_; _≤?_) renaming (_⊔_ to max)
open import Data.Nat.Properties using ()
open import Data.Fin as Fin using (Fin; suc; zero; toℕ; _≟_)
open import Data.Fin.Properties using (suc-injective)
open import Data.Vec using (Vec; []; _∷_; lookup)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Empty using (⊥-elim)
open import Relation.Nullary using (yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; _≢_; sym; cong)

open import cbcast n using (VectorClock; Message; Msg; Process; Proc; deliverable)

vcTickImpl : ∀ {n} → Fin n → Vec ℕ n → Vec ℕ n
vcTickImpl zero      (x ∷ xs) = x + 1 ∷ xs
vcTickImpl (suc fn') (x ∷ xs) = x ∷ vcTickImpl fn' xs

vcTick : Fin n → VectorClock → VectorClock
vcTick p xs = vcTickImpl p xs

vcCombineImpl : ∀ {n} → Vec ℕ n → Vec ℕ n → Vec ℕ n
vcCombineImpl []       []       = []
vcCombineImpl (x ∷ xs) (y ∷ ys) with x ≤? y
...                                | (yes _) = y ∷ vcCombineImpl xs ys
...                                | (no  _) = x ∷ vcCombineImpl xs ys

vcCombine : VectorClock → VectorClock → VectorClock
vcCombine xs ys = vcCombineImpl xs ys

-- proof

postulate lemma₁ : ∀ {n} {fn : Fin n} → suc fn ≢ zero
postulate lemma₂ : ∀ {n} {fn : Fin n} → zero ≢ suc fn

tickCorrect : ∀ {n} (idx : Fin n) (v : Vec ℕ n)
              → ∀ (k : Fin n)
              →   (k ≡ idx → lookup (vcTickImpl idx v) k ≡ lookup v k + 1)
                × (k ≢ idx → lookup (vcTickImpl idx v) k ≡ lookup v k)
tickCorrect zero (x ∷ xs) zero         = (λ _ → refl) , λ t → ⊥-elim (t refl)
tickCorrect zero (x ∷ xs) (suc k)      = (λ t → ⊥-elim (lemma₁ t)) , λ _ → refl
tickCorrect (suc idx) (x ∷ xs) zero    = (λ t → ⊥-elim (lemma₂ t)) , λ _ → refl
tickCorrect (suc idx) (x ∷ xs) (suc k) = (λ t → proj₁ (tickCorrect idx xs k) (suc-injective t)) , λ t → proj₂ (tickCorrect idx xs k) λ t' → t (cong suc t')

combineCorrect : ∀ {n} (v₁ v₂ : Vec ℕ n)
                 → ∀ (k : Fin n)
                 →   (lookup v₁ k ≤ lookup v₂ k → lookup (vcCombineImpl v₁ v₂) k ≡ lookup v₂ k)
                   × (lookup v₁ k ≰ lookup v₂ k → lookup (vcCombineImpl v₁ v₂) k ≡ lookup v₁ k)
combineCorrect (x ∷ xs) (y ∷ ys) k       with x ≤? y
combineCorrect (x ∷ xs) (y ∷ ys) zero       | (yes ev) = (λ _ → refl) , λ t → ⊥-elim (t ev)
combineCorrect (x ∷ xs) (y ∷ ys) zero       | (no  ev) = (λ t → ⊥-elim (ev t)) , λ _ → refl
combineCorrect (x ∷ xs) (y ∷ ys) (suc k)    | (yes ev) = (λ t → proj₁ (combineCorrect xs ys k) t) , λ t → proj₂ (combineCorrect xs ys k) t
combineCorrect (x ∷ xs) (y ∷ ys) (suc k)    | (no  ev) = (λ t → proj₁ (combineCorrect xs ys k) t) , λ t → proj₂ (combineCorrect xs ys k) t

-- extensional equality
_ex≡_ : ∀ {n} {A} → Vec A n → Vec A n → Set
_ex≡_ {n} {A} v₁ v₂ = ∀ (k : Fin n) → lookup v₁ k ≡ lookup v₂ k

-- extensional implies intensional equality
ex≡→≡ : ∀ {n} {A} {v₁ v₂ : Vec A n} → v₁ ex≡ v₂ → v₁ ≡ v₂
ex≡→≡ {_} {_} {[]}     {[]}     v₁ex≡v₂                                                                          = refl
ex≡→≡ {_} {_} {x ∷ xs} {y ∷ ys} v₁ex≡v₂ rewrite v₁ex≡v₂ zero | ex≡→≡ {v₁ = xs} {v₂ = ys} (λ k → v₁ex≡v₂ (suc k)) = refl

postulate lemma : ∀ {a b} → a ≡ b + 1 → a ≰ b

tick-ex≡-combine : ∀ (m : Message) (p : Process)
                   → deliverable m p
                   → vcTick (Message.id m) (Process.vc p) ex≡ vcCombine (Message.vc m) (Process.vc p)
tick-ex≡-combine (Msg senderId vcₘ) (Proc _ vcₚ) mdp k
  with k ≟ senderId | lookup vcₘ k ≤? lookup vcₚ k
...  | (yes refl)   | (yes ev)                     = ⊥-elim (lemma (proj₁ (mdp k) refl) ev)
...  | (no  ev₁)    | (no  ev₂)                    = ⊥-elim (ev₂ (proj₂ (mdp k) ev₁))
...  | (yes refl)   | (no  ev)                     rewrite proj₁ (tickCorrect senderId vcₚ k) refl
                                                         | proj₂ (combineCorrect vcₘ vcₚ k) ev = sym (proj₁ (mdp k) refl)
...  | (no  ev₁)    | (yes ev₂)                    rewrite proj₂ (tickCorrect senderId vcₚ k) ev₁
                                                         | proj₁ (combineCorrect vcₘ vcₚ k) ev₂ = refl

tick≡combine : ∀ (m : Message) (p : Process)
                 → deliverable m p
                 → vcTick (Message.id m) (Process.vc p) ≡ vcCombine (Message.vc m) (Process.vc p)
tick≡combine m p mdp = ex≡→≡ (tick-ex≡-combine m p mdp)