[ZK] Cairo

TL;DR

Cairo에서는 “제약식을 직접 설계”하지 않는다. VM(Cairo CPU)의 AIR(=고정된 제약)가 이미 있고, 일반 함수를 작성한 뒤 그 안에서 assert(...) 등으로 “원하는 명제가 참이어야만 실행이 성공”하도록 만든다. 그 실행 트레이스가 STARK로 증명된다.

1. What is Cairo

“Cairo — 튜링 완전한 STARK 친화적 CPU 아키텍처”

• 튜링 완전 : 어떤 종류의 연산이던 전부 수행할 수 있음을 의미
• STARK 친화적 :  Cairo는 STARK 기반의 증명 생성을 프로그래밍으로 대체할 수 있도록 해주는 언어 - 효율적으로 proof를 생성할 수 있게 해줌
• CPU 아키텍처 : 컴퓨터의 아키텍처 수준에서 긴밀하게 소통하는 저수준 언어

proof 생성 시에는 2가지로 인해 비효율성이 발생한다.

• Statement의 다항방정식 표현으로 인한 비효율 : 새로운 변수 및 연산의 증가: 증명하고자 하는 일반적인 계산(statement)을 ZK-STARKs나 ZK-SNARKs가 요구하는 형식인 다항방정식(Polynomial Equation) 형태로 변환(R1CS 등)할 때, 원래의 연산에는 없던 새로운 임의의 변수가 추가되거나 필요한 연산의 개수가 늘어남 → Proof를 생성하는 증명자(Prover)의 부담을 가중시키고, 결과적으로 증명 생성의 속도를 늦춤
• 제어 흐름(Control Flow)으로 인한 비효율 : Loop나 Branch (조건문)와 같은 제어 흐름 구조를 다항방정식으로 표현하는 과정에서, 실제로 필요한 연산 횟수보다 훨씬 많은 횟수의 연산을 강제로 수행해야 하는 비효율이 발생

Cairo는 이 비효율을 해소하기 위해 CPU 아키텍처 수준에서 설계된 저수준 언어를 선택했다. Proof 생성을 위해 최적화된 CPU 아키텍처와 Instruction Set(명령어 집합)을 새로 만들어, 이 집합을 만족하는 방식으로 프로그램을 작성하면, 애초에 다항방정식으로의 변환이 필요 없거나 또는 변환이 매우 효율적으로 이루어지게 되어, 불필요한 변수와 연산의 수를 근본적으로 줄일 수 있게 된다.

2. Deep Dive to Cairo

Cairo = CPU + AIR

Cairo를 좀 더 어렵게 이야기 하면 다음과 같다.

“계산의 무결성(Computational Integrity)을 증명하는 다항방정식 형태의 Proof인 AIR(Algebraic Intermediate Representation)을 쉽고 효율적으로 생성하기 위해 CPU 아키텍처단부터 새로 설계하여 만든 폰-노이만 아키텍처”

이전에 STRAK를 공부했을 때, “AIR”를 볼 수 있었는데, AIR는 쉽게 말하면 우리가 증명하려고 하는 statement가 지켜야 할 규칙(제약 조건)을 다항식 형태로 나타낸 것이다. Cairo는 Proof 생성에 최적화된 폰-노이만 아키텍처와 Instruction Set(명령어 집합)을 새로 설계하여 프로그램의 한 상태(행 Rowi)에서 다음 상태(행 Rowi+1)로 넘어갈 때 발생하는 변화가 가장 단순하고 적은 수의 다항식 제약 조건(AIR)으로 표현되도록 구성되어 있다.

즉, 복잡한 Statement를 처음부터 다항식으로 변환하기 쉬운 저수준 Assembly로 작성하도록 유도하여, 불필요한 변수(Trace Table}의 크기와 연산(Constraint의 차수)의 증가를 최소화한다.

Cairo의 설계

특이한 메모리 구조

