[PoC] Abstract symbolic multiplication (abst_evm_bvmul) for vault-style verification

[gustavo-grieco]

Description

Stacked on #996 (base branch poc-div-encoding). Extends the arithmetic
abstraction from division to multiplication — the missing piece for
verifying vault-style (ERC-4626) properties, where the hard part is the
nonlinear q·S ≤ q·A cancellation, not the division itself.

Symbolic×symbolic Mul is encoded as an uninterpreted function
abst_evm_bvmul (concrete / 0 / 1 / power-of-two factors stay native), with
no ground truth, so the solver never bit-blasts a symbolic product. Meaning
is given by sound lemmas only:

• commutativity, and 0/1 identities (x*0 == 0, x*1 == x)
• div×mul link: (x/y)*y <= x
• division monotonicity in the dividend, and anti-monotonicity in the divisor
• multiplication monotonicity, guarded by a cheap sufficient no-overflow
  condition x <= 2^128-1 && y <= 2^128-1 (so the product fits in 256 bits).
  This is the width-budget idea Halmos uses; it replaces the exact bound-free
  predicate extract 511 256 (zext x * zext y) = 0, whose 512-bit multiply was
  the dominant solver cost and timed out for large operands.
• mulDiv bound: for (x*y)/z, y <= z => (x*y)/z <= x (guarded by no-overflow)
• const-mul monotonicity: x <= y => c*x <= c*y for a literal c. Constant
  multiplies stay native bvmul, but a symbolic operand times a large constant
  is costly to bit-blast and compare; since c is concrete the exact no-overflow
  bound floor((2^256-1)/c) is computed at encode time, so the guard is one
  constant comparison.
• const cancellation: (c1*x)/c2 == (c1/c2)*x for literals with c2 | c1 (its
  special case c1==c2 gives (c*x)/c == x). The multiply stays native bvmul
  but the surrounding divide is abstracted, so a precision-scaling wrapper
  (x * 1e18 / 1e18, the identity, or the rescale x * 1e18 / 1e6 == x * 1e12) is
  not otherwise provably exact; this pins it, under the encode-time bound
  floor((2^256-1)/c1). It fires when the divisor literal divides the multiplier
  literal.
• nested-division collapse: (A/c1)/c2 == A/(c1*c2) for literals c1,c2 with
  c1*c2 < 2^256. Two successive constant divides of an abstracted quotient stay
  uninterpreted and unrelatable to the single combined divide; this folds them, so
  a two-step constant rescale (A / 1e9 / 1e18 == A / 1e27) is equatable with its
  one-step form. The collapsed single divide A/(c1*c2) is also added to the div
  set, so the lemmas below (const-cancel, fraction-reduce, telescoping) match code
  that splits precision across two divides (e.g. _getSUsdsValue's x*rate/1e9/1e18,
  whose collapsed x*rate/1e27 is what they key on) — not only the one-step form.
• fraction-reduce: (c1*x)/c2 == x/(c2/c1) for literals with c1 | c2. The mirror
  of const cancellation (which needs c2 | c1): this is the c1 | c2 direction —
  multiply by a small constant, divide by a large one — such as x * 1e6 / 1e18 == x / 1e12 (precision scaling down, e.g. converting to a lower-decimal token).
  Sound because, under the same encode-time bound floor((2^256-1)/c1), c1*x is
  exact and floor(c1*x / (c1*k)) = floor(x/k). It fires when the multiplier
  literal divides the divisor literal (and c1 != c2, the const-cancel case).
• ceilDiv-cancel: the round-up sibling of const-cancel. OpenZeppelin
  Math.ceilDiv(c1*x, c2) is (c1*x == 0) ? 0 : (c1*x - 1)/c2 + 1, so the
  abstracted divide is over the c1*x - 1 dividend. When c2 | c1 the product is
  always a multiple of c2, hence ceil == floor and the whole ceilDiv collapses to
  (c1/c2)*x; the lemma pins the inner divide — for x >= 1,
  (c1*x - 1)/c2 == (c1/c2)*x - 1 (then +1 recovers (c1/c2)*x), under the same
  floor((2^256-1)/c1) bound. This discharges round-up precision conversions that
  scale to a coarser unit exactly (e.g. an 18→6→18-decimal ceilDiv(x*1e18, 1e6) == x*1e12).
• cancellation synthesis: when an abstract product a*b has a factor reused as a
  divisor elsewhere, the synthetic exact division (a*b)/b is added to the div
  set, letting the lemmas above bridge nested divisions ((a*b)/b <= a plus
  div-monotonicity across the shared divisor). This is what proves cross-divisor
  round-trips like ((x*s)/a)*a/s <= x, and it also discharges Solidity 0.8's
  div(mul(a,b),a) overflow guards, so checked arithmetic proves as written.
• scaled-product telescoping: (a*b)/c - (a*(b-k))/c == a*(k/c) for a literal
  divisor c and literal step k with c | k (no-overflow guarded, and b >= k
  so the step is a true difference). Every lemma above relates a product to a
  constant or to itself; this is the only one that pins the EXACT difference of
  two distinct abstract products. It discharges value-change accounting — the
  recurring vault-test shape "Δvalue == driver × rate-delta" — e.g.
  susds*rate/1e27 - susds == susds*(rate-1e27)/1e27. Sound because
  a*b = a*(b-k) + a*k and a*k is an exact multiple of c, so removing it shifts
  the floor by exactly a*(k/c).

