 Timestamp:
 Jul 17, 2012, 10:18:01 AM (8 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2193 r2194 853 853 qed. 854 854 855 lemma monotone_sigma: 856 ∀program. \snd program ≤ 2^16 → 857 ∀sigma: Word → Word. ∀policy: Word → bool. 858 sigma_policy_specification program sigma policy → 859 ∀ppc1,ppc2. 860 nat_of_bitvector … ppc2 ≤ \snd program → 861 nat_of_bitvector … ppc1 ≤ nat_of_bitvector … ppc2 → 862 (nat_of_bitvector … (sigma ppc1) ≤ nat_of_bitvector … (sigma ppc2) ∨ 863 sigma ppc2 = zero …). 864 #program #program_bounded #sigma #policy * #SIGMAOK1 #SIGMAOK2 #ppc1 #ppc2 865 #ppc2_ok #LE 866 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc1) 867 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc2) 868 lapply (le_n … (nat_of_bitvector … ppc2)) 869 elim LE in ⊢ (?%? → %); 870 [ #_ % % 871  #m #LE_ppc1_m #IH #BOUNDED 872 cases (IH ?) 873 [3: @(transitive_le … BOUNDED) %2 % 874 2: #eq_zero %2 cases daemon (*CSC: True from spec *) ] 875 IH #IH 876 cut (m < \snd program) [ @(lt_to_le_to_lt … ppc2_ok) assumption ] #LT1 877 cut (m < 2^16) [ @(lt_to_le_to_lt … program_bounded) assumption ] #LT2 878 cases (SIGMAOK2 (bitvector_of_nat … m) ?) SIGMAOK2 879 [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption ] 880 #H * 881 [ #LTsigma_m %1 @(transitive_le … IH) IH 882 <add_bitvector_of_nat_Sm >add_commutative >H H 883 >nat_of_bitvector_add 884 [ // 885  >nat_of_bitvector_bitvector_of_nat_inverse try assumption lapply LTsigma_m 886 whd in match instruction_size; normalize nodelta 887 inversion (assembly_1_pseudoinstruction ??????) #len #assembled #EQ #X 888 @(transitive_le … X) @le_S_S // 889 ] 890  * #EQ1 #EQ2 %2 891 <add_bitvector_of_nat_Sm >add_commutative >H 892 lapply (eq_f … (bitvector_of_nat 16) … EQ2) 893 <add_bitvector_of_nat_plus 894 >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero 895 ]] 896 qed. 897 855 898 definition assembly: 856 899 ∀p: pseudo_assembly_program. … … 937 980 [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2)  skip] 938 981 #abs2 change with (0 = S ?) in abs2; destruct(abs2) ] 939  *#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_code982  #sigma_pol_ok cases sigma_pol_ok #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 940 983 #IH cases (IH ? instr_list_ok) [2: % assumption ] IH 941 984 * * #IH1 #IH2 #IH3 #IH4 … … 1008 1051 >nat_of_bitvector_add >nat_of_bitvector_bitvector_of_nat_inverse // ]] 1009 1052  #ppc' #LTppc' cases hd in prf p2 EQpc_delta2 eq_fetch_pseudo_instruction; #label #pi #prf #p2 1010 #EQpc_delta2 #eq_fetch_pseudo_instruction #OR_lt_eq 1011 cut (ppc' = ppc ∨ ppc' ≠ ppc) [cases daemon (*CSC: True*)] * 1053 #EQpc_delta2 #eq_fetch_pseudo_instruction #OR_lt_eq @(eq_bv_elim … ppc' ppc) 1012 1054 [ #EQppc' >EQppc' in LTppc'; ppc' >prf 1013 1055 >IH1 #LTppc lapply LTppc … … 1072 1114  #j #LTj >reverse_append >reverse_reverse #K 1073 1115 >IH 1074 [2: >length_reverse (*CSC: ?????????? <IH3 (*CSC: USE MONOTONICITY *)*) cases daemon 1075  @shift_nth_prefix ]]]]] 1116 [ @shift_nth_prefix 1117  >length_reverse 1118 @(lt_to_le_to_lt … 1119 (nat_of_bitvector … (add … (sigma ppc') (bitvector_of_nat … (assembledi'))))) 1120 [ @lt_to_lt_nat_of_bitvector_add try assumption 1121 [ cases daemon (*CSC: True*) 1122  cases daemon (*CSC: True*) 1123 ] 1124  cases IH3 IH3 1125 [ #eq_code <eq_code 1126 @(transitive_le … (nat_of_bitvector … (sigma (add … ppc' (bitvector_of_nat … 1))))) 1127 [ cases daemon (*CSC: True*) 1128  cases (monotone_sigma … sigma_pol_ok … (add … ppc' (bitvector_of_nat … 1)) ppc ??) 1129 try assumption 1130 [ #X @X 1131  cases daemon (*CSC: False, sigma ppc = zero! *) 1132  @(transitive_le … ppc_ok) %2 % 1133  cases daemon (*CSC: True*) 1134 ]] 1135  * * #_ #relevant #_ >relevant 1136 @(transitive_le … (S ?) … (lt_nat_of_bitvector …)) [%2 %  skip]]] 1137 ]]]]] 1076 1138 qed. 1077 1139 
src/ASM/AssemblyProof.ma
r2160 r2194 179 179  _ ⇒ True 180 180 ]. 181 182 lemma monotone_sigma:183 ∀program. \snd program ≤ 2^16 →184 ∀sigma: Word → Word. ∀policy: Word → bool.185 sigma_policy_specification program sigma policy →186 ∀ppc1,ppc2.187 nat_of_bitvector … ppc2 ≤ \snd program →188 nat_of_bitvector … ppc1 ≤ nat_of_bitvector … ppc2 →189 (nat_of_bitvector … (sigma ppc1) ≤ nat_of_bitvector … (sigma ppc2) ∨190 sigma ppc2 = zero … ∧ nat_of_bitvector … ppc2 = \snd program).191 #program #program_bounded #sigma #policy * #SIGMAOK1 #SIGMAOK2 #ppc1 #ppc2192 #ppc2_ok #LE193 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc1)194 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc2) in ⊢ (?%(?%?));195 lapply (le_n … (nat_of_bitvector … ppc2))196 elim LE in ⊢ (?%? → %);197 [ #_ % %198  #m #LE_ppc1_m #IH #BOUNDED199 cases (IH ?)200 [3: @(transitive_le … BOUNDED) %2 %201 2: * #_ #abs @⊥ <abs in ppc2_ok; #abs'202 @(absurd ?? (not_le_Sn_n m))203 @(transitive_le … BOUNDED abs') ]204 IH #IH205 cut (m < \snd program) [ @(lt_to_le_to_lt … ppc2_ok) assumption ] #LT1206 cut (m < 2^16) [ @(lt_to_le_to_lt … program_bounded) assumption ] #LT2207 cases (SIGMAOK2 (bitvector_of_nat … m) ?) SIGMAOK2208 [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption ]209 #H *210 [ #LTsigma_m %1 @(transitive_le … IH) IH211 <add_bitvector_of_nat_Sm >add_commutative >H H212 >nat_of_bitvector_add213 [ //214  >nat_of_bitvector_bitvector_of_nat_inverse try assumption lapply LTsigma_m215 whd in match instruction_size; normalize nodelta216 inversion (assembly_1_pseudoinstruction ??????) #len #assembled #EQ #X217 @(transitive_le … X) @le_S_S //218 ]219  * #EQ1 #EQ2 %2 %220 [ <add_bitvector_of_nat_Sm >add_commutative >H221 lapply (eq_f … (bitvector_of_nat 16) … EQ2)222 <add_bitvector_of_nat_plus223 >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero224  <(nat_of_bitvector_bitvector_of_nat_inverse 16 m) try assumption225 ]]]226 qed.227 181 228 182 (* This is a non trivial consequence of fetch_assembly_pseudo +
Note: See TracChangeset
for help on using the changeset viewer.