Tautological postconditions: some merged contracts hold for any implementation (demonstrated by mutation)

[KyleClouthier]

This follows on from @feliperodri's comment in kani-verifier-blog#59, where the idea of automatically checking that assumptions are reachable came up. This is a case that check would not catch, and I think it is worth naming because it sits in the merged corpus today.

To be clear up front: this is not a defect report. Layout::for_value_raw is correct. The finding is about what its contract warrants, which turns out to be nothing.

The contract

library/core/src/alloc/layout.rs, its only postcondition:

#[ensures(|result| result.align().is_power_of_two())]
pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self

Layout's own type invariant guarantees align() is a power of two. It is enforced at construction, and Layout::from_size_align returns Err otherwise. So this clause holds for every possible implementation of for_value_raw, including one that ignores its argument.

Demonstrated by mutation

I replaced the body with one that ignores t entirely and returns a fixed layout, then ran the existing merged harness check_for_value_raw_i32 unchanged:

pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self {
    let _ = t;
    unsafe { Layout::from_size_align_unchecked(1, 1) }
}

For i32 the correct answer is size 4, align 4. This returns size 1, align 1, for every type.

	correct implementation	mutant that ignores t
current align().is_power_of_two()	1 verified, 0 failures	1 verified, 0 failures
proposed (below)	1 verified, 0 failures	0 verified, 1 failures

The current contract cannot distinguish the standard library's implementation from one that ignores its input.

The proposed form, verified

The strong form already exists forty lines up in the same file, on the sibling function Layout::for_value:

#[ensures(|result| result.align() == mem::align_of_val(t))]

Applying the same shape to for_value_raw:

#[ensures(|result| result.align() == unsafe { mem::align_of_val_raw(t) })]
#[ensures(|result| result.size()  == unsafe { mem::size_of_val_raw(t) })]

This verifies against the real implementation and fails against the mutant, with Kani naming the responsible clause:

Failed Checks: |result| result.align() == unsafe { mem::align_of_val_raw(t) }
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

So unsafe inside an #[ensures] works, and the stronger contract costs nothing beyond the change itself.

Why reachability checking will not find this

This is the part I think is interesting for the automation discussion.

There is nothing unreachable here. The assertion is reached, there is no assume, the proof is sound, and the verdict is correct. A cover-based check sees a completely healthy harness, because the harness is healthy. The weakness is in what the contract says, not in what the harness explores.

Vacuity and this are duals. One is a proof over the empty set. The other is a proof of something that holds over every set. Reachability analysis detects the first and is blind to the second. As far as I can tell, mutation is the only thing that separates them, which is why I raised it as verify-rust-std#617 Criterion 2.

Two others in the same shape

I have not mutated these, so treat them as candidates and not results.

Alignment::of in library/core/src/ptr/alignment.rs, where both clauses are tautologies:

#[requires(mem::align_of::<T>().is_power_of_two())]        // align_of always returns a power of two
#[ensures(|result| result.as_usize().is_power_of_two())]   // Alignment is an enum of powers of two

Its harness is currently commented out behind a FIXME citing kani#3905. Worth noting that when that unblocks, this harness will verify immediately and establish nothing, which is a slightly awkward failure mode because it will look like progress.

Layout::align_to carries ...align().is_power_of_two() alongside a genuinely meaningful clause, so it is less severe.

What I am offering

Happy to open a PR strengthening for_value_raw and Alignment::of along the lines above, with the mutants as evidence that each new clause has teeth. Also happy to leave it here if you would rather handle it internally, or if I have misread the intent of the weaker form.

Reproduced with Kani 0.67.0 / CBMC 6.8.0 against verify-rust-std at 2138bc6, using scripts/run-kani.sh --kani-args --harness check_for_value_raw_i32.

[KyleClouthier]

Follow-up: for_value_raw is not an outlier. I swept the corpus for the general shape and the pattern is systemic, so this is probably worth handling as a convention question and not as a one-line fix.

The mechanical test

A postcondition that references no input cannot constrain the input-output relation. It can only assert a property of the return value in isolation.

That is checkable. Counting bare identifiers in each #[ensures] (excluding method names and paths, treating self and parameters as inputs) turns up 26 postconditions that mention no input at all.

Two caveats before the list, because the heuristic is crude:

• It misses type parameters. Layout::new's result.size() == mem::size_of::<T>() references T and is a perfectly good contract; my pattern only matched lowercase identifiers, so it flagged it. Those are false positives.
• Input-free does not automatically mean vacuous. pad_to_align's result.size() % result.align() == 0 is not guaranteed by Layout, so it has teeth. It just cannot relate output to input.

The subset that has no teeth at all

The interesting cases are input-free and guaranteed by the return type. Those hold for every possible implementation. They cluster in four type families:

type	postcondition	why it cannot fail
NonZero	result.get() != 0	the type's invariant is non-zero
NonNull	!result.pointer.is_null()	the type's invariant is non-null
Unique	!result.is_null()	same
Alignment	result.as_usize().is_power_of_two()	an enum of powers of two
Layout	result.align().is_power_of_two()	enforced in from_size_align

Instances I found, all currently merged:

