From e745df50fcfbec609314e144e5ca8923d7daaff4 Mon Sep 17 00:00:00 2001 From: Stefano Angieri Date: Fri, 11 Oct 2024 16:14:33 +0200 Subject: [PATCH] self review --- .../v2/ics-004-packet-semantics/README.md | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/spec/core/v2/ics-004-packet-semantics/README.md b/spec/core/v2/ics-004-packet-semantics/README.md index 0c7af4014..921c85cee 100644 --- a/spec/core/v2/ics-004-packet-semantics/README.md +++ b/spec/core/v2/ics-004-packet-semantics/README.md @@ -291,8 +291,8 @@ Pre-conditions: | **Condition Type** | **Description** | **Code Checks** | |-------------------------------|------------------| ----------------| | **error-conditions** | 1. Invalid `clientId`
2. `Invalid channelId`
3. Unexpected keyPrefix format | 1. `client==null`
2.1 `validateId(channelId)==False`
2.2 `getChannel(channelId)!=null`
3. `isFormatOk(KeyPrefix)==False`
| -| **post-conditions (success)** | 1. A channel is set in store
2. The creator is set in store
3. `nextSequenceSend` is initialized
4. Event with relevant fields is emitted | 1. `storedChannel[channelId]!=null`
2. `channelCreator[channelId]!=null`
3. `nextSequenceSend[channelId]==1`
4. checkEventEmission | -| **post-conditions (error)** | - None of the post-conditions (success) is true
| 1. `storedChannel[channelId]==null`
2. `channelCreator[channelId]==null`
3. `nextSequenceSend[channelId]!=1`
| +| **post-conditions (success)** | 1. A channel is set in store
2. The creator is set in store
3. `nextSequenceSend` is initialized
4. Event with relevant fields is emitted | 1. `storedChannel[channelId]!=null`
2. `channelCreator[channelId]!=null`
3. `nextSequenceSend[channelId]==1`
4. Check Event Emission | +| **post-conditions (error)** | None of the post-conditions (success) is true
| 1. `storedChannel[channelId]==null`
2. `channelCreator[channelId]==null`
3. `nextSequenceSend[channelId]!=1`
4. No Event is Emitted
| ###### Pseudo-Code @@ -353,8 +353,8 @@ Pre-conditions: | **Condition Type** | **Description** | **Code Checks** | |-------------------------------|-----------------------------------|----------------------------| | **error-conditions** | 1. Invalid `channelId`
2. Creator authentication failed | 1.1 `validateId(channelId)==False`
1.2 `getChannel(channelId)==null`
2. `channelCreator[channelId]!=msg.signer()`
| -| **post-conditions (success)** | 1. The channel in store contains the `counterpartyChannelId` information
2. An event with relevant information has been emitted | 1. `storedChannel[channelId].counterpartyChannelId!=null`
| -| **post-conditions (error)** | 1. On the first call, the channel in store contains the `counterpartyChannelId` as an empty field
| 1. `storedChannel[channelId].counterpartyChannelId==null` | +| **post-conditions (success)** | 1. The channel in store contains the `counterpartyChannelId` information
2. An event with relevant information has been emitted | 1. `storedChannel[channelId].counterpartyChannelId!=null`
2. Check Event Emission | +| **post-conditions (error)** | 1. On the first call, the channel in store contains the `counterpartyChannelId` as an empty field
| 1. `storedChannel[channelId].counterpartyChannelId==null`
2. No Event is Emitted
| ###### Pseudo-Code @@ -542,8 +542,8 @@ Pre-conditions: | **Condition Type** |**Description** | **Code Checks**| |-------------------------------|--------------------------------------------------------|------------------------| | **Error-Conditions** | 1. Invalid `clientId`
2. Invalid `channelId`
3. Invalid `timeoutTimestamp`
4. Unsuccessful payload execution. | 1. `router.clients[channel.clientId]==null`
2. `getChannel(sourceChannelId)==null`
3.1 `timeoutTimestamp==0`
3.2 `timeoutTimestamp < currentTimestamp()`
3.3 `timeoutTimestamp > currentTimestamp() + MAX_TIMEOUT_DELTA`
4. `onSendPacket(..)==False`
| -| **Post-Conditions (Success)** | 1. `onSendPacket` is executed and the application state is modified
2. The `packetCommitment` is generated and stored under the expected `packetCommitmentPath`
3. The sequence number bound to `sourceId` is incremented by 1
4. Event with relevant information is emitted | 1. `onSendPacket(..)==True; app.State(beforeSendPacket)!=app.State(afterSendPacket)`
2. `commitment=commitV2Packet(packet), provableStore.get(packetCommitmentPath(sourceChannelId, sequence))==commitment`
3. `nextSequenceSend(beforeSendPacket[sourecChannelId])+1==SendPacket(..)`
4. CheckEventEmission | -| **Post-Conditions (Error)** | 1. if `onSendPacket` fails the application state is unchanged
2. No `packetCommitment` has been generated
3. The sequence number bound to `sourceId` is unchanged. | 1. `app.State(beforeSendPacket)==app.State(afterSendPacket)`
2. `commitment=commitV2Packet(packet), provableStore.get(packetCommitmentPath(sourceChannelId, sequence))==commitment`
3. `nextSequenceSend[sourecChannelId]==nextSequenceSend(beforeSendPacket)` | +| **Post-Conditions (Success)** | 1. `onSendPacket` is executed and the application state is modified
2. The `packetCommitment` is generated and stored under the expected `packetCommitmentPath`
3. The sequence number bound to `sourceId` is incremented by 1
4. Event with relevant information is emitted | 1. `onSendPacket(..)==True; app.State(beforeSendPacket)!=app.State(afterSendPacket)`
2. `commitment=commitV2Packet(packet), provableStore.get(packetCommitmentPath(sourceChannelId, sequence))==commitment`
3. `nextSequenceSend(beforeSendPacket[sourecChannelId])+1==SendPacket(..)`
4. Check Event Emission | +| **Post-Conditions (Error)** | 1. if `onSendPacket` fails the application state is unchanged
2. No `packetCommitment` has been generated
3. The sequence number bound to `sourceId` is unchanged
4. No Event Emission | 1. `app.State(beforeSendPacket)==app.State(afterSendPacket)`
2. `commitment=commitV2Packet(packet), provableStore.get(packetCommitmentPath(sourceChannelId, sequence))==commitment`
3. `nextSequenceSend[sourecChannelId]==nextSequenceSend(beforeSendPacket)`
4. Check No Event is Emitted
| ###### Pseudo-Code @@ -641,8 +641,8 @@ Pre-conditions: | **Condition Type** | **Description** | **Code Checks** | |-------------------------------|-----------------------------------------------|-----------------------------------------------| | **Error-Conditions** | 1. invalid `packetCommitment`, 2.`packetReceipt` already exists
3. Invalid timeoutTimestamp
4. Unsuccessful payload execution. | 1.1 `verifyMembership(packetCommitment)==false`
1.2 `provableStore.get(packetReceiptPath(packet.channelDestId, packet.sequence))!=null`
3. `timeoutTimestamp === 0`
3.1 `currentTimestamp() < packet.timeoutTimestamp)`
4. `onReceivePacket(..)==False` | -| **Post-Conditions (Success)** | 1. `onReceivePacket` is executed and the application state is modified
2. The `packetReceipt` is written
| 1. `onReceivePacket(..)==True; app.State(beforeReceivePacket)!=app.State(afterReceivePacket)`
2. `provableStore.get(packetReceiptPath(packet.channelDestId, packet.sequence))!=null`
| -| **Post-Conditions (Error)** | 1. if `onReceivePacket` fails the application state is unchanged
2. `packetReceipt is not written`
| 1. `app.State(beforeReceivePacket)==app.State(afterReceivePacket)`
2. `provableStore.get(packetReceiptPath(packet.channelDestId, packet.sequence))==null` | +| **Post-Conditions (Success)** | 1. `onReceivePacket` is executed and the application state is modified
2. The `packetReceipt` is written
3. Event is Emitted
| 1. `onReceivePacket(..)==True; app.State(beforeReceivePacket)!=app.State(afterReceivePacket)`
2. `provableStore.get(packetReceiptPath(packet.channelDestId, packet.sequence))!=null`
3. Check Event Emission
| +| **Post-Conditions (Error)** | 1. if `onReceivePacket` fails the application state is unchanged
2. `packetReceipt is not written`

