Movement 형식 검증 프레임워크 강화
Movement의 aptos-core 리포지토리 내 새로운 풀 리퀘스트(PR #308)는 Lean 4를 사용한 Move 표준 라이브러리의 형식 검증 인프라를 확장하고 있습니다. 이 업데이트는 `vector::index_of` 함수의 포괄적인 정확성 증명과 에러 처리, 옵션 타입, 서명자 작업, 고정소수점 연산을 포함하는 기본 표준 라이브러리 작업의 새로운 사양 모듈을 도입합니다.
Vector Index_Of 정제 증명
이 업데이트의 핵심은 `Refinement/Vector.lean`에 927줄의 새로운 코드를 추가하는 `vector::index_of`(`stdModuleEnv`의 바이트코드 인덱스 19)에 대한 포괄적인 정제 증명입니다. 이 증명은 전체 실행 경로를 포함합니다: 루프 설정(`evalProg`에서 루프 헤더까지 7단계), 발견된 경로(요소 매치가 `(true, k)` 반환), 반복 경로(매치 실패 시 `k+1`로 진행). 주요 증명 기법은 `(List.map MoveValue.u64 xs).length.toUInt64`를 사용하여 VM 단계 계산과 일치시키고 반사성 증명을 활성화하며, 오프셋 매개변수를 올바르게 추적하는 귀납적 증명에 `suffices` 일반화를 적용합니다. 증명에는 최상위 정리 `vectorIndexOf_returnValues_found`와 `vectorIndexOf_returnValues_notFound`가 포함됩니다.
새로운 표준 라이브러리 사양 모듈
이 풀 리퀘스트는 핵심 표준 라이브러리 작업을 다루는 5개의 새로운 사양 모듈을 도입합니다:
• Error.lean — 정규 오류 코드 및 중단 코드 산술
• Option.lean — `option::swap_or_fill` 사양 및 속성
• Signer.lean — 서명자 주소 추출 작업
• FixedPoint32.lean — `create_from_rational`, `floor`, `ceil`, `round`, `min`, `max` 작업을 포함한 고정소수점 산술
• BitVector.lean — `new`, `set`, `shift_left`, `is_index_set` 등의 비트벡터 작업
각 모듈에는 바이트코드 프로그램, 네이티브 함수 모델, Move 바이트코드 인터프리터에 연결하는 정제 증명이 포함되어 있습니다.
테스트 및 검증
이 변경 사항은 포괄적인 테스트를 통과합니다: `lake build`는 기존 `sorry` 경고만으로 성공적으로 완료되고, `lake build difftest` 차등 테스트 실행 파일은 오류 없이 컴파일되며, 완전한 차등 테스트 파이프라인은 Rust 코퍼스 검증, Move VM 오라클 생성, Lean 평가자 검증 전체에서 227개의 통과 테스트와 0개의 실패를 달성합니다.
Move 개발에 미치는 영향
이 형식 검증 확장은 Move 생태계의 바이트코드 수준에서 표준 라이브러리 함수의 정확성을 증명하는 능력을 강화합니다. 정제 증명은 고수준의 Move 코드를 저수준의 바이트코드 실행에 연결하여 개발자와 감사자가 중요한 작업이 정확히 사양대로 작동함을 검증할 수 있게 합니다.