[review] MIP-58: Lock/Mint-type Bridge Design

.github/CODEOWNERS

@@ -6,9 +6,10 @@
 /MIP/mip-0/ @l-monninger @apenzk
 /MD/md-0/ @l-monninger @apenzk
 /MG/mg-0/ @l-monninger @apenzk
-/MIP/mip1/ @l-monninger
+/MIP/mip-1/ @l-monninger
 /MD/md-3/ @l-monninger
 /MIP/mip-15/ @l-monninger @apenzk
 /MD/md-15/ @l-monninger @apenzk
 /MIP/mip-39/ @franck44
 /MIP/mip-53/ @l-monninger
+/MIP/mip-58/ @primata @apenzk

.vscode/settings.json

@@ -1,4 +1,5 @@
 {
     "stm32-for-vscode.openOCDPath": false,
-    "stm32-for-vscode.armToolchainPath": false
+    "stm32-for-vscode.armToolchainPath": false,
+    "spellright.userDictionary": "${workspaceFolder}/.vscode/spellright.dict"
 }

.vscode/spellright.dict

@@ -0,0 +1,5 @@
+Fastconfirmation
+multisig
+timelock
+timelocks
+trustlessness

MIP/mip-0/README.md

@@ -1,7 +1,8 @@
 # MIP-0: Formalize Movement Proposals
-- **Description**: A process through with Movement Improvement Proposals standardize and formalize specifications for Movement technologies.
-- **Authors**: [Liam Monninger](mailto:liam@movementlabs.xyz), [Andreas Penzkofer](mailto:andreas.penzkofer@movementlabs.xyz)
-- **Desiderata**: [MD-0](../MD/md-0)
+
+- **Description**: A process through which Movement Improvement Proposals standardize and formalize specifications for Movement technologies.
+- **Authors**: [Liam Monninger](mailto:liam@movementlabs.xyz), Andreas Penzkofer
+- **Desiderata**: [MD-0](../../MD/md-0)
 
 ## Abstract
 

MIP/mip-1/README.md

@@ -14,7 +14,7 @@ This protocol was originally suggested as a solution to minimizing trust assumpt
 
 ## Specification
 
-The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in RFC 2119 and RFC 8174.
+_The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in RFC 2119 and RFC 8174._
 
 ### Protocol Description
 
@@ -33,6 +33,7 @@ The following messages types are exchanged between the Enclave and the Client:
 These messages are exchanged as follows:
 
 **Synchronization Phase**
+
 1. Prior to sending its first application message, the Client generates and safely stores CSPRNG nonce and sends it to the Enclave in a SYN message.
 2. The Enclave processes the SYN message:
     - If enclave does not have a stored nonce, this indicates that no other client has attempted to synchronize with the Enclave. The Enclave MUST accept the nonce, store the nonce, and respond with a SYN-OK message.
@@ -41,6 +42,7 @@ These messages are exchanged as follows:
         - If the nonce is not at the top of the queue or has not passed its time-lock, the Enclave MUST respond with a SYN-TL message.
 
 **Application Phase**
+
 1. The Client sends an APP message to the Enclave with the application message and the nonce for the current message and the nonce for the next message.
 2. The Enclave processes the APP message:
     - If the nonce for the current message is the expected nonce, the Enclave MUST process the application message and update the nonce for the next message. It MUST responds with an APP-OK message.
@@ -66,9 +68,11 @@ A MLABSO is informed that the bridge service needs to be upgraded. Because the p
 Now, a malicious MLABSO decides to attempt to abuse the key. She knows she cannot directly access the key. She also knows that she will not be able to use the key until the program has synchronized to a nonce she controls. She deems discovering or replacing the nonce used in the existing program intractable. So, she must stop the service and start a new synchronization phase. This will time-lock the service for 20 minutes. However, in the end, she will have the ability to sign with the key. The MLABSO begins the synchronization phase. However, during this time, a legitimate MLABSO notices that the bridge service is being upgraded (perhaps even that it is down). The legitimate MLABSO then reviews access logs to discover the malicious MLABSO's actions. The malicious MLABSO and her program are then removed from the system before the new bridge service can be synchronized.
 
 ### Practical Considerations
-In practice, there are several phenomena regarded as external to the ENTL protocol which need to be considered in order to make it safely usable. 
+
+In practice, there are several phenomena regarded as external to the ENTL protocol which need to be considered in order to make it safely usable.
 
 #### Securing the Nonce
+
 In order to avoid the possibility of malicious usage, both the current nonce and the next nonce need to be stored in a manner that is difficult to access except by the current program. We do not intend to impose cryptographically secure requirements on this storage, as that begins to invoke concepts related to the literature on succinct arguments for programs. However, there are several simpler ways that can make accessing the and using the outside  nonce difficult.
 
 To describe these, it first helps to consider what enables a nonce attack and to consider the time these operations take.

MIP/mip-15/README.md

@@ -1,4 +1,5 @@
 # MIP-15: MG (Movement Gloss)
+
 - **Description**: Introduces the Movement Gloss (MG) document type and establishes a process for introducing new glossary terms. Introduces the [Glossary](../GLOSSARY.md), which contains an overview of all terms defined through MGs.
 - **Authors**: [Liam Monninger](mailto:liam@movementlabs.xyz)
 - **Reviewer**: Andreas Penzkofer
@@ -18,23 +19,27 @@ The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "S
 
 ### Glossary
 
-The [Glossary](../GLOSSARY.md) is an alphabetically ordered list of terms defined through MGs. Any term introduced through an MG MUST be declared in the Glossary. 
+The [Glossary](../GLOSSARY.md) is an alphabetically ordered list of terms defined through MGs. Any term introduced through an MG MUST be declared in the Glossary.
 
 The Glossary table contains the following columns:
