hoare_vcg_prop (in default wp set) throws away non-throw information

[Xaphiosis]

After discussing with @corlewis we didn't end up with a consensus on what if anything should be done about it.

In this situation:

 1. ⦃λ_. True⦄
    if UCAST(9 → 64) minIRQ ≤ irq ∧ irq ≤ Kernel_Config.maxIRQ then returnOk ()
    else throwError (Fault_H.syscall_error.RangeError (UCAST(9 → 64) minIRQ) Kernel_Config.maxIRQ) 
    ⦃λ_ _. toEnum (unat irq) ≤ Kernel_Config.maxIRQ⦄, ⦃λ_ _. True⦄

which is obviously true, if I ask wp to handle it, it gives me:

True ⟹ toEnum (unat irq) ≤ Kernel_Config.maxIRQ

which is obviously not true; I need to instead do this:

  apply (clarsimp simp: unlessE_def) (* don't block the if_split *)
  apply (rule conjI; clarsimp)
  apply wp (* non-throw case: gives provable goal *)
defer
  apply wp (* throw case: solves goal outright *)

With supply hoare_vcg_prop[wp del], I get the expected outcome:

True ⟹
        (UCAST(9 → 64) minIRQ ≤ irq ∧ irq ≤ Kernel_Config.maxIRQ ⟶ toEnum (unat irq) ≤ Kernel_Config.maxIRQ) ∧
        (¬ (UCAST(9 → 64) minIRQ ≤ irq ∧ irq ≤ Kernel_Config.maxIRQ) ⟶ True)

which simplifies to the one case I want:

⟦UCAST(9 → 64) minIRQ ≤ irq; irq ≤ Kernel_Config.maxIRQ⟧ ⟹ toEnum (unat irq) ≤ Kernel_Config.maxIRQ

So in this case our infrastructure is throwing info away. I tried rewriting the unlessE to a whenE, but that didn't change anything.

[corlewis]

For a bit more detail, my current thinking is that the problem in this case is that

hoare_vcg_prop: f ⦃λs. P⦄

is being applied by wp immediately, which means that the extra information from the if isn't being used.

In our setup we do have this comment,

hoare_vcg_prop is unsafe in certain circumstances but still useful to have applied automatically,
   so we make it the very last rule to be tried.

which is talking about exactly this problem. I haven't investigated further, but I now guess that what is happening is that hoare_vcg_prop is the last wp rule tried but it's still used before any wp_split rules, which is where the needed hoare_vcg_if_split rule lives. More thought is needed for if there's a better way of doing this.

[lsf37]

but I now guess that what is happening is that hoare_vcg_prop is the last wp rule tried but it's still used before any wp_split rules, which is where the needed hoare_vcg_if_split rule lives. More thought is needed for if there's a better way of doing this.

That sounds precisely right. Would it be possible to put hoare_vcg_if_split in as a normal wp rule (instead of a split rule) before hoare_vcg_prop?

[corlewis]

but I now guess that what is happening is that hoare_vcg_prop is the last wp rule tried but it's still used before any wp_split rules, which is where the needed hoare_vcg_if_split rule lives. More thought is needed for if there's a better way of doing this.

That sounds precisely right. Would it be possible to put hoare_vcg_if_split in as a normal wp rule (instead of a split rule) before hoare_vcg_prop?

Do you mean to do that locally to resolve the specific goal, or change it globally? If doing it globally I imagine there's lots of other split rules that we'd also want to trigger first, in which case it might make more sense to do the reverse and move hoare_vcg_prop to some new set that actually is tried last.

[corlewis]

but I now guess that what is happening is that hoare_vcg_prop is the last wp rule tried but it's still used before any wp_split rules, which is where the needed hoare_vcg_if_split rule lives. More thought is needed for if there's a better way of doing this.

That sounds precisely right. Would it be possible to put hoare_vcg_if_split in as a normal wp rule (instead of a split rule) before hoare_vcg_prop?

Do you mean to do that locally to resolve the specific goal, or change it globally? If doing it globally I imagine there's lots of other split rules that we'd also want to trigger first, in which case it might make more sense to do the reverse and move hoare_vcg_prop to some new set that actually is tried last.

Another option is to add hoare_vcg_prop to wp_unsafe, so that it's suggested when it could be used but isn't automatically applied. The problem there though is that since we never made much use of wp_unsafe I think we've all been trained into ignoring the message that it does sometimes print.

[lsf37]

Do you mean to do that locally to resolve the specific goal, or change it globally? If doing it globally I imagine there's lots of other split rules that we'd also want to trigger first, in which case it might make more sense to do the reverse and move hoare_vcg_prop to some new set that actually is tried last.

I meant globally, but it's not clear how much that would change the current behaviour. Having a set that is tried last is not a bad idea, it would be useful for a few other things as well.

Another option is to add hoare_vcg_prop to wp_unsafe, so that it's suggested when it could be used but isn't automatically applied. The problem there though is that since we never made much use of wp_unsafe I think we've all been trained into ignoring the message that it does sometimes print.

It's also used quite a bit in the current proofs, so we'd need to add it explicitly everywhere where that is the case.