Machine integers or "True" integers?
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
- Refactorización
- Claridad
- Necesita aclaración
- Estado de actividad
- Estancado
- Stack tecnológico
- wasm
- Área
- compilers
Línea de trabajo
El issue identifica numeric.md como el punto de entrada actual para las reglas personalizadas y señala el módulo MINT en K's domains.k. Lee primero esas definiciones y luego compara la representación existente con MINT en cuanto a su impacto en las pruebas y la ejecución concreta; para darlo por terminado se requiere un enfoque acordado y los cambios semánticos correspondientes, pero no se especifican criterios de aceptación.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
In K's builtin domains.k library we find a suite of functions implementing machine integers of arbitrary bit width represented in 2's complement. For example:
/*@
* Addition, subtraction, and multiplication are the same for signed and
* unsigned integers represented in 2's complement
*/
syntax MInt ::= addMInt(MInt, MInt) [function, hook(MINT.add), smt-hook(bvadd)]
| subMInt(MInt, MInt) [function, hook(MINT.sub), smt-hook(bvsub)]
| mulMInt(MInt, MInt) [function, hook(MINT.mul), smt-hook(bvmul)]
Currently, this repo is not using these builtins, but rather, similar to evm-semantics, uses "True" integer representations + modulo operations.
I'm curious what the best approach is here. In writing proofs of EVM programs, a lot of effort goes in into writing lemmas that deals with quite simple arithmetic, which can otherwise be proven directly using the right SMT definitions. On the other hand, SMT theories dealing with large bitvectors (such as the 256-bit words of the EVM) quickly start being more difficult to reason with than modulo integer arithmetic.
There might also be speedups of concrete executions to consider in this choice. I expect the MINT library to be faster than custom made extra rules.
I'm tentatively in favor of replacing the custom rules dealing with machine integers in numeric.md in favor of the MINT module of domains.k, but I'm curious of others people's thoughts here. @ehildenb @hjorthjort @dwightguth
- Lenguaje dominante
- WebAssembly
- Estrellas
- 106
- Forks
- 24
- Métricas de merge de PR
- Sin PR fusionados en 30 d
Preparar el entorno
Primeros pasos
- Lee el issue completo y luego la guía de contribución del proyecto.
- Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
- Haz un fork del repositorio y trabaja en una rama.
- Abre un pull request que haga referencia al número del issue.
Más de runtimeverification/wasm-semantics
-
enhancement
Dificultad 2/5 1-3 horas Aptitud para principiantes 55/100
-
bug
Dificultad 4/5 3-5 días Aptitud para principiantes 35/100
-
Dificultad 3/5 1-2 días Aptitud para principiantes 48/100
-
Dificultad 3/5 1-2 días Aptitud para principiantes 55/100
-
Improve tokenisation supportAbierto
Dificultad 4/5 3-5 días Aptitud para principiantes 35/100
Todos los issues de runtimeverification/wasm-semantics
Issues similares
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 84/100
objectionary/jeo-maven-plugin#1827 ·
Los mantenedores suelen responder en 4 días
-
backend:DirectX
Dificultad 2/5 1-3 horas Aptitud para principiantes 84/100
llvm/llvm-project#227530 ·
Los mantenedores suelen responder en 1 día
-
`enzymexla.linalg.lu` lowering fails for a tall matrix: the permutation is built with the pivot typeAbierto
Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100
EnzymeAD/Enzyme-JAX#3286 ·
Los mantenedores suelen responder en 1 día
-
bot-triaged oncall: cpu inductor
Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100
pytorch/pytorch#199058 · 1 comentario ·
Los mantenedores suelen responder en 1 día
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 82/100
WebAssembly/component-model#733 · 1 comentario ·
Los mantenedores suelen responder en 2 días