Sound integer abstraction in nelli's symbolic executor

TL;DR

nelli’s symbolic walker encodes every integer as a bit-vector and then promotes a parameter to Z3’s unbounded Z3Int only where a static range analysis proves the two semantics agree over every value that parameter can take. On code with range-bounded parameters the promotion makes symexFind roughly 2 to 3 times faster end to end. On bit-manipulating code nothing is promoted and nothing changes. The design goal is that a proof that fails costs you performance and never correctness. The shipped version does not fully meet that goal yet: the proof covers a parameter’s own values and not the arithmetic done on it, and there is a reproducible wrong answer below to show for it. This post is what the analysis establishes today, what is written but not yet connected, and what that gap costs. It follows on from the nelli overview , which stated the rule without the argument underneath it.

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 slower to solve than the integer theory. How much slower is measured below.
• 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

A fixed-width Nim integer does one of two things when a result does not fit. Same program, three builds, Nim 2.2.10:

Unsigned arithmetic wraps in every build. Signed arithmetic raises unless checks are off, and since Nim 1.0 -d:release leaves them on. There is no build in which int32.high + 1 quietly becomes a larger number.

An unbounded integer models neither behavior. Take:

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

Ask what can happen for non-negative x and y. Over Z3Int, x + y < 0 ∧ x ≥ 0 ∧ y ≥ 0 is unsatisfiable, and the sum never leaves any window because there is no window. So a Z3Int walker reports that the branch is unreachable and that nothing raises.

It is wrong about both builds, in different ways. Under -d:danger, x = int32.high, y = 1 wraps to a negative number and takes the branch the walker called unreachable. Under the default and under -d:release the same input raises OverflowDefect, and the walker has no such path to report. The second failure is the worse one. An OverflowDefect in production is a crash, and it is the kind of thing you ran the tool to find.

A bit-vector encoding gets both right. Wrapping is what bit-vector addition does, and “this addition overflowed” is an exact predicate over the same bits. nelli’s default models the checked build: signed fixed-width add, subtract, and multiply each push Z3’s no-overflow and no-underflow predicates onto the path, and the walker forks a raising path where they can fail. Unsigned operations are skipped, because Nim does not raise there. Asking the walker whether OverflowDefect is reachable gives the runtime table back row for row:

Turning the arithmetic checks off in the settings models the wrapping build.

Notice what this means for promotion. The bit-vector encoding is what builds the overflow predicate. Promote a value to Z3Int and you do more than risk wrong arithmetic: you delete the fork that creates the defect path. So a promotion proof has two jobs. It has to show the arithmetic agrees, and it has to show the defect path it is about to remove was vacuous anyway. The last row of the table is the case where that holds. Two values in 0..1000 cannot overflow an int by addition, so sxUnsat is the true answer and promoting costs nothing.

This 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 machine semantics differ is every fixed-width arithmetic operation, because every one of them either wraps or raises where the unbounded version does neither. 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, but acting on it soundly takes a proof rather than a heuristic that fires when the shape looks right.

nelli’s default (integerSemantics = isOptimised) encodes every integer as a bit-vector, then promotes a parameter 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 parameter can take. The proof is the artifact and the speedup is what falls out of it, so when the proof fails the parameter stays a bit-vector. The invariant the design is built around is that a failed abstraction costs performance, never soundness. The shipped proof is narrower than that invariant needs. “What the gap costs” below shows where. 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

The decision is made once per integer parameter, at the point the walker allocates its symbolic value. A parameter is promoted when three things hold: it has a known range, that range fits inside the bit-vector window for its type, and it is not banned.

Ranges 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. This is the highest-yield source, and range-typed parameters are already idiomatic in nelli-heavy code because the property-testing side derives strategies straight from them .

Ranges from assertions in the function. When the type says nothing, the walker mines the body of the function under test for assert and assume statements of simple shapes: x >= K, x < K, conjunctions of those. Each one tightens the range recorded for x. A type-level range takes precedence when both exist.

There is one case where this mining has to be switched off. If the target of the search is “find an input that violates an assertion”, the mined ranges cannot be used. They would be asserted to the solver as initial constraints, the solver would then be looking for a violation of assert x <= 100 among inputs where x <= 100, and the search would come back empty for a reason that has nothing to do with the code. So the walker checks the target kind first and skips the mining for that one.

