Types (and type inference) in Pact

Today, we released Pact 2.0 to our open source repo. The headline feature is the addition of static/explicit types.

Why was Pact untyped before?

Pact was designed to be highly legible, and easy to program. Our goal in not having types was to keep clutter out of the code, and enable rapid prototyping and development. With database programming, we liked the idea of being able to add extra data to a row to capture arbitrary event details that weren’t important to the smart contract functionality itself.

With Pact 2.0, you can still code this way. But most importantly, you can get all the benefit of strong typing without littering types all over your code, thanks to the magic of type inference.

Type Inference in Pact

Pact types, when specified, are enforced at runtime. If you say that argument a of your function is a string and the user passes in an integer, the interpreter enforces this and errors out before your function executes.

As such, Pact does no typechecking when you load code into the environment. Instead, the REPL environment offers the typecheck function, which will perform type inference on the entire module and alert you to any type errors, or anywhere it cannot determine the type.

The type inference algorithm is based on Hindley-Milner, although it is “lazier” about function types for some native functions which are overloaded. For instance, the + function is heavily overloaded to handle numbers, lists, objects and strings, and even handle upcasting integer/decimal combinations:

Overloads for +

x <a[integer,decimal]>, y <a[integer,decimal]> → <a[integer,decimal]>

x <a[integer,decimal]>, y <b[integer,decimal]> → decimal

x <a[string,[<l>],object:<{o}>]>, y <a[string,[<l>],object:<{o}>]>
     → <a[string,[<l>],object:<{o}>]>

As a result, the type inference must first substitute all types for non-overloaded functions, before attempting to solve each overload.

Also, Pact does not typecheck user code as-is. When it typechecks a function, it resolves the entire AST of the function with all of its references fully inlined. As a result, function types as specifid are not used per-se, but instead applied piecewise to the AST elements in whatever application is using them.

So, Pact inference is its own unique beast, but it works well and is a superb development aid.

Formal Verification

The typechecker is also essential for a new feature we will be demonstrating at the Stanford Blockchain Conference: formal verification of Pact functions by compiling Pact to SMT-LIB2 and using Z3.

The typechecker’s exploded, inlined AST result is precisely what is needed for SMT-LIB2 compilation. Since Pact is already SSA and Turing-incomplete, its compiled form is strikingly similar to the SMT language.

Preview of Z3 compilation

Preview of Z3 compilation

But the code must fully typecheck: the prover can’t work with anything but concrete types.

Code Your Way

Type inference makes for a pretty unique system. You can code without types altogether, relying on unit tests to provide necessary coverage.

;; module with no types
(module pay 'module-keyset

  (deftable accounts)

  (defun pay (from to amount)
    (with-read accounts from { "balance":= from-bal }
      (with-read accounts to { "balance":= to-bal }
          (check-balance)
          (update accounts from
            { "balance": (- from-bal amount),
              "amount": (- amount) })
          (update accounts to
            { "balance": (+ to-bal amount),
              "amount": amount }))))

  (defun check-balance (balance amount)
    (enforce (>= balance amount) "Insufficient Funds")))

You can use the typechecker to add “just enough” types for it to be happy, meaning you’re fully type-safe, and no more. Why have the runtime check more types than it absolutely needs?

;; module with schema and types to keep TC happy
(module pay 'module-keyset

  (defschema account
     balance:decimal
     amount:decimal)

  (deftable accounts:{account})

  (defun pay (from to amount)
    (with-read accounts from { "balance":= from-bal }
      (with-read accounts to { "balance":= to-bal }
          (check-balance)
          (update accounts from
            { "balance": (- from-bal amount),
              "amount": (- amount) })
          (update accounts to
            { "balance": (+ to-bal amount),
              "amount": amount }))))

  (defun check-balance (balance:decimal amount)
    (enforce (>= balance amount) "Insufficient Funds")))

Note that last function: since >= expects both arguments to be the same type, the typechecker only needs to know the type of one of the arguments.

But, you might want types to document your API. So go fully-typed:

;; module with schema and types to keep TC happy
(module pay 'module-keyset

  (defschema account
     balance:decimal amount:decimal)

  (deftable accounts:{account})

  (defun pay (from:string to:string amount:decimal)
    (with-read accounts from { "balance":= from-bal }
      (with-read accounts to { "balance":= to-bal }
          (check-balance)
          (update accounts from
            { "balance": (- from-bal amount),
              "amount": (- amount) })
          (update accounts to
            { "balance": (+ to-bal amount),
              "amount": amount }))))

  (defun check-balance (balance:decimal amount:decimal)
    (enforce (>= balance amount) "Insufficient Funds")))

