almost free solidity

The project's goal is achieved by a combination of many instruments used in the different stages. The first stage is preprocessing, here the user's code gets modified and all the needed modifications are injected. The original code of the annotated function is used later in the process. We defined a custom set of EVM opcodes and the interpreter within the SP1 VM to prove the execution of the function's code.

After the proving, batches of proofs are aggregated and sent to the blockchain. Within those aggregated proofs, every single one has its own Merkle path that can be later used for verification purposes. Those are sent to the special contract called Oracle.

After they are present in the Oracle contract,

We use solc modifications, SP1, Rust, and Foundry.

System workflow:

1. Preprocessing
   1. Use a custom Solidity preprocessor to find all the functions with @free annotation in the source code.
   2. Separate the implementations and compile them to EVM bytecode.
   3. Replace their implementations with a call to the verification oracle.
   4. Replace calldatasize() with calldataload(caldatasize() - 32) in the EVM bytecode. It allows us to pass additional witnesses needed for ZKP verification without affecting the function selectors and contract logic.
2. Proving
   1. Receive the bytecodes from step 1.2 along with the function inputs.
   2. Use a specialized server with a custom EVM implementation to ensure that the function execution can be performed without interactions with the state.
   3. Use SP1 zkVM to prove the EVM execution of the function's bytecode with specific calldata.
3. Aggregation
   1. Proofs from different users of the protocol are batched to share the verification cost.
   2. Final proof is sent to the blockchain, all the nested proofs are merklized, and the root is used as a part of the public input.
   3. Each of the nested proofs within the final one gets a Merkle proof to verify that it belongs to the verified batch.
4. Execution
   1. When calling the initial contract, the Merkle proof is provided in the "buffer" that was allocated in the calldata during preprocessing.
   2. Merkle proof is used to call the oracle and ensure that the function with the specific input will return a specific output.