Changeset 2021 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 7, 2012, 1:44:18 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.