From 7c8ec015f37cc40615de7c58c23e901e9bdb45fb Mon Sep 17 00:00:00 2001 From: Conradin Laux Date: Thu, 28 Nov 2024 11:51:07 +0100 Subject: [PATCH 01/11] view function that converts []byte -> seq[byte] --- byteslice/byteslice.gobra | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/byteslice/byteslice.gobra b/byteslice/byteslice.gobra index 5335034..48c8804 100644 --- a/byteslice/byteslice.gobra +++ b/byteslice/byteslice.gobra @@ -33,6 +33,15 @@ 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 len(ub) +opaque +pure func View(ub []byte) (res seq[byte]) + ghost requires 0 < p requires acc(Bytes(s, start, end), p) From 88221e980351567173074698aae28e79995df378 Mon Sep 17 00:00:00 2001 From: Conradin Laux Date: Thu, 28 Nov 2024 12:03:37 +0100 Subject: [PATCH 02/11] Split pure function --- bytes/bytes.gobra | 25 +++++++++++++++++++++++++ bytes/bytes_test.gobra | 19 +++++++++++++++++++ 2 files changed, 44 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..d365550 --- /dev/null +++ b/bytes/bytes.gobra @@ -0,0 +1,25 @@ +//+gobra + +package bytes + +ghost +requires 0 < len(sep) +decreases +pure func Split(b, sep seq[byte]) (res seq[seq[byte]]) { + return SplitInner(b, sep, seq[byte]{}) +} + +ghost +requires 0 < len(sep) +decreases len(s) +pure func SplitInner(s, sep, ac seq[byte]) (res seq[seq[byte]]) { + return len(s) == 0 ? + ( len(ac) == 0 ? + seq[seq[byte]]{} : + seq[seq[byte]]{ac}) : + ( sep == s ? + seq[seq[byte]]{ ac, seq[byte]{} } : + 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..37abc26 --- /dev/null +++ b/bytes/bytes_test.gobra @@ -0,0 +1,19 @@ +package bytes + +ghost +decreases +func testSplit() { + abcd := seq[byte]{'a','b','c','d'} + + 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'} } +} From 740904fa7eb75ab4624379779402ad87cdb92f23 Mon Sep 17 00:00:00 2001 From: Conradin Laux Date: Thu, 28 Nov 2024 12:03:47 +0100 Subject: [PATCH 03/11] Repeat pure function --- bytes/bytes.gobra | 8 ++++++++ bytes/bytes_test.gobra | 10 ++++++++++ 2 files changed, 18 insertions(+) diff --git a/bytes/bytes.gobra b/bytes/bytes.gobra index d365550..7e2f148 100644 --- a/bytes/bytes.gobra +++ b/bytes/bytes.gobra @@ -2,6 +2,14 @@ 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) decreases diff --git a/bytes/bytes_test.gobra b/bytes/bytes_test.gobra index 37abc26..097cfef 100644 --- a/bytes/bytes_test.gobra +++ b/bytes/bytes_test.gobra @@ -5,6 +5,7 @@ decreases func testSplit() { abcd := seq[byte]{'a','b','c','d'} + // this block of assertions is simply to teach gobra how to unfold 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'}} @@ -17,3 +18,12 @@ func testSplit() { assert Split(abcd, seq[byte]{'a'}) == seq[seq[byte]]{ seq[byte]{}, seq[byte]{'b','c','d'} } } + +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'} +} From fad4908dd60be949477887cb8ec80f1f8b5aafa1 Mon Sep 17 00:00:00 2001 From: Conradin Laux Date: Thu, 28 Nov 2024 14:02:34 +0100 Subject: [PATCH 04/11] provide body for View --- byteslice/byteslice.gobra | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/byteslice/byteslice.gobra b/byteslice/byteslice.gobra index 48c8804..6e09ad1 100644 --- a/byteslice/byteslice.gobra +++ b/byteslice/byteslice.gobra @@ -35,12 +35,23 @@ func Byte(s []byte, start int, end int, i int) byte { ghost requires acc(Bytes(ub, 0, len(ub)), _) -ensures len(res) == len(ub) -ensures forall i int :: { res[i] } 0 <= i && i < 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 len(ub) +decreases opaque -pure func View(ub []byte) (res seq[byte]) +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 From 7f561ee7d8372b3d2b787bc084dcac1405afd4f8 Mon Sep 17 00:00:00 2001 From: Conradin Laux Date: Thu, 28 Nov 2024 14:33:51 +0100 Subject: [PATCH 05/11] fix Split to behave as Go's Split does --- bytes/bytes.gobra | 12 ++++-------- bytes/bytes_test.gobra | 30 ++++++++++++++++++++++++++++++ 2 files changed, 34 insertions(+), 8 deletions(-) diff --git a/bytes/bytes.gobra b/bytes/bytes.gobra index 7e2f148..317924e 100644 --- a/bytes/bytes.gobra +++ b/bytes/bytes.gobra @@ -22,12 +22,8 @@ requires 0 < len(sep) decreases len(s) pure func SplitInner(s, sep, ac seq[byte]) (res seq[seq[byte]]) { return len(s) == 0 ? - ( len(ac) == 0 ? - seq[seq[byte]]{} : - seq[seq[byte]]{ac}) : - ( sep == s ? - seq[seq[byte]]{ ac, seq[byte]{} } : - s[:len(sep)] == sep ? - seq[seq[byte]]{ac} ++ SplitInner(s[len(sep):], sep, seq[byte]{}) : - SplitInner(s[1:], sep, ac ++ seq[byte]{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 index 097cfef..a54a10a 100644 --- a/bytes/bytes_test.gobra +++ b/bytes/bytes_test.gobra @@ -19,6 +19,36 @@ func testSplit() { 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() { From d5193e64696606e95b25935345a24b4ba8b90aa4 Mon Sep 17 00:00:00 2001 From: Conradin Laux Date: Thu, 28 Nov 2024 14:44:03 +0100 Subject: [PATCH 06/11] this postcondition turns out to be convenient --- bytes/bytes.gobra | 2 ++ 1 file changed, 2 insertions(+) diff --git a/bytes/bytes.gobra b/bytes/bytes.gobra index 317924e..369a8b1 100644 --- a/bytes/bytes.gobra +++ b/bytes/bytes.gobra @@ -12,6 +12,7 @@ pure func Repeat(b seq[byte], count int) (res seq[byte]) { 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]{}) @@ -19,6 +20,7 @@ pure func Split(b, sep seq[byte]) (res seq[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 ? From 0285438d9b61c2109bc17569ac4765f146a5221e Mon Sep 17 00:00:00 2001 From: Conradin Laux Date: Thu, 28 Nov 2024 14:49:46 +0100 Subject: [PATCH 07/11] add copyright header --- bytes/bytes.gobra | 14 ++++++++++++++ bytes/bytes_test.gobra | 14 ++++++++++++++ 2 files changed, 28 insertions(+) diff --git a/bytes/bytes.gobra b/bytes/bytes.gobra index 369a8b1..866efe8 100644 --- a/bytes/bytes.gobra +++ b/bytes/bytes.gobra @@ -1,3 +1,17 @@ +// 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 diff --git a/bytes/bytes_test.gobra b/bytes/bytes_test.gobra index a54a10a..ed62637 100644 --- a/bytes/bytes_test.gobra +++ b/bytes/bytes_test.gobra @@ -1,3 +1,17 @@ +// 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 From cfe458bdb8e25ffc421bab1874266bc83d30aeda Mon Sep 17 00:00:00 2001 From: Conradin Laux Date: Thu, 28 Nov 2024 14:50:20 +0100 Subject: [PATCH 08/11] make viewInner public --- byteslice/byteslice.gobra | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/byteslice/byteslice.gobra b/byteslice/byteslice.gobra index 6e09ad1..225d7dc 100644 --- a/byteslice/byteslice.gobra +++ b/byteslice/byteslice.gobra @@ -41,7 +41,7 @@ ensures forall i int :: { res[i] } 0 <= i && i < len(ub) ==> decreases opaque pure func View(ub []byte) (res seq[byte]) { - return unfolding acc(Bytes(ub, 0, len(ub)), _) in viewInner(ub) + return unfolding acc(Bytes(ub, 0, len(ub)), _) in ViewInner(ub) } ghost @@ -49,8 +49,8 @@ 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]} +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 From e1d7e9ffedee7eebd6fe3e625ea5c7b4cf271dc7 Mon Sep 17 00:00:00 2001 From: Conradin Laux Date: Thu, 28 Nov 2024 14:51:02 +0100 Subject: [PATCH 09/11] fix formatting --- byteslice/byteslice.gobra | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/byteslice/byteslice.gobra b/byteslice/byteslice.gobra index 225d7dc..db39f0f 100644 --- a/byteslice/byteslice.gobra +++ b/byteslice/byteslice.gobra @@ -45,7 +45,7 @@ pure func View(ub []byte) (res seq[byte]) { } ghost -requires forall i int :: {&ub[i]} 0 <= i && i < len(ub) ==> acc(&ub[i], _) +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) From 1d9228d8b290bf91bb5c0322aa2a045e7e6b4ebd Mon Sep 17 00:00:00 2001 From: Conradin Laux Date: Thu, 28 Nov 2024 14:54:44 +0100 Subject: [PATCH 10/11] reword --- bytes/bytes_test.gobra | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bytes/bytes_test.gobra b/bytes/bytes_test.gobra index ed62637..979e03b 100644 --- a/bytes/bytes_test.gobra +++ b/bytes/bytes_test.gobra @@ -19,7 +19,7 @@ decreases func testSplit() { abcd := seq[byte]{'a','b','c','d'} - // this block of assertions is simply to teach gobra how to unfold the definition of `SplitInner` + // 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'}} From c7d45a331602b7afd06f0d5552d773e1dfffd8f9 Mon Sep 17 00:00:00 2001 From: HSMF <59176979+HSMF@users.noreply.github.com> Date: Thu, 28 Nov 2024 14:58:59 +0100 Subject: [PATCH 11/11] Update bytes/bytes.gobra MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: João Pereira --- bytes/bytes.gobra | 1 - 1 file changed, 1 deletion(-) diff --git a/bytes/bytes.gobra b/bytes/bytes.gobra index 866efe8..b245d30 100644 --- a/bytes/bytes.gobra +++ b/bytes/bytes.gobra @@ -15,7 +15,6 @@ //+gobra package bytes - ghost requires count >= 0