Additional Log Entries for Tracking Progress

[JKTKops]

It would be great if we could get a log entry for when the prover starts working on a proof (e.g. DebugStartedProveClaim) and also when it succeeds or fails.

On the KEVM proof suite we're trying to use the new one-line logs to collect data about which rules (or sequences of rules) are used frequently and how long they take (see runtimeverification/evm-semantics#1048). To separate different proofs in the same file, and to get an approximate duration for the first rule of each proof, we need to know when the proof started.

Additionally, we need a oneLineDoc implementation for the DebugProven entry, and something like DebugNotProven for a generic "the proof failed" entry would be quite helpful for distinguishing the last step of a proof from the last step before a timeout.

[JKTKops]

According to @ttuegel, our methodology misattributes quite a bit of non-rewriting time to rewriting. In order to do better, we would also want a log entry immediately before rewriting starts.

Also, our proofs don't branch, so we don't need to worry about that for our purposes. However since this is a change to Kore we may want to think about that if it's relevant.

[ana-pantilie]

According to @ttuegel, our methodology misattributes quite a bit of non-rewriting time to rewriting. In order to do better, we would also want a log entry immediately before rewriting starts.

What exactly are you interested in timing? Basically, the backend goes through the following loop every rewrite step:

1. We simplify the LHS and the RHS of the claim we are currently proving
2. We check the implication
3. We apply claims
4. We apply axioms
5. We simplify the LHS and the RHS again

So, are you interested in only timing 3. and 4. (the actual rewriting), or is simplification time of interest as well?

[ehildenb]

I'm interested in (1) and (4).

Specifically, I want to know if a given rule causes a lot of time to be spend in (1) the next step, or if a given rule takes a lot of time to unify/simplify side-conditions (4).

[ana-pantilie]

We should also remove DebugClaimState separately which kind of does this but is not useful.

[JKTKops]

Any more information on this? I'll go ahead on a branch and start adding the infrastructure for some new log types, but I'd need some guidance as to (1) what new things are worth logging to measure 1 and 4 above and (2) where to actually invoke the logger.

It looks to me like DebugProven, DebugAppliedRewriteRules, DebugUnification, and DebugSubstitutionSimplifier are all potentially useful. I've also locally started adding stuff for a DebugBeginClaim. It would be nice if we could get the source locations of claims for one-line logs, but based on DebugProven I'm not sure if those are available.

[ana-pantilie]

Sorry, my understanding was that @ttuegel already discussed what the next steps are, I probably just misunderstood.

So, I was thinking about DebugClaimState. Right now, this logs every transition (meaning step from the list in the comment above, we call these steps transitions) after it was executed, together with the previous configuration and the new configuration. This information is too verbose and I don't think anyone uses this log entry.

We should look into replacing this with some log entry (or entries) with separate logging actions for beginning a transition and ending one. We'll have to see what the best approach will be here, below I'm going to add a general outline to what I'd rather go with, please let me know if anyone thinks it's not going to work.

So, I'd keep this under one log entry type instead of creating separate types for each transition and scattering the logging throughout the code, so this will be a modified DebugClaimState entry type. We could change debugClaimStateBracket to log before and after. If any rules apply during that transition (which could happen if it's an ApplyClaims or ApplyAxioms transition), we should be able to extract that information from TransitionT, right? So we should have all the necessary information available: the claim, the transition, and any applied rewrite rules. This will also take care of logging if the claim is proven or stuck.

Now, about logging when we start to prove a claim, I think @JKTKops ' idea of adding DebugBeginClaim is good, I think we could log this information right before proveClaim.

[JKTKops]

If any rules apply during that transition ... we should be able to extract that information from TransitionT, right?

If I'm understanding correctly, to do this we'd want to lift the look function from Control.Monad.Trans.Accum.look and then specialize debugClaimStateBracket to TransitionT.

We'd probably want to modify DebugClaimState so that it only carries one Maybe (ClaimState SomeClaim)^1 and additionally carries a list of rules (specifically, their source locations are probably what we care about for KEVM) and an indication of if this is a 'before' log or an 'after' log^2. Then debugClaimStateBracket would log the Prim and ClaimState in a before log, and would log the Prim, optional ClaimState, and list of rules [locations only?] in an after log.

Finally, DebugClaimState probably gets renamed to DebugTransition, and gets a one-line doc format. I think it makes the most sense to separate it into DebugBeforeTransition and DebugAfterTransition. I think debugClaimStateFinal would need a DebugAfterTransition based on how it's being used now.

Does all that sound right? If so I can get to work on that.

I also noticed that some of these debugYYY functions have coerce viewPatterns in their arguments being used at Prim -> Prim. I could clean those up while I'm there, unless they're doing something I don't understand.

---

^1 Which is always present in the 'before' log but only optionally present in the 'after' log... this makes me think that maybe separating the before and after logs should be a consideration).

^2 Probably another reason to separate them.

[JKTKops]

I went ahead in the draft PR and tentatively tried to do this.

Lifting Control.Monad.Trans.Accum.look isn't good enough, because in this case we actually do want the behavior of MonadWriter.listen. Instead, I implemented a Transition.record function which behaves like listen, giving only the rules which were added during that action.

[ana-pantilie]

We'd probably want to modify DebugClaimState so that it only carries one Maybe (ClaimState SomeClaim)^1 and additionally carries a list of rules (specifically, their source locations are probably what we care about for KEVM) and an indication of if this is a 'before' log or an 'after' log^2.

I was initially thinking of separating the two cases by making the new DebugClaimState a sum type.

I think it makes the most sense to separate it into DebugBeforeTransition and DebugAfterTransition.

We could also do that, having two types would imply the following:

1. users can choose to print only "before" or only "after" logs
2. users would have to specify both log entries when wanting to see full transitions

My concern is that people would generally want to see full transitions, so it'd be more user friendly to not separate the log entries. But, if you think (1) would be useful to you, then we can go that way.

[JKTKops]

No this is a good point, I think we'd always want both. On the other hand, how would we set up specifying that we only care about the (first) simplification step and the ApplyAxioms step? (which is what Everett suspects we want) Perhaps the best way is to say "you don't get to specify that, but you can pull it out of the logged information." This seemed to be the conclusion in today's standup, so I'll go with that.