Strengthen Duration::from_secs contract to exclude fractional seconds

[Adkid-Zephyr]

Summary

• Require Duration::from_secs to return zero subsecond nanoseconds.
• Keep the standard-library implementation unchanged.

Motivation

The current contract guarantees that the result is representation-safe and that its secs field equals the input, but it does not constrain the fractional component. An implementation can therefore preserve secs, add any valid number of nanoseconds, and still satisfy the contract.

The new clause captures the documented whole-seconds semantics:

#[ensures(|duration| duration.nanos.as_inner() == 0)]

Mutation evidence

Implementation	Current contract	Strengthened contract
Correct	pass	pass
Fixed 1 ns fraction	pass	fail
Input-derived fraction	pass	fail
999,999,999 ns fraction	pass	fail

The mutation kill rate increases from 0/3 to 3/3. The contract harnesses use unconstrained u64 inputs, no kani::assume, and a separate cover check reaches u64::MAX.

Validation

• Standalone Kani mutation matrix: MUTATION_MATRIX=PASS
• Correct strengthened contract: successful
• Three strengthened mutants: fail at result.nanos == 0
• Full-width reachability: 1/1 cover property satisfied
• Independent Rust reference/mutant tests: 4 passed
• cargo fmt --check: passed
• git diff --check: passed

The production diff is contract-only and adds no precondition or runtime behavior change.

Related to the contract-strength discussion in #630.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.