Hacktoberfest 2026: những issue maintainer đã đánh dấu cho tháng Mười, đang mở và phù hợp người mới. Xem issue Hacktoberfest

All-path reachability proof checker

Đang mở
  • Có gì không ổn?
#4,936 0 bình luận 0 reaction 0 người được giao Xem trên GitHub

Chưa có ai nhận issue này.

Đánh giá

Độ khó
5/5
Thời gian dự kiến
Hơn một tuần
Mức phù hợp với người mới
30/100
Loại issue
Tính năng
Độ rõ ràng
Khá rõ ràng
Mức độ hoạt động
Ít trao đổi
Công nghệ
haskell, python
Lĩnh vực
backend, compilers

Hướng nghiên cứu

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.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

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.

Ngôn ngữ chính
Python
Star
591
Fork
163
Không có pull request nào được merge trong 30 ngày

Chuẩn bị môi trường

Bắt đầu từ đâu

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của runtimeverification/k

Tất cả issue của runtimeverification/k

Issue tương tự

Thêm issue về Python

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.