Changeset 1711 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Feb 20, 2012, 11:15:52 AM (8 years ago)
Author:
mulligan
Message:

finished block_cost' proof: 1.5 minutes to typecheck qed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1710 r1711  
    11141114    @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
    11151115    destruct %
    1116   |62,63,64,65,66,67,68,69,99,101,102:
     1116  |60,61,62,63,64,65,66,67,68,69,99,101,100,102:
    11171117    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    11181118    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
     
    12111211    >(le_to_leb_true … program_counter_lt') %
    12121212    (* XXX: got to here *)
    1213   |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,
    1214    94:
     1213  |6,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,71,74,77,80,83,86,89,
     1214   92:
    12151215    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    12161216    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    12291229        nat_of_bitvector … program_counter'')
    12301230    assumption
    1231   |62,63,64,65,66,67,68,69,70,101,102,103:
    1232     #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    1233     cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
    1234       reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost'
    1235     try (@(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl …) destruct %)
    1236     cases daemon (* XXX: ???, same as above case *)
    1237   |96,99:
    1238     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1239     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1240     <FETCH normalize nodelta <instr normalize nodelta *
    1241     #program_counter_lt' #program_counter_lt_tps' %
    1242     [1,3:
    1243       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1244       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1245       >(le_to_leb_true … program_counter_lt') %
    1246     |2,4:
    1247       assumption
    1248     ]
    1249   |98,104,107:
    1250     #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    1251     cases(block_cost' ?????????) -block_cost'
    1252     @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness first_time_around … recursive_case … FETCH … the_trace program_counter_refl …)
    1253     destruct %
    1254   |105:
    1255     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1256     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1257     <FETCH normalize nodelta <instr normalize nodelta
    1258     @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    1259     * * * * #n'
    1260     #_ #_ #program_counter_lt' #program_counter_lt_tps'
    1261     %
    1262     [1:
    1263       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1264       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1265       >(le_to_leb_true … program_counter_lt') %
    1266     |2:
    1267       assumption
    1268     ]
    1269   |106:
    1270     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1271     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1272     <FETCH normalize nodelta <instr normalize nodelta
    1273     @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    1274     * * * * #n'
    1275     #_ #_ #program_counter_lt' #program_counter_lt_tps'
    1276     @(transitive_le
    1277       total_program_size
    1278       ((S program_size') + nat_of_bitvector … program_counter')
    1279       (program_size' + nat_of_bitvector … program_counter'') recursive_case)
    1280     normalize in match (S program_size' + nat_of_bitvector … program_counter');
    1281     >plus_n_Sm
    1282     @monotonic_le_plus_r
    1283     change with (
    1284       nat_of_bitvector … program_counter' <
    1285         nat_of_bitvector … program_counter'')
    1286     assumption
    1287   |108:
    1288     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1289     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1290     <FETCH normalize nodelta <instr normalize nodelta
    1291     @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    1292     cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
    1293     cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    1294     cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
    1295     #_ #_ #program_counter_lt' #program_counter_lt_tps'
    1296     %
    1297     [1:
    1298       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1299       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1300       >(le_to_leb_true … program_counter_lt') %
    1301     |2:
    1302       assumption
    1303     ]
    1304   |109:
    1305     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1306     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1307     <FETCH normalize nodelta <instr normalize nodelta
    1308     @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    1309     cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
    1310     cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    1311     cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
    1312     #_ #_ #program_counter_lt' #program_counter_lt_tps'
    1313     @(transitive_le
    1314       total_program_size
    1315       ((S program_size') + nat_of_bitvector … program_counter')
    1316       (program_size' + nat_of_bitvector … program_counter'') recursive_case)
    1317     normalize in match (S program_size' + nat_of_bitvector … program_counter');
    1318     >plus_n_Sm
    1319     @monotonic_le_plus_r
    1320     change with (
    1321       nat_of_bitvector … program_counter' <
    1322         nat_of_bitvector … program_counter'')
    1323     assumption
    1324   |97,100:
     1231  |95,98:
    13251232    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    13261233    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    13411248  ]
    13421249qed.
    1343 
    1344 (*
    1345   (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
    1346     (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
    1347       (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
    1348         (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
    1349           on program_size:
    1350           total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
    1351           Σcost_of_block: nat.
    1352           if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
    1353             ∀start_status: Status code_memory'.
    1354             ∀final_status: Status code_memory'.
    1355             ∀trace_ends_flag.
    1356             ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    1357               program_counter' = program_counter … start_status →
    1358                 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
    1359                   cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
    1360           else
    1361             (cost_of_block = 0)
    1362 *)
    13631250
    13641251definition block_cost:
Note: See TracChangeset for help on using the changeset viewer.