feat(constraints): add rpo constraints #257

tohrnii · 2023-04-18T07:54:48Z

Addressing #212.

Question: Should I split it into another module assuming modules will be able to import other modules in the future or just leave it as is for now?

Fumuran

Thank you @tohrnii, looks good! I left just few small nits.

Fumuran · 2023-04-24T11:42:32Z

constraints/miden-vm/hash.air

    cycle_row_7: [0, 0, 0, 0, 0, 0, 0, 1]
-
+    ark_0: [5789762306288267264, 12987190162843097088, 18072785500942327808, 5674685213610122240, 4887609836208846848, 16308865189192448000, 7123075680859040768, 0]


Maybe we should add a blank line between cycle_row_7 and ark_0 to separate general periodic columns of the hasher and periodic columns that are required for the RPO, that will look more structured.

Fumuran · 2023-04-24T12:01:39Z

constraints/miden-vm/hash.air

+    let ark = [ark_0, ark_1, ark_2, ark_3, ark_4, ark_5, ark_6, ark_7, ark_8, ark_9, ark_10,
+        ark_11, ark_12, ark_13, ark_14, ark_15, ark_16, ark_17, ark_18, ark_19, ark_20, ark_21,
+        ark_22, ark_23]


Maybe move whole ark array to the constants as well? Wdyt?

I'm not sure that would work since the values are different based on the row. Or maybe I misunderstood something?

Ah, my bad, ark_i are periodic columns, not constant arrays.

Fumuran · 2023-04-24T12:08:29Z

constraints/miden-vm/hash.air

@@ -181,6 +225,33 @@ ev hasher_state(main: [s[3], h[12], i]):
        is_unchanged(h[j + 4]) for j in 0..4 when !b & f_absorb_node
        h[j + 8]' = h[j + 4] for j in 0..4 when b & f_absorb_node

+ev enforce_rpo_round(main: [h[12]]):


We don't need segment names any more, so here and in the other evaluators we should get rid of them.

But maybe it will be better to remove them in a future PR, I'm not sure.

Done in this PR.

Fumuran · 2023-04-24T12:20:25Z

About your question: in my opinion it will be indeed better to move RPO constraints to the separate file, since they have a lot of data that is needed just for RPO and require only h columns to be evaluated.

tohrnii · 2023-04-24T15:05:56Z

About your question: in my opinion it will be indeed better to move RPO constraints to the separate file, since they have a lot of data that is needed just for RPO and require only h columns to be evaluated.

Makes sense. Moved to another file.

Fumuran

Looks great to me, thank you @tohrnii!

constraints/miden-vm/rpo.air

grjte

Thanks @tohrnii, looks good overall. I left a few things inline

grjte · 2023-05-01T08:40:44Z

constraints/miden-vm/hash.air

+use rpo::enforce_rpo_round
+


