はじめに

最終更新: 2026-08-10

このドキュメントは、STARK Ballot Simulator の公開向けガイドです。 STARK Ballot Simulator は投票の完全性を段階的に検証する教育・ポートフォリオ向けの PoC であり、実運用の選挙基盤ではありません。

目的

• システムの全体像を短時間で把握できるようにする
• 暗号プロトコルと検証パイプラインの設計根拠を説明する
• 検証手順を再現できる情報を提供する

公開状態

本書は、ライブデモと公開用ソース snapshot の読者に向けたドキュメントです。 公開 repository snapshot は hwatanabe-jp/stark-ballot-simulator-public で確認できます。

再現手順は、対象リリースの bundle.zip と対応する公開 repository snapshot を照合して実行してください。 必要な材料と bundle.zip 単体では揃わない証拠は 第三者検証ガイド にまとめています。

公開仕様は、runtime、検証、artifact の 3 つの境界を説明します。 これらは利用者、監査者、実装追跡者が確認できる範囲です。 内部の作業記録や運用証跡は本書の範囲外であり、完了状態として主張しません。

想定読者

• 暗号検証や監査、本アプリケーションの設計に関心のある技術者

本書の用語表記

本書では、語彙の揺れを避けるために次の表記へ統一します。 詳細な定義は 用語集 を参照してください。

• 日本語に統一する語：コミットメント（文脈に応じて「投票コミットメント」「入力コミットメント」を区別）、包含証明、整合性証明、投票レシート、掲示板、ジャーナル
• 英語のまま使う語：STARK、zkVM、Image ID、RFC 6962、capability、bundle.zip、fail-closed、finalization（集計確定）
• 識別子は原文のまま：ファイル名、API フィールド、契約名（journal.json、verificationStatus など）はコードフォントの英語表記を保ちます。
• コンポーネント名：概念としては「検証サービス」、バイナリ名・パスとしては verifier-service を使います。
• 役割名とリソース名：概念・役割としては「プローバー」「検証 worker」、リソース・コンポーネント固有名（prover semaphore、proof-dispatcher、verification-worker など）は原文の英語表記を保ちます。

バンドル関連は、次の 3 語を使い分けます。

verification.json は protected report artifact であり、public bundle.zip のメンバーではありません。 階層関係は バンドル構造 と 公開境界 を参照してください。

本書の読み方

標準ルート

1. まず 全体像 でシステムの概要を掴む
2. 利用フロー で Home から Verify までの画面と API の流れを確認する
3. 暗号プロトコル でコミットメントや Merkle ツリーなどの基盤を理解する
4. zkVM 設計 でゲストプログラムと証明生成の仕組みを学ぶ
5. 検証パイプライン で 4 段階検証モデルの全体と公開境界を把握する
6. 改ざんシナリオ で教育的シミュレーションの動作を確認する
7. 品質保証と形式手法 でテスト、PBT、Lean による品質境界を確認する
8. AWS アーキテクチャ で runtime の責務分担を理解する
9. API リファレンス でエンドポイント仕様を参照する
10. 実際に検証する場合は 第三者検証ガイド で bundle.zip を使ったローカル検証手順を実行する

PoC として受け入れている制約は 全体像、 設計背景の一次資料は 参考文献 から参照してください。

読者別ルート

いずれも標準ルートの 1〜2（全体像、利用フロー）を読み終えていることを前提に、そこから先の重点だけを示します。

監査者向け

bundle.zip を検証ページから取得し、独立にローカル監査したい読者向けです。

1. 検証パイプライン で /verify の最終判定ロジックを理解する
2. 公開境界 で public bundle.zip と protected report artifact（verification.json）の境界を確認する
3. チェック一覧 で各チェック ID と判定条件を確認する
4. 第三者検証ガイド で bundle.zip のローカル監査手順を実行する

用語集 を手元に置き、テストと形式化が守る境界は 品質保証と形式手法 で補足してください。 飛ばしてよい: 暗号プロトコル の数式詳細、AWS アーキテクチャ のインフラ詳細

実装者向け

クライアント、サーバー、zkVM のいずれかの実装を変更または追従したい読者向けです。

1. 暗号プロトコル でコミットメント、Merkle、入力コミットメントの正準形を把握する
2. zkVM 設計 でゲストとホストの責務分担と Image ID 管理を理解する
3. 検証パイプライン でチェック評価、ゲーティング、公開境界を把握する
4. API リファレンス でエンドポイント仕様と session-scoped 認可を確認する

テストのレイヤー分担は 品質保証と形式手法 を参照してください。 飛ばしてよい: 第三者検証ガイド（実装変更後の動作確認には 改ざんシナリオ を使う方が早い）

運用者向け

AWS インフラ、非同期プローバー、デプロイを担当する読者向けです。

1. AWS runtime 境界 で frontend、API、DynamoDB、async prover、artifact delivery の責務分担を把握する
2. AWS アーキテクチャ で runtime 構成、環境分離、Terraform-managed infrastructure の連携点を把握する
3. 非同期プローバー で SQS、Step Functions、ECS の責務を理解する
4. 可観測性設計 で構造化ログ、検出、相関、通知境界を確認する
5. イメージ署名 と Image ID で署名検証と Image ID 解決の連動を確認する
6. 公開境界 と バンドル構造 で artifact の公開 / 保護境界を把握する

観測対象となるエンドポイントの契約は API リファレンス を参照してください。 飛ばしてよい: 暗号プロトコル の数式、改ざんシナリオ の教育的デモ詳細

全体像

STARK Ballot Simulator は、投票の完全性を段階的に検証するための PoC です。 AWS runtime は個人プロジェクトとして運用できるよう、WAF を採用せず、artifact lifecycle やオンデマンド実行を前提にコストを抑える設計です。

flowchart LR
  A[Cast-as-Intended] --> B[Recorded-as-Cast]
  B --> C[Counted-as-Recorded]
  C --> D[STARK Verification]

投票から検証までの流れ

sequenceDiagram
  participant V as 投票者
  participant S as サーバー
  participant B as 掲示板
  participant Z as zkVM
  participant VS as 検証サービス

  V->>S: 投票意図（選択肢・乱数）+ コミットメント
  S->>B: 掲示板に追記
  S-->>V: 投票レシート
  Note over S: ボット投票を自動追加
  V->>S: POST /api/sessions/:sessionId/finalizations で finalization を要求
  S->>Z: 同期または SQS / Step Functions / ECS 経由で証明生成
  Z-->>S: STARK レシート + ジャーナル
  S-->>V: /result で tally と finalization output を表示
  V->>S: POST /api/sessions/:sessionId/finalizations/:finalizationId/verification
  alt local profile
    S->>VS: local bundle の verifier-service を同期実行
  else target AWS profile
    S->>VS: durable SQS queue 経由で verification worker を実行
  end
  VS-->>S: receipt を検証し protected report artifact を保存
  V->>S: /verify が同じ finalization-scoped verification GET をポーリング
  S-->>V: 段階別チェックと overall verdict を表示

図から読み取れない要点は次の 3 点です。

• finalization と STARK receipt verification は別の lifecycle です。finalization は集計結果、zkVM ジャーナル、STARK レシート、配布用バンドルを作る段階であり、STARK receipt verification が常に同時に完了するわけではありません。
• 実行形態は profile で分かれます。ローカル構成は finalization と verifier-service を同期実行できますが、AWS target runtime は finalization を SQS、Step Functions、ECS Fargate で非同期実行し、STARK receipt verification は durable SQS queue 経由の verification worker が担います。非同期のあいだ、ブラウザは GET /api/sessions/:sessionId/finalizations/current と finalization-scoped verification GET をポーリングします。
• verification POST 応答の verificationStatus と、available な verification GET resource の verifierResult.status は STARK receipt verification の状態であり、どちらも overall verdict ではありません。ブラウザはローカルの Cast-as-Intended 証拠を server checks に重ね、共有 presentation policy が 4 段階の必須チェックと hard-failure 条件を評価して、最終的な「Verified / 失敗 / 制限付き」などの表示を導きます。

検証で扱う要素

各段階の目的、必要な証拠、失敗モードは 4 段階検証モデル を参照してください。

バンドル用語の階層

検証で扱うアーティファクト群は、証明バンドル ⊃ 配布対象アーカイブ ⊃ bundle.zip（ファイル） の 3 層で呼び分けます。 定義は 用語集 > 証明バンドル、詳細は バンドル構造 を参照してください。 verification.json は bundle.zip のメンバーではなく、capability 保護された report artifact として扱います。

PoC として受け入れている制約

次の制約は、検証可能投票の E2E フローを明瞭に示すための意図的な PoC スコープです。実装漏れでも、本番選挙システムとしての安全性・性能の主張でも ありません。正確な定数や mode 条件は各技術章を単一の参照先とします。

プロジェクト規模

コードベースの規模は、テストを含め約 33 万行です。内訳は次のとおりです（2026 年 8 月時点）。

各章への案内

利用フロー

このページは、ブラウザでの通常利用順と、その裏で使われる API を一続きで示します。 検証モデルや zkVM の詳細に入る前に、どの画面で何が作られ、どの時点で何を検証するのかを把握するための入口です。

画面と API の対応

正確な path、request/response schema、公開エラーは エンドポイント一覧 を参照してください。

POST /api/sessions を除く session-scoped API は、path の :sessionId と X-Session-Capability ヘッダーだけで現在の session を特定して保護します。 finalization、verification、bundle / report の resource は path の :finalizationId にも結び付けられ、session capability と一致した場合だけ返されます。 ヘッダー要件の詳細は エンドポイント一覧 > 共通 contract を参照してください。

1. Home

Home で開始すると、ブラウザは POST /api/sessions を送ります。 サーバーは sessionId、capabilityToken、electionId、electionConfigHash、logId などを返し、ブラウザはそれらをローカル session state に保存して Vote へ進みます。

この session が以後の API 呼び出しの権限境界です。 別タブや古い session が現在の session と食い違う場合、後続画面は fail-closed に扱います。

2. Vote と bot progress

Vote では、ブラウザが投票選択と乱数からコミットメントを作り、POST /api/sessions/:sessionId/votes に送信します。 成功すると、投票者は voteId、bulletinIndex、bulletinRootAtCast を含む投票レシートを受け取ります。

その後、デモ用のボット投票が進むあいだ GET /api/sessions/:sessionId/progress をポーリングします。 これは最終的な集計に十分な投票が揃うまでの進捗表示であり、検証の成功判定ではありません。

3. Aggregate と async status

Aggregate では、ユーザーが通常シナリオまたは教育用 tamper scenario を選び、POST /api/sessions/:sessionId/finalizations を送ります。 この段階で、集計結果、zkVM の公開出力、receipt、bundle.zip 用の公開可能アーティファクトなどが作られます。

finalization 作成要求は同期結果を返す場合も、202 Accepted で非同期 queue に入る場合もあります。 非同期の場合、ブラウザは GET /api/sessions/:sessionId/finalizations/current をポーリングします。 current finalization resource は pending、running、succeeded、failed、timeout のいずれかであり（status ごとのフィールドは エンドポイント一覧 > Finalization resource）、ブラウザは succeeded の result だけを Result へ引き継ぎ、failed と timeout は失敗として扱います。

finalization と STARK receipt verification は同一ではありません。 finalization は proof material と結果を作る段階ですが、STARK verification が常にこの時点で完了しているとは限りません。

4. Result から Verify へ

Result は current finalization resource の succeeded result から、tally、scenario、journal / receipt 由来の表示材料などを表示します。 finalization response のアーティファクト情報は available / unavailable の bounded availability であり、raw locator やダウンロード URL ではありません。

ユーザーが検証へ進むと、ブラウザは STARK verification が未開始なら POST /api/sessions/:sessionId/finalizations/:finalizationId/verification を送ってから /verify へ遷移します。 この要求は terminal status まで待たず、/verify 側で同じ finalization-scoped resource を GET でポーリングしながら状態を解決します。

verification POST 応答の verificationStatus と、available な verification GET resource の verifierResult.status は STARK receipt verification の状態を示す信号であり、Cast-as-Intended、 Recorded-as-Cast、Counted-as-Recorded を含む overall verdict そのものではありません。 UI が “Verified” を表示できるかは、全 required checks の評価と hard-failure 条件から別途導かれます。

5. Verify

Verify は GET /api/sessions/:sessionId/finalizations/:finalizationId/verification で検証ペイロードを取得します。 resource は available、unavailable、corrupt を明示します。available の場合は proofAuthority、presentation、verifierResult、verification.checks / verification.steps、 voterEvidence、journal の included / omitted discriminator を返します。投票レシートと自票 proof は voterEvidence.availability = "available" の場合だけ存在し、それ以外は理由を伴って unavailable になります。

STARK verification が not_run の場合、Verify は同じ finalization-scoped verification resource への POST を一度起動します。not_run または running の間は、terminal status に到達するまで GET をポーリングします。 その後、4 段階のチェック結果から最終表示を解決します。 required check が未実行、実行中、失敗、または hard-failure に該当する場合、成功した overall verification にはなりません。

server-validated な検証シーケンスが terminal status まで完了すると、ブラウザは POST /api/sessions/:sessionId/finalizations/:finalizationId/verification/observations で Cast-as-Intended の観測結果を best-effort に記録します。 これは telemetry であり、送信の成否が画面の verdict を変更することはありません。

検証の詳しい評価順序は 検証パイプライン と ゲーティングロジック を参照してください。

6. Bundle と report

検証画面から取得できる bundle.zip は、秘密を含まない公開可能アーティファクトだけを含む監査用 ZIP です。 一方、verification.json は検証サービスの protected report artifact であり、bundle.zip のメンバーではありません。

ブラウザは、検証レスポンスで admit した finalizationId と現在の session identity から authenticated artifact URL を組み立てます。 通常の取得経路はどちらも capability 保護 API であり、レスポンス内の raw locator をたどる方式ではありません。

ここでいう public は「秘密を含まず第三者検証に使える」という機密性の分類であり、無認証公開を意味しません。 ファイル構成と除外対象は 公開境界 と バンドル構造 を参照してください。

Receipt と proof mode の読み分け

ローカル UI 開発では local-demo の mock zkVM、実装連携確認では local-proof-development の development receipt、本番相当の検証では local-proof-production または target runtime の production STARK proof を使います。 mock や dev-mode receipt はデモや開発速度のための経路であり、production STARK proof と同じ保証を持ちません。

このページでは利用順だけを扱います。 receipt の意味、Image ID、dev-mode の fail-closed ルールは zkVM 設計 と 4 段階検証モデル を参照してください。

暗号プロトコル

この部は、投票の検証可能性を支える暗号プリミティブを説明します。

公開データに対する投票の秘匿性（hiding）と束縛性（binding）は、コミットメントスキームで扱います。 追記専用の掲示板は、RFC 6962 に基づく CT スタイルの Merkle ツリーで扱います。 zkVM 入力のうち対象となる公開フィールドの束縛は、正準エンコーディングと入力コミットメントで扱います。

本書で「コミットメント」は、投票コミットメント（個々の投票の束縛）と 入力コミットメント（zkVM 公開入力のうち正準エンコーディング対象フィールドの束縛）の 2 種を指します。 両者は対象とドメイン分離タグが異なるため、それぞれ独立した章で説明します。

プロトコル章の構成

• コミットメントスキーム：投票コミットメントの構成と安全性
• CT Merkle ツリー：CT スタイルの追記専用掲示板
• 入力コミットメント：zkVM 公開入力の対象フィールドに対するコミットメントの正準エンコーディング
• STH ダイジェスト：スプリットビュー緩和のためのツリーヘッドダイジェスト
• ビットマップ Merkle：投票カウント証明のためのビットマップツリー

想定読者と前提

• 想定読者：暗号プリミティブの仕様を実装または監査する技術者
• 前提：SHA-256 ハッシュ計算と Merkle ツリーの基本概念を把握していること

扱わない範囲

• SHA-256 や Pedersen コミットメントなど暗号プリミティブの数学的安全性証明
• RFC 6962 / CT エコシステムの運用詳細（証明書ログ、Monitor 役割など）
• 暗号ライブラリ実装の詳細（定数時間実装、サイドチャネル対策）

関連する章

• zkVM 設計：このプロトコルが zkVM 入力としてどう使われるか
• 検証パイプライン：このプロトコルに対応する検証チェック
• 用語集：暗号プリミティブの用語定義

コミットメントスキーム

この章では、投票者の選択を公開データから隠しつつ、後から変更できないようにするコミットメントスキームを説明します。

本システムの投票コミットメントは SHA-256 を使い、投票内容に対する hiding（秘匿性）と binding（束縛性）を支えます。 ドメイン分離タグは、他のハッシュ用途との入力解釈の混同を避けるために使います。

概要

投票コミットメントは、投票者が選んだ選択肢を公開データから隠したまま、その選択に束縛されることを可能にする暗号プリミティブです。 掲示板に記録されるのはコミットメント値のみです。 選択肢と乱数（opening）は、掲示板や bundle.zip 内の public-input.json などの公開配布物には現れません。 投票者は Cast-as-Intended 検証のために opening をローカルに保持します。

flowchart LR
  subgraph 入力
    E[選挙 ID<br/>16 バイト UUID]
    C[選択肢<br/>1 バイト]
    R[乱数<br/>32 バイト]
  end
  E --> H[SHA-256]
  C --> H
  R --> H
  T["ドメインタグ<br/>&quot;stark-ballot:commit|v1.0&quot;"] --> H
  H --> CM[コミットメント<br/>32 バイト]

コミットメントの正準フォーマット

コミットメント値は、次の入力を連結して SHA-256 に渡すことで生成されます。

commitment = SHA-256(
    domain_tag  ||   ← "stark-ballot:commit|v1.0" (24 バイト, UTF-8)
    election_id ||   ← UUID v4 のバイナリ表現 (16 バイト)
    choice      ||   ← 選択肢の値 (1 バイト, 0〜4)
    random           ← 一様乱数 (32 バイト)
)

各フィールドの仕様

SHA-256 への入力は合計 73 バイト、出力は 32 バイト（16 進数表記で 64 文字、0x プレフィックス付きでは 66 文字）です。

ドメイン分離

ドメインタグ "stark-ballot:commit|v1.0" は、このコミットメントを他のハッシュ用途から分離するための仕組みです。

本システムの主要なハッシュ用途では、用途ごとに次のドメインタグまたは構造的プレフィックスを使います。 これにより、ハッシュ入力の意味を分離します。

STH ダイジェストは専用のドメインタグを持ちません。 ログ ID を含む正準フォーマットで束縛されます（STH ダイジェスト を参照）。

安全性

Hiding（秘匿性）

乱数フィールドが 32 バイト（256 ビット）のエントロピーを持つため、公開されたコミットメント値から選択肢を推測することは計算量的に不可能です。

前提条件:

• 乱数は暗号学的に安全な乱数生成器（CSPRNG）から生成される
• 同じ乱数は決して再利用しない（再利用すると、同じ選択肢で同じコミットメント値が現れて情報が漏えいする）

PoC の制約: 本 PoC は operator に対する完全な秘匿性を目的としていません。 投票 API に送信された opening（選択肢と乱数）はサーバー側ストアに保持されうるため、ここでいう hiding は公開観測者と公開配布物に対する性質を指します。

Binding（束縛性）

SHA-256 の原像耐性（preimage resistance）と第二原像耐性（second-preimage resistance）により、一度コミットした値と異なる選択肢に対して同じコミットメント値を生成することは計算量的に不可能です。

つまり、投票者はコミットメント公開後に「別の選択肢に投票した」と主張を変えることができません。

TypeScript と Rust の実装同期

コミットメントは、TypeScript（クライアントとサーバー）と Rust 実装（zkVM guest/host から共有される zkvm/contract-core）の双方で計算されます。 この 2 系統の実装は、バイトレベルで完全に同一の出力を生成する必要があります。

同期が必要な要素:

• ドメインタグの文字列とエンコーディング（UTF-8）
• UUID からバイト列への変換規則（ハイフン除去 → 16 進数デコード）
• 選択肢の整数エンコーディング（1 バイト、符号なし）
• 乱数の 16 進数デコード規則

ドメインタグやエンコーディング規則を変更する場合は、TypeScript と Rust の両実装を同時に更新する必要があります。 どちらか一方のみの変更は、コミットメント照合の失敗を引き起こします。

検証パイプラインにおける役割

コミットメントは、4 段階検証モデルの最初の 3 段階で使われます。

注意: Cast-as-Intended と Counted-as-Recorded は同じコミットメント計算式を使いますが、opening の出所が異なります（投票者ローカル / prover に渡された値）。

Recorded-as-Cast は、投票時点（cast-time）のツリー状態に対する包含証明を使います。 この包含証明を、レシートの bulletinRootAtCast と整合させます。 rootAtCast の保存と再導出の詳細は CT Merkle ツリー を参照してください。

各チェックの判定ロジックは チェック一覧 > Cast-as-Intended を参照してください。

sequenceDiagram
    participant V as 投票者
    participant S as サーバー
    participant B as 掲示板
    participant Z as zkVM

    V->>V: (選択肢, 乱数) を選び<br/>コミットメントを計算
    V->>S: コミットメント, 選択肢, 乱数を送信
    S->>S: opening から<br/>コミットメントを再計算して照合
    S->>B: コミットメントを掲示板に追記
    S-->>V: 投票レシート（インデックス,<br/>bulletinRootAtCast）
    Note over V: ローカルに (選択肢, 乱数) を保存
    Note over Z: ゲストプログラムが<br/>コミットメントを再計算し<br/>掲示板の値と照合

CT Merkle ツリー

この章は、RFC 6962 を参照した追記専用 Merkle ツリーによって、掲示板の透明性をどう作るかを説明します。

リーフハッシュ（0x00 プレフィックス）とノードハッシュ（0x01 プレフィックス）の区別により、second-preimage 攻撃を防止します。 包含証明と整合性証明により、投票の記録と掲示板の追記専用性を検証可能にします。

なぜ RFC 6962 CT スタイルか

• 整合性証明で追記専用性を示せるため、Recorded-as-Cast に必要な「後から削除や改変がされていない」保証を与えられる。
• 包含証明と整合性証明の両方を同一モデルで扱える。
• STH ダイジェストと組み合わせてスプリットビュー攻撃の検出力を上げられる。

概要

本システムの掲示板（Bulletin Board）は、Certificate Transparency (CT) で実績のある追記専用ログの設計を投票に応用しています。 各投票コミットメントは Merkle ツリーのリーフとして追記され、一度記録されたエントリは削除や改変ができません。

graph TD
  subgraph "8 リーフのツリー（N=8）"
    R["ルート<br/>SHA-256(0x01 || L || R)"]
    N1["ノード"]
    N2["ノード"]
    N3["ノード"]
    N4["ノード"]
    N5["ノード"]
    N6["ノード"]
    L0["リーフ 0"]
    L1["リーフ 1"]
    L2["リーフ 2"]
    L3["リーフ 3"]
    L4["リーフ 4"]
    L5["リーフ 5"]
    L6["リーフ 6"]
    L7["リーフ 7"]

    R --> N1
    R --> N2
    N1 --> N3
    N1 --> N4
    N2 --> N5
    N2 --> N6
    N3 --> L0
    N3 --> L1
    N4 --> L2
    N4 --> L3
    N5 --> L4
    N5 --> L5
    N6 --> L6
    N6 --> L7
  end

RFC 6962 参照ハッシュ規則

RFC 6962 Section 2 に従い、リーフノードと内部ノードに異なるドメイン分離プレフィックスを適用します。

リーフハッシュ

LeafHash = SHA-256(0x00 || "stark-ballot:leaf|v1" || leaf_data)

内部ノードハッシュ

NodeHash = SHA-256(0x01 || left_hash || right_hash)

ドメイン分離の安全性

0x00（リーフ）と 0x01（内部ノード）のプレフィックス区別は、second-preimage 攻撃を防止するために必要です。 この区別がなければ、攻撃者はリーフノードを内部ノードとして解釈させる（またはその逆の）偽造データを構築できる可能性があります。

使用タグ "stark-ballot:leaf|v1" は、他システムのリーフハッシュとの偶発的な衝突を防止する追加の防御層です。

Merkle Tree Hash（MTH）アルゴリズム

RFC 6962 で定義される MTH アルゴリズムは、任意のサイズのデータセットからルートハッシュを計算します。

アルゴリズムの定義

1. 空のツリー: MTH({}) = SHA-256() （空入力のハッシュ）
2. 単一リーフ: MTH({d₀}) = LeafHash(d₀)
3. 複数リーフ: サイズ n のツリーに対し、k を n 未満の最大の 2 のべき乗とする

MTH({d₀, ..., dₙ₋₁}) = SHA-256(0x01 || MTH({d₀, ..., dₖ₋₁}) || MTH({dₖ, ..., dₙ₋₁}))

非 2 のべき乗サイズへの対応

