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

WIP: Cont dev #210

Closed
wants to merge 28 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
cbb0f3c
feat: support continuation
junyu0312 Nov 14, 2023
b1a0d92
refine pre image table assignment
junyu0312 Nov 26, 2023
07c8724
refine post image table
junyu0312 Nov 26, 2023
5d79eda
review 1 fixed
junyu0312 Nov 27, 2023
2da075a
fix
junyu0312 Nov 27, 2023
f2fbe05
update comment
junyu0312 Dec 11, 2023
7530eb2
fix: use F instead of AssignedCell to avoid unwrap
junyu0312 Dec 11, 2023
64fda69
fix: fix termination state and imtable
junyu0312 Dec 11, 2023
2517cc2
fix etable assignment
junyu0312 Dec 12, 2023
dad3058
fix: fix constraints of etable
junyu0312 Dec 12, 2023
d3d0986
refine image table
junyu0312 Dec 12, 2023
3e234ba
refine image table
junyu0312 Dec 12, 2023
29c99b4
fix hardcode
junyu0312 Dec 13, 2023
06f99e4
add transpose for InitializationState
junyu0312 Dec 13, 2023
9febe19
chore: refine image table assignment
junyu0312 Dec 13, 2023
0a6b45d
fmt code
junyu0312 Dec 13, 2023
b54a506
set the number of frame table entry always 2
junyu0312 Dec 14, 2023
09b8638
fix code style
junyu0312 Dec 14, 2023
208b804
fix comment
junyu0312 Dec 14, 2023
6773632
add name for post image table col
junyu0312 Dec 14, 2023
d861066
fix image table assigner
junyu0312 Dec 14, 2023
1fd2066
fix circuit_without_witness
junyu0312 Dec 15, 2023
ce30af3
fix rlp_slice test
junyu0312 Dec 15, 2023
bdfbb8e
fix compiling error
junyu0312 Dec 15, 2023
418274f
fix code style
junyu0312 Dec 18, 2023
e884de6
fix: fix a bug of post image table
junyu0312 Dec 18, 2023
11a01cc
refine etable assignment
junyu0312 Dec 21, 2023
f933ea8
decrease the degree of post init memory lookup
junyu0312 Dec 22, 2023
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
19 changes: 10 additions & 9 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

3 changes: 2 additions & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,12 @@ exclude = ["third-party/wasmi", "crates/playground"]

[workspace.dependencies]
anyhow = { version = "1.0.68", features = ["backtrace"] }
cfg-if = "1.0.0"
halo2aggregator-s = { git = "https://github.com/DelphinusLab/halo2aggregator-s.git", branch = "main", features = ["unsafe"] }
halo2_proofs = { git = "https://github.com/DelphinusLab/halo2-gpu-specific.git", default-features = true }
parity-wasm = { version = "0.42.0", features = ["sign_ext"] }
rayon = "1.8.0"
wasmi = { path = "third-party/wasmi" }

