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.

[feliperodri]

Note: reviewed as part of Ch9 triage. This PR is a narrow but sound contract hardening (adds #[ensures(|d| d.nanos.as_inner() == 0)] to Duration::from_secs), not a Ch9 solution attempt (Ch9 is already marked Resolved). No cfg body swaps, no runtime logic changes, non-vacuous ensures, and covered symbolically by the existing autoharness allowlist for time::Duration::from_secs (with --default-unwind 1000). Good followup direction: matching hardening for from_millis/from_micros/from_nanos. When ready to un-draft this can land as a hardening PR.

[Adkid-Zephyr]

Thanks for the review. This PR is already ready for review (marked ready on August 29). I rechecked the current head, 6a3c8e3: 26 checks pass, with two skipped. The diff remains the single from_secs postcondition, with no runtime changes.

I agree that this is contract hardening rather than a Ch9 solution. The matching constructors would be a separate follow-up so this PR stays focused.