# Theory MemoryImplementation

Up to index of Isabelle/HOL/TLA/Memory

theory MemoryImplementation
imports Memory RPC MemClerk
uses [MemoryImplementation.ML]
begin

    (*
        File:        MemoryImplementation.thy
        ID:          $Id: MemoryImplementation.thy,v 1.5 2005/09/07 18:22:42 wenzelm Exp $
        Author:      Stephan Merz
        Copyright:   1997 University of Munich

        Theory Name: MemoryImplementation
        Logic Image: TLA

        RPC-Memory example: Memory implementation
    *)

    theory MemoryImplementation
    imports Memory RPC MemClerk
    begin

    datatype histState = histA | histB

    types
      histType  = "(PrIds => histState) stfun"     (* the type of the history variable *)

    consts
      (* the specification *)
         (* channel (external) *)
      memCh         :: "memChType"
         (* internal variables *)
      mm            :: "memType"

      (* the state variables of the implementation *)
         (* channels *)
      (* same interface channel memCh *)
      crCh          :: "rpcSndChType"
      rmCh          :: "rpcRcvChType"
         (* internal variables *)
      (* identity refinement mapping for mm -- simply reused *)
      rst           :: "rpcStType"
      cst           :: "mClkStType"
      ires          :: "resType"

    constdefs
      (* auxiliary predicates *)
      MVOKBARF      :: "Vals => bool"
         "MVOKBARF v == (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
      MVOKBA        :: "Vals => bool"
         "MVOKBA v   == (v : MemVal) | (v = OK) | (v = BadArg)"
      MVNROKBA      :: "Vals => bool"
         "MVNROKBA v == (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)"

      (* tuples of state functions changed by the various components *)
      e             :: "PrIds => (bit * memOp) stfun"
         "e p == PRED (caller memCh!p)"
      c             :: "PrIds => (mClkState * (bit * Vals) * (bit * rpcOp)) stfun"
         "c p == PRED (cst!p, rtrner memCh!p, caller crCh!p)"
      r             :: "PrIds => (rpcState * (bit * Vals) * (bit * memOp)) stfun"
         "r p == PRED (rst!p, rtrner crCh!p, caller rmCh!p)"
      m             :: "PrIds => ((bit * Vals) * Vals) stfun"
         "m p == PRED (rtrner rmCh!p, ires!p)"

      (* the environment action *)
      ENext         :: "PrIds => action"
         "ENext p == ACT (? l. #l : #MemLoc & Call memCh p #(read l))"

      (* specification of the history variable *)
      HInit         :: "histType => PrIds => stpred"
         "HInit rmhist p == PRED rmhist!p = #histA"

      HNext         :: "histType => PrIds => action"
         "HNext rmhist p == ACT (rmhist!p)$ =
                         (if (MemReturn rmCh ires p | RPCFail crCh rmCh rst p)
                          then #histB
                          else if (MClkReply memCh crCh cst p)
                               then #histA
                               else $(rmhist!p))"

      HistP         :: "histType => PrIds => temporal"
         "HistP rmhist p == TEMP Init HInit rmhist p
                               & [][HNext rmhist p]_(c p,r p,m p, rmhist!p)"

      Hist          :: "histType => temporal"
          "Hist rmhist == TEMP (ALL p. HistP rmhist p)"

      (* the implementation *)
      IPImp          :: "PrIds => temporal"
         "IPImp p == TEMP (  Init ~Calling memCh p & [][ENext p]_(e p)
                           & MClkIPSpec memCh crCh cst p
                           & RPCIPSpec crCh rmCh rst p
                           & RPSpec rmCh mm ires p
                           & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l))"

      ImpInit        :: "PrIds => stpred"
          "ImpInit p == PRED (  ~Calling memCh p
                              & MClkInit crCh cst p
                              & RPCInit rmCh rst p
                              & PInit ires p)"

      ImpNext        :: "PrIds => action"
          "ImpNext p == ACT  [ENext p]_(e p)
                           & [MClkNext memCh crCh cst p]_(c p)
                           & [RPCNext crCh rmCh rst p]_(r p)
                           & [RNext rmCh mm ires p]_(m p)"

      ImpLive        :: "PrIds => temporal"
          "ImpLive p == TEMP  WF(MClkFwd memCh crCh cst p)_(c p)
                            & SF(MClkReply memCh crCh cst p)_(c p)
                            & WF(RPCNext crCh rmCh rst p)_(r p)
                            & WF(RNext rmCh mm ires p)_(m p)
                            & WF(MemReturn rmCh ires p)_(m p)"

      Implementation :: "temporal"
          "Implementation == TEMP ( (ALL p. Init (~Calling memCh p) & [][ENext p]_(e p))
                                   & MClkISpec memCh crCh cst
                                   & RPCISpec crCh rmCh rst
                                   & IRSpec rmCh mm ires)"

      (* the predicate S describes the states of the implementation.
         slight simplification: two "histState" parameters instead of a
         (one- or two-element) set.
         NB: The second conjunct of the definition in the paper is taken care of by
         the type definitions. The last conjunct is asserted separately as the memory
         invariant MemInv, proved in Memory.ML. *)
      S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred"
          "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p == PRED
                    Calling memCh p = #ecalling
                  & Calling crCh p  = #ccalling
                  & (#ccalling --> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
                  & (~ #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>)
                  & Calling rmCh p  = #rcalling
                  & (#rcalling --> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
                  & (~ #rcalling --> ires!p = #NotAResult)
                  & (~ #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>)
                  & cst!p = #cs
                  & rst!p = #rs
                  & (rmhist!p = #hs1 | rmhist!p = #hs2)
                  & MVNROKBA<ires!p>"

      (* predicates S1 -- S6 define special instances of S *)
      S1            :: "histType => PrIds => stpred"
          "S1 rmhist p == S rmhist False False False clkA rpcA histA histA p"
      S2            :: "histType => PrIds => stpred"
          "S2 rmhist p == S rmhist True False False clkA rpcA histA histA p"
      S3            :: "histType => PrIds => stpred"
          "S3 rmhist p == S rmhist True True False clkB rpcA histA histB p"
      S4            :: "histType => PrIds => stpred"
          "S4 rmhist p == S rmhist True True True clkB rpcB histA histB p"
      S5            :: "histType => PrIds => stpred"
          "S5 rmhist p == S rmhist True True False clkB rpcB histB histB p"
      S6            :: "histType => PrIds => stpred"
          "S6 rmhist p == S rmhist True False False clkB rpcA histB histB p"

      (* The invariant asserts that the system is always in one of S1 - S6, for every p *)
      ImpInv         :: "histType => PrIds => stpred"
          "ImpInv rmhist p == PRED (  S1 rmhist p | S2 rmhist p | S3 rmhist p
                                    | S4 rmhist p | S5 rmhist p | S6 rmhist p)"

      resbar        :: "histType => resType"        (* refinement mapping *)
          "resbar rmhist s p ==
                      (if (S1 rmhist p s | S2 rmhist p s)
                       then ires s p
                       else if S3 rmhist p s
                       then if rmhist s p = histA
                            then ires s p else MemFailure
                       else if S4 rmhist p s
                       then if (rmhist s p = histB & ires s p = NotAResult)
                            then MemFailure else ires s p
                       else if S5 rmhist p s
                       then res (rmCh s p)
                       else if S6 rmhist p s
                       then if res (crCh s p) = RPCFailure
                            then MemFailure else res (crCh s p)
                       else NotAResult)" (* dummy value *)

    axioms
      (* the "base" variables: everything except resbar and hist (for any index) *)
      MI_base:       "basevars (caller memCh!p,
                               (rtrner memCh!p, caller crCh!p, cst!p),
                               (rtrner crCh!p, caller rmCh!p, rst!p),
                               (mm!l, rtrner rmCh!p, ires!p))"

    ML {* use_legacy_bindings (the_context ()) *}

    end

## History variable

theorem HistoryLemma:

      |- Init (∀p. ImpInit p) ∧ [](∀p. ImpNext p) -->
         (∃∃ rmhist.
             Init (∀p. HInit rmhist p) ∧
             [](∀p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))

theorem History:

      |- Implementation --> (∃∃ rmhist. Hist rmhist)

## The safety part

theorem MVOKBAnotRF:

      MVOKBA x ==> x ≠ RPCFailure

theorem MVOKBARFnotNR:

      MVOKBARF x ==> x ≠ NotAResult

theorem S2_excl:

      |- S2 rmhist p --> S2 rmhist p ∧ ¬ S1 rmhist p

theorem S3_excl:

      |- S3 rmhist p --> S3 rmhist p ∧ ¬ S1 rmhist p ∧ ¬ S2 rmhist p

theorem S4_excl:

      |- S4 rmhist p --> S4 rmhist p ∧ ¬ S1 rmhist p ∧ ¬ S2 rmhist p ∧ ¬ S3 rmhist p

theorem S5_excl:

      |- S5 rmhist p -->
         S5 rmhist p ∧ ¬ S1 rmhist p ∧ ¬ S2 rmhist p ∧ ¬ S3 rmhist p ∧ ¬ S4 rmhist p

theorem S6_excl:

      |- S6 rmhist p -->
         S6 rmhist p ∧
         ¬ S1 rmhist p ∧ ¬ S2 rmhist p ∧ ¬ S3 rmhist p ∧ ¬ S4 rmhist p ∧ ¬ S5 rmhist p

theorem Envbusy:

      |- $Calling memCh p --> ¬ ENext p

theorem S1Env:

      |- ENext p ∧ $S1 rmhist p ∧ unchanged (c p, r p, m p, rmhist!p) --> S2 rmhist p$

theorem S1ClerkUnch:

      |- [MClkNext memCh crCh cst p]_(c p) ∧ $S1 rmhist p --> unchanged c p

theorem S1RPCUnch:

      |- [RPCNext crCh rmCh rst p]_(r p) ∧ $S1 rmhist p --> unchanged r p

theorem S1MemUnch:

      |- [RNext rmCh mm ires p]_(m p) ∧ $S1 rmhist p --> unchanged m p

theorem S1Hist:

      |- [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ $S1 rmhist p -->
         unchanged (rmhist!p)

theorem S2EnvUnch:

      |- [ENext p]_(e p) ∧ $S2 rmhist p --> unchanged e p

theorem S2Clerk:

      |- MClkNext memCh crCh cst p ∧ $S2 rmhist p --> MClkFwd memCh crCh cst p

theorem S2Forward:

      |- $S2 rmhist p ∧
         MClkFwd memCh crCh cst p ∧ unchanged (e p, r p, m p, rmhist!p) -->
         S3 rmhist p$

theorem S2RPCUnch:

      |- [RPCNext crCh rmCh rst p]_(r p) ∧ $S2 rmhist p --> unchanged r p

theorem S2MemUnch:

      |- [RNext rmCh mm ires p]_(m p) ∧ $S2 rmhist p --> unchanged m p

theorem S2Hist:

      |- [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ $S2 rmhist p -->
         unchanged (rmhist!p)

theorem S3EnvUnch:

      |- [ENext p]_(e p) ∧ $S3 rmhist p --> unchanged e p

theorem S3ClerkUnch:

      |- [MClkNext memCh crCh cst p]_(c p) ∧ $S3 rmhist p --> unchanged c p

theorem S3LegalRcvArg:

      |- S3 rmhist p --> IsLegalRcvArg<arg<crCh!p>>

theorem S3RPC:

      |- RPCNext crCh rmCh rst p ∧ $S3 rmhist p -->
         RPCFwd crCh rmCh rst p ∨ RPCFail crCh rmCh rst p

theorem S3Forward:

      |- RPCFwd crCh rmCh rst p ∧
         HNext rmhist p ∧ $S3 rmhist p ∧ unchanged (e p, c p, m p) -->
         S4 rmhist p$ ∧ unchanged (rmhist!p)

theorem S3Fail:

      |- RPCFail crCh rmCh rst p ∧
         $S3 rmhist p ∧ HNext rmhist p ∧ unchanged (e p, c p, m p) -->
         S6 rmhist p$

theorem S3MemUnch:

      |- [RNext rmCh mm ires p]_(m p) ∧ $S3 rmhist p --> unchanged m p

theorem S3Hist:

      |- HNext rmhist p ∧ $S3 rmhist p ∧ unchanged r p --> unchanged (rmhist!p)

theorem S4EnvUnch:

      |- [ENext p]_(e p) ∧ $S4 rmhist p --> unchanged e p

theorem S4ClerkUnch:

      |- [MClkNext memCh crCh cst p]_(c p) ∧ $S4 rmhist p --> unchanged c p

theorem S4RPCUnch:

      |- [RPCNext crCh rmCh rst p]_(r p) ∧ $S4 rmhist p --> unchanged r p

theorem S4ReadInner:

      |- ReadInner rmCh mm ires p l ∧
         $S4 rmhist p ∧ unchanged (e p, c p, r p) ∧ HNext rmhist p ∧ $MemInv mm l -->
         S4 rmhist p$ ∧ unchanged (rmhist!p)

theorem S4Read:

      |- Read rmCh mm ires p ∧
         $S4 rmhist p ∧
         unchanged (e p, c p, r p) ∧ HNext rmhist p ∧ (∀l. $MemInv mm l) -->
         S4 rmhist p$ ∧ unchanged (rmhist!p)

theorem S4WriteInner:

      |- WriteInner rmCh mm ires p l v ∧
         $S4 rmhist p ∧ unchanged (e p, c p, r p) ∧ HNext rmhist p -->
         S4 rmhist p$ ∧ unchanged (rmhist!p)

theorem S4Write:

      |- Write rmCh mm ires p l ∧
         $S4 rmhist p ∧ unchanged (e p, c p, r p) ∧ HNext rmhist p -->
         S4 rmhist p$ ∧ unchanged (rmhist!p)

theorem WriteS4:

      |- $ImpInv rmhist p ∧ Write rmCh mm ires p l --> $S4 rmhist p

theorem S4Return:

      |- MemReturn rmCh ires p ∧
         $S4 rmhist p ∧ unchanged (e p, c p, r p) ∧ HNext rmhist p -->
         S5 rmhist p$

theorem S4Hist:

      |- HNext rmhist p ∧ $S4 rmhist p ∧ m p$ = $m p --> (rmhist!p)$ = $(rmhist!p)

theorem S5EnvUnch:

      |- [ENext p]_(e p) ∧ $S5 rmhist p --> unchanged e p

theorem S5ClerkUnch:

      |- [MClkNext memCh crCh cst p]_(c p) ∧ $S5 rmhist p --> unchanged c p

theorem S5RPC:

      |- RPCNext crCh rmCh rst p ∧ $S5 rmhist p -->
         RPCReply crCh rmCh rst p ∨ RPCFail crCh rmCh rst p

theorem S5Reply:

      |- RPCReply crCh rmCh rst p ∧
         $S5 rmhist p ∧ unchanged (e p, c p, m p, rmhist!p) -->
         S6 rmhist p$

theorem S5Fail:

      |- RPCFail crCh rmCh rst p ∧
         $S5 rmhist p ∧ unchanged (e p, c p, m p, rmhist!p) -->
         S6 rmhist p$

theorem S5MemUnch:

      |- [RNext rmCh mm ires p]_(m p) ∧ $S5 rmhist p --> unchanged m p

theorem S5Hist:

      |- [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ $S5 rmhist p -->
         (rmhist!p)$ = $(rmhist!p)

theorem S6EnvUnch:

      |- [ENext p]_(e p) ∧ $S6 rmhist p --> unchanged e p

theorem S6Clerk:

      |- MClkNext memCh crCh cst p ∧ $S6 rmhist p -->
         MClkRetry memCh crCh cst p ∨ MClkReply memCh crCh cst p

theorem S6Retry:

      |- MClkRetry memCh crCh cst p ∧
         HNext rmhist p ∧ $S6 rmhist p ∧ unchanged (e p, r p, m p) -->
         S3 rmhist p$ ∧ unchanged (rmhist!p)

theorem S6Reply:

      |- MClkReply memCh crCh cst p ∧
         HNext rmhist p ∧ $S6 rmhist p ∧ unchanged (e p, r p, m p) -->
         S1 rmhist p$

theorem S6RPCUnch:

      |- [RPCNext crCh rmCh rst p]_(r p) ∧ $S6 rmhist p --> unchanged r p

theorem S6MemUnch:

      |- [RNext rmCh mm ires p]_(m p) ∧ $S6 rmhist p --> unchanged m p

theorem S6Hist:

      |- HNext rmhist p ∧ $S6 rmhist p ∧ c p$ = $c p --> (rmhist!p)$ = $(rmhist!p)

## Correctness of predicate-action diagram

theorem Step1_1:

      |- ImpInit p ∧ HInit rmhist p --> S1 rmhist p

theorem Step1_2_1:

      |- [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧
         ImpNext p ∧ ¬ unchanged (e p, c p, r p, m p, rmhist!p) ∧ $S1 rmhist p -->
         S2 rmhist p$ ∧ ENext p ∧ unchanged (c p, r p, m p)

theorem Step1_2_2:

      |- [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧
         ImpNext p ∧ ¬ unchanged (e p, c p, r p, m p, rmhist!p) ∧ $S2 rmhist p -->
         S3 rmhist p$ ∧ MClkFwd memCh crCh cst p ∧ unchanged (e p, r p, m p, rmhist!p)

theorem Step1_2_3:

      |- [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧
         ImpNext p ∧ ¬ unchanged (e p, c p, r p, m p, rmhist!p) ∧ $S3 rmhist p -->
         S4 rmhist p$ ∧ RPCFwd crCh rmCh rst p ∧ unchanged (e p, c p, m p, rmhist!p) ∨
         S6 rmhist p$ ∧ RPCFail crCh rmCh rst p ∧ unchanged (e p, c p, m p)

theorem Step1_2_4:

      |- [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧
         ImpNext p ∧
         ¬ unchanged (e p, c p, r p, m p, rmhist!p) ∧
         $S4 rmhist p ∧ (∀l. $MemInv mm l) -->
         S4 rmhist p$ ∧ Read rmCh mm ires p ∧ unchanged (e p, c p, r p, rmhist!p) ∨
         S4 rmhist p$ ∧
         (∃l. Write rmCh mm ires p l) ∧ unchanged (e p, c p, r p, rmhist!p) ∨
         S5 rmhist p$ ∧ MemReturn rmCh ires p ∧ unchanged (e p, c p, r p)

theorem Step1_2_5:

      |- [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧
         ImpNext p ∧ ¬ unchanged (e p, c p, r p, m p, rmhist!p) ∧ $S5 rmhist p -->
         S6 rmhist p$ ∧ RPCReply crCh rmCh rst p ∧ unchanged (e p, c p, m p) ∨
         S6 rmhist p$ ∧ RPCFail crCh rmCh rst p ∧ unchanged (e p, c p, m p)

theorem Step1_2_6:

      |- [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧
         ImpNext p ∧ ¬ unchanged (e p, c p, r p, m p, rmhist!p) ∧ $S6 rmhist p -->
         S1 rmhist p$ ∧ MClkReply memCh crCh cst p ∧ unchanged (e p, r p, m p) ∨
         S3 rmhist p$ ∧
         MClkRetry memCh crCh cst p ∧ unchanged (e p, r p, m p, rmhist!p)

## Initialization (Step 1.3)

theorem Step1_3:

      |- S1 rmhist p --> PInit (resbar rmhist) p

## Step simulation (Step 1.4)

theorem Step1_4_1:

      |- ENext p ∧ $S1 rmhist p ∧ S2 rmhist p$ ∧ unchanged (c p, r p, m p) -->
         unchanged (rtrner memCh!p, resbar rmhist!p)

theorem Step1_4_2:

      |- MClkFwd memCh crCh cst p ∧
         $S2 rmhist p ∧ S3 rmhist p$ ∧ unchanged (e p, r p, m p, rmhist!p) -->
         unchanged (rtrner memCh!p, resbar rmhist!p)

theorem Step1_4_3a:

      |- RPCFwd crCh rmCh rst p ∧
         $S3 rmhist p ∧ S4 rmhist p$ ∧ unchanged (e p, c p, m p, rmhist!p) -->
         unchanged (rtrner memCh!p, resbar rmhist!p)

theorem Step1_4_3b:

      |- RPCFail crCh rmCh rst p ∧
         $S3 rmhist p ∧ S6 rmhist p$ ∧ unchanged (e p, c p, m p) -->
         MemFail memCh (resbar rmhist) p

theorem Step1_4_4a1:

      |- $S4 rmhist p ∧
         S4 rmhist p$ ∧
         ReadInner rmCh mm ires p l ∧
         unchanged (e p, c p, r p, rmhist!p) ∧ $MemInv mm l -->
         ReadInner memCh mm (resbar rmhist) p l

theorem Step1_4_4a:

      |- Read rmCh mm ires p ∧
         $S4 rmhist p ∧
         S4 rmhist p$ ∧ unchanged (e p, c p, r p, rmhist!p) ∧ (∀l. $MemInv mm l) -->
         Read memCh mm (resbar rmhist) p

theorem Step1_4_4b1:

      |- $S4 rmhist p ∧
         S4 rmhist p$ ∧
         WriteInner rmCh mm ires p l v ∧ unchanged (e p, c p, r p, rmhist!p) -->
         WriteInner memCh mm (resbar rmhist) p l v

theorem Step1_4_4b:

      |- Write rmCh mm ires p l ∧
         $S4 rmhist p ∧ S4 rmhist p$ ∧ unchanged (e p, c p, r p, rmhist!p) -->
         Write memCh mm (resbar rmhist) p l

theorem Step1_4_4c:

      |- MemReturn rmCh ires p ∧
         $S4 rmhist p ∧ S5 rmhist p$ ∧ unchanged (e p, c p, r p) -->
         unchanged (rtrner memCh!p, resbar rmhist!p)

theorem Step1_4_5a:

      |- RPCReply crCh rmCh rst p ∧
         $S5 rmhist p ∧ S6 rmhist p$ ∧ unchanged (e p, c p, m p) -->
         unchanged (rtrner memCh!p, resbar rmhist!p)

theorem Step1_4_5b:

      |- RPCFail crCh rmCh rst p ∧
         $S5 rmhist p ∧ S6 rmhist p$ ∧ unchanged (e p, c p, m p) -->
         MemFail memCh (resbar rmhist) p

theorem Step1_4_6a:

      |- MClkReply memCh crCh cst p ∧
         $S6 rmhist p ∧ S1 rmhist p$ ∧ unchanged (e p, r p, m p) -->
         MemReturn memCh (resbar rmhist) p

theorem Step1_4_6b:

      |- MClkRetry memCh crCh cst p ∧
         $S6 rmhist p ∧ S3 rmhist p$ ∧ unchanged (e p, r p, m p, rmhist!p) -->
         MemFail memCh (resbar rmhist) p

theorem S_lemma:

      |- unchanged (e p, c p, r p, m p, rmhist!p) -->
         unchanged S rmhist ec cc rc cs rs hs1.0 hs2.0 p

theorem Step1_4_7H:

      |- unchanged (e p, c p, r p, m p, rmhist!p) -->
         unchanged (rtrner memCh!p, S1 rmhist p, S2 rmhist p, S3 rmhist p,
                    S4 rmhist p, S5 rmhist p, S6 rmhist p)

theorem Step1_4_7:

      |- unchanged (e p, c p, r p, m p, rmhist!p) -->
         unchanged (rtrner memCh!p, resbar rmhist!p, S1 rmhist p, S2 rmhist p,
                    S3 rmhist p, S4 rmhist p, S5 rmhist p, S6 rmhist p)

theorem unchanged_safe:

      |- (¬ unchanged (e p, c p, r p, m p, rmhist!p) -->
          [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)) -->
         [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)

theorem unchanged_safeI:

      ((e p t, c p t, r p t, m p t, (rmhist!p) t) ≠
       (e p s, c p s, r p s, m p s, (rmhist!p) s)
       ==> (s, t) |= [UNext memCh mm (resbar rmhist)
                       p]_(rtrner memCh!p, resbar rmhist!p))
      ==> (s, t) |= [UNext memCh mm (resbar rmhist)
                      p]_(rtrner memCh!p, resbar rmhist!p)

theorem S1safe:

      |- $S1 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) -->
         [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)

theorem S2safe:

      |- $S2 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) -->
         [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)

theorem S3safe:

      |- $S3 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) -->
         [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)

theorem S4safe:

      |- $S4 rmhist p ∧
         ImpNext p ∧
         [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ (∀l. $MemInv mm l) -->
         [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)

theorem S5safe:

      |- $S5 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) -->
         [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)

theorem S6safe:

      |- $S6 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) -->
         [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)

## The liveness part

theorem S1_successors:

      |- $S1 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) -->
         S1 rmhist p$ ∨ S2 rmhist p$

theorem S1_RNextdisabled:

      |- S1 rmhist p -->
         ¬ Enabled (<RNext memCh mm (resbar rmhist)
                      p>_(rtrner memCh!p, resbar rmhist!p))

theorem S1_Returndisabled:

      |- S1 rmhist p -->
         ¬ Enabled (<MemReturn memCh (resbar rmhist)
                      p>_(rtrner memCh!p, resbar rmhist!p))

theorem RNext_fair:

      |- []<>S1 rmhist p -->
         WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)

theorem Return_fair:

      |- []<>S1 rmhist p -->
         WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)

theorem S2_successors:

      |- $S2 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) -->
         S2 rmhist p$ ∨ S3 rmhist p$

theorem S2MClkFwd_successors:

      |- ($S2 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p)) ∧
         <MClkFwd memCh crCh cst p>_(c p) -->
         S3 rmhist p$

theorem S2MClkFwd_enabled:

      |- $S2 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) -->
         $Enabled (<MClkFwd memCh crCh cst p>_(c p))

theorem S2_live:

      |- [](ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p)) ∧
         WF(MClkFwd memCh crCh cst p)_c p -->
         (S2 rmhist p ~> S3 rmhist p)

theorem S3_successors:

      |- $S3 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) -->
         S3 rmhist p$ ∨ (S4 rmhist p ∨ S6 rmhist p)$

theorem S3RPC_successors:

      |- ($S3 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p)) ∧
         <RPCNext crCh rmCh rst p>_(r p) -->
         (S4 rmhist p ∨ S6 rmhist p)$

