Upstream symbolic bytes lemmas for CSE
Valutazione
Questa issue non è ancora stata valutata.
Descrizione
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.
- Lingua principale
- KCL
- Stelle
- 595
- Fork
- 159
- Merge medio
- 4g 3h
- PR unite (30g)
- 1
Preparare l'ambiente
Questo progetto non fornisce container di sviluppo, Dockerfile né guida per i contributori, quindi l'ambiente è a tuo carico: parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di runtimeverification/evm-semantics
-
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 78/100
runtimeverification/evm-semantics#1190 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100
runtimeverification/evm-semantics#2879 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/evm-semantics#2869 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/evm-semantics#2832 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 30/100
runtimeverification/evm-semantics#2824 ·