bitfield.v 8.94 KB
Newer Older
Paul's avatar
Paul committed
1
From refinedc.lang Require Import base int_type.
Paul's avatar
Paul committed
2
From refinedc.lithium Require Import simpl_classes Z_bitblast tactics_extend infrastructure interpreter.
Paul's avatar
Paul committed
3
From refinedc.mask_core Require Export calculus semantics normalize typecheck provability int_mask.
Paul's avatar
Paul committed
4
From stdpp Require Import vector.
Fengmin Zhu's avatar
Fengmin Zhu committed
5

Michael Sammler's avatar
Michael Sammler committed
6
Local Open Scope Z_scope.
Paul's avatar
Paul committed
7
Local Open Scope bf_scope.
Fengmin Zhu's avatar
Fengmin Zhu committed
8

Paul's avatar
Paul committed
9
10
(* eval *)

Paul's avatar
Paul committed
11
12
Definition bf_to_Z (t : tm) (it : int_type) : Z :=
  eval (bits_per_int it) t.
Fengmin Zhu's avatar
Fengmin Zhu committed
13

Paul's avatar
Paul committed
14
15
Lemma bf_to_Z_bf_val x it :
  bf_to_Z (bf_val x) it = x.
Paul's avatar
Paul committed
16
Proof. unfold bf_to_Z. done. Qed.
Fengmin Zhu's avatar
Fengmin Zhu committed
17

Paul's avatar
Paul committed
18
19
20
Lemma bf_to_Z_it_extend it1 it2 σ t :
  sig_within_bits σ (bits_per_int it1) 
  sig_within_bits σ (bits_per_int it2) 
Paul's avatar
Paul committed
21
  value t 
Paul's avatar
Paul committed
22
23
   t : bv σ 
  bf_to_Z t it1 = bf_to_Z t it2.
Fengmin Zhu's avatar
Fengmin Zhu committed
24
Proof.
Paul's avatar
Paul committed
25
  intros. unfold bf_to_Z. erewrite eval_extend; eauto.
Paul's avatar
Paul committed
26
Qed.
Fengmin Zhu's avatar
Fengmin Zhu committed
27

Paul's avatar
Paul committed
28
29
Lemma bf_to_Z_in_range t σ it :
  it_signed it = false 
Paul's avatar
Paul committed
30
  value t 
Paul's avatar
Paul committed
31
32
  has_sort t (bv σ) 
  sig_within_bits σ (bits_per_int it) 
Paul's avatar
Paul committed
33
  bf_to_Z t it  it.
Fengmin Zhu's avatar
Fengmin Zhu committed
34
Proof.
Paul's avatar
Paul committed
35
  intros Hs. rewrite /bf_to_Z /elem_of /int_elem_of_it => ? ? ?.
