Bytes

bytes/bytes.gobra

@@ -0,0 +1,29 @@
+//+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)
+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 ?
+		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]})
+}

bytes/bytes_test.gobra

@@ -0,0 +1,59 @@
+package bytes
+
+ghost
+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'}}
+	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'}
+}

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)