more efficient variant of check_has_ty_conditions

theories/lang/bitfield.v

@@ -65,7 +65,7 @@ Lemma ensure_mv_spec (σ : signature) t :
   has_ty t (mv σ).
 Proof.
   unfold ensure_mv. move => ?.
-  apply check_has_ty_spec. { by rewrite check_has_ty_conditions_mv_nil. }
+  apply check_has_ty_mv_spec.
   have ? := is_Some_None. case_match; naive_solver.
 Qed.
 
@@ -73,7 +73,7 @@ Definition ensure_bv (σ : signature) (t : tm) : option () :=
   if check_has_ty t (bv σ) then Some () else None.
 
 Lemma ensure_bv_spec σ t :
-  Forall id (check_has_ty_conditions t (bv σ)) →
+  Forall id (check_has_ty_conditions t None) →
   is_Some (ensure_bv σ t) →
   has_ty t (bv σ).
 Proof.
@@ -89,8 +89,8 @@ Definition ensure_both_bv (R : Type) `{BitfieldDesc R} (tp : tm * tm) : option (
   end.
 
 Lemma ensure_both_bv_spec R `{BitfieldDesc R} t1 t2 :
-  Forall id (check_has_ty_conditions t1 (bv bitfield_sig)) →
-  Forall id (check_has_ty_conditions t2 (bv bitfield_sig)) →
+  Forall id (check_has_ty_conditions t1 None) →
+  Forall id (check_has_ty_conditions t2 None) →
   is_Some (ensure_both_bv R (t1, t2)) →
   has_ty t1 (bv bitfield_sig) ∧ has_ty t2 (bv bitfield_sig).
 Proof.
@@ -118,7 +118,7 @@ Proof.
   move => ? ? Hs. econstructor; eauto.
   unfold ensure_or_cond in Hs.
   have ? := is_Some_None. repeat case_match; last naive_solver.
-  - right. apply check_has_ty_spec => //. by rewrite check_has_ty_conditions_mv_nil.
+  - right. by apply check_has_ty_mv_spec.
   - left. by apply check_disjoint_spec.
 Qed.
 
@@ -132,14 +132,14 @@ Definition ensure_or_cond_raw σ (tp : tm * tm) : option bool :=
 Lemma ensure_or_cond_raw_spec σ t1 t2 b :
   has_ty t1 (bv σ) →
   ensure_or_cond_raw σ (t1, t2) = Some b →
-  (if b then Forall id (check_has_ty_conditions t2 (bv σ)) else True) →
+  (if b then Forall id (check_has_ty_conditions t2 None) else True) →
   has_ty (bf_or t1 t2) (bv σ).
 Proof.
   move => ? Hs ?. unfold ensure_or_cond_raw in Hs.
   destruct (check_has_ty t2 (mv σ)) eqn:?; simplify_eq.
   - econstructor; eauto.
-    * apply subsume_mv_bv. apply check_has_ty_spec => //. by rewrite check_has_ty_conditions_mv_nil.
-    * right. apply check_has_ty_spec => //. by rewrite check_has_ty_conditions_mv_nil.
+    * apply subsume_mv_bv. by apply check_has_ty_mv_spec.
+    * right. by apply check_has_ty_mv_spec.
   - destruct (check_has_ty t2 (bv σ)) eqn:?; simplify_eq.
     destruct (check_disjoint (ranges t1) (ranges t2)) eqn:? => //; simplify_eq/=.
     econstructor; eauto.

theories/mask_core/typecheck.v

