source: src/ASM/AssemblyProof.ma @ 840

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

sigma defined

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