Changeset 2026


Ignore:
Timestamp:
Jun 7, 2012, 4:37:42 PM (5 years ago)
Author:
mulligan
Message:

Added a new file to house the main theorem as the type checking time for the main lemma is ridiculous.

Location:
src/ASM
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2024 r2026  
    13931393qed.
    13941394
    1395 theorem main_thm:
    1396   ∀M, M': internal_pseudo_address_map.
    1397   ∀program: pseudo_assembly_program.
    1398   ∀sigma: Word → Word.
    1399   ∀policy: Word → bool.
    1400   ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
    1401   ∀ps: PseudoStatus program.
    1402     next_internal_pseudo_address_map M program ps = Some … M' →
    1403       ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
    1404         status_of_pseudo_status M' …
    1405           (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy.
    1406   #M #M' * #preamble #instr_list #sigma #policy #sigma_policy_witness #ps
    1407   change with (next_internal_pseudo_address_map0 ????? = ? → ?)
    1408   @(pose … (program_counter ?? ps)) #ppc #EQppc
    1409   check fetch_assembly_pseudo2
    1410   generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?;
    1411   @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
    1412   @pair_elim #assembled #costs' #assembly_refl normalize nodelta
    1413   lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
    1414   @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
    1415   @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
    1416   @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    1417   whd in match execute_1_pseudo_instruction; normalize nodelta
    1418   whd in match ticks_of; normalize nodelta <EQppc >fetch_pseudo_refl normalize nodelta
    1419   lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc
    1420   lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc pi … EQlookup_labels EQlookup_datalabels ?)
    1421   [1: >fetch_pseudo_refl % ]
    1422   #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
    1423   generalize in match assm1; -assm1 -assm2 -assm3
    1424   normalize nodelta
    1425   cases pi
    1426   [2,3:
    1427     #arg
    1428     (* XXX: we first work on sigma_increment_commutation *)
    1429     #sigma_increment_commutation
    1430     normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
    1431     (* XXX: we work on the maps *)
    1432     whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
    1433     (* XXX: we assume the fetch_many hypothesis *)
    1434     #fetch_many_assm
    1435     (* XXX: we give the existential *)
    1436     %{0}
    1437     whd in match (execute_1_pseudo_instruction0 ?????);
    1438     (* XXX: work on the left hand side of the equality *)
    1439     whd in ⊢ (??%?);
    1440     @split_eq_status //
    1441     [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ]
    1442   |6: (* Mov *)
    1443     #arg1 #arg2
    1444     (* XXX: we first work on sigma_increment_commutation *)
    1445     #sigma_increment_commutation
    1446     normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
    1447     (* XXX: we work on the maps *)
    1448     whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
    1449     (* XXX: we assume the fetch_many hypothesis *)
    1450     #fetch_many_assm
    1451     (* XXX: we give the existential *)
    1452     %{1}
    1453     whd in match (execute_1_pseudo_instruction0 ?????);
    1454     (* XXX: work on the left hand side of the equality *)
    1455     whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
    1456     (* XXX: execute fetches some more *)
    1457     whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    1458     whd in fetch_many_assm;
    1459     >EQassembled in fetch_many_assm;
    1460     cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
    1461     #eq_instr
    1462     #fetch_many_assm whd in fetch_many_assm;
    1463     lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    1464     destruct whd in ⊢ (??%?);
    1465     (* XXX: now we start to work on the mk_PreStatus equality *)
    1466     (* XXX: lhs *)
    1467     change with (set_arg_16 ????? = ?)
    1468     >set_program_counter_mk_Status_commutation
    1469     >set_clock_mk_Status_commutation
    1470     >set_arg_16_mk_Status_commutation
    1471     (* XXX: rhs *)
    1472     change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
    1473     >set_program_counter_mk_Status_commutation
    1474     >set_clock_mk_Status_commutation
    1475     >set_arg_16_mk_Status_commutation in ⊢ (???%);
    1476     (* here we are *)
    1477     @split_eq_status //
    1478     [1:
    1479       assumption
    1480     |2:
    1481       @special_function_registers_8051_set_arg_16
    1482       [2: %
    1483       |1: //
    1484       ]
    1485     ]
    1486   |1: (* Instruction *) -pi; #instr
    1487     @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy
    1488         sigma_policy_witness ps ppc EQppc labels costs create_label_cost_refl ? lookup_datalabels)
    1489     check (main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness
    1490       … EQppc … create_label_cost_refl … assembly_refl EQassembled … EQlookup_labels …
    1491       EQlookup_datalabels EQnewppc instr … (refl …) … (refl …) … (refl …) … (refl …))
    1492   |4,5: cases daemon
    1493   ]
    1494 qed.
    14951395(* 
    14961396    *
Note: See TracChangeset for help on using the changeset viewer.