source: src/ASM/AssemblyProof.ma @ 2272

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

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

File size: 60.6 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3include "ASM/StatusProofs.ma".
4include alias "arithmetics/nat.ma".
5
6let rec encoding_check
7  (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
8    (encoding: list Byte)
9      on encoding: Prop ≝
10  match encoding with
11  [ nil ⇒ final_pc = pc
12  | cons hd tl ⇒
13    let 〈new_pc, byte〉 ≝ next code_memory pc in
14      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
15  ].
16
17lemma encoding_check_append:
18  ∀code_memory: BitVectorTrie Byte 16.
19  ∀final_pc: Word.
20  ∀l1: list Byte.
21  ∀pc: Word.
22  ∀l2: list Byte.
23    encoding_check code_memory pc final_pc (l1@l2) →
24      let pc_plus_len ≝ add … pc (bitvector_of_nat … (length … l1)) in
25        encoding_check code_memory pc pc_plus_len l1 ∧
26          encoding_check code_memory pc_plus_len final_pc l2.
27  #code_memory #final_pc #l1 elim l1
28  [1:
29    #pc #l2
30    whd in ⊢ (????% → ?); #H
31    <add_zero
32    whd whd in ⊢ (?%?); /2/
33  |2:
34    #hd #tl #IH #pc #l2 * #H1 #H2
35(*    >add_SO in H2; #H2 *)
36    cases (IH … H2) #E1 #E2 %
37    [1:
38      % try @H1
39      <(add_bitvector_of_nat_Sm 16 (|tl|)) in E1;
40      <add_associative #assm assumption
41    |2:
42      <add_associative in E2;
43      <(add_bitvector_of_nat_Sm 16 (|tl|)) #assm
44      assumption
45    ]
46  ]
47qed.
48
49definition ticks_of_instruction ≝
50  λi.
51    let trivial_code_memory ≝ assembly1 i in
52    let trivial_status ≝ load_code_memory trivial_code_memory in
53      \snd (fetch trivial_status (zero ?)).
54
55lemma fetch_assembly:
56  ∀pc: Word.
57  ∀i: instruction.
58  ∀code_memory: BitVectorTrie Byte 16.
59  ∀assembled: list Byte.
60    assembled = assembly1 i →
61      let len ≝ length … assembled in
62      let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
63        encoding_check code_memory pc pc_plus_len assembled →
64          let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in
65           (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true.
66  cases daemon
67(* XXX: commented out as takes ages to typecheck
68  #pc #i #code_memory #assembled cases i [8: *]
69 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
70 [47,48,49:
71 |*: #arg @(subaddressing_mode_elim … arg)
72  [2,3,5,7,10,12,16,17,18,21,26,27,28,31,32,33,37,38,39,40,41,42,43,44,45,48,51,58,
73   59,60,63,64,65,66,67: #ARG]]
74 [4,5,6,7,8,9,10,11,12,13,22,23,24,27,28,39,40,41,42,43,44,45,46,47,48,49,50,51,52,
75  56,57,69,70,72: #arg2 @(subaddressing_mode_elim … arg2)
76  [1,2,4,7,9,11,12,14,15,17,18,19,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,
77   39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,
78   68,69,70,71: #ARG2]]
79 [1,2,19,20: #arg3 @(subaddressing_mode_elim … arg3) #ARG3]
80 normalize in ⊢ (???% → ?);
81 [92,94,42,93,95: @vsplit_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
82  normalize in ⊢ (???% → ?);]
83 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
84 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
85 whd in match fetch; normalize nodelta <H1 whd in ⊢ (match % with [ _ ⇒ ? ]);
86 [17,18,19,20,21,22,23,24,25,26,32,34,35,36,37,39: <H3]
87 try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl *)
88qed.
89
90let rec fetch_many
91  (code_memory: BitVectorTrie Byte 16) (final_pc: Word) (pc: Word)
92    (expected: list instruction)
93      on expected: Prop ≝
94  match expected with
95  [ nil ⇒ eq_bv … pc final_pc = true
96  | cons i tl ⇒
97    let pc' ≝ add 16 pc (bitvector_of_nat 16 (|assembly1 … i|)) in
98      (〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
99        fetch_many code_memory final_pc pc' tl)
100  ].
101         
102lemma fetch_assembly_pseudo':
103  ∀lookup_labels.
104  ∀sigma: Word → Word.
105  ∀policy: Word → bool.
106  ∀ppc.
107  ∀lookup_datalabels.
108  ∀pi.
109  ∀code_memory.
110  ∀len.
111  ∀assembled.
112  ∀instructions.
113    let pc ≝ sigma ppc in
114      instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi →
115        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi →
116          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
117            encoding_check code_memory pc pc_plus_len assembled →
118              fetch_many code_memory pc_plus_len pc instructions.
119  #lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
120  normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
121  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
122  >len_refl >assembled_refl -len_refl
123  generalize in match (add 16 (sigma ppc)
124    (bitvector_of_nat 16
125     (|flatten (Vector bool 8)
126       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
127  #final_pc
128  generalize in match (sigma ppc); elim instructions
129  [1:
130    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
131  |2:
132    #i #tl #IH #pc #H whd
133    cases (encoding_check_append ????? H) -H #H1 #H2
134    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);   
135    cases (fetch ??) * #instr #pc' #ticks
136    #H3 lapply (H3 H1) -H3 normalize nodelta #H3
137    lapply (conjunction_true ?? H3) * #H4 #H5
138    lapply (conjunction_true … H4) * #B1 #B2
139    >(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) %
140    >(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2
141  ]
142qed.
143
144lemma fetch_assembly_pseudo:
145  ∀program: pseudo_assembly_program.
146  ∀sigma: Word → Word.
147  ∀policy: Word → bool.
148  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
149  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
150  ∀ppc.∀ppc_ok.
151  ∀code_memory.
152  let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
153  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
154  let pc ≝ sigma ppc in
155  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
156  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
157  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
158    encoding_check code_memory pc pc_plus_len assembled →
159      fetch_many code_memory pc_plus_len pc instructions.
160  #program #sigma #policy
161  @pair_elim #labels #costs #create_label_cost_map_refl
162  letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory
163  letin lookup_datalabels ≝ (λx.?)
164  letin pi ≝ (fst ???)
165  letin pc ≝ (sigma ?)
166  letin instructions ≝ (expand_pseudo_instruction ??????)
167  @pair_elim #len #assembled #assembled_refl normalize nodelta
168  #H
169  generalize in match
170   (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
171  #X destruct normalize nodelta @X try % <assembled_refl try % assumption
172qed.
173
174definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
175  λpseudo_instruction.
176    match pseudo_instruction with
177    [ Comment c ⇒ False
178    | Cost c ⇒ False
179    | _ ⇒ True
180    ].
181
182(* This is a non trivial consequence of fetch_assembly_pseudo +
183   load_code_memory_ok because of the finite amount of memory. In
184   particular the case when the compiled program exhausts the
185   code memory is very tricky. It also requires monotonicity of
186   sigma in the out-of-bounds region too. *)     
187lemma assembly_ok:
188  ∀program.
189  ∀length_proof: |\snd program| ≤ 2^16.
190  ∀sigma: Word → Word.
191  ∀policy: Word → bool.
192  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
193  ∀assembled.
194  ∀costs': BitVectorTrie costlabel 16.
195  let 〈preamble, instr_list〉 ≝ program in
196  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
197  let datalabels ≝ construct_datalabels preamble in
198  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
199    〈assembled,costs'〉 = assembly program sigma policy →
200      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
201        let code_memory ≝ load_code_memory assembled in
202        let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
203          ∀ppc.∀ppc_ok.
204            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
205            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
206            let pc ≝ sigma ppc in
207            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
208              encoding_check code_memory pc pc_plus_len assembled ∧
209                  sigma newppc = add … pc (bitvector_of_nat … len).
210  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
211  cases (assembly program sigma policy) * #assembled' #costs''
212  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
213  cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
214  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
215  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
216  * * #assembly_ok1 #assembly_ok3 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
217  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
218  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
219  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
220  >eq_fetch_pseudo_instruction
221  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ? ∧ ∀j.∀H:j<|assembledi|.?) → ?)
222  >eq_assembly_1_pseudoinstruction
223  whd in ⊢ (% → ?); * #assembly_ok4 #assembly_ok
224  %
225  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
226      >snd_fetch_pseudo_instruction
227      cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
228      #spw1 #_ >spw1 -spw1 @eq_f @eq_f
229      >eq_fetch_pseudo_instruction whd in match instruction_size;
230      normalize nodelta >create_label_cost_refl
231      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
232      [>eq_assembly_1_pseudoinstruction % | skip]
233  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
234    #load_code_memory_ok
235    lapply (fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) #EQlen
236    (* Nice statement here *)
237    cut (∀j. ∀H: j < |assembled|.
238          nth_safe Byte j assembled H =
239          \snd (next (load_code_memory assembled')
240          (bitvector_of_nat 16
241           (nat_of_bitvector …
242            (add … (sigma ppc) (bitvector_of_nat … j))))))
243    [1: #j #H cases (assembly_ok … H) #K -assembly_ok #assembly_ok <load_code_memory_ok
244        [ @assembly_ok | skip ]
245    |2:
246      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
247      elim assembled
248      [1:
249        #pc #_ whd <add_zero %
250      | #hd #tl #IH #pc #H %
251         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
252           >H -H whd in ⊢ (??%?); <add_zero //
253         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
254           [2: <add_bitvector_of_nat_Sm @add_associative ]
255           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
256           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
257           >add_associative % ]]]]
258qed.
259
260(* XXX: should we add that costs = costs'? *)
261lemma fetch_assembly_pseudo2:
262  ∀program.
263  ∀length_proof: |\snd program| ≤ 2^16.
264  ∀sigma.
265  ∀policy.
266  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
267  ∀ppc.∀ppc_ok.
268  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
269  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
270  let code_memory ≝ load_code_memory assembled in
271  let data_labels ≝ construct_datalabels (\fst program) in
272  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
273  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
274  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
275  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
276    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
277  * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
278  @pair_elim #labels #costs #create_label_map_refl
279  @pair_elim #assembled #costs' #assembled_refl
280  letin code_memory ≝ (load_code_memory ?)
281  letin data_labels ≝ (construct_datalabels ?)
282  letin lookup_labels ≝ (λx. ?)
283  letin lookup_datalabels ≝ (λx. ?)
284  @pair_elim #pi #newppc #fetch_pseudo_refl
285  lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
286  normalize nodelta try assumption
287  >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H
288  lapply (H (sym_eq … assembled_refl)) -H
289  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
290  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
291  #len #assembledi #EQ4 #H
292  lapply (H ppc) >fetch_pseudo_refl #H
293  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy)
294  >create_label_map_refl #X lapply (X ppc ppc_ok (load_code_memory assembled)) -X
295  >EQ4 #H1 cases (H ppc_ok)
296  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
297  >fetch_pseudo_refl in H1; #assm @assm assumption
298qed.
299
300inductive upper_lower: Type[0] ≝
301  | upper: upper_lower
302  | lower: upper_lower.
303
304definition eq_upper_lower:
305    upper_lower → upper_lower → bool ≝
306  λleft: upper_lower.
307  λright: upper_lower.
308  match left with
309  [ upper ⇒
310    match right with
311    [ upper ⇒ true
312    | _     ⇒ false
313    ]
314  | lower ⇒
315    match right with
316    [ lower ⇒ true
317    | _     ⇒ false
318    ]
319  ].
320
321lemma eq_upper_lower_true_to_eq:
322  ∀left: upper_lower.
323  ∀right: upper_lower.
324    eq_upper_lower left right = true → left = right.
325  * * normalize try (#_ %)
326  #absurd destruct(absurd)
327qed.
328
329lemma eq_upper_lower_false_to_neq:
330  ∀left: upper_lower.
331  ∀right: upper_lower.
332    eq_upper_lower left right = false → left ≠ right.
333  * * normalize try (#absurd destruct(absurd))
334  @nmk #absurd destruct(absurd)
335qed.
336
337(* XXX: if upper then the byte in the entry is the least significant byte of the address and
338        the byte in the status is the most significant, otherwise if lower then the
339        other way around
340*)
341definition address_entry ≝ upper_lower × Byte.
342
343definition eq_accumulator_address_map_entry:
344    option address_entry → option address_entry → bool ≝
345  λleft.
346  λright.
347    match left with
348    [ None                   ⇒
349      match right with
350      [ None ⇒ true
351      | _    ⇒ false
352      ]
353    | Some upper_lower_addr ⇒
354      let 〈upper_lower, addr〉 ≝ upper_lower_addr in
355      match right with
356      [ Some upper_lower_addr' ⇒
357        let 〈upper_lower', addr'〉 ≝ upper_lower_addr' in
358          eq_upper_lower upper_lower upper_lower' ∧ eq_bv … addr addr'
359      | _                          ⇒ false
360      ]
361    ].
362
363lemma eq_accumulator_address_map_entry_true_to_eq:
364  ∀left: option address_entry.
365  ∀right: option address_entry.
366    eq_accumulator_address_map_entry left right = true → left = right.
367  #left #right cases left cases right
368  [1:
369    #_ %
370  |2,3:
371    * * #word normalize #absurd destruct(absurd)
372  |4:
373    * * #word * * #word'
374    [2,3:
375      #absurd normalize in absurd; destruct(absurd)
376    ]
377    normalize change with (eq_bv 8 ?? = true → ?)
378    #relevant >(eq_bv_eq … relevant) %
379  ]
380qed.
381
382lemma eq_bv_false_to_neq:
383  ∀n: nat.
384  ∀left, right: BitVector n.
385    eq_bv n left right = false → left ≠ right.
386  #n #left elim left
387  [1:
388    #right >(BitVector_O … right) normalize #absurd destruct(absurd)
389  |2:
390    #n' #hd #tl #inductive_hypothesis #right
391    cases (BitVector_Sn … right) #hd' * #tl' #right_refl
392    >right_refl normalize
393    cases hd normalize nodelta
394    cases hd' normalize nodelta
395    [2,3:
396      #_ @nmk #absurd destruct(absurd)
397    ]
398    change with (eq_bv ??? = false → ?)
399    #relevant lapply (inductive_hypothesis … relevant)
400    #tl_neq_assm @nmk #tl_eq_assm cases tl_neq_assm
401    #tl_eq_assm' @tl_eq_assm' destruct(tl_eq_assm) %
402  ]
403qed.
404   
405lemma eq_accumulator_address_map_entry_false_to_neq:
406  ∀left: option address_entry.
407  ∀right: option address_entry.
408    eq_accumulator_address_map_entry left right = false → left ≠ right.
409  #left #right cases left cases right
410  [1:
411    normalize #absurd destruct(absurd)
412  |2,3:
413    * * #word normalize #_ % #absurd destruct(absurd)
414  |4:
415    * * #word * * #word' normalize
416    [2,3:
417      #_ % #absurd destruct(absurd)
418    ]
419    change with (eq_bv ??? = false → ?)
420    #eq_bv_false_assm lapply (eq_bv_false_to_neq … eq_bv_false_assm)
421    #word_neq_assm % @Some_Some_elim #address_eq_assm cases word_neq_assm
422    #word_eq_assm @word_eq_assm destruct(address_eq_assm) %
423  ]
424qed.
425
426(* XXX: changed this type.  Bool specifies whether byte is first or second
427        component of an address, and the Word is the pseudoaddress that it
428        corresponds to.  Second component is the same principle for the accumulator
429        A.
430*)
431definition internal_pseudo_address_map ≝
432  (* low, high, acc *)
433  (BitVectorTrie address_entry 7) × (BitVectorTrie address_entry 7) × (option address_entry).
434
435include alias "ASM/BitVectorTrie.ma".
436 
437include "common/AssocList.ma".
438
439axiom bvt_map2:
440  ∀A, B, C: Type[0].
441  ∀n: nat.
442  ∀bvt_1: BitVectorTrie A n.
443  ∀bvt_2: BitVectorTrie B n.
444  ∀f: ∀a: option A. ∀b: option B. option C.
445    BitVectorTrie C n.
446
447axiom is_in_domain:
448  ∀A: Type[0].
449  ∀n: nat.
450  ∀bvt: BitVectorTrie A n.
451  ∀b: BitVector n.
452    Prop.
453
454axiom bvt_map2_function_extensionality:
455  ∀A, B, C: Type[0].
456  ∀n: nat.
457  ∀bvt_1: BitVectorTrie A n.
458  ∀bvt_2, bvt_2': BitVectorTrie B n.
459  ∀f: ∀a: option A. ∀b: option B. option C.
460    (∀addr.
461      is_in_domain … bvt_1 addr ∨ is_in_domain … bvt_2 addr ∨ is_in_domain … bvt_2' addr →
462        f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2) = f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2')) →
463          bvt_map2 … bvt_1 bvt_2 f = bvt_map2 … bvt_1 bvt_2' f.
464
465definition internal_ram_of_pseudo_internal_ram:
466    ∀sigma: Word → Word.
467    ∀ram: BitVectorTrie Byte 7.
468    ∀map: BitVectorTrie address_entry 7.
469      BitVectorTrie Byte 7 ≝
470  λsigma, ram, map.
471      bvt_map2 ??? ? ram map (λv. λul_addr.
472        match
473        match ul_addr with
474        [ None ⇒ v
475        | Some ul_addr' ⇒
476          let 〈ul, addr〉 ≝ ul_addr' in
477          let v ≝ match v with [ None ⇒ zero … | Some v ⇒ v ] in
478          match ul with
479          [ upper ⇒
480            let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (v@@addr)) in
481              Some … high
482          | lower ⇒
483            let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (addr@@v)) in
484              Some … low
485          ]
486        ] with
487        [ None ⇒ None …
488        | Some v ⇒
489          if eq_bv … v (zero …) then
490            None …
491          else
492            Some … v
493        ]).
494
495definition low_internal_ram_of_pseudo_low_internal_ram:
496    ∀M: internal_pseudo_address_map.
497    ∀sigma: Word → Word.
498    ∀ram: BitVectorTrie Byte 7.
499      BitVectorTrie Byte 7 ≝
500  λM, sigma, ram.
501    let 〈low, high, accA〉 ≝ M in
502      internal_ram_of_pseudo_internal_ram sigma ram low.
503
504definition high_internal_ram_of_pseudo_high_internal_ram:
505    ∀M: internal_pseudo_address_map.
506    ∀sigma: Word → Word.
507    ∀ram: BitVectorTrie Byte 7.
508      BitVectorTrie Byte 7 ≝
509  λM, sigma, ram.
510    let 〈low, high, accA〉 ≝ M in
511      internal_ram_of_pseudo_internal_ram sigma ram high.
512
513(*
514axiom low_internal_ram_of_pseudo_internal_ram_hit:
515 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.
516  lookup_opt ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉  →
517   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in
518   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
519   let bl ≝ lookup ? 7 addr ram (zero 8) in
520   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
521   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (sigma points_to) in
522     if eq_upper_lower upper_lower upper then
523       (pbl = higher) ∧ (bl = phigher)
524     else
525       (pbl = lower) ∧ (bl = plower).
526*)
527
528(* changed from add to sub *)
529axiom low_internal_ram_of_pseudo_internal_ram_miss:
530 ∀T.∀M:internal_pseudo_address_map.∀sigma. ∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
531  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in
532    lookup_opt … addr (\fst (\fst M)) = None … →
533      lookup … addr ram (zero …) = lookup … addr (low_internal_ram … s) (zero ?).
534
535definition exists:
536    ∀A: Type[0].
537    ∀n: nat.
538    ∀v: BitVector n.
539    ∀bvt: BitVectorTrie A n.
540      bool ≝
541  λA, n, v, bvt.
542    match lookup_opt … v bvt with
543    [ None ⇒ false
544    | _    ⇒ true
545    ].
546
547definition data_or_address ≝
548  λT.
549  λM: internal_pseudo_address_map.
550  λcm.
551  λs: PreStatus T cm.
552  λaddr: addressing_mode.
553  let 〈low, high, accA〉 ≝ M in
554  match addr return λx. option (option address_entry) with
555    [ DIRECT d ⇒
556       let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
557         match head' … hd with
558         [ true ⇒
559             if eq_bv … d (bitvector_of_nat … 224) then
560               Some … accA
561             else
562               Some … (None …)
563         | false ⇒ Some … (lookup_opt … seven_bits low)
564         ]
565    | INDIRECT i ⇒
566        let d ≝ get_register … s [[false;false;i]] in
567        let address ≝ bit_address_of_register … s [[false;false;i]] in
568          if ¬exists … address low then
569            let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
570              if head' … 0 bit_one then
571                Some … (lookup_opt … seven_bits high)
572              else
573                Some … (lookup_opt … seven_bits low)
574          else
575            None ?
576    | EXT_INDIRECT e ⇒
577        let address ≝ bit_address_of_register … s [[false;false;e]] in
578          if ¬exists … address low then
579            Some … (None …)
580          else
581            None ?
582    | REGISTER r ⇒
583        let address ≝ bit_address_of_register … s r in
584          Some … (lookup_opt … address low)
585    | ACC_A ⇒ Some … accA
586    | ACC_B ⇒ Some … (None …)
587    | DPTR ⇒ Some … (None …)
588    | DATA _ ⇒ Some … (None …)
589    | DATA16 _ ⇒ Some … (None …)
590    | ACC_DPTR ⇒ Some … (None …)
591    | ACC_PC ⇒ Some … (None …)
592    | EXT_INDIRECT_DPTR ⇒ Some … (None …)
593    | INDIRECT_DPTR ⇒ Some … (None …)
594    | CARRY ⇒ Some … (None …)
595    | BIT_ADDR b ⇒
596      let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
597      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
598        if head' bool 0 bit_one then
599            if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *)
600              Some … accA
601            else
602              Some … (None …)
603        else
604          let address' ≝ [[true; false; false]]@@four_bits in
605            Some … (lookup_opt … address' low)
606    | N_BIT_ADDR b ⇒
607      let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
608      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
609        if head' bool 0 bit_one then
610            if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *)
611              Some … accA
612            else
613              Some … (None …)
614        else
615          let address' ≝ [[true; false; false]]@@four_bits in
616            Some … (lookup_opt … address' low)
617    | RELATIVE _ ⇒ Some … (None …)
618    | ADDR11 _ ⇒ Some … (None …)
619    | ADDR16 _ ⇒ Some … (None …)
620    ].
621
622definition assert_data ≝
623  λT.
624  λM: internal_pseudo_address_map.
625  λcm.
626  λs: PreStatus T cm.
627  λaddr: addressing_mode.
628    match data_or_address T M cm s addr with
629    [ None   ⇒ false
630    | Some s ⇒
631      match s with
632      [ None ⇒ true
633      | _    ⇒ false
634      ]
635    ].
636   
637definition insert_into_internal_ram:
638  ∀addr: Byte.
639  ∀v: address_entry.
640  ∀M: internal_pseudo_address_map.
641    internal_pseudo_address_map ≝
642  λaddr, v, M.
643    let 〈low, high, accA〉 ≝ M in
644    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
645      if head' … bit_one then
646        〈insert … seven_bits v low, high, accA〉
647      else
648        〈low, insert … seven_bits v high, accA〉.
649   
650axiom delete:
651  ∀A: Type[0].
652  ∀n: nat.
653  ∀b: BitVector n.
654    BitVectorTrie A n → BitVectorTrie A n.
655
656definition delete_from_internal_ram:
657    ∀addr: Byte.
658    ∀M: internal_pseudo_address_map.
659      internal_pseudo_address_map ≝
660  λaddr, M.
661    let 〈low, high, accA〉 ≝ M in
662    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
663      if head' … bit_one then
664        〈delete … seven_bits low, high, accA〉
665      else
666        〈low, delete … seven_bits high, accA〉.
667
668definition overwrite_or_delete_from_internal_ram:
669    ∀addr: Byte.
670    ∀v: option address_entry.
671    ∀M: internal_pseudo_address_map.
672      internal_pseudo_address_map ≝
673  λaddr, v, M.
674    let 〈low, high, accA〉 ≝ M in
675      match v with
676      [ None ⇒ delete_from_internal_ram addr M
677      | Some v' ⇒ insert_into_internal_ram addr v' M
678      ].
679
680definition lookup_from_internal_ram:
681    ∀addr: Byte.
682    ∀M: internal_pseudo_address_map.
683      option address_entry ≝
684  λaddr, M.
685    let 〈low, high, accA〉 ≝ M in
686    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
687      if head' … bit_one then
688        lookup_opt … seven_bits high
689      else
690        lookup_opt … seven_bits low.
691   
692definition next_internal_pseudo_address_map0 ≝
693  λT.
694  λcm:T.
695  λaddr_of: Identifier → PreStatus T cm → Word.
696  λfetched.
697  λM: internal_pseudo_address_map.
698  λs: PreStatus T cm.
699  let 〈low, high, accA〉 ≝ M in
700   match fetched with
701    [ Comment _ ⇒ Some ? M
702    | Cost _ ⇒ Some … M
703    | Jmp _ ⇒ Some … M
704    | Call a ⇒
705      let a' ≝ addr_of a s in
706      let 〈upA, lowA〉 ≝ vsplit bool 8 8 a' in
707        Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) 〈lower, upA〉
708                (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) 〈upper, lowA〉 M))
709    | Mov _ _ ⇒ Some … M
710    | Instruction instr ⇒
711      match instr return λx. option internal_pseudo_address_map with
712       [ ADD addr1 addr2 ⇒
713         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
714           Some ? M
715         else
716           None ?
717       | ADDC addr1 addr2 ⇒
718         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
719           Some ? M
720         else
721           None ?
722       | SUBB addr1 addr2 ⇒
723         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
724           Some ? M
725         else
726           None ?
727       | INC addr1 ⇒
728         if assert_data T M ? s addr1 then
729           Some ? M
730         else
731           None ?
732       | DEC addr1 ⇒
733         if assert_data T M … s addr1 then
734           Some ? M
735         else
736           None ?
737       | MUL addr1 addr2 ⇒
738         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
739           Some ? M
740         else
741           None ?
742       | DIV addr1 addr2 ⇒
743         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
744           Some ? M
745         else
746           None ?
747       | DA addr1 ⇒
748         if assert_data T M … s addr1 then
749           Some ? M
750         else
751           None ?
752       | JC addr1 ⇒ Some ? M
753       | JNC addr1 ⇒ Some ? M
754       | JB addr1 addr2 ⇒ Some ? M
755       | JNB addr1 addr2 ⇒ Some ? M
756       | JBC addr1 addr2 ⇒ Some ? M
757       | JZ addr1 ⇒ Some ? M
758       | JNZ addr1 ⇒ Some ? M
759       | CJNE addr1 addr2 ⇒
760         match addr1 with
761         [ inl l ⇒
762           let 〈left, right〉 ≝ l in
763             if assert_data T M … s left ∧ assert_data T M … s right then
764               Some ? M
765             else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then
766               Some ? M
767             else
768               None ?
769         | inr r ⇒
770           let 〈left, right〉 ≝ r in
771             if assert_data T M … s left ∧ assert_data T M … s right then
772               Some ? M
773             else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then
774               Some ? M
775             else
776               None ?
777         ]
778       | DJNZ addr1 addr2 ⇒
779         if assert_data T M … s addr1 then
780           Some ? M
781         else
782           None ?
783       | CLR addr1 ⇒
784         if assert_data T M … s addr1 then
785           Some ? M
786         else
787           None ?
788       | CPL addr1 ⇒
789         if assert_data T M … s addr1 then
790           Some ? M
791         else
792           None ?
793       | RL addr1 ⇒
794         if assert_data T M … s addr1 then
795           Some ? M
796         else
797           None ?
798       | RLC addr1 ⇒
799         if assert_data T M … s addr1 then
800           Some ? M
801         else
802           None ?
803       | RR addr1 ⇒
804         if assert_data T M … s addr1 then
805           Some ? M
806         else
807           None ?
808       | RRC addr1 ⇒
809         if assert_data T M … s addr1 then
810           Some ? M
811         else
812           None ?
813       | SWAP addr1 ⇒
814         if assert_data T M … s addr1 then
815           Some ? M
816         else
817           None ?
818       | SETB addr1 ⇒
819         if assert_data T M … s addr1 then
820           Some ? M
821         else
822           None ?
823       (* XXX: need to track addresses pushed and popped off the stack? *)
824       | PUSH addr1 ⇒
825         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
826         [ DIRECT d ⇒ λproof.
827           let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
828             if head' … bit_one then
829               if eq_bv … seven_bits (bitvector_of_nat … 224) then
830                 Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) accA M)
831               else
832                 Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M)
833             else
834               match lookup_from_internal_ram … d M with
835               [ None ⇒
836                   Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M)
837               | Some ul_addr ⇒
838                   Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) ul_addr M)
839               ]
840         | _ ⇒ λother: False. ⊥
841         ] (subaddressing_modein … addr1)
842       | POP addr1 ⇒
843         let sp ≝ get_8051_sfr ?? s SFR_SP in
844         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
845         [ DIRECT d ⇒ λproof.
846           let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
847             if head' … bit_one then
848               if eq_bv … d (bitvector_of_nat … 224) then
849                 Some … 〈low, high, lookup_from_internal_ram … sp M〉
850               else
851                 match lookup_from_internal_ram sp M with
852                 [ None ⇒ Some ? M
853                 | _    ⇒ None ?
854                 ]
855             else
856               Some … (overwrite_or_delete_from_internal_ram d (lookup_from_internal_ram … sp M) M)
857         | _ ⇒ λother: False. ⊥
858         ] (subaddressing_modein … addr1)
859       | XCH addr1 addr2 ⇒
860         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
861           Some ? M
862         else
863           None ?
864       | XCHD addr1 addr2 ⇒
865         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
866           Some ? M
867         else
868           None ?
869      | RET ⇒
870        let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
871        let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
872        match lookup_from_internal_ram sp_minus_1 M with
873        [ None ⇒ None …
874        | Some low_addr_high ⇒
875            match lookup_from_internal_ram sp_minus_2 M with
876            [ None ⇒ None …
877            | Some high_addr_low ⇒
878              let 〈low, addr_high〉 ≝ low_addr_high in
879              let 〈high, addr_low〉 ≝ high_addr_low in
880              let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
881              let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
882                if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
883                  Some ? M
884                else
885                  None ?
886            ]
887        ]
888      | RETI ⇒
889        let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
890        let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
891        match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M with
892        [ None ⇒ None …
893        | Some low_addr_high ⇒
894            match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) M with
895            [ None ⇒ None …
896            | Some high_addr_low ⇒
897              let 〈low, addr_high〉 ≝ low_addr_high in
898              let 〈high, addr_low〉 ≝ high_addr_low in
899              let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
900              let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
901                if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
902                  Some ? M
903                else
904                  None ?
905            ]
906        ]
907      | NOP ⇒ Some … M
908      | MOVX addr1 ⇒
909        match addr1 with
910        [ inl l ⇒
911            Some ? 〈low, high, None …〉
912        | inr r ⇒
913          let 〈others, acc_a〉 ≝ r in
914            if assert_data T M … s acc_a then
915              Some ? M
916            else
917              None ?
918        ]
919      | XRL addr1 ⇒
920        match addr1 with
921        [ inl l ⇒
922          let 〈acc_a, others〉 ≝ l in
923          let acc_a_ok ≝ assert_data T M … s acc_a in
924          let others_ok ≝ assert_data T M … s others in
925          if acc_a_ok ∧ others_ok then
926            Some ? M
927          else
928            None ?
929        | inr r ⇒
930          let 〈direct, others〉 ≝ r in
931          let direct_ok ≝ assert_data T M … s direct in
932          let others_ok ≝ assert_data T M … s others in
933          if direct_ok ∧ others_ok then
934            Some ? M
935          else
936            None ?
937        ]
938      | ORL addr1 ⇒
939        match addr1 with
940        [ inl l ⇒
941          match l with
942          [ inl l ⇒
943            let 〈acc_a, others〉 ≝ l in
944            let acc_a_ok ≝ assert_data T M … s acc_a in
945            let others_ok ≝ assert_data T M … s others in
946            if acc_a_ok ∧ others_ok then
947              Some ? M
948            else
949              None ?
950          | inr r ⇒
951            let 〈direct, others〉 ≝ r in
952            let direct_ok ≝ assert_data T M … s direct in
953            let others_ok ≝ assert_data T M … s others in
954            if direct_ok ∧ others_ok then
955              Some ? M
956            else
957              None ?
958          ]
959        | inr r ⇒
960          let 〈carry, others〉 ≝ r in
961          let carry_ok ≝ assert_data T M … s carry in
962          let others_ok ≝ assert_data T M … s others in
963          if carry_ok ∧ others_ok then
964            Some ? M
965          else
966            None ?
967        ]
968      | ANL addr1 ⇒
969        match addr1 with
970        [ inl l ⇒
971          match l with
972          [ inl l ⇒
973            let 〈acc_a, others〉 ≝ l in
974            let acc_a_ok ≝ assert_data T M … s acc_a in
975            let others_ok ≝ assert_data T M … s others in
976            if acc_a_ok ∧ others_ok then
977              Some ? M
978            else
979              None ?
980          | inr r ⇒
981            let 〈direct, others〉 ≝ r in
982            let direct_ok ≝ assert_data T M … s direct in
983            let others_ok ≝ assert_data T M … s others in
984            if direct_ok ∧ others_ok then
985              Some ? M
986            else
987              None ?
988          ]
989        | inr r ⇒
990          let 〈carry, others〉 ≝ r in
991          let carry_ok ≝ assert_data T M … s carry in
992          let others_ok ≝ assert_data T M … s others in
993          if carry_ok ∧ others_ok then
994            Some ? M
995          else
996            None ?
997        ]
998      | MOV addr1 ⇒
999        (* XXX: wrong *)
1000        match addr1 with
1001        [ inl l ⇒
1002          match l with
1003          [ inl l' ⇒
1004            match l' with
1005            [ inl l'' ⇒
1006              match l'' with
1007              [ inl l''' ⇒
1008                match l''' with
1009                [ inl l'''' ⇒
1010                  let 〈acc_a, others〉 ≝ l'''' in
1011                    match data_or_address T M … s others with
1012                    [ None ⇒ None ?
1013                    | Some s ⇒
1014                        Some … 〈low, high, s〉
1015                    ]
1016                | inr r ⇒
1017                  let 〈others, others'〉 ≝ r in
1018                  let address ≝
1019                    match others return λx. bool_to_Prop (is_in … [[ registr; indirect ]] x) → ? with
1020                    [ REGISTER r ⇒ λproof. false:::bit_address_of_register … s r
1021                    | INDIRECT i ⇒ λproof. get_register … s [[false; false; i]]
1022                    | _ ⇒ λother: False. ⊥
1023                    ] (subaddressing_modein … others)
1024                  in
1025                    match data_or_address T M … s others' with
1026                    [ None ⇒ None ?
1027                    | Some s ⇒
1028                        Some … (overwrite_or_delete_from_internal_ram address s M)
1029                    ]
1030                ]
1031              | inr r ⇒
1032                let 〈direct', others〉 ≝ r in
1033                  match direct' return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
1034                  [ DIRECT d ⇒ λproof.
1035                    match data_or_address T M … s others with
1036                    [ None ⇒ None ?
1037                    | Some s' ⇒
1038                        let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
1039                          if head' … bit_one then
1040                            if eq_bv … d (bitvector_of_nat … 224) then
1041                              Some … 〈low, high, s'〉
1042                            else
1043                              match s' with
1044                              [ None ⇒ Some ? M
1045                              | Some s'' ⇒ None ?
1046                              ]
1047                          else
1048                            Some … (overwrite_or_delete_from_internal_ram d s' M)
1049                    ]
1050                  | _ ⇒ λother: False. ⊥
1051                  ] (subaddressing_modein … direct')
1052              ]
1053            | inr r ⇒ Some … M
1054            ]
1055          | inr r ⇒
1056            let 〈carry, bit_addr〉 ≝ r in
1057            if assert_data T M … s bit_addr then
1058              Some ? M
1059            else
1060              None ?
1061          ]
1062        | inr r ⇒
1063          let 〈bit_addr, carry〉 ≝ r in
1064          if assert_data T M … s bit_addr then
1065            Some ? M
1066          else
1067            None ?
1068        ]
1069      ]
1070    ].
1071    cases other
1072qed.
1073
1074definition next_internal_pseudo_address_map ≝
1075 λM:internal_pseudo_address_map.
1076 λcm.
1077 λaddr_of.
1078 λs:PseudoStatus cm.
1079 λppc_ok.
1080    next_internal_pseudo_address_map0 ? cm addr_of
1081     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
1082
1083definition code_memory_of_pseudo_assembly_program:
1084    ∀pap:pseudo_assembly_program.
1085      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
1086  λpap.
1087  λsigma.
1088  λpolicy.
1089    let p ≝ pi1 … (assembly pap sigma policy) in
1090      load_code_memory (\fst p).
1091
1092definition sfr_8051_of_pseudo_sfr_8051 ≝
1093  λM: internal_pseudo_address_map.
1094  λsfrs: Vector Byte 19.
1095  λsigma: Word → Word.
1096    match \snd M with
1097    [ None ⇒ sfrs
1098    | Some upper_lower_address ⇒
1099      let index ≝ sfr_8051_index SFR_ACC_A in
1100      let acc_a ≝ get_index_v … sfrs index ? in
1101      let 〈upper_lower, address〉 ≝ upper_lower_address in
1102        if eq_upper_lower upper_lower upper then
1103          let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (acc_a@@address)) in
1104            set_index Byte 19 sfrs index high ?
1105        else
1106          let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (address@@acc_a)) in
1107            set_index Byte 19 sfrs index low ?
1108    ].
1109  //
1110qed.
1111
1112definition status_of_pseudo_status:
1113    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
1114      ∀sigma: Word → Word. ∀policy: Word → bool.
1115        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
1116  λM.
1117  λpap.
1118  λps.
1119  λsigma.
1120  λpolicy.
1121  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
1122  let pc ≝ sigma (program_counter … ps) in
1123  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … ps) in
1124  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M sigma (high_internal_ram … ps) in
1125     mk_PreStatus (BitVectorTrie Byte 16)
1126      cm
1127      lir
1128      hir
1129      (external_ram … ps)
1130      pc
1131      (sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma)
1132      (special_function_registers_8052 … ps)
1133      (p1_latch … ps)
1134      (p3_latch … ps)
1135      (clock … ps).
1136
1137(*
1138definition write_at_stack_pointer':
1139 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1140  λM: Type[0].
1141  λs: PreStatus M.
1142  λv: Byte.
1143    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
1144    let bit_zero ≝ get_index_v… nu O ? in
1145    let bit_1 ≝ get_index_v… nu 1 ? in
1146    let bit_2 ≝ get_index_v… nu 2 ? in
1147    let bit_3 ≝ get_index_v… nu 3 ? in
1148      if bit_zero then
1149        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1150                              v (low_internal_ram ? s) in
1151          set_low_internal_ram ? s memory
1152      else
1153        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1154                              v (high_internal_ram ? s) in
1155          set_high_internal_ram ? s memory.
1156  [ cases l0 %
1157  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1158qed.
1159
1160definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1161 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1162
1163  λticks_of.
1164  λs.
1165  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1166  let ticks ≝ ticks_of (program_counter ? s) in
1167  let s ≝ set_clock ? s (clock ? s + ticks) in
1168  let s ≝ set_program_counter ? s pc in
1169    match instr with
1170    [ Instruction instr ⇒
1171       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1172    | Comment cmt ⇒ s
1173    | Cost cst ⇒ s
1174    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1175    | Call call ⇒
1176      let a ≝ address_of_word_labels s call in
1177      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1178      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1179      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
1180      let s ≝ write_at_stack_pointer' ? s pc_bl in
1181      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1182      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1183      let s ≝ write_at_stack_pointer' ? s pc_bu in
1184        set_program_counter ? s a
1185    | Mov dptr ident ⇒
1186       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1187    ].
1188 [
1189 |2,3,4: %
1190 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1191 |
1192 | %
1193 ]
1194 cases not_implemented
1195qed.
1196*)
1197
1198(*
1199lemma execute_code_memory_unchanged:
1200 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1201 #ticks #ps whd in ⊢ (??? (??%))
1202 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1203  (program_counter pseudo_assembly_program ps)) #instr #pc
1204 whd in ⊢ (??? (??%)) cases instr
1205  [ #pre cases pre
1206     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1207       cases (vsplit ????) #z1 #z2 %
1208     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1209       cases (vsplit ????) #z1 #z2 %
1210     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1211       cases (vsplit ????) #z1 #z2 %
1212     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1213       [ #x1 whd in ⊢ (??? (??%))
1214     | *: cases not_implemented
1215     ]
1216  | #comment %
1217  | #cost %
1218  | #label %
1219  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1220    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1221    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
1222    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1223    (* CSC: ??? *)
1224  | #dptr #label (* CSC: ??? *)
1225  ]
1226  cases not_implemented
1227qed.
1228*)
1229
1230(* XXX: check values returned for conditional jumps below! They are wrong,
1231        find correct values *)
1232definition ticks_of0:
1233    ∀p:pseudo_assembly_program.
1234      (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
1235  λprogram: pseudo_assembly_program.
1236  λlookup_labels: Identifier → Word.
1237  λsigma.
1238  λpolicy.
1239  λppc: Word.
1240  λfetched.
1241    match fetched with
1242    [ Instruction instr ⇒
1243      match instr with
1244      [ JC lbl ⇒
1245        let lookup_address ≝ sigma (lookup_labels lbl) in
1246        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1247        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1248          if sj_possible then
1249            〈2, 2〉
1250          else
1251            〈4, 4〉
1252      | JNC lbl ⇒
1253        let lookup_address ≝ sigma (lookup_labels lbl) in
1254        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1255        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1256          if sj_possible then
1257            〈2, 2〉
1258          else
1259            〈4, 4〉
1260      | JB bit lbl ⇒
1261        let lookup_address ≝ sigma (lookup_labels lbl) in
1262        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1263        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1264          if sj_possible then
1265            〈2, 2〉
1266          else
1267            〈4, 4〉
1268      | JNB bit lbl ⇒
1269        let lookup_address ≝ sigma (lookup_labels lbl) in
1270        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1271        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1272          if sj_possible then
1273            〈2, 2〉
1274          else
1275            〈4, 4〉
1276      | JBC bit lbl ⇒
1277        let lookup_address ≝ sigma (lookup_labels lbl) in
1278        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1279        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1280          if sj_possible then
1281            〈2, 2〉
1282          else
1283            〈4, 4〉
1284      | JZ lbl ⇒
1285        let lookup_address ≝ sigma (lookup_labels lbl) in
1286        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1287        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1288          if sj_possible then
1289            〈2, 2〉
1290          else
1291            〈4, 4〉
1292      | JNZ lbl ⇒
1293        let lookup_address ≝ sigma (lookup_labels lbl) in
1294        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1295        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1296          if sj_possible then
1297            〈2, 2〉
1298          else
1299            〈4, 4〉
1300      | CJNE arg lbl ⇒
1301        let lookup_address ≝ sigma (lookup_labels lbl) in
1302        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1303        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1304          if sj_possible then
1305            〈2, 2〉
1306          else
1307            〈4, 4〉
1308      | DJNZ arg lbl ⇒
1309        let lookup_address ≝ sigma (lookup_labels lbl) in
1310        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1311        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1312          if sj_possible then
1313            〈2, 2〉
1314          else
1315            〈4, 4〉
1316      | ADD arg1 arg2 ⇒
1317        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1318         〈ticks, ticks〉
1319      | ADDC arg1 arg2 ⇒
1320        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1321         〈ticks, ticks〉
1322      | SUBB arg1 arg2 ⇒
1323        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1324         〈ticks, ticks〉
1325      | INC arg ⇒
1326        let ticks ≝ ticks_of_instruction (INC ? arg) in
1327         〈ticks, ticks〉
1328      | DEC arg ⇒
1329        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1330         〈ticks, ticks〉
1331      | MUL arg1 arg2 ⇒
1332        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1333         〈ticks, ticks〉
1334      | DIV arg1 arg2 ⇒
1335        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1336         〈ticks, ticks〉
1337      | DA arg ⇒
1338        let ticks ≝ ticks_of_instruction (DA ? arg) in
1339         〈ticks, ticks〉
1340      | ANL arg ⇒
1341        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1342         〈ticks, ticks〉
1343      | ORL arg ⇒
1344        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1345         〈ticks, ticks〉
1346      | XRL arg ⇒
1347        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1348         〈ticks, ticks〉
1349      | CLR arg ⇒
1350        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1351         〈ticks, ticks〉
1352      | CPL arg ⇒
1353        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1354         〈ticks, ticks〉
1355      | RL arg ⇒
1356        let ticks ≝ ticks_of_instruction (RL ? arg) in
1357         〈ticks, ticks〉
1358      | RLC arg ⇒
1359        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1360         〈ticks, ticks〉
1361      | RR arg ⇒
1362        let ticks ≝ ticks_of_instruction (RR ? arg) in
1363         〈ticks, ticks〉
1364      | RRC arg ⇒
1365        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1366         〈ticks, ticks〉
1367      | SWAP arg ⇒
1368        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1369         〈ticks, ticks〉
1370      | MOV arg ⇒
1371        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1372         〈ticks, ticks〉
1373      | MOVX arg ⇒
1374        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1375         〈ticks, ticks〉
1376      | SETB arg ⇒
1377        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1378         〈ticks, ticks〉
1379      | PUSH arg ⇒
1380        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1381         〈ticks, ticks〉
1382      | POP arg ⇒
1383        let ticks ≝ ticks_of_instruction (POP ? arg) in
1384         〈ticks, ticks〉
1385      | XCH arg1 arg2 ⇒
1386        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1387         〈ticks, ticks〉
1388      | XCHD arg1 arg2 ⇒
1389        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1390         〈ticks, ticks〉
1391      | RET ⇒
1392        let ticks ≝ ticks_of_instruction (RET ?) in
1393         〈ticks, ticks〉
1394      | RETI ⇒
1395        let ticks ≝ ticks_of_instruction (RETI ?) in
1396         〈ticks, ticks〉
1397      | NOP ⇒
1398        let ticks ≝ ticks_of_instruction (NOP ?) in
1399         〈ticks, ticks〉
1400      ]
1401    | Comment comment ⇒ 〈0, 0〉
1402    | Cost cost ⇒ 〈0, 0〉
1403    | Jmp jmp ⇒
1404      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1405      let do_a_long ≝ policy ppc in
1406      let lookup_address ≝ sigma (lookup_labels jmp) in
1407      let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1408        if sj_possible ∧ ¬ do_a_long then
1409          〈2, 2〉 (* XXX: SJMP *)
1410        else
1411        let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1412          if mj_possible ∧ ¬ do_a_long then
1413            〈2, 2〉 (* XXX: AJMP *)
1414          else
1415            〈2, 2〉 (* XXX: LJMP *)
1416    | Call call ⇒
1417      (* XXX: collapse the branches as they are identical? *)
1418      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1419      let lookup_address ≝ sigma (lookup_labels call) in
1420      let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1421      let do_a_long ≝ policy ppc in
1422      if mj_possible ∧ ¬ do_a_long then
1423        〈2, 2〉 (* ACALL *)
1424      else
1425        〈2, 2〉 (* LCALL *)
1426    | Mov dptr tgt ⇒ 〈2, 2〉
1427    ].
1428
1429definition ticks_of:
1430    ∀p:pseudo_assembly_program.
1431      (Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word.
1432       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
1433  λprogram: pseudo_assembly_program.
1434  λlookup_labels.
1435  λsigma.
1436  λpolicy.
1437  λppc: Word. λppc_ok.
1438    let pseudo ≝ \snd program in
1439    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
1440     ticks_of0 program lookup_labels sigma policy ppc fetched.
1441
1442(*
1443lemma blah:
1444  ∀m: internal_pseudo_address_map.
1445  ∀s: PseudoStatus.
1446  ∀arg: Byte.
1447  ∀b: bool.
1448    assert_data m s (DIRECT arg) = true →
1449      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1450      get_arg_8 ? s b (DIRECT arg).
1451  [2, 3: normalize % ]
1452  #m #s #arg #b #hyp
1453  whd in ⊢ (??%%)
1454  @vsplit_elim''
1455  #nu' #nl' #arg_nu_nl_eq
1456  normalize nodelta
1457  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1458  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1459  #get_index_v_eq
1460  normalize nodelta
1461  [2:
1462    normalize nodelta
1463    @vsplit_elim''
1464    #bit_one' #three_bits' #bit_one_three_bit_eq
1465    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1466    normalize nodelta
1467    generalize in match (refl ? (sub_7_with_carry ? ? ?))
1468    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1469    #Saddr #carr' #Saddr_carr_eq
1470    normalize nodelta
1471    #carr_hyp'
1472    @carr_hyp'
1473    [1:
1474    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1475        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1476        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1477        #member_eq
1478        normalize nodelta
1479        [2: #destr destruct(destr)
1480        |1: -carr_hyp';
1481            >arg_nu_nl_eq
1482            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1483            [1: >get_index_v_eq in ⊢ (??%? → ?)
1484            |2: @le_S @le_S @le_S @le_n
1485            ]
1486            cases (member (BitVector 8) ? (\fst ?) ?)
1487            [1: #destr normalize in destr; destruct(destr)
1488            |2:
1489            ]
1490        ]
1491    |3: >get_index_v_eq in ⊢ (??%?)
1492        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1493        >(vsplit_vector_singleton … bit_one_three_bit_eq)
1494        <arg_nu_nl_eq
1495        whd in hyp:(??%?)
1496        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1497        normalize nodelta [*: #ignore @sym_eq ]
1498    ]
1499  |
1500  ].
1501*)
1502(*
1503map_address0 ... (DIRECT arg) = Some .. →
1504  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1505  get_arg_8 (internal_ram ...) (DIRECT arg)
1506
1507((if assert_data M ps ACC_A∧assert_data M ps (DIRECT ARG2) 
1508                     then Some internal_pseudo_address_map M 
1509                     else None internal_pseudo_address_map )
1510                    =Some internal_pseudo_address_map M')
1511
1512axiom low_internal_ram_write_at_stack_pointer:
1513 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
1514 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1515  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1516  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
1517  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1518  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1519  bu@@bl = sigma (pbu@@pbl) →
1520   low_internal_ram T1 cm1
1521     (write_at_stack_pointer …
1522       (set_8051_sfr …
1523         (write_at_stack_pointer …
1524           (set_8051_sfr …
1525             (set_low_internal_ram … s1
1526               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
1527             SFR_SP sp1)
1528          bl)
1529        SFR_SP sp2)
1530      bu)
1531   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1532      (low_internal_ram …
1533       (write_at_stack_pointer …
1534         (set_8051_sfr …
1535           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1536          SFR_SP sp2)
1537        pbu)).
1538
1539lemma high_internal_ram_write_at_stack_pointer:
1540 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
1541 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1542  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1543  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
1544  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1545  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1546  bu@@bl = sigma (pbu@@pbl) →
1547   high_internal_ram T1 cm1
1548     (write_at_stack_pointer …
1549       (set_8051_sfr …
1550         (write_at_stack_pointer …
1551           (set_8051_sfr …
1552             (set_high_internal_ram … s1
1553               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
1554             SFR_SP sp1)
1555          bl)
1556        SFR_SP sp2)
1557      bu)
1558   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
1559      (high_internal_ram …
1560       (write_at_stack_pointer …
1561         (set_8051_sfr …
1562           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1563          SFR_SP sp2)
1564        pbu)).
1565  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
1566  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
1567  cases daemon (* XXX: !!! *)
1568qed.
1569*)
1570
1571lemma snd_assembly_1_pseudoinstruction_ok:
1572  ∀program: pseudo_assembly_program.
1573  ∀program_length_proof: |\snd program| ≤ 2^16.
1574  ∀sigma: Word → Word.
1575  ∀policy: Word → bool.
1576  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1577  ∀ppc: Word.
1578  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
1579  ∀pi.
1580  ∀lookup_labels.
1581  ∀lookup_datalabels.
1582    let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
1583    lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →
1584    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1585    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
1586    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
1587      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
1588  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
1589  #lookup_labels #lookup_datalabels
1590  @pair_elim #labels #costs #create_label_cost_map_refl
1591  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
1592  normalize nodelta
1593  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
1594  #fetch_pseudo_refl
1595  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
1596  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
1597  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
1598  @pair_elim #preamble #instr_list #program_refl
1599  lapply create_label_cost_map_refl; -create_label_cost_map_refl
1600  >program_refl in ⊢ (% → ?); #create_label_cost_map_refl
1601  >create_label_cost_map_refl
1602  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
1603  lapply (H ppc ppc_in_bounds) -H
1604  @pair_elim #pi' #newppc #fetch_pseudo_refl'
1605  @pair_elim #len #assembled #assembly1_refl #H
1606  cases H
1607  #encoding_check_assm #sigma_newppc_refl
1608  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
1609  >pi_refl' in assembly1_refl; #assembly1_refl
1610  >lookup_labels_refl >lookup_datalabels_refl
1611  >program_refl normalize nodelta
1612  >assembly1_refl
1613  <sigma_newppc_refl
1614  generalize in match fetch_pseudo_refl';
1615  whd in match (fetch_pseudo_instruction ???);
1616  @pair_elim #lbl #instr #nth_refl normalize nodelta
1617  #G cases (pair_destruct_right ?????? G) %
1618qed.
1619
1620(* To be moved in ProofStatus *)
1621lemma program_counter_set_program_counter:
1622  ∀T.
1623  ∀cm.
1624  ∀s.
1625  ∀x.
1626    program_counter T cm (set_program_counter T cm s x) = x.
1627  //
1628qed.
Note: See TracBrowser for help on using the repository browser.