Re: [bitcoin-dev] BitVM: Compute Anything on Bitcoin

From: "Russell O'Connor" <roconnor@blockstream•com>
To: Robin Linus <robin@zerosync•org>,
	 Bitcoin Protocol Discussion
	<bitcoin-dev@lists•linuxfoundation.org>
Subject: Re: [bitcoin-dev] BitVM: Compute Anything on Bitcoin
Date: Tue, 17 Oct 2023 14:00:26 -0400	[thread overview]
Message-ID: <CAMZUoKm56htx9Ux4D8CvgpQ+W_f1qw9HrkWBfkFPo699Esp--Q@mail.gmail.com> (raw)
In-Reply-To: <CCA561B6-A2DE-46FD-A2F8-98E0C34A3EEE@zerosync.org>

[-- Attachment #1: Type: text/plain, Size: 2664 bytes --]

While I haven't looked at the BitVM in detail, I would like to mention that
Simplicity's core language (excluding introspection primitives) has the
same expressivity as Boolean circuits.

A few years ago I did some experiments to compile Simplicity expressions to
a system of polynomial constraints (R1CS).  The experiments were
successful. For instance, I was able to compile our Sha256 compression
function specification written in Simplicity to a set of approximately
128,000 constraints.  Under this "circuit" interpretation, Simplicity types
represent cables, which are a bundle of wires equal to the 'bit size' of
the given type. The 'case' combinator ends up being the only "active"
component (implementing a demux).  The 'injr' and 'injr' combinators output
some fixed Boolean values. The rest of the combinations end up only
connecting, bundling and unbundling wires, and contribute no constraints at
all.

While my previous experiment was generating constraints, it is clear to me
that a similar interpretation could instead generate logic gates, and I
would expect the same order of magnitude in the number of gates generated
as the number of constraints generated above.  Thus Simplicity could be
used as a source of ready made expressions to generate useful circuits for
the BitVM, should someone be interested in pursuing this angle.

On Mon, Oct 9, 2023 at 10:05 AM Robin Linus via bitcoin-dev <
bitcoin-dev@lists•linuxfoundation.org> wrote:

> Abstract. BitVM is a computing paradigm to express Turing-complete Bitcoin
> contracts. This requires no changes to the network’s consensus rules.
> Rather than executing computations on Bitcoin, they are merely verified,
> similarly to optimistic rollups. A prover makes a claim that a given
> function evaluates for some particular inputs to some specific output. If
> that claim is false, then the verifier can perform a succinct fraud proof
> and punish the prover. Using this mechanism, any computable function can be
> verified on Bitcoin. Committing to a large program in a Taproot address
> requires significant amounts of off-chain computation and communication,
> however the resulting on-chain footprint is minimal. As long as both
> parties collaborate, they can perform arbitrarily complex, stateful
> off-chain computation, without leaving any trace in the chain. On-chain
> execution is required only in case of a dispute.
>
> https://bitvm.org/bitvm.pdf
> _______________________________________________
> bitcoin-dev mailing list
> bitcoin-dev@lists•linuxfoundation.org
> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
>

[-- Attachment #2: Type: text/html, Size: 3297 bytes --]