forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
word_preludeScriptOld.sml
182 lines (140 loc) · 6.72 KB
/
word_preludeScriptOld.sml
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
open HolKernel Parse boolLib bossLib; val _ = new_theory "word_prelude";
open arithmeticTheory listTheory wordsTheory wordsLib;
open ml_translatorLib ml_translatorTheory std_preludeTheory;
val _ = translation_extends "std_prelude";
(* bit *)
val res = translate bitTheory.MOD_2EXP_def;
val res = translate bitTheory.DIV_2EXP_def;
val res = translate DIV2_def;
val res = translate bitTheory.BITS_THM2;
val res = translate (SIMP_RULE std_ss [bitTheory.BITS_THM,DECIDE ``SUC n - n = 1``] bitTheory.BIT_def);
val res = translate bitTheory.SBIT_def;
(* words *)
val WORD_def = Define `WORD w = NUM (w2n w)`;
val _ = add_type_inv (inst [alpha|->``:32``] ``WORD``) ``:num``
val _ = add_type_inv (inst [alpha|->``:16``] ``WORD``) ``:num``
val _ = add_type_inv (inst [alpha|->``:8``] ``WORD``) ``:num``
val EqualityType_WORD = Q.prove(
`EqualityType WORD`,
EVAL_TAC THEN SRW_TAC [] [] THEN EVAL_TAC)
|> store_eq_thm;
val Eval_w2n_word32 = Q.prove(
`!v. ((NUM --> NUM) (\x.x)) v ==> ((WORD --> NUM) (w2n:word32->num)) v`,
SIMP_TAC std_ss [Arrow_def,AppReturns_def,WORD_def])
|> MATCH_MP (MATCH_MP Eval_WEAKEN (hol2deep ``\x.x:num``))
|> store_eval_thm;
val Eval_w2n_word16 = Q.prove(
`!v. ((NUM --> NUM) (\x.x)) v ==> ((WORD --> NUM) (w2n:word16->num)) v`,
SIMP_TAC std_ss [Arrow_def,AppReturns_def,WORD_def])
|> MATCH_MP (MATCH_MP Eval_WEAKEN (hol2deep ``\x.x:num``))
|> store_eval_thm;
val Eval_w2n_word8 = Q.prove(
`!v. ((NUM --> NUM) (\x.x)) v ==> ((WORD --> NUM) (w2n:word8->num)) v`,
SIMP_TAC std_ss [Arrow_def,AppReturns_def,WORD_def])
|> MATCH_MP (MATCH_MP Eval_WEAKEN (hol2deep ``\x.x:num``))
|> store_eval_thm;
val Eval_n2w_word32 = Q.prove(
`!v. ((NUM --> NUM) (\x.x MOD 4294967296)) v ==> ((NUM --> WORD) (n2w:num->word32)) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,WORD_def,w2n_n2w])
|> MATCH_MP (MATCH_MP Eval_WEAKEN (hol2deep ``\x.x MOD 4294967296``))
|> store_eval_thm;
val Eval_n2w_word16 = Q.prove(
`!v. ((NUM --> NUM) (\x.x MOD 65536)) v ==> ((NUM --> WORD)
(n2w:num->word16)) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,WORD_def,w2n_n2w])
|> MATCH_MP (MATCH_MP Eval_WEAKEN (hol2deep ``\x.x MOD 65536``))
|> store_eval_thm;
val Eval_n2w_word8 = Q.prove(
`!v. ((NUM --> NUM) (\x.x MOD 256)) v ==> ((NUM --> WORD) (n2w:num->word8)) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,WORD_def,w2n_n2w])
|> MATCH_MP (MATCH_MP Eval_WEAKEN (hol2deep ``\x.x MOD 256``))
|> store_eval_thm;
val res = translate (word_add_def |> INST_TYPE [alpha|->``:32``]);
val res = translate (word_mul_def |> INST_TYPE [alpha|->``:32``]);
val res = translate (word_add_def |> INST_TYPE [alpha|->``:16``]);
val res = translate (word_mul_def |> INST_TYPE [alpha|->``:16``]);
val res = translate (word_add_def |> INST_TYPE [alpha|->``:8``]);
val res = translate (word_mul_def |> INST_TYPE [alpha|->``:8``]);
val res = translate (bitTheory.BITWISE_def)
val word_xor_lemma = Q.prove(
`!w v:word32. (w ?? v) = n2w (BITWISE 32 (\x y. x <> y) (w2n w) (w2n v))`,
REPEAT Cases THEN FULL_SIMP_TAC (srw_ss()) [word_xor_n2w]);
val word_xor_lemma8 = Q.prove(
`!w v:word8. (w ?? v) = n2w (BITWISE 8 (\x y. x <> y) (w2n w) (w2n v))`,
REPEAT Cases THEN FULL_SIMP_TAC (srw_ss()) [word_xor_n2w]);
val word_xor_lemma16 = Q.prove(
`!w v:word16. (w ?? v) = n2w (BITWISE 16 (\x y. x <> y) (w2n w) (w2n v))`,
REPEAT Cases THEN FULL_SIMP_TAC (srw_ss()) [word_xor_n2w]);
val res = translate word_xor_lemma
val res = translate word_xor_lemma8
val res = translate word_xor_lemma16
val word_or_lemma = Q.prove(
`!w v:word32. (w !! v) = n2w (BITWISE 32 (\x y. x \/ y) (w2n w) (w2n v))`,
REPEAT Cases THEN FULL_SIMP_TAC (srw_ss()) [word_or_n2w]
THEN `(\x y. x \/ y) = $\/` by FULL_SIMP_TAC std_ss [FUN_EQ_THM]
THEN FULL_SIMP_TAC std_ss []);
val word_or_lemma16 = Q.prove(
`!w v:word16. (w !! v) = n2w (BITWISE 16 (\x y. x \/ y) (w2n w) (w2n v))`,
REPEAT Cases THEN FULL_SIMP_TAC (srw_ss()) [word_or_n2w]
THEN `(\x y. x \/ y) = $\/` by FULL_SIMP_TAC std_ss [FUN_EQ_THM]
THEN FULL_SIMP_TAC std_ss []);
val res = translate word_or_lemma
val res = translate word_or_lemma16
val word_and_lemma = Q.prove(
`!w v:word32. (w && v) = n2w (BITWISE 32 (\x y. x /\ y) (w2n w) (w2n v))`,
REPEAT Cases THEN FULL_SIMP_TAC (srw_ss()) [word_and_n2w]
THEN `(\x y. x /\ y) = (/\)` by FULL_SIMP_TAC std_ss [FUN_EQ_THM]
THEN FULL_SIMP_TAC std_ss []);
val res = translate word_and_lemma
val res = translate (WORD_MUL_LSL |> INST_TYPE [alpha|->``:32``])
val res = translate (WORD_MUL_LSL |> INST_TYPE [alpha|->``:16``])
val res = translate (WORD_MUL_LSL |> INST_TYPE [alpha|->``:8``])
val WORD_LSR_LEMMA = Q.prove(
`!w n. (w >>> n) = n2w (w2n w DIV 2**n)`,
Cases THEN SIMP_TAC std_ss [GSYM w2n_11,w2n_lsr,w2n_n2w,n2w_w2n]
THEN REPEAT STRIP_TAC
THEN `n MOD dimword (:'a) DIV 2 ** n' < dimword (:'a)` by ALL_TAC
THEN FULL_SIMP_TAC std_ss [DIV_LT_X]
THEN Cases_on `(2:num) ** n'`
THEN FULL_SIMP_TAC std_ss [ADD1] THEN DECIDE_TAC);
val res = translate (WORD_LSR_LEMMA |> INST_TYPE [alpha|->``:32``])
val res = translate (WORD_LSR_LEMMA |> INST_TYPE [alpha|->``:16``])
val res = translate (WORD_LSR_LEMMA |> INST_TYPE [alpha|->``:8``])
val word_msb_thm = Q.prove(
`!w. word_msb (w:'a word) = BIT (dimindex (:'a) - 1) (w2n w)`,
Cases THEN FULL_SIMP_TAC std_ss [word_msb_n2w,w2n_n2w]);
val word_lsb_thm = Q.prove(
`!w. word_lsb (w:'a word) = ~(w2n w MOD 2 = 0)`,
Cases THEN FULL_SIMP_TAC std_ss [word_lsb_n2w,w2n_n2w,ODD_EVEN,EVEN_MOD2]);
val sub_lemma = SIMP_RULE std_ss [word_2comp_def] word_sub_def
fun f32 lemma =
lemma |> INST_TYPE [alpha|->``:32``] |> SIMP_RULE (srw_ss()) []
fun f16 lemma =
lemma |> INST_TYPE [alpha|->``:16``] |> SIMP_RULE (srw_ss()) []
fun f8 lemma =
lemma |> INST_TYPE [alpha|->``:8``] |> SIMP_RULE (srw_ss()) []
fun ff32 lemma =
lemma |> INST_TYPE [alpha|->``:32``] |> SIMP_RULE (std_ss++SIZES_ss) []
fun ff16 lemma =
lemma |> INST_TYPE [alpha|->``:16``] |> SIMP_RULE (std_ss++SIZES_ss) []
fun ff8 lemma =
lemma |> INST_TYPE [alpha|->``:8``] |> SIMP_RULE (std_ss++SIZES_ss) []
val res = translate (f32 word_msb_thm);
val res = translate (f16 word_msb_thm);
val res = translate (f8 word_msb_thm);
val res = translate (f32 word_lsb_thm);
val res = translate (f16 word_lsb_thm);
val res = translate (f8 word_lsb_thm);
val res = translate (f32 word_asr_n2w);
val res = translate (f16 word_asr_n2w);
val res = translate (ff32 sub_lemma);
val res = translate (ff16 sub_lemma);
val res = translate (ff8 sub_lemma);
val lemma = Q.prove(
`(h--l) (w:word32 ) = n2w (BITS (MIN h 31) l (w2n w))`,
`(h--l) w = (h--l) (n2w (w2n w))` by METIS_TAC [n2w_w2n]
THEN SRW_TAC [] [word_bits_n2w, dimindex_32]);
val res = translate lemma;
val res = translate (ff32 wordsTheory.word_ror)
val res = translate (ff32 wordsTheory.word_rol_def)
val _ = export_theory();