コード生成の走査網羅性 (traversal/site totality)

almidecompilerverification

マルチターゲット codegen で最も危険なバグは「間違った処理」ではなく「抜けた処理」 — パスが手書き再帰で match expr.kind { … _ => {} } と書くと、明示していないノード種が _ に落ちて黙って素通りする。片方のターゲットだけが処理し他方が取りこぼせば、出力が silent に乖離する。これを走査の網羅性 (traversal/site totality) として静的に保証すべき、という原則。

なぜ silent な乖離になるか

単一ターゲットなら「最適化漏れ」で済むことが、native(Rust 経由)と WASM の2系統では「出力が食い違うが、どちらもビルドは通る」になる。しかも特定の config — Linux + release + wasm 強制 — でしか踏まないパスに潜むと、ローカルでは再現せず、その CI 枠だけが落ちる(あるいは誰も気づかない)。

flowchart TB
    add["新しいノード種を追加"] --> nat["native 走査: 処理した"]
    add --> wasm["wasm 走査: _ => {} に落ちた"]
    nat --> on["native 出力: 正"]
    wasm --> ow["wasm 出力: 取りこぼし"]
    on --> div{"両方ビルド通過<br/>出力だけ食い違う"}
    ow --> div
    div --> hidden["Linux+release+wasm<br/>でしか踏まない silent バグ"]

単発ではなくクラス

今日の2件は同じ形 — 「走査が忘れたノード種」:

バグ取りこぼした所
map_foreach の Swiss-table 取り残し反復ノードの後始末サイト
variant の identity-hashバリアント payload のハッシュサイト

そして anf-closure-lifting-bug も同型(ANF パスが __closure_* 関数を走査していなかった)。→ 個別修正では尽きない。「走査が漏れる」という構造そのものが源流。

Almide での規模

効くのは discipline ではなく静的保証

「新しいノード種を足したら 24 パス全部に手で追加する」運用はスケールせず、失敗が silent。構造で潰す:

手段仕組み効果
catch-all を禁じた網羅 match_ => {} を消す新バリアント追加が型エラーになり、全サイトを潰すまでビルドが通らない
catamorphism / 汎用走査畳み込みが構造的に全ノードを訪れるper-node の代数だけ書けば totality は fold が担保
仕組みの位置づけ「取りこぼし」を表現不能にする を走査に適用漏れが「書ける状態」として存在しなくなる

兄弟は Determinism/Purity Belt — どちらも「忘れるな/使うな」という規律を機械的な CI ゲートに変換する発想。

→ なぜ最高レバレッジか: sweep や 差分ゲートは乖離を事後に捕まえる。totality を静的にするとクラスごと構造的に消える — 一番捕まえにくい「特定 config でしか出ない silent バグ」を源流で断つ。

cross-target 等価性の残ギャップ

totality(#1)を筆頭に、native↔WASM で残る既知の乖離:

#ギャップ中身直し方
1traversal/site totality~24/37 パスの手書き再帰。源流クラス取りこぼしをコンパイルエラー/CI fail に
2float.to_stringwasm が固定精度、native は [ryu|Ryu]。同じ float が 0.3 vs 0.30000000000000004 に。唯一の tracked な数値乖離wasm ランタイムに Ryu 移植
3fan. の意味論race/any/timeout/map-err が cross-target で乖離(ビルドは通る)仕様を固定し両ターゲットで一致させる
4closure completenesswasm-remaining(意図的 skip 8件)残りを実装し skip を解消
5ゲートのカバレッジ穴wasm_cross_target_spec は spec/wasm_cross/ の手選びファイルしか byte 比較しない。今日の variant バグは hash_protocol_test が wasm_cross に無く素通り、Test WASM だけが捕捉ゲートを全 spec に広げる

#1 と #5 は同じ「カバレッジ穴」が2層に出たもの — #1 はコンパイラ自身の走査の穴、#5 はテストゲートのファイル選定の穴。どちらも問いは「本当に全部訪れたか?」。

押さえどころ（カード化候補）

関連

Graph

Backlinks