The function double doubles a natural number state:

def double : StateM Nat Unit := do modify (2 * ·)

Thinking chronologically, a reasonable specification is that value of the output state is twice that of the input state. This is expressed using a schematic variable that stands for the initial state:

theorem double_spec : ⦃ fun s => ⌜s = n⌝ ⦄ double ⦃ ⇓ () s => ⌜s = 2 * n⌝ ⦄ := byn:Nat⊢ ⦃fun s => ⌜s = n⌝⦄ double ⦃PostCond.noThrow fun x s => ⌜s = 2 * n⌝⦄ simp [double]n:Nat⊢ ⦃fun s => ⌜s = n⌝⦄ modify fun x => 2 * x ⦃PostCond.noThrow fun x s => ⌜s = 2 * n⌝⦄ mvcgen with grindAll goals completed! 🐙

However, an equivalent specification that treats the postcondition schematically will lead to smaller verification conditions when double is used in other functions:

@[spec] theorem better_double_spec {Q : PostCond Unit (.arg Nat .pure)} : ⦃ fun s => Q.1 () (2 * s) ⦄ double ⦃ Q ⦄ := byQ:PostCond Unit (PostShape.arg Nat PostShape.pure)⊢ ⦃fun s => Q.fst () (2 * s)⦄ double ⦃Q⦄ simp [double]Q:PostCond Unit (PostShape.arg Nat PostShape.pure)⊢ ⦃fun s => Q.fst () (2 * s)⦄ modify fun x => 2 * x ⦃Q⦄ mvcgen with grindAll goals completed! 🐙

The first projection of the postcondition is its stateful assertion. Now, the precondition merely states that the postcondition should hold for double the initial state.

The monad LogM maintains an append-only log during a computation:

structure LogM (β : Type u) (α : Type v) : Type (max u v) where log : Array β value : α instance : Monad (LogM β) where pure x := ⟨#[], x⟩ bind x f := let { log, value } := f x.value { log := x.log ++ log, value }

It has a LawfulMonad instance as well.

The log can be written to using log, and a value and the associated log can be computed using LogM.run.

