 Timestamp:
 Jun 28, 2012, 2:34:55 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2132 r2135 197 197 inversion (assembly_1_pseudoinstruction ??????) #len' #assembled' 198 198 whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct % 199 qed.200 201 (* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *)202 lemma assembly_ok:203 ∀program.204 ∀length_proof: \snd program ≤ 2^16.205 ∀sigma: Word → Word.206 ∀policy: Word → bool.207 ∀sigma_policy_witness: sigma_policy_specification program sigma policy.208 ∀assembled.209 ∀costs': BitVectorTrie costlabel 16.210 let 〈preamble, instr_list〉 ≝ program in211 let 〈labels, costs〉 ≝ create_label_cost_map instr_list in212 let datalabels ≝ construct_datalabels preamble in213 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in214 〈assembled,costs'〉 = assembly program sigma policy →215 (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)216 let code_memory ≝ load_code_memory assembled in217 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in218 ∀ppc.∀ppc_ok.219 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in220 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in221 let pc ≝ sigma ppc in222 let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in223 encoding_check code_memory pc pc_plus_len assembled ∧224 sigma newppc = add … pc (bitvector_of_nat … len).225 #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'226 cases (assembly program sigma policy) * #assembled' #costs''227 @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);228 cut (instr_list ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok229 #H lapply (H sigma_policy_witness instr_list_ok) H whd in ⊢ (% → ?);230 @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);231 * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd232 #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction233 @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd234 lapply (assembly_ok2 ppc ?) try // assembly_ok2235 >eq_fetch_pseudo_instruction236 change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<assembledi.?) → ?)237 >eq_assembly_1_pseudoinstruction238 whd in ⊢ (% → ?); #assembly_ok239 %240 [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))241 >snd_fetch_pseudo_instruction242 cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) H243 #spw1 #_ >spw1 spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f244 >eq_fetch_pseudo_instruction whd in match instruction_size;245 normalize nodelta >create_label_cost_refl246 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels247 [>eq_assembly_1_pseudoinstruction %  skip]248  lapply (load_code_memory_ok assembled' ?) [ assumption ]249 #load_code_memory_ok250 lapply (fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) #EQlen251 (* Nice statement here *)252 cut (∀j. ∀H: j < assembled.253 nth_safe Byte j assembled H =254 \snd (next (load_code_memory assembled')255 (bitvector_of_nat 16256 (nat_of_bitvector …257 (add … (sigma ppc) (bitvector_of_nat … j))))))258 [1:259 cases daemon260 2:261 assembly_ok load_code_memory_ok generalize in match (sigma ppc); >EQlen len262 elim assembled263 [1:264 #pc #_ whd <add_zero %265  #hd #tl #IH #pc #H %266 [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); H #H267 >H H whd in ⊢ (??%?); <add_zero //268  >(?: add … pc (bitvector_of_nat … (S (tl))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (tl)))269 [2: <add_bitvector_of_nat_Sm @add_associative ]270 @IH IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]271 <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm272 >add_associative % ]]273 ]]274 qed.275 276 (* XXX: should we add that costs = costs'? *)277 lemma fetch_assembly_pseudo2:278 ∀program.279 ∀length_proof: \snd program ≤ 2^16.280 ∀sigma.281 ∀policy.282 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.283 ∀ppc.∀ppc_ok.284 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in285 let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in286 let code_memory ≝ load_code_memory assembled in287 let data_labels ≝ construct_datalabels (\fst program) in288 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in289 let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in290 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in291 let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in292 fetch_many code_memory (sigma newppc) (sigma ppc) instructions.293 * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok294 @pair_elim #labels #costs #create_label_map_refl295 @pair_elim #assembled #costs' #assembled_refl296 letin code_memory ≝ (load_code_memory ?)297 letin data_labels ≝ (construct_datalabels ?)298 letin lookup_labels ≝ (λx. ?)299 letin lookup_datalabels ≝ (λx. ?)300 @pair_elim #pi #newppc #fetch_pseudo_refl301 lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')302 normalize nodelta try assumption303 >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H304 lapply (H (sym_eq … assembled_refl)) H305 lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))306 cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);307 #len #assembledi #EQ4 #H308 lapply (H ppc) >fetch_pseudo_refl #H309 lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy)310 >create_label_map_refl #X lapply (X ppc ppc_ok (load_code_memory assembled)) X311 >EQ4 #H1 cases (H ppc_ok)312 #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta313 >fetch_pseudo_refl in H1; #assm @assm assumption314 qed.315 316 (* XXX: changed this type. Bool specifies whether byte is first or second317 component of an address, and the Word is the pseudoaddress that it318 corresponds to. Second component is the same principle for the accumulator319 A.320 *)321 definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).322 323 include alias "ASM/BitVectorTrie.ma".324 325 include "common/AssocList.ma".326 327 axiom low_internal_ram_of_pseudo_low_internal_ram:328 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.329 330 axiom high_internal_ram_of_pseudo_high_internal_ram:331 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.332 333 axiom low_internal_ram_of_pseudo_internal_ram_hit:334 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7.335 assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉) →336 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in337 let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in338 let bl ≝ lookup ? 7 addr ram (zero 8) in339 let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in340 let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in341 if high then342 (pbl = higher) ∧ (bl = phigher)343 else344 (pbl = lower) ∧ (bl = plower).345 346 (* changed from add to sub *)347 axiom low_internal_ram_of_pseudo_internal_ram_miss:348 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.349 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in350 assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →351 lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).352 353 definition addressing_mode_ok ≝354 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.355 λaddr:addressing_mode.356 match addr with357 [ DIRECT d ⇒358 ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧359 ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))360  INDIRECT i ⇒361 let d ≝ get_register … s [[false;false;i]] in362 ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧363 ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))364  EXT_INDIRECT _ ⇒ true365  REGISTER _ ⇒ true366  ACC_A ⇒ match \snd M with [ None ⇒ true  _ ⇒ false ]367  ACC_B ⇒ true368  DPTR ⇒ true369  DATA _ ⇒ true370  DATA16 _ ⇒ true371  ACC_DPTR ⇒ true372  ACC_PC ⇒ true373  EXT_INDIRECT_DPTR ⇒ true374  INDIRECT_DPTR ⇒ true375  CARRY ⇒ true376  BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)377  N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)378  RELATIVE _ ⇒ true379  ADDR11 _ ⇒ true380  ADDR16 _ ⇒ true ].381 382 definition next_internal_pseudo_address_map0 ≝383 λT.384 λcm:T.385 λaddr_of: Identifier → PreStatus T cm → Word.386 λfetched.387 λM: internal_pseudo_address_map.388 λs: PreStatus T cm.389 match fetched with390 [ Comment _ ⇒ Some ? M391  Cost _ ⇒ Some … M392  Jmp _ ⇒ Some … M393  Call a ⇒394 let a' ≝ addr_of a s in395 let 〈callM, accM〉 ≝ M in396 Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉::397 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉398  Mov _ _ ⇒ Some … M399  Instruction instr ⇒400 match instr with401 [ ADD addr1 addr2 ⇒402 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then403 Some ? M404 else405 None ?406  ADDC addr1 addr2 ⇒407 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then408 Some ? M409 else410 None ?411  SUBB addr1 addr2 ⇒412 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then413 Some ? M414 else415 None ?416  _ ⇒ (* TO BE COMPLETED *) Some ? M ]].417 418 definition next_internal_pseudo_address_map ≝419 λM:internal_pseudo_address_map.420 λcm.421 λaddr_of.422 λs:PseudoStatus cm.423 λppc_ok.424 next_internal_pseudo_address_map0 ? cm addr_of425 (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.426 427 definition code_memory_of_pseudo_assembly_program:428 ∀pap:pseudo_assembly_program.429 (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝430 λpap.431 λsigma.432 λpolicy.433 let p ≝ pi1 … (assembly pap sigma policy) in434 load_code_memory (\fst p).435 436 definition sfr_8051_of_pseudo_sfr_8051 ≝437 λM: internal_pseudo_address_map.438 λsfrs: Vector Byte 19.439 λsigma: Word → Word.440 match \snd M with441 [ None ⇒ sfrs442  Some s ⇒443 let 〈high, address〉 ≝ s in444 let index ≝ sfr_8051_index SFR_ACC_A in445 let 〈upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in446 if high then447 set_index Byte 19 sfrs index upper ?448 else449 set_index Byte 19 sfrs index lower ?450 ].451 //452 qed.453 454 definition status_of_pseudo_status:455 internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.456 ∀sigma: Word → Word. ∀policy: Word → bool.457 Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝458 λM.459 λpap.460 λps.461 λsigma.462 λpolicy.463 let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in464 let pc ≝ sigma (program_counter … ps) in465 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in466 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in467 mk_PreStatus (BitVectorTrie Byte 16)468 cm469 lir470 hir471 (external_ram … ps)472 pc473 (special_function_registers_8051 … ps)474 (special_function_registers_8052 … ps)475 (p1_latch … ps)476 (p3_latch … ps)477 (clock … ps).478 479 (*480 definition write_at_stack_pointer':481 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝482 λM: Type[0].483 λs: PreStatus M.484 λv: Byte.485 let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in486 let bit_zero ≝ get_index_v… nu O ? in487 let bit_1 ≝ get_index_v… nu 1 ? in488 let bit_2 ≝ get_index_v… nu 2 ? in489 let bit_3 ≝ get_index_v… nu 3 ? in490 if bit_zero then491 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)492 v (low_internal_ram ? s) in493 set_low_internal_ram ? s memory494 else495 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)496 v (high_internal_ram ? s) in497 set_high_internal_ram ? s memory.498 [ cases l0 %499 2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]500 qed.501 502 definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.503 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')504 ≝505 λticks_of.506 λs.507 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in508 let ticks ≝ ticks_of (program_counter ? s) in509 let s ≝ set_clock ? s (clock ? s + ticks) in510 let s ≝ set_program_counter ? s pc in511 match instr with512 [ Instruction instr ⇒513 execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s514  Comment cmt ⇒ s515  Cost cst ⇒ s516  Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)517  Call call ⇒518 let a ≝ address_of_word_labels s call in519 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in520 let s ≝ set_8051_sfr ? s SFR_SP new_sp in521 let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in522 let s ≝ write_at_stack_pointer' ? s pc_bl in523 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in524 let s ≝ set_8051_sfr ? s SFR_SP new_sp in525 let s ≝ write_at_stack_pointer' ? s pc_bu in526 set_program_counter ? s a527  Mov dptr ident ⇒528 set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr529 ].530 [531 2,3,4: %532  <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %533 534  %535 ]536 cases not_implemented537 qed.538 *)539 540 (*541 lemma execute_code_memory_unchanged:542 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).543 #ticks #ps whd in ⊢ (??? (??%))544 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))545 (program_counter pseudo_assembly_program ps)) #instr #pc546 whd in ⊢ (??? (??%)) cases instr547 [ #pre cases pre548 [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))549 cases (vsplit ????) #z1 #z2 %550  #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))551 cases (vsplit ????) #z1 #z2 %552  #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))553 cases (vsplit ????) #z1 #z2 %554  #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x555 [ #x1 whd in ⊢ (??? (??%))556  *: cases not_implemented557 ]558  #comment %559  #cost %560  #label %561  #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))562 cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2563 whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2564 whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))565 (* CSC: ??? *)566  #dptr #label (* CSC: ??? *)567 ]568 cases not_implemented569 qed.570 *)571 572 (* DEAD CODE?573 lemma status_of_pseudo_status_failure_depends_only_on_code_memory:574 ∀M:internal_pseudo_address_map.575 ∀ps,ps': PseudoStatus.576 ∀pol.577 ∀prf:code_memory … ps = code_memory … ps'.578 let pol' ≝ ? in579 match status_of_pseudo_status M ps pol with580 [ None ⇒ status_of_pseudo_status M ps' pol' = None …581  Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w582 ].583 [2: <prf @pol]584 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ])585 generalize in match (refl … (assembly (code_memory … ps) pol))586 cases (assembly ??) in ⊢ (???% → %)587 [ #K whd whd in ⊢ (??%?) <H >K %588  #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]589 qed.590 *)591 592 definition ticks_of0:593 ∀p:pseudo_assembly_program.594 (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝595 λprogram: pseudo_assembly_program.596 λsigma.597 λpolicy.598 λppc: Word.599 λfetched.600 match fetched with601 [ Instruction instr ⇒602 match instr with603 [ JC lbl ⇒ ? (*604 match pol lookup_labels ppc with605 [ short_jump ⇒ 〈2, 2〉606  absolute_jump ⇒ ?607  long_jump ⇒ 〈4, 4〉608 ] *)609  JNC lbl ⇒ ? (*610 match pol lookup_labels ppc with611 [ short_jump ⇒ 〈2, 2〉612  absolute_jump ⇒ ?613  long_jump ⇒ 〈4, 4〉614 ] *)615  JB bit lbl ⇒ ? (*616 match pol lookup_labels ppc with617 [ short_jump ⇒ 〈2, 2〉618  absolute_jump ⇒ ?619  long_jump ⇒ 〈4, 4〉620 ] *)621  JNB bit lbl ⇒ ? (*622 match pol lookup_labels ppc with623 [ short_jump ⇒ 〈2, 2〉624  absolute_jump ⇒ ?625  long_jump ⇒ 〈4, 4〉626 ] *)627  JBC bit lbl ⇒ ? (*628 match pol lookup_labels ppc with629 [ short_jump ⇒ 〈2, 2〉630  absolute_jump ⇒ ?631  long_jump ⇒ 〈4, 4〉632 ] *)633  JZ lbl ⇒ ? (*634 match pol lookup_labels ppc with635 [ short_jump ⇒ 〈2, 2〉636  absolute_jump ⇒ ?637  long_jump ⇒ 〈4, 4〉638 ] *)639  JNZ lbl ⇒ ? (*640 match pol lookup_labels ppc with641 [ short_jump ⇒ 〈2, 2〉642  absolute_jump ⇒ ?643  long_jump ⇒ 〈4, 4〉644 ] *)645  CJNE arg lbl ⇒ ? (*646 match pol lookup_labels ppc with647 [ short_jump ⇒ 〈2, 2〉648  absolute_jump ⇒ ?649  long_jump ⇒ 〈4, 4〉650 ] *)651  DJNZ arg lbl ⇒ ? (*652 match pol lookup_labels ppc with653 [ short_jump ⇒ 〈2, 2〉654  absolute_jump ⇒ ?655  long_jump ⇒ 〈4, 4〉656 ] *)657  ADD arg1 arg2 ⇒658 let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in659 〈ticks, ticks〉660  ADDC arg1 arg2 ⇒661 let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in662 〈ticks, ticks〉663  SUBB arg1 arg2 ⇒664 let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in665 〈ticks, ticks〉666  INC arg ⇒667 let ticks ≝ ticks_of_instruction (INC ? arg) in668 〈ticks, ticks〉669  DEC arg ⇒670 let ticks ≝ ticks_of_instruction (DEC ? arg) in671 〈ticks, ticks〉672  MUL arg1 arg2 ⇒673 let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in674 〈ticks, ticks〉675  DIV arg1 arg2 ⇒676 let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in677 〈ticks, ticks〉678  DA arg ⇒679 let ticks ≝ ticks_of_instruction (DA ? arg) in680 〈ticks, ticks〉681  ANL arg ⇒682 let ticks ≝ ticks_of_instruction (ANL ? arg) in683 〈ticks, ticks〉684  ORL arg ⇒685 let ticks ≝ ticks_of_instruction (ORL ? arg) in686 〈ticks, ticks〉687  XRL arg ⇒688 let ticks ≝ ticks_of_instruction (XRL ? arg) in689 〈ticks, ticks〉690  CLR arg ⇒691 let ticks ≝ ticks_of_instruction (CLR ? arg) in692 〈ticks, ticks〉693  CPL arg ⇒694 let ticks ≝ ticks_of_instruction (CPL ? arg) in695 〈ticks, ticks〉696  RL arg ⇒697 let ticks ≝ ticks_of_instruction (RL ? arg) in698 〈ticks, ticks〉699  RLC arg ⇒700 let ticks ≝ ticks_of_instruction (RLC ? arg) in701 〈ticks, ticks〉702  RR arg ⇒703 let ticks ≝ ticks_of_instruction (RR ? arg) in704 〈ticks, ticks〉705  RRC arg ⇒706 let ticks ≝ ticks_of_instruction (RRC ? arg) in707 〈ticks, ticks〉708  SWAP arg ⇒709 let ticks ≝ ticks_of_instruction (SWAP ? arg) in710 〈ticks, ticks〉711  MOV arg ⇒712 let ticks ≝ ticks_of_instruction (MOV ? arg) in713 〈ticks, ticks〉714  MOVX arg ⇒715 let ticks ≝ ticks_of_instruction (MOVX ? arg) in716 〈ticks, ticks〉717  SETB arg ⇒718 let ticks ≝ ticks_of_instruction (SETB ? arg) in719 〈ticks, ticks〉720  PUSH arg ⇒721 let ticks ≝ ticks_of_instruction (PUSH ? arg) in722 〈ticks, ticks〉723  POP arg ⇒724 let ticks ≝ ticks_of_instruction (POP ? arg) in725 〈ticks, ticks〉726  XCH arg1 arg2 ⇒727 let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in728 〈ticks, ticks〉729  XCHD arg1 arg2 ⇒730 let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in731 〈ticks, ticks〉732  RET ⇒733 let ticks ≝ ticks_of_instruction (RET ?) in734 〈ticks, ticks〉735  RETI ⇒736 let ticks ≝ ticks_of_instruction (RETI ?) in737 〈ticks, ticks〉738  NOP ⇒739 let ticks ≝ ticks_of_instruction (NOP ?) in740 〈ticks, ticks〉741 ]742  Comment comment ⇒ 〈0, 0〉743  Cost cost ⇒ 〈0, 0〉744  Jmp jmp ⇒ 〈2, 2〉745  Call call ⇒ 〈2, 2〉746  Mov dptr tgt ⇒ 〈2, 2〉747 ].748 cases daemon749 qed.750 751 definition ticks_of:752 ∀p:pseudo_assembly_program.753 (Word → Word) → (Word → bool) → ∀ppc:Word.754 nat_of_bitvector … ppc < \snd p → nat × nat ≝755 λprogram: pseudo_assembly_program.756 λsigma.757 λpolicy.758 λppc: Word. λppc_ok.759 let pseudo ≝ \snd program in760 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in761 ticks_of0 program sigma policy ppc fetched.762 763 (*764 lemma blah:765 ∀m: internal_pseudo_address_map.766 ∀s: PseudoStatus.767 ∀arg: Byte.768 ∀b: bool.769 addressing_mode_ok m s (DIRECT arg) = true →770 get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =771 get_arg_8 ? s b (DIRECT arg).772 [2, 3: normalize % ]773 #m #s #arg #b #hyp774 whd in ⊢ (??%%)775 @vsplit_elim''776 #nu' #nl' #arg_nu_nl_eq777 normalize nodelta778 generalize in match (refl ? (get_index_v bool 4 nu' ? ?))779 cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)780 #get_index_v_eq781 normalize nodelta782 [2:783 normalize nodelta784 @vsplit_elim''785 #bit_one' #three_bits' #bit_one_three_bit_eq786 generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))787 normalize nodelta788 generalize in match (refl ? (sub_7_with_carry ? ? ?))789 cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)790 #Saddr #carr' #Saddr_carr_eq791 normalize nodelta792 #carr_hyp'793 @carr_hyp'794 [1:795 2: whd in hyp:(??%?); generalize in match hyp; hyp;796 generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))797 cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)798 #member_eq799 normalize nodelta800 [2: #destr destruct(destr)801 1: carr_hyp';802 >arg_nu_nl_eq803 <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)804 [1: >get_index_v_eq in ⊢ (??%? → ?)805 2: @le_S @le_S @le_S @le_n806 ]807 cases (member (BitVector 8) ? (\fst ?) ?)808 [1: #destr normalize in destr; destruct(destr)809 2:810 ]811 ]812 3: >get_index_v_eq in ⊢ (??%?)813 change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')814 >(vsplit_vector_singleton … bit_one_three_bit_eq)815 <arg_nu_nl_eq816 whd in hyp:(??%?)817 cases (member (BitVector 8) (eq_bv 8) arg m) in hyp818 normalize nodelta [*: #ignore @sym_eq ]819 ]820 821 ].822 *)823 (*824 map_address0 ... (DIRECT arg) = Some .. →825 get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =826 get_arg_8 (internal_ram ...) (DIRECT arg)827 828 ((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2)829 then Some internal_pseudo_address_map M830 else None internal_pseudo_address_map )831 =Some internal_pseudo_address_map M')832 833 axiom low_internal_ram_write_at_stack_pointer:834 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.835 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.836 get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →837 low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →838 sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →839 sp2 = add ? sp1 (bitvector_of_nat 8 1) →840 bu@@bl = sigma (pbu@@pbl) →841 low_internal_ram T1 cm1842 (write_at_stack_pointer …843 (set_8051_sfr …844 (write_at_stack_pointer …845 (set_8051_sfr …846 (set_low_internal_ram … s1847 (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))848 SFR_SP sp1)849 bl)850 SFR_SP sp2)851 bu)852 = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)853 (low_internal_ram …854 (write_at_stack_pointer …855 (set_8051_sfr …856 (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)857 SFR_SP sp2)858 pbu)).859 860 lemma high_internal_ram_write_at_stack_pointer:861 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.862 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.863 get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →864 high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →865 sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →866 sp2 = add ? sp1 (bitvector_of_nat 8 1) →867 bu@@bl = sigma (pbu@@pbl) →868 high_internal_ram T1 cm1869 (write_at_stack_pointer …870 (set_8051_sfr …871 (write_at_stack_pointer …872 (set_8051_sfr …873 (set_high_internal_ram … s1874 (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))875 SFR_SP sp1)876 bl)877 SFR_SP sp2)878 bu)879 = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)880 (high_internal_ram …881 (write_at_stack_pointer …882 (set_8051_sfr …883 (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)884 SFR_SP sp2)885 pbu)).886 #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2887 #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl888 cases daemon (* XXX: !!! *)889 qed.890 *)891 892 (*CSC: ???*)893 (* XXX: we need a precondition here stating that the PPC is within the894 bounds of the instruction list in order for Jaap's specification to895 apply.896 *)897 lemma snd_assembly_1_pseudoinstruction_ok:898 ∀program: pseudo_assembly_program.899 ∀program_length_proof: \snd program ≤ 2^16.900 ∀sigma: Word → Word.901 ∀policy: Word → bool.902 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.903 ∀ppc: Word.904 ∀ppc_in_bounds: nat_of_bitvector 16 ppc < \snd program.905 ∀pi.906 ∀lookup_labels.907 ∀lookup_datalabels.908 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in909 lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →910 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →911 \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →912 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in913 sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).914 #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi915 #lookup_labels #lookup_datalabels916 @pair_elim #labels #costs #create_label_cost_map_refl917 #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl918 normalize nodelta919 generalize in match fetch_pseudo_refl; fetch_pseudo_refl920 #fetch_pseudo_refl921 letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))922 letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))923 lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)924 @pair_elim #preamble #instr_list #program_refl925 lapply create_label_cost_map_refl; create_label_cost_map_refl926 >program_refl in ⊢ (% → ?); #create_label_cost_map_refl927 >create_label_cost_map_refl928 <eq_pair_fst_snd #H lapply (H (refl …)) H #H929 lapply (H ppc ppc_in_bounds) H930 @pair_elim #pi' #newppc #fetch_pseudo_refl'931 @pair_elim #len #assembled #assembly1_refl #H932 cases H933 #encoding_check_assm #sigma_newppc_refl934 >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'935 >pi_refl' in assembly1_refl; #assembly1_refl936 >lookup_labels_refl >lookup_datalabels_refl937 >program_refl normalize nodelta938 >assembly1_refl939 <sigma_newppc_refl940 generalize in match fetch_pseudo_refl';941 whd in match (fetch_pseudo_instruction ???);942 @pair_elim #lbl #instr #nth_refl normalize nodelta943 #G cases (pair_destruct_right ?????? G) %944 qed.945 946 (* To be moved in ProofStatus *)947 lemma program_counter_set_program_counter:948 ∀T.949 ∀cm.950 ∀s.951 ∀x.952 program_counter T cm (set_program_counter T cm s x) = x.953 //954 199 qed. 955 200 … … 1030 275 *) 1031 276 qed. 277 278 (*CSC: move elsewhere*) 279 lemma flatten_singleton: 280 ∀A,a. flatten A [a] = a. 281 #A #a normalize // 282 qed. 283 284 (*CSC: move elsewhere*) 285 lemma length_flatten_cons: 286 ∀A,hd,tl. 287 flatten A (hd::tl) = hd + flatten A tl. 288 #A #hd #tl normalize // 289 qed. 290 291 lemma tech_transitive_lt_3: 292 ∀n1,n2,n3,b. 293 n1 < b → n2 < b → n3 < b → 294 n1 + n2 + n3 < 3 * b. 295 #n1 #n2 #n3 #b #H1 #H2 #H3 296 @(transitive_lt … (b + n2 + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_l // ] 297 @(transitive_lt … (b + b + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_r // ] 298 @(lt_to_le_to_lt … (b + b + b)) [ @monotonic_lt_plus_r // ] // 299 qed. 300 301 lemma assembly1_pseudoinstruction_lt_2_to_16: 302 ∀lookup_labels,sigma,policy,ppc,lookup_datalabels,pi. 303 \snd (assembly_1_pseudoinstruction 304 lookup_labels sigma policy ppc lookup_datalabels pi) 305 < 2^16. 306 #lookup_labels #sigma #policy #ppc #lookup_datalabels * 307 [ cut (128 < 2^16) [@leb_true_to_le %] #LT 308 * whd in match (assembly_1_pseudoinstruction ??????); 309 whd in match (expand_pseudo_instruction ??????); 310 whd in match assembly_1_pseudoinstruction; normalize nodelta 311 try (#arg1 #arg2 #arg3) try (#arg1 #arg2) try #arg1 312 whd in match (expand_pseudo_instruction ??????); 313 try 314 (change with (flatten ? [assembly1 ?] < ?) 315 >flatten_singleton 316 @(transitive_lt … (assembly1_lt_128 ?)) 317 @LT) 318 @pair_elim #x #y #_ cases x normalize nodelta 319 try 320 (change with (flatten ? [assembly1 ?] < ?) 321 >flatten_singleton 322 @(transitive_lt … (assembly1_lt_128 ?)) 323 @LT) 324 change with (flatten ? [assembly1 ?; assembly1 ?; assembly1 ?] < ?) 325 >length_flatten_cons >length_flatten_cons >length_flatten_cons <plus_n_O 326 <associative_plus @(transitive_lt … (tech_transitive_lt_3 … (2^7) ???)) 327 try @assembly1_lt_128 @leb_true_to_le % 328 2,3: #msg normalize in ⊢ (?%?); // 329  #label whd in match (assembly_1_pseudoinstruction ??????); 330 whd in match (expand_pseudo_instruction ??????); 331 @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_ 332 [2: @pair_elim #x #y #_ cases (?∧?)] 333 normalize in ⊢ (?%?); // 334  #label whd in match (assembly_1_pseudoinstruction ??????); 335 whd in match (expand_pseudo_instruction ??????); 336 @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_ 337 normalize in ⊢ (?%?); // 338  #dptr #id normalize in ⊢ (?%?); // 339 ] 340 qed. 341 342 (*CSC: move elsewhere*) 343 axiom lt_to_lt_nat_of_bitvector_add: 344 ∀n,v,m1,m2. 345 m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 → 346 nat_of_bitvector n (add n v (bitvector_of_nat n m1)) < 347 nat_of_bitvector n (add n v (bitvector_of_nat n m2)). 348 349 (* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *) 350 lemma assembly_ok: 351 ∀program. 352 ∀length_proof: \snd program ≤ 2^16. 353 ∀sigma: Word → Word. 354 ∀policy: Word → bool. 355 ∀sigma_policy_witness: sigma_policy_specification program sigma policy. 356 ∀assembled. 357 ∀costs': BitVectorTrie costlabel 16. 358 let 〈preamble, instr_list〉 ≝ program in 359 let 〈labels, costs〉 ≝ create_label_cost_map instr_list in 360 let datalabels ≝ construct_datalabels preamble in 361 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in 362 〈assembled,costs'〉 = assembly program sigma policy → 363 (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *) 364 let code_memory ≝ load_code_memory assembled in 365 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 366 ∀ppc.∀ppc_ok. 367 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in 368 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in 369 let pc ≝ sigma ppc in 370 let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in 371 encoding_check code_memory pc pc_plus_len assembled ∧ 372 sigma newppc = add … pc (bitvector_of_nat … len). 373 #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs' 374 cases (assembly program sigma policy) * #assembled' #costs'' 375 @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %); 376 cut (instr_list ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok 377 #H lapply (H sigma_policy_witness instr_list_ok) H whd in ⊢ (% → ?); 378 @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %); 379 * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd 380 #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction 381 @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd 382 lapply (assembly_ok2 ppc ?) try // assembly_ok2 383 >eq_fetch_pseudo_instruction 384 change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<assembledi.?) → ?) 385 >eq_assembly_1_pseudoinstruction 386 whd in ⊢ (% → ?); #assembly_ok 387 % 388 [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction)) 389 >snd_fetch_pseudo_instruction 390 cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) H 391 #spw1 #_ >spw1 spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f 392 >eq_fetch_pseudo_instruction whd in match instruction_size; 393 normalize nodelta >create_label_cost_refl 394 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels 395 [>eq_assembly_1_pseudoinstruction %  skip] 396  lapply (load_code_memory_ok assembled' ?) [ assumption ] 397 #load_code_memory_ok 398 lapply (fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) #EQlen 399 (* Nice statement here *) 400 cut (∀j. ∀H: j < assembled. 401 nth_safe Byte j assembled H = 402 \snd (next (load_code_memory assembled') 403 (bitvector_of_nat 16 404 (nat_of_bitvector … 405 (add … (sigma ppc) (bitvector_of_nat … j)))))) 406 [1: #j #H <load_code_memory_ok 407 [ @assembly_ok cases daemon 408  cut (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (assembled))) ≤ assembled') 409 [ 410  #LE @(lt_to_le_to_lt … LE) 411 @lt_to_lt_nat_of_bitvector_add 412 [ @(eq_ind ?? (λp.λ_. \snd p < 2^16) ?? eq_assembly_1_pseudoinstruction) 413 / by / 414  @(transitive_le ???? assembly_ok1) cases daemon 415  assumption 416 ] 417 ] 418 ] 419 2: 420 assembly_ok load_code_memory_ok generalize in match (sigma ppc); >EQlen len 421 elim assembled 422 [1: 423 #pc #_ whd <add_zero % 424  #hd #tl #IH #pc #H % 425 [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); H #H 426 >H H whd in ⊢ (??%?); <add_zero // 427  >(?: add … pc (bitvector_of_nat … (S (tl))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (tl))) 428 [2: <add_bitvector_of_nat_Sm @add_associative ] 429 @IH IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ] 430 <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm 431 >add_associative % ]] 432 ]] 433 qed. 434 435 (* XXX: should we add that costs = costs'? *) 436 lemma fetch_assembly_pseudo2: 437 ∀program. 438 ∀length_proof: \snd program ≤ 2^16. 439 ∀sigma. 440 ∀policy. 441 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 442 ∀ppc.∀ppc_ok. 443 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 444 let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in 445 let code_memory ≝ load_code_memory assembled in 446 let data_labels ≝ construct_datalabels (\fst program) in 447 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 448 let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in 449 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in 450 let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in 451 fetch_many code_memory (sigma newppc) (sigma ppc) instructions. 452 * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok 453 @pair_elim #labels #costs #create_label_map_refl 454 @pair_elim #assembled #costs' #assembled_refl 455 letin code_memory ≝ (load_code_memory ?) 456 letin data_labels ≝ (construct_datalabels ?) 457 letin lookup_labels ≝ (λx. ?) 458 letin lookup_datalabels ≝ (λx. ?) 459 @pair_elim #pi #newppc #fetch_pseudo_refl 460 lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs') 461 normalize nodelta try assumption 462 >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H 463 lapply (H (sym_eq … assembled_refl)) H 464 lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi)) 465 cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?); 466 #len #assembledi #EQ4 #H 467 lapply (H ppc) >fetch_pseudo_refl #H 468 lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy) 469 >create_label_map_refl #X lapply (X ppc ppc_ok (load_code_memory assembled)) X 470 >EQ4 #H1 cases (H ppc_ok) 471 #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta 472 >fetch_pseudo_refl in H1; #assm @assm assumption 473 qed. 474 475 (* XXX: changed this type. Bool specifies whether byte is first or second 476 component of an address, and the Word is the pseudoaddress that it 477 corresponds to. Second component is the same principle for the accumulator 478 A. 479 *) 480 definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)). 481 482 include alias "ASM/BitVectorTrie.ma". 483 484 include "common/AssocList.ma". 485 486 axiom low_internal_ram_of_pseudo_low_internal_ram: 487 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7. 488 489 axiom high_internal_ram_of_pseudo_high_internal_ram: 490 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7. 491 492 axiom low_internal_ram_of_pseudo_internal_ram_hit: 493 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7. 494 assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉) → 495 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 496 let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in 497 let bl ≝ lookup ? 7 addr ram (zero 8) in 498 let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in 499 let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in 500 if high then 501 (pbl = higher) ∧ (bl = phigher) 502 else 503 (pbl = lower) ∧ (bl = plower). 504 505 (* changed from add to sub *) 506 axiom low_internal_ram_of_pseudo_internal_ram_miss: 507 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7. 508 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 509 assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false → 510 lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?). 511 512 definition addressing_mode_ok ≝ 513 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm. 514 λaddr:addressing_mode. 515 match addr with 516 [ DIRECT d ⇒ 517 ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧ 518 ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M)) 519  INDIRECT i ⇒ 520 let d ≝ get_register … s [[false;false;i]] in 521 ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧ 522 ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M)) 523  EXT_INDIRECT _ ⇒ true 524  REGISTER _ ⇒ true 525  ACC_A ⇒ match \snd M with [ None ⇒ true  _ ⇒ false ] 526  ACC_B ⇒ true 527  DPTR ⇒ true 528  DATA _ ⇒ true 529  DATA16 _ ⇒ true 530  ACC_DPTR ⇒ true 531  ACC_PC ⇒ true 532  EXT_INDIRECT_DPTR ⇒ true 533  INDIRECT_DPTR ⇒ true 534  CARRY ⇒ true 535  BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *) 536  N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *) 537  RELATIVE _ ⇒ true 538  ADDR11 _ ⇒ true 539  ADDR16 _ ⇒ true ]. 540 541 definition next_internal_pseudo_address_map0 ≝ 542 λT. 543 λcm:T. 544 λaddr_of: Identifier → PreStatus T cm → Word. 545 λfetched. 546 λM: internal_pseudo_address_map. 547 λs: PreStatus T cm. 548 match fetched with 549 [ Comment _ ⇒ Some ? M 550  Cost _ ⇒ Some … M 551  Jmp _ ⇒ Some … M 552  Call a ⇒ 553 let a' ≝ addr_of a s in 554 let 〈callM, accM〉 ≝ M in 555 Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉:: 556 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉 557  Mov _ _ ⇒ Some … M 558  Instruction instr ⇒ 559 match instr with 560 [ ADD addr1 addr2 ⇒ 561 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 562 Some ? M 563 else 564 None ? 565  ADDC addr1 addr2 ⇒ 566 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 567 Some ? M 568 else 569 None ? 570  SUBB addr1 addr2 ⇒ 571 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 572 Some ? M 573 else 574 None ? 575  _ ⇒ (* TO BE COMPLETED *) Some ? M ]]. 576 577 definition next_internal_pseudo_address_map ≝ 578 λM:internal_pseudo_address_map. 579 λcm. 580 λaddr_of. 581 λs:PseudoStatus cm. 582 λppc_ok. 583 next_internal_pseudo_address_map0 ? cm addr_of 584 (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s. 585 586 definition code_memory_of_pseudo_assembly_program: 587 ∀pap:pseudo_assembly_program. 588 (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝ 589 λpap. 590 λsigma. 591 λpolicy. 592 let p ≝ pi1 … (assembly pap sigma policy) in 593 load_code_memory (\fst p). 594 595 definition sfr_8051_of_pseudo_sfr_8051 ≝ 596 λM: internal_pseudo_address_map. 597 λsfrs: Vector Byte 19. 598 λsigma: Word → Word. 599 match \snd M with 600 [ None ⇒ sfrs 601  Some s ⇒ 602 let 〈high, address〉 ≝ s in 603 let index ≝ sfr_8051_index SFR_ACC_A in 604 let 〈upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in 605 if high then 606 set_index Byte 19 sfrs index upper ? 607 else 608 set_index Byte 19 sfrs index lower ? 609 ]. 610 // 611 qed. 612 613 definition status_of_pseudo_status: 614 internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap. 615 ∀sigma: Word → Word. ∀policy: Word → bool. 616 Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝ 617 λM. 618 λpap. 619 λps. 620 λsigma. 621 λpolicy. 622 let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in 623 let pc ≝ sigma (program_counter … ps) in 624 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in 625 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in 626 mk_PreStatus (BitVectorTrie Byte 16) 627 cm 628 lir 629 hir 630 (external_ram … ps) 631 pc 632 (special_function_registers_8051 … ps) 633 (special_function_registers_8052 … ps) 634 (p1_latch … ps) 635 (p3_latch … ps) 636 (clock … ps). 637 638 (* 639 definition write_at_stack_pointer': 640 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝ 641 λM: Type[0]. 642 λs: PreStatus M. 643 λv: Byte. 644 let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in 645 let bit_zero ≝ get_index_v… nu O ? in 646 let bit_1 ≝ get_index_v… nu 1 ? in 647 let bit_2 ≝ get_index_v… nu 2 ? in 648 let bit_3 ≝ get_index_v… nu 3 ? in 649 if bit_zero then 650 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 651 v (low_internal_ram ? s) in 652 set_low_internal_ram ? s memory 653 else 654 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 655 v (high_internal_ram ? s) in 656 set_high_internal_ram ? s memory. 657 [ cases l0 % 658 2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ] 659 qed. 660 661 definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus. 662 Σps':PseudoStatus.(code_memory … ps = code_memory … ps') 663 ≝ 664 λticks_of. 665 λs. 666 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in 667 let ticks ≝ ticks_of (program_counter ? s) in 668 let s ≝ set_clock ? s (clock ? s + ticks) in 669 let s ≝ set_program_counter ? s pc in 670 match instr with 671 [ Instruction instr ⇒ 672 execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s 673  Comment cmt ⇒ s 674  Cost cst ⇒ s 675  Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp) 676  Call call ⇒ 677 let a ≝ address_of_word_labels s call in 678 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 679 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 680 let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in 681 let s ≝ write_at_stack_pointer' ? s pc_bl in 682 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 683 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 684 let s ≝ write_at_stack_pointer' ? s pc_bu in 685 set_program_counter ? s a 686  Mov dptr ident ⇒ 687 set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr 688 ]. 689 [ 690 2,3,4: % 691  <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) % 692  693  % 694 ] 695 cases not_implemented 696 qed. 697 *) 698 699 (* 700 lemma execute_code_memory_unchanged: 701 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps). 702 #ticks #ps whd in ⊢ (??? (??%)) 703 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps)) 704 (program_counter pseudo_assembly_program ps)) #instr #pc 705 whd in ⊢ (??? (??%)) cases instr 706 [ #pre cases pre 707 [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%)) 708 cases (vsplit ????) #z1 #z2 % 709  #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%)) 710 cases (vsplit ????) #z1 #z2 % 711  #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%)) 712 cases (vsplit ????) #z1 #z2 % 713  #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x 714 [ #x1 whd in ⊢ (??? (??%)) 715  *: cases not_implemented 716 ] 717  #comment % 718  #cost % 719  #label % 720  #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%)) 721 cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2 722 whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2 723 whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%)) 724 (* CSC: ??? *) 725  #dptr #label (* CSC: ??? *) 726 ] 727 cases not_implemented 728 qed. 729 *) 730 731 (* DEAD CODE? 732 lemma status_of_pseudo_status_failure_depends_only_on_code_memory: 733 ∀M:internal_pseudo_address_map. 734 ∀ps,ps': PseudoStatus. 735 ∀pol. 736 ∀prf:code_memory … ps = code_memory … ps'. 737 let pol' ≝ ? in 738 match status_of_pseudo_status M ps pol with 739 [ None ⇒ status_of_pseudo_status M ps' pol' = None … 740  Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w 741 ]. 742 [2: <prf @pol] 743 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]) 744 generalize in match (refl … (assembly (code_memory … ps) pol)) 745 cases (assembly ??) in ⊢ (???% → %) 746 [ #K whd whd in ⊢ (??%?) <H >K % 747  #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ] 748 qed. 749 *) 750 751 definition ticks_of0: 752 ∀p:pseudo_assembly_program. 753 (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝ 754 λprogram: pseudo_assembly_program. 755 λsigma. 756 λpolicy. 757 λppc: Word. 758 λfetched. 759 match fetched with 760 [ Instruction instr ⇒ 761 match instr with 762 [ JC lbl ⇒ ? (* 763 match pol lookup_labels ppc with 764 [ short_jump ⇒ 〈2, 2〉 765  absolute_jump ⇒ ? 766  long_jump ⇒ 〈4, 4〉 767 ] *) 768  JNC lbl ⇒ ? (* 769 match pol lookup_labels ppc with 770 [ short_jump ⇒ 〈2, 2〉 771  absolute_jump ⇒ ? 772  long_jump ⇒ 〈4, 4〉 773 ] *) 774  JB bit lbl ⇒ ? (* 775 match pol lookup_labels ppc with 776 [ short_jump ⇒ 〈2, 2〉 777  absolute_jump ⇒ ? 778  long_jump ⇒ 〈4, 4〉 779 ] *) 780  JNB bit lbl ⇒ ? (* 781 match pol lookup_labels ppc with 782 [ short_jump ⇒ 〈2, 2〉 783  absolute_jump ⇒ ? 784  long_jump ⇒ 〈4, 4〉 785 ] *) 786  JBC bit lbl ⇒ ? (* 787 match pol lookup_labels ppc with 788 [ short_jump ⇒ 〈2, 2〉 789  absolute_jump ⇒ ? 790  long_jump ⇒ 〈4, 4〉 791 ] *) 792  JZ lbl ⇒ ? (* 793 match pol lookup_labels ppc with 794 [ short_jump ⇒ 〈2, 2〉 795  absolute_jump ⇒ ? 796  long_jump ⇒ 〈4, 4〉 797 ] *) 798  JNZ lbl ⇒ ? (* 799 match pol lookup_labels ppc with 800 [ short_jump ⇒ 〈2, 2〉 801  absolute_jump ⇒ ? 802  long_jump ⇒ 〈4, 4〉 803 ] *) 804  CJNE arg lbl ⇒ ? (* 805 match pol lookup_labels ppc with 806 [ short_jump ⇒ 〈2, 2〉 807  absolute_jump ⇒ ? 808  long_jump ⇒ 〈4, 4〉 809 ] *) 810  DJNZ arg lbl ⇒ ? (* 811 match pol lookup_labels ppc with 812 [ short_jump ⇒ 〈2, 2〉 813  absolute_jump ⇒ ? 814  long_jump ⇒ 〈4, 4〉 815 ] *) 816  ADD arg1 arg2 ⇒ 817 let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in 818 〈ticks, ticks〉 819  ADDC arg1 arg2 ⇒ 820 let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in 821 〈ticks, ticks〉 822  SUBB arg1 arg2 ⇒ 823 let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in 824 〈ticks, ticks〉 825  INC arg ⇒ 826 let ticks ≝ ticks_of_instruction (INC ? arg) in 827 〈ticks, ticks〉 828  DEC arg ⇒ 829 let ticks ≝ ticks_of_instruction (DEC ? arg) in 830 〈ticks, ticks〉 831  MUL arg1 arg2 ⇒ 832 let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in 833 〈ticks, ticks〉 834  DIV arg1 arg2 ⇒ 835 let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in 836 〈ticks, ticks〉 837  DA arg ⇒ 838 let ticks ≝ ticks_of_instruction (DA ? arg) in 839 〈ticks, ticks〉 840  ANL arg ⇒ 841 let ticks ≝ ticks_of_instruction (ANL ? arg) in 842 〈ticks, ticks〉 843  ORL arg ⇒ 844 let ticks ≝ ticks_of_instruction (ORL ? arg) in 845 〈ticks, ticks〉 846  XRL arg ⇒ 847 let ticks ≝ ticks_of_instruction (XRL ? arg) in 848 〈ticks, ticks〉 849  CLR arg ⇒ 850 let ticks ≝ ticks_of_instruction (CLR ? arg) in 851 〈ticks, ticks〉 852  CPL arg ⇒ 853 let ticks ≝ ticks_of_instruction (CPL ? arg) in 854 〈ticks, ticks〉 855  RL arg ⇒ 856 let ticks ≝ ticks_of_instruction (RL ? arg) in 857 〈ticks, ticks〉 858  RLC arg ⇒ 859 let ticks ≝ ticks_of_instruction (RLC ? arg) in 860 〈ticks, ticks〉 861  RR arg ⇒ 862 let ticks ≝ ticks_of_instruction (RR ? arg) in 863 〈ticks, ticks〉 864  RRC arg ⇒ 865 let ticks ≝ ticks_of_instruction (RRC ? arg) in 866 〈ticks, ticks〉 867  SWAP arg ⇒ 868 let ticks ≝ ticks_of_instruction (SWAP ? arg) in 869 〈ticks, ticks〉 870  MOV arg ⇒ 871 let ticks ≝ ticks_of_instruction (MOV ? arg) in 872 〈ticks, ticks〉 873  MOVX arg ⇒ 874 let ticks ≝ ticks_of_instruction (MOVX ? arg) in 875 〈ticks, ticks〉 876  SETB arg ⇒ 877 let ticks ≝ ticks_of_instruction (SETB ? arg) in 878 〈ticks, ticks〉 879  PUSH arg ⇒ 880 let ticks ≝ ticks_of_instruction (PUSH ? arg) in 881 〈ticks, ticks〉 882  POP arg ⇒ 883 let ticks ≝ ticks_of_instruction (POP ? arg) in 884 〈ticks, ticks〉 885  XCH arg1 arg2 ⇒ 886 let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in 887 〈ticks, ticks〉 888  XCHD arg1 arg2 ⇒ 889 let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in 890 〈ticks, ticks〉 891  RET ⇒ 892 let ticks ≝ ticks_of_instruction (RET ?) in 893 〈ticks, ticks〉 894  RETI ⇒ 895 let ticks ≝ ticks_of_instruction (RETI ?) in 896 〈ticks, ticks〉 897  NOP ⇒ 898 let ticks ≝ ticks_of_instruction (NOP ?) in 899 〈ticks, ticks〉 900 ] 901  Comment comment ⇒ 〈0, 0〉 902  Cost cost ⇒ 〈0, 0〉 903  Jmp jmp ⇒ 〈2, 2〉 904  Call call ⇒ 〈2, 2〉 905  Mov dptr tgt ⇒ 〈2, 2〉 906 ]. 907 cases daemon 908 qed. 909 910 definition ticks_of: 911 ∀p:pseudo_assembly_program. 912 (Word → Word) → (Word → bool) → ∀ppc:Word. 913 nat_of_bitvector … ppc < \snd p → nat × nat ≝ 914 λprogram: pseudo_assembly_program. 915 λsigma. 916 λpolicy. 917 λppc: Word. λppc_ok. 918 let pseudo ≝ \snd program in 919 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in 920 ticks_of0 program sigma policy ppc fetched. 921 922 (* 923 lemma blah: 924 ∀m: internal_pseudo_address_map. 925 ∀s: PseudoStatus. 926 ∀arg: Byte. 927 ∀b: bool. 928 addressing_mode_ok m s (DIRECT arg) = true → 929 get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) = 930 get_arg_8 ? s b (DIRECT arg). 931 [2, 3: normalize % ] 932 #m #s #arg #b #hyp 933 whd in ⊢ (??%%) 934 @vsplit_elim'' 935 #nu' #nl' #arg_nu_nl_eq 936 normalize nodelta 937 generalize in match (refl ? (get_index_v bool 4 nu' ? ?)) 938 cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %) 939 #get_index_v_eq 940 normalize nodelta 941 [2: 942 normalize nodelta 943 @vsplit_elim'' 944 #bit_one' #three_bits' #bit_one_three_bit_eq 945 generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl')) 946 normalize nodelta 947 generalize in match (refl ? (sub_7_with_carry ? ? ?)) 948 cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %) 949 #Saddr #carr' #Saddr_carr_eq 950 normalize nodelta 951 #carr_hyp' 952 @carr_hyp' 953 [1: 954 2: whd in hyp:(??%?); generalize in match hyp; hyp; 955 generalize in match (refl ? (¬(member (BitVector 8) ? arg m))) 956 cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %) 957 #member_eq 958 normalize nodelta 959 [2: #destr destruct(destr) 960 1: carr_hyp'; 961 >arg_nu_nl_eq 962 <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq) 963 [1: >get_index_v_eq in ⊢ (??%? → ?) 964 2: @le_S @le_S @le_S @le_n 965 ] 966 cases (member (BitVector 8) ? (\fst ?) ?) 967 [1: #destr normalize in destr; destruct(destr) 968 2: 969 ] 970 ] 971 3: >get_index_v_eq in ⊢ (??%?) 972 change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl') 973 >(vsplit_vector_singleton … bit_one_three_bit_eq) 974 <arg_nu_nl_eq 975 whd in hyp:(??%?) 976 cases (member (BitVector 8) (eq_bv 8) arg m) in hyp 977 normalize nodelta [*: #ignore @sym_eq ] 978 ] 979  980 ]. 981 *) 982 (* 983 map_address0 ... (DIRECT arg) = Some .. → 984 get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) = 985 get_arg_8 (internal_ram ...) (DIRECT arg) 986 987 ((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 988 then Some internal_pseudo_address_map M 989 else None internal_pseudo_address_map ) 990 =Some internal_pseudo_address_map M') 991 992 axiom low_internal_ram_write_at_stack_pointer: 993 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool. 994 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 995 get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP → 996 low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 → 997 sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) → 998 sp2 = add ? sp1 (bitvector_of_nat 8 1) → 999 bu@@bl = sigma (pbu@@pbl) → 1000 low_internal_ram T1 cm1 1001 (write_at_stack_pointer … 1002 (set_8051_sfr … 1003 (write_at_stack_pointer … 1004 (set_8051_sfr … 1005 (set_low_internal_ram … s1 1006 (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2))) 1007 SFR_SP sp1) 1008 bl) 1009 SFR_SP sp2) 1010 bu) 1011 = low_internal_ram_of_pseudo_low_internal_ram (sp1::M) 1012 (low_internal_ram … 1013 (write_at_stack_pointer … 1014 (set_8051_sfr … 1015 (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl) 1016 SFR_SP sp2) 1017 pbu)). 1018 1019 lemma high_internal_ram_write_at_stack_pointer: 1020 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool. 1021 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 1022 get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP → 1023 high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 → 1024 sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) → 1025 sp2 = add ? sp1 (bitvector_of_nat 8 1) → 1026 bu@@bl = sigma (pbu@@pbl) → 1027 high_internal_ram T1 cm1 1028 (write_at_stack_pointer … 1029 (set_8051_sfr … 1030 (write_at_stack_pointer … 1031 (set_8051_sfr … 1032 (set_high_internal_ram … s1 1033 (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2))) 1034 SFR_SP sp1) 1035 bl) 1036 SFR_SP sp2) 1037 bu) 1038 = high_internal_ram_of_pseudo_high_internal_ram (sp1::M) 1039 (high_internal_ram … 1040 (write_at_stack_pointer … 1041 (set_8051_sfr … 1042 (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl) 1043 SFR_SP sp2) 1044 pbu)). 1045 #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2 1046 #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl 1047 cases daemon (* XXX: !!! *) 1048 qed. 1049 *) 1050 1051 (*CSC: ???*) 1052 (* XXX: we need a precondition here stating that the PPC is within the 1053 bounds of the instruction list in order for Jaap's specification to 1054 apply. 1055 *) 1056 lemma snd_assembly_1_pseudoinstruction_ok: 1057 ∀program: pseudo_assembly_program. 1058 ∀program_length_proof: \snd program ≤ 2^16. 1059 ∀sigma: Word → Word. 1060 ∀policy: Word → bool. 1061 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 1062 ∀ppc: Word. 1063 ∀ppc_in_bounds: nat_of_bitvector 16 ppc < \snd program. 1064 ∀pi. 1065 ∀lookup_labels. 1066 ∀lookup_datalabels. 1067 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 1068 lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) → 1069 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 1070 \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi → 1071 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in 1072 sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len). 1073 #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi 1074 #lookup_labels #lookup_datalabels 1075 @pair_elim #labels #costs #create_label_cost_map_refl 1076 #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl 1077 normalize nodelta 1078 generalize in match fetch_pseudo_refl; fetch_pseudo_refl 1079 #fetch_pseudo_refl 1080 letin assembled ≝ (\fst (pi1 … (assembly program sigma policy))) 1081 letin costs ≝ (\snd (pi1 … (assembly program sigma policy))) 1082 lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs) 1083 @pair_elim #preamble #instr_list #program_refl 1084 lapply create_label_cost_map_refl; create_label_cost_map_refl 1085 >program_refl in ⊢ (% → ?); #create_label_cost_map_refl 1086 >create_label_cost_map_refl 1087 <eq_pair_fst_snd #H lapply (H (refl …)) H #H 1088 lapply (H ppc ppc_in_bounds) H 1089 @pair_elim #pi' #newppc #fetch_pseudo_refl' 1090 @pair_elim #len #assembled #assembly1_refl #H 1091 cases H 1092 #encoding_check_assm #sigma_newppc_refl 1093 >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl' 1094 >pi_refl' in assembly1_refl; #assembly1_refl 1095 >lookup_labels_refl >lookup_datalabels_refl 1096 >program_refl normalize nodelta 1097 >assembly1_refl 1098 <sigma_newppc_refl 1099 generalize in match fetch_pseudo_refl'; 1100 whd in match (fetch_pseudo_instruction ???); 1101 @pair_elim #lbl #instr #nth_refl normalize nodelta 1102 #G cases (pair_destruct_right ?????? G) % 1103 qed. 1104 1105 (* To be moved in ProofStatus *) 1106 lemma program_counter_set_program_counter: 1107 ∀T. 1108 ∀cm. 1109 ∀s. 1110 ∀x. 1111 program_counter T cm (set_program_counter T cm s x) = x. 1112 // 1113 qed.
Note: See TracChangeset
for help on using the changeset viewer.