src/HOL/TLA/Memory/Memory.thy

A formalization of TLA in HOL -- by Stephan Merz;

(*
    File:        Memory.thy
    Author:      Stephan Merz
    Copyright:   1997 University of Munich

    Theory Name: Memory
    Logic Image: TLA

    RPC-Memory example: Memory specification
*)

Memory = MemoryParameters + ProcedureInterface +

types
  memChType  = "(memArgType,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"

rules
  MInit_def         "$(MInit mm l) .= ($(mm@l) .= # InitVal)"
  PInit_def         "$(PInit rs p) .= ($(rs@p) .= # NotAResult)"

  RdRequest_def     "$(RdRequest ch p l) .= 
                         ($(Calling ch p) .& (arg[$(ch@p)] .= #(Inl (read,l))))"
  WrRequest_def     "$(WrRequest ch p l v) .=
                         ($(Calling ch p) .& (arg[$(ch@p)] .= #(Inr (write,l,v))))"
  (* a read that doesn't raise BadArg *)
  GoodRead_def      "GoodRead mm rs p l ==
                        #(MemLoc l) .& (rs@p)$ .= $(mm@l)"
  (* a read that raises BadArg *)
  BadRead_def       "BadRead mm rs p l ==
                        .~ #(MemLoc l) .& (rs@p)$ .= #BadArg"
  (* the read action with l visible *)
  ReadInner_def     "ReadInner ch mm rs p l ==
                         $(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 == REX l. ReadInner ch mm rs p l"

  (* similar definitions for the write action *)
  GoodWrite_def     "GoodWrite mm rs p l v ==
                        #(MemLoc l) .& #(MemVal v) 
                        .& (mm@l)$ .= #v .& (rs@p)$ .= #OK"
  BadWrite_def      "BadWrite mm rs p l v ==
                        .~ (#(MemLoc l) .& #(MemVal v))
                        .& (rs@p)$ .= #BadArg .& unchanged (mm@l)"
  WriteInner_def    "WriteInner ch mm rs p l v ==
                        $(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 == REX v. WriteInner ch mm rs p l v"

  (* the return action *)
  MemReturn_def     "MemReturn ch rs p ==
                        $(rs@p) .~= #NotAResult
                        .& (rs@p)$ .= #NotAResult
                        .& Return ch p ($(rs@p))"
  (* the failure action of the unreliable memory *)
  MemFail_def       "MemFail ch rs p ==
                        $(Calling ch p)
                        .& (rs@p)$ .= #MemFailure
                        .& unchanged (rtrner ch @ p)"
  RNext_def         "RNext ch mm rs p ==
                        Read ch mm rs p
                        .| (REX l. Write ch mm rs p l)
                        .| MemReturn ch rs p"
  UNext_def         "UNext ch mm rs p ==
                        RNext ch mm rs p .| MemFail ch rs p"

  RPSpec_def        "RPSpec ch mm rs p ==
                        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 ==
                        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 ==
                        Init($(MInit mm l))
                        .& [][ REX p. Write ch mm rs p l ]_(mm@l)"
  IRSpec_def        "IRSpec ch mm rs ==
                        (RALL p. RPSpec ch mm rs p)
                        .& (RALL l. #(MemLoc l) .-> MSpec ch mm rs l)"
  IUSpec_def        "IUSpec ch mm rs ==
                        (RALL p. UPSpec ch mm rs p)
                        .& (RALL l. #(MemLoc l) .-> MSpec ch mm rs l)"

  RSpec_def         "RSpec ch rs == EEX mm. IRSpec ch mm rs"
  USpec_def         "USpec ch == EEX mm rs. IUSpec ch mm rs"

  MemInv_def        "$(MemInv mm l) .=
                        (#(MemLoc l) .-> MemVal[ $(mm@l)])"
end