Fix assert! and cover! expansions in expression contexts

[trevordcampbell]

Problem and resulting behavior

The no-message assert! arm and all three kani::cover! arms emit a trailing semicolon without an enclosing Rust block. Valid expression-position calls therefore produce a trailing-semicolon diagnostic; with warnings denied, compilation fails before verification.

This is also a future-compatibility defect, tracked in rust-lang/rust#79813. Our original Kani 0.68.0 environment (nightly-2026-08-21) reported semicolon_in_expressions_from_macros; the PR's newer nightly-2026-09-23 reports semicolon_in_expressions_from_non_local_macros. The underlying invalid expansion is the same.

Resolves #4874. Related: #1572 addressed expression-context expansion for a message-bearing assertion.

Changes

• Make the no-message assert! arm emit a unit-valued block expression, matching the existing message-bearing arms.
• Add the requested comment explaining why the extra braces are necessary.
• Apply the same repair to all three kani::cover! forms: location, condition, and condition with a literal message.
• Preserve the matchers, supported optional comma, condition evaluation count, assertion/coverage calls, diagnostic text, and assertion's !! handling from Kani assert override is more restrictive than standard assert #2108.

The inner braces are emitted as a Rust block, so the existing call's semicolon is valid inside it:

($cond:expr, $msg:literal) => {{
    kani::cover($cond, $msg);
}};

No additional branch, allocation, formatting operation, or condition evaluation is introduced. No caller rewrite or lint suppression is needed.

Regression coverage

tests/kani/Assert/expression_contexts.rs denies warnings and covers constant initializers, inline constants, statement/expression forms, the optional comma, single condition evaluation, and a separate #[kani::should_panic] control to reject a no-op assertion implementation.

tests/expected/cover/expression-contexts/ uses the existing expected-output suite. Under #![deny(warnings)], all three cover forms appear as unit-typed initializers. The test requires:

• The location and side-effecting condition covers to be SATISFIED.
• The reachable false condition to be UNSATISFIABLE.
• The original default and supplied messages and source locations.
• Exactly two of three cover properties satisfied and successful verification.
• The condition to be evaluated exactly once.

Checking the emitted properties and their outcomes prevents a no-op cover implementation from passing.

Validation

Focused follow-up validation (Linux aarch64, nightly-2026-09-23): used the compiler from this PR's successful CI bundle build, rebuilding the verifier/model libraries from the PR source plus these changes in an isolated installation.

• Before the cover repair, all three expression-position cover invocations failed compilation with the trailing-semicolon diagnostic.
• After the repair, the native compiletest selection --suite expected --mode expected --timeout 120 cover/ passed 6 tests, including the new exact-output regression and existing cover cases.
• The native compiletest selection --suite kani --mode kani --timeout 120 Assert/ passed 13 tests, including the original assertion regression and its expected-failure harness.
• Rustfmt checks passed for both changed library files and both regression source files using Kani's pinned toolchain and formatting configuration.

Independent maintainer validation of the original assertion fix: feliperodri reproduced seven expression-position errors on main and confirmed the fix passes, with the kani, expected, and ui suites green and assertion messages unchanged.

Earlier downstream validation: the assertion repair was also validated with the released Kani 0.68.0 compiler, strict-warning positive and deliberate-failure controls, and an existing downstream proof suite, without changing application assertions or warning policy.

The full upstream suite and other platforms have not been rerun locally for this follow-up; the new commit's CI remains the broader check. The previously reported Intel macOS cargo_autoharness_fmt_impls timeout also occurred on upstream main, as the maintainer confirmed.

Adoption

Distribute the corrected libraries through Kani's normal release process so affected users can return to the unmodified official bundle.

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

[trevordcampbell]

I investigated the Intel macOS failure. cargo_autoharness_fmt_impls exceeded the 60-second CBMC timeout, preventing the expected assertion diagnostics from appearing.

The same fixture also failed with a timeout on the upstream base commit, before this PR. The assertion regression suite passed, and all other platform regression jobs passed.

This appears to be an existing intermittent timeout. Could a maintainer rerun the failed job? My account lacks permission to trigger it.

[Copilot]

Copilot review overview

🟢 Approval recommended

The targeted fix matches existing macro patterns and is comprehensively covered.

Review effort: Balanced
Findings: None

What changed in this PR

Fixes no-message assert! usage in expression contexts by emitting a unit-valued block.

Changes:

• Wraps the macro expansion in an explicit block.
• Adds regression coverage for expression contexts, evaluation count, and failure behavior.

File	Description
library/​std/​src/​lib.rs	Corrects the no-message assert! expansion.
tests/​kani/​Assert/​expression_contexts.rs	Adds focused regression harnesses.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

Approving. Reproduced on main: the new test fails with 7 trailing semicolon in macro used in expression position errors and passes with the fix. kani/expected/ui suites are green, and no assertion message changed.

One point that strengthens the case: this lint is future-incompatible (rust-lang/rust#79813, "will become a hard error in a future release"), so it isn't only a -D warnings problem. Without the fix, a future toolchain would break expression-position asserts for everyone. On this nightly the lint is semicolon_in_expressions_from_non_local_macros, not ..._from_macros.

kani::cover! (library/kani/src/lib.rs, all three arms) has the same shape and fails the same way: true => kani::cover!(), errors under -D warnings even with this PR. Not blocking; it would fit here as the same three-line change, or as a follow-up.

The macOS-Intel failure (cargo_autoharness_fmt_impls) isn't from this PR: the same test fails on main at 3e07bd2de.

[trevordcampbell]

Merged current upstream main (f314aefb8ed0369c838c474924fc1937afea40b2) into this branch as 33649c38c56ab4c5edfcb895325c5c731af67687. Compared the PR against its new base: the same five files, blob contents, and patches remain; the assertion/coverage repair and regression tests are unchanged.

I also investigated all four failures from the preceding d6175fb run:

Job	Finding
Intel macOS regression	cargo_autoharness_fmt_impls timed out on the Pointer and UpperExp implementations. The Kani suite (614 passed) and expected-output suite (479 passed) completed successfully beforehand. This is the previously reported timeout family.
perf	s2n-quic-platform fails with E0276 because its Environment::close implementation adds a Send bound removed by bach 0.1.3.
compile-timer-long	The same error occurs while compiling the old/base revision 52c68879.
perf-benchcomp	Both variants encounter the dependency error. Separately, the final performance gate flags u32_u16_differential at 11.21368s → 18.05306s solver time.

The dependency failure also occurs on current upstream main after the s2n-quic update. I posted the source diagnosis, proposed s2n-quic repair, and validation boundary on #4901.

The same checksum timing gate also trips on current main (12.14612s → 22.71049s). I added these measurements and the caveat that equal VCC/step counts do not establish formula identity on #4846. A controlled repeat is still needed before attributing or dismissing a change-specific slowdown; the full benchmark runs were not clean.

I found no correctness change needed in the macro patch from this investigation. The new Kani CI run and companion workflows are currently action_required, with execution awaiting maintainer approval. Could a maintainer approve the new runs? The benchmark dependency problem above will still need its own repair.