9 begin |
9 begin |
10 |
10 |
11 declare [[smt2_oracle = true]] |
11 declare [[smt2_oracle = true]] |
12 declare [[z3_new_extensions = true]] |
12 declare [[z3_new_extensions = true]] |
13 declare [[smt2_certificates = "SMT_Word_Examples.certs2"]] |
13 declare [[smt2_certificates = "SMT_Word_Examples.certs2"]] |
14 declare [[smt2_read_only_certificates = false]] (* FIXME *) |
14 declare [[smt2_read_only_certificates = true]] |
15 |
15 |
16 text {* |
16 text {* |
17 Currently, there is no proof reconstruction for words. |
17 Currently, there is no proof reconstruction for words. |
18 All lemmas are proved using the oracle mechanism. |
18 All lemmas are proved using the oracle mechanism. |
19 *} |
19 *} |
20 |
20 |
21 |
21 |
22 section {* Bitvector numbers *} |
22 section {* Bitvector numbers *} |
23 |
23 |
24 lemma "(27 :: 4 word) = -5" by smt2 |
24 lemma "(27 :: 4 word) = -5" by smt2 |
25 |
|
26 lemma "(27 :: 4 word) = 11" by smt2 |
25 lemma "(27 :: 4 word) = 11" by smt2 |
27 |
|
28 lemma "23 < (27::8 word)" by smt2 |
26 lemma "23 < (27::8 word)" by smt2 |
29 |
|
30 lemma "27 + 11 = (6::5 word)" by smt2 |
27 lemma "27 + 11 = (6::5 word)" by smt2 |
31 |
|
32 lemma "7 * 3 = (21::8 word)" by smt2 |
28 lemma "7 * 3 = (21::8 word)" by smt2 |
33 |
|
34 lemma "11 - 27 = (-16::8 word)" by smt2 |
29 lemma "11 - 27 = (-16::8 word)" by smt2 |
35 |
|
36 lemma "- -11 = (11::5 word)" by smt2 |
30 lemma "- -11 = (11::5 word)" by smt2 |
37 |
|
38 lemma "-40 + 1 = (-39::7 word)" by smt2 |
31 lemma "-40 + 1 = (-39::7 word)" by smt2 |
39 |
|
40 lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by smt2 |
32 lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by smt2 |
41 |
|
42 lemma "x = (5 :: 4 word) \<Longrightarrow> 4 * x = 4" by smt2 |
33 lemma "x = (5 :: 4 word) \<Longrightarrow> 4 * x = 4" by smt2 |
43 |
34 |
44 |
35 |
45 section {* Bit-level logic *} |
36 section {* Bit-level logic *} |
46 |
37 |
47 lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by smt2 |
38 lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by smt2 |
48 |
|
49 lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by smt2 |
39 lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by smt2 |
50 |
|
51 lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)" by smt2 |
40 lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)" by smt2 |
52 |
|
53 lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by smt2 |
41 lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by smt2 |
54 |
|
55 lemma "word_cat (27::4 word) (27::8 word) = (2843::12 word)" by smt2 |
42 lemma "word_cat (27::4 word) (27::8 word) = (2843::12 word)" by smt2 |
56 |
|
57 lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" by smt2 |
43 lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" by smt2 |
58 |
|
59 lemma "slice 1 (0b10110 :: 4 word) = (0b11 :: 2 word)" by smt2 |
44 lemma "slice 1 (0b10110 :: 4 word) = (0b11 :: 2 word)" by smt2 |
60 |
|
61 lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by smt2 |
45 lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by smt2 |
62 |
|
63 lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by smt2 |
46 lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by smt2 |
64 |
|
65 lemma "0b10011 << 2 = (0b1001100::8 word)" by smt2 |
47 lemma "0b10011 << 2 = (0b1001100::8 word)" by smt2 |
66 |
|
67 lemma "0b11001 >> 2 = (0b110::8 word)" by smt2 |
48 lemma "0b11001 >> 2 = (0b110::8 word)" by smt2 |
68 |
|
69 lemma "0b10011 >>> 2 = (0b100::8 word)" by smt2 |
49 lemma "0b10011 >>> 2 = (0b100::8 word)" by smt2 |
70 |
|
71 lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by smt2 |
50 lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by smt2 |
72 |
|
73 lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by smt2 |
51 lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by smt2 |
74 |
|
75 lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by smt2 |
52 lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by smt2 |
76 |
|
77 lemma "w < 256 \<Longrightarrow> (w :: 16 word) AND 0x00FF = w" by smt2 |
53 lemma "w < 256 \<Longrightarrow> (w :: 16 word) AND 0x00FF = w" by smt2 |
78 |
54 |
79 |
55 |
80 section {* Combined integer-bitvector properties *} |
56 section {* Combined integer-bitvector properties *} |
81 |
57 |