forIn loop-invariant gadgets

ForIn.forInWithInvariant and ForIn'.forInWithInvariant' annotate a forIn/forIn' loop with its invariant so that vcgen reads the invariant from the program. Their @[spec] specifications restate Spec.forIn_list/Spec.forIn'_list for every container with a PureForIn instance.

Gadgets

@[inline]

def Std.Internal.Do.ForIn.forInWithInvariant {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred : Type (max u₁ u₂)} {ρ : Type w} [ForIn m ρ α] (xs : ρ) (init : β) (f : α → β → m (ForInStep β)) (inv : Invariant α β Pred) : m β

A forIn loop annotated with its loop invariant, which vcgen reads from the inv argument. It is definitionally forIn xs init f, so the annotation is erased at runtime. The invariant ranges over the elements consumed so far, the elements remaining, and the loop state.

Equations

• Std.Internal.Do.ForIn.forInWithInvariant xs init f inv = forIn xs init f

@[inline]

def Std.Internal.Do.ForIn'.forInWithInvariant' {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred : Type (max u₁ u₂)} {ρ : Type w} {d : Membership α ρ} [ForIn' m ρ α d] (xs : ρ) (init : β) (f : (a : α) → a ∈ xs → β → m (ForInStep β)) (inv : Invariant α β Pred) : m β

A membership-aware forIn' loop annotated with its loop invariant, which vcgen reads from the inv argument. It is definitionally forIn' xs init f, so the annotation is erased at runtime. The invariant ranges over the elements consumed so far, the elements remaining, and the loop state.

Equations

• Std.Internal.Do.ForIn'.forInWithInvariant' xs init f inv = forIn' xs init f

Specifications

theorem Std.Internal.Do.Spec.forInWithInvariant {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ρ : Type w} [ForIn m ρ α] [ForIn Id ρ α] [PureForIn m ρ α] {xs : ρ} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant α β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α), ForIn.toList xs = pref ++ cur :: suff → ∀ (b : β), ⦃ inv pref (cur :: suff) b ⦄ f cur b ⦃ fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv (pref ++ [cur]) suff b' | ForInStep.done b' => inv (ForIn.toList xs) [] b'; epost ⦄) : ⦃ inv [] (ForIn.toList xs) init ⦄ ForIn.forInWithInvariant xs init f inv ⦃ fun (b : β) => inv (ForIn.toList xs) [] b; epost ⦄

theorem Std.Internal.Do.Spec.forInWithInvariant' {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ρ : Type w} {d : Membership α ρ} [ForIn' m ρ α d] [ForIn Id ρ α] [LawfulMemForInId ρ α] [PureForIn' m ρ α] {xs : ρ} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant α β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : ForIn.toList xs = pref ++ cur :: suff) (b : β), ⦃ inv pref (cur :: suff) b ⦄ f cur ⋯ b ⦃ fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv (pref ++ [cur]) suff b' | ForInStep.done b' => inv (ForIn.toList xs) [] b'; epost ⦄) : ⦃ inv [] (ForIn.toList xs) init ⦄ ForIn'.forInWithInvariant' xs init f inv ⦃ fun (b : β) => inv (ForIn.toList xs) [] b; epost ⦄