 Timestamp:
 Jul 17, 2012, 5:40:00 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2197 r2199 851 851  #dptr #id normalize in ⊢ (?%?); // 852 852 ] 853 qed.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 #ppc2865 #ppc2_ok #LE866 <(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 #BOUNDED872 cases (IH ?)873 [3: @(transitive_le … BOUNDED) %2 %874 2: #eq_zero %2 cases daemon (*CSC: True from spec *) ]875 IH #IH876 cut (m < \snd program) [ @(lt_to_le_to_lt … ppc2_ok) assumption ] #LT1877 cut (m < 2^16) [ @(lt_to_le_to_lt … program_bounded) assumption ] #LT2878 cases (SIGMAOK2 (bitvector_of_nat … m) ?) SIGMAOK2879 [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption ]880 #H *881 [ #LTsigma_m %1 @(transitive_le … IH) IH882 <add_bitvector_of_nat_Sm >add_commutative >H H883 >nat_of_bitvector_add884 [ //885  >nat_of_bitvector_bitvector_of_nat_inverse try assumption lapply LTsigma_m886 whd in match instruction_size; normalize nodelta887 inversion (assembly_1_pseudoinstruction ??????) #len #assembled #EQ #X888 @(transitive_le … X) @le_S_S //889 ]890  * #EQ1 #EQ2 %2891 <add_bitvector_of_nat_Sm >add_commutative >H892 lapply (eq_f … (bitvector_of_nat 16) … EQ2)893 <add_bitvector_of_nat_plus894 >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero895 ]]896 853 qed. 897 854
Note: See TracChangeset
for help on using the changeset viewer.