Mappings#

Mappings are the primary data structure in Solidity smart contracts. StrataSolidity has strong support for reasoning about mappings, including simple mappings, nested mappings, and mappings with computed keys.

Simple mappings#

mapping(address => uint256) public balances;

/// @custom:strata ensures balances[to] == old(balances[to]) + amount
function mint(address to, uint256 amount) external {
    balances[to] += amount;
}

Mapping access in specifications uses the same syntax as Solidity: balances[key].

Nested mappings#

Nested mappings (e.g., ERC20 allowances) are fully supported:

mapping(address => mapping(address => uint256)) public allowance;

/// @custom:strata requires allowance[from][msg.sender] >= amount
/// @custom:strata ensures allowance[from][msg.sender] == old(allowance[from][msg.sender]) - amount
/// @custom:strata modifies allowance[from][msg.sender]
function transferFrom(address from, address to, uint256 amount) external {
    require(allowance[from][msg.sender] >= amount, "Allowance exceeded");
    allowance[from][msg.sender] -= amount;
    balances[from] -= amount;
    balances[to] += amount;
}

Computed keys#

Mappings keyed by hash functions are supported — keccak256 and sha256 are modeled as uninterpreted functions:

mapping(bytes32 => uint256) public data;

/// @custom:strata ensures data[keccak256(abi.encodePacked(a, b))] == value
function store(address a, uint256 b, uint256 value) external {
    data[keccak256(abi.encodePacked(a, b))] = value;
}

The verifier treats keccak256 as a function that is consistent (same input → same output) but otherwise uninterpreted — it does not reason about the hash algorithm itself.

Mapping semantics#

Solidity mappings have infinite domain with default zero values — every key “exists” and maps to zero until explicitly set. StrataSolidity models this using SMT arrays with select/store operations, which faithfully captures this semantics.

Current limitation: struct fields through mappings#

Accessing struct fields through mapping values is not yet supported in specifications:

struct Payment { uint256 amount; bool captured; }
mapping(bytes32 => Payment) public payments;

/// @custom:strata ensures payments[id].amount == amt  // ❌ NOT SUPPORTED

Workaround: Flatten structs into separate mappings:

mapping(bytes32 => uint256) public paymentAmounts;
mapping(bytes32 => bool) public paymentCaptured;

/// @custom:strata ensures paymentAmounts[id] == amt  // ✅ SUPPORTED

See Current Limitations for details.