Dealing with Missing Type Instances

Follow Along by downloading the Rocq source of this tutorial, or the full docs tarball.
Some code is deliberately elided for presentation purposes, the full, working source code can be downloaded with the above link.

Sometimes, a proof will get stuck because the automation can not prove the a reference is valid. In these cases, the proof usually gets stuck on a reference_to<ty> p obligation.

A contrived program that exhibits this behavior is:

struct C {};
void test(C c) {
  C& r{c};
}

This proof gets stuck on the following goal:

Lemma test_ok : verify[source] "test(C)".
Proof.
  verify_spec.
  go.

  _ : c_addr |-> CR q
  --------------------------------------∗
  reference_to "C" c_addr ∗
  (r_addr |-> refR<"C"> 1$m c_addr -∗
   interp source 1
     (wp_decls source [region: "r" @ r_addr; "c" @ c_addr; return {?: "void"}] []
        (λ (ρ : region) (free' : FreeTemps),
           ▷ wp_block source ρ []
               (Kfree source (free' >*> FreeTemps.delete "C&" r_addr)
                  (Kcleanup source [] (Kreturn (λ v : ptr, ▷ _PostPred_ v)))))))

The automation is stuck verifying this goal because it can not prove the reference_to "C" c_addr obligation.

Solution: Add a Hint

This is most commonly solved using a Typed hint on the class. The following code creates this hint automatically.

  #[only(type_ptr="C")] derive CR.

After introducing the hint, the automation can make progress.

In this case, #[only(type_ptr)] derive CR. is also sufficient, because the automation can infer the type C from CR's definition.

go.