Skip to content

Commit

Permalink
cannon: Implement MIPS64Memory.sol (ethereum-optimism#12653)
Browse files Browse the repository at this point in the history
* cannon: Implement MIPS64Memory.sol

* add non-zero revert data; cleanup go-ffi script
  • Loading branch information
Inphi authored Oct 29, 2024
1 parent 4b1c12a commit 2780ad1
Show file tree
Hide file tree
Showing 6 changed files with 524 additions and 43 deletions.
1 change: 1 addition & 0 deletions packages/contracts-bedrock/.gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ kontrol_prove_report.xml

# Scripts
scripts/go-ffi/go-ffi
scripts/go-ffi/go-ffi-cannon64

# Environment Variables
.envrc
Expand Down
8 changes: 7 additions & 1 deletion packages/contracts-bedrock/justfile
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,15 @@ forge-build:
build: prebuild lint-fix-no-fail forge-build interfaces-check-no-build

# Builds the go-ffi tool for contract tests.
build-go-ffi:
build-go-ffi-default:
cd ./scripts/go-ffi && go build

# Builds the go-ffi tool for MIPS64 contract tests.
build-go-ffi-cannon64:
cd ./scripts/go-ffi && go build -tags=cannon64 -o ./go-ffi-cannon64

build-go-ffi: build-go-ffi-default build-go-ffi-cannon64

# Cleans build artifacts and deployments.
clean:
rm -rf ./artifacts ./forge-artifacts ./cache ./scripts/go-ffi/go-ffi ./deployments/hardhat/*
Expand Down
87 changes: 45 additions & 42 deletions packages/contracts-bedrock/scripts/go-ffi/differential-testing.go
Original file line number Diff line number Diff line change
Expand Up @@ -360,68 +360,71 @@ func DiffTestUtils() {
// Print the output
fmt.Print(hexutil.Encode(packed[32:]))
case "cannonMemoryProof":
// <pc, insn, [memAddr, memValue], [memAddr2, memValue2]>
// Generates a memory proof of `memAddr` for a trie containing memValue and memValue2
// <memAddr0, memValue0, [memAddr1, memValue1], [memAddr2, memValue2]>
// Generates memory proofs of `memAddr0` for a trie containing memValue0 and `memAddr1` for a trie containing memValue1 and memValue2
// For the cannon stf, this is equivalent to the prestate proofs of the program counter and memory access for instruction execution
mem := memory.NewMemory()
if len(args) != 3 && len(args) != 5 && len(args) != 7 {
panic("Error: cannonMemoryProofWithProof requires 2, 4, or 6 arguments")
}
pc, err := strconv.ParseUint(args[1], 10, 32)
memAddr0, err := strconv.ParseUint(args[1], 10, arch.WordSize)
checkErr(err, "Error decoding addr")
insn, err := strconv.ParseUint(args[2], 10, 32)
checkErr(err, "Error decoding insn")
mem.SetWord(arch.Word(pc), arch.Word(insn))
memValue0, err := strconv.ParseUint(args[2], 10, arch.WordSize)
checkErr(err, "Error decoding memValue0")
mem.SetWord(arch.Word(memAddr0), arch.Word(memValue0))

var insnProof, memProof [896]byte
var proof1 []byte
if len(args) >= 5 {
memAddr, err := strconv.ParseUint(args[3], 10, 32)
memAddr, err := strconv.ParseUint(args[3], 10, arch.WordSize)
checkErr(err, "Error decoding memAddr")
memValue, err := strconv.ParseUint(args[4], 10, 32)
memValue, err := strconv.ParseUint(args[4], 10, arch.WordSize)
checkErr(err, "Error decoding memValue")
mem.SetWord(arch.Word(memAddr), arch.Word(memValue))
memProof = mem.MerkleProof(arch.Word(memAddr))
proof := mem.MerkleProof(arch.Word(memAddr))
proof1 = proof[:]
}
if len(args) == 7 {
memAddr, err := strconv.ParseUint(args[5], 10, 32)
memAddr, err := strconv.ParseUint(args[5], 10, arch.WordSize)
checkErr(err, "Error decoding memAddr")
memValue, err := strconv.ParseUint(args[6], 10, 32)
memValue, err := strconv.ParseUint(args[6], 10, arch.WordSize)
checkErr(err, "Error decoding memValue")
mem.SetWord(arch.Word(memAddr), arch.Word(memValue))
memProof = mem.MerkleProof(arch.Word(memAddr))
proof := mem.MerkleProof(arch.Word(memAddr))
proof1 = proof[:]
}
insnProof = mem.MerkleProof(arch.Word(pc))
proof0 := mem.MerkleProof(arch.Word(memAddr0))

output := struct {
MemRoot common.Hash
Proof []byte
}{
MemRoot: mem.MerkleRoot(),
Proof: append(insnProof[:], memProof[:]...),
Proof: append(proof0[:], proof1...),
}
packed, err := cannonMemoryProofArgs.Pack(&output)
checkErr(err, "Error encoding output")
fmt.Print(hexutil.Encode(packed[32:]))
case "cannonMemoryProof2":
// <pc, insn, [memAddr, memValue], memAddr2>
// Generates a memory proof of memAddr2 for a trie containing memValue
// <memAddr0, memValue0, [memAddr1, memValue1], memAddr2>
// Generates memory proof of `memAddr2` for a trie containing `memValue0` and `memValue1`
mem := memory.NewMemory()
if len(args) != 6 {
panic("Error: cannonMemoryProofWithProof2 requires 5 arguments")
}
pc, err := strconv.ParseUint(args[1], 10, 32)
memAddr0, err := strconv.ParseUint(args[1], 10, arch.WordSize)
checkErr(err, "Error decoding addr")
insn, err := strconv.ParseUint(args[2], 10, 32)
checkErr(err, "Error decoding insn")
mem.SetWord(arch.Word(pc), arch.Word(insn))
memValue0, err := strconv.ParseUint(args[2], 10, arch.WordSize)
checkErr(err, "Error decoding memValue0")
mem.SetWord(arch.Word(memAddr0), arch.Word(memValue0))

var memProof [896]byte
memAddr, err := strconv.ParseUint(args[3], 10, 32)
var memProof [memory.MemProofSize]byte
memAddr, err := strconv.ParseUint(args[3], 10, arch.WordSize)
checkErr(err, "Error decoding memAddr")
memValue, err := strconv.ParseUint(args[4], 10, 32)
checkErr(err, "Error decoding memValue")
mem.SetWord(arch.Word(memAddr), arch.Word(memValue))
memValue1, err := strconv.ParseUint(args[4], 10, arch.WordSize)
checkErr(err, "Error decoding memValue1")
mem.SetWord(arch.Word(memAddr), arch.Word(memValue1))

memAddr2, err := strconv.ParseUint(args[5], 10, 32)
memAddr2, err := strconv.ParseUint(args[5], 10, arch.WordSize)
checkErr(err, "Error decoding memAddr")
memProof = mem.MerkleProof(arch.Word(memAddr2))

Expand All @@ -436,27 +439,27 @@ func DiffTestUtils() {
checkErr(err, "Error encoding output")
fmt.Print(hexutil.Encode(packed[32:]))
case "cannonMemoryProofWrongLeaf":
// <pc, insn, memAddr, memValue>
// <memAddr0, memValue0, memAddr1, memValue1>
mem := memory.NewMemory()
if len(args) != 5 {
panic("Error: cannonMemoryProofWrongLeaf requires 4 arguments")
}
pc, err := strconv.ParseUint(args[1], 10, 32)
checkErr(err, "Error decoding addr")
insn, err := strconv.ParseUint(args[2], 10, 32)
checkErr(err, "Error decoding insn")
mem.SetWord(arch.Word(pc), arch.Word(insn))

var insnProof, memProof [896]byte
memAddr, err := strconv.ParseUint(args[3], 10, 32)
checkErr(err, "Error decoding memAddr")
memValue, err := strconv.ParseUint(args[4], 10, 32)
checkErr(err, "Error decoding memValue")
mem.SetWord(arch.Word(memAddr), arch.Word(memValue))
memAddr0, err := strconv.ParseUint(args[1], 10, arch.WordSize)
checkErr(err, "Error decoding memAddr0")
memValue0, err := strconv.ParseUint(args[2], 10, arch.WordSize)
checkErr(err, "Error decoding memValue0")
mem.SetWord(arch.Word(memAddr0), arch.Word(memValue0))

var insnProof, memProof [memory.MemProofSize]byte
memAddr1, err := strconv.ParseUint(args[3], 10, arch.WordSize)
checkErr(err, "Error decoding memAddr1")
memValue1, err := strconv.ParseUint(args[4], 10, arch.WordSize)
checkErr(err, "Error decoding memValue1")
mem.SetWord(arch.Word(memAddr1), arch.Word(memValue1))

// Compute a valid proof for the root, but for the wrong leaves.
memProof = mem.MerkleProof(arch.Word(memAddr + 32))
insnProof = mem.MerkleProof(arch.Word(pc + 32))
memProof = mem.MerkleProof(arch.Word(memAddr1 + arch.WordSize))
insnProof = mem.MerkleProof(arch.Word(memAddr0 + arch.WordSize))

output := struct {
MemRoot common.Hash
Expand Down
176 changes: 176 additions & 0 deletions packages/contracts-bedrock/src/cannon/libraries/MIPS64Memory.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,176 @@
// SPDX-License-Identifier: MIT
pragma solidity 0.8.15;

import "src/cannon/libraries/CannonErrors.sol";

library MIPS64Memory {
uint64 internal constant EXT_MASK = 0x7;
uint64 internal constant MEM_PROOF_LEAF_COUNT = 60;
uint256 internal constant U64_MASK = 0xFFFFFFFFFFFFFFFF;

/// @notice Reads a 64-bit word from memory.
/// @param _memRoot The current memory root
/// @param _addr The address to read from.
/// @param _proofOffset The offset of the memory proof in calldata.
/// @return out_ The hashed MIPS state.
function readMem(bytes32 _memRoot, uint64 _addr, uint256 _proofOffset) internal pure returns (uint64 out_) {
bool valid;
(out_, valid) = readMemUnchecked(_memRoot, _addr, _proofOffset);
if (!valid) {
revert InvalidMemoryProof();
}
}

/// @notice Reads a 64-bit word from memory.
/// @param _memRoot The current memory root
/// @param _addr The address to read from.
/// @param _proofOffset The offset of the memory proof in calldata.
/// @return out_ The hashed MIPS state.
/// valid_ Whether the proof is valid.
function readMemUnchecked(
bytes32 _memRoot,
uint64 _addr,
uint256 _proofOffset
)
internal
pure
returns (uint64 out_, bool valid_)
{
unchecked {
validateMemoryProofAvailability(_proofOffset);
assembly {
// Validate the address alignment.
if and(_addr, EXT_MASK) {
// revert InvalidAddress();
let ptr := mload(0x40)
mstore(ptr, shl(224, 0xe6c4247b))
revert(ptr, 0x4)
}

// Load the leaf value.
let leaf := calldataload(_proofOffset)
_proofOffset := add(_proofOffset, 32)

// Convenience function to hash two nodes together in scratch space.
function hashPair(a, b) -> h {
mstore(0, a)
mstore(32, b)
h := keccak256(0, 64)
}

// Start with the leaf node.
// Work back up by combining with siblings, to reconstruct the root.
let path := shr(5, _addr)
let node := leaf
let end := sub(MEM_PROOF_LEAF_COUNT, 1)
for { let i := 0 } lt(i, end) { i := add(i, 1) } {
let sibling := calldataload(_proofOffset)
_proofOffset := add(_proofOffset, 32)
switch and(shr(i, path), 1)
case 0 { node := hashPair(node, sibling) }
case 1 { node := hashPair(sibling, node) }
}

// Verify the root matches.
valid_ := eq(node, _memRoot)
if valid_ {
// Bits to shift = (32 - 8 - (addr % 32)) * 8
let shamt := shl(3, sub(sub(32, 8), and(_addr, 31)))
out_ := and(shr(shamt, leaf), U64_MASK)
}
}
}
}

/// @notice Writes a 64-bit word to memory.
/// This function first overwrites the part of the leaf.
/// Then it recomputes the memory merkle root.
/// @param _addr The address to write to.
/// @param _proofOffset The offset of the memory proof in calldata.
/// @param _val The value to write.
/// @return newMemRoot_ The new memory root after modification
function writeMem(uint64 _addr, uint256 _proofOffset, uint64 _val) internal pure returns (bytes32 newMemRoot_) {
unchecked {
validateMemoryProofAvailability(_proofOffset);
assembly {
// Validate the address alignment.
if and(_addr, EXT_MASK) {
// revert InvalidAddress();
let ptr := mload(0x40)
mstore(ptr, shl(224, 0xe6c4247b))
revert(ptr, 0x4)
}

// Load the leaf value.
let leaf := calldataload(_proofOffset)
let shamt := shl(3, sub(sub(32, 8), and(_addr, 31)))

// Mask out 8 bytes, and OR in the value
leaf := or(and(leaf, not(shl(shamt, U64_MASK))), shl(shamt, _val))
_proofOffset := add(_proofOffset, 32)

// Convenience function to hash two nodes together in scratch space.
function hashPair(a, b) -> h {
mstore(0, a)
mstore(32, b)
h := keccak256(0, 64)
}

// Start with the leaf node.
// Work back up by combining with siblings, to reconstruct the root.
let path := shr(5, _addr)
let node := leaf
let end := sub(MEM_PROOF_LEAF_COUNT, 1)
for { let i := 0 } lt(i, end) { i := add(i, 1) } {
let sibling := calldataload(_proofOffset)
_proofOffset := add(_proofOffset, 32)
switch and(shr(i, path), 1)
case 0 { node := hashPair(node, sibling) }
case 1 { node := hashPair(sibling, node) }
}

newMemRoot_ := node
}
return newMemRoot_;
}
}

/// @notice Verifies a memory proof.
/// @param _memRoot The expected memory root
/// @param _addr The _addr proven.
/// @param _proofOffset The offset of the memory proof in calldata.
/// @return valid_ True iff it is a valid proof.
function isValidProof(bytes32 _memRoot, uint64 _addr, uint256 _proofOffset) internal pure returns (bool valid_) {
(, valid_) = readMemUnchecked(_memRoot, _addr, _proofOffset);
}

/// @notice Computes the offset of a memory proof in the calldata.
/// @param _proofDataOffset The offset of the set of all memory proof data within calldata (proof.offset)
/// Equal to the offset of the first memory proof (at _proofIndex 0).
/// @param _proofIndex The index of the proof in the calldata.
/// @return offset_ The offset of the memory proof at the given _proofIndex in the calldata.
function memoryProofOffset(uint256 _proofDataOffset, uint8 _proofIndex) internal pure returns (uint256 offset_) {
unchecked {
// A proof of 64-bit memory, with 32-byte leaf values, is (64-5)=59 bytes32 entries.
// And the leaf value itself needs to be encoded as well: (59 + 1) = 60 bytes32 entries.
offset_ = _proofDataOffset + (uint256(_proofIndex) * (MEM_PROOF_LEAF_COUNT * 32));
return offset_;
}
}

/// @notice Validates that enough calldata is available to hold a full memory proof at the given offset
/// @param _proofStartOffset The index of the first byte of the target memory proof in calldata
function validateMemoryProofAvailability(uint256 _proofStartOffset) internal pure {
unchecked {
uint256 s = 0;
assembly {
s := calldatasize()
}
// A memory proof consists of MEM_PROOF_LEAF_COUNT bytes32 values - verify we have enough calldata
require(
s >= (_proofStartOffset + MEM_PROOF_LEAF_COUNT * 32),
"MIPS64Memory: check that there is enough calldata"
);
}
}
}
Loading

0 comments on commit 2780ad1

Please sign in to comment.