> Are you including Bitcoin script when you say consensus?
Currently, no. Our model considers "consensus" to be agreement on the ordering of transactions. We don't yet interpret the transactions.
However, agreement on the state follows directly provided nodes have a function (in the "functional programming" sense), call it `Process`, that returns the current state given the ordered list of transactions. If all nodes have the same the function, they will have the same state.
The BIP-0050 issue (in my understanding) is that different Bitcoin versions had different consensus rules, i.e. their `Process` functions were different. As far as I know, Bitcoin script is deterministic, so it should be possible to define it functionally. We haven't begun looking at this, though, and I don't know of anyone that has -- some people are working on verified implementations of the EVM, however.
> It seems like a huge task to formally model the whole consensus system, including OP_CODESEPARATOR.
It is a huge task, yes, but it can be done modularly such that reasoning about script interpretation can be almost entirely separated from reasoning about Nakamoto consensus. (This is a bit subtle, since the fork choice rule needs to check if blocks are valid, which relies on script interpretation.)
I don't really understand OP_CODESEPARATOR. As long as it is deterministic, it shouldn't be an issue.
Currently, no. Our model considers "consensus" to be agreement on the ordering of transactions. We don't yet interpret the transactions.
However, agreement on the state follows directly provided nodes have a function (in the "functional programming" sense), call it `Process`, that returns the current state given the ordered list of transactions. If all nodes have the same the function, they will have the same state.
The BIP-0050 issue (in my understanding) is that different Bitcoin versions had different consensus rules, i.e. their `Process` functions were different. As far as I know, Bitcoin script is deterministic, so it should be possible to define it functionally. We haven't begun looking at this, though, and I don't know of anyone that has -- some people are working on verified implementations of the EVM, however.
> It seems like a huge task to formally model the whole consensus system, including OP_CODESEPARATOR.
It is a huge task, yes, but it can be done modularly such that reasoning about script interpretation can be almost entirely separated from reasoning about Nakamoto consensus. (This is a bit subtle, since the fork choice rule needs to check if blocks are valid, which relies on script interpretation.)
I don't really understand OP_CODESEPARATOR. As long as it is deterministic, it shouldn't be an issue.