ツリーサイズが 2 のべき乗でない場合（例: 5, 6, 7 リーフ）、MTH アルゴリズムは「n 未満の最大の 2 のべき乗」で分割を行います。 これにより、左部分木は常に完全二分木（2 のべき乗サイズ）となり、右部分木にのみ不完全さが集中します。

graph TD
  subgraph "5 リーフのツリー（k=4 で分割）"
    Root["ルート"]
    Left["左部分木<br/>MTH(d₀..d₃)<br/>完全二分木"]
    Right["右部分木<br/>MTH(d₄)<br/>単一リーフ"]
    Root --> Left
    Root --> Right
  end

デフォルトのデモ構成では 64 票（2⁶）を扱うため、最終的なツリーは完全二分木になります。 ただし投票の追加途中や小規模な検証ケースでは非 2 のべき乗サイズが現れるため、実装は任意の treeSize に対する一般対応を備えます。

掲示板のリーフデータ形式

掲示板に追記される各投票のリーフデータは、コミットメントの正規化された 16 進数表現（0x なし、小文字、64 文字）を 32 バイトにデコードした生バイト列です。

leaf_data = hex_decode(normalized_commitment_hex) (32 バイト)

掲示板は以下の不変条件を維持します:

• 単調増加インデックス: 各投票に 0 から始まる連番が割り当てられる
• 重複排除: 同一の投票 ID やコミットメントの二重追記を拒否する
• ルート履歴: 各追記時点のルートハッシュをタイムスタンプとともに保存する

包含証明（Inclusion Proof）

包含証明は、特定のコミットメントがツリーの特定位置に含まれていることを、ルートハッシュに対して暗号学的に証明するものです。

構造

包含証明は以下の要素で構成されます:

実装での名称

本章では RFC 6962 の抽象名を使いますが、API では異なるフィールド名で返します。

finalization-scoped verification GET の voterEvidence.userVote.proof や /api/sessions/:sessionId/votes/:voteId/inclusion-proof がこの構造に対応します。

PATH アルゴリズム

RFC 6962 の PATH 関数に従い、Merkle パス（audit path、監査パス）を再帰的に生成します。

1. ツリーをサイズ k（n 未満の最大の 2 のべき乗）で左右に分割
2. 対象リーフが左部分木にある場合（index < k）:
   • 左部分木の PATH を再帰計算
   • 右部分木のハッシュをMerkle パスに追加
3. 対象リーフが右部分木にある場合（index >= k）:
   • 右部分木の PATH を再帰計算（インデックスを index - k に調整）
   • 左部分木のハッシュをMerkle パスに追加

検証手順

検証者は以下の手順で包含を確認します:

1. コミットメントのリーフハッシュを計算: LeafHash(commitment)
2. PATH アルゴリズムと同じ木構造に従い、Merkle パスのノードを順に結合
3. 計算されたルートが期待するルートハッシュと一致するか確認

Recorded-as-Cast では、包含証明に加えて以下の cast-time 一貫性も確認します:

• leafIndex がレシートの bulletinIndex と一致すること
• treeSize が bulletinIndex + 1 と一致すること（投票時点のツリーサイズ）

Merkle パスのサイズは O(log n) であり、64 票のツリーでは最大 6 ノードです。

graph TD
  subgraph "インデックス 5 の包含証明"
    Root["ルート ✓"]
    N1["H(N3, N4)<br/>Merkle パス"]
    N2["H(N5, N6) ← 計算対象"]
    N3["H(L0,L1)"]
    N4["H(L2,L3)"]
    N5["H(L4,L5) ← 計算対象"]
    N6["H(L6,L7)<br/>Merkle パス"]
    L4["L4<br/>Merkle パス"]
    L5["L5 ← 対象リーフ"]

    Root --> N1
    Root --> N2
    N1 --> N3
    N1 --> N4
    N2 --> N5
    N2 --> N6
    N5 --> L4
    N5 --> L5
  end

  style L5 fill:#4CAF50,color:#fff
  style N1 fill:#2196F3,color:#fff
  style N6 fill:#2196F3,color:#fff
  style L4 fill:#2196F3,color:#fff

整合性証明（Consistency Proof）

整合性証明は、古いツリー状態（サイズ m）が新しいツリー状態（サイズ n）の前方互換的なプレフィックスであることを暗号学的に証明するものです。 これは追記専用性の確認に使われます。

構造

補足: /api/sessions/:sessionId/bulletin/consistency-proof は proofNodes に加えて rootAtFromTreeSize と rootAtToTreeSize も返します。verification GET の recorded_consistency_proof 判定では、サーバーが取得・検査済みの root と整合性証明だけを 判定に使います。判定では from root を レシートの bulletinRootAtCast、to root を最終 bulletinRoot と照合します。

SUBPROOF アルゴリズム

RFC 6962 の SUBPROOF 関数に基づき、整合性証明を再帰的に生成します。

1. m = n かつ古いツリーが完全部分木: 空の証明を返す
2. m = n かつ完全部分木でない: 部分木のルートハッシュを返す
3. m = 1、n = 2、かつ古いツリーが完全部分木: 2 番目のリーフの生データを返す
4. k を n 未満の最大の 2 のべき乗とし:
   • m <= k の場合: 左部分木の SUBPROOF + 右部分木のハッシュ
   • m > k の場合: 右部分木の SUBPROOF + 左部分木のハッシュ

1→2 の特殊ケースでは、証明ノードは 2 番目のリーフの MTH ではなく生の 32 バイトリーフです。 検証時にそのリーフへ通常の LeafHash を適用し、SHA-256(0x01 || oldRoot || LeafHash(second_leaf)) が新しいルートと一致するかを確認します。

検証の意味

整合性証明の検証が成功することは、以下を意味します:

• 古いツリーのすべてのリーフが、新しいツリーにも同じ位置に同じ値で存在する
• 新しいツリーは古いツリーの末尾にリーフを追加しただけで構成されている
• 古いツリーのルートハッシュと新しいツリーのルートハッシュの両方が、提供された証明ノードから独立に再構成できる

この性質により、サーバーが過去に記録した投票を密かに削除したり順序を変更したりする攻撃を検出できます。

検証パイプラインにおける役割

CT Merkle ツリーは、4 段階検証モデルの主に 2 段階で使用されます。

Recorded-as-Cast では recorded_inclusion_proof と recorded_consistency_proof が表の役割を担当し、他の派生チェックもこれらの結果に基づきます。 ハッシュ規則の不一致は zkVM ゲスト内での検証失敗として即座に検出されます。

各チェックの判定ロジックは チェック一覧 > Recorded-as-Cast を参照してください。

RFC 6962 参照範囲

リーフハッシュへの使用タグ "stark-ballot:leaf|v1" の追加は RFC 6962 にない拡張であり、標準の CT 実装との直接的な相互運用は意図していません。

入力コミットメント

この章では、zkVM 入力のうち公開検証に使うフィールドを正準エンコーディングで束縛し、ジャーナルから再計算できる入力コミットメントを定義します。

入力コミットメントは、「証明されたデータセット」と「主張されたデータセット」の一致を検証可能にします。 バイトレベルの正準化は、TypeScript と Rust が同じ入力から決定的に同じ値を計算するための前提です。

概要

入力コミットメントは、公開可能な検証フィールドにドメインタグとバージョンを加えて正準連結し、SHA-256 で集約したハッシュ値です。

このハッシュ値は zkVM のジャーナル（公開出力）にコミットされます。 第三者は、ジャーナルに記録された入力コミットメントと、public-input.json などの公開可能な検証データから再計算した値を照合できます。 この照合により、zkVM が実際にどのデータセットを処理したかを独立に検証できます。

flowchart TB
  IN["入力データ<br/>electionId / bulletinRoot / treeSize<br/>/ totalExpected / votes (index 昇順)"]
  SPEC["固定値<br/>domainTag: stark-ballot:input|v1.0<br/>version: 10"]

  IN --> ENC[正準エンコーディング]
  SPEC --> ENC
  ENC --> H[SHA-256]
  H --> IC[入力コミットメント<br/>32 バイト]
  IC --> CMP["第三者照合<br/>再計算値 = journal.inputCommitment"]

入力コミットメントが解決する問題

zkVM の STARK 証明は、「ゲストプログラムが正しく実行された」ことを証明します。 一方で、「どの入力に対して実行されたか」は STARK 証明単体のスコープ外です。 入力コミットメントがなければ、悪意あるサーバーは次の攻撃が可能です。

1. 投票を除外した入力で zkVM を実行し、有効な STARK 証明を取得する
2. 公開用の入力データには除外されていない投票を含めて提示する
3. 第三者は STARK 証明が有効であることを確認できるが、実際に処理された入力は異なる

入力コミットメントをジャーナルに含めることで、第三者は「公開データから再計算した入力コミットメント」と「ジャーナルに記録された入力コミットメント」を照合できます。 不一致があれば、公開データと証明された入力の食い違いを検出できます。

正準エンコーディング

入力コミットメントの計算では、すべてのフィールドを決定的な順序とエンコーディングで連結します。

バイトレイアウト

input_commitment = SHA-256(
    domain_tag       ← "stark-ballot:input|v1.0" (23 バイト, UTF-8)
    || version       ← u32 リトルエンディアン (4 バイト) = 10
    || election_id   ← UUID v4 バイナリ (16 バイト)
    || bulletin_root ← 32 バイト
    || tree_size     ← u32 リトルエンディアン (4 バイト)
    || total_expected← u32 リトルエンディアン (4 バイト)
    || votes_count   ← u32 リトルエンディアン (4 バイト)
    || [投票データ]  ← インデックス昇順でソートされた各投票
)

各投票のエンコーディング

投票配列の各要素は次の形式でエンコードされます。

vote_entry =
    index            ← u32 リトルエンディアン (4 バイト)
    || commitment_len← u16 リトルエンディアン (2 バイト) = 32 (固定)
    || commitment    ← 32 バイト
    || path_len      ← u16 リトルエンディアン (2 バイト)
    || path_nodes    ← path_len × 32 バイト

フィールド一覧

public-input.json と公開監査アーティファクトとの関係

要点: public-input.json の全フィールドが入力コミットメントに束縛されるわけではありません。 残りのフィールドは、別のチェックで補完的に検証されます。

public-input.json は、zkVM 検証に使う秘密データを含まない検証用レコードです。 現行実装では schema、version、electionId、electionConfigHash、bulletinRoot、treeSize、totalExpected、logId、timestamp、methodVersion を含みます。 各投票については、index、コミットメント値、Merkle パスを含みます。

入力コミットメントが直接束縛するのは、フィールド一覧に示した対象のみです。 schema、version、electionConfigHash、logId、timestamp、methodVersion は対象外です。 対象外のフィールドは、proof bundle 内の election-manifest.json や close-statement.json を組み合わせて、次のように照合されます。

• electionConfigHash → counted_election_manifest_consistent（manifest と journal 等を照合）
• logId と timestamp → counted_close_statement_consistent（close statement と journal 等を照合）
• schema、version → public-input.json の管理対象 artifact format として artifact 採用時に検証
• methodVersion → public-input.json 採用時に journal と照合 Image ID 解決では正規化済み journal 値を使用

正準化規則

エンコーディングの決定性を保つために、次の規則を使います。

ソート規則

投票はエンコーディング前にインデックスの昇順にソートします。 各投票の index は一意であることが前提です。 この規則により、同じ投票集合から常に同一のバイト列が生成されます。 この規則に違反すると、TypeScript と Rust で異なるハッシュ値が計算され、検証が失敗します。

異常系の補助: 重複インデックスはプロトコル違反です。 TS/Rust 双方は決定性のために commitment / merklePath で tie-break しますが、正常系仕様は index 昇順のままです。

エンディアン規則

すべての整数フィールドはリトルエンディアンでエンコードされます。

16 進数正規化

コミットメント値やパスノードなどの 16 進数表現は、0x プレフィックスを除去した上でバイト列にデコードされます。 16 進数文字列のまま連結するのではなく、常にバイナリ表現を使用します。

TypeScript と Rust の同期

入力コミットメントは TypeScript（サーバー側）と Rust（zkVM ゲスト内）の双方で独立に計算されます。 両者の結果は一致する必要があります。

flowchart LR
  subgraph TypeScript
    TS_IN[public-input.json から抽出した<br/>入力コミットメント対象フィールド] --> TS_CALC[正準エンコーディング<br/>+ SHA-256]
    TS_CALC --> TS_IC[入力コミットメント A]
  end

  subgraph "Rust (zkVM ゲスト)"
    RS_IN[ゲスト入力] --> RS_CALC[正準エンコーディング<br/>+ SHA-256]
    RS_CALC --> RS_IC[入力コミットメント B]
  end

  TS_IC --> CMP{A = B ?}
  RS_IC --> CMP
  CMP -->|一致| OK[検証成功]
  CMP -->|不一致| NG[検証失敗:<br/>入力データが異なる]

同期が破壊される典型的な原因は次のとおりです。

• ソート順序の不一致
• エンディアンの不一致
• ドメインタグの文字列差異
• バージョン番号の不一致
• 16 進数正規化規則の差異（大文字/小文字、0x プレフィックスの有無）

検証パイプラインにおける役割

入力コミットメントは、Counted-as-Recorded 段階の検証チェック counted_input_commitment_match で使用されます。

このチェックが失敗すると、zkVM が処理した入力データと、公開可能な検証データから再構成される対象フィールドが食い違うことを意味します。 その場合、結果の信頼性は根本的に損なわれます。 対象外フィールドの補完検証は上記のとおりです。

各チェックの判定ロジックは チェック一覧 > Counted-as-Recorded を参照してください。

注意事項

入力コミットメントには、投票者の秘密データ（選択肢や乱数）は含まれません。 したがって、入力コミットメントの公開は投票の秘密性を損ないません。

入力順序に依存しない正準エンコーディングは、Property-based Testing の permutation invariance と、Lean による形式化 の input-commitment vectors で検査します。

STH ダイジェスト

このページでは、Signed Tree Head ダイジェストを第三者と照合し、スプリットビュー攻撃を緩和する仕組みを説明します。

ログ ID、ツリーサイズ、タイムスタンプ、掲示板ルートを束縛するダイジェストにより、サーバーが異なるクライアントに異なるツリー状態を提示する攻撃を検出可能にします。

スプリットビュー攻撃に対する位置づけ

スプリットビュー攻撃（split-view attack）とは、悪意あるサーバーが異なる検証者に対して異なる掲示板の状態を提示する攻撃です。 STH ダイジェストは、掲示板の状態を（ログ ID、ツリーサイズ、タイムスタンプ、ルートハッシュ）の組として束縛し、独立した第三者ソースとの合意確認を通じてこの攻撃を検出します。 具体的な攻撃と検出の流れは後述します。

flowchart TD
  subgraph "STH ダイジェストの構成"
    LID[ログ ID<br/>32 バイト]
    TSZ[ツリーサイズ<br/>4 バイト]
    TS[タイムスタンプ<br/>8 バイト]
    BR[掲示板ルート<br/>32 バイト]
  end

  LID --> H[SHA-256]
  TSZ --> H
  TS --> H
  BR --> H
  H --> STH[STH ダイジェスト<br/>32 バイト]

  STH --> J[zkVM ジャーナルに記録]
  STH --> CS[close-statement.json に記録]
  STH --> TP[第三者ソースの STH と照合]

本実装での検証対象: このページで言う「STH ダイジェスト」は sthDigest 自体です。 本実装は STH の署名検証は行いません（スコープの詳細は 合意ロジック を参照）。

ダイジェストフォーマット

sth_digest = SHA-256(
    log_id        ← 32 バイト
    || tree_size  ← u32 リトルエンディアン (4 バイト)
    || timestamp  ← u64 リトルエンディアン (8 バイト, Unix 時刻ミリ秒)
    || bulletin_root ← 32 バイト
)

SHA-256 への入力は合計 76 バイトです。

各フィールドの仕様

ログ ID

ログ ID は掲示板インスタンスを一意に識別する値です。 次の式で生成されます。

log_id = SHA-256("stark-ballot:bulletin-log|v1.0" || seed)

ドメインタグ "stark-ballot:bulletin-log|v1.0" と任意のシード値を連結し、SHA-256 でハッシュします。 ログ ID は掲示板のライフタイム中に変化しない固定値です。

ログ ID を STH ダイジェストに含めることで、異なる掲示板インスタンスの STH が偶然に衝突することを防止します。

スプリットビュー攻撃と検出メカニズム

攻撃シナリオ

sequenceDiagram
    participant A as 投票者 A
    participant S as 悪意あるサーバー
    participant B as 投票者 B

    S->>A: ツリー状態 X<br/>(64 票、ルート R₁)
    S->>B: ツリー状態 Y<br/>(63 票、ルート R₂)
    Note over A,B: A と B は互いに異なる<br/>ツリー状態を見ている

この攻撃では、サーバーは投票者 B に対して特定の票を除外したツリーを見せています。 投票者 B は自身に提示されたツリーに対する包含証明や整合性証明を検証できますが、投票者 A とは異なるツリーを見ていることに気づけません。

第三者合意による検出

検証 API は、VITE_STH_SOURCES に設定されたソースから STH evidence を取得し、ジャーナル内の STH ダイジェストと照合することでスプリットビューを検出できます。

sequenceDiagram
    participant V as 検証者
    participant S as 検証 API
    participant T1 as 第三者ソース 1
    participant T2 as 第三者ソース 2

    V->>S: 検証リソースを要求
    S->>S: ジャーナルから STH ダイジェスト D' を取得
    S->>T1: STH を問い合わせ → D₁
    S->>T2: STH を問い合わせ → D₂
    S->>S: D' = D₁ = D₂ ?
    alt 全て一致
        S->>V: 合意成立を含む検証結果
    else 不一致あり
        S->>V: スプリットビューの疑い → 検証失敗
    end

合意ロジック

合意判定の条件（最小一致数と全会一致の要求）は チェック一覧 > recorded_sth_third_party を正とします。 各ソースに対して次のフィールドを照合します。

外部 HTTPS ソースの応答は、sthDigest、bulletinRoot、treeSize、timestamp、logId だけを許可する flat な canonical record として fail-closed に受理します。sthDigest は必須で、 その他のフィールドは任意ですが、指定された場合は型と形式を検証します。wrapper、未知のキー、 digest / root / log_id などの alias は受理しません。 設定済みソースの取得失敗、利用不能、または malformed response は、ほかの受理済みソースが 最小一致数を満たしていても合意失敗になります。

冒頭の注記のとおり応答署名は検証しません。外部アンカリングと STH の自動公開も本実装のスコープ外です。

zkVM との連携

zkVM ゲストプログラムは、入力として受け取ったログ ID、ツリーサイズ、タイムスタンプ、掲示板ルートから STH ダイジェストを再計算し、ジャーナルにコミットします。

finalize 時には、同じツリー状態から close-statement.json も構築されます。 sthDigest は、配布対象アーカイブ bundle.zip に含まれる公開監査アーティファクトへ反映されます。

この仕組みにより、STARK 証明と bundle.zip 内の close-statement.json がともに特定のツリー状態へ束縛されます。 第三者はジャーナルの STH ダイジェストを独立ソースの値と照合することで、サーバーが証明と異なるツリー状態を提示していないかを確認できます。

検証パイプラインにおける役割

STH ダイジェストは 2 つの段階で利用されます。

recorded_sth_third_party は既定では任意チェック（optional）ですが、STH ソースが設定されている場合は required に昇格します（昇格と最終判定の規則は ゲーティングロジック を参照）。

counted_close_statement_consistent は常に必須チェック（required）です。 close-statement.json がジャーナルと整合しない場合、検証は失敗します。

各チェックの判定ロジックは チェック一覧 > Recorded-as-Cast と チェック一覧 > Counted-as-Recorded を参照してください。

設定

第三者 STH 検証は環境変数で制御されます。

STH ソースが未設定の場合、recorded_sth_third_party は not_run（未実行）となり、第三者照合は行いません。

開発用の .env.local.example では、必要な場合に有効化する例として次の値がコメントで示されています。

• VITE_STH_SOURCES=/api/sessions/:sessionId/bulletin/sth
• VITE_STH_MIN_MATCHES=1

same-origin template と外部 HTTPS source の取り扱い

same-origin template: 相対 source として受理するのは exact template /api/sessions/:sessionId/bulletin/sth だけです。任意で auditorId query を 1 つ指定できます。 検証 API は :sessionId を現在の session ID で解決し、認証済み session context から STH を 直接 project します。この内部取得では HTTP request や session capability header の転送を行いません。

同じ path を通常の HTTP endpoint として直接取得する場合は、same-origin request と path の session ID に対応する X-Session-Capability が必要です。finalization が成功している session に限り、 { data: { sth: { ... } }, meta } envelope を返します。

外部 HTTPS source: absolute HTTPS URL は、app と同じ origin を指す場合でも外部 source として 取得します。repository の session capability や同等の認証情報は送信しません。そのため、独立した 第三者 source は session 認証に依存しない公開 STH endpoint である必要があります。

same-origin projection の timestamp: same-origin projection が返す timestamp はジャーナル内の canonical な時刻ではなく session.voting.lastActivityMs です。 そのため、第三者合意の一致判定で実際に照合するのは必須の sthDigest と、ソースが返した場合の bulletinRoot / treeSize です。

PoC における制約

本 PoC の開発用テンプレート（.env.local.example）では、STH ソースとして同一サーバー上の session-scoped template（/api/sessions/:sessionId/bulletin/sth）を使う例を示しています。 同一サーバー上のソースのみでは防御力が限定的であるため、独立した組織が運営する複数ソースを VITE_STH_MIN_MATCHES >= 2 で構成することを推奨します。

ビットマップ Merkle

自票が集計に含まれたかを Merkle 証明で開示するためのビットマップツリーを扱う章です。

zkVM ゲスト内で計算されるビットマップにより、各投票インデックスが集計に含まれたかどうかを個別に検証可能にします。 Merkle 証明により、自票が含まれていることをサーバーを信頼せずに確認できます。

概要

Counted-as-Recorded 段階の検証では、zkVM に提示された入力に対する集計の正しさは STARK 証明で保証されますが、個々の投票者にとって「自票が集計に含まれたか」を直接確認する手段が別途必要です。

ビットマップ Merkle ツリーは、この「個別のカウント証明」を提供します。 zkVM ゲストは投票ごとの状態をビットマップとしてエンコードし、その Merkle ルートをジャーナルにコミットします。 投票者は自分のインデックスに対応するビットの Merkle 証明を取得し、「自票がカウントされたか」「そもそも prover に提示されたか」を独立に検証できます。

flowchart TD
  subgraph "zkVM ゲスト内"
    BM["ビットマップ<br/>[true, true, false, true, ...]"] --> PK[ビットパッキング<br/>LSB-first]
    PK --> CH[32 バイトチャンク分割]
    CH --> LH["リーフハッシュ<br/>SHA-256(0x00 || tag || chunk)"]
    LH --> MT[Merkle ツリー構築]
    MT --> ROOT["includedBitmapRoot / seenBitmapRoot"]
  end

  ROOT --> JNL[ジャーナルにコミット]

ビットマップの構造

ビットマップの定義

ビットマップは、ツリーサイズ（投票数）と同じ長さのブール配列です。 現行実装では同じエンコーディング規則を持つ 2 種類のビットマップを扱います。

• includedBitmap[i] = true: インデックス i の投票が正常に検証され、集計に含まれた
• includedBitmap[i] = false: インデックス i の投票が除外された
• seenBitmap[i] = true: インデックス i の投票が prover に提示された
• seenBitmap[i] = false: インデックス i の投票が prover に提示されなかった

本 PoC では 64 票を扱うため、ビットマップは 64 ビット（= 8 バイト）です。

LSB-first ビットパッキング

ブール配列は LSB-first（Least Significant Bit first）方式でバイト列にパッキングされます。

ビット配列: [b₀, b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, ...]

バイト 0 = b₀ | (b₁ << 1) | (b₂ << 2) | ... | (b₇ << 7)
バイト 1 = b₈ | (b₉ << 1) | ...

64 ビットのビットマップは 8 バイトにパッキングされます。

32 バイトチャンク分割

パッキングされたバイト列は 32 バイト（256 ビット）単位のチャンクに分割されます。 各チャンクが Merkle ツリーの 1 つのリーフとなります。

• 1 チャンク = 32 バイト = 256 ビット分の投票カウント状態
• 最後のチャンクが 32 バイトに満たない場合はゼロパディング

本 PoC の 64 票は 8 バイトであるため、1 つのチャンク（24 バイトのゼロパディング付き）に収まります。

Merkle ツリーの構築

ハッシュ規則

ビットマップ Merkle ツリーは、CT Merkle ツリーと同一のハッシュ規則を使用します。

リーフハッシュ:

LeafHash = SHA-256(0x00 || "stark-ballot:leaf|v1" || chunk)

内部ノードハッシュ:

