# SolidityChip

## Overview:
SolidityChip adds support for proving statements about solidity operations over EVM storage in halo2 using axiom-core. It allows a user to prove a vector of witness values represents a primitive solidity type and provides methods for constraining the computation of these types to prove statements about values within ethereum storage. Given a supplied vector of witnesses, and a SolidityChip a user can constrain:
- The field elements of the witness values of the vector represent byte values range 0-255
- The supplied byte vector represents a primitive fixed or dynamic size solidity type:
- Fixed Size: bytes32, address, uint8, uint16, uint32, uint64, uint128, uint256
- Dynamic Size: bytes, string

- Given a user supplied solidity type `key` and fixed bytes32 `mapping_slot` the storage slot corresponding to the value of `key` for a solidity mapping `mapping(key => value)` is constrained as follows:
- (1): If `key` is a Fixed size solidity type, `key` is treated as a fixed size input and left padded to 32 bytes. The storage slot of the value of `key` for a solidity mapping `mapping(key => value)` is constrained as:
<br>`value_slot = fix_len_keccak256(left_pad_32(key) . mapping_slot)`<br>
To constrain left_pad_32 the value byte array of key is left 0-padded to 32 bytes and constrained to be a SafeType::Bytes32 value. Since both the padded `key` and `mapping_slot` are of constrained fixed length there concatenation is performed by directly appending there witness vectors without range check. To constrain the computation of the slot fixed length keccak is performed over 64 bytes.
- (2): If `key` is a Dynamic size solidity type, `key` is treated as a variable length input with associated `max_len` and assigned witness`var_len` supplied by the user. The storage slot of the value of `key` for a solidity mapping `mapping(key => value)` is constrained as:
<br>`value_slot = var_len_keccak256(key . mapping_slot)`<br>
Since `key` is a variable length input the concatenation of `key` and `mapping_slot` is performed by first concatenating `key` and `mapping_slot` and then right 0-padding the resulting concatenation to `max_len`. The concatenation is constrained in `phase1` of halo2's proving system by computing the RLC's of `key` up to `var_len`, `mapping_slot` up to its fixed length, and `concat` to the `var_len` + 32. To constrain the computation of the slot value variable length keccak is performed over the `var_len` + 32
## Description:

### Constraining a Vector of Assigned Witnesses is a Solidity Type
To represent a primitive solidity type, the user converts a vector of assigned witness values representing bytes into a `SafeType` or `AssignedBytes` then wraps it as an enum variant of `SolidityType`. `SafeType` constrains that the assigned witness values of the input witness vector are within the range of one byte. For fixed `SolidityType` variants `Address`, `Bytes32`, `Uint` the uint value of the bytes represented by the witnesses of inputted array are further constrained to be within the correct range for the number of bits the type represents i.e. uint8 = 0..255 and that the "byte array" has enough elements to support this range.

### Constraining a Solidity Mapping:
`SolidityChip` supplies functions that support proving the storage slot of a value corresponding to a solidity type `key` in a solidity mapping `mapping(key => value)` located in storage at `mapping_slot` represented as a `Bytes32` solidity type. A user instantiates a `EthChip` which implements `SolidityChip` and calls `parse_mapping_phase0` then `parse_mapping_phase1`. `parse_mapping_phase0` delegates how the mapping slot is calculated based on the `key` supplied by the user. If `key` is a variant of `SolidityType` that represents a fixed type the mapping slot value is constrained as explained in (1) if `key` is `SolidityType::NonValue` enum variant it is treated as a dynamic solidity type and variable length input and an additional witness value `var_len` wrapped within the enum variant is used to constrain the mapping slot value as described in (2). In both cases of `parse_mapping_phase0` witness assignment and computation is performed and the assigned concat value passed into zkevm::keccak to be computed in phase1. In `parse_mapping_phase1` rlc concatentation is performed to constrain the variable length computation for dynamic type keys.

### AssignedByte

Represents a variable length vector of bytes. Constrains field elements of witness values of to be within the range of bytes.

### VarAssignedBytes

Struct of AssigneBytes and AssignedValue. Associates a variable length byte vector with assigned value representing its variable length. Upon creation asserts that var_len.value() < value.len() (TODO: this should be a range check). Handles checks for variable length.

### SafeInt

Constrains a vector of assigned witness values represents a signed two's complement integer.

Constrains that the value of the array represents a two's compliment integer within a bit range.

Has bytes and assc. sign

1.) Constrain each element is a byte value
2.) Constrain the number of inputs is enough to hold TOTAL_BITS based on

### Utilities:

`bytes_to_assigned_bytes`:
- Converts a vector of byte values to a vector of assigned witness values within halo2.

### Tests:
- Pos Unit test for fixed SolidityType's types with on chain data sourced from the WETH contract `mapping(address => uint256)` asserting a test circuit that checks the concatenated value and resulting key are equal to the sourced data is satisfied.
- Pos Unit test for SolidityType::NonValue types with data sourced from deploying a test contract to a anvil mainnet fork with `mapping(bytes => uint256)` asserting a test circuit that checks the concatenated value and resulting key are equal to the sourced data is satisfied using halo2's mock prover.
- Pos Unit tests for SolidityType variants of NonValue, Address, Uint8, Uint16, Uint32, Uint64, Uint128, Uint256 that generate random assigned witness vectors of bytes, computes a ground truth concat value and slot value using ether-rs, and asserts a test circuit that checks the concatenated value and resulting key are equal to the sourced data is satisfied using halo2's mock prover
- Neg Unit test for SolidityType's checking that assertions on input values panic when invalid `max_len` and `var_len` parameters are passed.
- Pos property tests for Fixed and Dynamic SolidityType's that generate random assigned witness vectors of bytes, compute the ground truth concat value and slot value, asserts a test circuit that checks the concatenated value and resulting key are equal to the sourced data is satisfied using halo2's mock prover
- A benchmark that creates a circuit constrains the computation of 10 mapping slot and runs halo2's prover and verifier and asserts the circuit is satisfied

## Outcomes:
- A pull request to axion-core-working consisting of a solidity module that defines:
- A new module `solidity` in axiom-eth modeled after `storage`
- A Trait `SolidityChip` that `parse_mapping_phase0`, `parse_mapping_phase1`, `parse_mappings_phase0`, `parse_mappings_phase1`.
- An enum `ValueType` delineating the different ways solidity types are calculated in mappings
- Mock Prover test for generating a storage proof of a mapping
- Mock Prover test for generating multiple storage proofs of mapping in parallel in phase1
- Satisfiability tests for all types that could be a key of a mapping
- Benchmark of circuit
- Helper methods to convert from &[u8] to FixedByteArray/SafeTypes -> TBD

## TODO/Next Steps (Listed in priority):
- Finish Variable length keys
- Provide support for nested mappings
- Simpligy SolidityChip implementation by adding a trait abstraction for Value/NonValue types and using enum dispatch
- Add end to end test sourcing a storage proof to provide an example of usage of SolidityChip
- Add Support for two's complement Int solidity types by extending SafeTypes
- Support proving statements about of struct values and there members
- Support proving statements about values over multiple storage slots
- Support proving statements about packed storage slots