Binary search over a sorted List<Int> — returns the index or -1
Also includes lower_bound (first index >= target), the building block for insertion into a sorted array. Demonstrates: while loop, mid = (lo+hi)/2 with floor, negative-literal sentinel, and known-answer tests.
A Soma program from the algorithms part of the verified corpus: 50 lines, cells BinarySearch, BinarySearchTests. It passes soma check with soma 3.2.4.
How it is built
The cell BinarySearch declares 2 signals in its face: search(xs: List, target: Int) -> Int and lower_bound(xs: List, target: Int) -> Int. Handlers: search (line 14) and lower_bound (line 26).
The file also holds 1 test cell (BinarySearchTests) with 9 assertions, run by soma test.
The source
binary_search_list.cell
// Binary search over a sorted List<Int> — returns the index or -1.
// Also includes lower_bound (first index >= target), the building block for
// insertion into a sorted array. Demonstrates: while loop, mid = (lo+hi)/2
// with floor, negative-literal sentinel, and known-answer tests.
//
// soma test examples/corpus/algorithms/binary_search_list.cell
cell BinarySearch {
face {
signal search(xs: List, target: Int) -> Int
signal lower_bound(xs: List, target: Int) -> Int
}
on search(xs: List, target: Int) {
let lo = 0
let hi = len(xs) - 1
while lo <= hi {
let mid = floor((lo + hi) / 2)
if xs[mid] == target { return mid }
if xs[mid] < target { lo = mid + 1 } else { hi = mid - 1 }
}
return -1
}
// first index i with xs[i] >= target (== len(xs) if none)
on lower_bound(xs: List, target: Int) {
let lo = 0
let hi = len(xs)
while lo < hi {
let mid = floor((lo + hi) / 2)
if xs[mid] < target { lo = mid + 1 } else { hi = mid }
}
return lo
}
}
cell test BinarySearchTests {
rules {
assert search([1, 3, 5, 7, 9, 11], 7) == 3
assert search([1, 3, 5, 7, 9, 11], 1) == 0
assert search([1, 3, 5, 7, 9, 11], 11) == 5
assert search([1, 3, 5, 7, 9, 11], 4) == -1
assert search(list(), 4) == -1
assert lower_bound([1, 3, 5, 7], 5) == 2
assert lower_bound([1, 3, 5, 7], 4) == 2
assert lower_bound([1, 3, 5, 7], 0) == 0
assert lower_bound([1, 3, 5, 7], 99) == 4
}
}What the toolchain says
$ soma check binary_search_list.cell
✓ All checks passed.$ soma test binary_search_list.cell
test BinarySearchTests ...
✓ assert search([1, 3, 5, 7, 9, 11], 7) == 3
✓ assert search([1, 3, 5, 7, 9, 11], 1) == 0
✓ assert search([1, 3, 5, 7, 9, 11], 11) == 5
✓ assert search([1, 3, 5, 7, 9, 11], 4) == -1
✓ assert search(list(), 4) == -1
✓ assert lower_bound([1, 3, 5, 7], 5) == 2
✓ assert lower_bound([1, 3, 5, 7], 4) == 2
✓ assert lower_bound([1, 3, 5, 7], 0) == 0
✓ assert lower_bound([1, 3, 5, 7], 99) == 4
9 tests: 9 passed, 0 failed$ soma verify binary_search_list.cell
Verifying binary_search_list.cell...
BinarySearch/termination:
⚠ handler `search`: while-loop without provable termination bound (write `while [loop_bound(N)] cond { … }`, or a for-loop over a bounded range)
⚠ handler `lower_bound`: while-loop without provable termination bound (write `while [loop_bound(N)] cond { … }`, or a for-loop over a bounded range)
0 passed, 2 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK