Zero-Knowledge Proofs, from a Compiler Perspective

[Zero-Knowledge Proofs, from a Compiler Perspective] 보통 ZK를 설명할 때는 prover, verifier, statement, witness 같은 암호학적 구조에서 시작합니다. 이 설명은 당연히 중요합니다. ZK proof가 왜 설득력 있는지, private witness를 공개하지 않고도 어떤 claim을 믿게 만들 수 있는지 설명해주기 때문입니다. 하지만 개발자의 입장에서 보면 이 설명만으로는 중간이 비어 있습니다. 우리는 프로그램을 작성합니다. verifier는 proof를 검증합니다. 그 사이에서는 무슨 일이 일어날까요? source code, circuit DSL, guest program, assertion 같은 개발자의 의도는 그대로 proof가 되지 않습니다. 먼저 relation, constraint, circuit, AIR, trace, IR, VM semantics 같은 proof-friendly representation으로 바뀌어야 합니다. 바로 이 변환 과정에서 compiler perspective가 중요해집니다. [Practical ZK system은 compiler system이기도 하다] Cryptography는 proof가 왜 설득력 있는지를 설명합니다. Compilation은 그 proof가 무엇에 대한 것인지를 정의합니다. 즉, proof system은 어떤 relation이 만족되었다고 말해줄 수 있습니다. 하지만 그 relation이 정말 개발자가 증명하려던 claim을 표현하는지는 compiler side의 문제입니다. ZK proof는 source code에서 직접 만들어지는 것이 아닙니다. proof는 relation과 witness 또는 trace로부터 만들어집니다. source code는 그 relation으로 compile되어야 하고, private input은 그 relation을 만족하는 witness나 execution trace가 되어야 합니다. 그래서 ZK pipeline은 크게 세 부분으로 볼 수 있습니다. frontend/compiler layer는 “무엇을 증명할 것인가?”를 정의합니다. source program이나 circuit DSL을 constraint, circuit, AIR, trace relation, IR, VM semantics 같은 representation으로 낮춥니다. witness/execution layer는 “어떤 값들이 이 relation을 만족한다고 주장하는가?”를 만듭니다. circuit system에서는 witness assignment가 되고, zkVM에서는 guest program execution trace가 됩니다. proving backend는 “그 relation이 만족되었다는 사실을 어떻게 증명할 것인가?”를 담당합니다. 여기서 SNARK, STARK, folding, recursion, lookup, polynomial commitment 같은 proof-system-side 기술이 붙습니다. [Verifier는 source code를 확인하지 않는다] 예를 들어 source code에 이런 assertion이 있다고 해도, assert!(age = 18); verifier가 이 코드를 읽고 “age가 18 이상이구나”라고 판단하는 것은 아닙니다. verifier가 보는 것은 compiled relation, public input, verification key 또는 program identity, 그리고 proof입니다. 이 지점에서 일반적인 프로그램 실행과 ZK의 trust model이 갈라집니다. 일반 software에서는 CPU나 VM이 정해진 semantics에 따라 instruction을 실행했고, 그 결과가 프로그램의 결과라고 받아들이는 구조입니다. 하지만 ZK verifier는 prover의 실행을 직접 신뢰하지 않습니다. prover가 “이 프로그램을 실행했다”고 말하는 것만으로는 충분하지 않습니다. 실행의 의미가 compiled relation이나 trace constraint 같은 obligation으로 바뀌어야 하고, verifier는 그 obligation이 만족되었다는 proof를 확인합니다. 따라서 중요한 질문은 이것입니다. source-level claim이 lowering 이후에도 같은 의미로 남아 있는가? comparison은 올바르게 range check되었는가? boolean result는 제대로 constrain되었는가? public input은 private witness와 제대로 binding되었는가? zkVM이라면 proof가 올바른 program image와 VM semantics에 묶여 있는가? 이 부분에서 compiler bug는 단순한 compiler bug가 아닐 수 있습니다. ZK에서는 어느 layer에서 생긴 버그든 verifier-trust bug가 될 수 있습니다. 결과는 단순히 실패하는 proof가 아니라, verifier가 잘못된 claim을 믿게 만드는 valid proof일 수 있습니다. [Cryptography는 보장하고, compilation은 정의한다] ZK ecosystem은 단순히 “좋은 proof system을 고르는 문제”가 아닙니다. source language, IR, arithmetization, witness generation, proving backend, verifier interface가 모두 연결된 compiler stack에 가깝습니다. Circom, Noir, Cairo, RISC Zero, SP1, LLZK 같은 도구들도 결국 이 compiler boundary를 어디에 그리는지, 무엇을 frontend가 책임지고 무엇을 backend가 책임지는지를 다르게 선택한 결과로 볼 수 있습니다. ZK를 암호학으로 이해하는 것은 반드시 필요합니다. 하지만 practical ZK system을 만들고 사용하려면, 암호학만으로는 부족합니다. 개발자가 작성한 프로그램은 그대로 proof가 되지 않습니다. 그 프로그램은 어떤 relation으로 변환되고, 그 relation은 witness나 trace와 만나고, backend는 그 relation이 만족되었다는 사실을 증명합니다. compiler perspective에서 보면 많은 질문이 더 선명해집니다. 무엇을 증명하는가? 그 claim은 어떤 representation으로 바뀌었는가? 그 변환은 meaning-preserving한가? verifier가 믿는 relation은 개발자가 의도한 relation과 같은가? 이 질문들이 practical ZK system의 핵심이라고 생각합니다. Full version: [link]