source: src/ASM/AssemblyProof.ma @ 2132

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

Two more daemons closed, one left.

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