only one admitted left

theories/typing/bitfield.v

@@ -304,18 +304,20 @@ Section programs.
     TypedBinOpVal v1 (t1 @ bitfield_tpd it σ)%I v2 (n @ int it)%I AndOp (IntOp it) (IntOp it) :=
     λ T, i2p (type_and_neg_bitfield_tpd_int_mask T it σ n t1 t2 v1 v2).
 
-  Lemma type_shr_bitfield_tpd_int T it σ n t1 v1 v2 :
-      (∃ r x, ⌜t1 = bf_cons r (bf_val x) bf_nil⌝ ∗ ⌜0 ≤ n < bits_per_int it⌝ ∗
+  Lemma type_shr_bitfield_tpd_int T it σ (n : Z) t1 v1 v2 :
+      (∃ r x, ⌜t1 = bf_cons r (bf_val x) bf_nil⌝ ∗ ⌜n = r.1⌝ ∗
       T (i2v x it) (t2mt (x @ int it))) -∗
     typed_bin_op v1 (v1 ◁ᵥ t1 @ bitfield_tpd it σ) v2 (v2 ◁ᵥ n @ int it) ShrOp (IntOp it) (IntOp it) T.
   Proof.
-    iDestruct 1 as (r x -> ?) "HT". iIntros "[% [[% %] Hv1]] Hv2".
+    iDestruct 1 as (r x -> ->) "HT". iIntros "[% [[% %] Hv1]] Hv2".
     iApply type_val_expr_mono_strong.
     iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
-    iIntros "_ _". iSplitR. { iPureIntro => /=. split; [done|]. admit. }
-    have Hx : x = bf_to_Z (bf_cons r (bf_val x) bf_nil) bitfield_it ≫ n. { admit. }
+    iIntros "_ _". iSplitR. { iPureIntro => /=. admit. }
+    have Hx : x = bf_to_Z (bf_cons r (bf_val x) bf_nil) it ≫ r.1. {
+      admit.
+    }
     iExists (t2mt _). iIntros "?".
-     (* rewrite {1}Hx. iFrame "HT" => /=. by rewrite {4 5}Hx. *)
+     rewrite {1}Hx. iFrame "HT" => /=. by rewrite {4 5}Hx.
   Admitted.
   Global Instance type_shr_bitfield_tpd_int_inst it σ n t1 v1 v2 :
     TypedBinOpVal v1 (t1 @ bitfield_tpd it σ)%I v2 (n @ int it)%I ShrOp (IntOp it) (IntOp it) :=
@@ -435,16 +437,18 @@ Section programs.
       λ T, i2p (type_or_bitfield_raw T it v1 v2 t1 t2).
 
   Lemma type_or_bitfield_tpd_int T it σ n t1 t2 `{!BfFromZ n it t2} v1 v2 :
-    (let norm := normalize (bf_or t1 t2) in
-      T (i2v (bf_to_Z norm it) it) (t2mt (norm @ bitfield_tpd it σ))) -∗
+    (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⌝ ∗
+     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.
-  Proof. Admitted.
-    (* remember (normalize (bf_or t1 t2)) as t' eqn:Heqt.
-    iIntros "HT [% [[% %] Hv1]] Hv2".
-    (* rewrite (bf_is_mask_proof (n:=n) (it:=it)). *)
-    have Hty : has_ty (bf_or t1 t2) (bv σ).
-    { econstructor; eauto. apply check_has_ty_spec; [ by rewrite check_has_ty_conditions_mv_nil| apply bf_ensure_mv_proof]. }
-    have Hn : bf_to_Z t' it = Z.land (bf_to_Z t1 it) (bf_to_Z t2 it).
+  Proof.
+    unfold tactic_hint, vm_compute_hint.
+    remember (normalize (bf_or t1 t2)) as t' eqn:Heqt.
+    iIntros "[% [%Hor [% HT]]] [% [[% %] Hv1]] Hv2".
+    rewrite (bf_from_Z_proof (n:=n) (it:=it)).
+    have Hty : has_ty (bf_or t1 t2) (bv σ) by apply: ensure_or_cond_raw_spec.
+    have Hn : bf_to_Z t' it = Z.lor (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.
     iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
@@ -452,22 +456,7 @@ Section programs.
     iIntros "?". rewrite Hn. iFrame "HT". iSplitR; last iSplitR => //.
     { iPureIntro. rewrite Heqt; by apply normalize_preserves_type. }
     by rewrite /ty_own_val /= Hn.
-      Proof. Admitted. *)
-      (*
-    remember (normalize (bf_and t1 t2)) as n eqn:Heqn.
-    iIntros "[% [% HT]] [% Hv1] Hv2".
-    have Hty : has_ty (bf_and t1 t2) (bv bitfield_sig).
-    { econstructor; eauto. by apply ensure_mv_spec. }
-    have Hn : bf_to_Z n bitfield_it = Z.land (bf_to_Z t1 bitfield_it) (bf_to_Z t2 bitfield_it).
-    { rewrite Heqn. by rewrite normalize_preserves_bf_to_Z. }
-    iApply type_val_expr_mono_strong.
-*)
-    (* iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
-    iIntros "_ _". iSplitR => //. iExists _.
-    rewrite /ty_own_val /= Hn.
-    iIntros "?". iFrame. iSplitR.
-    { iPureIntro. rewrite Heqn; by apply normalize_preserves_type. }
-    by rewrite /ty_own_val /= Hn. *)
+  Qed.
   Global Instance type_or_bitfield_tpd_int_inst it σ n t1 t2 `{!BfFromZ n it t2} v1 v2 :
     TypedBinOpVal v1 (t1 @ bitfield_tpd it σ)%I v2 (n @ int it)%I OrOp (IntOp it) (IntOp it) :=
     λ T, i2p (type_or_bitfield_tpd_int T it σ n t1 t2 v1 v2).
@@ -572,17 +561,40 @@ Section programs.
   Global Instance subsume_place_bitfield_raw_tpd_inst it σ l β t t' : SubsumePlace l β (t @ bitfield_raw it) (t' @ bitfield_tpd it σ) :=
     λ T, i2p (subsume_place_bitfield_raw_tpd T it σ l β t t').
 
-  (* TODO: add val instance *)
   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 σ))⌝ ∗
