Changeset 979


Ignore:
Timestamp:
Jun 16, 2011, 2:26:47 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r977 r979  
    11301130qed.
    11311131
     1132example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
     1133 cases daemon.
     1134qed.
     1135
     1136axiom construct_costs_sigma:
     1137 ∀p,ppc,pc,pc',costs,costs',i.
     1138  bitvector_of_nat ? pc = sigma p (bitvector_of_nat ? ppc) →
     1139   Some … 〈pc',costs'〉 = construct_costs p ppc pc (λx.zero 16) (λx.zero 16) costs i →
     1140    bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)).
     1141
    11321142definition build_maps' ≝
    11331143  λpseudo_program.
     
    11391149      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
    11401150      let 〈pc',costs〉 ≝ pc_costs in
     1151       bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧
    11411152       ppc' = length … pre ∧
    11421153       tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
     
    11691180   let 〈pc, costs〉 ≝ pc_costs in
    11701181    〈labels, costs〉.
    1171  [3: whd % [%] // #id normalize in ⊢ (% → ?) #abs @⊥ //
    1172  | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * #IH0 #IH1 #IH2
    1173    cases construct in p4 #PC #CODE #JMEQ % [%]
    1174    [ >length_append <IH0 normalize; //
     1182 [3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
     1183 | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
     1184   cases construct in p4 #PC #CODE #JMEQ % [% [%]]
     1185   [ @(construct_costs_sigma … IHn1) [4: <JMEQ % |*: skip]
     1186   | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
    11751187   | @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
    11761188   | #id normalize nodelta; -labels1; cases label; normalize nodelta
    1177      [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 //
     1189     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
    11781190     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
    11791191       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
    11801192        [ #EQ #_ <(eq_bv_to_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
    1181           <IH0
    1182         | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: /2/]
    1183           <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 //]]]
     1193          <IH0 [@IHn1 | <(eq_bv_to_eq … EQ) in H #H @H]
     1194        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
     1195          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
    11841196 | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
    11851197   @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
Note: See TracChangeset for help on using the changeset viewer.