Write hasher multiset check constraints in AirScript #261

Fumuran · 2023-04-20T15:59:11Z

Addressing: #200
This PR adds constraints for the hash chiplet bus and hash chiplet sibling table.

grjte

Thanks @Overcastan! I left my comments inline

grjte · 2023-05-03T08:58:24Z

constraints/miden-vm/hash.air

+# Set to 1 when selector flags are (1,0,0) on rows which are multiples of 8. This is flag of the 
+# single permutation, a 2-to-1 hash, or a linear hash of many elements.


nit: I would change the second sentence to "This flag indicates that we are initiating computation of a single permutation, a 2-to-1 hash, or a linear hash of many elements."

grjte · 2023-05-03T09:01:28Z

constraints/miden-vm/hash.air

+# Set to 1 when selector flags are (0,0,0) on rows which are 1 less than a multiple of 8. This is 
+# flag of the instruction that returns the result of the currently running computation.


nit: Since it's not exactly an instruction, I would change the second sentence to "This flag indicates that the result of the currently running computation is returned."

grjte · 2023-05-03T09:01:52Z

constraints/miden-vm/hash.air

+# Set to 1 when selector flags are (0,0,1) on rows which are 1 less than a multiple of 8. This is 
+# flag of the instruction that returns the whole hasher state.


nit: I would change the second sentence to "This flag indicates that the entire hasher state is returned."

grjte · 2023-05-03T09:03:38Z

constraints/miden-vm/hash.air

-    return cycle_row_7 & binary_not(s[0]) & binary_not(s[1])
-
-
-# Flag f_out_next is set to 1 when either f_hout = 1 or f_sout = 1 in the next row.
-fn get_f_out_next(s: vector[3]) -> scalar:
-    return cycle_row_6 & binary_not(s[0]') & binary_not(s[1]')
+    return cycle_row_7 & !s[0] & !s[1]


We can't actually make this change because these flags use different periodic columns

grjte · 2023-05-03T09:05:08Z

constraints/miden-vm/hash.air

+    let s_next = [s_i' for s_i in s]
+


This variable shouldn't be necessary - we can just pass s' instead.

grjte · 2023-05-03T09:20:10Z

constraints/miden-vm/hash.air

+    p0' = p0 * ((get_f_bp(s) + get_f_sout(s)) * v_all + (get_f_mp(s) + get_f_mv(s) + get_f_mu(s)) * 
+        v_leaf + get_f_abp(s) * v_abp + get_f_hout(s) * v_res + 1 - 
+        (get_f_bp(s) + get_f_mp(s) + get_f_mv(s) + get_f_mu(s) + get_f_abp(s) + get_f_out(s)))


nit: almost all of these flags are computed twice, which I would probably avoid. It's not a big deal, though, since it will be optimized by the compiler anyway.

Let's also add a comment with the constraint degree

grjte · 2023-05-03T09:23:36Z

constraints/miden-vm/hash.air

+
+
+# Enforce constraints for the hash chiplet sibling table.


nit: I would change this to: "Enforce constraints for the hash chiplet sibling table, which is used to keep track of sibling nodes used during Merkle root update computations." I would probably even add the next bit from the docs with the 2 rules that need to be enforced.

grjte · 2023-05-03T09:26:14Z

constraints/miden-vm/hash.air

-    # TODO: Apply multiset check constraints
+    # TODO: Apply multiset check constraints
+


The new helper evaluators should go above in the helper evaluator section so that the hash_chiplet evaluator is still the last thing in the file as we've done in other places.

We should add calls to the two new evaluators here and remove this TODO

grjte · 2023-05-03T09:27:24Z

constraints/miden-vm/hash.air

+    enf p1' * ((get_f_mv(s) + get_f_mva(s)) * v_sibling + 1 - (get_f_mv(s) + get_f_mva(s))) = 
+        p1 * ((get_f_mu(s) + get_f_mua(s)) * v_sibling + 1 - (get_f_mu(s) + get_f_mua(s)))


Let's add a comment with the constraint degree

