Changeset 2110
 Timestamp:
 Jun 26, 2012, 4:05:15 PM (9 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2108 r2110 801 801 (*CSC: move elsewhere *) 802 802 lemma fetch_pseudo_instruction_append: 803 ∀l1,l2. l1@l2 <2^16 → ∀ppc,ppc_ok,ppc_ok'.803 ∀l1,l2. l1@l2 ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'. 804 804 let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in 805 805 fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (l1)) (ppc)) ppc_ok' = … … 807 807 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta 808 808 cut (l1 + nat_of_bitvector … ppc < 2^16) 809 [ @(transitive_l t … l1l2_ok) >length_append /2 by monotonic_lt_plus_r/]809 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ] 810 810 l1l2_ok #l1ppc_ok >nat_of_bitvector_add 811 811 >nat_of_bitvector_bitvector_of_nat_inverse try assumption … … 833 833 ∨ (nat_of_bitvector … ppc = instr_list → next_pc = (zero …))). 834 834 835 (*CSC: Move elsewhere *) 836 axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n. 837 835 838 definition assembly: 836 839 ∀p: pseudo_assembly_program. … … 840 843 sigma_policy_specification p sigma policy → 841 844 let 〈preamble,instr_list〉 ≝ p in 842 instr_list <2^16 →845 instr_list ≤ 2^16 → 843 846 let 〈assembled,costs〉 ≝ res in 847 assembled ≤ 2^16 ∧ 844 848 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 845 849 let datalabels ≝ construct_datalabels preamble in 846 let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in850 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in 847 851 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 848 852 ∀ppc. ∀ppc_ok:nat_of_bitvector … ppc < instr_list. … … 861 865 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 862 866 let datalabels ≝ construct_datalabels preamble in 863 let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in867 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in 864 868 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 865 869 let 〈ignore,revcode〉 ≝ pi1 … ( … … 868 872 (λpre. Σppc_code:(Word × (list Byte)). 869 873 sigma_policy_specification 〈preamble,instr_list〉 sigma policy → 870 instr_list <2^16 →874 instr_list ≤ 2^16 → 871 875 let 〈ppc,code〉 ≝ ppc_code in 872 876 ppc = bitvector_of_nat … (pre) ∧ 873 877 nat_of_bitvector … (sigma ppc) = code ∧ 874 878 ∀ppc'.∀ppc_ok'. 875 nat_of_bitvector … ppc' < nat_of_bitvector … ppc→879 (nat_of_bitvector … ppc' < nat_of_bitvector … ppc ∨ pre = 2^16) → 876 880 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' ppc_ok' in 877 881 let 〈len,assembledi〉 ≝ … … 892 896 [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode 893 897 >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok 894 cases (Hfold sigma_pol_ok instr_list_ok) Hfold * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2 895 >Hfold1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 898 cases (Hfold sigma_pol_ok instr_list_ok) Hfold * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd % 899 [2: #ppc #LTppc @Hfold2 >Hfold1 @(eqb_elim (instr_list) 2^16) 900 [ #limit %2 @limit 901  #nlimit %1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 902 @not_eq_to_le_to_lt assumption ] 903  >length_reverse <Hfold3 904 @(transitive_le … (S (nat_of_bitvector … (sigma ignore)))) 905 [ //  change with (? < ?); @lt_nat_of_bitvector ]] 896 906  * #sigma_pol_ok1 #_ #instr_list_ok % 897 907 [ % // >sigma_pol_ok1 % ] 898 #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs)  skip] 908 #ppc' #ppc_ok' #abs @⊥ cases abs 909 [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2)  skip] 910 #abs2 change with (0 = S ?) in abs2; destruct(abs2) ] 899 911  * #sigma_pol_ok1 #sigma_pol_ok2 #instr_list_ok cases ppc_code in p1; ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; EQppc_code 900 912 #IH cases (IH ? instr_list_ok) [2: % assumption ] * #IH1 #IH3 #IH2 whd % [% 901 913 [ >length_append normalize nodelta >IH1 (*CSC: TRUE, LEMMA NEEDED *) cases daemon 902 914 2: (*CSC: NEES JAAP INVARIANT*) cases daemon]] 903 #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 #LTppc_ppc 904 cases (le_to_or_lt_eq … LTppc_ppc) 905 [2: #S_S_eq normalize nodelta in S_S_eq; 906 (*CSC: TRUE, NEEDS SOME WORK *) 907 cut (ppc' = ppc) [ cases daemon] S_S_eq #EQppc' >EQppc' in LTppc'; ppc' >prf 908 >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc 909 >(add_zero … (bitvector_of_nat 16 (prefix))) in ⊢ (% → match % with [_ ⇒ ?]); 910 >fetch_pseudo_instruction_append 911 [3: @le_S_S @le_O_n 912 2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (prefix))) in ⊢ (% → ?); #H @H 913 4: <prf <p_refl in instr_list_ok; #H @H ] 914 #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2 915 #j #LTj >nat_of_bitvector_add 916 >nat_of_bitvector_bitvector_of_nat_inverse 917 [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon 918 3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ] 919 >reverse_append >reverse_reverse >IH3 <(length_reverse … code) 920 @nth_safe_prepend 921  #LTppc'' 922 cut (nat_of_bitvector … ppc' < instr_list) 923 [ normalize nodelta in LTppc''; 924 @(transitive_le … (nat_of_bitvector … ppc)) 925 [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse 926 [ // 927  <p_refl in instr_list_ok; #instr_list_ok 928 @(transitive_le … (S (instr_list))) try assumption >prf >length_append // ] 929  @le_S_S_to_le >nat_of_bitvector_add in LTppc''; 930 [ >commutative_plus #H @H 931  >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus 932 @(transitive_le … (S (instr_list))) 933 [2: <p_refl in instr_list_ok; #instr_list_ok assumption 934  >IH1 >prf >length_append @le_S_S >(commutative_plus (prefix)) 935 >length_append >nat_of_bitvector_bitvector_of_nat_inverse 936 [2: <p_refl in instr_list_ok; >prf >length_append #H 937 @(transitive_le … H) // 938  @le_S_S // ]]]]] 915 #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 * 916 cases daemon (* 917 ?????????????? PRIMA NON C'ERA L'OR :( 918 MANTENERE LO SCHEMA DI PRIMA CON DUE CASI, MA IN UN CASO ppc=0 OVERFLOWED 919 [2: #eq_S_prefix_bound IH @(IH2 ? LTppc') 920 @pair_elim #pi' #newppc' #eq_fetch_pseudo_instruction' 921 @pair_elim 922  #LTppc_ppc 923 cases (le_to_or_lt_eq … LTppc_ppc) 924 [2: #S_S_eq normalize nodelta in S_S_eq; 925 (*CSC: TRUE, NEEDS SOME WORK *) 926 cut (ppc' = ppc) [ cases daemon] S_S_eq #EQppc' >EQppc' in LTppc'; ppc' >prf 927 >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc 928 >(add_zero … (bitvector_of_nat 16 (prefix))) in ⊢ (% → match % with [_ ⇒ ?]); 929 >fetch_pseudo_instruction_append 930 [3: @le_S_S @le_O_n 931 2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (prefix))) in ⊢ (% → ?); #H @H 932 4: <prf <p_refl in instr_list_ok; #H @H ] 933 #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2 934 #j #LTj >nat_of_bitvector_add 935 >nat_of_bitvector_bitvector_of_nat_inverse 936 [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon 937 3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ] 938 >reverse_append >reverse_reverse >IH3 <(length_reverse … code) 939 @nth_safe_prepend 940  #LTppc'' 941 cut (nat_of_bitvector … ppc' < instr_list) 942 [ normalize nodelta in LTppc''; 943 @(transitive_le … (nat_of_bitvector … ppc)) 944 [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse 945 [ // 946  <p_refl in instr_list_ok; #instr_list_ok 947 @(transitive_le … (S (instr_list))) try assumption >prf >length_append // ] 948  @le_S_S_to_le >nat_of_bitvector_add in LTppc''; 949 [ >commutative_plus #H @H 950  >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus 951 @(transitive_le … (instr_list)) 952 [2: <p_refl in instr_list_ok; #instr_list_ok assumption 953  >IH1 >prf >length_append @le_S_S >(commutative_plus (prefix)) 954 >length_append >nat_of_bitvector_bitvector_of_nat_inverse 955 [2: <p_refl in instr_list_ok; >prf >length_append #H 956 @(transitive_le … H) // 957  @le_S_S // ]]]]] 939 958 #X lapply (IH2 ppc' X) 940 959 @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction … … 952 971  >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse 953 972 [ //  <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]] 954 qed.973 *)qed. 955 974 956 975 definition assembly_unlabelled_program: 
src/ASM/AssemblyProof.ma
r2108 r2110 1511 1511 lemma assembly_ok: 1512 1512 ∀program. 1513 ∀length_proof: \snd program <2^16.1513 ∀length_proof: \snd program ≤ 2^16. 1514 1514 ∀sigma: Word → Word. 1515 1515 ∀policy: Word → bool. … … 1533 1533 sigma newppc = add … pc (bitvector_of_nat … len). 1534 1534 #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs' 1535 @pair_elim #preamble #instr_list #EQprogram1536 1535 cases (assembly program sigma policy) * #assembled' #costs'' 1537 >EQprogram normalize nodelta1538 @pair_elim #labels #costs #EQcreate_label_cost_refl normalize nodelta1539 # assembly_ok #Pair_eq destruct(Pair_eq) whd1540 #ppc #ppc_ok1541 @pair_elim #pi #newppc #EQfetch_pseudo_instruction1542 >EQprogram in sigma_policy_witness; #sigma_policy_witness1543 lapply (assembly_ok sigma_policy_witness ? ppc ?)1544 [2: >EQprogram in length_proof; #length_proof; assumption ] try assumption1545 > EQfetch_pseudo_instruction normalize nodelta1536 @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %); 1537 cut (instr_list ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok 1538 #H lapply (H sigma_policy_witness instr_list_ok) H whd in ⊢ (% → ?); 1539 @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %); 1540 * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd 1541 #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction 1542 @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd 1543 lapply (assembly_ok2 ppc ?) try // assembly_ok2 1544 >eq_fetch_pseudo_instruction 1546 1545 change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<assembledi.?) → ?) 1547 @pair_elim #len #assembledi #EQassembly_1_pseudo_instruction 1548 letin lookup_labels ≝ (λx.sigma (bitvector_of_nat 16 (lookup_def ASMTag ℕ labels x O))) 1549 letin lookup_datalabels ≝ (λx. lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)) 1550 >(? : assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi = 〈len,assembledi〉) 1551 [2: <EQassembly_1_pseudo_instruction % ] 1552 whd in ⊢ (% → ?); #assembly_ok % 1553 [2: (*CSC: Use Jaap's invariant here *) cases daemon 1554 1: 1555 lapply (load_code_memory_ok assembledi ?) 1556 [1: 1557 lapply sigma_policy_witness whd in match sigma_policy_specification; 1558 normalize nodelta * #_ #relevant 1559 (* XXX: wait for Jaap to propagate the property that program 1560 is less than 2^16. 1561 *) 1546 > (?:((λx.bitvector_of_nat ? (lookup_def … labels x 0)) = 1547 (λx.address_of_word_labels_code_mem instr_list x))) 1548 [2: lapply (create_label_cost_map_ok 〈preamble,instr_list〉) >create_label_cost_refl 1549 #H (*CSC: REQUIRES FUNCTIONAL EXTENSIONALITY; REPHRASE THE LEMMA *) cases daemon ] 1550 >eq_assembly_1_pseudoinstruction 1551 whd in ⊢ (% → ?); #assembly_ok 1552 % 1553 [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction)) 1554 >snd_fetch_pseudo_instruction 1555 cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) H 1556 #spw1 #_ >spw1 spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f 1557 >eq_fetch_pseudo_instruction whd in match instruction_size; 1558 normalize nodelta (*CSC: TRUE, NEEDS LEMMA AND FUNCTIONAL EXTENSIONALITY *) 1562 1559 cases daemon 1563 1560  lapply (load_code_memory_ok assembled' ?) [ assumption ] 1564 1561 #load_code_memory_ok 1565 cut (len=assembled i)1562 cut (len=assembled) 1566 1563 [1: (*CSC: provable before cleaning *) 1567 1564 cases daemon … … 1569 1566 #EQlen 1570 1567 (* Nice statement here *) 1571 cut (∀j. ∀H: j < assembled i.1572 nth_safe Byte j assembled iH =1568 cut (∀j. ∀H: j < assembled. 1569 nth_safe Byte j assembled H = 1573 1570 \snd (next (load_code_memory assembled') 1574 1571 (bitvector_of_nat 16 … … 1579 1576 2: 1580 1577 assembly_ok load_code_memory_ok generalize in match (sigma ppc); >EQlen len 1581 elim assembled i1578 elim assembled 1582 1579 [1: 1583 #pc #_ whd (*<add_zero %1584 1580 #pc #_ whd <add_zero % 1581  #hd #tl #IH #pc #H % 1585 1582 [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); H #H 1586 1583 >H H whd in ⊢ (??%?); <add_zero // 1587 1584  >(?: add … pc (bitvector_of_nat … (S (tl))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (tl))) 1588 [2: (*CSC: TRUE, ARITHMETIC*) cases daemon]1585 [2: <add_bitvector_of_nat_Sm @add_associative ] 1589 1586 @IH IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ] 1590 <(nth_safe_prepend … [hd] … LTj) #IH >IH 1591 (*CSC: TRUE, ARITHMETICS*) 1592 cases daemon 1593 ] 1594 ] *) cases daemon 1595 ] 1596 cases daemon 1587 <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm 1588 >add_associative % ]] 1589 ]] 1597 1590 qed. 1598 1591 … … 1600 1593 lemma fetch_assembly_pseudo2: 1601 1594 ∀program. 1602 ∀length_proof: \snd program <2^16.1595 ∀length_proof: \snd program ≤ 2^16. 1603 1596 ∀sigma. 1604 1597 ∀policy. … … 1973 1966 match pol lookup_labels ppc with 1974 1967 [ short_jump ⇒ 〈2, 2〉 1975  medium_jump ⇒ ?1968  absolute_jump ⇒ ? 1976 1969  long_jump ⇒ 〈4, 4〉 1977 1970 ] *) … … 1979 1972 match pol lookup_labels ppc with 1980 1973 [ short_jump ⇒ 〈2, 2〉 1981  medium_jump ⇒ ?1974  absolute_jump ⇒ ? 1982 1975  long_jump ⇒ 〈4, 4〉 1983 1976 ] *) … … 1985 1978 match pol lookup_labels ppc with 1986 1979 [ short_jump ⇒ 〈2, 2〉 1987  medium_jump ⇒ ?1980  absolute_jump ⇒ ? 1988 1981  long_jump ⇒ 〈4, 4〉 1989 1982 ] *) … … 1991 1984 match pol lookup_labels ppc with 1992 1985 [ short_jump ⇒ 〈2, 2〉 1993  medium_jump ⇒ ?1986  absolute_jump ⇒ ? 1994 1987  long_jump ⇒ 〈4, 4〉 1995 1988 ] *) … … 1997 1990 match pol lookup_labels ppc with 1998 1991 [ short_jump ⇒ 〈2, 2〉 1999  medium_jump ⇒ ?1992  absolute_jump ⇒ ? 2000 1993  long_jump ⇒ 〈4, 4〉 2001 1994 ] *) … … 2003 1996 match pol lookup_labels ppc with 2004 1997 [ short_jump ⇒ 〈2, 2〉 2005  medium_jump ⇒ ?1998  absolute_jump ⇒ ? 2006 1999  long_jump ⇒ 〈4, 4〉 2007 2000 ] *) … … 2009 2002 match pol lookup_labels ppc with 2010 2003 [ short_jump ⇒ 〈2, 2〉 2011  medium_jump ⇒ ?2004  absolute_jump ⇒ ? 2012 2005  long_jump ⇒ 〈4, 4〉 2013 2006 ] *) … … 2015 2008 match pol lookup_labels ppc with 2016 2009 [ short_jump ⇒ 〈2, 2〉 2017  medium_jump ⇒ ?2010  absolute_jump ⇒ ? 2018 2011  long_jump ⇒ 〈4, 4〉 2019 2012 ] *) … … 2021 2014 match pol lookup_labels ppc with 2022 2015 [ short_jump ⇒ 〈2, 2〉 2023  medium_jump ⇒ ?2016  absolute_jump ⇒ ? 2024 2017  long_jump ⇒ 〈4, 4〉 2025 2018 ] *) … … 2320 2313 lemma snd_assembly_1_pseudoinstruction_ok: 2321 2314 ∀program: pseudo_assembly_program. 2322 ∀program_length_proof: \snd program <2^16.2315 ∀program_length_proof: \snd program ≤ 2^16. 2323 2316 ∀sigma: Word → Word. 2324 2317 ∀policy: Word → bool. 
src/ASM/AssemblyProofSplitSplit.ma
r2062 r2110 81 81 qed. 82 82 83 lemma medium_jump_cond_ok:83 lemma absolute_jump_cond_ok: 84 84 ∀v1, v2: Word. 85 85 ∀is_possible, offset, v1_upper, v1_lower. 86 〈is_possible, offset〉 = medium_jump_cond v1 v2 →86 〈is_possible, offset〉 = absolute_jump_cond v1 v2 → 87 87 〈v1_upper, v1_lower〉 = vsplit ? 5 11 v1 → 88 88 is_possible → v2 = v1_upper @@ offset. 89 89 #v1 #v2 #is_possible #offset #v1_upper #v1_lower 90 whd in match medium_jump_cond; normalize nodelta90 whd in match absolute_jump_cond; normalize nodelta 91 91 @pair_elim #fst_5_addr #rest_addr #vsplit_v2_refl 92 92 @pair_elim #fst_5_pc #rest_pc #vsplit_v1_refl … … 202 202 inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta 203 203 [2: 204 inversion ( medium_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta204 inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta 205 205 inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta 206 206 ] … … 240 240 [1: 241 241 >EQlookup_labels in mjc_refl; #mjc_refl 242 @( medium_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))242 @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl)) 243 243 >(andb_true_l … mj_possible_refl) @I 244 244 ]
Note: See TracChangeset
for help on using the changeset viewer.