Imports should go after the module declaration. (In the case of the top-level AIR file, they'll go after the def statement.)

mod HashChipletAir use rpo::enforce_rpo_round ...

grjte · 2023-05-01T08:41:08Z

constraints/miden-vm/hash.air

 periodic_columns:
    cycle_row_0: [1, 0, 0, 0, 0, 0, 0, 0]
    cycle_row_6: [0, 0, 0, 0, 0, 0, 1, 0]
    cycle_row_7: [0, 0, 0, 0, 0, 0, 0, 1]

-


nit: I would leave the blank line above the comment

grjte · 2023-05-01T08:41:28Z

constraints/miden-vm/hash.air

 mod HashChipletAir

 ### Constants and periodic columns ################################################################
-


nit: I would probably leave this blank line. I think we do it in most other places, because when there are multiple things in a section it helps readability

grjte · 2023-05-01T08:43:00Z

constraints/miden-vm/rpo.air

@@ -0,0 +1,80 @@
+mod RPOAir


nit: I would do this like Rust as RpoAir

grjte · 2023-05-01T08:44:39Z

constraints/miden-vm/hash.air

@@ -83,21 +83,20 @@ fn get_f_out(s: vector[3]) -> scalar:
 fn get_f_out_next(s: vector[3]) -> scalar:
    return cycle_row_6 & binary_not(s[0]') & binary_not(s[1]')

-


I noticed that there is an error in the function above this get_f_out_next and maybe in other functions. Functions cannot call evaluators or access the next row. These should be fixed as a separate PR

I fixed it in the hasher multiset check constraints PR (here)

grjte · 2023-05-01T08:45:10Z

constraints/miden-vm/hash.air

@@ -83,21 +83,20 @@ fn get_f_out(s: vector[3]) -> scalar:
 fn get_f_out_next(s: vector[3]) -> scalar:
    return cycle_row_6 & binary_not(s[0]') & binary_not(s[1]')

-


I noticed that there is an error in the function above this get_f_out_next and maybe in other functions. Functions cannot call evaluators or access the next row. These should be fixed as a separate PR

grjte · 2023-05-01T08:50:24Z

constraints/miden-vm/hash.air

@@ -198,7 +196,8 @@ ev hash_chiplet(main: [s[3], r, h[12], i]):
    enf node_index([s, i])

    ## Hasher state constraints ##
-    # TODO: apply RPO constraints to the hasher state
+    enf enforce_rpo_round([h]) when !cycle_row_0


I think this is supposed to be when !cycle_row_7. Previously it was k0, but k0 was [0,0,0,0,0,0,0,1]. We've now renamed these based on which values are set. Please check carefully to make sure I'm right.

You're right. Thanks, fixed.

grjte · 2023-05-01T09:15:31Z

constraints/miden-vm/rpo.air

+    ark_0: [5789762306288267264, 12987190162843097088, 18072785500942327808, 5674685213610122240, 4887609836208846848, 16308865189192448000, 7123075680859040768, 0]
+    ark_1: [6522564764413702144, 653957632802705280, 6200974112677013504, 5759084860419474432, 3027115137917284352, 11977192855656443904, 1034205548717903104, 0]
+    ark_2: [17809893479458207744, 4441654670647621120, 17682092219085883392, 13943282657648898048, 9595098600469471232, 12532242556065779712, 7717824418247931904, 0]
+    ark_3: [107145243989736512, 4038207883745915904, 10599526828986757120, 1352748651966375424, 10528569829048483840, 14594890931430969344, 3019070937878604288, 0]
+    ark_4: [6388978042437517312, 5613464648874829824, 975003873302957312, 17110913224029904896, 7864689113198940160, 7291784239689209856, 11403792746066868224, 0]
+    ark_5: [15844067734406017024, 13222989726778339328, 8264241093196931072, 1003883795902368384, 17533723827845969920, 5514718540551361536, 10280580802233112576, 0]
+    ark_6: [9975000513555218432, 3037761201230264320, 10065763900435474432, 4141870621881018368, 5781638039037711360, 10025733853830934528, 337153209462421248, 0]
+    ark_7: [3344984123768313344, 16683759727265179648, 2181131744534710272, 8121410972417424384, 17024078752430718976, 7293794580341021696, 13333398568519923712, 0]
+    ark_8: [9959189626657347584, 8337364536491240448, 6317303992309419008, 14300518605864919040, 109659393484013504, 6728552937464861696, 3596153696935337472, 0]
+    ark_9: [12960773468763564032, 3227397518293416448, 1401440938888741632, 13712227150607669248, 7158933660534805504, 6332385040983343104, 8104208463525993472, 0]
+    ark_10: [9602914297752487936, 8110510111539675136, 8884468225181997056, 17021852944633065472, 2955076958026921984, 13277683694236792832, 14345062289456084992, 0]
+    ark_11: [16657542370200465408, 2872078294163232256, 13066900325715521536, 6252096473787587584, 7433723648458773504, 2600778905124452864, 17036731477169661952, 0]
+    ark_12: [6077062762357203968, 6202948458916100096, 8023374565629191168, 18389244934624493568, 6982293561042363392, 3736792340494631424, 17130398059294019584, 0]
+    ark_13: [15277620170502010880, 17690140365333231616, 15013690343205953536, 16731736864863924224, 14065426295947720704, 577852220195055360, 519782857322262016, 0]
+    ark_14: [5358738125714196480, 3595001575307484672, 4485500052507913216, 4440209734760478208, 16451845770444974080, 6689998335515780096, 9625384390925084672, 0]
+    ark_15: [14233283787297595392, 373995945117666496, 12489737547229155328, 17208448209698889728, 7139138592091307008, 13886063479078012928, 1664893052631119104, 0]
+    ark_16: [13792579614346651648, 1235734395091296000, 9500452585969031168, 8739495587021565952, 9012006439959783424, 14358505101923203072, 7629576092524553216, 0]
+    ark_17: [11614812331536766976, 14172757457833930752, 2054001340201038848, 17000774922218162176, 14619614108529063936, 7744142531772273664, 3485239601103661568, 0]
+    ark_18: [14871063686742261760, 707573103686350208, 12420704059284934656, 13533282547195531264, 1394813199588124416, 16135070735728404480, 9755891797164034048, 0]
+    ark_19: [10148237148793042944, 15453217512188186624, 355990932618543744, 525402848358706240, 4635111139507788800, 12290902521256030208, 15218148195153268736, 0]
+    ark_20: [4457428952329675776, 219777875004506016, 9071225051243524096, 16987541523062161408, 16217473952264204288, 12059913662657710080, 16460604813734957056, 0]
+    ark_21: [15590786458219171840, 17876696346199468032, 12766199826003447808, 5466806524462796800, 10782018226466330624, 16456018495793752064, 9643968136937730048, 0]
+    ark_22: [10063319113072093184, 17731621626449383424, 9045979173463557120, 14512769585918244864, 6844229992533661696, 4571485474751953408, 3611348709641382912, 0]
+    ark_23: [14200078843431360512, 2897136237748376064, 12934431667190679552, 10973956031244050432, 7446486531695178752, 17200392109565784064, 18256379591337758720, 0]


These round constants don't look right. Also, I think for clarity it would be good to use names like ark1_0, ..., ark1_11 and ark2_0, ..., ark2_11

These round constants don't look right

Can you please elaborate what you mean?

grjte · 2023-05-01T09:21:20Z

constraints/miden-vm/rpo.air

+    [23, 8, 26, 13, 10, 9, 7, 6, 22, 21, 8, 7]
+]
+
+periodic_columns:


