Kaniの探索が終わらないとき — 境界を狭める前に記録すること

探索を小さくしたとき，何を証明することになったか

KaniでHarnessを書き，cargo kaniを実行する．小さな関数ではすぐ結果が返っても，CollectionやLoop，深いCall Graphを含むCodeでは，時間やMemoryの予算内に終わらないことがあります．

そこで入力を8件から4件へ減らす．kani::assumeを足す．重い関数をStubにする．探索を扱える大きさへ変えることは必要です．そのとき，最初に確かめたかったClaimと，最後の結果が保証するClaimを対応付けて残すことが重要になります．

形式検証を開発ループへの続編として，本稿ではProof Journal，前提の分類，未完了な保証の管理を扱います．Kaniの公式Guideも，Loop，Symbolicな型，大きな整数演算などを切り分け，Solver変更や入力分割を試す手順を説明しています．[1]

サンプル一式は，架空の状態遷移，Harness，Journal，Assumption Registry，未記入の実行記録と独立したLoop Contract例です．Rust Build・Test，Kani・CBMC，Coverage，実行時間・Memory測定は実行していません．小さな例が実際に遅かったという報告でもありません．実行予定と観測済みEvidenceを分けます．

1．Claim・Model・探索条件・結果を分ける

「Kaniで証明済み」だけでは，何を判断できるか分かりません．少なくとも次をCodeと一緒に保存します．

結果が返らなかったときは，「安全」とも「Bugがある」ともまだ結論しません．どの段階で止まったか，Compiler・展開・Solverのどこまで進んだかをLogに残します．「Kaniは遅い」という一般論へ変える前に，対象と条件を固定します．

公式の実Code向けGuideは，多数のLoop，複雑なData Structure，I/O，深いCall Graph，大きなGlobal Stateを最初の対象として避けることを勧めています．検証が難しいことは責務の分離を見直すSignalになり得ますが，それだけで設計が悪いと決まるわけではありません．[2]

2．状態遷移と，履歴Propertyを定義する

例では，JobをPending → Approved → Executing → DoneまたはFailedへ進めます．未対応のCommandは状態を変えず，DoneとFailedは終端です．これは説明用のSemanticsであり，前稿のResultを返す遷移APIとは異なります．

#[derive(Copy, Clone, Debug, Eq, PartialEq)]
#[cfg_attr(kani, derive(kani::Arbitrary))]
pub enum JobState { Pending, Approved, Executing, Done, Failed }

#[derive(Copy, Clone, Debug, Eq, PartialEq)]
#[cfg_attr(kani, derive(kani::Arbitrary))]
pub enum Command { Approve, Start, Complete, Fail }

// This educational model treats unsupported transitions as no-ops.
// It is distinct from the earlier article's Result-returning transition API.
pub fn transition(state: JobState, command: Command) -> JobState {
    match (state, command) {
        (JobState::Pending, Command::Approve) => JobState::Approved,
        (JobState::Approved, Command::Start) => JobState::Executing,
        (JobState::Executing, Command::Complete) => JobState::Done,
        (JobState::Executing, Command::Fail) => JobState::Failed,
        _ => state,
    }
}

確認したいのは，「Pendingから始まり，最後がDoneなら，それより前にExecutingを訪れている」です．履歴はCommand適用前の状態から更新します．DoneになっただけでFlagを立てると，確認したい性質を計測Code自身へ埋め込んでしまいます．

// History records the state BEFORE this command is applied.
// Entering Done does not itself set the history flag.
pub fn step_with_history(state: JobState, seen: bool, command: Command)
    -> (JobState, bool)
{
    (transition(state, command), seen || state == JobState::Executing)
}

pub fn run_with_trace(mut state: JobState, commands: &[Command]) -> (JobState, bool) {
    let mut seen = state == JobState::Executing;
    let mut index = 0;
    while index < commands.len() {
        (state, seen) = step_with_history(state, seen, commands[index]);
        index += 1;
    }
    (state, seen)
}

