Changeset 2198


Ignore:
Timestamp:
Jul 17, 2012, 4:27:29 PM (5 years ago)
Author:
mulligan
Message:

Work from today.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2187 r2198  
    101101  ∀cm: pseudo_assembly_program.
    102102  ∀status.
    103   ∀b: BitVector 7.
    104     lookup … b (low_internal_ram … cm status) (zero 8) = false:::b.
     103  ∀b, b': BitVector 7.
     104    b = b' →
     105    lookup … b (low_internal_ram … cm status) (zero 8) = false:::b'.
    105106  #cm * #low_internal_ram #high_internal_ram #external_ram #program_counter
    106   #sfr_8051 #sfr_8052 #p1_latch #p3_latch #clock #b
     107  #sfr_8051 #sfr_8052 #p1_latch #p3_latch #clock #b #b' #b_refl
    107108  cases daemon (* XXX: cannot eliminate, case analyse or invert the BitVectorTrie *)
    108109qed.
    109110
    110111lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr:
    111   ∀M', cm, status, sigma.
     112  ∀M', cm, status, status', sigma.
    112113  ∀addr1: [[acc_a; registr; direct; indirect; data]]. (* XXX: expand as needed *)
     114    status = status' →
    113115    addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
    114     map_address_mode_using_internal_pseudo_address_map_ok1 M' cm status sigma addr1.
    115   #M' #cm #status #sigma #addr1
     116    map_address_mode_using_internal_pseudo_address_map_ok1 M' cm status' sigma addr1.
     117  #M' #cm #status #status' #sigma #addr1 #status_refl <status_refl
    116118  @(subaddressing_mode_elim … addr1) try (#w #_ @I)
    117119  [1: #_ @I ]
     
    123125    #_
    124126    @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
    125     cases w whd in ⊢ (??%%); @lookup_low_internal_ram_false
     127    cases w whd in ⊢ (??%%); @lookup_low_internal_ram_false % (* XXX: dubious *)
    126128  ]
    127129qed.
     
    757759  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    758760  whd in match execute_1_preinstruction; normalize nodelta
    759   [4,5,6,7,8,9: (* INC and DEC *)
     761  [35: (* XRL *)
     762    inversion addr
     763    [1:
     764      #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
     765      >EQP -P normalize nodelta
     766      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     767      whd in maps_assm:(??%%);
     768      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     769      [2: normalize nodelta #absurd destruct(absurd) ]
     770      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     771      [2: normalize nodelta #absurd destruct(absurd) ]
     772      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     773      whd in ⊢ (??%?);
     774      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     775      whd in ⊢ (??%?); normalize nodelta
     776      lapply addr_refl @(subaddressing_mode_elim … acc_a) #addr_refl normalize nodelta
     777      @set_8051_sfr_status_of_pseudo_status
     778      [1:
     779        @sym_eq @set_clock_status_of_pseudo_status
     780        >EQs >EQticks <instr_refl >addr_refl %
     781      |2:
     782        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … acc_a addressing_mode_ok_assm_1)
     783        normalize nodelta @eq_f2
     784        [1:
     785          @(pose … (set_clock ????)) #status #status_refl
     786          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl
     787          >EQs >EQticks <instr_refl >addr_refl
     788          [1:
     789            @sym_eq @set_clock_status_of_pseudo_status try %
     790          |2:
     791            whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … acc_a addressing_mode_ok_assm_1) %
     792          |3:
     793            @I
     794          ]
     795        |2:
     796          @(pose … (set_clock ????)) #status #status_refl
     797          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl
     798          >EQs >EQticks <instr_refl >addr_refl
     799          [1:
     800            @sym_eq @set_clock_status_of_pseudo_status try %
     801          |2:
     802            lapply addressing_mode_ok_assm_2 cases others #addressing_mode cases addressing_mode
     803            try (#w whd in ⊢ (% → ?); #absurd #addressing_mode_ok_assm_2 cases absurd)
     804            try (whd in ⊢ (% → ?); #absurd #addressing_mode_ok_assm_2 cases absurd)
     805            whd in ⊢ (??%?); try % whd in addressing_mode_ok_assm_2:(??%?);
     806            (* XXX: subaddressing_mode_elim is too slow above so do it by hand *)
     807            [1:
     808            |2,3:
     809              lapply addressing_mode_ok_assm_2
     810              inversion (assoc_list_exists ?????) #assoc_list_exists_assm normalize nodelta
     811              [1,3: #absurd destruct(absurd) ] #_
     812              >(assoc_list_exists_false_to_assoc_list_lookup_None ????????? assoc_list_exists_assm) in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? ])?);
     813              %
     814            ]
     815          |3:
     816            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others)
     817            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]
     818            whd in ⊢ (??%?);
     819            lapply addressing_mode_ok_assm_2 cases others #addressing_mode cases addressing_mode
     820            try (#w whd in ⊢ (% → ?); #absurd #addressing_mode_ok_assm_2 cases absurd)
     821            try (whd in ⊢ (% → ?); #absurd #addressing_mode_ok_assm_2 cases absurd)
     822            whd whd in addressing_mode_ok_assm_2:(??%?); try @I
     823            inversion (assoc_list_exists ?????) in addressing_mode_ok_assm_2;
     824            #assoc_list_exists_assm normalize nodelta
     825            [1:
     826              #absurd destruct(absurd)
     827            |2:
     828              #_ @(assoc_list_exists_false_to_assoc_list_lookup_None ????????? assoc_list_exists_assm)
     829              try %
     830              whd in match get_register; normalize nodelta
     831              @lookup_low_internal_ram_false
     832              @eq_f2 try % whd in ⊢ (???%);
     833            ]
     834          ]
     835        ]
     836      ]
     837    |2:
     838    ]
     839  |4,5,6,7,8,9: (* INC and DEC *)
    760840    cases daemon
    761841  |42,44: (* RL and RR *)
     
    12711351      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data M' cm … addr addressing_mode_ok_assm_1)
    12721352      [2: <EQaddr % ] normalize nodelta @eq_f
    1273       @sym_eq @(get_8051_sfr_status_of_pseudo_status M')
    1274      
    1275     ]
    1276    
     1353      @(pose … (set_clock ????)) #status #status_refl
     1354      @sym_eq @(get_8051_sfr_status_of_pseudo_status M' … status) >status_refl
     1355      >EQs >EQticks <instr_refl try %
     1356      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addr addressing_mode_ok_assm_1)
     1357      [2: <EQaddr % ] %
     1358    ]
     1359  |40: (* CPL *)
     1360    >EQP -P normalize nodelta
     1361    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1362    whd in maps_assm:(??%%);
     1363    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1364    [2: normalize nodelta #absurd destruct(absurd) ]
     1365    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1366    whd in ⊢ (??%?);
     1367    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1368    whd in ⊢ (??%?); normalize nodelta
     1369    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
     1370    normalize nodelta #subaddressing_modein_witness
     1371    @set_arg_1_status_of_pseudo_status try %
     1372    [1:
     1373      @eq_f @(get_arg_1_status_of_pseudo_status … M') try %
     1374      @sym_eq @set_clock_status_of_pseudo_status
     1375      >EQs >EQticks <instr_refl <EQaddr %
     1376    |2:
     1377      @sym_eq @set_clock_status_of_pseudo_status
     1378      >EQs >EQticks <instr_refl <EQaddr %
     1379    ]
     1380  |41: (* CPL *)
     1381    >EQP -P normalize nodelta
     1382    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1383    whd in maps_assm:(??%%);
     1384    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1385    [2: normalize nodelta #absurd destruct(absurd) ]
     1386    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1387    whd in ⊢ (??%?);
     1388    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1389    whd in ⊢ (??%?); normalize nodelta
     1390    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
     1391    normalize nodelta #subaddressing_modein_witness
     1392    @set_arg_1_status_of_pseudo_status
     1393    [1:
     1394      @eq_f
     1395      @(pose … (set_clock ????)) #status #status_refl
     1396      @(get_arg_1_status_of_pseudo_status … M' … status) try % >status_refl
     1397      >EQs >EQticks <instr_refl <EQaddr
     1398      [1:
     1399        @sym_eq @set_clock_status_of_pseudo_status %
     1400      |2:
     1401        (* XXX: ??? *)
     1402        cases daemon
     1403      ]
     1404    |2:
     1405      @sym_eq @set_clock_status_of_pseudo_status
     1406      >EQs >EQticks <instr_refl <EQaddr %
     1407    |*:
     1408      (* XXX: same as above, provable but tedious *)
     1409      cases daemon
     1410    ]
    12771411  |33: (* (* ANL *)
    12781412    (* XXX: work on the right hand side *)
     
    13711505    whd in ⊢ (??%?);
    13721506    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1373     whd in ⊢ (??%?); normalize nodelta
     1507    whd in ⊢ (??%?); normalize nodelta *)
    13741508  |16: (* JC *)
    13751509    (* XXX: work on the right hand side *)
     
    14011535          whd in match addr_of_relative; normalize nodelta
    14021536          whd in match (program_counter ???);
     1537          check address_of_word_labels_code_mem_Some_hit
     1538          >EQlookup_labels
     1539         
    14031540          >sigma_increment_commutation
    14041541          whd in match assembly_1_pseudoinstruction; normalize nodelta
     
    14111548          |2:
    14121549            >sj_possible_refl normalize nodelta normalize in match (length ??);
     1550            lapply sigma_increment_commutation
     1551            whd in match assembly_1_pseudoinstruction; normalize nodelta
     1552            whd in match (length ??); normalize nodelta
    14131553            cases daemon
    14141554            (* XXX: missing invariant? *)
Note: See TracChangeset for help on using the changeset viewer.