Commit bd257222 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

Merge branch 'master' into rr

parents f6c582bf 7f3eee0b
......@@ -30,10 +30,10 @@ variables:
- api
## Build jobs
build-coq.8.13.2-timing:
build-coq.8.14.0-timing:
<<: *template
variables:
OPAM_PINS: "coq version 8.13.2 cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
OPAM_PINS: "coq version 8.14.0 cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
DENY_WARNINGS: "1"
OPAM_PKG: "1"
only:
......@@ -43,10 +43,10 @@ build-coq.8.13.2-timing:
tags:
- fp-timing
build-coq.8.13.2:
build-coq.8.14.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.13.2 cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
OPAM_PINS: "coq version 8.14.0 cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
DENY_WARNINGS: "1"
only:
- /^ci/@iris/refinedc
......@@ -54,7 +54,7 @@ build-coq.8.13.2:
trigger-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.13.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
OPAM_PINS: "coq version 8.14.0 coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
except:
only:
- triggers
......
(lang dune 2.7)
(lang dune 2.9)
(name refinedc)
(using coq 0.2)
(using coq 0.3)
......@@ -230,13 +230,13 @@ Section defs.
apply: fsm_invariant_partial_alter => //; destruct ir, ir'; naive_solver.
Qed.
Global Instance simpl_lookup_fsm_map_and mp key items n ir o `{!FastDone (fsm_invariant mp items)} `{!FastDone (probe_ref key items = Some (n, ir))}:
Global Instance simpl_lookup_fsm_map_and mp key items n ir o `{!TCFastDone (fsm_invariant mp items)} `{!TCFastDone (probe_ref key items = Some (n, ir))}:
SimplBothRel (=) (mp !! key) o (item_ref_to_ty ir = o).
Proof. unfold FastDone in *. by rewrite (fsm_invariant_lookup _ items _ n ir (item_ref_to_ty ir)). Qed.
Proof. unfold TCFastDone in *. by rewrite (fsm_invariant_lookup _ items _ n ir (item_ref_to_ty ir)). Qed.
Global Instance simpl_fsm_invariant_and mp1 mp2 items `{!IsProtected mp1} `{!FastDone (fsm_invariant mp2 items)}:
Global Instance simpl_fsm_invariant_and mp1 mp2 items `{!IsProtected mp1} `{!TCFastDone (fsm_invariant mp2 items)}:
SimplAndUnsafe true (fsm_invariant mp1 items) (λ T, mp1 = mp2 T) | 50.
Proof. unfold FastDone in *. by move => ? [->]. Qed.
Proof. unfold TCFastDone in *. by move => ? [->]. Qed.
Global Instance simpl_fsm_invariant_shelve_and mp items `{!ContainsProtected mp}:
SimplAndUnsafe true (fsm_invariant mp items) (λ T, shelve_hint (fsm_invariant mp items) T) | 100.
Proof. move => ?; unfold shelve_hint; eauto. Qed.
......
......@@ -61,13 +61,13 @@ Inductive range : Type :=
| ei : nat nat range (* (l, r] *)
.
Instance range_elem_of : ElemOf nat range := λ i I,
Global Instance range_elem_of : ElemOf nat range := λ i I,
match I with
| ie l r => l i i < r
| ei l r => l < i i r
end.
Instance range_elem_of_decision (i : nat) (I : range) : Decision (i I).
Global Instance range_elem_of_decision (i : nat) (I : range) : Decision (i I).
Proof.
destruct I as [l r | l r].
- destruct (decide (l i i < r)); by [ left | right ].
......
......@@ -7,7 +7,7 @@ Definition WrappingAdd (it1 it2 : int_type) (es : list expr) : expr :=
| _ => Val VOID
end%E.
Program Instance WrappingAdd_wf it1 it2 : MacroWfSubst (WrappingAdd it1 it2).
Global Program Instance WrappingAdd_wf it1 it2 : MacroWfSubst (WrappingAdd it1 it2).
Next Obligation. move => ???? [|?[|?[|??]]]//. Qed.
Typeclasses Opaque WrappingAdd.
......@@ -1288,7 +1288,13 @@ let pp_proof : Coq_path.t -> func_def -> import list -> string list
List.iter (fun (x,_) -> pp " arg_%s" x) def.func_args;
List.iter (fun (x,_) -> pp " local_%s" x) def.func_vars
end;
pp ".@;split_blocks ((";
pp ".@;";
if func_annot.fa_parameters <> [] then
begin
let pp_var ff (x, _) = pp_print_string ff x in
pp "prepare_parameters (%a).@;" (pp_sep " " pp_var) func_annot.fa_parameters;
end;
pp "split_blocks ((";
let pp_inv (id, annot) =
(* Opening a box and printing the existentials. *)
pp "@; @[<v 2><[ \"%s\" :=" id;
......
......@@ -72,9 +72,9 @@ 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::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}")]]
[[rc::requires("{normalize_bitfield (bf_slice a k r) res}")]]
[[rc::requires("{normalize_bitfield_eq (bf_slice a k r) res}")]]
[[rc::returns("res @ int<u64>")]]
[[rc::tactics("all: unfold normalize_bitfield in *; subst.")]]
[[rc::tactics("all: unfold normalize_bitfield_eq in *; subst.")]]
[[rc::tactics("all: try rewrite Z.add_simpl_r Z_least_significant_one_nonempty_mask.")]]
[[rc::tactics("all: try solve_goal.")]]
[[rc::lemmas("bf_mask_cons_singleton_nonempty", "bf_shr_singleton")]]
......@@ -208,7 +208,6 @@ static bool kvm_pte_valid(kvm_pte_t pte)
[[rc::returns("{if bool_decide (level = max_level - 1) then false \
else if negb (pte_valid pte) then false \
else bool_decide (pte_type pte = pte_type_table)} @ boolean<bool_it>")]]
[[rc::tactics("all: simpl_bool_hyp.")]]
static bool kvm_pte_table(kvm_pte_t pte, u32 level)
{
if (level == KVM_PGTABLE_MAX_LEVELS - 1)
......@@ -221,7 +220,7 @@ static bool kvm_pte_table(kvm_pte_t pte, u32 level)
[[rc::parameters("pte : Pte", "p : loc")]]
[[rc::args("p @ &own<pte @ bitfield<Pte>>")]]
[[rc::requires("{bitfield_wf pte}")]]
[[rc::ensures("own p : {pte_set_invalid pte} @ bitfield<Pte>")]]
[[rc::ensures("own p : {pte <| pte_valid := false |>} @ bitfield<Pte>")]]
static void kvm_set_invalid_pte(kvm_pte_t *ptep)
{
kvm_pte_t pte = *ptep;
......@@ -247,7 +246,8 @@ static kvm_pte_t kvm_phys_to_pte(u64 pa)
[[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 : { {| pte_valid := true; pte_type := pte_type_table; pte_leaf_attr_lo := 0; pte_addr := (addr_of pa); pte_undef := 0; pte_leaf_attr_hi := 0 |} } @ bitfield<Pte>")]]
[[rc::ensures("own p : {mk_pte_addr (addr_of pa) <| pte_type := pte_type_table |>"
"<| pte_valid := true |>} @ bitfield<Pte>")]]
static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
struct kvm_pgtable_mm_ops *mm_ops)
{
......@@ -263,10 +263,10 @@ static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
[[rc::args("p @ &own<pte @ bitfield<Pte>>", "pa @ int<u64>", "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 = {| pte_valid := true; pte_type := type; pte_leaf_attr_lo := pte_leaf_attr_lo attr; pte_addr := (addr_of pa); pte_undef := 0; pte_leaf_attr_hi := pte_leaf_attr_hi attr |} }")]]
[[rc::requires("{pte1 = mk_pte_addr (addr_of 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} @ boolean<bool_it>")]]
[[rc::ensures("own p : {if pte_valid pte then pte else pte1} @ bitfield<Pte>")]]
[[rc::tactics("all: simpl_bool_hyp.")]]
static bool kvm_set_valid_leaf_pte(kvm_pte_t *ptep, u64 pa, kvm_pte_t attr,
u32 level)
{
......@@ -305,8 +305,6 @@ 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::tactics("all: try congruence.")]]
[[rc::tactics("all: simpl_bool_hyp.")]]
static int hyp_map_set_prot_attr(kvm_pgtable_prot prot, struct hyp_map_data *data)
{
// TODO: remove 0 != once issue #45 is fixed
......
......@@ -2,7 +2,7 @@ From refinedc.typing Require Import typing.
(* pte *)
Record Pte := {
Record Pte := mk_pte {
pte_valid : bool;
pte_type : Z;
pte_leaf_attr_lo : Z;
......@@ -11,24 +11,20 @@ Record Pte := {
pte_leaf_attr_hi : Z;
}.
Definition pte_set_invalid (pte : Pte) : Pte := {|
pte_valid := false;
pte_type := pte_type pte;
pte_leaf_attr_lo := pte_leaf_attr_lo pte;
pte_addr := pte_addr pte;
pte_undef := pte_undef pte;
pte_leaf_attr_hi := pte_leaf_attr_hi pte;
|}.
Global Instance Pte_settable : Settable _ := settable! mk_pte
<pte_valid; pte_type; pte_leaf_attr_lo; pte_addr; pte_undef; pte_leaf_attr_hi>.
Definition mk_pte_addr (a : Z) : Pte := {|
Definition empty_pte := {|
pte_valid := false;
pte_type := 0;
pte_leaf_attr_lo := 0;
pte_addr := a;
pte_addr := 0;
pte_undef := 0;
pte_leaf_attr_hi := 0;
|}.
Definition mk_pte_addr (a : addr) : Pte := empty_pte <| pte_addr := a |>.
Definition pte_repr (p : Pte) : Z :=
bf_cons 0 1 (Z_of_bool $ pte_valid p) $
bf_cons 1 1 (pte_type p) $
......@@ -54,6 +50,29 @@ Global Instance Pte_BitfieldDesc : BitfieldDesc Pte := {|
bitfield_wf := pte_wf;
|}.
Global Instance simpl_exist_Pte P : SimplExist Pte P
( valid type leaf_attr_lo addr undef leaf_attr_hi,
P {|
pte_valid := valid;
pte_type := type;
pte_leaf_attr_lo := leaf_attr_lo;
pte_addr := addr;
pte_undef := undef;
pte_leaf_attr_hi := leaf_attr_hi;
|}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_Pte P : SimplForall Pte 6 P
( valid type leaf_attr_lo addr undef leaf_attr_hi,
P {|
pte_valid := valid;
pte_type := type;
pte_leaf_attr_lo := leaf_attr_lo;
pte_addr := addr;
pte_undef := undef;
pte_leaf_attr_hi := leaf_attr_hi;
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Definition addr_of (n : Z) : Z :=
bf_slice 12 36 n.
......@@ -119,6 +138,12 @@ Global Instance Prot_BitfieldDesc : BitfieldDesc Prot := {|
bitfield_repr := prot_repr;
bitfield_wf := prot_wf;
|}.
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.
Global Instance simpl_forall_Prot P : SimplForall Prot 4 P ( x w r device,
P {| prot_x := x; prot_w := w; prot_r := r; prot_device := device |}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
(* struct, const *)
......@@ -136,19 +161,3 @@ Definition ap_rw : Z := 1.
Definition ap_ro : Z := 3.
Definition sh_is : Z := 3.
Definition err_code : Z := 22.
(* tactics TODO: SimplImpl *)
Ltac simpl_bool_hyp :=
repeat (match goal with
| [ H : negb ?b = true |- _ ] =>
assert (b = false) by apply negb_true_iff; clear H
| [ H : negb ?b = false |- _ ] =>
assert (b = true) by apply negb_false_iff; clear H
| [ H : bf_cons ?a 1 (Z_of_bool ?b) bf_nil = 0 |- _ ] =>
assert (b = false) by (by apply (bf_cons_bool_singleton_false_iff a b)); clear H
| [ H : bf_cons ?a 1 (Z_of_bool ?b) bf_nil 0 |- _ ] =>
assert (b = true) by (by apply (bf_cons_bool_singleton_true_iff a b)); clear H
| [ H : ?b = false |- _ ] => try (rewrite !H; clear H)
| [ H : ?b = true |- _ ] => try (rewrite !H; clear H)
end; try solve_goal).
......@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
Lemma shift_12_eq_mul_4096 n :
(n 12) = n * 4096.
Proof. by rewrite Z.shiftl_mul_pow2. Qed.
Hint Rewrite shift_12_eq_mul_4096 : lithium_rewrite.
#[export] Hint Rewrite shift_12_eq_mul_4096 : lithium_rewrite.
Lemma ly_size_PAGES i : ly_size (PAGES i) = (i * Z.to_nat PAGE_SIZE)%nat.
Proof. by rewrite /PAGES /ly_with_align /ly_size. Qed.
......@@ -38,12 +38,12 @@ Proof. rewrite !ly_size_PAGES. lia. Qed.
Typeclasses Opaque PAGES.
Global Opaque PAGES.
Hint Rewrite ly_size_ly_offset : lithium_rewrite.
Hint Rewrite ly_size_PAGES_sub : lithium_rewrite.
Hint Rewrite ly_size_PAGES : lithium_rewrite.
Hint Rewrite ly_offset_PAGES : lithium_rewrite.
#[export] Hint Rewrite ly_size_ly_offset : lithium_rewrite.
#[export] Hint Rewrite ly_size_PAGES_sub : lithium_rewrite.
#[export] Hint Rewrite ly_size_PAGES : lithium_rewrite.
#[export] Hint Rewrite ly_offset_PAGES : lithium_rewrite.
Hint Rewrite ly_size_ly_offset : refinedc_loc_eq_rewrite.
Hint Rewrite ly_size_PAGES_sub : refinedc_loc_eq_rewrite.
Hint Rewrite ly_size_PAGES : refinedc_loc_eq_rewrite.
Hint Rewrite ly_offset_PAGES : refinedc_loc_eq_rewrite.
#[export] Hint Rewrite ly_size_ly_offset : refinedc_loc_eq_rewrite.
#[export] Hint Rewrite ly_size_PAGES_sub : refinedc_loc_eq_rewrite.
#[export] Hint Rewrite ly_size_PAGES : refinedc_loc_eq_rewrite.
#[export] Hint Rewrite ly_offset_PAGES : refinedc_loc_eq_rewrite.
......@@ -25,7 +25,7 @@ Class spinlockG Σ := SpinLockG {
Definition spinlockΣ : gFunctors :=
#[GFunctor (constRF (gmapR Z (exclR unitO)));
GFunctor (constRF (excl_authR ZO))].
Instance subG_spinlockG {Σ} : subG spinlockΣ Σ spinlockG Σ.
Global Instance subG_spinlockG {Σ} : subG spinlockΣ Σ spinlockG Σ.
Proof. solve_inG. Qed.
Section type.
......
......@@ -16,14 +16,15 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
depends: [
"coq" { (>= "8.13.2" & < "8.15~") }
"coq" { (>= "8.14.0" & < "8.15~") }
"coq-iris" { (= "dev.2021-09-13.0.6575260a") | (= "dev") }
"dune" {>= "2.7.0"}
"dune" {>= "2.9.1"}
"cerberus" {= "~dev"}
"cmdliner" {>= "1.0.4"}
"earley" {= "3.0.0"}
"toml" {= "5.0.0"}
"ubase" {= "0.04"}
"coq-record-update" {= "0.3.0"}
]
build: [
......
From refinedc.lang Require Import base int_type builtins_specs.
From refinedc.lithium Require Import simpl_classes tactics_extend infrastructure Z_bitblast.
From refinedc.lithium Require Import simpl_classes tactics_extend infrastructure Z_bitblast classes.
Local Open Scope Z_scope.
(* raw bit vector constructors *)
Definition bf_nil : Z := 0.
......@@ -26,25 +27,35 @@ Proof.
bitblast.
Qed.
Lemma bf_cons_singleton_z_iff a k x :
0 a
bf_cons a k x bf_nil = 0 x = 0.
Proof.
move => ?. rewrite /bf_cons /bf_nil Z.lor_0_r.
by apply Z.shiftl_eq_0_iff.
Qed.
Lemma bf_cons_singleton_nz_iff a k x :
0 a
bf_cons a k x bf_nil 0 x 0.
Proof.
move => ?. by apply not_iff_compat, bf_cons_singleton_z_iff.
Qed.
Lemma bf_cons_bool_singleton_false_iff a b :
0 a
bf_cons a 1 (Z_of_bool b) bf_nil = 0 b = false.
Proof.
intros. rewrite /bf_cons /bf_nil Z.lor_0_r.
split.
- destruct b; last done.
simplify_eq/=. rewrite Z.shiftl_1_l.
have ? : 2 ^ a 0 by apply Z.pow_nonzero.
contradiction.
- move => ->. simplify_eq/=. by rewrite Z.shiftl_0_l.
move => ?. rewrite bf_cons_singleton_z_iff; last done.
by destruct b.
Qed.
Lemma bf_cons_bool_singleton_true_iff a b :
0 a
bf_cons a 1 (Z_of_bool b) bf_nil 0 b = true.
Proof.
intros. rewrite /not bf_cons_bool_singleton_false_iff //.
destruct b; naive_solver.
move => ?. rewrite bf_cons_singleton_nz_iff; last done.
by destruct b.
Qed.
Lemma bf_mask_cons_singleton a k :
......@@ -267,40 +278,62 @@ Qed.
(* rewrite & simpl rules *)
Create HintDb bitfield_rewrite discriminated.
Hint Rewrite bf_land_nil : bitfield_rewrite.
Hint Rewrite bf_land_mask_cons using can_solve_tac : bitfield_rewrite.
Hint Rewrite bf_land_mask_flip using can_solve_tac : bitfield_rewrite.
Hint Rewrite bf_lor_nil_l : bitfield_rewrite.
Hint Rewrite bf_lor_nil_r : bitfield_rewrite.
Hint Rewrite bf_lor_update using lia : bitfield_rewrite.
Hint Rewrite bf_lor_update_ne using lia : bitfield_rewrite.
Hint Rewrite bf_lor_mask_cons_l using lia : bitfield_rewrite.
Hint Rewrite bf_lor_mask_cons_ne_l using lia : bitfield_rewrite.
Hint Rewrite bf_lor_mask_cons_r using lia : bitfield_rewrite.
Hint Rewrite bf_lor_mask_cons_ne_r using lia : bitfield_rewrite.
Hint Rewrite bf_lor_mask_cons using lia : bitfield_rewrite.
Hint Rewrite bf_slice_nil : bitfield_rewrite.
Hint Rewrite bf_slice_cons using can_solve_tac : bitfield_rewrite.
Hint Rewrite bf_slice_cons_ne using lia : bitfield_rewrite.
Hint Rewrite bf_update_nil : bitfield_rewrite.
Hint Rewrite bf_update_cons using can_solve_tac : bitfield_rewrite.
Hint Rewrite bf_update_cons_ne using lia : bitfield_rewrite.
Definition normalize_bitfield (bv norm : Z) : Prop := bv = norm.
#[export] Hint Rewrite bf_land_nil : bitfield_rewrite.
#[export] Hint Rewrite bf_land_mask_cons using can_solve_tac : bitfield_rewrite.
#[export] Hint Rewrite bf_land_mask_flip using can_solve_tac : bitfield_rewrite.
#[export] Hint Rewrite bf_lor_nil_l : bitfield_rewrite.
#[export] Hint Rewrite bf_lor_nil_r : bitfield_rewrite.
#[export] Hint Rewrite bf_lor_update using lia : bitfield_rewrite.
#[export] Hint Rewrite bf_lor_update_ne using lia : bitfield_rewrite.
#[export] Hint Rewrite bf_lor_mask_cons_l using lia : bitfield_rewrite.
#[export] Hint Rewrite bf_lor_mask_cons_ne_l using lia : bitfield_rewrite.
#[export] Hint Rewrite bf_lor_mask_cons_r using lia : bitfield_rewrite.
#[export] Hint Rewrite bf_lor_mask_cons_ne_r using lia : bitfield_rewrite.
#[export] Hint Rewrite bf_lor_mask_cons using lia : bitfield_rewrite.
#[export] Hint Rewrite bf_slice_nil : bitfield_rewrite.
#[export] Hint Rewrite bf_slice_cons using can_solve_tac : bitfield_rewrite.
#[export] Hint Rewrite bf_slice_cons_ne using lia : bitfield_rewrite.
#[export] Hint Rewrite bf_update_nil : bitfield_rewrite.
#[export] Hint Rewrite bf_update_cons using can_solve_tac : bitfield_rewrite.
#[export] Hint Rewrite bf_update_cons_ne using lia : bitfield_rewrite.
(* Tactic to normalize a bitfield *)
Ltac normalize_bitfield :=
autorewrite with bitfield_rewrite; exact: eq_refl.
(* enable using normalize_bitfield with tactic_hint *)
Definition normalize_bitfield {Σ} (bv : Z) (T : Z iProp Σ) : iProp Σ := T bv.
Typeclasses Opaque normalize_bitfield.
Program Definition normalize_bitfield_hint {Σ} bv norm :
bv = norm
TacticHint (normalize_bitfield (Σ:=Σ) bv) := λ H, {|
tactic_hint_P T := T norm;
|}.
Next Obligation. move => ??? -> ?. unfold normalize_bitfield. iIntros "$". Qed.
Global Hint Extern 10 (TacticHint (normalize_bitfield _)) =>
eapply normalize_bitfield_hint; normalize_bitfield : typeclass_instances.
(* enable using normalize_bitfield in function call specifications
where one cannot use tactic_hint *)
(* TODO: figure out how to make the following unnecessary *)
Definition normalize_bitfield_eq (bv norm : Z) : Prop := bv = norm.
Typeclasses Opaque normalize_bitfield_eq.
Class NormalizeBitfield (bv norm : Z) : Prop :=
normalize_bitfield_proof : bv = norm.
Global Instance simpl_and_normalize_bitfield bv norm `{!NormalizeBitfield bv norm'} `{!IsProtected norm} :
SimplAnd (normalize_bitfield bv norm) (λ T, norm' = norm T).
SimplAnd (normalize_bitfield_eq bv norm) (λ T, norm' = norm T).
Proof. erewrite normalize_bitfield_proof. done. Qed.
Global Hint Extern 10 (NormalizeBitfield _ _) =>
autorewrite with bitfield_rewrite; exact: eq_refl : typeclass_instances.
normalize_bitfield : typeclass_instances.
(* Side cond: ∀ i ∈ I, Z.testbit bv i = false. *)
Global Instance bf_range_empty_nil_inst a k :
......@@ -321,6 +354,37 @@ Proof.
split; naive_solver.
Qed.
(* Simplify singleton data list =/≠ 0 *)
Global Instance bf_cons_singleton_z a k x `{!CanSolve (0 a)} :
SimplBothRel (=) 0 (bf_cons a k x bf_nil) (x = 0).
Proof.
have := (bf_cons_singleton_z_iff a k x).
split; naive_solver.
Qed.
Global Instance bf_cons_singleton_nz_1 a k x `{!CanSolve (0 a)} :
SimplBoth (bf_cons a k x bf_nil 0) (x 0).
Proof.
have := (bf_cons_singleton_nz_iff a k x).
split; naive_solver.
Qed.
Global Instance bf_cons_singleton_nz_2 a k x `{!CanSolve (0 a)} :
SimplBoth (0 bf_cons a k x bf_nil) (x 0).
Proof.
have := (bf_cons_singleton_nz_iff a k x).
split; naive_solver.
Qed.
(* Simplify data list eq *)
Global Instance bf_cons_eq a k x1 l1 x2 l2 :
SimplAndUnsafe true (bf_cons a k x1 l1 = bf_cons a k x2 l2) (λ T, x1 = x2 l1 = l2 T).
Proof.
unfold CanSolve, SimplAndUnsafe in *.
naive_solver.
Qed.
(* Linux macros for bits *)
Lemma Z_shl_bound a k x N :
......
......@@ -17,7 +17,7 @@ Record byte :=
Program Definition byte0 : byte := {| byte_val := 0; |}.
Next Obligation. done. Qed.
Instance byte_eq_dec : EqDecision byte.
#[export] Instance byte_eq_dec : EqDecision byte.
Proof.
move => [b1 H1] [b2 H2]. destruct (decide (b1 = b2)) as [->|].
- left. assert (H1 = H2) as ->; [|done]. apply proof_irrel.
......
......@@ -188,7 +188,7 @@ Qed.
(** An allocation can either be a stack allocation or a heap allocation. *)
Inductive alloc_kind : Set :=
| HeapAlloc
| StackAlloc
| StackAlloc
| GlobalAlloc.
Record allocation :=
......@@ -222,7 +222,7 @@ memory (e.g., does not contain NULL). *)
Definition allocation_in_range (al : allocation) : Prop :=
min_alloc_start al.(al_start) al_end al max_alloc_end.
Instance elem_of_alloc : ElemOf addr allocation :=
Global Instance elem_of_alloc : ElemOf addr allocation :=
λ a al, al.(al_start) a < al_end al.
(** ** Representation of the state of the heap and allocation operations. *)
......
......@@ -672,7 +672,7 @@ Lemma val_stuck e1 σ1 κ e2 σ2 ef :
runtime_step e1 σ1 κ e2 σ2 ef to_val e1 = None.
Proof. destruct 1 => //. revert select (expr_step _ _ _ _ _ _). by destruct 1. Qed.
Instance fill_item_inj Ki : Inj (=) (=) (lang_fill_item Ki).
Global Instance fill_item_inj Ki : Inj (=) (=) (lang_fill_item Ki).
Proof. destruct Ki as [E|E ?]; destruct E; intros ???; simplify_eq/=; auto with f_equal. Qed.
Lemma fill_item_val Ki e :
......@@ -708,15 +708,15 @@ Canonical Structure c_lang := LanguageOfEctx c_ectx_lang.
(** * Useful instances and canonical structures *)
Instance mbyte_inhabited : Inhabited mbyte := populate (MPoison).
Instance val_inhabited : Inhabited val := _.
Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
Instance stmt_inhabited : Inhabited stmt := populate (Goto "a").
Instance function_inhabited : Inhabited function :=
Global Instance mbyte_inhabited : Inhabited mbyte := populate (MPoison).
Global Instance val_inhabited : Inhabited val := _.
Global Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
Global Instance stmt_inhabited : Inhabited stmt := populate (Goto "a").
Global Instance function_inhabited : Inhabited function :=
populate {| f_args := []; f_local_vars := []; f_code := ; f_init := "" |}.
Instance heap_state_inhabited : Inhabited heap_state :=
Global Instance heap_state_inhabited : Inhabited heap_state :=
populate {| hs_heap := inhabitant; hs_allocs := inhabitant; |}.
Instance state_inhabited : Inhabited state :=
Global Instance state_inhabited : Inhabited state :=
populate {| st_heap := inhabitant; st_fntbl := inhabitant; |}.