source: src/ASM/AssemblyProof.ma @ 2276

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

...

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