Skip to content

Commit 566c314

Browse files
fix: align EnumerableMap FV comments with invariants (#6190)
1 parent b1df0c2 commit 566c314

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

fv/specs/EnumerableMap.spec

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ invariant indexedContained(uint256 index)
5353

5454
/*
5555
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
56-
Invariant: A value can only be stored at a single location
56+
Invariant: A key can only be stored at a single location
5757
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
5858
*/
5959
invariant atUniqueness(uint256 index1, uint256 index2)
@@ -72,9 +72,9 @@ invariant atUniqueness(uint256 index1, uint256 index2)
7272

7373
/*
7474
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
75-
Invariant: index <> value relationship is consistent
75+
Invariant: index <> key relationship is consistent
7676
│ │
77-
Note that the two consistencyXxx invariants, put together, prove that at_ and _positionOf are inverse of one
77+
Note that the two consistencyXxx invariants, put together, prove that key_at and _positionOf are inverse of one
7878
another. This proves that we have a bijection between indices (the enumerability part) and keys (the entries that
7979
are set and removed from the EnumerableMap). │
8080
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

0 commit comments

Comments
 (0)