Changeset 1971


Ignore:
Timestamp:
May 20, 2012, 10:34:31 PM (6 years ago)
Author:
sacerdot
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

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r1969 r1971  
    8888 #P #A #a #abs destruct
    8989qed.
     90
     91(*
     92lemma pi1_let_commute:
     93 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
     94 pi1 … (let 〈x1,y1〉 ≝ c in t) = (let 〈x1,y1〉 ≝ c in pi1 … t).
     95 #A #B #C #P * #a #b * //
     96qed.
     97
     98lemma pi1_let_as_commute:
     99 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
     100 pi1 … (let 〈x1,y1〉 as H ≝ c in t) =
     101  (let 〈x1,y1〉 as H ≝ c in pi1 … t).
     102 #A #B #C #P * #a #b * //
     103qed.
     104*)
     105
     106lemma tech_pi1_let_as_commute:
     107 ∀A,B,C,P. ∀f. ∀c,c':A × B.
     108 ∀t: ∀a,b. 〈a,b〉=c → Σc:C.P c.
     109 ∀t': ∀a,b. 〈a,b〉=c' → Σc:C.P c.
     110  c=c' → (∀x,y,H,H'.t x y H = f (pi1 … (t' x y H'))) →
     111  pi1 … (let 〈x1,y1〉 as H ≝ c in t x1 y1 H) =
     112   f (pi1 … (let 〈x1,y1〉 as H ≝ c' in t' x1 y1 H)).
     113 #A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/
     114qed.
     115
     116include alias "arithmetics/nat.ma".
     117include alias "basics/logic.ma".
     118include alias "ASM/BitVectorTrie.ma".
     119
     120lemma pair_replace:
     121 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c=c' → c ≃ 〈a,b〉 →
     122  P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b').
     123 #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct //
     124qed.
     125
     126lemma main_lemma_preinstruction:
     127 ∀M,M': internal_pseudo_address_map.
     128 ∀preamble : preamble. ∀instr_list : list labelled_instruction.
     129 ∀cm: pseudo_assembly_program.
     130 ∀EQcm: cm = 〈preamble,instr_list〉.
     131 ∀sigma : Word→Word. ∀policy : Word→bool.
     132 ∀sigma_policy_witness : sigma_policy_specification cm sigma policy.
     133 ∀ps : PseudoStatus cm.
     134 ∀ppc : Word.
     135 ∀EQppc : ppc=program_counter pseudo_assembly_program cm ps.
     136 ∀labels : label_map.
     137 ∀costs : BitVectorTrie costlabel 16.
     138 ∀create_label_cost_refl : create_label_cost_map instr_list=〈labels,costs〉.
     139 ∀assembled : list Byte.
     140 ∀costs' : BitVectorTrie costlabel 16.
     141 ∀assembly_refl : assembly 〈preamble,instr_list〉 sigma policy=〈assembled,costs'〉.
     142 ∀EQassembled : assembled=\fst  (assembly cm sigma policy).
     143 ∀newppc : Word.
     144 ∀lookup_labels : Identifier→Word.
     145 ∀EQlookup_labels : lookup_labels = (λx:Identifier.sigma (address_of_word_labels_code_mem instr_list x)).
     146 ∀lookup_datalabels : identifier ASMTag→Word.
     147 ∀ EQlookup_datalabels : lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
     148 ∀EQnewppc : newppc=add 16 ppc (bitvector_of_nat 16 1).
     149 ∀instr: preinstruction Identifier.
     150 ∀ticks.
     151 ∀EQticks: ticks = ticks_of0 〈preamble,instr_list〉 sigma policy ppc (Instruction instr).
     152 ∀addr_of.
     153 ∀EQaddr_of: addr_of = (λx:Identifier
     154         .λy:PreStatus pseudo_assembly_program cm
     155          .address_of_word_labels cm x).
     156 ∀s.
     157 ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps
     158         (add 16 ppc (bitvector_of_nat 16 1))).
     159 ∀P.
     160 ∀EQP:
     161  P = (λs. ∃n:ℕ
     162      .execute n
     163       (code_memory_of_pseudo_assembly_program cm sigma
     164        policy)
     165       (status_of_pseudo_status M cm ps sigma policy)
     166      =status_of_pseudo_status M' cm s sigma policy).
     167  sigma (add 16 ppc (bitvector_of_nat 16 1))
     168   =add 16 (sigma ppc)
     169    (bitvector_of_nat 16
     170     (\fst  (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
     171                  lookup_datalabels (Instruction instr))))
     172   →next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr)
     173    M cm ps
     174    =Some internal_pseudo_address_map M'
     175    →fetch_many (load_code_memory assembled)
     176     (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma ppc)
     177     (expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels
     178      (Instruction instr))
     179     →P (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm
     180         addr_of instr s).
     181 #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
     182 #costs #create_label_cost_refl #assembled #costs' #assembly_refl #EQassembled #newppc
     183 #lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr
     184 #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
     185 #sigma_increment_commutation #maps_assm #fetch_many_assm
     186 letin a ≝ Identifier letin m ≝ pseudo_assembly_program
     187 cut (Σxxx:PseudoStatus cm. P (execute_1_preinstruction ticks a m cm addr_of instr s))
     188 [2: * // ]
     189 @(
     190  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
     191  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
     192  match instr in preinstruction return λx. x = instr → Σs'.? with
     193        [ ADD addr1 addr2 ⇒ λinstr_refl.
     194            let s ≝ add_ticks1 s in
     195            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
     196                                                   (get_arg_8 … s false addr2) false in
     197            let cy_flag ≝ get_index' ? O  ? flags in
     198            let ac_flag ≝ get_index' ? 1 ? flags in
     199            let ov_flag ≝ get_index' ? 2 ? flags in
     200            let s ≝ set_arg_8 … s ACC_A result in
     201              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
     202        | ADDC addr1 addr2 ⇒ λinstr_refl.
     203            let s ≝ add_ticks1 s in
     204            let old_cy_flag ≝ get_cy_flag ?? s in
     205            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
     206                                                   (get_arg_8 … s false addr2) old_cy_flag in
     207            let cy_flag ≝ get_index' ? O ? flags in
     208            let ac_flag ≝ get_index' ? 1 ? flags in
     209            let ov_flag ≝ get_index' ? 2 ? flags in
     210            let s ≝ set_arg_8 … s ACC_A result in
     211              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
     212        | SUBB addr1 addr2 ⇒ λinstr_refl.
     213            let s ≝ add_ticks1 s in
     214            let old_cy_flag ≝ get_cy_flag ?? s in
     215            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
     216                                                   (get_arg_8 … s false addr2) old_cy_flag in
     217            let cy_flag ≝ get_index' ? O ? flags in
     218            let ac_flag ≝ get_index' ? 1 ? flags in
     219            let ov_flag ≝ get_index' ? 2 ? flags in
     220            let s ≝ set_arg_8 … s ACC_A result in
     221              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
     222        | ANL addr ⇒ λinstr_refl.
     223          let s ≝ add_ticks1 s in
     224          match addr with
     225            [ inl l ⇒
     226              match l with
     227                [ inl l' ⇒
     228                  let 〈addr1, addr2〉 ≝ l' in
     229                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     230                    set_arg_8 … s addr1 and_val
     231                | inr r ⇒
     232                  let 〈addr1, addr2〉 ≝ r in
     233                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     234                    set_arg_8 … s addr1 and_val
     235                ]
     236            | inr r ⇒
     237              let 〈addr1, addr2〉 ≝ r in
     238              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
     239               set_flags … s and_val (None ?) (get_ov_flag ?? s)
     240            ]
     241        | ORL addr ⇒ λinstr_refl.
     242          let s ≝ add_ticks1 s in
     243          match addr with
     244            [ inl l ⇒
     245              match l with
     246                [ inl l' ⇒
     247                  let 〈addr1, addr2〉 ≝ l' in
     248                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     249                    set_arg_8 … s addr1 or_val
     250                | inr r ⇒
     251                  let 〈addr1, addr2〉 ≝ r in
     252                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     253                    set_arg_8 … s addr1 or_val
     254                ]
     255            | inr r ⇒
     256              let 〈addr1, addr2〉 ≝ r in
     257              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
     258               set_flags … s or_val (None ?) (get_ov_flag … s)
     259            ]
     260        | XRL addr ⇒ λinstr_refl.
     261          let s ≝ add_ticks1 s in
     262          match addr with
     263            [ inl l' ⇒
     264              let 〈addr1, addr2〉 ≝ l' in
     265              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     266                set_arg_8 … s addr1 xor_val
     267            | inr r ⇒
     268              let 〈addr1, addr2〉 ≝ r in
     269              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     270                set_arg_8 … s addr1 xor_val
     271            ]
     272        | INC addr ⇒ λinstr_refl.
     273            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with
     274              [ ACC_A ⇒ λacc_a: True.
     275                let s' ≝ add_ticks1 s in
     276                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
     277                 set_arg_8 … s' ACC_A result
     278              | REGISTER r ⇒ λregister: True.
     279                let s' ≝ add_ticks1 s in
     280                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
     281                 set_arg_8 … s' (REGISTER r) result
     282              | DIRECT d ⇒ λdirect: True.
     283                let s' ≝ add_ticks1 s in
     284                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
     285                 set_arg_8 … s' (DIRECT d) result
     286              | INDIRECT i ⇒ λindirect: True.
     287                let s' ≝ add_ticks1 s in
     288                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
     289                 set_arg_8 … s' (INDIRECT i) result
     290              | DPTR ⇒ λdptr: True.
     291                let s' ≝ add_ticks1 s in
     292                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
     293                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
     294                let s ≝ set_8051_sfr … s' SFR_DPL bl in
     295                 set_8051_sfr … s' SFR_DPH bu
     296              | _ ⇒ λother: False. ⊥
     297              ] (subaddressing_modein … addr)
     298        | NOP ⇒ λinstr_refl.
     299           let s ≝ add_ticks2 s in
     300            s
     301        | DEC addr ⇒ λinstr_refl.
     302           let s ≝ add_ticks1 s in
     303           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
     304             set_arg_8 … s addr result
     305        | MUL addr1 addr2 ⇒ λinstr_refl.
     306           let s ≝ add_ticks1 s in
     307           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
     308           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
     309           let product ≝ acc_a_nat * acc_b_nat in
     310           let ov_flag ≝ product ≥ 256 in
     311           let low ≝ bitvector_of_nat 8 (product mod 256) in
     312           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
     313           let s ≝ set_8051_sfr … s SFR_ACC_A low in
     314             set_8051_sfr … s SFR_ACC_B high
     315        | DIV addr1 addr2 ⇒ λinstr_refl.
     316           let s ≝ add_ticks1 s in
     317           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
     318           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
     319             match acc_b_nat with
     320               [ O ⇒ set_flags … s false (None Bit) true
     321               | S o ⇒
     322                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
     323                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
     324                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
     325                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
     326                   set_flags … s false (None Bit) false
     327               ]
     328        | DA addr ⇒ λinstr_refl.
     329            let s ≝ add_ticks1 s in
     330            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
     331              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
     332                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
     333                let cy_flag ≝ get_index' ? O ? flags in
     334                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
     335                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
     336                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
     337                    let new_acc ≝ nu @@ acc_nl' in
     338                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
     339                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
     340                  else
     341                    s
     342              else
     343                s
     344        | CLR addr ⇒ λinstr_refl.
     345          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
     346            [ ACC_A ⇒ λacc_a: True.
     347              let s ≝ add_ticks1 s in
     348               set_arg_8 … s ACC_A (zero 8)
     349            | CARRY ⇒ λcarry: True.
     350              let s ≝ add_ticks1 s in
     351               set_arg_1 … s CARRY false
     352            | BIT_ADDR b ⇒ λbit_addr: True.
     353              let s ≝ add_ticks1 s in
     354               set_arg_1 … s (BIT_ADDR b) false
     355            | _ ⇒ λother: False. ⊥
     356            ] (subaddressing_modein … addr)
     357        | CPL addr ⇒ λinstr_refl.
     358          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
     359            [ ACC_A ⇒ λacc_a: True.
     360                let s ≝ add_ticks1 s in
     361                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     362                let new_acc ≝ negation_bv ? old_acc in
     363                 set_8051_sfr … s SFR_ACC_A new_acc
     364            | CARRY ⇒ λcarry: True.
     365                let s ≝ add_ticks1 s in
     366                let old_cy_flag ≝ get_arg_1 … s CARRY true in
     367                let new_cy_flag ≝ ¬old_cy_flag in
     368                 set_arg_1 … s CARRY new_cy_flag
     369            | BIT_ADDR b ⇒ λbit_addr: True.
     370                let s ≝ add_ticks1 s in
     371                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
     372                let new_bit ≝ ¬old_bit in
     373                 set_arg_1 … s (BIT_ADDR b) new_bit
     374            | _ ⇒ λother: False. ?
     375            ] (subaddressing_modein … addr)
     376        | SETB b ⇒ λinstr_refl.
     377            let s ≝ add_ticks1 s in
     378            set_arg_1 … s b false
     379        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     380            let s ≝ add_ticks1 s in
     381            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     382            let new_acc ≝ rotate_left … 1 old_acc in
     383              set_8051_sfr … s SFR_ACC_A new_acc
     384        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     385            let s ≝ add_ticks1 s in
     386            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     387            let new_acc ≝ rotate_right … 1 old_acc in
     388              set_8051_sfr … s SFR_ACC_A new_acc
     389        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     390            let s ≝ add_ticks1 s in
     391            let old_cy_flag ≝ get_cy_flag ?? s in
     392            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     393            let new_cy_flag ≝ get_index' ? O ? old_acc in
     394            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
     395            let s ≝ set_arg_1 … s CARRY new_cy_flag in
     396              set_8051_sfr … s SFR_ACC_A new_acc
     397        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     398            let s ≝ add_ticks1 s in
     399            let old_cy_flag ≝ get_cy_flag ?? s in
     400            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     401            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
     402            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
     403            let s ≝ set_arg_1 … s CARRY new_cy_flag in
     404              set_8051_sfr … s SFR_ACC_A new_acc
     405        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     406            let s ≝ add_ticks1 s in
     407            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     408            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
     409            let new_acc ≝ nl @@ nu in
     410              set_8051_sfr … s SFR_ACC_A new_acc
     411        | PUSH addr ⇒ λinstr_refl.
     412            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with
     413              [ DIRECT d ⇒ λdirect: True.
     414                let s ≝ add_ticks1 s in
     415                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     416                let s ≝ set_8051_sfr … s SFR_SP new_sp in
     417                  write_at_stack_pointer … s d
     418              | _ ⇒ λother: False. ⊥
     419              ] (subaddressing_modein … addr)
     420        | POP addr ⇒ λinstr_refl.
     421            let s ≝ add_ticks1 s in
     422            let contents ≝ read_at_stack_pointer ?? s in
     423            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     424            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     425              set_arg_8 … s addr contents
     426        | XCH addr1 addr2 ⇒ λinstr_refl.
     427            let s ≝ add_ticks1 s in
     428            let old_addr ≝ get_arg_8 … s false addr2 in
     429            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     430            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
     431              set_arg_8 … s addr2 old_acc
     432        | XCHD addr1 addr2 ⇒ λinstr_refl.
     433            let s ≝ add_ticks1 s in
     434            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
     435            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
     436            let new_acc ≝ acc_nu @@ arg_nl in
     437            let new_arg ≝ arg_nu @@ acc_nl in
     438            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
     439              set_arg_8 … s addr2 new_arg
     440        | RET ⇒ λinstr_refl.
     441            let s ≝ add_ticks1 s in
     442            let high_bits ≝ read_at_stack_pointer ?? s in
     443            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     444            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     445            let low_bits ≝ read_at_stack_pointer ?? s in
     446            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     447            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     448            let new_pc ≝ high_bits @@ low_bits in
     449              set_program_counter … s new_pc
     450        | RETI ⇒ λinstr_refl.
     451            let s ≝ add_ticks1 s in
     452            let high_bits ≝ read_at_stack_pointer ?? s in
     453            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     454            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     455            let low_bits ≝ read_at_stack_pointer ?? s in
     456            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     457            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     458            let new_pc ≝ high_bits @@ low_bits in
     459              set_program_counter … s new_pc
     460        | MOVX addr ⇒ λinstr_refl.
     461          let s ≝ add_ticks1 s in
     462          (* DPM: only copies --- doesn't affect I/O *)
     463          match addr with
     464            [ inl l ⇒
     465              let 〈addr1, addr2〉 ≝ l in
     466                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     467            | inr r ⇒
     468              let 〈addr1, addr2〉 ≝ r in
     469                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     470            ]
     471        | MOV addr ⇒ λinstr_refl.
     472          let s ≝ add_ticks1 s in
     473          match addr with
     474            [ inl l ⇒
     475              match l with
     476                [ inl l' ⇒
     477                  match l' with
     478                    [ inl l'' ⇒
     479                      match l'' with
     480                        [ inl l''' ⇒
     481                          match l''' with
     482                            [ inl l'''' ⇒
     483                              let 〈addr1, addr2〉 ≝ l'''' in
     484                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     485                            | inr r'''' ⇒
     486                              let 〈addr1, addr2〉 ≝ r'''' in
     487                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     488                            ]
     489                        | inr r''' ⇒
     490                          let 〈addr1, addr2〉 ≝ r''' in
     491                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     492                        ]
     493                    | inr r'' ⇒
     494                      let 〈addr1, addr2〉 ≝ r'' in
     495                       set_arg_16 … s (get_arg_16 … s addr2) addr1
     496                    ]
     497                | inr r ⇒
     498                  let 〈addr1, addr2〉 ≝ r in
     499                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
     500                ]
     501            | inr r ⇒
     502              let 〈addr1, addr2〉 ≝ r in
     503               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
     504            ]
     505          | JC addr ⇒ λinstr_refl.
     506                  if get_cy_flag ?? s then
     507                    let s ≝ add_ticks1 s in
     508                      set_program_counter … s (addr_of addr s)
     509                  else
     510                    let s ≝ add_ticks2 s in
     511                      s
     512            | JNC addr ⇒ λinstr_refl.
     513                  if ¬(get_cy_flag ?? s) then
     514                   let s ≝ add_ticks1 s in
     515                     set_program_counter … s (addr_of addr s)
     516                  else
     517                   let s ≝ add_ticks2 s in
     518                    s
     519            | JB addr1 addr2 ⇒ λinstr_refl.
     520                  if get_arg_1 … s addr1 false then
     521                   let s ≝ add_ticks1 s in
     522                    set_program_counter … s (addr_of addr2 s)
     523                  else
     524                   let s ≝ add_ticks2 s in
     525                    s
     526            | JNB addr1 addr2 ⇒ λinstr_refl.
     527                  if ¬(get_arg_1 … s addr1 false) then
     528                   let s ≝ add_ticks1 s in
     529                    set_program_counter … s (addr_of addr2 s)
     530                  else
     531                   let s ≝ add_ticks2 s in
     532                    s
     533            | JBC addr1 addr2 ⇒ λinstr_refl.
     534                  let s ≝ set_arg_1 … s addr1 false in
     535                    if get_arg_1 … s addr1 false then
     536                     let s ≝ add_ticks1 s in
     537                      set_program_counter … s (addr_of addr2 s)
     538                    else
     539                     let s ≝ add_ticks2 s in
     540                      s
     541            | JZ addr ⇒ λinstr_refl.
     542                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
     543                     let s ≝ add_ticks1 s in
     544                      set_program_counter … s (addr_of addr s)
     545                    else
     546                     let s ≝ add_ticks2 s in
     547                      s
     548            | JNZ addr ⇒ λinstr_refl.
     549                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
     550                     let s ≝ add_ticks1 s in
     551                      set_program_counter … s (addr_of addr s)
     552                    else
     553                     let s ≝ add_ticks2 s in
     554                      s
     555            | CJNE addr1 addr2 ⇒ λinstr_refl.
     556                  match addr1 with
     557                    [ inl l ⇒
     558                        let 〈addr1, addr2'〉 ≝ l in
     559                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
     560                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
     561                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
     562                            let s ≝ add_ticks1 s in
     563                            let s ≝ set_program_counter … s (addr_of addr2 s) in
     564                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
     565                          else
     566                            let s ≝ add_ticks2 s in
     567                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
     568                    | inr r' ⇒
     569                        let 〈addr1, addr2'〉 ≝ r' in
     570                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
     571                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
     572                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
     573                            let s ≝ add_ticks1 s in
     574                            let s ≝ set_program_counter … s (addr_of addr2 s) in
     575                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
     576                          else
     577                            let s ≝ add_ticks2 s in
     578                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
     579                    ]
     580            | DJNZ addr1 addr2 ⇒ λinstr_refl.
     581              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
     582              let s ≝ set_arg_8 … s addr1 result in
     583                if ¬(eq_bv ? result (zero 8)) then
     584                 let s ≝ add_ticks1 s in
     585                  set_program_counter … s (addr_of addr2 s)
     586                else
     587                 let s ≝ add_ticks2 s in
     588                  s
     589           ] (refl … instr))
     590 try (cases(other))
     591 try assumption (*20s*)
     592 try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
     593 try (
     594   @(execute_1_technical … (subaddressing_modein …))
     595   @I
     596 ) (*66s*)
     597whd in match execute_1_preinstruction; normalize nodelta
     598[1: (* ADD *)
     599  >p normalize nodelta
     600  >EQP %{1}
     601  whd in ⊢ (??%?);
     602  (* work on fetch_many *)
     603  <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
     604  whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     605  whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
     606  <EQppc
     607  cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
     608  #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
     609  lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
     610  >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
     611  @(pair_replace ?????????? p)
     612   [2: normalize nodelta >EQs -s >EQticks' -ticks'
     613       <instr_refl in EQticks; #EQticks >EQticks -ticks
     614       <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
     615       whd in ⊢ (??%%);
     616       @split_eq_status
     617       try %
     618       [3: whd in ⊢ (??%%); >EQnewpc >sigma_increment_commutation %
     619       |2: whd in ⊢ (??%%); >set_clock_mk_Status_commutation
     620           whd in match (set_flags ??????);
     621           (* CSC: TO BE COMPLETED *)
     622       ]
     623   | (*>get_arg_8_ok_set_clock*) (*CSC: to be done *)
     624   ]
     625
     626] cases daemon
     627qed.
     628(*   
     629   
     630
     631    @list_addressing_mode_tags_elim_prop try % whd
     632    @list_addressing_mode_tags_elim_prop try % whd #arg
     633    (* XXX: we first work on sigma_increment_commutation *)
     634    #sigma_increment_commutation
     635    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
     636    (* XXX: we work on the maps *)
     637    whd in ⊢ (??%? → ?);
     638    try (change with (if ? then ? else ? = ? → ?)
     639         cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta)
     640    #H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm
     641    (* XXX: we assume the fetch_many hypothesis *)
     642    #fetch_many_assm
     643    (* XXX: we give the existential *)
     644    %{1}
     645    whd in match (execute_1_pseudo_instruction0 ?????);
     646    (* XXX: work on the left hand side of the equality *)
     647    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
     648    (* XXX: execute fetches some more *)
     649    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     650    whd in fetch_many_assm;
     651    >EQassembled in fetch_many_assm;
     652    cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
     653    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
     654    #fetch_many_assm whd in fetch_many_assm;
     655    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
     656    >(eq_instruction_to_eq … eq_instr) -instr
     657    [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs
     658      @(pose …
     659        (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy))
     660      #Pl #EQPl
     661      cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq
     662      lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) -XX >EQlhs -lhs
     663      whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%)));
     664      @pair_elim
     665      >tech_pi1_let_as_commute
     666
     667*) 
     668
    90669
    91670theorem main_thm:
     
    180759      ]
    181760    ]
    182   |1: (* Instruction *) -pi;  *
     761  |1: (* Instruction *) -pi; #instr
     762    @(main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness
     763      … EQppc … create_label_cost_refl … assembly_refl EQassembled … EQlookup_labels …
     764      EQlookup_datalabels EQnewppc instr … (refl …) … (refl …) … (refl …) … (refl …))
     765  |4,5: cases daemon
     766  ]
     767qed.
     768(* 
     769    *
    183770    [1,2,3: (* ADD, ADDC, SUBB *)
    184771    @list_addressing_mode_tags_elim_prop try % whd
     
    207794    #fetch_many_assm whd in fetch_many_assm;
    208795    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    209     >(eq_instruction_to_eq … eq_instr) -instr whd in ⊢ (??%?);
     796    >(eq_instruction_to_eq … eq_instr) -instr
     797    [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs
     798      @(pose …
     799        (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy))
     800      #Pl #EQPl
     801      cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq
     802      lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) -XX >EQlhs -lhs
     803      whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%)));
     804      @pair_elim
     805      >tech_pi1_let_as_commute
     806   
     807   
     808    whd in ⊢ (??%?);
    210809    [ @(pose … (execute_1_preinstruction' ???????))
    211810      #lhs whd in ⊢ (???% → ?); #EQlhs
    212811      @(pose … (execute_1_preinstruction' ???????))
    213812      #rhs whd in ⊢ (???% → ?); #EQrhs
    214      
     813
     814
    215815      CSC: delirium
    216816     
     
    5731173cases daemon (* EASY CASES TO BE COMPLETED *)
    5741174qed.
     1175*)
  • src/ASM/Interpret.ma

    r1969 r1971  
    112112include alias "ASM/BitVectorTrie.ma".
    113113
    114 definition execute_1_preinstruction':
     114definition execute_1_preinstruction:
    115115  ∀ticks: nat × nat.
    116116  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → ∀instr: preinstruction a.
    117   ∀s: PreStatus m cm.
    118     Σs': PreStatus m cm.
    119       And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
    120         (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) ≝
     117  ∀s: PreStatus m cm. PreStatus m cm ≝
    121118  λticks: nat × nat.
    122119  λa, m: Type[0]. λcm.
     
    126123  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
    127124  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
    128   match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm.
    129     And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
    130       (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) with
     125  match instr in preinstruction return λx. x = instr → PreStatus m cm with
    131126        [ ADD addr1 addr2 ⇒ λinstr_refl.
    132127            let s ≝ add_ticks1 s in
     
    533528      @I
    534529    ) (*66s*)
     530qed.
     531
     532definition execute_1_preinstruction_ok':
     533  ∀ticks: nat × nat.
     534  ∀a, m: Type[0]. ∀cm. ∀addr_of:a → PreStatus m cm → Word. ∀instr: preinstruction a.
     535  ∀s: PreStatus m cm.
     536    Σs': PreStatus m cm.
     537      (*And ( *) let s' ≝ execute_1_preinstruction ticks a m cm addr_of instr s in
     538      (And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
     539        (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)) ≝
     540  λticks: nat × nat.
     541  λa, m: Type[0]. λcm.
     542  λaddr_of: a → PreStatus m cm → Word.
     543  λinstr: preinstruction a.
     544  λs: PreStatus m cm.
     545  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
     546  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
     547  match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm.
     548    ?(*And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
     549      (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)*) with
     550        [ ADD addr1 addr2 ⇒ λinstr_refl.
     551            let s ≝ add_ticks1 s in
     552            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
     553                                                   (get_arg_8 … s false addr2) false in
     554            let cy_flag ≝ get_index' ? O  ? flags in
     555            let ac_flag ≝ get_index' ? 1 ? flags in
     556            let ov_flag ≝ get_index' ? 2 ? flags in
     557            let s ≝ set_arg_8 … s ACC_A result in
     558              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
     559        | ADDC addr1 addr2 ⇒ λinstr_refl.
     560            let s ≝ add_ticks1 s in
     561            let old_cy_flag ≝ get_cy_flag ?? s in
     562            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
     563                                                   (get_arg_8 … s false addr2) old_cy_flag in
     564            let cy_flag ≝ get_index' ? O ? flags in
     565            let ac_flag ≝ get_index' ? 1 ? flags in
     566            let ov_flag ≝ get_index' ? 2 ? flags in
     567            let s ≝ set_arg_8 … s ACC_A result in
     568              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
     569        | SUBB addr1 addr2 ⇒ λinstr_refl.
     570            let s ≝ add_ticks1 s in
     571            let old_cy_flag ≝ get_cy_flag ?? s in
     572            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
     573                                                   (get_arg_8 … s false addr2) old_cy_flag in
     574            let cy_flag ≝ get_index' ? O ? flags in
     575            let ac_flag ≝ get_index' ? 1 ? flags in
     576            let ov_flag ≝ get_index' ? 2 ? flags in
     577            let s ≝ set_arg_8 … s ACC_A result in
     578              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
     579        | ANL addr ⇒ λinstr_refl.
     580          let s ≝ add_ticks1 s in
     581          match addr with
     582            [ inl l ⇒
     583              match l with
     584                [ inl l' ⇒
     585                  let 〈addr1, addr2〉 ≝ l' in
     586                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     587                    set_arg_8 … s addr1 and_val
     588                | inr r ⇒
     589                  let 〈addr1, addr2〉 ≝ r in
     590                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     591                    set_arg_8 … s addr1 and_val
     592                ]
     593            | inr r ⇒
     594              let 〈addr1, addr2〉 ≝ r in
     595              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
     596               set_flags … s and_val (None ?) (get_ov_flag ?? s)
     597            ]
     598        | ORL addr ⇒ λinstr_refl.
     599          let s ≝ add_ticks1 s in
     600          match addr with
     601            [ inl l ⇒
     602              match l with
     603                [ inl l' ⇒
     604                  let 〈addr1, addr2〉 ≝ l' in
     605                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     606                    set_arg_8 … s addr1 or_val
     607                | inr r ⇒
     608                  let 〈addr1, addr2〉 ≝ r in
     609                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     610                    set_arg_8 … s addr1 or_val
     611                ]
     612            | inr r ⇒
     613              let 〈addr1, addr2〉 ≝ r in
     614              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
     615               set_flags … s or_val (None ?) (get_ov_flag … s)
     616            ]
     617        | XRL addr ⇒ λinstr_refl.
     618          let s ≝ add_ticks1 s in
     619          match addr with
     620            [ inl l' ⇒
     621              let 〈addr1, addr2〉 ≝ l' in
     622              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     623                set_arg_8 … s addr1 xor_val
     624            | inr r ⇒
     625              let 〈addr1, addr2〉 ≝ r in
     626              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
     627                set_arg_8 … s addr1 xor_val
     628            ]
     629        | INC addr ⇒ λinstr_refl.
     630            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x=addr → Σs': PreStatus m cm. ? with
     631              [ ACC_A ⇒ λacc_a: True. λEQaddr.
     632                let s' ≝ add_ticks1 s in
     633                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
     634                 set_arg_8 … s' ACC_A result
     635              | REGISTER r ⇒ λregister: True. λEQaddr.
     636                let s' ≝ add_ticks1 s in
     637                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
     638                 set_arg_8 … s' (REGISTER r) result
     639              | DIRECT d ⇒ λdirect: True. λEQaddr.
     640                let s' ≝ add_ticks1 s in
     641                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
     642                 set_arg_8 … s' (DIRECT d) result
     643              | INDIRECT i ⇒ λindirect: True. λEQaddr.
     644                let s' ≝ add_ticks1 s in
     645                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
     646                 set_arg_8 … s' (INDIRECT i) result
     647              | DPTR ⇒ λdptr: True. λEQaddr.
     648                let s' ≝ add_ticks1 s in
     649                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
     650                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
     651                let s ≝ set_8051_sfr … s' SFR_DPL bl in
     652                 set_8051_sfr … s' SFR_DPH bu
     653              | _ ⇒ λother: False. ⊥
     654              ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr))
     655        | NOP ⇒ λinstr_refl.
     656           let s ≝ add_ticks2 s in
     657            s
     658        | DEC addr ⇒ λinstr_refl.
     659           let s ≝ add_ticks1 s in
     660           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
     661             set_arg_8 … s addr result
     662        | MUL addr1 addr2 ⇒ λinstr_refl.
     663           let s ≝ add_ticks1 s in
     664           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
     665           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
     666           let product ≝ acc_a_nat * acc_b_nat in
     667           let ov_flag ≝ product ≥ 256 in
     668           let low ≝ bitvector_of_nat 8 (product mod 256) in
     669           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
     670           let s ≝ set_8051_sfr … s SFR_ACC_A low in
     671             set_8051_sfr … s SFR_ACC_B high
     672        | DIV addr1 addr2 ⇒ λinstr_refl.
     673           let s ≝ add_ticks1 s in
     674           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
     675           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
     676             match acc_b_nat with
     677               [ O ⇒ set_flags … s false (None Bit) true
     678               | S o ⇒
     679                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
     680                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
     681                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
     682                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
     683                   set_flags … s false (None Bit) false
     684               ]
     685        | DA addr ⇒ λinstr_refl.
     686            let s ≝ add_ticks1 s in
     687            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
     688              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
     689                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
     690                let cy_flag ≝ get_index' ? O ? flags in
     691                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
     692                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
     693                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
     694                    let new_acc ≝ nu @@ acc_nl' in
     695                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
     696                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
     697                  else
     698                    s
     699              else
     700                s
     701        | CLR addr ⇒ λinstr_refl.
     702          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with
     703            [ ACC_A ⇒ λacc_a: True. λEQaddr.
     704              let s ≝ add_ticks1 s in
     705               set_arg_8 … s ACC_A (zero 8)
     706            | CARRY ⇒ λcarry: True. λEQaddr.
     707              let s ≝ add_ticks1 s in
     708               set_arg_1 … s CARRY false
     709            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
     710              let s ≝ add_ticks1 s in
     711               set_arg_1 … s (BIT_ADDR b) false
     712            | _ ⇒ λother: False. ⊥
     713            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
     714        | CPL addr ⇒ λinstr_refl.
     715          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with
     716            [ ACC_A ⇒ λacc_a: True. λEQaddr.
     717                let s ≝ add_ticks1 s in
     718                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     719                let new_acc ≝ negation_bv ? old_acc in
     720                 set_8051_sfr … s SFR_ACC_A new_acc
     721            | CARRY ⇒ λcarry: True. λEQaddr.
     722                let s ≝ add_ticks1 s in
     723                let old_cy_flag ≝ get_arg_1 … s CARRY true in
     724                let new_cy_flag ≝ ¬old_cy_flag in
     725                 set_arg_1 … s CARRY new_cy_flag
     726            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
     727                let s ≝ add_ticks1 s in
     728                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
     729                let new_bit ≝ ¬old_bit in
     730                 set_arg_1 … s (BIT_ADDR b) new_bit
     731            | _ ⇒ λother: False. ?
     732            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
     733        | SETB b ⇒ λinstr_refl.
     734            let s ≝ add_ticks1 s in
     735            set_arg_1 … s b false
     736        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     737            let s ≝ add_ticks1 s in
     738            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     739            let new_acc ≝ rotate_left … 1 old_acc in
     740              set_8051_sfr … s SFR_ACC_A new_acc
     741        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     742            let s ≝ add_ticks1 s in
     743            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     744            let new_acc ≝ rotate_right … 1 old_acc in
     745              set_8051_sfr … s SFR_ACC_A new_acc
     746        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     747            let s ≝ add_ticks1 s in
     748            let old_cy_flag ≝ get_cy_flag ?? s in
     749            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     750            let new_cy_flag ≝ get_index' ? O ? old_acc in
     751            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
     752            let s ≝ set_arg_1 … s CARRY new_cy_flag in
     753              set_8051_sfr … s SFR_ACC_A new_acc
     754        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     755            let s ≝ add_ticks1 s in
     756            let old_cy_flag ≝ get_cy_flag ?? s in
     757            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     758            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
     759            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
     760            let s ≝ set_arg_1 … s CARRY new_cy_flag in
     761              set_8051_sfr … s SFR_ACC_A new_acc
     762        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
     763            let s ≝ add_ticks1 s in
     764            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     765            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
     766            let new_acc ≝ nl @@ nu in
     767              set_8051_sfr … s SFR_ACC_A new_acc
     768        | PUSH addr ⇒ λinstr_refl.
     769            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x=addr → Σs': PreStatus m cm. ? with
     770              [ DIRECT d ⇒ λdirect: True. λEQaddr.
     771                let s ≝ add_ticks1 s in
     772                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     773                let s ≝ set_8051_sfr … s SFR_SP new_sp in
     774                  write_at_stack_pointer … s d
     775              | _ ⇒ λother: False. ⊥
     776              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
     777        | POP addr ⇒ λinstr_refl.
     778            let s ≝ add_ticks1 s in
     779            let contents ≝ read_at_stack_pointer ?? s in
     780            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     781            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     782              set_arg_8 … s addr contents
     783        | XCH addr1 addr2 ⇒ λinstr_refl.
     784            let s ≝ add_ticks1 s in
     785            let old_addr ≝ get_arg_8 … s false addr2 in
     786            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     787            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
     788              set_arg_8 … s addr2 old_acc
     789        | XCHD addr1 addr2 ⇒ λinstr_refl.
     790            let s ≝ add_ticks1 s in
     791            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
     792            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
     793            let new_acc ≝ acc_nu @@ arg_nl in
     794            let new_arg ≝ arg_nu @@ acc_nl in
     795            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
     796              set_arg_8 … s addr2 new_arg
     797        | RET ⇒ λinstr_refl.
     798            let s ≝ add_ticks1 s in
     799            let high_bits ≝ read_at_stack_pointer ?? s in
     800            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     801            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     802            let low_bits ≝ read_at_stack_pointer ?? s in
     803            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     804            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     805            let new_pc ≝ high_bits @@ low_bits in
     806              set_program_counter … s new_pc
     807        | RETI ⇒ λinstr_refl.
     808            let s ≝ add_ticks1 s in
     809            let high_bits ≝ read_at_stack_pointer ?? s in
     810            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     811            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     812            let low_bits ≝ read_at_stack_pointer ?? s in
     813            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
     814            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     815            let new_pc ≝ high_bits @@ low_bits in
     816              set_program_counter … s new_pc
     817        | MOVX addr ⇒ λinstr_refl.
     818          let s ≝ add_ticks1 s in
     819          (* DPM: only copies --- doesn't affect I/O *)
     820          match addr with
     821            [ inl l ⇒
     822              let 〈addr1, addr2〉 ≝ l in
     823                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     824            | inr r ⇒
     825              let 〈addr1, addr2〉 ≝ r in
     826                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     827            ]
     828        | MOV addr ⇒ λinstr_refl.
     829          let s ≝ add_ticks1 s in
     830          match addr with
     831            [ inl l ⇒
     832              match l with
     833                [ inl l' ⇒
     834                  match l' with
     835                    [ inl l'' ⇒
     836                      match l'' with
     837                        [ inl l''' ⇒
     838                          match l''' with
     839                            [ inl l'''' ⇒
     840                              let 〈addr1, addr2〉 ≝ l'''' in
     841                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     842                            | inr r'''' ⇒
     843                              let 〈addr1, addr2〉 ≝ r'''' in
     844                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     845                            ]
     846                        | inr r''' ⇒
     847                          let 〈addr1, addr2〉 ≝ r''' in
     848                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
     849                        ]
     850                    | inr r'' ⇒
     851                      let 〈addr1, addr2〉 ≝ r'' in
     852                       set_arg_16 … s (get_arg_16 … s addr2) addr1
     853                    ]
     854                | inr r ⇒
     855                  let 〈addr1, addr2〉 ≝ r in
     856                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
     857                ]
     858            | inr r ⇒
     859              let 〈addr1, addr2〉 ≝ r in
     860               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
     861            ]
     862          | JC addr ⇒ λinstr_refl.
     863                  if get_cy_flag ?? s then
     864                    let s ≝ add_ticks1 s in
     865                      set_program_counter … s (addr_of addr s)
     866                  else
     867                    let s ≝ add_ticks2 s in
     868                      s
     869            | JNC addr ⇒ λinstr_refl.
     870                  if ¬(get_cy_flag ?? s) then
     871                   let s ≝ add_ticks1 s in
     872                     set_program_counter … s (addr_of addr s)
     873                  else
     874                   let s ≝ add_ticks2 s in
     875                    s
     876            | JB addr1 addr2 ⇒ λinstr_refl.
     877                  if get_arg_1 … s addr1 false then
     878                   let s ≝ add_ticks1 s in
     879                    set_program_counter … s (addr_of addr2 s)
     880                  else
     881                   let s ≝ add_ticks2 s in
     882                    s
     883            | JNB addr1 addr2 ⇒ λinstr_refl.
     884                  if ¬(get_arg_1 … s addr1 false) then
     885                   let s ≝ add_ticks1 s in
     886                    set_program_counter … s (addr_of addr2 s)
     887                  else
     888                   let s ≝ add_ticks2 s in
     889                    s
     890            | JBC addr1 addr2 ⇒ λinstr_refl.
     891                  let s ≝ set_arg_1 … s addr1 false in
     892                    if get_arg_1 … s addr1 false then
     893                     let s ≝ add_ticks1 s in
     894                      set_program_counter … s (addr_of addr2 s)
     895                    else
     896                     let s ≝ add_ticks2 s in
     897                      s
     898            | JZ addr ⇒ λinstr_refl.
     899                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
     900                     let s ≝ add_ticks1 s in
     901                      set_program_counter … s (addr_of addr s)
     902                    else
     903                     let s ≝ add_ticks2 s in
     904                      s
     905            | JNZ addr ⇒ λinstr_refl.
     906                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
     907                     let s ≝ add_ticks1 s in
     908                      set_program_counter … s (addr_of addr s)
     909                    else
     910                     let s ≝ add_ticks2 s in
     911                      s
     912            | CJNE addr1 addr2 ⇒ λinstr_refl.
     913                  match addr1 with
     914                    [ inl l ⇒
     915                        let 〈addr1, addr2'〉 ≝ l in
     916                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
     917                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
     918                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
     919                            let s ≝ add_ticks1 s in
     920                            let s ≝ set_program_counter … s (addr_of addr2 s) in
     921                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
     922                          else
     923                            let s ≝ add_ticks2 s in
     924                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
     925                    | inr r' ⇒
     926                        let 〈addr1, addr2'〉 ≝ r' in
     927                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
     928                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
     929                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
     930                            let s ≝ add_ticks1 s in
     931                            let s ≝ set_program_counter … s (addr_of addr2 s) in
     932                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
     933                          else
     934                            let s ≝ add_ticks2 s in
     935                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
     936                    ]
     937            | DJNZ addr1 addr2 ⇒ λinstr_refl.
     938              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
     939              let s ≝ set_arg_8 … s addr1 result in
     940                if ¬(eq_bv ? result (zero 8)) then
     941                 let s ≝ add_ticks1 s in
     942                  set_program_counter … s (addr_of addr2 s)
     943                else
     944                 let s ≝ add_ticks2 s in
     945                  s
     946            ] (refl … instr).
     947    try (cases(other))
     948    try assumption (*20s*)
     949    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
     950    try (
     951      @(execute_1_technical … (subaddressing_modein …))
     952      @I
     953    ) (*66s*)
     954    whd in match execute_1_preinstruction;
    535955    normalize nodelta %
    536     try (<instr_refl change with (cl_jump = cl_other → ?) #absurd destruct(absurd))
    537     try (<instr_refl change with (cl_return = cl_other → ?) #absurd destruct(absurd))
     956    [21,22,23,24: (* DIV *)
     957     normalize nodelta in p;
     958    |7,8,9,10,11,12,13,14,15,16, (* INC *)
     959     71,72,73,74,75,76, (* CLR *)
     960     77,78,79,80,81,82, (* CPL *)
     961     99,100: (* PUSH *)
     962      lapply (subaddressing_modein ???) <EQaddr normalize nodelta #b
     963    |93,94: (* MOV *)
     964      cases addr * normalize nodelta
     965       [1,2,4,5: * normalize nodelta
     966        [1,2,4,5: * normalize nodelta
     967         [1,2,4,5: * normalize nodelta
     968          [1,2,4,5: * normalize nodelta ]]]]
     969       #arg1 #arg2
     970    |65,66, (* ANL *)
     971     67,68, (* ORL *)
     972     95,96: (* MOVX*)
     973      cases addr * try (change with (? × ? → ?) * normalize nodelta) #addr11 #addr12 normalize nodelta
     974    |59,60: (* CJNE *)
     975      cases addr1 normalize nodelta * #addr11 #addr12 normalize nodelta
     976      cases (¬(eq_bv ???)) normalize nodelta
     977    |69,70: (* XRL *)
     978      cases addr normalize nodelta * #addr1 #addr2 normalize nodelta
     979    ]
     980    try (>p normalize nodelta
     981         try (>p1 normalize nodelta
     982              try (>p2 normalize nodelta
     983                   try (>p3 normalize nodelta
     984                        try (>p4 normalize nodelta
     985                             try (>p5 normalize nodelta))))))
     986    try (change with (cl_jump = cl_other → ?) #absurd destruct(absurd))
     987    try (change with (cl_return = cl_other → ?) #absurd destruct(absurd))
    538988    try (@or_introl //)
    539989    try (@or_intror //)
    540     #_ /demod/ %
    541 qed.
    542 
    543 definition execute_1_preinstruction:
    544   ∀ticks: nat × nat.
    545   ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a →
    546   PreStatus m cm → PreStatus m cm ≝ execute_1_preinstruction'.
    547  
     990    try (#_ /demod/ %)
     991    try (#_ //)   
     992    [ <set_arg_8_ok @or_introl //
     993    |*: <set_arg_1_ok @or_introl // ]
     994qed.
     995
    548996lemma execute_1_preinstruction_ok:
    549997 ∀ticks,a,m,cm,f,i,s.
     
    551999  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s) ∧
    5521000    (ASM_classify00 a i = cl_other → program_counter ?? (execute_1_preinstruction ticks a m cm f i s) = program_counter … s).
    553  #ticks #a #m #cm #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2
     1001 #ticks #a #m #cm #f #i #s cases (execute_1_preinstruction_ok' ticks a m cm f i s) //
    5541002qed.
    5551003
Note: See TracChangeset for help on using the changeset viewer.