Ragu로 Tachyon 폴딩하기

Project Tachyon이 Zcash의 새로운 쉴디드 프로토콜 Tachyon과, 그 암호의 기반이 되는 Rust 재귀 zk-SNARK 툴킷 Ragu를 소개했다. Tachyon은 타협 없는 프라이버시 기술이 안고 있는 근본적 확장성 문제를 다루며, Ragu는 Tachyon의 필요와 현실적 제약에 맞춰 만들어졌다. 신뢰 설정 없이 ECDLP 기반 재귀 SNARK를 제시한 Halo 논문을 실사용 수준으로 구현하려는 것으로, 이른바 재귀 Bulletproofs의 구현에 가깝다고 설명한다.

Ragu는 위험 회피 차원에서 Zcash가 이미 배포한 도구에 크게 의존한다. Pasta 곡선 사이클, 원래의 Poseidon 해시, 내적 증명 기반 단변수 다항식 멀티 커밋먼트 방식은 모두 몇 년 전 Orchard에서 쓰였으며 2021년 이전의 오래된 암호는 대체로 피한다. Orchard의 halo2가 손으로 최적화한 PLONK 기반 산술화를 쓴 것과 달리 Ragu는 [BCCGP16] 계열의 단순한 R1CS 유사 방식을 쓴다. FFT나 다항식 곱셈이 필요한 경우는 증명을 완전히 간결하게 만드는 때처럼 드문 경계에 한정된다.

그 밖에 Tachyon에 중요한 특징들이 있다. 비균일 PCD 모델에서 각 노드가 실제로 쓰는 기능에만 비용을 내며, 여러 하위 프로토콜을 서로 다른 회로로 나눠 동시에 실행한다. 모든 구조가 단변수 다항식 커밋먼트를 중심으로 돌아가고, 애플리케이션 회로 안에서 다항식 오라클을 질의할 수 있다. 검증 성능은 전처리에 의존하지 않으며, Halo 논문의 기법으로 회로를 서술하는 공개 다항식의 평가 주장을 누산한다. 이는 이후 글에서 다룰 새로운 협력적 설정을 가능하게 한다.

고신뢰 엔지니어링도 강조한다. 암호 설계와 구현을 함께 개발하며 전문가의 피드백을 받았고, 감사, 광범위한 테스트, AI 분석 도구에 더해 퍼징과 Lean 기반 형식 검증 도구를 쓴다. 형식 검증에는 zkSecurity의 Clean 프레임워크를 도입해 Rust 쪽에서 제약과 증인을 Lean 구문으로 기록하고, Lean 쪽에서 가젯별 사전·사후 조건과 soundness/completeness 정리를 연결한다. 이를 위해 zkSecurity와 협의해 API를 조정하고 자동 검사를 CI에 통합했다. 퍼징은 zkSecurity의 연구와 Aztec의 기법을 참고했다.

문서화도 필수로 본다. 형식 검증은 프로그램이 명세와 일치함을 증명할 뿐 명세가 의도를 제대로 담았는지는 보장하지 못하기 때문이다. 팀은 Ragu를 개발하며 암호를 설명하는 두꺼운 책을 쓰고 있고, 아직 미완성이지만 이 문서 검토만으로 코드와 프로토콜에서 큰 개선점을 찾았다. Tachyon은 ZIP 절차에 따라 완전히 명세되며, Ragu도 특히 halo2와 비교해 더 엄밀히 명세하려 한다. 지침은 불가피한 곳에 복잡성을 모으고 나머지는 최대한 단순하게 유지하는 것이다.