Changeset 1971 for src/ASM

Ignore:
Timestamp:
May 20, 2012, 10:34:31 PM (8 years ago)
Message:
1. Interpret.ma: we need to prove \sigma (execute_preinstruction s) = execute_preinstruction (\sigma s)

Thus execute_preinstruction cannot be defined using Russell.
Changed, but the proof of the properties still uses Russell
(with a trick...)

1. AssemblyProofSplit?: the preinstruction case of the main theorem moved to a main lemma which is also proved using the Russell trick. This seems very promising ATM.
Location:
src/ASM
Files:
2 edited

Unmodified
Added
Removed
• src/ASM/AssemblyProofSplit.ma

 r1969 #P #A #a #abs destruct qed. (* lemma pi1_let_commute: ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c. pi1 … (let 〈x1,y1〉 ≝ c in t) = (let 〈x1,y1〉 ≝ c in pi1 … t). #A #B #C #P * #a #b * // qed. lemma pi1_let_as_commute: ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c. pi1 … (let 〈x1,y1〉 as H ≝ c in t) = (let 〈x1,y1〉 as H ≝ c in pi1 … t). #A #B #C #P * #a #b * // qed. *) lemma tech_pi1_let_as_commute: ∀A,B,C,P. ∀f. ∀c,c':A × B. ∀t: ∀a,b. 〈a,b〉=c → Σc:C.P c. ∀t': ∀a,b. 〈a,b〉=c' → Σc:C.P c. c=c' → (∀x,y,H,H'.t x y H = f (pi1 … (t' x y H'))) → pi1 … (let 〈x1,y1〉 as H ≝ c in t x1 y1 H) = f (pi1 … (let 〈x1,y1〉 as H ≝ c' in t' x1 y1 H)). #A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/ qed. include alias "arithmetics/nat.ma". include alias "basics/logic.ma". include alias "ASM/BitVectorTrie.ma". lemma pair_replace: ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c=c' → c ≃ 〈a,b〉 → P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b'). #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct // qed. lemma main_lemma_preinstruction: ∀M,M': internal_pseudo_address_map. ∀preamble : preamble. ∀instr_list : list labelled_instruction. ∀cm: pseudo_assembly_program. ∀EQcm: cm = 〈preamble,instr_list〉. ∀sigma : Word→Word. ∀policy : Word→bool. ∀sigma_policy_witness : sigma_policy_specification cm sigma policy. ∀ps : PseudoStatus cm. ∀ppc : Word. ∀EQppc : ppc=program_counter pseudo_assembly_program cm ps. ∀labels : label_map. ∀costs : BitVectorTrie costlabel 16. ∀create_label_cost_refl : create_label_cost_map instr_list=〈labels,costs〉. ∀assembled : list Byte. ∀costs' : BitVectorTrie costlabel 16. ∀assembly_refl : assembly 〈preamble,instr_list〉 sigma policy=〈assembled,costs'〉. ∀EQassembled : assembled=\fst  (assembly cm sigma policy). ∀newppc : Word. ∀lookup_labels : Identifier→Word. ∀EQlookup_labels : lookup_labels = (λx:Identifier.sigma (address_of_word_labels_code_mem instr_list x)). ∀lookup_datalabels : identifier ASMTag→Word. ∀ EQlookup_datalabels : lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)). ∀EQnewppc : newppc=add 16 ppc (bitvector_of_nat 16 1). ∀instr: preinstruction Identifier. ∀ticks. ∀EQticks: ticks = ticks_of0 〈preamble,instr_list〉 sigma policy ppc (Instruction instr). ∀addr_of. ∀EQaddr_of: addr_of = (λx:Identifier .λy:PreStatus pseudo_assembly_program cm .address_of_word_labels cm x). ∀s. ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))). ∀P. ∀EQP: P = (λs. ∃n:ℕ .execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =status_of_pseudo_status M' cm s sigma policy). sigma (add 16 ppc (bitvector_of_nat 16 1)) =add 16 (sigma ppc) (bitvector_of_nat 16 (\fst  (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels (Instruction instr)))) →next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cm ps =Some internal_pseudo_address_map M' →fetch_many (load_code_memory assembled) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma ppc) (expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels (Instruction instr)) →P (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s). #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels #costs #create_label_cost_refl #assembled #costs' #assembly_refl #EQassembled #newppc #lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP #sigma_increment_commutation #maps_assm #fetch_many_assm letin a ≝ Identifier letin m ≝ pseudo_assembly_program cut (Σxxx:PseudoStatus cm. P (execute_1_preinstruction ticks a m cm addr_of instr s)) [2: * // ] @( let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in match instr in preinstruction return λx. x = instr → Σs'.? with [ ADD addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) (get_arg_8 … s false addr2) false in let cy_flag ≝ get_index' ? O  ? flags in let ac_flag ≝ get_index' ? 1 ? flags in let ov_flag ≝ get_index' ? 2 ? flags in let s ≝ set_arg_8 … s ACC_A result in set_flags … s cy_flag (Some Bit ac_flag) ov_flag | ADDC addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let old_cy_flag ≝ get_cy_flag ?? s in let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) (get_arg_8 … s false addr2) old_cy_flag in let cy_flag ≝ get_index' ? O ? flags in let ac_flag ≝ get_index' ? 1 ? flags in let ov_flag ≝ get_index' ? 2 ? flags in let s ≝ set_arg_8 … s ACC_A result in set_flags … s cy_flag (Some Bit ac_flag) ov_flag | SUBB addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let old_cy_flag ≝ get_cy_flag ?? s in let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1) (get_arg_8 … s false addr2) old_cy_flag in let cy_flag ≝ get_index' ? O ? flags in let ac_flag ≝ get_index' ? 1 ? flags in let ov_flag ≝ get_index' ? 2 ? flags in let s ≝ set_arg_8 … s ACC_A result in set_flags … s cy_flag (Some Bit ac_flag) ov_flag | ANL addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in match addr with [ inl l ⇒ match l with [ inl l' ⇒ let 〈addr1, addr2〉 ≝ l' in let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in set_arg_8 … s addr1 and_val | inr r ⇒ let 〈addr1, addr2〉 ≝ r in let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in set_arg_8 … s addr1 and_val ] | inr r ⇒ let 〈addr1, addr2〉 ≝ r in let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in set_flags … s and_val (None ?) (get_ov_flag ?? s) ] | ORL addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in match addr with [ inl l ⇒ match l with [ inl l' ⇒ let 〈addr1, addr2〉 ≝ l' in let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in set_arg_8 … s addr1 or_val | inr r ⇒ let 〈addr1, addr2〉 ≝ r in let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in set_arg_8 … s addr1 or_val ] | inr r ⇒ let 〈addr1, addr2〉 ≝ r in let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in set_flags … s or_val (None ?) (get_ov_flag … s) ] | XRL addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in match addr with [ inl l' ⇒ let 〈addr1, addr2〉 ≝ l' in let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in set_arg_8 … s addr1 xor_val | inr r ⇒ let 〈addr1, addr2〉 ≝ r in let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in set_arg_8 … s addr1 xor_val ] | INC addr ⇒ λinstr_refl. match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with [ ACC_A ⇒ λacc_a: True. let s' ≝ add_ticks1 s in let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in set_arg_8 … s' ACC_A result | REGISTER r ⇒ λregister: True. let s' ≝ add_ticks1 s in let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in set_arg_8 … s' (REGISTER r) result | DIRECT d ⇒ λdirect: True. let s' ≝ add_ticks1 s in let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in set_arg_8 … s' (DIRECT d) result | INDIRECT i ⇒ λindirect: True. let s' ≝ add_ticks1 s in let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in set_arg_8 … s' (INDIRECT i) result | DPTR ⇒ λdptr: True. let s' ≝ add_ticks1 s in let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in let s ≝ set_8051_sfr … s' SFR_DPL bl in set_8051_sfr … s' SFR_DPH bu | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … addr) | NOP ⇒ λinstr_refl. let s ≝ add_ticks2 s in s | DEC addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in set_arg_8 … s addr result | MUL addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in let product ≝ acc_a_nat * acc_b_nat in let ov_flag ≝ product ≥ 256 in let low ≝ bitvector_of_nat 8 (product mod 256) in let high ≝ bitvector_of_nat 8 (product ÷ 256) in let s ≝ set_8051_sfr … s SFR_ACC_A low in set_8051_sfr … s SFR_ACC_B high | DIV addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in match acc_b_nat with [ O ⇒ set_flags … s false (None Bit) true | S o ⇒ let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in let s ≝ set_8051_sfr … s SFR_ACC_A q in let s ≝ set_8051_sfr … s SFR_ACC_B r in set_flags … s false (None Bit) false ] | DA addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in let cy_flag ≝ get_index' ? O ? flags in let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in let new_acc ≝ nu @@ acc_nl' in let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s) else s else s | CLR addr ⇒ λinstr_refl. match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with [ ACC_A ⇒ λacc_a: True. let s ≝ add_ticks1 s in set_arg_8 … s ACC_A (zero 8) | CARRY ⇒ λcarry: True. let s ≝ add_ticks1 s in set_arg_1 … s CARRY false | BIT_ADDR b ⇒ λbit_addr: True. let s ≝ add_ticks1 s in set_arg_1 … s (BIT_ADDR b) false | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … addr) | CPL addr ⇒ λinstr_refl. match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with [ ACC_A ⇒ λacc_a: True. let s ≝ add_ticks1 s in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let new_acc ≝ negation_bv ? old_acc in set_8051_sfr … s SFR_ACC_A new_acc | CARRY ⇒ λcarry: True. let s ≝ add_ticks1 s in let old_cy_flag ≝ get_arg_1 … s CARRY true in let new_cy_flag ≝ ¬old_cy_flag in set_arg_1 … s CARRY new_cy_flag | BIT_ADDR b ⇒ λbit_addr: True. let s ≝ add_ticks1 s in let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in let new_bit ≝ ¬old_bit in set_arg_1 … s (BIT_ADDR b) new_bit | _ ⇒ λother: False. ? ] (subaddressing_modein … addr) | SETB b ⇒ λinstr_refl. let s ≝ add_ticks1 s in set_arg_1 … s b false | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *) let s ≝ add_ticks1 s in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let new_acc ≝ rotate_left … 1 old_acc in set_8051_sfr … s SFR_ACC_A new_acc | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *) let s ≝ add_ticks1 s in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let new_acc ≝ rotate_right … 1 old_acc in set_8051_sfr … s SFR_ACC_A new_acc | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) let s ≝ add_ticks1 s in let old_cy_flag ≝ get_cy_flag ?? s in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let new_cy_flag ≝ get_index' ? O ? old_acc in let new_acc ≝ shift_left … 1 old_acc old_cy_flag in let s ≝ set_arg_1 … s CARRY new_cy_flag in set_8051_sfr … s SFR_ACC_A new_acc | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) let s ≝ add_ticks1 s in let old_cy_flag ≝ get_cy_flag ?? s in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let new_cy_flag ≝ get_index' ? 7 ? old_acc in let new_acc ≝ shift_right … 1 old_acc old_cy_flag in let s ≝ set_arg_1 … s CARRY new_cy_flag in set_8051_sfr … s SFR_ACC_A new_acc | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *) let s ≝ add_ticks1 s in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let 〈nu,nl〉 ≝ split ? 4 4 old_acc in let new_acc ≝ nl @@ nu in set_8051_sfr … s SFR_ACC_A new_acc | PUSH addr ⇒ λinstr_refl. match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with [ DIRECT d ⇒ λdirect: True. let s ≝ add_ticks1 s in let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in let s ≝ set_8051_sfr … s SFR_SP new_sp in write_at_stack_pointer … s d | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … addr) | POP addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in let contents ≝ read_at_stack_pointer ?? s in let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in let s ≝ set_8051_sfr … s SFR_SP new_sp in set_arg_8 … s addr contents | XCH addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let old_addr ≝ get_arg_8 … s false addr2 in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in set_arg_8 … s addr2 old_acc | XCHD addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in let new_acc ≝ acc_nu @@ arg_nl in let new_arg ≝ arg_nu @@ acc_nl in let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in set_arg_8 … s addr2 new_arg | RET ⇒ λinstr_refl. let s ≝ add_ticks1 s in let high_bits ≝ read_at_stack_pointer ?? s in let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in let s ≝ set_8051_sfr … s SFR_SP new_sp in let low_bits ≝ read_at_stack_pointer ?? s in let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in let s ≝ set_8051_sfr … s SFR_SP new_sp in let new_pc ≝ high_bits @@ low_bits in set_program_counter … s new_pc | RETI ⇒ λinstr_refl. let s ≝ add_ticks1 s in let high_bits ≝ read_at_stack_pointer ?? s in let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in let s ≝ set_8051_sfr … s SFR_SP new_sp in let low_bits ≝ read_at_stack_pointer ?? s in let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in let s ≝ set_8051_sfr … s SFR_SP new_sp in let new_pc ≝ high_bits @@ low_bits in set_program_counter … s new_pc | MOVX addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in (* DPM: only copies --- doesn't affect I/O *) match addr with [ inl l ⇒ let 〈addr1, addr2〉 ≝ l in set_arg_8 … s addr1 (get_arg_8 … s false addr2) | inr r ⇒ let 〈addr1, addr2〉 ≝ r in set_arg_8 … s addr1 (get_arg_8 … s false addr2) ] | MOV addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in match addr with [ inl l ⇒ match l with [ inl l' ⇒ match l' with [ inl l'' ⇒ match l'' with [ inl l''' ⇒ match l''' with [ inl l'''' ⇒ let 〈addr1, addr2〉 ≝ l'''' in set_arg_8 … s addr1 (get_arg_8 … s false addr2) | inr r'''' ⇒ let 〈addr1, addr2〉 ≝ r'''' in set_arg_8 … s addr1 (get_arg_8 … s false addr2) ] | inr r''' ⇒ let 〈addr1, addr2〉 ≝ r''' in set_arg_8 … s addr1 (get_arg_8 … s false addr2) ] | inr r'' ⇒ let 〈addr1, addr2〉 ≝ r'' in set_arg_16 … s (get_arg_16 … s addr2) addr1 ] | inr r ⇒ let 〈addr1, addr2〉 ≝ r in set_arg_1 … s addr1 (get_arg_1 … s addr2 false) ] | inr r ⇒ let 〈addr1, addr2〉 ≝ r in set_arg_1 … s addr1 (get_arg_1 … s addr2 false) ] | JC addr ⇒ λinstr_refl. if get_cy_flag ?? s then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr s) else let s ≝ add_ticks2 s in s | JNC addr ⇒ λinstr_refl. if ¬(get_cy_flag ?? s) then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr s) else let s ≝ add_ticks2 s in s | JB addr1 addr2 ⇒ λinstr_refl. if get_arg_1 … s addr1 false then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr2 s) else let s ≝ add_ticks2 s in s | JNB addr1 addr2 ⇒ λinstr_refl. if ¬(get_arg_1 … s addr1 false) then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr2 s) else let s ≝ add_ticks2 s in s | JBC addr1 addr2 ⇒ λinstr_refl. let s ≝ set_arg_1 … s addr1 false in if get_arg_1 … s addr1 false then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr2 s) else let s ≝ add_ticks2 s in s | JZ addr ⇒ λinstr_refl. if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr s) else let s ≝ add_ticks2 s in s | JNZ addr ⇒ λinstr_refl. if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr s) else let s ≝ add_ticks2 s in s | CJNE addr1 addr2 ⇒ λinstr_refl. match addr1 with [ inl l ⇒ let 〈addr1, addr2'〉 ≝ l in let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) (nat_of_bitvector ? (get_arg_8 … s false addr2')) in if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then let s ≝ add_ticks1 s in let s ≝ set_program_counter … s (addr_of addr2 s) in set_flags … s new_cy (None ?) (get_ov_flag ?? s) else let s ≝ add_ticks2 s in set_flags … s new_cy (None ?) (get_ov_flag ?? s) | inr r' ⇒ let 〈addr1, addr2'〉 ≝ r' in let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) (nat_of_bitvector ? (get_arg_8 … s false addr2')) in if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then let s ≝ add_ticks1 s in let s ≝ set_program_counter … s (addr_of addr2 s) in set_flags … s new_cy (None ?) (get_ov_flag ?? s) else let s ≝ add_ticks2 s in set_flags … s new_cy (None ?) (get_ov_flag ?? s) ] | DJNZ addr1 addr2 ⇒ λinstr_refl. let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in let s ≝ set_arg_8 … s addr1 result in if ¬(eq_bv ? result (zero 8)) then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr2 s) else let s ≝ add_ticks2 s in s ] (refl … instr)) try (cases(other)) try assumption (*20s*) try (% @False) (*6s*) (* Bug exploited here to implement solve :-*) try ( @(execute_1_technical … (subaddressing_modein …)) @I ) (*66s*) whd in match execute_1_preinstruction; normalize nodelta [1: (* ADD *) >p normalize nodelta >EQP %{1} whd in ⊢ (??%?); (* work on fetch_many *) EQassembled whd in match code_memory_of_pseudo_assembly_program; normalize nodelta whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); (eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?); @(pair_replace ?????????? p) [2: normalize nodelta >EQs -s >EQticks' -ticks' EQticks -ticks EQnewpc >sigma_increment_commutation % |2: whd in ⊢ (??%%); >set_clock_mk_Status_commutation whd in match (set_flags ??????); (* CSC: TO BE COMPLETED *) ] | (*>get_arg_8_ok_set_clock*) (*CSC: to be done *) ] ] cases daemon qed. (* @list_addressing_mode_tags_elim_prop try % whd @list_addressing_mode_tags_elim_prop try % whd #arg (* XXX: we first work on sigma_increment_commutation *) #sigma_increment_commutation normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; (* XXX: we work on the maps *) whd in ⊢ (??%? → ?); try (change with (if ? then ? else ? = ? → ?) cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta) #H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm EQassembled in fetch_many_assm; cases (fetch ??) * #instr #newpc #ticks normalize nodelta * * #eq_instr #EQticks whd in EQticks:(???%); >EQticks #fetch_many_assm whd in fetch_many_assm; lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc >(eq_instruction_to_eq … eq_instr) -instr [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs @(pose … (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy)) #Pl #EQPl cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) -XX >EQlhs -lhs whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%))); @pair_elim >tech_pi1_let_as_commute *) theorem main_thm: ] ] |1: (* Instruction *) -pi;  * |1: (* Instruction *) -pi; #instr @(main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness … EQppc … create_label_cost_refl … assembly_refl EQassembled … EQlookup_labels … EQlookup_datalabels EQnewppc instr … (refl …) … (refl …) … (refl …) … (refl …)) |4,5: cases daemon ] qed. (* * [1,2,3: (* ADD, ADDC, SUBB *) @list_addressing_mode_tags_elim_prop try % whd #fetch_many_assm whd in fetch_many_assm; lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc >(eq_instruction_to_eq … eq_instr) -instr whd in ⊢ (??%?); >(eq_instruction_to_eq … eq_instr) -instr [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs @(pose … (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy)) #Pl #EQPl cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) -XX >EQlhs -lhs whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%))); @pair_elim >tech_pi1_let_as_commute whd in ⊢ (??%?); [ @(pose … (execute_1_preinstruction' ???????)) #lhs whd in ⊢ (???% → ?); #EQlhs @(pose … (execute_1_preinstruction' ???????)) #rhs whd in ⊢ (???% → ?); #EQrhs CSC: delirium cases daemon (* EASY CASES TO BE COMPLETED *) qed. *)
