package for working with slices of runes (#24)

This PR introduces a `runeslice` package that contains utilities for
working with `[]rune`. It has been copied from th `byteslice` package.

Only `Runes`, `Rune`, and `View` are actually used downstream, but the
other ghost functions might prove useful for further users.

runeslice/runeslice.gobra

@@ -0,0 +1,154 @@
+// Copyright 2024 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package runeslice
+
+// Runes represents the permission to access the elements of s starting
+// at index start (inclusive) and ending in index end (exclusive).
+pred Runes(s []rune, start int, end int) {
+	0 <= start &&
+	start <= end &&
+	end <= cap(s) &&
+	forall i int :: { &s[i] } start <= i && i < end ==> acc(&s[i])
+}
+
+pure
+requires acc(Runes(s, start, end), _)
+requires start <= i && i < end
+decreases
+func Rune(s []rune, start int, end int, i int) rune {
+	return unfolding acc(Runes(s, start, end), _) in s[i]
+}
+
+ghost
+requires acc(Runes(ub, 0, len(ub)), _)
+ensures  len(res) == len(ub)
+ensures  forall i int :: { res[i] } 0 <= i && i < len(ub) ==>
+    res[i] == Rune(ub, 0, len(ub), i)
+decreases
+opaque
+pure func View(ub []rune) (res seq[rune]) {
+	return unfolding acc(Runes(ub, 0, len(ub)), _) in ViewInner(ub)
+}
+
+ghost
+requires forall i int :: { &ub[i] } 0 <= i && i < len(ub) ==> acc(&ub[i], _)
+ensures  len(res) == len(ub)
+ensures  forall i int :: { res[i] } 0 <= i && i < len(ub) ==> res[i] == ub[i]
+decreases len(ub)
+pure func ViewInner(ub []rune) (res seq[rune]) {
+	return len(ub) == 0 ? seq[rune]{} :  ViewInner(ub[:len(ub)-1]) ++ seq[rune]{ub[len(ub)-1]}
+}
+
+ghost
+requires 0 < p
+requires acc(Runes(s, start, end), p)
+requires start <= idx && idx <= end
+ensures  acc(Runes(s, start, idx), p)
+ensures  acc(Runes(s, idx, end), p)
+decreases
+func SplitAt(s []rune, start int, end int, idx int, p perm) {
+	unfold acc(Runes(s, start, end), p)
+	fold   acc(Runes(s, start, idx), p)
+	fold   acc(Runes(s, idx, end), p)
+}
+
+ghost
+requires 0 < p
+requires acc(Runes(s, start, idx), p)
+requires acc(Runes(s, idx,   end), p)
+ensures  acc(Runes(s, start, end), p)
+decreases
+func CombineAt(s []rune, start int, end int, idx int, p perm) {
+	unfold acc(Runes(s, start, idx), p)
+	unfold acc(Runes(s, idx,   end), p)
+	fold   acc(Runes(s, start, end), p)
+}
+
+ghost
+requires 0 < p
+requires 0 <= start && start <= end && end <= cap(s)
+requires acc(Runes(s, start, end), p)
+ensures  acc(Runes(s[start:end], 0, len(s[start:end])), p)
+decreases
+func Reslice(s []rune, start int, end int, p perm) {
+	unfold acc(Runes(s, start, end), p)
+	assert forall i int :: { &s[start:end][i] } 0 <= i && i < (end-start) ==>
+		&s[start:end][i] == &s[start + i]
+	fold  acc(Runes(s[start:end], 0, len(s[start:end])), p)
+}
+
+ghost
+requires 0 < p
+requires 0 <= start && start <= end && end <= cap(s)
+requires len(s[start:end]) <= cap(s)
+requires acc(Runes(s[start:end], 0, len(s[start:end])), p)
+ensures  acc(Runes(s, start, end), p)
+decreases
+func Unslice(s []rune, start int, end int, p perm) {
+	unfold acc(Runes(s[start:end], 0, len(s[start:end])), p)
+	assert forall i int :: { &s[start:end][i] } 0 <= i && i < len(s[start:end]) ==>
+		&s[start:end][i] == &s[start + i]
+
+	invariant 0 <= j && j <= len(s[start:end])
+	invariant forall i int :: { &s[start:end][i] } j <= i && i < len(s[start:end]) ==>
+		acc(&s[start:end][i], p)
+	invariant forall i int :: { &s[start:end][i] } 0 <= i && i < len(s[start:end]) ==>
+		&s[start:end][i] == &s[start + i]
+	invariant forall i int :: { &s[i] } start <= i && i < start+j ==>
+		acc(&s[i], p)
+	decreases len(s[start:end]) - j
+	for j := 0; j < len(s[start:end]); j++ {
+		assert &s[start:end][j] == &s[start + j]
+		assert forall i int :: { &s[i] } start <= i && i <= start+j ==> acc(&s[i], p)
+	}
+	fold acc(Runes(s, start, end), p)
+}
+
+ghost
+requires 0 < p
+requires 0 <= start && start <= end && end <= len(s)
+requires acc(Runes(s, 0, len(s)), p)
+ensures  acc(Runes(s[start:end], 0, end-start), p)
+ensures  acc(Runes(s, 0, start), p)
+ensures  acc(Runes(s, end, len(s)), p)
+decreases
+func SplitRange(s []rune, start int, end int, p perm) {
+	SplitAt(s, 0, len(s), start, p)
+	SplitAt(s, start, len(s), end, p)
+	Reslice(s, start, end, p)
+}
+
+ghost
+requires 0 < p
+requires 0 <= start && start <= end && end <= len(s)
+requires acc(Runes(s, 0, start), p)
+requires acc(Runes(s[start:end], 0, end-start), p)
+requires acc(Runes(s, end, len(s)), p)
+ensures  acc(Runes(s, 0, len(s)), p)
+decreases
+func CombineRange(s []rune, start int, end int, p perm) {
+	Unslice(s, start, end, p)
+	CombineAt(s, start, len(s), end, p)
+	CombineAt(s, 0, len(s), start, p)
+}
+
+ghost
+ensures Runes(nil, 0, 0)
+decreases
+func NilRunes() {
+	fold Runes(nil, 0, 0)
+}