@@ -86,9 +86,9 @@ pub const BIT_FLAG_COLUMNS: &[usize] = &[
8686 cols:: ECALL ,
8787 cols:: EBREAK ,
8888 // Sign bits
89- cols:: RV1_SIGN_BIT ,
90- cols:: ARG2_SIGN_BIT ,
91- cols:: RES_SIGN_BIT ,
89+ cols:: RV1_EXT_BIT ,
90+ cols:: RV2_EXT_BIT ,
91+ cols:: RES_EXT_BIT ,
9292 // Computed flags
9393 cols:: IS_EQUAL ,
9494 cols:: BRANCH_COND ,
@@ -379,7 +379,7 @@ impl TransitionConstraint<GoldilocksField, GoldilocksExtension> for Arg1LowerCon
379379 }
380380}
381381
382- /// Constraint: arg1[4:8] = rv1[2] * (1 - word_instr) + (2^32 - 1) * rv1_sign_bit * signed
382+ /// Constraint: arg1[4:8] = rv1[2] * (1 - word_instr) + (2^32 - 1) * rv1_ext_bit * signed
383383///
384384/// Upper 32 bits of arg1 depends on word_instr and sign extension.
385385pub struct Arg1UpperConstraint {
@@ -406,15 +406,15 @@ impl Arg1UpperConstraint {
406406 . get_main_evaluation_element ( 0 , cols:: WORD_INSTR )
407407 . clone ( ) ;
408408 let signed = step. get_main_evaluation_element ( 0 , cols:: SIGNED ) . clone ( ) ;
409- let rv1_sign_bit = step
410- . get_main_evaluation_element ( 0 , cols:: RV1_SIGN_BIT )
409+ let rv1_ext_bit = step
410+ . get_main_evaluation_element ( 0 , cols:: RV1_EXT_BIT )
411411 . clone ( ) ;
412412
413413 let one = FieldElement :: < F > :: one ( ) ;
414414 let mask_32: FieldElement < F > = FieldElement :: from ( ( 1u64 << 32 ) - 1 ) ; // 2^32 - 1
415415
416- // Expected: rv1_upper * (1 - word_instr) + mask_32 * rv1_sign_bit * signed
417- let expected = rv1_upper * ( one - & word_instr) + mask_32 * rv1_sign_bit * signed;
416+ // Expected: rv1_upper * (1 - word_instr) + mask_32 * rv1_ext_bit * signed
417+ let expected = rv1_upper * ( one - & word_instr) + mask_32 * rv1_ext_bit * signed;
418418
419419 // Constraint: arg1_hi - expected = 0
420420 arg1_hi - expected
@@ -423,7 +423,7 @@ impl Arg1UpperConstraint {
423423
424424impl TransitionConstraint < GoldilocksField , GoldilocksExtension > for Arg1UpperConstraint {
425425 fn degree ( & self ) -> usize {
426- // rv1_sign_bit * signed * word_instr has degree 3
426+ // rv1_ext_bit * signed * word_instr has degree 3
427427 3
428428 }
429429
@@ -549,47 +549,47 @@ pub fn create_slt_res_zero_constraints(
549549}
550550
551551// =========================================================================
552- // Sign Bit Constraints
552+ // Extension Bit Constraints (SIGN template from spec)
553553// =========================================================================
554554
555- /// Constraint: sign bits are zero when word_instr = 0
555+ /// Constraint: ext_bit must be zero when word_instr = 0
556556///
557- /// (rv1_sign_bit + arg2_sign_bit + res_sign_bit) * (1 - word_instr) = 0
558- pub struct SignBitZeroConstraint {
557+ /// (1 - word_instr) * ext_bit = 0
558+ ///
559+ /// One instance per extension bit (rv1_ext_bit, rv2_ext_bit, res_ext_bit).
560+ pub struct ExtBitZeroConstraint {
559561 constraint_idx : usize ,
562+ ext_bit_col : usize ,
560563}
561564
562- impl SignBitZeroConstraint {
563- pub fn new ( constraint_idx : usize ) -> Self {
564- Self { constraint_idx }
565+ impl ExtBitZeroConstraint {
566+ pub fn new ( constraint_idx : usize , ext_bit_col : usize ) -> Self {
567+ Self {
568+ constraint_idx,
569+ ext_bit_col,
570+ }
565571 }
566572
567573 fn compute < F , E > ( & self , step : & TableView < F , E > ) -> FieldElement < F >
568574 where
569575 F : IsSubFieldOf < E > ,
570576 E : IsField ,
571577 {
572- let rv1_sign_bit = step
573- . get_main_evaluation_element ( 0 , cols:: RV1_SIGN_BIT )
574- . clone ( ) ;
575- let arg2_sign_bit = step
576- . get_main_evaluation_element ( 0 , cols:: ARG2_SIGN_BIT )
577- . clone ( ) ;
578- let res_sign_bit = step
579- . get_main_evaluation_element ( 0 , cols:: RES_SIGN_BIT )
578+ let ext_bit = step
579+ . get_main_evaluation_element ( 0 , self . ext_bit_col )
580580 . clone ( ) ;
581581 let word_instr = step
582582 . get_main_evaluation_element ( 0 , cols:: WORD_INSTR )
583583 . clone ( ) ;
584584
585585 let one = FieldElement :: < F > :: one ( ) ;
586586
587- // (sum of sign bits) * ( 1 - word_instr) = 0
588- ( rv1_sign_bit + arg2_sign_bit + res_sign_bit ) * ( one - word_instr)
587+ // (1 - word_instr) * ext_bit = 0
588+ ( one - word_instr) * ext_bit
589589 }
590590}
591591
592- impl TransitionConstraint < GoldilocksField , GoldilocksExtension > for SignBitZeroConstraint {
592+ impl TransitionConstraint < GoldilocksField , GoldilocksExtension > for ExtBitZeroConstraint {
593593 fn degree ( & self ) -> usize {
594594 2
595595 }
@@ -842,7 +842,7 @@ impl TransitionConstraint<GoldilocksField, GoldilocksExtension> for Arg2LowerCon
842842 }
843843}
844844
845- /// Constraint: arg2[4:] = (1-LOAD)*((1-word_instr)*rv2[2] + signed*arg2_sign_bit *(2^32-1)) + (1-BEQ-BLT-STORE)*imm[1]
845+ /// Constraint: arg2[4:] = (1-LOAD)*((1-word_instr)*rv2[2] + signed*rv2_ext_bit *(2^32-1)) + (1-BEQ-BLT-STORE)*imm[1]
846846///
847847/// arg2 upper 32 bits with sign extension logic.
848848pub struct Arg2UpperConstraint {
@@ -880,13 +880,13 @@ impl Arg2UpperConstraint {
880880 let blt = step. get_main_evaluation_element ( 0 , cols:: BLT ) ;
881881 let word_instr = step. get_main_evaluation_element ( 0 , cols:: WORD_INSTR ) ;
882882 let signed = step. get_main_evaluation_element ( 0 , cols:: SIGNED ) ;
883- let arg2_sign_bit = step. get_main_evaluation_element ( 0 , cols:: ARG2_SIGN_BIT ) ;
883+ let rv2_ext_bit = step. get_main_evaluation_element ( 0 , cols:: RV2_EXT_BIT ) ;
884884
885885 let one = FieldElement :: < F > :: one ( ) ;
886886 let mask_32: FieldElement < F > = FieldElement :: from ( ( 1u64 << 32 ) - 1 ) ;
887887
888- // rv2_term = (1 - word_instr) * rv2[2] + signed * arg2_sign_bit * (2^32 - 1)
889- let rv2_term = ( & one - word_instr) * rv2_upper + signed * arg2_sign_bit * & mask_32;
888+ // rv2_term = (1 - word_instr) * rv2[2] + signed * rv2_ext_bit * (2^32 - 1)
889+ let rv2_term = ( & one - word_instr) * rv2_upper + signed * rv2_ext_bit * & mask_32;
890890
891891 // expected = (1-LOAD) * rv2_term + (1-BEQ-BLT-STORE) * imm[1]
892892 // STORE now gets rv2_term (with sign extension), not imm
@@ -899,7 +899,7 @@ impl Arg2UpperConstraint {
899899
900900impl TransitionConstraint < GoldilocksField , GoldilocksExtension > for Arg2UpperConstraint {
901901 fn degree ( & self ) -> usize {
902- // (1-LOAD) * signed * arg2_sign_bit has degree 3
902+ // (1-LOAD) * signed * rv2_ext_bit has degree 3
903903 3
904904 }
905905
@@ -989,7 +989,7 @@ impl TransitionConstraint<GoldilocksField, GoldilocksExtension> for RvdLowerCons
989989 }
990990}
991991
992- /// Constraint: (1-LOAD) * (rvd[1] - ((1-word_instr)*res[4:] + res_sign_bit *(2^32-1))) = 0
992+ /// Constraint: (1-LOAD) * (rvd[1] - ((1-word_instr)*res[4:] + res_ext_bit *(2^32-1))) = 0
993993///
994994/// When not LOAD, rvd upper 32 bits equals res upper with sign extension.
995995/// For LOAD: rvd is the loaded value, not res (which is the address).
@@ -1016,13 +1016,13 @@ impl RvdUpperConstraint {
10161016
10171017 let load = step. get_main_evaluation_element ( 0 , cols:: LOAD ) ;
10181018 let word_instr = step. get_main_evaluation_element ( 0 , cols:: WORD_INSTR ) ;
1019- let res_sign_bit = step. get_main_evaluation_element ( 0 , cols:: RES_SIGN_BIT ) ;
1019+ let res_ext_bit = step. get_main_evaluation_element ( 0 , cols:: RES_EXT_BIT ) ;
10201020
10211021 let one = FieldElement :: < F > :: one ( ) ;
10221022 let mask_32: FieldElement < F > = FieldElement :: from ( ( 1u64 << 32 ) - 1 ) ;
10231023
1024- // expected = (1 - word_instr) * res_hi + res_sign_bit * (2^32 - 1)
1025- let expected = ( & one - word_instr) * res_hi + res_sign_bit * mask_32;
1024+ // expected = (1 - word_instr) * res_hi + res_ext_bit * (2^32 - 1)
1025+ let expected = ( & one - word_instr) * res_hi + res_ext_bit * mask_32;
10261026
10271027 // (1 - LOAD) * (rvd[1] - expected) = 0
10281028 ( one - load) * ( rvd_1 - expected)
@@ -1217,14 +1217,14 @@ pub fn create_jalr_constraints(constraint_idx_start: usize) -> (Vec<AddConstrain
12171217/// - Rvd lower: 1
12181218/// - Rvd upper: 1
12191219/// - SLT res zero: 7 (bytes 1-7)
1220- /// - Sign bit zero: 1
1220+ /// - Ext bit zero (SIGN template): 3 (rv1_ext_bit, rv2_ext_bit, res_ext_bit)
12211221/// - rv1 zero-forcing (CM48): 3 (rv1[0..2] when read_register1 = 0)
12221222/// - rv2 zero-forcing (CM50): 3 (rv2[0..2] when read_register2 = 0)
12231223/// - Next PC (non-branching): 2
12241224///
1225- /// Total: 64 constraints (32 IS_BIT + 8 ADD + 24 other)
1225+ /// Total: 66 constraints (32 IS_BIT + 8 ADD + 26 other)
12261226pub const NUM_CPU_CONSTRAINTS : usize =
1227- 32 + 2 + 2 + 2 + 2 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 7 + 1 + 3 + 3 + 2 ;
1227+ 32 + 2 + 2 + 2 + 2 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 7 + 3 + 3 + 3 + 2 ;
12281228
12291229/// Creates all CPU constraints.
12301230///
@@ -1313,8 +1313,21 @@ pub fn create_all_cpu_constraints() -> (
13131313 other. push ( Box :: new ( c) ) ;
13141314 }
13151315
1316- // Sign bit zero constraint
1317- other. push ( Box :: new ( SignBitZeroConstraint :: new ( next_idx) ) ) ;
1316+ // Extension bit zero constraints (SIGN template: !word_instr => ext_bit = 0)
1317+ other. push ( Box :: new ( ExtBitZeroConstraint :: new (
1318+ next_idx,
1319+ cols:: RV1_EXT_BIT ,
1320+ ) ) ) ;
1321+ next_idx += 1 ;
1322+ other. push ( Box :: new ( ExtBitZeroConstraint :: new (
1323+ next_idx,
1324+ cols:: RV2_EXT_BIT ,
1325+ ) ) ) ;
1326+ next_idx += 1 ;
1327+ other. push ( Box :: new ( ExtBitZeroConstraint :: new (
1328+ next_idx,
1329+ cols:: RES_EXT_BIT ,
1330+ ) ) ) ;
13181331 next_idx += 1 ;
13191332
13201333 // Next PC (non-branching) constraints
0 commit comments