`add` / `sub` / `mul` on `Uint256` wrap — Solidity 0.8 semantics require explicit `safeAdd`

[fricoben]

What I was trying to do

Model ordinary Solidity 0.8+ arithmetic, which reverts with Panic(0x11)
on overflow / underflow:

// contracts/v1/lib/MathLib.sol:146-151
function plusInt256(uint256 a, int256 b) internal pure returns (uint256) {
    if (b < 0) {
        return a - uint256(-b);   // reverts if b > a  (underflow)
    }
    return a + uint256(b);         // reverts if a + b > type(uint256).max
}

https://github.com/term-structure/termmax-contract-v2/blob/64bd47b98e064c7fb91ab4a59b70520e0ec285d5/contracts/v1/lib/MathLib.sol#L146-L151

What I tried

Write the Verity body with the same shape as the Solidity source:

function plusInt256Body (a : Uint256, b : Int256) : Uint256 := do
  return (ite (b < 0) (sub a (toUint256 (sub 0 b))) (add a (toUint256 b)))

Why it failed

add and sub compile — but they correspond to the EVM ADD / SUB
opcodes and wrap mod 2^256, not revert. Solidity 0.8 a + b reverts
on overflow by default; Verity's add a b does not.

The only way to get Solidity-0.8 semantics today is to explicitly swap
every add / sub / mul for the safeAdd / safeSub / safeMul
family (see SafeCounter at https://veritylang.com/examples), for example:

let newCount ← requireSomeUint (safeAdd current 1) "Overflow"

which visually diverges from the Solidity source and requires choosing a
Verity error name (the Solidity Panic(0x11) selector has no first-class
Verity equivalent).

Default-semantics mismatch:

op	Solidity 0.8 default	Verity default
a + b	revert with Panic(0x11)	wrap mod 2^256
a - b	revert with Panic(0x11)	wrap mod 2^256
a * b	revert with Panic(0x11)	wrap mod 2^256

Reproduces on Verity 74d8fe20ffa2f5dbb94959f3dd40a62df6aa8224 (release
v1.0.0).