Smart Contract Modeling Language (SmartCML) - ADOxx Application Library and Code Generator

Smart Contract Modeling Language (SmartCML) Reference Sheet Simon Curty Contents 1 Language Concepts 1 1.1 Overview ........................................ 1 1.2 Omitted Solidity Language Features ......................... 4 2 Graphical Notation 5 3 By Example 7 3.1 Operations ....................................... 7 3.2 Function Returns .................................... 7 3.3 Reading from Contract State ............................. 8 3.4 Writing to Contract State ............................... 8 3.5 Emitting Events .................................... 9 3.6 Simple Conditions ................................... 9 3.7 If-Else Conditions and the Identity Operation .................... 10 3.8 Nested Conditions ................................... 10 3.9 Chaining Conditions .................................. 11 3.10 Guards and Failures .................................. 12 3.11 Arrays .......................................... 12 3.12 Structs and Mappings ................................. 13 3.13 Code Blocks ....................................... 13 3.14 Loops .......................................... 14 3.15 Function Calls ..................................... 15 1 Language Concepts The Smart Contract Modeling Language (SmartCML) is a domain-specific visual programming language for the development of Ethereum-compatible smart contracts. In its current iteration, SmartCML translates into Solidity and supports some of the language features specific to Solidity. Smart contracts are modeled as a set of function graphs that specify actions to be taken (such as an arithmetic operation) and the execution flow (the context-dependent sequence of execution steps) of a function invocation. Boundaries define how data can be exchanged outside of the scope of a function graph. 1.1 Overview Execution flow: The execution flow is the context-dependent sequence of execution steps, as defined by the relations connecting Ports of Action elements with subsequent model elements. A flow is thus a traversal of the respective function graph. 1 Action: Actions are elements that model some functional behavior, for example, an operation or a Boolean condition. Each action has a set of Ports depending on the concrete type of action. Port: Each Action has outgoing ports that define the execution flow. The ports available depend on the concrete type of action. Relations are attached to ports and are activated, that is followed as part of an execution flow, depending on a fixed port precedence: initial > true > false > mid/call > final initial: The initial port is activated before the behavior specified by the Action element is executed. That is, the execution flow is re-directed to the model element connected to this port. true and false: The true and false ports are only available for actions of type Condition (see Table 1). If the condition is true, then the true port is activated; otherwise, and only if connected, the false port is activated. mid/call: The mid/call port is only available for actions of type Emission and Function Call (see Table 1). This port is activated as part of the execution of the action, for example, to emit a parameterized event. final: The final port is activated last and only if the execution flow did not terminated. Boundary: ABoundary element defines the communication points to exchange data outside of the scope of the contract function. This includes the entry point of an execution flow through a Function Interface element or the emission of an Event (see Table 1). Definitions: SmartCML is typed. The available types are defined by the modeler in a shared model, called Definitions map. It is distinguished between Basic Types for primitive data types and Complex Type for maps, arrays, and structs. Further, Builtin Functions, that is, the functions provided by the execution environment, that is, the EVM, are also defined by the modeler as part of the Definitions map. SmartCML Concept (supertype) Out Ports Description Solidity language feature Operation (Action) initial, final (i) Arithmetical or Boolean operation with assignment to a result variable. (ii) Assignment of values to a variable (unary identity operation). Local variable assignment statement, expressions. Condition (Action) initial, true, false, final Branch control structure based on a Boolean expression. If the expression is true, the true port is triggered, otherwise, and only if specified, the false port is triggered. The final port specifies how the program should continue, regardless of the condition’s result. Conditions can be utilized to model loops. if-else-statements and whilestatements Declaration (Action) initial, final Used to declare an instance variable and to instantiate a struct with specifiable parameters). Struct instantiation statement with assignment to a (local) variable. 2 SmartCML concepts — Table continued from previous page SmartCML Concept (supertype) Ports Description Solidity language feature Emission (Action) initial, mid, final Specification of data to be routed through a boundary element for the purpose of (i) returning function results (via Function Interface), (ii) emitting events (via Event), and throwing failures (via Failure). return/event/error parameter assignment Function Call (Action) initial, call, final Specification of function parameters for an invocation of an internal (contract-scope) function via a Function Interface, or an external (imported or builtin) function via a Proxy Interface. Function call parameter assignment Code Block (Action) initial, final General purpose element for the inclusion of user-specified code or unsupported language features such as EVM assembly. n/a Function Interface (Boundary) final (implicit) Defines a contract function and its (if any) parameters and return types. The Function Interface is the starting point of an execution flow. A function return is specified in combination with an Emission Action. A Function Interface can be called within the contract using a Function Call Action. Function declaration Proxy Interface (Boundary) none Serves as reference to either a builtin function of the execution environment (EVM) or an external function imported from another contract. A Proxy Interface is called with a Function Call Action. Native EVM function call or external contract function call. Event (Boundary) none Defines an event with optional parameters that can be emitted through an Emission Action. Emitting an event does not terminate the function flow. Event definition Failure (Boundary) none Defines an error with optional parameters that can be thrown through an Emission Action. Throwing a failure does terminate a function flow. Error definition Storage none Declaration of a contract state variable. A Storage is part of the contract-scope, not of a single function flow. Read and write operations must be modeled explicitly. Contract state variable definition Flow (Relation) n/a From an outgoing port of any action or a Function Interface specifies the subsequent action or boundary element to be executed. If an element has multiple ports, attached flow relations are triggered according to a fixed port precedence: initial > true > false > mid/call > final. Order of statements 3 SmartCML concepts — Table continued from previous page SmartCML Concept (supertype) Ports Description Solidity language feature Read-access (Relation) n/a Defines a explicit read-only access to a contract-scope Storage element making the underlying state variable available to an action. The Read-Access Relation is triggered from the initial port of an action. Reading the value from a contract state variable Write-Access (Relation) n/a Defines the explicit writing of a value to a contract-scope Storage element and thus indicates a contract state change. The WriteAccess Relation is triggered from an outgoing port of an action. Writing a value to a contract state variable Call (Relation) n/a Specifies a invocation of a Proxy Interface (reference to a builtin or external function) or a Function Interface (contract function). Function invocation Basic Type (Definition) n/a Defines a basic (primitive) data type as part of a shared Definitions map model. Basic types in Solidity, e.g., integers and Booleans. Complex Type (Definition) n/a Defines a data structure type as part of a shared Definitions map model. In particular, aComplex Type defines a typed struct, map, or an array. Types for structs, mappings, and arrays Table 1: Summary of SmartCML concepts and their mapping to Solidity language features. 1.2 Omitted Solidity Language Features Some features of Solidity have been omitted and are not directly supported on the basis of low popularity of features, contradiction with core design choices, or simplicity. Some of the omitted features can be substituted with another construct. A summary of notable omitted features is given below: •inline assembly (can be achieved with Code Blocks) •enumerations (rarely used) •for-loops and do-while (substituted with while-loops) •require (substituted with revert and errors) •try statements •modifiers 4 2 Graphical Notation The graphical notation is based on simple geometric shapes in which related elements share design elements. The elements are used in two model types: The Definitions map is used to define data types, data structure types, and builtin function. The notation used in this model type is illustrated in Table 2. The Smart Contract model type then defines the actual behavior and structure of a contract. The visual representation of the elements and relations comprising a smart contract is given in Table ??. Each Action type is denoted by a distinctive decorated circle and has an annotation that designates what the action represents. For example, a Condition could have the annotation «if» or «while», depending on whether the element translates to an if-else statement or a loop. Boundary elements, that is, Interfaces and Emitters, are uniquely named as they represent a distinct definition in the smart contract, for example, of an error. In addition, Boundaries display what data is transmitted in the form of parameters and return values. Each relation shows the port from which it is activated. The visualization of the Access relation is based on the access mode (read or write) and additionally denotes the variables read from, or written to state, represented by the Storage element. Basic Type Array Type «pre-defined» uint «pre-defined» UintArray uint[] Definition of a basic (primitive) data type Definition of an array data structure type Map Type Struct Type «pre-defined» IntStrMap (int -> string) «user-defined» Person name : string addr : address Definition of a mapping data structure type Definition of a struct (object-like) data structure type Builtin Function «user-defined» ƒ concat string,string -> string Definition of a builtin function as part of the execution environment Table 2: Graphical notation of the modeling elements that comprise a SmartCML Definitions map model. 5 Operation Condition Declaration a «- b + c «op» a == b «if» a_struct «- new Struct «create» Arithmetic or Boolean operation with assignment (action element) Branching control structure: if-else, while (action element) Declaration of an instance variable, for example, for a struct (action element) Emission Function Call Code Block via Event a_param «emit» ƒ function «call» { • } «code» Assignment of variables for emission (or return) of data via a boundary element, for example, an Event (action element) Assignment of variables for invoking a function represented as Function Interface or a Proxy (action element) Inclusion of additional code such as EVM assembly (action element) Function Interface Failure Event function » arg1:int « 1:int AFailure « arg1:int AnEvent « arg1:int Definition of a parameterized contract function (boundary element) Definition of a failure that when triggered reverts a transaction (boundary element) Definition of an event that carries outgoing data (boundary element) Proxy Storage Flow Relation function ƒ state_var : int [port] Delegates a function call to a Builtin Definition or an external Function Interface (element) Definition of a typed smart contract state variable (element) Specifies the subsequent action or boundary from the outgoing port (relation) Access Relation (read) Access Relation (write) Call Relation [port] state_a [port] write_state [port] Read access to a contract Storage element (relation) Write access to a contract Storage element (relation ) Specification of the target of a Function Call action. Valid targets are internal Function Interfaces and Proxy elements (relation) Table 3: Graphical notation of the modeling elements that comprise a SmartCML Visual Smart Contract model. 6 3 By Example In the following, the concepts of SmartCML are introduced with examples. Each example is accompanied by an excerpt of the Solidity code that corresponds to the model. 3.1 Operations add » a:uint, b:uint res «- a + b «op» Figure 1: Function for adding two integers. The function is defined by the Function Interface named add. Below its symbol the function parameters with name and type are listed. An action of type Operation then adds the variables and assigns the result to a new local variable res. Note that this function does not return anything. Listing 1: Generated solidity code that corresponds to Figure 1. function add(uint a, uint b) public pure { uint res = a + b; } 3.2 Function Returns add » a:uint, b:uint « 1:uint res «- a + b «op» via add res «return» [final] [final] Figure 2: Function for adding two integers and returning the result. The Function Interface named add specifies a single integer return type (unnamed, the position of the return argument is indicated by the index). After the first action element, adding the numbers, the final port is activated and the subsequent Emission action executed. This action specifies that the local variableres is to be returned via the initial boundary, the Function Interface add. This is modeled by connecting the flow from the final port back to the interface. Listing 2: Generated solidity code that corresponds to Figure 2. function add(uint a, uint b) public pure returns (uint) { uint res = a + b; return (res); } 7 3.3 Reading from Contract State add » a:uint « 1:uint res «- a + num «op» via add res «return» [final] [final] num : uint [initial] num Figure 3: Before the first action element, adding the numbers, is executed, the initial port is activated and the state variable num is read from the Storage element, modeled using a ReadAccess relation. This makes the state variable available to the action. Listing 3: Generated solidity code that corresponds to Figure 3. uint num; function add(uint a) public view returns (uint) { uint res = a + num; return (res); } 3.4 Writing to Contract State add » a:uint « 1:uint res «- a + num «op» via add res «return» [final] [final] num : uint [initial] num [initial] res Figure 4: Before the Emission action returns the value of res, the initial port is activated. The port connects the action element with the Storage element using a Write-Access relation, modeling an assignment of the value of res to the contract state variable num. This results in a modification of the contract state. Listing 4: Generated solidity code that corresponds to Figure 4. uint num; function add(uint a) public returns (uint) { uint res = a + num; num = res; return (res); } 8 3.5 Emitting Events add » a:uint res «- a + num «op» via NewNum res «emit» [final] num : uint [initial] num [initial] res NewNum « number:uint [final] Figure 5: Instead of returning the operation’s result, it is emitted as part of an Event boundary element, named NewNum. The Event boundary element defines a type of event on the contractscope. The Emission action element assigns the event parameters and emits it as part of an execution flow and assigns the event parameters. Listing 5: Generated solidity code that corresponds to Figure 5. event NewNum(uint number); uint num; function add(uint a) public { uint res = a + num; num = res; emit NewNum(res); } 3.6 Simple Conditions storeNum » a:uint a > `10` «if» num : uint [true] a Figure 6: This function stores an integer in the contract state if the given number is greater than 10. This is modeled using a Condition action and subsequent activation of the true port with a Write-Access relation attached. Here, the false port is not used, that is, there is no else-condition specified — it is not required to use all ports. Similarly, the final port is also not used. As such, after the condition has been executed, including the true and false ports, there is no further step specified. Listing 6: Generated solidity code that corresponds to Figure 6. uint num; function storeNum(uint a) public { if (a > 10) { num = a; } } 9