Cairo의 메모리 구조는 다소 특이한데, Nondeterministic Continuous Read-Only Random Access Memory 구조를 지닌다. 이는 매우 경직된 메모리 구조로 execution 도중에 memory의 수정이 불가하다. 다만 이러한 제한을 통해서 AIR을 활용의 효율성이 극대화된다.

public memory의 효율성을 재고

Zk proof의 특성 상 code + output이 공유되어야 하므로 memory cell은 verifier에게 공유되어야 한다. Cairo의 경우 이러한 공유를 위해 일반적인 연산이 아니라 boundary를 제한하는 방식을 채택해 verifier가 이러한 공유 과정에 4개의 산술만이 필요하도록 만들었다.

연산 최적화

Cairo는 증명의 검증을 위해 자주 사용되는 Permutation Range check 등의 연산을 최적화한다. Cairo 상에서는 3개의 trace cell만으로 [0,2¹⁶) 범위 내에 trace가 존재하는지 확인할 수 있다.(일반적인 binary approach는 16개의 trace cell이 필요)

Cairo CPU

• 최적화된 Instruction Set 제공
  
  • 모든 명령어가 작고 단순한 (15 bit flags + 3 integers) RISC 형태로 구성되어, 타의 추종을 불허하는 수준으로 trace cell을 적게 사용하여 증명 생성(최적화).

• 실용적인 기능 제공
  • Conditional branch, memory, function call, 재귀(Recursion) 등 개발에 필요한 기능을 충분히 지원.
  • Nondeterministic 특성 덕분에 Recursive proof 및 병렬 연산 지원.
• Built-in 최적화
  • Cryptographic hash function 등 자주 쓰이는 중요한 연산에 대해 최적화된 built-in을 제공하여 편의성과 효율성을 동시에 높임.
• Product Level 표준 제시
  • Cairo 기반으로 생성된 모든 오프체인 증명은 동일한 Ethereum 스마트 컨트랙트에서 검증될 수 있는 단일 프레임워크를 제공하여, 생태계 확장에 기여.

3. Simple Example

3 * 4 = 12 증명

prover

use core::hash::HashStateTrait;
use core::poseidon::PoseidonTrait;

pub fn create_commitment(a: felt252, b: felt252, nonce: felt252) -> felt252 {
    let mut state = PoseidonTrait::new();
    state = state.update(a);
    state = state.update(b);
    state = state.update(nonce);
    let commitment = state.finalize();

    commitment
}

pub fn generate_zk_proof(a: felt252, b: felt252, c: felt252, commitment: felt252) -> felt252 {
    let computed_c = a * b;
    assert(computed_c == c, 'Multiplication mismatch');

    let mut proof_state = PoseidonTrait::new();
    proof_state = proof_state.update(commitment);
    proof_state = proof_state.update(c);
    let zk_proof = proof_state.finalize();

    zk_proof
}

#[executable]
fn main(a: felt252, b: felt252, c: felt252, nonce: felt252) -> (felt252, felt252) {
    let commitment = create_commitment(a, b, nonce);
    let zk_proof = generate_zk_proof(a, b, c, commitment);

    println!("commitment: {}", commitment);
    println!("zk_proof: {}", zk_proof);

    (commitment, zk_proof)
}

verifier

#[starknet::interface]
pub trait IMultiplicationVerifier<TContractState> {
    fn verify_zk_proof(
        ref self: TContractState, commitment: felt252, zk_proof: felt252, c: felt252,
    ) -> bool;
}

#[starknet::contract]
mod MultiplicationVerifier {
    use core::hash::HashStateTrait;
    use core::poseidon::PoseidonTrait;

    #[storage]
    struct Storage {}

    #[abi(embed_v0)]
    impl AgeVerifierImpl of super::IMultiplicationVerifier<ContractState> {
        fn verify_zk_proof(
            ref self: ContractState, commitment: felt252, zk_proof: felt252, c: felt252,
        ) -> bool {
            let mut proof_state = PoseidonTrait::new();
            proof_state = proof_state.update(commitment);
            proof_state = proof_state.update(c);
            let calculated_proof = proof_state.finalize();

            zk_proof == calculated_proof
        }
    }
}

