Solve failed implies in the test-prove

[Stevengre]

• Add symbolic execution rules for readByteBF in sparse-bytes.md #73 introduce simplification rules for bytes to simplify the result of readbyteBF.
• However, its corresponding test is failed with last implies request for kore-rpc-booster.
• We should solve this problem. The detailed info is in the PR.

What we need to do:

• improve the booster implies endpoint to handle this case
• find out why my \ceil simplification does not fire.

[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.