 Timestamp:
 Jul 17, 2012, 3:23:51 PM (7 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2194 r2197 917 917 assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in 918 918 assembledi ≤ assembled ∧ 919 ∀j:nat. ∀H: j < assembledi. ∀K.919 ∀j:nat. ∀H: j < assembledi. ∃K. 920 920 nth_safe ? j assembledi H = 921 921 nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j))) … … 951 951 assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in 952 952 assembledi ≤ reverse … code ∧ 953 ∀j:nat. ∀H: j < assembledi. ∀K.953 ∀j:nat. ∀H: j < assembledi. ∃K. 954 954 nth_safe ? j assembledi H = 955 955 nth_safe ? (nat_of_bitvector … (add … (sigma ppc') (bitvector_of_nat ? j))) (reverse … code) K) … … 1071 1071 >reverse_append >reverse_reverse 1072 1072 cases IH3 IH3 1073 [ #IH3 >IH3 <(length_reverse … code) @nth_safe_prepend 1073 [ #IH3 >IH3 <(length_reverse … code) % 1074 [ >length_append @monotonic_lt_plus_r assumption 1075  @nth_safe_prepend ] 1074 1076  * * #IH3a #IH3b #IH3c >IH3a @⊥ 1075 1077 cut (program = 0) … … 1112 1114 >(fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) 1113 1115 @(transitive_le … IH6) // 1114  #j #LTj >reverse_append >reverse_reverse #K 1115 >IH 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 ]]]]] 1116  #j #LTj >reverse_append >reverse_reverse cases (IH … LTj) IH #K #IH % 1117 [ >length_append @(lt_to_le_to_lt … K) // 1118  >IH @shift_nth_prefix ]]]]] 1138 1119 qed. 1139 1120 
src/ASM/AssemblyProof.ma
r2195 r2197 241 241 (nat_of_bitvector … 242 242 (add … (sigma ppc) (bitvector_of_nat … j)))))) 243 [1: #j #H <load_code_memory_ok 244 [ @assembly_ok 245  cut (0=assembled' → False) 246 [ #abs <abs in assembly_ok4; >EQlen #abs' 247 @(absurd ?? (not_le_Sn_O j)) @(transitive_le … H) assumption ] #NOT_EMPTY 248 cases assembly_ok3 assembly_ok3 249 [2: * #_ #EQ2 >EQ2 @lt_nat_of_bitvector ] 250 #EQlen_assembled' <EQlen_assembled' 251 cases sigma_policy_witness #sigma_zero >EQprogram #sigma_ok 252 cases (sigma_ok … ppc_ok) sigma_ok >eq_fetch_pseudo_instruction 253 whd in match instruction_size; normalize nodelta 254 >create_label_cost_refl 255 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels 256 [>eq_assembly_1_pseudoinstruction 2: skip] #OK >OK <EQlen * 257 [2: * #EQ1 #EQ2 258 @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (assembled))))) 259 [1: @lt_to_lt_nat_of_bitvector_add try assumption 260 cases daemon (* XXX: two cases to prove, both true *) 261 2: cases daemon (* XXX: use monotonicity of sigma *) 262 ] 263 ] 264 cases (le_to_or_lt_eq … instr_list_ok) 265 [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero 266 assumption ] 267 #instr_list_ok' #NO_OVERFLOW 268 @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (assembled))))) 269 [ @lt_to_lt_nat_of_bitvector_add 270 [ @(eq_ind ?? (λp.λ_. \snd p < 2^16) ?? eq_assembly_1_pseudoinstruction) 271 / by / 272  <EQlen assumption 273  assumption 274 ] 275  <EQlen <OK 276 cases (monotone_sigma ???? sigma_policy_witness 277 (add … ppc (bitvector_of_nat … 1)) 278 (bitvector_of_nat … (instr_list)) ??) try assumption 279 [ #H @H 280 3: >EQprogram >nat_of_bitvector_bitvector_of_nat_inverse 281 try % assumption 282 4: >nat_of_bitvector_bitvector_of_nat_inverse try assumption 283 >nat_of_bitvector_add <plus_n_Sm <plus_n_O try assumption 284 @(transitive_le … instr_list_ok') @le_S_S assumption 285  #EQ1 @⊥ >EQ1 in EQlen_assembled'; assumption ]]] 243 [1: #j #H cases (assembly_ok … H) #K assembly_ok #assembly_ok <load_code_memory_ok 244 [ @assembly_ok  skip ] 286 245 2: 287 246 assembly_ok load_code_memory_ok generalize in match (sigma ppc); >EQlen len
Note: See TracChangeset
for help on using the changeset viewer.