ゲストプログラム

zkVM 内のゲストは、入力検証から集計、ビットマップ計算までを実行します。

ゲストプログラムは、投票コミットメントの再計算、RFC 6962 包含証明の検証、集計の実行、ビットマップルートの計算を行い、結果をジャーナルにコミットします。

契約上重要なヘルパー（コミットメント計算、正準エンコーディング、RFC 6962 包含証明、ビットマップルートなど）は zkvm/contract-core/ に集約されており、ゲストとホストが同じ実装を参照します。

概要

ゲストプログラムは RISC Zero zkVM 上で動作する Rust プログラムです。 現行の guest crate は #![no_std] で構築され、risc0-zkvm の default features を無効化した上で heap-embedded-alloc を使用します。 ホストから投票データ（選択肢、乱数、コミットメント、Merkle パスと選挙メタデータ）を受け取り、以下の処理を行います:

1. 各投票の正当性検証（コミットメント再計算 + 包含証明）
2. 有効投票の集計
3. カウント状態と提示状態のビットマップ計算
4. 入力コミットメントと STH ダイジェストの計算
5. 結果のジャーナルへのコミット

ゲスト内の処理はすべて STARK 証明に含まれるため、出力（ジャーナル）の正しさはゲストロジックに対して暗号学的に保証されます。

入力構造

ゲストプログラムが受け取る入力（AggregatorInput）の構造を示します。

各 VoteWithProof は以下のフィールドを持ちます。

処理パイプライン

ゲストプログラムの処理は、入力検証、投票検証と集計、出力構築の 3 フェーズで構成されます。

flowchart TD
  subgraph "フェーズ 1: 入力検証"
    I1[入力デシリアライズ] --> I2{掲示板ルート<br/>が非ゼロ?}
    I2 -->|Yes| I3{ツリーサイズ<br/>が正の値?}
    I2 -->|No| FAIL[不正入力]
    I3 -->|Yes| I4{タイムスタンプ<br/>が正の値?}
    I3 -->|No| FAIL
    I4 -->|Yes| I5{guest 境界と<br/>Merkle パス長が有効?}
    I4 -->|No| FAIL
    I5 -->|Yes| NEXT[フェーズ 2 へ]
    I5 -->|No| FAIL
  end

  subgraph "フェーズ 2: 投票検証と集計"
    NEXT --> LOOP[各投票に対して]
    LOOP --> V1[6 段階検証]
    V1 -->|有効| TALLY[集計に加算]
    V1 -->|無効| EXCL[却下カウントと<br/>スロット統計に反映]
    TALLY --> BIT[ビットマップ更新]
  end

  subgraph "フェーズ 3: 出力構築"
    LOOP -->|全投票完了| O1[ビットマップルート計算]
    O1 --> O2[入力コミットメント計算]
    O2 --> O3[STH ダイジェスト計算]
    O3 --> O4[ジャーナルにコミット]
  end

入力の境界条件

次のいずれかに該当する入力は、ジャーナル生成前に fail-closed で拒否されます。

• bulletin_root がゼロ
• tree_size が 0
• timestamp が 0
• tree_size > 1,000,000
• total_expected > 1,000,000
• votes.length > 1,000,000
• 候補別 tally bucket が 1,000,000 を超える
• Merkle パス長が u16::MAX を超える
• Merkle パスノード総数が 1,000,000 を超える
• 推定構造化入力サイズが 64 MiB を超える

votes.length > tree_size のような入力は、上記境界内であれば事前 reject されません。 重複や範囲外は record 単位で rejectedRecords に反映されます。

投票の 6 段階検証

各投票に対して、以下の 6 つの検証が順に実行されます。 いずれかが失敗した投票は即座に「無効」として除外され、以降の検証はスキップされます。

各検証の失敗条件と、失敗したレコードがどのカウンタに反映されるかを示します。

#3〜#6 で無効化された範囲内かつ初出のスロットは invalidPresentedSlots として観測され、#1〜#2 の却下は rejectedRecords のみに反映されます。 ビットマップへの反映を含む各カウンタの意味論は スロット / レコード分離モデル を正とします。

コミットメント再計算と照合（#4）

ゲスト内で投票者の（選択肢, 乱数, 選挙 ID）からコミットメントを再計算し、入力として渡された値と照合します。 これにより、投票者が主張する選択肢が掲示板上のコミットメントと一致することが保証されます。 計算規則は コミットメントスキーム を参照してください。

RFC 6962 包含証明検証（#6）

投票のコミットメントが掲示板 Merkle ツリーに含まれることを、RFC 6962 PATH 関数ベースの CT スタイル包含証明で検証します。 投票のインデックスと Merkle パスから掲示板ルートを再計算し、入力の bulletin_root と一致するかを確認します。 リーフとノードハッシュの規則とドメインタグは CT Merkle ツリー を参照してください。

集計ロジック

