Implement element-addressable memory #1598

plafer · 2024-12-10T21:04:04Z

Note that I changed the batch column to hold 4 * previous_defn_of_batch (now effectively the first address in the batch). This is to avoid a needless division per row in the processor.

This PR does not address the concern raised #1064 (comment); we should do that one in a subsequent PR, as it is a backend thing, and getting this PR out the door will allow miden-base and the compiler to start working fixing their code.

plafer · 2024-12-12T21:19:25Z

@bobbinth I am done implementing the processor part of the change, which is ready for review. All tests in the processor pass (except 2 which run the verifier, or verify the correctness of the bus).

Left to do after (high-level):

fix bus
update air constraints
update the book
a bit of cleanup (the TODO(plafer)'s)

bobbinth

Looks good! Thank you! I reviewed most of the non-test and non-MASM code - though, I only had a superficial look at the constraint evaluation code. Left some comments inline - mostly small/nits.

A couple of questions:

How did these changes impact performance?
Would the current design support reading multiple elements from the same word in the same cycle? (see here for context).

CHANGELOG.md

air/src/trace/mod.rs

docs/src/user_docs/stdlib/mem.md

stdlib/docs/mem.md

miden/src/repl/mod.rs

processor/src/chiplets/aux_trace/mod.rs

air/src/trace/chiplets/memory.rs

assembly/src/assembler/mod.rs

docs/src/user_docs/stdlib/collections.md

Al-Kindi-0 · 2025-01-06T10:49:39Z

air/src/constraints/chiplets/memory/mod.rs

+        let c_i = |f_i| {
+            frame.read_write_next()
+                + binary_not(frame.read_write_next())
+                    * binary_not(frame.element_or_word_next())
+                    * binary_not(f_i)
+        };
+
+        (c_i(f0), c_i(f1), c_i(f2), c_i(f3))


I would use the intermediate variable z_i and add the explanations in this comment with the modifications needed (e.g., use next variables in the definition and remove f_scb from the expression defining c_i.).
This will help in understanding the logic and catching soundness bugs in the future.

I added z_i, and a bunch of comments (including the docstring for the method). Let me know if anything important is still missing.

air/src/constraints/chiplets/memory/mod.rs

Al-Kindi-0 · 2025-01-06T10:55:59Z

air/src/constraints/chiplets/memory/mod.rs

+
+    #[inline(always)]
+    fn element_or_word(&self) -> E {
+        self.current()[MEMORY_ELEMENT_OR_WORD_COL_IDX]


nit: this might be a personal cognitive bias but I would've preferred IS_ELEMENT_OP or something similar as a name for the flag indicating whether the current op is element or word based.
Similarly for MEMORY_READ_WRITE_COL_IDX, taking reads as the default or base op, I would have called it instead IS_MEMORY_WRITE_COL_IDX and similarly for related methods and constants.

Agreed, fixed. I had started with similar names but reverted for some reason that I can't recall... Definitely more readable now.

air/src/constraints/chiplets/memory/tests.rs

Al-Kindi-0 · 2025-01-06T10:59:26Z

air/src/constraints/chiplets/memory/tests.rs

 /// the specified delta type, which determines the column over which the delta and delta inverse
 /// values of the trace would be calculated.
 ///
 /// - When the delta type is Context, the address and clock columns can be anything.
-/// - When the delta type is Address, the context must remain unchanged but the clock can change.
+/// - When the delta type is Batch, the context must remain unchanged but the clock can change.
 /// - When the delta type is Clock, both the context and address columns must remain unchanged.


should be context and batch.
Also is it Batch or batch?

Fixed.

Also is it Batch or batch?

I went with capitalized when designating a variant of MemoryTestDeltaType, and not capitalized otherwise.

Al-Kindi-0 · 2025-01-06T11:46:16Z

processor/src/chiplets/memory/mod.rs

 ///   clock cycles computed as described above.
+/// - `f_scb` is a flag indicating whether the context and the batch are the same as in the next


nit: " .. and the batch of the current row are the same as in the next one."

Al-Kindi-0 · 2025-01-06T12:11:19Z

stdlib/asm/crypto/dsa/rpo_falcon512.masm

        mem_loadw

-        # load pi_{i+512}
+        # load pi_{i+2048}


the index of the coefficient of the polynomial should stay the same

Al-Kindi-0 · 2025-01-06T12:11:30Z

stdlib/asm/crypto/dsa/rpo_falcon512.masm

        padw
        dup.12
        mem_loadw
-        #=> [PI, PI_{i+512}, C, pi_ptr, ...]
+        #=> [PI, PI_{i+2048}, C, pi_ptr, ...]


same comment here

Al-Kindi-0 · 2025-01-06T12:11:56Z

stdlib/asm/crypto/dsa/rpo_falcon512.masm

-#! The i-th coefficient s1_i of s1 is equal to c_i - (pi_i - pi_{512 + i}) which is equal to
-#! c_i  + pi_{512 + i} - pi_i. Now, we know that the size of the pi_i coefficients is bounded by
-#! J := 512 * q^2 and this means that J + pi_{512 + i} - pi_i does not Q-underflow and since
+#! The i-th coefficient s1_i of s1 is equal to c_i - (pi_i - pi_{2048 + i}) which is equal to


the index of the coefficient of the polynomial should stay the same

Right; reverted

Al-Kindi-0 · 2025-01-06T12:21:01Z

stdlib/asm/crypto/stark/random_coin.masm

We should probably add a disclaimer that most, if not all, of the procedures in this file assume that the input pointers are word-aligned.

Al-Kindi-0 · 2025-01-06T12:23:14Z

Looks great, thank you!
I did an initial round of reviews and left some comments inline. Went through all files in detail except for the constraints one as it seems to have some todos.

air/src/trace/mod.rs

core/src/debuginfo/source_file.rs

miden/src/helpers.rs

processor/src/chiplets/aux_trace/mod.rs

plafer · 2025-01-07T22:41:23Z

@bobbinth @Al-Kindi-0 ready for another look. I addressed all comments, and TODO(plafer). I will open an issue tomorrow for what's left after this PR (namely docs and implementing the additional required range-checks).

bobbinth · 2025-01-07T22:49:04Z

@bobbinth @Al-Kindi-0 ready for another look. I addressed all comments, and TODO(plafer). I will open an issue tomorrow for what's left after this PR (namely docs and implementing the additional required range-checks).

How does the performance look like in this branch vs. next?

assembly/src/assembler/instruction/mem_ops.rs

assembly/src/assembler/mod.rs

processor/src/errors.rs

plafer · 2025-01-08T14:29:14Z

How does the performance look like in this branch vs. next?

No change in the program_execution benchmarks

bobbinth

Looks good! Thank you! This is almost a full review (I have just a handful of files to go through).

assembly/src/assembler/procedure.rs

assembly/src/assembler/mod.rs

assembly/src/assembler/procedure.rs

assembly/src/errors.rs

processor/src/chiplets/aux_trace/mod.rs

stdlib/asm/crypto/dsa/rpo_falcon512.masm

bobbinth · 2025-01-09T09:57:17Z

btw, I think we should probably merge this into a new branch - e.g., something like element-mem. This way, we can start migrating miden-base to this branch but at the same time, would be able to make additional PRs against it.

Al-Kindi-0

Went through the constraints and all looks good except for a few questions and comments.

air/src/constraints/chiplets/memory/mod.rs

Al-Kindi-0 · 2025-01-09T12:48:30Z

air/src/constraints/chiplets/memory/mod.rs

+    result: &mut [E],
+    memory_flag_no_last_row: E,
+) -> usize {
+    result[0] = memory_flag_no_last_row


Is this consistent with the original definition $f_{scb} = [1 - (n_0 + (1-n_0) \cdot n_1)] \cdot f_{mem}'$ ? The expression is correct but what is current and what is next is a bit different.
If the code is correct then it would be nice to update the constraints appearing in the discussions.

Ah yes good point. In the discussions, given a frame, the result for "same context and word address" was stored in the current row, whereas in the implementation it is stored in the next row. I only did that since it was easier to implement given how Memory::fill_trace() is structured, but both are equivalent.

And after double-checking, this version is also correct given how memory_flag_not_last_row works (i.e. it is turned off when the next row of the frame lies outside the chiplet, so we never access the memory of the wrong chiplet).

If the code is correct then it would be nice to update the constraints appearing in the discussions.

This would be hard since it spans many posts, half of which are written by Bobbin. I will instead properly document the current constraints in the docs (#1616).

air/src/constraints/chiplets/memory/mod.rs

Al-Kindi-0 · 2025-01-09T12:59:11Z

air/src/constraints/chiplets/memory/mod.rs

+        let f3 = frame.idx1_next() * frame.idx0_next();
+
+        let c_i = |f_i| {
+            // z_i is set to 1 when `v'[i]` is not being accessed.


Should it be:
z_i is set to 1 when we are operating on elements but not the i-th element

but not the i-th element

It's not quite the i-th element that's not set to 1; doesn't that mean that all i are not set to 1?

I reworded to something that's hopefully better

It's not quite the i-th element that's not set to 1; doesn't that mean that all i are not set to 1?

Yeah it is the z_i we are talking about.
I still feel that the sentence doesn't capture the function of z_i but it should be easy to get it from the expression in the second line, hopefully.

I updated it to be your suggestion z_i is set to 1 when we are operating on elements but not the i-th element

air/src/constraints/chiplets/memory/mod.rs

bobbinth

Looks good! Thank you! I didn't review the constraints in too much detail, but will do this when reviewing the docs PR.

No additional comments from this review, but there are a couple of comments remain from the previous review (re handling padding for locals and updating cycles counts so that at least what we have there is not wrong).

Al-Kindi-0 · 2025-01-10T09:53:35Z

All looks good to me now, thanks again!

plafer force-pushed the plafer-1064-element-addressable-mem branch 2 times, most recently from 6eadbd9 to 74efdb5 Compare December 12, 2024 21:17

plafer requested a review from bobbinth December 12, 2024 21:17

plafer force-pushed the plafer-1064-element-addressable-mem branch 3 times, most recently from 83c63ef to ec1094f Compare December 18, 2024 22:05

plafer added 6 commits December 19, 2024 06:28

feat: update memory chiplet to be element-addressable

aacb9d4

feat(air): fix air constraints for new memory chiplet

3de8441

feat(bus): fix bus for element-addressable memory

fdda2f8

fix: fix stdlib after element-addressable memory

bd6e746

changelog

06750d4

more test fixes

f07da49

plafer force-pushed the plafer-1064-element-addressable-mem branch from 31c3e2a to f07da49 Compare December 19, 2024 20:53

plafer added 2 commits December 21, 2024 11:08

fix: recursive verifier

51f11c3

fix sha256

6f3c11b

plafer marked this pull request as ready for review December 21, 2024 18:40

bobbinth reviewed Jan 6, 2025

View reviewed changes

bobbinth requested review from Al-Kindi-0 and paracetamolo January 6, 2025 09:20

Al-Kindi-0 reviewed Jan 6, 2025

View reviewed changes

plafer added 2 commits January 6, 2025 14:43

PR fixes

eb33e0f

nomenclature: change batch -> word

06782a6

plafer mentioned this pull request Jan 6, 2025

VmState memory address: use u32 instead of u64 #1612

Open

plafer added 2 commits January 6, 2025 15:32

more PR fixes

19c3a9c

clippy

d9581d5

bobbinth reviewed Jan 7, 2025

View reviewed changes

air/src/trace/mod.rs Outdated Show resolved Hide resolved

core/src/debuginfo/source_file.rs Show resolved Hide resolved

miden/src/helpers.rs Outdated Show resolved Hide resolved

processor/src/chiplets/aux_trace/mod.rs Outdated Show resolved Hide resolved

cleanup

9a81fe7

plafer mentioned this pull request Jan 7, 2025

Make all fields of Chiplets public #1613

Open

plafer added 2 commits January 7, 2025 15:49

feat: make the number of locals element-addressable

6e4fd25

fix: fix stdlib after locals change

a21e20f

plafer requested review from Al-Kindi-0 and bobbinth January 7, 2025 22:40

bobbinth reviewed Jan 8, 2025

View reviewed changes

assembly/src/assembler/instruction/mem_ops.rs Show resolved Hide resolved

assembly/src/assembler/mod.rs Outdated Show resolved Hide resolved

processor/src/errors.rs Outdated Show resolved Hide resolved

more PR fixes

07aab25

plafer requested a review from bobbinth January 8, 2025 15:01

plafer mentioned this pull request Jan 8, 2025

Element-addressable memory follow-up #1614

Open

3 tasks

bobbinth reviewed Jan 9, 2025

View reviewed changes

Al-Kindi-0 reviewed Jan 9, 2025

View reviewed changes

more PR fixes

9883cb0

plafer changed the base branch from next to element-addressable-memory January 9, 2025 20:48

plafer requested review from Al-Kindi-0 and bobbinth January 9, 2025 20:50

bobbinth approved these changes Jan 10, 2025

View reviewed changes

plafer added 2 commits January 10, 2025 11:13

fix rounding up of locals

868bf1e

PR fixes

90a979e

plafer merged commit 0e7c1d6 into element-addressable-memory Jan 10, 2025
9 checks passed

plafer deleted the plafer-1064-element-addressable-mem branch January 10, 2025 16:56

bobbinth mentioned this pull request Jan 10, 2025

Migrate to element-addressable memory 0xPolygonMiden/miden-base#1059

Open

greenhat mentioned this pull request Jan 15, 2025

Migrate to element-addressable memory VM 0xPolygonMiden/compiler#374

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement element-addressable memory #1598

Implement element-addressable memory #1598

plafer commented Dec 10, 2024 •

edited

Loading

plafer commented Dec 12, 2024 •

edited

Loading

bobbinth left a comment

Al-Kindi-0 Jan 6, 2025

plafer Jan 6, 2025

Al-Kindi-0 Jan 6, 2025

plafer Jan 6, 2025

Al-Kindi-0 Jan 6, 2025

plafer Jan 6, 2025

Al-Kindi-0 Jan 6, 2025

plafer Jan 6, 2025

Al-Kindi-0 Jan 6, 2025

plafer Jan 6, 2025

Al-Kindi-0 Jan 6, 2025

plafer Jan 6, 2025

Al-Kindi-0 Jan 6, 2025

plafer Jan 6, 2025

Al-Kindi-0 Jan 6, 2025

plafer Jan 6, 2025

Al-Kindi-0 commented Jan 6, 2025

plafer commented Jan 7, 2025

bobbinth commented Jan 7, 2025

plafer commented Jan 8, 2025

bobbinth left a comment

bobbinth commented Jan 9, 2025

Al-Kindi-0 left a comment

Al-Kindi-0 Jan 9, 2025

plafer Jan 9, 2025

Al-Kindi-0 Jan 9, 2025

plafer Jan 9, 2025

Al-Kindi-0 Jan 10, 2025

plafer Jan 10, 2025

bobbinth left a comment •

edited

Loading

Al-Kindi-0 commented Jan 10, 2025

		/// clock cycles computed as described above.
		/// - `f_scb` is a flag indicating whether the context and the batch are the same as in the next

Implement element-addressable memory #1598

Implement element-addressable memory #1598

Conversation

plafer commented Dec 10, 2024 • edited Loading

plafer commented Dec 12, 2024 • edited Loading

bobbinth left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Al-Kindi-0 commented Jan 6, 2025

plafer commented Jan 7, 2025

bobbinth commented Jan 7, 2025

plafer commented Jan 8, 2025

bobbinth left a comment

Choose a reason for hiding this comment

bobbinth commented Jan 9, 2025

Al-Kindi-0 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bobbinth left a comment • edited Loading

Choose a reason for hiding this comment

Al-Kindi-0 commented Jan 10, 2025

plafer commented Dec 10, 2024 •

edited

Loading

plafer commented Dec 12, 2024 •

edited

Loading

bobbinth left a comment •

edited

Loading