Skip to content

use BTreeSet and BTreeMap for containers#474

Open
ed255 wants to merge 5 commits intomainfrom
feat/btree
Open

use BTreeSet and BTreeMap for containers#474
ed255 wants to merge 5 commits intomainfrom
feat/btree

Conversation

@ed255
Copy link
Collaborator

@ed255 ed255 commented Feb 4, 2026

Previously we were using HashMap and HashSet for the Dictionary and Set containers. This was very efficient but it was slightly inconvenient because sometimes we iterate over the entries of those collections to generate statements for recursive predicates, leading to non-deterministic order of statements which makes debugging issues harder.

By using BTreeMap and BTreeSet we always get deterministic iteration over the container entries, at a small cost of performance (which should be negligible because we target consumer devices and the bottleneck is in the proving process).

As an added bonus, now when we iterate over the Dictionary and Set we visit the entries in the same order as they are laid out in the Merkle Tree.

I've also done a small change in MultiPodBuilder to make an internal structure deterministic.

I've requested review of 2 people to get critical feedback on this change.

@ed255 ed255 requested review from arnaucube and robknight February 4, 2026 16:37
// Group statement indices by their content.
let mut content_to_indices: HashMap<&Statement, Vec<usize>> = HashMap::new();
let mut statement_dedup_index: HashMap<&Statement, usize> = HashMap::new();
let mut statement_content_groups = Vec::new();
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

This change is to generate a deterministic statement_content_groups.

Copy link
Collaborator

@robknight robknight left a comment

Choose a reason for hiding this comment

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

I think this is a good idea in principle but we ought to consider the issue pointed out in #393 before merging.


impl Eq for Value {}

impl Ord for Value {
Copy link
Collaborator

Choose a reason for hiding this comment

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

This used to exist and was intentionally removed: #393

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Thanks for pointing that out!
So one issue is that given x and y Values, if they are i64 the result of x < y and x <= y doesn't match the predicate Lt and LtEq because the encoding of i64 into RawValue uses two's complement which means negative numbers have the most significant bit set and would be treated as big non-negative numbers by Ord.

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