Formal professional services

[rainbreak]

previous latest run from https://github.com/dapphub/k-dss/pull/39: https://dapp.ci/k-dss/4296d527e38631f8b756/

796/812 accepted proofs.

Remaining problem areas:

• vat lemmas for fold/grab/frob/fork fail cases
• skip/bite pass cases
• end.cage k performance (oom currently)
• drip fail cases are entering rpow loop and timing out
• flapper.tend fail case timing out

[MrChico]

I have corrected the mul lemma me and @livnev found a problem with yesterday:

444c444
< rule A *Int #unsigned(B) => #unsigned(A *Int B)
---
> rule A *Word #unsigned(B) => #unsigned(A *Int B)

but since it is in lemmas.k.md this will trigger rerun (and we haven't tested whether this causes problems)

[mhhf]

@rainbreak something we changed yesterday let us make progress with cat bite, however - the constraints seems to be codependent :(

[livnev]

@rainbreak @MrChico can this be merged?

[MrChico]

Fine by me

[gbalabasquer]

Guys can this be merged, please?

[gbalabasquer]

Thanks!