Add specs for digit_unchecked + comments

Author: nilehmann

library/core/src/ascii/ascii_char.rs

@@ -479,6 +479,7 @@ impl AsciiChar {
     /// `b` must be in `0..=127`, or else this is UB.
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[inline]
+    #[cfg_attr(flux, flux::spec(fn(b: u8{b <= 127}) -> Self))]
     #[requires(b <= 127)]
     #[ensures(|result| *result as u8 == b)]
     pub const unsafe fn from_u8_unchecked(b: u8) -> Self {
@@ -516,6 +517,7 @@ impl AsciiChar {
     /// when writing code using this method, since the implementation doesn't
     /// need something really specific, not to make those other arguments do
     /// something useful. It might be tightened before stabilization.)
+    #[cfg_attr(flux, flux::spec(fn(d: u8{d < 10}) -> Self))]
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[inline]
     #[track_caller]

library/core/src/num/uint_macros.rs

@@ -581,6 +581,7 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline(always)]
         #[track_caller]
+        #[cfg_attr(flux, flux::spec(fn(self: Self, rhs: Self{self + rhs <= $MaxV}) -> Self[self + rhs]))]
         #[requires(!self.overflowing_add(rhs).1)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(

library/core/src/pat.rs

@@ -13,6 +13,18 @@ macro_rules! pattern_type {
     };
 }
 
+// The Flux spec for the `trait RangePattern` below uses
+// [associated refinements](https://flux-rs.github.io/flux/tutorial/08-traits.html)
+// The `sub_one` method may only be safe for certain values,
+// e.g. when the value is not the "minimum of the type" as in the
+// case of the `char` implementation below. To specify this precondition generically
+// 1. at the trait level, we introduce the predicate `sub_ok`
+//    which characterizes the "valid" values at which `sub_one`
+//    can be safely called, and by default, specify this predicate
+//    is "true";
+// 2. at the impl level, we can provide a type-specific implementation
+//    of `sub_ok` that permits the verification of the impl for that type.
+
 /// A trait implemented for integer types and `char`.
 /// Useful in the future for generic pattern types, but
 /// used right now to simplify ast lowering of pattern type ranges.
@@ -63,13 +75,16 @@ impl_range_pat! {
     u8, u16, u32, u64, u128, usize,
 }
 
+// The "associated refinement" `sub_ok` is defined as `non-zero` for `char`, to let Flux
+// verify that the `self as u32 -1` in the impl does not underflow.
 #[cfg_attr(flux, flux::assoc(fn sub_ok(self: char) -> bool { 0 < char_to_int(self)}))]
 #[rustc_const_unstable(feature = "pattern_type_range_trait", issue = "123646")]
 impl const RangePattern for char {
     const MIN: Self = char::MIN;
 
     const MAX: Self = char::MAX;
 
+
     #[cfg_attr(flux, flux::spec(fn (self: char{<char as RangePattern>::sub_ok(self)}) -> char))]
     fn sub_one(self) -> Self {
         match char::from_u32(self as u32 - 1) {