source: src/ASM/AssemblyProof.ma @ 868

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

more changes

File size: 36.0 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3
4(* RUSSEL **)
5
6include "basics/jmeq.ma".
7
8notation > "hvbox(a break ≃ b)"
9  non associative with precedence 45
10for @{ 'jmeq ? $a ? $b }.
11
12notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
13  non associative with precedence 45
14for @{ 'jmeq $t $a $u $b }.
15
16interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
17
18lemma eq_to_jmeq:
19  ∀A: Type[0].
20  ∀x, y: A.
21    x = y → x ≃ y.
22  //
23qed.
24
25definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
26definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
27
28coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
29coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
30
31axiom VOID: Type[0].
32axiom assert_false: VOID.
33definition bigbang: ∀A:Type[0].False → VOID → A.
34 #A #abs cases abs
35qed.
36
37coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.
38
39lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
40 #A #P #p cases p #w #q @q
41qed.
42
43lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
44 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
45qed.
46
47coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
48
49(* END RUSSELL **)
50
51let rec foldl_strong_internal
52  (A: Type[0]) (P: list A → Type[0]) (l: list A)
53  (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]))
54  (prefix: list A) (suffix: list A) (acc: P prefix) on suffix:
55    l = prefix @ suffix → P(prefix @ suffix) ≝
56  match suffix return λl'. l = prefix @ l' → P (prefix @ l') with
57  [ nil ⇒ λprf. ?
58  | cons hd tl ⇒ λprf. ?
59  ].
60  [ > (append_nil ?)
61    @ acc
62  | applyS (foldl_strong_internal A P l H (prefix @ [hd]) tl ? ?)
63    [ @ (H prefix hd tl prf acc)
64    | applyS prf
65    ]
66  ]
67qed.
68
69definition foldl_strong ≝
70  λA: Type[0].
71  λP: list A → Type[0].
72  λl: list A.
73  λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
74  λacc: P [ ].
75    foldl_strong_internal A P l H [ ] l acc (refl …).
76
77definition bit_elim: ∀P: bool → bool. bool ≝
78  λP.
79    P true ∧ P false.
80
81let rec bitvector_elim_internal
82  (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝
83  match m return λm. m ≤ n → BitVector (n - m) → bool with
84  [ O    ⇒ λprf1. λprefix. P ?
85  | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
86  ].
87  [ applyS prefix
88  | letin res ≝ (bit ::: prefix)
89    < (minus_S_S ? ?)
90    > (minus_Sn_m ? ?)
91    [ @ res
92    | @ prf2
93    ]
94  | /2/
95  ].
96qed.
97
98definition bitvector_elim ≝
99  λn: nat.
100  λP: BitVector n → bool.
101    bitvector_elim_internal n P n ? ?.
102  [ @ (le_n ?)
103  | < (minus_n_n ?)
104    @ [[ ]]
105  ]
106qed.
107
108axiom vector_associative_append:
109  ∀A: Type[0].
110  ∀n, m, o:  nat.
111  ∀v: Vector A n.
112  ∀q: Vector A m.
113  ∀r: Vector A o.
114    ((v @@ q) @@ r)
115    ≃
116    (v @@ (q @@ r)).
117       
118lemma vector_cons_append:
119  ∀A: Type[0].
120  ∀n: nat.
121  ∀e: A.
122  ∀v: Vector A n.
123    e ::: v = [[ e ]] @@ v.
124  # A # N # E # V
125  elim V
126  [ normalize %
127  | # NN # AA # VV # IH
128    normalize
129    %
130  ]
131qed.
132
133lemma super_rewrite2:
134 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
135  ∀P: ∀m. Vector A m → Prop.
136   n=m → v1 ≃ v2 → P n v1 → P m v2.
137 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
138qed.
139
140lemma mem_middle_vector:
141  ∀A: Type[0].
142  ∀m, o: nat.
143  ∀eq: A → A → bool.
144  ∀reflex: ∀a. eq a a = true.
145  ∀p: Vector A m.
146  ∀a: A.
147  ∀r: Vector A o.
148    mem A eq ? (p@@(a:::r)) a = true.
149  # A # M # O # EQ # REFLEX # P # A
150  elim P
151  [ normalize
152    > (REFLEX A)
153    normalize
154    # H
155    %
156  | # NN # AA # PP # IH
157    normalize
158    cases (EQ A AA) //
159     @ IH
160  ]
161qed.
162
163lemma mem_monotonic_wrt_append:
164  ∀A: Type[0].
165  ∀m, o: nat.
166  ∀eq: A → A → bool.
167  ∀reflex: ∀a. eq a a = true.
168  ∀p: Vector A m.
169  ∀a: A.
170  ∀r: Vector A o.
171    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
172  # A # M # O # EQ # REFLEX # P # A
173  elim P
174  [ #R #H @H
175  | #NN #AA # PP # IH #R #H
176    normalize
177    cases (EQ A AA)
178    [ normalize %
179    | @ IH @ H
180    ]
181  ]
182qed.
183
184lemma subvector_multiple_append:
185  ∀A: Type[0].
186  ∀o, n: nat.
187  ∀eq: A → A → bool.
188  ∀refl: ∀a. eq a a = true.
189  ∀h: Vector A o.
190  ∀v: Vector A n.
191  ∀m: nat.
192  ∀q: Vector A m.
193    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
194  # A # O # N # EQ # REFLEX # H # V
195  elim V
196  [ normalize
197    # M # V %
198  | # NN # AA # VV # IH # MM # QQ
199    change with (bool_to_Prop (andb ??))
200    cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true)
201    [
202    | # HH > HH
203      > (vector_cons_append ? ? AA VV)
204      change with (bool_to_Prop (subvector_with ??????))
205      @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ??
206        (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS)))
207        ?
208        (vector_associative_append A ? ? ? QQ [[AA]] VV))
209      [ >associative_plus //
210      | @IH ]
211    ]
212    @(mem_monotonic_wrt_append)
213    [ @ REFLEX
214    | @(mem_monotonic_wrt_append)
215      [ @ REFLEX
216      | normalize
217        > REFLEX
218        normalize
219        %
220      ]
221    ]
222qed.
223
224lemma vector_cons_empty:
225  ∀A: Type[0].
226  ∀n: nat.
227  ∀v: Vector A n.
228    [[ ]] @@ v = v.
229  # A # N # V
230  elim V
231  [ normalize %
232  | # NN # HH # VV #H %
233  ]
234qed.
235
236corollary subvector_hd_tl:
237  ∀A: Type[0].
238  ∀o: nat.
239  ∀eq: A → A → bool.
240  ∀refl: ∀a. eq a a = true.
241  ∀h: A.
242  ∀v: Vector A o.
243    bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
244  # A # O # EQ # REFLEX # H # V
245  > (vector_cons_append A ? H V)
246  < (vector_cons_empty A ? ([[H]] @@ V))
247  @ (subvector_multiple_append A ? ? EQ REFLEX [[]] V ? [[ H ]])
248qed.
249
250lemma eq_a_reflexive:
251  ∀a. eq_a a a = true.
252  # A
253  cases A
254  %
255qed.
256
257lemma is_in_monotonic_wrt_append:
258  ∀m, n: nat.
259  ∀p: Vector addressing_mode_tag m.
260  ∀q: Vector addressing_mode_tag n.
261  ∀to_search: addressing_mode.
262    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
263  # M # N # P # Q # TO_SEARCH
264  # H
265  elim Q
266  [ normalize
267    @ H
268  | # NN # PP # QQ # IH
269    normalize
270    cases (is_a PP TO_SEARCH)
271    [ normalize
272      %
273    | normalize
274      normalize in IH
275      @ IH
276    ]
277  ]
278qed.
279
280corollary is_in_hd_tl:
281  ∀to_search: addressing_mode.
282  ∀hd: addressing_mode_tag.
283  ∀n: nat.
284  ∀v: Vector addressing_mode_tag n.
285    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
286  # TO_SEARCH # HD # N # V
287  elim V
288  [ # H
289    normalize in H;
290    cases H
291  | # NN # HHD # VV # IH # HH
292    > vector_cons_append
293    > (vector_cons_append ? ? HHD VV)
294    @ (is_in_monotonic_wrt_append ? 1 ([[HHD]]@@VV) [[HD]] TO_SEARCH)
295    @ HH
296  ]
297qed.
298 
299let rec list_addressing_mode_tags_elim
300  (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
301  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
302   (l → bool) → bool ] with
303  [ VEmpty      ⇒  true 
304  | VCons len hd tl ⇒ λP.
305    let process_hd ≝
306      match hd return λhd. ∀P: hd:::tl → bool. bool with
307      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
308      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
309      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
310      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
311      | acc_a ⇒ λP.P ACC_A
312      | acc_b ⇒ λP.P ACC_B
313      | dptr ⇒ λP.P DPTR
314      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
315      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
316      | acc_dptr ⇒ λP.P ACC_DPTR
317      | acc_pc ⇒ λP.P ACC_PC
318      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
319      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
320      | carry ⇒ λP.P CARRY
321      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
322      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
323      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
324      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
325      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
326      ]
327    in
328      andb (process_hd P)
329       (match len return λx. x = len → bool with
330         [ O ⇒ λprf. true
331         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
332  ].
333  try %
334  [ 2: cases (sym_eq ??? prf); @tl
335  | cases prf in tl H; #tl
336    normalize in ⊢ (∀_: %. ?)
337    # H
338    whd
339    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
340    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
341qed.
342
343definition product_elim ≝
344  λm, n: nat.
345  λv: Vector addressing_mode_tag (S m).
346  λq: Vector addressing_mode_tag (S n).
347  λP: (Vector addressing_mode_tag (S m) × (Vector addressing_mode_tag (S n))) → bool.
348    P 〈v, q〉.
349
350axiom union_elim:
351  ∀m, n: nat. ((Vector addressing_mode_tag m ⊎ Vector addressing_mode_tag n) → bool) → bool.
352
353definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
354  λP.
355    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧
356    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧
357    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧
358    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧
359    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧
360    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧
361    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧
362    list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. P (DJNZ ? ? addr)) ∧
363    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧
364    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧
365    P (DA ? ACC_A) ∧
366    P (JC ? ?) ∧
367    P (JNC ? ?) ∧
368    P (JZ ? ?) ∧
369    P (JNZ ? ?) ∧
370    bitvector_elim 8 (λx. P (JB ? (BIT_ADDR x))). ∧
371    P (JNB ? [[ bit_addr ]] ?) ∧
372    P (JBC ? [[ bit_addr ]] ?) ∧
373    P (RL ? ACC_A).
374   
375   
376   
377   
378   
379   
380    list_addressing_mode_tags_elim ? [[ data ]] (λaddr. P (CJNE ? (inl ? ? (〈ACC_A, addr)).
381
382    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ANL ? addr)) ∧
383    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ORL ? addr)) ∧
384    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XRL ? addr)) ∧
385    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RL ? addr)) ∧
386    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RLC ? addr)) ∧
387    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RR ? addr)) ∧
388    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RRC ? addr)) ∧
389    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SWAP ? addr)) ∧
390    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOV ? addr)) ∧
391    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOVX ? addr)) ∧
392    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SETB ? addr)) ∧
393    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (PUSH ? addr)) ∧
394    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (POP ? addr)) ∧
395    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XCH ? addr)) ∧
396    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XCHD ? addr)) ∧
397    P (RET ?) ∧
398    P (RETI ?) ∧
399    P (NOP ?).
400 
401
402definition instruction_elim: ∀P: instruction → bool. bool.
403 
404 
405lemma instruction_elim_correct:
406  ∀i: instruction.
407  ∀P: instruction → bool.
408    instruction_elim P = true → ∀j. P j = true.
409 
410lemma test:
411  ∀i: instruction.
412  ∃pc.
413  let assembled ≝ assembly1 i in
414  let code_memory ≝ load_code_memory assembled in
415  let fetched ≝ fetch code_memory pc in
416  let 〈instr_pc, ticks〉 ≝ fetched in
417    \fst instr_pc = i.
418  # INSTR
419  @ (ex_intro ?)
420  [ @ (zero 16)
421  | @ (instruction_elim INSTR)
422  ].
423 
424(* This establishes the correspondence between pseudo program counters and
425   program counters. It is at the heart of the proof. *)
426(*CSC: code taken from build_maps *)
427definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16))) ≝
428 λinstr_list.
429  foldl ??
430    (λt. λi.
431       match t with
432       [ None ⇒ None ?
433       | Some ppc_pc_map ⇒
434         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
435         let 〈program_counter, sigma_map〉 ≝ pc_map in
436         let 〈label, i〉 ≝ i in
437          match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
438           [ None ⇒ None ?
439           | Some pc_ignore ⇒
440              let 〈pc,ignore〉 ≝ pc_ignore in
441              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
442       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list).
443       
444definition tech_pc_sigma0: pseudo_assembly_program → option (nat × (BitVectorTrie Word 16)) ≝
445 λinstr_list.
446  match sigma0 instr_list with
447   [ None ⇒ None …
448   | Some result ⇒
449      let 〈ppc,pc_sigma_map〉 ≝ result in
450       Some … pc_sigma_map ].
451
452definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
453 λinstr_list.
454  match sigma0 instr_list with
455  [ None ⇒ None ?
456  | Some result ⇒
457    let 〈ppc,pc_sigma_map〉 ≝ result in
458    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
459      if gtb pc (2^16) then
460        None ?
461      else
462        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
463
464axiom policy_ok: ∀p. sigma_safe p ≠ None ….
465
466definition sigma: pseudo_assembly_program → Word → Word ≝
467 λp.
468  match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
469   [ None ⇒ λabs. ⊥
470   | Some r ⇒ λ_.r] (policy_ok p).
471 cases abs //
472qed.
473
474lemma length_append:
475 ∀A.∀l1,l2:list A.
476  |l1 @ l2| = |l1| + |l2|.
477 #A #l1 elim l1
478  [ //
479  | #hd #tl #IH #l2 normalize <IH //]
480qed.
481
482let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
483 match l with
484  [ nil ⇒ true
485  | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].
486
487lemma does_not_occur_None:
488 ∀id,i,list_instr.
489  does_not_occur id (list_instr@[〈None …,i〉]) =
490  does_not_occur id list_instr.
491 #id #i #list_instr elim list_instr
492  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH %]
493qed.
494
495let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
496 match l with
497  [ nil ⇒ false
498  | cons hd tl ⇒
499     if instruction_matches_identifier id hd then
500      does_not_occur id tl
501     else
502      occurs_exactly_once id tl ].
503
504lemma occurs_exactly_once_None:
505 ∀id,i,list_instr.
506  occurs_exactly_once id (list_instr@[〈None …,i〉]) =
507  occurs_exactly_once id list_instr.
508 #id #i #list_instr elim list_instr
509  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %]
510qed.
511
512coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
513
514lemma index_of_internal_None: ∀i,id,instr_list,n.
515 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
516  index_of_internal ? (instruction_matches_identifier id) instr_list n =
517   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
518 #i #id #instr_list elim instr_list
519  [ #n #abs whd in abs; cases abs
520  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
521    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
522    [ #H %
523    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
524      [ #_ % | #abs cases abs ]]]
525qed.
526
527lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
528 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
529  address_of_word_labels_code_mem instr_list id =
530  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
531 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
532 >(index_of_internal_None … H) %
533qed.
534
535axiom tech_pc_sigma0_append:
536 ∀preamble,instr_list,prefix,label,i,pc',code,pc,costs,costs'.
537  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
538   construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
539    tech_pc_sigma0 〈preamble,prefix@[〈label,i〉]〉 = Some … 〈pc',costs'〉.
540
541axiom tech_pc_sigma0_append_None:
542 ∀preamble,instr_list,prefix,i,pc,costs.
543  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
544   construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None …
545    → False.
546
547definition build_maps' ≝
548  λpseudo_program.
549  let 〈preamble,instr_list〉 ≝ pseudo_program in
550  let result ≝
551   foldl_strong
552    (option Identifier × pseudo_instruction)
553    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
554      let pre' ≝ 〈preamble,pre〉 in
555      let 〈labels,pc_costs〉 ≝ res in
556       tech_pc_sigma0 pre' = Some … pc_costs ∧
557       ∀id. occurs_exactly_once id pre →
558        lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id))
559    instr_list
560    (λprefix,i,tl,prf,t.
561      let 〈labels, pc_costs〉 ≝ t in
562      let 〈program_counter, costs〉 ≝ pc_costs in
563       let 〈label, i'〉 ≝ i in
564       let labels ≝
565         match label with
566         [ None ⇒ labels
567         | Some label ⇒
568           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
569             insert ? ? label program_counter_bv labels
570         ]
571       in
572         match construct_costs 〈preamble,instr_list〉 program_counter (λx. zero ?) (λx. zero ?) costs i' with
573         [ None ⇒
574            let dummy ≝ 〈labels,pc_costs〉 in
575             dummy
576         | Some construct ⇒ 〈labels, construct〉
577         ]
578    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉
579  in
580   let 〈labels, pc_costs〉 ≝ result in
581   let 〈pc, costs〉 ≝ pc_costs in
582    〈labels, costs〉.
583 [3: whd % // #id normalize in ⊢ (% → ?) #abs @⊥ //
584 | whd cases construct in p3 #PC #CODE #JMEQ %
585    [ @(tech_pc_sigma0_append ??????????? (jmeq_to_eq ??? JMEQ)) | #id #Hid ]
586 | (* dummy case *) @⊥
587   @(tech_pc_sigma0_append_None ?? prefix ???? (jmeq_to_eq ??? p3)) ]
588 [*: generalize in match (sig2 … t) whd in ⊢ (% → ?)
589     >p whd in ⊢ (% → ?) >p1 * #IH0 #IH1 >IH0 // ]
590 whd in ⊢ (??(????%?)?) -labels1;
591 cases label in Hid
592  [ #Hid whd in ⊢ (??(????%?)?) >IH1 -IH1
593     [ >(address_of_word_labels_code_mem_None … Hid)
594       (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *)
595     | whd in Hid >occurs_exactly_once_None in Hid // ]
596  | -label #label #Hid whd in ⊢ (??(????%?)?)
597   
598  ]
599qed.
600
601(*
602(*
603notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
604 with precedence 10
605for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
606*)
607
608lemma build_maps_ok:
609 ∀p:pseudo_assembly_program.
610  let 〈labels,costs〉 ≝ build_maps' p in
611   ∀pc.
612    (nat_of_bitvector … pc) < length … (\snd p) →
613     lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
614 #p cases p #preamble #instr_list
615  elim instr_list
616   [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
617   | #hd #tl #IH
618    whd in ⊢ (match % with [ _ ⇒ ?])
619   ]
620qed.
621*)
622
623(*
624lemma list_elim_rev:
625 ∀A:Type[0].∀P:list A → Prop.
626  P [ ] → (∀n,l. length l = n → P l → 
627  P [ ] → (∀l,a. P l → P (l@[a])) →
628   ∀l. P l.
629 #A #P
630qed.*)
631
632lemma rev_preserves_length:
633 ∀A.∀l. length … (rev A l) = length … l.
634  #A #l elim l
635   [ %
636   | #hd #tl #IH normalize >length_append normalize /2/ ]
637qed.
638
639lemma rev_append:
640 ∀A.∀l1,l2.
641  rev A (l1@l2) = rev A l2 @ rev A l1.
642 #A #l1 elim l1 normalize //
643qed.
644 
645lemma rev_rev: ∀A.∀l. rev … (rev A l) = l.
646 #A #l elim l
647  [ //
648  | #hd #tl #IH normalize >rev_append normalize // ]
649qed.
650
651lemma split_len_Sn:
652 ∀A:Type[0].∀l:list A.∀len.
653  length … l = S len →
654   Σl'.Σa. l = l'@[a] ∧ length … l' = len.
655 #A #l elim l
656  [ normalize #len #abs destruct
657  | #hd #tl #IH #len
658    generalize in match (rev_rev … tl)
659    cases (rev A tl) in ⊢ (??%? → ?)
660     [ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/ 
661     | #a #l' #H <H normalize #EQ
662      %[@(hd::rev … l')] %[@a] % //
663      >length_append in EQ #EQ normalize in EQ; normalize;
664      generalize in match (injective_S … EQ) #EQ2 /2/ ]]
665qed.
666
667lemma list_elim_rev:
668 ∀A:Type[0].∀P:list A → Type[0].
669  P [ ] → (∀l,a. P l → P (l@[a])) →
670   ∀l. P l.
671 #A #P #H1 #H2 #l
672 generalize in match (refl … (length … l))
673 generalize in ⊢ (???% → ?) #n generalize in match l
674 elim n
675  [ #L cases L [ // | #x #w #abs (normalize in abs) @⊥ // ]
676  | #m #IH #L #EQ
677    cases (split_len_Sn … EQ) #l' * #a * /3/ ]
678qed.
679
680axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
681axiom prefix_of_append:
682 ∀A:Type[0].∀l,l1,l2:list A.
683  is_prefix … l l1 → is_prefix … l (l1@l2).
684axiom prefix_reflexive: ∀A,l. is_prefix A l l.
685axiom nil_prefix: ∀A,l. is_prefix A [ ] l.
686
687record Propify (A:Type[0]) : Type[0] (*Prop*) ≝ { in_propify: A }.
688
689definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
690 λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
691
692definition app ≝
693 λA:Type[0].λl1:Propify (list A).λl2:list A.
694  match l1 with
695   [ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ].
696
697lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
698 #A * /3/
699qed.
700
701lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
702 #A * #l1 normalize //
703qed.
704
705let rec foldli (A: Type[0]) (B: Propify (list A) → Type[0])
706 (f: ∀prefix. B prefix → ∀x.B (app … prefix [x]))
707 (prefix: Propify (list A)) (b: B prefix) (l: list A) on l :
708 B (app … prefix l) ≝
709  match l with
710  [ nil ⇒ ? (* b *)
711  | cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
712  ].
713 [ applyS b
714 | <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ]
715qed.
716
717(*
718let rec foldli (A: Type[0]) (B: list A → Type[0]) (f: ∀prefix. B prefix → ∀x. B (prefix@[x]))
719 (prefix: list A) (b: B prefix) (l: list A) on l : B (prefix@l) ≝
720  match l with
721  [ nil ⇒ ? (* b *)
722  | cons hd tl ⇒
723     ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
724  ].
725 [ applyS b
726 | applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ]
727qed.
728*)
729
730definition foldll:
731 ∀A:Type[0].∀B: Propify (list A) → Type[0].
732  (∀prefix. B prefix → ∀x. B (app … prefix [x])) →
733   B (mk_Propify … []) → ∀l: list A. B (mk_Propify … l)
734 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
735
736axiom is_pprefix: ∀A:Type[0]. Propify (list A) → list A → Prop.
737axiom pprefix_of_append:
738 ∀A:Type[0].∀l,l1,l2.
739  is_pprefix A l l1 → is_pprefix A l (l1@l2).
740axiom pprefix_reflexive: ∀A,l. is_pprefix A (mk_Propify … l) l.
741axiom nil_pprefix: ∀A,l. is_pprefix A (mk_Propify … [ ]) l.
742
743
744axiom foldll':
745 ∀A:Type[0].∀l: list A.
746  ∀B: ∀prefix:Propify (list A). is_pprefix ? prefix l → Type[0].
747  (∀prefix,proof. B prefix proof → ∀x,proof'. B (app … prefix [x]) proof') →
748   B (mk_Propify … [ ]) (nil_pprefix …) → B (mk_Propify … l) (pprefix_reflexive … l).
749 #A #l #B
750 generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH
751 
752 
753  #H #acc
754 @foldll
755  [
756  |
757  ]
758 
759 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
760
761
762(*
763record subset (A:Type[0]) (P: A → Prop): Type[0] ≝
764 { subset_wit:> A;
765   subset_proof: P subset_wit
766 }.
767*)
768
769definition build_maps' ≝
770  λpseudo_program.
771  let 〈preamble,instr_list〉 ≝ pseudo_program in
772  let result ≝
773   foldll
774    (option Identifier × pseudo_instruction)
775    (λprefix.
776      Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
777       match prefix return λ_.Prop with [mk_Propify prefix ⇒ tech_pc_sigma0 〈preamble,prefix〉 ≠ None ?])
778    (λprefix,t,i.
779      let 〈labels, pc_costs〉 ≝ t in
780      let 〈program_counter, costs〉 ≝ pc_costs in
781       let 〈label, i'〉 ≝ i in
782       let labels ≝
783         match label with
784         [ None ⇒ labels
785         | Some label ⇒
786           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
787             insert ? ? label program_counter_bv labels
788         ]
789       in
790         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
791         [ None ⇒
792            let dummy ≝ 〈labels,pc_costs〉 in
793              dummy
794         | Some construct ⇒ 〈labels, construct〉
795         ]
796    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
797  in
798   let 〈labels, pc_costs〉 ≝ result in
799   let 〈pc, costs〉 ≝ pc_costs in
800    〈labels, costs〉.
801 [
802 | @⊥
803 | normalize % //
804 ]
805qed.
806
807definition build_maps' ≝
808  λpseudo_program.
809  let 〈preamble,instr_list〉 ≝ pseudo_program in
810  let result ≝
811   foldl
812    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
813          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
814           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
815    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
816          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
817           is_prefix ? instr_list_prefix' instr_list →
818           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
819    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
820          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
821           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
822     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
823          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
824           is_prefix ? instr_list_prefix' instr_list →
825           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
826      let 〈labels, pc_costs〉 ≝ t in
827      let 〈program_counter, costs〉 ≝ pc_costs in
828       let 〈label, i'〉 ≝ i in
829       let labels ≝
830         match label with
831         [ None ⇒ labels
832         | Some label ⇒
833           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
834             insert ? ? label program_counter_bv labels
835         ]
836       in
837         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
838         [ None ⇒
839            let dummy ≝ 〈labels,pc_costs〉 in
840              dummy
841         | Some construct ⇒ 〈labels, construct〉
842         ]
843    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
844  in
845   let 〈labels, pc_costs〉 ≝ result in
846   let 〈pc, costs〉 ≝ pc_costs in
847    〈labels, costs〉.
848 [4: @(list_elim_rev ?
849       (λinstr_list. list (
850        (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
851          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
852           is_prefix ? instr_list_prefix' instr_list →
853           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)))
854       ?? instr_list) (* CSC: BAD ORDER FOR CODE EXTRACTION *)
855      [ @[ ]
856      | #l' #a #limage %2
857        [ %[@a] #PREFIX #PREFIX_OK
858        | (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN
859             THE INDUCTION HYPOTHESIS INSTEAD *)
860          elim limage
861           [ %1
862           | #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K3
863             @K1 @(prefix_of_append ???? K3)
864           ] 
865        ]
866       
867       
868     
869 
870  cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
871     % [@ (LIST_PREFIX @ [i])] %
872      [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
873      | (* DOABLE IN PRINCIPLE *)
874      ]
875 | (* assert false case *)
876 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
877 |   
878
879let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
880                       (encoding: list Byte) on encoding: Prop ≝
881  match encoding with
882  [ nil ⇒ final_pc = pc
883  | cons hd tl ⇒
884    let 〈new_pc, byte〉 ≝ next code_memory pc in
885      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
886  ].
887
888definition assembly_specification:
889  ∀assembly_program: pseudo_assembly_program.
890  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
891  λpseudo_assembly_program.
892  λcode_mem.
893    ∀pc: Word.
894      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
895      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
896      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
897      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
898      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
899       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
900      match pre_assembled with
901       [ None ⇒ True
902       | Some pc_code ⇒
903          let 〈new_pc,code〉 ≝ pc_code in
904           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
905
906axiom assembly_meets_specification:
907  ∀pseudo_assembly_program.
908    match assembly pseudo_assembly_program with
909    [ None ⇒ True
910    | Some code_mem_cost ⇒
911      let 〈code_mem, cost〉 ≝ code_mem_cost in
912        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
913    ].
914(*
915  # PROGRAM
916  [ cases PROGRAM
917    # PREAMBLE
918    # INSTR_LIST
919    elim INSTR_LIST
920    [ whd
921      whd in ⊢ (∀_. %)
922      # PC
923      whd
924    | # INSTR
925      # INSTR_LIST_TL
926      # H
927      whd
928      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
929    ]
930  | cases not_implemented
931  ] *)
932
933definition status_of_pseudo_status: PseudoStatus → option Status ≝
934 λps.
935  let pap ≝ code_memory … ps in
936   match assembly pap with
937    [ None ⇒ None …
938    | Some p ⇒
939       let cm ≝ load_code_memory (\fst p) in
940       let pc ≝ sigma' pap (program_counter ? ps) in
941        Some …
942         (mk_PreStatus (BitVectorTrie Byte 16)
943           cm
944           (low_internal_ram … ps)
945           (high_internal_ram … ps)
946           (external_ram … ps)
947           pc
948           (special_function_registers_8051 … ps)
949           (special_function_registers_8052 … ps)
950           (p1_latch … ps)
951           (p3_latch … ps)
952           (clock … ps)) ].
953
954definition write_at_stack_pointer':
955 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
956  λM: Type[0].
957  λs: PreStatus M.
958  λv: Byte.
959    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
960    let bit_zero ≝ get_index_v… nu O ? in
961    let bit_1 ≝ get_index_v… nu 1 ? in
962    let bit_2 ≝ get_index_v… nu 2 ? in
963    let bit_3 ≝ get_index_v… nu 3 ? in
964      if bit_zero then
965        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
966                              v (low_internal_ram ? s) in
967          set_low_internal_ram ? s memory
968      else
969        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
970                              v (high_internal_ram ? s) in
971          set_high_internal_ram ? s memory.
972  [ cases l0 %
973  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
974qed.
975
976definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
977 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
978
979  λticks_of.
980  λs.
981  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
982  let ticks ≝ ticks_of (program_counter ? s) in
983  let s ≝ set_clock ? s (clock ? s + ticks) in
984  let s ≝ set_program_counter ? s pc in
985    match instr with
986    [ Instruction instr ⇒
987       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
988    | Comment cmt ⇒ s
989    | Cost cst ⇒ s
990    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
991    | Call call ⇒
992      let a ≝ address_of_word_labels s call in
993      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
994      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
995      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
996      let s ≝ write_at_stack_pointer' ? s pc_bl in
997      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
998      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
999      let s ≝ write_at_stack_pointer' ? s pc_bu in
1000        set_program_counter ? s a
1001    | Mov dptr ident ⇒
1002       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1003    ].
1004 [
1005 |2,3,4: %
1006 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1007 |
1008 | %
1009 ]
1010 cases not_implemented
1011qed.
1012
1013(*
1014lemma execute_code_memory_unchanged:
1015 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1016 #ticks #ps whd in ⊢ (??? (??%))
1017 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1018  (program_counter pseudo_assembly_program ps)) #instr #pc
1019 whd in ⊢ (??? (??%)) cases instr
1020  [ #pre cases pre
1021     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1022       cases (split ????) #z1 #z2 %
1023     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1024       cases (split ????) #z1 #z2 %
1025     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1026       cases (split ????) #z1 #z2 %
1027     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1028       [ #x1 whd in ⊢ (??? (??%))
1029     | *: cases not_implemented
1030     ]
1031  | #comment %
1032  | #cost %
1033  | #label %
1034  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1035    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1036    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
1037    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1038    (* CSC: ??? *)
1039  | #dptr #label (* CSC: ??? *)
1040  ]
1041  cases not_implemented
1042qed.
1043*)
1044
1045lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1046 ∀ps,ps': PseudoStatus.
1047  code_memory … ps = code_memory … ps' →
1048   match status_of_pseudo_status ps with
1049    [ None ⇒ status_of_pseudo_status ps' = None …
1050    | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
1051    ].
1052 #ps #ps' #H whd in ⊢ (mat
1053 ch % with [ _ ⇒ ? | _ ⇒ ? ])
1054 generalize in match (refl … (assembly (code_memory … ps)))
1055 cases (assembly ?) in ⊢ (???% → %)
1056  [ #K whd whd in ⊢ (??%?) <H >K %
1057  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1058qed.*)
1059
1060let rec encoding_check' (code_memory: BitVectorTrie Byte 16) (pc: Word) (encoding: list Byte) on encoding: Prop ≝
1061  match encoding with
1062  [ nil ⇒ True
1063  | cons hd tl ⇒
1064    let 〈new_pc, byte〉 ≝ next code_memory pc in
1065      hd = byte ∧ encoding_check' code_memory new_pc tl
1066  ].
1067
1068(* prove later *)
1069axiom test:
1070  ∀pc: Word.
1071  ∀code_memory: BitVectorTrie Byte 16.
1072  ∀i: instruction.
1073    let assembled ≝ assembly1 i in
1074      encoding_check' code_memory pc assembled →
1075        let 〈instr_pc, ignore〉 ≝ fetch code_memory pc in
1076        let 〈instr, pc〉 ≝ instr_pc in
1077          instr = i.
1078 
1079lemma main_thm:
1080 ∀ticks_of.
1081 ∀ps: PseudoStatus.
1082  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
1083  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
1084  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
1085  let s' ≝ execute_1 s in
1086   s = s'']].
1087 #ticks_of #ps
1088 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1089 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
1090 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1091 generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))
1092 
1093 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
Note: See TracBrowser for help on using the repository browser.