a. 먼저 prover에서 zk proof 생성

scarb execute --print-program-output --arguments 3,4,12,12345

b. verifier에서 contract 배포

declare

sncast --account=sepolia declare \                    
    --contract-name=MultiplicationVerifier \
    --network=sepolia

deploy

sncast --account=sepolia deploy \                
    --class-hash=0x495bea3bbb205d321f11e05311705de016ce02354c0c6e1cc0263f379823467 \
    --network=sepolia

c. test

sncast call --network sepolia \              
  --contract-address 0x04707bca34bc2ce4d7e9e7aa82bab4d702472d3686915837e72be81264a5f3e7 \
  --function verify_zk_proof \
  --calldata \
  3383298923621555134881407750558353577883516115305139938260704789276607526339 \
  110104513817474511716189280977084708273832431304331938192148989180448298497 \
  12

4. Challenges

맨 처음에는 아래와 같이 코드를 작성한 후에, execute를 실행했다.

pub fn mul(a: u32, b: u32) -> u32 {
    a * b
}

pub fn is_correct(a: u32, b: u32, c: u32) -> bool {
    let mut is_correct = false;
    if (mul(a, b) == c) {
        is_correct = true;
    }
    is_correct
}

#[executable]
fn main(input: (u32, u32, u32)) -> bool {
    let (a, b, c) = input;
    is_correct(a, b, c)
}

그런데 해당 코드의 경우에는 execution-id 1에 대해서는 잘 작동했지만(proof 생성과 verify가 가능), execution-id 2에서부터는 잘 작동하지 않았다.

이러한 오류는 Trace의 길이가 짧기 때문에 발생하는 오류였다.. Cairo 코드가 mul(3, 4)처럼 매우 단순한 계산만 수행할 경우, Execution Trace(AET)의 행(Row) 수가 10~20개 정도로 짧게 기록된다. 이 짧은 Trace는 STARK Prover가 요구하는 두 가지 최소 안전성 조건을 충족하지 못하기 때문에 오류가 발생한다.

• STARK 안전성을 위한 최소 길이 요구

  STARK 프로토콜은 통계적 건전성(Soundness)을 확보하기 위해 Trace Table의 길이가 일정 크기 이상이어야 한다.

  이 과정의 핵심은 LDE(Low-Degree Extension)이다. LDE는 Trace Table을 나타내는 다항식을 더 넓은 정의역으로 확장하는 과정인데, Trace의 길이가 너무 짧으면 다항식 확장을 수행할 여유가 없거나 알고리즘 자체가 실행되지 못한다.

  결과적으로 Prover는 log_size >= LOG_N_LANES와 같은 최소 크기 요구 조건을 만족하지 못해 증명 생성이 중단된다.

• Built-in 함수의 Trace 기록 요구 사항

  이 오류는 u32와 같은 정수 타입의 오버플로우 검사를 위해 Cairo가 사용하는 Range Check Built-in 함수와 관련이 있다.

  Cairo는 u32 타입을 사용할 때 자동으로 Range Check 코드를 CASM에 추가하며, 이 Built-in 함수는 자신의 Proof를 생성하기 위해 Trace Table에 특정 구조를 기록해야 한다.

  그러나 매우 단순한 연산만 수행할 경우, 이러한 구조를 완성하기 위한 최소한의 Trace 행(Row) 수가 확보되지 않아 증명 생성이 실패한다.

5. Reference

https://eprint.iacr.org/2021/1063.pdf

https://www.starknet.io/cairo-book/ch01-03-proving-a-prime-number.html?highlight=prime#proving-that-a-number-is-prime

https://velog.io/@0xmuang/ZK-ZK-Programming

https://blog.tetedo.com/385?category=1058574

https://www.certik.com/resources/blog/an-introduction-to-the-cairo-programming-language