source: Deliverables/D4.1/Matita/Test.ma @ 347

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

Work on main execution loop. All cases covered. Need to close open proof states and remove computational axioms.

File size: 7.6 KB
Line 
1include "Interpret.ma".
2include "Assembly.ma".
3
4ndefinition test: List instruction ≝
5 [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]]);
6  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;false;true;false;false]]);
7  SJMP … (RELATIVE [[true;true;true;true;true;true;true;false]]);
8  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;false;false;true;true;true]])〉))));
9  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;true;true;true;false]]);
10  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
11  Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;true]]));
12  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
13  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
14  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
15  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
16  Jump … (JZ … (RELATIVE [[false;false;false;true;true;false;true;true]]));
17  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
18  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;true;false]])〉)));
19  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
20  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
21  CLR … (ACC_A);
22  MOVC … (ACC_A) (ACC_DPTR);
23  MOVX … (Right … 〈(EXT_INDIRECT false),(ACC_A)〉);
24  INC … (DPTR);
25  INC … (REGISTER [[false;false;false]]);
26  Jump … (CJNE … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉) (RELATIVE [[false;false;false;false;false;false;true;false]]));
27  INC … (DIRECT [[true;false;true;false;false;false;false;false]]);
28  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;false;true;false;false]]));
29  Jump … (DJNZ … (REGISTER [[false;true;false]]) (RELATIVE [[true;true;true;true;false;false;true;false]]));
30  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
31  CLR … (ACC_A);
32  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));
33  MOV … (Left … (Left … (Left … (Left … (Right … 〈(INDIRECT false),(ACC_A)〉)))));
34  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;true]]));
35  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
36  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
37  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
38  Jump … (JZ … (RELATIVE [[false;false;false;false;true;false;true;false]]));
39  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
40  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
41  CLR … (ACC_A);
42  MOVX … (Right … 〈(EXT_INDIRECT true),(ACC_A)〉);
43  INC … (REGISTER [[false;false;true]]);
44  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
45  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
46  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
47  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
48  Jump … (JZ … (RELATIVE [[false;false;false;false;true;true;false;false]]));
49  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
50  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
51  CLR … (ACC_A);
52  MOVX … (Right … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
53  INC … (DPTR);
54  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
55  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;true;false;true;false]]));
56  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
57  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉)))));
58  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(DATA [[false;false;false;false;true;true;true;true]])〉))));
59  XCHD … (ACC_A) (INDIRECT false);
60  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
61  RET … ;
62  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
63  RET … ;
64  NOP … ;
65  NOP … ;
66  NOP … ;
67  NOP … ;
68  NOP … ;
69  NOP … ;
70  NOP … ;
71  NOP … ;
72  NOP … ;
73  NOP … ;
74  NOP … ;
75  NOP … ;
76  NOP … ;
77  NOP … ;
78  NOP … ;
79  NOP … ;
80  NOP … ;
81  NOP … ;
82  NOP … ;
83  NOP … ;
84  NOP … ;
85  NOP … ;
86  NOP … ;
87  NOP … ;
88  NOP … ;
89  NOP … ;
90  NOP … ;
91  NOP … ;
92  NOP … ;
93  NOP … ;
94  NOP … ;
95  NOP … ;
96  NOP … ;
97  NOP … ;
98  NOP … ;
99  NOP … ;
100  NOP … ;
101  NOP … ;
102  NOP … ;
103  NOP … ;
104  NOP … ;
105  NOP … ;
106  NOP … ;
107  NOP … ;
108  NOP … ;
109  NOP … ;
110  NOP … ;
111  NOP … ;
112  NOP … ;
113  NOP … ;
114  NOP … ;
115  NOP … ;
116  NOP … ;
117  NOP … ;
118  NOP … ;
119  NOP … ;
120  NOP … ;
121  NOP … ;
122  NOP … ;
123  NOP … ;
124  NOP … ;
125  NOP … ;
126  NOP … ;
127  NOP … ;
128  NOP … ;
129  NOP … ;
130  NOP … ;
131  NOP … ;
132  NOP … ;
133  NOP … ;
134  NOP … ;
135  NOP … ;
136  NOP … ;
137  NOP … ;
138  NOP … ;
139  NOP … ;
140  NOP … ;
141  NOP … ;
142  NOP … ;
143  NOP … ;
144  NOP … ;
145  NOP … ;
146  NOP … ;
147  NOP … ;
148  NOP … ;
149  NOP … ;
150  NOP … ].
151 @.
152nqed.
153
154ndefinition testmem ≝ assembly test.
155
156nlemma foo: testmem = testmem.
157 nnormalize; @.
158nqed.
159
160ndefinition teststatus ≝ load testmem initialise_status.
161
162nlemma goo: teststatus = teststatus.
163 nnormalize; @.
164nqed.
165
166ndefinition testfinal ≝ execute five teststatus.
167
168nlemma hoo: testfinal = testfinal.
169 nwhd in ⊢ (???%);
170 nnormalize; @.
171nqed.
Note: See TracBrowser for help on using the repository browser.