Skip to content

Commit

Permalink
some refactoring
Browse files Browse the repository at this point in the history
  • Loading branch information
kevjue committed May 10, 2024
1 parent ac68482 commit 57633ef
Show file tree
Hide file tree
Showing 3 changed files with 59 additions and 39 deletions.
4 changes: 0 additions & 4 deletions .github/workflows/pr.yml
Original file line number Diff line number Diff line change
Expand Up @@ -162,7 +162,6 @@ jobs:
run: |
cd cli
cargo install --locked --path .
<<<<<<< HEAD
cd ~
- name: Run cargo prove new
Expand All @@ -176,6 +175,3 @@ jobs:
cargo prove build
cd ../script
SP1_DEV=1 RUST_LOG=info cargo run --release
=======
cd ~
>>>>>>> dev
60 changes: 25 additions & 35 deletions recursion/core/src/cpu/air/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ mod branch;
mod jump;
mod memory;
mod operands;
mod system;

use std::borrow::Borrow;

Expand Down Expand Up @@ -78,45 +79,13 @@ where

// Constrain the system instructions (TRAP, HALT).
self.eval_system_instructions(builder, local, next);

// Constrain the is_real_flag.
self.eval_is_real(builder, local, next);
}
}

impl<F: Field> CpuChip<F> {
/// Eval the system instructions (TRAP, HALT).
///
/// This method will contrain the following:
/// 1) Ensure that none of the instructions where TRAP.
/// 2) Ensure that the last real instruction is a HALT.
pub fn eval_system_instructions<AB>(
&self,
builder: &mut AB,
local: &CpuCols<AB::Var>,
next: &CpuCols<AB::Var>,
) where
AB: SP1RecursionAirBuilder,
{
builder
.when(local.is_real)
.assert_zero(local.selectors.is_trap);

builder
.when_transition()
.when(local.is_real)
.when_not(next.is_real)
.assert_one(local.selectors.is_halt);

builder.assert_bool(local.is_real);

builder.when_first_row().assert_one(local.is_real);

builder
.when_transition()
.when_not(local.is_real)
.assert_zero(next.is_real);

builder.when_last_row().assert_zero(local.is_real);
}

/// Eval the clk.
///
/// For all instructions except for FRI fold, the next clk is the current clk + 4.
Expand All @@ -139,6 +108,27 @@ impl<F: Field> CpuChip<F> {
.assert_eq(local.clk.into() + local.a.value()[0], next.clk);
}

/// Eval the is_real flag.
pub fn eval_is_real<AB>(
&self,
builder: &mut AB,
local: &CpuCols<AB::Var>,
next: &CpuCols<AB::Var>,
) where
AB: SP1RecursionAirBuilder,
{
builder.assert_bool(local.is_real);

// First row should be real.
builder.when_first_row().assert_one(local.is_real);

// Once rows transition to not real, then they should stay not real.
builder
.when_transition()
.when_not(local.is_real)
.assert_zero(next.is_real);
}

/// Expr to check for alu instructions.
pub fn is_alu_instruction<AB>(&self, local: &CpuCols<AB::Var>) -> AB::Expr
where
Expand Down
34 changes: 34 additions & 0 deletions recursion/core/src/cpu/air/system.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
use p3_air::AirBuilder;
use p3_field::Field;
use sp1_core::air::BaseAirBuilder;

use crate::{
air::SP1RecursionAirBuilder,
cpu::{CpuChip, CpuCols},
};

impl<F: Field> CpuChip<F> {
/// Eval the system instructions (TRAP, HALT).
///
/// This method will contrain the following:
/// 1) Ensure that none of the instructions where TRAP.
/// 2) Ensure that the last real instruction is a HALT.
pub fn eval_system_instructions<AB>(
&self,
builder: &mut AB,
local: &CpuCols<AB::Var>,
next: &CpuCols<AB::Var>,
) where
AB: SP1RecursionAirBuilder,
{
builder
.when(local.is_real)
.assert_zero(local.selectors.is_trap);

builder
.when_transition()
.when(local.is_real)
.when_not(next.is_real)
.assert_one(local.selectors.is_halt);
}
}

0 comments on commit 57633ef

Please sign in to comment.