Cowrie Research

dark-forest-v0-3-rangeproof-lessthan-bit-length-precondition-omission-near-miss-2021-09-30

11 min read

Dark Forest v0.3 RangeProof / LessThan(bits) Bit-Length Precondition Omission Near Miss (2021-09-30)

  • Name: Dark Forest v0.3 RangeProof / LessThan(bits) bit-length precondition omission near miss
  • Date: 2021-09-30
  • Protocol: Dark Forest v0.3
  • Chain: Ethereum
  • Category: bit-length precondition omission / comparator width underconstraint / out-of-bounds coordinate near miss
  • Loss: no public exploitation was documented, but the game acknowledged that a malicious player could otherwise satisfy the coordinate range proof with oversized values and initialize or act at locations outside the intended bounded map radius
  • Summary: Dark Forest’s early Circom RangeProof logic tried to prevent coordinate-overflow tricks by routing signed-coordinate bounds through circomlib’s LessThan(bits) comparator. The bug was that LessThan(bits) only behaves as intended when both operands already fit inside the expected bit width; the circuit never proved that hidden precondition. In the original RangeProof(bits, max_abs_value) template, the shifted coordinate expression max_abs_value + in and the bound itself were fed into LessThan(bits) without any Num2Bits-style width proof. That meant a malicious witness could use larger field elements whose semantics wrapped outside the comparator’s intended domain, satisfy the proof, and make in-range mean something weaker than the game designers thought. Dark Forest fixed the bug by moving the width proof into the circuit itself: it added explicit Num2Bits checks for both the shifted coordinate and max_abs_value, widened the comparator calls to LessThan(bits+1), and made the range proof prove the hidden bit-length assumptions that had previously lived only in reviewer intuition.
  • Trigger / entry point:
    • Dark Forest’s Circom circuits used a reusable RangeProof helper to argue that a coordinate’s absolute value stayed below a configured maximum.
    • That helper delegated the actual comparison to circomlib’s LessThan(bits) template.
    • LessThan(bits) assumes its inputs already fit within the declared bit width.
    • The original RangeProof(bits, max_abs_value) template never proved that max_abs_value + in or max_abs_value satisfied that width requirement.
  • Root cause:
    • The circuit treated LessThan(bits) as if it were both a comparator and an input-width proof.
    • In reality, the comparator only made sense once the surrounding circuit had already constrained the operands into the expected width.
    • Because the bit-length assumption stayed implicit, the proved statement weakened from this coordinate is inside the intended bounded interval to this arithmetic relation holds for some field elements that happen to drive LessThan(bits) the right way.
    • The safety check against overflow therefore existed in code structure but not yet in full constraint semantics.
  • Failure path:
    1. A player chose witness values for in that were semantically outside the intended coordinate bound but still exploitable inside the field arithmetic seen by the circuit.
    2. The original RangeProof(bits, max_abs_value) computed max_abs_value + in and fed it into LessThan(bits)-based lower and upper bound checks.
    3. Because neither the shifted input nor max_abs_value had been range-constrained to the comparator’s intended width, LessThan(bits) was operating outside its semantic domain.
    4. The comparator could therefore return outputs consistent with an in-range witness even though the underlying coordinate was not inside the intended bounded interval.
    5. The proof would then certify a weaker statement than the game expected, reopening the coordinate-overflow / out-of-bounds-location risk the range proof was supposed to close.
  • What the attacker needed to be true:
    • The game had to rely on the original RangeProof(bits, max_abs_value) helper rather than the patched version.
    • The attacker had to control witness values for the coordinate input.
    • The circuit had to keep trusting LessThan(bits) without separately proving the bit length of the comparator operands.
    • No downstream contract or game logic could independently reject the resulting oversized coordinate once the proof was accepted.
  • Technical anatomy worth remembering:
    • This is a classic helper is fine, caller forgot the helper's domain assumptions bug. circomlib’s LessThan(bits) was not broken; the outer circuit simply treated it as stronger than it was.
    • The subtlety mattered because Dark Forest was already thinking about overflow. The bug was not nobody considered wide witnesses; it was the mitigation itself still depended on an unproved width precondition.
    • The production fix shows the real invariant location. Dark Forest did not replace LessThan; it added Num2Bits(bits+1) for in + (1 << bits) and Num2Bits(bits) for max_abs_value, then widened the comparator calls to LessThan(bits+1) so the comparison finally lived on a proved-width domain.
    • This incident is a clean proof-circuit reminder that range proof is not a label; it is the exact set of constraints that force the compared object into a range-safe representation before the comparison runs.
  • Representative circuits and artifacts:
    • Vulnerable helper shape published in the Dark Forest circuit writeup: template RangeProof(bits, max_abs_value) using two LessThan(bits) comparators without explicit width proofs on the inputs
    • Vulnerable comparator dependency: circomlib LessThan(n)
    • Fixed helper: template RangeProof(bits) with explicit Num2Bits(bits+1) and Num2Bits(bits) checks plus LessThan(bits+1) comparisons
    • Public writeup that disclosed the subtle bug: ZKPs for Engineers: A look at the Dark Forest ZKPs (Bonus 1: Range Proofs)
    • Public fix commit: darkforest-eth/circuits@1b5c8440a487614d4a3e6ed523df0aee71a05b6e
  • Response / mitigation:
    • Dark Forest updated the published circuit design and production range-proof implementation to add the missing width constraints.
    • The fixed RangeProof(bits) explicitly proves that both max_abs_value and the shifted signed input fit inside the widths that make the comparator meaningful.
    • The durable lesson is that helper-gadget preconditions belong in constraints, not in code comments or reviewer background knowledge.

