class DY.WP [ExecTraceTypes] [ProofTraceTypes] (m : Type u → Type v) : Type (max (u + 1) v)

• wp {a : Type u} : m a → (a → ProofTrace → Prop) → ProofTrace → Prop

@[instance_reducible]

instance DY.instWPId [ExecTraceTypes] [ProofTraceTypes] : WP Id

Equations

• DY.instWPId = { wp := fun {a : Type ?u.1} (f : Id a) (post : a → DY.ProofTrace → Prop) (tr_proof : DY.ProofTrace) => post f.run tr_proof }

@[instance_reducible]

instance DY.instWPErr [ExecTraceTypes] [ProofTraceTypes] : WP Err

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.instWPTracefulOfTraceInvariant [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] : WP Traceful

Equations

• One or more equations did not get rendered due to their size.

def DY.hoareTriple {m : Type u_1 → Type u_2} {a : Type u_1} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [WP m] (f : m a) (pre : ProofTrace → Prop) (post : a → ProofTrace → Prop) : Prop

Equations

• DY.hoareTriple f pre post = ∀ (tr : DY.ProofTrace), pre tr → DY.Trace.Invariant tr → DY.wp f post tr

class DY.HasGhostArgumentType {a : Sort u_1} (x : a) (g : outParam (Type u_g)) : Type

This typeclass notifies the step tactic that the hoare triple for x expects a ghost parameter of type g. Knowing this type is crucial to provide useful error message when a user provides a ghost parameter with the wrong type.

• dummy : Unit

structure DY.GhostParameterFinder : Type

Some ghost parameters can be found automatically by looking into the context. This structure holds a metaprogram which is called with a metavariable for the ghost parameter, and the expression corresponding to the hoare triple that requires the ghost parameter. It is expected to assign the ghost parameter metavariable.

• findGhost : Lean.MVarId → Lean.Expr → Lean.MetaM Unit

class DY.HasGhostMetaprogram {a : Sort u_1} (x : a) (metaprog : outParam GhostParameterFinder) : Type

This typeclass notifies the step tactic that metaprog can automatically find the ghost parameter of the the hoare triple associated with x. For technical reasons, metaprog must be a top-level declaration, it cannot be written inline in the declaration. This is to prevent it to depend on local variables specific to this instance.

• dummy : Unit

class DY.HasIndirectGhostMetaprogram {a : Sort u_1} {b : outParam (Sort u_2)} (x : a) (metaprog : outParam GhostParameterFinder) (y : outParam b) : Type

Some hoare triples are derived from others, for example we can create a hoare triple for lift x given a hoare triple for x. In this case, both hoare triple use the same ghost parameter, but the metaprogram that finds the ghost parameter for x won't work if we feed it lift x instead of x. To solve this issue, HasIndirectGhostMetaprogram x metaprog y notifies the step tactic that metaprog is expected to be called with the expression of y instead of the expression of x.

• dummy : Unit

@[instance_reducible]

instance DY.instHasIndirectGhostMetaprogramOfHasGhostMetaprogram {a✝ : Sort u_1} {x : a✝} {metaprog : GhostParameterFinder} [HasGhostMetaprogram x metaprog] : HasIndirectGhostMetaprogram x metaprog x

Equations

• DY.instHasIndirectGhostMetaprogramOfHasGhostMetaprogram = { dummy := () }

class DY.HoareTripleGhost {m : Type u_1 → Type u_2} {a : Type u_1} {g : Type u_3} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [WP m] (f : m a) [HasGhostArgumentType f g] (ghost : g) (pre : outParam (ProofTrace → Prop)) (post : outParam (a → ProofTrace → Prop)) : Prop

• pf : hoareTriple f pre post

class DY.HoareTriple {m : Type u_1 → Type u_2} {a : Type u_1} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [WP m] (f : m a) (pre : outParam (ProofTrace → Prop)) (post : outParam (a → ProofTrace → Prop)) : Prop

• pf : hoareTriple f pre post

@[instance_reducible]

