#lang ivy1.6

include shard
include table
include key

type value

instance shard : table_shard(key,value)
instance tab : hash_table(key,value,shard)

object impl = {
    interpret value -> bv[4]
    interpret key.t -> bv[4]
}

export tab.set
export tab.get
export tab.extract_
export tab.incorporate

isolate iso_tab = tab with tab,shard,key
isolate iso_key = key


extract iso_impl = tab,shard,key,impl

trusted isolate iso_test = tab with shard,key,impl