NodeHash = SHA-256(0x01 || left_hash || right_hash)

ドメイン分離プレフィックス（0x00 / 0x01）と使用タグ（"stark-ballot:leaf|v1"）は、CT Merkle ツリーの章で解説したものと同一です。

ツリー構築アルゴリズム

1. 各 32 バイトチャンクにリーフハッシュを適用
2. ボトムアップでペアを結合し、内部ノードハッシュを計算
3. 奇数ノードがある場合は、そのまま次のレベルに昇格（ハッシュなし）
4. ルートに到達するまで繰り返す

graph TD
  subgraph "3 チャンクの場合"
    R["ルート<br/>SHA-256(0x01 || N1 || C2)"]
    N1["ノード<br/>SHA-256(0x01 || C0 || C1)"]
    C2["リーフ 2<br/>SHA-256(0x00 || tag || chunk₂)"]
    C0["リーフ 0<br/>SHA-256(0x00 || tag || chunk₀)"]
    C1["リーフ 1<br/>SHA-256(0x00 || tag || chunk₁)"]

    R --> N1
    R --> C2
    N1 --> C0
    N1 --> C1
  end

Merkle 証明の生成と検証

証明の構造

GET /api/sessions/:sessionId/finalizations/current/bitmap-proofs/:kind/:voteIndex は、現在の finalization に対する証明材料を返します。kind と voteIndex はどちらも必須の path parameter です。成功時の標準 JSON envelope は次の形です。

{
  "data": {
    "leafChunk": "...",
    "auditPath": []
  },
  "meta": {
    "requestId": "..."
  }
}

data は以下の要素で構成されます:

leafIndex（floor(voteIndex / 256)）と bitOffset（voteIndex mod 256）は、クライアント側で path の voteIndex から導出します。 サーバーは返しません。

• kind=included: includedBitmapRoot に対する証明を返す
• kind=seen: seenBitmapRoot に対する証明を返す

このエンドポイントは path のセッション ID と X-Session-Capability を必須とし、 voteIndex はそのセッションで cast した自票の index に限られます （任意の近傍 index に対する proof oracle としては利用できません）。

ビット抽出

投票者は受け取ったチャンクから、path で指定した voteIndex に対応する bitIndex のビットを以下の手順で抽出します:

bit_offset  = bit_index mod 256
byte_index  = bit_offset / 8    (整数除算)
bit_in_byte = bit_offset mod 8

included = (chunk[byte_index] AND (1 << bit_in_byte)) != 0

kind=included で included = true なら、自票がカウントされたことを意味します。 kind=seen で included = true なら、自票が prover に提示されたことを意味します。

検証手順

1. ジャーナルの正の整数 treeSize と 32 バイトの対象 root を認証済み context として使い、 bitIndex が 0 <= bitIndex < treeSize を満たすことを確認
2. leafIndex = floor(bitIndex / 256)、bitOffset = bitIndex mod 256、 leafCount = ceil(treeSize / 256) をクライアント側で導出
3. leafChunk が 32 バイト、各 sibling hash が 32 バイトであることに加え、 auditPath の長さと left / right の並びが leafIndex と leafCount から 一意に決まる tree shape と一致することを確認
4. 最終 chunk の treeSize より後ろにある未使用 bit がすべて 0 であることを確認
5. チャンクのリーフハッシュを計算: SHA-256(0x00 || "stark-ballot:leaf|v1" || chunk)
6. Merkle パス（auditPath）に沿ってルートまで再計算:
   • 兄弟の位置が left → SHA-256(0x01 || sibling || current)
   • 兄弟の位置が right → SHA-256(0x01 || current || sibling)
7. 計算されたルートが、kind に対応するジャーナル上のルートと一致するか確認
   • kind=included → includedBitmapRoot
   • kind=seen → seenBitmapRoot
8. 以上がすべて成功した場合にのみ、チャンクから抽出したビット値を個票の状態として解釈

flowchart TD
  CK[チャンク受信] --> SH{treeSize / index / path shape<br/>unused padding は正しい?}
  SH -->|正しい| LH["リーフハッシュ計算"]
  LH --> AP[Merkle パスに沿って<br/>ルートを再計算]
  AP --> CMP{計算ルート =<br/>bitmap root ?}
  CMP -->|一致| EX[ビット抽出結果を解釈<br/>included = true/false]
  EX --> V[証明有効]
  CMP -->|不一致| IV[証明無効]
  SH -->|不正| IV

zkVM ゲストとの連携

ビットマップルートは zkVM ゲストプログラム内で計算され、ジャーナルにコミットされます。

ゲストプログラムは以下の手順を実行します:

1. 各投票に対してコミットメントの再計算と包含証明の検証を実施
2. prover に提示された投票インデックスを seenBitmap に記録
3. 検証に成功して集計対象になった投票インデックスを includedBitmap に記録
4. それぞれのビットマップを LSB-first でパッキングし、32 バイトチャンクに分割
5. CT スタイルのハッシュ規則で Merkle ルートを計算
6. seenBitmapRoot と includedBitmapRoot をジャーナルにコミット

この計算はゲスト内で行われるため、STARK 証明がビットマップの正しさも保証します。 サーバーが事後的にビットマップを改ざんしても、ジャーナルのルート値と一致しなくなるため検出されます。

サーバーのビットマップデータ管理

現行 method 14 のジャーナルは includedBitmapRoot と seenBitmapRoot の両方を必須で コミットします。full bitmap 自体はジャーナルの公開出力ではありません。production host は admitted prover input から includedBitmap と seenBitmap を再構成し、guest output の root と 一致した場合に sidecar を出力します。finalization 時の保存・復元と bitmap-proof endpoint はさらに、 bitmap の長さが treeSize と一致し、再計算した root が保存 root とジャーナル root の両方に 一致した場合にのみ、その非公開 sidecar を採用します。 これらは配布対象アーカイブ bundle.zip には含まれません。 async finalize 経路では、必要に応じて S3 の sibling object から復元されます。

安全性ゲートと検証結果の分岐

採用前と採用後で、counted_my_vote_included の判定が次の 2 つに分岐します。

• 採用前に弾かれる、または証明材料が取得できない → counted_my_vote_included は not_run（証拠不足による fail-closed）。 例:
  • private bitmap sidecar が無い
  • 保存や復元時の root 一致ゲートで採用されなかった
  • cast-time 証跡（voteReceipt / userVote.proof）が store から再構成できず voteReceipt.bulletinIndex が確定しない
• 採用後にクライアント側の root 照合が失敗 → counted_my_vote_included は failed。 サーバーが返した chunk と Merkle パスから再計算したルートが、ジャーナルの includedBitmapRoot（または seenBitmapRoot）と一致しない。

採用前ゲートおよび counted_my_vote_included の評価詳細は チェック一覧 > counted_my_vote_included を参照してください。

検証パイプラインにおける役割

ビットマップ Merkle 証明は、Counted-as-Recorded 段階のチェックとして使用されます。

対応する seenBitmap sidecar から生成した proof も取得・採用できた場合 （seenBitmapRoot はジャーナル必須。前述）、 このチェックは「prover に提示されたが無効化された」 と「そもそも提示されなかった」を区別して説明します。seen proof が取得または検証できない場合は、 included bit が false である理由を unknown_excluded として fail-closed に扱い、推測で分類しません。

各チェックの判定ロジックは チェック一覧 > Counted-as-Recorded を参照してください。

プライバシーに関する注意

ビットマップ Merkle 証明では、対象ビットを含む 32 バイトチャンク全体がクライアントに提供されます。 1 チャンクは 256 ビット分のカウント状態を含むため、近傍のインデックスのカウント状態が同時に開示されます。

本 PoC では 64 票が 1 チャンクに収まるため、チャンクを受け取った投票者は全 64 票のカウント状態を知ることができます。 この設計は、63 票がボットでありチャンク漏洩の情報価値が限定的である、という割り切りに基づきます。

開示範囲を狭めるには、chunk を小さくして Merkle tree を深くする方法があります。 一方で leaf 数、proof path、guest 内の hash 計算が増えるため、証明時間と artifact サイズを再評価する必要があります。現行 PoC は 32 バイト chunk を維持し、この 緩和は実装していません。

LSB-first packing とビット境界の扱いは、Property-based Testing で生成入力を使って境界条件を探索し、Lean による形式化 の bitmap vectors で抽象モデルとの対応を検査します。

zkVM 設計

この章群では、投票集計の正当性を RISC Zero zkVM で検証し、レシートとジャーナルを検証パイプラインへ渡す流れを説明します。 mock、RISC0_DEV_MODE=1、production STARK proof は、それぞれ異なる検証前提として区別します。

この部の章

• zkVM の基礎 では、zkVM の概念、RISC Zero の選択理由、データフロー、保証境界を扱います。
• ゲストプログラム では、zkVM 内で実行される検証と集計ロジックを扱います。
• ホストと証明生成 では、ホストプログラムと同期または非同期の証明パスを扱います。
• 検証サービス では、Rust ベースのレシート検証を扱います。
• Image ID では、ゲストバイナリの暗号的識別子と管理を扱います。

想定読者と前提

• 想定読者は、集計の正当性を STARK で証明したい実装者と運用者です。
• 前提は、暗号プロトコル の入力コミットメントと Merkle ツリーを把握していることです。

この部で扱わないもの

• RISC Zero SDK の API リファレンスやアップグレード手順
• STARK / FRI の数学的構成証明
• ECS Fargate などインフラ側の構成

STARK / FRI の概念は zkVM の基礎 で扱います。 インフラ側の構成は AWS アーキテクチャ を参照してください。

関連する章

• 暗号プロトコル は、ゲストプログラムが入力として受け取るプリミティブを説明します。
• 検証パイプライン は、生成されたレシートとジャーナルの検証方法を説明します。
• AWS アーキテクチャ は、非同期プローバーの実行環境を説明します。
• 第三者検証ガイド は、bundle.zip でレシートをローカル監査する手順を説明します。

zkVM の基礎

RISC Zero zkVM を採用した理由、データフロー、暗号学的保証の境界を整理する章です。

RISC Zero を採用する理由

• Trusted setup 不要で扱いやすい。
• RISC-V 上で通常の Rust コードを使えるため、実装と監査の往復がしやすい。
• Image ID による実行バイナリ照合と組み合わせやすい。

アーキテクチャ概要

zkVM パイプラインは 3 つのコンポーネントで構成されます。

flowchart TB
  subgraph C1["第1フェーズ: 入力構築"]
    SES[セッションデータ] --> IB[入力ビルダー]
    IB --> INP[ZkVMInput]
  end

  subgraph C2["第2フェーズ: 証明生成"]
    INP --> HOST[ホストプログラム]
    HOST --> GUEST["ゲストプログラム<br/>(zkVM 内実行)"]
    GUEST --> JNL[ジャーナル]
    HOST --> RCP[レシート<br/>STARK 証明]
  end

  subgraph C3["第3フェーズ: 検証"]
    RCP --> VS[検証サービス]
    VS --> VR[検証レポート]
  end

zkVM とは

RISC Zero zkVM は、RISC-V（RV32IM）命令列として実行されるゲストプログラムについて、その実行が正しいことを STARK 証明で示すゼロ知識 VM です。

本システムでは「投票検証と集計」をゲストとして実行し、ホストがレシート（seal + journal）を生成します。 第三者は Receipt::verify(image_id) により、指定したゲストバイナリ（Image ID）で実行された結果であることを検証できます。

30 秒で要点

ジャーナルは証明に束縛される公開出力であり、検証成功後に改ざんできません。 Receipt::verify(image_id) 単体は、ゲストに渡された非公開入力を特定せず、公開された public-input.json との一致も保証しません。 本 PoC は、公開入力のうちコミットメント対象フィールドから値を再計算し、ジャーナルの inputCommitment と照合する必須チェック counted_input_commitment_match によって、その対象フィールドを証明済み実行へ束縛します。 対象外フィールドは別の必須チェックで補完します。詳細は 入力コミットメント を参照してください。 ジャーナル項目の一覧と各フィールドが何を保証するかは ゲストプログラム > ジャーナル出力 を参照してください。 配布対象ファイル（bundle.zip 等）との違いは バンドル構造 を参照してください。

RISC Zero zkVM 実装の要点

RISC Zero 公式ドキュメントに基づく実装上の要点です。

1. 実行モデル: ゲストは RV32IM として決定論的に実行され、外部との境界は syscall (ecall) で扱う
2. 証明の分割: 長い実行はセグメント証明に分割される（大規模実行を扱うため）
3. 再帰合成と圧縮: SDK は再帰合成や succinct / Groth16 への圧縮をサポートするが、本 PoC は Composite receipt のまま配布する
4. 検証 API: Receipt::verify(image_id) が、証明本体と Image ID の束縛を同時に検証する
5. 公開出力の束縛: journal は証明に束縛されるため、検証成功後に改ざんできない

ジャーナルとレシート

• ジャーナル: ゲストが公開出力としてコミットするデータ（検証済み集計、除外情報、入力コミットメントなど）
• レシート: ジャーナルと STARK 証明（seal）のペア。 検証成功時、ジャーナルは正しいゲスト実行結果として受理できる

flowchart TB
  R[レシート]
  R --> S[Seal<br/>STARK 証明]
  R --> J[ジャーナル<br/>公開出力]

ジャーナル各フィールドの定義と検証チェックとの対応は ゲストプログラム > ジャーナル出力 を参照してください。 excludedSlots と rejectedRecords の使い分けは スロット / レコード分離モデル を参照してください。

数学ミニ補足（読み飛ばし可）

STARK の直感的理解に必要な最小限の説明だけを記します。

1. 巡回ドメイン（cyclic domain）

有限体 F の乗法群の部分群 H = {1, w, w^2, ..., w^(n-1)} を評価点集合（ドメイン）として使います。 RISC Zero はこれを cyclic domain と呼びます。 実行トレース（レジスタ値や遷移）は、この H 上で評価される多項式として扱われます。

2. 有限体上の多項式除算

制約違反の有無は、概念的には次の形で整理できます。

• 制約多項式を C(x) とする
• 評価領域 H の零化多項式を Z_H(x) とする（典型例: Z_H(x) = x^n - 1）
• すべての点で制約を満たすなら C(h)=0（h in H）となり、C(x) は Z_H(x) で割り切れる
• したがって Q(x) = C(x) / Z_H(x) が多項式として成立するかを検査すれば、制約満足性をチェックできる

実際の STARK では、FRI（Fast Reed-Solomon IOP）と Merkle コミットメントを組み合わせて、この条件を効率的に検証します。

この PoC での保証境界

Receipt::verify(image_id) の成功は強い保証ですが、それ単体では「全票が提示された」ことまでは保証せず、Verified 表示には不十分です。 Verified は、STARK 検証成功に加えて、excludedSlots == 0、totalExpected == treeSize、追記専用性と締切 STH を含む必須チェックがすべて成功した場合にのみ成立します。 詳細なゲーティング規範と判定ロジックは ゲーティングロジック を参照してください。

参考資料（RISC Zero 公式）

• zkVM Technical Specification
• Recursion (proof composition)
• STARK by Hand

データフロー

投票セッションの開始からレシート検証までの全体的なデータフローを示します。

sequenceDiagram
  participant V as 投票者
  participant S as サーバー
  participant B as 掲示板
  participant H as ホスト
  participant G as ゲスト (zkVM)
  participant VS as 検証サービス

  Note over V,B: 投票フェーズ
  V->>S: 投票意図（選択肢・乱数）+ コミットメント
  S->>B: 掲示板に追記
  S-->>V: 投票レシート (インデックス, ルート)
  Note over S: ボット投票を自動追加

  Note over S,G: 集計フェーズ
  S->>S: 入力ビルダーで ZkVMInput を構築
  S->>H: ZkVMInput を渡す
  H->>G: ゲスト実行を開始
  G->>G: 各投票のコミットメント検証
  G->>G: 各投票の包含証明検証
  G->>G: 集計 + ビットマップ計算
  G-->>H: ジャーナル出力
  H-->>S: STARK レシート + ジャーナル

  Note over S,VS: 検証フェーズ
  S->>VS: 検証 bundle 参照 + 期待 Image ID
  VS->>VS: bundle 内の receipt.json を解決
  VS->>VS: Receipt::verify(image_id)
  VS-->>S: 検証レポート
  S-->>V: 検証結果を提供

ゲストプログラム

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 は、抽象モデルと実装の対応付けを検査します。

ホストと証明生成

この章では、ホストプログラムが zkVM 入力を組み立て、同期モードまたは非同期モードで STARK 証明を生成する流れを扱います。

どちらのモードも同じ Rust ホスト CLI / 入出力契約を使用します。

このページの構成:

• パイプライン全体像
• 入力構築
• ホストプログラムの実行
• 同期モード
• 非同期モード
• 開発モードの動作

パイプライン全体像

証明生成パイプラインは、入力構築、ホスト実行、出力処理の 3 フェーズで構成されます。

flowchart TD
  subgraph "第1フェーズ: 入力構築 (TypeScript)"
    SD[セッションデータ] --> IB[入力ビルダー]
    IB --> ZI[ZkVMInput]
    ZI --> SER[シリアライズ<br/>JSON ファイル]
  end

  subgraph "第2フェーズ: ホスト実行 (Rust)"
    SER --> HOST[ホストバイナリ]
    HOST --> ENV[ExecutorEnv 構築]
    ENV --> PROVER[デフォルトプローバー]
    PROVER --> GUEST[ゲスト実行]
    GUEST --> PROOF[STARK 証明生成]
  end

  subgraph "第3フェーズ: 出力処理"
    PROOF --> RCP["レシートラッパー JSON<br/>(seal + journal)"]
    PROOF --> OUT["出力 JSON<br/>(デコード済みジャーナル)"]
  end

入力構築

現行 PoC の選挙 shape

デモの session orchestration は、選択肢 A〜E、ユーザー 1 票、 ボット 63 票、合計 64 slot、Merkle tree depth 6 に固定されています。 default config の authority は packages/zkvm-contract/src/zkvm/contract-constants.ts と packages/zkvm-contract/src/zkvm/election-config.ts です。domain と verification package の公開定数は repository boundary test で同値性を確認します。

これは PoC の再現可能なデモ構成であり、zkVM guest や RFC 6962 Merkle 実装を任意の session で常に 64 票に制限するプロトコル主張ではありません。 host input は admitted election configuration の totalExpected と bulletin の treeSize を保持し、その一致は検証パイプラインで fail-closed に確認します。

セッションデータからの抽出

入力ビルダーは、投票セッションに蓄積されたデータから zkVM 入力を構築します。

flowchart LR
  subgraph セッションデータ
    EID[選挙 ID]
    ECFG[選挙設定<br/>+ 設定ハッシュ]
    VOTES["投票データ<br/>(選択肢, 乱数, コミットメント)"]
    BULL["掲示板<br/>(ルート履歴, 包含証明)"]
    LID[ログ ID]
  end

  subgraph ZkVMInput
    EID2[election_id]
    ECFG2[election_config_hash]
    BR[bulletin_root]
    TS[tree_size]
    TE[total_expected]
    VWP["votes[]<br/>(VoteWithProof)"]
    LID2[log_id]
    TSTAMP[timestamp]
  end

  EID --> EID2
  ECFG --> ECFG2
  ECFG --> TE
  BULL --> BR
  BULL --> TS
  VOTES --> VWP
  LID --> LID2

入力構築の主な処理は次のとおりです。

1. 掲示板の最新 STH スナップショット取得: ルートハッシュ、ツリーサイズ、タイムスタンプを取得します。
2. 選挙設定の整合性確認: electionConfig と electionConfigHash が一致することを確認します。
3. 投票データの変換: 各投票の選択肢を整数に変換します（A=0, B=1, C=2, D=3, E=4）。
4. Merkle パスの解決: 各投票について、掲示板から最新の包含証明を取得します。
5. 総投票数の設定: 選挙設定の totalExpected を設定します（デモ定数は 現行 PoC の選挙 shape を参照）。

通常のセッション入力では、投票インデックスが 0 から連続する canonical CT index であることを要求します。 教育的な除外シナリオでは、元の掲示板インデックスを保つために sparse index を許可します。 これにより、ゲスト側で missingSlots として観測できます。

Merkle パスの解決戦略

各投票の Merkle パスは、session の canonical bulletin authority から解決します。 保存済みの投票レコードは proof path を保持しないため、別の事前計算パスへの fallback はありません。

flowchart TD
  START[Merkle パス解決] --> P1{掲示板から<br/>包含証明を取得可能?}
  P1 -->|Yes| CHK{leaf index と<br/>treeSize が一致?}
  CHK -->|Yes| USE1[掲示板の証明を使用]
  CHK -->|No| ERR[エラー]
  P1 -->|No| ERR

ホストプログラムの実行

ホストバイナリの役割

ホストバイナリは Rust で記述された CLI プログラムです。 証明モードでは次の処理を行います。

1. JSON 形式の入力ファイルを読み込みます。
2. JSON のバイト配列表現を Rust の固定長配列型へ変換します（Vec<u8> → [u8; 16/32]）。
3. ExecutorEnv に入力をシリアライズして設定します。
4. デフォルトプローバーを使用して zkVM ゲストを実行します。
5. レシート（STARK 証明 + ジャーナル）を取得します。
6. ジャーナルをデコードし、出力ファイルに書き出します。

入力 JSON は TypeScript 側のエグゼキューターが事前に正規化して生成します（UUID/ハッシュ文字列をバイト配列へ変換）。

Image ID の確認だけを行う場合は host --print-image-id [--json] を使います。 このモードでは入力ファイルを読まず、証明生成やアーティファクト出力も行いません。 --json 付きでは imageId と methodVersion を含む JSON を stdout に出力します。

境界に違反する入力が渡された場合、host run は fail-closed で停止し、receipt と journal を出力しません。 境界条件の詳細は 処理パイプライン を参照してください。

非同期モードで S3 に置かれる work input には、host CLI の証明入力に加えて election_config / electionConfig も含まれます。コンテナ entrypoint はこの設定を election-manifest.json の生成と入力の整合性検査に使います。退役済みの contractGeneration / contract_generation は work input に含めません。

出力ファイル

証明モードのホストバイナリは 2 つの JSON ファイルを出力します。 ビットマップ整合性検査を通過した場合は、private bitmap artifact も追加で出力します。

レシートラッパー JSON には top-level image_id フィールドも含まれます。 検証サービスでの使われ方は 検証サービス を参照してください。

ホストはビットマップの整合性を確認し、一致した場合のみ次の非公開アーティファクトを出力します。

非同期モードでの配置と非同梱の扱いは 配布対象アーカイブの構築 を参照してください。

同期モード

同期モードでは、TypeScript のサーバーサイドプロセスからホストバイナリを直接起動します。

sequenceDiagram
  participant S as サーバー (TypeScript)
  participant E as エグゼキューター
  participant H as ホストバイナリ (Rust)
  participant FS as ファイルシステム

  S->>E: executeZkVM(input)
  E->>FS: 入力 JSON を一時ファイルに書き出し
  E->>H: 子プロセスとして起動
  Note over H: zkVM ゲスト実行<br/>+ STARK 証明生成
  H->>FS: レシートラッパー JSON + 出力 JSON を書き出し
  H-->>E: プロセス終了
  E->>FS: 出力ファイルを読み取り
  E->>FS: 一時ファイルを削除
  E-->>S: ZkVMExecutionResult

同期モードの特性

結果の変換

エグゼキューターは出力 JSON のフィールドを TypeScript の命名規則へ正規化し、文字列だけでなくバイト配列形式の値も受理します。 ハッシュ系フィールドは 0x 付き 16 進文字列に、election_id は UUID 文字列に変換して ZkVMExecutionResult を構築します。

非同期モード

AWS 環境では、証明生成を ECS Fargate タスクとして非同期に実行します。 STARK 証明の生成に数分を要するため、Lambda のタイムアウト制限を回避し、専用のコンピューティングリソースを割り当てます。

sequenceDiagram
  participant S as サーバー
  participant SQS as SQS
  participant D as ディスパッチ Lambda
  participant SFN as Step Functions
  participant ECS as ECS Fargate
  participant S3 as S3
  participant CB as コールバック Lambda

  S->>S3: 入力 JSON アップロード
  S->>SQS: finalization リクエスト<br/>(inputS3Key を含む)
  SQS->>D: work message
  D->>SFN: SFN 実行開始<br/>(inputS3Key を渡す)
  Note over SFN: イメージ署名チェック
  SFN->>ECS: プローバータスク起動
  ECS->>S3: 入力 JSON ダウンロード
  Note over ECS: ホストバイナリ実行<br/>+ STARK 証明生成
  ECS->>S3: レシート・出力・公開アーティファクト・<br/>バンドルをアップロード
  ECS-->>SFN: タスク完了
  SFN->>CB: 成功コールバック
  CB->>CB: セッションデータ更新

イメージ署名チェック

Step Functions はプローバータスク起動前にコンテナイメージの署名を検証し、承認されたイメージ以外の実行を拒否します。 署名と digest pin の運用は イメージ署名 を参照してください。

配布対象アーカイブの構築

非同期モードでは、ホストバイナリの出力のうち秘密データを含まないファイルだけを bundle.zip に同梱し、input.json などの秘密入力は含めません。 同梱対象の一覧、整合性検査ルール、取得経路は バンドル構造 を、public-input.json の項目と inputCommitment の関係は 入力コミットメント を参照してください。

async Docker entrypoint は、journal.json、public-input.json、election-manifest.json、close-statement.json を生成する際に methodVersion（現行 14）と inputCommitment の整合性を検査し、契約と一致しない host artifact は fail-closed で停止します。 非同期 S3 出力では、通常は次のオブジェクトが保存されます。

• ホスト生出力の *-output.json と *-receipt.json
• 生成済みの公開アーティファクト
• private bitmap sibling（included-bitmap.json / seen-bitmap.json。非公開のまま bundle.zip には同梱しない）
• bundle.zip

journal.json は bundle.zip の中に生成される公開アーティファクトであり、固定名の standalone journal.json は sibling object として保存しません。

entrypoint が非ゼロ終了した場合は、失敗分類だけを持つ private sibling artifact failure-marker.json を同じ finalization scope に best-effort で保存します。S3 object は sessions/{sessionId}/{finalizationId}/failure-marker.json という finalization identity に 従います（分類の制限、create-only 保存、finalization writer による検証などの契約は 非同期プローバー を参照）。

非同期モードの特性

開発モードの動作

dev-mode build のホストで RISC0_DEV_MODE=1 を設定すると、RISC Zero は STARK 証明を生成せず、フェイクレシートを返します。 フェイクレシートを作れるのは pnpm build:zkvm:dev-mode など dev mode を許可するホストビルドだけです。 production feature 有効のホスト（pnpm build:zkvm や Fargate prover image）は RISC0_DEV_MODE=1 を受理しません。非同期 prover の entrypoint は production proof profile （S3-backed 実行では RUNTIME_PROFILE=target-aws-async）を要求し、退役済みの RISC0_DEV_MODE / FORCE_DEV_MODE を host process の環境から除去します。

production receipt が証明するのは、対応する Image ID の guest が公開 journal を生成したことです。 これだけで投票システム全体の安全性、運用者に対する ballot secrecy、または選挙運用の妥当性まで 証明するものではありません。

開発モードのレシートは内部的には InnerReceipt::Fake 型です。 検証サービス では通常 dev_mode 扱いになります（image_id 不一致などの事前条件違反時のみ Failed）。 dev_mode は診断ステータスであり、本番モードの成功検証としては採用されません。

開発モードは次の用途に限定されます。

• host CLI や verifier 連携を含むローカルの高速フィードバック
• TypeScript と Rust の契約を短時間で確認する smoke test
• dev-mode receipt 分岐を明示的に通す CLI と E2E 検証

アプリケーションの proof executor は immutable な runtime profile が選択します。 mock 系 profile（local-demo / static-mock-e2e）の mock executor は、ホストバイナリも RISC Zero SDK も呼びません。profile ごとの proof evidence の対応は AWS runtime 境界 を参照してください。 USE_MOCK_ZKVM と server 設定としての RISC0_DEV_MODE は置換済み selector であり、 runtime profile の入力に混在させると fail-closed で拒否されます。なお、dev-mode 対応 host CLI を直接診断するときの RISC0_DEV_MODE=1 は、この application runtime selector とは 異なる低レベルの host 設定です。

検証サービス

この章では、STARK レシートを検証する Rust サービスの構造と、ローカルおよび Lambda での使い方を扱います。

検証サービスは、レシートの STARK 検証をサーバー側で実行し、結果をレポートとしてクライアントに提供する Rust コンポーネントです。

概要

STARK 証明の検証は証明生成に比べれば計算コストが低い処理で、本システムではサーバー側で検証を行い、その結果をレポートとしてクライアントに提供します（委任の理由と信頼境界は サーバー側検証の信頼境界 を参照）。

flowchart LR
  subgraph 入力
    RCP[レシート / バンドル]
    EID["期待 Image ID"]
  end

  RCP --> VS[検証サービス]
  EID --> VS
  VS --> RPT[検証レポート]

検証フロー

検証サービスは、次の手順でレシートを検証します。

flowchart TD
  START[レシート / バンドル読み込み] --> FORMAT{入力形式<br/>の判定}
  FORMAT -->|フラット JSON| F1[直接パース]
  FORMAT -->|ネスト JSON| F2[receipt フィールドを抽出]
  FORMAT -->|ディレクトリ| F3[receipt.json または<br/>*-receipt.json を探索]
  FORMAT -->|ZIP アーカイブ| F4[末尾が receipt.json のファイルを探索]
  F1 --> EXTRACT[Image ID 抽出]
  F2 --> EXTRACT
  F3 --> EXTRACT
  F4 --> EXTRACT

  EXTRACT --> MODE[InnerReceipt を判定<br/>Fake は dev_mode 候補として記録]
  MODE --> PRESENT{メタデータ image_id<br/>が存在?}
  PRESENT -->|欠落 + 非 Fake| FAIL0[failed]
  PRESENT -->|欠落 + Fake| VERIFY
  PRESENT -->|存在| MATCH{メタデータ Image ID<br/>= 期待 Image ID ?}
  MATCH -->|不一致| FAIL1[failed:<br/>Image ID 不一致]
  MATCH -->|一致| VERIFY["Receipt::verify(expected_image_id)<br/>STARK 検証実行"]
  VERIFY -->|成功 かつ Fake| DEVMODE[dev_mode]
  VERIFY -->|失敗 かつ Fake + InvalidProof| DEVMODE
  VERIFY -->|成功 かつ 非 Fake| SUCCESS[success]
  VERIFY -->|失敗（その他）| FAIL2[failed]

入力形式の解決

検証サービスは、単一のレシートファイルだけでなく、レシートを含むバンドルディレクトリや ZIP にも対応しています。 image_id はラッパーの top-level フィールドであり、レシート本体の内部フィールドではありません。 同期 finalization 経路では proof bundle ディレクトリ全体を渡し、その中の receipt.json を解決します。

Image ID 照合と Fake receipt の扱い

ラッパーの image_id は、開発モード生成を示す Fake 型（InnerReceipt）でも期待値との一致が必須であり、不一致なら failed として即時拒否します。 image_id が欠落した場合は、非 Fake 型は failed になり、Fake 型だけが Receipt::verify まで進んで結果に応じて dev_mode または failed に振り分けられます（分岐の全体は上のフローチャートを参照）。 Image ID の管理は Image ID を参照してください。

STARK 検証の実行

top-level の Image ID 照合に成功した後、または Fake 型で image_id が欠落している場合に、RISC Zero SDK の Receipt::verify(expected_image_id) でレシートを検証します。 検証成功は、次の内容を保証します。

• レシートに含まれる seal（証明データ）が有効
• ジャーナルが指定 Image ID のゲスト実行結果である
• 証明生成後にレシートが改ざんされていない

検証レポート

検証サービスは、検証が最後まで到達した試行について JSON レポートを出力します。 exit code とレポート出力の関係は次のとおりです。

呼び出し側は exit code とレポートの両方を見ます。 --quiet を指定すると stdout 出力は抑制されます。 その場合は --output も併せて指定し、レポートを保存します。

errors は固定のエラーコード一覧ではなく、実装が積む自由形式の診断文字列です。

ステータスの意味づけ

各ステータスが最終表示に与える影響は ゲーティングロジック > STARK 検証のゲーティング を参照してください。

デプロイメントモデル

検証サービス（Rust バイナリ verifier-service）は、呼び出し経路ごとに実行場所が異なります。

呼び出しパターン

検証サービスの呼び出しは 3 分類です。 明示的検証はいずれも、サーバー側で保持している finalization result に紐付いた 権威ある bundle locator だけを使います。 クライアントが任意の S3 キーや local パスを指定し、検証サービスに検証させることはできません。

S3 artifact backend は target profile 専用で、API が verification-worker Lambda を同期 invoke する non-target S3 経路や backend fallback はありません。

非同期 finalization のコールバック Lambda は、結果の復元と保存を担当します。 STARK 検証は自動実行されず、POST /api/sessions/:sessionId/finalizations/:finalizationId/verification で実行します。 target AWS runtime での流れは次のとおりです。

1. この POST は verifier-service の完了を待たず、verificationResult.status=running を保存して SQS work を発行する
2. verification-worker が SQS event を受け取り、S3 bundle を検査・展開して verifier-service を実行する
3. 検証が完了した場合は、verification.json の report locator と report を含む terminal verificationResult を finalization-scoped な独立 record としてセッションストアへ保存する
4. S3 の取得、bundle の検査、verifier-service の起動、artifact の upload などの infrastructure failure は SQS で再試行する
5. 3 回目の受信でも失敗した場合は terminal failed と internal-only の failureCategory を保存する。この終端失敗には verifier report がないため、report locator も保存しない

既存の verificationResult.status ごとの POST /api/sessions/:sessionId/finalizations/:finalizationId/verification の挙動は次のとおりです。

実行シーケンス（補足）

次のシーケンス図は、上記 3 分類の実行経路を補足するものです。

sequenceDiagram
  participant C as クライアント
  participant API as API サーバー
  participant Q as verification-work SQS
  participant RUNNER as verification-worker Lambda
  participant VS as verifier-service バイナリ
  participant S3 as S3
  participant STORE as セッションストア

  C->>API: POST /api/sessions/:sessionId/finalizations/:finalizationId/verification
  API->>API: session capability と finalization result を確認
  alt target AWS runtime + S3 bundle locator がある
    API->>STORE: verificationResult を running に更新
    API->>Q: 検証 work を送信（recordType, sessionId, finalizationId, queuedAtMs, bundleKey, expectedImageId）
    API-->>C: running
    Q-->>RUNNER: SQS event
    RUNNER->>S3: bundle.zip を取得・展開
    RUNNER->>VS: bundle ディレクトリ + 期待 Image ID + reportPath
    VS->>VS: STARK 検証実行 + verification.json 書き出し
    VS-->>RUNNER: 検証レポート
    RUNNER->>S3: public bundle.zip / verification.json / sidecar を保存
    RUNNER->>STORE: report locator と terminal verificationResult を保存
  else 信頼済み local bundle がある
    API->>VS: bundle ディレクトリ + 期待 Image ID + reportPath
    VS->>VS: STARK 検証実行 + verification.json 書き出し
    VS-->>API: 検証レポート
    API->>STORE: verificationResult / execution 状態を更新
    API-->>C: 検証結果
  end

検証パイプラインにおける役割

検証サービスは、4 段階検証モデルの最終段階である STARK 検証を担当します。

stark_image_id_match は、verifier report の expected_image_id と receipt_image_id が一致することを検証します。 検証パイプラインはさらに、claimed 側および comparison 側の Image ID とも整合することを確認します。

これらのチェックが両方成功した場合に限り、「STARK Verified」のステータスが付与されます。 これは STARK 検証段階のステータスであり、全体の Verified 判定とは区別されます。 詳細は 4 段階検証モデル を参照してください。

セキュリティ上の考慮事項

サーバー側検証の信頼境界

検証サービスはサーバー側で実行されるため、クライアントはサーバーの検証結果を信頼する必要があります。 この PoC における信頼モデルは次のとおりです。

• STARK 証明自体は秘密データを含まない検証データ: レシートと Image ID があれば、第三者が独立に検証可能
• 検証サービスは利便性のための委任: ブラウザ上で RISC Zero の検証ロジックを実行することは現時点では実用的でないため、サーバー側で検証する。実用的になれば、クライアント側のみで完結させることも理論上は可能
• 配布対象アーカイブ: レシートと public-input.json は ZIP ローカル検証（Ubuntu） の手順で独立検証できる

verification.json の非公開性

verification.json は bundle.zip に含めず、必要時のみ capability 保護の report エンドポイントで配布します（境界は 公開境界）。 第三者検証では、レシートファイルを直接使った独立検証が推奨されます。

Image ID

Image ID は、ゲストバイナリを一意に識別する値です。 検証時には、この値でレシートがどのゲストプログラムの実行結果かを照合します。

Image ID は、ゲストプログラムの ELF バイナリから決定的に導出される 256 ビットのハッシュ値です。 レシート検証時に期待値との一致を確認することで、レシートが正しいプログラムの実行結果であることを検証します。

RISC Zero の Image ID

RISC Zero zkVM では、ゲストプログラムの ELF バイナリが Image ID と呼ばれる 256 ビットの識別子に変換されます。 この変換は決定的であり、同一のバイナリからは常に同一の Image ID が生成されます。

Receipt::verify(image_id) は、レシートが指定した Image ID のゲスト実行結果であることを暗号学的に検証します。 期待する Image ID と一致しないレシートは拒否されます。 ラッパーメタデータとの照合手順は 検証サービス を参照してください。

flowchart LR
  ELF["ゲスト ELF バイナリ"] --> HASH["RISC Zero<br/>Image ID 導出"]
  HASH --> IID["Image ID<br/>(256 ビット)"]

  IID --> EMBED["ホストバイナリに埋め込み"]
  IID --> MAP["マッピングファイルに記録"]
  IID --> VS["検証サービスの期待値"]

Image ID の導出

Image ID は RISC Zero のビルドシステムによってコンパイル時に自動生成されます。

Image ID が変わる要因

同一のゲストソースコードであっても、以下の要因により異なる Image ID が生成され得ます:

variant とアーキテクチャ

本システムでは、同一バージョンのゲストに対して default と x86_64 の 2 つの variant authority をマッピング上で管理します。 各 authority は次の排他的な状態です。

• state: "confirmed": imageId と由来を示す provenance を持つ
• state: "unconfirmed": requiredEvidence: "accepted-prover-release" だけを持ち、Image ID として解決できない

app deployment では、選択された prover release metadata から Image ID と methodVersion を導出し、mapping は互換性と公開台帳の証拠として照合します。 public/imageId-mapping.json は公開検証者が expected Image ID を解決するための互換性台帳であり、prover image digest の承認 authority ではありません。 ECR digest と Image ID / methodVersion の組み合わせは、選択された prover release record と app deployment record で固定します（candidate metadata から app deployment record までの chain は イメージ署名 を参照）。

現行実装では、実行環境を自動判定して x86_64 を選びません。 未指定時は default variant を選択します。 選択した variant が unconfirmed なら fail-closed で停止し、もう一方へフォールバックしません。 x86_64 用の値を使うには、アプリ側で EXPECTED_IMAGE_ID_VARIANT=x86_64 を設定するか、呼び出し側で variant を明示します。 variant 選択と EXPECTED_IMAGE_ID オーバーライドの優先順位は、下の Image ID の解決 を参照してください。

Image ID マッピング

期待される Image ID は、バージョンごとにマッピングファイルで管理されます。

マッピングファイルの構造

マッピングファイルには、各バージョンの variant authority、説明、機能リストを記録します。

current と deprecated の扱い

マッピングファイルは、現在信頼するバージョンと、必要な場合に限って非推奨バージョンを保持します。 current フィールドは現在有効なバージョンを指し、deprecated フィールドは過去のバージョンを列挙します。 全 method mapping は両 variant の authority を持ちますが、両方が confirmed とは限りません。

現行実装では current は 14 で、deprecated は空です。 明示的な trust rotation により v13 以下の mapping は削除されており、現行 mapping からは解決できません。 v14 の mapping は variants.default と variants.x86_64 を保持します。

flowchart LR
  CUR["current v14<br/>(default + x86_64 authority)"]
  DEP["deprecated<br/>(現在は空)"]
  CUR -. version up .-> DEP

Image ID の解決

検証時に使用する期待 Image ID の決定方法は、EXPECTED_IMAGE_ID の有無で分かれます。 EXPECTED_IMAGE_ID が設定されている場合は、その値を使用します。 設定されていない場合は、methodVersion と variant を使ってマッピングから解決します。

flowchart TD
  START[Image ID 解決] --> P1{EXPECTED_IMAGE_ID?}
  P1 -->|設定済み| USE1[その値を採用]
  P1 -->|未設定| P2[マッピングから解決]
  P2 --> P3{variant?}
  P3 -->|default| F1[variants.default]
  P3 -->|x86_64| F2[variants.x86_64]
  F1 --> CHK[fail-closed 条件を適用]
  F2 --> CHK

version 選択

• EXPECTED_IMAGE_ID 環境変数は最優先のオーバーライドです。 設定されている場合は mapping と variant による解決を行わず、その値を期待 Image ID として採用します。 運用者は、この値が対象 methodVersion のデプロイ済みゲスト Image ID と一致することを別途保証する必要があります。 不一致なら stark_image_id_match または stark_receipt_verify が失敗します。
• resolveExpectedImageId() / POST /api/sessions/:sessionId/finalizations/:finalizationId/verification の version 選択は、省略時はマッピングの current を使用し、明示時は CURRENT_METHOD_VERSION と一致する場合のみ受理します（deprecated 側は拒否）。
• 低レベルのマッピング読み取り API は、mapping に保持されている version だけを明示的に解決できます。 現行 mapping には v13 以下が存在しないため、それらも fail-closed で拒否します。
• 現行の検証実行フローでは、正規化済みのジャーナルから methodVersion を取得して resolveExpectedImageId(methodVersion) を呼びます（public-input.json フォールバックは現行未使用）。

variant 選択

• variant は EXPECTED_IMAGE_ID_VARIANT（default または x86_64）または呼び出し側の明示 option で選択し、未指定時は default です。 それ以外の値は受け付けません。
• app deployment flow（default / ARM64 trust material）では、variant 未指定の default を使用します。
• ローカル / CI フロー（x86_64 trust material）では、EXPECTED_IMAGE_ID_VARIANT=x86_64 を明示します。 verifier-service 単体は EXPECTED_IMAGE_ID_VARIANT を直接読みません。 第三者検証では read-image-id.mjs --variant x86_64 または同スクリプト実行時の EXPECTED_IMAGE_ID_VARIANT=x86_64 で EXPECTED_IMAGE_ID を導出し、verifier-service に渡します。

fail-closed 条件

未対応 methodVersion、マッピング読み込み失敗、unsupported variant、選択した variant が unconfirmed、または authority の形が不正な場合は、いずれも暗黙のフォールバックを行わず fail-closed でエラーになります。

検証パイプラインでの役割

Image ID は 4 段階検証モデルの STARK 検証段階で使用されます。

Image ID 関連チェック

現行実装では、STARK 検証段階で次の 2 つの必須チェックが Image ID に関与します。

• stark_image_id_match: receipt.json ラッパーの image_id と期待値を照合する
• stark_receipt_verify: 同じ期待 Image ID を使って Receipt::verify(expected_image_id) を実行する

詳細は 検証サービス を参照してください。

Image ID が不一致の場合は、以下のいずれかの状況が考えられます:

Image ID が一致していても、RISC0_DEV_MODE=1 の dev-mode receipt（フェイクレシート）は production STARK proof として扱いません（生成側は ホストと証明生成、判定側は ゲーティングロジック を参照）。

Image ID 更新時の手順

ゲストプログラムを変更した場合、Image ID を更新する必要があります。

1. ゲスト変更と authority schema を Commit A に入れ、target default を unconfirmed にする
2. 管理された Prover lane でイメージを 1 回ビルドし、push 前後の host --print-image-id --json が一致することを確認して release を昇格する（candidate build と promotion の AWS 側の詳細は イメージ署名 を参照）
3. accepted Prover release の immutable key / VersionId / body SHA-256 を確認する
4. Commit B で default を confirmed にし、accepted release の Image ID、image digest、candidate/release/Toolchain record checksum を provenance に記録する
5. Foundation と App の saved-plan lane で Commit B を反映する。App は Prover release の zkvmContractHash と App source の再計算値も照合する

--json を付けると {"imageId":"0x...","methodVersion":14} の形で出力されます。

同一リリースで同期するもの

Image ID / methodVersion が変わる場合は、Prover release record と Commit B の imageId-mapping.json を同じ昇格系列で結びます。 Commit A の unconfirmed 期間は意図的に App deployment が停止します。 片方だけをデプロイ可能な状態にするフォールバックはありません。 一方で、entrypoint だけの prover container rebuild のように guest Image ID が変わらない変更では、ECR digest は変わっても mapping を更新する必要はありません。

• 通常の POST /api/sessions/:sessionId/finalizations/:finalizationId/verification フローでは、現行の journal contract のみ受け付ける
• 旧成果物は Image ID 照合に進む前に、未対応の journal contract として失敗し得る
• DEFAULT_POC_IMAGE_ID はテスト用定数で、期待 Image ID の解決経路には現れない（マッピングが source of truth）

信頼アンカーとしての位置づけ

Image ID は、zkVM の信頼モデルにおける信頼アンカーです。

• Image ID を知っている検証者は、対象ゲストプログラムの実行を検証できる: レシートが有効であれば、そのロジックが実行されたことを確認できる
• Image ID の管理が破綻すると、検証の信頼性が失われる: 攻撃者が独自のゲストプログラムで有効なレシートを生成し、その Image ID がマッピングに混入すると、不正な集計が「検証済み」として受理され得る

マッピングファイルは公開リポジトリにコミットされ、変更履歴を追跡できます。 AWS 構成では、イメージ署名検証と組み合わせることで、承認されたプローバーイメージだけを使用する設計です。 イメージ署名の詳細は イメージ署名 を参照してください。

検証パイプライン

この部では、投票の完全性を 4 段階に分けて検証するパイプラインを扱います。

この部の前提となる原則は次の 4 点です。

• 最終的な Verified 判定は fail-closed で、required check が失敗、未実行、保留中、実行中のまま残る場合は successful overall result になりません。verificationStatus や stark_receipt_verify は STARK receipt verification の信号にすぎず、単独で overall verdict を表しません（ゲーティングロジック）。
• 判定確定後に送る POST /api/sessions/:sessionId/finalizations/:finalizationId/verification/observations は observability 専用で、送信の成否が verdict を変更することはありません（設計と実行フロー）。
• public bundle.zip は保護対象 artifact を含まない監査用アーカイブで、public は無認証公開を意味しません（境界の正本は 公開境界）。
• RISC0_DEV_MODE=1 の receipt は production STARK proof ではありません。

この部の章

読み順は次のとおりです。

• 設計と実行フロー：設計原則、パイプライン構造、実行フロー、判定確定後の observability
• 4 段階検証モデル：検証の全体設計と各段階の保証
• チェック一覧：全検証チェック ID とその判定ロジック
• ゲーティングロジック：「Verified」表示の条件と不変条件
• 公開境界：public bundle.zip と protected report artifact の境界
• バンドル構造：証明バンドルの公開可能なアーティファクトと非公開アーティファクト

想定読者と前提

• 想定読者：/verify 画面の最終判定ロジックを把握したい監査者と実装者
• 前提：暗号プロトコル と zkVM 設計 の概要を読み終えていること

この部で扱わないもの

• bundle.zip のローカル監査手順（第三者検証ガイド を参照）
• 改ざんシナリオごとの検出表（改ざんシナリオ を参照）
• UI コンポーネントや Storybook 配置の詳細

関連する章

• 暗号プロトコル：チェック対象となるプリミティブ
• zkVM 設計：ジャーナルとレシートの構造
• 改ざんシナリオ：どのチェックがどの改ざんを検出するか
• 可観測性設計：verdict authority と判定後 observation の分離
• 第三者検証ガイド：bundle.zip を使ったローカル監査
• 用語集：チェック種別とゲーティング用語の定義

設計と実行フロー

この章では、検証パイプラインの設計原則と、リクエストから判定までの実行フローを説明します。

設計原則

本システムの検証パイプラインは、5 つの原則に基づいています。

原則 1: 必要な検証が未実行なら Verified を表示しない

required チェックが not_run（未実行）、pending（依存待ち）、running（実行中）のいずれかにある場合、システムは「Verified」を表示しません。 証拠の不在や未解決状態は成功として扱いません。

原則 2: 失敗した検証は即座にブロックする

いずれかの必須チェックが失敗すれば、「Verified」表示は即座にブロックされます。 代表的な失敗条件は次のとおりです。

• excludedSlots > 0（除外されたスロットが存在する）
• 整合性証明の失敗
• 公開監査アーティファクトとの不一致
• 第三者 STH 合意の不成立（設定時）

原則 3: チェック評価と集約の責務を分ける

チェック評価はサーバーが担い（GET /api/sessions/:sessionId/finalizations/:finalizationId/verification が Stage 2-4 を評価し、STARK 検証は同じ resource への POST で実行）、Cast-as-Intended のローカル再評価と最終判定の集約はクライアントが担います。 集約ルールと最終判定の決まり方は ゲーティングロジック を参照してください。

原則 4: evidence の取得・admission と評価を分ける

