Commit a22bdb00 authored by Paul's avatar Paul
Browse files

solve_sig_wf tactic

parent 36ed1a5c
Pipeline #60279 passed with stage
in 30 minutes and 48 seconds
......@@ -894,7 +894,7 @@ let pp_spec : Coq_path.t -> import list -> bitfields_spec list ->
pp " bitfield_wf := %s_wf;@;" n;
pp " bitfield_sig := λ _, %s_sig;@;" n;
pp "|}.@;";
pp "Next Obligation. Admitted.\n@;";
pp "Next Obligation. destruct 1; solve_sig_wf. Qed.\n@;";
let pp_inst_body q =
pp " %s %a, P {|@;" q (pp_sep " " pp_print_string) (List.map fst fs);
......
......@@ -33,9 +33,11 @@ Definition Pte_S1_attr_lo_wf (r : Pte_S1_attr_lo) : Prop :=
Definition Pte_S1_attr_lo_sig :=
sig_atom (range_of 2 3) $
sig_atom (range_of 5 1) $ (* undef *)
sig_atom (range_of 6 2) $
sig_atom (range_of 8 2) $
sig_atom (range_of 10 1) $
sig_atom (range_of 11 1) $ (* undef *)
sig_end.
Global Instance Pte_S1_attr_lo_sig_wf : SigWf Pte_S1_attr_lo_sig.
Proof. solve_sig_wf. Qed.
......@@ -65,7 +67,10 @@ Definition Pte_S1_attr_hi_wf (r : Pte_S1_attr_hi) : Prop :=
True.
Definition Pte_S1_attr_hi_sig :=
sig_atom (range_of 54 1) sig_end.
sig_atom (range_of 51 3) $ (* undef *)
sig_atom (range_of 54 1) $
sig_atom (range_of 55 9) $ (* undef *)
sig_end.
Global Instance Pte_S1_attr_hi_sig_wf : SigWf Pte_S1_attr_hi_sig.
Proof. solve_sig_wf. Qed.
......@@ -113,10 +118,12 @@ Definition Pte_S2_attr_lo_wf (r : Pte_S2_attr_lo) : Prop :=
Definition Pte_S2_attr_lo_sig :=
sig_atom (range_of 2 3) $
sig_atom (range_of 5 1) $ (* undef *)
sig_atom (range_of 6 1) $
sig_atom (range_of 7 1) $
sig_atom (range_of 8 2) $
sig_atom (range_of 10 1) $
sig_atom (range_of 11 1) $ (* undef *)
sig_end.
Global Instance Pte_S2_attr_lo_sig_wf : SigWf Pte_S2_attr_lo_sig.
Proof. solve_sig_wf. Qed.
......@@ -145,8 +152,11 @@ Definition Pte_S2_attr_hi_wf (r : Pte_S2_attr_hi) : Prop :=
0 bool_to_Z $ attr_hi_s2_xn r < 2^1
True.
Definition Pte_S2_attr_hi_sig :=
sig_atom (range_of 54 1) sig_end.
Definition Pte_S2_attr_hi_sig :=
sig_atom (range_of 51 3) $ (* undef *)
sig_atom (range_of 54 1) $
sig_atom (range_of 55 9) $ (* undef *)
sig_end.
Global Instance Pte_S2_attr_hi_sig_wf : SigWf Pte_S2_attr_hi_sig.
Proof. solve_sig_wf. Qed.
......@@ -228,7 +238,7 @@ Definition Pte_sig (s : stage) :=
sig_end.
Global Instance Pte_sig_wf s : SigWf (Pte_sig s).
Admitted.
Proof. destruct s; solve_sig_wf. Qed.
Definition Pte_constraints (s : stage) (r : Pte) :=
match s with
......@@ -359,7 +369,7 @@ Global Program Instance Prot_BitfieldDesc : BitfieldDesc Prot := {|
sig_atom (range_of 3 1) $
sig_end
|}.
Next Obligation. Admitted.
Next Obligation. destruct 1; solve_sig_wf. 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 |}).
......
......@@ -146,36 +146,24 @@ Inductive sig_matches : signature → range → Prop :=
| sig_matches_nested_singleton r σr :
sig_matches σr r
sig_matches (sig_nested r σr sig_end) r
| sig_matches_atom (a k' k : nat) σ :
0 < k' < k
sig_matches σ (range_of (a + k') (k - k'))
sig_matches (sig_atom (range_of a k') σ) (range_of a k)
| sig_matches_nested (a k' k : nat) σr σ :
0 < k' < k
sig_matches σ (range_of (a + k') (k - k'))
sig_matches σr (range_of a k')
sig_matches (sig_nested (range_of a k') σr σ) (range_of a k)
| sig_matches_atom (r r' : range) σ :
offset r = offset r'
width r < width r'
sig_matches σ (range_of (offset r + width r) (width r' - width r))
sig_matches (sig_atom r σ) r'
| sig_matches_nested (r r' : range) σr σ :
offset r = offset r'
width r < width r'
sig_matches σ (range_of (offset r + width r) (width r' - width r))
sig_matches σr r
sig_matches (sig_nested r σr σ) r'
.
Fixpoint check_sig_matches σ (a k : nat) : bool :=
match σ with
| sig_end => (k =? 0)%nat
| sig_atom r σ' =>
if (offset r =? a)%nat && (width r <? k)%nat
then check_sig_matches σ' (a + width r) (k - width r)
else false
| sig_nested r σr σ' =>
if (offset r =? a)%nat && (width r <? k)%nat
then check_sig_matches σr (offset r) (width r) &&
check_sig_matches σ' (a + width r) (k - width r)
else false
Ltac solve_sig_matches :=
repeat match goal with
| |- sig_matches _ _ => constructor; try done
end.
(* Lemma check_sig_matches_spec σ (r : range) :
check_sig_matches σ (offset r) (width r) = true →
sig_matches σ r.
*)
Inductive sig_wf : signature Prop :=
| sig_wf_end : sig_wf sig_end
| sig_wf_atom r σ :
......@@ -215,19 +203,25 @@ Proof.
induction 1.
- repeat constructor.
- constructor => //. all: constructor.
- constructor => //. apply Forall_HdRel, Forall_forall => r Hr.
eapply Forall_forall in Hr; last by apply sig_covered_by_Forall, sig_matches_impl_covered_by; eauto.
unfold subseteq, range_subseteq in Hr. unfold range_lt. simpl in *. lia.
- constructor => //. apply Forall_HdRel, Forall_forall => r Hr.
eapply Forall_forall in Hr; last by apply sig_covered_by_Forall, sig_matches_impl_covered_by; eauto.
unfold subseteq, range_subseteq in Hr. unfold range_lt. simpl in *. lia.
- constructor => //. apply Forall_HdRel, Forall_forall => x Hx.
eapply Forall_forall in Hx; last by apply sig_covered_by_Forall, sig_matches_impl_covered_by; eauto.
unfold subseteq, range_subseteq in Hx. unfold range_lt. simpl in *. lia.
- constructor => //. apply Forall_HdRel, Forall_forall => x Hx.
eapply Forall_forall in Hx; last by apply sig_covered_by_Forall, sig_matches_impl_covered_by; eauto.
unfold subseteq, range_subseteq in Hx. unfold range_lt. simpl in *. lia.
Qed.
Ltac solve_sig_wf := repeat constructor; unfold range_lt; simpl; lia.
Class SigWf (σ : signature) : Prop :=
sig_wf_proof : sig_wf σ.
Ltac solve_sig_wf :=
repeat match goal with
| |- HdRel range_lt _ _ => constructor; try done
| |- SigWf _ => constructor
| |- sig_wf _ => constructor
| |- sig_matches _ _ => solve_sig_matches
end.
Global Instance sig_end_wf : SigWf sig_end.
Proof.
constructor => //.
......
......@@ -556,6 +556,14 @@ Proof.
+ apply IHv2 => //. all: repeat constructor => //.
Qed.
Lemma offset_range_of (a k : Z) :
0 a Z.of_nat (offset (range_of a k)) = a.
Proof. simpl. lia. Qed.
Lemma width_range_of (a k : Z) :
0 < k Z.of_nat (width (range_of a k)) = k.
Proof. simpl. lia. Qed.
Lemma mk_full_mask_eval σ N (r : range) :
sig_matches σ r
offset r + width r N
......@@ -566,19 +574,19 @@ Proof.
- invert Hm.
* rewrite rc.bf_slice_singleton; try lia.
by apply Z_ones_bounded.
* eapply rc.bf_slice_mask_cons; simpl; try lia.
specialize (IHσ _ H3). simpl in *.
have -> : Z.to_nat a + S (Z.to_nat (k' - 1)) = Z.to_nat (a + k') by lia.
have -> : S (Z.to_nat (k - 1)) - S (Z.to_nat (k' - 1)) = S (Z.to_nat (k - k' - 1)) by lia.
apply IHσ; lia.
* have -> : offset r' = offset r by done.
eapply rc.bf_slice_mask_cons; simpl; try lia.
specialize (IHσ (range_of (offset r + width r') (width r - width r'))).
rewrite offset_range_of ?width_range_of in IHσ; [lia..|].
apply IHσ; [congruence | lia].
- invert Hm.
* rewrite rc.bf_slice_singleton; try lia.
by apply Z_ones_bounded.
* eapply rc.bf_slice_mask_cons; simpl; try lia.
specialize (IHσ _ H4). simpl in *.
have -> : Z.to_nat a + S (Z.to_nat (k' - 1)) = Z.to_nat (a + k') by lia.
have -> : S (Z.to_nat (k - 1)) - S (Z.to_nat (k' - 1)) = S (Z.to_nat (k - k' - 1)) by lia.
apply IHσ; lia.
* have -> : offset r' = offset r by done.
eapply rc.bf_slice_mask_cons; simpl; try lia.
specialize (IHσ (range_of (offset r + width r') (width r - width r'))).
rewrite offset_range_of ?width_range_of in IHσ; [lia..|].
apply IHσ; [congruence | lia].
Qed.
Lemma normalize_and_neg_eval N v1 v2 σ :
......
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