source: src/ASM/AssemblyProof.ma @ 2128

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

Final shuffling around

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