Roadmap to Kontrol 1.0

[PetarMax]

Required

Kontrol

• Kontrol general lemmas file included unconditionally (to be populated by @PetarMax)
• Keccak lemmas file included conditionally (PR)

KEVM

• Minor adjustments related to the pyk information-reuse PR mentioned below
• Upstreaming above to Kontrol

pyk

• Re-using information from the back-end to optimise KCFG generation (PR)
• Upstreaming above to Kontrol

Back-end

• Branch in which prelude is not checked separately every time, but only once at the start
• Upstreaning above to Kontrol
• Making --no-post-exec-simplify the default option (4012 evaluate pattern pruning haskell-backend#4020)

Optional by end-week, needed in immediate next steps (excluding CSE)

• Back-end: cutting of ground truth and prelude (super-high priority)
• Front-end + back-end: syntactic simplifications

If there are any items that I've forgotten, please feel free to edit directly.

[ehildenb]

Do we have the example Kontrol lemmas? If they are KEVM generic, then we can merge them there and already have lemma testing harnesses for them. If we put them in Kontrol, we should test them, either with Solidity property tests or KClaims.

[PetarMax]

Yes, we will merge them into KEVM as we progress. Perhaps right now we could include them in Kontrol as optional, together with the keccak lemmas, and then as they get upstreamed remove them from there, but certainly make sure that they are all upstreamed.

Right now, we keep copying them from engagement to engagement because of various time constraints.

[ehildenb]

Sounds like a good idea! Let's make a good effort to make sure there are tests in Kontrol then too!

[palinatolmach]

Closed as 1.0 has been released.