Architecture

As mentioned, JOLT Atlas is built upon JOLT and the differences are the result of replacing the RISC-V computational model with ONNX. While JOLT can be seen as a CPU, JOLT Atlas can be seen as a DAG.

As a DAG, JOLT Atlas doesn't need to store and load from RAM. Instead of registers, JOLT Atlas uses a heap abstraction. The rest of the diagram above remains almost exactly as the original JOLT codebase. The reader can find the bytecode and instruction execution documentation in their docs.

The prover begins by cryptographically committing to the execution trace $z$ of the ONNX VM on the appropriate input. Then, the prover in JOLT Atlas proves that:

• The state transition function of the ONNX virtual machine encoded in R1CS is enforced. It proves that $z$ is a valid execution trace assuming $z$ satisfies memory-consistency and relevant entries of $z$ are indeed in the relevant lookup tables capturing evaluation of the ONNX instructions. JOLT Atlas applies Spartan to establish that z satisfies the constraint system.

• Every ONNX instruction is executed correctly. Like JOLT, This is primarily achieved through the Shout lookup argument.

• At each cycle of the ONNX virtual machine, the current instruction (as indicated by the program counter) is "fetched" from the bytecode and decoded. In Jolt Atlas, this is proven by treating the bytecode as a lookup table, and fetches as lookups. To prove the correctness of these lookups, we also use the Shout lookup argument.

• The correctness of heap operations using the Twist memory checking algorithm.

• The correctness of guest program outputs via the output check sumcheck. Memory constraints are different compared to the original JOLT zkVM.