| float_minmax | Project.FloatMinmax.Spec.FloatMinmaxSpec Describe what `float_minmax` computes here, then replace `True` with a `TerminatesWith` / `PartiallyMeets` statement over `«module»` (the decoded program emitted into `Program.lean`). | 0 | 0 | unproven |
| float_reinterpret | Project.FloatReinterpret.Spec.FloatReinterpretSpec | 0 | 1 | 1 proof |
| float_round | Project.FloatRound.Spec.FloatRoundSpec | 1 | 1 | 1 proof |
| float_trunc | Project.FloatTrunc.Spec.FloatTruncSpec | 1 | 1 | 1 proof |
| 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. Given indices `i, j` both in bounds (`< len`); an array region `[ptr, ptr + 8 * len)` that is addressable (`ptr.toNat + 8 | 1 | 1 | 1 proof |
| total_variation | Project.TotalVariation.Spec.TotalVariationSpec | 1 | 1 | 1 proof |