Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
N
nebula
Project
Project
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
exchain
nebula
Commits
eee8369b
Commit
eee8369b
authored
Sep 25, 2021
by
George Hotz
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
cartesi too complex, think we can do sub 200 lines for the mips machine
parent
c2f67a9c
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
134 additions
and
11 deletions
+134
-11
CHALLENGE
CHALLENGE
+28
-11
MIPS.sol
contracts/MIPS.sol
+106
-0
No files found.
CHALLENGE
View file @
eee8369b
...
...
@@ -24,31 +24,37 @@ PreimageOracle -- key value store
returns
$v0 = preimage[$t7...$t0] >> ($a0 * 32)
Program returns a hash in [$t7...$t0] and exits(
special instruction
) with the hash in the state
Program returns a hash in [$t7...$t0] and exits(
jump to 0xDEADDEAD
) with the hash in the state
Challenge Flow:
C is challenger, D is defender
Super nice, the defender barely needs to spend gas!
C: InitiateChallenge(bytes blockHeaderN, bytes blockHeaderNp1,
C: InitiateChallenge(
uint blockNumberN,
bytes blockHeaderN, bytes blockHeaderNp1,
bytes32 assertionHash, bytes32 finalSystemHash, string[] assertionProof, uint256 stepCount)
* checks hashes of the block headers
* saves inputs for input oracle
* confirms assertionHash != blockHeaderNp1.Hash
* expectCorrect = (assertionHash == blockHeaderNp1.Hash)
* confirm assertionProof proves the final state of [$t7...$t0] in finalSystemHash is assertionHash
* confirm assertionProof
proves the final state of *$pc in finalSystemHash is special exit instruction
* L = 0, R = stepCount
-1
# we agree at L=0, we disagree at R=stepCount
* confirm assertionProof
[0..7]
proves the final state of [$t7...$t0] in finalSystemHash is assertionHash
* confirm assertionProof
[8] proves the final state of $pc in finalSystemHash is 0xDEADDEAD
* L = 0, R = stepCount # we agree at L=0, we disagree at R=stepCount
* return new challengeId
* assertedRiscState[0] = GlobalStartSystemHash
* assertedRiscState[stepCount-1] = finalSystemHash
* defendedRiscState[0] = GlobalStartSystemHash
* assertedRiscState[stepCount] = finalSystemHash
........
if it's one step, we are done. considering it's not, we binary search
........
C: ProposeRiscState(uint256 challengeId, uint256 riscState)
* stepNumber = GetStepNumber(uint256 challengeId) returns floor((L + R) / 2)
* assert assertedRiscState[stepNumber] == 0
* assertedRiscState[stepNumber] = riscState
D: RespondRiscState(uint256 challengeId,
bool yes
) onlyOwner
D: RespondRiscState(uint256 challengeId,
uint256 riscState
) onlyOwner
* off-chain: run to step = stepNumber, get state hash, check if it matches
* if yes:
* stepNumber = GetStepNumber(uint256 challengeId) returns floor((L + R) / 2)
* defendedRiscState[stepNumber] = riscState
* if assertedRiscState[stepNumber] == defendedRiscState[stepNumber]:
L = stepNumber # we agree at stepNumber
else:
R = stepNumber # we disagree at stepNumber
...
...
@@ -59,13 +65,24 @@ the issue is with the L->R transition
aka assertedRiscState[L] -> assertedRiscState[R]
........
# call this at any time (global), adds them to a preimage lookup for PreimageOracle
# put these on the MIPS contract
C: ProposePreimage(bytes anything)
* preimageLookup[keccak256(anything)] = anything
C: ConfirmStateTransition(uint256 challengeId, ustrings proofs)
C: AddMerkleState(uint256 stateHash, uint32 addr, uint32 value, string proof)
* validate proof in assertedRiscState[stepNumber]
* riscMemory[stepNumber][address] = value
* Final
C: ConfirmStateTransition(uint256 challengeId)
* assert L+1 == R
* validate all proofs in assertedRiscState[L]
* do the state transition
* if any needed pieces of start state are missing, challenge fails (it can try again)
* if any needed pieces of start state are missing
in riscMemory
, challenge fails (it can try again)
* reconstruct the riscState after transition -> newRiscState
* assert assertedRiscState[R] == newRiscState
* pay out bounty
# optional claim for the defender
# prove the defendedRiscState[L] -> defendedRiscState[R]
# NOTE, if it's the last step, defendedRiscState[R] might not exist.
TODO: ensure the state merklization is canonical. if it doesn't match perfectly you can lose
\ No newline at end of file
contracts/MIPS.sol
0 → 100644
View file @
eee8369b
pragma solidity ^0.8.0;
// https://inst.eecs.berkeley.edu/~cs61c/resources/MIPS_Green_Sheet.pdf
// https://uweb.engr.arizona.edu/~ece369/Resources/spim/MIPSReference.pdf
contract MIPS {
// This state is global
mapping(bytes32 => mapping (uint32 => uint64)) public state;
mapping(bytes32 => bytes) public preimage;
function AddPreimage(bytes calldata anything) public {
preimage[keccak256((anything))] = anything;
}
function AddMerkleState(bytes32 stateHash, uint32 addr, uint32 value, string calldata proof) public {
// TODO: check proof
state[stateHash][addr] = (1 << 32) | value;
}
uint32 constant REG_OFFSET = 0xc0000000;
uint32 constant REG_PC = REG_OFFSET + 21*4;
function getState(bytes32 stateHash, uint32 addr) public view returns (uint32) {
if (addr == REG_OFFSET) {
// zero register is always 0
return 0;
}
assert(addr & 3 == 0); // aligned access only
uint64 ret = state[stateHash][addr];
assert((ret >> 32) == 1); // was set
return uint32(ret);
}
// compute the next state
// will revert if any input state is missing
function Step(bytes32 stateHash) public view returns (uint64[] memory) {
// instruction fetch
uint32 pc = getState(stateHash, REG_PC);
uint32 insn = getState(stateHash, pc);
uint32 opcode = insn >> 26; // 6-bits
// decode
// register fetch
uint32 rs;
uint32 rt;
if (opcode != 2 && opcode != 3) { // j and jal have no register fetch
// R-type or I-type (stores rt)
rs = getState(stateHash, REG_OFFSET + ((insn >> 19) & 0x7C));
if (opcode == 0) {
// R-type (stores rd)
rt = getState(stateHash, REG_OFFSET + ((insn >> 14) & 0x7C));
}
}
// memory fetch (all I-type)
// we do the load for stores also
uint32 mem;
if (opcode >= 0x20) {
// M[R[rs]+SignExtImm]
uint32 SignExtImm = insn&0xFFFF | (insn&0x8000 != 0 ? 0xFFFF0000 : 0);
mem = getState(stateHash, (rs + SignExtImm) & 0xFFFFFFFC);
}
// execute
execute(insn, rs, rt, mem);
// write back
}
function execute(uint32 insn, uint32 rs, uint32 rt, uint32 mem) public pure returns (uint32) {
uint32 opcode = insn >> 26; // 6-bits
uint32 func = insn & 0x3f; // 6-bits
// TODO: deref the immed into a register
if (opcode == 0) {
uint32 shamt = (insn >> 6) & 0x1f;
// R-type (ArithLog)
if (func == 0x20 || func == 0x21) { return rs+rt; // add or addu
} else if (func == 0x24) { return rs&rt; // and
} else if (func == 0x27) { return ~(rs|rt); // nor
} else if (func == 0x25) { return (rs|rt); // or
} else if (func == 0x22 || func == 0x23) {
return rs-rt; // sub or subu
} else if (func == 0x2a) {
return int32(rs)<int32(rt) ? 1 : 0; // slt
} else if (func == 0x26) {
return rs<rt ? 1 : 0; // sltu
// Shift and ShiftV
} else if (func == 0x00) { return rt << shamt; // sll
} else if (func == 0x04) { return rt << rs; // sllv
} else if (func == 0x03) { return rt >> shamt; // sra
} else if (func == 0x07) { return rt >> rs; // srav
} else if (func == 0x02) { return rt >> shamt; // srl
} else if (func == 0x06) { return rt >> rs; // srlv
}
} else if (func == 0x20) { return mem; // lb
} else if (func == 0x24) { return mem; // lbu
} else if (func == 0x21) { return mem; // lh
} else if (func == 0x25) { return mem; // lhu
} else if (func == 0x23) { return mem; // lw
} else if (func&0x3c == 0x28) { return rt; // sb, sh, sw
}
}
}
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment