기술 요약: Lean 에서 비트벡터 및 유한체 동치 증명 자동화

문제 제기

영지식 증명 (ZKP) 회로 인코딩의 검증은 비트벡터 연산(표준 기계 산술, $2^N$ 모듈로) 과 유한체 연산(대규모 소수 $P$ 모듈로 산술) 을 동시에 사용하는 양자화 없는 문장의 증명이라는 중대한 과제에 직면해 있습니다. ZKP 시스템은 종종 비트벡터 논리를 유한체 다항식으로 인코딩하는 "산술화 (arithmetizations)"를 요구합니다. 이러한 인코딩의 정확성을 보장하는 것은 ZKP 시스템의 건전성에 필수적이지만, 이를 구성하는 과정은 오류가 발생하기 쉽습니다.

기존 검증 워크플로는 두 가지 주요 한계를 겪고 있습니다:

1. 수동 검증: Lean 과 같은 상호작용 정리 증명기 (ITP) 에 전체 ZKP 시스템을 임베딩하는 것은 강력한 보장을 제공하지만 상당한 인적 노력이 필요합니다. ZKP 최적화가 빠르게 진화함에 따라 이러한 수동 증명은 종종 상당한 재작업을 요구합니다.
2. 자동 SMT 검증: 검증을 이론에 따른 만족도 (SMT) 쿼리로 축소하면 자동화가 증가하지만 두 가지 근본적인 문제에 직면합니다:
   • 이론 변환: SMT 솔버는 유한체와 비트벡터 간 변환을 위한 네이티브 지원을 부족합니다. 비트 분할과 같은 우회 방법은 과도한 변수를 도입하며, 범위 확인은 솔버 성능을 저하시키는 복잡한 다항식을 요구합니다.
   • 신뢰할 수 있는 코드베이스 (TCB): SMT 솔버는 ITP 보다 훨씬 더 큰 TCB 를 가지므로, 버그를 놓칠 위험이 증가합니다.

방법론

저자들은 유한체 인코딩과 해당 비트벡터 의미론 간의 동치를 자동으로 증명하도록 설계된 새로운 Lean 전술인 BitModEq를 제시합니다. 이 접근법은 ITP 의 풍부한 의미론을 활용하여 직접적인 타입 변환을 수행하면서도, 특수화된 워크플로우를 통해 SMT 해결의 자동화를 유지합니다.

핵심 워크플로우

BitModEq 는 논문의 그림 1 에 제시된 네 가지 명확한 단계로 작동합니다:

1. 유한체에서 자연수로 변환: 유한체 ($FP$) 정렬의 모든 항을 자연수 ($N$) 로 변환합니다. 여기에는 산술 식을 통해 toNat 과 같은 변환 연산자를 안쪽으로 밀어 넣는 작업이 포함됩니다.
2. 범위 분석: 변환 과정에서 생성된 자연수에 대한 부등식을 전용 범위 분석 알고리즘을 사용하여 해결합니다.
3. 자연수에서 비트벡터로 변환: 남은 자연수 항을 비트벡터 ($BV_N$) 로 변환합니다.
4. 비트 분해 (Bit-Blasting): 최종 비트벡터 등식 목표는 Lean 에 구현된 비트 분해 결정 절차인 bv_decide 를 사용하여 해결됩니다.

주요 기술 구성 요소

1. 변환 미적분 (4.2 절)
전술은 도메인 간 이동을 위한 일련의 변환 규칙을 사용합니다:

• $FP \to N$: distNat 과 같은 규칙은 덧셈과 곱셈에 대해 toNat 을 분배합니다. 중요한 점은 전술이 모듈로 래핑 (modular wraparound) 을 배제할 수 있는 경우 (단순 뺄셈 허용) 와 배제할 수 없는 경우 (모듈로 $P$ 를 더한 후 모듈로 연산 필요) 를 구분한다는 것입니다. sqrBds 와 같은 규칙은 비트 인코딩 ($x^2 = x$) 을 감지하여 이를 범위 ($x \le 1$) 로 변환합니다.
• $N \to BV$: distBV 와 같은 규칙은 연산에 대해 toBV 를 분배합니다. $FP \to N$ 단계와 달리, 이러한 규칙은 대상 공간이 본질적으로 $2^N$ 모듈로이므로 모듈로 연산자를 추가할 필요가 없습니다.

2. 범위 분석 (4.3 절)
기존 Lean 전술 (예: omega, linarith) 은 큰 계수와 복잡한 변수 의존성으로 인해 ZKP 산술화에서 종종 실패합니다. BitModEq 는 구문 지향적인 맞춤형 범위 분석 미적분을 도입합니다:

