diff --git a/Haskell-Generate/GenPrimitive.hs b/Haskell-Generate/GenPrimitive.hs
index 827e90bcd..c238355eb 100644
--- a/Haskell-Generate/GenPrimitive.hs
+++ b/Haskell-Generate/GenPrimitive.hs
@@ -13,18 +13,18 @@ import Numeric (showHex)
 
 import NameWrangler
 import Simplicity.Digest
-import Simplicity.Elements.Jets
-import Simplicity.Elements.Term
+import qualified Simplicity.Elements.Jets as Elements
 import Simplicity.MerkleRoot
 import Simplicity.Serialization
 import Simplicity.Ty
 import Simplicity.Weight
 
-jetList :: [SomeArrow JetType]
-jetList = sortBy (compare `on` name) $ Map.elems jetMap
- where
-  name :: SomeArrow JetType -> String
-  name (SomeArrow j) = mkName j
+data JetInfo = JetInfo { name :: String
+                       , cmr :: Hash256
+                       , mw :: Integer
+                       , sourceType :: Ty
+                       , targetType :: Ty
+                       }
 
 data CompactTy = CTyOne
                | CTyWord Int
@@ -83,29 +83,25 @@ cInitializeTy ty = showString "(*bound_var)[" . compactCName ty
                          . showString "], &(*bound_var)[" . compactCName y
                          . showString "] } }"
 
-cJetNode :: (TyC x, TyC y) => String -> JetType x y -> String
-cJetNode name jt = unlines
-  [ "[" ++ upperSnakeCase name ++ "] ="
+cJetNode :: JetInfo -> String
+cJetNode ji = unlines
+  [ "[" ++ upperSnakeCase (name ji) ++ "] ="
   , "{ .tag = JET"
-  , ", .jet = simplicity_" ++ lowerSnakeCase name
-  , ", .cmr = {{" ++ showCHash (commitmentRoot (asJet jt)) ++ "}}"
-  , ", .sourceIx = " ++ compactCName (compactTy (unreflect tyx)) ""
-  , ", .targetIx = " ++ compactCName (compactTy (unreflect tyy)) ""
-  , ", .cost = " ++ show (milliWeight (jetCost jt)) ++ " /* milli weight units */"
+  , ", .jet = simplicity_" ++ lowerSnakeCase (name ji)
+  , ", .cmr = {{" ++ showCHash (cmr ji) ++ "}}"
+  , ", .sourceIx = " ++ compactCName (compactTy (sourceType ji)) ""
+  , ", .targetIx = " ++ compactCName (compactTy (targetType ji)) ""
+  , ", .cost = " ++ show (mw ji) ++ " /* milli weight units */"
   , "}"
   ]
- where
-  (tyx, tyy) = reifyArrow jt
 
-tyList :: [CompactTy]
-tyList = Map.keys . foldr combine wordMap $ (tys =<< jetList)
+mkTyList :: [JetInfo] -> [CompactTy]
+mkTyList jetList = Map.keys . foldr combine wordMap $ (tys =<< jetList)
  where
   wordMap = Map.fromList [(CTyWord n, ty) | (n, ty) <- Prelude.take 32 words]
    where
     words = (1, sum one one) : [(2*n, prod ty ty) | (n, ty) <- words]
-  tys (SomeArrow jet) = [unreflect x, unreflect y]
-   where
-    (x,y) = reifyArrow jet
+  tys ji = [sourceType ji, targetType ji]
   combine ty map | isJust (Map.lookup cTy map) = map
                  | otherwise = Map.insert cTy ty (foldr combine map (children ty))
    where
@@ -114,35 +110,51 @@ tyList = Map.keys . foldr combine wordMap $ (tys =<< jetList)
     children (Fix (Sum x y)) = [x,y]
     children (Fix (Prod x y)) = [x,y]
 
-cEnumTyFile :: String
-cEnumTyFile = unlines . fmap item $ tyList
+cEnumTyFile :: [CompactTy] -> String
+cEnumTyFile tyList = unlines . fmap item $ tyList
  where
   item ty@CTyOne = compactCName ty " = 0,"
   item ty@(CTyWord n) = compactCName ty " = " ++ show (1 + ln n) ++ ","
   item ty = compactCName ty ","
   ln n = length . Prelude.drop 1 . takeWhile (0 <) $ iterate (`div` 2) n
 
-cInitializeTyFile :: String
-cInitializeTyFile = unlines $ cInitializeTy <$> tyList
+cInitializeTyFile :: [CompactTy] -> String
+cInitializeTyFile tyList = unlines $ cInitializeTy <$> tyList
 
-cEnumJetFile :: String
-cEnumJetFile = unlines $ map f jetList
+cEnumJetFile :: [JetInfo] -> String
+cEnumJetFile jetList = unlines $ map f jetList
  where
-  f :: SomeArrow JetType -> String
-  f (SomeArrow jet) = (upperSnakeCase . mkName $ jet) ++ ","
+  f ji = (upperSnakeCase (name ji)) ++ ","
 
-cJetNodeFile :: String
-cJetNodeFile = intercalate "," $ map f jetList
- where
-  f (SomeArrow jet) = cJetNode (mkName jet) jet
+cJetNodeFile :: [JetInfo] -> String
+cJetNodeFile jetList = intercalate "," $ map cJetNode jetList
 
 writeIncludeFile :: FilePath -> String -> IO ()
 writeIncludeFile name content = writeFile name (header ++ content)
  where
   header = "/* This file has been automatically generated. */\n"
 
+mkJetList :: (a -> JetInfo) -> [a] -> [JetInfo]
+mkJetList f l = sortBy (compare `on` name) . map f $ l
+
+writeFiles list = do
+  writeIncludeFile ("primitiveEnumTy.inc") (cEnumTyFile tyList)
+  writeIncludeFile ("primitiveInitTy.inc") (cInitializeTyFile tyList)
+  writeIncludeFile ("primitiveEnumJet.inc") (cEnumJetFile list)
+  writeIncludeFile ("primitiveJetNode.inc") (cJetNodeFile list)
+ where
+  tyList = mkTyList list
+
 main = do
-  writeIncludeFile "primitiveEnumTy.inc" cEnumTyFile
-  writeIncludeFile "primitiveInitTy.inc" cInitializeTyFile
-  writeIncludeFile "primitiveEnumJet.inc" cEnumJetFile
-  writeIncludeFile "primitiveJetNode.inc" cJetNodeFile
+  writeFiles elementsJetList
+ where
+  elementsJetList = mkJetList fromElements $ Map.elems Elements.jetMap
+  fromElements :: SomeArrow Elements.JetType -> JetInfo
+  fromElements (SomeArrow jt) = JetInfo { name = mkName jt
+                                        , cmr = commitmentRoot (Elements.asJet jt)
+                                        , mw = milliWeight (Elements.jetCost jt)
+                                        , sourceType = unreflect tyx
+                                        , targetType = unreflect tyy
+                                        }
+   where
+    (tyx, tyy) = reifyArrow jt
diff --git a/Haskell/Bitcoin/Simplicity/Bitcoin/DataTypes.hs b/Haskell/Bitcoin/Simplicity/Bitcoin/DataTypes.hs
index 05dedb2b9..8a2b1525a 100644
--- a/Haskell/Bitcoin/Simplicity/Bitcoin/DataTypes.hs
+++ b/Haskell/Bitcoin/Simplicity/Bitcoin/DataTypes.hs
@@ -1,28 +1,40 @@
 -- | This module defines the data structures that make up the signed data in a Bitcoin transaction.
 module Simplicity.Bitcoin.DataTypes
   ( Script, Lock, Value
-  , Outpoint(Outpoint), opHash, opIndex
-  , SigTxInput(SigTxInput), sigTxiPreviousOutpoint, sigTxiValue, sigTxiSequence, sigTxiAnnex, sigTxiScriptSig
+  , Outpoint(Outpoint), opHash, opIndex, putOutpointBE
+  , SigTxInput(SigTxInput), sigTxiPreviousOutpoint, sigTxiTxo, sigTxiSequence, sigTxiAnnex, sigTxiScriptSig, sigTxiValue, sigTxiScript
   , TxOutput(TxOutput), txoValue, txoScript
   , SigTx(SigTx), sigTxVersion, sigTxIn, sigTxOut, sigTxLock
+  , putNoWitnessTx, txid
   , TapEnv(..)
+  , txTotalInputValue, txTotalOutputValue, txFee
   , txIsFinal, txLockDistance, txLockDuration
+  , outputValuesHash, outputScriptsHash
+  , outputsHash, outputHash
+  , inputOutpointsHash, inputValuesHash, inputScriptsHash, inputUtxosHash
+  , inputSequencesHash, inputAnnexesHash, inputScriptSigsHash, inputsHash, inputHash
+  , txHash
+  , tapleafHash, tappathHash, tapEnvHash
+  , taptweak
   , module Simplicity.Bitcoin
   ) where
 
 import Control.Monad (guard)
 import qualified Data.ByteString as BS
 import qualified Data.ByteString.Lazy as BSL
-import Data.Semigroup (Max(Max,getMax))
+import Data.Semigroup (Max(Max,getMax), Sum(Sum,getSum))
 import Data.Word (Word64, Word32, Word16, Word8)
 import Data.Serialize ( Serialize
                       , Get, get, getWord8, getWord16le, getWord32le, getWord64le, getLazyByteString
-                      , Put, put, putWord8, putWord16le, putWord32le, putWord64le, putLazyByteString, runPutLazy
+                      , Putter, put, putWord8, putWord16le, putWord32be, putWord32le, putWord64be, putWord64le, putLazyByteString, runPutLazy
                       )
+import Data.String (fromString)
 import Data.Vector (Vector)
+import qualified Data.Vector as V
 
 import Simplicity.Bitcoin
 import Simplicity.Digest
+import Simplicity.LibSecp256k1.Spec
 import Simplicity.LibSecp256k1.Schnorr
 
 {-
@@ -84,15 +96,28 @@ instance Serialize Outpoint where
   get = Outpoint <$> get <*> getWord32le
   put (Outpoint h i) = put h >> putWord32le i
 
+-- | Big endian serialization of an 'Outpoint'
+putOutpointBE :: Putter Outpoint
+putOutpointBE op = put (opHash op)
+                >> putWord32be (opIndex op)
+
 -- | The data type for signed transaction inputs.
 -- Note that signed transaction inputs for BIP 143 include the value of the input, which doesn't appear in the serialized transaction input format.
 data SigTxInput = SigTxInput { sigTxiPreviousOutpoint :: Outpoint
-                             , sigTxiValue :: Value
+                             , sigTxiTxo :: TxOutput
                              , sigTxiSequence :: Word32
                              , sigTxiAnnex :: Maybe BSL.ByteString
                              , sigTxiScriptSig :: Script -- length must be strictly less than 2^32.
                              } deriving Show
 
+-- | The value of the input being spent.
+sigTxiValue :: SigTxInput -> Value
+sigTxiValue = txoValue . sigTxiTxo
+
+-- | The value of the input being spent.
+sigTxiScript :: SigTxInput -> Script
+sigTxiScript = txoScript . sigTxiTxo
+
 {-
 instance Serialize SigTxInput where
   get = SigTxInput <$> get <*> getValue <*> getWord32le
@@ -132,6 +157,15 @@ data TapEnv = TapEnv { tapleafVersion :: Word8
                      , tapScriptCMR :: Hash256
                      } deriving Show
 
+txTotalInputValue :: SigTx -> Value
+txTotalInputValue tx = getSum . foldMap (Sum . sigTxiValue) $ sigTxIn tx
+
+txTotalOutputValue :: SigTx -> Value
+txTotalOutputValue tx = getSum . foldMap (Sum . txoValue) $ sigTxOut tx
+
+txFee :: SigTx -> Value
+txFee tx = txTotalInputValue tx - txTotalOutputValue tx
+
 txIsFinal :: SigTx -> Bool
 txIsFinal tx = all finalSequence (sigTxIn tx)
  where
@@ -152,3 +186,188 @@ txLockDuration tx | sigTxVersion tx < 2 = 0
   duration sigin = case parseSequence (sigTxiSequence sigin) of
                      Just (Right x) -> Max x
                      _ -> mempty
+
+-- | A hash of all 'txoValues's.
+outputValuesHash :: SigTx -> Hash256
+outputValuesHash tx = bslHash . runPutLazy $ mapM_ (putWord64be . txoValue) (sigTxOut tx)
+
+-- | A hash of all 'txoScript' hashes.
+outputScriptsHash :: SigTx -> Hash256
+outputScriptsHash tx = bslHash . runPutLazy $ mapM_ (put . bslHash . txoScript) (sigTxOut tx)
+
+-- | A hash of
+--
+-- * 'outputValuesHash'
+-- * 'outputScriptsHash'
+outputsHash :: SigTx -> Hash256
+outputsHash tx = bslHash . runPutLazy $ do
+                   put $ outputValuesHash tx
+                   put $ outputScriptsHash tx
+
+-- | A hash of one output's
+--
+-- * value
+-- * hash of its script
+outputHash :: TxOutput -> Hash256
+outputHash txo = bslHash . runPutLazy $ do
+                   putWord64be $ txoValue txo
+                   put . bslHash $ txoScript txo
+
+-- | Serialize an input's previous output including whether the previous input is from an pegin or not, and which parent chain if it is a pegin.
+putOutpoint :: Putter SigTxInput
+putOutpoint txi = putOutpointBE (sigTxiPreviousOutpoint txi)
+
+-- | A hash of all 'sigTxiPreviousOutpoint's.
+inputOutpointsHash :: SigTx -> Hash256
+inputOutpointsHash tx = bslHash . runPutLazy $ mapM_ putOutpoint (sigTxIn tx)
+
+-- | A hash of all 'utxoValue's.
+inputValuesHash :: SigTx -> Hash256
+inputValuesHash tx = bslHash . runPutLazy $ mapM_ (putWord64be . sigTxiValue) (sigTxIn tx)
+
+-- | A hash of all 'utxoScript' hashes.
+inputScriptsHash :: SigTx -> Hash256
+inputScriptsHash tx = bslHash . runPutLazy $ mapM_ (put . bslHash . sigTxiScript) (sigTxIn tx)
+
+-- | A hash of
+--
+-- * 'inputValuesHash'
+-- * 'inputScriptsHash'
+inputUtxosHash :: SigTx -> Hash256
+inputUtxosHash tx = bslHash . runPutLazy $ do
+                      put $ inputValuesHash tx
+                      put $ inputScriptsHash tx
+
+-- | A hash of all 'sigTxiSequence's.
+inputSequencesHash :: SigTx -> Hash256
+inputSequencesHash tx = bslHash . runPutLazy $ mapM_ (putWord32be . sigTxiSequence) (sigTxIn tx)
+
+putAnnex :: Putter (Maybe BSL.ByteString)
+putAnnex Nothing = putWord8 0x00
+putAnnex (Just annex) = putWord8 0x01 >> put (bslHash annex)
+
+-- | A hash of all 'sigTxiAnnex' hashes.
+inputAnnexesHash :: SigTx -> Hash256
+inputAnnexesHash tx = bslHash . runPutLazy $ mapM_ (putAnnex . sigTxiAnnex) (sigTxIn tx)
+
+-- | A hash of all 'sigTxiScriptSig' hashes.
+inputScriptSigsHash :: SigTx -> Hash256
+inputScriptSigsHash tx = bslHash . runPutLazy $ mapM_ (put . bslHash . sigTxiScriptSig) (sigTxIn tx)
+
+-- | A hash of
+--
+-- * 'inputOutpointsHash'
+-- * 'inputSequencesHash'
+-- * 'inputAnnexesHash'
+--
+-- Note that 'inputScriptSigsHash' is excluded.
+inputsHash :: SigTx -> Hash256
+inputsHash tx = bslHash . runPutLazy $ do
+                  put $ inputOutpointsHash tx
+                  put $ inputSequencesHash tx
+                  put $ inputAnnexesHash tx
+
+-- | A hash of
+--
+-- * The inputs's outpoint (including if and where the pegin came from)
+-- * The inputs's sequence number
+-- * Whether or not the input has an annex and the hash of that annex.
+inputHash :: SigTxInput -> Hash256
+inputHash txi = bslHash . runPutLazy $ do
+                  putOutpoint txi
+                  putWord32be $ sigTxiSequence txi
+                  putAnnex $ sigTxiAnnex txi
+
+-- | A hash of
+--
+-- * 'sigTxVersion'
+-- * 'sigTxLock'
+-- * 'inputsHash'
+-- * 'outputsHash'
+-- * 'inputUtxosHash'
+txHash :: SigTx -> Hash256
+txHash tx = bslHash . runPutLazy $ do
+              putWord32be $ sigTxVersion tx
+              putWord32be $ sigTxLock tx
+              put $ inputsHash tx
+              put $ outputsHash tx
+              put $ inputUtxosHash tx
+
+-- | Serialize transaction data without witness data.
+-- Mainly suitable for computing a 'txid'.
+putNoWitnessTx :: Putter SigTx
+putNoWitnessTx tx = do
+  putWord32le $ sigTxVersion tx
+  putVarInt (V.length (sigTxIn tx))
+  mapM_ putInput (sigTxIn tx)
+  putVarInt (V.length (sigTxOut tx))
+  mapM_ putOutput (sigTxOut tx)
+  putWord32le $ sigTxLock tx
+ where
+  putVarInt x | x < 0 = error "putVarInt: negative value"
+              | x <= 0xFC = putWord8 (fromIntegral x)
+              | x <= 0xFFFF = putWord8 0xFD >> putWord16le (fromIntegral x)
+              | x <= 0xFFFFFFFF = putWord8 0xFE >> putWord32le (fromIntegral x)
+              | x <= 0xFFFFFFFFFFFFFFFF = putWord8 0xFF >> putWord64le (fromIntegral x)
+  putInput txi = do
+    put (opHash (sigTxiPreviousOutpoint txi))
+    putWord32le (opIndex (sigTxiPreviousOutpoint txi))
+    putVarInt (BSL.length (sigTxiScriptSig txi))
+    putLazyByteString (sigTxiScriptSig txi)
+    putWord32le (sigTxiSequence txi)
+
+  putOutput txo = do
+    putWord64le (txoValue txo)
+    putVarInt (BSL.length (txoScript txo))
+    putLazyByteString (txoScript txo)
+
+-- | Return the txid of the transaction.
+txid :: SigTx -> Hash256
+txid = bslDoubleHash . runPutLazy . putNoWitnessTx
+
+-- | A hash of
+--
+-- * 'tapleafVersion'
+-- * 'tapScriptCMR'
+tapleafHash :: TapEnv -> Hash256
+tapleafHash tapEnv = bslHash . runPutLazy $ do
+  put tag
+  put tag
+  putWord8 $ tapleafVersion tapEnv
+  putWord8 32
+  put $ tapScriptCMR tapEnv
+ where
+  tag = bsHash (fromString "TapLeaf")
+
+-- | A hash of 'tappath's.
+tappathHash :: TapEnv -> Hash256
+tappathHash tapEnv = bslHash . runPutLazy $ mapM_ put (tappath tapEnv)
+
+-- | A hash of
+--
+-- * 'tapleafHash'
+-- * 'tappathHash'
+-- * 'tapInternalKey'
+tapEnvHash :: TapEnv -> Hash256
+tapEnvHash tapEnv = bslHash . runPutLazy $ do
+              put $ tapleafHash tapEnv
+              put $ tappathHash tapEnv
+              put $ tapInternalKey tapEnv
+
+-- | Implementation of BIP-0341's taptweak function.
+taptweak :: PubKey -> Hash256 -> Maybe PubKey
+taptweak (PubKey internalKey) h = do
+  guard $ toInteger internalKey < fieldOrder
+  guard $ h0 < groupOrder
+  a <- scale (scalar h0) g
+  b <- decompress (Point False xkey)
+  GE x y <- gej_normalize . snd $ gej_ge_add_ex a b
+  return $ PubKey (fe_pack x)
+ where
+  xkey = fe (toInteger internalKey)
+  h0 = integerHash256 . bslHash . runPutLazy $ do
+    put tag
+    put tag
+    put (fe_pack xkey)
+    put h
+  tag = bsHash (fromString "TapTweak")
diff --git a/Haskell/Bitcoin/Simplicity/Bitcoin/Primitive.hs b/Haskell/Bitcoin/Simplicity/Bitcoin/Primitive.hs
index 6988d4594..db60f5a13 100644
--- a/Haskell/Bitcoin/Simplicity/Bitcoin/Primitive.hs
+++ b/Haskell/Bitcoin/Simplicity/Bitcoin/Primitive.hs
@@ -2,7 +2,7 @@
 -- | This module provides the Simplicity primitives specific for Bitcoin or Bitcoin-like applications.
 module Simplicity.Bitcoin.Primitive
   ( Prim(..), primPrefix, primName
-  , PrimEnv(..), primEnv
+  , PrimEnv(..), primEnv, primEnvHash
   , primSem
   -- * Re-exported Types
   , PubKey
@@ -11,7 +11,7 @@ module Simplicity.Bitcoin.Primitive
 import qualified Data.List as List
 import Data.Maybe (listToMaybe)
 import Data.Serialize (Get, getWord8,
-                       Putter, put, putWord8, putWord32le, putWord64le, runPutLazy)
+                       Putter, put, putWord8, putWord32be, putWord32le, putWord64le, runPutLazy)
 import qualified Data.Word
 import Data.Vector as Vector ((!?), length)
 
@@ -26,40 +26,38 @@ import Simplicity.Ty.Word
 data Prim a b where
   Version :: Prim () Word32
   LockTime :: Prim () Word32
-  TotalInputValue :: Prim () Word64
   CurrentIndex :: Prim () Word32
-  InputPrevOutpoint :: Prim Word32 (Either () (Word256,Word32))
-  InputValue :: Prim Word32 (Either () Word64)
-  InputSequence :: Prim Word32 (Either () Word32)
-  InputAnnexHash :: Prim Word32 (Either () (Either () Word256))
-  InputScriptSigHash :: Prim Word32 (Either () Word256)
-  TotalOutputValue :: Prim () Word64
-  OutputValue :: Prim Word32 (Either () Word64)
-  OutputScriptHash :: Prim Word32 (Either () Word256)
+  InputPrevOutpoint :: Prim Word32 (S (Word256,Word32))
+  InputValue :: Prim Word32 (S Word64)
+  InputScriptHash :: Prim Word32 (S Word256)
+  InputSequence :: Prim Word32 (S Word32)
+  InputAnnexHash :: Prim Word32 (S (S Word256))
+  InputScriptSigHash :: Prim Word32 (S Word256)
+  OutputValue :: Prim Word32 (S Word64)
+  OutputScriptHash :: Prim Word32 (S Word256)
   TapleafVersion :: Prim () Word8
-  Tappath :: Prim Word8 (Either () Word256)
+  Tappath :: Prim Word8 (S Word256)
   InternalKey :: Prim () PubKey
   ScriptCMR :: Prim () Word256
--- Other possible ideas:
-  -- TxId :: Prim () Word256
+  TransactionId :: Prim () Word256
 
 instance Eq (Prim a b) where
   Version == Version = True
   LockTime == LockTime = True
-  TotalInputValue == TotalInputValue = True
   CurrentIndex == CurrentIndex = True
   InputPrevOutpoint == InputPrevOutpoint = True
   InputValue == InputValue = True
+  InputScriptHash == InputScriptHash = True
   InputSequence == InputSequence = True
   InputAnnexHash == InputAnnexHash = True
   InputScriptSigHash == InputScriptSigHash = True
-  TotalOutputValue == TotalOutputValue = True
   OutputValue == OutputValue = True
   OutputScriptHash == OutputScriptHash = True
   TapleafVersion == TapleafVersion = True
   Tappath == Tappath = True
   InternalKey == InternalKey = True
   ScriptCMR == ScriptCMR = True
+  TransactionId == TransactionId = True
   _ == _ = False
 
 primPrefix :: String
@@ -69,20 +67,20 @@ primPrefix = "Bitcoin"
 primName :: Prim a b -> String
 primName Version = "version"
 primName LockTime = "lockTime"
-primName TotalInputValue = "totalInputValue"
 primName CurrentIndex = "currentIndex"
 primName InputPrevOutpoint = "inputPrevOutpoint"
 primName InputValue = "inputValue"
+primName InputScriptHash = "inputScriptHash"
 primName InputSequence = "inputSequence"
 primName InputAnnexHash = "inputAnnexHash"
 primName InputScriptSigHash = "inputScriptSigHash"
-primName TotalOutputValue = "totalOutputValue"
 primName OutputValue = "outputValue"
 primName OutputScriptHash = "outputScriptHash"
 primName TapleafVersion = "tapleafVersion"
 primName Tappath = "tappath"
 primName InternalKey = "internalKey"
 primName ScriptCMR = "scriptCMR"
+primName TransactionId = "transactionId"
 
 data PrimEnv = PrimEnv { envTx :: SigTx
                        , envIx :: Data.Word.Word32
@@ -107,6 +105,19 @@ primEnv tx ix tap | cond = Just $ PrimEnv { envTx = tx
  where
   cond = fromIntegral ix < Vector.length (sigTxIn tx)
 
+-- | A hash of
+--
+-- * 'txHash'
+-- * 'tapEnvHash'
+-- * 'envIx'
+--
+-- Note: this is the hash used for the "sig-all" hash.
+primEnvHash :: PrimEnv -> Hash256
+primEnvHash env = bslHash . runPutLazy $ do
+                    put $ txHash (envTx env)
+                    put $ tapEnvHash (envTap env)
+                    putWord32be $ envIx env
+
 primSem :: Prim a b -> a -> PrimEnv -> Maybe b
 primSem p a env = interpret p a
  where
@@ -131,17 +142,17 @@ primSem p a env = interpret p a
   encodeKey (Schnorr.PubKey x) = toWord256 . toInteger $ x
   interpret Version = element . return . toWord32 . toInteger $ sigTxVersion tx
   interpret LockTime = element . return . toWord32 . toInteger $ sigTxLock tx
-  interpret TotalInputValue = element . return . toWord64 . fromIntegral . List.sum $ sigTxiValue <$> sigTxIn tx
   interpret CurrentIndex = element . return . toWord32 . toInteger $ ix
   interpret InputPrevOutpoint = return . (atInput $ encodeOutpoint . sigTxiPreviousOutpoint)
   interpret InputValue = return . (atInput $ toWord64 . toInteger . sigTxiValue)
+  interpret InputScriptHash = return . (atInput $ encodeHash . bslHash . sigTxiScript)
   interpret InputSequence = return . (atInput $ toWord32 . toInteger . sigTxiSequence)
   interpret InputAnnexHash = return . (atInput $ cast . fmap (encodeHash . bslHash) . sigTxiAnnex)
   interpret InputScriptSigHash = return . (atInput $ encodeHash . bslHash . sigTxiScriptSig)
-  interpret TotalOutputValue = element . return . toWord64 . fromIntegral . List.sum $ txoValue <$> sigTxOut tx
   interpret OutputValue = return . (atOutput $ toWord64 . fromIntegral . txoValue)
   interpret OutputScriptHash = return . (atOutput $ encodeHash . bslHash . txoScript)
   interpret TapleafVersion = element . return . toWord8 . toInteger . tapleafVersion $ envTap env
   interpret Tappath = return . cast . fmap encodeHash . listToMaybe . flip drop (tappath (envTap env)) . fromInteger . fromWord8
   interpret InternalKey = element . return . encodeKey . tapInternalKey $ envTap env
   interpret ScriptCMR = element . return . toWord256 . integerHash256 . tapScriptCMR $ envTap env
+  interpret TransactionId = element . return . encodeHash . txid $ tx
diff --git a/Haskell/Core/Simplicity/Programs/Bitcoin.hs b/Haskell/Core/Simplicity/Programs/Bitcoin.hs
new file mode 100644
index 000000000..e6ac1b07b
--- /dev/null
+++ b/Haskell/Core/Simplicity/Programs/Bitcoin.hs
@@ -0,0 +1,126 @@
+{-# LANGUAGE ScopedTypeVariables, GADTs, RankNTypes, RecordWildCards #-}
+-- | This module defines Simplicity expressions that implement pure calculations used by Bitcoin.
+module Simplicity.Programs.Bitcoin
+  ( Lib(Lib), mkLib
+  , buildTapleafSimplicity, buildTapbranch
+  , LibAssert(LibAssert), mkLibAssert
+  , outpointHash, annexHash
+  , buildTaptweak
+  -- * Example instances
+  , lib, libAssert
+  -- * Reexports
+  , Hash, Ctx8
+  ) where
+
+import Prelude hiding (Word, drop, not, subtract, take)
+import Data.String (fromString)
+import Lens.Family2 (over, review)
+
+import Simplicity.Digest
+import Simplicity.Functor
+import Simplicity.LibSecp256k1.Spec (fieldOrder, groupOrder)
+import Simplicity.Programs.Bit
+import Simplicity.Programs.Generic
+import Simplicity.Programs.Arith
+import Simplicity.Programs.Word
+import Simplicity.Term.Core hiding (one)
+import qualified Simplicity.Programs.LibSecp256k1 as LibSecp256k1
+import Simplicity.Programs.LibSecp256k1 hiding (Lib(Lib), mkLib, lib)
+import qualified Simplicity.Programs.Sha256 as Sha256
+import Simplicity.Programs.Sha256 hiding ( Lib(Lib), lib
+                                         , LibAssert(LibAssert), mkLibAssert, libAssert)
+
+-- | A collection of core Simplicity expressions for Bitcoin calculations.
+-- Use 'mkLib' to construct an instance of this library.
+data Lib term =
+ Lib
+  { buildTapleafSimplicity :: term Hash Hash
+
+    -- | Compute a tapbranch hash from two branches.
+  , buildTapbranch :: term (Hash, Hash) Hash
+  }
+
+-- | A collection of Simplicity with Assertions expressions for Bitcoin calculations.
+-- Use 'mkLibAssert' to construct an instance of this library.
+data LibAssert term =
+ LibAssert
+  { -- | A hash of an outpoint.
+    outpointHash :: term (Ctx8, (Word256, Word32)) Ctx8
+    -- | A hash of an optional hash.
+  , annexHash :: term (Ctx8, S Word256) Ctx8
+    -- | Compute a taptweak hash from a pubkey and a hash.
+  , buildTaptweak :: term (PubKey, Hash) PubKey
+  }
+
+instance SimplicityFunctor Lib where
+  sfmap m Lib{..} =
+   Lib
+    { buildTapleafSimplicity = m buildTapleafSimplicity
+    , buildTapbranch = m buildTapbranch
+    }
+
+instance SimplicityFunctor LibAssert where
+  sfmap m LibAssert{..} =
+   LibAssert
+    { outpointHash = m outpointHash
+    , annexHash = m annexHash
+    , buildTaptweak = m buildTaptweak
+    }
+
+-- | Build the Bitcoin 'Lib' library from its dependencies.
+mkLib :: forall term. Core term => Sha256.Lib term -- ^ "Simplicity.Programs.Sha256"
+                                -> Lib term
+mkLib Sha256.Lib{..} = lib
+ where
+  lib@Lib{..} = Lib {
+    buildTapleafSimplicity = (unit >>> tapleafPrefix)
+                         &&& ((unit >>> (simplicityVersion &&& scribe (toWord8 32))) &&& iden >>> full_shift word16 word256 >>>
+                              (oh &&& ((((ih &&& (unit >>> scribe (toWord16 0x8000))) &&& (unit >>> zero word32)) &&& (unit >>> zero word64)) &&& (unit >>> scribe (toWord128 (512+16+256))))))
+                         >>> hashBlock
+  , buildTapbranch = ((unit >>> tapbranchPrefix)
+                 &&& (lt word256 &&& iden >>> cond iden (ih &&& oh))
+                 >>> hashBlock)
+                 &&& (unit >>> scribe (toWord512 $ 2^511 + 1024)) >>> hashBlock
+  } where
+    tapleafPrefix = scribe . toWord256 . integerHash256 . ivHash . tagIv $ fromString "TapLeaf"
+    tapbranchPrefix = scribe . toWord256 . integerHash256 . ivHash . tagIv $ fromString "TapBranch"
+    simplicityVersion = scribe . toWord8 $ 0xbe
+
+-- | An instance of the Bitcoin 'Lib' library.
+-- This instance does not share its dependencies.
+-- Users should prefer to use 'mkLib' in order to share library dependencies.
+-- This instance is provided mostly for testing purposes.
+lib :: Core term => Lib term
+lib = mkLib Sha256.lib
+
+-- | Build the Bitcoin 'LibAssert' library.
+mkLibAssert :: forall term. Assert term => Sha256.Lib term -- ^ "Simplicity.Programs.Sha256"
+                                        -> Sha256.LibAssert term -- ^ "Simplicity.Programs.Sha256"
+                                        -> LibSecp256k1.Lib term -- ^ "Simplicity.Programs.Libsecp256k1"
+                                        -> LibAssert term
+mkLibAssert Sha256.Lib{..} Sha256.LibAssert{..} LibSecp256k1.Lib{..} = libAssert
+ where
+  libAssert@LibAssert{..} = LibAssert {
+    outpointHash = (oh &&& ioh >>> ctx8Add32) &&& iih >>> ctx8Add4
+  , annexHash = ih &&& oh
+            >>> match (ih &&& take (zero word8) >>> ctx8Add1)
+                      ((ih &&& (unit >>> scribe (toWord8 0x01)) >>> ctx8Add1) &&& oh >>> ctx8Add32)
+  , buildTaptweak = assert (
+                  (((assert (oh &&& (unit >>> scribe (toWord256 fieldOrder)) >>> lt256) >>> taptweakPrefix) &&& iden >>> hashBlock)
+                &&& (unit >>> scribe (toWord512 $ 2^511 + 1024)) >>> hashBlock >>>
+                   (assert (iden &&& (unit >>> scribe (toWord256 groupOrder)) >>> lt256) &&& iden) >>> drop generate)
+                &&& assert ((unit >>> false) &&& oh >>> decompress)
+                >>> gej_ge_add >>> gej_normalize) >>> oh
+  } where
+    lt256 = lt word256
+    ctx8Add32 = ctx8Addn vector32
+    ctx8Add8 = ctx8Addn vector8
+    ctx8Add4 = ctx8Addn vector4
+    taptweakPrefix = scribe . toWord256 . integerHash256 . ivHash . tagIv $ fromString "TapTweak"
+
+-- | An instance of the Bitcoin 'LibAssert' library.
+-- This instance does not share its dependencies.
+-- Users should prefer to use 'mkLibAssert' in order to share library dependencies.
+-- This instance is provided mostly for testing purposes.
+libAssert :: Assert term => LibAssert term
+libAssert = mkLibAssert Sha256.lib Sha256.libAssert LibSecp256k1.lib
diff --git a/Haskell/Core/Simplicity/Programs/Bitcoin/Lib.hs b/Haskell/Core/Simplicity/Programs/Bitcoin/Lib.hs
new file mode 100644
index 000000000..9cbac6e00
--- /dev/null
+++ b/Haskell/Core/Simplicity/Programs/Bitcoin/Lib.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+-- | This module unpacks the 'Simplicity.Programs.Bitcoin.lib' library instance into individual functions.
+-- Users should prefer to use 'Simplicity.Programs.Bitcoin.mkLib' in order to share library dependencies.
+-- This module is provided mostly for testing purposes.
+module Simplicity.Programs.Bitcoin.Lib
+  ( buildTapleafSimplicity, buildTapbranch
+  , outpointHash, annexHash
+  , buildTaptweak
+  , Bitcoin.Hash, Bitcoin.Ctx8
+  ) where
+
+import qualified Simplicity.Programs.Bitcoin as Bitcoin
+
+-- Maybe this ought to be Template Haskell.
+buildTapleafSimplicity = Bitcoin.buildTapleafSimplicity Bitcoin.lib
+buildTapbranch = Bitcoin.buildTapbranch Bitcoin.lib
+outpointHash = Bitcoin.outpointHash Bitcoin.libAssert
+annexHash = Bitcoin.annexHash Bitcoin.libAssert
+buildTaptweak = Bitcoin.buildTaptweak Bitcoin.libAssert
diff --git a/Haskell/Core/Simplicity/Ty/Sha256.hs b/Haskell/Core/Simplicity/Ty/Sha256.hs
new file mode 100644
index 000000000..848932740
--- /dev/null
+++ b/Haskell/Core/Simplicity/Ty/Sha256.hs
@@ -0,0 +1,27 @@
+-- | This modules provides some functions for mashalling data to and from Simplicity types that are used for some SHA-256 operations.
+module Simplicity.Ty.Sha256
+ ( fromHash
+ , fromCtx8, toCtx8
+ , Ctx, Ctx8
+ ) where
+
+import qualified Data.ByteString as BS
+import Lens.Family2 ((^..), over, review)
+
+import Simplicity.Digest
+import Simplicity.Programs.Sha256
+import Simplicity.Ty.Word
+
+fromHash :: Hash -> Hash256
+fromHash = review (over be256) . fromIntegral . fromWord256
+
+fromCtx8 :: Ctx8 -> Maybe Ctx
+fromCtx8 (buffer, (count, midstate)) = ctxBuild (fromInteger . fromWord8 <$> buffer^..buffer_ buffer63)
+                                               (fromWord64 count)
+                                               (fromHash midstate)
+toCtx8 :: Ctx -> Ctx8
+toCtx8 ctx = (buffer, (count, midstate))
+ where
+  buffer = fst $ bufferFill buffer63 (toWord8 . fromIntegral <$> BS.unpack (ctxBuffer ctx))
+  count = toWord64 . fromIntegral $ ctxCounter ctx
+  midstate = toWord256 . integerHash256 . ivHash $ ctxIV ctx
diff --git a/Haskell/Simplicity/Bitcoin/Jets.hs b/Haskell/Simplicity/Bitcoin/Jets.hs
index 7a65249e8..585bdf558 100644
--- a/Haskell/Simplicity/Bitcoin/Jets.hs
+++ b/Haskell/Simplicity/Bitcoin/Jets.hs
@@ -1,7 +1,8 @@
 -- | This module provides a canonical set of known jets for Simplicity for Bitcoin. (At the moment this just consists of 'CoreJet's.)
 {-# LANGUAGE GADTs, StandaloneDeriving, TypeFamilies #-}
 module Simplicity.Bitcoin.Jets
-  ( JetType(..)
+  ( JetType(..), BitcoinJet(..), SigHashJet(..), TimeLockJet(..), TransactionJet(..)
+  , bitcoinCatalogue
   , asJet
   , jetSubst, pruneSubst
   , getTermLengthCode, putTermLengthCode
@@ -18,10 +19,16 @@ module Simplicity.Bitcoin.Jets
 import Prelude hiding (fail, drop, take)
 
 import Control.Applicative ((<|>))
+import Control.Monad (guard)
+import Data.Foldable (toList)
 import qualified Data.Map as Map
 import Data.Proxy (Proxy(Proxy))
 import Data.Type.Equality ((:~:)(Refl))
+import Data.Serialize (runPut, put, putWord8)
+import Data.String (fromString)
+import Data.Vector ((!?))
 import Data.Void (Void, vacuous)
+import Lens.Family2 ((^..), over, review)
 
 import Simplicity.Digest
 import Simplicity.CoreJets (CoreJet, coreJetMap, ConstWordContent(..), SomeConstWordContent(..))
@@ -31,20 +38,26 @@ import qualified Simplicity.Bitcoin.Dag as Dag
 import Simplicity.Bitcoin.Term
 import Simplicity.Bitcoin.DataTypes
 import qualified Simplicity.Bitcoin.JetType
-import Simplicity.Bitcoin.Primitive (PrimEnv, envTx, PubKey)
+import Simplicity.Bitcoin.Primitive (PrimEnv, PubKey, primEnvHash, envTx, envTap)
 import qualified Simplicity.Bitcoin.Primitive as Prim
 import qualified Simplicity.Bitcoin.Serialization.BitString as BitString
 import qualified Simplicity.Bitcoin.Semantics as Semantics
+import qualified Simplicity.Bitcoin.Programs.SigHash.Lib as SigHash
 import qualified Simplicity.Bitcoin.Programs.TimeLock as TimeLock
 import qualified Simplicity.Bitcoin.Programs.Transaction.Lib as Prog
+import qualified Simplicity.LibSecp256k1.Schnorr as Schnorr
 import Simplicity.MerkleRoot
+import Simplicity.Programs.Sha256.Lib (Ctx8)
+import qualified Simplicity.Programs.Bitcoin.Lib as Prog
 import Simplicity.Programs.Word
 import Simplicity.Serialization
 import Simplicity.Tensor
 import Simplicity.Tree
 import Simplicity.Ty
 import Simplicity.Ty.Bit
+import Simplicity.Ty.Sha256
 import Simplicity.Ty.Word
+import qualified Simplicity.Word as W
 
 -- | A type of tokens for the canonical set of known jets for Simplicity for Bitcoin. (At the moment this just consists of 'CoreJet's.)
 --
@@ -57,11 +70,40 @@ deriving instance Eq (JetType a b)
 deriving instance Show (JetType a b)
 
 data BitcoinJet a b where
+  SigHashJet :: SigHashJet a b -> BitcoinJet a b
   TimeLockJet :: TimeLockJet a b -> BitcoinJet a b
   TransactionJet :: TransactionJet a b -> BitcoinJet a b
 deriving instance Eq (BitcoinJet a b)
 deriving instance Show (BitcoinJet a b)
 
+data SigHashJet a b where
+  SigAllHash :: SigHashJet () Word256
+  TxHash :: SigHashJet () Word256
+  TapEnvHash :: SigHashJet () Word256
+  OutputsHash :: SigHashJet () Word256
+  InputsHash :: SigHashJet () Word256
+  InputUtxosHash :: SigHashJet () Word256
+  OutputHash :: SigHashJet Word32 (S Word256)
+  OutputValuesHash :: SigHashJet () Word256
+  OutputScriptsHash :: SigHashJet () Word256
+  InputHash :: SigHashJet Word32 (S Word256)
+  InputOutpointsHash :: SigHashJet () Word256
+  InputSequencesHash :: SigHashJet () Word256
+  InputAnnexesHash :: SigHashJet () Word256
+  InputScriptSigsHash :: SigHashJet () Word256
+  InputUtxoHash :: SigHashJet Word32 (S Word256)
+  InputValuesHash :: SigHashJet () Word256
+  InputScriptsHash :: SigHashJet () Word256
+  TapleafHash :: SigHashJet () Word256
+  TappathHash :: SigHashJet () Word256
+  OutpointHash :: SigHashJet (Ctx8, (Word256, Word32)) Ctx8
+  AnnexHash :: SigHashJet (Ctx8, S Word256) Ctx8
+  BuildTapleafSimplicity :: SigHashJet Word256 Word256
+  BuildTapbranch :: SigHashJet (Word256, Word256) Word256
+  BuildTaptweak :: SigHashJet (PubKey, Word256) PubKey
+deriving instance Eq (SigHashJet a b)
+deriving instance Show (SigHashJet a b)
+
 data TimeLockJet a b where
   CheckLockHeight :: TimeLockJet TimeLock.Height ()
   CheckLockTime :: TimeLockJet TimeLock.Time ()
@@ -82,16 +124,19 @@ data TransactionJet a b where
   NumInputs :: TransactionJet () Word32
   NumOutputs :: TransactionJet () Word32
   LockTime :: TransactionJet () Word32
+  Fee :: TransactionJet () Word64
   OutputValue :: TransactionJet Word32 (Either () Word64)
   OutputScriptHash :: TransactionJet Word32 (Either () Word256)
   TotalOutputValue :: TransactionJet () Word64
   CurrentPrevOutpoint :: TransactionJet () (Word256,Word32)
   CurrentValue :: TransactionJet () Word64
+  CurrentScriptHash :: TransactionJet () Word256
   CurrentSequence :: TransactionJet () Word32
   CurrentAnnexHash :: TransactionJet () (Either () Word256)
   CurrentScriptSigHash :: TransactionJet () Word256
   InputPrevOutpoint :: TransactionJet Word32 (Either () (Word256,Word32))
   InputValue :: TransactionJet Word32 (Either () Word64)
+  InputScriptHash :: TransactionJet Word32 (S Word256)
   InputSequence :: TransactionJet Word32 (Either () Word32)
   InputAnnexHash :: TransactionJet Word32 (Either () (Either () Word256))
   InputScriptSigHash :: TransactionJet Word32 (Either () Word256)
@@ -99,14 +144,41 @@ data TransactionJet a b where
   TapleafVersion :: TransactionJet () Word8
   Tappath :: TransactionJet Word8 (Either () Word256)
   Version :: TransactionJet () Word32
-
+  TransactionId :: TransactionJet () Word256
 deriving instance Eq (TransactionJet a b)
 deriving instance Show (TransactionJet a b)
 
 specificationBitcoin :: (Assert term, Primitive term) => BitcoinJet a b -> term a b
+specificationBitcoin (SigHashJet x) = specificationSigHash x
 specificationBitcoin (TimeLockJet x) = specificationTimeLock x
 specificationBitcoin (TransactionJet x) = specificationTransaction x
 
+specificationSigHash :: (Assert term, Primitive term) => SigHashJet a b -> term a b
+specificationSigHash SigAllHash = SigHash.sigAllHash
+specificationSigHash TxHash = SigHash.txHash
+specificationSigHash TapEnvHash = SigHash.tapEnvHash
+specificationSigHash OutputsHash = SigHash.outputsHash
+specificationSigHash InputsHash = SigHash.inputsHash
+specificationSigHash InputUtxosHash = SigHash.inputUtxosHash
+specificationSigHash OutputHash = SigHash.outputHash
+specificationSigHash OutputValuesHash = SigHash.outputValuesHash
+specificationSigHash OutputScriptsHash = SigHash.outputScriptsHash
+specificationSigHash InputHash = SigHash.inputHash
+specificationSigHash InputOutpointsHash = SigHash.inputOutpointsHash
+specificationSigHash InputSequencesHash = SigHash.inputSequencesHash
+specificationSigHash InputAnnexesHash = SigHash.inputAnnexesHash
+specificationSigHash InputScriptSigsHash = SigHash.inputScriptSigsHash
+specificationSigHash InputUtxoHash = SigHash.inputUtxoHash
+specificationSigHash InputValuesHash = SigHash.inputValuesHash
+specificationSigHash InputScriptsHash = SigHash.inputScriptsHash
+specificationSigHash TapleafHash = SigHash.tapleafHash
+specificationSigHash TappathHash = SigHash.tappathHash
+specificationSigHash OutpointHash = Prog.outpointHash
+specificationSigHash AnnexHash = Prog.annexHash
+specificationSigHash BuildTapleafSimplicity = Prog.buildTapleafSimplicity
+specificationSigHash BuildTapbranch = Prog.buildTapbranch
+specificationSigHash BuildTaptweak = Prog.buildTaptweak
+
 specificationTimeLock :: (Assert term, Primitive term) => TimeLockJet a b -> term a b
 specificationTimeLock CheckLockHeight = TimeLock.checkLockHeight
 specificationTimeLock CheckLockTime = TimeLock.checkLockTime
@@ -127,37 +199,112 @@ specificationTransaction NumOutputs = Prog.numOutputs
 specificationTransaction LockTime = primitive Prim.LockTime
 specificationTransaction OutputValue = primitive Prim.OutputValue
 specificationTransaction OutputScriptHash = primitive Prim.OutputScriptHash
-specificationTransaction TotalOutputValue = primitive Prim.TotalOutputValue
+specificationTransaction TotalOutputValue = Prog.totalOutputValue
 specificationTransaction CurrentPrevOutpoint = Prog.currentPrevOutpoint
 specificationTransaction CurrentValue = Prog.currentValue
+specificationTransaction CurrentScriptHash = Prog.currentScriptHash
 specificationTransaction CurrentSequence = Prog.currentSequence
 specificationTransaction CurrentAnnexHash = Prog.currentAnnexHash
 specificationTransaction CurrentScriptSigHash = Prog.currentScriptSigHash
 specificationTransaction InputPrevOutpoint = primitive Prim.InputPrevOutpoint
 specificationTransaction InputValue = primitive Prim.InputValue
+specificationTransaction InputScriptHash = primitive Prim.InputScriptHash
 specificationTransaction InputSequence = primitive Prim.InputSequence
 specificationTransaction InputAnnexHash = primitive Prim.InputAnnexHash
 specificationTransaction InputScriptSigHash = primitive Prim.InputScriptSigHash
-specificationTransaction TotalInputValue = primitive Prim.TotalInputValue
+specificationTransaction TotalInputValue = Prog.totalInputValue
+specificationTransaction Fee = Prog.fee
 specificationTransaction TapleafVersion = primitive Prim.TapleafVersion
 specificationTransaction Tappath = primitive Prim.Tappath
 specificationTransaction Version = primitive Prim.Version
+specificationTransaction TransactionId = primitive Prim.TransactionId
 
 implementationBitcoin :: BitcoinJet a b -> PrimEnv -> a -> Maybe b
+implementationBitcoin (SigHashJet x) = implementationSigHash x
 implementationBitcoin (TimeLockJet x) = implementationTimeLock x
 implementationBitcoin (TransactionJet x) = implementationTransaction x
 
+implementationSigHash :: SigHashJet a b -> PrimEnv -> a -> Maybe b
+implementationSigHash SigAllHash env _ = Just . toWord256 . integerHash256 $ primEnvHash env
+implementationSigHash TxHash env _ = Just . toWord256 . integerHash256 $ txHash (envTx env)
+implementationSigHash TapEnvHash env _ = Just . toWord256 . integerHash256 $ tapEnvHash (envTap env)
+implementationSigHash OutputsHash env _ = Just . toWord256 . integerHash256 $ outputsHash (envTx env)
+implementationSigHash InputsHash env _ = Just . toWord256 . integerHash256 $ inputsHash (envTx env)
+implementationSigHash InputUtxosHash env _ = Just . toWord256 . integerHash256 $ inputUtxosHash (envTx env)
+implementationSigHash OutputHash env i = Just . fmap (toWord256 . integerHash256 . outputHash) . maybe (Left ()) Right
+                                       $ sigTxOut (envTx env) !? (fromIntegral $ fromWord32 i)
+implementationSigHash OutputValuesHash env _ = Just . toWord256 . integerHash256 $ outputValuesHash (envTx env)
+implementationSigHash OutputScriptsHash env _ = Just . toWord256 . integerHash256 $ outputScriptsHash (envTx env)
+implementationSigHash InputHash env i = Just . fmap (toWord256 . integerHash256 . inputHash) . maybe (Left ()) Right
+                                      $ sigTxIn (envTx env) !? (fromIntegral $ fromWord32 i)
+implementationSigHash InputOutpointsHash env _ = Just . toWord256 . integerHash256 $ inputOutpointsHash (envTx env)
+implementationSigHash InputSequencesHash env _ = Just . toWord256 . integerHash256 $ inputSequencesHash (envTx env)
+implementationSigHash InputAnnexesHash env _ = Just . toWord256 . integerHash256 $ inputAnnexesHash (envTx env)
+implementationSigHash InputScriptSigsHash env _ = Just . toWord256 . integerHash256 $ inputScriptSigsHash (envTx env)
+implementationSigHash InputUtxoHash env i = Just . fmap (toWord256 . integerHash256 . outputHash . sigTxiTxo) . maybe (Left ()) Right
+                                          $ sigTxIn (envTx env) !? (fromIntegral $ fromWord32 i)
+implementationSigHash InputValuesHash env _ = Just . toWord256 . integerHash256 $ inputValuesHash (envTx env)
+implementationSigHash InputScriptsHash env _ = Just . toWord256 . integerHash256 $ inputScriptsHash (envTx env)
+implementationSigHash TapleafHash env _ = Just . toWord256 . integerHash256 $ tapleafHash (envTap env)
+implementationSigHash TappathHash env _ = Just . toWord256 . integerHash256 $ tappathHash (envTap env)
+implementationSigHash OutpointHash _env (ctx, op) = toCtx8 <$> (flip ctxAdd (runPut (putOutpointBE (cast op))) =<< fromCtx8 ctx)
+ where
+  cast (h, i) = Outpoint (review (over be256) (fromW256 h)) (fromW32 i)
+  fromW256 = fromIntegral . fromWord256
+  fromW32 = fromIntegral . fromWord32
+implementationSigHash AnnexHash _env (ctx, mw256) = toCtx8 <$> (flip ctxAdd (runPut . putMW256 $ mw256) =<< fromCtx8 ctx)
+ where
+  putMW256 (Left _) = putWord8 0x00
+  putMW256 (Right w256) = putWord8 0x01 >> put (fromIntegral (fromWord256 w256) :: W.Word256)
+implementationSigHash BuildTapleafSimplicity _env cmr = Just . toWord256 . integerHash256 . bsHash . runPut
+                                                      $ put tag >> put tag >> putWord8 tapleafSimplicityVersion >> putWord8 32 >> put (fromW256 cmr)
+ where
+  tag = bsHash (fromString "TapLeaf")
+  tapleafSimplicityVersion = 0xbe
+  fromW256 :: Word256 -> W.Word256
+  fromW256 = fromIntegral . fromWord256
+
+implementationSigHash BuildTapbranch _env (wa,wb) = Just . toWord256 . integerHash256 . bsHash . runPut
+                                                  $ put tag >> put tag >> put min >> put max
+ where
+  a = fromW256 wa
+  b = fromW256 wb
+  min = if a < b then a else b
+  max = if a < b then b else a
+  tag = bsHash (fromString "TapBranch")
+  fromW256 :: Word256 -> W.Word256
+  fromW256 = fromIntegral . fromWord256
+implementationSigHash BuildTaptweak _env (key,h) = cast <$> taptweak pk h0
+ where
+  pk = Schnorr.PubKey (fromW256 key)
+  h0 = review (over be256) (fromW256 h)
+  cast (Schnorr.PubKey k) = toWord256 . toInteger $ k
+  fromW256 :: Word256 -> W.Word256
+  fromW256 = fromIntegral . fromWord256
+
 implementationTimeLock :: TimeLockJet a b -> PrimEnv -> a -> Maybe b
+implementationTimeLock CheckLockHeight env x | txIsFinal (envTx env) = guard $ fromWord32 x <= 0
+                                             | Left l <- parseLock lock = guard $ fromWord32 x <= fromIntegral l
+                                             | otherwise = guard $ fromWord32 x <= 0
+ where
+  lock = fromIntegral . sigTxLock . envTx $ env
+implementationTimeLock CheckLockTime env x | txIsFinal (envTx env) = guard $ fromWord32 x <= 0
+                                           | Right l <- parseLock lock = guard $ fromWord32 x <= fromIntegral l
+                                           | otherwise = guard $ fromWord32 x <= 0
+ where
+  lock = fromIntegral . sigTxLock . envTx $ env
 implementationTimeLock CheckLockDistance env x | fromWord16 x <= fromIntegral (txLockDistance (envTx env)) = Just ()
                                                | otherwise = Nothing
 implementationTimeLock CheckLockDuration env x | fromWord16 x <= fromIntegral (txLockDuration (envTx env)) = Just ()
                                                | otherwise = Nothing
-implementationTimeLock TxLockHeight env () | txIsFinal (envTx env) && lock < 500000000 = Just . toWord32 . fromIntegral . sigTxLock . envTx $ env
+implementationTimeLock TxLockHeight env () | txIsFinal (envTx env) = Just (toWord32 0)
+                                           | Left l <- parseLock lock = Just . toWord32 $ fromIntegral l
                                            | otherwise = Just (toWord32 0)
  where
   lock = fromIntegral . sigTxLock . envTx $ env
-implementationTimeLock TxLockTime env () | txIsFinal (envTx env) && 500000000 <= lock = Just . toWord32 . fromIntegral . sigTxLock . envTx $ env
-                                           | otherwise = Just (toWord32 0)
+implementationTimeLock TxLockTime env () | txIsFinal (envTx env) = Just (toWord32 0)
+                                         | Right l <- parseLock lock = Just . toWord32 $ fromIntegral l
+                                         | otherwise = Just (toWord32 0)
  where
   lock = fromIntegral . sigTxLock . envTx $ env
 implementationTimeLock TxLockDistance env () = Just . toWord16 . fromIntegral $ txLockDistance (envTx env)
@@ -165,70 +312,128 @@ implementationTimeLock TxLockDuration env () = Just . toWord16 . fromIntegral $
 implementationTimeLock TxIsFinal env () = Just $ toBit (txIsFinal (envTx env))
 
 implementationTransaction :: TransactionJet a b -> PrimEnv -> a -> Maybe b
+implementationTransaction TotalOutputValue env _ = Just . toWord64 . fromIntegral $ txTotalOutputValue (envTx env)
+implementationTransaction TotalInputValue env _ = Just . toWord64 . fromIntegral $ txTotalInputValue (envTx env)
+implementationTransaction Fee env _ = Just . toWord64 . fromIntegral $ txFee (envTx env)
 implementationTransaction x env i = Semantics.sem (specificationTransaction x) env i
 
 getJetBitBitcoin :: (Monad m) => m Void -> m Bool -> m (SomeArrow BitcoinJet)
 getJetBitBitcoin = getCatalogue bitcoinCatalogue
- where
-  bitcoinCatalogue = Shelf
-   [ Missing
-   , someArrowMap TimeLockJet <$> timeLockCatalogue
-   , someArrowMap TransactionJet <$> transactionCatalogue
-   ]
-  timeLockCatalogue = book
-   [ SomeArrow CheckLockHeight
-   , SomeArrow CheckLockTime
-   , SomeArrow CheckLockDistance
-   , SomeArrow CheckLockDuration
-   , SomeArrow TxLockHeight
-   , SomeArrow TxLockTime
-   , SomeArrow TxLockDistance
-   , SomeArrow TxLockDuration
-   , SomeArrow TxIsFinal
-   ]
-  transactionCatalogue = Shelf
-   [ Item $ SomeArrow ScriptCMR
-   , Item $ SomeArrow InternalKey
-   , Item $ SomeArrow CurrentIndex
-   , Item $ SomeArrow NumInputs
-   , Item $ SomeArrow NumOutputs
-   , Item $ SomeArrow LockTime
-   , Missing
-   , Item $ SomeArrow OutputValue
-   , Item $ SomeArrow OutputScriptHash
-   , Item $ SomeArrow TotalOutputValue
-   , Item $ SomeArrow CurrentPrevOutpoint
-   , Item $ SomeArrow CurrentValue
-   , Missing
-   , Item $ SomeArrow CurrentSequence
-   , Item $ SomeArrow CurrentAnnexHash
-   , Item $ SomeArrow CurrentScriptSigHash
-   , Item $ SomeArrow InputPrevOutpoint
-   , Item $ SomeArrow InputValue
-   , Missing
-   , Item $ SomeArrow InputSequence
-   , Item $ SomeArrow InputAnnexHash
-   , Item $ SomeArrow InputScriptSigHash
-   , Item $ SomeArrow TotalInputValue
-   , Item $ SomeArrow TapleafVersion
-   , Item $ SomeArrow Tappath
-   , Item $ SomeArrow Version
-   ]
+
+bitcoinCatalogue :: Catalogue (SomeArrow BitcoinJet)
+bitcoinCatalogue = Shelf
+ [ someArrowMap SigHashJet <$> sigHashCatalogue
+ , someArrowMap TimeLockJet <$> timeLockCatalogue
+ , someArrowMap TransactionJet <$> transactionCatalogue
+ ]
+sigHashCatalogue = book
+ [ SomeArrow SigAllHash
+ , SomeArrow TxHash
+ , SomeArrow TapEnvHash
+ , SomeArrow OutputsHash
+ , SomeArrow InputsHash
+ , SomeArrow InputUtxosHash
+ , SomeArrow OutputHash
+ , SomeArrow OutputValuesHash
+ , SomeArrow OutputScriptsHash
+ , SomeArrow InputHash
+ , SomeArrow InputOutpointsHash
+ , SomeArrow InputSequencesHash
+ , SomeArrow InputAnnexesHash
+ , SomeArrow InputScriptSigsHash
+ , SomeArrow InputUtxoHash
+ , SomeArrow InputValuesHash
+ , SomeArrow InputScriptsHash
+ , SomeArrow TapleafHash
+ , SomeArrow TappathHash
+ , SomeArrow OutpointHash
+ , SomeArrow AnnexHash
+ , SomeArrow BuildTapleafSimplicity
+ , SomeArrow BuildTapbranch
+ , SomeArrow BuildTaptweak
+ ]
+timeLockCatalogue = book
+ [ SomeArrow CheckLockHeight
+ , SomeArrow CheckLockTime
+ , SomeArrow CheckLockDistance
+ , SomeArrow CheckLockDuration
+ , SomeArrow TxLockHeight
+ , SomeArrow TxLockTime
+ , SomeArrow TxLockDistance
+ , SomeArrow TxLockDuration
+ , SomeArrow TxIsFinal
+ ]
+transactionCatalogue = book
+ [ SomeArrow ScriptCMR
+ , SomeArrow InternalKey
+ , SomeArrow CurrentIndex
+ , SomeArrow NumInputs
+ , SomeArrow NumOutputs
+ , SomeArrow LockTime
+ , SomeArrow Fee
+ , SomeArrow OutputValue
+ , SomeArrow OutputScriptHash
+ , SomeArrow TotalOutputValue
+ , SomeArrow CurrentPrevOutpoint
+ , SomeArrow CurrentValue
+ , SomeArrow CurrentScriptHash
+ , SomeArrow CurrentSequence
+ , SomeArrow CurrentAnnexHash
+ , SomeArrow CurrentScriptSigHash
+ , SomeArrow InputPrevOutpoint
+ , SomeArrow InputValue
+ , SomeArrow InputScriptHash
+ , SomeArrow InputSequence
+ , SomeArrow InputAnnexHash
+ , SomeArrow InputScriptSigHash
+ , SomeArrow TotalInputValue
+ , SomeArrow TapleafVersion
+ , SomeArrow Tappath
+ , SomeArrow Version
+ , SomeArrow TransactionId
+ ]
 
 putJetBitBitcoin :: BitcoinJet a b -> DList Bool
+putJetBitBitcoin (SigHashJet x) = putPositive 1 . putJetBitSigHash x
 putJetBitBitcoin (TimeLockJet x) = putPositive 2 . putJetBitTimeLock x
 putJetBitBitcoin (TransactionJet x) = putPositive 3 . putJetBitTransaction x
 
+putJetBitSigHash :: SigHashJet a b -> DList Bool
+putJetBitSigHash SigAllHash             = putPositive 1
+putJetBitSigHash TxHash                 = putPositive 2
+putJetBitSigHash TapEnvHash             = putPositive 3
+putJetBitSigHash OutputsHash            = putPositive 4
+putJetBitSigHash InputsHash             = putPositive 5
+putJetBitSigHash InputUtxosHash         = putPositive 6
+putJetBitSigHash OutputHash             = putPositive 7
+putJetBitSigHash OutputValuesHash       = putPositive 8
+putJetBitSigHash OutputScriptsHash      = putPositive 9
+putJetBitSigHash InputHash              = putPositive 10
+putJetBitSigHash InputOutpointsHash     = putPositive 11
+putJetBitSigHash InputSequencesHash     = putPositive 12
+putJetBitSigHash InputAnnexesHash       = putPositive 13
+putJetBitSigHash InputScriptSigsHash    = putPositive 14
+putJetBitSigHash InputUtxoHash          = putPositive 15
+putJetBitSigHash InputValuesHash        = putPositive 16
+putJetBitSigHash InputScriptsHash       = putPositive 17
+putJetBitSigHash TapleafHash            = putPositive 18
+putJetBitSigHash TappathHash            = putPositive 19
+putJetBitSigHash OutpointHash           = putPositive 20
+putJetBitSigHash AnnexHash              = putPositive 21
+putJetBitSigHash BuildTapleafSimplicity = putPositive 22
+putJetBitSigHash BuildTapbranch         = putPositive 23
+putJetBitSigHash BuildTaptweak          = putPositive 24
+
 putJetBitTimeLock :: TimeLockJet a b -> DList Bool
 putJetBitTimeLock CheckLockHeight   = putPositive 1
 putJetBitTimeLock CheckLockTime     = putPositive 2
 putJetBitTimeLock CheckLockDistance = putPositive 3
 putJetBitTimeLock CheckLockDuration = putPositive 4
-putJetBitTimeLock TxLockHeight   = putPositive 5
-putJetBitTimeLock TxLockTime     = putPositive 6
-putJetBitTimeLock TxLockDistance = putPositive 7
-putJetBitTimeLock TxLockDuration = putPositive 8
-putJetBitTimeLock TxIsFinal      = putPositive 9
+putJetBitTimeLock TxLockHeight      = putPositive 5
+putJetBitTimeLock TxLockTime        = putPositive 6
+putJetBitTimeLock TxLockDistance    = putPositive 7
+putJetBitTimeLock TxLockDuration    = putPositive 8
+putJetBitTimeLock TxIsFinal         = putPositive 9
 
 putJetBitTransaction :: TransactionJet a b -> DList Bool
 putJetBitTransaction ScriptCMR            = putPositive 1
@@ -237,67 +442,33 @@ putJetBitTransaction CurrentIndex         = putPositive 3
 putJetBitTransaction NumInputs            = putPositive 4
 putJetBitTransaction NumOutputs           = putPositive 5
 putJetBitTransaction LockTime             = putPositive 6
-
+putJetBitTransaction Fee                  = putPositive 7
 putJetBitTransaction OutputValue          = putPositive 8
 putJetBitTransaction OutputScriptHash     = putPositive 9
 putJetBitTransaction TotalOutputValue     = putPositive 10
 putJetBitTransaction CurrentPrevOutpoint  = putPositive 11
 putJetBitTransaction CurrentValue         = putPositive 12
-
+putJetBitTransaction CurrentScriptHash    = putPositive 13
 putJetBitTransaction CurrentSequence      = putPositive 14
 putJetBitTransaction CurrentAnnexHash     = putPositive 15
 putJetBitTransaction CurrentScriptSigHash = putPositive 16
 putJetBitTransaction InputPrevOutpoint    = putPositive 17
 putJetBitTransaction InputValue           = putPositive 18
-
+putJetBitTransaction InputScriptHash      = putPositive 19
 putJetBitTransaction InputSequence        = putPositive 20
 putJetBitTransaction InputAnnexHash       = putPositive 21
 putJetBitTransaction InputScriptSigHash   = putPositive 22
 putJetBitTransaction TotalInputValue      = putPositive 23
 putJetBitTransaction TapleafVersion       = putPositive 24
-putJetBitTransaction Tappath            = putPositive 25
+putJetBitTransaction Tappath              = putPositive 25
 putJetBitTransaction Version              = putPositive 26
+putJetBitTransaction TransactionId        = putPositive 27
 
 bitcoinJetMap :: Map.Map Hash256 (SomeArrow BitcoinJet)
-bitcoinJetMap = Map.fromList
-  [ -- TimeLockJet
-    mkAssoc (TimeLockJet CheckLockHeight)
-  , mkAssoc (TimeLockJet CheckLockTime)
-  , mkAssoc (TimeLockJet CheckLockDistance)
-  , mkAssoc (TimeLockJet CheckLockDuration)
-  , mkAssoc (TimeLockJet TxLockHeight)
-  , mkAssoc (TimeLockJet TxLockTime)
-  , mkAssoc (TimeLockJet TxLockDistance)
-  , mkAssoc (TimeLockJet TxLockDuration)
-  , mkAssoc (TimeLockJet TxIsFinal)
-    -- TransactionJet
-  , mkAssoc (TransactionJet ScriptCMR)
-  , mkAssoc (TransactionJet InternalKey)
-  , mkAssoc (TransactionJet CurrentIndex)
-  , mkAssoc (TransactionJet NumInputs)
-  , mkAssoc (TransactionJet NumOutputs)
-  , mkAssoc (TransactionJet LockTime)
-  , mkAssoc (TransactionJet OutputValue)
-  , mkAssoc (TransactionJet OutputScriptHash)
-  , mkAssoc (TransactionJet TotalOutputValue)
-  , mkAssoc (TransactionJet CurrentPrevOutpoint)
-  , mkAssoc (TransactionJet CurrentValue)
-  , mkAssoc (TransactionJet CurrentSequence)
-  , mkAssoc (TransactionJet CurrentAnnexHash)
-  , mkAssoc (TransactionJet CurrentScriptSigHash)
-  , mkAssoc (TransactionJet InputPrevOutpoint)
-  , mkAssoc (TransactionJet InputValue)
-  , mkAssoc (TransactionJet InputSequence)
-  , mkAssoc (TransactionJet InputAnnexHash)
-  , mkAssoc (TransactionJet InputScriptSigHash)
-  , mkAssoc (TransactionJet TotalInputValue)
-  , mkAssoc (TransactionJet TapleafVersion)
-  , mkAssoc (TransactionJet Tappath)
-  , mkAssoc (TransactionJet Version)
-  ]
+bitcoinJetMap = Map.fromList . fmap mkAssoc $ toList bitcoinCatalogue
  where
-  mkAssoc :: (TyC a, TyC b) => BitcoinJet a b -> (Hash256, (SomeArrow BitcoinJet))
-  mkAssoc jt = (identityHash (specificationBitcoin jt), SomeArrow jt)
+  mkAssoc :: SomeArrow BitcoinJet -> (Hash256, (SomeArrow BitcoinJet))
+  mkAssoc wrapped@(SomeArrow jt) = (identityHash (specificationBitcoin jt), wrapped)
 
 data MatcherInfo a b = MatcherInfo (Product ConstWord IdentityRoot a b)
 
@@ -308,6 +479,7 @@ instance Simplicity.Bitcoin.JetType.JetType JetType where
   specification (CoreJet jt) = CoreJets.specification jt
   specification (BitcoinJet jt) = specificationBitcoin jt
 
+  implementation (ConstWordJet cw) _env = CoreJets.implementationConstWord cw
   implementation (CoreJet jt) _env = CoreJets.implementation jt
   implementation (BitcoinJet jt) env = implementationBitcoin jt env
 
diff --git a/Haskell/Simplicity/Bitcoin/Programs/SigHash.hs b/Haskell/Simplicity/Bitcoin/Programs/SigHash.hs
new file mode 100644
index 000000000..1a4e7899d
--- /dev/null
+++ b/Haskell/Simplicity/Bitcoin/Programs/SigHash.hs
@@ -0,0 +1,231 @@
+{-# LANGUAGE ScopedTypeVariables, GADTs, RankNTypes, RecordWildCards #-}
+-- | This module defines Simplicity expressions that implement timelock functions from "Simplicity.Bitcoin.DataTypes".
+module Simplicity.Bitcoin.Programs.SigHash
+ ( Lib(Lib), mkLib
+ , outputValuesHash, outputScriptsHash
+ , outputsHash, outputHash
+ , inputValuesHash, inputScriptsHash, inputUtxosHash, inputUtxoHash
+ , inputOutpointsHash, inputSequencesHash, inputAnnexesHash, inputScriptSigsHash, inputsHash, inputHash
+ , txHash
+ , tapleafHash, tappathHash, tapEnvHash
+ , sigAllHash
+ -- * Example instances
+ , lib
+ ) where
+
+import Prelude hiding (Word, all, drop, max, not, take)
+import Data.String (fromString)
+
+import Simplicity.Digest
+import Simplicity.Bitcoin.Primitive
+import Simplicity.Bitcoin.Term hiding (one)
+import Simplicity.Functor
+import Simplicity.Programs.Arith
+import Simplicity.Programs.Bit
+import Simplicity.Programs.Generic
+import Simplicity.Programs.Word
+import qualified Simplicity.Programs.Sha256 as Sha256
+import Simplicity.Programs.Sha256 (Ctx8)
+import qualified Simplicity.Bitcoin.Programs.Transaction as Transaction
+import Simplicity.Programs.Bitcoin.Lib
+
+data Lib term =
+ Lib
+  { -- | A hash of all 'Transaction.outputValue's.
+    outputValuesHash :: term () Word256
+    -- | A hash of all 'OutputScriptHash's.
+  , outputScriptsHash :: term () Word256
+    -- | A hash of
+    --
+    -- * 'outputValuesHash'
+    -- * 'outputScriptsHash'
+  , outputsHash :: term () Word256
+    -- | If the given output index exists, returns a hash of
+    --
+    -- * The serialization of the output's value fields.
+    -- * A hash of the output's scriptPubKey.
+  , outputHash :: term Word32 (S Word256)
+    -- | A hash of all 'Transaction.inputValue's.
+  , inputValuesHash :: term () Word256
+    -- | A hash of all 'InputScriptHash's.
+  , inputScriptsHash :: term () Word256
+    -- | A hash of
+    --
+    -- * 'inputValuesHash'
+    -- * 'inputScriptsHash'
+  , inputUtxosHash :: term () Word256
+    -- | If the given input index exists, returns a hash of
+    --
+    -- * The serialization of the input UTXO's value field.
+    -- * A hash of the input UTXO's scriptPubKey.
+  , inputUtxoHash :: term Word32 (S Word256)
+    -- | A hash of all 'InputPrevOutpoint's.
+  , inputOutpointsHash :: term () Word256
+    -- | A hash of all 'InputSequence's.
+  , inputSequencesHash :: term () Word256
+    -- | A hash of all 'InputAnnexHash's.
+  , inputAnnexesHash :: term () Word256
+    -- | A hash of all 'InputScriptSigHash's.
+  , inputScriptSigsHash :: term () Word256
+    -- | A hash of
+    --
+    -- * 'inputOutpointsHash'
+    -- * 'inputSequencesHash'
+    -- * 'inputAnnexesHash'
+    --
+    -- Note that 'InputScriptSigHash' is excluded.
+  , inputsHash :: term () Word256
+    -- | If the given input index exists, returns a hash of
+    --
+    -- * The input's serialized previous transaction id.
+    -- * The input's previous transaction index in big endian format.
+    -- * The input's sequence number in big endian format.
+    -- * If the input has no annex, or isn't a taproot spend, then the byte 0x00.
+    -- * If the input has an annex, then the byte 0x01 followed by a SHA256 hash of the annex.
+  , inputHash :: term Word32 (S Word256)
+    -- | A hash of
+    --
+    -- * 'Version'
+    -- * 'LockTime'
+    -- * 'inputsHash'
+    -- * 'outputsHash'
+    -- * 'inputUtxosHash'
+  , txHash :: term () Word256
+    -- | A hash of
+    --
+    -- * 'TapleafVersion'
+    -- * 'ScriptCMR'
+  , tapleafHash :: term () Word256
+    -- | A hash of all 'Tappath's.
+  , tappathHash :: term () Word256
+    -- | A hash of
+    --
+    -- * 'tapleafHash'
+    -- * 'tappathHash'
+    -- * 'InternalKey'
+  , tapEnvHash :: term () Word256
+    -- | A hash of
+    --
+    -- * 'txHash'
+    -- * 'tapEnvHash'
+    -- * 'CurrentIndex'
+  , sigAllHash :: term () Word256
+  }
+
+instance SimplicityFunctor Lib where
+  sfmap m Lib{..} =
+   Lib
+    { outputValuesHash = m outputValuesHash
+    , outputScriptsHash = m outputScriptsHash
+    , outputsHash = m outputsHash
+    , outputHash = m outputHash
+    , inputValuesHash = m inputValuesHash
+    , inputScriptsHash = m inputScriptsHash
+    , inputUtxosHash = m inputUtxosHash
+    , inputUtxoHash = m inputUtxoHash
+    , inputOutpointsHash = m inputOutpointsHash
+    , inputSequencesHash = m inputSequencesHash
+    , inputAnnexesHash = m inputAnnexesHash
+    , inputsHash = m inputsHash
+    , inputHash = m inputHash
+    , inputScriptSigsHash = m inputScriptSigsHash
+    , txHash = m txHash
+    , tapleafHash = m tapleafHash
+    , tappathHash = m tappathHash
+    , tapEnvHash = m tapEnvHash
+    , sigAllHash = m sigAllHash
+    }
+
+mkLib :: forall term. (Assert term, Primitive term) => Sha256.Lib term -- ^ "Simplicity.Programs.Sha256"
+                                                    -> Sha256.LibAssert term -- ^ "Simplicity.Programs.Sha256"
+                                                    -> Transaction.Lib term -- ^ "Simplicity.Bitcoin.Programs.Transaction"
+                                                    -> Lib term
+mkLib Sha256.Lib{..} Sha256.LibAssert{..} Transaction.Lib{..} = lib
+ where
+  lib@Lib{..} = Lib {
+    outputValuesHash = hashWord64s (drop (primitive OutputValue))
+
+  , outputScriptsHash = hashWord256s32 (drop (primitive OutputScriptHash))
+
+  , outputsHash = ctx8Init &&& (outputValuesHash &&& outputScriptsHash) >>> ctx8Add64 >>> ctx8Finalize
+
+  , outputHash = (primitive OutputValue &&& primitive OutputScriptHash)
+             >>> match (injl unit)
+                       (injr (((unit >>> ctx8Init) &&& oh >>> ctx8Add8)
+                         &&& (drop . assert $ iden) >>> ctx8Add32 >>> ctx8Finalize))
+
+  , inputValuesHash = hashWord64s (drop (primitive InputValue))
+
+  , inputScriptsHash = hashWord256s32 (drop (primitive InputScriptHash))
+
+  , inputUtxosHash = ctx8Init &&& (inputValuesHash &&& inputScriptsHash) >>> ctx8Addn vector64 >>> ctx8Finalize
+
+  , inputUtxoHash = (primitive InputValue &&& primitive InputScriptHash)
+             >>> match (injl unit)
+                       (injr (((unit >>> ctx8Init) &&& oh >>> ctx8Add8)
+                         &&& (drop . assert $ iden) >>> ctx8Add32 >>> ctx8Finalize))
+
+  , inputOutpointsHash =
+     let
+      finalize = ctx8Finalize
+      body = (take (drop (primitive InputPrevOutpoint)) &&& ih)
+         >>> match (injl ih) (injr (ih &&& oh >>> outpointHash))
+     in
+      unit &&& ctx8Init >>> forWhile word32 body >>> copair finalize finalize
+
+  , inputSequencesHash = hashWord32s (drop (primitive InputSequence))
+
+  , inputAnnexesHash =
+     let
+      finalize = ctx8Finalize
+      body = take (drop (primitive InputAnnexHash)) &&& ih
+         >>> match (injl ih) (injr (ih &&& oh >>> annexHash))
+     in
+      unit &&& ctx8Init >>> forWhile word32 body >>> copair finalize finalize
+
+  , inputScriptSigsHash = hashWord256s32 (drop (primitive InputScriptSigHash))
+
+  , inputsHash = (ctx8Init &&& (inputOutpointsHash &&& inputSequencesHash) >>> ctx8Addn vector64)
+             &&& inputAnnexesHash >>> ctx8Addn vector32 >>> ctx8Finalize
+
+  , inputHash = (primitive InputPrevOutpoint &&& (primitive InputSequence &&& primitive InputAnnexHash))
+            >>> match (injl unit)
+                      (injr ((((unit >>> ctx8Init) &&& oh >>> outpointHash)
+                    &&& (drop . take . assert $ iden) >>> ctx8Add4)
+                    &&& (drop . drop . assert $ iden) >>> annexHash >>> ctx8Finalize))
+
+  , txHash = ((ctx8Init &&& (primitive Version &&& primitive LockTime) >>> ctx8Addn vector8)
+         &&& (inputsHash &&& outputsHash) >>> ctx8Addn vector64)
+         &&& inputUtxosHash >>> ctx8Addn vector32 >>> ctx8Finalize
+
+  , tapleafHash = ((Sha256.ctx8InitTag "TapLeaf")
+              &&& (primitive TapleafVersion &&& scribe (toWord8 32)) >>> ctx8Addn vector2)
+              &&& (primitive ScriptCMR) >>> ctx8Addn vector32 >>> ctx8Finalize
+
+  , tappathHash = hashWord256s8 (drop (primitive Tappath))
+
+  , tapEnvHash = (ctx8Init &&& tapleafHash >>> ctx8Addn vector32)
+             &&& (tappathHash &&& primitive InternalKey) >>> ctx8Addn vector64 >>> ctx8Finalize
+
+  , sigAllHash = (ctx8Init &&& (txHash &&& tapEnvHash) >>> ctx8Addn vector64)
+             &&& primitive CurrentIndex >>> ctx8Addn vector4 >>> ctx8Finalize
+  }
+  hashLoop256 :: (TyC w, TyC c) => Word w -> term (c, w) (S Word256) -> term (c, Ctx8) Ctx8
+  hashLoop256 = Sha256.hashLoop vector32
+  hashWord256s :: (TyC w, TyC c) => Word w -> term (c, w) (S Word256) -> term c Word256
+  hashWord256s w array = iden &&& (unit >>> ctx8Init) >>> hashLoop256 w array >>> ctx8Finalize
+  hashWord256s32 = hashWord256s word32
+  hashWord256s8 = hashWord256s word8
+  hashWord64s array = iden &&& (unit >>> ctx8Init) >>> Sha256.hashLoop vector8 word32 array >>> ctx8Finalize
+  hashWord32s array = iden &&& (unit >>> ctx8Init) >>> Sha256.hashLoop vector4 word32 array >>> ctx8Finalize
+  ctx8Add4 = ctx8Addn vector4
+  ctx8Add8 = ctx8Addn vector8
+  ctx8Add32 = ctx8Addn vector32
+  ctx8Add64 = ctx8Addn vector64
+
+-- | An instance of the SigHash 'Lib' library.
+-- This instance does not share its dependencies.
+-- Users should prefer to use 'mkLib' in order to share library dependencies.
+-- This instance is provided mostly for testing purposes.
+lib :: (Assert term, Primitive term) => Lib term
+lib = mkLib Sha256.lib Sha256.libAssert Transaction.lib
diff --git a/Haskell/Simplicity/Bitcoin/Programs/SigHash/Lib.hs b/Haskell/Simplicity/Bitcoin/Programs/SigHash/Lib.hs
new file mode 100644
index 000000000..c3c3b1748
--- /dev/null
+++ b/Haskell/Simplicity/Bitcoin/Programs/SigHash/Lib.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+-- | This module unpacks the 'Simplicity.Bitcoin.Programs.SigHash.lib' library instance into individual functions.
+-- Users should prefer to use 'Simplicity.Bitcoin.Programs.SigHash.mkLib' in order to share library dependencies.
+-- This module is provided mostly for testing purposes.
+module Simplicity.Bitcoin.Programs.SigHash.Lib
+ ( outputValuesHash, outputScriptsHash
+ , outputsHash, outputHash
+ , inputValuesHash, inputScriptsHash, inputUtxosHash, inputUtxoHash
+ , inputOutpointsHash, inputSequencesHash, inputAnnexesHash, inputScriptSigsHash, inputsHash, inputHash
+ , txHash
+ , tapleafHash, tappathHash, tapEnvHash
+ , sigAllHash
+ ) where
+
+import qualified Simplicity.Bitcoin.Programs.SigHash as SigHash
+
+outputValuesHash = SigHash.outputValuesHash SigHash.lib
+outputScriptsHash = SigHash.outputScriptsHash SigHash.lib
+outputsHash = SigHash.outputsHash SigHash.lib
+outputHash = SigHash.outputHash SigHash.lib
+inputValuesHash = SigHash.inputValuesHash SigHash.lib
+inputScriptsHash = SigHash.inputScriptsHash SigHash.lib
+inputUtxosHash = SigHash.inputUtxosHash SigHash.lib
+inputUtxoHash = SigHash.inputUtxoHash SigHash.lib
+inputOutpointsHash = SigHash.inputOutpointsHash SigHash.lib
+inputSequencesHash = SigHash.inputSequencesHash SigHash.lib
+inputAnnexesHash = SigHash.inputAnnexesHash SigHash.lib
+inputsHash = SigHash.inputsHash SigHash.lib
+inputHash = SigHash.inputHash SigHash.lib
+inputScriptSigsHash = SigHash.inputScriptSigsHash SigHash.lib
+txHash = SigHash.txHash SigHash.lib
+tapleafHash = SigHash.tapleafHash SigHash.lib
+tappathHash = SigHash.tappathHash SigHash.lib
+tapEnvHash = SigHash.tapEnvHash SigHash.lib
+sigAllHash = SigHash.sigAllHash SigHash.lib
diff --git a/Haskell/Simplicity/Bitcoin/Programs/Transaction.hs b/Haskell/Simplicity/Bitcoin/Programs/Transaction.hs
index 926a68720..59f3fbf6d 100644
--- a/Haskell/Simplicity/Bitcoin/Programs/Transaction.hs
+++ b/Haskell/Simplicity/Bitcoin/Programs/Transaction.hs
@@ -4,20 +4,24 @@ module Simplicity.Bitcoin.Programs.Transaction
  ( Lib(Lib), lib
  , numInputs
  , numOutputs
+ , totalInputValue
+ , totalOutputValue
+ , fee
  , currentPrevOutpoint
  , currentValue
--- , currentScriptHash
+ , currentScriptHash
  , currentSequence
  , currentAnnexHash
  , currentScriptSigHash
  ) where
 
-import Prelude hiding (take, drop)
+import Prelude hiding (take, drop, subtract)
 
 import Simplicity.Digest
 import Simplicity.Bitcoin.Primitive
 import Simplicity.Bitcoin.Term hiding (one)
 import Simplicity.Functor
+import Simplicity.Programs.Arith
 import Simplicity.Programs.Bit
 import Simplicity.Programs.Word
 import Simplicity.Ty.Word
@@ -29,12 +33,15 @@ data Lib term =
     numInputs :: term () Word32
     -- | Returns the number of outputs the transaction has.
   , numOutputs :: term () Word32
+  , totalInputValue :: term () Word64
+  , totalOutputValue :: term () Word64
+  , fee :: term () Word64
     -- | Returns the `InputPrevOutpoint` of the `CurrentIndex`.
   , currentPrevOutpoint :: term () (Word256,Word32)
     -- | Returns the `InputValue` of the `CurrentIndex`.
   , currentValue :: term () Word64
---    -- | Returns the `InputScriptHash` of the `CurrentIndex`.
---  , currentScriptHash :: term () Word256
+    -- | Returns the `InputScriptHash` of the `CurrentIndex`.
+  , currentScriptHash :: term () Word256
     -- | Returns the `InputSequence` of the `CurrentIndex`.
   , currentSequence :: term () Word32
     -- | Returns the `InputAnnexHash` of the `CurrentIndex`.
@@ -49,9 +56,12 @@ instance SimplicityFunctor Lib where
     {
       numInputs = m numInputs
     , numOutputs = m numOutputs
+    , totalInputValue = m totalInputValue
+    , totalOutputValue = m totalOutputValue
+    , fee = m fee
     , currentPrevOutpoint = m currentPrevOutpoint
     , currentValue = m currentValue
---    , currentScriptHash = m currentScriptHash
+    , currentScriptHash = m currentScriptHash
     , currentSequence = m currentSequence
     , currentAnnexHash = m currentAnnexHash
     , currentScriptSigHash = m currentScriptSigHash
@@ -66,11 +76,21 @@ lib = l
 
   , numOutputs = firstFail word32 (primitive OutputValue)
 
+  , totalInputValue = let
+      body = take (drop (primitive InputValue)) &&& ih >>> match (injl ih) (injr (add word64 >>> ih))
+     in (iden &&& zero word64) >>> forWhile word32 body >>> copair iden iden
+
+  , totalOutputValue = let
+      body = take (drop (primitive OutputValue)) &&& ih >>> match (injl ih) (injr (add word64 >>> ih))
+     in (iden &&& zero word64) >>> forWhile word32 body >>> copair iden iden
+
+  , fee = totalInputValue &&& totalOutputValue >>> subtract word64 >>> ih
+
   , currentPrevOutpoint = primitive CurrentIndex >>> assert (primitive InputPrevOutpoint)
 
   , currentValue = primitive CurrentIndex >>> assert (primitive InputValue)
 
---  , currentScriptHash = primitive CurrentIndex >>> assert (primitive InputScriptHash)
+  , currentScriptHash = primitive CurrentIndex >>> assert (primitive InputScriptHash)
 
   , currentSequence = primitive CurrentIndex >>> assert (primitive InputSequence)
 
diff --git a/Haskell/Simplicity/Bitcoin/Programs/Transaction/Lib.hs b/Haskell/Simplicity/Bitcoin/Programs/Transaction/Lib.hs
index bb9a1ab28..642f9910a 100644
--- a/Haskell/Simplicity/Bitcoin/Programs/Transaction/Lib.hs
+++ b/Haskell/Simplicity/Bitcoin/Programs/Transaction/Lib.hs
@@ -3,9 +3,12 @@
 module Simplicity.Bitcoin.Programs.Transaction.Lib
   ( numInputs
   , numOutputs
+  , totalInputValue
+  , totalOutputValue
+  , fee
   , currentPrevOutpoint
   , currentValue
---  , currentScriptHash
+  , currentScriptHash
   , currentSequence
   , currentAnnexHash
   , currentScriptSigHash
@@ -15,9 +18,12 @@ import qualified Simplicity.Bitcoin.Programs.Transaction as Transaction
 
 numInputs = Transaction.numInputs Transaction.lib
 numOutputs = Transaction.numOutputs Transaction.lib
+totalInputValue = Transaction.totalInputValue Transaction.lib
+totalOutputValue = Transaction.totalOutputValue Transaction.lib
+fee = Transaction.fee Transaction.lib
 currentPrevOutpoint = Transaction.currentPrevOutpoint Transaction.lib
 currentValue = Transaction.currentValue Transaction.lib
--- currentScriptHash = Transaction.currentScriptHash Transaction.lib
+currentScriptHash = Transaction.currentScriptHash Transaction.lib
 currentSequence = Transaction.currentSequence Transaction.lib
 currentAnnexHash = Transaction.currentAnnexHash Transaction.lib
 currentScriptSigHash = Transaction.currentScriptSigHash Transaction.lib
diff --git a/Haskell/Simplicity/Elements/Jets.hs b/Haskell/Simplicity/Elements/Jets.hs
index 8a30e193f..9e30c75e7 100644
--- a/Haskell/Simplicity/Elements/Jets.hs
+++ b/Haskell/Simplicity/Elements/Jets.hs
@@ -21,7 +21,6 @@ import Prelude hiding (fail, drop, take)
 import Control.Applicative ((<|>))
 import Control.Arrow ((***), (+++))
 import Control.Monad (guard)
-import qualified Data.ByteString as BS
 import Data.Either (isRight)
 import Data.Foldable (toList)
 import qualified Data.Map as Map
@@ -54,7 +53,7 @@ import qualified Simplicity.Elements.Programs.Transaction.Lib as Prog
 import Simplicity.LibSecp256k1.Spec (fe)
 import qualified Simplicity.LibSecp256k1.Schnorr as Schnorr
 import Simplicity.MerkleRoot
-import Simplicity.Programs.Elements.Lib (Ctx8)
+import Simplicity.Programs.Sha256.Lib (Ctx8)
 import qualified Simplicity.Programs.Elements.Lib as Prog
 import Simplicity.Programs.Word
 import Simplicity.Serialization
@@ -62,6 +61,7 @@ import Simplicity.Tensor
 import Simplicity.Tree
 import Simplicity.Ty
 import Simplicity.Ty.Bit
+import Simplicity.Ty.Sha256
 import Simplicity.Ty.Word
 import qualified Simplicity.Word as W
 import Simplicity.Weight
@@ -359,14 +359,14 @@ implementationSigHash InputAmountsHash env _ = Just . toWord256 . integerHash256
 implementationSigHash InputScriptsHash env _ = Just . toWord256 . integerHash256 $ inputScriptsHash (envTx env)
 implementationSigHash TapleafHash env _ = Just . toWord256 . integerHash256 $ tapleafHash (envTap env)
 implementationSigHash TappathHash env _ = Just . toWord256 . integerHash256 $ tappathHash (envTap env)
-implementationSigHash OutpointHash _env (ctx, (mw256, op)) = toCtx <$> (flip ctxAdd (runPut (putMW256 mw256 >> putOutpointBE (cast op))) =<< fromCtx ctx)
+implementationSigHash OutpointHash _env (ctx, (mw256, op)) = toCtx8 <$> (flip ctxAdd (runPut (putMW256 mw256 >> putOutpointBE (cast op))) =<< fromCtx8 ctx)
  where
   putMW256 (Left _) = putWord8 0x00
   putMW256 (Right w256) = putWord8 0x01 >> put (fromIntegral (fromWord256 w256) :: W.Word256)
   cast (h, i) = Outpoint (review (over be256) (fromW256 h)) (fromW32 i)
   fromW256 = fromIntegral . fromWord256
   fromW32 = fromIntegral . fromWord32
-implementationSigHash AssetAmountHash _env (ctx, (cw256, cw64)) = toCtx <$> (flip ctxAdd (runPut (put256 cw256 >> put64 cw64)) =<< fromCtx ctx)
+implementationSigHash AssetAmountHash _env (ctx, (cw256, cw64)) = toCtx8 <$> (flip ctxAdd (runPut (put256 cw256 >> put64 cw64)) =<< fromCtx8 ctx)
  where
   put256 (Left (by, x)) = putWord8 (if fromBit by then 0xb else 0x0a) >> put (fromW256 x)
   put256 (Right w256) = putWord8 0x01 >> put (fromW256 w256)
@@ -376,10 +376,10 @@ implementationSigHash AssetAmountHash _env (ctx, (cw256, cw64)) = toCtx <$> (fli
   fromW256 = fromIntegral . fromWord256
   fromW64 :: Word64 -> W.Word64
   fromW64 = fromIntegral . fromWord64
-implementationSigHash NonceHash _env (ctx, mcw256) = toCtx <$> (flip ctxAdd (runPut . putNonce $ nonce) =<< fromCtx ctx)
+implementationSigHash NonceHash _env (ctx, mcw256) = toCtx8 <$> (flip ctxAdd (runPut . putNonce $ nonce) =<< fromCtx8 ctx)
  where
   nonce = either (const Nothing) (Just . Nonce . ((fromBit *** (fromIntegral . fromWord256)) +++ fromHash)) mcw256
-implementationSigHash AnnexHash _env (ctx, mw256) = toCtx <$> (flip ctxAdd (runPut . putMW256 $ mw256) =<< fromCtx ctx)
+implementationSigHash AnnexHash _env (ctx, mw256) = toCtx8 <$> (flip ctxAdd (runPut . putMW256 $ mw256) =<< fromCtx8 ctx)
  where
   putMW256 (Left _) = putWord8 0x00
   putMW256 (Right w256) = putWord8 0x01 >> put (fromIntegral (fromWord256 w256) :: W.Word256)
@@ -971,12 +971,3 @@ instance Primitive MatcherInfo where
   primitive p = MatcherInfo (primitive p)
 
 fromPoint (by, x) = Point (fromBit by) (fe (fromWord256 x))
-fromHash = review (over be256) . fromIntegral . fromWord256
-fromCtx (buffer, (count, midstate)) = ctxBuild (fromInteger . fromWord8 <$> buffer^..buffer_ buffer63)
-                                               (fromWord64 count)
-                                               (fromHash midstate)
-toCtx ctx = (buffer, (count, midstate))
- where
-  buffer = fst $ bufferFill buffer63 (toWord8 . fromIntegral <$> BS.unpack (ctxBuffer ctx))
-  count = toWord64 . fromIntegral $ ctxCounter ctx
-  midstate = toWord256 . integerHash256 . ivHash $ ctxIV ctx
diff --git a/Haskell/Simplicity/Elements/Programs/SigHash.hs b/Haskell/Simplicity/Elements/Programs/SigHash.hs
index 18e0f8976..e6c377cc1 100644
--- a/Haskell/Simplicity/Elements/Programs/SigHash.hs
+++ b/Haskell/Simplicity/Elements/Programs/SigHash.hs
@@ -181,6 +181,7 @@ data Lib term =
     -- | A hash of
     --
     -- * 'GenesisBlockHash' twice (This is effectively a tag.)
+    -- * 'txHash'
     -- * 'tapEnvHash'
     -- * 'CurrentIndex'
   , sigAllHash :: term () Word256
diff --git a/Haskell/Tests/Simplicity/Bitcoin/Arbitrary.hs b/Haskell/Tests/Simplicity/Bitcoin/Arbitrary.hs
new file mode 100644
index 000000000..8deb1ed2a
--- /dev/null
+++ b/Haskell/Tests/Simplicity/Bitcoin/Arbitrary.hs
@@ -0,0 +1,95 @@
+-- This module tests the Simplicity programs on arbitrary inputs.
+module Simplicity.Bitcoin.Arbitrary
+ ( arbitraryHash256, arbitraryLock
+ , genPrimEnv, forallPrimEnv, forallInPrimEnv, forallOutPrimEnv
+ ) where
+
+import Data.Bits ((.&.))
+import qualified Data.ByteString.Lazy as BSL
+import Data.Vector (fromList)
+import Lens.Family2 (review, over)
+
+import Simplicity.Arbitrary
+import Simplicity.Digest
+import Simplicity.Bitcoin.DataTypes
+import Simplicity.Bitcoin.Primitive
+import Simplicity.LibSecp256k1.Spec
+import Simplicity.Ty.Arbitrary
+import Simplicity.Word
+
+import Test.Tasty.QuickCheck ( Arbitrary(..), Discard(Discard), Gen, Property, Testable
+                             , arbitraryBoundedIntegral, arbitrarySizedBoundedIntegral
+                             , choose, oneof, listOf, listOf1
+                             , forAll, property
+                             )
+
+arbitraryVersion :: Gen Word32
+arbitraryVersion = genBoundaryCases 2
+
+arbitraryLock :: Gen Lock
+arbitraryLock = genBoundaryCases 500000000
+
+arbitraryHash256 :: Gen Hash256
+arbitraryHash256 = review (over be256) <$> arbitraryBoundedIntegral
+
+arbitraryPoint :: Gen Point
+arbitraryPoint = pointAsSpec <$> arbitrary
+
+arbitraryBS :: Gen BSL.ByteString
+arbitraryBS = BSL.pack <$> listOf arbitrary
+
+instance Arbitrary TxOutput where
+  arbitrary = TxOutput <$> arbitrarySizedBoundedIntegral <*> arbitraryBS
+
+instance Arbitrary Outpoint where
+  arbitrary = Outpoint <$> arbitraryHash256 <*> arbitrarySizedBoundedIntegral
+
+instance Arbitrary SigTxInput where
+  arbitrary = SigTxInput <$> arbitrary
+                         <*> arbitrary
+                         <*> oneof [return maxBound, arbitraryBoundedIntegral]
+                         <*> oneof [return Nothing, Just <$> arbitraryBS]
+                         <*> arbitraryBS
+
+instance Arbitrary SigTx where
+  arbitrary = SigTx <$> arbitraryVersion
+                    <*> (fromList <$> listOf1 arbitrary)
+                    <*> (fromList <$> listOf1 arbitrary)
+                    <*> arbitraryLock
+
+instance Arbitrary TapEnv where
+  arbitrary = TapEnv <$> ((0xfe .&.) <$> arbitraryBoundedIntegral)
+                     <*> (mkPubKey <$> arbitraryPoint)
+                     <*> listOf arbitraryHash256
+                     <*> arbitraryHash256
+   where
+    mkPubKey (Point _ x) = PubKey (fe_pack x)
+
+genPrimEnv :: Gen (Maybe PrimEnv)
+genPrimEnv = do
+   tx <- arbitrary
+   tapenv <- arbitrary
+   ix <- fromIntegral <$> choose (0, length (sigTxIn tx) - 1)
+   return $ primEnv tx ix tapenv
+
+forallPrimEnv :: Testable prop => (PrimEnv -> prop) -> Property
+forallPrimEnv p = forAll genPrimEnv go
+  where
+   go (Just env) = property $ p env
+   go Nothing = property Discard
+
+forallInPrimEnv :: Testable prop => (PrimEnv -> Word32 -> prop) -> Property
+forallInPrimEnv p = forAll genPrimEnv go
+  where
+   go Nothing = property Discard
+   go (Just env) = forAll genIx $ \i -> property $ p env i
+    where
+     genIx = fromIntegral <$> genBoundaryCases (length (sigTxIn (envTx env))) -- Generate out of bounds cases too.
+
+forallOutPrimEnv :: Testable prop => (PrimEnv -> Word32 -> prop) -> Property
+forallOutPrimEnv p = forAll genPrimEnv go
+  where
+   go Nothing = property Discard
+   go (Just env) = forAll genIx $ \i -> property $ p env i
+    where
+     genIx = fromIntegral <$> genBoundaryCases (length (sigTxOut (envTx env))) -- Generate out of bounds cases too.
diff --git a/Haskell/Tests/Simplicity/Bitcoin/TestEval.hs b/Haskell/Tests/Simplicity/Bitcoin/TestEval.hs
new file mode 100644
index 000000000..73e66b2e6
--- /dev/null
+++ b/Haskell/Tests/Simplicity/Bitcoin/TestEval.hs
@@ -0,0 +1,55 @@
+-- | This module builds a wrapper around 'Simplicity.Bitcoin.Semantics.fastEval' to define a 'testEval' variant.
+module Simplicity.Bitcoin.TestEval
+  ( testEval, TestEval
+  ) where
+
+import Prelude hiding (drop, take, fail)
+
+import Control.Arrow (Kleisli(..), first)
+import Control.Monad.Reader (ReaderT(..))
+
+import qualified Simplicity.Bitcoin.Jets as Jets
+import Simplicity.Bitcoin.JetType
+import Simplicity.Bitcoin.Primitive
+import Simplicity.Bitcoin.Semantics
+import Simplicity.Bitcoin.Term
+
+-- | An Assert instance for 'testCoreEval'.
+data TestEval jt a b = TestEval { testEvalSem :: Kleisli (ReaderT PrimEnv Maybe) a b
+                                , testEvalFast :: FastEval jt a b
+                                }
+
+-- | 'testEval' optimizes Simplicity with assertions evaluation using jets, similar to 'fastEval',
+-- but excludes the expression itself from being substituted.
+-- This is used in for testing jets against their specifications under the assumption that jets for any subexpressions are correct.
+-- Delegation, witnesses, and jets are not supported since they are not allowed within jet definitions.
+testEval :: TestEval Jets.JetType a b -> PrimEnv -> a -> Maybe b
+testEval = flip . (runReaderT .) . runKleisli . testEvalSem
+
+testFastKleisli = Kleisli . (ReaderT .) . flip . fastEval . testEvalFast
+
+mkLeaf sComb fComb = TestEval sComb fComb
+
+mkUnary sComb fComb t = TestEval (sComb (testFastKleisli t)) (fComb (testEvalFast t))
+
+mkBinary sComb fComb s t = TestEval (sComb (testFastKleisli s) (testFastKleisli t))
+                                    (fComb (testEvalFast s) (testEvalFast t))
+
+instance JetType jt => Core (TestEval jt) where
+  iden = mkLeaf iden iden
+  comp = mkBinary comp comp
+  unit = mkLeaf unit unit
+  injl = mkUnary injl injl
+  injr = mkUnary injr injr
+  match = mkBinary match match
+  pair = mkBinary pair pair
+  take = mkUnary take take
+  drop = mkUnary drop drop
+
+instance JetType jt => Assert (TestEval jt) where
+  assertl s h = mkUnary (flip assertl h) (flip assertl h) s
+  assertr h t = mkUnary (assertr h) (assertr h) t
+  fail b = mkLeaf (fail b) (fail b)
+
+instance JetType jt => Primitive (TestEval jt)  where
+  primitive p = mkLeaf (primitive p) (primitive p)
diff --git a/Haskell/Tests/Simplicity/Bitcoin/Tests.hs b/Haskell/Tests/Simplicity/Bitcoin/Tests.hs
new file mode 100644
index 000000000..ee5cfbed0
--- /dev/null
+++ b/Haskell/Tests/Simplicity/Bitcoin/Tests.hs
@@ -0,0 +1,429 @@
+module Simplicity.Bitcoin.Tests (tests) where
+
+import Control.Arrow ((***), (+++))
+import qualified Data.ByteString.Char8 as BSC
+import qualified Data.ByteString.Lazy as BSL
+import qualified Data.Map as Map
+import Data.Maybe (fromMaybe, isJust)
+import Data.Serialize (encode, put, putWord8, putWord32be, runPutLazy)
+import Data.Vector ((!), (!?), fromList)
+import Lens.Family2 (review, over, under, view)
+
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (Assertion, (@?=), assertBool, testCase)
+import Test.Tasty.QuickCheck (Property, NonNegative(..), arbitrary, classify, forAll, testProperty)
+
+import Simplicity.Arbitrary
+import Simplicity.Digest
+import Simplicity.Bitcoin.Arbitrary
+import Simplicity.Bitcoin.DataTypes
+import Simplicity.Bitcoin.Jets
+import Simplicity.Bitcoin.Term
+import Simplicity.Bitcoin.TestEval
+import Simplicity.Bitcoin.Primitive (primEnv, primEnvHash, envTx, envTap)
+import qualified Simplicity.Bitcoin.Programs.TimeLock as Prog
+import Simplicity.Bitcoin.Semantics
+import qualified Simplicity.LibSecp256k1.Spec as Schnorr
+import Simplicity.MerkleRoot
+import Simplicity.Programs.CheckSig.Lib
+import qualified Simplicity.Programs.Sha256 as Sha256
+import qualified Simplicity.Programs.Bitcoin.Lib as Prog
+import qualified Simplicity.Bitcoin.Programs.SigHash.Lib as Prog
+import Simplicity.TestCoreEval
+import Simplicity.Ty.Arbitrary
+import Simplicity.Ty.Word
+import qualified Simplicity.Word as Word
+
+toW32 :: Word.Word32 -> Word32
+toW32 = toWord32 . fromIntegral
+
+toW16 :: Word.Word16 -> Word16
+toW16 = toWord16 . fromIntegral
+
+toW8 :: Word.Word8 -> Word8
+toW8 = toWord8 . fromIntegral
+
+tests :: TestTree
+tests = testGroup "Bitcoin"
+        [ -- Regression.tests
+          testGroup "TimeLock"
+          [ testProperty "tx_is_final" prop_tx_is_final
+          , testProperty "tx_lock_height" prop_tx_lock_height
+          , testProperty "tx_lock_time" prop_tx_lock_time
+          , testProperty "tx_lock_distance" prop_tx_lock_distance
+          , testProperty "tx_lock_duration" prop_tx_lock_duration
+          , testProperty "check_lock_height" prop_check_lock_height
+          , testProperty "check_lock_time" prop_check_lock_time
+          , testProperty "check_lock_distance" prop_check_lock_distance
+          , testProperty "check_lock_duration" prop_check_lock_duration
+          ]
+        , testGroup "Bitcoin Functions"
+          [ testProperty "outpoint_hash" prop_outpoint_hash
+          , testProperty "annex_hash" prop_annex_hash
+          , testProperty "build_tapleaf_simplicity" prop_build_tapleaf_simplicity
+          , testProperty "build_tapbranch" prop_build_tapbranch
+          , testProperty "build_taptweak" prop_build_taptweak
+          , testProperty "output_values_hash" prop_output_values_hash
+          , testProperty "output_scripts_hash" prop_output_scripts_hash
+          , testProperty "outputs_hash" prop_outputs_hash
+          , testProperty "output_hash" prop_output_hash
+          , testProperty "input_outpoints_hash" prop_input_outpoints_hash
+          , testProperty "input_values_hash" prop_input_values_hash
+          , testProperty "input_scripts_hash" prop_input_scripts_hash
+          , testProperty "input_utxos_hash" prop_input_utxos_hash
+          , testProperty "input_utxo_hash" prop_input_utxo_hash
+          , testProperty "input_sequences_hash" prop_input_sequences_hash
+          , testProperty "input_annexes_hash" prop_input_annexes_hash
+          , testProperty "input_script_sigs_hash" prop_input_script_sigs_hash
+          , testProperty "inputs_hash" prop_inputs_hash
+          , testProperty "input_hash" prop_input_hash
+          , testProperty "tx_hash" prop_tx_hash
+          , testProperty "tap_env_hash" prop_tap_env_hash
+          , testProperty "tappath_hash" prop_tappath_hash
+          , testProperty "tapleaf_hash" prop_tapleaf_hash
+          , testProperty "sig_all_hash" prop_sig_all_hash
+          , testProperty "script_cmr" prop_script_cmr
+          , testProperty "internal_key" prop_internal_key
+          , testProperty "current_index" prop_current_index
+          , testProperty "num_inputs" prop_num_inputs
+          , testProperty "num_outputs" prop_num_outputs
+          , testProperty "lock_time" prop_lock_time
+          , testProperty "output_value" prop_output_value
+          , testProperty "output_script_hash" prop_output_script_hash
+          , testProperty "total_output_value" prop_total_output_value
+          , testProperty "current_prev_outpoint" prop_current_prev_outpoint
+          , testProperty "current_value" prop_current_value
+          , testProperty "current_script_hash" prop_current_script_hash
+          , testProperty "current_sequence" prop_current_sequence
+          , testProperty "current_annex_hash" prop_current_annex_hash
+          , testProperty "current_script_sig_hash" prop_current_script_sig_hash
+          , testProperty "input_prev_outpoint" prop_input_prev_outpoint
+          , testProperty "input_value" prop_input_value
+          , testProperty "input_script_hash" prop_input_script_hash
+          , testProperty "input_sequence" prop_input_sequence
+          , testProperty "input_annex_hash" prop_input_annex_hash
+          , testProperty "input_script_sig_hash" prop_input_script_sig_hash
+          , testProperty "total_input_value" prop_total_input_value
+          , testProperty "fee" prop_fee
+          , testProperty "tapleaf_version" prop_tapleaf_version
+          , testProperty "tappath" prop_tappath
+          , testProperty "version" prop_version
+          , testProperty "transaction_id" prop_transaction_id
+          ]
+        , testCase "sigHashAll" (assertBool "sigHashAll_matches" hunit_sigHashAll)
+        ]
+
+-- We use continuations here because we need to ensure that 'fastSpec' is memoized outside of any lambda expressions.
+checkJet jet k = k (\env a -> fastSpec env a == implementation jet env a)
+ where
+  fastSpec = testEval (specification jet)
+
+prop_tx_is_final :: Property
+prop_tx_is_final = checkJet (BitcoinJet (TimeLockJet TxIsFinal))
+                 $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_tx_lock_height :: Property
+prop_tx_lock_height = checkJet (BitcoinJet (TimeLockJet TxLockHeight))
+                    $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_tx_lock_time :: Property
+prop_tx_lock_time = checkJet (BitcoinJet (TimeLockJet TxLockTime))
+                  $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_tx_lock_distance :: Property
+prop_tx_lock_distance = checkJet (BitcoinJet (TimeLockJet TxLockDistance))
+                      $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_tx_lock_duration :: Property
+prop_tx_lock_duration = checkJet (BitcoinJet (TimeLockJet TxLockDuration))
+                      $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_check_lock_height :: Property
+prop_check_lock_height = checkJet (BitcoinJet (TimeLockJet CheckLockHeight))
+                       $ \check -> forallPrimEnv $ \env -> forAll (genBoundaryCases . sigTxLock $ envTx env)
+                                                 $ \w -> check env (toW32 w)
+
+prop_check_lock_time :: Property
+prop_check_lock_time = checkJet (BitcoinJet (TimeLockJet CheckLockTime))
+                     $ \check -> forallPrimEnv $ \env -> forAll (genBoundaryCases . sigTxLock $ envTx env)
+                                               $ \w -> check env (toW32 w)
+
+prop_check_lock_distance :: Property
+prop_check_lock_distance = checkJet (BitcoinJet (TimeLockJet CheckLockDistance))
+                         $ \check -> forallPrimEnv $ \env -> forAll (genBoundaryCases . txLockDistance $ envTx env)
+                                                   $ \w -> check env (toW16 w)
+
+prop_check_lock_duration :: Property
+prop_check_lock_duration = checkJet (BitcoinJet (TimeLockJet CheckLockDuration))
+                         $ \check -> forallPrimEnv $ \env -> forAll (genBoundaryCases . txLockDuration $ envTx env)
+                                                   $ \w -> check env (toW16 w)
+
+prop_build_tapleaf_simplicity :: HashElement -> Bool
+prop_build_tapleaf_simplicity = \cmr ->
+  let input = heAsTy cmr in
+  fast_build_tapleaf_simplicity input ==
+    implementation (BitcoinJet (SigHashJet BuildTapleafSimplicity)) undefined input
+ where
+  fast_build_tapleaf_simplicity = testCoreEval Prog.buildTapleafSimplicity
+
+prop_build_tapbranch :: HashElement -> HashElement -> Bool
+prop_build_tapbranch = \a b ->
+  let input = (heAsTy a, heAsTy b) in
+  fast_build_tapbranch input ==
+    implementation (BitcoinJet (SigHashJet BuildTapbranch)) undefined input
+ where
+  fast_build_tapbranch = testCoreEval Prog.buildTapbranch
+
+prop_build_taptweak :: FieldElement -> HashElement -> Bool
+prop_build_taptweak = \a b ->
+  let input = (feAsTy a, heAsTy b) in
+  fast_build_taptweak input ==
+    implementation (BitcoinJet (SigHashJet BuildTaptweak)) undefined input
+ where
+  fast_build_taptweak = testCoreEval Prog.buildTaptweak
+
+prop_outpoint_hash :: Sha256CtxElement -> (HashElement, Word.Word32) -> Bool
+prop_outpoint_hash = \ctx op ->
+  let input = (ctxAsTy ctx, (heAsTy *** (toWord32 . fromIntegral) $ op))
+  in fast_outpoint_hash input == implementation (BitcoinJet (SigHashJet OutpointHash)) undefined input
+ where
+  fast_outpoint_hash = testCoreEval Prog.outpointHash
+
+prop_annex_hash :: Sha256CtxElement -> Maybe Word256 -> Bool
+prop_annex_hash = \ctx mw256 ->
+  let input = (ctxAsTy ctx, cast mw256)
+  in fast_annex_hash input == implementation (BitcoinJet (SigHashJet AnnexHash)) undefined input
+ where
+  fast_annex_hash = testCoreEval Prog.annexHash
+  cast = maybe (Left ()) Right
+
+prop_output_values_hash :: Property
+prop_output_values_hash = checkJet (BitcoinJet (SigHashJet OutputValuesHash))
+                         $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_output_scripts_hash :: Property
+prop_output_scripts_hash = checkJet (BitcoinJet (SigHashJet OutputScriptsHash))
+                         $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_outputs_hash :: Property
+prop_outputs_hash = checkJet (BitcoinJet (SigHashJet OutputsHash))
+                  $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_output_hash :: Property
+prop_output_hash = checkJet (BitcoinJet (SigHashJet OutputHash))
+                  $ \check -> forallOutPrimEnv $ \env i -> check env (toW32 i)
+
+prop_input_outpoints_hash :: Property
+prop_input_outpoints_hash = checkJet (BitcoinJet (SigHashJet InputOutpointsHash))
+                          $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_input_values_hash :: Property
+prop_input_values_hash = checkJet (BitcoinJet (SigHashJet InputValuesHash))
+                        $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_input_scripts_hash :: Property
+prop_input_scripts_hash = checkJet (BitcoinJet (SigHashJet InputScriptsHash))
+                        $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_input_utxos_hash :: Property
+prop_input_utxos_hash = checkJet (BitcoinJet (SigHashJet InputUtxosHash))
+                      $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_input_utxo_hash :: Property
+prop_input_utxo_hash = checkJet (BitcoinJet (SigHashJet InputUtxoHash))
+                     $ \check -> forallInPrimEnv $ \env i -> check env (toW32 i)
+
+prop_input_sequences_hash :: Property
+prop_input_sequences_hash = checkJet (BitcoinJet (SigHashJet InputSequencesHash))
+                          $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_input_annexes_hash :: Property
+prop_input_annexes_hash = checkJet (BitcoinJet (SigHashJet InputAnnexesHash))
+                        $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_input_script_sigs_hash :: Property
+prop_input_script_sigs_hash = checkJet (BitcoinJet (SigHashJet InputScriptSigsHash))
+                            $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_inputs_hash :: Property
+prop_inputs_hash = checkJet (BitcoinJet (SigHashJet InputsHash))
+                 $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_input_hash :: Property
+prop_input_hash = checkJet (BitcoinJet (SigHashJet InputHash))
+                 $ \check -> forallInPrimEnv $ \env i -> check env (toW32 i)
+
+prop_tx_hash :: Property
+prop_tx_hash = checkJet (BitcoinJet (SigHashJet TxHash))
+             $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_tappath_hash :: Property
+prop_tappath_hash = checkJet (BitcoinJet (SigHashJet TappathHash))
+                    $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_tapleaf_hash :: Property
+prop_tapleaf_hash = checkJet (BitcoinJet (SigHashJet TapleafHash))
+                  $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_tap_env_hash :: Property
+prop_tap_env_hash = checkJet (BitcoinJet (SigHashJet TapEnvHash))
+                  $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_sig_all_hash :: Property
+prop_sig_all_hash = checkJet (BitcoinJet (SigHashJet SigAllHash))
+                  $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_script_cmr :: Property
+prop_script_cmr = checkJet (BitcoinJet (TransactionJet ScriptCMR))
+                $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_internal_key :: Property
+prop_internal_key = checkJet (BitcoinJet (TransactionJet InternalKey))
+                  $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_current_index :: Property
+prop_current_index = checkJet (BitcoinJet (TransactionJet CurrentIndex))
+                   $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_num_inputs :: Property
+prop_num_inputs = checkJet (BitcoinJet (TransactionJet NumInputs))
+                $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_num_outputs :: Property
+prop_num_outputs = checkJet (BitcoinJet (TransactionJet NumOutputs))
+                 $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_lock_time :: Property
+prop_lock_time = checkJet (BitcoinJet (TransactionJet LockTime))
+               $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_output_value :: Property
+prop_output_value = checkJet (BitcoinJet (TransactionJet OutputValue))
+                   $ \check -> forallOutPrimEnv $ \env i -> check env (toW32 i)
+
+prop_output_script_hash :: Property
+prop_output_script_hash = checkJet (BitcoinJet (TransactionJet OutputScriptHash))
+                        $ \check -> forallOutPrimEnv $ \env i -> check env (toW32 i)
+
+prop_total_output_value :: Property
+prop_total_output_value = checkJet (BitcoinJet (TransactionJet TotalOutputValue))
+                        $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_current_prev_outpoint :: Property
+prop_current_prev_outpoint = checkJet (BitcoinJet (TransactionJet CurrentPrevOutpoint))
+                           $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_current_value :: Property
+prop_current_value = checkJet (BitcoinJet (TransactionJet CurrentValue))
+                    $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_current_script_hash :: Property
+prop_current_script_hash = checkJet (BitcoinJet (TransactionJet CurrentScriptHash))
+                         $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_current_sequence :: Property
+prop_current_sequence = checkJet (BitcoinJet (TransactionJet CurrentSequence))
+                      $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_current_annex_hash :: Property
+prop_current_annex_hash = checkJet (BitcoinJet (TransactionJet CurrentAnnexHash))
+                        $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_current_script_sig_hash :: Property
+prop_current_script_sig_hash = checkJet (BitcoinJet (TransactionJet CurrentScriptSigHash))
+                             $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_input_prev_outpoint :: Property
+prop_input_prev_outpoint = checkJet (BitcoinJet (TransactionJet InputPrevOutpoint))
+                         $ \check -> forallInPrimEnv $ \env i -> check env (toW32 i)
+
+prop_input_value :: Property
+prop_input_value = checkJet (BitcoinJet (TransactionJet InputValue))
+                  $ \check -> forallInPrimEnv $ \env i -> check env (toW32 i)
+
+prop_input_script_hash :: Property
+prop_input_script_hash = checkJet (BitcoinJet (TransactionJet InputScriptHash))
+                       $ \check -> forallInPrimEnv $ \env i -> check env (toW32 i)
+
+prop_input_sequence :: Property
+prop_input_sequence = checkJet (BitcoinJet (TransactionJet InputSequence))
+                    $ \check -> forallInPrimEnv $ \env i -> check env (toW32 i)
+
+prop_input_annex_hash :: Property
+prop_input_annex_hash = checkJet (BitcoinJet (TransactionJet InputAnnexHash))
+                      $ \check -> forallInPrimEnv $ \env i -> check env (toW32 i)
+
+prop_input_script_sig_hash :: Property
+prop_input_script_sig_hash = checkJet (BitcoinJet (TransactionJet InputScriptSigHash))
+                           $ \check -> forallInPrimEnv $ \env i -> check env (toW32 i)
+
+prop_total_input_value :: Property
+prop_total_input_value = checkJet (BitcoinJet (TransactionJet TotalInputValue))
+                       $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_fee :: Property
+prop_fee = checkJet (BitcoinJet (TransactionJet Fee))
+         $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_tapleaf_version :: Property
+prop_tapleaf_version = checkJet (BitcoinJet (TransactionJet TapleafVersion))
+                     $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_tappath :: Property
+prop_tappath = checkJet (BitcoinJet (TransactionJet Tappath))
+               $ \check -> forallPrimEnv $ \env -> forAll (genTappathIx env) $ \i -> check env (toW8 i)
+ where
+  genTappathIx = genBoundaryCases . fromIntegral . length . tappath . envTap
+
+prop_version :: Property
+prop_version = checkJet (BitcoinJet (TransactionJet Version))
+             $ \check -> forallPrimEnv $ \env -> check env ()
+
+prop_transaction_id :: Property
+prop_transaction_id = checkJet (BitcoinJet (TransactionJet TransactionId))
+                        $ \check -> forallPrimEnv $ \env -> check env ()
+
+tapEnv :: TapEnv
+tapEnv = TapEnv
+         { tapleafVersion = 0xbe
+         , tapInternalKey = Schnorr.PubKey 0x00000000000000000000003b78ce563f89a0ed9414f5aa28ad0d96d6795f9c63
+         , tappath = []
+         , tapScriptCMR = review (over be256) 0x896b16e4692350cb43c4807c8f9f63637f70f84a17b678ca9467109ff1e50f61
+         }
+
+tx1 :: SigTx
+tx1 = SigTx
+      { sigTxVersion = 0x00000002
+      , sigTxIn = fromList [input0]
+      , sigTxOut = fromList [output0]
+      , sigTxLock = 0
+      }
+ where
+  input0 = SigTxInput
+    { sigTxiPreviousOutpoint = Outpoint (review (over be256) 0xeb04b68e9a26d116046c76e8ff47332fb71dda90ff4bef5370f25226d3bc09fc) 0
+    , sigTxiTxo = TxOutput
+        { txoValue = 10000000000
+        , txoScript = BSL.empty
+        }
+    , sigTxiSequence = 0xfffffffe
+    , sigTxiAnnex = Nothing
+    , sigTxiScriptSig = BSL.empty
+    }
+  output0 = TxOutput
+    { txoValue = 9999996700
+    , txoScript = BSL.pack
+        [ 0x19, 0x76, 0xa9, 0x14, 0x48, 0x63, 0x3e, 0x2c, 0x0e, 0xe9, 0x49, 0x5d, 0xd3, 0xf9, 0xc4, 0x37
+        , 0x32, 0xc4, 0x7f, 0x47, 0x02, 0xa3, 0x62, 0xc8, 0x88, 0xac]
+    }
+
+hunit_sigHashAll :: Bool
+hunit_sigHashAll = Just (integerHash256 sigHashAll_spec) == (fromWord256 <$> (sem (sigHash' Prog.sigAllHash) txEnv ()))
+ where
+  ix = 0
+  txo = sigTxiTxo (sigTxIn tx1 ! (fromIntegral ix))
+  Just txEnv = primEnv tx1 ix tapEnv
+  signatureTag = bsHash $ BSC.pack "Simplicity\USSignature"
+  sigHashAll_spec = bslHash . runPutLazy
+                  $ put signatureTag >> put signatureTag
+                 >> put (commitmentRoot Prog.sigAllHash)
+                 >> put (primEnvHash txEnv)
diff --git a/Haskell/Tests/Simplicity/Elements/Tests.hs b/Haskell/Tests/Simplicity/Elements/Tests.hs
index ce48d141e..64be611e6 100644
--- a/Haskell/Tests/Simplicity/Elements/Tests.hs
+++ b/Haskell/Tests/Simplicity/Elements/Tests.hs
@@ -170,7 +170,6 @@ tests = testGroup "Elements"
         , testCase "sigHashAll" (assertBool "sigHashAll_matches" hunit_sigHashAll)
         ]
 
-
 -- We use continuations here because we need to ensure that 'fastSpec' is memoized outside of any lambda expressions.
 checkJet jet k = k (\env a -> fastSpec env a == implementation jet env a)
  where
diff --git a/Haskell/Tests/Tests.hs b/Haskell/Tests/Tests.hs
index f9cd99415..48334a67d 100644
--- a/Haskell/Tests/Tests.hs
+++ b/Haskell/Tests/Tests.hs
@@ -7,6 +7,7 @@ import qualified Simplicity.BitMachine.Tests as BitMachine
 import qualified Simplicity.BitMachine.StaticAnalysis.Tests as StaticAnalysis
 import qualified Simplicity.FFI.Tests as FFI
 import qualified Simplicity.Programs.Tests as Programs
+import qualified Simplicity.Bitcoin.Tests as Bitcoin
 import qualified Simplicity.Bitcoin.Serialization.Tests as BitcoinSerialization
 import qualified Simplicity.Elements.Tests as Elements
 import qualified Simplicity.Elements.FFI.Tests as ElementsFFI
@@ -23,6 +24,7 @@ tests = testGroup "Tests"
       , FFI.tests
       , BitMachine.tests
       , StaticAnalysis.tests
+      , Bitcoin.tests
       , BitcoinSerialization.tests
       , Ty.tests
       , Elements.tests
diff --git a/Simplicity.cabal b/Simplicity.cabal
index a31b38407..f1f9cd628 100644
--- a/Simplicity.cabal
+++ b/Simplicity.cabal
@@ -18,7 +18,7 @@ library Simplicity-Core
                        Haskell/cbits/frame.c, Haskell/cbits/coreJets.c
   Include-dirs:        C
   Includes:            sha256.h, frame.h, jets.h
-  exposed-modules:     Simplicity.Ty, Simplicity.Ty.Bit, Simplicity.Ty.Word, Simplicity.Ty.LibSecp256k1,
+  exposed-modules:     Simplicity.Ty, Simplicity.Ty.Bit, Simplicity.Ty.Word, Simplicity.Ty.LibSecp256k1, Simplicity.Ty.Sha256,
                        Simplicity.Term.Core,
                        Simplicity.CoreJets,
                        Simplicity.Functor, Simplicity.Tensor,
@@ -32,6 +32,7 @@ library Simplicity-Core
                        Simplicity.Programs.Sha256, Simplicity.Programs.Sha256.Lib,
                        Simplicity.Programs.LibSecp256k1, Simplicity.Programs.LibSecp256k1.Lib,
                        Simplicity.Programs.CheckSig, Simplicity.Programs.CheckSig.Lib,
+                       Simplicity.Programs.Bitcoin, Simplicity.Programs.Bitcoin.Lib,
                        Simplicity.Programs.Elements, Simplicity.Programs.Elements.Lib,
                        Simplicity.Programs.TimeLock,
                        Simplicity.Digest, Simplicity.Digest.Pure.SHA,
@@ -128,14 +129,15 @@ library
                        Haskell/cbits/elements/jets.c Haskell/cbits/elements/env.c
   Include-dirs:        C C/include
   Includes:            elements/elementsJets.h elements/primitive.h simplicity/elements/env.h
-  exposed-modules:     Simplicity.Bitcoin.Programs.Transaction, Simplicity.Bitcoin.Programs.Transaction.Lib,
+  exposed-modules:     Simplicity.Bitcoin.Programs.SigHash, Simplicity.Bitcoin.Programs.SigHash.Lib,
+                       Simplicity.Bitcoin.Programs.Transaction, Simplicity.Bitcoin.Programs.Transaction.Lib,
                        Simplicity.Bitcoin.Programs.TimeLock, Simplicity.Elements.Programs.TimeLock,
                        Simplicity.Elements.Programs.Issuance, Simplicity.Elements.Programs.Issuance.Lib,
                        Simplicity.Elements.Programs.SigHash, Simplicity.Elements.Programs.SigHash.Lib,
                        Simplicity.Elements.Programs.Transaction, Simplicity.Elements.Programs.Transaction.Lib,
                        Simplicity.Bitcoin.Jets, Simplicity.Elements.Jets,
                        Simplicity.Elements.FFI.Env, Simplicity.Elements.FFI.Jets
-  reexported-modules:  Simplicity.Ty, Simplicity.Ty.Bit, Simplicity.Ty.Word, Simplicity.Ty.LibSecp256k1,
+  reexported-modules:  Simplicity.Ty, Simplicity.Ty.Bit, Simplicity.Ty.Word, Simplicity.Ty.LibSecp256k1, Simplicity.Ty.Sha256,
                        Simplicity.Term.Core,
                        Simplicity.CoreJets,
                        Simplicity.Functor, Simplicity.Tensor,
@@ -149,6 +151,7 @@ library
                        Simplicity.Programs.Sha256, Simplicity.Programs.Sha256.Lib,
                        Simplicity.Programs.LibSecp256k1, Simplicity.Programs.LibSecp256k1.Lib,
                        Simplicity.Programs.CheckSig, Simplicity.Programs.CheckSig.Lib,
+                       Simplicity.Programs.Bitcoin, Simplicity.Programs.Bitcoin.Lib,
                        Simplicity.Programs.Elements, Simplicity.Programs.Elements.Lib,
                        Simplicity.Programs.TimeLock,
                        Simplicity.Digest,
@@ -224,8 +227,9 @@ Test-Suite testsuite
   ghc-options:         -threaded -O0 -with-rtsopts=-c
   other-modules:       Simplicity.Programs.Example,
                        Simplicity.Bip0340,
-                       Simplicity.Arbitrary, Simplicity.Ty.Arbitrary, Simplicity.Elements.Arbitrary,
+                       Simplicity.Arbitrary, Simplicity.Ty.Arbitrary, Simplicity.Bitcoin.Arbitrary, Simplicity.Elements.Arbitrary,
                        Simplicity.BitMachine.StaticAnalysis.Tests, Simplicity.BitMachine.Tests,
+                       Simplicity.Bitcoin.TestEval, Simplicity.Bitcoin.Tests,
                        Simplicity.Bitcoin.Serialization.Tests,
                        Simplicity.FFI.Bitstream, Simplicity.FFI.Dag,
                        Simplicity.Elements.FFI.Primitive,