src/HOL/TLA/Memory/Memory.thy

tuned headers;

(*  Title:      HOL/TLA/Memory/Memory.thy
    Author:     Stephan Merz, University of Munich
*)

header {* RPC-Memory example: Memory specification *}

theory Memory
imports MemoryParameters ProcedureInterface
begin

types
  memChType  = "(memOp, Vals) channel"
  memType = "(Locs => Vals) stfun"      (* intention: MemLocs => MemVals *)
  resType = "(PrIds => Vals) stfun"

consts
  (* state predicates *)
  MInit      :: "memType => Locs => stpred"
  PInit      :: "resType => PrIds => stpred"
  (* auxiliary predicates: is there a pending read/write request for
     some process id and location/value? *)
  RdRequest  :: "memChType => PrIds => Locs => stpred"
  WrRequest  :: "memChType => PrIds => Locs => Vals => stpred"

  (* actions *)
  GoodRead   :: "memType => resType => PrIds => Locs => action"
  BadRead    :: "memType => resType => PrIds => Locs => action"
  ReadInner  :: "memChType => memType => resType => PrIds => Locs => action"
  Read       :: "memChType => memType => resType => PrIds => action"
  GoodWrite  :: "memType => resType => PrIds => Locs => Vals => action"
  BadWrite   :: "memType => resType => PrIds => Locs => Vals => action"
  WriteInner :: "memChType => memType => resType => PrIds => Locs => Vals => action"
  Write      :: "memChType => memType => resType => PrIds => Locs => action"
  MemReturn  :: "memChType => resType => PrIds => action"
  MemFail    :: "memChType => resType => PrIds => action"
  RNext      :: "memChType => memType => resType => PrIds => action"
  UNext      :: "memChType => memType => resType => PrIds => action"

  (* temporal formulas *)
  RPSpec     :: "memChType => memType => resType => PrIds => temporal"
  UPSpec     :: "memChType => memType => resType => PrIds => temporal"
  MSpec      :: "memChType => memType => resType => Locs => temporal"
  IRSpec     :: "memChType => memType => resType => temporal"
  IUSpec     :: "memChType => memType => resType => temporal"

  RSpec      :: "memChType => resType => temporal"
  USpec      :: "memChType => temporal"

  (* memory invariant: in the paper, the invariant is hidden in the definition of
     the predicate S used in the implementation proof, but it is easier to verify
     at this level. *)
  MemInv    :: "memType => Locs => stpred"

