Is it possible to design a recursive covenant opcode that results in a full node stuck in an infinite verification loop?

Question

Is it possible to design a new opcode enabling recursive covenants that could result in a full node stuck in an infinite loop of verifying transactions? (Obviously this would never be considered for a Bitcoin soft fork, I'm just wondering about the limits of the design space for covenant opcodes)

e.g. A -> B -> C

A, B, C are transactions. B spends A, C spends B. A imposes constraint on spending conditions of B. B imposes constraint on spending conditions of C. But the spending conditions of C have to check something in A (something that wasn't hashed, perhaps the first few bits of a signature in the witness). As a result of that verification B has to check something in A and the infinite verification loop is set in motion.

I'm leaning towards no but not 100 percent sure. It isn't enough for C to check something in A, it needs to change A in some way such that B needs to verified again. This might even be prevented by the UTXO model (versus account model). In an account model you could refer to the balance of any previous block and get into an infinite verification loop that way.

Answer 1

Thanks to Russell O'Connor and Sanket Kanjalkar for answering this on IRC (I've only lightly paraphrased their answers, any errors are my own though.)

Is it possible to design a new opcode enabling recursive covenants that could result in a full node stuck in an infinite loop of verifying transactions?

No. Recursive in the Bitcoin covenant context only means something like spending an output back to the identical script template.

At the time of writing the only previously formally proposed Bitcoin opcode that when used could result in a script not terminating is OP_EVAL. With scripts that don't use OP_EVAL you can just count the opcodes and each opcode is evaluated at most once.

Consider you have access to OP_EVAL and two other new opcodes: OP_RED (check if the current block has a valid transaction that has OP_BLUE in it) and OP_BLUE (check if the current block has a valid transaction that has OP_RED in it). The block could have two transaction outputs with OP_EVAL, OP_BLUE and OP_EVAL, OP_RED in them respectively. This would require an infinite loop of checks.

The design space for new opcodes is vast. There are lots of principles of various levels of importance that could be violated by newly designed opcodes. For example you would generally want the script result to only be a function of the transaction itself and nothing external to the transaction. You would also want the static analysis of resources to be computable in linear time.

Hence rather than starting from clearly unsafe (but perhaps maximally flexible opcodes) and restricting functionality to make them safe it is probably a better approach to work on proving that certain opcodes are terminating and non-harmful.

The aim of ongoing work on Simplicity is to offer maximal flexibility while still being subject to the desired constraints and principles discussed above. Without something like Simplicity it is difficult to know for sure that any opcodes(s) are provably safe whilst at the same time offering maximal flexibility.