TraceもReview対象です．今回のFlagはProcess内の観測であり，永続化されたAudit Logの完全性や，外部Jobが本当に実行されたことの証拠ではありません．初期状態を任意の復元状態へ変えるなら，初期Doneや履歴欠落をどう扱うかからClaimを見直します．

3．「ちょうど8件」と「0〜8件」は違う

let commands: [Command; 8] = kani::any();をそのまま渡すHarnessは，ちょうど8件を表します．Journalにmax_length: 8と書くだけで，空列や短い列を明示的に検証したことにはなりません．

今回の終端状態とNo-opの性質から，Paddingによる関係を別途論じることはできます．しかしその補題を暗黙にする必要はありません．長さもSymbolicにして，0〜8件を直接表します．

fn history_invariant(state: JobState, seen: bool) -> bool {
    state != JobState::Done || seen
}

/// JOB-001: all represented lengths from zero through eight.
/// Unwind 9 is a proposed setting, not an observed sufficient bound.
#[kani::proof]
#[kani::unwind(9)]
fn job_001_up_to_eight() {
    let storage: [Command; 8] = kani::any();
    let len: usize = kani::any();
    // V-001: verification-only size limit; no production batch contract exists.
    kani::assume(len <= storage.len());
    let (state, seen) = run_with_trace(JobState::Pending, &storage[..len]);
    kani::cover!(len == 0, "empty sequence is represented");
    kani::cover!(state == JobState::Done, "Done is reachable");
    kani::cover!(state == JobState::Failed, "Failed is reachable");
    assert!(history_invariant(state, seen));
}

storageの8要素自体が既に表現上のBoundです．assumeだけを検索しても，こうした制限は見つかりません．このHarnessのClaimは，表現したCommandの，長さ0〜8のすべての列についてのものです．任意長の列，Concurrency，Persistence，分散Retryは含みません．

#[kani::unwind(9)]は，この単純なLoopに対する候補設定です．実際に十分だったという実行結果はありません．Input BoundとUnwindの意味を，次に分けます．

4．小さいUnwindで，展開不足を診断する

KaniのGuideは，小さい#[kani::unwind(1)]で早期に展開を止め，問題を切り分ける方法を示しています．ただしLoop前の処理や別の高価な演算もあるため，短時間での終了を保証する設定ではありません．必要ならProcess全体の時間・Memory予算も別に設けます．[2][3]

# 実行予定．本稿では実行していません．
cargo kani --harness job_001_up_to_eight --unwind 1
cargo kani --harness job_001_up_to_eight --unwind 4
cargo kani --harness job_001_up_to_eight --unwind 9

特定Harnessの--unwindは注釈を上書きできます．--default-unwindは明示BoundのないHarnessの既定値です．実行Commandを保存しないと，Sourceの注釈だけから条件を復元できません．[3][4]

Unwinding Assertionの失敗は，指定した展開でLoopの完了を扱い切れていないことを示します．対象のAssertionが成功表示でも，他がUNDETERMINEDなら，必要なProof全体が完了したとは扱いません．展開Checkを消して緑にする方法は，その不足を解決していません．

公式Tutorialでは，単純なLoopで反復数より一つ多いBoundが必要になる例と，break／continue等では対応がもっと複雑になる場合を説明しています．「8回だから必ず9」を一般則にせず，Checkと実際のLoop構造を確認します．[3]

すべての高速化が保証を狭めるわけではありません． 一方，不完全な探索を「小さい範囲の成功」と言い換えることもできません．

5．assumeを，理由ごとに分類する

kani::assume(condition)は探索順のHintではなく，条件を満たさない経路を除外します．assume(false)の後続CheckがUNREACHABLEになることも公式FAQで説明されています．[5]

今回，次を追加した場合は明確な範囲縮小です．

// V-002: verification-only reduction; see verification/JOB-001.md.
kani::assume(len <= 4);

付属サンプルでは，元のHarnessを上書きせず，job_001_reduced_to_fourとして分けています．4件なら速かったという実測値もありません．比較候補と，元の0〜8件のObligationを残します．

ProductionがMAX_BATCH=32で本当に拒否するなら，その上限を前提にすることは可能です．ただしAPIだけでなく，Batch，内部Call，復元Dataなど，対象関数へ届く入口で成立するか確認します．HarnessのassumeはProductionのValidationを実装しません．

