Changeset 2181
 Timestamp:
 Jul 13, 2012, 11:00:04 AM (8 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2173 r2181 35 35 destruct(absurd) 36 36 ] 37 qed. 38 39 lemma addressing_mode_ok_to_snd_M_data: 40 ∀M, cm, ps. 41 ∀addr: [[acc_a]]. 42 addressing_mode_ok pseudo_assembly_program M cm ps addr = true → 43 \snd M = data. 44 #M #addr #ps #addr 45 @(subaddressing_mode_elim … addr) 46 whd in ⊢ (??%? → ?); 47 cases (\snd M) normalize nodelta 48 [2: 49 * #address #absurd destruct(absurd) 50 ] 51 #_ % 52 qed. 53 54 lemma assoc_list_exists_true_to_assoc_list_lookup_Some: 55 ∀A, B: Type[0]. 56 ∀e: A. 57 ∀the_list: list (A × B). 58 ∀eq_f: A → A → bool. 59 assoc_list_exists A B e eq_f the_list = true → 60 ∃e'. assoc_list_lookup A B e eq_f the_list = Some … e'. 61 #A #B #e #the_list #eq_f elim the_list 62 [1: 63 whd in ⊢ (??%? → ?); #absurd destruct(absurd) 64 2: 65 #hd #tl #inductive_hypothesis 66 whd in ⊢ (??%? → ?); whd in match (assoc_list_lookup ?????); 67 cases (eq_f (\fst hd) e) normalize nodelta 68 [1: 69 #_ %{(\snd hd)} % 70 2: 71 @inductive_hypothesis 72 ] 73 ] 74 qed. 75 76 lemma assoc_list_exists_false_to_assoc_list_lookup_None: 77 ∀A, B: Type[0]. 78 ∀e, e': A. 79 ∀the_list, the_list': list (A × B). 80 ∀eq_f: A → A → bool. 81 e = e' → 82 the_list = the_list' → 83 assoc_list_exists A B e eq_f the_list = false → 84 assoc_list_lookup A B e' eq_f the_list' = None …. 85 #A #B #e #e' #the_list elim the_list 86 [1: 87 #the_list' #eq_f #e_refl <e_refl #the_list_refl <the_list_refl #_ % 88 2: 89 #hd #tl #inductive_hypothesis #the_list' #eq_f #e_refl #the_list_refl <the_list_refl 90 whd in ⊢ (??%? → ??%?); <e_refl 91 cases (eq_f (\fst hd) e) normalize nodelta 92 [1: 93 #absurd destruct(absurd) 94 2: 95 >e_refl in ⊢ (? → %); @inductive_hypothesis try % assumption 96 ] 97 ] 98 qed. 99 100 lemma lookup_low_internal_ram_false: 101 ∀cm: pseudo_assembly_program. 102 ∀status. 103 ∀b: BitVector 7. 104 lookup … b (low_internal_ram … cm status) (zero 8) = false:::b. 105 #cm * #low_internal_ram #high_internal_ram #external_ram #program_counter 106 #sfr_8051 #sfr_8052 #p1_latch #p3_latch #clock #b 107 cases daemon (* XXX: cannot eliminate, case analyse or invert the BitVectorTrie *) 108 qed. 109 110 lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr: 111 ∀M', cm, status, sigma. 112 ∀addr1: [[acc_a; registr; direct; indirect; data]]. (* XXX: expand as needed *) 113 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 @(subaddressing_mode_elim … addr1) try (#w #_ @I) 117 [1: #_ @I ] 118 #w whd in ⊢ (??%? → %); 119 inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta 120 [1: 121 #absurd destruct(absurd) 122 2: 123 #_ 124 @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl) 125 cases w whd in ⊢ (??%%); @lookup_low_internal_ram_false 126 ] 127 qed. 128 129 lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2: 130 ∀M', cm. 131 ∀sigma, status, b. 132 ∀addr1: [[acc_a; registr; direct; indirect; data]]. (* XXX: expand as needed *) 133 addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true → 134 map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status addr1 b = b. 135 #M' #cm #sigma #status #b #addr1 136 @(subaddressing_mode_elim … addr1) 137 [1: 138 whd in ⊢ (??%? → ??%?); cases (\snd M') 139 [1: 140 normalize nodelta #_ % 141 2: 142 * #address normalize nodelta #absurd destruct(absurd) 143 ] 144 2,4: 145 #w whd in ⊢ (??%? → ??%?); 146 inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta 147 [1,3: 148 #absurd destruct(absurd) 149 2,4: 150 #_ >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl) 151 normalize nodelta % 152 ] 153 3: 154 #w whd in ⊢ (??%? → ??%?); 155 cases daemon (* XXX: ??? *) 156 5: 157 #w #_ % 158 ] 159 qed. 160 161 lemma set_flags_status_of_pseudo_status: 162 ∀M. 163 ∀sigma. 164 ∀policy. 165 ∀code_memory: pseudo_assembly_program. 166 ∀s: PreStatus ? code_memory. 167 ∀s'. 168 ∀b, b': Bit. 169 ∀opt, opt': option Bit. 170 ∀c, c': Bit. 171 b = b' → 172 opt = opt' → 173 c = c' → 174 status_of_pseudo_status M code_memory s sigma policy = s' → 175 set_flags … s' b opt c = 176 status_of_pseudo_status M code_memory (set_flags … code_memory s b' opt' c') sigma policy. 177 #M #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c' 178 #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl <s_refl 179 whd in match status_of_pseudo_status; normalize nodelta 180 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 181 cases (\snd M) 182 [1: 183 normalize nodelta % 184 2: 185 * #address normalize nodelta 186 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 187 whd in ⊢ (??%%); cases opt try #opt' normalize nodelta 188 @split_eq_status try % whd in match (sfr_8051_index ?); 189 cases daemon 190 ] 191 qed. 192 193 (* XXX: copied from Test.ma *) 194 lemma let_pair_in_status_of_pseudo_status: 195 ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'. 196 c = c' → 197 (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') → 198 let 〈left, right〉 ≝ c' in (s' left right c') = 199 status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy. 200 #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta // 201 qed. 202 203 (* XXX: copied from Test.ma *) 204 lemma let_pair_as_in_status_of_pseudo_status: 205 ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'. 206 c = c' → 207 (∀left, right, H, H'. status_of_pseudo_status M cm (s left right H c) sigma policy = s' left right H' c') → 208 let 〈left, right〉 as H' ≝ c' in (s' left right H' c') = 209 status_of_pseudo_status M cm (let 〈left, right〉 as H ≝ c in s left right H c) sigma policy. 210 #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta #destruct_refl 211 destruct(destruct_refl) /2/ 37 212 qed. 38 213 … … 1068 1243 try @split_eq_status try % 1069 1244 cases daemon *) 1070 [42,43,44,45,49,52,56: 1245 [42,44: (* RL and RR *) 1246 (* XXX: work on the right hand side *) 1247 (* XXX: switch to the left hand side *) 1248 >EQP P normalize nodelta 1249 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1250 whd in maps_assm:(??%%); 1251 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm 1252 [2,4: normalize nodelta #absurd destruct(absurd) ] 1253 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1254 whd in ⊢ (??%?); 1255 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm >EQs >EQticks <instr_refl 1256 change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status 1257 [2,4: 1258 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) 1259 @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 1260 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) 1261 % 1262 ] 1263 @sym_eq @set_clock_status_of_pseudo_status 1264 [2,4: 1265 % 1266 ] 1267 @sym_eq @set_program_counter_status_of_pseudo_status % 1268 43,45: (* RLC and RRC *) 1269 (* XXX: work on the right hand side *) 1270 (* XXX: switch to the left hand side *) 1271 >EQP P normalize nodelta 1272 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1273 whd in maps_assm:(??%%); 1274 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm 1275 [2,4: normalize nodelta #absurd destruct(absurd) ] 1276 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1277 whd in ⊢ (??%?); 1278 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm >EQs >EQticks <instr_refl 1279 change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status 1280 [2,4: 1281 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) 1282 @eq_f2 1283 [1,3: 1284 @sym_eq 1285 @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 1286 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) % 1287 2,4: 1288 @sym_eq @(get_cy_flag_status_of_pseudo_status … M') 1289 @sym_eq @set_clock_status_of_pseudo_status % 1290 ] 1291 1,3: 1292 @sym_eq @set_arg_1_status_of_pseudo_status try % 1293 @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) 1294 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) % 1295 ] 1296 1,2: (* ADD and ADDC *) 1297 (* XXX: work on the right hand side *) 1298 (* XXX: switch to the left hand side *) 1299 >EQP P normalize nodelta 1300 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1301 whd in maps_assm:(??%%); 1302 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1303 [2,4: normalize nodelta #absurd destruct(absurd) ] 1304 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1305 [2,4: normalize nodelta #absurd destruct(absurd) ] 1306 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1307 whd in ⊢ (??%?); 1308 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm >EQs >EQticks <instr_refl 1309 whd in ⊢ (??%?); 1310 @(pair_replace ?????????? p) 1311 [2,4: 1312 @(pair_replace ?????????? p) 1313 [2,4: 1314 normalize nodelta 1315 @set_flags_status_of_pseudo_status try % 1316 @sym_eq @set_arg_8_status_of_pseudo_status try % 1317 @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1) 1318 1,3: 1319 @eq_f3 1320 [1,2,4,5: 1321 normalize nodelta 1322 >EQs >EQticks <instr_refl % 1323 3: 1324 % 1325 6: 1326 normalize nodelta 1327 @eq_f @eq_f2 1328 [1: 1329 >EQs % 1330 2: 1331 >EQticks @eq_f2 <instr_refl try % >EQs % 1332 ] 1333 ] 1334 ] 1335 1,3: 1336 @eq_f3 1337 [1,2,4,5: 1338 normalize nodelta 1339 >EQs >EQticks <instr_refl 1340 cases daemon (* XXX: matita dies here *) 1341 3: 1342 % 1343 6: 1344 normalize nodelta 1345 @(get_cy_flag_status_of_pseudo_status … M') 1346 @sym_eq @set_clock_status_of_pseudo_status 1347 [1: 1348 @sym_eq >EQs 1349 @set_program_counter_status_of_pseudo_status % 1350 2: 1351 >EQticks <instr_refl >EQs % 1352 ] 1353 ] 1354 ] 1355 3: (* SUB *) 1356 (* XXX: work on the right hand side *) 1357 (* XXX: switch to the left hand side *) 1358 >EQP P normalize nodelta 1359 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1360 whd in maps_assm:(??%%); 1361 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1362 [2,4: normalize nodelta #absurd destruct(absurd) ] 1363 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1364 [2,4: 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 >EQs >EQticks <instr_refl 1368 whd in ⊢ (??%?); 1369 @(pair_replace ?????????? p) 1370 [1: 1371 @eq_f3 1372 normalize nodelta >EQs >EQticks <instr_refl 1373 [1: 1374 @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl 1375 @(get_arg_8_status_of_pseudo_status cm status … M') 1376 [1: 1377 >status_refl @sym_eq @set_clock_status_of_pseudo_status % 1378 2: 1379 >status_refl 1380 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1) 1381 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1382 lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta 1383 @(subaddressing_mode_elim … addr1) 1384 3: 1385 >status_refl 1386 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1) 1387 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1388 lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta 1389 @(subaddressing_mode_elim … addr1) 1390 ] 1391 2: 1392 @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl 1393 @(get_arg_8_status_of_pseudo_status cm status … M') 1394 [1: 1395 >status_refl @sym_eq @set_clock_status_of_pseudo_status % 1396 2: 1397 >status_refl 1398 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2) 1399 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1400 lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta 1401 cases daemon (* XXX: ??? *) 1402 3: 1403 >status_refl 1404 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2) 1405 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1406 lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta 1407 cases daemon (* XXX: ??? *) 1408 ] 1409 3: 1410 @(get_cy_flag_status_of_pseudo_status … M') 1411 @sym_eq @set_clock_status_of_pseudo_status 1412 [1: 1413 >sigma_increment_commutation 1414 2: 1415 % 1416 ] 1417 ] 1418 2: 1419 normalize nodelta 1420 @(pair_replace ?????????? p) 1421 [1: 1422 @eq_f3 normalize nodelta >EQs >EQticks <instr_refl % 1423 2: 1424 @set_flags_status_of_pseudo_status try % 1425 @sym_eq @set_arg_8_status_of_pseudo_status 1426 [1: 1427 @sym_eq @set_clock_status_of_pseudo_status % 1428 2: 1429 @I 1430 3: 1431 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A) 1432 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 1433 whd in ⊢ (??%?); 1434 >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % 1435 ] 1436 ] 1437 ] 1438 4,5,6,7,8,9: (* INC and DEC *) 1439 (* XXX: work on the right hand side *) 1440 (* XXX: switch to the left hand side *) 1441 >EQP P normalize nodelta 1442 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1443 whd in maps_assm:(??%%); 1444 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm 1445 [2,4,6,8,10,12: normalize nodelta #absurd destruct(absurd) ] 1446 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1447 whd in ⊢ (??%?); 1448 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 1449 @(subaddressing_mode_elim … addr) try #w whd in ⊢ (??%?); normalize nodelta 1450 [1: 1451 @(jmpair_as_replace ?????????? p) 1452 [1: 1453 @eq_f2 try % normalize nodelta 1454 XXX 1455 2: 1456 @(jmpair_as_replace ?????????? p) 1457 ] 1071 1458 10: (* MUL *) 1072 (* XXX: work on the right hand side *) 1073 (* XXX: switch to the left hand side *) 1074 >EQP P normalize nodelta 1075 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1076 whd in maps_assm:(??%%); 1077 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1078 [2: normalize nodelta #absurd destruct(absurd) ] 1079 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1080 [2: normalize nodelta #absurd destruct(absurd) ] 1081 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1082 whd in ⊢ (??%?); 1083 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm >EQs >EQticks <instr_refl 1084 change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status 1085 [2: 1086 whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f 1087 @sym_eq 1088 [1: 1089 @(get_8051_sfr_status_of_pseudo_status … policy) 1090 cases daemon (* XXX: need a lemma *) 1091 2: 1092 @(get_8051_sfr_status_of_pseudo_status M' … policy) 1093 @sym_eq @set_clock_status_of_pseudo_status [2: % ] 1094 @sym_eq @set_program_counter_status_of_pseudo_status % 1095 ] 1096 ] 1097 @sym_eq @set_8051_sfr_status_of_pseudo_status 1098 [2: 1099 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1) 1100 @eq_f @eq_f2 try % @eq_f2 @eq_f 1101 @sym_eq 1102 [1: 1103 @(get_8051_sfr_status_of_pseudo_status … policy) 1104 cases daemon (* XXX: needs a lemma *) 1105 2: 1106 @(get_8051_sfr_status_of_pseudo_status M' … policy) 1107 @sym_eq @set_clock_status_of_pseudo_status [2: % ] 1108 @sym_eq @set_program_counter_status_of_pseudo_status % 1109 ] 1110 ] 1111 @sym_eq @set_clock_status_of_pseudo_status 1112 [2: 1113 @eq_f % 1114 ] 1115 @sym_eq @set_program_counter_status_of_pseudo_status % 1459 (* XXX: work on the right hand side *) 1460 (* XXX: switch to the left hand side *) 1461 >EQP P normalize nodelta 1462 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1463 whd in maps_assm:(??%%); 1464 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1465 [2: normalize nodelta #absurd destruct(absurd) ] 1466 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1467 [2: normalize nodelta #absurd destruct(absurd) ] 1468 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1469 whd in ⊢ (??%?); 1470 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm >EQs >EQticks <instr_refl 1471 change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status 1472 [2: 1473 whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f 1474 @sym_eq 1475 [1: 1476 @(get_8051_sfr_status_of_pseudo_status … policy) #_ 1477 @(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) 1478 2: 1479 @(get_8051_sfr_status_of_pseudo_status M' … policy) 1480 @sym_eq @set_clock_status_of_pseudo_status [2: % ] 1481 @sym_eq @set_program_counter_status_of_pseudo_status % 1482 ] 1483 ] 1484 @sym_eq @set_8051_sfr_status_of_pseudo_status 1485 [2: 1486 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1) 1487 @eq_f @eq_f2 try % @eq_f2 @eq_f 1488 @sym_eq 1489 [1: 1490 @(get_8051_sfr_status_of_pseudo_status … policy) #_ 1491 @(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) 1492 2: 1493 @(get_8051_sfr_status_of_pseudo_status M' … policy) 1494 @sym_eq @set_clock_status_of_pseudo_status [2: % ] 1495 @sym_eq @set_program_counter_status_of_pseudo_status % 1496 ] 1497 ] 1498 @sym_eq @set_clock_status_of_pseudo_status 1499 [2: 1500 @eq_f % 1501 ] 1502 @sym_eq @set_program_counter_status_of_pseudo_status % 1503 11,12: (* DIV *) 1504 (* XXX: work on the right hand side *) 1505 (* XXX: switch to the left hand side *) 1506 >EQP P normalize nodelta 1507 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1508 whd in maps_assm:(??%%); 1509 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1510 [2,4: normalize nodelta #absurd destruct(absurd) ] 1511 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1512 [2,4: normalize nodelta #absurd destruct(absurd) ] 1513 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1514 whd in ⊢ (??%?); 1515 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm >EQs >EQticks <instr_refl 1516 whd in ⊢ (??%?); 1517 @(pose … (nat_of_bitvector ??)) #nat_of_bitvector_assm #pose_refl @sym_eq 1518 @(pose … (nat_of_bitvector ??)) #nat_of_bitvector_assm' #pose_refl' 1519 cut(nat_of_bitvector_assm = nat_of_bitvector_assm') 1520 [1,3: 1521 2,4: 1522 #cut_assm <cut_assm cases nat_of_bitvector_assm try #n' normalize nodelta 1523 @set_flags_status_of_pseudo_status 1524 ] 1525 1116 1526 1117 1527 (* XXX: work on the left hand side *) 
