source: src/ASM/AssemblyProof.ma @ 2279

Last change on this file since 2279 was 2279, checked in by sacerdot, 8 years ago
  1. Bug fixed in the semantics of PUSH (no indirection performed)
  2. Proved write_at_stack_pointer_status_of_pseudo_status
  3. PUSH case of main lemma almost done
File size: 62.1 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 lookup_from_internal_ram:
466    ∀addr: Byte.
467    ∀M: internal_pseudo_address_map.
468      option address_entry ≝
469  λaddr, M.
470    let 〈low, high, accA〉 ≝ M in
471    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
472      if head' … bit_one then
473        lookup_opt … seven_bits high
474      else
475        lookup_opt … seven_bits low.
476
477definition map_value_using_opt_address_entry:
478  (Word → Word) → Byte → option address_entry → Byte ≝
479  λsigma: Word → Word.
480  λvalue: Byte.
481  λul_addr: option address_entry.
482  match ul_addr with
483  [ None ⇒ value
484  | Some upper_lower_word ⇒
485    let 〈upper_lower, word〉 ≝ upper_lower_word in
486      if eq_upper_lower upper_lower upper then
487        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in
488          high
489      else
490        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in
491          low
492  ].
493
494definition map_acc_a_using_internal_pseudo_address_map:
495 ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝
496   λM, sigma, v. map_value_using_opt_address_entry sigma v (\snd M).
497
498definition map_internal_ram_address_using_pseudo_address_map:
499  ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
500  λM: internal_pseudo_address_map.
501  λsigma: Word → Word.
502  λaddress: Byte.
503  λvalue: Byte.
504   map_value_using_opt_address_entry sigma value
505    (lookup_from_internal_ram … address M ).
506
507definition map_opt_value_using_opt_address_entry:
508 (Word → Word) → option Byte → option address_entry → option Byte ≝
509 λsigma,v,ul_addr.
510  let v ≝ match v with [ None ⇒ zero … | Some v ⇒ v ] in
511  let v' ≝ map_value_using_opt_address_entry sigma v ul_addr in
512    if eq_bv … v' (zero …) then
513      None …
514    else
515      Some … v'.
516
517definition internal_ram_of_pseudo_internal_ram:
518    ∀sigma: Word → Word.
519    ∀ram: BitVectorTrie Byte 7.
520    ∀map: BitVectorTrie address_entry 7.
521      BitVectorTrie Byte 7 ≝
522  λsigma, ram, map.
523      bvt_map2 ??? ? ram map (map_opt_value_using_opt_address_entry sigma).
524
525definition internal_half_pseudo_address_map_equal_up_to_address:
526 BitVectorTrie address_entry 7 → BitVectorTrie address_entry 7 → (Word → Word) →
527  BitVector 7 → Byte → Byte → Prop
528 ≝
529 λM,M',sigma,addr,v,v'.
530  v' = map_value_using_opt_address_entry sigma v (lookup_opt … addr M') ∧
531   ∀addr'. addr' ≠ addr → lookup_opt … addr' M = lookup_opt … addr' M'. 
532
533axiom insert_internal_ram_of_pseudo_internal_ram:
534 ∀M,M',sigma,addr,v,v',ram.
535  internal_half_pseudo_address_map_equal_up_to_address M M' sigma addr v v' →
536  insert Byte … addr v' (internal_ram_of_pseudo_internal_ram sigma ram M)
537  = internal_ram_of_pseudo_internal_ram sigma (insert ?? addr v ram) M'.
538
539definition low_internal_ram_of_pseudo_low_internal_ram:
540    ∀M: internal_pseudo_address_map.
541    ∀sigma: Word → Word.
542    ∀ram: BitVectorTrie Byte 7.
543      BitVectorTrie Byte 7 ≝
544  λM, sigma, ram.
545    let 〈low, high, accA〉 ≝ M in
546      internal_ram_of_pseudo_internal_ram sigma ram low.
547
548definition high_internal_ram_of_pseudo_high_internal_ram:
549    ∀M: internal_pseudo_address_map.
550    ∀sigma: Word → Word.
551    ∀ram: BitVectorTrie Byte 7.
552      BitVectorTrie Byte 7 ≝
553  λM, sigma, ram.
554    let 〈low, high, accA〉 ≝ M in
555      internal_ram_of_pseudo_internal_ram sigma ram high.
556
557(*
558axiom low_internal_ram_of_pseudo_internal_ram_hit:
559 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.
560  lookup_opt ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉  →
561   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in
562   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
563   let bl ≝ lookup ? 7 addr ram (zero 8) in
564   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
565   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (sigma points_to) in
566     if eq_upper_lower upper_lower upper then
567       (pbl = higher) ∧ (bl = phigher)
568     else
569       (pbl = lower) ∧ (bl = plower).
570*)
571
572(* changed from add to sub *)
573axiom low_internal_ram_of_pseudo_internal_ram_miss:
574 ∀T.∀M:internal_pseudo_address_map.∀sigma. ∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
575  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in
576    lookup_opt … addr (\fst (\fst M)) = None … →
577      lookup … addr ram (zero …) = lookup … addr (low_internal_ram … s) (zero ?).
578
579definition exists:
580    ∀A: Type[0].
581    ∀n: nat.
582    ∀v: BitVector n.
583    ∀bvt: BitVectorTrie A n.
584      bool ≝
585  λA, n, v, bvt.
586    match lookup_opt … v bvt with
587    [ None ⇒ false
588    | _    ⇒ true
589    ].
590
591definition data_or_address ≝
592  λT.
593  λM: internal_pseudo_address_map.
594  λcm.
595  λs: PreStatus T cm.
596  λaddr: addressing_mode.
597  let 〈low, high, accA〉 ≝ M in
598  match addr return λx. option (option address_entry) with
599    [ DIRECT d ⇒
600       let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
601         match head' … hd with
602         [ true ⇒
603             if eq_bv … d (bitvector_of_nat … 224) then
604               Some … accA
605             else
606               Some … (None …)
607         | false ⇒ Some … (lookup_opt … seven_bits low)
608         ]
609    | INDIRECT i ⇒
610        let d ≝ get_register … s [[false;false;i]] in
611        let address ≝ bit_address_of_register … s [[false;false;i]] in
612          if ¬exists … address low then
613            let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
614              if head' … 0 bit_one then
615                Some … (lookup_opt … seven_bits high)
616              else
617                Some … (lookup_opt … seven_bits low)
618          else
619            None ?
620    | EXT_INDIRECT e ⇒
621        let address ≝ bit_address_of_register … s [[false;false;e]] in
622          if ¬exists … address low then
623            Some … (None …)
624          else
625            None ?
626    | REGISTER r ⇒
627        let address ≝ bit_address_of_register … s r in
628          Some … (lookup_opt … address low)
629    | ACC_A ⇒ Some … accA
630    | ACC_B ⇒ Some … (None …)
631    | DPTR ⇒ Some … (None …)
632    | DATA _ ⇒ Some … (None …)
633    | DATA16 _ ⇒ Some … (None …)
634    | ACC_DPTR ⇒ Some … (None …)
635    | ACC_PC ⇒ Some … (None …)
636    | EXT_INDIRECT_DPTR ⇒ Some … (None …)
637    | INDIRECT_DPTR ⇒ Some … (None …)
638    | CARRY ⇒ Some … (None …)
639    | BIT_ADDR b ⇒
640      let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
641      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
642        if head' bool 0 bit_one then
643            if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *)
644              Some … accA
645            else
646              Some … (None …)
647        else
648          let address' ≝ [[true; false; false]]@@four_bits in
649            Some … (lookup_opt … address' low)
650    | N_BIT_ADDR b ⇒
651      let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
652      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
653        if head' bool 0 bit_one then
654            if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *)
655              Some … accA
656            else
657              Some … (None …)
658        else
659          let address' ≝ [[true; false; false]]@@four_bits in
660            Some … (lookup_opt … address' low)
661    | RELATIVE _ ⇒ Some … (None …)
662    | ADDR11 _ ⇒ Some … (None …)
663    | ADDR16 _ ⇒ Some … (None …)
664    ].
665
666definition assert_data ≝
667  λT.
668  λM: internal_pseudo_address_map.
669  λcm.
670  λs: PreStatus T cm.
671  λaddr: addressing_mode.
672    match data_or_address T M cm s addr with
673    [ None   ⇒ false
674    | Some s ⇒
675      match s with
676      [ None ⇒ true
677      | _    ⇒ false
678      ]
679    ].
680   
681definition insert_into_internal_ram:
682  ∀addr: Byte.
683  ∀v: address_entry.
684  ∀M: internal_pseudo_address_map.
685    internal_pseudo_address_map ≝
686  λaddr, v, M.
687    let 〈low, high, accA〉 ≝ M in
688    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
689      if head' … bit_one then
690        〈low, insert … seven_bits v high, accA〉
691      else
692        〈insert … seven_bits v low, high, accA〉.
693   
694axiom delete:
695  ∀A: Type[0].
696  ∀n: nat.
697  ∀b: BitVector n.
698    BitVectorTrie A n → BitVectorTrie A n.
699
700definition delete_from_internal_ram:
701    ∀addr: Byte.
702    ∀M: internal_pseudo_address_map.
703      internal_pseudo_address_map ≝
704  λaddr, M.
705    let 〈low, high, accA〉 ≝ M in
706    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
707      if head' … bit_one then
708        〈low,delete … seven_bits high, accA〉
709      else
710        〈delete … seven_bits low, high, accA〉.
711
712definition overwrite_or_delete_from_internal_ram:
713    ∀addr: Byte.
714    ∀v: option address_entry.
715    ∀M: internal_pseudo_address_map.
716      internal_pseudo_address_map ≝
717  λaddr, v, M.
718    match v with
719    [ None ⇒ delete_from_internal_ram addr M
720    | Some v' ⇒ insert_into_internal_ram addr v' M
721    ].
722   
723definition next_internal_pseudo_address_map0 ≝
724  λT.
725  λcm:T.
726  λaddr_of: Identifier → PreStatus T cm → Word.
727  λfetched.
728  λM: internal_pseudo_address_map.
729  λs: PreStatus T cm.
730  let 〈low, high, accA〉 ≝ M in
731   match fetched with
732    [ Comment _ ⇒ Some ? M
733    | Cost _ ⇒ Some … M
734    | Jmp _ ⇒ Some … M
735    | Call a ⇒
736      let a' ≝ addr_of a s in
737      let 〈upA, lowA〉 ≝ vsplit bool 8 8 a' in
738        Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) 〈lower, upA〉
739                (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) 〈upper, lowA〉 M))
740    | Mov _ _ ⇒ Some … M
741    | Instruction instr ⇒
742      match instr return λx. option internal_pseudo_address_map with
743       [ ADD addr1 addr2 ⇒
744         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
745           Some ? M
746         else
747           None ?
748       | ADDC addr1 addr2 ⇒
749         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
750           Some ? M
751         else
752           None ?
753       | SUBB addr1 addr2 ⇒
754         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
755           Some ? M
756         else
757           None ?
758       | INC addr1 ⇒
759         if assert_data T M ? s addr1 then
760           Some ? M
761         else
762           None ?
763       | DEC addr1 ⇒
764         if assert_data T M … s addr1 then
765           Some ? M
766         else
767           None ?
768       | MUL addr1 addr2 ⇒
769         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
770           Some ? M
771         else
772           None ?
773       | DIV addr1 addr2 ⇒
774         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
775           Some ? M
776         else
777           None ?
778       | DA addr1 ⇒
779         if assert_data T M … s addr1 then
780           Some ? M
781         else
782           None ?
783       | JC addr1 ⇒ Some ? M
784       | JNC addr1 ⇒ Some ? M
785       | JB addr1 addr2 ⇒ Some ? M
786       | JNB addr1 addr2 ⇒ Some ? M
787       | JBC addr1 addr2 ⇒ Some ? M
788       | JZ addr1 ⇒ Some ? M
789       | JNZ addr1 ⇒ Some ? M
790       | CJNE addr1 addr2 ⇒
791         match addr1 with
792         [ inl l ⇒
793           let 〈left, right〉 ≝ l in
794             if assert_data T M … s left ∧ assert_data T M … s right then
795               Some ? M
796             else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then
797               Some ? M
798             else
799               None ?
800         | inr r ⇒
801           let 〈left, right〉 ≝ r in
802             if assert_data T M … s left ∧ assert_data T M … s right then
803               Some ? M
804             else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then
805               Some ? M
806             else
807               None ?
808         ]
809       | DJNZ addr1 addr2 ⇒
810         if assert_data T M … s addr1 then
811           Some ? M
812         else
813           None ?
814       | CLR addr1 ⇒
815         if assert_data T M … s addr1 then
816           Some ? M
817         else
818           None ?
819       | CPL addr1 ⇒
820         if assert_data T M … s addr1 then
821           Some ? M
822         else
823           None ?
824       | RL addr1 ⇒
825         if assert_data T M … s addr1 then
826           Some ? M
827         else
828           None ?
829       | RLC addr1 ⇒
830         if assert_data T M … s addr1 then
831           Some ? M
832         else
833           None ?
834       | RR addr1 ⇒
835         if assert_data T M … s addr1 then
836           Some ? M
837         else
838           None ?
839       | RRC addr1 ⇒
840         if assert_data T M … s addr1 then
841           Some ? M
842         else
843           None ?
844       | SWAP addr1 ⇒
845         if assert_data T M … s addr1 then
846           Some ? M
847         else
848           None ?
849       | SETB addr1 ⇒
850         if assert_data T M … s addr1 then
851           Some ? M
852         else
853           None ?
854       (* XXX: need to track addresses pushed and popped off the stack? *)
855       | PUSH addr1 ⇒
856         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
857         [ DIRECT d ⇒ λproof.
858           let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
859             if head' … bit_one then
860               if eq_bv … seven_bits (bitvector_of_nat … 224) then
861                 Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) accA M)
862               else
863                 Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M)
864             else
865               match lookup_from_internal_ram … d M with
866               [ None ⇒
867                   Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M)
868               | Some ul_addr ⇒
869                   Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) ul_addr M)
870               ]
871         | _ ⇒ λother: False. ⊥
872         ] (subaddressing_modein … addr1)
873       | POP addr1 ⇒
874         let sp ≝ get_8051_sfr ?? s SFR_SP in
875         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
876         [ DIRECT d ⇒ λproof.
877           let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
878             if head' … bit_one then
879               if eq_bv … d (bitvector_of_nat … 224) then
880                 Some … 〈low, high, lookup_from_internal_ram … sp M〉
881               else
882                 match lookup_from_internal_ram sp M with
883                 [ None ⇒ Some ? M
884                 | _    ⇒ None ?
885                 ]
886             else
887               Some … (overwrite_or_delete_from_internal_ram d (lookup_from_internal_ram … sp M) M)
888         | _ ⇒ λother: False. ⊥
889         ] (subaddressing_modein … addr1)
890       | XCH addr1 addr2 ⇒
891         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
892           Some ? M
893         else
894           None ?
895       | XCHD addr1 addr2 ⇒
896         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
897           Some ? M
898         else
899           None ?
900      | RET ⇒
901        let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
902        let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
903        match lookup_from_internal_ram sp_minus_1 M with
904        [ None ⇒ None …
905        | Some low_addr_high ⇒
906            match lookup_from_internal_ram sp_minus_2 M with
907            [ None ⇒ None …
908            | Some high_addr_low ⇒
909              let 〈low, addr_high〉 ≝ low_addr_high in
910              let 〈high, addr_low〉 ≝ high_addr_low in
911              let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
912              let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
913                if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
914                  Some ? M
915                else
916                  None ?
917            ]
918        ]
919      | RETI ⇒
920        let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
921        let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
922        match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M with
923        [ None ⇒ None …
924        | Some low_addr_high ⇒
925            match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) M with
926            [ None ⇒ None …
927            | Some high_addr_low ⇒
928              let 〈low, addr_high〉 ≝ low_addr_high in
929              let 〈high, addr_low〉 ≝ high_addr_low in
930              let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
931              let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
932                if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
933                  Some ? M
934                else
935                  None ?
936            ]
937        ]
938      | NOP ⇒ Some … M
939      | MOVX addr1 ⇒
940        match addr1 with
941        [ inl l ⇒
942            Some ? 〈low, high, None …〉
943        | inr r ⇒
944          let 〈others, acc_a〉 ≝ r in
945            if assert_data T M … s acc_a then
946              Some ? M
947            else
948              None ?
949        ]
950      | XRL addr1 ⇒
951        match addr1 with
952        [ inl l ⇒
953          let 〈acc_a, others〉 ≝ l in
954          let acc_a_ok ≝ assert_data T M … s acc_a in
955          let others_ok ≝ assert_data T M … s others in
956          if acc_a_ok ∧ others_ok then
957            Some ? M
958          else
959            None ?
960        | inr r ⇒
961          let 〈direct, others〉 ≝ r in
962          let direct_ok ≝ assert_data T M … s direct in
963          let others_ok ≝ assert_data T M … s others in
964          if direct_ok ∧ others_ok then
965            Some ? M
966          else
967            None ?
968        ]
969      | ORL addr1 ⇒
970        match addr1 with
971        [ inl l ⇒
972          match l with
973          [ inl l ⇒
974            let 〈acc_a, others〉 ≝ l in
975            let acc_a_ok ≝ assert_data T M … s acc_a in
976            let others_ok ≝ assert_data T M … s others in
977            if acc_a_ok ∧ others_ok then
978              Some ? M
979            else
980              None ?
981          | inr r ⇒
982            let 〈direct, others〉 ≝ r in
983            let direct_ok ≝ assert_data T M … s direct in
984            let others_ok ≝ assert_data T M … s others in
985            if direct_ok ∧ others_ok then
986              Some ? M
987            else
988              None ?
989          ]
990        | inr r ⇒
991          let 〈carry, others〉 ≝ r in
992          let carry_ok ≝ assert_data T M … s carry in
993          let others_ok ≝ assert_data T M … s others in
994          if carry_ok ∧ others_ok then
995            Some ? M
996          else
997            None ?
998        ]
999      | ANL addr1 ⇒
1000        match addr1 with
1001        [ inl l ⇒
1002          match l with
1003          [ inl l ⇒
1004            let 〈acc_a, others〉 ≝ l in
1005            let acc_a_ok ≝ assert_data T M … s acc_a in
1006            let others_ok ≝ assert_data T M … s others in
1007            if acc_a_ok ∧ others_ok then
1008              Some ? M
1009            else
1010              None ?
1011          | inr r ⇒
1012            let 〈direct, others〉 ≝ r in
1013            let direct_ok ≝ assert_data T M … s direct in
1014            let others_ok ≝ assert_data T M … s others in
1015            if direct_ok ∧ others_ok then
1016              Some ? M
1017            else
1018              None ?
1019          ]
1020        | inr r ⇒
1021          let 〈carry, others〉 ≝ r in
1022          let carry_ok ≝ assert_data T M … s carry in
1023          let others_ok ≝ assert_data T M … s others in
1024          if carry_ok ∧ others_ok then
1025            Some ? M
1026          else
1027            None ?
1028        ]
1029      | MOV addr1 ⇒
1030        (* XXX: wrong *)
1031        match addr1 with
1032        [ inl l ⇒
1033          match l with
1034          [ inl l' ⇒
1035            match l' with
1036            [ inl l'' ⇒
1037              match l'' with
1038              [ inl l''' ⇒
1039                match l''' with
1040                [ inl l'''' ⇒
1041                  let 〈acc_a, others〉 ≝ l'''' in
1042                    match data_or_address T M … s others with
1043                    [ None ⇒ None ?
1044                    | Some s ⇒
1045                        Some … 〈low, high, s〉
1046                    ]
1047                | inr r ⇒
1048                  let 〈others, others'〉 ≝ r in
1049                  let address ≝
1050                    match others return λx. bool_to_Prop (is_in … [[ registr; indirect ]] x) → ? with
1051                    [ REGISTER r ⇒ λproof. false:::bit_address_of_register … s r
1052                    | INDIRECT i ⇒ λproof. get_register … s [[false; false; i]]
1053                    | _ ⇒ λother: False. ⊥
1054                    ] (subaddressing_modein … others)
1055                  in
1056                    match data_or_address T M … s others' with
1057                    [ None ⇒ None ?
1058                    | Some s ⇒
1059                        Some … (overwrite_or_delete_from_internal_ram address s M)
1060                    ]
1061                ]
1062              | inr r ⇒
1063                let 〈direct', others〉 ≝ r in
1064                  match direct' return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
1065                  [ DIRECT d ⇒ λproof.
1066                    match data_or_address T M … s others with
1067                    [ None ⇒ None ?
1068                    | Some s' ⇒
1069                        let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
1070                          if head' … bit_one then
1071                            if eq_bv … d (bitvector_of_nat … 224) then
1072                              Some … 〈low, high, s'〉
1073                            else
1074                              match s' with
1075                              [ None ⇒ Some ? M
1076                              | Some s'' ⇒ None ?
1077                              ]
1078                          else
1079                            Some … (overwrite_or_delete_from_internal_ram d s' M)
1080                    ]
1081                  | _ ⇒ λother: False. ⊥
1082                  ] (subaddressing_modein … direct')
1083              ]
1084            | inr r ⇒ Some … M
1085            ]
1086          | inr r ⇒
1087            let 〈carry, bit_addr〉 ≝ r in
1088            if assert_data T M … s bit_addr then
1089              Some ? M
1090            else
1091              None ?
1092          ]
1093        | inr r ⇒
1094          let 〈bit_addr, carry〉 ≝ r in
1095          if assert_data T M … s bit_addr then
1096            Some ? M
1097          else
1098            None ?
1099        ]
1100      ]
1101    ].
1102    cases other
1103qed.
1104
1105definition next_internal_pseudo_address_map ≝
1106 λM:internal_pseudo_address_map.
1107 λcm.
1108 λaddr_of.
1109 λs:PseudoStatus cm.
1110 λppc_ok.
1111    next_internal_pseudo_address_map0 ? cm addr_of
1112     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
1113
1114definition code_memory_of_pseudo_assembly_program:
1115    ∀pap:pseudo_assembly_program.
1116      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
1117  λpap.
1118  λsigma.
1119  λpolicy.
1120    let p ≝ pi1 … (assembly pap sigma policy) in
1121      load_code_memory (\fst p).
1122
1123definition sfr_8051_of_pseudo_sfr_8051 ≝
1124  λM: internal_pseudo_address_map.
1125  λsfrs: Vector Byte 19.
1126  λsigma: Word → Word.
1127    match \snd M with
1128    [ None ⇒ sfrs
1129    | Some upper_lower_address ⇒
1130      let index ≝ sfr_8051_index SFR_ACC_A in
1131      let acc_a ≝ get_index_v … sfrs index ? in
1132      let 〈upper_lower, address〉 ≝ upper_lower_address in
1133        if eq_upper_lower upper_lower upper then
1134          let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (acc_a@@address)) in
1135            set_index Byte 19 sfrs index high ?
1136        else
1137          let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (address@@acc_a)) in
1138            set_index Byte 19 sfrs index low ?
1139    ].
1140  //
1141qed.
1142
1143definition status_of_pseudo_status:
1144    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
1145      ∀sigma: Word → Word. ∀policy: Word → bool.
1146        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
1147  λM.
1148  λpap.
1149  λps.
1150  λsigma.
1151  λpolicy.
1152  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
1153  let pc ≝ sigma (program_counter … ps) in
1154  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … ps) in
1155  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M sigma (high_internal_ram … ps) in
1156     mk_PreStatus (BitVectorTrie Byte 16)
1157      cm
1158      lir
1159      hir
1160      (external_ram … ps)
1161      pc
1162      (sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma)
1163      (special_function_registers_8052 … ps)
1164      (p1_latch … ps)
1165      (p3_latch … ps)
1166      (clock … ps).
1167
1168(*
1169definition write_at_stack_pointer':
1170 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1171  λM: Type[0].
1172  λs: PreStatus M.
1173  λv: Byte.
1174    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
1175    let bit_zero ≝ get_index_v… nu O ? in
1176    let bit_1 ≝ get_index_v… nu 1 ? in
1177    let bit_2 ≝ get_index_v… nu 2 ? in
1178    let bit_3 ≝ get_index_v… nu 3 ? in
1179      if bit_zero then
1180        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1181                              v (low_internal_ram ? s) in
1182          set_low_internal_ram ? s memory
1183      else
1184        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1185                              v (high_internal_ram ? s) in
1186          set_high_internal_ram ? s memory.
1187  [ cases l0 %
1188  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1189qed.
1190
1191definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1192 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1193
1194  λticks_of.
1195  λs.
1196  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1197  let ticks ≝ ticks_of (program_counter ? s) in
1198  let s ≝ set_clock ? s (clock ? s + ticks) in
1199  let s ≝ set_program_counter ? s pc in
1200    match instr with
1201    [ Instruction instr ⇒
1202       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1203    | Comment cmt ⇒ s
1204    | Cost cst ⇒ s
1205    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1206    | Call call ⇒
1207      let a ≝ address_of_word_labels s call in
1208      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1209      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1210      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
1211      let s ≝ write_at_stack_pointer' ? s pc_bl in
1212      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1213      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1214      let s ≝ write_at_stack_pointer' ? s pc_bu in
1215        set_program_counter ? s a
1216    | Mov dptr ident ⇒
1217       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1218    ].
1219 [
1220 |2,3,4: %
1221 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1222 |
1223 | %
1224 ]
1225 cases not_implemented
1226qed.
1227*)
1228
1229(*
1230lemma execute_code_memory_unchanged:
1231 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1232 #ticks #ps whd in ⊢ (??? (??%))
1233 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1234  (program_counter pseudo_assembly_program ps)) #instr #pc
1235 whd in ⊢ (??? (??%)) cases instr
1236  [ #pre cases pre
1237     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1238       cases (vsplit ????) #z1 #z2 %
1239     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1240       cases (vsplit ????) #z1 #z2 %
1241     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1242       cases (vsplit ????) #z1 #z2 %
1243     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1244       [ #x1 whd in ⊢ (??? (??%))
1245     | *: cases not_implemented
1246     ]
1247  | #comment %
1248  | #cost %
1249  | #label %
1250  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1251    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1252    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
1253    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1254    (* CSC: ??? *)
1255  | #dptr #label (* CSC: ??? *)
1256  ]
1257  cases not_implemented
1258qed.
1259*)
1260
1261(* XXX: check values returned for conditional jumps below! They are wrong,
1262        find correct values *)
1263definition ticks_of0:
1264    ∀p:pseudo_assembly_program.
1265      (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
1266  λprogram: pseudo_assembly_program.
1267  λlookup_labels: Identifier → Word.
1268  λsigma.
1269  λpolicy.
1270  λppc: Word.
1271  λfetched.
1272    match fetched with
1273    [ Instruction instr ⇒
1274      match instr with
1275      [ JC lbl ⇒
1276        let lookup_address ≝ sigma (lookup_labels lbl) in
1277        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1278        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1279          if sj_possible then
1280            〈2, 2〉
1281          else
1282            〈4, 4〉
1283      | JNC lbl ⇒
1284        let lookup_address ≝ sigma (lookup_labels lbl) in
1285        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1286        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1287          if sj_possible then
1288            〈2, 2〉
1289          else
1290            〈4, 4〉
1291      | JB bit lbl ⇒
1292        let lookup_address ≝ sigma (lookup_labels lbl) in
1293        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1294        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1295          if sj_possible then
1296            〈2, 2〉
1297          else
1298            〈4, 4〉
1299      | JNB bit lbl ⇒
1300        let lookup_address ≝ sigma (lookup_labels lbl) in
1301        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1302        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1303          if sj_possible then
1304            〈2, 2〉
1305          else
1306            〈4, 4〉
1307      | JBC bit lbl ⇒
1308        let lookup_address ≝ sigma (lookup_labels lbl) in
1309        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1310        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1311          if sj_possible then
1312            〈2, 2〉
1313          else
1314            〈4, 4〉
1315      | JZ lbl ⇒
1316        let lookup_address ≝ sigma (lookup_labels lbl) in
1317        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1318        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1319          if sj_possible then
1320            〈2, 2〉
1321          else
1322            〈4, 4〉
1323      | JNZ lbl ⇒
1324        let lookup_address ≝ sigma (lookup_labels lbl) in
1325        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1326        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1327          if sj_possible then
1328            〈2, 2〉
1329          else
1330            〈4, 4〉
1331      | CJNE arg lbl ⇒
1332        let lookup_address ≝ sigma (lookup_labels lbl) in
1333        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1334        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1335          if sj_possible then
1336            〈2, 2〉
1337          else
1338            〈4, 4〉
1339      | DJNZ arg lbl ⇒
1340        let lookup_address ≝ sigma (lookup_labels lbl) in
1341        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1342        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1343          if sj_possible then
1344            〈2, 2〉
1345          else
1346            〈4, 4〉
1347      | ADD arg1 arg2 ⇒
1348        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1349         〈ticks, ticks〉
1350      | ADDC arg1 arg2 ⇒
1351        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1352         〈ticks, ticks〉
1353      | SUBB arg1 arg2 ⇒
1354        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1355         〈ticks, ticks〉
1356      | INC arg ⇒
1357        let ticks ≝ ticks_of_instruction (INC ? arg) in
1358         〈ticks, ticks〉
1359      | DEC arg ⇒
1360        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1361         〈ticks, ticks〉
1362      | MUL arg1 arg2 ⇒
1363        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1364         〈ticks, ticks〉
1365      | DIV arg1 arg2 ⇒
1366        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1367         〈ticks, ticks〉
1368      | DA arg ⇒
1369        let ticks ≝ ticks_of_instruction (DA ? arg) in
1370         〈ticks, ticks〉
1371      | ANL arg ⇒
1372        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1373         〈ticks, ticks〉
1374      | ORL arg ⇒
1375        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1376         〈ticks, ticks〉
1377      | XRL arg ⇒
1378        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1379         〈ticks, ticks〉
1380      | CLR arg ⇒
1381        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1382         〈ticks, ticks〉
1383      | CPL arg ⇒
1384        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1385         〈ticks, ticks〉
1386      | RL arg ⇒
1387        let ticks ≝ ticks_of_instruction (RL ? arg) in
1388         〈ticks, ticks〉
1389      | RLC arg ⇒
1390        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1391         〈ticks, ticks〉
1392      | RR arg ⇒
1393        let ticks ≝ ticks_of_instruction (RR ? arg) in
1394         〈ticks, ticks〉
1395      | RRC arg ⇒
1396        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1397         〈ticks, ticks〉
1398      | SWAP arg ⇒
1399        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1400         〈ticks, ticks〉
1401      | MOV arg ⇒
1402        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1403         〈ticks, ticks〉
1404      | MOVX arg ⇒
1405        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1406         〈ticks, ticks〉
1407      | SETB arg ⇒
1408        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1409         〈ticks, ticks〉
1410      | PUSH arg ⇒
1411        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1412         〈ticks, ticks〉
1413      | POP arg ⇒
1414        let ticks ≝ ticks_of_instruction (POP ? arg) in
1415         〈ticks, ticks〉
1416      | XCH arg1 arg2 ⇒
1417        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1418         〈ticks, ticks〉
1419      | XCHD arg1 arg2 ⇒
1420        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1421         〈ticks, ticks〉
1422      | RET ⇒
1423        let ticks ≝ ticks_of_instruction (RET ?) in
1424         〈ticks, ticks〉
1425      | RETI ⇒
1426        let ticks ≝ ticks_of_instruction (RETI ?) in
1427         〈ticks, ticks〉
1428      | NOP ⇒
1429        let ticks ≝ ticks_of_instruction (NOP ?) in
1430         〈ticks, ticks〉
1431      ]
1432    | Comment comment ⇒ 〈0, 0〉
1433    | Cost cost ⇒ 〈0, 0〉
1434    | Jmp jmp ⇒
1435      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1436      let do_a_long ≝ policy ppc in
1437      let lookup_address ≝ sigma (lookup_labels jmp) in
1438      let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1439        if sj_possible ∧ ¬ do_a_long then
1440          〈2, 2〉 (* XXX: SJMP *)
1441        else
1442        let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1443          if mj_possible ∧ ¬ do_a_long then
1444            〈2, 2〉 (* XXX: AJMP *)
1445          else
1446            〈2, 2〉 (* XXX: LJMP *)
1447    | Call call ⇒
1448      (* XXX: collapse the branches as they are identical? *)
1449      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1450      let lookup_address ≝ sigma (lookup_labels call) in
1451      let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1452      let do_a_long ≝ policy ppc in
1453      if mj_possible ∧ ¬ do_a_long then
1454        〈2, 2〉 (* ACALL *)
1455      else
1456        〈2, 2〉 (* LCALL *)
1457    | Mov dptr tgt ⇒ 〈2, 2〉
1458    ].
1459
1460definition ticks_of:
1461    ∀p:pseudo_assembly_program.
1462      (Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word.
1463       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
1464  λprogram: pseudo_assembly_program.
1465  λlookup_labels.
1466  λsigma.
1467  λpolicy.
1468  λppc: Word. λppc_ok.
1469    let pseudo ≝ \snd program in
1470    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
1471     ticks_of0 program lookup_labels sigma policy ppc fetched.
1472
1473(*
1474lemma blah:
1475  ∀m: internal_pseudo_address_map.
1476  ∀s: PseudoStatus.
1477  ∀arg: Byte.
1478  ∀b: bool.
1479    assert_data m s (DIRECT arg) = true →
1480      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1481      get_arg_8 ? s b (DIRECT arg).
1482  [2, 3: normalize % ]
1483  #m #s #arg #b #hyp
1484  whd in ⊢ (??%%)
1485  @vsplit_elim''
1486  #nu' #nl' #arg_nu_nl_eq
1487  normalize nodelta
1488  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1489  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1490  #get_index_v_eq
1491  normalize nodelta
1492  [2:
1493    normalize nodelta
1494    @vsplit_elim''
1495    #bit_one' #three_bits' #bit_one_three_bit_eq
1496    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1497    normalize nodelta
1498    generalize in match (refl ? (sub_7_with_carry ? ? ?))
1499    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1500    #Saddr #carr' #Saddr_carr_eq
1501    normalize nodelta
1502    #carr_hyp'
1503    @carr_hyp'
1504    [1:
1505    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1506        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1507        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1508        #member_eq
1509        normalize nodelta
1510        [2: #destr destruct(destr)
1511        |1: -carr_hyp';
1512            >arg_nu_nl_eq
1513            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1514            [1: >get_index_v_eq in ⊢ (??%? → ?)
1515            |2: @le_S @le_S @le_S @le_n
1516            ]
1517            cases (member (BitVector 8) ? (\fst ?) ?)
1518            [1: #destr normalize in destr; destruct(destr)
1519            |2:
1520            ]
1521        ]
1522    |3: >get_index_v_eq in ⊢ (??%?)
1523        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1524        >(vsplit_vector_singleton … bit_one_three_bit_eq)
1525        <arg_nu_nl_eq
1526        whd in hyp:(??%?)
1527        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1528        normalize nodelta [*: #ignore @sym_eq ]
1529    ]
1530  |
1531  ].
1532*)
1533(*
1534map_address0 ... (DIRECT arg) = Some .. →
1535  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1536  get_arg_8 (internal_ram ...) (DIRECT arg)
1537
1538((if assert_data M ps ACC_A∧assert_data M ps (DIRECT ARG2) 
1539                     then Some internal_pseudo_address_map M 
1540                     else None internal_pseudo_address_map )
1541                    =Some internal_pseudo_address_map M')
1542
1543axiom low_internal_ram_write_at_stack_pointer:
1544 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
1545 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1546  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1547  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
1548  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1549  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1550  bu@@bl = sigma (pbu@@pbl) →
1551   low_internal_ram T1 cm1
1552     (write_at_stack_pointer …
1553       (set_8051_sfr …
1554         (write_at_stack_pointer …
1555           (set_8051_sfr …
1556             (set_low_internal_ram … s1
1557               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
1558             SFR_SP sp1)
1559          bl)
1560        SFR_SP sp2)
1561      bu)
1562   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1563      (low_internal_ram …
1564       (write_at_stack_pointer …
1565         (set_8051_sfr …
1566           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1567          SFR_SP sp2)
1568        pbu)).
1569
1570lemma high_internal_ram_write_at_stack_pointer:
1571 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
1572 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1573  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1574  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
1575  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1576  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1577  bu@@bl = sigma (pbu@@pbl) →
1578   high_internal_ram T1 cm1
1579     (write_at_stack_pointer …
1580       (set_8051_sfr …
1581         (write_at_stack_pointer …
1582           (set_8051_sfr …
1583             (set_high_internal_ram … s1
1584               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
1585             SFR_SP sp1)
1586          bl)
1587        SFR_SP sp2)
1588      bu)
1589   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
1590      (high_internal_ram …
1591       (write_at_stack_pointer …
1592         (set_8051_sfr …
1593           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1594          SFR_SP sp2)
1595        pbu)).
1596  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
1597  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
1598  cases daemon (* XXX: !!! *)
1599qed.
1600*)
1601
1602lemma snd_assembly_1_pseudoinstruction_ok:
1603  ∀program: pseudo_assembly_program.
1604  ∀program_length_proof: |\snd program| ≤ 2^16.
1605  ∀sigma: Word → Word.
1606  ∀policy: Word → bool.
1607  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1608  ∀ppc: Word.
1609  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
1610  ∀pi.
1611  ∀lookup_labels.
1612  ∀lookup_datalabels.
1613    let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
1614    lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →
1615    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1616    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
1617    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
1618      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
1619  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
1620  #lookup_labels #lookup_datalabels
1621  @pair_elim #labels #costs #create_label_cost_map_refl
1622  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
1623  normalize nodelta
1624  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
1625  #fetch_pseudo_refl
1626  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
1627  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
1628  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
1629  @pair_elim #preamble #instr_list #program_refl
1630  lapply create_label_cost_map_refl; -create_label_cost_map_refl
1631  >program_refl in ⊢ (% → ?); #create_label_cost_map_refl
1632  >create_label_cost_map_refl
1633  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
1634  lapply (H ppc ppc_in_bounds) -H
1635  @pair_elim #pi' #newppc #fetch_pseudo_refl'
1636  @pair_elim #len #assembled #assembly1_refl #H
1637  cases H
1638  #encoding_check_assm #sigma_newppc_refl
1639  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
1640  >pi_refl' in assembly1_refl; #assembly1_refl
1641  >lookup_labels_refl >lookup_datalabels_refl
1642  >program_refl normalize nodelta
1643  >assembly1_refl
1644  <sigma_newppc_refl
1645  generalize in match fetch_pseudo_refl';
1646  whd in match (fetch_pseudo_instruction ???);
1647  @pair_elim #lbl #instr #nth_refl normalize nodelta
1648  #G cases (pair_destruct_right ?????? G) %
1649qed.
1650
1651(* To be moved in ProofStatus *)
1652lemma program_counter_set_program_counter:
1653  ∀T.
1654  ∀cm.
1655  ∀s.
1656  ∀x.
1657    program_counter T cm (set_program_counter T cm s x) = x.
1658  //
1659qed.
Note: See TracBrowser for help on using the repository browser.