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.iter.t,hi:key.iter.t) returns(res:shard.t)

Incorporates a shard into a hash table

    action incorporate(s:shard.t)

Specification

    function hash(X:key.t) : value

    object spec = {
    init hash(X) = 0

    before set {
        hash(k) := v
    }

    after get {
        assert v = hash(k)
    }

    after extract_ {
        assert shard.lo(res) = lo;
        assert shard.hi(res) = hi;
        assert key.iter.between(lo,X,hi)-> shard.value(res,X) = hash(X);
        assert shard.valid(res)
    }

    before incorporate(s:shard.t) {
        assert shard.valid(s);
        hash(K) := shard.value(s,K)
                   if key.iter.between(shard.lo(s),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,0)
    }

    implement extract_ {
        res.kv := shard.kvt.empty;
            var idx := tab.lub(lo);
            while idx < hi
                invariant lo <= idx & (idx < hi -> tab.contains(idx.val))
                invariant lo.between(X,idx) & tab.contains(X) ->
                               exists I. (res.key_at(I,X) & tab.maps(X,res.value_at(I)))
                invariant res.key_at(I,X) -> lo.between(X,idx) & tab.contains(X)
                invariant shard.valid(res)
            {
                var k := idx.val;
                res.kv := res.kv.append_pair(k,tab.get(k,0));
                idx := tab.next(idx)
            };
            res.lo := lo;
            res.hi := hi
    }

    implement incorporate(s:shard.t) {
            var lo := s.lo;
            var hi := s.hi;
            call tab.erase(lo,hi);
            var pos:shard.index.t  := 0;
            while pos < s.kv.end
                invariant 0 <= pos & pos <= s.kv.end
                invariant lo.between(X,hi) & s.value(X) = 0 -> ~tab.contains(X)
                invariant lo.between(X,hi) & 0 <= Y & Y < pos & s.key_at(Y,X) & s.value(X) ~= 0
                                 -> tab.contains(X) & tab.maps(X,s.value(X))
                invariant ~lo.between(X,hi) -> spec.tab_invar(X,Y)

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

                invariant tab.maps(X,Y) & tab.maps(X,Z) -> Y = Z & tab.contains(X)
            {
                var k := s.kv.get_key(pos);
                var d := s.kv.get_value(pos);
                if lo.between(k,hi) & d ~= 0{
                    call tab.set(k,d)
                };
                pos := pos.next
            }
    }

    object spec = {
        function tab_invar(X,Y) =
          (tab.contains(X) & tab.maps(X,Y) -> hash(X) = Y)
          & (~tab.contains(X) -> hash(X) = 0)
          & (tab.contains(X) -> tab.maps(X,hash(X)))
    }

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

    conjecture spec.tab_invar(X,Y)

    }

}