From c398af536ab3be43171d5f09871e51cc4c0d6481 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Sun, 27 Sep 2026 01:16:00 +0000 Subject: [PATCH 1/4] tla-export: what toyDB's Raft model needs, found against its hand-written oracle Exporting toydb's src/raft/safety.rs and model-checking it at tla/Raft.cfg's bounds turned up four gaps, each fixed generally: - Set::range / range_inclusive (and FiniteRange::range_set) over integers print as `lo..hi-1` / `lo..hi`; they were refused as an uninterpreted trait method, which took inv_hosts, inv_lterms and inv_commits out of the .cfg. - A binder guarded by `S.contains(Ctor { f: x, .. })` (nested constructors too) ranges over `{m.f : m \in {m \in S : m.tag = "Ctor"}}`; it was a Dom_ hole per binder, 44 of them in safety.rs's invariants. - A disjunction of two state predicates outside what Init reaches prints as `IF a THEN TRUE ELSE b`: TLC branches on `\/` in an action, so `b == 0 || log[b - 1].term == bt` indexed log[0] and stopped TLC. - `exists|step: Step| next_step(pre, post, step)` over a step enum whose match arms each call one transition is one `\E` per variant, each field bounded from that transition's guard (`0 <= i < pre.n`, `net.contains(..)`, `b <= e <= h.log.len()`); fields only a type bounds keep the 2^10 cap. safety.rs's 41 step-field holes become 3 (the payload of a proposed command, the ghost ack map, and t_bump_term's new term), and TLC no longer builds the union of every variant's values in every state (about 10x). With these the export reproduces tla/Raft.tla's 597,764 distinct states and diameter 18 with no conjunct violated. The new test checks a small model of the same shapes with TLC (144 states, as a breadth-first search finds). Co-Authored-By: Claude Opus 5.5 --- source/rust_verify_test/tests/tla_export.rs | 94 +++- source/vir/src/tla.rs | 513 +++++++++++++++++++- 2 files changed, 604 insertions(+), 3 deletions(-) diff --git a/source/rust_verify_test/tests/tla_export.rs b/source/rust_verify_test/tests/tla_export.rs index 7ea64d0d3c..9276ead363 100644 --- a/source/rust_verify_test/tests/tla_export.rs +++ b/source/rust_verify_test/tests/tla_export.rs @@ -2222,7 +2222,9 @@ fn tla_export_caps_a_domain_read_off_a_type() { assert!(!ex.tla.contains("0..65535 :"), "{}", ex.tla); assert!(!ex.tla.contains("Dom_Option"), "{}", ex.tla); assert!( - ex.tla.contains("[tag |-> \"Nudge\", v0 |-> v0__4] : v0__4 \\in 0..255}"), + ex.tla.contains( + "(\\E v0__3 \\in 0..255 : (LET st == [tag |-> \"Nudge\", v0 |-> v0__3] IN step(st)))" + ), "{}", ex.tla ); @@ -2895,3 +2897,93 @@ fn tla_export_refuses_reals() { assert_eq!(run.violated, Vec::::new(), "{}", ex.tla); assert_eq!(run.distinct, 3, "{run:?}\n{}", ex.tla); } + +/// The shapes toyDB's Raft model (`src/raft/safety.rs`) writes, which the +/// export of it against the hand-written `tla/Raft.tla` turned up: a node set +/// `Set::range(0, n)` (refused as an uninterpreted trait method); a +/// quantifier guarded by `net.contains(Msg::Ping { from, round })` (a hole +/// per binder); `b == 0 || log[b - 1] < 1` in a transition (TLC branches on +/// the `\/` and indexes `log[-1]`); and `exists|step: Step|` whose arms call +/// one transition each (a hole per field, and the union of every variant's +/// values built in every state). 144 states, as a breadth-first search of +/// the same system finds. +const MESSAGES: &str = r#" +use vstd::prelude::*; +verus! { +pub enum Msg { Ping { from: int, round: nat }, Note { log: Seq } } + +pub struct State { pub n: nat, pub net: Set, pub log: Seq } + +pub open spec fn nodes(n: nat) -> Set { Set::::range(0, n as int) } + +pub open spec fn init(s: State) -> bool { + &&& s.n == 2 + &&& s.net == Set::::empty() + &&& s.log == Seq::::empty() +} + +pub open spec fn ping(pre: State, post: State, from: int, round: nat) -> bool { + &&& nodes(pre.n).contains(from) + &&& round < 2 + &&& post == State { net: pre.net.insert(Msg::Ping { from, round }), ..pre } +} + +pub open spec fn extend(pre: State, post: State, b: nat) -> bool { + &&& b <= pre.log.len() < 2 + &&& (b == 0 || pre.log[b - 1] < 1) + &&& post == State { log: pre.log.push(b as int), ..pre } +} + +pub open spec fn echo(pre: State, post: State, from: int, round: nat) -> bool { + &&& pre.net.contains(Msg::Ping { from, round }) + &&& pre.log.len() < 2 + &&& post == State { log: pre.log.push(from + round), ..pre } +} + +pub enum Step { Ping { from: int, round: nat }, Extend { b: nat }, Echo { from: int, round: nat } } + +pub open spec fn next_step(pre: State, post: State, step: Step) -> bool { + match step { + Step::Ping { from, round } => ping(pre, post, from, round), + Step::Extend { b } => extend(pre, post, b), + Step::Echo { from, round } => echo(pre, post, from, round), + } +} + +pub open spec fn next(pre: State, post: State) -> bool { + exists|step: Step| next_step(pre, post, step) +} + +pub open spec fn pings_ok(s: State) -> bool { + forall|from: int, round: nat| #[trigger] s.net.contains(Msg::Ping { from, round }) + ==> nodes(s.n).contains(from) && round < 2 +} + +pub open spec fn log_small(s: State) -> bool { + forall|i: int| 0 <= i < s.log.len() ==> 0 <= #[trigger] s.log[i] <= 2 +} +} +"#; + +#[test] +fn tla_export_bounds_message_fields_and_step_fields_from_their_guards() { + let ex = export_code(MESSAGES, "test_crate"); + assert_eq!(ex.report["refusals"], serde_json::json!([]), "{}", ex.tla); + assert_eq!(ex.report["holes"], serde_json::json!([]), "{}", ex.tla); + assert_eq!(names(&ex.report["invariants"]), ["pings_ok", "log_small"]); + // The node set is a range. + assert!(ex.tla.contains("(0)..((n_2) - 1)"), "{}", ex.tla); + // A message field ranges over the fields of the messages in `net`. + assert!(ex.tla.contains(".from : m__"), "{}", ex.tla); + assert!(ex.tla.contains(".tag = \"Ping\"}}"), "{}", ex.tla); + // The guarding disjunction is evaluated, not branched on. + assert!(ex.tla.contains("(IF (b = 0) THEN TRUE ELSE"), "{}", ex.tla); + // One \E per variant, over fields bounded by the transition's guard. + assert!(ex.tla.contains("(LET step == [tag |-> \"Extend\", b |-> b__] IN next_step(step))")); + assert!(!ex.tla.contains("\\cup {[tag |-> \"Extend\""), "{}", ex.tla); + let Some(jar) = tla_tools() else { return }; + sany(&jar, &ex.spec()); + let run = tlc(&jar, &ex.spec(), &ex.cfg); + assert_eq!(run.violated, Vec::::new(), "{}", ex.tla); + assert_eq!(run.distinct, 144, "{run:?}\n{}", ex.tla); +} diff --git a/source/vir/src/tla.rs b/source/vir/src/tla.rs index 0fd54d042a..4ee967e2c0 100644 --- a/source/vir/src/tla.rs +++ b/source/vir/src/tla.rs @@ -5,7 +5,11 @@ //! function the triple reaches. It keys on nothing from any one project: //! datatypes become records, `vstd` collections become TLA+ sequences, sets //! and functions, spec functions become operators, and a quantifier is -//! bounded from its own guard. Whatever it cannot express it refuses with a +//! bounded from its own guard (`S.contains(x)`, `lo <= x < hi`, and +//! `S.contains(Ctor { f: x, .. })`, which ranges `x` over the `f`s of `S`'s +//! members built by `Ctor`). An `exists` over a step enum that a `match` +//! dispatches is one `\E` per variant, each field bounded from the guard of +//! the transition its arm calls. Whatever it cannot express it refuses with a //! source location, and whatever it cannot bound becomes a `CONSTANT` the //! model config must supply. Both lists come back in the [`Report`]. //! @@ -198,11 +202,19 @@ struct Env { /// Variables bound to a closure or record value, kept symbolically so a /// later application or field selection can be reduced. values: HashMap)>, + /// Locals bound (by `let` or a pattern) to a value that reads the post + /// state, so reading them reads primed variables. + primed: HashSet, } impl Env { fn new() -> Self { - Env { roles: HashMap::new(), names: HashMap::new(), values: HashMap::new() } + Env { + roles: HashMap::new(), + names: HashMap::new(), + values: HashMap::new(), + primed: HashSet::new(), + } } fn name(&self, v: &VarIdent) -> String { self.names.get(v).cloned().unwrap_or_else(|| ident_name(v)) @@ -213,6 +225,36 @@ impl Env { fn symbolic_only(&self, v: &VarIdent) -> bool { self.values.contains_key(v) && !self.names.contains_key(v) && !self.roles.contains_key(v) } + /// Whether `v` reads the post state: the post-role parameter, or a local + /// bound to something that reads it. + fn post_var(&self, v: &VarIdent) -> bool { + self.roles.get(v) == Some(&Role::Post) || self.primed.contains(v) + } + /// Whether `e` reads the post state (primed variables), directly or + /// through a call it passes the post state to. + fn reads_post(&self, e: &Expr) -> bool { + let mut found = false; + crate::ast_visitor::expr_visitor_walk(e, &mut |x: &Expr| { + match &x.x { + ExprX::Var(u) if self.post_var(u) => found = true, + ExprX::ReadPlace(p, _) if self.place_reads_post(p) => found = true, + _ => {} + } + crate::visitor::VisitorControlFlow::Recurse + }); + found + } + fn place_reads_post(&self, p: &Place) -> bool { + match &p.x { + PlaceX::Local(u) => self.post_var(u), + PlaceX::Field(_, inner) + | PlaceX::DerefMut(inner) + | PlaceX::ModeUnwrap(inner, _) + | PlaceX::UserDefinedTypInvariantObligation(inner, _) => self.place_reads_post(inner), + PlaceX::Index(inner, idx, ..) => self.place_reads_post(inner) || self.reads_post(idx), + PlaceX::Temporary(e) | PlaceX::WithExpr(e, _) => self.reads_post(e), + } + } } struct Exporter { @@ -304,6 +346,8 @@ struct Exporter { datatype_names: HashMap, datatype_names_taken: HashSet, current: String, + /// Whether the operators being emitted are the ones Init reaches. + in_init: bool, } fn ident_name(v: &VarIdent) -> String { @@ -605,6 +649,10 @@ fn vstd_op(name: &str) -> Option<&'static str> { ("set", "is_empty") => "set_is_empty", ("set", "ext_equal") => "ext_equal", ("set", "full") => "set_full", + // `Set::range(lo, hi)` and the `FiniteRange::range_set` it inlines + // to: the integers `lo <= i < hi`. + ("set", "range") | ("set", "range_set") => "set_range", + ("set", "range_inclusive") => "set_range_inclusive", ("map", "dom") => "map_dom", ("map", "index") | ("map", "spec_index") => "map_index", ("map", "insert") => "map_insert", @@ -1158,6 +1206,19 @@ impl Exporter { let msg = self.assert_message(a, env, 0); format!("(IF {sa} THEN {sb} ELSE Assert(FALSE, {msg}))") } + // A disjunction of two state predicates, outside what Init + // reaches: `IF a THEN TRUE ELSE b`, the same boolean. In an + // action TLC branches on a `\/` rather than evaluating it, so + // `b` would be evaluated even where `a` holds and guards it (`b + // == 0 || log[b - 1] == x` indexing `log[-1]`). Init keeps the + // `\/`, whose branches may assign the state. + ExprX::Logical(LogicalOp::Or, a, b) + if !self.in_init && !env.reads_post(a) && !env.reads_post(b) => + { + let sa = self.quiet(|x| x.expr(a, env)); + let sb = self.quiet(|x| x.expr(b, env)); + format!("(IF {sa} THEN TRUE ELSE {sb})") + } ExprX::Logical(op, a, b) => { let (sa, sb) = match op { LogicalOp::And => (self.expr(a, env), self.expr(b, env)), @@ -1565,6 +1626,11 @@ impl Exporter { let value = self.quiet(|x| x.place(init, &env2)); let before = env2.clone(); let n = self.bind_var(&mut env2, name); + if before.place_reads_post(init) { + env2.primed.insert(name.clone()); + } else { + env2.primed.remove(name); + } if let Some(v) = symbolic { env2.values.insert(name.clone(), (v, Box::new(before))); } @@ -1600,6 +1666,17 @@ impl Exporter { for arm in arms.iter() { let mut env2 = env.clone(); let (cond, lets) = self.pattern(&m, &arm.x.pattern, &mut env2); + // A binding of a scrutinee that reads the post state reads it too. + let scrutinee_primed = env.place_reads_post(place); + for v in env2.names.keys().cloned().collect::>() { + if env2.names.get(&v) != env.names.get(&v) { + if scrutinee_primed { + env2.primed.insert(v); + } else { + env2.primed.remove(&v); + } + } + } let in_lets = |x: String| { if lets.is_empty() { x } else { format!("(LET {} IN {x})", lets.join(" ")) } }; @@ -2121,6 +2198,24 @@ impl Exporter { "set_finite" => format!("IsFiniteSet({})", g!(0)), "set_is_empty" => format!("({} = {{}})", g!(0)), "set_full" => self.refuse("Set::full (unbounded)", &e.span), + // Only integers: a `char` is a string here, with no range. + "set_range" | "set_range_inclusive" + if args.len() == 2 + && matches!( + &*crate::ast_util::undecorate_typ(&args[0].typ), + TypX::Int(r) if !matches!(r, IntRange::Char) + ) => + { + let (lo, hi) = (g!(0), g!(1)); + if op == "set_range" { + format!("({lo})..(({hi}) - 1)") + } else { + format!("({lo})..({hi})") + } + } + "set_range" | "set_range_inclusive" => { + self.refuse("Set::range over a type other than an integer", &e.span) + } "ext_equal" => format!("({} = {})", g!(0), g!(1)), "map_dom" => format!("DOMAIN {}", g!(0)), "map_index" => format!("{}[{}]", g!(0), g!(1)), @@ -2166,6 +2261,11 @@ impl Exporter { for b in binders.iter() { self.bind_var(&mut env2, &b.name); } + if !forall && binders.len() == 1 { + if let Some(out) = self.exists_per_variant(e, &binders[0], body, &env2) { + return out; + } + } // The guard: the antecedent of an implication (forall) or the // conjuncts of the body, a single one included (exists). // Explicit triggers wrap the body; the guard is underneath. @@ -2212,6 +2312,350 @@ impl Exporter { out } + /// `exists|x: T| body` for a datatype `T` that `body` matches on, + /// directly or in the function it passes `x` to (`next_step(pre, post, + /// step)`): one `\E` per variant over its fields instead of one over the + /// union of every variant's values, each field bounded where the arm + /// that variant takes guards it, reading the arm's transition (`Grant + /// { v, c, .. } => t_grant(pre, post, v, c, ..)` bounds `v` by + /// `t_grant`'s `0 <= v < pre.n`). A field no guard bounds is bounded by + /// its type, or is a hole. None when `x` has a guard of its own or + /// `body` is not such a match. + fn exists_per_variant( + &mut self, + e: &Expr, + binder: &VarBinder, + body: &Expr, + env: &Env, + ) -> Option { + let x = &binder.name; + let TypX::Datatype(Dt::Path(path), targs, _) = &*crate::ast_util::undecorate_typ(&binder.a) + else { + return None; + }; + let d = self.datatypes.get(path)?.clone(); + if matches!(d.x.transparency, DatatypeTransparency::Never) + || d.x.typ_params.len() != targs.len() + || d.x.variants.is_empty() + { + return None; + } + let inner = peel(body); + let guards: Vec = conjuncts(&inner); + let unbound = [x.clone()]; + if self.quiet(|this| this.bound_from_guard(x, &binder.a, &unbound, &guards, env)).is_some() + { + return None; + } + // The match on `x`, and the scope its arms read. + let (arms, arm_env, arm_unbound) = self.match_on(&inner, x, env)?; + let tagged = d.x.variants.len() > 1; + let instance = self.constant_typ_name(&binder.a); + let sb = self.in_branch(body, env); + let xname = env.name(x); + // Per variant: its name, fields, field binders and body, and each + // field's bound (from a guard, or from its type with its size and the + // holes that bounding added). + let mut all = Vec::new(); + let mut field_bounds = Vec::new(); + for variant in d.x.variants.iter() { + if variant.name.to_string() == "dummy_to_use_type_params" { + continue; + } + let fields: Vec<(Ident, Typ)> = variant + .fields + .iter() + .map(|f| { + let t = crate::sst_util::subst_typ_for_datatype(&d.x.typ_params, targs, &f.a.0); + (f.name.clone(), t) + }) + .collect(); + // The guarded expression each field is a parameter of. + let site = arms.iter().find_map(|arm| { + let PatternX::Constructor(_, v, pbinders) = &arm.x.pattern.x else { return None }; + if v != &variant.name + || !matches!(arm.x.guard.x, ExprX::Const(Constant::Bool(true))) + { + return None; + } + let mut vars: HashMap = HashMap::new(); + for b in pbinders.iter() { + if let PatternX::Var(PatternBinding { name, .. }) = &b.a.x { + vars.insert(b.name.clone(), name.clone()); + } + } + Some((vars, arm.x.body.clone())) + }); + let names: Vec = + fields.iter().map(|(f, _)| self.bind(&format!("{}__", field_name(f)))).collect(); + let mut record = Vec::new(); + if tagged { + record.push(format!("tag |-> \"{}\"", variant.name)); + } + for ((f, _), n) in fields.iter().zip(&names) { + record.push(format!("{} |-> {n}", field_name(f))); + } + let record = if record.is_empty() { + "[tag |-> \"unit\"]".to_string() + } else { + format!("[{}]", record.join(", ")) + }; + let out = format!("(LET {xname} == {record} IN {sb})"); + let mut bounded = Vec::new(); + for k in 0..fields.len() { + let from_guard = site.as_ref().and_then(|(vars, arm_body)| { + self.field_bound(k, &fields, &names, vars, arm_body, &arm_env, &arm_unbound) + }); + bounded.push(match from_guard { + Some(d) => (Some((d, None)), 0..0), + None => { + let first = self.holes.len(); + let b = + self.bound_from_type(&fields[k].1, &e.span, &mut vec![path.clone()]); + (b.map(|(d, n)| (d, Some(n))), first..self.holes.len()) + } + }); + } + all.push((variant.name.clone(), fields, names, out)); + field_bounds.push(bounded); + } + // What a variant's type-bounded fields take together, counting + // only those of at most one value once it is split; a variant over + // the cap, or every variant when they are together, is split: each + // of its type-bounded fields of more than one value is a hole (as + // for a domain read off the type, [`Exporter::bound_variants`]). + type FieldBound = (Option<(String, Option)>, std::ops::Range); + let size = |bounded: &Vec, split: bool| { + bounded + .iter() + .filter_map(|(b, _)| match b { + Some((_, Some(n))) => Some(*n), + Some((_, None)) => None, + None => Some(1), + }) + .filter(|n| !split || *n <= 1) + .fold(1u128, |acc, n| acc.saturating_mul(n)) + }; + let mut split: Vec = + field_bounds.iter().map(|b| size(b, false) > MAX_TYPE_DOMAIN).collect(); + let union = field_bounds + .iter() + .zip(&split) + .fold(0u128, |acc, (b, s)| acc.saturating_add(size(b, *s))); + if union > MAX_TYPE_DOMAIN { + for (b, s) in field_bounds.iter().zip(split.iter_mut()) { + *s = *s || size(b, false) > 1; + } + } + for (bounded, s) in field_bounds.iter().zip(&split).rev() { + if !*s { + continue; + } + for (b, holes) in bounded.iter().rev() { + if matches!(b, Some((_, Some(n))) if *n > 1) { + self.drop_hole_range(holes.clone()); + } + } + } + let mut parts = Vec::new(); + for ((vname, fields, names, mut out), (bounded, s)) in + all.into_iter().zip(field_bounds.into_iter().zip(split)) + { + let mut domains = Vec::new(); + for ((f, ftyp), (b, _)) in fields.iter().zip(bounded) { + let domain = match b { + Some((d, None)) => d, + Some((d, Some(n))) if !s || n <= 1 => d, + _ => { + let constant = + format!("Dom_{instance}_{}_{}", sanitize(&vname), field_name(f)); + self.constants.insert(constant.clone()); + self.holes.push(Hole { + variable: format!("{vname}.{}", field_name(f)), + typ: typ_name(ftyp), + constant: constant.clone(), + location: span_string(&e.span), + in_function: self.current.clone(), + }); + constant + } + }; + domains.push(domain); + } + for (n, dom) in names.iter().zip(domains).rev() { + out = format!("(\\E {n} \\in {dom} : {out})"); + } + parts.push(out); + } + if parts.is_empty() { + return None; + } + Some(format!("({})", parts.join(" \\/ "))) + } + + /// The arms of the `match` on `x` that `e` is, or that the body of the + /// function `e` calls with `x` is, with the scope the arms read: the + /// callee's state parameters in the roles of the state arguments, its + /// other parameters (besides the one `x` fills) unbound. + fn match_on( + &mut self, + e: &Expr, + x: &VarIdent, + env: &Env, + ) -> Option<(Arms, Env, Vec)> { + let is_x = |p: &Place| place_var(p).as_ref() == Some(x) && matches!(p.x, PlaceX::Local(_)); + if let ExprX::Match(place, arms, _) = &e.x { + return is_x(place).then(|| (arms.clone(), env.clone(), vec![])); + } + let ExprX::Call { target: CallTarget::Fun(kind, fun, ..), args, .. } = &e.x else { + return None; + }; + let callee = self.functions.get(&self.resolved_fun(kind, fun))?.clone(); + let body = peel(callee.x.body.as_ref()?); + let ExprX::Match(place, arms, _) = &body.x else { return None }; + let scrutinee = place_var(place).filter(|_| matches!(place.x, PlaceX::Local(_)))?; + let mut callee_env = Env::new(); + let mut unbound = Vec::new(); + let mut found = false; + for (p, a) in callee.x.params.iter().zip(args.iter()) { + let arg = read_var(a); + if arg.as_ref() == Some(x) && p.x.name == scrutinee { + found = true; + } else if let Some(role) = arg.as_ref().and_then(|v| env.roles.get(v)) { + callee_env.roles.insert(p.x.name.clone(), *role); + } else { + unbound.push(p.x.name.clone()); + } + } + found.then_some((arms.clone(), callee_env, unbound)) + } + + /// The domain of field `k` of a variant read off the guard of the arm + /// body `arm_body` (or of the function it calls), where the field is + /// the pattern variable `vars[field]`: the fields before it are bound + /// (as `names`), the ones after it are not. The callee's `let`s that + /// read only bound names wrap the domain. + #[allow(clippy::too_many_arguments)] + fn field_bound( + &mut self, + k: usize, + fields: &[(Ident, Typ)], + names: &[String], + vars: &HashMap, + arm_body: &Expr, + arm_env: &Env, + arm_unbound: &[VarIdent], + ) -> Option { + let field_of: HashMap = fields + .iter() + .enumerate() + .filter_map(|(i, (f, _))| vars.get(f).map(|v| (v.clone(), i))) + .collect(); + let target = vars.get(&fields[k].0)?.clone(); + let arm_body = peel(arm_body); + // The expression whose guard bounds the field, in its scope: the + // arm's transition call (its parameters for the pattern variables), + // or the arm body itself. + let mut env = Env::new(); + let mut unbound: Vec = arm_unbound.to_vec(); + let (guarded, target) = match &arm_body.x { + ExprX::Call { target: CallTarget::Fun(kind, fun, ..), args, .. } => { + let callee = self.functions.get(&self.resolved_fun(kind, fun))?.clone(); + let mut target_param = None; + for (p, a) in callee.x.params.iter().zip(args.iter()) { + let arg = read_var(a); + match arg.as_ref().and_then(|v| field_of.get(v).map(|i| (v, *i))) { + Some((_, i)) if i < k => { + env.names.insert(p.x.name.clone(), names[i].clone()); + } + Some((v, i)) => { + if v == &target && i == k { + target_param = Some(p.x.name.clone()); + } + unbound.push(p.x.name.clone()); + } + None => match arg.as_ref().and_then(|v| arm_env.roles.get(v)) { + Some(role) => { + env.roles.insert(p.x.name.clone(), *role); + } + None => unbound.push(p.x.name.clone()), + }, + } + } + (callee.x.body.clone()?, target_param?) + } + _ => { + env = arm_env.clone(); + for (v, i) in &field_of { + if *i < k { + env.names.insert(v.clone(), names[*i].clone()); + } else { + unbound.push(v.clone()); + } + } + (arm_body.clone(), target) + } + }; + // Reading the post state in a bound would read a primed variable + // before the step assigns it. + unbound.extend(env.roles.iter().filter(|(_, r)| **r == Role::Post).map(|(v, _)| v.clone())); + // The body's `let`s, as far as they read only what is bound. + let mut lets = Vec::new(); + let mut e = guarded; + loop { + match &e.x { + ExprX::Block(stmts, Some(tail)) => { + for st in stmts.iter() { + let StmtX::Decl { pattern, init: Some(init), .. } = &st.x else { continue }; + let PatternX::Var(PatternBinding { name, .. }) = &pattern.x else { + continue; + }; + let reads_unbound = match &init.x { + PlaceX::Temporary(v) | PlaceX::WithExpr(v, _) => { + unbound.iter().any(|u| mentions(v, u)) + } + _ => place_var(init).map_or(true, |b| unbound.contains(&b)), + }; + if reads_unbound + || typ_has_specfn(&pattern.typ, &self.datatypes, &mut HashSet::new()) + { + unbound.push(name.clone()); + continue; + } + let value = self.quiet(|this| this.place(init, &env)); + let n = self.bind_var(&mut env, name); + lets.push(format!("{n} == {value}")); + } + e = tail.clone(); + } + _ => { + // Past parentheses, boxes and triggers, maybe to a block. + let p = peel(&e); + let more = matches!(&p.x, ExprX::Block(st, Some(_)) if !st.is_empty()); + e = p; + if !more { + break; + } + } + } + } + let guard = conjuncts(&e); + let typ = &fields[k].1; + let mut ordered = vec![target.clone()]; + ordered.extend(unbound.into_iter().filter(|u| u != &target)); + // The guard must bound the field on its own, but for the 0 below an + // unsigned type: a side taken from a type as wide as `u8` is left to + // the cap on domains read off a type. + let unsigned = matches!( + &*crate::ast_util::undecorate_typ(typ), + TypX::Int(IntRange::Nat | IntRange::U(_) | IntRange::USize) + ); + let open: Typ = Arc::new(TypX::Int(if unsigned { IntRange::Nat } else { IntRange::Int })); + self.quiet(|this| this.bound_from_guard(&target, &open, &ordered, &guard, &env))?; + let dom = self.quiet(|this| this.bound_from_guard(&target, typ, &ordered, &guard, &env))?; + Some(if lets.is_empty() { dom } else { format!("(LET {} IN {dom})", lets.join(" ")) }) + } + /// A finite domain from the type alone, with its number of elements: /// booleans, integer types of at most [`MAX_TYPE_DOMAIN`] values (`u8`, /// `i8`), and datatypes and tuples whose fields are themselves bounded. @@ -2451,6 +2895,35 @@ impl Exporter { } } + /// Where `v` sits in the constructor `e`: the steps from the value to + /// it, each the variant to test (for a datatype of several variants) + /// and the field (a record label, or a tuple's 0-based position). None + /// when `e` is not a constructor holding `v` as a field, directly or in + /// a nested constructor, or has an update tail. + fn ctor_path( + &self, + e: &Expr, + v: &VarIdent, + ) -> Option, Result)>> { + let e = peel(e); + let ExprX::Ctor(dt, variant, binders, None) = &e.x else { return None }; + let tag = (!self.single_variant(dt)).then(|| variant.to_string()); + for b in binders.iter() { + let field = match dt { + Dt::Tuple(_) => Err(b.name.parse::().ok()?), + Dt::Path(_) => Ok(field_name(&b.name)), + }; + if read_var(&b.a).as_ref() == Some(v) { + return Some(vec![(tag, field)]); + } + if let Some(mut rest) = self.ctor_path(&b.a, v) { + rest.insert(0, (tag, field)); + return Some(rest); + } + } + None + } + /// A finite domain for `v` read off the guard's conjuncts: membership in /// a set, a map's domain, or an integer range from inequalities and /// chained comparisons (through binders not yet bound: `0 <= a < b < n` @@ -2490,6 +2963,37 @@ impl Exporter { let (sv, i) = (self.bind("s__"), self.bind("i__")); format!("(LET {sv} == {s} IN {{{sv}[{i}] : {i} \\in 1..Len({sv})}})") } + // `S.contains(Ctor { f: v, .. })`, also nested + // (`Ctor { f: Inner { g: v, .. }, .. }`): `v` is the + // `f` of a member of `S` built by that constructor, so + // it ranges over those members' `f`s. + Some(op @ ("set_contains" | "map_contains_key")) + if args.len() == 2 && free(&args[0]) => + { + let Some(path) = self.ctor_path(&args[1], v) else { continue }; + let s = self.expr(&args[0], env); + let s = if op == "map_contains_key" { format!("DOMAIN {s}") } else { s }; + let m = self.bind("m__"); + let mut tests = Vec::new(); + let mut access = m.clone(); + for (tag, field) in &path { + if let Some(t) = tag { + tests.push(format!("{access}.tag = \"{t}\"")); + } + access = match field { + Ok(label) => format!("{access}.{label}"), + Err(idx) => format!("{access}[{}]", idx + 1), + }; + } + if tests.is_empty() { + format!("{{{access} : {m} \\in {s}}}") + } else { + let m2 = self.bind("m__"); + let filtered = format!("{{{m} \\in {s} : {}}}", tests.join(" /\\ ")); + let access2 = access.replacen(&m, &m2, 1); + format!("{{{access2} : {m2} \\in {filtered}}}") + } + } _ => continue, }; let x = self.bind("x__"); @@ -3808,6 +4312,7 @@ pub fn export_module(krate: &Krate, arg: &str) -> Result { datatype_names: HashMap::new(), datatype_names_taken: HashSet::new(), current: String::new(), + in_init: false, }; for v in &state_vars { ex.used_names.insert(v.clone()); @@ -3843,6 +4348,7 @@ pub fn export_module(krate: &Krate, arg: &str) -> Result { ex.implications.clear(); ex.pre_assigned.clear(); ex.conj_level = true; + ex.in_init = i == 0; let body = match &f.x.body { Some(b) => match &peel(b).x { ExprX::Closure(params, body) => { @@ -3869,6 +4375,7 @@ pub fn export_module(krate: &Krate, arg: &str) -> Result { if ex.current_tainted { ex.tainted.insert(key); } + ex.in_init = false; match i { 0 => init_name = name, 1 => next_name = name, @@ -3876,7 +4383,9 @@ pub fn export_module(krate: &Krate, arg: &str) -> Result { } } } else { + ex.in_init = true; init_name = ex.ensure_function(&(triple.init.clone(), Variant::Plain)); + ex.in_init = false; next_name = ex.ensure_function(&(triple.next.clone(), Variant::Plain)); // A predicate init or next reads, unprimed or primed, is a guard or helper of // the transition, not an invariant, unless the command line names From 744f1b6e27de570fc6e46fcf8180fba9bc6d08f0 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Sun, 27 Sep 2026 18:10:41 +0000 Subject: [PATCH 2/4] tla-export: a step field bounded only from an arm taking every value; range_inclusive holds hi The per-variant expansion of `exists|step: Step|` read a variant's field bounds from the first unguarded constructor arm naming the variant, even when an earlier arm (guarded, a wildcard, an or-pattern) caught the variant first or the arm refuted a field (`R { a: true, b }`). Values a later arm admits were then dropped with no hole or refusal. Now only the first arm that could match the variant is read, and only when it is unguarded, that variant's constructor, and binds each field plainly or with `_`; otherwise the fields fall back to their type or a hole. `Set::range_inclusive(lo, hi)` printed as `lo..hi`, but vstd's is `range_set(lo, hi).insert(hi)`, which holds `hi` even below `lo`: now `(lo..hi \cup {hi})`. Tests: the refutable, guarded and wildcard arms (9 states; 4 before), an Init disjunction keeping its `\/` (2 initial states) beside range_inclusive, and a constructor-field bound through a nested constructor, a tuple and a map's keys, with an invariant TLC must find violated. Co-Authored-By: Claude Opus 5.5 --- source/rust_verify_test/tests/tla_export.rs | 170 ++++++++++++++++++++ source/vir/src/tla.rs | 60 +++++-- 2 files changed, 214 insertions(+), 16 deletions(-) diff --git a/source/rust_verify_test/tests/tla_export.rs b/source/rust_verify_test/tests/tla_export.rs index 9276ead363..dc9a0ecaa3 100644 --- a/source/rust_verify_test/tests/tla_export.rs +++ b/source/rust_verify_test/tests/tla_export.rs @@ -2987,3 +2987,173 @@ fn tla_export_bounds_message_fields_and_step_fields_from_their_guards() { assert_eq!(run.violated, Vec::::new(), "{}", ex.tla); assert_eq!(run.distinct, 144, "{run:?}\n{}", ex.tla); } + +/// Step fields are bounded from the guard of the arm a variant's values +/// take, and only when that arm takes all of them: the first arm that could +/// match the variant, unguarded, and binding each field plainly. Here an arm +/// refuting a field (`R { a: true, b }`), a guarded arm (`G { b } if b > 0`) +/// and a guarded wildcard each leave some values to a later arm, whose +/// guard (`b < 1`, `b < 0`) would drop `x = 21, 22, 31, 32, 50`. The nine +/// states are 0 and the eight values the arms reach (`t60` is unreachable). +const ARMS: &str = r#" +use vstd::prelude::*; +verus! { +pub struct State { pub x: int } + +pub open spec fn init(s: State) -> bool { s.x == 0 } + +pub open spec fn t10(pre: State, post: State, b: u8) -> bool { + &&& b < 1 &&& pre.x == 0 &&& post == State { x: 10 + b } +} +pub open spec fn t20(pre: State, post: State, b: u8) -> bool { + &&& b < 3 &&& pre.x == 0 &&& post == State { x: 20 + b } +} +pub open spec fn t30(pre: State, post: State, b: u8) -> bool { + &&& b < 3 &&& pre.x == 0 &&& post == State { x: 30 + b } +} +pub open spec fn t40(pre: State, post: State, b: u8) -> bool { + &&& b < 1 &&& pre.x == 0 &&& post == State { x: 40 + b } +} +pub open spec fn t60(pre: State, post: State, b: u8) -> bool { + &&& b < 0 &&& pre.x == 0 &&& post == State { x: 60 + b } +} + +pub enum Step { R { a: bool, b: u8 }, G { b: u8 }, W { b: u8 } } + +pub open spec fn next_step(pre: State, post: State, step: Step) -> bool { + match step { + Step::R { a: true, b } => t10(pre, post, b), + Step::R { a, b } => t20(pre, post, b), + Step::G { b } if b > 0 => t30(pre, post, b), + Step::G { b } => t40(pre, post, b), + _ if step is W => pre.x == 0 && post == State { x: 50 }, + Step::W { b } => t60(pre, post, b), + } +} + +pub open spec fn next(pre: State, post: State) -> bool { + exists|step: Step| next_step(pre, post, step) +} + +pub open spec fn small(s: State) -> bool { s.x <= 60 } +} +"#; + +#[test] +fn tla_export_bounds_a_step_field_only_from_an_arm_taking_every_value() { + let ex = export_code(ARMS, "test_crate"); + assert_eq!(ex.report["refusals"], serde_json::json!([]), "{}", ex.tla); + assert_eq!(ex.report["holes"], serde_json::json!([]), "{}", ex.tla); + // Each variant's `b` is read off its type: no arm bounds it alone. + assert!(!ex.tla.contains("\\in 0..(1) - 1"), "{}", ex.tla); + assert!(!ex.tla.contains("\\in 0..(0) - 1"), "{}", ex.tla); + let Some(jar) = tla_tools() else { return }; + sany(&jar, &ex.spec()); + let run = tlc(&jar, &ex.spec(), &ex.cfg); + assert_eq!(run.violated, Vec::::new(), "{}", ex.tla); + assert_eq!(run.distinct, 9, "{run:?}\n{}", ex.tla); +} + +/// A disjunction Init reaches keeps its `\/`, which TLC branches on to +/// assign the state (two initial states), while the same disjunction in an +/// action is evaluated. `Set::range_inclusive(lo, hi)` holds `hi` even below +/// `lo`, as vstd's `range_set(lo, hi).insert(hi)` does. +const INIT_OR: &str = r#" +use vstd::prelude::*; +verus! { +pub struct State { pub x: int, pub y: int } + +pub open spec fn init(s: State) -> bool { + &&& s.x == 0 || s.x == 1 + &&& s.y == 0 +} + +pub open spec fn next(pre: State, post: State) -> bool { + &&& pre.x == 0 || pre.x == 5 + &&& pre.y < 1 + &&& post == State { y: pre.y + 1, ..pre } +} + +pub open spec fn inclusive(s: State) -> bool { + &&& Set::::range_inclusive(3, 1).contains(1) + &&& !Set::::range_inclusive(3, 1).contains(3) + &&& Set::::range_inclusive(0, s.y).contains(s.y) +} +} +"#; + +#[test] +fn tla_export_keeps_a_disjunction_init_reaches() { + let ex = export_code(INIT_OR, "test_crate"); + assert_eq!(ex.report["refusals"], serde_json::json!([]), "{}", ex.tla); + assert_eq!(ex.report["holes"], serde_json::json!([]), "{}", ex.tla); + assert!(ex.tla.contains("(x = 0) \\/ (x = 1)"), "{}", ex.tla); + assert!(ex.tla.contains("(IF (x = 0) THEN TRUE ELSE (x = 5))"), "{}", ex.tla); + let Some(jar) = tla_tools() else { return }; + sany(&jar, &ex.spec()); + let out = tlc_output(&jar, &ex.spec(), &ex.cfg); + assert!(out.contains("2 distinct states generated"), "{}", out); + let run = tlc(&jar, &ex.spec(), &ex.cfg); + assert_eq!(run.violated, Vec::::new(), "{}", ex.tla); + // (0, 0), (1, 0) and (0, 1): the `x = 1` state takes no step. + assert_eq!(run.distinct, 3, "{run:?}\n{}", ex.tla); +} + +/// A binder that is a field of a constructor in a membership guard ranges +/// over that field of the members, through a nested constructor (with a +/// tag test at each level of several variants), a tuple, and a map's keys. +/// `wrong` holds of no member, so TLC must find it violated: the bound is +/// not empty. +const CTOR_FIELDS: &str = r#" +use vstd::prelude::*; +verus! { +pub enum Inner { A { v: int }, B } +pub enum Msg { Wrap { inner: Inner, t: (int, int) }, Other } + +pub struct State { pub net: Set, pub m: Map, pub k: int } + +pub open spec fn init(s: State) -> bool { + &&& s.net == Set::::empty().insert(Msg::Wrap { inner: Inner::A { v: 1 }, t: (2, 3) }) + .insert(Msg::Wrap { inner: Inner::B, t: (7, 7) }).insert(Msg::Other) + &&& s.m == Map::::empty().insert(Msg::Wrap { inner: Inner::A { v: 4 }, t: (5, 6) }, true) + &&& s.k == 0 +} + +pub open spec fn next(pre: State, post: State) -> bool { + &&& pre.k < 2 + &&& post == State { k: pre.k + 1, ..pre } +} + +pub open spec fn nested(s: State) -> bool { + forall|v: int, a: int, b: int| #[trigger] s.net.contains(Msg::Wrap { inner: Inner::A { v }, t: (a, b) }) + ==> v == 1 && a == 2 && b == 3 +} + +pub open spec fn keyed(s: State) -> bool { + forall|v: int, a: int, b: int| #[trigger] s.m.contains_key(Msg::Wrap { inner: Inner::A { v }, t: (a, b) }) + ==> v == 4 && a + b == 11 +} + +pub open spec fn wrong(s: State) -> bool { + forall|v: int, a: int, b: int| #[trigger] s.net.contains(Msg::Wrap { inner: Inner::A { v }, t: (a, b) }) + ==> v != 1 +} +} +"#; + +#[test] +fn tla_export_bounds_a_nested_tuple_and_map_key_constructor_field() { + let ex = export_code(CTOR_FIELDS, "test_crate"); + assert_eq!(ex.report["refusals"], serde_json::json!([]), "{}", ex.tla); + assert_eq!(ex.report["holes"], serde_json::json!([]), "{}", ex.tla); + assert!(ex.tla.contains(".inner.tag = \"A\""), "{}", ex.tla); + assert!(ex.tla.contains(".inner.v : m__"), "{}", ex.tla); + assert!(ex.tla.contains(".t[2] : m__"), "{}", ex.tla); + assert!(ex.tla.contains("\\in DOMAIN m : "), "{}", ex.tla); + let Some(jar) = tla_tools() else { return }; + sany(&jar, &ex.spec()); + let run = tlc(&jar, &ex.spec(), &ex.cfg); + // In each of the three states (`-continue`). + assert_eq!(run.violated, ["wrong", "wrong", "wrong"], "{}", ex.tla); + assert_eq!(run.distinct, 3, "{run:?}\n{}", ex.tla); +} diff --git a/source/vir/src/tla.rs b/source/vir/src/tla.rs index 4ee967e2c0..d56f1cd551 100644 --- a/source/vir/src/tla.rs +++ b/source/vir/src/tla.rs @@ -2210,7 +2210,9 @@ impl Exporter { if op == "set_range" { format!("({lo})..(({hi}) - 1)") } else { - format!("({lo})..({hi})") + // vstd's `range_set(lo, hi).insert(hi)`: `hi` even when + // it is below `lo`. + format!("(({lo})..({hi}) \\cup {{{hi}}})") } } "set_range" | "set_range_inclusive" => { @@ -2370,22 +2372,36 @@ impl Exporter { (f.name.clone(), t) }) .collect(); - // The guarded expression each field is a parameter of. - let site = arms.iter().find_map(|arm| { - let PatternX::Constructor(_, v, pbinders) = &arm.x.pattern.x else { return None }; - if v != &variant.name - || !matches!(arm.x.guard.x, ExprX::Const(Constant::Bool(true))) - { - return None; - } - let mut vars: HashMap = HashMap::new(); - for b in pbinders.iter() { - if let PatternX::Var(PatternBinding { name, .. }) = &b.a.x { - vars.insert(b.name.clone(), name.clone()); + // The guarded expression each field is a parameter of: the body + // of the first arm that could match the variant, when that arm + // takes every value of it (unguarded, the variant's constructor, + // and each field a plain binding or `_`). An arm that takes only + // some (`S { a: true, b }`, `S { b, .. } if b > 0`) leaves the + // rest to later arms, whose guards may admit more. + let site = arms + .iter() + .find(|arm| pattern_could_match(&arm.x.pattern, &variant.name)) + .and_then(|arm| { + let PatternX::Constructor(_, v, pbinders) = &arm.x.pattern.x else { + return None; + }; + if v != &variant.name + || !matches!(arm.x.guard.x, ExprX::Const(Constant::Bool(true))) + { + return None; } - } - Some((vars, arm.x.body.clone())) - }); + let mut vars: HashMap = HashMap::new(); + for b in pbinders.iter() { + match &b.a.x { + PatternX::Var(PatternBinding { name, .. }) => { + vars.insert(b.name.clone(), name.clone()); + } + PatternX::Wildcard(_) => {} + _ => return None, + } + } + Some((vars, arm.x.body.clone())) + }); let names: Vec = fields.iter().map(|(f, _)| self.bind(&format!("{}__", field_name(f)))).collect(); let mut record = Vec::new(); @@ -3831,6 +3847,18 @@ fn reached_functions(functions: &HashMap, root: &Fun) -> HashSet< seen } +/// Whether a pattern could match a value built by `variant`: only a +/// constructor of another variant is sure not to. +fn pattern_could_match(p: &Pattern, variant: &Ident) -> bool { + match &p.x { + PatternX::Constructor(_, v, _) => v == variant, + PatternX::Binding { sub_pat, .. } => pattern_could_match(sub_pat, variant), + PatternX::Or(a, b) => pattern_could_match(a, variant) || pattern_could_match(b, variant), + PatternX::MutRef(inner) | PatternX::ImmutRef(inner) => pattern_could_match(inner, variant), + PatternX::Wildcard(_) | PatternX::Var(_) | PatternX::Expr(_) | PatternX::Range(..) => true, + } +} + /// Whether a pattern binds a name anywhere in it. fn pattern_binds(p: &Pattern) -> bool { match &p.x { From da11dc1005700644d2c2405b9ae4d0716b21bd28 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Sun, 27 Sep 2026 19:12:07 +0000 Subject: [PATCH 3/4] tla-export: a disjunction over a post-state argument keeps its \/; step-field domains never read the step The `IF a THEN TRUE ELSE b` rewrite of a state-predicate disjunction broke TLC assigning a primed variable through a helper's parameter: `pick(post.x)` with `pick(v) = v == 0 || v == 1` became `IF v = 0 ...` on an unassigned `x'`. A call passing a post-reading argument to a non-state parameter now goes to the operator's `_postarg` variant (the OpKey carries the bit), whose parameters read the post state, so its disjunctions keep `\/`; a parameter a reduced application (`bind_args`) binds to a post-reading value does too. The record variant stays one operator per recursive function and reads its parameters that way always, as main did. A step field's domain read off its arm's guard sits outside the `LET` that binds the step, but the step binder and the callee's scrutinee parameter were not unbound, so `b < size(step)` printed `0..size(step) - 1` there. They are now unbound, as is every local a destructuring or valueless `let` binds (its names printed raw before, possibly as a state variable). Tests: `tla_export_keeps_a_disjunction_over_the_post_state` (a helper given `post.x`, a `let` of `post.z` and a match on `post.o`: 9 states) and `tla_export_bounds_a_step_field_whose_guard_reads_the_step` (callee and inline match: 7 states). The toyDB export is byte for byte unchanged. Co-Authored-By: Claude Opus 5.5 --- source/rust_verify_test/tests/tla_export.rs | 99 +++++++++++++++++++ source/vir/src/tla.rs | 101 +++++++++++++++----- 2 files changed, 178 insertions(+), 22 deletions(-) diff --git a/source/rust_verify_test/tests/tla_export.rs b/source/rust_verify_test/tests/tla_export.rs index dc9a0ecaa3..30d572f243 100644 --- a/source/rust_verify_test/tests/tla_export.rs +++ b/source/rust_verify_test/tests/tla_export.rs @@ -3157,3 +3157,102 @@ fn tla_export_bounds_a_nested_tuple_and_map_key_constructor_field() { assert_eq!(run.violated, ["wrong", "wrong", "wrong"], "{}", ex.tla); assert_eq!(run.distinct, 3, "{run:?}\n{}", ex.tla); } + +/// A disjunction over a value read in the post state keeps its `\/`, whose +/// branches TLC assigns the primed variable from: through a helper given +/// `post.x` (its own operator, whose parameter reads the post state), a +/// `let` bound to `post.z`, and a match on `post.o`. The same helper given a +/// pre-state value is evaluated. Nine states: the initial one, then two +/// values of `x` and two of `z` after each of the two steps. +const PRIMED_OR: &str = r#" +use vstd::prelude::*; +verus! { +pub struct State { pub x: int, pub y: int, pub z: int, pub o: Option } + +pub open spec fn init(s: State) -> bool { + &&& s.x == 0 &&& s.y == 0 &&& s.z == 0 &&& s.o == Option::::None +} + +pub open spec fn pick(v: int) -> bool { v == 0 || v == 1 } + +pub open spec fn next(pre: State, post: State) -> bool { + &&& pre.y < 2 + &&& pick(pre.x) + &&& post.y == pre.y + 1 + &&& post.o == Option::::Some(pre.y) + &&& pick(post.x) + &&& { let h = post.z; h == 0 || h == 2 } + &&& match post.o { Option::Some(v) => v == 0 || v >= 1, Option::None => false } +} + +pub open spec fn small(s: State) -> bool { s.x <= 1 && s.z <= 2 } +} +"#; + +#[test] +fn tla_export_keeps_a_disjunction_over_the_post_state() { + let ex = export_code(PRIMED_OR, "test_crate"); + assert_eq!(ex.report["refusals"], serde_json::json!([]), "{}", ex.tla); + assert_eq!(ex.report["holes"], serde_json::json!([]), "{}", ex.tla); + assert!(ex.tla.contains("pick(v) ==\n (IF (v = 0) THEN TRUE ELSE (v = 1))"), "{}", ex.tla); + assert!(ex.tla.contains("pick_postarg(v) ==\n ((v = 0) \\/ (v = 1))"), "{}", ex.tla); + assert!(ex.tla.contains("pick(x)"), "{}", ex.tla); + assert!(ex.tla.contains("pick_postarg(x')"), "{}", ex.tla); + assert!(ex.tla.contains("((h = 0) \\/ (h = 2))"), "{}", ex.tla); + assert!(ex.tla.contains("((v = 0) \\/ (v >= 1))"), "{}", ex.tla); + let Some(jar) = tla_tools() else { return }; + sany(&jar, &ex.spec()); + let run = tlc(&jar, &ex.spec(), &ex.cfg); + assert_eq!(run.violated, Vec::::new(), "{}", ex.tla); + assert_eq!(run.distinct, 9, "{run:?}\n{}", ex.tla); +} + +/// A step field whose guard reads the step value itself (`b < size(step)`) +/// is not bounded from it: the domain sits outside the `LET` binding the +/// step. It is bounded by its type (`u8`) instead, in the callee's match and +/// in a match written inline in the `exists`. `x` runs 0..6. +const STEP_GUARD: &str = r#" +use vstd::prelude::*; +verus! { +pub struct State { pub x: int } + +pub enum Step { A { b: u8 }, B { c: int } } + +pub open spec fn size(s: Step) -> int { match s { Step::A { .. } => 3, Step::B { .. } => 2 } } + +pub open spec fn init(s: State) -> bool { s.x == 0 } + +pub open spec fn next_step(pre: State, post: State, step: Step) -> bool { + match step { + Step::A { b } => b < size(step) && pre.x < 5 && post.x == pre.x + b, + Step::B { c } => 0 <= c < 2 && pre.x < 5 && post.x == pre.x + c, + } +} + +pub open spec fn next(pre: State, post: State) -> bool { + ||| exists|step: Step| next_step(pre, post, step) + ||| exists|st: Step| #![trigger size(st)] match st { + Step::A { b } => b < size(st) && pre.x < 4 && post.x == pre.x + b, + Step::B { c } => 0 <= c < 2 && pre.x < 4 && post.x == pre.x + c, + } +} + +pub open spec fn small(s: State) -> bool { s.x <= 6 } +} +"#; + +#[test] +fn tla_export_bounds_a_step_field_whose_guard_reads_the_step() { + let ex = export_code(STEP_GUARD, "test_crate"); + assert_eq!(ex.report["refusals"], serde_json::json!([]), "{}", ex.tla); + assert_eq!(ex.report["holes"], serde_json::json!([]), "{}", ex.tla); + assert!(!ex.tla.contains("(size(step)) - 1"), "{}", ex.tla); + assert!(!ex.tla.contains("(size(st)) - 1"), "{}", ex.tla); + assert!(ex.tla.contains("\\E b__ \\in 0..255 : (LET step =="), "{}", ex.tla); + assert!(ex.tla.contains("\\in 0..255 : (LET st =="), "{}", ex.tla); + let Some(jar) = tla_tools() else { return }; + sany(&jar, &ex.spec()); + let run = tlc(&jar, &ex.spec(), &ex.cfg); + assert_eq!(run.violated, Vec::::new(), "{}", ex.tla); + assert_eq!(run.distinct, 7, "{run:?}\n{}", ex.tla); +} diff --git a/source/vir/src/tla.rs b/source/vir/src/tla.rs index d56f1cd551..b84b8bd40b 100644 --- a/source/vir/src/tla.rs +++ b/source/vir/src/tla.rs @@ -167,8 +167,14 @@ struct Call { context: BTreeSet, } -/// An operator: a function, and which of its variants (see [`Variant`]). -type OpKey = (Fun, Variant); +/// An operator: a function, which of its variants (see [`Variant`]), and +/// whether a call gives it an argument that reads the post state. Its +/// parameters then read the post state too, so a disjunction over them keeps +/// its `\/`, whose branches TLC may need to assign a primed variable +/// (`pick(post.x)` with `pick(v) = v == 0 || v == 1`). The record variant +/// is always `false`: a recursive function has that one operator, whose +/// parameters are all read as the post state may be. +type OpKey = (Fun, Variant, bool); /// How an operator reads its state parameters. #[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)] @@ -800,7 +806,7 @@ impl Exporter { if let Some(n) = self.op_names.get(key) { return n.clone(); } - let (fun, variant) = key; + let (fun, variant, post_args) = key; let friendly = fun_as_friendly_rust_name(fun); let segs: Vec<&str> = friendly.split("::").collect(); let mut candidate = ident_name(&VarIdent( @@ -812,6 +818,9 @@ impl Exporter { Variant::Primed => candidate = format!("{candidate}_post"), Variant::Record => candidate = format!("{candidate}_rec"), } + if *post_args { + candidate = format!("{candidate}_postarg"); + } let taken = |this: &Self, c: &str| { this.used_names.contains(c) || this.locals_ever.contains(c) @@ -1112,7 +1121,7 @@ impl Exporter { } ExprX::VarAt(..) => self.refuse("old(...) reference", &e.span), ExprX::ConstVar(fun, _) | ExprX::StaticVar(fun) => { - self.ensure_function(&(fun.clone(), Variant::Plain)) + self.ensure_function(&(fun.clone(), Variant::Plain, false)) } ExprX::ReadPlace(place, _) => self.place(place, env), ExprX::Call { target, args, .. } => self.call(e, target, args, env), @@ -1211,7 +1220,9 @@ impl Exporter { // action TLC branches on a `\/` rather than evaluating it, so // `b` would be evaluated even where `a` holds and guards it (`b // == 0 || log[b - 1] == x` indexing `log[-1]`). Init keeps the - // `\/`, whose branches may assign the state. + // `\/`, whose branches may assign the state, as does a + // disjunction reading a local or parameter given a post-state + // value (see [`OpKey`]). ExprX::Logical(LogicalOp::Or, a, b) if !self.in_init && !env.reads_post(a) && !env.reads_post(b) => { @@ -1885,7 +1896,7 @@ impl Exporter { { let printed: Vec = args.iter().map(|a| self.expr(a, env)).collect(); self.conj_level = level; - let name = self.ensure_function(&(fun.clone(), Variant::Record)); + let name = self.ensure_function(&(fun.clone(), Variant::Record, false)); return format!("{name}({})", printed.join(", ")); } // Every state argument fits its role (checked above): it is @@ -1893,15 +1904,19 @@ impl Exporter { // selects the primed variant. let mut printed = Vec::new(); let mut variant = Variant::Plain; + let mut post_args = false; for (i, a) in args.iter().enumerate() { match (roles.get(i).copied().flatten(), arg_role(a)) { (Some(Role::Pre), Some(Role::Post)) => variant = Variant::Primed, (Some(_), _) => {} - (None, _) => printed.push(self.expr(a, env)), + (None, _) => { + post_args |= env.reads_post(a); + printed.push(self.expr(a, env)); + } } } self.conj_level = level; - let name = self.ensure_function(&(fun.clone(), variant)); + let name = self.ensure_function(&(fun.clone(), variant, post_args)); if printed.is_empty() { name } else { format!("{name}({})", printed.join(", ")) } } CallTarget::FnSpec(f) => { @@ -1960,10 +1975,17 @@ impl Exporter { for ((name, typ), a) in params.zip(args.iter()) { if let Some(role) = read_var(a).and_then(|v| env.roles.get(&v).copied()) { env2.roles.insert(name.clone(), role); + env2.primed.remove(&name); continue; } env2.roles.remove(&name); env2.names.remove(&name); + // A parameter given a value that reads the post state reads it. + if env.reads_post(a) { + env2.primed.insert(name.clone()); + } else { + env2.primed.remove(&name); + } env2.values.insert(name.clone(), (peel(a), Box::new(env.clone()))); if !typ_has_specfn(&typ, &self.datatypes, &mut HashSet::new()) { let value = self.expr(a, env); @@ -2512,7 +2534,9 @@ impl Exporter { /// The arms of the `match` on `x` that `e` is, or that the body of the /// function `e` calls with `x` is, with the scope the arms read: the /// callee's state parameters in the roles of the state arguments, its - /// other parameters (besides the one `x` fills) unbound. + /// other parameters unbound. The scrutinee (`x`, or the parameter it + /// fills) is unbound too: a field's domain sits outside the `LET` that + /// binds it. fn match_on( &mut self, e: &Expr, @@ -2521,7 +2545,7 @@ impl Exporter { ) -> Option<(Arms, Env, Vec)> { let is_x = |p: &Place| place_var(p).as_ref() == Some(x) && matches!(p.x, PlaceX::Local(_)); if let ExprX::Match(place, arms, _) = &e.x { - return is_x(place).then(|| (arms.clone(), env.clone(), vec![])); + return is_x(place).then(|| (arms.clone(), env.clone(), vec![x.clone()])); } let ExprX::Call { target: CallTarget::Fun(kind, fun, ..), args, .. } = &e.x else { return None; @@ -2537,6 +2561,7 @@ impl Exporter { let arg = read_var(a); if arg.as_ref() == Some(x) && p.x.name == scrutinee { found = true; + unbound.push(p.x.name.clone()); } else if let Some(role) = arg.as_ref().and_then(|v| env.roles.get(v)) { callee_env.roles.insert(p.x.name.clone(), *role); } else { @@ -2622,8 +2647,14 @@ impl Exporter { match &e.x { ExprX::Block(stmts, Some(tail)) => { for st in stmts.iter() { - let StmtX::Decl { pattern, init: Some(init), .. } = &st.x else { continue }; - let PatternX::Var(PatternBinding { name, .. }) = &pattern.x else { + let StmtX::Decl { pattern, init, .. } = &st.x else { continue }; + // A local this does not bind (a destructuring `let`, + // or one with no value) is not in scope of the + // domain: a guard reading it bounds nothing. + let (PatternX::Var(PatternBinding { name, .. }), Some(init)) = + (&pattern.x, init) + else { + pattern_names(pattern, &mut unbound); continue; }; let reads_unbound = match &init.x { @@ -3365,7 +3396,7 @@ impl Exporter { self.assign_through_call(key, reach); return name; } - let (fun, variant) = key; + let (fun, variant, post_args) = key; let Some(f) = self.functions.get(fun).cloned() else { return name }; self.emitting.insert(key.clone()); let previous = std::mem::replace(&mut self.current, fun_as_friendly_rust_name(fun)); @@ -3396,6 +3427,11 @@ impl Exporter { None => { let n = self.bind_var(&mut env, &p.x.name); params.push(n); + // The record variant is one operator for every call, + // some of which may pass the post state. + if *post_args || *variant == Variant::Record { + env.primed.insert(p.x.name.clone()); + } } } } @@ -3411,7 +3447,7 @@ impl Exporter { None => env.name(&p.x.name), }) .collect(); - let rec = self.ensure_function(&(fun.clone(), Variant::Record)); + let rec = self.ensure_function(&(fun.clone(), Variant::Record, false)); format!("{rec}({})", args.join(", ")) } else { match &f.x.body { @@ -3423,7 +3459,7 @@ impl Exporter { if params.is_empty() { name.clone() } else { format!("{name}({})", params.join(", ")) }; let mut def = String::new(); def.push_str(&format!( - "\\* {}{}, {}\n", + "\\* {}{}{}, {}\n", fun_as_friendly_rust_name(fun), match variant { Variant::Plain if !f.x.decrease.is_empty() => " (applies the record variant)", @@ -3431,6 +3467,7 @@ impl Exporter { Variant::Primed => " (read in the post state)", Variant::Record => " (the state passed as a record)", }, + if *post_args { " (given an argument read in the post state)" } else { "" }, span_string(&f.span) )); self.arity.insert(name.clone(), params.len()); @@ -3859,6 +3896,26 @@ fn pattern_could_match(p: &Pattern, variant: &Ident) -> bool { } } +/// The names a pattern binds, pushed onto `out`. +fn pattern_names(p: &Pattern, out: &mut Vec) { + match &p.x { + PatternX::Var(b) => out.push(b.name.clone()), + PatternX::Binding { binding, sub_pat } => { + out.push(binding.name.clone()); + pattern_names(sub_pat, out); + } + PatternX::Wildcard(_) | PatternX::Expr(_) | PatternX::Range(..) => {} + PatternX::Constructor(_, _, binders) => { + binders.iter().for_each(|b| pattern_names(&b.a, out)); + } + PatternX::Or(a, b) => { + pattern_names(a, out); + pattern_names(b, out); + } + PatternX::MutRef(inner) | PatternX::ImmutRef(inner) => pattern_names(inner, out), + } +} + /// Whether a pattern binds a name anywhere in it. fn pattern_binds(p: &Pattern) -> bool { match &p.x { @@ -4364,7 +4421,7 @@ pub fn export_module(krate: &Krate, arg: &str) -> Result { if verus_tla { for (i, r) in roots.iter().enumerate() { let f = ex.functions.get(r).cloned().ok_or("root missing")?; - let key = (r.clone(), Variant::Plain); + let key = (r.clone(), Variant::Plain, false); let name = ex.op_name(&key); ex.current = fun_as_friendly_rust_name(r); ex.bound.clear(); @@ -4412,20 +4469,20 @@ pub fn export_module(krate: &Krate, arg: &str) -> Result { } } else { ex.in_init = true; - init_name = ex.ensure_function(&(triple.init.clone(), Variant::Plain)); + init_name = ex.ensure_function(&(triple.init.clone(), Variant::Plain, false)); ex.in_init = false; - next_name = ex.ensure_function(&(triple.next.clone(), Variant::Plain)); + next_name = ex.ensure_function(&(triple.next.clone(), Variant::Plain, false)); // A predicate init or next reads, unprimed or primed, is a guard or helper of // the transition, not an invariant, unless the command line names // it; it is reported as excluded, never dropped silently. let transitions: HashSet = ex.emitted.clone(); for r in &selected { - let key = (r.clone(), Variant::Plain); + let key = (r.clone(), Variant::Plain, false); // Read primed (`p(post)` in next), or given a state value, is a // guard too. let reached = [Variant::Plain, Variant::Primed, Variant::Record] .iter() - .any(|v| transitions.contains(&(r.clone(), *v))); + .any(|v| [false, true].iter().any(|p| transitions.contains(&(r.clone(), *v, *p)))); if !triple.explicit && reached { outcome.insert( r.clone(), @@ -4489,7 +4546,7 @@ pub fn export_module(krate: &Krate, arg: &str) -> Result { } invs.retain(|(f, _, _)| !helpers.contains(f)); } - let transitions = ex.transitions(&(triple.next.clone(), Variant::Plain)); + let transitions = ex.transitions(&(triple.next.clone(), Variant::Plain, false)); let init_unassigned = match ex.functions.get(&triple.init).and_then(|f| f.x.body.clone()) { // verus-tla: the initial predicate is the body of the closure `init()` // returns, over its one parameter. @@ -4528,7 +4585,7 @@ pub fn export_module(krate: &Krate, arg: &str) -> Result { outcome.get(f).cloned().unwrap_or_else(|| (*selected, reason.clone())); Candidate { function: fun_as_friendly_rust_name(f), - operator: ex.op_names.get(&(f.clone(), Variant::Plain)).cloned(), + operator: ex.op_names.get(&(f.clone(), Variant::Plain, false)).cloned(), included, reason, } From 90253e37f62d71dc88351501413cc2f023672aa3 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Sun, 27 Sep 2026 19:23:42 +0000 Subject: [PATCH 4/4] tla-export: a local kept as a closure that captures the post state reads it A disjunction of that closure's applications keeps its \/ so TLC can assign through it, instead of becoming IF .. THEN TRUE ELSE .., which stopped TLC on an undefined primed variable. Co-Authored-By: Claude Opus 5.5 --- source/rust_verify_test/tests/tla_export.rs | 39 +++++++++++++++++++++ source/vir/src/tla.rs | 10 ++++-- 2 files changed, 46 insertions(+), 3 deletions(-) diff --git a/source/rust_verify_test/tests/tla_export.rs b/source/rust_verify_test/tests/tla_export.rs index 30d572f243..ece093aae1 100644 --- a/source/rust_verify_test/tests/tla_export.rs +++ b/source/rust_verify_test/tests/tla_export.rs @@ -3207,6 +3207,45 @@ fn tla_export_keeps_a_disjunction_over_the_post_state() { assert_eq!(run.distinct, 9, "{run:?}\n{}", ex.tla); } +/// A closure, or a record of closures, that captures the post state reads +/// it: a disjunction of its applications keeps its `\/`, whose branches +/// assign `x'`. From `y = 0` the steps take `x` to `y` or `y + 10`. +const CLOSURE_OR: &str = r#" +use vstd::prelude::*; +verus! { +pub struct State { pub x: int, pub y: int } + +pub struct Pair { pub f: spec_fn(int) -> bool } + +pub open spec fn init(s: State) -> bool { s.x == 0 && s.y == 0 } + +pub open spec fn next(pre: State, post: State) -> bool { + let f = |v: int| post.x == v; + let p = Pair { f: |v: int| post.x == v }; + &&& pre.y < 3 + &&& post.y == pre.y + 1 + &&& (f(pre.y) || f(pre.y + 10)) + &&& ((p.f)(pre.y) || (p.f)(pre.y + 10)) +} + +pub open spec fn small(s: State) -> bool { s.y <= 3 } +} +"#; + +#[test] +fn tla_export_keeps_a_disjunction_over_a_closure_reading_the_post_state() { + let ex = export_code(CLOSURE_OR, "test_crate"); + assert_eq!(ex.report["refusals"], serde_json::json!([]), "{}", ex.tla); + assert_eq!(ex.report["holes"], serde_json::json!([]), "{}", ex.tla); + assert!(!ex.tla.contains("IF (LET"), "{}", ex.tla); + let Some(jar) = tla_tools() else { return }; + sany(&jar, &ex.spec()); + let run = tlc(&jar, &ex.spec(), &ex.cfg); + assert_eq!(run.violated, Vec::::new(), "{}", ex.tla); + // (0,0); then x in {y, y+10} for y = 1..3 after each step: 1 + 2 + 2 + 2. + assert_eq!(run.distinct, 7, "{run:?}\n{}", ex.tla); +} + /// A step field whose guard reads the step value itself (`b < size(step)`) /// is not bounded from it: the domain sits outside the `LET` binding the /// step. It is bounded by its type (`u8`) instead, in the callee's match and diff --git a/source/vir/src/tla.rs b/source/vir/src/tla.rs index b84b8bd40b..72004c17d7 100644 --- a/source/vir/src/tla.rs +++ b/source/vir/src/tla.rs @@ -231,10 +231,14 @@ impl Env { fn symbolic_only(&self, v: &VarIdent) -> bool { self.values.contains_key(v) && !self.names.contains_key(v) && !self.roles.contains_key(v) } - /// Whether `v` reads the post state: the post-role parameter, or a local - /// bound to something that reads it. + /// Whether `v` reads the post state: the post-role parameter, a local + /// bound to something that reads it, or one kept symbolically (a closure + /// or record of closures) whose value reads it in the scope it was bound + /// in (`let f = |v| post.x == v`). fn post_var(&self, v: &VarIdent) -> bool { - self.roles.get(v) == Some(&Role::Post) || self.primed.contains(v) + self.roles.get(v) == Some(&Role::Post) + || self.primed.contains(v) + || self.values.get(v).is_some_and(|(e, scope)| scope.reads_post(e)) } /// Whether `e` reads the post state (primed variables), directly or /// through a call it passes the post state to.