This is a follow-up to the nelli overview . There I said the symbolic-execution walker “abstracts a fixed-width integer to Z3Int only when a static range analysis proves the abstraction sound.” This is what that sentence actually means, and why it’s the only honest way to get the speed.

The choice

A symbolic executor has to hand every integer in your code to the solver in some encoding, and for Nim there are two honest options:

  • Z3BitVec[W]: a width-W bit-vector. Arithmetic wraps at the width, exactly like the machine. Correct, but Z3’s bit-vector theory is one to two orders of magnitude slower than its integer theory.
  • Z3Int: an unbounded mathematical integer. Fast to solve, but it never overflows, so it does not describe what your code actually does.

The question is how much of your program you can afford to hand to the fast one.

What “sound” has to mean here

symexFind returns an input that drives your code to a target: a branch, a defect, a state. The tool’s entire value is that the witness is real. So soundness means exactly this: if it hands you an input w and claims f(w) reaches target T, then running f(w) reaches T.

A walker that returns a witness relying on arithmetic the real semantics would reject, or that calls a branch unreachable when an overflow would in fact reach it, is unsound. It lies to you. For a tool whose pitch is “the witnesses are correct,” that is disqualifying, not a rough edge.

Nim makes the choice for you, almost

Nim’s default integer operations are silently modular. x + y on int32 wraps at runtime with no trap and no signal. That one fact settles more than it looks like it should: the runtime semantics of every fixed-width Nim integer operation is exactly bit-vector semantics. So any encoding that diverges from bit-vectors on fixed-width values is unsound in the sense above. Not a precision issue, a correctness one.

That kills the obvious fast path of using Z3Int everywhere. Take:

proc f(x: int32, y: int32): bool =
  x + y < 0

Ask whether that branch can fire for non-negative x and y. Over Z3Int, x + y < 0 ∧ x ≥ 0 ∧ y ≥ 0 is unsatisfiable, so the walker reports the branch unreachable. At runtime, x = int32.high, y = 1 wraps straight to a negative number and fires it. The Z3Int walker’s answer is a lie, and a single real test reveals it.

It also kills the naive hybrid, the one that uses Z3Int until a bit-vector-specific operation shows up and then switches. The set of operations whose integer and bit-vector semantics differ is every fixed-width arithmetic operation, because every one of them is silently modular. Widen the trigger set until it’s sound and it covers everything, and the hybrid collapses into bit-vectors everywhere.

Bit-vectors as the floor, a proof on top

So bit-vectors are the floor: always correct, a mirror of the hardware. The cost is that they are slow on exactly the cases that never needed them, like a counter that runs for i in 0..n with a small n, or a parameter typed range[0..100]. The intuition “0..100 plus 0..100 can’t overflow an int32, so why pay bit-vector cost” is correct. The sound way to act on it is not a trigger. It’s a proof.

nelli’s default (integerSemantics = isOptimised) encodes every integer as a bit-vector, then promotes a variable to Z3Int only when a static range analysis proves the promotion sound: proves that the bit-vector and integer semantics agree over every value the variable can take, for the operations applied to it. The proof is the artifact. The speedup is the consequence. When the proof fails, the variable stays a bit-vector. A failed abstraction costs performance, never soundness. Each promotion and its proof obligation are recorded on the path (Path.abstractions) so a run can be audited after the fact.

How the proof gets built

Three techniques, cheapest first.

Range types from the type system. range[0..100], Natural, Positive, and any user range subtype carry exact, decidable bounds at the type level. The walker reads the type and seeds the range table directly. This is the highest-yield technique, and range-typed parameters are already idiomatic in nelli-heavy code because the property-testing side derives strategies straight from them .

Refinement constraints from the predicate DSL. When you pass a constraint: proc(x: int): bool = x in 0..100 to symexFind, the parser extracts the range and seeds the table with it, in addition to asserting the same bound to the solver. Both happen and reinforce each other.

Interval arithmetic on derived variables. For anything computed from other variables, compose the source intervals: a + b gives [lo_a + lo_b, hi_a + hi_b], a mod b (for b > 0) gives [0, hi_b - 1], and so on. The abstraction succeeds for a variable if, and only if, every operation in its def-use chain produces an interval that fits in [T.low, T.high] without overflow. The moment one interval leaves that window, the variable demotes to a bit-vector for the rest of the path.

The composition is monotonic on purpose: once a variable is a bit-vector, anything downstream that consumes it inherits bit-vector. That is what stops you from reintroducing the unsoundness by accident, as a “mostly-Z3Int with a surprise bit-vector at the bottom” that no longer agrees with itself.

Bit-twiddling (shl, shr, and, or, xor, not) always forces a bit-vector. There is no faithful unbounded-integer counterpart, so the abstraction check is skipped for those operations outright, and Z3Int and bit-vectors meet at cast points bridged with Z3_mk_int2bv / Z3_mk_bv2int.

The escape hatches

Three settings, because the default shouldn’t be the only option:

  • isExact: bit-vectors always. Sound, slowest, simplest. The escape hatch if you ever distrust the range analysis itself.
  • isOptimised: the default described above.
  • isLoose: Z3Int everywhere, no soundness proof. It can produce false-positive witnesses, so it prints a banner on every run and is documented as a footgun. It exists only so researchers comparing configurations have the unsound baseline for parity, and it’s loud about what it is.

What you get

The dominant shape in real code (bounded loop counters, refinement-constrained parameters) solves at near-Z3Int speed. Byte parsers and hash mixing (the code that actually twiddles bits) run at full bit-vector cost, which is the correct floor for it. And nobody gets a wrong answer. The abstraction is a performance optimization sitting on top of a correctness guarantee, not a correctness compromise made for speed.

The full decision, options, and interval rules are in the repo’s ADR-0001 . Code and issues: github.com/coreyleavitt/nelli . The companion piece is why nelli mutates the choice sequence instead of the bytes .