tm [ID: TYPE, ID1: ID]: THEORY   
%lemmas and procedures for verifying transactional memories

 BEGIN

  IMPORTING queue[ID,ID1]

  MEM:   TYPE = ARRAY[ADDRESS -> VALUE] 
  DOOM:  TYPE = ARRAY[ID      -> bool]
  TRANS: TYPE = ARRAY[ID      -> Q] 

  empty_mem:   MEM   = {i: ADDRESS | 0}
  init_doomed: DOOM  = {id: ID | FALSE}
  init_trans:  TRANS = {id: ID | null1}
 
  % === procedures and lemmas

  % get the value that was last written to adr
  % because of simplifying assumption it is mem[adr] 
  get_read_val(adr: ADDRESS, mem: MEM, trans_id: Q): VALUE = mem(adr)

  % check if the read events in q are consistent with mem
  read_events_consistent_with_mem(q: Q, mem: MEM): bool =
    (FORALL (i: posnat): i <= q`size IMPLIES 
       q`entry(i)`act = READ IMPLIES
         q`entry(i)`val = mem(q`entry(i)`adr)) 

  % if q1 is eql to q2 then q1 is consistent with mem iff
  %                         q2 is consistent with mem
  read_events_consistent_with_mem_iff_qs_eql: LEMMA
    FORALL (q1,q2: Q, mem: MEM):
      eql(q1,q2) IMPLIES
      (read_events_consistent_with_mem(q1,mem) IFF
         read_events_consistent_with_mem(q2,mem))

  % adding write/open to a projection doesn't change its
  % consistency with the memory
  adding_some_events_maintain_consistency: AXIOM
    FORALL (q1: Q, mem: MEM, id: ID, e: EVENT):
      (e`act = WRITE OR
       e`act = OPEN) IMPLIES
         (read_events_consistent_with_mem(project(q1)(id),mem) IFF
          read_events_consistent_with_mem(add(e,project(q1)(id)),mem))

  % adding read to a projection doesn't change its
  % consistency with the memory if the new event consistent
  adding_consistent_read_event_maintains_consistency: AXIOM
    FORALL (q1: Q, mem: MEM, id: ID, e: EVENT):
      (e`act = READ AND
       e`val = mem(e`adr)) IMPLIES
         (read_events_consistent_with_mem(project(q1)(id),mem) IFF
          read_events_consistent_with_mem(add(e,project(q1)(id)),mem))

  % update mem according to id's write events in q
  update_mem(mem: MEM, q: Q, id: ID): MEM =
    {i: nat | IF (NOT some(is_write_of_id(id),q)) 
                THEN mem(i)
                ELSE get_latest_write(id,i,reverse(q))
              ENDIF}

  % update mem according to id's write events in q is equal to
  % update mem according to id's write events in project(q)(id)
  q_id_update_mem_imp_proj_q_id_update_mem: AXIOM
    FORALL (q: Q, mem: MEM, id: ID): 
      update_mem(mem,q,id) = update_mem(mem,project(q)(id),id)

  % if q1 eql to q2
  % update mem according to id's write events in q1 is equal to
  % update mem according to id's write events in q2 is equal to
  upade_mem_imp_update_mem_of_eql: AXIOM
    FORALL (q1,q2: Q, mem: MEM, id: ID): 
      eql(q1,q2) IMPLIES 
        update_mem(mem,q1,id) = update_mem(mem,q2,id)

  % update a specific adr in mem
  update_adr(mem: MEM, adr: ADDRESS, val: VALUE): MEM =
    {i: nat | IF (i = adr) 
                THEN val
                ELSE mem(i)
              ENDIF}

  % doom those ids conflicts with commit_id's tr,
  % or already doomed,
  % undoomed commit_id
  doom_others(conflict_resolution: [Q,Q -> bool], 
              commit_id: ID, trans: [ID -> Q], doomed: DOOM): [ID -> bool] =
    (LAMBDA (id: ID): 
          doomed(id)
       OR (id /= commit_id AND
           conflict_resolution(trans(commit_id),trans(id))))

  % true if given event is not of commit_id or if its transaction
  % doesn't conflict with the of commit_id
  not_conflicting_and_not_own_id(conflict_resolution: [Q,Q -> bool], 
                                 commit_id: ID, project_q: [ID -> Q]): [EVENT -> bool] = 
    (LAMBDA (event: EVENT):
       not_of_id(commit_id)(event) AND
       (event`id /= commit_id AND
        NOT conflict_resolution(project_q(commit_id),project_q(event`id))))


  % removes all the events of id
  % removes all the events of clients that their tr conflicts with commit'id's
  fix_q_after_commit(conflict_resolution: [Q,Q -> bool], commit_id: ID, q: Q): Q = 
    projection(not_conflicting_and_not_own_id(conflict_resolution,commit_id,project(q)),q)

  % projectin the q after we fixed it at commit, on the commiting id is empty
  proj_of_id_after_fix_q_after_commit_of_id: AXIOM
    FORALL (q: Q, id: ID, conflict_resolution: [Q,Q -> bool]):
      empty(project(fix_q_after_commit(conflict_resolution,id,q))(id))

  % projectin the q after we fixed it at commit, on any id
  proj_of_id_after_fix_q_after_commit_of_commit_id: AXIOM
    FORALL (q: Q, id, commit_id: ID, conflict_resolution: [Q,Q -> bool]):
      id /= commit_id IMPLIES
        IF conflict_resolution(project(q)(commit_id),project(q)(id))
          THEN empty(project(fix_q_after_commit(conflict_resolution,commit_id,q))(id))
          ELSE eql(project(q)(id),
                   project(fix_q_after_commit(conflict_resolution,commit_id,q))(id))
        ENDIF

  % projectin the q after we fixed it at non-transactional write, on any id
  proj_of_id_after_fix_q_after_nt_write_of_write_id: AXIOM
    FORALL (q: Q, id, nt_write_id: ID, conflict_resolution: [Q,Q -> bool], adr: ADDRESS, val: VALUE):
      id /= nt_write_id IMPLIES
        IF conflict_resolution(project(add_ntwrite(nt_write_id,adr,val,q))(nt_write_id),project(q)(id))
          THEN empty(project(fix_q_after_commit(conflict_resolution,nt_write_id,q))(id))
          ELSE eql(project(q)(id),
                   project(fix_q_after_commit(conflict_resolution,nt_write_id,q))(id))
        ENDIF

  % projectin the q after we fixed it at commit, on any doomed id
  fix_after_others_commit: AXIOM
    FORALL (q: Q, id, commit_id: ID, doomed: DOOM, conflict_resolution: [Q,Q -> bool]):
      IF doomed(id)
        THEN eql(null1, 
                 project(fix_q_after_commit(conflict_resolution,commit_id,q))(id))
        ELSE eql(project(q)(id),
                 project(fix_q_after_commit(conflict_resolution,commit_id,q))(id))
      ENDIF
 
 END tm