source: src/ASM/AssemblyProof.ma @ 2124

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

Much more shuffling around to proper places

File size: 39.1 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3include "ASM/StatusProofs.ma".
4include alias "arithmetics/nat.ma".
5
6lemma is_in_monotonic_wrt_append:
7  ∀m, n: nat.
8  ∀p: Vector addressing_mode_tag m.
9  ∀q: Vector addressing_mode_tag n.
10  ∀to_search: addressing_mode.
11    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
12  #m #n #p #q #to_search #assm
13  elim q try assumption
14  #n' #hd #tl #inductive_hypothesis
15  normalize
16  cases (is_a ??) try @I
17  >inductive_hypothesis @I
18qed.
19
20corollary is_in_hd_tl:
21  ∀to_search: addressing_mode.
22  ∀hd: addressing_mode_tag.
23  ∀n: nat.
24  ∀v: Vector addressing_mode_tag n.
25    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
26  #to_search #hd #n #v
27  elim v
28  [1:
29    #absurd
30    normalize in absurd; cases absurd
31  |2:
32    #n' #hd' #tl #inductive_hypothesis #assm
33    >vector_cons_append >(vector_cons_append … hd' tl)
34    @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search)
35    assumption
36  ]
37qed.
38
39let rec encoding_check
40  (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
41    (encoding: list Byte)
42      on encoding: Prop ≝
43  match encoding with
44  [ nil ⇒ final_pc = pc
45  | cons hd tl ⇒
46    let 〈new_pc, byte〉 ≝ next code_memory pc in
47      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
48  ].
49
50lemma encoding_check_append:
51  ∀code_memory: BitVectorTrie Byte 16.
52  ∀final_pc: Word.
53  ∀l1: list Byte.
54  ∀pc: Word.
55  ∀l2: list Byte.
56    encoding_check code_memory pc final_pc (l1@l2) →
57      let pc_plus_len ≝ add … pc (bitvector_of_nat … (length … l1)) in
58        encoding_check code_memory pc pc_plus_len l1 ∧
59          encoding_check code_memory pc_plus_len final_pc l2.
60  #code_memory #final_pc #l1 elim l1
61  [1:
62    #pc #l2
63    whd in ⊢ (????% → ?); #H
64    <add_zero
65    whd whd in ⊢ (?%?); /2/
66  |2:
67    #hd #tl #IH #pc #l2 * #H1 #H2
68(*    >add_SO in H2; #H2 *)
69    cases (IH … H2) #E1 #E2 %
70    [1:
71      % try @H1
72      <(add_bitvector_of_nat_Sm 16 (|tl|)) in E1;
73      <add_associative #assm assumption
74    |2:
75      <add_associative in E2;
76      <(add_bitvector_of_nat_Sm 16 (|tl|)) #assm
77      assumption
78    ]
79  ]
80qed.
81
82definition ticks_of_instruction ≝
83  λi.
84    let trivial_code_memory ≝ assembly1 i in
85    let trivial_status ≝ load_code_memory trivial_code_memory in
86      \snd (fetch trivial_status (zero ?)).
87
88lemma fetch_assembly:
89  ∀pc: Word.
90  ∀i: instruction.
91  ∀code_memory: BitVectorTrie Byte 16.
92  ∀assembled: list Byte.
93    assembled = assembly1 i →
94      let len ≝ length … assembled in
95      let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
96        encoding_check code_memory pc pc_plus_len assembled →
97          let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in
98           (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true.
99  #pc #i #code_memory #assembled cases i [8: *]
100 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
101 [47,48,49:
102 |*: #arg @(subaddressing_mode_elim … arg)
103  [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,
104   59,60,63,64,65,66,67: #ARG]]
105 [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,
106  56,57,69,70,72: #arg2 @(subaddressing_mode_elim … arg2)
107  [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,
108   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,
109   68,69,70,71: #ARG2]]
110 [1,2,19,20: #arg3 @(subaddressing_mode_elim … arg3) #ARG3]
111 normalize in ⊢ (???% → ?);
112 [92,94,42,93,95: @vsplit_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
113  normalize in ⊢ (???% → ?);]
114 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
115 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
116 whd in match fetch; normalize nodelta <H1 whd in ⊢ (match % with [ _ ⇒ ? ]);
117 [17,18,19,20,21,22,23,24,25,26,32,34,35,36,37,39: <H3]
118 try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl
119qed.
120
121let rec fetch_many
122  (code_memory: BitVectorTrie Byte 16) (final_pc: Word) (pc: Word)
123    (expected: list instruction)
124      on expected: Prop ≝
125  match expected with
126  [ nil ⇒ eq_bv … pc final_pc = true
127  | cons i tl ⇒
128    let pc' ≝ add 16 pc (bitvector_of_nat 16 (|assembly1 … i|)) in
129      (〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
130        fetch_many code_memory final_pc pc' tl)
131  ].
132         
133lemma fetch_assembly_pseudo':
134  ∀lookup_labels.
135  ∀sigma: Word → Word.
136  ∀policy: Word → bool.
137  ∀ppc.
138  ∀lookup_datalabels.
139  ∀pi.
140  ∀code_memory.
141  ∀len.
142  ∀assembled.
143  ∀instructions.
144    let pc ≝ sigma ppc in
145      instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi →
146        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi →
147          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
148            encoding_check code_memory pc pc_plus_len assembled →
149              fetch_many code_memory pc_plus_len pc instructions.
150  #lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
151  normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
152  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
153  >len_refl >assembled_refl -len_refl
154  generalize in match (add 16 (sigma ppc)
155    (bitvector_of_nat 16
156     (|flatten (Vector bool 8)
157       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
158  #final_pc
159  generalize in match (sigma ppc); elim instructions
160  [1:
161    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
162  |2:
163    #i #tl #IH #pc #H whd
164    cases (encoding_check_append ????? H) -H #H1 #H2
165    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);   
166    cases (fetch ??) * #instr #pc' #ticks
167    #H3 lapply (H3 H1) -H3 normalize nodelta #H3
168    lapply (conjunction_true ?? H3) * #H4 #H5
169    lapply (conjunction_true … H4) * #B1 #B2
170    >(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) %
171    >(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2
172  ]
173qed.
174
175lemma fetch_assembly_pseudo:
176  ∀program: pseudo_assembly_program.
177  ∀sigma: Word → Word.
178  ∀policy: Word → bool.
179  let lookup_labels ≝ λx:Identifier. address_of_word_labels_code_mem (\snd  program) x in
180  ∀ppc.∀ppc_ok.
181  ∀code_memory.
182  let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
183  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
184  let pc ≝ sigma ppc in
185  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
186  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
187  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
188    encoding_check code_memory pc pc_plus_len assembled →
189      fetch_many code_memory pc_plus_len pc instructions.
190  #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory
191  letin lookup_datalabels ≝ (λx.?)
192  letin pi ≝ (fst ???)
193  letin pc ≝ (sigma ?)
194  letin instructions ≝ (expand_pseudo_instruction ??????)
195  @pair_elim #len #assembled #assembled_refl normalize nodelta
196  #H
197  generalize in match
198   (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
199  #X destruct normalize nodelta @X try % <assembled_refl try % assumption
200qed.
201
202definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
203  λpseudo_instruction.
204    match pseudo_instruction with
205    [ Comment c ⇒ False
206    | Cost c ⇒ False
207    | _ ⇒ True
208    ].
209
210(* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *)     
211lemma assembly_ok:
212  ∀program.
213  ∀length_proof: |\snd program| ≤ 2^16.
214  ∀sigma: Word → Word.
215  ∀policy: Word → bool.
216  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
217  ∀assembled.
218  ∀costs': BitVectorTrie costlabel 16.
219  let 〈preamble, instr_list〉 ≝ program in
220  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
221  let datalabels ≝ construct_datalabels preamble in
222  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
223    〈assembled,costs'〉 = assembly program sigma policy →
224      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
225        let code_memory ≝ load_code_memory assembled in
226        let lookup_labels ≝ λx. address_of_word_labels_code_mem instr_list x in 
227          ∀ppc.∀ppc_ok.
228            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
229            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
230            let pc ≝ sigma ppc in
231            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
232              encoding_check code_memory pc pc_plus_len assembled ∧
233                  sigma newppc = add … pc (bitvector_of_nat … len).
234  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
235  cases (assembly program sigma policy) * #assembled' #costs''
236  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
237  cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
238  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
239  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
240  * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
241  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
242  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
243  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
244  >eq_fetch_pseudo_instruction
245  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
246  > (?:((λx.bitvector_of_nat ? (lookup_def … labels x 0)) =
247       (λx.address_of_word_labels_code_mem instr_list x)))
248  [2: lapply (create_label_cost_map_ok 〈preamble,instr_list〉) >create_label_cost_refl
249      #H (*CSC: REQUIRES FUNCTIONAL EXTENSIONALITY; REPHRASE THE LEMMA *) cases daemon ]
250  >eq_assembly_1_pseudoinstruction
251  whd in ⊢ (% → ?); #assembly_ok
252  %
253  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
254      >snd_fetch_pseudo_instruction
255      cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
256      #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f
257      >eq_fetch_pseudo_instruction whd in match instruction_size;
258      normalize nodelta (*CSC: TRUE, NEEDS LEMMA AND FUNCTIONAL EXTENSIONALITY *)
259      cases daemon
260  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
261    #load_code_memory_ok
262    cut (len=|assembled|)
263    [1: (*CSC: provable before cleaning *)
264        cases daemon
265    ]
266    #EQlen
267    (* Nice statement here *)
268    cut (∀j. ∀H: j < |assembled|.
269          nth_safe Byte j assembled H =
270          \snd (next (load_code_memory assembled')
271          (bitvector_of_nat 16
272           (nat_of_bitvector …
273            (add … (sigma ppc) (bitvector_of_nat … j))))))
274    [1:
275      cases daemon
276    |2:
277      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
278      elim assembled
279      [1:
280        #pc #_ whd <add_zero %
281      | #hd #tl #IH #pc #H %
282         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
283           >H -H whd in ⊢ (??%?); <add_zero //
284         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
285           [2: <add_bitvector_of_nat_Sm @add_associative ]
286           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
287           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
288           >add_associative % ]]
289  ]]
290qed.
291
292(* XXX: should we add that costs = costs'? *)
293lemma fetch_assembly_pseudo2:
294  ∀program.
295  ∀length_proof: |\snd program| ≤ 2^16.
296  ∀sigma.
297  ∀policy.
298  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
299  ∀ppc.∀ppc_ok.
300  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
301  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
302  let code_memory ≝ load_code_memory assembled in
303  let data_labels ≝ construct_datalabels (\fst program) in
304  let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in 
305  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
306  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
307  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
308    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
309  * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
310  @pair_elim #labels #costs #create_label_map_refl
311  @pair_elim #assembled #costs' #assembled_refl
312  letin code_memory ≝ (load_code_memory ?)
313  letin data_labels ≝ (construct_datalabels ?)
314  letin lookup_labels ≝ (λx. ?)
315  letin lookup_datalabels ≝ (λx. ?)
316  @pair_elim #pi #newppc #fetch_pseudo_refl
317  lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
318  normalize nodelta try assumption
319  @pair_elim #labels' #costs' #create_label_map_refl' #H
320  lapply (H (sym_eq … assembled_refl)) -H
321  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
322  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
323  #len #assembledi #EQ4 #H
324  lapply (H ppc) >fetch_pseudo_refl #H
325  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc ppc_ok (load_code_memory assembled))
326  >EQ4 #H1 cases (H ppc_ok)
327  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
328  >fetch_pseudo_refl in H1; #assm @assm assumption
329qed.
330
331(* XXX: changed this type.  Bool specifies whether byte is first or second
332        component of an address, and the Word is the pseudoaddress that it
333        corresponds to.  Second component is the same principle for the accumulator
334        A.
335*)
336definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).
337
338include alias "ASM/BitVectorTrie.ma".
339 
340include "common/AssocList.ma".
341
342axiom low_internal_ram_of_pseudo_low_internal_ram:
343 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
344
345axiom high_internal_ram_of_pseudo_high_internal_ram:
346 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
347
348axiom low_internal_ram_of_pseudo_internal_ram_hit:
349 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7.
350  assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉)  →
351   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
352   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
353   let bl ≝ lookup ? 7 addr ram (zero 8) in
354   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
355   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
356     if high then
357       (pbl = higher) ∧ (bl = phigher)
358     else
359       (pbl = lower) ∧ (bl = plower).
360
361(* changed from add to sub *)
362axiom low_internal_ram_of_pseudo_internal_ram_miss:
363 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
364  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
365    assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →
366      lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
367
368definition addressing_mode_ok ≝
369 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
370  λaddr:addressing_mode.
371   match addr with
372    [ DIRECT d ⇒
373       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
374       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
375    | INDIRECT i ⇒
376       let d ≝ get_register … s [[false;false;i]] in
377       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
378       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
379    | EXT_INDIRECT _ ⇒ true
380    | REGISTER _ ⇒ true
381    | ACC_A ⇒ match \snd M with [ None ⇒ true | _ ⇒ false ]
382    | ACC_B ⇒ true
383    | DPTR ⇒ true
384    | DATA _ ⇒ true
385    | DATA16 _ ⇒ true
386    | ACC_DPTR ⇒ true
387    | ACC_PC ⇒ true
388    | EXT_INDIRECT_DPTR ⇒ true
389    | INDIRECT_DPTR ⇒ true
390    | CARRY ⇒ true
391    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
392    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
393    | RELATIVE _ ⇒ true
394    | ADDR11 _ ⇒ true
395    | ADDR16 _ ⇒ true ].
396   
397definition next_internal_pseudo_address_map0 ≝
398  λT.
399  λcm:T.
400  λaddr_of: Identifier → PreStatus T cm → Word.
401  λfetched.
402  λM: internal_pseudo_address_map.
403  λs: PreStatus T cm.
404   match fetched with
405    [ Comment _ ⇒ Some ? M
406    | Cost _ ⇒ Some … M
407    | Jmp _ ⇒ Some … M
408    | Call a ⇒
409      let a' ≝ addr_of a s in
410      let 〈callM, accM〉 ≝ M in
411         Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉::
412                 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉
413    | Mov _ _ ⇒ Some … M
414    | Instruction instr ⇒
415       match instr with
416        [ ADD addr1 addr2 ⇒
417           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
418            Some ? M
419           else
420            None ?
421        | ADDC addr1 addr2 ⇒
422           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
423            Some ? M
424           else
425            None ?
426        | SUBB addr1 addr2 ⇒
427           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
428            Some ? M
429           else
430            None ?       
431        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
432
433definition next_internal_pseudo_address_map ≝
434 λM:internal_pseudo_address_map.
435 λcm.
436 λaddr_of.
437 λs:PseudoStatus cm.
438 λppc_ok.
439    next_internal_pseudo_address_map0 ? cm addr_of
440     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
441
442definition code_memory_of_pseudo_assembly_program:
443    ∀pap:pseudo_assembly_program.
444      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
445  λpap.
446  λsigma.
447  λpolicy.
448    let p ≝ pi1 … (assembly pap sigma policy) in
449      load_code_memory (\fst p).
450
451definition sfr_8051_of_pseudo_sfr_8051 ≝
452  λM: internal_pseudo_address_map.
453  λsfrs: Vector Byte 19.
454  λsigma: Word → Word.
455    match \snd M with
456    [ None ⇒ sfrs
457    | Some s ⇒
458      let 〈high, address〉 ≝ s in
459      let index ≝ sfr_8051_index SFR_ACC_A in
460      let 〈upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in
461        if high then
462          set_index Byte 19 sfrs index upper ?
463        else
464          set_index Byte 19 sfrs index lower ?
465    ].
466  //
467qed.
468
469definition status_of_pseudo_status:
470    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
471      ∀sigma: Word → Word. ∀policy: Word → bool.
472        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
473  λM.
474  λpap.
475  λps.
476  λsigma.
477  λpolicy.
478  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
479  let pc ≝ sigma (program_counter … ps) in
480  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
481  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
482     mk_PreStatus (BitVectorTrie Byte 16)
483      cm
484      lir
485      hir
486      (external_ram … ps)
487      pc
488      (special_function_registers_8051 … ps)
489      (special_function_registers_8052 … ps)
490      (p1_latch … ps)
491      (p3_latch … ps)
492      (clock … ps).
493
494(*
495definition write_at_stack_pointer':
496 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
497  λM: Type[0].
498  λs: PreStatus M.
499  λv: Byte.
500    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
501    let bit_zero ≝ get_index_v… nu O ? in
502    let bit_1 ≝ get_index_v… nu 1 ? in
503    let bit_2 ≝ get_index_v… nu 2 ? in
504    let bit_3 ≝ get_index_v… nu 3 ? in
505      if bit_zero then
506        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
507                              v (low_internal_ram ? s) in
508          set_low_internal_ram ? s memory
509      else
510        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
511                              v (high_internal_ram ? s) in
512          set_high_internal_ram ? s memory.
513  [ cases l0 %
514  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
515qed.
516
517definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
518 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
519
520  λticks_of.
521  λs.
522  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
523  let ticks ≝ ticks_of (program_counter ? s) in
524  let s ≝ set_clock ? s (clock ? s + ticks) in
525  let s ≝ set_program_counter ? s pc in
526    match instr with
527    [ Instruction instr ⇒
528       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
529    | Comment cmt ⇒ s
530    | Cost cst ⇒ s
531    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
532    | Call call ⇒
533      let a ≝ address_of_word_labels s call in
534      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
535      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
536      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
537      let s ≝ write_at_stack_pointer' ? s pc_bl in
538      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
539      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
540      let s ≝ write_at_stack_pointer' ? s pc_bu in
541        set_program_counter ? s a
542    | Mov dptr ident ⇒
543       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
544    ].
545 [
546 |2,3,4: %
547 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
548 |
549 | %
550 ]
551 cases not_implemented
552qed.
553*)
554
555(*
556lemma execute_code_memory_unchanged:
557 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
558 #ticks #ps whd in ⊢ (??? (??%))
559 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
560  (program_counter pseudo_assembly_program ps)) #instr #pc
561 whd in ⊢ (??? (??%)) cases instr
562  [ #pre cases pre
563     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
564       cases (vsplit ????) #z1 #z2 %
565     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
566       cases (vsplit ????) #z1 #z2 %
567     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
568       cases (vsplit ????) #z1 #z2 %
569     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
570       [ #x1 whd in ⊢ (??? (??%))
571     | *: cases not_implemented
572     ]
573  | #comment %
574  | #cost %
575  | #label %
576  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
577    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
578    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
579    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
580    (* CSC: ??? *)
581  | #dptr #label (* CSC: ??? *)
582  ]
583  cases not_implemented
584qed.
585*)
586
587(* DEAD CODE?
588lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
589 ∀M:internal_pseudo_address_map.
590 ∀ps,ps': PseudoStatus.
591 ∀pol.
592  ∀prf:code_memory … ps = code_memory … ps'.
593   let pol' ≝ ? in
594   match status_of_pseudo_status M ps pol with
595    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
596    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
597    ].
598 [2: <prf @pol]
599 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
600 generalize in match (refl … (assembly (code_memory … ps) pol))
601 cases (assembly ??) in ⊢ (???% → %)
602  [ #K whd whd in ⊢ (??%?) <H >K %
603  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
604qed.
605*)
606
607definition ticks_of0:
608    ∀p:pseudo_assembly_program.
609      (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
610  λprogram: pseudo_assembly_program.
611  λsigma.
612  λpolicy.
613  λppc: Word.
614  λfetched.
615    match fetched with
616    [ Instruction instr ⇒
617      match instr with
618      [ JC lbl ⇒ ? (*
619        match pol lookup_labels ppc with
620        [ short_jump ⇒ 〈2, 2〉
621        | absolute_jump ⇒ ?
622        | long_jump ⇒ 〈4, 4〉
623        ] *)
624      | JNC lbl ⇒ ? (*
625        match pol lookup_labels ppc with
626        [ short_jump ⇒ 〈2, 2〉
627        | absolute_jump ⇒ ?
628        | long_jump ⇒ 〈4, 4〉
629        ] *)
630      | JB bit lbl ⇒ ? (*
631        match pol lookup_labels ppc with
632        [ short_jump ⇒ 〈2, 2〉
633        | absolute_jump ⇒ ?
634        | long_jump ⇒ 〈4, 4〉
635        ] *)
636      | JNB bit lbl ⇒ ? (*
637        match pol lookup_labels ppc with
638        [ short_jump ⇒ 〈2, 2〉
639        | absolute_jump ⇒ ?
640        | long_jump ⇒ 〈4, 4〉
641        ] *)
642      | JBC bit lbl ⇒ ? (*
643        match pol lookup_labels ppc with
644        [ short_jump ⇒ 〈2, 2〉
645        | absolute_jump ⇒ ?
646        | long_jump ⇒ 〈4, 4〉
647        ] *)
648      | JZ lbl ⇒ ? (*
649        match pol lookup_labels ppc with
650        [ short_jump ⇒ 〈2, 2〉
651        | absolute_jump ⇒ ?
652        | long_jump ⇒ 〈4, 4〉
653        ] *)
654      | JNZ lbl ⇒ ? (*
655        match pol lookup_labels  ppc with
656        [ short_jump ⇒ 〈2, 2〉
657        | absolute_jump ⇒ ?
658        | long_jump ⇒ 〈4, 4〉
659        ] *)
660      | CJNE arg lbl ⇒ ? (*
661        match pol lookup_labels ppc with
662        [ short_jump ⇒ 〈2, 2〉
663        | absolute_jump ⇒ ?
664        | long_jump ⇒ 〈4, 4〉
665        ] *)
666      | DJNZ arg lbl ⇒ ? (*
667        match pol lookup_labels ppc with
668        [ short_jump ⇒ 〈2, 2〉
669        | absolute_jump ⇒ ?
670        | long_jump ⇒ 〈4, 4〉
671        ] *)
672      | ADD arg1 arg2 ⇒
673        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
674         〈ticks, ticks〉
675      | ADDC arg1 arg2 ⇒
676        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
677         〈ticks, ticks〉
678      | SUBB arg1 arg2 ⇒
679        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
680         〈ticks, ticks〉
681      | INC arg ⇒
682        let ticks ≝ ticks_of_instruction (INC ? arg) in
683         〈ticks, ticks〉
684      | DEC arg ⇒
685        let ticks ≝ ticks_of_instruction (DEC ? arg) in
686         〈ticks, ticks〉
687      | MUL arg1 arg2 ⇒
688        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
689         〈ticks, ticks〉
690      | DIV arg1 arg2 ⇒
691        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
692         〈ticks, ticks〉
693      | DA arg ⇒
694        let ticks ≝ ticks_of_instruction (DA ? arg) in
695         〈ticks, ticks〉
696      | ANL arg ⇒
697        let ticks ≝ ticks_of_instruction (ANL ? arg) in
698         〈ticks, ticks〉
699      | ORL arg ⇒
700        let ticks ≝ ticks_of_instruction (ORL ? arg) in
701         〈ticks, ticks〉
702      | XRL arg ⇒
703        let ticks ≝ ticks_of_instruction (XRL ? arg) in
704         〈ticks, ticks〉
705      | CLR arg ⇒
706        let ticks ≝ ticks_of_instruction (CLR ? arg) in
707         〈ticks, ticks〉
708      | CPL arg ⇒
709        let ticks ≝ ticks_of_instruction (CPL ? arg) in
710         〈ticks, ticks〉
711      | RL arg ⇒
712        let ticks ≝ ticks_of_instruction (RL ? arg) in
713         〈ticks, ticks〉
714      | RLC arg ⇒
715        let ticks ≝ ticks_of_instruction (RLC ? arg) in
716         〈ticks, ticks〉
717      | RR arg ⇒
718        let ticks ≝ ticks_of_instruction (RR ? arg) in
719         〈ticks, ticks〉
720      | RRC arg ⇒
721        let ticks ≝ ticks_of_instruction (RRC ? arg) in
722         〈ticks, ticks〉
723      | SWAP arg ⇒
724        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
725         〈ticks, ticks〉
726      | MOV arg ⇒
727        let ticks ≝ ticks_of_instruction (MOV ? arg) in
728         〈ticks, ticks〉
729      | MOVX arg ⇒
730        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
731         〈ticks, ticks〉
732      | SETB arg ⇒
733        let ticks ≝ ticks_of_instruction (SETB ? arg) in
734         〈ticks, ticks〉
735      | PUSH arg ⇒
736        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
737         〈ticks, ticks〉
738      | POP arg ⇒
739        let ticks ≝ ticks_of_instruction (POP ? arg) in
740         〈ticks, ticks〉
741      | XCH arg1 arg2 ⇒
742        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
743         〈ticks, ticks〉
744      | XCHD arg1 arg2 ⇒
745        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
746         〈ticks, ticks〉
747      | RET ⇒
748        let ticks ≝ ticks_of_instruction (RET ?) in
749         〈ticks, ticks〉
750      | RETI ⇒
751        let ticks ≝ ticks_of_instruction (RETI ?) in
752         〈ticks, ticks〉
753      | NOP ⇒
754        let ticks ≝ ticks_of_instruction (NOP ?) in
755         〈ticks, ticks〉
756      ]
757    | Comment comment ⇒ 〈0, 0〉
758    | Cost cost ⇒ 〈0, 0〉
759    | Jmp jmp ⇒ 〈2, 2〉
760    | Call call ⇒ 〈2, 2〉
761    | Mov dptr tgt ⇒ 〈2, 2〉
762    ].
763    cases daemon
764qed.
765
766definition ticks_of:
767    ∀p:pseudo_assembly_program.
768      (Word → Word) → (Word → bool) → ∀ppc:Word.
769       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
770  λprogram: pseudo_assembly_program.
771  λsigma.
772  λpolicy.
773  λppc: Word. λppc_ok.
774    let pseudo ≝ \snd program in
775    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
776     ticks_of0 program sigma policy ppc fetched.
777
778(*
779lemma blah:
780  ∀m: internal_pseudo_address_map.
781  ∀s: PseudoStatus.
782  ∀arg: Byte.
783  ∀b: bool.
784    addressing_mode_ok m s (DIRECT arg) = true →
785      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
786      get_arg_8 ? s b (DIRECT arg).
787  [2, 3: normalize % ]
788  #m #s #arg #b #hyp
789  whd in ⊢ (??%%)
790  @vsplit_elim''
791  #nu' #nl' #arg_nu_nl_eq
792  normalize nodelta
793  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
794  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
795  #get_index_v_eq
796  normalize nodelta
797  [2:
798    normalize nodelta
799    @vsplit_elim''
800    #bit_one' #three_bits' #bit_one_three_bit_eq
801    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
802    normalize nodelta
803    generalize in match (refl ? (sub_7_with_carry ? ? ?))
804    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
805    #Saddr #carr' #Saddr_carr_eq
806    normalize nodelta
807    #carr_hyp'
808    @carr_hyp'
809    [1:
810    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
811        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
812        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
813        #member_eq
814        normalize nodelta
815        [2: #destr destruct(destr)
816        |1: -carr_hyp';
817            >arg_nu_nl_eq
818            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
819            [1: >get_index_v_eq in ⊢ (??%? → ?)
820            |2: @le_S @le_S @le_S @le_n
821            ]
822            cases (member (BitVector 8) ? (\fst ?) ?)
823            [1: #destr normalize in destr; destruct(destr)
824            |2:
825            ]
826        ]
827    |3: >get_index_v_eq in ⊢ (??%?)
828        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
829        >(vsplit_vector_singleton … bit_one_three_bit_eq)
830        <arg_nu_nl_eq
831        whd in hyp:(??%?)
832        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
833        normalize nodelta [*: #ignore @sym_eq ]
834    ]
835  |
836  ].
837*)
838(*
839map_address0 ... (DIRECT arg) = Some .. →
840  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
841  get_arg_8 (internal_ram ...) (DIRECT arg)
842
843((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
844                     then Some internal_pseudo_address_map M 
845                     else None internal_pseudo_address_map )
846                    =Some internal_pseudo_address_map M')
847
848axiom low_internal_ram_write_at_stack_pointer:
849 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
850 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
851  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
852  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
853  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
854  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
855  bu@@bl = sigma (pbu@@pbl) →
856   low_internal_ram T1 cm1
857     (write_at_stack_pointer …
858       (set_8051_sfr …
859         (write_at_stack_pointer …
860           (set_8051_sfr …
861             (set_low_internal_ram … s1
862               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
863             SFR_SP sp1)
864          bl)
865        SFR_SP sp2)
866      bu)
867   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
868      (low_internal_ram …
869       (write_at_stack_pointer …
870         (set_8051_sfr …
871           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
872          SFR_SP sp2)
873        pbu)).
874
875lemma high_internal_ram_write_at_stack_pointer:
876 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
877 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
878  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
879  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
880  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
881  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
882  bu@@bl = sigma (pbu@@pbl) →
883   high_internal_ram T1 cm1
884     (write_at_stack_pointer …
885       (set_8051_sfr …
886         (write_at_stack_pointer …
887           (set_8051_sfr …
888             (set_high_internal_ram … s1
889               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
890             SFR_SP sp1)
891          bl)
892        SFR_SP sp2)
893      bu)
894   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
895      (high_internal_ram …
896       (write_at_stack_pointer …
897         (set_8051_sfr …
898           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
899          SFR_SP sp2)
900        pbu)).
901  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
902  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
903  cases daemon (* XXX: !!! *)
904qed.
905*)
906
907(*CSC: ???*)
908(* XXX: we need a precondition here stating that the PPC is within the
909        bounds of the instruction list in order for Jaap's specification to
910        apply.
911*)
912lemma snd_assembly_1_pseudoinstruction_ok:
913  ∀program: pseudo_assembly_program.
914  ∀program_length_proof: |\snd program| ≤ 2^16.
915  ∀sigma: Word → Word.
916  ∀policy: Word → bool.
917  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
918  ∀ppc: Word.
919  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
920  ∀pi.
921  ∀lookup_labels.
922  ∀lookup_datalabels.
923    lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) →
924    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
925    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
926    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
927      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
928  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
929  #lookup_labels #lookup_datalabels
930  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
931  normalize nodelta
932  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
933  #fetch_pseudo_refl
934  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
935  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
936  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
937  @pair_elim #preamble #instr_list #program_refl
938  @pair_elim #labels #costs' #create_label_cost_map_refl
939  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
940  lapply (H ppc ppc_in_bounds) -H
941  @pair_elim #pi' #newppc #fetch_pseudo_refl'
942  @pair_elim #len #assembled #assembly1_refl #H
943  cases H
944  #encoding_check_assm #sigma_newppc_refl
945  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
946  >pi_refl' in assembly1_refl; #assembly1_refl
947  >lookup_labels_refl >lookup_datalabels_refl
948  >program_refl normalize nodelta
949  >assembly1_refl
950  <sigma_newppc_refl
951  generalize in match fetch_pseudo_refl';
952  whd in match (fetch_pseudo_instruction ???);
953  @pair_elim #lbl #instr #nth_refl normalize nodelta
954  #G cases (pair_destruct_right ?????? G) %
955qed.
956
957(* To be moved in ProofStatus *)
958lemma program_counter_set_program_counter:
959  ∀T.
960  ∀cm.
961  ∀s.
962  ∀x.
963    program_counter T cm (set_program_counter T cm s x) = x.
964  //
965qed.
966
967(* XXX: easy but tedious *)
968lemma assembly1_lt_128:
969  ∀i: instruction.
970    |(assembly1 i)| < 128.
971  #i cases i
972  try (#assm1 #assm2) try #assm1
973  [8:
974    cases assm1
975    try (#assm1 #assm2) try #assm1
976    whd in match assembly1; normalize nodelta
977    whd in match assembly_preinstruction; normalize nodelta
978    try @(subaddressing_mode_elim … assm2)
979    try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta
980    [32:
981      cases assm1 -assm1 #assm1 normalize nodelta
982      cases assm1 #addr1 #addr2 normalize nodelta
983      [1:
984        @(subaddressing_mode_elim … addr2)
985      |2:
986        @(subaddressing_mode_elim … addr1)
987      ]
988      #w
989    |35,36,37:
990      cases assm1 -assm1 #assm1 normalize nodelta
991      [1,3:
992        cases assm1 -assm1 #assm1 normalize nodelta
993      ]
994      cases assm1 #addr1 #addr2 normalize nodelta
995      @(subaddressing_mode_elim … addr2) try #w
996    |49:
997      cases assm1 -assm1 #assm1 normalize nodelta
998      [1:
999        cases assm1 -assm1 #assm1 normalize nodelta
1000        [1:
1001          cases assm1 -assm1 #assm1 normalize nodelta
1002          [1:
1003            cases assm1 -assm1 #assm1 normalize nodelta
1004            [1:
1005              cases assm1 -assm1 #assm1 normalize nodelta
1006            ]
1007          ]
1008        ]
1009      ]
1010      cases assm1 #addr1 #addr2 normalize nodelta
1011      [1,3,4,5:
1012        @(subaddressing_mode_elim … addr2) try #w
1013      |*:
1014        @(subaddressing_mode_elim … addr1) try #w
1015        normalize nodelta
1016        [1,2:
1017          @(subaddressing_mode_elim … addr2) try #w
1018        ]
1019      ]
1020    |50:
1021      cases assm1 -assm1 #assm1 normalize nodelta
1022      cases assm1 #addr1 #addr2 normalize nodelta
1023      [1:
1024        @(subaddressing_mode_elim … addr2) try #w
1025      |2:
1026        @(subaddressing_mode_elim … addr1) try #w
1027      ]
1028    ]
1029    normalize repeat @le_S_S @le_O_n
1030  ]
1031  whd in match assembly1; normalize nodelta
1032  [6:
1033    normalize repeat @le_S_S @le_O_n
1034  |7:
1035    @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n
1036  |*:
1037    @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
1038  ]
1039qed.
Note: See TracBrowser for help on using the repository browser.