Changeset 2187 for src


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

Work from today on the big proof.

Location:
src/ASM
Files:
2 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 *)

  • src/ASM/Test.ma

    r2183 r2187  
    713713  ∀cm.
    714714  ∀ps.
    715   ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
     715  ∀addr, addr':[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
    716716  ∀value.
    717717  ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
     718   addr = addr' →
    718719   status_of_pseudo_status M cm ps sigma policy = s' →
    719720   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
    … …  
    722723      (code_memory_of_pseudo_assembly_program cm sigma policy)
    723724      s' addr value' =
    724     status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
    725   #cm #ps #addr #value
     725    status_of_pseudo_status M cm (set_arg_8 … cm ps addr' value) sigma policy.
     726  #cm #ps #addr #addr' #value
    726727  cases (set_arg_8_status_of_pseudo_status' cm ps addr value) #_ #relevant
     728  #M #sigma #policy #s' #value' #addr_refl <addr_refl
    727729  @relevant
    728730qed.
    … …  
    11051107  ∀cm.
    11061108  ∀ps.
    1107   ∀addr: [[bit_addr; n_bit_addr; carry]].
     1109  ∀addr, addr': [[bit_addr; n_bit_addr; carry]].
    11081110  ∀l.
    11091111  ∀M. ∀sigma. ∀policy. ∀s'.
     1112    addr = addr' →
    11101113    status_of_pseudo_status M cm ps sigma policy = s' →
    11111114      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
    11121115      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
    11131116      s' addr l =
    1114       (get_arg_1 … cm ps addr l).
    1115   #cm #ps #addr #l
     1117      (get_arg_1 … cm ps addr' l).
     1118  #cm #ps #addr #addr' #l
    11161119  cases (get_arg_1_status_of_pseudo_status' cm ps addr l) #_ #assm
     1120  #M #sigma #policy #s' #addr_refl <addr_refl
    11171121  @assm
    11181122qed.
Note: See TracChangeset for help on using the changeset viewer.