creusot-std: Add specs for Wrapping arithmetic operators

[MavenRain]

Closes #1923.

std::num::Wrapping<T> is the transparent integer newtype whose arithmetic
operators wrap around on overflow . . . Wrapping(a) + Wrapping(b) == Wrapping(a.wrapping_add(b)),
and likewise for -, * and unary -. It had no specs, so verified code could not reason through it.

This adds, in creusot-std/src/std/num.rs:

• DeepModel for Wrapping<T>, modelled on the existing Reverse<T>
  instance in cmp.rs:

  impl<T: DeepModel> DeepModel for Wrapping<T> {
      type DeepModelTy = Wrapping<T::DeepModelTy>;
      #[logic(open, inline)]
      fn deep_model(self) -> Self::DeepModelTy {
          pearlite! { Wrapping(self.0.deep_model()) }
      }
  }

• extern_spec! specs for Add, Sub, Mul and Neg, generated per
  integer type (u8…isize) by a small spec_wrapping! macro. Each spec relates
  the wrapped field of the result to the wrapping operation on the operands:

  impl core::ops::Add<Wrapping<$t>> for Wrapping<$t> {
      #[ensures(result.0 == self.0 + rhs.0)]
      fn add(self, rhs: Wrapping<$t>) -> Wrapping<$t> {
          Wrapping(self.0.wrapping_add(rhs.0))
      }
  }

  This mirrors how the existing primitive-integer specs are written: on a machine
  integer, +/-/*/unary - already denote the wrapping (builtin) operations,
  so wrapping_add is specced as result == self + rhs and wrapping_neg as
  result == -self. The Wrapping operator specs reuse exactly that, and the
  reference bodies match the std impls.

Scope

Kept intentionally to the wrapping arithmetic operators the issue calls out. Natural
follow-ups, deferred to keep this reviewable: the assigning operators
(AddAssign, …), Div/Rem (which carry a non-zero-divisor precondition), and
the bitwise/shift operators. I'd be happy to add these in a follow-up (or here) if you'd
prefer.

Verification

• creusot-std translates cleanly with the new specs (./t ui creusot-std), and
  tests/creusot-std/creusot-std.coma is regenerated. The delta is exactly 48 new
  _body modules — Add/Sub/Mul/Neg × the 12 integer types, plus reordering;
  nothing is removed.
• Every one of those 48 obligations discharges. Proving them with Z3 (from the
  regenerated coma) reports Valid for all of them, e.g.
  vc_extern_spec_core_ops_Add_Wrapping_u32_Wrapping_u32_add_body … Valid. The proof
  is the trivial rewrite: the reference body Wrapping(self.0.wrapping_add(rhs.0))
  gives result.0 == self.0.wrapping_add(rhs.0), and wrapping_add's own spec is
  result == self + rhs.
• why3session.xml still needs regenerating for the new goals (I verified they
  prove, but haven't committed the session — a from-scratch regen rewrites the whole
  session with fresh prover times, and my local run also tripped an unrelated,
  pre-existing goal on a macOS alt-ergo/cvc4 quirk). I'd be happy to regenerate it however
  you prefer, or leave it to the standard ./testsuite_regenerate run.

Note

Drafted with AI assistance; the specs and the Z3 checks above were reviewed and run by me.

[Lysxia]

Can you remove this?

[Lysxia]

While you're at it, can you add extern specs for the impls with reference types? Add<&Wrapping<u8>> for &Wrapping<u8> etc.

To update the why3session.xml file, ./ide tests/creusot-std/creusot-std.coma, click on creusot-std.coma, then press 4 (or menu Tools > Strategies > Creusot Auto) and save (Ctrl+S).

And for the doc failure, this is going to be addressed by #2197

[Lysxia]

We can get rid of this and the other comments. They don't say anything informative.

[jhjourdan]

Thanks!

Could you indeed add instances for AddAssign and friends, Div/Mod and bitwise operations? Instances for reference types would be great too.