Precision Loss & Rounding Errors

Domain

Web3 & smart contracts

ROOTVIEL support

Verified by ROOTVIEL — A deterministic, LLM-free verifier settles a specific property under stated assumptions — either a structural property over a graph, or an effect reproduced in execution. It does not by itself mean the whole system is secure, nor that an end-to-end exploit was run beyond what the evidence scope states.

Evidence scope

Observed in execution — Reproduced in an isolated sandbox or local fork — the effect was actually triggered under stated conditions.

Analysis family

RootRaven

CWE

CWE-682, CWE-1339

OWASP

SC03

Precision loss is the discrepancy between the exact mathematical result of a calculation and the integer value a contract actually computes and stores. Because EVM arithmetic is integer-only, any division discards the remainder — it rounds toward zero — and any fixed-point representation has a finite number of decimals. When the contract’s correctness depends on an exact ratio, share price, or fee, the discarded remainder becomes economically meaningful.

A rounding error is the specific case where the direction of truncation systematically benefits one side of a transaction. If the protocol rounds a user’s debt down and their collateral credit up, or mints shares rounding up while redeeming rounding down in the user’s favour, the aggregate of many small favourable roundings is a real, extractable transfer of value — with no overflow, no revert, and no single transaction that looks wrong.

Precision issues live in exactly the contracts that do the most arithmetic: anything that converts between a quantity and its value, or splits a pool among shareholders.

• ▸Vault / share accounting (ERC-4626-style): converting assets↔shares, where rounding direction decides who eats the dust.
• ▸Fee and interest math: basis-point fees computed as amount * bps / 10000, where small amounts round the fee to zero.
• ▸AMM and swap pricing: reserve ratios and invariants where truncation shifts the marginal price.
• ▸Reward distribution: per-share accumulators (acc * amount / 1e18) where residues accrue to or leak from the pool.
• ▸Fixed-point scaling: WAD/RAY (1e18 / 1e27) math where multiply-after-divide loses precision a divide-after-multiply would keep.

There are no fractional numbers on the EVM. Solidity’s integer division (DIV / SDIV) returns the quotient and silently drops the remainder, always rounding toward zero. There is no IEEE-754 float, and the fixed-point types the language reserves (fixed / ufixed) are not implemented. Every "decimal" in DeFi is therefore an integer scaled by a constant — 1e18 (WAD), 1e27 (RAY), or a token’s own decimals — and all rounding is a consequence of where division sits in the expression.

Because multiplication is exact up to the type’s range, the single most important rule is order of operations: compute a * b / c, not a / c * b. The former keeps full precision until the final divide; the latter truncates a / c first and then multiplies the error back up. The trade-off is that a * b may itself overflow, which is why precision-safe code uses a full-width mulDiv helper (512-bit intermediate) rather than naïve multiply-then-divide — precision and overflow are two faces of the same expression.

Truncation (round toward zero)

Integer division drops the remainder; 7 / 2 == 3, and (−7) / 2 == −3. The EVM never rounds to nearest.

WAD / RAY

Conventional fixed-point scales: 1e18 (18 decimals) and 1e27 (27 decimals). A "1.5x" factor is stored as 1.5e18.

Rounding direction

Whether a result is forced up or down. Safe protocols round in the protocol’s favour for every path so dust can never be extracted.

mulDiv

A full-precision floor((a*b)/denominator) computed via a 512-bit intermediate, avoiding both precision loss from early division and overflow from naïve multiply.

Dust / residue

The sub-unit remainder discarded by each division; harmless once, extractable when it accumulates or is amplified by scale.

The root cause is that a contract models a continuous quantity (a price, a ratio, a share of a pool) with discrete integers, and the quantisation error is not neutralised. Two sub-causes dominate: operation order that divides before multiplying (destroying precision that the type could have retained), and inconsistent rounding direction (rounding one leg of a conversion up and the inverse leg up as well, so a round-trip gains value).

Crucially, the result is in-range. The 0.8 overflow checks never trigger, no revert occurs, and each individual transaction is internally consistent. The defect only becomes visible as a conservation-of-value invariant violation across the whole system — the sum of what users can withdraw exceeds what was deposited, by the accumulated rounding. That is why this class hides so well and why it must be reasoned about as an invariant, not a line bug.

The classic form is "favourable-rounding round-tripping": the attacker repeatedly performs a conversion whose forward and reverse legs both round in their favour, pocketing a residue each cycle, often amplified by choosing amounts just below a rounding boundary.

1. 1The attacker identifies a conversion where rounding direction favours the caller — e.g. shares minted on deposit round such that a tiny deposit yields a disproportionate claim, or a redemption rounds the payout up.
2. 2They choose an amount near a truncation boundary so the discarded remainder is maximised relative to the amount (small amounts where amount * bps / 10000 rounds the fee to zero, or deposits that mint an extra share-unit).
3. 3They execute the favourable leg, capturing the residue; where the protocol pays out rounded-up and charges rounded-down, a single round-trip nets a sub-unit gain.
4. 4They repeat the cycle many times — cheaply if batched or flash-loan-funded — so the per-cycle dust accumulates into a material amount.
5. 5The pool’s backing now falls short of its outstanding claims by the accumulated residue; late or large holders absorb the shortfall.

