source: src/ASM/AssemblyProof.ma @ 2143

Last change on this file since 2143 was 2143, checked in by mulligan, 8 years ago

Changes to the subaddressing mode elim functions moved into their correct place in ASM.ma. ticks_of0 completed, with all daemons removed. Another commutation lemma added in AssemblyProofSplit?.ma.

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