mirror of
https://github.com/powdr-labs/powdr.git
synced 2026-04-20 03:03:25 -04:00
1c465e566b
This PR adds a new memory machine to the standard library that also
supports a `mstore_bootloader` operation: It's like a normal `mstore`,
but the first access to every memory cell *has to* come from this
operation.
As a follow-up, we'll be able to use it in the RISC-V machine (#1462).
I think this is best reviewed by reviewing the diff to the normal memory
machine and comparing it to [the code we have currently inlined in the
RISC-V
machine](abbe26618f/riscv/src/code_gen.rs (L500-L553)):
```diff
3,5c3,7
< // A read/write memory, similar to that of Polygon:
< // https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/pil/mem.pil
< machine Memory with
---
> /// This machine is a slightly extended version of std::machines::memory::Memory,
> /// where in addition to mstore, there is an mstore_bootloader operation. It behaves
> /// just like mstore, except that the first access to each memory cell must come
> /// from the mstore_bootloader operation.
> machine MemoryWithBootloaderWrite with
7c9
< operation_id: m_is_write,
---
> operation_id: operation_id,
13a16
> operation mstore_bootloader<2> m_addr, m_step, m_value ->;
29a33
> col witness m_is_bootloader_write;
30a35,36
> std::utils::force_bool(m_is_bootloader_write);
> col operation_id = m_is_write + 2 * m_is_bootloader_write;
35a42
> (1 - is_mem_op) * m_is_bootloader_write = 0;
37,39c44,45
< // 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;
---
> // The first operation of a new address has to be a bootloader write
> m_change * (1 - m_is_bootloader_write') = 0;
41,42c47,52
< // 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;
---
> // 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;
46c56
< (1 - m_is_write') * (1 - m_change) * (m_value' - m_value) = 0;
---
> (1 - m_is_write' - m_is_bootloader_write') * (1 - m_change) * (m_value' - m_value) = 0;
➜ powdr git:(memory-with-bootloader-write) ✗
```
69 lines
1.5 KiB
Rust
69 lines
1.5 KiB
Rust
use std::machines::memory_with_bootloader_write::MemoryWithBootloaderWrite;
|
|
|
|
machine Main with degree: 65536 {
|
|
reg pc[@pc];
|
|
reg X[<=];
|
|
reg Y[<=];
|
|
reg A;
|
|
|
|
col fixed STEP(i) { i };
|
|
MemoryWithBootloaderWrite memory;
|
|
|
|
instr mload X -> Y link ~> Y = memory.mload(X, STEP);
|
|
instr mstore X, Y -> link ~> memory.mstore(X, STEP, Y);
|
|
instr mstore_bootloader X, Y -> link ~> memory.mstore_bootloader(X, STEP, Y);
|
|
|
|
instr assert_eq X, Y {
|
|
X = Y
|
|
}
|
|
|
|
function main {
|
|
|
|
// Initialize memory cells:
|
|
mstore_bootloader 100, 0;
|
|
mstore_bootloader 104, 0;
|
|
mstore_bootloader 200, 0;
|
|
mstore_bootloader 0xfffffffc, 0;
|
|
|
|
// Store 4
|
|
mstore 100, 4;
|
|
|
|
// Read initial memory value
|
|
A <== mload(104);
|
|
assert_eq A, 0;
|
|
|
|
// Read previously stored value
|
|
A <== mload(100);
|
|
assert_eq A, 4;
|
|
|
|
// Update previously stored value
|
|
mstore 100, 7;
|
|
mstore 100, 8;
|
|
|
|
// Read updated values (twice)
|
|
A <== mload(100);
|
|
assert_eq A, 8;
|
|
A <== mload(100);
|
|
assert_eq A, 8;
|
|
|
|
// Write to previously initialized memory cell
|
|
mstore 104, 1234;
|
|
A <== mload(104);
|
|
assert_eq A, 1234;
|
|
|
|
// Write very big field element
|
|
mstore 200, -1;
|
|
A <== mload(200);
|
|
assert_eq A, -1;
|
|
|
|
// Store at maximal address
|
|
mstore 0xfffffffc, 1;
|
|
A <== mload(0xfffffffc);
|
|
assert_eq A, 1;
|
|
|
|
|
|
|
|
return;
|
|
}
|
|
}
|