source: src/ASM/Test.ma @ 2181

Last change on this file since 2181 was 2181, checked in by mulligan, 9 years ago

Work from the last week on the new formulation of the main lemma for assembler correctness.
File size: 53.6 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3include "ASM/StatusProofs.ma".
4include alias "arithmetics/nat.ma".
5include "ASM/AssemblyProof.ma".
6
7lemma set_program_counter_status_of_pseudo_status:
8  ∀M.
9  ∀cm.
10  ∀sigma.
11  ∀policy.
12  ∀s, s'.
13  ∀new_ppc.
14    status_of_pseudo_status M cm s sigma policy = s' →
15    set_program_counter (BitVectorTrie Byte 16)
16      (code_memory_of_pseudo_assembly_program cm sigma policy)
17      s'
18      (sigma new_ppc) =
19    status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy.
20  #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl //
21qed.
22
23lemma if_then_else_status_of_pseudo_status_true:
24  ∀M: internal_pseudo_address_map.
25  ∀cm: pseudo_assembly_program.
26  ∀sigma: Word → Word.
27  ∀policy: Word → bool.
28  ∀s, s', s'', s'''.
29  ∀t: bool.
30    t = true →
31    status_of_pseudo_status M cm s sigma policy = s' →
32      if t then
33        s'
34      else
35        s'' =
36      status_of_pseudo_status M cm (if t then s else s''') sigma policy.
37  #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl
38  >t_refl normalize nodelta >s_refl %
39qed.
40
41lemma if_then_else_status_of_pseudo_status_false:
42  ∀M: internal_pseudo_address_map.
43  ∀cm: pseudo_assembly_program.
44  ∀sigma: Word → Word.
45  ∀policy: Word → bool.
46  ∀s, s', s'', s'''.
47  ∀t: bool.
48    t = false →
49    status_of_pseudo_status M cm s sigma policy = s' →
50      if t then
51        s''
52      else
53        s' =
54      status_of_pseudo_status M cm (if t then s''' else s) sigma policy.
55  #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl
56  >t_refl normalize nodelta >s_refl %
57qed.
58
59lemma set_p1_latch_status_of_pseudo_status:
60  ∀M.
61  ∀code_memory.
62  ∀sigma.
63  ∀policy.
64  ∀s,s'.
65  ∀v.
66   status_of_pseudo_status M code_memory s sigma policy = s' →
67    set_p1_latch (BitVectorTrie Byte 16)
68      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
69      s' v =
70    status_of_pseudo_status M code_memory
71      (set_p1_latch pseudo_assembly_program code_memory s v) sigma policy.
72  #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl //
73qed.
74
75lemma set_p3_latch_status_of_pseudo_status:
76  ∀M.
77  ∀code_memory.
78  ∀sigma.
79  ∀policy.
80  ∀s, s'.
81  ∀v.
82  status_of_pseudo_status M code_memory s sigma policy = s' →
83    set_p3_latch (BitVectorTrie Byte 16)
84      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
85      s' v =
86    status_of_pseudo_status M code_memory
87      (set_p3_latch pseudo_assembly_program code_memory s v) sigma policy.
88  #M #code_memory #sigma #policy #s #s' #v #s_refl <s_refl //
89qed.
90
91definition map_acc_a_using_internal_pseudo_address_map:
92    ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝
93  λM, sigma, v.
94  match \snd M with
95  [ data ⇒ v
96  | address upper_lower word ⇒
97    let mapped ≝ sigma word in
98    let 〈high, low〉 ≝ vsplit bool 8 8 mapped in
99      if eq_upper_lower upper_lower upper then
100        high
101      else
102        low
103  ].
104
105(*CSC: Taken from AssemblyProofSplit.ma; there named map_lower_internal... *)
106definition map_internal_ram_address_using_pseudo_address_map:
107  ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
108  λM: internal_pseudo_address_map.
109  λsigma: Word → Word.
110  λaddress: Byte.
111  λvalue: Byte.
112  match assoc_list_lookup ?? address (eq_bv …) (\fst M) with
113  [ None ⇒ value
114  | Some upper_lower_word ⇒
115    let 〈upper_lower, word〉 ≝ upper_lower_word in
116    let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in
117      if eq_upper_lower upper_lower upper then
118        high
119      else
120        low
121  ].
122
123definition map_address_using_internal_pseudo_address_map:
124    ∀M: internal_pseudo_address_map. (Word → Word) → SFR8051 → Byte → Byte ≝
125  λM, sigma, sfr, v.
126  match sfr with
127  [ SFR_ACC_A ⇒ map_acc_a_using_internal_pseudo_address_map M sigma v
128  | _         ⇒ v
129  ].
130
131lemma set_index_set_index_overwrite:
132  ∀A: Type[0].
133  ∀n: nat.
134  ∀v: Vector A n.
135  ∀index: nat.
136  ∀e, e': A.
137  ∀proof.
138  ∀proof'.
139    set_index A n v index e proof =
140      set_index A n (set_index A n v index e' proof') index e proof.
141  #A #n #v elim v normalize
142  [1:
143    #index #e #e' #absurd cases (lt_to_not_zero … absurd)
144  |2:
145    #n' #hd #tl #inductive_hypothesis #index #e #e' cases index #proof #proof'
146    normalize //
147  ]
148qed.
149
150lemma set_index_set_index_commutation:
151  ∀A: Type[0].
152  ∀n: nat.
153  ∀v: Vector A n.
154  ∀m, o: nat.
155  ∀m_lt_proof: m < n.
156  ∀o_lt_proof: o < n.
157  ∀e, f: A.
158    m ≠ o →
159      set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof =
160        set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof.
161  #A #n #v elim v
162  [1:
163    #m #o #m_lt_proof
164    normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof)
165  |2:
166    #n' #hd #tl #inductive_hypothesis
167    #m #o
168    cases m cases o
169    [1:
170      #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant
171      @relevant %
172    |2,3:
173      #o' normalize //
174    |4:
175      #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm
176      normalize @eq_f @inductive_hypothesis @nmk #relevant
177      >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
178    ]
179  ]
180qed.
181
182(* XXX: move elsewhere *)
183lemma get_index_v_set_index_miss:
184  ∀a: Type[0].
185  ∀n: nat.
186  ∀v: Vector a n.
187  ∀i, j: nat.
188  ∀e: a.
189  ∀i_proof: i < n.
190  ∀j_proof: j < n.
191    i ≠ j →
192      get_index_v a n (set_index a n v i e i_proof) j j_proof =
193        get_index_v a n v j j_proof.
194  #a #n #v elim v
195  [1:
196    #i #j #e #i_proof
197    cases (lt_to_not_zero … i_proof)
198  |2:
199    #n' #hd #tl #inductive_hypothesis #i #j
200    cases i cases j
201    [1:
202      #e #i_proof #j_proof #neq_assm
203      cases (absurd ? (refl … 0) neq_assm)
204    |2,3:
205      #i' #e #i_proof #j_proof #_ %
206    |4:
207      #i' #j' #e #i_proof #j_proof #neq_assm
208      @inductive_hypothesis @nmk #eq_assm
209      >eq_assm in neq_assm; #neq_assm
210      cases (absurd ? (refl ??) neq_assm)
211    ]
212  ]
213qed.
214
215lemma set_index_status_of_pseudo_status:
216  ∀M, code_memory, sigma, policy, s, sfr, v, v'.
217    map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
218(set_index Byte 19
219  (special_function_registers_8051 (BitVectorTrie Byte 16)
220   (code_memory_of_pseudo_assembly_program code_memory sigma policy)
221   (status_of_pseudo_status M code_memory s sigma policy))
222  (sfr_8051_index sfr) v' (sfr8051_index_19 sfr)
223  =sfr_8051_of_pseudo_sfr_8051 M
224   (special_function_registers_8051 pseudo_assembly_program code_memory
225    (set_8051_sfr pseudo_assembly_program code_memory s sfr v)) sigma).
226  #M #code_memory #sigma #policy #s #sfr #v #v' #sfr_neq_acc_a_assm
227  whd in match status_of_pseudo_status; normalize nodelta
228  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
229  inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta
230  [1:
231    <sfr_neq_acc_a_assm cases sfr
232    [18:
233      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
234      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
235      >sndM_refl %
236    ]
237    %
238  |2:
239    @pair_elim #high #low #high_low_refl normalize nodelta
240    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
241    <sfr_neq_acc_a_assm cases sfr
242    [18,37:
243      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
244      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
245      >sndM_refl normalize nodelta >high_low_refl normalize nodelta
246      >eq_upper_lower_refl normalize nodelta
247      whd in match (set_8051_sfr ?????);
248      [1:
249        <set_index_set_index_overwrite in ⊢ (??%?);
250        <set_index_set_index_overwrite in ⊢ (???%); %
251      |2:
252        <set_index_set_index_overwrite in ⊢ (??%?);
253        <set_index_set_index_overwrite in ⊢ (???%); %
254      ]
255    ]
256    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
257    whd in match (set_8051_sfr ?????); @set_index_set_index_commutation normalize
258    @nmk #absurd destruct(absurd)
259  ]
260qed.
261
262lemma get_index_v_status_of_pseudo_status:
263  ∀M, code_memory, sigma, policy, s, s', sfr.
264    map_address_using_internal_pseudo_address_map M sigma sfr
265      (get_index_v Byte 19
266        (special_function_registers_8051 pseudo_assembly_program code_memory s)
267        (sfr_8051_index sfr) (sfr8051_index_19 sfr)) = s' →
268    get_index_v Byte 19
269      (special_function_registers_8051 (BitVectorTrie Byte 16)
270      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
271      (status_of_pseudo_status M code_memory s sigma policy))
272      (sfr_8051_index sfr) (sfr8051_index_19 sfr) = s'.
273  #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl
274  whd in match status_of_pseudo_status; normalize nodelta
275  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
276  inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta
277 [1:
278    cases sfr
279    [18:
280      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
281      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
282      >sndM_refl %
283    ]
284    %
285  |2:
286    @pair_elim #high #low #high_low_refl normalize nodelta
287    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
288    cases sfr
289    [18,37:
290      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
291      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
292      >sndM_refl normalize nodelta >high_low_refl normalize nodelta
293      >eq_upper_lower_refl normalize nodelta
294      whd in match (set_8051_sfr ?????); //
295    ]
296    @get_index_v_set_index_miss whd in ⊢ (?(??%%));
297    @nmk #absurd destruct(absurd)
298  ]
299qed.
300
301lemma set_8051_sfr_status_of_pseudo_status:
302  ∀M, code_memory, sigma, policy, s, s', sfr, v,v'.
303    status_of_pseudo_status M code_memory s sigma policy = s' →
304    map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
305      set_8051_sfr ? (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v' =
306      status_of_pseudo_status M code_memory
307        (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy.
308  #M #code_memory #sigma #policy #s #s' #sfr #v #v' #s_ok #v_ok
309  <s_ok whd in ⊢ (??%%); @split_eq_status try % /2/
310qed.
311
312lemma get_8051_sfr_status_of_pseudo_status:
313  ∀M, code_memory, sigma, policy, s, s', s'', sfr.
314    status_of_pseudo_status M code_memory s sigma policy = s' →
315    map_address_using_internal_pseudo_address_map M sigma sfr
316     (get_8051_sfr pseudo_assembly_program code_memory s sfr) = s'' →
317  get_8051_sfr (BitVectorTrie Byte 16)
318    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
319     s' sfr = s''.
320  #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' <s_refl <s_refl'
321  whd in match get_8051_sfr; normalize nodelta
322  @get_index_v_status_of_pseudo_status %
323qed.
324
325lemma get_8052_sfr_status_of_pseudo_status:
326  ∀M, code_memory, sigma, policy, s, s', sfr.
327  status_of_pseudo_status M code_memory s sigma policy = s' →
328  (get_8052_sfr (BitVectorTrie Byte 16)
329    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
330    s' sfr =
331   (get_8052_sfr pseudo_assembly_program code_memory s sfr)).
332  #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl //
333qed.
334
335lemma set_8052_sfr_status_of_pseudo_status:
336  ∀M, code_memory, sigma, policy, s, s', sfr, v.
337  status_of_pseudo_status M code_memory s sigma policy = s' →
338    (set_8052_sfr (BitVectorTrie Byte 16)
339      (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v =
340    status_of_pseudo_status M code_memory
341     (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
342  #M #code_memory #sigma #policy #s #s' #sfr #v #s_refl <s_refl //
343qed.
344 
345definition map_address_Byte_using_internal_pseudo_address_map ≝
346 λM,sigma,d,v.
347  match sfr_of_Byte d with
348  [ None ⇒ v
349  | Some sfr8051_8052 ⇒
350    match sfr8051_8052 with
351    [ inl sfr ⇒
352      map_address_using_internal_pseudo_address_map M sigma sfr v
353    | inr _ ⇒ v
354    ]
355  ].
356
357lemma set_bit_addressable_sfr_status_of_pseudo_status':
358  let M ≝ pseudo_assembly_program in
359    ∀code_memory: M.
360    ∀s: PreStatus M code_memory.
361    ∀d: Byte.
362    ∀v: Byte.
363      Σp: PreStatus M code_memory.
364        ∀M.
365        ∀sigma.
366        ∀policy.
367        ∀s'.
368        ∀v'.
369          status_of_pseudo_status M code_memory s sigma policy = s' →
370            map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
371              (set_bit_addressable_sfr (BitVectorTrie Byte 16)
372                (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' d v' =
373              status_of_pseudo_status M code_memory
374                (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
375  whd in match map_address_Byte_using_internal_pseudo_address_map;
376  whd in match set_bit_addressable_sfr;
377  normalize nodelta
378  @(let M ≝ pseudo_assembly_program in
379  λcode_memory:M.
380  λs: PreStatus M code_memory.
381  λb: Byte.
382  λv: Byte.
383   match sfr_of_Byte b with
384   [ None ⇒ match not_implemented in False with [ ]
385   | Some sfr8051_8052 ⇒
386      match sfr8051_8052 with
387      [ inl sfr ⇒
388         match sfr with
389         [ SFR_P1 ⇒
390           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
391           set_p1_latch ?? s v
392         | SFR_P3 ⇒
393           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
394           set_p3_latch ?? s v
395         | _ ⇒ set_8051_sfr ?? s sfr v ]
396      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
397  normalize nodelta #M #sigma #policy #s' #v' #s_refl <s_refl
398  /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
399  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
400  #v_refl >v_refl //
401qed.
402
403lemma set_bit_addressable_sfr_status_of_pseudo_status:
404 ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte.
405  ∀M. ∀sigma. ∀policy. ∀s': Status ?. ∀v'.
406  status_of_pseudo_status M code_memory s sigma policy = s' →
407  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
408 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
409  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
410  s' d v'
411  =status_of_pseudo_status M code_memory
412   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
413 #code #s #d #v cases (set_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_
414 #H @H
415qed.
416
417lemma set_low_internal_ram_status_of_pseudo_status:
418 ∀cm,sigma,policy,M,s,s',ram.
419  status_of_pseudo_status M cm s sigma policy = s' →
420  set_low_internal_ram (BitVectorTrie Byte 16)
421  (code_memory_of_pseudo_assembly_program cm sigma policy)
422  s'
423  (low_internal_ram_of_pseudo_low_internal_ram M ram)
424  = status_of_pseudo_status M cm
425    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
426  #cm #sigma #policy #M #s #s' #ram #s_refl <s_refl //
427qed.
428
429(* Real axiom ATM *)
430axiom insert_low_internal_ram_of_pseudo_low_internal_ram:
431 ∀M,sigma,cm,s,addr,v,v'.
432 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
433  insert Byte 7 addr v'
434  (low_internal_ram_of_pseudo_low_internal_ram M
435   (low_internal_ram pseudo_assembly_program cm s))
436  =low_internal_ram_of_pseudo_low_internal_ram M
437   (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
438               
439lemma insert_low_internal_ram_status_of_pseudo_status:
440 ∀M,cm,sigma,policy,s,addr,v,v'.
441 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
442  insert Byte 7 addr v'
443   (low_internal_ram (BitVectorTrie Byte 16)
444    (code_memory_of_pseudo_assembly_program cm sigma policy)
445    (status_of_pseudo_status M cm s sigma policy))
446  = low_internal_ram_of_pseudo_low_internal_ram M
447     (insert Byte 7 addr v
448      (low_internal_ram pseudo_assembly_program cm s)).
449 /2 by insert_low_internal_ram_of_pseudo_low_internal_ram/
450qed.
451
452(* Real axiom ATM *)
453axiom insert_high_internal_ram_of_pseudo_high_internal_ram:
454 ∀M,sigma,cm,s,addr,v,v'.
455 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
456  insert Byte 7 addr v'
457  (high_internal_ram_of_pseudo_high_internal_ram M
458   (high_internal_ram pseudo_assembly_program cm s))
459  =high_internal_ram_of_pseudo_high_internal_ram M
460   (insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)).
461
462lemma insert_high_internal_ram_status_of_pseudo_status:
463 ∀M,cm,sigma,policy,s,addr,v,v'.
464 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
465  insert Byte 7 addr v'
466   (high_internal_ram (BitVectorTrie Byte 16)
467    (code_memory_of_pseudo_assembly_program cm sigma policy)
468    (status_of_pseudo_status M cm s sigma policy))
469  = high_internal_ram_of_pseudo_high_internal_ram M
470     (insert Byte 7 addr v
471      (high_internal_ram pseudo_assembly_program cm s)).
472 /2 by insert_high_internal_ram_of_pseudo_high_internal_ram/
473qed.
474
475lemma bit_address_of_register_status_of_pseudo_status:
476 ∀M,cm,s,sigma,policy,r.
477  bit_address_of_register …
478  (code_memory_of_pseudo_assembly_program cm sigma policy)
479  (status_of_pseudo_status M cm s sigma policy) r =
480  bit_address_of_register … cm s r.
481 #M #cm #s #sigma #policy #r whd in ⊢ (??%%);
482 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
483 @pair_elim #un #ln #_
484 @pair_elim #r1 #r0 #_ %
485qed.
486
487(*CSC: provable using the axiom in AssemblyProof, but this one seems more
488  primitive *)
489axiom lookup_low_internal_ram_of_pseudo_low_internal_ram:
490 ∀M,sigma,cm,s,s',addr.
491  map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr)
492  (lookup Byte 7 addr
493   (low_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
494  lookup Byte 7 addr
495  (low_internal_ram_of_pseudo_low_internal_ram M
496   (low_internal_ram pseudo_assembly_program cm s)) (zero 8)
497  = s'.
498
499(*CSC: provable using the axiom in AssemblyProof, but this one seems more
500  primitive *)
501axiom lookup_high_internal_ram_of_pseudo_high_internal_ram:
502 ∀M,sigma,cm,s,s',addr.
503  map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr)
504  (lookup Byte 7 addr
505   (high_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
506  lookup Byte 7 addr
507  (high_internal_ram_of_pseudo_high_internal_ram M
508   (high_internal_ram pseudo_assembly_program cm s)) (zero 8)
509  = s'.
510
511lemma get_register_status_of_pseudo_status:
512 ∀M,cm,sigma,policy,s,s',s'',r.
513  status_of_pseudo_status M cm s sigma policy = s' →
514  map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
515   (get_register … cm s r) = s'' →
516  get_register …
517   (code_memory_of_pseudo_assembly_program cm sigma policy)
518   s' r = s''.
519 #M #cm #sigma #policy #s #s' #s'' #r #s_refl #s_refl' <s_refl <s_refl'
520 whd in match get_register; normalize nodelta
521 whd in match status_of_pseudo_status; normalize nodelta
522 >bit_address_of_register_status_of_pseudo_status
523 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … (refl …))
524qed.
525
526lemma external_ram_status_of_pseudo_status:
527 ∀M,cm,s,sigma,policy.
528  external_ram …
529   (code_memory_of_pseudo_assembly_program cm sigma policy)
530   (status_of_pseudo_status M cm s sigma policy) =
531  external_ram … cm s.
532 //
533qed.
534
535lemma set_external_ram_status_of_pseudo_status:
536  ∀M,cm,ps,sigma,policy,ram.
537    set_external_ram …
538      (code_memory_of_pseudo_assembly_program cm sigma policy)
539      (status_of_pseudo_status M cm ps sigma policy)
540      ram =
541    status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy.
542  //
543qed.
544
545lemma set_register_status_of_pseudo_status:
546 ∀M,sigma,policy,cm,s,s',r,v,v'.
547  status_of_pseudo_status M cm s sigma policy = s' →
548  map_internal_ram_address_using_pseudo_address_map M sigma
549   (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' →
550  set_register (BitVectorTrie Byte 16)
551   (code_memory_of_pseudo_assembly_program cm sigma policy)
552   s' r v'
553  = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v)
554    sigma policy.
555  #M #sigma #policy #cm #s #s' #r #v #v' #s_refl <s_refl #v_ok
556 whd in match set_register; normalize nodelta
557 >bit_address_of_register_status_of_pseudo_status
558 >(insert_low_internal_ram_status_of_pseudo_status … v_ok)
559 @set_low_internal_ram_status_of_pseudo_status %
560qed.
561
562definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝
563 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λsigma. λaddr.
564  match addr with
565  [ INDIRECT i ⇒
566     assoc_list_lookup ??
567      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None …
568  | EXT_INDIRECT e ⇒
569     assoc_list_lookup ??
570      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None …
571  | ACC_DPTR ⇒
572    (* XXX: \snd M = None plus in the very rare case when we are trying to dereference a null (O) pointer
573            in the ACC_A *)
574      map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
575        get_8051_sfr … cm s SFR_ACC_A
576  | ACC_PC ⇒
577      (* XXX: as above *)
578      map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
579        get_8051_sfr … cm s SFR_ACC_A ∧ sigma (program_counter … s) = program_counter … s
580  | _ ⇒ True ].
581
582definition map_address_mode_using_internal_pseudo_address_map_ok2 ≝
583 λT,M,sigma,cm.λs:PreStatus T cm.λaddr,v.
584  match addr with
585  [ DIRECT d ⇒
586     let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in
587     match head' … bit_one with
588     [ true ⇒
589      map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v
590     | false ⇒
591      map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ]
592  | INDIRECT i ⇒
593     let register ≝ get_register ?? s [[ false; false; i ]] in
594     map_internal_ram_address_using_pseudo_address_map M sigma register v
595  | REGISTER r ⇒
596     map_internal_ram_address_using_pseudo_address_map M sigma
597      (false:::bit_address_of_register … s r) v
598  | ACC_A ⇒
599     map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v
600  | _ ⇒ v ].
601
602(*CSC: move elsewhere*)
603lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v.
604 #A #n #v inversion v in ⊢ ?;
605 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/
606 | #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ]
607qed.
608
609(*CSC: move elsewhere*)
610lemma tail_singleton: ∀A,v. tail A 0 v = [[]].
611 #A #v inversion v in ⊢ ?;
612 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H)
613 | #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize
614   /2 by jmeq_to_eq/
615 ]
616qed.
617
618(*CSC: move elsewhere*)
619lemma eq_cons_head_append:
620 ∀A,n.∀hd: Vector A 1. ∀tl: Vector A n.
621  head' A 0 hd:::tl = hd@@tl.
622 #A #n #hd #tl >(eq_head' … hd) >tail_singleton %
623qed.
624
625lemma set_arg_8_status_of_pseudo_status':
626  ∀cm.
627  ∀ps.
628  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
629  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
630   status_of_pseudo_status M cm ps sigma policy = s' →
631   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
632   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
633    set_arg_8 (BitVectorTrie Byte 16)
634      (code_memory_of_pseudo_assembly_program cm sigma policy)
635      s' addr value' =
636    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
637  whd in match set_arg_8; normalize nodelta
638  @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ;
639                                   acc_a ; acc_b ; ext_indirect ;
640                                   ext_indirect_dptr ]]. λv.
641    match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
642                                                acc_a ; acc_b ; ext_indirect ;
643                                                ext_indirect_dptr ]] addr) →
644                   Σp.?
645            with
646      [ DIRECT d ⇒
647        λdirect: True.
648          deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in
649            match head' … bit_one with
650              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
651              | false ⇒
652                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
653                  set_low_internal_ram ?? s memory
654              ]
655      | INDIRECT i ⇒
656        λindirect: True.
657          let register ≝ get_register ?? s [[ false; false; i ]] in
658          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
659            match head' … bit_one with
660              [ false ⇒
661                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
662                  set_low_internal_ram ?? s memory
663              | true ⇒
664                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
665                  set_high_internal_ram ?? s memory
666              ]
667      | REGISTER r ⇒ λregister: True. set_register ?? s r v
668      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
669      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
670      | EXT_INDIRECT e ⇒
671        λext_indirect: True.
672          let address ≝ get_register ?? s [[ false; false; e ]] in
673          let padded_address ≝ pad 8 8 address in
674          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
675            set_external_ram ?? s memory
676      | EXT_INDIRECT_DPTR ⇒
677        λext_indirect_dptr: True.
678          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
679          let memory ≝ insert ? 16 address v (external_ram ?? s) in
680            set_external_ram ?? s memory
681      | _ ⇒
682        λother: False.
683          match other in False with [ ]
684      ] (subaddressing_modein … a)) normalize nodelta
685  #M #sigma #policy #s' #v' #s_refl <s_refl
686  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
687  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
688  [1,2:
689    <vsplit_refl normalize nodelta >p normalize nodelta
690    [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status
691    | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
692  |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p;
693      >(get_register_status_of_pseudo_status … (refl …) (refl …))
694      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
695      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
696      [ >(insert_high_internal_ram_status_of_pseudo_status … v)
697      | >(insert_low_internal_ram_status_of_pseudo_status … v) ]
698      // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
699  |5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …))
700      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
701      >EQ1 normalize nodelta
702      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
703  |6: #EQ1 #EQ2 <EQ2 /2 by set_register_status_of_pseudo_status/
704  |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
705  |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
706  |9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
707      >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
708      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] %
709qed.
710
711lemma set_arg_8_status_of_pseudo_status:
712  ∀cm.
713  ∀ps.
714  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
715  ∀value.
716  ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
717   status_of_pseudo_status M cm ps sigma policy = s' →
718   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
719   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
720    set_arg_8 (BitVectorTrie Byte 16)
721      (code_memory_of_pseudo_assembly_program cm sigma policy)
722      s' addr value' =
723    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
724  #cm #ps #addr #value
725  cases (set_arg_8_status_of_pseudo_status' cm ps addr value) #_ #relevant
726  @relevant
727qed.
728
729lemma p1_latch_status_of_pseudo_status:
730    ∀M.
731    ∀sigma.
732    ∀policy.
733    ∀code_memory: pseudo_assembly_program.
734    ∀s: PreStatus … code_memory.
735    ∀s'.
736    (status_of_pseudo_status M code_memory s sigma policy) = s' →
737    (p1_latch (BitVectorTrie Byte 16)
738      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
739      s' =
740    (p1_latch pseudo_assembly_program code_memory s)).
741  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
742qed.
743
744lemma p3_latch_status_of_pseudo_status:
745    ∀M.
746    ∀sigma.
747    ∀policy.
748    ∀code_memory: pseudo_assembly_program.
749    ∀s: PreStatus … code_memory.
750    ∀s'.
751    (status_of_pseudo_status M code_memory s sigma policy) = s' →
752    (p3_latch (BitVectorTrie Byte 16)
753      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
754      (status_of_pseudo_status M code_memory s sigma policy) =
755    (p3_latch pseudo_assembly_program code_memory s)).
756  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
757qed.
758
759lemma get_bit_addressable_sfr_status_of_pseudo_status':
760  let M ≝ pseudo_assembly_program in
761    ∀code_memory: M.
762    ∀s: PreStatus M code_memory.
763    ∀d: Byte.
764    ∀l: bool.
765      Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
766        status_of_pseudo_status M code_memory s sigma policy = s' →
767        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
768          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
769          s' d l =
770        map_address_Byte_using_internal_pseudo_address_map M sigma
771         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)).
772  whd in match get_bit_addressable_sfr;
773  whd in match map_address_Byte_using_internal_pseudo_address_map;
774  normalize nodelta
775  @(let M ≝ pseudo_assembly_program in
776    λcode_memory:M.
777    λs: PreStatus M code_memory.
778    λb: Byte.
779    λl: bool.
780    match sfr_of_Byte b with
781    [ None ⇒ match not_implemented in False with [ ]
782    | Some sfr8051_8052 ⇒
783    match sfr8051_8052 with
784    [ inl sfr ⇒
785      match sfr with
786      [ SFR_P1 ⇒
787        if l then
788          p1_latch … s
789        else
790          get_8051_sfr … s SFR_P1
791      | SFR_P3 ⇒
792        if l then
793          p3_latch … s
794        else
795          get_8051_sfr … s SFR_P3
796      | _ ⇒ get_8051_sfr … s sfr
797      ]
798    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
799    ]
800    ])
801  #M #sigma #policy #s' #s_refl <s_refl normalize nodelta
802  /2 by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/
803qed.
804
805lemma get_bit_addressable_sfr_status_of_pseudo_status:
806  let M ≝ pseudo_assembly_program in
807    ∀code_memory: M.
808    ∀s: PreStatus M code_memory.
809    ∀d: Byte.
810    ∀l: bool.
811    ∀M. ∀sigma. ∀policy. ∀s'. ∀s''.
812      map_address_Byte_using_internal_pseudo_address_map M sigma
813         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l) = s'' →
814      (status_of_pseudo_status M code_memory s sigma policy) = s' →
815        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
816          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
817          s' d l) = s''.
818 #code #s #d #v
819 cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ #relevant
820 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl <s_refl' @relevant %
821qed.
822
823lemma program_counter_status_of_pseudo_status:
824    ∀M. ∀sigma: Word → Word. ∀policy.
825    ∀code_memory: pseudo_assembly_program.
826    ∀s: PreStatus ? code_memory.
827    ∀s'.
828    ∀s''.
829    sigma (program_counter … s) = s'' →
830    (status_of_pseudo_status M code_memory s sigma policy) = s' →
831      program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy)
832        s' = s''.
833  #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl <s_refl' //
834qed.
835
836lemma get_cy_flag_status_of_pseudo_status:
837  ∀M, cm, sigma, policy, s, s'.
838  (status_of_pseudo_status M cm s sigma policy) = s' →
839  (get_cy_flag (BitVectorTrie Byte 16)
840    (code_memory_of_pseudo_assembly_program cm sigma policy)
841    s' =
842  get_cy_flag pseudo_assembly_program cm s).
843  #M #cm #sigma #policy #s #s' #s_refl <s_refl
844  whd in match get_cy_flag; normalize nodelta
845  >(get_index_v_status_of_pseudo_status … (refl …)) %
846qed.
847
848lemma get_arg_8_status_of_pseudo_status':
849  ∀cm.
850  ∀ps.
851  ∀l.
852  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
853    Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
854      (status_of_pseudo_status M cm ps sigma policy) = s' →
855      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
856      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
857      s' l addr =
858      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr).
859  whd in match get_arg_8; normalize nodelta
860  @(let m ≝ pseudo_assembly_program in
861    λcm: m. λs: PreStatus m cm. λl: bool. λa: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr]].
862    match a return λx. bool_to_Prop (is_in ? [[ direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr ]] x) → Σp. ? with
863      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
864      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
865      | DATA d ⇒ λdata: True. d
866      | REGISTER r ⇒ λregister: True. get_register ?? s r
867      | EXT_INDIRECT_DPTR ⇒
868        λext_indirect_dptr: True.
869          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
870            lookup ? 16 address (external_ram ?? s) (zero 8)
871      | EXT_INDIRECT e ⇒
872        λext_indirect: True.
873          let address ≝ get_register ?? s [[ false; false; e ]]  in
874          let padded_address ≝ pad 8 8 address in
875            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
876      | ACC_DPTR ⇒
877        λacc_dptr: True.
878          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
879          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
880          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
881            lookup ? 16 address (external_ram ?? s) (zero 8)
882      | ACC_PC ⇒
883        λacc_pc: True.
884          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
885          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
886            lookup ? 16 address (external_ram ?? s) (zero 8)
887      | DIRECT d ⇒
888        λdirect: True.
889          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
890            match head' … hd with
891            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
892            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
893            ]
894      | INDIRECT i ⇒
895        λindirect: True.
896          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
897            match head' … hd with
898            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
899            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
900            ]
901      | _ ⇒ λother: False.
902        match other in False with [ ]
903      ] (subaddressing_modein … a)) normalize nodelta
904  #M #sigma #policy #s' #s_refl <s_refl
905  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
906  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
907  [1:
908    #_ >p normalize nodelta >p1 normalize nodelta
909    @(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) %
910  |2:
911    #_>p normalize nodelta >p1 normalize nodelta
912    @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) %
913  |3,4:
914    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
915    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
916    >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta
917    [1:
918      @(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma)
919    |2:
920      @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
921    ]
922    @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
923  |5:
924    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
925    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
926    >assoc_list_assm normalize nodelta %
927  |6,7,8,9:
928    #_ /2 by refl, get_register_status_of_pseudo_status, get_index_v_status_of_pseudo_status/
929  |10:
930    #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
931    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
932    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
933    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
934    >acc_a_assm >p normalize nodelta //
935  |11:
936    * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
937    >(program_counter_status_of_pseudo_status … (refl …) (refl …))
938    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
939    >sigma_assm >map_acc_a_assm >p normalize nodelta //
940  |12:
941    #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
942    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
943    >external_ram_status_of_pseudo_status //
944  ]
945qed.
946
947lemma get_arg_8_status_of_pseudo_status:
948  ∀cm.
949  ∀ps.
950  ∀l.
951  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
952  ∀M. ∀sigma. ∀policy. ∀s', s''.
953      (status_of_pseudo_status M cm ps sigma policy) = s' →
954      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr) = s'' →
955      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
956      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
957      s' l addr = s''.
958  #cm #ps #l #addr
959  cases (get_arg_8_status_of_pseudo_status' cm ps l addr) #_ #relevant
960  #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl'
961  @relevant assumption
962qed.
963
964lemma get_arg_16_status_of_pseudo_status:
965  ∀cm.
966  ∀ps.
967  ∀addr: [[data16]].
968  ∀M. ∀sigma. ∀policy. ∀s'.
969    status_of_pseudo_status M cm ps sigma policy = s' →
970      get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
971      s' addr =
972      (get_arg_16 … cm ps addr).
973  #cm #ps #addr #M #sigma #policy #s' #s_refl <s_refl //
974qed.
975
976lemma set_arg_16_status_of_pseudo_status:
977  ∀cm.
978  ∀ps.
979  ∀addr: [[dptr]].
980  ∀v: Word.
981  ∀M. ∀sigma. ∀policy. ∀s'.
982    status_of_pseudo_status M cm ps sigma policy = s' →
983      set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
984      s' v addr =
985      status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy.
986  #cm #ps #addr #v #M #sigma #policy #s' #s_refl <s_refl
987  @(subaddressing_mode_elim … addr)
988  whd in match set_arg_16; normalize nodelta
989  whd in match set_arg_16'; normalize nodelta
990  @(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta
991  @set_8051_sfr_status_of_pseudo_status try % @sym_eq
992  @set_8051_sfr_status_of_pseudo_status %
993qed.
994
995definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝
996 λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl.
997  match addr with
998  [ BIT_ADDR b ⇒
999    let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1000    match head' … bit_1 with
1001    [ true ⇒
1002      let address ≝ nat_of_bitvector … seven_bits in
1003      let d ≝ address ÷ 8 in
1004      let m ≝ address mod 8 in
1005      let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1006        map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l
1007    | false ⇒
1008      let address ≝ nat_of_bitvector … seven_bits in
1009      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1010      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1011        map_internal_ram_address_using_pseudo_address_map M sigma
1012          (false:::address') t = t
1013    ]
1014  | N_BIT_ADDR b ⇒
1015    let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1016    match head' … bit_1 with
1017    [ true ⇒
1018      let address ≝ nat_of_bitvector … seven_bits in
1019      let d ≝ address ÷ 8 in
1020      let m ≝ address mod 8 in
1021      let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1022        map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l
1023    | false ⇒
1024      let address ≝ nat_of_bitvector … seven_bits in
1025      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1026      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1027        map_internal_ram_address_using_pseudo_address_map M sigma
1028          (false:::address') t = t
1029    ]
1030  | _ ⇒ True ].
1031
1032lemma get_arg_1_status_of_pseudo_status':
1033  ∀cm.
1034  ∀ps.
1035  ∀addr: [[bit_addr; n_bit_addr; carry]].
1036  ∀l.
1037    Σb: bool. ∀M. ∀sigma. ∀policy. ∀s'.
1038      status_of_pseudo_status M cm ps sigma policy = s' →
1039      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
1040      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1041      s' addr l =
1042      (get_arg_1 … cm ps addr l).
1043  whd in match get_arg_1; normalize nodelta
1044  @(let m ≝ pseudo_assembly_program in
1045    λcm: m. λs: PseudoStatus cm. λa:[[bit_addr; n_bit_addr; carry]]. λl.
1046    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
1047                                                 n_bit_addr ;
1048                                                 carry ]] x) → Σb: bool. ? with
1049      [ BIT_ADDR b ⇒
1050        λbit_addr: True.
1051        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1052        match head' … bit_1 with
1053        [ true ⇒
1054          let address ≝ nat_of_bitvector … seven_bits in
1055          let d ≝ address ÷ 8 in
1056          let m ≝ address mod 8 in
1057          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1058          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1059            get_index_v … sfr m ?
1060        | false ⇒
1061          let address ≝ nat_of_bitvector … seven_bits in
1062          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1063          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1064            get_index_v … t (modulus address 8) ?
1065        ]
1066      | N_BIT_ADDR n ⇒
1067        λn_bit_addr: True.
1068        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
1069        match head' … bit_1 with
1070        [ true ⇒
1071          let address ≝ nat_of_bitvector … seven_bits in
1072          let d ≝ address ÷ 8 in
1073          let m ≝ address mod 8 in
1074          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1075          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1076            ¬(get_index_v … sfr m ?)
1077        | false ⇒
1078          let address ≝ nat_of_bitvector … seven_bits in
1079          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1080          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1081            ¬(get_index_v … t (modulus address 8) ?)
1082        ]
1083      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
1084      | _ ⇒ λother.
1085        match other in False with [ ]
1086      ] (subaddressing_modein … a)) normalize nodelta
1087  try @modulus_less_than
1088  #M #sigma #policy #s' #s_refl <s_refl
1089  [1:
1090    #_ >(get_cy_flag_status_of_pseudo_status … (refl …)) %
1091  |2,4:
1092    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
1093    >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) #map_address_assm
1094    >map_address_assm %
1095  |3,5:
1096    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
1097    whd in match status_of_pseudo_status; normalize nodelta
1098    >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
1099    #map_address_assm >map_address_assm %
1100  ]
1101qed.
1102
1103lemma get_arg_1_status_of_pseudo_status:
1104  ∀cm.
1105  ∀ps.
1106  ∀addr: [[bit_addr; n_bit_addr; carry]].
1107  ∀l.
1108  ∀M. ∀sigma. ∀policy. ∀s'.
1109    status_of_pseudo_status M cm ps sigma policy = s' →
1110      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
1111      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1112      s' addr l =
1113      (get_arg_1 … cm ps addr l).
1114  #cm #ps #addr #l
1115  cases (get_arg_1_status_of_pseudo_status' cm ps addr l) #_ #assm
1116  @assm
1117qed.
1118
1119definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝
1120  λM: internal_pseudo_address_map.
1121  λcm: pseudo_assembly_program.
1122  λs: PreStatus ? cm.
1123  λsigma: Word → Word.
1124  λaddr: [[bit_addr; carry]].
1125  λv: Bit.
1126  match addr with
1127  [ BIT_ADDR b ⇒
1128    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1129    match head' … bit_1 with
1130    [ true ⇒
1131      let address ≝ nat_of_bitvector … seven_bits in
1132      let d ≝ address ÷ 8 in
1133      let m ≝ address mod 8 in
1134      let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1135      let sfr ≝ get_bit_addressable_sfr … s t true in
1136        map_address_Byte_using_internal_pseudo_address_map M sigma t sfr = sfr
1137    | false ⇒
1138      let address ≝ nat_of_bitvector … seven_bits in
1139      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1140      let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1141        map_internal_ram_address_using_pseudo_address_map M sigma
1142          (false:::address') t = t
1143    ]   
1144  | CARRY ⇒ True
1145  | _ ⇒ True
1146  ].
1147
1148definition map_bit_address_mode_using_internal_pseudo_address_map_set_2 ≝
1149  λM: internal_pseudo_address_map.
1150  λcm: pseudo_assembly_program.
1151  λs: PreStatus ? cm.
1152  λsigma: Word → Word.
1153  λaddr: [[bit_addr; carry]].
1154  λv: Bit.
1155  match addr with
1156  [ BIT_ADDR b ⇒
1157    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1158    match head' … bit_1 with
1159    [ true ⇒
1160      let address ≝ nat_of_bitvector … seven_bits in
1161      let d ≝ address ÷ 8 in
1162      let m ≝ address mod 8 in
1163      let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1164      let sfr ≝ get_bit_addressable_sfr … s t true in
1165      let new_sfr ≝ set_index … sfr m v ? in
1166        map_address_Byte_using_internal_pseudo_address_map M sigma new_sfr t = t
1167    | false ⇒
1168      let address ≝ nat_of_bitvector … seven_bits in
1169      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1170      let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1171      let n_bit ≝ set_index … t (modulus address 8) v ? in
1172      let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1173        map_internal_ram_address_using_pseudo_address_map M sigma
1174          (false:::address') n_bit = n_bit
1175    ]   
1176  | CARRY ⇒ True
1177  | _ ⇒ True
1178  ].
1179  @modulus_less_than
1180qed.
1181
1182lemma set_arg_1_status_of_pseudo_status':
1183  ∀cm: pseudo_assembly_program.
1184  ∀ps: PreStatus pseudo_assembly_program cm.
1185  ∀addr: [[bit_addr; carry]].
1186  ∀b: Bit.
1187    Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
1188      b = b' →
1189      status_of_pseudo_status M cm ps sigma policy = s' →
1190      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
1191      map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
1192        set_arg_1 (BitVectorTrie Byte 16)
1193          (code_memory_of_pseudo_assembly_program cm sigma policy)
1194          s' addr b =
1195        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
1196  whd in match set_arg_1; normalize nodelta
1197  whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta
1198  whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_2; normalize nodelta
1199  @(let m ≝ pseudo_assembly_program in
1200    λcm.
1201    λs: PreStatus m cm.
1202    λa: [[bit_addr; carry]].
1203    λv: Bit.
1204    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with
1205      [ BIT_ADDR b ⇒ λbit_addr: True.
1206        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1207        match head' … bit_1 with
1208        [ true ⇒
1209          let address ≝ nat_of_bitvector … seven_bits in
1210          let d ≝ address ÷ 8 in
1211          let m ≝ address mod 8 in
1212          let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1213          let sfr ≝ get_bit_addressable_sfr … s t true in
1214          let new_sfr ≝ set_index … sfr m v ? in
1215            set_bit_addressable_sfr … s new_sfr t
1216        | false ⇒
1217          let address ≝ nat_of_bitvector … seven_bits in
1218          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1219          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1220          let n_bit ≝ set_index … t (modulus address 8) v ? in
1221          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1222            set_low_internal_ram … s memory
1223        ]
1224      | CARRY ⇒
1225        λcarry: True.
1226        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1227        let new_psw ≝ v:::seven_bits in
1228          set_8051_sfr ?? s SFR_PSW new_psw
1229      | _ ⇒
1230        λother: False.
1231          match other in False with
1232            [ ]
1233      ] (subaddressing_modein … a)) normalize nodelta
1234  try @modulus_less_than #M #sigma #policy #s' #b' #b_refl <b_refl #s_refl <s_refl
1235  [1:
1236    #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
1237    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
1238    >p normalize nodelta @set_8051_sfr_status_of_pseudo_status %
1239  |2,3:
1240    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
1241    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
1242    >p normalize nodelta >p1 normalize nodelta
1243    #map_bit_address_assm_1 #map_bit_address_assm_2
1244    [1:
1245      >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …))
1246      >map_bit_address_assm_1
1247      >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) %
1248    |2:
1249      whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta
1250      >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
1251      >map_bit_address_assm_1
1252      >(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2)
1253      >set_low_internal_ram_status_of_pseudo_status in ⊢ (??%?); %
1254    ]
1255  ]
1256qed.
1257
1258lemma set_arg_1_status_of_pseudo_status:
1259  ∀cm: pseudo_assembly_program.
1260  ∀ps: PreStatus pseudo_assembly_program cm.
1261  ∀addr: [[bit_addr; carry]].
1262  ∀b: Bit.
1263  ∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
1264      b = b' →
1265      status_of_pseudo_status M cm ps sigma policy = s' →
1266      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
1267      map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
1268        set_arg_1 (BitVectorTrie Byte 16)
1269          (code_memory_of_pseudo_assembly_program cm sigma policy)
1270          s' addr b =
1271        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
1272  #cm #ps #addr #b
1273  cases (set_arg_1_status_of_pseudo_status' cm ps addr b) #_ #relevant
1274  @relevant
1275qed.
1276
1277lemma clock_status_of_pseudo_status:
1278 ∀M,cm,sigma,policy,s,s'.
1279  (status_of_pseudo_status M cm s sigma policy) = s' →
1280  clock …
1281   (code_memory_of_pseudo_assembly_program cm sigma policy)
1282   s'
1283  = clock … cm s.
1284  #M #cm #sigma #policy #s #s' #s_refl <s_refl //
1285qed.
1286
1287lemma set_clock_status_of_pseudo_status:
1288 ∀M,cm,sigma,policy,s,s',v,v'.
1289 status_of_pseudo_status M cm s sigma policy = s' →
1290 v = v' →
1291  set_clock …
1292   (code_memory_of_pseudo_assembly_program cm sigma policy)
1293   s' v
1294  = status_of_pseudo_status M cm (set_clock … cm s v') sigma policy.
1295  #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl <s_refl <v_refl //
1296qed.
1297
1298lemma let_pair_in_status_of_pseudo_status:
1299  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
1300    c = c' →
1301    (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') →
1302    let 〈left, right〉 ≝ c' in s' left right c' =
1303    status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy.
1304  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta //
1305qed.
1306
1307lemma let_pair_as_in_status_of_pseudo_status:
1308  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
1309  ∀c_refl: c = c'.
1310    (∀left, right, H. status_of_pseudo_status M cm (s left right H c') sigma policy = s' left right H c) →
1311    let 〈left, right〉 as H ≝ c' in s' left right H c =
1312    status_of_pseudo_status M cm (let 〈left, right〉 as H' ≝ c in s left right ? c) sigma policy.
1313  [2: >H' assumption ]
1314  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s'
1315  #destruct_assm destruct(destruct_assm) normalize nodelta
1316  #status_of_pseudo_status_assm >status_of_pseudo_status_assm //
1317qed.
1318
1319lemma if_then_else_status_of_pseudo_status:
1320  ∀M: internal_pseudo_address_map.
1321  ∀cm: pseudo_assembly_program.
1322  ∀sigma: Word → Word.
1323  ∀policy: Word → bool.
1324  ∀s, s', s'', s'''.
1325  ∀t, t': bool.
1326    t = t' →
1327    status_of_pseudo_status M cm s sigma policy = s' →
1328    status_of_pseudo_status M cm s'' sigma policy = s''' →
1329      if t then
1330        s'
1331      else
1332        s''' =
1333      status_of_pseudo_status M cm (if t' then s else s'') sigma policy.
1334  #M #cm #sigma #policy #s #s' #s'' #s''' #t #t' #t_refl #s_refl
1335  >t_refl normalize nodelta >s_refl cases t' normalize nodelta //
1336qed.
Note: See TracBrowser for help on using the repository browser.