From 9816da78ce26eaf00e6cfc3281e447fd769494a2 Mon Sep 17 00:00:00 2001 From: HSMF <59176979+HSMF@users.noreply.github.com> Date: Thu, 28 Nov 2024 20:26:53 +0100 Subject: [PATCH] Bytes (#23) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Introduce a `bytes` package that mirrors go's `bytes` package. Currently supported functions are `Split` and `Repeat`. Furthermore, a function `View` in `byteslice` is added to map `[]byte -> seq[byte]`. For `Split`, we require the separator to be non-empty. The Go implementation handles this case by returning a string split at every utf8 codepoint boundary: `Split("abc☺", "") -> "a", "b", "c", "☺"` Do we want to mimic this behavior? --------- Co-authored-by: João Pereira --- bytes/bytes.gobra | 44 +++++++++++++++++++++++ bytes/bytes_test.gobra | 73 +++++++++++++++++++++++++++++++++++++++ byteslice/byteslice.gobra | 20 +++++++++++ 3 files changed, 137 insertions(+) create mode 100644 bytes/bytes.gobra create mode 100644 bytes/bytes_test.gobra diff --git a/bytes/bytes.gobra b/bytes/bytes.gobra new file mode 100644 index 0000000..b245d30 --- /dev/null +++ b/bytes/bytes.gobra @@ -0,0 +1,44 @@ +// 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 bytes + +ghost +requires count >= 0 +decreases count +pure func Repeat(b seq[byte], count int) (res seq[byte]) { + return count == 0 ? seq[byte]{} : ( b ++ Repeat(b, count - 1) ) +} + +ghost +requires 0 < len(sep) +ensures 0 < len(res) +decreases +pure func Split(b, sep seq[byte]) (res seq[seq[byte]]) { + return SplitInner(b, sep, seq[byte]{}) +} + +ghost +requires 0 < len(sep) +ensures 0 < len(res) +decreases len(s) +pure func SplitInner(s, sep, ac seq[byte]) (res seq[seq[byte]]) { + return len(s) == 0 ? + seq[seq[byte]]{ac} : + s[:len(sep)] == sep ? + seq[seq[byte]]{ac} ++ SplitInner(s[len(sep):], sep, seq[byte]{}) : + SplitInner(s[1:], sep, ac ++ seq[byte]{s[0]}) +} diff --git a/bytes/bytes_test.gobra b/bytes/bytes_test.gobra new file mode 100644 index 0000000..979e03b --- /dev/null +++ b/bytes/bytes_test.gobra @@ -0,0 +1,73 @@ +// 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. + +package bytes + +ghost +decreases +func testSplit() { + abcd := seq[byte]{'a','b','c','d'} + + // these assertions force Gobra to expand the definition of `SplitInner` + assert SplitInner(seq[byte]{}, seq[byte]{'a'}, seq[byte]{'b', 'c', 'd'}) == seq[seq[byte]]{seq[byte]{'b', 'c', 'd'}} + assert seq[byte]{'d'}[1:] == seq[byte]{} + assert SplitInner(seq[byte]{'d'}, seq[byte]{'a'}, seq[byte]{'b', 'c'}) == seq[seq[byte]]{seq[byte]{'b', 'c', 'd'}} + assert seq[byte]{'c', 'd'}[1:] == seq[byte]{'d'} + assert SplitInner(seq[byte]{'c', 'd'}, seq[byte]{'a'}, seq[byte]{'b'}) == seq[seq[byte]]{seq[byte]{'b', 'c', 'd'}} + assert seq[byte]{'b', 'c', 'd'}[1:] == seq[byte]{'c', 'd'} + assert SplitInner(seq[byte]{'b', 'c', 'd'}, seq[byte]{'a'}, seq[byte]{}) == seq[seq[byte]]{seq[byte]{'b', 'c', 'd'}} + assert seq[byte]{'a', 'b', 'c', 'd'}[1:] == seq[byte]{'b', 'c', 'd'} + assert SplitInner(seq[byte]{'a', 'b', 'c', 'd'}, seq[byte]{'a'}, seq[byte]{}) == seq[seq[byte]]{seq[byte]{}, seq[byte]{'b', 'c', 'd'}} + + assert Split(abcd, seq[byte]{'a'}) == seq[seq[byte]]{ seq[byte]{}, seq[byte]{'b','c','d'} } +} + +ghost +decreases +func testSplitEnd() { + abcd := seq[byte]{'a','b','c','d'} + abc := seq[byte]{'a','b','c'} + sep := seq[byte]{'d'} + + assert SplitInner(seq[byte]{}, sep, seq[byte]{}) == seq[seq[byte]]{seq[byte]{}} + assert sep[1:] == seq[byte]{} + assert SplitInner(sep, sep, abc) == seq[seq[byte]]{abc, seq[byte]{}} + assert seq[byte]{'c', 'd'}[1:] == sep + assert SplitInner(seq[byte]{'c', 'd'}, sep, seq[byte]{'a', 'b'}) == seq[seq[byte]]{abc, seq[byte]{}} + assert seq[byte]{'b', 'c', 'd'}[1:] == seq[byte]{'c', 'd'} + assert SplitInner(seq[byte]{'b', 'c', 'd'}, sep, seq[byte]{'a'}) == seq[seq[byte]]{abc, seq[byte]{}} + assert abcd[1:] == seq[byte]{'b', 'c', 'd'} + assert SplitInner(abcd, sep, seq[byte]{}) == seq[seq[byte]]{abc, seq[byte]{}} + assert Split(abcd, sep) == seq[seq[byte]]{abc, seq[byte]{}} + + assert Split(abcd, seq[byte]{'d'}) == seq[seq[byte]]{ seq[byte]{'a','b','c'}, seq[byte]{} } +} + +ghost +decreases +func testSplitEmpty() { + sep := seq[byte]{'/'} + + assert SplitInner(seq[byte]{}, sep, seq[byte]{}) == seq[seq[byte]]{seq[byte]{}} + assert Split(seq[byte]{}, sep) == seq[seq[byte]]{seq[byte]{}} +} + +ghost +decreases +func testRepeat() { + assert Repeat(seq[byte]{'a', 'b'}, 0) == seq[byte]{} + assert Repeat(seq[byte]{'a', 'b'}, 1) == seq[byte]{'a', 'b'} + + assert Repeat(seq[byte]{'a', 'b'}, 2) == seq[byte]{'a', 'b', 'a', 'b'} +} diff --git a/byteslice/byteslice.gobra b/byteslice/byteslice.gobra index 5335034..db39f0f 100644 --- a/byteslice/byteslice.gobra +++ b/byteslice/byteslice.gobra @@ -33,6 +33,26 @@ func Byte(s []byte, start int, end int, i int) byte { return unfolding acc(Bytes(s, start, end), _) in s[i] } +ghost +requires acc(Bytes(ub, 0, len(ub)), _) +ensures len(res) == len(ub) +ensures forall i int :: { res[i] } 0 <= i && i < len(ub) ==> + res[i] == Byte(ub, 0, len(ub), i) +decreases +opaque +pure func View(ub []byte) (res seq[byte]) { + return unfolding acc(Bytes(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 []byte) (res seq[byte]) { + return len(ub) == 0 ? seq[byte]{} : ViewInner(ub[:len(ub)-1]) ++ seq[byte]{ub[len(ub)-1]} +} + ghost requires 0 < p requires acc(Bytes(s, start, end), p)