source: src/ASM/AssemblyProof.ma @ 828

Last change on this file since 828 was 828, checked in by sacerdot, 10 years ago

Proof statement.

File size: 2.7 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3
4let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
5                       (encoding: list Byte) on encoding: Prop ≝
6  match encoding with
7  [ nil ⇒ final_pc = pc
8  | cons hd tl ⇒
9    let 〈new_pc, byte〉 ≝ next code_memory pc in
10      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
11  ].
12
13definition assembly_specification:
14  ∀sigma: Word → Word. ∀assembly_program: pseudo_assembly_program.
15  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
16  λsigma.
17  λpseudo_assembly_program.
18  λcode_mem.
19    ∀pc: Word.
20      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
21      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
22      let address_of ≝ ? in
23      let labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in
24      let datalabels ≝ λx. sigma (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
25      let pre_assembled ≝ assembly_1_pseudoinstruction labels datalabels address_of 〈None ?, pre_instr〉 in
26        encoding_check code_mem pc (sigma pre_new_pc) pre_assembled.
27      cases not_implemented
28qed.
29
30axiom assembly_meets_specification:
31  ∀pseudo_assembly_program.
32    match assembly pseudo_assembly_program with
33    [ None ⇒ True
34    | Some code_mem_cost ⇒
35      let 〈code_mem, cost〉 ≝ code_mem_cost in
36        assembly_specification ? pseudo_assembly_program (load_code_memory code_mem)
37    ].
38cases not_implemented (*
39  # PROGRAM
40  [ cases PROGRAM
41    # PREAMBLE
42    # INSTR_LIST
43    elim INSTR_LIST
44    [ whd
45      whd in ⊢ (∀_. %)
46      # PC
47      whd
48    | # INSTR
49      # INSTR_LIST_TL
50      # H
51      whd
52      normalize
53    ]
54  | cases not_implemented
55  ] *)
56qed.
57
58axiom sigma: pseudo_assembly_program → Word → Word.
59
60definition status_of_pseudo_status: PseudoStatus → option Status ≝
61 λps.
62  let pap ≝ code_memory … ps in
63   match assembly pap with
64    [ None ⇒ None …
65    | Some p ⇒
66       let cm ≝ load_code_memory (\fst p) in
67       let pc ≝ sigma pap (program_counter ? ps) in
68        Some …
69         (mk_PreStatus (BitVectorTrie Byte 16)
70           cm
71           (low_internal_ram … ps)
72           (high_internal_ram … ps)
73           (external_ram … ps)
74           pc
75           (special_function_registers_8051 … ps)
76           (special_function_registers_8052 … ps)
77           (p1_latch … ps)
78           (p3_latch … ps)
79           (clock … ps)) ].
80
81lemma foo:
82 ∀ticks_of.
83 ∀ps: PseudoStatus.
84  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
85  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
86  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
87  let s' ≝ execute_1 s in
88   s = s'']].
Note: See TracBrowser for help on using the repository browser.