Commit 1c077e3d authored by Paul's avatar Paul
Browse files

update bitfield_tpd to encode the actual int_type

parent c13a42a2
......@@ -114,9 +114,6 @@ struct [[rc::refined_by("mm_ops : mm_callbacks")]] kvm_pgtable_mm_ops {
//@Definition pte_from_addr (pa : Pte) : Pte :=
//@ zero_Pte <| pte_addr := pte_addr pa |>.
//@
//@Definition pte_pa (pa : Pte) : tm :=
//@ bf_cons (range_of 12 36) (bf_val $ pte_addr pa) bf_nil.
//@
//@Record mm_callbacks := {
//@ virt_to_phys : Z → Pte;
//@}.
......@@ -168,9 +165,7 @@ static void kvm_set_invalid_pte(kvm_pte_t *ptep)
WRITE_ONCE(*ptep, pte & ~KVM_PTE_VALID);
}
[[rc::parameters("pa : Pte")]]
[[rc::args("pa @ bitfield<Pte>")]]
[[rc::returns("{pte_pa pa} @ bitfield_tpd<Pte>")]]
[[rc::inlined]]
static kvm_pte_t kvm_phys_to_pte(u64 pa)
{
kvm_pte_t pte = pa & KVM_PTE_ADDR_MASK;
......
......@@ -23,35 +23,34 @@ Class BitfieldDesc (R : Type) : Type := {
bitfield_it_matches_sig : bits_per_int bitfield_it = sig_bits bitfield_sig;
}.
Lemma normalize_preserves_bf_to_Z R `{BitfieldDesc R} t :
has_ty t (bv bitfield_sig)
bf_to_Z (normalize t) bitfield_it = bf_to_Z t bitfield_it.
Lemma normalize_preserves_bf_to_Z σ t it :
has_ty t (bv σ)
sig_bits σ bits_per_int it
bf_to_Z (normalize t) it = bf_to_Z t it.
Proof.
move => ?. unfold bf_to_Z.
have -> : bits_per_int bitfield_it = (sig_bits_of (bv bitfield_sig))
by apply bitfield_it_matches_sig.
by rewrite normalize_preserves_eval.
move => ? ?. unfold bf_to_Z.
eapply normalize_preserves_eval; eauto.
Qed.
Definition ensure_mv (R : Type) `{BitfieldDesc R} (t : tm) : option () :=
if check_has_ty t (mv bitfield_sig) then Some () else None.
Definition ensure_mv (σ : signature) (t : tm) : option () :=
if check_has_ty t (mv σ) then Some () else None.
Lemma ensure_mv_spec R `{BitfieldDesc R} t :
is_Some (ensure_mv R t)
has_ty t (mv bitfield_sig).
Lemma ensure_mv_spec (σ : signature) t :
is_Some (ensure_mv σ t)
has_ty t (mv σ).
Proof.
unfold ensure_mv. move => ?.
apply check_has_ty_spec. { by rewrite check_has_ty_conditions_mv_nil. }
have ? := is_Some_None. case_match; naive_solver.
Qed.
Definition ensure_bv (R : Type) `{BitfieldDesc R} (t : tm) : option () :=
if check_has_ty t (bv bitfield_sig) then Some () else None.
Definition ensure_bv (σ : signature) (t : tm) : option () :=
if check_has_ty t (bv σ) then Some () else None.
Lemma ensure_bv_spec R `{BitfieldDesc R} t :
Forall id (check_has_ty_conditions t (bv bitfield_sig))
is_Some (ensure_bv R t)
has_ty t (bv bitfield_sig).
Lemma ensure_bv_spec σ t :
Forall id (check_has_ty_conditions t (bv σ))
is_Some (ensure_bv σ t)
has_ty t (bv σ).
Proof.
unfold ensure_bv. move => ??.
apply check_has_ty_spec => //.
......@@ -76,20 +75,20 @@ Proof.
move => ?. split; by apply check_has_ty_spec.
Qed.
Definition ensure_or_cond (R : Type) `{BitfieldDesc R} (tp : tm * tm) : option () :=
Definition ensure_or_cond (σ : signature) (tp : tm * tm) : option () :=
match tp with (t1, t2) =>
if check_has_ty t2 (mv bitfield_sig) then Some ()
if check_has_ty t2 (mv σ) then Some ()
else if check_disjoint (ranges t1) (ranges t2) then Some ()
else None
end.
Arguments ensure_or_cond _/.
Lemma ensure_or_cond_spec R `{BitfieldDesc R} t1 t2 :
has_ty t1 (bv bitfield_sig)
has_ty t2 (bv bitfield_sig)
is_Some (ensure_or_cond R (t1, t2))
has_ty (bf_or t1 t2) (bv bitfield_sig).
Lemma ensure_or_cond_spec σ t1 t2 :
has_ty t1 (bv σ)
has_ty t2 (bv σ)
is_Some (ensure_or_cond σ (t1, t2))
has_ty (bf_or t1 t2) (bv σ).
Proof.
move => ? ? Hs. econstructor; eauto.
unfold ensure_or_cond in Hs.
......@@ -98,25 +97,25 @@ Proof.
- left. by apply check_disjoint_spec.
Qed.
Definition ensure_or_cond_raw (R : Type) `{BitfieldDesc R} (tp : tm * tm) : option bool :=
Definition ensure_or_cond_raw σ (tp : tm * tm) : option bool :=
match tp with (t1, t2) =>
if check_has_ty t2 (mv bitfield_sig) then Some false
else if check_has_ty t2 (bv bitfield_sig) && check_disjoint (ranges t1) (ranges t2) then Some true
if check_has_ty t2 (mv σ) then Some false
else if check_has_ty t2 (bv σ) && check_disjoint (ranges t1) (ranges t2) then Some true
else None
end.
Lemma ensure_or_cond_raw_spec R `{BitfieldDesc R} t1 t2 b :
has_ty t1 (bv bitfield_sig)
ensure_or_cond_raw R (t1, t2) = Some b
(if b then Forall id (check_has_ty_conditions t2 (bv bitfield_sig)) else True)
has_ty (bf_or t1 t2) (bv bitfield_sig).
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)
has_ty (bf_or t1 t2) (bv σ).
Proof.
move => ? Hs ?. unfold ensure_or_cond_raw in Hs.
destruct (check_has_ty t2 (mv bitfield_sig)) eqn:?; simplify_eq.
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.
- destruct (check_has_ty t2 (bv bitfield_sig)) eqn:?; simplify_eq.
- destruct (check_has_ty t2 (bv σ)) eqn:?; simplify_eq.
destruct (check_disjoint (ranges t1) (ranges t2)) eqn:? => //; simplify_eq/=.
econstructor; eauto.
* by apply check_has_ty_spec.
......@@ -128,15 +127,14 @@ Definition ensure_eq (t1 t2 : tm) (it : int_type) : Prop :=
Arguments ensure_eq _/.
Lemma ensure_eq_spec R `{BitfieldDesc R} t1 t2 :
has_ty t1 (bv bitfield_sig)
has_ty t2 (bv bitfield_sig)
ensure_eq t1 t2 bitfield_it bf_to_Z t1 bitfield_it = bf_to_Z t2 bitfield_it.
Lemma ensure_eq_spec it σ t1 t2 :
has_ty t1 (bv σ)
has_ty t2 (bv σ)
sig_bits σ bits_per_int it
ensure_eq t1 t2 it bf_to_Z t1 it = bf_to_Z t2 it.
Proof.
move => ? ?. unfold ensure_eq.
have Hit : bits_per_int bitfield_it = (sig_bits_of (bv bitfield_sig))
by apply bitfield_it_matches_sig.
rewrite Hit check_eq_sound_complete // -Hit //.
move => ? ? ?. unfold ensure_eq.
erewrite check_eq_sound_complete; eauto.
Qed.
(* boolean version *)
......@@ -187,17 +185,16 @@ Proof.
- rewrite bool_decide_eq_false. naive_solver.
Qed.
Lemma bf_zb_spec R `{BitfieldDesc R} t :
has_ty t (bv bitfield_sig)
bf_zb t bitfield_it = bool_decide (0 = bf_to_Z t bitfield_it).
Lemma bf_zb_spec it σ t :
has_ty t (bv σ)
sig_bits σ bits_per_int it
bf_zb t it = bool_decide (0 = bf_to_Z t it).
Proof.
move => ? => /=.
symmetry. rewrite /bf_to_Z bool_decide_eqb bf_value_zb_spec.
rewrite bitfield_it_matches_sig cmp_zero_spec.
2: by apply normalize_preserves_type.
2: by eapply normalize_spec.
have -> : sig_bits bitfield_sig = sig_bits_of (bv bitfield_sig) by done.
rewrite normalize_preserves_eval //.
move => ? ? => /=.
symmetry. rewrite /bf_to_Z bool_decide_eqb bf_value_zb_spec cmp_zero_spec; eauto.
* by erewrite normalize_preserves_eval; eauto.
* by apply normalize_preserves_type.
* by eapply normalize_spec.
Qed.
Definition bf_eqb (t1 t2 : tm) (it : int_type) : bool :=
......@@ -205,19 +202,18 @@ Definition bf_eqb (t1 t2 : tm) (it : int_type) : bool :=
Arguments bf_eqb _/.
Lemma bf_eqb_spec R `{BitfieldDesc R} t1 t2 :
has_ty t1 (bv bitfield_sig)
has_ty t2 (bv bitfield_sig)
bf_eqb t1 t2 bitfield_it = bool_decide (bf_to_Z t1 bitfield_it = bf_to_Z t2 bitfield_it).
Lemma bf_eqb_spec it σ t1 t2 :
has_ty t1 (bv σ)
has_ty t2 (bv σ)
sig_bits σ bits_per_int it
bf_eqb t1 t2 it = bool_decide (bf_to_Z t1 it = bf_to_Z t2 it).
Proof.
move => ? ? => /=.
symmetry. rewrite /bf_to_Z bool_decide_eqb bf_value_eqb_spec.
rewrite bitfield_it_matches_sig.
have -> : sig_bits bitfield_sig = sig_bits_of (bv bitfield_sig) by done.
rewrite cmp_spec.
move => ? ? ? => /=.
symmetry. rewrite /bf_to_Z bool_decide_eqb bf_value_eqb_spec cmp_spec.
all: try by apply normalize_preserves_type.
all: try by eapply normalize_spec.
rewrite !normalize_preserves_eval //.
2: done.
repeat (erewrite normalize_preserves_eval; eauto).
Qed.
(** * Typeclasses to convert integers to bitfields *)
......@@ -342,3 +338,4 @@ Global Instance max_int_u64_le_lt x :
Proof.
unfold SimplBoth. by apply max_int_unsigned_le_lt.
Qed.
......@@ -159,11 +159,12 @@ Qed.
From refinedc.mask_core Require Import semantics.
Corollary normalize_preserves_eval t τ :
Corollary normalize_preserves_eval t τ (N : Z) :
t : τ
eval (sig_bits_of τ) (normalize t) = eval (sig_bits_of τ) t.
(sig_bits_of τ N)%Z
eval N (normalize t) = eval N t.
Proof.
move => ?.
move => ? ?.
have ? : t ↠ᵣ normalize t by eapply normalize_spec; eauto.
eapply multi_step_preserves_eval; eauto.
Qed.
......@@ -17,12 +17,13 @@ Fixpoint cmp_zero (N : Z) (v : tm) : Prop :=
| _ => False (* error *)
end.
Lemma cmp_zero_spec v σ :
Lemma cmp_zero_spec v σ N :
v : bv σ
value v
cmp_zero (sig_bits σ) v eval (sig_bits σ) v = 0.
sig_bits σ N
cmp_zero N v eval N v = 0.
Proof.
induction v as [?|?| |r x _ v IHv|??|???|??|??|??]; inversion 1; inversion 1; subst => //=.
induction v as [?|?| |r x _ v IHv|??|???|??|??|??]; inversion 1; inversion 1; subst => ? //=.
rewrite IHv //.
rewrite rc.bf_cons_zero_iff //. lia.
Qed.
......@@ -54,16 +55,17 @@ Lemma cmp_cons N r1 x1 v1 r2 x2 v2 :
else eval N x2 = 0 cmp N (bf_cons r1 x1 v1) v2.
Proof. done. Qed.
Lemma cmp_bv_spec v1 v2 σ :
Lemma cmp_bv_spec v1 v2 σ N :
v1 : bv σ
v2 : bv σ
value v1
value v2
cmp (sig_bits σ) v1 v2 eval (sig_bits σ) v1 = eval (sig_bits σ) v2.
sig_bits σ N
cmp N v1 v2 eval N v1 = eval N v2.
Proof.
move : v2.
induction v1 as [?|?| |r1 x1 _ v1 IHv1|??|???|??|??|??] => v2.
all: induction v2 as [?|?| |r2 x2 _ v2 IHv2|??|???|??|??|??]; do 4 (inversion 1); subst => //.
all: induction v2 as [?|?| |r2 x2 _ v2 IHv2|??|???|??|??|??]; do 4 (inversion 1); subst => ? //.
3: rewrite cmp_cons; repeat case_match.
- rewrite cmp_nil_l cmp_zero_spec /rc.bf_nil; eauto => //.
- rewrite cmp_nil_r cmp_zero_spec /rc.bf_nil; eauto.
......@@ -79,7 +81,7 @@ Proof.
+ move => Heq. apply rc.bf_cons_lt_inj in Heq => //; try lia.
* eapply val_bounded; eauto.
* eapply bv_range_empty; eauto.
* have -> : rc.bf_cons (offset r2) (width r2) (eval (sig_bits σ) x2) (eval (sig_bits σ) v2) = (eval (sig_bits σ) (bf_cons r2 x2 v2)) by done.
* have -> : rc.bf_cons (offset r2) (width r2) (eval N x2) (eval N v2) = (eval N (bf_cons r2 x2 v2)) by done.
eapply bv_range_empty; eauto.
- have ? : r2 r1.
{ have Hr : r1 = r2 r1 r2 r2 r1 by eapply sig_range_comparable; eauto.
......@@ -90,28 +92,30 @@ Proof.
+ move => Heq. symmetry in Heq. apply rc.bf_cons_lt_inj in Heq => //; try lia.
* eapply val_bounded; eauto.
* eapply bv_range_empty; eauto.
* have -> : rc.bf_cons (offset r1) (width r1) (eval (sig_bits σ) x1) (eval (sig_bits σ) v1) = (eval (sig_bits σ) (bf_cons r1 x1 v1)) by done.
* have -> : rc.bf_cons (offset r1) (width r1) (eval N x1) (eval N v1) = (eval N (bf_cons r1 x1 v1)) by done.
eapply bv_range_empty; eauto.
Qed.
Lemma cmp_val_spec v1 v2 σ f :
Lemma cmp_val_spec v1 v2 σ f N :
v1 : val σ f
v2 : val σ f
value v1
value v2
cmp (sig_bits σ) v1 v2 eval (sig_bits σ) v1 = eval (sig_bits σ) v2.
sig_bits σ N
cmp N v1 v2 eval N v1 = eval N v2.
Proof.
move : v2.
induction v1 as [?|?| |r1 x1 _ v1 IHv1|??|???|??|??|??] => v2.
all: induction v2 as [?|?| |r2 x2 _ v2 IHv2|??|???|??|??|??]; do 4 (inversion 1); subst => //.
all: induction v2 as [?|?| |r2 x2 _ v2 IHv2|??|???|??|??|??]; do 4 (inversion 1); subst => ? //.
Qed.
Lemma cmp_spec v1 v2 τ :
Lemma cmp_spec v1 v2 τ N :
v1 : τ
v2 : τ
value v1
value v2
cmp (sig_bits_of τ) v1 v2 eval (sig_bits_of τ) v1 = eval (sig_bits_of τ) v2.
sig_bits_of τ N
cmp N v1 v2 eval N v1 = eval N v2.
Proof.
move => Hty1 Hty2 ? ?. destruct τ.
- eapply cmp_val_spec; eauto.
......@@ -127,12 +131,13 @@ Arguments check_eq _/.
(* main theorem *)
Theorem check_eq_sound_complete t1 t2 τ :
Theorem check_eq_sound_complete t1 t2 τ N :
t1 : τ
t2 : τ
check_eq (sig_bits_of τ) t1 t2 sem_eq (sig_bits_of τ) t1 t2.
sig_bits_of τ N
check_eq N t1 t2 sem_eq N t1 t2.
Proof.
unfold check_eq, sem_eq => Hty1 Hty2.
unfold check_eq, sem_eq => Hty1 Hty2 ?.
have Hty1' := Hty1.
have Hty2' := Hty2.
apply normalize_spec in Hty1' as [Ht1 Hv1].
......
......@@ -40,17 +40,18 @@ Proof.
apply sig_ranges_bounded.
Qed.
Lemma bv_bounded t σ :
Lemma bv_bounded t σ N :
t : bv σ
0 eval (sig_bits σ) t < 2 ^ (sig_bits σ).
sig_bits σ N
0 eval N t < 2 ^ N.
Proof.
induction t; inversion 1; subst => /=.
induction t; inversion 1; subst => ? /=.
- unfold rc.bf_nil. split; [done| apply Z.pow_pos_nonneg; lia].
- apply rc.bf_cons_bounded; eauto; try lia.
* eapply range_bounded; eauto.
* etrans; first eapply range_bounded; eauto.
* eapply val_bounded; eauto.
- apply rc.bf_update_bounded; eauto; try lia.
* eapply range_bounded; eauto.
* etrans; first eapply range_bounded; eauto.
* eapply val_bounded; eauto.
- have ? : t2 : bv σ by apply subsume_mv_bv.
apply rc.Z_land_bounded_nonneg; eauto; lia.
......@@ -90,13 +91,14 @@ Definition sig_bits_of (τ : ty) : nat :=
| bv σ => sig_bits σ
end.
Lemma step_preserves_eval t t' τ :
Lemma step_preserves_eval t t' τ N :
t : τ
t t'
eval (sig_bits_of τ) t' = eval (sig_bits_of τ) t.
sig_bits_of τ N
eval N t' = eval N t.
Proof.
move => Hty Hst.
move : τ Hty. induction Hst => τ Hty /=.
move : τ Hty. induction Hst => τ Hty ? /=.
all: invert Hty.
all: try by (f_equal; naive_solver).
- inversion Hst.
......@@ -114,11 +116,11 @@ Proof.
* eapply bv_range_empty; eauto.
- auto_inv. rewrite rc.bf_update_cons_skip; try lia.
* eapply val_bounded; eauto.
* eapply range_bounded; eauto.
* etrans; first eapply range_bounded; eauto.
* naive_solver.
- auto_inv. rewrite rc.bf_update_cons_insert; try lia.
* naive_solver.
* eapply range_bounded; eauto.
* etrans; first eapply range_bounded; eauto.
* eapply val_bounded; eauto.
* eapply bv_bounded; eauto.
* eapply bv_range_empty; eauto.
......@@ -140,15 +142,15 @@ Proof.
- rewrite rc.bf_lor_update_r; try lia. naive_solver.
Qed.
Lemma multi_step_preserves_eval t t' τ :
Lemma multi_step_preserves_eval t t' τ N :
t : τ
t ↠ᵣ t'
eval (sig_bits_of τ) t' = eval (sig_bits_of τ) t.
sig_bits_of τ N
eval N t' = eval N t.
Proof.
move => Hty. induction 1 as [|t t' t''] => //.
move => Hty. induction 1 as [|t t' t''] => ? //.
have ? : t' : τ
by eapply multi_step_preserves_type; eauto; apply rtc_once.
have <- : eval (sig_bits_of τ) t' = eval (sig_bits_of τ) t
by eapply step_preserves_eval; eauto.
have <- : eval N t' = eval N t by eapply step_preserves_eval; eauto.
naive_solver.
Qed.
This diff is collapsed.
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