Changeset 1691


Ignore:
Timestamp:
Feb 14, 2012, 1:43:38 AM (6 years ago)
Author:
sacerdot
Message:

Some progress in the proof: less daemons, less hypotheses in lemmas.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1684 r1691  
    561561  ∀program_counter'' : Word.
    562562  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
    563   ∀real_instruction : (preinstruction [[relative]]).
    564   ∀real_instruction_refl : (RealInstruction … real_instruction = instruction).
    565563  ∀start_status : (Status code_memory').
    566564  ∀final_status : (Status code_memory').
     
    600598  #reachable_program_counter_witness #good_program_witness
    601599  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
    602   #real_instruction #real_instruction_refl #start_status #final_status
     600  #start_status #final_status
    603601  #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost
    604602  #recursive_assm @(trace_any_label_inv_ind … the_trace)
     
    724722  ∀program_counter'': Word.
    725723  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
    726   ∀real_instruction: (preinstruction [[relative]]).
    727   ∀real_instruction_refl: (RealInstruction … real_instruction = instruction).
    728724  ∀start_status: (Status code_memory').
    729725  ∀final_status: (Status code_memory').
     
    732728  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
    733729  ∀classify_assm: ASM_classify0 instruction = cl_jump.
    734  (∀pi1:ℕ
    735   .if match lookup_opt costlabel 16 program_counter' cost_labels with 
    736         [None⇒true|Some _ ⇒first_time_around] 
    737    then (∀start_status0:Status code_memory'
    738              .∀final_status0:Status code_memory'
    739               .∀trace_ends_flag0:trace_ends_with_ret
    740                .∀the_trace0:trace_any_label
    741                                         (ASM_abstract_status code_memory' cost_labels)
    742                                         trace_ends_flag0 start_status0 final_status0
    743                 .program_counter'
    744                  =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
    745                  →(∃n:ℕ
    746                    .trace_any_label_length code_memory' cost_labels trace_ends_flag0
    747                     start_status0 final_status0 the_trace0
    748                     +S n
    749                     =total_program_size)
    750                   ∧pi1
    751                    =compute_paid_trace_any_label code_memory' cost_labels
    752                     trace_ends_flag0 start_status0 final_status0 the_trace0) 
    753    else (pi1=O) 
    754    →(∃n:ℕ
     730   (∃n:ℕ
    755731     .trace_any_label_length code_memory' cost_labels trace_ends_flag
    756732      start_status final_status the_trace
     
    759735    ∧ticks
    760736     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    761       start_status final_status the_trace).
     737      start_status final_status the_trace.
    762738  #code_memory' #program_counter' #total_program_size #cost_labels
    763739  #reachable_program_counter_witness #good_program_witness #first_time_around
    764740  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
    765   #real_instruction #real_instruction_refl #start_status #final_status
     741  #start_status #final_status
    766742  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
    767   #recursive_block_cost #recursive_assm
    768743  @(trace_any_label_inv_ind … the_trace)
    769744  [1:
     
    783758      #absurd cases absurd
    784759    |2:
    785       #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
    786       generalize in match recursive_assm;
    787       cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … start_status')))
    788       [1:
    789         <fetch_twice_fetch_execute_1 <FETCH %
    790       |2:
    791         cases daemon
    792       ]
     760      #costlabel #Some_lookup_opt_assm normalize nodelta #ignore %
     761      [2: <FETCH %
     762      | cases daemon ]
    793763    ]
    794764  |2:
     
    829799  ∀program_counter'' : Word.
    830800  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
    831   ∀real_instruction : (preinstruction [[relative]]).
    832   ∀real_instruction_refl : (RealInstruction … real_instruction = instruction).
    833801  ∀start_status : (Status code_memory').
    834802  ∀final_status : (Status code_memory').
     
    867835  #code_memory' #program_counter' #total_program_size #cost_labels
    868836  #reachable_program_counter_witness #good_program_witness #program_size'
    869   #recursive_case #ticks #instruction #program_counter'' #FETCH #real_instruction
    870   #real_instruction_refl #start_status #final_status #trace_ends_flag
     837  #recursive_case #ticks #instruction #program_counter'' #FETCH
     838  #start_status #final_status #trace_ends_flag
    871839  #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm
    872840  @(trace_any_label_inv_ind … the_trace)
     
    970938    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    971939    cases(block_cost' ?????????) -block_cost'
    972     #recursive_block_cost #recursive_assm
    973     @(trace_any_label_inv_ind … the_trace)
    974     [1,6,11:
    975       #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
    976       #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    977       destruct @⊥
    978     |2,7,12:
    979       #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
    980       #start_status_refl #final_status_refl #the_trace_refl
    981       destruct @⊥
    982     |3,8,13:
    983       #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    984       #classifier_assm #after_return_assm #trace_label_return #costed_assm
    985       #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    986       destruct
    987       whd in match (trace_any_label_length … (tal_base_call …));
    988       whd in match (compute_paid_trace_any_label … (tal_base_call …));
    989       whd in costed_assm;
    990       generalize in match costed_assm;
    991       generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
    992       [1:
    993         generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
    994           in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
    995       |2:
    996         generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
    997           in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
    998       |3:
    999         generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
    1000           in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
    1001       ] (* XXX: matita bug here: generalize in match ... above works OK on each
    1002                 individual goal, but fails when you try to do it across multiple goals
    1003                 with a delifting error. *)
    1004       #lookup_assm cases lookup_assm
    1005       [1,3,5:
    1006         #None_lookup_opt normalize nodelta #absurd cases absurd
    1007       |2,4,6:
    1008         #costlabel #Some_lookup_opt normalize nodelta #ignore
    1009         generalize in match recursive_assm;
    1010         cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_pre_fun_call)))
    1011         [1,3,5:
    1012           <fetch_twice_fetch_execute_1 <FETCH %
    1013         |2,4,6: (* XXX: got to here *)
    1014           #program_counter_assm >program_counter_assm <Some_lookup_opt
    1015           normalize nodelta #new_recursive_assm >new_recursive_assm %
    1016           [1:
    1017             %{(pred total_program_size)} whd in ⊢ (??%?);
    1018             @S_pred
    1019             @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
    1020           |2:
    1021             cut(ticks = \snd (fetch code_memory'
    1022                (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
    1023             [1:
    1024               <FETCH %
    1025             |2:
    1026               #ticks_refl_assm >ticks_refl_assm
    1027               <plus_n_O %
    1028             ]
    1029           ]
    1030         ]
    1031       ]
    1032     |4,9,14:
    1033       #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    1034       #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
    1035       #not_costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    1036       #final_status_refl #the_trace_refl
    1037       destruct (* XXX: relevant *) cases daemon
    1038     |5,10,15:
    1039       #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
    1040       #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
    1041       #final_status_refl #the_trace_refl
    1042       destruct @⊥
    1043     ]
    1044     try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
    1045     try (change with (ASM_classify0 ? = ?) in classifier_assm;)
    1046     whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    1047     whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    1048     <FETCH in classifier_assm;
    1049     try(whd in ⊢ ((??%?) → ?); #absurd destruct(absurd))
    1050     whd in ⊢ (?(??%?)(??%?) → ?); #absurd
    1051     cases absurd #absurd destruct(absurd)
     940    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … program_counter_refl)
     941    destruct %
    1052942  |4,7,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,71,74,77,80,83,86,89,
    1053    92:
     943   92,95:
    1054944    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    1055945    cases(block_cost' ?????????) -block_cost'
    1056     @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … real_instruction_refl … the_trace program_counter_refl …)
     946    @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
    1057947    destruct %
    1058   |95:
    1059     #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    1060     cases(block_cost' ?????????) -block_cost'
    1061     #recursive_block_cost #recursive_assm
    1062     @(trace_any_label_inv_ind … the_trace)
    1063     [5:
    1064       #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
    1065       #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
    1066       #the_trace_refl
    1067       destruct
    1068       whd in match (trace_any_label_length … (tal_step_default …));
    1069       whd in match (compute_paid_trace_any_label … (tal_step_default …));
    1070       whd in costed_assm:(?%);
    1071       generalize in match costed_assm;
    1072       generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
    1073       generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
    1074         in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
    1075       #lookup_assm cases lookup_assm
    1076       [1:
    1077         #None_lookup_opt_assm normalize nodelta #ignore
    1078         generalize in match recursive_assm;
    1079         cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre)))
    1080         [1:
    1081           <fetch_twice_fetch_execute_1 <FETCH %
    1082         |2:
    1083           #program_counter_assm >program_counter_assm <None_lookup_opt_assm
    1084           normalize nodelta #new_recursive_assm
    1085           cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
    1086             end_flag trace_any_label ?) [2: % ]
    1087           #exists_assm #recursive_block_cost_assm %
    1088           [1:
    1089             cases exists_assm #exists_n #total_program_size_refl
    1090             <total_program_size_refl
    1091             %{(exists_n - current_instruction_cost … status_pre)}
    1092             (* XXX: Christ knows what's going on with the rewrite tactic here? *)
    1093             cases daemon
    1094           |2:
    1095             >recursive_block_cost_assm
    1096             whd in match (current_instruction_cost … status_pre);
    1097             cut(ticks = \snd (fetch code_memory'
    1098                (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
    1099             [1:
    1100               <FETCH %
    1101             |2:
    1102               #ticks_refl_assm >ticks_refl_assm %
    1103             ]
    1104           ]
    1105         ]
    1106       |2:
    1107         #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
    1108         #absurd cases absurd #absurd cases(absurd I)
    1109       ]
    1110     |1:
    1111       #status_start #status_final #execute_assm #classifier_assm #costed_assm
    1112       #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    1113       destruct
    1114       whd in match (trace_any_label_length … (tal_base_not_return …));
    1115       whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
    1116       whd in costed_assm;
    1117       generalize in match costed_assm;
    1118       generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
    1119       generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
    1120         in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
    1121       #lookup_assm cases lookup_assm
    1122       [1:
    1123         #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
    1124         #absurd cases absurd
    1125       |2:
    1126         #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
    1127         generalize in match recursive_assm;
    1128         cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start)))
    1129         [1:
    1130           <fetch_twice_fetch_execute_1 <FETCH %
    1131         |2:
    1132           #program_counter_assm >program_counter_assm <Some_lookup_opt_assm
    1133           normalize nodelta #new_recursive_assm >new_recursive_assm %
    1134           [1:
    1135             %{(pred total_program_size)} whd in ⊢ (??%?);
    1136             @S_pred
    1137             @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
    1138           |2:
    1139             cut(ticks = \snd (fetch code_memory'
    1140                (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
    1141             [1:
    1142               <FETCH %
    1143             |2:
    1144               #ticks_refl_assm >ticks_refl_assm
    1145               <plus_n_O %
    1146             ]
    1147           ]
    1148         ]
    1149       ]
    1150     |2:
    1151       #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
    1152       #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
    1153     |3:
    1154       #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    1155       #classifier_assm #after_return_assm #trace_label_return #costed_assm
    1156       #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    1157       destruct @⊥
    1158     |4:
    1159       #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    1160       #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
    1161       #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    1162       #final_status_refl #the_trace_refl destruct @⊥
    1163     ]
    1164     change with (ASM_classify0 ? = ?) in classifier_assm;
    1165     whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    1166     whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    1167     <FETCH in classifier_assm; whd in ⊢ ((??%?) → ?); #absurd destruct(absurd)
    1168948  |62,63,64,65,66,67,68,69,101,102,103:
    1169     #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    1170     cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
    1171       reachable_program_counter_witness good_program_witness first_time_around ?)
    1172     try (@(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … real_instruction_refl … the_trace program_counter_refl …) destruct %)
    1173     |2:
    1174     ]
    1175     cases daemon
     949    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
     950    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
     951    destruct %
    1176952  |96,99:
    1177953    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
Note: See TracChangeset for help on using the changeset viewer.