Talos

Telegram

Talos는 Lean 4로 작성된 WebAssembly 인터프리터이며, 크레타를 지키던 그리스 신화의 청동 거인에게서 이름을 따왔습니다. 이 기계적 수호자는 규칙을 강제하기 위해 만들어졌습니다.

Wasm 프로그램을 _실행_하는 데 사용되는 정의와 _추론_할 때 사용하는 정의는 동일합니다. 동기화해야 할 별도의 사양 인터프리터가 없습니다: 평가(evaluation)와 증명(proof)은 단일 코드베이스를 공유합니다.

작업 진행 중. Talos는 활발하게 개발되고 있습니다. API 및 증명 인터페이스는 변경될 수 있습니다.

시각적 개요 (Visual overview)

WebAssembly, Talos, 그리고 Lean이 컴파일된 프로그램에 대한 증명을 지원하기 위해 어떻게 함께 작동하는지 보여주는 시각적인 소개입니다.

이것이란 무엇인가 (What this is)

목표는 WebAssembly의 기능적으로 완전한(feature-complete) 실행 가능 의미론을 확보하여 이를 형식적 객체로 활용하는 것입니다. 사용자는 다음을 수행할 수 있습니다:

• 구체적인 입력값으로 프로그램을 실행합니다.
• Lean의 증명 도구를 사용하여 프로그램 동작에 대한 정리(theorem)를 설정하고 증명할 수 있습니다. (예: 사양 대비 정확성, 프로그램 간 동등성, 모든 입력에 대해 성립하는 속성 등)

이 인터프리터는 실행 속도보다 추론의 명확성에 의도적으로 최적화되었습니다. Talos는 전체 Wasm 커버리지를 목표로 하지만, 당장의 초점은 비최적화된 상위 레벨 소스 코드(Rust, C 등)에서 자연스럽게 발생하는 기능들의 부분집합—즉, 프로그램이 얼마나 빨리 작동하는지가 아니라 무엇을 하는지를 검증하고 싶을 때 실제로 중요한 의미론입니다.

증명(Proof)이 북극성입니다. 성능 관련 작업은 별도로 증명된 동등한 구현 뒤에 속해야 합니다.

추론 기반 (Reasoning foundation)

Talos의 증명은 최약 전제 조건(weakest precondition, WP) 계산을 기반으로 구축되었습니다. 이는 술어 변환 의미론(predicate transformer semantics)으로, 사후 조건(postconditions)으로부터 이를 보장하는 전제 조건(preconditions)까지 역방향으로 추론할 수 있게 해줍니다. 이를 통해 루프, 분기, 함수 호출에 대해 인터프리터를 매 단계마다 재전개하지 않고도 구조적이고 조합적인 증명을 제공합니다.

빠른 시작 (Quick start)

.wat 모듈 실행:

cd interpreter
lake exe runner samples/factorial.wat fact 5

출력: 120

연료 제한을 두고 실행하기 (Fuel cap) (기본값 1,000,000 스텝):

lake exe runner --fuel 10000 samples/factorial.wat fact 5

최소 예제 모듈은 interpreter/samples/factorial.wat를 참조하세요.

그것에 대해 증명하기:

interpreter/Interpreter/Wasm/Examples/Factorial.lean는 명령어 단위의 작은 단계 추적(instruction-granular small-step traces)을 조합하여 완전한 정확성 증명을 보여줍니다.

리포지토리 레이아웃 (Repository layout)

엄격한 의존성 체인을 형성하는 모노레포 내 세 개의 Lake 패키지가 있습니다:

의존성으로 사용하기 (Using as a dependency)

인터프리터에만 의존할 경우 (Wasm 의미론 + WP 계산):

# lakefile.toml
[[require]]
name = "WasmInterpreterLean"
...

CodeLib에 의존할 경우 (위에 리프팅 보조정리(lifting lemmas) 및 추론 도우미 추가):

[[require]]
name = "CodeLib"
path = "path/to/repo/codelib"

CodeLib을 가져오는 코드는 인터프리터를 직접 가져올 필요가 없습니다. CodeLib은 하위 증명(downstream proofs)이 필요로 하는 인터프리터의 부분들을 재내보냅니다 (re-exports).

빌드하기 (Building)

just build   # interpreter → codelib → programs 순서로 빌드합니다

또는 단일 패키지를 빌드합니다:

cd interpreter  && lake build
cd codelib      && lake build
cd programs/lean && lake build

의존성:

• Lean 4 — interpreter/lean-toolchain에 고정된 툴체인이며, elan에 의해 자동으로 가져옵니다.
• wasm-tools — .wasm 바이너리를 디코딩하고 Wasm 테스트 스위트를 실행하는 데 필요합니다. brew install wasm-tools 또는 cargo install wasm-tools를 사용하세요.

Wasm 테스트 스위트 실행하기 (Running the Wasm testsuite)

just testsuite

이름으로 특정 파일 필터링:

just testsuite i32

기여하기 (Contributing)

CONTRIBUTING.md를 참조하세요.

라이선스

GNU Affero General Public License v3.0 — 자세한 내용은 [LICENSE]를 참조하십시오.