Skip to content

Commit d47bfc6

Browse files
roconnor-blockstreamroconnor-blockstream
committed
Test Bitcoin jet deserialization
1 parent 3059d42 commit d47bfc6

File tree

6 files changed

+235
-155
lines changed

6 files changed

+235
-155
lines changed

‎C/bitcoin/primitive.h‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@
55

66
#include "../bitstream.h"
77
#include "../typeInference.h"
8-
#include "txEnv.h"
98

109
/* Allocate a fresh set of unification variables bound to at least all the types necessary
1110
* for all the jets that can be created by 'decodeJet', and also the type 'TWO^256',

‎Haskell/Tests/Simplicity/Bitcoin/FFI/Primitive.hs‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
{-# LANGUAGE ForeignFunctionInterface #-}
2+
module Simplicity.Bitcoin.FFI.Primitive
3+
( decodeJetCMR
4+
, ErrorCode(..)
5+
) where
6+
7+
import Foreign.C.Types (CInt(..))
8+
import Foreign.Ptr (Ptr)
9+
import Foreign.Marshal.Unsafe (unsafeLocalState)
10+
11+
import Simplicity.Digest
12+
import Simplicity.FFI.Bitstream
13+
import Simplicity.FFI.Dag
14+
15+
data ErrorCode = BitstreamEof | DataOutOfRange deriving (Eq, Show)
16+
17+
decodeError :: CInt -> Either ErrorCode ()
18+
decodeError 0 = Right ()
19+
decodeError (-2) = Left DataOutOfRange
20+
decodeError (-12) = Left BitstreamEof
21+
decodeError err = error $ "Simplicity.Bitcoin.FFI.Primitive.decodeError: Unexpected error code " ++ show err
22+
23+
foreign import ccall unsafe "" simplicity_bitcoin_decodeJet :: Ptr DagNode -> Ptr Bitstream -> IO CInt
24+
25+
decodeJetNode :: Ptr Bitstream -> (Either ErrorCode (Ptr DagNode) -> IO a) -> IO a
26+
decodeJetNode pstream k =
27+
withDagNode $ \pnode -> do
28+
error <- simplicity_bitcoin_decodeJet pnode pstream
29+
k (decodeError error >> return pnode)
30+
31+
decodeJetCMR :: [Bool] -> Either ErrorCode Hash256
32+
decodeJetCMR codeWord = unsafeLocalState $
33+
initializeBitstream codeWord $ \pstream ->
34+
decodeJetNode pstream $ \result ->
35+
case result of
36+
Left err -> return $ Left err
37+
Right pnode -> Right <$> dagNodeGetCMR pnode

‎Haskell/Tests/Simplicity/Bitcoin/Serialization/Tests.hs‎

Lines changed: 39 additions & 148 deletions
Original file line numberDiff line numberDiff line change
@@ -1,164 +1,55 @@
1-
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
2-
-- This modules tests Simplicity's serialization and deserialization functions.
1+
-- This module tests some serialization functionality.
32
module Simplicity.Bitcoin.Serialization.Tests (tests) where
43

5-
import Control.Arrow ((|||))
6-
import Data.Either (lefts)
4+
import Control.Monad (mzero)
75
import Data.Foldable (toList)
8-
import Data.Maybe (fromMaybe)
9-
import Data.Serialize (Get, Putter, runGetState, runPut)
10-
import qualified Data.Vector as V
11-
import qualified Data.Vector.Unboxed as UV
12-
import Lens.Family2 (Traversal, (&), (.~))
13-
14-
import Simplicity.Bitcoin.Dag
15-
import Simplicity.Bitcoin.Inference
6+
import qualified Data.List as List
7+
import qualified Data.Vector.Unboxed as V
8+
9+
import Simplicity.Arbitrary
10+
import Simplicity.CoreJets
11+
import Simplicity.Bitcoin.Jets as Bitcoin
12+
import Simplicity.Bitcoin.FFI.Primitive as Bitcoin
13+
import Simplicity.FFI.Dag
1614
import Simplicity.MerkleRoot
17-
import Simplicity.Bitcoin.Primitive
18-
import Simplicity.Bitcoin.JetType
19-
import Simplicity.Bitcoin.Serialization.BitString as BitString
20-
import Simplicity.Bitcoin.Serialization.ByteString as ByteString
21-
import Simplicity.Bitcoin.Term
22-
import Simplicity.Digest
23-
import qualified Simplicity.Programs.Arith as Arith
24-
import Simplicity.Programs.Sha256.Lib
2515
import Simplicity.Serialization
26-
import Simplicity.Ty.Tests hiding (tests)
16+
import Simplicity.Ty
2717
import Simplicity.Ty.Word
2818

2919
import Test.Tasty (TestTree, testGroup)
30-
import Test.Tasty.QuickCheck ( Testable, testProperty, Positive(Positive)
31-
, Gen, Property, arbitrary, choose, elements, forAll, listOf1, oneof)
32-
import Test.QuickCheck.Property (Result, failed, succeeded, reason)
20+
import Test.Tasty.HUnit ((@=?), testCase)
21+
import Test.Tasty.QuickCheck (Property, arbitrary, forAll, chooseInt, testProperty, vectorOf)
3322

34-
-- This collects the tests for the various serialization/deserialization pairs.
23+
-- Run tests comparing Bit Machine execution with Simplicity's denotational semantics using both naive and TCO translation.
3524
tests :: TestTree
36-
tests = testGroup "Serialization"
37-
[ testProperty "get-put bit-string" prop_getPutBitString
38-
, testProperty "get-put positive" prop_getPutPositive
39-
, testProperty "get-put BitString DAG" prop_getPutBitStringDag
40-
, testProperty "get-put ByteString DAG" prop_getPutByteStringDag
41-
-- This collection tests type inference on a few sample programs.
42-
, testGroup "Inference"
43-
[ testInference "full_add word8" (Arith.full_add word8)
44-
, testInference "add word8" (Arith.add word8)
45-
, testInference "full_multiply word8" (Arith.full_multiply word8)
46-
, testInference "multiply word8" (Arith.multiply word8)
47-
, testInference "hashBlock" hashBlock
48-
] ]
49-
50-
-- Check that deserialization of serialization of bit-strings returns the original input.
51-
prop_getPutBitString :: [Bool] -> Bool
52-
prop_getPutBitString l = evalExactVector getBitString (UV.fromList (putBitString l [])) == Just l
53-
54-
-- Check that deserialization of serialization of positive numbers returns the original input.
55-
prop_getPutPositive :: Positive Integer -> Bool
56-
prop_getPutPositive (Positive n) = evalExactVector getPositive (UV.fromList (putPositive n [])) == Just n
57-
58-
-- Test a 'SimplicityDag' predicate over suitable Arbitrary inputs.
59-
forallSimplicityDag :: Testable prop => (SimplicityDag [] Ty (SomeArrow NoJets) UntypedValue -> prop) -> Property
60-
forallSimplicityDag = forAll gen_UntypedTermF_list
25+
tests = testGroup "Bitcoin Serialization"
26+
[ testGroup "Haskell"
27+
[ testDecodeBitcoinJet jt | SomeArrow jt@(Bitcoin.BitcoinJet _) <- toList Bitcoin.jetMap ]
28+
, testGroup "C"
29+
$ [ testDecodeBitcoinJetFFI jt | SomeArrow jt <- toList Bitcoin.jetMap ]
30+
++ [ testProperty "prop_wordCMR" prop_wordCMR ]
31+
]
32+
33+
testDecodeBitcoinJet :: (TyC a, TyC b) => Bitcoin.JetType a b -> TestTree
34+
testDecodeBitcoinJet jt = testCase (show jt) (Just (SomeArrow jt) @=? decode)
6135
where
62-
gen_UntypedTermF_list = do
63-
l <- traverse f =<< (zip [1..] <$> listOf1 gen_UntypedTermF)
64-
case l of
65-
[] -> return []
66-
nl -> (:nl) <$> elements [Iden one, Unit one]
67-
where
68-
f (i, term) = traverse (const (choose (1,i))) term
69-
-- We are subverting putDag's type annotation requirement. It is for purpose of testing the 'putDag' function, so maybe it is okay to do.
70-
-- :TODO: replace this with a proper generator for well-typed Simplicity terms.
71-
gen_UntypedTermF :: Gen (TermF Ty j UntypedValue ())
72-
gen_UntypedTermF = oneof
73-
[ pure $ Iden one
74-
, pure $ Unit one
75-
, pure $ Injl one one one ()
76-
, pure $ Injr one one one ()
77-
, pure $ Take one one one ()
78-
, pure $ Drop one one one ()
79-
, pure $ Comp one one one () ()
80-
, pure $ Case one one one one () ()
81-
, pure $ Pair one one one () ()
82-
, pure $ Disconnect one one one one () ()
83-
, Hidden <$> get256Bits arbitrary
84-
, wit
85-
]
86-
where
87-
-- Here we are careful to place a correct type annotation for witness values.
88-
wit = do
89-
b <- arbTy
90-
v <- case reflect b of SomeTy rb -> untypedValue <$> arbValueR rb
91-
return (Witness one b v)
36+
vector = V.fromList $ Bitcoin.putJetBit jt []
37+
decode = evalExactVector (Bitcoin.getJetBit mzero) vector
9238

93-
-- Compare 'SimplicityDag' disregarding most type annotations.
94-
-- Witness nodes are compared using the 'compareWitness' function which may or may not consider type annotations.
95-
compareDag :: (Eq a, Eq j) => (ty0 -> w0 -> ty1 -> w1 -> Bool) -> [TermF ty0 j w0 a] -> [TermF ty1 j w1 a] -> Bool
96-
compareDag compareWitness v1 v2 = (and $ zipWith compareNode v1 v2) && (length v1 == length v2)
39+
testDecodeBitcoinJetFFI :: (TyC a, TyC b) => Bitcoin.JetType a b -> TestTree
40+
testDecodeBitcoinJetFFI jt = testCase (show jt) (Right cmr @=? Bitcoin.decodeJetCMR bitstream)
9741
where
98-
compareNode (Iden _) (Iden _) = True
99-
compareNode (Unit _) (Unit _) = True
100-
compareNode (Injl _ _ _ x0) (Injl _ _ _ x1) = x0 == x1
101-
compareNode (Injr _ _ _ x0) (Injr _ _ _ x1) = x0 == x1
102-
compareNode (Take _ _ _ x0) (Take _ _ _ x1) = x0 == x1
103-
compareNode (Drop _ _ _ x0) (Drop _ _ _ x1) = x0 == x1
104-
compareNode (Comp _ _ _ x0 y0) (Comp _ _ _ x1 y1) = [x0,y0] == [x1,y1]
105-
compareNode (Case _ _ _ _ x0 y0) (Case _ _ _ _ x1 y1) = [x0,y0] == [x1,y1]
106-
compareNode (Pair _ _ _ x0 y0) (Pair _ _ _ x1 y1) = [x0,y0] == [x1,y1]
107-
compareNode (Disconnect _ _ _ _ x0 y0) (Disconnect _ _ _ _ x1 y1) = [x0,y0] == [x1,y1]
108-
compareNode (Hidden h0) (Hidden h1) = h0 == h1
109-
compareNode (Witness _ b0 w0) (Witness _ b1 w1) = compareWitness b0 w0 b1 w1
110-
compareNode (Jet j0) (Jet j1) = j0 == j1
111-
compareNode _ _ = False
42+
-- All jet encodings should begin with a 1 bit, which we consume.
43+
True:bitstream = Bitcoin.putJetBit jt []
44+
cmr = commitmentRoot (asJet jt)
11245

113-
-- Check that 'BitString.putDag's serialization of 'SimplicityDag's works can be deserialized by a combination of 'BitString.getDagNoWitness' and 'BitString.getWitnessData'.
114-
-- Note: Because we do not yet have a generator for arbitrary well-typed Simplicity expressions we cannot easily test 'BitString.putTerm' with 'BitString.getTerm'.
115-
-- Instead we perform an awkward combinator of 'BitString.getDagNoWitness' and 'BitString.getWitnessData' on mostly untyped Simplicity DAGs for now.
116-
prop_getPutBitStringDag :: Property
117-
prop_getPutBitStringDag = forallSimplicityDag prop
46+
prop_wordCMR :: SomeConstWordContent -> Property
47+
prop_wordCMR (SomeConstWordContent cwc) = forAll prefix prop
11848
where
119-
compareWitness _ w0 _ w1 = w0 == w1
120-
prop :: SimplicityDag [] Ty (SomeArrow NoJets) UntypedValue -> Result
121-
prop v = case eval of
122-
Left msg -> failed { reason = show msg }
123-
Right (pdag, wdag) | not (compareDag (\_ _ _ _ -> True) v (toList pdag)) -> failed { reason = "Bitstring.getDagNoWiness returned bad value" }
124-
| not (compareDag compareWitness v (toList wdag)) -> failed { reason = "Bitstring.getWitnessData returned bad value" }
125-
| otherwise -> succeeded
49+
prefix = do
50+
n <- chooseInt (0, 7)
51+
vectorOf n arbitrary
52+
prop l = wordCMR == computeWordCMR (length l) (l ++ stream)
12653
where
127-
pbs = BitString.putDagNoWitnessLengthCode v
128-
Just wbs = BitString.putWitnessData v -- generation is designed to create terms that always succeed at serializaiton.
129-
evalPDag = flip evalStreamWithError pbs $ \abort next -> do
130-
BitString.getDagNoWitnessLengthCode abort next
131-
evalWDag = flip evalStreamWithError wbs $ \abort next -> do
132-
BitString.getWitnessData vStripped next
133-
eval = (,) <$> evalPDag <*> evalWDag
134-
vStripped = v & traverse . witness_ .~ ()
135-
where
136-
witness_ :: Traversal (TermF ty j w0 a) (TermF ty j w1 a) w0 w1
137-
witness_ = witnessData . const
138-
139-
-- Check that deserialization of serialization of 'SimplicityDag's works for the byte-string serialization.
140-
prop_getPutByteStringDag :: Property
141-
prop_getPutByteStringDag = forallSimplicityDag prop
142-
where
143-
compareWitness b w0 _ w1 = case reflect b of
144-
SomeTy rb -> fromMaybe False $ (==) <$> castUntypedValueR rb w0 <*> evalExactVector (getValueR rb) w1
145-
prop v = case runGetState (toList <$> ByteString.getDag) bs 0 of
146-
Left _ -> False
147-
Right (v', rest) -> rest == mempty && compareDag compareWitness v (v' :: SimplicityDag [] () (SomeArrow NoJets) (UV.Vector Bool))
148-
where
149-
Just bs = runPut <$> ByteString.putDag v -- generation is designed to create terms that always succeed at serializaiton.
150-
151-
-- Check that type inference on Simplicity expressions produce correct terms by testing their Merkle roots.
152-
testInference :: forall a b. (TyC a, TyC b) => String -> (forall term. (Core term) => term a b) -> TestTree
153-
testInference name program = testGroup name [testProperty "CommitmentRoot" assertion1, testProperty "AnnotatedRoot" assertion2]
154-
where
155-
dag :: NoJetDag a b
156-
dag = program
157-
-- type inference on first pass is not necessarily equal to the original program because the Haskell type of internal nodes in the original program might not have the term's principle type.
158-
pass1 :: forall term. Simplicity term => Either String (term a b)
159-
pass1 = typeCheck =<< typeInference dag (jetDag dag)
160-
-- Type inference on the second pass ought to always be equal to the first pass.
161-
pass2 :: forall term. Simplicity term => Either String (term a b)
162-
pass2 = typeCheck =<< (typeInference dag . jetDag) =<< (pass1 :: Either String (NoJetDag a b))
163-
assertion1 = pass1 == Right (program :: CommitmentRoot a b)
164-
assertion2 = pass2 == (pass1 :: Either String (AnnotatedRoot a b))
54+
wordCMR = commitmentRoot $ asJet (ConstWordJet cwc)
55+
stream = putConstWordValueBit cwc

‎Haskell/Tests/Simplicity/Elements/Serialization/Tests.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ import Test.Tasty.QuickCheck (Property, arbitrary, forAll, chooseInt, testProper
2222

2323
-- Run tests comparing Bit Machine execution with Simplicity's denotational semantics using both naive and TCO translation.
2424
tests :: TestTree
25-
tests = testGroup "Serialization"
25+
tests = testGroup "Elements Serialization"
2626
[ testGroup "Haskell"
2727
[ testDecodeElementsJet jt | SomeArrow jt@(ElementsJet _) <- toList Elements.jetMap ]
2828
, testGroup "C"

0 commit comments

Comments
 (0)