class AtomicReads_Rewrite
  include Bud

  state do
    table :commit, [:batch]
    scratch :del_commit_r0, [:batch]
    scratch :del_write_r0, [:wid] => [:batch, :name, :val]
    table :dom, [:wid]
    scratch :live, [:wid] => [:batch, :name, :val, :prev_wid]
    scratch :r0_write_commit_joinbuf, [:write_wid, :write_batch, :write_name, :write_val, :commit_batch]
    scratch :r0_write_commit_missing, [:write_wid, :write_batch, :write_name, :write_val, :commit_batch]
    table :read, [:batch]
    range :read_commit, [:batch]
    scratch :read_event, [:batch]
    scratch :read_view, [:effective, :wid, :batch, :name, :val, :prev_wid]
    range :seal_commit, [:ignored]
    range :seal_commit_batch, [:batch]
    range :seal_write, [:ignored]
    range :seal_write_batch, [:batch]
    table :snapshot, [:effective, :wid, :batch, :name, :val, :prev_wid]
    range :snapshot_exists, [:batch]
    table :write, [:wid] => [:batch, :name, :val]
    scratch :write_commit_event, [:wid] => [:batch, :name, :val]
    table :write_log, [:wid] => [:batch, :name, :val, :prev_wid]
    range :write_log_keys, [:wid]
  end

  bloom do
    (commit < -del_commit_r0)
    (dom < -(dom * write_log_keys).lefts(:wid => :wid).notin(write_log, :wid => :wid))
    (read < -(read * snapshot_exists).lefts(:batch => :batch))
    (snapshot < -(snapshot * read_commit).lefts(:effective => :batch))
    (write < -del_write_r0)
    (write_log < +(write_commit_event * live).outer(:name => :name) do |e, l|
  (e + [l.wid.nil? ? (0) : (l.wid)])
end.notin(write_log_keys, 0 => :wid))
    (write_log < -(write_log * dom).lefts(:wid => :wid))
    del_commit_r0 <= (commit * seal_write).lefts.notin(r0_write_commit_missing, :batch => :commit_batch)
    del_commit_r0 <= (commit * seal_write_batch).lefts(:batch => :batch).notin(r0_write_commit_missing, :batch => :commit_batch)
    del_write_r0 <= (write * commit).lefts(:batch => :batch).notin(r0_write_commit_missing, :wid => :write_wid, :batch => :write_batch, :name => :write_name, :val => :write_val)
    del_write_r0 <= (write * seal_commit).lefts.notin(r0_write_commit_missing, :wid => :write_wid, :batch => :write_batch, :name => :write_name, :val => :write_val)
    del_write_r0 <= (write * seal_commit_batch).lefts(:batch => :batch).notin(r0_write_commit_missing, :wid => :write_wid, :batch => :write_batch, :name => :write_name, :val => :write_val)
    del_write_r0 <= (write * write_log).lefts(:wid => :wid)
    dom <= (write_log { |l| [l.prev_wid] })
    live <= (write_log.notin(dom, :wid => :wid))
    r0_write_commit_joinbuf <= (write * commit * write_log).combos(write.batch => commit.batch, write_log.wid => write.wid) {|x,y,z| x + y}
    r0_write_commit_missing <= (write * commit).pairs(write.batch => commit.batch) {|x,y| x + y}.notin(r0_write_commit_joinbuf)
    read_event <= (read.notin(snapshot_exists, :batch => :batch))
    read_view <= (snapshot.notin(read_commit, :effective => :batch))
    snapshot < (+(read_event * live).pairs { |r, l| (r + l) })
    snapshot_exists <= (snapshot { |r| [r.effective] })
    write_commit_event <= ((write * commit).lefts(:batch => :batch).notin(write_log, 0 => :wid))
    write_log_keys <+ write_log {|r| [r.wid]}
  end
end