• 플레이스홀더 변수: 알고리즘은 복잡한 부등식을 분해하기 위해 존재적 플레이스홀더 변수를 도입합니다.
• 분해 및 제거: 규칙은 부등식을 분해합니다 (예: $a + b \le w$는 $a \le w_1, b \le w_2, w_1+w_2 \le w$로 변환). 그런 다음 플레이스홀더를 가정이나 알려진 속성 (예: 유한체 원소는 $P-1$ 이하로 제한됨) 에서 유도된 경계로 인스턴스화하여 제거합니다.
• 의존성 처리: ineqCases, ineqXOR 와 같은 특수 규칙은 비트 (0 또는 1) 를 시뮬레이션하는 변수에 대해 표적화된 경우 분석을 수행하여 표준 산술 솔버가 놓치는 의존성을 해결합니다.

3. 구현
이 전술은 정리와 bv_decide 를 위한 최종 비트 분해 단계를 위해 mathlib 를 활용하여 Lean 4.23.0 에서 구현되었습니다. 이는 최소한의 신뢰할 수 있는 컴퓨팅 기반 (TCB) 을 보장하기 위해 증명 검증을 위해 Lean 의 커널에 의존합니다.

주요 기여

1. BitModEq 전술: 유한체 연산을 비트벡터로 변환하고 비트 분해를 통해 결과 목표를 해결하여 ITP 의 정확성 보장을 유지하는 Lean 전술.
2. 실제 인코딩의 유계 검증: 이전 기법보다 더 높은 비트 너비 경계를 달성하는 두 가지 실제 ZKP 시스템 (Jolt 및 CirC) 에 대한 개념 증명 검증.
3. 전용 범위 분석: ZKP 산술화에서 흔히 발생하는 변수 의존성 및 부등식 제약을 처리하도록 특별히 설계된, 변환으로 인한 목표 증명을 위한 새로운 Lean 전술.

결과 및 평가

저자들은 Jolt(zkVM) 와 CirC(zkVM 컴파일러) 에서 추출한 벤치마크에 대해 최신 SMT 솔버 (전체 및 분할 그뢰브너 기저를 사용하는 cvc5 포함) 에 대해 BitModEq 를 평가했습니다.

• 성능: BitModEq 는 최상의 성능을 보이는 SMT 구성보다 19% 더 많은 벤치마크를 해결했습니다.
  • Jolt 벤치마크 (8 비트 및 32 비트 룩업 테이블) 에서 BitModEq 는 cvc5(약한 인코딩) 보다 8 비트 인스턴스 3 개와 32 비트 인스턴스 7 개를 더 많이 해결했습니다.
  • CirC 벤치마크에서 BitModEq 는 테스트된 17 개 비트 너비 중 13 개에서 더 많은 인스턴스를 해결했습니다.
• 확장성: cvc5 는 더 작은 비트 너비에서 더 잘 수행되었지만, 비트 분할로 인한 변수의 폭발로 인해 비트 너비가 증가함에 따라 성능이 크게 저하되었습니다. BitModEq 는 32 비트 입력까지 효과적으로 확장되었습니다.
• 효율성: 절멸 연구 (ablation study) 는 맞춤형 범위 분석이 중요함을 보여주었습니다. 경우 분할을 제거하면 해결된 벤치마크 수가 크게 감소했습니다 (예: CirC 에서 737 개에서 720 개로, Jolt 에서 24 개에서 21 개로). 표준 Lean 전술 (ring_nf, linarith 등) 로 맞춤형 분석을 대체하면 해결된 인스턴스가 급격히 감소했습니다 (예: CirC 에서 434 대 737).
• 실행 시간: 범위 분석은 총 실행 시간의 약 52% 를 차지했으며, 그 다음으로 변환 (23%) 과 비트 분해 (21%) 가 뒤따랐습니다.
• 버그 발견: CirC 평가 중 저자들은 정수 오버플로우와 관련된 32 비트 산술 오른쪽 시프트 구현에서 건전성 버그를 발견했으며, 이는 더 작은 비트 너비에서는 감지되지 않았습니다.

중요성 및 주장

이 논문은 BitModEq 가 ITP 의 건전성과 자동 추론을 결합함으로써 현재 ZKP 검증 워크플로의 특정 한계를 해결한다고 주장합니다. 유한체 제약을 비트벡터로 다시 변환함으로써, 이 접근법은 SMT 이론 변환의 성능 병목 현상과 SMT 솔버의 큰 TCB 를 피합니다.

저자들은 그들의 접근 방식이 현대 ZK 시스템에서 일반적인 패턴인 유한체 내에서 비트 수준 연산을 시뮬레이션하는 ZKP 산술화에 특히 효과적이라고 강조합니다. 이 방법은 완전하지는 않습니다 (특정 복잡한 의존성이나 역수와 같은 필드 특정 연산에 대해 "알 수 없음"을 반환할 수 있음). 그러나 이전에는 자동 도구에 대해 해결 불가능했던 실제 인코딩을 성공적으로 검증하여 이러한 중요한 암호학적 구성 요소의 정확성에 대한 커널 검증 증명을 제공합니다.