Skip to content

GitLab

Commit 54eaf6ac authored by Paul's avatar Paul
Browse files

draft impl using deep terms

parent 098b83ba
Expand all Hide whitespace changes
Inline Side-by-side
linux/casestudies/bits.h
View file @ 54eaf6ac
......@@ -10,29 +10,33 @@ typedef uint8_t u8;
#define BITS_PER_LONG (sizeof(long) * 8)
[[rc::parameters("i : Z")]]
[[rc::parameters("i : nat")]]
[[rc::args("i @ int<i32>")]]
[[rc::requires("{0 ≤ i < 64}")]]
[[rc::returns("{bf_mask_cons i 1 bf_nil} @ bitfield_raw<u64>")]]
[[rc::returns("{bf_cons (i, 1)%nat (bf_mask 1) bf_nil} @ bitfield_raw<u64>")]]
[[rc::trust_me]]
u64 BIT(int i);
[[rc::parameters("h : Z", "l : Z")]]
[[rc::parameters("h : nat", "l : nat")]]
[[rc::args("h @ int<i32>", "l @ int<i32>")]]
[[rc::requires("{0 ≤ l}", "{l < h < 64}")]]
[[rc::returns("{bf_mask_cons l (h - l + 1) bf_nil} @ bitfield_raw<u64>")]]
[[rc::returns("{bf_cons (l, h - l + 1)%nat (bf_mask (h - l + 1)) bf_nil} @ bitfield_raw<u64>")]]
[[rc::trust_me]]
u64 GENMASK(int h, int l);
[[rc::parameters("r : Z", "a : Z", "k : Z", "res : Z")]]
[[rc::args("{bf_mask_cons a k bf_nil} @ bitfield_raw<u64>", "r @ bitfield_raw<u64>")]]
[[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::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}")]]
[[rc::requires("{normalize_bitfield_eq (bf_slice a k r) res}")]]
[[rc::returns("res @ int<u64>")]]
[[rc::requires("{normalize (bf_slice (a, k) r) = norm}")]]
[[rc::returns("{eval norm} @ int<u64>")]]
[[rc::trust_me]]
u64 FIELD_GET(u64 _mask, u64 _reg);
[[rc::parameters("a : Z", "k : Z", "v : Z")]]
[[rc::args("{bf_mask_cons a k bf_nil} @ bitfield_raw<u64>", "v @ int<u64>")]]
[[rc::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}", "{0 ≤ v < 2^k}")]]
[[rc::returns("{bf_cons a k v bf_nil} @ bitfield_raw<u64>")]]
[[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::requires("{a + k ≤ 64}", "{0 ≤ v < 2^k}")]]
[[rc::returns("{bf_cons (a, k) (bf_val v) bf_nil} @ bitfield_raw<u64>")]]
[[rc::trust_me]]
u64 FIELD_PREP(u64 _mask, u64 _val);
#endif
linux/casestudies/pgtable.c
View file @ 54eaf6ac
......@@ -51,7 +51,7 @@ struct [[rc::refined_by("mm_ops : mm_callbacks")]] kvm_pgtable_mm_ops {
// void (*put_page)(void *addr);
// int (*page_count)(void *addr);
// void* (*phys_to_virt)(phys_addr_t phys);
[[rc::field("function_ptr<{fn(∀ (p, a) : loc * Z; p @ &own (a @ int u64); True) → ∃ () : (), (mm_ops.(virt_to_phys) a) @ bitfield_raw u64; True}>")]]
[[rc::field("function_ptr<{fn(∀ (p, a) : loc * Z; p @ &own (a @ int u64); True) → ∃ () : (), (mm_ops.(virt_to_phys) a) @ bitfield Pte; True}>")]]
phys_addr_t (*virt_to_phys)(void *addr);
};
......@@ -123,9 +123,9 @@ static void kvm_set_invalid_pte(kvm_pte_t *ptep)
WRITE_ONCE(*ptep, pte & ~KVM_PTE_VALID);
}
[[rc::parameters("pa : Z")]]
[[rc::args("pa @ int<u64>")]]
[[rc::returns("{mk_pte_addr (addr_of pa)} @ bitfield<Pte>")]]
[[rc::parameters("pa : Pte")]]
[[rc::args("pa @ bitfield<Pte>")]]
[[rc::returns("{pte_pa pa} @ bitfield_tpd<Pte>")]]
static kvm_pte_t kvm_phys_to_pte(u64 pa)
{
kvm_pte_t pte = pa & KVM_PTE_ADDR_MASK;
......@@ -140,10 +140,9 @@ static kvm_pte_t kvm_phys_to_pte(u64 pa)
[[rc::args("p @ &own<pte @ bitfield<Pte>>", "q @ &own<va @ int<u64>>",
"o @ &own<mm_ops @ kvm_pgtable_mm_ops>")]]
[[rc::requires("{bitfield_wf pte}", "{pte_valid pte}")]]
[[rc::exists("pa : Z")]]
[[rc::ensures("{mm_ops.(virt_to_phys) va = pa}")]]
[[rc::ensures("own p : {mk_pte_addr (addr_of pa) <| pte_type := pte_type_table |>"
[[rc::ensures("own p : {(pte_from_addr (mm_ops.(virt_to_phys) va)) <| pte_type := pte_type_table |>"
"<| pte_valid := true |>} @ bitfield<Pte>")]]
// [[rc::trust_me]] // `virt_to_phys mm_ops va` not destructed?
static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
struct kvm_pgtable_mm_ops *mm_ops)
{
......@@ -155,14 +154,15 @@ static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
*ptep = pte;
}
[[rc::parameters("p : loc", "pte : Pte", "pa : Z", "attr : Pte", "level : Z", "type : Z", "pte1 : Pte")]]
[[rc::args("p @ &own<pte @ bitfield<Pte>>", "pa @ int<u64>", "attr @ bitfield<Pte>", "level @ int<u32>")]]
[[rc::parameters("p : loc", "pte : Pte", "pa : Pte", "attr : Pte", "level : Z", "type : Z", "pte1 : Pte")]]
[[rc::args("p @ &own<pte @ bitfield<Pte>>", "pa @ bitfield<Pte>", "attr @ bitfield<Pte>", "level @ int<u32>")]]
[[rc::requires("{bitfield_wf pte}", "{bitfield_wf attr}")]]
[[rc::requires("{type = (if bool_decide (level = max_level - 1) then pte_type_page else pte_type_block)}")]]
[[rc::requires("{pte1 = mk_pte_addr (addr_of pa) <| pte_valid := true |> <| pte_type := type |>"
[[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 (bitfield_repr pte = bitfield_repr pte1) else true} @ builtin_boolean")]]
[[rc::returns("{if pte_valid pte then bool_decide (eval (bitfield_repr pte) = eval (bitfield_repr pte1)) 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,
u32 level)
{
......@@ -201,6 +201,7 @@ struct [[rc::refined_by("phys : Z", "attr : Attr", "mm_ops : mm_callbacks", "o :
[[rc::requires("{attr = {| attr_lo_s1_attridx := mtype; attr_lo_s1_ap := ap; attr_lo_s1_sh := sh_is; attr_lo_s1_af := true; attr_hi_s1_xn := xn |} }")]]
[[rc::returns("{if err then -err_code else 0} @ int<i32>")]]
[[rc::ensures("own d : {if err then (phys, a, mm_ops, o) else (phys, attr, mm_ops, o)} @ hyp_map_data")]]
// [[rc::trust_me]]
static int hyp_map_set_prot_attr(kvm_pgtable_prot prot, struct hyp_map_data *data)
{
// TODO: remove 0 != once issue #45 is fixed
......
linux/casestudies/proofs/pgtable/pgtable_lemmas.v
View file @ 54eaf6ac
From refinedc.typing Require Import typing.
From refinedc.lang.bitfield Require Import bitwise.
(* pte *)
......@@ -23,15 +24,19 @@ Definition empty_pte := {|
pte_leaf_attr_hi := 0;
|}.
Definition mk_pte_addr (a : addr) : Pte := empty_pte <| pte_addr := a |>.
Definition pte_from_addr (pa : Pte) : Pte :=
empty_pte <| pte_addr := pte_addr pa |>.
Definition pte_repr (p : Pte) : Z :=
bf_cons 0 1 (bool_to_Z $ pte_valid p) $
bf_cons 1 1 (pte_type p) $
bf_cons 2 10 (pte_leaf_attr_lo p) $
bf_cons 12 36 (pte_addr p) $
bf_cons 48 3 (pte_undef p) $
bf_cons 51 13 (pte_leaf_attr_hi p) $
Definition pte_pa (pa : Pte) : tm :=
bf_cons (12, 36)%nat (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_nil.
Arguments pte_repr _/.
......@@ -44,11 +49,21 @@ Definition pte_wf (p : Pte) : Prop :=
0 ≤ pte_undef p < 2^3 ∧
0 ≤ pte_leaf_attr_hi p < 2^13.
Global Instance Pte_BitfieldDesc : BitfieldDesc Pte := {|
Global Program Instance Pte_BitfieldDesc : BitfieldDesc Pte := {|
bitfield_it := u64;
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]
|}
|}.
Next Obligation. Admitted.
Example pte_repr_sound p :
pte_wf p → check_has_ty (pte_repr p) (bv bitfield_sig).
Admitted.
Global Instance simpl_exist_Pte P : SimplExist Pte P
(∃ valid type leaf_attr_lo addr undef leaf_attr_hi,
......@@ -73,9 +88,6 @@ Global Instance simpl_forall_Pte P : SimplForall Pte 6 P
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Definition addr_of (n : Z) : Z :=
bf_slice 12 36 n.
(* pte attr *)
Record Attr := {
......@@ -86,12 +98,12 @@ Record Attr := {
attr_hi_s1_xn : bool;
}.
Definition attr_repr (a : Attr) : Z :=
bf_cons 2 2 (attr_lo_s1_attridx a) $
bf_cons 6 2 (attr_lo_s1_ap a) $
bf_cons 8 2 (attr_lo_s1_sh a) $
bf_cons 10 1 (bool_to_Z $ attr_lo_s1_af a) $
bf_cons 54 1 (bool_to_Z $ attr_hi_s1_xn a)
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_nil.
Arguments attr_repr _/.
......@@ -103,11 +115,17 @@ Definition attr_wf (a : Attr) : Prop :=
0 ≤ bool_to_Z $ attr_lo_s1_af a < 2^1 ∧
0 ≤ bool_to_Z $ attr_hi_s1_xn a < 2^1.
Global Instance Attr_BitfieldDesc : BitfieldDesc Attr := {|
Global Program Instance Attr_BitfieldDesc : BitfieldDesc Attr := {|
bitfield_it := u64;
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]
|}
|}.
Next Obligation. Admitted.
(* pte prot *)
......@@ -118,11 +136,11 @@ Record Prot := {
prot_device : bool;
}.
Definition prot_repr (p : Prot) : Z :=
bf_cons 0 1 (bool_to_Z $ prot_x p) $
bf_cons 1 1 (bool_to_Z $ prot_w p) $
bf_cons 2 1 (bool_to_Z $ prot_r p) $
bf_cons 3 1 (bool_to_Z $ prot_device p) $
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_nil.
Arguments prot_repr _/.
......@@ -133,11 +151,17 @@ Definition prot_wf (p : Prot) : Prop :=
0 ≤ bool_to_Z $ prot_r p < 2^1 ∧
0 ≤ bool_to_Z $ prot_device p < 2^1.
Global Instance Prot_BitfieldDesc : BitfieldDesc Prot := {|
Global Program Instance Prot_BitfieldDesc : BitfieldDesc Prot := {|
bitfield_it := u64;
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]
|}
|}.
Next Obligation. Admitted.
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 |}).
Proof. unfold SimplExist. naive_solver. Qed.
......@@ -148,7 +172,7 @@ Proof. unfold SimplForall => ? []. naive_solver. Qed.
(* struct, const *)
Record mm_callbacks := {
virt_to_phys : Z → Z;
virt_to_phys : Z → Pte;
}.
Definition max_level : Z := 4.
......
theories/lang/bitfield/bitblast.v 0 → 100644
View file @ 54eaf6ac
From Coq Require Import ssreflect.
From stdpp Require Import prelude.
From Coq.btauto Require Export Btauto.
Local Set Keyed Unification.
Local Open Scope bool_scope.
Local Open Scope Z_scope.
Create HintDb simplify_bool_eq_db discriminated.
Hint Rewrite
Bool.andb_false_r
Bool.andb_true_r
Bool.andb_false_l
Bool.andb_true_l
Bool.orb_false_r
Bool.orb_true_r
Bool.orb_false_l
Bool.orb_true_l
Bool.xorb_false_r
Bool.xorb_true_r
Bool.xorb_false_l
Bool.xorb_true_l
: simplify_bool_eq_db.
Ltac simplify_bool_eq := autorewrite with simplify_bool_eq_db.
Create HintDb simplify_index_db discriminated.
Hint Rewrite
Z.sub_add
Z.add_simpl_r
: simplify_index_db.
Local Ltac simplify_index := autorewrite with simplify_index_db.
Lemma Z_bits_1_0 k :
k = 0 → Z.testbit 1 k = true.
Proof. naive_solver. Qed.
Lemma Z_bits_1_above k :
0 < k → Z.testbit 1 k = false.
Proof.
intros. rewrite Z.bits_above_log2 //=.
Qed.
Create HintDb rewrite_bits_db discriminated.
Hint Rewrite
(* 0 *)
Z.bits_0
(* 1 *)
Z_bits_1_0
Z_bits_1_above
(* -1 *)
Z.bits_m1
(* bitwise *)
Z.land_spec
Z.lor_spec
Z.lxor_spec
Z.shiftl_spec
Z.shiftr_spec
Z.lnot_spec
Z.ldiff_spec
(* Z.ones *)
Z.ones_spec_high
Z.ones_spec_low
(* Z.testbit, Z.setbit *)
Z.testbit_neg_r
Z.setbit_eq
Z.setbit_neq
(* out-of-bound index *)
Z.bits_above_log2
using lia : rewrite_bits_db.
Local Ltac rewrite_bits := rewrite_strat (repeat (topdown (hints rewrite_bits_db))).
Ltac rewrite_testbit := repeat (simplify_bool_eq || simplify_index || rewrite_bits).
Local Ltac compare_cases cst i :=
tryif (first [assert (cst ≤ i) by lia | assert (i < cst) by lia])
then fail
else (let C := fresh "C" in
assert (i < cst ∨ cst ≤ i) as C by lia;
ring_simplify i in C;
destruct C as [C | C]).
Local Ltac solve_or_split_step :=
rewrite_testbit;
try solve [f_equal; (reflexivity || lia)];
match goal with
| |- context [Z.testbit _ ?i] => compare_cases 0 i
| |- context [Z.testbit (Z.ones ?sz) ?i] => compare_cases sz i
end.
Ltac bitblast :=
apply Z.bits_inj'; intros ?i ?Hi;
repeat solve_or_split_step;
rewrite_testbit;
try btauto.
(** tests **)
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.
by intros; bitblast. Abort.
Goal ∀ i,
1 ≪ i = Z.land (Z.ones 1) (Z.ones 1) ≪ i.
by intros; bitblast. Abort.
Goal ∀ N k,
0 ≤ k ≤ N → Z.ones N ≫ (N - k) = Z.ones k.
by intros; bitblast. Abort.
theories/lang/bitfield/bitwise.v 0 → 100644
View file @ 54eaf6ac
From Coq Require Import ssreflect.
From stdpp Require Import numbers.
From refinedc.lang.bitfield 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 *)
Definition bf_nil : Z := 0.
Definition bf_cons (a k x : Z) (l : Z) :=
Z.lor (x ≪ a) l.
Definition bf_mask_cons (a k : Z) (l : Z) : Z :=
bf_cons a k (Z.ones k) l.
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).
(* bound lemmas *)
Lemma bf_slice_bounded a k x :
0 ≤ k →
0 ≤ bf_slice a k x < 2 ^ k.
Proof.
intros. rewrite /bf_slice Z.land_ones; last done.
apply Z.mod_pos_bound, Z.pow_pos_nonneg; lia.
Qed.
(* bf range empty *)
Definition bf_range_empty a k bv : Prop :=
∀ i, a ≤ i < a + k → Z.testbit bv i = false.
Lemma bf_range_empty_nil a k :
bf_range_empty a k bf_nil.
Proof.
rewrite /bf_range_empty /bf_nil => i ?.
by rewrite Z.bits_0.
Qed.
Lemma bf_range_empty_cons a k x l a' k' :
0 ≤ a → 0 ≤ k → 0 ≤ a' → 0 ≤ k' →
0 ≤ x < 2^k →
(a + k ≤ a' ∨ a' + k' ≤ a) →
bf_range_empty a' k' (bf_cons a k x l) ↔ bf_range_empty a' k' l.
Proof.
rewrite /bf_range_empty /bf_cons => ???? [??] Hor.
split.
- move => Hl i [??].
have : Z.testbit (Z.lor (x ≪ a) l) i = false by apply Hl.
rewrite Z.lor_spec Z.shiftl_spec ?Hl; [|lia..].
by apply orb_false_elim.
- move => Hl i [??].
rewrite Z.lor_spec Z.shiftl_spec ?Hl; [|lia..].
simplify_bool_eq. destruct Hor.
+ apply (Z_bounded_iff_bits_nonneg k x); lia.
+ rewrite Z.testbit_neg_r //. lia.
Qed.
Lemma bf_range_empty_update a k x l a' k' :
0 ≤ a → 0 ≤ k → 0 ≤ a' → 0 ≤ k' →
0 ≤ x < 2^k →
(a + k ≤ a' ∨ a' + k' ≤ a) →
bf_range_empty a' k' l →
bf_range_empty a' k' (bf_update a k x l).
Proof.
rewrite /bf_range_empty /bf_update => ???? [??] Hor Hl i [??].
rewrite Z.lor_spec Z.land_spec Hl; [|lia].
simplify_bool_eq.
rewrite Z.shiftl_spec; [|lia].
destruct Hor.
+ apply (Z_bounded_iff_bits_nonneg k x); lia.
+ rewrite Z.testbit_neg_r //. lia.
Qed.
Lemma bf_range_empty_land a k bv1 bv2 :
(bf_range_empty a k bv1 ∨ bf_range_empty a k bv2) →
bf_range_empty a k (Z.land bv1 bv2).
Proof.
rewrite /bf_range_empty => Hbv i Hi.
destruct Hbv as [Hbv | Hbv].
all: specialize (Hbv _ Hi); rewrite Z.land_spec Hbv; by simplify_bool_eq.
Qed.
Lemma bf_range_empty_lor a k bv1 bv2 :
bf_range_empty a k bv1 →
bf_range_empty a k bv2 →
bf_range_empty a k (Z.lor bv1 bv2).
Proof.
rewrite /bf_range_empty => Hbv1 Hbv2 i Hi.
specialize (Hbv1 _ Hi).
specialize (Hbv2 _ Hi).
by rewrite Z.lor_spec Hbv1 Hbv2.
Qed.
Lemma bf_slice_zero_if_range_empty a k l :
0 ≤ k →
bf_range_empty a k l →
bf_slice a k l = 0.
Proof.
move => ? He. rewrite /bf_slice.
bitblast.
apply He. lia.
Qed.
(* Rewriting rules *)
Lemma bf_land_nil bv :
Z.land bv bf_nil = bf_nil.
Proof.
by rewrite Z.land_0_r.
Qed.
Lemma bf_land_mask_cons bv a k l :
0 ≤ a → 0 ≤ k →
Z.land bv (bf_mask_cons a k l) = bf_cons a k (bf_slice a k bv) (Z.land bv l).
Proof.
rewrite /bf_mask_cons /bf_cons /bf_slice => ??.
bitblast.
Qed.
Lemma bf_lor_nil_l bv :
Z.lor bf_nil bv = bv.
Proof. done. Qed.
Lemma bf_lor_nil_r bv :
Z.lor bv bf_nil = bv.
Proof.
by rewrite Z.lor_0_r.
Qed.
Lemma bf_lor_update_l a1 k1 x1 a2 k2 x2 dl1 dl2 :
0 ≤ a1 → 0 ≤ k1 → 0 ≤ a2 → 0 ≤ k2 →
a1 + k1 ≤ a2 →
Z.lor (bf_cons a1 k1 x1 dl1) (bf_cons a2 k2 x2 dl2) = bf_cons a1 k1 x1 (Z.lor dl1 (bf_cons a2 k2 x2 dl2)).
Proof.
rewrite /bf_cons => ?????.
bitblast.
Qed.
Lemma bf_lor_update_r a1 k1 x1 a2 k2 x2 dl1 dl2 :
0 ≤ a1 → 0 ≤ k1 → 0 ≤ a2 → 0 ≤ k2 →
a2 + k2 ≤ a1 →
Z.lor (bf_cons a1 k1 x1 dl1) (bf_cons a2 k2 x2 dl2) = bf_cons a2 k2 x2 (Z.lor (bf_cons a1 k1 x1 dl1) dl2).
Proof.
rewrite /bf_cons => ?????.
bitblast.
Qed.
Lemma bf_lor_mask_cons_r a k x dl1 dl2 :
0 ≤ a → 0 ≤ k →
0 ≤ x < 2^k →
Z.lor (bf_cons a k x dl1) (bf_mask_cons a k dl2) = bf_cons a k (Z.ones k) (Z.lor dl1 dl2).
Proof.
move => ? ? ?.
rewrite /bf_mask_cons /bf_cons.
bitblast.
have -> : Z.testbit x (i - a) = false
by apply (Z_bounded_iff_bits_nonneg k x); lia.
done.
Qed.
Lemma bf_slice_nil a k :
bf_slice a k bf_nil = 0.
Proof.
rewrite /bf_slice /bf_nil.
bitblast.
Qed.
Lemma bf_slice_cons a k x l :
0 ≤ a → 0 ≤ k →
0 ≤ x < 2^k →
bf_range_empty a k l →
bf_slice a k (bf_cons a k x l) = x.
Proof.
rewrite /bf_slice /bf_cons => ??? Hi.
bitblast.
rewrite Hi; [by simplify_bool_eq | lia].
symmetry. apply (Z_bounded_iff_bits_nonneg k x); lia.