Paul's avatar
Paul committed
36
37
38
39
40
  have -> : min_int it = 0.
  { rewrite /min_int Hs //. }
  have -> : max_int it = 2 ^ (bits_per_int it) - 1.
  { rewrite /max_int Hs //. }
  suff : 0  eval (bits_per_int it) t < 2 ^ (bits_per_int it) by lia.
Paul's avatar
Paul committed
41
42
43
  eapply eval_bounded; eauto.
  have := bits_per_int_gt_0; lia.
Qed.
Fengmin Zhu's avatar
Fengmin Zhu committed
44

Paul's avatar
Paul committed
45
46
Lemma bf_to_Z_nonneg t σ it :
  it_signed it = false 
Paul's avatar
Paul committed
47
  value t 
Paul's avatar
Paul committed
48
49
  has_sort t (bv σ) 
  sig_within_bits σ (bits_per_int it) 
Paul's avatar
Paul committed
50
  0  bf_to_Z t it.
Fengmin Zhu's avatar
Fengmin Zhu committed
51
Proof.
Paul's avatar
Paul committed
52
  intros Hs ???. have : bf_to_Z t it  it by eapply bf_to_Z_in_range.
Paul's avatar
Paul committed
53
  rewrite /bf_to_Z /elem_of /int_elem_of_it /min_int Hs. lia.
Fengmin Zhu's avatar
Fengmin Zhu committed
54
55
Qed.

Paul's avatar
Paul committed
56
#[export] Hint Rewrite bf_to_Z_bf_val : lithium_rewrite.
Fengmin Zhu's avatar
Fengmin Zhu committed
57

Paul's avatar
Paul committed
58
59
(* BitfieldDesc *)

Paul's avatar
Paul committed
60
61
Class BitfieldDesc (R : Type) : Type := {
  bitfield_it : int_type;
62
  bitfield_args : Type;
63
  bitfield_constraints : bitfield_args  R  Prop;
Paul's avatar
Paul committed
64
65
  bitfield_wf : R  Prop;
  bitfield_repr : R  tm;
Paul's avatar
Paul committed
66
67
  bitfield_sig : bitfield_args  signature;
  bitfield_sig_wf :  x, SigWf (bitfield_sig x);
Paul's avatar
Paul committed
68
}.
Fengmin Zhu's avatar
Fengmin Zhu committed
69

Paul's avatar
Paul committed
70
71
72
Arguments bitfield_constraints _/.
Arguments bitfield_repr _/.

Paul's avatar
Paul committed
73
74
(* Global Hint Extern 10 (SigWf _) => *)
  (* solve_sig_wf : typeclass_instances. *)
Paul's avatar
Paul committed
75

Paul's avatar
Paul committed
76
(* Global Instance simpl_SigWf σ `{!SigWf σ} :
Paul's avatar
Paul committed
77
  SimplAnd (SigWf σ) (λ T, T).
Paul's avatar
Paul committed
78
Proof. split; naive_solver. Qed. *)
Paul's avatar
Paul committed
79

80
Definition sum_elim {A B T : Type} (x : A + B) (fl : A  T) (fr : B  T) :=
Paul's avatar
Paul committed
81
  match x with
82
83
  | inl a => fl a
  | inr b => fr b
Paul's avatar
Paul committed
84
85
  end.

Paul's avatar
Paul committed
86
(* normalize *)
Paul's avatar
Paul committed
87

Paul's avatar
Paul committed
88
89
90
Lemma normalize_and_preserves_bf_to_Z σ it t1 t2 :
  value t1 
  value t2 
Paul's avatar
Paul committed
91
92
   t1 : bv σ 
   t2 : mv σ 
Paul's avatar
Paul committed
93
  sig_within_bits σ (bits_per_int it) 
Paul's avatar
Paul committed
94
  bf_to_Z (normalize_and t1 t2) it = bf_to_Z (bf_and t1 t2) it.
Paul's avatar
Paul committed
95
Proof.
Paul's avatar
Paul committed
96
97
  intros. eapply normalize_and_eval; eauto.
  have := bits_per_int_gt_0; lia.
Paul's avatar
Paul committed
98
Qed.
Paul's avatar
Paul committed
99

Paul's avatar
Paul committed
100
Lemma normalize_and_neg_preserves_bf_to_Z σ it t1 t2 :
Paul's avatar
Paul committed
101
102
  value t1 
  value t2 
Paul's avatar
Paul committed
103
104
   t1 : bv σ 
   t2 : mv σ 
Paul's avatar
Paul committed
105
  sig_within_bits σ (bits_per_int it) 
Paul's avatar
Paul committed
106
  bf_to_Z (normalize_and_neg σ t2 t1) it = bf_to_Z (bf_and_neg t1 t2) it.
Paul's avatar
Paul committed
107
Proof.
Paul's avatar
Paul committed
108
109
110
  intros. eapply normalize_and_neg_eval; eauto.
  have := bits_per_int_gt_0; lia.
Qed.
Paul's avatar
Paul committed
111

Paul's avatar
Paul committed
112
113
114
Lemma normalize_or_preserves_bf_to_Z σ it t1 t2 :
  value t1 
  value t2 
Paul's avatar
Paul committed
115
116
117
   t1 : bv σ 
   t2 : bv σ 
  is_mask t2  t1 ## t2 
Paul's avatar
Paul committed
118
  sig_within_bits σ (bits_per_int it) 
Paul's avatar
Paul committed
119
  bf_to_Z (normalize_or t1 t2) it = bf_to_Z (bf_or t1 t2) it.
Fengmin Zhu's avatar
Fengmin Zhu committed
120
Proof.
Paul's avatar
Paul committed
121
122
  intros. eapply normalize_or_eval; eauto.
  have := bits_per_int_gt_0; lia.
Fengmin Zhu's avatar
Fengmin Zhu committed
123
124
Qed.

Paul's avatar
Paul committed
125
(* checkers *)
Fengmin Zhu's avatar
Fengmin Zhu committed
126

Paul's avatar
Paul committed
127
128
Definition ensure_mask (t : tm) : option () :=
  if check_is_mask t then Some () else None.
Fengmin Zhu's avatar
Fengmin Zhu committed
129

Paul's avatar
Paul committed
130
Lemma ensure_mask_spec t :
Paul's avatar
Paul committed
131
  is_Some (ensure_mask t)  is_mask t.
Fengmin Zhu's avatar
Fengmin Zhu committed
132
Proof.
Paul's avatar
Paul committed
133
134
135
  unfold ensure_mask => ?.
  have ? := is_Some_None. case_match; last naive_solver.
  by apply check_is_mask_spec.
Fengmin Zhu's avatar
Fengmin Zhu committed
136
137
Qed.

Paul's avatar
Paul committed
138
139
Definition ensure_or_cond (t1 t2 : tm) : Prop :=
  check_is_mask t2 || check_disjoint t1 t2 = true.
Fengmin Zhu's avatar
Fengmin Zhu committed
140

Paul's avatar
Paul committed
141
Arguments ensure_or_cond _/.
Fengmin Zhu's avatar
Fengmin Zhu committed
142

Paul's avatar
Paul committed
143
144
Lemma ensure_or_cond_spec t1 t2 :
  ensure_or_cond t1 t2  is_mask t2  t1 ## t2.
Paul's avatar
Paul committed
145
Proof.
Paul's avatar
Paul committed
146
  rewrite /ensure_or_cond orb_true_iff => Heqb. destruct Heqb.
Paul's avatar
Paul committed
147
148
  - left. by apply check_is_mask_spec.
  - right. by apply check_disjoint_spec.
Fengmin Zhu's avatar
Fengmin Zhu committed
149
150
Qed.

Paul's avatar
Paul committed
151
152
Definition ensure_bv (σ : signature) (t : tm) : option Prop :=
  check_bv t σ.
Fengmin Zhu's avatar
Fengmin Zhu committed
153

Paul's avatar
Paul committed
154
155
Lemma ensure_bv_spec σ `{!SigWf σ} t P :
  ensure_bv σ t = Some P 
Paul's avatar
Paul committed
156
  P 
Paul's avatar
Paul committed
157
158
159
160
161
162
   t : bv σ.
Proof. by apply check_bv_spec. Qed.

Global Instance has_sort_check_bv t σ `{!SigWf σ}
  `{H : CanSolve ( P, check_bv t σ = Some P  P)} :
  SimplAnd ( t : bv σ) (λ T, T) | 100.
Paul's avatar
Paul committed
163
Proof.
Paul's avatar
Paul committed
164
165
166
167
  unfold CanSolve in H. destruct H as [P [? ?]].
  have ? :  t : bv σ by eapply check_bv_spec; eauto.
  split; naive_solver.
Qed.
Paul's avatar
Paul committed
168

Paul's avatar
Paul committed
169
170
171
172
173
174
175
176
Global Instance simpl_and_is_value t `{!IsValue t} :
  SimplAnd (IsValue t) (λ T, T).
Proof. split; naive_solver. Qed.

Global Instance simpl_and_has_sort t `{!HasSort t σ} :
  SimplAnd (HasSort t σ) (λ T, T).
Proof. split; naive_solver. Qed.

Paul's avatar
Paul committed
177
178
179
(* sem eq *)

Global Instance simpl_sem_eq_sum_elim_refl N {A B} (x p : A + B) `{!IsProtected p} tA tB :
Paul's avatar
Paul committed
180
181
182
183
  SimplAndUnsafe true (SemEq N (sum_elim x tA tB) (sum_elim p tA tB)) (λ T, p = x  T).
Proof.
  move => T [-> ?]. by split.
Qed.
Paul's avatar
Paul committed
184
185

Global Instance simpl_sem_eq_sum_elim_inl N {A B} (p : A + B) `{!IsProtected p} tA tB a :
Paul's avatar
Paul committed
186
187
188
189
  SimplAndUnsafe true (SemEq N (tA a) (sum_elim p tA tB)) (λ T, p = inl a  T).
Proof.
  move => T [-> ?]. by split.
Qed.
Paul's avatar
Paul committed
190
191

Global Instance simpl_sem_eq_sum_elim_inr N {A B} (p : A + B) `{!IsProtected p} tA tB b :
Paul's avatar
Paul committed
192
193
194
195
  SimplAndUnsafe true (SemEq N (tB b) (sum_elim p tA tB)) (λ T, p = inr b  T).
Proof.
  move => T [-> ?]. by split.
Qed.
Fengmin Zhu's avatar
Fengmin Zhu committed
196

Paul's avatar
Paul committed
197
Definition ensure_eq (t1 t2 : tm) (it : int_type) : Prop :=
Paul's avatar
Paul committed
198
  cmp (bits_per_int it) t1 t2.
Fengmin Zhu's avatar
Fengmin Zhu committed
199

Paul's avatar
Paul committed
200
Arguments ensure_eq _/.
Fengmin Zhu's avatar
Fengmin Zhu committed
201

Paul's avatar
Paul committed
202
Lemma ensure_eq_spec it σ t1 t2 :
Paul's avatar
Paul committed
203
204
   t1 : bv σ 
   t2 : bv σ 
Paul's avatar
Paul committed
205
206
  value t1 
  value t2 
Paul's avatar
Paul committed
207
  sig_within_bits σ (bits_per_int it) 
Paul's avatar
Paul committed
208
  ensure_eq t1 t2 it  bf_to_Z t1 it = bf_to_Z t2 it.
Fengmin Zhu's avatar
Fengmin Zhu committed
209
Proof.
Paul's avatar
Paul committed
210
211
  intros. unfold ensure_eq. rewrite cmp_spec; eauto.
  have := bits_per_int_gt_0; lia.
Fengmin Zhu's avatar
Fengmin Zhu committed
212
213
Qed.

Paul's avatar
Paul committed
214
(* sem eq boolean version *)
Paul's avatar
Paul committed
215

Paul's avatar
Paul committed
216
Definition bf_zb (v : tm) (it : int_type) : bool := cmp_zb v.
Paul's avatar
Paul committed
217
218
219
220
221
222
223
224
225
226
227
228

Arguments bf_zb _/.

Lemma bool_decide_eqb P `{Decision P} b :
  bool_decide P = b  (P  b = true).
Proof.
  destruct b.
  - rewrite bool_decide_eq_true. naive_solver.
  - rewrite bool_decide_eq_false. naive_solver.
Qed.

Lemma bf_zb_spec it σ t :
Paul's avatar
Paul committed
229
230
   t : bv σ 
  value t 
Paul's avatar
Paul committed
231
  sig_within_bits σ (bits_per_int it) 
Paul's avatar
Paul committed
232
233
  bf_zb t it = bool_decide (0 = bf_to_Z t it).
Proof.
Paul's avatar
Paul committed
234
235
236
237
  intros. simpl.
  symmetry. rewrite /bf_to_Z bool_decide_eqb cmp_zb_spec cmp_zero_spec; eauto; [lia|].
  have := bits_per_int_gt_0; lia.
Qed.
Paul's avatar
Paul committed
238

Paul's avatar
Paul committed
239
Definition bf_eqb (v1 v2 : tm) (it : int_type) : bool := cmp_eqb (bits_per_int it) v1 v2.
Paul's avatar
Paul committed
240
241
242
243

Arguments bf_eqb _/.

Lemma bf_eqb_spec it σ t1 t2 :
Paul's avatar
Paul committed
244
245
246
247
   t1 : bv σ 
   t2 : bv σ 
  value t1 
  value t2 
Paul's avatar
Paul committed
248
  sig_within_bits σ (bits_per_int it) 
Paul's avatar
Paul committed
249
  bf_eqb t1 t2 it = bool_decide (bf_to_Z t1 it = bf_to_Z t2 it).
Fengmin Zhu's avatar
Fengmin Zhu committed
250
Proof.
Paul's avatar
Paul committed
251
  intros. simpl.
Paul's avatar
Paul committed
252
  symmetry. rewrite /bf_to_Z bool_decide_eqb cmp_eqb_spec cmp_enforce_spec; eauto.
Paul's avatar
Paul committed
253
254
  have := bits_per_int_gt_0; lia.
Qed.
Paul's avatar
Paul committed
255

Paul's avatar
Paul committed
256
(* int -> term *)
Paul's avatar
Paul committed
257
258
259
260
Class IntToTerm (n : Z) (it : int_type) (σ : signature) (t : tm) := {
  int_to_term_sort : SigWf σ  has_sort t (bv σ);
  int_to_term_value : value t;
  int_to_term_sem : bf_to_Z t it = n;
Paul's avatar
Paul committed
261
}.
Paul's avatar
Paul committed
262
Global Hint Mode IntToTerm + + + - : typeclass_instances.
Paul's avatar
Paul committed
263

Paul's avatar
Paul committed
264
265
Lemma convert_int_to_term n it σ t :
  int_to_tm n σ = Some t  IntToTerm n it σ t.
Fengmin Zhu's avatar
Fengmin Zhu committed
266
Proof.
Paul's avatar
Paul committed
267
268
269
270
  intros Ht. constructor.
  - intros. eapply int_to_tm_sort; eauto.
  - eapply int_to_tm_value; eauto.
  - eapply int_to_tm_eval in Ht; eauto.
Fengmin Zhu's avatar
Fengmin Zhu committed
271
Qed.
Paul's avatar
Paul committed
272
273
Global Hint Extern 10 (IntToTerm _ _ _ _) =>
  eapply convert_int_to_term; eauto : typeclass_instances.
Fengmin Zhu's avatar
Fengmin Zhu committed
274

Paul's avatar
Paul committed
275
276
277
278
Class IntToNegTerm (n : Z) (it : int_type) (σ : signature) (t : tm) := {
  int_to_neg_term_sort : SigWf σ  has_sort t (bv σ);
  int_to_neg_term_value : value t;
  int_to_neg_term_sem : Z_lunot (bits_per_int it) (bf_to_Z t it) = n;
Paul's avatar
Paul committed
279
}.
Paul's avatar
Paul committed
280
281
282
283
284
285
Global Hint Mode IntToNegTerm + + + - : typeclass_instances.
Global Program Instance int_to_neg_term_inst n it σ t `{!IntToTerm n it σ t} :
  IntToNegTerm (Z_lunot (bits_per_int it) n) it σ t.
Next Obligation. intros. destruct IntToTerm0. eauto. Qed.
Next Obligation. intros. destruct IntToTerm0. eauto. Qed.
Next Obligation. intros. destruct IntToTerm0. f_equal. eauto. Qed.
Fengmin Zhu's avatar
Fengmin Zhu committed
286

Paul's avatar
Paul committed
287
288
(** * Helper Lemmas *)
(* simpl `_ ≤ max_int uN` to `_ < 2^N` *)
Fengmin Zhu's avatar
Fengmin Zhu committed
289

Paul's avatar
Paul committed
290
291
292
Lemma max_int_unsigned_le_lt x (it : int_type) :
  it_signed it = false 
  x  max_int it  x < 2 ^ (bits_per_int it).
Fengmin Zhu's avatar
Fengmin Zhu committed
293
Proof.
Paul's avatar
Paul committed
294
295
  unfold max_int, int_modulus.
  case_match => ? //. lia.
Fengmin Zhu's avatar
Fengmin Zhu committed
296
297
Qed.

Paul's avatar
Paul committed
298
299
Global Instance max_int_u8_le_lt x :
  SimplBoth (x  max_int u8) (x < 2^8).
Fengmin Zhu's avatar
Fengmin Zhu committed
300
Proof.
Paul's avatar
Paul committed
301
  unfold SimplBoth. by apply max_int_unsigned_le_lt.
Fengmin Zhu's avatar
Fengmin Zhu committed
302
Qed.
Paul's avatar
Paul committed
303
304
Global Instance max_int_u16_le_lt x :
  SimplBoth (x  max_int u16) (x < 2^16).
Fengmin Zhu's avatar
Fengmin Zhu committed
305
Proof.
Paul's avatar
Paul committed
306
  unfold SimplBoth. by apply max_int_unsigned_le_lt.
Fengmin Zhu's avatar
Fengmin Zhu committed
307
Qed.
Paul's avatar
Paul committed
308
309
Global Instance max_int_u32_le_lt x :
  SimplBoth (x  max_int u32) (x < 2^32).
Fengmin Zhu's avatar
Fengmin Zhu committed
310
Proof.
Paul's avatar
Paul committed
311
  unfold SimplBoth. by apply max_int_unsigned_le_lt.
Fengmin Zhu's avatar
Fengmin Zhu committed
312
Qed.
Paul's avatar
Paul committed
313
314
Global Instance max_int_u64_le_lt x :
  SimplBoth (x  max_int u64) (x < 2^64).
Fengmin Zhu's avatar
Fengmin Zhu committed
315
Proof.
Paul's avatar
Paul committed
316
  unfold SimplBoth. by apply max_int_unsigned_le_lt.
Fengmin Zhu's avatar
Fengmin Zhu committed
317
Qed.