defs
  MInit_def:         "MInit mm l == PRED mm!l = #InitVal"
  PInit_def:         "PInit rs p == PRED rs!p = #NotAResult"

  RdRequest_def:     "RdRequest ch p l == PRED
                         Calling ch p & (arg<ch!p> = #(read l))"
  WrRequest_def:     "WrRequest ch p l v == PRED
                         Calling ch p & (arg<ch!p> = #(write l v))"
  (* a read that doesn't raise BadArg *)
  GoodRead_def:      "GoodRead mm rs p l == ACT
                        #l : #MemLoc & ((rs!p)$ = $(mm!l))"
  (* a read that raises BadArg *)
  BadRead_def:       "BadRead mm rs p l == ACT
                        #l ~: #MemLoc & ((rs!p)$ = #BadArg)"
  (* the read action with l visible *)
  ReadInner_def:     "ReadInner ch mm rs p l == ACT
                         $(RdRequest ch p l)
                         & (GoodRead mm rs p l  |  BadRead mm rs p l)
                         & unchanged (rtrner ch ! p)"
  (* the read action with l quantified *)
  Read_def:          "Read ch mm rs p == ACT (EX l. ReadInner ch mm rs p l)"

  (* similar definitions for the write action *)
  GoodWrite_def:     "GoodWrite mm rs p l v == ACT
                        #l : #MemLoc & #v : #MemVal
                        & ((mm!l)$ = #v) & ((rs!p)$ = #OK)"
  BadWrite_def:      "BadWrite mm rs p l v == ACT
                        ~ (#l : #MemLoc & #v : #MemVal)
                        & ((rs!p)$ = #BadArg) & unchanged (mm!l)"
  WriteInner_def:    "WriteInner ch mm rs p l v == ACT
                        $(WrRequest ch p l v)
                        & (GoodWrite mm rs p l v  |  BadWrite mm rs p l v)
                        & unchanged (rtrner ch ! p)"
  Write_def:         "Write ch mm rs p l == ACT (EX v. WriteInner ch mm rs p l v)"

  (* the return action *)
  MemReturn_def:     "MemReturn ch rs p == ACT
                       (   ($(rs!p) ~= #NotAResult)
                        & ((rs!p)$ = #NotAResult)
                        & Return ch p (rs!p))"

  (* the failure action of the unreliable memory *)
  MemFail_def:       "MemFail ch rs p == ACT
                        $(Calling ch p)
                        & ((rs!p)$ = #MemFailure)
                        & unchanged (rtrner ch ! p)"
  (* next-state relations for reliable / unreliable memory *)
  RNext_def:         "RNext ch mm rs p == ACT
                       (  Read ch mm rs p
                        | (EX l. Write ch mm rs p l)
                        | MemReturn ch rs p)"
  UNext_def:         "UNext ch mm rs p == ACT
                        (RNext ch mm rs p | MemFail ch rs p)"

  RPSpec_def:        "RPSpec ch mm rs p == TEMP
                        Init(PInit rs p)
                        & [][ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
                        & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
                        & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
  UPSpec_def:        "UPSpec ch mm rs p == TEMP
                        Init(PInit rs p)
                        & [][ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
                        & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
                        & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
  MSpec_def:         "MSpec ch mm rs l == TEMP
                        Init(MInit mm l)
                        & [][ EX p. Write ch mm rs p l ]_(mm!l)"
  IRSpec_def:        "IRSpec ch mm rs == TEMP
                        (ALL p. RPSpec ch mm rs p)
                        & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
  IUSpec_def:        "IUSpec ch mm rs == TEMP
                        (ALL p. UPSpec ch mm rs p)
                        & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"

  RSpec_def:         "RSpec ch rs == TEMP (EEX mm. IRSpec ch mm rs)"
  USpec_def:         "USpec ch == TEMP (EEX mm rs. IUSpec ch mm rs)"

  MemInv_def:        "MemInv mm l == PRED  #l : #MemLoc --> mm!l : #MemVal"

lemmas RM_action_defs =
  MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def
  GoodRead_def BadRead_def ReadInner_def Read_def
  GoodWrite_def BadWrite_def WriteInner_def Write_def
  MemReturn_def RNext_def

lemmas UM_action_defs = RM_action_defs MemFail_def UNext_def

lemmas RM_temp_defs = RPSpec_def MSpec_def IRSpec_def
lemmas UM_temp_defs = UPSpec_def MSpec_def IUSpec_def


(* The reliable memory is an implementation of the unreliable one *)
lemma ReliableImplementsUnReliable: "|- IRSpec ch mm rs --> IUSpec ch mm rs"
  by (force simp: UNext_def UPSpec_def IUSpec_def RM_temp_defs elim!: STL4E [temp_use] squareE)

(* The memory spec implies the memory invariant *)
lemma MemoryInvariant: "|- MSpec ch mm rs l --> [](MemInv mm l)"
  by (tactic {* auto_inv_tac
    (@{simpset} addsimps (@{thms RM_temp_defs} @ @{thms RM_action_defs})) 1 *})

(* The invariant is trivial for non-locations *)
lemma NonMemLocInvariant: "|- #l ~: #MemLoc --> [](MemInv mm l)"
  by (auto simp: MemInv_def intro!: necT [temp_use])

lemma MemoryInvariantAll:
    "|- (ALL l. #l : #MemLoc --> MSpec ch mm rs l) --> (ALL l. [](MemInv mm l))"
  apply clarify
  apply (auto elim!: MemoryInvariant [temp_use] NonMemLocInvariant [temp_use])
  done

(* The memory engages in an action for process p only if there is an
   unanswered call from p.
   We need this only for the reliable memory.
*)

lemma Memoryidle: "|- ~$(Calling ch p) --> ~ RNext ch mm rs p"
  by (auto simp: Return_def RM_action_defs)

(* Enabledness conditions *)

lemma MemReturn_change: "|- MemReturn ch rs p --> <MemReturn ch rs p>_(rtrner ch ! p, rs!p)"
  by (force simp: MemReturn_def angle_def)

lemma MemReturn_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==>
      |- Calling ch p & (rs!p ~= #NotAResult)
         --> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
  apply (tactic
    {* action_simp_tac @{simpset} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1 *})
  apply (tactic
    {* action_simp_tac (@{simpset} addsimps [@{thm MemReturn_def}, @{thm Return_def},
      @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
  done

lemma ReadInner_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==>
      |- Calling ch p & (arg<ch!p> = #(read l)) --> Enabled (ReadInner ch mm rs p l)"
  apply (case_tac "l : MemLoc")
  apply (force simp: ReadInner_def GoodRead_def BadRead_def RdRequest_def
    intro!: exI elim!: base_enabled [temp_use])+
  done

lemma WriteInner_enabled: "!!p. basevars (mm!l, rtrner ch ! p, rs!p) ==>
      |- Calling ch p & (arg<ch!p> = #(write l v))
         --> Enabled (WriteInner ch mm rs p l v)"
  apply (case_tac "l:MemLoc & v:MemVal")
  apply (force simp: WriteInner_def GoodWrite_def BadWrite_def WrRequest_def
    intro!: exI elim!: base_enabled [temp_use])+
  done

lemma ReadResult: "|- Read ch mm rs p & (!l. $(MemInv mm l)) --> (rs!p)` ~= #NotAResult"
  by (force simp: Read_def ReadInner_def GoodRead_def BadRead_def MemInv_def)

lemma WriteResult: "|- Write ch mm rs p l --> (rs!p)` ~= #NotAResult"
  by (auto simp: Write_def WriteInner_def GoodWrite_def BadWrite_def)

lemma ReturnNotReadWrite: "|- (ALL l. $MemInv mm l) & MemReturn ch rs p
         --> ~ Read ch mm rs p & (ALL l. ~ Write ch mm rs p l)"
  by (auto simp: MemReturn_def dest!: WriteResult [temp_use] ReadResult [temp_use])

lemma RWRNext_enabled: "|- (rs!p = #NotAResult) & (!l. MemInv mm l)
         & Enabled (Read ch mm rs p | (? l. Write ch mm rs p l))
         --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
  by (force simp: RNext_def angle_def elim!: enabled_mono2
    dest: ReadResult [temp_use] WriteResult [temp_use])


(* Combine previous lemmas: the memory can make a visible step if there is an
   outstanding call for which no result has been produced.
*)
lemma RNext_enabled: "!!p. !l. basevars (mm!l, rtrner ch!p, rs!p) ==>
      |- (rs!p = #NotAResult) & Calling ch p & (!l. MemInv mm l)
         --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
  apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
  apply (case_tac "arg (ch w p)")
   apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm Read_def},
     temp_rewrite @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
   apply (force dest: base_pair [temp_use])
  apply (erule contrapos_np)
  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm Write_def},
    temp_rewrite @{thm enabled_ex}])
    [@{thm WriteInner_enabled}, exI] [] 1 *})
  done

end