Ignore:
Timestamp:
Jun 28, 2012, 12:55:05 AM (7 years ago)
Author:
sacerdot
Message:

No more need for functional extensionality.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2129 r2131  
    6363    lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
    6464    @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
    65     @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels
     65    @(pose … (λx. bitvector_of_nat ? (lookup_def … labels x 0))) #lookup_labels #EQlookup_labels
    6666    @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    6767    whd in match execute_1_pseudo_instruction; normalize nodelta
    6868    whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
    6969    lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
    70     lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?)
    71     [1: >fetch_pseudo_refl % |2: skip |3: assumption ]
     70    lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc … pi … lookup_labels lookup_datalabels)
     71    [1: assumption |2: assumption] >create_label_cost_refl
     72    #X lapply (X EQlookup_labels EQlookup_datalabels ?) -X
     73    [1: >fetch_pseudo_refl %]
    7274    #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
    7375    generalize in match assm1; -assm1 -assm2 -assm3
    7476    normalize nodelta
    7577    inversion pi
    76     [(*2,3:
     78    [2,3:
    7779      #arg #_
    7880      (* XXX: we first work on sigma_increment_commutation *)
     
    138140        (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
    139141        (refl …) ? (refl …))
    140       try assumption try % >assembly_refl assumption
     142      [1,2,3: try assumption try %] >assembly_refl assumption
    141143    |4: (* Jmp *)
    142144      #arg1 #pi_refl
     
    182184          >EQnewpc
    183185          inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
    184           @sym_eq >address_of_word_labels_assm
    185           [1:
    186             >EQlookup_labels in mjc_refl; #mjc_refl
    187             @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
    188             >(andb_true_l … mj_possible_refl) @I
    189           ]
     186          @sym_eq
     187          >EQlookup_labels in mjc_refl; #mjc_refl
     188          @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
     189          >(andb_true_l … mj_possible_refl) @I
    190190        |3:
    191           >EQlookup_labels normalize nodelta
    192           >address_of_word_labels_assm try %
     191          >EQlookup_labels normalize nodelta %
    193192        |5:
    194193          >EQnewpc
    195194          inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
    196           @sym_eq >address_of_word_labels_assm
    197           [1:
    198             >EQlookup_labels in sjc_refl; #sjc_refl
    199             >(pair_destruct_2 ????? (sym_eq … half_add_refl))
    200             @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
    201             >(andb_true_l … sj_possible_refl) @I
    202           ]
     195          @sym_eq
     196          >EQlookup_labels in sjc_refl; #sjc_refl
     197          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
     198          @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
     199          >(andb_true_l … sj_possible_refl) @I
    203200        ]
    204201        @(is_well_labelled_witness … fetch_pseudo_refl)
     
    212209        @commutative_plus
    213210      ]
    214     |*)5: (* Call *)
     211    |5: (* Call *)
    215212      #arg1 #pi_refl
    216213      (* XXX: we first work on sigma_increment_commutation *)
     
    249246        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
    250247        try /demod nohyps/ [1: %]
    251         @pair_elim #thr #eig #thr_eig_refl
    252248        @pair_elim #fiv #thr' #fiv_thr_refl' whd in ⊢ (??%%);
    253249        @split_eq_status try /demod nohyps/ try %
     
    256252          cases daemon
    257253        |3:
    258           >program_counter_set_program_counter
    259254          whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
    260255          >EQlookup_labels normalize nodelta
     
    262257          <EQnewpc @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
    263258          #relevant >fst_5_rest_refl
    264           check absolute_jump_cond
    265           <(vsplit_ok ?????? (sym_eq … thr_eig_refl))
    266259          lapply pc_bu_bl_refl' -pc_bu_bl_refl'
    267260          >program_counter_set_8051_sfr >set_clock_set_program_counter
Note: See TracChangeset for help on using the changeset viewer.