github/powdr
1
1
Fork 0
mirror of https://github.com/powdr-labs/powdr.git synced 2026-04-20 03:03:25 -04:00
Code Issues Packages Projects Releases Wiki Activity

Remove inlined memory machine from RISC-V machine 🎉 (#1462)

Browse Source 
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.
```
This commit is contained in:
Georg Wiese
2024-06-25 11:42:44 +02:00
committed by GitHub
parent 1c465e566b
commit c19de6ba83
1 changed files with 9 additions and 125 deletions
Download Patch File Download Diff File Expand all files Collapse all files

134
riscv/src/code_gen.rs
View File

@@ -497,127 +497,23 @@ fn mul_instruction<T: FieldElement>(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 {