src/ASM/Test.ma
r2173 r2181 19 19 status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy. 20 20 #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl // 21 qed. 22 23 lemma if_then_else_status_of_pseudo_status_true: 24 ∀M: internal_pseudo_address_map. 25 ∀cm: pseudo_assembly_program. 26 ∀sigma: Word → Word. 27 ∀policy: Word → bool. 28 ∀s, s', s'', s'''. 29 ∀t: bool. 30 t = true → 31 status_of_pseudo_status M cm s sigma policy = s' → 32 if t then 33 s' 34 else 35 s'' = 36 status_of_pseudo_status M cm (if t then s else s''') sigma policy. 37 #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl 38 >t_refl normalize nodelta >s_refl % 39 qed. 40 41 lemma if_then_else_status_of_pseudo_status_false: 42 ∀M: internal_pseudo_address_map. 43 ∀cm: pseudo_assembly_program. 44 ∀sigma: Word → Word. 45 ∀policy: Word → bool. 46 ∀s, s', s'', s'''. 47 ∀t: bool. 48 t = false → 49 status_of_pseudo_status M cm s sigma policy = s' → 50 if t then 51 s'' 52 else 53 s' = 54 status_of_pseudo_status M cm (if t then s''' else s) sigma policy. 55 #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl 56 >t_refl normalize nodelta >s_refl % 21 57 qed. 22 58 … … 225 261 226 262 lemma get_index_v_status_of_pseudo_status: 227 ∀M, code_memory, sigma, policy, s, sfr. 228 (get_index_v Byte 19 263 ∀M, code_memory, sigma, policy, s, s', sfr. 264 map_address_using_internal_pseudo_address_map M sigma sfr 265 (get_index_v Byte 19 266 (special_function_registers_8051 pseudo_assembly_program code_memory s) 267 (sfr_8051_index sfr) (sfr8051_index_19 sfr)) = s' → 268 get_index_v Byte 19 229 269 (special_function_registers_8051 (BitVectorTrie Byte 16) 230 270 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 231 271 (status_of_pseudo_status M code_memory s sigma policy)) 232 (sfr_8051_index sfr) (sfr8051_index_19 sfr) = 233 map_address_using_internal_pseudo_address_map M sigma sfr 234 (get_index_v Byte 19 235 (special_function_registers_8051 pseudo_assembly_program code_memory s) 236 (sfr_8051_index sfr) (sfr8051_index_19 sfr))). 237 #M #code_memory #sigma #policy #s #sfr 272 (sfr_8051_index sfr) (sfr8051_index_19 sfr) = s'. 273 #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl 238 274 whd in match status_of_pseudo_status; normalize nodelta 239 275 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta … … 275 311 276 312 lemma get_8051_sfr_status_of_pseudo_status: 277 ∀M, code_memory, sigma, policy, s, s', s fr.313 ∀M, code_memory, sigma, policy, s, s', s'', sfr. 278 314 status_of_pseudo_status M code_memory s sigma policy = s' → 279 (get_8051_sfr (BitVectorTrie Byte 16) 315 map_address_using_internal_pseudo_address_map M sigma sfr 316 (get_8051_sfr pseudo_assembly_program code_memory s sfr) = s'' → 317 get_8051_sfr (BitVectorTrie Byte 16) 280 318 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 281 s' sfr = 282 map_address_using_internal_pseudo_address_map M sigma sfr 283 (get_8051_sfr pseudo_assembly_program code_memory s sfr)). 284 #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl 319 s' sfr = s''. 320 #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' <s_refl <s_refl' 285 321 whd in match get_8051_sfr; normalize nodelta 286 @get_index_v_status_of_pseudo_status 322 @get_index_v_status_of_pseudo_status % 287 323 qed. 288 324 … … 444 480 bit_address_of_register … cm s r. 445 481 #M #cm #s #sigma #policy #r whd in ⊢ (??%%); 446 >(get_8051_sfr_status_of_pseudo_status … (refl …) )482 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 447 483 @pair_elim #un #ln #_ 448 484 @pair_elim #r1 #r0 #_ % … … 452 488 primitive *) 453 489 axiom lookup_low_internal_ram_of_pseudo_low_internal_ram: 454 ∀M,sigma,cm,s,addr. 490 ∀M,sigma,cm,s,s',addr. 491 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) 492 (lookup Byte 7 addr 493 (low_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' → 455 494 lookup Byte 7 addr 456 495 (low_internal_ram_of_pseudo_low_internal_ram M 457 496 (low_internal_ram pseudo_assembly_program cm s)) (zero 8) 458 = 459 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) 460 (lookup Byte 7 addr 461 (low_internal_ram pseudo_assembly_program cm s) (zero 8)). 497 = s'. 462 498 463 499 (*CSC: provable using the axiom in AssemblyProof, but this one seems more 464 500 primitive *) 465 501 axiom lookup_high_internal_ram_of_pseudo_high_internal_ram: 466 ∀M,sigma,cm,s,addr. 502 ∀M,sigma,cm,s,s',addr. 503 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) 504 (lookup Byte 7 addr 505 (high_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' → 467 506 lookup Byte 7 addr 468 507 (high_internal_ram_of_pseudo_high_internal_ram M 469 508 (high_internal_ram pseudo_assembly_program cm s)) (zero 8) 470 = 471 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) 472 (lookup Byte 7 addr 473 (high_internal_ram pseudo_assembly_program cm s) (zero 8)). 509 = s'. 474 510 475 511 lemma get_register_status_of_pseudo_status: 476 ∀M,cm,sigma,policy,s,s', r.512 ∀M,cm,sigma,policy,s,s',s'',r. 477 513 status_of_pseudo_status M cm s sigma policy = s' → 514 map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r) 515 (get_register … cm s r) = s'' → 478 516 get_register … 479 517 (code_memory_of_pseudo_assembly_program cm sigma policy) 480 s' r = 481 map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r) 482 (get_register … cm s r). 483 #M #cm #sigma #policy #s #s' #r #s_refl <s_refl whd in match get_register; normalize nodelta 518 s' r = s''. 519 #M #cm #sigma #policy #s #s' #s'' #r #s_refl #s_refl' <s_refl <s_refl' 520 whd in match get_register; normalize nodelta 484 521 whd in match status_of_pseudo_status; normalize nodelta 485 522 >bit_address_of_register_status_of_pseudo_status 486 @ lookup_low_internal_ram_of_pseudo_low_internal_ram523 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … (refl …)) 487 524 qed. 488 525 … … 586 623 qed. 587 624 588 lemma set_arg_8_status_of_pseudo_status :625 lemma set_arg_8_status_of_pseudo_status': 589 626 ∀cm. 590 627 ∀ps. … … 654 691  #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ] 655 692 3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p; 656 >(get_register_status_of_pseudo_status … (refl …) )693 >(get_register_status_of_pseudo_status … (refl …) (refl …)) 657 694 whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 658 695 >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta … … 660 697  >(insert_low_internal_ram_status_of_pseudo_status … v) ] 661 698 // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % 662 5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) )699 5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …)) 663 700 whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 664 701 >EQ1 normalize nodelta … … 667 704 7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/ 668 705 8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status % 669 9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …) )670 >(get_8051_sfr_status_of_pseudo_status … (refl …) )706 9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 707 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 671 708 >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] % 709 qed. 710 711 lemma set_arg_8_status_of_pseudo_status: 712 ∀cm. 713 ∀ps. 714 ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]]. 715 ∀value. 716 ∀M. ∀sigma. ∀policy. ∀s'. ∀value'. 717 status_of_pseudo_status M cm ps sigma policy = s' → 718 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → 719 map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' → 720 set_arg_8 (BitVectorTrie Byte 16) 721 (code_memory_of_pseudo_assembly_program cm sigma policy) 722 s' addr value' = 723 status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy. 724 #cm #ps #addr #value 725 cases (set_arg_8_status_of_pseudo_status' cm ps addr value) #_ #relevant 726 @relevant 672 727 qed. 673 728 … … 754 809 ∀d: Byte. 755 810 ∀l: bool. 756 ∀M. ∀sigma. ∀policy. ∀s'. 811 ∀M. ∀sigma. ∀policy. ∀s'. ∀s''. 812 map_address_Byte_using_internal_pseudo_address_map M sigma 813 d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l) = s'' → 757 814 (status_of_pseudo_status M code_memory s sigma policy) = s' → 758 815 (get_bit_addressable_sfr (BitVectorTrie Byte 16) 759 816 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 760 s' d l = 761 map_address_Byte_using_internal_pseudo_address_map M sigma 762 d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)). 763 #code #s #d #v cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ 764 #H @H 817 s' d l) = s''. 818 #code #s #d #v 819 cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ #relevant 820 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl <s_refl' @relevant % 765 821 qed. 766 822 767 823 lemma program_counter_status_of_pseudo_status: 768 ∀M. ∀sigma . ∀policy.824 ∀M. ∀sigma: Word → Word. ∀policy. 769 825 ∀code_memory: pseudo_assembly_program. 770 826 ∀s: PreStatus ? code_memory. 771 827 ∀s'. 828 ∀s''. 829 sigma (program_counter … s) = s'' → 772 830 (status_of_pseudo_status M code_memory s sigma policy) = s' → 773 831 program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy) 774 s' = 775 sigma (program_counter … s). 776 #M #sigma #policy #code_memory #s #s' #s_refl <s_refl // 832 s' = s''. 833 #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl <s_refl' // 777 834 qed. 778 835 … … 786 843 #M #cm #sigma #policy #s #s' #s_refl <s_refl 787 844 whd in match get_cy_flag; normalize nodelta 788 > get_index_v_status_of_pseudo_status%789 qed. 790 791 lemma get_arg_8_status_of_pseudo_status :845 >(get_index_v_status_of_pseudo_status … (refl …)) % 846 qed. 847 848 lemma get_arg_8_status_of_pseudo_status': 792 849 ∀cm. 793 850 ∀ps. … … 850 907 [1: 851 908 #_ >p normalize nodelta >p1 normalize nodelta 852 @ get_bit_addressable_sfr_status_of_pseudo_status%909 @(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) % 853 910 2: 854 911 #_>p normalize nodelta >p1 normalize nodelta 855 @ lookup_low_internal_ram_of_pseudo_low_internal_ram912 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) % 856 913 3,4: 857 #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) )914 #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …)) 858 915 whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta 859 916 >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta 860 917 [1: 861 >(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma)918 @(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma) 862 919 2: 863 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)920 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) 864 921 ] 865 922 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % 866 923 5: 867 #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) )924 #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …)) 868 925 whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta 869 926 >assoc_list_assm normalize nodelta % 870 927 6,7,8,9: 871 #_ /2 /928 #_ /2 by refl, get_register_status_of_pseudo_status, get_index_v_status_of_pseudo_status/ 872 929 10: 873 #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) )874 >(get_8051_sfr_status_of_pseudo_status … (refl …) )875 >(get_8051_sfr_status_of_pseudo_status … (refl …) )930 #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 931 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 932 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 876 933 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 877 934 >acc_a_assm >p normalize nodelta // 878 935 11: 879 * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) )880 >(program_counter_status_of_pseudo_status … (refl …) )936 * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 937 >(program_counter_status_of_pseudo_status … (refl …) (refl …)) 881 938 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 882 939 >sigma_assm >map_acc_a_assm >p normalize nodelta // 883 940 12: 884 #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) )885 >(get_8051_sfr_status_of_pseudo_status … (refl …) )941 #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 942 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 886 943 >external_ram_status_of_pseudo_status // 887 944 ] 945 qed. 946 947 lemma get_arg_8_status_of_pseudo_status: 948 ∀cm. 949 ∀ps. 950 ∀l. 951 ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]]. 952 ∀M. ∀sigma. ∀policy. ∀s', s''. 953 (status_of_pseudo_status M cm ps sigma policy) = s' → 954 map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr) = s'' → 955 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → 956 get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) 957 s' l addr = s''. 958 #cm #ps #l #addr 959 cases (get_arg_8_status_of_pseudo_status' cm ps l addr) #_ #relevant 960 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl' 961 @relevant assumption 888 962 qed. 889 963 … … 1017 1091 2,4: 1018 1092 whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta 1019 >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) ) #map_address_assm1093 >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) #map_address_assm 1020 1094 >map_address_assm % 1021 1095 3,5: 1022 1096 whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta 1023 1097 whd in match status_of_pseudo_status; normalize nodelta 1024 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma )1098 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …)) 1025 1099 #map_address_assm >map_address_assm % 1026 1100 ] … … 1106 1180 qed. 1107 1181 1108 lemma set_arg_1_status_of_pseudo_status :1182 lemma set_arg_1_status_of_pseudo_status': 1109 1183 ∀cm: pseudo_assembly_program. 1110 1184 ∀ps: PreStatus pseudo_assembly_program cm. 1111 1185 ∀addr: [[bit_addr; carry]]. 1112 1186 ∀b: Bit. 1113 Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'. 1187 Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀b'. 1188 b = b' → 1114 1189 status_of_pseudo_status M cm ps sigma policy = s' → 1115 1190 map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b → … … 1118 1193 (code_memory_of_pseudo_assembly_program cm sigma policy) 1119 1194 s' addr b = 1120 status_of_pseudo_status M cm (set_arg_1 … cm ps addr b ) sigma policy.1195 status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy. 1121 1196 whd in match set_arg_1; normalize nodelta 1122 1197 whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta … … 1157 1232 [ ] 1158 1233 ] (subaddressing_modein … a)) normalize nodelta 1159 try @modulus_less_than #M #sigma #policy #s' # s_refl <s_refl1234 try @modulus_less_than #M #sigma #policy #s' #b' #b_refl <b_refl #s_refl <s_refl 1160 1235 [1: 1161 #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) )1236 #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 1162 1237 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 1163 1238 >p normalize nodelta @set_8051_sfr_status_of_pseudo_status % 1164 1239 2,3: 1165 >(get_8051_sfr_status_of_pseudo_status … (refl …) )1240 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 1166 1241 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 1167 1242 >p normalize nodelta >p1 normalize nodelta 1168 1243 #map_bit_address_assm_1 #map_bit_address_assm_2 1169 1244 [1: 1170 >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) )1245 >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) 1171 1246 >map_bit_address_assm_1 1172 1247 >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) % 1173 1248 2: 1174 1249 whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta 1175 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma )1250 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …)) 1176 1251 >map_bit_address_assm_1 1177 1252 >(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2) … … 1179 1254 ] 1180 1255 ] 1256 qed. 1257 1258 lemma set_arg_1_status_of_pseudo_status: 1259 ∀cm: pseudo_assembly_program. 1260 ∀ps: PreStatus pseudo_assembly_program cm. 1261 ∀addr: [[bit_addr; carry]]. 1262 ∀b: Bit. 1263 ∀M. ∀sigma. ∀policy. ∀s'. ∀b'. 1264 b = b' → 1265 status_of_pseudo_status M cm ps sigma policy = s' → 1266 map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b → 1267 map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b → 1268 set_arg_1 (BitVectorTrie Byte 16) 1269 (code_memory_of_pseudo_assembly_program cm sigma policy) 1270 s' addr b = 1271 status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy. 1272 #cm #ps #addr #b 1273 cases (set_arg_1_status_of_pseudo_status' cm ps addr b) #_ #relevant 1274 @relevant 1181 1275 qed. 1182 1276 … … 1201 1295 #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl <s_refl <v_refl // 1202 1296 qed. 1297 1298 lemma let_pair_in_status_of_pseudo_status: 1299 ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'. 1300 c = c' → 1301 (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') → 1302 let 〈left, right〉 ≝ c' in s' left right c' = 1303 status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy. 1304 #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta // 1305 qed. 1306 1307 lemma let_pair_as_in_status_of_pseudo_status: 1308 ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'. 1309 ∀c_refl: c = c'. 1310 (∀left, right, H. status_of_pseudo_status M cm (s left right H c') sigma policy = s' left right H c) → 1311 let 〈left, right〉 as H ≝ c' in s' left right H c = 1312 status_of_pseudo_status M cm (let 〈left, right〉 as H' ≝ c in s left right ? c) sigma policy. 1313 [2: >H' assumption ] 1314 #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' 1315 #destruct_assm destruct(destruct_assm) normalize nodelta 1316 #status_of_pseudo_status_assm >status_of_pseudo_status_assm // 1317 qed. 1318 1319 lemma if_then_else_status_of_pseudo_status: 1320 ∀M: internal_pseudo_address_map. 1321 ∀cm: pseudo_assembly_program. 1322 ∀sigma: Word → Word. 1323 ∀policy: Word → bool. 1324 ∀s, s', s'', s'''. 1325 ∀t, t': bool. 1326 t = t' → 1327 status_of_pseudo_status M cm s sigma policy = s' → 1328 status_of_pseudo_status M cm s'' sigma policy = s''' → 1329 if t then 1330 s' 1331 else 1332 s''' = 1333 status_of_pseudo_status M cm (if t' then s else s'') sigma policy. 1334 #M #cm #sigma #policy #s #s' #s'' #s''' #t #t' #t_refl #s_refl 1335 >t_refl normalize nodelta >s_refl cases t' normalize nodelta // 1336 qed.
Note: See TracChangeset
for help on using the changeset viewer.