Use when and make eager checking for spec fn requires configurable

[utaal]

---

NOTE: This is the original proposal. See the new proposal #764 (comment) based on feedback in this discussion.

---

Original proposal

Based on the discussion on the Slack, and on offline discussions with @Chris-Hawblitzel and @jonhnet, here is a proposal to change the user experience around "requires" for `spec` functions (by @jonhnet and @utaal). Proposal first, the rationale follows.

spec functions can optionally have a when clause.

spec fn some_gt_0(s: Option<int>) -> bool
  when s.is_some()
{
  s.unwrap() > 0
}

When clauses take up the role of recommends, but are checked by default on calls from other spec functions.

spec fn gt_0(s: Option<int>) -> bool
{
  some_gt_0(s) // ERROR: failed when
}

This is a hard error (unlike current recommends).

Optionally, the user can disable when-checking for spec functions:

• find a motivating example for why you'd ever want this, for the docs.

spec(unchecked) fn gt_0(s: Option<int>) -> bool
{
  some_gt_0(s) // no error
}

when always restricts where the function is defined, so:

spec fn minus2(i: int) -> int
  when i >= 2
{
  i - 2
}
proof fn test() {
  assert(minus2(2) == 0); // succeeds
  assert(minus2(0) == -2); // assertion fails because `minus2` is undefined for `i == 0`, warning for the failed `when` of `minus2`
}

If a recursive function only decreases with certain arguments, when takes up the same role as before: restricting where the function is defined, and for which values of the arguments one needs to prove termination.

spec fn minus2(n: nat) -> nat
  decreases n
  when n >= 2
{
  if n == 2 {
    0
  } else {
    1 + minus2(n - 1)
  }
}

With the upcoming spec-ensures, if a spec function has when W ensures E, then we learn that W ==> E. We are not going to have hard-checks on when for spec functions in proof and exec code, so we cannot simply learn E after a call to the function.

Spec functions are otherwise treated as before in proof and exec contexts (modulo the restriction of the definition to when). When a proof fails, we'd check the whens of functions invoked by the proof, and report failures as warnings.

An attribute #![when(warn|allow)] (or a similar name) disables hard errors for whens inside a module or crate, and optionally turns them into warnings instead. This does not change semantics / soundness, due to how termination and ensures are treated. This restores (most) of the previous recommends behavior for folks/projects that prefer it.

---

Rationale

This does not require emitting hard-precondition checks in proof and exec functions. But this helps catch mistakes in spec functions early, which @jonhnet has found to be very valuable (rather, delaying these findings can be very costly during development).

Patterns supported by a mix of decreases when and recommends can still be supported, but a bit more verbosely. See below.

The name when is used instead of requires because in proof and exec contexts (and in spec(unchecked)) we don't emit a verification condition for when but allow the proof to fail due to it being not satisfied. when is "when" the function is defined.

Behavior of spec-ensures: in Dafny, failure to satisfy the requires appears as an error and if the remaining proof text relies on the assumption of the ensures, there would be no further errors. Under this proposal, the failure to satisfy the when appears as a warning, and then an additional error would appear related to the unavailable ensures conclusion. To recover the Dafny behavior, which we believe is more desirable, we can hold off on reporting errors for a failing proof, but re-run the query with hard requires checks, and strong ensures assumptions; more thought may be required in handling "nested" unchecked specs.

Support for advanced patterns

It still allows advanced patterns when needed.

If we want to avoid a check at a call-site for certain functions where a hard-when check would be burdensome (e.g. spec_index), we can write something like:

spec fn spec_index(x)
  // note: absence of `when` clause (e.g. `when P`)
  ensures P => Q
{
  if P {
    // ... satisfies Q
  } else {
    arbitrary()
  }
}

And we can similarly support cases in which the hard-when would be cumbersome in recursive functions, like in @matthias-brun's example (with the current meaning of recommends):

spec fn sum_many(s: Seq<nat>, indices: Seq<int>) -> nat
    recommends forall|i| 0 <= i < indices.len() ==> 0 <= #[trigger] indices[i] < s.len()
    decreases indices.len()
{
    if indices.len() > 0 { s[indices[0]] + sum_many(s, indices.drop_first()) } else { 0 }
}

which can still be represented as:

spec fn sum_many(s: Seq<nat>, indices: Seq<int>) -> nat
    decreases indices.len()
{
  if forall|i| 0 <= i < indices.len() ==> 0 <= #[trigger] indices[i] < s.len() {
    if indices.len() > 0 { s[indices[0]] + sum_many(s, indices.drop_first()) } else { 0 }
  } else { arbitrary() }
}

