fix: align EnumerableMap FV comments with invariants

[SashaMalysehko]

Update the FV comments for EnumerableMap to describe the actual invariants over keys instead of values. The atUniqueness invariant now explicitly states that a key can only be stored at a single location, and the index–key consistency block is documented as an index–key relationship.

The note explaining the bijection between indices and keys now refers to key_at and positionOf as inverses, matching the methods used in the spec. These changes make the comments consistent with the formal invariants and the underlying EnumerableMap/EnumerableSet implementation, avoiding confusion for readers of the proofs.

[changeset-bot]

⚠️ No Changeset found

Latest commit: 72ee45d

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

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

[coderabbitai]

Walkthrough

This pull request updates documentation and terminology in the EnumerableMap specification file. The changes include revisions to invariant headers and descriptive notes to align terminology around keys rather than values. Specifically, the atUniqueness invariant header was modified, the consistency invariant header was updated to reference key-index relationships, and a note describing function relationships was adjusted to identify "key_at" and "_positionOf" as inverse operations. No modifications were made to functional logic, control flow, or error handling, and no public entity signatures were altered.

Pre-merge checks and finishing touches

✅ Passed checks (3 passed)

Check name	Status	Explanation
Title check	✅ Passed	The title 'fix: align EnumerableMap FV comments with invariants' accurately describes the main change - updating formal verification documentation to align with the actual invariants.
Description check	✅ Passed	The description is directly related to the changeset, explaining the specific updates to FV comments for EnumerableMap regarding key-based invariants and terminology corrections.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.

✨ Finishing touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Post copyable unit tests in a comment

---

📜 Recent review details

Configuration used: CodeRabbit UI

Review profile: CHILL

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between 77bc564 and 72ee45d.

📒 Files selected for processing (1)

• fv/specs/EnumerableMap.spec (2 hunks)

⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (4)

• GitHub Check: Redirect rules - solidity-contracts
• GitHub Check: Header rules - solidity-contracts
• GitHub Check: Pages changed - solidity-contracts
• GitHub Check: halmos

🔇 Additional comments (1)

fv/specs/EnumerableMap.spec (1)

54-72: Improve clarity of invariant description.

The updated header for atUniqueness now correctly refers to keys rather than values, which aligns with the invariant's logic that checks uniqueness of keys across indices. This clarifies the invariant's purpose for readers of the formal specification.

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands and usage tips.}