using this semantics in Coq
Nadie ha tomado este issue todavía.
Evaluación
- Dificultad
- 5/5
- Tiempo estimado
- Más de una semana
- Aptitud para principiantes
- 20/100
- Tipo de issue
- Nueva funcionalidad
- Claridad
- Necesita aclaración
- Estado de actividad
- Estancado
- Área
- blockchain, compilers
Línea de trabajo
El issue no menciona archivos, pruebas ni puntos de entrada. Empieza revisando los repositorios de KEVM y K en busca de trabajos existentes de traducción a Coq o de integración de pruebas, y determina después si un traductor genérico entra en el alcance. La tarea estará terminada cuando exista un camino documentado y acordado para usar KEVM en Coq, o un plan de implementación claramente delimitado.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
Has anyone explored how to use the KEVM semantics in Coq? Is there a generic K to Coq translator or has someone written a specific translation for KEVM?
I would like to use this semantics to prove correctness of an implementation of an optimized EVM interpretor or jit compliler.
- Lenguaje dominante
- KCL
- Estrellas
- 592
- Forks
- 156
- Merge medio
- 2 h 19 min
- PR fusionados (30 d)
- 1
Preparar el entorno
Aún no hemos revisado los archivos de configuración de este proyecto. Empieza por su README y consulta nuestra guía para la primera contribución para los pasos generales.
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/evm-semantics
-
Dificultad 1/5 Menos de una hora Aptitud para principiantes 78/100
runtimeverification/evm-semantics#1190 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 45/100
runtimeverification/evm-semantics#2879 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 35/100
runtimeverification/evm-semantics#2869 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 35/100
runtimeverification/evm-semantics#2832 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 30/100
runtimeverification/evm-semantics#2824 ·
Todos los issues de runtimeverification/evm-semantics
Issues similares
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 86/100
OpenZeppelin/openzeppelin-community-contracts#292 ·
Los mantenedores suelen responder en 2 días
-
submission
Dificultad 2/5 1-3 horas Aptitud para principiantes 72/100
Uniswap/hooklist#10463 · 1 comentario ·
Los mantenedores suelen responder en 1 día
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 85/100
lambdaclass/ethrex#7329 ·
Los mantenedores suelen responder en 1 día
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 82/100
status-im/nimbus-eth1#4867 ·
Los mantenedores suelen responder en 1 día
-
Dificultad 1/5 Menos de una hora Aptitud para principiantes 88/100
open-web3-stack/boka#399 ·