Skip to content

Commit 385e06f

Browse files
committed
combine INV-023 and INV-024 into a single threshold bounds invariant
1 parent 99cb879 commit 385e06f

File tree

1 file changed

+10
-18
lines changed

1 file changed

+10
-18
lines changed

docs/INVARIANTS.md

Lines changed: 10 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -208,52 +208,44 @@
208208
- **Enforcement**: Assertions on transceiver management code paths
209209
- **Code Reference**: `TransceiverRegistry.sol` (EVM)
210210

211-
### INV-023: Attestation Threshold Bounds
211+
### INV-023: Minimum and Maximum Threshold Bounds
212212

213-
- **Invariant**: `threshold <= number_of_enabled_transceivers && threshold > 0`
213+
- **Invariant**: Threshold must be 1) greater than zero and 2) less than or equal to the number of enabled transceivers
214214
- **Description**: Attestation threshold must not exceed available transceivers and must be positive
215215
- **Enforcement**: Explicit bounds checking in threshold setting functions
216-
- **Error Codes**: `ThresholdTooHigh`, `ZeroThreshold` (EVM/Solana), **MISSING VALIDATION** (Sui)
216+
- **Error Codes**: `ThresholdTooHigh`, `ZeroThreshold` (EVM/Solana)
217217
- **Code Reference**: `_checkThresholdInvariants()` (EVM), error enforcement (Solana), `EThresholdTooHigh` (Sui)
218218

219-
### INV-024: Non-Zero Threshold Requirement
220-
221-
- **Invariant**: Threshold must be greater than zero (after initial deployment)
222-
- **Description**: Prevents configuration where messages cannot be approved due to zero threshold
223-
- **Enforcement**: Zero threshold validation when transceivers exist
224-
- **Error Codes**: `ZeroThreshold` (EVM/Solana), `EZeroThreshold` (Sui)
225-
- **Code Reference**: `if (numTransceivers.registered > 0 && threshold == 0) revert ZeroThreshold();`
226-
227-
### INV-025: Minimum Transceiver Requirement
219+
### INV-024: Minimum Transceiver Requirement
228220

229221
- **Invariant**: At least one transceiver must be enabled for operations (after initial deployment)
230222
- **Description**: Prevents operations when no transceivers are available to process messages
231223
- **Enforcement**: Enabled transceiver count validation before operations
232224
- **Error Codes**: `NoEnabledTransceivers` (EVM), `NoRegisteredTransceivers` (Solana)
233225

234-
### INV-026: Transceiver Registration Requirement
226+
### INV-025: Transceiver Registration Requirement
235227

236228
- **Invariant**: A transceiver cannot be unregistered and its index must not change
237229
- **Description**: Transceivers should never be truly deleted, only disabled. This preserves their index into the bitmap which is crucial for attestation.
238230
- **Enforcement**: Assertions on transceiver management code paths
239231

240-
### INV-027: Transceiver Registration Requirement
232+
### INV-026: Transceiver index should always increase
241233

242234
- **Invariant**: The next transceiver index must always increase monotically
243235
- **Description**: The next transceiver index should always go up by one. This guarantees uniqueness of indices into the bitmap which is crucial for attestation.
244236
- **Enforcement**: Assertions on transceiver management code paths
245237

246238
## Timing and Release Controls
247239

248-
### INV-028: Release Timing Validation
240+
### INV-027: Release Timing Validation
249241

250242
- **Invariant**: Transfers can only be released after rate limit delay expires
251243
- **Description**: Enforces time-based delays for rate-limited transfers
252244
- **Enforcement**: Timestamp validation before transfer release
253245
- **Error Codes**: `CantReleaseYet` (Solana), `ECantReleaseYet` (Sui)
254246
- **Code Reference**: Rate limiter queue system with timestamp checks, `try_release()` functions
255247

256-
### INV-029: Transfer Redemption Controls
248+
### INV-028: Transfer Redemption Controls
257249

258250
- **Invariant**: Transfers must be properly approved and not already redeemed before processing
259251
- **Description**: Prevents unauthorized or duplicate transfer redemptions
@@ -263,15 +255,15 @@
263255

264256
## Message Size Constraints
265257

266-
### INV-030: Payload Length Limitation
258+
### INV-029: Payload Length Limitation
267259

268260
- **Invariant**: NttManagerMessages and AdditionalPayloads must not exceed uint16 in size
269261
- **Description**: Prevents unbounded message sizes that could cause processing issues
270262
- **Enforcement**: Assertions in encoding logic
271263
- **Error Codes**: `PayloadTooLong` (EVM)
272264
- **Code Reference**: `TransceiverStructs.sol` (EVM), implementation of `Writable` trait for `NativeTokenTransfer` (Solana)
273265

274-
### INV-031: Transceiver Instruction Length Limitation
266+
### INV-030: Transceiver Instruction Length Limitation
275267

276268
- **Invariant**: Individual transceiver instruction payloads must not exceed uint8 in size
277269
- **Description**: Prevents unbounded message sizes that could cause processing issues

0 commit comments

Comments
 (0)