diff --git a/byteslice/byteslice.gobra b/byteslice/byteslice.gobra new file mode 100644 index 0000000..5335034 --- /dev/null +++ b/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) +}