Talos · verification report

All specs

49 specs across 7 projects · 48 proven · 1 unproven
Project Spec Bound exports Proofs Status
num_integer Project.NumInteger.Spec.GcdU64Spec
The exported `gcd_u64` returns the greatest common divisor of two `u64` operands, computed by the binary-GCD (Stein's) algorithm. The `num-integer` convention `gcd(0, 0) = 0` is preserved. The `initi
1 1 1 proof
rust_array Project.RustArray.Spec.LenSpec 0 1 1 proof
rust_array Project.RustArray.Spec.IsEmptySpec 0 1 1 proof
rust_array Project.RustArray.Spec.LenExportSpec 1 1 1 proof
rust_array Project.RustArray.Spec.IsEmptyExportSpec 1 1 1 proof
rust_array_tests Project.RustArrayTests.Spec.LenPlusOneSpec 0 1 1 proof
rust_array_tests Project.RustArrayTests.Spec.LenPlusArgSpec 0 1 1 proof
rust_array_tests Project.RustArrayTests.Spec.EmptyPlusThreeSpec 0 1 1 proof
rust_array_tests Project.RustArrayTests.Spec.EmptyXorFlagSpec 0 1 1 proof
rust_array_tests Project.RustArrayTests.Spec.LenPlusOneExportSpec 1 1 1 proof
rust_array_tests Project.RustArrayTests.Spec.LenPlusArgExportSpec 1 1 1 proof
rust_array_tests Project.RustArrayTests.Spec.EmptyPlusThreeExportSpec 1 1 1 proof
rust_array_tests Project.RustArrayTests.Spec.EmptyXorFlagExportSpec 1 1 1 proof
rust_u64 Project.RustU64.Spec.AbsDiffSpec 0 1 1 proof
rust_u64 Project.RustU64.Spec.AddSpec 1 1 1 proof
rust_u64 Project.RustU64.Spec.SubSpec 1 1 1 proof
rust_u64 Project.RustU64.Spec.MulSpec 1 1 1 proof
rust_u64 Project.RustU64.Spec.DivSpec 1 1 1 proof
rust_u64 Project.RustU64.Spec.RemSpec 1 1 1 proof
rust_u64 Project.RustU64.Spec.BitAndSpec 1 1 1 proof
rust_u64 Project.RustU64.Spec.BitOrSpec 1 1 1 proof
rust_u64 Project.RustU64.Spec.BitXorSpec 1 1 1 proof
rust_u64 Project.RustU64.Spec.NotSpec 1 1 1 proof
rust_u64 Project.RustU64.Spec.ShlSpec 1 1 1 proof
rust_u64 Project.RustU64.Spec.ShrSpec 1 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.AddChainSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.AddThenMulSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.SubChainSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.SubThenAddSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.MulChainSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.MulThenAddSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.AndChainSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.AndThenOrSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.OrChainSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.OrThenXorSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.XorChainSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.XorThenAndSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.NotTwiceSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.NotThenXorSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.DivThenAddSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.DivThenMulSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.RemThenAddSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.RemThenMulSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.ShlThenAddSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.ShlTwiceSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.ShrThenSubSpec 0 1 1 proof
rust_u64_tests Project.RustU64Tests.Spec.ShrTwiceSpec 0 1 1 proof
swap_elements Project.SwapElements.Spec.SwapElementsSpec
The exported `swap_elements` swaps two elements of a `[u64]` slice in place. Informal spec. Given indices `i, j` both in bounds (`< len`) and an array region `[ptr, ptr + 8 * len)` that sits at or ab
1 0 unproven
total_variation Project.TotalVariation.Spec.TotalVariationSpec 1 1 1 proof