// SPDX-License-Identifier: MIT
pragma solidity ^0.8;
// Regression test: sub-underflow result widened to uint256 must preserve EVM
// modular semantics.
//
// Bug (crates/newyork/src/to_llvm.rs ~5977-5999): when `BinaryOperation::Sub`
// is codegen'd with both operands LLVM-narrowed to <= 64 bits (via
// `try_narrow_let_binding` Strategy 1 — structural proof from `and value, mask`)
// and the consumer's demand for the let binding holding the sub result is None
// (here: the result is mstored as a uint256), codegen takes the i128 fast-path:
// sub at i128 of (0, 1) → 2^128 - 1 (high bit set)
// Later widening via ensure_word_type → build_int_z_extend produces
// 0x...0000FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF instead of 2^256 - 1.
//
// Inline assembly is used so the masks land as IR constants (Solidity's
// non-asm path wraps integer literals through a `convert_rational_*` function,
// which defeats the structural narrowness proof).
/* runner.json
{
"differential": true,
"actions": [
{
"Instantiate": {
"code": { "Solidity": { "contract": "SubUnderflowZext", "solc_optimizer": false } }
}
},
{
"Call": {
"dest": { "Instantiated": 0 },
"data": "0aa7a67700000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001"
}
}
]
}
*/
contract SubUnderflowZext {
function sub_underflow(uint256 a, uint256 b) external pure returns (uint256 r) {
assembly {
let x := and(a, 0xff)
let y := and(b, 0xff)
r := sub(x, y)
}
}
}