Permutation instructions/links #1126

pacheco · 2024-03-05T19:58:08Z

Allow asm machines to be linked by permutation arguments.
The syntax is the same as for lookups, but uses a ~ (tilde) instead of =.

This PR is written in a way that there's no change to existing asm/pil code and tests, and so witgen support can be implemented separately

ast/src/object/mod.rs

parser/src/powdr.lalrpop

georgwiese · 2024-03-06T09:43:31Z

I tried implementing memory with it: #1129

One issue that I think should be fixed in this PR is that it seems like the selectors can't actually be used. I expect this to be a common pattern:

let is_mem_op = array::sum(selectors);

This currently gives me symbol not found in '::std::memory': 'selectors' even though the selectors do appear in the correct namespace in the final pil. So I guess they are added too late for the check to pass.

chriseth · 2024-03-07T07:54:52Z

I tried implementing memory with it: #1129

One issue that I think should be fixed in this PR is that it seems like the selectors can't actually be used. I expect this to be a common pattern:
let is_mem_op = array::sum(selectors);
This currently gives me symbol not found in '::std::memory': 'selectors' even though the selectors do appear in the correct namespace in the final pil. So I guess they are added too late for the check to pass.

I think they are missing from Machine::local_names()

ast/src/parsed/asm.rs

georgwiese

Hmm, I think the approach of completely hiding the selectors from the user introduces some issues:

I re-based my memory PR onto this branch and now I have this issue. Basically, I need access to the used flag in the constraints.
As mentioned in the comment below, I think the current way to keep selectors constant in the block fails if the latch is in the first row.

I'm not sure what the best abstraction is. My original proposal (just adding the selectors, maybe bit-constrain them, but no other magic) wouldn't have these issues and instead require the user to figure this out for their machine. I wonder if at this point that is the better approach until we know the patterns and figured out an abstraction that is flexible enough to cover all use-cases...

georgwiese · 2024-03-13T09:05:43Z

pipeline/tests/asm.rs

