Changeset 2194 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jul 17, 2012, 10:18:01 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.