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

Apply knowledge of constraints to SSA constant folding #4070

Closed
2 tasks
TomAFrench opened this issue Jan 17, 2024 · 0 comments · Fixed by #4060
Closed
2 tasks

Apply knowledge of constraints to SSA constant folding #4070

TomAFrench opened this issue Jan 17, 2024 · 0 comments · Fixed by #4060
Assignees
Labels
enhancement New feature or request

Comments

@TomAFrench
Copy link
Member

Currently we do not use the fact that we know a particular value is constrained to be equal to something else in SSA to simplify the circuit.

A glaring example of this is execution_success/references, this is currently represented by the SSA:

After Fill Internal Slice Dummy Data:
acir fn main f0 {
  b0(v0: Field):
    v1383 = add v0, Field 1
    v1384 = eq v1383, Field 3
    constrain v0 == Field 2
    constrain v0 == Field 2
    constrain v0 == Field 2
    constrain v0 == Field 2
    v1385 = eq v1383, Field 10
    v1386 = not v1385
    enable_side_effects v1386
    v1387 = eq v1383, Field 20
    v1388 = not v1387
    v1389 = mul v1386, v1388
    enable_side_effects v1386
    v1390 = cast v1388 as Field
    v1391 = cast v1387 as Field
    v1392 = mul v1390, Field 2
    v1393 = mul v1391, Field 15
    v1394 = add v1392, v1393
    enable_side_effects u1 1
    v1395 = cast v1386 as Field
    v1396 = cast v1385 as Field
    v1397 = mul v1395, v1394
    v1398 = mul v1396, Field 20
    v1399 = add v1397, v1398
    constrain v1399 == Field 2
    v1400 = eq Field 20, v1383
    v1401 = not v1400
    enable_side_effects u1 1
    v1402 = cast v1401 as Field
    v1403 = cast v1400 as Field
    v1404 = mul v1402, Field 15
    v1405 = mul v1403, Field 20
    v1406 = add v1404, v1405
    constrain v1406 == Field 15
    v1407 = not v1384
    enable_side_effects v1407
    v1408 = mul v1407, v1388
    enable_side_effects u1 1
    v1409 = cast v1407 as Field
    v1410 = cast v1384 as Field
    v1411 = mul v1409, v1394
    v1412 = mul v1410, Field 20
    v1413 = add v1411, v1412
    constrain v1413 == Field 20
    enable_side_effects u1 1
    v1414 = mul v1395, Field 2
    v1415 = add v1414, v1398
    constrain v1415 == Field 2
    enable_side_effects v1386
    v1416 = add v1392, v1391
    enable_side_effects u1 1
    v1417 = mul v1395, v1416
    enable_side_effects v1386
    v1418 = mul v1391, v1416
    v1419 = add v1392, v1418
    enable_side_effects v1386
    v1420 = mul v1391, v1419
    v1421 = add v1392, v1420
    enable_side_effects v1386
    v1422 = mul v1391, v1421
    v1423 = add v1392, v1422
    enable_side_effects v1386
    v1424 = mul v1391, v1423
    v1425 = add v1392, v1424
    enable_side_effects u1 1
    v1426 = mul v1395, v1425
    v1427 = add v1426, v1398
    constrain v1427 == Field 2
    enable_side_effects v1386
    v1428 = mul v1386, v1386
    enable_side_effects v1386
    v1429 = mul v1396, v1427
    v1430 = add v1417, v1429
    enable_side_effects v1386
    v1431 = mul v1396, v1430
    v1432 = add v1417, v1431
    enable_side_effects v1386
    v1433 = mul v1396, v1432
    v1434 = add v1417, v1433
    enable_side_effects v1386
    v1435 = mul v1396, v1434
    v1436 = add v1417, v1435
    enable_side_effects v1386
    v1437 = mul v1396, v1436
    v1438 = add v1417, v1437
    enable_side_effects u1 1
    v1439 = mul v1395, v1438
    v1440 = add v1439, v1398
    constrain v1440 == Field 2
    constrain v0 == Field 2 // See this line down here? What if it were at the top?
    return 
}

All of the previous instructions are irrelevant as they all follow from v0 == Field 2. If we knew that at the beginning then we could just remove all of those instructions. We then need to tackle the following tasks:

Tasks

Preview Give feedback
@TomAFrench TomAFrench added the enhancement New feature or request label Jan 17, 2024
@TomAFrench TomAFrench self-assigned this Jan 17, 2024
@github-project-automation github-project-automation bot moved this to 📋 Backlog in Noir Jan 17, 2024
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.
@github-project-automation github-project-automation bot moved this from 📋 Backlog to ✅ Done in Noir Feb 7, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
Archived in project
Development

Successfully merging a pull request may close this issue.

1 participant