Add specs for digit_unchecked + comments

Author: nilehmann

.github/workflows/flux.yml

@@ -9,7 +9,7 @@ on:
 
 env:
   FIXPOINT_VERSION: "556104ba5508891c357b0bdf819ce706e93d9349"
-  FLUX_VERSION: "347252ab34de1594a7531d9bdc4477369623ead3"
+  FLUX_VERSION: "bfecf2ae0d181993c4e07f3233f7e04c5ed5ad1a"
 
 jobs:
   check-flux-on-core:

library/core/src/ascii/ascii_char.rs

@@ -471,6 +471,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 {
@@ -508,6 +509,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

@@ -582,6 +582,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) {