source: src/ASM/AssemblyProof.ma @ 2147

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

Theorem closed (up to one more lemma on overflow), but new proof obligation
for the assembly function.

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