Commit 49b66356 authored by Paul's avatar Paul
Browse files

disable rewriting rules; add a failure goal

parent ff098768
Pipeline #55570 canceled with stage
in 7 seconds
......@@ -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("{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 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")]]
......
......@@ -287,7 +287,7 @@ Qed.
(* rewrite & simpl rules *)
Create HintDb bitfield_rewrite discriminated.
(* Create HintDb bitfield_rewrite discriminated.
#[export] Hint Rewrite bf_land_nil : bitfield_rewrite.
#[export] Hint Rewrite bf_land_mask_cons using can_solve_tac : bitfield_rewrite.
......@@ -309,8 +309,8 @@ Create HintDb bitfield_rewrite discriminated.
#[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.
#[export] Hint Rewrite bf_update_cons_ne using lia : bitfield_rewrite. *)
(*
Definition normalize_bitfield (bv norm : Z) : Prop := bv = norm.
Typeclasses Opaque normalize_bitfield.
......@@ -319,10 +319,10 @@ Class NormalizeBitfield (bv norm : Z) : Prop :=
Global Instance simpl_and_normalize_bitfield bv norm `{!NormalizeBitfield bv norm'} `{!IsProtected norm} :
SimplAnd (normalize_bitfield bv norm) (λ T, norm' = norm ∧ T).
Proof. erewrite normalize_bitfield_proof. done. Qed.
Proof. erewrite normalize_bitfield_proof. done. Qed. *)
(*
Global Hint Extern 10 (NormalizeBitfield _ _) =>
autorewrite with bitfield_rewrite; exact: eq_refl : typeclass_instances.
autorewrite with bitfield_rewrite; exact: eq_refl : typeclass_instances. *)
(* Side cond: ∀ i ∈ I, Z.testbit bv i = false. *)
Global Instance bf_range_empty_nil_inst a k :
......@@ -457,9 +457,9 @@ Global Opaque bf_nil bf_cons bf_mask_cons bf_slice bf_update.
(* deep-embedded terms *)
Definition range : Type := nat * nat.
Definition range : Type := Z * Z.
Notation "'offset' r" := (fst r) (at level 40).
Notation "'width' r" := (S (snd r)) (at level 40). (* always positive *)
Notation "'width' r" := (snd r) (at level 40).
(* r1 comes before r2, without overlap *)
Definition range_prec : relation range :=
......@@ -563,17 +563,17 @@ Ltac to_deep e :=
| bf_cons ?a ?k ?x ?l =>
let tx := to_deep x in
let t := to_deep l in
constr:(deep.bf_cons (Z.to_nat a, Z.to_nat (k - 1)) tx t)
constr:(deep.bf_cons (a, k) tx t)
| bf_mask_cons ?a ?k ?l =>
let t := to_deep l in
constr:(deep.bf_cons (Z.to_nat a, Z.to_nat (k - 1)) (deep.bf_val (Z.ones k)) t)
constr:(deep.bf_cons (a, k) (deep.bf_val (Z.ones k)) t)
| bf_slice ?a ?k ?l =>
let t := to_deep l in
constr:(deep.bf_slice (Z.to_nat a, Z.to_nat (k - 1)) t)
constr:(deep.bf_slice (a, k) t)
| bf_update ?a ?k ?x ?l =>
let tx := to_deep x in
let t := to_deep l in
constr:(deep.bf_update (Z.to_nat a, Z.to_nat (k - 1)) tx t)
constr:(deep.bf_update (a, k) tx t)
| Z.land ?e1 ?e2 =>
let t1 := to_deep e1 in
let t2 := to_deep e2 in
......@@ -585,23 +585,34 @@ Ltac to_deep e :=
| _ => constr:(deep.bf_val e)
end.
Lemma normalize_preserves_shallow t :
to_shallow (deep.normalize t) = to_shallow t.
Admitted.
Ltac normalize_bf_eq :=
lazymatch goal with
| [ |- context C [?e1 = ?e2] ] =>
| [ |- context C [?e1 = ?norm] ] =>
let t1 := to_deep e1 in
let t2 := to_deep e2 in
let P := context C [to_shallow (deep.normalize t1) = to_shallow (deep.normalize t2)] in
change_no_check P; simpl
end.
Ltac normalize_bf :=
lazymatch goal with
| [ |- context C [normalize_bitfield ?e ?norm] ] =>
let t := to_deep e in
let P := context C [normalize_bitfield (to_shallow (deep.normalize t)) norm] in
change_no_check P; simpl
let P := context C [to_shallow (deep.normalize t1) = norm] in
change P
end.
Goal Z.land (bf_cons 0 1 1 $ bf_cons 3 1 0 $ bf_nil) (bf_mask_cons 3 1 bf_nil) = bf_cons 3 1 0 $ bf_nil.
normalize_bf_eq. reflexivity.
Qed.
normalize_bf_eq. reflexivity.
Qed.
Goal Z.lor
(Z.lor
(bf_cons 0 1 0%nat
(bf_cons 1 1 0
(bf_cons 2 10 0
(bf_cons 12 36 22
(bf_cons 48 3 0 (bf_cons 51 13 0 bf_nil))))))
(bf_cons 1 1 1 bf_nil)) (bf_mask_cons 0 1 bf_nil) =
bf_cons 0 1 1%nat
(bf_cons 1 1 0
(bf_cons 2 10 0
(bf_cons 12 36 22
(bf_cons 48 3 0 (bf_cons 51 13 0 bf_nil))))).
(* normalize_bf_eq. *)
Abort.
......@@ -129,15 +129,15 @@ Section programs.
Lemma type_arithop_bitfield_raw it v1 bv1 v2 bv2 T bv op:
arith_op_result it bv1 bv2 op = Some bv
(bv1 it - bv2 it - arith_op_sidecond it bv1 bv2 bv op norm,
(normalize_bitfield bv norm T (i2v norm it) (t2mt (norm @ bitfield_raw it)))) -
(bv1 it - bv2 it - arith_op_sidecond it bv1 bv2 bv op
T (i2v bv it) (t2mt (bv @ bitfield_raw it))) -
typed_bin_op v1 (v1 ◁ᵥ bv1 @ bitfield_raw it) v2 (v2 ◁ᵥ bv2 @ bitfield_raw it) op (IntOp it) (IntOp it) T.
Proof.
iIntros "%Hop HT Hv1 Hv2".
iApply type_val_expr_mono_strong.
iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
iIntros "Hbv1 Hbv2".
iDestruct ("HT" with "Hbv1 Hbv2") as "[% [%norm [<- ?]]]".
iDestruct ("HT" with "Hbv1 Hbv2") as "[% ?]".
iSplitR => //.
iExists _. by iFrame.
Qed.
......@@ -206,15 +206,14 @@ Section programs.
Lemma type_arithop_bitfield_raw_int it v1 bv v2 n T bv' op:
arith_op_result it bv n op = Some bv'
(bv it - n it - arith_op_sidecond it bv n bv' op norm,
(normalize_bitfield bv' norm T (i2v norm it) (t2mt (norm @ bitfield_raw it)))) -
(bv it - n it - arith_op_sidecond it bv n bv' op T (i2v bv' it) (t2mt (bv' @ bitfield_raw it))) -
typed_bin_op v1 (v1 ◁ᵥ bv @ bitfield_raw it) v2 (v2 ◁ᵥ n @ int it) op (IntOp it) (IntOp it) T.
Proof.
iIntros "%Hop HT Hv1 Hv2".
iApply type_val_expr_mono_strong.
iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
iIntros "Hbv1 Hbv2".
iDestruct ("HT" with "Hbv1 Hbv2") as "[% [%norm [<- ?]]]".
iDestruct ("HT" with "Hbv1 Hbv2") as "[% ?]".
iSplitR => //.
iExists _. by iFrame.
Qed.
......@@ -227,15 +226,14 @@ Section programs.
Lemma type_arithop_int_bitfield_raw it v1 n v2 bv T bv' op:
arith_op_result it n bv op = Some bv'
(n it - bv it - arith_op_sidecond it n bv bv' op norm,
(normalize_bitfield bv' norm T (i2v norm it) (t2mt (norm @ bitfield_raw it)))) -
(n it - bv it - arith_op_sidecond it n bv bv' op T (i2v bv' it) (t2mt (bv' @ bitfield_raw it))) -
typed_bin_op v1 (v1 ◁ᵥ n @ int it) v2 (v2 ◁ᵥ bv @ bitfield_raw it) op (IntOp it) (IntOp it) T.
Proof.
iIntros "%Hop HT Hv1 Hv2".
iApply type_val_expr_mono_strong.
iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
iIntros "Hbv1 Hbv2".
iDestruct ("HT" with "Hbv1 Hbv2") as "[% [%norm [<- ?]]]".
iDestruct ("HT" with "Hbv1 Hbv2") as "[% ?]".
iSplitR => //.
iExists _. by iFrame.
Qed.
......
Markdown is supported
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