Traits§
- AddSpec
- AddSpec
Impl - BitAnd
Spec - BitAnd
Spec Impl - BitOr
Spec - BitOr
Spec Impl - BitXor
Spec - BitXor
Spec Impl - DivSpec
- DivSpec
Impl - ExAdd
- ExBit
And - ExBitOr
- ExBit
Xor - ExDiv
- ExMul
- ExNeg
- ExNot
- ExRem
- ExShl
- ExShr
- ExSub
- MulSpec
- MulSpec
Impl - NegSpec
- NegSpec
Impl - NotSpec
- NotSpec
Impl - RemSpec
- RemSpec
Impl - ShlSpec
- ShlSpec
Impl - ShrSpec
- ShrSpec
Impl - SubSpec
- SubSpec
Impl
Functions§
- _verus_
external_ ⚠fn_ specification_ 414__ 60__ 32_ f32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 415__ 60__ 32_ f32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 416__ 60__ 32_ f32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 417__ 60__ 32_ f32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 418__ 60__ 32_ f32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 419__ 60__ 32_ f64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 420__ 60__ 32_ f64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 421__ 60__ 32_ f64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 422__ 60__ 32_ f64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 423__ 60__ 32_ f64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 424__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 425__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 426__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 427__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 428__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 429__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 430__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 431__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 432__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 433__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 434__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 435__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shr_ 32__ 62__ 32__ 58__ 58__ 32_ shr - _verus_
external_ ⚠fn_ specification_ 436__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 437__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 438__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 439__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 440__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 441__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 442__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 443__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 444__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 445__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 446__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 447__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Shl_ 32__ 62__ 32__ 58__ 58__ 32_ shl - _verus_
external_ ⚠fn_ specification_ 448__ 60__ 32_ bool_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 449__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 450__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 451__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 452__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 453__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 454__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 455__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 456__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 457__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 458__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 459__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 460__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitXor_ 32__ 62__ 32__ 58__ 58__ 32_ bitxor - _verus_
external_ ⚠fn_ specification_ 461__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 462__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 463__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 464__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 465__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 466__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 467__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 468__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 469__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 470__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 471__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 472__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitOr_ 32__ 62__ 32__ 58__ 58__ 32_ bitor - _verus_
external_ ⚠fn_ specification_ 473__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 474__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 475__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 476__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 477__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 478__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 479__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 480__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 481__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 482__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 483__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 484__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ BitAnd_ 32__ 62__ 32__ 58__ 58__ 32_ bitand - _verus_
external_ ⚠fn_ specification_ 485__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 486__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 487__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 488__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 489__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 490__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 491__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 492__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 493__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 494__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 495__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 496__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Rem_ 32__ 62__ 32__ 58__ 58__ 32_ rem - _verus_
external_ ⚠fn_ specification_ 497__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 498__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 499__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 500__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 501__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 502__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 503__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 504__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 505__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 506__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 507__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 508__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Div_ 32__ 62__ 32__ 58__ 58__ 32_ div - _verus_
external_ ⚠fn_ specification_ 509__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 510__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 511__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 512__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 513__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 514__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 515__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 516__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 517__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 518__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 519__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 520__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Mul_ 32__ 62__ 32__ 58__ 58__ 32_ mul - _verus_
external_ ⚠fn_ specification_ 521__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 522__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 523__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 524__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 525__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 526__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 527__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 528__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 529__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 530__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 531__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 532__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Sub_ 32__ 62__ 32__ 58__ 58__ 32_ sub - _verus_
external_ ⚠fn_ specification_ 533__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 534__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 535__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 536__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 537__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 538__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 539__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 540__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 541__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 542__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 543__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 544__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Add_ 32__ 62__ 32__ 58__ 58__ 32_ add - _verus_
external_ ⚠fn_ specification_ 545__ 60__ 32_ bool_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 546__ 60__ 32_ usize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 547__ 60__ 32_ u8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 548__ 60__ 32_ u16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 549__ 60__ 32_ u32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 550__ 60__ 32_ u64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 551__ 60__ 32_ u128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 552__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 553__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 554__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 555__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 556__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 557__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Not_ 32__ 62__ 32__ 58__ 58__ 32_ not - _verus_
external_ ⚠fn_ specification_ 558__ 60__ 32_ isize_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 559__ 60__ 32_ i8_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 560__ 60__ 32_ i16_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 561__ 60__ 32_ i32_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 562__ 60__ 32_ i64_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - _verus_
external_ ⚠fn_ specification_ 563__ 60__ 32_ i128_ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ ops_ 32__ 58__ 58__ 32_ Neg_ 32__ 62__ 32__ 58__ 58__ 32_ neg - add_
ensures - div_
ensures - mul_
ensures - neg_
ensures - sub_
ensures