Claim #1 — Verification of <T as num_conv::Widen>::widen (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
impl<T: sealed::Integer> num_conv::Widen for T
pub fn widen<U>(self: Self) -> U where T: WidenTarget<U>Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a
Preconditions
true
Formal statement
NumConvProof.widen_all_spec
then(∀ (x : Aeneas.Std.U8),
∃ out, num_conv_verification_api.widen_u8_u8 x = Aeneas.Std.Result.ok out ∧ NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U8),
∃ out,
num_conv_verification_api.widen_u8_u16 x = Aeneas.Std.Result.ok out ∧ NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U8),
∃ out,
num_conv_verification_api.widen_u8_u32 x = Aeneas.Std.Result.ok out ∧ NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U8),
∃ out,
num_conv_verification_api.widen_u8_u64 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U8),
∃ out,
num_conv_verification_api.widen_u8_u128 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U8),
∃ out,
num_conv_verification_api.widen_u8_usize x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U16),
∃ out,
num_conv_verification_api.widen_u16_u16 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U16),
∃ out,
num_conv_verification_api.widen_u16_u32 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U16),
∃ out,
num_conv_verification_api.widen_u16_u64 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U16),
∃ out,
num_conv_verification_api.widen_u16_u128 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U16),
∃ out,
num_conv_verification_api.widen_u16_usize x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U32),
∃ out,
num_conv_verification_api.widen_u32_u32 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U32),
∃ out,
num_conv_verification_api.widen_u32_u64 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U32),
∃ out,
num_conv_verification_api.widen_u32_u128 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.widen_u64_u64 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.widen_u64_u128 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.widen_u128_u128 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.Usize),
∃ out,
num_conv_verification_api.widen_usize_usize x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.I8),
∃ out,
num_conv_verification_api.widen_i8_i8 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I8),
∃ out,
num_conv_verification_api.widen_i8_i16 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I8),
∃ out,
num_conv_verification_api.widen_i8_i32 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I8),
∃ out,
num_conv_verification_api.widen_i8_i64 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I8),
∃ out,
num_conv_verification_api.widen_i8_i128 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I8),
∃ out,
num_conv_verification_api.widen_i8_isize x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I16),
∃ out,
num_conv_verification_api.widen_i16_i16 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I16),
∃ out,
num_conv_verification_api.widen_i16_i32 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I16),
∃ out,
num_conv_verification_api.widen_i16_i64 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I16),
∃ out,
num_conv_verification_api.widen_i16_i128 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I16),
∃ out,
num_conv_verification_api.widen_i16_isize x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I32),
∃ out,
num_conv_verification_api.widen_i32_i32 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I32),
∃ out,
num_conv_verification_api.widen_i32_i64 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I32),
∃ out,
num_conv_verification_api.widen_i32_i128 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.widen_i64_i64 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.widen_i64_i128 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.widen_i128_i128 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out) ∧
∀ (x : Aeneas.Std.Isize),
∃ out,
num_conv_verification_api.widen_isize_isize
x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.preservesValue ↑x ↑out
Complete Lean proposition
And
(∀ (x : Aeneas.Std.U8),
@Exists.{1} Aeneas.Std.U8 fun (out : Aeneas.Std.U8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U8) (num_conv_verification_api.widen_u8_u8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U8 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 x))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 out))))
(And
(∀ (x : Aeneas.Std.U8),
@Exists.{1} Aeneas.Std.U16 fun (out : Aeneas.Std.U16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U16) (num_conv_verification_api.widen_u8_u16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U16 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 x))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 out))))
(And
(∀ (x : Aeneas.Std.U8),
@Exists.{1} Aeneas.Std.U32 fun (out : Aeneas.Std.U32) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U32) (num_conv_verification_api.widen_u8_u32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U32 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 x))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 out))))
(And
(∀ (x : Aeneas.Std.U8),
@Exists.{1} Aeneas.Std.U64 fun (out : Aeneas.Std.U64) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U64) (num_conv_verification_api.widen_u8_u64 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U64 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 x))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 out))))
(And
(∀ (x : Aeneas.Std.U8),
@Exists.{1} Aeneas.Std.U128 fun (out : Aeneas.Std.U128) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U128) (num_conv_verification_api.widen_u8_u128 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U128 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 x))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U128 out))))
(And
(∀ (x : Aeneas.Std.U8),
@Exists.{1} Aeneas.Std.Usize fun (out : Aeneas.Std.Usize) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.Usize) (num_conv_verification_api.widen_u8_usize x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.Usize out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 x))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize out))))
(And
(∀ (x : Aeneas.Std.U16),
@Exists.{1} Aeneas.Std.U16 fun (out : Aeneas.Std.U16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U16) (num_conv_verification_api.widen_u16_u16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U16 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 x))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 out))))
(And
(∀ (x : Aeneas.Std.U16),
@Exists.{1} Aeneas.Std.U32 fun (out : Aeneas.Std.U32) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U32) (num_conv_verification_api.widen_u16_u32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U32 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 x))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 out))))
(And
(∀ (x : Aeneas.Std.U16),
@Exists.{1} Aeneas.Std.U64 fun (out : Aeneas.Std.U64) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U64) (num_conv_verification_api.widen_u16_u64 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U64 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 x))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 out))))
(And
(∀ (x : Aeneas.Std.U16),
@Exists.{1} Aeneas.Std.U128 fun (out : Aeneas.Std.U128) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U128) (num_conv_verification_api.widen_u16_u128 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U128 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 x))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U128 out))))
(And
(∀ (x : Aeneas.Std.U16),
@Exists.{1} Aeneas.Std.Usize fun (out : Aeneas.Std.Usize) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.Usize)
(num_conv_verification_api.widen_u16_usize x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.Usize out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 x))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize out))))
(And
(∀ (x : Aeneas.Std.U32),
@Exists.{1} Aeneas.Std.U32 fun (out : Aeneas.Std.U32) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U32)
(num_conv_verification_api.widen_u32_u32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U32 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 x))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 out))))
(And
(∀ (x : Aeneas.Std.U32),
@Exists.{1} Aeneas.Std.U64 fun (out : Aeneas.Std.U64) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U64)
(num_conv_verification_api.widen_u32_u64 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U64 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 x))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 out))))
(And
(∀ (x : Aeneas.Std.U32),
@Exists.{1} Aeneas.Std.U128 fun (out : Aeneas.Std.U128) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U128)
(num_conv_verification_api.widen_u32_u128 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U128 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 x))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U128 out))))
(And
(∀ (x : Aeneas.Std.U64),
@Exists.{1} Aeneas.Std.U64 fun (out : Aeneas.Std.U64) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U64)
(num_conv_verification_api.widen_u64_u64 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U64 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 x))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 out))))
(And
(∀ (x : Aeneas.Std.U64),
@Exists.{1} Aeneas.Std.U128 fun (out : Aeneas.Std.U128) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U128)
(num_conv_verification_api.widen_u64_u128 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U128 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 x))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U128 out))))
(And
(∀ (x : Aeneas.Std.U128),
@Exists.{1} Aeneas.Std.U128 fun (out : Aeneas.Std.U128) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U128)
(num_conv_verification_api.widen_u128_u128 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U128 out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U128 x))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U128 out))))
(And
(∀ (x : Aeneas.Std.Usize),
@Exists.{1} Aeneas.Std.Usize fun (out : Aeneas.Std.Usize) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.Usize)
(num_conv_verification_api.widen_usize_usize x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.Usize out))
(NumConvSpec.preservesValue
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize x))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize out))))
(And
(∀ (x : Aeneas.Std.I8),
@Exists.{1} Aeneas.Std.I8 fun (out : Aeneas.Std.I8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I8)
(num_conv_verification_api.widen_i8_i8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I8 out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 x)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 out)))
(And
(∀ (x : Aeneas.Std.I8),
@Exists.{1} Aeneas.Std.I16 fun (out : Aeneas.Std.I16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I16)
(num_conv_verification_api.widen_i8_i16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I16 out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 x)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 out)))
(And
(∀ (x : Aeneas.Std.I8),
@Exists.{1} Aeneas.Std.I32 fun (out : Aeneas.Std.I32) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I32)
(num_conv_verification_api.widen_i8_i32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I32 out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 x)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I32 out)))
(And
(∀ (x : Aeneas.Std.I8),
@Exists.{1} Aeneas.Std.I64 fun (out : Aeneas.Std.I64) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I64)
(num_conv_verification_api.widen_i8_i64 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I64 out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 x)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I64 out)))
(And
(∀ (x : Aeneas.Std.I8),
@Exists.{1} Aeneas.Std.I128 fun (out : Aeneas.Std.I128) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I128)
(num_conv_verification_api.widen_i8_i128 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I128 out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 x)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I128 out)))
(And
(∀ (x : Aeneas.Std.I8),
@Exists.{1} Aeneas.Std.Isize fun (out : Aeneas.Std.Isize) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.Isize)
(num_conv_verification_api.widen_i8_isize x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.Isize out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 x)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.Isize out)))
(And
(∀ (x : Aeneas.Std.I16),
@Exists.{1} Aeneas.Std.I16 fun (out : Aeneas.Std.I16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I16)
(num_conv_verification_api.widen_i16_i16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I16 out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 x)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 out)))
(And
(∀ (x : Aeneas.Std.I16),
@Exists.{1} Aeneas.Std.I32 fun (out : Aeneas.Std.I32) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I32)
(num_conv_verification_api.widen_i16_i32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I32 out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 x)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I32 out)))
(And
(∀ (x : Aeneas.Std.I16),
@Exists.{1} Aeneas.Std.I64 fun (out : Aeneas.Std.I64) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I64)
(num_conv_verification_api.widen_i16_i64 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I64 out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 x)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I64 out)))
(And
(∀ (x : Aeneas.Std.I16),
@Exists.{1} Aeneas.Std.I128 fun (out : Aeneas.Std.I128) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I128)
(num_conv_verification_api.widen_i16_i128 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I128 out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 x)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I128
out)))
(And
(∀ (x : Aeneas.Std.I16),
@Exists.{1} Aeneas.Std.Isize fun (out : Aeneas.Std.Isize) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.Isize)
(num_conv_verification_api.widen_i16_isize x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.Isize out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 x)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.Isize
out)))
(And
(∀ (x : Aeneas.Std.I32),
@Exists.{1} Aeneas.Std.I32 fun (out : Aeneas.Std.I32) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I32)
(num_conv_verification_api.widen_i32_i32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I32 out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I32 x)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I32
out)))
(And
(∀ (x : Aeneas.Std.I32),
@Exists.{1} Aeneas.Std.I64 fun (out : Aeneas.Std.I64) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I64)
(num_conv_verification_api.widen_i32_i64 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I64 out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I32
x)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I64
out)))
(And
(∀ (x : Aeneas.Std.I32),
@Exists.{1} Aeneas.Std.I128
fun (out : Aeneas.Std.I128) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I128)
(num_conv_verification_api.widen_i32_i128 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I128 out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I32 x)
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I128 out)))
(And
(∀ (x : Aeneas.Std.I64),
@Exists.{1} Aeneas.Std.I64
fun (out : Aeneas.Std.I64) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I64)
(num_conv_verification_api.widen_i64_i64 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I64
out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I64 x)
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I64 out)))
(And
(∀ (x : Aeneas.Std.I64),
@Exists.{1} Aeneas.Std.I128
fun (out : Aeneas.Std.I128) =>
And
(@Eq.{1}
(Aeneas.Std.Result.{0} Aeneas.Std.I128)
(num_conv_verification_api.widen_i64_i128 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I128
out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I64 x)
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I128 out)))
(And
(∀ (x : Aeneas.Std.I128),
@Exists.{1} Aeneas.Std.I128
fun (out : Aeneas.Std.I128) =>
And
(@Eq.{1}
(Aeneas.Std.Result.{0} Aeneas.Std.I128)
(num_conv_verification_api.widen_i128_i128
x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I128
out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I128 x)
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I128 out)))
(∀ (x : Aeneas.Std.Isize),
@Exists.{1} Aeneas.Std.Isize
fun (out : Aeneas.Std.Isize) =>
And
(@Eq.{1}
(Aeneas.Std.Result.{0} Aeneas.Std.Isize)
(num_conv_verification_api.widen_isize_isize
x)
(@Aeneas.Std.Result.ok.{0}
Aeneas.Std.Isize out))
(NumConvSpec.preservesValue
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.Isize x)
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.Isize
out)))))))))))))))))))))))))))))))))))))Theorem source at recorded commit · Recorded check
Referenced definitions (up to 100 direct references)
And· Init.PreludeAeneas.Std.U8· Aeneas.Std.Scalar.CoreExists· Init.CoreEq· Init.PreludeAeneas.Std.Result· Aeneas.Std.Primitivesnum_conv_verification_api.widen_u8_u8Aeneas.Std.Result.ok· Aeneas.Std.PrimitivesNumConvSpec.preservesValueNat.cast· Init.Data.CastInt· Init.Data.Int.BasicinstNatCastInt· Init.Data.Int.BasicAeneas.Std.UScalar.val· Aeneas.Std.Scalar.CoreAeneas.Std.UScalarTy.U8· Aeneas.Std.Scalar.CoreAeneas.Std.U16· Aeneas.Std.Scalar.Corenum_conv_verification_api.widen_u8_u16Aeneas.Std.UScalarTy.U16· Aeneas.Std.Scalar.CoreAeneas.Std.U32· Aeneas.Std.Scalar.Corenum_conv_verification_api.widen_u8_u32Aeneas.Std.UScalarTy.U32· Aeneas.Std.Scalar.CoreAeneas.Std.U64· Aeneas.Std.Scalar.Corenum_conv_verification_api.widen_u8_u64Aeneas.Std.UScalarTy.U64· Aeneas.Std.Scalar.CoreAeneas.Std.U128· Aeneas.Std.Scalar.Corenum_conv_verification_api.widen_u8_u128Aeneas.Std.UScalarTy.U128· Aeneas.Std.Scalar.CoreAeneas.Std.Usize· Aeneas.Std.Scalar.Corenum_conv_verification_api.widen_u8_usizeAeneas.Std.UScalarTy.Usize· Aeneas.Std.Scalar.Corenum_conv_verification_api.widen_u16_u16num_conv_verification_api.widen_u16_u32num_conv_verification_api.widen_u16_u64num_conv_verification_api.widen_u16_u128num_conv_verification_api.widen_u16_usizenum_conv_verification_api.widen_u32_u32num_conv_verification_api.widen_u32_u64num_conv_verification_api.widen_u32_u128num_conv_verification_api.widen_u64_u64num_conv_verification_api.widen_u64_u128num_conv_verification_api.widen_u128_u128num_conv_verification_api.widen_usize_usizeAeneas.Std.I8· Aeneas.Std.Scalar.Corenum_conv_verification_api.widen_i8_i8Aeneas.Std.IScalar.val· Aeneas.Std.Scalar.CoreAeneas.Std.IScalarTy.I8· Aeneas.Std.Scalar.CoreAeneas.Std.I16· Aeneas.Std.Scalar.Corenum_conv_verification_api.widen_i8_i16Aeneas.Std.IScalarTy.I16· Aeneas.Std.Scalar.CoreAeneas.Std.I32· Aeneas.Std.Scalar.Corenum_conv_verification_api.widen_i8_i32Aeneas.Std.IScalarTy.I32· Aeneas.Std.Scalar.CoreAeneas.Std.I64· Aeneas.Std.Scalar.Corenum_conv_verification_api.widen_i8_i64Aeneas.Std.IScalarTy.I64· Aeneas.Std.Scalar.CoreAeneas.Std.I128· Aeneas.Std.Scalar.Corenum_conv_verification_api.widen_i8_i128Aeneas.Std.IScalarTy.I128· Aeneas.Std.Scalar.CoreAeneas.Std.Isize· Aeneas.Std.Scalar.Corenum_conv_verification_api.widen_i8_isizeAeneas.Std.IScalarTy.Isize· Aeneas.Std.Scalar.Corenum_conv_verification_api.widen_i16_i16num_conv_verification_api.widen_i16_i32num_conv_verification_api.widen_i16_i64num_conv_verification_api.widen_i16_i128num_conv_verification_api.widen_i16_isizenum_conv_verification_api.widen_i32_i32num_conv_verification_api.widen_i32_i64num_conv_verification_api.widen_i32_i128num_conv_verification_api.widen_i64_i64num_conv_verification_api.widen_i64_i128num_conv_verification_api.widen_i128_i128num_conv_verification_api.widen_isize_isize
Evidence
What is trusted
From the report
The argument depends on the Aeneas/Charon translation and its integer, cast and
execution models corresponding to Rust, and on Lean and its kernel. The harness
loads the unchanged release source as a module and invokes its public methods;
correspondence with the ordinarily linked release is not separately proved.
Technical limitations
From the report
The extraction target is aarch64-apple-darwin; this result does not establish
behavior on another
pointer width or target. Native tests are separate from the formal contracts.
Tool limitations
Lean backend only, requiring cargo-proofs 0.4.0 or later. The version identifies the official Aeneas Git revision pinned in lake-manifest.json (backends/lean); this revision uses Lean 4.35.0. The recorder checks committed Lean theorem declarations and permits only propext, Classical.choice, and Quot.sound as transitive axioms. It rejects sorryAx and custom axioms, including axiomatized external models. Charon/Aeneas extraction is not rerun. The author must review that the committed functional model matches the recorded Rust source, that the named theorem corresponds to the public API, and that the reported precondition matches the theorem. A checked theorem alone does not establish those links or the adequacy of the specification. The current adapter records the default Cargo configuration, with ordinary Lean module paths and a pinned official Git dependency. Other backends, custom Lake source directories, and local-path Aeneas dependencies are unsupported. See https://proofs.rs/book/aeneas.html and https://github.com/AeneasVerif/aeneas/tree/be86ab0f1989d04944292b345b24c435be3ad10a.
Aeneas be86ab0f1989d04944292b345b24c435be3ad10a — version details