creport2.ivy

#lang ivy1.7

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