Actually the example is still not fully-typed: pay is string, since update returns a status message; check-balance is bool, per enforce. They don’t add any information to your API, so why bother?

Other benefits of type inference

Coders familiar with Haskell or Scala know how nice type inference is, compared to Java or C++: once you go inference-style, other code just seems riddled with warts everywhere, harming readability.

In Pact’s case, there are other benefits too. Leaving types off will cause the typechecker to fail if a variable is unused, as it can’t use a function signature to infer the type. This is especially helpful during refactoring, where maybe you’re no longer updating that one field in the database: the typechecker’s complaints might save the day!

What’s the big deal?

With type inference and database schemas, the typical database-focused pact code won’t need any types outside of the schemas. At which point Pact starts to look a lot like SQL, which is of course strongly-typed by dint of the column types in the database, without needing to declare them in each query.

That’s a good thing: we want Pact to stay as streamlined as possible. Meanwhile, though, there is a sophisticated type inference engine that can handle far more complex scenarios that don’t touch the database: for all of it’s Turing-incompleteness, single-assignment, and simplicity, Pact is still a full programming language. As such, it’s nice to have an advanced feature like type inference to boost productivity!


Open-sourcing the Pact Smart Contract Language

We’re extremely excited to announce that we are releasing our smart-contract language Pact as open-source today.

Pact is a new way to write smart contracts on a blockchain, with a level of assurance not possible with other smart-contract languages. Pact is an expressive, easy-to-learn, and productive language to code in, with excellent tooling. Try it today, download a build or build and hack on it yourself.

The power of open source

Open-sourcing is all about empowering users, which is what motivates Pact as well: empowering users to enact meaningful events on a blockchain, safely and quickly. Open-sourcing amplifies this further.

For developers

If you are a developer writing smart contracts, an open-source language means you’re not dependent on out-of-date docs to educate you since you can always look at the code, and if there’s a problem you want to fix now, you simply fork and fix it.

For business users

If you are a business user, open-source means you can develop your business logic in Pact to run on a fast blockchain like ScalableBFT knowing that your code is your own, and is not encumbered by NDAs or licenses.

For us!

It even empowers us at Kadena, by leveraging the amazing ecosystem for software development. Pact is hosted on Github, is automatically built on every commit by Travis-CI, which we further leverage to make builds for multiple OSs on our downloads page. Our docs are hosted on readthedocs.org.

All of these amazing resources work together seamlessly and for free – if your project is open-source. It’s an excellent example of alternate incentivization schemes to encourage contributions to the public. And of course, we couldn’t even develop the technology without the peerless open-source language Haskell and all of the unbelievable community libraries available for it.

Pact Features

Headline features of Pact are:

Easy-to-use database metaphor

Pact puts the power of a flexible, fast key-value versioned database in your hands, making it easy to quickly model assets or other entities.

Simple module system

Pact allows for great factoring of smart-contract solutions. Modules hold related functions and constants, and also have the ability to “guard” tables. Re-using and factoring code is safe and easy.

Durable, safe code

Pact code is Turing-incomplete – unbounded looping is impossible, and recursion is detected when smart-contract modules are loaded into the blockchain. Pact code can only be a DAG (directed acyclic graph), which means also that any referenced code is inlined at load time, making for blazing performance, but also insuring that your code will not be harmed if an imported module is later re-defined.

Public-key authorization schemes, with external verification

Inspired by Bitcoin scripts, Pact is designed with access control in mind from the ground-up. The concept of keysets ensures that any resource can be controlled by one or more public keys. Modules, tables and even rows in the database can all be governed by separate keyset rules. The key verification itself is handled by the blockchain running the contract: a developer never need worry about faulty crypto.

Confidential multi-phase transactions with “pacts”

Confidentiality on-chain demands new approaches to business logic, as the “one database to rule them all” of Bitcoin and public chains no longer applies. “Pacts” offer a way to ensure that while you cannot see your counterparty’s code, you can ensure they are acting in lock-step with you to complete a multi-phase transaction, like debit -> credit, or RFQ -> quote -> purchase -> deliver -> settle.

Go forth and transact!

Finally there’s an alternative for creating smart contracts. We’re very excited to see what developers and business users can create with this technology. Once you’re ready to run them on the fastest blockchain, send us a note.


