morley 1.7.0 → 1.7.1

raw patch · 20 files changed

+787/−107 lines, 20 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGES.md +4/−3
• README.md +53/−46
• app/Main.hs +1/−1
• app/REPL.hs +6/−1
• docs/language/morleyInstructions.md +76/−0
• docs/language/morleyLanguage.md +42/−0
• docs/language/morleyLet.md +168/−0
• docs/language/morleyMacros.md +69/−0
• docs/language/morleySyntaxSugar.md +138/−0
• docs/michelsonTypes.md +43/−0
• docs/morleyInterpreter.md +55/−0
• docs/morleyRuntime.md +49/−0
• docs/morleyTypechecker.md +31/−0
• morley.cabal +12/−4
• src/Michelson/FailPattern.hs +17/−14
• src/Michelson/Interpret/Unpack.hs +0/−5
• src/Michelson/Runtime.hs +12/−2
• src/Michelson/Typed/Value.hs +3/−27
• src/Morley/Micheline/Json.hs +4/−0
• src/Tezos/Crypto/Util.hs +4/−4

@@ -1,6 +1,7 @@-Unreleased-==========-<!-- Append new entries here -->+1.7.1+=====+* [!549](https://gitlab.com/morley-framework/morley/-/merge_requests/549)+  Add `instance Buildable TezosInt64`.  1.7.0 =====

@@ -2,56 +2,22 @@  [![Hackage](https://img.shields.io/hackage/v/morley.svg)](https://hackage.haskell.org/package/morley) -Morley is a library to make writing smart contracts in Michelson pleasant and-effective.--## I: A reimplementation of the Michelson Language in Haskell--It consists of the following parts:--- [`Tezos.*`](src/Tezos/) hierarchy is designed to implement cryptographic primitives, string and byte formats, and any other functionality specific to the Tezos protocol which is required for testing/execution of Michelson contracts but is used not only by Michelson.-- [`Michelson.Untyped`](src/Michelson/Untyped.hs) and [`Michelson.Typed`](src/Michelson/Typed.hs) hierarchies define Haskell data types that assemble a Michelson contract. See [michelsonTypes.md](/docs/michelsonTypes.md).-- [`Michelson.TypeCheck`](src/Michelson/TypeCheck.hs): A typechecker that validates Michelson contracts according to the Michelson's typing rules. Essentially, it performs conversion from untyped representation to the typed one. See [morleyTypechecker.md](/docs/morleyTypechecker.md).-- [`Michelson.Interpret`](src/Michelson/Interpret.hs): An interpreter for Michelson contracts which doesn't perform any side effects. See [morleyInterpreter.md](/docs/morleyInterpreter.md).-- [`Michelson.Macro`](src/Michelson/Macro.hs) Types for macros, syntactic sugar, and other extensions that are described in the next chapter.-- [`Michelson.Parser`](src/Michelson/Parser.hs) A parser to turn a `.tz` or `.mtz` file (`.mtz` is a Michelson contract with Morley extensions) into a Haskell ADT.-- [`Michelson.Runtime`](src/Michelson/Runtime.hs): A high-level interface to Morley functionality, see [morleyRuntime.md](/docs/morleyRuntime.md).--## II: Morley extensions--One way to test Michelson contracts is to use the Morley language.-It is a superset of the Michelson language, which means that each Michelson contract is also a valid Morley contract but not vice versa.-There are several extensions which make it more convenient to write Michelson contracts and test them.-For example, one can write inline assertions in their contracts for testing.-All the details can be found in [the document](/docs/morleyLanguage.md) about these extensions.-Also, there is a transpiler from Morley to Michelson.--## III: Morley-to-Michelson transpiler--Morley-to-Michelson transpiler can be used to produce a Michelson contract from a Morley contract.-You should use it if you want to develop contracts in Morley and submit them to the Tezos network.-Workflow is the following:--1. If your contract is called `foo.mtz`, use `morley print --contract foo.mtz --output foo.tz`. Note that normally you should not use `morley` directly, you should use `morley.sh` or `stack exec -- morley`. See usage instructions below.-2. After that, you can use existing Tezos tools to deploy your contract. You can also typecheck or interpret it using a reference implementation. If you are not familiar with the Tezos tooling, please read [Tezos documentation](https://tezos.gitlab.io/index.html) or [Michelson tutorial](https://gitlab.com/morley-framework/michelson-tutorial).--## Running and building+Morley aims to make writing smart contracts in Michelson pleasant and effective.+It contains 3 major things:+1. An [executable](#morley-executable) that lets you perform various operations on Michelson smart contracts.+2. A [library](#morley-library) with core Tezos and Michelson data types, and functions such as Michelson typechecker and interpreter.+3. A superset of the Michelson language that we call the [Morley language](#morley-language).+It relaxes Michelson parser rules, adds some syntax sugar and simple features. -Morley executable provides the following functionality:-- `parse` contract and return its representation in Haskell types.-- `typecheck` contract.-- `run` contract. A given contract is being originated first, and then the transaction is being sent to it-- `originate` contract.-- `transfer` tokens to a given address.-- `print` produce `.tz` contract that can be parsed by the OCaml referenced client from `.mtz` or `.tz` contract.+## Morley executable -You can get more info about this command by running `morley <command> --help`+### How to install  There are three ways to get Morley executable: - [Docker](https://docs.docker.com/) based (preferable).   * Get [script](/scripts/morley.sh)  (e. g. using `curl https://gitlab.com/morley-framework/morley/raw/master/scripts/morley.sh > morley.sh`)-  and run it `./morley.sh <args>`. This script will pull a docker image that contains the latest version of Morley executable from the master branch and run it with the given arguments.+  and run it `./morley.sh <args>`. This script will pull a docker image that contains the latest version of Morley executable from the `production` branch and run it with the given arguments.     You'll need `coreutils` to be installed in order to use `morley.sh`.   * Usage example:     + `./morley.sh` to see help message@@ -69,6 +35,47 @@     + `cabal new-run -- morley --help` to see help message     + `cabal new-run -- morley originate --contract contracts/tezos_examples/attic/add1.tz --storage 1 --verbose` -For more information about Morley commands, check out the following docs:-- [Interpreter doc](/docs/morleyInterpreter.md)-- [Typechecker doc](/docs/morleyTypechecker.md)+### Usage++Morley executable does not interact with Tezos node and Tezos network.+It works in _emulated environment_ which is stored in a simple JSON file on disk.+The following commands depend on environment and may modify it:+- `originate` a contract.+- `transfer` tokens to a given address (and call a smart contract if it's the destination).+- `run` a contract. A given contract is being originated first, and then the transaction is being sent to it.++The following commands don't depend on environment:+- `optimize` a contract by replacing certain sequences of instructions with equivalent but more efficient ones.+- `typecheck` a contract.+- `repl` starts a REPL where you can type Michelson instructions and interpret them.+- `analyze` a contract and print some statistics about it.+- `print` a contract in vanilla Michelson format.+It can be useful in some cases:+  + You have a smart contract that uses [Morley extensions](#morley-language) and want to convert it to vanilla Michelson format that can be handled by Tezos reference implementation.+  + You have a contract with inconsistent/ugly formatting and want to format it in uniform style.+  + You want to print a contract on a single line.+- `parse` a contract and return its representation in Haskell types.++You can get more info about these commands by running `morley <command> --help`.+Run `morley --help` to get the list of all commands.++## Morley library++Morley-the library is available on [Hackage](https://hackage.haskell.org/package/morley).+It consists of the following parts:++- [`Tezos.*`](src/Tezos/) hierarchy is designed to implement cryptographic primitives, string and byte formats, and any other functionality specific to the Tezos protocol which is required for testing/execution of Michelson contracts but is used not only by Michelson.+- [`Michelson.Untyped`](src/Michelson/Untyped.hs) and [`Michelson.Typed`](src/Michelson/Typed.hs) hierarchies define Haskell data types that assemble a Michelson contract. See [michelsonTypes.md](./docs/michelsonTypes.md).+- [`Michelson.TypeCheck`](src/Michelson/TypeCheck.hs): A typechecker that validates Michelson contracts according to the Michelson's typing rules. Essentially, it performs conversion from untyped representation to the typed one. See [morleyTypechecker.md](./docs/morleyTypechecker.md).+- [`Michelson.Interpret`](src/Michelson/Interpret.hs): An interpreter for Michelson contracts which doesn't perform any side effects. See [morleyInterpreter.md](./docs/morleyInterpreter.md).+- [`Michelson.Macro`](src/Michelson/Macro.hs) Types for macros, syntactic sugar, and other extensions that are described in the next chapter.+- [`Michelson.Parser`](src/Michelson/Parser.hs) A parser to turn a `.tz` or `.mtz` file (`.mtz` is a Michelson contract with Morley extensions) into a Haskell ADT.+- [`Michelson.Runtime`](src/Michelson/Runtime.hs): A high-level interface to Morley functionality, see [morleyRuntime.md](./docs/morleyRuntime.md).++## Morley language++Morley-the-language is a superset of the Michelson language, which means that each Michelson contract is also a valid Morley contract but not vice versa.+There are several extensions which make it more convenient to write Michelson contracts and test them.+For example, one can write inline assertions in their contracts for testing.+All the details can be found in [the document](./docs/language/morleyLanguage.md) about these extensions.+A smart contract written in the Morley language can be transpiled to Michelson using the aforementioned `morley print` command.

@@ -301,7 +301,7 @@         putTextLn "Contract is well-typed"       Run RunOptions {..} -> do         michelsonContract <- prepareContract roContractFile-        runContract roNow roMaxSteps roInitBalance roDBPath roStorageValue michelsonContract roTxData+        void $ runContract roNow roMaxSteps roInitBalance roDBPath roStorageValue michelsonContract roTxData           ! #verbose roVerbose           ! #dryRun (not roWrite)       Originate OriginateOptions {..} -> do

@@ -60,6 +60,11 @@ -- a result of user pressing Ctrl-c in an attempt to end a loop. repl :: ReplM () repl = do+  printHelp+  repl_++repl_ :: ReplM ()+repl_ = do    minput <- getInputLine "Morley>>> "    case strStrip <$> minput of      Nothing -> pass -- Ctrl D@@ -77,7 +82,7 @@         (stripPrefix ":" -> Just cmd) ->           printErr $ "Unknown command`"<> (toText cmd) <> "`. Use :help to see a list of commands"         _ -> handle (\Interrupt -> putTextLn "Cancelled") $ withInterrupt $ runCode (toText input)-      repl+      repl_   where     strStrip = toString . strip . toText 

@@ -0,0 +1,76 @@+<!--+SPDX-FileCopyrightText: 2020 Tocqueville Group++SPDX-License-Identifier: LicenseRef-MIT-TQ+-->++# Morley Ext Instructions++Morley adds some additional instructions of its own to the existing set of+Michelson instructions. These instructions are not macros and have no effect on+a contract's execution. That is, they cannot write or alter any value on the+stack, but simply provide a mechanism to pass additional+information to Morley's typechecker or runtime.++## `STACKTYPE`++The `STACKTYPE` instruction allows us to assert that the stack has a given type+signature. For example, `STACKTYPE '[]` asserts that the stack is the empty+stack, and tells the typechecker to fail the contract otherwise.++### Stack Type Signature++A stack signature can be either an empty stack, a list of types, or a pattern+match on the head of the stack:++```+Empty stack: '[]+stack of three int: '[int, int, int]+A pattern match on a stack with two int at the top: '[int, int, ...]+```++More formally, a stack signature is like a `cons` list with two distinct+`nil`-like terminators:++```+<stack-sig> := "'[" (<empty-stack> | <rest-of-stack> | <stack-cons>)+<empty-stack> := "]"+<rest-of-stack> := "...]"+<stack-cons> := (<type> | "_" ) (("," (<stack-cons> | <stack-rest)) | <empty-stack>)+```++## PRINT++`PRINT` instructs Morley to print a comment during execution, optionally with+a reference into the stack. For example, `PRINT "hello"` will print `hello`.++Stack references may be written within the print-comment as `%[n]`, replacing+`n` with any natural number, which prints the `n`-th stack element from the+head.++For example, `PRINT "Head is: %[0]"` on `'[1, ...]` will print++```+Head is: int 1+```++## TEST_ASSERT++The `TEST_ASSERT` instruction allows us to declare an inline test assertion, which is+a labeled sequence of instructions that runs on a copy of the current stack.+That is, an assertion has no actual effect on the program but can return the+result of some computation on the stack.++For example, suppose we want to verify that the sum of two numbers is greater+than 10:++```+parameter unit;+storage unit;+code { DROP;+       PUSH int 2;+       PUSH int 10;+       TEST_ASSERT Test1 "%[0] + %[1] > 10" {ADD; PUSH int 10; COMPARE;LT;};+       DROP; UNIT; NIL operation; PAIR; };++```

@@ -0,0 +1,42 @@+<!--+SPDX-FileCopyrightText: 2020 Tocqueville Group++SPDX-License-Identifier: LicenseRef-MIT-TQ+-->++# Morley Language++The Morley Language is a low-level syntactic sugar over the core Michelson+instructions (core Michelson being the instructions which are actually executed+in the Tezos blockchain, as opposed to the various syntactic conveniences+provided by the OCaml reference client).++The general principle is that any syntactically valid core Michelson expression+will also be a valid Morley expression, i.e. Morley is a superset of+Michelson. Any language extensions that break this principle must be explicitly+enabled.++## Syntax Sugar++[See `morleySyntaxSugar.md`](./morleySyntaxSugar.md).++## Instruction and type names++In Michelson, all letters in all instructions must be CAPITAL and all letters in types and type constructors must be lowercase.+In Morley, one can also use lowercase letters in instructions.+For example, `ABS` and `abs` are both valid names of the same instruction.++Types and type constructors can start with a capital letter (like in Haskell).+For example, both `Unit` and `unit` are valid names of the unit type.++## Macros and Type synonyms++[See `morleyMacros.md`](./morleyMacros.md).++## Extended NOP Instructions++[See `morleyInstructions.md`](./morleyInstructions.md).++## Let-block Definitions++[See `morleyLet.md`](./morleyLet.md).

@@ -0,0 +1,168 @@+<!--+SPDX-FileCopyrightText: 2020 Tocqueville Group++SPDX-License-Identifier: LicenseRef-MIT-TQ+-->++# Let-block Definitions++In addition to the built-in macros defined in the Michelson specification,+Morley allows the programmer to define their own custom macros, as well as value+and type synonyms in a new top-level block:++```+let {+  type num = int;+  Three :: int = 3;+  add3 :: '[int] -> '[int] = {push int 3; add;};+  add3 :: '[int] -> '[int] = {push num Three; add;};+  add :: '[int, int] -> '[int] = {sub;};+  stkRest :: '[int, ...] -> '[int, ...] = {push int 3; ADD;};+};++parameter unit;+storage unit;+code { DROP;+       PUSH nat Three;+       drop;+       PUSH num Three;+       push Three;+       add;+       stacktype '[int, ...];+       stkRest;+       DROP;+       UNIT; NIL operation; PAIR; };+```++More formally:++```+let {<let>};++<let> := type <string> = type;+    | <string> :: <type> = <value>;+    | <string> :: <type-sig> = {op};+```++As a concrete example:++```+let {+  type num = int;+  Three :: int = 3;+  add3 :: '[int] -> '[int] = {push int 3; add;};+};+```++There are three distinct types of let:++- Type synonyms+- Constants+- Macros++## Constants++Constants may be pushed directly to the stack like so:++```+let {+  Three :: int = 3;+};+...+code {+  ...+  push Three;+  ...+  }+```++At present, constants are not checked statically, only when pushed.++## Type Synonyms++Type synonyms allow for labeling types. A synonym can be referred to anywhere a+type would be expected:++```+let {+  type num = int;+}+code {+  ...+  push num 3;+  ...+  }+```++This `push num 3` instruction pushes the value 3 with the type `int :num` onto+the stack.++Note that type synonyms with names `Parameter` and `Storage` are prohibited, these+names are used for implicit contracts parameter and storage types.++The interaction between type synonyms and type annotations is that if the+synonym's definition contains no annotation, the name of the synonym will be+used. If the synonym definition does contain a type annotation, the annotation+takes precedence and will be preserved:++```+type color = int;     ~> int :color+type color = int :rgb ~> int :rgb+```++## Let Macros++```+add3 :: '[int] -> '[int] = {push int 3; add;};+```++The first line of the macro declaration is the type signature, which denotes the+stack transformation the macro performs.++Crucially, if both input and output stack types contain a `<rest-of-stack>`+pattern match (syntactically `...]`), then the stack type captured by both+pattern matches must be identical.++For example, the type signature of++```+add3 :: '[int, ...] -> '[int, ...] = {push int 3; add;}+```++would be written using the type notation from the Michelson specification as:++```+add3 :: int : 'S -> int : 'S+```++meaning that the pattern match must be universally quantified over the same+stack-type `'S`.++Furthermore, type signatures can also have universally quantified type+parameters, which must be declared in a `forall`:++For instance, the type of the primitive `SWAP` instruction could be notated as:++```+swap :: forall a b. '[a, b, ...] -> '[b, a, ...]+```++It is important to note that type variables are not checked statically (at+present), but rather concretized in-place during type-checking. That is, the+typechecker replaces any unbound type parameter with the concrete type at that+position in the stack, and checks for consistency with any other instances of+that parameter.++## Non-recursive References++These definitions allow for non-recursive references to other definitions,+so one can define:++```+let {+  foo :: '[unit] -> '[unit, unit] = {unit;};+  bar :: '[unit] -> '[unit] = {foo; drop;};+};+```++A reference must always come after the let it refers to in the block.

@@ -0,0 +1,69 @@+<!--+SPDX-FileCopyrightText: 2020 Tocqueville Group++SPDX-License-Identifier: LicenseRef-MIT-TQ+-->++# Morley Language: Macros and Type synonyms++Morley language supports all macros from the OCaml reference implementation and additionally introduces some extra macros and type synonyms.++## A1 macros++First group of macros implemented in Morley consists of macros proposed in [A1 TZIP](https://gitlab.com/tzip/tzip/-/blob/c42e3f0f5e73669e84e615d69bee73281572eb0a/proposals/tzip-4/tzip-4.md).+In order to avoid duplication of documentation we don't copy it here, please refer to the A1 document for more information.++## Macros to work with tuples++Large tuples are desugared as right-balanced trees of `Pair`, thus working with them manually is inconvenient and produces fragile code.+The following macros can be used to work with tuples without caring about their actual Michelson representation.++### ACCESS++This macro retrieves an element of a tuple.+It accepts two arguments - 0-based index of desired element and overall tuple size.+For now `ACCESS` is just a macro, not a full-featured morley instruction, thus programmer has to specify tuple size explicitly.++Example:+```+push (int, bool, string, unit) (1, False, "", ());+access 1 4;+# Now stack contains `False` at the top+```++### SET++Modifies single element of a tuple.+This macro has signature similar to one of `ACCESS`, and accepts two stack arguments - original tuple and new value.++Example:+```+push (int, bool, string, unit) (1, False, "", ());+push bool True;+set 1 4;+# Now stack contains `(1, True, "", ())` at the top+```++### CONSTRUCT++Builds a tuple.+For each position of the tuple you provide a code block which builds an element for that position.++Example:+```+construct+  { push int 1 }+  { sender }+  { unit; some }+# Pushes `(1, <sender address>, some ())` on stack+```++Each code block has access to the stack at the moment of `construct` call and eventually have to push exactly one element to stack. This will also work:+```+push 5+construct+  { dup }+  { push int 3 }+  { dup; push int 3; add }+# Now stack is [(5, 3, 8), 5, ...]+```

@@ -0,0 +1,138 @@+<!--+SPDX-FileCopyrightText: 2020 Tocqueville Group++SPDX-License-Identifier: LicenseRef-MIT-TQ+-->++# Morley Language: Syntax Sugar++## Summary++| type   | Sugar                                   | Desugar                                   |+|--------|-----------------------------------------|-------------------------------------------|+| pair   | `(a ,b)`                                | `(pair a b)`                              |+| pair   | `(a, b) :t %f`                          | `(pair :t %f a b)`                        |+| pair   | `(a,b,c)`                               | `(a,(b,c))`                               |+| pair   | `(a, b, c) :t %f`                       | `(a, (b, c)) :t %f`                       |+| pair   | `(a :ta %fa, b :tb %fb, c :tc %fc)`     | `(a :ta %fa, (b :tb %fb, c :tc %fc))`     |+| or     | `(a \| b)`                              | `(or a b)`                                |+| or     | `(a \| b) :t %f`                        | `(or :t %f a b)`                          |+| or     | `(a \| b \| c)`                         | `(a \| (b \| c))`                         |+| or     | `(a \| b \| c) :t %f`                   | `(a \| (b \| c)) :t %f`                   |+| or     | `(a :ta %fa \| b :tb %fb \| c :tc %fc)` | `(a :ta %fa \| (b :tb %fb \| c :tc %fc))` |+| unit   | `()`                                    | `unit`                                    |+| lambda | `(\ a -> b)`                            | `lambda a b`                              |+| list   | `[a]`                                   | `list a`                                  |+| set    | `{a}`                                   | `set a`                                   |++++| Value | Sugar       | Desugar      |+|-------|-------------|--------------|+| Pair  | `(a, b)`    | `(Pair a b)` |+| Pair  | `(a, b, c)` | `(a,(b,c))`  |+| Unit  | `()`        | `Unit`       |++## Pairs++### Type Syntax+`pair` types may be written using Haskell-style tuples:++```+(a, b) ~ (pair a b)+(a, b) :t %f ~ (pair :t %f a b)+```++When tuples are nested, parenthesis may be omitted:++```+(a,b,c) ~ (a,(b,c))+```++Unsugaring will be performed in a way which provides the best average access time.+In essence, the tuple is split so that the left part has less by one+or the same size as the right part, these parts are recursively split+until one element remains, and resulting pieces are merged into an `Pair` tree.++For instance:++```+(a, b, c, d, e) ~ ((a, b), (c, (d, e)))+```++For nested tuples, only the outer pair may be annotated:++```+(a, b, c) :t %f ~ (a, (b, c)) :t %f+```++Inner types may be annotated as usual:++```+(a :ta %fa, b :tb %fb, c :tc %fc) ~ (a :ta %fa, (b :tb %fb, c :tc %fc))+```++### Value Syntax++`Pair` values may also be written with tuples:++```+(a, b) ~ (Pair a b)+(a, b, c) ~ (a,(b,c))+```++## Unions++### Type Syntax++`or` types may be written using the `|` character:++```+(or a b) ~ (a | b)+(or :t %f a b) ~ (a | b) :t %f+```++When bars are nested, parenthesis may be omitted:++```+(a | b | c) ~ (a | (b | c))+```++As for tuples, desugaring large unions produces right-balanced trees of `Or`s.++Annotations follow the same pattern as Tuples:+```+(a | b | c) :t %f ~ (a | (b | c)) :t %f+(a :ta %fa | b :tb %fb | c :tc %fc) ~ (a :ta %fa | (b :tb %fb | c :tc %fc))+```++## Unit++The `unit` type may be written as a `0`-tuple++```+unit ~ ()+```++The `Unit` value may also be written this way:++```+Unit ~ ()+```++## Lambda:++They `lambda` type may be written:++```+(lambda a b) ~ (\ a -> b)+```++## Containers++The `list` and `set` types may be written:++```+(list a) ~ [a]+(set a) ~ {a}+```

@@ -0,0 +1,43 @@+<!--+SPDX-FileCopyrightText: 2020 Tocqueville Group++SPDX-License-Identifier: LicenseRef-MIT-TQ+-->++# Michelson Types++We have two representations of types that assemble a Michelson contract: typed and untyped representations.+The former is located in the `Michelson.Typed` module hierarchy, the latter is in `Michelson.Untyped`.++## Untyped types++An untyped version of types is used to represent a contract after it is parsed.+It is capable of representing instructions and values with and without macros because it is parameterized by a type parameter for instructions.+This parameter can be an instruction with macros or without.++`U.Value` (a.k.a. [`Michelson.Untyped.Value`](/code/morley/src/Michelson/Untyped/Aliases.hs)) type is used to represent values as they are written in Michelson contracts.+It means that we don't have separate constructors for `address`, `key`, etc.+All these types are represented as strings.+The same applies to sets and lists, for example.++Untyped types are simple and easy to use, but they are not very powerful.+For instance, you can't statically ensure that all items in an untyped value storing a list have the same type.+Even if you check it, you will not be able to pass this guarantee to places where it matters thus still needing to handle impossible cases (via runtime errors).++## Typed types++A typed version of types is used to represent a contract after it is typechecked.+They actively use GHC extensions such as `GADTs` and `DataKinds`.+These types are more advanced than untyped types and are a bit harder to use.+However, they are much more powerful.++A typed Michelson value has type `T.Value t` (a.k.a. [`Michelson.Typed.Value`](/code/morley/src/Michelson/Typed/Aliases.hs)) where `t` has kind `T` and `T` represents one of the Michelson types.+It allows statically knowing the Michelson type of each value.+As a consequence, we can ensure that a typed list always contains values of the same type.++A typed Michelson instruction has type `Instr (inp :: [T]) (out :: [T])` where `inp` and `out` are lists of Michelson types.+`inp` is input stack type, `out` is output stack type.+It allows us to specify the type of each Michelson instruction directly in Haskell.+This representation makes interpreter implementation much easier and less error-prone.+For instance, if you encounter the `CHECK_SIGNATURE` instruction, you statically know that current stack contains values of types `key`, `signature`, and `bytes`.+You don't need to check types dynamically, you can't confuse their order.

@@ -0,0 +1,55 @@+<!--+SPDX-FileCopyrightText: 2020 Tocqueville Group++SPDX-License-Identifier: LicenseRef-MIT-TQ+-->++# Morley Interpreter++Morley interpreter takes a well-typed Morley contract (in [typed representation](./michelsonTypes.md#typed-types)), interprets all its instructions according to the Michelson specification and then performs side effects.+There can be the following side effects:+1. Update storage value of a contract.+2. Update balance of an address.+3. An operation returned by a contract (`operation` type from Michelson).++Morley interpreter is implemented in two layers:+* An interpreter for the core Michelson language which doesn't perform any side effects.+It means that it always interprets only one contract.+It's located in `Michelson.Interpret`.+* High-level Morley interpreter (we call it **executor**) that runs smart contracts using Michelson interpreter and _executes_ side effects.+It's located in `Morley.Runtime`.++## Michelson interpreter++Michelson interpreter simply implements the specification of the Michelson language.+It's implemented as a pure function which takes all necessary data as pure Haskell values stored inside a Haskell data type called `ContractEnv`.+This design allows the interpreter to work in any environment: it can work with real blockchain data, with data supplied by the user, with randomly generated data, etc.++## High-level executor++High-level executor works with [global blockchain state](./morleyRuntime.md#blockchain-state).+This executor has the following goals:+1. Execute operations returned by contracts.+An operation can originate a new contract or call another contract by sending a transaction to its address.+2. Perform other side effects: update storages of all the executed contracts and their balances.+3. Write an updated blockchain state on disk.++An end user can apply one of the following commands to run the executor.+* The `transfer` command sends a transaction from one address to another address.+If the destination address is a smart contract, its code will be executed.+Its storage will be updated, and it may return some operations which will also be executed.+The destination contract must be originated first.+* The `run` command originates a smart contract and transfers tokens to it.+By default, it doesn't update the global state.+It's intended to be used when one just wants to quickly interpret one contract and doesn't care about a global state file.+The command still needs to read the DB (JSON file) to know about all originated contracts and their parameters.+It's needed for the `CONTRACT` instruction.+Other environment data can be passed from CLI, but it's not mandatory, and default values are used if they are not passed explicitly.++Examples:+* `morley transfer --to KT1L39q6uCg1wQPB796q5oQQgDW673uo1s5y --parameter 'Left 10'` (`KT1L39q6uCg1wQPB796q5oQQgDW673uo1s5y` must be originated first).+* `morley run --contract foo.tz --parameter '"aaa"' --storage Unit` (in this case the contract will be originated automatically).++By default, each operation uses _genesis address_ as a sender.+This address initially has a lot of tokens.+We do not require signatures for transactions, anyone can spend tokens without any private keys because it's irrelevant to Michelson.

@@ -0,0 +1,49 @@+<!--+SPDX-FileCopyrightText: 2020 Tocqueville Group++SPDX-License-Identifier: LicenseRef-MIT-TQ+-->++# Morley Runtime++Morley runtime (`Michelson.Runtime*` modules) provides a high-level interface to Morley functionality.+It implements [high-level Morley executor](./morleyInterpreter.md#high-level-executor) and provides functions to read and parse a contract, originate it, transfer tokens, etc.++At present, Morley runtime doesn't communicate with any real Tezos network.+Instead, we emulate global blockchain state and store it on disk in a single JSON file.++## Blockchain State++A data type representing blockchain state is called `GState` (short for "Global State").+It stores a balance of each address, storage of each contract, and other data necessary to interpreter contracts.+Initially, the global state contains a number of addresses with a lot of tokens which we call _genesis addresses_.++We currently use a simple JSON format to encode and decode this data type.+This format should be considered internal and may be changed later.+You should use `morley` commands to update this state:+* `originate` command can be used to originate a contract.+This command reads a given contract, parses it, and typechecks it.+If the contract is well-typed, it's added to the global state, and its address is returned.+* `transfer` command can be used to change balances.+It sends a transaction from one address to another address.+It can also be used to update a storage value of a contract because a contract's code is executed when a transaction is sent to it.++Some data which is necessary to execute a contract and is not a part of a contract is not stored in `GState` but is passed via CLI:+* Gas limit is passed using the `--max-steps` option.+* Current timestamp (the result of the `NOW` instruction) is passed using the `--now` option.++Both options have default values.++For example, suppose you want to run a contract `a.tz` with the following blockchain state:+1. The contract `b.tz` should be originated, its balance should be 300, and its storage value should be `True`.+2. `a.tz` itself should have a balance of 500, and its storage should be 10.+3. The contract execution is allowed to consume at most 1000 gas.++In this case you should:+1. Run `morley originate --contract b.tz --storage True --balance 300` to originate `b.tz`. It should print the address of `b.tz`.+2. Run `morley originate --contract a.tz --storage 10 --balance 500` to originate `a.tz`. It should print the address of `a.tz`.+3. Run `morley transfer --parameter 10 --to KT1L39q6uCg1wQPB796q5oQQgDW673uo1s5y --max-steps 1000`, assuming `KT1L39q6uCg1wQPB796q5oQQgDW673uo1s5y` is the address of `a.tz`. It will actually execute `a.tz`. By default, the `transfer` command transfers 0 tokens. You can use the `--amount` option to specify a non-zero amount. It will be returned by the `AMOUNT` instruction. By default, tokens are sent from a genesis address which has a lot of money initially.++If later you want to transfer 10 tokens from `KT1L39q6uCg1wQPB796q5oQQgDW673uo1s5y` to `tz1faswCTDciRzE4oJ9jn2Vm2dvjeyA9fUzU` (just an arbitrary `tz1` address), you can use the `transfer` command again: `morley transfer --parameter Unit --to tz1faswCTDciRzE4oJ9jn2Vm2dvjeyA9fUzU --sender KT1L39q6uCg1wQPB796q5oQQgDW673uo1s5y --amount 10`. Notice that we pass `Unit` as a parameter because the destination address is the `tz1` address, it doesn't have any code.++It also should be noted that currently we ignore transaction fees (they are always 0).

@@ -0,0 +1,31 @@+<!--+SPDX-FileCopyrightText: 2020 Tocqueville Group++SPDX-License-Identifier: LicenseRef-MIT-TQ+-->++# Morley Typechecker++In Morley, we have a typechecker for the core Michelson language, i. e. without macros.+It is located in `Michelson.TypeCheck` and designed in the following way:+* It takes a core Michelson contract extended with `EXT` instruction to support additional instructions described in the [`morleyInstructions.md`](language/morleyInstructions.md) document.+* The contract passed to the typechecker uses [untyped representation](./michelsonTypes.md).+* During typechecking, we verify that instructions are well-typed and provide evidence to the compiler that allows us to convert instructions into [typed representation](./michelsonTypes.md). If the contract is ill-typed, the typechecking process fails with an error.+* The typechecker can check a whole contract or a standalone value (for example, a lambda).+In the former case it needs to know the parameter type of the contract (to check `SELF`).++## CLI++End users can use the `typecheck` command to execute the typechecker.+It parses the contract, performs macro expansion, and passes it to the typechecker which says that the contract is well-typed or produces an error message.++Example: `morley typecheck --contract auction.tz`.++## Internals++An internal structure of the typechecker is pretty well described in Haddock comments.+Two main modules are:+* [`Michelson.TypeCheck.Value`](/code/morley/src/Michelson/TypeCheck/Value.hs) contains logic for checking Michelson values.+* [`Michelson.TypeCheck.Instr`](/code/morley/src/Michelson/TypeCheck/Instr.hs) contains logic for checking Michelson instructions and the whole contract.++Their functionality is re-exported from the [`Michelson.TypeCheck`](/code/morley/src/Michelson/TypeCheck.hs) module along with some auxiliary types and functions.

@@ -1,13 +1,11 @@ cabal-version: 2.2 --- This file has been generated from package.yaml by hpack version 0.33.0.+-- This file has been generated from package.yaml by hpack version 0.34.2. -- -- see: https://github.com/sol/hpack------ hash: eb134e14a2fe104820cbd6241dea8a67f3cd12bdc52681163d54531e450bf30c  name:           morley-version:        1.7.0+version:        1.7.1 synopsis:       Developer tools for the Michelson Language description:    A library to make writing smart contracts in Michelson — the smart contract language of the Tezos blockchain — pleasant and effective. category:       Language@@ -22,6 +20,16 @@ extra-source-files:     CHANGES.md     README.md+extra-doc-files:+    docs/michelsonTypes.md+    docs/morleyInterpreter.md+    docs/morleyRuntime.md+    docs/morleyTypechecker.md+    docs/language/morleyInstructions.md+    docs/language/morleyLanguage.md+    docs/language/morleyLet.md+    docs/language/morleyMacros.md+    docs/language/morleySyntaxSugar.md  source-repository head   type: git

@@ -45,22 +45,25 @@ -- passed to other instructions. -- -- The instruction MUST be linearized to the left (see 'linearizeLeft').+--+-- *IMPORTANT* be careful if you want to rewrite this function.+-- It took GHC about 30 seconds to compile this function previously.+-- The clause @isTypicalPreFailWith (Seq x PAIR) = ..@ is crucial, so please+-- don't move these two case branches in this clause outside of it:+-- either in different patten matching or in case or \case clause,+-- I usually experienced a regression for any of these options. isTypicalFailWith :: Instr inp out -> Maybe TypicalFailWith-isTypicalFailWith = \case-  Seq i1 FAILWITH -> isTypicalPreFailWith i1-  _ -> Nothing+isTypicalFailWith (Seq i1 FAILWITH) = isTypicalPreFailWith i1   where-    isTypicalPreFailWith ::-      Instr inp (a ': out) -> Maybe TypicalFailWith-    isTypicalPreFailWith =-      \case-        PUSH v -> isTypicalErrorConstant v-        Seq _ (PUSH v) -> isTypicalErrorConstant v--        Seq (PUSH v) PAIR -> FailWithStackValue <$> isStringValue v-        Seq (Seq _ (PUSH v)) PAIR -> FailWithStackValue <$> isStringValue v--        _ -> Nothing+    isTypicalPreFailWith :: Instr inp (a ': out) -> Maybe TypicalFailWith+    isTypicalPreFailWith (Seq x PAIR) = case x of+      Seq _ (PUSH v) -> FailWithStackValue <$> isStringValue v+      PUSH v         -> FailWithStackValue <$> isStringValue v+      _              -> Nothing+    isTypicalPreFailWith (Seq _ (PUSH v)) = isTypicalErrorConstant v+    isTypicalPreFailWith (PUSH v) = isTypicalErrorConstant v+    isTypicalPreFailWith _ = Nothing+isTypicalFailWith _ = Nothing  isTypicalErrorConstant ::   forall t. ConstantScope t => Value t -> Maybe TypicalFailWith

@@ -396,11 +396,6 @@   where     tcErrToFail err = fail $ "Type check failed: " +| err |+ ""     tcInitEnv =-      -- In Tezos @UNPACK@ instruction does not depend on environment.-      ---      -- We initialize each of the fields as 'error' (rather than just defining-      -- the whole datatype as 'error') to make source of error more obvious-      -- if access to one of these fields is performed after all.       TypeCheckEnv       { tcExtFrames = error "runInstrImpl(UNPACK): tcExtFrames touched"         --- ^ This is safe because @UNPACK@ never produces Ext instructions

@@ -270,17 +270,19 @@   -> TxData   -> "verbose" :! Bool   -> "dryRun" :! Bool-  -> IO ()+  -> IO U.Value runContract maybeNow maxSteps initBalance dbPath uStorage uContract txData   verbose (arg #dryRun -> dryRun) = do   origination <- either throwM pure $     mkOrigination <$> typeCheckContractAndStorage uContract uStorage-  void $ runExecutorMWithDB maybeNow dbPath (RemainingSteps maxSteps) verbose ! #dryRun dryRun $ do+  (_, newSt) <- runExecutorMWithDB maybeNow dbPath (RemainingSteps maxSteps) verbose ! #dryRun dryRun $ do     -- Here we are safe to bypass executeGlobalOperations for origination,     -- since origination can't generate more operations.     addr <- executeGlobalOrigination origination     let transferOp = TransferOp addr txData     executeGlobalOperations [transferOp]+    getContractStorage addr+  return newSt   where     -- We hardcode some random key hash here as delegate to make sure that:     -- 1. Contract's address won't clash with already originated one (because@@ -297,6 +299,14 @@       , ooStorage = storage       , ooContract = contract       }++    getContractStorage :: Address -> ExecutorM U.Value+    getContractStorage addr = do+      addrs <- use (esGState . gsAddressesL)+      case addrs ^. at addr of+        Nothing -> error $ pretty addr <> " is unknown"+        Just (ASSimple {}) -> error $ pretty addr <> " is a simple address"+        Just (ASContract (ContractState{..})) -> return $ untypeValue csStorage  -- | Send a transaction to given address with given parameters. transfer ::

@@ -186,33 +186,9 @@   RfAlwaysFails i -> RfAlwaysFails $ f i  getComparableProofS :: Sing (a :: T) -> Maybe (Dict (Comparable a))-getComparableProofS s = case s of-  STPair a b -> do-    Dict <- getComparableProofS a-    Dict <- getComparableProofS b-    pure Dict-  STInt -> Just Dict-  STNat -> Just Dict-  STString -> Just Dict-  STBytes -> Just Dict-  STMutez -> Just Dict-  STBool -> Just Dict-  STKeyHash -> Just Dict-  STTimestamp -> Just Dict-  STAddress -> Just Dict-  STKey -> Nothing-  STUnit -> Nothing-  STSignature -> Nothing-  STChainId -> Nothing-  STOption{} -> Nothing-  STList{} -> Nothing-  STSet{} -> Nothing-  STOperation -> Nothing-  STContract{} -> Nothing-  STOr{} -> Nothing-  STLambda{} -> Nothing-  STMap{} -> Nothing-  STBigMap{} -> Nothing+getComparableProofS s = case checkComparability s of+  CanBeCompared -> Just Dict+  CannotBeCompared -> Nothing  -- | Constraint which ensures that type is comparable. type family IsComparable (t :: T) :: Bool where

@@ -16,6 +16,7 @@ import qualified Data.Aeson.Types as Aeson import Data.Bits (Bits) import Data.Typeable (typeRep)+import Fmt (Buildable(..)) import qualified Text.Show as T  parseAsString :: forall a. (Read a, Typeable a) => Aeson.Value -> Aeson.Parser a@@ -42,6 +43,9 @@  instance FromJSON TezosInt64 where   parseJSON = parseStringEncodedIntegral++instance Buildable TezosInt64 where+  build = show  instance ToJSON TezosInt64 where   toJSON (StringEncode x) = Aeson.String $ show x

@@ -28,19 +28,19 @@   ) where  import Crypto.Error (CryptoError)-import Crypto.Number.Serialize (i2ospOf_, os2ip) import Crypto.Number.ModArithmetic (squareRoot)-import Crypto.Random (ChaChaDRG, MonadPseudoRandom, drgNewSeed, seedFromInteger, withDRG)+import Crypto.Number.Serialize (i2ospOf_, os2ip) import qualified Crypto.PubKey.ECC.ECDSA as ECDSA import qualified Crypto.PubKey.ECC.Generate as ECC.Generate import Crypto.PubKey.ECC.Types   (Curve(..), CurveCommon(..), CurvePrime(..), Point(..), curveSizeBits)+import Crypto.Random (ChaChaDRG, MonadPseudoRandom, drgNewSeed, seedFromInteger, withDRG) import qualified Data.Binary.Get as Get import qualified Data.ByteArray as BA import qualified Data.ByteString as BS import qualified Data.ByteString.Base58 as Base58 import qualified Data.ByteString.Lazy as LBS-import Fmt (Buildable, Builder, (+|), (|+), build, fmt, hexF)+import Fmt (Buildable, Builder, build, fmt, hexF, (+|), (|+))  import Tezos.Crypto.Hash import Util.Binary (getRemainingByteStringCopy)@@ -178,7 +178,7 @@       beta <- squareRoot p alpha                 & maybeToRight (CryptoParseBinaryError "Could not find square root.")       let (evenBeta, oddBeta) =-            if (beta `mod` 2 == 0) then+            if even beta then               (beta, p - beta)             else               (p - beta, beta)