BitVM and SatoshiVM Circuit
Last updated
Last updated
SatoshiVM adopts BitVM's approach to verifying arbitrary computations on the Bitcoin blockchain: using the primitive, non-Turing-complete Bitcoin Script code to simulate the effect of logic gate circuits, then utilizing a massive amount of logic gate circuits to achieve the functionality of complex virtual machines.
We know that computers/processors are input-output systems composed of a large number of logic gate circuits. BitVM attempts to simulate the input-output effect of logic gate circuits using Bitcoin Script. As long as the logic gate circuits can be simulated, in theory, it is possible to realize a Turing machine, completing all computable tasks.
In the interactive fraud proof protocol of Arbitrum, the disputing parties engage in multiple rounds of communication to continually subdivide a particular transaction instruction until they localize a disputed opcode. Then, this opcode, along with its input and output results, is executed directly on the Ethereum blockchain for verification. This process determines which party's claim is correct and penalizes the malicious party.
In the Bitcoin and BitVM schemes, due to the simplicity of Bitcoin Script, it's not feasible to directly verify EVM opcodes as done in Ethereum Layer2 solutions. Therefore, an alternative approach is employed: opcodes compiled from any high-level language are decoded again into the form of logic gate circuits. Then, Bitcoin Script is used to simulate the operation of these logic gate circuits. This allows for the indirect simulation of the operational effects of virtual machine opcodes, such as those of the EVM, on the Bitcoin blockchain. We can consider the logic gate circuits as an Intermediate Representation (IR) between EVM opcodes and Bitcoin Script opcodes.
SatoshiVM employs the Bristol format to illustrate its logic gate circuit structure. The Bristol format is a commonly used method in the field of circuit for expressing logic gate circuits. In essence, it provides a standardized way to describe the layout of complex logic gate circuits, including the inputs and outputs of digital circuits, the functions of logic gates (such as AND, OR, NOT gates), and their specific connections.The Bristol format typically includes the following parts:
Circuit Size Information: Describes the basic attributes of the circuit, such as the total number of logic gates, the number of input and output signals, etc.
Input and Output Information: Provides detailed information about the assignment of each input and output signal.
Gate Description: Gives a specific description of the function of each logic gate, including the gate type (AND, OR, NOT, etc.) and its connected input and output signals.
Here is an example of Bristol format code:
The visualization of the aforementioned Bristol format circuit is as follows:
The components are as follows:
The first line's 4,7 respectively indicate that this part of the circuit has 4 logic gates and 7 signal lines.
The first number in the second line represents the bit size of the circuit's input signals, and the second number represents the quantity of input signals. For example, in the case above, it includes a one-bit input, but the input signals comprise three separate inputs (0), (2), and (3).
The first number in the third line indicates the quantity of the circuit's output signals, and the second number represents the bit size of the outputs. In the case above, it contains one output, which only includes a single digit (6).
Apart from the above three lines, the rest of the content specifically defines each logic gate and signal line within the circuit, listing the following details for every logic gate:
The number of input signal lines
The number of output signal lines
The identifiers for the input lines
The identifiers for the output lines
The function of the logic gate
For example, 1 1 0 1 INV indicates that the logic gate has one input line, one output line, the input line identifier is (0), the output line identifier is (1), and the logic gate operation is INV. This effectively describes gate A in the aforementioned example circuit.
In this document, we only use INV and AND logic gates. INV represents the NOT operation, and it operates according to the following rule:
0
1
1
0
The AND logic gate represents the AND operation, and it operates according to the following rule:
0
0
0
0
1
0
1
0
0
1
1
1
A more complex case like 2 1 3 5 6 AND indicates that the logic gate has two input lines, one output line, the input line identifiers are (3) and (5), the output line identifier is (6), and the logic gate operation is AND. This actually defines gate D in the example circuit. We can also represent gate D with the mathematical formula .
