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: implement buses #371

Open
wants to merge 60 commits into
base: next
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
60 commits
Select commit Hold shift + click to select a range
9438b12
feat: implement bus declaration parsing
Leo-Besancon Feb 5, 2025
e9886ff
Attempting to add bus constraints parsing, may need rework
Leo-Besancon Feb 6, 2025
ee630e2
Add Expr::BusOperation variant
Leo-Besancon Feb 7, 2025
509839c
Fix grammar naming + add bus operation test placeholder
Leo-Besancon Feb 7, 2025
311ff56
docs: Clarify buses are unimplemented on the AST > AIR pipeline
Leo-Besancon Feb 10, 2025
6e12cc0
feat: Add visit_mut_bus_operation AST visitor helper
Leo-Besancon Feb 10, 2025
75da91e
Add Null expression for Empty bus representation
Leo-Besancon Feb 10, 2025
4065a66
Improve parser + lexer for buses
Leo-Besancon Feb 10, 2025
3652c71
Add semantic analysis base for buses
Leo-Besancon Feb 10, 2025
5abc556
Add boundary and integrity tests for buses operations
Leo-Besancon Feb 10, 2025
510a384
Fix lexing (BusIdent > Ident) and tests
Leo-Besancon Feb 10, 2025
eade510
Handle most of semantic analysis for buses
Leo-Besancon Feb 10, 2025
cdb5374
Ignore bus test on MIR, fix tests
Leo-Besancon Feb 10, 2025
4562516
feat: improve semantic analysis for buses, add tests
Leo-Besancon Feb 11, 2025
629f071
derive Hash and Default for BusType
Soulthym Feb 10, 2025
599ea27
Add Bus struct to the mir::Graph
Soulthym Feb 10, 2025
468c2c8
store buses in a BTreeMap by their Identifiet
Soulthym Feb 11, 2025
781cd0e
implement mir::BusOp as Op, Owner and Node variants
Soulthym Feb 11, 2025
c73399d
pass buses to the program
Soulthym Feb 12, 2025
9f29abe
translate ast::Bus into mir: track definitions
Soulthym Feb 12, 2025
924a190
derive Debug on struct Builders
Soulthym Feb 13, 2025
9312db7
translate BusOperations from ast to mir
Soulthym Feb 13, 2025
47ae5dd
cargo fmt + clippy
Soulthym Feb 13, 2025
e9030f8
Fix translate of bus constraints
Leo-Besancon Feb 14, 2025
8c26537
draft: add bus operation expand in MIR
Leo-Besancon Feb 17, 2025
d985704
feat: add bus operation expand in MIR
Leo-Besancon Feb 17, 2025
4e53055
Bugfix stackoverflow + mir utils + buses test
Soulthym Feb 18, 2025
31aaa91
cargo fmt + clippy
Soulthym Feb 18, 2025
7f1129e
Handle bus boundary constraint to public inputs
Leo-Besancon Feb 19, 2025
072450c
Translate bus boundary constraint in Link<Bus>
Leo-Besancon Feb 19, 2025
bd10571
feat: only null are currently supported as buses boundary constraints
Leo-Besancon Feb 20, 2025
cfbe7ea
refactor: Better expand bus null boundary constraints
Leo-Besancon Feb 20, 2025
13f31a6
feat: Include BusOpExpand pass in all MIR pipelines
Leo-Besancon Feb 20, 2025
0322ee5
feat: Add BusOpExpand pass everywhere
Leo-Besancon Feb 20, 2025
35c6ae9
fix infinite loop on hash and partial_eq for Bus/BusOp, bus.add/rem api
Soulthym Feb 20, 2025
c299a22
chore: fix conflict after merge
Leo-Besancon Feb 20, 2025
195a619
feat: handle both aux and buses for now
Leo-Besancon Feb 20, 2025
37f7432
tests: add buses codegen tests (for winterfell and masm, unchecked)
Leo-Besancon Feb 20, 2025
e7c939d
tests: add codegen failure tests on WithoutMIR pipeline
Leo-Besancon Feb 20, 2025
21ebd2c
tests: Include 2 buse codegen tests
Leo-Besancon Feb 20, 2025
510ca8c
Visit all bus operations
Leo-Besancon Feb 20, 2025
4e89655
docs: Add brief bus documentation
Leo-Besancon Feb 21, 2025
2970265
relax dependencies patch versions
Soulthym Mar 25, 2025
a489b15
Improve bus documentation
Soulthym Mar 25, 2025
aa1e68d
fix: Use Mul instead of Add to combine multiset check constraints
Leo-Besancon Mar 26, 2025
230e1b1
tests: update buses_simple test to be more useful
Leo-Besancon Mar 26, 2025
a0d5ff7
tests: update buses_complex test with different tuples
Leo-Besancon Mar 26, 2025
410fe17
feat: remove "noops" in Bus constraints : +0 and *1
Leo-Besancon Mar 26, 2025
d3dd4d0
chore: various fixes following review (format, comments removal / rew…
Leo-Besancon Mar 26, 2025
fec28df
feat: do not allow empty bus section
Leo-Besancon Mar 27, 2025
d832a24
Update MathJax support
Leo-Besancon Mar 27, 2025
1cc8402
feat: reworked how BusOperations and Null are handled as Expr and Sca…
Leo-Besancon Mar 27, 2025
d331fb8
add multiset citation
Soulthym Mar 27, 2025
c1f5e9a
chore: removed a todo!() on empty selector with buses
Leo-Besancon Mar 27, 2025
ce1a900
Merge branch 'feat-implement-bus' of https://github.com/massalabs/air…
Leo-Besancon Mar 27, 2025
9c6ae82
remove leftover debugging
Soulthym Mar 27, 2025
ee2878e
cleanup comments formatting
Soulthym Mar 27, 2025
effd6a3
chore: document unused ControlFlow and fix nightly clippy warns
Leo-Besancon Mar 28, 2025
a8a028a
document `when`, `for` and `in` keywords
Soulthym Mar 28, 2025
78edc46
chore: removed irrelevant commented code
Leo-Besancon Mar 28, 2025
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 air-script/src/cli/transpile.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,7 @@ impl Transpile {
.chain(mir::passes::AstToMir::new(&diagnostics))
.chain(mir::passes::Inlining::new(&diagnostics))
.chain(mir::passes::Unrolling::new(&diagnostics))
.chain(mir::passes::BusOpExpand::new(&diagnostics))
.chain(air_ir::passes::MirToAir::new(&diagnostics));
pipeline.run(ast)
})
Expand Down
39 changes: 39 additions & 0 deletions air-script/tests/buses/buses_complex.air
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
def BusesAir