provider 選択、URL fetch、capability 付与、store read、外部 response の strict admission、transport/unavailable/malformed の分類は application/API の acquisition boundary が担います。verification evaluator は admission 済みの consistency proof、 STH result、bitmap material、session/finalization authority を受け取り、transport や credential を解決しません。

取得失敗を成功相当の空値に変換せず、閉じた unavailable/corrupt または check status へ fail-closed に写像することで、I/O と暗号・整合性評価を独立に検査できます。

原則 5: proof authority と presentation を分ける

proofAuthority、included journal、公開監査 artifact は検証根拠です。 claimed tally、scenario、tamper 表示、shared policy result は presentation として分離し、authority から導出または照合します。 presentation の都合で proof-bound data を書き換えず、両者が不一致なら published_tally_mismatch などの失敗として表示します。

検証パイプラインの全体構造

パイプラインは Stage 1（Cast-as-Intended）→ Stage 2（Recorded-as-Cast）→ Stage 3（Counted-as-Recorded）→ Stage 4（STARK Verification）→ 結果表示の順に評価されます。

実行責務

GET /api/sessions/:sessionId/finalizations/:finalizationId/verification は 22 チェックのレスポンスを組み立てます。

• 評価対象: サーバーは Stage 2-4 の 18 チェックを評価し、Cast-as-Intended の 4 チェックは not_run で返します。クライアントがローカル再評価で上書きします。summary の導出（deriveVerificationSummary）はサーバー側の verification resource とクライアント側の /verify の両方で使われます。
• 200 + fail-closed のケース:
  • Recorded-as-Cast は cast-time 証跡（voteReceipt と userVote.proof）を前提とします。exact proof を store から取得できない場合でも verification resource は 200 を返し、voterEvidence.availability = "unavailable" と関連チェックの not_run によって全体判定を missing_evidence 側へ倒します。flat field や不完全な proof への fallback はありません。
  • userVote.proof.treeSize など exact voter evidence 側の必要データが不在のときは、関連チェックを not_run に補正します。
  • サーバーは verificationStatus を fail-closed に補正します。unsupported な verifier status でも verificationSteps / verificationChecks を含む 200 応答を返します。
• corrupt のケース: journal は成功済み finalization の必須 authority です。不在または malformed なら check 単位に修復せず、corrupt として fail-closed に扱います。

flowchart TD
  subgraph SERVER["サーバー側"]
    VFY["GET .../finalizations/:finalizationId/verification<br/>Stage 2-4 を評価<br/>Cast は not_run（クライアント再評価）"]
    RUN["POST .../finalizations/:finalizationId/verification<br/>bundle 参照と expected Image ID で<br/>Stage 4 を検証"]
    OBS["POST .../verification/observations<br/>（非ゲート観測）"]
  end

  subgraph CLIENT["クライアント（UI）"]
    UI["Cast のローカル再評価<br/>STARK 解決後に step 表示を開始<br/>明示的 failure / hard-failure override / summary / pending から最終判定"]
  end

  VFY --> UI
  RUN --> UI
  UI -. "判定確定後に送信（非ゲート）" .-> OBS

検証の実行フロー

検証導線では通常、/result から /verify へ進みます。

1. /result は正準な finalization snapshot をクライアント状態に保存します。 「検証へ進む」を押すと verificationRequestedAt を保存し、必要なら POST /api/sessions/:sessionId/finalizations/:finalizationId/verification を非同期に先行起動します（完了を待たずに /verify へ遷移します）。
2. /verify はその継続状態がある場合に検証シーケンスを続行します。 STARK が未開始ならシーケンス内で起動できます。
3. 継続状態がなく STARK が not_run のまま直接 /verify へアクセスした場合は、自動続行せずブロックします
4. /verify の UI シーケンスは、step を順に見せる前に STARK が terminal status に到達するまでポーリングします。 timeout や transport failure は STARK failure として扱われます。
5. UI の最終判定が確定し、pending check がなく、server response が検証済みで、STARK status が terminal なら、/verify は POST /api/sessions/:sessionId/finalizations/:finalizationId/verification/observations を best-effort で送信します。 current finalizationId は path authority であり、body に identity を重複させません。strict body は 4 個の browser-local Cast check status だけを持ちます。この事後観測は表示済みの verdict を gate または変更せず、送信失敗も検証失敗として扱いません。 リクエスト内容と authority 規則は API エンドポイント を参照してください。

継続判定に使うクライアント状態キーの視点は セッションライフサイクル を参照してください。

sequenceDiagram
  participant U as ブラウザ
  participant R as /result
  participant V as /verify
  participant A as API サーバー
  participant VS as 検証サービス

  Note over R: finalization snapshot は /result 表示時に保存済み
  U->>R: 「検証へ進む」をクリック
  R->>R: verificationRequestedAt を保存
  R->>A: POST .../finalizations/:finalizationId/verification（fire-and-forget）
  R-->>V: /verify へ遷移（run 完了は待たない）

  Note over V: /verify 到達時に未開始なら<br/>同じ finalization-scoped POST を起動

  A->>VS: bundle 参照 + expected Image ID
  VS->>VS: Receipt::verify(image_id)
  VS-->>A: 検証レポート保存

  loop STARK 完了までポーリング
    V->>A: GET .../finalizations/:finalizationId/verification
    A-->>V: 検証ペイロード<br/>(ステップ, チェック, 証明材料)
  end

  Note over V: 継続には verificationRequestedAt と finalization snapshot が必要<br/>not_run の direct access はブロック<br/>step 表示は STARK 解決後に開始
  V-->>U: ローカル Cast check を含む最終判定を表示

  opt 判定確定後の observability
    V->>A: POST .../verification/observations（非ゲート）
    A-->>V: recorded または idempotent
  end

4 段階の概要

各段階が何を証明するかは 4 段階検証モデル を参照してください。 この章の観点で重要なのは、検証の実行場所が段階ごとに異なることです。

各ステージの導出ルール（required チェック群からの集約、STH source 設定時の昇格、ガード条件）は ゲーティングロジック を参照してください。

検証チェック数

パイプライン全体で 22 個の検証チェックが定義されており、各チェックには一意の ID が割り当てられています。 チェック ID の単一ソースは packages/verification/src/verification/verification-checks.ts です。

各チェックの重要度（required / optional）と判定ロジックは チェック一覧 を参照してください。

4 段階検証モデル

この章では、E2E 検証可能投票の各段階（Cast-as-Intended / Recorded-as-Cast / Counted-as-Recorded / STARK Verification）で成立する保証を説明します。

段階間の依存関係

概念モデルでは 4 段階を順に評価します。 ただし、実行場所は段階ごとに異なります。 Stage 1 はクライアントで実行し、Stage 2 から Stage 4 はサーバー中心で実行します。 実行責務の詳細は 設計と実行フロー を参照してください。

flowchart LR
  subgraph "証拠の生成"
    V["投票時<br/>投票レシート発行"]
    F["集計時<br/>zkVM 実行"]
  end

  subgraph "4 段階検証"
    S1["Stage 1<br/>Cast-as-Intended"]
    S2["Stage 2<br/>Recorded-as-Cast"]
    S3["Stage 3<br/>Counted-as-Recorded"]
    S4["Stage 4<br/>STARK Verification"]
  end

  V --> S1
  V --> S2
  F --> S3
  F --> S4

  S1 ~~~ S2
  S2 ~~~ S3
  S3 ~~~ S4

Stage 1: Cast-as-Intended

目的

投票者が意図した選択肢のコミットメントが、サーバーから返却された投票レシートと一致することを確認します。 この確認により、サーバーが投票者の選択を差し替える攻撃を検出します。

検証する内容

/verify 画面のクライアントコードがローカルに保持された 3 つの値（選挙 ID、選択肢、乱数）からコミットメントを再計算し、投票レシートのコミットメント値と照合します。 再計算の規則（ドメインタグ、正準フォーマット）は コミットメントスキーム を参照してください。

flowchart LR
  subgraph "投票時に確定したデータ"
    EID[選挙 ID]
    CH[選択肢]
    RND[乱数]
  end

  subgraph "再計算"
    HASH["SHA-256<br/>(ドメインタグ || 選挙ID || 選択肢 || 乱数)"]
  end

  subgraph "照合"
    CMP{"一致?"}
    REC[投票レシートの<br/>コミットメント]
  end

  EID --> HASH
  CH --> HASH
  RND --> HASH
  HASH --> CMP
  REC --> CMP

必要な証拠

選挙 ID、選択肢、乱数はクライアントセッション（localStorage.starkBallotSession）に保持されます。 投票レシートは capability で保護された GET /api/sessions/:sessionId/finalizations/:finalizationId/verification 応答の data.voterEvidence が availability: "available" のときに、その voteReceipt から取得します。

cast-time 証跡を再構成できない場合、data.voterEvidence は availability: "unavailable" と reason を返し、投票レシートは得られません（取得と fail-closed 挙動の正本は 設計と実行フロー）。

失敗モード

限界

この段階は投票者の手元データに依存します。 そのため、localStorage 消去後や別端末からは検証できません。

Stage 2: Recorded-as-Cast

目的

投票者のコミットメントが、追記専用の掲示板（CT Merkle ツリー）に正しく記録されていることを確認します。 さらに、掲示板が追記専用性を維持していることを検証します。 つまり、過去のエントリが削除や改変を受けていないことを確認します。 掲示板のツリー構造とハッシュ規則は CT Merkle ツリー を参照してください。

検証する内容

この段階には 3 系統の検証があります。

flowchart TB
  subgraph "2a: 包含証明"
    IP["包含証明の検証<br/>自分のコミットメントが<br/>ツリーに存在するか"]
  end

  subgraph "2b: 整合性証明"
    CP["整合性証明の検証<br/>投票時のルートから<br/>最終ルートへの追記専用性"]
  end

  subgraph "2c: 第三者 STH 検証"
    STH["STH 合意の検証<br/>独立したソース間で<br/>ツリー状態が一致するか"]
  end

  IP --> RESULT{"Recorded 系の証拠を総合評価"}
  CP --> RESULT
  STH --> RESULT

2a: 包含証明（Inclusion Proof）

RFC 6962 の PATH 関数に基づく CT スタイルの Merkle 包含証明を検証し、投票者のコミットメントが掲示板のツリーに含まれていることを確認します。 検証者はリーフハッシュと Merkle パスからルートハッシュを再計算し、期待されるルートと照合します。

2b: 整合性証明（Consistency Proof）

投票時点のツリー状態（ルートとサイズ）から、最終的なツリー状態への遷移が追記のみで行われたことを検証します。 RFC 6962 の SUBPROOF アルゴリズムに基づく整合性証明により、サーバーが過去のエントリを密かに削除したり順序を変更したりするスプリットビュー攻撃を検出します。

2c: 第三者 STH 検証（オプション）

複数の独立した STH（Signed Tree Head）ソースに問い合わせ、合意が成立しているかを確認します。 この確認により、サーバーが検証者ごとに異なるツリー状態を提示するスプリットビュー攻撃を検出します。 照合対象となるダイジェストの構成は STH ダイジェスト を、照合条件の詳細は チェック一覧 を参照してください。

必要な証拠

Recorded の検証リソースは GET /api/sessions/:sessionId/finalizations/:finalizationId/verification の data です。

cast-time 証跡（voteReceipt と、oldSize を与える userVote.proof.treeSize）を再構成できない場合、Recorded の必須チェックは not_run となり、全体判定は fail-closed で missing_evidence 側へ倒れます。 取得と admission の分離は 設計原則 4 を、check 単位の判定は チェック一覧 を参照してください。

失敗モード

Stage 3: Counted-as-Recorded

目的

掲示板に記録された全投票が、zkVM の集計処理に正しく含まれたことを確認します。 投票の除外、欠落、重複がないことも確認します。 さらに、公開された claimed tally（表示用集計値）が zkVM の verifiedTally と一致することを検証し、集計結果の完全性と整合性を保証します。

検証する内容

この段階では 10 個の required チェックが全て success であることを要求します。 導出ルールと journal 省略時のガード補正は ゲーティングロジック を参照してください。

1 つでも success でないチェックが残る場合、Counted は成功にならず、Verified をブロックします。

必要な証拠

公開入力サマリーはサーバー内部表現であり、レスポンスにそのまま含まれません。 inputCommitment が束縛するのは public-input.json の部分集合です。 通常応答で proof-bound な値は data.proofAuthority、claimed tally は data.presentation.tally に分離され、旧 flat field への fallback はありません。 各チェックの判定ロジックは チェック一覧 を参照してください。

重要な判定: 除外数（excludedSlots）

excludedSlots > 0 はハード失敗であり、全体の検証成功を阻止します。 除外数の解決順序と legacy aliases の扱いは チェック一覧の counted_missing_indices_zero を、全体判定への影響は ゲーティングロジック を参照してください。

失敗モード

Stage 4: STARK Verification

目的

zkVM の実行が正しく行われたことを STARK 証明（レシート）の暗号学的検証により確認します。 レシートの検証に成功すれば、ジャーナルの内容（集計結果、除外情報、入力コミットメント等）がゲストプログラムの正しい実行の結果であることが保証されます。

検証する内容

flowchart LR
  subgraph "入力"
    RCP[レシート<br/>Seal + Journal]
    EID[期待 Image ID]
  end

  subgraph "Rust 検証サービス"
    VF["Receipt::verify(image_id)"]
  end

  subgraph "結果"
    OK["success<br/>暗号学的に検証済み"]
    NG["failed<br/>証明が無効"]
    DM["dev_mode<br/>フェイクレシート"]
  end

  RCP --> VF
  EID --> VF
  VF --> OK
  VF --> NG
  VF --> DM

検証の 2 段階

STARK Verification では 2 つのチェックを実行します。

Image ID 照合: verifier-confirmed な receipt_image_id が期待 Image ID と一致し、ホスト主張値（imageId）や comparison-only の journal.imageId とも矛盾しないことを確認します。 Image ID はゲストプログラムから導出される暗号的識別子であり、プログラムの改変やホスト主張値の食い違いを検出します。 解決順の詳細は チェック一覧 を参照してください。

レシート検証: RISC Zero の Receipt::verify(image_id) を呼び出し、Seal（STARK 証明）がジャーナルと Image ID に対して暗号学的に正当であることを検証します。 この検証は計算量が多いため、サーバー側の Rust 検証サービスで実行されます。

必要な証拠

開発モードの検出

RISC0_DEV_MODE=1 で生成された dev-mode receipt はフェイクレシートであり、本物の STARK 証明ではありません。 dev_mode ステータスの検出、正規化、Demo Only（demo_only）表示のルールは ゲーティングロジック を参照してください。 profile ごとの帰結は次節の失敗モード表にまとめています。

失敗モードと非 production evidence

UI ステップの対応チェック、集約ルール、最終判定の決定方法は ゲーティングロジック を参照してください。

チェック一覧

全検証チェック ID の定義、判定ロジック、失敗時の影響を一覧で示します。

各チェックは一意の ID を持ち、success / failed / not_run / running / pending のステータスで管理されます。 required チェックが not_run / running / pending のまま残っている場合、「Verified」は表示されません。 optional チェックの取り扱いは ゲーティングロジック を参照してください。

チェックの属性

各チェックには以下の属性が定義されています。

証拠種別

現行 22 チェックで使う証拠種別は次のとおりです。

定義上のチェックは local / public / zk のいずれかを持ちます。 RISC0_DEV_MODE=1 の receipt が明示的に許可された場合だけ、表示用のチェック結果で zk 証拠が demo に置き換えられます（正規化と表示のルールは ゲーティングロジック）。 demo 証拠は demo_only 扱いであり、production STARK proof としての Verified にはなりません。

重要度

代表例は recorded_sth_third_party です。

注意: verificationChecks と UI 表示用の verificationSteps は 1 対 1 ではありません。 対応関係は ゲーティングロジック を参照してください。

全チェック早見表

Cast-as-Intended（4 チェック）

投票者の意図通りにコミットメントが生成されたかを検証するチェック群です。 ブラウザはこのカテゴリを、capability 保護された GET /api/sessions/:sessionId/finalizations/:finalizationId/verification の voterEvidence が available の場合に得られる voteReceipt と、保存済みのローカル投票意図 （electionId / myVote / myRand）から評価します。API 応答上の Cast チェックは いったん not_run とし、ブラウザがローカルで再計算した結果を overlay します。

判定ロジックの詳細

cast_receipt_present

voteReceipt が存在し、voteId と commitment フィールドが存在することを確認します。 このチェック単体では UUID/hex 形式までは検証しません。

cast_choice_range

投票時データの選択肢が A〜E のいずれかであることを確認します。 範囲外の値は不正な入力として failed となります。

cast_random_format

投票時データの乱数が 32 バイト（64 文字）の 16 進数文字列であることを確認します。 0x プレフィックスの有無は正規化により吸収されます。

cast_commitment_match

投票時データから再計算した投票コミットメントが投票レシートの commitment 値と一致することを確認します。 再計算規則（ドメインタグ、正準フォーマット）は コミットメントスキーム を参照してください。

Recorded-as-Cast（6 チェック）

コミットメントが掲示板に正しく記録されたかを検証するチェック群です。

判定ロジックの詳細

recorded_inclusion_proof と recorded_consistency_proof は cast-time 証跡（voteReceipt と userVote.proof）の存在を前提とします。 両チェックは、まず cast snapshot の一貫性（leafIndex、treeSize、bulletinRootAtCast が receipt と矛盾しないこと）を確認してから個別の検証に進みます。 証跡が揃わない場合はどちらも not_run となり、全体判定は fail-closed で missing_evidence 側へ倒れます。

recorded_commitment_in_bulletin

包含証明（recorded_inclusion_proof）の結果から派生します。 包含証明が成功すれば、コミットメントがツリーに存在することが暗号学的に証明されています。

recorded_index_in_range

掲示板インデックスが 0 <= index < treeSize の範囲内であることを確認します。 範囲外のインデックスは、データの不整合を示します。

recorded_root_at_cast_consistent

整合性証明（recorded_consistency_proof）の結果から派生します。 整合性証明が成功すれば、投票時のルートが最終ツリーの有効な追記専用プレフィックスであることが証明されています。

recorded_inclusion_proof

投票者のコミットメントに対する RFC 6962 包含証明（Merkle パス）を検証します。 リーフハッシュと Merkle パスから cast 時点のルートを再計算し、receipt の bulletinRootAtCast と一致することを確認します。 proof の treeSize が voteReceipt.bulletinIndex + 1 と一致しない場合は failed です。

recorded_consistency_proof

投票時のツリー（oldSize, oldRoot）から最終ツリー（newSize, newRoot）への RFC 6962 整合性証明を検証します。 evidence の取得と admission は acquisition boundary が担います（設計原則 4）。判定条件は次のとおりです。

• evidence の old/new 両時点の tree size と root が、receipt / 最終 bulletin authority の期待値と一致すること
• 投票時ルートが最終ツリーの追記専用プレフィックスであること
• treeSize チェックは包含証明と同条件
• evidence が unavailable の場合は not_run、malformed または transport_failed の場合は failed

recorded_sth_third_party

設定された STH ソースからスナップショットを取得し、比較可能な応答同士で合意を確認します。 判定は matchingSources >= minMatches（デフォルト: 2）に加えて、比較対象になった応答間の全会一致（consensus）が必要です。 照合対象は STH ダイジェストが必須で、bulletinRoot / treeSize は各ソースが返した場合に追加で照合されます。 STH ソースが未設定の場合は not_run になります。

早見表では optional ですが、STH ソース設定時は required 相当に昇格します（昇格ルールはゲーティングロジックが定めます）。

Counted-as-Recorded（10 チェック）

記録された全投票が正しく集計に含まれたかを検証するチェック群です。

判定ロジックの詳細

counted_input_sanity

public-input.json 相当から組み立てた公開入力サマリーが存在し、スキーマ検証に成功していることを確認します。 さらに、treeSize が正の整数、votesCount <= treeSize、bulletinRoot が 32 バイト hex かつゼロ値でないことを要求します。

counted_unique_indices

zkVM に渡された全投票のインデックスが重複なく一意であることを確認します。 重複インデックスは、同一投票の二重カウントを示す可能性があります。

counted_unique_commitments

zkVM に渡された全投票のコミットメントが重複なく一意であることを確認します。 重複コミットメントは、同一コミットメントに対する複数投票を示す可能性があります。

counted_tally_consistent

ジャーナルが存在し、journal.totalVotes が 0 の場合は、zkVM が投票を 1 件も処理していないため failed とします。

主経路では、公開される claimed tally（tally.counts）が zkVM の verifiedTally と選択肢ごとに一致し、かつ verifiedTally の合計が tally.totalVotes と一致することを確認します。 これにより「公開表示された集計値」と「zkVM が証明した集計値」の不一致を検出します。 claimed tally が利用できない場合は、フォールバックとして journal.verifiedTally の合計と journal.validVotes の一致を検証します。

counted_missing_indices_zero

fail-closed（安全側に倒す）な除外数が 0 であることを確認します。 除外数は次の優先順で解決し、0 でなければ即座に failed とします。

1. journal がある場合: journal.excludedSlots を proof-bound な除外数として使用し、excludedSlots / missingSlots / invalidPresentedSlots / validVotes が非負整数であることも先に確認する
2. journal がない場合: excludedSlots → missingSlots + invalidPresentedSlots の順で探索

rejectedRecords は説明用の補助値で、この判定には使いません。 旧フィールド (excludedCount / missingIndices / invalidIndices) は fail-closed 補正経路でのみ参照され、本判定では使用しません。

counted_expected_vs_tree_size

totalExpected（期待される投票数）が掲示板のツリーサイズと一致することを確認します。 不一致は、暗黙の投票除外を示す可能性があります。

counted_election_manifest_consistent

election-manifest.json の electionConfigHash を再計算し、manifest 自身の宣言値と一致することを確認します。 そのうえで electionId と electionConfigHash を、セッション値、publicInputArtifact を厳密に admit して得た内部 publicInputAuthority、ジャーナルに含まれる対応値と相互照合します。

counted_close_statement_consistent

close-statement.json から sthDigest を再計算し、宣言された snapshot と一致することを確認します。 そのうえで timestamp が、publicInputArtifact を厳密に admit して得た内部 publicInputAuthority.timestamp と一致することを確認します。 さらに logId / treeSize / bulletinRoot / sthDigest が、検証入力やジャーナルと矛盾しないことを確認します。

counted_my_vote_included

includedBitmapRoot に対する bitmap Merkle 証明を検証し、投票者のインデックスに対応するビットが 1（counted に含まれた）であることを確認します。

verification handler は対象 finalization の included proof evidence と、seenBitmapRoot がある場合の seen proof evidence を取得・admit してから evaluator に渡します。両方の evidence がある場合は、 presented but invalid / not presented to the prover / unknown excluded を説明可能にします。 owner-scoped な proof building block の現行 endpoint は GET /api/sessions/:sessionId/finalizations/current/bitmap-proofs/:kind/:voteIndex です。

証明材料が取得できない場合は not_run になり、補助 note が付くことがあります。

counted_input_commitment_match

公開入力から再構成した入力コミットメントが、zkVM ジャーナルの値と一致することを確認します。 対象フィールドの集合と正準エンコーディングは 入力コミットメント を参照してください。 public-input.json 全体の単純なハッシュではない点に注意してください。

STARK Verification（2 チェック）

STARK 証明の暗号学的正当性を検証するチェック群です。

判定ロジックの詳細

stark_image_id_match

STARK status が success に解決された後で、期待 Image ID、verifier-confirmed Image ID、ホスト主張値が相互に矛盾しないことを確認します。 期待 Image ID を解決できない場合は、暗黙にフォールバックせず fail-closed で失敗します。 解決順と variant の指定規則、整合条件（report に Image ID フィールドが揃わない場合の挙動を含む）は Image ID を参照してください。

stark_receipt_verify

サーバー側の Rust 検証サービスが Receipt::verify(image_id) を実行し、Seal（STARK 証明）が暗号学的に正当であることを確認します。 チェック結果は success / failed / not_run / running で表現され、dev_mode は ゲーティングロジック に従って正規化されます（証拠種別 を参照）。

チェックステータスの解決

チェックごとの永続的な状態機械は持ちません。evaluator はその時点で admit 済みの入力と 依存する STARK status から各チェックの snapshot status を再計算します。そのため、証拠の取得や 検証結果の更新により、not_run または pending から success / failed へ直接解決する ことがあります。

全体判定（集約結果）の決まり方は ゲーティングロジック を参照してください。

ゲーティングロジック

この章は、「Verified」を表示してよい条件と、表示を必ず阻止する不変条件を定義します。

「必要な検証が未実行または失敗なら Verified を表示しない」という原則のもと、各チェックの結果がどう最終判定に集約されるかを定式化します。

この章での Verified は、UI の最終表示が緑色の Verified になってよいかだけを指します。 verificationStatus='success' や stark_receipt_verify=success は STARK receipt 検証成功の信号にすぎず、単独で overall verification の成功を意味しません。

