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

Add validity constraints #84

Closed
Tracked by #75 ...
tohrnii opened this issue Nov 28, 2022 · 7 comments
Closed
Tracked by #75 ...

Add validity constraints #84

tohrnii opened this issue Nov 28, 2022 · 7 comments
Assignees

Comments

@tohrnii
Copy link
Contributor

tohrnii commented Nov 28, 2022

We should add support for defining validity constraints. These constraints would be similar to transition constraints, with the only exception that they would work only with the current row of the trace. For example:

trace_columns:
    main: [a, b, c]

integrity_constraints:
    enf a^2 - a = 0    # this is a validity constraint

These constraints should be in the same section as transition constraints however we should change the name of the combined section to integrity_constraints (or something similar). Also, in the IR we should still probably have a single algebraic DAG, but we could mark entry points as transition vs. validity constraints.

Originally posted by @bobbinth in #53.

@grjte
Copy link
Contributor

grjte commented Nov 29, 2022

I think integrity_constraints is fine as a name

@grjte
Copy link
Contributor

grjte commented Nov 29, 2022

Our existing "transition_constraints" currently includes both validity and transition constraints, so the only change needed there is to distinguish between the constraint types in the IR.

I think the tasklist for this issue looks something like the following:

  • rename transition_constraints to integrity_constraints
  • in the IR, identify constraints as "validity" or "transition" while adding them to the graph, and label them somehow in the entry point lists

Question: Instead of tracking 1 array of entry nodes should we track 2 arrays of constraint entry nodes - one for validity constraints and one for transition constraints? We don't need this for Miden, but it would be needed for something like Polygon Zero.

@bobbinth what do you think?

@bobbinth
Copy link
Contributor

For what we need now, two separate arrays will probably suffice, but I wonder if we should make this even more general for what we might do in the future. Specifically, each entry point could contain a set of row offsets used for a given constraints. The offsets here would be similar to the ones mentioned in #54.

For example, if the set of offsets consists of a single offset 0, then this is a validity constraint. If the set of offsets consists of offsets 0 and 1, this is a transition constraint. In the future, we might have different types of transition constraints - e.g., a constraint which accesses rows 0, 1, and 5 or something like that.

@grjte
Copy link
Contributor

grjte commented Dec 1, 2022

Sure, I think this makes sense to do. The more general approach is better for the future, and it's probably equal work, since making the change for #54 will probably help with identifying validity vs. transition constraints.

That means this issue is blocked by #54 and we should do that first.

Then for this issue, we would need to update the way constraints are tracked, so that instead of an array of NodeIndex (entry points to the constraint in the AlgebraicGraph), we would use something else that has the NodeIndex data and the row offset data?

@bobbinth
Copy link
Contributor

bobbinth commented Dec 1, 2022

Agreed! And yes, instead of just NodeIndex it would be some struct which could look like this:

struct ConstraintRoot {
    index: NodeIndex,
    offsets: Vec<usize>,
}

(open to changing any of the names in the above)

@grjte
Copy link
Contributor

grjte commented Dec 20, 2022

@Overcastan since there are 2 steps required, I recommend that the first PR just handles the renaming

  • rename transition_constraints to integrity_constraints
  • in the IR, identify constraints as "validity" or "transition" while adding them to the graph, and label them somehow in the entry point lists

@grjte
Copy link
Contributor

grjte commented Jan 18, 2023

closed by #111

@grjte grjte closed this as completed Jan 18, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

4 participants