[BTC Language] OP_CHECKLOCKTIME implementation

symbolic_execution/language/bitcoin/op_codes.py

@@ -18,6 +18,11 @@ from symbolic_execution.program.instruction.stack_based import (
     SwapDataOperator,
 )
 from symbolic_execution.hardware.machines.btc_machine import BTCVector, BTCMachine
+from z3 import And, Int, Or
+
+# Special Bitcoin Fields
+nLockTime = Int("nLockTime")
+nSequence = Int("nSequence")
 
 
 def arithmetic_constraint_on_operands_size(op: BTCVector):
@@ -32,6 +37,36 @@ def arithmetic_constraint_on_operands_size(op: BTCVector):
     return op.size == BTCVector._min_bytes_needed(op.val)
 
 
+def locktime_constraint(op: BTCVector):
+    """Return a constraint to mimic OP_CHECKLOCKTIMEVERIFY specification.
+
+    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
+        * the input's nSequence field != 0xffffffff.
+    while it must stay positive.
+    """
+    LOCKTIME_THRESHOLD = 500000000
+
+    condition = And(
+        op.val <= nLockTime,
+        op.val >= 0,
+        Or(
+            And(nLockTime > LOCKTIME_THRESHOLD, op.val >= LOCKTIME_THRESHOLD),
+            And(nLockTime < LOCKTIME_THRESHOLD, op.val < LOCKTIME_THRESHOLD),
+        ),
+        nSequence != 0xFFFFFFFF,
+    )
+
+    return condition
+
+
+def id(a):
+    """Id function."""
+    return a
+
+
 class OpCode:
     """Represent an opcode in a language."""
 
@@ -654,15 +689,17 @@ class OpCodes:
         ),
         # expansion
         "OP_NOP1": OpCode("OP_NOP1", instruction_constructor=NOP),
-        # TODO implement
         "OP_CHECKLOCKTIME": OpCode(
             "OP_CHECKLOCKTIME",
-            instruction_constructor=InvalidInstruction,
+            instruction_constructor=ArithmeticOperator,
             default_args={
-                "token": "OP_CHECKLOCKTIME",
-                "tag": InstructionTag.NOT_IMPLEMENTED,
+                "arity": 1,
+                "operator": id,
+                "symbol": "check_lock_time",
+                "constraint_on_operands": locktime_constraint,
             },
         ),
+        # TODO implement
         "OP_CHECKSEQUENCE": OpCode(
             "OP_CHECKSEQUENCE",
             instruction_constructor=InvalidInstruction,