instance DY.instHasGhostArgumentTypeUnitOfHoareTriple [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {m : Type u → Type v} [WP m] {a : Type u} (f : m a) (pre : ProofTrace → Prop) (post : a → ProofTrace → Prop) [HoareTriple f pre post] : HasGhostArgumentType f Unit

Equations

• DY.instHasGhostArgumentTypeUnitOfHoareTriple f pre post = { dummy := () }

instance DY.instHoareTripleGhostUnitUnit [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {m : Type u → Type v} [WP m] {a : Type u} (f : m a) (pre : ProofTrace → Prop) (post : a → ProofTrace → Prop) [HoareTriple f pre post] : HoareTripleGhost f () pre post

class DY.WPLift [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] (m : Type u → Type v) (n : Type u → Type w) [MonadLift m n] [WP m] [WP n] : Prop

• pf {a : Type u} (x : m a) (post : a → ProofTrace → Prop) (tr : ProofTrace) : Trace.Invariant tr → wp x post tr → wp (liftM x) post tr

@[instance_reducible]

instance DY.instHasGhostArgumentTypeLiftM {m : Type u → Type v} {n : Type u → Type w} [MonadLift m n] {a : Type u} {g : Type u_g} (x : m a) [HasGhostArgumentType x g] : HasGhostArgumentType (liftM x) g

Equations

• DY.instHasGhostArgumentTypeLiftM x = { dummy := () }

@[instance_reducible]

instance DY.instHasIndirectGhostMetaprogramLiftM {metaprog : GhostParameterFinder} {m : Type u → Type v} {n : Type u → Type w} [MonadLift m n] {a : Type u} {b : Type z} (x : m a) (y : b) [HasIndirectGhostMetaprogram x metaprog y] : HasIndirectGhostMetaprogram (liftM x) metaprog y

Equations

• DY.instHasIndirectGhostMetaprogramLiftM x y = { dummy := () }

instance DY.instHoareTripleGhostLiftMOfWPLift [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {m : Type u → Type v} {n : Type u → Type w} [MonadLift m n] [WP m] [WP n] [wplift : WPLift m n] {a : Type u} {g : Type u_g} (x : m a) (ghost : g) (pre : ProofTrace → Prop) (post : a → ProofTrace → Prop) [HasGhostArgumentType x g] [ht : HoareTripleGhost x ghost pre post] : HoareTripleGhost (liftM x) ghost pre post

instance DY.instWPLiftErrTraceful [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] : WPLift Err Traceful

theorem DY.Traceful.bind_wp [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {a b : Type} {g : Type u_1} (ghost : g) (x : Traceful a) (f : a → Traceful b) (post_f : b → ProofTrace → Prop) (tr : ProofTrace) {pre_x : ProofTrace → Prop} {post_x : a → ProofTrace → Prop} [HasGhostArgumentType x g] [ht : HoareTripleGhost x ghost pre_x post_x] (pf_tr_inv : Trace.Invariant tr) (pf_pre_x : pre_x tr) (pf_next : ∀ (tr_mid : ProofTrace) (x' : a), post_x x' tr_mid → Trace.Invariant tr_mid → tr ≤ tr_mid → wp (f x') post_f tr_mid) : wp (x >>= f) post_f tr

theorem DY.Traceful.finish_wp [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {a : Type} {g : Type u_1} (ghost : g) (x : Traceful a) (post : a → ProofTrace → Prop) (tr : ProofTrace) {pre_x : ProofTrace → Prop} {post_x : a → ProofTrace → Prop} [HasGhostArgumentType x g] [ht : HoareTripleGhost x ghost pre_x post_x] (pf_tr_inv : Trace.Invariant tr) (pf_pre_x : pre_x tr) (pf_next : ∀ (tr_mid : ProofTrace) (x' : a), post_x x' tr_mid → Trace.Invariant tr_mid → tr ≤ tr_mid → post x' tr_mid) : wp x post tr

class DY.HoareTriplePureGhost {a : Sort u_1} {g : Type u_2} [ExecTraceTypes] [ProofTraceTypes] (x : a) [HasGhostArgumentType x g] (ghost : g) (pre : outParam (ProofTrace → Prop)) (post : outParam (a → ProofTrace → Prop)) : Prop

• pf (tr : ProofTrace) : pre tr → post x tr

class DY.HoareTriplePure {a : Sort u_1} [ExecTraceTypes] [ProofTraceTypes] (x : a) (pre : outParam (ProofTrace → Prop)) (post : outParam (a → ProofTrace → Prop)) : Prop

• pf (tr : ProofTrace) : pre tr → post x tr

@[instance_reducible]

instance DY.instHasGhostArgumentTypeUnitOfHoareTriplePure {a : Sort u_1} [ExecTraceTypes] [ProofTraceTypes] (x : a) (pre : ProofTrace → Prop) (post : a → ProofTrace → Prop) [HoareTriplePure x pre post] : HasGhostArgumentType x Unit

Equations

• DY.instHasGhostArgumentTypeUnitOfHoareTriplePure x pre post = { dummy := () }

instance DY.instHoareTriplePureGhostUnitUnit {a : Sort u_1} [ExecTraceTypes] [ProofTraceTypes] (x : a) (pre : ProofTrace → Prop) (post : a → ProofTrace → Prop) [HoareTriplePure x pre post] : HoareTriplePureGhost x () pre post

theorem DY.apply_hoare_triple_pure [ExecTraceTypes] [ProofTraceTypes] {a : Sort u_1} {g : Type u_2} (ghost : g) (x : a) {pre : ProofTrace → Prop} {post : a → ProofTrace → Prop} [HasGhostArgumentType x g] [ht : HoareTriplePureGhost x ghost pre post] (tr : ProofTrace) (p : pre tr) : post x tr

@[instance_reducible]

instance DY.instHasGhostArgumentTypeTracefulUnitGuardEqBoolTrueOfProofTraceTypes {g : Type u_1} [ExecTraceTypes] [ProofTraceTypes] (b : Bool) [HasGhostArgumentType b g] : HasGhostArgumentType (guard (b = true)) g

Equations

• DY.instHasGhostArgumentTypeTracefulUnitGuardEqBoolTrueOfProofTraceTypes b = { dummy := () }

@[instance_reducible]

instance DY.instHasIndirectGhostMetaprogramTracefulUnitGuardEqBoolTrueOfProofTraceTypes {metaprog : GhostParameterFinder} {b✝ : Sort u_1} {y : b✝} [ExecTraceTypes] [ProofTraceTypes] (b : Bool) [HasIndirectGhostMetaprogram b metaprog y] : HasIndirectGhostMetaprogram (guard (b = true)) metaprog y

Equations

• DY.instHasIndirectGhostMetaprogramTracefulUnitGuardEqBoolTrueOfProofTraceTypes b = { dummy := () }

instance DY.instHoareTripleGhostTracefulUnitGuardEqBoolTrueOfHoareTriplePureGhost {g : Type u_1} {ghost : g} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] (b : Bool) (pre : ProofTrace → Prop) (post : Bool → ProofTrace → Prop) [HasGhostArgumentType b g] [ht : HoareTriplePureGhost b ghost pre post] : HoareTripleGhost (guard (b = true)) ghost (fun (tr : ProofTrace) => pre tr) fun (x : Unit) (tr : ProofTrace) => post true tr

@[instance 100]

instance DY.instHoareTripleTracefulUnitGuardTrue [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] (b : Prop) [Decidable b] : HoareTriple (guard b) (fun (x : ProofTrace) => True) fun (x : Unit) (x_1 : ProofTrace) => b

instance DY.instHoareTripleTracefulPureTrueEq {a : Type} {x : a} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] : HoareTriple (pure x) (fun (x : ProofTrace) => True) fun (res : a) (x_1 : ProofTrace) => res = x

instance DY.instHoareTripleTracefulFailureTrue {a : Type} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] : HoareTriple failure (fun (x : ProofTrace) => True) fun (x : a) (x_1 : ProofTrace) => True

def DY.appendEntry [ExecTraceTypes] {EntryT : Type} [ExecTraceTypes.Has EntryT] (entry : EntryT) : Traceful Nat

Equations

• DY.appendEntry entry = DY.Traceful.mk fun (tr : DY.ExecTrace) => (some (DY.Trace.length tr), ⟨DY.Trace.append tr entry, ⋯⟩)

@[instance_reducible]

instance DY.instHasGhostArgumentTypeTracefulNatAppendEntryForallOfExecEntryAssociatedWithProofEntryOfHas [ExecTraceTypes] [ProofTraceTypes] {ExecEntryT ProofEntryT : Type} [ExecEntryAssociatedWithProofEntry ExecEntryT ProofEntryT] [ErasableProofEntry ExecEntryT ProofEntryT] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] (entry : ExecEntryT) : HasGhostArgumentType (appendEntry entry) (Nat → ProofEntryT)

Equations

• DY.instHasGhostArgumentTypeTracefulNatAppendEntryForallOfExecEntryAssociatedWithProofEntryOfHas entry = { dummy := () }

instance DY.appendEntry.spec [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {ExecEntryT ProofEntryT : Type} [ExecEntryAssociatedWithProofEntry ExecEntryT ProofEntryT] [ErasableProofEntry ExecEntryT ProofEntryT] [SubTraceInvariant ProofEntryT] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [TraceInvariant.Has ProofEntryT] (execEntry : ExecEntryT) (mkProofEntry : Nat → ProofEntryT) : HoareTripleGhost (appendEntry execEntry) mkProofEntry (fun (tr : ProofTrace) => ∀ (time : Nat), ErasableProofEntry.erase (mkProofEntry time) = execEntry ∧ SubTraceInvariant.invariant tr (mkProofEntry time)) fun (time : Nat) (tr : ProofTrace) => Trace.at? tr time = some (mkProofEntry time)

def DY.getEntry [ExecTraceTypes] {EntryT : Type} [ExecTraceTypes.Has EntryT] (timestamp : Nat) : Traceful EntryT

Equations

• DY.getEntry timestamp = DY.Traceful.mk fun (tr : DY.ExecTrace) => have result := DY.Trace.at? tr timestamp; (result, ⟨tr, ⋯⟩)

instance DY.getEntry.spec [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {ExecEntryT ProofEntryT : Type} [ExecEntryAssociatedWithProofEntry ExecEntryT ProofEntryT] [ErasableProofEntry ExecEntryT ProofEntryT] [SubTraceInvariant ProofEntryT] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [TraceInvariant.Has ProofEntryT] (timestamp : Nat) : HoareTriple (getEntry timestamp) (fun (x : ProofTrace) => True) fun (entry : ExecEntryT) (tr : ProofTrace) => ∃ (proofEntry : ProofEntryT), entry = ErasableProofEntry.erase proofEntry ∧ SubTraceInvariant.invariant (Trace.prefix tr timestamp) proofEntry

theorem DY.getEntry.preservesReachability [ExecTraceTypes] {ExecEntryT : Type} [ExecTraceTypes.Has ExecEntryT] (config : ReachabilityConfig) (timestamp : Nat) : Traceful.PreservesReachability config (getEntry timestamp) (fun (x : ExecTrace) => True) fun (entry : ExecEntryT) (tr : ExecTrace) => Trace.at? tr timestamp = some entry

def DY.getTimestamp [ExecTraceTypes] : Traceful Nat

Equations

• DY.getTimestamp = DY.Traceful.mk fun (tr : DY.ExecTrace) => (some (DY.Trace.length tr), ⟨tr, ⋯⟩)

instance DY.getTimestamp.spec [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] : HoareTriple getTimestamp (fun (x : ProofTrace) => True) fun (x : Nat) (x_1 : ProofTrace) => True

structure DY.LoopInvariantAndProof' [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {α : Type} {xs : List α} {β : Type} (f : (a : α) → a ∈ xs → β → Traceful (ForInStep β)) : Type

• inv : xs.Cursor × β → ProofTrace → Prop
• step (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β) : HoareTriple (f cur ⋯ b) (self.inv ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)) fun (r : ForInStep β) => match (motive := ForInStep β → ProofTrace → Prop) r with | ForInStep.yield b' => self.inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b') | ForInStep.done b' => self.inv ({ «prefix» := xs, suffix := [], property := ⋯ }, b')

@[instance_reducible]

instance DY.instHasGhostArgumentTypeTracefulForIn'ListLoopInvariantAndProof' [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {α β : Type} (xs : List α) (init : β) (f : (a : α) → a ∈ xs → β → Traceful (ForInStep β)) : HasGhostArgumentType (forIn' xs init f) (LoopInvariantAndProof' f)

Equations

• DY.instHasGhostArgumentTypeTracefulForIn'ListLoopInvariantAndProof' xs init f = { dummy := () }

instance DY.forIn'.spec [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {α β : Type} (xs : List α) (init : β) {f : (a : α) → a ∈ xs → β → Traceful (ForInStep β)} (invAndProof : LoopInvariantAndProof' f) : HoareTripleGhost (forIn' xs init f) invAndProof (invAndProof.inv ({ «prefix» := [], suffix := xs, property := ⋯ }, init)) fun (b : β) => invAndProof.inv ({ «prefix» := xs, suffix := [], property := ⋯ }, b)

structure DY.LoopInvariantAndProof [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {α : Type} (xs : List α) {β : Type} (f : α → β → Traceful (ForInStep β)) : Type

• inv : xs.Cursor × β → ProofTrace → Prop
• step (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β) : HoareTriple (f cur b) (self.inv ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)) fun (r : ForInStep β) => match (motive := ForInStep β → ProofTrace → Prop) r with | ForInStep.yield b' => self.inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b') | ForInStep.done b' => self.inv ({ «prefix» := xs, suffix := [], property := ⋯ }, b')

@[instance_reducible]

instance DY.instHasGhostArgumentTypeTracefulForInListLoopInvariantAndProof [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {α β : Type} (xs : List α) (init : β) (f : α → β → Traceful (ForInStep β)) : HasGhostArgumentType (forIn xs init f) (LoopInvariantAndProof xs f)

Equations

• DY.instHasGhostArgumentTypeTracefulForInListLoopInvariantAndProof xs init f = { dummy := () }

instance DY.forIn.spec [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {α β : Type} (xs : List α) (init : β) {f : α → β → Traceful (ForInStep β)} (invAndProof : LoopInvariantAndProof xs f) : HoareTripleGhost (forIn xs init f) invAndProof (invAndProof.inv ({ «prefix» := [], suffix := xs, property := ⋯ }, init)) fun (b : β) => invAndProof.inv ({ «prefix» := xs, suffix := [], property := ⋯ }, b)