Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Dev/mem heap #180

Merged
merged 3 commits into from
Dec 9, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 10 additions & 1 deletion circuits/src/cpu/cpu_stark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -845,7 +845,6 @@ impl<
+ lv[COL_S_SSTORE]
+ lv[COL_S_TLOAD] * (lv[COL_OP0] * lv[COL_OP1] + (P::ONES - lv[COL_OP0]))
+ lv[COL_S_TSTORE] * lv[COL_OP1]
+ lv[COL_S_TSTORE] * lv[COL_OP1]
+ lv[COL_S_CALL_SC]
+ lv[COL_S_END] * (P::ONES - lv_is_entry_sc);
let is_crossing_inst = lv[COL_IS_NEXT_LINE_DIFF_INST];
Expand Down Expand Up @@ -1017,6 +1016,16 @@ mod tests {
test_cpu_with_asm_file_name(program_path.to_string(), Some(call_data), None);
}

#[test]
fn test_global() {
let call_data = vec![
GoldilocksField::ZERO,
GoldilocksField::from_canonical_u64(4171824493),
];
let program_path = "global.json";
test_cpu_with_asm_file_name(program_path.to_string(), Some(call_data), None);
}

#[test]
fn test_malloc() {
let program_path = "malloc.json";
Expand Down
53 changes: 46 additions & 7 deletions circuits/src/memory/memory_stark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,9 @@ pub fn ctl_filter_with_poseidon_chunk<F: Field>() -> Column<F> {
Column::single(COL_MEM_S_POSEIDON)
}

const ADDR_HEAP_PTR: u64 = 18446744060824649731u64;
const INIT_VALUE_HEAP_PTR: u64 = ADDR_HEAP_PTR + 1;

#[derive(Copy, Clone, Default)]
pub struct MemoryStark<F, const D: usize> {
pub f: PhantomData<F>,
Expand Down Expand Up @@ -110,6 +113,8 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F

let p = P::ZEROS;
let span = P::Scalar::from_canonical_u64(2_u64.pow(32).sub(1));
let addr_heap_ptr = P::Scalar::from_canonical_u64(ADDR_HEAP_PTR);
let init_value_heap_ptr = P::Scalar::from_canonical_u64(INIT_VALUE_HEAP_PTR);

let is_rw = lv[COL_MEM_IS_RW];
let region_prophet = lv[COL_MEM_REGION_PROPHET];
Expand All @@ -129,7 +134,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
let nv_rw_addr_unchanged = nv[COL_MEM_RW_ADDR_UNCHANGED];
let diff_addr_cond = lv[COL_MEM_DIFF_ADDR_COND];
let value = lv[COL_MEM_VALUE];
let nv_value = lv[COL_MEM_VALUE];
let nv_value = nv[COL_MEM_VALUE];
let diff_clk = lv[COL_MEM_DIFF_CLK];
let rc_value = lv[COL_MEM_RC_VALUE];
let filter_looking_rc = lv[COL_MEM_FILTER_LOOKING_RC];
Expand Down Expand Up @@ -267,16 +272,40 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
// * (nv[COL_MEM_ENV_IDX] - lv[COL_MEM_ENV_IDX]

// read/write constraint:
// 1. first operation for each addr must be write;
// 2. next value does not change if it is read.
yield_constr.constraint_first_row(P::ONES - is_write);
// 1. first operation for each addr must be write(except heap ptr);
// 2. next value does not change if it is read(except heap ptr).
// 3. if heap ptr first op is read, it must be heap_ptr + 1.
yield_constr.constraint_first_row(is_rw * (P::ONES - is_write) * (addr - addr_heap_ptr));
yield_constr.constraint(
(nv[COL_MEM_TX_IDX] - lv[COL_MEM_TX_IDX])
* (nv[COL_MEM_ENV_IDX] - lv[COL_MEM_ENV_IDX])
* (P::ONES - nv_is_write),
* nv[COL_MEM_IS_RW]
* (P::ONES - nv_is_write)
* (nv_addr - addr_heap_ptr),
);
yield_constr
.constraint((nv_addr - addr) * (P::ONES - nv_is_write) * (nv_addr - addr_heap_ptr));
yield_constr
.constraint((P::ONES - nv_is_write) * (nv_value - value) * (nv_addr - addr_heap_ptr));

let is_next_addr_heap_ptr = if (nv_addr - P::Scalar::from_canonical_u64(ADDR_HEAP_PTR))
.as_slice()
.iter()
.all(|item| item.is_zero())
{
P::ONES
} else {
P::ZEROS
};
yield_constr.constraint(
is_next_addr_heap_ptr * (nv_addr - P::Scalar::from_canonical_u64(ADDR_HEAP_PTR)),
);
yield_constr.constraint(
(addr - P::Scalar::from_canonical_u64(ADDR_HEAP_PTR))
* is_next_addr_heap_ptr
* (P::ONES - nv_is_write)
* (nv_value - P::Scalar::from_canonical_u64(INIT_VALUE_HEAP_PTR)),
);
yield_constr.constraint((nv_addr - addr) * (P::ONES - nv_is_write));
yield_constr.constraint((P::ONES - nv_is_write) * (nv_value - value));

// rc_value constraint:
yield_constr.constraint_transition(
Expand Down Expand Up @@ -373,6 +402,16 @@ mod tests {
test_memory_with_asm_file_name(program_path.to_string(), Some(call_data));
}

#[test]
fn test_memory_global() {
let call_data = vec![
GoldilocksField::ZERO,
GoldilocksField::from_canonical_u64(4171824493),
];
let program_path = "global.json";
test_memory_with_asm_file_name(program_path.to_string(), Some(call_data));
}

#[allow(unused)]
fn test_memory_with_asm_file_name(file_name: String, call_data: Option<Vec<GoldilocksField>>) {
let mut path = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
Expand Down
9 changes: 9 additions & 0 deletions circuits/src/stark/ola_stark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -761,6 +761,15 @@ mod tests {
test_by_asm_json("storage_u32.json".to_string(), Some(call_data), None);
}

#[test]
fn test_ola_global() {
let call_data = vec![
GoldilocksField::ZERO,
GoldilocksField::from_canonical_u64(4171824493),
];
test_by_asm_json("global.json".to_string(), Some(call_data), None);
}

#[test]
fn test_ola_malloc() {
test_by_asm_json("malloc.json".to_string(), None, None);
Expand Down
17 changes: 13 additions & 4 deletions executor/src/trace.rs
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@
use crate::{GoldilocksField, MemRangeType, Process};
use core::merkle_tree::log::WitnessStorageLog;
use core::merkle_tree::tree::AccountTree;
use core::program::Program;
use core::trace::dump::{DumpMemoryRow, DumpStep, DumpTapeRow, DumpTrace};
use core::trace::trace::{MemoryTraceCell, StorageHashRow, TapeRow};
use core::types::merkle_tree::constant::ROOT_TREE_DEPTH;
use core::types::merkle_tree::{tree_key_to_u256, TreeKeyU256, TREE_VALUE_LEN};
use core::vm::error::ProcessorError;
use core::vm::memory::HP_START_ADDR;
use core::vm::memory::MEM_SPAN_SIZE;
use log::debug;
use plonky2::field::types::{Field, Field64, PrimeField64};
use core::merkle_tree::log::WitnessStorageLog;
use core::vm::memory::HP_START_ADDR;

use std::collections::HashMap;
use std::fs::File;
Expand All @@ -30,7 +30,12 @@ pub fn gen_memory_table(
let mut first_row_flag = true;
let mut first_heap_row_flag = true;

process.memory.trace.get_mut(&HP_START_ADDR).unwrap().remove(0);
process
.memory
.trace
.get_mut(&HP_START_ADDR)
.unwrap()
.remove(0);
for (field_addr, cells) in process.memory.trace.iter() {
let mut new_addr_flag = true;

Expand Down Expand Up @@ -210,7 +215,11 @@ pub fn storage_hash_table_gen(

let mut root_hashes = Vec::new();

for (chunk, log) in hash_traces.chunks(ROOT_TREE_DEPTH).enumerate().zip(storage_logs) {
for (chunk, log) in hash_traces
.chunks(ROOT_TREE_DEPTH)
.enumerate()
.zip(storage_logs)
{
let is_write = GoldilocksField::from_canonical_u64(log.storage_log.kind as u64);
let mut root_hash = [GoldilocksField::ZERO; TREE_VALUE_LEN];
root_hash.clone_from_slice(&chunk.1.last().unwrap().0.output[0..4]);
Expand Down
Loading