Ignore:
Timestamp:
May 20, 2012, 10:34:31 PM (7 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.
File:
1 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*)
Note: See TracChangeset for help on using the changeset viewer.