soma.cell

A FIFO queue and a sliding-window maximum over a List

Demonstrates: enqueue (push to the back) / dequeue (take from the front), returning a {value, rest} record from dequeue, and a windowed scan.

A Soma program from the algorithms part of the verified corpus: 48 lines, cells Queue, QueueTests. It passes soma check with soma 3.2.4.

How it is built

The cell Queue declares 3 signals in its face: enqueue(q: List, v: Int) -> List, dequeue(q: List) -> Map and window_max(xs: List, k: Int) -> List. Handlers: enqueue (line 15), dequeue (line 20) and window_max (line 28).

The file also holds 1 test cell (QueueTests) with 5 assertions, run by soma test.

Generated from soma describe on this file.

The source

queue.cell

// A FIFO queue and a sliding-window maximum over a List.
// Demonstrates: enqueue (push to the back) / dequeue (take from the front),
// returning a {value, rest} record from dequeue, and a windowed scan.
//
//   soma run  examples/corpus/algorithms/queue.cell window_max "[1,3,-1,-3,5,3,6,7]" 3
//   soma test examples/corpus/algorithms/queue.cell

cell Queue {
    face {
        signal enqueue(q: List, v: Int) -> List
        signal dequeue(q: List) -> Map
        signal window_max(xs: List, k: Int) -> List
    }

    on enqueue(q: List, v: Int) {
        return push(q, v)
    }

    // front element + the remaining queue, as a record
    on dequeue(q: List) {
        if len(q) == 0 { return Deque { value: (), rest: list() } }
        let rest = list()
        for i in range(1, len(q)) { rest = push(rest, q[i]) }
        return Deque { value: q[0], rest: rest }
    }

    // max of every contiguous window of width k
    on window_max(xs: List, k: Int) {
        let out = list()
        for i in range(0, len(xs) - k + 1) {
            let win = list()
            for j in range(i, i + k) { win = push(win, xs[j]) }
            out = push(out, max(win))
        }
        return out
    }
}

cell test QueueTests {
    rules {
        assert dequeue(enqueue(enqueue(list(), 7), 9)).value == 7
        assert to_string(dequeue([1, 2, 3]).rest) == to_string([2, 3])
        assert dequeue(list()).value == ()
        assert to_string(window_max([1, 3, -1, -3, 5, 3, 6, 7], 3)) == to_string([3, 3, 5, 5, 6, 7])
        assert to_string(window_max([4, 4, 4], 1)) == to_string([4, 4, 4])
    }
}

What the toolchain says

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

$ soma check queue.cell
✓ All checks passed.
$ soma test queue.cell
test QueueTests ...
  ✓ assert dequeue(enqueue(enqueue(list(), 7), 9)).value == 7
  ✓ assert to_string(dequeue([1, 2, 3]).rest) == to_string([2, 3])
  ✓ assert dequeue(list()).value == ()
  ✓ assert to_string(window_max([1, 3, -1, -3, 5, 3, 6, 7], 3)) == to_string([3, 3, 5, 5, 6, 7])
  ✓ assert to_string(window_max([4, 4, 4], 1)) == to_string([4, 4, 4])

5 tests: 5 passed, 0 failed
$ soma verify queue.cell
Verifying queue.cell...
No state machine in this program: nothing to prove beyond `soma check` (invariants and lifecycles are what verify proves).
VERIFY OK (vacuous — no state machine)
$ soma run queue.cell window_max "[1,3,-1,-3,5,3,6,7]" 3
[3, 3, 5, 5, 6, 7]

Builtins used

len, list, max, push, range, to_string

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