example-based test는 맵을 만들고 연산을 수행한 뒤 결과를 확인하며, iddqd는 내부 unit test와 public API integration test를 갖고 있음
이 테스트들은 doctest로도 존재해 문서 역할을 함께 함
병적인 테스트는 buggy Ord와 다른 trait 구현을 공급함
CI에서는 regular test와 pathological test를 Miri 아래에서 실행해 여러 종류의 UB를 탐지함
중복 인덱스가 없어야 한다는 불변식 같은 조건은 Miri 밖의 일반 테스트 환경에서도 확인할 수 있음
모델 기반 테스트와 fault injection
iddqd는 두 계층의 randomized testing을 사용함: 올바른 oracle과 비교하는 model-based testing, 그리고 그 위의 fault injection
model-based testing 또는 stateful property-based testing은 무작위 연산 시퀀스를 타입 인스턴스에 적용하고, 결과를 올바르다고 알려진 oracle과 비교함
iddqd는 비효율적이지만 명확하게 올바른 NaiveMap oracle을 기준으로 광범위한 model-based test를 실행함
fault injection은 user code에 버그를 무작위로 넣는 방식이며, iddqd에서는 panic safety가 특히 유효한 축이었음
user code가 연산 중간에 panic하더라도 맵의 불변식이 깨지면 안 됨
각 맵 연산에 무작위 panic countdown을 붙이고, user code 호출마다 countdown을 1씩 줄이다가 0이 되면 panic하게 해 무작위 panic safety testing을 수행함
이 방식은 iddqd에서 미묘한 버그 여러 개를 찾았고, 일부는 unsoundness로 이어졌음
model-based test는 각 연산 뒤에 no-duplicate-index 같은 내부 불변식도 검증함
model-based test는 Miri 아래에서 실행하기에는 너무 느려서, soundness와 correctness가 의존하는 불변식을 별도로 확인함
LLM 적대적 리뷰와 형식 기법
current-generation frontier model은 맵을 손상시키는 병적인 user code 구현을 여러 개 찾아냄
한 notable case에서는 custom allocator가 panic하고 unwind할 때 맵 불변식이 깨지는 경로를 LLM이 구성함
이는 기존 panic safety test가 다루던 Ord 구현 같은 일반 user code panic과 다른 panic safety 문제였음
LLM은 그럴듯하지만 틀린 soundness claim도 만들 수 있으므로, Miri를 oracle로 쓰는 red-green TDD가 방어책이 됨
soundness bug에서는 먼저 Miri 아래에서 UB를 보이는 테스트를 만들고, 수정 뒤 같은 테스트가 통과하는지 다시 확인함
Kani 같은 model checker로 맵 불변식을 증명하는 접근은 iddqd가 너무 복잡해 필요한 proof가 도구가 감당하기 어려운 수준으로 커짐
Creusot은 Rust 코드가 panic과 다른 오류에서 자유롭다는 점을 증명하는 데 도움을 줄 수 있지만, user code가 panic하거나 잘못 동작해도 유지되어야 하는 불변식은 현 시점에서 증명하지 못함
NaiveMap은 iddqd에 가장 가까운 specification 역할을 하며, CI에서 model-based test를 수천 번 실행해 구현이 specification과 맞는지에 대한 높은 신뢰를 얻음
cargo-anneal은 unsafe Rust 옆 doc comment에 Lean soundness proof를 넣을 수 있게 하는 개발 중 도구로 관심 대상임
iddqd는 명확한 불변식과 제한적이지만 사소하지 않은 범위를 갖고 있어 형식 검증 도구의 benchmark 후보가 됨
결론
unsafe generic Rust는 임의의 trait 구현과 적대적 구현까지 고려해 각 불변식을 유지해야 하므로 극히 어렵다
iddqd의 버그는 병적인 Ord 구현이 맵을 속여 같은 메모리에 대한 mutable alias를 만들 수 있음을 보여줌
단일 기법만으로 모든 버그를 잡을 수 없으므로, 사람의 line-by-line unsafe reasoning, example-based test, pathological test, randomized test, frontier model adversarial review를 함께 사용함
Oxide는 foundational infrastructure에서 이런 수준의 엄격함이 정당하다고 봄