feat: caller lookups for read-write memory accesses (3/3) - #2081
Open
OlivierBBB wants to merge 11 commits into
Open
feat: caller lookups for read-write memory accesses (3/3)#2081OlivierBBB wants to merge 11 commits into
OlivierBBB wants to merge 11 commits into
Conversation
Every read-write memory access now emits a lookup tying it to a row of that memory's table, through the same per-site machinery as calls and access-once memories: the source tuple carries the accessor's address, data and threaded timestamp registers (gated by the shared line/path selector), and maps onto the table's ADDRESS, VALUE_WRITTEN and TIMESTAMP_WRITTEN columns. A read's data registers are its outputs — the value read back — which the table exposes in VALUE_WRITTEN too, since a read row writes back what it found. The access's read/write kind is pinned by the target-side filter rather than a tuple element (MIR lookup tuples carry register accesses only): the table gains two fully-determined selector columns, EXEC_WRITE = EXEC * IS_WRITE and EXEC_READ (via EXEC_WRITE + EXEC_READ == EXEC), filled by the observer; a write site's lookup targets the table filtered by EXEC_WRITE, a read site's by EXEC_READ. With this, the guest-facing columns of every access row are pinned by the caller and the row-local constraints hold end-to-end; the remaining gap — that VALUE_READ genuinely returns the last value written to the address — is the offline memory-checking bus (#2068). Part 3 of 3 of the RAM timestamps feature (#1807). Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>
Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>
…erge Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>
Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>
Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>
Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>
Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>
Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>
Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>
Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>
This file contains hidden or 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
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.
Part 3 of 3 of the RAM timestamps feature (#1807), stacked on #2080 (which stacks on #2079); the diff shown here is only this PR's changes.
What it does
Every read-write memory access now emits a lookup tying it to a row of that memory's table, through the same per-site machinery as calls and access-once memories: the source tuple carries the accessor's address, data and threaded timestamp registers — gated by the shared line/path selector — and maps onto the table's
ADDRESS,VALUE_WRITTENandTIMESTAMP_WRITTENcolumns. Multiple accesses on one row each get their own lookup. A read's data registers are its outputs (the value read back), which the table exposes inVALUE_WRITTENtoo, since a read row writes back what it found (VALUE_READ == VALUE_WRITTEN).The access's read/write kind is pinned by the target-side filter rather than a tuple element (MIR lookup tuples carry register accesses only): the table gains two fully-determined selector columns,
EXEC_WRITE = EXEC · IS_WRITEandEXEC_READ(viaEXEC_WRITE + EXEC_READ == EXEC), filled by the observer. A write site's lookup targets the table filtered byEXEC_WRITE, a read site's byEXEC_READ.With this, the guest-facing columns of every access row are pinned by the caller, and the row-local constraints hold end-to-end. The remaining gap — that
VALUE_READgenuinely returns the last value written to the address — is the offline memory-checking bus, tracked in #2068 together with the finalization rows.Testing
The
ram_01..10fixtures and the RAM-heavy benches (blake / sort / keccakf / poseidon) now run with the complete chain live — threading → table → lookups — across the fullTest_ZkcUnit|Test_ZkcMixed|Test_ZkcInvalidand bench suites; lint clean.🤖 Generated with Claude Code