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
|
Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
Require Import Bedrock.Word.
Require Import Crypto.Tactics.VerdiTactics.
Require Import Crypto.Spec.Encoding.
Require Import Crypto.Spec.ModularWordEncoding.
Local Open Scope F_scope.
Section SignBit.
Context {m : Z} {prime_m : prime m} {two_lt_m : (2 < m)%Z} {sz : nat} {bound_check : (Z.to_nat m < 2 ^ sz)%nat}.
Lemma m_pos : (0 < m)%Z.
Proof.
apply prime_ge_2 in prime_m; omega.
Qed.
Arguments modular_word_encoding {m} {sz} m_pos bound_check.
Let Fm_encoding := modular_word_encoding m_pos bound_check.
Definition sign_bit (x : F m) :=
match (@enc _ _ Fm_encoding x) with
| Word.WO => false
| Word.WS b _ w' => b
end.
Lemma sign_bit_parity : forall x, sign_bit x = Z.odd x.
Proof.
unfold sign_bit; intros.
unfold Fm_encoding, enc, modular_word_encoding, Fm_enc.
pose proof (shatter_word (NToWord sz (Z.to_N x))) as shatter.
case_eq sz; intros; subst; rewrite shatter.
+ pose proof (prime_ge_2 m prime_m).
simpl in bound_check.
assert (m < 1)%Z by (apply Z2Nat.inj_lt; try omega; assumption).
omega.
+ pose proof (FieldToZ_range x m_pos).
destruct (FieldToZ x); auto.
- destruct p; auto.
- pose proof (Pos2Z.neg_is_neg p); omega.
Qed.
Lemma sign_bit_zero : sign_bit 0 = false.
Proof.
rewrite sign_bit_parity; auto.
Qed.
(* TODO : move to ZUtil *)
Lemma Z_odd_mod : forall a b, (b <> 0)%Z ->
Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a.
Proof.
intros.
rewrite Zmod_eq_full by assumption.
rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul.
break_if; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r.
Qed.
(* TODO : move to ModularArithmeticTheorems *)
Lemma F_FieldToZ_add_opp : forall x : F m, x <> 0 -> (FieldToZ x + FieldToZ (opp x) = m)%Z.
Proof.
intros.
rewrite FieldToZ_opp.
rewrite Z_mod_nz_opp_full, mod_FieldToZ; try omega.
rewrite mod_FieldToZ.
replace 0%Z with (@FieldToZ m 0) by auto.
intro false_eq.
rewrite <-F_eq in false_eq.
congruence.
Qed.
Lemma sign_bit_opp : forall (x : F m), x <> 0 -> negb (sign_bit x) = sign_bit (opp x).
Proof.
intros.
pose proof sign_bit_zero as sign_zero.
rewrite !sign_bit_parity in *.
pose proof (F_opp_spec x) as opp_spec_x.
apply F_eq in opp_spec_x.
rewrite FieldToZ_add in opp_spec_x.
rewrite <-opp_spec_x, Z_odd_mod in sign_zero by omega.
replace (Z.odd m) with true in sign_zero by (destruct (ZUtil.prime_odd_or_2 m prime_m); auto || omega).
rewrite Z.odd_add, F_FieldToZ_add_opp, Z.div_same, Bool.xorb_true_r in sign_zero by assumption || omega.
apply Bool.xorb_eq.
rewrite <-Bool.negb_xorb_l.
assumption.
Qed.
End SignBit.
|
