chore(recursion): convert ext2felt to hint (#771)

succinctlabs · May 24, 2024 · 7ea90f9 · 7ea90f9
1 parent bc8b593
commit 7ea90f9
Show file tree

Hide file tree

Showing 9 changed files with 41 additions and 19 deletions.
diff --git a/recursion/compiler/src/asm/compiler.rs b/recursion/compiler/src/asm/compiler.rs
@@ -485,9 +485,9 @@ impl<F: PrimeField32 + TwoAdicField, EF: ExtensionField<F> + TwoAdicField> AsmCo
                 DslIr::PrintF(dst) => self.push(AsmInstruction::PrintF(dst.fp()), trace),
                 DslIr::PrintV(dst) => self.push(AsmInstruction::PrintV(dst.fp()), trace),
                 DslIr::PrintE(dst) => self.push(AsmInstruction::PrintE(dst.fp()), trace),
-                DslIr::Ext2Felt(dst, src) => match (dst, src) {
+                DslIr::HintExt2Felt(dst, src) => match (dst, src) {
                     (Array::Dyn(dst, _), src) => {
-                        self.push(AsmInstruction::Ext2Felt(dst.fp(), src.fp()), trace)
+                        self.push(AsmInstruction::HintExt2Felt(dst.fp(), src.fp()), trace)
                     }
                     _ => unimplemented!(),
                 },

diff --git a/recursion/compiler/src/asm/instruction.rs b/recursion/compiler/src/asm/instruction.rs
@@ -160,7 +160,7 @@ pub enum AsmInstruction<F, EF> {
     PrintE(i32),
 
     /// Convert an extension element to field elements.
-    Ext2Felt(i32, i32),
+    HintExt2Felt(i32, i32),
 
     /// Hint the lenght of the next vector of blocks.
     HintLen(i32),
@@ -786,8 +786,8 @@ impl<F: PrimeField32, EF: ExtensionField<F>> AsmInstruction<F, EF> {
                 false,
                 name,
             ),
-            AsmInstruction::Ext2Felt(dst, src) => Instruction::new(
-                Opcode::Ext2Felt,
+            AsmInstruction::HintExt2Felt(dst, src) => Instruction::new(
+                Opcode::HintExt2Felt,
                 i32_f(dst),
                 i32_f_arr(src),
                 f_u32(F::zero()),
@@ -1113,7 +1113,9 @@ impl<F: PrimeField32, EF: ExtensionField<F>> AsmInstruction<F, EF> {
             AsmInstruction::PrintE(dst) => {
                 write!(f, "print_e ({})fp", dst)
             }
-            AsmInstruction::Ext2Felt(dst, src) => write!(f, "ext2felt ({})fp, {})fp", dst, src),
+            AsmInstruction::HintExt2Felt(dst, src) => {
+                write!(f, "hintExt2felt ({})fp, {})fp", dst, src)
+            }
             AsmInstruction::HintLen(dst) => write!(f, "hint_len ({})fp", dst),
             AsmInstruction::Hint(dst) => write!(f, "hint ({})fp", dst),
             AsmInstruction::FriFold(m, input_ptr) => {

diff --git a/recursion/compiler/src/ir/instructions.rs b/recursion/compiler/src/ir/instructions.rs
@@ -146,7 +146,7 @@ pub enum DslIr<C: Config> {
     TwoAdicGenerator(Felt<C::F>, Usize<C::N>),
     ExpUsizeV(Var<C::N>, Var<C::N>, Usize<C::N>),
     ExpUsizeF(Felt<C::F>, Felt<C::F>, Usize<C::N>),
-    Ext2Felt(Array<C, Felt<C::F>>, Ext<C::F, C::EF>),
+    HintExt2Felt(Array<C, Felt<C::F>>, Ext<C::F, C::EF>),
     HintLen(Var<C::N>),
     HintVars(Array<C, Var<C::N>>),
     HintFelts(Array<C, Felt<C::F>>),

diff --git a/recursion/compiler/src/ir/utils.rs b/recursion/compiler/src/ir/utils.rs
@@ -202,7 +202,19 @@ impl<C: Config> Builder<C> {
     /// Converts an ext to a slice of felts.
     pub fn ext2felt(&mut self, value: Ext<C::F, C::EF>) -> Array<C, Felt<C::F>> {
         let result = self.dyn_array(4);
-        self.operations.push(DslIr::Ext2Felt(result.clone(), value));
+        self.operations
+            .push(DslIr::HintExt2Felt(result.clone(), value));
+
+        // Verify that the decomposed extension element is correct.
+        let mut reconstructed_ext: Ext<C::F, C::EF> = self.constant(C::EF::zero());
+        for i in 0..4 {
+            let felt = self.get(&result, i);
+            let monomial: Ext<C::F, C::EF> = self.constant(C::EF::monomial(i));
+            reconstructed_ext = self.eval(reconstructed_ext + monomial * felt);
+        }
+
+        self.assert_ext_eq(reconstructed_ext, value);
+
         result
     }
 

diff --git a/recursion/core/src/cpu/air/mod.rs b/recursion/core/src/cpu/air/mod.rs
@@ -183,6 +183,8 @@ impl<F: Field> CpuChip<F> {
             + local.selectors.is_fri_fold
             + local.selectors.is_poseidon
             + local.selectors.is_store
+            + local.selectors.is_noop
+            + local.selectors.is_ext_to_felt
     }
 
     /// Expr to check for instructions that are commit instructions.

diff --git a/recursion/core/src/cpu/columns/opcode.rs b/recursion/core/src/cpu/columns/opcode.rs
@@ -40,6 +40,7 @@ pub struct OpcodeSelectorCols<T> {
     pub is_poseidon: T,
     pub is_fri_fold: T,
     pub is_commit: T,
+    pub is_ext_to_felt: T,
 }
 
 impl<F: Field> OpcodeSelectorCols<F> {
@@ -65,14 +66,19 @@ impl<F: Field> OpcodeSelectorCols<F> {
             Opcode::HALT => self.is_halt = F::one(),
             Opcode::FRIFold => self.is_fri_fold = F::one(),
             Opcode::Poseidon2Compress => self.is_poseidon = F::one(),
-            // TODO: Double-check that `is_noop` is constrained properly in the CPU air.
-            Opcode::Ext2Felt => self.is_noop = F::one(),
-            Opcode::HintBits => self.is_noop = F::one(),
-            Opcode::PrintF => self.is_noop = F::one(),
-            Opcode::PrintE => self.is_noop = F::one(),
             Opcode::Commit => self.is_commit = F::one(),
-            Opcode::RegisterPublicValue => self.is_noop = F::one(),
-            _ => {}
+            Opcode::HintExt2Felt => self.is_ext_to_felt = F::one(),
+
+            Opcode::Hint
+            | Opcode::HintBits
+            | Opcode::PrintF
+            | Opcode::PrintE
+            | Opcode::RegisterPublicValue
+            | Opcode::CycleTracker => {
+                self.is_noop = F::one();
+            }
+
+            Opcode::HintLen | Opcode::LessThanF => {}
         }
 
         if matches!(
@@ -109,6 +115,7 @@ impl<T: Copy> IntoIterator for &OpcodeSelectorCols<T> {
             self.is_poseidon,
             self.is_fri_fold,
             self.is_commit,
+            self.is_ext_to_felt,
         ]
         .into_iter()
     }

diff --git a/recursion/core/src/runtime/mod.rs b/recursion/core/src/runtime/mod.rs
@@ -604,10 +604,9 @@ where
                     let (a_val, b_val, c_val) = self.all_rr(&instruction);
                     (a, b, c) = (a_val, b_val, c_val);
                 }
-                Opcode::Ext2Felt => {
+                Opcode::HintExt2Felt => {
                     let (a_val, b_val, c_val) = self.all_rr(&instruction);
                     let dst = a_val[0].as_canonical_u32() as usize;
-                    // TODO: this should be a hint and perhaps the compiler needs to change to make it a hint?
                     self.mw_uninitialized(dst, Block::from(b_val[0]));
                     self.mw_uninitialized(dst + 1, Block::from(b_val[1]));
                     self.mw_uninitialized(dst + 2, Block::from(b_val[2]));

diff --git a/recursion/core/src/runtime/opcode.rs b/recursion/core/src/runtime/opcode.rs
@@ -40,7 +40,7 @@ pub enum Opcode {
 
     PrintF = 33,
     PrintE = 34,
-    Ext2Felt = 35,
+    HintExt2Felt = 35,
 
     FRIFold = 36,
     HintLen = 37,

diff --git a/recursion/core/src/stark/mod.rs b/recursion/core/src/stark/mod.rs
@@ -77,7 +77,7 @@ impl<F: PrimeField32 + BinomiallyExtendable<D>, const DEGREE: usize> RecursionAi
     pub fn get_wrap_all() -> Vec<Self> {
         once(RecursionAir::Program(ProgramChip))
             .chain(once(RecursionAir::Cpu(CpuChip {
-                fixed_log2_rows: Some(20),
+                fixed_log2_rows: Some(21),
                 _phantom: PhantomData,
             })))
             .chain(once(RecursionAir::MemoryGlobal(MemoryGlobalChip {