Move에서의 명령형 일급 함수 (Imperative First-Class Functions)에 대한 형식 검증 (Formal

Move Prover (MVP)는 Move 프로그래밍 언어로 작성된 스마트 컨트랙트 (Smart Contracts)를 위한 형식 검증기 (Formal Verifier)입니다. 최근 Aptos의 Move는 고차 함수 (Higher-order functions)를 통해 확장되었습니다. 즉, 전달될 수 있고, 데이터 구조 (Data structs)에 저장될 수 있으며, 영구 저장소 (Persistent storage)에 보관될 수 있는 일급 값 (First-class values)으로서의 명령형 함수 (Imperative functions)가 도입되어 동적 디스패치 (Dynamic dispatch)가 가능해졌습니다. 본 논문은 Move 명세 언어 (Specification language)에서의 함수 값 (Function values) 표현 방식과 MVP에서의 구현 방법을 설명합니다. 우리는 단일 상태 (Single-state) 또는 이중 상태 (Two-state) 술어 (Predicates)를 통해 Move 함수를 특징짓는 동작 술어 (Behavioral predicates, 중단 (Aborts) 및 전/후 조건 (Pre/post conditions))를 도입합니다. 또한, 식이 평가되는 중간 메모리 상태 (Intermediate memory states)를 명명하기 위한 상태 레이블 (State labels)을 도입하며, 이를 통해 상태 전이 (State transitions)의 시퀀스를 설명하기 위한 동작 술어의 결합을 허용합니다. SMT 레벨에서 함수 값은 호출 지점 (Call site)에 도달하는 가능한 함수 값들을 판별함으로써 인코딩됩니다. 구체적인 함수가 알려진 경우 그 효과가 직접 계산되며, 함수 파라미터(Function parameter)나 저장소에서 로드된 클로저(Closure)와 같이 함수가 알려지지 않은 경우, 해당 함수의 동작 술어가 그 효과를 설명합니다. 우리의 접근 방식은 예를 들어 Dafny와 달리, Rust 스타일의 참조 (References) 및 전역 변수 (Global variables)를 통해 상태를 수정할 수 있는 명령형 일급 함수를 지원한다는 점에서 차별화되며, Move가 가능하게 하는 메모리의 정적 분리 (Static separation) 덕분에 분리 논리 (Separation logic)보다 더 효율적인 SMT 인코딩을 제공합니다. 나아가 우리는 MVP의 명세 추론 (Specification inference) 도구를 함수 값과 함께 작동하도록 확장했습니다. 임의의 고차 Move 코드가 주어지면, 약한 전제 조건 (Weakest-precondition) 분석이 동작 술어 기반의 명세를 반자동으로 도출하여, 주석 작성 (Annotation) 부담을 줄이고 새로운 명세 구조를 위한 검증 파이프라인을 제공합니다.