Reward Size in USD

10 USD

Feature Proposal

demo proposal

Acceptance Criteria

Go to Mintycode to approve the Feature Proposal.

At the moment, the TLB is implemented as an off-chain optimization to machine-emulator, but not on-chain in machine-solidity-step. This works for conforming software that executes a fence.vma instruction whenever the virtual memory map is changed. This is the way to ensure deterministic behavior according to the RISC-V specification. However, an ill-formed or malicious program can mess with the virtual memory map and then fail to execute fence.vma, either by accident or on purpose. This would cause the TLB to be outdated relative to the virtual memory map, and thus lead to mismatching behavior on- and off-chain.

To be on the safe side and prevent this potential source of non-determinism, we have decided to have matching TLB implementations on- and off-chain. This will require changes to the machine-emulator implementation, so it becomes possible to efficiently implement the TLB on-chain. Then, the state accesses related to the TLB will have to be logged. Once these changes have been made, a matching TLB implementation will be added to the on-chain code in machine-solidity-step.

This issue will track the progress of these changes.

See cartesi/machine-emulator#21.

Context

CI is taking too long to finish. The bottleneck is the log tests, which can take up to 2 hours in the current version.

Possible solutions

Configure the log tests only being executed during official releases, so small PRs can be much faster and efficient. One can always run the tests in his local environment for his concern.

The goal of this issue is to:

• implement a new entrypoint contract and function MetaStep
• the MetaStep introduces a concept of meta-machine, which hides the details of implementation difference of big-machine and micro-machine away from the user
• implement a library and function UArchReset, which resets the micro-machine back to its pristine state
• the MetaStep will either call UArchStep or UAarchStep + UArchReset based on the MetaCounter value
• a big-machine step is equivilent to MetaCounter increasing 2^a, and equivilent to executing UArchStep (2^a) - 1 times and UArchStep + UArchReset once, e.g., ask the meta-machine to give the state at MetaCounter 90 + (1 << a)*27, meta-machine will call big-machine step 27 times, and then UArchStep 90 times; meta-machine could instead call (UArchStep 2^a times and one UArchReset) 27 times, and then UArchStep 90 times and it would give the same value.
• UArchReset will receive a machine hash, a memory region hash and its corresponding proofs as validation. And it will reconstruct the machine hash by replacing the memory region hash with a pre-calculated pristine hash

cc: @mpernambuco @GCdePaula

Original post here: https://discordapp.com/channels/600597137524391947/1113159025920593930/1113160593193574451

Second alternative: since we don't need incremental stuff, let's simplify things and make the interface more generic. The idea is to verify proofs as accesses are requested by step. This way we don't need to know the type of the access beforehand.

Imagine that we receive something like a buffer called proofs, which have all the necessary data for all accesses. We create an abstraction called MemoryAccess around that buffer which holds both the last read position in that buffer and the state hash of the machine, and offers the methods:

writeRegion(&ctx, offset, log2size, merkleHash)
readRegion(&ctx, offset, log2size) returns (bytes32)
writeWordHash(&ctx, address, wordHash)
readWordHash(&ctx, address) returns (bytes32)
readWord(&ctx, address) returns (u64)

When step calls readWord, it will "eat up" from the buffer a word, sixty-one siblings, and verify whether that word really is on that position in the machine state. If so, it will return the word. When step calls writeWord, it will eat up from the buffer a hash, sixty-one siblings, verify whether that's a match, and then update the machine state. Likewise for the other methods. If a proof is incorrect, we revert. It should be exactly the same amount of code we have now, but done during step instead of on a loop before step.

We could split this buffer into two, one holding hashes and another holding words, possibly would be cleaner.

When step finishes, we read the final state stored in MemoryAccess and check whether that's the claimed final hash. If so, all's good, otherwise revert. 

cc: @GCdePaula

Context

Make the MemoryAccessLog more generic so the accesses are not limited to word size but any valid aligned memory region that's larger than a word. This can be helpful for the UArchReset feature, and also let the rollups insert input drives easily.

Possible solutions

A possible solution can be found on a thread on Discord that's proposed by @GCdePaula.
https://discord.com/channels/600597137524391947/1113159025920593930/1113160593193574451

In summary, the new library would implement below functions:

writeRegion(ctx, region, newHash)
readRegion(ctx, region) returns (bytes32)
writeWordHash(ctx, addr, newHash)
readWordHash(ctx, addr) returns (bytes32)
readWord(ctx, addr) returns (u64)
writeWord(ctx, addr, newValue) returns (uint64)

The ctx is a memory struct argument that keeps track of the current machine root hash and all related proofs and hashes.
The region is a new structure that should present an aligned memory region, replacing the old (position, log2Size) tuple.

It would be so cool to have a ZKP about a Linux machine. Which basically just means deploying this contract to the zkSync2.0 testnet. How long would it take to generate a proof for the execution of a simple python script?

Context

CSRs addresses (such as UCYCLE, UHALT, UPC, UX0) are currently hard coded in the contract, ideally it's values should be automatically generated from the C++ implementation, therefore in case they change, the changes would be automatically be reflected in the contract by simply regenerating it.

Solution

We should first expose them in the emulator sources, then we can improve the generator script.

so there's only one 'machine' to deal with, not machine+helper

see https://discord.com/channels/600597137524391947/1104008133250138222/1113872750881275944 for context