最終判定の種類

検証パイプラインの最終表示は shared deriveVerificationPresentationPolicy が一元的に決定します。この policy は deriveVerificationSummary の集約結果に、evidence availability、hard failure、 明示的な server failure、表示 sequence の readiness を合わせ、UI 上の次の ステータスと「Verified」表示資格を返します。API と browser は同じ policy を使い、 UI は policy が許可した最終表示だけを描画します。

Verified の必要条件は 不変条件のまとめ に集約しています。 要点は、既知の required check がすべて存在してすべて success であること、票除外（excludedSlots > 0）がないこと、dev-mode receipt を production STARK proof として扱っていないことです。

ステータスの判定順序

この表は deriveVerificationSummary の集約結果です。 チェックが空、または未知チェックだけで既知チェックが 1 件も解決できない場合、summary は null になり、Verified ではなく最終サマリー未表示として扱われます。

未知チェックが既知チェックと混在する場合も、summary は missing_evidence になります。 これは将来のチェック追加や API drift を成功として解釈しないための fail-closed ルールです。

shared policy の readiness は、検証開始済み、表示 sequence 完了、check の pending / running 解消がそろうまで renderedStatus を返しません。表示 source は (1) 明示的な server failure、(2) hard-failure fallback、(3) summary、 (4) pending warning の順で policy 内で解決されます。/verify ページは timeout や sequence failure を明示的な server failure input として渡し、独自の 「Verified」override は持ちません。

STARK 検証のゲーティング

STARK 検証は整合性検証とは独立に評価されます。

stark_receipt_verify=success でも、他の required checks のいずれかが失敗、未実行、または進行中なら fully verified にはなりません（不変条件のまとめを参照）。

zkGate: STARK 結果に基づく Counted チェックの制御

STARK 検証の結果は、Counted-as-Recorded 段階のチェック評価にも影響します。 これを zkGate と呼びます。

core evaluator では、dev_mode は事前に success または not_run に正規化されてから zkGate に入力されます。 一方、現行の GET /api/sessions/:sessionId/finalizations/:finalizationId/verification の表示用ステータス組み立てでは、dev mode が許可されていない場合は fail-closed の failed として反映されます。

ステップとチェックの対応関係

UI に表示される 4 つのステップは、現行実装では 22 個のチェック定義から派生します。

ただし、verificationSteps[].status は「その stage で required 扱いになるチェック群」から導出されます。 verificationSteps[].inputs は stage 内の 全チェック定義 から集約されます。

補足:

• recorded_commitment_in_bulletin は recorded_inclusion_proof から、recorded_root_at_cast_consistent は recorded_consistency_proof から導出される表示用チェックです。 チェック一覧には現れますが、単独では step status を決定しません。
• recorded_sth_third_party は通常は optional ですが、STH source が設定されている場合だけ required に昇格し、Recorded-as-Cast の step status と最終判定をブロックし得ます。

ステップのステータスは、required 扱いになったチェックのステータスから次の順序で集約されます。

さらに現行実装には、単純集約だけではない 3 つの補正があります。

• counted_as_recorded は journal が存在しない場合、required チェックに failed がない限り not_run に補正されます。
• recorded_as_cast は userVote.proof.treeSize がない場合、not_run に補正されます。
• GET /api/sessions/:sessionId/finalizations/:finalizationId/verification は castSource='client' で verificationSteps / verificationChecks を組み立てるため、API 応答上の Cast-as-Intended はいったん not_run です。 その後ブラウザ側で保存済みセッション情報から Cast チェックを再評価して上書きし、最終的な UI 表示と summary にはそのローカル結果が反映されます。

検証実行と UI 表示の時系列（ポーリングとステップ表示の順序）は 設計と実行フロー を参照してください。

不変条件のまとめ

以下の不変条件は、コードの変更によっても決して緩和してはなりません。

これらの不変条件は、改ざんシナリオ（S0〜S5）の検出を保証する基盤です。 各シナリオがどのチェックで検出されるかは、検出メカニズム を参照してください。

この fail-closed モデルは、単体、結合、E2E テスト で「Verified を誤表示しない」ケースを継続的に検査しています。 形式化側では Lean による形式化 の verification summary / display vectors を通じて、モデルと実装の対応を確認します。

公開境界

検証アーティファクトは、bundle.zip に入れる公開可能データと、保護対象として残すデータに分かれます。

ここでいう public は、「秘密を含まず、第三者検証に使える公開可能データ」という機密性の分類です。 「無認証で誰でも取得できること」は意味しません。 通常のブラウザと CLI では、bundle.zip も検証レポートも session capability で保護された API から取得します。

境界の原則

bundle.zip は、公開可能アーティファクトだけを含む監査用アーカイブです。 zkVM の witness、投票内容を復元し得る入力、個票状態を細かく説明する private bitmap、検証サービスの protected report artifact は含めません。

この境界は利便性より優先します。 bundle.zip 単体で /verify 画面の最終判定を完全再現できない場合でも、private artifact を公開アーカイブへ混ぜません。 UI の最終判定には、session-scoped な自票 proof、bitmap proof、設定時の third-party STH evidence、サーバー側の STARK receipt verification 結果も関わります。

public bundle の default-deny manifest

同期生成の bundle.zip は次の member に限定されます。async bundle は共通の必須 5 member だけを含みます。

receipt.json が含まれていても、それだけで production STARK proof として成功扱いにはなりません。 開発モードの receipt は production STARK proof ではなく、production 検証では fail-closed に扱います。

新しい artifact は、生成された時点では private です。公開可能かどうかを各 builder や配信 handler が個別に推測せず、canonical manifest に明示的に追加され、sync/async member set と completed-archive admission の review を通過した場合にだけ bundle.zip へ入れられます。この default-private / allowlist-driven 方針により、 新しい内部 artifact の追加が意図しない公開へ直結することを防ぎます。

manifest にない member は private が既定です。required member の欠落、private/unknown member、 duplicate/case conflict、traversal・absolute・非 canonical path を含む completed ZIP は publication/delivery より前に拒否されます。

bundle.zip に入れないファイル

次のファイルは bundle.zip のメンバーではありません。

input.json、verification.json、included-bitmap.json、seen-bitmap.json の 4 つは、モードに依存しない保護対象です。 verification.json は必要な場合に bundle.zip とは別の report endpoint から取得します。 failure-marker.json は非同期モードのみで生成され得る private diagnostic で、report endpoint からも配布しません。ライフサイクル契約の詳細は 非同期プローバー を参照してください。

bundle と report の取得経路

通常のブラウザと CLI の contract は、次の capability 保護 API です。

どちらも session capability によって保護されます。 finalizationId は、その session の現在の succeeded finalization record が持つ finalizationId と一致している必要があります。

S3-backed 実行でも、ブラウザと CLI は raw S3 URL や presigned URL を通常契約として使いません。 API handler が権限と finalization scope を確認したうえで、ローカル保存または S3 から artifact を読み出して返します。 大きい S3 bundle は、同じ API 経由の range response で配信されます。

sync mode と async mode の差分

公開境界(何を入れないか)は sync mode と async mode で同じです。 モードごとの実際のメンバー構成、生成環境、生成フローの差分は バンドル構造 を参照してください。

実装上の照合点

この境界を確認するときは、次の実装を合わせて参照します。

• mode-aware manifest and archive admission: packages/verification/src/verification/public-bundle-manifest.{json,ts}
• sync/async builders: packages/verification/src/verification/verification-bundle.ts, infra/docker/entrypoint.sh
• async prover failure marker: infra/docker/prover-failure-marker-contract.json, packages/aws-adapters/src/finalize/async-prover-artifacts.ts
• authenticated bundle/report delivery: apps/api/src/server/api/handlers/verificationBundles.ts
• 現行 verification flow notes: docs/verification/README.md

詳細なファイル構造とローカル監査手順は、バンドル構造 と 第三者検証ガイド を参照してください。

バンドル構造

この章は、証明バンドルのファイル構造と、同期モードと非同期モードの差分を説明します。 公開可能アーティファクトと保護対象アーティファクトの境界は 公開境界 に集約しています。

概要

証明バンドル は、zkVM の実行結果を検証可能な形で保存し、配布するためのアーティファクト群です。 実際に配布される bundle.zip は、mode-aware な default-deny manifest によって公開可能アーティファクトだけを含める配布対象アーカイブです。

ここでいう public / 「公開可能」は「秘密を含まず第三者検証に使える」という機密性の分類です（public ≠ 無認証公開の正本は 公開境界）。

bundle.zip は監査用成果物であり、/verify 画面の最終判定を単体で完全再現することは目的としていません。 UI 最終判定に必要な追加材料は 第三者検証ガイド を参照してください。

flowchart TB
  subgraph "バンドルディレクトリ"
    subgraph "公開可能アーティファクト"
      PI["public-input.json<br/>公開入力"]
      EM["election-manifest.json<br/>選挙マニフェスト"]
      CS["close-statement.json<br/>締切ステートメント"]
      RC["receipt.json<br/>STARK レシート"]
      JN["journal.json<br/>zkVM ジャーナル"]
      MT["metadata.json<br/>メタデータ（syncのみ）"]
      STH["sth.json<br/>STH スナップショット"]
      CP["consistency-proof.json<br/>整合性証明"]
    end

    subgraph "非公開アーティファクト"
      IN["input.json<br/>秘匿入力（ウィットネス）"]
      VR["verification.json<br/>検証レポート"]
      IB["included-bitmap.json<br/>厳密 counted bitmap"]
      SB["seen-bitmap.json<br/>厳密 presented bitmap"]
      FM["failure-marker.json<br/>非同期失敗分類"]
    end

    BZ["bundle.zip<br/>配布対象アーカイブ"]
  end

  PI --> BZ
  EM --> BZ
  CS --> BZ
  RC --> BZ
  JN --> BZ
  MT --> BZ
  STH -.-> BZ
  CP -.-> BZ
  IN -.-x BZ
  VR -.-x BZ
  IB -.-x BZ
  SB -.-x BZ
  FM -.-x BZ

公開境界の要約

配布対象アーカイブ（bundle.zip）に含められるファイルは、default-deny manifest によって厳格に制限されています。 この節は構造を読むための要約です。境界の規則そのものは 公開境界 が正です。

bundle.zip に入る公開可能アーティファクト

receipt.json の存在だけでは成功扱いになりません。dev-mode（RISC0_DEV_MODE=1）receipt の扱いは 公開境界 と同じ規則です。 metadata.json は sync bundle で必須です。sth.json と consistency-proof.json は sync bundle の optional member ですが、現行フローでは通常生成されません。

bundle.zip に入れない保護対象アーティファクト

冒頭図の非公開アーティファクト 5 ファイルは bundle.zip のメンバーではありません。 対象ファイルの一覧と除外理由は 公開境界 を参照してください。

公開入力の構造

public-input.json は、第三者検証に必要で、かつ選択肢と乱数を含まない入力側レコードです。 input.json の単純なサブセットではありません。

votes 配列の内容から、第三者は入力コミットメントを再計算できます。選択肢と乱数はこのファイルに含まれません。

public-input.json と inputCommitment は同一ではありません。 後者が直接束縛するのはこのレコードの一部です。 計算対象フィールドと非対象フィールドの整理は 入力コミットメント を参照してください。

同期バンドルと非同期バンドルの違い

証明生成には、同期モード（local profile の TypeScript API プロセスが生成）と 非同期モード（ECS Fargate コンテナの entrypoint.sh が生成し、S3 経由でコールバック Lambda がセッションに反映）の 2 つのパスがあります。 両モードとも、public-input.json、election-manifest.json、close-statement.json は journal.json と正準な proof-bound data との整合性検査を通過した場合にのみ bundle 化されます。 不一致があれば fail-closed で処理を中断します。

非同期バンドルの生成フロー

非同期モードでは、ECS Fargate コンテナの entrypoint.sh が次の手順でバンドルを構築します。

1. S3 から入力 JSON をダウンロード
2. ホストバイナリを実行し、レシートと出力を生成
3. 出力から journal.json を変換生成
4. 入力と出力から public-input.json、election-manifest.json、close-statement.json を構築
5. 整合性検査（本節冒頭参照）を通過したものだけを bundle に含める
6. shared manifest の async member set から bundle.zip を作る
7. completed ZIP の member 構成と path を admission する
8. 次を S3 にアップロード
   • ホストの生出力: *-receipt.json、*-output.json
   • 公開可能アーティファクト: public-input.json、election-manifest.json、close-statement.json
   • 非公開の隣接 artifact: included-bitmap.json、seen-bitmap.json
   • 配布対象アーカイブ: bundle.zip

上記は成功時の生成フローです。 非ゼロ終了時、entrypoint は failure-marker.json（bounded な失敗カテゴリだけを持つ private sibling object）を同じ execution scope の private S3 prefix へ best-effort で保存します。 bundle.zip にも protected verification.json report にも取り込まれません。カテゴリ集合や配信されない規則を含む契約の詳細は 非同期プローバー を参照してください。

コールバック Lambda は S3 の bundle.zip からジャーナル、レシート、public-input.json、election-manifest.json、close-statement.json を復元します。 利用可能な場合は隣接オブジェクトの bitmap artifact も取り込み、bundle locator と監査用データを保存します。 report locator は後続の POST /api/sessions/:sessionId/finalizations/:finalizationId/verification が verification work を起動し、 worker が report を保存した場合に記録されます。 ブラウザと CLI への通常配信は capability 保護 API が担当します。

infra/docker/entrypoint.sh は methodVersion 14 のホスト出力を検証し、現行契約と一致しない出力は fail-closed で停止します。 journal.json と public-input.json の methodVersion および inputCommitment が一致し、election-manifest.json と close-statement.json が各自の公開監査フィールドと整合することを確認してから bundle.zip を生成します。

バンドルディレクトリ構造

同期モード（ローカルファイルシステム）

{VERIFIER_WORK_DIR}/
  {sessionId}/
    {finalizationId}/
      input.json               ← 非公開: ウィットネス
      public-input.json        ← 公開可能
      election-manifest.json   ← 公開可能
      close-statement.json     ← 公開可能
      journal.json             ← 公開可能
      receipt.json             ← 公開可能
      metadata.json            ← 公開可能
      included-bitmap.json     ← 非公開: 厳密 counted bitmap artifact
      seen-bitmap.json         ← 非公開: 厳密 presented bitmap artifact
      verification.json        ← 非公開: 検証レポート
      bundle.zip               ← 配布対象: manifest member の admitted archive

非同期モード（S3）

s3://{BUCKET}/sessions/{sessionId}/{finalizationId}/
  input.json                 ← 非公開: ワーク入力
  {inputBase}-receipt.json   ← ホストの生出力
  {inputBase}-output.json    ← ホストの生出力
  {inputBase}-journal.json   ← ホストが生成した場合のみ
  public-input.json          ← 公開可能
  election-manifest.json     ← 公開可能
  close-statement.json       ← 公開可能
  included-bitmap.json       ← 非公開: 厳密 counted bitmap artifact
  seen-bitmap.json           ← 非公開: 厳密 presented bitmap artifact
  bundle.zip                 ← 配布対象: 内部は receipt.json / journal.json / public-input.json / election-manifest.json / close-statement.json
  verification.json          ← scoped verification POST の worker 完了後に参照可能になる場合あり（非公開）
  failure-marker.json        ← 非ゼロ終了時のみ: bounded category-only diagnostic（非公開、best-effort）

補足

• 上記の S3 構造は成功時と失敗時の任意 artifact をまとめたものです。bundle.zip と failure-marker.json が同時に生成されることを意味しません。
• 非同期モードの S3 オブジェクト名は、コンテナ実行時に生成される一時入力ファイル名 inputBase に依存するため、固定の receipt.json / journal.json になりません。
• target AWS profile の capability 保護 API は、sessionId と finalizationId から導出した canonical S3 key の report だけを読み出します。
• local profile の API は同じ identity から導出したローカル report だけを読み出します。profile をまたぐ fallback はなく、選択された backend に artifact がなければ 404 を返します。

バンドルのアクセス方法

ダウンロードエンドポイント

取得経路とアクセスポリシーは 公開境界 > bundle と report の取得経路 を、wire 契約（status、Range、エラーコード）は API エンドポイント を参照してください。

アーカイブの再現性

同期モード（verification-bundle.ts）の bundle.zip は再現性を確保するため、次の措置を講じています。

• エントリのタイムスタンプをゼロに固定
• shared manifest に一致するファイルのみを含める
• ファイル名のアルファベット順でエントリを追加

非同期モード（infra/docker/entrypoint.sh）は zip -r で作成されます。 そのため、上記の再現性制御とは実装が異なります。

セキュリティ上の制約

パストラバーサル防止

バンドルのパスセグメント（セッション ID、finalization ID）は英数字とハイフンのみに制限されています。 .. を含むパスや許可されていない文字を含むパスは拒否されます。 completed ZIP も required member の欠落、private/unknown member、duplicate/case conflict、 traversal・absolute・非 canonical member name を含む場合は拒否されます。

改ざんシナリオ

STARK Ballot Simulator は、E2E 検証可能投票の教育的デモとして、正常系 S0 と改ざんシナリオ S1 から S5 を提供します。 S1 から S5 は特定の異常ケースを模擬し、検証パイプラインがどのチェックで異常を検出するかを示します。

この部の章

• シナリオ一覧: S0 から S5 の定義、データフロー、実装上の扱い
• 検出メカニズム: シナリオ別に失敗するチェックと最終判定

想定読者と前提

想定読者は、検証パイプラインの教育的デモを試したい技術者です。 読む前に、検証パイプライン の 4 段階モデルを把握していることを前提にします。

この部で扱わないもの

• 実世界の投票システムに対する攻撃手法の一般論
• 本番投票システム向けの脅威モデリングや対策ガイド
• S2 と S4 を proof-tampering とみなすなど、PoC スコープを超える攻撃シナリオ

関連する章

• 検証パイプライン: 各シナリオに対応するチェックの一覧
• 第三者検証ガイド: シナリオごとに生成された bundle.zip を監査する手順
• 用語集: シナリオと改ざんに関する用語定義

シナリオ一覧

改ざんシナリオ S0〜S5 の定義と、実装上どこを改変するかを整理します。 説明の中心は、zkVM 入力、主張集計（claimed tally）、ジャーナル統計（missing/invalid/excluded）の関係です。

教育モードの目的

改ざんシナリオは、暗号的検証が実際に機能することを確認するために設計されています。

• 正常ケース（S0）を基準として、検証パイプラインが通過する状態を確認する
• 攻撃シナリオ（S1〜S5）を適用して、どの不変条件が破れると検証が失敗するかを確認する

攻撃の類型

• 入力改ざん (tamperMode=input): S1 / S3 / S5
• 主張改ざん (tamperMode=claim): S2 / S4

この分類は「改ざんがどこに入るか」のみを示します。 どのチェックで失敗するかの詳細は 検出メカニズム を参照してください。

実装上の共通前提

• 1 回の finalize で選択されるシナリオは 1 つ（S0〜S5）
  • UI: /aggregate は single-select（S0〜S5 のラジオボタン）
  • API: POST /api/sessions/:sessionId/finalizations は scenarioId を 1 つ受け取る
• totalExpected は 64（ユーザー 1 + ボット 63）
• 掲示板（CT Merkle）は追記専用で、シナリオ適用で既存エントリは削除しない
• tamperMode は none / input / claim の 3 種

実行モードと検証の前提

• 本章は実 API 経路（POST /api/sessions/:sessionId/finalizations → finalizeSessionHandler → finalizeSessionUsecase → finalizeSync|finalizeAsync）を基準に説明する
• finalize 実行モード（同期 / 非同期）は RUNTIME_PROFILE が一意に決める。profile ごとの意味論は AWS runtime 境界 を参照
• mock mode の差分: browser mock（VITE_RUNTIME_PROFILE=local-demo）の API fixture は本章と異なるチェック結果を返すことがあり、local-demo / static-mock-e2e の mock zkVM executor は production STARK proof を生成しない
• local-proof-development の dev-mode receipt も production STARK proof ではない
• 本章の「主な失敗点」は STARK 検証が success の局面を前提とする（zkGate の詳細は 検出メカニズム を参照）

tamperMode は、シナリオ変更を zkVM 入力へ反映するかどうかを決めます。

flowchart TD
  A[シナリオ選択] --> B{tamperMode}
  B -->|none / claim| C[元の votes を zkVM 入力へ]
  B -->|input| D[modifiedVotes を zkVM 入力へ]
  C --> E[zkVM 実行]
  D --> E

シナリオ一覧表

シナリオ別に失敗するチェックは 検出メカニズム > シナリオ別の主な失敗チェック を参照してください。

S0: 正常（改ざんなし）

改ざんを適用しない基準シナリオです。

S1: ユーザー票の除外

ユーザー票（インデックス 0）を modifiedVotes から削除し、63 票を zkVM に渡します。

失敗するチェックは 検出メカニズム を参照してください。

S2: ユーザー票に関する主張集計の改ざん

ユーザー票に対する「主張集計（表示する tally）」のみ改ざんします。 zkVM には元の 64 票を渡します。

失敗するチェックは 検出メカニズム を参照してください。

S3: ボット票の除外

現行実装ではボット票インデックス 1（targetBotId 初期値）を削除し、63 票を zkVM に渡します。

S1 との違い

• S1: ユーザー自身の未集計をビットマップで直接示せる
• S3: ユーザー票は含まれるが、集計全体の完全性違反で検出される

S4: ボット票に関する主張集計の改ざん

1 票のボット票に関する「主張集計」だけを改ざんします。 zkVM 入力は元の 64 票のままです。

S2 と同様に、改ざん対象は tally.counts 側です。失敗するチェックは 検出メカニズム を参照してください。

S5: ランダムな票の除外

現行実装では、64 票からランダムに 1 票を選び、modifiedVotes から削除します。 選んだ票の候補を別候補へ変える処理はありません。

S5 の処理

• tamperMode は常に input のため、zkVM 入力は常に modifiedVotes が使われる
• シナリオ変更は IGNORED として記録され、ignoredCount=1, recountedCount=0 になる
• 元の掲示板インデックスは保存される（失敗するチェックは 検出メカニズム を参照）

ジャーナル統計の扱い（sync / async 共通）

現行実装では、missingSlots / invalidPresentedSlots / excludedSlots / validVotes などのジャーナル統計は、sync / async いずれも zkVM が返した proof-derived な値をそのまま使います。

• sync / async いずれも、finalize 後にジャーナル統計を上書きしない
• target async finalize は finalization writer が S3 の bundle.zip から復元した journal をそのまま使う

シナリオ由来の ignoredCount / recountedCount / claimedCounts は presentation 用であり、journal の統計値を書き換えません。

• ignoredCount / recountedCount → tamperSummary や tamperedCount に反映
• claimedCounts → S2/S4 の表示用 tally

tamperMode=claim（S2/S4）でも同様に、ジャーナル統計は zkVM の値のままです。

集計フローへの挿入点

flowchart TB
  A[セッション votes 読み込み] --> B[シナリオ適用]
  B --> C{tamperMode}
  C -- input --> D[modifiedVotes で zkVM 入力生成]
  C -- claim --> E[元の votes で zkVM 入力生成]
  D --> F[zkVM 実行]
  E --> F
  F --> G[finalizationResult 保存]
  B --> H[claimedCounts 計算]
  H --> G

検出メカニズム

各改ざんシナリオに対して、検証パイプラインがどのチェックで失敗するかを整理します。 このページは実 API の判定ロジックを基準にしており、STARK 検証が success になった後の挙動を前提とします。

前提

• 実行モードと検証の前提は シナリオ一覧 > 実行モードと検証の前提 と同じ。
• 現行の verification resource は GET /api/sessions/:sessionId/finalizations/:finalizationId/verification で取得する。
• サーバー応答は castSource=client のため、raw な verification.checks の cast_* は シナリオに関係なく not_run。ブラウザは保持している投票内容と乱数、サーバーから取得した exact receipt を使って local cast checks を評価し、この 4 チェックを overlay してから表示用の stage と最終判定を導出する。

Counted 系チェックの zkGate

verification resource の Counted 系チェックには、STARK 前に評価できる項目と、STARK 状態でゲートされる項目が混在します。

• counted_input_sanity / counted_unique_indices / counted_unique_commitments は、publicInputArtifact から導出した内部 publicInputAuthority があれば STARK 未解決でも評価されます。
• counted_tally_consistent / counted_missing_indices_zero / counted_expected_vs_tree_size / counted_election_manifest_consistent / counted_close_statement_consistent / counted_my_vote_included / counted_input_commitment_match は zkGate の対象です。
• STARK 未解決（not_run/running）の間、zkGate 対象チェックは原則として not_run または pending になります。
• 例外として、counted_missing_indices_zero は journal count の異常や excludedSlots > 0 が既に解決できる場合、STARK 未解決でも fail-closed に failed になり得ます。
• verifierResult.status=failed では、zkGate 対象チェックも failed になり得ます。

