Rules for substrBytes

[hjorthjort]

It was suggested these rules from the Ewasm semantics should be upstreamed.

[dwightguth]

If these are intended for use for the haskell backend, they should not be in a module marked [kast].

[ehildenb]

They should specifically be in a module marked kore (llvm and haskell backends), or symbolic, kore (haskell backend). kast is for ocaml/java backend.

[hjorthjort]

It should be for the Haskell backend. Looking here, I assume the module should be named BYTES-KORE-SYMBOLIC. https://github.com/kframework/k/blob/e45e3d9359f428680a4c07c494cb831fc8636ef4/k-distribution/include/builtin/domains.k#L161

[hjorthjort]

Not sure about what the right import is: BYTES-IN-K or BYTES-KORE. The lemmas are based on the semantics described in BYTES-IN-K.

[dwightguth]

It should probably import BYTES-KORE because that's what the haskell backend uses.

[ehildenb]

@hjorthjort please update this to (i) remove all the #Ceil rules, and (ii) port to the markdown format files.

[ehildenb]

Closing as this is likely outdated and has horrible conflicts at this point. Re-open if still needed @hjorthjort .