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

Rule coverage and configuration well-formedness

Aperta
  • Qualcosa non va?
#2,291 1 commento 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
25/100
Tipo di issue
Funzionalità
Chiarezza
Da chiarire
Stato di attività
Ferma
Ambito
compilers

Direzione di ricerca

Esamina le due regole checkBalanceUnderflow mostrate nell’issue e la semantica EVM circostante. Determina innanzitutto se un account mancante è consentito in una configurazione ben formata, quindi verifica se set di regole simili sono incompleti. Il lavoro è completo quando la conclusione è documentata e viene valutato se la creazione delle definizioni può rilevare automaticamente questi casi.

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

Descrizione

enhancement

The rules for checkBalanceUnderflow:

     rule <k> #checkBalanceUnderflow ACCT VALUE => #refund GCALL ~> #pushCallStack ~> #pushWorldState ~> #end EVMC_BALANCE_UNDERFLOW ... </k>
         <output> _ => .Bytes </output>
         <callGas> GCALL </callGas>
         <account>
           <acctID> ACCT </acctID>
           <balance> BAL </balance>
           ...
         </account>
      requires VALUE >Int BAL

    rule <k> #checkBalanceUnderflow ACCT VALUE => . ... </k>
         <account>
           <acctID> ACCT </acctID>
           <balance> BAL </balance>
           ...
         </account>
      requires VALUE <=Int BAL

only consider configurations in which the account with identifier ACCT is present.

Is this:

  • an omission, in the sense that there should be a third rule when the account is not present; or
  • a consequence of having a well-formed EVM configuration, in the sense that an account with identifier ACCT must always be present when there is an #checkBalanceUnderflow check?

Perhaps it would be a good idea if we went through the semantics to see if there are other sets of rules that are incomplete in this sense. Is there a way of understanding this automatically, perhaps on definition creation? @ehildenb @jberthold

Lingua principale
KCL
Stelle
592
Fork
156
Merge medio
2h 19m
PR unite (30g)
1

Preparare l'ambiente

Non abbiamo ancora controllato i file di configurazione di questo progetto. 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 Compilers

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.