Claim #3 — Verification of <T as num_conv::Truncate>::truncate (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
<T as num_conv::Truncate>::truncate
impl<T: sealed::Integer> num_conv::Truncate for T
pub fn truncate<U>(self: Self) -> U where T: TruncateTarget<U>Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a
Preconditions
true
Formal statement
NumConvProof.truncate_all_spec
then(∀ (x : Aeneas.Std.U8),
∃ out,
num_conv_verification_api.truncate_u8_u8 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 8 0 (NumConvSpec.unsignedMax 8) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U16),
∃ out,
num_conv_verification_api.truncate_u16_u8 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 8 0 (NumConvSpec.unsignedMax 8) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U32),
∃ out,
num_conv_verification_api.truncate_u32_u8 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 8 0 (NumConvSpec.unsignedMax 8) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.truncate_u64_u8 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 8 0 (NumConvSpec.unsignedMax 8) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.truncate_u128_u8 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 8 0 (NumConvSpec.unsignedMax 8) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.Usize),
∃ out,
num_conv_verification_api.truncate_usize_u8 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 8 0 (NumConvSpec.unsignedMax 8) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U16),
∃ out,
num_conv_verification_api.truncate_u16_u16 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 16 0 (NumConvSpec.unsignedMax 16) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U32),
∃ out,
num_conv_verification_api.truncate_u32_u16 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 16 0 (NumConvSpec.unsignedMax 16) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.truncate_u64_u16 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 16 0 (NumConvSpec.unsignedMax 16) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.truncate_u128_u16 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 16 0 (NumConvSpec.unsignedMax 16) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.Usize),
∃ out,
num_conv_verification_api.truncate_usize_u16 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 16 0 (NumConvSpec.unsignedMax 16) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U32),
∃ out,
num_conv_verification_api.truncate_u32_u32 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 32 0 (NumConvSpec.unsignedMax 32) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.truncate_u64_u32 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 32 0 (NumConvSpec.unsignedMax 32) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.truncate_u128_u32 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 32 0 (NumConvSpec.unsignedMax 32) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.truncate_u64_u64 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 64 0 (NumConvSpec.unsignedMax 64) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.truncate_u128_u64 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 64 0 (NumConvSpec.unsignedMax 64) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.truncate_u128_u128 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 128 0 (NumConvSpec.unsignedMax 128) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.Usize),
∃ out,
num_conv_verification_api.truncate_usize_usize x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent Aeneas.Std.UScalarTy.Usize.numBits 0
(NumConvSpec.unsignedMax Aeneas.Std.UScalarTy.Usize.numBits) ↑↑x ↑↑out) ∧
(∀ (x : Aeneas.Std.I8),
∃ out,
num_conv_verification_api.truncate_i8_i8 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 8 (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I16),
∃ out,
num_conv_verification_api.truncate_i16_i8 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 8 (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I32),
∃ out,
num_conv_verification_api.truncate_i32_i8 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 8 (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.truncate_i64_i8 x = Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 8 (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.truncate_i128_i8 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 8 (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.Isize),
∃ out,
num_conv_verification_api.truncate_isize_i8 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 8 (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I16),
∃ out,
num_conv_verification_api.truncate_i16_i16 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 16 (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I32),
∃ out,
num_conv_verification_api.truncate_i32_i16 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 16 (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.truncate_i64_i16 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 16 (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.truncate_i128_i16 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 16 (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.Isize),
∃ out,
num_conv_verification_api.truncate_isize_i16 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 16
(NumConvSpec.signedMin 16) (NumConvSpec.signedMax 16)
↑x ↑out) ∧
(∀ (x : Aeneas.Std.I32),
∃ out,
num_conv_verification_api.truncate_i32_i32 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 32
(NumConvSpec.signedMin 32)
(NumConvSpec.signedMax 32) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.truncate_i64_i32 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 32
(NumConvSpec.signedMin 32)
(NumConvSpec.signedMax 32) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.truncate_i128_i32 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 32
(NumConvSpec.signedMin 32)
(NumConvSpec.signedMax 32) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.truncate_i64_i64 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 64
(NumConvSpec.signedMin 64)
(NumConvSpec.signedMax 64) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.truncate_i128_i64 x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 64
(NumConvSpec.signedMin 64)
(NumConvSpec.signedMax 64) ↑x ↑out) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.truncate_i128_i128
x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent 128
(NumConvSpec.signedMin 128)
(NumConvSpec.signedMax 128) ↑x ↑out) ∧
∀ (x : Aeneas.Std.Isize),
∃ out,
num_conv_verification_api.truncate_isize_isize
x =
Aeneas.Std.Result.ok out ∧
NumConvSpec.boundedCongruent
Aeneas.Std.IScalarTy.Isize.numBits
(NumConvSpec.signedMin
Aeneas.Std.IScalarTy.Isize.numBits)
(NumConvSpec.signedMax
Aeneas.Std.IScalarTy.Isize.numBits)
↑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.truncate_u8_u8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U8 out))
(NumConvSpec.boundedCongruent (@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))
(@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))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 out))))
(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.truncate_u16_u8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U8 out))
(NumConvSpec.boundedCongruent (@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))
(@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))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 out))))
(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.truncate_u32_u8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U8 out))
(NumConvSpec.boundedCongruent (@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))
(@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))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 out))))
(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.truncate_u64_u8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U8 out))
(NumConvSpec.boundedCongruent (@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))
(@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))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 out))))
(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.truncate_u128_u8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U8 out))
(NumConvSpec.boundedCongruent (@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))
(@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))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 out))))
(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.truncate_usize_u8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U8 out))
(NumConvSpec.boundedCongruent (@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))
(@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))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 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.truncate_u16_u16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U16 out))
(NumConvSpec.boundedCongruent (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
(@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))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 out))))
(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.truncate_u32_u16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U16 out))
(NumConvSpec.boundedCongruent (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
(@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))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 out))))
(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.truncate_u64_u16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U16 out))
(NumConvSpec.boundedCongruent (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
(@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))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 out))))
(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.truncate_u128_u16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U16 out))
(NumConvSpec.boundedCongruent (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
(@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))
(@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 out))))
(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.truncate_usize_u16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U16 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
(@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))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 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.truncate_u32_u32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U32 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32)))
(@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))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 out))))
(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.truncate_u64_u32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U32 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32)))
(@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))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 out))))
(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.truncate_u128_u32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U32 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32)))
(@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))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 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.truncate_u64_u64 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U64 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 64) (instOfNatNat (nat_lit 64)))
(@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))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 out))))
(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.truncate_u128_u64 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U64 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 64) (instOfNatNat (nat_lit 64)))
(@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))
(@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 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.truncate_u128_u128 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.U128 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 128) (instOfNatNat (nat_lit 128)))
(@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))
(@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.truncate_usize_usize x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.Usize out))
(NumConvSpec.boundedCongruent
(Aeneas.Std.UScalarTy.numBits Aeneas.Std.UScalarTy.Usize)
(@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))
(@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.truncate_i8_i8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I8 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))
(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)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 out)))
(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.truncate_i16_i8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I8 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))
(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)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 out)))
(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.truncate_i32_i8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I8 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))
(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)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 out)))
(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.truncate_i64_i8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I8 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))
(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)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 out)))
(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.truncate_i128_i8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I8 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))
(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)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 out)))
(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.truncate_isize_i8 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I8 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 8) (instOfNatNat (nat_lit 8)))
(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)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 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.truncate_i16_i16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I16 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16)))
(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)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 out)))
(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.truncate_i32_i16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I16 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16)))
(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)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 out)))
(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.truncate_i64_i16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I16 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16)))
(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)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 out)))
(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.truncate_i128_i16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I16 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16)))
(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)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 out)))
(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.truncate_isize_i16 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I16 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 16)
(instOfNatNat (nat_lit 16)))
(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)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16
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.truncate_i32_i32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I32 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 32)
(instOfNatNat (nat_lit 32)))
(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)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I32
out)))
(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.truncate_i64_i32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I32 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 32)
(instOfNatNat (nat_lit 32)))
(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)
(@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I32
out)))
(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.truncate_i128_i32 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I32 out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 32)
(instOfNatNat (nat_lit 32)))
(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)
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I32 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.truncate_i64_i64 x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I64
out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 64)
(instOfNatNat (nat_lit 64)))
(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)
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I64 out)))
(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.truncate_i128_i64
x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I64
out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 64)
(instOfNatNat (nat_lit 64)))
(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)
(@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I64 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.truncate_i128_i128
x)
(@Aeneas.Std.Result.ok.{0} Aeneas.Std.I128
out))
(NumConvSpec.boundedCongruent
(@OfNat.ofNat.{0} Nat (nat_lit 128)
(instOfNatNat (nat_lit 128)))
(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)
(@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.truncate_isize_isize
x)
(@Aeneas.Std.Result.ok.{0}
Aeneas.Std.Isize out))
(NumConvSpec.boundedCongruent
(Aeneas.Std.IScalarTy.numBits
Aeneas.Std.IScalarTy.Isize)
(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)
(@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.truncate_u8_u8Aeneas.Std.Result.ok· Aeneas.Std.PrimitivesNumConvSpec.boundedCongruentOfNat.ofNat· Init.PreludeNat· Init.PreludeinstOfNatNat· Init.PreludeInt· Init.Data.Int.BasicinstOfNat· Init.Data.Int.BasicNumConvSpec.unsignedMaxNat.cast· Init.Data.CastinstNatCastInt· 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.truncate_u16_u8Aeneas.Std.UScalarTy.U16· Aeneas.Std.Scalar.CoreAeneas.Std.U32· Aeneas.Std.Scalar.Corenum_conv_verification_api.truncate_u32_u8Aeneas.Std.UScalarTy.U32· Aeneas.Std.Scalar.CoreAeneas.Std.U64· Aeneas.Std.Scalar.Corenum_conv_verification_api.truncate_u64_u8Aeneas.Std.UScalarTy.U64· Aeneas.Std.Scalar.CoreAeneas.Std.U128· Aeneas.Std.Scalar.Corenum_conv_verification_api.truncate_u128_u8Aeneas.Std.UScalarTy.U128· Aeneas.Std.Scalar.CoreAeneas.Std.Usize· Aeneas.Std.Scalar.Corenum_conv_verification_api.truncate_usize_u8Aeneas.Std.UScalarTy.Usize· Aeneas.Std.Scalar.Corenum_conv_verification_api.truncate_u16_u16num_conv_verification_api.truncate_u32_u16num_conv_verification_api.truncate_u64_u16num_conv_verification_api.truncate_u128_u16num_conv_verification_api.truncate_usize_u16num_conv_verification_api.truncate_u32_u32num_conv_verification_api.truncate_u64_u32num_conv_verification_api.truncate_u128_u32num_conv_verification_api.truncate_u64_u64num_conv_verification_api.truncate_u128_u64num_conv_verification_api.truncate_u128_u128num_conv_verification_api.truncate_usize_usizeAeneas.Std.UScalarTy.numBits· Aeneas.Std.Scalar.CoreAeneas.Std.I8· Aeneas.Std.Scalar.Corenum_conv_verification_api.truncate_i8_i8NumConvSpec.signedMinNumConvSpec.signedMaxAeneas.Std.IScalar.val· Aeneas.Std.Scalar.CoreAeneas.Std.IScalarTy.I8· Aeneas.Std.Scalar.CoreAeneas.Std.I16· Aeneas.Std.Scalar.Corenum_conv_verification_api.truncate_i16_i8Aeneas.Std.IScalarTy.I16· Aeneas.Std.Scalar.CoreAeneas.Std.I32· Aeneas.Std.Scalar.Corenum_conv_verification_api.truncate_i32_i8Aeneas.Std.IScalarTy.I32· Aeneas.Std.Scalar.CoreAeneas.Std.I64· Aeneas.Std.Scalar.Corenum_conv_verification_api.truncate_i64_i8Aeneas.Std.IScalarTy.I64· Aeneas.Std.Scalar.CoreAeneas.Std.I128· Aeneas.Std.Scalar.Corenum_conv_verification_api.truncate_i128_i8Aeneas.Std.IScalarTy.I128· Aeneas.Std.Scalar.CoreAeneas.Std.Isize· Aeneas.Std.Scalar.Corenum_conv_verification_api.truncate_isize_i8Aeneas.Std.IScalarTy.Isize· Aeneas.Std.Scalar.Corenum_conv_verification_api.truncate_i16_i16num_conv_verification_api.truncate_i32_i16num_conv_verification_api.truncate_i64_i16num_conv_verification_api.truncate_i128_i16num_conv_verification_api.truncate_isize_i16num_conv_verification_api.truncate_i32_i32num_conv_verification_api.truncate_i64_i32num_conv_verification_api.truncate_i128_i32num_conv_verification_api.truncate_i64_i64num_conv_verification_api.truncate_i128_i64num_conv_verification_api.truncate_i128_i128num_conv_verification_api.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