source: src/ASM/AssemblyProof.ma @ 833

Last change on this file since 833 was 833, checked in by sacerdot, 8 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.