source: src/ASM/AssemblyProof.ma @ 2129

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

Large changes from today trying to complete the main theorem. Again :(

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