Theory Dali_Combined


theory Dali_Combined
  imports "HOL-CSPM" "HOL-CSP.GenFixrec-HOLCF" "GenFixrec-RS"
begin

text ‹ This model is based on the IFM 2025 Article: 
"Model-Checking Buffered Durable Linearizability in CSP" by 
Edmonds, C., Derrick, J., Dongol, B., Schellhorn, G., Wehrheim, H.

A Zenodo Distribution on  the sources can be found under:
🌐‹https://zenodo.org/records/15041794›.

Meanwhile, a corrigendum appeared.
›

type_synonym NodeIds = nat
type_synonym Keys    = nat
type_synonym Pointer = nat
type_synonym Values  = nat   (* better completely parametric ? 'a ?? *)
type_synonym Tids    = nat
type_synonym Epoches = nat

text‹The data of the model are indexed by natural numbers; their ranges are bounded by the
parameters of the locale ‹Dali› below (instead of an ad-hoc finitization by enumeration types).›

datatype NodeIDType      = Null | N NodeIds
datatype KeyType         = K Keys
datatype Pointers        = Bot | P Pointer
datatype ValType         = TNull | V Values
datatype ThreadID        = Th Tids
datatype BucketEpochType = BE Epoches

text‹Names for the first elements, as in the original (finite) model:›

abbreviation ‹N0 ≡ N 0›    abbreviation ‹N1 ≡ N 1›    abbreviation ‹N2 ≡ N 2›
abbreviation ‹K0 ≡ K 0›    abbreviation ‹K1 ≡ K 1›
abbreviation ‹P0 ≡ P 0›    abbreviation ‹P1 ≡ P 1›    abbreviation ‹P2 ≡ P 2›
abbreviation ‹V0 ≡ V 0›    abbreviation ‹V1 ≡ V 1›
abbreviation ‹T0 ≡ Th 0›   abbreviation ‹T1 ≡ Th 1›   abbreviation ‹T2 ≡ Th 2›
abbreviation ‹BE0 ≡ BE 0›  abbreviation ‹BE1 ≡ BE 1›  abbreviation ‹BE2 ≡ BE 2›

datatype channels = initNode ‹NodeIDType × KeyType × ValType›
  | getVal ‹NodeIDType × ValType›
  | getKey ‹NodeIDType × KeyType›
  | getNext ‹NodeIDType × NodeIDType›
  | setNext ‹NodeIDType × NodeIDType›
  | noFreeNode
  | persistNode NodeIDType
  | crash

  | setPointerNode ‹Pointers × NodeIDType›
  | getPointerNode ‹Pointers × NodeIDType›

  | getActiveNode Pointers
  | getCommittedNode Pointers
  | getFlightNode Pointers
  | getBucketEpoch BucketEpochType
  | setStat ‹Pointers × Pointers × Pointers × BucketEpochType›

  | lock
  | unlock

  | invRead ‹ThreadID × KeyType›
  | resRead ‹ThreadID × ValType›

  | invUpdate ‹ThreadID × KeyType × ValType›
  | resUpdate ThreadID
  | resUpdateFull ThreadID

  | getGlobalEpoch ‹ThreadID × BucketEpochType›
  | getGlobalEpochW BucketEpochType
  | incGlobalEpoch
  | persistGlobalEpoch
  | setEpochLock bool

  | addFailure BucketEpochType
  | persistFailureList
  | ssFail ‹BucketEpochType × bool›

  | getTIDTransaction ‹ThreadID × BucketEpochType›

  | pickFreeTID ThreadID

  | doRead ‹ThreadID × KeyType × ValType›
  | doUpdate ‹ThreadID × KeyType × ValType›
  | doUpdateFull ThreadID
  | persist
  | getUsedThreads ‹ThreadID set›

 


section ‹Auxiliaries: Traces and Hiding in the Traces Model›

text‹FDR checks trace assertions in the traces model, where hiding is just the projection of
traces; divergence is irrelevant there. ‹traces_hiding› captures this notion of hiding.›

lemma replicate_setinterleaves: 
  ‹x ∈ S ⟹ replicate n x setinterleaves ((replicate n x, replicate n x), S)›
  by (induct n) auto

lemma replicate_strict_mono: ‹strict_mono (λi. replicate i x)›
proof (rule strict_monoI)
  fix i j :: nat assume ‹i < j›
  hence ‹replicate j x = replicate i x @ replicate (j - i) x›
    by (simp add: replicate_add[symmetric])
  moreover from ‹i < j› have ‹replicate i x ≠ replicate j x›
    by (metis length_replicate less_irrefl_nat)
  ultimately show ‹replicate i x < replicate j x›
    by (auto simp: less_list_def less_eq_list_def prefix_def)
qed



(*
lemma T_write0I: ‹s ∈ 𝒯 Proc ⟹ ev a # s ∈ 𝒯 (a → Proc)› by (simp add: T_write0)

lemma T_writeI: ‹s ∈ 𝒯 Proc ⟹ ev (c a) # s ∈ 𝒯 (c!a → Proc)› by (simp add: T_write)
lemma T_readI: ‹inj_on c A ⟹ x ∈ A ⟹ s ∈ 𝒯 (Qf x) ⟹ ev (c x) # s ∈ 𝒯 (read c A Qf)›
  by (auto simp: T_read inv_into_f_f)
lemma T_DetI1: ‹s ∈ 𝒯 Proc1 ⟹ s ∈ 𝒯 (Proc1 □ Proc2)› by (simp add: T_Det)
lemma T_DetI2: ‹s ∈ 𝒯 Proc2 ⟹ s ∈ 𝒯 (Proc1 □ Proc2)› by (simp add: T_Det)
lemma T_ThrowI1: ‹t ∈ 𝒯 Proc ⟹ set t ∩ ev ` A = {} ⟹ t ∈ 𝒯 (Proc Θ a ∈ A. Qf a)›
  by (simp add: T_Throw)
lemma T_ThrowI2: ‹t1 @ [ev a] ∈ 𝒯 Proc ⟹ set t1 ∩ ev ` A = {} ⟹ a ∈ A ⟹ t2 ∈ 𝒯 (Qf a)
                  ⟹ t1 @ ev a # t2 ∈ 𝒯 (Proc Θ a ∈ A. Qf a)›
  unfolding T_Throw by blast *)
lemma T_SyncI_right: ‹u ∈ 𝒯 Proc2 ⟹ ∀x∈set u. x ∉ range tick ∪ ev ` S ⟹ u ∈ 𝒯 (Proc1 ⟦S⟧ Proc2)›
  by (rule T_SyncI[OF Nil_elem_T], assumption, rule emptyLeftSelf) blast
lemma T_SyncI_left: ‹t ∈ 𝒯 Proc1 ⟹ ∀x∈set t. x ∉ range tick ∪ ev ` S ⟹ t ∈ 𝒯 (Proc1 ⟦S⟧ Proc2)›
  by (metis Sync_commute T_SyncI_right)


lemma T_GlobalDetI: ‹x ∈ A ⟹ s ∈ 𝒯 (Pf x) ⟹ s ∈ 𝒯 (□x ∈ A. Pf x)›
  by (auto simp: T_GlobalDet')


locale Dali =
  fixes MaxNIds MaxKeys MaxcPtr MaxVal MaxTid MaxEpoch :: nat
  assumes MaxcPtr_ge_2 : ‹2 ≤ MaxcPtr›
    ― ‹at least three pointers (active, in-flight, committed)›
begin

definition NodeID :: ‹NodeIDType set›
  where ‹NodeID = N ` {0 .. MaxNIds}›

definition Key :: ‹KeyType set›
  where ‹Key = K ` {0 .. MaxKeys}›

definition Val :: ‹ValType set›
  where ‹Val = V ` {0 .. MaxVal}›

definition Pointer :: ‹Pointers set›
  where ‹Pointer = P ` {0 .. MaxcPtr}›

definition ThreadIDs :: ‹ThreadID set›
  where ‹ThreadIDs = Th ` {0 .. MaxTid}›

definition BucketEpochs :: ‹BucketEpochType set›
  where ‹BucketEpochs ≡ BE ` {0 .. MaxEpoch}›

lemma NodeID_nonempty[simp]: ‹NodeID ≠ {}›
  and Null_notin_NodeID[simp]: ‹Null ∉ NodeID›
  and finite_NodeID[simp]: ‹finite NodeID›
  and finite_Key[simp]: ‹finite Key›
  and finite_Val[simp]: ‹finite Val›
  and finite_Pointer[simp]: ‹finite Pointer›
  and finite_ThreadIDs[simp]: ‹finite ThreadIDs›
  and finite_BucketEpochs[simp]: ‹finite BucketEpochs›
  by (auto simp: NodeID_def Key_def Val_def Pointer_def ThreadIDs_def BucketEpochs_def)

lemma NodeID_iff: ‹x ∈ NodeID ⟷ (∃i ≤ MaxNIds. x = N i)›
  and ThreadIDs_iff: ‹t ∈ ThreadIDs ⟷ (∃i ≤ MaxTid. t = Th i)›
  by (auto simp: NodeID_def ThreadIDs_def)

text‹Epochs are counted cyclically modulo ‹MaxEpoch + 1›:›

fun epochToInt :: ‹BucketEpochType ⇒ int› where
  ‹epochToInt (BE n) = int n›

fun prevEpoch :: ‹BucketEpochType ⇒ BucketEpochType› where
  ‹prevEpoch (BE n) = BE ((n + MaxEpoch) mod Suc MaxEpoch)›

fun nextEpoch :: ‹BucketEpochType ⇒ BucketEpochType› where
  ‹nextEpoch (BE n) = BE (Suc n mod Suc MaxEpoch)›

fun intToEpoch :: ‹int ⇒ BucketEpochType› where
  ‹intToEpoch x = (if 0 ≤ x ∧ x ≤ int MaxEpoch then BE (nat x) else BE MaxEpoch)›

text‹The first pointer that is neither the active nor the committed one:›

definition freePointer :: ‹Pointers ⇒ Pointers ⇒ Pointers›
  where ‹freePointer a c ≡ P (LEAST i. P i ≠ a ∧ P i ≠ c)›


(* concrete.csp*)

Fixrec [RS, HOLCF] NodeHandler :: ‹NodeIDType ⇒ KeyType ⇒ ValType ⇒ NodeIDType ⇒ bool ⇒ channels process›
  and InitNode :: ‹NodeIDType ⇒ channels process›
  where NodeHandler_rec [simp del]: ‹NodeHandler me k v nxt pers =
       (getKey!(me,k) → NodeHandler me k v nxt pers)
   □   (getVal!(me,v) → NodeHandler me k v nxt pers)
   □   (getNext!(me,nxt) → NodeHandler me k v nxt pers)
   □   (setNext?(m,n)|(m = me ∧ n ∈ NodeID) → NodeHandler me k v n pers)
   □   (persistNode!me → NodeHandler me k v nxt True)
   □   (crash →(if pers
                 then NodeHandler me k v nxt pers
                 else InitNode me))›
  | InitNode_rec [simp del]: ‹InitNode me =
      (initNode?(n,k,v)|(n = me) → NodeHandler me k v Null False)
    □ (crash → InitNode me)›


definition alphaNode :: ‹NodeIDType ⇒ channels set›
  where ‹alphaNode me ≡
   {x. ∃k v. x = initNode (me,k,v)}
 ∪ {x. ∃v. x = getVal (me,v)}
 ∪ {x. ∃k. x = getKey (me,k)}
 ∪ {x. ∃n. x = getNext (me,n)}
 ∪ {x. ∃n. x = setNext (me,n)}
 ∪ {noFreeNode}
 ∪ {persistNode me}
 ∪ {crash}›

definition AllNodes :: ‹channels process›
  where ‹AllNodes ≡ ||| n ∈# mset_set NodeID. InitNode n›

definition nodeSyncSet :: ‹channels set›
  where ‹nodeSyncSet ≡ {x. ∃n∈NodeID. ∃k v. x = initNode (n,k,v)}
    ∪ {x. ∃n∈NodeID. ∃k. x = getKey (n,k)}
    ∪ {x. ∃n∈NodeID. ∃v. x = getVal (n,v)}
    ∪ {x. ∃n∈NodeID. ∃nxt. x = getNext (n,nxt)}
    ∪ {x. ∃n∈NodeID. ∃nxt. x = setNext (n,nxt)}
    ∪ {x. ∃n∈NodeID. x = persistNode n}
    ∪ {noFreeNode}
    ∪ {crash}›

definition nodeSyncSeti :: ‹channels set›
  where ‹nodeSyncSeti ≡ {x. ∃n∈NodeID. ∃k v. x = initNode (n,k,v)}
    ∪ {x. ∃n∈NodeID. ∃k. x = getKey (n,k)}
    ∪ {x. ∃n∈NodeID. ∃v. x = getVal (n,v)}
    ∪ {x. ∃n∈NodeID. ∃nxt. x = getNext (n,nxt)}
    ∪ {x. ∃n∈NodeID. ∃nxt. x = setNext (n,nxt)}
    ∪ {x. ∃n∈NodeID. x = persistNode n}
    ∪ {noFreeNode}›


Fixrec [RS, HOLCF] PointerHandler :: ‹Pointers ⇒ NodeIDType ⇒ channels process›
  where PointerHandler_rec [simp del]: ‹PointerHandler me node = 
        (setPointerNode?(p,n)|(p = me) → PointerHandler me n)
     □  (getPointerNode!(me,node) → PointerHandler me node)›

definition Pointers :: ‹channels process›
  where ‹Pointers ≡ ||| p ∈# mset_set Pointer. PointerHandler p Null›

definition pointerSyncSet :: ‹channels set›
  where ‹pointerSyncSet ≡ {x. ∃p n. x = setPointerNode (p,n)}
 ∪ {x. ∃p n. x = getPointerNode (p,n)}›

definition maxEpoch :: BucketEpochType
  where ‹maxEpoch ≡ BE MaxEpoch›


Fixrec [RS, HOLCF] BucketVarHandler :: ‹Pointers ⇒ Pointers ⇒ Pointers ⇒ BucketEpochType ⇒ channels process›
  where BucketVarHandler_rec [simp del]: ‹BucketVarHandler a f c ss = (getBucketEpoch!ss → BucketVarHandler a f c ss)
     □  (getActiveNode!a → BucketVarHandler a f c ss)
     □  (getFlightNode!f → BucketVarHandler a f c ss)
     □  (getCommittedNode!c → BucketVarHandler a f c ss)
     □  (setStat?(newA,newF,newC,newSS) → BucketVarHandler newA newF newC newSS)›


definition InitBucket :: ‹channels process›
  where ‹InitBucket ≡ BucketVarHandler P0 Bot P2 BE0›

definition alphaBucket :: ‹channels set›
  where ‹alphaBucket ≡ {x. ∃p. x = getActiveNode p}
∪ {x. ∃p. x = getFlightNode p}
∪ {x. ∃p. x = getCommittedNode p}
∪ {x. ∃e. x = getBucketEpoch e}
∪ {x. ∃a f c e. x = setStat (a,f,c,e)}›


definition alphaLock :: ‹channels set›
  where ‹alphaLock ≡ {lock, unlock}›


Fixrec [RS, HOLCF] BucketLockHandler :: ‹channels process›
  where BucketLockHandler_rec [simp del]: ‹BucketLockHandler = (lock → unlock → BucketLockHandler)›

Fixrec [RS, HOLCF] FailureListHandler :: ‹BucketEpochType set ⇒ BucketEpochType set ⇒ channels process›
  where FailureListHandler_rec [simp del]: ‹FailureListHandler fs pfs = (addFailure?f
            → FailureListHandler (insert f fs) pfs)
    □  (persistFailureList → FailureListHandler fs fs)
    □  (ssFail?(f,b)|(b = (f ∈ pfs)) → FailureListHandler fs pfs)
    □  (crash → FailureListHandler pfs pfs)›


definition InitFailureList :: ‹channels process›
  where ‹InitFailureList ≡ FailureListHandler {} {}›


definition alphaFailureList :: ‹channels set›
  where ‹alphaFailureList ≡
      {x. ∃f. x = addFailure f}
    ∪ {persistFailureList}
    ∪ {x. ∃f b. x = ssFail (f,b)}›


Fixrec [RS, HOLCF] GlobalEpochHandler :: ‹BucketEpochType ⇒ BucketEpochType ⇒ bool ⇒ channels process›
  where GlobalEpochHandler_rec [simp del]: ‹GlobalEpochHandler e pe lt =
       ((if lt
        then (getGlobalEpoch?(t,v)|((v = pe)) → GlobalEpochHandler e pe lt)
        else (getGlobalEpoch?(t,v)|((v = e)) → GlobalEpochHandler e pe lt)))
   □  (getGlobalEpochW!e → GlobalEpochHandler e pe lt)
   □  (incGlobalEpoch →
          (if e = maxEpoch
           then Skip
           else GlobalEpochHandler (nextEpoch e) pe lt))
   □  (persistGlobalEpoch → GlobalEpochHandler e e lt)
   □  (crash → GlobalEpochHandler pe pe False)
   □  (setEpochLock?l → GlobalEpochHandler e pe l)›

definition InitGlobalEpoch :: ‹channels process›
  where ‹InitGlobalEpoch ≡ GlobalEpochHandler BE0 BE0 False›

definition alphaGlobalEpoch :: ‹channels set›
  where ‹alphaGlobalEpoch ≡
      {x. ∃t e. x = getGlobalEpoch (t,e)}
    ∪ {x. ∃e. x = getGlobalEpochW e}
    ∪ {incGlobalEpoch}
    ∪ {persistGlobalEpoch}
    ∪ {x. ∃l. x = setEpochLock l}
    ∪ {crash}›



Fixrec [RS, HOLCF] GlobalArrayHandler :: ‹(ThreadID ⇒ BucketEpochType) ⇒ channels process›
  where GlobalArrayHandler_rec [simp del]: ‹GlobalArrayHandler tm =
       (getTIDTransaction?(t,e)|(t ∈ ThreadIDs ∧ e = tm t) → GlobalArrayHandler tm)
   □   (getGlobalEpoch?(t,e) → GlobalArrayHandler (tm(t := e)))
   □   (resRead?(t,v) → GlobalArrayHandler (tm(t := BE0)))
   □   (resUpdate?t → GlobalArrayHandler (tm(t := BE0)))
   □   (resUpdateFull?t → GlobalArrayHandler (tm(t := BE0)))›


definition initMap :: ‹ThreadID ⇒ BucketEpochType›
  where ‹initMap ≡ (λ_. BE0)›

definition InitGlobalArray :: ‹channels process›
  where ‹InitGlobalArray ≡ GlobalArrayHandler initMap›

definition transSyncSet :: ‹channels set›
  where ‹transSyncSet ≡
      {x. ∃t e. x = getTIDTransaction (t,e)}
    ∪ {x. ∃t e. x = getGlobalEpoch (t,e)}
    ∪ {x. ∃t v. x = resRead (t,v)}
    ∪ {x. ∃t. x = resUpdate t}
    ∪ {x. ∃t. x = resUpdateFull t}›

definition alphaTransArray :: ‹channels set›
  where ‹alphaTransArray ≡ {x. ∃t e. x = getTIDTransaction (t,e)}›


Fixrec [RS, HOLCF] FreeTIDsHandler :: ‹ThreadID set ⇒ channels process›
  where FreeTIDsHandler_rec [simp del]: ‹FreeTIDsHandler F =
       (pickFreeTID?t|(t ∈ F) → FreeTIDsHandler (F - {t}))›

definition FreeTIDs :: ‹channels process›
  where ‹FreeTIDs ≡ FreeTIDsHandler ThreadIDs›

definition SyncSetFreeTIDs :: ‹channels set›
  where ‹SyncSetFreeTIDs ≡ {x. ∃t. x = pickFreeTID t}›


section‹ APPLICATION THREAD Methods ›

text‹The application thread loops: after a response, it continues as ‹Thread›
(as in ‹concrete.csp›); the thread methods form one system of mutually recursive processes.›

Fixrec [RS, HOLCF] ReadSearch :: ‹ThreadID ⇒ KeyType ⇒ NodeIDType ⇒ channels process›
  and Read :: ‹ThreadID ⇒ KeyType ⇒ channels process›
  and SetStat :: ‹ThreadID ⇒ BucketEpochType ⇒ Pointers ⇒ Pointers ⇒ Pointers ⇒ channels process›
  and Lookup :: ‹ThreadID ⇒ BucketEpochType ⇒ bool ⇒ bool ⇒ NodeIDType ⇒ Pointers ⇒ BucketEpochType ⇒ channels process›
  and Update' :: ‹ThreadID ⇒ NodeIDType ⇒ BucketEpochType ⇒ channels process›
  and Update :: ‹ThreadID ⇒ KeyType ⇒ ValType ⇒ channels process›
  and Thread :: ‹ThreadID ⇒ channels process›
  where ReadSearch_rec [simp del]: ‹ReadSearch me key validHead = 
        (if validHead = Null 
        then resRead!(me,TNull) →  unlock → Thread me
        else (getKey?(n,k)|(n = validHead ∧ k ∈ Key)
              → (if key = k
                 then (getVal?(n,value)|(n = validHead) → resRead!(me,value)
                       → unlock → Thread me)
                 else (getNext?(n,next)|(n = validHead)  → ReadSearch me key next))))›
  | Read_rec [simp del]: ‹Read me key = lock
     →  getGlobalEpoch?(t,e)|(t = me)  →  getBucketEpoch?SS
     →  (if SS = BE0 
         then ReadSearch me key Null
         else ssFail?(f,currFail)|(f = SS)
     →  (if ¬ currFail 
         then (getActiveNode?headNode → getPointerNode?(p,h)|(p = headNode)
               → ReadSearch me key h)
         else ssFail?(f2,prevFail)|(f2 = prevEpoch SS) → getFlightNode?headNodef
      → (if ((¬ prevFail) ∧ (headNodef ≠ Bot)) 
         then getPointerNode?(p,h)|(p = headNodef) → ReadSearch me key h
         else getCommittedNode?headNodec → getPointerNode?(p,h)|(p = headNodec)
              → ReadSearch me key h)))›
  | SetStat_rec [simp del]: ‹SetStat me epoch newA newF newC = setStat!(newA,newF,newC,epoch)
     →  resUpdate!me
     →  unlock
     →  Thread me›
  | Lookup_rec [simp del]: ‹Lookup me SS currFail prevFail newNode headNode epoch =
      getPointerNode?(p,h)|(p = headNode)
   →  setNext!(newNode,h)
   →  getActiveNode?oldA
   →  getFlightNode?oldF
   →  getCommittedNode?oldC
   → (if SS = epoch 
      then setPointerNode!(oldA,newNode) → SetStat me epoch oldA oldF oldC
      else if (SS = prevEpoch epoch ∧ (¬ currFail) ∧ (¬ prevFail) ∧ (oldF ≠ Bot)) 
      then setPointerNode!(oldC,newNode) → SetStat me epoch oldC oldA oldF
      else if (SS = prevEpoch epoch ∧ (¬ currFail) ∧ (oldF = Bot)) 
      then (setPointerNode!(freePointer oldA oldC,newNode)
            → SetStat me epoch (freePointer oldA oldC) oldA oldC)
      else if (SS = prevEpoch epoch ∧ (¬ currFail)) 
      then setPointerNode!(oldF,newNode) → SetStat me epoch oldF oldA oldC
      else if (SS = prevEpoch epoch) 
      then setPointerNode!(oldA,newNode) → SetStat me epoch oldA Bot oldC
      else if (epochToInt SS < epochToInt (prevEpoch epoch) ∧ (¬ currFail)) 
      then setPointerNode!(oldC,newNode) → SetStat me epoch oldC Bot oldA
      else if (epochToInt SS < epochToInt (prevEpoch epoch) ∧ currFail ∧ (¬ prevFail) ∧ (oldF ≠ Bot)) 
      then setPointerNode!(oldA,newNode) → SetStat me epoch oldA Bot oldF
      else setPointerNode!(oldA,newNode) → SetStat me epoch oldA Bot oldC)›
  | Update'_rec [simp del]: ‹Update' me node gepoch = getBucketEpoch?SS →
        (if SS = BE0 
        then getActiveNode?headNode →  Lookup me SS False False node headNode gepoch
        else ssFail?(f,currFail)|(f = SS) →  ssFail?(f2,prevFail)|(f2 = prevEpoch SS)
        → (if ¬ currFail 
           then getActiveNode?headNode →  Lookup me SS currFail prevFail node headNode gepoch
           else getFlightNode?headNodef
           → (if ((¬ prevFail) ∧ (headNodef ≠ Bot)) 
              then Lookup me SS currFail prevFail node headNodef gepoch
              else getCommittedNode?headNodec 
               →  Lookup me SS currFail prevFail node headNodec gepoch)))›
  | Update_rec [simp del]: ‹Update me key val = lock →  getGlobalEpoch?(t,e)|(t = me)
     → ((initNode?(node,k,v)|(k = key ∧ v = val) → Update' me node e)
       □ (noFreeNode → resUpdateFull!me → unlock → Thread me))›
  | Thread_rec [simp del]: ‹Thread me =(invRead?(t,k)|(t = me) → Read me k)
       □  (invUpdate?(t,k,v)|(t = me) → Update me k v)›


section‹ WORKER THREAD METHODS ›

Fixrec [RS, HOLCF] WaitOnTransactions :: ‹ThreadID set ⇒ BucketEpochType ⇒ channels process›
  where WaitOnTransactions_rec [simp del]: ‹WaitOnTransactions Threads e =
      (if Threads = {}
       then Skip
       else getTIDTransaction?(t,v)|(t ∈ Threads) →
                (if v ≠ e
                 then WaitOnTransactions (Threads - {t}) e
                 else WaitOnTransactions Threads e))›

Fixrec [RS, HOLCF] WriteBackLoop :: ‹NodeIDType ⇒ NodeIDType ⇒ channels process›
  where WriteBackLoop_rec [simp del]: ‹WriteBackLoop cnode n =
      (if n = Null
       then Skip
       else persistNode!n
         → getNext?(x,n2)|(x = n)
         → (if n2 = cnode
            then Skip
            else WriteBackLoop cnode n2))›

Fixrec [RS, HOLCF] WriteBack :: ‹channels process›
  where WriteBack_rec [simp del]: ‹WriteBack =
      getCommittedNode?cnode
   →  getActiveNode?n
   →  getPointerNode?(p1,c)|(p1 = cnode)
   →  getPointerNode?(p2,a)|(p2 = n)
   →  WriteBackLoop c a›

Fixrec [RS, HOLCF] WorkerThread :: ‹channels process›
  where WorkerThread_rec [simp del]: ‹WorkerThread =
      getGlobalEpochW?e
   →  setEpochLock!True
   →  incGlobalEpoch
   →  persistGlobalEpoch
   →  setEpochLock!False
   → ((WaitOnTransactions ThreadIDs e)
        ; WriteBack
        ; WorkerThread)›

definition ApplicationThreads :: ‹channels process›
  where ‹ApplicationThreads ≡ (pickFreeTID?t1 → Thread t1) ||| (pickFreeTID?t2 → Thread t2)›

definition AllThreads :: ‹channels process›
  where ‹AllThreads ≡ ApplicationThreads ||| WorkerThread›

definition Recovery :: ‹channels process›
  where ‹Recovery ≡ getGlobalEpochW?F
   →  addFailure!F
   →  addFailure!(prevEpoch F)
   →  persistFailureList
   →  setEpochLock!True
   →  incGlobalEpoch
   →  persistGlobalEpoch
   →  setEpochLock!False
   →  Skip›

definition alphaCrash :: ‹channels set›
  where ‹alphaCrash ≡ {crash}›


definition alphaGlobal :: ‹channels set›
  where ‹alphaGlobal ≡ alphaFailureList ∪ alphaGlobalEpoch›


definition alphaG :: ‹channels set›
  where ‹alphaG ≡  alphaGlobal
    ∪ nodeSyncSet
    ∪ alphaBucket
    ∪ SyncSetFreeTIDs
    ∪ alphaCrash
    ∪ pointerSyncSet›

definition GlobalProcesses :: ‹channels process›
  where ‹GlobalProcesses ≡ (((AllNodes ⟦alphaCrash⟧ InitGlobalEpoch)
        ⟦alphaCrash⟧
        InitFailureList)
      ||| InitBucket
      ||| FreeTIDs
      ||| Pointers)›

definition DaliArray :: ‹channels process›
  where ‹DaliArray ≡ ((AllThreads ⟦transSyncSet⟧ InitGlobalArray)
       \ alphaTransArray)›

definition DaliMethods :: ‹channels process›
  where ‹DaliMethods ≡ ((DaliArray ⟦alphaLock⟧ BucketLockHandler)
       \ alphaLock)›

definition internalEvents :: ‹channels set›
  where ‹internalEvents ≡ alphaGlobal
    ∪ nodeSyncSeti
    ∪ alphaBucket
    ∪ SyncSetFreeTIDs
    ∪ pointerSyncSet›

definition DaliL :: ‹channels process›
  where ‹DaliL ≡ ((DaliMethods ⟦alphaG⟧ GlobalProcesses) \ internalEvents)›

definition DaliRecovery :: ‹channels process›
  where ‹DaliRecovery ≡ Recovery ; DaliMethods›

Fixrec [RS, HOLCF] DaliCrash :: ‹channels process›
  and DaliCrashR :: ‹channels process›
  where DaliCrash_rec [simp del]: ‹DaliCrash =
       ((DaliMethods ||| (crash → Skip))
          Θ a ∈ alphaCrash. DaliCrashR)›
 | DaliCrashR_rec [simp del]:
   ‹DaliCrashR =
       ((DaliRecovery ||| (crash → Skip))
          Θ a ∈ alphaCrash. DaliCrashR)›

definition Dali :: ‹channels process›
  where ‹Dali ≡ ((DaliCrash ⟦alphaG⟧ GlobalProcesses) \ internalEvents)›

definition DaliE :: ‹channels process›
  where ‹DaliE ≡ Dali \ {x. ∃t k. x = invRead (t,k)} \ {x. ∃t k v. x = invUpdate (t,k,v)}›

(* spec.csp*)

section‹ABSTRACT MAP SPECIFICATION›

definition maxNodes :: int
  where ‹maxNodes ≡ int (card NodeID)›


type_synonym MapMem = ‹KeyType ⇒ ValType›

type_synonym MapState = ‹MapMem × MapMem × int × int›

definition emptyMap :: MapMem
  where ‹emptyMap ≡ (λ_. TNull)›

definition mapLookupNull :: ‹MapMem ⇒ KeyType ⇒ ValType›
  where ‹mapLookupNull m k ≡ m k›

definition mapUpdate :: ‹MapMem ⇒ KeyType ⇒ ValType ⇒ MapMem›
  where ‹mapUpdate m k v ≡ m(k := v)›


(*vmem = volatile memory
  pmem = persisted memory
  c    = nodes that may have been used
  pc   = persisted node count

  crash -> nondeterministically rollback to any x in {pc..c}
*)

Fixrec [RS, HOLCF] MapOps :: ‹MapState ⇒ channels process›
  where MapOps_rec [simp del]: ‹MapOps (vmem, pmem, c, pmemc) = 
        ((if vmem = emptyMap
          then (doRead?(t,k,v)|(v = TNull) → MapOps (vmem, pmem, c, pmemc))
          else (doRead?(t,k,v)|(v = mapLookupNull vmem k) → MapOps (vmem, pmem, c, pmemc))))
    □  ((if c < maxNodes 
         then (doUpdate?(t,k,v) → MapOps (mapUpdate vmem k v, pmem, c + 1, pmemc))
         else (doUpdateFull?t → MapOps (vmem, pmem, c, pmemc))))
    □  (crash → (□x ∈ {pmemc..c}. MapOps (pmem, pmem, x, x)))
    □  (persist → MapOps (vmem, vmem, c, c))›

definition MapSpec0 :: ‹channels process›
  where ‹MapSpec0 ≡ MapOps (emptyMap, emptyMap, 0, 0)›

definition MapSpec :: ‹channels process›
  where ‹MapSpec ≡ MapSpec0›

Fixrec [RS, HOLCF] Persist :: ‹channels process›
  where Persist_rec : ‹Persist = persist → Persist›

Fixrec [RS, HOLCF] AllThreadHandler :: ‹ThreadID set ⇒ channels process›
  where AllThreadHandler_rec : ‹AllThreadHandler usedThreads =
                                   (invRead?(t,k) → AllThreadHandler (insert t usedThreads))
                                □  (invUpdate?(t,k,v) → AllThreadHandler (insert t usedThreads))
                                □  (getUsedThreads!usedThreads → AllThreadHandler usedThreads)›

Fixrec [RS, HOLCF] MapThread :: ‹ThreadID ⇒ channels process›
  where MapThread_rec : ‹MapThread me =   (invRead?(t,key)|(t = me)
                                            → doRead?(t2,k2,value)|(t2 = me ∧ k2 = key)
                                               → resRead!(me,value) → MapThread me)
                                       □ (invUpdate?(t,key,value)|(t = me)
                                            → ((doUpdateFull!me
                                                  → resUpdateFull!me → MapThread me)
                                                □ (doUpdate!(me,key,value)
                                                      → resUpdate!me
                                                           → MapThread me)))›

Fixrec [RS, HOLCF] AllMapThreads :: ‹channels process›
  where AllMapThreads_rec : ‹AllMapThreads = getUsedThreads?ts
                                             → (||| t ∈# mset_set (ThreadIDs - ts). MapThread t)›

definition specSyncSet :: ‹channels set›
  where ‹specSyncSet   ≡ {x. ∃t k v. x = doUpdate (t,k,v)}
                       ∪ {x. ∃t k v. x = doRead (t,k,v)}
                       ∪ {x. ∃t. x = doUpdateFull t}
                       ∪ {crash}
                       ∪ {persist}›

definition internal   :: ‹channels set›
  where ‹internal      ≡ {x. ∃t k v. x = doUpdate (t,k,v)}
                       ∪ {x. ∃t k v. x = doRead (t,k,v)}
                       ∪ {x. ∃t. x = doUpdateFull t}
                       ∪ {persist}›

definition threadSyncSet :: ‹channels set›
  where ‹threadSyncSet ≡ {x. ∃t k. x = invRead (t,k)}
                       ∪ {x. ∃t k v. x = invUpdate (t,k,v)}
                       ∪ {x. ∃ts. x = getUsedThreads ts}›

definition internalSpec :: ‹channels set›
  where ‹internalSpec ≡ {x. ∃t k v. x = doUpdate (t,k,v)}
                      ∪ {x. ∃t k v. x = doRead (t,k,v)}
                      ∪ {x. ∃t. x = doUpdateFull t}
                      ∪ {persist}›

definition alphaThread :: ‹channels set›
  where ‹alphaThread ≡ {x. ∃ts. x = getUsedThreads ts}›

definition SpecThreadsL :: ‹channels process›
  where ‹SpecThreadsL ≡ ((AllMapThreads ⟦threadSyncSet⟧ AllThreadHandler {}) \ alphaThread)›

definition SpecL :: ‹channels process›
  where ‹SpecL ≡ ((SpecThreadsL ⟦specSyncSet⟧ MapSpec) \ internalSpec)›


Fixrec [RS, HOLCF] Spec_with_crash :: ‹channels process›
  where Spec_with_crash_rec : ‹Spec_with_crash = ((AllMapThreads ||| (crash → Skip))
                                                 Θ a ∈ {crash}. Spec_with_crash)›

definition SpecThreads :: ‹channels process›
  where ‹SpecThreads ≡ (((Spec_with_crash ⟦threadSyncSet⟧ AllThreadHandler {}) \ alphaThread)
                       ||| Persist)›

definition Spec :: ‹channels process›
  where ‹Spec ≡ ((SpecThreads ⟦specSyncSet⟧ MapSpec) \ internalSpec)›
text‹Note that the event term‹persist› is in term‹internalSpec›, and since
 term‹Persist = persist → Persist› can happen at any time, the hiding operator will
thus produce a term‹⊥› for this trace. Thus, there is a divergence in this model 
(which was already present in the original version by Edmonds, Derrick, et al). 
This limits the current model to trace - and failure analysis. An alternative would 
have been to exclude term‹persist› from the internals, but this has other consequences.›


text‹Formally: an infinite run of hidden const‹persist› events makes const‹Spec› divergent
from the start, i.e., equal to ‹⊥›:›

lemma persist_Persist: ‹replicate n (ev persist) ∈ 𝒯 Persist›
  by (induct n) (simp, subst Persist_rec, simp add: T_write0)

lemma persist_MapOps: ‹replicate n (ev persist) ∈ 𝒯 (MapOps (m, m, c, c))›
proof (induct n arbitrary: m c)
  case 0 show ?case by simp
next
  case (Suc n) show ?case
    by (subst MapOps_rec, unfold T_Det, rule UnI2) (simp add: T_write0 Suc)
qed

lemma persist_SpecThreads: ‹replicate n (ev persist) ∈ 𝒯 SpecThreads›
  unfolding SpecThreads_def 
  by (rule T_SyncI[OF Nil_elem_T persist_Persist], rule emptyLeftSelf) auto

lemma persist_SpecU: ‹replicate n (ev persist) ∈ 𝒯 (SpecThreads ⟦specSyncSet⟧ MapSpec)›
proof (unfold MapSpec_def MapSpec0_def, rule T_SyncI)
  show ‹replicate n (ev persist) ∈ 𝒯 SpecThreads› by (fact persist_SpecThreads)
  show ‹replicate n (ev persist) ∈ 𝒯 (MapOps (emptyMap, emptyMap, 0, 0))› by (fact persist_MapOps)
  show ‹replicate n (ev persist) setinterleaves 
          ((replicate n (ev persist), replicate n (ev persist)), range tick ∪ ev ` specSyncSet)›
    by (rule replicate_setinterleaves) (simp add: specSyncSet_def)
qed

lemma Spec_is_BOT: ‹Spec = ⊥›
proof -
  let ?f = ‹λi. replicate i (ev persist)›
  have run : ‹isInfHiddenRun ?f (SpecThreads ⟦specSyncSet⟧ MapSpec) internalSpec›
    by (simp add: replicate_strict_mono persist_SpecU internalSpec_def)
  have start : ‹[] ∈ range ?f› by (metis range_eqI replicate_0)
  have hide : ‹[] = trace_hide [] (ev ` internalSpec) @ []› by simp
  have ‹[] ∈ 𝒟 Spec›
    unfolding Spec_def D_Hiding mem_Collect_eq
    using run start hide ftF_Nil tF_Nil by blast
  thus ‹Spec = ⊥› by (simp add: BOT_iff_Nil_D)
qed

definition alphaEndEvents :: ‹channels set›
  where ‹alphaEndEvents ≡    {x. ∃t v. x = resRead (t,v)}
                           ∪ {x. ∃t. x = resUpdate t}
                           ∪ {x. ∃t. x = resUpdateFull t}›


definition SpecE :: ‹channels process›
  where ‹SpecE ≡ Spec \ alphaEndEvents›


end (* locale Dali *)

section‹The General Dali Model Instantiated›

text‹The original, finite model of the article is the instance with three nodes and pointers,
two keys, values and threads, and three epochs:›

locale Dali_orig = Dali 2 1 2 1 1 2
  ― ‹the instance as a context for tests: inside, ‹Spec›, ‹Dali›, ‹NodeID›, ... 
     denote the processes and data of this instance›

text‹The instance is consistent:›
interpretation orig : Dali_orig by standard simp

context Dali_orig begin

lemma ‹NodeID = {N0, N1, N2}› and ‹ThreadIDs = {T0, T1}›
  unfolding set_eq_iff NodeID_iff ThreadIDs_iff
  by (auto simp: numeral_2_eq_2 le_Suc_eq)


subsection ‹Component Traces›

lemma ThreadIDs_orig: ‹ThreadIDs = {T0, T1}›
  unfolding set_eq_iff ThreadIDs_iff by (auto simp: le_Suc_eq)

lemma NodeID_orig: ‹NodeID = {N0, N1, N2}›
  unfolding set_eq_iff NodeID_iff by (auto simp: numeral_2_eq_2 le_Suc_eq)

lemma maxNodes_orig: ‹maxNodes = 3› by (simp add: maxNodes_def NodeID_orig)

lemma MapThread_update_trace:
  ‹[ev (invUpdate (T0,K0,V0)), ev (doUpdate (T0,K0,V0)), ev (resUpdate T0)] ∈ 𝒯 (MapThread T0)›
  apply (subst MapThread_rec, rule T_DetI2, rule T_readI[where x = ‹(T0,K0,V0)›])
    apply (simp_all add: inj_on_def)
  by (rule T_DetI2, rule T_writeI, rule T_writeI, rule Nil_elem_T)

lemma MapThread_read_trace:
  ‹[ev (invRead (T1,K0)), ev (doRead (T1,K0,V0)), ev (resRead (T1,V0))] ∈ 𝒯 (MapThread T1)›
  apply (subst MapThread_rec, rule T_DetI1, rule T_readI[where x = ‹(T1,K0)›])
    apply (simp_all add: inj_on_def)
  apply (rule T_readI)
    apply (simp_all add: inj_on_def)
  by (rule T_writeI, rule Nil_elem_T)

lemma AllMapThreads_trace1:
  ‹[ev (getUsedThreads {}), 
    ev (invUpdate (T0,K0,V0)), 
    ev (doUpdate (T0,K0,V0)), 
    ev (resUpdate T0)]
   ∈ 𝒯 AllMapThreads›
  apply (subst AllMapThreads_rec, rule T_readI[where x = ‹{}›])
    apply (simp_all add: inj_on_def ThreadIDs_orig[simplified])
  by (rule T_SyncI_left[OF MapThread_update_trace]) auto

lemma AllMapThreads_trace2:
  ‹[ev (getUsedThreads {T0}), 
    ev (invRead (T1,K0)), 
    ev (doRead (T1,K0,V0)), 
    ev (resRead (T1,V0))]
   ∈ 𝒯 AllMapThreads›
  apply (subst AllMapThreads_rec, rule T_readI[where x = ‹{T0}›])
    apply (simp_all add: inj_on_def ThreadIDs_orig[simplified] insert_Diff_if)
  using MapThread_read_trace by simp

lemma Spec_with_crash_trace:
  ‹[ev (getUsedThreads {}), ev (invUpdate (T0,K0,V0)), ev (doUpdate (T0,K0,V0)), ev (resUpdate T0)]
   @ ev crash #
   [ev (getUsedThreads {T0}), ev (invRead (T1,K0)), ev (doRead (T1,K0,V0)), ev (resRead (T1,V0))]
   ∈ 𝒯 Spec_with_crash›
proof (subst Spec_with_crash_rec, rule T_ThrowI2)
  show ‹[ev (getUsedThreads {}), ev (invUpdate (T0,K0,V0)), ev (doUpdate (T0,K0,V0)), ev (resUpdate T0)]
        @ [ev crash] ∈ 𝒯 (AllMapThreads ||| (crash → Skip))›
    by (rule T_SyncI[OF AllMapThreads_trace1 T_write0I[OF Nil_elem_T]]) auto
  show ‹[ev (getUsedThreads {T0}), ev (invRead (T1,K0)), ev (doRead (T1,K0,V0)), ev (resRead (T1,V0))]
        ∈ 𝒯 Spec_with_crash›
    by (subst Spec_with_crash_rec, rule T_ThrowI1, rule T_SyncI_left[OF AllMapThreads_trace2]) auto
qed auto

lemma AllThreadHandler_trace:
  ‹[ev (getUsedThreads {}), 
    ev (invUpdate (T0,K0,V0)), 
    ev (getUsedThreads {T0}), 
    ev (invRead (T1,K0))]
   ∈ 𝒯 (AllThreadHandler {})›
  apply (subst AllThreadHandler_rec, rule T_DetI2, rule T_writeI)
  apply (subst AllThreadHandler_rec, rule T_DetI1, rule T_DetI2)
  apply (rule T_readI, simp add: inj_on_def, simp, simp only: prod.case)
  apply (subst AllThreadHandler_rec, rule T_DetI2, rule T_writeI)
  apply (subst AllThreadHandler_rec, rule T_DetI1, rule T_DetI1)
  by (rule T_readI, simp add: inj_on_def, simp, rule Nil_elem_T)

lemma MapSpec_trace:
  ‹[ev (doUpdate (T0,K0,V0)), ev persist, ev crash, ev (doRead (T1,K0,V0))] ∈ 𝒯 MapSpec›
proof -
  have c0: ‹(0::int) < maxNodes› by (simp add: maxNodes_orig)
  have m1: ‹mapUpdate emptyMap K0 V0 ≠ emptyMap›
    by (auto simp: mapUpdate_def emptyMap_def fun_eq_iff)
  show ?thesis
    unfolding MapSpec_def MapSpec0_def
    apply (subst MapOps_rec, rule T_DetI1, rule T_DetI1, rule T_DetI2)
    apply (simp only: if_P[OF c0])
    apply (rule T_readI, simp add: inj_on_def, simp, simp only: prod.case)
    apply (subst MapOps_rec, rule T_DetI2, rule T_write0I)
    apply (subst MapOps_rec, rule T_DetI1, rule T_DetI2, rule T_write0I)
    apply (rule T_GlobalDetI[where x = ‹0 + 1›], simp)
    apply (subst MapOps_rec, rule T_DetI1, rule T_DetI1, rule T_DetI1)
    apply (simp only: if_not_P[OF m1])
    by (rule T_readI, simp add: inj_on_def, 
        simp add: mapLookupNull_def mapUpdate_def, rule Nil_elem_T)
qed

lemma crash_Spec_with_crash: ‹[ev crash] ∈ 𝒯 Spec_with_crash›
  by (subst Spec_with_crash_rec, subst AllMapThreads_rec)
    (simp add: read_Sync_write0_indep Throw_Det Throw_write0 T_Det T_write0)


section‹Assertions› 

text‹ Following ‹assertions.csp› in the original text.›

lemma dali_trace_refinement: ‹Spec ⊑T Dali› oops

lemma daliL_trace_refinement: ‹SpecL ⊑T DaliL› oops

definition traces_hiding :: ‹('a, 'r) processptick ⇒ 'a set ⇒ ('a, 'r) traceptick set›
  where ‹traces_hiding Proc A ≡ {trace_hide t (ev ` A) |t. t ∈ 𝒯 Proc}›

lemma traces_hidingI: ‹t ∈ 𝒯 Proc ⟹ s = trace_hide t (ev ` A) ⟹ s ∈ traces_hiding Proc A›
  unfolding traces_hiding_def by blast

lemma spec_has_crash_trace:
  ‹[ev crash] ∈ traces_hiding (SpecThreads ⟦specSyncSet⟧ MapSpec) internalSpec›
proof (rule traces_hidingI)
  have ‹[ev crash] ∈ 𝒯 SpecThreads›
  proof (unfold SpecThreads_def, rule T_SyncI_left)
    have inner: ‹[ev crash] ∈ 𝒯 (Spec_with_crash ⟦threadSyncSet⟧ AllThreadHandler {})›
      by (rule T_SyncI_left[OF crash_Spec_with_crash]) (auto simp: threadSyncSet_def)
    have ‹trace_hide [ev crash] (ev ` alphaThread) = [ev crash]› by (auto simp: alphaThread_def)
    with mem_T_imp_mem_T_Hiding[OF inner, of alphaThread]
    show ‹[ev crash] ∈ 𝒯 ((Spec_with_crash ⟦threadSyncSet⟧ AllThreadHandler {}) \ alphaThread)›
      by metis
  qed auto
  moreover have ‹[ev crash] ∈ 𝒯 MapSpec›
    unfolding MapSpec_def MapSpec0_def
    by (subst MapOps_rec, rule T_DetI1, rule T_DetI2, rule T_write0I, rule Nil_elem_T)
  ultimately show ‹[ev crash] ∈ 𝒯 (SpecThreads ⟦specSyncSet⟧ MapSpec)›
    by (rule T_SyncI) (simp add: specSyncSet_def)
qed (auto simp: internalSpec_def)

lemma spec_trace_crash_read_value:
  ‹map ev [invUpdate (T0,K0,V0), resUpdate T0, crash, invRead (T1,K0), resRead (T1,V0)]
   ∈ traces_hiding (SpecThreads ⟦specSyncSet⟧ MapSpec) internalSpec›
proof (rule traces_hidingI)
  let ?tIn = ‹[ev (getUsedThreads {}), ev (invUpdate (T0,K0,V0)), ev (doUpdate (T0,K0,V0)),
               ev (resUpdate T0), ev crash, ev (getUsedThreads {T0}), ev (invRead (T1,K0)),
               ev (doRead (T1,K0,V0)), ev (resRead (T1,V0))]›
  let ?tX = ‹[ev (invUpdate (T0,K0,V0)), ev (doUpdate (T0,K0,V0)), ev (resUpdate T0), ev crash,
              ev (invRead (T1,K0)), ev (doRead (T1,K0,V0)), ev (resRead (T1,V0))]›
  let ?tST = ‹[ev (invUpdate (T0,K0,V0)), ev (doUpdate (T0,K0,V0)), ev (resUpdate T0), ev persist,
               ev crash, ev (invRead (T1,K0)), ev (doRead (T1,K0,V0)), ev (resRead (T1,V0))]›
  have inner: ‹?tIn ∈ 𝒯 (Spec_with_crash ⟦threadSyncSet⟧ AllThreadHandler {})›
    by (rule T_SyncI[OF Spec_with_crash_trace AllThreadHandler_trace]) (auto simp: threadSyncSet_def)
  have hide: ‹trace_hide ?tIn (ev ` alphaThread) = ?tX› by (auto simp: alphaThread_def)
  have X: ‹?tX ∈ 𝒯 ((Spec_with_crash ⟦threadSyncSet⟧ AllThreadHandler {}) \ alphaThread)›
    using mem_T_imp_mem_T_Hiding[OF inner, of alphaThread] hide by metis
  have persist: ‹[ev persist] ∈ 𝒯 Persist›
    by (subst Persist_rec, rule T_write0I, rule Nil_elem_T)
  have ST: ‹?tST ∈ 𝒯 SpecThreads›
    unfolding SpecThreads_def by (rule T_SyncI[OF X persist]) auto
  show ‹?tST ∈ 𝒯 (SpecThreads ⟦specSyncSet⟧ MapSpec)›
    by (rule T_SyncI[OF ST MapSpec_trace]) (auto simp: specSyncSet_def)
  show ‹map ev [invUpdate (T0,K0,V0), resUpdate T0, crash, invRead (T1,K0), resRead (T1,V0)]
        = trace_hide ?tST (ev ` internalSpec)›
    by (auto simp: internalSpec_def)
qed

lemma spec_trace_crash_read_null:
  ‹map(ev)[
      invUpdate (T0,K0,V0),
      resUpdate T0,
      crash,
      invRead (T1,K0),
      resRead (T1,TNull)
   ] ∈ Traces Spec›
  oops

lemma dali_has_crash_trace: ‹[ev crash] ∈ Traces Dali› oops

lemma dali_simple_update_trace: ‹map(ev)[invUpdate (T0,K0,V0), resUpdate T0] ∈ Traces Dali› oops

lemma dali_trace_crash_read_null:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      resUpdate T0,
      crash,
      invRead (T1,K0),
      resRead (T1,TNull)
   ] ∈ Traces Dali›
  oops

lemma dali_trace_crash_read_value:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      resUpdate T0,
      crash,
      invRead (T1,K0),
      resRead (T1,V0)
   ] ∈ Traces Dali›
  oops

lemma spec_trace_complex_1:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      crash,
      invUpdate (T1,K1,V0),
      resUpdate T1,
      invUpdate (T1,K1,V1),
      resUpdate T1,
      invRead (T1,K1),
      resRead (T1,V1),
      invRead (T1,K0),
      resRead (T1,TNull)
   ] ∈ Traces Spec›
  oops

lemma spec_trace_complex_2:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      resUpdate T0,
      crash,
      invUpdate (T1,K1,V0),
      resUpdate T1,
      invUpdate (T1,K1,V1),
      resUpdate T1,
      invRead (T1,K1),
      resRead (T1,V1),
      invRead (T1,K0),
      resRead (T1,V0)
   ] ∈ Traces Spec›
  oops

lemma dali_trace_complex_1:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      crash,
      invUpdate (T1,K1,V0),
      resUpdate T1,
      invUpdate (T1,K1,V1),
      resUpdate T1,
      invRead (T1,K1),
      resRead (T1,V1),
      invRead (T1,K0),
      resRead (T1,TNull)
   ] ∈ Traces Dali›
  oops


lemma dali_trace_complex_2:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      resUpdate T0,
      crash,
      invUpdate (T1,K1,V0),
      resUpdate T1,
      invUpdate (T1,K1,V1),
      resUpdate T1,
      invRead (T1,K1),
      resRead (T1,V1),
      invRead (T1,K0),
      resRead (T1,V0)
   ] ∈ Traces Dali›
  oops


lemma spec_trace_multi_crash_1:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      crash,
      invUpdate (T1,K1,V0),
      resUpdate T1,
      crash,
      invUpdate (T2,K1,V1),
      resUpdate T2,
      invRead (T2,K1),
      resRead (T2,V1),
      invRead (T2,K0),
      resRead (T2,TNull)
   ] ∈ Traces Spec›
  oops


lemma spec_trace_multi_crash_2:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      resUpdate T0,
      crash,
      invUpdate (T1,K1,V0),
      resUpdate T1,
      invUpdate (T1,K1,V1),
      crash,
      invRead (T2,K1),
      resRead (T2,V0),
      invRead (T2,K0),
      resRead (T2,V0)
   ] ∈ Traces Spec›
  oops


lemma dali_trace_complex_1:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      crash,
      invUpdate (T1,K1,V0),
      resUpdate T1,
      invUpdate (T1,K1,V1),
      resUpdate T1,
      invRead (T1,K1),
      resRead (T1,V1),
      invRead (T1,K0),
      resRead (T1,TNull)
   ] ∈ Traces Dali›
  oops


lemma dali_trace_multi_crash_epoch:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      resUpdate T0,
      crash,
      invUpdate (T1,K1,V0),
      resUpdate T1,
      invUpdate (T1,K1,V1),
      crash,
      invRead (T2,K1),
      resRead (T2,V0),
      invRead (T2,K0),
      resRead (T2,V0)
   ] ∈ Traces Dali›
  oops


lemma spec_trace_multi_crash_3:
  ‹map(ev)[
      invUpdate (T0,K0,V0),
      resUpdate T0,
      crash,
      crash,
      invRead (T1,K0),
      resRead (T1,TNull),
      invUpdate (T1,K1,V0),
      resUpdate T1,
      invUpdate (T1,K0,V0),
      resUpdate T1,
      crash,
      invRead (T2,K1),
      resRead (T2,V0),
      invRead (T2,K0),
      resRead (T2,TNull)
   ] ∈ Traces Spec›
  oops


lemma dali_trace_multi_crash_3:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      resUpdate T0,
      crash,
      crash,
      invRead (T1,K0),
      resRead (T1,TNull),
      invUpdate (T1,K1,V0),
      resUpdate T1,
      invUpdate (T1,K0,V0),
      resUpdate T1,
      crash,
      invRead (T2,K1),
      resRead (T2,V0),
      invRead (T2,K0),
      resRead (T2,TNull)
   ] ∈ Traces Dali›
  oops


lemma spec_trace_concurrent_1:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      invUpdate (T1,K1,V1),
      resUpdate T0,
      resUpdate T1,
      crash,
      invRead (T2,K1),
      resRead (T2,V1),
      invRead (T2,K0),
      resRead (T2,V0)
   ] ∈ Traces Spec›
  oops


lemma spec_trace_concurrent_2:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      invUpdate (T1,K1,V1),
      resUpdate T0,
      resUpdate T1,
      crash,
      invRead (T2,K1),
      resRead (T2,TNull),
      invRead (T2,K0),
      resRead (T2,V0)
   ] ∈ Traces Spec›
  oops


lemma dali_trace_concurrent_1:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      invUpdate (T1,K1,V1),
      resUpdate T0,
      resUpdate T1,
      crash,
      invRead (T2,K1),
      resRead (T2,V1),
      invRead (T2,K0),
      resRead (T2,V0)
   ] ∈ Traces Dali›
  oops


lemma dali_trace_concurrent_2:
  ‹map(ev) [
      invUpdate (T0,K0,V0),
      invUpdate (T1,K1,V1),
      resUpdate T0,
      resUpdate T1,
      crash,
      invRead (T2,K1),
      resRead (T2,TNull),
      invRead (T2,K0),
      resRead (T2,V0)
   ] ∈ Traces Dali›
  oops




end


section ‹Check: Dali is Accepted in Restriction Spaces›

text ‹With ‹Fixrec [RS, HOLCF]›, a failing constructiveness proof falls back to HOLCF silently.
The following assertion guards against this: all recursive definitions of Dali must be
restriction fixpoints ‹υ› (this relies in particular on
@{thm [source] ThrowR_constructive} for the crash handling).›

ML ‹
local
  val ctxt = @{context}
  val rec_defs = Facts.dest_static false [] (Proof_Context.facts_of ctxt) |> map fst
    |> filter (fn n => String.isPrefix "Dali_Combined." n andalso String.isSuffix "_rec_def" n)
  fun is_rs n = exists_Const (fn (c, _) => c = const_name‹restriction_fix›)
                  (Thm.prop_of (hd (Proof_Context.get_thms ctxt n)))
  val non_rs = filter_out is_rs rec_defs
in
  val _ = @{assert} (not (null rec_defs))
  val _ = null non_rs orelse error ("Dali: not accepted in RS: " ^ commas non_rs)
end
›

end