Add package byteslice adapted from verifiedSCION (#20)

This PR adds features to treat slices of bytes abstractly. This is often
a better alternative to propagating quantified permissions to a slice,
both in terms of readability and verification performance

byteslice/byteslice.gobra

@@ -0,0 +1,134 @@
+// 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 byteslice
+
+// Bytes represents the permission to access the elements of s starting
+// at index start (inclusive) and ending in index end (exclusive).
+pred Bytes(s []byte, 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(Bytes(s, start, end), _)
+requires start <= i && i < end
+decreases
+func Byte(s []byte, start int, end int, i int) byte {
+	return unfolding acc(Bytes(s, start, end), _) in s[i]
+}
+
+ghost
+requires 0 < p
+requires acc(Bytes(s, start, end), p)
+requires start <= idx && idx <= end
+ensures  acc(Bytes(s, start, idx), p)
+ensures  acc(Bytes(s, idx, end), p)
+decreases
+func SplitAt(s []byte, start int, end int, idx int, p perm) {
+	unfold acc(Bytes(s, start, end), p)
+	fold   acc(Bytes(s, start, idx), p)
+	fold   acc(Bytes(s, idx, end), p)
+}
+
+ghost
+requires 0 < p
+requires acc(Bytes(s, start, idx), p)
+requires acc(Bytes(s, idx,   end), p)
+ensures  acc(Bytes(s, start, end), p)
+decreases
+func CombineAt(s []byte, start int, end int, idx int, p perm) {
+	unfold acc(Bytes(s, start, idx), p)
+	unfold acc(Bytes(s, idx,   end), p)
+	fold   acc(Bytes(s, start, end), p)
+}
+
+ghost
+requires 0 < p
+requires 0 <= start && start <= end && end <= cap(s)
+requires acc(Bytes(s, start, end), p)
+ensures  acc(Bytes(s[start:end], 0, len(s[start:end])), p)
+decreases
+func Reslice(s []byte, start int, end int, p perm) {
+	unfold acc(Bytes(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(Bytes(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(Bytes(s[start:end], 0, len(s[start:end])), p)
+ensures  acc(Bytes(s, start, end), p)
+decreases
+func Unslice(s []byte, start int, end int, p perm) {
+	unfold acc(Bytes(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(Bytes(s, start, end), p)
+}
+
+ghost
+requires 0 < p
+requires 0 <= start && start <= end && end <= len(s)
+requires acc(Bytes(s, 0, len(s)), p)
+ensures  acc(Bytes(s[start:end], 0, end-start), p)
+ensures  acc(Bytes(s, 0, start), p)
+ensures  acc(Bytes(s, end, len(s)), p)
+decreases
+func SplitRange(s []byte, 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(Bytes(s, 0, start), p)
+requires acc(Bytes(s[start:end], 0, end-start), p)
+requires acc(Bytes(s, end, len(s)), p)
+ensures  acc(Bytes(s, 0, len(s)), p)
+decreases
+func CombineRange(s []byte, 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 Bytes(nil, 0, 0)
+decreases
+func NilBytes() {
+	fold Bytes(nil, 0, 0)
+}