// SPDX-License-Identifier: MIT
pragma solidity ^0.8;
/// Soundness PoC: `mem_opt::FmpPropagation::propagate_statements`
/// tracks the known FMP value across statements. Its MStore handler
/// detects FMP writes by `region == FreePointerSlot ||
/// resolved_offset == Some(0x40)`. For an mstore with a *dynamic*
/// offset whose runtime value happens to be 0x40 (but the simplifier
/// can't see that — e.g. `calldataload(...)`), neither condition
/// fires: the simplifier leaves `region == Unknown` because the
/// offset isn't a literal, and `resolve_offset` returns None because
/// the value isn't tracked in the local constants map. The
/// `fmp_value` stays stale.
///
/// A subsequent `mload(0x40)` IS recognized as an FMP load (because
/// 0x40 is a literal). FmpPropagation folds it to the stale literal
/// `fmp_value` at IR level — diverging from EVM which reads the
/// overwritten memory.
///
/// Both values (`0x100`, `0x200`) fit in the heap-size range so the
/// FMP-load range proof (`to_llvm.rs::apply_range_proof`) doesn't
/// affect this test.
contract FmpDynStoreBug {
fallback() external {
uint256 offset;
assembly {
// Set FMP via a recognized FMP-slot mstore.
mstore(0x40, 0x100)
// Caller passes 0x40 as calldata so offset = 0x40 at
// runtime, but the simplifier sees an opaque calldataload.
offset := calldataload(0)
// Dynamic-offset mstore. FmpPropagation can't tell this
// hits 0x40, so it doesn't invalidate the known fmp_value.
mstore(offset, 0x200)
let v := mload(0x40)
mstore(0x100, v)
return(0x100, 32)
}
}
}