The ban scan. Before any of this, the walker scans the body for bit-twiddling: shl, shr, and, or, xor. Any integer parameter that appears in such an expression is banned from promotion for the whole run. There is no faithful unbounded-integer counterpart for those operations, so there is nothing to prove.

The window check. For width W signed the window is [-2^(W-1), 2^(W-1) - 1]; for unsigned it is [0, 2^W - 1]. A value whose range sits inside the window means the same thing as a bit-vector and as an integer. That containment is the proof, and each promotion is logged with the interval and the evidence it came from.

Written, tested, not connected

The original design goes one step further: interval arithmetic over derived variables. For anything computed from other variables, compose the source intervals (a + b gives [lo_a + lo_b, hi_a + hi_b], and so on) and keep a promotion only when every operation in the def-use chain stays inside the window.

That propagation exists in the repo as a pure module with its own tests. Nothing in the walker calls it yet. Promotion today is decided for parameters only, from the two range sources above, and an earlier version of this post described the derived-variable rule as shipped behavior.

The module is also narrower than I described. It has no rule for div or mod. Sound bounds for those depend on whether the divisor’s interval includes zero and on signedness, so the code declines and the comment says that div-heavy code stays in bit-vectors. Declining is the right failure here. A missing rule costs a promotion. A wrong rule would cost a witness.

What the gap costs

The window check proves that a parameter’s own values fit its type. It says nothing about values computed from it. And a promoted parameter does not carry its bit width into the integer theory, so arithmetic on it does not fork on overflow. (Stamping the width there was tried. It turned every comparison against such a parameter into a fresh fork, and one test suite went from under a minute to not finishing, so it was scoped out and the code says so.)

Put those together and there is a hole:

proc mul64(a, b: range[0'i64..4_000_000_000'i64]) =
  let c = a * b

Each parameter fits an int64 with room to spare, so both are promoted. The product can reach 1.6e19, which does not fit. Calling it with both arguments at the upper bound raises OverflowDefect. Asking the walker whether OverflowDefect is reachable:

The default says the crash cannot happen. That is a wrong answer, caused by the abstraction, in the mode this post recommends. It is the failure the unconnected interval module exists to prevent: the interval for a * b leaves the window, and under the designed rule both parameters would have stayed bit-vectors.

Until that is wired in, the honest guidance is this. Promotion is safe when the arithmetic on the promoted parameters cannot leave the type’s window, which covers loop bounds, indices, and small counters, and is where the speedup comes from. If you are hunting overflow defects in code that multiplies or accumulates range-typed values, use isExact.

A second, unrelated defect came out of the same probe. With the parameters typed range[0'i32..100000'i32], the product overflows int32 and raises at runtime, and both settings answer sxUnsat. The walker appears to lose the 32-bit base type of the range. That one is a plain bug and has nothing to do with promotion.

Where Z3Int and bit-vector values do meet, the walker reconciles the two operands to one representation before it dispatches the operation.

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 distrust the range analysis, and per the section above there is currently a reason to.
• 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 it buys, measured

Four small functions, each solved with isExact (bit-vectors always) and with the default isOptimised. Median of 5 runs. The benchmark asserts that both settings return the same verdict and that the promotions shown did fire.

These are end-to-end times for a symexFind call, walker included, on a machine that was doing other things. Across repeated runs the absolute times moved by 2 to 3x and the ratios held. Over ten promotable measurements, including a sweep of the loop bound from 8 to 32, the speedup ranged from 1.6x to 6.4x with a median of 2.55x. The summary I will stand behind is roughly 2 to 3x on code whose parameters carry ranges, and no change on code that manipulates bits. An earlier version of this post said one to two orders of magnitude. I had not measured it, and these functions do not show it.

The last row is the flip side, and it is the steadiest number in the table. Byte parsers and hash mixing run at full bit-vector cost, which is the correct floor for them. Both settings returned the same verdict on all four functions, and the benchmark asserts it. They do not always, as the section above shows. The abstraction is meant to be a performance optimization sitting on top of a correctness guarantee, and closing that gap is what makes it one.

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 .

Corrected 2026-09-17. The first version of this post described interval propagation over derived variables, and a mod interval rule, as shipped. The first is not wired in and the second does not exist. It also said ranges could be passed to symexFind as a constraint argument (they are mined from assertions in the function), that Nim integers wrap silently by default (signed overflow raises unless checks are off), and it quoted a speedup I had not measured. Checking those claims also turned up the overflow hole described above, which the first version did not know about.