LuminAIR’s primary goal is to cryptographically demonstrate that a computational graph has been executed correctly. This proof allows verifiers to validate the integrity of the computation using significantly fewer resources than re-executing the graph.

The underlying technology enabling this is STARKs (Scalable Transparent Arguments of Knowledge), which ensures computational integrity through a transparent, scalable, and post-quantum secure proof system.

Using STARKs to Prove Computational Graphs

Mapping Computational Graph Nodes to AIR Components

In LuminAIR, computational graphs are transformed into AIR constraints and executed to generate an algebraic execution trace.

Each node in the computational graph corresponds to a distinct AIR component, which has its own set of local constraints. These constraints ensure that each operation in the graph is executed correctly.

/// Returns the `ComponentProver` of each components, used by the prover.
pub fn provers(&self) -> Vec<&dyn ComponentProver<SimdBackend>> {
    self.add
        .iter()
        .map(|c| c as &dyn ComponentProver<SimdBackend>)
        .chain(
            self.mul
                .iter()
                .map(|c| c as &dyn ComponentProver<SimdBackend>),
        )
        .collect()
}

Ensuring Data Flow Integrity Between Nodes

While each AIR component verifies its local operation, it is equally important to ensure proper data flow between nodes in the computational graph. Specifically, the output of one node must match the input of another node.

This consistency is enforced using the LogUp lookup argument protocol, which establishes a system of relations between tensor values.

Output Yields (Positive Multiplicity)

  • When a node produces an output that will be consumed by other nodes, its multiplicity equals the number of consumers.
  • This indicates that the value is “yielded” for use elsewhere in the graph.

Input Consumes (Negative Multiplicity)

  • When a node receives an input from another node, its multiplicity is -1.
  • This signifies that the value is “consumed” by the operation.

Special Cases (Zero Multiplicity)

  • Graph Inputs (Initializers): Tensors that serve as initial inputs to the graph have zero multiplicity because they are not consumed by any prior operation.
  • Graph Outputs (Final Results): Tensors that represent final outputs of the graph also have zero multiplicity since they are not yielded to subsequent operations.