Std.Do spec lemmas the toolchain does not ship.

Std.Do.Triple.SpecLemmas covers forIn/forIn'/foldlM over lists, arrays, ranges and iterators — every shape a for loop elaborates to. It does not cover List.mapM, which is what a pass written with mapM rather than with for actually calls, and which mvcgen therefore walks straight past.

theorem Std.Do.Spec.mapM_list {m : Type u → Type v} {ps : PostShape} [Monad m] [LawfulMonad m] [WPMonad m ps] {α β : Type u} {xs : List α} {f : α → m β} (inv : Invariant xs (List β) ps) (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (bs : List β), ⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, bs)⦄ f cur ⦃(fun (b : β) => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, bs ++ [b]), inv.snd)⦄) : ⦃inv.fst ({ «prefix» := [], suffix := xs, property := ⋯ }, [])⦄ List.mapM f xs ⦃(fun (bs : List β) => inv.fst ({ «prefix» := xs, suffix := [], property := ⋯ }, bs), inv.snd)⦄

List.mapM's loop-invariant spec, in the same shape Spec.foldlM_list has: an Invariant indexed by how much of the list has been consumed, plus one obligation per element.

The invariant's second component is the list of results collected so far, in order — the natural thing to state an invariant about. List.mapM itself accumulates them reversed (List.mapM_eq_reverse_foldlM_cons), and undoing that here is the whole content of the proof.

Registered @[spec], so mvcgen invariants ⟨…⟩ picks it up on a mapM exactly as it does on a for loop.