Commit a51c705c authored by Paul's avatar Paul
Browse files

prove type casting rule

parent f4877c57
......@@ -13,6 +13,31 @@ Lemma bf_to_Z_bf_val x it :
bf_to_Z (bf_val x) it = x.
Proof. done. Qed.
Lemma bf_to_Z_it_extend it σ t :
sig_bits σ bits_per_int it
has_ty t (bv σ)
bf_to_Z t it = eval (sig_bits σ) t.
Proof.
intros. rewrite /bf_to_Z.
have -> : sig_bits σ = sig_bits_of (bv σ) by done.
apply eval_extend => //.
Qed.
Lemma bf_to_Z_in_range t σ it :
it_signed it = false
has_ty t (bv σ)
sig_bits σ bits_per_int it
bf_to_Z t it it.
Proof.
intros Hs. rewrite /bf_to_Z /elem_of /int_elem_of_it => ? ?.
have -> : min_int it = 0.
{ rewrite /min_int Hs //. }
have -> : max_int it = 2 ^ (bits_per_int it) - 1.
{ rewrite /max_int Hs //. }
suff : 0 eval (bits_per_int it) t < 2 ^ (bits_per_int it) by lia.
eapply bv_bounded; eauto.
Qed.
#[export] Hint Rewrite bf_to_Z_bf_val : lithium_rewrite.
Class BitfieldDesc (R : Type) : Type := {
......@@ -170,7 +195,14 @@ Fixpoint bf_value_eqb (N : Z) (v1 : tm) : tm → bool :=
Fixpoint bf_value_eqb_spec N v1 v2 :
bf_value_eqb N v1 v2 = true cmp N v1 v2.
Proof.
Admitted.
induction v1; induction v2 => //=.
all: rewrite ?bool_decide_eq_true //.
all: rewrite ?andb_true_iff ?bool_decide_eq_true.
1-2: rewrite ZifyClasses.and_morph // bf_value_zb_spec //.
repeat case_match.
all: rewrite ?andb_true_iff ?bool_decide_eq_true ZifyClasses.and_morph //.
eauto.
Qed.
Definition bf_zb (t : tm) (it : int_type) : bool :=
bf_value_zb (bits_per_int it) (normalize t).
......
......@@ -7,6 +7,20 @@ Local Set SsrOldRewriteGoalsOrder.
Local Open Scope Z_scope.
(* Z.land Z_lunot *)
Lemma Z_land_lunot_bits N M n x :
0 N M
0 n < 2 ^ N
Z.land n (Z_lunot M x) = Z.land n (Z_lunot N x).
Proof.
intros.
bitblast.
have -> : Z.testbit n i = false
by apply (Z_bounded_iff_bits_nonneg N n); lia.
by simplify_bool_eq.
Qed.
Module rc.
(* raw bit vector constructors *)
......
......@@ -154,3 +154,22 @@ Proof.
have <- : eval N t' = eval N t by eapply step_preserves_eval; eauto.
naive_solver.
Qed.
Lemma eval_extend t τ N :
t : τ
sig_bits_of τ N
eval N t = eval (sig_bits_of τ) t.
Proof.
move : τ. induction t; inversion 1; subst => HN //=.
all: try by f_equal; naive_solver.
- erewrite IHt1; eauto. simpl.
erewrite IHt2; eauto. simpl.
simpl in HN.
rewrite /rc.bf_update (Z_land_lunot_bits (sig_bits σ) N) //; [lia|].
eapply bv_bounded; eauto. lia.
- erewrite IHt1; eauto. simpl.
erewrite IHt2; eauto. simpl.
simpl in HN.
rewrite (Z_land_lunot_bits (sig_bits σ) N) //; [lia|].
eapply bv_bounded; eauto. lia.
Qed.
......@@ -359,14 +359,14 @@ Section programs.
TypedBinOpVal v1 (t1 @ bitfield_tpd it σ)%I v2 (t2 @ bitfield_neg it)%I AndOp (IntOp it) (IntOp it) :=
λ T, i2p (type_and_bitfield_tpd_neg T it σ v1 v2 t1 t2).
Lemma type_and_bitfield_raw_neg T it v1 v2 t1 t2 :
(* Lemma type_and_bitfield_raw_neg T it v1 v2 t1 t2 :
(let t' := bf_and_neg t1 t2 in
T (i2v (bf_to_Z t' it) it) (t2mt (t' @ bitfield_raw it))) -∗
typed_bin_op v1 (v1 ◁ᵥ t1 @ bitfield_raw it) v2 (v2 ◁ᵥ t2 @ bitfield_neg it) AndOp (IntOp it) (IntOp it) T.
Proof. Admitted.
Global Instance type_and_bitfield_raw_neg_inst it v1 t1 v2 t2 :
TypedBinOpVal v1 (t1 @ bitfield_raw it)%I v2 (t2 @ bitfield_neg it)%I AndOp (IntOp it) (IntOp it) :=
λ T, i2p (type_and_bitfield_raw_neg T it v1 v2 t1 t2).
λ T, i2p (type_and_bitfield_raw_neg T it v1 v2 t1 t2). *)
Lemma type_or_bitfield_tpd T it σ v1 v2 t1 t2 :
(tactic_hint (vm_compute_hint (ensure_or_cond σ) (t1, t2)) (λ _,
......@@ -438,7 +438,21 @@ Section programs.
(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.
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).
{ rewrite Heqt. erewrite normalize_preserves_bf_to_Z; eauto. }
iApply type_val_expr_mono_strong.
iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
iIntros "_ _". iSplitR => //. iExists (t2mt _).
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".
......@@ -581,15 +595,15 @@ Section programs.
Qed.
Lemma type_if_bitfield_tpd it σ v t T1 T2:
(True (bf_zb t it = false - T1) (bf_zb t it = true - T2)) -
((bf_zb t it = false - T1) (bf_zb t it = true - T2)) -
typed_if (IntOp it) v (v ◁ᵥ t @ bitfield_tpd it σ) T1 T2.
Proof.
iIntros "[% Hb] [% Hv]" => //.
(* rewrite bf_zb_spec // bool_decide_eq_swap. *)
(* iExists _. iFrame.
iIntros "Hb [% [[% %] Hv]]" => //.
erewrite bf_zb_spec => //. rewrite bool_decide_eq_swap.
iExists _. iFrame.
rewrite -negb_bool_decide_eq. case_bool_decide => /=.
all: by iApply "Hb". *)
Admitted.
all: by iApply "Hb".
Qed.
Global Instance type_if_bitfield_tpd_inst it σ v t : TypedIf (IntOp it) v (v ◁ᵥ t @ bitfield_tpd it σ)%I :=
λ T1 T2, i2p (type_if_bitfield_tpd it σ v t T1 T2).
......@@ -618,24 +632,20 @@ Section programs.
by rewrite /ty_own /= Heq.
Qed.
(* TODO: do we need them? *)
(* Global Instance simple_subsume_val_bitfield_raw it t1 t2 :
SimpleSubsumeVal (t1 @ bitfield_raw it) (t2 @ bitfield_raw it) (⌜bf_to_Z t1 it = bf_to_Z t2 it⌝) | 50.
Proof.
iIntros (v) "%Heq Hv".
by rewrite /ty_own_val /= Heq.
Qed.
Global Instance simple_subsume_place_bitfield_raw it t1 t2 :
SimpleSubsumePlace (t1 @ bitfield_raw it) (t2 @ bitfield_raw it) (⌜bf_to_Z t1 it = bf_to_Z t2 it⌝) | 50.
Proof.
Admitted. *)
Lemma type_cast_bitfield_tpd T σ it1 it2 v t :
(True - True v, T v (t2mt (t @ bitfield_tpd it2 σ))) -
(it_signed it2 = false sig_bits σ bits_per_int it2 v, T v (t2mt (t @ bitfield_tpd it2 σ))) -
typed_un_op v (v ◁ᵥ t @ bitfield_tpd it1 σ)%I (CastOp (IntOp it2)) (IntOp it1) T.
Proof.
Admitted.
iIntros "[[% %] HT] [% [[% %] Hv]]".
iApply type_val_expr_mono_strong.
iApply (type_cast_int with "[HT] Hv") => //.
have -> : bf_to_Z t it1 = bf_to_Z t it2.
{ erewrite bf_to_Z_it_extend; eauto. erewrite bf_to_Z_it_extend; eauto. }
iIntros (_). iSplitR.
{ iPureIntro. eapply bf_to_Z_in_range; eauto. }
iIntros (v'). iSpecialize ("HT" $! v'). iExists _. iFrame.
iIntros "?". iSplitR => //. iSplitR => //.
Qed.
Global Instance type_cast_bitfield_tpd_inst σ it1 it2 v t :
TypedUnOpVal v (t @ bitfield_tpd it1 σ)%I (CastOp (IntOp it2)) (IntOp it1) :=
λ T, i2p (type_cast_bitfield_tpd T σ it1 it2 v t).
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment