source: src/ASM/DoTest.ma @ 688

Last change on this file since 688 was 472, checked in by mulligan, 10 years ago

More changes to debug and testing files to get them to work with the standard library.

File size: 12.2 KB
Line 
1include "Test.ma".
2include "Interpret.ma".
3include "Assembly.ma".
4
5ndefinition steps ≝ 1.
6
7ndefinition testmem ≝ assembly_unlabelled_program test.
8ndefinition teststatus ≝
9 match testmem with
10  [ None ⇒ None …
11  | Some testmem ⇒ Some … (load (fst … testmem) initialise_status)].
12ndefinition testfinal ≝
13 match teststatus with
14  [ None ⇒ None …
15  | Some teststatus ⇒ Some … (execute steps teststatus)].
16
17notation "'STATUS' pc sfr" with precedence 90 for @{ 'status $pc $sfr }.
18interpretation "status" 'status pc sfr = (mk_Status ? ? ? ? pc sfr ? ? ? ?).
19
20nlet rec execute_trace (n: nat) (s: Status) on n: list ? ≝
21  match n with
22    [ O ⇒ []
23    | S o ⇒
24       fst … (fst … (fetch (code_memory s) (program_counter s))) :: execute_trace o (execute_1 s)
25    ].
26
27ndefinition testtrace ≝
28 match teststatus with
29  [ None ⇒ None …
30  | Some teststatus ⇒ Some … (execute_trace steps teststatus)].
31
32interpretation "left" 'left x = (inl ?? x).
33interpretation "right" 'right x = (inr ?? x).
34
35notation < "'L' x" with precedence 70 for @{ 'left $x }.
36notation < "'R' x" with precedence 70 for @{ 'right $x }.
37
38notation < "𝟘" with precedence 90 for @{ 'zero }.
39notation < "𝟙" with precedence 90 for @{ 'one }.
40notation < "𝟚" with precedence 90 for @{ 'two }.
41notation < "𝟛" with precedence 90 for @{ 'three }.
42notation < "𝟜" with precedence 90 for @{ 'four }.
43notation < "𝟝" with precedence 90 for @{ 'five }.
44notation < "𝟞" with precedence 90 for @{ 'six }.
45notation < "𝟟" with precedence 90 for @{ 'seven }.
46notation < "𝟠" with precedence 90 for @{ 'eight }.
47notation < "𝟡" with precedence 90 for @{ 'nine }.
48notation < "𝔸" with precedence 90 for @{ 'a }.
49notation < "𝔹" with precedence 90 for @{ 'b }.
50notation < "∁" with precedence 90 for @{ 'c }.
51notation < "𝔻" with precedence 90 for @{ 'd }.
52notation < "𝔼" with precedence 90 for @{ 'e }.
53notation < "𝔽" with precedence 90 for @{ 'f }.
54
55
56interpretation "zero" 'zero = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ?? false (VEmpty ?))))).
57interpretation "one" 'one = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ?? true (VEmpty ?))))).
58interpretation "two" 'two = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ?? false (VEmpty ?))))).
59interpretation "three" 'three = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ?? true (VEmpty ?))))).
60interpretation "four" 'four = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ?? false (VEmpty ?))))).
61interpretation "five" 'five = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ?? true (VEmpty ?))))).
62interpretation "six" 'six = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ?? false (VEmpty ?))))).
63interpretation "seven" 'seven = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ?? true (VEmpty ?))))).
64interpretation "eight" 'eight = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ?? false (VEmpty ?))))).
65interpretation "nine" 'nine = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ?? true (VEmpty ?))))).
66interpretation "A" 'a = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ?? false (VEmpty ?))))).
67interpretation "B" 'b = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ?? true (VEmpty ?))))).
68interpretation "C" 'c = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ?? false (VEmpty ?))))).
69interpretation "D" 'd = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ?? true (VEmpty ?))))).
70interpretation "E" 'e = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ?? false (VEmpty ?))))).
71interpretation "F" 'f = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ?? true (VEmpty ?))))).
72
73notation < "𝟘l" with precedence 90 for @{ 'zero4 $l }.
74notation < "𝟙l" with precedence 90 for @{ 'one4 $l }.
75notation < "𝟚l" with precedence 90 for @{ 'two4 $l }.
76notation < "𝟛l" with precedence 90 for @{ 'three4 $l }.
77notation < "𝟜l" with precedence 90 for @{ 'four4 $l }.
78notation < "𝟝l" with precedence 90 for @{ 'five4 $l }.
79notation < "𝟞l" with precedence 90 for @{ 'six4 $l }.
80notation < "𝟟l" with precedence 90 for @{ 'seven4 $l }.
81notation < "𝟠l" with precedence 90 for @{ 'eight4 $l }.
82notation < "𝟡l" with precedence 90 for @{ 'nine4 $l }.
83notation < "𝔸l" with precedence 90 for @{ 'a4 $l }.
84notation < "𝔹l" with precedence 90 for @{ 'b4 $l }.
85notation < "∁l" with precedence 90 for @{ 'c4 $l }.
86notation < "𝔻l" with precedence 90 for @{ 'd4 $l }.
87notation < "𝔼l" with precedence 90 for @{ 'e4 $l }.
88notation < "𝔽l" with precedence 90 for @{ 'f4 $l }.
89
90interpretation "zero4" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S O)))) false l)))).
91interpretation "one4" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S O)))) true l)))).
92interpretation "two4" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S O)))) false l)))).
93interpretation "three4" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S O)))) true l)))).
94interpretation "four4" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S O)))) false l)))).
95interpretation "five4" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S O)))) true l)))).
96interpretation "six4" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S O)))) false l)))).
97interpretation "seven4" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S O)))) true l)))).
98interpretation "eight4" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S O)))) false l)))).
99interpretation "nine4" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S O)))) true l)))).
100interpretation "A4" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S O)))) false l)))).
101interpretation "B4" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S O)))) true l)))).
102interpretation "C4" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S O)))) false l)))).
103interpretation "D4" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S O)))) true l)))).
104interpretation "E4" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S O)))) false l)))).
105interpretation "F4" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S O)))) true l)))).
106
107interpretation "zero8" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
108interpretation "one8" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
109interpretation "two8" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
110interpretation "three8" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
111interpretation "four8" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
112interpretation "five8" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
113interpretation "six8" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
114interpretation "seven8" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
115interpretation "eight8" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
116interpretation "nine8" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
117interpretation "A8" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
118interpretation "B8" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
119interpretation "C8" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
120interpretation "D8" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
121interpretation "E8" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
122interpretation "F8" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
123
124interpretation "zero16" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
125interpretation "one16" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
126interpretation "two16" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
127interpretation "three16" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
128interpretation "four16" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
129interpretation "five16" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
130interpretation "six16" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
131interpretation "seven16" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
132interpretation "eight16" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
133interpretation "nine16" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
134interpretation "A16" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
135interpretation "B16" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
136interpretation "C16" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
137interpretation "D16" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
138interpretation "E16" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
139interpretation "F16" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
140
141notation < "…" with precedence 90 for @{ 'hide }.
142interpretation "[[relative]]" 'hide = (VCons ?? relative (VEmpty ?)).
143
144ndefinition dbg ≝
145  match teststatus with
146    [ None ⇒ None ?
147    | Some s ⇒
148      let lk ≝ lookup ? 7 ([[ false; false; false ]] @@ (max 4)) (low_internal_ram s) (zero ?) in
149        Some … 〈lk, program_counter s〉
150    ].
151   
152nlemma test:
153  dbg = dbg.
154  nnormalize;
155  @;
156nqed.
157
158nlemma test3:
159  half_add ? (sign_extension (bitvector_of_nat 8 (256 - 3)))
160                                     (bitvector_of_nat 16 32) =
161  half_add ? (sign_extension (bitvector_of_nat 8 (256 - 3)))
162                                     (bitvector_of_nat 16 32).
163  nnormalize;
164  @;
165nqed.
166
167ndefinition instr ≝
168  match teststatus with
169    [ None ⇒ None …   
170    | Some teststatus ⇒
171        Some … (fetch (code_memory teststatus) (bitvector_of_nat ? (256 + 32 + 24)))
172    ].
173
174ndefinition ftchtst ≝
175  match testfinal with
176    [ None ⇒ None …
177    | Some teststatus ⇒ Some … (next (code_memory teststatus) (program_counter teststatus))
178    ].
179
180(*   
181nlemma test5:
182  ftchtst = ftchtst.
183  nnormalize;
184
185nlemma test4:
186  instr = instr.
187  nnormalize;
188  @;
189nqed.
190
191nlemma test2:
192  get_arg_8 initialise_status false ACC_A =
193  get_arg_8 initialise_status false ACC_A.
194  nnormalize;
195  @;
196nqed.
197*)
198
199nlemma do_test: testtrace = testtrace.
200 nnormalize in ⊢ (??%?); (* STOP HERE TO SEE THE TRACE *)
201 nnormalize;
202 @.
203nqed.
Note: See TracBrowser for help on using the repository browser.