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

Feat/Aggregation VM STARK #76

Merged
merged 66 commits into from
Jun 25, 2024
Merged
Show file tree
Hide file tree
Changes from 47 commits
Commits
Show all changes
66 commits
Select commit Hold shift + click to select a range
ac1f18c
Create stark-vm crate
TlatoaniHJ Jun 18, 2024
aaf5c55
Add lib.rs, add afs-chips dependency, add CPU chip
TlatoaniHJ Jun 18, 2024
74f86d8
Make and use OpCode enum
TlatoaniHJ Jun 18, 2024
6698d7f
Refactor CPU tests
TlatoaniHJ Jun 18, 2024
b436471
Add program chip
TlatoaniHJ Jun 19, 2024
c8c6535
Actually add program chip
TlatoaniHJ Jun 19, 2024
13e7fd8
feat: imp arithmetic unit, minus tests
Jun 19, 2024
b73125c
chore: merge branch 'feat/vm' of github.com:axiom-crypto/afs-prototyp…
Jun 19, 2024
65c8d30
Use destructuring in cpu/air.rs
TlatoaniHJ Jun 19, 2024
33c40e8
Merge branch 'feat/vm' of https://github.com/axiom-crypto/afs-prototy…
TlatoaniHJ Jun 19, 2024
66d8057
Add negative test for CPU
TlatoaniHJ Jun 19, 2024
61ce20e
Reformat cpu and program
TlatoaniHJ Jun 19, 2024
c99b9df
chore: fix generate_trace, remove AUChip and replace with AUAir
Jun 20, 2024
f5080bf
Merge branch 'feat/vm' of github.com:axiom-crypto/afs-prototype into …
Jun 20, 2024
d09b186
Add explanations for test programs
TlatoaniHJ Jun 20, 2024
0a1dfaf
Merge branch 'feat/vm' of https://github.com/axiom-crypto/afs-prototy…
TlatoaniHJ Jun 20, 2024
d581205
chore: resolve conflict
bfan05 Jun 20, 2024
e8dbabf
Derive new for instruction
TlatoaniHJ Jun 20, 2024
2abdbcc
Merge branch 'feat/vm' of https://github.com/axiom-crypto/afs-prototy…
TlatoaniHJ Jun 20, 2024
d784145
chore: change Operation to MemoryAccess
bfan05 Jun 20, 2024
90a17d1
Align MemoryAccess with memory chip
TlatoaniHJ Jun 20, 2024
c956771
fix(au): width misalignment, incorrect trace generation
Jun 20, 2024
bd61350
Merge branch 'feat/vm' of github.com:axiom-crypto/afs-prototype into …
Jun 20, 2024
70e3730
fix(au bridge): positive tests run
Jun 20, 2024
5416c69
fix(trace): fix bug in AUCols::new, add negative tests
Jun 20, 2024
684dc4f
chore: rename AUAir -> FieldArithmeticAir, remove AUChip
Jun 20, 2024
6f907f6
Add terminate instruction
TlatoaniHJ Jun 20, 2024
e7f1846
chore: un-expand constraints using AB::Expr::one()
Jun 20, 2024
106e1c0
Address some zlangley comments
TlatoaniHJ Jun 20, 2024
892628c
docs(au)
Jun 20, 2024
578bbf4
Commit zlangley suggestion
TlatoaniHJ Jun 20, 2024
8b8cb47
merge: Merge branch 'feat/vm' of github.com:axiom-crypto/afs-prototyp…
Jun 20, 2024
d8d2fc6
Commit zlangley suggestion
TlatoaniHJ Jun 20, 2024
68a16e5
Merge branch 'feat/vm' of github.com:axiom-crypto/afs-prototype into …
Jun 20, 2024
c53d5a9
Make inst_width.clone() unnecessary
TlatoaniHJ Jun 20, 2024
526b7c7
Address zlangley comment
TlatoaniHJ Jun 20, 2024
d829bc0
Rename as_b, as_c to d, e
TlatoaniHJ Jun 20, 2024
f3990b9
feat: Memory op interactions
bfan05 Jun 20, 2024
5955589
Add negative test for termination check
TlatoaniHJ Jun 20, 2024
7bdbd00
Merge branch 'feat/vm' of https://github.com/axiom-crypto/afs-prototy…
TlatoaniHJ Jun 20, 2024
ea4e33d
Add failing test for secret write vulnerability
TlatoaniHJ Jun 20, 2024
7ed127c
Add failing test for disable write vulnerability
TlatoaniHJ Jun 20, 2024
754643e
Add failing test for disable read vulnerability
TlatoaniHJ Jun 20, 2024
534e322
Check access enabled in AIR
TlatoaniHJ Jun 20, 2024
365d694
Actually fix access enabled check
TlatoaniHJ Jun 20, 2024
f783a5c
Simplify cpu/tests/mod.rs
TlatoaniHJ Jun 20, 2024
821e7bc
Don't mock arithmetic chip when testing with is_field_arithmetic = false
TlatoaniHJ Jun 20, 2024
b4f59bc
chore: add test for invalid read
bfan05 Jun 20, 2024
becd9a6
Attempt to write integration test
TlatoaniHJ Jun 20, 2024
cdb3662
Merge branch 'feat/vm' of https://github.com/axiom-crypto/afs-prototy…
TlatoaniHJ Jun 20, 2024
f7f9d47
Conditionally use arith chip in integration test
TlatoaniHJ Jun 20, 2024
7c4e59b
Fix integration test wrt range checker
TlatoaniHJ Jun 20, 2024
88aacf8
Lint
TlatoaniHJ Jun 21, 2024
d46bcf9
Use unique memory timestamp instead of clock cycle
TlatoaniHJ Jun 24, 2024
d5ebe91
chore: rename MemoryAccess clock field to timestamp
bfan05 Jun 24, 2024
73d479d
feat: fp4_extension chip for addition and subtraction
bfan05 Jun 24, 2024
55dda4c
CPU -> Cpu
TlatoaniHJ Jun 24, 2024
7fe9be5
Use FieldArithmeticAir::solve
TlatoaniHJ Jun 24, 2024
0ff4796
Rename CpuChip::generate_trace to generate_program_execution
TlatoaniHJ Jun 24, 2024
af4bd54
feat: field extension multiplication
bfan05 Jun 24, 2024
893b1ae
Change field arithmetic address space
TlatoaniHJ Jun 24, 2024
655ff3b
chore: revert field extension changes
bfan05 Jun 25, 2024
2dc6375
Rename au directory to field_arithmetic, use super instead of crate::…
TlatoaniHJ Jun 25, 2024
5f86912
Addressed zlangley comments on memory
TlatoaniHJ Jun 25, 2024
39be7cf
Move arithmetic col generation to trace.rs
TlatoaniHJ Jun 25, 2024
0765fff
Fix lint
zlangley Jun 25, 2024
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
1 change: 1 addition & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ members = [
"test-utils",
"derive",
"logical-interface",
"vm",
]
resolver = "2"

