Ignore:
Timestamp:
May 8, 2012, 3:29:25 PM (8 years ago)
Author:
mulligan
Message:

Horror proof mostly finished (compiles all way until end of CostsProof?.ma).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r1919 r1921  
    4040       match ${fresh xy} return λx.∀${ident E}:? = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
    4141        λ${ident E}.$s ] ] (refl ? $t) }.
     42
     43definition nat_of_bool: bool → nat ≝
     44  λb: bool.
     45  match b with
     46  [ true ⇒ 1
     47  | false ⇒ 0
     48  ].
     49
     50lemma blah:
     51  ∀n: nat.
     52  ∀bv: BitVector n.
     53  ∀buffer: nat.
     54    nat_of_bitvector_aux n buffer bv = nat_of_bitvector n bv + (buffer * 2^n).
     55  #n #bv elim bv
     56  [1:
     57    #buffer elim buffer try %
     58    #buffer' #inductive_hypothesis
     59    normalize <times_n_1 %
     60  |2:
     61    #n' #hd #tl #inductive_hypothesis
     62    #buffer cases hd normalize
     63    >inductive_hypothesis
     64    >inductive_hypothesis
     65    [1:
     66      change with (
     67        ? + (2 * buffer + 1) * ?) in ⊢ (??%?);
     68      change with (
     69        ? + buffer * (2 * 2^n')) in ⊢ (???%);
     70      cases daemon
     71    ]
     72  ]
     73  cases daemon
     74qed.
     75
     76lemma nat_of_bitvector_aux_hd_tl:
     77  ∀n: nat.
     78  ∀tl: BitVector n.
     79  ∀hd: bool.
     80    nat_of_bitvector (S n) (hd:::tl) =
     81      nat_of_bitvector n tl + (nat_of_bool hd * 2^n).
     82  #n #tl elim tl
     83  [1:
     84    #hd cases hd %
     85  |2:
     86    #n' #hd' #tl' #inductive_hypothesis #hd
     87    cases hd whd in ⊢ (??%?); normalize nodelta
     88    >inductive_hypothesis cases hd' normalize nodelta
     89    normalize in match (nat_of_bool ?);
     90    normalize in match (nat_of_bool ?);
     91    [4:
     92      normalize in match (2 * ?);
     93      <plus_n_O <plus_n_O %
     94    |3:
     95      normalize in match (2 * ?);
     96      normalize in match (0 + 1);
     97      <plus_n_O
     98      normalize in match (1 * ?);
     99      <plus_n_O
     100      cases daemon
     101      (* XXX: lemma *)
     102    |*:
     103      cases daemon
     104    ]
     105  ]
     106qed.
    42107
    43108lemma succ_nat_of_bitvector_aux_half_add_1:
     
    74139qed.
    75140   
     141include alias "arithmetics/nat.ma".
     142include alias "basics/logic.ma".
     143   
    76144let rec traverse_code_internal
    77145  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     
    89157            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧
    90158              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
    91                 pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
     159                pi1 … (block_cost code_memory pc fixed_program_size fixed_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
    92160  match program_size return λx. x = program_size → Σcost_map: ?. ? with
    93161  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
     
    98166    [ None ⇒ λlookup_refl. pi1 … cost_mapping
    99167    | Some lbl ⇒ λlookup_refl.
    100       let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
     168      let cost ≝ block_cost code_memory program_counter fixed_program_size fixed_program_size_limit cost_labels ? good_program_witness in
    101169        add … cost_mapping lbl cost
    102170    ] (refl … (lookup_opt … program_counter cost_labels))
     
    395463      (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    396464        ∃reachable_witness: reachable_program_counter code_memory program_size pc.
    397           pi1 … (block_cost code_memory pc program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
     465          pi1 … (block_cost code_memory pc program_size program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
    398466  λcode_memory: BitVectorTrie Byte 16.
    399467  λcost_labels: BitVectorTrie costlabel 16.
Note: See TracChangeset for help on using the changeset viewer.