Skip to content

Plonky3 MidenVM Air constraints #2562

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.

Sign up for GitHub

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

Draft
Leo-Besancon wants to merge 1 commit into
base: next
Choose a base branch
from
Draft

Plonky3 MidenVM Air constraints #2562

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
33 changes: 33 additions & 0 deletions air/src/constraints/chiplets/ace/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
use miden_core::field::PrimeCharacteristicRing;
use miden_crypto::stark::air::MidenAirBuilder;

use crate::MainTraceRow;

pub fn enforce_ace_chiplet_constraints<AB>(
builder: &mut AB,
local: &MainTraceRow<AB::Var>,
next: &MainTraceRow<AB::Var>,
) where
AB: MidenAirBuilder,
{
builder.assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * (local.chiplets[4].clone().into() * local.chiplets[4].clone().into() - local.chiplets[4].clone().into()));
builder.assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * (local.chiplets[5].clone().into() * local.chiplets[5].clone().into() - local.chiplets[5].clone().into()));
builder.when_transition().assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * next.chiplets[3].clone().into() * local.chiplets[4].clone().into());
builder.when_transition().assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * (AB::Expr::ONE - next.chiplets[3].clone().into()) * local.chiplets[4].clone().into() * next.chiplets[4].clone().into());
builder.assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * local.chiplets[4].clone().into() * local.chiplets[5].clone().into());
builder.when_transition().assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * (AB::Expr::ONE - local.chiplets[4].clone().into()) * local.chiplets[5].clone().into() * (AB::Expr::ONE - next.chiplets[5].clone().into()));
builder.when_transition().assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * ((AB::Expr::ONE - next.chiplets[3].clone().into()) * local.chiplets[4].clone().into() + next.chiplets[3].clone().into() - (AB::Expr::ONE - next.chiplets[3].clone().into()) * local.chiplets[4].clone().into() * next.chiplets[3].clone().into()) * (AB::Expr::ONE - local.chiplets[5].clone().into()));
builder.when_transition().assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * (AB::Expr::ONE - local.chiplets[5].clone().into()) * ((AB::Expr::ONE - next.chiplets[5].clone().into()) * (next.chiplets[16].clone().into() - (next.chiplets[10].clone().into() + AB::Expr::ONE)) + next.chiplets[10].clone().into() + AB::Expr::ONE - local.chiplets[16].clone().into()));
builder.when_transition().assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * (AB::Expr::ONE - next.chiplets[3].clone().into()) * (AB::Expr::ONE - next.chiplets[4].clone().into()) * (next.chiplets[6].clone().into() - local.chiplets[6].clone().into()));
builder.when_transition().assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * (AB::Expr::ONE - next.chiplets[3].clone().into()) * (AB::Expr::ONE - next.chiplets[4].clone().into()) * (next.chiplets[8].clone().into() - local.chiplets[8].clone().into()));
builder.when_transition().assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * (AB::Expr::ONE - next.chiplets[3].clone().into()) * (AB::Expr::ONE - next.chiplets[4].clone().into()) * (next.chiplets[7].clone().into() - (local.chiplets[7].clone().into() + AB::Expr::from_u64(4) * (AB::Expr::ONE - local.chiplets[5].clone().into()) + local.chiplets[5].clone().into())));
builder.when_transition().assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * (AB::Expr::ONE - next.chiplets[3].clone().into()) * (AB::Expr::ONE - next.chiplets[4].clone().into()) * (local.chiplets[10].clone().into() - (next.chiplets[10].clone().into() + (AB::Expr::ONE - local.chiplets[5].clone().into()).double() + local.chiplets[5].clone().into())));
builder.assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * (AB::Expr::ONE - local.chiplets[5].clone().into()) * (local.chiplets[13].clone().into() - (local.chiplets[10].clone().into() - AB::Expr::ONE)));
builder.assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * local.chiplets[5].clone().into() * local.chiplets[9].clone().into() * (local.chiplets[9].clone().into() - AB::Expr::ONE) * (local.chiplets[9].clone().into() + AB::Expr::ONE));
builder.assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * local.chiplets[5].clone().into() * (local.chiplets[9].clone().into() * local.chiplets[9].clone().into() * (local.chiplets[14].clone().into() + local.chiplets[9].clone().into() * local.chiplets[17].clone().into() - (local.chiplets[14].clone().into() * local.chiplets[17].clone().into() - local.chiplets[15].clone().into().double() * local.chiplets[18].clone().into())) + local.chiplets[14].clone().into() * local.chiplets[17].clone().into() - local.chiplets[15].clone().into().double() * local.chiplets[18].clone().into() - local.chiplets[11].clone().into()));
builder.assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * local.chiplets[5].clone().into() * (local.chiplets[9].clone().into() * local.chiplets[9].clone().into() * (local.chiplets[15].clone().into() + local.chiplets[9].clone().into() * local.chiplets[18].clone().into() - ((local.chiplets[17].clone().into() + local.chiplets[18].clone().into()) * (local.chiplets[14].clone().into() + local.chiplets[15].clone().into()) - local.chiplets[14].clone().into() * local.chiplets[17].clone().into())) + (local.chiplets[17].clone().into() + local.chiplets[18].clone().into()) * (local.chiplets[14].clone().into() + local.chiplets[15].clone().into()) - local.chiplets[14].clone().into() * local.chiplets[17].clone().into() - local.chiplets[12].clone().into()));
builder.when_transition().assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * ((AB::Expr::ONE - next.chiplets[3].clone().into()) * next.chiplets[4].clone().into() + next.chiplets[3].clone().into() - (AB::Expr::ONE - next.chiplets[3].clone().into()) * next.chiplets[4].clone().into() * next.chiplets[3].clone().into()) * local.chiplets[11].clone().into());
builder.when_transition().assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * ((AB::Expr::ONE - next.chiplets[3].clone().into()) * next.chiplets[4].clone().into() + next.chiplets[3].clone().into() - (AB::Expr::ONE - next.chiplets[3].clone().into()) * next.chiplets[4].clone().into() * next.chiplets[3].clone().into()) * local.chiplets[12].clone().into());
builder.when_transition().assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * local.chiplets[2].clone().into() * (AB::Expr::ONE - local.chiplets[3].clone().into()) * ((AB::Expr::ONE - next.chiplets[3].clone().into()) * next.chiplets[4].clone().into() + next.chiplets[3].clone().into() - (AB::Expr::ONE - next.chiplets[3].clone().into()) * next.chiplets[4].clone().into() * next.chiplets[3].clone().into()) * local.chiplets[10].clone().into());
builder.when_transition().assert_zero(local.chiplets[0].clone().into() * local.chiplets[1].clone().into() * (AB::Expr::ONE - local.chiplets[2].clone().into()) * next.chiplets[2].clone().into() * (next.chiplets[4].clone().into() - AB::Expr::ONE));
}
32 changes: 32 additions & 0 deletions air/src/constraints/chiplets/bitwise/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
use miden_core::field::PrimeCharacteristicRing;
use miden_crypto::stark::air::MidenAirBuilder;

