Claim #4 — Verification of <T as num_conv::Truncate>::saturating_truncate (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
<T as num_conv::Truncate>::saturating_truncate
impl<T: sealed::Integer> num_conv::Truncate for T
pub fn saturating_truncate<U>(self: Self) -> U where T: TruncateTarget<U>Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a
Preconditions
true
Formal statement
NumConvProof.saturating_truncate_all_spec
then(∀ (x : Aeneas.Std.U8),
∃ out,
num_conv_verification_api.saturating_truncate_u8_u8 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 8) ↑↑x) ∧
(∀ (x : Aeneas.Std.U16),
∃ out,
num_conv_verification_api.saturating_truncate_u16_u8 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 8) ↑↑x) ∧
(∀ (x : Aeneas.Std.U32),
∃ out,
num_conv_verification_api.saturating_truncate_u32_u8 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 8) ↑↑x) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.saturating_truncate_u64_u8 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 8) ↑↑x) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.saturating_truncate_u128_u8 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 8) ↑↑x) ∧
(∀ (x : Aeneas.Std.Usize),
∃ out,
num_conv_verification_api.saturating_truncate_usize_u8 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 8) ↑↑x) ∧
(∀ (x : Aeneas.Std.U16),
∃ out,
num_conv_verification_api.saturating_truncate_u16_u16 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 16) ↑↑x) ∧
(∀ (x : Aeneas.Std.U32),
∃ out,
num_conv_verification_api.saturating_truncate_u32_u16 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 16) ↑↑x) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.saturating_truncate_u64_u16 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 16) ↑↑x) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.saturating_truncate_u128_u16 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 16) ↑↑x) ∧
(∀ (x : Aeneas.Std.Usize),
∃ out,
num_conv_verification_api.saturating_truncate_usize_u16 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 16) ↑↑x) ∧
(∀ (x : Aeneas.Std.U32),
∃ out,
num_conv_verification_api.saturating_truncate_u32_u32 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 32) ↑↑x) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.saturating_truncate_u64_u32 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 32) ↑↑x) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.saturating_truncate_u128_u32 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 32) ↑↑x) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.saturating_truncate_u64_u64 x = Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 64) ↑↑x) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.saturating_truncate_u128_u64 x =
Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 64) ↑↑x) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.saturating_truncate_u128_u128 x =
Aeneas.Std.Result.ok out ∧
↑↑out = NumConvSpec.saturate 0 (NumConvSpec.unsignedMax 128) ↑↑x) ∧
(∀ (x : Aeneas.Std.Usize),
∃ out,
num_conv_verification_api.saturating_truncate_usize_usize x =
Aeneas.Std.Result.ok out ∧
↑↑out =
NumConvSpec.saturate 0
(NumConvSpec.unsignedMax Aeneas.Std.UScalarTy.Usize.numBits) ↑↑x) ∧
(∀ (x : Aeneas.Std.I8),
∃ out,
num_conv_verification_api.saturating_truncate_i8_i8 x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 8) (NumConvSpec.signedMax 8)
↑x) ∧
(∀ (x : Aeneas.Std.I16),
∃ out,
num_conv_verification_api.saturating_truncate_i16_i8 x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 8) (NumConvSpec.signedMax 8)
↑x) ∧
(∀ (x : Aeneas.Std.I32),
∃ out,
num_conv_verification_api.saturating_truncate_i32_i8 x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.saturating_truncate_i64_i8 x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.saturating_truncate_i128_i8 x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x) ∧
(∀ (x : Aeneas.Std.Isize),
∃ out,
num_conv_verification_api.saturating_truncate_isize_i8 x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x) ∧
(∀ (x : Aeneas.Std.I16),
∃ out,
num_conv_verification_api.saturating_truncate_i16_i16 x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x) ∧
(∀ (x : Aeneas.Std.I32),
∃ out,
num_conv_verification_api.saturating_truncate_i32_i16 x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.saturating_truncate_i64_i16 x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.saturating_truncate_i128_i16 x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x) ∧
(∀ (x : Aeneas.Std.Isize),
∃ out,
num_conv_verification_api.saturating_truncate_isize_i16
x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x) ∧
(∀ (x : Aeneas.Std.I32),
∃ out,
num_conv_verification_api.saturating_truncate_i32_i32
x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 32)
(NumConvSpec.signedMax 32) ↑x) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.saturating_truncate_i64_i32
x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 32)
(NumConvSpec.signedMax 32) ↑x) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.saturating_truncate_i128_i32
x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate (NumConvSpec.signedMin 32)
(NumConvSpec.signedMax 32) ↑x) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.saturating_truncate_i64_i64
x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate
(NumConvSpec.signedMin 64)
(NumConvSpec.signedMax 64) ↑x) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.saturating_truncate_i128_i64
x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate
(NumConvSpec.signedMin 64)
(NumConvSpec.signedMax 64) ↑x) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.saturating_truncate_i128_i128
x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate
(NumConvSpec.signedMin 128)
(NumConvSpec.signedMax 128) ↑x) ∧
∀ (x : Aeneas.Std.Isize),
∃ out,
num_conv_verification_api.saturating_truncate_isize_isize
x =
Aeneas.Std.Result.ok out ∧
↑out =
NumConvSpec.saturate
(NumConvSpec.signedMin
Aeneas.Std.IScalarTy.Isize.numBits)
(NumConvSpec.signedMax
Aeneas.Std.IScalarTy.Isize.numBits)
↑x
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.saturating_truncate_u8_u8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U8 out))
(@Eq.{1} Int (@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax (@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 x)))))
(And
(∀ (x : Aeneas.Std.U16),
@Exists.{1} Aeneas.Std.U8 fun (out : Aeneas.Std.U8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U8) (num_conv_verification_api.saturating_truncate_u16_u8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U8 out))
(@Eq.{1} Int (@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax (@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 x)))))
(And
(∀ (x : Aeneas.Std.U32),
@Exists.{1} Aeneas.Std.U8 fun (out : Aeneas.Std.U8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U8) (num_conv_verification_api.saturating_truncate_u32_u8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U8 out))
(@Eq.{1} Int (@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax (@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 x)))))
(And
(∀ (x : Aeneas.Std.U64),
@Exists.{1} Aeneas.Std.U8 fun (out : Aeneas.Std.U8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U8) (num_conv_verification_api.saturating_truncate_u64_u8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U8 out))
(@Eq.{1} Int (@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax (@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 x)))))
(And
(∀ (x : Aeneas.Std.U128),
@Exists.{1} Aeneas.Std.U8 fun (out : Aeneas.Std.U8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U8) (num_conv_verification_api.saturating_truncate_u128_u8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U8 out))
(@Eq.{1} Int (@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax (@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U128 x)))))
(And
(∀ (x : Aeneas.Std.Usize),
@Exists.{1} Aeneas.Std.U8 fun (out : Aeneas.Std.U8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U8)
(num_conv_verification_api.saturating_truncate_usize_u8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U8 out))
(@Eq.{1} Int (@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax (@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize x)))))
(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.saturating_truncate_u16_u16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U16 out))
(@Eq.{1} Int
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16))))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 x)))))
(And
(∀ (x : Aeneas.Std.U32),
@Exists.{1} Aeneas.Std.U16 fun (out : Aeneas.Std.U16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U16)
(num_conv_verification_api.saturating_truncate_u32_u16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U16 out))
(@Eq.{1} Int
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16))))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 x)))))
(And
(∀ (x : Aeneas.Std.U64),
@Exists.{1} Aeneas.Std.U16 fun (out : Aeneas.Std.U16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U16)
(num_conv_verification_api.saturating_truncate_u64_u16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U16 out))
(@Eq.{1} Int
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16))))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 x)))))
(And
(∀ (x : Aeneas.Std.U128),
@Exists.{1} Aeneas.Std.U16 fun (out : Aeneas.Std.U16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U16)
(num_conv_verification_api.saturating_truncate_u128_u16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U16 out))
(@Eq.{1} Int
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16))))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U128 x)))))
(And
(∀ (x : Aeneas.Std.Usize),
@Exists.{1} Aeneas.Std.U16 fun (out : Aeneas.Std.U16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U16)
(num_conv_verification_api.saturating_truncate_usize_u16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U16 out))
(@Eq.{1} Int
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax
(@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16))))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize x)))))
(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.saturating_truncate_u32_u32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U32 out))
(@Eq.{1} Int
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax
(@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32))))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 x)))))
(And
(∀ (x : Aeneas.Std.U64),
@Exists.{1} Aeneas.Std.U32 fun (out : Aeneas.Std.U32) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U32)
(num_conv_verification_api.saturating_truncate_u64_u32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U32 out))
(@Eq.{1} Int
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax
(@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32))))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 x)))))
(And
(∀ (x : Aeneas.Std.U128),
@Exists.{1} Aeneas.Std.U32 fun (out : Aeneas.Std.U32) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U32)
(num_conv_verification_api.saturating_truncate_u128_u32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U32 out))
(@Eq.{1} Int
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax
(@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32))))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U128 x)))))
(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.saturating_truncate_u64_u64 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U64 out))
(@Eq.{1} Int
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 out))
(NumConvSpec.saturate (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax
(@OfNat.ofNat.{0} Nat (nat_lit 64) (instOfNatNat (nat_lit 64))))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 x)))))
(And
(∀ (x : Aeneas.Std.U128),
@Exists.{1} Aeneas.Std.U64 fun (out : Aeneas.Std.U64) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U64)
(num_conv_verification_api.saturating_truncate_u128_u64 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U64 out))
(@Eq.{1} Int
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 out))
(NumConvSpec.saturate
(@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax
(@OfNat.ofNat.{0} Nat (nat_lit 64) (instOfNatNat (nat_lit 64))))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U128 x)))))
(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.saturating_truncate_u128_u128 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U128 out))
(@Eq.{1} Int
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U128 out))
(NumConvSpec.saturate
(@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax
(@OfNat.ofNat.{0} Nat (nat_lit 128) (instOfNatNat (nat_lit 128))))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U128 x)))))
(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.saturating_truncate_usize_usize x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.Usize out))
(@Eq.{1} Int
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize out))
(NumConvSpec.saturate
(@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))
(NumConvSpec.unsignedMax
(Aeneas.Std.UScalarTy.numBits Aeneas.Std.UScalarTy.Usize))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize x)))))
(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.saturating_truncate_i8_i8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I8 out))
(@Eq.{1} Int (@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 x))))
(And
(∀ (x : Aeneas.Std.I16),
@Exists.{1} Aeneas.Std.I8 fun (out : Aeneas.Std.I8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I8)
(num_conv_verification_api.saturating_truncate_i16_i8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I8 out))
(@Eq.{1} Int (@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 x))))
(And
(∀ (x : Aeneas.Std.I32),
@Exists.{1} Aeneas.Std.I8 fun (out : Aeneas.Std.I8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I8)
(num_conv_verification_api.saturating_truncate_i32_i8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I8 out))
(@Eq.{1} Int (@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I32 x))))
(And
(∀ (x : Aeneas.Std.I64),
@Exists.{1} Aeneas.Std.I8 fun (out : Aeneas.Std.I8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I8)
(num_conv_verification_api.saturating_truncate_i64_i8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I8 out))
(@Eq.{1} Int (@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I64 x))))
(And
(∀ (x : Aeneas.Std.I128),
@Exists.{1} Aeneas.Std.I8 fun (out : Aeneas.Std.I8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I8)
(num_conv_verification_api.saturating_truncate_i128_i8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I8 out))
(@Eq.{1} Int (@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8))))
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I128 x))))
(And
(∀ (x : Aeneas.Std.Isize),
@Exists.{1} Aeneas.Std.I8 fun (out : Aeneas.Std.I8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I8)
(num_conv_verification_api.saturating_truncate_isize_i8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I8 out))
(@Eq.{1} Int (@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 8)
(instOfNatNat (nat_lit 8))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 8)
(instOfNatNat (nat_lit 8))))
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.Isize x))))
(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.saturating_truncate_i16_i16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I16 out))
(@Eq.{1} Int
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16))))
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 x))))
(And
(∀ (x : Aeneas.Std.I32),
@Exists.{1} Aeneas.Std.I16 fun (out : Aeneas.Std.I16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I16)
(num_conv_verification_api.saturating_truncate_i32_i16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I16 out))
(@Eq.{1} Int
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16))))
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I32 x))))
(And
(∀ (x : Aeneas.Std.I64),
@Exists.{1} Aeneas.Std.I16 fun (out : Aeneas.Std.I16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I16)
(num_conv_verification_api.saturating_truncate_i64_i16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I16 out))
(@Eq.{1} Int
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16))))
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I64 x))))
(And
(∀ (x : Aeneas.Std.I128),
@Exists.{1} Aeneas.Std.I16 fun (out : Aeneas.Std.I16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I16)
(num_conv_verification_api.saturating_truncate_i128_i16
x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I16 out))
(@Eq.{1} Int
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16))))
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I128
x))))
(And
(∀ (x : Aeneas.Std.Isize),
@Exists.{1} Aeneas.Std.I16 fun (out : Aeneas.Std.I16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I16)
(num_conv_verification_api.saturating_truncate_isize_i16
x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I16 out))
(@Eq.{1} Int
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16))))
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.Isize
x))))
(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.saturating_truncate_i32_i32
x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I32 out))
(@Eq.{1} Int
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I32
out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 32)
(instOfNatNat (nat_lit 32))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 32)
(instOfNatNat (nat_lit 32))))
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I32
x))))
(And
(∀ (x : Aeneas.Std.I64),
@Exists.{1} Aeneas.Std.I32 fun (out : Aeneas.Std.I32) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I32)
(num_conv_verification_api.saturating_truncate_i64_i32
x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I32 out))
(@Eq.{1} Int
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I32
out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 32)
(instOfNatNat (nat_lit 32))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 32)
(instOfNatNat (nat_lit 32))))
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I64 x))))
(And
(∀ (x : Aeneas.Std.I128),
@Exists.{1} Aeneas.Std.I32
fun (out : Aeneas.Std.I32) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.I32)
(num_conv_verification_api.saturating_truncate_i128_i32
x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I32 out))
(@Eq.{1} Int
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I32 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 32)
(instOfNatNat (nat_lit 32))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 32)
(instOfNatNat (nat_lit 32))))
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I128 x))))
(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.saturating_truncate_i64_i64
x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I64
out))
(@Eq.{1} Int
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I64 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 64)
(instOfNatNat (nat_lit 64))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 64)
(instOfNatNat (nat_lit 64))))
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I64 x))))
(And
(∀ (x : Aeneas.Std.I128),
@Exists.{1} Aeneas.Std.I64
fun (out : Aeneas.Std.I64) =>
And
(@Eq.{1}
(Aeneas.Std.Result.{0} Aeneas.Std.I64)
(num_conv_verification_api.saturating_truncate_i128_i64
x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I64
out))
(@Eq.{1} Int
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I64 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 64)
(instOfNatNat (nat_lit 64))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 64)
(instOfNatNat (nat_lit 64))))
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I128 x))))
(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.saturating_truncate_i128_i128
x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I128
out))
(@Eq.{1} Int
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I128 out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(@OfNat.ofNat.{0} Nat (nat_lit 128)
(instOfNatNat (nat_lit 128))))
(NumConvSpec.signedMax
(@OfNat.ofNat.{0} Nat (nat_lit 128)
(instOfNatNat (nat_lit 128))))
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I128 x))))
(∀ (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.saturating_truncate_isize_isize
x)
(@Aeneas.Std.Result.ok.{0}
Aeneas.Std.Isize out))
(@Eq.{1} Int
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.Isize out)
(NumConvSpec.saturate
(NumConvSpec.signedMin
(Aeneas.Std.IScalarTy.numBits
Aeneas.Std.IScalarTy.Isize))
(NumConvSpec.signedMax
(Aeneas.Std.IScalarTy.numBits
Aeneas.Std.IScalarTy.Isize))
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.Isize
x))))))))))))))))))))))))))))))))))))))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.saturating_truncate_u8_u8Aeneas.Std.Result.ok· Aeneas.Std.PrimitivesInt· Init.Data.Int.BasicNat.cast· Init.Data.CastinstNatCastInt· Init.Data.Int.BasicAeneas.Std.UScalar.val· Aeneas.Std.Scalar.CoreAeneas.Std.UScalarTy.U8· Aeneas.Std.Scalar.CoreNumConvSpec.saturateOfNat.ofNat· Init.PreludeinstOfNat· Init.Data.Int.BasicNumConvSpec.unsignedMaxNat· Init.PreludeinstOfNatNat· Init.PreludeAeneas.Std.U16· Aeneas.Std.Scalar.Corenum_conv_verification_api.saturating_truncate_u16_u8Aeneas.Std.UScalarTy.U16· Aeneas.Std.Scalar.CoreAeneas.Std.U32· Aeneas.Std.Scalar.Corenum_conv_verification_api.saturating_truncate_u32_u8Aeneas.Std.UScalarTy.U32· Aeneas.Std.Scalar.CoreAeneas.Std.U64· Aeneas.Std.Scalar.Corenum_conv_verification_api.saturating_truncate_u64_u8Aeneas.Std.UScalarTy.U64· Aeneas.Std.Scalar.CoreAeneas.Std.U128· Aeneas.Std.Scalar.Corenum_conv_verification_api.saturating_truncate_u128_u8Aeneas.Std.UScalarTy.U128· Aeneas.Std.Scalar.CoreAeneas.Std.Usize· Aeneas.Std.Scalar.Corenum_conv_verification_api.saturating_truncate_usize_u8Aeneas.Std.UScalarTy.Usize· Aeneas.Std.Scalar.Corenum_conv_verification_api.saturating_truncate_u16_u16num_conv_verification_api.saturating_truncate_u32_u16num_conv_verification_api.saturating_truncate_u64_u16num_conv_verification_api.saturating_truncate_u128_u16num_conv_verification_api.saturating_truncate_usize_u16num_conv_verification_api.saturating_truncate_u32_u32num_conv_verification_api.saturating_truncate_u64_u32num_conv_verification_api.saturating_truncate_u128_u32num_conv_verification_api.saturating_truncate_u64_u64num_conv_verification_api.saturating_truncate_u128_u64num_conv_verification_api.saturating_truncate_u128_u128num_conv_verification_api.saturating_truncate_usize_usizeAeneas.Std.UScalarTy.numBits· Aeneas.Std.Scalar.CoreAeneas.Std.I8· Aeneas.Std.Scalar.Corenum_conv_verification_api.saturating_truncate_i8_i8Aeneas.Std.IScalar.val· Aeneas.Std.Scalar.CoreAeneas.Std.IScalarTy.I8· Aeneas.Std.Scalar.CoreNumConvSpec.signedMinNumConvSpec.signedMaxAeneas.Std.I16· Aeneas.Std.Scalar.Corenum_conv_verification_api.saturating_truncate_i16_i8Aeneas.Std.IScalarTy.I16· Aeneas.Std.Scalar.CoreAeneas.Std.I32· Aeneas.Std.Scalar.Corenum_conv_verification_api.saturating_truncate_i32_i8Aeneas.Std.IScalarTy.I32· Aeneas.Std.Scalar.CoreAeneas.Std.I64· Aeneas.Std.Scalar.Corenum_conv_verification_api.saturating_truncate_i64_i8Aeneas.Std.IScalarTy.I64· Aeneas.Std.Scalar.CoreAeneas.Std.I128· Aeneas.Std.Scalar.Corenum_conv_verification_api.saturating_truncate_i128_i8Aeneas.Std.IScalarTy.I128· Aeneas.Std.Scalar.CoreAeneas.Std.Isize· Aeneas.Std.Scalar.Corenum_conv_verification_api.saturating_truncate_isize_i8Aeneas.Std.IScalarTy.Isize· Aeneas.Std.Scalar.Corenum_conv_verification_api.saturating_truncate_i16_i16num_conv_verification_api.saturating_truncate_i32_i16num_conv_verification_api.saturating_truncate_i64_i16num_conv_verification_api.saturating_truncate_i128_i16num_conv_verification_api.saturating_truncate_isize_i16num_conv_verification_api.saturating_truncate_i32_i32num_conv_verification_api.saturating_truncate_i64_i32num_conv_verification_api.saturating_truncate_i128_i32num_conv_verification_api.saturating_truncate_i64_i64num_conv_verification_api.saturating_truncate_i128_i64num_conv_verification_api.saturating_truncate_i128_i128num_conv_verification_api.saturating_truncate_isize_isizeAeneas.Std.IScalarTy.numBits· Aeneas.Std.Scalar.Core
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