Claim #5 — Verification of <T as num_conv::Truncate>::checked_truncate (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
<T as num_conv::Truncate>::checked_truncate
impl<T: sealed::Integer> num_conv::Truncate for T
pub fn checked_truncate<U>(self: Self) -> Option<U> where T: TruncateTarget<U>Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a
Preconditions
true
Formal statement
NumConvProof.checked_truncate_all_spec
then(∀ (x : Aeneas.Std.U8),
∃ out,
num_conv_verification_api.checked_truncate_u8_u8 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out = NumConvSpec.checked 0 (NumConvSpec.unsignedMax 8) ↑↑x) ∧
(∀ (x : Aeneas.Std.U16),
∃ out,
num_conv_verification_api.checked_truncate_u16_u8 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out = NumConvSpec.checked 0 (NumConvSpec.unsignedMax 8) ↑↑x) ∧
(∀ (x : Aeneas.Std.U32),
∃ out,
num_conv_verification_api.checked_truncate_u32_u8 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out = NumConvSpec.checked 0 (NumConvSpec.unsignedMax 8) ↑↑x) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.checked_truncate_u64_u8 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out = NumConvSpec.checked 0 (NumConvSpec.unsignedMax 8) ↑↑x) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.checked_truncate_u128_u8 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out = NumConvSpec.checked 0 (NumConvSpec.unsignedMax 8) ↑↑x) ∧
(∀ (x : Aeneas.Std.Usize),
∃ out,
num_conv_verification_api.checked_truncate_usize_u8 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out = NumConvSpec.checked 0 (NumConvSpec.unsignedMax 8) ↑↑x) ∧
(∀ (x : Aeneas.Std.U16),
∃ out,
num_conv_verification_api.checked_truncate_u16_u16 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out = NumConvSpec.checked 0 (NumConvSpec.unsignedMax 16) ↑↑x) ∧
(∀ (x : Aeneas.Std.U32),
∃ out,
num_conv_verification_api.checked_truncate_u32_u16 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out = NumConvSpec.checked 0 (NumConvSpec.unsignedMax 16) ↑↑x) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.checked_truncate_u64_u16 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out = NumConvSpec.checked 0 (NumConvSpec.unsignedMax 16) ↑↑x) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.checked_truncate_u128_u16 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out = NumConvSpec.checked 0 (NumConvSpec.unsignedMax 16) ↑↑x) ∧
(∀ (x : Aeneas.Std.Usize),
∃ out,
num_conv_verification_api.checked_truncate_usize_u16 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out = NumConvSpec.checked 0 (NumConvSpec.unsignedMax 16) ↑↑x) ∧
(∀ (x : Aeneas.Std.U32),
∃ out,
num_conv_verification_api.checked_truncate_u32_u32 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out = NumConvSpec.checked 0 (NumConvSpec.unsignedMax 32) ↑↑x) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.checked_truncate_u64_u32 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out =
NumConvSpec.checked 0 (NumConvSpec.unsignedMax 32) ↑↑x) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.checked_truncate_u128_u32 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out =
NumConvSpec.checked 0 (NumConvSpec.unsignedMax 32) ↑↑x) ∧
(∀ (x : Aeneas.Std.U64),
∃ out,
num_conv_verification_api.checked_truncate_u64_u64 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out =
NumConvSpec.checked 0 (NumConvSpec.unsignedMax 64) ↑↑x) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.checked_truncate_u128_u64 x = Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out =
NumConvSpec.checked 0 (NumConvSpec.unsignedMax 64) ↑↑x) ∧
(∀ (x : Aeneas.Std.U128),
∃ out,
num_conv_verification_api.checked_truncate_u128_u128 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out =
NumConvSpec.checked 0 (NumConvSpec.unsignedMax 128) ↑↑x) ∧
(∀ (x : Aeneas.Std.Usize),
∃ out,
num_conv_verification_api.checked_truncate_usize_usize x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑↑v) out =
NumConvSpec.checked 0
(NumConvSpec.unsignedMax Aeneas.Std.UScalarTy.Usize.numBits) ↑↑x) ∧
(∀ (x : Aeneas.Std.I8),
∃ out,
num_conv_verification_api.checked_truncate_i8_i8 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 8) (NumConvSpec.signedMax 8)
↑x) ∧
(∀ (x : Aeneas.Std.I16),
∃ out,
num_conv_verification_api.checked_truncate_i16_i8 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 8) (NumConvSpec.signedMax 8)
↑x) ∧
(∀ (x : Aeneas.Std.I32),
∃ out,
num_conv_verification_api.checked_truncate_i32_i8 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.checked_truncate_i64_i8 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.checked_truncate_i128_i8 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x) ∧
(∀ (x : Aeneas.Std.Isize),
∃ out,
num_conv_verification_api.checked_truncate_isize_i8 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 8)
(NumConvSpec.signedMax 8) ↑x) ∧
(∀ (x : Aeneas.Std.I16),
∃ out,
num_conv_verification_api.checked_truncate_i16_i16 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x) ∧
(∀ (x : Aeneas.Std.I32),
∃ out,
num_conv_verification_api.checked_truncate_i32_i16 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.checked_truncate_i64_i16 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.checked_truncate_i128_i16 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x) ∧
(∀ (x : Aeneas.Std.Isize),
∃ out,
num_conv_verification_api.checked_truncate_isize_i16 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 16)
(NumConvSpec.signedMax 16) ↑x) ∧
(∀ (x : Aeneas.Std.I32),
∃ out,
num_conv_verification_api.checked_truncate_i32_i32 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 32)
(NumConvSpec.signedMax 32) ↑x) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.checked_truncate_i64_i32 x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 32)
(NumConvSpec.signedMax 32) ↑x) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.checked_truncate_i128_i32
x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 32)
(NumConvSpec.signedMax 32) ↑x) ∧
(∀ (x : Aeneas.Std.I64),
∃ out,
num_conv_verification_api.checked_truncate_i64_i64
x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked (NumConvSpec.signedMin 64)
(NumConvSpec.signedMax 64) ↑x) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.checked_truncate_i128_i64
x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked
(NumConvSpec.signedMin 64)
(NumConvSpec.signedMax 64) ↑x) ∧
(∀ (x : Aeneas.Std.I128),
∃ out,
num_conv_verification_api.checked_truncate_i128_i128
x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked
(NumConvSpec.signedMin 128)
(NumConvSpec.signedMax 128) ↑x) ∧
∀ (x : Aeneas.Std.Isize),
∃ out,
num_conv_verification_api.checked_truncate_isize_isize
x =
Aeneas.Std.Result.ok out ∧
Option.map (fun v => ↑v) out =
NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.U8) fun (out : Option.{0} Aeneas.Std.U8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U8)) (num_conv_verification_api.checked_truncate_u8_u8 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U8) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U8 Int
(fun (v : Aeneas.Std.U8) =>
@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U8) fun (out : Option.{0} Aeneas.Std.U8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U8))
(num_conv_verification_api.checked_truncate_u16_u8 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U8) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U8 Int
(fun (v : Aeneas.Std.U8) =>
@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U8) fun (out : Option.{0} Aeneas.Std.U8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U8))
(num_conv_verification_api.checked_truncate_u32_u8 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U8) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U8 Int
(fun (v : Aeneas.Std.U8) =>
@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U8) fun (out : Option.{0} Aeneas.Std.U8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U8))
(num_conv_verification_api.checked_truncate_u64_u8 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U8) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U8 Int
(fun (v : Aeneas.Std.U8) =>
@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U8) fun (out : Option.{0} Aeneas.Std.U8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U8))
(num_conv_verification_api.checked_truncate_u128_u8 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U8) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U8 Int
(fun (v : Aeneas.Std.U8) =>
@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U8) fun (out : Option.{0} Aeneas.Std.U8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U8))
(num_conv_verification_api.checked_truncate_usize_u8 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U8) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U8 Int
(fun (v : Aeneas.Std.U8) =>
@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U16) fun (out : Option.{0} Aeneas.Std.U16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U16))
(num_conv_verification_api.checked_truncate_u16_u16 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U16) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U16 Int
(fun (v : Aeneas.Std.U16) =>
@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U16) fun (out : Option.{0} Aeneas.Std.U16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U16))
(num_conv_verification_api.checked_truncate_u32_u16 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U16) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U16 Int
(fun (v : Aeneas.Std.U16) =>
@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U16) fun (out : Option.{0} Aeneas.Std.U16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U16))
(num_conv_verification_api.checked_truncate_u64_u16 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U16) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U16 Int
(fun (v : Aeneas.Std.U16) =>
@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U16) fun (out : Option.{0} Aeneas.Std.U16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U16))
(num_conv_verification_api.checked_truncate_u128_u16 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U16) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U16 Int
(fun (v : Aeneas.Std.U16) =>
@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U16) fun (out : Option.{0} Aeneas.Std.U16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U16))
(num_conv_verification_api.checked_truncate_usize_u16 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U16) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U16 Int
(fun (v : Aeneas.Std.U16) =>
@Nat.cast.{0} Int instNatCastInt (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U16 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U32) fun (out : Option.{0} Aeneas.Std.U32) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U32))
(num_conv_verification_api.checked_truncate_u32_u32 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U32) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U32 Int
(fun (v : Aeneas.Std.U32) =>
@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U32) fun (out : Option.{0} Aeneas.Std.U32) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U32))
(num_conv_verification_api.checked_truncate_u64_u32 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U32) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U32 Int
(fun (v : Aeneas.Std.U32) =>
@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U32) fun (out : Option.{0} Aeneas.Std.U32) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U32))
(num_conv_verification_api.checked_truncate_u128_u32 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U32) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U32 Int
(fun (v : Aeneas.Std.U32) =>
@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U32 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U64) fun (out : Option.{0} Aeneas.Std.U64) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U64))
(num_conv_verification_api.checked_truncate_u64_u64 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U64) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U64 Int
(fun (v : Aeneas.Std.U64) =>
@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U64) fun (out : Option.{0} Aeneas.Std.U64) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U64))
(num_conv_verification_api.checked_truncate_u128_u64 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U64) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U64 Int
(fun (v : Aeneas.Std.U64) =>
@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U64 v))
out)
(NumConvSpec.checked (@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} (Option.{0} Aeneas.Std.U128) fun (out : Option.{0} Aeneas.Std.U128) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.U128))
(num_conv_verification_api.checked_truncate_u128_u128 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.U128) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.U128 Int
(fun (v : Aeneas.Std.U128) =>
@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U128 v))
out)
(NumConvSpec.checked
(@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} (Option.{0} Aeneas.Std.Usize)
fun (out : Option.{0} Aeneas.Std.Usize) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.Usize))
(num_conv_verification_api.checked_truncate_usize_usize x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.Usize) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.Usize Int
(fun (v : Aeneas.Std.Usize) =>
@Nat.cast.{0} Int instNatCastInt
(@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize v))
out)
(NumConvSpec.checked
(@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} (Option.{0} Aeneas.Std.I8) fun (out : Option.{0} Aeneas.Std.I8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.I8))
(num_conv_verification_api.checked_truncate_i8_i8 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.I8) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I8 Int
(fun (v : Aeneas.Std.I8) =>
@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I8) fun (out : Option.{0} Aeneas.Std.I8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.I8))
(num_conv_verification_api.checked_truncate_i16_i8 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.I8) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I8 Int
(fun (v : Aeneas.Std.I8) =>
@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I8)
fun (out : Option.{0} Aeneas.Std.I8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.I8))
(num_conv_verification_api.checked_truncate_i32_i8 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.I8) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I8 Int
(fun (v : Aeneas.Std.I8) =>
@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I8)
fun (out : Option.{0} Aeneas.Std.I8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.I8))
(num_conv_verification_api.checked_truncate_i64_i8 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.I8) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I8 Int
(fun (v : Aeneas.Std.I8) =>
@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I8)
fun (out : Option.{0} Aeneas.Std.I8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.I8))
(num_conv_verification_api.checked_truncate_i128_i8 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.I8) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I8 Int
(fun (v : Aeneas.Std.I8) =>
@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I8)
fun (out : Option.{0} Aeneas.Std.I8) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.I8))
(num_conv_verification_api.checked_truncate_isize_i8 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.I8) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I8 Int
(fun (v : Aeneas.Std.I8) =>
@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I8 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I16)
fun (out : Option.{0} Aeneas.Std.I16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.I16))
(num_conv_verification_api.checked_truncate_i16_i16 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.I16) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I16 Int
(fun (v : Aeneas.Std.I16) =>
@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I16)
fun (out : Option.{0} Aeneas.Std.I16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.I16))
(num_conv_verification_api.checked_truncate_i32_i16 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.I16) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I16 Int
(fun (v : Aeneas.Std.I16) =>
@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I16)
fun (out : Option.{0} Aeneas.Std.I16) =>
And
(@Eq.{1} (Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.I16))
(num_conv_verification_api.checked_truncate_i64_i16 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.I16)
out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I16 Int
(fun (v : Aeneas.Std.I16) =>
@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I16)
fun (out : Option.{0} Aeneas.Std.I16) =>
And
(@Eq.{1}
(Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.I16))
(num_conv_verification_api.checked_truncate_i128_i16 x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.I16)
out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I16 Int
(fun (v : Aeneas.Std.I16) =>
@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I16)
fun (out : Option.{0} Aeneas.Std.I16) =>
And
(@Eq.{1}
(Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.I16))
(num_conv_verification_api.checked_truncate_isize_i16
x)
(@Aeneas.Std.Result.ok.{0} (Option.{0} Aeneas.Std.I16)
out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I16 Int
(fun (v : Aeneas.Std.I16) =>
@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I16
v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I32)
fun (out : Option.{0} Aeneas.Std.I32) =>
And
(@Eq.{1}
(Aeneas.Std.Result.{0} (Option.{0} Aeneas.Std.I32))
(num_conv_verification_api.checked_truncate_i32_i32
x)
(@Aeneas.Std.Result.ok.{0}
(Option.{0} Aeneas.Std.I32) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I32 Int
(fun (v : Aeneas.Std.I32) =>
@Aeneas.Std.IScalar.val Aeneas.Std.IScalarTy.I32
v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I32)
fun (out : Option.{0} Aeneas.Std.I32) =>
And
(@Eq.{1}
(Aeneas.Std.Result.{0}
(Option.{0} Aeneas.Std.I32))
(num_conv_verification_api.checked_truncate_i64_i32
x)
(@Aeneas.Std.Result.ok.{0}
(Option.{0} Aeneas.Std.I32) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I32 Int
(fun (v : Aeneas.Std.I32) =>
@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I32 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I32)
fun (out : Option.{0} Aeneas.Std.I32) =>
And
(@Eq.{1}
(Aeneas.Std.Result.{0}
(Option.{0} Aeneas.Std.I32))
(num_conv_verification_api.checked_truncate_i128_i32
x)
(@Aeneas.Std.Result.ok.{0}
(Option.{0} Aeneas.Std.I32) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I32 Int
(fun (v : Aeneas.Std.I32) =>
@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I32 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I64)
fun (out : Option.{0} Aeneas.Std.I64) =>
And
(@Eq.{1}
(Aeneas.Std.Result.{0}
(Option.{0} Aeneas.Std.I64))
(num_conv_verification_api.checked_truncate_i64_i64
x)
(@Aeneas.Std.Result.ok.{0}
(Option.{0} Aeneas.Std.I64) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I64 Int
(fun (v : Aeneas.Std.I64) =>
@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I64 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I64)
fun (out : Option.{0} Aeneas.Std.I64) =>
And
(@Eq.{1}
(Aeneas.Std.Result.{0}
(Option.{0} Aeneas.Std.I64))
(num_conv_verification_api.checked_truncate_i128_i64
x)
(@Aeneas.Std.Result.ok.{0}
(Option.{0} Aeneas.Std.I64) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I64 Int
(fun (v : Aeneas.Std.I64) =>
@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I64 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.I128)
fun (out : Option.{0} Aeneas.Std.I128) =>
And
(@Eq.{1}
(Aeneas.Std.Result.{0}
(Option.{0} Aeneas.Std.I128))
(num_conv_verification_api.checked_truncate_i128_i128
x)
(@Aeneas.Std.Result.ok.{0}
(Option.{0} Aeneas.Std.I128) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.I128 Int
(fun (v : Aeneas.Std.I128) =>
@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.I128 v)
out)
(NumConvSpec.checked
(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} (Option.{0} Aeneas.Std.Isize)
fun (out : Option.{0} Aeneas.Std.Isize) =>
And
(@Eq.{1}
(Aeneas.Std.Result.{0}
(Option.{0} Aeneas.Std.Isize))
(num_conv_verification_api.checked_truncate_isize_isize
x)
(@Aeneas.Std.Result.ok.{0}
(Option.{0} Aeneas.Std.Isize) out))
(@Eq.{1} (Option.{0} Int)
(@Option.map.{0, 0} Aeneas.Std.Isize Int
(fun (v : Aeneas.Std.Isize) =>
@Aeneas.Std.IScalar.val
Aeneas.Std.IScalarTy.Isize v)
out)
(NumConvSpec.checked
(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.CoreOption· Init.PreludeEq· Init.PreludeAeneas.Std.Result· Aeneas.Std.Primitivesnum_conv_verification_api.checked_truncate_u8_u8Aeneas.Std.Result.ok· Aeneas.Std.PrimitivesInt· Init.Data.Int.BasicOption.map· Init.PreludeNat.cast· Init.Data.CastinstNatCastInt· Init.Data.Int.BasicAeneas.Std.UScalar.val· Aeneas.Std.Scalar.CoreAeneas.Std.UScalarTy.U8· Aeneas.Std.Scalar.CoreNumConvSpec.checkedOfNat.ofNat· Init.PreludeinstOfNat· Init.Data.Int.BasicNumConvSpec.unsignedMaxNat· Init.PreludeinstOfNatNat· Init.PreludeAeneas.Std.U16· Aeneas.Std.Scalar.Corenum_conv_verification_api.checked_truncate_u16_u8Aeneas.Std.UScalarTy.U16· Aeneas.Std.Scalar.CoreAeneas.Std.U32· Aeneas.Std.Scalar.Corenum_conv_verification_api.checked_truncate_u32_u8Aeneas.Std.UScalarTy.U32· Aeneas.Std.Scalar.CoreAeneas.Std.U64· Aeneas.Std.Scalar.Corenum_conv_verification_api.checked_truncate_u64_u8Aeneas.Std.UScalarTy.U64· Aeneas.Std.Scalar.CoreAeneas.Std.U128· Aeneas.Std.Scalar.Corenum_conv_verification_api.checked_truncate_u128_u8Aeneas.Std.UScalarTy.U128· Aeneas.Std.Scalar.CoreAeneas.Std.Usize· Aeneas.Std.Scalar.Corenum_conv_verification_api.checked_truncate_usize_u8Aeneas.Std.UScalarTy.Usize· Aeneas.Std.Scalar.Corenum_conv_verification_api.checked_truncate_u16_u16num_conv_verification_api.checked_truncate_u32_u16num_conv_verification_api.checked_truncate_u64_u16num_conv_verification_api.checked_truncate_u128_u16num_conv_verification_api.checked_truncate_usize_u16num_conv_verification_api.checked_truncate_u32_u32num_conv_verification_api.checked_truncate_u64_u32num_conv_verification_api.checked_truncate_u128_u32num_conv_verification_api.checked_truncate_u64_u64num_conv_verification_api.checked_truncate_u128_u64num_conv_verification_api.checked_truncate_u128_u128num_conv_verification_api.checked_truncate_usize_usizeAeneas.Std.UScalarTy.numBits· Aeneas.Std.Scalar.CoreAeneas.Std.I8· Aeneas.Std.Scalar.Corenum_conv_verification_api.checked_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.checked_truncate_i16_i8Aeneas.Std.IScalarTy.I16· Aeneas.Std.Scalar.CoreAeneas.Std.I32· Aeneas.Std.Scalar.Corenum_conv_verification_api.checked_truncate_i32_i8Aeneas.Std.IScalarTy.I32· Aeneas.Std.Scalar.CoreAeneas.Std.I64· Aeneas.Std.Scalar.Corenum_conv_verification_api.checked_truncate_i64_i8Aeneas.Std.IScalarTy.I64· Aeneas.Std.Scalar.CoreAeneas.Std.I128· Aeneas.Std.Scalar.Corenum_conv_verification_api.checked_truncate_i128_i8Aeneas.Std.IScalarTy.I128· Aeneas.Std.Scalar.CoreAeneas.Std.Isize· Aeneas.Std.Scalar.Corenum_conv_verification_api.checked_truncate_isize_i8Aeneas.Std.IScalarTy.Isize· Aeneas.Std.Scalar.Corenum_conv_verification_api.checked_truncate_i16_i16num_conv_verification_api.checked_truncate_i32_i16num_conv_verification_api.checked_truncate_i64_i16num_conv_verification_api.checked_truncate_i128_i16num_conv_verification_api.checked_truncate_isize_i16num_conv_verification_api.checked_truncate_i32_i32num_conv_verification_api.checked_truncate_i64_i32num_conv_verification_api.checked_truncate_i128_i32num_conv_verification_api.checked_truncate_i64_i64num_conv_verification_api.checked_truncate_i128_i64num_conv_verification_api.checked_truncate_i128_i128num_conv_verification_api.checked_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