source: src/ASM/AssemblyProof.ma @ 2144

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