source: src/ASM/AssemblyProof.ma @ 2151

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