trace_columns {
main: [a, b, s1, s2, d],
}

buses {
unit p,
mult q,
}

public_inputs {
inputs: [2],
}

boundary_constraints {
enf p.first = null;
enf q.first = null;
enf p.last = null;
enf q.last = null;
# TODO: to be used when we have support for variable-length public inputs
#enf p.last = inputs;
#enf q.last = inputs;
}

integrity_constraints {
enf s1^2 = s1;
enf s2^2 = s2;

p.add(1, a) when s1;
p.rem(1, b) when s2;

p.add(2, b) when 1 - s1;
p.rem(2, a) when 1 - s2;

q.add(3, a) when s1;
q.add(3, a) when s1;
q.rem(4, b) for d;
}
179 changes: 179 additions & 0 deletions air-script/tests/buses/buses_complex.masm
Original file line number Diff line number Diff line change
@@ -0,0 +1,179 @@
# Procedure to efficiently compute the required exponentiations of the out-of-domain point `z` and cache them for later use.
#
# This computes the power of `z` needed to evaluate the periodic polynomials and the constraint divisors
#
# Input: [...]
# Output: [...]
proc.cache_z_exp
padw mem_loadw.4294903304 drop drop # load z
# => [z_1, z_0, ...]
# Exponentiate z trace_len times
mem_load.4294903307 neg
# => [count, z_1, z_0, ...] where count = -log2(trace_len)
dup.0 neq.0
while.true
movdn.2 dup.1 dup.1 ext2mul
# => [(e_1, e_0)^n, i, ...]
movup.2 add.1 dup.0 neq.0
# => [b, i+1, (e_1, e_0)^n, ...]
end # END while
push.0 mem_storew.500000100 # z^trace_len
# => [0, 0, (z_1, z_0)^trace_len, ...]
dropw # Clean stack
end # END PROC cache_z_exp

# Procedure to compute the exemption points.
#
# Input: [...]
# Output: [g^{-2}, g^{-1}, ...]
proc.get_exemptions_points
mem_load.4294799999
# => [g, ...]
push.1 swap div
# => [g^{-1}, ...]
dup.0 dup.0 mul
# => [g^{-2}, g^{-1}, ...]
end # END PROC get_exemptions_points

