Fix soundness bug in mul instruction of RISC-V machine

cli/src/main.rs

@@ -476,13 +476,6 @@ fn run_command(command: Commands) {
             just_execute,
             continuations,
         } => {
-            let coprocessors = match coprocessors {
-                Some(list) => {
-                    powdr_riscv::CoProcessors::try_from(list.split(',').collect::<Vec<_>>())
-                        .unwrap()
-                }
-                None => powdr_riscv::CoProcessors::base(),
-            };
             call_with_field!(run_rust::<field>(
                 &file,
                 split_inputs(&inputs),
@@ -518,13 +511,6 @@ fn run_command(command: Commands) {
                 Cow::Borrowed("output")
             };
 
-            let coprocessors = match coprocessors {
-                Some(list) => {
-                    powdr_riscv::CoProcessors::try_from(list.split(',').collect::<Vec<_>>())
-                        .unwrap()
-                }
-                None => powdr_riscv::CoProcessors::base(),
-            };
             call_with_field!(run_riscv_asm::<field>(
                 &name,
                 files.into_iter(),
@@ -681,11 +667,17 @@ fn run_rust<F: FieldElement>(
     prove_with: Option<BackendType>,
     export_csv: bool,
     csv_mode: CsvRenderModeCLI,
-    coprocessors: powdr_riscv::CoProcessors,
+    coprocessors: Option<String>,
     just_execute: bool,
     continuations: bool,
 ) -> Result<(), Vec<String>> {
-    let (asm_file_path, asm_contents) = compile_rust(
+    let coprocessors = match coprocessors {
+        Some(list) => {
+            powdr_riscv::CoProcessors::try_from(list.split(',').collect::<Vec<_>>()).unwrap()
+        }
+        None => powdr_riscv::CoProcessors::base::<F>(),
+    };
+    let (asm_file_path, asm_contents) = compile_rust::<F>(
         file_name,
         output_dir,
         force_overwrite,
@@ -724,11 +716,17 @@ fn run_riscv_asm<F: FieldElement>(
     prove_with: Option<BackendType>,
     export_csv: bool,
     csv_mode: CsvRenderModeCLI,
-    coprocessors: powdr_riscv::CoProcessors,
+    coprocessors: Option<String>,
     just_execute: bool,
     continuations: bool,
 ) -> Result<(), Vec<String>> {
-    let (asm_file_path, asm_contents) = compile_riscv_asm(
+    let coprocessors = match coprocessors {
+        Some(list) => {
+            powdr_riscv::CoProcessors::try_from(list.split(',').collect::<Vec<_>>()).unwrap()
+        }
+        None => powdr_riscv::CoProcessors::base::<F>(),
+    };
+    let (asm_file_path, asm_contents) = compile_riscv_asm::<F>(
         original_file_name,
         file_names,
         output_dir,

pipeline/benches/executor_benchmark.rs

@@ -32,7 +32,7 @@ fn executor_benchmark(c: &mut Criterion) {
     let tmp_dir = Temp::new_dir().unwrap();
     let riscv_asm_files =
         compile_rust_crate_to_riscv_asm("../riscv/tests/riscv_data/keccak/Cargo.toml", &tmp_dir);
-    let contents = compiler::compile(riscv_asm_files, &CoProcessors::base(), false);
+    let contents = compiler::compile::<T>(riscv_asm_files, &CoProcessors::base::<T>(), false);
     let mut pipeline = Pipeline::<T>::default().from_asm_string(contents, None);
     let pil = pipeline.compute_optimized_pil().unwrap();
     let fixed_cols = pipeline.compute_fixed_cols().unwrap();
@@ -44,7 +44,11 @@ fn executor_benchmark(c: &mut Criterion) {
     // The first chunk of `many_chunks`, with Poseidon co-processor & bootloader
     let riscv_asm_files =
         compile_rust_to_riscv_asm("../riscv/tests/riscv_data/many_chunks.rs", &tmp_dir);
-    let contents = compiler::compile(riscv_asm_files, &CoProcessors::base().with_poseidon(), true);
+    let contents = compiler::compile::<T>(
+        riscv_asm_files,
+        &CoProcessors::base::<T>().with_poseidon(),
+        true,
+    );
     let mut pipeline = Pipeline::<T>::default().from_asm_string(contents, None);
     let pil = pipeline.compute_optimized_pil().unwrap();
     let fixed_cols = pipeline.compute_fixed_cols().unwrap();

riscv/src/compiler.rs

@@ -15,6 +15,7 @@ use powdr_asm_utils::{
     },
     Architecture,
 };
+use powdr_number::{FieldElement, KnownField};
 
 use crate::continuations::bootloader::{bootloader_and_shutdown_routine, bootloader_preamble};
 use crate::coprocessors::*;
@@ -102,7 +103,7 @@ impl Architecture for RiscvArchitecture {
 }
 
 /// Compiles riscv assembly to a powdr assembly file. Adds required library routines.
-pub fn compile(
+pub fn compile<T: FieldElement>(
     mut assemblies: BTreeMap<String, String>,
     coprocessors: &CoProcessors,
     with_bootloader: bool,
@@ -258,7 +259,7 @@ pub fn compile(
 
     riscv_machine(
         &coprocessors.machine_imports(),
-        &preamble(degree, coprocessors, with_bootloader),
+        &preamble::<T>(degree, coprocessors, with_bootloader),
         initial_mem,
         &coprocessors.declarations(),
         program,
@@ -475,13 +476,19 @@ let initial_memory: (fe, fe)[] = [
     )
 }
 
-fn preamble(degree: u64, coprocessors: &CoProcessors, with_bootloader: bool) -> String {
+fn preamble<T: FieldElement>(
+    degree: u64,
+    coprocessors: &CoProcessors,
+    with_bootloader: bool,
+) -> String {
     let bootloader_preamble_if_included = if with_bootloader {
         bootloader_preamble()
     } else {
         "".to_string()
     };
 
+    let mul_instruction = mul_instruction::<T>();
+
     format!("degree {degree};")
         + r#"
     reg pc[@pc];
@@ -643,7 +650,15 @@ fn preamble(degree: u64, coprocessors: &CoProcessors, with_bootloader: bool) ->
         // quotient is 32 bits:
         Z = X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000
     }
+"# + mul_instruction
+}
 
+fn mul_instruction<T: FieldElement>() -> &'static str {
+    match T::known_field().expect("Unknown field!") {
+        KnownField::Bn254Field => {
+            // The BN254 field can fit any 64-bit number, so we can naively de-compose
+            // Z * W into 8 bytes and put them together to get the upper and lower word.
+            r#"
     // Multiply two 32-bits unsigned, return the upper and lower unsigned 32-bit
     // halves of the result.
     // X is the lower half (least significant bits)
@@ -654,6 +669,19 @@ fn preamble(degree: u64, coprocessors: &CoProcessors, with_bootloader: bool) ->
         Y = Y_b5 + Y_b6 * 0x100 + Y_b7 * 0x10000 + Y_b8 * 0x1000000
     }
 "#
+        }
+        KnownField::GoldilocksField => {
+            // The Goldilocks field cannot fit some 64-bit numbers, so we have to use
+            // the split machine. Note that it can fit a product of two 32-bit numbers.
+            r#"
+    // Multiply two 32-bits unsigned, return the upper and lower unsigned 32-bit
+    // halves of the result.
+    // X is the lower half (least significant bits)
+    // Y is the higher half (most significant bits)
+    instr mul Z, W -> X, Y = split_gl.split Z * W -> X, Y;
+"#
+        }
+    }
 }
 
 fn memory(with_bootloader: bool) -> String {

riscv/src/coprocessors.rs

@@ -3,6 +3,8 @@ use std::{
     convert::TryFrom,
 };
 
+use powdr_number::{FieldElement, KnownField};
+
 type RuntimeFunctionImpl = (&'static str, fn() -> String);
 
 #[derive(Debug, Clone, Ord, PartialOrd, Eq, PartialEq)]
@@ -120,14 +122,19 @@ impl TryFrom<Vec<&str>> for CoProcessors {
 
 impl CoProcessors {
     /// The base version only adds the commonly used bitwise and shift operations.
-    pub fn base() -> CoProcessors {
-        Self {
-            coprocessors: BTreeMap::from([
-                (BINARY_COPROCESSOR.name, &BINARY_COPROCESSOR),
-                (SHIFT_COPROCESSOR.name, &SHIFT_COPROCESSOR),
-                (INPUT_COPROCESSOR.name, &INPUT_COPROCESSOR),
-            ]),
+    pub fn base<T: FieldElement>() -> CoProcessors {
+        let mut coprocessors = BTreeMap::from([
+            (BINARY_COPROCESSOR.name, &BINARY_COPROCESSOR),
+            (SHIFT_COPROCESSOR.name, &SHIFT_COPROCESSOR),
+            (INPUT_COPROCESSOR.name, &INPUT_COPROCESSOR),
+        ]);
+
+        if matches!(T::known_field(), Some(KnownField::GoldilocksField)) {
+            // The mul instructions needs the split machine.
+            coprocessors.insert(SPLIT_GL_COPROCESSOR.name, &SPLIT_GL_COPROCESSOR);
         }
+
+        Self { coprocessors }
     }
 
     /// Poseidon also uses the Split machine.

riscv/src/lib.rs

@@ -9,6 +9,7 @@ use std::{
 };
 
 use mktemp::Temp;
+use powdr_number::FieldElement;
 use serde_json::Value as JsonValue;
 use std::fs;
 
@@ -28,7 +29,7 @@ type Expression = powdr_asm_utils::ast::Expression<FunctionKind>;
 /// Compiles a rust file all the way down to PIL and generates
 /// fixed and witness columns.
 #[allow(clippy::print_stderr)]
-pub fn compile_rust(
+pub fn compile_rust<T: FieldElement>(
     file_name: &str,
     output_dir: &Path,
     force_overwrite: bool,
@@ -69,7 +70,7 @@ pub fn compile_rust(
         log::info!("Wrote {}", riscv_asm_file_name.to_str().unwrap());
     }
 
-    compile_riscv_asm_bundle(
+    compile_riscv_asm_bundle::<T>(
         file_name,
         riscv_asm,
         output_dir,
@@ -80,7 +81,7 @@ pub fn compile_rust(
 }
 
 #[allow(clippy::print_stderr)]
-pub fn compile_riscv_asm_bundle(
+pub fn compile_riscv_asm_bundle<T: FieldElement>(
     original_file_name: &str,
     riscv_asm_files: BTreeMap<String, String>,
     output_dir: &Path,
@@ -104,7 +105,7 @@ pub fn compile_riscv_asm_bundle(
         return None;
     }
 
-    let powdr_asm = compiler::compile(riscv_asm_files, coprocessors, with_bootloader);
+    let powdr_asm = compiler::compile::<T>(riscv_asm_files, coprocessors, with_bootloader);
 
     fs::write(powdr_asm_file_name.clone(), &powdr_asm).unwrap();
     log::info!("Wrote {}", powdr_asm_file_name.to_str().unwrap());
@@ -114,15 +115,15 @@ pub fn compile_riscv_asm_bundle(
 
 /// Compiles a riscv asm file all the way down to PIL and generates
 /// fixed and witness columns.
-pub fn compile_riscv_asm(
+pub fn compile_riscv_asm<T: FieldElement>(
     original_file_name: &str,
     file_names: impl Iterator<Item = String>,
     output_dir: &Path,
     force_overwrite: bool,
     coprocessors: &CoProcessors,
     with_bootloader: bool,
 ) -> Option<(PathBuf, String)> {
-    compile_riscv_asm_bundle(
+    compile_riscv_asm_bundle::<T>(
         original_file_name,
         file_names
             .map(|name| {

riscv/tests/instructions.rs

@@ -2,15 +2,16 @@ mod common;
 
 mod instruction_tests {
     use crate::common::verify_riscv_asm_string;
+    use powdr_number::GoldilocksField;
     use powdr_riscv::compiler::compile;
     use powdr_riscv::CoProcessors;
     use test_log::test;
 
     fn run_instruction_test(assembly: &str, name: &str) {
         // TODO Should we create one powdr-asm from all tests or keep them separate?
-        let powdr_asm = compile(
+        let powdr_asm = compile::<GoldilocksField>(
             [(name.to_string(), assembly.to_string())].into(),
-            &CoProcessors::base(),
+            &CoProcessors::base::<GoldilocksField>(),
             false,
         );