Commit 8a7d451a authored by Paul's avatar Paul
Browse files

prove most typing rules

parent 54eaf6ac
......@@ -14,3 +14,4 @@ _opam
**/proofs/*/generated*
**/proofs/*/dune
**/proofs/*/proof_files
*.DS_Store
......@@ -10,32 +10,32 @@ typedef uint8_t u8;
#define BITS_PER_LONG (sizeof(long) * 8)
[[rc::parameters("i : nat")]]
[[rc::parameters("i : Z")]]
[[rc::args("i @ int<i32>")]]
[[rc::requires("{0 ≤ i < 64}")]]
[[rc::returns("{bf_cons (i, 1)%nat (bf_mask 1) bf_nil} @ bitfield_raw<u64>")]]
[[rc::returns("{bf_cons (range_of i 1) (bf_mask 1) bf_nil} @ bitfield_raw<u64>")]]
[[rc::trust_me]]
u64 BIT(int i);
[[rc::parameters("h : nat", "l : nat")]]
[[rc::parameters("h : Z", "l : Z")]]
[[rc::args("h @ int<i32>", "l @ int<i32>")]]
[[rc::requires("{0 ≤ l}", "{l < h < 64}")]]
[[rc::returns("{bf_cons (l, h - l + 1)%nat (bf_mask (h - l + 1)) bf_nil} @ bitfield_raw<u64>")]]
[[rc::returns("{bf_cons (range_of l (h - l + 1)) (bf_mask (h - l + 1)) bf_nil} @ bitfield_raw<u64>")]]
[[rc::trust_me]]
u64 GENMASK(int h, int l);
[[rc::parameters("r : tm", "a : nat", "k : nat", "norm : tm")]]
[[rc::args("{bf_cons (a, k) (bf_mask k) bf_nil} @ bitfield_raw<u64>", "r @ bitfield_raw<u64>")]]
[[rc::parameters("r : tm", "a : Z", "k : Z", "norm : tm")]]
[[rc::args("{bf_cons (range_of a k) (bf_mask k) bf_nil} @ bitfield_raw<u64>", "r @ bitfield_raw<u64>")]]
[[rc::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}")]]
[[rc::requires("{normalize (bf_slice (a, k) r) = norm}")]]
[[rc::returns("{eval norm} @ int<u64>")]]
[[rc::requires("{normalize (bf_slice (range_of a k) r) = norm}")]]
[[rc::returns("{bf_to_Z norm u64} @ int<u64>")]]
[[rc::trust_me]]
u64 FIELD_GET(u64 _mask, u64 _reg);
[[rc::parameters("a : nat", "k : nat", "v : Z")]]
[[rc::args("{bf_cons (a, k) (bf_mask k) bf_nil} @ bitfield_raw<u64>", "v @ int<u64>")]]
[[rc::parameters("a : Z", "k : Z", "v : Z")]]
[[rc::args("{bf_cons (range_of a k) (bf_mask k) bf_nil} @ bitfield_raw<u64>", "v @ int<u64>")]]
[[rc::requires("{a + k ≤ 64}", "{0 ≤ v < 2^k}")]]
[[rc::returns("{bf_cons (a, k) (bf_val v) bf_nil} @ bitfield_raw<u64>")]]
[[rc::returns("{bf_cons (range_of a k) (bf_val v) bf_nil} @ bitfield_raw<u64>")]]
[[rc::trust_me]]
u64 FIELD_PREP(u64 _mask, u64 _val);
......
......@@ -160,7 +160,7 @@ static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
[[rc::requires("{type = (if bool_decide (level = max_level - 1) then pte_type_page else pte_type_block)}")]]
[[rc::requires("{pte1 = (pte_from_addr pa) <| pte_valid := true |> <| pte_type := type |>"
"<| pte_leaf_attr_lo := pte_leaf_attr_lo attr |> <| pte_leaf_attr_hi := pte_leaf_attr_hi attr |>}")]]
[[rc::returns("{if pte_valid pte then bool_decide (eval (bitfield_repr pte) = eval (bitfield_repr pte1)) else true} @ boolean<bool_it>")]]
[[rc::returns("{if pte_valid pte then bf_eqb (bitfield_repr pte) (bitfield_repr pte1) bitfield_it else true} @ boolean<bool_it>")]]
[[rc::ensures("own p : {if pte_valid pte then pte else pte1} @ bitfield<Pte>")]]
// [[rc::trust_me]] // why term eq?
static bool kvm_set_valid_leaf_pte(kvm_pte_t *ptep, u64 pa, kvm_pte_t attr,
......
From refinedc.typing Require Import typing.
From refinedc.lang.bitfield Require Import bitwise.
(* pte *)
......@@ -28,15 +27,15 @@ Definition pte_from_addr (pa : Pte) : Pte :=
empty_pte <| pte_addr := pte_addr pa |>.
Definition pte_pa (pa : Pte) : tm :=
bf_cons (12, 36)%nat (bf_val $ pte_addr pa) bf_nil.
bf_cons (range_of 12 36) (bf_val $ pte_addr pa) bf_nil.
Definition pte_repr (p : Pte) : tm :=
bf_cons (0, 1)%nat (bf_val $ Z_of_bool $ pte_valid p) $
bf_cons (1, 1)%nat (bf_val $ pte_type p) $
bf_cons (2, 10)%nat (bf_val $ pte_leaf_attr_lo p) $
bf_cons (12, 36)%nat (bf_val $ pte_addr p) $
bf_cons (48, 3)%nat (bf_val $ pte_undef p) $
bf_cons (51, 13)%nat (bf_val $ pte_leaf_attr_hi p) $
bf_cons (range_of 0 1) (bf_val $ Z_of_bool $ pte_valid p) $
bf_cons (range_of 1 1) (bf_val $ pte_type p) $
bf_cons (range_of 2 10) (bf_val $ pte_leaf_attr_lo p) $
bf_cons (range_of 12 36) (bf_val $ pte_addr p) $
bf_cons (range_of 48 3) (bf_val $ pte_undef p) $
bf_cons (range_of 51 13) (bf_val $ pte_leaf_attr_hi p) $
bf_nil.
Arguments pte_repr _/.
......@@ -54,16 +53,19 @@ Global Program Instance Pte_BitfieldDesc : BitfieldDesc Pte := {|
bitfield_repr := pte_repr;
bitfield_wf := pte_wf;
bitfield_sig := {|
sig_length := 6;
sig_ranges := [# (0, 1)%nat; (1, 1)%nat; (2, 10)%nat; (12, 36)%nat;
(48, 3)%nat; (51, 13)%nat]
sig_bits := 64;
sig_ranges := [# (range_of 0 1); (range_of 1 1); (range_of 2 10); (range_of 12 36);
(range_of 48 3); (range_of 51 13)];
|}
|}.
Next Obligation. by repeat econstructor. Qed.
Next Obligation. Admitted. (* derivable from the first *)
Next Obligation. Admitted.
Next Obligation. done. Qed.
(*
Example pte_repr_sound p :
pte_wf p → check_has_ty (pte_repr p) (bv bitfield_sig).
Admitted.
Admitted. *)
Global Instance simpl_exist_Pte P : SimplExist Pte P
( valid type leaf_attr_lo addr undef leaf_attr_hi,
......@@ -99,11 +101,11 @@ Record Attr := {
}.
Definition attr_repr (a : Attr) : tm :=
bf_cons (2, 3)%nat (bf_val $ attr_lo_s1_attridx a) $
bf_cons (6, 2)%nat (bf_val $ attr_lo_s1_ap a) $
bf_cons (8, 2)%nat (bf_val $ attr_lo_s1_sh a) $
bf_cons (10, 1)%nat (bf_val $ Z_of_bool $ attr_lo_s1_af a) $
bf_cons (54, 1)%nat (bf_val $ Z_of_bool $ attr_hi_s1_xn a)
bf_cons (range_of 2 3) (bf_val $ attr_lo_s1_attridx a) $
bf_cons (range_of 6 2) (bf_val $ attr_lo_s1_ap a) $
bf_cons (range_of 8 2) (bf_val $ attr_lo_s1_sh a) $
bf_cons (range_of 10 1) (bf_val $ Z_of_bool $ attr_lo_s1_af a) $
bf_cons (range_of 54 1) (bf_val $ Z_of_bool $ attr_hi_s1_xn a)
bf_nil.
Arguments attr_repr _/.
......@@ -120,12 +122,15 @@ Global Program Instance Attr_BitfieldDesc : BitfieldDesc Attr := {|
bitfield_repr := attr_repr;
bitfield_wf := attr_wf;
bitfield_sig := {|
sig_length := 5;
sig_ranges := [# (2, 2)%nat; (6, 2)%nat; (8, 2)%nat; (10, 1)%nat;
(54, 1)%nat]
sig_bits := 64;
sig_ranges := [# (range_of 2 3); (range_of 6 2); (range_of 8 2); (range_of 10 1);
(range_of 54 1)]
|}
|}.
Next Obligation. Admitted.
Next Obligation. Admitted.
Next Obligation. Admitted.
Next Obligation. done. Qed.
(* pte prot *)
......@@ -137,10 +142,10 @@ Record Prot := {
}.
Definition prot_repr (p : Prot) : tm :=
bf_cons (0, 1)%nat (bf_val $ Z_of_bool $ prot_x p) $
bf_cons (1, 1)%nat (bf_val $ Z_of_bool $ prot_w p) $
bf_cons (2, 1)%nat (bf_val $ Z_of_bool $ prot_r p) $
bf_cons (3, 1)%nat (bf_val $ Z_of_bool $ prot_device p) $
bf_cons (range_of 0 1) (bf_val $ Z_of_bool $ prot_x p) $
bf_cons (range_of 1 1) (bf_val $ Z_of_bool $ prot_w p) $
bf_cons (range_of 2 1) (bf_val $ Z_of_bool $ prot_r p) $
bf_cons (range_of 3 1) (bf_val $ Z_of_bool $ prot_device p) $
bf_nil.
Arguments prot_repr _/.
......@@ -156,11 +161,14 @@ Global Program Instance Prot_BitfieldDesc : BitfieldDesc Prot := {|
bitfield_repr := prot_repr;
bitfield_wf := prot_wf;
bitfield_sig := {|
sig_length := 4;
sig_ranges := [# (0, 1)%nat; (1, 1)%nat; (2, 1)%nat; (3, 1)%nat]
sig_bits := 64;
sig_ranges := [# range_of 0 1; range_of 1 1; range_of 2 1; range_of 3 1]
|}
|}.
Next Obligation. Admitted.
Next Obligation. Admitted.
Next Obligation. Admitted.
Next Obligation. done. Qed.
Global Instance simpl_exist_Prot P : SimplExist Prot P ( x w r device,
P {| prot_x := x; prot_w := w; prot_r := r; prot_device := device |}).
......
This diff is collapsed.
From stdpp Require Import relations fin.
From Coq Require Import ssreflect.
From refinedc.lang.bitfield Require Import calculus semantics provability.
From refinedc.lithium Require Import base simpl_classes.
(* Actually all apis used by RefinedC *)
Local Open Scope Z_scope.
Local Open Scope bf_scope.
Definition check_range_eq (r1 r2 : range) : bool :=
(offset r1 =? offset r2)%nat && (width r1 =? width r2)%nat.
Infix "=?" := check_range_eq (at level 70) : bf_scope.
Lemma check_range_eq_spec r1 r2 :
r1 = r2 r1 =? r2 = true.
Proof.
rewrite andb_true_iff !Nat.eqb_eq.
destruct r1; destruct r2; rewrite pair_equal_spec.
naive_solver.
Qed.
Definition check_range_prec (r1 r2 : range) : bool :=
offset r1 + width r1 <=? offset r2.
Infix "≺?" := check_range_prec (at level 40) : bf_scope.
Lemma check_range_prec_spec r1 r2 :
r1 r2 r1 ? r2 = true.
Proof.
by rewrite Z.leb_le.
Qed.
Definition check_range_prec_head (r : range) (l : list range) : bool :=
match l with
| [] => true
| r' :: _ => r ? r'
end.
Lemma check_range_prec_head_spec r l :
range_prec_head r l check_range_prec_head r l = true.
Proof.
destruct l => //=.
by rewrite check_range_prec_spec.
Qed.
Definition check_disjoint (l1 : list range) (l2 : list range) : bool := true.
Lemma check_disjoint_spec l1 l2 :
l1 ## l2 check_disjoint l1 l2 = true.
Admitted.
Fixpoint check_has_ty (t : tm) (τ : ty) : bool :=
match t, τ with
| bf_val n, val σ f =>
bool_decide (0 n < 2 ^ (field_width σ f))
| bf_mask k, val σ f =>
(k =? field_width σ f)%nat
| bf_nil, bv σ => true
| bf_nil, mv σ => true
| bf_cons r x t, bv σ =>
default false (
f recognize σ r;
Some (check_range_prec_head r (ranges t)
&& check_has_ty x (val σ f)
&& check_has_ty t (bv σ))
)
| bf_cons r (bf_mask k) t, mv σ =>
default false (
f recognize σ r;
Some (check_range_prec_head r (ranges t)
&& (width r =? k)%Z
&& check_has_ty t (mv σ))
)
| bf_slice r t, val σ f =>
(sig_ranges σ !!! f =? r) && check_has_ty t (bv σ)
| bf_update r x t, bv σ =>
default false (
f recognize σ r;
Some (check_has_ty x (val σ f) && check_has_ty t (mv σ))
)
| bf_and t1 t2, bv σ =>
check_has_ty t1 (bv σ) && check_has_ty t2 (mv σ)
| bf_and_neg t1 t2, bv σ =>
check_has_ty t1 (bv σ) && check_has_ty t2 (mv σ)
| bf_or t1 t2, mv σ =>
check_has_ty t1 (mv σ) && check_has_ty t2 (mv σ)
&& (check_disjoint (ranges t1) (ranges t2))
| bf_or t1 t2, bv σ =>
check_has_ty t1 (bv σ) && check_has_ty t2 (bv σ)
&& (check_disjoint (ranges t1) (ranges t2) || check_has_ty t2 (mv σ))
| _, _ => false
end.
Ltac push_Some :=
repeat match goal with
| [ H : ?o = Some _ |- context [ (?o = _) ] ] =>
rewrite H; simpl
end.
Lemma check_has_ty_spec t τ :
t : τ check_has_ty t τ = true.
Proof.
split.
- induction 1; simpl check_has_ty.
all: rewrite ?andb_true_iff ?bool_decide_eq_true //.
+ by apply Nat.eqb_eq.
+ push_Some. destruct x => //.
all: do 2 rewrite andb_true_iff.
all: rewrite -check_range_prec_head_spec; naive_solver.
+ push_Some. rewrite !andb_true_iff -check_range_prec_head_spec.
Admitted.
Fixpoint check_nonzero (t : tm) : bool :=
match t with
| bf_cons r x t => bool_decide (eval x 0) || check_nonzero t
| _ => false
end.
Fixpoint check_zero (t : tm) : bool :=
match t with
| bf_cons r x t => bool_decide (eval x = 0) && check_zero t
| _ => true
end.
Fixpoint ensure_zero (v : tm) : Prop :=
match v with
| bf_nil => True
| bf_cons r x v' => (eval x = 0) ensure_zero v'
| _ => False (* error *)
end.
Fixpoint ensure_eq (v1 : tm) : tm Prop :=
fix cmp_aux v2 :=
match v1, v2 with
| bf_nil, _ => ensure_zero v2
| _, bf_nil => ensure_zero v1
| bf_cons r1 x1 v1', bf_cons r2 x2 v2' =>
if (r1 =? r2) then (eval x1 = eval x2) ensure_eq v1' v2'
else if (r1 ? r2) then (eval x1 = 0) ensure_eq v1' (bf_cons r2 x2 v2')
else (eval x2 = 0) cmp_aux v2'
| _, _ => eval v1 = eval v2
end.
Global Instance bf_cons_eq r x1 l1 x2 l2 :
SimplAnd (bf_cons r x1 l1 = bf_cons r x2 l2) (λ T, x1 = x2 l1 = l2 T).
Proof.
unfold SimplAnd in *.
naive_solver.
Qed.
Global Instance bf_val_eq x1 x2 :
SimplAnd (bf_val x1 = bf_val x2) (λ T, x1 = x2 T).
Proof.
unfold SimplAnd in *.
naive_solver.
Qed.
(* TODO *)
Definition check_bound (t : tm) (bits : Z) : bool := true.
(* normalize no bool decide *)
Fixpoint do_slice (r' : range) (v' : tm) : tm :=
match v' with
| bf_cons r x v => if r =? r' then x else do_slice r' v
| _ => bf_val 0
end.
Fixpoint do_update (r' : range) (x' v' : tm) : tm :=
match v' with
| bf_nil => bf_cons r' x' bf_nil
| bf_cons r x v =>
if (r =? r') then bf_cons r' x' v
else if (r ? r') then bf_cons r x (do_update r' x' v)
else (* r' ≺ r *) bf_cons r' x' v'
| _ => bf_nil (* error *)
end.
Fixpoint do_mask (v1 v2 : tm) : tm :=
match v2 with
| bf_cons r _ (* is mask *) v => bf_cons r (do_slice r v1) (do_mask v1 v)
| _ => bf_nil
end.
Fixpoint do_clr (v1 v2 : tm) : tm :=
match v2 with
| bf_cons r _ (* is mask *) v => do_update r (bf_val 0) (do_clr v1 v)
| _ => v1
end.
Fixpoint do_union (v1' v2' : tm) {struct v1'} : tm :=
let fix union_aux v2' {struct v2'} :=
match v1', v2' with
| bf_nil, _ => v2'
| _, bf_nil => v1'
| bf_cons r1 x1 v1, bf_cons r2 x2 v2 =>
if (r1 =? r2) then (* x2 is mask *) bf_cons r2 x2 (do_union v1 v2)
else if (r1 ? r2) then bf_cons r1 x1 (do_union v1 v2')
else (* r2 ≺ r1 *) bf_cons r2 x2 (union_aux v2)
| _, _ => bf_nil (* error *)
end
in union_aux v2'.
Fixpoint do_normalize (t : tm) : tm :=
match t with
| bf_val _ => t
| bf_mask _ => t
| bf_nil => t
| bf_cons r x t => bf_cons r (do_normalize x) (do_normalize t)
| bf_slice r t => do_slice r (do_normalize t)
| bf_update r x t => do_update r (do_normalize x) (do_normalize t)
| bf_and t1 t2 => do_mask (do_normalize t1) (do_normalize t2)
| bf_and_neg t1 t2 => do_clr (do_normalize t1) (do_normalize t2)
| bf_or t1 t2 => do_union (do_normalize t1) (do_normalize t2)
end.
......@@ -3,4 +3,4 @@
(package refinedc)
(flags -w -notation-overridden -w -redundant-canonical-projection)
(synopsis "Core language")
(theories refinedc.lithium))
(theories refinedc.lithium refinedc.mask_core))
......@@ -31,7 +31,7 @@ Ltac normalize_autorewrite :=
#[export] Hint Rewrite keep_factor2_min_1 keep_factor2_twice : lithium_rewrite.
(* basic boolean simplification *)
#[export] Hint Rewrite Bool.andb_false_r Bool.andb_true_r Bool.orb_true_r Bool.orb_false_r : lithium_rewrite.
#[export] Hint Rewrite andb_false_r andb_true_r orb_true_r orb_false_r negb_involutive : lithium_rewrite.
Lemma bool_decide_Z_of_bool_z b :
bool_decide (Z_of_bool b = 0) = negb b.
......
......@@ -7,9 +7,34 @@ Local Set Keyed Unification.
Local Open Scope bool_scope.
Local Open Scope Z_scope.
(* Z_lunot *)
Definition Z_lunot (N n : Z) := Z.lnot n `mod` 2 ^ N.
Lemma Z_lunot_spec N n k :
0 k < N Z.testbit (Z_lunot N n) k = negb (Z.testbit n k).
Proof.
move => [? ?].
by rewrite Z.mod_pow2_bits_low ?Z.lnot_spec.
Qed.
Lemma Z_lunot_spec_high N n k:
0 N k Z.testbit (Z_lunot N n) k = false.
Proof.
move => ?. by rewrite Z.mod_pow2_bits_high.
Qed.
Lemma Z_lunot_bounded N n:
0 N 0 Z_lunot N n < 2 ^ N.
Proof.
move => ?.
apply: Z.mod_pos_bound.
by apply: Z.pow_pos_nonneg.
Qed.
Create HintDb simplify_bool_eq_db discriminated.
Hint Rewrite
#[export] Hint Rewrite
Bool.andb_false_r
Bool.andb_true_r
Bool.andb_false_l
......@@ -28,7 +53,7 @@ Ltac simplify_bool_eq := autorewrite with simplify_bool_eq_db.
Create HintDb simplify_index_db discriminated.
Hint Rewrite
#[export] Hint Rewrite
Z.sub_add
Z.add_simpl_r
: simplify_index_db.
......@@ -47,7 +72,7 @@ Qed.
Create HintDb rewrite_bits_db discriminated.
Hint Rewrite
#[export] Hint Rewrite
(* 0 *)
Z.bits_0
(* 1 *)
......@@ -62,6 +87,8 @@ Hint Rewrite
Z.shiftl_spec
Z.shiftr_spec
Z.lnot_spec
Z_lunot_spec
Z_lunot_spec_high
Z.ldiff_spec
(* Z.ones *)
Z.ones_spec_high
......@@ -92,6 +119,7 @@ Local Ltac solve_or_split_step :=
match goal with
| |- context [Z.testbit _ ?i] => compare_cases 0 i
| |- context [Z.testbit (Z.ones ?sz) ?i] => compare_cases sz i
| |- context [Z.testbit (Z_lunot ?sz _) ?i] => compare_cases sz i
end.
Ltac bitblast :=
......@@ -102,6 +130,12 @@ Ltac bitblast :=
(** tests **)
Lemma Z_lunot_0 N :
0 N Z_lunot N 0 = Z.ones N.
Proof.
intros. bitblast.
Qed.
Goal x a k,
Z.land x (Z.land (Z.ones k) (Z.ones k) a) =
Z.land (Z.land (x a) (Z.ones k)) (Z.ones k) a.
......
From Coq Require Import ssreflect.
From stdpp Require Import numbers.
From refinedc.lang.bitfield Require Import bitblast.
From refinedc.mask_core Require Import bitblast.
(* To be compatible with proofs made in RefinedC. *)
Local Set SsrOldRewriteGoalsOrder.
Local Open Scope Z_scope.
Definition Z_lunot (bits n : Z) := Z.lnot n `mod` 2 ^ bits.
Module rc.
(* raw bit vector constructors *)
......@@ -24,8 +22,8 @@ Definition bf_mask_cons (a k : Z) (l : Z) : Z :=
Definition bf_slice (a k : Z) (bv : Z) : Z :=
Z.land (bv a) (Z.ones k).
Definition bf_update (a k x : Z) (bv : Z) : Z :=
Z.lor (Z.land bv (Z.lnot (Z.ones k a))) (x a).
Definition bf_update (a k x : Z) (bv : Z) (N : Z) : Z :=
Z.lor (Z.land bv (Z_lunot N (Z.ones k a))) (x a).
(* bound lemmas *)
......@@ -37,6 +35,72 @@ Proof.
apply Z.mod_pos_bound, Z.pow_pos_nonneg; lia.
Qed.
Lemma Z_land_bounded_nonneg a b N :
0 N
0 a < 2 ^ N
0 b < 2 ^ N
0 Z.land a b < 2 ^ N.
Proof.
move => ? [? Ha] [? Hb].
move : Ha Hb.
have ? : 0 Z.land a b by apply Z.land_nonneg; naive_solver.
rewrite !Z_bounded_iff_bits_nonneg //.
setoid_rewrite Z.land_spec.
setoid_rewrite andb_false_iff.
naive_solver.
Qed.
Lemma Z_lor_bounded_nonneg a b N :
0 N
0 a < 2 ^ N
0 b < 2 ^ N
0 Z.lor a b < 2 ^ N.