Sht

include proto
include reference
include key
include trans
include udp
include shard
include seq_num

type id
type data


instance r : sht_reference(id,key,data)
instance s : table_shard(key.t,data)
instance n: sequence_numbers
instance p(X:id) : sht_protocol(X,r,t,id,key,data,s)
instance t : net(u,p.req.t,s.t,n,data)
instance u : udp_simple(id,t.net_msg.t)

isolate iso_key = key.impl with key
isolate iso_s = s.impl with s,key
isolate iso_n = n.impl with n
isolate iso_t = t.impl with t,u,n
isolate iso_p = p.impl with p,r,t,key,s
isolate iso_dm(me:id) = p.impl.dm.impl(me) with p.impl.dm(me), key
isolate iso_hash(me:id) = p.impl.hash.impl(me) with p.impl.hash(me),key,s

export p.set
export p.get
export p.delegate_
import p.answer

object impl = {
    interpret id -> bv[1]
    interpret t.impl.mq.impl.range -> bv[3]
}

object debug = {
    action send(dst:id,m:t.net_msg.t)
    action recv(dts:id,m:t.net_msg.t)
    before u.send {
    call send(dst,v)
    }
    before u.recv{
    call recv(dst,v)
    }
}
import debug.send
import debug.recv

extract iso_impl(me:id) = key.impl,key.iter,s,n.impl,t.impl(me),p.impl(me),u.impl(me)