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

More guidance on where to continue execution

Aperta
  • Qualcosa non va?
#1,753 1 commento 0 reazioni 0 assegnatari Vedi su GitHub

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
4/5
Tempo stimato
3-5 giorni
Idoneità per principianti
38/100
Tipo di issue
Funzionalità
Chiarezza
Abbastanza chiara
Stato di attività
Ferma
Ambito
blockchain, testing-qa

Direzione di ricerca

Inizia leggendo APRProof e APRProver.refute_edge, quindi esamina il test funzionante esistente in k-files/simple-proofs.k o k-files/imp-simple-spec.k. Aggiungi un test comparabile per le dimostrazioni KEVM e verifica che confutare un ramo selezionato crei il sotto-proof Equality previsto e impedisca ulteriori esplorazioni.

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

Descrizione

enhancement

Currently, we are not prioritizing any order on the frontier node exploration. But often, we can have branches that the user thinks are uninteresting or infeasible. So we could have a way for the user to say "keep exploring branch B1, but do not explore B2, B3, B4, because I will go and find a way to refute those branches".

Perhaps we could basically build a smaller proof obligation (an equality proof that reduces to false) that then the user has to discharge.

  • Automated proof handling (sub-proof obligations). Proofs carry with them a list sub-proofs (can be added directly to Proof class, and we can add Proof.add_subproof(proof: Proof) -> None, which injects these subproofs. summary is modified to aso print out the status of subproof obligations. Pyk PR: https://github.com/runtimeverification/pyk/pull/394
  • Generic functionality for refute-edge in APRProof class. APRProver.refute_edge method is added, which allows specifying a given edge as refuted and will:
    • Apply expanded to the target of the edge to prevert further exploration.
    • Do APRPRoof.add_subproof with the Equality proof specifying that the edge condition goes to false.
  • Working test in either k-files/simple-proofs.k module or k-files/imp-simple-spec.k module. The key is a specification that leads to a branch, run the rpoof until teh branch is introduced, and then call the refute_edge routine on one of the branches, and assert that the resulting Equality proof that is generated looks correct.
  • Test said functionality on KEVM proofs.
Lingua principale
KCL
Stelle
595
Fork
159
Merge medio
4g 3h
PR unite (30g)
1

Preparare l'ambiente

Questo progetto non fornisce container di sviluppo, Dockerfile né guida per i contributori, quindi l'ambiente è a tuo carico: parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.

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/evm-semantics

Tutte le issue di runtimeverification/evm-semantics

Issue simili

Altre issue su Blockchain

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.