source: src/ASM/AssemblyProof.ma @ 834

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

Russell at work.

File size: 10.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
13(*
14definition assembly_specification:
15  ∀sigma: Word → Word. ∀assembly_program: pseudo_assembly_program.
16  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
17  λsigma.
18  λpseudo_assembly_program.
19  λcode_mem.
20    ∀pc: Word.
21      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
22      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
23      let address_of ≝ ? in
24      let labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in
25      let datalabels ≝ λx. sigma (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
26      let pre_assembled ≝ assembly_1_pseudoinstruction labels datalabels address_of 〈None ?, pre_instr〉 in
27        encoding_check code_mem pc (sigma pre_new_pc) pre_assembled.
28      cases not_implemented
29qed.
30
31axiom assembly_meets_specification:
32  ∀pseudo_assembly_program.
33    match assembly pseudo_assembly_program with
34    [ None ⇒ True
35    | Some code_mem_cost ⇒
36      let 〈code_mem, cost〉 ≝ code_mem_cost in
37        assembly_specification ? pseudo_assembly_program (load_code_memory code_mem)
38    ].
39cases not_implemented (*
40  # PROGRAM
41  [ cases PROGRAM
42    # PREAMBLE
43    # INSTR_LIST
44    elim INSTR_LIST
45    [ whd
46      whd in ⊢ (∀_. %)
47      # PC
48      whd
49    | # INSTR
50      # INSTR_LIST_TL
51      # H
52      whd
53      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
54    ]
55  | cases not_implemented
56  ] *)
57qed.
58*)
59
60axiom sigma: pseudo_assembly_program → Word → Word.
61
62(*
63definition status_of_pseudo_status: PseudoStatus → option Status ≝
64 λps.
65  let pap ≝ code_memory … ps in
66   match assembly pap with
67    [ None ⇒ None …
68    | Some p ⇒
69       let cm ≝ load_code_memory (\fst p) in
70       let pc ≝ sigma pap (program_counter ? ps) in
71        Some …
72         (mk_PreStatus (BitVectorTrie Byte 16)
73           cm
74           (low_internal_ram … ps)
75           (high_internal_ram … ps)
76           (external_ram … ps)
77           pc
78           (special_function_registers_8051 … ps)
79           (special_function_registers_8052 … ps)
80           (p1_latch … ps)
81           (p3_latch … ps)
82           (clock … ps)) ].
83*)
84
85(* RUSSEL **)
86
87include "basics/jmeq.ma".
88
89definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
90definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
91
92coercion inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
93coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
94
95lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
96 #A #P #p cases p #w #q @q
97qed.
98
99(* END RUSSELL **)
100
101definition write_at_stack_pointer:
102 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
103  λM: Type[0].
104  λs: PreStatus M.
105  λv: Byte.
106    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
107    let bit_zero ≝ get_index_v… nu O ? in
108    let bit_1 ≝ get_index_v… nu 1 ? in
109    let bit_2 ≝ get_index_v… nu 2 ? in
110    let bit_3 ≝ get_index_v… nu 3 ? in
111      if bit_zero then
112        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
113                              v (low_internal_ram ? s) in
114          set_low_internal_ram ? s memory
115      else
116        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
117                              v (high_internal_ram ? s) in
118          set_high_internal_ram ? s memory.
119  [ cases l0 %
120  |2,3,4,5: cases not_implemented (* CSC: ???? normalize repeat (@ le_S_S) @ le_O_n *)
121  ]
122qed.
123
124definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
125 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
126
127  λticks_of.
128  λs.
129  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
130  let ticks ≝ ticks_of (program_counter ? s) in
131  let s ≝ set_clock ? s (clock ? s + ticks) in
132  let s ≝ set_program_counter ? s pc in
133    match instr with
134    [ Instruction instr ⇒
135       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
136    | Comment cmt ⇒ s
137    | Cost cst ⇒ s
138    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
139    | Call call ⇒
140      let a ≝ address_of_word_labels s call in
141      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
142      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
143      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
144      let s ≝ write_at_stack_pointer ? s pc_bl in
145      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
146      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
147      let s ≝ write_at_stack_pointer ? s pc_bu in
148        set_program_counter ? s a
149    | Mov dptr ident ⇒
150       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
151    ].
152 [
153 |2,3,4: %
154 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
155 |
156 | (*CSC: ??? *)
157 | (*CSC: ??? *)
158 | %
159 ]
160qed.
161
162  λticks_of.
163  λs.
164  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
165  let ticks ≝ ticks_of (program_counter ? s) in
166  let s ≝ set_clock ? s (clock ? s + ticks) in
167  let s ≝ set_program_counter ? s pc in
168  let s ≝
169    match instr with
170    [ Instruction instr ⇒
171       Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
172    | Comment cmt ⇒ Some PseudoStatus s
173    | Cost cst ⇒ Some PseudoStatus s
174    | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
175    | Call call ⇒
176      let a ≝ address_of_word_labels s call in
177      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
178      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
179      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
180      let s ≝ write_at_stack_pointer ? s pc_bl 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 s ≝ write_at_stack_pointer ? s pc_bu in
184        Some PseudoStatus (set_program_counter ? s a)
185    | Mov dptr ident ⇒
186       Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
187    ]
188  in
189    s.
190  [2: % ]
191  normalize
192  @ I
193qed.
194
195
196
197definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
198 {{ ps':PseudoStatus | code_memory … ps = code_memory … ps' }
199
200  λticks_of.
201  λs.
202  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
203  let ticks ≝ ticks_of (program_counter ? s) in
204  let s ≝ set_clock ? s (clock ? s + ticks) in
205  let s ≝ set_program_counter ? s pc in
206  let s ≝
207    match instr with
208    [ Instruction instr ⇒
209       Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
210    | Comment cmt ⇒ Some PseudoStatus s
211    | Cost cst ⇒ Some PseudoStatus s
212    | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
213    | Call call ⇒
214      let a ≝ address_of_word_labels s call in
215      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
216      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
217      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
218      let s ≝ write_at_stack_pointer ? s pc_bl in
219      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
220      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
221      let s ≝ write_at_stack_pointer ? s pc_bu in
222        Some PseudoStatus (set_program_counter ? s a)
223    | Mov dptr ident ⇒
224       Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
225    ]
226  in
227    s.
228  [2: % ]
229  normalize
230  @ I
231qed.
232
233
234
235lemma execute_code_memory_unchanged:
236 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
237 #ticks #ps whd in ⊢ (??? (??%))
238 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
239  (program_counter pseudo_assembly_program ps)) #instr #pc
240 whd in ⊢ (??? (??%)) cases instr
241  [ #pre cases pre
242     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
243       cases (split ????) #z1 #z2 %
244     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
245       cases (split ????) #z1 #z2 %
246     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
247       cases (split ????) #z1 #z2 %
248     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
249       [ #x1 whd in ⊢ (??? (??%))
250     | *: cases not_implemented
251     ]
252  | #comment %
253  | #cost %
254  | #label %
255  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
256    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
257    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
258    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
259    (* CSC: ??? *)
260  | #dptr #label (* CSC: ??? *)
261  ]
262  cases not_implemented
263qed.
264
265lemma foo:
266 ∀ticks_of.
267 ∀ps: PseudoStatus.
268  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
269  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
270  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
271  let s' ≝ execute_1 s in
272   s = s'']].
273 #ticks_of #ps
274 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
275 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
276 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
277 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
Note: See TracBrowser for help on using the repository browser.