| 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 from the canonical instantiated store. The contract uses the authoritative small-step machine and Iris partial correct | 1 | 1 | 1 proof |
| num_integer_opt3 | Project.NumIntegerOpt3.Spec.GcdU64Spec Public fuel-free specification of the optimized exported `gcd_u64`. Unlike the retained compatibility theorem below, this contract is stated entirely over the authoritative small-step machine. | 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.SmallStepSpec.SwapElementsDistinctSpec Public small-step contract for the non-aliasing case of the generated `swap_elements` export. The conclusion describes the physical memory in every successfully reached terminal store; it is not mere | 0 | 0 | unproven |
| swap_elements | Project.SwapElements.SmallStepSpec.SwapElementsAliasSpec Public small-step contract for equal indices. It deliberately asks for one array-word owner, so it remains usable with exclusive byte ownership. | 0 | 0 | unproven |
| 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 | 2 | 2 proofs |
| total_variation | Project.TotalVariation.Spec.TotalVariationSpec | 1 | 1 | 1 proof |