6 段階検証をすべて通過した投票は「有効」として集計に加算されます。 集計は選択肢ごとの配列（5 要素）で管理し、有効投票のインデックスに対応する includedBitmap のビットを true に設定します。 無効票の seenBitmap / includedBitmap への反映は スロット / レコード分離モデル を参照してください。

スロット / レコード分離モデル

現行のゲストプログラムは、掲示板スロットに対する完全性と入力レコードの異常を別々に記録します。

flowchart LR
  TS["ツリーサイズ<br/>(全スロット)"]
  TS --> CNT["カウント済み<br/>validVotes"]
  TS --> INV["提示されたが未計上<br/>invalidPresentedSlots"]
  TS --> MIS["未提示<br/>missingSlots"]
  REC["入力レコード"] --> REJ["却下レコード<br/>rejectedRecords"]

スロット単位の 3 分類は、現行実装では常に次の関係を満たします:

validVotes + invalidPresentedSlots + missingSlots = treeSize

fail-closed 判定に使われる除外数は、スロット単位の excludedSlots です:

excludedSlots = missingSlots + invalidPresentedSlots

excludedSlots > 0 は検証失敗の決定的な指標です。 1 スロットでも未提示または未計上であれば、集計結果の完全性が損なわれていることを意味します。

一方で rejectedRecords はレコード単位の補助指標です。 たとえば次のようなケースでは rejectedRecords は増えても excludedSlots は増えません。

• 既に正しくカウント済みのスロットに対する重複インデックスレコード
• tree_size の外側を指す範囲外レコード

旧 public contract の互換名は現行 journal にも公開レスポンスにも現れません。 参考までに 1 対 1 対応を示します。

※ rejectedRecords は record 単位の新設カウントで、旧 invalidIndices の mirror は invalidPresentedSlots 側。

ジャーナル出力

ゲストプログラムがジャーナルにコミットする出力構造（VerificationOutput）を示します。

ジャーナルの信頼モデル

ジャーナルの各フィールドは、対応する STARK 証明により「ゲストプログラムが正しく計算した結果」であることが保証されます。

一方、STARK 証明だけでは保証されないものがあります。 「ゲストに提示されなかった票」「第三者 STH との合意」「ホストやサーバーの正直性」はジャーナル外の独立チェックで確認します。 第三者はレシートの STARK 検証を行うだけで上記の保証を取得でき、ゲストロジックの信頼以外にホストやサーバーを信頼する必要はありません。

ビットマップルートの計算

ゲストプログラムは投票検証と並行して、seenBitmap（範囲内かつ初出として提示されたインデックス集合）と includedBitmap（6 段階検証を通過したインデックス集合）の 2 種類を構築します。 また、それぞれの Merkle ルートをジャーナルにコミットします。 この 2 つのルートを併用することで、公開検証側は「prover に提示されたが無効化された票」と「そもそも提示されなかった票」を区別できます。

LSB-first のバイト列パッキング、32 バイト境界による単一リーフ / 分割リーフの扱い、leaf / node hash 規則は ビットマップ Merkle を参照してください。

入力コミットメントと STH ダイジェスト

ゲストプログラムは投票処理の後、2 つの追加ハッシュ値を計算してジャーナルにコミットします。

入力コミットメント

ゲストに渡された入力のうち、公開フィールドを正準エンコーディングで連結し SHA-256 で圧縮します。 現行実装では固定のドメインタグと format version を先頭に付与した上で、electionId、bulletinRoot、treeSize、totalExpected、votesCount と各投票の index、コミットメント値、Merkle パスを束縛します。 投票列はハッシュ前に index 昇順で正規化されます（異常入力時の tie-break 補助ルールは 入力コミットメント > ソート規則 を参照）。

第三者は public-input.json などの公開検証用レコードから同じ値を再計算し、ジャーナルの値と照合することで、zkVM が処理した入力の同一性を検証できます。

詳細は 入力コミットメント を参照してください。

STH ダイジェスト

掲示板のログ ID、ツリーサイズ、タイムスタンプ、ルートハッシュを結合して SHA-256 で圧縮します。 このダイジェストは第三者の STH ソースとの照合に使用され、サーバーが異なる投票者に異なる掲示板ビューを提示するスプリットビュー攻撃を緩和します。

詳細は STH ダイジェスト を参照してください。

ゲストプログラムのバージョニング

ゲストプログラムにはバージョン番号が割り当てられ、ジャーナルの methodVersion フィールドに記録されます。 現行のジャーナル契約は 14 です。

バージョン番号は Image ID の管理と連動しており、ゲストプログラムの変更は新しい Image ID の生成を伴います。 検証時には、期待 Image ID との一致が確認されます。

ゲストの抽象 tally / rejection model と guest bounds は、Lean による形式化 で説明しています。 Rust 側の guest-vector tests は、抽象モデルと実装の対応付けを検査します。