The function double doubles a natural number state:

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

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

theorem double_spec {n : Nat} : ⦃ fun s => s = n ⦄ double ⦃ fun _ s => s = 2 * n ⦄ := byn:Nat⊢ ⦃ fun s => s = n ⦄ double ⦃ fun x s => s = 2 * n ⦄ simp [double]n:Nat⊢ ⦃ fun s => s = n ⦄ modify fun x => 2 * x ⦃ fun x s => s = 2 * n ⦄ vcgen with finishAll goals completed! 🐙

However, an equivalent auto-framing specification leads to smaller verification conditions when double is used in other functions:

@[spec] theorem better_double_spec {Q : Unit → Nat → Prop} : ⦃ fun s => Q () (2 * s) ⦄ double ⦃ Q ⦄ := byQ:Unit → Nat → Prop⊢ ⦃ fun s => Q () (2 * s) ⦄ double ⦃ Q ⦄ simp [double]Q:Unit → Nat → Prop⊢ ⦃ fun s => Q () (2 * s) ⦄ modify fun x => 2 * x ⦃ Q ⦄ vcgen with finishAll goals completed! 🐙

Now, the precondition merely states that the postcondition should hold for double the initial state. Any property that Q states about state that double does not change, such as a second state layer in a monad transformer stack, holds after the call. At a call of double, vcgen instantiates Q with the postcondition that the rest of the program requires, so no entailment between postconditions remains as a verification condition.

The precondition of better_double_spec is exactly the weakest precondition of double, so callers depend on the complete behavior of double. An auto-framing specification can also leave details open. For example, the precondition fun s => ∀ s', s ≤ s' → Q () s' only promises that double does not decrease the 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 β α) α (Array β → Prop) EStack⟨⟩ where wpTrans | { log, value } => PredTrans.pushArg (fun s => pure (value, s ++ log)) wp_trans_monotone x := fun _ _ _ _ _ hpost s => hpost x.value (s ++ x.log)

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

instance : WPMonad (LogM β) (Array β → Prop) EStack⟨⟩ where toWP _ := inferInstance pure_le_wp_pure x post epost := byPred:Type uEPred:Type vα:Type winst✝²:Assertion Predinst✝¹:Assertion EPredProg:Type uValue:Type vinst✝:WP Prog Value Pred EPredprog:Progpost✝:Value → Predepost✝:EPredβ:Type ?u.23α✝:Type ?u.26x:α✝post:α✝ → Array β → Propepost:EStack⟨⟩⊢ post x ⊑ wp (pure x) post epost simp [wp, WP.wpTrans, pure]All goals completed! 🐙 bind_le_wp_bind x f post epost := byPred:Type uEPred:Type vα:Type winst✝²:Assertion Predinst✝¹:Assertion EPredProg:Type uValue:Type vinst✝:WP Prog Value Pred EPredprog:Progpost✝:Value → Predepost✝:EPredβ:Type ?u.23α✝:Type ?u.26β✝:Type ?u.26x:LogM β α✝f:α✝ → LogM β β✝post:β✝ → Array β → Propepost:EStack⟨⟩⊢ wp x (fun a => wp (f a) post epost) epost ⊑ wp (x >>= f) post epost simp [wp, WP.wpTrans, bind]All goals completed! 🐙

The soundness lemma has one important detail: the weakest precondition 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_run_eq_wp {α : Type u} {β : Type v} {x : α × Array β} {prog : LogM β α} (h : LogM.run prog = x) (P : α × Array β → Prop) (hwp : wp prog (fun v l => P (v, l)) () #[]) : P x := byα:Type uβ:Type vx:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Prophwp:wp prog (fun v l => P (v, l)) () #[]⊢ P x rw [← hα:Type uβ:Type vx:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Prophwp:wp prog (fun v l => P (v, l)) () #[]⊢ P prog.run]α:Type uβ:Type vx:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Prophwp:wp prog (fun v l => P (v, l)) () #[]⊢ P prog.run simp [wp, WP.wpTrans] at hwpα:Type uβ:Type vx:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Prophwp:P (prog.value, prog.log)⊢ P prog.run exact hwpAll 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 : β} {s' : Array β} : ⦃ fun s => s = s' ⦄ log x ⦃ fun _ s => s = s'.push x ⦄ := byβ:Type u_1x:βs':Array β⊢ ⦃ fun s => s = s' ⦄ log x ⦃ fun x_1 s => s = s'.push x ⦄ constructorβ:Type u_1x:βs':Array β⊢ (fun s => s = s') ⊑ wp (log x) (fun x_1 s => s = s'.push x) ⊥ simp [log, wp, WP.wpTrans]All goals completed! 🐙

A better specification for log is an auto-framing specification:

@[spec] theorem log_spec_better {x : β} {Q : Unit → Array β → Prop} : ⦃ fun s => Q () (s.push x) ⦄ log x ⦃ Q ⦄ := byβ:Type u_1x:βQ:Unit → Array β → Prop⊢ ⦃ fun s => Q () (s.push x) ⦄ log x ⦃ Q ⦄ constructorβ:Type u_1x:βQ:Unit → Array β → Prop⊢ (fun s => Q () (s.push x)) ⊑ wp (log x) Q ⊥ simp [log, wp, WP.wpTrans]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 {n : Nat} : (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 __s => do log i pure (ForInStep.yield PUnit.unit) pure ()).run = x⊢ x.snd.size = n apply LogM.of_run_eq_wp hn:Natx:Unit × Array Nath:(do forIn (0...n) PUnit.unit fun i __s => do log i pure (ForInStep.yield PUnit.unit) pure ()).run = x⊢ wp (do forIn (0...n) PUnit.unit fun i __s => do log i pure (ForInStep.yield PUnit.unit) pure ()) (fun v l => (v, l).snd.size = n) () #[] vcgen invariants · fun pref suff _ s => pref.length = s.sizevc1n:Natx:PUnit × Array Nath:(do forIn (0...n) PUnit.unit fun i __s => do log i pure (ForInStep.yield PUnit.unit) pure PUnit.unit).run = x⊢ [].length = { toList := [] }.sizevc2n:Natx:PUnit × Array Nath:(do forIn (0...n) PUnit.unit fun i __s => do log i pure (ForInStep.yield PUnit.unit) pure PUnit.unit).run = xa✝¹:PUnits✝:Array Nata✝:(ForIn.toList (0...n)).length = s✝.size⊢ (PUnit.unit, s✝).snd.size = nvc3n:Natx:PUnit × Array Nath:(do forIn (0...n) PUnit.unit fun i __s => do log i pure (ForInStep.yield PUnit.unit) pure PUnit.unit).run = xpref✝:List Natcur✝:Natsuff✝:List Nat_h✝:ForIn.toList (0...n) = pref✝ ++ cur✝ :: suff✝b✝:PUnits✝:Array Nata✝:pref✝.length = s✝.size⊢ (pref✝ ++ [cur✝]).length = (s✝.push cur✝).size all_goals simp_all [Std.Internal.ForIn.toList_rco]All goals completed! 🐙