Ignore:
Timestamp:
May 9, 2012, 2:44:39 PM (8 years ago)
Author:
mulligan
Message:

Simplified proof by removing most of the invariants on the statements all together (reachable_program_counter, good_program), and fixing the size of the total_program_size to be constantly 216.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r1928 r1929  
    66let rec traverse_code_internal
    77  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    8     (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
    9       (reachable_program_counter_witness:
    10           ∀lbl: costlabel.
    11           ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
    12             reachable_program_counter code_memory fixed_program_size program_counter)
    13         (good_program_witness: good_program code_memory fixed_program_size)
    14         (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size)
    15         (fixed_program_size_limit: fixed_program_size ≤ 2^16)
     8    (program_counter: Word) (program_size: nat)
     9      (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16)
    1610        on program_size:
    1711          Σcost_map: identifier_map CostTag nat.
    1812            (∀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) ∧
    1913            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧
    20               ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
    21                 pi1 … (block_cost code_memory pc fixed_program_size fixed_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
     14               pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
    2215  match program_size return λx. x = program_size → Σcost_map: ?. ? with
    2316  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
    2417  | S program_size' ⇒ λprogram_size_refl.
    2518    deplet 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in
    26     let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' fixed_program_size program_size' ? good_program_witness ? fixed_program_size_limit in
     19    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in
    2720    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
    2821    [ None ⇒ λlookup_refl. pi1 … cost_mapping
    2922    | Some lbl ⇒ λlookup_refl.
    30       let cost ≝ block_cost code_memory program_counter fixed_program_size fixed_program_size_limit cost_labels ? good_program_witness in
     23      let cost ≝ block_cost code_memory program_counter cost_labels in
    3124        add … cost_mapping lbl cost
    3225    ] (refl … (lookup_opt … program_counter cost_labels))
    3326  ] (refl … program_size).
    34   [5:
    35     assumption
    36   |4:
    37     @(reachable_program_counter_witness lbl)
    38     @lookup_refl
    39   |3:
     27  [3:
    4028    cases program_size_invariant
    4129    [1:
     
    8068              @succ_nat_of_bitvector_half_add_1
    8169              @le_plus_to_minus_r
    82               @(transitive_le … fixed_program_size_limit)
    8370              change with (S ? ≤ ?) >plus_n_Sm
     71              <program_size_invariant'
    8472              @monotonic_le_plus_r
    8573              @le_S_S @le_S_S @le_O_n
     
    128116            >eq_assm >lookup_refl %
    129117          |2:
    130             %{(reachable_program_counter_witness …)} try assumption
    131118            >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
    132119          ]
     
    142129              cases ind_hyp' #assm #_ assumption
    143130            |2:
    144               cases ind_hyp' #lookup_opt_assm * #reachable_witness'
    145               #ind_hyp'' %{reachable_witness'} >ind_hyp''
     131              cases ind_hyp' #lookup_opt_assm #ind_hyp'' >ind_hyp''
    146132              @sym_eq @lookup_present_add_miss assumption
    147133            ]
     
    207193                  @succ_nat_of_bitvector_half_add_1
    208194                  @le_plus_to_minus_r
    209                   @(transitive_le … fixed_program_size_limit)
    210195                  change with (S ? ≤ ?) >plus_n_Sm
     196                  <program_size_invariant
    211197                  @monotonic_le_plus_r
    212198                  @le_S_S @le_S_S @le_O_n
     
    228214              @succ_nat_of_bitvector_half_add_1
    229215              @le_plus_to_minus_r
    230               @(transitive_le … fixed_program_size_limit)
    231216              change with (S ? ≤ ?) >plus_n_Sm
     217              <program_size_invariant
    232218              @monotonic_le_plus_r
    233219              @le_S_S @le_S_S @le_O_n
     
    244230      assumption
    245231    ]
    246   |6:
     232  |4:
    247233    inversion program_size'
    248234    [1:
     
    262248          @succ_nat_of_bitvector_half_add_1
    263249          @le_plus_to_minus_r
    264           @(transitive_le … fixed_program_size_limit)
    265250          change with (S ? ≤ ?) >plus_n_Sm
     251          <relevant
    266252          @monotonic_le_plus_r
    267253          @le_S_S @le_S_S @le_O_n
     
    288274qed.
    289275
     276(* XXX:
     277 * At the moment we do a full traversal of the code memory, however we could do
     278 * a fold over the domain of the cost labels map.
     279 *
     280 *)
    290281definition traverse_code:
    291282  ∀code_memory: BitVectorTrie Byte 16.
     
    295286      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
    296287        pc = pc'.
    297   ∀program_size: nat.
    298   ∀program_size_limit: program_size ≤ 2^16.
    299   ∀reachable_program_counter_witness:
    300     ∀lbl: costlabel.
    301     ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
    302       reachable_program_counter code_memory program_size program_counter.
    303   ∀good_program_witness: good_program code_memory program_size.
    304288    Σcost_map: identifier_map CostTag nat.
    305       (∀pc,k. nat_of_bitvector … pc < program_size → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
     289      (∀pc,k. nat_of_bitvector … pc < 2^16 → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    306290      (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    307         ∃reachable_witness: reachable_program_counter code_memory program_size pc.
    308           pi1 … (block_cost code_memory pc program_size program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
     291          pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
    309292  λcode_memory: BitVectorTrie Byte 16.
    310293  λcost_labels: BitVectorTrie costlabel 16.
    311294  λcost_labels_injective.
    312   λprogram_size: nat.
    313   λprogram_size_limit: program_size ≤ 2^16.
    314   λreachable_program_counter_witness:
    315           ∀lbl: costlabel.
    316           ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
    317             reachable_program_counter code_memory program_size program_counter.
    318   λgood_program_witness: good_program code_memory program_size.
    319     pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness ? program_size_limit).
     295    pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?).
    320296  [1:
    321297    @or_intror %
    322298  |2:
    323     cases (traverse_code_internal ? ? ? ? ? ? ? ? ?)
     299    cases (traverse_code_internal ?????)
    324300    #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 %
    325301    [1:
     
    335311      #k #k_pres #pc #lookup_opt_assm
    336312      cases (inductive_hypothesis2 ? k_pres)
    337       #program_counter' * #lookup_opt_assm' * #reachable_witness
    338       #block_cost_assm
     313      #program_counter' * #lookup_opt_assm' #block_cost_assm
    339314      >(cost_labels_injective … lookup_opt_assm lookup_opt_assm')
    340       %{reachable_witness} assumption
     315      assumption
    341316    ]
    342317  ]
     
    350325      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
    351326        pc = pc'.
    352   λreachable_program_witness.
    353   λgood_program_witness: good_program (load_code_memory program) (|program|).
    354   λprogram_size_limit: |program| ≤ 2^16.
    355327    let program_size ≝ |program| in
    356328    let code_memory ≝ load_code_memory program in
    357       traverse_code code_memory cost_labels cost_labels_injective program_size program_size_limit reachable_program_witness good_program_witness.
     329      traverse_code code_memory cost_labels cost_labels_injective.
Note: See TracChangeset for help on using the changeset viewer.