Phased and Confused: typestate enforcement for post-mono Body invariants by cds-amal · Pull Request #136 · runtimeverification/stable-mir-json

cds-amal · 2026-03-05T02:13:20Z

No description provided.

Wrap Body in a Phased<T, S> generic wrapper parameterized by phase markers Raw and Mono. Phase 1+2 code works with Item<Raw> (bodies may contain ConstantKind::Unevaluated); the phase 2→3 boundary validates each body via UnevaluatedChecker (a MirVisitor that panics on any remaining unevaluated constant) before promoting to Item<Mono>. This makes the invariant that was previously implicit (all unevaluated constants resolved by the fixpoint loop) into a compile-time guarantee: phase 3 code structurally receives validated data. Phased serializes transparently (delegates to inner T), so JSON output is unchanged.

The UnevaluatedChecker panic now explains what happened (the fixpoint loop didn't resolve a surviving unevaluated constant), why it matters (the input program likely triggers an unhandled code path), and what the user should do (file an issue with the triggering .rs file).

Copilot

Pull request overview

This PR introduces a typestate-based phase marker system to enforce an invariant that MIR bodies stored post-fixpoint (phase 3) contain no ConstantKind::Unevaluated, by wrapping bodies and validating them at the phase 2 → 3 boundary.

Changes:

Added phased::Phased<Body, S> with Raw/Mono markers and a validation step that checks for unevaluated constants.
Made Item and MonoItemKind generic over the phase marker and validated all collected items before assembling SmirJson.
Updated graph renderers to work with the new phased body wrapper.

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
`src/printer/schema.rs`	Makes `Item` generic over phase marker and wires `Item<Raw> -> Item<Mono>` validation; updates `SmirJson`/`CollectedCrate` to store `Item<Mono>`.
`src/printer/phased.rs`	New typestate wrapper `Phased` plus MIR visitor that enforces the “no unevaluated constants” invariant.
`src/printer/mod.rs`	Registers the new `phased` module and updates module-level docs/re-exports.
`src/printer/items.rs`	Makes `MonoItemKind` generic and wraps bodies in `Phased<Body, Raw>` during item construction.
`src/printer/collect.rs`	Validates all items at the phase 2 → 3 boundary before building `CollectedCrate`.
`src/mk_graph/output/dot.rs`	Adapts DOT rendering to use `Phased::inner()` for body access.
`src/mk_graph/output/d2.rs`	Adapts D2 rendering to use `Phased::inner()` for body access.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-03-07T19:29:23Z

+    /// Validate that the body contains no `ConstantKind::Unevaluated`, then
+    /// promote to the `Mono` phase. Panics if the invariant is violated.
+    pub fn validate(self) -> Phased<Body, Mono> {
+        UnevaluatedChecker.visit_body(&self.0);


Phased<Body, Raw>::validate calls UnevaluatedChecker.visit_body(...), but MirVisitor::visit_body requires &mut self. Calling it on the unit struct value will not compile; create a mutable UnevaluatedChecker instance (e.g., let mut checker = UnevaluatedChecker; checker.visit_body(...)).

Suggested change

UnevaluatedChecker.visit_body(&self.0);

let mut checker = UnevaluatedChecker;

checker.visit_body(&self.0);

Copilot · 2026-03-07T19:29:23Z

+
+use std::marker::PhantomData;
+
+use crate::compat::serde;


use crate::compat::serde; is unused in this module. CI runs clippy with -Dwarnings and builds with --deny warnings, so this will fail the build; please remove the import (or use it if it’s needed).

Suggested change

use crate::compat::serde;

Copilot · 2026-03-07T19:29:24Z

+                        for (index, decl) in body.cloned().unwrap().local_decls() {
                            let ty_with_layout = ctx.render_type_with_layout(decl.ty);
                            vector.push(format!("{index} = {}", ty_with_layout));


body.cloned().unwrap() will panic when a function body is missing (which is explicitly handled later via the <empty body> branch). Consider handling None here as well (e.g., skip locals rendering or emit an empty locals node) so to_dot_file can render crates even when some bodies aren’t available.

Suggested change

for (index, decl) in body.cloned().unwrap().local_decls() {

let ty_with_layout = ctx.render_type_with_layout(decl.ty);

vector.push(format!("{index} = {}", ty_with_layout));

if let Some(body) = body {

for (index, decl) in body.local_decls() {

let ty_with_layout = ctx.render_type_with_layout(decl.ty);

vector.push(format!("{index} = {}", ty_with_layout));

}

Copilot · 2026-03-07T19:29:24Z

 // Re-exports preserving the public API
 pub use collect::collect_smir;
 pub use items::MonoItemKind;
+pub use phased::Mono;
 pub use schema::{AllocInfo, FnSymType, Item, LinkMapKey, SmirJson, TypeMetadata};


Item and MonoItemKind are now generic over a phase marker (Item<S>, MonoItemKind<S>), which is a breaking change for downstream users of the printer public API. If this is intended, the comment about “preserving the public API” is now misleading; consider updating it and/or providing compatibility type aliases (e.g., pub type ItemMono = Item<Mono>) for the common externally-consumed types.

Suggested change

// Re-exports preserving the public API

pub use collect::collect_smir;

pub use items::MonoItemKind;

pub use phased::Mono;

pub use schema::{AllocInfo, FnSymType, Item, LinkMapKey, SmirJson, TypeMetadata};

// Public re-exports and backwards-compatible aliases

pub use collect::collect_smir;

pub use items::MonoItemKind;

pub use phased::Mono;

pub use schema::{AllocInfo, FnSymType, Item, LinkMapKey, SmirJson, TypeMetadata};

/// Backwards-compatible alias for the monomorphized `Item` phase.

pub type ItemMono = Item<Mono>;

/// Backwards-compatible alias for the monomorphized `MonoItemKind` phase.

pub type MonoItemKindMono = MonoItemKind<Mono>;

Copilot · 2026-03-07T19:29:24Z

+        &self.0
+    }
+
+    /// Consume the wrapper, returning the inner value.


Phased::into_inner is currently unused within the crate, and since phased is not a public module this will trigger the dead_code lint (“method is never used”) under CI’s --deny warnings. Consider removing it for now, or annotate it with an appropriate #[allow(dead_code)] if you want to keep it for future use.

Suggested change

/// Consume the wrapper, returning the inner value.

/// Consume the wrapper, returning the inner value.

#[allow(dead_code)]

cds-amal added 2 commits March 4, 2026 21:11

cds-amal changed the title ~~Cds/phased body typestate~~ Phased and Confused: typestate enforcement for post-mono Body invariants Mar 7, 2026

cds-amal marked this pull request as ready for review March 7, 2026 19:25

cds-amal requested review from a team and Copilot March 7, 2026 19:25

Copilot started reviewing on behalf of cds-amal March 7, 2026 19:26 View session

Copilot AI reviewed Mar 7, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Phased and Confused: typestate enforcement for post-mono Body invariants#136

Phased and Confused: typestate enforcement for post-mono Body invariants#136
cds-amal wants to merge 2 commits intomasterfrom
cds/phased-body-typestate

cds-amal commented Mar 5, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Mar 7, 2026

Uh oh!

Copilot AI Mar 7, 2026

Uh oh!

Copilot AI Mar 7, 2026

Uh oh!

Copilot AI Mar 7, 2026

Uh oh!

Copilot AI Mar 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

	UnevaluatedChecker.visit_body(&self.0);
	let mut checker = UnevaluatedChecker;
	checker.visit_body(&self.0);

	/// Consume the wrapper, returning the inner value.
	/// Consume the wrapper, returning the inner value.
	#[allow(dead_code)]

Conversation

cds-amal commented Mar 5, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Mar 7, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 7, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 7, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 7, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 7, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants