Add a verify jet.

C/jets.c

@@ -1,17 +1,24 @@
 #include "jets.h"
 
+/* verify : TWO |- ONE */
+bool verify(frameItem* dst, frameItem src, const txEnv* env) {
+  (void) env; // env is unused;
+  (void) dst; // dst is unused;
+  return readBit(&src);
+}
+
 /* low_32 : ONE |- TWO^32 */
 bool low_32(frameItem* dst, frameItem src, const txEnv* env) {
   (void) env; // env is unused;
-  (void) src; // env is unused;
+  (void) src; // src is unused;
   write32(dst, 0);
   return true;
 }
 
 /* one_32 : ONE |- TWO^32 */
 bool one_32(frameItem* dst, frameItem src, const txEnv* env) {
   (void) env; // env is unused;
-  (void) src; // env is unused;
+  (void) src; // src is unused;
   write32(dst, 1);
   return true;
 }

C/jets.h

@@ -21,6 +21,7 @@ typedef struct txEnv txEnv;
  */
 typedef bool (*jet_ptr)(frameItem* dst, frameItem src, const txEnv* env);
 
+bool verify(frameItem* dst, frameItem src, const txEnv* env);
 bool low_32(frameItem* dst, frameItem src, const txEnv* env);
 bool one_32(frameItem* dst, frameItem src, const txEnv* env);
 bool eq_32(frameItem* dst, frameItem src, const txEnv* env);

C/primitive/elements/checkSigHashAllTx1.c

