-
Notifications
You must be signed in to change notification settings - Fork 83
/
Word64ProgScript.sml
127 lines (100 loc) · 3.68 KB
/
Word64ProgScript.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
(*
Module about the built-in word64 type.
*)
open preamble ml_translatorLib ml_progLib basisFunctionsLib
CharProgTheory
val _ = new_theory "Word64Prog";
val _ = translation_extends "CharProg";
(* Word64 module -- translated *)
val _ = ml_prog_update (open_module "Word64");
val () = generate_sigs := true;
val _ = ml_prog_update (add_dec
``Dtabbrev unknown_loc [] "word" (Atapp [] (Short "word64"))`` I);
(* to/from int *)
val _ = trans "fromInt" ``n2w:num->word64``;
val _ = trans "toInt" ``w2n:word64->num``;
val _ = trans "toIntSigned" ``w2i:word64->int``;
(* bitwise operations *)
val _ = trans "andb" ``word_and:word64->word64->word64``;;
val _ = trans "orb" ``word_or:word64->word64->word64``;
val _ = trans "xorb" ``word_xor:word64->word64->word64``;
val word_1comp_eq = prove(
``word_1comp w = word_xor w 0xFFFFFFFFFFFFFFFFw:word64``,
fs []);
val _ = (next_ml_names := ["notb"]);
val _ = translate word_1comp_eq
(* arithmetic *)
val _ = trans "+" ``word_add:word64->word64->word64``;
val _ = trans "-" ``word_sub:word64->word64->word64``;
(* shifts *)
val var_word_lsl_def = Define `
var_word_lsl (w:word64) (n:num) = if 64 < n then 0w
else if n < 8 then
if n < 4 then
if n < 2 then if n < 1 then w else w << 1
else if n < 3 then w << 2
else w << 3
else if n < 6 then if n < 5 then w << 4 else w << 5
else if n < 7 then w << 6
else w << 7 else var_word_lsl (w << 8) (n − 8)`
Theorem var_word_lsl_thm[simp]:
var_word_lsl w n = word_lsl w n
Proof
ntac 32 (
Cases_on `n` \\ fs [ADD1] THEN1 (EVAL_TAC \\ fs [LSL_ADD])
\\ Cases_on `n'` \\ fs [ADD1] THEN1 (EVAL_TAC \\ fs [LSL_ADD]))
\\ ntac 9 (once_rewrite_tac [var_word_lsl_def] \\ fs [])
QED
val var_word_lsr_def = Define `
var_word_lsr (w:word64) (n:num) = if 64 < n then 0w
else if n < 8 then
if n < 4 then
if n < 2 then if n < 1 then w else w >>> 1
else if n < 3 then w >>> 2
else w >>> 3
else if n < 6 then if n < 5 then w >>> 4 else w >>> 5
else if n < 7 then w >>> 6
else w >>> 7 else var_word_lsr (w >>> 8) (n − 8)`
Theorem var_word_lsr_thm[simp]:
var_word_lsr w n = word_lsr w n
Proof
ntac 32 (
Cases_on `n` \\ fs [ADD1] THEN1 (EVAL_TAC \\ fs [LSR_ADD])
\\ Cases_on `n'` \\ fs [ADD1] THEN1 (EVAL_TAC \\ fs [LSR_ADD]))
\\ ntac 9 (once_rewrite_tac [var_word_lsr_def] \\ fs [])
QED
val var_word_asr_def = Define `
var_word_asr (w:word64) (n:num) = if 64 < n then w >> 64
else if n < 8 then
if n < 4 then
if n < 2 then if n < 1 then w else w >> 1
else if n < 3 then w >> 2
else w >> 3
else if n < 6 then if n < 5 then w >> 4 else w >> 5
else if n < 7 then w >> 6
else w >> 7 else var_word_asr (w >> 8) (n − 8)`
Theorem var_word_asr_thm[simp]:
var_word_asr w n = word_asr w n
Proof
ntac 32 (
Cases_on `n` \\ fs [ADD1] THEN1 (EVAL_TAC \\ fs [ASR_ADD])
\\ Cases_on `n'` \\ fs [ADD1] THEN1 (EVAL_TAC \\ fs [ASR_ADD]))
\\ ntac 9 (once_rewrite_tac [var_word_asr_def] \\ fs [])
QED
val _ = (next_ml_names := ["<<"]);
val _ = translate var_word_lsl_def;
val _ = (next_ml_names := [">>"]);
val _ = translate var_word_lsr_def;
val _ = (next_ml_names := ["~>>"]);
val _ = translate var_word_asr_def;
val concat_all_def = Define `
concat_all (a:word8) b c d e f g h =
concat_word_list [a;b;c;d;e;f;g;h]:64 word`
val concat_all_impl =
REWRITE_RULE [concat_word_list_def, dimindex_8, ZERO_SHIFT, WORD_OR_CLAUSES] concat_all_def;
val _ = (next_ml_names := ["concatAll"]);
val _ = translate concat_all_impl;
val sigs = module_signatures ["fromInt", "toInt", "andb",
"orb", "xorb", "notb", "+", "-", "<<", ">>", "~>>", "concatAll"];
val _ = ml_prog_update (close_module (SOME sigs));
val _ = export_theory();