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
|
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,184,42,0,0,0,0,0,0,0,195]"
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
|