State machine AIR

[shaharsamocha7]

This change is 

[shaharsamocha7]

• trace in bit reverse order #857
• State machine prover #845
• State machine AIR #841 👈
• Add constraint for Logup claimed cumsum #830
• Logup generator returns multiple prefix sums #829
• Logup - rename claimed_sum to total_sum #825
• Revert logup without is_first #818
• dev

This stack of pull requests is managed by Graphite. Learn more about stacking.

Join @shaharsamocha7 and the rest of your teammates on Graphite

[codecov-commenter]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 91.91%. Comparing base (6e649fc) to head (7372a06).
Report is 3 commits behind head on dev.

Additional details and impacted files

@@           Coverage Diff           @@
##              dev     #841   +/-   ##
=======================================
  Coverage   91.91%   91.91%           
=======================================
  Files          90       90           
  Lines       12375    12375           
  Branches    12375    12375           
=======================================
  Hits        11374    11374           
  Misses        892      892           
  Partials      109      109           

Flag	Coverage Δ
	91.91% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[Alon-Ti]

Reviewed 4 of 4 files at r1, all commit messages.
Reviewable status: all files reviewed, 8 unresolved discussions (waiting on @shaharsamocha7)

---

crates/prover/src/examples/state_machine/components.rs line 8 at r1 (raw file):

use crate::core::lookups::utils::Fraction;

pub const N_STATE: usize = 2;

STATE_SIZE / STATE_LEN / N_FELTS_IN_STATE.

Code quote:

N_STATE

---

crates/prover/src/examples/state_machine/components.rs line 9 at r1 (raw file):

pub const N_STATE: usize = 2;
pub type StateMachineElements = LookupElements<N_STATE>;

Since this is the usage example, document what the sum with multiple lookup elements should look like.

---

crates/prover/src/examples/state_machine/components.rs line 14 at r1 (raw file):

/// Transition `INDEX` of state increments the state by 1 at that offset.
#[derive(Clone)]
pub struct StateTransitionEval<const INDEX: usize> {

COORDINATE?

Code quote:

INDEX

---

crates/prover/src/examples/state_machine/components.rs line 25 at r1 (raw file):

    }
    fn max_constraint_log_degree_bound(&self) -> u32 {
        self.log_n_rows + 1

LOG_BLOW_UP_FACTOR

Code quote:

1

---

crates/prover/src/examples/state_machine/components.rs line 32 at r1 (raw file):

        let input_state: [_; N_STATE] = std::array::from_fn(|_| eval.next_trace_mask());
        let q0: E::EF = self.lookup_elements.combine(&input_state);

input_denom

Code quote:

q0

---

crates/prover/src/examples/state_machine/gen.rs line 27 at r1 (raw file):

    inc_index: usize,
) -> ColumnVec<CircleEvaluation<SimdBackend, M31, BitReversedOrder>> {
    let n_lanes = PackedM31::broadcast(M31::from_u32_unchecked(N_LANES as u32));

Isn't there AddAssign<M31> for PackedM31? If not maybe it's clearer to implement that that to generate this.

---

crates/prover/src/examples/state_machine/gen.rs line 61 at r1 (raw file):

) {
    let ones = PackedM31::broadcast(M31::one());
    let n_lanes_minus_one = PackedM31::broadcast(M31::from_u32_unchecked(N_LANES as u32)) - ones;

Same as above.

---

crates/prover/src/examples/state_machine/gen.rs line 72 at r1 (raw file):

    for vec_row in 0..(1 << (log_size - LOG_N_LANES)) {
        let q0: PackedQM31 = lookup_elements.combine(&packed_state);

Same as above.

Code quote:

q0

[shaharsamocha7]

Reviewable status: 1 of 4 files reviewed, 8 unresolved discussions (waiting on @Alon-Ti)

---

crates/prover/src/examples/state_machine/components.rs line 8 at r1 (raw file):

Previously, Alon-Ti wrote…

STATE_SIZE / STATE_LEN / N_FELTS_IN_STATE.

Done.

---

crates/prover/src/examples/state_machine/components.rs line 9 at r1 (raw file):

Previously, Alon-Ti wrote…

Since this is the usage example, document what the sum with multiple lookup elements should look like.

Done
I think we should document the LookupElements better in the struct itself.

---

crates/prover/src/examples/state_machine/components.rs line 14 at r1 (raw file):

Previously, Alon-Ti wrote…

COORDINATE?

Done.

---

crates/prover/src/examples/state_machine/components.rs line 25 at r1 (raw file):

Previously, Alon-Ti wrote…

LOG_BLOW_UP_FACTOR

Done
This is not due to the blow_up factor, this is defined in the PCS.
Here the +1 is because the log constraint degree is 1.

---

crates/prover/src/examples/state_machine/components.rs line 32 at r1 (raw file):

Previously, Alon-Ti wrote…

input_denom

Done.

---

crates/prover/src/examples/state_machine/gen.rs line 27 at r1 (raw file):

Previously, Alon-Ti wrote…

Isn't there AddAssign<M31> for PackedM31? If not maybe it's clearer to implement that that to generate this.

I think we don't have that.
Also that kind of implementation will use PackedM31::broadcast each time, no?

---

crates/prover/src/examples/state_machine/gen.rs line 61 at r1 (raw file):

Previously, Alon-Ti wrote…

Same as above.

Same as above

---

crates/prover/src/examples/state_machine/gen.rs line 72 at r1 (raw file):

Previously, Alon-Ti wrote…

Same as above.

Done.

[Alon-Ti]

up to the stylistic suggestions.

Reviewed 3 of 3 files at r2, all commit messages.
Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @shaharsamocha7)

---

crates/prover/src/examples/state_machine/components.rs line 9 at r1 (raw file):

Previously, shaharsamocha7 wrote…

Done
I think we should document the LookupElements better in the struct itself.

I agree, add TODO?

---

crates/prover/src/examples/state_machine/gen.rs line 27 at r1 (raw file):

Previously, shaharsamocha7 wrote…

I think we don't have that.
Also that kind of implementation will use PackedM31::broadcast each time, no?

It can (but you could also not generate another packed element, maybe this could be better if we increase VeryPacked size too much), but it'll be cleaner here.

[shaharsamocha7]

Reviewable status: 2 of 4 files reviewed, 1 unresolved discussion (waiting on @Alon-Ti)

---

crates/prover/src/examples/state_machine/components.rs line 9 at r1 (raw file):

Previously, Alon-Ti wrote…

I agree, add TODO?

On a second thought I think that the lookup elements doesn't need more documentation

---

crates/prover/src/examples/state_machine/gen.rs line 27 at r1 (raw file):

Previously, Alon-Ti wrote…

It can (but you could also not generate another packed element, maybe this could be better if we increase VeryPacked size too much), but it'll be cleaner here.

Removed.

[shaharsamocha7]

Merge activity

• Sep 26, 10:27 AM EDT: @shaharsamocha7 started a stack merge that includes this pull request via Graphite.
• Sep 26, 10:27 AM EDT: @shaharsamocha7 merged this pull request with Graphite.