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

요약

Aptos의 Move 언어에 도입된 명령형 일급 함수(Imperative First-Class Functions)를 Move Prover(MVP)에서 형식 검증하기 위한 새로운 방법론을 제안합니다. 동작 술어(Behavioral predicates)와 상태 레이블(State labels)을 도입하여 함수 값의 상태 전이를 설명하며, SMT 인코딩을 통해 고차 함수를 효율적으로 검증합니다. 또한, 약한 전제 조건(Weakest-precondition) 분석을 통해 명세를 반자동으로 도출하는 추론 도구 확장 기능도 포함합니다.

핵심 포인트

• Move의 고차 함수 도입에 따른 동적 디스패치 및 명령형 함수 검증 방법론 제시
• 단일/이중 상태 술어와 상태 레이블을 활용한 함수 동작 및 상태 전이 모델링
• Rust 스타일의 참조 및 전역 변수 수정을 지원하는 명령형 일급 함수 검증 방식
• Move의 메모리 정적 분리 특성을 활용하여 분리 논리보다 효율적인 SMT 인코딩 구현
• 명세 추론 도구를 통한 약한 전제 조건 기반의 반자동 명세 도출 기능