use crate::MainTraceRow;

pub fn enforce_bitwise_chiplet_constraints<AB>(
builder: &mut AB,
local: &MainTraceRow<AB::Var>,
next: &MainTraceRow<AB::Var>,
periodic_values: &[AB::PeriodicVal],
) where
AB: MidenAirBuilder,
{
builder.assert_zero(local.chiplets[0].clone().into() * (AB::Expr::ONE - local.chiplets[1].clone().into()) * (local.chiplets[2].clone().into() * local.chiplets[2].clone().into() - local.chiplets[2].clone().into()));
builder.when_transition().assert_zero_ext(AB::ExprEF::from(local.chiplets[0].clone().into()) * (AB::ExprEF::ONE - AB::ExprEF::from(local.chiplets[1].clone().into())) * AB::ExprEF::from(periodic_values[1].clone().into()) * (AB::ExprEF::from(next.chiplets[2].clone().into()) - AB::ExprEF::from(local.chiplets[2].clone().into())));
builder.assert_zero(local.chiplets[0].clone().into() * (AB::Expr::ONE - local.chiplets[1].clone().into()) * (local.chiplets[5].clone().into() * local.chiplets[5].clone().into() - local.chiplets[5].clone().into()));
builder.assert_zero(local.chiplets[0].clone().into() * (AB::Expr::ONE - local.chiplets[1].clone().into()) * (local.chiplets[6].clone().into() * local.chiplets[6].clone().into() - local.chiplets[6].clone().into()));
builder.assert_zero(local.chiplets[0].clone().into() * (AB::Expr::ONE - local.chiplets[1].clone().into()) * (local.chiplets[7].clone().into() * local.chiplets[7].clone().into() - local.chiplets[7].clone().into()));
builder.assert_zero(local.chiplets[0].clone().into() * (AB::Expr::ONE - local.chiplets[1].clone().into()) * (local.chiplets[8].clone().into() * local.chiplets[8].clone().into() - local.chiplets[8].clone().into()));
builder.assert_zero(local.chiplets[0].clone().into() * (AB::Expr::ONE - local.chiplets[1].clone().into()) * (local.chiplets[9].clone().into() * local.chiplets[9].clone().into() - local.chiplets[9].clone().into()));
builder.assert_zero(local.chiplets[0].clone().into() * (AB::Expr::ONE - local.chiplets[1].clone().into()) * (local.chiplets[10].clone().into() * local.chiplets[10].clone().into() - local.chiplets[10].clone().into()));
builder.assert_zero(local.chiplets[0].clone().into() * (AB::Expr::ONE - local.chiplets[1].clone().into()) * (local.chiplets[11].clone().into() * local.chiplets[11].clone().into() - local.chiplets[11].clone().into()));
builder.assert_zero(local.chiplets[0].clone().into() * (AB::Expr::ONE - local.chiplets[1].clone().into()) * (local.chiplets[12].clone().into() * local.chiplets[12].clone().into() - local.chiplets[12].clone().into()));
builder.assert_zero_ext(AB::ExprEF::from(local.chiplets[0].clone().into()) * (AB::ExprEF::ONE - AB::ExprEF::from(local.chiplets[1].clone().into())) * AB::ExprEF::from(periodic_values[0].clone().into()) * (AB::ExprEF::from(local.chiplets[3].clone().into()) - (AB::ExprEF::from(local.chiplets[5].clone().into()) + AB::ExprEF::from(local.chiplets[6].clone().into()).double() + AB::ExprEF::from_u64(4) * AB::ExprEF::from(local.chiplets[7].clone().into()) + AB::ExprEF::from_u64(8) * AB::ExprEF::from(local.chiplets[8].clone().into()))));
builder.assert_zero_ext(AB::ExprEF::from(local.chiplets[0].clone().into()) * (AB::ExprEF::ONE - AB::ExprEF::from(local.chiplets[1].clone().into())) * AB::ExprEF::from(periodic_values[0].clone().into()) * (AB::ExprEF::from(local.chiplets[4].clone().into()) - (AB::ExprEF::from(local.chiplets[9].clone().into()) + AB::ExprEF::from(local.chiplets[10].clone().into()).double() + AB::ExprEF::from_u64(4) * AB::ExprEF::from(local.chiplets[11].clone().into()) + AB::ExprEF::from_u64(8) * AB::ExprEF::from(local.chiplets[12].clone().into()))));
builder.when_transition().assert_zero_ext(AB::ExprEF::from(local.chiplets[0].clone().into()) * (AB::ExprEF::ONE - AB::ExprEF::from(local.chiplets[1].clone().into())) * AB::ExprEF::from(periodic_values[1].clone().into()) * (AB::ExprEF::from(next.chiplets[3].clone().into()) - (AB::ExprEF::from(local.chiplets[3].clone().into()) * AB::ExprEF::from_u64(16) + AB::ExprEF::from(local.chiplets[5].clone().into()) + AB::ExprEF::from(local.chiplets[6].clone().into()).double() + AB::ExprEF::from_u64(4) * AB::ExprEF::from(local.chiplets[7].clone().into()) + AB::ExprEF::from_u64(8) * AB::ExprEF::from(local.chiplets[8].clone().into()))));
builder.when_transition().assert_zero_ext(AB::ExprEF::from(local.chiplets[0].clone().into()) * (AB::ExprEF::ONE - AB::ExprEF::from(local.chiplets[1].clone().into())) * AB::ExprEF::from(periodic_values[1].clone().into()) * (AB::ExprEF::from(next.chiplets[4].clone().into()) - (AB::ExprEF::from(local.chiplets[4].clone().into()) * AB::ExprEF::from_u64(16) + AB::ExprEF::from(local.chiplets[9].clone().into()) + AB::ExprEF::from(local.chiplets[10].clone().into()).double() + AB::ExprEF::from_u64(4) * AB::ExprEF::from(local.chiplets[11].clone().into()) + AB::ExprEF::from_u64(8) * AB::ExprEF::from(local.chiplets[12].clone().into()))));
builder.assert_zero_ext(AB::ExprEF::from(local.chiplets[0].clone().into()) * (AB::ExprEF::ONE - AB::ExprEF::from(local.chiplets[1].clone().into())) * AB::ExprEF::from(periodic_values[0].clone().into()) * AB::ExprEF::from(local.chiplets[13].clone().into()));
builder.when_transition().assert_zero_ext(AB::ExprEF::from(local.chiplets[0].clone().into()) * (AB::ExprEF::ONE - AB::ExprEF::from(local.chiplets[1].clone().into())) * AB::ExprEF::from(periodic_values[1].clone().into()) * (AB::ExprEF::from(next.chiplets[13].clone().into()) - AB::ExprEF::from(local.chiplets[14].clone().into())));
builder.assert_zero(local.chiplets[0].clone().into() * (AB::Expr::ONE - local.chiplets[1].clone().into()) * (local.chiplets[14].clone().into() - (local.chiplets[13].clone().into() * AB::Expr::from_u64(16) + local.chiplets[2].clone().into() * (local.chiplets[5].clone().into() + local.chiplets[9].clone().into() - (local.chiplets[5].clone().into() * local.chiplets[9].clone().into() + local.chiplets[5].clone().into() * local.chiplets[9].clone().into()) + (local.chiplets[6].clone().into() + local.chiplets[10].clone().into() - (local.chiplets[6].clone().into() * local.chiplets[10].clone().into() + local.chiplets[6].clone().into() * local.chiplets[10].clone().into())).double() + AB::Expr::from_u64(4) * (local.chiplets[7].clone().into() + local.chiplets[11].clone().into() - (local.chiplets[7].clone().into() * local.chiplets[11].clone().into() + local.chiplets[7].clone().into() * local.chiplets[11].clone().into())) + AB::Expr::from_u64(8) * (local.chiplets[8].clone().into() + local.chiplets[12].clone().into() - (local.chiplets[8].clone().into() * local.chiplets[12].clone().into() + local.chiplets[8].clone().into() * local.chiplets[12].clone().into())) - (local.chiplets[5].clone().into() * local.chiplets[9].clone().into() + local.chiplets[6].clone().into() * local.chiplets[10].clone().into() + local.chiplets[6].clone().into() * local.chiplets[10].clone().into() + AB::Expr::from_u64(4) * local.chiplets[7].clone().into() * local.chiplets[11].clone().into() + AB::Expr::from_u64(8) * local.chiplets[8].clone().into() * local.chiplets[12].clone().into())) + local.chiplets[5].clone().into() * local.chiplets[9].clone().into() + local.chiplets[6].clone().into() * local.chiplets[10].clone().into() + local.chiplets[6].clone().into() * local.chiplets[10].clone().into() + AB::Expr::from_u64(4) * local.chiplets[7].clone().into() * local.chiplets[11].clone().into() + AB::Expr::from_u64(8) * local.chiplets[8].clone().into() * local.chiplets[12].clone().into())));

}
Loading
Loading