From c7f778fd9e0322d1a3f9851554df169a22ce1d29 Mon Sep 17 00:00:00 2001 From: chriseth Date: Fri, 20 Oct 2023 15:56:44 +0200 Subject: [PATCH 1/3] Implement mload with alignment correction built in. --- riscv/src/compiler.rs | 63 +++++++++++++++++++++---------------------- 1 file changed, 30 insertions(+), 33 deletions(-) diff --git a/riscv/src/compiler.rs b/riscv/src/compiler.rs index 0490c73f2..c716638d6 100644 --- a/riscv/src/compiler.rs +++ b/riscv/src/compiler.rs @@ -501,12 +501,31 @@ fn preamble(coprocessors: &CoProcessors) -> String { // ============== memory instructions ============== + let up_to_three = |i| i % 4; + let six_bits = |i| i % 2**6; + /// Loads one word from an address Y, where Y can be between 0 and 2**33 (sic!), + /// wraps the address to 32 bits and rounds it down to the next multiple of 4. + /// Returns the loaded word and the remainder of the division by 4. + instr mload Y -> X, Z { + // Z * (Z - 1) * (Z - 2) * (Z - 3) = 0, + { Z } in { up_to_three }, + Y = wrap_bit * 2**32 + X_b4 * 0x1000000 + X_b3 * 0x10000 + X_b2 * 0x100 + X_b1 * 4 + Z, + { X_b1 } in { six_bits }, + { + X_b4 * 0x1000000 + X_b3 * 0x10000 + X_b2 * 0x100 + X_b1 * 4, + STEP, + X + } is m_is_read { m_addr, m_step, m_value } + // If we could access the shift machine here, we + // could even do the following to complete the mload: + // { W, X, Z} in { shr.value, shr.amount, shr.amount} + } + instr mstore Y, Z { { X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000, STEP, Z } is m_is_write { m_addr, m_step, m_value }, // Wrap the addr value Y = (X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000) + wrap_bit * 2**32 } - instr mload -> X { { addr, STEP, X } is m_is_read { m_addr, m_step, m_value } } // ============== control-flow instructions ============== @@ -1174,23 +1193,14 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso "lw" => { let (rd, rs, off) = rro(args); // TODO we need to consider misaligned loads / stores - only_if_no_write_to_zero_vec( - vec![ - format!("addr <== wrap({rs} + {off});"), - format!("{rd} <== mload();"), - ], - rd, - ) + only_if_no_write_to_zero_vec(vec![format!("{rd}, tmp1 <== mload({rs} + {off});")], rd) } "lb" => { // load byte and sign-extend. the memory is little-endian. let (rd, rs, off) = rro(args); only_if_no_write_to_zero_vec( vec![ - format!("tmp1 <== wrap({rs} + {off});"), - "addr <== and(tmp1, 0xfffffffc);".to_string(), - "tmp2 <== and(tmp1, 0x3);".to_string(), - format!("{rd} <== mload();"), + format!("{rd}, tmp2 <== mload({rs} + {off});"), format!("{rd} <== shr({rd}, 8 * tmp2);"), format!("{rd} <== sign_extend_byte({rd});"), ], @@ -1202,10 +1212,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso let (rd, rs, off) = rro(args); only_if_no_write_to_zero_vec( vec![ - format!("tmp1 <== wrap({rs} + {off});"), - "addr <== and(tmp1, 0xfffffffc);".to_string(), - "tmp2 <== and(tmp1, 0x3);".to_string(), - format!("{rd} <== mload();"), + format!("{rd}, tmp2 <== mload({rs} + {off});"), format!("{rd} <== shr({rd}, 8 * tmp2);"), format!("{rd} <== and({rd}, 0xff);"), ], @@ -1218,10 +1225,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso let (rd, rs, off) = rro(args); only_if_no_write_to_zero_vec( vec![ - format!("tmp1 <== wrap({rs} + {off});"), - "addr <== and(tmp1, 0xfffffffc);".to_string(), - "tmp2 <== and(tmp1, 0x3);".to_string(), - format!("{rd} <== mload();"), + format!("{rd}, tmp2 <== mload({rs} + {off});"), format!("{rd} <== shr({rd}, 8 * tmp2);"), format!("{rd} <== sign_extend_16_bits({rd});"), ], @@ -1234,10 +1238,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso let (rd, rs, off) = rro(args); only_if_no_write_to_zero_vec( vec![ - format!("tmp1 <== wrap({rs} + {off});"), - "addr <== and(tmp1, 0xfffffffc);".to_string(), - "tmp2 <== and(tmp1, 0x3);".to_string(), - format!("{rd} <== mload();"), + format!("{rd}, tmp2 <== mload({rs} + {off});"), format!("{rd} <== shr({rd}, 8 * tmp2);"), format!("{rd} <== and({rd}, 0x0000ffff);"), ], @@ -1257,8 +1258,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso vec![ format!("tmp1 <== wrap({rd} + {off});"), "addr <== and(tmp1, 0xfffffffc);".to_string(), - "tmp2 <== and(tmp1, 0x3);".to_string(), - "tmp1 <== mload();".to_string(), + format!("tmp1, tmp2 <== mload({rd} + {off});"), "tmp3 <== shl(0xffff, 8 * tmp2);".to_string(), "tmp3 <== xor(tmp3, 0xffffffff);".to_string(), "tmp1 <== and(tmp1, tmp3);".to_string(), @@ -1274,8 +1274,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso vec![ format!("tmp1 <== wrap({rd} + {off});"), "addr <== and(tmp1, 0xfffffffc);".to_string(), - "tmp2 <== and(tmp1, 0x3);".to_string(), - "tmp1 <== mload();".to_string(), + format!("tmp1, tmp2 <== mload({rd} + {off});"), "tmp3 <== shl(0xff, 8 * tmp2);".to_string(), "tmp3 <== xor(tmp3, 0xffffffff);".to_string(), "tmp1 <== and(tmp1, tmp3);".to_string(), @@ -1309,7 +1308,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso vec![ format!("addr <=X= {rs1};"), - format!("{rd} <== mload();"), + format!("{rd}, tmp1 <== mload({rs1});"), format!("tmp1 <== wrap({rd} + {rs2});"), format!("mstore addr, tmp1;"), ] @@ -1320,10 +1319,8 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso let (rd, rs, off) = rro(args); assert_eq!(off, 0); // TODO misaligned access should raise misaligned address exceptions - let mut statments = only_if_no_write_to_zero_vec( - vec![format!("addr <=X= {rs};"), format!("{rd} <== mload();")], - rd, - ); + let mut statments = + only_if_no_write_to_zero_vec(vec![format!("{rd}, tmp1 <== mload({rs});")], rd); statments.push("lr_sc_reservation <=X= 1;".into()); statments } From 554d123a2c46d925e7ebf38d99097421d61c2e53 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 25 Oct 2023 15:57:49 +0200 Subject: [PATCH 2/3] Remove addr register. --- riscv/src/compiler.rs | 31 ++++++++++++------------------- 1 file changed, 12 insertions(+), 19 deletions(-) diff --git a/riscv/src/compiler.rs b/riscv/src/compiler.rs index c716638d6..7f21cb60c 100644 --- a/riscv/src/compiler.rs +++ b/riscv/src/compiler.rs @@ -441,8 +441,6 @@ fn preamble(coprocessors: &CoProcessors) -> String { .collect::>() .concat() + r#" - // TODO: addr can be removed once mload also takes it via argument - reg addr; x0 = 0; @@ -521,6 +519,8 @@ fn preamble(coprocessors: &CoProcessors) -> String { // { W, X, Z} in { shr.value, shr.amount, shr.amount} } + /// Stores Z at address Y % 2**32. Y can be between 0 and 2**33. + /// Y should be a multiple of 4, but this instruction does not enforce it. instr mstore Y, Z { { X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000, STEP, Z } is m_is_write { m_addr, m_step, m_value }, // Wrap the addr value @@ -1256,8 +1256,6 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso let (rs, rd, off) = rro(args); vec![ - format!("tmp1 <== wrap({rd} + {off});"), - "addr <== and(tmp1, 0xfffffffc);".to_string(), format!("tmp1, tmp2 <== mload({rd} + {off});"), "tmp3 <== shl(0xffff, 8 * tmp2);".to_string(), "tmp3 <== xor(tmp3, 0xffffffff);".to_string(), @@ -1265,15 +1263,13 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso format!("tmp3 <== and({rs}, 0xffff);"), "tmp3 <== shl(tmp3, 8 * tmp2);".to_string(), "tmp1 <== or(tmp1, tmp3);".to_string(), - "mstore addr, tmp1;".to_string(), + format!("mstore {rd} + {off} - tmp2, tmp1;"), ] } "sb" => { // store byte let (rs, rd, off) = rro(args); vec![ - format!("tmp1 <== wrap({rd} + {off});"), - "addr <== and(tmp1, 0xfffffffc);".to_string(), format!("tmp1, tmp2 <== mload({rd} + {off});"), "tmp3 <== shl(0xff, 8 * tmp2);".to_string(), "tmp3 <== xor(tmp3, 0xffffffff);".to_string(), @@ -1281,7 +1277,7 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso format!("tmp3 <== and({rs}, 0xff);"), "tmp3 <== shl(tmp3, 8 * tmp2);".to_string(), "tmp1 <== or(tmp1, tmp3);".to_string(), - "mstore addr, tmp1;".to_string(), + format!("mstore {rd} + {off} - tmp2, tmp1;"), ] } "nop" => vec![], @@ -1300,18 +1296,15 @@ fn process_instruction(instr: &str, args: &[Argument], coprocessors: &CoProcesso let (rd, rs2, rs1, off) = rrro(args); assert_eq!(off, 0); - let rd = if rd.is_zero() { - "tmp2".to_string() - } else { - rd.to_string() - }; - - vec![ - format!("addr <=X= {rs1};"), - format!("{rd}, tmp1 <== mload({rs1});"), - format!("tmp1 <== wrap({rd} + {rs2});"), - format!("mstore addr, tmp1;"), + [ + vec![ + format!("tmp1, tmp2 <== mload({rs1});"), + format!("tmp2 <== wrap(tmp1 + {rs2});"), + format!("mstore {rs1}, tmp2;"), + ], + only_if_no_write_to_zero(format!("{rd} <== tmp1"), rd), ] + .concat() } insn if insn.starts_with("lr.w") => { From 86083d26a926210febbf8bd0f8d0901f3efe596a Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 26 Oct 2023 12:02:05 +0200 Subject: [PATCH 3/3] Extend panic message --- .../src/witgen/machines/double_sorted_witness_machine.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/executor/src/witgen/machines/double_sorted_witness_machine.rs b/executor/src/witgen/machines/double_sorted_witness_machine.rs index 98850fd89..67b985148 100644 --- a/executor/src/witgen/machines/double_sorted_witness_machine.rs +++ b/executor/src/witgen/machines/double_sorted_witness_machine.rs @@ -209,7 +209,11 @@ impl DoubleSortedWitnesses { left[2] ); if !(addr.clone().to_arbitrary_integer() % 4u32).is_zero() { - panic!("UNALIGNED"); + panic!( + "Unaligned memory access: addr={:x}, step={step}, write: {is_write}, left: {}", + addr.to_arbitrary_integer(), + left[2] + ); } // TODO this does not check any of the failure modes