# field-arithmetic-wraparound

> A directly published Field operation on preserved unsigned quantities may wrap without a proved bound.

Canonical: https://nightshade.dicksonwu.xyz/rules/field-arithmetic-wraparound.html
Release: Nightshade 0.1.1 (v0.1.1)

| Field | Value |
| --- | --- |
| Rule ID | `field-arithmetic-wraparound` |
| Severity | medium |
| Confidence | varies |
| Maturity | experimental |
| Selection | Opt-in |
| Policy intent | not required |
| Default enabled | no |
| Category | Other active opt-ins / Source structure and validation |
| Engine facts used | resolved-types, numeric-operands, successful-predicates, public-sinks |
| Release | v0.1.1 |

## Selection and scope

Not selected by default. Select it with `--detectors` or the `detectors` list in nightshade.json. Either one replaces profile selection, so list every rule you want.

```sh
./.nightshade/node_modules/.bin/nightshade ./contracts --detectors field-arithmetic-wraparound
./.nightshade/node_modules/.bin/nightshade detector show field-arithmetic-wraparound
```

The first command runs only this rule; `--detectors` takes a comma-separated list. The second prints the rule's metadata from your installed version.

Severity is review priority. It does not express exploitability or impact. Confidence is detector metadata, not a probability. All built-in rules are experimental.

Compiler scope: the engine supports the pinned profiles 0.28.0, 0.29.0, 0.30.0, 0.31.1, 0.33.0-rc.2, 0.34.0, 0.35.0-rc.1 and 0.35.0, with ZKIR2 by default. Support for this rule can be narrower; the rule documentation below states any narrower scope.

## Corpus checks

Synthetic corpus checks for this rule in the 0.1.1 proof run. A check counts only with compiler acceptance and complete analysis.

| Positive detected | Corrected quiet | Lookalike quiet | Other negative quiet | Incomplete |
| ---: | ---: | ---: | ---: | ---: |
| 1/1 | 1/1 | 1/1 | 0/0 | 0 |

No deviations were recorded for this rule.

These are behavior checks on synthetic fixtures, not a precision or recall estimate. See [evaluation](https://nightshade.dicksonwu.xyz/evaluation.md#synthetic-corpus).

## Rule documentation

From https://github.com/DicksonWu654/nightshade/blob/v0.1.1/docs/detectors/field-arithmetic-wraparound.md at v0.1.1.

### Description

This rule reports a directly published Field `+`, `-` or `*` expression when an
operand preserves a nonconstant Uint value through explicit conversion or implicit arithmetic coercion and the successful transaction does
not prove that the unreduced arithmetic stays within the Field range. Compact
Field arithmetic reduces modulo the field; performing a quantity operation in
Field can bypass the rejection behavior of checked unsigned arithmetic.

### Example and scenario

```compact
export circuit decrease(amount: Uint<64>): [] {
  const previous = balance as Uint<64>;
  balance = disclose((previous as Field) - (amount as Field));
}
```

When the amount exceeds the previous quantity, Field subtraction can publish a
large residue instead of rejecting underflow. Prefer checked Uint subtraction
before widening, or assert `previous >= amount` on the same immutable operands.
A later assertion on that same successful transaction also protects an earlier
atomic write. A guard on replacement storage, another Map lookup, or another
invocation of the same arithmetic helper does not protect these operands.

### Evidence and limitations

The shared engine assigns deterministic result identities only from the exact operator
and immutable operand identities/constants; unavailable identities remain fresh.
It retains immutable shallow operator operands, value-preserving
Uint conversion evidence and conservative integer envelopes. Same-pair orders,
scalar equality aliases, successful checked-cast domains on the same immutable
result, inherent ranges of proven scalar equality aliases, and excluded interval endpoints can discharge the rule. Cast domains
protect earlier writes and uncast aliases of that result; a different result or
exclusive history cannot borrow them. Domains are bounded at 256 per history and
charged against the shared abstract-value budget.
Addition/multiplication are safe when their unreduced maximum is below the Field
modulus. A checked result cast only discharges wrapping residues that are all
outside the successful result domain: a cast often rejects small-Uint subtraction
underflow, but addition/multiplication may wrap to small values that pass it.

Only successful histories contribute findings; earlier writes remain observable
when later overwritten. Findings group effects at the same operation site and
entry, without sharing guards between histories or helper invocations. An
exported return is an application output, not necessarily public ledger storage.

This is a bounded quantity-conversion rule, not general arithmetic verification.
Constant-only operations and generic Field-only algebra stay quiet. Nested
operator origins, arithmetic used only inside a hash or condition, arbitrary
quantity intent and algebraic safety identities are outside the shallow contract.
A pure Field balance/amount pair without a preserved Uint conversion is therefore
not covered. A potential interval wrap does not prove a feasible input or a
vulnerability. Intentional modular use of Uint-derived operands may match and
should receive a reasoned suppression after review.

Exact arithmetic and all successful predicates are required. Unsupported evidence
produces `arithmetic-evidence-unavailable`, `arithmetic-domain-incomplete` or
`arithmetic-constraints-incomplete`; review allowance exhaustion produces
`arithmetic-review-budget` or `arithmetic-domain-budget`. The allowance is 200,000 work units, in addition to
normal path/step/value budgets; exhaustion remains incomplete. The structural
applicability scan is bounded and conservatively enables observation if exhausted.
Exact arithmetic observation bypasses specialized compressed hash/fold histories,
so corpus completion must be measured when this rule is enabled.

## Suppress a match

If a match is intentional, suppress it on the line before with the exact rule ID and a reason of at least eight characters:

```compact
// nightshade-disable-next-line field-arithmetic-wraparound -- Reason this match is intentional
```

Diagnostics cannot be suppressed, and an unmatched directive for a selected rule makes analysis incomplete. See [configuration](https://nightshade.dicksonwu.xyz/configuration.md#suppress-an-intentional-match) for fingerprint suppressions and baselines.

## References

- [Rule source document at v0.1.1](https://github.com/DicksonWu654/nightshade/blob/v0.1.1/docs/detectors/field-arithmetic-wraparound.md)
- [Catalog entry in rules.json](https://nightshade.dicksonwu.xyz/rules.json)
- [All rules](https://nightshade.dicksonwu.xyz/rules.md#source-structure-and-validation)
- [Limitations](https://nightshade.dicksonwu.xyz/limitations.md)