Upstream symbolic bytes lookup, List membership lemmas
#2702
Conversation
palinatolmach
changed the title
bytes lookup lemmas for symbolic immutablesbytes lookup, List membership lemmas
|
|
||
| rule [lookup-as-asWord]: | ||
| B:Bytes [ I:Int ] => #asWord ( #range ( B, I, 1 ) ) | ||
| requires 0 <=Int I andBool I <=Int lengthBytes(B) |
There was a problem hiding this comment.
Shouldn't this be I <Int lengthBytes(B) instead?
There was a problem hiding this comment.
You're right, it should be, thank you @lucasmt! It is I <Int lengthBytes(B) in the rule we're using in Kontrol, I'll update it here. I guess I should also make sure Kontrol tests are passing with this version of KEVM, I'll open a PR in Kontrol checking that and will merge it — with the <Int change — if they're passing.
There was a problem hiding this comment.
Fixed in d38bec6.
|
I opened a PR in Kontrol to test if upstreamed lemmas don't negatively affect the tests and are applied if I take out the same lemmas from Kontrol aux files. The tests are passing: runtimeverification/kontrol#1059 (there's a minor expected output diff in some |
Closes #2476.
This PR adds lemmas for lookups in partially symbolic
bytesarrays; specifically, in runtime bytecode of contracts that containimmutablevariables that are initialized in a constructor with a symbolic value. It also addsListmembership lemmas that facilitate checking if a performed call is allowed in Kontrol when theallowCallscheatcode is used.Once this PR is merged, the relevant lemmas should be removed from
KONTROL-AUX-LEMMASand https://github.com/runtimeverification/kontrol/blob/master/src/tests/integration/test-data/symbolic-bytes-lemmas.k.