[Simplicity] Pretty Printer example program (was: Fuzz testing vectors)

[Russell O'Connor]

Dear subscribers,

Given Greg's recent collection of Simplicity test vectors, I thought it
might be helpful if I created a little Haskell program to pretty-print
Simplicity programs.  My main motivation here is to illustrate how to use
the Haskell Simplicity library in a small application.

This program, PrettyPrint.hs, depends on the Simplicity library from commit
https://github.com/ElementsProject/simplicity/tree/cf12c6947c2d6730e31482ec291658f10ccc9207
.

----8<----
module Main where

import Control.Monad
import qualified Data.ByteString as BS
import Data.Functor.Fixedpoint
import Data.Foldable
import Data.Sequence (Seq)
import Data.Serialize
import Data.Void
import Lens.Family2
import Lens.Family2.Stock
import System.IO

import Simplicity.Elements.Inference
import Simplicity.Elements.Serialization.BitString
import Simplicity.Serialization
import qualified Simplicity.Tensor as Tensor
import Simplicity.Ty (Ty, UntypedValue)
import qualified Simplicity.Ty as Ty

-- Printing out raw Simplicity types gets pretty exhausting
-- Below we build a custom data type for Simplicity type annotations so we
can nicely display common Simplicity types.
data PrettyTy = Two Integer -- This constructor represents n bit word types
in Simplicity when n is 0 or a power of 2.
              | Sum PrettyTy PrettyTy
              | Prod PrettyTy PrettyTy

-- The heart of the 'PrettyTy' pretty printer
instance Show PrettyTy where
  showsPrec _ (Two 0) = showString "One" -- a 0-bit type is the unit type.
  showsPrec _ (Two 1) = showString "Two" -- a 1-bit type
  showsPrec _ (Two n) = showString "Two^" . shows n -- an n-bit type
  -- One + X is the canonical way to represent the Maybe type, usually
denoted by 'S'
  showsPrec _ (Sum (Two 0) y) = showParen True (showString "S " . shows y)
  showsPrec _ (Sum x y) = showParen True (shows x . showString " + " .
shows y)
  showsPrec _ (Prod x y) = showParen True (shows x . showString " × " .
shows y)

-- The transformation from a Simplicity type into 'PrettyTy' making it
ready for pretty printing.
mkPrettyType :: Ty -> PrettyTy
mkPrettyType = cata f
 where
  f Ty.One = Two 0
  f (Ty.Sum (Two 0) (Two 0)) = Two 1
  f (Ty.Sum x y) = Sum x y
  f (Ty.Prod (Two i) (Two j)) | i == j && i /= 0 = (Two (i+j))
  f (Ty.Prod x y) = Prod x y

-- The type 'forall m. Monad m => m Void -> m Bool -> m X' is a generic
function for parsing bitstreams into a value X.
-- The two parameters, 'next' and 'abort', provide generic callbacks for
requesting a bit, or indicating a parse failure.
--
-- In Simplicity, we can only complete parsing of the witness bitstream
after type inference.
-- In this function we first parse the untyped Simplicity program from the
bitstream (using 'abort' and 'next').
-- Next we run type typeInference to add Simplicity type annotations to the
dag for a Simplicity program.
-- which is a Simplicity expression with a type from Unit to Unit.
-- Lastly, if typeInference was successful, we parse the witness data
bitstream and fill in any witness combinators with their data.
getDagAndWitness :: Monad m => m Void -> m Bool -> m (Either String
(SimplicityDag Seq Ty UntypedValue))
getDagAndWitness abort next = do
  uterm <- getDagNoWitnessLengthCode abort next
  let tterm = typeInference ((),()) uterm :: Either String (SimplicityDag
Seq Ty ())
  wterm <- traverse (\term -> getWitnessData term abort next) tterm --
traversing (Either String)
  return wterm

-- The main program reads a Simplicity program encoded as a bitstream from
stdin and pretty prints it to stdout.
-- Each node in the pretty printed DAG is on its own line, with a line
number prefix.
-- The nodes have pretty printed type annotations, and references to the
line numbers of their children expressions (if any).
-- If there is a failure, instead an error message is printed to 'stderr'.
main :: IO ()
main = do
  bs <- BS.getContents -- read all of stdin.
  let wterm = flip runGet bs (getEvalBitStream getDagAndWitness) -- parse
stdin using the 'getDagAndWitness' parser.
  case join wterm of -- join on (Either String) combines the outer errors
from runGet with the inner errors from 'getDagAndWitness'
    Left err -> hPutStrLn stderr $ "Error: " ++ err
    Right term ->
      -- 'typeCheck' performs a double check on the type annotations.  We
ignore any return value.
      case typeCheck term :: Either String (Tensor.Unit () ()) of
      Left err -> hPutStrLn stderr $ "Error: " ++ err
      Right _ -> do
        let zippedList = zip [0..] (toList term) -- create line numbers
from the list of nodes.
        let padding = length (show (length zippedList - 1))
        let printNode (i, item) = putStrLn (pad padding (show i) ++ ": "
                               ++ show (item & tyAnnotation %~ mkPrettyType
-- change the type annotations into pretty printed ones.
                                             & mapped %~ (i -))) -- convert
the references to children from relative to absolute.
        mapM_ printNode zippedList
 where
  pad n str = replicate (n - length str) ' ' ++ str
----8<----

Below I give an example run of the above program on one of Greg's test
vectors (see https://lists.ozlabs.org/pipermail/simplicity/2019/000019.html
).

----8<----
$ runhaskell PrettyPrint.hs < assert_9
 0: Prim (someArrow currentAsset)
 1: Prim (someArrow outputNullDatum)
 2: Prim (someArrow version)
 3: Pair One Two^32 Two^32 2 2
 4: Injl Two^64 (S (S ((Two^2 × Two^256) + (Two + Two^4)))) One 1
 5: Comp One Two^64 ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One) 3 4
 6: Prim (someArrow currentIssuanceContract)
 7: Prim (someArrow currentScriptHash)
 8: Pair One Two^256 ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One) 7 5
 9: Pair One (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) +
