source: src/ASM/AssemblyProof.ma @ 2173

Last change on this file since 2173 was 2160, checked in by mulligan, 7 years ago

Added a new scratch file Test.ma for working on lemmas that are needed in the massive proof to avoid having to retypecheck everything. Lots of work from the last week on the AssemblyProofSplit?.ma file, as well as an attempt to use Russell-style types on set_arg_8.

File size: 53.4 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 monotone_sigma:
183 ∀program. |\snd program| ≤ 2^16 →
184 ∀sigma: Word → Word. ∀policy: Word → bool.
185  sigma_policy_specification program sigma policy →
186   ∀ppc1,ppc2.
187    nat_of_bitvector … ppc2 ≤ |\snd program| →
188    nat_of_bitvector … ppc1 ≤ nat_of_bitvector … ppc2 →
189     (nat_of_bitvector … (sigma ppc1) ≤ nat_of_bitvector … (sigma ppc2) ∨
190      sigma ppc2 = zero … ∧ nat_of_bitvector … ppc2 = |\snd program|).
191 #program #program_bounded #sigma #policy * #SIGMAOK1 #SIGMAOK2 #ppc1 #ppc2
192 #ppc2_ok #LE
193 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc1)
194 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc2) in ⊢ (?%(?%?));
195 lapply (le_n … (nat_of_bitvector … ppc2))
196 elim LE in ⊢ (?%? → %);
197 [ #_ % %
198 | #m #LE_ppc1_m #IH #BOUNDED
199   cases (IH ?)
200   [3: @(transitive_le … BOUNDED) %2 %
201   |2: * #_ #abs @⊥ <abs in ppc2_ok; #abs'
202       @(absurd ?? (not_le_Sn_n m))
203       @(transitive_le … BOUNDED abs') ]
204   -IH #IH
205   cut (m < |\snd program|) [ @(lt_to_le_to_lt … ppc2_ok) assumption ] #LT1
206   cut (m < 2^16) [ @(lt_to_le_to_lt … program_bounded) assumption ] #LT2
207   cases (SIGMAOK2 (bitvector_of_nat … m) ?) -SIGMAOK2
208   [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption ]
209   #H *
210   [ #LTsigma_m %1 @(transitive_le … IH) -IH
211     <add_bitvector_of_nat_Sm >add_commutative >H -H
212     >nat_of_bitvector_add
213     [ //
214     | >nat_of_bitvector_bitvector_of_nat_inverse try assumption lapply LTsigma_m
215       whd in match instruction_size; normalize nodelta
216       inversion (assembly_1_pseudoinstruction ??????) #len #assembled #EQ #X
217       @(transitive_le … X) @le_S_S //
218     ]
219   | * #EQ1 #EQ2 %2 %
220     [ <add_bitvector_of_nat_Sm >add_commutative >H
221       lapply (eq_f … (bitvector_of_nat 16) … EQ2)
222       <add_bitvector_of_nat_plus
223       >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero
224     | <(nat_of_bitvector_bitvector_of_nat_inverse 16 m) try assumption
225     ]]]
226qed.
227
228(* This is a non trivial consequence of fetch_assembly_pseudo +
229   load_code_memory_ok because of the finite amount of memory. In
230   particular the case when the compiled program exhausts the
231   code memory is very tricky. It also requires monotonicity of
232   sigma in the out-of-bounds region too. *)     
233lemma assembly_ok:
234  ∀program.
235  ∀length_proof: |\snd program| ≤ 2^16.
236  ∀sigma: Word → Word.
237  ∀policy: Word → bool.
238  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
239  ∀assembled.
240  ∀costs': BitVectorTrie costlabel 16.
241  let 〈preamble, instr_list〉 ≝ program in
242  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
243  let datalabels ≝ construct_datalabels preamble in
244  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
245    〈assembled,costs'〉 = assembly program sigma policy →
246      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
247        let code_memory ≝ load_code_memory assembled in
248        let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
249          ∀ppc.∀ppc_ok.
250            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
251            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
252            let pc ≝ sigma ppc in
253            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
254              encoding_check code_memory pc pc_plus_len assembled ∧
255                  sigma newppc = add … pc (bitvector_of_nat … len).
256  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
257  cases (assembly program sigma policy) * #assembled' #costs''
258  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
259  cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
260  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
261  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
262  * * #assembly_ok1 #assembly_ok3 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
263  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
264  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
265  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
266  >eq_fetch_pseudo_instruction
267  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ? ∧ ∀j.∀H:j<|assembledi|.?) → ?)
268  >eq_assembly_1_pseudoinstruction
269  whd in ⊢ (% → ?); * #assembly_ok4 #assembly_ok
270  %
271  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
272      >snd_fetch_pseudo_instruction
273      cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
274      #spw1 #_ >spw1 -spw1 @eq_f @eq_f
275      >eq_fetch_pseudo_instruction whd in match instruction_size;
276      normalize nodelta >create_label_cost_refl
277      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
278      [>eq_assembly_1_pseudoinstruction % | skip]
279  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
280    #load_code_memory_ok
281    lapply (fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) #EQlen
282    (* Nice statement here *)
283    cut (∀j. ∀H: j < |assembled|.
284          nth_safe Byte j assembled H =
285          \snd (next (load_code_memory assembled')
286          (bitvector_of_nat 16
287           (nat_of_bitvector …
288            (add … (sigma ppc) (bitvector_of_nat … j))))))
289    [1: #j #H <load_code_memory_ok
290        [ @assembly_ok
291        | cut (0=|assembled'| → False)
292          [ #abs <abs in assembly_ok4; >EQlen #abs'
293            @(absurd ?? (not_le_Sn_O j)) @(transitive_le … H) assumption ] #NOT_EMPTY
294          cases assembly_ok3 -assembly_ok3
295          [2: * #_ #EQ2 >EQ2 @lt_nat_of_bitvector ]
296          #EQlen_assembled' <EQlen_assembled'
297          cases sigma_policy_witness #sigma_zero >EQprogram #sigma_ok
298          cases (sigma_ok … ppc_ok) -sigma_ok >eq_fetch_pseudo_instruction
299          whd in match instruction_size; normalize nodelta
300          >create_label_cost_refl
301          >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
302          [>eq_assembly_1_pseudoinstruction |2: skip] #OK >OK <EQlen *
303          [2: * #EQ1 #EQ2 @⊥ <EQ1 in EQlen_assembled';
304              <add_bitvector_of_nat_Sm >add_commutative
305              >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2
306              lapply (eq_f … (bitvector_of_nat 16) … EQ2) -EQ2
307              <add_bitvector_of_nat_plus >bitvector_of_nat_inverse_nat_of_bitvector
308              #X >X #Y @NOT_EMPTY <Y >bitvector_of_nat_exp_zero % ]
309          cases (le_to_or_lt_eq … instr_list_ok)
310          [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero
311              assumption ]
312          #instr_list_ok' #NO_OVERFLOW
313          @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|)))))
314          [ @lt_to_lt_nat_of_bitvector_add
315            [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction)
316              / by /
317            | <EQlen assumption
318            | assumption
319            ]
320          | <EQlen <OK
321            cases (monotone_sigma ???? sigma_policy_witness
322             (add … ppc (bitvector_of_nat … 1))
323             (bitvector_of_nat … (|instr_list|)) ??) try assumption
324            [ #H @H
325            |3: >EQprogram >nat_of_bitvector_bitvector_of_nat_inverse
326                try % assumption
327            |4: >nat_of_bitvector_bitvector_of_nat_inverse try assumption
328                >nat_of_bitvector_add <plus_n_Sm <plus_n_O try assumption
329                @(transitive_le … instr_list_ok') @le_S_S assumption
330            | * #EQ1 @⊥ >EQ1 in EQlen_assembled'; assumption ]]]
331    |2:
332      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
333      elim assembled
334      [1:
335        #pc #_ whd <add_zero %
336      | #hd #tl #IH #pc #H %
337         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
338           >H -H whd in ⊢ (??%?); <add_zero //
339         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
340           [2: <add_bitvector_of_nat_Sm @add_associative ]
341           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
342           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
343           >add_associative % ]]]]
344qed.
345
346(* XXX: should we add that costs = costs'? *)
347lemma fetch_assembly_pseudo2:
348  ∀program.
349  ∀length_proof: |\snd program| ≤ 2^16.
350  ∀sigma.
351  ∀policy.
352  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
353  ∀ppc.∀ppc_ok.
354  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
355  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
356  let code_memory ≝ load_code_memory assembled in
357  let data_labels ≝ construct_datalabels (\fst program) in
358  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
359  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
360  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
361  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
362    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
363  * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
364  @pair_elim #labels #costs #create_label_map_refl
365  @pair_elim #assembled #costs' #assembled_refl
366  letin code_memory ≝ (load_code_memory ?)
367  letin data_labels ≝ (construct_datalabels ?)
368  letin lookup_labels ≝ (λx. ?)
369  letin lookup_datalabels ≝ (λx. ?)
370  @pair_elim #pi #newppc #fetch_pseudo_refl
371  lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
372  normalize nodelta try assumption
373  >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H
374  lapply (H (sym_eq … assembled_refl)) -H
375  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
376  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
377  #len #assembledi #EQ4 #H
378  lapply (H ppc) >fetch_pseudo_refl #H
379  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy)
380  >create_label_map_refl #X lapply (X ppc ppc_ok (load_code_memory assembled)) -X
381  >EQ4 #H1 cases (H ppc_ok)
382  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
383  >fetch_pseudo_refl in H1; #assm @assm assumption
384qed.
385
386inductive upper_lower: Type[0] ≝
387  | upper: upper_lower
388  | lower: upper_lower.
389
390definition eq_upper_lower:
391    upper_lower → upper_lower → bool ≝
392  λleft: upper_lower.
393  λright: upper_lower.
394  match left with
395  [ upper ⇒
396    match right with
397    [ upper ⇒ true
398    | _     ⇒ false
399    ]
400  | lower ⇒
401    match right with
402    [ lower ⇒ true
403    | _     ⇒ false
404    ]
405  ].
406
407lemma eq_upper_lower_true_to_eq:
408  ∀left: upper_lower.
409  ∀right: upper_lower.
410    eq_upper_lower left right = true → left = right.
411  * * normalize try (#_ %)
412  #absurd destruct(absurd)
413qed.
414
415lemma eq_upper_lower_false_to_neq:
416  ∀left: upper_lower.
417  ∀right: upper_lower.
418    eq_upper_lower left right = false → left ≠ right.
419  * * normalize try (#absurd destruct(absurd))
420  @nmk #absurd destruct(absurd)
421qed.
422
423inductive accumulator_address_map_entry: Type[0] ≝
424  | data: accumulator_address_map_entry
425  | address: upper_lower → Word → accumulator_address_map_entry.
426
427definition eq_accumulator_address_map_entry:
428    accumulator_address_map_entry → accumulator_address_map_entry → bool ≝
429  λleft: accumulator_address_map_entry.
430  λright: accumulator_address_map_entry.
431    match left with
432    [ data                     ⇒
433      match right with
434      [ data ⇒ true
435      | _    ⇒ false
436      ]
437    | address upper_lower word ⇒
438      match right with
439      [ address upper_lower' word' ⇒
440          eq_upper_lower upper_lower upper_lower' ∧ eq_bv … word word'
441      | _                          ⇒ false
442      ]
443    ].
444
445lemma eq_accumulator_address_map_entry_true_to_eq:
446  ∀left: accumulator_address_map_entry.
447  ∀right: accumulator_address_map_entry.
448    eq_accumulator_address_map_entry left right = true → left = right.
449  #left #right cases left cases right
450  [1:
451    #_ %
452  |2,3:
453    #upper_lower #word normalize #absurd destruct(absurd)
454  |4:
455    #upper_lower #word #upper_lower' #word' normalize
456    cases upper_lower' normalize nodelta
457    cases upper_lower normalize
458    [2,3:
459      #absurd destruct(absurd)
460    ]
461    change with (eq_bv 16 ?? = true → ?)
462    #relevant lapply (eq_bv_eq … relevant)
463    #word_refl >word_refl %
464  ]
465qed.
466
467lemma eq_bv_false_to_neq:
468  ∀n: nat.
469  ∀left, right: BitVector n.
470    eq_bv n left right = false → left ≠ right.
471  #n #left elim left
472  [1:
473    #right >(BitVector_O … right) normalize #absurd destruct(absurd)
474  |2:
475    #n' #hd #tl #inductive_hypothesis #right
476    cases (BitVector_Sn … right) #hd' * #tl' #right_refl
477    >right_refl normalize
478    cases hd normalize nodelta
479    cases hd' normalize nodelta
480    [2,3:
481      #_ @nmk #absurd destruct(absurd)
482    ]
483    change with (eq_bv ??? = false → ?)
484    #relevant lapply (inductive_hypothesis … relevant)
485    #tl_neq_assm @nmk #tl_eq_assm cases tl_neq_assm
486    #tl_eq_assm' @tl_eq_assm' destruct(tl_eq_assm) %
487  ]
488qed.
489   
490lemma eq_accumulator_address_map_entry_false_to_neq:
491  ∀left: accumulator_address_map_entry.
492  ∀right: accumulator_address_map_entry.
493    eq_accumulator_address_map_entry left right = false → left ≠ right.
494  #left #right cases left cases right
495  [1:
496    normalize #absurd destruct(absurd)
497  |2,3:
498    #upper_lower #word normalize #_
499    @nmk #absurd destruct(absurd)
500  |4:
501    #upper_lower #word #upper_lower' #word' normalize
502    cases upper_lower' normalize nodelta
503    cases upper_lower normalize nodelta
504    [2,3:
505      #_ @nmk #absurd destruct(absurd)
506    ]
507    change with (eq_bv ??? = false → ?)
508    #eq_bv_false_assm lapply(eq_bv_false_to_neq … eq_bv_false_assm)
509    #word_neq_assm @nmk #address_eq_assm cases word_neq_assm
510    #word_eq_assm @word_eq_assm destruct(address_eq_assm) %
511  ]
512qed.
513
514(* XXX: changed this type.  Bool specifies whether byte is first or second
515        component of an address, and the Word is the pseudoaddress that it
516        corresponds to.  Second component is the same principle for the accumulator
517        A.
518*)
519definition internal_pseudo_address_map ≝ list (Byte × (upper_lower × Word)) × accumulator_address_map_entry.
520
521include alias "ASM/BitVectorTrie.ma".
522 
523include "common/AssocList.ma".
524
525axiom low_internal_ram_of_pseudo_low_internal_ram:
526 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
527
528axiom high_internal_ram_of_pseudo_high_internal_ram:
529 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
530
531axiom low_internal_ram_of_pseudo_internal_ram_hit:
532 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.
533  assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉  →
534   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
535   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
536   let bl ≝ lookup ? 7 addr ram (zero 8) in
537   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
538   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
539     if eq_upper_lower upper_lower upper then
540       (pbl = higher) ∧ (bl = phigher)
541     else
542       (pbl = lower) ∧ (bl = plower).
543
544(* changed from add to sub *)
545axiom low_internal_ram_of_pseudo_internal_ram_miss:
546 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
547  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
548    assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →
549      lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
550
551definition addressing_mode_ok ≝
552 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
553  λaddr:addressing_mode.
554   match addr with
555    [ DIRECT d ⇒
556        if eq_bv … d (bitvector_of_nat … 224) then
557          ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) ∧ eq_accumulator_address_map_entry (\snd M) data
558        else
559         ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
560    | INDIRECT i ⇒
561       let d ≝ get_register … s [[false;false;i]] in
562       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M))
563    | EXT_INDIRECT _ ⇒ true
564    | REGISTER r ⇒
565        let address ≝ bit_address_of_register … s r in
566          ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M)
567    | ACC_A ⇒ match \snd M with [ data ⇒ true | _ ⇒ false ]
568    | ACC_B ⇒ true
569    | DPTR ⇒ true
570    | DATA _ ⇒ true
571    | DATA16 _ ⇒ true
572    | ACC_DPTR ⇒ true
573    | ACC_PC ⇒ true
574    | EXT_INDIRECT_DPTR ⇒ true
575    | INDIRECT_DPTR ⇒ true
576    | CARRY ⇒ true
577    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
578    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
579    | RELATIVE _ ⇒ true
580    | ADDR11 _ ⇒ true
581    | ADDR16 _ ⇒ true
582    ].
583   
584definition next_internal_pseudo_address_map0 ≝
585  λT.
586  λcm:T.
587  λaddr_of: Identifier → PreStatus T cm → Word.
588  λfetched.
589  λM: internal_pseudo_address_map.
590  λs: PreStatus T cm.
591   match fetched with
592    [ Comment _ ⇒ Some ? M
593    | Cost _ ⇒ Some … M
594    | Jmp _ ⇒ Some … M
595    | Call a ⇒
596      let a' ≝ addr_of a s in
597      let 〈callM, accM〉 ≝ M in
598         Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, a'〉〉::
599                 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈upper, a'〉〉::callM, accM〉
600    | Mov _ _ ⇒ Some … M
601    | Instruction instr ⇒
602      match instr return λx. option internal_pseudo_address_map with
603       [ ADD addr1 addr2 ⇒
604         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
605           Some ? M
606         else
607           None ?
608       | ADDC addr1 addr2 ⇒
609         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
610           Some ? M
611         else
612           None ?
613       | SUBB addr1 addr2 ⇒
614         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
615           Some ? M
616         else
617           None ?
618       | INC addr1 ⇒
619         if addressing_mode_ok T M ? s addr1 then
620           Some ? M
621         else
622           None ?
623       | DEC addr1 ⇒
624         if addressing_mode_ok T M … s addr1 then
625           Some ? M
626         else
627           None ?
628       | MUL addr1 addr2 ⇒
629         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
630           Some ? M
631         else
632           None ?
633       | DIV addr1 addr2 ⇒
634         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
635           Some ? M
636         else
637           None ?
638       | DA addr1 ⇒
639         if addressing_mode_ok T M … s addr1 then
640           Some ? M
641         else
642           None ?
643       | JC addr1 ⇒ Some ? M
644       | JNC addr1 ⇒ Some ? M
645       | JB addr1 addr2 ⇒ Some ? M
646       | JNB addr1 addr2 ⇒ Some ? M
647       | JBC addr1 addr2 ⇒ Some ? M
648       | JZ addr1 ⇒ Some ? M
649       | JNZ addr1 ⇒ Some ? M
650       | CJNE addr1 addr2 ⇒
651         match addr1 with
652         [ inl l ⇒
653           let 〈left, right〉 ≝ l in
654             if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then
655               Some ? M
656             else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then
657               Some ? M
658             else
659               None ?
660         | inr r ⇒
661           let 〈left, right〉 ≝ r in
662             if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then
663               Some ? M
664             else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then
665               Some ? M
666             else
667               None ?
668         ]
669       | DJNZ addr1 addr2 ⇒
670         if addressing_mode_ok T M … s addr1 then
671           Some ? M
672         else
673           None ?
674       | CLR addr1 ⇒
675         if addressing_mode_ok T M … s addr1 then
676           Some ? M
677         else
678           None ?
679       | CPL addr1 ⇒
680         if addressing_mode_ok T M … s addr1 then
681           Some ? M
682         else
683           None ?
684       | RL addr1 ⇒
685         if addressing_mode_ok T M … s addr1 then
686           Some ? M
687         else
688           None ?
689       | RLC addr1 ⇒
690         if addressing_mode_ok T M … s addr1 then
691           Some ? M
692         else
693           None ?
694       | RR addr1 ⇒
695         if addressing_mode_ok T M … s addr1 then
696           Some ? M
697         else
698           None ?
699       | RRC addr1 ⇒
700         if addressing_mode_ok T M … s addr1 then
701           Some ? M
702         else
703           None ?
704       | SWAP addr1 ⇒
705         if addressing_mode_ok T M … s addr1 then
706           Some ? M
707         else
708           None ?
709       | SETB addr1 ⇒
710         if addressing_mode_ok T M … s addr1 then
711           Some ? M
712         else
713           None ?
714       (* XXX: need to track addresses pushed and popped off the stack? *)
715       | PUSH addr1 ⇒
716         let 〈callM, accM〉 ≝ M in
717         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
718         [ DIRECT d ⇒ λproof.
719           let extended ≝ pad 8 8 d in
720             Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, extended〉〉::callM, accM〉
721         | _ ⇒ λother: False. ⊥
722         ] (subaddressing_modein … addr1)
723       | POP addr1 ⇒ Some … M
724       | XCH addr1 addr2 ⇒
725         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
726           Some ? M
727         else
728           None ?
729       | XCHD addr1 addr2 ⇒
730         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
731           Some ? M
732         else
733           None ?
734      | RET ⇒
735        let 〈callM, accM〉 ≝ M in
736        let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
737        let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
738          if sp_plus_1 ∧ sp_plus_2 then
739            Some … M
740          else
741            None ?
742      | RETI ⇒
743        let 〈callM, accM〉 ≝ M in
744        let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
745        let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
746          if sp_plus_1 ∧ sp_plus_2 then
747            Some … M
748          else
749            None ?
750      | NOP ⇒ Some … M
751      | MOVX addr1 ⇒ Some … M
752      | XRL addr1 ⇒
753        match addr1 with
754        [ inl l ⇒
755          let 〈acc_a, others〉 ≝ l in
756          let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
757          let others_ok ≝ addressing_mode_ok T M … s others in
758          if acc_a_ok ∧ others_ok then
759            Some ? M
760          else
761            None ?
762        | inr r ⇒
763          let 〈direct, others〉 ≝ r in
764          let direct_ok ≝ addressing_mode_ok T M … s direct in
765          let others_ok ≝ addressing_mode_ok T M … s others in
766          if direct_ok ∧ others_ok then
767            Some ? M
768          else
769            None ?
770        ]
771      | ORL addr1 ⇒
772        match addr1 with
773        [ inl l ⇒
774          match l with
775          [ inl l ⇒
776            let 〈acc_a, others〉 ≝ l in
777            let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
778            let others_ok ≝ addressing_mode_ok T M … s others in
779            if acc_a_ok ∧ others_ok then
780              Some ? M
781            else
782              None ?
783          | inr r ⇒
784            let 〈direct, others〉 ≝ r in
785            let direct_ok ≝ addressing_mode_ok T M … s direct in
786            let others_ok ≝ addressing_mode_ok T M … s others in
787            if direct_ok ∧ others_ok then
788              Some ? M
789            else
790              None ?
791          ]
792        | inr r ⇒
793          let 〈carry, others〉 ≝ r in
794          let carry_ok ≝ addressing_mode_ok T M … s carry in
795          let others_ok ≝ addressing_mode_ok T M … s others in
796          if carry_ok ∧ others_ok then
797            Some ? M
798          else
799            None ?
800        ]
801      | ANL addr1 ⇒
802        match addr1 with
803        [ inl l ⇒
804          match l with
805          [ inl l ⇒
806            let 〈acc_a, others〉 ≝ l in
807            let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
808            let others_ok ≝ addressing_mode_ok T M … s others in
809            if acc_a_ok ∧ others_ok then
810              Some ? M
811            else
812              None ?
813          | inr r ⇒
814            let 〈direct, others〉 ≝ r in
815            let direct_ok ≝ addressing_mode_ok T M … s direct in
816            let others_ok ≝ addressing_mode_ok T M … s others in
817            if direct_ok ∧ others_ok then
818              Some ? M
819            else
820              None ?
821          ]
822        | inr r ⇒
823          let 〈carry, others〉 ≝ r in
824          let carry_ok ≝ addressing_mode_ok T M … s carry in
825          let others_ok ≝ addressing_mode_ok T M … s others in
826          if carry_ok ∧ others_ok then
827            Some ? M
828          else
829            None ?
830        ]
831      | MOV addr1 ⇒ Some … M
832      ]
833    ].
834    cases other
835qed.
836
837definition next_internal_pseudo_address_map ≝
838 λM:internal_pseudo_address_map.
839 λcm.
840 λaddr_of.
841 λs:PseudoStatus cm.
842 λppc_ok.
843    next_internal_pseudo_address_map0 ? cm addr_of
844     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
845
846definition code_memory_of_pseudo_assembly_program:
847    ∀pap:pseudo_assembly_program.
848      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
849  λpap.
850  λsigma.
851  λpolicy.
852    let p ≝ pi1 … (assembly pap sigma policy) in
853      load_code_memory (\fst p).
854
855definition sfr_8051_of_pseudo_sfr_8051 ≝
856  λM: internal_pseudo_address_map.
857  λsfrs: Vector Byte 19.
858  λsigma: Word → Word.
859    match \snd M with
860    [ data ⇒ sfrs
861    | address upper_lower address ⇒
862      let index ≝ sfr_8051_index SFR_ACC_A in
863      let 〈high, low〉 ≝ vsplit ? 8 8 (sigma address) in
864        if eq_upper_lower upper_lower upper then
865          set_index Byte 19 sfrs index high ?
866        else
867          set_index Byte 19 sfrs index low ?
868    ].
869  //
870qed.
871
872definition status_of_pseudo_status:
873    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
874      ∀sigma: Word → Word. ∀policy: Word → bool.
875        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
876  λM.
877  λpap.
878  λps.
879  λsigma.
880  λpolicy.
881  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
882  let pc ≝ sigma (program_counter … ps) in
883  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
884  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
885     mk_PreStatus (BitVectorTrie Byte 16)
886      cm
887      lir
888      hir
889      (external_ram … ps)
890      pc
891      (sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma)
892      (special_function_registers_8052 … ps)
893      (p1_latch … ps)
894      (p3_latch … ps)
895      (clock … ps).
896
897(*
898definition write_at_stack_pointer':
899 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
900  λM: Type[0].
901  λs: PreStatus M.
902  λv: Byte.
903    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
904    let bit_zero ≝ get_index_v… nu O ? in
905    let bit_1 ≝ get_index_v… nu 1 ? in
906    let bit_2 ≝ get_index_v… nu 2 ? in
907    let bit_3 ≝ get_index_v… nu 3 ? in
908      if bit_zero then
909        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
910                              v (low_internal_ram ? s) in
911          set_low_internal_ram ? s memory
912      else
913        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
914                              v (high_internal_ram ? s) in
915          set_high_internal_ram ? s memory.
916  [ cases l0 %
917  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
918qed.
919
920definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
921 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
922
923  λticks_of.
924  λs.
925  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
926  let ticks ≝ ticks_of (program_counter ? s) in
927  let s ≝ set_clock ? s (clock ? s + ticks) in
928  let s ≝ set_program_counter ? s pc in
929    match instr with
930    [ Instruction instr ⇒
931       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
932    | Comment cmt ⇒ s
933    | Cost cst ⇒ s
934    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
935    | Call call ⇒
936      let a ≝ address_of_word_labels s call in
937      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
938      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
939      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
940      let s ≝ write_at_stack_pointer' ? s pc_bl in
941      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
942      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
943      let s ≝ write_at_stack_pointer' ? s pc_bu in
944        set_program_counter ? s a
945    | Mov dptr ident ⇒
946       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
947    ].
948 [
949 |2,3,4: %
950 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
951 |
952 | %
953 ]
954 cases not_implemented
955qed.
956*)
957
958(*
959lemma execute_code_memory_unchanged:
960 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
961 #ticks #ps whd in ⊢ (??? (??%))
962 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
963  (program_counter pseudo_assembly_program ps)) #instr #pc
964 whd in ⊢ (??? (??%)) cases instr
965  [ #pre cases pre
966     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
967       cases (vsplit ????) #z1 #z2 %
968     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
969       cases (vsplit ????) #z1 #z2 %
970     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
971       cases (vsplit ????) #z1 #z2 %
972     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
973       [ #x1 whd in ⊢ (??? (??%))
974     | *: cases not_implemented
975     ]
976  | #comment %
977  | #cost %
978  | #label %
979  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
980    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
981    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
982    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
983    (* CSC: ??? *)
984  | #dptr #label (* CSC: ??? *)
985  ]
986  cases not_implemented
987qed.
988*)
989
990(* XXX: check values returned for conditional jumps below! They are wrong,
991        find correct values *)
992definition ticks_of0:
993    ∀p:pseudo_assembly_program.
994      (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
995  λprogram: pseudo_assembly_program.
996  λlookup_labels: Identifier → Word.
997  λsigma.
998  λpolicy.
999  λppc: Word.
1000  λfetched.
1001    match fetched with
1002    [ Instruction instr ⇒
1003      match instr with
1004      [ JC lbl ⇒
1005        let lookup_address ≝ sigma (lookup_labels lbl) in
1006        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1007        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1008          if sj_possible then
1009            〈2, 2〉
1010          else
1011            〈4, 4〉
1012      | JNC lbl ⇒
1013        let lookup_address ≝ sigma (lookup_labels lbl) in
1014        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1015        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1016          if sj_possible then
1017            〈2, 2〉
1018          else
1019            〈4, 4〉
1020      | JB bit lbl ⇒
1021        let lookup_address ≝ sigma (lookup_labels lbl) in
1022        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1023        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1024          if sj_possible then
1025            〈2, 2〉
1026          else
1027            〈4, 4〉
1028      | JNB bit lbl ⇒
1029        let lookup_address ≝ sigma (lookup_labels lbl) in
1030        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1031        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1032          if sj_possible then
1033            〈2, 2〉
1034          else
1035            〈4, 4〉
1036      | JBC bit lbl ⇒
1037        let lookup_address ≝ sigma (lookup_labels lbl) in
1038        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1039        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1040          if sj_possible then
1041            〈2, 2〉
1042          else
1043            〈4, 4〉
1044      | JZ lbl ⇒
1045        let lookup_address ≝ sigma (lookup_labels lbl) in
1046        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1047        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1048          if sj_possible then
1049            〈2, 2〉
1050          else
1051            〈4, 4〉
1052      | JNZ lbl ⇒
1053        let lookup_address ≝ sigma (lookup_labels lbl) in
1054        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1055        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1056          if sj_possible then
1057            〈2, 2〉
1058          else
1059            〈4, 4〉
1060      | CJNE arg lbl ⇒
1061        let lookup_address ≝ sigma (lookup_labels lbl) in
1062        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1063        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1064          if sj_possible then
1065            〈2, 2〉
1066          else
1067            〈4, 4〉
1068      | DJNZ arg lbl ⇒
1069        let lookup_address ≝ sigma (lookup_labels lbl) in
1070        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1071        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1072          if sj_possible then
1073            〈2, 2〉
1074          else
1075            〈4, 4〉
1076      | ADD arg1 arg2 ⇒
1077        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1078         〈ticks, ticks〉
1079      | ADDC arg1 arg2 ⇒
1080        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1081         〈ticks, ticks〉
1082      | SUBB arg1 arg2 ⇒
1083        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1084         〈ticks, ticks〉
1085      | INC arg ⇒
1086        let ticks ≝ ticks_of_instruction (INC ? arg) in
1087         〈ticks, ticks〉
1088      | DEC arg ⇒
1089        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1090         〈ticks, ticks〉
1091      | MUL arg1 arg2 ⇒
1092        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1093         〈ticks, ticks〉
1094      | DIV arg1 arg2 ⇒
1095        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1096         〈ticks, ticks〉
1097      | DA arg ⇒
1098        let ticks ≝ ticks_of_instruction (DA ? arg) in
1099         〈ticks, ticks〉
1100      | ANL arg ⇒
1101        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1102         〈ticks, ticks〉
1103      | ORL arg ⇒
1104        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1105         〈ticks, ticks〉
1106      | XRL arg ⇒
1107        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1108         〈ticks, ticks〉
1109      | CLR arg ⇒
1110        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1111         〈ticks, ticks〉
1112      | CPL arg ⇒
1113        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1114         〈ticks, ticks〉
1115      | RL arg ⇒
1116        let ticks ≝ ticks_of_instruction (RL ? arg) in
1117         〈ticks, ticks〉
1118      | RLC arg ⇒
1119        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1120         〈ticks, ticks〉
1121      | RR arg ⇒
1122        let ticks ≝ ticks_of_instruction (RR ? arg) in
1123         〈ticks, ticks〉
1124      | RRC arg ⇒
1125        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1126         〈ticks, ticks〉
1127      | SWAP arg ⇒
1128        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1129         〈ticks, ticks〉
1130      | MOV arg ⇒
1131        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1132         〈ticks, ticks〉
1133      | MOVX arg ⇒
1134        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1135         〈ticks, ticks〉
1136      | SETB arg ⇒
1137        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1138         〈ticks, ticks〉
1139      | PUSH arg ⇒
1140        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1141         〈ticks, ticks〉
1142      | POP arg ⇒
1143        let ticks ≝ ticks_of_instruction (POP ? arg) in
1144         〈ticks, ticks〉
1145      | XCH arg1 arg2 ⇒
1146        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1147         〈ticks, ticks〉
1148      | XCHD arg1 arg2 ⇒
1149        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1150         〈ticks, ticks〉
1151      | RET ⇒
1152        let ticks ≝ ticks_of_instruction (RET ?) in
1153         〈ticks, ticks〉
1154      | RETI ⇒
1155        let ticks ≝ ticks_of_instruction (RETI ?) in
1156         〈ticks, ticks〉
1157      | NOP ⇒
1158        let ticks ≝ ticks_of_instruction (NOP ?) in
1159         〈ticks, ticks〉
1160      ]
1161    | Comment comment ⇒ 〈0, 0〉
1162    | Cost cost ⇒ 〈0, 0〉
1163    | Jmp jmp ⇒
1164      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1165      let do_a_long ≝ policy ppc in
1166      let lookup_address ≝ sigma (lookup_labels jmp) in
1167      let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
1168        if sj_possible ∧ ¬ do_a_long then
1169          〈2, 2〉 (* XXX: SJMP *)
1170        else
1171        let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1172          if mj_possible ∧ ¬ do_a_long then
1173            〈2, 2〉 (* XXX: AJMP *)
1174          else
1175            〈2, 2〉 (* XXX: LJMP *)
1176    | Call call ⇒
1177      (* XXX: collapse the branches as they are identical? *)
1178      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
1179      let lookup_address ≝ sigma (lookup_labels call) in
1180      let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
1181      let do_a_long ≝ policy ppc in
1182      if mj_possible ∧ ¬ do_a_long then
1183        〈2, 2〉 (* ACALL *)
1184      else
1185        〈2, 2〉 (* LCALL *)
1186    | Mov dptr tgt ⇒ 〈2, 2〉
1187    ].
1188
1189definition ticks_of:
1190    ∀p:pseudo_assembly_program.
1191      (Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word.
1192       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
1193  λprogram: pseudo_assembly_program.
1194  λlookup_labels.
1195  λsigma.
1196  λpolicy.
1197  λppc: Word. λppc_ok.
1198    let pseudo ≝ \snd program in
1199    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
1200     ticks_of0 program lookup_labels sigma policy ppc fetched.
1201
1202(*
1203lemma blah:
1204  ∀m: internal_pseudo_address_map.
1205  ∀s: PseudoStatus.
1206  ∀arg: Byte.
1207  ∀b: bool.
1208    addressing_mode_ok m s (DIRECT arg) = true →
1209      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1210      get_arg_8 ? s b (DIRECT arg).
1211  [2, 3: normalize % ]
1212  #m #s #arg #b #hyp
1213  whd in ⊢ (??%%)
1214  @vsplit_elim''
1215  #nu' #nl' #arg_nu_nl_eq
1216  normalize nodelta
1217  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1218  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1219  #get_index_v_eq
1220  normalize nodelta
1221  [2:
1222    normalize nodelta
1223    @vsplit_elim''
1224    #bit_one' #three_bits' #bit_one_three_bit_eq
1225    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1226    normalize nodelta
1227    generalize in match (refl ? (sub_7_with_carry ? ? ?))
1228    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1229    #Saddr #carr' #Saddr_carr_eq
1230    normalize nodelta
1231    #carr_hyp'
1232    @carr_hyp'
1233    [1:
1234    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1235        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1236        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1237        #member_eq
1238        normalize nodelta
1239        [2: #destr destruct(destr)
1240        |1: -carr_hyp';
1241            >arg_nu_nl_eq
1242            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1243            [1: >get_index_v_eq in ⊢ (??%? → ?)
1244            |2: @le_S @le_S @le_S @le_n
1245            ]
1246            cases (member (BitVector 8) ? (\fst ?) ?)
1247            [1: #destr normalize in destr; destruct(destr)
1248            |2:
1249            ]
1250        ]
1251    |3: >get_index_v_eq in ⊢ (??%?)
1252        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1253        >(vsplit_vector_singleton … bit_one_three_bit_eq)
1254        <arg_nu_nl_eq
1255        whd in hyp:(??%?)
1256        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1257        normalize nodelta [*: #ignore @sym_eq ]
1258    ]
1259  |
1260  ].
1261*)
1262(*
1263map_address0 ... (DIRECT arg) = Some .. →
1264  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1265  get_arg_8 (internal_ram ...) (DIRECT arg)
1266
1267((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
1268                     then Some internal_pseudo_address_map M 
1269                     else None internal_pseudo_address_map )
1270                    =Some internal_pseudo_address_map M')
1271
1272axiom low_internal_ram_write_at_stack_pointer:
1273 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
1274 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1275  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1276  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
1277  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1278  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1279  bu@@bl = sigma (pbu@@pbl) →
1280   low_internal_ram T1 cm1
1281     (write_at_stack_pointer …
1282       (set_8051_sfr …
1283         (write_at_stack_pointer …
1284           (set_8051_sfr …
1285             (set_low_internal_ram … s1
1286               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
1287             SFR_SP sp1)
1288          bl)
1289        SFR_SP sp2)
1290      bu)
1291   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1292      (low_internal_ram …
1293       (write_at_stack_pointer …
1294         (set_8051_sfr …
1295           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1296          SFR_SP sp2)
1297        pbu)).
1298
1299lemma high_internal_ram_write_at_stack_pointer:
1300 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
1301 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1302  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1303  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
1304  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1305  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1306  bu@@bl = sigma (pbu@@pbl) →
1307   high_internal_ram T1 cm1
1308     (write_at_stack_pointer …
1309       (set_8051_sfr …
1310         (write_at_stack_pointer …
1311           (set_8051_sfr …
1312             (set_high_internal_ram … s1
1313               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
1314             SFR_SP sp1)
1315          bl)
1316        SFR_SP sp2)
1317      bu)
1318   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
1319      (high_internal_ram …
1320       (write_at_stack_pointer …
1321         (set_8051_sfr …
1322           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1323          SFR_SP sp2)
1324        pbu)).
1325  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
1326  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
1327  cases daemon (* XXX: !!! *)
1328qed.
1329*)
1330
1331lemma snd_assembly_1_pseudoinstruction_ok:
1332  ∀program: pseudo_assembly_program.
1333  ∀program_length_proof: |\snd program| ≤ 2^16.
1334  ∀sigma: Word → Word.
1335  ∀policy: Word → bool.
1336  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1337  ∀ppc: Word.
1338  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
1339  ∀pi.
1340  ∀lookup_labels.
1341  ∀lookup_datalabels.
1342    let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
1343    lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →
1344    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1345    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
1346    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
1347      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
1348  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
1349  #lookup_labels #lookup_datalabels
1350  @pair_elim #labels #costs #create_label_cost_map_refl
1351  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
1352  normalize nodelta
1353  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
1354  #fetch_pseudo_refl
1355  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
1356  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
1357  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
1358  @pair_elim #preamble #instr_list #program_refl
1359  lapply create_label_cost_map_refl; -create_label_cost_map_refl
1360  >program_refl in ⊢ (% → ?); #create_label_cost_map_refl
1361  >create_label_cost_map_refl
1362  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
1363  lapply (H ppc ppc_in_bounds) -H
1364  @pair_elim #pi' #newppc #fetch_pseudo_refl'
1365  @pair_elim #len #assembled #assembly1_refl #H
1366  cases H
1367  #encoding_check_assm #sigma_newppc_refl
1368  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
1369  >pi_refl' in assembly1_refl; #assembly1_refl
1370  >lookup_labels_refl >lookup_datalabels_refl
1371  >program_refl normalize nodelta
1372  >assembly1_refl
1373  <sigma_newppc_refl
1374  generalize in match fetch_pseudo_refl';
1375  whd in match (fetch_pseudo_instruction ???);
1376  @pair_elim #lbl #instr #nth_refl normalize nodelta
1377  #G cases (pair_destruct_right ?????? G) %
1378qed.
1379
1380(* To be moved in ProofStatus *)
1381lemma program_counter_set_program_counter:
1382  ∀T.
1383  ∀cm.
1384  ∀s.
1385  ∀x.
1386    program_counter T cm (set_program_counter T cm s x) = x.
1387  //
1388qed.
Note: See TracBrowser for help on using the repository browser.