diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra new file mode 100644 index 00000000000..740547f5c8a --- /dev/null +++ b/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. + preserves acc(Mem(elems), ReadPerm) + ensures res == len(elems) + 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. + ghost + preserves acc(Mem(elems), ReadPerm) + 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) + 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) + decreases + LemmaLessIsTransitive(ghost elems seq[any]) + + requires acc(Mem(elems), ReadPerm) + requires 0 <= i && i < len(elems) + requires 0 <= j && j < len(elems) + ensures i == j ==> !res + decreases + 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. + preserves acc(Mem(elems), ReadPerm) + requires 0 <= i && i < len(elems) + requires 0 <= j && j < len(elems) + 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) + requires 0 <= j && j < len(elems) + ensures Mem(swapped_elems) + ensures haveSameElements(elems, swapped_elems) + ensures 0 <= i && i < len(elems) + ensures 0 <= j && j < len(elems) + ensures elems[i] === swapped_elems[j] + ensures elems[j] === swapped_elems[i] + ensures forall x int :: {elems[x]} {swapped_elems[x]} (0 <= x && x < len(elems) && x != i && x != j) ==> (elems[x] === swapped_elems[x]) + 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. + ensures old(less_spec(j, i, elems)) ==> !less_spec(j, i, swapped_elems) + 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. +//# isPartiallySorted is intended to be used in specifications. +//# It reports whether the elemented from indicies 'start' to 'end' (inclusive) are sorted in non-decreasing order according to 'less_spec' +ghost +requires data != nil +requires data.Mem(elems) +requires 0 <= start && start < len(elems) +requires start <= end && end < len(elems) +ensures end == start ==> sorted +ensures (end > start && !data.less_spec(end, end - 1, elems)) ==> sorted == isPartiallySorted(data, start, end - 1, elems) +ensures (end > start && data.less_spec(end, end - 1, elems)) ==> !sorted +decreases end - start +pure +func isPartiallySorted(data Interface, start, end int, ghost elems seq[any]) (sorted bool) { + return (end == start) ? 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))) + decreases i + for i := n - 1; i > 0; i-- { + if data.Less(i, i - 1, elems) { + return false + } + assert !data.less_spec(i, i - 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 :: {&s[j]} 0 <= j && j < len(s) ==> acc(&s[j], _) +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 :: {&x[j]} 0 <= j && j < len(x) ==> acc(&x[j]) && + s == toSeq(x) +} + +preserves acc(x.Mem(elems), ReadPerm) +ensures unfolding acc(x.Mem(elems), ReadPerm) in res == len(elems) +decreases +func (x IntSlice) Len(ghost elems seq[any]) (res int) { + return len(x) +} + +ghost +preserves acc(x.Mem(elems), ReadPerm) +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) +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) +decreases +func (x IntSlice) LemmaLessIsTransitive(ghost elems seq[any]){ + unfold acc(x.Mem(elems), ReadPerm) + fold acc(x.Mem(elems), ReadPerm) +} + +requires acc(x.Mem(elems), ReadPerm) +requires 0 <= i && i < len(elems) +requires 0 <= j && j < len(elems) +ensures i == j ==> !res +decreases +pure func (x IntSlice) less_spec(i, j int, ghost elems seq[any]) (res bool){ + return unfolding acc(x.Mem(elems), ReadPerm) in x[i] < x[j] +} + +preserves acc(x.Mem(elems), ReadPerm) +requires 0 <= i && i < len(elems) +requires 0 <= j && j < len(elems) +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 haveSameElements(elems, swapped_elems) +ensures 0 <= i && i < len(elems) +ensures 0 <= j && j < len(elems) +ensures elems[i] === swapped_elems[j] +ensures elems[j] === swapped_elems[i] +ensures forall idx int :: {elems[idx]} {swapped_elems[idx]} (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) +ensures old(x.less_spec(i, j, elems)) ==> !x.less_spec(i, j, swapped_elems) +ensures old(x.less_spec(j, i, elems)) ==> !x.less_spec(j, i, 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 forall idx int :: (0 <= idx && idx < len(elems)) ==> elems[idx] == old(unfolding x.Mem(elems) in x[idx]) //# Cannot be asserted in GobraCLI but works in GobraIDE as of Jan 23rd 2023 + assert forall idx int :: (0 <= idx && idx < len(swapped_elems)) ==> swapped_elems[idx] == unfolding x.Mem(swapped_elems) in x[idx] + assume haveSameElements(elems, swapped_elems) //# We believe this to be true. +} + +//# 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) +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 + decreases b-i + for i := a + 1; i < b; i++ { + 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-1] is always sorted and [j:i] is always sorted + 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 { + assert !data.less_spec(j, j - 1, sorted_elems) + 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]){ + return (len(elemsSeq) == 0 ? mset[any]{} : + mset[any]{elemsSeq[len(elemsSeq) - 1]} union toMultiSet(elemsSeq[:len(elemsSeq) - 1])) +} + + + + +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]}) +} +*/ + + +