Changeset 1684


Ignore:
Timestamp:
Feb 9, 2012, 5:42:24 PM (6 years ago)
Author:
mulligan
Message:

changes from the past week

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1669 r1684  
    532532  cases instruction_pc #instruction #pc normalize nodelta *)
    533533
    534 lemma blah:
     534lemma reachable_program_counter_to_0_lt_total_program_size:
     535  ∀code_memory: BitVectorTrie Byte 16.
     536  ∀program_counter: Word.
     537  ∀total_program_size: nat.
     538    reachable_program_counter code_memory total_program_size program_counter →
     539      0 < total_program_size.
     540  #code_memory #program_counter #total_program_size
     541  whd in match reachable_program_counter; normalize nodelta * * #some_n
     542  #_ cases (nat_of_bitvector 16 program_counter)
     543  [1:
     544    #assm assumption
     545  |2:
     546    #new_pc @ltn_to_ltO
     547  ]
     548qed.
     549
     550lemma trace_compute_paid_trace_cl_other:
    535551  ∀code_memory' : (BitVectorTrie Byte 16).
    536552  ∀program_counter' : Word.
     
    616632            <total_program_size_refl
    617633            %{(exists_n - current_instruction_cost … status_pre)}
     634            (* XXX: Christ knows what's going on with the rewrite tactic here? *)
     635            cases daemon
    618636          |2:
    619637            >recursive_block_cost_assm
     
    659677            %{(pred total_program_size)} whd in ⊢ (??%?);
    660678            @S_pred
    661             generalize in match good_program_witness;
    662             whd in match (good_program … total_program_size);
    663             #good_program_hyp
    664             lapply(good_program_hyp (program_counter … status_start) reachable_program_counter_witness)
    665             <FETCH normalize nodelta -good_program_hyp (* XXX: Claudio here *)
     679            @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
    666680          |2:
    667681            cut(ticks = \snd (fetch code_memory'
     
    675689          ]
    676690        ]
    677       |2:
    678         #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
    679         #absurd cases absurd #absurd cases(absurd I)
    680691      ]
    681692    |2:
     
    687698      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    688699      destruct @⊥
    689     ]
    690       change with (
    691         ASM_classify0 ? = ?) in classifier_assm;
    692       whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    693       whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    694       <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
     700    |4:
     701      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     702      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     703      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
     704      #final_status_refl #the_trace_refl destruct @⊥
     705    ]
     706  change with (ASM_classify0 ? = ?) in classifier_assm;
     707  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     708  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     709  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
     710qed.
     711
     712lemma trace_compute_paid_trace_cl_jump:
     713  ∀code_memory': BitVectorTrie Byte 16.
     714  ∀program_counter': Word.
     715  ∀total_program_size: ℕ.
     716  ∀cost_labels: BitVectorTrie costlabel 16.
     717  ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
     718  ∀good_program_witness: good_program code_memory' total_program_size.
     719  ∀first_time_around: bool.
     720  ∀program_size': ℕ.
     721  ∀recursive_case: total_program_size ≤ S program_size'+nat_of_bitvector 16 program_counter'.
     722  ∀ticks: ℕ.
     723  ∀instruction: instruction.
     724  ∀program_counter'': Word.
     725  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
     726  ∀real_instruction: (preinstruction [[relative]]).
     727  ∀real_instruction_refl: (RealInstruction … real_instruction = instruction).
     728  ∀start_status: (Status code_memory').
     729  ∀final_status: (Status code_memory').
     730  ∀trace_ends_flag: trace_ends_with_ret.
     731  ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
     732  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
     733  ∀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:ℕ
     755     .trace_any_label_length code_memory' cost_labels trace_ends_flag
     756      start_status final_status the_trace
     757      +S n
     758      =total_program_size)
     759    ∧ticks
     760     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
     761      start_status final_status the_trace).
     762  #code_memory' #program_counter' #total_program_size #cost_labels
     763  #reachable_program_counter_witness #good_program_witness #first_time_around
     764  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
     765  #real_instruction #real_instruction_refl #start_status #final_status
     766  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
     767  #recursive_block_cost #recursive_assm
     768  @(trace_any_label_inv_ind … the_trace)
     769  [1:
     770    #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
     771    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     772    destruct
     773    whd in match (trace_any_label_length … (tal_base_not_return …));
     774    whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
     775    whd in costed_assm;
     776    generalize in match costed_assm;
     777    generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … start_status')) cost_labels));
     778    generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' start_status')) cost_labels)
     779      in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
     780    #lookup_assm cases lookup_assm
     781    [1:
     782      #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
     783      #absurd cases absurd
     784    |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      ]
     793    ]
     794  |2:
     795    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
     796    #start_status_refl #final_status_refl #the_trace_refl destruct @⊥
     797  |3:
     798    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     799    #classifier_assm #after_return_assm #trace_label_return #costed_assm
     800    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     801    destruct @⊥
     802  |4:
     803    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     804    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     805    #costed_assm #trace_any_label_return #trace_ends_flag_refl #start_status_refl
     806    #final_status_refl #the_trace_refl destruct @⊥
     807  |5:
     808    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     809    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
     810    #final_status_refl #the_trace_refl destruct @⊥
     811  ]
     812  change with (ASM_classify0 ? = ?) in classifier_assm;
     813  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     814  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     815  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
     816qed.
     817
     818lemma trace_compute_paid_trace_cl_call:
     819  ∀code_memory' : (BitVectorTrie Byte 16).
     820  ∀program_counter' : Word.
     821  ∀total_program_size : ℕ.
     822  ∀cost_labels : (BitVectorTrie costlabel 16).
     823  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
     824  ∀good_program_witness : (good_program code_memory' total_program_size).
     825  ∀program_size' : ℕ.
     826  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
     827  ∀ticks : ℕ.
     828  ∀instruction : instruction.
     829  ∀program_counter'' : Word.
     830  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
     831  ∀real_instruction : (preinstruction [[relative]]).
     832  ∀real_instruction_refl : (RealInstruction … real_instruction = instruction).
     833  ∀start_status : (Status code_memory').
     834  ∀final_status : (Status code_memory').
     835  ∀trace_ends_flag : trace_ends_with_ret.
     836  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
     837  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
     838  ∀classify_assm: ASM_classify0 instruction = cl_call.
     839  ∀pi1 : ℕ.
     840  if match lookup_opt costlabel 16 program_counter'' cost_labels with 
     841        [None ⇒ true|Some _ ⇒ false] 
     842   then (∀start_status0:Status code_memory'
     843             .∀final_status0:Status code_memory'
     844              .∀trace_ends_flag0:trace_ends_with_ret
     845               .∀the_trace0:trace_any_label
     846                                        (ASM_abstract_status code_memory' cost_labels)
     847                                        trace_ends_flag0 start_status0 final_status0
     848                .program_counter''
     849                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
     850                 →(∃n:ℕ
     851                   .trace_any_label_length code_memory' cost_labels trace_ends_flag0
     852                    start_status0 final_status0 the_trace0
     853                    +S n
     854                    =total_program_size)
     855                  ∧pi1
     856                   =compute_paid_trace_any_label code_memory' cost_labels
     857                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
     858   else (pi1=O) 
     859   →(∃n:ℕ
     860     .trace_any_label_length code_memory' cost_labels trace_ends_flag
     861      start_status final_status the_trace
     862      +S n
     863      =total_program_size)
     864    ∧ticks+pi1
     865     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
     866      start_status final_status the_trace.
     867  #code_memory' #program_counter' #total_program_size #cost_labels
     868  #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
     871  #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm
     872  @(trace_any_label_inv_ind … the_trace)
     873  cases daemon
    695874qed.
    696875
     
    782961    @(le_to_lt_to_lt … base_case hyp)
    783962  |2:
    784       change with (
    785         if to_continue then
    786           ?
    787         else
    788           (? = 0)) >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
    789        @pi2
     963    change with (if to_continue then ? else (? = 0))
     964    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
     965    @pi2
    790966  |3:
     967    change with (if to_continue then ? else (0 = 0))
     968    >p normalize nodelta %
     969  |98,104,107:
     970    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
     971    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)
     1052  |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:
     1054    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
     1055    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 …)
     1057    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)
     1168  |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
     1176  |96,99:
     1177    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1178    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1179    <FETCH normalize nodelta <instr normalize nodelta *
     1180    #program_counter_lt' #program_counter_lt_tps' %
     1181    [1,3:
     1182      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     1183      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     1184      >(le_to_leb_true … program_counter_lt') %
     1185    |2,4:
     1186      assumption
     1187    ]
     1188  |105:
     1189    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1190    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1191    <FETCH normalize nodelta <instr normalize nodelta
     1192    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
     1193    * * * * #n'
     1194    #_ #_ #program_counter_lt' #program_counter_lt_tps'
     1195    %
     1196    [1:
     1197      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     1198      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     1199      >(le_to_leb_true … program_counter_lt') %
     1200    |2:
     1201      assumption
     1202    ]
     1203  |106:
     1204    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1205    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1206    <FETCH normalize nodelta <instr normalize nodelta
     1207    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
     1208    * * * * #n'
     1209    #_ #_ #program_counter_lt' #program_counter_lt_tps'
     1210    @(transitive_le
     1211      total_program_size
     1212      ((S program_size') + nat_of_bitvector … program_counter')
     1213      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
     1214    normalize in match (S program_size' + nat_of_bitvector … program_counter');
     1215    >plus_n_Sm
     1216    @monotonic_le_plus_r
    7911217    change with (
    792       if to_continue then
    793         ?
    794       else
    795         (0 = 0)) >p normalize nodelta %
     1218      nat_of_bitvector … program_counter' <
     1219        nat_of_bitvector … program_counter'')
     1220    assumption
     1221  |108:
     1222    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1223    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1224    <FETCH normalize nodelta <instr normalize nodelta
     1225    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
     1226    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
     1227    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
     1228    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
     1229    #_ #_ #program_counter_lt' #program_counter_lt_tps'
     1230    %
     1231    [1:
     1232      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     1233      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     1234      >(le_to_leb_true … program_counter_lt') %
     1235    |2:
     1236      assumption
     1237    ]
     1238  |109:
     1239    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1240    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1241    <FETCH normalize nodelta <instr normalize nodelta
     1242    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
     1243    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
     1244    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
     1245    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
     1246    #_ #_ #program_counter_lt' #program_counter_lt_tps'
     1247    @(transitive_le
     1248      total_program_size
     1249      ((S program_size') + nat_of_bitvector … program_counter')
     1250      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
     1251    normalize in match (S program_size' + nat_of_bitvector … program_counter');
     1252    >plus_n_Sm
     1253    @monotonic_le_plus_r
     1254    change with (
     1255      nat_of_bitvector … program_counter' <
     1256        nat_of_bitvector … program_counter'')
     1257    assumption
     1258  |5,8,12,14,15,18,20,21,24,27,30,33,36,39,42,45,48,51,54,57,60,72,75,
     1259   78,81,84,87,90,93:
     1260    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1261    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1262    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
     1263    #program_counter_lt' #program_counter_lt_tps' %
     1264    try assumption
     1265    %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     1266    <FETCH normalize nodelta whd in match ltb; normalize nodelta
     1267    >(le_to_leb_true … program_counter_lt') %
     1268  |97,100:
     1269    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1270    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1271    <FETCH normalize nodelta <instr normalize nodelta
     1272    try(<real_instruction_refl <instr normalize nodelta) *
     1273    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
     1274    @(transitive_le
     1275      total_program_size
     1276      ((S program_size') + nat_of_bitvector … program_counter')
     1277      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
     1278    normalize in match (S program_size' + nat_of_bitvector … program_counter');
     1279    >plus_n_Sm
     1280    @monotonic_le_plus_r
     1281    change with (
     1282      nat_of_bitvector … program_counter' <
     1283        nat_of_bitvector … program_counter'')
     1284    assumption
     1285  |6,9,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,73,76,79,82,85,88,91,
     1286   94:
     1287    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1288    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1289    <FETCH normalize nodelta
     1290    <real_instruction_refl <instr normalize nodelta *
     1291    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
     1292    @(transitive_le
     1293      total_program_size
     1294      ((S program_size') + nat_of_bitvector … program_counter')
     1295      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
     1296    normalize in match (S program_size' + nat_of_bitvector … program_counter');
     1297    >plus_n_Sm
     1298    @monotonic_le_plus_r
     1299    change with (
     1300      nat_of_bitvector … program_counter' <
     1301        nat_of_bitvector … program_counter'')
     1302    assumption
     1303  |10:
     1304    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
     1305    cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
     1306      reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost'
     1307    [1:
     1308      @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness …
     1309        recursive_case … instruction program_counter' … FETCH)
     1310    |2:
     1311    ]
     1312  ]
     1313qed.
     1314 
     1315 
     1316 
     1317 
     1318    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1319    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1320    <FETCH normalize nodelta
     1321    <real_instruction_refl <instr normalize nodelta *
     1322    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
     1323    @(transitive_le
     1324      total_program_size
     1325      ((S program_size') + nat_of_bitvector … program_counter')
     1326      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
     1327    normalize in match (S program_size' + nat_of_bitvector … program_counter');
     1328    >plus_n_Sm
     1329    @monotonic_le_plus_r
     1330    change with (
     1331      nat_of_bitvector … program_counter' <
     1332        nat_of_bitvector … program_counter'')
     1333    assumption
    7961334  |4:
    7971335    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    798     cases(block_cost' ?????????) -block_cost'
    799     @(blah … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … real_instruction_refl … the_trace program_counter_refl …)
    800     destruct %
    801   |4:
    802     #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    803     cases(block_cost' ?????????) -block_cost'
     1336    cases(block_cost' ??? ? ?????) -block_cost'
    8041337    #recursive_block_cost #recursive_assm
    8051338    @(trace_any_label_inv_ind … the_trace)
     
    8431376      @⊥ <FETCH in classifier_assm; normalize nodelta
    8441377      #absurd destruct(absurd)
    845     |5:
    8461378    ]
    8471379   
Note: See TracChangeset for help on using the changeset viewer.