Formal Verification of Imperative First-Class Functions in Move

이 논문은 간단한 언어와 창의적인 비유를 사용하여 설명합니다.

큰 그림: "스마트 계약" 공장

아프토스 (Aptos) 를 디지털 자산 (예: 돈이나 티켓) 을 무브 (Move) 라는 특수 언어로 제작하는 고보안 공장으로 상상해 보세요. 이러한 자산이 도난당하거나 손상되지 않도록 하기 위해, 이 공장은 무브 프로버 (MVP) 라는 로봇 검사관을 사용합니다. 이 로봇은 설계도 (코드) 를 읽어 공장 가동 전에 모든 것이 올바르게 작동할 수 있음을 수학적으로 증명합니다.

오랫동안 이 로봇은 간단한 지시사항을 확인하는 데 뛰어났습니다. 하지만 최근 공장은 1 등 함수 (First-Class Functions) 라는 새롭고 까다로운 기능을 추가했습니다.

이 새로운 함수들을 마법 지팡이로 생각하세요.

• 과거 방식: 마법을 부리기 위해 직접 지팡이를 들고 있어야 했습니다. 로봇은 당신이 어떤 마법을 부리는지 정확히 알 수 있었습니다.
• 새로운 방식: 지팡이를 상자에 넣고 친구에게 건네거나, 금고에 보관하거나, 내용물을 모르는 기계에 전달할 수 있습니다. 이 기계는 단지 "지팡이를 흔들어 마법을 부려야 한다"는 사실만 알 뿐, 마지막 순간이 될 때까지 어떤 지팡이인지 알지 못합니다.

이를 동적 디스패치 (Dynamic Dispatch) 라고 합니다. 이는 강력하지만, 로봇 검사관이 어떤 특정 마법이 부려질지 미래를 볼 수 없기 때문에 로봇을 혼란에 빠뜨립니다.

문제: "블랙박스" 딜레마

이 논문은 저자들이 로봇 검사관 (MVP) 을 이러한 마법 지팡이를 당황하지 않고 처리할 수 있도록 업그레이드한 방법을 설명합니다.

이전에는 함수가 "블랙박스"(함수를 담고 있는 변수) 일 경우, 로봇은 모든 가능성을 추측하거나 한 번에 모두 확인해야 했으며, 이로 인해 수학 계산이 폭발하고 로봇이 느려졌습니다.

저자들은 이 문제를 해결하기 위해 두 가지 새로운 도구를 도입했습니다.

1. 행동 술어 (Behavioral Predicates): "보증서"

로봇은 이제 마법 지팡이 내부가 어떻게 작동하는지 들여다보는 대신, 지팡이에 부착된 보증서를 봅니다.

• 과거 방식: "사용을 허가하기 전에 이 가격계산 지팡이가 코드 한 줄 한 줄까지 어떻게 작동하는지 정확히 알아야 합니다."
• 새로운 방식: "지팡이 내부가 어떻게 작동하는지는 중요하지 않습니다. 보증서만 읽으면 됩니다. 보증서에는 다음과 같이 적혀 있습니다: '5 개의 코인을 주면 3 개의 코인을 돌려주고, 절대 고장 나지 않습니다.'"

논문은 이를 행동 술어 (Behavioral Predicates) 라고 부릅니다. 이는 다음을 설명하는 계약과 같습니다:

• 전제 조건 (Pre-conditions): 지팡이를 흔들기 전에 무엇이 참이어야 하는지.
• 후제 조건 (Post-conditions): 지팡이를 흔든 후 무엇이 참이 될 것인지.
• 중단 조건 (Abort conditions): 지팡이가 폭발 (실패) 할 수 있는 경우.

이를 통해 로봇은 지팡이 내부의 비밀 레시피를 알 필요 없이 지팡이의 약속만 확인하면 됩니다.

2. 상태 레이블 (State Labels): "타임스탬프 카메라"

때로는 일련의 사건이 발생합니다. 예를 들어, 공장에서 한 로봇이 자동차를 페인트하고 다른 로봇이 바퀴를 장착한다고 상상해 보세요.

자동차가 안전한지 증명하려면 페인트 작업이 끝난 후, 바퀴가 장착되기 전의 자동차 상태를 알아야 합니다.

