docs(memory): fix delta encoding comments in memory trace#2910
docs(memory): fix delta encoding comments in memory trace#2910alimmaster wants to merge 7 commits into0xMiden:nextfrom
Conversation
Fixes misleading memory trace documentation in `processor/src/trace/chiplets/memory/mod.rs`. Changes: - corrected the same-word delta description from `new_clk - old_clk - 1` to `new_clk - old_clk` - updated the first-row trace description to match the current `prev_clk` initialization - aligned the nearby inline comments in `append_range_checks()` and `fill_trace()` with the actual implementation This is a documentation-only change and does not affect runtime behavior.
|
Closes #2815 |
|
@alimmaster please add a Changelog line, you can take #2925 as an example |
Added the changelog entry. |
adr1anh
left a comment
adr1anh
left a comment
There was a problem hiding this comment.
It took me a while to make sense of the comments, even before the change. I’m mostly familiar with the constraints but it's been a while since I checked the trace generation.
I left some comments with my understanding which I'm not completely sure of. It'd be great if you could actually explain how this works, and propose something clearer overall.
While the changes might be slightly more correct, I don't think they actually help understand what's going on.
| @@ -82,13 +82,14 @@ const INIT_MEM_VALUE: Word = EMPTY_WORD; | |||
| /// - When the context remains the same but the word changes, these columns contain (`new_word` | |||
| /// - `old_word`). | |||
| /// - When both the context and the word remain the same, these columns contain (`new_clk` - | |||
| /// `old_clk` - 1). | |||
| /// `old_clk`). | |||
| /// - `d_inv` contains the inverse of the delta between two consecutive context IDs, words, or clock | |||
| /// cycles computed as described above. It is the field inverse of `(d_1 * 2^16) + d_0` | |||
| /// - `f_scw` is a flag indicating whether the context and the word of the current row are the same | |||
| /// as in the next row. | |||
| /// as in the previous row. | |||
| /// | |||
| /// For the first row of the trace, values in `d0`, `d1`, and `d_inv` are set to zeros. | |||
| /// For the first row of the trace, `prev_clk` is initialized to `first_clk - 1`, so `d0`, | |||
| /// `d1`, and `d_inv` reflect the delta against that value rather than being forced to zero. | |||
There was a problem hiding this comment.
I find the old/new a bit confusing when it comes to the constraints, since we often use local/current and next for the two consecutive rows.
I get the this trace is a bit special because we're treating the current row as the previous state and the next one as the current one, but maybe a better naming would be prev/curr to be a bit more consistent?
Cc @Al-Kindi-0, @plafer
| @@ -248,8 +249,9 @@ impl Memory { | |||
| /// [RangeChecker] chiplet instance, along with their row in the finalized execution trace. | |||
| pub fn append_range_checks(&self, memory_start_row: RowIndex, range: &mut RangeChecker) { | |||
| // set the previous address and clock cycle to the first address and clock cycle of the | |||
There was a problem hiding this comment.
Nit: should this be "initialize the previous..."
| // trace; we also adjust the clock cycle so that delta value for the first row would end | ||
| // up being ZERO. if the trace is empty, return without any further processing. | ||
| // trace; we also adjust the clock cycle to be one less than the first row's clock so the | ||
| // first-row delta is computed against the immediately preceding clock. if the trace is |
There was a problem hiding this comment.
This means the delta is one right? Isn't that clearer?
| // set the previous address and clock cycle to the first address and clock cycle of the | ||
| // trace; we also adjust the clock cycle to be one less than the first row's clock so the | ||
| // first-row delta is computed against the immediately preceding clock. if the trace is | ||
| // empty, return without any further processing. |
…the first-row delta is 1, and updated the inline comments in both trace-generation paths to describe the initialization more directly.
3 participants
Current behavior
The memory trace documentation in
processor/src/trace/chiplets/memory/mod.rsstates that repeated accesses to the same word/context use a delta ofnew_clk - old_clk - 1.However, both
append_range_checks()andfill_trace()compute the same-word delta asnew_clk - old_clk.The file also says that the first row has
d0,d1, andd_invset to zero, while the implementation initializesprev_clkto one less than the first row clock and computes the first-row delta from that value.New behavior
The documentation now matches the implementation:
new_clk - old_clkprev_clkinitializationBreaking changes
None.
Other info
Documentation-only update.
No code behavior was changed.
Fixes #2815