[jaybosamiya]

I generally like this new proposal! The more errors detected earlier, the better!

A small part of it is a bit confusing though. Specifically, the example immediately after the line “when always restricts where the function is defined:” is a bit confusing (the assert(minus2(0) == -2) "fails") since it appears to imply that it is checked at use-site rather than at definition site, which seems to be in contradiction with a later statement that says “We are not going to have hard-checks on when for spec functions in proof and exec code”. As I understand it, the intention is to encode that specific spec fn minus2(i: int) -> int when i >= 2 { i - 2 } as a if i >= 2 { i - 2 } else { arbitrary }, and that is what is causing the failure at the assert, and not the actual when clause, correct?

If that is indeed the case, then the encoding is already including the when clause at each use-point, which means that the encoding is not as clean as a simple i - 2 anyways, at which point, I am not sure I am seeing a good reason to not make it a hard error everywhere (including in proof and exec code). Thus presumably I am missing something in what I've written above. I assume some others could be confused on this point too, so it might help to expand a bit on why we aren't going the full-hard-error version.

---

Also, as another note, rather than #![when(warn|allow)], the general Rust convention would be something like #![allow(when)] or such.

[utaal]

Good point, let me clarify:

proof fn test() {
  assert(minus2(2) == 0); // succeeds
  assert(minus2(0) == -2); // assertion fails because `minus2` is undefined for `i == 0`, warning for the failed `when` of `minus2`
}

The intention is to encode that specific spec fn minus2(i: int) -> int when i >= 2 { i - 2 } as a if i >= 2 { i - 2 } else { arbitrary }, and that is what is causing the failure at the assert, and not the actual when clause, correct?

That's correct.

then the encoding is already including the when clause at each use-point

It wouldn't, the clause would be on the axiom that's used to define the function (which would still slightly complicate the encoding).

[utaal]

Also, as another note, rather than #![when(warn|allow)], the general Rust convention would be something like #![allow(when)] or such.

I believe it is the convention for lint-like checks (case, unused variables, etc.). This switch changes VC generation (though, not semantics) significantly, so it may be good to communicate that with different syntax, but I don't have a strong opinion there.

[utaal]

@Chris-Hawblitzel asked about functions like Seq::spec_index, choose, and Option::spec_unwrap that currently use recommends, and don't immediately fit in this proposal.

The intent of the proposal is to have a single user-facing concept which interacts clearly with decreases and ensures. I think important questions for these functions are:

• would we be okay with just doing hard when checking for all these too?
• are these cases uncommon, and mainly in the standard library? If so, should we address them with an "advanced" feature that users don't initially have to think about? (That would likely be the equivalent of the current recommends . Users would get warnings, not hard errors, for failed recommends. We would not allow both when and recommends on the same function.)

[Chris-Hawblitzel]

My understanding of this proposal is that it intends to maximize the benefits of catching mistakes early (particularly mistakes related to passing incorrect arguments to spec functions), while minimizing the costs to the SMT solver. I definititely agree with this intent.

I fear, though, that "when" clauses, as proposed here, may be significantly more expensive to the SMT solver than recommends clauses, even in proof and exec functions, and even though the proposal strives to avoid extra overhead in proof and exec functions.

Preconditions have a tendency to accumulate in long series of nested definitions. In the following example, g needs to declare P1 as a precondition because f needs it, and h needs to declare P1 && P2 as a precondition because g needs it:

spec fn f(x) when P1 { ... }
spec fn g(x) when P1 && P2 { ...f(x)... }
spec fn h(x) when P1 && P2 && P3 { ...g(x)... }

When the SMT solver expands h(arg) = body_h[x := arg], including expanding g and f, it has to jump through many hoops, proving P1 three times, P2 twice, and P3 once. If we used recommends instead:

spec fn f(x) recommends P1 { ... }
spec fn g(x) recommends P1 && P2 { ...f(x)... }
spec fn h(x) recommends P1 && P2 && P3 { ...g(x)... }

then the SMT solver can simply substitute the bodies of f, g, and h directly, with no additional proof obligations, when expanding h(arg).

This overhead is necessary for recursive definitions. But for most definitions, I think this overhead is all SMT cost and little programmer benefit. If our goal is to check spec function preconditions more eagerly and in more places, I'd rather just check "arg" at the call site to h, instead of adding extra SMT overhead to the expansion of h, g, and f. Perhaps we could do this with recommends if the recommends checking is sufficiently convenient to customize (e.g. #![recommends(warn|allow)]).