저자들은 상태 레이블 (State Labels) 을 도입했습니다. 이를 과정의 특정 지점에 설치된 타임스탬프 카메라로 생각하세요.

• 카메라 A (시작): 자동차는 맨몸의 금속 상태입니다.
• 카메라 B (중간): 자동차는 페인트가 칠해졌습니다.
• 카메라 C (끝): 바퀴가 장착되었습니다.

이제 로봇은 다음과 같이 말할 수 있습니다: "페인트 작업은 카메라 A 와 B 사이에서 발생했고, 바퀴는 카메라 B 와 C 사이에 장착되었습니다." 이는 로봇이 어떤 순간의 세계가 어떻게 보였는지 혼동하지 않고 복잡한 사건 순서에 대해 추론할 수 있게 합니다.

로봇이 실제로 작동하는 방식 (스위치보드)

논문은 로봇이 이러한 아이디어를 컴퓨터가 해결할 수 있는 수학 (SMT 논리) 으로 어떻게 변환하는지 설명합니다.

로봇에게 스위치보드가 있다고 상상해 보세요.

1. 시나리오 A (알려진 지팡이): 로봇이 특정하고 알려진 지팡이 (예: product 함수) 를 보면 스위치를 "직접 모드"로 전환합니다. 보증서를 무시하고 해당 특정 지팡이의 실제 코드만 확인합니다.
2. 시나리오 B (알 수 없는 지팡이): 로봇이 일반적인 상자 (변수) 를 보면 스위치를 "추상 모드"로 전환합니다. 코드는 완전히 무시하고 시스템이 안전한지 증명하기 위해 **보증서 (행동 술어)**에만 의존합니다.

이 방식은 효율적입니다. 로봇이 가능한 모든 상자를 열어보려고 노력할 필요가 없기 때문입니다. 로봇은 알고 있는 상자만 열고, 나머지는 계약서를 신뢰합니다.

"자동 검사관" (명세 추론)

이 논문의 가장 멋진 부분 중 하나는 로봇이 이제 자신의 보증서를 작성할 수 있다는 점입니다.

보통 인간이 수동으로 이러한 보증서를 작성해야 하는데 이는 지루한 작업입니다. 저자들은 로봇이 코드를 보고 보증서에 무엇이 적혀야 하는지 파악하여 대신 작성할 수 있도록 업그레이드했습니다.

• 입력: 마법 지팡이가 포함된 지저분한 코드 조각.
• 로봇 행동: "이 코드가 수수료 존재 여부를 확인하는 것을 보았습니다. 저는 ' 수수료가 없으면 이 지팡이는 폭발합니다'라고 적힌 보증서를 작성하겠습니다."
• 결과: 로봇이 자신의 작업을 확인합니다. 코드가 보증서와 일치하면 통과됩니다.

논문에서는 자동 시장 제조자 (AMM) 예시로 이를 시연합니다. 이는 자산을 거래하는 시스템입니다. 로봇은 가격 결정 규칙 (마법 지팡이) 이 사용자에 의해 변경될 수 있음에도 불구하고, 새로운 지팡이가 보증서에 적힌 규칙을 따르는 한 시스템이 결코 충돌하거나 자산을 잃지 않음을 증명했습니다.

성과 요약

이 논문은 스마트 계약 검증에서 큰 골치 아픈 문제를 해결했다고 주장합니다.

1. 저장, 전달, 동적 변경이 가능하도록 **마법 지팡이 (함수)**를 안전하게 사용할 수 있게 했습니다.
2. 로봇이 지팡이 내부를 볼 필요 없이 이러한 지팡이에 대해 이야기할 수 있는 새로운 언어 (행동 술어 + 상태 레이블) 를 만들었습니다.
3. 코드와 계약을 번갈아 보는 "스위치보드" 방식을 사용하여 로봇을 더 빠르고 똑똑하게 만들었습니다.
4. 로봇이 필요한 계약을 자동으로 생성하도록 하여 서류 작업을 자동화했습니다.

요약하자면, 그들은 로봇 검사관에게 stranger 의 비밀을 알 필요 없이 stranger 의 약속 (계약) 을 신뢰하는 법을 가르쳤으며, 이로 인해 공장은 더 안전하고 유연해졌습니다.