grjte · 2023-05-03T09:28:36Z

constraints/miden-vm/hash.air

+    # Enforce that computation of the old Merkle root is immediately followed by the computation of 
+    # the new Merkle root.
+    enf (get_f_bp(s) + get_f_mp(s) + get_f_mv(s) * (1 - p1)) = 0


The paren is in the wrong place here. This should be:

enf (get_f_bp(s) + get_f_mp(s) + get_f_mv(s)) * (1 - p1) = 0

Let's also add a comment with the constraint degree.

Fumuran · 2023-05-04T10:53:23Z

constraints/miden-vm/hash.air

+    # Constraints degree: 7
    enf is_unchanged([s[1]]) when !f_out & !f_out_next
    enf is_unchanged([s[2]]) when !f_out & !f_out_next


I think there is a typo in the docs regarding the degree of these constraints (imho it should be 7, not 9). The f_out flag has degree 3, not 4, since it is computed using only one periodic column and two selectors (as opposed to f_hout and f_sout flags, which use three selectors)

Fumuran · 2023-05-04T10:55:07Z

constraints/miden-vm/hash.air

+    # Constraint degree: 4
    enf f_out * i = 0


Similar comment to the one above: I think the degree of this constraint should be 4, not 5.

Fumuran · 2023-05-04T10:58:35Z

constraints/miden-vm/hash.air

+    # TODO: Apply row address constraints:
+    # 1. Boundary constraint `enf r.first = 1`
+    # 2. Transition constraint. It requires chiplets module's selector flag s0.


I think we can add this transition constraint, I'm just not sure where we should place chip_s0 chiplet module's selector flag -- to the first (main) segment, or to the second (aux).

Fumuran requested review from grjte and tohrnii April 20, 2023 15:59

grjte suggested changes May 3, 2023

View reviewed changes

Fumuran commented May 4, 2023

View reviewed changes

Fumuran requested a review from grjte May 4, 2023 10:59

Fumuran mentioned this pull request May 4, 2023

feat(constraints): add rpo constraints #257

Open

Fumuran added 4 commits June 7, 2023 14:11

feat: write hasher bus constraints

e689b57

feat: write hasher sibling table constraints

6b8e657

refactor: improve docs and names, fix bugs

4ecfb3e

refactor: move chiplet bus constraints to the separate file

c8b3431

Fumuran force-pushed the andrew-hasher-multiset-constraints branch from a42f7bd to c8b3431 Compare June 7, 2023 11:21

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Write hasher multiset check constraints in AirScript #261

Write hasher multiset check constraints in AirScript #261

Fumuran commented Apr 20, 2023

grjte left a comment

grjte May 3, 2023

grjte May 3, 2023

grjte May 3, 2023

grjte May 3, 2023

grjte May 3, 2023

grjte May 3, 2023

grjte May 3, 2023

grjte May 3, 2023

grjte May 3, 2023

grjte May 3, 2023

Fumuran May 4, 2023 •

edited

Loading

Fumuran May 4, 2023

Fumuran May 4, 2023

		# Set to 1 when selector flags are (1,0,0) on rows which are multiples of 8. This is flag of the
		# single permutation, a 2-to-1 hash, or a linear hash of many elements.

		# Set to 1 when selector flags are (0,0,0) on rows which are 1 less than a multiple of 8. This is
		# flag of the instruction that returns the result of the currently running computation.

		# TODO: Apply multiset check constraints No newline at end of file
		# TODO: Apply multiset check constraints

		enf p1' * ((get_f_mv(s) + get_f_mva(s)) * v_sibling + 1 - (get_f_mv(s) + get_f_mva(s))) =
		p1 * ((get_f_mu(s) + get_f_mua(s)) * v_sibling + 1 - (get_f_mu(s) + get_f_mua(s)))

Write hasher multiset check constraints in AirScript #261

Are you sure you want to change the base?

Write hasher multiset check constraints in AirScript #261

Conversation

Fumuran commented Apr 20, 2023

grjte 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

Fumuran May 4, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Fumuran May 4, 2023 •

edited

Loading