From 1e8276a3ffbc53a36dbdcf82c79757769cff640d Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Sat, 15 Aug 2026 03:55:13 -0700 Subject: [PATCH] emit: sequence a unit after a conditional that names its join state Pulse rejects an annotated conditional in tail position: the annotation and the enclosing signature's postcondition are two postconditions for the same term, and the checker reports the pair rather than reconciling them. Emitting a unit after the conditional keeps the annotation local to the join, which is the only place it constrains anything. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 6578d2a80c9ce6f3a6b9cb10ba2cdcc99fc78972) --- src/pass/emit.rs | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/pass/emit.rs b/src/pass/emit.rs index c12737a4..71eebac8 100644 --- a/src/pass/emit.rs +++ b/src/pass/emit.rs @@ -4399,6 +4399,18 @@ impl<'a> Emitter<'a> { doc = doc.append(Doc::line().append(self.emit_stmt(&env, stmt))); env.push_stmt(stmt); idx += 1; + // A conditional that names its own join state cannot be the last + // thing in a block: Pulse would then have two postconditions for + // it -- the annotated one and the one the enclosing signature + // already fixed -- and rejects the pair rather than reconciling + // them. Sequencing a unit after it keeps the annotation local to + // the join, which is the only place it says anything. + if idx == stmts.len() + && let StmtT::If { ensures, .. } = &stmt.val + && !ensures.is_empty() + { + doc = doc.append(Doc::line().append("()")); + } } doc }