From 04ad48a1f465cf0d6b47d12940d1848493c89f8b Mon Sep 17 00:00:00 2001 From: Lucas Clemente Vella Date: Wed, 31 Jan 2024 18:33:40 +0000 Subject: [PATCH 1/2] Merging instructions and saving a couple of columns. --- riscv-executor/src/lib.rs | 36 +++------------------------ riscv/src/compiler.rs | 52 +++++++++++++++++++++------------------ 2 files changed, 31 insertions(+), 57 deletions(-) diff --git a/riscv-executor/src/lib.rs b/riscv-executor/src/lib.rs index 6f9a8f91b..65ae2a87b 100644 --- a/riscv-executor/src/lib.rs +++ b/riscv-executor/src/lib.rs @@ -558,16 +558,12 @@ impl<'a, 'b, F: FieldElement> Executor<'a, 'b, F> { vec![] } - "jump" => { - self.proc.set_pc(args[0]); - - Vec::new() - } "load_label" => args, - "jump_dyn" => { + "jump" | "jump_dyn" => { + let next_pc = self.proc.get_pc().u() + 1; self.proc.set_pc(args[0]); - Vec::new() + vec![next_pc.into()] } "jump_to_bootloader_input" => { let bootloader_input_idx = args[0].0 as usize; @@ -576,32 +572,6 @@ impl<'a, 'b, F: FieldElement> Executor<'a, 'b, F> { Vec::new() } - "jump_and_link_dyn" => { - let pc = self.proc.get_pc(); - self.proc.set_reg("x1", pc.u() + 1); - self.proc.set_pc(args[0]); - - Vec::new() - } - "call" => { - let pc = self.proc.get_pc(); - self.proc.set_reg("x1", pc.u() + 1); - self.proc.set_pc(args[0]); - - Vec::new() - } - "tail" => { - self.proc.set_pc(args[0]); - self.proc.set_reg("x6", args[0]); - - Vec::new() - } - "ret" => { - let target = self.proc.get_reg("x1"); - self.proc.set_pc(target); - - Vec::new() - } "branch_if_nonzero" => { if args[0].0 != 0 { self.proc.set_pc(args[1]); diff --git a/riscv/src/compiler.rs b/riscv/src/compiler.rs index ea5be4e3f..5881bd200 100644 --- a/riscv/src/compiler.rs +++ b/riscv/src/compiler.rs @@ -187,10 +187,10 @@ pub fn compile( .into_iter() .map(|(id, dir, file)| format!(".debug file {id} {} {};", quote(&dir), quote(&file))) .chain(bootloader_and_shutdown_routine_lines) - .chain(["call __data_init;".to_string()]) + .chain(["x1 <== jump(__data_init);".to_string()]) .chain([ format!("// Set stack pointer\nx2 <=X= {stack_start};"), - "call __runtime_start;".to_string(), + "x1 <== jump(__runtime_start);".to_string(), "return;".to_string(), // This is not "riscv ret", but "return from powdr asm function". ]) .chain( @@ -200,7 +200,10 @@ pub fn compile( ) .chain(["// This is the data initialization routine.\n__data_init:".to_string()]) .chain(data_code) - .chain(["// This is the end of the data initialization routine.\nret;".to_string()]) + .chain([ + "// This is the end of the data initialization routine.\ntmp1 <== jump_dyn(x1);" + .to_string(), + ]) .collect(); // The program ROM needs to fit the degree, so we use the next power of 2. @@ -475,12 +478,10 @@ fn preamble(degree: u64, coprocessors: &CoProcessors, with_bootloader: bool) -> // ============== control-flow instructions ============== - instr jump l: label { pc' = l } instr load_label l: label -> X { X = l } - instr jump_dyn X { pc' = X } - instr jump_and_link_dyn X { pc' = X, x1' = pc + 1 } - instr call l: label { pc' = l, x1' = pc + 1 } - instr ret { pc' = x1 } + + instr jump l: label -> Y { pc' = l, Y = pc + 1} + instr jump_dyn X -> Y { pc' = X, Y = pc + 1} instr branch_if_nonzero X, l: label { pc' = (1 - XIsZero) * l + XIsZero * (pc + 1) } instr branch_if_zero X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) } @@ -933,7 +934,11 @@ fn try_coprocessor_substitution(label: &str, coprocessors: &CoProcessors) -> Opt fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcessors) -> Vec { match instr { // load/store registers - "li" => { + "li" | "la" => { + // The difference between "li" and "la" in RISC-V is that the former + // is for loading values as is, and the later is for loading PC + // relative values. But since we work on a higher abstraction level, + // for us they are the same thing. let (rd, imm) = ri(args); only_if_no_write_to_zero(format!("{rd} <=X= {imm};"), rd) } @@ -942,10 +947,6 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso let (rd, imm) = ri(args); only_if_no_write_to_zero(format!("{rd} <=X= {};", imm << 12), rd) } - "la" => { - let (rd, addr) = ri(args); - only_if_no_write_to_zero(format!("{rd} <=X= {};", addr), rd) - } "mv" => { let (rd, rs) = rr(args); only_if_no_write_to_zero(format!("{rd} <=X= {rs};"), rd) @@ -1250,14 +1251,17 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso // jump and call "j" => { if let [label] = args { - vec![format!("jump {};", argument_to_escaped_symbol(label))] + vec![format!( + "tmp1 <== jump({});", + argument_to_escaped_symbol(label) + )] } else { panic!() } } "jr" => { let rs = r(args); - vec![format!("jump_dyn {rs};")] + vec![format!("tmp1 <== jump_dyn({rs});")] } "jal" => { let (_rd, _label) = rl(args); @@ -1266,7 +1270,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso "jalr" => { // TODO there is also a form that takes more arguments let rs = r(args); - vec![format!("jump_and_link_dyn {rs};")] + vec![format!("x1 <== jump_dyn({rs});")] } "call" | "tail" => { // Depending on what symbol is called, the call is replaced by a @@ -1282,9 +1286,9 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso }; match (replacement, instr) { (None, instr) => { - let instr = if instr == "tail" { "jump" } else { instr }; let arg = argument_to_escaped_symbol(label); - vec![format!("{instr} {arg};")] + let dest = if instr == "tail" { "tmp1" } else { "x1" }; + vec![format!("{dest} <== jump({arg});")] } // Both "call" and "tail" are pseudoinstructions that are // supposed to use x6 to calculate the high bits of the @@ -1292,7 +1296,9 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso // but no sane program would rely on this behavior, so we are // probably fine. (Some(replacement), "call") => vec![replacement], - (Some(replacement), "tail") => vec![replacement, "ret;".to_string()], + (Some(replacement), "tail") => { + vec![replacement, "tmp1 <== jump_dyn(x1);".to_string()] + } (Some(_), _) => unreachable!(), } } @@ -1308,7 +1314,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso } "ret" => { assert!(args.is_empty()); - vec!["ret;".to_string()] + vec!["tmp1 <== jump_dyn(x1);".to_string()] } // memory access @@ -1402,7 +1408,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso format!("mstore {rd} + {off} - tmp2, tmp1;"), ] } - "nop" => vec![], + "fence" | "fence.i" | "nop" => vec![], "unimp" => vec!["fail;".to_string()], // Special instruction that is inserted to allow dynamic label references @@ -1411,9 +1417,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso only_if_no_write_to_zero(format!("{rd} <== load_label({label});"), rd) } - // atomic and synchronization - "fence" | "fence.i" => vec![], - + // atomic instructions insn if insn.starts_with("amoadd.w") => { let (rd, rs2, rs1, off) = rrro(args); assert_eq!(off, 0); From d5958d9fbd7235ebf9d593b0a42feaa251504eda Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Thu, 1 Feb 2024 09:40:21 +0100 Subject: [PATCH 2/2] Fix bootloader --- riscv/src/continuations/bootloader.rs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/riscv/src/continuations/bootloader.rs b/riscv/src/continuations/bootloader.rs index 56b649705..264aecc18 100644 --- a/riscv/src/continuations/bootloader.rs +++ b/riscv/src/continuations/bootloader.rs @@ -138,19 +138,19 @@ pub fn bootloader_and_shutdown_routine(submachine_initialization: &[String]) -> bootloader.push_str(&format!( r#" // Skip the next instruction -jump submachine_init; +tmp1 <== jump(submachine_init); // For convenience, this instruction has a known fixed PC ({DEFAULT_PC}) and just jumps // to whatever comes after the bootloader + shutdown routine. This avoids having to count // the instructions of the bootloader and the submachine initialization. -jump computation_start; +tmp1 <== jump(computation_start); // Similarly, this instruction has a known fixed PC ({SHUTDOWN_START}) and just jumps // to the shutdown routine. -jump shutdown_start; +tmp1 <== jump(shutdown_start); shutdown_sink: -jump shutdown_sink; +tmp1 <== jump(shutdown_sink); // Submachine initialization: Calls each submachine once, because that helps witness // generation figure out default values that can be used if the machine is never used. @@ -282,7 +282,7 @@ P4 <== load_bootloader_input(x2 * {BOOTLOADER_INPUTS_PER_PAGE} + {PAGE_INPUTS_OF P5 <== load_bootloader_input(x2 * {BOOTLOADER_INPUTS_PER_PAGE} + {PAGE_INPUTS_OFFSET} + 1 + {WORDS_PER_PAGE} + 4 + {i} * 4 + 1); P6 <== load_bootloader_input(x2 * {BOOTLOADER_INPUTS_PER_PAGE} + {PAGE_INPUTS_OFFSET} + 1 + {WORDS_PER_PAGE} + 4 + {i} * 4 + 2); P7 <== load_bootloader_input(x2 * {BOOTLOADER_INPUTS_PER_PAGE} + {PAGE_INPUTS_OFFSET} + 1 + {WORDS_PER_PAGE} + 4 + {i} * 4 + 3); -jump bootloader_level_{i}_end; +tmp1 <== jump(bootloader_level_{i}_end); bootloader_level_{i}_is_right: P4 <=X= P0; P5 <=X= P1; @@ -307,7 +307,7 @@ branch_if_nonzero P0 - x5, bootloader_memory_hash_mismatch; branch_if_nonzero P1 - x6, bootloader_memory_hash_mismatch; branch_if_nonzero P2 - x7, bootloader_memory_hash_mismatch; branch_if_nonzero P3 - x8, bootloader_memory_hash_mismatch; -jump bootloader_memory_hash_ok; +tmp1 <== jump(bootloader_memory_hash_ok); bootloader_memory_hash_mismatch: fail; bootloader_memory_hash_ok: @@ -322,7 +322,7 @@ P2 <== load_bootloader_input(x2 * {BOOTLOADER_INPUTS_PER_PAGE} + {PAGE_INPUTS_OF P3 <== load_bootloader_input(x2 * {BOOTLOADER_INPUTS_PER_PAGE} + {PAGE_INPUTS_OFFSET} + 1 + {WORDS_PER_PAGE} + 3); // Repeat Merkle proof validation loop to compute updated Merkle root -jump bootloader_merkle_proof_validation_loop; +tmp1 <== jump(bootloader_merkle_proof_validation_loop); bootloader_update_memory_hash: @@ -478,7 +478,7 @@ branch_if_nonzero x2 - x1, shutdown_start_page_loop; shutdown_end_page_loop: -jump shutdown_sink; +tmp1 <== jump(shutdown_sink); // END OF SHUTDOWN ROUTINE