source: Deliverables/D4.1/Matita/DoTest.ma @ 557

Last change on this file since 557 was 472, checked in by mulligan, 9 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.