3. No Event Emission
| 1. `app.State(beforeReceivePacket)==app.State(afterReceivePacket)`
2. `provableStore.get(packetReceiptPath(packet.channelDestId, packet.sequence))==null`
3. Check No Event is Emitted
| ###### Pseudo-Code @@ -748,8 +748,8 @@ Pre-conditions: | **Condition Type** | **Description** | **Code Checks** | |-------------------------------|------------|------------| | **Error-Conditions** | 1. acknowledgement is empty
2. The `packetAcknowledgementPath` stores already a value. | 1. `len(acknowledgement) === 0`
2. `provableStore.get(packetAcknowledgementPath(packet.channelDestId, packet.sequence) !== null` | -| **Post-Conditions (Success)** | 1. opaque acknowledgement has been written at `packetAcknowledgementPath` | 1. `provableStore.get(packetAcknowledgementPath(packet.channelDestId, packet.sequence) !== null` | -| **Post-Conditions (Error)** | 1. No value is stored at the `packetAcknowledgementPath`. | 1. `provableStore.get(packetAcknowledgementPath(packet.channelDestId, packet.sequence) === null` | +| **Post-Conditions (Success)** | 1. opaque acknowledgement has been written at `packetAcknowledgementPath`
2. Event is Emitted
| 1. `provableStore.get(packetAcknowledgementPath(packet.channelDestId, packet.sequence) !== null`
2. Check Event Emission
| +| **Post-Conditions (Error)** | 1. No value is stored at the `packetAcknowledgementPath`.
2. No Event is Emitted
| 1. `provableStore.get(packetAcknowledgementPath(packet.channelDestId, packet.sequence) === null`
2. Check No Event is Emitted
| ###### Pseudo-Code @@ -801,8 +801,8 @@ Pre-conditions: | **Condition Type** | **Description** | **Code Checks** | |-------------------------------|---------------------------------|---------------------------------| | **Error-Conditions** | 1. `packetCommitment` already cleared out
2. Unset Acknowledgment
3. Unsuccessful payload execution. | 1. `provableStore.get(packetCommitmentPath(packet.channelSourceId, packet.sequence)) === null`
2. `verifyMembership(packetacknowledgementPath,...,) == False`
3. `onAcknowledgePacket(packet.channelSourceId,payload, acknowledgement) == False` | -| **Post-Conditions (Success)** | 1. `onAcknowledgePacket` is executed and the application state is modified
2. `packetCommitment` has been cleared out. | 1. `onAcknowledgePacket(..)==True; app.State(beforeAcknowledgePacket)!=app.State(afterAcknowledgePacket)`
2. `provableStore.get(packetCommitmentPath(packet.channelSourceId, packet.sequence)) === null` | -| **Post-Conditions (Error)** | 1. If `onAcknowledgePacket` fails the application state is unchanged
2. `packetCommitment` has not been cleared out
3. acknowledgement is stil in store | 1. `onAcknowledgePacket(..)==False; app.State(beforeAcknowledgePacket)==app.State(afterAcknowledgePacket)`
2. `provableStore.get(packetCommitmentPath(packet.channelSourceId, packet.sequence)) === commitV2Packet(packet)` 3. `verifyMembership(packetAcknowledgementPath,...,) == True`| +| **Post-Conditions (Success)** | 1. `onAcknowledgePacket` is executed and the application state is modified
2. `packetCommitment` has been cleared out
4. Event is Emission
| 1. `onAcknowledgePacket(..)==True; app.State(beforeAcknowledgePacket)!=app.State(afterAcknowledgePacket)`
2. `provableStore.get(packetCommitmentPath(packet.channelSourceId, packet.sequence)) === null`,
4. Check Event is Emitted
| +| **Post-Conditions (Error)** | 1. If `onAcknowledgePacket` fails the application state is unchanged
2. `packetCommitment` has not been cleared out
3. acknowledgement is stil in store
4. No Event Emission
| 1. `onAcknowledgePacket(..)==False; app.State(beforeAcknowledgePacket)==app.State(afterAcknowledgePacket)`
2. `provableStore.get(packetCommitmentPath(packet.channelSourceId, packet.sequence)) === commitV2Packet(packet)` 3. `verifyMembership(packetAcknowledgementPath,...,) == True`
4. Check No Event is Emitted
| ###### Pseudo-Code @@ -913,8 +913,8 @@ Pre-conditions: | **Condition Type** | **Description**| **Code Checks**| |-------------------------------|--------------------|--------------------| | **Error-Conditions** | 1. `packetCommitment` already cleared out
2. `packetReceipt` is not empty
3. Unsuccessful payload execution
4. `timeoutTimestamp` not elapsed on the receiving chain| 1. `provableStore.get(packetCommitmentPath(packet.channelSourceId, packet.sequence)) === null`
2. `provableStore.get(packetReceiptPath(packet.channelDestId, packet.sequence))!=null`
3. `onTimeoutPacket(packet.channelSourceId,payload) == False`
4.1 `packet.timeoutTimestamp > 0`
4.2 `proofTimestamp = client.getTimestampAtHeight(proofHeight); proofTimestamp >= packet.timeoutTimestamp` | -| **Post-Conditions (Success)** | 1. `onTimeoutPacket` is executed and the application state is modified
2. `packetCommitment` has been cleared out
3. `packetReceipt` is empty | 1. `onTimeoutPacket(..)==True; app.State(beforeTimeoutPacket)!=app.State(afterTimeoutPacket)`
2. `provableStore.get(packetCommitmentPath(packet.channelSourceId, packet.sequence)) === null`
3. `provableStore.get(packetReceiptPath(packet.channelDestId, packet.sequence))==null`
| -| **Post-Conditions (Error)** | 1. If `onTimeoutPacket` fails and the application state is unchanged
2. `packetCommitment` is not cleared out | 1. `onTimeoutPacket(..)==True; app.State(beforeTimeoutPacket)!=app.State(afterTimeoutPacket)`
2. `provableStore.get(packetCommitmentPath(packet.channelSourceId, packet.sequence)) === null` | +| **Post-Conditions (Success)** | 1. `onTimeoutPacket` is executed and the application state is modified
2. `packetCommitment` has been cleared out
3. `packetReceipt` is empty
4. Event is Emitted
| 1. `onTimeoutPacket(..)==True; app.State(beforeTimeoutPacket)!=app.State(afterTimeoutPacket)`
2. `provableStore.get(packetCommitmentPath(packet.channelSourceId, packet.sequence)) === null`
3. `provableStore.get(packetReceiptPath(packet.channelDestId, packet.sequence))==null`
4. Check Event is Emitted
| +| **Post-Conditions (Error)** | 1. If `onTimeoutPacket` fails and the application state is unchanged
2. `packetCommitment` is not cleared out
3. No Event Emission
| 1. `onTimeoutPacket(..)==True; app.State(beforeTimeoutPacket)!=app.State(afterTimeoutPacket)`
2. `provableStore.get(packetCommitmentPath(packet.channelSourceId, packet.sequence)) === null`
3. Check No Event is Emitted
| ###### Pseudo-Code