Hacktoberfest 2026: los issues que los mantenedores marcaron para octubre, abiertos y aptos para principiantes. Explorar issues de Hacktoberfest

Project Proposal

Abierto
  • ¿Algo no está bien?
#234 0 comentarios 0 reacciones 0 asignados Ver en GitHub

Nadie ha tomado este issue todavía.

Evaluación

Dificultad
5/5
Tiempo estimado
Más de una semana
Aptitud para principiantes
25/100
Tipo de issue
Nueva funcionalidad
Claridad
Necesita aclaración
Estado de actividad
Estancado
Stack tecnológico
wasm
Área
compilers

Línea de trabajo

Comienza revisando la semántica de KWasm y los entregables de la propuesta, especialmente la verificación WRC20 planificada y la integración de KWasm en CI. Para darlo por terminado, habría que seleccionar y verificar los programas Wasm propuestos, actualizar KWasm según sea necesario, integrar sus especificaciones K en CI y actualizar la documentación en línea.

Escrito por el modelo de indexación a partir del texto del issue.

Descripción

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”.

Lenguaje dominante
WebAssembly
Estrellas
106
Forks
24
Sin PR fusionados en 30 d

Preparar el entorno

Primeros pasos

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Más de runtimeverification/wasm-semantics

Todos los issues de runtimeverification/wasm-semantics

Issues similares

Más issues de Compilers

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.