@@ -45,6 +45,8 @@ impl Alignment {
4545 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
4646 #[ inline]
4747 #[ must_use]
48+ #[ rustc_allow_const_fn_unstable( contracts) ]
49+ #[ core:: contracts:: ensures( |result: & Alignment | result. as_usize( ) . is_power_of_two( ) ) ]
4850 pub const fn of < T > ( ) -> Self {
4951 // This can't actually panic since type alignment is always a power of two.
5052 const { Alignment :: new ( align_of :: < T > ( ) ) . unwrap ( ) }
@@ -56,6 +58,11 @@ impl Alignment {
5658 /// Note that `0` is not a power of two, nor a valid alignment.
5759 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
5860 #[ inline]
61+ #[ rustc_allow_const_fn_unstable( contracts) ]
62+ #[ core:: contracts:: ensures(
63+ move |result: & Option <Alignment >|
64+ align. is_power_of_two( ) == result. is_some( ) &&
65+ ( result. is_none( ) || result. unwrap( ) . as_usize( ) == align) ) ]
5966 pub const fn new ( align : usize ) -> Option < Self > {
6067 if align. is_power_of_two ( ) {
6168 // SAFETY: Just checked it only has one bit set
@@ -76,6 +83,11 @@ impl Alignment {
7683 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
7784 #[ inline]
7885 #[ track_caller]
86+ #[ rustc_allow_const_fn_unstable( contracts) ]
87+ #[ core:: contracts:: requires( align. is_power_of_two( ) ) ]
88+ #[ core:: contracts:: ensures(
89+ move |result: & Alignment |
90+ result. as_usize( ) == align && result. as_usize( ) . is_power_of_two( ) ) ]
7991 pub const unsafe fn new_unchecked ( align : usize ) -> Self {
8092 assert_unsafe_precondition ! (
8193 check_language_ub,
@@ -91,13 +103,19 @@ impl Alignment {
91103 /// Returns the alignment as a [`usize`].
92104 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
93105 #[ inline]
106+ #[ rustc_allow_const_fn_unstable( contracts) ]
107+ #[ core:: contracts:: ensures( |result: & usize | result. is_power_of_two( ) ) ]
94108 pub const fn as_usize ( self ) -> usize {
95109 self . 0 as usize
96110 }
97111
98112 /// Returns the alignment as a <code>[NonZero]<[usize]></code>.
99113 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
100114 #[ inline]
115+ #[ rustc_allow_const_fn_unstable( contracts) ]
116+ #[ core:: contracts:: ensures(
117+ move |result: & NonZero <usize >|
118+ result. get( ) . is_power_of_two( ) && result. get( ) == self . as_usize( ) ) ]
101119 pub const fn as_nonzero ( self ) -> NonZero < usize > {
102120 // This transmutes directly to avoid the UbCheck in `NonZero::new_unchecked`
103121 // since there's no way for the user to trip that check anyway -- the
@@ -123,6 +141,11 @@ impl Alignment {
123141 /// ```
124142 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
125143 #[ inline]
144+ #[ rustc_const_unstable( feature = "contracts" , issue = "128044" ) ]
145+ #[ core:: contracts:: requires( self . as_usize( ) . is_power_of_two( ) ) ]
146+ #[ core:: contracts:: ensures(
147+ move |result: & u32 |
148+ * result < usize :: BITS && ( 1usize << * result) == self . as_usize( ) ) ]
126149 pub const fn log2 ( self ) -> u32 {
127150 self . as_nonzero ( ) . trailing_zeros ( )
128151 }
@@ -152,6 +175,11 @@ impl Alignment {
152175 /// ```
153176 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
154177 #[ inline]
178+ #[ rustc_const_unstable( feature = "contracts" , issue = "128044" ) ]
179+ #[ core:: contracts:: ensures(
180+ move |result: & usize |
181+ * result > 0 && * result == !( self . as_usize( ) -1 ) &&
182+ self . as_usize( ) & * result == self . as_usize( ) ) ]
155183 pub const fn mask ( self ) -> usize {
156184 // SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
157185 !( unsafe { self . as_usize ( ) . unchecked_sub ( 1 ) } )
0 commit comments