A synthetic vault. The deposit path divides before multiplying and the fee rounds to zero for small amounts; the redeem path rounds the payout up. Each is innocuous alone; together a round-trip can extract value.

synthetic — do not use; order-of-ops + rounding direction
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

contract LossyVault {
    uint256 public totalAssets;
    uint256 public totalShares;
    mapping(address => uint256) public shares;

    // UNSAFE: divides before multiplying -> precision destroyed early.
    function depositShares(uint256 assets) public view returns (uint256) {
        if (totalShares == 0) return assets;
        // (assets / totalAssets) truncates to 0 for small assets,
        // then * totalShares keeps it 0 -> attacker pays, gets nothing,
        // OR for crafted ratios mints one extra unit.
        return (assets / totalAssets) * totalShares;
    }

    // UNSAFE: fee rounds to ZERO for small amounts.
    function feeOf(uint256 amount) public pure returns (uint256) {
        return amount * 30 / 10000;        // 0.30% ... but 30 wei -> 0 fee
    }

    // UNSAFE: redemption rounds payout UP in the caller's favour.
    function redeemAssets(uint256 shareAmt) public view returns (uint256) {
        // ceil division favouring the caller:
        return (shareAmt * totalAssets + (totalShares - 1)) / totalShares;
    }
}

• ▸Slow value leak: accumulated residue drains a pool’s backing over many transactions, so outstanding claims exceed assets held.
• ▸Fee evasion: amounts small enough to round the fee to zero let an attacker transact fee-free, starving protocol revenue.
• ▸Share mispricing: an early depositor or a crafted ratio can mint shares worth more than deposited, diluting everyone else (the seed of share-inflation attacks).
• ▸Cross-user unfairness: rounding that consistently favours the caller is a transfer from passive holders to active, boundary-seeking ones.

Precision loss is harder to detect than overflow because nothing reverts and no value goes out of range; the evidence is an invariant that drifts.

Static analysis

Flags divide-before-multiply patterns, fee expressions that can round to zero, and asymmetric rounding helpers. These are strong SIGNALS of a precision hazard but not proof that value is extractable.

Dynamic / differential testing

Compare the contract’s integer result against a high-precision reference (rational or big-decimal) for chosen inputs; a divergence beyond one unit in the wrong direction is concrete evidence for that input.

Symbolic execution

A solver can search for inputs that maximise the rounding residue or that make a round-trip profitable; a returned model is a counterexample. Division makes constraints harder, so timeouts mean UNKNOWN.

Fuzzing

Invariant fuzzers assert conservation properties (sum of redeemable ≤ totalAssets; round-trip of deposit→redeem never yields more than input) across random sequences. A broken invariant is a reproducible finding.

Formal verification

Prove a monotonicity/conservation property — e.g. that rounding always favours the protocol — with the SMTChecker or an external prover. The proof holds only for the modelled operations and scaling assumptions.

An autonomous investigator frames precision loss as "can a conservation invariant be driven negative?" and seeks a concrete, replayable sequence rather than reasoning about the algebra in prose.

1. 1Observe: locate conversion and fee expressions; note division order and rounding direction at each; mark boundary-sensitive amounts as candidates.
2. 2Hypothesise: state a profit claim ("depositing X then immediately redeeming returns > X" or "fee is 0 for amounts ≤ K"), including the exact invariant it would violate.
3. 3Experiment: deploy to a local chain, run the candidate sequence with boundary inputs (and repeat it N times to accumulate residue), recording balances before and after.
4. 4Collect evidence: the measured net gain/loss and the drift in the conservation invariant — numbers from execution, not from the model’s estimate.
5. 5Decide: promote to a finding only if a real sequence produced a net extraction or a genuine invariant break; otherwise UNKNOWN (dust below gas cost, or no profitable input found within budget).

RootRaven treats a precision hazard as a hypothesis and tries to extract value for real. It deploys the contract to a disposable local blockchain (or a local fork of real state), executes a candidate sequence of conversions at boundary inputs, and lets a deterministic, AI-free verifier compare measured balances and conservation invariants before and after. The model composes the candidate sequence; it does not decide whether value moved.

Observation

Divide-before-multiply, zero-rounding fees, and asymmetric rounding helpers are marked as candidate sites — SIGNALS only.

Hypothesis

A quantified claim: a specific sequence and input set should net positive to the caller or break a stated conservation invariant.

Experiment

Run the sequence on a local chain/fork, repeated to accumulate residue; measure assets in vs. claims out. No live-network attack mode.

