Skip to content

Instantly share code, notes, and snippets.

@sskeirik

sskeirik/byte-manipulation-lemmas.k

Created March 21, 2020 03:36
Show Gist options
  • Save sskeirik/06d8bf552202679d2ea2e5392cef9794 to your computer and use it in GitHub Desktop.
Save sskeirik/06d8bf552202679d2ea2e5392cef9794 to your computer and use it in GitHub Desktop.
Download ZIP
KWasm Lemmas for Byte Manipulation
Raw
byte-manipulation-lemmas.k
rule lengthBytes(B1 +Bytes B2) => lengthBytes(B1) +Int lengthBytes(B2) [simplification]
rule substrBytes(B1 +Bytes B2, START, END)
=> substrBytes(B1, START, END)
requires lengthBytes(B1) >=Int END
[simplification]
rule substrBytes(B1 +Bytes B2, START, END)
=> substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1))
requires lengthBytes(B1) <=Int START
[simplification]
rule substrBytes(B1 +Bytes B2, START, END)
=> substrBytes(B1, START, lengthBytes(B1)) +Bytes
substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1))
requires notBool (lengthBytes(B1) >=Int END)
andBool notBool (lengthBytes(B1) <=Int START)
[simplification]
rule substrBytes(B, 0, END) => B
requires lengthBytes(B) ==Int END
[simplification]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment