source: src/ASM/AssemblyProof.ma @ 2148

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