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

Project Proposal

Aperta
  • Qualcosa non va?
#234 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
25/100
Tipo di issue
Funzionalità
Chiarezza
Da chiarire
Stato di attività
Ferma
Stack tecnologico
wasm
Ambito
compilers

Direzione di ricerca

Inizia esaminando la semantica di KWasm e i deliverable della proposta, in particolare la verifica WRC20 pianificata e l'integrazione di KWasm nella CI. Per considerarlo completato, sarebbe necessario selezionare e verificare i programmi Wasm proposti, aggiornare KWasm secondo necessità, integrare le relative specifiche K nella CI e aggiornare la documentazione online.

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

Descrizione

dLab Fellowship Program: Tuning KWasm for Symbolic Execution

Introduction

Runtime Verification developed the KWasm semantics in anticipation of the next generation blockchains, many of which use Wasm (WebAssembly). KEVM is used extensively by Runtime Verification and the broader Ethereum community to verify smart contracts, but the impending switch to eWasm as the target VM (and development of other blockchains targeting Wasm) means that the tooling around KEVM needs to be retargeted to Wasm. The modular nature of the K Framework means the retargeting effort is minimal, but there is still work needed in tuning the semantics for symbolic execution.

Note that this tuning will come in three forms: (i) tuning the Haskell backend of K to be able to handle KWasm proofs, (ii) tuning KWasm to be better suited for symbolic execution, and (iii) adding standard lemmas to the global bag that all KWasm proofs can use. All three categories will benefit all users of KWasm trying to verify smart contracts written in Wasm.

Deliverables:
  • Selection of 6 Wasm programs to verify using KWasm, each incrementally using more features of Wasm and more complicated program logic.
  • K specification of each algorithm, 1 per month, along with updates to KWasm needed to make verifying that algorithm feasible.
  • Integration of developed K specs into KWasm CI so that updates to KWasm do not break them.
  • JelloPaper-like online documentation updated on pushes to KWasm repository.

From the start date, we will (i) select the program to verify for that month, (ii) implement it in Wasm, and (iii) verify it. One week will be allocated to select and write the program, and three weeks will be allocated to verify said program using KWasm. Each program will be allocated roughly a month.

The first algorithm to verify will be a WRC20, which is a Wasm adaption of an ERC20. ERC20 is the most basic token standard used in Ethereum, and is the building block of many other tokens. This program has no loops and no heap manipulation, so serves as a nice first step towards ironing out issues in KWasm regarding symbolic execution, while also being highly applicable to the smart contract domain.

Community Value:

Already KEVM is used extensively outside of Runtime Verification for verification of smart contracts (most notably by the Ethereum Foundation and MakerDAO). Runtime Verification already had to tune KEVM for symbolic execution “on-the-fly”, often extending the time that our verification engagements took with work not directly related to engagement. Each external actor also benefited from this work, as they did not need to tune the semantics themselves. This proposal seeks to front-load as much of that tuning effort as possible, so that as verification engagements for Wasm roll in both Runtime Verification and the broader community can benefit from a ready-to-go KWasm semantics. By the end of this engagement, “KWasm will be ready to use for commercial verification by RV and other companies”.

Lingua principale
WebAssembly
Stelle
107
Fork
26
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/wasm-semantics

Tutte le issue di runtimeverification/wasm-semantics

Issue simili

Altre issue su Compilers

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.