Commit 866a8ce3 authored by Michael Sammler's avatar Michael Sammler Committed by Paul
Browse files

add shr rule

parent d2dcdaf6
......@@ -320,6 +320,30 @@ Section programs.
TypedBinOpVal v1 (t1 @ bitfield_tpd R)%I v2 (n @ int it)%I AndOp (IntOp it) (IntOp it) :=
λ T, i2p (type_and_neg_bitfield_tpd_int_mask T R n it t1 t2 v1 v2).
Lemma type_shr_bitfield_tpd_int T R `{BitfieldDesc R} n it t1 v1 v2 :
( r x, t1 = bf_cons r (bf_val x) bf_nil
T (i2v x it) (t2mt (x @ int it))) -
typed_bin_op v1 (v1 ◁ᵥ t1 @ bitfield_tpd R) v2 (v2 ◁ᵥ n @ int it) ShrOp (IntOp it) (IntOp it) T.
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 = (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. *)
Global Instance type_shr_bitfield_tpd_int_inst R `{BitfieldDesc R} n it t1 v1 v2 :
TypedBinOpVal v1 (t1 @ bitfield_tpd R)%I v2 (n @ int it)%I ShrOp (IntOp it) (IntOp it) :=
λ T, i2p (type_shr_bitfield_tpd_int T R n it t1 v1 v2).
Lemma type_not_bitfield_raw T it v t :
(it_signed it = false let n := Z_lunot (bits_per_int it) (bf_to_Z t it) in T (i2v n it) (t2mt (t @ bitfield_neg it))) -
typed_un_op v (v ◁ᵥ t @ bitfield_raw it)%I (NotIntOp) (IntOp it) 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