기술 요약: 확장성 상수 배열에 대한 만족도 (Satisfiability Modulo Extensional Constant Arrays)

문제 제기

기계 정수와 결합된 배열 데이터 구조에 대한 추론은 하드웨어 및 소프트웨어 검증의 기본 요구사항입니다. SMT-LIB 에서 정의되고 McCarthy 에 의해 공리화된 표준 만족도 이론 (Satisfiability Modulo Theories, SMT) 인 확장성 배열 이론은 select(읽기) 와 store(쓰기) 연산자 및 확장성 공리를 제공합니다. 많은 검증 작업에 충분하지만, 기본값으로 초기화된 배열 (예: 0 으로 초기화된 메모리) 을 모델링할 때 이 이론은 간결성이 부족합니다.

표준 이론에서 이러한 초기화는 모든 관련 인덱스에 기본값을 쓰는 깊이 중첩된 store 표현을 통해 표현되어야 합니다. 이는 모델링의 부정확성 (인덱스는 명시적으로 재작성될 수 있음) 과 store 체인의 깊이로 인한 해결 절차의 심각한 비효율성을 초래합니다.

모든 인덱스에 단일 요소를 저장하는 상수 배열로 이론을 확장하면 간결한 해결책을 제공합니다. 그러나 기존 확장성 상수 배열에 대한 결정 절차는 무한 인덱스 도메인으로 제한됩니다. 유한 인덱스 도메인의 경우, 기존 SMT 솔버는 비확장성 조각만 지원하거나, 일부 솔버의 경우 유한 인덱스를 가진 상수 배열에 대한 확장성 추론 시 잘못된 답변을 생성합니다. 핵심 과제는 유한 도메인을 가진 서로 다른 상수 배열에 대한 store 연산 시퀀스가 인덱스를 충분히 업데이트함으로써 동일하게 만들 수 있는지 여부를 결정하는 것이며, 이는 무한한 경우에서는 발생하지 않는 문제입니다.

방법론

저자들은 유한 도메인을 포함한 임의의 인덱스 도메인을 지원하는 확장성 상수 배열 이론 ($T_{\langle A \rangle}$) 에 대한 새로운 결정 절차를 제시합니다. 이 절차는 이전 작업에서 제시된 확장성 배열 (DPA) 에 대한 요구 사항에 따른 레마 (Lemmas on Demand, LOD) 절차를 일반화하고 확장한 CAEXT라는 추상적 연산으로 형식화됩니다.

연산 CAEXT

이 연산은 $\langle A, I, \pi \rangle$ 구성에서 작동하며, 여기서 $A$는 평탄한 리터럴 (flat literals) 의 집합, $I$는 빈 이론 ($T_E$) 에 대한 해석, $\pi$는 전파 단계의 매핑입니다. 이 절차는 모든 인덱스에 대한 가상 읽기를 도입하는 것 (무한 도메인에서는 불가능하고 대규모 유한 도메인에서는 계산 비용이 많이 듦) 을 피하고, 대신 기본값을 전파하고 업데이트된 인덱스를 추적합니다.

연산의 주요 구성 요소는 다음과 같습니다:

1. 기본 연산 (AEXT): LOD 절차를 임의의 인덱스 및 요소 정렬로 일반화하여 특정 이론 조합과 분리합니다. 이는 McCarthy 의 읽기 - 쓰기 공리 (row-eq, row-ne) 와 확장성 공리 (ext) 에 기반하여 읽기 정보를 전파합니다.
2. 상수 배열 확장:
   • 기본값 전파: 모든 인덱스에 대한 읽기를 생성하는 대신, 연산은 상수 배열 $\langle v \rangle$의 기본값 $v$를 다른 배열로 전파합니다. 이는 전파 경로에서 배열 $a$가 기본값 $\langle v \rangle$와 다른 인덱스를 나타내는 업데이트된 인덱스 집합 $I(a, \langle v \rangle)$를 유지합니다.
   • 충돌 감지 (CongC): 서로 다른 기본값 $v$와 $w$가 동일한 배열 $a$로 전파될 때, 연산은 업데이트된 인덱스 집합 $I(a, \langle v \rangle) \cup I(a, \langle w \rangle)$가 전체 인덱스 도메인을 덮는지 확인합니다. 도메인이 유한하고 업데이트된 인덱스가 모든 가능한 인덱스를 덮지 않는다면, $v \approx w$가 아닌 한 충돌이 발생합니다.
   • DistinctN 인코딩: 양화된 공식 $\exists i : \sigma. \bigwedge_{k \in I} i \neq k$(업데이트되지 않은 인덱스가 존재하는지 확인) 을 효율적으로 처리하기 위해, 구현은 이를 특수한 distinctN 제약으로 인코딩합니다. 이는 업데이트된 인덱스 집합이 인덱스 도메인의 크기 $n$만큼의 서로 다른 값을 포함하는지 확인합니다.

