Turn redundent Bitcoin primitives into Jets

[roconnor-blockstream]

Some Bitcoin primitives are redundant because I thought it was impractical to iterate over all possible inputs of a transaction which is limited to 2^32 inputs due to limits in Bitcoin's format.

However recent experiments show that, while Simplicity specifications of such large iterations are not reasonable to execute, they are still practical to define and reason about by using a generic monoidal (semi-group) sumMap construction:

-- A monoid sum of all f :: term (k, i) a for every value of type i in lexicographical order with @dot@ as the monoidal operator.
sumMap :: forall term a i k. (Core term, TyC a, TyC i, TyC k) => term (a, a) a -> term (k, i) a -> term k a
sumMap dot = rec reify
 where
  rec :: forall i k. (TyC k) => TyReflect i -> term (k, i) a -> term k a
  rec OneR f = iden &&& unit >>> f
  rec (SumR il ir) f = (rec il (oh &&& injl ih >>> f)) &&& (rec ir (oh &&& injr ih >>> f)) >>> dot
  rec (ProdR i1 i2) f = rec i1 (rec i2 (ooh &&& (oih &&& ih) >>> f))

For example we can write totalInputValue as a jet:

totalInputValue :: (Primitive term, Core term) => term () Word64
totalInputValue = sumMap add64 (drop (primitive InputValue) &&& unit >>> match zero64 oh)
 where
  zero64 = zero word64
  add64 = adder word64 >>> ih

The resulting Simplicity DAG specifying this expression has only 1000 nodes, and the code will be easy to formally reason about. A more sophisticated implementation may even be practically executable for small transactions.

We should be able to turn the following Bitcoin primitives into jets:

• inputsHash
• outputsHash
• numInputs (find the minimal index where the inputPrevOutpoint fails).
• totalInputValue
• numOutputs
• totalOuputValue

The current* primitives may also be replaced by jets if we are willing to accept a definition using assertions that provably never fail.