source: src/ASM/AssemblyProof.ma @ 2195

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

Got AssemblyProof?.ma compiling again using daemons.

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