Skip to content

Commit 289385c

Browse files
tohrniitohrnii
committed
refactor(constraints): move rpo constraints to another file
1 parent c05e0e4 commit 289385c

File tree

2 files changed

+90
-82
lines changed

2 files changed

+90
-82
lines changed

‎constraints/miden-vm/hash.air‎

Lines changed: 9 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -1,49 +1,12 @@
1+
use rpo::enforce_rpo_round
2+
13
mod HashChipletAir
24

35
### Constants and periodic columns ################################################################
4-
const MDS = [
5-
[7, 23, 8, 26, 13, 10, 9, 7, 6, 22, 21, 8],
6-
[8, 7, 23, 8, 26, 13, 10, 9, 7, 6, 22, 21],
7-
[21, 8, 7, 23, 8, 26, 13, 10, 9, 7, 6, 22],
8-
[22, 21, 8, 7, 23, 8, 26, 13, 10, 9, 7, 6],
9-
[6, 22, 21, 8, 7, 23, 8, 26, 13, 10, 9, 7],
10-
[7, 6, 22, 21, 8, 7, 23, 8, 26, 13, 10, 9],
11-
[9, 7, 6, 22, 21, 8, 7, 23, 8, 26, 13, 10],
12-
[10, 9, 7, 6, 22, 21, 8, 7, 23, 8, 26, 13],
13-
[13, 10, 9, 7, 6, 22, 21, 8, 7, 23, 8, 26],
14-
[26, 13, 10, 9, 7, 6, 22, 21, 8, 7, 23, 8],
15-
[8, 26, 13, 10, 9, 7, 6, 22, 21, 8, 7, 23],
16-
[23, 8, 26, 13, 10, 9, 7, 6, 22, 21, 8, 7]
17-
]
18-
196
periodic_columns:
207
cycle_row_0: [1, 0, 0, 0, 0, 0, 0, 0]
218
cycle_row_6: [0, 0, 0, 0, 0, 0, 1, 0]
229
cycle_row_7: [0, 0, 0, 0, 0, 0, 0, 1]
23-
ark_0: [5789762306288267264, 12987190162843097088, 18072785500942327808, 5674685213610122240, 4887609836208846848, 16308865189192448000, 7123075680859040768, 0]
24-
ark_1: [6522564764413702144, 653957632802705280, 6200974112677013504, 5759084860419474432, 3027115137917284352, 11977192855656443904, 1034205548717903104, 0]
25-
ark_2: [17809893479458207744, 4441654670647621120, 17682092219085883392, 13943282657648898048, 9595098600469471232, 12532242556065779712, 7717824418247931904, 0]
26-
ark_3: [107145243989736512, 4038207883745915904, 10599526828986757120, 1352748651966375424, 10528569829048483840, 14594890931430969344, 3019070937878604288, 0]
27-
ark_4: [6388978042437517312, 5613464648874829824, 975003873302957312, 17110913224029904896, 7864689113198940160, 7291784239689209856, 11403792746066868224, 0]
28-
ark_5: [15844067734406017024, 13222989726778339328, 8264241093196931072, 1003883795902368384, 17533723827845969920, 5514718540551361536, 10280580802233112576, 0]
29-
ark_6: [9975000513555218432, 3037761201230264320, 10065763900435474432, 4141870621881018368, 5781638039037711360, 10025733853830934528, 337153209462421248, 0]
30-
ark_7: [3344984123768313344, 16683759727265179648, 2181131744534710272, 8121410972417424384, 17024078752430718976, 7293794580341021696, 13333398568519923712, 0]
31-
ark_8: [9959189626657347584, 8337364536491240448, 6317303992309419008, 14300518605864919040, 109659393484013504, 6728552937464861696, 3596153696935337472, 0]
32-
ark_9: [12960773468763564032, 3227397518293416448, 1401440938888741632, 13712227150607669248, 7158933660534805504, 6332385040983343104, 8104208463525993472, 0]
33-
ark_10: [9602914297752487936, 8110510111539675136, 8884468225181997056, 17021852944633065472, 2955076958026921984, 13277683694236792832, 14345062289456084992, 0]
34-
ark_11: [16657542370200465408, 2872078294163232256, 13066900325715521536, 6252096473787587584, 7433723648458773504, 2600778905124452864, 17036731477169661952, 0]
35-
ark_12: [6077062762357203968, 6202948458916100096, 8023374565629191168, 18389244934624493568, 6982293561042363392, 3736792340494631424, 17130398059294019584, 0]
36-
ark_13: [15277620170502010880, 17690140365333231616, 15013690343205953536, 16731736864863924224, 14065426295947720704, 577852220195055360, 519782857322262016, 0]
37-
ark_14: [5358738125714196480, 3595001575307484672, 4485500052507913216, 4440209734760478208, 16451845770444974080, 6689998335515780096, 9625384390925084672, 0]
38-
ark_15: [14233283787297595392, 373995945117666496, 12489737547229155328, 17208448209698889728, 7139138592091307008, 13886063479078012928, 1664893052631119104, 0]
39-
ark_16: [13792579614346651648, 1235734395091296000, 9500452585969031168, 8739495587021565952, 9012006439959783424, 14358505101923203072, 7629576092524553216, 0]
40-
ark_17: [11614812331536766976, 14172757457833930752, 2054001340201038848, 17000774922218162176, 14619614108529063936, 7744142531772273664, 3485239601103661568, 0]
41-
ark_18: [14871063686742261760, 707573103686350208, 12420704059284934656, 13533282547195531264, 1394813199588124416, 16135070735728404480, 9755891797164034048, 0]
42-
ark_19: [10148237148793042944, 15453217512188186624, 355990932618543744, 525402848358706240, 4635111139507788800, 12290902521256030208, 15218148195153268736, 0]
43-
ark_20: [4457428952329675776, 219777875004506016, 9071225051243524096, 16987541523062161408, 16217473952264204288, 12059913662657710080, 16460604813734957056, 0]
44-
ark_21: [15590786458219171840, 17876696346199468032, 12766199826003447808, 5466806524462796800, 10782018226466330624, 16456018495793752064, 9643968136937730048, 0]
45-
ark_22: [10063319113072093184, 17731621626449383424, 9045979173463557120, 14512769585918244864, 6844229992533661696, 4571485474751953408, 3611348709641382912, 0]
46-
ark_23: [14200078843431360512, 2897136237748376064, 12934431667190679552, 10973956031244050432, 7446486531695178752, 17200392109565784064, 18256379591337758720, 0]
4710

