Talos: Lean 4에서의 형식적 추론을 위한 오픈 소스 WASM 인터프리터
Talos는 Lean 4로 개발된 오픈 소스 WebAssembly (Wasm) 인터프리터로, 사용자가 Wasm 프로그램을 실행하고 그 동작을 형식적으로 증명할 수 있게 해줍니다. 실행과 형식적 검증 모두에 단일 코드베이스를 사용함으로써, Talos는 별도의 명세 인터프리터를 유지 관리할 필요를 없애며, 프로그램의 평가와 그 정확성에 관한 증명이 완벽하게 동기화되도록 보장합니다.
형식적 검증을 위한 실행 가능한 의미론
Talos는 WebAssembly에 대해 기능적으로 완전한 실행 가능한 의미론을 제공하며, Wasm 환경을 형식적 객체로 취급합니다. 이 아키텍처를 통해 개발자는 동일한 시스템 내에서 두 가지 주요 작업을 수행할 수 있습니다:
- 프로그램 실행: 사용자는 구체적인 입력을 사용하여 Wasm 프로그램을 실행하고 그 동작을 관찰할 수 있습니다.
- 형식적 증명: 사용자는 명세에 대한 정확성, 두 프로그램 간의 동등성, 또는 모든 가능한 입력에 대해 유지되는 속성 등 프로그램 동작에 대한 정리를 정리하고 증명할 수 있습니다.
형식적 추론을 우선시하기 위해, Talos는 원시 실행 속도보다 추론의 명확성을 위해 의도적으로 최적화되었습니다. 이 프로젝트는 Rust 및 C와 같은 고수준 소스 언어에서 일반적으로 생성되는 Wasm 기능의 하위 집합에 집중하여, 성능 최적화보다 검증에 필수적인 의미론을 우선시하도록 보장합니다.
추론 기반: 최약 전제 조건 계산법 (Weakest Precondition Calculus)
Talos의 형식적 증명은 술어 변환 의미론의 한 형태인 최약 전제 조건 (WP) 계산법을 사용하여 구현됩니다. 이 접근 방식은 개발자가 원하는 사후 조건(postcondition)으로부터 역방향으로 추론하여 해당 조건을 보장하는 전제 조건(preconditions)을 결정할 수 있게 합니다.
WP 계산법을 사용함으로써, Talos는 루프, 분기, 함수 호출을 포함한 복잡한 프로그램 구조에 대해 구조화되고 합성 가능한 증명을 제공합니다. 이는 증명 과정의 매 단계마다 인터프리터의 상태를 다시 펼칠 필요를 없애주어, Wasm 프로그램의 검증을 더 관리하기 쉽게 만듭니다.
프로젝트 아키텍처 및 저장소 레이아웃
Talos는 엄격한 의존성 체인을 가진 세 개의 Lake 패키지를 포함하는 모노레포로 구성됩니다:
| 패키지 | 경로 | 목적 |
|---|---|---|
Interpreter |
interpreter/ |
Wasm AST, 의미론 및 WP tactic 레이어를 포함함 |
CodeLib |
codelib/ |
리프팅 보조 정리(lifting lemmas) 및 프로그램 추론 도우미를 제공함 |
Programs |
programs/ |
구체적인 Rust-to-Wasm 검증 작업을 포함함 |
Talos를 의존성으로 통합하는 개발자의 경우, Interpreter 패키지는 핵심 Wasm 의미론과 WP 계산법을 제공하며, CodeLib은 상위 수준의 추론 도우미를 추가하고 인터프리터의 필요한 부분을 재내보내기(re-export)합니다.
시작하기 및 도구
Talos는 Lean 4와 wasm-tools (.wasm 바이너리를 디코딩하고 테스트 스위트를 실행하기 위해 필요)가 필요합니다. 사용자는 runner 실행 파일을 사용하여 .wat 모듈을 실행할 수 있습니다:
cd interpreter
lake exe runner samples/factorial.wat fact 5
실행 중 무한 루프를 방지하기 위해, Talos는 연료 캡(fuel cap) 메커니즘(기본값 1,000,000 단계)을 포함하며, 이는 --fuel 플래그를 통해 조정할 수 있습니다. 팩토리얼 함수에 대한 정확성 증명의 완전한 예제는 Interpreter/Wasm/Examples/Factorial.lean 파일에서 확인할 수 있습니다 있습니다.