@@ -13,7 +13,7 @@ methods {
1313 function get (bytes32 ) external returns (bytes32 ) envfree ;
1414
1515 // FV
16- function _indexOf (bytes32 ) external returns (uint256 ) envfree ;
16+ function _positionOf (bytes32 ) external returns (uint256 ) envfree ;
1717}
1818
1919/ *
@@ -69,13 +69,13 @@ invariant atUniqueness(uint256 index1, uint256 index2)
6969┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
7070│ Invariant : index <> value relationship is consistent │
7171│ │
72- │ Note that the two consistencyXxx invariants , put together , prove that at_ and _indexOf are inverse of one another . │
73- │ This proves that we have a bijection between indices (the enumerability part ) and keys (the entries that are set │
74- │ and removed from the EnumerableMap ). │
72+ │ Note that the two consistencyXxx invariants , put together , prove that at_ and _positionOf are inverse of one │
73+ │ another . This proves that we have a bijection between indices (the enumerability part ) and keys (the entries that │
74+ │ are set and removed from the EnumerableMap ). │
7575└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
7676* /
7777invariant consistencyIndex (uint256 index )
78- index < length () = > to_mathint (_indexOf (key_at (index ))) == index + 1
78+ index < length () = > to_mathint (_positionOf (key_at (index ))) == index + 1
7979 {
8080 preserved remove (bytes32 key ) {
8181 requireInvariant consistencyIndex (require_uint256 (length () - 1 ));
@@ -84,16 +84,16 @@ invariant consistencyIndex(uint256 index)
8484
8585invariant consistencyKey (bytes32 key )
8686 contains (key ) = > (
87- _indexOf (key ) > 0 & &
88- _indexOf (key ) <= length () & &
89- key_at (require_uint256 (_indexOf (key ) - 1 )) == key
87+ _positionOf (key ) > 0 & &
88+ _positionOf (key ) <= length () & &
89+ key_at (require_uint256 (_positionOf (key ) - 1 )) == key
9090 )
9191 {
9292 preserved remove (bytes32 otherKey ) {
9393 requireInvariant consistencyKey (otherKey );
9494 requireInvariant atUniqueness (
95- require_uint256 (_indexOf (key ) - 1 ),
96- require_uint256 (_indexOf (otherKey ) - 1 )
95+ require_uint256 (_positionOf (key ) - 1 ),
96+ require_uint256 (_positionOf (otherKey ) - 1 )
9797 );
9898 }
9999 }
0 commit comments