-
Notifications
You must be signed in to change notification settings - Fork 122
Find and replace functions that compute "are all equal zero" #3046
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
Open
chriseth
wants to merge
323
commits into
main
Choose a base branch
from
seqz
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
+1,058
−164
Open
Changes from 1 commit
Commits
Show all changes
323 commits
Select commit
Hold shift + click to select a range
f37f0e4
Apply split.
chriseth 354aa7c
adjustments
chriseth 5757c59
try to support nonzero constants.
chriseth 29b56d4
Compute unique modular solution.
chriseth 59d036b
more impl
chriseth 964bd4a
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth de909cd
fix
chriseth 63e74d3
Add some more tests.
chriseth 42437cc
try something
chriseth cd1103d
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth df0d55b
fix
chriseth 035f464
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth 2a50fec
comment
chriseth 1c0bcf5
debug info.
chriseth b524f69
remove debug
chriseth 94182fa
Handle negative offset
chriseth 6af1c34
Add constraints.
chriseth 13a1e5c
Update expectations.
chriseth fe255d0
Merge remote-tracking branch 'origin/main' into seqz
chriseth 8a2cf42
Update expectations.
chriseth ca42418
Update constraints.
chriseth d52a893
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth 417646d
clippy
chriseth 11de0fb
Add test for sltu_2
chriseth b562ba2
Fix for negative.
chriseth d817d9b
Update expectations.
chriseth 8afe6fe
Add test case.
chriseth cdffdee
Extract negation.
chriseth 550019c
Remove negation.
chriseth 8dcde91
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth fd12e5d
update constraints
chriseth db7cbc4
Update expectations.
chriseth ca5395f
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth 1a91941
cleanup
chriseth a54bd4e
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth 7504689
Update expectations.
chriseth cd95a52
Update expectations.
chriseth eab2e3e
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth df866be
Move constraint splitting into the solver.
chriseth 02ca577
refactor
chriseth aa376e0
more
chriseth 1ad6271
more
chriseth ce4cb1b
more
chriseth 90ac6d9
refactor
chriseth 2b92494
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth f1342a4
Negate constant.
chriseth eefaa24
Un-scope test.
chriseth 4139c68
cleanup
chriseth 0bd3fda
remove comments.
chriseth 922cef9
simplify
chriseth d14e6ef
remove todo
chriseth 90c91e2
Apply equivalences.
chriseth 5e629e8
Update expectations.
chriseth a6becf3
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth a2969c2
Update expectations.
chriseth e5077c4
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth 30ab418
Update expectations.
chriseth 4bf2df4
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth a85ba9d
wip
chriseth 35d1c0d
Use RuntimeConstant instead of FieldElement.
chriseth 84e277a
Merge branch 'use_runtime_constant' into quadratic_equiv_revamped
chriseth 4619d3d
Introduce AlgebraicConstraint.
chriseth 624738f
debug
chriseth c12a7db
Display for Block.
chriseth 6c35d16
Merge branch 'display_for_block' into quadratic_equiv_revamped
chriseth 01f071d
Add test.
chriseth f02386c
add test
chriseth d6b6d4d
test.
chriseth 8d7b5c5
Another test.
chriseth 336a25d
simplify test.
chriseth 6111134
Adjust tests.
chriseth b91f0e7
More restricted.
chriseth 6d0618e
Potential fix.
chriseth 4f065eb
extend
chriseth 07ed16f
update expectations
chriseth cce9c66
update expectations
chriseth c4287c7
Add test file.
chriseth 61f0d65
Improve bounds
chriseth d084ec4
Add test.
chriseth b328b02
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth 9e3cd4a
cleanup
chriseth 25e5c04
Only add new constraints.
chriseth 7dec5f0
cleanup
chriseth 0ad5b4d
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth e5028f6
cleanup
chriseth 59840e0
Merge remote-tracking branch 'origin/main' into seqz
chriseth 92e77ac
Merge branch 'quadratic_equiv_revamped' into seqz
chriseth 6433555
Re-add new variable and update expectations.
chriseth 5f4ddec
Remove print statements.
chriseth ac0490a
No need to constrain result.
chriseth 795aa74
Try to figure out if the constraints to delete are redundant.
chriseth 94fc7b5
Explain grouping.
chriseth 6683be7
Update constraint-solver/src/solver/constraint_splitter.rs
chriseth 0902838
Apply suggestion from @Schaeff
chriseth bddbd5c
Move comment.
chriseth 19be95b
Clarify comment.
chriseth 2f3c075
document
chriseth 3338a8b
avoid clone.
chriseth 5b2e954
Rename tests.
chriseth ccf14bc
Add some negative tests.
chriseth e91c4f6
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth 5cf2b2f
More details for docstring.
chriseth b479bc9
Do some early range constraint checks.
chriseth 998d31a
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth 67ed03d
Improvement on checking redundancy.
chriseth bb0663c
reduce restrictions
chriseth f695710
Completed "determine_redundancy"
chriseth ded6df0
Move reachability.
chriseth b519bfc
Use RuntimeConstant.
chriseth 49729e1
Use indexed system for reachability search.
chriseth 3a37d82
System splitter.
chriseth 54d0168
Move all bounds to where clause.
chriseth 2d474c3
Also return blocking variables as reachable variables.
chriseth 12e4745
Merge branch 'adjust_reachability' into seqz
chriseth 02ef28f
review
chriseth 87698c6
Merge branch 'move_reachability' into adjust_reachability
chriseth 8eb3efd
Merge branch 'move_reachability' into system_splitter
chriseth 542f0b4
Merge branch 'adjust_reachability' into seqz
chriseth 4614cd2
Merge branch 'system_splitter' into seqz
chriseth aa019bf
Try split system.
chriseth 7bb4a15
cleanup
chriseth b9e5928
Update expectations.
chriseth 9f03c65
Merge branch 'move_reachability'
chriseth 7b2d553
Merge branch 'main' into adjust_reachability
chriseth 293a32d
Merge branch 'adjust_reachability' into seqz
chriseth 8371de3
Split the function at a different point.
chriseth 7ca2542
Merge branch 'quadratic_equiv_revamped' into seqz
chriseth 4d73c1f
solve merge conflicts.
chriseth d0188b1
review
chriseth db7a187
update comment
chriseth b04c6d2
Merge remote-tracking branch 'origin/main' into quadratic_equiv_revamped
chriseth 639e43f
Merge branch 'adjust_reachability'
chriseth 902a2c5
Merge branch 'main' into system_splitter
chriseth 6ba0ff2
Merge branch 'system_splitter' into seqz
chriseth 6c46216
Merge branch 'quadratic_equiv_revamped' into seqz
chriseth 625ab8f
cleanup
chriseth df6a955
Merge remote-tracking branch 'origin/main' into seqz
chriseth 913f7f4
'fix' test
chriseth 47016c1
Merge branch 'quadratic_equiv_revamped'
chriseth c791393
Merge branch 'main' into seqz
chriseth ac771e9
Merge remote-tracking branch 'origin/main' into seqz
chriseth 2fb1a0a
Add ability to create new variables.
chriseth 98bf73d
Merge branch 'new_var' into seqz
chriseth 696dfcf
Try to derive computation method.
chriseth 19b9483
clippy
chriseth 892cdd4
Try to match pattern.
chriseth 7aed8d1
Relax bounds for GroupedExpression.
chriseth 0e3eb11
Split into parts and relax bounds.
chriseth da7b969
Relax mul
chriseth 7920df3
Relax mul.
chriseth 606018e
Merge branch 'relax_bounds' into seqz
chriseth c9d39e2
Revert "Merge branch 'relax_bounds' into seqz"
chriseth 9eed819
Merge remote-tracking branch 'origin/main' into seqz
chriseth 044ea81
Add derived columns.
chriseth 673b4a7
Update computation methods.
chriseth b2e9897
We usually always mean unknown variables.
chriseth 8eab301
Remove ReferencedSymbols trait.
chriseth e5ceff7
Some more derived columns work.
chriseth db01624
Merge remote-tracking branch 'origin/main' into derived_columns
chriseth 2141640
more stuff
chriseth 5696552
Merge branch 'use_unknown_variables'
chriseth 0498d36
Merge branch 'main' into derived_columns
chriseth fbf1786
clippy
chriseth baeffe1
Merge remote-tracking branch 'origin/main' into derived_columns
chriseth 16e55c8
docstrings
chriseth faa6731
more work on derived columns.
chriseth 3fb138f
substitute.
chriseth 71ecdd4
Merge remote-tracking branch 'origin/main' into derived_columns
chriseth 7b54eb5
Remove derived variables.
chriseth 0576c80
fix
chriseth 33e8e06
update type in machine.
chriseth 38099a2
Update cbor files.
chriseth f467bc8
clippy
chriseth fc6ebee
Merge remote-tracking branch 'origin/main' into seqz
chriseth ce8cb7d
Merge branch 'derived_columns' into seqz
chriseth 91224ad
Add derived variable.
chriseth ec9b5fa
Use range constraints in exhaustive search.
chriseth d52abf4
clippy
chriseth cf4c8f0
Test updates.
chriseth 50ef402
fix
chriseth e64c8f1
Update expectations.
chriseth f601bd1
more updates.
chriseth 41bdc7e
Add some early return.
chriseth 3a701a0
Track unsuccessful sets.
chriseth a716ee6
Merge remote-tracking branch 'origin/main' into seqz
chriseth 1abc438
Fix merge problems.
chriseth eccbff4
Merge remote-tracking branch 'origin/main' into seqz
chriseth 0d546b8
Apply suggestion from @chriseth
chriseth b09207e
Undo merge problems.
chriseth 90874bc
Merge remote-tracking branch 'origin/main' into use_range_constraints…
chriseth bdc21a8
Update docstrings.
chriseth dd7de27
Rename functions.
chriseth 3aa3e96
Review.
chriseth 08ec4bb
Merge remote-tracking branch 'origin/main' into use_range_constraints…
chriseth ab2bc32
Merge remote-tracking branch 'origin/main' into seqz
chriseth f865064
Merge remote-tracking branch 'origin/main' into seqz
chriseth 51ab148
Cleanup
chriseth 7503a44
Re-index before split.
chriseth d9846ba
Optimize system splitting.
chriseth b327682
Allow iter over hash.
chriseth 29f6870
Clean up comments.
chriseth 5ff42bf
Cleanup
chriseth c66e937
cleanup
chriseth 716e493
Merge remote-tracking branch 'origin/main' into seqz
chriseth cb3c6eb
Improve system splitter speed.
chriseth 392d719
Merge remote-tracking branch 'origin/faster_system_splitter' into seqz
chriseth a727058
update comment.
chriseth dd1eed3
Another comment update.
chriseth 5973951
Merge branch 'faster_system_splitter' into seqz
chriseth 4bddb1a
Merge remote-tracking branch 'origin/main' into seqz
chriseth 199f179
Merge remote-tracking branch 'origin/main' into seqz
chriseth 9b14805
Update expectations.
chriseth f138fb0
Document and tune.
chriseth 3fce698
Update expectations.
chriseth 52f3726
Fix merge conflict.
chriseth d1731ed
fix
chriseth 7d170ac
Reduce changes to outside code.
chriseth e9133b6
Use existing column allocator.
chriseth e41f566
Adjust expectations.
chriseth b6057d7
Update expectations.
chriseth 3c4fb10
Extend product combination.
chriseth ea6688c
Merge remote-tracking branch 'origin/main' into seqz
chriseth 968689d
Merge remote-tracking branch 'origin/main' into use_range_constraints…
chriseth d9127d1
Merge branch 'use_range_constraints_in_exhaustive_search' into seqz
chriseth 5ec7e4e
Undo change to range constraints.
chriseth 064ee28
cleanup
chriseth a8780b4
cleanup
chriseth 366a325
Fixes.
chriseth 795d3bf
fix
chriseth 2e1684d
Fix?
chriseth a7cf50c
simplify
chriseth 7139a42
Adjust mask after addition.
chriseth 83e7b2c
cleanup
chriseth c8881cb
Adjust mask after addition.
chriseth 22bb850
Merge branch 'adjust_mask_after_addition' into seqz
chriseth ef60ba5
Avoid conjunctions.
chriseth 03dc6ae
cleanup
chriseth 6737ff6
Merge remote-tracking branch 'origin/main' into use_range_constraints…
chriseth c26f42c
Update expectations.
chriseth 3536d07
Merge remote-tracking branch 'origin/main' into use_range_constraints…
chriseth 0bf6a5d
Merge remote-tracking branch 'origin/main' into use_range_constraints…
chriseth 93edd6f
Merge branch 'use_range_constraints_in_exhaustive_search'
chriseth add2adb
Merge branch 'main' into seqz
chriseth 25755d6
Fix clippy.
chriseth a6aa4dd
Update constraint-solver/src/solver/base.rs
chriseth c97a173
Update autoprecompiles/src/constraint_optimizer/equal_zero_checks.rs
chriseth f1edea9
Update autoprecompiles/src/constraint_optimizer/equal_zero_checks.rs
chriseth ccc46b9
Update autoprecompiles/src/constraint_optimizer/equal_zero_checks.rs
chriseth 1e53628
Review comments.
chriseth 80f155a
Merge branch 'seqz' of ssh://github.com/powdr-labs/powdr into seqz
chriseth File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,40 @@ | ||
| // Bus 0 (EXECUTION_BRIDGE): | ||
| mult=-is_valid, args=[from_state__pc_0, writes_aux__base__prev_timestamp_0 + writes_aux__base__timestamp_lt_aux__lower_decomp__0_0 + 131072 * writes_aux__base__timestamp_lt_aux__lower_decomp__1_0 - 1] | ||
| mult=is_valid, args=[from_state__pc_0 + 4, writes_aux__base__prev_timestamp_0 + writes_aux__base__timestamp_lt_aux__lower_decomp__0_0 + 131072 * writes_aux__base__timestamp_lt_aux__lower_decomp__1_0 + 2] | ||
|
|
||
| // Bus 1 (MEMORY): | ||
| mult=is_valid * -1, args=[1, 116, b__0_0, b__1_0, b__2_0, b__3_0, writes_aux__base__prev_timestamp_0 + writes_aux__base__timestamp_lt_aux__lower_decomp__0_0 + 131072 * writes_aux__base__timestamp_lt_aux__lower_decomp__1_0 - (reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0 + 131072 * reads_aux__0__base__timestamp_lt_aux__lower_decomp__1_0 + 2)] | ||
| mult=is_valid * 1, args=[1, 116, cmp_result_0, 0, 0, 0, writes_aux__base__prev_timestamp_0 + writes_aux__base__timestamp_lt_aux__lower_decomp__0_0 + 131072 * writes_aux__base__timestamp_lt_aux__lower_decomp__1_0 + 1] | ||
|
|
||
| // Bus 2 (PC_LOOKUP): | ||
| mult=is_valid, args=[from_state__pc_0, 4351, 0, 0, 0, 0, 0, 0, 0] | ||
|
|
||
| // Bus 3 (VARIABLE_RANGE_CHECKER): | ||
| mult=is_valid * 1, args=[reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0, 17] | ||
| mult=is_valid * 1, args=[reads_aux__0__base__timestamp_lt_aux__lower_decomp__1_0, 12] | ||
| mult=is_valid * 1, args=[writes_aux__base__timestamp_lt_aux__lower_decomp__0_0, 17] | ||
| mult=is_valid * 1, args=[writes_aux__base__timestamp_lt_aux__lower_decomp__1_0, 12] | ||
|
|
||
| // Bus 6 (BITWISE_LOOKUP): | ||
| mult=diff_marker__0_0 + diff_marker__1_0 + diff_marker__2_0 + diff_marker__3_0, args=[diff_val_0 - 1, 0, 0, 0] | ||
| mult=is_valid * 1, args=[b_msb_f_0, 0, 0, 0] | ||
|
|
||
| // Algebraic constraints: | ||
| cmp_result_0 * (cmp_result_0 - 1) = 0 | ||
| (b__3_0 - b_msb_f_0) * (b_msb_f_0 + 256 - b__3_0) = 0 | ||
| diff_marker__3_0 * (diff_marker__3_0 - 1) = 0 | ||
| -((1 - diff_marker__3_0) * (b_msb_f_0 * (2 * cmp_result_0 - 1))) = 0 | ||
| diff_marker__3_0 * (b_msb_f_0 * (2 * cmp_result_0 - 1) + diff_val_0) = 0 | ||
| diff_marker__2_0 * (diff_marker__2_0 - 1) = 0 | ||
| -((1 - (diff_marker__2_0 + diff_marker__3_0)) * (b__2_0 * (2 * cmp_result_0 - 1))) = 0 | ||
| diff_marker__2_0 * (b__2_0 * (2 * cmp_result_0 - 1) + diff_val_0) = 0 | ||
| diff_marker__1_0 * (diff_marker__1_0 - 1) = 0 | ||
| -((1 - (diff_marker__1_0 + diff_marker__2_0 + diff_marker__3_0)) * (b__1_0 * (2 * cmp_result_0 - 1))) = 0 | ||
| diff_marker__1_0 * (b__1_0 * (2 * cmp_result_0 - 1) + diff_val_0) = 0 | ||
| diff_marker__0_0 * (diff_marker__0_0 - 1) = 0 | ||
| (1 * is_valid - (diff_marker__0_0 + diff_marker__1_0 + diff_marker__2_0 + diff_marker__3_0)) * ((1 - b__0_0) * (2 * cmp_result_0 - 1)) = 0 | ||
| diff_marker__0_0 * ((b__0_0 - 1) * (2 * cmp_result_0 - 1) + diff_val_0) = 0 | ||
| (diff_marker__0_0 + diff_marker__1_0 + diff_marker__2_0 + diff_marker__3_0) * (diff_marker__0_0 + diff_marker__1_0 + diff_marker__2_0 + diff_marker__3_0 - 1) = 0 | ||
| (1 - (diff_marker__0_0 + diff_marker__1_0 + diff_marker__2_0 + diff_marker__3_0)) * cmp_result_0 = 0 | ||
| (1 - is_valid) * (diff_marker__0_0 + diff_marker__1_0 + diff_marker__2_0 + diff_marker__3_0) = 0 | ||
| is_valid * (is_valid - 1) = 0 | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The code starting here should be equivalent to
(where
acorresponds tob__0_0,bcorresponds tob__1_0etc.)these are 13 columns, while the present code also has 13 columns, but performs two bitwise lookups.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If we allow two bitwise lookups, we get
Which has only 11 columns. Adding another bitwise lookup we get to
which only has 9 columns.
Maybe it also makes sense to subtract 5 from the columns (4 inputs, one output), because those will likely be consumed by the preceding and following instructions. Then we would have
two lookups: from 8 to 6
three lookups: from 8 to 4
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actually it's even simpler.
We know that
0 <= a, b, c, d <= 255. Because of that, if we definex = a + b + c + d, then0 <= x <= 0x3fcwhich is less than half the modulus. This means thatxis zero if and only if all ofa, b, c, dare zero.Now the system reads:
Of course, we can always inline
x, and thus we have only one additional column, zero lookups and 6 columns in total.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The slight problem here is that we might need witgen for
x_inv.