 Timestamp:
 Jun 16, 2011, 2:26:47 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r977 r979 1130 1130 qed. 1131 1131 1132 example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0. 1133 cases daemon. 1134 qed. 1135 1136 axiom 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 1132 1142 definition build_maps' ≝ 1133 1143 λpseudo_program. … … 1139 1149 let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in 1140 1150 let 〈pc',costs〉 ≝ pc_costs in 1151 bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧ 1141 1152 ppc' = length … pre ∧ 1142 1153 tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧ … … 1169 1180 let 〈pc, costs〉 ≝ pc_costs in 1170 1181 〈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!*) // 1175 1187  @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ)) 1176 1188  #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!*) // 1178 1190  #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?; 1179 1191 generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %) 1180 1192 [ #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; //]]] 1184 1196  (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2 1185 1197 @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
Note: See TracChangeset
for help on using the changeset viewer.