From dd3225e33b159b484a1261d916e97bf3729d7416 Mon Sep 17 00:00:00 2001 From: HSMF <59176979+HSMF@users.noreply.github.com> Date: Tue, 3 Dec 2024 10:34:02 +0100 Subject: [PATCH] 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 | 154 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 154 insertions(+) create mode 100644 runeslice/runeslice.gobra diff --git a/runeslice/runeslice.gobra b/runeslice/runeslice.gobra new file mode 100644 index 0000000..64ac89c --- /dev/null +++ b/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) +}