let's add a comment to explain the round constants and how they are laid out here

grjte · 2023-05-01T09:27:16Z

constraints/miden-vm/rpo.air

+    let ark = [ark_0, ark_1, ark_2, ark_3, ark_4, ark_5, ark_6, ark_7, ark_8, ark_9, ark_10,
+        ark_11, ark_12, ark_13, ark_14, ark_15, ark_16, ark_17, ark_18, ark_19, ark_20, ark_21,
+        ark_22, ark_23]


For clarity, let's define a constant for STATE_WIDTH and use it everywhere instead of 12. I think it might also be clearer if we defined separate variables for ark1 and ark2. We couldn't do that in the Rust implementation because of the way we get periodic values from Winterfell, but we can do it here.

feat(constraints): add rpo constraints

c05e0e4

tohrnii requested review from Fumuran and grjte April 18, 2023 07:54

tohrnii marked this pull request as ready for review April 18, 2023 07:56

Fumuran requested changes Apr 24, 2023

View reviewed changes

tohrnii requested a review from Fumuran April 24, 2023 15:06

Fumuran approved these changes Apr 24, 2023

View reviewed changes

bobbinth reviewed Apr 24, 2023

View reviewed changes

constraints/miden-vm/rpo.air Outdated Show resolved Hide resolved

tohrnii force-pushed the tohrnii-rpo-constraints branch from 289385c to 691ac8e Compare April 24, 2023 18:41

grjte suggested changes May 1, 2023

View reviewed changes

tohrnii force-pushed the tohrnii-rpo-constraints branch from 691ac8e to 50d4856 Compare May 1, 2023 10:25

refactor(constraints): move rpo constraints to another file

37471df

tohrnii force-pushed the tohrnii-rpo-constraints branch from 50d4856 to 37471df Compare May 1, 2023 15:49

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(constraints): add rpo constraints #257

feat(constraints): add rpo constraints #257

tohrnii commented Apr 18, 2023 •

edited

Loading

Fumuran left a comment

Fumuran Apr 24, 2023

Fumuran Apr 24, 2023

tohrnii Apr 24, 2023

Fumuran Apr 24, 2023

Fumuran Apr 24, 2023

tohrnii Apr 24, 2023

Fumuran commented Apr 24, 2023

tohrnii commented Apr 24, 2023

Fumuran left a comment

grjte left a comment

grjte May 1, 2023

grjte May 1, 2023

grjte May 1, 2023

grjte May 1, 2023

grjte May 1, 2023

Fumuran May 4, 2023

grjte May 1, 2023

grjte May 1, 2023

tohrnii May 1, 2023

grjte May 1, 2023

tohrnii May 1, 2023

grjte May 1, 2023

grjte May 1, 2023

		cycle_row_7: [0, 0, 0, 0, 0, 0, 0, 1]

		ark_0: [5789762306288267264, 12987190162843097088, 18072785500942327808, 5674685213610122240, 4887609836208846848, 16308865189192448000, 7123075680859040768, 0]

		mod HashChipletAir

		### Constants and periodic columns ################################################################

		@@ -83,21 +83,20 @@ fn get_f_out(s: vector[3]) -> scalar:
		fn get_f_out_next(s: vector[3]) -> scalar:
		return cycle_row_6 & binary_not(s[0]') & binary_not(s[1]')

feat(constraints): add rpo constraints #257

Are you sure you want to change the base?

feat(constraints): add rpo constraints #257

Conversation

tohrnii commented Apr 18, 2023 • edited Loading

Fumuran 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

Fumuran commented Apr 24, 2023

tohrnii commented Apr 24, 2023

Fumuran left a comment

Choose a reason for hiding this comment

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tohrnii commented Apr 18, 2023 •

edited

Loading