source: src/ASM/AssemblyProof.ma @ 3051

Last change on this file since 3051 was 2899, checked in by sacerdot, 7 years ago
  1. some renaming ASM_xxx to OC_xxx
  2. ASM_pre_classified_system implemented (up to the same missing cases as OC_pre_classified_system) Note: the invariant that the pc is always in the program cannot be maintained in case of function pointer calls and returns. To be dropped.
File size: 54.1 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3include "ASM/StatusProofs.ma".
4include alias "arithmetics/nat.ma".
5
6let rec encoding_check
7  (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
8    (encoding: list Byte)
9      on encoding: Prop ≝
10  match encoding with
11  [ nil ⇒ final_pc = pc
12  | cons hd tl ⇒
13    let 〈new_pc, byte〉 ≝ next code_memory pc in
14      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
15  ].
16
17lemma encoding_check_append:
18  ∀code_memory: BitVectorTrie Byte 16.
19  ∀final_pc: Word.
20  ∀l1: list Byte.
21  ∀pc: Word.
22  ∀l2: list Byte.
23    encoding_check code_memory pc final_pc (l1@l2) →
24      let pc_plus_len ≝ add … pc (bitvector_of_nat … (length … l1)) in
25        encoding_check code_memory pc pc_plus_len l1 ∧
26          encoding_check code_memory pc_plus_len final_pc l2.
27  #code_memory #final_pc #l1 elim l1
28  [1:
29    #pc #l2
30    whd in ⊢ (????% → ?); #H
31    <add_zero
32    whd whd in ⊢ (?%?); /2/
33  |2:
34    #hd #tl #IH #pc #l2 * #H1 #H2
35(*    >add_SO in H2; #H2 *)
36    cases (IH … H2) #E1 #E2 %
37    [1:
38      % try @H1
39      <(add_bitvector_of_nat_Sm 16 (|tl|)) in E1;
40      <add_associative #assm assumption
41    |2:
42      <add_associative in E2;
43      <(add_bitvector_of_nat_Sm 16 (|tl|)) #assm
44      assumption
45    ]
46  ]
47qed.
48
49lemma fetch_assembly:
50  ∀pc: Word.
51  ∀i: instruction.
52  ∀code_memory: BitVectorTrie Byte 16.
53  ∀assembled: list Byte.
54    assembled = assembly1 i →
55      let len ≝ length … assembled in
56      let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
57        encoding_check code_memory pc pc_plus_len assembled →
58          let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in
59           (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true.
60  cases daemon
61(* XXX: commented out as takes ages to typecheck
62  #pc #i #code_memory #assembled cases i [8: *]
63 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
64 [47,48,49:
65 |*: #arg @(subaddressing_mode_elim … arg)
66  [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,
67   59,60,63,64,65,66,67: #ARG]]
68 [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,
69  56,57,69,70,72: #arg2 @(subaddressing_mode_elim … arg2)
70  [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,
71   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,
72   68,69,70,71: #ARG2]]
73 [1,2,19,20: #arg3 @(subaddressing_mode_elim … arg3) #ARG3]
74 normalize in ⊢ (???% → ?);
75 [92,94,42,93,95: @vsplit_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
76  normalize in ⊢ (???% → ?);]
77 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
78 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
79 whd in match fetch; normalize nodelta <H1 whd in ⊢ (match % with [ _ ⇒ ? ]);
80 [17,18,19,20,21,22,23,24,25,26,32,34,35,36,37,39: <H3]
81 try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl *)
82qed.
83
84let rec fetch_many
85  (code_memory: BitVectorTrie Byte 16) (final_pc: Word) (pc: Word)
86    (expected: list instruction)
87      on expected: Prop ≝
88  match expected with
89  [ nil ⇒ eq_bv … pc final_pc = true
90  | cons i tl ⇒
91    let pc' ≝ add 16 pc (bitvector_of_nat 16 (|assembly1 … i|)) in
92      (〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
93        fetch_many code_memory final_pc pc' tl)
94  ].
95         
96lemma fetch_assembly_pseudo':
97  ∀lookup_labels.
98  ∀sigma: Word → Word.
99  ∀policy: Word → bool.
100  ∀ppc.
101  ∀lookup_datalabels.
102  ∀pi.
103  ∀code_memory.
104  ∀len.
105  ∀assembled.
106  ∀instructions.
107    let pc ≝ sigma ppc in
108      instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi →
109        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi →
110          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
111            encoding_check code_memory pc pc_plus_len assembled →
112              fetch_many code_memory pc_plus_len pc instructions.
113  #lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
114  normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
115  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
116  >len_refl >assembled_refl -len_refl
117  generalize in match (add 16 (sigma ppc)
118    (bitvector_of_nat 16
119     (|flatten (Vector bool 8)
120       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
121  #final_pc
122  generalize in match (sigma ppc); elim instructions
123  [1:
124    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
125  |2:
126    #i #tl #IH #pc #H whd
127    cases (encoding_check_append ????? H) -H #H1 #H2
128    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);   
129    cases (fetch ??) * #instr #pc' #ticks
130    #H3 lapply (H3 H1) -H3 normalize nodelta #H3
131    lapply (conjunction_true ?? H3) * #H4 #H5
132    lapply (conjunction_true … H4) * #B1 #B2
133    >(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) %
134    >(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2
135  ]
136qed.
137
138lemma fetch_assembly_pseudo:
139  ∀program: pseudo_assembly_program.
140  ∀sigma: Word → Word.
141  ∀policy: Word → bool.
142  let 〈labels, costs〉 ≝ create_label_cost_map (code program) in
143  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
144  ∀ppc.∀ppc_ok.
145  ∀code_memory.
146  let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (preamble program)) x (zero 16) in
147  let pi ≝  \fst  (fetch_pseudo_instruction (code program) ppc ppc_ok) in
148  let pc ≝ sigma ppc in
149  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
150  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
151  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
152    encoding_check code_memory pc pc_plus_len assembled →
153      fetch_many code_memory pc_plus_len pc instructions.
154  #program #sigma #policy
155  @pair_elim #labels #costs #create_label_cost_map_refl
156  letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory
157  letin lookup_datalabels ≝ (λx.?)
158  letin pi ≝ (fst ???)
159  letin pc ≝ (sigma ?)
160  letin instructions ≝ (expand_pseudo_instruction ??????)
161  @pair_elim #len #assembled #assembled_refl normalize nodelta
162  #H
163  generalize in match
164   (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
165  #X destruct normalize nodelta @X try % <assembled_refl try % assumption
166qed.
167
168definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
169  λpseudo_instruction.
170    match pseudo_instruction with
171    [ Comment c ⇒ False
172    | Cost c ⇒ False
173    | _ ⇒ True
174    ].
175
176(* This is a non trivial consequence of fetch_assembly_pseudo +
177   load_code_memory_ok because of the finite amount of memory. In
178   particular the case when the compiled program exhausts the
179   code memory is very tricky. It also requires monotonicity of
180   sigma in the out-of-bounds region too. *)     
181lemma assembly_ok:
182  ∀program: pseudo_assembly_program.
183  ∀length_proof: |code program| ≤ 2^16.
184  ∀sigma: Word → Word.
185  ∀policy: Word → bool.
186  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
187  ∀assembled: object_code.
188  ∀costs': BitVectorTrie costlabel 16.
189  let preamble ≝ preamble program in
190  let instr_list ≝ code program in
191  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
192  let datalabels ≝ construct_datalabels preamble in
193  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
194    let loc ≝ pi1 … (assembly program sigma policy) in
195    let assembled ≝ oc loc in
196    let costs' ≝ costlabels loc in
197      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
198        let code_memory ≝ load_code_memory assembled in
199        let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
200          ∀ppc.∀ppc_ok.
201            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (code program) ppc ppc_ok in     
202            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
203            let pc ≝ sigma ppc in
204            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
205              encoding_check code_memory pc pc_plus_len assembled ∧
206                  sigma newppc = add … pc (bitvector_of_nat … len).
207  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
208  cases (assembly program sigma policy) * #assembled' #costs'' #symbol_table #fpc #inj
209  cut (|code program| ≤ 2^16) [ // ] #instr_list_ok
210  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
211  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
212  * * #assembly_ok1 #assembly_ok3 #assembly_ok2
213  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
214  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
215  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
216  >eq_fetch_pseudo_instruction
217  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ? ∧ ∀j.∀H:j<|assembledi|.?) → ?)
218  >eq_assembly_1_pseudoinstruction
219  whd in ⊢ (% → ?); * #assembly_ok4 #assembly_ok
220  %
221  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
222      >snd_fetch_pseudo_instruction
223      cases sigma_policy_witness #_ #H cases (H ? ppc_ok) -H
224      #spw1 #_ >spw1 -spw1 @eq_f @eq_f
225      >eq_fetch_pseudo_instruction whd in match instruction_size;
226      normalize nodelta >create_label_cost_refl
227      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
228      [>eq_assembly_1_pseudoinstruction % | skip]
229  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
230    #load_code_memory_ok
231    lapply (fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) #EQlen
232    (* Nice statement here *)
233    cut (∀j. ∀H: j < |assembled|.
234          nth_safe Byte j assembled H =
235          \snd (next (load_code_memory assembled')
236          (bitvector_of_nat 16
237           (nat_of_bitvector …
238            (add … (sigma ppc) (bitvector_of_nat … j))))))
239    [1: #j #H cases (assembly_ok … H) #K -assembly_ok #assembly_ok <load_code_memory_ok
240        [ @assembly_ok | skip ]
241    |2:
242      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
243      elim assembled
244      [1:
245        #pc #_ whd <add_zero %
246      | #hd #tl #IH #pc #H %
247         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
248           >H -H whd in ⊢ (??%?); <add_zero //
249         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
250           [2: <add_bitvector_of_nat_Sm @add_associative ]
251           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
252           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
253           >add_associative % ]]]]
254qed.
255
256(* XXX: should we add that costs = costs'? *)
257lemma fetch_assembly_pseudo2:
258  ∀program.
259  ∀length_proof: |code program| ≤ 2^16.
260  ∀sigma.
261  ∀policy.
262  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
263  ∀ppc.∀ppc_ok.
264  let 〈labels, costs〉 ≝ create_label_cost_map (code program) in
265  let res ≝ pi1 … (assembly program sigma policy) in
266  let assembled ≝ oc res in
267  let cost' ≝ costlabels res in
268  let code_memory ≝ load_code_memory assembled in
269  let data_labels ≝ construct_datalabels (preamble program) in
270  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
271  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
272  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (code program) ppc ppc_ok in
273  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
274    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
275  * #preamble #instr_list #code_size_ok #renamed_symbol #final_label
276  #inj #well_labelled #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
277  @pair_elim #labels #costs #create_label_map_refl
278  letin res ≝ (assembly ???)
279  letin assembled ≝ (oc ?)
280  letin costs' ≝ (costlabels ?)
281  letin code_memory ≝ (load_code_memory ?)
282  letin data_labels ≝ (construct_datalabels ?)
283  letin lookup_labels ≝ (λx. ?)
284  letin lookup_datalabels ≝ (λx. ?)
285  lapply (assembly_ok ?? sigma policy sigma_policy_specification_witness assembled costs')
286  normalize nodelta try assumption
287  >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H
288  lapply (H … ppc_ok) -H
289  @pair_elim #pi #newppc #EQpi_neqppc
290(*CSC: was working, to be repaired after change in datatypes representation
291  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
292  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
293  #len #assembledi #EQ4 #H
294  lapply (H ppc) >fetch_pseudo_refl #H
295  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy)
296  >create_label_map_refl #X lapply (X ppc ppc_ok (load_code_memory assembled)) -X
297  >EQ4 #H1 cases (H ppc_ok)
298  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
299  >fetch_pseudo_refl in H1; #assm @assm assumption *) cases daemon
300qed.
301
302inductive upper_lower: Type[0] ≝
303  | upper: upper_lower
304  | lower: upper_lower.
305
306definition eq_upper_lower:
307    upper_lower → upper_lower → bool ≝
308  λleft: upper_lower.
309  λright: upper_lower.
310  match left with
311  [ upper ⇒
312    match right with
313    [ upper ⇒ true
314    | _     ⇒ false
315    ]
316  | lower ⇒
317    match right with
318    [ lower ⇒ true
319    | _     ⇒ false
320    ]
321  ].
322
323lemma eq_upper_lower_true_to_eq:
324  ∀left: upper_lower.
325  ∀right: upper_lower.
326    eq_upper_lower left right = true → left = right.
327  * * normalize try (#_ %)
328  #absurd destruct(absurd)
329qed.
330
331lemma eq_upper_lower_false_to_neq:
332  ∀left: upper_lower.
333  ∀right: upper_lower.
334    eq_upper_lower left right = false → left ≠ right.
335  * * normalize try (#absurd destruct(absurd))
336  @nmk #absurd destruct(absurd)
337qed.
338
339(* XXX: if upper then the byte in the entry is the least significant byte of the address and
340        the byte in the status is the most significant, otherwise if lower then the
341        other way around
342*)
343definition address_entry ≝ upper_lower × Byte.
344
345definition eq_accumulator_address_map_entry:
346    option address_entry → option address_entry → bool ≝
347  λleft.
348  λright.
349    match left with
350    [ None                   ⇒
351      match right with
352      [ None ⇒ true
353      | _    ⇒ false
354      ]
355    | Some upper_lower_addr ⇒
356      let 〈upper_lower, addr〉 ≝ upper_lower_addr in
357      match right with
358      [ Some upper_lower_addr' ⇒
359        let 〈upper_lower', addr'〉 ≝ upper_lower_addr' in
360          eq_upper_lower upper_lower upper_lower' ∧ eq_bv … addr addr'
361      | _                          ⇒ false
362      ]
363    ].
364
365lemma eq_accumulator_address_map_entry_true_to_eq:
366  ∀left: option address_entry.
367  ∀right: option address_entry.
368    eq_accumulator_address_map_entry left right = true → left = right.
369  #left #right cases left cases right
370  [1:
371    #_ %
372  |2,3:
373    * * #word normalize #absurd destruct(absurd)
374  |4:
375    * * #word * * #word'
376    [2,3:
377      #absurd normalize in absurd; destruct(absurd)
378    ]
379    normalize change with (eq_bv 8 ?? = true → ?)
380    #relevant >(eq_bv_eq … relevant) %
381  ]
382qed.
383
384lemma eq_bv_false_to_neq:
385  ∀n: nat.
386  ∀left, right: BitVector n.
387    eq_bv n left right = false → left ≠ right.
388  #n #left elim left
389  [1:
390    #right >(BitVector_O … right) normalize #absurd destruct(absurd)
391  |2:
392    #n' #hd #tl #inductive_hypothesis #right
393    cases (BitVector_Sn … right) #hd' * #tl' #right_refl
394    >right_refl normalize
395    cases hd normalize nodelta
396    cases hd' normalize nodelta
397    [2,3:
398      #_ @nmk #absurd destruct(absurd)
399    ]
400    change with (eq_bv ??? = false → ?)
401    #relevant lapply (inductive_hypothesis … relevant)
402    #tl_neq_assm @nmk #tl_eq_assm cases tl_neq_assm
403    #tl_eq_assm' @tl_eq_assm' destruct(tl_eq_assm) %
404  ]
405qed.
406   
407lemma eq_accumulator_address_map_entry_false_to_neq:
408  ∀left: option address_entry.
409  ∀right: option address_entry.
410    eq_accumulator_address_map_entry left right = false → left ≠ right.
411  #left #right cases left cases right
412  [1:
413    normalize #absurd destruct(absurd)
414  |2,3:
415    * * #word normalize #_ % #absurd destruct(absurd)
416  |4:
417    * * #word * * #word' normalize
418    [2,3:
419      #_ % #absurd destruct(absurd)
420    ]
421    change with (eq_bv ??? = false → ?)
422    #eq_bv_false_assm lapply (eq_bv_false_to_neq … eq_bv_false_assm)
423    #word_neq_assm % @Some_Some_elim #address_eq_assm cases word_neq_assm
424    #word_eq_assm @word_eq_assm destruct(address_eq_assm) %
425  ]
426qed.
427
428(* XXX: changed this type.  Bool specifies whether byte is first or second
429        component of an address, and the Word is the pseudoaddress that it
430        corresponds to.  Second component is the same principle for the accumulator
431        A.
432*)
433definition internal_pseudo_address_map ≝
434  (* low, high, acc *)
435  (BitVectorTrie address_entry 7) × (BitVectorTrie address_entry 7) × (option address_entry).
436
437include alias "ASM/BitVectorTrie.ma".
438 
439include "common/AssocList.ma".
440
441axiom bvt_map2:
442  ∀A, B, C: Type[0].
443  ∀n: nat.
444  ∀bvt_1: BitVectorTrie A n.
445  ∀bvt_2: BitVectorTrie B n.
446  ∀f: ∀a: option A. ∀b: option B. option C.
447    BitVectorTrie C n.
448
449(*
450axiom is_in_domain:
451  ∀A: Type[0].
452  ∀n: nat.
453  ∀bvt: BitVectorTrie A n.
454  ∀b: BitVector n.
455    Prop.
456
457axiom bvt_map2_function_extensionality:
458  ∀A, B, C: Type[0].
459  ∀n: nat.
460  ∀bvt_1: BitVectorTrie A n.
461  ∀bvt_2, bvt_2': BitVectorTrie B n.
462  ∀f: ∀a: option A. ∀b: option B. option C.
463    (∀addr.
464      is_in_domain … bvt_1 addr ∨ is_in_domain … bvt_2 addr ∨ is_in_domain … bvt_2' addr →
465        f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2) = f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2')) →
466          bvt_map2 … bvt_1 bvt_2 f = bvt_map2 … bvt_1 bvt_2' f.
467*)
468
469axiom lookup_opt_bvt_map2:
470 ∀A,B,C,n,map1,map2,f,addr.
471lookup_opt … addr (bvt_map2 A B C n map1 map2 f) =
472 f (lookup_opt … addr map1) (lookup_opt … addr map2).
473
474definition lookup_from_internal_ram:
475    ∀addr: Byte.
476    ∀M: internal_pseudo_address_map.
477      option address_entry ≝
478  λaddr, M.
479    let 〈low, high, accA〉 ≝ M in
480    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
481      if head' … bit_one then
482        lookup_opt … seven_bits high
483      else
484        lookup_opt … seven_bits low.
485
486definition map_value_using_opt_address_entry:
487  (Word → Word) → Byte → option address_entry → Byte ≝
488  λsigma: Word → Word.
489  λvalue: Byte.
490  λul_addr: option address_entry.
491  match ul_addr with
492  [ None ⇒ value
493  | Some upper_lower_word ⇒
494    let 〈upper_lower, word〉 ≝ upper_lower_word in
495      if eq_upper_lower upper_lower upper then
496        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in
497          high
498      else
499        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in
500          low
501  ].
502
503definition map_acc_a_using_internal_pseudo_address_map:
504 ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝
505   λM, sigma, v. map_value_using_opt_address_entry sigma v (\snd M).
506
507definition map_internal_ram_address_using_pseudo_address_map:
508  ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
509  λM: internal_pseudo_address_map.
510  λsigma: Word → Word.
511  λaddress: Byte.
512  λvalue: Byte.
513   map_value_using_opt_address_entry sigma value
514    (lookup_from_internal_ram … address M ).
515
516definition map_opt_value_using_opt_address_entry:
517 (Word → Word) → option Byte → option address_entry → option Byte ≝
518 λsigma,v,ul_addr.
519  let v ≝ match v with [ None ⇒ zero … | Some v ⇒ v ] in
520  let v' ≝ map_value_using_opt_address_entry sigma v ul_addr in
521    if eq_bv … v' (zero …) then
522      None …
523    else
524      Some … v'.
525
526definition internal_ram_of_pseudo_internal_ram:
527    ∀sigma: Word → Word.
528    ∀ram: BitVectorTrie Byte 7.
529    ∀map: BitVectorTrie address_entry 7.
530      BitVectorTrie Byte 7 ≝
531  λsigma, ram, map.
532      bvt_map2 ??? ? ram map (map_opt_value_using_opt_address_entry sigma).
533
534definition internal_half_pseudo_address_map_equal_up_to_address:
535 BitVectorTrie address_entry 7 → BitVectorTrie address_entry 7 → (Word → Word) →
536  BitVector 7 → Byte → Byte → Prop
537 ≝
538 λM,M',sigma,addr,v,v'.
539  v' = map_value_using_opt_address_entry sigma v (lookup_opt … addr M') ∧
540   ∀addr'. addr' ≠ addr → lookup_opt … addr' M = lookup_opt … addr' M'. 
541
542axiom insert_internal_ram_of_pseudo_internal_ram:
543 ∀M,M',sigma,addr,v,v',ram.
544  internal_half_pseudo_address_map_equal_up_to_address M M' sigma addr v v' →
545  insert Byte … addr v' (internal_ram_of_pseudo_internal_ram sigma ram M)
546  = internal_ram_of_pseudo_internal_ram sigma (insert ?? addr v ram) M'.
547
548definition low_internal_ram_of_pseudo_low_internal_ram:
549    ∀M: internal_pseudo_address_map.
550    ∀sigma: Word → Word.
551    ∀ram: BitVectorTrie Byte 7.
552      BitVectorTrie Byte 7 ≝
553  λM, sigma, ram.
554    let 〈low, high, accA〉 ≝ M in
555      internal_ram_of_pseudo_internal_ram sigma ram low.
556
557definition high_internal_ram_of_pseudo_high_internal_ram:
558    ∀M: internal_pseudo_address_map.
559    ∀sigma: Word → Word.
560    ∀ram: BitVectorTrie Byte 7.
561      BitVectorTrie Byte 7 ≝
562  λM, sigma, ram.
563    let 〈low, high, accA〉 ≝ M in
564      internal_ram_of_pseudo_internal_ram sigma ram high.
565
566(*
567axiom low_internal_ram_of_pseudo_internal_ram_hit:
568 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.
569  lookup_opt ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉  →
570   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in
571   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
572   let bl ≝ lookup ? 7 addr ram (zero 8) in
573   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
574   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (sigma points_to) in
575     if eq_upper_lower upper_lower upper then
576       (pbl = higher) ∧ (bl = phigher)
577     else
578       (pbl = lower) ∧ (bl = plower).
579*)
580
581(* changed from add to sub *)
582axiom low_internal_ram_of_pseudo_internal_ram_miss:
583 ∀T.∀M:internal_pseudo_address_map.∀sigma. ∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
584  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in
585    lookup_opt … addr (\fst (\fst M)) = None … →
586      lookup … addr ram (zero …) = lookup … addr (low_internal_ram … s) (zero ?).
587
588definition exists:
589    ∀A: Type[0].
590    ∀n: nat.
591    ∀v: BitVector n.
592    ∀bvt: BitVectorTrie A n.
593      bool ≝
594  λA, n, v, bvt.
595    match lookup_opt … v bvt with
596    [ None ⇒ false
597    | _    ⇒ true
598    ].
599
600definition data_or_address ≝
601  λT.
602  λM: internal_pseudo_address_map.
603  λcm.
604  λs: PreStatus T cm.
605  λaddr: addressing_mode.
606  let 〈low, high, accA〉 ≝ M in
607  match addr return λx. option (option address_entry) with
608    [ DIRECT d ⇒
609       let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
610         match head' … hd with
611         [ true ⇒
612             if eq_bv … d (bitvector_of_nat … 224) then
613               Some … accA
614             else
615               Some … (None …)
616         | false ⇒ Some … (lookup_opt … seven_bits low)
617         ]
618    | INDIRECT i ⇒
619        let d ≝ get_register … s [[false;false;i]] in
620        let address ≝ bit_address_of_register … s [[false;false;i]] in
621          if ¬exists … address low then
622            let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
623              if head' … 0 bit_one then
624                Some … (lookup_opt … seven_bits high)
625              else
626                Some … (lookup_opt … seven_bits low)
627          else
628            None ?
629    | EXT_INDIRECT e ⇒
630        let address ≝ bit_address_of_register … s [[false;false;e]] in
631          if ¬exists … address low then
632            Some … (None …)
633          else
634            None ?
635    | REGISTER r ⇒
636        let address ≝ bit_address_of_register … s r in
637          Some … (lookup_opt … address low)
638    | ACC_A ⇒ Some … accA
639    | ACC_B ⇒ Some … (None …)
640    | DPTR ⇒ Some … (None …)
641    | DATA _ ⇒ Some … (None …)
642    | DATA16 _ ⇒ Some … (None …)
643    | ACC_DPTR ⇒ Some … (None …)
644    | ACC_PC ⇒ Some … (None …)
645    | EXT_INDIRECT_DPTR ⇒ Some … (None …)
646    | INDIRECT_DPTR ⇒ Some … (None …)
647    | CARRY ⇒ Some … (None …)
648    | BIT_ADDR b ⇒
649      let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
650      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
651        if head' bool 0 bit_one then
652            if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *)
653              Some … accA
654            else
655              Some … (None …)
656        else
657          let address' ≝ [[true; false; false]]@@four_bits in
658            Some … (lookup_opt … address' low)
659    | N_BIT_ADDR b ⇒
660      let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
661      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
662        if head' bool 0 bit_one then
663            if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *)
664              Some … accA
665            else
666              Some … (None …)
667        else
668          let address' ≝ [[true; false; false]]@@four_bits in
669            Some … (lookup_opt … address' low)
670    | RELATIVE _ ⇒ Some … (None …)
671    | ADDR11 _ ⇒ Some … (None …)
672    | ADDR16 _ ⇒ Some … (None …)
673    ].
674
675definition assert_data ≝
676  λT.
677  λM: internal_pseudo_address_map.
678  λcm.
679  λs: PreStatus T cm.
680  λaddr: addressing_mode.
681    match data_or_address T M cm s addr with
682    [ None   ⇒ false
683    | Some s ⇒
684      match s with
685      [ None ⇒ true
686      | _    ⇒ false
687      ]
688    ].
689   
690definition insert_into_internal_ram:
691  ∀addr: Byte.
692  ∀v: address_entry.
693  ∀M: internal_pseudo_address_map.
694    internal_pseudo_address_map ≝
695  λaddr, v, M.
696    let 〈low, high, accA〉 ≝ M in
697    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
698      if head' … bit_one then
699        〈low, insert … seven_bits v high, accA〉
700      else
701        〈insert … seven_bits v low, high, accA〉.
702   
703axiom delete:
704  ∀A: Type[0].
705  ∀n: nat.
706  ∀b: BitVector n.
707    BitVectorTrie A n → BitVectorTrie A n.
708
709definition delete_from_internal_ram:
710    ∀addr: Byte.
711    ∀M: internal_pseudo_address_map.
712      internal_pseudo_address_map ≝
713  λaddr, M.
714    let 〈low, high, accA〉 ≝ M in
715    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
716      if head' … bit_one then
717        〈low,delete … seven_bits high, accA〉
718      else
719        〈delete … seven_bits low, high, accA〉.
720
721definition overwrite_or_delete_from_internal_ram:
722    ∀addr: Byte.
723    ∀v: option address_entry.
724    ∀M: internal_pseudo_address_map.
725      internal_pseudo_address_map ≝
726  λaddr, v, M.
727    match v with
728    [ None ⇒ delete_from_internal_ram addr M
729    | Some v' ⇒ insert_into_internal_ram addr v' M
730    ].
731   
732definition next_internal_pseudo_address_map0 ≝
733  λT.
734  λcm:T.
735  λaddr_of: Identifier → PreStatus T cm → Word.
736  λfetched.
737  λM: internal_pseudo_address_map.
738  λs: PreStatus T cm.
739  let 〈low, high, accA〉 ≝ M in
740   match fetched with
741    [ Comment _ ⇒ Some ? M
742    | Cost _ ⇒ Some … M
743    | Jmp _ ⇒ Some … M
744    | Jnz _ _ _ ⇒ Some … M
745    | MovSuccessor _ _ _ ⇒ ? (*CSC: TO BE IMPLEMENTED*)
746    | Call a ⇒
747      let a' ≝ addr_of a s in
748      let 〈upA, lowA〉 ≝ vsplit bool 8 8 a' in
749        Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) 〈lower, upA〉
750                (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) 〈upper, lowA〉 M))
751    | Mov _ _ ⇒ Some … M
752    | Instruction instr ⇒
753      match instr return λx. option internal_pseudo_address_map with
754       [ ADD addr1 addr2 ⇒
755         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
756           Some ? M
757         else
758           None ?
759       | ADDC addr1 addr2 ⇒
760         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
761           Some ? M
762         else
763           None ?
764       | SUBB addr1 addr2 ⇒
765         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
766           Some ? M
767         else
768           None ?
769       | INC addr1 ⇒
770         if assert_data T M ? s addr1 then
771           Some ? M
772         else
773           None ?
774       | DEC addr1 ⇒
775         if assert_data T M … s addr1 then
776           Some ? M
777         else
778           None ?
779       | MUL addr1 addr2 ⇒
780         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
781           Some ? M
782         else
783           None ?
784       | DIV addr1 addr2 ⇒
785         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
786           Some ? M
787         else
788           None ?
789       | DA addr1 ⇒
790         if assert_data T M … s addr1 then
791           Some ? M
792         else
793           None ?
794       | JC addr1 ⇒ Some ? M
795       | JMP _ ⇒ ? (*CSC: TO BE IMPLEMENTED*)
796       | JNC addr1 ⇒ Some ? M
797       | JB addr1 addr2 ⇒ Some ? M
798       | JNB addr1 addr2 ⇒ Some ? M
799       | JBC addr1 addr2 ⇒ Some ? M
800       | JZ addr1 ⇒ Some ? M
801       | JNZ addr1 ⇒ Some ? M
802       | CJNE addr1 addr2 ⇒
803         match addr1 with
804         [ inl l ⇒
805           let 〈left, right〉 ≝ l in
806             if assert_data T M … s left ∧ assert_data T M … s right then
807               Some ? M
808             else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then
809               Some ? M
810             else
811               None ?
812         | inr r ⇒
813           let 〈left, right〉 ≝ r in
814             if assert_data T M … s left ∧ assert_data T M … s right then
815               Some ? M
816             else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then
817               Some ? M
818             else
819               None ?
820         ]
821       | DJNZ addr1 addr2 ⇒
822         if assert_data T M … s addr1 then
823           Some ? M
824         else
825           None ?
826       | CLR addr1 ⇒
827         if assert_data T M … s addr1 then
828           Some ? M
829         else
830           None ?
831       | CPL addr1 ⇒
832         if assert_data T M … s addr1 then
833           Some ? M
834         else
835           None ?
836       | RL addr1 ⇒
837         if assert_data T M … s addr1 then
838           Some ? M
839         else
840           None ?
841       | RLC addr1 ⇒
842         if assert_data T M … s addr1 then
843           Some ? M
844         else
845           None ?
846       | RR addr1 ⇒
847         if assert_data T M … s addr1 then
848           Some ? M
849         else
850           None ?
851       | RRC addr1 ⇒
852         if assert_data T M … s addr1 then
853           Some ? M
854         else
855           None ?
856       | SWAP addr1 ⇒
857         if assert_data T M … s addr1 then
858           Some ? M
859         else
860           None ?
861       | SETB addr1 ⇒
862         if assert_data T M … s addr1 then
863           Some ? M
864         else
865           None ?
866       (* XXX: need to track addresses pushed and popped off the stack? *)
867       | PUSH addr1 ⇒
868         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
869         [ DIRECT d ⇒ λproof.
870           let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
871             if head' … bit_one then
872               if eq_bv … seven_bits (bitvector_of_nat … 224) then
873                 Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) accA M)
874               else
875                 Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M)
876             else
877               Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (lookup_from_internal_ram … d M) M)
878         | _ ⇒ λother: False. ⊥
879         ] (subaddressing_modein … addr1)
880       | POP addr1 ⇒
881         let sp ≝ get_8051_sfr ?? s SFR_SP in
882         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
883         [ DIRECT d ⇒ λproof.
884           let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
885             if head' … bit_one then
886               if eq_bv … d (bitvector_of_nat … 224) then
887                 Some … 〈low, high, lookup_from_internal_ram … sp M〉
888               else
889                 match lookup_from_internal_ram sp M with
890                 [ None ⇒ Some ? M
891                 | _    ⇒ None ?
892                 ]
893             else
894               Some … (overwrite_or_delete_from_internal_ram d (lookup_from_internal_ram … sp M) M)
895         | _ ⇒ λother: False. ⊥
896         ] (subaddressing_modein … addr1)
897       | XCH addr1 addr2 ⇒
898         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
899           Some ? M
900         else
901           None ?
902       | XCHD addr1 addr2 ⇒
903         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
904           Some ? M
905         else
906           None ?
907      | RET ⇒
908        let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
909        let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
910        match lookup_from_internal_ram sp_minus_1 M with
911        [ None ⇒ None …
912        | Some low_addr_high ⇒
913            match lookup_from_internal_ram sp_minus_2 M with
914            [ None ⇒ None …
915            | Some high_addr_low ⇒
916              let 〈low, addr_high〉 ≝ low_addr_high in
917              let 〈high, addr_low〉 ≝ high_addr_low in
918              let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
919              let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
920                if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
921                  Some ? M
922                else
923                  None ?
924            ]
925        ]
926      | RETI ⇒
927        let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
928        let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
929        match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M with
930        [ None ⇒ None …
931        | Some low_addr_high ⇒
932            match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) M with
933            [ None ⇒ None …
934            | Some high_addr_low ⇒
935              let 〈low, addr_high〉 ≝ low_addr_high in
936              let 〈high, addr_low〉 ≝ high_addr_low in
937              let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
938              let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
939                if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
940                  Some ? M
941                else
942                  None ?
943            ]
944        ]
945      | NOP ⇒ Some … M
946      | MOVX addr1 ⇒
947        match addr1 with
948        [ inl l ⇒
949            Some ? 〈low, high, None …〉
950        | inr r ⇒
951          let 〈others, acc_a〉 ≝ r in
952            if assert_data T M … s acc_a then
953              Some ? M
954            else
955              None ?
956        ]
957      | XRL addr1 ⇒
958        match addr1 with
959        [ inl l ⇒
960          let 〈acc_a, others〉 ≝ l in
961          let acc_a_ok ≝ assert_data T M … s acc_a in
962          let others_ok ≝ assert_data T M … s others in
963          if acc_a_ok ∧ others_ok then
964            Some ? M
965          else
966            None ?
967        | inr r ⇒
968          let 〈direct, others〉 ≝ r in
969          let direct_ok ≝ assert_data T M … s direct in
970          let others_ok ≝ assert_data T M … s others in
971          if direct_ok ∧ others_ok then
972            Some ? M
973          else
974            None ?
975        ]
976      | ORL addr1 ⇒
977        match addr1 with
978        [ inl l ⇒
979          match l with
980          [ inl l ⇒
981            let 〈acc_a, others〉 ≝ l in
982            let acc_a_ok ≝ assert_data T M … s acc_a in
983            let others_ok ≝ assert_data T M … s others in
984            if acc_a_ok ∧ others_ok then
985              Some ? M
986            else
987              None ?
988          | inr r ⇒
989            let 〈direct, others〉 ≝ r in
990            let direct_ok ≝ assert_data T M … s direct in
991            let others_ok ≝ assert_data T M … s others in
992            if direct_ok ∧ others_ok then
993              Some ? M
994            else
995              None ?
996          ]
997        | inr r ⇒
998          let 〈carry, others〉 ≝ r in
999          let carry_ok ≝ assert_data T M … s carry in
1000          let others_ok ≝ assert_data T M … s others in
1001          if carry_ok ∧ others_ok then
1002            Some ? M
1003          else
1004            None ?
1005        ]
1006      | ANL addr1 ⇒
1007        match addr1 with
1008        [ inl l ⇒
1009          match l with
1010          [ inl l ⇒
1011            let 〈acc_a, others〉 ≝ l in
1012            let acc_a_ok ≝ assert_data T M … s acc_a in
1013            let others_ok ≝ assert_data T M … s others in
1014            if acc_a_ok ∧ others_ok then
1015              Some ? M
1016            else
1017              None ?
1018          | inr r ⇒
1019            let 〈direct, others〉 ≝ r in
1020            let direct_ok ≝ assert_data T M … s direct in
1021            let others_ok ≝ assert_data T M … s others in
1022            if direct_ok ∧ others_ok then
1023              Some ? M
1024            else
1025              None ?
1026          ]
1027        | inr r ⇒
1028          let 〈carry, others〉 ≝ r in
1029          let carry_ok ≝ assert_data T M … s carry in
1030          let others_ok ≝ assert_data T M … s others in
1031          if carry_ok ∧ others_ok then
1032            Some ? M
1033          else
1034            None ?
1035        ]
1036      | MOV addr1 ⇒
1037        (* XXX: wrong *)
1038        match addr1 with
1039        [ inl l ⇒
1040          match l with
1041          [ inl l' ⇒
1042            match l' with
1043            [ inl l'' ⇒
1044              match l'' with
1045              [ inl l''' ⇒
1046                match l''' with
1047                [ inl l'''' ⇒
1048                  let 〈acc_a, others〉 ≝ l'''' in
1049                    match data_or_address T M … s others with
1050                    [ None ⇒ None ?
1051                    | Some s ⇒
1052                        Some … 〈low, high, s〉
1053                    ]
1054                | inr r ⇒
1055                  let 〈others, others'〉 ≝ r in
1056                  let address ≝
1057                    match others return λx. bool_to_Prop (is_in … [[ registr; indirect ]] x) → ? with
1058                    [ REGISTER r ⇒ λproof. false:::bit_address_of_register … s r
1059                    | INDIRECT i ⇒ λproof. get_register … s [[false; false; i]]
1060                    | _ ⇒ λother: False. ⊥
1061                    ] (subaddressing_modein … others)
1062                  in
1063                    match data_or_address T M … s others' with
1064                    [ None ⇒ None ?
1065                    | Some s ⇒
1066                        Some … (overwrite_or_delete_from_internal_ram address s M)
1067                    ]
1068                ]
1069              | inr r ⇒
1070                let 〈direct', others〉 ≝ r in
1071                  match direct' return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
1072                  [ DIRECT d ⇒ λproof.
1073                    match data_or_address T M … s others with
1074                    [ None ⇒ None ?
1075                    | Some s' ⇒
1076                        let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
1077                          if head' … bit_one then
1078                            if eq_bv … d (bitvector_of_nat … 224) then
1079                              Some … 〈low, high, s'〉
1080                            else
1081                              match s' with
1082                              [ None ⇒ Some ? M
1083                              | Some s'' ⇒ None ?
1084                              ]
1085                          else
1086                            Some … (overwrite_or_delete_from_internal_ram d s' M)
1087                    ]
1088                  | _ ⇒ λother: False. ⊥
1089                  ] (subaddressing_modein … direct')
1090              ]
1091            | inr r ⇒ Some … M
1092            ]
1093          | inr r ⇒
1094            let 〈carry, bit_addr〉 ≝ r in
1095            if assert_data T M … s bit_addr then
1096              Some ? M
1097            else
1098              None ?
1099          ]
1100        | inr r ⇒
1101          let 〈bit_addr, carry〉 ≝ r in
1102          if assert_data T M … s bit_addr then
1103            Some ? M
1104          else
1105            None ?
1106        ]
1107      ]
1108    ].
1109    cases other
1110qed.
1111
1112definition next_internal_pseudo_address_map ≝
1113 λM:internal_pseudo_address_map.
1114 λcm.
1115 λaddr_of.
1116 λs:PseudoStatus cm.
1117 λppc_ok.
1118    next_internal_pseudo_address_map0 ? cm addr_of
1119     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
1120
1121definition code_memory_of_pseudo_assembly_program:
1122    ∀pap:pseudo_assembly_program.
1123      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
1124  λpap.
1125  λsigma.
1126  λpolicy.
1127    let p ≝ pi1 … (assembly pap sigma policy) in
1128      load_code_memory (\fst p).
1129
1130definition sfr_8051_of_pseudo_sfr_8051 ≝
1131  λM: internal_pseudo_address_map.
1132  λsfrs: Vector Byte 19.
1133  λsigma: Word → Word.
1134    match \snd M with
1135    [ None ⇒ sfrs
1136    | Some upper_lower_address ⇒
1137      let index ≝ sfr_8051_index SFR_ACC_A in
1138      let acc_a ≝ get_index_v … sfrs index ? in
1139      let 〈upper_lower, address〉 ≝ upper_lower_address in
1140        if eq_upper_lower upper_lower upper then
1141          let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (acc_a@@address)) in
1142            set_index Byte 19 sfrs index high ?
1143        else
1144          let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (address@@acc_a)) in
1145            set_index Byte 19 sfrs index low ?
1146    ].
1147  //
1148qed.
1149
1150definition status_of_pseudo_status:
1151    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
1152      ∀sigma: Word → Word. ∀policy: Word → bool.
1153        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
1154  λM.
1155  λpap.
1156  λps.
1157  λsigma.
1158  λpolicy.
1159  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
1160  let pc ≝ sigma (program_counter … ps) in
1161  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … ps) in
1162  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M sigma (high_internal_ram … ps) in
1163     mk_PreStatus (BitVectorTrie Byte 16)
1164      cm
1165      lir
1166      hir
1167      (external_ram … ps)
1168      pc
1169      (sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma)
1170      (special_function_registers_8052 … ps)
1171      (p1_latch … ps)
1172      (p3_latch … ps)
1173      (clock … ps).
1174
1175(*
1176definition write_at_stack_pointer':
1177 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1178  λM: Type[0].
1179  λs: PreStatus M.
1180  λv: Byte.
1181    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
1182    let bit_zero ≝ get_index_v… nu O ? in
1183    let bit_1 ≝ get_index_v… nu 1 ? in
1184    let bit_2 ≝ get_index_v… nu 2 ? in
1185    let bit_3 ≝ get_index_v… nu 3 ? in
1186      if bit_zero then
1187        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1188                              v (low_internal_ram ? s) in
1189          set_low_internal_ram ? s memory
1190      else
1191        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1192                              v (high_internal_ram ? s) in
1193          set_high_internal_ram ? s memory.
1194  [ cases l0 %
1195  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1196qed.
1197
1198definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1199 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1200
1201  λticks_of.
1202  λs.
1203  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1204  let ticks ≝ ticks_of (program_counter ? s) in
1205  let s ≝ set_clock ? s (clock ? s + ticks) in
1206  let s ≝ set_program_counter ? s pc in
1207    match instr with
1208    [ Instruction instr ⇒
1209       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1210    | Comment cmt ⇒ s
1211    | Cost cst ⇒ s
1212    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1213    | Call call ⇒
1214      let a ≝ address_of_word_labels s call in
1215      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1216      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1217      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
1218      let s ≝ write_at_stack_pointer' ? s pc_bl in
1219      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1220      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1221      let s ≝ write_at_stack_pointer' ? s pc_bu in
1222        set_program_counter ? s a
1223    | Mov dptr ident ⇒
1224       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1225    ].
1226 [
1227 |2,3,4: %
1228 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1229 |
1230 | %
1231 ]
1232 cases not_implemented
1233qed.
1234*)
1235
1236(*
1237lemma execute_code_memory_unchanged:
1238 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1239 #ticks #ps whd in ⊢ (??? (??%))
1240 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1241  (program_counter pseudo_assembly_program ps)) #instr #pc
1242 whd in ⊢ (??? (??%)) cases instr
1243  [ #pre cases pre
1244     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1245       cases (vsplit ????) #z1 #z2 %
1246     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1247       cases (vsplit ????) #z1 #z2 %
1248     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1249       cases (vsplit ????) #z1 #z2 %
1250     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1251       [ #x1 whd in ⊢ (??? (??%))
1252     | *: cases not_implemented
1253     ]
1254  | #comment %
1255  | #cost %
1256  | #label %
1257  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1258    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1259    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
1260    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1261    (* CSC: ??? *)
1262  | #dptr #label (* CSC: ??? *)
1263  ]
1264  cases not_implemented
1265qed.
1266*)
1267
1268(* XXX: check values returned for conditional jumps below! They are wrong,
1269        find correct values *)
1270
1271(*
1272lemma blah:
1273  ∀m: internal_pseudo_address_map.
1274  ∀s: PseudoStatus.
1275  ∀arg: Byte.
1276  ∀b: bool.
1277    assert_data m s (DIRECT arg) = true →
1278      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1279      get_arg_8 ? s b (DIRECT arg).
1280  [2, 3: normalize % ]
1281  #m #s #arg #b #hyp
1282  whd in ⊢ (??%%)
1283  @vsplit_elim''
1284  #nu' #nl' #arg_nu_nl_eq
1285  normalize nodelta
1286  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1287  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1288  #get_index_v_eq
1289  normalize nodelta
1290  [2:
1291    normalize nodelta
1292    @vsplit_elim''
1293    #bit_one' #three_bits' #bit_one_three_bit_eq
1294    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1295    normalize nodelta
1296    generalize in match (refl ? (sub_7_with_carry ? ? ?))
1297    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1298    #Saddr #carr' #Saddr_carr_eq
1299    normalize nodelta
1300    #carr_hyp'
1301    @carr_hyp'
1302    [1:
1303    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1304        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1305        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1306        #member_eq
1307        normalize nodelta
1308        [2: #destr destruct(destr)
1309        |1: -carr_hyp';
1310            >arg_nu_nl_eq
1311            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1312            [1: >get_index_v_eq in ⊢ (??%? → ?)
1313            |2: @le_S @le_S @le_S @le_n
1314            ]
1315            cases (member (BitVector 8) ? (\fst ?) ?)
1316            [1: #destr normalize in destr; destruct(destr)
1317            |2:
1318            ]
1319        ]
1320    |3: >get_index_v_eq in ⊢ (??%?)
1321        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1322        >(vsplit_vector_singleton … bit_one_three_bit_eq)
1323        <arg_nu_nl_eq
1324        whd in hyp:(??%?)
1325        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1326        normalize nodelta [*: #ignore @sym_eq ]
1327    ]
1328  |
1329  ].
1330*)
1331(*
1332map_address0 ... (DIRECT arg) = Some .. →
1333  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1334  get_arg_8 (internal_ram ...) (DIRECT arg)
1335
1336((if assert_data M ps ACC_A∧assert_data M ps (DIRECT ARG2) 
1337                     then Some internal_pseudo_address_map M 
1338                     else None internal_pseudo_address_map )
1339                    =Some internal_pseudo_address_map M')
1340
1341axiom low_internal_ram_write_at_stack_pointer:
1342 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
1343 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1344  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1345  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
1346  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1347  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1348  bu@@bl = sigma (pbu@@pbl) →
1349   low_internal_ram T1 cm1
1350     (write_at_stack_pointer …
1351       (set_8051_sfr …
1352         (write_at_stack_pointer …
1353           (set_8051_sfr …
1354             (set_low_internal_ram … s1
1355               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
1356             SFR_SP sp1)
1357          bl)
1358        SFR_SP sp2)
1359      bu)
1360   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1361      (low_internal_ram …
1362       (write_at_stack_pointer …
1363         (set_8051_sfr …
1364           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1365          SFR_SP sp2)
1366        pbu)).
1367
1368lemma high_internal_ram_write_at_stack_pointer:
1369 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
1370 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1371  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1372  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
1373  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1374  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1375  bu@@bl = sigma (pbu@@pbl) →
1376   high_internal_ram T1 cm1
1377     (write_at_stack_pointer …
1378       (set_8051_sfr …
1379         (write_at_stack_pointer …
1380           (set_8051_sfr …
1381             (set_high_internal_ram … s1
1382               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
1383             SFR_SP sp1)
1384          bl)
1385        SFR_SP sp2)
1386      bu)
1387   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
1388      (high_internal_ram …
1389       (write_at_stack_pointer …
1390         (set_8051_sfr …
1391           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1392          SFR_SP sp2)
1393        pbu)).
1394  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
1395  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
1396  cases daemon (* XXX: !!! *)
1397qed.
1398*)
1399
1400lemma snd_assembly_1_pseudoinstruction_ok:
1401  ∀program: pseudo_assembly_program.
1402  ∀program_length_proof: |\snd program| ≤ 2^16.
1403  ∀sigma: Word → Word.
1404  ∀policy: Word → bool.
1405  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1406  ∀ppc: Word.
1407  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
1408  ∀pi.
1409  ∀lookup_labels.
1410  ∀lookup_datalabels.
1411    let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
1412    lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →
1413    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1414    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
1415    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
1416      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
1417  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
1418  #lookup_labels #lookup_datalabels
1419  @pair_elim #labels #costs #create_label_cost_map_refl
1420  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
1421  normalize nodelta
1422  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
1423  #fetch_pseudo_refl
1424  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
1425  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
1426  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
1427  @pair_elim #preamble #instr_list #program_refl
1428  lapply create_label_cost_map_refl; -create_label_cost_map_refl
1429  >program_refl in ⊢ (% → ?); #create_label_cost_map_refl
1430  >create_label_cost_map_refl
1431  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
1432  lapply (H ppc ppc_in_bounds) -H
1433  @pair_elim #pi' #newppc #fetch_pseudo_refl'
1434  @pair_elim #len #assembled #assembly1_refl #H
1435  cases H
1436  #encoding_check_assm #sigma_newppc_refl
1437  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
1438  >pi_refl' in assembly1_refl; #assembly1_refl
1439  >lookup_labels_refl >lookup_datalabels_refl
1440  >program_refl normalize nodelta
1441  >assembly1_refl
1442  <sigma_newppc_refl
1443  generalize in match fetch_pseudo_refl';
1444  whd in match (fetch_pseudo_instruction ???);
1445  @pair_elim #lbl #instr #nth_refl normalize nodelta
1446  #G cases (pair_destruct_right ?????? G) %
1447qed.
1448
1449(* To be moved in ProofStatus *)
1450lemma program_counter_set_program_counter:
1451  ∀T.
1452  ∀cm.
1453  ∀s.
1454  ∀x.
1455    program_counter T cm (set_program_counter T cm s x) = x.
1456  //
1457qed.
Note: See TracBrowser for help on using the repository browser.