仕様として上限を導入する場合も，業務要件，Latency，運用上の理解可能性などを含むDecisionにします．Verifier都合の4件を，説明なくProductの上限へ昇格させません．

6．coverで空虚な成功を探す

Doneならseenという含意は，Doneに到達できなければ反例を持ちません．Pendingから2 Commandだけでは，Approve → Start → Completeという3段階を通れません．このModelではDoneへのCoverは到達不能になるとCodeから読めますが，Kaniの観測結果は未取得です．

付属のdiagnostic_two_command_vacuityは，この違いを調べるための独立Harnessです．Intentionalな到達不能Coverを，通常の「すべて成功」のGateへ混ぜません．

cover!の満足は，Model内にその条件を満たす経路があるという存在のEvidenceです．Assertionは対象経路すべてについて性質を確かめます．両者の結果を別々に保存します．DoneとFailedのCoverが満たされても，すべての業務Scenarioや入力の組合せを含むことまでは示しません．[5]

Source Coverageも補助になります．参照版ではExperimental Featureです．[6]

cargo kani \
  --coverage -Z source-coverage \
  --harness job_001_up_to_eight \
  --unwind 9

NONEのLineには，Domain上の理由があるのか，追加した前提で消したのかを確認します．逆に全LineがFULLでも，全PathやRequirementの網羅を証明したことにはなりません．特定の誤りを検出できるかは，別途，PropertyとHarnessのReviewや意図した変異に対する確認で点検します．

7．境界の分解と，Stubによる置換を区別する

Authorizationを調べようとして，DB，Parser，Network Client，Cacheまで展開しているなら，PureなPolicy判断を取り出せないか検討します．Kaniの実Code向けGuideも，I/Oの振る舞いを直接証明する対象として扱わず，Pure Computationを分離する方針を説明しています．[2]

例えば「有効なPrincipal・Policy・Actionから，不許可のAllowを返さない」をKaniへ渡し，「外部Dataを正しく取得・変換する」をIntegration Testへ分けます．Pure Coreが正しくても，古いPolicyや違うUserをAdapterが渡せば，SystemのClaimは崩れます．二つを接続する責務も記録します．

Stubは別の操作です．#[kani::stub(original, replacement)]は，対象関数を別実装へ置き換えます．参照資料では-Z stubbingを使うExperimental Featureで，通常のStubの意味が元の関数と同じだと自動証明されるわけではありません．[7]

Parserを「任意のValid Policyを返す」に変える場合，正常な戻り値は広く覆えても，Parse Errorを扱う経路を消すかもしれません．入力と戻り値の関係や副作用も失われます．過大近似なら同じSafety Claimを保てる可能性があり，過小近似なら実際の失敗を消す可能性があります． その包含関係とPropertyの種類を論じて初めて，結果を元の実装へ結び付けられます．

8．Contractと入力分割で，Claimを保ったまま小さくする

KaniのFunction Contractは，requires／ensuresを記述し，proof_for_contractでCalleeのObligationを検証し，stub_verifiedでCaller側を抽象化する仕組みです．参照版では-Z function-contractsを使います．[8]

名称にVerifiedがあっても，対応する実行Evidenceなしに「検証済み」と記録しません．ContractとCalleeのRevision，Precondition，戻り値，変更可能なState，Callerでの前提成立を一つの依存関係として保存します．Contractに書いていない性質が，自動でCallerへ引き継がれるわけではありません．

入力分割も有効です．例えば長さ0〜4，5〜8へ分け，両方で同じPropertyを確認すれば，和集合で0〜8を覆えます．0〜4だけが成功した段階では，元のObligationは完了していません．境界の抜け，整数のOff-by-one，分割ごとに違うStubを使っていないかをReviewします．[1]

今回の状態機械には，別の分解もあります．I(state, seen) = state != Done || seenというInvariantのBase Caseと，一段の保存性を分けます．

/// Separate induction obligations; see the journal's composition limits.
#[kani::proof]
fn job_001_induction_base() {
    assert!(history_invariant(JobState::Pending, false));
}

