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

Static chip preprocessed trace #142

Draft
wants to merge 26 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
26 commits
Select commit Hold shift + click to select a range
c2b4bfb
wip: static data chip: using a preprocessed trace
morganthomas Apr 5, 2024
656e2e2
Merge branch 'morgan/issue/133' of github.com:valida-xyz/valida into …
morganthomas Apr 5, 2024
1d9ecf9
wip: preprocessed traces
morganthomas Apr 6, 2024
f9f6bac
issue/143: duplicate basic crate
morganthomas Apr 6, 2024
7bb573f
issue/143: remove macros from basic machine
morganthomas Apr 6, 2024
c13fadf
issue/143: wip: de-macroify run
morganthomas Apr 6, 2024
ac02d95
issue/143: wip: de-macroify prove
morganthomas Apr 6, 2024
5c90dd1
issue/143: wip: de-macroify verify
morganthomas Apr 6, 2024
b71d2ae
issue/143: bugfixes
morganthomas Apr 6, 2024
1c51e9c
issue/143: cargo fmt
morganthomas Apr 6, 2024
4e16400
issue/143: remove no_std from basic_macro lib (is breaking ci?)
morganthomas Apr 6, 2024
93678d9
Merge branch 'main' into morgan/issue/143
morganthomas Apr 8, 2024
8314901
issue/143: fix merge
morganthomas Apr 9, 2024
125b33b
issue/143: cargo fmt
morganthomas Apr 9, 2024
982a157
Merge branch 'morgan/issue/143' into morgan/issue/140
morganthomas Apr 9, 2024
d61efe8
issue/140: fix merge of morgan/issue/143
morganthomas Apr 9, 2024
15c4c2f
issue/140: wip: bugfix static data chip
morganthomas Apr 9, 2024
28c147a
issue/140: wip: bugfix static data chip
morganthomas Apr 10, 2024
f115fe8
issue/140: more specific failures to verify
morganthomas Apr 11, 2024
77fae7b
issue/140: wip: bugfix preprocessed stuff
morganthomas Apr 11, 2024
11c2bed
issue/140: wip: bugfix preprocessed stuff
morganthomas Apr 11, 2024
35ce1c0
issue/140: wip: bugfix preprocessed stuff
morganthomas Apr 12, 2024
0cadb44
issue/140: wip: bugfix preprocessed stuff
morganthomas Apr 12, 2024
c1a47a0
issue/140: wip: bugfix preprocessed stuff
morganthomas Apr 12, 2024
6dc4511
issue/140: add a redundant check of the preprocessed commitment (for …
morganthomas Apr 14, 2024
c0a0abe
issue/140: wip: un-batch the opening proofs to figure out which one i…
morganthomas Apr 15, 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
505 changes: 475 additions & 30 deletions Cargo.lock

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ members = [
"assembler",
"alu_u32",
"basic",
# "basic_macro",
"bus",
"cpu",
"derive",
Expand Down
4 changes: 2 additions & 2 deletions alu_u32/src/add/stark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,10 @@ use core::borrow::Borrow;

use crate::add::columns::NUM_ADD_COLS;
use p3_air::{Air, AirBuilder, BaseAir};
use p3_field::PrimeField;
use p3_field::{AbstractField, PrimeField};
use p3_matrix::MatrixRowSlices;

impl<F> BaseAir<F> for Add32Chip {
impl<F: AbstractField> BaseAir<F> for Add32Chip {
fn width(&self) -> usize {
NUM_ADD_COLS
}
Expand Down
2 changes: 1 addition & 1 deletion alu_u32/src/bitwise/stark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ use p3_air::{Air, AirBuilder, BaseAir};
use p3_field::AbstractField;
use p3_matrix::MatrixRowSlices;

impl<F> BaseAir<F> for Bitwise32Chip {
impl<F: AbstractField> BaseAir<F> for Bitwise32Chip {
fn width(&self) -> usize {
NUM_BITWISE_COLS
}
Expand Down
2 changes: 1 addition & 1 deletion alu_u32/src/com/stark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use p3_air::{Air, AirBuilder, BaseAir};
use p3_field::AbstractField;
use p3_matrix::MatrixRowSlices;

impl<F> BaseAir<F> for Com32Chip {
impl<F: AbstractField> BaseAir<F> for Com32Chip {
fn width(&self) -> usize {
NUM_COM_COLS
}
Expand Down
4 changes: 2 additions & 2 deletions alu_u32/src/div/stark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@ use super::Div32Chip;

use crate::div::columns::NUM_DIV_COLS;
use p3_air::{Air, AirBuilder, BaseAir};
use p3_field::PrimeField;
use p3_field::{AbstractField, PrimeField};

impl<F> BaseAir<F> for Div32Chip {
impl<F: AbstractField> BaseAir<F> for Div32Chip {
fn width(&self) -> usize {
NUM_DIV_COLS
}
Expand Down
2 changes: 1 addition & 1 deletion alu_u32/src/lt/stark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use p3_air::{Air, AirBuilder, BaseAir};
use p3_field::AbstractField;
use p3_matrix::MatrixRowSlices;

impl<F> BaseAir<F> for Lt32Chip {
impl<F: AbstractField> BaseAir<F> for Lt32Chip {
fn width(&self) -> usize {
NUM_LT_COLS
}
Expand Down
2 changes: 1 addition & 1 deletion alu_u32/src/mul/stark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use p3_air::{Air, AirBuilder, BaseAir};
use p3_field::{AbstractField, PrimeField};
use p3_matrix::MatrixRowSlices;

impl<F> BaseAir<F> for Mul32Chip {
impl<F: AbstractField> BaseAir<F> for Mul32Chip {
fn width(&self) -> usize {
NUM_MUL_COLS
}
Expand Down
2 changes: 1 addition & 1 deletion alu_u32/src/shift/stark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use p3_air::{Air, AirBuilder, BaseAir};
use p3_field::AbstractField;
use p3_matrix::MatrixRowSlices;

impl<F> BaseAir<F> for Shift32Chip {
impl<F: AbstractField> BaseAir<F> for Shift32Chip {
fn width(&self) -> usize {
NUM_SHIFT_COLS
}
Expand Down
2 changes: 1 addition & 1 deletion alu_u32/src/sub/stark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use p3_air::{Air, AirBuilder, BaseAir};
use p3_field::{AbstractField, PrimeField};
use p3_matrix::MatrixRowSlices;

impl<F> BaseAir<F> for Sub32Chip {
impl<F: AbstractField> BaseAir<F> for Sub32Chip {
fn width(&self) -> usize {
NUM_SUB_COLS
}
Expand Down
43 changes: 21 additions & 22 deletions basic/src/bin/valida.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use p3_baby_bear::BabyBear;

use p3_fri::{FriConfig, TwoAdicFriPcs, TwoAdicFriPcsConfig};
use valida_cpu::MachineWithCpuChip;
use valida_machine::{Machine, MachineProof, ProgramROM, StdinAdviceProvider};
use valida_machine::{Machine, MachineProof, ProgramROM, StdinAdviceProvider, StoppingFlag};
use valida_memory::MachineWithMemoryChip;

use valida_elf::{load_executable_file, Program};
Expand All @@ -34,7 +34,7 @@ use valida_output::MachineWithOutputChip;
use reedline_repl_rs::clap::{Arg, ArgMatches, Command};
use reedline_repl_rs::{Repl, Result};

#[derive(Parser)]
#[derive(Parser, Clone)]
struct Args {
/// Command option either "run" or "prove" or "verify" or "interactive"
#[arg(name = "Action Option")]
Expand All @@ -53,23 +53,23 @@ struct Args {
stack_height: u32,
}

struct Context<'a> {
struct Context {
machine_: BasicMachine<BabyBear>,
args_: &'a Args,
args_: Args,
breakpoints_: Vec<u32>,
stopped_: bool,
stopped_: StoppingFlag,
last_fp_: u32,
recorded_current_fp_: u32,
last_fp_size_: u32,
}

impl Context<'_> {
impl Context {
fn new(args: &Args) -> Context {
let mut context = Context {
machine_: BasicMachine::<BabyBear>::default(),
args_: args.clone(),
args_: (*args).clone(),
breakpoints_: Vec::new(),
stopped_: false,
stopped_: StoppingFlag::DidNotStop,
last_fp_: args.stack_height,
recorded_current_fp_: args.stack_height,
last_fp_size_: 0,
Expand All @@ -87,10 +87,10 @@ impl Context<'_> {
context
}

fn step(&mut self) -> (bool, u32) {
fn step(&mut self) -> (StoppingFlag, u32) {
// do not execute if already stopped
if self.stopped_ {
return (true, 0);
if self.stopped_ == StoppingFlag::DidStop {
return (StoppingFlag::DidStop, 0);
}
let state = self.machine_.step(&mut StdinAdviceProvider);
let pc = self.machine_.cpu().pc;
Expand All @@ -109,21 +109,20 @@ impl Context<'_> {
}
}

fn init_context(args: ArgMatches, context: &mut Context) -> Result<Option<String>> {
fn init_context(_args: ArgMatches, _context: &mut Context) -> Result<Option<String>> {
Ok(Some(String::from("created machine")))
}

fn status(args: ArgMatches, context: &mut Context) -> Result<Option<String>> {
fn status(_args: ArgMatches, context: &mut Context) -> Result<Option<String>> {
// construct machine status
let mut status = String::new();
status.push_str("FP: ");
status.push_str(&context.machine_.cpu().fp.to_string());
status.push_str(", PC: ");
status.push_str(&context.machine_.cpu().pc.to_string());
status.push_str(if context.stopped_ {
", Stopped"
} else {
", Running"
status.push_str(match context.stopped_ {
StoppingFlag::DidStop => ", Stopped",
StoppingFlag::DidNotStop => ", Running",
});
Ok(Some(status))
}
Expand Down Expand Up @@ -204,11 +203,11 @@ fn set_bp(args: ArgMatches, context: &mut Context) -> Result<Option<String>> {
Ok(Some(message))
}

fn run_until(args: ArgMatches, context: &mut Context) -> Result<Option<String>> {
fn run_until(_args: ArgMatches, context: &mut Context) -> Result<Option<String>> {
let mut message = String::new();
loop {
let (stop, pc) = context.step();
if stop {
if stop == StoppingFlag::DidStop {
message.push_str("Execution stopped");
break;
}
Expand All @@ -221,10 +220,10 @@ fn run_until(args: ArgMatches, context: &mut Context) -> Result<Option<String>>
Ok(Some(message))
}

fn step(args: ArgMatches, context: &mut Context) -> Result<Option<String>> {
fn step(_args: ArgMatches, context: &mut Context) -> Result<Option<String>> {
let (stop, _) = context.step();
if stop {
context.stopped_ = true;
if stop == StoppingFlag::DidStop {
context.stopped_ = StoppingFlag::DidStop;
Ok(Some(String::from("Execution stopped")))
} else {
Ok(None)
Expand Down
Loading
Loading