From 1d99270f7c1f892d8dbd6d7c197310f22fd8a85a Mon Sep 17 00:00:00 2001
From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com>
Date: Thu, 8 Feb 2024 14:49:28 +0100
Subject: [PATCH] Add initial sequences package + Make package names consistent
 (#11)

Implements all definitions from Dafny that do not rely on any
(multi)set-related definitions. These will be implemented using separate
branches.

Additionally renames the packages to their singular form, and updates
folder and file names for consistency.
---
 math.gobra => math/math.gobra         |   0
 seqs/seqs.gobra                       | 434 ++++++++++++++++++++++++++
 sets/sets.gobra                       | 158 +++++-----
 utils/verify.gobra => util/util.gobra |   7 +-
 4 files changed, 517 insertions(+), 82 deletions(-)
 rename math.gobra => math/math.gobra (100%)
 create mode 100644 seqs/seqs.gobra
 rename utils/verify.gobra => util/util.gobra (94%)

diff --git a/math.gobra b/math/math.gobra
similarity index 100%
rename from math.gobra
rename to math/math.gobra
diff --git a/seqs/seqs.gobra b/seqs/seqs.gobra
new file mode 100644
index 0000000..4ee8d6a
--- /dev/null
+++ b/seqs/seqs.gobra
@@ -0,0 +1,434 @@
+/*
+  This file is part of gobra-libs which is released under the MIT license.
+  See LICENSE or go to https://github.com/viperproject/gobra-libs/blob/main/LICENSE
+  for full license details.
+
+  This file is inspired by the standard libraries and axiomatisations of the following verifiers:
+  - dafny-lang/libraries: https://github.com/dafny-lang/libraries/blob/master/src/Collections/Sequences/Seq.dfy
+*/
+
+// This package defines lemmas for sequences commonly used in specifications.
+package seqs
+
+import "util"
+import "math"
+
+// A sequence is empty if it has length 0.
+ghost
+decreases
+pure func IsEmpty(xs seq[int]) bool {
+	return len(xs) == 0
+}
+
+// Returns the empty sequence.
+ghost
+ensures IsEmpty(result)
+decreases
+pure func Empty() (result seq[int]) {
+	return seq[int]{}
+}
+
+// A sequence is a singleton if it has length 1.
+ghost
+decreases
+pure func IsSingleton(xs seq[int]) bool {
+	return len(xs) == 1
+}
+
+// Creates a singleton sequence from e.
+ghost
+ensures IsSingleton(result)
+decreases
+pure func Singleton(e int) (result seq[int]) {
+	return seq[int]{e}
+}
+
+// Returns the first element of a non-empty sequence.
+ghost
+requires len(xs) > 0
+decreases
+pure func First(xs seq[int]) int {
+	return xs[0]
+}
+
+// Drops the first element of a non-empty sequences.
+ghost
+requires len(xs) > 0
+decreases
+pure func DropFirst(xs seq[int]) seq[int] {
+	return xs[1:]
+}
+
+// Adds e to the beginning of a sequence.
+ghost
+decreases
+pure func Prepend(xs seq[int], e int) seq[int] {
+	return Singleton(e) ++ xs
+}
+
+// Dropping and then prepending the first element preserves the sequence.
+ghost
+requires len(xs) > 0
+ensures xs == Prepend(DropFirst(xs), First(xs))
+decreases
+pure func DropFirstPrependFirst(xs seq[int]) util.Unit {
+	return util.Unit{}
+}
+
+// Returns the last element of a non-empty sequence.
+ghost
+requires len(xs) > 0
+decreases
+pure func Last(xs seq[int]) int {
+	return xs[len(xs)-1]
+}
+
+// Drops the last element of a non-empty sequence.
+ghost
+requires len(xs) > 0
+decreases
+pure func DropLast(xs seq[int]) seq[int] {
+	return xs[:len(xs)-1]
+}
+
+// Adds e to the end of a sequence.
+ghost
+decreases
+pure func Append(xs seq[int], e int) seq[int] {
+	return xs ++ Singleton(e)
+}
+
+// Dropping and then appending the last element preserves the sequence.
+ghost
+requires len(xs) > 0
+ensures xs == Append(DropLast(xs), Last(xs))
+decreases
+pure func DropLastAppendLast(xs seq[int]) util.Unit {
+	return util.Unit{}
+}
+
+// Returns true if xs is a prefix of ys.
+ghost
+decreases
+pure func IsPrefix(xs, ys seq[int]) bool {
+	return len(xs) <= len(ys) && xs == ys[:len(xs)]
+}
+
+// Returns true if xs is a suffix of ys.
+ghost
+decreases
+pure func IsSuffix(xs, ys seq[int]) bool {
+	return len(xs) <= len(ys) && xs == ys[len(ys)-len(xs):]
+}
+
+// Any element in a subsequence is included in the original sequence.
+ghost
+requires 0 <= a && a <= pos && pos < b && b <= len(xs)
+requires subseq == xs[a:b]
+ensures subseq[pos-a] == xs[pos]
+decreases
+pure func InSubseqInSeq(xs, subseq seq[int], a, b, pos int) util.Unit {
+	return util.Unit{}
+}
+
+// A subsequence [a2:b2] of a subsequence [a1:b1] is equal to the
+// the subsequence [a1+a2:b1+b2] of the original sequence.
+ghost
+requires 0 <= a1 && a1 <= b1 && b1 <= len(xs)
+requires 0 <= a2 && a2 <= b2 && b2 <= a1 - b1
+ensures xs[a1:b1][a2:b2] == xs[a1+a2:b1+b2]
+decreases
+pure func SubseqOfSubseq(xs seq[int], a1, b1, a2, b2 int) util.Unit {
+	return util.Unit{}
+}
+
+// The concatenation of sequences is associative.
+ghost
+ensures xs ++ (ys ++ zs) == (xs ++ ys) ++ zs
+decreases
+pure func ConcatIsAssociative(xs, ys, zs seq[int]) util.Unit {
+	return util.Unit{}
+}
+
+// Splitting and then concatenating a sequence preserves it.
+ghost
+requires 0 <= pos && pos < len(xs)
+ensures xs == xs[:pos] ++ xs[pos:]
+decreases
+pure func SplitConcat(xs seq[int], pos int) util.Unit {
+	return util.Unit{}
+}
+
+ghost
+requires len(ys) > 0
+ensures Last(xs ++ ys) == Last(ys)
+decreases
+pure func LastOfConcat(xs, ys seq[int]) util.Unit {
+	return util.Unit{}
+}
+
+ghost
+requires len(xs) > 0
+ensures DropFirst(xs ++ ys) == DropFirst(xs) ++ ys
+decreases
+pure func ConcatDropFirst(xs, ys seq[int]) util.Unit {
+	return util.Unit{}
+}
+
+ghost
+requires len(ys) > 0
+ensures DropLast(xs ++ ys) == xs ++ DropLast(ys)
+decreases
+pure func ConcatDropLast(xs, ys seq[int]) util.Unit {
+	return util.Unit{}
+}
+
+// Returns true if there are no duplicate values in the sequence.
+ghost
+decreases
+pure func HasNoDuplicates(xs seq[int]) bool {
+	return forall i, j int :: { xs[i], xs[j] } (0 <= i && i < j && j < len(xs)) ==> xs[i] != xs[j]
+}
+
+// If a sequence does not contain duplicates, dropping the first or last value
+// yields a sequence that does not contain the dropped value.
+ghost
+requires len(xs) > 0
+requires HasNoDuplicates(xs)
+ensures !(First(xs) in DropFirst(xs))
+ensures !(Last(xs) in DropLast(xs))
+decreases
+pure func DropExcludesValue(xs seq[int]) util.Unit {
+	return util.Unit{}
+}
+
+// Returns the index of the first occurrence of e in xs.
+// Use IndexOfReturnsFirst to instantiate the fact that the resulting index is
+// of the first occurrence.
+ghost
+requires e in xs
+ensures 0 <= result && result < len(xs)
+ensures xs[result] == e
+decreases xs
+pure func IndexOf(xs seq[int], e int) (result int) {
+	return First(xs) == e ? 0 : 1 + IndexOf(DropFirst(xs), e)
+}
+
+// IndexOf returns the first occurrence of e in xs.
+ghost
+requires e in xs
+requires 0 <= i && i < IndexOf(xs, e)
+ensures xs[i] != e
+decreases
+pure func IndexOfReturnsFirst(xs seq[int], e int, i int) util.Unit {
+	return quantifiedIndexOfReturnsFirst(xs, e)
+}
+
+ghost
+requires e in xs
+ensures forall i int :: { xs[i] } (0 <= i && i < IndexOf(xs, e)) ==> xs[i] != e
+decreases xs
+pure func quantifiedIndexOfReturnsFirst(xs seq[int], e int) util.Unit {
+	return First(xs) == e ? util.Unit{} : quantifiedIndexOfReturnsFirst(DropFirst(xs), e)
+}
+
+// Returns the index of the last occurrence of e in xs.
+// Use IndexOfLastReturnsLast to instantiate the fact the the resulting index is
+// of the last occurrence.
+ghost
+requires e in xs
+ensures 0 <= result && result < len(xs)
+ensures xs[result] == e
+decreases xs
+pure func IndexOfLast(xs seq[int], e int) (result int) {
+	return Last(xs) == e ? len(xs) - 1 : IndexOfLast(DropLast(xs), e)
+}
+
+// IndexOfLast returns the last occurrence of e in xs.
+ghost
+requires e in xs
+requires IndexOfLast(xs, e) < i && i < len(xs)
+ensures xs[i] != e
+decreases
+pure func IndexOfLastReturnsLast(xs seq[int], e int, i int) util.Unit {
+	return quantifiedIndexOfLastReturnsLast(xs, e)
+}
+
+ghost
+requires e in xs
+ensures forall i int :: { xs[i] } (IndexOfLast(xs, e) < i && i < len(xs)) ==> xs[i] != e
+decreases xs
+pure func quantifiedIndexOfLastReturnsLast(xs seq[int], e int) util.Unit {
+	return Last(xs) == e ? util.Unit{} : quantifiedIndexOfLastReturnsLast(DropLast(xs), e)
+}
+
+// Returns a sequence without the element at a given position.
+ghost
+requires 0 <= pos && pos < len(xs)
+ensures len(result) == len(xs) - 1
+ensures forall i int :: { result[i] } { xs[i] } (0 <= i && i < pos) ==> result[i] == xs[i]
+ensures forall i int :: { result[i] } (pos <= i && i < len(xs) - 1) ==> result[i] == xs[i+1]
+decreases
+pure func Remove(xs seq[int], pos int) (result seq[int]) {
+	return xs[:pos] ++ xs[pos+1:]
+}
+
+// Deletes the first occurrence of e in xs.
+ghost
+requires e in xs
+ensures len(result) == len(xs) - 1
+ensures forall i int :: { result[i] } { xs[i] } (0 <= i && i < IndexOf(xs, e)) ==> result[i] == xs[i]
+ensures forall i int :: { result[i] } (IndexOf(xs, e) <= i && i < len(xs) - 1) ==>
+	result[i] == xs[i+1]
+decreases
+pure func RemoveValue(xs seq[int], e int) (result seq[int]) {
+	return Remove(xs, IndexOf(xs , e))
+}
+
+// Inserts an element at a given position,
+ghost
+requires 0 <= pos && pos <= len(xs)
+ensures len(result) == len(xs) + 1
+ensures forall i int :: { result[i] } { xs[i] } (0 <= i && i < pos) ==> result[i] == xs[i]
+ensures result[pos] == e
+ensures forall i int :: { xs[i] } (pos <= i && i < len(xs)) ==> result[i+1] == xs[i]
+decreases
+pure func Insert(xs seq[int], e int, pos int) (result seq[int]) {
+	return xs[:pos] ++ Singleton(e) ++ xs[pos:]
+}
+
+// Reverses the sequence.
+ghost
+ensures len(result) == len(xs)
+ensures forall i int :: { result[i] } (0 <= i && i < len(xs)) ==>
+	result[i] == xs[len(xs)-i-1]
+decreases xs
+pure func Reverse(xs seq[int]) (result seq[int]) {
+	return IsEmpty(xs) ? Empty() : Prepend(Reverse(DropLast(xs)), Last(xs))
+}
+
+// Returns a constant sequence of a given length.
+ghost
+requires length >= 0
+ensures len(result) == length
+ensures forall i int :: { result[i] } (0 <= i && i < len(result)) ==> result[i] == e
+decreases length
+pure func Repeat(e int, length int) (result seq[int]) {
+	return length == 0 ? Empty() : Prepend(Repeat(e, length - 1), e)
+}
+
+// Returns the maximum of a non-empty sequence.
+ghost
+requires len(xs) > 0
+ensures forall k int :: { k in xs } (k in xs) ==> result >= k
+ensures result in xs
+decreases xs
+pure func Max(xs seq[int]) (result int) {
+	return let _ := DropFirstPrependFirst(xs) in
+	(IsSingleton(xs) ? First(xs) : math.Max(First(xs), Max(DropFirst(xs))))
+}
+
+// The maximum of the concatenation of two non-empty sequences is greater than
+// or equal to the maxima of its two non-empty subsequences.
+ghost
+requires len(xs) > 0 && len(ys) > 0
+ensures Max(xs ++ ys) >= Max(xs)
+ensures Max(xs ++ ys) >= Max(ys)
+ensures forall k int :: { k in xs ++ ys } (k in (xs ++ ys)) ==> Max(xs ++ ys) >= k
+decreases xs
+pure func MaxOfConcat(xs, ys seq[int]) util.Unit {
+	return let _ := ConcatDropFirst(xs, ys) in
+	(IsSingleton(xs) ? util.Unit{} : MaxOfConcat(DropFirst(xs), ys))
+}
+
+// Returns the minimum of a non-empty sequence.
+ghost
+requires len(xs) > 0
+ensures forall k int :: { k in xs } (k in xs) ==> result <= k
+ensures result in xs
+decreases xs
+pure func Min(xs seq[int]) (result int) {
+	return let _ := DropFirstPrependFirst(xs) in
+	(IsSingleton(xs) ? First(xs) : math.Min(First(xs), Min(DropFirst(xs))))
+}
+
+// The minimum of the concatenation of two non-empty sequences is less than or
+// equal to the minima of its two non-empty subsequences.
+ghost
+requires len(xs) > 0 && len(ys) > 0
+ensures Min(xs ++ ys) <= Min(xs)
+ensures Min(xs ++ ys) <= Min(ys)
+ensures forall k int :: { k in xs ++ ys } (k in xs ++ ys) ==> Min(xs ++ ys) <= k
+decreases xs
+pure func MinOfConcat(xs, ys seq[int]) util.Unit {
+	return let _ := ConcatDropFirst(xs, ys) in
+	(IsSingleton(xs) ? util.Unit{} : MinOfConcat(DropFirst(xs), ys))
+}
+
+// The maximum element in a non-empty sequence is greater than or equal to the
+// maxima of its non-empty subsequences.
+ghost
+requires 0 <= a && a < b && b <= len(xs)
+ensures Max(xs[a:b]) <= Max(xs)
+decreases
+pure func MaxOfSubseq(xs seq[int], a, b int) util.Unit {
+	return util.Asserting(Max(xs[a:b]) in xs)
+}
+
+// The minimum element in a non-empty sequence is less than or equal to the
+// minima of its non-empty subsequences.
+ghost
+requires 0 <= a && a < b && b <= len(xs)
+ensures Min(xs[a:b]) >= Min(xs)
+decreases
+pure func MinOfSubseq(xs seq[int], a, b int) util.Unit {
+	return util.Asserting(Min(xs[a:b]) in xs)
+}
+
+// Flattens a sequence of sequences into a single sequence.
+ghost
+decreases xs
+pure func Flatten(xs seq[seq[int]]) seq[int] {
+	return len(xs) == 0 ? Empty() : xs[0] ++ Flatten(xs[1:])
+}
+
+// Flatten is distributive over concatenation.
+ghost
+ensures Flatten(xs ++ ys) == Flatten(xs) ++ Flatten(ys)
+decreases xs
+pure func FlattenConcat(xs, ys seq[seq[int]]) util.Unit {
+	return len(xs) == 0 ? util.Unit{} :
+	let _ := util.Asserting((xs ++ ys)[1:] == xs[1:] ++ ys) in
+	FlattenConcat(xs[1:], ys)
+}
+
+// Flattening a sequence containing a single sequence yields the sequence within.
+ghost
+ensures Flatten(seq[seq[int]]{xs}) == xs
+decreases
+pure func FlattenSingleton(xs seq[int]) util.Unit {
+	// See https://github.com/viperproject/silicon/issues/803 for an explanation
+	// of this proof.
+	return util.Asserting(Flatten(seq[seq[int]]{xs}[1:]) == Empty())
+}
+
+// The length of a flattened sequence of sequences xs is greater than or equal
+// to any of the lengths of the elements of xs.
+ghost
+requires 0 <= i && i < len(xs)
+ensures len(Flatten(xs)) >= len(xs[i])
+decreases xs
+pure func FlattenLengthGeSingleElementLength(xs seq[seq[int]], i int) util.Unit {
+	return i <= 0 ? util.Unit{} : FlattenLengthGeSingleElementLength(xs[1:], i-1)
+}
+
+// The length of a flattened sequence of sequences xs is less than or equal to
+// the length of xs multiplied by an upper bound for the length of the sequences
+// in xs.
+ghost
+requires forall i int :: { len(xs[i]) } (0 <= i && i < len(xs)) ==> (len(xs[i]) <= j)
+ensures len(Flatten(xs)) <= len(xs) * j
+decreases xs
+pure func FlattenLengthLeMul(xs seq[seq[int]], j int) util.Unit {
+	return len(xs) == 0 ? util.Unit{} : FlattenLengthLeMul(xs[1:], j)
+}
diff --git a/sets/sets.gobra b/sets/sets.gobra
index 42b96bd..a7d2eed 100644
--- a/sets/sets.gobra
+++ b/sets/sets.gobra
@@ -14,7 +14,7 @@
 // This package defines lemmas for sets commonly used in specifications.
 package sets
 
-import utils "utils"
+import "util"
 
 // A set is empty if it has cardinality 0.
 ghost
@@ -36,8 +36,8 @@ ghost
 requires IsEmpty(xs)
 ensures xs == Empty()
 decreases
-pure func EmptyIsUnique(xs set[int]) utils.Unit {
-	return utils.Unit{}
+pure func EmptyIsUnique(xs set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // An empty set doesn't have any elements.
@@ -45,8 +45,8 @@ ghost
 requires IsEmpty(xs)
 ensures !(e in xs)
 decreases
-pure func NotInEmpty(xs set[int], e int) utils.Unit {
-	return utils.Unit{}
+pure func NotInEmpty(xs set[int], e int) util.Unit {
+	return util.Unit{}
 }
 
 // A set is a singleton if it has cardinality 1.
@@ -71,8 +71,8 @@ requires IsSingleton(xs)
 requires e in xs
 ensures xs == SingletonSet(e)
 decreases
-pure func SingletonIsSingletonSet(xs set[int], e int) utils.Unit {
-	return let _ := choose(xs) in utils.Unit{}
+pure func SingletonIsSingletonSet(xs set[int], e int) util.Unit {
+	return let _ := choose(xs) in util.Unit{}
 }
 
 // Elements in a singleton set are equal to each other.
@@ -82,8 +82,8 @@ requires a in xs
 requires b in xs
 ensures a == b
 decreases
-pure func SingletonEquality(xs set[int], a int, b int) utils.Unit {
-	return let _ := choose(xs) in utils.Unit{}
+pure func SingletonEquality(xs set[int], a int, b int) util.Unit {
+	return let _ := choose(xs) in util.Unit{}
 }
 
 // Constructs a set with all integers in the range [a, b).
@@ -137,8 +137,8 @@ pure func AreDisjoint(xs, ys set[int]) bool {
 ghost
 ensures (xs == ys) == (forall e int :: {e in xs} {e in ys} ((e in xs) == (e in ys)))
 decreases
-pure func SetEquality(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func SetEquality(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // Definition of subset without quantifiers.
@@ -147,16 +147,16 @@ requires e in xs
 requires xs subset ys
 ensures e in ys
 decreases
-pure func InSubset(xs, ys set[int], e int) utils.Unit {
-	return utils.Unit{}
+pure func InSubset(xs, ys set[int], e int) util.Unit {
+	return util.Unit{}
 }
 
 // Subset relation is reflexive.
 ghost
 ensures xs subset xs
 decreases
-pure func SubsetIsReflexive(xs set[int]) utils.Unit {
-	return utils.Unit{}
+pure func SubsetIsReflexive(xs set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // Subset relation is transitive.
@@ -165,8 +165,8 @@ requires xs subset ys
 requires ys subset zs
 ensures xs subset zs
 decreases
-pure func SubsetIsTransitive(xs, ys, zs set[int]) utils.Unit {
-	return utils.Unit{}
+pure func SubsetIsTransitive(xs, ys, zs set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // If xs is a subset of ys and both have the same cardinality, they are equal.
@@ -175,8 +175,8 @@ requires xs subset ys
 requires len(xs) == len(ys)
 ensures xs == ys
 decreases
-pure func SubsetEquality(xs, ys set[int]) utils.Unit {
-	return utils.Asserting(len(ys setminus xs) == len(ys) - len(xs))
+pure func SubsetEquality(xs, ys set[int]) util.Unit {
+	return util.Asserting(len(ys setminus xs) == len(ys) - len(xs))
 }
 
 // Returns whether xs is a proper subset of ys.
@@ -190,16 +190,16 @@ pure func IsProperSubset(xs, ys set[int]) bool {
 ghost
 ensures (e in (xs union ys)) == ((e in xs) || (e in ys))
 decreases
-pure func InUnionInOne(xs, ys set[int], e int) utils.Unit {
-	return utils.Unit{}
+pure func InUnionInOne(xs, ys set[int], e int) util.Unit {
+	return util.Unit{}
 }
 
 // Union is commutative.
 ghost
 ensures (xs union ys) == (ys union xs)
 decreases
-pure func UnionIsCommutative(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func UnionIsCommutative(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // Union is idempotent.
@@ -207,8 +207,8 @@ ghost
 ensures (xs union ys) union ys == xs union ys
 ensures xs union (xs union ys) == xs union ys
 decreases
-pure func UnionIsIdempotent(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func UnionIsIdempotent(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // Add x to xs.
@@ -227,8 +227,8 @@ pure func Add(xs set[int], e int) (result set[int]) {
 ghost
 ensures (a in Add(xs, b)) == ((a == b) || a in xs)
 decreases
-pure func InAdd(xs set[int], a, b int) utils.Unit {
-	return utils.Unit{}
+pure func InAdd(xs set[int], a, b int) util.Unit {
+	return util.Unit{}
 }
 
 // If a is in xs, then a will remain in xs no matter what we add to it.
@@ -236,8 +236,8 @@ ghost
 requires a in xs
 ensures a in Add(xs, b)
 decreases
-pure func InvarianceInAdd(xs set[int], a, b int) utils.Unit {
-	return utils.Unit{}
+pure func InvarianceInAdd(xs set[int], a, b int) util.Unit {
+	return util.Unit{}
 }
 
 // Remove e from xs. Does not require e to be in xs.
@@ -254,8 +254,8 @@ pure func Remove(xs set[int], e int) (result set[int]) {
 ghost
 ensures (xs intersection ys) == (ys intersection xs)
 decreases
-pure func IntersectionIsCommutative(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func IntersectionIsCommutative(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // Intersection is idempotent.
@@ -263,16 +263,16 @@ ghost
 ensures (xs intersection ys) intersection ys == (xs intersection ys)
 ensures xs intersection (xs intersection ys) == (xs intersection ys)
 decreases
-pure func IntersectionIsIdempotent(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func IntersectionIsIdempotent(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // If e is in the difference xs - ys, then e must be in xs but not in ys.
 ghost
 ensures (e in (xs setminus ys)) == ((e in xs) && !(e in ys))
 decreases
-pure func InDifference(xs, ys set[int], e int) utils.Unit {
-	return utils.Unit{}
+pure func InDifference(xs, ys set[int], e int) util.Unit {
+	return util.Unit{}
 }
 
 // If ys contains e, then the difference xs - ys does not contain e.
@@ -280,16 +280,16 @@ ghost
 requires e in ys
 ensures !(e in (xs setminus ys))
 decreases
-pure func NotInDifference(xs, ys set[int], e int) utils.Unit {
-	return utils.Unit{}
+pure func NotInDifference(xs, ys set[int], e int) util.Unit {
+	return util.Unit{}
 }
 
 // If e is in the intersection of xs and ys, then e must be both in xs and ys.
 ghost
 ensures e in (xs intersection ys) == ((e in xs) && (e in ys))
 decreases
-pure func InIntersectionInBoth(xs, ys set[int], e int) utils.Unit {
-	return utils.Unit{}
+pure func InIntersectionInBoth(xs, ys set[int], e int) util.Unit {
+	return util.Unit{}
 }
 
 // If xs and ys are disjoint, adding and then removing one from the other
@@ -299,8 +299,8 @@ requires AreDisjoint(xs, ys)
 ensures (xs union ys) setminus xs == ys
 ensures (xs union ys) setminus ys == xs
 decreases
-pure func DisjointUnionDifference(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func DisjointUnionDifference(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // If e is in xs, removing and adding it back yields the original set.
@@ -308,8 +308,8 @@ ghost
 requires e in xs
 ensures Add(Remove(xs, e), e) == xs
 decreases
-pure func AddRemove(xs set[int], e int) utils.Unit {
-	return utils.Unit{}
+pure func AddRemove(xs set[int], e int) util.Unit {
+	return util.Unit{}
 }
 
 // If we remove e from the set xs, it doesn't matter whether we have added e
@@ -317,16 +317,16 @@ pure func AddRemove(xs set[int], e int) utils.Unit {
 ghost
 ensures Remove(Add(xs, e), e) == Remove(xs, e)
 decreases
-pure func RemoveAdd(xs set[int], e int) utils.Unit {
-	return utils.Unit{}
+pure func RemoveAdd(xs set[int], e int) util.Unit {
+	return util.Unit{}
 }
 
 // xs - {e} is a subset of xs.
 ghost
 ensures Remove(xs, e) subset xs
 decreases
-pure func SubsetRemove(xs set[int], e int) utils.Unit {
-	return utils.Unit{}
+pure func SubsetRemove(xs set[int], e int) util.Unit {
+	return util.Unit{}
 }
 
 // xs and ys are subsets of the union of xs and ys.
@@ -334,8 +334,8 @@ ghost
 ensures xs subset (xs union ys)
 ensures ys subset (xs union ys)
 decreases
-pure func SubsetUnion(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func SubsetUnion(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // The intersection of xs and ys are subsets of xs, and ys.
@@ -343,24 +343,24 @@ ghost
 ensures (xs intersection ys) subset xs
 ensures (xs intersection ys) subset ys
 decreases
-pure func SubsetIntersection(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func SubsetIntersection(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // The difference xs - ys is a subset of xs.
 ghost
 ensures (xs setminus ys) subset xs 
 decreases
-pure func SubsetDifference(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func SubsetDifference(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // The cardinality of a set is non-negative.
 ghost
 ensures len(xs) >= 0
 decreases
-pure func NonNegativeLen(xs set[int]) utils.Unit {
-	return utils.Unit{}
+pure func NonNegativeLen(xs set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // If xs is a subset of ys, then the cardinality of xs is less than or equal to the cardinality of ys.
@@ -369,8 +369,8 @@ ghost
 decreases xs, ys
 ensures xs subset ys ==> len(xs) <= len(ys)
 ensures IsProperSubset(xs, ys) ==> len(xs) < len(ys)
-pure func SubsetLen(xs, ys set[int]) utils.Unit {
-	return (!(xs subset ys) || len(xs) == 0) ? utils.Unit{} :
+pure func SubsetLen(xs, ys set[int]) util.Unit {
+	return (!(xs subset ys) || len(xs) == 0) ? util.Unit{} :
 		len(xs) == len(ys) ?
 			let _ := SubsetEquality(xs, ys) in
 			(let e := choose(xs) in
@@ -386,14 +386,14 @@ ghost
 ensures len(xs union ys) >= len(xs)
 ensures len(xs union ys) >= len(ys)
 decreases ys
-pure func UnionLenLower(xs, ys set[int]) utils.Unit {
-	return IsEmpty(ys) ? utils.Unit{} :
+pure func UnionLenLower(xs, ys set[int]) util.Unit {
+	return IsEmpty(ys) ? util.Unit{} :
 		let y := choose(ys) in
 		(let yr := Remove(ys, y) in
 		(y in xs ?
 			(let xr := Remove(xs, y) in
-			(let _ := utils.Asserting(xr union yr == Remove(xs union ys, y)) in UnionLenLower(xr, yr))) :
-			(let _ := utils.Asserting(xs union yr == Remove(xs union ys, y)) in UnionLenLower(xs, yr))))
+			(let _ := util.Asserting(xr union yr == Remove(xs union ys, y)) in UnionLenLower(xr, yr))) :
+			(let _ := util.Asserting(xs union yr == Remove(xs union ys, y)) in UnionLenLower(xs, yr))))
 }
 
 // The cardinality of a union of two sets is less than or equal to the cardinality of
@@ -401,8 +401,8 @@ pure func UnionLenLower(xs, ys set[int]) utils.Unit {
 ghost
 ensures len(xs union ys) <= len(xs) + len(ys)
 decreases
-pure func UnionLenUpper(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func UnionLenUpper(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // The cardinality of the intersection of xs and ys is less than or equal to the
@@ -410,10 +410,10 @@ pure func UnionLenUpper(xs, ys set[int]) utils.Unit {
 ghost
 ensures len(xs intersection ys) <= len(xs)
 decreases xs
-pure func IntersectLenUpper(xs, ys set[int]) utils.Unit {
-	return IsEmpty(xs) ? utils.Unit{} :
+pure func IntersectLenUpper(xs, ys set[int]) util.Unit {
+	return IsEmpty(xs) ? util.Unit{} :
 		let x := choose(xs) in
-		(let _ := utils.Asserting((Remove(xs, x)) intersection ys == Remove((xs intersection ys), x)) in
+		(let _ := util.Asserting((Remove(xs, x)) intersection ys == Remove((xs intersection ys), x)) in
 		(IntersectLenUpper(Remove(xs, x), ys)))
 }
 
@@ -421,23 +421,23 @@ pure func IntersectLenUpper(xs, ys set[int]) utils.Unit {
 ghost
 ensures len(xs setminus ys) <= len(xs)
 decreases
-pure func DifferenceLenUpper(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func DifferenceLenUpper(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 ghost
 ensures len(xs union ys) == len(xs) + len(ys) - len(xs intersection ys)
 decreases
-pure func UnionLenEq(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func UnionLenEq(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 ghost
 ensures len(xs setminus ys) == len(xs) - len(xs intersection ys)
 ensures len(xs setminus ys) + len(ys setminus xs) + len(xs intersection ys) == len(xs union ys)
 decreases
-pure func DifferenceLenEq(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func DifferenceLenEq(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // If e is in xs, adding it to xs doesn't change the cardinality.
@@ -446,8 +446,8 @@ ghost
 ensures (e in xs) ==> (len(Add(xs, e)) == len(xs))
 ensures !(e in xs) ==> (len(Add(xs, e)) == len(xs) + 1)
 decreases
-func AddLen(xs set[int], e int) utils.Unit {
-	return utils.Unit{}
+func AddLen(xs set[int], e int) util.Unit {
+	return util.Unit{}
 }
 
 // If e is in xs, removing it from xs reduces the cardinality by 1.
@@ -456,8 +456,8 @@ ghost
 ensures (e in xs) ==> (len(Remove(xs, e)) == len(xs) - 1)
 ensures !(e in xs) ==> (len(Remove(xs, e)) == len(xs))
 decreases
-func RemoveLen(xs set[int], e int) utils.Unit {
-	return utils.Unit{}
+func RemoveLen(xs set[int], e int) util.Unit {
+	return util.Unit{}
 }
 
 // If xs and ys are disjoint, the cardinality of their union is equal to the
@@ -466,8 +466,8 @@ ghost
 requires AreDisjoint(xs, ys)
 ensures len(xs union ys) == len(xs) + len(ys)
 decreases
-pure func DisjointUnionLen(xs, ys set[int]) utils.Unit {
-	return utils.Unit{}
+pure func DisjointUnionLen(xs, ys set[int]) util.Unit {
+	return util.Unit{}
 }
 
 // If xs solely contains integers in the range [a, b), then its size is 
@@ -477,6 +477,6 @@ requires forall i int :: { i in xs } i in xs ==> (a <= i && i < b)
 requires a <= b
 ensures len(xs) <= b - a
 decreases
-pure func BoundedSetLen(xs set[int], a, b int) utils.Unit {
+pure func BoundedSetLen(xs set[int], a, b int) util.Unit {
 	return SubsetLen(xs, Range(a, b))
 }
diff --git a/utils/verify.gobra b/util/util.gobra
similarity index 94%
rename from utils/verify.gobra
rename to util/util.gobra
index c5fd454..6703a81 100644
--- a/utils/verify.gobra
+++ b/util/util.gobra
@@ -22,16 +22,17 @@ const Uncallable bool = false
 
 ghost
 requires false
-func Unreachable()
+decreases
+func Unreachable() { }
 
 ghost
 ensures false
-decreases _
+decreases
 func IgnoreBranch()
 
 ghost
 ensures false
-decreases _
+decreases
 func TODO()
 
 ghost