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

Interesting properties to prove

Abierto
  • ¿Algo no está bien?
#219 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

El issue no nombra archivos, tests ni puntos de entrada. Empieza localizando la semántica de memoria de KWasm y cualquier modelo de llamadas al host, después formaliza las invariantes keys-in-range y values-in-range y demuéstralas por inducción. Terminado significa que se han establecido las propiedades de soundness indicadas, incluido el efecto de las llamadas al host.

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

Descripción

  • (local.get I:Int) (local.set I:Int) is ust identity (no effect)
  • (ITYPE.store (i32.const ADDR) (ITYPE.load (i32.const ADDR))) is just identity (no effect)
  • A loop invariant: 1+2+...+n = n(n+1)/2
  • Soundness of KWasm: Memory byte arrays maintain their invariants
    • Keys-in-range property: All keys K in the map maintain 0 <= K < SIZE * 65536
      • No instruction can store to out of bounds (< 0 or >= SIZE * 65536)
      • No instruction can load from out of bounds
      • Putting them together with an induction proof: an empty memory has keys-in-range, and no statement can cause it to be violated, so it always holds. May require modelling host calls.
    • Values-in-range property: No instruction can modify the memory so that the value in a slot is <1 or > 255
    • Induction proof: an empty memory is valid, and no statement can cause a memory to become invalid, so the semantics never violate the invariant.

Feel free to add more.

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.