source: src/ASM/AssemblyProof.ma @ 2247

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

Work on the MOV instruction from today and bug fixes in set_arg_1.

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