We introduce a new construct \(\texttt {fail}\) which denotes the failure state, as an alternative to \(\sigma \).

For the assumption we only have a \(\top \) rule, the idea being if the assumption holds then the statement is equivalent to a \(\texttt {skip}\) otherwise the execution gets stuck but doesn't fail.

The idea with getting stuck being that since we aren't failing for the case of partial-correctness (failure or termination) it means we can simply ignore this case.

The final big-step evaluation rule is for the havoc statement:

In addition to our big-step evaluation rules we also have Hoare rules.

A central thing to understand with assertions especially is that they integrate a result's monad into the big-step evaluation semantics, in addition to the Hoare logic. So the idea is now instead of the relationship being denoted by:

It's now expressed as

Where we can model \(\texttt {Result}\) as the following monad

    inductive Result (α : Type)
    | ok : α → Result α      -- Normal termination with final state
    | fail : Result α        -- Assertion failure / error state
    deriving Repr, DecidableEq
  

At this point if you want to be pedantic it's worth mentioning that the implication is that we are lifting all other inference rules into the context of this result monad, though for pedagogical purposes its enough to just assume that \(\Downarrow \sigma \) just corresponds to \(\Downarrow \texttt {.ok} \sigma \) i.e. evaluated into a non-fail state.

The Hoare triple is where stuff becomes a bit more interesting. As a reminder, the classical hoare triple is basically just an alias for the logical formula:

Naturally because we know are no longer evaluating into just \(\sigma '\) but either an \(\texttt {ok}\) or \(\texttt {fail}\) state, it's worth asking how we actually represent that as a Hoare triple. We can start in much the same way as we do for the regular partial correctness hoare triple

Here we then run into I guess a design choice as to how we proceed, the two main possibilities are:

• We fail sometimes succeed other times this would mean that: \[ (\exists \sigma ', \sigma _t = \texttt {.ok}\ \sigma ' \land Q(\sigma ')) \] another way of seeing this is here we are disallowig failure meaning that for a hoare triple to be proven valid we must explicitly demonstrate as a side condition that we cannot fail otherwise our hoare triple is invalid.
• We never fail which would mean that: \[ (\forall \sigma ', \sigma _t = \texttt {.ok}\ \sigma ' \land Q(\sigma ')) \] for this rule another way of seeing it is we are ignoring failure or filter success states since we are clearly only quantifying over those states that are successfull.

The latter option seems to be generally more common in theoretical settings because it doesn't require explicitly accounting for failure states, they are just implicitly filtered out in the logic.

We can remember that the weakest precondition is simply what we can derive reasoning backwards from the formulaic expression of a hoare triple.

1. Considering our wp formula we have \[ \texttt {wp}(\texttt {assert}(b), Q)(\sigma ) \to (\texttt {assert}(b), \sigma ) \Downarrow \texttt {.ok}\ \sigma \to Q(\sigma ) \] reasoning backwards we can start with a case split on the evaluation of the assertion, this leads to two cases
   • \(b\) evaluates to true, as this case trivially implies that the assertion evaluates into \(\texttt {.ok}\ \sigma \) it means we must prove \(Q(\sigma )\). The only way we can prove this is by having our weakest precondition be a witness to this assertion.
   • \(b\) evaluates to false, as this would imply a contradiction since the assertion evaluates to \(\texttt {.ok}\ \sigma \), more specifically we know have to prove the contradiction that \(\texttt {.ok}\ \sigma = \texttt {.fail} \sigma \), we know (i.e. have a hypothesis) by inversion that \(b \Downarrow ^f \sigma \) since we know \(b\) has to be true to prove the contradiction we also must ensure the weakest precondition states that \(b \Downarrow ^t \sigma \)
   from these two cases we can conclude that two demonstrate the soundness of the weakest precondition for assert statements, it must be the case that the \(\texttt {wp}\) is the conjunction of the postcondition and the logical assertion that what is being asserted is indeed true, so we have that \[ \texttt {wp}(\texttt {assert}(b), Q)(\sigma ) \equiv (b \Downarrow ^t \sigma ) \land Q(\sigma ) \] the more intuitive reasoning here is that \(Q\) should hold before and after as an assert should, just by design, not do anything to the memory, it's only an assertion after all. Additionally, the condition should hold true as \(\texttt {wp}\) definitionally describes a set of states where all terminating executions end in a state satisfying \(Q\) thus if \(b\) does not evaluate to true, there is no terminating execution from \(\sigma \).
2. We can just use the more intuitive reasoning here, we know the weakest precondition characterizes a set of states where terminating executions end in a state satisfying \(Q\). The only way for something being assumed to be true leading to some other else is it if implies something else, thus our \(\texttt {wp}\) becomes \[ \texttt {wp}(\texttt {assume}(b), Q)(\sigma ) \equiv (b \Downarrow ^t \sigma ) \to Q(\sigma ) \] in terms of backward reasoning the idea is that \(\texttt {assume}(p)\) essentially just adds a raw hypothesis \((b \Downarrow ^t \sigma )\) but clearly that by itself doesn't somehow allow me to just manifest \(Q(\sigma )\), the only way we could possibly get \(Q\) from \(b\) being true is if we have a function which states that \(b\) being true implies \(Q\).