Home

Welcome to the Move Smart Contracts wiki!

• Starting the application
• Using the Model Editor panel
• Using the Move Code Editor panel
• Using the Verification Properties panel
• Creating an FSM from Move code
• Creating Move code from the Model
• Verifying the smart contract (model)

Using the Move Code Editor panel

The Move Code Editor panel allows users to create their own custom move code, use the code defined by their model, and create their FSM model by the code defined in the editor.

The code editor is set for Rust syntax highlighting, similar to how Diem has it.

To view saved code, the user can start writing code into the editor and click SAVE CODE. This will add a new attribute to the contract model (seen on the right-hand side in the property editor panel). The code will be saved here and can be reaccessed from the VIEW SAVED CODE button.

If you have an FSM model defined in the Model Editor panel, running the MoveCodeGenerator plugin will generate the Move code based on the model and that can be accessed using the VIEW GENERATED CODE button. Remember to click SAVE CODE afterward so that the customMoveCode attribute can be correctly updated.

To build the FSM based on the code in the move code editor, just save the code (so the customMoveCode attribute is updated) and run the FSMGenerator plugin. Then navigate back to the Model Editor panel and view your new FSM model.

Using the Verification Properties panel

The Verification Properties Panel acts as an interface to define specific Properties that want to be checked for in the Contract.

4 types of properties can be checked:

1. Action 1 cannot happen after Action 2
2. Action 1 can only happen after Action 2
3. If Action 1 happens, Action 2 can only happen after Action 3 happens
4. Action 1 will eventually happen after Action 2 happens

The actions are defined to be the transitions in the model editor.

To use this panel, add the properties by putting in the actions in their respective spots and clicking ADD. When the button is pressed, the properties are added into the Existing Properties category and more can be added afterward.

Note to add multiple actions into one sentence, the | operator can be used for “or” clauses.

Once these are all defined, the VerifyContract plugin can be used to verify the properties listed under Existing Properties

Creating an FSM from Move code

The FSMGenerator plugin uses the code inside the customMoveCode attribute of the model to create the FSM. The plugin will go into the Model Editor panel and remove all the nodes already in the panel (clear the panel) and then create an initial state and a base state as well as a createTransition transition from the initial state to the base state. The functions defined in the code will then be used as transitions to loop back the base state.

Creating Move code from the Model

When the model is created in the Model Editor and the code defined in it is to be retrieved, the MoveCodeGenerator plugin can be used. The generated code will be stored in the generatedMoveCode attribute and can be seen with the View Generated Code button in the Move Code Editor panel. This code can then be saved using the save code button into the CustomMoveCode attribute to be used further.

Verifying the smart contract (model)

The contract can be verified using the VerifyContract plugin. This plugin uses the properties defined in the Verification Properties panel and will allow users to download information about the contract.