Simplifications not applied when running `foundry-prove` using the booster backend

[lucasmt]

When running a certain proof with kevm foundry-prove with the --use-booster option, I get a branching condition as follows, where BUF is a large b"..." expression (that I believe corresponds to some contract bytecode):

{ true #Equals #asWord ( #range ( #buf ( 32 , ( maxUInt160 &Int #lookup ( ?STORAGE:Map , 3 ) ) ) +Bytes #buf ( 32 , #lookup ( ?STORAGE2:Map , 0 ) ) +Bytes #buf ( 32 , #lookup ( ?STORAGE3:Map , 0 ) ) +Bytes #buf ( 32 , #lookup ( ?STORAGE4:Map , 0 ) ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00.#M\xaeu\xc7\x93\xf6z5\x08\x9c\x9d\x99$^\x1cXG\x0b" +Bytes #buf ( 32 , #lookup ( ?STORAGE0:Map , 4 ) ) +Bytes BUF , 160 , 32 ) ) <=Int maxUInt64 }

However, this expression could be simplified down to #lookup ( ?STORAGE0:Map , 4 ) <=Int maxUInt64 by applying the following two lemmas, which already exist in bytes-simplification.k:

    rule [range-included-in-cHead]:
      #range(B1:Bytes +Bytes _:Bytes, S:Int, W:Int) => #range(B1, S, W)
      requires S +Int W <=Int lengthBytes(B1)
      [simplification]

    rule [range-outside-cHead]:
      #range(B1:Bytes +Bytes B2:Bytes, S:Int, W:Int) => #range(B2, S -Int lengthBytes(B1), W)
      requires lengthBytes(B1) <=Int S
      [simplification]

In fact, if I run the above expression as a runLemma/doneLemma claim, it does simplify as expected. Also, if the same proof is run using the legacy backend instead of the booster, the expression is also simplified. I don't know why the lemmas are not being applied when running the proof with the booster.

I have shared a bug report with @geo2a for a previous version of the proof that was exhibiting the same problem (but with a different expression). In both cases the same two lemmas above are not being applied.

[ehildenb]

The booster doesn't apply rule that have side-conditions in them. But perhaps it could call the simplify endpoint before passing the term back, to make sure that returned terms are fully simplified?

Or perhaps we can do that from the pyk side?

[goodlyrottenapple]

@lucasmt would it be possible to generate a bug_report for a state just before this branch? we could then start booster with -l Rewrite -l Simplify and get a trace of the attempted rewrite + simplifications. That should hopefully tell us whether the booster even attempts to apply the above rules and if it does, why does it fail...

[JuanCoRo]

I got non-appliance of rules when running the legacy backend. So it could be that this is not only related to the booster after all. In this case, the branching conditions are simplified correctly, but not the cells of the configuration (such as <output>). A claim for the expected simplification of the cell passes as well.

[geo2a]

We now have an experimental branch in Booster that calls the legacy simplifier in case of the branching result. This is roughly equivalent to calling simplify from pyk, but happens withing Booster.

I've tested the execute request mentioned above, and the K cell in the response now looks like:

      <k>
        JUMPI 10880 bool2Word ( maxUInt160 &Int #lookup ( ?STORAGE7:Map , 3 ) ==Int 0 )
        ~> #pc [ JUMPI ]
        ~> #execute
        ~> CONTINUATION:K
      </k>

Unfortunately, overriding kore-rpc-booster with kup seems broken now. Therefore, to use the experimental branch with KEVM, one needs to:

• build hs-backend-booster from source of the experimental branch using the build instructions. I can help with the Haskell stuff.
• Run proofs with kevm foundry-prove --kore-rpc-command 'kore-rpc-booster --simplify-after-exec', making sure to use the locally built executable from step one.

[geo2a]

@lucasmt I have updates:

• the --simplify-after-exec option has been merged to main (#249)
• kup has been patched and can now be used to override Booster in KEVM. Use kup update kevm --override k-framework/booster-backend main. Non need to build Booster from source anymore.

I think we could close this issue now.