Re: [bitcoin-dev] MATT: [demo] Optimistic execution of arbitrary programs

[Anthony Towns <aj@erisian.com.au>]

On Fri, Sep 29, 2023 at 03:14:25PM +0200, Johan Torås Halseth via bitcoin-dev wrote:
> TLDR; Using the proposed opcode OP_CHECKCONTRACTVERIFY and OP_CAT, we
> show to trace execution of the program `multiply` [1] and challenge
> this computation in O(n logn) on-chain transactions:

"O(n log n)" sounds wrong? Isn't it O(P + log(N)) where P is the size
of the program, and N is the number of steps (rounded up to a power of 2)?

You say:

> node = h( start_pc|start_i|start_x|end_pc|end_i|end_x|h( h(sub_node1)|h(sub_node2) )

But I don't think that works -- I think you want to know h(sub_node1)
and h(sub_node2) directly, so that you can compare them to the results
you get if you run the computation, and choose the one that's incorrect.
Otherwise you've got a 50/50 chance of choosing the subnode that's
actually correct, and you'll only be able to prove a mistake with
1/2**N odds?

Not a big change, it just becomes 32B longer (and drops some h()s):

  node = start_pc|start_i|start_x|end_pc|end_i|end_x|h(sub_node1)|h(sub_node2)
  leaf = start_pc|start_i|start_x|end_pc|end_i|end_x|null

I'm not seeing what forces the prover to come up with a balanced state
tree -- if they don't have to have a balanced tree, then I think there
are many possible trees for the same execution trace, and again it would
become easy to hide an error somewhere the challenger can't find. Adding a
"start_stepcount" and "end_stepcount" would probably remedy that?

There seems to be an error in the "what this would look like for 4 state
transitions" diagram -- the second node should read "0|0|2 -> 0|1|4"
(combining its two children), not "0|0|2 -> 1|0|2" matching its left
child.

I'm presuming that the counterparty verifies they know the program (ie,
all the leaves in the contract taptree) before agreeing to the contract
in the first place. I think that's fine.

Cheers,
aj