From c19de6ba83530853506155d8897bd2ad31eed2d2 Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Tue, 25 Jun 2024 11:42:44 +0200 Subject: [PATCH] =?UTF-8?q?Remove=20inlined=20memory=20machine=20from=20RI?= =?UTF-8?q?SC-V=20machine=20=F0=9F=8E=89=20=20(#1462)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Depends on #1463 With this PR, we finally use our std memory machine in the RISC-V machine. To test: ```bash cargo run -r --bin powdr-rs compile riscv/tests/riscv_data/keccak -o output -c cargo run -r --bin powdr-rs execute -c output/keccak.asm -o output --witness cargo run -r prove output/keccak.asm -d output/chunk_0 --backend estark-starky ``` The number of columns the same (for the simple memory machine): ``` Before: Removed 162 witness and 159 fixed columns. Total count now: 282 witness and 220 fixed columns. After: Removed 162 witness and 160 fixed columns. Total count now: 282 witness and 220 fixed columns. ``` --- riscv/src/code_gen.rs | 134 +++--------------------------------------- 1 file changed, 9 insertions(+), 125 deletions(-) diff --git a/riscv/src/code_gen.rs b/riscv/src/code_gen.rs index 231d1a3d1..622fb85b7 100644 --- a/riscv/src/code_gen.rs +++ b/riscv/src/code_gen.rs @@ -497,127 +497,23 @@ fn mul_instruction(runtime: &Runtime) -> &'static str { } fn memory(with_bootloader: bool) -> String { - // There are subtle differences between the memory machines with and without continuations: - // - There is an extra `mstore_bootloader` instruction. For the most part, it behaves just - // like `mstore`. - // - When `m_change` is true, the `m_is_bootloader_write` has to be true in the next row. - // - The `(1 - m_is_write') * m_change * m_value' = 0` constraint is removed, as we no longer can - // have a read as the first operation on a new address. - // - The `(1 - m_change) * LAST = 0` constraint is replaced with - // `LAST * (1 - m_change) * (m_addr + 1) = 0`. This allows for a valid assignment in the case - // where there is no memory operation in the entire chunk: The address can be set to -1 (which - // cannot be represented in 32 bits, hence there is can't be an actual memory operation - // associated with it). In that case, `m_change` can be 0 everywhere. - let bootloader_specific_parts = if with_bootloader { + let memory_machine = if with_bootloader { r#" - // Memory operation flags: If none is active, it's a read. - col witness m_is_write; - col witness m_is_bootloader_write; - std::utils::force_bool(m_is_write); - std::utils::force_bool(m_is_bootloader_write); - - // Selectors - col witness m_selector_read; - col witness m_selector_write; - col witness m_selector_bootloader_write; - std::utils::force_bool(m_selector_read); - std::utils::force_bool(m_selector_write); - std::utils::force_bool(m_selector_bootloader_write); - - // No selector active -> no write - (1 - m_selector_read - m_selector_write - m_selector_bootloader_write) * m_is_write = 0; - (1 - m_selector_read - m_selector_write - m_selector_bootloader_write) * m_is_bootloader_write = 0; - - // The first operation of a new address has to be a bootloader write - m_change * (1 - m_is_bootloader_write') = 0; - - // m_change has to be 1 in the last row, so that the above constraint is triggered. - // An exception to this when the last address is -1, which is only possible if there is - // no memory operation in the entire chunk (because addresses are 32 bit unsigned). - // This exception is necessary so that there can be valid assignment in this case. - pol m_change_or_no_memory_operations = (1 - m_change) * (m_addr + 1); - LAST * m_change_or_no_memory_operations = 0; - - // If the next line is a read and we stay at the same address, then the - // value cannot change. - (1 - m_is_write' - m_is_bootloader_write') * (1 - m_change) * (m_value' - m_value) = 0; - - col operation_id = m_is_write + 2 * m_is_bootloader_write; - - /// Like mstore, but setting the m_is_bootloader_write flag. - instr mstore_bootloader Y, Z { - { 2, X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000, STEP, Z } is m_selector_bootloader_write { operation_id, m_addr, m_step, m_value }, - // Wrap the addr value + std::machines::memory_with_bootloader_write::MemoryWithBootloaderWrite memory; + instr mstore_bootloader Y, Z -> link ~> memory.mstore_bootloader(X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000, STEP, Z) { Y = (X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000) + wrap_bit * 2**32 } "# } else { r#" - // Memory operation flags: If none is active, it's a read. - col witness m_is_write; - std::utils::force_bool(m_is_write); - - // Selectors - col witness m_selector_read; - col witness m_selector_write; - std::utils::force_bool(m_selector_read); - std::utils::force_bool(m_selector_write); - - // No selector active -> no write - (1 - m_selector_read - m_selector_write) * m_is_write = 0; - - col operation_id = m_is_write; - - // If the next line is a not a write and we have an address change, - // then the value is zero. - (1 - m_is_write') * m_change * m_value' = 0; - - // m_change has to be 1 in the last row, so that a first read on row zero is constrained to return 0 - (1 - m_change) * LAST = 0; - - // If the next line is a read and we stay at the same address, then the - // value cannot change. - (1 - m_is_write') * (1 - m_change) * (m_value' - m_value) = 0; + std::machines::memory::Memory memory; "# }; - r#" - - // =============== read-write memory ======================= - // Read-write memory. Columns are sorted by m_addr and - // then by m_step. m_change is 1 if and only if m_addr changes - // in the next row. - col witness m_addr; - col witness m_step; - col witness m_change; - col witness m_value; -"# - .to_string() - + bootloader_specific_parts + memory_machine.to_string() + r#" - col witness m_diff_lower; - col witness m_diff_upper; - col fixed FIRST = [1] + [0]*; - let LAST = FIRST'; col fixed STEP(i) { i }; - col fixed BIT16(i) { i & 0xffff }; - - {m_diff_lower} in {BIT16}; - {m_diff_upper} in {BIT16}; - - std::utils::force_bool(m_change); - - // if m_change is zero, m_addr has to stay the same. - (m_addr' - m_addr) * (1 - m_change) = 0; - - // Except for the last row, if m_change is 1, then m_addr has to increase, - // if it is zero, m_step has to increase. - // `m_diff_upper * 2**16 + m_diff_lower` has to be equal to the difference **minus one**. - // Since we know that both m_addr and m_step can only be 32-Bit, this enforces that - // the values are strictly increasing. - col diff = (m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step)); - (1 - LAST) * (diff - 1 - m_diff_upper * 2**16 - m_diff_lower) = 0; // ============== memory instructions ============== @@ -626,30 +522,18 @@ fn memory(with_bootloader: bool) -> String { /// 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, + instr mload Y -> X, Z link ~> X = memory.mload(X_b4 * 0x1000000 + X_b3 * 0x10000 + X_b2 * 0x100 + X_b1 * 4, STEP) { { 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 }, - { - 0, - X_b4 * 0x1000000 + X_b3 * 0x10000 + X_b2 * 0x100 + X_b1 * 4, - STEP, - X - } is m_selector_read { operation_id, 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} + { X_b1 } in { six_bits } } /// 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 { - { 1, X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000, STEP, Z } is m_selector_write { operation_id, m_addr, m_step, m_value }, - // Wrap the addr value + instr mstore Y, Z -> link ~> memory.mstore(X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000, STEP, Z) { Y = (X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000) + wrap_bit * 2**32 } - "# +"# } pub trait InstructionArgs {