Skip to content

Commit 13036e7

Browse files
authored
feat: constrain address spaces in native extension (#1305)
* feat: constrain native adapters to only access AS 0, 2, 4 * feat: constrain address spaces in native ALU * fix: update some tests * fix: lint * fix: test * fix: make test ranges disjoint * chore: remove magic numbers * fix: import * feat: allow e, f to be any address space in kernels * feat: remove tests on kernel guest macro * fix: remove deleted crate
1 parent b758220 commit 13036e7

34 files changed

+378
-860
lines changed

Cargo.lock

Lines changed: 0 additions & 31 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,8 +36,6 @@ members = [
3636
"extensions/native/compiler/derive",
3737
"extensions/native/recursion",
3838
"extensions/native/transpiler",
39-
"extensions/native/tests",
40-
"extensions/native/tests/guest-macro",
4139
"extensions/algebra/circuit",
4240
"extensions/algebra/transpiler",
4341
"extensions/algebra/guest",

docs/specs/ISA.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -281,7 +281,7 @@ The RV32IM extension defines the following phantom sub-instructions.
281281

282282
### Native Extension
283283

284-
The native extension operates over native field elements and has instructions tailored for STARK proof recursion. It operates over address spaces `0` and `4`, and does not constrain memory elements to be bytes.
284+
The native extension operates over native field elements and has instructions tailored for STARK proof recursion. It does not constrain memory elements to be bytes and most instructions only write to address space `4`, with the notable exception of CASTF.
285285

286286
#### Base
287287

@@ -304,7 +304,7 @@ reads but not allowed for writes. When using immediates, we interpret `[a]_0` as
304304

305305
#### Field Arithmetic
306306

307-
This instruction set does native field operations. Below, `e,f` may be either `0` or `4`.
307+
This instruction set does native field operations. Below, `e,f` may be any address space.
308308
When either `e` or `f` is zero, `[b]_0` and `[c]_0` should be interpreted as the immediates `b`
309309
and `c`, respectively.
310310

Lines changed: 231 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,231 @@
1+
use std::{
2+
borrow::{Borrow, BorrowMut},
3+
marker::PhantomData,
4+
};
5+
6+
use openvm_circuit::{
7+
arch::{
8+
AdapterAirContext, AdapterRuntimeContext, BasicAdapterInterface, ExecutionBridge,
9+
ExecutionBus, ExecutionState, MinimalInstruction, Result, VmAdapterAir, VmAdapterChip,
10+
VmAdapterInterface,
11+
},
12+
system::{
13+
memory::{
14+
offline_checker::{MemoryBridge, MemoryReadOrImmediateAuxCols, MemoryWriteAuxCols},
15+
MemoryAddress, MemoryController, OfflineMemory,
16+
},
17+
native_adapter::{NativeReadRecord, NativeWriteRecord},
18+
program::ProgramBus,
19+
},
20+
};
21+
use openvm_circuit_primitives_derive::AlignedBorrow;
22+
use openvm_instructions::{instruction::Instruction, program::DEFAULT_PC_STEP};
23+
use openvm_native_compiler::conversion::AS;
24+
use openvm_stark_backend::{
25+
interaction::InteractionBuilder,
26+
p3_air::BaseAir,
27+
p3_field::{Field, FieldAlgebra, PrimeField32},
28+
};
29+
30+
#[derive(Debug)]
31+
pub struct AluNativeAdapterChip<F: Field> {
32+
pub air: AluNativeAdapterAir,
33+
_marker: PhantomData<F>,
34+
}
35+
36+
impl<F: PrimeField32> AluNativeAdapterChip<F> {
37+
pub fn new(
38+
execution_bus: ExecutionBus,
39+
program_bus: ProgramBus,
40+
memory_bridge: MemoryBridge,
41+
) -> Self {
42+
Self {
43+
air: AluNativeAdapterAir {
44+
execution_bridge: ExecutionBridge::new(execution_bus, program_bus),
45+
memory_bridge,
46+
},
47+
_marker: PhantomData,
48+
}
49+
}
50+
}
51+
52+
#[repr(C)]
53+
#[derive(AlignedBorrow)]
54+
pub struct AluNativeAdapterCols<T> {
55+
pub from_state: ExecutionState<T>,
56+
pub a_pointer: T,
57+
pub b_pointer: T,
58+
pub c_pointer: T,
59+
pub e_as: T,
60+
pub f_as: T,
61+
pub reads_aux: [MemoryReadOrImmediateAuxCols<T>; 2],
62+
pub write_aux: MemoryWriteAuxCols<T, 1>,
63+
}
64+
65+
#[derive(Clone, Copy, Debug, derive_new::new)]
66+
pub struct AluNativeAdapterAir {
67+
pub(super) execution_bridge: ExecutionBridge,
68+
pub(super) memory_bridge: MemoryBridge,
69+
}
70+
71+
impl<F: Field> BaseAir<F> for AluNativeAdapterAir {
72+
fn width(&self) -> usize {
73+
AluNativeAdapterCols::<F>::width()
74+
}
75+
}
76+
77+
impl<AB: InteractionBuilder> VmAdapterAir<AB> for AluNativeAdapterAir {
78+
type Interface = BasicAdapterInterface<AB::Expr, MinimalInstruction<AB::Expr>, 2, 1, 1, 1>;
79+
80+
fn eval(
81+
&self,
82+
builder: &mut AB,
83+
local: &[AB::Var],
84+
ctx: AdapterAirContext<AB::Expr, Self::Interface>,
85+
) {
86+
let cols: &AluNativeAdapterCols<_> = local.borrow();
87+
let timestamp = cols.from_state.timestamp;
88+
let mut timestamp_delta = 0usize;
89+
let mut timestamp_pp = || {
90+
timestamp_delta += 1;
91+
timestamp + AB::F::from_canonical_usize(timestamp_delta - 1)
92+
};
93+
94+
let native_as = AB::Expr::from_canonical_u32(AS::Native as u32);
95+
96+
self.memory_bridge
97+
.read_or_immediate(
98+
MemoryAddress::new(cols.e_as, cols.b_pointer),
99+
ctx.reads[0][0].clone(),
100+
timestamp_pp(),
101+
&cols.reads_aux[0],
102+
)
103+
.eval(builder, ctx.instruction.is_valid.clone());
104+
105+
self.memory_bridge
106+
.read_or_immediate(
107+
MemoryAddress::new(cols.f_as, cols.c_pointer),
108+
ctx.reads[1][0].clone(),
109+
timestamp_pp(),
110+
&cols.reads_aux[1],
111+
)
112+
.eval(builder, ctx.instruction.is_valid.clone());
113+
114+
self.memory_bridge
115+
.write(
116+
MemoryAddress::new(native_as.clone(), cols.a_pointer),
117+
ctx.writes[0].clone(),
118+
timestamp_pp(),
119+
&cols.write_aux,
120+
)
121+
.eval(builder, ctx.instruction.is_valid.clone());
122+
123+
self.execution_bridge
124+
.execute_and_increment_or_set_pc(
125+
ctx.instruction.opcode,
126+
[
127+
cols.a_pointer.into(),
128+
cols.b_pointer.into(),
129+
cols.c_pointer.into(),
130+
native_as.clone(),
131+
cols.e_as.into(),
132+
cols.f_as.into(),
133+
],
134+
cols.from_state,
135+
AB::F::from_canonical_usize(timestamp_delta),
136+
(DEFAULT_PC_STEP, ctx.to_pc),
137+
)
138+
.eval(builder, ctx.instruction.is_valid);
139+
}
140+
141+
fn get_from_pc(&self, local: &[AB::Var]) -> AB::Var {
142+
let cols: &AluNativeAdapterCols<_> = local.borrow();
143+
cols.from_state.pc
144+
}
145+
}
146+
147+
impl<F: PrimeField32> VmAdapterChip<F> for AluNativeAdapterChip<F> {
148+
type ReadRecord = NativeReadRecord<F, 2>;
149+
type WriteRecord = NativeWriteRecord<F, 1>;
150+
type Air = AluNativeAdapterAir;
151+
type Interface = BasicAdapterInterface<F, MinimalInstruction<F>, 2, 1, 1, 1>;
152+
153+
fn preprocess(
154+
&mut self,
155+
memory: &mut MemoryController<F>,
156+
instruction: &Instruction<F>,
157+
) -> Result<(
158+
<Self::Interface as VmAdapterInterface<F>>::Reads,
159+
Self::ReadRecord,
160+
)> {
161+
let Instruction { b, c, e, f, .. } = *instruction;
162+
163+
let reads = vec![memory.read::<1>(e, b), memory.read::<1>(f, c)];
164+
let i_reads: [_; 2] = std::array::from_fn(|i| reads[i].1);
165+
166+
Ok((
167+
i_reads,
168+
Self::ReadRecord {
169+
reads: reads.try_into().unwrap(),
170+
},
171+
))
172+
}
173+
174+
fn postprocess(
175+
&mut self,
176+
memory: &mut MemoryController<F>,
177+
_instruction: &Instruction<F>,
178+
from_state: ExecutionState<u32>,
179+
output: AdapterRuntimeContext<F, Self::Interface>,
180+
_read_record: &Self::ReadRecord,
181+
) -> Result<(ExecutionState<u32>, Self::WriteRecord)> {
182+
let Instruction { a, .. } = *_instruction;
183+
let writes = vec![memory.write(
184+
F::from_canonical_u32(AS::Native as u32),
185+
a,
186+
output.writes[0],
187+
)];
188+
189+
Ok((
190+
ExecutionState {
191+
pc: output.to_pc.unwrap_or(from_state.pc + DEFAULT_PC_STEP),
192+
timestamp: memory.timestamp(),
193+
},
194+
Self::WriteRecord {
195+
from_state,
196+
writes: writes.try_into().unwrap(),
197+
},
198+
))
199+
}
200+
201+
fn generate_trace_row(
202+
&self,
203+
row_slice: &mut [F],
204+
read_record: Self::ReadRecord,
205+
write_record: Self::WriteRecord,
206+
memory: &OfflineMemory<F>,
207+
) {
208+
let row_slice: &mut AluNativeAdapterCols<_> = row_slice.borrow_mut();
209+
let aux_cols_factory = memory.aux_cols_factory();
210+
211+
row_slice.from_state = write_record.from_state.map(F::from_canonical_u32);
212+
213+
row_slice.a_pointer = memory.record_by_id(write_record.writes[0].0).pointer;
214+
row_slice.b_pointer = memory.record_by_id(read_record.reads[0].0).pointer;
215+
row_slice.c_pointer = memory.record_by_id(read_record.reads[1].0).pointer;
216+
row_slice.e_as = memory.record_by_id(read_record.reads[0].0).address_space;
217+
row_slice.f_as = memory.record_by_id(read_record.reads[1].0).address_space;
218+
219+
for (i, x) in read_record.reads.iter().enumerate() {
220+
let read = memory.record_by_id(x.0);
221+
aux_cols_factory.generate_read_or_immediate_aux(read, &mut row_slice.reads_aux[i]);
222+
}
223+
224+
let write = memory.record_by_id(write_record.writes[0].0);
225+
aux_cols_factory.generate_write_aux(write, &mut row_slice.write_aux);
226+
}
227+
228+
fn air(&self) -> &Self::Air {
229+
&self.air
230+
}
231+
}

extensions/native/circuit/src/adapters/branch_native_adapter.rs

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ use openvm_circuit::{
2020
};
2121
use openvm_circuit_primitives_derive::AlignedBorrow;
2222
use openvm_instructions::{instruction::Instruction, program::DEFAULT_PC_STEP};
23+
use openvm_native_compiler::conversion::AS;
2324
use openvm_stark_backend::{
2425
interaction::InteractionBuilder,
2526
p3_air::BaseAir,
@@ -91,6 +92,18 @@ impl<AB: InteractionBuilder> VmAdapterAir<AB> for BranchNativeAdapterAir {
9192
timestamp + AB::F::from_canonical_usize(timestamp_delta - 1)
9293
};
9394

95+
// check that d and e are in {0, 4}
96+
let d = cols.reads_aux[0].address.address_space;
97+
let e = cols.reads_aux[1].address.address_space;
98+
builder.assert_eq(
99+
d * (d - AB::F::from_canonical_u32(AS::Native as u32)),
100+
AB::F::ZERO,
101+
);
102+
builder.assert_eq(
103+
e * (e - AB::F::from_canonical_u32(AS::Native as u32)),
104+
AB::F::ZERO,
105+
);
106+
94107
self.memory_bridge
95108
.read_or_immediate(
96109
cols.reads_aux[0].address,

extensions/native/circuit/src/adapters/convert_adapter.rs

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ use openvm_circuit::{
1919
};
2020
use openvm_circuit_primitives_derive::AlignedBorrow;
2121
use openvm_instructions::{instruction::Instruction, program::DEFAULT_PC_STEP};
22+
use openvm_native_compiler::conversion::AS;
2223
use openvm_stark_backend::{
2324
interaction::InteractionBuilder,
2425
p3_air::BaseAir,
@@ -70,8 +71,6 @@ pub struct ConvertAdapterCols<T, const READ_SIZE: usize, const WRITE_SIZE: usize
7071
pub from_state: ExecutionState<T>,
7172
pub a_pointer: T,
7273
pub b_pointer: T,
73-
pub a_as: T,
74-
pub b_as: T,
7574
pub writes_aux: [MemoryWriteAuxCols<T, WRITE_SIZE>; 1],
7675
pub reads_aux: [MemoryReadAuxCols<T>; 1],
7776
}
@@ -110,9 +109,12 @@ impl<AB: InteractionBuilder, const READ_SIZE: usize, const WRITE_SIZE: usize> Vm
110109
timestamp + AB::F::from_canonical_usize(timestamp_delta - 1)
111110
};
112111

112+
let d = AB::Expr::TWO;
113+
let e = AB::Expr::from_canonical_u32(AS::Native as u32);
114+
113115
self.memory_bridge
114116
.read(
115-
MemoryAddress::new(cols.b_as, cols.b_pointer),
117+
MemoryAddress::new(e.clone(), cols.b_pointer),
116118
ctx.reads[0].clone(),
117119
timestamp_pp(),
118120
&cols.reads_aux[0],
@@ -121,7 +123,7 @@ impl<AB: InteractionBuilder, const READ_SIZE: usize, const WRITE_SIZE: usize> Vm
121123

122124
self.memory_bridge
123125
.write(
124-
MemoryAddress::new(cols.a_as, cols.a_pointer),
126+
MemoryAddress::new(d.clone(), cols.a_pointer),
125127
ctx.writes[0].clone(),
126128
timestamp_pp(),
127129
&cols.writes_aux[0],
@@ -135,8 +137,8 @@ impl<AB: InteractionBuilder, const READ_SIZE: usize, const WRITE_SIZE: usize> Vm
135137
cols.a_pointer.into(),
136138
cols.b_pointer.into(),
137139
AB::Expr::ZERO,
138-
cols.a_as.into(),
139-
cols.b_as.into(),
140+
d,
141+
e,
140142
],
141143
cols.from_state,
142144
AB::F::from_canonical_usize(timestamp_delta),
@@ -212,9 +214,7 @@ impl<F: PrimeField32, const READ_SIZE: usize, const WRITE_SIZE: usize> VmAdapter
212214

213215
row_slice.from_state = write_record.from_state.map(F::from_canonical_u32);
214216
row_slice.a_pointer = write.pointer;
215-
row_slice.a_as = write.address_space;
216217
row_slice.b_pointer = read.pointer;
217-
row_slice.b_as = read.address_space;
218218

219219
aux_cols_factory.generate_read_aux(read, &mut row_slice.reads_aux[0]);
220220
aux_cols_factory.generate_write_aux(write, &mut row_slice.writes_aux[0]);

0 commit comments

Comments
 (0)