대부분의 스마트 컨트랙트 버그는 생소한 것이 아닙니다. 그것은 >가 >=가 되었어야 했거나, 하나의 뮤테이터(mutator) 이후 조용히 깨져버리는 불변량(invariant), 혹은 회계 처리에서의 off-by-one 오류 같은 것들입니다. 테스트는 당신이 우연히 이를 깨뜨리는 입력을 테스트했을 때만 잡아낼 수 있습니다. 저는 모든 입력에 대해 속성이 유지됨을 증명하거나, 아니면 저에게 **구체적인 반례(concrete counterexample)**를 건네주는 무언가를 원했습니다. 그리고 저는 Z3, JavaSMT, 혹은 외부 솔버(solver) 없이 증명 코어(proving core)를 직접 구축하고 싶었습니다.

이것이 DhrLang의 contract prove가 작동하는 방식이며, 제가 의도적으로 선을 그은 지점입니다.

작성하는 컨트랙트

함수에 항상 참이어야 하는 내용을 주석으로 달고 프로버(prover)를 실행합니다:

@contract
class Adder {
    @checked
...

dhrlang contract prove --bound=8 adder.dhr

모든 의무(obligation)는 정확히 다음 세 가지 판결 중 하나로 돌아옵니다:

• PROVED — 모든 입력에 대해 참임 (여기서는 num 파라미터가 음수가 아닌 256비트 값이므로, a + b >= a임).
• REFUTED — 거짓이며, 재현 가능한 반례를 제공함.
• UNKNOWN — 프로버가 결정할 수 없으며, 추측하는 대신 이를 알림.

이 세 번째 판결이 이 도구의 핵심 윤리입니다. 즉, 이 도구는 **건전성(sound)**을 갖추고 있습니다. 실제 증명 없이 PROVED라고 말하지 않으며, 확인된 구체적인 실패 없이 REFUTED라고 말하지 않습니다.

명세 언어 (The spec language)

세 가지 어노테이션(annotation)과 산술 모드 마커가 있습니다:

• @requires(...) — 호출자가 충족해야 하는 전제 조건(precondition).
• @ensures(...) — 파라미터와 result에 대한 사후 조건(postcondition).
• @invariant(...) — 모든 뮤테이터(mutator)가 보존해야 하는 컨트랙트 전반의 속성(property).

가드된 뺄셈(guarded subtraction)은 정확히 다음과 같이 증명합니다:

@contract
class Sub {
    @requires(b <= a)
...

그리고 상태를 변경하는 메서드(state-mutating method, kaam은 DhrLang의 void 메서드 키워드임)에 대해 확인되는 컨트랙트 불변량(contract invariant)은 다음과 같습니다:

@invariant(total == a + b)
@contract
class Sum {
...

프로버는 컨트랙트의 제네시스 상태(genesis state)로부터 set을 기호적으로 실행(symbolically runs)하며, 이후에도 모든 x, y에 대해 total == a + b가 여전히 유지됨을 증명합니다.

작동 원리, 파트 1: 기호 실행 (symbolic execution)

각 함수는 표준적인 생성 후 상태(storage 스칼라 0)로부터 분석됩니다. 매개변수(Parameters)는 새로운 **비음수 256비트 심볼(non-negative 256-bit symbols)**이 됩니다. 그 후 본문은 기호적으로(symbolically) 해석됩니다:

• 순차적 코드(straight-line code), 지역 선언/할당, 그리고 스칼라 저장소(scalar storage) 쓰기는 기호 환경(symbolic environment)을 업데이트합니다.
• if / else는 경로를 **분기(forks)**하며, 분기 조건(또는 그 부정)을 가정(assumption)으로 추가합니다.
• require / assert / revert는 이후 과정에서 조건을 **가정(assume)**하거나 경로를 완전히 **제거(prune)**합니다.

리버트(reverting)되지 않는 각 터미널 경로에서, 증명기(prover)는 하나의 호어 스타일(Hoare-style) 의무(obligation)를 형성합니다:

(requires  ∧  path-conditions  ∧  every atom ≥ 0)   ⇒   goal

작동 원리, 파트 2: 선형성 유지하기 (재미있는 부분)

항(Terms)은 불변의 **선형 형태(linear form)**인 constant + Σ coeffᵢ · atomᵢ로 표현됩니다. 결정 절차(decision procedure)는 형태를 선형으로 유지하는 연산, 즉 덧셈, 뺄셈, 부정, 그리고 *상수(constant)*에 의한 곱셈/나눗셈만을 필요로 합니다.

그렇다면 진정으로 비선형적인 것들 — a * b, 나눗셈, 나머지, 시프트(shifts), 매핑(mapping) 읽기 등은 어떻게 될까요? 이러한 것들은 하나의 **불투명 원자(opaque atom)**로 접힙니다. 즉,

1. 목표 부정 (Negate the goal). 엄격한 부등식은 정수성 (integrality)을 사용하여 강화됩니다 — G > 0은 G ≥ 1 (즉, G - 1 ≥ 0)이 됩니다 — 그리고 등식 목표 G == 0은 두 개의 독립적인 반증(refutation), 즉 G ≥ 1과 G ≤ -1로 분리되며, 이 두 가지 모두 불가능해야 합니다.
2. 시스템 구축 (Build the system). 모든 가설, 부정된 목표, 그리고 각 원자(atom)당 하나의 atom ≥ 0 행(uint256 도메인 제약 조건)은 Σ coeffᵢ·atomᵢ + constant ≥ 0 형태의 행이 됩니다.
3. 제거 (Eliminate). Fourier–Motzkin 제거법을 사용하여 원자들을 하나씩 투영(project)합니다 — 각 양의 계수 행을 각 음의 계수 행과 쌍을 맺습니다 (양의 정수로만 스케일링하며, 나눗셈은 하지 않습니다). 만약 시스템이 순수한 constant < 0으로 붕괴된다면, 이는 모순입니다: 부정(negation)이 불가능하므로, 명세(spec)는 증명됨 (PROVED) 상태가 됩니다.

이것이 건전한(sound) 이유: 제거 과정은 유리수 (rationals) 상에서의 충족 가능성(satisfiability)을 결정하며, 유리수 해가 없는 시스템은 정수 해도 가질 수 없으므로, 유리수-UNSAT ⇒ 정수-UNSAT이 성립합니다. 따라서 증명기(prover)는 잘못하여 PROVED라고 선언할 수 없습니다. 최악의 경우 참인 사실을 증명하지 못할 뿐이며, 이는 단지 UNKNOWN이 됩니다.

체크된 산술 (checked arithmetic)이 핵심인 이유

선형 이론(linear theory)은 +, -, *를 수학적 정수로 모델링합니다. 이는 오버플로(overflow)가 조용히 래핑(wrap)되지 않을 때만 건전합니다. @checked 하에서는 오버플로가 발생하는 연산이 **리버트 (revert)**되므로, 모든 리버트되지 않는 경로에서 값은 정확한 수학적 결과와 일치하며 증명은 EVM으로 전달됩니다. @unchecked 하에서는 증명이 꺼지며 의무(obligation)는 UNKNOWN이 됩니다:

@unchecked
@ensures(result == a + b)
num addU(num a, num b) { return a + b; }   // → 설계에 따라 UNKNOWN

이것이 바로 DhrLang v4.0.0이 (Solidity 0.8+와 일치하도록) 체크된 산술을 **기본값 (default)**으로 설정한 정확한 이유입니다: 안전한 의미론(semantics)이 곧 증명 가능한 의미론이기 때문입니다.

증명할 수 없는 경우: 오탐(false positive) 없는 반증

명세를 거짓인 것으로 변경해 보겠습니다:

@checked
@ensures(result > a)     // b == 0일 때 거짓
num add(num a, num b) { return a + b; }

증명기(prover)는 유계 구체적 탐색(bounded concrete search)을 수행하여 a=0, b=0을 찾아냅니다. 결정적으로, 증명기는 선형 추론(linear reasoning)만으로 이를 보고하지 않습니다. 대신 후보를 DhrLang의 기존 구체적 스펙 퍼저(concrete spec-fuzzer, 즉 L3 엔진)에 전달하며, 해당 엔진이 실제로 함수를 실행하고 위반 사항을 재현했을 때만 REFUTED라고 보고합니다. 퍼저는 정답(ground-truth) 오라클 역할을 하므로, 위양성(false positives)이 전혀 없습니다. 깨진 불변량(total = x + y + 1)도 동일한 방식으로 포착되어 invariant violated로 보고됩니다.

의도적으로 수행하지 않는 것들

이 부분은 제가 어떤 인터뷰에서든 가장 먼저 언급할 부분입니다. 정직함이 핵심이기 때문입니다.

• **루프(Loops)**는 모델링되지 않습니다. while 문은 사후 조건(postcondition)을 UNKNOWN으로 만듭니다.
• **매핑 에일리어싱(Mapping aliasing), 외부 호출(external calls), 그리고 선형 이론(linear theory)이 감지할 수 없는 비선형 조합(nonlinear combinations)**은 모두 UNKNOWN으로 처리됩니다.
• 이것은 프로덕션용이 아닌 **실험적 단계(L2b)**이며, Certora나 Halmos의 경쟁자가 아닙니다. 그것들은 실제 Solidity를 검증하는 성숙하고 완전한 SMT 기반 도구들입니다. 이것은 심볼릭 실행(symbolic execution)과 결정 절차(decision procedures)를 밑바닥부터 이해하기 위해 제가 처음부터 구축한 핵심 엔진입니다.

이것의 정체는 다음과 같습니다: 외부 솔버 없이, 일련의 실제 컨트랙트 속성들을 '예(yes) / 반례(counterexample) / 정직한 어깨 으쓱(honest-shrug)' 답변으로 변환하는 작고 건전한(sound) 검증기입니다.

배운 점

이 프로젝트를 구축하면서 EVM 실행 모델, 계약에 의한 설계(design-by-contract), 심볼릭 실행(symbolic execution), 그리고 왜 유리수(rationals)가 여기서 Fourier–Motzkin을 건전하게 만드는지 알 수 있을 만큼의 증명 이론(proof theory)을 배웠습니다. 가장 어렵고도 만족스러웠던 결정은 UNKNOWN이라는 규율을 지키는 것이었습니다. 거짓말을 하는 검증기는 검증기가 없는 것보다 못하며, 대부분의 엔지니어링 작업은 과도하게 주장하지 않기 위해 투입되었습니다.

코드: github.com/dhruv-15-03/DhrLang (src/main/java/dhrlang/proving). 저의 다른 작업물: dhruvrastogi.me. 저는 블록체인 인프라 / 백엔드 / 툴링 역할을 찾고 있습니다. 이 내용에 대해 언제든 자세히 설명해 드릴 준비가 되어 있습니다.