-      ⌜it = it⌝ ∗ ⌜bf_to_Z t it = bf_to_Z t' it⌝ ∗ T)) -∗
+      ⌜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)) -∗
     subsume (l ◁ₗ{β} n @ int it) (l ◁ₗ{β} t' @ bitfield_tpd it σ) T.
-  Proof. Admitted.
+  Proof.
+    unfold tactic_hint, vm_compute_hint.
+    iIntros "[% [% [% [% [%Heq ?]]]]] Hl".
+    rewrite (bf_from_Z_proof (n:=n) (it:=it)) Heq.
+    iFrame. rewrite {2}/ty_own/={2}/ty_own/=. iFrame. iPureIntro. split; [|done].
+    by apply ensure_bv_spec.
+  Qed.
   Global Instance subsume_place_int_bitfield_tpd_inst it σ l β n t t' `{!BfFromZ n it t} :
     SubsumePlace l β (n @ int it) (t' @ bitfield_tpd it σ) :=
     λ T, i2p (subsume_place_int_bitfield_tpd T it σ l β n t t').
 
+  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 σ))⌝ ∗
+      ⌜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.
+  Proof.
+    unfold tactic_hint, vm_compute_hint.
+    iIntros "[% [% [% [% [%Heq ?]]]]] Hl".
+    rewrite (bf_from_Z_proof (n:=n) (it:=it)) Heq.
+    iFrame. iPureIntro. split; [|done]. by apply ensure_bv_spec.
+  Qed.
+  Global Instance subsume_val_int_bitfield_tpd_inst it σ v n t t' `{!BfFromZ n it t} :
+    SubsumeVal v (n @ int it) (t' @ bitfield_tpd it σ) :=
+    λ T, i2p (subsume_val_int_bitfield_tpd T it σ v n t t').
+
   Lemma bool_decide_eq_swap {A} (x y : A) `{!Decision (x = y)} `{!Decision (y = x)} :
     bool_decide (x = y) = bool_decide (y = x).
   Proof. (* TODO: is there a simpler way? *)