soma.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.

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.

Generated from soma describe on this file.

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

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ 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

Builtins used

floor, len, list

Source file: /corpus/algorithms/binary_search_list.cell · examples/corpus/algorithms/binary_search_list.cell