Fix typo in definition of k for subtree proofs - #120
Conversation
|
|
||
| * `0 <= start < end <= n` | ||
| * If `k` is the largest power of 2 that is greater than or equal to `end - start`, `start` must be a multiple of `k` | ||
| * If `k` is the largest power of 2 that is less than or equal to `end - start`, `start` must be a multiple of `k` |
There was a problem hiding this comment.
Hmm. I think greater is correct, unless I'm confused? [2, 5) is not a valid subtree because it makes this tree:
/\
/\ |
2 3 4
But then [0, 5) looks like this, which doesn't contain that tree:
/\
/ \
/\ |
/ \ |
/\ /\ |
0 1 2 3 4
So if the subtree has size 3, we need start to be 4-aligned, not just 2-aligned.
But in that case "largest power of 2" should be "smallest power of 2".
There was a problem hiding this comment.
Ah yes, you're right--thanks for the catch and the counterexample! I agree the correct version is "If k is the smallest power of 2 that is greater than or equal to end - start, start must be a multiple of k", since for any size subtree we want the start index to be aligned with the next-greatest power of two.
I got confused since RFC9162 and the subtree consistency proof section say "let k be the largest power of two smaller than n", but we're dealing with a different k here--that k is for a split index, but the k here is a restriction on the subtree start index. Maybe we pick a new letter like s for "start"?
Fix restriction on subtree `start` index. Other changes: - Rename `k` to `s` to avoid confusing with `k` uses in other sections of the doc. - Use "power of two" instead of "power of 2" for consistency with other usage in the doc and with RFC9162.
No description provided.