Hoare triple specifications for select functions #
This module contains Hoare triple specifications for some functions in Core.
theorem
Std.Do.Spec.monadMap_trans
{m : Type u → Type v}
{ps : PostShape}
{o : Type u → Type u_1}
{n : Type u → Type u_2}
{α : Type u}
{f : {β : Type u} → m β → m β}
{x : o α}
{Q : PostCond α ps}
[WP o ps]
[MonadFunctor n o]
[MonadFunctorT m n]
:
theorem
Std.Do.Spec.throw_Except
{m : Type u → Type v}
{ps : PostShape}
{ε α : Type u_1}
{e : ε}
{Q : PostCond α (PostShape.except ε PostShape.pure)}
[Monad m]
[WPMonad m ps]
:
theorem
Std.Do.Spec.get_EStateM
{ε σ : Type u_1}
{Q : PostCond σ (PostShape.except ε (PostShape.arg σ PostShape.pure))}
:
theorem
Std.Do.Spec.set_EStateM
{ε σ : Type}
{s : σ}
{Q : PostCond PUnit (PostShape.except ε (PostShape.arg σ PostShape.pure))}
:
theorem
Std.Do.Spec.modifyGet_EStateM
{ε σ α : Type u_1}
{f : σ → α × σ}
{Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure))}
:
theorem
Std.Do.Spec.throw_EStateM
{ε σ α : Type u_1}
{e : ε}
{Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure))}
:
theorem
Std.Do.Spec.tryCatch_EStateM
{α ε σ : Type u_1}
{x : EStateM ε σ α}
{h : ε → EStateM ε σ α}
(Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure)))
:
Lifting MonadStateOf #
Lifting MonadReaderOf #
Lifting MonadExceptOf #
theorem
Std.Do.Spec.throw_ReaderT
{m : Type u → Type v}
{sh : PostShape}
{ε : Type u_1}
{ρ α : Type u}
{e : ε}
{Q : PostCond α (PostShape.arg ρ sh)}
[WP m sh]
[Monad m]
[MonadExceptOf ε m]
:
theorem
Std.Do.Spec.throw_StateT
{m : Type u → Type v}
{ps : PostShape}
{ε : Type u_1}
{α σ : Type u}
{e : ε}
[WP m ps]
[Monad m]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.arg σ ps))
:
theorem
Std.Do.Spec.throw_ExceptT_lift
{m : Type u → Type v}
{ps : PostShape}
{ε α ε' : Type u}
{e : ε}
[WP m ps]
[Monad m]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.except ε' ps))
:
theorem
Std.Do.Spec.tryCatch_ReaderT
{m : Type u → Type v}
{ps : PostShape}
{ε : Type u_1}
{α ρ : Type u}
{x : ReaderT ρ m α}
{h : ε → ReaderT ρ m α}
[WP m ps]
[Monad m]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.arg ρ ps))
:
theorem
Std.Do.Spec.tryCatch_StateT
{m : Type u → Type v}
{ps : PostShape}
{ε : Type u_1}
{α σ : Type u}
{x : StateT σ m α}
{h : ε → StateT σ m α}
[WP m ps]
[Monad m]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.arg σ ps))
:
theorem
Std.Do.Spec.tryCatch_ExceptT_lift
{m : Type u → Type v}
{ps : PostShape}
{ε α ε' : Type u}
{x : ExceptT ε' m α}
{h : ε → ExceptT ε' m α}
[WP m ps]
[Monad m]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.except ε' ps))
:
@[reducible, inline]
The type of loop invariants used by the specifications of for ... in ... loops.
A loop invariant is a PostCond that takes as parameters
- A
List.Cursor xsrepresenting the iteration state of the loop. It is parameterized by the list of elementsxsthat theforloop iterates over. - A state tuple of type
β, which will be a nesting ofMProds representing the elaboration oflet mutvariables and early return.
The loop specification lemmas will use this in the following way:
Before entering the loop, the zipper's prefix is empty and the suffix is xs.
After leaving the loop, the zipper's suffix is empty and the prefix is xs.
During the induction step, the invariant holds for a suffix with head element x.
After running the loop body, the invariant then holds after shifting x to the prefix.
Equations
- Std.Do.Invariant xs β ps = Std.Do.PostCond (xs.Cursor × β) ps
Instances For
@[reducible, inline]
abbrev
Std.Do.Invariant.withEarlyReturn
{ps : PostShape}
{α✝ : Type u}
{xs : List α✝}
{β γ : Type u}
(onContinue : xs.Cursor → β → Assertion ps)
(onReturn : γ → β → Assertion ps)
(onExcept : ExceptConds ps := ExceptConds.false)
:
Helper definition for specifying loop invariants for loops with early return.
for ... in ... loops with early return of type γ elaborate to a call like this:
forIn (β := MProd (Option γ) ...) (b := ⟨none, ...⟩) collection loopBody
Note that the first component of the MProd state tuple is the optional early return value.
It is none as long as there was no early return and some r if the loop returned early with r.
This function allows to specify different invariants for the loop body depending on whether the loop
terminated early or not. When there was an early return, the loop has effectively finished, which is
encoded by the additional ⌜xs.suffix = []⌝ assertion in the invariant. This assertion is vital for
successfully proving the induction step, as it contradicts with the assumption that
xs.suffix = x::rest of the inductive hypothesis at the start of the loop body, meaning that users
won't need to prove anything about the bogus case where the loop has returned early yet takes
another iteration of the loop body.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Std.Do.Spec.forIn'_list
{m : Type u → Type v}
{ps : PostShape}
{α β : Type u}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant xs β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_list_const_inv
{m : Type u → Type v}
{ps : PostShape}
{α β : Type u}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
{inv : PostCond β ps}
(step :
∀ (x : α) (hx : x ∈ xs) (b : β),
⦃inv.fst b⦄ f x hx b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst b'
| ForInStep.done b' => inv.fst b', inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_list
{m : Type u → Type v}
{ps : PostShape}
{α β : Type u}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_list_const_inv
{m : Type u → Type v}
{ps : PostShape}
{α β : Type u}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : α → β → m (ForInStep β)}
{inv : PostCond β ps}
(step :
∀ (hd : α) (b : β),
⦃inv.fst b⦄ f hd b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst b'
| ForInStep.done b' => inv.fst b', inv.snd)⦄)
:
theorem
Std.Do.Spec.foldlM_list
{m : Type u → Type v}
{ps : PostShape}
{α β : Type u}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : β → α → m β}
(inv : Invariant xs β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f b cur ⦃(fun (b' : β) => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_range
{β : Type}
{m : Type → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Range}
{init : β}
{f : (a : Nat) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List Nat) (cur : Nat) (suff : List Nat) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_range
{β : Type}
{m : Type → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Range}
{init : β}
{f : Nat → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List Nat) (cur : Nat) (suff : List Nat) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_prange
{m : Type u → Type v}
{ps : PostShape}
{su sl : PRange.BoundShape}
{α β : Type u}
[Monad m]
[WPMonad m ps]
[PRange.UpwardEnumerable α]
[PRange.SupportsUpperBound su α]
[PRange.SupportsLowerBound sl α]
[PRange.HasFiniteRanges su α]
[PRange.BoundedUpwardEnumerable sl α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLowerBound sl α]
[PRange.LawfulUpwardEnumerableUpperBound su α]
{xs : PRange { lower := sl, upper := su } α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_prange
{m : Type u → Type v}
{ps : PostShape}
{su sl : PRange.BoundShape}
{α β : Type u}
[Monad m]
[WPMonad m ps]
[PRange.UpwardEnumerable α]
[PRange.SupportsUpperBound su α]
[PRange.SupportsLowerBound sl α]
[PRange.HasFiniteRanges su α]
[PRange.BoundedUpwardEnumerable sl α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLowerBound sl α]
[PRange.LawfulUpwardEnumerableUpperBound su α]
{xs : PRange { lower := sl, upper := su } α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_array
{m : Type u → Type v}
{ps : PostShape}
{α β : Type u}
[Monad m]
[WPMonad m ps]
{xs : Array α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_array
{m : Type u → Type v}
{ps : PostShape}
{α β : Type u}
[Monad m]
[WPMonad m ps]
{xs : Array α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.foldlM_array
{m : Type u → Type v}
{ps : PostShape}
{α β : Type u}
[Monad m]
[WPMonad m ps]
{xs : Array α}
{init : β}
{f : β → α → m β}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f b cur ⦃(fun (b' : β) => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b'), inv.snd)⦄)
: