class CausalKvsReplica_Rewrite
  include Bud

  state do
    scratch :del_dep_r4, [:id, :target]
    scratch :del_log_r0, [:id] => [:key, :val, :deps]
    scratch :del_log_r3, [:id] => [:key, :val, :deps]
    scratch :del_read_resp_r11, [:addr, :id, :key, :val]
    scratch :del_read_resp_r16, [:addr, :id, :key, :val]
    scratch :del_safe_dep_r8, [:target, :src_key]
    scratch :del_safe_r8, [:id] => [:key, :val]
    scratch :del_safe_r9, [:id] => [:key, :val]
    table :dep, [:id, :target]
    table :dom, [:id]
    table :log, [:id] => [:key, :val, :deps]
    channel :log_chn, [:@addr, :id] => [:key, :val, :deps]
    channel :log_chn_ack, [:@rce_sender, :addr, :id]
    range :log_chn_approx, [:addr, :id]
    scratch :missing_dep, [:id, :target]
    scratch :missing_read_dep, [:id, :target]
    sealed :node, [:addr]
    scratch :pending, [:id] => [:key, :val, :deps]
    scratch :r0_node_log_joinbuf, [:node_addr, :log_id, :log_key, :log_val, :log_deps]
    scratch :r0_node_log_missing, [:node_addr, :log_id, :log_key, :log_val, :log_deps]
    scratch :r8_safe_dep_safe_joinbuf, [:safe_dep_target, :safe_dep_src_key, :safe_id, :safe_key, :safe_val]
    scratch :r8_safe_dep_safe_missing, [:safe_dep_target, :safe_dep_src_key, :safe_id, :safe_key, :safe_val]
    table :read_buf, [:id] => [:key, :deps, :src_addr]
    range :read_buf_keys, [:id]
    scratch :read_dep, [:id, :target]
    scratch :read_pending, [:id] => [:key, :deps, :src_addr]
    table :read_req, [:addr, :id] => [:key, :deps]
    table :read_resp, [:addr, :id, :key, :val]
    table :read_result, [:addr, :id, :key, :val]
    channel :req_chn, [:@addr, :id] => [:key, :deps]
    channel :req_chn_ack, [:@rce_sender, :addr, :id]
    range :req_chn_approx, [:addr, :id]
    channel :resp_chn, [:@addr, :id, :key, :val]
    channel :resp_chn_ack, [:@rce_sender, :addr, :id, :key, :val]
    range :resp_chn_approx, [:addr, :id, :key, :val]
    scratch :rse_ready_safe, [:id] => [:key, :val]
    table :safe, [:id] => [:key, :val]
    table :safe_dep, [:target, :src_key]
    range :safe_keys, [:id]
    scratch :safe_read, [:id] => [:key, :deps, :src_addr]
    range :seal_dep, [:ignored]
    range :seal_dep_id, [:id]
    scratch :seal_done_dep_safe, [:id, :target]
    scratch :seal_done_safe_dep, [:id] => [:key, :val]
    range :seal_log, [:ignored]
    range :seal_node, [:ignored]
    range :seal_safe, [:ignored]
    range :seal_safe_dep, [:ignored]
    range :seal_safe_dep_src_key, [:src_key]
    range :seal_safe_dep_target, [:target]
    range :seal_safe_id, [:id]
    range :seal_safe_key, [:key]
    scratch :view, [:id] => [:key, :val]
  end

  bloom do
    (dom < -(dom * safe_keys).lefts(:id => :id).notin(safe, :id => :id))
    (log < -(del_log_r0 * del_log_r3).matches { |t0, t1| t0 })
    (log_chn < (node * log).pairs { |n, l| (n + l) }.notin(log_chn_approx, 0 => :addr, 1 => :id).~)
    (node < -(node * seal_log).lefts.notin(r0_node_log_missing, :addr => :node_addr))
    (read_buf < -(read_buf * read_resp).lefts(:id => :id))
    (read_buf <= req_chn { |r| [r.id, r.key, r.deps, r.source_addr] }.notin(read_buf_keys, 0 => :id))
    (read_req < -(read_req * req_chn_approx).lefts(0 => :addr, 1 => :id))
    (read_resp < -(del_read_resp_r11 * del_read_resp_r16).matches { |t0, t1| t0 })
    (req_chn < read_req.notin(req_chn_approx, 0 => :addr, 1 => :id).~)
    (resp_chn < read_resp.notin(resp_chn_approx, 0 => :addr, 1 => :id, 2 => :key, 3 => :val).~)
    (safe < +pending.notin(missing_dep, 0 => :id).pro { |p| [p.id, p.key, p.val] }.notin(safe_keys, 0 => :id))
    (safe_dep < -del_safe_dep_r8)
    (seal_done_dep_safe <= (del_dep_r4 * safe_keys).lefts(:id => :id))
    (seal_done_dep_safe <= (del_dep_r4 * seal_safe).lefts)
    (seal_done_dep_safe <= (del_dep_r4 * seal_safe_id).lefts(:id => :id))
    del_dep_r4 <= (dep * safe_keys).lefts(:target => :id)
    del_log_r0 <= (log * seal_node).lefts.notin(r0_node_log_missing, :id => :log_id, :key => :log_key, :val => :log_val, :deps => :log_deps)
    del_log_r3 <= (log * safe_keys).lefts(:id => :id)
    del_read_resp_r11 <= ((read_resp * read_buf_keys).lefts(:id => :id)).notin(read_buf, :id => :id)
    del_read_resp_r16 <= (read_resp * resp_chn_approx).lefts(0 => :addr, 1 => :id, 2 => :key, 3 => :val)
    del_safe_dep_r8 <= (safe_dep * dom).lefts(:target => :id)
    del_safe_dep_r8 <= (safe_dep * safe_keys).lefts(:target => :id).notin(r8_safe_dep_safe_missing, :target => :safe_dep_target, :src_key => :safe_dep_src_key)
    del_safe_dep_r8 <= (safe_dep * seal_safe).lefts.notin(r8_safe_dep_safe_missing, :target => :safe_dep_target, :src_key => :safe_dep_src_key)
    del_safe_dep_r8 <= (safe_dep * seal_safe_id).lefts(:target => :id).notin(r8_safe_dep_safe_missing, :target => :safe_dep_target, :src_key => :safe_dep_src_key)
    del_safe_dep_r8 <= (safe_dep * seal_safe_key).lefts(:src_key => :key).notin(r8_safe_dep_safe_missing, :target => :safe_dep_target, :src_key => :safe_dep_src_key)
    del_safe_r8 <= (safe * dom).lefts(:id => :id)
    del_safe_r8 <= (safe * safe_dep).lefts(:id => :target, :key => :src_key).notin(r8_safe_dep_safe_missing, :id => :safe_id, :key => :safe_key, :val => :safe_val)
    del_safe_r8 <= (safe * seal_safe_dep).lefts.notin(r8_safe_dep_safe_missing, :id => :safe_id, :key => :safe_key, :val => :safe_val)
    del_safe_r8 <= (safe * seal_safe_dep_src_key).lefts(:key => :src_key).notin(r8_safe_dep_safe_missing, :id => :safe_id, :key => :safe_key, :val => :safe_val)
    del_safe_r8 <= (safe * seal_safe_dep_target).lefts(:id => :target).notin(r8_safe_dep_safe_missing, :id => :safe_id, :key => :safe_key, :val => :safe_val)
    del_safe_r9 <= (safe * dom).lefts(:id => :id)
    dep <- seal_done_dep_safe
    dep <= (log.flat_map { |l| l.deps.pro { |d| [l.id, d] } })
    dom < (+(safe_dep * safe).lefts(:target => :id, :src_key => :key) { |d| [d.target] }.notin(dom, 0 => :id))
    log <= (log_chn.payloads)
    log_chn_ack <~ log_chn {|c| [c.source_addr, c.addr, c.id]}
    log_chn_approx <= (log_chn_ack.payloads)
    missing_dep <= (dep.notin(safe_keys, :target => :id))
    missing_read_dep <= (read_dep.notin(safe_keys, :target => :id))
    pending <= (log.notin(safe_keys, :id => :id))
    r0_node_log_joinbuf <= (node * log * log_chn_approx).combos(log_chn_approx.addr => node.addr, log_chn_approx.id => log.id) {|x,y,z| x + y}
    r0_node_log_missing <= (node * log).pairs {|x,y| x + y}.notin(r0_node_log_joinbuf)
    r8_safe_dep_safe_joinbuf <= (safe_dep * safe * dom).combos(safe_dep.target => safe.id, safe_dep.src_key => safe.key, dom.id => safe_dep.target) {|x,y,z| x + y}
    r8_safe_dep_safe_missing <= (safe_dep * safe).pairs(safe_dep.target => safe.id, safe_dep.src_key => safe.key) {|x,y| x + y}.notin(r8_safe_dep_safe_joinbuf)
    read_buf_keys <+ read_buf {|r| [r.id]}
    read_dep <= (read_pending.flat_map { |r| r.deps.pro { |d| [r.id, d] } })
    read_pending <= (read_buf.notin(read_resp, :id => :id))
    read_resp <= ((safe_read * view).pairs(:key => :key) do |r, v|
  [r.src_addr, r.id, r.key, v.val]
end)
    read_result <= (resp_chn)
    req_chn_ack <~ req_chn {|c| [c.source_addr, c.addr, c.id]}
    req_chn_approx <= (req_chn_ack.payloads)
    resp_chn_ack <~ resp_chn {|c| [c.source_addr, c.addr, c.id, c.key, c.val]}
    resp_chn_approx <= (resp_chn_ack.payloads)
    rse_ready_safe <= (del_safe_r8 * del_safe_r9).matches {|t0,t1| t0}
    safe <- seal_done_safe_dep
    safe_dep <= ((dep * safe).pairs(:id => :id) { |d, s| [d.target, s.key] })
    safe_keys <= (safe { |s| [s.id] })
    safe_read < (+read_pending.notin(missing_read_dep, 0 => :id))
    seal_dep_id <= log {|x| [x.id]}
    seal_done_safe_dep <= (rse_ready_safe * seal_dep).lefts
    seal_done_safe_dep <= (seal_dep_id * rse_ready_safe).rights(:id => :id)
    view <= (safe.notin(dom, :id => :id))
  end
end