Ignore:
Timestamp:
Jul 16, 2012, 5:19:06 PM (8 years ago)
Author:
mulligan
Message:

Work from today on the big proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2183 r2187  
    130130  ∀M', cm.
    131131  ∀sigma, status, b.
    132   ∀addr1: [[acc_a; registr; direct; indirect; data]]. (* XXX: expand as needed *)
     132  ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr]]. (* XXX: expand as needed *)
    133133    addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
    134134      map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status addr1 b = b.
     
    154154    #w whd in ⊢ (??%? → ??%?);
    155155    cases daemon (* XXX: ??? *)
    156   |5:
     156  |5,6:
    157157    #w #_ %
    158158  ]
     
    191191qed.
    192192
     193lemma get_ac_flag_status_of_pseudo_status:
     194  ∀M: internal_pseudo_address_map.
     195  ∀sigma: Word → Word.
     196  ∀policy: Word → bool.
     197  ∀code_memory: pseudo_assembly_program.
     198  ∀s: PreStatus ? code_memory.
     199  ∀s'.
     200    status_of_pseudo_status M code_memory s sigma policy = s' →
     201      get_ac_flag ?? s' = get_ac_flag ? code_memory s.
     202  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
     203  whd in match get_ac_flag; normalize nodelta
     204  whd in match status_of_pseudo_status; normalize nodelta
     205  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     206  cases (\snd M) try %
     207  * normalize nodelta #address
     208  @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
     209  whd in match sfr_8051_index; normalize nodelta
     210  >get_index_v_set_index_miss [2,4: /2/] %
     211qed.
     212
     213lemma get_cy_flag_status_of_pseudo_status:
     214  ∀M: internal_pseudo_address_map.
     215  ∀sigma: Word → Word.
     216  ∀policy: Word → bool.
     217  ∀code_memory: pseudo_assembly_program.
     218  ∀s: PreStatus ? code_memory.
     219  ∀s'.
     220    status_of_pseudo_status M code_memory s sigma policy = s' →
     221      get_cy_flag ?? s' = get_cy_flag ? code_memory s.
     222  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
     223  whd in match get_cy_flag; normalize nodelta
     224  whd in match status_of_pseudo_status; normalize nodelta
     225  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     226  cases (\snd M) try %
     227  * normalize nodelta #address
     228  @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
     229  whd in match sfr_8051_index; normalize nodelta
     230  >get_index_v_set_index_miss [2,4: /2/] %
     231qed.
     232
     233lemma get_ov_flag_status_of_pseudo_status:
     234  ∀M: internal_pseudo_address_map.
     235  ∀sigma: Word → Word.
     236  ∀policy: Word → bool.
     237  ∀code_memory: pseudo_assembly_program.
     238  ∀s: PreStatus ? code_memory.
     239  ∀s'.
     240    status_of_pseudo_status M code_memory s sigma policy = s' →
     241      get_ov_flag ?? s' = get_ov_flag ? code_memory s.
     242  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
     243  whd in match get_ov_flag; normalize nodelta
     244  whd in match status_of_pseudo_status; normalize nodelta
     245  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     246  cases (\snd M) try %
     247  * normalize nodelta #address
     248  @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
     249  whd in match sfr_8051_index; normalize nodelta
     250  >get_index_v_set_index_miss [2,4: /2/] %
     251qed.
     252
    193253lemma match_nat_status_of_pseudo_status:
    194254  ∀M, cm, sigma, policy, s, s', s'', s'''.
     
    232292      match l with [ O ⇒ o | S n ⇒ p ] = match r with [ O ⇒ o' | S n' ⇒ p' ].
    233293  #l #o #o #r #o' #p' #lr_refl #o_refl #p_refl >lr_refl >o_refl >p_refl %
     294qed.
     295
     296lemma conjunction_split:
     297  ∀l, l', r, r': bool.
     298    l = l' → r = r' → (l ∧ r) = (l' ∧ r').
     299  #l #l' #r #r' #l_refl #r_refl <l_refl <r_refl %
    234300qed.
    235301
     
    873939      |2:
    874940        @set_flags_status_of_pseudo_status try %
    875         @sym_eq @set_arg_8_status_of_pseudo_status
     941        @sym_eq @(set_arg_8_status_of_pseudo_status … (refl …))
    876942        [1:
    877943          @sym_eq @set_clock_status_of_pseudo_status %
     
    9721038          |2:
    9731039            change with (get_ac_flag ??? = get_ac_flag ???)
    974             (* XXX: requires get_ac_flag_status_of_pseudo_status *)
    975             cases daemon
     1040            @(get_ac_flag_status_of_pseudo_status M')
     1041            @sym_eq @set_clock_status_of_pseudo_status
     1042            >EQs >EQticks <instr_refl %
    9761043          ]
    9771044        |2:
     
    9931060            @set_flags_status_of_pseudo_status try %
    9941061            [1:
    995               @eq_f @sym_eq cases daemon
    996               (* XXX: get_ac_flag_status_of_pseudo_status *)
     1062              @eq_f @(get_ac_flag_status_of_pseudo_status M')
     1063              @sym_eq @set_8051_sfr_status_of_pseudo_status
     1064              [1:
     1065                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
     1066              |2:
     1067                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1068              ]
    9971069            |2:
    998               @sym_eq cases daemon
    999               (* XXX: get_ov_flag_status_of_pseudo_status *)
     1070              @(get_ov_flag_status_of_pseudo_status M')
     1071              @sym_eq @set_8051_sfr_status_of_pseudo_status
     1072              [1:
     1073                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
     1074              |2:
     1075                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1076              ]
    10001077            |3:
    10011078              @sym_eq @set_8051_sfr_status_of_pseudo_status
     
    10451122          |2:
    10461123            change with (get_ac_flag ??? = get_ac_flag ???)
    1047             (* XXX: requires get_ac_flag_status_of_pseudo_status *)
    1048             cases daemon
     1124            @(get_ac_flag_status_of_pseudo_status M')
     1125            @sym_eq @set_clock_status_of_pseudo_status
     1126            >EQs >EQticks <instr_refl %
    10491127          ]
    10501128        |2:
     
    11021180          |2:
    11031181            change with (get_ac_flag ??? = get_ac_flag ???)
    1104             (* XXX: requires get_ac_flag_status_of_pseudo_status *)
    1105             cases daemon
     1182            @(get_ac_flag_status_of_pseudo_status M')
     1183            @sym_eq @set_clock_status_of_pseudo_status
     1184            >EQs >EQticks <instr_refl %
    11061185          ]
    11071186        |2:
     
    11171196      ]
    11181197    ]
     1198  |36: (* CLR *)
     1199    >EQP -P normalize nodelta
     1200    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1201    whd in maps_assm:(??%%);
     1202    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1203    [2: normalize nodelta #absurd destruct(absurd) ]
     1204    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1205    whd in ⊢ (??%?);
     1206    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1207    whd in ⊢ (??%?); normalize nodelta
     1208    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
     1209    normalize nodelta #subaddressing_modein_witness
     1210    @set_arg_8_status_of_pseudo_status try %
     1211    [1:
     1212      @sym_eq @set_clock_status_of_pseudo_status
     1213      >EQs >EQticks <instr_refl %
     1214    |2:
     1215      whd in ⊢ (??%?);
     1216      >(addressing_mode_ok_to_snd_M_data M' cm … addr addressing_mode_ok_assm_1)
     1217      [2: <EQaddr % ] %
     1218    ]
     1219  |37: (* CLR *)
     1220    >EQP -P normalize nodelta
     1221    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1222    whd in maps_assm:(??%%);
     1223    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1224    [2: normalize nodelta #absurd destruct(absurd) ]
     1225    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1226    whd in ⊢ (??%?);
     1227    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1228    whd in ⊢ (??%?); normalize nodelta
     1229    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
     1230    normalize nodelta #subaddressing_modein_witness
     1231    @set_arg_1_status_of_pseudo_status try %
     1232    @sym_eq @set_clock_status_of_pseudo_status
     1233    >EQs >EQticks <instr_refl %
     1234  |38: (* CLR *)
     1235    >EQP -P normalize nodelta
     1236    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1237    whd in maps_assm:(??%%);
     1238    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1239    [2: normalize nodelta #absurd destruct(absurd) ]
     1240    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1241    whd in ⊢ (??%?);
     1242    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1243    whd in ⊢ (??%?); normalize nodelta
     1244    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
     1245    normalize nodelta #subaddressing_modein_witness
     1246    @set_arg_1_status_of_pseudo_status try %
     1247    [1:
     1248      @sym_eq @set_clock_status_of_pseudo_status
     1249      >EQs >EQticks <instr_refl %
     1250    |*:
     1251      (* XXX: ??? *)
     1252      cases daemon
     1253    ]
     1254  |39: (* CPL *)
     1255    >EQP -P normalize nodelta
     1256    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1257    whd in maps_assm:(??%%);
     1258    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1259    [2: normalize nodelta #absurd destruct(absurd) ]
     1260    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1261    whd in ⊢ (??%?);
     1262    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1263    whd in ⊢ (??%?); normalize nodelta
     1264    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
     1265    normalize nodelta #subaddressing_modein_witness
     1266    @set_8051_sfr_status_of_pseudo_status
     1267    [1:
     1268      @sym_eq @set_clock_status_of_pseudo_status
     1269      >EQs >EQticks <instr_refl %
     1270    |2:
     1271      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data M' cm … addr addressing_mode_ok_assm_1)
     1272      [2: <EQaddr % ] normalize nodelta @eq_f
     1273      @sym_eq @(get_8051_sfr_status_of_pseudo_status M')
     1274     
     1275    ]
     1276   
     1277  |33: (* (* ANL *)
     1278    (* XXX: work on the right hand side *)
     1279    (* XXX: switch to the left hand side *)
     1280    >EQP -P normalize nodelta lapply instr_refl
     1281    inversion addr
     1282    [1:
     1283      #addr' #addr_refl'
     1284      inversion addr'
     1285      #instr_refl #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} lapply maps_assm
     1286      whd in ⊢ (??%? → ?); normalize nodelta cases addr
     1287      [1:
     1288        #acc_a #others normalize nodelta
     1289        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1
     1290        [2: normalize nodelta #absurd destruct(absurd) ]
     1291        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1292        [2: normalize nodelta #absurd destruct(absurd) ]
     1293        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1294        whd in ⊢ (??%?);
     1295        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1296        whd in ⊢ (??%?); normalize nodelta
     1297        inversion addr #addr1 #addr2
     1298        @(subaddressing_mode_elim … addr1) @(subaddressing_mode_elim … acc_a)
     1299        @(subaddressing_mode_elim … addr2)
     1300        @set_arg_8_status_of_pseudo_status #addr_refl normalize nodelta try %
     1301        [1:
     1302          @sym_eq @set_clock_status_of_pseudo_status
     1303          >EQs >EQticks <addr_refl <instr_refl
     1304          [1:
     1305            @sym_eq @set_program_counter_status_of_pseudo_status %
     1306          |2:
     1307            @eq_f2
     1308            [1:
     1309              >addr_refl @(subaddressing_mode_elim … addr1) %
     1310            |2:
     1311              @(clock_status_of_pseudo_status M')
     1312              @sym_eq @set_program_counter_status_of_pseudo_status %
     1313            ]
     1314          ]
     1315        |2:
     1316          cases daemon (* XXX: matita dies here *)
     1317        ]
     1318      |2:
     1319        #direct #others
     1320        @pair_elim #direct' #others' #direct_others_refl' destruct(direct_others_refl') normalize nodelta
     1321        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1
     1322        [2: normalize nodelta #absurd destruct(absurd) ]
     1323        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1324        [2: normalize nodelta #absurd destruct(absurd) ]
     1325        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1326        whd in ⊢ (??%?);
     1327        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1328        whd in ⊢ (??%?); normalize nodelta
     1329        inversion addr #addr1 #addr2
     1330        @(subaddressing_mode_elim … addr1) @(subaddressing_mode_elim … addr2)
     1331        [1: #w |2: #w1 #w2 ] #addr_refl normalize nodelta
     1332        @set_arg_8_status_of_pseudo_status
     1333      ]
     1334    |2:
     1335      -addr #addr #instr_refl #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} lapply maps_assm
     1336      whd in ⊢ (??%? → ?); normalize nodelta cases addr #carry #others normalize nodelta
     1337      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1
     1338      [2: normalize nodelta #absurd destruct(absurd) ]
     1339      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1340      [2: normalize nodelta #absurd destruct(absurd) ]
     1341      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1342      whd in ⊢ (??%?);
     1343      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1344      whd in ⊢ (??%?); normalize nodelta
     1345      inversion addr #addr1 #addr2 #addr_refl normalize nodelta
     1346      @set_flags_status_of_pseudo_status try %
     1347      [1:
     1348        @conjunction_split
     1349        [1:
     1350          @(get_cy_flag_status_of_pseudo_status M')
     1351          @sym_eq @set_clock_status_of_pseudo_status
     1352          >EQs >EQticks <addr_refl <instr_refl %
     1353        |2:
     1354          >EQs >EQticks <addr_refl <instr_refl normalize nodelta
     1355          (* XXX: can't get get_arg_1_status_of_pseudo_status to apply *)
     1356          cases daemon
     1357        ]
     1358      |2:
     1359        @(get_ov_flag_status_of_pseudo_status M')
     1360        @sym_eq @set_clock_status_of_pseudo_status
     1361        >EQs >EQticks <instr_refl <addr_refl %
     1362      |3:
     1363        @sym_eq @set_clock_status_of_pseudo_status
     1364        >EQs >EQticks <instr_refl <addr_refl %
     1365      ]
     1366    ]
     1367    whd in maps_assm:(??%%);
     1368    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1369    [2: normalize nodelta #absurd destruct(absurd) ]
     1370    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1371    whd in ⊢ (??%?);
     1372    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1373    whd in ⊢ (??%?); normalize nodelta
    11191374  |16: (* JC *)
    11201375    (* XXX: work on the right hand side *)
Note: See TracChangeset for help on using the changeset viewer.