• src/ASM/Interpret.ma

 r1969 include alias "ASM/BitVectorTrie.ma". definition execute_1_preinstruction': definition execute_1_preinstruction: ∀ticks: nat × nat. ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → ∀instr: preinstruction a. ∀s: PreStatus m cm. Σs': PreStatus m cm. And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s)) (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) ≝ ∀s: PreStatus m cm. PreStatus m cm ≝ λticks: nat × nat. λa, m: Type[0]. λcm. let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm. And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s)) (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) with match instr in preinstruction return λx. x = instr → PreStatus m cm with [ ADD addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in @I ) (*66s*) qed. definition execute_1_preinstruction_ok': ∀ticks: nat × nat. ∀a, m: Type[0]. ∀cm. ∀addr_of:a → PreStatus m cm → Word. ∀instr: preinstruction a. ∀s: PreStatus m cm. Σs': PreStatus m cm. (*And ( *) let s' ≝ execute_1_preinstruction ticks a m cm addr_of instr s in (And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s)) (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)) ≝ λticks: nat × nat. λa, m: Type[0]. λcm. λaddr_of: a → PreStatus m cm → Word. λinstr: preinstruction a. λs: PreStatus m cm. let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm. ?(*And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s)) (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)*) with [ ADD addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) (get_arg_8 … s false addr2) false in let cy_flag ≝ get_index' ? O  ? flags in let ac_flag ≝ get_index' ? 1 ? flags in let ov_flag ≝ get_index' ? 2 ? flags in let s ≝ set_arg_8 … s ACC_A result in set_flags … s cy_flag (Some Bit ac_flag) ov_flag | ADDC addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let old_cy_flag ≝ get_cy_flag ?? s in let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) (get_arg_8 … s false addr2) old_cy_flag in let cy_flag ≝ get_index' ? O ? flags in let ac_flag ≝ get_index' ? 1 ? flags in let ov_flag ≝ get_index' ? 2 ? flags in let s ≝ set_arg_8 … s ACC_A result in set_flags … s cy_flag (Some Bit ac_flag) ov_flag | SUBB addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let old_cy_flag ≝ get_cy_flag ?? s in let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1) (get_arg_8 … s false addr2) old_cy_flag in let cy_flag ≝ get_index' ? O ? flags in let ac_flag ≝ get_index' ? 1 ? flags in let ov_flag ≝ get_index' ? 2 ? flags in let s ≝ set_arg_8 … s ACC_A result in set_flags … s cy_flag (Some Bit ac_flag) ov_flag | ANL addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in match addr with [ inl l ⇒ match l with [ inl l' ⇒ let 〈addr1, addr2〉 ≝ l' in let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in set_arg_8 … s addr1 and_val | inr r ⇒ let 〈addr1, addr2〉 ≝ r in let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in set_arg_8 … s addr1 and_val ] | inr r ⇒ let 〈addr1, addr2〉 ≝ r in let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in set_flags … s and_val (None ?) (get_ov_flag ?? s) ] | ORL addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in match addr with [ inl l ⇒ match l with [ inl l' ⇒ let 〈addr1, addr2〉 ≝ l' in let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in set_arg_8 … s addr1 or_val | inr r ⇒ let 〈addr1, addr2〉 ≝ r in let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in set_arg_8 … s addr1 or_val ] | inr r ⇒ let 〈addr1, addr2〉 ≝ r in let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in set_flags … s or_val (None ?) (get_ov_flag … s) ] | XRL addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in match addr with [ inl l' ⇒ let 〈addr1, addr2〉 ≝ l' in let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in set_arg_8 … s addr1 xor_val | inr r ⇒ let 〈addr1, addr2〉 ≝ r in let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in set_arg_8 … s addr1 xor_val ] | INC addr ⇒ λinstr_refl. match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x=addr → Σs': PreStatus m cm. ? with [ ACC_A ⇒ λacc_a: True. λEQaddr. let s' ≝ add_ticks1 s in let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in set_arg_8 … s' ACC_A result | REGISTER r ⇒ λregister: True. λEQaddr. let s' ≝ add_ticks1 s in let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in set_arg_8 … s' (REGISTER r) result | DIRECT d ⇒ λdirect: True. λEQaddr. let s' ≝ add_ticks1 s in let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in set_arg_8 … s' (DIRECT d) result | INDIRECT i ⇒ λindirect: True. λEQaddr. let s' ≝ add_ticks1 s in let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in set_arg_8 … s' (INDIRECT i) result | DPTR ⇒ λdptr: True. λEQaddr. let s' ≝ add_ticks1 s in let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in let s ≝ set_8051_sfr … s' SFR_DPL bl in set_8051_sfr … s' SFR_DPH bu | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr)) | NOP ⇒ λinstr_refl. let s ≝ add_ticks2 s in s | DEC addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in set_arg_8 … s addr result | MUL addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in let product ≝ acc_a_nat * acc_b_nat in let ov_flag ≝ product ≥ 256 in let low ≝ bitvector_of_nat 8 (product mod 256) in let high ≝ bitvector_of_nat 8 (product ÷ 256) in let s ≝ set_8051_sfr … s SFR_ACC_A low in set_8051_sfr … s SFR_ACC_B high | DIV addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in match acc_b_nat with [ O ⇒ set_flags … s false (None Bit) true | S o ⇒ let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in let s ≝ set_8051_sfr … s SFR_ACC_A q in let s ≝ set_8051_sfr … s SFR_ACC_B r in set_flags … s false (None Bit) false ] | DA addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in let cy_flag ≝ get_index' ? O ? flags in let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in let new_acc ≝ nu @@ acc_nl' in let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s) else s else s | CLR addr ⇒ λinstr_refl. match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with [ ACC_A ⇒ λacc_a: True. λEQaddr. let s ≝ add_ticks1 s in set_arg_8 … s ACC_A (zero 8) | CARRY ⇒ λcarry: True. λEQaddr. let s ≝ add_ticks1 s in set_arg_1 … s CARRY false | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr. let s ≝ add_ticks1 s in set_arg_1 … s (BIT_ADDR b) false | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) | CPL addr ⇒ λinstr_refl. match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with [ ACC_A ⇒ λacc_a: True. λEQaddr. let s ≝ add_ticks1 s in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let new_acc ≝ negation_bv ? old_acc in set_8051_sfr … s SFR_ACC_A new_acc | CARRY ⇒ λcarry: True. λEQaddr. let s ≝ add_ticks1 s in let old_cy_flag ≝ get_arg_1 … s CARRY true in let new_cy_flag ≝ ¬old_cy_flag in set_arg_1 … s CARRY new_cy_flag | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr. let s ≝ add_ticks1 s in let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in let new_bit ≝ ¬old_bit in set_arg_1 … s (BIT_ADDR b) new_bit | _ ⇒ λother: False. ? ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) | SETB b ⇒ λinstr_refl. let s ≝ add_ticks1 s in set_arg_1 … s b false | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *) let s ≝ add_ticks1 s in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let new_acc ≝ rotate_left … 1 old_acc in set_8051_sfr … s SFR_ACC_A new_acc | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *) let s ≝ add_ticks1 s in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let new_acc ≝ rotate_right … 1 old_acc in set_8051_sfr … s SFR_ACC_A new_acc | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) let s ≝ add_ticks1 s in let old_cy_flag ≝ get_cy_flag ?? s in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let new_cy_flag ≝ get_index' ? O ? old_acc in let new_acc ≝ shift_left … 1 old_acc old_cy_flag in let s ≝ set_arg_1 … s CARRY new_cy_flag in set_8051_sfr … s SFR_ACC_A new_acc | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) let s ≝ add_ticks1 s in let old_cy_flag ≝ get_cy_flag ?? s in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let new_cy_flag ≝ get_index' ? 7 ? old_acc in let new_acc ≝ shift_right … 1 old_acc old_cy_flag in let s ≝ set_arg_1 … s CARRY new_cy_flag in set_8051_sfr … s SFR_ACC_A new_acc | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *) let s ≝ add_ticks1 s in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let 〈nu,nl〉 ≝ split ? 4 4 old_acc in let new_acc ≝ nl @@ nu in set_8051_sfr … s SFR_ACC_A new_acc | PUSH addr ⇒ λinstr_refl. match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x=addr → Σs': PreStatus m cm. ? with [ DIRECT d ⇒ λdirect: True. λEQaddr. let s ≝ add_ticks1 s in let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in let s ≝ set_8051_sfr … s SFR_SP new_sp in write_at_stack_pointer … s d | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) | POP addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in let contents ≝ read_at_stack_pointer ?? s in let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in let s ≝ set_8051_sfr … s SFR_SP new_sp in set_arg_8 … s addr contents | XCH addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let old_addr ≝ get_arg_8 … s false addr2 in let old_acc ≝ get_8051_sfr … s SFR_ACC_A in let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in set_arg_8 … s addr2 old_acc | XCHD addr1 addr2 ⇒ λinstr_refl. let s ≝ add_ticks1 s in let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in let new_acc ≝ acc_nu @@ arg_nl in let new_arg ≝ arg_nu @@ acc_nl in let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in set_arg_8 … s addr2 new_arg | RET ⇒ λinstr_refl. let s ≝ add_ticks1 s in let high_bits ≝ read_at_stack_pointer ?? s in let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in let s ≝ set_8051_sfr … s SFR_SP new_sp in let low_bits ≝ read_at_stack_pointer ?? s in let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in let s ≝ set_8051_sfr … s SFR_SP new_sp in let new_pc ≝ high_bits @@ low_bits in set_program_counter … s new_pc | RETI ⇒ λinstr_refl. let s ≝ add_ticks1 s in let high_bits ≝ read_at_stack_pointer ?? s in let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in let s ≝ set_8051_sfr … s SFR_SP new_sp in let low_bits ≝ read_at_stack_pointer ?? s in let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in let s ≝ set_8051_sfr … s SFR_SP new_sp in let new_pc ≝ high_bits @@ low_bits in set_program_counter … s new_pc | MOVX addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in (* DPM: only copies --- doesn't affect I/O *) match addr with [ inl l ⇒ let 〈addr1, addr2〉 ≝ l in set_arg_8 … s addr1 (get_arg_8 … s false addr2) | inr r ⇒ let 〈addr1, addr2〉 ≝ r in set_arg_8 … s addr1 (get_arg_8 … s false addr2) ] | MOV addr ⇒ λinstr_refl. let s ≝ add_ticks1 s in match addr with [ inl l ⇒ match l with [ inl l' ⇒ match l' with [ inl l'' ⇒ match l'' with [ inl l''' ⇒ match l''' with [ inl l'''' ⇒ let 〈addr1, addr2〉 ≝ l'''' in set_arg_8 … s addr1 (get_arg_8 … s false addr2) | inr r'''' ⇒ let 〈addr1, addr2〉 ≝ r'''' in set_arg_8 … s addr1 (get_arg_8 … s false addr2) ] | inr r''' ⇒ let 〈addr1, addr2〉 ≝ r''' in set_arg_8 … s addr1 (get_arg_8 … s false addr2) ] | inr r'' ⇒ let 〈addr1, addr2〉 ≝ r'' in set_arg_16 … s (get_arg_16 … s addr2) addr1 ] | inr r ⇒ let 〈addr1, addr2〉 ≝ r in set_arg_1 … s addr1 (get_arg_1 … s addr2 false) ] | inr r ⇒ let 〈addr1, addr2〉 ≝ r in set_arg_1 … s addr1 (get_arg_1 … s addr2 false) ] | JC addr ⇒ λinstr_refl. if get_cy_flag ?? s then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr s) else let s ≝ add_ticks2 s in s | JNC addr ⇒ λinstr_refl. if ¬(get_cy_flag ?? s) then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr s) else let s ≝ add_ticks2 s in s | JB addr1 addr2 ⇒ λinstr_refl. if get_arg_1 … s addr1 false then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr2 s) else let s ≝ add_ticks2 s in s | JNB addr1 addr2 ⇒ λinstr_refl. if ¬(get_arg_1 … s addr1 false) then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr2 s) else let s ≝ add_ticks2 s in s | JBC addr1 addr2 ⇒ λinstr_refl. let s ≝ set_arg_1 … s addr1 false in if get_arg_1 … s addr1 false then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr2 s) else let s ≝ add_ticks2 s in s | JZ addr ⇒ λinstr_refl. if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr s) else let s ≝ add_ticks2 s in s | JNZ addr ⇒ λinstr_refl. if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr s) else let s ≝ add_ticks2 s in s | CJNE addr1 addr2 ⇒ λinstr_refl. match addr1 with [ inl l ⇒ let 〈addr1, addr2'〉 ≝ l in let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) (nat_of_bitvector ? (get_arg_8 … s false addr2')) in if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then let s ≝ add_ticks1 s in let s ≝ set_program_counter … s (addr_of addr2 s) in set_flags … s new_cy (None ?) (get_ov_flag ?? s) else let s ≝ add_ticks2 s in set_flags … s new_cy (None ?) (get_ov_flag ?? s) | inr r' ⇒ let 〈addr1, addr2'〉 ≝ r' in let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) (nat_of_bitvector ? (get_arg_8 … s false addr2')) in if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then let s ≝ add_ticks1 s in let s ≝ set_program_counter … s (addr_of addr2 s) in set_flags … s new_cy (None ?) (get_ov_flag ?? s) else let s ≝ add_ticks2 s in set_flags … s new_cy (None ?) (get_ov_flag ?? s) ] | DJNZ addr1 addr2 ⇒ λinstr_refl. let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in let s ≝ set_arg_8 … s addr1 result in if ¬(eq_bv ? result (zero 8)) then let s ≝ add_ticks1 s in set_program_counter … s (addr_of addr2 s) else let s ≝ add_ticks2 s in s ] (refl … instr). try (cases(other)) try assumption (*20s*) try (% @False) (*6s*) (* Bug exploited here to implement solve :-*) try ( @(execute_1_technical … (subaddressing_modein …)) @I ) (*66s*) whd in match execute_1_preinstruction; normalize nodelta % try (p normalize nodelta try (>p1 normalize nodelta try (>p2 normalize nodelta try (>p3 normalize nodelta try (>p4 normalize nodelta try (>p5 normalize nodelta)))))) try (change with (cl_jump = cl_other → ?) #absurd destruct(absurd)) try (change with (cl_return = cl_other → ?) #absurd destruct(absurd)) try (@or_introl //) try (@or_intror //) #_ /demod/ % qed. definition execute_1_preinstruction: ∀ticks: nat × nat. ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a → PreStatus m cm → PreStatus m cm ≝ execute_1_preinstruction'. try (#_ /demod/ %) try (#_ //) [
Note: See TracChangeset for help on using the changeset viewer.