intersectmbo / plutus

The Plutus language implementation and tools

Plutus Core

Table of Contents

• Introduction
• Development
  • How to develop and contribute to the project
  • How to submit an issue
  • How to depend on the project from another Haskell project
• Documentation
  • User documentation
  • Talks
  • Specifications and design
  • Academic papers
• Licensing

Introduction

Plutus Core is the scripting language embedded in the Cardano ledger and forms the basis of the Plutus Platform, an application development platform for developing distributed applications using the Cardano blockchain.

For more information about the projects, see the User documentation.

This repository contains:

• The implementation, specification, and mechanized metatheory of Plutus Core

• Plutus Tx, the compiler from Haskell to Plutus Core.

For people who want to use the project, please consult the User documentation.

Development

How to develop and contribute to the project

Run nix develop to enter the development shell and you will be presented with a list of available commands.

*Please see CONTRIBUTING for comprehensive documentation on how to contribute to the project, including development and submitting changes

How to submit an issue

Issues can be filed in the GitHub Issue tracker.

How to depend on the project from another Haskell project

The plutus libraries are published via CHaP. See the information there for how to use CHaP. After setting it up you should just be able to depend on the plutus packages as normal and cabal will find them.

Documentation

User documentation

The main documentation is located here.

The latest documentation for the metatheory can be found here.

Talks

• Functional Smart Contracts on Cardano (2020): an overview of the ideas behind the Plutus Platform.

• The Plutus Platform (2020): an overview of the Platform as a whole (including the Application Framework) at the time.

Specifications and design

• Plutus Technical Report (draft): a technical report and design document for the project.

• Plutus Core Specification: the formal specification of the core language.

• Extended UTXO Model: a design document for the core changes to the Cardano ledger.

Academic papers

• Unraveling Recursion: a description of some of the compilation strategies used in Plutus IR (published version).

• System F in Agda: a formal model of System F in Agda (published version).

• The Extended UTXO Model: a full presentation of the EUTXO ledger extension (published version).

• UTXOma: UTXO with Multi-Asset Support: a full presentation of the multi-asset ledger extension (published version).

• Native Custom Tokens in the Extended UTXO Model: a discussion of the interaction of the multi-asset support with EUTXO (published version).

• Translation Certification for Smart Contracts: a certifier of Plutus IR compiler passes written in Coq.

Licensing

You are free to copy, modify, and distribute this software under the terms of the Apache 2.0 license.

See the LICENSE and NOTICE files for details.

plutus's Issues

Bazelify plutus

This is a proof of concept for working with bazel in IOHK.

Contract ownership

This problem is related to the validating the next data script problem in that I came across it when attempting to implement solution (3) described there.

Problem

Suppose we have a contract with two participants, A and B. Some of the actions supported by the contract only affect one of the participants' stake in the contract. For example, in the interest rate swap either participant is able to increase their margin/deposit or transfer ownership of their stake in the contract to a third party. It should be possible to do this without involving the other participant (because that would give them a effectively a veto). At the same time, if there is an action that affects both parts of the contract then either participant should be able to perform that action regardless of any changes that have been made to the other part.

We want to avoid a requirement for B to know the most recent value of the state of A's part of the contract, because the only way that could be achieved is through de-serialisation of the data script (which we don't support at the moment) or by asking A to communicate the state through an external channel to B (which brings up trust and usability issues). We would like to get by with treating A's state as a binary blob that we don't need to touch.

Proposed solution

How can we implement this in the state machine?

At this point we shall introduce some terminology. We will say "role" to mean a part of the contract (the right to perform some actions on that contract) and "actor" to mean the individual, identified by a public key, who currently has that role. The roles of a contract stay the same, and are known before the contract begins, while the actors may change.

The first idea is to spread the contract across several addresses, namely one for each role. In the swap example, we have two roles, Floating and Fixed. An action that affects only one role is "transfer ownership", and an action that affects both role is "make payment". So we get the types Role = Floating | Fixed and Action = TransferOwnership PubKey | MakePayment OracleValue. We can then parameterise the validator script with the Role value, resulting in two distinct hashes for what is otherwise the same script. The validator script (still a state machine) now checks if the input it receives affects both roles, or just one of them. In case of TransferOwnership we can verify that no outputs from the other role's address are consumed, and in case of MakePayment we check that outputs at both addresses are spent and produced.

In this diagram, the circles are transaction inputs/outputs and the rectangles are transactions. Each horizontal lane corresponds to one of the two addresses of the contract. t1 and t3 are TransferOwnership actions and t2 and t4 are MakePayments.

Transaction t2 is submitted by the Floating actor. Let's look at its inputs and outputs. A and B are the data scripts of the inputs it consumes, and A' and B' are the data scripts of its outputs. If t2 changes the states of the Fixed and Floating roles, then A' != A and B' != B. However, when the Fixed actor wants to create t3 then they need to know B'. So we are back to where we started.

