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

Write general stack constraints in AirScript #239

Open
wants to merge 12 commits into
base: next
Choose a base branch
from

Conversation

Fumuran
Copy link
Contributor

@Fumuran Fumuran commented Mar 31, 2023

Addressing: #209
This PR adds constraints for every VM operation.

Comment on lines 615 to 620
ev mload(main: [s[16]], aux: [helper[3], clk, b_chip]):
let v = alpha[5] * s[0]' + sum([alpha[i + 5] * helper[3 - i]'])
let op_mem_read = 12
let u_mem = alpha[0] + alpha[1] * op_mem_read + alpha[3] * s[0] + alpha[4] * clk + v
enf f_mload(b) * (b_chip' * u_mem - b_chip) = 0
enf f_mload(b) * delta(s[i]) = 0 for i in 1..16
enf b_chip' * u_mem = b_chip
enf delta(s[i]) = 0 for i in 1..16
Copy link
Contributor

@bobbinth bobbinth Apr 4, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similar points to the previous comment: helper and clk columns are a part of the main trace (not auxiliary trace). Also, referencing random values should be done with $ prefix. I would rewrite this like this:

ev op_mload(main: [s[16], helpers[3], clk], aux: [b_chip]):
    # this is missing for part of the statement
    let v = $alpha[5] * s[0]' + sum([$alpha[i + 5] * helper[3 - i]'])
    let op_mem_read = 12
    let u_mem = $alpha[0] + $alpha[1] * op_mem_read + $alpha[3] * s[0] + $alpha[4] * clk + v
    enf b_chip' * u_mem = b_chip
    enf s[i]' = s[i] for i in 1..16 # this is missing constraint against s[0]

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure what constraint we should apply to the s[0]. For MLOAD we check memory access correctness and no change starting from position 1.

@Fumuran Fumuran force-pushed the andrew-stack-general-constraints branch from 6155c02 to 17cd103 Compare April 4, 2023 15:59

# Enforces the constraints on the stack.
# TODO: add docs for columns
ev stack_constraints(main: [stack[16], bookkeeping[2], h0, helper[6], clk, fmp], aux: [op_bits[7], extra, hasher5, b_chip, b_range]):
Copy link
Contributor

@bobbinth bobbinth Apr 4, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A few comments on these:

  • I would probably change stack to stack_top.
  • I'd combine bookkeeping and h0 into something like stack_helpers.
  • I'd rename helpers to op_helpers.
  • op_bits, extra are part of the main trace - not auxiliary trace. Also, I'd probably lump extra together with op_bits.
  • What is hasher5?

Overall, this could loo like so:

ev stack_constraints(
  main: [stack_top[16], stack_helpers[3], op_helper[6], op_bits[8], clk, fmp],
  aux: [hasher5, b_chip, b_range]
):

# No stack shift operations

ev noop(main: [s[16]]):
enf elem' = elem for elem in s
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since we are doing it everywhere else, we can probably use indexed access here as well. For example:

ev noop(main: [s[16]]):
    enf s[i]' = s[i] for i in 0..16


ev u32and(main: [s[16]], aux: [b_chip]):
let op_u32and = 2
enf b_chip' * ($alpha[0] + $alpha[1] * op_u32and + $alpha[2] * s[0] + $alpha[3] * s[1] + $alpha[4] * s[0]') = b_chip
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We'll probably need to put bus constraints into a separate module as they need to include both left and right sides of the bus, and here we are computing only the left side.

I'm thinking that we'd probably end up having each bus constraints being a separate module.