+#[should_panic = "Witness generation failed"]
+fn permutations_to_block_to_block() {
+    // TODO: witgen issue
+    let f = "asm/permutations_block_to_block.asm";


If I understand this right, the issue here is not the block-to-block think (which would be good to test!) But that a machine of block size 1 does not get recognized as a block machine. If the first machine had a block size > 1 it should work! I think it would be good testing this, because it makes sure that the calls to the second machine are masked out in the dummy blocks of the first!

georgwiese · 2024-03-13T09:13:57Z

test_data/asm/permutations_block_to_block.asm

+    link 1 ~> bin.or A, B -> X;
+    link 1 ~> bin.or C, D -> Y;
+    link 1 ~> bin.or X, Y -> E;
+
+    col fixed operation_id = [0]*;
+    col fixed latch = [1]*;


Suggested change

link 1 ~> bin.or A, B -> X;

link 1 ~> bin.or C, D -> Y;

link 1 ~> bin.or X, Y -> E;

col fixed operation_id = [0]*;

col fixed latch = [1]*;

link latch ~> bin.or A, B -> X;

link latch ~> bin.or C, D -> Y;

link latch ~> bin.or X, Y -> E;

col fixed operation_id = [0]*;

// TODO: Currently, witgen fails if we set the latch to [1]*, because then the machine

// does not get detected as a block machine and connecting VMs via permutations is not supported

// yet. By setting the latch to [0, 1]*, the first row of every block is completely unconstrained.

col fixed latch = [0, 1]*;

This seems to work!

The problem with the original example is not the block-to-block construction but that this machine does not have a latch (it gets optimized away). Feel free to keep the original file as a failing test, but I think it would be good to test the block-to-block case, because it tests that calls to Binary get masked out in the dummy blocks of Binary4!

Alright then we're hitting other bugs ^^

It works though if we have a strict 1-to-1 mappings (Main has 1 link to Binary4, which has 1 link to Binary). LMK if I should give it a shot to come up with a simple-enough-but not dumb example!

georgwiese · 2024-03-13T10:34:30Z

airgen/src/lib.rs

+            ]);
+            if let Some(latch) = &obj.latch {
+                obj.pil.push(parse_pil_statement(&format!(
+                    "std::array::map({LINK_SELECTOR_NAME}, |s| std::utils::unchanged_until(s, {latch}));"


Ah, I think this would be a problem if the latch is in the first row instead of the last :/

I think in that case it should be:
std::utils::unchanged_until(s, {latch}')); (note the '!)

Can we detect this? I guess not easily because we haven't evaluated the fixed columns yet?

I think Poseidon is a good test case for this. We could eventually change mos of our tests to use permutations instead of lookups.

I tried implementing this suggestion and testing with the Poseidon machine. I ran into more witgen issues which are fixed here: #1157

I think we can't, were still producing pil at this point

georgwiese · 2024-03-13T10:41:01Z

airgen/src/lib.rs

+    for (location, count) in incoming_permutations {
+        let obj = objects.get_mut(&location).unwrap();
+        if count > 0 {
+            // TODO: only block machines actually need a used flag to


Is this true? What if a VM calls another machine via a permutation?

The used flag is only used to filter out dummy blocks in the caller, and those (AFAIU) are not an issue in VMs, no?
But in any case, we don't know that here, so we add used anyways.

Ah, right, true!

pacheco · 2024-03-13T22:18:33Z

For the issue of accessing the selectors, is accessing the used flag directly (i.e., sum of selectors) instead of the selector array enough?
We could do one of the following:

a) try a builtin for that
b) allow machines to have an optional declaration (selector foo;?), which would be the name for the used flag in place of the default "hidden" name, and thus would be referenceable by machine code.

What do you think? I kinda like the second option

georgwiese · 2024-03-13T23:11:13Z

For the issue of accessing the selectors, is accessing the used flag directly (i.e., sum of selectors) instead of the selector array enough?

Not to fix the unchanged_until thing in Poseidon, as discussed above, right? But that would be fixed by giving the user access to the raw selectors and making the user responsible for keeping them constant if needed.

georgwiese

I just tested this by rebasing my memory PR (#1129) onto it and also trying to change the Poseidon machine so that it can be used via a lookup and permutation (by adding the call_selectors statement).

I ran into witgen issues with the selector[0] (reserved for lookups):

If I have the call_selectors statement, lookups compile to a selector of LATCH * selectors[0], in which case witgen doesn't detect the machine during witgen.
If the machine is connected only via permutation, we have an extra column selectors[0] which is never used. This also breaks machine detection for the memory machine.

Both of these could be fixed in witgen, but I'm not sure if there is need for this extra selector. It is not needed for the lookup argument, and just to pass a bit that is guaranteed to be 1 for any "real" call, we could also add an argument to the operation, as discussed in the chat.

georgwiese · 2024-03-18T09:54:33Z

pipeline/tests/asm.rs

+#[test]
+#[should_panic = "has outgoing permutations but doesn't declare call_selectors"]
+fn permutation_outgoing_needs_selector() {
+    // TODO: witgen issue


Suggested change

// TODO: witgen issue

georgwiese · 2024-03-18T09:54:40Z

pipeline/tests/asm.rs

+#[test]
+#[should_panic = "has incoming permutations but doesn't declare call_selectors"]
+fn permutation_incoming_needs_selector() {
+    // TODO: witgen issue


Suggested change

// TODO: witgen issue

georgwiese · 2024-03-18T09:56:13Z

test_data/asm/permutations/block_to_block.asm

+    instr or_into_C X, Y = bin.or X, Y -> C;
+
+    // permutation to machine bin4
+    instr or4 X, Y, Z, W -> R = bin4.or4;


These are lookups, no?

georgwiese · 2024-03-18T09:57:56Z

test_data/asm/permutations/block_to_block.asm

+    call_selectors sel;
+
+    // permutation links to Binary machine
+    link 1 ~> bin.or A, B -> X;


Suggested change

link 1 ~> bin.or A, B -> X;

link array::sum(sel) ~> bin.or A, B -> X;

No? Also, the sum of selectors needs to be constrained to be binary then I think.

I've updated the example. I think the constraint force_bool(sum(sel)) could also be auto inserted by the compiler, but from our discussions I left it up to the user to add it to the asm.

georgwiese

Great! With this and some other recently merged PRs, the memory machine is now working (#1129)! 🎉

I also tried adding call_selectors sel; to a bunch of machines in the standard library, so now we can use them both via a permutation and lookup. Probably, we should do that in a follow-up and also connect machines via permutations in the RISC-V machine!

As another follow-up, I think we need to update the book, right?

by instructions and links using `~` instead of `=`. Block machines must declare `call_selectors`.

chriseth reviewed Mar 6, 2024

View reviewed changes

ast/src/object/mod.rs Outdated Show resolved Hide resolved

chriseth reviewed Mar 6, 2024

View reviewed changes

parser/src/powdr.lalrpop Outdated Show resolved Hide resolved

chriseth reviewed Mar 7, 2024

View reviewed changes

ast/src/parsed/asm.rs Outdated Show resolved Hide resolved

pacheco force-pushed the instr_permutation branch from 6e5adde to c3f5aba Compare March 8, 2024 18:58

georgwiese mentioned this pull request Mar 11, 2024

Remove duplicate identities #1147

Merged

pacheco force-pushed the instr_permutation branch from 9884947 to 299b37b Compare March 12, 2024 17:39

pacheco marked this pull request as ready for review March 12, 2024 18:10

leonardoalt requested a review from chriseth March 12, 2024 18:53

georgwiese self-requested a review March 13, 2024 08:56

georgwiese reviewed Mar 13, 2024

View reviewed changes

georgwiese mentioned this pull request Mar 13, 2024

Fix Witgen for machines connected by permutation with latch on first row #1157

Merged

pacheco force-pushed the instr_permutation branch from 3293b4b to b64857b Compare March 15, 2024 19:33

georgwiese reviewed Mar 18, 2024

View reviewed changes

georgwiese approved these changes Mar 20, 2024

View reviewed changes

Allow machines to be linked via permutation

edaf536

by instructions and links using `~` instead of `=`. Block machines must declare `call_selectors`.

pacheco force-pushed the instr_permutation branch from 09a1651 to edaf536 Compare March 20, 2024 11:20

georgwiese added this pull request to the merge queue Mar 20, 2024

Merged via the queue into main with commit 9fc93a3 Mar 20, 2024
5 checks passed

georgwiese deleted the instr_permutation branch March 20, 2024 12:16

This was referenced Mar 22, 2024

Add read/write memory to standard library #1129

Merged

Powdr ASM: Allow machines to be linked via permutaions #1073

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Permutation instructions/links #1126

Permutation instructions/links #1126

pacheco commented Mar 5, 2024 •

edited

Loading

georgwiese commented Mar 6, 2024

chriseth commented Mar 7, 2024

georgwiese left a comment

georgwiese Mar 13, 2024

georgwiese Mar 13, 2024

georgwiese Mar 13, 2024

georgwiese Mar 13, 2024

georgwiese Mar 13, 2024

pacheco Mar 13, 2024 •

edited

Loading

georgwiese Mar 13, 2024

pacheco Mar 13, 2024 •

edited

Loading

georgwiese Mar 13, 2024

pacheco commented Mar 13, 2024

georgwiese commented Mar 13, 2024

georgwiese left a comment

georgwiese Mar 18, 2024

georgwiese Mar 18, 2024

georgwiese Mar 18, 2024

georgwiese Mar 18, 2024

pacheco Mar 18, 2024

georgwiese left a comment

-    link 1 ~> bin.or A, B -> X;
-    link 1 ~> bin.or C, D -> Y;
-    link 1 ~> bin.or X, Y -> E;
-    col fixed operation_id = [0]*;
-    col fixed latch = [1]*;
+    link latch ~> bin.or A, B -> X;
+    link latch ~> bin.or C, D -> Y;
+    link latch ~> bin.or X, Y -> E;
+    col fixed operation_id = [0]*;
+    // TODO: Currently, witgen fails if we set the latch to [1]*, because then the machine
+    // does not get detected as a block machine and connecting VMs via permutations is not supported
+    // yet. By setting the latch to [0, 1]*, the first row of every block is completely unconstrained.
+    col fixed latch = [0, 1]*;

	link 1 ~> bin.or A, B -> X;
	link array::sum(sel) ~> bin.or A, B -> X;

Permutation instructions/links #1126

Permutation instructions/links #1126

Conversation

pacheco commented Mar 5, 2024 • edited Loading

georgwiese commented Mar 6, 2024

chriseth commented Mar 7, 2024

georgwiese 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

pacheco Mar 13, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pacheco Mar 13, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pacheco commented Mar 13, 2024

georgwiese commented Mar 13, 2024

georgwiese 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

georgwiese left a comment

Choose a reason for hiding this comment

pacheco commented Mar 5, 2024 •

edited

Loading

pacheco Mar 13, 2024 •

edited

Loading

pacheco Mar 13, 2024 •

edited

Loading