One potential solution is to split up the roles even further, into an "internal" and an "external" address. The script at the internal address records the role's current actor, and the script at the external address contains the rest of the role's state. Whenever we modify the state, we look at the value at the role's internal state to make sure that the transaction is legitimate.

In this diagram I used coloured squares to indicate the actor that submits a transaction. At the beginning, Orange is the Fixed actor and Green is the Floating actor. In t1, Orange transfers their role to Yellow. In t2, Green performs the MakePayment action. This transaction consumes outputs from all four addresses. The internal data scripts stay the same, so A=E and C=G.

This is what I am implementing right now. The tricky part is that the validator script needs to consider four cases for each possible input (namely, Fixed-Internal, Fixed-External, Floating-Internal, Floating-External). Also I'm not entirely sure yet if we can prevent Green from tampering with the contract by producing their own version of "A" to the Fixed-Internal address. But I think that can be solved in the validator script.

Spec: CK halting state

I added an extra state (a big square) to the CK machine in the spec so that the machine can say that it's finished, and what the final result is. This happens when the stack is empty: I just added it to make it obvious to the reader when the machine is finished. We can take this back out, but we should still say somewhere that an empty stack means that the machine halts. I don't think this was mentioned explicitly before.

Extended UTxO: is DataScript a part of TxOut?

It's currently unclear from Extended UTxO if Data Script is a part of TxOut or not.
If Data Script is a part of TxOut this implies:

1. Data Script content is now a part of a transaction, its hash, hence its TxHash aka TxId.
   This means that Data Script can't hold any data that is dependent on its transaction data, for example signatures of its TxHash.
2. Data Script won't be a segregated witness, and thus can't be ever removed.

Either way it should be clarified in the documentation.

Add serialization builtin to Plutus

Add serialization builtin to Plutus, i.e.

serialize :: a -> ByteString

Error line highlighting in the editor is incorrect.

When you have a compiler error, the red X that appears in the editor is on the wrong line.

Partly this is the backend, but @shmish111 has fixed that and reports that the frontend is still off by one.

Playground warmup is very slow

We are being affected by haskell-hint/hint#56 so I will look into:

1. Will GHC 8.6 fix this?
2. Will using GHCI rather than hint fix this

Performance of abstract machines

This issue is for discussions about performance of evaluation of Plutus Core programs.