@@ -77,68 +77,68 @@ Fixpoint check_has_ty (t' : tm) (τ : ty) : bool :=
   | _, _ => false
   end.
 
-Fixpoint check_has_ty_conditions (t : tm) (τ : ty) : list Prop :=
-  match t, τ with
-  | bf_val n, val σ f =>
-      [0 ≤ n < 2 ^ (field_width σ f)]
-  | bf_mask k, val σ f => []
-  | bf_nil, bv σ => []
-  | bf_cons r x t, bv σ =>
-    default [] (
-      f ← recognize σ r;
-      Some (check_has_ty_conditions x (val σ f) ++ check_has_ty_conditions t (bv σ))
-    )
-  | bf_slice r t, val σ f => check_has_ty_conditions t (bv σ)
-  | bf_update r x t, bv σ =>
-    default [] (
-      f ← recognize σ r;
-      Some (check_has_ty_conditions x (val σ f))
-    )
-  | bf_and t1 t2, bv σ =>
-    check_has_ty_conditions t1 (bv σ)
-  | bf_and_neg t1 t2, bv σ =>
-    check_has_ty_conditions t1 (bv σ)
-  | bf_or t1 t2, bv σ =>
-    check_has_ty_conditions t1 (bv σ) ++ check_has_ty_conditions t2 (bv σ)
-  | _, _ => []
+Fixpoint check_has_ty_conditions (t : tm) (r : option range) : list Prop :=
+  match t with
+  | bf_val n =>
+      [if r is Some r' then 0 ≤ n < 2 ^ width r' else False]
+  | bf_cons r x t =>
+      check_has_ty_conditions x (Some r) ++ check_has_ty_conditions t None
+  | bf_slice r t => check_has_ty_conditions t None
+  | bf_update r x t =>
+      check_has_ty_conditions x (Some r)
+  | bf_and t1 t2 =>
+    check_has_ty_conditions t1 None
+  | bf_and_neg t1 t2 =>
+    check_has_ty_conditions t1 None
+  | bf_or t1 t2 =>
+    check_has_ty_conditions t1 None ++ check_has_ty_conditions t2 None
+  | _ => []
   end.
 
-Lemma check_has_ty_conditions_mv_nil t σ :
-  check_has_ty_conditions t (mv σ) = [].
-Proof. by destruct t. Qed.
+Lemma check_has_ty_mv_conditions t σ:
+  check_has_ty t (mv σ) = true → Forall id (check_has_ty_conditions t None).
+Proof. Admitted.
 
 Lemma check_has_ty_spec t τ :
-  Forall id (check_has_ty_conditions t τ) →
+  Forall id (check_has_ty_conditions t (if τ is val σ f then Some (sig_ranges σ !!! f) else None)) →
   check_has_ty t τ = true →
   ⊢ t : τ.
 Proof.
   move : τ. induction t; destruct τ => //=.
   all: try match goal with
   | |- context [ (?o ≫= _) ] =>
-    destruct o eqn:Heqn; simpl; try done
+    destruct o eqn:Heqn; simpl; try done; try (move: (Heqn) => /recognize_spec?)
   end.
   all: repeat case_match => //=.
   all: rewrite ?andb_true_iff ?range_ltb_head_spec ?range_eqb_spec ?Z.eqb_eq ?Nat.eqb_eq ?Fin.eqb_eq ?orb_true_iff.
-  all: rewrite ?Forall_app ?Forall_cons_iff ?Forall_singleton.
+  all: rewrite ?Forall_app ?Forall_cons_iff ?Forall_singleton /=.
   all: intros.
   all: repeat match goal with
   | [ H : _ ∧ _ |- _ ] => destruct H as [? ?]
   | [ H : _ ∨ _ |- _ ] => destruct H as [?|?]
   end => //; subst.
   all: try by repeat (econstructor; eauto).
-  all: try have ? : Forall id (check_has_ty_conditions t1 (mv σ)) by rewrite check_has_ty_conditions_mv_nil.
-  all: try have ? : Forall id (check_has_ty_conditions t2 (mv σ)) by rewrite check_has_ty_conditions_mv_nil.
+  all: try have ? : Forall id (check_has_ty_conditions t1 None) by apply: check_has_ty_mv_conditions; eassumption.
+  all: try have ? : Forall id (check_has_ty_conditions t2 None) by apply: check_has_ty_mv_conditions; eassumption.
   all: repeat (econstructor; eauto).
   - apply subsume_mv_bv. eauto.
   - by apply check_disjoint_spec.
   - by apply check_disjoint_spec.
 Qed.
 
+Lemma check_has_ty_mv_spec t σ :
+  check_has_ty t (mv σ) = true →
+  ⊢ t : mv σ.
+Proof.
+  move => ?. apply check_has_ty_spec; [|done].
+  apply: check_has_ty_mv_conditions; eassumption.
+Qed.
+
 Lemma has_ty_implies_check_has_ty_conditions t τ :
   ⊢ t : τ →
-  Forall id (check_has_ty_conditions t τ).
+  Forall id (check_has_ty_conditions t (if τ is val σ f then Some (sig_ranges σ !!! f) else None)).
 Proof.
   revert τ. induction t => τ; destruct τ; try case_match.
   all: simpl => //; inversion 1; simplify_option_eq.
   all: rewrite ?Forall_app; eauto.
-Qed.
+Admitted.

theories/typing/bitfield.v

@@ -267,7 +267,7 @@ Section programs.
     iIntros "HT [% [[% %] Hv1]] Hv2".
     rewrite (bf_is_mask_proof (n:=n) (it:=it)).
     have Hty : has_ty (bf_and t1 t2) (bv σ).
-    { econstructor; eauto. apply check_has_ty_spec; [ by rewrite check_has_ty_conditions_mv_nil| apply bf_ensure_mv_proof]. }
+    { econstructor; eauto. apply check_has_ty_mv_spec. apply bf_ensure_mv_proof. }
     have Hn : bf_to_Z t' it = Z.land (bf_to_Z t1 it) (bf_to_Z t2 it).
     { rewrite Heqt. erewrite normalize_preserves_bf_to_Z; eauto. }
     iApply type_val_expr_mono_strong.
@@ -290,7 +290,7 @@ Section programs.
     iIntros "HT [% [[% %] Hv1]] Hv2".
     rewrite (bf_is_neg_mask_proof (n:=n) (it:=it)).
     have Hty : has_ty (bf_and_neg t1 t2) (bv σ).
-    { econstructor; eauto. apply check_has_ty_spec; [ by rewrite check_has_ty_conditions_mv_nil| apply bf_ensure_mv_proof]. }
+    { econstructor; eauto. apply check_has_ty_mv_spec. apply bf_ensure_mv_proof. }
     have Hn : bf_to_Z t' it = Z.land (bf_to_Z t1 it) (Z_lunot (bits_per_int it) (bf_to_Z t2 it)).
     { rewrite Heqt. erewrite normalize_preserves_bf_to_Z; eauto. }
     iApply type_val_expr_mono_strong.
@@ -396,7 +396,7 @@ Section programs.
 
   Lemma type_or_bitfield_tpd_raw T it σ v1 v2 t1 t2 :
     (tactic_hint (vm_compute_hint (ensure_or_cond_raw σ) (t1, t2)) (λ b,
-      ⌜if b then Forall id (check_has_ty_conditions t2 (bv σ)) else True⌝ ∗
+      ⌜if b then Forall id (check_has_ty_conditions t2 None) else True⌝ ∗
       let norm := normalize (bf_or t1 t2) in
       T (i2v (bf_to_Z norm it) it) (t2mt (norm @ bitfield_tpd it σ)))) -∗
     typed_bin_op v1 (v1 ◁ᵥ t1 @ bitfield_tpd it σ) v2 (v2 ◁ᵥ t2 @ bitfield_raw it) OrOp (IntOp it) (IntOp it) T.
@@ -438,7 +438,7 @@ Section programs.
 
   Lemma type_or_bitfield_tpd_int T it σ n t1 t2 `{!BfFromZ n it t2} v1 v2 :
     (tactic_hint (vm_compute_hint (ensure_or_cond_raw σ) (t1, t2)) (λ b,
-      ⌜if b then Forall id (check_has_ty_conditions t2 (bv σ)) else True⌝ ∗
+      ⌜if b then Forall id (check_has_ty_conditions t2 None) else True⌝ ∗
      let norm := normalize (bf_or t1 t2) in
       T (i2v (bf_to_Z norm it) it) (t2mt (norm @ bitfield_tpd it σ)))) -∗
     typed_bin_op v1 (v1 ◁ᵥ t1 @ bitfield_tpd it σ) v2 (v2 ◁ᵥ n @ int it) OrOp (IntOp it) (IntOp it) T.
@@ -532,7 +532,7 @@ Section programs.
   (* raw -> tpd *)
   Lemma subsume_val_bitfield_raw_tpd T it σ v t t' :
     (tactic_hint (vm_compute_hint (ensure_bv σ) t) (λ _,
-      ⌜Forall id (check_has_ty_conditions t (bv σ))⌝ ∗ ⌜normalize t = t'⌝ ∗ ⌜it_signed it = false ∧ sig_bits σ ≤ bits_per_int it⌝ ∗ T)) -∗
+      ⌜Forall id (check_has_ty_conditions t None)⌝ ∗ ⌜normalize t = t'⌝ ∗ ⌜it_signed it = false ∧ sig_bits σ ≤ bits_per_int it⌝ ∗ T)) -∗
     subsume (v ◁ᵥ t @ bitfield_raw it) (v ◁ᵥ t' @ bitfield_tpd it σ) T.
   Proof.
     unfold tactic_hint, vm_compute_hint.
@@ -548,7 +548,7 @@ Section programs.
 
   Lemma subsume_place_bitfield_raw_tpd T it σ l β t t' :
     (tactic_hint (vm_compute_hint (ensure_bv σ) t') (λ _,
-      ⌜Forall id (check_has_ty_conditions t' (bv σ))⌝ ∗
+      ⌜Forall id (check_has_ty_conditions t' None)⌝ ∗
       ⌜it_signed it = false ∧ sig_bits σ ≤ bits_per_int it⌝ ∗ ⌜bf_to_Z t it = bf_to_Z t' it⌝ ∗ T)) -∗
     subsume (l ◁ₗ{β} t @ bitfield_raw it) (l ◁ₗ{β} t' @ bitfield_tpd it σ) T.
   Proof.
@@ -563,7 +563,7 @@ Section programs.
 
   Lemma subsume_place_int_bitfield_tpd T it σ l β n t t' `{!BfFromZ n it t}:
     (tactic_hint (vm_compute_hint (ensure_bv σ) t') (λ _,
-      ⌜Forall id (check_has_ty_conditions t' (bv σ))⌝ ∗
+      ⌜Forall id (check_has_ty_conditions t' None)⌝ ∗
       ⌜it_signed it = false ∧ sig_bits σ ≤ bits_per_int it⌝ ∗
       (* TODO: Shouldn't this be ensure_eq? *)
       ⌜bf_to_Z t it = bf_to_Z t' it⌝ ∗ T)) -∗
@@ -581,7 +581,7 @@ Section programs.
 
   Lemma subsume_val_int_bitfield_tpd T it σ v n t t' `{!BfFromZ n it t}:
     (tactic_hint (vm_compute_hint (ensure_bv σ) t') (λ _,
-      ⌜Forall id (check_has_ty_conditions t' (bv σ))⌝ ∗
+      ⌜Forall id (check_has_ty_conditions t' None)⌝ ∗
       ⌜it_signed it = false ∧ sig_bits σ ≤ bits_per_int it⌝ ∗
       ⌜bf_to_Z t it = bf_to_Z t' it⌝ ∗ T)) -∗
     subsume (v ◁ᵥ n @ int it) (v ◁ᵥ t' @ bitfield_tpd it σ) T.
@@ -622,11 +622,11 @@ Section programs.
   (* val eq *)
   (* TODO: somehow the check_has_ty_conditions feels unnecessary *)
   Global Instance simple_subsume_val_bitfield_tpd it σ t1 t2 :
-    SimpleSubsumeVal (t1 @ bitfield_tpd it σ) (t2 @ bitfield_tpd it σ) (⌜ensure_eq t1 t2 it⌝ ∗ ⌜is_Some (ensure_bv σ t2)⌝ ∗ ⌜Forall id (check_has_ty_conditions t1 (bv σ)) → Forall id (check_has_ty_conditions t2 (bv σ))⌝) | 50.
+    SimpleSubsumeVal (t1 @ bitfield_tpd it σ) (t2 @ bitfield_tpd it σ) (⌜ensure_eq t1 t2 it⌝ ∗ ⌜is_Some (ensure_bv σ t2)⌝ ∗ ⌜Forall id (check_has_ty_conditions t1 None) → Forall id (check_has_ty_conditions t2 None)⌝) | 50.
   Proof.
     iIntros (v) "[%Heq [%Hty %Himpl]] [% [[% %] Hv]]".
     apply ensure_bv_spec in Hty.
-    2: { apply Himpl. by apply has_ty_implies_check_has_ty_conditions. }
+    2: { apply Himpl. by apply: (has_ty_implies_check_has_ty_conditions _ (bv _)). }
     iSplitR; last iSplitR => //. { by iPureIntro. }
     eapply ensure_eq_spec in Heq; eauto.
     by rewrite /ty_own_val /= Heq.
@@ -634,11 +634,11 @@ Section programs.
 
   (* TODO: somehow the check_has_ty_conditions feels unnecessary *)
   Global Instance simple_subsume_place_bitfield_tpd it σ t1 t2 :
-    SimpleSubsumePlace (t1 @ bitfield_tpd it σ) (t2 @ bitfield_tpd it σ) (⌜ensure_eq t1 t2 it⌝ ∗ ⌜is_Some (ensure_bv σ t2)⌝ ∗ ⌜Forall id (check_has_ty_conditions t1 (bv σ)) → Forall id (check_has_ty_conditions t2 (bv σ))⌝) | 50.
+    SimpleSubsumePlace (t1 @ bitfield_tpd it σ) (t2 @ bitfield_tpd it σ) (⌜ensure_eq t1 t2 it⌝ ∗ ⌜is_Some (ensure_bv σ t2)⌝ ∗ ⌜Forall id (check_has_ty_conditions t1 None) → Forall id (check_has_ty_conditions t2 None)⌝) | 50.
   Proof.
     iIntros (l β) "[%Heq [%Hty %Himpl]] Hl". rewrite /ty_own /=. iDestruct "Hl" as "[% [[% %] Hl]]".
     apply ensure_bv_spec in Hty => //.
-    2: { apply Himpl. by apply has_ty_implies_check_has_ty_conditions. }
+    2: { apply Himpl. by apply: (has_ty_implies_check_has_ty_conditions _ (bv _)). }
     iSplitR; last iSplitR => //. { by iPureIntro. }
     eapply ensure_eq_spec in Heq; eauto.
     by rewrite /ty_own /= Heq.