source: src/ASM/AssemblyProof.ma @ 2197

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

Main lemmas all closed.

File size: 49.3 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
337inductive accumulator_address_map_entry: Type[0] ≝
338  | data: accumulator_address_map_entry
339  | address: upper_lower → Word → accumulator_address_map_entry.
340
341definition eq_accumulator_address_map_entry:
342    accumulator_address_map_entry → accumulator_address_map_entry → bool ≝
343  λleft: accumulator_address_map_entry.
344  λright: accumulator_address_map_entry.
345    match left with
346    [ data                     ⇒
347      match right with
348      [ data ⇒ true
349      | _    ⇒ false
350      ]
351    | address upper_lower word ⇒
352      match right with
353      [ address upper_lower' word' ⇒
354          eq_upper_lower upper_lower upper_lower' ∧ eq_bv … word word'
355      | _                          ⇒ false
356      ]
357    ].
358
359lemma eq_accumulator_address_map_entry_true_to_eq:
360  ∀left: accumulator_address_map_entry.
361  ∀right: accumulator_address_map_entry.
362    eq_accumulator_address_map_entry left right = true → left = right.
363  #left #right cases left cases right
364  [1:
365    #_ %
366  |2,3:
367    #upper_lower #word normalize #absurd destruct(absurd)
368  |4:
369    #upper_lower #word #upper_lower' #word' normalize
370    cases upper_lower' normalize nodelta
371    cases upper_lower normalize
372    [2,3:
373      #absurd destruct(absurd)
374    ]
375    change with (eq_bv 16 ?? = true → ?)
376    #relevant lapply (eq_bv_eq … relevant)
377    #word_refl >word_refl %
378  ]
379qed.
380
381lemma eq_bv_false_to_neq:
382  ∀n: nat.
383  ∀left, right: BitVector n.
384    eq_bv n left right = false → left ≠ right.
385  #n #left elim left
386  [1:
387    #right >(BitVector_O … right) normalize #absurd destruct(absurd)
388  |2:
389    #n' #hd #tl #inductive_hypothesis #right
390    cases (BitVector_Sn … right) #hd' * #tl' #right_refl
391    >right_refl normalize
392    cases hd normalize nodelta
393    cases hd' normalize nodelta
394    [2,3:
395      #_ @nmk #absurd destruct(absurd)
396    ]
397    change with (eq_bv ??? = false → ?)
398    #relevant lapply (inductive_hypothesis … relevant)
399    #tl_neq_assm @nmk #tl_eq_assm cases tl_neq_assm
400    #tl_eq_assm' @tl_eq_assm' destruct(tl_eq_assm) %
401  ]
402qed.
403   
404lemma eq_accumulator_address_map_entry_false_to_neq:
405  ∀left: accumulator_address_map_entry.
406  ∀right: accumulator_address_map_entry.
407    eq_accumulator_address_map_entry left right = false → left ≠ right.
408  #left #right cases left cases right
409  [1:
410    normalize #absurd destruct(absurd)
411  |2,3:
412    #upper_lower #word normalize #_
413    @nmk #absurd destruct(absurd)
414  |4:
415    #upper_lower #word #upper_lower' #word' normalize
416    cases upper_lower' normalize nodelta
417    cases upper_lower normalize nodelta
418    [2,3:
419      #_ @nmk #absurd destruct(absurd)
420    ]
421    change with (eq_bv ??? = false → ?)
422    #eq_bv_false_assm lapply(eq_bv_false_to_neq … eq_bv_false_assm)
423    #word_neq_assm @nmk #address_eq_assm cases word_neq_assm
424    #word_eq_assm @word_eq_assm destruct(address_eq_assm) %
425  ]
426qed.
427
428(* XXX: changed this type.  Bool specifies whether byte is first or second
429        component of an address, and the Word is the pseudoaddress that it
430        corresponds to.  Second component is the same principle for the accumulator
431        A.
432*)
433definition internal_pseudo_address_map ≝ list (Byte × (upper_lower × Word)) × accumulator_address_map_entry.
434
435include alias "ASM/BitVectorTrie.ma".
436 
437include "common/AssocList.ma".
438
439axiom low_internal_ram_of_pseudo_low_internal_ram:
440 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
441
442axiom high_internal_ram_of_pseudo_high_internal_ram:
443 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
444
445axiom low_internal_ram_of_pseudo_internal_ram_hit:
446 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.
447  assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉  →
448   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
449   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
450   let bl ≝ lookup ? 7 addr ram (zero 8) in
451   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
452   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
453     if eq_upper_lower upper_lower upper then
454       (pbl = higher) ∧ (bl = phigher)
455     else
456       (pbl = lower) ∧ (bl = plower).
457
458(* changed from add to sub *)
459axiom low_internal_ram_of_pseudo_internal_ram_miss:
460 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
461  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
462    assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →
463      lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
464
465definition addressing_mode_ok ≝
466 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
467  λaddr:addressing_mode.
468   match addr with
469    [ DIRECT d ⇒
470        if eq_bv … d (bitvector_of_nat … 224) then
471          ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) ∧ eq_accumulator_address_map_entry (\snd M) data
472        else
473         ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
474    | INDIRECT i ⇒
475       let d ≝ get_register … s [[false;false;i]] in
476       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M))
477    | EXT_INDIRECT _ ⇒ true
478    | REGISTER r ⇒
479        let address ≝ bit_address_of_register … s r in
480          ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M)
481    | ACC_A ⇒ match \snd M with [ data ⇒ true | _ ⇒ false ]
482    | ACC_B ⇒ true
483    | DPTR ⇒ true
484    | DATA _ ⇒ true
485    | DATA16 _ ⇒ true
486    | ACC_DPTR ⇒ true
487    | ACC_PC ⇒ true
488    | EXT_INDIRECT_DPTR ⇒ true
489    | INDIRECT_DPTR ⇒ true
490    | CARRY ⇒ true
491    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
492    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
493    | RELATIVE _ ⇒ true
494    | ADDR11 _ ⇒ true
495    | ADDR16 _ ⇒ true
496    ].
497   
498definition next_internal_pseudo_address_map0 ≝
499  λT.
500  λcm:T.
501  λaddr_of: Identifier → PreStatus T cm → Word.
502  λfetched.
503  λM: internal_pseudo_address_map.
504  λs: PreStatus T cm.
505   match fetched with
506    [ Comment _ ⇒ Some ? M
507    | Cost _ ⇒ Some … M
508    | Jmp _ ⇒ Some … M
509    | Call a ⇒
510      let a' ≝ addr_of a s in
511      let 〈callM, accM〉 ≝ M in
512         Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, a'〉〉::
513                 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈upper, a'〉〉::callM, accM〉
514    | Mov _ _ ⇒ Some … M
515    | Instruction instr ⇒
516      match instr return λx. option internal_pseudo_address_map with
517       [ ADD addr1 addr2 ⇒
518         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
519           Some ? M
520         else
521           None ?
522       | ADDC addr1 addr2 ⇒
523         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
524           Some ? M
525         else
526           None ?
527       | SUBB addr1 addr2 ⇒
528         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
529           Some ? M
530         else
531           None ?
532       | INC addr1 ⇒
533         if addressing_mode_ok T M ? s addr1 then
534           Some ? M
535         else
536           None ?
537       | DEC addr1 ⇒
538         if addressing_mode_ok T M … s addr1 then
539           Some ? M
540         else
541           None ?
542       | MUL addr1 addr2 ⇒
543         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
544           Some ? M
545         else
546           None ?
547       | DIV addr1 addr2 ⇒
548         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
549           Some ? M
550         else
551           None ?
552       | DA addr1 ⇒
553         if addressing_mode_ok T M … s addr1 then
554           Some ? M
555         else
556           None ?
557       | JC addr1 ⇒ Some ? M
558       | JNC addr1 ⇒ Some ? M
559       | JB addr1 addr2 ⇒ Some ? M
560       | JNB addr1 addr2 ⇒ Some ? M
561       | JBC addr1 addr2 ⇒ Some ? M
562       | JZ addr1 ⇒ Some ? M
563       | JNZ addr1 ⇒ Some ? M
564       | CJNE addr1 addr2 ⇒
565         match addr1 with
566         [ inl l ⇒
567           let 〈left, right〉 ≝ l in
568             if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then
569               Some ? M
570             else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then
571               Some ? M
572             else
573               None ?
574         | inr r ⇒
575           let 〈left, right〉 ≝ r in
576             if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then
577               Some ? M
578             else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then
579               Some ? M
580             else
581               None ?
582         ]
583       | DJNZ addr1 addr2 ⇒
584         if addressing_mode_ok T M … s addr1 then
585           Some ? M
586         else
587           None ?
588       | CLR addr1 ⇒
589         if addressing_mode_ok T M … s addr1 then
590           Some ? M
591         else
592           None ?
593       | CPL addr1 ⇒
594         if addressing_mode_ok T M … s addr1 then
595           Some ? M
596         else
597           None ?
598       | RL addr1 ⇒
599         if addressing_mode_ok T M … s addr1 then
600           Some ? M
601         else
602           None ?
603       | RLC addr1 ⇒
604         if addressing_mode_ok T M … s addr1 then
605           Some ? M
606         else
607           None ?
608       | RR addr1 ⇒
609         if addressing_mode_ok T M … s addr1 then
610           Some ? M
611         else
612           None ?
613       | RRC addr1 ⇒
614         if addressing_mode_ok T M … s addr1 then
615           Some ? M
616         else
617           None ?
618       | SWAP addr1 ⇒
619         if addressing_mode_ok T M … s addr1 then
620           Some ? M
621         else
622           None ?
623       | SETB addr1 ⇒
624         if addressing_mode_ok T M … s addr1 then
625           Some ? M
626         else
627           None ?
628       (* XXX: need to track addresses pushed and popped off the stack? *)
629       | PUSH addr1 ⇒
630         let 〈callM, accM〉 ≝ M in
631         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
632         [ DIRECT d ⇒ λproof.
633           let extended ≝ pad 8 8 d in
634             Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, extended〉〉::callM, accM〉
635         | _ ⇒ λother: False. ⊥
636         ] (subaddressing_modein … addr1)
637       | POP addr1 ⇒ Some … M
638       | XCH addr1 addr2 ⇒
639         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
640           Some ? M
641         else
642           None ?
643       | XCHD addr1 addr2 ⇒
644         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
645           Some ? M
646         else
647           None ?
648      | RET ⇒
649        let 〈callM, accM〉 ≝ M in
650        let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
651        let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
652          if sp_plus_1 ∧ sp_plus_2 then
653            Some … M
654          else
655            None ?
656      | RETI ⇒
657        let 〈callM, accM〉 ≝ M in
658        let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
659        let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
660          if sp_plus_1 ∧ sp_plus_2 then
661            Some … M
662          else
663            None ?
664      | NOP ⇒ Some … M
665      | MOVX addr1 ⇒ Some … M
666      | XRL addr1 ⇒
667        match addr1 with
668        [ inl l ⇒
669          let 〈acc_a, others〉 ≝ l in
670          let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
671          let others_ok ≝ addressing_mode_ok T M … s others in
672          if acc_a_ok ∧ others_ok then
673            Some ? M
674          else
675            None ?
676        | inr r ⇒
677          let 〈direct, others〉 ≝ r in
678          let direct_ok ≝ addressing_mode_ok T M … s direct in
679          let others_ok ≝ addressing_mode_ok T M … s others in
680          if direct_ok ∧ others_ok then
681            Some ? M
682          else
683            None ?
684        ]
685      | ORL addr1 ⇒
686        match addr1 with
687        [ inl l ⇒
688          match l with
689          [ inl l ⇒
690            let 〈acc_a, others〉 ≝ l in
691            let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
692            let others_ok ≝ addressing_mode_ok T M … s others in
693            if acc_a_ok ∧ others_ok then
694              Some ? M
695            else
696              None ?
697          | inr r ⇒
698            let 〈direct, others〉 ≝ r in
699            let direct_ok ≝ addressing_mode_ok T M … s direct in
700            let others_ok ≝ addressing_mode_ok T M … s others in
701            if direct_ok ∧ others_ok then
702              Some ? M
703            else
704              None ?
705          ]
706        | inr r ⇒
707          let 〈carry, others〉 ≝ r in
708          let carry_ok ≝ addressing_mode_ok T M … s carry in
709          let others_ok ≝ addressing_mode_ok T M … s others in
710          if carry_ok ∧ others_ok then
711            Some ? M
712          else
713            None ?
714        ]
715      | ANL addr1 ⇒
716        match addr1 with
717        [ inl l ⇒
718          match l with
719          [ inl l ⇒
720            let 〈acc_a, others〉 ≝ l in
721            let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
722            let others_ok ≝ addressing_mode_ok T M … s others in
723            if acc_a_ok ∧ others_ok then
724              Some ? M
725            else
726              None ?
727          | inr r ⇒
728            let 〈direct, others〉 ≝ r in
729            let direct_ok ≝ addressing_mode_ok T M … s direct in
730            let others_ok ≝ addressing_mode_ok T M … s others in
731            if direct_ok ∧ others_ok then
732              Some ? M
733            else
734              None ?
735          ]
736        | inr r ⇒
737          let 〈carry, others〉 ≝ r in
738          let carry_ok ≝ addressing_mode_ok T M … s carry in
739          let others_ok ≝ addressing_mode_ok T M … s others in
740          if carry_ok ∧ others_ok then
741            Some ? M
742          else
743            None ?
744        ]
745      | MOV addr1 ⇒ Some … M
746      ]
747    ].
748    cases other
749qed.
750
751definition next_internal_pseudo_address_map ≝
752 λM:internal_pseudo_address_map.
753 λcm.
754 λaddr_of.
755 λs:PseudoStatus cm.
756 λppc_ok.
757    next_internal_pseudo_address_map0 ? cm addr_of
758     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
759
760definition code_memory_of_pseudo_assembly_program:
761    ∀pap:pseudo_assembly_program.
762      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
763  λpap.
764  λsigma.
765  λpolicy.
766    let p ≝ pi1 … (assembly pap sigma policy) in
767      load_code_memory (\fst p).
768
769definition sfr_8051_of_pseudo_sfr_8051 ≝
770  λM: internal_pseudo_address_map.
771  λsfrs: Vector Byte 19.
772  λsigma: Word → Word.
773    match \snd M with
774    [ data ⇒ sfrs
775    | address upper_lower address ⇒
776      let index ≝ sfr_8051_index SFR_ACC_A in
777      let 〈high, low〉 ≝ vsplit ? 8 8 (sigma address) in
778        if eq_upper_lower upper_lower upper then
779          set_index Byte 19 sfrs index high ?
780        else
781          set_index Byte 19 sfrs index low ?
782    ].
783  //
784qed.
785
786definition status_of_pseudo_status:
787    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
788      ∀sigma: Word → Word. ∀policy: Word → bool.
789        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
790  λM.
791  λpap.
792  λps.
793  λsigma.
794  λpolicy.
795  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
796  let pc ≝ sigma (program_counter … ps) in
797  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
798  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
799     mk_PreStatus (BitVectorTrie Byte 16)
800      cm
801      lir
802      hir
803      (external_ram … ps)
804      pc
805      (sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma)
806      (special_function_registers_8052 … ps)
807      (p1_latch … ps)
808      (p3_latch … ps)
809      (clock … ps).
810
811(*
812definition write_at_stack_pointer':
813 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
814  λM: Type[0].
815  λs: PreStatus M.
816  λv: Byte.
817    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
818    let bit_zero ≝ get_index_v… nu O ? in
819    let bit_1 ≝ get_index_v… nu 1 ? in
820    let bit_2 ≝ get_index_v… nu 2 ? in
821    let bit_3 ≝ get_index_v… nu 3 ? in
822      if bit_zero then
823        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
824                              v (low_internal_ram ? s) in
825          set_low_internal_ram ? s memory
826      else
827        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
828                              v (high_internal_ram ? s) in
829          set_high_internal_ram ? s memory.
830  [ cases l0 %
831  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
832qed.
833
834definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
835 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
836
837  λticks_of.
838  λs.
839  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
840  let ticks ≝ ticks_of (program_counter ? s) in
841  let s ≝ set_clock ? s (clock ? s + ticks) in
842  let s ≝ set_program_counter ? s pc in
843    match instr with
844    [ Instruction instr ⇒
845       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
846    | Comment cmt ⇒ s
847    | Cost cst ⇒ s
848    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
849    | Call call ⇒
850      let a ≝ address_of_word_labels s call in
851      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
852      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
853      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
854      let s ≝ write_at_stack_pointer' ? s pc_bl in
855      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
856      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
857      let s ≝ write_at_stack_pointer' ? s pc_bu in
858        set_program_counter ? s a
859    | Mov dptr ident ⇒
860       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
861    ].
862 [
863 |2,3,4: %
864 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
865 |
866 | %
867 ]
868 cases not_implemented
869qed.
870*)
871
872(*
873lemma execute_code_memory_unchanged:
874 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
875 #ticks #ps whd in ⊢ (??? (??%))
876 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
877  (program_counter pseudo_assembly_program ps)) #instr #pc
878 whd in ⊢ (??? (??%)) cases instr
879  [ #pre cases pre
880     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
881       cases (vsplit ????) #z1 #z2 %
882     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
883       cases (vsplit ????) #z1 #z2 %
884     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
885       cases (vsplit ????) #z1 #z2 %
886     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
887       [ #x1 whd in ⊢ (??? (??%))
888     | *: cases not_implemented
889     ]
890  | #comment %
891  | #cost %
892  | #label %
893  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
894    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
895    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
896    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
897    (* CSC: ??? *)
898  | #dptr #label (* CSC: ??? *)
899  ]
900  cases not_implemented
901qed.
902*)
903
904(* XXX: check values returned for conditional jumps below! They are wrong,
905        find correct values *)
906definition ticks_of0:
907    ∀p:pseudo_assembly_program.
908      (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
909  λprogram: pseudo_assembly_program.
910  λlookup_labels: Identifier → Word.
911  λsigma.
912  λpolicy.
913  λppc: Word.
914  λfetched.
915    match fetched with
916    [ Instruction instr ⇒
917      match instr with
918      [ JC lbl ⇒
919        let lookup_address ≝ sigma (lookup_labels lbl) in
920        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
921        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
922          if sj_possible then
923            〈2, 2〉
924          else
925            〈4, 4〉
926      | JNC lbl ⇒
927        let lookup_address ≝ sigma (lookup_labels lbl) in
928        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
929        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
930          if sj_possible then
931            〈2, 2〉
932          else
933            〈4, 4〉
934      | JB bit lbl ⇒
935        let lookup_address ≝ sigma (lookup_labels lbl) in
936        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
937        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
938          if sj_possible then
939            〈2, 2〉
940          else
941            〈4, 4〉
942      | JNB bit lbl ⇒
943        let lookup_address ≝ sigma (lookup_labels lbl) in
944        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
945        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
946          if sj_possible then
947            〈2, 2〉
948          else
949            〈4, 4〉
950      | JBC bit lbl ⇒
951        let lookup_address ≝ sigma (lookup_labels lbl) in
952        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
953        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
954          if sj_possible then
955            〈2, 2〉
956          else
957            〈4, 4〉
958      | JZ lbl ⇒
959        let lookup_address ≝ sigma (lookup_labels lbl) in
960        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
961        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
962          if sj_possible then
963            〈2, 2〉
964          else
965            〈4, 4〉
966      | JNZ lbl ⇒
967        let lookup_address ≝ sigma (lookup_labels lbl) in
968        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
969        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
970          if sj_possible then
971            〈2, 2〉
972          else
973            〈4, 4〉
974      | CJNE arg lbl ⇒
975        let lookup_address ≝ sigma (lookup_labels lbl) in
976        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
977        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
978          if sj_possible then
979            〈2, 2〉
980          else
981            〈4, 4〉
982      | DJNZ arg lbl ⇒
983        let lookup_address ≝ sigma (lookup_labels lbl) in
984        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
985        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
986          if sj_possible then
987            〈2, 2〉
988          else
989            〈4, 4〉
990      | ADD arg1 arg2 ⇒
991        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
992         〈ticks, ticks〉
993      | ADDC arg1 arg2 ⇒
994        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
995         〈ticks, ticks〉
996      | SUBB arg1 arg2 ⇒
997        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
998         〈ticks, ticks〉
999      | INC arg ⇒
1000        let ticks ≝ ticks_of_instruction (INC ? arg) in
1001         〈ticks, ticks〉
1002      | DEC arg ⇒
1003        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1004         〈ticks, ticks〉
1005      | MUL arg1 arg2 ⇒
1006        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1007         〈ticks, ticks〉
1008      | DIV arg1 arg2 ⇒
1009        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1010         〈ticks, ticks〉
1011      | DA arg ⇒
1012        let ticks ≝ ticks_of_instruction (DA ? arg) in
1013         〈ticks, ticks〉
1014      | ANL arg ⇒
1015        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1016         〈ticks, ticks〉
1017      | ORL arg ⇒
1018        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1019         〈ticks, ticks〉
1020      | XRL arg ⇒
1021        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1022         〈ticks, ticks〉
1023      | CLR arg ⇒
1024        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1025         〈ticks, ticks〉
1026      | CPL arg ⇒
1027        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1028         〈ticks, ticks〉
1029      | RL arg ⇒
1030        let ticks ≝ ticks_of_instruction (RL ? arg) in
1031         〈ticks, ticks〉
1032      | RLC arg ⇒
1033        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1034         〈ticks, ticks〉
1035      | RR arg ⇒
1036        let ticks ≝ ticks_of_instruction (RR ? arg) in
1037         〈ticks, ticks〉
1038      | RRC arg ⇒
1039        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1040         〈ticks, ticks〉
1041      | SWAP arg ⇒
1042        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1043         〈ticks, ticks〉
1044      | MOV arg ⇒
1045        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1046         〈ticks, ticks〉
1047      | MOVX arg ⇒
1048        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1049         〈ticks, ticks〉
1050      | SETB arg ⇒
1051        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1052         〈ticks, ticks〉
1053      | PUSH arg ⇒
1054        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1055         〈ticks, ticks〉
1056      | POP arg ⇒
1057        let ticks ≝ ticks_of_instruction (POP ? arg) in
1058         〈ticks, ticks〉
1059      | XCH arg1 arg2 ⇒
1060        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1061         〈ticks, ticks〉
1062      | XCHD arg1 arg2 ⇒
1063        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1064         〈ticks, ticks〉
1065      | RET ⇒
1066        let ticks ≝ ticks_of_instruction (RET ?) in
1067         〈ticks, ticks〉
1068      | RETI ⇒
1069        let ticks ≝ ticks_of_instruction (RETI ?) in
1070         〈ticks, ticks〉
1071      | NOP ⇒
1072        let ticks ≝ ticks_of_instruction (NOP ?) in
1073         〈ticks, ticks〉
1074      ]
1075    | Comment comment ⇒ 〈0, 0〉
1076    | Cost cost ⇒ 〈0, 0〉
1077    | Jmp jmp ⇒
1078      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1079      let do_a_long ≝ policy ppc in
1080      let lookup_address ≝ sigma (lookup_labels jmp) in
1081      let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1082        if sj_possible ∧ ¬ do_a_long then
1083          〈2, 2〉 (* XXX: SJMP *)
1084        else
1085        let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1086          if mj_possible ∧ ¬ do_a_long then
1087            〈2, 2〉 (* XXX: AJMP *)
1088          else
1089            〈2, 2〉 (* XXX: LJMP *)
1090    | Call call ⇒
1091      (* XXX: collapse the branches as they are identical? *)
1092      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1093      let lookup_address ≝ sigma (lookup_labels call) in
1094      let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1095      let do_a_long ≝ policy ppc in
1096      if mj_possible ∧ ¬ do_a_long then
1097        〈2, 2〉 (* ACALL *)
1098      else
1099        〈2, 2〉 (* LCALL *)
1100    | Mov dptr tgt ⇒ 〈2, 2〉
1101    ].
1102
1103definition ticks_of:
1104    ∀p:pseudo_assembly_program.
1105      (Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word.
1106       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
1107  λprogram: pseudo_assembly_program.
1108  λlookup_labels.
1109  λsigma.
1110  λpolicy.
1111  λppc: Word. λppc_ok.
1112    let pseudo ≝ \snd program in
1113    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
1114     ticks_of0 program lookup_labels sigma policy ppc fetched.
1115
1116(*
1117lemma blah:
1118  ∀m: internal_pseudo_address_map.
1119  ∀s: PseudoStatus.
1120  ∀arg: Byte.
1121  ∀b: bool.
1122    addressing_mode_ok m s (DIRECT arg) = true →
1123      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1124      get_arg_8 ? s b (DIRECT arg).
1125  [2, 3: normalize % ]
1126  #m #s #arg #b #hyp
1127  whd in ⊢ (??%%)
1128  @vsplit_elim''
1129  #nu' #nl' #arg_nu_nl_eq
1130  normalize nodelta
1131  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1132  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1133  #get_index_v_eq
1134  normalize nodelta
1135  [2:
1136    normalize nodelta
1137    @vsplit_elim''
1138    #bit_one' #three_bits' #bit_one_three_bit_eq
1139    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1140    normalize nodelta
1141    generalize in match (refl ? (sub_7_with_carry ? ? ?))
1142    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1143    #Saddr #carr' #Saddr_carr_eq
1144    normalize nodelta
1145    #carr_hyp'
1146    @carr_hyp'
1147    [1:
1148    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1149        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1150        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1151        #member_eq
1152        normalize nodelta
1153        [2: #destr destruct(destr)
1154        |1: -carr_hyp';
1155            >arg_nu_nl_eq
1156            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1157            [1: >get_index_v_eq in ⊢ (??%? → ?)
1158            |2: @le_S @le_S @le_S @le_n
1159            ]
1160            cases (member (BitVector 8) ? (\fst ?) ?)
1161            [1: #destr normalize in destr; destruct(destr)
1162            |2:
1163            ]
1164        ]
1165    |3: >get_index_v_eq in ⊢ (??%?)
1166        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1167        >(vsplit_vector_singleton … bit_one_three_bit_eq)
1168        <arg_nu_nl_eq
1169        whd in hyp:(??%?)
1170        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1171        normalize nodelta [*: #ignore @sym_eq ]
1172    ]
1173  |
1174  ].
1175*)
1176(*
1177map_address0 ... (DIRECT arg) = Some .. →
1178  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1179  get_arg_8 (internal_ram ...) (DIRECT arg)
1180
1181((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
1182                     then Some internal_pseudo_address_map M 
1183                     else None internal_pseudo_address_map )
1184                    =Some internal_pseudo_address_map M')
1185
1186axiom low_internal_ram_write_at_stack_pointer:
1187 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
1188 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1189  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1190  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
1191  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1192  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1193  bu@@bl = sigma (pbu@@pbl) →
1194   low_internal_ram T1 cm1
1195     (write_at_stack_pointer …
1196       (set_8051_sfr …
1197         (write_at_stack_pointer …
1198           (set_8051_sfr …
1199             (set_low_internal_ram … s1
1200               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
1201             SFR_SP sp1)
1202          bl)
1203        SFR_SP sp2)
1204      bu)
1205   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1206      (low_internal_ram …
1207       (write_at_stack_pointer …
1208         (set_8051_sfr …
1209           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1210          SFR_SP sp2)
1211        pbu)).
1212
1213lemma high_internal_ram_write_at_stack_pointer:
1214 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
1215 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1216  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1217  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
1218  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1219  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1220  bu@@bl = sigma (pbu@@pbl) →
1221   high_internal_ram T1 cm1
1222     (write_at_stack_pointer …
1223       (set_8051_sfr …
1224         (write_at_stack_pointer …
1225           (set_8051_sfr …
1226             (set_high_internal_ram … s1
1227               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
1228             SFR_SP sp1)
1229          bl)
1230        SFR_SP sp2)
1231      bu)
1232   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
1233      (high_internal_ram …
1234       (write_at_stack_pointer …
1235         (set_8051_sfr …
1236           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1237          SFR_SP sp2)
1238        pbu)).
1239  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
1240  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
1241  cases daemon (* XXX: !!! *)
1242qed.
1243*)
1244
1245lemma snd_assembly_1_pseudoinstruction_ok:
1246  ∀program: pseudo_assembly_program.
1247  ∀program_length_proof: |\snd program| ≤ 2^16.
1248  ∀sigma: Word → Word.
1249  ∀policy: Word → bool.
1250  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1251  ∀ppc: Word.
1252  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
1253  ∀pi.
1254  ∀lookup_labels.
1255  ∀lookup_datalabels.
1256    let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
1257    lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →
1258    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1259    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
1260    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
1261      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
1262  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
1263  #lookup_labels #lookup_datalabels
1264  @pair_elim #labels #costs #create_label_cost_map_refl
1265  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
1266  normalize nodelta
1267  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
1268  #fetch_pseudo_refl
1269  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
1270  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
1271  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
1272  @pair_elim #preamble #instr_list #program_refl
1273  lapply create_label_cost_map_refl; -create_label_cost_map_refl
1274  >program_refl in ⊢ (% → ?); #create_label_cost_map_refl
1275  >create_label_cost_map_refl
1276  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
1277  lapply (H ppc ppc_in_bounds) -H
1278  @pair_elim #pi' #newppc #fetch_pseudo_refl'
1279  @pair_elim #len #assembled #assembly1_refl #H
1280  cases H
1281  #encoding_check_assm #sigma_newppc_refl
1282  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
1283  >pi_refl' in assembly1_refl; #assembly1_refl
1284  >lookup_labels_refl >lookup_datalabels_refl
1285  >program_refl normalize nodelta
1286  >assembly1_refl
1287  <sigma_newppc_refl
1288  generalize in match fetch_pseudo_refl';
1289  whd in match (fetch_pseudo_instruction ???);
1290  @pair_elim #lbl #instr #nth_refl normalize nodelta
1291  #G cases (pair_destruct_right ?????? G) %
1292qed.
1293
1294(* To be moved in ProofStatus *)
1295lemma program_counter_set_program_counter:
1296  ∀T.
1297  ∀cm.
1298  ∀s.
1299  ∀x.
1300    program_counter T cm (set_program_counter T cm s x) = x.
1301  //
1302qed.
Note: See TracBrowser for help on using the repository browser.