source: src/ASM/AssemblyProof.ma @ 2209

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

Closed major daemons in the supporting lemmas of the main lemma.

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