#[kani::proof]
fn job_001_induction_step() {
    let state: JobState = kani::any();
    let seen: bool = kani::any();
    let command: Command = kani::any();
    // IH-001: induction hypothesis, not a claim about arbitrary initial state.
    kani::assume(history_invariant(state, seen));
    let (next, next_seen) = step_with_history(state, seen, command);
    assert!(history_invariant(next, next_seen));
}

両方を実際に検証し，Historyの意味と遷移との対応を正当化できれば，数学的帰納法によって抽象的な遷移関係の任意の有限Traceへ議論を広げられます．現在は未実行です．

この議論だけで，任意サイズのRust Sliceを扱うWrapperのAllocation，Index，Terminationや，現実のJob Schedulerまで検証したとはいえません．帰納的なTransition Claimと，具体的なWrapperのBounded Harnessは別のObligationとして残します．

9．Loop Contractは，証明方法の変更として扱う

任意回数のLoopを展開する代わりに，InvariantでLoopを抽象化する選択肢があります．KaniのLoop ContractはExperimental Featureで，Entryで成立すること，一段後に保たれること，ExitからPostconditionが導けることを扱います．入力の表現や型の制限まで消えるわけではありません．[9]

単にprocessed <= commands.len()と書くだけでは，今回の履歴Propertyを導けません．StateとHistoryの関係もInvariantへ含める必要があります．Modified Stateの扱いも確認します．

次はJOB-001とは独立した，Countdownの説明例です．型から自明なInvariantと，進捗を表すDecreasesを分けています．Cargo Libraryには組み込まず，Standalone Sourceとして添付しています．

// Standalone experimental example, NOT part of the Cargo library.
// Pin the Kani/Rust versions and enable -Z loop-contracts before future use.
#![feature(stmt_expr_attributes)]
#![feature(proc_macro_hygiene)]

#[kani::proof]
fn countdown_contract() {
    let mut remaining: u8 = kani::any();
    #[kani::loop_invariant(remaining <= u8::MAX)]
    #[kani::loop_decreases(remaining)]
    while remaining > 0 {
        remaining -= 1;
    }
    assert_eq!(remaining, 0);
}

# 未実行．採用版のFeature・Compiler条件を確認してから実施します．
kani experimental/countdown.rs -Z loop-contracts

InvariantだけではTerminationを示しません．終了したときの性質を扱うPartial Correctnessと，終了することまで含むTotal Correctnessを区別します．到達しないLoop後のAssertionが反例を持たないことを，進捗の保証と読み替えません．

参照Commitの資料は，副作用のあるContract式を自動排除しないこと，loop_modifies推論，while let等の対応範囲，DecreasesのStruct Field，多次元式，Modifiesとの併用，Nested Loopに既知の制約があることも記載しています．採用版の制約を確認し，Contractは副作用なしで記述します．[9]

10．Timeoutと反例を，同じFAILへ潰さない

Journalでは，Toolの生出力を保持したうえで，Claim単位に次の分類を使えます．これはKani自身の出力文字列をそのまま置き換えるものではありません．

Unwinding Assertionの失敗だけでは，業務Propertyを反証したことにはなりません．逆に，実際のAssertionの反例を得たら，どの前提・Stubの下のTraceかを調べます．抽象化が作った偽反例なら，実Systemの反証と区別します．Exit Codeや一つの成功行だけで分類しません．

参照版のRust Feature SupportはConcurrencyを対象外とし，Concurrent CodeをSequentialとしてCompileする場合があると説明しています．そのHarnessでData Raceや全Interleavingを検証したとは主張できません．Inline Assembly等の未対応境界も，Stubで見えなくしたままにしません．[10]

実行Recordには，完全なCommand，Source Revisionと未Commit差分のHash，依存，Kaniと同梱Rust／CBMC，Target，Solver，Flags，Host／Containerと制限，終了理由，生Logを残します．Source CoverageやContractも版で変わるため，参照したDocumentationのCommitと，実行したBinaryは別項目です．

11．Proof BudgetとVerification Debtを管理する

