Changeset 2140


Ignore:
Timestamp:
Jun 28, 2012, 6:47:26 PM (5 years ago)
Author:
mulligan
Message:

Done the hardest cases in the main theorem. Just got a few daemons to close...

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2139 r2140  
    403403                      status_of_pseudo_status M' cm s sigma policy).
    404404    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
     405  (* XXX: takes about 45 minutes to type check! *)
    405406  #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
    406407  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
  • src/ASM/AssemblyProofSplitSplit.ma

    r2139 r2140  
    150150      |6:
    151151        >assembly_refl assumption
     152      |7:
     153        <EQassembled assumption
    152154      ]
    153155    |4: (* Jmp *)
     
    264266          cases daemon
    265267        |3:
    266           whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
    267           >EQlookup_labels normalize nodelta
    268           @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl normalize nodelta
    269           <EQnewpc @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
    270           #relevant
    271           lapply pc_bu_bl_refl' -pc_bu_bl_refl'
    272           >program_counter_set_8051_sfr >set_clock_set_program_counter
    273           >program_counter_set_program_counter >fst_5_rest_pc_refl
    274           cut(fst_5_addr = fst_5_pc)
    275           [1:
    276             cases daemon (* XXX: !! *)
    277           |2:
    278             #relevant2 >relevant2
     268          lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta
     269          change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
     270          #relevant <(relevant arg1)
     271          [2:
     272            @(is_well_labelled_witness … ppc_in_bounds pi)
     273            [1:
     274              >fetch_pseudo_refl %
     275            |2:
     276              >pi_refl %
     277            ]
     278          |1:
     279            whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
     280            >EQlookup_labels normalize nodelta
     281            @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl
     282            >fst_5_rest_refl normalize nodelta
     283            @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
     284            #pair_true_refl destruct(pair_true_refl)
     285            <EQnewpc in fst_5_rest_pc_refl;
     286            lapply pc_bu_bl_refl' -pc_bu_bl_refl'
     287            >program_counter_set_8051_sfr >set_clock_set_program_counter
     288            >program_counter_set_program_counter #relevant2
     289            <(vsplit_ok ?????? (sym_eq … relevant2))
    279290            <(vsplit_ok ?????? (sym_eq … fiv_thr_refl'))
    280             #relevant3
    281             lapply(vsplit_ok ?????? (sym_eq … relevant3))
    282             >(vector_associative_append bool 5 3 8) #relevant4
    283             cut(fiv = fst_5_pc ∧ thr'@@pc_bl' = rest_pc)
     291            >(vector_associative_append bool 5 3 8) #relevant3
     292            >(? : fiv = fst_5_addr)
    284293            [1:
    285               cases daemon (* XXX: !! *)
     294              %
    286295            |2:
    287               * #relevant5 #relevant6 >relevant5
    288               >(vector_associative_append bool 5 3 8) @eq_f
    289               destruct(relevant)
    290               <(vsplit_ok ?????? (sym_eq … thr_eig_refl)) @eq_f
     296              cases daemon
    291297            ]
    292           ] *)
     298          ]
    293299        |4:
    294300          >set_program_counter_mk_Status_commutation in ⊢ (???%);
     
    308314          [1: //
    309315          |2:
    310             normalize in match (assembly1 ?); >thr_eig_refl
    311             @(bitvector_3_elim_prop … thr) %
     316            normalize in match (assembly1 ?);
     317            @(bitvector_3_elim_prop … (\fst (vsplit bool 3 8 offset))) %
    312318          |3:
    313319            #fetch_2_refl >fetch_2_refl >commutative_plus %
    314320          ]
     321        ]
     322      |2:
     323        @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
     324        try /demod nohyps/ [1: %]
     325        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
     326        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
     327        try /demod nohyps/ [1: %]
     328        @split_eq_status try /demod nohyps/ try %
     329        [1:
     330          cut(pc_bu' @@ pc_bl' = sigma (pc_bu @@ pc_bl))
     331          [1:
     332            >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl')) /demod nohyps/
     333            >set_clock_set_program_counter >program_counter_set_program_counter
     334            >add_commutative >EQnewpc @eq_f @sym_eq @(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl))
     335          |2:
     336            #relevant cases daemon
     337            (* XXX: need axioms *)
     338          ]
    315339        |2:
     340          cases daemon (* XXX: need axioms from assembly.ma *)
     341        |3:
     342          change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
     343          lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta
     344          #relevant <(relevant arg1)
     345          [1:
     346            >EQlookup_labels %
     347          |2:
     348            @(is_well_labelled_witness … ppc_in_bounds pi)
     349            [1:
     350              >fetch_pseudo_refl %
     351            |2:
     352              >pi_refl %
     353            ]
     354          ]
     355        |4:
     356          >set_program_counter_mk_Status_commutation in ⊢ (???%);
     357          >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%);
     358          (* XXX: require set_8051_sfr_write_at_stack_pointer and
     359                          special_function_registers_8051_set_8051_sfr
     360          *)
     361          cases daemon
     362        |5,6,7:
     363          >set_program_counter_mk_Status_commutation in ⊢ (???%);
     364          (* XXX: similar to above but for 8052
     365          *)
     366          cases daemon
    316367        ]
    317368      ]
    318369    ]
    319   ]
    320370qed.
Note: See TracChangeset for help on using the changeset viewer.