zkGate の一般規則は ゲーティングロジック > zkGate を参照してください。

検出の 2 つの原理

• 原理1: 完全性違反 (excludedSlots > 0) → counted_missing_indices_zero が失敗（主に S1/S3/S5）。
• 原理2: 主張集計の不整合 (claimed ≠ verified) → counted_tally_consistent が失敗（主に S2/S4）。

シナリオ別の主な失敗チェック（STARK 解決後）

補足:

• S1 では、ビットマップ証明が利用可能な場合 counted_my_vote_included も失敗し得ます。
• S2/S4 では、zkVM 入力を改変していないため、counted_input_commitment_match は通常成功します。
• S5 ではランダム対象がユーザー票の場合、ビットマップ証明が利用可能なら counted_my_vote_included も失敗し得ます。

4 段階検証モデルとの対応（raw サーバー応答）

この表は「シナリオ適用による典型挙動」を示します。 running や追加の not_run は、運用状態や証拠不足により別途発生します。 ここでの値はサーバーが返す verification.steps の状態です。 verifierResult.status は STARK receipt 検証の状態であり、overall verdict そのものではありません。

ブラウザ表示では 前提 の overlay を適用します。 典型フローでは overlay 後の Cast-as-Intended は success になり、ローカル証拠が欠けるか不整合なら not_run または failed のままで、最終表示は Verified になりません。

主要チェック ID マトリクス（STARK 解決後の raw サーバーチェック）

• 証拠不足時の counted_my_vote_included は not_run になります。
• S5 の counted_tally_consistent が通常成功するのは、claimed tally と verified tally がどちらも除外後の 63 票入力ベースだからです。
• cast_commitment_match を含む 4 つの cast_* の not_run は raw サーバー値であり、前提 の overlay 後は通常 success になります。

S2/S4 の主張集計改ざん

S2/S4 は「入力改ざん」ではなく「主張集計改ざん」です。

flowchart TD
  A["tamperMode=claim (S2/S4)"]
  A --> V1["元の votes を zkVM 入力へ"]
  V1 --> V2["verifiedTally"]
  A --> C1["claimedCounts を改変"]
  C1 --> C2["API の presentation.tally.counts"]
  V2 --> X{"claimed と verified は一致?"}
  C2 --> X
  X -->|不一致| F["counted_tally_consistent = failed"]

このため、counted_input_commitment_match の失敗は通常発生しません。 zkVM 入力は元票であり、投票レシートと STARK 証明も有効なままです。

S5 の除外処理

S5 の定義と処理内容（tamperMode=input、modifiedVotes、ジャーナル統計の扱い）はシナリオ一覧 > S5を参照してください。 検出の主因は、missingSlots=1 / excludedSlots=1 による counted_missing_indices_zero の失敗です。

ビットマップ証明の役割

counted_my_vote_included は、チェック定義上 required のユーザー包含チェックです。

• S1（ユーザー票除外）では、証明が利用可能なら失敗して「自票が未集計」であることを直接示せる。
• 証拠不足で not_run になる場合でも、最終判定は Verified になりません:
  • 完全性違反が同時にある場合は votes_excluded_unknown になります。
  • 完全性違反がなく required evidence が欠ける場合は missing_evidence になります。

最終判定（Verified 表示）

最終表示は共有 verification-presentation-policy が決定します（厳密な判定条件は ゲーティングロジック を参照）。 ブラウザが policy に渡すのは、前提 の overlay 後の完全なチェック集合です。 policy は verification-summary に加えて、resource の availability、fail-closed exclusion signal、明示的な proof failure、検証シーケンスの完了状態を統合します。

flowchart TB
  A[raw サーバーチェック] --> B[browser-local cast checks を overlay]
  B --> C[共有 presentation policy]
  C --> D[summary + hard failure + explicit proof failure]
  D --> E{表示準備完了?}
  E -- no --> W[Verified を表示しない]
  E -- yes --> F{fullyVerifiedLabelEligible?}
  F -- no --> N[failed / warning / demo_only]
  F -- yes --> V[Verified]

fullyVerifiedLabelEligible が true になるのは、summary が fully_verified、hard failure がなく、 明示的な proof failure もなく、表示 readiness が ready で rendered status が verified の場合だけです。 summary 内の分類順序は ゲーティングロジック > ステータスの判定順序 を参照してください。

代表的な失敗ステータス:

• user_vote_excluded / votes_excluded / votes_excluded_unknown: 完全性違反（S1/S3/S5）
• published_tally_mismatch: claimed と verified の不一致（S2/S4）
• counted_integrity_failed: Counted 系必須チェック失敗の一般ケース

これらの検出経路は、単体、結合、E2E テスト の CLI と E2E フローで補強しています。 Merkle と journal の不変条件は、Property-based Testing でも補強しています。

品質保証と形式手法

この部では、STARK Ballot Simulator の検証ロジックをどの品質境界で支えているかを説明します。

本プロジェクトは AI コーディングエージェントと協業して実装を進めました。 そのため、実装速度だけでなく、AI 協業で混入しやすい次の乖離を検出する境界を重視します。

• 仕様と実装のドリフト
• 暗黙の fallback
• 公開してはいけないアーティファクトの混入
• Verified 判定ロジックの分散

この部の章

• 単体、結合、E2E テスト: example-based テストでの局所退行検出と CLI / E2E 経路
• Property-based Testing: fast-check と Rust proptest による入力空間探索
• Lean による形式化: 抽象モデルでの不変条件証明と CI 連携

想定読者と前提

• 想定読者: 実装に追従するテストや形式化の設計判断を確認したい開発者、監査者
• 前提: 単体テスト、結合テスト、E2E テストの一般的な区分と、Property-based Testing の基本概念を把握していること

品質保証のレイヤー

本書では、example-based tests、property-based testing、Lean による形式化、それらを CI に接続する仕組みを次のレイヤーで使い分けます。

中心に置く不変条件

最も重要な品質目標は、ユーザーに Verified と表示してよい条件を緩めないことです。

• required check が失敗、未実行、実行中なら Verified にしない
• excludedSlots > 0 を成功状態にしない
• STARK receipt verification だけを根拠に全体成功としない
• mode 非依存の保護 4 アーティファクト（公開境界）を公開配布対象に含めない
• mock / dev receipt / production STARK proof の違いをテスト階層で明示する

これらは ゲーティングロジック と バンドル構造 で説明した安全境界を、テストと形式化の側から支えるものです。

この部で扱わないもの

この部は、システム全体の完全な形式検証を主張するものではありません。 SHA-256 や RISC Zero の暗号学的健全性、各種ランタイムや AWS の正しさ、本番選挙システムとしての安全性は対象外です。 Lean が扱う射程と扱わない射程の詳細は Lean による形式化 > 証明していないこと を参照してください。

関連する章

• 検証パイプライン: テストと形式化が守る Verified 判定の本体
• ゲーティングロジック: 不変条件として品質保証が支える側のロジック
• バンドル構造: 公開境界の判定に関わる安全境界

単体、結合、E2E テスト

このページでは、example-based tests がどのリスクを守っているかを整理します。 焦点はテスト数ではなく、検証アプリとして失敗できない境界にどの層のテストを置いているかです。

テスト層の役割

単体テスト

単体テストは、純粋関数、小さな UI component、schema、環境変数 guard、エラー整形の退行検出に使います。

対象:

• 検証チェック定義と summary logic
• Lean 生成 vector と照合する verification summary / display / check definition
• zkVM journal / input commitment / bitmap helper
• session capability token と Turnstile bypass guard
• UI component と hooks
• i18n translation consistency

結合テスト

結合テストは、境界をまたいだ契約が崩れていないかを検査します。

対象:

• Hono 互換の API route inventory と request / response contract
• store 実装と finalization state transition
• verification bundle の public allowlist
• verifier-service client と STARK receipt status の扱い
• Lean 生成 vector と照合する input commitment / bitmap Merkle / Rust guest model
• bitmap proof、bulletin proof、verification run などの session-scoped API

CLI と E2E テスト

CLI と Playwright は、単一関数ではなく利用者フローとしての正しさを見ます。

• CLI flow: session 作成、投票、集計、検証をブラウザなしで実行する
• Playwright mock flow: Vite の local-mock build を static Hono server で配信し、主要画面を通す
• axe smoke: 主要ページの重大な accessibility violation を検出する
• real zkVM dev flow と real zkVM prod flow: proof contract 変更時に mock だけで完了扱いにしないための重い確認経路

主なコマンド

local-proof-development profile の receipt は production STARK proof ではなく、UI/API の回帰検出に有用でも proof soundness を確認したことにはなりません（判定側の扱いは ゲーティングロジック を参照）。

Vitest の ownership