@kwxm has done a great job at figuring out efficiency weak spots of our evaluators. What is not fixed right now is generation of booleans which slows down things a lot. There is a PR (#268) that fixes this, but we probably can do something better (quoting the PR's thread):

there is another thing to test: whether having booleans as CAFs (i.e. no Quote at all while evaluating things) gives a speedup or no. Quote is rather deeply incorporated into evaluation and we can't just remove it, because many things that use the same constant application machinery, that the machines use, do require unique names, but I think we can do some parameterization here.

Clarification on the NEO blockchain

The research reviews/overviews of other systems I find in the notes here are a bit off at times. For what it's worth, I thought I point things out regarding the NEO protocol:
The blockchain is running its mainnet version for two years now (not just testnet, however decentralization didn't take place yet either) and you don't necessarily need Visual Studio to generate code. E.g. the community provided a compiler from Python code to those bytecode files that you can upload to the chain (https://github.com/CityOfZion). Given that it has its own VM and isn't running e.g. JVM directly, the file I saw here outlining which chains have support for floats is also wrong - it doens't support it in any straightforward way.

Hope that helps and keep up the good work (dependent types shill here ;)

Compressability of Plutus Core

Code size has come up a few times as a potential issue for core nodes. An obvious way to mitigate this is good compressability of Plutus Core, both within a program and ideally across programs (if you are compressing the data for a series of transactions).

Compression algorithms love identical subequences, and at the moment we make things unnecessarily hard for them, at least two reasons:

• Actually identical terms won't have the same serialization, because their variables are identified by uniques, and so their serialization is affected by where they appear in the enclosing program.
  • The only good solution I can think of for this would be to switch to de Bruijn indices instead of uniques.
  • We could potentially do this just for serialization if we wanted. Being parametric over the types of names helps us!
  • This would also help with our current issue about debug printing in tests: we want to see distinct variables as distinct, but the particular uniques keep changing! Not a problem with de Bruijn indices.
• Terms that are identical up to variable names won't have the same serialization, because we serialize variable names (and annotations, but they're always unit, so that's okay).
  • This is easy to solve: just have a serialization mode that discards names, or run a pass over the program to discard them before serializing.

Playground releases

There are at least two external tutorials for PlutusTx now, and some of the code in those tutorials will stop working soon due to changes such as #474 (renaming PendingTx' to PendingTx).

The API is not finalised yet and further changes are unavoidable. To prevent a situation where a lot of the documentation is outdated before Plutus is even available on the blockchain we should

• Show the current version in the Playground (commit ref + date would be enough)
• Record all changes in the changelog
• Link from Playground to the deployed version on Github

Builtins

We have several kinds of builtins:

1. Static builtin names like addInteger, takeByteString, BlockNum, etc. Right now each of them has its Haskell interpretation except intToByteString, VerifySignature, TxHash and BlockNum. This document provides some information on how we compute static builtins application in a well-typed way. In the implementation static builtin names are not saturated, while in the specification they are saturated, so this is something that needs to be fixed.

2. Dynamic builtin names like charToString and trace. Those are functions that we can extend the language with, but that are not provided by default. Dynamic builtin names are handled analogously to static builtin names, it's just that for a static builtin name we know its TypeScheme (see the doc reference above) and interpretation statically, but for a dynamic builtin name we require the user (where "the user" = "someone who invokes the type checking procedure or one of the abstract machines") to provide them. This means that we only do some look-ups in maps storing types or interpretations of dynamic builtin names during type checking and evaluation, i.e. dynamic builtin names are not harder than static builtin names, just a little bit of boilerplate.

3. Dynamic builtin types. There are two possible forms of them: a complicated one and a very complicated one. Right now the former is implemented, but we really want the latter. The complicated form is described in Language.PlutusCore.Constant.Typed in Note [Semantics of dynamic built-in types]. The most important part is

We only allow dynamic built-in types that can be represented using static types in PLC. For example Haskell's 'Char' can be represented as integer 4 in PLC. This restriction makes the dynamic built-in types machinery somewhat similar to type aliases in Haskell (defined via the type keyword).

You might think this is a minor thing, however together with dynamic builtin names this gives us some great potential and a lot of complexity. For example, we already can convert Plutus Core values to Haskell values using some terrible hacks:

we evaluate terms using some evaluator (normally, the CEK machine). For the temporary lack of ability to put values of arbitrary Haskell types into the Plutus Core AST, we convert PLC values to Haskell values and "emit" the latter via a combination of unsafePerformIO and IORef. For example, we fold a PLC list with a dynamic built-in name (called emit) that calls unsafePerformIO over a Haskell function that appends an element to the list stored in an IORef:

    plcListToHaskellList list =
        evaluateCek anEnvironment (foldList {dyn} {unit} (\(r : unit) -> emit) unitval list)

After evaluation finishes, we read a Haskell list from the IORef (which requires another unsafePerformIO) and return it.

This all is elaborated in Language.PlutusCore.Constant.Typed.

However, we of course want to remove this unsafePerformIO nonsense which means we need to be able to somehow put values of arbitrary Haskell types into the Plutus Core AST. Having this ability we can simply fold over a PLC data type inside PLC (using the CEK machine or any other evaluators that knows how to handle dynamic builtin names), but collect a Haskell value in an accumulator. And then the result of evaluation of a fold over a PLC data type is a very shallow wrapper around a Haskell value which we can then easily extract. And it should be possible to construct such fold in generic way, i.e. derive them from the Generic instance of a Haskell data type.

Of course, embedding the entire Haskell into Plutus Core is not a trivial thing. I have some ideas, but I do not really know whether they make sense or not.

Meanwhile, @j-mueller, right now we can convert PLC lists to Haskell lists (and hence lists of lists, lists of lists of lists, etc). I think, I can add support for sum and product types (without unsafePerformIO nonsense). This does not allow to convert an arbitrary PLC to value to a Haskell value, but maybe it's enough to unblock you at least?

Oh, and please someone suggest better names for these things.

Merkelized abstract syntax trees

This is something we may want to consider to reduce, e.g., data transmission costs. (See also Simplicity.)

Plutus Core Specification

This ZenHub epic tracks all work on the PLC specification document(s).

Better publishing of our project Haddocks

At the moment there's a manually generated dump of some of the Haddock on our GH pages, but this is very ad hoc.

It would be better to generate a nice, combined Haddock bundle for all of our packages, and do so on the CI so we can always be pointing to an automatically generated, up to date version.

However, this is a bit annoying, since the Haddocks generated with Nix have links pointing at dependent packages in the store, so it'll be hard to stitch them together so the links point at each other instead.

cabal new-haddock seems promising for this, but I was unable to get it to work:

• It requires cabal new-build to work for starters
• It requires network access (offline mode is broken)

Might be able to do this ourselves with a bit of creativity.

Improve wallet API tutorial

• Get rid of the MockWallet type
• Link to haddocks
• Add explanation of extended UTxO somewhere

As well as these review comments:

• Re-export operators from Num Int and Ord Int in Plutus prelude
• Explain language pragmas and imports, are they necessary in every contract?
• Code blocks should be max. 80 characters wide
• "You need to explain that the general form is: Redeemer -> DataScript -> PendingTx -> Answer and that the Answer is always ignored, so might as well be ()"
• "so we need to import the ones that we want to use from the Validation module" You need to explain that the operators must come from Validation, not from the Haskell prelude, because only those operations are available for online code.
• Explain unused slots in match on PendingTx ins outs _ _ (Slot currentSlot) _
• Try to avoid matching on Slot, Value types to get their Ints
• "that is, to the current date" A slot number is not a date!
• "using Validation.foldr on the list of inputs ins" Is there a limit to the number of inputs of a transaction? What happens if the number of contributions exceeds this limit?
• Validation.foldr The program text refers to P.foldr.
• let v (PendingTxIn _ _ (Value vl)) = vl Explain in the text the purpose of v.
• ($$(P.error) ()) Perhaps explain why P.error is applied to the unit value.
• Collect option should be defined before Refund in validator script
• Avoid using $ in sample code & tutorial
• payToScript_ Why is there an underbar at the end of the name?
• W.ownSignature Doesn't this require as an argument the thing to be signed?
• At the beginning of the section, you said we needed three endpoints. But the section on endpoints is ending now, and you still haven't given the refund endpoint. Promise the reader that it is coming later. Or rewrite, to first explain all the collection endpoints and then explain all the triggers.
• "The wallet API allows us to specify EventTriggers with handlers to implement this." Rewrite to avoid "EventTriggers", use just "EventTrigger" instead. And the reader may not know what "this" refers to. Replace "to implement this" by "to automatically run collect".
• "GEQ" You need to explain this argument, and the other possible arguments; also give a pointer to where in the documentation they are described.
• "Interval" Explain Interval and the other possible alternatives for this argument. Is y in Interal x z when x <= y and y <= z (inclusive) or x < y and y < z (exclusive), or something else?
• "The handler is function" --> "The handler is a function"
• "Anything that happens in an EventHandleris a normal interaction with the blockchain facilitated by the wallet, so it is still our responsibility to submit valid transactions." Isn't this obvious? I don't see why this sentence is here. Is there a possible misconception you are trying to avoid? What is it?
• "so we could use collectFromScript to implement it" --> "so one might think we could use collectFromScript to implement it" (This text reads oddly to me. Just omit? Or first tell the reader about collectFromScript and then explain why it doesn't apply?)
• "$(mkFunction 'scheduleCollection) $(mkFunction 'contribute)" Are these supposed to be on two separate lines?
• "We can't use the usual Haskell syntax highlighting " --> "Careful readers will have spotted that the above lines aren't highlighted in the same ways as the previous example code"
• "is not available here" --> "is not available for this tutorial"
• Rewrite the tutorial to skip the intermediate definitions? That would be easier on the reader. It's tiring to be told "remember that thing you just took pains to understand? It's not actually the right way to do it."
• "The Plutus repository has a complete set of tests for the crowdfunding campaign:" This is rather unfair to the poor reader. "Go read this code and work out for yourself what it is doing." Best is to write a tutorial for this part as well. But if not, at least sound apologetic for not explaining it in detail. ("We plan to write a tutorial on this soon, but until then here is a pointer to the code, which we hope is fairly self-explanatory.")

Publically shareable Playround contracts

It would be nice if people were able to easily share complete Playgrounds contracts, ideally with a single immutable link.

However, we don't really want to store things ourselves.

Here's a way we could do this:

• Add Github auth
• Offer the option to "save" to a gist, then providing the result as an immutable link based on the gist (i.e. you can access it without having to be logged in)

Make the blockchain visualization easier to interpret

Right now it's quite faithful to the UTxO, but it's hard to interpret. You often have to work backwards to match up what you expect to see with what's there.

Not entirely sure how to do this. A few ideas:

• Maybe move away from Sankey diagrams as they're confusing when big.
• Can we somehow get user-defined labels for transactions or inputs/outputs?
  • Not sure if we can - our transaction model doesn't support that kind of metadata.
• Spread things out more, better labelling, legends, etc.

Plutus-core overflows for values allowed by the specification

The spec allows integers with size 1 as large as 127, but the reference implementation overflows at just 4.

$ cat overflow.plc
(program 0.1.0 (con 1 ! 4))
$ cat overflow.plc | language-plutus-core-run-ck
Integer overflow at 1:21.

Transactions should have an interval during which they can be validated

The reason for this change is explained here: IntersectMBO/cardano-ledger#139

This issue is for the implementation in the emulator (mockchain).

Validating the next data script

This is one of two problems related to contracts that span multiple transactions. By "contract" I mean a set of contract endpoints that spend and produce outputs to some script address. By "span multiple transactions" I mean that the contract results in at least one transaction that consumes outputs from and produces outputs to the contract address (this is not true for the crowdfunding campaign).

The problem

We can think of the contract as a state machine, with states of type S and inputs of type I. The state is kept in the data script, and the input is supplied as the redeemer script. The transition function t :: S -> I -> S is the validator (throwing an error if the transition is not allowed).

In order for this work, we need a transaction tx that spends an output from the script address (this output determines t and the current state s :: S) using a redeemer with the input i :: I. tx also produces a new output to the script address, with a data script s' :: S such that s' = t s i. How can the validator script ensure that the new data script is actually t s i, and not some other state? If it can't, then the contract can be manipulated very easily, by providing a different data script. This is the "validating the next data script" problem.

It is a problem because inside the validator script we only know t s i :: S and hash(s') :: ByteString, so we're either missing the actual s' :: S in non-hashed form, or a way to compute hash(t s i) :: ByteString.

Possible solutions

1. Implement a hashing function inside PlutusTx.
2. Allow the validator script to look at the values of the data scripts of tx.
3. Change the encoding of the state machine so that the validator gets hash(t s i) from the slot leader.

For (1), we need to make sure that we are computing the correct hash. The hash(s') that the validator script can see is really the hash of the serialised PLC term s', including the (program ...) tag. So the thing that's actually necessary in Plutus is a function serialiseS :: S -> ByteString that produces exactly the same output. We could potentially generate serialiseS using Template Haskell, similar to makeLift.

For (2) we need to consider that we don't know the type of the data scripts produced by tx in the validator script (they may all be of different types). So we would need something like the Data.Dynamic module.

For (3) we can change the signature of the validator function to v :: (S, I) -> (S, I) -> (). (Note that the data and redeemer scripts have the same type now). If we assume that the first element of the first argument is the current state, the first element of the second argument is the new state, and the second element of the second argument is the input then we can transform the old state machine into this format: v (currentState, _) (newState, input) = if t currentState Input == newState then checkHashes else error where checkHashes compares the hashes of the redeemer and the new data script (both hashes are available as part of the tx data supplied by the slot leader). This works already, without requiring any changes to the language. But it means that every (state, input) pair is put on the chain twice.

Export `Int` operators from Plutus Prelude

Change order of arguments in validator script

Currently we have Redeemer -> DataScript -> PendingTx -> () but it would be more natural to have DataScript -> Redeemer -> PendingTx -> () so that the arguments are ordered chronologically

Value checking and checking whether types are normalized

There are several problems in Language.PlutusCore.Check.Normal

1. An infinite loop:

checkTerm :: (AsNormalizationError e TyName Name a, MonadError e m) => Term TyName Name a -> m ()
checkTerm p = void $ throwingEither _NormalizationError $ checkTerm p

2. Why does checking that all types appearing in a term are normalized require return the term back?

checkT :: Term tyname name a -> Either (NormalizationError tyname name a) (Term tyname name a)

It can be just

checkT :: Term tyname name a -> Either (NormalizationError tyname name a) ()

Same for termValue, typeValue, etc.

3. NormalizationError is misleading: we do not normalize there, only check whether things are already normalized.

4. We have the problem that eqInteger {s} x y is considered a value. This is a long-standing problem which we can't solve right now, because we're not yet settled on whether builtins are saturated or not or maybe we want to throw static builtins away entirely (which is another argument for doing that).

5. Checking whether a term is a value also entails checking that all types in it are normalized. Those should be two distinct checks, because sometimes we want the former and not the latter and vice versa.

6. Names like checkT and preCheck are not helpful.

7. Checking whether a term is a value is also defined in View.hs. We need to merge the two versions (possibly by just throwing away isValue from View.hs).

Conditionally clearing out Actions when contracts are recompiled

At the moment we're fairly dumb about how recompilation can affect actions. When the software is recompiled, I think we need to keep the action list as-is unless the resulting schema has changed, in which case we must remove it and make the user start again.

Integration into Cardano Core

This ZenHub epic covers the integration of Plutus and the Extended UTxO model into Cardano Core.

Adapt Agda docs to new versions of Agda

The Agda people changed something and now we get lots of unsolved metavariables. Just need to provide more types.

Spec: validity of contexts

Figure 3 in the Plutus Core specification has rules for the validity of contexts. Only the rule for the empty context has a conclusion saying that it was valid; should the other two rules be changed to conclude that the things on the bottom are valid as well? [When I opened this issue I thought I'd changed this in the spec, but it seems not.]

This also raises the question of why we need validity. I don't think it's actually used anywhere else, so what purpose does it serve? Do we want to prove that the typing rules only allow you to construct valid contexts? Do we want to say that some rules are only applicable when the contexts are valid?

"User-friendly" description of type system in Plutus Core specification.

Before PlutusFest it was suggested that we should try to make the spec more user-friendly, and @mchakravarty proposed a plan here:

https://input-output-rnd.slack.com/archives/C21UF2WVC/p1543403856559300

I think the only thing that's still outstanding is explanation of the type system. Could you have a go at this please, Rebecca?

We've just been merging stuff with the master branch without pull requests, the idea being that we would try to get it roughly into shape and then polish it when everyone was done. I did quite a bit of fiddling with the Latex to try and get the figures into the right place.

Logging/monitoring for Core Node DevOps

Before we can deploy Plutus in production (or even on a testnet), we need to be able to monitor the PLC infrastructure that gets deployed as part of Core Nodes.

Multiple traces in the Playground

Often you want to test out several different scenarios when developing a contract (e.g. "successful campaign", "failed campaign"). At the moment you have to manually clear and re-enter each every time you want to use it.

Ideally we'd let you have several (named?) traces available at any one time. That would probably mean we need to change the UI a bit too - I was thinking something a bit more like Trello lists.

Plutus Core programs with interesting evaluation properties

We need to add Plutus Core programs which evaluation is somehow interesting. For example:

1. a program that takes long to compute, but does not allocate much (already implemented)
2. a program that uses mutual recursion (in process)
3. "Examples with a modest peak allocation but large total allocation would be ones where a GC really helps, and it'll be interesting to look at such examples since IELE currently lacks any GC support in its plutus impl." (citing Duncan)
4. a program with large total allocation to complement the previous case

Anything else?

building plutus fails on NixOS 18.09

When attempting to build the Plutus core on NixOS 18.09, I've experienced this error.

Is plutus ready for building at this time?

Error

$ nix build -f default.nix localPackages.language-plutus-core
[1/0/103 built, 0.0 MiB DL] building ghc-8.4.3 (buildPhase): "/build/ghc-8.4.3/inplace/bin/haddock" --verbosity=0 --odir="libraries/Cabal/Cabal/dist-install/doc/html/Cabal" --no-tmp-comp-dir --dump-interface=libraries/Cabal/Cabal/dist-install/doc/html/Cabal/Cabal.haddock builder for '/nix/store/h9ydgbajf3lrxkj3lj67mq9hg1g7w7r9-ghc-8.4.3.drv' failed with exit code 2; last 10 log lines:
      vectTopBinder vectTopBind
  Warning: WwLib: could not find link destinations for:
      WwResult
  Warning: DmdAnal: could not find link destinations for:
      useLhaddock: internal error: Unable to commit 1048576 bytes of memory
      (GHC version 8.4.3 for x86_64_unknown_linux)
      Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
  make[1]: *** [compiler/ghc.mk:448: compiler/stage2/doc/html/ghc/ghc.haddock] Aborted
  make[1]: *** Deleting file 'compiler/stage2/doc/html/ghc/ghc.haddock'
  make: *** [Makefile:127: all] Error 2
cannot build derivation '/nix/store/rn9w6rf9l8ya9kc3si2g8wy8wmqapsf3-language-plutus-core-0.1.0.0.drv': 1 dependencies couldn't be built
[0 built (1 failed), 0.0 MiB DL]
error: build of '/nix/store/rn9w6rf9l8ya9kc3si2g8wy8wmqapsf3-language-plutus-core-0.1.0.0.drv' failed

NixOS Machine Info

This is a Virtualbox virtual machine as well. Sourced from https://nixos.org/nixos/download.html

$ nix-shell -p nix-info --run "nix-info -m"
warning: ignoring untrusted substituter 'https://hydra.iohk.io'
these paths will be fetched (20.04 MiB download, 217.86 MiB unpacked):
  /nix/store/6yz7851vibc1xjxpiyfzqqi2ksbv6qah-binutils-wrapper-2.30
  /nix/store/h0lbngpv6ln56hjj59i6l77vxq25flbz-binutils-2.30
  /nix/store/i6vl5lwlz5jbkg4r6p340dwmj6fha3xq-stdenv-linux
  /nix/store/iw94llkj05wgaz268mlzvgx8jkbi1ss0-gcc-wrapper-7.3.0
  /nix/store/kic17fw8wil74k04kzh3dha43izrr9j3-bash-interactive-4.4-p23-dev
  /nix/store/ynb9h0q59ykdpmsn5m2qrkmnq1p683wr-expand-response-params
copying path '/nix/store/kic17fw8wil74k04kzh3dha43izrr9j3-bash-interactive-4.4-p23-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/h0lbngpv6ln56hjj59i6l77vxq25flbz-binutils-2.30' from 'https://cache.nixos.org'...
copying path '/nix/store/ynb9h0q59ykdpmsn5m2qrkmnq1p683wr-expand-response-params' from 'https://cache.nixos.org'...
copying path '/nix/store/6yz7851vibc1xjxpiyfzqqi2ksbv6qah-binutils-wrapper-2.30' from 'https://cache.nixos.org'...
copying path '/nix/store/iw94llkj05wgaz268mlzvgx8jkbi1ss0-gcc-wrapper-7.3.0' from 'https://cache.nixos.org'...
copying path '/nix/store/i6vl5lwlz5jbkg4r6p340dwmj6fha3xq-stdenv-linux' from 'https://cache.nixos.org'...
 - system: `"x86_64-linux"`
 - host os: `Linux 4.14.79, NixOS, 18.09.1228.a4c4cbb613c (Jellyfish)`
 - multi-user?: `yes`
 - sandbox: `yes`
 - version: `nix-env (Nix) 2.1.3`
 - channels(root): `"nixos-18.09.1228.a4c4cbb613c"`
 - nixpkgs: `/nix/var/nix/profiles/per-user/root/channels/nixos`

Resolve remaining issues with `ifix`

We have a few remaining questions we need to resolve:

• What should the syntactic form of ifix be?
  • Should it be saturated?
    • i.e. ifix f :: k -> * vs ifix f a :: *
  • Should it be a binder?
    • We could bind the argument of the pattern functor, and also the argument if it's a saturated form.
• Are there problems with preserving the normalization status of "multi-argment" pattern functors when we encode them into our unary version? (Not sure if I got that right, hopefully @effectfully can elaborate)

I believe the current state of the syntax is:

• The Haskell implementation has a saturated, non-binder ifix
• The Agda formalization has a non-staturated, non-binder ifix
• Rebecca's proposed formalization has a saturated, binder ifix

Plutus Playground: Attempting to use module ‘main:M585359051070849783727464’ which is not loaded

When compiling the following code via Plutus Playground this error pops up. I presume this stems from the fact that I haven't explicitly typed the inputs and thus there's a compiler error and the hint to be displayed is simply missing?

Line 1, Column 1:

error:
attempting to use module ‘main:M772636699082615801227464’ (/tmp/hint-6218b5e19d038a73/M772636699082615801227464.hs) which is not loaded

import qualified Language.PlutusTx            as PlutusTx
import qualified Language.PlutusTx.Prelude    as P
import           Ledger
import           Ledger.Validation
import           Wallet
import           Playground.Contract


walletValidator :: ValidatorScript
walletValidator = ValidatorScript (Ledger.fromCompiledCode $$(PlutusTx.compile [||
    (\_ _ _-> ()) ||]))

Fix untyped terms generation

I noticed that this property

propParser :: Property
propParser = property $ do
    prog <- forAll genProgram
    let reprint = BSL.fromStrict . encodeUtf8 . prettyPlcDefText
        proc = void <$> parse (reprint prog)
        compared = and (compareProgram (void prog) <$> proc)
    Hedgehog.assert compared

passes even if what is printed can't be parsed back, because parse returns an Either and and called over Left returns True. This kinda defeats the entire purpose of the test.

If I change the last two lines to

        compared = compareProgram (void prog) <$> proc
    Hedgehog.assert (fromRight False compared)

I immediately get parsing errors which are all due to poor terms generation:

1. since type-level and term-level lambdas are denoted the same way in our syntax, a type-level lambda generated at the term level (which should not happen) gets printed and parsed as a term-level lambda
2. constants bounds are not checked, so we generate stuff like this:

Program (Version () 0 0 0) (Constant () (BuiltinInt () 1 (-9859937)))

which doesn't parse due to the out-of-bounds constant (maybe we really shouldn't do bounds checking during parsing).

There are also problems in

genName :: MonadGen m => m (Name ())
genName = Name () <$> name' <*> int'
    where int' = Unique <$> Gen.int (Range.linear 0 3000)
          name' = BSL.fromStrict <$> Gen.utf8 (Range.linear 1 20) Gen.lower

because we can generate names that have same uniques, but distinct string representations which violates one of our invariants. Besides, with such generation, terms where the same variable appearing twice are rather rare.

Do not throw away `CheckState` on `TypeError`

In

newtype CheckM a = CheckM { unCheckM :: StateT CheckState (Either TypeError) a }

CheckState is thrown away if an arrow is returned. Having CheckState regardless of whether type checking returned an error or not can be useful for tests and debugging. So I propose

newtype CheckM a = CheckM { unCheckM :: ExceptT TypeError (State CheckState) a }

Build instructions

Hey,

I 'm new with Haskell techno stack.
Do you think it's possible to add few build instructions in readme file than can help me to run 'cabal repl' command ?
Currently I have :

$ cabal repl 
Package has never been configured. Configuring with default flags. If this
fails, please run configure manually.
Resolving dependencies...
Configuring plutus-prototype-0.1.0.0...
cabal: At least the following dependencies are missing:
cardano-crypto -any

Even if previous 'stack install' did fetch and build cardano-crypto dependency, build and cache plutus-prototype (with couple of warnings :)).
I am testing master branch.

Thanks for your help

Plutus Playgrounds

ZenHub epic issue comprising all the work on Plutus Playgrounds.

Tabs for different sections of the Playground

At the moment it's very long, it would be nice to have tabs for e.g.

• Editor
• Traces
• Visualization

Underscores in Numeric Literals

I am sorry if this is not the right place.

How about changing the syntax of numeric literals in plutus?
Haskell/GHC has recently adopted an extension that enables underscores in numeric literals:

• https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0009-numeric-underscores.rst

Current syntax

In my understanding, the current specification of numeric literals in plutus is below:

• https://cardanodocs.com/technical/plutus/types/#ints-floats-and-byte-strings

<int> ::= "-"? <digit>+
<float> ::= "-"? <digit>+ <fractExponent>
<digit> = "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
<fractExponent> ::= <fraction> <exponent>? | <exponent>
<fraction> ::= "." <digit>+
<exponent> ::= ("e" | "E") ("-" | "+") <digit>+

<bytestring> ::= "#" <byte>*
<byte> ::= <nybble> <nybble>
<nybble> ::= <digit>
           | "a" | "b" | "c" | "d" | "e" | "f"
           | "A" | "B" | "C" | "D" | "E" | "F"

Proposed change syntax

How about changing it as follows?
This improves the readability, quality and expressiveness, especially for large numeric literals.

- <int> ::= "-"? <digit>+
+ <int> ::= "-"? <digit> ("_"* <digit>)*

- <float> ::= "-"? <digit>+ <fractExponent>
+ <float> ::= "-"? <digit> ("_"* <digit>)* <fractExponent>

- <fraction> ::= "." <digit>+
+ <fraction> ::= "." <digit> ("_"* <digit>)*

- <exponent> ::= ("e" | "E") ("-" | "+") <digit>+
+ <exponent> ::= ("e" | "E") ("-" | "+") <digit> ("_"* <digit>)*

- <bytestring> ::= "#" <byte>*
+ <bytestring> ::= "#" (<byte> ("_"* <byte>)*)?

Example

The followings are examples of this proposal:

lovelace = 0.000_001 :: Float
ada = 1_000_000 :: Int

GHC 8.6 compatibility

We'd like to compile with 8.6, especially since this the major version planned to be used for the Shelly release.

However, there is at least one blocker, namely we are affected by https://ghc.haskell.org/trac/ghc/ticket/16104.

Plugin issues with optimization levels greater than 0

At least:

• Sometimes GHC replaces newtypes with their representation types.
  • I haven't been able to reproduce this, but it's sometimes visible on the Swap example contract.
  • Would probably be fixed by mirroring GHC's zero-cost newtypes by identifying the types on our side too, which we should probably do.
• GHC replaces some list literals with calls to build, which we can't deal with well.

Do not use lazy `ByteString`s for variable names

The docs state:

A key feature of lazy ByteStrings is the means to manipulate large or unbounded streams of data without requiring the entire sequence to be resident in memory. To take advantage of this you have to write your functions in a lazy streaming style, e.g. classic pipeline composition. The default I/O chunk size is 32k, which should be good in most circumstances.

so we shouldn't use lazy ByteStrings for variables names, because names are small.

Moreover, we probably shouldn't use any pinned-memory-based data structures for name handling, because they cause memory fragmentation when there are many of them and we don't want to analyze whether we have "many" names or not, because it's error-prone.

Our best bet is probably ShortText (which is defined in terms of ShortByteString which is not pinned-memory-based). Related blog post.

nix build gives 503 error ... guessing this can't be done so easily on ubuntu

warning: unable to download 'https://cache.nixos.org/nar/074xjadzxz09k69jnh4j2889w8k4wb8h7r2l0wgg3904cbnbk8ch.nar.xz': HTTP error 503; retrying in 283 ms

recommending any nix hosting service?

Plutus Playground: "UnexpectedHTTPStatus: 502 Bad Gateway" On Evaluating

So I've finally gotten around to begin reading through much of the github repo & attempt to write my own SC in Plutus Playground however I've run into some errors when straying off of the path of just running the pre-defined contracts.

In this case I successfully compiled, however upon depositing ada and then attempting to withdraw from the same wallet, when evaluating I simply get:

UnexpectedHTTPStatus: <html> <head><title>502 Bad Gateway</title></head> <body bgcolor="white"> <center><h1>502 Bad Gateway</h1></center> <hr><center>nginx</center> </body> </html> (StatusCode 502) Please try again or contact support for assistance.

import qualified Language.PlutusTx            as PlutusTx
import qualified Language.PlutusTx.Prelude    as P
import           Ledger
import           Ledger.Validation
import           Wallet
import           Playground.Contract


walletValidator :: ValidatorScript
walletValidator = Ledger.emptyValidator
              

scAddress :: Address'
scAddress = Ledger.scriptAddress walletValidator

deposit :: Value -> MockWallet ()
deposit val = payToScript_ scAddress val Ledger.unitData

withdraw :: MockWallet ()
withdraw = collectFromScript walletValidator Ledger.unitRedeemer

$(mkFunction 'deposit)
$(mkFunction 'withdraw)

Plutus Core library

This ZenHub epic tracks work on the Plutus Core language library.

Add convenience for `L.fromCompiledCode $$(P.compile ...)`

The two are used together quite often so the library should offer a function that combines them

Move from hint to runghc

hint took a long time to compile new code and for the server to
warm up, see haskell-hint/hint#56
Additionally, only one request could be processed at a time.
By spawning a runghc process for every request we get around
both of these problems. The trade off is that there is a startup
overhead, however some rough timing has shown this to be negligeable.

Do we have keywords?

Are syntax identifiers like lam, error etc. keywords?

• The spec says no: there is nothing in the grammar that says they're invalid identifiers.
• The parser says yes: you'll get an unexpected token error if you try to use one
  • echo "(program 1.0.0 (lam error (forall a (type) a)) error" | plc typecheck --stdin
  • Unexpected 'error' at 1:21