theory CXLMEM3 imports Main
begin
(* memory as finite association list: still code_pred has difficulty showing inductive relations between two states in a transition,
  we therefore revert to a different representation for ext/internal transitions*)

type_synonym mem = "(nat * int) list"

fun read_mem :: "mem ⇒ nat ⇒ int" where
  "read_mem [] i = 0"
| "read_mem ((j,v)#xs) i = (if i = j then v else read_mem xs i)"

fun write_mem :: "mem ⇒ nat ⇒ int ⇒ mem" where
  "write_mem [] i v = [(i, v)]"
| "write_mem ((j,w)#xs) i v = (if i = j then (i, v)#xs else (j, w)#write_mem xs i v)"

type_synonym txid = nat

datatype Memop = Read nat | Write nat int

datatype Memop_res = RdRes txid nat int | WrRes txid nat int | Pending txid Memop

fun perform_Memop :: "Memop ⇒ mem ⇒ (mem * int)" where
  "perform_Memop (Read i) m = (m, read_mem m i)"
| "perform_Memop (Write i v) m = (write_mem m i v, v)"

datatype Req = MemRd txid nat

datatype DRS = MemData txid int

datatype Rwd = MemWrite txid nat int

datatype NDR = Cmp txid

datatype mem_msg = ReqMsg Req | RwdMsg Rwd | BIRsp | NDRMsg NDR | DRSMsg DRS  | BISnp

fun get_op_addr :: "mem_msg ⇒ nat" where
  "get_op_addr m = (case m of (ReqMsg (MemRd txk i)) ⇒ i | _ ⇒ 0)"

record cxl_state =
  memory :: "mem"
  m2sreqs :: "Req list"
  m2srwds :: "Rwd list"
  s2mdrss :: "DRS list"
  s2mndrs :: "NDR list"
  counter :: nat

(* Transitions over tupled state for executability *)

inductive  external_step :: "(mem * Req list * Rwd list * DRS list * NDR list * nat * Memop list * Memop_res list)  ⇒ (mem * Req list * Rwd list * DRS list * NDR list * nat * Memop list * Memop_res list) ⇒ bool"
  (infix "↝e" 50)
  where
    read_to_memread:"(m, reqs, rwds, drss, ndrs, cnt, Read i # mops, mress) ↝e (m, MemRd cnt i # reqs, rwds, drss, ndrs, cnt+1, mops, Pending cnt (Read i) # mress)"
  | write_to_memwrite: "(m, reqs, rwds, drss, ndrs, cnt, Write i v # mops, mress) ↝e (m, reqs, MemWrite cnt i v # rwds, drss, ndrs, cnt+1, mops, Pending cnt (Write i v) # mress)"
  | write_cmp: "(m, reqs, rwds, drss, ndrs1 @ [Cmp txid] @ ndrs2, cnt, mops, mress1 @ [Pending txid (Write i v)] @ mress2) ↝e (m, reqs, rwds, drss, ndrs1@ndrs2, cnt, mops, WrRes txid i v # mress1 @ mress2)"
  | read_memdata: "(m, reqs, rwds, drss1 @ [MemData txid v] @ drss2, ndrss, cnt, mops, mress1 @ [Pending txid (Read i)] @ mress2) ↝e (m, reqs, rwds, drss1 @ drss2, ndrss, cnt, mops, RdRes txid i v # mress1 @ mress2)"


inductive internal_step :: "(mem * Req list * Rwd list * DRS list * NDR list * nat * Memop list * Memop_res list)  ⇒ (mem * Req list * Rwd list * DRS list * NDR list * nat * Memop list * Memop_res list) ⇒ bool"
  (infix "↝i" 50)
  where
    "(m, reqs1 @ [MemRd txid i] @ reqs2, rwds, drss, ndrs, cnt, mops, mress) ↝i (m, reqs1 @ reqs2, rwds, MemData txid (read_mem m i) # drss, ndrs, cnt, mops, mress)"
  | "(m, reqs, rwds1 @ [MemWrite txid i v] @ rwds2, drss, ndrs, cnt, mops, mress) ↝i (write_mem m i v, reqs, rwds1 @ rwds2, drss, Cmp txid # ndrs, cnt, mops, mress)"

inductive system_step :: "(mem * Req list * Rwd list * DRS list * NDR list * nat * Memop list * Memop_res list)  ⇒ (mem * Req list * Rwd list * DRS list * NDR list * nat * Memop list * Memop_res list) ⇒ bool"
  (infix "↝" 50)
  where
    "tuple1 ↝e tuple2 ⟹ tuple1 ↝ tuple2"
  | "tuple1 ↝i tuple2 ⟹ tuple1 ↝ tuple2"

definition mem3_42 :: "mem" where "mem3_42 = write_mem [] 3 42"

definition initial1 :: "mem * Req list * Rwd list * DRS list * NDR list * nat * Memop list * Memop_res list"
  where "initial1 = (mem3_42, [], [], [], [], 15, [Read 3], [])"


code_pred system_step .

values {x. initial1 ↝ x}

thm system_step.equation

Outer syntax error⌂: command expected,
but identifier initial1⌂ was found