@@ -43,6 +43,9 @@ impl Alignment {
4343 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
4444 #[ inline]
4545 #[ must_use]
46+ #[ rustc_allow_const_fn_unstable( contracts) ]
47+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
48+ |result: & Alignment | result. as_usize( ) . is_power_of_two( ) ) ) ]
4649 pub const fn of < T > ( ) -> Self {
4750 // This can't actually panic since type alignment is always a power of two.
4851 const { Alignment :: new ( align_of :: < T > ( ) ) . unwrap ( ) }
@@ -54,6 +57,11 @@ impl Alignment {
5457 /// Note that `0` is not a power of two, nor a valid alignment.
5558 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
5659 #[ inline]
60+ #[ rustc_allow_const_fn_unstable( contracts) ]
61+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
62+ move
63+ |result: & Option <Alignment >| align. is_power_of_two( ) == result. is_some( ) &&
64+ ( result. is_none( ) || result. unwrap( ) . as_usize( ) == align) ) ) ]
5765 pub const fn new ( align : usize ) -> Option < Self > {
5866 if align. is_power_of_two ( ) {
5967 // SAFETY: Just checked it only has one bit set
@@ -73,6 +81,12 @@ impl Alignment {
7381 /// It must *not* be zero.
7482 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
7583 #[ inline]
84+ #[ cfg_attr( not( bootstrap) , rustc_const_unstable( feature = "contracts" , issue = "128044" ) ) ]
85+ #[ cfg_attr( not( bootstrap) , core:: contracts:: requires( align. is_power_of_two( ) ) ) ]
86+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
87+ move
88+ |result: & Alignment | result. as_usize( ) == align &&
89+ result. as_usize( ) . is_power_of_two( ) ) ) ]
7690 pub const unsafe fn new_unchecked ( align : usize ) -> Self {
7791 assert_unsafe_precondition ! (
7892 check_language_ub,
@@ -88,13 +102,21 @@ impl Alignment {
88102 /// Returns the alignment as a [`usize`].
89103 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
90104 #[ inline]
105+ #[ rustc_allow_const_fn_unstable( contracts) ]
106+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
107+ |result: & usize | result. is_power_of_two( ) ) ) ]
91108 pub const fn as_usize ( self ) -> usize {
92109 self . 0 as usize
93110 }
94111
95112 /// Returns the alignment as a <code>[NonZero]<[usize]></code>.
96113 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
97114 #[ inline]
115+ #[ rustc_allow_const_fn_unstable( contracts) ]
116+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
117+ move
118+ |result: & NonZero <usize >| result. get( ) . is_power_of_two( ) &&
119+ result. get( ) == self . as_usize( ) ) ) ]
98120 pub const fn as_nonzero ( self ) -> NonZero < usize > {
99121 // This transmutes directly to avoid the UbCheck in `NonZero::new_unchecked`
100122 // since there's no way for the user to trip that check anyway -- the
@@ -120,6 +142,12 @@ impl Alignment {
120142 /// ```
121143 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
122144 #[ inline]
145+ #[ cfg_attr( not( bootstrap) , rustc_const_unstable( feature = "contracts" , issue = "128044" ) ) ]
146+ #[ cfg_attr( not( bootstrap) , core:: contracts:: requires( self . as_usize( ) . is_power_of_two( ) ) ) ]
147+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
148+ move
149+ |result: & u32 | * result < usize :: BITS &&
150+ ( 1usize << * result) == self . as_usize( ) ) ) ]
123151 pub const fn log2 ( self ) -> u32 {
124152 self . as_nonzero ( ) . trailing_zeros ( )
125153 }
@@ -149,6 +177,12 @@ impl Alignment {
149177 /// ```
150178 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
151179 #[ inline]
180+ #[ cfg_attr( not( bootstrap) , rustc_const_unstable( feature = "contracts" , issue = "128044" ) ) ]
181+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
182+ move
183+ |result: & usize | * result > 0 &&
184+ * result == !( self . as_usize( ) -1 ) &&
185+ self . as_usize( ) & * result == self . as_usize( ) ) ) ]
152186 pub const fn mask ( self ) -> usize {
153187 // SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
154188 !( unsafe { self . as_usize ( ) . unchecked_sub ( 1 ) } )
0 commit comments