Hacktoberfest 2026：メンテナが10月に向けて印を付けた、オープンで初心者向けの issue。 Hacktoberfest の issue を見る

All-path reachability proof checker

オープン
  • 何か問題がありますか？
#4,936 コメント 0 件 リアクション 0 件 担当者 0 名 GitHub で見る

まだ誰も着手していません。

評価

難易度
5/5
見積もり時間
1週間以上
初心者へのやさしさ
30/100
issue の種類
機能追加
明瞭さ
おおむね明確
活発さ
静か
技術スタック
haskell, python
領域
backend, compilers

調査の方向性

Start by locating the pyk APRProofChecker entry point and the Haskell backend RPC surface for guided_execute, then inspect the existing implies, get_model, and simplify RPCs. Done means the checker validates edges, splits, covers, and leaves, returns the specified status, remainders, and undecided obligations, and demonstrates the stated speed goal against the prover.

索引モデルが issue の本文から書いたものです。

説明

check(APRProof) → (ProofStatus, APRProof, [remainder], [undecided_obligation]).

The prover is slow because at every step it searches for applicable rules and calls SMT to decide which branches are feasible; re-establishing a proof (after a semantics change, or to trust one from elsewhere) re-pays all of it, though the finished proof already records which rules fire and where it branches.

The Checker instead treats the KCFG as a certificate and validates every element by its kind: edges are re-applied by the Haskell backend (force-apply the recorded rules, no search), splits and covers are discharged by SMT in pyk.
Because the fired rule is known, there is no rule-search SMT and the taken branch is feasible by its concrete witness; only the irreducible SMT remains — split coverage (parent ∧ ¬⋁cᵢ UNSAT) and cover subsumption (implies) — and even that moves off the critical path, since the rule sequence is fixed: rewrite streams ahead while SMT runs concurrently.
All soundness lives here.

Goal. ≥~2× faster than the prover, or reusing a proof / adding concolic execution is not worth it — measured once a first APRProofChecker exists, not before.

What is checked, and how
  • Edge source --[τ]--> target, a rule sequence τ = [r₁, …, rₙ] — Haskell backend.
    guided_execute force-applies τ to source and returns the resulting end state target'; it is agnostic to any previously recorded target.
    If a step branches before τ is exhausted, the edge hides an uncovered case and the check emits a remainder.
  • Split parent into branches with conditions c₁, …, cₖ — SMT.
    The branches must be exhaustive and non-vacuous: parent ∧ ¬(c₁ ∨ … ∨ cₖ) is UNSAT (nothing falls through the cracks) and each parent ∧ cᵢ is SAT.
    A satisfiable parent ∧ ¬⋁cᵢ is a coverage hole, and its model is a remainder seed.
  • Cover node ⟹ target (or an ancestor, under a substitution) — SMT, implies.
    This closes the final target and loops; a BMC depth bound is the backstop when no cover is found.
  • Leaf — it must subsume the target (success) or be a known terminal/bounded node; a stuck leaf that subsumes neither is a Failed counterexample.

Any of these SMT checks may return unknown/timeout → an UndecidedObligation; it never silently passes.

Layers
  • Haskell backend — guided_execute(S, τ) (new RPC).
    Force-apply rules from τ to S (no rule search), folding steps into a single Edge; cheap simplification discharges trivial guards.
    At the first step whose guard it cannot cheaply discharge, it solves C ∧ ¬guard in place: UNSAT → fold and continue (no round-trip); SAT → return the Edge (depth, end state S'), the taken branch's guard (the Split condition), and the remainder's model (the ¬guard seed); unknown → return an obligation; the trace end also returns.
    It uses SMT for these remainder checks but never for rule search, and can overlap rewriting along the fixed τ with the remainder solve.
    Checking the taken branch's feasibility is an optional parameter — skip it when a concrete witness already establishes it (explore mode), enable it when re-validating a proof without one.
  • pyk — the driver.
    Drive guided_execute and record its Edges, Splits, and remainder seeds; check aggregate split coverage (parent ∧ ¬⋁cᵢ) and cover subsumption via implies; maintain the KCFG and accumulate the result tuple and the monotone ProofStatus.
    Reuses the existing implies, get_model, and simplify RPCs.
Outputs
  • ProofStatus — Passed / Pending / Failed.
  • updated APRProof — the validated (and, when building, grown) KCFG.
  • [remainder] — coverage holes still open.
    Each is remainder = (depth, model, obligation): depth locates the node; model is a concrete seed for the uncovered sub-region (set when the residual is SAT); obligation is set instead when the solver could not decide.
  • [undecided_obligation] —
UndecidedObligation:
  source_node_id : int        # node whose check spawned the query (referenced, not owned)
  depth          : int        # rewrite steps from source_node_id to the query
  kind           : edge | split-coverage | cover
  rule_id        : str | None
  query          : Pattern    # the term the solver could not decide
  result         : unknown | timeout

Passed ⟺ remainders == [] and undecided_obligations == [] and every leaf subsumes the target.

主要言語
Python
スター
591
フォーク
163
30日以内にマージされた PR はありません

環境構築

はじめの一歩

  1. issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
  2. 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
  3. リポジトリをフォークし、ブランチを切って変更します。
  4. issue 番号を参照したプルリクエストを送ります。

runtimeverification/k のほかの issue

runtimeverification/k の issue をすべて見る

似ている issue

Python の issue をもっと見る

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。