Skip to content

[V12 near-miss] #79706/#79719 — range-check & decomposition soundness depends on fixed widths <=48 bits #68

Description

@n13

Context

From audits/chain-exploitability-analysis.md. Not exploitable today; usage-conditioned. Tracking umbrella: #64.

Findings

  • #79706 — Zero-width range decompositions leave values unconstrained. range_check(x, 0) is a no-op (empty split_le), adding no constraint.
  • #79719 — Decomposition helpers permit modulus-aliasing witnesses. When a decomposed width reaches ~64 bits (>= field modulus), distinct witnesses can alias mod p.

Why it's safe today

All wormhole range checks use fixed, nonzero widths <= 48 bits (2 / 14 / 32 / 48), which are strictly injective mod p, and none call range_check(x, 0) or a zero-width split_low_high side.

What would make it CRITICAL

  • A new constraint that range-checks near 64 bits → modulus aliasing (#79719).
  • Any range_check(x, 0) or zero-width split_low_high side → unconstrained value (#79706).

Action / guardrail

  • Keep range-check widths fixed and well below the field bit-width.
  • Consider asserting 0 < bits < 64 inside range_check / split_le so a zero or oversized width fails loudly instead of silently dropping the constraint.

Related audit category: #58 (Gate & constraint soundness).

Metadata

Metadata

Assignees

No one assigned

    Labels

    v12-auditV12 7xxxx-series audit remediation

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions