search

tradecraftio / tradecraft

Tradecraft integration/staging tree https://tradecraft.io/download
Other
13 stars 9 forks source link

Remove opcodes with environment-determined effects #18

Open maaku opened 5 years ago

maaku commented 5 years ago

The bitcoin and elements scripting languages contain some opcodes which evolve program state in ways dependent on the entire execution environment rather than just local parameters. These opcodes which present special challenges to any overlaid type system are:

RETURN: as originally defined, terminated execution and returned the top-most value on the stack. Any code fragment which contained a RETURN opcode potentially had non-functional effects not reflected in its type signature, as it would end termination if the RETURN was executed. The RETURN opcode has since been removed and any script containing it made invalid, but nevertheless it was once part of the bitcoin scripting language and has analogues in other Forth derived languages. It would be wise to review the literature surrounding concatenate languages and see if there are any constructs or compilation architectures for which a RETURN-like opcode makes sense, and how these exceptional termination conditions are handled by type systems, if at all.

DEPTH pushes the current size (in elements) of the stack. It is particularly useful in real world scripts as a way of conditioning based on the number of parameters provided in the witness, as well as other space saving optimizations. However it has the distinct drawback that its output, the value pushed on the stack, is not a function of its inputs, at least not in a way that is easily expressible or useful in practical type systems. Code using DEPTH is therefore difficult to reason about based on type signatures alone. Future script versions should probably have DEPTH removed for ease of analysis, but before doing so we should survey the literature to make sure that the opcode is in fact merely a non-vital optimization, and not e.g. an essential part of some compiler architectures or idiomatic Forth code. If it is to be kept, some way of reconciling its behavior with the type system needs to be found.

IFDUP duplicates the top-most stack item, but only if it evaluates as false. The type signature of this operation is thus data-dependent and from a type analysis perspective it leaves the stack in an indeterminate state.

maaku commented 5 years ago

Added a note to the original post about IFDUP, which also frustrates type analysis as its effect on the stack is data-dependent.