Ignore:
Timestamp:
Jul 26, 2012, 12:05:58 PM (7 years ago)
Author:
sacerdot
Message:

Call is now proved using the new strategy.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2266 r2267  
    205205      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
    206206      whd in match (expand_pseudo_instruction ??????);
    207       whd in match (ticks_of0 ??????);
    208       inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
    209       inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
    210       [2:
    211         inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
    212         inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
    213       ]
     207      whd in match (execute_1_pseudo_instruction0 ?????);
     208      inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta
     209      inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta
     210      @pair_elim #carry #new_sp #carry_new_sp_refl lapply (refl_to_jmrefl ??? carry_new_sp_refl) -carry_new_sp_refl #carry_new_sp_refl
     211      @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl lapply (refl_to_jmrefl ??? pc_bu_bl_refl) -pc_bu_bl_refl #pc_bu_bl_refl
     212      @pair_elim #carry' #new_sp' #carry_new_sp_refl' lapply (refl_to_jmrefl ??? carry_new_sp_refl') -carry_new_sp_refl' #carry_new_sp_refl'
    214213      #sigma_increment_commutation
    215214      normalize in sigma_increment_commutation:(???(???(??%)));
    216215      (* XXX: we work on the maps *)
    217       whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
     216      whd in ⊢ (??%? → ?);
     217      @pair_elim #callM #accM #Mrefl
     218      @Some_Some_elim #map_refl_assm <map_refl_assm
    218219      (* XXX: we assume the fetch_many hypothesis *)
    219220      * #fetch_refl #fetch_many_assm
     
    227228      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
    228229      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    229       change with (set_program_counter ???? =
    230        status_of_pseudo_status ?? (set_program_counter ????) ??)
    231        @set_program_counter_status_of_pseudo_status
    232        [2,4,6: @sym_eq @set_clock_status_of_pseudo_status try %
    233          [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
    234                  @sigma_increment_commutation
    235          | @eq_f2 try % @ticks_of_instruction_AJMP ]]
    236        whd in ⊢ (??%%); normalize nodelta whd in match address_of_word_labels;
    237        normalize nodelta
    238        [ inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
    239          >EQlookup_labels in mjc_refl; >create_label_cost_refl #mjc_refl
    240          @(absolute_jump_cond_ok ????? pc_bl (sym_eq … mjc_refl))
    241          [2: >(andb_true_l … mj_possible_refl) %
    242          | <vsplit_refl @eq_f <EQnewpc % ]
    243        | >EQlookup_labels >create_label_cost_refl %
    244        |  inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
    245           >create_label_cost_refl
    246           >EQlookup_labels in sjc_refl; #sjc_refl
    247           >(pair_destruct_2 ????? (sym_eq … half_add_refl))
    248           >(short_jump_cond_ok ???? (sym_eq … sjc_refl))
    249           [2: >(andb_true_l … sj_possible_refl) %
    250           | >EQnewpc % ]]
    251    
    252    
    253    
    254    
    255    
    256    
    257    
    258    
    259    
    260    
    261    
    262    
    263       #arg1 #pi_refl
    264       (* XXX: we first work on sigma_increment_commutation *)
    265       whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
    266       whd in match (expand_pseudo_instruction ??????);
    267       whd in match (execute_1_pseudo_instruction0 ?????);
    268       inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta
    269       inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta
    270       @pair_elim #carry #new_sp #carry_new_sp_refl lapply (refl_to_jmrefl ??? carry_new_sp_refl) -carry_new_sp_refl #carry_new_sp_refl
    271       @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl lapply (refl_to_jmrefl ??? pc_bu_bl_refl) -pc_bu_bl_refl #pc_bu_bl_refl
    272       @pair_elim #carry' #new_sp' #carry_new_sp_refl' lapply (refl_to_jmrefl ??? carry_new_sp_refl') -carry_new_sp_refl' #carry_new_sp_refl'
    273       #sigma_increment_commutation
    274       normalize in sigma_increment_commutation:(???(???(??%)));
    275       (* XXX: we work on the maps *)
    276       whd in ⊢ (??%? → ?);
    277       @pair_elim #callM #accM #Mrefl
    278       @Some_Some_elim #map_refl_assm <map_refl_assm
    279       (* XXX: we assume the fetch_many hypothesis *)
    280       * #fetch_refl #fetch_many_assm
    281       (* XXX: we give the existential *)
    282       %{1}
    283       (* XXX: work on the left hand side of the equality *)
    284       whd in ⊢ (??%?); whd in match (program_counter ???);
    285       (* XXX: execute fetches some more *)
    286       whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    287       whd in fetch_many_assm;
    288       >EQassembled in fetch_refl; #fetch_refl <fetch_refl
    289       lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    290       whd in ⊢ (??(???%)?); normalize in match (length ? (assembly1 …));
    291       normalize in match (length ? (assembly1 …)) in EQnewpc;
    292       normalize nodelta
     230      whd in ⊢ (??%?);
    293231      [1:
    294232        @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
    295         try /demod nohyps/ [1: %]
     233        [ @eq_f2 try %
     234          cases daemon (*CSC*)
     235        ] whd in ⊢ (??%?);
     236        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
     237        @(pair_replace ????? ?? ??? carry_new_sp_refl')
     238        [ @eq_f2 try %
     239          cases daemon (*CSC*)
     240        ]
     241        whd in ⊢ (??%?);
     242        @pair_elim #fiv #thr' #fiv_thr_refl'
     243        change with (set_program_counter ???? = ?)
     244        @set_program_counter_status_of_pseudo_status
     245        [2: @sym_eq cases daemon (*@write_at_stack_pointer_status_of_pseudo_status try %
     246          [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
     247                  @sigma_increment_commutation
     248          | @eq_f2 try % @ticks_of_instruction_AJMP ]*)]
     249        whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
     250        >EQlookup_labels normalize nodelta
     251        @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl
     252        >fst_5_rest_refl normalize nodelta
     253        @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
     254        #pair_true_refl destruct(pair_true_refl)
     255        <EQnewpc in fst_5_rest_pc_refl;
     256        lapply pc_bu_bl_refl' -pc_bu_bl_refl'
     257        >program_counter_set_8051_sfr >set_clock_set_program_counter
     258        >program_counter_set_program_counter #relevant2
     259        <(vsplit_ok ?????? (sym_eq … relevant2))
     260        <(vsplit_ok ?????? (sym_eq … fiv_thr_refl'))
     261        >(vector_associative_append bool 5 3 8) #relevant3
     262        >(? : fiv = fst_5_addr)
     263        [1: <fst_5_rest_refl whd in match address_of_word_labels; normalize nodelta
     264            >create_label_cost_refl %
     265        |2: 
     266          cases daemon (*CSC: make a lemma here!*)
     267        ]
     268      | @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
     269        [ @eq_f2 try % cases daemon ]
    296270        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
    297271        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
    298         try /demod nohyps/ [1: %]
    299         @pair_elim #fiv #thr' #fiv_thr_refl' whd in ⊢ (??%%);
    300         @split_eq_status try /demod nohyps/ try %
    301         [1,2:
    302           (* XXX: need the commented out axioms from AssemblyProof.ma *)
    303           cases daemon
    304         |3:
    305           lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta
    306           change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
    307           #relevant <(relevant arg1)
    308           [2:
    309             @(is_well_labelled_witness … ppc_in_bounds pi)
    310             [1:
    311               >fetch_pseudo_refl %
    312             |2:
    313               >pi_refl %
    314             ]
    315           |1:
    316             whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
    317             >EQlookup_labels normalize nodelta
    318             @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl
    319             >fst_5_rest_refl normalize nodelta
    320             @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
    321             #pair_true_refl destruct(pair_true_refl)
    322             <EQnewpc in fst_5_rest_pc_refl;
    323             lapply pc_bu_bl_refl' -pc_bu_bl_refl'
    324             >program_counter_set_8051_sfr >set_clock_set_program_counter
    325             >program_counter_set_program_counter #relevant2
    326             <(vsplit_ok ?????? (sym_eq … relevant2))
    327             <(vsplit_ok ?????? (sym_eq … fiv_thr_refl'))
    328             >(vector_associative_append bool 5 3 8) #relevant3
    329             >(? : fiv = fst_5_addr)
    330             [1:
    331               %
    332             |2:
    333               cases daemon
    334             ]
    335           ]
    336         |4:
    337           >set_program_counter_mk_Status_commutation in ⊢ (???%);
    338           >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%);
    339           (* XXX: require set_8051_sfr_write_at_stack_pointer and
    340                           special_function_registers_8051_set_8051_sfr
    341           *)
    342           cases daemon
    343         |5,6,7:
    344           >set_program_counter_mk_Status_commutation in ⊢ (???%);
    345           (* XXX: similar to above but for 8052
    346           *)
    347           cases daemon
    348         |8:
    349           whd in match (ticks_of_instruction ?);
    350           cut(\snd  (fetch (load_code_memory (assembly1 (ACALL (ADDR11 offset)))) (zero 16)) = 2)
    351           [1: //
    352           |2:
    353             normalize in match (assembly1 ?);
    354             @(bitvector_3_elim_prop … (\fst (vsplit bool 3 8 offset))) %
    355           |3:
    356             #fetch_2_refl >fetch_2_refl >commutative_plus %
    357           ]
    358         ]
    359       |2:
    360         @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
    361         try /demod nohyps/ [1: %]
    362         @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
    363         @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
    364         try /demod nohyps/ [1: %]
    365         @split_eq_status try /demod nohyps/ try %
     272        [ @eq_f2 try % cases daemon ]
     273        change with (set_program_counter ???? = ?)
     274        @set_program_counter_status_of_pseudo_status
     275        [ >EQlookup_labels whd in match address_of_word_labels; normalize nodelta
     276          >create_label_cost_refl % ]
     277        cut(pc_bu' @@ pc_bl' = sigma (pc_bu @@ pc_bl))
    366278        [1:
    367           cut(pc_bu' @@ pc_bl' = sigma (pc_bu @@ pc_bl))
    368           [1:
    369             >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl')) /demod nohyps/
    370             >set_clock_set_program_counter >program_counter_set_program_counter
    371             >add_commutative >EQnewpc @eq_f @sym_eq @(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl))
    372           |2:
    373             #relevant cases daemon
    374             (* XXX: need axioms *)
    375           ]
    376         |2:
    377           cases daemon (* XXX: need axioms from assembly.ma *)
    378         |3:
    379           change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
    380           lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta
    381           #relevant <(relevant arg1)
    382           [1:
    383             >EQlookup_labels %
    384           |2:
    385             @(is_well_labelled_witness … ppc_in_bounds pi)
    386             [1:
    387               >fetch_pseudo_refl %
    388             |2:
    389               >pi_refl %
    390             ]
    391           ]
    392         |4:
    393           >set_program_counter_mk_Status_commutation in ⊢ (???%);
    394           >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%);
    395           (* XXX: require set_8051_sfr_write_at_stack_pointer and
    396                           special_function_registers_8051_set_8051_sfr
    397           *)
    398           cases daemon
    399         |5,6,7:
    400           >set_program_counter_mk_Status_commutation in ⊢ (???%);
    401           (* XXX: similar to above but for 8052
    402           *)
    403           cases daemon
    404         ]
     279          >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl'))
     280          >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl))
     281          >add_commutative
     282          >program_counter_set_8051_sfr >set_clock_set_program_counter
     283          >program_counter_set_program_counter >add_commutative
     284          >program_counter_set_8051_sfr >set_clock_set_program_counter
     285          >program_counter_set_program_counter assumption ] #sigma_pc_bu_pc_bl_refl
     286        @sym_eq
     287        cases daemon
    405288      ]
    406289    ]
Note: See TracChangeset for help on using the changeset viewer.