-
Notifications
You must be signed in to change notification settings - Fork 11
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(constraints): add rpo constraints #257
base: next
Are you sure you want to change the base?
Changes from 1 commit
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,12 +1,49 @@ | ||
mod HashChipletAir | ||
|
||
### Constants and periodic columns ################################################################ | ||
const MDS = [ | ||
[7, 23, 8, 26, 13, 10, 9, 7, 6, 22, 21, 8], | ||
[8, 7, 23, 8, 26, 13, 10, 9, 7, 6, 22, 21], | ||
[21, 8, 7, 23, 8, 26, 13, 10, 9, 7, 6, 22], | ||
[22, 21, 8, 7, 23, 8, 26, 13, 10, 9, 7, 6], | ||
[6, 22, 21, 8, 7, 23, 8, 26, 13, 10, 9, 7], | ||
[7, 6, 22, 21, 8, 7, 23, 8, 26, 13, 10, 9], | ||
[9, 7, 6, 22, 21, 8, 7, 23, 8, 26, 13, 10], | ||
[10, 9, 7, 6, 22, 21, 8, 7, 23, 8, 26, 13], | ||
[13, 10, 9, 7, 6, 22, 21, 8, 7, 23, 8, 26], | ||
[26, 13, 10, 9, 7, 6, 22, 21, 8, 7, 23, 8], | ||
[8, 26, 13, 10, 9, 7, 6, 22, 21, 8, 7, 23], | ||
[23, 8, 26, 13, 10, 9, 7, 6, 22, 21, 8, 7] | ||
] | ||
|
||
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] | ||
|
||
ark_0: [5789762306288267264, 12987190162843097088, 18072785500942327808, 5674685213610122240, 4887609836208846848, 16308865189192448000, 7123075680859040768, 0] | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Maybe we should add a blank line between |
||
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] | ||
|
||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. nit: I would leave the blank line above the comment |
||
### Helper functions ############################################################################## | ||
|
||
|
@@ -83,6 +120,13 @@ 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]') | ||
|
||
fn apply_mds(state: vector[12]) -> vector[12]: | ||
let result = [sum([state[i] * mds_row[i] for i in 0..12]) for mds_row in MDS] | ||
return result | ||
|
||
fn apply_sbox(state: vector[12]) -> vector[12]: | ||
let result = [s^7 for s in state] | ||
return result | ||
|
||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I noticed that there is an error in the function above this There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I fixed it in the hasher multiset check constraints PR (here) There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I noticed that there is an error in the function above this |
||
### Helper evaluators ############################################################################# | ||
|
||
|
@@ -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]]): | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Done in this PR. |
||
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] | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Maybe move whole There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'm not sure that would work since the values are different based on the row. Or maybe I misunderstood something? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Ah, my bad, |
||
|
||
# compute the state that should result from applying the first 5 operations of the RPO round to | ||
# the current hash state. | ||
let step1_initial = apply_mds(h) | ||
|
||
# add constants | ||
let step1_with_constants = [step1_initial[i] + ark[i] for i in 0..12] | ||
|
||
# apply sbox | ||
let step1_with_sbox = apply_sbox(step1_with_constants) | ||
|
||
# apply mds | ||
let step1_with_mds = apply_mds(step1_with_sbox) | ||
|
||
# add constants | ||
let step1 = [step1_with_mds[i] + ark[i + 12] for i in 0..12] | ||
|
||
# compute the state that should result from applying the inverse of the last operation of the | ||
# RPO round to the next step of the computation. | ||
let step2 = apply_sbox(h) | ||
|
||
# make sure that the results are equal. | ||
enf step1[i] = step2[i] for i in 0..12 when !k0 | ||
|
||
### Hash Chiplet Air Constraints ################################################################## | ||
|
||
|
@@ -198,7 +269,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]) | ||
|
||
enf hasher_state([s, h, i]) | ||
|
||
# Multiset check constraints | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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