diff --git a/source/rust_verify_test/tests/tla_export.rs b/source/rust_verify_test/tests/tla_export.rs index 7ea64d0d3c..ece093aae1 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,401 @@ 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); +} + +/// 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); +} + +/// 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 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 +/// 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 0fd54d042a..72004c17d7 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`]. //! @@ -163,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)] @@ -198,11 +208,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 +231,40 @@ 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, 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.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. + 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 +356,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 +659,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", @@ -752,7 +810,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( @@ -764,6 +822,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) @@ -1064,7 +1125,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), @@ -1158,6 +1219,21 @@ 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, 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) => + { + 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 +1641,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 +1681,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(" ")) } }; @@ -1808,7 +1900,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 @@ -1816,15 +1908,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) => { @@ -1883,10 +1979,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); @@ -2121,6 +2224,26 @@ 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 { + // 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" => { + 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 +2289,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 +2340,373 @@ 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: 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; + } + 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(); + 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 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, + 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![x.clone()])); + } + 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; + 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 { + 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, .. } = &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 { + 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 +2946,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 +3014,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__"); @@ -2845,7 +3400,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)); @@ -2876,6 +3431,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()); + } } } } @@ -2891,7 +3451,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 { @@ -2903,7 +3463,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)", @@ -2911,6 +3471,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()); @@ -3327,6 +3888,38 @@ 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, + } +} + +/// 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 { @@ -3808,6 +4401,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()); @@ -3831,7 +4425,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(); @@ -3843,6 +4437,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 +4464,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,19 +4472,21 @@ pub fn export_module(krate: &Krate, arg: &str) -> Result { } } } else { - init_name = ex.ensure_function(&(triple.init.clone(), Variant::Plain)); - next_name = ex.ensure_function(&(triple.next.clone(), Variant::Plain)); + ex.in_init = true; + 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, 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(), @@ -3952,7 +4550,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. @@ -3991,7 +4589,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, }