Add symbolic execution rules for readByteBF in sparse-bytes.md

[Stevengre]

Enhance symbolic execution capabilities by introducing new rules to handle patterns of #bytes(B +Bytes _) _ and #bytes(B +Bytes BS) EF, allowing for more precise value retrieval in readByte.

This update improves the accuracy of symbolic execution in the context of byte reading operations.

[tothtamas28]

What's the issue here specifically?

[Stevengre]

The target node and the final node is syntatically the same. But the prover cannot return a correct result.

[Stevengre]

Here is the response from @jberthold:

I ran the last implies request 038 from your bug report, and got the following back (consistent with the response saved in the bug report):

$ jq .result.condition.predicate implies-response.json | ../../.build/kore/bin/pretty definition.kore /dev/stdin 
Pretty-printing predicates:
Bool predicates:
  kseq(
      signExtend( VarY:SortBytes{} [ "3" ] <<Int "8" |Int VarY:SortBytes{} [ "2" ] <<Int "8" |Int VarY:SortBytes{} [ "1" ] <<Int "8" |Int VarY:SortBytes{} [ "0" ] , "32" ),
      dotk
  ) ==K kseq(
      signExtend( VarY:SortBytes{} [ "3" ] <<Int "8" |Int VarY:SortBytes{} [ "2" ] <<Int "8" |Int VarY:SortBytes{} [ "1" ] <<Int "8" |Int VarY:SortBytes{} [ "0" ] , "32" ),
      dotk
  )
Ceil predicates:
  \ceil{}(VarY:SortBytes{} [ "0" ])
  \ceil{}(VarY:SortBytes{} [ "1" ])
  \ceil{}(VarY:SortBytes{} [ "2" ])
  \ceil{}(VarY:SortBytes{} [ "3" ])
Substitution:

In the logs I can see that the request is handled completely by kore (the legacy backend), not by booster.
So the legacy backend says that the implication holds under the printed conditions.

• The "Bool predicate" that signExtend(thing) == signExtend(thing), which is actually trivial, because thing is syntactically the same term. However, the legacy backend does not accept that to be automatically the same, because of
• the four \ceil predicates, saying that indexing with 0, 1, 2 and 3 into the Bytes in Y is defined. (so the legacy backend is cautious not to even accept the syntactic identity).

The request does not have any condition about the lengthBytes of Y . Maybe worth a shot adding a condition 3 <=Int length(Y) ? Howeverin the definition.kore I could not find any \ceil rules about BYTES.get (which is the implementation of the indexing _ [ _ ] on bytes.

Another thing that you could try is to add an "assume-defined": true to the parameters, then booster will try to run the implication (booster does not consider ceil requirements). Of course that means you as the caller have to be certain that your Y is long enough (four bytes at least).

[Stevengre]

But I think that the problem is not caused by the definedness problem, because:

• I still failed to pass this implies even I use "assume-defined": true
• I still fiailed after introducing the following simplification rule:

rule #Ceil(@X:Bytes[@I:Int]) => {(lengthBytes(@X) >Int @I) #Equals true} #And #Ceil(@X) #And #Ceil(@I) [simplification]

However, since I don't quite understand how the definedness transforms from / between the terms, I don't know if there any other rules should I introduce.

Additionally, I don't quite understand the preserve-definedness attribute for the simplification rules.

[Stevengre]

Becuase this is not trivial to solve this problem, I want to skip it now and may construct a small example to explore how to solve the problem.

BTW, I think the implies problem is not urgent. Because even we introduced these simplification rules to simplify the read process, it can still be some gap for verifying add here.

[tothtamas28]

I want to skip it now

Sure. Please open an issue for tracking purposes.

[jberthold]

I want to skip it now

Sure. Please open an issue for tracking purposes.

Yes, please open an issue and I can attach the information that we only have in slack at the moment. We want to a) improve the booster implies endpoint to handle this case, and b) find out why your \ceil simplification does not fire.

[Stevengre]

Sorry for my late reply. Here is the issue to this problem: #80