Hacktoberfest 2026: le issue che i maintainer hanno segnato per ottobre, aperte e adatte ai principianti. Sfoglia le issue Hacktoberfest

All-path reachability proof checker

Aperta
  • Qualcosa non va?
#4,936 0 commenti 0 reazioni 0 assegnatari Vedi su GitHub

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
5/5
Tempo stimato
Più di una settimana
Idoneità per principianti
30/100
Tipo di issue
Funzionalità
Chiarezza
Abbastanza chiara
Stato di attività
Tranquilla
Stack tecnologico
haskell, python
Ambito
backend, compilers

Direzione di ricerca

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.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

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.

Lingua principale
Python
Stelle
596
Fork
164
Nessuna PR unita negli ultimi 30g

Preparare l'ambiente

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di runtimeverification/k

Tutte le issue di runtimeverification/k

Issue simili

Altre issue su Python

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.