search

runtimeverification / kontrol

BSD 3-Clause "New" or "Revised" License
46 stars 5 forks source link

add_invariant is called on unsimplified term #295

Open dwightguth opened 7 months ago

dwightguth commented 7 months ago

In prove.py, KEVM.add_invariant is called. This function takes the contents of the callData cell and adds a predicate asserting something about the length of the callData. Because the term it is called on is unsimplified, it contains function symbols that when evaluated, add new constraints to the path condition. The necessity of supporting the equations needed in the Maude backend to propagate these constraints correctly causes the time spent loading KEVM in the Maude backend to increase from 2 seconds to 15 seconds. Ideally, we would simplify the term we create, then add the invariant using the simplified term. This is not hugely urgent, but it causes quite significantly quality of life improvement for developers working on improving the Maude backend's support for kontrol, so I'd like to know what might be able to be done.

palinatolmach commented 4 months ago

@dwightguth @ehildenb is Maude backend being worked on at the moment? If not, shall we deprioritize simplifying the term before passing it to add_invariant?