1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2022 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
Require Import Bvector.
(* Require Export BigNumPrelude. *)
Require Import Int31 Cyclic31.
Require Export Int63Native.
Require Export Int63Op.
Require Import Psatz.
Local Open Scope Z_scope.
(* Taken from BigNumPrelude *)
Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p.
Proof.
intros p x Hle;destruct (Z_le_gt_dec 0 p).
apply Zdiv_le_lower_bound;auto with zarith.
replace (2^p) with 0.
destruct x;compute;intro;discriminate.
destruct p;trivial;discriminate.
Qed.
Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y.
Proof.
intros p x y H;destruct (Z_le_gt_dec 0 p).
apply Zdiv_lt_upper_bound;auto with zarith.
apply Z.lt_le_trans with y;auto with zarith.
rewrite <- (Z.mul_1_r y);apply Z.mul_le_mono_nonneg;auto with zarith.
assert (0 < 2^p);auto with zarith.
replace (2^p) with 0.
destruct x;change (0<y);auto with zarith.
destruct p;trivial;discriminate.
Qed.
(* Int63Axioms *)
Definition wB := (2^(Z_of_nat size)).
Notation "[| x |]" := (to_Z x) (at level 0, x at level 99) : int63_scope.
Notation "[+| c |]" :=
(interp_carry 1 wB to_Z c) (at level 0, c at level 99) : int63_scope.
Notation "[-| c |]" :=
(interp_carry (-1) wB to_Z c) (at level 0, c at level 99) : int63_scope.
Notation "[|| x ||]" :=
(zn2z_to_Z wB to_Z x) (at level 0, x at level 99) : int63_scope.
Local Open Scope int63_scope.
Local Open Scope Z_scope.
(* Bijection : int63 <-> Bvector size *)
Theorem to_Z_inj : forall x y, [|x|] = [|y|] -> x = y.
Proof Ring31.Int31_canonic.
Theorem of_to_Z : forall x, of_Z ([|x|]) = x.
Proof. exact phi_inv_phi. Qed.
(* Comparisons *)
Theorem eqb_refl x : (x == x)%int = true.
Proof. now rewrite Ring31.eqb31_eq. Qed.
Theorem ltb_spec x y : (x < y)%int = true <-> [|x|] < [|y|].
Proof.
unfold ltb. rewrite spec_compare, <- Z.compare_lt_iff.
change (phi x ?= phi y) with ([|x|] ?= [|y|]).
case ([|x|] ?= [|y|]); intuition; discriminate.
Qed.
Theorem leb_spec x y : (x <= y)%int = true <-> [|x|] <= [|y|].
Proof.
unfold leb. rewrite spec_compare, <- Z.compare_le_iff.
change (phi x ?= phi y) with ([|x|] ?= [|y|]).
case ([|x|] ?= [|y|]); intuition; discriminate.
Qed.
(** Specification of logical operations *)
Lemma lsl_spec_alt p :
forall x, [| addmuldiv31_alt p x 0 |] = ([|x|] * 2^(Z.of_nat p)) mod wB.
Proof.
induction p as [ |p IHp]; simpl; intro x.
- rewrite Z.mul_1_r. symmetry. apply Zmod_small. apply phi_bounded.
- rewrite IHp, phi_twice, Zmult_mod_idemp_l, Z.double_spec,
Z.mul_comm, Z.mul_assoc, Z.mul_comm,
Z.pow_pos_fold, Zpos_P_of_succ_nat, <- Z.add_1_r, Z.pow_add_r.
* reflexivity.
* apply Zle_0_nat.
* exact Z.le_0_1.
Qed.
Theorem lsl_spec x p : [| x << p |] = ([|x|] * 2^[|p|]) mod wB.
Proof.
unfold lsl.
rewrite addmuldiv31_equiv, lsl_spec_alt, Nat2Z.inj_abs_nat, Z.abs_eq.
- reflexivity.
- now destruct (phi_bounded p).
Qed.
Lemma div_greater (p x:int) (H:Z.of_nat Int31.size <= [|p|]) : [|x|] / 2 ^ [|p|] = 0.
Proof.
apply Z.div_small. destruct (phi_bounded x) as [H1 H2]. split; auto.
apply (Z.lt_le_trans _ _ _ H2). apply Z.pow_le_mono_r; auto.
exact Z.lt_0_2.
Qed.
Theorem lsr_spec x p : [|x >> p|] = [|x|] / 2 ^ [|p|].
Proof.
unfold lsr. case_eq (p < 31%int31)%int; intro Heq.
- assert (H : [|31%int31 - p|] = 31 - [|p|]).
* rewrite spec_sub. rewrite Zmod_small; auto.
split.
+ rewrite ltb_spec in Heq. assert (forall x y, x < y -> 0 <= y - x) by (intros;lia); auto.
+ assert (H:forall x y z, 0 <= y /\ x < z -> x - y < z) by (intros;lia).
apply H. destruct (phi_bounded p). destruct (phi_bounded (31%int31)). split; auto.
* rewrite spec_add_mul_div.
+ rewrite Z.add_0_l. change (phi (31%int31 - p)) with [|31%int31 - p|]. rewrite H. replace (31 - (31 - [|p|])) with [|p|] by ring. apply Zmod_small. split.
++ apply div_le_0. now destruct (phi_bounded x).
++ apply div_lt. apply phi_bounded.
+ change (phi (31%int31 - p)) with [|31%int31 - p|]. rewrite H. assert (forall x y, 0 <= y -> x - y <= x) by (intros;lia). apply H0. now destruct (phi_bounded p).
- rewrite div_greater; auto.
destruct (Z.le_gt_cases [|31%int31|] [|p|]); auto.
rewrite <- ltb_spec in H. rewrite H in Heq. discriminate.
Qed.
Lemma bit_testbit x i : bit x i = Z.testbit [|x|] [|i|].
Admitted.
(* Proof. *)
(* case_eq [|i|]. *)
(* - simpl. change 0 with [|0|]. intro Heq. apply Ring31.Int31_canonic in Heq. subst i. *)
(* unfold bit. *)
Lemma Z_pos_xO_pow i x (Hi:0 <= i) : Z.pos x < 2 ^ i <-> Z.pos x~0 < 2 ^ (i+1).
Proof. rewrite Pos2Z.inj_xO, Z.pow_add_r; auto using Z.le_0_1; lia. Qed.
Lemma Z_pos_xI_pow i x (Hi:0 <= i) : Z.pos x < 2 ^ i <-> Z.pos x~1 < 2 ^ (i+1).
Proof. rewrite Pos2Z.inj_xI, Z.pow_add_r; auto using Z.le_0_1; lia. Qed.
Lemma pow_nonneg i (Hi : 1 <= 2 ^ i) : 0 <= i.
Proof.
destruct (Z.le_gt_cases 0 i); auto.
rewrite (Z.pow_neg_r _ _ H) in Hi. lia.
Qed.
Lemma pow_pos i (Hi : 1 < 2 ^ i) : 0 < i.
Proof.
destruct (Z.lt_trichotomy 0 i) as [H|[H|H]]; auto.
- subst i. lia.
- rewrite (Z.pow_neg_r _ _ H) in Hi. lia.
Qed.
Lemma pos_land_bounded : forall x y i,
Z.pos x < 2 ^ i -> Z.pos y < 2 ^ i -> Z.of_N (Pos.land x y) < 2 ^ i.
Proof.
induction x as [x IHx|x IHx| ]; intros [y|y| ] i; auto.
- simpl. intro H.
assert (H4:0 <= i - 1) by (assert (H4:0 < i); try lia; apply pow_pos; apply (Z.le_lt_trans _ (Z.pos x~1)); auto; lia).
generalize H. replace i with ((i-1)+1) at 1 2 by ring. rewrite <- !Z_pos_xI_pow; auto. intros H1 H2.
assert (H3:=IHx _ _ H1 H2).
unfold Pos.Nsucc_double. case_eq (Pos.land x y).
* intros _. eapply Z.le_lt_trans; [ |exact H]. clear. lia.
* intros p Hp. revert H3. rewrite Hp, N2Z.inj_pos, Z_pos_xI_pow; auto.
replace (i - 1 + 1) with i by ring. clear. lia.
- simpl. intro H.
assert (H4:0 <= i - 1) by (assert (H4:0 < i); try lia; apply pow_pos; apply (Z.le_lt_trans _ (Z.pos x~1)); auto; lia).
generalize H. replace i with ((i-1)+1) at 1 2 by ring. rewrite <- Z_pos_xI_pow, <- Z_pos_xO_pow; auto. intros H1 H2.
assert (H3:=IHx _ _ H1 H2).
unfold Pos.Ndouble. case_eq (Pos.land x y).
* intros _. eapply Z.le_lt_trans; [ |exact H]. clear. lia.
* intros p Hp. revert H3. rewrite Hp, N2Z.inj_pos, Z_pos_xO_pow; auto.
replace (i - 1 + 1) with i by ring. clear. lia.
- simpl. intro H.
assert (H4:0 <= i - 1) by (assert (H4:0 < i); try lia; apply pow_pos; apply (Z.le_lt_trans _ (Z.pos x~0)); auto; lia).
generalize H. replace i with ((i-1)+1) at 1 2 by ring. rewrite <- Z_pos_xI_pow, <- Z_pos_xO_pow; auto. intros H1 H2.
assert (H3:=IHx _ _ H1 H2).
unfold Pos.Ndouble. case_eq (Pos.land x y).
* intros _. eapply Z.le_lt_trans; [ |exact H]. clear. lia.
* intros p Hp. revert H3. rewrite Hp, N2Z.inj_pos, Z_pos_xO_pow; auto.
replace (i - 1 + 1) with i by ring. clear. lia.
- simpl. intro H.
assert (H4:0 <= i - 1) by (assert (H4:0 < i); try lia; apply pow_pos; apply (Z.le_lt_trans _ (Z.pos x~0)); auto; lia).
generalize H. replace i with ((i-1)+1) at 1 2 by ring. rewrite <- !Z_pos_xO_pow; auto. intros H1 H2.
assert (H3:=IHx _ _ H1 H2).
unfold Pos.Ndouble. case_eq (Pos.land x y).
* intros _. eapply Z.le_lt_trans; [ |exact H]. clear. lia.
* intros p Hp. revert H3. rewrite Hp, N2Z.inj_pos, Z_pos_xO_pow; auto.
replace (i - 1 + 1) with i by ring. clear. lia.
- simpl. intros H _. apply (Z.le_lt_trans _ (Z.pos x~0)); lia.
- simpl. intros H _. apply (Z.le_lt_trans _ 1); lia.
Qed.
Lemma Z_land_bounded i : forall x y,
0 <= x < 2 ^ i -> 0 <= y < 2 ^ i -> 0 <= Z.land x y < 2 ^ i.
Proof.
intros [ |p|p] [ |q|q]; auto.
- intros [_ H1] [_ H2]. simpl. split.
* apply N2Z.is_nonneg.
* now apply pos_land_bounded.
Admitted.
Theorem land_spec x y i : bit (x land y) i = bit x i && bit y i.
Proof.
rewrite !bit_testbit. change (x land y) with (land31 x y). unfold land31.
rewrite phi_phi_inv. rewrite Zmod_small.
- apply Z.land_spec.
- split.
* rewrite Z.land_nonneg. left. now destruct (phi_bounded x).
* now destruct (Z_land_bounded _ _ _ (phi_bounded x) (phi_bounded y)).
Qed.
Axiom lor_spec: forall x y i, bit (x lor y) i = bit x i || bit y i.
Axiom lxor_spec: forall x y i, bit (x lxor y) i = xorb (bit x i) (bit y i).
(** Specification of basic opetations *)
(* Arithmetic modulo operations *)
(* Remarque : les axiomes seraient plus simple si on utilise of_Z a la place :
exemple : add_spec : forall x y, of_Z (x + y) = of_Z x + of_Z y. *)
Axiom add_spec : forall x y, [|x + y|] = ([|x|] + [|y|]) mod wB.
Axiom sub_spec : forall x y, [|x - y|] = ([|x|] - [|y|]) mod wB.
Axiom mul_spec : forall x y, [| x * y |] = [|x|] * [|y|] mod wB.
Axiom mulc_spec : forall x y, [|x|] * [|y|] = [|fst (mulc x y)|] * wB + [|snd (mulc x y)|].
Axiom div_spec : forall x y, [|x / y|] = [|x|] / [|y|].
Axiom mod_spec : forall x y, [|x \% y|] = [|x|] mod [|y|].
(** Iterators *)
Axiom foldi_cont_gt : forall A B f from to cont,
(to < from)%int = true -> foldi_cont (A:=A) (B:=B) f from to cont = cont.
Axiom foldi_cont_eq : forall A B f from to cont,
from = to -> foldi_cont (A:=A) (B:=B) f from to cont = f from cont.
Axiom foldi_cont_lt : forall A B f from to cont,
(from < to)%int = true->
foldi_cont (A:=A) (B:=B) f from to cont =
f from (fun a' => foldi_cont f (from + 1%int) to cont a').
Axiom foldi_down_cont_lt : forall A B f from downto cont,
(from < downto)%int = true -> foldi_down_cont (A:=A) (B:=B) f from downto cont = cont.
Axiom foldi_down_cont_eq : forall A B f from downto cont,
from = downto -> foldi_down_cont (A:=A) (B:=B) f from downto cont = f from cont.
Axiom foldi_down_cont_gt : forall A B f from downto cont,
(downto < from)%int = true->
foldi_down_cont (A:=A) (B:=B) f from downto cont =
f from (fun a' => foldi_down_cont f (from-1) downto cont a').
(** Print *)
Axiom print_int_spec : forall x, x = print_int x.
(** Axioms on operations which are just short cut *)
Axiom compare_def_spec : forall x y, compare x y = compare_def x y.
Axiom head0_spec : forall x, 0 < [|x|] ->
wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB.
Axiom tail0_spec : forall x, 0 < [|x|] ->
(exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail0 x|]))%Z.
Axiom addc_def_spec : forall x y, (x +c y)%int = addc_def x y.
Axiom addcarryc_def_spec : forall x y, addcarryc x y = addcarryc_def x y.
Axiom subc_def_spec : forall x y, (x -c y)%int = subc_def x y.
Axiom subcarryc_def_spec : forall x y, subcarryc x y = subcarryc_def x y.
Axiom diveucl_def_spec : forall x y, diveucl x y = diveucl_def x y.
Axiom diveucl_21_spec : forall a1 a2 b,
let (q,r) := diveucl_21 a1 a2 b in
([|q|],[|r|]) = Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|].
Axiom addmuldiv_def_spec : forall p x y,
addmuldiv p x y = addmuldiv_def p x y.
(*
Local Variables:
coq-load-path: ((rec "../../.." "SMTCoq"))
End:
*)
|
