source: src/ASM/AssemblyProof.ma @ 2282

Last change on this file since 2282 was 2282, checked in by sacerdot, 8 years ago

PUSH case almost finished

File size: 61.8 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               Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (lookup_from_internal_ram … d M) M)
866         | _ ⇒ λother: False. ⊥
867         ] (subaddressing_modein … addr1)
868       | POP addr1 ⇒
869         let sp ≝ get_8051_sfr ?? s SFR_SP in
870         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
871         [ DIRECT d ⇒ λproof.
872           let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
873             if head' … bit_one then
874               if eq_bv … d (bitvector_of_nat … 224) then
875                 Some … 〈low, high, lookup_from_internal_ram … sp M〉
876               else
877                 match lookup_from_internal_ram sp M with
878                 [ None ⇒ Some ? M
879                 | _    ⇒ None ?
880                 ]
881             else
882               Some … (overwrite_or_delete_from_internal_ram d (lookup_from_internal_ram … sp M) M)
883         | _ ⇒ λother: False. ⊥
884         ] (subaddressing_modein … addr1)
885       | XCH addr1 addr2 ⇒
886         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
887           Some ? M
888         else
889           None ?
890       | XCHD 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      | RET ⇒
896        let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
897        let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
898        match lookup_from_internal_ram sp_minus_1 M with
899        [ None ⇒ None …
900        | Some low_addr_high ⇒
901            match lookup_from_internal_ram sp_minus_2 M with
902            [ None ⇒ None …
903            | Some high_addr_low ⇒
904              let 〈low, addr_high〉 ≝ low_addr_high in
905              let 〈high, addr_low〉 ≝ high_addr_low in
906              let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
907              let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
908                if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
909                  Some ? M
910                else
911                  None ?
912            ]
913        ]
914      | RETI ⇒
915        let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
916        let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
917        match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M with
918        [ None ⇒ None …
919        | Some low_addr_high ⇒
920            match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) M with
921            [ None ⇒ None …
922            | Some high_addr_low ⇒
923              let 〈low, addr_high〉 ≝ low_addr_high in
924              let 〈high, addr_low〉 ≝ high_addr_low in
925              let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
926              let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
927                if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
928                  Some ? M
929                else
930                  None ?
931            ]
932        ]
933      | NOP ⇒ Some … M
934      | MOVX addr1 ⇒
935        match addr1 with
936        [ inl l ⇒
937            Some ? 〈low, high, None …〉
938        | inr r ⇒
939          let 〈others, acc_a〉 ≝ r in
940            if assert_data T M … s acc_a then
941              Some ? M
942            else
943              None ?
944        ]
945      | XRL addr1 ⇒
946        match addr1 with
947        [ inl l ⇒
948          let 〈acc_a, others〉 ≝ l in
949          let acc_a_ok ≝ assert_data T M … s acc_a in
950          let others_ok ≝ assert_data T M … s others in
951          if acc_a_ok ∧ others_ok then
952            Some ? M
953          else
954            None ?
955        | inr r ⇒
956          let 〈direct, others〉 ≝ r in
957          let direct_ok ≝ assert_data T M … s direct in
958          let others_ok ≝ assert_data T M … s others in
959          if direct_ok ∧ others_ok then
960            Some ? M
961          else
962            None ?
963        ]
964      | ORL addr1 ⇒
965        match addr1 with
966        [ inl l ⇒
967          match l with
968          [ inl l ⇒
969            let 〈acc_a, others〉 ≝ l in
970            let acc_a_ok ≝ assert_data T M … s acc_a in
971            let others_ok ≝ assert_data T M … s others in
972            if acc_a_ok ∧ others_ok then
973              Some ? M
974            else
975              None ?
976          | inr r ⇒
977            let 〈direct, others〉 ≝ r in
978            let direct_ok ≝ assert_data T M … s direct in
979            let others_ok ≝ assert_data T M … s others in
980            if direct_ok ∧ others_ok then
981              Some ? M
982            else
983              None ?
984          ]
985        | inr r ⇒
986          let 〈carry, others〉 ≝ r in
987          let carry_ok ≝ assert_data T M … s carry in
988          let others_ok ≝ assert_data T M … s others in
989          if carry_ok ∧ others_ok then
990            Some ? M
991          else
992            None ?
993        ]
994      | ANL addr1 ⇒
995        match addr1 with
996        [ inl l ⇒
997          match l with
998          [ inl l ⇒
999            let 〈acc_a, others〉 ≝ l in
1000            let acc_a_ok ≝ assert_data T M … s acc_a in
1001            let others_ok ≝ assert_data T M … s others in
1002            if acc_a_ok ∧ others_ok then
1003              Some ? M
1004            else
1005              None ?
1006          | inr r ⇒
1007            let 〈direct, others〉 ≝ r in
1008            let direct_ok ≝ assert_data T M … s direct in
1009            let others_ok ≝ assert_data T M … s others in
1010            if direct_ok ∧ others_ok then
1011              Some ? M
1012            else
1013              None ?
1014          ]
1015        | inr r ⇒
1016          let 〈carry, others〉 ≝ r in
1017          let carry_ok ≝ assert_data T M … s carry in
1018          let others_ok ≝ assert_data T M … s others in
1019          if carry_ok ∧ others_ok then
1020            Some ? M
1021          else
1022            None ?
1023        ]
1024      | MOV addr1 ⇒
1025        (* XXX: wrong *)
1026        match addr1 with
1027        [ inl l ⇒
1028          match l with
1029          [ inl l' ⇒
1030            match l' with
1031            [ inl l'' ⇒
1032              match l'' with
1033              [ inl l''' ⇒
1034                match l''' with
1035                [ inl l'''' ⇒
1036                  let 〈acc_a, others〉 ≝ l'''' in
1037                    match data_or_address T M … s others with
1038                    [ None ⇒ None ?
1039                    | Some s ⇒
1040                        Some … 〈low, high, s〉
1041                    ]
1042                | inr r ⇒
1043                  let 〈others, others'〉 ≝ r in
1044                  let address ≝
1045                    match others return λx. bool_to_Prop (is_in … [[ registr; indirect ]] x) → ? with
1046                    [ REGISTER r ⇒ λproof. false:::bit_address_of_register … s r
1047                    | INDIRECT i ⇒ λproof. get_register … s [[false; false; i]]
1048                    | _ ⇒ λother: False. ⊥
1049                    ] (subaddressing_modein … others)
1050                  in
1051                    match data_or_address T M … s others' with
1052                    [ None ⇒ None ?
1053                    | Some s ⇒
1054                        Some … (overwrite_or_delete_from_internal_ram address s M)
1055                    ]
1056                ]
1057              | inr r ⇒
1058                let 〈direct', others〉 ≝ r in
1059                  match direct' return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
1060                  [ DIRECT d ⇒ λproof.
1061                    match data_or_address T M … s others with
1062                    [ None ⇒ None ?
1063                    | Some s' ⇒
1064                        let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
1065                          if head' … bit_one then
1066                            if eq_bv … d (bitvector_of_nat … 224) then
1067                              Some … 〈low, high, s'〉
1068                            else
1069                              match s' with
1070                              [ None ⇒ Some ? M
1071                              | Some s'' ⇒ None ?
1072                              ]
1073                          else
1074                            Some … (overwrite_or_delete_from_internal_ram d s' M)
1075                    ]
1076                  | _ ⇒ λother: False. ⊥
1077                  ] (subaddressing_modein … direct')
1078              ]
1079            | inr r ⇒ Some … M
1080            ]
1081          | inr r ⇒
1082            let 〈carry, bit_addr〉 ≝ r in
1083            if assert_data T M … s bit_addr then
1084              Some ? M
1085            else
1086              None ?
1087          ]
1088        | inr r ⇒
1089          let 〈bit_addr, carry〉 ≝ r in
1090          if assert_data T M … s bit_addr then
1091            Some ? M
1092          else
1093            None ?
1094        ]
1095      ]
1096    ].
1097    cases other
1098qed.
1099
1100definition next_internal_pseudo_address_map ≝
1101 λM:internal_pseudo_address_map.
1102 λcm.
1103 λaddr_of.
1104 λs:PseudoStatus cm.
1105 λppc_ok.
1106    next_internal_pseudo_address_map0 ? cm addr_of
1107     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
1108
1109definition code_memory_of_pseudo_assembly_program:
1110    ∀pap:pseudo_assembly_program.
1111      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
1112  λpap.
1113  λsigma.
1114  λpolicy.
1115    let p ≝ pi1 … (assembly pap sigma policy) in
1116      load_code_memory (\fst p).
1117
1118definition sfr_8051_of_pseudo_sfr_8051 ≝
1119  λM: internal_pseudo_address_map.
1120  λsfrs: Vector Byte 19.
1121  λsigma: Word → Word.
1122    match \snd M with
1123    [ None ⇒ sfrs
1124    | Some upper_lower_address ⇒
1125      let index ≝ sfr_8051_index SFR_ACC_A in
1126      let acc_a ≝ get_index_v … sfrs index ? in
1127      let 〈upper_lower, address〉 ≝ upper_lower_address in
1128        if eq_upper_lower upper_lower upper then
1129          let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (acc_a@@address)) in
1130            set_index Byte 19 sfrs index high ?
1131        else
1132          let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (address@@acc_a)) in
1133            set_index Byte 19 sfrs index low ?
1134    ].
1135  //
1136qed.
1137
1138definition status_of_pseudo_status:
1139    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
1140      ∀sigma: Word → Word. ∀policy: Word → bool.
1141        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
1142  λM.
1143  λpap.
1144  λps.
1145  λsigma.
1146  λpolicy.
1147  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
1148  let pc ≝ sigma (program_counter … ps) in
1149  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … ps) in
1150  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M sigma (high_internal_ram … ps) in
1151     mk_PreStatus (BitVectorTrie Byte 16)
1152      cm
1153      lir
1154      hir
1155      (external_ram … ps)
1156      pc
1157      (sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma)
1158      (special_function_registers_8052 … ps)
1159      (p1_latch … ps)
1160      (p3_latch … ps)
1161      (clock … ps).
1162
1163(*
1164definition write_at_stack_pointer':
1165 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1166  λM: Type[0].
1167  λs: PreStatus M.
1168  λv: Byte.
1169    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
1170    let bit_zero ≝ get_index_v… nu O ? in
1171    let bit_1 ≝ get_index_v… nu 1 ? in
1172    let bit_2 ≝ get_index_v… nu 2 ? in
1173    let bit_3 ≝ get_index_v… nu 3 ? in
1174      if bit_zero then
1175        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1176                              v (low_internal_ram ? s) in
1177          set_low_internal_ram ? s memory
1178      else
1179        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1180                              v (high_internal_ram ? s) in
1181          set_high_internal_ram ? s memory.
1182  [ cases l0 %
1183  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1184qed.
1185
1186definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1187 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1188
1189  λticks_of.
1190  λs.
1191  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1192  let ticks ≝ ticks_of (program_counter ? s) in
1193  let s ≝ set_clock ? s (clock ? s + ticks) in
1194  let s ≝ set_program_counter ? s pc in
1195    match instr with
1196    [ Instruction instr ⇒
1197       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1198    | Comment cmt ⇒ s
1199    | Cost cst ⇒ s
1200    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1201    | Call call ⇒
1202      let a ≝ address_of_word_labels s call in
1203      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1204      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1205      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
1206      let s ≝ write_at_stack_pointer' ? s pc_bl in
1207      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1208      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1209      let s ≝ write_at_stack_pointer' ? s pc_bu in
1210        set_program_counter ? s a
1211    | Mov dptr ident ⇒
1212       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1213    ].
1214 [
1215 |2,3,4: %
1216 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1217 |
1218 | %
1219 ]
1220 cases not_implemented
1221qed.
1222*)
1223
1224(*
1225lemma execute_code_memory_unchanged:
1226 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1227 #ticks #ps whd in ⊢ (??? (??%))
1228 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1229  (program_counter pseudo_assembly_program ps)) #instr #pc
1230 whd in ⊢ (??? (??%)) cases instr
1231  [ #pre cases pre
1232     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1233       cases (vsplit ????) #z1 #z2 %
1234     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1235       cases (vsplit ????) #z1 #z2 %
1236     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1237       cases (vsplit ????) #z1 #z2 %
1238     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1239       [ #x1 whd in ⊢ (??? (??%))
1240     | *: cases not_implemented
1241     ]
1242  | #comment %
1243  | #cost %
1244  | #label %
1245  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1246    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1247    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
1248    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1249    (* CSC: ??? *)
1250  | #dptr #label (* CSC: ??? *)
1251  ]
1252  cases not_implemented
1253qed.
1254*)
1255
1256(* XXX: check values returned for conditional jumps below! They are wrong,
1257        find correct values *)
1258definition ticks_of0:
1259    ∀p:pseudo_assembly_program.
1260      (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
1261  λprogram: pseudo_assembly_program.
1262  λlookup_labels: Identifier → Word.
1263  λsigma.
1264  λpolicy.
1265  λppc: Word.
1266  λfetched.
1267    match fetched with
1268    [ Instruction instr ⇒
1269      match instr with
1270      [ JC lbl ⇒
1271        let lookup_address ≝ sigma (lookup_labels lbl) in
1272        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1273        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1274          if sj_possible then
1275            〈2, 2〉
1276          else
1277            〈4, 4〉
1278      | JNC lbl ⇒
1279        let lookup_address ≝ sigma (lookup_labels lbl) in
1280        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1281        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1282          if sj_possible then
1283            〈2, 2〉
1284          else
1285            〈4, 4〉
1286      | JB bit lbl ⇒
1287        let lookup_address ≝ sigma (lookup_labels lbl) in
1288        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1289        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1290          if sj_possible then
1291            〈2, 2〉
1292          else
1293            〈4, 4〉
1294      | JNB bit lbl ⇒
1295        let lookup_address ≝ sigma (lookup_labels lbl) in
1296        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1297        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1298          if sj_possible then
1299            〈2, 2〉
1300          else
1301            〈4, 4〉
1302      | JBC bit lbl ⇒
1303        let lookup_address ≝ sigma (lookup_labels lbl) in
1304        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1305        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1306          if sj_possible then
1307            〈2, 2〉
1308          else
1309            〈4, 4〉
1310      | JZ lbl ⇒
1311        let lookup_address ≝ sigma (lookup_labels lbl) in
1312        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1313        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1314          if sj_possible then
1315            〈2, 2〉
1316          else
1317            〈4, 4〉
1318      | JNZ lbl ⇒
1319        let lookup_address ≝ sigma (lookup_labels lbl) in
1320        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1321        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1322          if sj_possible then
1323            〈2, 2〉
1324          else
1325            〈4, 4〉
1326      | CJNE arg lbl ⇒
1327        let lookup_address ≝ sigma (lookup_labels lbl) in
1328        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1329        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1330          if sj_possible then
1331            〈2, 2〉
1332          else
1333            〈4, 4〉
1334      | DJNZ arg lbl ⇒
1335        let lookup_address ≝ sigma (lookup_labels lbl) in
1336        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1337        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1338          if sj_possible then
1339            〈2, 2〉
1340          else
1341            〈4, 4〉
1342      | ADD arg1 arg2 ⇒
1343        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1344         〈ticks, ticks〉
1345      | ADDC arg1 arg2 ⇒
1346        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1347         〈ticks, ticks〉
1348      | SUBB arg1 arg2 ⇒
1349        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1350         〈ticks, ticks〉
1351      | INC arg ⇒
1352        let ticks ≝ ticks_of_instruction (INC ? arg) in
1353         〈ticks, ticks〉
1354      | DEC arg ⇒
1355        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1356         〈ticks, ticks〉
1357      | MUL arg1 arg2 ⇒
1358        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1359         〈ticks, ticks〉
1360      | DIV arg1 arg2 ⇒
1361        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1362         〈ticks, ticks〉
1363      | DA arg ⇒
1364        let ticks ≝ ticks_of_instruction (DA ? arg) in
1365         〈ticks, ticks〉
1366      | ANL arg ⇒
1367        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1368         〈ticks, ticks〉
1369      | ORL arg ⇒
1370        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1371         〈ticks, ticks〉
1372      | XRL arg ⇒
1373        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1374         〈ticks, ticks〉
1375      | CLR arg ⇒
1376        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1377         〈ticks, ticks〉
1378      | CPL arg ⇒
1379        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1380         〈ticks, ticks〉
1381      | RL arg ⇒
1382        let ticks ≝ ticks_of_instruction (RL ? arg) in
1383         〈ticks, ticks〉
1384      | RLC arg ⇒
1385        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1386         〈ticks, ticks〉
1387      | RR arg ⇒
1388        let ticks ≝ ticks_of_instruction (RR ? arg) in
1389         〈ticks, ticks〉
1390      | RRC arg ⇒
1391        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1392         〈ticks, ticks〉
1393      | SWAP arg ⇒
1394        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1395         〈ticks, ticks〉
1396      | MOV arg ⇒
1397        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1398         〈ticks, ticks〉
1399      | MOVX arg ⇒
1400        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1401         〈ticks, ticks〉
1402      | SETB arg ⇒
1403        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1404         〈ticks, ticks〉
1405      | PUSH arg ⇒
1406        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1407         〈ticks, ticks〉
1408      | POP arg ⇒
1409        let ticks ≝ ticks_of_instruction (POP ? arg) in
1410         〈ticks, ticks〉
1411      | XCH arg1 arg2 ⇒
1412        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1413         〈ticks, ticks〉
1414      | XCHD arg1 arg2 ⇒
1415        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1416         〈ticks, ticks〉
1417      | RET ⇒
1418        let ticks ≝ ticks_of_instruction (RET ?) in
1419         〈ticks, ticks〉
1420      | RETI ⇒
1421        let ticks ≝ ticks_of_instruction (RETI ?) in
1422         〈ticks, ticks〉
1423      | NOP ⇒
1424        let ticks ≝ ticks_of_instruction (NOP ?) in
1425         〈ticks, ticks〉
1426      ]
1427    | Comment comment ⇒ 〈0, 0〉
1428    | Cost cost ⇒ 〈0, 0〉
1429    | Jmp jmp ⇒
1430      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1431      let do_a_long ≝ policy ppc in
1432      let lookup_address ≝ sigma (lookup_labels jmp) in
1433      let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1434        if sj_possible ∧ ¬ do_a_long then
1435          〈2, 2〉 (* XXX: SJMP *)
1436        else
1437        let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1438          if mj_possible ∧ ¬ do_a_long then
1439            〈2, 2〉 (* XXX: AJMP *)
1440          else
1441            〈2, 2〉 (* XXX: LJMP *)
1442    | Call call ⇒
1443      (* XXX: collapse the branches as they are identical? *)
1444      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1445      let lookup_address ≝ sigma (lookup_labels call) in
1446      let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1447      let do_a_long ≝ policy ppc in
1448      if mj_possible ∧ ¬ do_a_long then
1449        〈2, 2〉 (* ACALL *)
1450      else
1451        〈2, 2〉 (* LCALL *)
1452    | Mov dptr tgt ⇒ 〈2, 2〉
1453    ].
1454
1455definition ticks_of:
1456    ∀p:pseudo_assembly_program.
1457      (Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word.
1458       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
1459  λprogram: pseudo_assembly_program.
1460  λlookup_labels.
1461  λsigma.
1462  λpolicy.
1463  λppc: Word. λppc_ok.
1464    let pseudo ≝ \snd program in
1465    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
1466     ticks_of0 program lookup_labels sigma policy ppc fetched.
1467
1468(*
1469lemma blah:
1470  ∀m: internal_pseudo_address_map.
1471  ∀s: PseudoStatus.
1472  ∀arg: Byte.
1473  ∀b: bool.
1474    assert_data m s (DIRECT arg) = true →
1475      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1476      get_arg_8 ? s b (DIRECT arg).
1477  [2, 3: normalize % ]
1478  #m #s #arg #b #hyp
1479  whd in ⊢ (??%%)
1480  @vsplit_elim''
1481  #nu' #nl' #arg_nu_nl_eq
1482  normalize nodelta
1483  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1484  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1485  #get_index_v_eq
1486  normalize nodelta
1487  [2:
1488    normalize nodelta
1489    @vsplit_elim''
1490    #bit_one' #three_bits' #bit_one_three_bit_eq
1491    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1492    normalize nodelta
1493    generalize in match (refl ? (sub_7_with_carry ? ? ?))
1494    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1495    #Saddr #carr' #Saddr_carr_eq
1496    normalize nodelta
1497    #carr_hyp'
1498    @carr_hyp'
1499    [1:
1500    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1501        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1502        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1503        #member_eq
1504        normalize nodelta
1505        [2: #destr destruct(destr)
1506        |1: -carr_hyp';
1507            >arg_nu_nl_eq
1508            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1509            [1: >get_index_v_eq in ⊢ (??%? → ?)
1510            |2: @le_S @le_S @le_S @le_n
1511            ]
1512            cases (member (BitVector 8) ? (\fst ?) ?)
1513            [1: #destr normalize in destr; destruct(destr)
1514            |2:
1515            ]
1516        ]
1517    |3: >get_index_v_eq in ⊢ (??%?)
1518        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1519        >(vsplit_vector_singleton … bit_one_three_bit_eq)
1520        <arg_nu_nl_eq
1521        whd in hyp:(??%?)
1522        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1523        normalize nodelta [*: #ignore @sym_eq ]
1524    ]
1525  |
1526  ].
1527*)
1528(*
1529map_address0 ... (DIRECT arg) = Some .. →
1530  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1531  get_arg_8 (internal_ram ...) (DIRECT arg)
1532
1533((if assert_data M ps ACC_A∧assert_data M ps (DIRECT ARG2) 
1534                     then Some internal_pseudo_address_map M 
1535                     else None internal_pseudo_address_map )
1536                    =Some internal_pseudo_address_map M')
1537
1538axiom low_internal_ram_write_at_stack_pointer:
1539 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
1540 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1541  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1542  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
1543  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1544  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1545  bu@@bl = sigma (pbu@@pbl) →
1546   low_internal_ram T1 cm1
1547     (write_at_stack_pointer …
1548       (set_8051_sfr …
1549         (write_at_stack_pointer …
1550           (set_8051_sfr …
1551             (set_low_internal_ram … s1
1552               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
1553             SFR_SP sp1)
1554          bl)
1555        SFR_SP sp2)
1556      bu)
1557   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1558      (low_internal_ram …
1559       (write_at_stack_pointer …
1560         (set_8051_sfr …
1561           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1562          SFR_SP sp2)
1563        pbu)).
1564
1565lemma high_internal_ram_write_at_stack_pointer:
1566 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
1567 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1568  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1569  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
1570  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1571  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1572  bu@@bl = sigma (pbu@@pbl) →
1573   high_internal_ram T1 cm1
1574     (write_at_stack_pointer …
1575       (set_8051_sfr …
1576         (write_at_stack_pointer …
1577           (set_8051_sfr …
1578             (set_high_internal_ram … s1
1579               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
1580             SFR_SP sp1)
1581          bl)
1582        SFR_SP sp2)
1583      bu)
1584   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
1585      (high_internal_ram …
1586       (write_at_stack_pointer …
1587         (set_8051_sfr …
1588           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1589          SFR_SP sp2)
1590        pbu)).
1591  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
1592  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
1593  cases daemon (* XXX: !!! *)
1594qed.
1595*)
1596
1597lemma snd_assembly_1_pseudoinstruction_ok:
1598  ∀program: pseudo_assembly_program.
1599  ∀program_length_proof: |\snd program| ≤ 2^16.
1600  ∀sigma: Word → Word.
1601  ∀policy: Word → bool.
1602  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1603  ∀ppc: Word.
1604  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
1605  ∀pi.
1606  ∀lookup_labels.
1607  ∀lookup_datalabels.
1608    let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
1609    lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →
1610    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1611    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
1612    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
1613      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
1614  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
1615  #lookup_labels #lookup_datalabels
1616  @pair_elim #labels #costs #create_label_cost_map_refl
1617  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
1618  normalize nodelta
1619  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
1620  #fetch_pseudo_refl
1621  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
1622  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
1623  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
1624  @pair_elim #preamble #instr_list #program_refl
1625  lapply create_label_cost_map_refl; -create_label_cost_map_refl
1626  >program_refl in ⊢ (% → ?); #create_label_cost_map_refl
1627  >create_label_cost_map_refl
1628  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
1629  lapply (H ppc ppc_in_bounds) -H
1630  @pair_elim #pi' #newppc #fetch_pseudo_refl'
1631  @pair_elim #len #assembled #assembly1_refl #H
1632  cases H
1633  #encoding_check_assm #sigma_newppc_refl
1634  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
1635  >pi_refl' in assembly1_refl; #assembly1_refl
1636  >lookup_labels_refl >lookup_datalabels_refl
1637  >program_refl normalize nodelta
1638  >assembly1_refl
1639  <sigma_newppc_refl
1640  generalize in match fetch_pseudo_refl';
1641  whd in match (fetch_pseudo_instruction ???);
1642  @pair_elim #lbl #instr #nth_refl normalize nodelta
1643  #G cases (pair_destruct_right ?????? G) %
1644qed.
1645
1646(* To be moved in ProofStatus *)
1647lemma program_counter_set_program_counter:
1648  ∀T.
1649  ∀cm.
1650  ∀s.
1651  ∀x.
1652    program_counter T cm (set_program_counter T cm s x) = x.
1653  //
1654qed.
Note: See TracBrowser for help on using the repository browser.