Skip to content

feat: Dadda tree implementation#20

Merged
osmanyasar05 merged 5 commits into
mainfrom
dadda
Jun 5, 2026
Merged

feat: Dadda tree implementation#20
osmanyasar05 merged 5 commits into
mainfrom
dadda

Conversation

@osmanyasar05

Copy link
Copy Markdown
Collaborator

This PR introduces the Dadda tree algorithm implementation.

@cowardsa cowardsa left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks really neat - very nice work - I've left a couple of suggestions about lifting repeatedly used code into a utility function - but otherwise nice!

If you can get BitVector to BitHeap working, then it should be trivial to start generating MLIR code

Output: A two-row bit heap.

(1) Compute the smallest 𝐿 such that 𝑚𝐿 ≥ ℎ, where the Dadda sequence is
given by 𝑚0 = 2 and 𝑚𝑙 = ⌊3/2 mₗ₋₁⌋.

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Super Nit: you switch into m_{l-1} from ml?

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

you mean it should have been m_l, right? good catch thanks!

Comment thread DatapathVerification/BitHeap/DaddaTree.lean
Comment thread DatapathVerification/BitHeap/DaddaTree.lean
Comment thread DatapathVerification/BitHeap/DaddaTree.lean Outdated
Comment on lines +76 to +77
match (h.get col).toList with
| x :: y :: _ =>

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This gets repeated a lot - anything we can do to wrap HAs and FAs?

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

hmm I am not sure what we can do here, since we do not match the same way exactly

Comment thread DatapathVerification/BitHeap/DaddaTree.lean Outdated
@osmanyasar05 osmanyasar05 merged commit 8f7142c into main Jun 5, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants