Purpose and Problem Solved
Overall, your understanding of the Finalizer seems inadequate. The purpose of a Finalizer is threefold: first, to convert EVM words to Circom words, second, to generate a circuit witness (which will be converted into a proof in the backend), and third, to analyze the chain of symbols and generate a permutation.
I think this part needs to be rewritten.
Backend Integration
I think this problem should be about Permutation. What is Permutation and why do we need that?
Raw placement data from execution can be inefficient (redundant wires, unused connections)
Nothing to do with efficiency. We have to do this so that Circom can deal with the data values produced by the Synthesizer. If we could avoid this, the performance had been improved.
Large circuits slow down proving time
This is true but not in this case. Doing this splitting wires slows down the proving time, but we have to do.
Circuit Optimization
"Circuit Optimization" -> "Precision alignment for Elliptic curve fields"
Purpose and Problem Solved The Finalizer bridges the gap between symbolic execution and concrete circuit generation: Problem 1: Symbolic → Concrete Conversion During execution, the Synthesizer works with symbolic pointers (e.g., StackPt, MemoryPt) The backend prover needs concrete numerical wire connections Solution: Finalizer converts all symbolic references into actual wire indices and constraint equations Problem 2: Circuit Optimization Raw placement data from execution can be inefficient (redundant wires, unused connections) Large circuits slow down proving time EVM uses 256-bit values but Circom's finite field is 254-bit (field overflow risk) Solution: PlacementRefactor optimizes wire sizes, removes unnecessary connections, and splits 256-bit values into two 128-bit limbs for field compatibility Problem 3: Backend Integration Frontend and backend use different data structures Backend needs standardized JSON format for circuit loading Solution: Permutation class generates JSON files that match backend's expected schema Problem 4: Witness Data Management Circuit needs both structure (permutation) and concrete values (witness) Witness data must align with circuit wire indices Solution: Generates permutation.json (structure) and placement-specific witness files
I think this introduction can be moved to the "Execution Flow" section.
Generate
"Utilize a combination of subcircuits to derive a new symbol to represent the true value in the EVM memory, from existing symbols in MemoryPt."
Constraints: ~5000
Better to change "Total constraints" to relieve confusion, since we are allowing up to 1024 contraints.
Synthesizer: Opcode Reference
This page is awesome.
7. Finalizer Class
We need to explain the Finalizer as well. What is the goal? Which problems it deals with? How it solves them?
Example Scenario
You had better show the figures.
Synthesizer: Code Examples
I think you can use the figures in the "Concept" page.
SSTORE, LOG
CALLER, SLOAD and SSTORE will be the third important things. CALLER is related to verifying the transaction signature. SLOAD and SSTORE should involve Merkle proof verification.
The current version of Synthesizer treats them as oracles, provided by EVM. I'm working on fundamentally treating those.
One of Synthesizer's most complex tasks is tracking overlapping memory writes:
This is second important part. In which cases this aliasing resolution is required? "Overlapping" is just one example but not all.
Example one: Suppose that MSTORE is going to store a DataPt "X" (32 bytes) in the memory at offset 0x03. After some time has passed, MLOAD is loading a 32-byte memory value at offset 0x00 to the stack. Say this "Y". Suppose there have been no "overlapping" during the meantime. Do you think the returned stack value "Y" is still the same as "X" even if there was no overlapping?
Example 2: In general, Calldata can be much longer than 32 bytes. So whenever EVM is going to load specific function input argument "Y" onto the stack, it chunks the Calldata.
It's quite tricky for a Synthesizer to shadow this, since DataPts cannot deal with words greater than 32 bytes! The current version of the Synthesizer avoids solving this problem: it simply takes the resulted chunk made by the EVM as an Oracle. The next version, currently in development, will fundamentally solve this: it will create another virtual MemoryPt dedicated to CallData and store DataPts for the function selector and function arguments there—this process is the reverse of resolving aliasing.
Please see this code for dealing with "CALLDATALOAD".
Synthesizer needs to convert between external values
Why do we have to do this? What would we lose if we do not this conversion? This question is all about the Synthesizer and the most important. So please add more introduction about Why and How.
internal symbols
Please mention that, .e.g, "Symbols are instantiated with the DataPt format."
Readers may be confused with the terminology "symbol", since we never defined it.
Important: The RPC connection remains active throughout execution, not just during initialization. When the EVM encounters SLOAD, BALANCE, EXTCODESIZE, etc., it queries the blockchain state through RPC in real-time.
This is true for the moment, but in the future updates it will be changed to not to do this.
Subcircuit Library Compilation: Circom compiles all the fundamental circuits (ALU1, bitify, XOR, etc.) into WebAssembly files. These are the building blocks that Synthesizer will use to construct the transaction-specific circuit.
This task should be separated from the Synthesizer. Please consider mentioning, e.g., "QAP-compiler compiles all fundamental subcircuits for I/O interface buffers, arithmetic and bitwise operations, and cryptographic primitives with Circom.", "See this page to find more details about the QAP-compiler."
We will add a page for the qap-compiler in the future.
Synthesizer: Key Terminology
Please move this page to the next to "Concepts". Terminologies should be defined first before going into the details. Same as coding.