@@ -8,17 +8,17 @@
  * with jets.
  */
 const unsigned char elementsCheckSigHashAllTx1[] = {
-  0xe4, 0x7e, 0x31, 0x10, 0x92, 0x04, 0x08, 0x10, 0x20, 0xb9, 0x08, 0x16, 0x41, 0x5d, 0x02, 0x51, 0x50, 0xb4, 0x05, 0xa0,
-  0x2d, 0xba, 0x04, 0xd0, 0x2c, 0xf7, 0x0a, 0x05, 0xaf, 0x80, 0x0b, 0x66, 0xa1, 0x40, 0xb0, 0x0b, 0x46, 0x81, 0x69, 0xdc,
-  0x28, 0x17, 0x02, 0xe0, 0x42, 0xe0, 0x41, 0x50, 0xb3, 0x0b, 0x80, 0x05, 0xc3, 0xc2, 0xe0, 0xdc, 0x04, 0x5c, 0x00, 0x2e,
-  0x11, 0xc2, 0x04, 0xe1, 0xe2, 0xa1, 0x70, 0xde, 0x0c, 0x2e, 0x04, 0x17, 0x08, 0xe2, 0x41, 0x68, 0x0a, 0x85, 0x90, 0x5c,
-  0x51, 0xc3, 0x04, 0xc4, 0x5c, 0x0f, 0x83, 0x0a, 0x05, 0xb7, 0x68, 0xb8, 0xb7, 0x89, 0x84, 0xe2, 0x01, 0x50, 0xb1, 0x0b,
-  0x50, 0x5c, 0x0f, 0x80, 0x0b, 0x8c, 0xb8, 0x08, 0xa0, 0x5c, 0x23, 0x88, 0x05, 0xc1, 0x38, 0x84, 0x50, 0x2c, 0x02, 0xe2,
-  0xce, 0x18, 0x2e, 0x26, 0xe2, 0x31, 0x40, 0xb8, 0x7f, 0x16, 0x0b, 0x8a, 0x38, 0xdc, 0x50, 0x2c, 0x02, 0xd0, 0x17, 0x00,
-  0x0b, 0x89, 0x88, 0xe0, 0xe0, 0x58, 0x1c, 0x51, 0xb1, 0x02, 0x3d, 0x20, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
-  0x00, 0x00, 0x00, 0x03, 0xb7, 0x8c, 0xe5, 0x63, 0xf8, 0x9a, 0x0e, 0xd9, 0x41, 0x4f, 0x5a, 0xa2, 0x8a, 0xd0, 0xd9, 0x6d,
-  0x67, 0x95, 0xf9, 0xc6, 0x30, 0x1d, 0xfe, 0x15, 0xb3, 0xbc, 0x1f, 0xf8, 0x53, 0x41, 0x12, 0xdf, 0x20, 0x0e, 0x93, 0x0d,
-  0x94, 0xcc, 0xb0, 0x80, 0xb3, 0x36, 0xb2, 0x67, 0x12, 0x5f, 0x8e, 0x76, 0x83, 0xca, 0x3d, 0x50, 0x50
+  0xe4, 0x7e, 0x4c, 0x44, 0x24, 0x81, 0x02, 0x04, 0x08, 0x2e, 0x42, 0x05, 0x90, 0x57, 0x40, 0x94, 0x54, 0x2d, 0x01, 0x68,
+  0x0b, 0x6e, 0x81, 0x34, 0x0b, 0x3d, 0xc2, 0x81, 0x6b, 0xe0, 0x02, 0xd9, 0xa8, 0x50, 0x2c, 0x02, 0xd1, 0xa0, 0x5a, 0x77,
+  0x0a, 0x05, 0xc0, 0xb8, 0x10, 0xb8, 0x10, 0x54, 0x2c, 0xc2, 0xe0, 0x01, 0x70, 0xf0, 0xb8, 0x37, 0x01, 0x17, 0x00, 0x0b,
+  0x84, 0x70, 0x81, 0x38, 0x78, 0xa8, 0x5c, 0x37, 0x83, 0x0b, 0x81, 0x05, 0xc2, 0x38, 0x90, 0x5a, 0x02, 0xa1, 0x64, 0x17,
+  0x14, 0x70, 0xc1, 0x31, 0x17, 0x03, 0xe0, 0xc2, 0x81, 0x6d, 0xda, 0x2e, 0x2d, 0xe2, 0x61, 0x38, 0x80, 0x54, 0x2c, 0x42,
+  0xd4, 0x17, 0x03, 0xe0, 0x02, 0xe3, 0x2e, 0x02, 0x28, 0x17, 0x08, 0xe2, 0x01, 0x70, 0x4e, 0x21, 0x14, 0x0b, 0x00, 0xb8,
+  0xb3, 0x86, 0x0b, 0x89, 0xb8, 0x8c, 0x50, 0x2e, 0x1f, 0xc5, 0x82, 0xe2, 0x8e, 0x37, 0x14, 0x0b, 0x00, 0xb4, 0x05, 0xc0,
+  0x02, 0xe2, 0x62, 0x38, 0x38, 0x16, 0x07, 0x14, 0x6c, 0x40, 0x8f, 0x48, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
+  0x00, 0x00, 0x00, 0x00, 0xed, 0xe3, 0x39, 0x58, 0xfe, 0x26, 0x83, 0xb6, 0x50, 0x53, 0xd6, 0xa8, 0xa2, 0xb4, 0x36, 0x5b,
+  0x59, 0xe5, 0x7e, 0x71, 0x8c, 0x07, 0x7f, 0x85, 0x6c, 0xef, 0x07, 0xfe, 0x14, 0xd0, 0x44, 0xb7, 0xc8, 0x03, 0xa4, 0xc3,
+  0x65, 0x33, 0x2c, 0x20, 0x2c, 0xcd, 0xac, 0x99, 0xc4, 0x97, 0xe3, 0x9d, 0xa0, 0xf2, 0x8f, 0x54, 0x14
 };
 
 const size_t sizeof_elementsCheckSigHashAllTx1 = sizeof(elementsCheckSigHashAllTx1);

C/primitive/elements/primitive.c

