source: src/ASM/AssemblyProof.ma @ 2149

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

Code shuffling to proper places.

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