Changeset 2021
 Timestamp:
 Jun 7, 2012, 1:44:18 AM (6 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2015 r2021 1224 1224 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2 1225 1225 qed. 1226 1226 1227 (*CSC: move elsewhere; also proved in CostProofs as shift_nth_safe *) 1228 lemma nth_safe_prepend: 1229 ∀A,l1,l2,j.∀H:j<l2.∀K:l1+j<(l1@l2). 1230 nth_safe A j l2 H =nth_safe A (l1+j) (l1@l2) K. 1231 #A #l1 elim l1 normalize // 1232 qed. 1233 1234 (*CSC: move elsewhere; also proved in CostProofs as shift_nth_prefix *) 1235 lemma shift_nth_prefix: 1236 ∀T,l1,i,l2,K1,K2. 1237 nth_safe T i l1 K1 = nth_safe T i (l1@l2) K2. 1238 #T #l1 elim l1 normalize 1239 [ 1240 #i #l1 #K1 cases(lt_to_not_zero … K1) 1241  1242 #hd #tl #IH #i #l2 1243 cases i 1244 [ 1245 // 1246  1247 #i' #K1 #K2 whd in ⊢ (??%%); 1248 @IH 1249 ] 1250 ] 1251 qed. 1252 1253 lemma nth_cons: 1254 ∀A,hd,tl,l2,j,d. 1255 nth j A (tl@l2) d =nth (1+j) A (hd::tl@l2) d. 1256 // 1257 qed. 1258 1259 (*CSC: move elsewhere *) 1260 lemma fetch_pseudo_instruction_append: 1261 ∀l1,l2,ppc. 1262 let code_newppc ≝ fetch_pseudo_instruction l2 ppc in 1263 fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (l1)) (ppc)) = 1264 〈\fst code_newppc, add … (bitvector_of_nat … (l1)) (\snd code_newppc)〉. 1265 #l1 elim l1 1266 [ #l2 #ppc >add_commutative <add_zero >add_commutative <add_zero // 1267  #hd #tl #IH #l2 #ppc whd whd in match fetch_pseudo_instruction in ⊢ (??%?); normalize nodelta 1268 (*CSC: FALSE, NEED INVARIANT? *) 1269 > (?: nat_of_bitvector … (add 16 (bitvector_of_nat 16 (hd::tl)) ppc) 1270 = 1 + nat_of_bitvector … (add … (bitvector_of_nat … (tl)) ppc)) [2: cases daemon] 1271 <nth_cons lapply (IH l2 ppc) IH normalize nodelta cases (fetch_pseudo_instruction l2 ppc) 1272 #i #newppc whd in match fetch_pseudo_instruction; normalize nodelta 1273 cases (nth ? labelled_instruction ??) #i' #newppc' normalize nodelta #EQ 1274 destruct EQ change with (add ??? = ?) in e0; 1275 (*CSC: TRUE, NEEDS TRIVIAL ARITHMETICS *) cases daemon 1276 ] 1277 qed. 1278 1227 1279 definition assembly: 1228 1280 ∀p: pseudo_assembly_program. 1229 1281 ∀sigma: Word → Word. 1230 1282 ∀policy: Word → bool. 1231 list Byte × (BitVectorTrie costlabel 16) ≝ 1283 Σres:list Byte × (BitVectorTrie costlabel 16). 1284 let 〈preamble,instr_list〉 ≝ p in 1285 let 〈assembled,costs〉 ≝ res in 1286 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 1287 let datalabels ≝ construct_datalabels preamble in 1288 let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in 1289 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 1290 ∀ppc. 1291 nat_of_bitvector … ppc < instr_list → 1292 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc in 1293 let 〈len,assembledi〉 ≝ 1294 assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in 1295 ∀j:nat. ∀H: j < assembledi. ∀K. 1296 nth_safe ? j assembledi H = 1297 nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j))) 1298 assembled K 1299 ≝ 1232 1300 λp. 1233 1301 λsigma. 1234 1302 λpolicy. 1235 let 〈preamble, instr_list〉≝ p in1303 deplet 〈preamble, instr_list〉 as p_refl ≝ p in 1236 1304 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 1237 1305 let datalabels ≝ construct_datalabels preamble in 1238 1306 let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in 1239 1307 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 1240 let result ≝1241 pi1 ?? (foldl_strong1308 let 〈ignore,revcode〉 ≝ pi1 … ( 1309 foldl_strong 1242 1310 (option Identifier × pseudo_instruction) 1243 (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))). 1244 let 〈pc,ppc_code〉 ≝ pc_ppc_code in 1311 (λpre. Σppc_code:(Word × (list Byte)). 1245 1312 let 〈ppc,code〉 ≝ ppc_code in 1313 ppc = bitvector_of_nat … (pre) ∧ 1246 1314 ∀ppc'. 1247 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in 1248 let 〈len,assembledi〉 ≝ 1249 assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in 1250 True) 1315 nat_of_bitvector … ppc' < nat_of_bitvector … ppc → 1316 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in 1317 let 〈len,assembledi〉 ≝ 1318 assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in 1319 ∀j:nat. ∀H: j < assembledi. ∀K. 1320 nth_safe ? j assembledi H = 1321 nth_safe ? (nat_of_bitvector … (add … (sigma ppc') (bitvector_of_nat ? j))) (reverse … code) K) 1251 1322 instr_list 1252 (λprefix,hd,tl,prf,pc_ppc_code. 1253 let 〈pc, ppc_code〉 ≝ pc_ppc_code in 1254 let 〈ppc, code〉 ≝ ppc_code in 1323 (λprefix,hd,tl,prf,ppc_code. 1324 let 〈ppc, code〉 ≝ pi1 … ppc_code in 1255 1325 let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels (\snd hd) in 1256 let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in1257 1326 let new_ppc ≝ add ? ppc (bitvector_of_nat ? 1) in 1258 〈new_p c, 〈new_ppc, (code @ program)〉〉)1259 〈(zero ?), 〈(zero ?), [ ]〉〉)1327 〈new_ppc, (reverse … program @ code)〉) 1328 〈(zero ?), [ ]〉) 1260 1329 in 1261 〈 \snd (\snd result),1330 〈reverse … revcode, 1262 1331 fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉. 1263 @pair_elim normalize nodelta #x #y #z 1264 @pair_elim normalize nodelta #w1 #w2 #w3 #w4 1265 @pair_elim // 1332 [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode 1333 >EQignore_revcode in Hfold; * #_ #Hfold whd >p1 whd #ppc #LTppc @Hfold 1334 (* CSC: ??? *) cases daemon 1335  % // #ppc' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs)  skip] 1336  cases ppc_code in p1; ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; EQppc_code 1337 * #IH1 #IH2 % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)] 1338 whd #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 1339 cases (le_to_or_lt_eq … LTppc') 1340 [2: #S_S_eq normalize nodelta in S_S_eq; 1341 (*CSC: FALSE, NEEDS INVARIANT *) 1342 cut (ppc' = ppc) [cases daemon] S_S_eq #EQppc' >EQppc' in LTppc'; ppc' #LTppc 1343 >prf >IH1 in ⊢ match % with [_ ⇒ ?]; >(add_zero … (bitvector_of_nat 16 (prefix))) in ⊢ match % with [_ ⇒ ?]; 1344 @pair_elim #pi' #newppc' >fetch_pseudo_instruction_append #EQpair destruct(EQpair) 1345 >p2 1346 #j #LTj 1347 (* CSC: FALSE, NEEDS INVARIANT *) 1348 >(?: nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … j)) = 1349 nat_of_bitvector … (sigma ppc) + j) [2: cases daemon] 1350 >reverse_append >reverse_reverse 1351 (* CSC: TRUE, NEEDS INVARIANT *) 1352 >(? : nat_of_bitvector … (sigma ppc) = reverse … code) [2: cases daemon] 1353 @nth_safe_prepend 1354  #LTppc' lapply (IH2 ppc' ?) [ (*CSC: EASY, FINISH*) cases daemon ] 1355 @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction 1356 @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH 1357 change with (let 〈len,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi' in ∀j:ℕ. ∀H:j<assembledi.?) 1358 >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K 1359 >IH 1360 [2: (*CSC: FALSE, NEEDS INVARIANT? *) cases daemon 1361  @shift_nth_prefix 1362 ] 1363 ] 1364 ] 1266 1365 qed. 1267 1366 
src/ASM/AssemblyProof.ma
r1984 r2021 1574 1574 does not overflow when put into code memory (i.e. shorter than 2^16 bytes). 1575 1575 *) 1576 1577 lemma load_code_memory_ok: 1578 ∀program. 1579 let program_size ≝ program in 1580 program_size ≤ 2^16 → 1581 ∀pc. ∀pc_ok: pc < program_size. 1582 nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)). 1583 #program elim program 1584 [ #_ #pc #abs normalize in abs; @⊥ /2/ 1585  #hd #tl #IH #size_ok * 1586 [ #pc_ok whd in ⊢ (??%?); whd in match (load_code_memory ?); 1587 whd in match next; normalize nodelta 1588  #pc' #pc_ok' whd in ⊢ (??%?); whd in match (load_code_memory ?); 1589 whd in match next; normalize nodelta 1590 ] 1591 cases daemon (*CSC: complete! *) 1592 qed. 1593 (*NO! Prima dimostrare tipo Russell di assembly in Assembly.ma 1594 Poi dimostrare che per ogni i, se fetcho l'iesimo bit di program 1595 e' come fetchare l'iesimo bit dalla memoria. 1596 Concludere assembly_ok come semplice corollario. 1597 *) 1576 1598 lemma assembly_ok: 1577 1599 ∀program. … … 1580 1602 ∀sigma_policy_witness: sigma_policy_specification program sigma policy. 1581 1603 ∀assembled. 1582 ∀costs' .1604 ∀costs': BitVectorTrie costlabel 16. 1583 1605 let 〈preamble, instr_list〉 ≝ program in 1584 1606 let 〈labels, costs〉 ≝ create_label_cost_map instr_list in … … 1586 1608 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in 1587 1609 〈assembled,costs'〉 = assembly program sigma policy → 1588 costs = costs' ∧1610 (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *) 1589 1611 let code_memory ≝ load_code_memory assembled in 1590 1612 let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in … … 1597 1619 sigma newppc = add … pc (bitvector_of_nat … len). 1598 1620 #program #sigma #policy #sigma_policy_witness #assembled #costs' 1599 @pair_elim #preamble #instr_list #program_refl 1600 @pair_elim #labels #costs #create_label_cost_refl 1601 #assembly_refl % cases daemon (* 1602 [1: 1603 (* XXX: lemma on BitVectorTries *) 1604 cases daemon 1605 2: 1606 #ppc #sigma_policy_specification_witness 1607 @pair_elim #pi #newppc #fetch_pseudo_refl 1608 cases pi 1609 [2,3: (* Cost and Comment cases *) 1610 #comment_or_cost normalize in ⊢ (% → ?); #absurd cases absurd 1611 1: (* PreInstruction cases *) 1612 #preinstruction #_ 1613 @pair_elim #len #assembled' #assembly_1_pseudo_refl 1614 normalize nodelta % 1615 [1: 1616 cases assembled' normalize 1617 2: 1618 ] 1619 ] 1620 ] 1621 cases daemon (* XXX: !!! *) *) 1621 cases (assembly program sigma policy) * #assembled' #costs'' 1622 @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %); 1623 @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %); 1624 #assembly_ok #Pair_eq destruct(Pair_eq) whd 1625 #ppc @pair_elim #pi #newppc #eq_fetch_pseudo_instruction 1626 @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd 1627 lapply (assembly_ok ppc ?) [(*CSC: ????? WRONG HERE?*) cases daemon] assembly_ok 1628 >eq_fetch_pseudo_instruction 1629 change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<assembledi.?) → ?) 1630 >(? : assembly_1_pseudoinstruction ????? pi = 〈len,assembled〉) 1631 [2: (*CSC: Provable, isn't it?*) cases daemon 1632  whd in ⊢ (% → ?); #assembly_ok 1633 % 1634 [2: (*CSC: Use Jaap's invariant here *) cases daemon 1635  lapply (load_code_memory_ok assembled' ?) [(*CSC: Jaap?*) cases daemon] 1636 #load_code_memory_ok 1637 eq_assembly_1_pseudoinstruction program policy costs'' labels preamble instr_list costs pi newppc 1638 cut (len=assembled) [(*CSC: provable before cleaning*) cases daemon] #EQlen 1639 (* Nice statement here *) 1640 cut (∀j. ∀H: j < assembled. 1641 nth_safe Byte j assembled H = 1642 \snd (next (load_code_memory assembled') 1643 (bitvector_of_nat 16 1644 (nat_of_bitvector … 1645 (add … (sigma ppc) (bitvector_of_nat … j)))))) 1646 [(*CSC: is it provable?*) cases daemon 1647  assembly_ok load_code_memory_ok generalize in match (sigma ppc); >EQlen len 1648 elim assembled 1649 [ #pc #_ whd <add_zero % 1650  #hd #tl #IH #pc #H % 1651 [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); H #H 1652 >H H whd in ⊢ (??%?); <add_zero // 1653  >(?: add … pc (bitvector_of_nat … (S (tl))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (tl))) 1654 [2: (*CSC: TRUE, ARITHMETIC*) cases daemon] 1655 @IH IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ] 1656 <(nth_safe_prepend … [hd] … LTj) #IH >IH 1657 (*CSC: TRUE, ARITHMETICS*) 1658 cases daemon 1659 ] 1660 ] 1622 1661 qed. 1623 1662 … … 1630 1669 ∀ppc. 1631 1670 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 1632 let 〈assembled, costs'〉 ≝ assembly program sigma policyin1671 let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in 1633 1672 let code_memory ≝ load_code_memory assembled in 1634 1673 let data_labels ≝ construct_datalabels (\fst program) in … … 1649 1688 normalize nodelta 1650 1689 @pair_elim #labels' #costs' #create_label_map_refl' #H 1651 cases (H (sym_eq … assembled_refl)) 1652 #_ 1690 lapply (H (sym_eq … assembled_refl)) H 1653 1691 lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi)) 1654 1692 cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?); … … 1814 1852 λsigma. 1815 1853 λpolicy. 1816 let p ≝ assembly pap sigma policyin1854 let p ≝ pi1 … (assembly pap sigma policy) in 1817 1855 load_code_memory (\fst p). 1818 1856 … … 2329 2367 generalize in match fetch_pseudo_refl; fetch_pseudo_refl 2330 2368 #fetch_pseudo_refl 2331 letin assembled ≝ (\fst ( assembly program sigma policy))2332 letin costs ≝ (\snd ( assembly program sigma policy))2369 letin assembled ≝ (\fst (pi1 … (assembly program sigma policy))) 2370 letin costs ≝ (\snd (pi1 … (assembly program sigma policy))) 2333 2371 lapply (assembly_ok program sigma policy sigma_policy_specification_witness assembled costs) 2334 2372 @pair_elim #preamble #instr_list #program_refl 2335 2373 @pair_elim #labels #costs' #create_label_cost_map_refl 2336 <eq_pair_fst_snd #H cases (H (refl …)) H #costs_refl#H2374 <eq_pair_fst_snd #H lapply (H (refl …)) H #H 2337 2375 lapply (H ppc) H 2338 2376 @pair_elim #pi' #newppc #fetch_pseudo_refl'
Note: See TracChangeset
for help on using the changeset viewer.