4811
### Helper functions ##############################################################################
4912

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

123-
fn apply_mds(state: vector[12]) -> vector[12]:
124-
let result = [sum([state[i] * mds_row[i] for i in 0..12]) for mds_row in MDS]
125-
return result
126-
127-
fn apply_sbox(state: vector[12]) -> vector[12]:
128-
let result = [s^7 for s in state]
129-
return result
130-
13186
### Helper evaluators #############################################################################
13287

13388
# Enforces that column must be binary.
134-
ev is_binary(main: [a]):
89+
ev is_binary([a]):
13590
enf a^2 = a
13691

13792

13893
# Enforces that value in column is copied over to the next row.
139-
ev is_unchanged(main: [column]):
94+
ev is_unchanged([column]):
14095
ev column' = column
14196

14297

14398
# Enforce selector columns constraints
144-
ev selector_columns(main: [s[3]]):
99+
ev selector_columns([s[3]]):
145100
let f_out = get_f_out(s)
146101
let f_out_next = get_f_out_next(s)
147102
let f_abp = get_f_abp(s)
@@ -170,7 +125,7 @@ ev selector_columns(main: [s[3]]):
170125

171126

172127
# Enforce node index constraints
173-
ev node_index(main: [s[3], i]):
128+
ev node_index([s[3], i]):
174129
let f_out = get_f_out(s)
175130
let f_mp = get_f_mp(s)
176131
let f_mv = get_f_mv(s)
@@ -200,7 +155,7 @@ ev node_index(main: [s[3], i]):
200155

201156

202157
# Enforce hasher state constraints
203-
ev hasher_state(main: [s[3], h[12], i]):
158+
ev hasher_state([s[3], h[12], i]):
204159
let f_mp = get_f_mp(s)
205160
let f_mv = get_f_mv(s)
206161
let f_mu = get_f_mu(s)
@@ -225,38 +180,10 @@ ev hasher_state(main: [s[3], h[12], i]):
225180
is_unchanged(h[j + 4]) for j in 0..4 when !b & f_absorb_node
226181
h[j + 8]' = h[j + 4] for j in 0..4 when b & f_absorb_node
227182