구현

이 결정 절차는 최첨단 SMT 솔버인 Bitwuzla에 구현되었습니다. 비트 - 벡터 솔버가 해석 $I$를 제공하는 Bitwuzla 의 기존 LOD 아키텍처와 원활하게 통합됩니다. 구현에는 distinctN 제약의 지연 확장 및 메모리 오버헤드를 최소화하기 위한 전파 경로에 대한 너비 우선 탐색과 같은 최적화가 포함되어 있습니다.

주요 기여

1. LOD 의 일반화: 저자들은 고정 크기 비트 - 벡터를 가진 확장성 배열에 대한 LOD 절차를 임의의 인덱스 및 요소 정렬로 일반화했습니다.
2. 추상 연산 AEXT: 그들은 LOD 해결 패러다임과 독립적인 확장성 배열 이론을 위한 분리된 추상 연산인 AEXT 를 제시했습니다.
3. 상수 배열로의 확장 (CAEXT): 그들은 AEXT 를 확장성 상수 배열을 처리하도록 확장하여 부정적 건전성(unsat 이 보고되면 입력이 만족 불가능함) 과 만족 가능성 건전성(unsat 없이 포화 구성에 도달하면 입력이 만족 가능함) 을 증명했습니다.
4. 구현 및 평가: 이 절차는 Bitwuzla 에 구현되었으며 다양한 벤치마크에서 평가되어 기존 Bitwuzla 및 기타 주요 솔버 (Z3, cvc5, MathSAT5) 보다 성능이 크게 향상됨을 입증했습니다.

결과

평가에는 다섯 가지 벤치마크 세트가 사용되었습니다: smtlib(양화 논리), mbqi(모델 기반 양화 인스턴스화의 하위 쿼리), k-ind(증분 하드웨어 모델 체킹), hevm(이더리움 가상 머신), crafted(유한 상수 배열 확장성을 테스트하도록 특별히 설계된 합성 벤치마크).

• 성능: 새로운 절차가 적용된 Bitwuzla(Bitwuzla⟨A⟩) 는 모든 다른 솔버를 크게 앞섰습니다. smtlib세트에서 해결된 벤치마크 수는 기존 Bitwuzla 대비 5 배 증가했습니다 (3,545 대 717). mbqi세트에서 Bitwuzla⟨A⟩는 4,147 개의 쿼리 전체를 해결한 반면, 기존 버전은 4 개만 해결했습니다.
• 정확성: 서로 다른 기본값을 가진 유한 상수 배열에 대한 등식을 인코딩한 crafted⟨A⟩세트에서 Bitwuzla⟨A⟩는 모든 인스턴스에 대해 정확한 답변을 제공한 유일한 솔버였습니다. Z3 와 MathSAT5 는 입력을 수락했지만 상당수의 벤치마크에서 잘못된 답변을 보고했습니다. cvc5 와 기존 Bitwuzla 는 지원 부족으로 인해 입력을 완전히 거부했습니다.
• 건전성 검증: 저자들은 crafted⟨A⟩세트에서 솔버가 생성한 모델을 검증했습니다. Bitwuzla⟨A⟩만이 자신의 만족 가능성 주장과 일치하는 모델을 생성했습니다. Z3 와 MathSAT5 는 원래 공식으로 다시 주장했을 때 모순을 초래하는 모델을 생성했습니다.

의의

이 논문은 제안된 결정 절차가 Bitwuzla 의 해결 능력을 크게 확장하여, 이전에는 다른 도구로 해결 불가능하거나 잘못 처리되었던 유한 인덱스 도메인을 가진 확장성 상수 배열과 관련된 문제를 처리할 수 있게 했다고 주장합니다.

이 연구는 SMT 해결의 중요한 격차를 해소합니다. 상수 배열은 메모리 초기화를 위한 표준 모델링 패턴이지만, 기존 솔버는 유한 도메인에서의 지원을欠하거나 건전하지 않은 결과를 제공합니다. 유한 및 무한을 포함한 확장성 상수 배열의 전체 이론에 대한 건전하고 완전한 결정 절차를 제공함으로써, 이 연구는 하드웨어 모델 체킹 및 스마트 계약 검증 (특히 이더리움 가상 머신용) 과 같은 응용 분야에서 더 정확하고 효율적인 검증을 가능하게 합니다. 저자들은 평가가 유한 도메인에 초점을 맞췄지만, 이 절차는 기본 솔버 아키텍처에 구애받지 않으며 무한 도메인 경우를 완전히 지원한다고 명시했습니다.