Upstream symbolic bytes lemmas for CSE
@palinatolmach ya está trabajando en esto.
Desde el 6/2/2025.
Evaluación
Este issue todavía no se ha evaluado.
Descripción
Now that we support symbolic parameters in constructors, we need lemmas to simplify expressions such as `
#dasmOpCode ( b"`\xc0`@R`\x01`\x01`\xf8\x1b\x03`\x80R4\x80\x15a\x00\x1bW`\x00\x80\xfd[P`@Qa\x01^8\x03\x80a\x01^\x839\x81\x01`@\x81\x90Ra\x00:\x91a\x00BV[`\xa0Ra\x00[V[`\x00` \x82\x84\x03\x12\x15a\x00TW`\x00\x80\xfd[PQ\x91\x90PV[`\x80Q`\xa0Q`\xe2a\x00|`\x009`\x00`}\x01R`\x00`E\x01R`\xe2`\x00\xf3\xfe`\x80`@R4\x80\x15`\x0fW`\x00\x80\xfd[P`\x046\x10`<W`\x005`\xe0\x1c\x80c\fUi\x9c\x14`AW\x80c\xa5m\xfeJ\x14`yW\x80c\xc5\xd7\x80.\x14`\x9fW[`\x00\x80\xfd[`g\x7f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`g\x7f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x81V[`g`\x01`\x01`\xf0\x1b\x03\x81V\xfe\xa2dipfsX\"\x12 }\xb9\xc9\xcfL\x8cd\x8e\xba`\xa7\xb9'\x9f\xfc\xba?\x0f\xe6\xe0\x9cDeK\x96\x12}\x19D\xd1=\fdsolcC\x00\x08\x17\x003" +Bytes #buf ( 32 , V0__y:Int ) [ 0 ] , SHANGHAI )
The lemmas should look like this:
//
// Alternative memory lookup
//
rule [bytes-concat-lookup-left]:
( B1:Bytes +Bytes B2:Bytes ) [ I:Int ] => B1 [ I ]
requires 0 <=Int I andBool I <Int lengthBytes(B1)
[simplification(40), preserves-definedness]
rule [bytes-concat-lookup-right]:
( B1:Bytes +Bytes B2:Bytes ) [ I:Int ] => B2 [ I -Int lengthBytes(B1) ]
requires lengthBytes(B1) <=Int I
[simplification(40), preserves-definedness]
rule [lookup-as-asWord]:
B:Bytes [ I:Int ] => #asWord ( #range ( B, I, 1 ) )
requires 0 <=Int I andBool I <=Int lengthBytes(B)
[simplification(60)]
Once upstreamed, we can remove this lemmas file from Kontrol test suite.
- 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 ·