Mining and private blockchains don't mix

Why you can’t use mining based consensus for private blockchains

Bitcoin’s mining mechanism is a masterstroke of algorithmic design, enabling a scalable Byzantine Fault Tolerant consensus by achieving a specific balance of incentives. Mining-based blockchains like Bitcoin are public: anyone can become a miner simply by downloading the software and firing it up. Permissioned, or private, blockchains seek to replicate the trustworthiness and robustness of public blockchains but with restricted memberships of known, approved participants, for regulatory reasons, for confidentiality, and with hopes of improved throughput and latency.

It is often assumed that if mining works for public blockchains then surely it must also work for permissioned ones, perhaps even more robustly since access is locked down, reducing attack vectors. Mining, however, is not public by accident, and indeed is incompatible with permissioned settings. It is public by design, which is critical to the functioning of its incentive model.

Incentives in Mining

The role of incentivization in mining is as follows:

Incentives must ensure that the act of mining the “latest block” and publishing it without delay is more profitable than mining a “fork” from a prior block, or delaying publication of the newly-mined block.

In Bitcoin we see that this holds: the value (in new coin and in transaction fees) for mining and publishing the latest block exceeds the value of mining a fork or delaying the new block’s publication for even a second. However in some alt-coins, we’ve seen this incentive fail leading to majority-mining attacks that result in large swaths of the ledger being rewritten. In small mining pools, attackers are incentivized to mine long forks and only publish them when they could supersede the primary blockchain’s history of transactions; these attacks can perform double-spends by invalidating transactions previously made for physical assets.

The need for incentivization at all is related to public blockchains’ scalability and anonymity requirements. By creating a consensus mechanism where participants are incentivized to behave in a non-Byzantine way, we remove the need for the mechanism to be auditable as well as the need for users to message every participant. Participants do the right thing because their interests are aligned with the interests of the system. As a result, the addition of a new pool of miners or a new group of users has effectively no impact on network load and in fact enhances fault-tolerance.

Mining is thus private and non-auditable by design. It is only when a new latest block is mined that miners need to talk, so they may publish the block and claim their reward. However, this implies that the system must correctly incentivize miners to behave in non-Byzantine ways as it has no ability to verify their actions (beyond validating a newly mined block).

Another form of fault-tolerance is the network’s ability to increase mining difficulty as the hash rate increases. However, this can only take place when miners are incentivized to win the next block as often as they can. If the incentives fail, and securing that block yields little inherent value, then miners have little incentive to publish that block to the network once found. This is not much of an issue for public chains but is a huge issue for permissioned blockchains.

Permissioned Blockchains

Permissioned chains can take many forms, but overall they can be thought of as a Bitcoin-like utility where only known participants can gain access and interact with the system. It can be seen as a database shared amongst potentially adversarial firms.

The motivations for firms to agree to use such a system are:

  • Decrease mutual costs: resources and risk required to settle assets, operational efficiencies in high availability and disaster recovery, etc.
  • Gain new capabilities: automated workflow via smart contracts, a shared standard library of business logic, etc.

An important distinction between public and permissioned chains is that while every participant in a public chain can choose to participate or not in consensus (by mining), every participant in a permissioned chain necessarily participates in consensus. Permissioned blockchains exist to serve essential business functionality for the firms themselves, tracking ownership, providing audit trails, and so forth. Since the consensus mechanism decides what and when things get written to the blockchain, no firm will be willing to let others “run consensus” for them: each firm will necessarily participate in consensus. Thus, if mining is used for consensus then every business will participate in mining.

A Tale of Three Banks: Sneaky, Virtuous, and Unaware

The issues associated with mining permissioned chains are easiest to demonstrate through a thought experiment. Imagine a permissioned blockchain that uses mining for consensus, which three banks are using to trade high-value assets. The mining difficulty is set to target 10 minutes. We’ll call the banks Sneaky, Virtuous and Unaware and these banks are the only miners of the permissioned chain.

At 9am Virtuous asks if Sneaky will sell an asset for $90M. Sneaky only has one of these assets in stock and, finding the price to be fair, agrees. The transaction is signed and submitted it to the blockchain for consensus at 9:01am. At 9:02am, Unaware asks Sneaky to sell the same asset for $100M.

