[BTC Language] Hash functions implemented.

symbolic_execution/hardware/machines/btc_machine.py

@@ -23,6 +23,7 @@ from z3 import (
     BitVecRef,
     Or,
     ExprRef,
+    Function,
 )
 
 from ..interfaces import (
@@ -194,20 +195,44 @@ class BTCVector:
         """If the input is 0 or 1, it is flipped. Otherwise the output will be 0."""
         return BTCVector(
             If(self.val == 0, self.BTC_TRUE, self.BTC_FALSE),
-            IntVal(8),  # True and False are always encoded on 1 byte.
+            IntVal(1),  # True and False are always encoded on 1 byte.
         )
 
     def __num_eq__(self, other):
         """Return the BTC vector `True` if `self.val == other.val`."""
         return BTCVector(
             If(self.val == other.val, self.BTC_TRUE, self.BTC_FALSE),
-            IntVal(8),  # True and False are always encoded on 1 byte.
+            IntVal(1),  # True and False are always encoded on 1 byte.
         )
 
     def __size__(self):
         """Return the number of bytes the vector is composed of."""
         return BTCVector(self.size, self._min_bytes_needed(self.size))
 
+    def __ripemd160__(self):
+        """Return a symbol that stands for the ripemd160 hash of the vector."""
+        f = Function('ripemd160', IntSort(), IntSort())
+        return BTCVector(f(self.val), IntVal(20))
+    
+    def __sha1__(self):
+        """Return a symbol that stands for the sha1 hash of the vector."""
+        f = Function('sha1', IntSort(), IntSort())
+        return BTCVector(f(self.val), IntVal(20))
+    
+    def __sha256__(self):
+        """Return a symbol that stands for the sha256 hash of the vector."""
+        f = Function('sha256', IntSort(), IntSort())
+        return BTCVector(f(self.val), IntVal(32))
+    
+    def __hash160__(self):
+        """Return a symbol that stands for the hash160 hash of the vector."""
+        f = Function('hash160', IntSort(), IntSort())
+        return BTCVector(f(self.val), IntVal(20))
+    
+    def __hash256__(self):
+        """Return a symbol that stands for the hash256 hash of the vector."""
+        f = Function('hash256', IntSort(), IntSort())
+        return BTCVector(f(self.val), IntVal(32))
 
 BTC_VECTOR_1 = BTCVector(IntVal(1), BTCVector._min_bytes_needed(1))
 

symbolic_execution/language/bitcoin/op_codes.py

@@ -634,34 +634,52 @@ class OpCodes:
                 "constraint_on_operands": arithmetic_constraint_on_operands_size,
             },
         ),
-        # TODO implement crypto
         "OP_RIPEMD160": OpCode(
             "OP_RIPEMD160",
-            instruction_constructor=InvalidInstruction,
+            instruction_constructor=ArithmeticOperator,
             default_args={
-                "token": "OP_RIPEMD160",
-                "tag": InstructionTag.NOT_IMPLEMENTED,
+                "arity": 1,
+                "operator": BTCVector.__ripemd160__,
+                "symbol": "ripemd160",
             },
         ),
         "OP_SHA1": OpCode(
             "OP_SHA1",
-            instruction_constructor=InvalidInstruction,
-            default_args={"token": "OP_SHA1", "tag": InstructionTag.NOT_IMPLEMENTED},
+            instruction_constructor=ArithmeticOperator,
+            default_args={
+                "arity": 1,
+                "operator": BTCVector.__sha1__,
+                "symbol": "sha1",
+            },
         ),
+        # TODO implement crypto
         "OP_SHA256": OpCode(
             "OP_SHA256",
-            instruction_constructor=InvalidInstruction,
-            default_args={"token": "OP_SHA256", "tag": InstructionTag.NOT_IMPLEMENTED},
+            instruction_constructor=ArithmeticOperator,
+            default_args={
+                "arity": 1,
+                "operator": BTCVector.__sha256__,
+                "symbol": "sha256",
+            },
         ),
         "OP_HASH160": OpCode(
             "OP_HASH160",
-            instruction_constructor=InvalidInstruction,
-            default_args={"token": "OP_HASH160", "tag": InstructionTag.NOT_IMPLEMENTED},
+            instruction_constructor=ArithmeticOperator,
+            default_args={
+                "arity": 1,
+                "operator": BTCVector.__hash160__,
+                "symbol": "hash160",
+            },
         ),
         "OP_HASH256": OpCode(
             "OP_HASH256",
-            instruction_constructor=InvalidInstruction,
-            default_args={"token": "OP_HASH256", "tag": InstructionTag.NOT_IMPLEMENTED},
+            instruction_constructor=ArithmeticOperator,
+            default_args={
+                "arity": 1,
+                "operator": BTCVector.__hash256__,
+                "symbol": "hash256",
+                "constraint_on_operands": arithmetic_constraint_on_operands_size,
+            },
         ),
         "OP_CODESEPARATOR": OpCode(
             "OP_CODESEPARATOR",