requires "evm.md" module BUF-SYNTAX imports EVM
#bufStrict(SIZE, DATA) and
#buf(SIZE, DATA) represents a symbolic byte array of length
SIZE bytes, left-padded with zeroes.
#bufStrict is partial and only defined when
DATA is in the range given by
It rewrites to
#buf when data is in range, and is expected to immediately evaluate into
#buf in all contexts.
#buf is total and artificially defined
modulo 2 ^Int (SIZE *Int 8).
This division is required to facilitate symbolic reasoning in Haskell backend, because Haskell has limitations
when dealing with partial functions.
Usage: All symbolic byte arrays must be originally created as
#buf is never present in out of range mode.
For this, definition rule RHS should always use
#bufStrict when array is first created, but may use
#buf when array
is just carried on from LHS without changes. Definition rule LHS should only use
Claims should always use
#bufStrict in LHS and
#buf in RHS.
syntax ByteArray ::= #bufStrict ( Int , Int ) [function] syntax ByteArray ::= #buf ( Int , Int ) [function, functional, smtlib(buf)] endmodule module BUF imports BUF-SYNTAX imports BUF-KORE rule #bufStrict(SIZE, DATA) => #buf(SIZE, DATA) requires #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) rule #buf(SIZE, DATA) => #padToWidth(SIZE, #asByteStack(DATA %Int (2 ^Int (SIZE *Int 8)))) [concrete] endmodule module BUF-KORE [kore, symbolic] imports BUF-SYNTAX rule #bufStrict(_, _) => #Bottom [owise] endmodule