layout.rs:233     for_value_raw     align().is_power_of_two()          (mutation-proven above)
layout.rs:273     align_to          ...align().is_power_of_two()       (has a meaningful sibling clause)
alignment.rs:59   of                as_usize().is_power_of_two()
alignment.rs:95   new_unchecked     as_usize().is_power_of_two()
alignment.rs:111  as_usize          result.is_power_of_two()
alignment.rs:120  as_nonzero        result.get().is_power_of_two()
non_null.rs:138   dangling          !result.pointer.is_null() && ...
non_null.rs:321   from_raw_parts    !result.pointer.is_null()
non_null.rs:397   map_addr          !result.as_ptr().is_null()
unique.rs:120     as_ptr            !result.is_null()
nonzero.rs:807    count_ones        result.get() > 0
nonzero.rs:840    rotate_left       result.get() != 0
nonzero.rs:873    rotate_right      result.get() != 0

I have only mutation-tested for_value_raw. The rest are candidates on the same reasoning, not results, and several sit beside genuinely strong clauses (rotate_left also asserts a round-trip through rotate_right, which is real).

A disclosure that I think is the actual point

While writing the blog post I added contracts to swap_bytes and reverse_bits, and I put result.get() != 0 on both. Same tautology. I copied it from the count_ones and rotate_left pattern directly above, because it looked like the local convention.

The contracts I added still have teeth, since I also asserted the involution and that population count is preserved, and those do fail against a mutant. But the non-zero clause is decoration and I did not notice until I ran this sweep an hour later.

That seems worth saying plainly, because it is the strongest evidence that this is a convention problem and not a diligence problem. The pattern is contagious specifically because it reads as house style. A contributor looking at neighbouring code will copy it, and nothing in review or CI distinguishes it from a clause that carries weight.

Suggestion

Nothing urgent, and I am not proposing anyone rewrite thirteen contracts tonight. But if a guideline for new contracts would be useful, something like:

A postcondition should relate the result to an input. A clause that only asserts a property the return type already guarantees is satisfied by every implementation, and reachability checking cannot detect it because nothing is unreachable.

Happy to open a PR strengthening the Layout and Alignment ones with mutants as evidence per clause, if that is useful. Equally happy to leave it if the weaker clauses are deliberate for reasons I have not understood.

[KyleClouthier]

I said in the comment above that only for_value_raw was mutation-tested and the rest were candidates. I have now tested more of them. Four for four survive, across four files and four type families.

Each mutant is written so the function does not do its job at all, while still type-checking and satisfying the return type's invariant. The harnesses are the merged ones, unmodified.

function	mutant	merged harness	result
Layout::for_value_raw	ignores its argument, returns Layout{size:1, align:1}	check_for_value_raw_i32	survives
Layout::dangling	ignores self.align, always address 1	check_dangling	survives
NonZero::count_ones	ignores self, always returns 1	nonzero_check_count_ones_for_{u8,i32}	survives
NonNull::map_addr	never applies f, returns self	non_null_check_map_addr	survives

Every one reports 0 failures.

Two of these are worth spelling out because the weak clause is about the right property and still cannot see the bug.

Layout::dangling is documented as returning a pointer "well-aligned for this Layout". Its contract is result.is_aligned(). But the return type is NonNull<u8> and align_of::<u8>() is 1, so the check asks whether an address is a multiple of one. A dangling that ignores self.align entirely and returns address 1 is misaligned for any layout requiring more, and passes.

NonNull::map_addr exists to apply a function to a pointer's address. Its contract asks only whether the result is non-null, and NonNull cannot be null. A map_addr that never applies f satisfies its specification completely.

Correction to my previous comment

I listed the two CStr contracts (from_ptr and from_bytes_with_nul_unchecked, both result.is_safe()) among the candidates. That was wrong and I withdraw it. is_safe() expands to

!bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len - 1].contains(&0)

which is genuine content about the value, not something the type guarantees for free. A mutant returning a CStr with an interior nul would be caught. Those contracts have teeth and I should have checked before listing them.

That takes the candidate set from 11 to 9.

Where the nine stand

4  mutation-tested, all survive     for_value_raw, Layout::dangling, count_ones, map_addr
3  untested, same shape             NonNull::dangling, NonNull::from_raw_parts, Unique::as_ptr
2  not testable as-is               Alignment::of (harness disabled behind kani#3905)
                                    Alignment::as_usize (no harness)

I am reporting exactly what I ran. The three untested ones assert !is_null() on a NonNull or Unique return, so I expect the same outcome, but expecting is not measuring and I have not measured them.

What I think this means

Not that anyone was careless. The pattern is local convention, and I demonstrated how contagious it is by walking into it myself last night in the same file. count_ones is the sharpest illustration: the harness that discharges it is one I wrote yesterday. I set out to fill in seven contracts in nonzero.rs that had never been proved, and at least one of those proofs establishes nothing, because the contract establishes nothing. I would have shipped a green check with no content and felt good about it.

The general rule that would have stopped all of this, me included:

A postcondition should relate the result to an input. A clause asserting only what the return type already guarantees is satisfied by every implementation, and no reachability analysis can detect that, because nothing is unreachable.

Still happy to open a PR strengthening these with a mutant per clause as evidence, if that is wanted. Reproduced with Kani 0.67.0 / CBMC 6.8.0 at 2138bc6; every file restored afterwards.