source: src/ASM/AssemblyProof.ma @ 2771

Last change on this file since 2771 was 2516, checked in by mckinna, 7 years ago

removed typedefs; restored older versions; moved typedefs to compiler.ma
AssemblyProofSplit? *still* doesn't typecheck: disambiguation errors!

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