Skip to content

Commit fb18534

Browse files
committed
air audit fix 5- remove condition from decode small sigh
1 parent 86f49af commit fb18534

File tree

19 files changed

+144
-84
lines changed

19 files changed

+144
-84
lines changed

stwo_cairo_prover/crates/cairo-air/src/components/subroutines/cond_felt_252_as_rel_imm.rs

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
// This file was created by the AIR team.
22

33
use crate::components::prelude::*;
4-
use crate::components::subroutines::cond_decode_small_sign::CondDecodeSmallSign;
54
use crate::components::subroutines::cond_range_check_2::CondRangeCheck2;
5+
use crate::components::subroutines::decode_small_sign::DecodeSmallSign;
66

77
#[derive(Copy, Clone, Serialize, Deserialize, CairoSerialize)]
88
pub struct CondFelt252AsRelImm {}
@@ -30,12 +30,7 @@ impl CondFelt252AsRelImm {
3030
let M31_512 = E::F::from(M31::from(512));
3131
let M31_536870912 = E::F::from(M31::from(536870912));
3232

33-
CondDecodeSmallSign::evaluate(
34-
[cond_felt_252_as_rel_imm_input_limb_28.clone()],
35-
msb_col0.clone(),
36-
mid_limbs_set_col1.clone(),
37-
eval,
38-
);
33+
DecodeSmallSign::evaluate([], msb_col0.clone(), mid_limbs_set_col1.clone(), eval);
3934
let remainder_bits_tmp_1e9bf_3 = eval.add_intermediate(
4035
(cond_felt_252_as_rel_imm_input_limb_3.clone()
4136
- (mid_limbs_set_col1.clone() * M31_508.clone())),
Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
// This file was created by the AIR team.
2+
3+
use crate::components::prelude::*;
4+
5+
#[derive(Copy, Clone, Serialize, Deserialize, CairoSerialize)]
6+
pub struct DecodeSmallSign {}
7+
8+
impl DecodeSmallSign {
9+
#[allow(unused_parens)]
10+
#[allow(clippy::double_parens)]
11+
#[allow(non_snake_case)]
12+
#[allow(clippy::unused_unit)]
13+
#[allow(unused_variables)]
14+
#[allow(clippy::too_many_arguments)]
15+
pub fn evaluate<E: EvalAtRow>(
16+
[]: [E::F; 0],
17+
msb_col0: E::F,
18+
mid_limbs_set_col1: E::F,
19+
eval: &mut E,
20+
) -> [E::F; 0] {
21+
let M31_1 = E::F::from(M31::from(1));
22+
23+
// msb is a bit.
24+
eval.add_constraint((msb_col0.clone() * (msb_col0.clone() - M31_1.clone())));
25+
// mid_limbs_set is a bit.
26+
eval.add_constraint(
27+
(mid_limbs_set_col1.clone() * (mid_limbs_set_col1.clone() - M31_1.clone())),
28+
);
29+
// Cannot have msb equals 0 and mid_limbs_set equals 1.
30+
eval.add_constraint((mid_limbs_set_col1.clone() * (msb_col0.clone() - M31_1.clone())));
31+
[]
32+
}
33+
}

stwo_cairo_prover/crates/cairo-air/src/components/subroutines/mod.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ pub mod bitwise_xor_num_bits_7;
55
pub mod bitwise_xor_num_bits_8;
66
pub mod bitwise_xor_num_bits_8_b;
77
pub mod bitwise_xor_num_bits_9;
8-
pub mod cond_decode_small_sign;
98
pub mod cond_felt_252_as_addr;
109
pub mod cond_felt_252_as_rel_imm;
1110
pub mod cond_range_check_2;
@@ -30,6 +29,7 @@ pub mod decode_instruction_de75a;
3029
pub mod decode_instruction_df7a6;
3130
pub mod decode_instruction_f1edd;
3231
pub mod decode_instruction_fe864;
32+
pub mod decode_small_sign;
3333
pub mod div_252;
3434
pub mod double_karatsuba_n_7_limb_max_bound_511;
3535
pub mod double_karatsuba_n_8_limb_max_bound_4095;

stwo_cairo_prover/crates/cairo-air/src/components/subroutines/read_small.rs

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
// This file was created by the AIR team.
22

33
use crate::components::prelude::*;
4-
use crate::components::subroutines::cond_decode_small_sign::CondDecodeSmallSign;
54
use crate::components::subroutines::cond_range_check_2::CondRangeCheck2;
5+
use crate::components::subroutines::decode_small_sign::DecodeSmallSign;
66
use crate::components::subroutines::read_id::ReadId;
77

88
#[derive(Copy, Clone, Serialize, Deserialize, CairoSerialize)]
@@ -46,12 +46,7 @@ impl ReadSmall {
4646
memory_address_to_id_lookup_elements,
4747
eval,
4848
);
49-
CondDecodeSmallSign::evaluate(
50-
[M31_1.clone()],
51-
msb_col1.clone(),
52-
mid_limbs_set_col2.clone(),
53-
eval,
54-
);
49+
DecodeSmallSign::evaluate([], msb_col1.clone(), mid_limbs_set_col2.clone(), eval);
5550
CondRangeCheck2::evaluate(
5651
[remainder_bits_col6.clone(), M31_1.clone()],
5752
partial_limb_msb_col7.clone(),

stwo_cairo_prover/crates/common/casm_registry.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
{
2-
"air_version": "c68bb12a",
2+
"air_version": "13816ba5",
33
"air_fns": {
44
"memory_address_to_id": {
55
"trace_type": "Memory",

stwo_cairo_prover/crates/prover/src/witness/components/add_ap_opcode.rs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -282,16 +282,17 @@ fn write_trace_simd(
282282
let memory_id_to_big_value_tmp_c921e_9 =
283283
memory_id_to_big_state.deduce_output(op1_id_col7);
284284

285-
// Cond Decode Small Sign.
285+
// Decode Small Sign.
286286

287287
let msb_tmp_c921e_10 = memory_id_to_big_value_tmp_c921e_9.get_m31(27).eq(M31_256);
288288
let msb_col8 = msb_tmp_c921e_10.as_m31();
289289
*row[8] = msb_col8;
290290
let mid_limbs_set_tmp_c921e_11 =
291-
memory_id_to_big_value_tmp_c921e_9.get_m31(20).eq(M31_511);
291+
((memory_id_to_big_value_tmp_c921e_9.get_m31(20).eq(M31_511))
292+
& (memory_id_to_big_value_tmp_c921e_9.get_m31(27).eq(M31_256)));
292293
let mid_limbs_set_col9 = mid_limbs_set_tmp_c921e_11.as_m31();
293294
*row[9] = mid_limbs_set_col9;
294-
let cond_decode_small_sign_output_tmp_c921e_12 = [msb_col8, mid_limbs_set_col9];
295+
let decode_small_sign_output_tmp_c921e_12 = [msb_col8, mid_limbs_set_col9];
295296

296297
let op1_limb_0_col10 = memory_id_to_big_value_tmp_c921e_9.get_m31(0);
297298
*row[10] = op1_limb_0_col10;

stwo_cairo_prover/crates/prover/src/witness/components/add_mod_builtin.rs

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1191,16 +1191,17 @@ fn write_trace_simd(
11911191
let memory_id_to_big_value_tmp_c1b19_74 =
11921192
memory_id_to_big_state.deduce_output(offsets_a_id_col84);
11931193

1194-
// Cond Decode Small Sign.
1194+
// Decode Small Sign.
11951195

11961196
let msb_tmp_c1b19_75 = memory_id_to_big_value_tmp_c1b19_74.get_m31(27).eq(M31_256);
11971197
let msb_col85 = msb_tmp_c1b19_75.as_m31();
11981198
*row[85] = msb_col85;
11991199
let mid_limbs_set_tmp_c1b19_76 =
1200-
memory_id_to_big_value_tmp_c1b19_74.get_m31(20).eq(M31_511);
1200+
((memory_id_to_big_value_tmp_c1b19_74.get_m31(20).eq(M31_511))
1201+
& (memory_id_to_big_value_tmp_c1b19_74.get_m31(27).eq(M31_256)));
12011202
let mid_limbs_set_col86 = mid_limbs_set_tmp_c1b19_76.as_m31();
12021203
*row[86] = mid_limbs_set_col86;
1203-
let cond_decode_small_sign_output_tmp_c1b19_77 = [msb_col85, mid_limbs_set_col86];
1204+
let decode_small_sign_output_tmp_c1b19_77 = [msb_col85, mid_limbs_set_col86];
12041205

12051206
let offsets_a_limb_0_col87 = memory_id_to_big_value_tmp_c1b19_74.get_m31(0);
12061207
*row[87] = offsets_a_limb_0_col87;
@@ -1278,16 +1279,17 @@ fn write_trace_simd(
12781279
let memory_id_to_big_value_tmp_c1b19_84 =
12791280
memory_id_to_big_state.deduce_output(offsets_b_id_col92);
12801281

1281-
// Cond Decode Small Sign.
1282+
// Decode Small Sign.
12821283

12831284
let msb_tmp_c1b19_85 = memory_id_to_big_value_tmp_c1b19_84.get_m31(27).eq(M31_256);
12841285
let msb_col93 = msb_tmp_c1b19_85.as_m31();
12851286
*row[93] = msb_col93;
12861287
let mid_limbs_set_tmp_c1b19_86 =
1287-
memory_id_to_big_value_tmp_c1b19_84.get_m31(20).eq(M31_511);
1288+
((memory_id_to_big_value_tmp_c1b19_84.get_m31(20).eq(M31_511))
1289+
& (memory_id_to_big_value_tmp_c1b19_84.get_m31(27).eq(M31_256)));
12881290
let mid_limbs_set_col94 = mid_limbs_set_tmp_c1b19_86.as_m31();
12891291
*row[94] = mid_limbs_set_col94;
1290-
let cond_decode_small_sign_output_tmp_c1b19_87 = [msb_col93, mid_limbs_set_col94];
1292+
let decode_small_sign_output_tmp_c1b19_87 = [msb_col93, mid_limbs_set_col94];
12911293

12921294
let offsets_b_limb_0_col95 = memory_id_to_big_value_tmp_c1b19_84.get_m31(0);
12931295
*row[95] = offsets_b_limb_0_col95;
@@ -1365,16 +1367,17 @@ fn write_trace_simd(
13651367
let memory_id_to_big_value_tmp_c1b19_94 =
13661368
memory_id_to_big_state.deduce_output(offsets_c_id_col100);
13671369

1368-
// Cond Decode Small Sign.
1370+
// Decode Small Sign.
13691371

13701372
let msb_tmp_c1b19_95 = memory_id_to_big_value_tmp_c1b19_94.get_m31(27).eq(M31_256);
13711373
let msb_col101 = msb_tmp_c1b19_95.as_m31();
13721374
*row[101] = msb_col101;
13731375
let mid_limbs_set_tmp_c1b19_96 =
1374-
memory_id_to_big_value_tmp_c1b19_94.get_m31(20).eq(M31_511);
1376+
((memory_id_to_big_value_tmp_c1b19_94.get_m31(20).eq(M31_511))
1377+
& (memory_id_to_big_value_tmp_c1b19_94.get_m31(27).eq(M31_256)));
13751378
let mid_limbs_set_col102 = mid_limbs_set_tmp_c1b19_96.as_m31();
13761379
*row[102] = mid_limbs_set_col102;
1377-
let cond_decode_small_sign_output_tmp_c1b19_97 = [msb_col101, mid_limbs_set_col102];
1380+
let decode_small_sign_output_tmp_c1b19_97 = [msb_col101, mid_limbs_set_col102];
13781381

13791382
let offsets_c_limb_0_col103 = memory_id_to_big_value_tmp_c1b19_94.get_m31(0);
13801383
*row[103] = offsets_c_limb_0_col103;

stwo_cairo_prover/crates/prover/src/witness/components/add_opcode_small.rs

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -323,16 +323,17 @@ fn write_trace_simd(
323323
let memory_id_to_big_value_tmp_756b7_14 =
324324
memory_id_to_big_state.deduce_output(dst_id_col14);
325325

326-
// Cond Decode Small Sign.
326+
// Decode Small Sign.
327327

328328
let msb_tmp_756b7_15 = memory_id_to_big_value_tmp_756b7_14.get_m31(27).eq(M31_256);
329329
let msb_col15 = msb_tmp_756b7_15.as_m31();
330330
*row[15] = msb_col15;
331331
let mid_limbs_set_tmp_756b7_16 =
332-
memory_id_to_big_value_tmp_756b7_14.get_m31(20).eq(M31_511);
332+
((memory_id_to_big_value_tmp_756b7_14.get_m31(20).eq(M31_511))
333+
& (memory_id_to_big_value_tmp_756b7_14.get_m31(27).eq(M31_256)));
333334
let mid_limbs_set_col16 = mid_limbs_set_tmp_756b7_16.as_m31();
334335
*row[16] = mid_limbs_set_col16;
335-
let cond_decode_small_sign_output_tmp_756b7_17 = [msb_col15, mid_limbs_set_col16];
336+
let decode_small_sign_output_tmp_756b7_17 = [msb_col15, mid_limbs_set_col16];
336337

337338
let dst_limb_0_col17 = memory_id_to_big_value_tmp_756b7_14.get_m31(0);
338339
*row[17] = dst_limb_0_col17;
@@ -414,16 +415,17 @@ fn write_trace_simd(
414415
let memory_id_to_big_value_tmp_756b7_24 =
415416
memory_id_to_big_state.deduce_output(op0_id_col22);
416417

417-
// Cond Decode Small Sign.
418+
// Decode Small Sign.
418419

419420
let msb_tmp_756b7_25 = memory_id_to_big_value_tmp_756b7_24.get_m31(27).eq(M31_256);
420421
let msb_col23 = msb_tmp_756b7_25.as_m31();
421422
*row[23] = msb_col23;
422423
let mid_limbs_set_tmp_756b7_26 =
423-
memory_id_to_big_value_tmp_756b7_24.get_m31(20).eq(M31_511);
424+
((memory_id_to_big_value_tmp_756b7_24.get_m31(20).eq(M31_511))
425+
& (memory_id_to_big_value_tmp_756b7_24.get_m31(27).eq(M31_256)));
424426
let mid_limbs_set_col24 = mid_limbs_set_tmp_756b7_26.as_m31();
425427
*row[24] = mid_limbs_set_col24;
426-
let cond_decode_small_sign_output_tmp_756b7_27 = [msb_col23, mid_limbs_set_col24];
428+
let decode_small_sign_output_tmp_756b7_27 = [msb_col23, mid_limbs_set_col24];
427429

428430
let op0_limb_0_col25 = memory_id_to_big_value_tmp_756b7_24.get_m31(0);
429431
*row[25] = op0_limb_0_col25;
@@ -505,16 +507,17 @@ fn write_trace_simd(
505507
let memory_id_to_big_value_tmp_756b7_34 =
506508
memory_id_to_big_state.deduce_output(op1_id_col30);
507509

508-
// Cond Decode Small Sign.
510+
// Decode Small Sign.
509511

510512
let msb_tmp_756b7_35 = memory_id_to_big_value_tmp_756b7_34.get_m31(27).eq(M31_256);
511513
let msb_col31 = msb_tmp_756b7_35.as_m31();
512514
*row[31] = msb_col31;
513515
let mid_limbs_set_tmp_756b7_36 =
514-
memory_id_to_big_value_tmp_756b7_34.get_m31(20).eq(M31_511);
516+
((memory_id_to_big_value_tmp_756b7_34.get_m31(20).eq(M31_511))
517+
& (memory_id_to_big_value_tmp_756b7_34.get_m31(27).eq(M31_256)));
515518
let mid_limbs_set_col32 = mid_limbs_set_tmp_756b7_36.as_m31();
516519
*row[32] = mid_limbs_set_col32;
517-
let cond_decode_small_sign_output_tmp_756b7_37 = [msb_col31, mid_limbs_set_col32];
520+
let decode_small_sign_output_tmp_756b7_37 = [msb_col31, mid_limbs_set_col32];
518521

519522
let op1_limb_0_col33 = memory_id_to_big_value_tmp_756b7_34.get_m31(0);
520523
*row[33] = op1_limb_0_col33;

stwo_cairo_prover/crates/prover/src/witness/components/call_opcode_rel_imm.rs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -393,16 +393,17 @@ fn write_trace_simd(
393393
let memory_id_to_big_value_tmp_9db06_19 =
394394
memory_id_to_big_state.deduce_output(distance_to_next_pc_id_col15);
395395

396-
// Cond Decode Small Sign.
396+
// Decode Small Sign.
397397

398398
let msb_tmp_9db06_20 = memory_id_to_big_value_tmp_9db06_19.get_m31(27).eq(M31_256);
399399
let msb_col16 = msb_tmp_9db06_20.as_m31();
400400
*row[16] = msb_col16;
401401
let mid_limbs_set_tmp_9db06_21 =
402-
memory_id_to_big_value_tmp_9db06_19.get_m31(20).eq(M31_511);
402+
((memory_id_to_big_value_tmp_9db06_19.get_m31(20).eq(M31_511))
403+
& (memory_id_to_big_value_tmp_9db06_19.get_m31(27).eq(M31_256)));
403404
let mid_limbs_set_col17 = mid_limbs_set_tmp_9db06_21.as_m31();
404405
*row[17] = mid_limbs_set_col17;
405-
let cond_decode_small_sign_output_tmp_9db06_22 = [msb_col16, mid_limbs_set_col17];
406+
let decode_small_sign_output_tmp_9db06_22 = [msb_col16, mid_limbs_set_col17];
406407

407408
let distance_to_next_pc_limb_0_col18 =
408409
memory_id_to_big_value_tmp_9db06_19.get_m31(0);

stwo_cairo_prover/crates/prover/src/witness/components/generic_opcode.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -708,11 +708,11 @@ verify_instruction_state: &verify_instruction::ClaimGenerator,
708708

709709
// Cond Felt 252 As Rel Imm.
710710

711-
// Cond Decode Small Sign.
711+
// Decode Small Sign.
712712

713713
let msb_tmp_57455_95 = res_limb_27_col224.eq(M31_256);let msb_col229 = msb_tmp_57455_95.as_m31();
714-
*row[229] = msb_col229;let mid_limbs_set_tmp_57455_96 = res_limb_20_col217.eq(M31_511);let mid_limbs_set_col230 = mid_limbs_set_tmp_57455_96.as_m31();
715-
*row[230] = mid_limbs_set_col230;let cond_decode_small_sign_output_tmp_57455_97 = [msb_col229, mid_limbs_set_col230];
714+
*row[229] = msb_col229;let mid_limbs_set_tmp_57455_96 = ((res_limb_20_col217.eq(M31_511)) & (res_limb_27_col224.eq(M31_256)));let mid_limbs_set_col230 = mid_limbs_set_tmp_57455_96.as_m31();
715+
*row[230] = mid_limbs_set_col230;let decode_small_sign_output_tmp_57455_97 = [msb_col229, mid_limbs_set_col230];
716716

717717
let remainder_bits_tmp_57455_98 = ((res_limb_3_col200) - (((mid_limbs_set_col230) * (M31_508))));
718718

@@ -730,11 +730,11 @@ verify_instruction_state: &verify_instruction::ClaimGenerator,
730730

731731
// Cond Felt 252 As Rel Imm.
732732

733-
// Cond Decode Small Sign.
733+
// Decode Small Sign.
734734

735735
let msb_tmp_57455_107 = op1_limb_27_col111.eq(M31_256);let msb_col235 = msb_tmp_57455_107.as_m31();
736-
*row[235] = msb_col235;let mid_limbs_set_tmp_57455_108 = op1_limb_20_col104.eq(M31_511);let mid_limbs_set_col236 = mid_limbs_set_tmp_57455_108.as_m31();
737-
*row[236] = mid_limbs_set_col236;let cond_decode_small_sign_output_tmp_57455_109 = [msb_col235, mid_limbs_set_col236];
736+
*row[235] = msb_col235;let mid_limbs_set_tmp_57455_108 = ((op1_limb_20_col104.eq(M31_511)) & (op1_limb_27_col111.eq(M31_256)));let mid_limbs_set_col236 = mid_limbs_set_tmp_57455_108.as_m31();
737+
*row[236] = mid_limbs_set_col236;let decode_small_sign_output_tmp_57455_109 = [msb_col235, mid_limbs_set_col236];
738738

739739
let remainder_bits_tmp_57455_110 = ((op1_limb_3_col87) - (((mid_limbs_set_col236) * (M31_508))));
740740

0 commit comments

Comments
 (0)