Pattern tags

  • bit-length-precondition-omission
  • Dark Forest’s RangeProof looked like an overflow defense, but the LessThan(bits) comparators were only sound once the circuit had separately proved that the compared values actually fit in the expected width.
  • The decisive failure was not comparison output ignored; it was comparison consumed with hidden domain assumptions still unproved.

Three range-boundary promotions this incident collapsed

  1. A comparator-backed range-check object existed at all

    • Dark Forest really did wrap signed-coordinate bounds in a reusable RangeProof helper and really did call circomlib’s LessThan(bits) on the shifted coordinate and the configured bound.
    • That only answered the gadget-existence question: some range-looking helper sat next to the game boundary.

  2. That helper output was treated as canonical in-range truth for this exact coordinate object

    • The live bug sat here. The circuit quietly promoted the comparator returned the expected relation on these field elements into the shifted coordinate and bound had already been proved to live inside the comparator's semantic width domain.
    • In other words, Dark Forest treated a comparator result as map-bound truth before proving the hidden bit-length facts that made the comparator’s answer mean in range rather than merely satisfies this arithmetic relation under a wider field interpretation.

  3. That accepted range truth still deserved map-entry authority

    • Once the helper output was read as real coordinate-bounds truth, it could authorize world initialization or movement at locations the bounded-map design meant to exclude.
    • The dangerous authority question was therefore not only did the comparator run? but why did a comparator result earned on an unproved-width domain still get to decide where a player may exist in the game world?

Why the exploit worked

  • The original circuit used the right-looking primitive for the wrong proof shape. LessThan(bits) can support a range proof, but only after the circuit first proves its operands really are bits-wide values.
  • Dark Forest’s early helper skipped that step. It pushed a shifted signed coordinate and the claimed bound into LessThan(bits) directly, so the comparator’s output no longer had the narrow semantic meaning the surrounding game logic assumed.
  • That is why the bug sits in the bit-length precondition omission family rather than validation-output nonconsumption. The result bit was consumed; the hidden premise that made the result meaningful was not.
  • The fix’s structure is the important preserved lesson: prove width first, compare second.

Detection and audit pivots

  • Grep every Circom LessThan(bits), GreaterEqThan(bits), Num2Bits, or bound-check helper and ask where the compared values are themselves proven to fit the required width.
  • Distinguish output bit is enforced from output bit is semantically meaningful. A comparator can still be fully wired into the statement and remain unsafe if the surrounding circuit never constrained its domain.
  • For signed-coordinate or shifted-range constructions like max + in, range-check the shifted object directly rather than assuming the shift made it safe.
  • Fuzz boundary-adjacent witnesses that differ only by hidden width: honest in-range values, the same values with higher bits set, and field-wraparound variants should not all satisfy the same range proof.
  • When a team says we added a range proof to stop overflow, inspect the exact helper preconditions, not just the helper name.

Why this incident matters

  • It is one of the cleanest public examples of a proof helper being reused correctly at the API level but unsafely at the statement level.
  • It gives the corpus a concrete comparator-width exemplar for the bit-length precondition omission family, which otherwise risks staying too abstract.
  • It also preserves an important review habit for zk-heavy applications: if a gadget only works for n-bit inputs, the proof must establish n-bit inputs before the gadget’s output can become game truth.

Failure-prevention checklist

  • Treat every comparator width parameter as a hard precondition that must be re-proved at each call site.
  • Constrain shifted signed values like max + in directly; do not assume the arithmetic transformation itself keeps them inside the comparator’s semantic domain.
  • Add Num2Bits or equivalent width proofs before LessThan / GreaterEqThan style gadgets, not after the fact in prose.
  • Keep helper wrappers honest: if a template is called RangeProof, it should itself prove the width assumptions that make the comparison sound.
  • Test malicious witnesses that exceed the intended width while preserving the same apparent semantic claim.
  • During audits, separate helper output consumed bugs from helper precondition omitted bugs; both are dangerous, but they fail for different reasons.
  • Prefer library-local checked wrappers over open-coded gadget compositions that require each caller to remember invisible domain assumptions.
  • Document the exact semantic type of every coordinate, bound, and shifted comparison object before converting it into field arithmetic.

Audit prompts

  • Where is the proof that each LessThan(bits) operand is actually a bits-wide value?
  • If the circuit shifts a signed value before comparison, where is the proof that the shifted object still lives in the intended comparator domain?
  • Would adding higher bits to the witness preserve satisfiability even though the semantic coordinate is now out of bounds?
  • Is this circuit relying on a helper’s common usage pattern, or on an explicitly proven statement about the helper inputs?
  • Does the wrapper template prove width and representation, or does it merely expose a narrower-looking name over a looser gadget composition?
  • If the proof claims coordinate is inside map radius, what exact constraints turn that into more than comparator returned 1 on some field elements?

Lessons that should already be standard

  • We used a comparator is not the same claim as we proved a range.
  • Helper-gadget names are not constraints. Their documented preconditions must be reified in the surrounding circuit.
  • Consuming a validator output is insufficient if the validator was never operating on a proved-valid domain.
  • Shifted signed arithmetic is a favorite place for width assumptions to disappear behind tidy-looking algebra.
  • The cleanest fix is usually not a new gadget; it is proving the missing premise that made the original gadget meaningful.
  • Public zk writeups are worth revisiting after disclosure notes. Dark Forest’s own article now preserves the exact subtlety reviewers should watch for elsewhere.

Internal linkages

Control surface

Graph View

Backlinks