Assertion reducer

[pieter-bos]

It's a common technique to add a bunch of assertions as intermediate steps if a proof goal fails. Once that repairs the proof goal, some of the assertions may still be necessary as a proof step, but many are probably superfluous. It might be nice if VerCors can run the verifier a bunch of times and automatically infer which assertions do not improve the verification time and/or maintain the proof.

[ArmborstL]

Some more detailed thoughts:

• assertion reduction: which assertions are needed to guide the prover?

  • kick out assert, see if program still verifies
  • question: what is good order of kicking out, taking into account dependencies between asserts?
    • do we need multiple runs to check interdependent asserts, searching for something like a fixpoint?
    • it might be enough to kick out asserts from bottom to top in a one-pass approach
  • question: if assert speeds up verification but does not influence the verification result, does that justify keeping it? What speedup is a good threshold for keeping? (see also profiling below)
  • question: stability: Some asserts may ensure that the prover always returns the same result, within the same execution time. Removing the assert may mean that the verification becomes unstable. How to handle that? Multiple runs for each removed assert to check stability?
  • how to report results? Print a pvl/java/... file only containing necessary asserts, completely removing others? Just comment out?
  • lift to other proof goals, like loop invariants

• assertion profiling: how long does each assertion take? Which ones are holding up verification?

  • links to speedup question above
  • silicon/z3 report timing of their proof goals, but their proof goals do not exactly match assertions in VerCors frontend
    -> need to link backend ticks back to frontend assertions
    • use origin system to group proof goals? I.e. all proof goals with the same origin are considered one single frontend assertion
      • a bit hacky (origins are not always precise; maybe wonky if not file origin but e.g. stdin)
    • use blame, redirect ticks on silicon nodes to be ticks on frontend nodes
      • more work (need to implement it for every node type)
  • how to report results? annotated pvl.java/... file with times after each assert? printing table in console?
  • lift to other proof goals, like loop invariants

• frontend: How to use these tools?

  • CLI flags?
  • inline code annotations to turn on/off for specific block?