[utaal]

Thank you for the write-up. I had not considered the tendency of preconditions to accumulate.

I believe restricting the domain as proposed for when helps with the uniformity of treatment of function definitions, ensures and decreases. However, the SMT cost you're discussing may very well be too high of a price.

Here's a question: if we kept all the strict checking as discussed above, but changed when to not restrict the domain of the function for non-recursive definitions (which would result in something similar to current recommends but with strict checking), would we think that would be confusing? That is:

spec fn minus2(i: int) -> (res: int)
  when i >= 2
  ensures res >= 0
{
  i - 2
}
proof fn test() {
  assert(minus2(2) == 0); // succeeds
  assert(minus2(0) == -2); // succeeds (!!! do we think this would be confusing? !!!)
}

spec fn caller(i: int) -> bool {
  minus2(i) == 0 // ERROR `when` not satisfied
}

[Chris-Hawblitzel]

The distinction between checking spec functions preconditions in spec function bodies but not in exec and proof function bodies is interesting. I agree that we should strive to avoid checking exec/proof obligations and spec precondition obligations together in one giant verification condition. But if we wanted to eagerly check spec function preconditions in exec/proof code (I'm not saying we do, necessarily), we could potentially check them separately, with one VC for the spec precondition checking and one for the exec/proof obligations. And the VC for spec precondition checking could run first.

[utaal]

The following is the first revised proposal, #764 (comment) is the latest.

First revised proposal.

Here is a proposed revision, based on the feedback so far:

spec functions can optionally have a when clause.

spec fn some_gt_0(s: Option<int>) -> bool
  when s.is_some()
{
  s.unwrap() > 0
}

When clauses take up the role of recommends, but are checked by default on calls from other spec functions.

spec fn gt_0(s: Option<int>) -> bool
{
  some_gt_0(s) // ERROR: failed when
}

This is a hard error (unlike current recommends).

Optionally, the user can disable when-checking for spec functions:

• find a motivating example for why you'd ever want this, for the docs.

spec(unchecked) fn gt_0(s: Option<int>) -> bool
{
  some_gt_0(s) // no error
}

when does not restrict where a non-recursive function is defined, so:

spec fn minus2(i: int) -> int
  when i >= 2
{
  i - 2
}
proof fn test() {
  assert(minus2(2) == 0); // succeeds
  assert(minus2(0) == -2); // succeeds !!! do we think this would be confusing? !!!
}

If a recursive function only decreases with certain arguments, when takes up the same role as before: restricting where the function is defined, and for which values of the arguments one needs to prove termination.

spec fn minus2_rec(n: nat) -> nat
  decreases n
  when n >= 2
{
  if n == 2 {
    0
  } else {
    1 + minus2(n - 1)
  }
}

With the upcoming spec-ensures, if a spec function has when W ensures E, then we learn that W ==> E. We are not going to have hard-checks on when for spec functions in proof and exec code, so we cannot simply learn E after a call to the function.

spec lambdas bodies are checked for when failures. To address these errors, users can add when to the lambda: |x| when x >=2 { minus2(x) } to make it partial, as proposed in #838. A total lambda can also be marked unchecked / #[allow(...)] to suppress recommends checks in its body: unchecked |x| minus2(x).

spec functions are otherwise treated as before in proof and exec contexts. When a proof fails, we'd check the whens of functions invoked by the proof, and report failures as warnings.

An attribute #![when(warn|allow)] (or a similar name) disables hard errors for whens inside a module or crate, and optionally turns them into warnings instead. This does not change semantics / soundness, due to how termination and ensures are treated. This restores (most) of the previous recommends behavior for folks/projects that prefer it.

Avoiding hard errors in common cases where they don't matter

We can keep an (advanced) affordance for functions for which we do not want strict precondition checks but we do want warnings when arguments may be outside a certain domain (like Seq::spec_index, choose, and Option::spec_unwrap: when can be changed to recommends to write:

pub open spec fn spec_index(self, i: int) -> A
    recommends 0 <= i < self.len()
{
    self.index(i)
}

when and recommends are mutually exclusive. Callers of spec_index would always get warnings, not hard errors for calls that fail the recommends.

How to silence recommends failures

If they don't want to introduce a when, spec function callers can either:

• write if i < s.len() { s.index(i) } else { arbitrary() }, or
• use an attribute #[allow(failed_recommends)] at the function level (and technically at a module and crate level).

spec lambda bodies are automatically #[allow(failed_recommends)].

spec functions callers can also request to always have hard errors for recommends with #[deny(failed_recommends)], at a function, module, or crate level.

Calls in a function marked spec(unchecked) are never checked for recommends failure.

Recursive functions

recommends would only be allowed on non-recursive functions, to prevent confusion about the function domain and VCs.
(Advanced?) users can otherwise opt-out of (strictly checked) when in recursive functions like in the original proposal:

spec fn sum_many(s: Seq<nat>, indices: Seq<int>) -> nat
    decreases indices.len()
{
  if forall|i| 0 <= i < indices.len() ==> 0 <= #[trigger] indices[i] < s.len() {
    if indices.len() > 0 { s[indices[0]] + sum_many(s, indices.drop_first()) } else { 0 }
  } else { arbitrary() }
}

Spec-ensures

If a non-recursive spec function has recommends R ensures E, then we learn R ==> E. Because of this we may want to name this when(warn) (or similar), rather than recommends.

[jonhnet]

Sub-proposal: Name the recommends feature with an attribute to indicate it's a power-user/deep-in-the-standard-library thing, not something end users should worry about. Perhaps #[when-is-warning] or something. My motivation here is that, as I imagine teaching people to read and write this language, I don't want them to see recommends and think "hey, I should try that!"

[utaal]

Rationale

Most user level code should only need when.

Power users (like library authors) can use recommends to avoid hard errors for functions that are commonly used without knowing the precondition is true (e.g. Seq::spec_index), especially for functions commonly used in lambdas so they almost never need when (based on our experience in Dafny that the most common use for a lambda requires is a sequence bound).

[Chris-Hawblitzel]

I'd like to argue against defaulting to "hard errors" when checking spec functions. I have to admit that I have a bias here: I was the one who implemented the far opposite, of defaulting to no checks at all, and having to opt in just to get warnings ("spec(checked)"). I do like the idea of making this option easily configurable at a function level, module level, and crate level via something like #![allow(when)], #![warn(when)], #![deny(when)], etc. As a compromise, I'd suggest making #![warn(when)] the default, and if people want to elevate this to an error, they can easily say #![deny(when)] for their whole crate, which is analogous to how people can configure compilers with some kind of warn-as-error option.

Here's my reason for suggesting "warn by default". Verus's ultimate goal is to verify exec functions. For these, verification is mandatory; it's unsound to disable verification. Proof functions can support exec functions, and for soundness, proof functions must also be verified. Finally, for soundness, recursive spec functions need to have their decreases clauses verified. Beyond this, verifying spec functions is not strictly necessary, but can be helpful in catching bug in spec definitions early. As long as it's helpful, people should enable checking inside spec function definitions. However, this checking is not an end in itself, but rather a tool for easing the verification of proof and exec code, which is the ultimate goal. If checking spec function definitions ever starts to become more of a burden than a benefit, people should simply not enable this checking in places where the pain exceeds the gain. This is why I like the idea of making this checking easily configurable, making it convenient to promote to "error" to demote to "warn" or "allow" as is appropriate to each situation.

I'm worried that if the default for checking spec functions is "error", people will get the impression that demoting the checking to "warn" or "allow" is unsound and will be afraid to do this, even when they should, and spec functions will simply pile up more and more proof obligations out of a sense of dutiful completeness. To continue my earlier example, suppose someone implements a series of functions f, g, h, and wants to use h to implement view:

spec fn f(x) when P1 { ... }
spec fn g(x) when P1 && P2 { ...f(x)... }
spec fn h(x) when P1 && P2 && P3 { ...g(x)... }
impl View for S {
    spec fn view(&self) -> ... { ... h(...) ... }
}

The programmer might see a warning or error when their implementation of view calls h(...), because View::view doesn't have any when or recommends clauses:

pub trait View {
    type V;
    spec fn view(&self) -> Self::V;
}

I'm afraid that with a default of "error", people will assume that they have to keep propagating the error, and think that View needs to be rewritten as:

pub trait View {
    type V;
    spec fn view_precondition(&self) -> bool;
    spec fn view(&self) when self.view_precondition() -> Self::V;
}

I think this would be the wrong conclusion; I would consider view_precondition to be needless complexity. In this example, I think verifying f, g, and h is useful, but verifying the call from S::view to h(...) is a place where the checking is more of a burden than a benefit. I would hope that in this situation, it would be clear to programmers that they can simply use #[allow(when)] or something similar, and that they can do so without fear of unsoundness.

I think warn-by-default is a nice balance here: it makes people aware of checking spec functions, so that they can decide for themselves whether to be more strict (e.g. "deny(when)") or more lenient (e.g. "allow(when)").

[jonhnet]

The central issue here is our mental model of the people we're trying to design the language for. The concept of deliberately using functions outside their intended domain to improve verification performance is a very advanced one, a subtle compile-time optimization. When I sort the concepts my students and engineering colleagues have acquired and need to acquire, that one is very late in the list. One could build a big project and never need it. Code (proof) that exploits it is much less readable, so even if one engineer gets it, they're setting a trap for the next unsuspecting person that joins the team.

I'm not persuaded by the argument that "someone might think it unsound". Verus should have a mode akin to the /noCheating flag we added to Dafny in Ironfleet: the tool enforces only sound text in _v files; the user may only introduce axioms (and hence potential unsoundness) in _t files. Once we have an unambiguous way to mark files in sound-only mode, it should be very clear to (advanced) users that using the #[allow(when)] must not introduce a soundness risk.

By the way, as a sorta-advanced user, there are places in our Dafny corpus where we explicitly deployed this advanced mode by writing

if precond(x) then body(x) else arbitrary

...so I think of #[allow(warn)] as sugar for such an explicit hack. But I also actively avoided this style, because it made debugging elsewhere so painful! requires P ensures Q is vastly easier to interact with than ensures P ==> Q.

Another way for an advanced user to mitigate verification performance creep is to roll a long P1 && P2 && P3 && P4 precondition up into a single named and closed predicate. I think that'll happen naturally at abstracted module boundaries, once we have good tooling and techniques to deploy them.

If you're worried that default-deny will prevent anyone from discovering the performance crimes they're committing: I propose we address that with good tooling. A verification-perf linter might say something like "in this project, when-checking these three spec fns is costing 470ms, which is 2.6% of total verification time. To reduce it, read this chapter (link) on allow(when)." Then users can decide for themselves whether introducing the debug trap is worth reducing the verification cost.

In summary: my intuition is that the language design shouldn't be targeting people with Hawblitzel-level comprehension of what's happening under the covers. Default deny is a velvet rope that keeps less sophisticated users from creating infuriating debugging nightmares for themselves or their teammates. Being able to optionally disable when-checking (via an attribute or one of the syntaxes I mentioned) will allow advanced users to create molten lava traps if they are so inclined.

[Chris-Hawblitzel]

Just to be clear, my objection to error-by-default is not about performance, and my argument never mentioned performance. I'm not trying to push "advanced" features onto novice users. Rather, my concern is precisely about novice users getting themselves into trouble by doing more verification work than they need to and adding more complexity than they need to. Verification is too hard, and many beginners working on verification will not realize that the verifier is asking them to spend more time verifying than they actually need to by encouraging them to accumulate more and more preconditions on spec functions. They won't realize that this accumulation is entirely optional. They may end up writing extra proof blocks and lemmas inside the spec functions to deal with the "errors" that the verifier reports, not realizing that these proof blocks and lemmas are unnecessary for the ultimate goal of verifying the exec and proof functions. I think doing more work than necessary is one of the easiest traps for beginning users to fall into. This is why I think warn-by-default is a balance between helping beginning users diagnose potential problems early, and avoiding leading users towards excessive complexity that actually makes verification more work.

The mental model that I want beginning users to have in mind is simple: spec functions are total.

[jonhnet]

Oh! Thank you for clarifying.

I guess my experience is that "spec functions are total" is not a simplifying model. I understand your concern about accumulating obligations, but in practice, I basically always abstract them into a clump (wf()). The downside to total spec functions is that, in practice, they lead to wild goose chases that eventually terminate in a forehead slap and "I wish I'd just gotten that as an error three hours ago."

[utaal]

Here is an alternative revision, that allows both styles (error-by-default and warn-by-default), using a flag, like Rust's lint levels (as suggested by @jaybosamiya): #[deny(unfulfilled_when)], #[warn(unfulfilled_when)], #[allow(unfulfilled_when)]. This tries to be a compromise between the two schools of thought, roughly that (a) issues in spec functions should be caught early, and (b) users should not think they should do more work than they strictly need to.

Shorter suggestions for unfulfilled_when are very welcome. Is when enough? (e.g. #[allow(when)], #[warn(when)], #[deny(when)])

It does so trying to fulfill as best I can the priorities of both: (a) ensuring that users get early, actionable, and easy-to-parse feedback to avoid "wild goose chases", and (b) making it clear to users that fulfilling when (recommends) is entirely optional.

The default level is #[warn(unfulfilled_when)], and it can be upgraded to #[deny(unfulfilled_when)] at a crate/module/function level. The guide can recommend addressing warnings early, like one often does in Rust, or even recommend enabling #[deny(unfufilled_when)] for modules/crates containing complex spec function definitions.

spec functions can optionally have a when clause.

spec fn some_gt_0(s: Option<int>) -> bool
  when s.is_some()
{
  s.unwrap() > 0
}

When clauses are checked by default on calls from other spec functions, and produce a warning or error depending on the unfulfilled_when level.

spec fn gt_0(s: Option<int>) -> bool
{
  some_gt_0(s) // WARNING or ERROR: unfulfilled when
}

Optionally, the user can disable when-checking for spec functions:

#[allow(unfulfilled_when)]
spec fn gt_0(s: Option<int>) -> bool
{
  some_gt_0(s) // no error
}

when does not restrict where a non-recursive function is defined, so:

spec fn minus2(i: int) -> int
  when i >= 2
{
  i - 2
}
proof fn test() {
  assert(minus2(2) == 0); // succeeds
  assert(minus2(0) == -2); // succeeds
}

If a recursive function only decreases with certain arguments, when takes up the same role as before: restricting where the function is defined, and for which values of the arguments one needs to prove termination.

spec fn minus2_rec(n: nat) -> (r: nat)
  decreases n
  when n >= 2
  ensures r == n - 2
{
  if n == 2 {
    0
  } else {
    1 + minus2(n - 1)
  }
}

With the upcoming spec-ensures, if a spec function has when W ensures E, then we learn that W ==> E. We are not going to have hard-checks on when for spec functions in proof and exec code, so we cannot simply learn E after a call to the function. When checking when (both in spec and proof/exec functions) we would assume the ensures of spec functions that were called explicitly. This is consistent with the common Dafny proof debugging pattern:

proof fn caller(i: nat) {
  let j = minus2_rec(i); // WARNING: unfulfilled when
  assert(j == i - 2); // no error
}

Proofs for decreases and ensures are allowed inline and assume that the when is satisfied. This deprecates decreases_by and recommends_by.

spec lambdas bodies are checked for when failures. To address these errors, users can add when to the lambda: |x| when x >=2 { minus2(x) } to make it partial, as proposed in #838. A total lambda can also be marked #[allow(unfulfilled_when)] to suppress when checks in its body: #[allow(unfulfilled_when)] |x| minus2(x).

spec functions are otherwise treated as before in proof and exec contexts. When a proof fails, we'd check the whens of functions invoked by the proof, and report failures as warnings. In other words, #[deny(unfulfilled_when)] does not apply to proof and exec functions. To help avoid users missing failed whens when they are only reported as warnings, we report them in source order with the other proof errors (which would also be reported in source order). (When a verification time threshold is reached, we can report the errors we've found immediately, as suggested by @Chris-Hawblitzel, to improve perceived responsiveness.)

[utaal]

Moving @jonhnet's comment here to keep it attached to this proposal:

@jonhnet:

I endorse this proposal because it achieves my highest priority: offering a default mode that acts almost as if when is enforced rigorously. As I understand it, in the absence of anyone writing annotations, the user will always see a message (albeit a warning in the proof/exec context) when when is violated. I can teach users "yeah, don't let those warning slide; fix them first to avoid going on a wild goose chase."

I'm emphasizing this rationale because users will see text that appears to say "function f(x) is defined as body", and will expect mentions of f to, in fact, be equal to the body without having to manually test that every time with an assert. Similarly, if I see a call to a proof fn lemma and no error messages, I expect that its requires must already be known to be true before the call site, and the ensures must be known be true just after the call site; I never need to write those asserts to confirm it. Mentions of spec fns with when and ensures should give me the same certainty.

This proposal achieves that user experience goal almost completely. The only exception is that, in a proof/exec context that verifies, a when may silently not hold. However, the moment a user begins debugging such a context (such as by introducing a failing postcondition or assert), the warning appears conspicuously in the order of its call site, mitigating the danger.

[tjhance]

In other words, #[deny(unfulfilled_when)] does not apply to proof and exec functions.

I wonder if it would make the most sense for unfulfilled_when to apply to signatures (like requires and ensures) but not the proof bodies.