Proof helpers

A proof body is ordinary code plus a few calls from org.bmc4j.Bmc. How it works covers the idea; this is the reference for the calls themselves.

import org.bmc4j.Bmc.*
import org.bmc4j.kotlin.assumeValid

Symbolic inputs

Each any... call stands for every value of its type at once. The solver is free to pick any of them while it looks for a counterexample.

Call	Ranges over
`anyInt()`, `anyInt(min, max)`	every `Int`, or a closed range
`anyLong()`, `anyLong(min, max)`	every `Long`, or a closed range
`anyBoolean()`	`true` or `false`
`anyByte()`, `anyChar()`	every `Byte` / `Char`
`anyDouble()`, `anyDouble(min, max)`	every `Double`, or a closed range
`anyString(maxLength)`, `anyString(min, max)`, `anyString(maxLength, alphabet)`	strings up to a length, optionally from a restricted alphabet

String length and modelling also interact with maxStringLength and the string mode.

Assumptions

Assumptions narrow the inputs the proof considers.

assume(condition) keeps only inputs where condition holds. assume(x > 0) proves the rest of the body for positive x only.
assumeValid { ... } (Kotlin) builds an object and prunes the inputs its constructor rejects, so validation written as require / init checks becomes the input domain. “Assume valid” means “assume construction didn’t throw.”
```
@JvmInline value class Port(val n: Int) { init { require(n in 1..65535) } }

val p = assumeValid { Port(anyInt()) }   // only 1..65535 survive
```
assumeUnreachable() prunes the current path outright. Reaching it is a contradiction, which is how assumeValid discards a rejected construction.

Assumptions are trusted, not checked: you are narrowing what the proof looks at, so make sure the condition is one you can rely on. Narrow too far and there’s nothing left to prove, which bmc4j reports as VACUOUS rather than a pass.

The property

check(condition) is the thing being proven. If any allowed input makes it false, the proof is refuted with that input as the counterexample. check(condition, message) adds a label to the failure.

You don’t always need a check. A proof with none still refutes on any exception, assertion, or error the code throws, which is the simplest way to prove a function never blows up. See Your First Proofs.