@Fumuran Fumuran force-pushed the andrew-stack-general-constraints branch from 30d6d60 to 22f05e1 Compare April 6, 2023 16:31
Comment on lines 382 to 386
fn compute_op_flags(op_bits: vector[8]) -> vector[88]:
return [
f_noop(op_bits),
f_eqz(op_bits),
f_neg(op_bits),
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure putting each operation flag into a separate function gives us much in terms of modularity or readability. Maybe we should get rid of individual functions and just add some comments here? For example, this could look like:

fn compute_op_flags(op_bits: vector[8]) -> vector[88]:
    return [
        f_000(op_bits) & f_x0000(op_bits), # noop
        f_000(op_bits) & f_x0001(op_bits), # eqz
        f_000(op_bits) & f_x0010(op_bits), # neg

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree. I thought that we would use each flag individually, but since we have the compute_op_flags function they lose their main purpose.

@Fumuran Fumuran force-pushed the andrew-stack-general-constraints branch 2 times, most recently from c83e9b9 to baa9d73 Compare April 12, 2023 17:38
@Fumuran Fumuran force-pushed the andrew-stack-general-constraints branch from 0f3097d to 445393e Compare June 6, 2023 13:43
@Fumuran Fumuran marked this pull request as ready for review June 6, 2023 14:33
Comment on lines 686 to 696
ev mstream([s[16], op_bits[8], op_helpers[6]]):
enf s[i]' = s[i] for i in 8..12
enf s[i]' = s[i] for i in 13..16
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should there also be another constraint to enforce that s[12]' = s[12] + 2?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed! I mistakenly decided that this constraint will be part of the bus constraint, but it is not. Thank you!

Copy link
Contributor

@tohrnii tohrnii left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you @Overcastan, looks great! I've left a few small comments. I haven't reviewed the u32 constraints yet.

Comment on lines 378 to 387
ev advpopw([s[16]]):
enf s[i]' = s[i] for i in 4..16

ev expacc([s[16], h0]):
enf is_binary([s[0]'])
enf s[1]' = s[1]^2
enf h0 = (s[1] - 1) * s[0]' + 1
enf s[2]' = s[2] * h0
enf s[3]' = s[3] * 2 + s[0]'
enf s[i]' = s[i] for i in 4..16
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: should these be moved below so that all mov operations are together? Also, should movup and movdn operations be clubbed separately? Might help with readability.

Comment on lines 434 to 439
ev ext2mul([s[16]]):
enf s[0]' = s[0]
enf s[1]' = s[1]
enf s[2]' = (s[0] + s[1]) * (s[2] + s[3]) - s[0] * s[2]
enf s[3]' = s[1] * s[3] - 2 * s[0] * s[2]
enf s[i]' = s[i] for i in 4..16
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: should we move this below and keep mov operations together?

Comment on lines 429 to 432
ev swapw([s[16]]):
enf s[i]' = s[i + 4] for i in 0..4
enf s[i + 4]' = s[i] for i in 0..4
enf s[i]' = s[i] for i in 8..16
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: should we move this below and keep mov operations together?

enf s[i]' = s[i] for i in 7..16

ev movup7([s[16]]):
enf s[0]' = s[7] = 0
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be enf s[0]' = s[7]

enf s[i]' = s[i] for i in 4..8
enf s[i]' = s[i] for i in 12..16

# Should we enforce that elements in position grater than 15 do not change?
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think they would change since we are swapping the first word with the last?

enf s[i + 12]' = s[i] for i in 0..4
enf s[i]' = s[i] for i in 4..12

# Should we enforce that elements in position grater than 15 do not change?
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think they would change since we are swapping those words.

Comment on lines 525 to 542
# Bus constraint is implemented in a separate file
ev mloadw([s[16], clk]):
enf s[i]' = s[i + 1] for i in 4..15

# Bus constraint is implemented in a separate file
ev mstore([s[16], clk]):
enf s[i]' = s[i + 1] for i in 0..15

# Bus constraint is implemented in a separate file
ev mstorew([s[16], clk]):
enf s[i]' = s[i + 1] for i in 0..15
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

question: Is the clk parameter for bus constraints? In that case, these should also take memory context I think.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just forget to remove clk from input values when I was moving bus constraints to the separate file, so both clk and ctx will be used for bus constraints and are not needed here. Great catch, thank you!

Comment on lines 210 to 225
ev check_element_validity([op_helpers[6]]):
let m = op_helpers[4]
let v_hi = 2^16 * op_helpers[3] + op_helpers[2]
let v_lo = 2^16 * op_helpers[1] + op_helpers[0]
enf (1 - m * (2^32 - 1 - v_hi)) * v_lo = 0


ev b0_is_zero([op_bits[8]]):
enf op_bits[6] & !op_bits[5] & op_bits[0] = 0


ev b0_b1_is_zero([op_bits[8]]):
enf op_bits[6] & op_bits[5] & op_bits[0] = 0
enf op_bits[6] & op_bits[5] & op_bits[1] = 0
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: It would be great to have comments for these.

@Fumuran Fumuran force-pushed the andrew-stack-general-constraints branch from 5208891 to d6c8555 Compare June 7, 2023 15:11
@Fumuran Fumuran requested a review from tohrnii June 9, 2023 21:18
Copy link
Contributor

@tohrnii tohrnii left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you. Looks good. Should the remaining constraints be added in the same PR or a follow up PR?

@@ -0,0 +1,739 @@
mod StacktAir
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: Typo


### Helper evaluators #############################################################################

# Enforces that the provided columns must be binary.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

minor nit: Should this be "Enforces that the provided columns are binary."

@Fumuran
Copy link
Contributor Author

Fumuran commented Jun 10, 2023

@tohrnii I think it will be better to add remaining constraints in a separate PR, because I'll need some time to understand how they work and come up with some constraints.

@grjte grjte removed their request for review June 12, 2023 13:57
@Fumuran Fumuran marked this pull request as draft June 20, 2023 20:12
@Fumuran Fumuran force-pushed the andrew-stack-general-constraints branch from 324367c to 31d2715 Compare June 21, 2023 14:23
@Fumuran Fumuran marked this pull request as ready for review June 21, 2023 15:07
@Fumuran Fumuran force-pushed the andrew-stack-general-constraints branch from 31d2715 to f2a39c2 Compare June 21, 2023 17:04
@Fumuran Fumuran force-pushed the andrew-stack-general-constraints branch from f2a39c2 to 146c947 Compare June 21, 2023 18:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

write MidenVM constraints for the stack (general) and determine operation flag handling
3 participants