source: src/ASM/AssemblyProof.ma @ 2194

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