Date: Tue, 10 Oct 2023 11:27:08 +1000
From: Anthony Towns <aj@erisian.com.au>
To: Robin Linus <robin@zerosync.org>,
 Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.org>
Message-ID: <ZSSobP+VJSIeXE+U@erisian.com.au>
References: <CCA561B6-A2DE-46FD-A2F8-98E0C34A3EEE@zerosync.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <CCA561B6-A2DE-46FD-A2F8-98E0C34A3EEE@zerosync.org>
X-Spam_score: -0.0
X-Spam_bar: /
Subject: Re: [bitcoin-dev] BitVM: Compute Anything on Bitcoin
X-BeenThere: bitcoin-dev@lists.linuxfoundation.org
X-Mailman-Version: 2.1.15
Precedence: list
List-Id: Bitcoin Protocol Discussion <bitcoin-dev.lists.linuxfoundation.org>
List-Unsubscribe: <https://lists.linuxfoundation.org/mailman/options/bitcoin-dev>, 
 <mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=unsubscribe>
List-Archive: <http://lists.linuxfoundation.org/pipermail/bitcoin-dev/>
List-Post: <mailto:bitcoin-dev@lists.linuxfoundation.org>
List-Help: <mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=help>
List-Subscribe: <https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev>, 
 <mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=subscribe>
X-List-Received-Date: Tue, 10 Oct 2023 01:27:23 -0000

On Mon, Oct 09, 2023 at 03:46:24PM +0200, Robin Linus via bitcoin-dev wrote:
> Abstract. BitVM is a computing paradigm to express Turing-complete
> Bitcoin contracts.

Please correct me if I'm wrong:

The way I understand this idea is that you take an N-bit claim (in the
given example N=4), and provide a NAND circuit that asserts whether
the claim is valid or not (in the example, if I did the maths right,
valid values take the form xxx0, 1x01, and only three bits were
actually needed). It would be very straightforward afaics to allow
for AND/OR/XOR/etc gates, or to have operations with more than two
inputs/one output.

The model is then a prover/challenger one: where the prover claims to
have a solution, and the verifier issues challenges that the prover
only be able to reply to consistently if the solution is correct. If
the prover doesn't meet the challenge, they lose the funds.

The circuit entails C individual assertions, with two inputs (selected
from either the N inputs bits, or the output of one of the previous
assertions) and a single output. You then encode each of those C
assertions as tapleafs, so that spending a tx via that tapleaf validates
that individual assertion.

You also have an additional tapleaf per input/assertion, that allows
the verifier to claim the funds immediately rather than issue another
challenge if the prover ever gave two inconsistent values for either an
input or the result of one of the assertions.

If the prover tries to cheat -- eg, claiming that 1111 is a valid input
in the example -- then the verifier can run the circuit themselves
offline, establish that it's an invalid, and work backwards from the
tip to establish the error. For example:

   TRUE=NAND(L,D)  -- D is true, so L better be false
   L=NAND(J,A) -- A is true, so J better be true for L to be false
   J=NAND(H,I) -- one of H or I must be false for J to be true,
     prover will have to pick. suppose they pick I.

   I=NAND(G,B) -- B is true, so if I was false, G was true
   G=NAND(A,C) -- can only pass at this point with some of A,C,G
     being given an inconsistent value

So you should need enough challenges to cover the longest circuit path
(call it P) in order to reliably invalidate an attempt to cheat. I guess
if your path isn't "branching" (ie one of the NAND inputs is something
you already have a commitment to) then you can skip back to something
that NAND's two "unknowns", at which point either one of the inputs is
wrong, and you trace it further down, or the output is correct, in which
case you can do a binary search across the NAND's where there wasn't
any branching, which should get you roughly to P=log(C) steps, at which
point you can do a billion gate circuit in ~100 on-chain transactions?

I think the "reponse enabled by challenge revealing a unique preimage"
approach allows you to do all the interesting work in the witness,
which then means you can pre-generate 2-of-2 signatures to ensure the
protocol is followed, without needing CTV/APO.

You'd need to exchange O(C*log(C)) hashes for the challenge hashes as
well as the 2*C commitment hashes, so if you wanted to limit that setup
to 20GB, then 24M gates would be about the max.

I think APO/CTV would let you avoid all the challenge hashes -- you'd
instead construct P challenge txs, and P*C response txs; with the output
of the C responses at level i being the i+1'th challenge, and each
of the tapscripts in the P challenges having a CTV-ish commitment to a
unique response tx. Still a lot of calculation, but less transfer needed.
You'd still need to transfer 2*C hashes for the commitments to each of
the assertions; but 20GB gets you a circuit with about ~300M gates then.

> It is inefficient to express functions in simple NAND circuits. Programs
> can be expressed more efficiently by using more high-level opcodes. E.g.,
> Bitcoin script supports adding 32-bit numbers, so we need no binary
> circuit for that.

I don't think that really works, though? You need a way of committing
to the 32-bit number in a way that allows proof of equivocation; but
without something like OP_CHECKFROMSTACK, I don't think we really have
that. You could certainly have 2**K hashes to allow a K-bit number,
but I think you'd have a hard time enumerating even three 16bit numbers
into a 4MB tapscript even.

CSFS-ish behaviour would let you make the commitments by signature,
so you wouldn't need to transfer hashes in advance at all, I think.

Cheers,
aj