source: src/ASM/AssemblyProof.ma @ 2146

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