228-
ev enforce_rpo_round(main: [h[12]]):
229-
let ark = [ark_0, ark_1, ark_2, ark_3, ark_4, ark_5, ark_6, ark_7, ark_8, ark_9, ark_10,
230-
ark_11, ark_12, ark_13, ark_14, ark_15, ark_16, ark_17, ark_18, ark_19, ark_20, ark_21,
231-
ark_22, ark_23]
232-
233-
# compute the state that should result from applying the first 5 operations of the RPO round to
234-
# the current hash state.
235-
let step1_initial = apply_mds(h)
236-
237-
# add constants
238-
let step1_with_constants = [step1_initial[i] + ark[i] for i in 0..12]
239-
240-
# apply sbox
241-
let step1_with_sbox = apply_sbox(step1_with_constants)
242-
243-
# apply mds
244-
let step1_with_mds = apply_mds(step1_with_sbox)
245-
246-
# add constants
247-
let step1 = [step1_with_mds[i] + ark[i + 12] for i in 0..12]
248-
249-
# compute the state that should result from applying the inverse of the last operation of the
250-
# RPO round to the next step of the computation.
251-
let step2 = apply_sbox(h)
252-
253-
# make sure that the results are equal.
254-
enf step1[i] = step2[i] for i in 0..12 when !k0
255-
256183
### Hash Chiplet Air Constraints ##################################################################
257184

258185
# Enforces the constraints on the hash chiplet, given the columns of the hash execution trace.
259-
ev hash_chiplet(main: [s[3], r, h[12], i]):
186+
ev hash_chiplet([s[3], r, h[12], i]):
260187
## Row address constraint ##
261188
# TODO: Apply row address constraints:
262189
# 1. Boundary constraint `enf r.first = 1`
@@ -269,7 +196,7 @@ ev hash_chiplet(main: [s[3], r, h[12], i]):
269196
enf node_index([s, i])
270197

271198
## Hasher state constraints ##
272-
enf enforce_rpo_round([h])
199+
enf enforce_rpo_round([h]) when !cycle_row_0
273200

274201
enf hasher_state([s, h, i])
275202

