Add [cast_to_bool] and factorise "if" rules.

theories/lang/heap.v

@@ -357,6 +357,15 @@ Proof.
   by rewrite !option_guard_True.
 Qed.
 
+(** ** Converting a value to a boolean (for conditionals). *)
+
+Definition cast_to_bool (ot: op_type) (v: val) (st: heap_state) : option bool :=
+  match ot with
+  | IntOp it => val_to_Z v it ≫= λ n, Some (bool_decide (n ≠ 0))
+  | PtrOp    => val_to_loc v ≫= λ l, heap_loc_eq l NULL_loc st ≫= λ b, Some (negb b)
+  | _        => None
+  end.
+
 (** ** MemCast: Transforming bytes read from memory.
   [mem_cast] is corresponds to the [abst] function in the VIP paper.
 

theories/lang/lang.v

@@ -477,13 +477,9 @@ Inductive stmt_step : stmt → runtime_function → state → list Empty_set →
     v2 `has_layout_val` (ot_layout ot) →
     heap_at l (ot_layout ot) v' start_st σ.(st_heap).(hs_heap) →
     stmt_step (Assign o ot (Val v1) (Val v2) s) rf σ [] (to_rtstmt rf end_stmt) (heap_fmap (heap_upd l end_val end_st) σ) []
-| IfSSI it v s1 s2 rf σ n:
-    val_to_Z v it = Some n →
-    stmt_step (IfS (IntOp it) (Val v) s1 s2) rf σ [] (to_rtstmt rf ((if bool_decide (n ≠ 0) then s1 else s2))) σ []
-| IfSSP v s1 s2 rf σ l b:
-    val_to_loc v = Some l →
-    heap_loc_eq l NULL_loc σ.(st_heap) = Some b →
-    stmt_step (IfS PtrOp (Val v) s1 s2) rf σ [] (to_rtstmt rf ((if b then s2 else s1))) σ []
+| IfSS ot v s1 s2 rf σ b:
+    cast_to_bool ot v σ.(st_heap) = Some b →
+    stmt_step (IfS ot (Val v) s1 s2) rf σ [] (to_rtstmt rf ((if b then s1 else s2))) σ []
 | SwitchS rf σ v n m bs s def it :
     val_to_Z v it = Some n →
     (∀ i : nat, m !! n = Some i → is_Some (bs !! i)) →

theories/lang/lifting.v

@@ -1009,8 +1009,8 @@ Lemma wps_if Q Ψ it v s1 s2 n:
   WPs (if{IntOp it}: (Val v) then s1 else s2) {{ Q , Ψ }}.
 Proof.
   iIntros (Hn) "Hs". rewrite !stmt_wp_eq. iIntros (?? ->) "?".
-  iApply wp_lift_stmt_step. iIntros (?) "Hσ".
-  iModIntro. iSplit; first by eauto 8 using IfSSI.
+  iApply wp_lift_stmt_step. iIntros (?) "Hσ". iModIntro.
+  iSplit. { iPureIntro. repeat eexists. apply IfSS. rewrite /= Hn //. }
   iIntros (???? Hstep ?) "!> !>". inv_stmt_step. iSplit; first done.
   iFrame "Hσ". case_bool_decide; by iApply "Hs".
 Qed.
@@ -1023,8 +1023,8 @@ Lemma wps_if_ptr Q Ψ v s1 s2 l:
 Proof.
   iIntros (Hl) "Hlib Hs". rewrite !stmt_wp_eq. iIntros (?? ->) "?".
   iApply wp_lift_stmt_step. iIntros (σ1) "Hσ1 !>".
-  iDestruct (wp_if_precond_heap_loc_eq with "Hlib Hσ1") as %?.
-  iSplit; first by eauto 8 using IfSSP.
+  iDestruct (wp_if_precond_heap_loc_eq with "Hlib Hσ1") as %Heq.
+  iSplit. { iPureIntro. repeat eexists. apply IfSS. rewrite /= Hl /= Heq //. }
   iIntros (???? Hstep ?) "!> !>". inv_stmt_step. iSplit; first done.
   iFrame "Hσ1". do 2 case_bool_decide => //; by iApply "Hs".
 Qed.