Domain splitting

Some proofs are hard not because the code is big but because one input ranges over a huge space the solver struggles with in a single go, the classic case being wide integer arithmetic. Domain splitting cuts that input into slices, proves each slice on its own, and proves the slices cover the whole range so nothing is skipped.

The DSL

@BmcProof
fun `decode round-trips for every value`() {
    val v = anyLong()
    domainSplit(v in Long.MIN_VALUE..Long.MAX_VALUE) {
        slice(v >= 0)
        slice(v < 0)
    }
    check(decode(encode(v)) == v)
}

Each slice is verified as its own smaller proof, and bmc4j additionally proves the slices add up to the range you declared. If they don’t, that is a failure, not a silent pass, so you can trust the split as much as the slices.

Conditions can be passed separately, slice(v >= 10, v <= 99), which the engine assumes as two facts rather than one. Splitting on the digit-width or sign of a value, rather than on raw size, often lands each slice in a part of the space the solver finds easy.

A split can fan out into many slices. To run them in parallel across CI machines, see Sharding.