diff --git a/symbolic_execution/hardware/interfaces.py b/symbolic_execution/hardware/interfaces.py index d867ac3f3699c03167a89724375cc8b698bf90e1..8174e83e87153d49445c1ea0841f933b1af8ea2a 100644 --- a/symbolic_execution/hardware/interfaces.py +++ b/symbolic_execution/hardware/interfaces.py @@ -124,6 +124,11 @@ class IStackBasedMachine(IMachine): """ pass + @abstractmethod + def drop_from_stack(self, drop_n: int, n: int = 0) -> int: + """Drop {drop_n} elements from the stack {n} and return the new position.""" + pass + @abstractmethod def count_stack_elements(self, n: int = 0) -> int: """Return the number of elements on the stack {n}.""" diff --git a/symbolic_execution/hardware/machines/btc_machine.py b/symbolic_execution/hardware/machines/btc_machine.py index 0d9b7fe220b6cf60f01d16b1f9428a65b0b84367..7dad13fa67b6671a0cc91d45430a71e5e410dd74 100644 --- a/symbolic_execution/hardware/machines/btc_machine.py +++ b/symbolic_execution/hardware/machines/btc_machine.py @@ -305,9 +305,11 @@ class BTCVector: return self def check_sig(pubkeys: list, signatures: list): - """Check a list of signatures against a list of public keys.""" + """Check a signature against a public key.""" # TODO Could be refined. We could compute the signature in case both signature # and key are constants. + if len(pubkeys) != 1 and len(signatures) != 1: + raise ValueError("One public key and one signature are expected.") ret = CHECK_SINGLE_SIG(pubkeys[0].val, signatures[0].val) return BTCVector( @@ -315,6 +317,25 @@ class BTCVector: If(ret == BoolVal(False), IntVal(0), IntVal(1)), ) + def check_multisig(pubkeys_cnt, sigs_cnt): + """Check a list of signatures against a list of public keys.""" + # TODO Could be refined. We could compute the signature in case both signature + # and key are constants. + + # If the number of keys is not hardcoded, it is possible to alter it and pass + # more keys + if not is_int_value(pubkeys_cnt): + return BTCVector( + BTCVector.BTC_TRUE, + IntVal(1) + ) + + return BTCVector( + BTCVector.BTC_FALSE, + IntVal(0) + ) + + def is_result_of_hash(self): def parse_ast(e): if e.decl().name() == "if": @@ -508,6 +529,13 @@ class BTCMachine(IStackBasedMachine, IRAMBasedMachine, ISymbolicMachine): self._stack_sizes[n] -= 1 return BTCVector(top_word.val, top_word.size) + @_check_nth_stack + def drop_from_stack(self, drop_n: int, n: int = 0) -> int: + """Drop {drop_n} elements from the stack {n}.""" + self._mem_pos[n] -= drop_n.val + + return self._mem_pos[n] + @_check_nth_stack def count_stack_elements(self, n: int = 0) -> BTCVector: """Return the number of elements on the stack {n}.""" diff --git a/symbolic_execution/language/bitcoin/op_codes.py b/symbolic_execution/language/bitcoin/op_codes.py index c75142d00c522ec546cb46da6cca18e630603328..3550a6506535e3987a048255ef9ad9c6064a40cc 100644 --- a/symbolic_execution/language/bitcoin/op_codes.py +++ b/symbolic_execution/language/bitcoin/op_codes.py @@ -1,6 +1,6 @@ """Code by Vincent Jacquot - University of Liège.""" import operator -from typing import Any, Callable, Dict, List +from typing import Any, Callable, Dict, List, Tuple from symbolic_execution.language.exceptions import InvalidOpCode from symbolic_execution.program.instruction.general import ( NOP, @@ -13,6 +13,7 @@ from symbolic_execution.program.instruction.hybrid import PickInstruction from symbolic_execution.program.instruction.interfaces import IInstruction from symbolic_execution.program.instruction.stack_based import ( ArithmeticOperator, + CheckMultiSigInstruction, CheckSigInstruction, ConditionalJump, PushDataOperator, @@ -737,13 +738,10 @@ class OpCodes: instruction_constructor=CheckSigInstruction, default_args={"sig_function": BTCVector.check_sig, "constraint_on_operands": signature_constraints}, ), - # TODO implementing multisig requires to support symbolic block read - # i.e. the ability to read `n` elements from the stack, `n` being symbolic - # In the meanwhile, let's suppose the result is always false. "OP_CHECKMULTISIG": OpCode( "OP_CHECKMULTISIG", - instruction_constructor=PushDataOperator, - default_args={"data": 0}, + instruction_constructor=CheckMultiSigInstruction, + default_args={"sig_function": BTCVector.check_multisig}, ), # expansion "OP_NOP1": OpCode("OP_NOP1", instruction_constructor=NOP), diff --git a/symbolic_execution/program/instruction/stack_based.py b/symbolic_execution/program/instruction/stack_based.py index 58d047e2a7fbd1dc9d67b62921678471bf4978a6..13165163a253cd5330309b70ca8f59bf1ed86c48 100644 --- a/symbolic_execution/program/instruction/stack_based.py +++ b/symbolic_execution/program/instruction/stack_based.py @@ -257,7 +257,7 @@ class CheckSigInstruction(IInstruction): self._constraint_on_operands = constraint_on_operands def run(self, machine: IStackBasedMachine): - """Check a or several signatures against public keys.""" + """Check a signature against a public key.""" super().run(machine) pubkey = machine.pop_from_stack() @@ -272,3 +272,32 @@ class CheckSigInstruction(IInstruction): def __repr__(self) -> str: """Return the string representation of the instruction.""" return f"{super().__repr__()}({'single_sig'})" + + +class CheckMultiSigInstruction(IInstruction): + """IInstruction that checks several signatures against public keys.""" + + def __init__(self, pc: int, sig_function: Callable, **args): + """Initialize the check sig instruction.""" + super().__init__(pc, **args) + + if sig_function is None: + raise InstructionInitializationError("The signature function is None.") + self._sig_function = sig_function + + def run(self, machine: IStackBasedMachine): + """Check several signatures against several public keys.""" + super().run(machine) + + # NOTE this code will crash against symbolic keys and signatures count + pubkeys_count = machine.pop_from_stack() + machine.drop_from_stack(pubkeys_count) + sig_count = machine.pop_from_stack() + machine.drop_from_stack(sig_count) + + ret = self._sig_function(pubkeys_count, sig_count) + machine.push_onto_stack(ret) + + def __repr__(self) -> str: + """Return the string representation of the instruction.""" + return f"{super().__repr__()}({'multi_sig'})" \ No newline at end of file diff --git a/tests/language/bitcoin/symbolic/testing_scenarii.py b/tests/language/bitcoin/symbolic/testing_scenarii.py index 4aa5916e3c7187ae78bc4f6b406ae925587ec2fe..98f9d2438c8f828408c4c56ab6afa2d781c7ae88 100644 --- a/tests/language/bitcoin/symbolic/testing_scenarii.py +++ b/tests/language/bitcoin/symbolic/testing_scenarii.py @@ -4,34 +4,37 @@ from symbolic_execution.language.bitcoin.symbolic_interpreter import Satifiabili TestScenario = namedtuple( - "TestScenario", "execution_status hex_script" + "TestScenario", "name execution_status hex_script" ) TESTING_SCENARII = [ - TestScenario(Satifiability.UNSATISFIABLE, "6382012088a820be087f56dfd0645993c60f742a32dcd733c75db11a946692500a6b07f65503388876a9148230631bc6978af49e056f58ba57485203df81706704e01d1560b17576a914166ddfe42c7effda275da84e1eda8583cc8794f96888ac"), - TestScenario(Satifiability.UNSATISFIABLE, "632103d619512240e2da7360e0ba988d222824a8384f7d43f07ceca01825add8802a3d6754b275210205bfac414d5b0078691c01627b30bb3ea3eafdc3dd45f9634a2eb5a0eccd38fd68ac"), - TestScenario(Satifiability.UNSATISFIABLE, "632102fb8af52ae49c7ff02c04d5474a09fc35bef47080a9f9f5614b14a7e81c96750767029000b275210234405f5183510dfaef4281619e0e0e8d54a169de87c3a9429e6815262ed644c168ac"), - TestScenario(Satifiability.UNSATISFIABLE, "a9144b1fec264ddee03172e6a0d0e99c9f7b75fd3013876321025990676edd76a365a067a708bb3b25334472846395460a58038a90f86c58a95c67029000b275210393ef9cffe8ffd90393ca96c277c89858f1f7d65aad75df6ed1a88d62ce5da5ff68ac"), - TestScenario(Satifiability.UNSATISFIABLE, "63a914bb408296de2420403aa79eb61426bb588a08691f8876a91431b31321831520e346b069feebe6e9cf3dd7239c670400925e5ab17576a9140d22433293fe9652ea00d21c5061697aef5ddb296888ac"), - TestScenario(Satifiability.UNSATISFIABLE, "632102ed03e275914c2c9012623815d82536c3cd0f236800a909e3be35144b776ad43767030ce707b17521029f93a84f6a6fc93b479fc845eb120d0d94188f9ef4fdfcfac03d8f45083c79da68ac"), - TestScenario(Satifiability.UNSATISFIABLE, "8201208763a914a9ddc31c3aa662dd3df25cfaacf32626bcb9b310882103dddd27e12856ab9f506c18694bc3c4b3419ba266cc4e401fb19123eaa32856ea67750311a409b1752102e90d0b6a7fa8c21630535a77ba0dcaec9a321fe825a401633e70cdd33ca369d268ac"), - TestScenario(Satifiability.UNSATISFIABLE, "a9144fa22d2b4eed18e026d4a716ef432224b4dfc81b876321038f21a7d24de9bda130b0d85c045e5dffccc0256dea567771f5ea4223ffb05d45670341bd0ab17521021a535dc1ecf9428f2b42f4448e706a80a0b215cdb4cfb904da41db616654aa7a68ac"), - TestScenario(Satifiability.UNSATISFIABLE, "a820b1a01a9c34ddc93c48e50d55073354fdfa6cbf13db97d9c1dfd98e994b7c492c876321024e8768b37746b1c65fdaaaee241b2f6a6b4f742d637249d1973a14b25a7ae96b6752b2752103e5f85f417a2cb89f0bfc4338eba791bc9ecbb7e1fd0038b1b0ef2e4359ee412268ac"), - TestScenario(Satifiability.UNSATISFIABLE, "a8205a917fe0e9a08004ea16bd682d656f8780b33af30c1e6d1b483652cecbb9d2908763210219b65599338687c784f5b78a23cac164a9094e94af6ec49532132da22d74e4226703931b06b1752102cff5fe1dae742d57cf2be42ae607f28ae0e4837019ca4b8b1bcdc96bcf4af9ee68ac"), - TestScenario(Satifiability.UNSATISFIABLE, "a97614b6a9c8c230722b7c748331a8b450f05566dc7d0f87630120b26d41049a797cd64043177214982114420e9e88a1bda92693f35de6934109b015b1c4ecb18570a29dc749e489377b4a6414d01af464773ed5e72abe95c812143eff7a3467148ef113ab29409765b689baab8f1a1fd3e966825887640499ad4658b17568410484ccd0f7c843d9738114e8e59cb057d2cb505892f6bdec8100d404fe33826f9f68300593395478fe13fe39d610d84c51d19e451275d86af3b7c2a3a003c4256468ac"), - TestScenario(Satifiability.UNSATISFIABLE, "63a820254e38932fdb9fc27f82aac2a5cc6d789664832383e3cf3298f8c120812712db882102661f72301363d25bda5e083342747032bc2a00ac58d74509d902f87a8f086bee675ab2752102661f72301363d25bda5e083342747032bc2a00ac58d74509d902f87a8f086bee68ac"), - TestScenario(Satifiability.SATISFIABLE, "210246414b45204b45592046414b45204b45592046414b45204b45592046414b45206eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75abac91"), - TestScenario(Satifiability.SATISFIABLE, "210246414b45204b45592046414b45204b45592046414b45204b45592046414b45206eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75abac91"), - TestScenario(Satifiability.SATISFIABLE, "64410408e496fc785089e54dfeb5d1c0ba06f99bee96951e1f9f4ac74b8118b3964cb1f38369f9c972c11ab4b6427f0b2355d0d116269f4043a44332e3ecec5d321d7641046fe513c87278d706338fe95241c183722204483fb19aed9abf2c3259755913b0988ab8385bf615d777d934d7109e9a064a6ca9de0f36f53348c9d760acfc2e0b410421ea36180cc830d85136a2a8c31020d30403f9bf3f0d89918f6f1a68adcb6aa44a354048734132250ce66ecaf55d8ce75140cd175e4a086f17f1b79ef425445f4104f5f5edaed4464297be1b612af7115ec11f40c510946491ab19aeaca4aec226620cd601ffa15cf2a8c7117cc4aba830e9f1a567fc9ab9cf5bd9024f25b67bf4ba4104cd2d1c08987da5f5c9815e675ccc428681632c70c364183bd438f8ebaed029e7e34a9a8ae661cadc9ac34871e2b478ec2a2ce0f267ef7234e949f990851dd4844104d83c59cef19de270175442a4b6517cb293bd401b55997053987bdb0f17e128e13830a4a4e67983c48f9624e86903afdd3206878b2c01ca2c715c618380ea50ed410454f272658d005fcbdf6bada5b161085ededf384ee6a431cded391487767a9e6a8f219b6203943b60acc88cc3b3688f4b1ea06f5a8dbd12f5f3db76a7b80e842f41042ec20548ca134276341806afe0aa5b3f9fb56b5b9d3340b0226719584396044bba2ab0e98af0d3f3b157a667609319296f25b92ab9953607ea6437bb00b9332e4104b17318e61cf59d37a61e8c0c317a2e173a56af5ce64bec421613100e04b689d7099e08231f73fc3b77aa677772fca9daa6147e0014885ddbfd6b092f3c81b24f4104ef03dced2196fece4667d762fd19ac565bc8dcfda40d8f8a3f7c6b6626fe2cc90039dd6af4862f559ef48ab567d8f7c8e7912484b5939903b904654a7680603e41047552bcf8182b037a60eab0137793b39a5ef86c0f172b6a59e096629197944b0abcdc14e7e0bdb83fb57cc31080c55f0fd968d63494d7e2814bc5d7477a7bfe1841041a944fb54d5e9ecddb67f88c64611fe49ac996e204b5df5383b1b43bd7b581ba66f683517481981749849fb93d63d362b701e3c1353e7b0103672077d105195e4104fb1322874b4b0ba454a3c73b08a615bab48370cd2239b693e322e955ac297e86b51ee33f7c4da4cd55f2a13bac5eaa2010953756d2b3ab073ead4c4f0e51b62441042f1eafd03e769be35b7db0044d352363722d152447007386a9ae983197d358604ec8b5f9afa02517fd1d5a9c11148b5f959487067c13c604d15072e68ad296864104b2aec0edd4c5ca08f50bbe9d66954dd5218cd5f4cde6d87cb7c44cb4c41f1faeb70df4532eb88655c93a348b235b3f623ff6028c333d64965fea830d953f755e4104411691845b47eae100fb853b57f99a846ce1dc4dd09be701ef800f8c66b3dcd0bbf0cff20c619db33a590905ee170cedc7fdf1beaa3cf677d5d66416130b0fa841044c17ca58e9eb5769644ef3643c4db4707a16d89f3be5b023933bd914dadd9f6ba8eeedfc7dcb41b23e68c81c633dd77631217ecbf9213f62b319b2aa52692ec3410482a6917e1a9a5141f21b2c5e6bb79b1d00af43ce6c6cd223e4d3146d03a7d73eff12b5f7041d013fe7be806b4a4adb4bcfd34c8b693d01050d397abb70ea6c1e410473a7c78f9ff430f2da389d8c6c40563dc992177aa1466f61c6d0764404475398201fe65bc82eed9ee141d1460b7e9735471c19389cb957bc47502fcc4cb0aaba4104fe0667649e22b3241d2960e654c75635605723cf4e3fcf3940ddc55d6180d098cab35d24df3ccbba83443ab5308efd434247745e69d6b63c4edd5feb5d390de364ae"), - TestScenario(Satifiability.SATISFIABLE, "2102cf6397ab627bf61f94f594b0650f72b1efdd0278deed0e6a11d62c08df65ffa2ac7c2102a7783ab0b0b05fc022c1cb0d6cbf31bc83570df40fcd5b6f96141c0d14dc97c5ac937c2103243167b9773d537be3fe118d1c4f17c35d5abdd1c1f6f501b7aa006b24eab71eac937c766302e803b26968937c766302d007b26968935387"), - TestScenario(Satifiability.UNSATISFIABLE, "63140bdc9d2d256b3ee9daae347be6f4dc835a467ffe2102259b57015e60de464e1d83c375bdd01d272290c51cede0b794301de1b7770c7bac670450143458b17521023927b837a922696836e26399f759965328437f93aafaf3e02767d22860c0fba7ac68"), - TestScenario(Satifiability.SATISFIABLE, "2103fb0b46d9443b88da50dba2a321b35ef38f52d83decbd121d18c16aed13e5aea4ac6374632103f9d1dffcb32de42982f022db41eed2deec76856798919028585bb28117e546e9ac6704fdf0ee58b16868"), - TestScenario(Satifiability.SATISFIABLE, "0400925e5a7576140d22433293fe9652ea00d21c5061697aef5ddb2988ac"), - TestScenario(Satifiability.UNSATISFIABLE, "6e8791695221028e7253e764c010a4eb73de72bf2280890eada8759ef1adfb5a9393e8133192987652ae"), - TestScenario(Satifiability.SATISFIABLE, "63030d95315fae6857"), - TestScenario(Satifiability.UNSATISFIABLE, "6a76a914cd2b3298b7f455f39805377e5f213093df3cc09a88ac"), - TestScenario(Satifiability.SATISFIABLE, ""), - + TestScenario("", Satifiability.UNSATISFIABLE, "6382012088a820be087f56dfd0645993c60f742a32dcd733c75db11a946692500a6b07f65503388876a9148230631bc6978af49e056f58ba57485203df81706704e01d1560b17576a914166ddfe42c7effda275da84e1eda8583cc8794f96888ac"), + TestScenario("", Satifiability.UNSATISFIABLE, "632103d619512240e2da7360e0ba988d222824a8384f7d43f07ceca01825add8802a3d6754b275210205bfac414d5b0078691c01627b30bb3ea3eafdc3dd45f9634a2eb5a0eccd38fd68ac"), + TestScenario("", Satifiability.UNSATISFIABLE, "632102fb8af52ae49c7ff02c04d5474a09fc35bef47080a9f9f5614b14a7e81c96750767029000b275210234405f5183510dfaef4281619e0e0e8d54a169de87c3a9429e6815262ed644c168ac"), + TestScenario("", Satifiability.UNSATISFIABLE, "a9144b1fec264ddee03172e6a0d0e99c9f7b75fd3013876321025990676edd76a365a067a708bb3b25334472846395460a58038a90f86c58a95c67029000b275210393ef9cffe8ffd90393ca96c277c89858f1f7d65aad75df6ed1a88d62ce5da5ff68ac"), + TestScenario("", Satifiability.UNSATISFIABLE, "63a914bb408296de2420403aa79eb61426bb588a08691f8876a91431b31321831520e346b069feebe6e9cf3dd7239c670400925e5ab17576a9140d22433293fe9652ea00d21c5061697aef5ddb296888ac"), + TestScenario("", Satifiability.UNSATISFIABLE, "632102ed03e275914c2c9012623815d82536c3cd0f236800a909e3be35144b776ad43767030ce707b17521029f93a84f6a6fc93b479fc845eb120d0d94188f9ef4fdfcfac03d8f45083c79da68ac"), + TestScenario("", Satifiability.UNSATISFIABLE, "8201208763a914a9ddc31c3aa662dd3df25cfaacf32626bcb9b310882103dddd27e12856ab9f506c18694bc3c4b3419ba266cc4e401fb19123eaa32856ea67750311a409b1752102e90d0b6a7fa8c21630535a77ba0dcaec9a321fe825a401633e70cdd33ca369d268ac"), + TestScenario("", Satifiability.UNSATISFIABLE, "a9144fa22d2b4eed18e026d4a716ef432224b4dfc81b876321038f21a7d24de9bda130b0d85c045e5dffccc0256dea567771f5ea4223ffb05d45670341bd0ab17521021a535dc1ecf9428f2b42f4448e706a80a0b215cdb4cfb904da41db616654aa7a68ac"), + TestScenario("", Satifiability.UNSATISFIABLE, "a820b1a01a9c34ddc93c48e50d55073354fdfa6cbf13db97d9c1dfd98e994b7c492c876321024e8768b37746b1c65fdaaaee241b2f6a6b4f742d637249d1973a14b25a7ae96b6752b2752103e5f85f417a2cb89f0bfc4338eba791bc9ecbb7e1fd0038b1b0ef2e4359ee412268ac"), + TestScenario("", Satifiability.UNSATISFIABLE, "a8205a917fe0e9a08004ea16bd682d656f8780b33af30c1e6d1b483652cecbb9d2908763210219b65599338687c784f5b78a23cac164a9094e94af6ec49532132da22d74e4226703931b06b1752102cff5fe1dae742d57cf2be42ae607f28ae0e4837019ca4b8b1bcdc96bcf4af9ee68ac"), + TestScenario("", Satifiability.UNSATISFIABLE, "a97614b6a9c8c230722b7c748331a8b450f05566dc7d0f87630120b26d41049a797cd64043177214982114420e9e88a1bda92693f35de6934109b015b1c4ecb18570a29dc749e489377b4a6414d01af464773ed5e72abe95c812143eff7a3467148ef113ab29409765b689baab8f1a1fd3e966825887640499ad4658b17568410484ccd0f7c843d9738114e8e59cb057d2cb505892f6bdec8100d404fe33826f9f68300593395478fe13fe39d610d84c51d19e451275d86af3b7c2a3a003c4256468ac"), + TestScenario("", Satifiability.UNSATISFIABLE, "63a820254e38932fdb9fc27f82aac2a5cc6d789664832383e3cf3298f8c120812712db882102661f72301363d25bda5e083342747032bc2a00ac58d74509d902f87a8f086bee675ab2752102661f72301363d25bda5e083342747032bc2a00ac58d74509d902f87a8f086bee68ac"), + TestScenario("", Satifiability.SATISFIABLE, "210246414b45204b45592046414b45204b45592046414b45204b45592046414b45206eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75abac91"), + TestScenario("", Satifiability.SATISFIABLE, "210246414b45204b45592046414b45204b45592046414b45204b45592046414b45206eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75abac91"), + TestScenario("", Satifiability.SATISFIABLE, "64410408e496fc785089e54dfeb5d1c0ba06f99bee96951e1f9f4ac74b8118b3964cb1f38369f9c972c11ab4b6427f0b2355d0d116269f4043a44332e3ecec5d321d7641046fe513c87278d706338fe95241c183722204483fb19aed9abf2c3259755913b0988ab8385bf615d777d934d7109e9a064a6ca9de0f36f53348c9d760acfc2e0b410421ea36180cc830d85136a2a8c31020d30403f9bf3f0d89918f6f1a68adcb6aa44a354048734132250ce66ecaf55d8ce75140cd175e4a086f17f1b79ef425445f4104f5f5edaed4464297be1b612af7115ec11f40c510946491ab19aeaca4aec226620cd601ffa15cf2a8c7117cc4aba830e9f1a567fc9ab9cf5bd9024f25b67bf4ba4104cd2d1c08987da5f5c9815e675ccc428681632c70c364183bd438f8ebaed029e7e34a9a8ae661cadc9ac34871e2b478ec2a2ce0f267ef7234e949f990851dd4844104d83c59cef19de270175442a4b6517cb293bd401b55997053987bdb0f17e128e13830a4a4e67983c48f9624e86903afdd3206878b2c01ca2c715c618380ea50ed410454f272658d005fcbdf6bada5b161085ededf384ee6a431cded391487767a9e6a8f219b6203943b60acc88cc3b3688f4b1ea06f5a8dbd12f5f3db76a7b80e842f41042ec20548ca134276341806afe0aa5b3f9fb56b5b9d3340b0226719584396044bba2ab0e98af0d3f3b157a667609319296f25b92ab9953607ea6437bb00b9332e4104b17318e61cf59d37a61e8c0c317a2e173a56af5ce64bec421613100e04b689d7099e08231f73fc3b77aa677772fca9daa6147e0014885ddbfd6b092f3c81b24f4104ef03dced2196fece4667d762fd19ac565bc8dcfda40d8f8a3f7c6b6626fe2cc90039dd6af4862f559ef48ab567d8f7c8e7912484b5939903b904654a7680603e41047552bcf8182b037a60eab0137793b39a5ef86c0f172b6a59e096629197944b0abcdc14e7e0bdb83fb57cc31080c55f0fd968d63494d7e2814bc5d7477a7bfe1841041a944fb54d5e9ecddb67f88c64611fe49ac996e204b5df5383b1b43bd7b581ba66f683517481981749849fb93d63d362b701e3c1353e7b0103672077d105195e4104fb1322874b4b0ba454a3c73b08a615bab48370cd2239b693e322e955ac297e86b51ee33f7c4da4cd55f2a13bac5eaa2010953756d2b3ab073ead4c4f0e51b62441042f1eafd03e769be35b7db0044d352363722d152447007386a9ae983197d358604ec8b5f9afa02517fd1d5a9c11148b5f959487067c13c604d15072e68ad296864104b2aec0edd4c5ca08f50bbe9d66954dd5218cd5f4cde6d87cb7c44cb4c41f1faeb70df4532eb88655c93a348b235b3f623ff6028c333d64965fea830d953f755e4104411691845b47eae100fb853b57f99a846ce1dc4dd09be701ef800f8c66b3dcd0bbf0cff20c619db33a590905ee170cedc7fdf1beaa3cf677d5d66416130b0fa841044c17ca58e9eb5769644ef3643c4db4707a16d89f3be5b023933bd914dadd9f6ba8eeedfc7dcb41b23e68c81c633dd77631217ecbf9213f62b319b2aa52692ec3410482a6917e1a9a5141f21b2c5e6bb79b1d00af43ce6c6cd223e4d3146d03a7d73eff12b5f7041d013fe7be806b4a4adb4bcfd34c8b693d01050d397abb70ea6c1e410473a7c78f9ff430f2da389d8c6c40563dc992177aa1466f61c6d0764404475398201fe65bc82eed9ee141d1460b7e9735471c19389cb957bc47502fcc4cb0aaba4104fe0667649e22b3241d2960e654c75635605723cf4e3fcf3940ddc55d6180d098cab35d24df3ccbba83443ab5308efd434247745e69d6b63c4edd5feb5d390de364ae"), + TestScenario("", Satifiability.SATISFIABLE, "2102cf6397ab627bf61f94f594b0650f72b1efdd0278deed0e6a11d62c08df65ffa2ac7c2102a7783ab0b0b05fc022c1cb0d6cbf31bc83570df40fcd5b6f96141c0d14dc97c5ac937c2103243167b9773d537be3fe118d1c4f17c35d5abdd1c1f6f501b7aa006b24eab71eac937c766302e803b26968937c766302d007b26968935387"), + TestScenario("", Satifiability.UNSATISFIABLE, "63140bdc9d2d256b3ee9daae347be6f4dc835a467ffe2102259b57015e60de464e1d83c375bdd01d272290c51cede0b794301de1b7770c7bac670450143458b17521023927b837a922696836e26399f759965328437f93aafaf3e02767d22860c0fba7ac68"), + TestScenario("", Satifiability.SATISFIABLE, "2103fb0b46d9443b88da50dba2a321b35ef38f52d83decbd121d18c16aed13e5aea4ac6374632103f9d1dffcb32de42982f022db41eed2deec76856798919028585bb28117e546e9ac6704fdf0ee58b16868"), + TestScenario("", Satifiability.SATISFIABLE, "0400925e5a7576140d22433293fe9652ea00d21c5061697aef5ddb2988ac"), + TestScenario("", Satifiability.UNSATISFIABLE, "6e8791695221028e7253e764c010a4eb73de72bf2280890eada8759ef1adfb5a9393e8133192987652ae"), + TestScenario("", Satifiability.SATISFIABLE, "63030d95315fae6857"), + TestScenario("", Satifiability.UNSATISFIABLE, "6a76a914cd2b3298b7f455f39805377e5f213093df3cc09a88ac"), + TestScenario("3BYmEwgV2vANrmfRymr1mFnHXgLjD6gAWm", Satifiability.SATISFIABLE, "ae"), + TestScenario("36pW5sDLZx5dMEgXzY8bwMoQX9uCLXT3nD", Satifiability.SATISFIABLE, "ae91"), + TestScenario("3Q4cu49Vpg3cddMLLjBCMgQQzs7ZLpRDVt", Satifiability.SATISFIABLE, "0000ae"), + TestScenario("3LQmDsDi7oPNkWPBgXjZHVVMBx9JZ2nZov", Satifiability.UNSATISFIABLE, "5121025858585858585858585858585858585858585858585858585858585858585858766e6f6f6f6e5fae91"), + TestScenario("", Satifiability.SATISFIABLE, "037974875fae"), ] \ No newline at end of file diff --git a/tests/language/bitcoin/test_parser.py b/tests/language/bitcoin/test_parser.py index bfb05c5d34faf2f9f968c586faab6db6b4f7d395..0281511c8da3b17341458596ec8484f92fde5dc7 100644 --- a/tests/language/bitcoin/test_parser.py +++ b/tests/language/bitcoin/test_parser.py @@ -88,8 +88,8 @@ class TestParser(unittest.TestCase): elt_i += 1 def test_symbolic_execution(self): - for i, scenario in enumerate(SYMBOLIC_TESTING_SCENARII): - with self.subTest(i): + for _, scenario in enumerate(SYMBOLIC_TESTING_SCENARII): + with self.subTest(scenario.hex_script): _, status = find_unlocking_script(scenario.hex_script) self.assertEqual(status, scenario.execution_status)