30秒の手元確認，5分のPR，30分のNightlyなど，予算を分けることはできます．これらは設計例であり，このHarnessの計測値ではありません．Timeoutを適用するなら，子Processまで終了・回収し，部分Log，Signal，終了時刻を保存する仕組みが必要です．付属サンプルにそのRunnerは実装していません．

GNU/Linuxの/usr/bin/time -vとmacOSの/usr/bin/time -lは異なります．Peak RSSも親Process，子Processを含む最大値，同時のProcess Tree合計などで意味が変わります．複数値を足して実Peakと呼ばず，測定方式を記録します．

同じClaimの実行が12秒から4分へ変わったなら，SourceだけでなくToolchain，Solver，Host競合，Cache条件も比較します．新しいLoopやCall Graphが原因なら設計のFeedbackにできます．一回の遅延だけで意味を縮める判断はしません．

付属RegistryはすべてNOT_RUNで，Revision・Log・時間・Memoryはnullです．未実行なのに「Timeout」や「PROVED」を埋めません．JournalにはExact 8，0〜8，0〜4，診断用Unwind，帰納法の候補を別行で保存しています．

{
  "claim": "JOB-001",
  "result": {
    "status": "NOT_RUN",
    "reason": null,
    "source_revision": null,
    "source_patch_sha256": null,
    "toolchain": null,
    "raw_log": null,
    "wall_seconds": null,
    "peak_memory_bytes": null
  },
  "debt": {
    "id": "VD-001",
    "owner": null,
    "review_date": null,
    "remaining": "bounded_to_all_finite_trace_argument_and_execution"
  }
}

VD-001は，Boundedな0〜8件と任意有限Traceとの距離です．4件の結果が得られても，自動的に閉じません．担当者とReview期限は運用導入時に割り当て，未割当の値を作り話で埋めないようにします．

12．PRでは，結果と保証範囲の差分を一緒に見る

HarnessもSpecification Codeです．assume(action != Delete)を追加すれば，Deleteを含むClaimへのEvidenceではなくなります．kani::any()を具体値へ変える診断も同じです．原因の切り分けに使ったModelを，元のProofとして残さないようにします．

Reviewでは次を対応付けます．

• 変更前後のClaimとInput Domain，空入力・初期状態の扱い．
• 表現Bound，Unwind，Assumption，Stub／Contract，無効化したCheck．
• 必須AssertionとSafety Check，Cover Witness，未解決のObligation．
• Source・Toolchain・Flags・予算に結び付いた実行Artifact．
• Claimを分割した場合の網羅性と，残したVerification Debt．

関連する認証・認可基盤PoCは，担当範囲と設計判断の文脈です．本稿のJob Model，Harness，Tool版，Coverageや性能を，その案件で実施したEvidenceとは扱いません．Tamarinと実装の対応も，同じくModelと実Systemの距離を管理する論点です．

探索を小さくする方法には，Claimを狭める方法，同じClaimを分割する方法，完全性をまだ満たさない診断があります．それぞれを名前と記録で区別します．成功表示が残るだけでなく，何について，どの条件で成功したかを後から説明できることを，Proof Engineeringの成果にします．

参考資料

1. Debugging Slow Proofs — 遅いProofの原因，Solver変更，入力分割．
2. Using Kani on Real Code — 対象の切り出し，I/O，小さいUnwind．
3. Loop Unwinding — 展開不足，Check，Input Boundとの関係．
4. Using Kani — Harness選択とCLIの設定．
5. Frequently Asked Questions — assume(false)，到達不能，cover．
6. Source Coverage — ExperimentalなLine Coverage．
7. Stubbing — 置換の意味とExperimental Flag．
8. Function Contracts — Pre/Postcondition，Callee検証とCaller抽象化．
9. Loop Contracts — Invariant，Decreases，Side Effectと既知の制約．
10. Rust Feature Support — Concurrency，Assembly等の境界．

参照する公式資料のSourceをCommit 103dca2dfae56ad9a0dd48df83c0a4f84583abe3で照合しました．これは参照資料の版であり，サンプルをそのBinaryで実行したという意味ではありません．