Changeset 2023


Ignore:
Timestamp:
Jun 7, 2012, 2:08:18 PM (5 years ago)
Author:
mulligan
Message:

Closed main lemma modulo closing trivial subgoals about commutations and addressing modes being in vectors of addressing modes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2020 r2023  
    311311qed.
    312312
     313lemma set_program_counter_set_program_counter:
     314  ∀M: Type[0].
     315  ∀cm: M.
     316  ∀s: PreStatus M cm.
     317  ∀pc: Word.
     318  ∀pc': Word.
     319    set_program_counter M cm (set_program_counter M cm s pc) pc' =
     320      set_program_counter M cm s pc'.
     321  #M #cm #s #pc #pc' %
     322qed.
     323
    313324lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
    314325 #P #A #a #abs destruct
     
    397408
    398409lemma main_lemma_preinstruction:
    399  ∀M,M': internal_pseudo_address_map.
    400  ∀preamble : preamble. ∀instr_list : list labelled_instruction.
    401  ∀cm: pseudo_assembly_program.
    402  ∀EQcm: cm = 〈preamble,instr_list〉.
    403  ∀sigma : Word→Word. ∀policy : Word→bool.
    404  ∀sigma_policy_witness : sigma_policy_specification cm sigma policy.
    405  ∀ps : PseudoStatus cm.
    406  ∀ppc : Word.
    407  ∀EQppc : ppc=program_counter pseudo_assembly_program cm ps.
    408  ∀labels : label_map.
    409  ∀costs : BitVectorTrie costlabel 16.
    410  ∀create_label_cost_refl : create_label_cost_map instr_list=〈labels,costs〉.
    411  ∀newppc : Word.
    412  ∀lookup_labels : Identifier→Word.
    413  ∀EQlookup_labels : lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x).
    414  ∀lookup_datalabels : identifier ASMTag→Word.
    415  ∀EQlookup_datalabels : lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
    416  ∀EQnewppc : newppc=add 16 ppc (bitvector_of_nat 16 1).
    417  ∀instr: preinstruction Identifier.
    418  ∀ticks.
    419  ∀EQticks: ticks = ticks_of0 〈preamble,instr_list〉 sigma policy ppc (Instruction instr).
    420  ∀addr_of.
    421  ∀EQaddr_of: addr_of = (λx:Identifier
    422          .λy:PreStatus pseudo_assembly_program cm
    423           .address_of_word_labels cm x).
    424  ∀s.
    425  ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps
    426          (add 16 ppc (bitvector_of_nat 16 1))).
    427  ∀P.
    428  ∀EQP: P = (λinstr, s.
    429   sigma (add 16 ppc (bitvector_of_nat 16 1))
    430    =add 16 (sigma ppc)
    431     (bitvector_of_nat 16
    432      (\fst  (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
    433                   lookup_datalabels (Instruction instr))))
    434    →next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr)
    435     M cm ps
    436     =Some internal_pseudo_address_map M'
    437     →fetch_many (load_code_memory (\fst  (assembly cm sigma policy)))
    438      (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps))
    439      (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels
    440       (Instruction instr))
    441      → ∃n. execute n
    442        (code_memory_of_pseudo_assembly_program cm sigma
    443         policy)
    444        (status_of_pseudo_status M cm ps sigma policy)
    445       =status_of_pseudo_status M' cm s sigma policy).
    446      P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm
    447          addr_of instr s).
    448  #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
    449  #costs #create_label_cost_refl #newppc
    450  #lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr
    451  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
    452  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
    453  letin a ≝ Identifier letin m ≝ pseudo_assembly_program
    454  cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
    455  [2: * // ]
    456  @(
     410  ∀M, M': internal_pseudo_address_map.
     411  ∀preamble: preamble.
     412  ∀instr_list: list labelled_instruction.
     413  ∀cm: pseudo_assembly_program.
     414  ∀EQcm: cm = 〈preamble, instr_list〉.
     415  ∀sigma: Word → Word.
     416  ∀policy: Word → bool.
     417  ∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
     418  ∀ps: PseudoStatus cm.
     419  ∀ppc: Word.
     420  ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
     421  ∀labels: label_map.
     422  ∀costs: BitVectorTrie costlabel 16.
     423  ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
     424  ∀newppc: Word.
     425  ∀lookup_labels: Identifier → Word.
     426  ∀EQlookup_labels: lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x).
     427  ∀lookup_datalabels: Identifier → Word.
     428  ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
     429  ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
     430  ∀instr: preinstruction Identifier.
     431  ∀ticks: nat × nat.
     432  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr).
     433  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
     434  ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
     435  ∀s: PreStatus pseudo_assembly_program cm.
     436  ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
     437  ∀P: preinstruction Identifier → PseudoStatus cm → Prop.
     438  ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
     439              (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
     440                  lookup_datalabels (Instruction instr)))) →
     441              next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cm ps = Some internal_pseudo_address_map M' →
     442                fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps))
     443                  (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
     444                    ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
     445                      status_of_pseudo_status M' cm s sigma policy).
     446    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
     447  #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
     448  #costs #create_label_cost_refl #newppc
     449  #lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr
     450  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
     451  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
     452  letin a ≝ Identifier letin m ≝ pseudo_assembly_program
     453  cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
     454  [2: * // ]
     455  @(
    457456  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
    458457  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
     
    860859  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    861860  whd in match execute_1_preinstruction; normalize nodelta
    862   [31: (* DJNZ *)
     861  [31,32: (* DJNZ *)
    863862  (* XXX: work on the right hand side *)
    864863  >p normalize nodelta
     
    872871  @pair_elim #upper #lower #split_refl
    873872  cases (eq_bv ???) normalize nodelta
    874   [1:
     873  [1,3:
    875874    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    876875    whd in ⊢ (??%?);
    877876    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    878877    (* XXX: work on the left hand side *)
    879     check pair_replace
    880878    @(pair_replace ?????????? p) normalize nodelta
    881     [1:
     879    [1,3:
    882880      cases daemon
    883881    ]
     
    889887    @split_eq_status try %
    890888    cases daemon
    891   |2:
     889  |2,4:
    892890    >EQppc
    893891    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
     
    899897    #status_after_1 #EQstatus_after_1
    900898    <(?: ? = status_after_1)
    901     [3:
     899    [3,6:
    902900      >EQstatus_after_1 in ⊢ (???%);
    903901      whd in ⊢ (???%);
    904       <fetch_refl in ⊢ (???%);
     902      [1:
     903        <fetch_refl in ⊢ (???%);
     904      |2:
     905        <fetch_refl in ⊢ (???%);
     906      ]
    905907      whd in ⊢ (???%);
    906908      @(pair_replace ?????????? p)
    907       [1:
     909      [1,3:
    908910        cases daemon
    909       |2:
     911      |2,4:
    910912        normalize nodelta
    911913        whd in match (addr_of_relative ????);
     
    915917        change with (add ???) in match (\snd (half_add ???));
    916918        >set_arg_8_set_program_counter in ⊢ (???%);
    917         [2,4: cases daemon ]
     919        [2,4,6,8: cases daemon ]
    918920        >program_counter_set_program_counter in ⊢ (???%);
    919921        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
    920         [2,4:
     922        [2,4,6,8:
    921923          >bitvector_of_nat_sign_extension_equivalence
    922           [1,3:
     924          [1,3,5,7:
    923925            >EQintermediate_pc' %
    924926          |*:
     
    926928          ]
    927929        ]
    928         [1: % ]
     930        [1,3: % ]
    929931      ]
    930     |1:
     932    |1,4:
    931933      skip
    932934    ]
    933     [2:
     935    [3,4:
    934936      -status_after_1
    935937      @(pose … (execute_1 ? (mk_PreStatus …)))
    936938      #status_after_1 #EQstatus_after_1
    937939      <(?: ? = status_after_1)
    938       [3:
     940      [3,6:
    939941        >EQstatus_after_1 in ⊢ (???%);
    940942        whd in ⊢ (???%);
    941943        (* XXX: matita bug with patterns across multiple goals *)
    942         <fetch_refl'' in ⊢ (???%);
    943         whd in ⊢ (???%); %
    944     |1:
    945       skip
     944        [1:
     945          <fetch_refl'' in ⊢ (???%);
     946        |2:
     947          <fetch_refl'' in ⊢ (???%);
     948        ]
     949        [2: % |1: whd in ⊢ (???%); % ]
     950      |1,4:
     951        skip
     952      ]
     953      -status_after_1 whd in ⊢ (??%?);
     954      (* XXX: switch to the right hand side *)
     955      normalize nodelta >EQs -s >EQticks -ticks
     956      cases (¬ eq_bv ???) normalize nodelta
     957      whd in ⊢ (??%%);
    946958    ]
    947     -status_after_1 whd in ⊢ (??%?);
    948     (* XXX: switch to the right hand side *)
    949     normalize nodelta >EQs -s >EQticks -ticks
    950     cases (¬ eq_bv ???) normalize nodelta
     959    (* XXX: finally, prove the equality using sigma commutation *)
     960    @split_eq_status try %
    951961    whd in ⊢ (??%%);
     962    cases daemon
    952963  ]
    953   (* XXX: finally, prove the equality using sigma commutation *)
    954   @split_eq_status XXX try %
    955   cases daemon
    956964  |30: (* CJNE *)
    957965  (* XXX: work on the right hand side *)
     
    10551063    (* XXX: finally, prove the equality using sigma commutation *)
    10561064    @split_eq_status try %
    1057     [3:
    1058       whd in ⊢ (??%?);
    1059       cases daemon
    1060     |*:
    1061       cases daemon
    1062     ]
     1065    cases daemon
    10631066  ]
    10641067  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
     
    12381241  (* XXX: finally, prove the equality using sigma commutation *)
    12391242  try @split_eq_status try % whd in ⊢ (??%%);
    1240   [1:
    1241     >low_internal_ram_set_8051_sfr >low_internal_ram_set_clock
    1242     >low_internal_ram_set_program_counter @eq_f2 try %
    1243     whd in maps_assm:(??%?); destruct %
    1244   |2:
    1245     >high_internal_ram_set_8051_sfr >high_internal_ram_set_clock
    1246     >high_internal_ram_set_program_counter @eq_f2 try %
    1247     whd in maps_assm:(??%?); destruct %
    1248   |3:
    1249     >clock_set_program_counter >clock_set_program_counter <instr_refl %
    1250   |4,6:
    1251     >set_clock_set_program_counter >get_arg_8_set_program_counter
    1252     >clock_set_program_counter >set_clock_mk_Status_commutation
    1253     >set_clock_mk_Status_commutation >clock_set_program_counter <instr_refl
    1254   |8:
    1255     cases daemon
    1256   ]
     1243  cases daemon
    12571244  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
    12581245  (* XXX: work on the right hand side *)
     
    12831270  (* XXX: finally, prove the equality using sigma commutation *)
    12841271  try @split_eq_status try %
    1285   >set_clock_mk_Status_commutation
    1286   cases daemon (*
    1287        @split_eq_status try %
    1288        [*: whd in ⊢ (??%%); >set_clock_mk_Status_commutation
    1289            whd in match (set_flags ??????);
    1290            (* CSC: TO BE COMPLETED *)
    1291        ] *)
     1272  cases daemon
    12921273  |10,42,43,44,45,49,52,56: (* MUL *)
    12931274  (* XXX: work on the right hand side *)
     
    14101391  cases daemon
    14111392  ]
    1412 ]
    1413 cases daemon (* XXX: CJNE and DJNZ cases *)
    1414 qed.
    1415 (*   
    1416    
    1417 
    1418     @list_addressing_mode_tags_elim_prop try % whd
    1419     @list_addressing_mode_tags_elim_prop try % whd #arg
    1420     (* XXX: we first work on sigma_increment_commutation *)
    1421     #sigma_increment_commutation
    1422     normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
    1423     (* XXX: we work on the maps *)
    1424     whd in ⊢ (??%? → ?);
    1425     try (change with (if ? then ? else ? = ? → ?)
    1426          cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta)
    1427     #H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm
    1428     (* XXX: we assume the fetch_many hypothesis *)
    1429     #fetch_many_assm
    1430     (* XXX: we give the existential *)
    1431     %{1}
    1432     whd in match (execute_1_pseudo_instruction0 ?????);
    1433     (* XXX: work on the left hand side of the equality *)
    1434     whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
    1435     (* XXX: execute fetches some more *)
    1436     whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    1437     whd in fetch_many_assm;
    1438     >EQassembled in fetch_many_assm;
    1439     cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
    1440     #eq_instr #EQticks whd in EQticks:(???%); >EQticks
    1441     #fetch_many_assm whd in fetch_many_assm;
    1442     lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    1443     >(eq_instruction_to_eq … eq_instr) -instr
    1444     [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs
    1445       @(pose …
    1446         (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy))
    1447       #Pl #EQPl
    1448       cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq
    1449       lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) -XX >EQlhs -lhs
    1450       whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%)));
    1451       @pair_elim
    1452       >tech_pi1_let_as_commute
    1453 
    1454 *) 
    1455 
     1393qed.
    14561394
    14571395theorem main_thm:
Note: See TracChangeset for help on using the changeset viewer.