Pass all relevant information from Kontrol to KaaS

[PetarMax]

Currently, KaaS requires of a user to upload the out folder of the project, that is, the kompiled definition and the associated proofs. For users of KaaS us to be able to reproduce the proofs themselves, and also for us to be able to use KaaS to run proofs more efficiently, I think that it would be good to include at least the following information somewhere in the out folder, possibly in the digest file:

1. the version of Kontrol used to kompile the definition and run the proofs;
2. the full command used to kompile the definition - this is relevant because perhaps lemmas have been incorporated, etc.
3. the commit hash of the project at the time of kompilation and proof-running.

These three would allow both KaaS and any user to re-create the definition, assuming it is able to access the project repository, so perhaps if we had this information we would not need to upload the entire out folder. In discussion with @ehildenb, it came up that definitions may vary slightly from machine to machine (say, Ubuntu vs. Mac) so having the above info might even be essential.

The situation is a bit more complex when it comes to replaying the proofs, because the KCFGs could have been created bit-by-bit, using a number of different kontrol prove commands, and modified using node refutations, unrefutations, deletions, etc. If we wanted to replicate a specific KCFG at hand, we would, I think, have to store all the specific commands used, together with some indicators of how long they were executed for (in the sense of if I ran a command with max-iterations set to 100, but stopped the execution after 25, I would ideally record the 25).

If we don't care about fully replaying KCFGs but rather being able to inspect them and continue execution, then we could potentially provide to KaaS the values of the parameters that we expect the proof to be continued with (e.g., max-depth, max-iterations, etc.).

[palinatolmach]

After a discussion with @yale-vinson and @F-WRunTime today, we've decided to

• add Kontrol version and kontrol build command used to build a project to the digest file
• add a command, e.g., kontrol digest-check, to generate a new digest file without having to run kontrol build
• this command generates a digest-diff file if there're changes from the previous digest file, and just creates a digest file if there's no previous file This information can then be used by KaaS to make a decision on whether there's a need to rekompile the project.

[F-WRunTime]

This could help provide useful information to the user when they run remote compute jobs. Having in the list of jobs executed a compute entry could show the flags passed to kontrol build / prove within the 'tile' for that job.