Expand Down
20 changes: 20 additions & 0 deletions chips/src/is_equal/columns.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,17 @@ pub struct IsEqualAuxCols<T> {
pub inv: T,
}

impl<T: Clone> IsEqualAuxCols<T> {
pub fn from_slice(slc: &[T]) -> IsEqualAuxCols<T> {
IsEqualAuxCols {
inv: slc[0].clone(),
}
}

pub fn flatten(&self) -> Vec<T> {
vec![self.inv.clone()]
}
}
impl<T: Clone> IsEqualCols<T> {
pub const fn new(x: T, y: T, is_equal: T, inv: T) -> IsEqualCols<T> {
IsEqualCols {
Expand All @@ -38,6 +49,15 @@ impl<T: Clone> IsEqualCols<T> {
IsEqualCols::new(x, y, is_equal, inv)
}

pub fn flatten(&self) -> Vec<T> {
vec![
self.io.x.clone(),
self.io.y.clone(),
self.io.is_equal.clone(),
self.aux.inv.clone(),
]
}

pub fn get_width() -> usize {
NUM_COLS
}
Expand Down
49 changes: 49 additions & 0 deletions vm/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
[package]
name = "stark-vm"
version.workspace = true
authors.workspace = true
edition.workspace = true
description = "Aggregation VM STARK"

[dependencies]
p3-air = { workspace = true }
p3-baby-bear = { workspace = true, optional = true }
p3-commit = { workspace = true }
p3-field = { workspace = true }
p3-keccak = { workspace = true }
p3-keccak-air = { workspace = true }
p3-matrix = { workspace = true }
p3-maybe-rayon = { workspace = true }
p3-symmetric = { workspace = true }
p3-util = { workspace = true }
p3-uni-stark = { workspace = true }
rand = "0.8"

afs-chips = { path = "../chips" }
afs-stark-backend = { path = "../stark-backend" }
afs-derive = { path = "../derive" }
afs-test-utils = { path = "../test-utils" }
parking_lot = "0.12.2"
tracing = "0.1.40"
itertools = "0.13.0"
getset = "0.1.2"
derive-new = "0.5.1"

[dev-dependencies]
p3-uni-stark = { workspace = true }
p3-baby-bear = { workspace = true }
p3-challenger = { workspace = true }
p3-dft = { workspace = true }
p3-fri = { workspace = true }
p3-goldilocks = { workspace = true }
p3-keccak = { workspace = true }
p3-merkle-tree = { workspace = true }
p3-poseidon2 = { workspace = true }
p3-symmetric = { workspace = true }
tracing-subscriber = { version = "0.3.17", features = ["std", "env-filter"] }
tracing-forest = { version = "0.1.6", features = ["ansi", "smallvec"] }
test-case = "3.3.1"

[features]
default = ["test-traits"]
test-traits = ["p3-baby-bear"]
59 changes: 59 additions & 0 deletions vm/src/au/air.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
use std::borrow::Borrow;
TlatoaniHJ marked this conversation as resolved.
Show resolved Hide resolved

use p3_air::{Air, AirBuilder, BaseAir};
use p3_field::{AbstractField, Field};
use p3_matrix::Matrix;

use super::{columns::FieldArithmeticCols, FieldArithmeticAir};
use afs_chips::sub_chip::AirConfig;

impl AirConfig for FieldArithmeticAir {
type Cols<T> = FieldArithmeticCols<T>;
}

impl<F: Field> BaseAir<F> for FieldArithmeticAir {
fn width(&self) -> usize {
FieldArithmeticCols::<F>::NUM_COLS
}
}

impl<AB: AirBuilder> Air<AB> for FieldArithmeticAir {
fn eval(&self, builder: &mut AB) {
let main = builder.main();

let local = main.row_slice(0);
let au_cols: &FieldArithmeticCols<_> = (*local).borrow();

let FieldArithmeticCols { io, aux } = au_cols;

builder.assert_bool(aux.opcode_lo);
builder.assert_bool(aux.opcode_hi);

builder.assert_eq(
io.opcode,
aux.opcode_lo
+ aux.opcode_hi * AB::Expr::two()
+ AB::F::from_canonical_u8(FieldArithmeticAir::BASE_OP),
);

builder.assert_eq(
aux.is_mul,
aux.opcode_hi * (AB::Expr::one() - aux.opcode_lo),
);
builder.assert_eq(aux.is_div, aux.opcode_hi * aux.opcode_lo);

builder.assert_eq(aux.product, io.x * io.y);
builder.assert_eq(aux.quotient * io.y, io.x);
builder.assert_eq(
au_cols.aux.sum_or_diff,
io.x + io.y - AB::Expr::two() * aux.opcode_lo * io.y,
);

builder.assert_eq(
io.z,
aux.is_mul * aux.product
+ aux.is_div * aux.quotient
+ aux.sum_or_diff * (AB::Expr::one() - aux.opcode_hi),
);
}
}
18 changes: 18 additions & 0 deletions vm/src/au/bridge.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
use afs_stark_backend::interaction::{AirBridge, Interaction};
use p3_air::VirtualPairCol;
use p3_field::Field;

use crate::au::{columns::FieldArithmeticCols, FieldArithmeticAir};

/// Receives all IO columns from another chip on bus 2 (FieldArithmeticAir::BUS_INDEX).
impl<T: Field> AirBridge<T> for FieldArithmeticAir {
fn receives(&self) -> Vec<Interaction<T>> {
vec![Interaction {
fields: (0..FieldArithmeticCols::<T>::NUM_IO_COLS)
.map(VirtualPairCol::single_main)
.collect(),
count: VirtualPairCol::one(),
argument_index: Self::BUS_INDEX,
}]
}
}
117 changes: 117 additions & 0 deletions vm/src/au/columns.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,117 @@
use crate::cpu::OpCode;
use afs_derive::AlignedBorrow;
use p3_field::Field;

use crate::au::FieldArithmeticAir;

/// Columns for field arithmetic chip.
///
/// Four IO columns for opcode, x, y, result.
/// Seven aux columns for interpreting opcode, evaluating indicators, and explicit computations.
#[derive(AlignedBorrow)]
pub struct FieldArithmeticCols<T> {
pub io: FieldArithmeticIOCols<T>,
pub aux: FieldArithmeticAuxCols<T>,
}

pub struct FieldArithmeticIOCols<T> {
pub opcode: T,
pub x: T,
pub y: T,
pub z: T,
}

pub struct FieldArithmeticAuxCols<T> {
pub opcode_lo: T,
pub opcode_hi: T,
pub is_mul: T,
pub is_div: T,
pub sum_or_diff: T,
pub product: T,
pub quotient: T,
}

impl<T> FieldArithmeticCols<T>
where
T: Field,
{
pub const NUM_COLS: usize = 11;
pub const NUM_IO_COLS: usize = 4;
pub const NUM_AUX_COLS: usize = 6;

/// Constructs a new set of columns (including auxiliary columns) given inputs.
pub fn new(op: OpCode, x: T, y: T) -> Self {
let opcode = op as u32;
let opcode_value = opcode - FieldArithmeticAir::BASE_OP as u32;
let opcode_lo_u32 = opcode_value % 2;
let opcode_hi_u32 = opcode_value / 2;
let opcode_lo = T::from_canonical_u32(opcode_lo_u32);
let opcode_hi = T::from_canonical_u32(opcode_hi_u32);
let is_div = T::from_bool(op == OpCode::FDIV);
let is_mul = T::from_bool(op == OpCode::FMUL);
let sum_or_diff = x + y - T::two() * opcode_lo * y;
let product = x * y;
let quotient = if y == T::zero() {
T::zero()
} else {
x * y.inverse()
};
let z = is_mul * product + is_div * quotient + (T::one() - opcode_hi) * sum_or_diff;
TlatoaniHJ marked this conversation as resolved.
Show resolved Hide resolved

Self {
io: FieldArithmeticIOCols {
opcode: T::from_canonical_u32(opcode),
x,
y,
z,
},
aux: FieldArithmeticAuxCols {
opcode_lo,
opcode_hi,
is_mul,
is_div,
sum_or_diff,
product,
quotient,
},
}
}

pub fn get_width() -> usize {
FieldArithmeticIOCols::<T>::get_width() + FieldArithmeticAuxCols::<T>::get_width()
}

pub fn flatten(&self) -> Vec<T> {
let mut result = self.io.flatten();
result.extend(self.aux.flatten());
result
}
}

impl<T: Field> FieldArithmeticIOCols<T> {
pub fn get_width() -> usize {
4
}

pub fn flatten(&self) -> Vec<T> {
vec![self.opcode, self.x, self.y, self.z]
}
}

impl<T: Field> FieldArithmeticAuxCols<T> {
pub fn get_width() -> usize {
7
}

pub fn flatten(&self) -> Vec<T> {
vec![
self.opcode_lo,
self.opcode_hi,
self.is_mul,
self.is_div,
self.sum_or_diff,
self.product,
self.quotient,
]
}
}
69 changes: 69 additions & 0 deletions vm/src/au/mod.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,69 @@
use super::cpu::trace::ArithmeticOperation;
use crate::cpu::OpCode;
use p3_field::Field;

#[cfg(test)]
pub mod tests;

pub mod air;
pub mod bridge;
pub mod columns;
pub mod trace;

/// Field arithmetic chip.
///
/// Carries information about opcodes (currently 5..=8) and bus index (currently 2).
#[derive(Default, Clone, Copy)]
pub struct FieldArithmeticAir {}

impl FieldArithmeticAir {
pub const BASE_OP: u8 = 6;
pub const BUS_INDEX: usize = 2;

pub fn new() -> Self {
Self {}
}

/// Evaluates given opcode using given operands.
///
/// Returns None for non-arithmetic operations.
pub fn solve<T: Field>(op: OpCode, operands: (T, T)) -> Option<T> {
match op {
OpCode::LOADW => None,
OpCode::STOREW => None,
OpCode::JAL => None,
OpCode::BEQ => None,
OpCode::BNE => None,
OpCode::TERMINATE => None,
TlatoaniHJ marked this conversation as resolved.
Show resolved Hide resolved

OpCode::FADD => Some(operands.0 + operands.1),
OpCode::FSUB => Some(operands.0 - operands.1),
OpCode::FMUL => Some(operands.0 * operands.1),
OpCode::FDIV => Some(operands.0 / operands.1),
}
}

/// Vectorized solve<>
pub fn solve_all<T: Field>(ops: Vec<OpCode>, operands: Vec<(T, T)>) -> Vec<T> {
ops.iter()
.zip(operands.iter())
.filter_map(|(op, operand)| Self::solve::<T>(*op, *operand))
.collect()
}

/// Converts vectorized opcodes and operands into vectorized ArithmeticOperations.
pub fn request<T: Field>(
ops: Vec<OpCode>,
operands: Vec<(T, T)>,
) -> Vec<ArithmeticOperation<T>> {
ops.iter()
.zip(operands.iter())
.map(|(op, operand)| ArithmeticOperation {
opcode: *op,
operand1: operand.0,
operand2: operand.1,
result: Self::solve::<T>(*op, *operand).unwrap(),
})
.collect()
}
}
Loading
Loading