+
 - The Term
 - A short definition
 - The number of the MG that introduces the term
 
 ### MG Document Type
+
 A template for the MG is provided at [mg-template](../../md-template.md). An example MG is provided at [mg-0](../../MG/mg-0/README.md). These templates cover the requested elements listed in [MD-15.D1](../MD/md-15/README.md).
 
 ### MG Process
+
 1. A new glossary term MUST be defined in an MG document matching the provided templates.
 2. An MG document MUST not be accepted unless justified in an MIP.
 
-For example, herein, we justify the introduction of [MG-0](../../MG/mg-0/README.md). MG-0 defines the term "gloss" which is used in the context of Movement Labs to denote the definition of a term as would feature as an entry in a glossary. It is important to include in the glossary both clarify as the acronym "MG" and to provide an example gloss. 
+For example, herein, we justify the introduction of [MG-0](../../MG/mg-0/README.md). MG-0 defines the term "gloss" which is used in the context of Movement Labs to denote the definition of a term as would feature as an entry in a glossary. It is important to include in the glossary both clarify as the acronym "MG" and to provide an example gloss.
 
 ## Reference Implementation
+
 See the MG document type template at [mg-template](../../md-template.md) and the example MG at [mg-0](../../MG/mg-0/README.md).
 
 ## Verification

MIP/mip-39/README.md

@@ -17,7 +17,7 @@ This MIP describes the high-level architecture of the [HTLC-based](https://bitco
 
 The Movement chain (L2) uses the \$L2MOVE token to pay for gas fees. As a result users need to hold \$L2MOVE tokens to pay for their transactions.
 
-> [!IMPORTANT] 
+> [!IMPORTANT]
 > The _native_ \$L1MOVE token is an ERC-20 contract on Ethereum (L1).  By native, we mean that this is the location where the token is minted and burned and where the total supply is set and possibly modified (inflation/deflation). The **\$L1MOVE token reserve**  is in the L1 contract.
 
 To use the Movement chain and pay for gas fees, a user will acquire \$L1MOVE (native) tokens on L1, and _bridge_ them to L2. On the L2 they can use the token to pay for gas fees or with any other dApps that transact the \$L2MOVE token.
@@ -282,7 +282,7 @@ To reproduce the results and check the properties on the model, you need a worki
 
 The results of the model-checking verification are as follows: let $maxRelayerDelay $ be the **maximum delay** for the relayer to relay an event, and $timeLock1$ and $timeLock2$ be the timelocks on L1 and L2 respectively.
 
-> [!IMPORTANT] 
+> [!IMPORTANT]
 > **Verification results**
 > We have **proved** (model-checked with UPPAAL) the following properties (valid using the versions of the contracts below):
 >

MIP/mip-53/README.md

@@ -1,8 +1,8 @@
 # MIP-53: Conventions for Proposing Progressive L2 Models
+
 - **Description**: Introduces conventions for proposing progressive L2 models.
 - **Authors**: [Liam Monninger](mailto:liam@movementlabs.xyz)
-- **Reviewer**: [Andreas Penzkofer](mailto:andreas.penzkofer@movementlabs.xyz)
-- **Desiderata**: $\emptyset$
+- **Reviewer**: Andreas Penzkofer
 
 ## Abstract
 
@@ -15,6 +15,7 @@ We propose a set of conventions including naming, formatting, and related standa
 In order to facilitate the development of L2 systems, it is important to have a clear and consistent way to propose and review models for these systems. This MIP aims to provide a set of conventions for proposing progressive L2 models that will help to ensure that proposals are clear, consistent, and easy to review.
 
 ## Specification
+
 Progressive L2 models should adhere to conventions of the following forms:
 
 - **naming**: apply a standard naming format.
@@ -24,18 +25,21 @@ Progressive L2 models should adhere to conventions of the following forms:
 - **pros and cons**: a list of pros and cons.
 
 ### Naming
-All proposed progressive L2 models MUST adopt a name of the form "The [Location] Model" where [Location] is a location where the proposal was drafted or a similarly symbolic location. This name should be the title of the associated MIP. 
 
-In text, the model SHOULD be referred to as "[Location] Model," that is, the name of the model in title case. 
+All proposed progressive L2 models MUST adopt a name of the form "The [Location] Model" where [Location] is a location where the proposal was drafted or a similarly symbolic location. This name should be the title of the associated MIP.
+
+In text, the model SHOULD be referred to as "[Location] Model," that is, the name of the model in title case.
 
 ### Acknowledgement of Standards
+
 At the start of the "Specification" section of the MIP, the author MUST include the following markdown snippet:
 
 ```
 We acknowledge and apply the conventions of [MIP-53: Conventions for Proposing Progressive L2 Models](../mip-53/).
 ```
 
 ### Summary Table
+
 All proposed progressive L2 models MUST complete the following table:
 
 | Category | Criterion | Evaluation |
@@ -51,9 +55,11 @@ All proposed progressive L2 models MUST complete the following table:
 |X| [Component Name 2](link/to/component/design) | A description of usage of said component.  |
 
 ### Statement Towards Progression
+
 All proposed progressive L2 models MUST include a statement of how the model suits a progressive approach to L2 design and release. This statement SHOULD be a paragraph in length and immediately follow the summary table--as if it were a caption for the table.
 
 ### Pros and Cons
+
 All proposed progressive L2 models MUST include a list of pros and cons. This list SHOULD be formatted as two separate bulleted lists in subsections titled "Pros" and "Cons."
 
 ## Verification