Remove ROM from platform #773
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Previously we had machinery that makes sure that executable code and data memory do not overlap. But in a Harvard Archicture where code and data live in different address spaces anyway, that is not necessary. (Our VM implements a Harvard Architecture. Our circuits have always implemented that archicture, and the emulator has recently followed suit.) Note how this PR does not remove any checks or constraints from the circuits. Ie a sufficiently motivated and independent minded prover could have always done what this PR makes easier.
matthiasgoergens
requested review from
lispc,
hero78119,
kunxian-xia and
naure
|
Converted to draft because of some issues around JAL and JALR and wrap around. |
matthiasgoergens
removed request for
kunxian-xia,
lispc,
hero78119 and
naure
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
(Extracted from the work on the Rust standard library support for guests.)
Previously we had machinery that makes sure that executable code and data memory do not overlap. But in a Harvard Archicture where code and data live in different address spaces anyway, that is not necessary.
(Our VM implements a Harvard Architecture. Our circuits have always implemented that archicture, and the emulator has recently followed suit.)
Note how this PR does not remove any checks or constraints from the circuits. Ie a sufficiently motivated and independent minded prover could have always done what this PR makes easier.
Btw, as far as I can tell, we do not currently check in the circuits whether the execution actually starts with the entry point. Neither the entry point of the ELF nor the entry point of the Platform. (And that's true before and after this PR.)