source: src/ASM/AssemblyProof.ma @ 833

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

Bug fixed to make the file compile.
But the type of the assembly function is no more right.

File size: 9.1 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      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
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
81(* RUSSEL **)
82
83include "basics/jmeq.ma".
84
85definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
86definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
87
88coercion inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
89coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
90
91(* END RUSSELL **)
92
93definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
94 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
95
96  λticks_of.
97  λs.
98  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
99  let ticks ≝ ticks_of (program_counter ? s) in
100  let s ≝ set_clock ? s (clock ? s + ticks) in
101  let s ≝ set_program_counter ? s pc in
102  let s ≝
103    match instr with
104    [ Instruction instr ⇒
105       Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
106    | Comment cmt ⇒ Some PseudoStatus s
107    | Cost cst ⇒ Some PseudoStatus s
108    | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
109    | Call call ⇒
110      let a ≝ address_of_word_labels s call in
111      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
112      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
113      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
114      let s ≝ write_at_stack_pointer ? s pc_bl in
115      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
116      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
117      let s ≝ write_at_stack_pointer ? s pc_bu in
118        Some PseudoStatus (set_program_counter ? s a)
119    | Mov dptr ident ⇒
120       Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
121    ]
122  in
123    s.
124 [
125 |2,3,4: %
126 | whd % 
127
128  λticks_of.
129  λs.
130  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
131  let ticks ≝ ticks_of (program_counter ? s) in
132  let s ≝ set_clock ? s (clock ? s + ticks) in
133  let s ≝ set_program_counter ? s pc in
134  let s ≝
135    match instr with
136    [ Instruction instr ⇒
137       Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
138    | Comment cmt ⇒ Some PseudoStatus s
139    | Cost cst ⇒ Some PseudoStatus s
140    | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
141    | Call call ⇒
142      let a ≝ address_of_word_labels s call in
143      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
144      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
145      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
146      let s ≝ write_at_stack_pointer ? s pc_bl in
147      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
148      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
149      let s ≝ write_at_stack_pointer ? s pc_bu in
150        Some PseudoStatus (set_program_counter ? s a)
151    | Mov dptr ident ⇒
152       Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
153    ]
154  in
155    s.
156  [2: % ]
157  normalize
158  @ I
159qed.
160
161
162
163definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
164 {{ ps':PseudoStatus | code_memory … ps = code_memory … ps' }
165
166  λticks_of.
167  λs.
168  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
169  let ticks ≝ ticks_of (program_counter ? s) in
170  let s ≝ set_clock ? s (clock ? s + ticks) in
171  let s ≝ set_program_counter ? s pc in
172  let s ≝
173    match instr with
174    [ Instruction instr ⇒
175       Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
176    | Comment cmt ⇒ Some PseudoStatus s
177    | Cost cst ⇒ Some PseudoStatus s
178    | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
179    | Call call ⇒
180      let a ≝ address_of_word_labels s call in
181      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
182      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
183      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
184      let s ≝ write_at_stack_pointer ? s pc_bl in
185      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
186      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
187      let s ≝ write_at_stack_pointer ? s pc_bu in
188        Some PseudoStatus (set_program_counter ? s a)
189    | Mov dptr ident ⇒
190       Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
191    ]
192  in
193    s.
194  [2: % ]
195  normalize
196  @ I
197qed.
198
199
200
201lemma execute_code_memory_unchanged:
202 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
203 #ticks #ps whd in ⊢ (??? (??%))
204 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
205  (program_counter pseudo_assembly_program ps)) #instr #pc
206 whd in ⊢ (??? (??%)) cases instr
207  [ #pre cases pre
208     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
209       cases (split ????) #z1 #z2 %
210     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
211       cases (split ????) #z1 #z2 %
212     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
213       cases (split ????) #z1 #z2 %
214     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
215       [ #x1 whd in ⊢ (??? (??%))
216     | *: cases not_implemented
217     ]
218  | #comment %
219  | #cost %
220  | #label %
221  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
222    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
223    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
224    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
225    (* CSC: ??? *)
226  | #dptr #label (* CSC: ??? *)
227  ]
228  cases not_implemented
229qed.
230
231lemma foo:
232 ∀ticks_of.
233 ∀ps: PseudoStatus.
234  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
235  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
236  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
237  let s' ≝ execute_1 s in
238   s = s'']].
239 #ticks_of #ps
240 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
241 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
242 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
243 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
Note: See TracBrowser for help on using the repository browser.