open import Tagged
open import GeneralLemmas using (Dec; _≡_)
module Backup
  {Machine Msg : Set}
  (_⟶Machine<_>_ : Machine  Tagged Msg  Machine  Set)
  where

open import GeneralLemmas
open import Relation

-- | A machine that can crash
data _⟶Crashy<_>_ : Maybe Machine  Tagged Msg  Maybe Machine  Set where

  -- | The underlying machine takes a normal step
  normal-step :  {tmsg m m'} 
    m ⟶Machine< tmsg > m' 
    just m ⟶Crashy< tmsg > just m'

  -- | The machine crashes
  CRASH :  {m} 
    just m ⟶Crashy< silent > nothing

-- | A machine with a backup
Backup = Machine × Machine
data _⟶Backup<_>_ : Backup  Tagged Msg  Backup  Set where
  silent-step :  {m n m'} 
    just m ⟶Crashy< silent > just m' 
    (m , n)  ⟶Backup< silent > (m' , n)

  receive-step :  {m n m' msg} 
    just m ⟶Crashy< receive msg > just m' 
    (m , n)  ⟶Backup< receive msg > (m' , m') -- create backup

  send-step :  {m n m' msg} 
    just m ⟶Crashy< send msg > just m' 
    (m , n)  ⟶Backup< send msg > (m' , m') -- create backup

  recover :  {m n} 
    just m  ⟶Crashy< silent > nothing 
    (m , n) ⟶Backup< silent > (n , n)

-- | The transition relation for a single node
_⟶Machine_ : Machine  Machine  Set
m₁ ⟶Machine m₂ =  λ tmsg  m₁ ⟶Machine< tmsg > m₂

module Assumptions
  (active : Machine  Set)
  (is-active : (m : Machine)  Dec (active m))
  (active-silent-active :  {m m'} 
    m ⟶Machine< silent > m'  active m × active m')
  (active-send-inactive :  {m m' msg} 
    m ⟶Machine< send    msg > m'  active m × ¬ (active m'))
  (inactive-receive-active :  {m m' msg} 
    m ⟶Machine< receive msg > m'  ¬ (active m) × active m')
  where
  _⟶Machine*_ = _⟶Machine_ *

  _⟶MSilent_ : Machine  Machine  Set
  m₁ ⟶MSilent b₂ = m₁ ⟶Machine< silent > b₂
  _⟶MSilent*_ = _⟶MSilent_ *

  _⟶Backup_ : Backup  Backup  Set
  b₁ ⟶Backup b₂ =  λ tmsg  b₁ ⟶Backup< tmsg > b₂
  _⟶Backup*_ = _⟶Backup_ *

  _⟶BSilent_ : Backup  Backup  Set
  b₁ ⟶BSilent b₂ = b₁ ⟶Backup< silent > b₂
  _⟶BSilent*_ = _⟶BSilent_ *

  data IO (A : Set) : Set where
    send receive : A  IO A

  -- | The input/output behaviour of a trace (ignores silent steps)
  ⟦_⟧B :  {b₁ b₂}  b₁ ⟶Backup* b₂  List (IO Msg)
   [] ⟧B = []
   ((silent        , _)  steps) ⟧B =  steps ⟧B
   ((send     msg  , _)  steps) ⟧B = send     msg   steps ⟧B
   ((receive  msg  , _)  steps) ⟧B = receive  msg   steps ⟧B

  ⟦_⟧M :  {m₁ m₂}  m₁ ⟶Machine* m₂  List (IO Msg)
   [] ⟧M = []
   ((silent        , _)  steps) ⟧M =  steps ⟧M
   ((send     msg  , _)  steps) ⟧M = send     msg   steps ⟧M
   ((receive  msg  , _)  steps) ⟧M = receive  msg   steps ⟧M

  activeB : Backup  Set
  activeB (b , _) = active b

  inactiveM : Machine  Set
  inactiveM m = ¬ active m

  inactiveB : Backup  Set
  inactiveB b = ¬ activeB b

  soundness :  {m₁ m₂ b₁}
    (mtrace : m₁ ⟶Machine* m₂) 
    ∃₂ λ b₂ (btrace : (m₁ , b₁) ⟶Backup* (m₂ , b₂)) 
          btrace ⟧B   mtrace ⟧M
  soundness [] = _ , [] , refl
  soundness ((silent , st)  mtrace) =
    let (b₂ , btrace , eq) = soundness mtrace
     in b₂ , (silent , silent-step (normal-step st))  btrace , eq
  soundness ((send msg , st)  mtrace) =
    let (b₂ , btrace , eq) = soundness mtrace
     in b₂ , (send msg , send-step (normal-step st))  btrace , cong (_∷_ _) eq
  soundness ((receive msg , st)  mtrace) =
    let (b₂ , btrace , eq) = soundness mtrace
     in b₂ , (receive msg , receive-step (normal-step st))  btrace , cong (_∷_ _) eq

  thread-crashes :  {m₁ m₂}  m₁ ⟶Backup* m₂  Set
  thread-crashes [] = 
  thread-crashes (_∷_  (.silent , silent-step x) s) = thread-crashes s
  thread-crashes (_∷_  (._ , receive-step x) s) = 
  thread-crashes (_∷_  (._ , send-step x) s) = 
  thread-crashes (_∷_  (.silent , recover x) s) = 

  does-thread-crash :  {m₁ m₂}  (s : m₁ ⟶Backup* m₂)  Dec (thread-crashes s)
  does-thread-crash [] = no  z  z)
  does-thread-crash  (_∷_  (.silent , silent-step x) s) = does-thread-crash s
  does-thread-crash  (_∷_  (._ , receive-step x) s) = no  z  z)
  does-thread-crash  (_∷_  (._ , send-step x) s) = no  z  z)
  does-thread-crash  (_∷_  (.silent , recover x) s) = yes tt

  fast-forward-to-crash :  {m₁ m₂ b₁ b₂ n} 
                      (s : (m₁ , b₁) ⟶Backup* (m₂ , b₂))  thread-crashes s  *length s  n 
                  λ (s' : (b₁ , b₁)  ⟶Backup* (m₂ , b₂))  (¬ thread-crashes s') ×
                                                            ( s ⟧B   s' ⟧B) ×
                                                            (*length s'  n)
  fast-forward-to-crash [] ()
  fast-forward-to-crash  (_∷_  (.silent , silent-step x) s) tc (s≤s len≤n) =
    let (s' , no-crash) = fast-forward-to-crash s tc (≤-steps 1 len≤n)
     in s' , no-crash
  fast-forward-to-crash  (_∷_  (._ , receive-step x) s) () len≤n
  fast-forward-to-crash  (_∷_  (._ , send-step x) s) () len≤n
  fast-forward-to-crash  (_∷_  (.silent , recover x) s) tc (s≤s len≤n) with does-thread-crash s
  ... | yes it-does   = fast-forward-to-crash s it-does (≤-steps 1 len≤n)
  ... | no it-doesn't = s , it-doesn't , refl , ≤-steps 1 len≤n

  fast-forward :  {m₂ b₁ b₂ n} 
                      (s : (b₁ , b₁) ⟶Backup* (m₂ , b₂))  *length s  n 
                  λ (s' : (b₁ , b₁)  ⟶Backup* (m₂ , b₂))  (¬ thread-crashes s') ×
                                                            ( s ⟧B   s' ⟧B) ×
                                                            (*length s'  n)
  fast-forward s len≤n with does-thread-crash s
  ... | yes it-does = fast-forward-to-crash s it-does len≤n
  ... | no it-doesn't = s , it-doesn't , refl , len≤n

  completeness-inactive :  {m₂ b₁ b₂} n
    (bs : (b₁ , b₁) ⟶Backup* (m₂ , b₂))  *length bs  n 
    inactiveB (b₁ , b₁) 
     λ (ms : b₁ ⟶Machine* m₂)   bs ⟧B   ms ⟧M

  completeness-active :  {m₁ m₂ b₁ b₂} n
    (bs : (m₁ , b₁) ⟶Backup* (m₂ , b₂))  *length bs  n 
    activeB (m₁ , b₁)  ¬ thread-crashes bs 
    (backup : b₁ ⟶MSilent* m₁) 
     λ (ms : m₁ ⟶Machine* m₂)   bs ⟧B   ms ⟧M

  completeness-inactive zero [] z≤n inactive = [] , refl
  completeness-inactive zero (_∷_ x steps) () inactive
  completeness-inactive (suc n) [] z≤n inactive = [] , refl
  completeness-inactive (suc n) (_∷_ (.silent , silent-step (normal-step s)) steps) (s≤s len≤n) inactive =
    ⊥-elim (inactive (proj₁ (active-silent-active s)))
  completeness-inactive (suc n) (_∷_ (._ , receive-step (normal-step s)) steps) (s≤s len≤n) inactive =
    let steps' , ¬crash , eq , len'≤n = fast-forward steps len≤n
        msteps , eq' = completeness-active n steps' len'≤n (proj₂ (inactive-receive-active s)) ¬crash []
     in (receive _ , s)  msteps , cong (_∷_ _) (trans eq eq')
  completeness-inactive (suc n) (_∷_ (._ , send-step (normal-step s)) steps) (s≤s len≤n) inactive =
    ⊥-elim (inactive (proj₁ (active-send-inactive s)))
  completeness-inactive (suc n) (_∷_ (.silent , recover CRASH) steps) (s≤s len≤n) inactive =
    completeness-inactive n steps len≤n inactive

  completeness-active zero [] z≤n active ¬crash backup = [] , refl
  completeness-active zero (_∷_ x steps) () active ¬crash backup
  completeness-active (suc n) [] z≤n active ¬crash backup = [] , refl
  completeness-active (suc n) (_∷_ (.silent , silent-step (normal-step s)) steps) (s≤s len≤n) active ¬crash backup =
    let msteps , eq = completeness-active n steps len≤n (proj₂ (active-silent-active s)) ¬crash (backup *++ (s  []))
     in (silent , s)  msteps , eq
  completeness-active (suc n) (_∷_ (._ , receive-step (normal-step s)) steps) (s≤s len≤n) active ¬crash backup =
    ⊥-elim (proj₁ (inactive-receive-active s) active)
  completeness-active (suc n) (_∷_ (._ , send-step (normal-step s)) steps) (s≤s len≤n) active ¬crash backup =
    let msteps , eq = completeness-inactive n steps len≤n (proj₂ (active-send-inactive s))
     in (send _ , s)  msteps , cong (_∷_ _) eq
  completeness-active (suc n) (_∷_ (.silent , recover CRASH) steps) (s≤s len≤n) active ¬crash backup =
    ⊥-elim (¬crash tt)

  completeness :  {b₁ m₂ b₂}
    (bs : (b₁ , b₁) ⟶Backup* (m₂ , b₂)) 
     λ (ms : b₁ ⟶Machine* m₂) 
              bs ⟧B   ms ⟧M
  completeness {b₁ = b₁} bs with is-active b₁
  ... | yes it-is   = let bs' , ¬crash , eq , len≤n = fast-forward bs ≤-refl
                          ms , eq' = completeness-active (*length bs') bs' ≤-refl it-is ¬crash []
                       in ms , trans eq eq'
  ... | no it's-not = completeness-inactive (*length bs) bs ≤-refl it's-not