Commit e02efb12 authored by Paul's avatar Paul
Browse files

prove type_shr_bitfield_tpd_int

parent 36e97ba3
......@@ -38,6 +38,16 @@ Proof.
eapply bv_bounded; eauto.
Qed.
Lemma bf_to_Z_nonneg t σ it :
it_signed it = false
has_ty t (bv σ)
sig_bits σ bits_per_int it
0 bf_to_Z t it.
Proof.
intros Hs ? ?. have : bf_to_Z t it it by eapply bf_to_Z_in_range.
rewrite /bf_to_Z /elem_of /int_elem_of_it /min_int Hs. lia.
Qed.
#[export] Hint Rewrite bf_to_Z_bf_val : lithium_rewrite.
Class BitfieldDesc (R : Type) : Type := {
......
......@@ -268,6 +268,13 @@ Proof.
symmetry. apply (Z_bounded_iff_bits_nonneg k x); lia.
Qed.
Lemma bf_cons_shr a k x :
0 a 0 k
(bf_cons a k x bf_nil) a = x.
Proof.
rewrite /bf_cons /bf_nil => ? ?. bitblast.
Qed.
Lemma bf_slice_cons_ne a k x a' k' l :
0 a 0 k 0 a' 0 k'
0 x < 2^k
......
......@@ -309,16 +309,22 @@ Section programs.
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 "[%Hty [[% %] Hv1]] Hv2".
iApply type_val_expr_mono_strong.
iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
iIntros "_ _". iSplitR. { iPureIntro => /=. admit. }
have Hx : x = bf_to_Z (bf_cons r (bf_val x) bf_nil) it r.1. {
admit.
}
iIntros "_ _". iSplitR.
{ iPureIntro => /=. split.
* split; first lia. inversion Hty; subst; clear Hty.
have <- : sig_ranges σ !!! f = r by apply recognize_spec.
have ? := (sig_ranges_bounded σ f).
eapply Z.lt_le_trans; eauto.
eapply (Z.lt_le_add_lt 0 (Z.of_nat (width (sig_ranges σ !!! f)))); [lia | by rewrite Z.add_0_r].
* eapply bf_to_Z_nonneg; eauto. }
have Hx : x = bf_to_Z (bf_cons r (bf_val x) bf_nil) it r.1.
{ rewrite /bf_to_Z /=. rewrite bitwise.rc.bf_cons_shr //. lia. }
iExists (t2mt _). iIntros "?".
rewrite {1}Hx. iFrame "HT" => /=. by rewrite {4 5}Hx.
Admitted.
Qed.
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) :=
λ T, i2p (type_shr_bitfield_tpd_int T it σ n t1 v1 v2).
......
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