The Haskell package plutus-core
implements a range of functionality for manipulating Plutus Core programs. The implementation is based on the Plutus Core language specification.
-
Parser and pretty-printer for textual Plutus Core representation as per the Plutus Core specification
-
Binary serialisation and deserialisation using the
cborg
package (coordinate with Duncan) -
Plutus Core abstract syntax
-
Renamer
-
Type checker
-
Evaluator (interpreter based on the CK machine) that closely follows the Plutus Core specification (the aim is to obviously match the specification without much concern for efficiency)
-
Testsuite based on the
hedgehog
andtasty
packages -
Round trip testing of parser with pretty-printer and serialisation with deserialisation using
hedgehog
-
Golden tests against sample PLC programs
-
Comprehensive documentation of all non-trivial functions and types
-
API documentation with Haddock
The lexer & parser are based on Alex & Happy and the pretty printer uses the prettyprinter
package. Names (identifiers) are interned using uniques as per Language.PlutusCore.Name
. They are also parameterised with an attribute used differently in different stages.
Parsing, pretty-printing and the AST representation closely follow the Plutus Core specification. AST nodes are parametereised with the same attribute as the embedded names.
NB: At this stage, every occurrences of a particular name (identifier lexeme) receives the same unique. Hence, binders can be shadowed according to the scoping rules of Plutus Core.
The renamer performs scope resolution and replaces all usage occurrences of identifiers with their definition. In the case of Plutus Core, identifiers are either term or type variables whose definition assigns a type or kind, respectively. In other words, we can regard the renamer phase as the propagation of kind and type information from the site of the declaration of a term or type variable to all usages positions of those variables.
Moreover, renaming ensures that programs meet the global uniqueness property: every unique in a program is only bound exactly once. Hence, there is no shadowing or reusing of names in disjoint scopes anymore after this phase.
If program transformations are performed on renamed programs (such as substitution on subterms with free variables), the global uniqueness property may no longer hold. It is recommended to simply perform all necessary transformations without expecting or reinstating the global uniqueness property in between individual transformation steps. When the final form of the program has been reached (or when a program needs to be type checked), an additional use of the renamer can reinstate the global unqiueness property again.
NB: Whenever the global uniqueness property is not a given, care needs be taken to correctly handle binders. For example, when implementing substitution, we need to ensure that we do not propagate a substitution below a binder matching the susbtituted variable and we need to avoid variable capture (as per standard treatments of names in lambda calculi).
The type checker synthesises the kind of a given type and the type of a given term. This does not involve any form of inference as Plutus Core is already fully typed. It merely checks the consistency of all variable declarations and the well-formedness of types and terms, while deriving the kind or type of the given type or term.
NB: The type checker requires terms to meet the global unqiueness property. If this is not a given, use a renamer pass to suitably pre-process the term in question.
You can install the executables described below via either stack
or nix
.
Run nix build -f default.nix haskell.projectPackages.plutus-core.components.exes.plc
being in the plutus
folder. Once the build finishes, copy the executables from the result/bin
folder to somewhere in $PATH.
Run stack install plutus-core
in your terminal being in any subfolder of plutus
. Once the build finishes, you'll be shown the following lines:
Copied executables to ~/.local/bin:
- plutus-core-generate-evaluation-test
- plc
The CK machine can be used to evaluate programs. For this, feed a type checked
Plutus Core term to the unsafeEvaluateCk
function defined in the
Language.PlutusCore.Evaluation.Machine.Ck
module (the DynamicBuiltinNameMeanings
argument contains information about
extra built-in functions and can safely be set to Data.Map.empty
for simple
programs):
unsafeEvaluateCk
:: DynamicBuiltinNameMeanings (CkValue uni)
-> Term TyName Name uni () -> EvaluationResult (Term TyName Name uni ())
It returns an EvaluationResult
which is either a succesfully computed Term
or a failure:
data EvaluationResult a
= EvaluationSuccess a
| EvaluationFailure
It can also raise an exception, as indicated by unsafe
in the name, but this should not happen for well-formed programs.
There is an executable that runs programs on the CK machine: you can feed a program to plc evaluate
, the program will be run and the result will be printed.
An example of usage:
echo "(program 0.1.0 [(lam x (con integer) x) (con integer 271)])" | plc evaluate --stdin -mCK
A term generation machinery sits in the Language.PlutusCore.Generators.Internal.Entity
module. It allows to generate terms that contain built-ins (integers, bytestrings, sizes and booleans), constant applications and first-order functions.
The generator makes sure a term is well-typed and keeps track of what it's supposed to evaluate to.
There is an executable that prints a term and the expected result of evaluation. Run it as plutus-core-generate-evaluation-test
, and you'll be shown two terms separated by a newline.
(program 0.1.0 [ (lam x0 (con bool) [ [ (builtin dropByteString) [ [ (builtin multiplyInteger) [ [ (builtin addInteger) (con integer 3) ] (con integer 3) ] ] [ [ (builtin multiplyInteger) (con integer 2) ] (con integer 1) ] ] ] [ (builtin sha3_256) [ [ (builtin takeByteString) (con integer 2) ] (con bytestring #7661) ] ] ] ) [ [ (builtin greaterThanInteger) [ [ (builtin multiplyInteger) [ [ (builtin multiplyInteger) (con integer 2) ] (con integer 0) ] ] [ [ (builtin subtractInteger) (con integer 3) ] (con integer 3) ] ] ] [ [ (builtin addInteger) [ [ (builtin multiplyInteger) (con integer 1) ] (con integer 1) ] ] [ [ (builtin addInteger) (con integer 1) ] (con integer 1) ] ] ] ] )
(con bytestring #4b6e4ba90e78b6601bc63c806d34f914b983acc3)
where the first line is a program, the second line is empty and the third line is the result of evaluation of the program (in this case, the Plutus Core representation of a bytestring). Output is always structured this way: three lines with the second one being empty.