(define-fun initial () State
  (state zeros zeros slots slots slots emptypositions emptyqueues unseen slots))

(define-fun pc ((s State) (t Index)) Index
  (at (counters s) t))

(define-fun reg ((s State) (t Index) (r Index)) Word
  (at (registers s) (bvadd (bvmul #x08 t) r)))

(define-fun pending ((s State) (t Index)) Index
  (bvsub (at (tails s) t) (at (heads s) t)))

(define-fun read ((s State) (t Index) (a Index)) Word
  (let ((index (at (at (positions s) t) a)))
    (ite (and (bvuge index (at (heads s) t))
              (bvult index (at (tails s) t)))
      (at (at (values s) t) (bvand index #x07))
      (at (memory s) a))))

(define-fun advance ((s State) (t Index) (p Index)) State
  (state (memory s) (registers s) (update (counters s) t p)
    (heads s) (tails s) (addresses s) (values s) (positions s) (critical s)))

(define-fun put ((s State) (t Index) (r Index) (v Word)) State
  (state (memory s) (update (registers s) (bvadd (bvmul #x08 t) r) v)
    (counters s) (heads s) (tails s)
    (addresses s) (values s) (positions s) (critical s)))

(define-fun write ((s State) (t Index) (a Index) (v Word)) State
  (let ((index (at (tails s) t)))
    (state (memory s) (registers s) (counters s) (heads s)
      (update (tails s) t (bvadd index #x01))
      (update (addresses s) t (update (at (addresses s) t) (bvand index #x07) a))
      (update (values s) t (update (at (values s) t) (bvand index #x07) v))
      (update (positions s) t (update (at (positions s) t) a index))
      (critical s))))

(define-fun drain ((s State) (t Index)) State
  (let ((index (at (heads s) t)))
    (state
      (update (memory s)
        (at (at (addresses s) t) (bvand index #x07))
        (at (at (values s) t) (bvand index #x07)))
      (registers s) (counters s)
      (update (heads s) t (bvadd index #x01)) (tails s)
      (addresses s) (values s) (positions s) (critical s))))

(define-fun mark ((s State) (t Index) (v Index)) State
  (state (memory s) (registers s) (counters s)
    (heads s) (tails s) (addresses s) (values s) (positions s)
    (update (critical s) t v)))

(define-fun exchange ((s State) (t Index) (a Index) (r Index) (v Word)) State
  (state (update (memory s) a v)
    (update (registers s) (bvadd (bvmul #x08 t) r) (at (memory s) a))
    (counters s) (heads s) (tails s)
    (addresses s) (values s) (positions s) (critical s)))

(define-fun store-step ((s State) (t Index) (a Index) (v Word) (sc Bool)) State
  (let ((next (write s t a v)))
    (advance (ite sc (drain next t) next) t (bvadd (pc s t) #x01))))

(define-fun load-step ((s State) (t Index) (a Index) (r Index)) State
  (advance (put s t r (read s t a)) t (bvadd (pc s t) #x01)))

(define-fun fence-step ((s State) (t Index)) State
  (advance s t (bvadd (pc s t) #x01)))

(define-fun move-step ((s State) (t Index) (r Index) (v Word)) State
  (advance (put s t r v) t (bvadd (pc s t) #x01)))

(define-fun branch-step
  ((s State) (t Index) (r Index) (v Word) (target Index)) State
  (advance s t (ite (= (reg s t r) v) target (bvadd (pc s t) #x01))))

(define-fun enter-step ((s State) (t Index)) State
  (advance (mark s t #x01) t (bvadd (pc s t) #x01)))

(define-fun leave-step ((s State) (t Index)) State
  (advance (mark s t #x00) t (bvadd (pc s t) #x01)))

(define-fun exchange-step
  ((s State) (t Index) (a Index) (r Index) (v Word)) State
  (advance (exchange s t a r v) t (bvadd (pc s t) #x01)))

(define-fun overlap ((s State)) Bool
  (and (= (at (critical s) #x00) #x01)
       (= (at (critical s) #x01) #x01)))