Creport2

include order
include collections
include deduction

module shift_theory(idx) = {
    relation r(T : idx, X : idx, Y : idx)
    action f(t:idx,x:idx) returns (y:idx)
    action b(t:idx,x:idx) returns (y:idx)

    specification {
    property r(T,X,Y) & r(T,X,Y1) -> Y = Y1
    property r(T,X,Y) & r(T,X1,Y) -> X = X1
    property r(T,X1,Y1) & r(T,X2,Y2) & X1 < X2 -> Y1 < Y2
    property r(T1,X,Y1) & r(T2,X,Y2) & T1 < T2 -> Y2 < Y1
        property r(T,X1,Y1) & idx.succ(X1,X2) & idx.succ(Y1,Y2) -> r(T,X2,Y2)
        property r(0,X,X)
        property r(X,X,0)
        property r(T,X,Y) -> Y <= X & T <= X
        theorem [into] {property X >= T -> exists Y. r(T,X,Y)}
        proof {
            apply introImp;
            apply introE with witness = X - T
        }
    around f {
           require t <= x;
            ...
       ensure r(t,x,y)
    }
    after b {
       ensure r(t,y,x)
    }

    } # end specification section
    implementation {
        definition r(T,X,Y) = (X = Y + T)
        implement f {
            y := x - t
        }
        implement b {
            y := x + t
        }
    }
    isolate iso = this with idx.impl
}

module mysegment(domain,range,none) = {

    type this

    relation value(S:this,D:domain,R:range)
    relation begin(S:this,D:domain)
    relation end(S:this,D:domain)

    action set(w:this, i:domain, v:range) returns (w:this)
    action read(w:this, i:domain) returns (v:range)
    action trim(w:this, i:domain) returns (w:this)
    action empty(i:domain) returns (w:this)
    action merge(w: this, max_w: this) returns (max_w: this)
    action getBegin(w:this) returns (i:domain)
    action getEnd(w:this) returns (i:domain)

    specification {

        after init {

        }
        around set {
            require v ~= none;
            require exists I. begin(w, I) & I <= i;
        ...
            ensure I = i -> (value(w, I, V) <-> V = v);
            ensure I ~= i & value(old w, I, V) -> value(w, I, V)
        }
    around read {
            require exists I. begin(w, I) & I <= i;
            ...
            ensure value(w, i, v);
        }
        around trim {
            require exists I. begin(w, I) & I <= i;
            ...
            ensure begin(w, I) <-> I = i;
            ensure i <= I & value(old w, I, V) -> value(w, I, V)
            proof assume shift.into with T = i, X = I;
            ensure I < i -> (value(w, I, V) <-> V = none);
        }

after empty { ensure value(w, I, V, O) <-> V = none; ensure begin(w, I) <-> I = i; }

around getBegin { ... ensure begin(w, i); }

around getEnd { ... ensure forall I. i <= I -> value(w, I, none); }

        property value(W, I, V1) & value(W, I, V2) -> V1 = V2
        property value(W, I, V) -> 0 <= I
    property begin(W, I) & begin(W, I2) -> I = I2

property end(W, IE) & I >= IE -> value(W, I, none)

    }

    implementation {

        instance shift : shift_theory(slot)
        instance arr : array(domain,range)
        destructor elems(W:this) : arr
        destructor offset(W:this) : domain

        property X < offset(W) -> value(W,X,none)
        property shift.r(offset(W),X,Y) & Y < elems(W).end -> value(W,X,elems(W).value(Y))

property shift.r(offset(W),X,Y) & Y >= elems(W).end -> value(W,X,none)

        property value(W, I, V1) & value(W, I, V2) -> V1 = V2
        property value(W, I, V) -> 0 <= I

definition value(w:this,x:domain,v:range) = (exists Y. shift.r(offset(w),x,Y) & (v = elems(w).value(Y) if Y < elems(w).end else none)) | x < offset(w) & v = none

        definition value(w:this,x:domain,v:range) =
                  (exists Y. shift.r(offset(w),x,Y) &
                        (v = elems(w).value(Y) if Y < elems(w).end else none))
                  | x < offset(w) & v = none

        definition begin(W,I) = (I = offset(W))
        definition end(W,I) = shift.r(offset(W),I,elems(W).end)

        implement set {
        var index := shift.f(offset(w), i);
        if w.elems.end <= index {
        w.elems := w.elems.resize(index.next, none);
        };
            w.elems := w.elems.set(index, v);
        }


        implement read {
            var index := shift.f(offset(w),i);
        v := none if (index >= w.elems.end) else w.elems.value(index)
        }

        implement trim {
            var bound := shift.b(offset(w),w.elems.end);
            var j := i;
            if j < bound {
                while j < bound
                invariant i <= j & j <= bound
                invariant shift.r(offset(old w),bound,old w.elems.end)
                invariant j <= X & X < bound & shift.r(offset(old w),X,Y) -> value(old w,X,w.elems.value(Y))
                invariant X < j & shift.r(i,X,Y) -> value(old w,X,w.elems.value(Y))
                invariant w.offset <= j & w.offset = offset(old w)
                invariant w.elems.end = elems(old w).end

invariant shift.r(i,j,X) -> X < w.elems.end

                {
                    w.elems := w.elems.set(shift.f(i,j),w.elems.value(shift.f(w.offset,j)));
                    j := j.next;
                };
                w.elems := w.elems.resize(shift.f(i,bound),0);
                w.offset := i
            }
            else {
        assume false;
                w.elems := arr.empty;
                w.offset := i;
        };
        bound := shift.b(offset(w),w.elems.end)  # just for a witness
        }

implement trim { var j := i; if j <= bound(w) { while j < bound(w) invariant i <= j invariant j <= bound(w) invariant shift.r(offset(w),bound(w),content(w).end) invariant j <= X & X < bound(w) & shift.r(offset(w),X,Y) -> value(old w, X, maxview(content(w).value(Y)), maxop(content(w).value(Y))) invariant i <= X & X < j & shift.r(i,X,Y) -> value(old w, X, maxview(content(w).value(Y)), maxop(content(w).value(Y)) ) invariant bound(w) = bound(old w) invariant offset(w) = offset(old w) invariant content(w).end = content(old w).end { content(w) := content(w).set(shift.f(i,j),content(w).value(shift.f(offset(w),j))); j := j.next; }; content(w) := content(w).resize(shift.f(i,bound(w)),0); offset(w) := i } else { content(w) := arr.empty; offset(w) := i; bound(w) := i; } }

    }

    isolate iso = this with domain
}

instance slot : unbounded_sequence
type data
individual none : data

instance foo : mysegment(slot,data,none)

export foo.set
export foo.read
export foo.trim