Module ops

Module ops 

Source

Traits§

AddSpec
AddSpecImpl
BitAndSpec
BitAndSpecImpl
BitOrSpec
BitOrSpecImpl
BitXorSpec
BitXorSpecImpl
DivSpec
DivSpecImpl
ExAdd
ExBitAnd
ExBitOr
ExBitXor
ExDiv
ExMul
ExNeg
ExNot
ExRem
ExShl
ExShr
ExSub
MulSpec
MulSpecImpl
NegSpec
NegSpecImpl
NotSpec
NotSpecImpl
RemSpec
RemSpecImpl
ShlSpec
ShlSpecImpl
ShrSpec
ShrSpecImpl
SubSpec
SubSpecImpl

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