Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Property-based Testing

Property-based Testing (PBT) は、少数の fixture では見落としやすい境界条件を、生成入力と「常に成り立つべき性質」で検査します。

本プロジェクトでは、Merkle tree、bitmap packing、input commitment、journal count のように、順序、境界、改ざん耐性が重要なロジックに PBT を置いています。

PBT を導入した理由

Example-based tests は既知のシナリオを守ります。 PBT はそれに加えて、input commitment の順序不変性、Merkle proof の改ざん拒否、LSB-first bitmap packing の境界安定性、journal count の分解式のような仕様レベルの性質を、生成器が到達できる範囲で探索します。

PBT は数学的証明ではありません（限界）。 それでも、CI で広い生成入力を継続的に試せるため、暗号周辺の encoding drift や境界条件の退行を早期に検出しやすくなります。

TypeScript 側の PBT

RFC 6962 Merkle tree

対象:

  • packages/merkle/src/rfc6962-merkle-tree.property.test.ts

検査する性質:

  • 任意の leaf set について inclusion proof が round-trip する
  • root、leaf、index、proof node を改ざんすると検証に失敗する
  • append-only consistency proof が old size / new size の組み合わせで検証できる
  • 奇数サイズ tree の代表ケースを固定 regression として保持する

Bitmap Merkle

対象:

  • packages/verification/src/merkle/bitmap-merkle-tree.property.test.ts

検査する性質:

  • 生成した bitmap の任意 index について proof が round-trip する
  • proof から抽出した included が元の bit と一致する
  • leaf chunk や Merkle パスの改ざんを拒否する
  • 認証済みの logical tree size から外れる bit の proof を拒否する
  • logical tree size より後ろの padding bit が非ゼロなら拒否する
  • 0, 1, 7, 8, 255, 256, 257, 511, 512, 513, 1025 bit の境界を固定ケースで検査する

Input commitment

対象:

  • packages/zkvm-contract/src/zkvm/__tests__/input-commitment.property.test.ts

検査する性質:

  • 同じ vote multiset の順序を入れ替えても input commitment が変わらない
  • duplicate index がある異常入力でも deterministic tie-break により順序が安定する
  • election ID、bulletin root、tree size、total expected を変えると commitment が変わる
  • vote の index、commitment、Merkle パスを変えると commitment が変わる

Journal invariants

対象:

  • packages/node-adapters/src/zkvm/journal-invariants.property.test.ts

検査する性質:

  • totalVotes = validVotes + rejectedRecords
  • invalidVotes = rejectedRecords
  • seenIndicesCount = validVotes + invalidPresentedSlots
  • validVotes + invalidPresentedSlots + missingSlots = treeSize
  • excludedSlots = missingSlots + invalidPresentedSlots
  • included bitmap の true は seen bitmap の true を含意する

Rust 側の PBT

対象:

  • zkvm/methods/guest/src/property_tests.rs

検査する性質:

  • input commitment が vote order に対して permutation invariant
  • duplicate index の tie-break を含めても permutation invariant
  • RFC 6962 inclusion proof が reference tree と一致する
  • root / leaf / path 改ざんを拒否する
  • bitmap root が reference oracle と一致する
  • bit flip で bitmap root が変わる
  • guest の slot / record accounting が現在の journal semantics と一致する
  • duplicate index の処理順序 semantics を固定する

Rust 側の PBT は、zkVM guest / contract-core で使う低レベル実装に近い場所で動きます。 TypeScript 側と同じ性質を別実装として検査します。

Lean との関係

PBT は実装に対して広い入力空間を探索します。 Lean は同種の不変条件を抽象モデル上で証明します。 両者の役割分担と、Lean から出力した generated vectors を介して実装テストに接続する仕組みは Lean による形式化 > 実装との接続 に整理しています。

限界

  • PBT は数学的証明ではない
  • 生成範囲は CI 実行時間とのバランスで制限する
  • SHA-256 の衝突困難性は PBT では証明しない
  • RISC Zero receipt soundness も PBT の対象ではない
  • 生成器に含めていない入力領域は探索されない

そのため、PBT は example-based tests や Lean formalization を置き換えるものではありません。 境界条件と実装 drift を検出する追加レイヤーとして扱います。