Fix leq for PatriciaTreeMap when branches have uneven depths - #31
Closed
rootkiller6788 wants to merge 1 commit into
Closed
Fix leq for PatriciaTreeMap when branches have uneven depths#31rootkiller6788 wants to merge 1 commit into
rootkiller6788 wants to merge 1 commit into
Conversation
The branch-vs-branch case of `Node::is_tree_leq_impl` had its two arms
swapped: when the compared trees have prefixes of different lengths (one
prefix is a proper prefix of the other), the implicit-value condition and
the recursion direction were both mirrored relative to the C++ reference
implementation in `PatriciaTreeCore.h`.
This produced wrong `leq` results for `PatriciaTreeMapAbstractPartition`
(implicit Bottom) and `PatriciaTreeMapAbstractEnvironment` (implicit Top)
whenever one map's key set is a strict subset/superset of the other's. For
example, with Bottom implicit values, `{0, 2} <= {0, 1, 2, 3}` incorrectly
returned false.
Align the two arms with the C++ semantics and add regression tests for
both the partition and environment flavors.
meta-cla
Bot
added
the
CLA Signed
arthaud
approved these changes
Aug 20, 2026
|
@arthaud has imported this pull request. If you are a Meta employee, you can view this in D116755789. |
Contributor
|
LGTM, thanks for the fix |
meta-codesync Bot
pushed a commit
to facebook/redex
that referenced
this pull request
Aug 20, 2026
Summary:
## Problem
The branch-vs-branch case of `Node::is_tree_leq_impl` in `rust/src/datatype/patricia_tree_impl.rs` had its two arms swapped. When the two compared Patricia trees have branch prefixes of different lengths (one prefix is a proper prefix of the other), both the implicit-value condition (`is_top()` vs `is_bottom()`) and the recursion direction were mirrored relative to the reference implementation in `include/sparta/PatriciaTreeCore.h`.
This produces incorrect `leq` results for both map flavors:
- `PatriciaTreeMapAbstractPartition::leq` (implicit value = Bottom)
- `PatriciaTreeMapAbstractEnvironment::leq` (implicit value = Top)
## Concrete counterexample
With Bottom implicit values, `{0, 2}.leq({0, 1, 2, 3})` should be `true` (the missing bindings in the smaller map are Bottom, which is `<=` any value), but the swapped arm short-circuited on `implicit_value.is_top()` and returned `false`.
Symmetrically, with Top implicit values, `{0, 1, 2, 3}.leq({0, 2})` should be `true` (the larger map's extra bindings are `<=` Top), but it returned `false`.
## Fix
Align the two arms with the C++ `is_tree_leq` semantics:
- `s_prefix.begins_with(t_prefix)` (s is deeper, s's keys are a subset of t's): require `implicit_value.is_bottom()` and recurse into the matching child of `t`.
- `t_prefix.begins_with(s_prefix)` (t is deeper, t's keys are a subset of s's): require `implicit_value.is_top()` and recurse into the matching child of `s`.
## Tests
Added `test_ptmap_leq_uneven_branch_depths` to `rust/tests/abstract_partition_test.rs` and `test_ptmae_leq_uneven_branch_depths` to `rust/tests/abstract_environment_test.rs`. Both fail before the fix and pass after it, and cover the `leq` direction in both directions.
X-link: facebook/SPARTA#31
Reviewed By: arnaudvenet
Differential Revision: D116755789
Pulled By: arthaud
fbshipit-source-id: 7a1e7fe82827f5fab4bd3c03893152e50c284f6b
meta-codesync Bot
pushed a commit
to facebook/redex
that referenced
this pull request
Aug 20, 2026
Summary:
## Problem
The branch-vs-branch case of `Node::is_tree_leq_impl` in `rust/src/datatype/patricia_tree_impl.rs` had its two arms swapped. When the two compared Patricia trees have branch prefixes of different lengths (one prefix is a proper prefix of the other), both the implicit-value condition (`is_top()` vs `is_bottom()`) and the recursion direction were mirrored relative to the reference implementation in `include/sparta/PatriciaTreeCore.h`.
This produces incorrect `leq` results for both map flavors:
- `PatriciaTreeMapAbstractPartition::leq` (implicit value = Bottom)
- `PatriciaTreeMapAbstractEnvironment::leq` (implicit value = Top)
## Concrete counterexample
With Bottom implicit values, `{0, 2}.leq({0, 1, 2, 3})` should be `true` (the missing bindings in the smaller map are Bottom, which is `<=` any value), but the swapped arm short-circuited on `implicit_value.is_top()` and returned `false`.
Symmetrically, with Top implicit values, `{0, 1, 2, 3}.leq({0, 2})` should be `true` (the larger map's extra bindings are `<=` Top), but it returned `false`.
## Fix
Align the two arms with the C++ `is_tree_leq` semantics:
- `s_prefix.begins_with(t_prefix)` (s is deeper, s's keys are a subset of t's): require `implicit_value.is_bottom()` and recurse into the matching child of `t`.
- `t_prefix.begins_with(s_prefix)` (t is deeper, t's keys are a subset of s's): require `implicit_value.is_top()` and recurse into the matching child of `s`.
## Tests
Added `test_ptmap_leq_uneven_branch_depths` to `rust/tests/abstract_partition_test.rs` and `test_ptmae_leq_uneven_branch_depths` to `rust/tests/abstract_environment_test.rs`. Both fail before the fix and pass after it, and cover the `leq` direction in both directions.
X-link: facebook/SPARTA#31
Reviewed By: arnaudvenet
Differential Revision: D116755789
Pulled By: arthaud
fbshipit-source-id: 7a1e7fe82827f5fab4bd3c03893152e50c284f6b
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Problem
The branch-vs-branch case of
Node::is_tree_leq_implinrust/src/datatype/patricia_tree_impl.rshad its two arms swapped. When the two compared Patricia trees have branch prefixes of different lengths (one prefix is a proper prefix of the other), both the implicit-value condition (is_top()vsis_bottom()) and the recursion direction were mirrored relative to the reference implementation ininclude/sparta/PatriciaTreeCore.h.This produces incorrect
leqresults for both map flavors:PatriciaTreeMapAbstractPartition::leq(implicit value = Bottom)PatriciaTreeMapAbstractEnvironment::leq(implicit value = Top)Concrete counterexample
With Bottom implicit values,
{0, 2}.leq({0, 1, 2, 3})should betrue(the missing bindings in the smaller map are Bottom, which is<=any value), but the swapped arm short-circuited onimplicit_value.is_top()and returnedfalse.Symmetrically, with Top implicit values,
{0, 1, 2, 3}.leq({0, 2})should betrue(the larger map's extra bindings are<=Top), but it returnedfalse.Fix
Align the two arms with the C++
is_tree_leqsemantics:s_prefix.begins_with(t_prefix)(s is deeper, s's keys are a subset of t's): requireimplicit_value.is_bottom()and recurse into the matching child oft.t_prefix.begins_with(s_prefix)(t is deeper, t's keys are a subset of s's): requireimplicit_value.is_top()and recurse into the matching child ofs.Tests
Added
test_ptmap_leq_uneven_branch_depthstorust/tests/abstract_partition_test.rsandtest_ptmae_leq_uneven_branch_depthstorust/tests/abstract_environment_test.rs. Both fail before the fix and pass after it, and cover theleqdirection in both directions.