Table

include collections

module hash_table(key,value,shard) = {

Interface

Set the value of a key

    action set(k:key.t, v:value)

Get the value of a key

    action get(k:key.t) returns (v:value)

Extract a shard from a hash table

    action extract_(lo:key.t,hi:key.t) returns(res:shard.t)

Incorporates a shard into a hash table

    action incorporate(s:shard.t)

Specification

    function hash(X:key.t) : value
    init hash(X) = 0

    object spec = {
    before set {
        hash(k) := v
    }

    after get {
        assert v = hash(k)
    }

    after extract_ {
        assert shard.lo(res) = lo;
        assert (lo <= hi -> lo <= shard.hi(res)) & shard.hi(res) <= hi;
        assert (shard.lo(res) <= X & X <= shard.hi(res)) -> shard.value(res,X) = hash(X)
    }

    before incorporate(s:shard.t) {
        assert shard.valid(s);
        hash(K) := shard.value(s,K) if (shard.lo(s) <= K & K <= shard.hi(s)) else hash(K)
    }
    }

Implementation

    object impl = {

    instance tab : ordered_map(key,value)

    implement set {
        call tab.set(k,v)
    }

    implement get {
        v := tab.get(k)
    }

    implement extract_ {
        shard.second(res,X) := 0;
        local idx : key.iter.t, pos : shard.iter.t, lim: key.iter.t  {
        idx := tab.begin(lo);
        lim := key.iter.begin(hi);
        pos := shard.iter.begin(0);
        while ~shard.iter.iter_end(pos) & idx <= lim
            invariant ~shard.iter.done(X,pos) -> shard.second(res,X) = 0
                    invariant lo <= X & key.iter.done(X,idx) -> shard.value(res,X) = hash(X)
            invariant ~key.iter.iter_end(idx) -> lo <= key.iter.iter_val(idx)
            invariant shard.iter.iter_end(pos) -> key.iter.done(lo,idx)
            invariant ~key.iter.done(X,idx) -> ~shard.at(res,X,Y)
            invariant shard.at(res,X,Y) & shard.at(res,X,Z) -> Y = Z
        {
            shard.first(res,shard.iter.val(pos)) := key.iter.val(idx);
            shard.second(res,shard.iter.val(pos)) := tab.get(key.iter.val(idx));
            idx := tab.next(idx);
            pos := shard.iter.next(pos)
        };
        shard.lo(res) := lo;
        if key.iter.done(hi,idx) {
            shard.hi(res) := hi
        } else {
            shard.hi(res) := key.iter.val(key.iter.prev(idx))
        }
        }
    }

    implement incorporate(s:shard.t) {
        local lo:key.t, hi:key.t {
        lo := shard.lo(s);
        hi := shard.hi(s);
        call tab.erase(lo,hi);
        local idx : key.iter.t, pos : shard.iter.t {
            pos := shard.iter.begin(0);
            while ~shard.iter.iter_end(pos)
            invariant lo <= X & X <= hi & shard.value(s,X) = 0 -> ~tab.s(X)
            invariant lo <= X & X <= hi & shard.iter.done(Y,pos) & shard.at(s,X,Y) -> tab.s(X) & tab.r(X,shard.value(s,X))
            invariant ~(lo <= X & X <= hi) -> spec.tab_invar(X,Y)

following are object invariants of tab and shouldn't be needed here

            invariant tab.r(X,Y) & tab.r(X,Z) -> Y = Z
            {
            local r : shard.range {
                r := shard.iter.val(pos);
                if lo <= shard.first(s,r) & shard.first(s,r) <= hi & shard.second(s,r) ~= 0 {
                call tab.set(shard.first(s,r),shard.second(s,r))
                }
            };
            pos := shard.iter.next(pos)
            }
        }
        }
    }

    object spec = {
        derived tab_invar(X,Y) =
          (tab.s(X) & tab.r(X,Y) -> hash(X) = Y)
          & (~tab.s(X) -> hash(X) = 0)
          & (tab.s(X) -> tab.r(X,hash(X)))
    }

    conjecture shard.value(S,X)=Z -> spec.tab_invar(X,Y)

    }

}