-
Notifications
You must be signed in to change notification settings - Fork 22
/
air.rs
3322 lines (3086 loc) · 164 KB
/
air.rs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
use super::BITWISE_RATIO;
use super::CYCLE_HEIGHT;
use super::ECDSA_BUILTIN_RATIO;
use super::EC_OP_BUILTIN_RATIO;
use super::EC_OP_SCALAR_HEIGHT;
use super::MEMORY_STEP;
use super::PEDERSEN_BUILTIN_RATIO;
use super::POSEIDON_RATIO;
use super::POSEIDON_ROUNDS_FULL;
use super::PUBLIC_MEMORY_STEP;
use super::RANGE_CHECK_BUILTIN_PARTS;
use super::RANGE_CHECK_BUILTIN_RATIO;
use super::RANGE_CHECK_STEP;
use super::DILUTED_CHECK_N_BITS;
use super::DILUTED_CHECK_SPACING;
use super::ECDSA_SIG_CONFIG_ALPHA;
use super::ECDSA_SIG_CONFIG_BETA;
use crate::CairoAirConfig;
use crate::utils;
use crate::utils::compute_diluted_cumulative_value;
use crate::utils::map_into_fp_array;
use ark_ff::MontFp;
use ark_poly::EvaluationDomain;
use ark_poly::Radix2EvaluationDomain;
use binary::AirPublicInput;
use builtins::ecdsa;
use builtins::pedersen;
use builtins::poseidon;
use ministark::constraints::CompositionConstraint;
use ministark::constraints::CompositionItem;
use ministark::constraints::PeriodicColumn;
use ministark_gpu::fields::p3618502788666131213697322783095070105623107215331596699973092056135872020481::ark::Fp;
use ark_ff::Field;
use ministark::challenges::Challenges;
use ministark::constraints::AlgebraicItem;
use ministark::constraints::Constraint;
use ministark::constraints::ExecutionTraceColumn;
use ministark::constraints::Hint;
use ministark::constraints::VerifierChallenge;
use ministark::expression::Expr;
use ministark::hints::Hints;
use ministark::utils::FieldVariant;
use num_bigint::BigUint;
use num_traits::Pow;
use strum_macros::EnumIter;
const PEDERSEN_POINT_X: PeriodicColumn<'static, FieldVariant<Fp, Fp>> = {
const INTERVAL_SIZE: usize = super::PEDERSEN_BUILTIN_RATIO * super::CYCLE_HEIGHT;
const COEFFS: [FieldVariant<Fp, Fp>; 512] =
map_into_fp_array(pedersen::periodic::HASH_POINTS_X_COEFFS);
PeriodicColumn::new(&COEFFS, INTERVAL_SIZE)
};
const PEDERSEN_POINT_Y: PeriodicColumn<'static, FieldVariant<Fp, Fp>> = {
const INTERVAL_SIZE: usize = super::PEDERSEN_BUILTIN_RATIO * super::CYCLE_HEIGHT;
const COEFFS: [FieldVariant<Fp, Fp>; 512] =
map_into_fp_array(pedersen::periodic::HASH_POINTS_Y_COEFFS);
PeriodicColumn::new(&COEFFS, INTERVAL_SIZE)
};
const ECDSA_GENERATOR_POINT_X: PeriodicColumn<'static, FieldVariant<Fp, Fp>> = {
const INTERVAL_SIZE: usize = super::ECDSA_BUILTIN_RATIO * super::CYCLE_HEIGHT;
const COEFFS: [FieldVariant<Fp, Fp>; 256] =
map_into_fp_array(ecdsa::periodic::GENERATOR_POINTS_X_COEFFS);
PeriodicColumn::new(&COEFFS, INTERVAL_SIZE)
};
const ECDSA_GENERATOR_POINT_Y: PeriodicColumn<'static, FieldVariant<Fp, Fp>> = {
const INTERVAL_SIZE: usize = super::ECDSA_BUILTIN_RATIO * super::CYCLE_HEIGHT;
const COEFFS: [FieldVariant<Fp, Fp>; 256] =
map_into_fp_array(ecdsa::periodic::GENERATOR_POINTS_Y_COEFFS);
PeriodicColumn::new(&COEFFS, INTERVAL_SIZE)
};
const POSEIDON_POSEIDON_FULL_ROUND_KEY0: PeriodicColumn<'static, FieldVariant<Fp, Fp>> = {
const INTERVAL_SIZE: usize = super::POSEIDON_RATIO * super::CYCLE_HEIGHT;
const COEFFS: [FieldVariant<Fp, Fp>; 8] =
map_into_fp_array(poseidon::periodic::FULL_ROUND_KEY_0_COEFFS);
PeriodicColumn::new(&COEFFS, INTERVAL_SIZE)
};
const POSEIDON_POSEIDON_FULL_ROUND_KEY1: PeriodicColumn<'static, FieldVariant<Fp, Fp>> = {
const INTERVAL_SIZE: usize = super::POSEIDON_RATIO * super::CYCLE_HEIGHT;
const COEFFS: [FieldVariant<Fp, Fp>; 8] =
map_into_fp_array(poseidon::periodic::FULL_ROUND_KEY_1_COEFFS);
PeriodicColumn::new(&COEFFS, INTERVAL_SIZE)
};
const POSEIDON_POSEIDON_FULL_ROUND_KEY2: PeriodicColumn<'static, FieldVariant<Fp, Fp>> = {
const INTERVAL_SIZE: usize = super::POSEIDON_RATIO * super::CYCLE_HEIGHT;
const COEFFS: [FieldVariant<Fp, Fp>; 8] =
map_into_fp_array(poseidon::periodic::FULL_ROUND_KEY_2_COEFFS);
PeriodicColumn::new(&COEFFS, INTERVAL_SIZE)
};
const POSEIDON_POSEIDON_PARTIAL_ROUND_KEY0: PeriodicColumn<'static, FieldVariant<Fp, Fp>> = {
const INTERVAL_SIZE: usize = super::POSEIDON_RATIO * super::CYCLE_HEIGHT;
const COEFFS: [FieldVariant<Fp, Fp>; 64] =
map_into_fp_array(poseidon::periodic::PARTIAL_ROUND_KEY_0_COEFFS);
PeriodicColumn::new(&COEFFS, INTERVAL_SIZE)
};
const POSEIDON_POSEIDON_PARTIAL_ROUND_KEY1: PeriodicColumn<'static, FieldVariant<Fp, Fp>> = {
const INTERVAL_SIZE: usize = super::POSEIDON_RATIO * super::CYCLE_HEIGHT;
const COEFFS: [FieldVariant<Fp, Fp>; 32] =
map_into_fp_array(poseidon::periodic::PARTIAL_ROUND_KEY_1_COEFFS);
PeriodicColumn::new(&COEFFS, INTERVAL_SIZE)
};
pub struct AirConfig;
impl ministark::air::AirConfig for AirConfig {
const NUM_BASE_COLUMNS: usize = 9;
const NUM_EXTENSION_COLUMNS: usize = 1;
type Fp = Fp;
type Fq = Fp;
type PublicInputs = AirPublicInput<Fp>;
fn constraints(trace_len: usize) -> Vec<Constraint<FieldVariant<Fp, Fp>>> {
use AlgebraicItem::*;
use PublicInputHint::*;
// TODO: figure out why this value
let n = trace_len;
let trace_domain = Radix2EvaluationDomain::<Fp>::new(n).unwrap();
let g = trace_domain.group_gen();
assert!(n >= CYCLE_HEIGHT, "must be a multiple of cycle height");
// TODO: might be good to have more trace size assertions for builtins etc.
// for example ECDSA requires a minimum trace size of 2048 for this layout.
// NOTE: All this stuff is taken care by the runner of if you run properly
// i.e correct params
let x = Expr::from(X);
let one = Expr::from(Constant(FieldVariant::Fp(Fp::ONE)));
let two = Expr::from(Constant(FieldVariant::Fp(Fp::from(2u32))));
let four = Expr::from(Constant(FieldVariant::Fp(Fp::from(4u32))));
let offset_size = Expr::from(Constant(FieldVariant::Fp(Fp::from(2u32.pow(16)))));
let half_offset_size = Expr::from(Constant(FieldVariant::Fp(Fp::from(2u32.pow(15)))));
// cpu/decode/flag_op1_base_op0_0
let cpu_decode_flag_op1_base_op0_0 =
&one - (Flag::Op1Imm.curr() + Flag::Op1Ap.curr() + Flag::Op1Fp.curr());
// cpu/decode/flag_res_op1_0
let cpu_decode_flag_res_op1_0 =
&one - (Flag::ResAdd.curr() + Flag::ResMul.curr() + Flag::PcJnz.curr());
// cpu/decode/flag_pc_update_regular_0
let cpu_decode_flag_pc_update_regular_0 =
&one - (Flag::PcJumpAbs.curr() + Flag::PcJumpRel.curr() + Flag::PcJnz.curr());
// cpu/decode/fp_update_regular_0
let cpu_decode_fp_update_regular_0 =
&one - (Flag::OpcodeCall.curr() + Flag::OpcodeRet.curr());
// NOTE: npc_reg_0 = pc + instruction_size
// NOTE: instruction_size = fOP1_IMM + 1
let npc_reg_0 = Npc::Pc.curr() + Flag::Op1Imm.curr() + &one;
let memory_address_diff_0 = Mem::Address.next() - Mem::Address.curr();
let rc16_diff_0 = RangeCheck::Ordered.next() - RangeCheck::Ordered.curr();
// TODO: builtins
let pedersen_hash0_ec_subset_sum_b0 =
Pedersen::Suffix.curr() - (Pedersen::Suffix.next() + Pedersen::Suffix.next());
let pedersen_hash0_ec_subset_sum_b0_negate = &one - &pedersen_hash0_ec_subset_sum_b0;
let rc_builtin_value0_0 = RangeCheckBuiltin::Rc16Component.offset(0);
let rc_builtin_value1_0 =
&rc_builtin_value0_0 * &offset_size + RangeCheckBuiltin::Rc16Component.offset(1);
let rc_builtin_value2_0 =
&rc_builtin_value1_0 * &offset_size + RangeCheckBuiltin::Rc16Component.offset(2);
let rc_builtin_value3_0 =
&rc_builtin_value2_0 * &offset_size + RangeCheckBuiltin::Rc16Component.offset(3);
let rc_builtin_value4_0 =
&rc_builtin_value3_0 * &offset_size + RangeCheckBuiltin::Rc16Component.offset(4);
let rc_builtin_value5_0 =
&rc_builtin_value4_0 * &offset_size + RangeCheckBuiltin::Rc16Component.offset(5);
let rc_builtin_value6_0 =
&rc_builtin_value5_0 * &offset_size + RangeCheckBuiltin::Rc16Component.offset(6);
let rc_builtin_value7_0 =
&rc_builtin_value6_0 * &offset_size + RangeCheckBuiltin::Rc16Component.offset(7);
let ecdsa_sig0_doubling_key_x_squared =
Ecdsa::PubkeyDoublingX.curr() * Ecdsa::PubkeyDoublingX.curr();
let ecdsa_sig0_exponentiate_generator_b0 = Ecdsa::MessageSuffix.curr()
- (Ecdsa::MessageSuffix.next() + Ecdsa::MessageSuffix.next());
let ecdsa_sig0_exponentiate_generator_b0_neg = &one - &ecdsa_sig0_exponentiate_generator_b0;
let ecdsa_sig0_exponentiate_key_b0 =
Ecdsa::RSuffix.curr() - (Ecdsa::RSuffix.next() + Ecdsa::RSuffix.next());
let ecdsa_sig0_exponentiate_key_b0_neg = &one - &ecdsa_sig0_exponentiate_key_b0;
// bits 0->127 (inclusive) of a bitwise number
let bitwise_sum_var_0_0 = Bitwise::Bits16Chunk0Offset0.curr()
+ Bitwise::Bits16Chunk0Offset1.curr() * (&two).pow(1)
+ Bitwise::Bits16Chunk0Offset2.curr() * (&two).pow(2)
+ Bitwise::Bits16Chunk0Offset3.curr() * (&two).pow(3)
+ Bitwise::Bits16Chunk1Offset0.curr() * (&two).pow(64)
+ Bitwise::Bits16Chunk1Offset1.curr() * (&two).pow(65)
+ Bitwise::Bits16Chunk1Offset2.curr() * (&two).pow(66)
+ Bitwise::Bits16Chunk1Offset3.curr() * (&two).pow(67);
// bits 128->255 (inclusive) of a bitwise number
let bitwise_sum_var_8_0 = Bitwise::Bits16Chunk2Offset0.curr() * (&two).pow(128)
+ Bitwise::Bits16Chunk2Offset1.curr() * (&two).pow(129)
+ Bitwise::Bits16Chunk2Offset2.curr() * (&two).pow(130)
+ Bitwise::Bits16Chunk2Offset3.curr() * (&two).pow(131)
+ Bitwise::Bits16Chunk3Offset0.curr() * (&two).pow(192)
+ Bitwise::Bits16Chunk3Offset1.curr() * (&two).pow(193)
+ Bitwise::Bits16Chunk3Offset2.curr() * (&two).pow(194)
+ Bitwise::Bits16Chunk3Offset3.curr() * (&two).pow(195);
let ec_op_doubling_q_x_squared_0 = EcOp::QDoublingX.curr() * EcOp::QDoublingX.curr();
let ec_op_ec_subset_sum_bit_0 =
EcOp::MSuffix.curr() - (EcOp::MSuffix.next() + EcOp::MSuffix.next());
let ec_op_ec_subset_sum_bit_0_neg = &one - &ec_op_ec_subset_sum_bit_0;
let poseidon_poseidon_full_rounds_state0_cubed_0 =
Poseidon::FullRoundsState0.offset(0) * Poseidon::FullRoundsState0Squared.offset(0);
let poseidon_poseidon_full_rounds_state1_cubed_0 =
Poseidon::FullRoundsState1.offset(0) * Poseidon::FullRoundsState1Squared.offset(0);
let poseidon_poseidon_full_rounds_state2_cubed_0 =
Poseidon::FullRoundsState2.offset(0) * Poseidon::FullRoundsState2Squared.offset(0);
let poseidon_poseidon_full_rounds_state0_cubed_7 =
Poseidon::FullRoundsState0.offset(7) * Poseidon::FullRoundsState0Squared.offset(7);
let poseidon_poseidon_full_rounds_state1_cubed_7 =
Poseidon::FullRoundsState1.offset(7) * Poseidon::FullRoundsState1Squared.offset(7);
let poseidon_poseidon_full_rounds_state2_cubed_7 =
Poseidon::FullRoundsState2.offset(7) * Poseidon::FullRoundsState2Squared.offset(7);
let poseidon_poseidon_full_rounds_state0_cubed_3 =
Poseidon::FullRoundsState0.offset(3) * Poseidon::FullRoundsState0Squared.offset(3);
let poseidon_poseidon_full_rounds_state1_cubed_3 =
Poseidon::FullRoundsState1.offset(3) * Poseidon::FullRoundsState1Squared.offset(3);
let poseidon_poseidon_full_rounds_state2_cubed_3 =
Poseidon::FullRoundsState2.offset(3) * Poseidon::FullRoundsState2Squared.offset(3);
let poseidon_poseidon_partial_rounds_state0_cubed_0 = Poseidon::PartialRoundsState0
.offset(0)
* Poseidon::PartialRoundsState0Squared.offset(0);
let poseidon_poseidon_partial_rounds_state0_cubed_1 = Poseidon::PartialRoundsState0
.offset(1)
* Poseidon::PartialRoundsState0Squared.offset(1);
let poseidon_poseidon_partial_rounds_state0_cubed_2 = Poseidon::PartialRoundsState0
.offset(2)
* Poseidon::PartialRoundsState0Squared.offset(2);
let poseidon_poseidon_partial_rounds_state1_cubed_0 = Poseidon::PartialRoundsState1
.offset(0)
* Poseidon::PartialRoundsState1Squared.offset(0);
let poseidon_poseidon_partial_rounds_state1_cubed_1 = Poseidon::PartialRoundsState1
.offset(1)
* Poseidon::PartialRoundsState1Squared.offset(1);
let poseidon_poseidon_partial_rounds_state1_cubed_2 = Poseidon::PartialRoundsState1
.offset(2)
* Poseidon::PartialRoundsState1Squared.offset(2);
let poseidon_poseidon_partial_rounds_state1_cubed_19 = Poseidon::PartialRoundsState1
.offset(19)
* Poseidon::PartialRoundsState1Squared.offset(19);
let poseidon_poseidon_partial_rounds_state1_cubed_20 = Poseidon::PartialRoundsState1
.offset(20)
* Poseidon::PartialRoundsState1Squared.offset(20);
let poseidon_poseidon_partial_rounds_state1_cubed_21 = Poseidon::PartialRoundsState1
.offset(21)
* Poseidon::PartialRoundsState1Squared.offset(21);
// example for trace length n=64
// =============================
// x^(n/16) = (x - ω_0)(x - ω_16)(x - ω_32)(x - ω_48)
// x^(n/16) - c = (x - c*ω_0)(x - c*ω_16)(x - c*ω_32)(x - c*ω_48)
// x^(n/16) - ω^(n/16) = (x - ω_1)(x - ω_17)(x - ω_33)(x - )
// x^(n/16) - ω^(n/16)^(15) = (x - ω_15)(x - ω_31)(x - ω_47)(x - ω_6ω_493)
let flag0_offset =
FieldVariant::Fp(g.pow([(Flag::Zero as usize * n / CYCLE_HEIGHT) as u64]));
let flag0_zerofier = X.pow(n / CYCLE_HEIGHT) - Constant(flag0_offset);
let every_row_zerofier = X.pow(n) - &one;
let every_row_zerofier_inv = &one / every_row_zerofier;
let flags_zerofier_inv = &flag0_zerofier * &every_row_zerofier_inv;
// check decoded flag values are 0 or 1
// NOTE: This expression is a bit confusing. The zerofier forces this constraint
// to apply in all rows of the trace therefore it applies to all flags (not just
// DstReg). Funnily enough any flag here would work (it just wouldn't be SHARP
// compatible).
let cpu_decode_opcode_rc_b =
(Flag::DstReg.curr() * Flag::DstReg.curr() - Flag::DstReg.curr()) * &flags_zerofier_inv;
// The first word of each instruction:
// ┌─────────────────────────────────────────────────────────────────────────┐
// │ off_dst (biased representation) │
// ├─────────────────────────────────────────────────────────────────────────┤
// │ off_op0 (biased representation) │
// ├─────────────────────────────────────────────────────────────────────────┤
// │ off_op1 (biased representation) │
// ├─────┬─────┬───────┬───────┬───────────┬────────┬───────────────────┬────┤
// │ dst │ op0 │ op1 │ res │ pc │ ap │ opcode │ 0 │
// │ reg │ reg │ src │ logic │ update │ update │ │ │
// ├─────┼─────┼───┬───┼───┬───┼───┬───┬───┼───┬────┼────┬────┬────┬────┼────┤
// │ 0 │ 1 │ 2 │ 3 │ 4 │ 5 │ 6 │ 7 │ 8 │ 9 │ 10 │ 11 │ 12 │ 13 │ 14 │ 15 │
// └─────┴─────┴───┴───┴───┴───┴───┴───┴───┴───┴────┴────┴────┴────┴────┴────┘
let whole_flag_prefix = Expr::from(Trace(0, 0));
// NOTE: Forces the `0` flag prefix to =0 in every cycle.
let cpu_decode_opcode_rc_zero = &whole_flag_prefix / flag0_zerofier;
// force constraint to apply every 16 trace rows (every cairo cycle)
// e.g. (x - ω_0)(x - ω_16)(x - ω_32)(x - ω_48) for n=64
let all_cycles_zerofier = X.pow(n / CYCLE_HEIGHT) - &one;
let all_cycles_zerofier_inv = &one / all_cycles_zerofier;
let cpu_decode_opcode_rc_input = (Npc::Instruction.curr()
- (((&whole_flag_prefix * &offset_size + RangeCheck::OffOp1.curr()) * &offset_size
+ RangeCheck::OffOp0.curr())
* &offset_size
+ RangeCheck::OffDst.curr()))
* &all_cycles_zerofier_inv;
// constraint for the Op1Src flag group - forces vals 000, 100, 010 or 001
let cpu_decode_flag_op1_base_op0_bit = (&cpu_decode_flag_op1_base_op0_0
* &cpu_decode_flag_op1_base_op0_0
- &cpu_decode_flag_op1_base_op0_0)
* &all_cycles_zerofier_inv;
// forces only one or none of ResAdd, ResMul or PcJnz to be 1
// TODO: Why the F is PcJnz in here? Res flag group is only bit 5 and 6
// NOTE: looks like it's a handy optimization to calculate next_fp and next_ap
let cpu_decode_flag_res_op1_bit = (&cpu_decode_flag_res_op1_0 * &cpu_decode_flag_res_op1_0
- &cpu_decode_flag_res_op1_0)
* &all_cycles_zerofier_inv;
// constraint forces PcUpdate flag to be 000, 100, 010 or 001
let cpu_decode_flag_pc_update_regular_bit = (&cpu_decode_flag_pc_update_regular_0
* &cpu_decode_flag_pc_update_regular_0
- &cpu_decode_flag_pc_update_regular_0)
* &all_cycles_zerofier_inv;
// forces max only OpcodeRet or OpcodeAssertEq to be 1
// TODO: why OpcodeCall not included? that would make whole flag group
let cpu_decode_fp_update_regular_bit = (&cpu_decode_fp_update_regular_0
* &cpu_decode_fp_update_regular_0
- &cpu_decode_fp_update_regular_0)
* &all_cycles_zerofier_inv;
// cpu/operands/mem_dst_addr
// NOTE: Pseudo code from cairo whitepaper
// ```
// if dst_reg == 0:
// dst = m(ap + offdst)
// else:
// dst = m(fp + offdst)
// ```
// NOTE: Trace(5, 8) dest mem address
let cpu_operands_mem_dst_addr = (Npc::MemDstAddr.curr() + &half_offset_size
- (Flag::DstReg.curr() * Auxiliary::Fp.curr()
+ (&one - Flag::DstReg.curr()) * Auxiliary::Ap.curr()
+ RangeCheck::OffDst.curr()))
* &all_cycles_zerofier_inv;
// whitepaper pseudocode
// ```
// # Compute op0.
// if op0_reg == 0:
// op0 = m(-->>ap + offop0<<--)
// else:
// op0 = m(-->>fp + offop0<<--)
// ```
// NOTE: StarkEx contracts as: cpu_operands_mem0_addr
let cpu_operands_mem_op0_addr = (Npc::MemOp0Addr.curr() + &half_offset_size
- (Flag::Op0Reg.curr() * Auxiliary::Fp.curr()
+ (&one - Flag::Op0Reg.curr()) * Auxiliary::Ap.curr()
+ RangeCheck::OffOp0.curr()))
* &all_cycles_zerofier_inv;
// NOTE: StarkEx contracts as: cpu_operands_mem1_addr
let cpu_operands_mem_op1_addr = (Npc::MemOp1Addr.curr() + &half_offset_size
- (Flag::Op1Imm.curr() * Npc::Pc.curr()
+ Flag::Op1Ap.curr() * Auxiliary::Ap.curr()
+ Flag::Op1Fp.curr() * Auxiliary::Fp.curr()
+ &cpu_decode_flag_op1_base_op0_0 * Npc::MemOp0.curr()
+ RangeCheck::OffOp1.curr()))
* &all_cycles_zerofier_inv;
// op1 * op0
// NOTE: starkex cpu/operands/ops_mul
let cpu_operands_ops_mul = (Auxiliary::Op0MulOp1.curr()
- Npc::MemOp0.curr() * Npc::MemOp1.curr())
* &all_cycles_zerofier_inv;
// From cairo whitepaper
// ```
// # Compute res.
// if pc_update == 4:
// if res_logic == 0 && opcode == 0 && ap_update != 1:
// res = Unused
// else:
// Undefined Behavior
// else if pc_update = 0, 1 or 2:
// switch res_logic:
// case 0: res = op1
// case 1: res = op0 + op1
// case 2: res = op0 * op1
// default: Undefined Behavior
// else: Undefined Behavior
// ```
// NOTE: this constraint only handles:
// ```
// else if pc_update = 0, 1 or 2:
// switch res_logic:
// case 0: res = op1
// case 1: res = op0 + op1
// case 2: res = op0 * op1
// ```
let cpu_operands_res = ((&one - Flag::PcJnz.curr()) * Auxiliary::Res.curr()
- (Flag::ResAdd.curr() * (Npc::MemOp0.curr() + Npc::MemOp1.curr())
+ Flag::ResMul.curr() * Auxiliary::Op0MulOp1.curr()
+ &cpu_decode_flag_res_op1_0 * Npc::MemOp1.curr()))
* &all_cycles_zerofier_inv;
// example for trace length n=64
// =============================
// all_cycles_zerofier = (x - ω_0)(x - ω_16)(x - ω_32)(x - ω_48)
// X - ω^(16*(n/16 - 1)) = x - ω^n/w^16 = x - 1/w_16 = x - w_48
// (X - w_48) / all_cycles_zerofier = (x - ω_0)(x - ω_16)(x - ω_32)
let last_cycle_zerofier = X - Constant(FieldVariant::Fp(
g.pow([(CYCLE_HEIGHT * (n / CYCLE_HEIGHT - 1)) as u64]),
));
let last_cycle_zerofier_inv = &one / &last_cycle_zerofier;
let all_cycles_except_last_zerofier_inv = &last_cycle_zerofier * &all_cycles_zerofier_inv;
// Updating the program counter
// ============================
// This is not as straight forward as the other constraints. Read section 9.5
// Updating pc to understand.
// from whitepaper `t0 = fPC_JNZ * dst`
let cpu_update_registers_update_pc_tmp0 = (Auxiliary::Tmp0.curr()
- Flag::PcJnz.curr() * Npc::MemDst.curr())
* &all_cycles_except_last_zerofier_inv;
// From the whitepaper "To verify that we make a regular update if dst = 0, we
// need an auxiliary variable, v (to fill the trace in the case dst != 0, set v
// = dst^(−1)): `fPC_JNZ * (dst * v − 1) * (next_pc − (pc + instruction_size)) =
// 0` NOTE: if fPC_JNZ=1 then `res` is "unused" and repurposed as our
// temporary variable `v`. The value assigned to v is `dst^(−1)`.
// NOTE: `t1 = t0 * v`
let cpu_update_registers_update_pc_tmp1 = (Auxiliary::Tmp1.curr()
- Auxiliary::Tmp0.curr() * Auxiliary::Res.curr())
* &all_cycles_except_last_zerofier_inv;
// There are two constraints here bundled in one. The first is `t0 * (next_pc −
// (pc + op1)) = 0` (ensures if dst != 0 a relative jump is made) and the second
// is `(1−fPC_JNZ) * next_pc - (regular_update * (pc + instruction_size) +
// fPC_JUMP_ABS * res + fPC_JUMP_REL * (pc + res)) = 0` (handles update except
// for jnz). Note that due to the flag group constraints for PcUpdate if jnz=1
// then the second constraint is trivially 0=0 and if jnz=0 then the first
// constraint is trivially 0=0. For this reason we can bundle these constraints
// into one.
// TODO: fix padding bug
let cpu_update_registers_update_pc_pc_cond_negative = ((&one - Flag::PcJnz.curr())
* Npc::Pc.next()
+ Auxiliary::Tmp0.curr() * (Npc::Pc.next() - (Npc::Pc.curr() + Npc::MemOp1.curr()))
- (&cpu_decode_flag_pc_update_regular_0 * &npc_reg_0
+ Flag::PcJumpAbs.curr() * Auxiliary::Res.curr()
+ Flag::PcJumpRel.curr() * (Npc::Pc.curr() + Auxiliary::Res.curr())))
* &all_cycles_except_last_zerofier_inv;
// ensure `if dst == 0: pc + instruction_size == next_pc`
let cpu_update_registers_update_pc_pc_cond_positive =
((Auxiliary::Tmp1.curr() - Flag::PcJnz.curr()) * (Npc::Pc.next() - npc_reg_0))
* &all_cycles_except_last_zerofier_inv;
// Updating the allocation pointer
// ===============================
// TODO: seems fishy don't see how `next_ap = ap + fAP_ADD · res + fAP_ADD1 · 1
// + fOPCODE_CALL · 2` meets the pseudo code in the whitepaper
// Ok, it does kinda make sense. move the `opcode == 1` statement inside and
// move the switch to the outside and it's more clear.
let cpu_update_registers_update_ap_ap_update = (Auxiliary::Ap.next()
- (Auxiliary::Ap.curr()
+ Flag::ApAdd.curr() * Auxiliary::Res.curr()
+ Flag::ApAdd1.curr()
+ Flag::OpcodeCall.curr() * &two))
* &all_cycles_except_last_zerofier_inv;
// Updating the frame pointer
// ==========================
// This handles all fp update except the `op0 == pc + instruction_size`, `res =
// dst` and `dst == fp` assertions.
// TODO: fix padding bug
let cpu_update_registers_update_fp_fp_update = (Auxiliary::Fp.next()
- (&cpu_decode_fp_update_regular_0 * Auxiliary::Fp.curr()
+ Flag::OpcodeRet.curr() * Npc::MemDst.curr()
+ Flag::OpcodeCall.curr() * (Auxiliary::Ap.curr() + &two)))
* &all_cycles_except_last_zerofier_inv;
// push registers to memory (see section 8.4 in the whitepaper).
// These are essentially the assertions for assert `op0 == pc +
// instruction_size` and `assert dst == fp`.
let cpu_opcodes_call_push_fp = (Flag::OpcodeCall.curr()
* (Npc::MemDst.curr() - Auxiliary::Fp.curr()))
* &all_cycles_zerofier_inv;
let cpu_opcodes_call_push_pc = (Flag::OpcodeCall.curr()
* (Npc::MemOp0.curr() - (Npc::Pc.curr() + Flag::Op1Imm.curr() + &one)))
* &all_cycles_zerofier_inv;
// make sure all offsets are valid for the call opcode
// ===================================================
// checks `if opcode == OpcodeCall: assert off_dst = 2^15`
// this is supplementary to the constraints above because
// offsets are in the range [-2^15, 2^15) encoded using
// biased representation
let cpu_opcodes_call_off0 = (Flag::OpcodeCall.curr()
* (RangeCheck::OffDst.curr() - &half_offset_size))
* &all_cycles_zerofier_inv;
// checks `if opcode == OpcodeCall: assert off_op0 = 2^15 + 1`
// TODO: why +1?
let cpu_opcodes_call_off1 = (Flag::OpcodeCall.curr()
* (RangeCheck::OffOp0.curr() - (&half_offset_size + &one)))
* &all_cycles_zerofier_inv;
// TODO: I don't understand this one - Flag::OpcodeCall.curr() is 0 or 1. Why
// not just replace `Flag::OpcodeCall.curr() + Flag::OpcodeCall.curr() +
// &one + &one` with `4`
let cpu_opcodes_call_flags = (Flag::OpcodeCall.curr()
* (Flag::OpcodeCall.curr() + Flag::OpcodeCall.curr() + &one + &one
- (Flag::DstReg.curr() + Flag::Op0Reg.curr() + &four)))
* &all_cycles_zerofier_inv;
// checks `if opcode == OpcodeRet: assert off_dst = 2^15 - 2`
// TODO: why -2 🤯? Instruction size?
let cpu_opcodes_ret_off0 = (Flag::OpcodeRet.curr()
* (RangeCheck::OffDst.curr() + &two - &half_offset_size))
* &all_cycles_zerofier_inv;
// checks `if opcode == OpcodeRet: assert off_op1 = 2^15 - 1`
// TODO: why -1?
let cpu_opcodes_ret_off2 = (Flag::OpcodeRet.curr()
* (RangeCheck::OffOp1.curr() + &one - &half_offset_size))
* &all_cycles_zerofier_inv;
// checks `if OpcodeRet: assert PcJumpAbs=1, DstReg=1, Op1Fp=1, ResLogic=0`
let cpu_opcodes_ret_flags = (Flag::OpcodeRet.curr()
* (Flag::PcJumpAbs.curr()
+ Flag::DstReg.curr()
+ Flag::Op1Fp.curr()
+ &cpu_decode_flag_res_op1_0
- &four))
* &all_cycles_zerofier_inv;
// handles the "assert equal" instruction. Represents this pseudo code from the
// whitepaper `assert res = dst`.
let cpu_opcodes_assert_eq_assert_eq = (Flag::OpcodeAssertEq.curr()
* (Npc::MemDst.curr() - Auxiliary::Res.curr()))
* &all_cycles_zerofier_inv;
let first_row_zerofier = &x - &one;
let first_row_zerofier_inv = &one / first_row_zerofier;
// boundary constraint expression for initial registers
let initial_ap = (Auxiliary::Ap.curr() - InitialAp.hint()) * &first_row_zerofier_inv;
let initial_fp = (Auxiliary::Fp.curr() - InitialAp.hint()) * &first_row_zerofier_inv;
let initial_pc = (Npc::Pc.curr() - InitialPc.hint()) * &first_row_zerofier_inv;
// boundary constraint expression for final registers
let final_ap = (Auxiliary::Ap.curr() - FinalAp.hint()) * &last_cycle_zerofier_inv;
let final_fp = (Auxiliary::Fp.curr() - InitialAp.hint()) * &last_cycle_zerofier_inv;
let final_pc = (Npc::Pc.curr() - FinalPc.hint()) * &last_cycle_zerofier_inv;
// examples for trace length n=8
// =============================
// x^(n/2) - 1 = (x - ω_0)(x - ω_2)(x - ω_4)(x - ω_6)
// x - ω^(2*(n/2 - 1)) = x - ω^n/w^2 = x - 1/w_2 = x - w_6
// (x - w_6) / x^(n/2) - 1 = (x - ω_0)(x - ω_2)(x - ω_4)
let every_second_row_zerofier = X.pow(n / 2) - &one;
let second_last_row_zerofier =
X - Constant(FieldVariant::Fp(g.pow([2 * (n as u64 / 2 - 1)])));
let every_second_row_except_last_zerofier_inv =
&second_last_row_zerofier / &every_second_row_zerofier;
// Memory access constraints
// =========================
// All these constraints make more sense once you understand how the permutation
// column is calculated (look at get_ordered_memory_accesses()). Sections 9.8
// and 9.7 of the Cairo paper justify these constraints.
// memory permutation boundary constraint
let memory_multi_column_perm_perm_init0 = ((MemoryPermutation::Z.challenge()
- (Mem::Address.curr() + MemoryPermutation::A.challenge() * Mem::Value.curr()))
* Permutation::Memory.curr()
+ Npc::Pc.curr()
+ MemoryPermutation::A.challenge() * Npc::Instruction.curr()
- MemoryPermutation::Z.challenge())
* &first_row_zerofier_inv;
// memory permutation transition constraint
// NOTE: memory entries are stacked in the trace like so:
// ┌─────┬───────────┬─────┐
// │ ... │ ... │ ... │
// ├─────┼───────────┼─────┤
// │ ... │ address 0 │ ... │
// ├─────┼───────────┼─────┤
// │ ... │ value 0 │ ... │
// ├─────┼───────────┼─────┤
// │ ... │ address 1 │ ... │
// ├─────┼───────────┼─────┤
// │ ... │ value 1 │ ... │
// ├─────┼───────────┼─────┤
// │ ... │ ... │ ... │
// └─────┴───────────┴─────┘
let memory_multi_column_perm_perm_step0 = ((MemoryPermutation::Z.challenge()
- (Mem::Address.next() + MemoryPermutation::A.challenge() * Mem::Value.next()))
* Permutation::Memory.next()
- (MemoryPermutation::Z.challenge()
- (Npc::PubMemAddr.curr()
+ MemoryPermutation::A.challenge() * Npc::PubMemVal.curr()))
* Permutation::Memory.curr())
* &every_second_row_except_last_zerofier_inv;
// Check the last permutation value to verify public memory
let memory_multi_column_perm_perm_last =
(Permutation::Memory.curr() - MemoryQuotient.hint()) / &second_last_row_zerofier;
// Constraint expression for memory/diff_is_bit
// checks the address doesn't change or increases by 1
// "Continuity" constraint in cairo whitepaper 9.7.2
let memory_diff_is_bit = (&memory_address_diff_0 * &memory_address_diff_0
- &memory_address_diff_0)
* &every_second_row_except_last_zerofier_inv;
// if the address stays the same then the value stays the same
// "Single-valued" constraint in cairo whitepaper 9.7.2.
// cairo uses nondeterministic read-only memory so if the address is the same
// the value should also stay the same.
let memory_is_func = ((&memory_address_diff_0 - &one)
* (Mem::Value.curr() - Mem::Value.next()))
* &every_second_row_except_last_zerofier_inv;
// boundary condition stating the first memory address == 1
let memory_initial_addr = (Mem::Address.curr() - &one) * &first_row_zerofier_inv;
// applies every 8 rows
let every_eighth_row_zerofier = X.pow(n / 8) - &one;
let every_eighth_row_zerofier_inv = &one / &every_eighth_row_zerofier;
// Read cairo whitepaper section 9.8 as to why the public memory cells are 0.
// The high level is that the way public memory works is that the prover is
// forced (with these constraints) to exclude the public memory from one of
// the permutation products. This means the running permutation column
// terminates with more-or-less the permutation of just the public input. The
// verifier can relatively cheaply calculate this terminal. The constraint for
// this terminal is `memory_multi_column_perm_perm_last`.
let public_memory_addr_zero = Npc::PubMemAddr.curr() * &every_eighth_row_zerofier_inv;
let public_memory_value_zero = Npc::PubMemVal.curr() * &every_eighth_row_zerofier_inv;
// examples for trace length n=16
// =====================================
// x^(n/4) - 1 = (x - ω_0)(x - ω_4)(x - ω_8)(x - ω_12)
// x - ω^(4*(n/4 - 1)) = x - ω^n/w^4 = x - 1/w_4 = x - w_12
// (x - w_12) / x^(n/4) - 1 = (x - ω_0)(x - ω_4)(x - ω_8)
let every_fourth_row_zerofier_inv = &one / (X.pow(n / 4) - &one);
let fourth_last_row_zerofier =
X - Constant(FieldVariant::Fp(g.pow([4 * (n as u64 / 4 - 1)])));
let every_fourth_row_except_last_zerofier_inv =
&fourth_last_row_zerofier * &every_fourth_row_zerofier_inv;
// Range check constraints
// =======================
// Look at memory to understand the general approach to permutation.
// More info in section 9.9 of the Cairo paper.
let rc16_perm_init0 = ((RangeCheckPermutation::Z.challenge() - RangeCheck::Ordered.curr())
* Permutation::RangeCheck.curr()
+ RangeCheck::OffDst.curr()
- RangeCheckPermutation::Z.challenge())
* &first_row_zerofier_inv;
let rc16_perm_step0 = ((RangeCheckPermutation::Z.challenge() - RangeCheck::Ordered.next())
* Permutation::RangeCheck.next()
- (RangeCheckPermutation::Z.challenge() - RangeCheck::OffOp1.curr())
* Permutation::RangeCheck.curr())
* &every_fourth_row_except_last_zerofier_inv;
let rc16_perm_last =
(Permutation::RangeCheck.curr() - RangeCheckProduct.hint()) / &fourth_last_row_zerofier;
// Check the value increases by 0 or 1
let rc16_diff_is_bit = (&rc16_diff_0 * &rc16_diff_0 - &rc16_diff_0)
* &every_fourth_row_except_last_zerofier_inv;
// Prover sends the minimim and maximum as a public input.
// Verifier checks the RC min and max fall within [0, 2^16).
let rc16_minimum =
(RangeCheck::Ordered.curr() - RangeCheckMin.hint()) * &first_row_zerofier_inv;
let rc16_maximum =
(RangeCheck::Ordered.curr() - RangeCheckMax.hint()) / &fourth_last_row_zerofier;
// Diluted Check constraints
// =========================
// A "dilution" is spreading out of the bits in a number.
// Dilutions have two parameters (1) the number of bits they operate on and
// (2) the spread of each bit. For example the the dilution of binary
// digit 1111 to 0001000100010001 operates on 4 bits with a spread of 4.
let diluted_check_permutation_init0 = ((DilutedCheckPermutation::Z.challenge()
- DilutedCheck::Ordered.curr())
* Permutation::DilutedCheck.curr()
+ DilutedCheck::Unordered.curr()
- DilutedCheckPermutation::Z.challenge())
* &first_row_zerofier_inv;
// Diluted checks operate every 8 rows (twice per cycle)
let zerofier_8th_last_row = X - Constant(FieldVariant::Fp(g.pow([8 * (n as u64 / 8 - 1)])));
let zerofier_8th_last_row_inv = &one / &zerofier_8th_last_row;
let every_8_row_zerofier = X.pow(n / 8) - &one;
let every_8_row_zerofier_inv = &one / &every_8_row_zerofier;
let every_8_rows_except_last_zerofier_inv =
&zerofier_8th_last_row * &every_8_row_zerofier_inv;
// we have an out-of-order and in-order list of diluted values for this layout
// (starknet). We want to check each list is a permutation of one another
let diluted_check_permutation_step0 = ((DilutedCheckPermutation::Z.challenge()
- DilutedCheck::Ordered.next())
* Permutation::DilutedCheck.next()
- (DilutedCheckPermutation::Z.challenge() - DilutedCheck::Unordered.next())
* Permutation::DilutedCheck.curr())
* &every_8_rows_except_last_zerofier_inv;
let diluted_check_permutation_last = (Permutation::DilutedCheck.curr()
- DilutedCheckProduct.hint())
* &zerofier_8th_last_row_inv;
// Initial aggregate value should be =1
let diluted_check_init = (DilutedCheck::Aggregate.curr() - &one) * &first_row_zerofier_inv;
// Check first, in-order, diluted value
let diluted_check_first_element =
(DilutedCheck::Ordered.curr() - DilutedCheckFirst.hint()) * &first_row_zerofier_inv;
// TODO: add more docs
// `diluted_diff` is related to `u` in `compute_diluted_cumulative_value`
// Note that if there is no difference between the current and next ordered
// diluted values then `diluted_diff == 0` and the previous aggregate value is
// copied over
let diluted_diff = DilutedCheck::Ordered.next() - DilutedCheck::Ordered.curr();
let diluted_check_step = (DilutedCheck::Aggregate.next()
- (DilutedCheck::Aggregate.curr()
* (&one + DilutedCheckAggregation::Z.challenge() * &diluted_diff)
+ DilutedCheckAggregation::A.challenge() * &diluted_diff * diluted_diff))
* &every_8_rows_except_last_zerofier_inv;
// Check the last cumulative value.
// NOTE: This can be calculated efficiently by the verifier.
let diluted_check_last = (DilutedCheck::Aggregate.curr()
- DilutedCheckCumulativeValue.hint())
* &zerofier_8th_last_row_inv;
// Pedersen builtin
// ================
// Each hash spans across 256 rows - that's one hash per 16 cairo steps.
let every_256_row_zerofier_inv = &one / (X.pow(n / 256) - &one);
// These first few pedersen constraints check that the number is in the range
// ```text
// 100000000000000000000000000000000000000000000000000000010001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001
// ^ ^ ^
// 251 196 191
// ```
// Use knowledge of bits 251,196,192 to determine if there is a unique unpacking
let pedersen_hash0_ec_subset_sub_bit_unpacking_last_one_is_zero =
(Pedersen::Bit251AndBit196AndBit192.curr()
* (Pedersen::Suffix.curr() - (Pedersen::Suffix.next() + Pedersen::Suffix.next())))
* &every_256_row_zerofier_inv;
let shift191 = Constant(FieldVariant::Fp(Fp::from(BigUint::from(2u32).pow(191u32))));
let pedersen_hash0_ec_subset_sub_bit_unpacking_zeros_between_ones =
(Pedersen::Bit251AndBit196AndBit192.curr()
* (Pedersen::Suffix.offset(1) - Pedersen::Suffix.offset(192) * shift191))
* &every_256_row_zerofier_inv;
let pedersen_hash0_ec_subset_sum_bit_unpacking_cumulative_bit192 =
(Pedersen::Bit251AndBit196AndBit192.curr()
- Pedersen::Bit251AndBit196.curr()
* (Pedersen::Suffix.offset(192)
- (Pedersen::Suffix.offset(193) + Pedersen::Suffix.offset(193))))
* &every_256_row_zerofier_inv;
let shift3 = Constant(FieldVariant::Fp(Fp::from(BigUint::from(2u32).pow(3u32))));
let pedersen_hash0_ec_subset_sum_bit_unpacking_zeroes_between_ones192 =
(Pedersen::Bit251AndBit196.curr()
* (Pedersen::Suffix.offset(193) - Pedersen::Suffix.offset(196) * shift3))
* &every_256_row_zerofier_inv;
let pedersen_hash0_ec_subset_sum_bit_unpacking_cumulative_bit196 =
(Pedersen::Bit251AndBit196.curr()
- (Pedersen::Suffix.offset(251)
- (Pedersen::Suffix.offset(252) + Pedersen::Suffix.offset(252)))
* (Pedersen::Suffix.offset(196)
- (Pedersen::Suffix.offset(197) + Pedersen::Suffix.offset(197))))
* &every_256_row_zerofier_inv;
// TODO: docs
let shift54 = Constant(FieldVariant::Fp(Fp::from(BigUint::from(2u32).pow(54u32))));
let pedersen_hash0_ec_subset_sum_bit_unpacking_zeroes_between_ones196 = ((Pedersen::Suffix
.offset(251)
- (Pedersen::Suffix.offset(252) + Pedersen::Suffix.offset(252)))
* (Pedersen::Suffix.offset(197) - Pedersen::Suffix.offset(251) * shift54))
* &every_256_row_zerofier_inv;
// example for trace length n=512
// =============================
// x^(n/256) - ω^(255*n/256) = (x-ω^255)(x-ω^511)
// (x-ω^255)(x-ω^511) / (X^n-1) = 1/(x-ω^0)..(x-ω^254)(x-ω^256)..(x-ω^510)
// vanishes on groups of 256 consecutive rows except the last row in each group
// TODO: come up with better names for these
let pedersen_transition_zerofier_inv = (X.pow(n / 256)
- Constant(FieldVariant::Fp(g.pow([(255 * n / 256) as u64]))))
* &every_row_zerofier_inv;
// Constraint operated on groups of 256 rows.
// Each row shifts a large number to the right. E.g.
// ```text
// row0: 10101...10001 <- constraint applied
// row1: 1010...11000 <- constraint applied
// ... ... <- constraint applied
// row255: 0 <- constraint disabled
// row256: 11101...10001 <- constraint applied
// row257: 1110...01000 <- constraint applied
// ... ... <- constraint applied
// row511: 0 <- constraint disabled
// ... ...
// ```
let pedersen_hash0_ec_subset_sum_booleanity_test = (&pedersen_hash0_ec_subset_sum_b0
* (&pedersen_hash0_ec_subset_sum_b0 - &one))
* &pedersen_transition_zerofier_inv;
// example for trace length n=512
// =============================
// x^(n/256) - ω^(63*n/64) = x^(n/256) - ω^(252*n/256)
// x^(n/256) - ω^(255*n/256) = (x-ω^252)(x-ω^508)
// (x-ω^255)(x-ω^511) / (X^n-1) = 1/(x-ω^0)..(x-ω^254)(x-ω^256)..(x-ω^510)
// vanishes on the 252nd row of every 256 rows
let pedersen_zero_suffix_zerofier_inv =
&one / (X.pow(n / 256) - Constant(FieldVariant::Fp(g.pow([(63 * n / 64) as u64]))));
// Note that with cairo's default field each element is 252 bits.
// Therefore we are decomposing 252 bit numbers to do pedersen hash.
// Since we have a column that right shifts a number each row we check that the
// suffix of row 252 (of every 256 row group) equals 0 e.g.
// ```text
// row0: 10101...10001
// row1: 1010...11000
// ... ...
// row250: 10
// row251: 1
// row252: 0 <- check zero
// row253: 0
// row254: 0
// row255: 0
// row256: 11101...10001
// row257: 1110...01000
// ... ...
// row506: 11
// row507: 1
// row508: 0 <- check zero
// row509: 0
// ... ...
// ```
// <https://docs.starkware.co/starkex/crypto/pedersen-hash-function.html>
let pedersen_hash0_ec_subset_sum_bit_extraction_end =
Pedersen::Suffix.curr() * &pedersen_zero_suffix_zerofier_inv;
// TODO: is this constraint even needed?
// check suffix in row 255 of each 256 row group is zero
let pedersen_hash0_ec_subset_sum_zeros_tail = Pedersen::Suffix.curr()
* (&one / (X.pow(n / 256) - Constant(FieldVariant::Fp(g.pow([255 * n as u64 / 256])))));
// Create a periodic table comprising of the constant Pedersen points we need to
// add together. The columns of this table are represented by polynomials that
// evaluate to the `i`th row when evaluated on the `i`th power of the 512th root
// of unity. e.g.
//
// let:
// - `[P]_x` denotes the x-coordinate of an elliptic-curve point P
// - P_1, P_2, P_3, P_4 be fixed elliptic curve points that parameterize the
// Pedersen hash function
//
// then our point table is:
// ┌───────────┬────────────────────┬────────────────────┐
// │ X │ F_x(X) │ F_y(X) │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^0 │ [P_1 * 2^0]_x │ [P_1 * 2^0]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^1 │ [P_1 * 2^1]_x │ [P_1 * 2^1]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ... │ ... │ ... │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^247 │ [P_1 * 2^247]_x │ [P_1 * 2^247]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^248 │ [P_2 * 2^0]_x │ [P_2 * 2^0]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^249 │ [P_2 * 2^1]_x │ [P_2 * 2^1]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^250 │ [P_2 * 2^2]_x │ [P_2 * 2^2]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^251 │ [P_2 * 2^3]_x │ [P_2 * 2^3]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^252 │ [P_2 * 2^3]_x │ [P_2 * 2^3]_y │<- unused copy of prev
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^253 │ [P_2 * 2^3]_x │ [P_2 * 2^3]_y │<- unused copy of prev
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^254 │ [P_2 * 2^3]_x │ [P_2 * 2^3]_y │<- unused copy of prev
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^255 │ [P_2 * 2^3]_x │ [P_2 * 2^3]_y │<- unused copy of prev
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^256 │ [P_3 * 2^0]_x │ [P_3 * 2^0]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^257 │ [P_3 * 2^1]_x │ [P_3 * 2^1]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ... │ ... │ ... │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^503 │ [P_3 * 2^247]_x │ [P_3 * 2^247]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^504 │ [P_4 * 2^0]_x │ [P_4 * 2^0]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^505 │ [P_4 * 2^1]_x │ [P_4 * 2^1]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^506 │ [P_4 * 2^2]_x │ [P_4 * 2^2]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^507 │ [P_4 * 2^3]_x │ [P_4 * 2^3]_y │
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^508 │ [P_4 * 2^3]_x │ [P_4 * 2^3]_y │<- unused copy of prev
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^509 │ [P_4 * 2^3]_x │ [P_4 * 2^3]_y │<- unused copy of prev
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^510 │ [P_4 * 2^3]_x │ [P_4 * 2^3]_y │<- unused copy of prev
// ├───────────┼────────────────────┼────────────────────┤
// │ ω^511 │ [P_4 * 2^3]_x │ [P_4 * 2^3]_y │<- unused copy of prev
// └───────────┴────────────────────┴────────────────────┘
let pedersen_point_x = Expr::from(Periodic(PEDERSEN_POINT_X));
let pedersen_point_y = Expr::from(Periodic(PEDERSEN_POINT_Y));
// let `P = (Px, Py)` be the point to be added (see above)
// let `Q = (Qx, Qy)` be the partial result
// note that the slope = dy/dx with dy = Qy - Py, dx = Qx - Px
// this constraint is equivalent to: bit * dy = dy/dx * dx
// NOTE: slope is 0 if bit is 0
let pedersen_hash0_ec_subset_sum_add_points_slope = (&pedersen_hash0_ec_subset_sum_b0
* (Pedersen::PartialSumY.curr() - &pedersen_point_y)
- Pedersen::Slope.curr() * (Pedersen::PartialSumX.curr() - &pedersen_point_x))
* &pedersen_transition_zerofier_inv;
// These two constraint check classic short Weierstrass curve point addition.
// Constraint is equivalent to:
// - `Qx_next = m^2 - Qx - Px, m = dy/dx`
// - `Qy_next = m*(Qx - Qx_next) - Qy, m = dy/dx`
let pedersen_hash0_ec_subset_sum_add_points_x = (Pedersen::Slope.curr()
* Pedersen::Slope.curr()
- &pedersen_hash0_ec_subset_sum_b0
* (Pedersen::PartialSumX.curr()
+ &pedersen_point_x
+ Pedersen::PartialSumX.next()))
* &pedersen_transition_zerofier_inv;
let pedersen_hash0_ec_subset_sum_add_points_y = (&pedersen_hash0_ec_subset_sum_b0
* (Pedersen::PartialSumY.curr() + Pedersen::PartialSumY.next())
- Pedersen::Slope.curr()
* (Pedersen::PartialSumX.curr() - Pedersen::PartialSumX.next()))
* &pedersen_transition_zerofier_inv;
// if the bit is 0 then just copy the previous point
let pedersen_hash0_ec_subset_sum_copy_point_x = (&pedersen_hash0_ec_subset_sum_b0_negate
* (Pedersen::PartialSumX.next() - Pedersen::PartialSumX.curr()))
* &pedersen_transition_zerofier_inv;
let pedersen_hash0_ec_subset_sum_copy_point_y = (&pedersen_hash0_ec_subset_sum_b0_negate
* (Pedersen::PartialSumY.next() - Pedersen::PartialSumY.curr()))
* &pedersen_transition_zerofier_inv;
// example for trace length n=1024
// =============================
// x^(n/512) - ω^(n/2) = x^(n/512) - ω^(256*n/512)
// x^(n/512) - ω^(256*n/512) = (x-ω^256)(x-ω^768)
// x^(n/256) - 1 = (x-ω_0)(x-ω_256)(x-ω_512)(x-ω_768)
// (x-ω^256)(x-ω^768) / (x^(n/256)-1) = 1/(x-ω_0)(x-ω_512)
// 1/(x^(n/512) - 1) = 1/(x-ω_0)(x-ω_512)
// NOTE: By using `(x-ω^256)(x-ω^768) / (x^(n/256)-1)` rather than
// `1/(x^(n/512) - 1)` we save an inversion operation since 1 / (x^(n/256)-1)
// has been calculated already and as a result of how constraints are
// evaluated it will be cached.
// TODO: check all zerofiers are being multiplied or divided correctly
let every_512_row_zerofier_inv = (X.pow(n / 512)
- Constant(FieldVariant::Fp(g.pow([n as u64 / 2]))))
* &every_256_row_zerofier_inv;
// A single pedersen hash `H(a, b)` is computed every 512 cycles.
// The constraints for each hash is split in two consecutive 256 row groups.
// - 1st group computes `e0 = P0 + a_low * P1 + a_high * P2`
// - 2nd group computes `e1 = e0 + B_low * P3 + B_high * P4`
// We make sure the initial value of each group is loaded correctly:
// - 1st group we check P0 (the shift point) is the first partial sum
// - 2nd group we check e0 (processed `a`) is the first partial sum
let pedersen_hash0_copy_point_x = (Pedersen::PartialSumX.offset(256)
- Pedersen::PartialSumX.offset(255))
* &every_512_row_zerofier_inv;
let pedersen_hash0_copy_point_y = (Pedersen::PartialSumY.offset(256)
- Pedersen::PartialSumY.offset(255))
* &every_512_row_zerofier_inv;
// TODO: introducing a new zerofier that's equivalent to the
// previous one? double check every_512_row_zerofier
let every_512_row_zerofier = X.pow(n / 512) - Constant(FieldVariant::Fp(Fp::ONE));
let every_512_row_zerofier_inv = &one / &every_512_row_zerofier;
let shift_point = pedersen::constants::P0;
let pedersen_hash0_init_x = (Pedersen::PartialSumX.curr()
- Constant(FieldVariant::Fp(shift_point.x)))
* &every_512_row_zerofier_inv;
let pedersen_hash0_init_y = (Pedersen::PartialSumY.curr()
- Constant(FieldVariant::Fp(shift_point.y)))
* &every_512_row_zerofier_inv;
// TODO: fix naming
let zerofier_512th_last_row =
X - Constant(FieldVariant::Fp(g.pow([512 * (n as u64 / 512 - 1)])));
let every_512_rows_except_last_zerofier =
&zerofier_512th_last_row * &every_512_row_zerofier_inv;
// Link Input0 into the memory pool.
let pedersen_input0_value0 =
(Npc::PedersenInput0Val.curr() - Pedersen::Suffix.curr()) * &every_512_row_zerofier_inv;
// Input0's next address should be the address directly
// after the output address of the previous hash
let pedersen_input0_addr = (Npc::PedersenInput0Addr.next()
- (Npc::PedersenOutputAddr.curr() + &one))
* &every_512_rows_except_last_zerofier;
// Ensure the first pedersen address matches the hint
let pedersen_init_addr =
(Npc::PedersenInput0Addr.curr() - InitialPedersenAddr.hint()) * &first_row_zerofier_inv;
// Link Input1 into the memory pool.
// Input1's address should be the address directly after input0's address
let pedersen_input1_value0 = (Npc::PedersenInput1Val.curr() - Pedersen::Suffix.offset(256))
* &every_512_row_zerofier_inv;
let pedersen_input1_addr = (Npc::PedersenInput1Addr.curr()
- (Npc::PedersenInput0Addr.curr() + &one))