Changeset 3097
 Timestamp:
 Apr 5, 2013, 9:53:44 PM (6 years ago)
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

driver/extracted/policyStep.ml
r3095 r3097 92 92 PolicyFront.ppc_pc_map Types.option) Types.prod Types.sig0 **) 93 93 let jump_expansion_step program labels old_sigma = 94 (let { Types.fst = final_added; Types.snd = final_policy} =94 (let { Types.fst = ignore; Types.snd = res } = 95 95 Types.pi1 96 (FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ acc > 97 let prefixlen = List.length prefix in 98 let bvprefixlen = 99 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 100 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 101 (Nat.S (Nat.S Nat.O)))))))))))))))) prefixlen 102 in 96 (FoldStuff.foldl_strong (Types.pi1 program) 97 (fun prefix x tl _ prefixlens_acc > 98 (let { Types.fst = prefixlens; Types.snd = acc } = 99 Types.pi1 prefixlens_acc 100 in 101 (fun _ > 102 (let { Types.fst = prefixlen; Types.snd = bvprefixlen } = prefixlens 103 in 104 (fun _ > 103 105 let bvSprefixlen = 104 106 Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 106 108 (Nat.S Nat.O)))))))))))))))) bvprefixlen 107 109 in 108 (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } = 109 Types.pi1 acc 110 in 110 (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } = acc in 111 111 (fun _ > 112 112 (let { Types.fst = label; Types.snd = instr } = x in … … 174 174 Types.snd = new_length } inc_sigma) 175 175 in 176 { Types.fst = { Types.fst = (Nat.S prefixlen); Types.snd = 177 (Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 178 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 179 (Nat.S Nat.O)))))))))))))))) bvprefixlen) }; Types.snd = 176 180 { Types.fst = new_added; Types.snd = { Types.fst = 177 (Nat.plus inc_pc isize); Types.snd = updated_sigma } })) __)) __) 178 { Types.fst = Nat.O; Types.snd = { Types.fst = Nat.O; Types.snd = 181 (Nat.plus inc_pc isize); Types.snd = updated_sigma } } })) __)) __)) 182 __)) __) { Types.fst = { Types.fst = Nat.O; Types.snd = 183 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 184 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 185 Nat.O))))))))))))))))) }; Types.snd = { Types.fst = Nat.O; 186 Types.snd = { Types.fst = Nat.O; Types.snd = 179 187 (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 180 188 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 193 201 Assembly.Short_jump }).Types.snd } (BitVectorTrie.Stub (Nat.S 194 202 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 195 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } } )203 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } } }) 196 204 in 205 (fun _ > 206 (let { Types.fst = final_added; Types.snd = final_policy } = res in 197 207 (fun _ > 198 208 (match Util.gtb final_policy.Types.fst … … 205 215  Bool.False > 206 216 (fun _ > { Types.fst = (Nat.eqb final_added Nat.O); Types.snd = 207 (Types.Some final_policy) })) __)) __ 208 217 (Types.Some final_policy) })) __)) __)) __ 218 
src/ASM/PolicyStep.ma
r3095 r3097 1137 1137 ≝ 1138 1138 λprogram.λlabels.λold_sigma. 1139 let 〈 final_added, final_policy〉 ≝1139 let 〈ignore,res〉 ≝ 1140 1140 pi1 ?? (foldl_strong (option Identifier × pseudo_instruction) 1141 (λprefix.Σx:ℕ × ppc_pc_map. 1141 (λprefix.Σxx:(ℕ × Word) × (ℕ × ppc_pc_map). 1142 let 〈prefixlens,x〉 ≝ xx in 1143 let 〈prefixlen,bvprefixlen〉 ≝ prefixlens in 1142 1144 let 〈added,policy〉 ≝ x in 1143 And (And (And (And (And (And (And (And (And (not_jump_default prefix policy) 1145 And (And (prefixlen = prefix) (bvprefixlen = bitvector_of_nat … prefixlen)) 1146 (And (And (And (And (And (And (And (And (And (not_jump_default prefix policy) 1144 1147 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 1145 1148 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉))) … … 1151 1154 (\fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉) = 1152 1155 \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) + added)) 1153 (sigma_safe prefix labels old_sigma policy)) 1156 (sigma_safe prefix labels old_sigma policy))) 1154 1157 program 1155 (λprefix.λx.λtl.λprf.λ acc.1156 let prefixlen ≝ prefixin1157 let bvprefixlen ≝ bitvector_of_nat ? prefixlenin1158 let bvSprefixlen ≝ increment … bvprefixlen in 1159 let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc)in1158 (λprefix.λx.λtl.λprf.λprefixlens_acc. 1159 let 〈prefixlens,acc〉 ≝ (pi1 ?? prefixlens_acc) in 1160 let 〈prefixlen,bvprefixlen〉 ≝ prefixlens in 1161 let bvSprefixlen ≝ increment … bvprefixlen in 1162 let 〈inc_added, inc_pc_sigma〉 ≝ acc in 1160 1163 let 〈label,instr〉 ≝ x in 1161 1164 (* Now, we must add the current ppc and its pc translation. … … 1192 1195 bvt_insert … bvSprefixlen 〈inc_pc + isize, old_Slength〉 1193 1196 (bvt_insert … bvprefixlen 〈inc_pc, new_length〉 inc_sigma) in 1194 〈 new_added, 〈plus inc_pc isize, updated_sigma〉〉1195 ) 〈 0, 〈0,1197 〈〈S prefixlen,increment … bvprefixlen〉,〈new_added, 〈plus inc_pc isize, updated_sigma〉〉〉 1198 ) 〈〈0,zero 16〉,〈0, 〈0, 1196 1199 bvt_insert … 1197 1200 (bitvector_of_nat ? 0) 1198 1201 〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉 1199 (Stub ??)〉〉 1202 (Stub ??)〉〉〉 1200 1203 ) in 1204 let 〈final_added, final_policy〉 ≝ res in 1201 1205 if gtb (\fst final_policy) 2^16 then 1202 1206 〈eqb final_added 0, None ?〉 … … 1204 1208 〈eqb final_added 0, Some ? final_policy〉. 1205 1209 [ normalize nodelta @nmk #Habs lapply p p cases (foldl_strong ? (λ_.Σx.?) ???) 1206 #x #H #Heq >Heq in H; normalize nodelta Heq x #Hind 1210 #x #H #Heq >Heq in H; normalize nodelta Heq x cases ignore #prefixlen #bvprefixlen 1211 >p1 res normalize nodelta * #EQprefixlens #Hind 1207 1212 (* USE: inc_pc = fst of policy (from fold) *) 1208 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p 1;1213 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p2; 1209 1214 (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *) 1210 1215 lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) … … 1236 1241 @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge 1237 1242 ] 1238  normalize nodelta lapply p p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2 1239 >H2 in H; normalize nodelta H2 x #H @conj 1240 [ @conj [ @conj 1243  normalize nodelta lapply p p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); 1244 #x normalize nodelta #H #H2 1245 >H2 in H; normalize nodelta H2 x cases ignore ignore #prefixlen #bvprefixlen 1246 normalize nodelta >p1 p1 normalize nodelta * #EQprefixlens #H @conj 1247 [ @conj [ @conj 1241 1248 [ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy, 1242 1249 * jump_increase, sigma_compact_unsafe (from fold) *) … … 1248 1255 #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2 1249 1256 ] 1250  @not_lt_to_le @ltb_false_to_not_lt @p 11257  @not_lt_to_le @ltb_false_to_not_lt @p2 1251 1258 ] 1252 1259 4: 1253 >(?:bvSprefixlen = bitvector_of_nat … (S prefixlen)) 1254 [2: normalize nodelta >increment_zero_bitvector_of_nat_1 <add_bitvector_of_nat %] 1255 lapply (pi2 ?? acc) >p acc inversion inc_pc_sigma 1260 lapply (pi2 ?? prefixlens_acc) >p in ⊢ (% → ?); prefixlens_acc normalize nodelta 1261 >p1 prefixlens >p2 acc >p3 in prf; x #prf normalize nodelta inversion inc_pc_sigma 1256 1262 #inc_pc #inc_sigma #Hips normalize nodelta 1257 1263 inversion (bvt_lookup … bvprefixlen (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 1258 #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim 1259 #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta 1260 #Heq1 #Heq2 1264 #old_pc #old_length #Holdeq ** #Hpolicy1 >Hpolicy1 prefixlen 1265 #Hpolicy2 >Hpolicy2 in Holdeq; bvprefixlen #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim * 1266 #prefixlen' #bvprefixlen' * #added #policy normalize nodelta @pair_elim #new_length #isize 1267 normalize nodelta #Heq1 #Heq2 cases (pair_destruct ?????? Heq2) Heq2 1268 #Heq2c cases (pair_destruct ?????? Heq2c) Heq2c #Heq2c <Heq2c prefixlen' 1269 #Heq2d <Heq2d bvprefixlen' #Heq2 1261 1270 cut (S (prefix) < 2^16) 1262 1271 [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length 1263 1272 <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1 1264 1273 cut (prefix < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok 1265 cases (pair_destruct ?????? Heq2) Heq2 #Heq2a #Heq2b 1266 % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]] 1267 [ (* not_jump_default *) 1274 cases (pair_destruct ?????? Heq2) Heq2 #Heq2a 1275 >(?:increment … (bitvector_of_nat … (prefix)) = bitvector_of_nat … (S (prefix))) 1276 [2: >increment_zero_bitvector_of_nat_1 <add_bitvector_of_nat %] 1277 #Heq2b <Heq2a normalize nodelta 1278 % [ %  % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]] 1279 [ >length_append <plus_n_Sm <plus_n_O % 1280  % 1281  (* not_jump_default *) 1268 1282 @(jump_expansion_step1 … Heq1 Heq2b) try assumption 1269 1283 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) … … 1275 1289 <Heq2b >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 1276 1290  (* jump_increase *) 1277 @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … p1??? old_length Holdeq1291 @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … ???? old_length Holdeq 1278 1292 … Heq1 prefix_ok1 prefix_ok Heq2b) 1279 1293 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 1280 cases (pi2 … old_sigma) * * * #Hnjd #_ #_ #_ #_ @Hnjd1294 try % cases (pi2 … old_sigma) * * * #Hnjd #_ #_ #_ #_ @Hnjd 1281 1295  (* sigma_compact_unsafe *) 1282 1296 @(jump_expansion_step4 … Heq1 … Heq2b) try assumption … … 1286 1300  (* policy_jump_equal → added = 0 *) 1287 1301 @(jump_expansion_step5 … inc_added … Holdeq … Heq1 … Heq2b) try assumption 1288 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) 1302 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) try % 1289 1303 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1290 1304  (* added = 0 → policy_pc_equal *) 1305 >Heq2a 1291 1306 @(jump_expansion_step6 (pi1 ?? program) (pi1 ?? labels) (pi1 ?? old_sigma) … Holdeq … Heq1 … Heq2a Heq2b) try assumption 1292 1307 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) 1293 1308 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1294 cases (pi2 … old_sigma) * #_ #X #_ @X1309 try (cases (pi2 … old_sigma) * #_ #X #_ @X) % 1295 1310  (* out_of_program_none *) 1296 1311 @(jump_expansion_step7 … Heq2b) 1297 1312 @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) 1298 1313  (* lookup p = lookup old_sigma + added *) 1314 >Heq2a 1299 1315 @(jump_expansion_step8 (pi1 ?? program) (pi1 ?? labels) (pi1 ?? old_sigma) … Holdeq … Heq1 Heq2a Heq2b) try assumption 1300 1316 [ cases (pi2 … old_sigma) * #_ #H1 #H2 % assumption 1317  % 1301 1318  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1302  @(proj2 ?? (proj1 ?? Hpolicy)) ] 1319  >(proj2 ?? (proj1 ?? Hpolicy)) @eq_f2 try % 1320 cases (lookup (? × ?)????) in Holdeq; #x #y #H destruct (H) % 1321 ] 1303 1322  (* sigma_safe *) 1304 @(jump_expansion_step9 … prf … p1 … Holdeq … Heq1 prefix_ok1 prefix_ok) 1323 >Heq2a 1324 @(jump_expansion_step9 … prf … Holdeq … Heq1 prefix_ok1 prefix_ok) 1305 1325 [ @inc_pc_sigma 1326  % 1306 1327  >Hips % 1307 1328  @inc_added 1308 1329  >Hips @Heq2b 1309 1330  @(proj2 ?? (proj1 ?? (pi2 ?? old_sigma))) 1310  >Hips @(proj2 ?? (proj1 ?? Hpolicy)) 1331  >Hips >(proj2 ?? (proj1 ?? Hpolicy)) @eq_f2 try % 1332 cases (lookup (? × ?)????) in Holdeq; #x #y #H destruct (H) % 1311 1333  >Hips @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1312 1334  >Hips @(proj2 ?? Hpolicy) 1313 1335 ] 1314 1336 ] 1315  normalize nodelta % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]] 1316 [ #i cases i 1337  normalize nodelta % [%  % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]] 1338 [ % 1339  % 1340  #i cases i 1317 1341 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1318 1342  i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O 1319 1343 ] 1320  >lookup_insert_hit @refl 1344  >lookup_insert_hit @refl 1321 1345  >lookup_insert_hit @refl 1322 1346  #i #Hi <(le_n_O_to_eq … Hi)
Note: See TracChangeset
for help on using the changeset viewer.