sort PR

src/sort/sort_partial.gobra

@@ -0,0 +1,294 @@
+// Copyright 2009 The Go Authors. All rights reserved.
+// Use of this source code is governed by a BSD-style
+// license that can be found in the LICENSE file.
+
+//go:generate go run gen_sort_variants.go
+
+// Package sort provides primitives for sorting slices and user-defined collections.
+// +gobra
+package sort
+
+//# import "math/bits" //# Had to comment this out for verification to work.
+
+ghost const ReadPerm perm = 1/2
+
+// An implementation of Interface can be sorted by the routines in this package.
+// The methods refer to elements of the underlying collection by integer index.
+type Interface interface {
+	pred Mem(ghost s seq[any])
+
+	// Len is the number of elements in the collection.
+	requires acc(Mem(elems), ReadPerm)
+	ensures  acc(Mem(elems), ReadPerm)
+	ensures  res == len(elems)
+	ensures  res >= 0
+	decreases
+	Len(ghost elems seq[any]) (res int)
+
+	// Less reports whether the element with index i
+	// must sort before the element with index j.
+	//
+	// If both Less(i, j) and Less(j, i) are false,
+	// then the elements at index i and j are considered equal.
+	// Sort may place equal elements in any order in the final result,
+	// while Stable preserves the original input order of equal elements.
+	//
+	// Less must describe a transitive ordering:
+	//  - if both Less(i, j) and Less(j, k) are true, then Less(i, k) must be true as well.
+	//  - if both Less(i, j) and Less(j, k) are false, then Less(i, k) must be false as well.
+	requires Mem(elems)
+	requires 0 <= i && i < len(elems)
+	requires 0 <= j && j < len(elems)
+	ensures  forall a, b, c int :: {less_spec(a, b, elems), less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && less_spec(a, b, elems) && less_spec(b, c, elems)) ==> less_spec(a, c, elems)
+	pure less_spec(i, j int, ghost elems seq[any]) (res bool)
+	//
+	// Note that floating-point comparison (the < operator on float32 or float64 values)
+	// is not a transitive ordering when not-a-number (NaN) values are involved.
+	// See Float64Slice.Less for a correct implementation for floating-point values.
+	requires acc(Mem(elems), ReadPerm)
+	requires 0 <= i && i < len(elems)
+	requires 0 <= j && j < len(elems)
+	ensures  acc(Mem(elems), ReadPerm)
+	ensures  res == less_spec(i, j, elems)
+	decreases
+	Less(i, j int, ghost elems seq[any]) (res bool)
+
+	// Swap swaps the elements with indexes i and j.
+	requires Mem(elems)
+	requires 0 <= i && i < len(elems) //# possibly make Len() pure and use that
+	requires 0 <= j && j < len(elems) //# possibly make Len() pure and use that
+	ensures  Mem(swapped_elems)
+	ensures  len(elems) == len(swapped_elems) //# somehow this does not suffice to infer i and j are in range [0, len(swapped_elems)-1]
+	ensures  0 <= i && i < len(elems) && i < len(swapped_elems) //# possibly make Len() pure and use that
+	ensures  0 <= j && j < len(elems) && j < len(swapped_elems) //# possibly make Len() pure and use that
+	ensures  elems[i] === swapped_elems[j]
+	ensures  elems[j] === swapped_elems[i]
+	ensures  forall x int :: (0 <= x && x < len(elems) && x != i && x != j) ==> (elems[x] === swapped_elems[x]) //# find triggers
+	ensures  haveSameElements(elems, swapped_elems)
+	ensures  old(less_spec(i, j, elems)) ==> !less_spec(i, j, swapped_elems) //# We make the effect of the Swap operation on the Less relation explicit.
+	decreases
+	Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any])
+}
+
+
+//# PLACEHOLDER: Here would be more code from the original sort.go file.
+
+ghost
+requires data != nil
+requires data.Mem(elems)
+requires 0 <= start && start < len(elems)
+requires start <= end && end < len(elems)
+ensures  end - start == 0 ==> res == true
+ensures  (end - start > 0 && !data.less_spec(end, end - 1, elems)) ==> res == isPartiallySorted(data, start, end - 1, elems)
+ensures  (end - start > 0 &&  data.less_spec(end, end - 1, elems)) ==> !res
+//ensures  res ==> (forall idx int :: ((start < idx && idx <= end) ==> !data.less_spec(idx, idx - 1, elems))) //# find triggers
+//# The below line verifies and should just be an unrolled version of the above line in cases were start+2 < end. However, the above line does not verify.
+//ensures (res && start+2 < end) ==> !data.less_spec(end, end - 1, elems) && !data.less_spec(end-1, end - 2, elems) && !data.less_spec(end-2, end-3, elems)
+pure
+func isPartiallySorted(data Interface, start, end int, ghost elems seq[any]) (res bool) {
+	return (end - start == 0) ? true : (!data.less_spec(end, end - 1, elems) ? isPartiallySorted(data, start, end - 1, elems) : false)
+}
+
+// IsSorted reports whether data is sorted.
+preserves data.Mem(elems)
+requires  data != nil
+ensures   res ==> forall idx int :: {data.less_spec(idx, idx - 1, elems)} ((0 < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx - 1, elems)))
+ensures   !res ==> !(forall idx int :: {data.less_spec(idx, idx - 1, elems)} ((0 < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx - 1, elems))))
+decreases
+func IsSorted(data Interface, ghost elems seq[any]) (res bool) {
+	n := data.Len(elems)
+
+	res = true //# moved this up for use in the invariant
+
+	invariant res
+	invariant i < n
+	invariant len(elems) > 0 ==> 0 <= i //# if n==0 then i==-1 after initialization
+	invariant data.Mem(elems)
+	invariant len(elems) != 0 ==> (forall idx int :: {data.less_spec(idx, idx - 1, elems)} ((i < idx && idx < len(elems)) ==> !data.less_spec(idx, idx - 1, elems)))
+	//invariant len(elems) != 0 ==> isPartiallySorted(data, i, n - 1, elems) //# Would like for this to hold here
+	decreases i
+	for i := n - 1; i > 0; i-- {
+		if data.Less(i, i - 1, elems) {
+			return false
+		}
+		//assert isPartiallySorted(data, i, n - 1, elems)
+	}
+	assert res
+	return
+}
+
+// Convenience types for common cases
+
+// IntSlice attaches the methods of Interface to []int, sorting in increasing order.
+type IntSlice []int
+
+//# Adapted from Gobra tutorial
+ghost
+requires forall j int :: 0 <= j && j < len(s) ==> acc(&s[j], _) //# find triggers
+ensures len(res) == len(s)
+ensures forall j int :: {s[j]} {res[j]} 0 <= j && j < len(s) ==> s[j] == res[j]
+decreases len(s)
+pure func toSeq(s []int) (res seq[any]) {
+  return (len(s) == 0 ? seq[any]{} :
+      toSeq(s[:len(s) - 1]) ++ seq[any]{s[len(s) - 1]})
+}
+
+pred (x IntSlice) Mem(ghost s seq[any]){
+	len(x) == len(s) && //# If this is not the first line in the predicate, then we cannot verify e.g. the last postcondition in Len()
+	forall j int :: 0 <= j && j < len(x) ==> acc(&x[j]) && //# find triggers
+	s == toSeq(x) &&
+	forall j int :: {x[j]} {s[j]} 0 <= j && j < len(s) ==> x[j] == s[j]
+}
+
+requires acc(x.Mem(elems), ReadPerm)
+ensures  acc(x.Mem(elems), ReadPerm)
+ensures  unfolding acc(x.Mem(elems), ReadPerm) in res == len(elems)
+ensures  res >= 0
+decreases
+func (x IntSlice) Len(ghost elems seq[any]) (res int) {
+	return len(x)
+}
+
+requires x.Mem(elems)
+requires 0 <= i && i < len(elems)
+requires 0 <= j && j < len(elems)
+ensures  forall a, b, c int :: {x.less_spec(a, b, elems), x.less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && x.less_spec(a, b, elems) && x.less_spec(b, c, elems)) ==> x.less_spec(a, c, elems)
+pure func (x IntSlice) less_spec(i, j int, ghost elems seq[any]) (res bool){
+	return unfolding x.Mem(elems) in x[i] < x[j]
+}
+
+
+requires acc(x.Mem(elems), ReadPerm)
+requires 0 <= i && i < len(elems)
+requires 0 <= j && j < len(elems)
+ensures  acc(x.Mem(elems), ReadPerm)
+ensures  res == x.less_spec(i, j, elems)
+decreases
+func (x IntSlice) Less(i, j int, ghost elems seq[any]) (res bool) {
+	return unfolding acc(x.Mem(elems), ReadPerm) in x[i] < x[j]
+}
+
+
+requires x.Mem(elems)
+requires 0 <= i && i < len(elems)
+requires 0 <= j && j < len(elems)
+ensures  x.Mem(swapped_elems)
+ensures  len(elems) == len(swapped_elems) //# Somehow this does not suffice to infer i and j are in range [0, len(swapped_elems)-1] and it needs to be stated explicitly below.
+ensures  0 <= i && i < len(elems) && i < len(swapped_elems)
+ensures  0 <= j && j < len(elems) && j < len(swapped_elems)
+//# This line is required..
+ensures  forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (old(unfolding x.Mem(elems) in x[idx]) == (unfolding x.Mem(swapped_elems) in x[idx])) //# find triggers
+//# ..for these 3 corresponding lines to work.
+ensures  elems[i] === swapped_elems[j]
+ensures  elems[j] === swapped_elems[i]
+ensures  forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) //# find triggers
+ensures  haveSameElements(elems, swapped_elems)
+ensures  old(x.less_spec(i, j, elems)) ==> !x.less_spec(i, j, swapped_elems)
+decreases
+func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) {
+	unfold x.Mem(elems)
+	x[i], x[j] = x[j], x[i]
+	swapped_elems = toSeq(x)
+	fold x.Mem(swapped_elems)
+	assume haveSameElements(elems, swapped_elems) //# We believe this to be true. I was not able to establish this as a fact and I was not able to map directly from IntSlice to mset[any].
+
+	//# These four following assumptions should not be required, it works without them in GobraIDE stable version as of Jan. 20th 2023.
+	assume forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (old(unfolding x.Mem(elems) in x[idx]) == (unfolding x.Mem(swapped_elems) in x[idx]))
+	assume  elems[i] === swapped_elems[j]
+	assume  elems[j] === swapped_elems[i]
+	assume forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx])
+}
+
+//# implementation proof
+(IntSlice) implements Interface{ }
+
+
+
+// ######### BEGIN FROM zsortinterface.go ##############
+// insertionSort sorts data[a:b] using insertion sort.
+requires data.Mem(elems)
+requires data != nil
+requires 0 <= a && a < len(elems)
+requires a <= b && b <= len(elems) //# the element at position b does not get sorted
+ensures  data.Mem(sorted_elems)
+ensures  haveSameElements(elems, sorted_elems)
+ensures  a == b ==> isPartiallySorted(data, a, a, sorted_elems)
+//ensures  isPartiallySorted(data, a, b - 1, sorted_elems)
+decreases
+func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted_elems seq[any]) {
+	sorted_elems = elems
+	assert data.Mem(sorted_elems)
+
+	invariant haveSameElements(elems, sorted_elems)
+	invariant a < i
+	invariant a < b ==> i <= b
+	invariant data.Mem(sorted_elems)
+	//# invariant prefix [a:i] is always sorted
+	//invariant forall idx int :: (a < idx && idx < i && i < b) ==> !data.less_spec(idx, idx - 1, sorted_elems)  //# find triggers
+	//invariant isPartiallySorted(data, a, i - 1, sorted_elems)
+	decreases b-i
+	for i := a + 1; i < b; i++ { //# for any kind of sorting to happen b has to be at least a+2, does this mean if called with b=a+1 that this will not be sorted? Answer: YES, should we enforce that in the precondition?
+		invariant haveSameElements(elems, sorted_elems)
+		invariant i < b
+		invariant a <= j && j <= i
+		invariant a < j ==> 0 <= j - 1
+		invariant data.Mem(sorted_elems)
+		//# invariant prefix [a:j-2] is always sorted and [j:i] is always sorted
+		//invariant forall idx int :: (j < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems)  //# find triggers
+		//invariant isPartiallySorted(data, a, XXX, sorted_elems)
+		//invariant isPartiallySorted(data, YYY, i, sorted_elems)
+		decreases j-a
+		for j := i; j > a /*&& data.Less(j, j - 1, elems)*/; j-- { //# The second conjunct in the loop condition was commented out. See comment below.
+			assert 0 <= j - 1
+			assert i < b
+			assert i < len(sorted_elems)
+			if data.Less(j, j - 1, sorted_elems) { //# The second conjunct in the loop condition was commented out and introduced here as an IF block. This is due to a bug in Gobra where short circuiting is not detected. See https://github.com/viperproject/gobra/issues/511
+				sorted_elems = data.Swap(j, j - 1, sorted_elems)
+				assert !data.less_spec(j, j - 1, sorted_elems)
+			} else {
+				break
+			}
+		}
+	}
+}
+// ######### END FROM zsortinterface.go ##############
+
+
+//# helper:
+
+ghost
+ensures forall e any :: e in elemsSeq ==> e in elemsMultiSet //# find triggers
+ensures len(elemsSeq) == len(elemsMultiSet)
+pure func toMultiSet(ghost elemsSeq seq[any]) (ghost elemsMultiSet mset[any])
+
+
+
+ghost
+ensures toMultiSet(seq1) === toMultiSet(seq2) ==> res
+ensures toMultiSet(seq1) !== toMultiSet(seq2) ==> !res
+ensures res ==> len(seq1) == len(seq2)
+pure func haveSameElements(ghost seq1 seq[any], ghost seq2 seq[any]) (res bool){
+	return toMultiSet(seq1) === toMultiSet(seq2)
+}
+
+
+
+/*
+ensures forall e int :: e in s1 ==> e in s2 //# this causes gobra to crash, it works with mset[int] as the return type
+pure func test(ghost s1 mset[int]) (ghost s2 mset[any])
+*/
+
+
+/*
+ghost
+requires forall j int :: 0 <= j && j < len(s) ==> acc(&s[j], _)
+ensures len(res) == len(s)
+ensures forall j int :: 0 <= j && j < len(s) ==> s[j] in res
+pure func toMultiSet(s []int) (res mset[any]) {
+  return (len(s) == 0 ? mset[any]{} :
+      toSeqX(s[:len(s) - 1]) union mset[any]{s[len(s) - 1]})
+}
+*/
+
+
+