Changeset 1693 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Feb 14, 2012, 4:38:06 PM (8 years ago)
Author:
mulligan
Message:

Changes to ASMCosts and CostsProofs? files to get everything working again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1692 r1693  
    13381338qed.
    13391339
    1340 definition block_cost ≝
     1340(*
     1341  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
     1342    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
     1343      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
     1344        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
     1345          on program_size:
     1346          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
     1347          Σcost_of_block: nat.
     1348          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
     1349            ∀start_status: Status code_memory'.
     1350            ∀final_status: Status code_memory'.
     1351            ∀trace_ends_flag.
     1352            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     1353              program_counter' = program_counter … start_status →
     1354                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
     1355                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
     1356          else
     1357            (cost_of_block = 0)
     1358*)
     1359
     1360definition block_cost:
     1361    ∀code_memory': BitVectorTrie Byte 16.
     1362    ∀program_counter': Word.
     1363    ∀total_program_size: nat.
     1364    ∀cost_labels: BitVectorTrie costlabel 16.
     1365    ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
     1366    ∀good_program_witness: good_program code_memory' total_program_size.
     1367      Σcost_of_block: nat.
     1368        ∀start_status: Status code_memory'.
     1369        ∀final_status: Status code_memory'.
     1370        ∀trace_ends_flag.
     1371        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     1372          program_counter' = program_counter … start_status →
     1373            (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
     1374              cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
    13411375  λcode_memory: BitVectorTrie Byte 16.
    13421376  λprogram_counter: Word.
     
    13441378  λcost_labels: BitVectorTrie costlabel 16.
    13451379  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
    1346   λgood_program_witness: good_program code_memory total_program_size.
    1347     block_cost' code_memory program_counter total_program_size total_program_size cost_labels
    1348       reachable_program_counter_witness good_program_witness true ?.
    1349   @le_plus_n_r
     1380  λgood_program_witness: good_program code_memory total_program_size. ?.
     1381  cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels
     1382    reachable_program_counter_witness good_program_witness true ?)
     1383  [1:
     1384    #cost_of_block #block_cost_hyp
     1385    %{cost_of_block}
     1386    cases(lookup_opt … cost_labels) in block_cost_hyp;
     1387    [2: #cost_label] normalize nodelta
     1388    #hyp assumption
     1389  |2:
     1390    @le_plus_n_r
     1391  ]
    13501392qed.
    13511393
Note: See TracChangeset for help on using the changeset viewer.