Ignore:
Timestamp:
Apr 23, 2012, 3:46:35 PM (8 years ago)
Author:
mulligan
Message:

Changes to proof, and pushed through those changes to rest of the file.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r1896 r1897  
    113113        (good_program_witness: good_program code_memory fixed_program_size)
    114114        (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size)
    115         (fixed_program_size_limit: fixed_program_size < 2^16)
     115        (fixed_program_size_limit: fixed_program_size 2^16)
    116116        on program_size:
    117117          Σcost_map: identifier_map CostTag nat.
     
    179179              destruct
    180180              @succ_nat_of_bitvector_half_add_1
    181               @(plus_lt_to_lt ? (S n') (2^16 - 1))
    182181              @le_plus_to_minus_r
    183               change with (? < ?)
    184               <plus_n_Sm <plus_n_O >plus_n_Sm assumption
     182              @(transitive_le … fixed_program_size_limit)
     183              change with (S ? ≤ ?) >plus_n_Sm
     184              @monotonic_le_plus_r
     185              @le_S_S @le_S_S @le_O_n
    185186            |2:
    186187              #S_assm
     
    297298                  destruct
    298299                  @succ_nat_of_bitvector_half_add_1
    299                   @(plus_lt_to_lt ? (S n') (2^16 - 1))
    300300                  @le_plus_to_minus_r
    301                   change with (? < ?)
    302                   <plus_n_Sm <plus_n_O >plus_n_Sm assumption
     301                  @(transitive_le … fixed_program_size_limit)
     302                  change with (S ? ≤ ?) >plus_n_Sm
     303                  @monotonic_le_plus_r
     304                  @le_S_S @le_S_S @le_O_n
    303305                |2:
    304306                  #Sn_refl_assm >Sn_refl_assm <NEW_PC' @le_n
     
    315317            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
    316318            [1:
     319              destruct
    317320              @succ_nat_of_bitvector_half_add_1
    318               @(plus_lt_to_lt ? (S n') (2^16 - 1))
    319321              @le_plus_to_minus_r
    320               change with (? < ?)
    321               <plus_n_Sm <plus_n_O >plus_n_Sm assumption
     322              @(transitive_le … fixed_program_size_limit)
     323              change with (S ? ≤ ?) >plus_n_Sm
     324              @monotonic_le_plus_r
     325              @le_S_S @le_S_S @le_O_n
    322326            |2:
    323327              #S_assm
     
    347351        cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
    348352        [1:
     353          destruct
    349354          @succ_nat_of_bitvector_half_add_1
    350355          @le_plus_to_minus_r
    351356          @(transitive_le … fixed_program_size_limit)
    352           destruct <plus_n_Sm <plus_n_Sm
    353           change with (S (S ?) + ? ≤ S (S ?) + ?)
    354           @monotonic_le_plus_r @le_O_n
     357          change with (S ? ≤ ?) >plus_n_Sm
     358          @monotonic_le_plus_r
     359          @le_S_S @le_S_S @le_O_n
    355360        |2:
    356361          #S_assm
     
    375380qed.
    376381
     382(*
     383let rec traverse_code_internal
     384  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     385    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
     386      (reachable_program_counter_witness:
     387          ∀lbl: costlabel.
     388          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
     389            reachable_program_counter code_memory fixed_program_size program_counter)
     390        (good_program_witness: good_program code_memory fixed_program_size)
     391        (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size)
     392        (fixed_program_size_limit: fixed_program_size < 2^16)
     393        on program_size:
     394          Σcost_map: identifier_map CostTag nat.
     395            (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
     396            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
     397              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
     398                pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
     399*)
     400
    377401definition traverse_code:
    378402  ∀code_memory: BitVectorTrie Byte 16.
    379403  ∀cost_labels: BitVectorTrie costlabel 16.
    380404  ∀program_size: nat.
     405  ∀program_size_limit: program_size ≤ 2^16.
    381406  ∀reachable_program_counter_witness:
    382407    ∀lbl: costlabel.
     
    385410  ∀good_program_witness: good_program code_memory program_size.
    386411    Σcost_map: identifier_map CostTag nat.
     412      (∀pc,k. nat_of_bitvector … pc < program_size → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    387413      (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
    388414        ∃reachable_witness: reachable_program_counter code_memory program_size pc.
     
    391417  λcost_labels: BitVectorTrie costlabel 16.
    392418  λprogram_size: nat.
     419  λprogram_size_limit: program_size ≤ 2^16.
    393420  λreachable_program_counter_witness:
    394421          ∀lbl: costlabel.
     
    396423            reachable_program_counter code_memory program_size program_counter.
    397424  λgood_program_witness: good_program code_memory program_size.
    398     traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness.
    399  
     425    pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness ? program_size_limit).
     426  [1:
     427    @or_intror %
     428  |2:
     429    cases (traverse_code_internal ? ? ? ? ? ? ? ? ?)
     430    #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 %
     431    try assumption #pc #k #pc_program_size_assm
     432    @inductive_hypothesis1
     433    [1:
     434      @le_O_n
     435    |2:
     436      normalize in match (nat_of_bitvector 16 (zero 16));
     437      <plus_n_O assumption
     438    ]
     439  ]
     440qed.
     441   
    400442definition compute_costs ≝
    401443  λprogram: list Byte.
    402444  λcost_labels: BitVectorTrie costlabel 16.
    403445  λreachable_program_witness.
    404   λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
    405     let program_size ≝ |program| + 1 in
     446  λgood_program_witness: good_program (load_code_memory program) (|program|).
     447  λprogram_size_limit: |program| ≤ 2^16.
     448    let program_size ≝ |program| in
    406449    let code_memory ≝ load_code_memory program in
    407       traverse_code code_memory cost_labels program_size reachable_program_witness ?.
    408   @good_program_witness
    409 qed.
     450      traverse_code code_memory cost_labels program_size program_size_limit reachable_program_witness good_program_witness.
Note: See TracChangeset for help on using the changeset viewer.