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

section ‹RPC-Memory example: Memory specification›

theory Memory
imports MemoryParameters ProcedureInterface
begin

type_synonym memChType = "(memOp, Vals) channel"
type_synonym memType = "(Locs → Vals) stfun"  (* intention: MemLocs \<Rightarrow> MemVals *)
type_synonym resType = "(PrIds → Vals) stfun"


(* state predicates *)

definition MInit :: "memType → Locs → stpred"
  where "MInit mm l == PRED mm!l = #InitVal"

definition PInit :: "resType → PrIds → stpred"
  where "PInit rs p == PRED rs!p = #NotAResult"


(* auxiliary predicates: is there a pending read/write request for
   some process id and location/value? *)

definition RdRequest :: "memChType → PrIds → Locs → stpred"
  where "RdRequest ch p l == PRED Calling ch p ∧ (arg<ch!p> = #(read l))"

definition WrRequest :: "memChType → PrIds → Locs → Vals → stpred"
  where "WrRequest ch p l v == PRED Calling ch p ∧ (arg<ch!p> = #(write l v))"


(* actions *)

(* a read that doesn't raise BadArg *)
definition GoodRead :: "memType → resType → PrIds → Locs → action"
  where "GoodRead mm rs p l == ACT #l ∈ #MemLoc ∧ ((rs!p)$ = $(mm!l))"

(* a read that raises BadArg *)
definition BadRead :: "memType → resType → PrIds → Locs → action"
  where "BadRead mm rs p l == ACT #l ∉ #MemLoc ∧ ((rs!p)$ = #BadArg)"

(* the read action with l visible *)
definition ReadInner :: "memChType → memType → resType → PrIds → Locs → action"
  where "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 *)
definition Read :: "memChType → memType → resType → PrIds → action"
  where "Read ch mm rs p == ACT (∃l. ReadInner ch mm rs p l)"

(* similar definitions for the write action *)
definition GoodWrite :: "memType → resType → PrIds → Locs → Vals → action"
  where "GoodWrite mm rs p l v ==
    ACT #l ∈ #MemLoc ∧ #v ∈ #MemVal
      ∧ ((mm!l)$ = #v) ∧ ((rs!p)$ = #OK)"

definition BadWrite :: "memType → resType → PrIds → Locs → Vals → action"
  where "BadWrite mm rs p l v == ACT
    ¬ (#l ∈ #MemLoc ∧ #v ∈ #MemVal)
    ∧ ((rs!p)$ = #BadArg) ∧ unchanged (mm!l)"

definition WriteInner :: "memChType → memType → resType → PrIds → Locs → Vals → action"
  where "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)"

definition Write :: "memChType → memType → resType → PrIds → Locs → action"
  where "Write ch mm rs p l == ACT (∃v. WriteInner ch mm rs p l v)"


(* the return action *)
definition MemReturn :: "memChType → resType → PrIds → action"
  where "MemReturn ch rs p == ACT
   ( ($(rs!p) ≠ #NotAResult)
    ∧ ((rs!p)$ = #NotAResult)
    ∧ Return ch p (rs!p))"

(* the failure action of the unreliable memory *)
definition MemFail :: "memChType → resType → PrIds → action"
  where "MemFail ch rs p == ACT
    $(Calling ch p)
    ∧ ((rs!p)$ = #MemFailure)
    ∧ unchanged (rtrner ch ! p)"

(* next-state relations for reliable / unreliable memory *)
definition RNext :: "memChType → memType → resType → PrIds → action"
  where "RNext ch mm rs p == ACT
   ( Read ch mm rs p
    ∨ (∃l. Write ch mm rs p l)
    ∨ MemReturn ch rs p)"

definition UNext :: "memChType → memType → resType → PrIds → action"
  where "UNext ch mm rs p == ACT (RNext ch mm rs p ∨ MemFail ch rs p)"


(* temporal formulas *)

definition RPSpec :: "memChType → memType → resType → PrIds → temporal"
  where "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)"

definition UPSpec :: "memChType → memType → resType → PrIds → temporal"
  where "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)"

definition MSpec :: "memChType → memType → resType → Locs → temporal"
  where "MSpec ch mm rs l == TEMP
    Init(MInit mm l)
    ∧ ◻[ ∃p. Write ch mm rs p l ]_(mm!l)"

definition IRSpec :: "memChType → memType → resType → temporal"
  where "IRSpec ch mm rs == TEMP
    (∀p. RPSpec ch mm rs p)
    ∧ (∀l. #l ∈ #MemLoc ⟶ MSpec ch mm rs l)"

definition IUSpec :: "memChType → memType → resType → temporal"
  where "IUSpec ch mm rs == TEMP
    (∀p. UPSpec ch mm rs p)
    ∧ (∀l. #l ∈ #MemLoc ⟶ MSpec ch mm rs l)"

definition RSpec :: "memChType → resType → temporal"
  where "RSpec ch rs == TEMP (∃∃mm. IRSpec ch mm rs)"

definition USpec :: "memChType → temporal"
  where "USpec ch == TEMP (∃∃mm rs. IUSpec ch mm rs)"

(* 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. *)
definition MemInv :: "memType → Locs → stpred"
  where "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 (auto_invariant simp: RM_temp_defs RM_action_defs)

(* 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:
    "⊨ (∀l. #l ∈ #MemLoc ⟶ MSpec ch mm rs l) ⟶ (∀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: AReturn_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 context [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1›)
  apply (tactic
    ‹action_simp_tac (context addsimps [@{thm MemReturn_def}, @{thm AReturn_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: "⊨ (∀l. $MemInv mm l) ∧ MemReturn ch rs p
         ⟶ ¬ Read ch mm rs p ∧ (∀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 (context addsimps [@{thm Read_def},
 temp_rewrite context @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1›)
   apply (force dest: base_pair [temp_use])
  apply (erule contrapos_np)
  apply (tactic ‹action_simp_tac (context addsimps [@{thm Write_def},
 temp_rewrite context @{thm enabled_ex}])
 [@{thm WriteInner_enabled}, exI] [] 1›)
  done

end