[BTC Language] OP_CHECKSEQUENCEVERIFY implementation

symbolic_execution/hardware/machines/btc_machine.py

 """Implementation of a stack-based machine able to run Bitcoin scripts."""
 from copy import deepcopy
-import hashlib
 from math import ceil, floor, log2
 from typing import Any, Callable, Dict, List, Tuple
 from symbolic_execution.hardware.memory.ram import Word
@@ -280,6 +279,10 @@ class BTCVector:
 
         return hash_of_vector
 
+    def __identity__(self):
+        """Return self"""
+        return self
+
 
 BTC_VECTOR_1 = BTCVector(IntVal(1), BTCVector._min_bytes_needed(1))
 

symbolic_execution/language/bitcoin/op_codes.py

@@ -25,6 +25,7 @@ from Crypto.Hash import RIPEMD160
 # Special Bitcoin Fields
 nLockTime = Int("nLockTime")
 nSequence = Int("nSequence")
+version = Int("version")
 
 
 def arithmetic_constraint_on_operands_size(op: BTCVector):
@@ -45,13 +46,15 @@ def locktime_constraint(op: BTCVector):
     The conditions are:
         * top stack item <= the transaction's nLockTime field;
         * top stack item >= 0
-        * If the transaction's nLockTime field >= 500000000, then top stack item >= 500000000
+        * If the transaction's nLockTime field >= 500000000,
+          then top stack item >= 500000000
         * the input's nSequence field != 0xffffffff.
     while it must stay positive.
     """
     LOCKTIME_THRESHOLD = 500000000
 
     condition = And(
+        op.size <= 5,
         op.val <= nLockTime,
         op.val >= 0,
         Or(
@@ -64,9 +67,47 @@ def locktime_constraint(op: BTCVector):
     return condition
 
 
-def id(a):
-    """Id function."""
-    return a
+def sequence_constraint(op: BTCVector):
+    """Return a constraint to mimic OP_CHECKSEQUENCEVERIFY specification.
+
+    The conditions are:
+        * the top item is >= 0
+        * the top item has the disable flag (1 << 31) set; or
+            * the transaction version >= 2; and
+            * the transaction input sequence number disable flag (1 << 31) is unset; and
+            * the relative lock-time type is the same; and
+            * the top stack item is smaller or equal than the
+              transaction input sequence (when masked according to the BIP68);
+
+    Note: we don't need to implement the condition relative to the relative locktime,
+    because an unsafe script that can't be unlocked right now should still be considered
+    unsafe.
+
+    See https://github.com/bitcoin/bips/blob/master/bip-0112.mediawiki
+    """
+
+    def disable_flag(val):
+        """Return the 32nd bit of the vector."""
+        return (val % (2 ** 32)) / (2 ** 31)
+
+    def lock_time_type_flag(val):
+        """Return the 23th bit of the vector."""
+        return (val % (2 ** 23)) / (2 ** 22)
+
+    condition = And(
+        op.size <= 5,
+        op.val >= 0,
+        Or(
+            And(
+                version >= 2,
+                disable_flag(nSequence) == 0,
+                lock_time_type_flag(op.val) == lock_time_type_flag(nSequence),
+                op.val <= nSequence,
+            )
+        ),
+    )
+
+    return condition
 
 
 class OpCode:
@@ -695,17 +736,19 @@ class OpCodes:
             instruction_constructor=ArithmeticOperator,
             default_args={
                 "arity": 1,
-                "operator": id,
+                "operator": BTCVector.__identity__,
                 "symbol": "check_lock_time",
                 "constraint_on_operands": locktime_constraint,
             },
-        ),  # TODO implement
+        ),
         "OP_CHECKSEQUENCE": OpCode(
             "OP_CHECKSEQUENCE",
-            instruction_constructor=InvalidInstruction,
+            instruction_constructor=ArithmeticOperator,
             default_args={
-                "token": "OP_CHECKSEQUENCE",
-                "tag": InstructionTag.NOT_IMPLEMENTED,
+                "arity": 1,
+                "operator": BTCVector.__identity__,
+                "symbol": "check_sequence",
+                "constraint_on_operands": sequence_constraint,
             },
         ),
         "OP_NOP4": OpCode("OP_NOP4", instruction_constructor=NOP),