source: src/ASM/AssemblyProof.ma @ 2142

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

Down to one daemon that requires one lemma (monotonicity of sigma).

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