source: src/ASM/AssemblyProof.ma @ 851

Last change on this file since 851 was 851, checked in by mulligan, 8 years ago

strong foldl added

File size: 22.0 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3
4axiom append_cons_commute:
5  ∀A: Type[0].
6  ∀l, r: list A.
7  ∀h: A.
8    l @ h::r = l @ [h] @ r.
9
10(*
11axiom append_associative:
12  ∀A: Type[0].
13  ∀l, c, r: list A.
14    (l @ c) @ r = l
15*)
16
17let rec foldl_strong
18  (A: Type[0]) (P: list A → Prop) (l: list A)
19  (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]))
20  (prefix: list A) (suffix: list A) (acc: P prefix) on suffix:
21    l = prefix @ suffix → P(prefix @ suffix) ≝
22  match suffix return λl'. l = prefix @ l' → P (prefix @ l') with
23  [ nil ⇒ λprf. ?
24  | cons hd tl ⇒ λprf. ?
25  ].
26  [ > (append_nil ?)
27    @ acc
28  | applyS (foldl_strong A P l H (prefix @ [hd]) tl ? ?)
29    [ @ (H prefix hd tl prf acc)
30    | applyS prf
31    ]
32  ]
33qed.
34 
35    (* > append_cons_commute
36    @
37
38(* RUSSEL **)
39
40axiom addr11_elim:
41  ∀P: Word11 → Prop.
42    (∀b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11: bool.
43      P [[ b1; b2; b3; b4; b5; b6; b7; b8; b9; b10; b11]])→
44        ∀w: Word11. P w.
45
46(* using modified version of matita with hacked ng_refiner/nCicMetaSubst.ml *)
47lemma test:
48  ∀i: instruction.
49  ∃pc.
50  let assembled ≝ assembly1 i in
51  let code_memory ≝ load_code_memory assembled in
52  let fetched ≝ fetch code_memory pc in
53  let 〈instr_pc, ticks〉 ≝ fetched in
54    \fst instr_pc = i.
55  # INSTR
56  %
57  [ @ (zero 16)
58  | cases INSTR
59    [ #ADDR11 cases ADDR11 #ADDRX cases ADDRX
60       [18: #A #P
61        @ (addr11_elim … A)
62        ***********
63        [ normalize
64cases B1
65        normalize; whd;
66     
67   
68      whd
69      normalize in ⊢ (match (?(?(%))?) with [ _ ⇒ ? ])
70      letin xxx ≝ (subaddressing_modeel O [[addr11]] ADDR11)
71      normalize in xxx;
72      normalize in ⊢ (match (?(?(%))?) with [ _ ⇒ ? ])
73    ]
74  ].
75
76include "basics/jmeq.ma".
77
78definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
79definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
80
81coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
82coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
83
84axiom VOID: Type[0].
85axiom assert_false: VOID.
86definition bigbang: ∀A:Type[0].False → VOID → A.
87 #A #abs cases abs
88qed.
89
90coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.
91
92lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
93 #A #P #p cases p #w #q @q
94qed.
95
96(* END RUSSELL **)
97
98(* This establishes the correspondence between pseudo program counters and
99   program counters. It is at the heart of the proof. *)
100(*CSC: code taken from build_maps *)
101definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16))) ≝
102 λinstr_list.
103  foldl ??
104    (λt. λi.
105       match t with
106       [ None ⇒ None ?
107       | Some ppc_pc_map ⇒
108         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
109         let 〈program_counter, sigma_map〉 ≝ pc_map in
110         let 〈label, i〉 ≝ i in
111          match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
112           [ None ⇒ None ?
113           | Some pc_ignore ⇒
114              let 〈pc,ignore〉 ≝ pc_ignore in
115              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
116       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list).
117       
118definition tech_pc_sigma0: pseudo_assembly_program → option nat ≝
119 λinstr_list.
120  match sigma0 instr_list with
121   [ None ⇒ None …
122   | Some result ⇒
123      let 〈ppc,pc_sigma_map〉 ≝ result in
124      let 〈pc, sigma_map〉 ≝ pc_sigma_map in
125       Some … pc ].
126
127definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
128 λinstr_list.
129  match sigma0 instr_list with
130  [ None ⇒ None ?
131  | Some result ⇒
132    let 〈ppc,pc_sigma_map〉 ≝ result in
133    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
134      if gtb pc (2^16) then
135        None ?
136      else
137        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
138
139axiom policy_ok: ∀p. sigma_safe p ≠ None ….
140
141definition sigma: pseudo_assembly_program → Word → Word ≝
142 λp.
143  match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
144   [ None ⇒ λabs. ⊥
145   | Some r ⇒ λ_.r] (policy_ok p).
146 cases abs //
147qed.
148
149(*
150definition build_maps' ≝
151  λpseudo_program.
152  let 〈preamble,instr_list〉 ≝ pseudo_program in
153  let result ≝
154   foldl
155    ((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16)))
156    (option Identifier × pseudo_instruction)
157    (λt,i.
158      let 〈labels, pc_costs〉 ≝ t in
159      let 〈program_counter, costs〉 ≝ pc_costs in
160       let 〈label, i'〉 ≝ i in
161       let labels ≝
162         match label with
163         [ None ⇒ labels
164         | Some label ⇒
165           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
166             insert ? ? label program_counter_bv labels
167         ]
168       in
169         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
170         [ None ⇒
171            let dummy ≝ 〈labels,pc_costs〉 in
172             dummy
173         | Some construct ⇒ 〈labels, construct〉
174         ]
175    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
176  in
177   let 〈labels, pc_costs〉 ≝ result in
178   let 〈pc, costs〉 ≝ pc_costs in
179    〈labels, costs〉.
180
181(*
182notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
183 with precedence 10
184for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
185*)
186
187lemma build_maps_ok:
188 ∀p:pseudo_assembly_program.
189  let 〈labels,costs〉 ≝ build_maps' p in
190   ∀pc.
191    (nat_of_bitvector … pc) < length … (\snd p) →
192     lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
193 #p cases p #preamble #instr_list
194  elim instr_list
195   [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
196   | #hd #tl #IH
197    whd in ⊢ (match % with [ _ ⇒ ?])
198   ]
199qed.
200*)
201
202(*
203lemma list_elim_rev:
204 ∀A:Type[0].∀P:list A → Prop.
205  P [ ] → (∀n,l. length l = n → P l → 
206  P [ ] → (∀l,a. P l → P (l@[a])) →
207   ∀l. P l.
208 #A #P
209qed.*)
210
211lemma length_append:
212 ∀A.∀l1,l2:list A.
213  |l1 @ l2| = |l1| + |l2|.
214 #A #l1 elim l1
215  [ //
216  | #hd #tl #IH #l2 normalize <IH //]
217qed.
218
219lemma rev_preserves_length:
220 ∀A.∀l. length … (rev A l) = length … l.
221  #A #l elim l
222   [ %
223   | #hd #tl #IH normalize >length_append normalize /2/ ]
224qed.
225
226lemma rev_append:
227 ∀A.∀l1,l2.
228  rev A (l1@l2) = rev A l2 @ rev A l1.
229 #A #l1 elim l1 normalize //
230qed.
231 
232lemma rev_rev: ∀A.∀l. rev … (rev A l) = l.
233 #A #l elim l
234  [ //
235  | #hd #tl #IH normalize >rev_append normalize // ]
236qed.
237
238lemma split_len_Sn:
239 ∀A:Type[0].∀l:list A.∀len.
240  length … l = S len →
241   Σl'.Σa. l = l'@[a] ∧ length … l' = len.
242 #A #l elim l
243  [ normalize #len #abs destruct
244  | #hd #tl #IH #len
245    generalize in match (rev_rev … tl)
246    cases (rev A tl) in ⊢ (??%? → ?)
247     [ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/ 
248     | #a #l' #H <H normalize #EQ
249      %[@(hd::rev … l')] %[@a] % //
250      >length_append in EQ #EQ normalize in EQ; normalize;
251      generalize in match (injective_S … EQ) #EQ2 /2/ ]]
252qed.
253
254lemma list_elim_rev:
255 ∀A:Type[0].∀P:list A → Type[0].
256  P [ ] → (∀l,a. P l → P (l@[a])) →
257   ∀l. P l.
258 #A #P #H1 #H2 #l
259 generalize in match (refl … (length … l))
260 generalize in ⊢ (???% → ?) #n generalize in match l
261 elim n
262  [ #L cases L [ // | #x #w #abs (normalize in abs) @⊥ // ]
263  | #m #IH #L #EQ
264    cases (split_len_Sn … EQ) #l' * #a * /3/ ]
265qed.
266
267axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
268axiom prefix_of_append:
269 ∀A:Type[0].∀l,l1,l2:list A.
270  is_prefix … l l1 → is_prefix … l (l1@l2).
271
272record Propify (A:Type[0]) : Prop ≝ { in_propify: A }.
273
274definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
275 λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
276
277definition app ≝
278 λA:Type[0].λl1:Propify (list A).λl2:list A.
279  match l1 with
280   [ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ].
281
282lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
283 #A * /3/
284qed.
285
286lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
287 #A * #l1 normalize //
288qed.
289
290let rec foldli (A: Type[0]) (B: Propify (list A) → Type[0])
291 (f: ∀prefix. B prefix → ∀x.B (app … prefix [x]))
292 (prefix: Propify (list A)) (b: B prefix) (l: list A) on l :
293 B (app … prefix l) ≝
294  match l with
295  [ nil ⇒ ? (* b *)
296  | cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
297  ].
298 [ applyS b
299 | <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ]
300qed.
301
302(*
303let rec foldli (A: Type[0]) (B: list A → Type[0]) (f: ∀prefix. B prefix → ∀x. B (prefix@[x]))
304 (prefix: list A) (b: B prefix) (l: list A) on l : B (prefix@l) ≝
305  match l with
306  [ nil ⇒ ? (* b *)
307  | cons hd tl ⇒
308     ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
309  ].
310 [ applyS b
311 | applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ]
312qed.
313*)
314
315definition foldll:
316 ∀A:Type[0].∀B: Propify (list A) → Type[0].
317  (∀prefix. B prefix → ∀x. B (app … prefix [x])) →
318   B (mk_Propify … []) → ∀l: list A. B (mk_Propify … l)
319 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
320
321definition build_maps' ≝
322  λpseudo_program.
323  let 〈preamble,instr_list〉 ≝ pseudo_program in
324  let result ≝
325   foldl
326    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
327          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
328           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
329    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
330          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
331           is_prefix ? instr_list_prefix' instr_list →
332           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
333    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
334          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
335           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
336     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
337          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
338           is_prefix ? instr_list_prefix' instr_list →
339           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
340      let 〈labels, pc_costs〉 ≝ t in
341      let 〈program_counter, costs〉 ≝ pc_costs in
342       let 〈label, i'〉 ≝ i in
343       let labels ≝
344         match label with
345         [ None ⇒ labels
346         | Some label ⇒
347           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
348             insert ? ? label program_counter_bv labels
349         ]
350       in
351         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
352         [ None ⇒
353            let dummy ≝ 〈labels,pc_costs〉 in
354              dummy
355         | Some construct ⇒ 〈labels, construct〉
356         ]
357    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
358  in
359   let 〈labels, pc_costs〉 ≝ result in
360   let 〈pc, costs〉 ≝ pc_costs in
361    〈labels, costs〉.
362
363definition build_maps' ≝
364  λpseudo_program.
365  let 〈preamble,instr_list〉 ≝ pseudo_program in
366  let result ≝
367   foldl
368    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
369          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
370           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
371    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
372          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
373           is_prefix ? instr_list_prefix' instr_list →
374           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
375    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
376          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
377           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
378     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
379          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
380           is_prefix ? instr_list_prefix' instr_list →
381           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
382      let 〈labels, pc_costs〉 ≝ t in
383      let 〈program_counter, costs〉 ≝ pc_costs in
384       let 〈label, i'〉 ≝ i in
385       let labels ≝
386         match label with
387         [ None ⇒ labels
388         | Some label ⇒
389           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
390             insert ? ? label program_counter_bv labels
391         ]
392       in
393         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
394         [ None ⇒
395            let dummy ≝ 〈labels,pc_costs〉 in
396              dummy
397         | Some construct ⇒ 〈labels, construct〉
398         ]
399    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
400  in
401   let 〈labels, pc_costs〉 ≝ result in
402   let 〈pc, costs〉 ≝ pc_costs in
403    〈labels, costs〉.
404 [4: @(list_elim_rev ?
405       (λinstr_list. list (
406        (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
407          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
408           is_prefix ? instr_list_prefix' instr_list →
409           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)))
410       ?? instr_list) (* CSC: BAD ORDER FOR CODE EXTRACTION *)
411      [ @[ ]
412      | #l' #a #limage %2
413        [ %[@a] #PREFIX #PREFIX_OK
414        | (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN
415             THE INDUCTION HYPOTHESIS INSTEAD *)
416          elim limage
417           [ %1
418           | #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K3
419             @K1 @(prefix_of_append ???? K3)
420           ] 
421        ]
422       
423       
424     
425 
426  cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
427     % [@ (LIST_PREFIX @ [i])] %
428      [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
429      | (* DOABLE IN PRINCIPLE *)
430      ]
431 | (* assert false case *)
432 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
433 |   
434
435let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
436                       (encoding: list Byte) on encoding: Prop ≝
437  match encoding with
438  [ nil ⇒ final_pc = pc
439  | cons hd tl ⇒
440    let 〈new_pc, byte〉 ≝ next code_memory pc in
441      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
442  ].
443
444definition assembly_specification:
445  ∀assembly_program: pseudo_assembly_program.
446  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
447  λpseudo_assembly_program.
448  λcode_mem.
449    ∀pc: Word.
450      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
451      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
452      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
453      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
454      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
455       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
456      match pre_assembled with
457       [ None ⇒ True
458       | Some pc_code ⇒
459          let 〈new_pc,code〉 ≝ pc_code in
460           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
461
462axiom assembly_meets_specification:
463  ∀pseudo_assembly_program.
464    match assembly pseudo_assembly_program with
465    [ None ⇒ True
466    | Some code_mem_cost ⇒
467      let 〈code_mem, cost〉 ≝ code_mem_cost in
468        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
469    ].
470(*
471  # PROGRAM
472  [ cases PROGRAM
473    # PREAMBLE
474    # INSTR_LIST
475    elim INSTR_LIST
476    [ whd
477      whd in ⊢ (∀_. %)
478      # PC
479      whd
480    | # INSTR
481      # INSTR_LIST_TL
482      # H
483      whd
484      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
485    ]
486  | cases not_implemented
487  ] *)
488
489definition status_of_pseudo_status: PseudoStatus → option Status ≝
490 λps.
491  let pap ≝ code_memory … ps in
492   match assembly pap with
493    [ None ⇒ None …
494    | Some p ⇒
495       let cm ≝ load_code_memory (\fst p) in
496       let pc ≝ sigma' pap (program_counter ? ps) in
497        Some …
498         (mk_PreStatus (BitVectorTrie Byte 16)
499           cm
500           (low_internal_ram … ps)
501           (high_internal_ram … ps)
502           (external_ram … ps)
503           pc
504           (special_function_registers_8051 … ps)
505           (special_function_registers_8052 … ps)
506           (p1_latch … ps)
507           (p3_latch … ps)
508           (clock … ps)) ].
509
510definition write_at_stack_pointer':
511 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
512  λM: Type[0].
513  λs: PreStatus M.
514  λv: Byte.
515    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
516    let bit_zero ≝ get_index_v… nu O ? in
517    let bit_1 ≝ get_index_v… nu 1 ? in
518    let bit_2 ≝ get_index_v… nu 2 ? in
519    let bit_3 ≝ get_index_v… nu 3 ? in
520      if bit_zero then
521        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
522                              v (low_internal_ram ? s) in
523          set_low_internal_ram ? s memory
524      else
525        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
526                              v (high_internal_ram ? s) in
527          set_high_internal_ram ? s memory.
528  [ cases l0 %
529  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
530qed.
531
532definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
533 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
534
535  λticks_of.
536  λs.
537  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
538  let ticks ≝ ticks_of (program_counter ? s) in
539  let s ≝ set_clock ? s (clock ? s + ticks) in
540  let s ≝ set_program_counter ? s pc in
541    match instr with
542    [ Instruction instr ⇒
543       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
544    | Comment cmt ⇒ s
545    | Cost cst ⇒ s
546    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
547    | Call call ⇒
548      let a ≝ address_of_word_labels s call in
549      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
550      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
551      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
552      let s ≝ write_at_stack_pointer' ? s pc_bl in
553      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
554      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
555      let s ≝ write_at_stack_pointer' ? s pc_bu in
556        set_program_counter ? s a
557    | Mov dptr ident ⇒
558       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
559    ].
560 [
561 |2,3,4: %
562 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
563 |
564 | %
565 ]
566 cases not_implemented
567qed.
568
569(*
570lemma execute_code_memory_unchanged:
571 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
572 #ticks #ps whd in ⊢ (??? (??%))
573 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
574  (program_counter pseudo_assembly_program ps)) #instr #pc
575 whd in ⊢ (??? (??%)) cases instr
576  [ #pre cases pre
577     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
578       cases (split ????) #z1 #z2 %
579     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
580       cases (split ????) #z1 #z2 %
581     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
582       cases (split ????) #z1 #z2 %
583     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
584       [ #x1 whd in ⊢ (??? (??%))
585     | *: cases not_implemented
586     ]
587  | #comment %
588  | #cost %
589  | #label %
590  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
591    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
592    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
593    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
594    (* CSC: ??? *)
595  | #dptr #label (* CSC: ??? *)
596  ]
597  cases not_implemented
598qed.
599*)
600
601lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
602 ∀ps,ps': PseudoStatus.
603  code_memory … ps = code_memory … ps' →
604   match status_of_pseudo_status ps with
605    [ None ⇒ status_of_pseudo_status ps' = None …
606    | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
607    ].
608 #ps #ps' #H whd in ⊢ (mat
609 ch % with [ _ ⇒ ? | _ ⇒ ? ])
610 generalize in match (refl … (assembly (code_memory … ps)))
611 cases (assembly ?) in ⊢ (???% → %)
612  [ #K whd whd in ⊢ (??%?) <H >K %
613  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
614qed.*)
615
616let rec encoding_check' (code_memory: BitVectorTrie Byte 16) (pc: Word) (encoding: list Byte) on encoding: Prop ≝
617  match encoding with
618  [ nil ⇒ True
619  | cons hd tl ⇒
620    let 〈new_pc, byte〉 ≝ next code_memory pc in
621      hd = byte ∧ encoding_check' code_memory new_pc tl
622  ].
623
624(* prove later *)
625axiom test:
626  ∀pc: Word.
627  ∀code_memory: BitVectorTrie Byte 16.
628  ∀i: instruction.
629    let assembled ≝ assembly1 i in
630      encoding_check' code_memory pc assembled →
631        let 〈instr_pc, ignore〉 ≝ fetch code_memory pc in
632        let 〈instr, pc〉 ≝ instr_pc in
633          instr = i.
634 
635lemma main_thm:
636 ∀ticks_of.
637 ∀ps: PseudoStatus.
638  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
639  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
640  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
641  let s' ≝ execute_1 s in
642   s = s'']].
643 #ticks_of #ps
644 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
645 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
646 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
647 generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))
648 
649 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
Note: See TracBrowser for help on using the repository browser.