root の pnpm test:run は、workspace manifest と repository tooling metadata から導出した明示的な Vitest project を実行します。 各 apps/*、packages/*、scripts/、repository tooling scope が自身の test file を所有し、重複した project ownership を許しません。

test environment も scope ごとに固定します。 browser component を持つ @stark-ballot/web だけが jsdom と browser setup を使い、それ以外の workspace と repository tooling は Node environment で実行します。 各 workspace の local test task は狭い確認用で、root の pnpm test:run が repository 全体の単体・結合テスト gate です。 public snapshot では pnpm test:public が公開対象に残した範囲だけを実行します。

mock mode の実行経路

pnpm dev と Playwright mock E2E は、どちらもローカル確認用の mock evidence を使いますが、同じ runtime path ではありません。

static-mock-e2e はブラウザ内だけで API を完結させず static Hono server を通るため、pnpm dev より本番配信形に近い経路を確認します。 この分離により、日常の UI 反復は Vite dev server で速く回し、E2E では production-mode の静的 frontend 配信、Hono API handler、session-scoped endpoint、mock zkVM / mock store の結合を確認します。 個別の mock、store、proof、Turnstile flag は runtime selector として使いません。profile の意味論は AWS runtime 境界 を参照してください。 target / reusable な pnpm build:ci artifact は target-aws-async browser profile を選択し、artifact scan で mock API や test-only の Turnstile bypass が混入していないことを確認します。

検査観点

Verified を誤表示しない

このアプリの最優先 invariant は、必要な暗号チェックと整合性チェックが通っていない状態で Verified を表示しないことです。

テストでは次のような状態を fail-closed に扱います。

• required check が failed
• required check が not_run / pending / running
• STARK receipt verification が失敗または未解決
• unknown check や空の check set
• excludedSlots > 0
• public tally と verified tally の不一致

この観点は ゲーティングロジック の実装側の安全網です。

公開 artifact 境界

bundle.zip は第三者検証に必要な公開可能 artifact だけを含みます。 公開してよいものは allowlist で管理し、mode 非依存の保護 4 アーティファクトは配布対象に含めません（一覧と理由は 公開境界 を参照）。

この境界は sync 生成、async container、bundle/report delivery の複数箇所にまたがるため、テストで契約として固定します。

mock zkVM と real zkVM の境界

mock zkVM は UI や API flow の高速な退行検出に使います。 一方で、journal format、input commitment、Image ID、receipt verification contract に触れる変更では、Rust 側や real zkVM 経路を使って TypeScript と Rust の対応を確認します。

コストの違いを前提に、普段は軽い gate を使い、proof contract に触れる変更では重い gate へ進む設計です。

UI と accessibility

Playwright は、ユーザーが実際に触る投票、集計、検証の流れを production-mode の static Hono server 上で確認します。 テスト ID は翻訳文ではなく安定した data-testid を使い、i18n やレイアウト変更に引きずられにくくしています。

CI での位置づけ

CI では、TypeScript の core checks、UI mock E2E、Rust tests、formal checks、public snapshot checks が役割を分けて動きます。 変更領域に応じて必要な gate を選ぶ方針は mock zkVM と real zkVM の境界 と同じです。

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 を検出する追加レイヤーとして扱います。

Lean による形式化

本プロジェクトでは Lean 4 を使い、Verified 表示の fail-closed 条件、journal count の整合性、input commitment の canonical encoding、LSB-first bitmap packing、抽象 guest tally model の不変条件を形式化しています。

Lean は実装を直接証明しません。 代わりに、抽象モデル上で不変条件を証明し、そこから生成した generated vectors、formal report、formal audit を TypeScript / Rust のテストと CI に接続します。 この接続により、モデルと実装の対応付けを継続的に検査します。 Lean が扱わない範囲は末尾の 証明していないこと を参照してください。

Lean で定義しているもの

GuestModel.lean は zkvm/methods/guest/src/main.rs を行単位で翻訳したものではありません。 外部的に重要な処理順序を抽象 state machine として表します。 具体的には、インデックス範囲、重複 index、選択肢、コミットメント、重複 commitment、包含証明、集計反映の順序をモデル化します。

Lean で証明していること

これらは抽象モデル上の主張であり、実装との対応は次節の generated vectors とテストで検査します。

実装との接続

flowchart LR
  L["Lean models<br/>formal/StarkBallotFormal/*.lean"]
  T["Theorems<br/>形式的な不変条件"]
  R["formal-report.json<br/>主張と前提"]
  V["generated-vectors/*.json<br/>実装対応付けケース"]
  A["formal-audit.json<br/>theorem hash / dependency / hygiene"]
  TS["TypeScript tests<br/>Vitest"]
  RS["Rust vector tests<br/>cargo test"]
  FCI["formal CI<br/>pnpm formal:verify"]
  RCI["Rust tests workflow<br/>cargo test"]

  L --> T
  T --> R
  L --> V
  T --> A
  V --> TS
  V --> RS
  R --> FCI
  V --> FCI
  A --> FCI
  TS --> FCI
  RS --> RCI

pnpm formal:verify は Lean build、formal report、generated vectors、audit の freshness、TypeScript の vector-consuming tests、生成 JSON の format check をまとめて実行します。 Rust 側の vector-consuming tests は docs/formal/generated-vectors/** の変更で起動する Rust tests workflow の cargo test によって検査します。 公開 repository snapshot の release workflow でも export 前に Lean workspace を build して pnpm formal:verify を実行します。 そのため、formal artifact が古い、または formal verification が失敗する状態では公開 snapshot を生成できません。

この接続により、Lean model と実装のどちらが変わっても、追従していない drift を CI 上で検出できます。

対応付けを支える成果物

前掲の generated vectors と vector-consuming tests に加えて、次の audit artifact と検査を組み込んでいます。

• theorem statement hash と generated-vector hash
• #print axioms に基づく theorem dependency audit
• proof hygiene scan
• treeSize <= 1,000,000 と vote count <= 1,000,000 の explicit guest input bounds、およびそこから導く candidate tally bucket <= 1,000,000

実行コマンド

証明していないこと

Lean は次を証明しません。

• SHA-256 の衝突困難性
• RISC Zero receipt soundness
• Rust compiler / TypeScript runtime / browser runtime の完全な正しさ
• AWS runtime behavior
• React rendering 全体の正しさ
• 本番選挙システムとしての安全性
• zkVM guest Rust 実装全体の line-by-line verification

したがって、主張は「投票システム全体を形式検証した」ではありません。 選択した安全モデルを Lean で証明し、generated vectors と CI drift guard によって TypeScript / Rust 実装との対応を検査しています。

AWS アーキテクチャ

この部は、STARK Ballot Simulator を AWS 上で動かす場合の runtime 境界とサービス責務を説明します。 まず AWS runtime 境界 を読み、公開仕様として扱う範囲を確認してください。

AWS runtime は、Terraform 管理の静的フロントエンド、Hono/API ランタイム、DynamoDB ストア、非同期プローバー、検証 worker、private proof artifact storage で構成されます。 この部はそれぞれの責務分担を説明します。

ここでいう public は「秘密を含まず第三者検証に使える」という機密性の分類です（無認証公開ではありません。定義は 公開境界）。 bundle / report の通常取得経路は capability 保護 API です（公開境界 > bundle と report の取得経路）。

この部の章

• AWS runtime 境界：公開仕様として扱う runtime 境界、artifact 境界、扱わない情報
• 現行構成とサービス一覧：runtime 管理境界、環境分離、主要サービスの責務
• トポロジー：レイヤ別のサービス構成と通信フロー
• 非同期プローバー：SQS → Step Functions → ECS による証明パイプライン
• 可観測性設計：verdict authority と分離した構造化ログ、検出、相関、通知境界
• イメージ署名：AWS Signer managed signing と deployment preflight / ECS 実行前の暗号学的検証
• Terraform：IaC による root ownership、recovery selection、deployment / release authority、runtime wiring

想定読者と前提

• 想定読者: 公開仕様として AWS runtime の責務分担を把握したい読者
• 前提: AWS の基本サービス（S3 / SQS / Step Functions / ECS）、CloudFront / KMS / CodePipeline などの配信・デプロイ系サービス、Terraform の概念を把握していること

この部で扱わないもの

• 退役済み Amplify / AppSync 構成の詳細
• Terraform 文法・モジュール設計の一般論
• 個別 account の alarm tuning、24 時間 on-call、詳細なコスト最適化
• 個別アカウント、秘密値、アカウント固有の承認手順や詳細な証跡
• 移行作業記録と、環境切り替え、本番環境の初期構築、独自ドメインの本番 DNS 切り替え、旧 AWS アカウント削除の進捗・完了状態

関連する章

• zkVM 設計：ECS 上で実行されるホストとレシート生成
• バンドル構造：bundle.zip と protected report artifact の境界
• 第三者検証ガイド：capability 保護 API から取得した bundle.zip を使うローカル監査
• 用語集：インフラ用語の定義

AWS runtime 境界

このページは、AWS 章で前提にする公開仕様上の runtime 境界を定義します。 ここでいう runtime は、ブラウザから投票、集計、検証を実行するための target 構成です。 扱わない範囲は末尾の このページで扱わないもの にまとめます。

Semantic runtime profiles

server は RUNTIME_PROFILE、browser build は VITE_RUNTIME_PROFILE で実行意図を 一度だけ選びます。server resolver は adapter construction より前に profile を解決し、 store、proof evidence、finalization、artifact backend、rate limit、Turnstile posture の混在を拒否します。

target profile は production proof、DynamoDB、S3、async orchestration、Dynamo rate limit、bypass 不可を一体として選びます。quiesced profile は develop recovery 専用で browser public projection には公開しません。secret 値と外部 resource identifier は profile 名に埋め込まず、target runtime の参照入力として別に検証します。

公開仕様として扱う境界

Frontend

ブラウザアプリケーションは Vite / React Router で生成された静的 frontend です。 ビルド成果物は CloudFront から配信され、origin は private S3 bucket です。 S3 frontend origin は直接公開せず、CloudFront が静的 asset と browser route fallback の入口になります。

ブラウザからの API 呼び出しは、通常 same-origin の /api/* として CloudFront に送られます。 CloudFront は静的 asset を S3 origin へ、/api/* を API Gateway origin へ routing します。 これにより、frontend と API の公開入口は同じ origin 上に投影されます。

Develop target では、静的 frontend と API の両方を含む CloudFront behavior を operator / tester 向けの signed-cookie gate で保護します。 署名用の秘密鍵は KMS 内で管理し、対応する公開鍵だけを CloudFront trusted key group に登録します。 この gate は環境全体への入口を制限するもので、session-scoped な capability token の代わりにはなりません。

API

API Gateway は /api/* を受け取り、Lambda 上の Hono runtime adapter に渡します。 実際の wire-level API surface は packages/api-contract/src/routes/inventory.ts が正準です。 apps/api/src/server/api/routes/definitions.ts はその contract を runtime mode 別に投影し、Hono は contract で定義された route と handler を AWS runtime に接続します。

Target runtime では、CloudFront が API origin への転送時に origin-verification header を付与し、Hono はその値が欠落または不一致のリクエストを拒否します。 したがって、API Gateway の直接 URL は通常の browser / CLI contract ではなく、認可された CloudFront origin path が外側の admission boundary です。

その内側で、session-scoped な現行 route は path の sessionId と X-Session-Capability を照合します（対象 route と header の契約は API リファレンス > セッション capability）。

Data store

DynamoDB は session、vote、finalization state、verification run state、rate-limit state、prover semaphore state などの runtime state を保持します。 ブラウザが DynamoDB に直接アクセスする経路はありません。 API Lambda と worker Lambda が、それぞれの IAM role に基づく最小権限で DynamoDB を読み書きします。

Async prover

長時間かかる STARK 証明生成は、非同期 runtime に分離されます。 非同期モードの POST /api/sessions/:sessionId/finalizations は work item を SQS に登録します。 Step Functions は署名確認や concurrency semaphore などの gate を通過した場合だけ ECS Fargate task を起動し、zkVM host が証明と公開監査用 artifact を生成します。 生成結果は finalization-writer Lambda が finalization record に反映し、ブラウザは GET /api/sessions/:sessionId/finalizations/current を capability 付きでポーリングします。 パイプラインの詳細は 非同期プローバー を参照してください。

Verification worker

Target runtime の POST /api/sessions/:sessionId/finalizations/:finalizationId/verification は、 path と session capability、current succeeded finalization、finalization-scoped な bundle locator、 expected Image ID を確認したうえで verification work を durable queue に登録します。 verification-worker Lambda は private S3 bucket から bundle.zip を取得して verifier-service で STARK レシートを検証します。検証結果は sessionId と finalizationId で scope された verification result record に、S3 の bundle/report locator は分離された AWS delivery metadata に保存されます。 ブラウザは通常の API flow から検証状態を取得し、worker や S3 に直接アクセスしません（検証内容は 検証サービス を参照）。

Proof artifacts

Proof artifact storage は private S3 bucket です。 保護対象 artifact を public bundle.zip に含めない分類と除外リストは、公開境界 に従います。 bundle.zip と report（verification.json）の通常配信は capability 保護 API 経由で、raw S3 URL や presigned URL は通常の browser / CLI contract ではありません（取得経路とアクセスポリシーは 公開境界 > bundle と report の取得経路）。

このページで扱わないもの

この runtime boundary は公開仕様としての責務分担に限定します。 次の情報は扱いません。

• AWS account ID、具体的な ARN、bucket 名、secret 名
• secret / config handoff の手順や証跡
• post-merge Plan 02 / Plan 03 の完了条件や blocking status
• production DNS cutover の進捗
• CodePipeline / CodeBuild の詳細な承認証跡
• legacy AWS account deletion の状態

関連する章

• 現行構成とサービス一覧：AWS service ごとの責務
• トポロジー：CloudFront、API Gateway、Lambda、DynamoDB、S3、SQS、Step Functions、ECS の通信経路
• 非同期プローバー：SQS / Step Functions / ECS Fargate による証明生成
• 可観測性設計：runtime を横断する構造化ログ、検出、相関、通知境界
• バンドル構造：bundle.zip と private artifact の境界

現行構成とサービス一覧

AWS runtime の管理境界、環境分離、主要サービスの責務を公開仕様として整理します。 前提となる公開境界と、個別デプロイの承認記録・内部運用証跡など扱わない範囲は AWS runtime 境界 を参照してください。

Terraform root ごとの管理境界

AWS runtime は Terraform の root ごとに責務を分けて管理します。 root ごとの管理対象と所有しない範囲の正本は Terraform > Root ownership です。要約は次のとおりです。

• infra/terraform/app：target application runtime（CloudFront + frontend、API、DynamoDB、queue / SFN / ECS / S3、observability）。ECR repository や image publication は所有せず、digest 固定の prover image URI を消費する
• infra/terraform/foundation：app 実行の前提リソース（ECR、ECR retention controller、manifest storage、secret / config container、prover networking）。app runtime resource は作らない
• infra/terraform/bootstrap：Terraform state backend と deployment-control lane、report-only controls、暗号化された authority storage。runtime workload resource は所有しない
• infra/terraform/legacy：retained historical context。現行 runtime の authority ではない

環境分離

develop と main は source branch / account alias / deployment environment / state scope を分けて扱います。 現在の live target app lane は stark-dev/develop/app です。 stark-prod/main/app は protected production contract の repository evidence として render されます。 これは非変更 evidence であり、live production deployment はまだ承認しません。 Target は target-aws-async profile による production STARK 証明を前提にします。Local 実行意図の authority は semantic RUNTIME_PROFILE（local-demo、static-mock-e2e、local-proof-development、local-proof-production）であり、置き換え済みの RISC0_DEV_MODE / USE_MOCK_ZKVM selector は拒否します。

環境別に分かれるものは次のとおりです。

• app runtime state、proof artifact storage
• DynamoDB と選択された recovery pair
• queue / worker、Step Functions、ECS task definition
• runtime SSM refs
• CloudWatch logs / metrics / alarms / ledger
• develop operator gate の trust resources

ECR repository や manifest storage など、app 実行の前提になるリソースは foundation root の責務として扱います。

全体構成図

図: STARK Ballot Simulator の AWS 全体構成（クリックで拡大）。

サービス一覧

この runtime が使う主要な AWS サービスと役割です。

App runtime

サービス表の補足は次のとおりです。

• Observability：telemetry は verification verdict を変更せず、自動 remediation も起動しません。Verification invariant の直接通知と、隔離された ops-actionable 経路の routing 対象（damped alarm と exact owned-pipeline failure）は 可観測性設計 > 通知の境界 が正本です。その他の調査用 alarm は passive です。
• Artifact 境界：public の分類、bundle.zip の除外 artifact、verification.json の capability 保護配信は 公開境界 の定義に従います。
• DynamoDB recovery：4 phase の定義と quiesce を含む切替契約は Terraform を参照してください。
• Develop operator gate：追跡対象の keyset manifest を authority とし、KMS の private signing material を Terraform state、pipeline artifact、runtime role に渡しません。KMS から導出した public key だけを CloudFront trust group に登録し、署名権限は target runtime の責務外に保ちます。

Foundation resources

Prover image metadata、promotion evidence、release record / accepted pointer は proof artifact bucket ではなく image build / signing と runtime wiring の境界に属し、旧構成の SSM current pointer は候補 metadata lookup にとどまります（target topology の release authority ではありません）。 Image build、digest 固定、署名ステータス確認、Image ID との関係は イメージ署名 に集約します。 ECR retention は count / age ベースの native lifecycle expiry ではなく、Foundation-owned の reference-aware retention controller が担います（保護対象と動作の正本は Terraform > Retention authority）。

Deployment control

Report-only drift は accepted Terraform baseline と exact historical source を使って refresh-enabled plan を実行し、redacted report だけを保存します。Rollback / recovery readiness も同じ隔離された App planning 境界を使います。どちらも Apply、state / pointer write、remediation、rollback / recovery exercise を起動せず、その結果は saved plan や mutation の authority になりません。

図: GitHub から CodePipeline deployment lanes を経て app runtime に到達するデプロイ制御フロー（クリックで拡大）。

個別の承認手順、証跡、昇格判断の詳細は公開仕様の範囲外です。

Approval の条件は次のとおりです。

• approval を省略できるのは、normal mode で saved plan に変更がないと機械的に証明された場合だけです。
• Rollback は Terraform plan が空でも approval を必須とします。

Post-apply smoke 後の immutable acceptance evidence 保存と accepted-deployment index の compare-and-swap 更新を含め、詳細は Terraform を参照してください。

Runtime wiring

Runtime の連携は Terraform output、SSM reference、Lambda environment、S3 / SQS / Step Functions locator によって行われます。

flowchart TB
  subgraph FOUNDATION["infra/terraform/foundation"]
    ECR["ECR repositories<br/>prover / toolchain"]
    MANIFEST["Manifest storage<br/>release records / promotion evidence"]
    CONFIG["Secret/config containers<br/>Secrets Manager / SSM"]
    NET["Prover networking inputs"]
    RETENTION["Reference-aware ECR retention"]
  end

  subgraph APP["infra/terraform/app"]
    OUT["Terraform outputs<br/>API / bucket / queue / lambda names"]
    PARAM["SSM refs<br/>runtime config"]
    RUNTIME["Runtime resources<br/>CloudFront / API / DDB / SQS / SFN / ECS"]
    GATE["Develop operator gate<br/>KMS signing keys / CloudFront trust group"]
    DATA["DynamoDB active pair<br/>primary or validated replacement"]
    SEM["Prover semaphore<br/>DDB lock row / janitor"]
    ARTIFACTS["Private proof artifact S3<br/>bundle source / protected report"]
    OBS["Observability<br/>CloudWatch / EventBridge / SNS"]
  end

  subgraph BOOT["infra/terraform/bootstrap"]
    CONTROL["Deployment control lanes"]
    AUTHORITY["Encrypted authority storage<br/>deployables / acceptance / Terraform baseline / reports"]
    REPORT["Report-only controls<br/>drift / readiness"]
  end

  ECR --> RUNTIME
  ECR --> RETENTION
  MANIFEST --> RUNTIME
  MANIFEST --> RETENTION
  CONFIG --> PARAM
  NET --> RUNTIME
  CONTROL --> RUNTIME
  CONTROL --> AUTHORITY
  AUTHORITY --> CONTROL
  AUTHORITY --> RETENTION
  AUTHORITY --> REPORT
  REPORT --> AUTHORITY
  PARAM --> RUNTIME
  GATE --> RUNTIME
  RUNTIME --> DATA
  RUNTIME --> SEM
  SEM --> RUNTIME
  RUNTIME --> ARTIFACTS
  RUNTIME --> OBS
  RUNTIME --> RETENTION
  REPORT -. "refresh-only inspection" .-> RUNTIME
  CONTROL --> OBS
  RUNTIME --> OUT

canonical runtime component name と legacy/historical name の対応は次のとおりです。legacy 名は historical context としてのみ扱います。

現行アーキテクチャの責務分離

現行構成は、一つの hosting/backend lifecycle にすべての責務を集約しません。 短い user-facing Web/API request と数分規模の proof work を分ける理由は 非同期プローバー > 実行リソースと mode 境界、 runtime、前提 resource、deployment control を Terraform root ごとに分ける理由は Terraform > Root ownership が現在の参照先です。

この分離により、proof capacity や image authority の変更を API request lifecycle から切り離し、IaC の plan、権限、review、rollback 判断を change lifecycle ごとに 限定できます。過去の Amplify / AppSync / Next.js 構成や手動 handoff は現行 runtime contract ではありません。

関連する章

• トポロジー：リクエスト経路とコンポーネント間の通信フロー
• 非同期プローバー：SQS → Step Functions → ECS の実行時フロー
• 可観測性設計：CloudWatch / EventBridge / SNS のシグナルと authority 境界
• Terraform：target app/bootstrap state と runtime wiring

トポロジー

AWS 上のサービス配置とコンポーネント間の通信経路を示します。 このページは runtime の責務分担を説明します（個別環境の導入進捗は扱いません）。

本システムは次の 6 つの論理レイヤで構成されます。

• Web レイヤ：静的配信と develop signed-cookie gate
• API レイヤ：API Gateway と public-api Lambda
• Data レイヤ：DynamoDB による永続化
• Prover レイヤ：SQS / Step Functions / ECS による証明生成
• Verification レイヤ：STARK レシート検証
• Storage レイヤ：proof artifact の S3 保存

レイヤ別トポロジー

Web レイヤ

CloudFront が private S3 origin の Vite/React 静的アセットを配信します。 /api/* は同じ CloudFront distribution から API Gateway origin に routing されます。 extensionless browser route は viewer-request fallback で index.html に解決します。

develop で operator gate が有効な場合、static frontend、browser route、/api、/api/* の viewer access は CloudFront signed cookie を要求します。 信頼する public key group は、追跡対象 keyset に従って Terraform が管理する非対称 KMS signing key から public key を導出して構成します。 KMS の private signing material は CloudFront、app runtime role、Terraform state には渡しません。 この gate は develop 固有の条件付き境界であり、すべての環境に一律適用されるものではありません。

API レイヤ

API Gateway（HTTP API）が /api/* パスパターンのリクエストを受け取り、単一の Lambda 関数（public-api）にプロキシします。 public-api は Hono route inventory を実行する runtime adapter で、ルーティング、セッション管理、Turnstile 検証、レート制限を処理します。 下図の「主なリクエスト制御」は、public-api がルートごとに適用有無と順序を切り替える代表的な要素を示します。 固定順のパイプラインではありません。

flowchart LR
  Client["クライアント"] --> CF["CloudFront"]
  KMS["KMS<br/>(develop signing keys)"] --> KG["CloudFront trusted key group<br/>(public keys only)"]
  KG -. develop signed-cookie gate .-> CF
  CF --> FRONT["S3<br/>(static frontend)"]
  CF --> APIGW["API Gateway<br/>(HTTP API)"]
  APIGW --> API["public-api<br/>Lambda"]
  API --> DDB["DynamoDB<br/>(sessions / votes / rate limits)"]
  API --> SQS["SQS<br/>(非同期証明)"]
  API --> VQS["SQS<br/>(検証 work queue)"]
  API --> S3["S3<br/>(bundle / report delivery)"]
  VQS --> VW["verification-worker<br/>Lambda"]
  VW --> S3
  VW --> DDB

  subgraph "主なリクエスト制御（ルートごとに適用）"
    direction TB
    RATE["IP / zkVM レート制限"]
    SESS["セッション / capability 検証"]
    TURN["Turnstile 検証"]
    BODY["入力検証"]
    HAND["ハンドラー実行"]
    RATE -.-> HAND
    SESS -.-> HAND
    TURN -.-> HAND
    BODY -.-> HAND
  end

CORS 設定で X-Session-Capability ヘッダーを許可し、session-scoped route は path の sessionId と capability トークンを照合します（契約は API リファレンス > セッション capability）。 POST /api/sessions/{sessionId}/finalizations/{finalizationId}/verification は、target runtime では検証 work を verification-work キューへ登録し、HTTP 応答では verificationStatus=running、finalizationId、推定所要時間、idempotent 判定を返します。 実際の STARK レシート検証と protected report の保存は verification-worker の責務です。 後述のエンドツーエンドのデータフローも参照してください。

Data レイヤ

DynamoDB が、セッション、投票、集計結果、レート制限状態の永続化を担当します。 データプレーンは target Lambda IAM role ごとの最小権限で制限され、ブラウザから DynamoDB へ直接アクセスする経路はありません。

通常時は Terraform-owned primary sessions / votes table pair を参照します。 DynamoDB recovery の 4 phase 定義と切替契約は Terraform を参照してください（quiesced phase の図への影響は エンドツーエンドのデータフロー に注記）。

sessions table は string partition key sessionId を使いますが、単一の aggregate session row は保存しません。 identity、voting、finalization、verification、artifact delivery を、責務ごとの record family と prefixed key に分離します。 votes table は引き続き (sessionId, voteIndex) の複合キーを使います。

session-owned record には用途に応じた expiresAt を持たせます。 receipt board の global counter は sessions table 上の独立した非 TTL record です。

レート制限用に 2 つの追加テーブル（RateLimitEvents、RateLimitCounters）が PAY_PER_REQUEST モードで運用されています。 これとは別に、同時実行数を制御する prover semaphore table も DynamoDB 上で管理します。

Prover レイヤ

STARK 証明の生成を担当するレイヤです。 SQS キュー、Step Functions ステートマシン、ECS Fargate タスクで構成されます。 詳細は 非同期プローバー を参照してください。

flowchart LR
  CODEBUILD["CodeBuild<br/>プローバー候補イメージ"] --> META["S3<br/>候補 metadata / promotion evidence"]
  CODEBUILD -. legacy / optional<br/>非 authority .-> SSM["SSM Parameter<br/>current metadata"]
  META --> RECORD["Prover release record<br/>accepted pointer"]
  RECORD --> PREFLIGHT["image-signature-verifier<br/>preflight alias"]
  PREFLIGHT -. VERIFIED evidence .-> APP["App deployment record"]
  SQS["SQS<br/>ワークキュー"] --> DP["proof-dispatcher<br/>Lambda"]
  DP --> SFN["Step Functions<br/>ディスパッチャー"]
  APP -. digest / verifier authority .-> SFN
  SFN --> SIG["image-signature-verifier<br/>runtime alias"]
  SIG -. VERIFIED .-> SFN
  SFN <--> SEM["DynamoDB<br/>prover semaphore"]
  JANITOR["semaphore-janitor<br/>Lambda"] --> SEM
  SFN --> ECS["ECS Fargate<br/>ARM64 Linux / CPU-only"]
  SFN --> CALLBACK["finalization-writer<br/>Lambda"]
  ECS --> S3["S3<br/>証明バンドル"]

normal App deployment は、選択した digest 固定 Prover image を immutable verifier version の preflight alias で検証し、その evidence と verifier authority を App deployment record に固定します。 runtime では Step Functions の最初の state が同じ authority の runtime alias を呼び、暗号学的検証に成功した場合だけ semaphore の取得と ECS 起動へ進みます。

ECS タスクは ARM64 アーキテクチャの Fargate で実行され、Foundation-owned VPC（10.42.0.0/20）内のパブリックサブネットに配置されます（セキュリティグループの設定は ネットワーク構成 を参照）。 Step Functions は DynamoDB の semaphore row で prover slot を取得・解放し、semaphore-janitor は terminal execution event と定期 sweep から stale slot を回収します。

Verification レイヤ

STARK レシート検証を担当するレイヤです。 public-api は session capability、finalization state、bundle locator、Image ID を確認したうえで検証 work を SQS に登録します。 verification-worker は work item に含まれる sessionId、finalizationId、bundleKey、expected Image ID を使って private S3 bucket から bundle.zip を取得します。 その後、verifier-service で Receipt::verify(expected_image_id) を実行します。

検証結果は protected report artifact（verification.json）として保存されます（扱いは 公開境界 と後述の Storage レイヤ）。

Storage レイヤ

S3 バケットが、証明バンドルに含まれる配布対象アーティファクトと非公開ワーク入力の保存を担当します。 Target Terraform はこれに加えて、プローバーイメージ候補の metadata、promotion evidence、release record / accepted pointer 用の非公開 S3 storage を管理します。 実行対象は選択された app deployment record から渡される digest 固定 prover image URI で決まります。

プローバー release metadata / evidence は foundation 側の versioned manifest storage に保存します。 CodeBuild からの publish 仕様、legacy/optional SSM current pointer の非 authority 境界、digest 固定 runtime input の関係は イメージ署名 > ビルドと署名の概念 を参照してください。

証明バンドル側のオブジェクトパスは既定で sessions/{sessionId}/{finalizationId}/ 配下です。 target runtime では S3_PROOF_PREFIX=sessions/ が Terraform と runtime validation の契約です。 この prefix を変更するには、public-api、verification-worker、proof-dispatcher、finalization-writer、CLI/report delivery の S3 policy と artifact lookup を同時に変更する必要があります。 影響範囲は 非同期プローバー > Dispatch 処理 を参照してください。

配布対象（bundle.zip とその同梱物）と保護対象（input.json、bitmap sibling object など）の区分は 公開境界 を、bundle member と S3 レイアウトの詳細は バンドル構造 を参照してください。 このレイヤに固有のファイルは次のとおりです。

エンドツーエンドのデータフロー

投票から検証までのデータフローを、レイヤ間の通信として示します。 以下は primary_active または replacement_active の非 quiesced phase における処理です。 *_quiesced phase では、この図に含まれる新規 session admission と prover / verification queue consumption は利用できません。 図では API request ごとの CloudFront hop を省略していますが、develop operator gate が有効な場合は frontend と API の両方で viewer request の signed cookie を検証します。

sequenceDiagram
  participant C as クライアント
  participant W as Web レイヤ<br/>(CloudFront + S3)
  participant A as API レイヤ<br/>(API GW + Lambda)
  participant Q as 検証キュー<br/>(verification-work)
  participant V as 検証レイヤ<br/>(verification-worker)
  participant D as Data レイヤ<br/>(DynamoDB)
  participant P as Prover レイヤ<br/>(SQS → SFN → ECS)
  participant S as Storage レイヤ<br/>(S3)

  Note over C,D: 投票フェーズ
  C->>W: ページ読み込み
  opt develop operator gate enabled
    W->>W: CloudFront signed-cookie 検証
  end
  C->>A: POST /api/sessions
  A->>D: セッション作成
  C->>A: POST /api/sessions/{sessionId}/votes
  A->>D: 投票 + コミットメント保存
  A-->>C: 投票レシート返却
  Note over A,D: ボット投票を自動追加

  Note over C,P: 集計フェーズ
  C->>A: POST /api/sessions/{sessionId}/finalizations
  A->>P: SQS メッセージ送信
  A-->>C: 202 Accepted
  P->>S: input.json 保存（SFN 起動前）
  P->>P: イメージ署名検証
  P->>P: ECS タスクで証明生成
  P->>S: 実行成果物 + 公開監査アーティファクト + bundle.zip 保存
  P->>D: コールバックで結果書き込み

  Note over C,S: 検証フェーズ
  C->>A: GET /api/sessions/{sessionId}/finalizations/{finalizationId}/verification
  A->>D: identity + voting + finalization + verification record 取得
  A-->>C: 検証ペイロード返却
  C->>A: POST /api/sessions/{sessionId}/finalizations/{finalizationId}/verification
  A->>Q: 検証 work を登録
  A->>D: VERIFICATION_RESULT に running を記録
  A-->>C: verificationStatus=running + finalizationId 返却
  Q->>V: work item 配信
  V->>S: bundle.zip 取得
  V->>V: verifier-service 実行
  V->>S: verification.json を protected report として保存
  V->>D: verification result と delivery metadata を別 record に記録
  C->>A: GET /api/sessions/{sessionId}/finalizations/{finalizationId}/verification
  A->>D: 最新の検証状態取得
  A-->>C: 検証結果を含むペイロード返却

verification-worker は bundle.zip を検証入力として読み取り、target AWS runtime では verification.json が存在しない場合や S3 upload に失敗した場合に fail-closed に失敗します。 保存に成功した report locator は VERIFICATION_DELIVERY record に、検証結果は VERIFICATION_RESULT record に保存し、pure finalization state には混在させません。 report 保存に失敗しても delivery metadata の既存 s3BundleKey は維持されますが、verification run 自体は成功扱いになりません（report と bitmap sibling object の扱いは バンドル構造）。

ネットワーク構成

VPC

Foundation Terraform が管理する VPC は、ECS Fargate タスク専用です。 API Gateway、target Lambdas、DynamoDB、S3、CloudFront は VPC 外の managed service boundary で動作します。 VPC は 10.42.0.0/20 で、最初の 2 つの available AZ に /24 public subnet を 1 つずつ配置します。 AZ 名は Terraform が実行時に取得するため、特定の AZ suffix には固定しません。

flowchart TD
  subgraph VPC["Foundation-owned VPC (10.42.0.0/20)"]
    subgraph AZ1["available AZ 1"]
      S1["パブリックサブネット<br/>10.42.0.0/24"]
    end
    subgraph AZ2["available AZ 2"]
      S2["パブリックサブネット<br/>10.42.1.0/24"]
    end
    SG["セキュリティグループ<br/>Ingress: なし<br/>Egress: all protocols / ports"]
  end

  IGW["インターネット<br/>ゲートウェイ"]
  ECR["ECR<br/>(イメージ取得)"]
  S3["S3<br/>(バンドル保存)"]

  VPC --> IGW
  IGW --> ECR
  IGW --> S3

ECS タスクはパブリック IP を持ちますが、セキュリティグループがインバウンドを全拒否するため、外部からのアクセスはできません。 アウトバウンドは 0.0.0.0/0 に対する全 protocol / port を許可します。 この egress 全許可は、public subnet から ECR、S3、CloudWatch Logs などへ到達するための develop prover の割り切りです。

監視とロギング

この節はログの物理配置と保持期間を示します。 ログ、メトリクス、alarm、operations ledger の authority と読み方は 可観測性設計 を参照してください。

主な CloudWatch ログ群

runtime のログ群（ECS Fargate タスク、Step Functions 実行、public-api / proof-dispatcher / finalization-writer / verification-worker / image-signature-verifier / semaphore-janitor の各 Lambda、API Gateway アクセスログ）の保持期間は develop 90 日 / main 180 日で統一しています。 例外は次の 2 つです。

ロググループ名は Terraform-managed physical names と component suffix に揃えます（image-signature-verifier の log group だけは stark-ballot-sim- を name prefix に使います）。 deployment pipeline の CodeBuild log group は bootstrap root の管理対象です。 develop / main の保持期間は、bootstrap pipeline が 30 / 365 日、App pipeline が 180 / 365 日、Foundation と image release pipeline が 365 / 365 日です。

CloudTrail

CloudTrail は current target app/bootstrap/foundation Terraform runtime の構成要素ではなく、account-plane または organization-level の監査証跡として別途管理される場合があります。 旧構成の残存ロググループ、旧 standalone prover/toolchain CodeBuild log group、旧 Terraform の multi-region CloudTrail（main 環境のみ、90 日保持）は、この topology の runtime authority に含めません。

関連する章

• 現行構成とサービス一覧：サービスごとの責務一覧
• 非同期プローバー：Prover レイヤの実行時フロー
• 可観測性設計：ログ、検出、相関、通知境界
• バンドル構造：Storage レイヤの artifact 境界

非同期プローバー

このページは、AWS runtime で STARK 証明生成を HTTP リクエストから分離する非同期プローバー経路を説明します。 対象は RUNTIME_PROFILE=target-aws-async の経路です。

STARK 証明生成はブラウザ操作や API Gateway / Lambda の短い応答時間より長くかかります。 そのため、POST /api/sessions/:sessionId/finalizations は作業を受理してすぐ返し、証明生成は SQS、Step Functions、ECS Fargate に委ねます。 ブラウザは capability token 付きの current finalization API をポーリングし、完了後に bundle / report を取得します（Bundle / report delivery。public の分類は 公開境界 の定義に従います）。

実行リソースと mode 境界

target の prover task は ARM64 Linux の CPU-only ECS Fargate task で、現行 IaC default は 16 vCPU / 32 GiB です。target-aws-async profile は production proof evidence と async finalization だけを許可し、mock / development receipt や同期 execution を選べません。

local/test profile は同じ target topology を模倣するものではありません。 local-demo と static-mock-e2e は mock evidence、 local-proof-development は development-only receipt、 local-proof-production は production proof をそれぞれ同期実行します。profile 全体の対応表は AWS runtime 境界 > Semantic runtime profiles を参照してください。

この分離により、短い Web/API request lifecycle は work acceptance と status 取得に集中し、数分規模・高 resource の proof lifecycle は queue、retry、 capacity control、artifact publication を独立して扱えます。CPU/GPU や task resource を変更する場合は、この非同期境界を保ったまま proof-time と cost の evidence を取り直す必要があります。

全体像

flowchart TB
  API["POST /api/sessions/:sessionId/finalizations<br/>capability protected"] --> S3IN["Private S3<br/>input.json"]
  API --> SQS["SQS<br/>prover work queue"]
  SQS --> DISPATCH["proof-dispatcher Lambda"]
  DISPATCH --> SFN["Step Functions<br/>finalization state machine"]
  SFN --> SIG["image-signature-verifier Lambda<br/>runtime alias"]
  SIG --> CHECK{"cryptographic result<br/>VERIFIED?"}
  CHECK -->|Yes| SEM["DynamoDB<br/>prover semaphore"]
  JANITOR["semaphore-janitor Lambda<br/>compensating cleanup"] -.-> SEM
  SEM --> STARTED["finalization-writer Lambda<br/>running admitted"]
  STARTED --> ECS["ECS Fargate task<br/>zkVM host"]
  CHECK -->|No| CALLBACK_FAIL["finalization-writer Lambda<br/>failed"]
  ECS --> S3OUT["Private S3<br/>bundle.zip + sibling artifacts"]
  ECS --> CALLBACK_OK["finalization-writer Lambda<br/>succeeded / timeout / failed"]
  CALLBACK_OK --> DDB["DynamoDB<br/>session finalization state"]
  CALLBACK_FAIL --> DDB
  DDB --> STATUS["GET /api/sessions/:sessionId/finalizations/current<br/>capability protected"]
  S3OUT --> DOWNLOAD["GET .../:finalizationId/artifacts/bundle<br/>GET .../:finalizationId/artifacts/report<br/>capability protected"]

主要な責務は次のとおりです。

Finalize 受付

POST /api/sessions/:sessionId/finalizations は session-scoped な操作であり、path の sessionId と X-Session-Capability の検証を通過した場合だけ処理されます（契約は API リファレンス > セッション capability）。

非同期モードでは、API handler は同期的に証明を作らず、次の処理を行います。

1. セッションが finalize 可能な状態か検証する。
2. zkVM 入力を構築し、finalization state を pending として保存する。
3. target AWS runtime では sessions/{sessionId}/{finalizationId}/input.json に zkVM 入力を保存する。
4. SQS work queue に、正準 S3 key を含む prover work message を送る。
5. 202 Accepted と pending の FinalizationResource を返す。現行 resource は status URL を含まない。

返却後のクライアントのポーリングと status の判定境界は Client polling と判定境界 を参照してください。

Dispatch 処理

proof-dispatcher Lambda は SQS message を 1 件ずつ処理します。 SQS は長時間の証明生成を直接抱えるのではなく、Step Functions execution を開始するための durable dispatch queue です。

dispatcher は次を検証します。

• strict な message shape と recordType、session ID、finalization ID
• input.json、output prefix、bundle.zip の S3 key が session / finalization scope の正準 layout に一致すること
• AWS runtime に必要な環境設定が存在すること

検証後、dispatcher は Step Functions を StartExecution で開始します。 dispatcher は input.json を保存せず、StartExecution 成功だけで finalization state を running にもしません（running へ遷移する条件は Step Functions）。