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

Valid slice access fails constraint #2645

Closed
vezenovm opened this issue Sep 11, 2023 · 2 comments · Fixed by #2647
Closed

Valid slice access fails constraint #2645

vezenovm opened this issue Sep 11, 2023 · 2 comments · Fixed by #2647
Assignees
Labels
bug Something isn't working

Comments

@vezenovm
Copy link
Contributor

Aim

Merging slices based off of witness values requires tracking a user facing dynamic slice length (original issue here: #1889). This required adding a slice access check before any slice access. I expect to have accurate error locations and slice length checks.

Expected Behavior

When I do something like this:

fn main(x: Field, y: Field) {
 let slice = merge_slices_mutate(x, y);
 assert(slice.len() == 3);
 assert(slice[3] == 5);
}

fn merge_slices_mutate(x: Field, y: Field) -> [Field] {
    let mut slice = [0; 2];
    if x != y {
        slice = slice.push_back(y);
        slice = slice.push_back(x);
    } else {
        slice = slice.push_back(x);
    }
    slice
}

I should have a constraint failure at assert(slice.len() == 3);

Bug

The line slice.len() == 3 should be where I get a failed constraint. But instead I get a failed constraint here assert(slice[3] == 5);. This is due to us replacing the dynamic value for the length during SSA when it should be checked during runtime.

To Reproduce

  1. Use snippet posted above
  2. Run nargo execute
  3. See output failure at assert(slice[3] == 5);

Installation Method

Compiled from source

Nargo Version

nargo 0.11.1 (git version hash: 3847e9c, is dirty: true)

Additional Context

No response

Would you like to submit a PR for this Issue?

No

Support Needs

No response

@vezenovm vezenovm added the bug Something isn't working label Sep 11, 2023
@vezenovm
Copy link
Contributor Author

This is happening after this PR (#2483) which is a useful optimizations in some instances but can lead to mismatched constraints when we are re-using SSA values internally. After removing the changes in #2483 though the error is not much clearer as it looks there is missing location information.

@vezenovm vezenovm self-assigned this Sep 11, 2023
@vezenovm
Copy link
Contributor Author

#2476 looks to be the cause of the missing location data as we use an iterator which is lazy and is thus doing nothing. So we are just taking self.locations but not inserting anything.

github-merge-queue bot pushed a commit that referenced this issue Feb 7, 2024
# Description

## Problem\*

Resolves #4070

## Summary\*

This PR uses `Instruction::Constrain` to perform simplifications in SSA
where one value is swapped for another simpler value due to the fact
that the circuit will be unsatisfiable should the two values not be
equivalent (because of the `Instruction::Constrain`.

A previous implementation of this resulted in the bug
#2645. This was because
constraints which were only active in certain areas of the code were
applied across all of the SSA. This implementation avoids this by using
a separate cache for the constrained values for each value of
`side_effects_enabled_var`. This means that passing a
`Instruction::EnableSideEffects` instruction will "forget" any
constraints which aren't currently active.

One trouble from this PR is that we now require multiple passes in order
to fully simplify the circuit. I've simply added another set of the
final 3 passes but we could in future perform extra passes until the SSA
stabilises.

## Additional Context



## Documentation\*

Check one:
- [x] No documentation needed.
- [ ] Documentation included in this PR.
- [ ] **[Exceptional Case]** Documentation to be submitted in a separate
PR.

# PR Checklist\*

- [x] I have tested the changes locally.
- [x] I have formatted the changes with [Prettier](https://prettier.io/)
and/or `cargo fmt` on default settings.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
Archived in project
Development

Successfully merging a pull request may close this issue.

1 participant