theorem S3RPC_enabled:

      |- $S3 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) -->
         $Enabled (<RPCNext crCh rmCh rst p>_(r p))

theorem S3_live:

      |- [](ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p)) ∧
         WF(RPCNext crCh rmCh rst p)_r p -->
         (S3 rmhist p ~> S4 rmhist p ∨ S6 rmhist p)

theorem S4_successors:

      |- $S4 rmhist p ∧
         ImpNext p ∧
         [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ (∀l. $MemInv mm l) -->
         S4 rmhist p$ ∨ S5 rmhist p$

theorem S4a_successors:

      |- $(S4 rmhist p ∧ ires!p = #NotAResult) ∧
         ImpNext p ∧
         [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ (∀l. $MemInv mm l) -->
         (S4 rmhist p ∧ ires!p = #NotAResult)$ ∨
         (S4 rmhist p ∧ ires!p ≠ #NotAResult ∨ S5 rmhist p)$

theorem S4aRNext_successors:

      |- ($(S4 rmhist p ∧ ires!p = #NotAResult) ∧
          ImpNext p ∧
          [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ (∀l. $MemInv mm l)) ∧
         <RNext rmCh mm ires p>_(m p) -->
         (S4 rmhist p ∧ ires!p ≠ #NotAResult ∨ S5 rmhist p)$

theorem S4aRNext_enabled:

      |- $(S4 rmhist p ∧ ires!p = #NotAResult) ∧
         ImpNext p ∧
         [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ (∀l. $MemInv mm l) -->
         $Enabled (<RNext rmCh mm ires p>_(m p))

theorem S4a_live:

      |- [](ImpNext p ∧
            [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ (∀l. $MemInv mm l)) ∧
         WF(RNext rmCh mm ires p)_m p -->
         (S4 rmhist p ∧
          ires!p = #NotAResult ~> S4 rmhist p ∧ ires!p ≠ #NotAResult ∨ S5 rmhist p)

theorem S4b_successors:

      |- $(S4 rmhist p ∧ ires!p ≠ #NotAResult) ∧
         ImpNext p ∧
         [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ (∀l. $MemInv mm l) -->
         (S4 rmhist p ∧ ires!p ≠ #NotAResult)$ ∨ S5 rmhist p$

theorem S4bReturn_successors:

      |- ($(S4 rmhist p ∧ ires!p ≠ #NotAResult) ∧
          ImpNext p ∧
          [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ (∀l. $MemInv mm l)) ∧
         <MemReturn rmCh ires p>_(m p) -->
         S5 rmhist p$

theorem S4bReturn_enabled:

      |- $(S4 rmhist p ∧ ires!p ≠ #NotAResult) ∧
         ImpNext p ∧
         [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ (∀l. $MemInv mm l) -->
         $Enabled (<MemReturn rmCh ires p>_(m p))

theorem S4b_live:

      |- [](ImpNext p ∧
            [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ (∀l. $MemInv mm l)) ∧
         WF(MemReturn rmCh ires p)_m p -->
         (S4 rmhist p ∧ ires!p ≠ #NotAResult ~> S5 rmhist p)

theorem S5_successors:

      |- $S5 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) -->
         S5 rmhist p$ ∨ S6 rmhist p$

theorem S5RPC_successors:

      |- ($S5 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p)) ∧
         <RPCNext crCh rmCh rst p>_(r p) -->
         S6 rmhist p$

theorem S5RPC_enabled:

      |- $S5 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) -->
         $Enabled (<RPCNext crCh rmCh rst p>_(r p))

theorem S5_live:

      |- [](ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p)) ∧
         WF(RPCNext crCh rmCh rst p)_r p -->
         (S5 rmhist p ~> S6 rmhist p)

theorem S6_successors:

      |- $S6 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) -->
         S1 rmhist p$ ∨ S3 rmhist p$ ∨ S6 rmhist p$

theorem S6MClkReply_successors:

      |- ($S6 rmhist p ∧ ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p)) ∧
         <MClkReply memCh crCh cst p>_(c p) -->
         S1 rmhist p$

theorem MClkReplyS6:

      |- $ImpInv rmhist p ∧ <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p

theorem S6MClkReply_enabled:

      |- S6 rmhist p --> Enabled (<MClkReply memCh crCh cst p>_(c p))

theorem S6_live:

      |- [](ImpNext p ∧
            [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ $ImpInv rmhist p) ∧
         SF(MClkReply memCh crCh cst p)_c p ∧ []<>S6 rmhist p -->
         []<>S1 rmhist p

theorem S5S6LeadstoS6:

      sigma |= S5 rmhist p ~> S6 rmhist p
      ==> sigma |= S5 rmhist p ∨ S6 rmhist p ~> S6 rmhist p

theorem S4bS5S6LeadstoS6:

      [| sigma |= S4 rmhist p ∧ ires!p ≠ #NotAResult ~> S5 rmhist p;
         sigma |= S5 rmhist p ~> S6 rmhist p |]
      ==> sigma |= S4 rmhist p ∧ ires!p ≠ #NotAResult ∨
                   S5 rmhist p ∨ S6 rmhist p ~> S6 rmhist p

theorem S4S5S6LeadstoS6:

      [| sigma |= S4 rmhist p ∧
                  ires!p =
                  #NotAResult ~> S4 rmhist p ∧ ires!p ≠ #NotAResult ∨ S5 rmhist p;
         sigma |= S4 rmhist p ∧ ires!p ≠ #NotAResult ~> S5 rmhist p;
         sigma |= S5 rmhist p ~> S6 rmhist p |]
      ==> sigma |= S4 rmhist p ∨ S5 rmhist p ∨ S6 rmhist p ~> S6 rmhist p

theorem S3S4S5S6LeadstoS6:

      [| sigma |= S3 rmhist p ~> S4 rmhist p ∨ S6 rmhist p;
         sigma |= S4 rmhist p ∧
                  ires!p =
                  #NotAResult ~> S4 rmhist p ∧ ires!p ≠ #NotAResult ∨ S5 rmhist p;
         sigma |= S4 rmhist p ∧ ires!p ≠ #NotAResult ~> S5 rmhist p;
         sigma |= S5 rmhist p ~> S6 rmhist p |]
      ==> sigma |= S3 rmhist p ∨
                   S4 rmhist p ∨ S5 rmhist p ∨ S6 rmhist p ~> S6 rmhist p

theorem S2S3S4S5S6LeadstoS6:

      [| sigma |= S2 rmhist p ~> S3 rmhist p;
         sigma |= S3 rmhist p ~> S4 rmhist p ∨ S6 rmhist p;
         sigma |= S4 rmhist p ∧
                  ires!p =
                  #NotAResult ~> S4 rmhist p ∧ ires!p ≠ #NotAResult ∨ S5 rmhist p;
         sigma |= S4 rmhist p ∧ ires!p ≠ #NotAResult ~> S5 rmhist p;
         sigma |= S5 rmhist p ~> S6 rmhist p |]
      ==> sigma |= S2 rmhist p ∨
                   S3 rmhist p ∨
                   S4 rmhist p ∨ S5 rmhist p ∨ S6 rmhist p ~> S6 rmhist p

theorem NotS1LeadstoS6:

      [| sigma |= []ImpInv rmhist p; sigma |= S2 rmhist p ~> S3 rmhist p;
         sigma |= S3 rmhist p ~> S4 rmhist p ∨ S6 rmhist p;
         sigma |= S4 rmhist p ∧
                  ires!p =
                  #NotAResult ~> S4 rmhist p ∧ ires!p ≠ #NotAResult ∨ S5 rmhist p;
         sigma |= S4 rmhist p ∧ ires!p ≠ #NotAResult ~> S5 rmhist p;
         sigma |= S5 rmhist p ~> S6 rmhist p |]
      ==> sigma |= ¬ S1 rmhist p ~> S6 rmhist p

theorem S1Infinite:

      [| sigma |= ¬ S1 rmhist p ~> S6 rmhist p;
         sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |]
      ==> sigma |= []<>S1 rmhist p

## Refinement proof (step 1.5)

theorem Step1_5_1a:

      |- IPImp p --> (∀l. []$MemInv mm l)

theorem Step1_5_1b:

      |- Init (ImpInit p ∧ HInit rmhist p) ∧
         []ImpNext p ∧
         [][HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ [](∀l. $MemInv mm l) -->
         []ImpInv rmhist p

theorem Step1_5_2a:

      |- Init (ImpInit p ∧ HInit rmhist p) --> Init PInit (resbar rmhist) p

theorem Step1_5_2b:

      |- [](ImpNext p ∧
            [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧
            $ImpInv rmhist p ∧ (∀l. $MemInv mm l)) -->
         [][UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)

theorem GoodImpl:

      |- IPImp p ∧ HistP rmhist p -->
         Init (ImpInit p ∧ HInit rmhist p) ∧
         [](ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p)) ∧
         [](∀l. $MemInv mm l) ∧ []$ImpInv rmhist p ∧ ImpLive p

theorem Step1_5_3a:

      |- [](ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p)) ∧
         [](∀l. $MemInv mm l) ∧ []$ImpInv rmhist p ∧ ImpLive p -->
         []<>S1 rmhist p

theorem Step1_5_3b:

      |- [](ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p)) ∧
         [](∀l. $MemInv mm l) ∧ []$ImpInv rmhist p ∧ ImpLive p -->
         WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)

theorem Step1_5_3c:

      |- [](ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p)) ∧
         [](∀l. $MemInv mm l) ∧ []$ImpInv rmhist p ∧ ImpLive p -->
         WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)

theorem Step1:

      |- IPImp p ∧ HistP rmhist p --> UPSpec memCh mm (resbar rmhist) p

## Step 2

theorem Step2_2a:

      |- Write rmCh mm ires p l ∧
         ImpNext p ∧ [HNext rmhist p]_(c p, r p, m p, rmhist!p) ∧ $ImpInv rmhist p -->
         S4 rmhist p$ ∧ unchanged (e p, c p, r p, rmhist!p)

theorem Step2_2:

      |- (∀p. ImpNext p) ∧
         (∀p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) ∧
         (∀p. $ImpInv rmhist p) ∧ [∃q. Write rmCh mm ires q l]_(mm!l) -->
         [∃q. Write memCh mm (resbar rmhist) q l]_(mm!l)

theorem Step2_lemma:

      |- []((∀p. ImpNext p) ∧
            (∀p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) ∧
            (∀p. $ImpInv rmhist p) ∧ [∃q. Write rmCh mm ires q l]_(mm!l)) -->
         [][∃q. Write memCh mm (resbar rmhist) q l]_(mm!l)

theorem Step2:

      |- #l ∈ #MemLoc ∧ (∀p. IPImp p ∧ HistP rmhist p) -->
         MSpec memCh mm (resbar rmhist) l

## Memory implementation

theorem Impl_IUSpec:

      |- Implementation ∧ Hist rmhist --> IUSpec memCh mm (resbar rmhist)

theorem Implementation:

      |- Implementation --> USpec memCh