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

Sort boundary constraints #315

Open
hackaugusto opened this issue Jun 17, 2023 · 1 comment
Open

Sort boundary constraints #315

hackaugusto opened this issue Jun 17, 2023 · 1 comment

Comments

@hackaugusto
Copy link
Contributor

The order in which the boundary constraints are defined is important. For example:

boundary_constraints:
    enf p.last = 1
    enf p.first = 1

Is not the same as:

boundary_constraints:
    enf p.first = 1
    enf p.last = 1

The first will emit the following code for the winterfell backend:

    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(0, self.last_step(), E::ONE));
        result
    }

And the later

    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, self.last_step(), E::ONE));
        result.push(Assertion::single(0, 0, E::ONE));
        result
    }

The issue is that the order of Vec<Assertion<E>> determines the order of the composition coefficients, so proofs of the two systems above are not interchangeable. Additionally, this may introduce bugs across different backends, since the order of the coefficients is implicitly defined and can easily become out of sync.

To fix the issue above an ordering is required. A proposal is to sort by (trace, column_name, step), similar to #314

@hackaugusto
Copy link
Contributor Author

hackaugusto commented Jun 17, 2023

On thing that I forgot. Winterfell does sort assertions by something similar to (stride, step, column), which is total. So the proofs should be fine, unlike what I wrote above. The issue is more on the backends.

Edit: To implement this some changes to the IR are necessary. The information is lost when creating the Algebraic graph, since the boundary constraint can be defined in term of other columns, enf a.first = b, looking for the trace access is not sufficient. And when the constraint boundary definitions are not forwarded from the constraint builder to the air definition.

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

No branches or pull requests

1 participant