Operand bounding (e.g. require(x < 2**128)) is supplied in Solidity. Enabled by
the same --abstract-arith flag as #996.

Soundness

hevm stays sound — it is a prover here, never a source of false bugs:

• A QED is a real proof: every lemma over-approximates real EVM arithmetic, so
  unsat under abstraction implies unsat in reality.
• Because abst_evm_bvmul is uninterpreted, a SAT model may assign products
  inconsistent with real multiplication, so a counterexample cannot be trusted.
  When the mul abstraction is active a SAT result is downgraded to Unknown
  rather than reported. Division-only counterexamples (division is exact via its
  ground truth) are unaffected.
• The lemmas are mutually consistent: the *-not-unsound tests confirm
  genuinely-false properties stay Unknown (never a spurious QED) and the
  *-cex-preserved tests confirm real counterexamples are still reported.

Properties it proves

Monotonicity of conversion functions (more in ⇒ at least as much out; a higher
backing ratio ⇒ at least as much value), divisor ordering, mulDiv bounds, and
cross-divisor round-trips (convertToAssets(convertToShares(x)) <= x and its
reverse — value in/out cannot increase across a round-trip). The const-cancel and
nested-division-collapse lemmas additionally prove exact-value constant-rescale
identities (e.g. a x * 1e18 / 1e6 precision conversion equals x * 1e12) — a
qualitative step past the relational facts above, since an abstracted divide
otherwise leaves the quotient uninterpreted. All are unknown natively (the
nested symbolic products bit-blast) and QED with --abstract-arith.

Example

A minimal ERC-4626 vault, ordinary checked arithmetic. Share-price monotonicity
and the round-trip both prove QED with --abstract-arith (and unknown
natively):

contract Vault {
    uint256 public totalAssets;
    uint256 public totalShares;

    function convertToShares(uint256 assets) public view returns (uint256) {
        if (totalAssets != 0) return assets * totalShares / totalAssets;
        return assets;
    }
    function convertToAssets(uint256 shares) public view returns (uint256) {
        if (totalShares != 0) return shares * totalAssets / totalShares;
        return shares;
    }

    // more assets in => never fewer shares minted
    function prove_shares_monotonic(uint256 a, uint256 b) external view {
        require(totalAssets != 0);
        require(a < 2**128 && b < 2**128 && totalShares < 2**128);
        require(a <= b);
        assert(convertToShares(a) <= convertToShares(b));
    }

    // value -> shares -> value never creates value
    function prove_roundtrip(uint256 x) external view {
        require(totalAssets != 0 && totalShares != 0);
        require(x < 2**128 && totalShares < 2**128 && totalAssets < 2**128);
        assert(convertToAssets(convertToShares(x)) <= x);
    }
}

Use bitwuzla (the bit-vector solver hevm defaults to): it discharges the
checked-arithmetic overflow guards that z3 struggles with on the deepest nested
round-trips. Both solvers are sound.

Verification status

Every property's result (QED / Unknown / CEX) was confirmed through the hevm
CLI locally (bitwuzla 0.8.2). The test group Mul-Abstraction runs in CI.

Known limitation: undefined symbol with abstracted arithmetic over storage-resolved values

The abstraction lemmas (assertPropsAbstract) are encoded over the raw props ps,
whereas SMT variables are declared from the eliminated props
(eliminateProps . concKeccak[Simp] . [decompose] $ ps). When a calldata value
reaches the abstracted arithmetic through storage — e.g. written into a mapping slot
via vm.store, or read back across a contract boundary — the lemma encoder
(exprToSMTWith) resolves the read to the calldata symbol, but the
variable-declaration pass (referencedVars over the eliminated props) represents it
differently and never declares it. The emitted lemma then mentions an undeclared
symbol and the solver errors:

[error] undefined symbol 'arg2'
while sending: (assert (= ... (abst_evm_bvudiv (bvmul (_ bv1000000000000000000 256) arg2)
                                               (_ bv1000000000000000000 256)) ...))

This is not unsoundness — the solver errors out and hevm reports the property as
unknown / partially-explored, never a spurious QED. But it turns some provable
properties into false negatives.

Observed on PSM3's previewWithdraw under --abstract-arith: a vm.store'd
shares[msg.sender] mapping read, plus a totalAssets formed as a sum of
cross-contract balance reads, feeding a general-branch round-up division. It does
not reduce to a small standalone contract — a single mapping store, a cross-contract
read, and the round-up ceilDiv each prove fine in isolation — so the divergence
depends on the specific elimination/decomposition of the combined query.

Partial fix direction: encoding the abstraction lemmas over the same eliminated
props the declarations use removes the vm.store-into-mapping class of this; a
deeper case remains for cross-contract balance reads that exprToSMTWith resolves
only inside nested arithmetic, where referencedVars still does not declare the
symbol. Left as a known limitation for now since it yields unknown, not a wrong
answer.

Checklist

• tested locally
• added automated tests (group Mul-Abstraction)
• updated the docs
• updated the changelog

[msooseth]

Wow, ok. I should really review and merge this #996 .... damn. Yeah, it's probably not totally stupid to merge #996. I'll have a look.

[gustavo-grieco]

Actually I have refactored and consolidated here: #1075 lets close this one