One)) (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)) 8 8
10: Pair One ((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) +
One)) × (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)))
Two^256 9 7
11: Unit ((((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))
× (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))) ×
Two^256) × ((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))
× (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))))
12: Pair One (((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) +
One)) × (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))) ×
Two^256) ((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)) ×
(Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))) 10 9
13: Comp One ((((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) +
One)) × (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))) ×
Two^256) × ((Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One))
× (Two^256 × ((S (S ((Two^2 × Two^256) + (Two + Two^4)))) + One)))) One 12
11
----8<----

The output above writes "line numbers" for each combinator, given their
inferred type annotations, and then references to the line numbers of their
child subexpressions.

When we inspect the test vectors we see many of them have disconnected
DAGs, where some lines do not have references (in the above example line 6
is unused).  Some examples are even more extreme with the program
ending in Iden
One or Unit One, which makes the root of the DAG disconnected from the rest
of the graph.  Eventually these sorts of non-canonically encoded programs
will be rejected by the C implementation.  Despite this, the fuzzer does
seem to do a reasonable job of exercising the deserializer and the
typechecker, both of which operate on the whole DAG, even if it is
disconnected.  Some kind of special purpose generator of well-typed
Simplicity programs may be needed to exercise the evaluation engine.

I hope this example program proves useful.  For me, it has already been
useful.  I added the tyAnnotation traversal (
https://github.com/ElementsProject/simplicity/blob/cf12c6947c2d6730e31482ec291658f10ccc9207/Haskell/Indef/Simplicity/Inference.hs#L159-L161)
in order to pretty print the type annotations, and I now see that it might
be helpful to rearrange the parameters to getWitnessData to make partial
application easier.

Keep in mind that the library and even binary format is still under
development, and this program and these specific test vectors are not
guaranteed to remain fixed at this point in time.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.ozlabs.org/pipermail/simplicity/attachments/20191126/d2172832/attachment.htm>