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

Last change on this file since 372 was 372, checked in by sacerdot, 9 years ago

No more axioms! All proofs completed.
(Interrupts, I/O and timers not ported to Matita yet)

File size: 1.6 KB
Line 
1include "Test.ma".
2include "Interpret.ma".
3include "Assembly.ma".
4
5ndefinition testmem ≝ assembly test.
6ndefinition teststatus ≝ load testmem initialise_status.
7ndefinition testfinal ≝ execute (four * two_hundred_and_fifty_six) teststatus.
8
9notation "'STATUS'" with precedence 90 for @{ 'status }.
10interpretation "status" 'status = (mk_Status ??????????).
11
12(*
13nlemma xoo: testfinal = testfinal.
14 nnormalize in ⊢ (??%?); @;
15nqed.
16*)
17
18(*
19nlemma test:
20 (let status ≝
21 load
22  (assembly [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]])])
23   initialise_status
24  in
25   fetch (code_memory status) (program_counter status)
26  ) = ?.
27##[ nnormalize in ⊢ (??%?);
28*)
29
30(*
31nlemma xoo:
32 (let testfinal ≝ testfinal in
33 first … (first … (fetch (code_memory testfinal) (program_counter testfinal)))) =
34 first … (first … (fetch (code_memory testfinal) (program_counter testfinal))).
35 nnormalize in ⊢ (??%?);
36nqed.
37
38ndefinition is_JZ ≝
39 λi: instruction.match i with
40     [ Jump arg ⇒
41        match arg with
42         [ JZ arg ⇒
43            match arg with
44             [ RELATIVE arg ⇒ arg
45             | _ ⇒ zero eight ]
46         | _ ⇒ zero eight ]
47     | _ ⇒ zero eight ].
48
49nlemma xoo:
50 (let testfinal ≝ testfinal in
51   is_JZ
52    (first … (first … (fetch (code_memory testfinal) (program_counter testfinal))))
53    )
54  = zero eight.
55 nnormalize in ⊢ (??%?);
56
57*)
58
59
60nlemma xoo: program_counter testfinal = program_counter testfinal.
61 nnormalize in ⊢ (??%?);
62 nnormalize in ⊢ (???%);
63 @.
64nqed.
Note: See TracBrowser for help on using the repository browser.