def log (v : β) : LogM β Unit := { log := #[v], value := () } def LogM.run (x : LogM β α) : α × Array β := (x.value, x.log)

Rather than writing it from scratch, the WP instance uses PredTrans.pushArg. This operator was designed to model state monads, but LogM can be seen as a state monad that can only append to the state. This appending is visible in the body of the instance, where the initial state and the log that resulted from the action are appended:

instance : WP (LogM β) (.arg (Array β) .pure) where wp | { log, value } => PredTrans.pushArg (fun s => PredTrans.pure (value, s ++ log))

The WPMonad instance also benefits from the conceptual model as a state monad and admits very short proofs:

instance : WPMonad (LogM β) (.arg (Array β) .pure) where wp_pure x := byα:Type ?u.5σ:List (Type u)ps:PostShapex✝:PredTrans ps αy:PredTrans ps αQ:Assertion psβ:Type ?u.20α✝:Type ?u.20x:α✝⊢ wp (pure x) = pure x extα:Type ?u.5σ:List (Type u)ps:PostShapex✝:PredTrans ps αy:PredTrans ps αQ:Assertion psβ:Type ?u.20α✝:Type ?u.20x:α✝Q✝:PostCond α✝ (PostShape.arg (Array β) PostShape.pure)s✝:Array β⊢ (wp⟦pure x⟧ Q✝ s✝).down ↔ ((pure x).apply Q✝ s✝).down simp [wp, pure]All goals completed! 🐙 wp_bind _ _ := byα:Type ?u.5σ:List (Type u)ps:PostShapex:PredTrans ps αy:PredTrans ps αQ:Assertion psβ:Type ?u.20α✝:Type ?u.20β✝:Type ?u.20x✝¹:LogM β α✝x✝:α✝ → LogM β β✝⊢ (wp do let a ← x✝¹ x✝ a) = do let a ← wp x✝¹ wp (x✝ a) extα:Type ?u.5σ:List (Type u)ps:PostShapex:PredTrans ps αy:PredTrans ps αQ:Assertion psβ:Type ?u.20α✝:Type ?u.20β✝:Type ?u.20x✝¹:LogM β α✝x✝:α✝ → LogM β β✝Q✝:PostCond β✝ (PostShape.arg (Array β) PostShape.pure)s✝:Array β⊢ (wp⟦do let a ← x✝¹ x✝ a⟧ Q✝ s✝).down ↔ ((do let a ← wp x✝¹ wp (x✝ a)).apply Q✝ s✝).down simp [wp, bind]All goals completed! 🐙

The adequacy lemma has one important detail: the result of the weakest precondition transformation is applied to the empty array. This is necessary because the logging computation has been modeled as an append-only state, so there must be some initial state. Semantically, the empty array is the correct choice so as to not place items in a log that don't come from the program; technically, it must also be a value that commutes with the append operator on arrays.

theorem LogM.of_wp_run_eq {x : α × Array β} {prog : LogM β α} (h : LogM.run prog = x) (P : α × Array β → Prop) : (⊢ₛ wp⟦prog⟧ (⇓ v l => ⌜P (v, l)⌝) #[]) → P x := byα:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Prop⊢ (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun v l => ⌜P (v, l)⌝) #[]) → P x rw [← hα:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Prop⊢ (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun v l => ⌜P (v, l)⌝) #[]) → P prog.run]α:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Prop⊢ (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun v l => ⌜P (v, l)⌝) #[]) → P prog.run intro h'α:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Proph':⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun v l => ⌜P (v, l)⌝) #[]⊢ P prog.run simp [wp] at h'α:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Proph':P (prog.value, prog.log)⊢ P prog.run exact h'All goals completed! 🐙

Next, each operator in the library should be provided with a specification lemma. There is only one: log. For new monads, these proofs must often break the abstraction boundaries of Hoare triples and weakest preconditions; the specifications that they provide can then be used abstractly by clients of the library.

theorem log_spec {x : β} : ⦃ fun s => ⌜s = s'⌝ ⦄ log x ⦃ ⇓ () s => ⌜s = s'.push x⌝ ⦄ := byβ:Types':Array βx:β⊢ ⦃fun s => ⌜s = s'⌝⦄ log x ⦃PostCond.noThrow fun x_1 s => ⌜s = s'.push x⌝⦄ simp [log, Triple, wp]All goals completed! 🐙

A better specification for log uses a schematic postcondition:

variable {Q : PostCond Unit (.arg (Array β) .pure)} @[spec] theorem log_spec_better {x : β} : ⦃ fun s => Q.1 () (s.push x) ⦄ log x ⦃ Q ⦄ := byβ:TypeQ:PostCond Unit (PostShape.arg (Array β) PostShape.pure)x:β⊢ ⦃fun s => Q.fst () (s.push x)⦄ log x ⦃Q⦄ simp [log, Triple, wp]All goals completed! 🐙

A function logUntil that logs all the natural numbers up to some bound will always result in a log whose length is equal to its argument:

def logUntil (n : Nat) : LogM Nat Unit := do for i in 0...n do log i theorem logUntil_length : (logUntil n).run.2.size = n := byn:Nat⊢ (logUntil n).run.snd.size = n generalize h : (logUntil n).run = xn:Natx:Unit × Array Nath:(logUntil n).run = x⊢ x.snd.size = n unfold logUntil at hn:Natx:Unit × Array Nath:(do forIn (0...n) PUnit.unit fun i r => do log i pure (ForInStep.yield PUnit.unit) pure PUnit.unit).run = x⊢ x.snd.size = n apply LogM.of_wp_run_eq hn:Natx:Unit × Array Nath:(do forIn (0...n) PUnit.unit fun i r => do log i pure (ForInStep.yield PUnit.unit) pure PUnit.unit).run = x⊢ ⊢ₛ wp⟦do forIn (0...n) PUnit.unit fun i r => do log i pure (ForInStep.yield PUnit.unit) pure PUnit.unit⟧ (PostCond.noThrow fun v l => ⌜(v, l).snd.size = n⌝) #[] mvcgen invariants · ⇓⟨xs, _⟩ s => ⌜xs.pos = s.size⌝ with simp_all [List.Cursor.pos]All goals completed! 🐙 <;> grind [Std.PRange.Nat.size_rco, Std.Rco.length_toList]