[profile.dev]
opt-level = 3
opt-level = 3
18 changes: 15 additions & 3 deletions crates/cli/src/exec.rs
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ pub fn exec_setup(
info!("Create Verifying to {:?}", vk_path);
let loader = ZkWasmLoader::<Bn256>::new(zkwasm_k, wasm_binary, phantom_functions)?;

let vkey = loader.create_vkey(&params)?;
let vkey = loader.create_vkey(&params, true)?;
Copy link
Collaborator Author

@junyu0312 junyu0312 Nov 27, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

dump vkey of diffierent circuits


let mut fd = std::fs::File::create(&vk_path)?;
vkey.write(&mut fd)?;
Expand All @@ -96,12 +96,18 @@ pub fn exec_image_checksum(
) -> Result<()> {
let loader = ZkWasmLoader::<Bn256>::new(zkwasm_k, wasm_binary, phantom_functions)?;

let image = if cfg!(feature = "continuation") {
todo!("read slice image from file?");
} else {
loader.compile_without_env()?.tables
};

let params = load_or_build_unsafe_params::<Bn256>(
zkwasm_k,
Some(&output_dir.join(format!("K{}.params", zkwasm_k))),
);

let checksum = loader.checksum(&params)?;
let checksum = loader.checksum(&image, &params)?;
assert_eq!(checksum.len(), 1);
let checksum = checksum[0];

Expand Down Expand Up @@ -333,7 +339,13 @@ pub fn exec_verify_proof(

let proof = load_proof(proof_path);

loader.verify_proof(&params, vkey, instances, proof)?;
let image = if cfg!(feature = "continuation") {
todo!("read slice image from file?")
} else {
loader.compile_without_env()?.tables
};

loader.verify_proof(&image, &params, vkey, &instances, proof)?;

info!("Verifing proof passed");

Expand Down
1 change: 1 addition & 0 deletions crates/specs/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ serde = { version = "1.0", features = ["derive", "rc"] }
serde_json = "1.0"
strum = "0.24.1"
strum_macros = "0.24.1"
cfg-if.workspace = true
halo2_proofs.workspace = true
parity-wasm.workspace = true
rayon.workspace = true
Expand Down
2 changes: 1 addition & 1 deletion crates/specs/src/brtable.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ pub struct BrTableEntry {
pub dst_pc: u32,
}

#[derive(Debug)]
#[derive(Default, Serialize, Debug, Clone)]
pub struct BrTable(Vec<BrTableEntry>);

impl BrTable {
Expand Down
37 changes: 22 additions & 15 deletions crates/specs/src/encode/init_memory_table.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,43 +2,50 @@ use num_bigint::BigUint;
use num_bigint::ToBigUint;

use super::FromBn;
use crate::encode::COMMON_RANGE_OFFSET;
use crate::imtable::InitMemoryTableEntry;

pub(crate) const INIT_MEMORY_ENCODE_BOUNDARY: u32 = 224;
pub const MEMORY_ADDRESS_OFFSET: u32 = 97;

pub fn encode_init_memory_table_address<T: FromBn>(location_type: T, offset: T) -> T {
location_type * T::from_bn(&(1u64.to_biguint().unwrap() << 32)) + offset
}

pub fn encode_init_memory_table_entry<T: FromBn>(
ltype: T,
offset: T,
is_mutable: T,
start_offset: T,
end_offset: T,
eid: T,
value: T,
) -> T {
const LTYPE_SHIFT: u32 = IS_MUTABLE_SHIFT + 1;
const IS_MUTABLE_SHIFT: u32 = START_OFFSET_SHIFT + COMMON_RANGE_OFFSET;
const START_OFFSET_SHIFT: u32 = END_OFFSET_SHIFT + COMMON_RANGE_OFFSET;
const END_OFFSET_SHIFT: u32 = EID_OFFSET_SHIFT + 32;
const EID_OFFSET_SHIFT: u32 = VALUE_SHIFT + 64;
const LTYPE_SHIFT: u32 = OFFSET_SHIFT + u32::BITS;
const OFFSET_SHIFT: u32 = IS_MUTABLE_SHIFT + 1;
const IS_MUTABLE_SHIFT: u32 = EID_OFFSET_SHIFT + u32::BITS;
const EID_OFFSET_SHIFT: u32 = VALUE_SHIFT + u64::BITS;
const VALUE_SHIFT: u32 = 0;

assert_eq!(OFFSET_SHIFT, MEMORY_ADDRESS_OFFSET);
assert!(LTYPE_SHIFT + 8 <= INIT_MEMORY_ENCODE_BOUNDARY);

ltype * T::from_bn(&(1u64.to_biguint().unwrap() << LTYPE_SHIFT))
+ is_mutable * T::from_bn(&(1u64.to_biguint().unwrap() << IS_MUTABLE_SHIFT))
+ start_offset * T::from_bn(&(1u64.to_biguint().unwrap() << START_OFFSET_SHIFT))
+ end_offset * T::from_bn(&(1u64.to_biguint().unwrap() << END_OFFSET_SHIFT))
let encode = is_mutable * T::from_bn(&(1u64.to_biguint().unwrap() << IS_MUTABLE_SHIFT))
+ eid * T::from_bn(&(1u64.to_biguint().unwrap() << EID_OFFSET_SHIFT))
+ value
+ value;

if cfg!(feature = "continuation") {
encode
} else {
ltype * T::from_bn(&(1u64.to_biguint().unwrap() << LTYPE_SHIFT))
+ offset * T::from_bn(&(1u64.to_biguint().unwrap() << OFFSET_SHIFT))
+ encode
}
}

impl InitMemoryTableEntry {
pub fn encode(&self) -> BigUint {
encode_init_memory_table_entry(
BigUint::from(self.ltype as u32),
BigUint::from(self.offset),
BigUint::from(self.is_mutable as u32),
BigUint::from(self.start_offset),
BigUint::from(self.end_offset),
BigUint::from(self.eid),
self.value.to_biguint().unwrap(),
)
Expand Down
4 changes: 4 additions & 0 deletions crates/specs/src/etable.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,10 @@ impl EventTable {
Self(entries)
}

pub fn unwrap(self) -> Vec<EventTableEntry> {
self.0
}

pub fn entries(&self) -> &Vec<EventTableEntry> {
&self.0
}
Expand Down
142 changes: 13 additions & 129 deletions crates/specs/src/imtable.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
use std::cmp::Ordering;
use std::collections::BTreeMap;

use crate::mtable::LocationType;
Expand All @@ -9,151 +8,36 @@ use serde::Serialize;
pub struct InitMemoryTableEntry {
pub ltype: LocationType,
pub is_mutable: bool,
pub start_offset: u32,
pub end_offset: u32,
pub offset: u32,
pub vtype: VarType,
/// convert from [u8; 8] via u64::from_le_bytes
pub value: u64,
pub eid: u32,
}

#[derive(Serialize, Default, Debug, Clone)]
pub struct InitMemoryTable {
entries: Vec<InitMemoryTableEntry>,
sorted_global_init_entries: BTreeMap<u32, InitMemoryTableEntry>,
sorted_stack_init_entries: BTreeMap<u32, InitMemoryTableEntry>,
sorted_heap_init_entries: Vec<InitMemoryTableEntry>,
}
pub struct InitMemoryTable(pub BTreeMap<(LocationType, u32), InitMemoryTableEntry>);

impl InitMemoryTable {
pub fn new(mut entries: Vec<InitMemoryTableEntry>) -> Self {
fn sort(entries: &mut Vec<InitMemoryTableEntry>) {
entries.sort_by_key(|item| (item.ltype, item.start_offset));
}

fn merge(entries: Vec<InitMemoryTableEntry>) -> Vec<InitMemoryTableEntry> {
let mut merged_entries: Vec<_> = entries
.iter()
.filter(|entry| entry.ltype != LocationType::Heap)
.map(|entry| entry.clone())
.collect();

let heap_initial: Vec<_> = entries
.iter()
.filter(|entry| entry.ltype == LocationType::Heap)
.collect();

if !heap_initial.is_empty() {
let mut scan = 0;
let mut cursor = scan + 1;
while scan < heap_initial.len() && cursor < heap_initial.len() {
if heap_initial[scan].value == heap_initial[cursor].value
&& heap_initial[scan].eid == heap_initial[cursor].eid
{
cursor += 1;
} else {
merged_entries.push(InitMemoryTableEntry {
ltype: LocationType::Heap,
is_mutable: true,
start_offset: heap_initial[scan].start_offset,
end_offset: heap_initial[cursor - 1].end_offset,
vtype: VarType::I64,
value: heap_initial[scan].value,
eid: heap_initial[scan].eid,
});

scan = cursor;
cursor = scan + 1;
}
}
merged_entries.push(InitMemoryTableEntry {
ltype: LocationType::Heap,
is_mutable: true,
start_offset: heap_initial[scan].start_offset,
end_offset: heap_initial[cursor - 1].end_offset,
vtype: VarType::I64,
value: heap_initial[scan].value,
eid: heap_initial[scan].eid,
});
}
pub fn new(entries: Vec<InitMemoryTableEntry>) -> Self {
let mut map = BTreeMap::new();

merged_entries
}
entries.into_iter().for_each(|entry| {
map.insert((entry.ltype, entry.offset), entry);
});

sort(&mut entries);
let entries = merge(entries);

let sorted_heap_init_entries = entries
.iter()
.filter(|entry| entry.ltype == LocationType::Heap)
.map(|entry| entry.clone())
.collect();
let sorted_global_init_entries = entries
.iter()
.filter(|entry| entry.ltype == LocationType::Global)
.map(|entry| (entry.start_offset, entry.clone()))
.collect();
let sorted_stack_init_entries = entries
.iter()
.filter(|entry| entry.ltype == LocationType::Stack)
.map(|entry| (entry.start_offset, entry.clone()))
.collect();

InitMemoryTable {
entries,
sorted_global_init_entries,
sorted_stack_init_entries,
sorted_heap_init_entries,
}
Self(map)
}

pub fn entries(&self) -> &Vec<InitMemoryTableEntry> {
&self.entries
pub fn entries(&self) -> &BTreeMap<(LocationType, u32), InitMemoryTableEntry> {
&self.0
}

pub fn to_string(&self) -> String {
serde_json::to_string(&self.entries).unwrap()
}

pub fn try_find(&self, ltype: LocationType, offset: u32) -> Option<(u32, u32, u32, u64)> {
match ltype {
LocationType::Heap => {
let idx = self
.sorted_heap_init_entries
.binary_search_by(|entry| {
if offset >= entry.start_offset && offset <= entry.end_offset {
Ordering::Equal
} else if offset < entry.start_offset {
Ordering::Greater
} else {
Ordering::Less
}
})
.unwrap();

return Some((
self.sorted_heap_init_entries[idx].start_offset,
self.sorted_heap_init_entries[idx].end_offset,
self.sorted_heap_init_entries[idx].eid,
self.sorted_heap_init_entries[idx].value,
));
}
LocationType::Global => {
return self
.sorted_global_init_entries
.get(&offset)
.map(|entry| (entry.start_offset, entry.end_offset, entry.eid, entry.value));
}
LocationType::Stack => {
return self
.sorted_stack_init_entries
.get(&offset)
.map(|entry| (entry.start_offset, entry.end_offset, entry.eid, entry.value));
}
}
serde_json::to_string(&self.0).unwrap()
}

pub fn filter(&self, ltype: LocationType) -> Vec<&InitMemoryTableEntry> {
self.entries.iter().filter(|e| e.ltype == ltype).collect()
pub fn try_find(&self, ltype: LocationType, offset: u32) -> Option<&InitMemoryTableEntry> {
self.0.get(&(ltype, offset))
}
}
4 changes: 4 additions & 0 deletions crates/specs/src/jtable.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,10 @@
use super::itable::InstructionTableEntry;
use serde::Serialize;

// 1. jumps to zkmain
// 2. jumps to start(if exists)
pub const STATIC_FRAME_ENTRY_NUMBER: usize = 2;

#[derive(Default, Serialize, Debug, Clone)]
pub struct StaticFrameEntry {
pub enable: bool,
Expand Down
Loading
Loading