No description, website, or topics provided.
Switch branches/tags
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
ext
lib
t
.gitignore
.gitmodules
LICENSE
README.md
build
plutus-core.md
sum-to-10-spec.k
typing-tests.md
typing.md
unit-tests.md
verification.md

README.md

In this repository we implement the Plutus Core specification defined here. The IOHK Plutus implementation is here. At the moment we target version v1.0 (RC5.5).

Installation

After installing python3, pandoc and ninja-build as dependencies and placing them in $PATH, simply run ./build to setup OCaml, K, compile the semantics and run the tests. TODO: All reachability-based tests (unit-tests etc) are not run against the lazy semantics yet (though they should pass).

The file plutus-core.md defines the Plutus Core language, and the file plutus-core-spec.md defines unit tests as a reachability specification.

Errors / Questions from specification / reference implementation

Reference implementation

Specification

  • Type of integers/bytestrings in syntax does not match with Figure 13.

  • Type synthesis (Fig. 5), inst rule - should S be A?

  • What is floor syntax?

  • (fix ...) as a term construct is still present. See pgs 12, 13, 15.

  • What does V refer to in the second to last case in Figure 12?

  • In syntax, (Fig. 2), lambdas and other constructs take in Type Values, but in the semantics (Fig. 9), they take in any Type

    Fixed: Commit that fixes this.

  • Underspecified grammar, for example [ Term TermList ] doesn't parse.

    Grammar follows what internal AST representation is

  • (fix ...) rule changes type (Fig. 9)

    Deprecated, (fix ...) is no longer a term-level construct.

  • resizeInteger and intToByteString: arguments say i has size s1, should it be s0?

    Fixed: Commit that fixes this.

  • intToByteString: Behaviour for negative integers is not specified. Which binary representation should we use?

    Two’s complement. Not yet added to spec.