~james/span

span/tests/Examples.thy -rw-r--r-- 2.2 KiB
0c6f163a — james chore(import): snapshot james.dad.town/span at 868a68649c22 14 hours ago 
                                                                                
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

theory Examples
  imports "../src/Frontend"
begin

definition cascade :: "nat instruction list" where
  "cascade = [Jump 127, Jump 130] @ replicate 128 Nop @ [Stop]"

definition countdown :: "nat instruction list" where
  "countdown = [Inc, Inc, Inc, Dec, Zero 6, Jump 3, Stop]"

definition forward :: "nat \<Rightarrow> nat instruction list" where
  "forward n = [Jump (Suc n)] @ replicate n Nop @ [Stop]"

definition backward :: "nat \<Rightarrow> nat instruction list" where
  "backward n = replicate n Nop @ [Jump 0, Stop]"

lemma cascade_rounds:
  "map (\<lambda>W. filter (\<lambda>i. i \<in> W) [0..<length cascade]) (history cascade {}) = [[], [1], [0,1]]"
  by eval

lemma cascade_size: "map_option length (assemble cascade) = Some 135"
  by eval

lemma forward_short: "layout (forward 127) = {}"
  by eval

lemma forward_long: "layout (forward 128) = {0}"
  by eval

lemma backward_short: "layout (backward 126) = {}"
  by eval

lemma backward_long: "layout (backward 127) = {127}"
  by eval

lemma countdown_execution:
  "execute (source_step countdown) 32 (0,0) = (6,0)"
  by eval

lemma countdown_bytes:
  "assemble countdown = Some [1,1,1,2,17,130,16,123,3]"
  by eval

lemma short_negative_boundary:
  "decode [16,0] = Some (Branch False False (-128), [])"
  by eval

lemma long_negative_boundary:
  "decode [18,0,0] = Some (Branch False True (-32768), [])"
  by eval

lemma long_positive_boundary:
  "decode [18,255,255] = Some (Branch False True 32767, [])"
  by eval

lemma truncated_rejected: "decode [18,1] = None"
  by eval

lemma unknown_rejected: "decode [255] = None"
  by eval

lemma short_payload_rejected: "decode [16,256] = None"
  by eval

lemma long_payload_rejected: "decode [19,0,256] = None"
  by eval

lemma decoder_preserves_tail:
  "decode [19,255,255,3,255] = Some (Branch True True 32767, [3,255])"
  by eval

lemma undefined_rejected:
  "compile ''jmp missing'' = Error ''undefined label missing''"
  by eval

lemma duplicate_rejected:
  "compile (''label a'' @ newline @ ''label a'') = Error ''duplicate label a''"
  by eval

lemma final_label_rejected:
  "compile (''jmp end'' @ newline @ ''label end'') = Error ''branch targets a label after the final instruction''"
  by eval

end