Weakest preconditions for total program correctness

This MR implements weakest preconditions for total program correctness using a least fixpoint (as suggested by @abizjak). These weakest preconditions are defined without the later modality, so one can only open invariants whose contents is timeless.

Note that for the case of concurrency, these total weakest preconditions are probably not so useful: one typically wants to prove something like totality assuming fair scheduling. To do that, we probably need something TotalTaDa-ish, but that is beyond the scope of this MR. The weakest preconditions in this MR are intended mainly to be used for sequential code.

TODO

• Prove generic weakest precondition lemmas
• Prove adequacy
• Prove the lifting lemmas
• Implement proofmode support, this depends on !64 (merged)
• Wait for !71 (merged) to be merged.

theories/heap_lang/lib/assert.v

@@ -9,6 +9,13 @@ Definition assert : val :=
 (* just below ;; *)
 Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
 
+Lemma twp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
+  WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗ WP assert: e @ E [{ Φ }].
+Proof.
+  iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
+  wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
+Qed.
+
 Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
   WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP assert: e @ E {{ Φ }}.
 Proof.