# Procedure to compute the integrity constraint divisor.
#
# The divisor is defined as `(z^trace_len - 1) / ((z - g^{trace_len-2}) * (z - g^{trace_len-1}))`
# Procedure `cache_z_exp` must have been called prior to this.
#
# Input: [...]
# Output: [divisor_1, divisor_0, ...]
proc.compute_integrity_constraint_divisor
padw mem_loadw.500000100 drop drop # load z^trace_len
# Comments below use zt = `z^trace_len`
# => [zt_1, zt_0, ...]
push.1 push.0 ext2sub
# => [zt_1-1, zt_0-1, ...]
padw mem_loadw.4294903304 drop drop # load z
# => [z_1, z_0, zt_1-1, zt_0-1, ...]
exec.get_exemptions_points
# => [g^{trace_len-2}, g^{trace_len-1}, z_1, z_0, zt_1-1, zt_0-1, ...]
dup.0 mem_store.500000101 # Save a copy of `g^{trace_len-2} to be used by the boundary divisor
dup.3 dup.3 movup.3 push.0 ext2sub
# => [e_1, e_0, g^{trace_len-1}, z_1, z_0, zt_1-1, zt_0-1, ...]
movup.4 movup.4 movup.4 push.0 ext2sub
# => [e_3, e_2, e_1, e_0, zt_1-1, zt_0-1, ...]
ext2mul
# => [denominator_1, denominator_0, zt_1-1, zt_0-1, ...]
ext2div
# => [divisor_1, divisor_0, ...]
end # END PROC compute_integrity_constraint_divisor

# Procedure to evaluate numerators of all integrity constraints.
#
# All the 2 main and 2 auxiliary constraints are evaluated.
# The result of each evaluation is kept on the stack, with the top of the stack
# containing the evaluations for the auxiliary trace (if any) followed by the main trace.
#
# Input: [...]
# Output: [(r_1, r_0)*, ...]
# where: (r_1, r_0) is the quadratic extension element resulting from the integrity constraint evaluation.
# This procedure pushes 4 quadratic extension field elements to the stack
proc.compute_integrity_constraints
# integrity constraint 0 for main
padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2mul padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2sub
# Multiply by the composition coefficient
padw mem_loadw.4294900200 movdn.3 movdn.3 drop drop ext2mul
# integrity constraint 1 for main
padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop ext2mul padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop ext2sub
# Multiply by the composition coefficient
padw mem_loadw.4294900200 drop drop ext2mul
# integrity constraint 0 for aux
padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.1 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2mul push.1 push.0 padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2sub ext2add padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.2 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900001 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add push.1 push.0 padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2sub ext2mul push.1 push.0 push.1 push.0 padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2sub ext2sub ext2add ext2mul padw mem_loadw.4294900072 movdn.3 movdn.3 drop drop ext2mul padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.1 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900001 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop ext2mul push.1 push.0 padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop ext2sub ext2add padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.2 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add push.1 push.0 padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop ext2sub ext2mul push.1 push.0 push.1 push.0 padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop ext2sub ext2sub ext2add ext2mul padw mem_loadw.4294900072 drop drop ext2mul ext2sub
# Multiply by the composition coefficient
padw mem_loadw.4294900201 movdn.3 movdn.3 drop drop ext2mul
# integrity constraint 1 for aux
padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.4 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900001 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900073 movdn.3 movdn.3 drop drop ext2mul padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.4 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900001 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2mul padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.4 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900001 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2mul ext2add ext2add padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.4 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900001 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900073 drop drop ext2mul padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900004 movdn.3 movdn.3 drop drop ext2mul ext2add ext2sub
# Multiply by the composition coefficient
padw mem_loadw.4294900201 drop drop ext2mul
end # END PROC compute_integrity_constraints

# Procedure to evaluate the boundary constraint numerator for the first row of the auxiliary trace
#
# Input: [...]
# Output: [(r_1, r_0)*, ...]
# Where: (r_1, r_0) is one quadratic extension field element for each constraint
proc.compute_boundary_constraints_aux_first
# boundary constraint 0 for aux
padw mem_loadw.4294900072 movdn.3 movdn.3 drop drop push.1 push.0 ext2sub
# Multiply by the composition coefficient
padw mem_loadw.4294900202 movdn.3 movdn.3 drop drop ext2mul
# boundary constraint 1 for aux
padw mem_loadw.4294900073 movdn.3 movdn.3 drop drop push.0 push.0 ext2sub
# Multiply by the composition coefficient
padw mem_loadw.4294900202 drop drop ext2mul
end # END PROC compute_boundary_constraints_aux_first

