Skip calling `kompile` when doing `kontrol build`

[ehildenb]

Currently, when working with a Kontorl project, every change to the Soldiity code results in having to call kompile again. This is because we generate K code representing sugar for that specific contract and use that sugar in the proofs. In general, this isn't really necessary, we only are doing this to introduce macros for prettier syntax, and it slows down development of Kontrol proofs quite a bit.

We should:

• Some initial cleanup. Eliminate deadcode from the Python codebase #976
• Avoid generating any of the calldata sugar rules, instead generate the needed calldata directly in the proof init states. Also avoid generating the selector aliases. Do not generate calldata sugar rules #978
• Simplify the generated module structure now that no rules are being generated. Simplify generated module structure #1003
• Build different versions of Kontrol for each lemma body directly (--no-aux-lemmas and --keccak-lemmas), so they don't need to be included at kontrol build ... time. Prebuild optimized definition #1002
• Do not rekompile the K definition when only Solidity code changes: Do not rekompile on Solidity code changes #1007.
• Minor cleanups to how extra lemmas are included in kontrol prove ..., and extending it to be included in all commands which use the RPC server. Also minor cleanups in kontrol build ... options parsing: Update/generalize option to include lemmas at prove time #979.
• No need to actually build the base Kontrol definitions, other than to make sure that they do build. Maybe on CI we can shorten time by not building them? Maybe if a user is not supplying --requires ... --module-imports ... we could also have faster kontrol build ... time by just using one of the prebuilt base modules directly?
• Final cleanup and deadcode elimination.
  • Use deadcode src/
  • DONE: It's unclear if functions like gen_bin_runtime, bin_runtime, solc_to_k, etc... are used for anything except testing at this point. So they can probably be removed and then the repo updated/simplified quite a bit without them. Remove kontrol solc-to-k ... and related deadcode #1005
• Update Kontrol documentation with the following points:
  • How to use kontrol prove ... --lemmas LEMMAS-FILE:LEMMAS-MODULE (renamed from --extra-module).
  • How to know when to rekompile or not (currently we recommend to rekompile when solidity code changes: Do not rekompile on Solidity code changes #1007 (comment)).
  • Subsumed: Updates to Kontrol Documentation #1018

[tothtamas28]

Related:

• Make calldata sugar generation optional #170