@@ -84,14 +84,16 @@ static int32_t decodePrimitive(jetName* result, bitstream* stream) {
         code = decodeUptoMaxInt(stream);
         if (code < 0) return code;
         switch (code) {
-         case 1: /* Low */
+         case 1: /* Verify */
+          *result = VERIFY; return 0;
+         case 2: /* Low */
           code = decodeUptoMaxInt(stream);
           if (code < 0) return code;
           switch (code) {
            case 5: *result = LOW_32; return 0;
           }
           break;
-         case 12: /* Eq */
+         case 13: /* Eq */
           code = decodeUptoMaxInt(stream);
           if (code < 0) return code;
           switch (code) {

C/primitive/elements/primitiveEnumJet.inc

@@ -160,4 +160,5 @@ TX_LOCK_DISTANCE,
 TX_LOCK_DURATION,
 TX_LOCK_HEIGHT,
 TX_LOCK_TIME,
+VERIFY,
 VERSION,

C/primitive/elements/primitiveInitJet.inc

@@ -160,4 +160,5 @@ MK_JET(TX_LOCK_DISTANCE, 0xccfdc62au, 0xed510ca0u, 0xdaeeffb5u, 0x0c6dabc1u, 0x1
 MK_JET(TX_LOCK_DURATION, 0x8526e3d4u, 0x3f43bd2bu, 0x4b1985c0u, 0xb9301d9au, 0x98290167u, 0xe587e5c3u, 0xcf135bc6u, 0xb1231346u);
 MK_JET(TX_LOCK_HEIGHT, 0xf94f86a6u, 0xf07995ddu, 0xcdf8ccafu, 0xdeea8e58u, 0x450bcac4u, 0xde783597u, 0xf86ab089u, 0xeb64f7fcu);
 MK_JET(TX_LOCK_TIME, 0xd44ce14cu, 0xcfb3a1bcu, 0xb71210c0u, 0xa2e15bc9u, 0xf5c9a251u, 0x29a037beu, 0x483f16c3u, 0xa505db59u);
+MK_JET(VERIFY, 0xa17534a4u, 0x9acbecb1u, 0x554d6ec5u, 0xc6da50c2u, 0x8c9cd95eu, 0xa0b44886u, 0xb8e094adu, 0xa777c1d4u);
 MK_JET(VERSION, 0xd3cadcbdu, 0xaf57f8e5u, 0xb48eb763u, 0x8c75438du, 0x67376c79u, 0xb4cf70b2u, 0x582e32d9u, 0x31c42cdfu);

C/primitive/elements/primitiveJetNode.inc

@@ -965,6 +965,12 @@
 , .sourceIx = ty_u
 , .targetIx = ty_w32
 }
+,[VERIFY] =
+{ .tag = JET
+, .jet = verify
+, .sourceIx = ty_b
+, .targetIx = ty_u
+}
 ,[VERSION] =
 { .tag = JET
 , .jet = version

C/schnorr0.c

@@ -16,11 +16,11 @@ const unsigned char schnorr0[] = {
   0x13, 0x86, 0x0b, 0x8a, 0xb8, 0x8c, 0x50, 0x2e, 0x19, 0xc5, 0x02, 0xe0, 0xfc, 0x40, 0x28, 0x16, 0x01, 0x71, 0x67, 0x18,
   0x0b, 0x8d, 0x78, 0xd8, 0x4e, 0x39, 0x15, 0x0b, 0x8d, 0xf8, 0xdc, 0x5b, 0x78, 0xd0, 0x50, 0x2c, 0x02, 0xd2, 0x17, 0x1a,
   0xe8, 0x13, 0x8c, 0x85, 0xc8, 0x2e, 0x34, 0x17, 0x1a, 0xf1, 0xe0, 0xa0, 0x58, 0x05, 0xc1, 0xf8, 0xbc, 0x5c, 0x88, 0xe4,
-  0x28, 0x9c, 0x80, 0x15, 0x0b, 0x90, 0x7c, 0x08, 0x4e, 0x43, 0x0a, 0x85, 0xa0, 0x2d, 0xe1, 0x71, 0x0b, 0x18, 0x88, 0x10,
-  0x20, 0x58, 0x9c, 0x51, 0xb1, 0x80, 0x8f, 0x48, 0x03, 0xa4, 0x1e, 0x0c, 0x7e, 0x02, 0x12, 0x34, 0x41, 0xa6, 0x94, 0xdc,
-  0x6d, 0x00, 0x90, 0x40, 0xd9, 0x2f, 0x7c, 0x71, 0x7e, 0x0c, 0x1e, 0xc0, 0x21, 0x31, 0x57, 0xc7, 0x38, 0xb7, 0x2a, 0x08,
-  0x54, 0x97, 0xd9, 0xa9, 0x2a, 0x17, 0xaa, 0x2d, 0xc7, 0x92, 0x0a, 0x9d, 0x3c, 0xe0, 0xb4, 0xb3, 0x97, 0xaf, 0xbb, 0xa3,
-  0xf6, 0xc8, 0x5c, 0xbd, 0x1d, 0xf7, 0xd2, 0x40, 0x34, 0xc4, 0x14, 0xdb, 0x00
+  0x28, 0x9c, 0x80, 0x15, 0x0b, 0x90, 0x7c, 0x08, 0x4e, 0x43, 0x0a, 0x85, 0xa0, 0x2d, 0xe1, 0x71, 0x0b, 0x26, 0x22, 0x04,
+  0x08, 0x16, 0x27, 0x14, 0x6c, 0x60, 0x23, 0xd2, 0x00, 0xe9, 0x07, 0x83, 0x1f, 0x80, 0x84, 0x8d, 0x10, 0x69, 0xa5, 0x37,
+  0x1b, 0x40, 0x24, 0x10, 0x36, 0x4b, 0xdf, 0x1c, 0x5f, 0x83, 0x07, 0xb0, 0x08, 0x4c, 0x55, 0xf1, 0xce, 0x2d, 0xca, 0x82,
+  0x15, 0x25, 0xf6, 0x6a, 0x4a, 0x85, 0xea, 0x8b, 0x71, 0xe4, 0x82, 0xa7, 0x4f, 0x38, 0x2d, 0x2c, 0xe5, 0xeb, 0xee, 0xe8,
+  0xfd, 0xb2, 0x17, 0x2f, 0x47, 0x7d, 0xf4, 0x90, 0x0d, 0x31, 0x05, 0x36, 0xc0
 };
 
 const size_t sizeof_schnorr0 = sizeof(schnorr0);

Haskell/Core/Simplicity/CoreJets.hs

@@ -27,6 +27,7 @@ import Simplicity.Digest
 import Simplicity.FFI.Jets as FFI
 import Simplicity.MerkleRoot
 import Simplicity.Serialization
+import Simplicity.Programs.Bit as Prog
 import Simplicity.Programs.Arith as Prog
 import Simplicity.Programs.Generic as Prog
 import qualified Simplicity.Programs.CheckSig.Lib as CheckSig
@@ -49,6 +50,7 @@ deriving instance Eq (CoreJet a b)
 deriving instance Show (CoreJet a b)
 
 data WordJet a b where
+  Verify :: WordJet Bit ()
   Low32 :: WordJet () Word32
   Eq32 :: WordJet (Word32, Word32) Bit
   Eq256 :: WordJet (Word256, Word256) Bit
@@ -150,6 +152,7 @@ specification (SignatureJet x) = specificationSignature x
 specification (BitcoinJet x) = specificationBitcoin x
 
 specificationWord :: Assert term => WordJet a b -> term a b
+specificationWord Verify = assert iden
 specificationWord Low32 = zero word32
 specificationWord Eq32 = eq
 specificationWord Eq256 = eq
@@ -243,6 +246,7 @@ implementation (SignatureJet x) = implementationSignature x
 implementation (BitcoinJet x) = implementationBitcoin x
 
 implementationWord :: WordJet a b -> a -> Maybe b
+implementationWord Verify = either (const Nothing) Just
 implementationWord Low32 = const . return $ toWord32 0
 implementationWord Eq32 = \(x, y) -> return (toBit (x == y))
 implementationWord Eq256 = \(x, y) -> return (toBit (x == y))
@@ -373,8 +377,9 @@ getJetBit abort next =  getPositive next >>= match
   getJetBitWord :: (Monad m) => m Void -> m Bool -> m (SomeArrow WordJet)
   getJetBitWord abort next = getPositive next >>= matchWord
    where
-    matchWord 1 = getPositive next >>= matchLow
-    matchWord 12 = getPositive next >>= matchEq
+    matchWord 1 = makeArrow Verify
+    matchWord 2 = getPositive next >>= matchLow
+    matchWord 13 = getPositive next >>= matchEq
     matchLow 5 = makeArrow Low32
     matchLow _ = vacuous abort
     matchEq 5 = makeArrow Eq32
@@ -501,9 +506,10 @@ putJetBit (SignatureJet x) = putPositive 5 . putJetBitSignature x
 putJetBit (BitcoinJet x) = putPositive 7 . putJetBitBitcoin x
 
 putJetBitWord :: WordJet a b -> DList Bool
-putJetBitWord Low32 = putPositive 1 . putPositive 5
-putJetBitWord Eq32 = putPositive 12 . putPositive 5
-putJetBitWord Eq256 = putPositive 12 . putPositive 8
+putJetBitWord Verify = putPositive 1 . putPositive 5
+putJetBitWord Low32  = putPositive 2 . putPositive 5
+putJetBitWord Eq32   = putPositive 13 . putPositive 5
+putJetBitWord Eq256  = putPositive 13 . putPositive 8
 
 putJetBitArith :: ArithJet a b -> DList Bool
 putJetBitArith One32          = putPositive 1 . putPositive 5
@@ -585,7 +591,8 @@ putJetBitBitcoin ParseSequence  = putPositive 2
 coreJetMap :: Map.Map Hash256 (SomeArrow CoreJet)
 coreJetMap = Map.fromList
   [ -- WordJet
-    mkAssoc (WordJet Low32)
+    mkAssoc (WordJet Verify)
+  , mkAssoc (WordJet Low32)
   , mkAssoc (WordJet Eq32)
   , mkAssoc (WordJet Eq256)
     -- ArithJet

Haskell/Core/Simplicity/FFI/Jets.hs

@@ -1,7 +1,8 @@
 -- | This module binds the C implementation of jets for Simplicity for assertions.
 {-# LANGUAGE ForeignFunctionInterface #-}
 module Simplicity.FFI.Jets
- ( low_32, one_32
+ ( verify
+ , low_32, one_32
  , eq_32, eq_256
  , add_32, full_add_32
  , subtract_32, full_subtract_32
@@ -40,6 +41,7 @@ import Simplicity.Programs.LibSecp256k1.Lib (FE, Scalar, GE, GEJ, Point, PubKey,
 import qualified Simplicity.Programs.LibSecp256k1.Lib as LibSecp256k1
 import Simplicity.Ty.Word
 
+foreign import ccall unsafe "" c_verify :: Ptr FrameItem -> Ptr FrameItem -> IO CBool
 foreign import ccall unsafe "" c_low_32 :: Ptr FrameItem -> Ptr FrameItem -> IO CBool
 foreign import ccall unsafe "" c_one_32 :: Ptr FrameItem -> Ptr FrameItem -> IO CBool
 foreign import ccall unsafe "" c_eq_32 :: Ptr FrameItem -> Ptr FrameItem -> IO CBool
@@ -111,6 +113,9 @@ foreign import ccall unsafe "" c_bip_0340_verify :: Ptr FrameItem -> Ptr FrameIt
 foreign import ccall unsafe "" c_parse_lock :: Ptr FrameItem -> Ptr FrameItem -> IO CBool
 foreign import ccall unsafe "" c_parse_sequence :: Ptr FrameItem -> Ptr FrameItem -> IO CBool
 
+verify :: Bit -> Maybe ()
+verify = unsafeLocalCoreJet c_verify
+
 low_32 :: () -> Maybe Word32
 low_32 = unsafeLocalCoreJet c_low_32
 

Haskell/Tests/Simplicity/FFI/Tests.hs

@@ -30,7 +30,8 @@ main = defaultMain tests
 tests :: TestTree
 tests = testGroup "C / SPEC"
       [ testGroup "word" $
-        [ testCase     "low_32" assert_low_32
+        [ testCase     "verify" assert_verify
+        , testCase     "low_32" assert_low_32
         , testProperty "eq_32"  prop_eq_32
         , testProperty "eq_256"  prop_eq_256
         ]
@@ -141,6 +142,13 @@ tests = testGroup "C / SPEC"
         , testProperty "check_sig_verify_true" prop_check_sig_verify_true
         ]
       ]
+assert_verify :: Assertion
+assert_verify =
+  (fastF (toBit False), fastF (toBit True))
+    @=?
+  (verify (toBit False), verify (toBit True))
+ where
+  fastF = testCoreEval (specification (WordJet Verify))
 
 assert_low_32 :: Assertion
 assert_low_32 = fastF () @=? C.low_32 ()

Haskell/Tests/Simplicity/Programs/Tests.hs

@@ -51,7 +51,8 @@ toW16 = toWord16 . fromIntegral
 tests :: TestTree
 tests = testGroup "Programs"
       [ testGroup "Word"
-        [ testCase "low word8" assert_low8
+        [ testCase "verify" assert_verify
+        , testCase "low word8" assert_low8
         , testCase "high word8" assert_high8
         , testCase "low_32" assert_low_32
         , testProperty "compelment word8" prop_complement8
@@ -189,6 +190,15 @@ tests = testGroup "Programs"
         ]
       ]
 
+assert_verify :: Assertion
+assert_verify =
+  (fastF (toBit False), fastF (toBit True))
+    @=?
+  (implF (toBit False), implF (toBit True))
+ where
+  fastF = testCoreEval (specification (WordJet Verify))
+  implF = implementation (WordJet Verify)
+
 assert_low8 :: Assertion
 assert_low8 = 0 @=? fromWord8 (low word8 ())
 

Haskell/cbits/coreJets.c

@@ -1,6 +1,7 @@
 #include "jets.h"
 #include "wrappers.h"
 
+COREWRAP_(verify)
 COREWRAP_(low_32)
 COREWRAP_(one_32)
 COREWRAP_(eq_32)