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
|
theory Examples
imports Frontend
begin
lemma overflow: "operate Add (-1) 1 = 0"
by eval
lemma multiply_overflow: "operate Mul (2 ^ 63) 2 = 0"
by eval
lemma shift_mask: "operate Shl 7 64 = 7"
by eval
lemma shift_wrap: "operate Shl 7 65 = 14"
by eval
lemma logical_shift: "operate Shr (-1) 63 = 1"
by eval
lemma unsigned_comparison: "operate Less (-1) 1 = 0"
by eval
lemma unsigned_high_bit: "operate Less 1 (2 ^ 63) = 1"
by eval
lemma constant_fold:
"optimise (Binary Add (Literal (-1)) (Literal 1)) = Literal 0"
by eval
lemma neutral_arithmetic:
"optimise (Binary Mul (Binary Add (Input X) (Literal 0)) (Literal 1)) = Input X"
by eval
lemma neutral_bits:
"optimise (Binary And (Binary Xor (Input Y) (Literal 0)) (Literal (-1))) = Input Y"
by eval
lemma absorbing_arithmetic:
"optimise (Binary Mul (Input X) (Literal 0)) = Literal 0"
by eval
lemma absorbing_bits:
"optimise (Binary Or (Binary And (Input Y) (Literal 0)) (Literal (-1))) = Literal (-1)"
by eval
lemma dead_branch:
"optimise (Cond (Literal 0) (Input X) (Input Y)) = Input Y"
by eval
lemma equal_branches:
"optimise (Cond (Input T) (Input X) (Input X)) = Input X"
by eval
lemma stack_bound_tight:
"bounded 2 (compile (Binary Add (Input X) (Input Y)) []) 0 \<and>
\<not> bounded 1 (compile (Binary Add (Input X) (Input Y)) []) 0"
by eval
lemma literal_code:
"executable (Literal 42) = [72,199,192,42,0,0,0,195]"
by eval
lemma signed_immediates:
"encode (Immediate (-1)) = [72,199,192,255,255,255,255] \<and>
length (encode (Immediate 2147483647)) = 7 \<and>
length (encode (Immediate 2147483648)) = 10 \<and>
length (encode (Immediate (-2147483648))) = 7 \<and>
length (encode (Immediate (-2147483649))) = 10"
by eval
lemma compact_slots:
"encode (Peek 15) = [72,139,68,36,120] \<and>
length (encode (Peek 16)) = 8 \<and>
decode [72,139,68,36,128] = None \<and>
decode [72,139,68,36,7] = None"
by eval
lemma opcode_roundtrip:
"decode [72,145,72,211,232,195] = Some (Arithmetic Shr,[195])"
by eval
lemma truncated_literal: "decode [72,184,0,0] = None"
by eval
lemma unaligned_slot: "decode [72,139,132,36,1,0,0,0] = None"
by eval
lemma negative_slot: "decode [72,139,132,36,0,0,0,128] = None"
by eval
lemma lexical_shadow:
"reference ''(let x 7 (let x (+ x 2) (* x x)))'' ''1'' ''2'' ''3'' = (True,''81'' @ newline)"
by eval
lemma numeric_identifier:
"reference ''(let x1 7 (let x1 (+ x1 2) (* x1 x1)))'' ''0'' ''0'' ''0'' = (True,''81'' @ newline)"
by eval
lemma numeric_prefix_rejected: "prepare ''(let 1x 3 1x)'' = None"
by eval
lemma nested_temporaries:
"reference ''(+ 10 (let a 3 (+ a (let b 4 (* a b)))))'' ''0'' ''0'' ''0'' = (True,''25'' @ newline)"
by eval
lemma unbound_rejected: "prepare ''(let a 3 b)'' = None"
by eval
lemma trailing_rejected: "prepare ''(+ x y) 1'' = None"
by eval
lemma literal_overflow_rejected: "prepare ''18446744073709551616'' = None"
by eval
lemma hexadecimal_boundaries:
"number ''0xffffffffffffffff'' = Some (2 ^ 64 - 1) \<and>
number ''0x10000000000000000'' = None"
by eval
lemma hexadecimal_execution:
"reference ''(+ x 0XfF)'' ''0x1'' ''0'' ''0'' = (True,''256'' @ newline)"
by eval
lemma incomplete_rejected: "prepare ''(if x y)'' = None"
by eval
lemma comment_tokens:
"lex (''(+ x; ignore ) tokens'' @ newline @ ''y) ; end'') [] [] = [''('', ''+'', ''x'', ''y'', '')'']"
by eval
lemma missing_operand_offset:
"source_error ''(+ x)'' = ''syntax error at token 3'' @ newline"
by eval
lemma trailing_token_offset:
"source_error ''(+ x y) 1'' = ''syntax error at token 5'' @ newline"
by eval
lemma exhausted_parser:
"diagnose 0 [] [''1''] 7 = Failed (Exhausted 7)"
by (subst diagnose.simps) simp
end
|