# Procedure to evaluate the boundary constraint numerator for the last row of the auxiliary trace
#
# Input: [...]
# Output: [(r_1, r_0)*, ...]
# Where: (r_1, r_0) is one quadratic extension field element for each constraint
proc.compute_boundary_constraints_aux_last
# boundary constraint 2 for aux
padw mem_loadw.4294900072 movdn.3 movdn.3 drop drop push.1 push.0 ext2sub
# Multiply by the composition coefficient
padw mem_loadw.4294900203 movdn.3 movdn.3 drop drop ext2mul
# boundary constraint 3 for aux
padw mem_loadw.4294900073 movdn.3 movdn.3 drop drop push.0 push.0 ext2sub
# Multiply by the composition coefficient
padw mem_loadw.4294900203 drop drop ext2mul
end # END PROC compute_boundary_constraints_aux_last

# Procedure to evaluate all integrity constraints.
#
# Input: [...]
# Output: [(r_1, r_0), ...]
# Where: (r_1, r_0) is the final result with the divisor applied
proc.evaluate_integrity_constraints
exec.compute_integrity_constraints
# Numerator of the transition constraint polynomial
ext2add ext2add ext2add ext2add
# Divisor of the transition constraint polynomial
exec.compute_integrity_constraint_divisor
ext2div # divide the numerator by the divisor
end # END PROC evaluate_integrity_constraints

# Procedure to evaluate all boundary constraints.
#
# Input: [...]
# Output: [(r_1, r_0), ...]
# Where: (r_1, r_0) is the final result with the divisor applied
proc.evaluate_boundary_constraints
exec.compute_boundary_constraints_aux_last
# Accumulate the numerator for segment 1 LastRow
ext2add ext2add
# => [(aux_last1, aux_last0), ...]
# Compute the denominator for domain LastRow
padw mem_loadw.4294903304 drop drop # load z
mem_load.500000101 push.0 ext2sub
# Compute numerator/denominator for last row
ext2div
exec.compute_boundary_constraints_aux_first
# Accumulate the numerator for segment 1 FirstRow
ext2add ext2add
# => [(aux_first1, aux_first0), ...]
# Compute the denominator for domain FirstRow
padw mem_loadw.4294903304 drop drop # load z
push.1 push.0 ext2sub
# Compute numerator/denominator for first row
ext2div
# Add first and last row groups
ext2add
end # END PROC evaluate_boundary_constraints

# Procedure to evaluate the integrity and boundary constraints.
#
# Input: [...]
# Output: [(r_1, r_0), ...]
export.evaluate_constraints
exec.cache_z_exp
exec.evaluate_integrity_constraints
exec.evaluate_boundary_constraints
ext2add
end # END PROC evaluate_constraints

96 changes: 96 additions & 0 deletions air-script/tests/buses/buses_complex.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,96 @@
use winter_air::{Air, AirContext, Assertion, AuxTraceRandElements, EvaluationFrame, ProofOptions as WinterProofOptions, TransitionConstraintDegree, TraceInfo};
use winter_math::fields::f64::BaseElement as Felt;
use winter_math::{ExtensionOf, FieldElement};
use winter_utils::collections::Vec;
use winter_utils::{ByteWriter, Serializable};

pub struct PublicInputs {
inputs: [Felt; 2],
}

impl PublicInputs {
pub fn new(inputs: [Felt; 2]) -> Self {
Self { inputs }
}
}

impl Serializable for PublicInputs {
fn write_into<W: ByteWriter>(&self, target: &mut W) {
target.write(self.inputs.as_slice());
}
}

pub struct BusesAir {
context: AirContext<Felt>,
inputs: [Felt; 2],
}

impl BusesAir {
pub fn last_step(&self) -> usize {
self.trace_length() - self.context().num_transition_exemptions()
}
}