Evidence

The recorded net transfer and the signed drift of the conservation invariant — raw numbers from execution.

Verification

A deterministic checker confirms net extraction exceeds zero (and exceeds gas, where relevant) and that the invariant moved against the protocol — no model in the loop.

Finding

Promoted only when real execution extracted value or broke conservation; a residue too small to extract, or no profitable input found, is UNKNOWN.

• ▸Order operations to multiply before dividing; use a full-precision mulDiv helper to keep precision without risking overflow in the intermediate.
• ▸Round consistently in the protocol’s favour on every path: mint shares rounding down, charge fees rounding up, pay redemptions rounding down — so a round-trip can never gain.
• ▸Make rounding direction explicit in the API (a Rounding.Up / Rounding.Down parameter) rather than implicit in expression order, following the ERC-4626 conversion conventions.
• ▸Guard against the dust-extraction edge: enforce a minimum deposit/mint, and seed the vault (or burn initial shares) so the first depositor cannot manipulate the ratio.
• ▸Reject amounts that round a fee or a share to zero, or treat them as a no-op, so boundary-seeking inputs gain nothing.
• ▸State and test a conservation-of-value invariant as a first-class property, not an afterthought.

The corrected vault multiplies before dividing via mulDiv, rounds every path in the protocol’s favour, and rejects dust-sized amounts. A round-trip can no longer gain because each leg rounds against the caller.

synthetic — multiply-before-divide + protocol-favouring rounding
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

library Math {
    // floor((a*b)/d) at full precision (512-bit intermediate omitted for brevity).
    function mulDiv(uint256 a, uint256 b, uint256 d) internal pure returns (uint256) {
        return (a * b) / d;            // illustrative; use a full mulDiv in practice
    }
}

contract TightVault {
    using Math for uint256;
    uint256 public totalAssets;
    uint256 public totalShares;

    // WHY: multiply first (full precision), floor-divide so SHARES round DOWN
    // (against the depositor). Reject dust that would mint zero shares.
    function sharesFor(uint256 assets) public view returns (uint256 s) {
        if (totalShares == 0) return assets;
        s = assets.mulDiv(totalShares, totalAssets);   // floor -> favours protocol
        require(s > 0, "amount too small");
    }

    // WHY: fee rounds UP, so no amount can round it to zero.
    function feeOf(uint256 amount) public pure returns (uint256) {
        return (amount * 30 + 9999) / 10000;           // ceil -> favours protocol
    }

    // WHY: redemption floors the payout (against the caller), so a
    // deposit->redeem round-trip never returns more than was put in.
    function assetsFor(uint256 shareAmt) public view returns (uint256) {
        return shareAmt.mulDiv(totalAssets, totalShares);  // floor
    }
}

Verify by asserting conservation and round-trip properties over randomized sequences and by checking that boundary amounts can no longer extract value. The sketches below are conceptual Foundry/Echidna-style tests, not guarantees.

conceptual — Foundry fuzz: round-trip never profitable
function testFuzz_roundTripNeverGains(uint256 assets) public {
    assets = bound(assets, 1, 1e24);
    uint256 s = vault.sharesFor(assets);
    vm.assume(s > 0);
    uint256 back = vault.assetsFor(s);
    assertLe(back, assets);            // floored both ways -> cannot gain
}

// Invariant: outstanding claims never exceed assets held.
function invariant_claimsBackedByAssets() public {
    assertLe(vault.redeemableTotal(), vault.totalAssets());
}

conceptual — Echidna property: fee never zero for nonzero amount
function echidna_fee_nonzero_for_nonzero() public view returns (bool) {
    uint256 a = _lastAmount();
    return a == 0 || vault.feeOf(a) > 0;   // ceil fee can't round to zero
}

• ▸In-range by nature: overflow checks never fire, so this class is invisible to overflow tooling; it needs invariant-level reasoning.
• ▸Economic threshold: a residue smaller than gas cost is not extractable; RootRaven reports such hazards as UNKNOWN rather than as findings.
• ▸Reference oracle problem: detection by differential testing is only as good as the high-precision reference model used for comparison.
• ▸Multi-contract accounting: residues that flow across contracts are hard to attribute; reproduction may be incomplete, leaving UNKNOWN.
• ▸Rounding is a trade-off, not a cure: a fix relocates dust to the protocol; "no leak" is not "no error".
• ▸Maturity caveat: straightforward single-vault round-trips reproduce well; sprawling fixed-point systems may resist a clean counterexample.

Precision loss is the in-range sibling of integer overflow — same arithmetic surface, no wrap — and it is the foundation of accounting and share-inflation attacks, where favourable rounding on an unseeded vault lets an early actor dilute everyone. Oracle manipulation often supplies the extreme ratio that makes a rounding edge profitable, and flash loans provide the capital to repeat a sub-unit round-trip enough times to matter.