Very slow KEVM proof

[ehildenb]

On latest KEVM master, this proof takes quite a while (20x slower than Java backend).

I've attached the bug report, which I've confirmed that with Haskell backend commit b77cf98 - Simplify right-hand side of claims (#2080), it takes about 1000s on my machine (compared to about 60s on the Java backend).

kevm-bug.tar.gz

My suspects of the problem:

1. The backend doesn't support bytes-level reasoning well enough.
2. The Java-only lemmas cause some terms to be simplified out which are quite slow to reason about (investigating this one currently, it takes a while though).
3. Some other backend issue.

I was suspecting (2) for a while, but stepping through the execution with kore-repl, I don't see any very large unsimplified terms. Our definedness side-condition looks like this:

 #Ceil ( #encodeArgsAux ( .TypedArgs , 32 , b"" ++ #buf ( 32 , #getValue ( #uint256 ( A0 ) ) ) , b"" ) )
#And                      
  #Ceil ( #getValue ( #uint256 ( A0 ) ) )
#And                  
  #Ceil ( SetItem ( 1 )                                                                                                                                                                                               
  _36 )                                                                                                                                                                                                               
#And                                                                               
  #Ceil ( SetItem ( CALLEE_ID:Int )                                                                 
  _36 )                
#And                               
  #Ceil ( SetItem ( CONTRACT_ID:Int )
  _36 )                      
#And                       
  #Not ( {                                                            
    CALLEE_ID              
  #Equals                  
    1                      
  } )                   

So it could very well be the #Ceil(...) on #getValue(...), or on #encodeArgsAux(...). But I'm just not sure.