impl Air for BusesAir {
type BaseField = Felt;
type PublicInputs = PublicInputs;

fn context(&self) -> &AirContext<Felt> {
&self.context
}

fn new(trace_info: TraceInfo, public_inputs: PublicInputs, options: WinterProofOptions) -> Self {
let main_degrees = vec![TransitionConstraintDegree::new(2), TransitionConstraintDegree::new(2)];
let aux_degrees = vec![TransitionConstraintDegree::new(5), TransitionConstraintDegree::new(4)];
let num_main_assertions = 0;
let num_aux_assertions = 4;

let context = AirContext::new_multi_segment(
trace_info,
main_degrees,
aux_degrees,
num_main_assertions,
num_aux_assertions,
options,
)
.set_num_transition_exemptions(2);
Self { context, inputs: public_inputs.inputs }
}

fn get_periodic_column_values(&self) -> Vec<Vec<Felt>> {
vec![]
}

fn get_assertions(&self) -> Vec<Assertion<Felt>> {
let mut result = Vec::new();
result
}

fn get_aux_assertions<E: FieldElement<BaseField = Felt>>(&self, aux_rand_elements: &AuxTraceRandElements<E>) -> Vec<Assertion<E>> {
let mut result = Vec::new();
result.push(Assertion::single(0, 0, E::ONE));
result.push(Assertion::single(1, 0, E::ZERO));
result.push(Assertion::single(0, self.last_step(), E::ONE));
result.push(Assertion::single(1, self.last_step(), E::ZERO));
result
}

fn evaluate_transition<E: FieldElement<BaseField = Felt>>(&self, frame: &EvaluationFrame<E>, periodic_values: &[E], result: &mut [E]) {
let main_current = frame.current();
let main_next = frame.next();
result[0] = main_current[2] * main_current[2] - main_current[2];
result[1] = main_current[3] * main_current[3] - main_current[3];
}

fn evaluate_aux_transition<F, E>(&self, main_frame: &EvaluationFrame<F>, aux_frame: &EvaluationFrame<E>, _periodic_values: &[F], aux_rand_elements: &AuxTraceRandElements<E>, result: &mut [E])
where F: FieldElement<BaseField = Felt>,
E: FieldElement<BaseField = Felt> + ExtensionOf<F>,
{
let main_current = main_frame.current();
let main_next = main_frame.next();
let aux_current = aux_frame.current();
let aux_next = aux_frame.next();
result[0] = ((aux_rand_elements.get_segment_elements(0)[0] + E::ONE * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[0]) * aux_rand_elements.get_segment_elements(0)[2]) * E::from(main_current[2]) + E::ONE - E::from(main_current[2])) * ((aux_rand_elements.get_segment_elements(0)[0] + E::from(2_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[1]) * aux_rand_elements.get_segment_elements(0)[2]) * (E::ONE - E::from(main_current[2])) + E::ONE - (E::ONE - E::from(main_current[2]))) * aux_current[0] - ((aux_rand_elements.get_segment_elements(0)[0] + E::ONE * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[1]) * aux_rand_elements.get_segment_elements(0)[2]) * E::from(main_current[3]) + E::ONE - E::from(main_current[3])) * ((aux_rand_elements.get_segment_elements(0)[0] + E::from(2_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[0]) * aux_rand_elements.get_segment_elements(0)[2]) * (E::ONE - E::from(main_current[3])) + E::ONE - (E::ONE - E::from(main_current[3]))) * aux_next[0];
result[1] = (aux_rand_elements.get_segment_elements(0)[0] + E::from(3_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[0]) * aux_rand_elements.get_segment_elements(0)[2]) * (aux_rand_elements.get_segment_elements(0)[0] + E::from(3_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[0]) * aux_rand_elements.get_segment_elements(0)[2]) * (aux_rand_elements.get_segment_elements(0)[0] + E::from(4_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[1]) * aux_rand_elements.get_segment_elements(0)[2]) * aux_current[1] + (aux_rand_elements.get_segment_elements(0)[0] + E::from(3_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[0]) * aux_rand_elements.get_segment_elements(0)[2]) * (aux_rand_elements.get_segment_elements(0)[0] + E::from(4_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[1]) * aux_rand_elements.get_segment_elements(0)[2]) * E::from(main_current[2]) + (aux_rand_elements.get_segment_elements(0)[0] + E::from(3_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[0]) * aux_rand_elements.get_segment_elements(0)[2]) * (aux_rand_elements.get_segment_elements(0)[0] + E::from(4_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[1]) * aux_rand_elements.get_segment_elements(0)[2]) * E::from(main_current[2]) - ((aux_rand_elements.get_segment_elements(0)[0] + E::from(3_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[0]) * aux_rand_elements.get_segment_elements(0)[2]) * (aux_rand_elements.get_segment_elements(0)[0] + E::from(3_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[0]) * aux_rand_elements.get_segment_elements(0)[2]) * (aux_rand_elements.get_segment_elements(0)[0] + E::from(4_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[1]) * aux_rand_elements.get_segment_elements(0)[2]) * aux_next[1] + (aux_rand_elements.get_segment_elements(0)[0] + E::from(3_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[0]) * aux_rand_elements.get_segment_elements(0)[2]) * (aux_rand_elements.get_segment_elements(0)[0] + E::from(3_u64) * aux_rand_elements.get_segment_elements(0)[1] + E::from(main_current[0]) * aux_rand_elements.get_segment_elements(0)[2]) * E::from(main_current[4]));
}
}
Loading
Loading