Unware has no idea that Sneaky just signed a transaction with Virtuous, and Sneaky has no reason to inform him. Seeing an opportunity, Sneaky agrees to the transaction with Unware, signs the transaction but makes sure that the new transaction references the same asset Sneaky used with Virtuous, and submits it to the blockchain at 9:03am. There are now two conflicting transactions out for consensus.

Sneaky now has a $10M incentive to invalidate the Sneaky-Virtuous transaction by making sure the Sneaky-Unaware transaction is mined first. Sneaky already knew that any coins and/or fees received from mining are insignificant in comparison to the value of the transactions Sneaky would be conducting. Moreover, Sneaky knows that so long as they publish mined blocks with the expected frequency distribution their cluster size will appear to be in line with the chain’s 10min difficulty level.

For just these scenarios, Sneaky has a large, on-demand mining cluster hidden in reserve. It is leased from a bitcoin mining farm at the rate of $1M for two blocks and is over several thousand times larger than the size of the cluster the permissioned blockchain is tuned for. Sneaky, in effect, can win any block for $1M, which is easily covered by the $10M potential profit. Sneaky switches it on and mines a block with the Sneaky-Unaware transaction in it. The block invalidating the Sneaky-Virtuous transaction is mined by 9:04am and a subsequent block is built off of it is mined at 9:05am. The 9:04am block is not published until 9:09am so as to keep up the appearance of a smaller cluster and the 9:05am block is kept in reserve, only to be published if a fork occurs when the 9:04am block is published. Sneaky has the incentive to run an 18 block long fork before the cost of forking matches the $10M incentive.

It is interesting to consider what possible equilibrium would result from this type of system, something like each bank continually generating a portfolio of possible next blocks on large, hidden clusters, allocating mining resources based on risk. However, no matter what the equilibrium is, it is clear that mining in a permissioned context has substantially different incentives than those of a public chain. Without proper incentive alignment, mining fails to fulfill its purpose of providing BFT consensus.

That equilibrium could look much like mining’s equilibrium today, just on a much larger scale – imagine the mining cluster size if every new block was worth $10M. The thought experiment suggests a direct relationship between the value of transactions on a private blockchain and the mining cluster size used for it. It seems that mining will always be inventive based, even if you remove its primary incentives. Furthermore, mining works because of incentives and it seems that the larger the incentives, the more resources are used to mine.

If it is the case that mined permissioned chains require very large clusters, then mined permissioned chains will never take off. They will simply be too expensive to operate when compared to traditional systems.

The question becomes: how to fix mining in such a way that we keep mining clusters small?

Imperfect Solutions

One solution to the issues described is to register all transactions with some central authority, so that the order of transactions is not determined by the miners. This centralizes the blockchain, at which point why bother with mining and a blockchain at all; the central registration authority is more than capable of ordering and replicating transactions with more familiar technologies. Indeed, this is how many of current systems work, with public-private institutions handling the settlement synchronization.

Another solution is a legal agreement that limits mining resources and bans invalidating transactions. This solution however misses the point. Permissioned blockchains are meant to enable adversaries to work together without trusting each other, instead trusting the system. If we have to rely on the courts for a BFT algorithm to function, then the algorithm is not BFT.

A bit of market research

Luckily, most large enterprise institutions do not want a permissioned blockchain that requires mining for other reasons:

  • Mining is wasteful: cycles must be burned to mine the next block which enterprise users see as inefficient.
  • Mining is probabilistic in nature: enterprise adopters tend to dislike that a transaction’s success if a probability, worrying about the rare but possible event of informing a client of a successful transaction only to have the transaction later be invalidated.
  • Mining is slow: being partly a function of time, mining is necessarily slow and cannot be sped up. For most enterprise applications, 7-14 transactions per second with 1-10 minute latencies is far too slow.

NB: the costs of mining mentioned above are well worth the mechanism’s utility when it comes to public chains – in return you get anonymous participation, massive robustness, and near infinite scalability.

Conclusion

Public blockchains herald a fundamentally new approach to solving many real world problems, and the ideas they illustrate hold substantial benefits for in industrial settings. Adoption by industry demands a robust, performant and fault-tolerant design that can provide BFT consensus in a private, permissioned context. As we have shown, mining cannot provide this, as it needs the public context for its incentives to function, and would be inefficient and slow.

Providing a solution to this challenge is a core reason we founded Kadena. Our solution is ScalableBFT, the first scalable high-performance permissioned BFT consensus mechanism. If you’re interested in learning more about it, please see our Consensus White Paper or .