Refactor DoubleEndedQueue

[Amxx]

The use of signed integer is confusing, the cast decrease readability, and that is not actually needed.
Using uint128 is cleaner IMO.

We can discuss narrowing down the scope of the unchecked block. Also, we could remove possibly the Full() check.

This not upgrade-compatible, so I'm targeting 5.0. Otherwise, the interface is backward compatible.

Note that there is currently an comment saying
// We also assume there are at most int256.max items in the queue.
But since the queue is stored in a mapping(int128 → uint256) the size limit is 2**128, which is WAY smaller than int256.max

Fixes LIB-953

PR Checklist

• Tests
• Documentation
• Changeset entry (run npx changeset add)

[changeset-bot]

🦋 Changeset detected

Latest commit: 3a2ec00

The changes in this PR will be included in the next version bump.

This PR includes changesets to release 1 package

Name	Type
openzeppelin-solidity	Major

Not sure what this means? Click here to learn what changesets are.

Click here if you're a maintainer who wants to add another changeset to this PR

[frangio]

I don't really see a clear benefit in this. We can equally say that the use of unsinged integer wraparound is confusing.

[Amxx]

The points was that it would avoid some (problematic?) casting in length() while also reducing the cost of empty().

The wraparound would not only be verified by FV, but the FV would also become cleaner because the "full" case is clearer. We would need to make fewer "value does not overflow" assumptions in the specs.

[frangio]

The points was that it would avoid some (problematic?) casting in length() while also reducing the cost of empty().

These are very marginal benefits IMO.

That said, if this makes FV cleaner I would support it, but that also shows that we would need to update the spec, which may nonetheless be a can of worms. Overall I don't think this is worth prioritizing at this moment.

I analyzed whether this could be a backwards compatible change, but it turns out that when computing the hash to locate a value in a mapping with integer keys, the key is sign-extended rathert than zero-padded, so the upgrade from mapping(int128 => bytes32 to mapping(uint128 => bytes32) would be breaking.

[Amxx]

I analyzed whether this could be a backwards compatible change, but it turns out that when computing the hash to locate a value in a mapping with integer keys, the key is sign-extended rathert than zero-padded, so the upgrade from mapping(int128 => bytes32 to mapping(uint128 => bytes32) would be breaking.

Yes, that is why I wanted to do it in 5.0

[Amxx]

Note: this change overall reduces the gas cost

[ernestognw]

I can confirm this would make FV simpler and shouldn't be a big change there because the contract behaves the same. Also, with the overall gas reduction I think we have good reasons (still marginally good) to include this change in 5.0 with no caveat as far as I know.

[frangio]

Let's move ahead with this then.

[Amxx]

This is an internal change that doesn't affect the library interface, does it need a changelog?

---

I also updated the Certora specs. I bumped it to Certora 4 (CVL2). Please note that we no longer need any boundedQueue or boundariesConsistency assumptions!

[frangio]

This is an internal change that doesn't affect the library interface, does it need a changelog?

Yes, according to the guidelines:

All changes to the core codebase (excluding tests, auxiliary scripts, etc.) must be documented in a changelog, except for purely cosmetic or documentation changes.

The reasoning is that users may see that a contract was updated in X.Y.Z and may want to see exactly what changed.

[frangio]

If we merge this will all the existing specs stop working?

[Amxx]

They already don't work ... because 3.6.4 is no longer supported

[Amxx]

We'll have to do a "bump FV to new format" task during the quality control sprint. I can take care of it.

[frangio]

This looks good to me. Sorry, minor comment though. I am ready to merge basically, beyond that comment.

Can this be moved out of draft?