‎constraints/miden-vm/rpo.air‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
mod RPOAir
2+
3+
### Constants and periodic columns ################################################################
4+
const MDS = [
5+
[7, 23, 8, 26, 13, 10, 9, 7, 6, 22, 21, 8],
6+
[8, 7, 23, 8, 26, 13, 10, 9, 7, 6, 22, 21],
7+
[21, 8, 7, 23, 8, 26, 13, 10, 9, 7, 6, 22],
8+
[22, 21, 8, 7, 23, 8, 26, 13, 10, 9, 7, 6],
9+
[6, 22, 21, 8, 7, 23, 8, 26, 13, 10, 9, 7],
10+
[7, 6, 22, 21, 8, 7, 23, 8, 26, 13, 10, 9],
11+
[9, 7, 6, 22, 21, 8, 7, 23, 8, 26, 13, 10],
12+
[10, 9, 7, 6, 22, 21, 8, 7, 23, 8, 26, 13],
13+
[13, 10, 9, 7, 6, 22, 21, 8, 7, 23, 8, 26],
14+
[26, 13, 10, 9, 7, 6, 22, 21, 8, 7, 23, 8],
15+
[8, 26, 13, 10, 9, 7, 6, 22, 21, 8, 7, 23],
16+
[23, 8, 26, 13, 10, 9, 7, 6, 22, 21, 8, 7]
17+
]
18+
19+
periodic_columns:
20+
ark_0: [5789762306288267264, 12987190162843097088, 18072785500942327808, 5674685213610122240, 4887609836208846848, 16308865189192448000, 7123075680859040768, 0]
21+
ark_1: [6522564764413702144, 653957632802705280, 6200974112677013504, 5759084860419474432, 3027115137917284352, 11977192855656443904, 1034205548717903104, 0]
22+
ark_2: [17809893479458207744, 4441654670647621120, 17682092219085883392, 13943282657648898048, 9595098600469471232, 12532242556065779712, 7717824418247931904, 0]
23+
ark_3: [107145243989736512, 4038207883745915904, 10599526828986757120, 1352748651966375424, 10528569829048483840, 14594890931430969344, 3019070937878604288, 0]
24+
ark_4: [6388978042437517312, 5613464648874829824, 975003873302957312, 17110913224029904896, 7864689113198940160, 7291784239689209856, 11403792746066868224, 0]
25+
ark_5: [15844067734406017024, 13222989726778339328, 8264241093196931072, 1003883795902368384, 17533723827845969920, 5514718540551361536, 10280580802233112576, 0]
26+
ark_6: [9975000513555218432, 3037761201230264320, 10065763900435474432, 4141870621881018368, 5781638039037711360, 10025733853830934528, 337153209462421248, 0]
27+
ark_7: [3344984123768313344, 16683759727265179648, 2181131744534710272, 8121410972417424384, 17024078752430718976, 7293794580341021696, 13333398568519923712, 0]
28+
ark_8: [9959189626657347584, 8337364536491240448, 6317303992309419008, 14300518605864919040, 109659393484013504, 6728552937464861696, 3596153696935337472, 0]
29+
ark_9: [12960773468763564032, 3227397518293416448, 1401440938888741632, 13712227150607669248, 7158933660534805504, 6332385040983343104, 8104208463525993472, 0]
30+
ark_10: [9602914297752487936, 8110510111539675136, 8884468225181997056, 17021852944633065472, 2955076958026921984, 13277683694236792832, 14345062289456084992, 0]
31+
ark_11: [16657542370200465408, 2872078294163232256, 13066900325715521536, 6252096473787587584, 7433723648458773504, 2600778905124452864, 17036731477169661952, 0]
32+
ark_12: [6077062762357203968, 6202948458916100096, 8023374565629191168, 18389244934624493568, 6982293561042363392, 3736792340494631424, 17130398059294019584, 0]
33+
ark_13: [15277620170502010880, 17690140365333231616, 15013690343205953536, 16731736864863924224, 14065426295947720704, 577852220195055360, 519782857322262016, 0]
34+
ark_14: [5358738125714196480, 3595001575307484672, 4485500052507913216, 4440209734760478208, 16451845770444974080, 6689998335515780096, 9625384390925084672, 0]
35+
ark_15: [14233283787297595392, 373995945117666496, 12489737547229155328, 17208448209698889728, 7139138592091307008, 13886063479078012928, 1664893052631119104, 0]
36+
ark_16: [13792579614346651648, 1235734395091296000, 9500452585969031168, 8739495587021565952, 9012006439959783424, 14358505101923203072, 7629576092524553216, 0]
37+
ark_17: [11614812331536766976, 14172757457833930752, 2054001340201038848, 17000774922218162176, 14619614108529063936, 7744142531772273664, 3485239601103661568, 0]
38+
ark_18: [14871063686742261760, 707573103686350208, 12420704059284934656, 13533282547195531264, 1394813199588124416, 16135070735728404480, 9755891797164034048, 0]
39+
ark_19: [10148237148793042944, 15453217512188186624, 355990932618543744, 525402848358706240, 4635111139507788800, 12290902521256030208, 15218148195153268736, 0]
40+
ark_20: [4457428952329675776, 219777875004506016, 9071225051243524096, 16987541523062161408, 16217473952264204288, 12059913662657710080, 16460604813734957056, 0]
41+
ark_21: [15590786458219171840, 17876696346199468032, 12766199826003447808, 5466806524462796800, 10782018226466330624, 16456018495793752064, 9643968136937730048, 0]
42+
ark_22: [10063319113072093184, 17731621626449383424, 9045979173463557120, 14512769585918244864, 6844229992533661696, 4571485474751953408, 3611348709641382912, 0]
43+
ark_23: [14200078843431360512, 2897136237748376064, 12934431667190679552, 10973956031244050432, 7446486531695178752, 17200392109565784064, 18256379591337758720, 0]
44+
45+
### Helper functions ##############################################################################
46+
47+
fn apply_mds(state: vector[12]) -> vector[12]:
48+
return [sum([state[i] * mds_row[i] for i in 0..12]) for mds_row in MDS]
49+
50+
fn apply_sbox(state: vector[12]) -> vector[12]:
51+
return [s^7 for s in state]
52+
53+
### RPO Air Constraints ##################################################################
54+
55+
ev enforce_rpo_round([h[12]]):
56+
let ark = [ark_0, ark_1, ark_2, ark_3, ark_4, ark_5, ark_6, ark_7, ark_8, ark_9, ark_10,
57+
ark_11, ark_12, ark_13, ark_14, ark_15, ark_16, ark_17, ark_18, ark_19, ark_20, ark_21,
58+
ark_22, ark_23]
59+
60+
# compute the state that should result from applying the first 5 operations of the RPO round to
61+
# the current hash state.
62+
let step1_initial = apply_mds(h)
63+
64+
# add constants
65+
let step1_with_constants = [step1_initial[i] + ark[i] for i in 0..12]
66+
67+
# apply sbox
68+
let step1_with_sbox = apply_sbox(step1_with_constants)
69+
70+
# apply mds
71+
let step1_with_mds = apply_mds(step1_with_sbox)
72+
73+
# add constants
74+
let step1 = [step1_with_mds[i] + ark[i + 12] for i in 0..12]
75+
76+
# compute the state that should result from applying the inverse of the last operation of the
77+
# RPO round to the next step of the computation.
78+
let step2 = apply_sbox(h)
79+
80+
# make sure that the results are equal.
81+
enf step1[i] = step2[i] for i in 0..12

0 commit comments

Comments
 (0)