The types the guarded program declares

The emitted guarded program declares the types of the init items of the WP walk: a known type, or the type of a name resolved at emission (emit_tys). A WP walk declares as known types only declared types of the walked fragment and the Boolean type, records as declared types only those and the initial ones, and refers to the type of a name, directly or through a type reference of a fresh name, only for names that are no variable of the initial types or that the fragment reads or writes (TyInv, TyOut, wpList_tySpec). Hence every type the output of wpEntry declares is a declared type of the input, the Boolean type, or the type in tys of a variable the input reads or writes (wpEntry_initTypes).

Key definitions: wTyRefs, itemTys, RefOK, TyInv, TyOut, TySpec.

Key theorems: emit_tys, wpList_tySpec, wpEntry_initTypes.

Types of items

@[irreducible]

def Imperative.WP.wTyRefs {P : PureExpr} : List (WItem P) → List (TyRef P)

The type references of the init items of a list of guarded items, at any depth.

Equations

• Imperative.WP.wTyRefs [] = []
• Imperative.WP.wTyRefs (Imperative.WP.WItem.init x_1 ty e :: rest) = ty :: Imperative.WP.wTyRefs rest
• Imperative.WP.wTyRefs (Imperative.WP.WItem.branch t e :: rest) = Imperative.WP.wTyRefs t ++ Imperative.WP.wTyRefs e ++ Imperative.WP.wTyRefs rest
• Imperative.WP.wTyRefs (head :: rest) = Imperative.WP.wTyRefs rest

@[irreducible]

def Imperative.WP.itemTys {P : PureExpr} : List (Item P) → List P.Ty

The declared types of the statements of a list of flat items, at any depth.

Equations

• Imperative.WP.itemTys [] = []
• Imperative.WP.itemTys (Imperative.WP.Item.plain s :: rest) = Imperative.Stmt.initTypes s ++ Imperative.WP.itemTys rest
• Imperative.WP.itemTys (Imperative.WP.Item.obls reach cs :: rest) = Imperative.Block.initTypes cs ++ Imperative.WP.itemTys rest
• Imperative.WP.itemTys (Imperative.WP.Item.branch t e :: rest) = Imperative.WP.itemTys t ++ Imperative.WP.itemTys e ++ Imperative.WP.itemTys rest

theorem Imperative.WP.wTyRefs_append {P : PureExpr} (a b : List (WItem P)) : wTyRefs (a ++ b) = wTyRefs a ++ wTyRefs b

The type references of a concatenation are those of its parts.

theorem Imperative.WP.mergeObls_tys {P : PureExpr} [iDE : DecidableEq P.Ident] (l : List (Item P)) (ty : P.Ty) : ty ∈ itemTys (mergeObls l) → ty ∈ itemTys l

Merging adjacent obligation runs keeps the declared types of the items.

theorem Imperative.WP.nest_tys {P : PureExpr} [iHB : HasBool P] [iHF : HasFvar P] [iW : WPOps P] (l : List (Item P)) (ty : P.Ty) : ty ∈ Block.initTypes (nest l) → ty ∈ itemTys l

Every declared type of the nesting of flat items is one of the items.

def Imperative.WP.RefTy {P : PureExpr} [iBE : BEq P.Ident] [iHa : Hashable P.Ident] [iW : WPOps P] (T : Std.HashMap P.Ident P.Ty) (Y : Std.HashMap P.Ident P.Ident) (ty : P.Ty) : TyRef P → Prop

A resolved type reference: a known type, or the type tyOfName gives the name.

Equations

• Imperative.WP.RefTy T Y ty (Imperative.WP.TyRef.known ty') = (ty' = ty)
• Imperative.WP.RefTy T Y ty (Imperative.WP.TyRef.of y) = (Imperative.WP.tyOfName T Y y = Except.ok ty)

theorem Imperative.WP.resolveItems_tys {P : PureExpr} [iBE : BEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHa : Hashable P.Ident] [iW : WPOps P] {T : Std.HashMap P.Ident P.Ty} {Y : Std.HashMap P.Ident P.Ident} (l : List (WItem P)) (items : List (Item P)) : resolveItems T Y l = Except.ok items → ∀ (ty : P.Ty), ty ∈ itemTys items → ∃ (t : TyRef P), t ∈ wTyRefs l ∧ RefTy T Y ty t

Every declared type of resolved items resolves a type reference of the items.

theorem Imperative.WP.emit_tys {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHa : Hashable P.Ident] [iW : WPOps P] {T : Std.HashMap P.Ident P.Ty} {Y : Std.HashMap P.Ident P.Ident} {s : Strata.Util.Rope (WItem P)} {lay : BigStep.PStmts P} (h : emit T Y s = Except.ok lay) (ty : P.Ty) : ty ∈ Block.initTypes lay → ∃ (t : TyRef P), t ∈ wTyRefs s.toList ∧ RefTy T Y ty t

The declared types of the emitted guarded program resolve type references of the items of the rope.

The type facts of a walk

def Imperative.WP.RefOK {P : PureExpr} (K V : List P.Ident) (Θ : P.Ty → Prop) : TyRef P → Prop

A type reference allowed in the output of a walk: a known type satisfying Θ, or the type of a name that is in V when it is in K.

Equations

• Imperative.WP.RefOK K V Θ (Imperative.WP.TyRef.known ty') = Θ ty'
• Imperative.WP.RefOK K V Θ (Imperative.WP.TyRef.of y) = (y ∈ K → y ∈ V)

structure Imperative.WP.TyInv {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] (K V : List P.Ident) (Θ : P.Ty → Prop) (T0 : Std.HashMap P.Ident P.Ty) (st : WSt P) : Prop

The type facts of a walk state st, for the names K (the variables of the initial types) avoided by fresh names, the names V allowed among them, the allowed types Θ and the initial declared types T0: the Boolean type is allowed; the names of K are avoided and are no recorded renaming; a declared type is allowed or the initial one; the target of a type reference and of a carried merge is in V when it is in K.

• bool : Θ HasBool.boolTy
• av (k : P.Ident) : k ∈ K → st.avoid.contains k = true
• nm (x n : P.Ident) : st.nm[x]? = some n → ¬n ∈ K
• tys (k : P.Ident) (ty : P.Ty) : st.tys[k]? = some ty → Θ ty ∨ T0[k]? = some ty
• tyOf (k z : P.Ident) : st.tyOf[k]? = some z → z ∈ K → z ∈ V
• car (j : Nat) (q : P.Ident × WExpr P × P.Ident) : q ∈ st.carries.getD j [] → q.fst ∈ K → q.fst ∈ V

structure Imperative.WP.TyOut {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] (K V : List P.Ident) (Θ : P.Ty → Prop) (r : WRes P) : Prop

The type facts of a walk result r: its output holds only allowed type references (RefOK), and every name it assigns is in V when it is in K.

• refs (t : TyRef P) : t ∈ wTyRefs r.out.toList → RefOK K V Θ t
• A (n : P.Ident) : r.A.contains n = true → n ∈ K → n ∈ V

def Imperative.WP.TySpec {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] (K V : List P.Ident) (Θ : P.Ty → Prop) (T0 : Std.HashMap P.Ident P.Ty) (m : WM P (WRes P)) (ss : BigStep.PStmts P) : Prop

The type property of the walk m of a fragment ss: every run from a state with the type facts, of a fragment whose declared types are allowed, whose variables of K it reads or writes are in V, and which declares no name of K, ends in a state with the type facts and has a result with the type facts.

Equations

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

theorem Imperative.WP.TyInv.step {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} {st st' : WSt P} (h : TyInv K V Θ T0 st) (ha : st'.avoid = st.avoid) (hn : ∀ (x n : P.Ident), st'.nm[x]? = some n → st.nm[x]? = some n ∨ st.avoid.contains n = false) (ht : ∀ (k : P.Ident) (ty : P.Ty), st'.tys[k]? = some ty → st.tys[k]? = some ty ∨ Θ ty) (ho : ∀ (k z : P.Ident), st'.tyOf[k]? = some z → st.tyOf[k]? = some z ∨ (z ∈ K → z ∈ V)) (hc : ∀ (j : Nat) (q : P.Ident × WExpr P × P.Ident), q ∈ st'.carries.getD j [] → q ∈ st.carries.getD j [] ∨ (q.fst ∈ K → q.fst ∈ V)) : TyInv K V Θ T0 st'

A state with the avoided names of a state st with the type facts, whose renamings are those of st or names st does not avoid, and whose declared types, type references and carried merges are those of st or allowed ones, has the type facts.

theorem Imperative.WP.getElem?_insert_or {α β : Type} [BEq α] [Hashable α] [LawfulBEq α] {m : Std.HashMap α β} {a : α} {b : β} {Q : β → Prop} (hb : Q b) (k : α) (v : β) : (m.insert a b)[k]? = some v → m[k]? = some v ∨ Q v

A value of a hash map after an insertion of a value satisfying Q is a value before it or satisfies Q.

theorem Imperative.WP.wName_ty {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iL : LawfulHasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} {st st' : WSt P} {x n : P.Ident} (h : StateT.run (wName x) st = Except.ok (n, st')) (hi : TyInv K V Θ T0 st) : TyInv K V Θ T0 st' ∧ (n ∈ K → n = x)

A run of wName x keeps the type facts and returns x or a name not in K.

theorem Imperative.WP.wDecl_ty {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iL : LawfulHasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} {st st' : WSt P} {x n : P.Ident} (h : StateT.run (wDecl x) st = Except.ok (n, st')) (hi : TyInv K V Θ T0 st) : TyInv K V Θ T0 st'

A run of wDecl x keeps the type facts.

theorem Imperative.WP.wRen_ty {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iL : LawfulHasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} {st st' : WSt P} {e : P.Expr} {p : WExpr P × List P.Ident} (h : StateT.run (wRen e) st = Except.ok (p, st')) (hi : TyInv K V Θ T0 st) : TyInv K V Θ T0 st'

A run of wRen e keeps the type facts.

theorem Imperative.WP.liveAdd_ty {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} {st st' : WSt P} {xs : List P.Ident} {u : Unit} (h : StateT.run (liveAdd xs) st = Except.ok (u, st')) (hi : TyInv K V Θ T0 st) : TyInv K V Θ T0 st'

A run of liveAdd xs keeps the type facts.

theorem Imperative.WP.wFreshBool_ty {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} {st st' : WSt P} {n : P.Ident} {b : String} (h : StateT.run (wFreshBool b) st = Except.ok (n, st')) (hi : TyInv K V Θ T0 st) : TyInv K V Θ T0 st'

A run of wFreshBool b keeps the type facts.

theorem Imperative.WP.wFreshLike_ty {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} {st st' : WSt P} {n y : P.Ident} (h : StateT.run (wFreshLike y) st = Except.ok (n, st')) (hi : TyInv K V Θ T0 st) (hy : y ∈ K → y ∈ V) : TyInv K V Θ T0 st'

A run of wFreshLike y for a name y in V when it is in K keeps the type facts.

theorem Imperative.WP.saveRestore_ty {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} {st st' : WSt P} {xs : List P.Ident} {r : Strata.Util.Rope (WItem P) × Strata.Util.Rope (WItem P) × Strata.Util.Rope (WItem P) × List (P.Ident × P.Ident)} (h : StateT.run (saveRestore xs) st = Except.ok (r, st')) (hi : TyInv K V Θ T0 st) (hx : ∀ (y : P.Ident), y ∈ xs → y ∈ K → y ∈ V) : TyInv K V Θ T0 st' ∧ (∀ (t : TyRef P), t ∈ wTyRefs (r.fst.toList ++ r.snd.fst.toList ++ r.snd.snd.fst.toList) → RefOK K V Θ t) ∧ ∀ (p : P.Ident × P.Ident), p ∈ r.snd.snd.snd → p.fst ∈ xs

A run of saveRestore xs for names xs in V when they are in K keeps the type facts; its saves, copies and restores hold only references to the types of names of xs, and its copy pairs pair names of xs.

theorem Imperative.WP.tyOut_nil {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] {K V : List P.Ident} {Θ : P.Ty → Prop} {r : WRes P} (ho : r.out = Strata.Util.Rope.nil) (hA : r.A = ∅) : TyOut K V Θ r

A result without output and assigned names has the type facts.

theorem Imperative.WP.tySpec_cmd {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iL : LawfulHasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} (κ : RE P) (d : Nat) (f : Bool) (c : CmdExt P) : TySpec K V Θ T0 (wpStmt κ d f (Stmt.cmd c)) [Stmt.cmd c]

The walk of a command has the type property.

theorem Imperative.WP.setReach_refs {P : PureExpr} (κ : RE P) (X : WExpr P) : wTyRefs (setReach κ X).toList = []

The items of setReach κ X hold no type reference.

theorem Imperative.WP.tySpec_exit {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} (κ : RE P) (d : Nat) (f : Bool) (l : String) (md : MetaData P) : TySpec K V Θ T0 (wpStmt κ d f (Stmt.exit l md)) [Stmt.exit l md]

The walk of an exit has the type property.

theorem Imperative.WP.tySpec_other {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} (κ : RE P) (d : Nat) (f : Bool) (s : BigStep.PStmt P) (hs : (∀ (c : CmdExt P), s ≠ Stmt.cmd c) ∧ (∀ (l : String) (md : MetaData P), s ≠ Stmt.exit l md) ∧ (∀ (l : String) (b : List (Stmt P (CmdExt P))) (md : MetaData P), s ≠ Stmt.block l b md) ∧ ∀ (c : P.Expr) (t e : List (Stmt P (CmdExt P))) (md : MetaData P), s ≠ Stmt.ite (ExprOrNondet.det c) t e md) : TySpec K V Θ T0 (wpStmt κ d f s) [s]

The walk of a statement that is not a command, an exit, a block or a deterministic ite has the type property.

theorem Imperative.WP.tySpec_nil {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} (κ : RE P) (d : Nat) (fEnd : Bool) : TySpec K V Θ T0 (wpList κ d fEnd []) []

The walk of the empty list has the type property.

theorem Imperative.WP.tySpec_cons {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} {κ : RE P} {d : Nat} {fEnd : Bool} {s : BigStep.PStmt P} {rest : BigStep.PStmts P} (hs : ∀ (f : Bool), TySpec K V Θ T0 (wpStmt κ d f s) [s]) (hr : TySpec K V Θ T0 (wpList κ d fEnd rest) rest) : TySpec K V Θ T0 (wpList κ d fEnd (s :: rest)) (s :: rest)

The walk of s :: rest has the type property when the walks of s (for every obligation bit) and of rest have it.

theorem Imperative.WP.foldl_set_refs {P : PureExpr} {α : Type} (g : α → P.Ident) (v : α → Option (WExpr P)) (L : List α) (s : Strata.Util.Rope (WItem P)) : wTyRefs (List.foldl (fun (acc : Strata.Util.Rope (WItem P)) (x : α) => acc.app (Strata.Util.Rope.one (WItem.set (g x) (v x)))) s L).toList = wTyRefs s.toList

Appending set items to a rope adds no type reference.

theorem Imperative.WP.tySpec_block {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} {κ : RE P} {d : Nat} {f : Bool} {l : String} {body : BigStep.PStmts P} (md : MetaData P) (hB : ∀ (κB : RE P), TySpec K V Θ T0 (wpList κB (d + 1) f body) body) : TySpec K V Θ T0 (wpStmt κ d f (Stmt.block l body md)) [Stmt.block l body md]

The walk of a block has the type property when the walks of its body (at the next depth, under every context) have it.

theorem Imperative.WP.tySpec_iteReal {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iL : LawfulHasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} {κ : RE P} {d : Nat} {c : P.Expr} {tss ess : BigStep.PStmts P} (md : MetaData P) (hT : TySpec K V Θ T0 (wpList RE.top d false tss) tss) (hE : TySpec K V Θ T0 (wpList RE.top d false ess) ess) : TySpec K V Θ T0 (wpIteReal κ d c tss ess) [Stmt.ite (ExprOrNondet.det c) tss ess md]

The walk of a real branch has the type property when the walks of its arms (under top, no obligation following them) have it.

theorem Imperative.WP.optDraw_ty {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} {b : String} {s s' : WSt P} {o : Option P.Ident} (h : OptDraw b s s' o) (hi : TyInv K V Θ T0 s) : TyInv K V Θ T0 s'

An optional draw of a Boolean name keeps the type facts.

theorem Imperative.WP.mem_wTyRefs_flatMap {P : PureExpr} {α : Type} {f : α → List (WItem P)} {t : TyRef P} {L : List α} : t ∈ wTyRefs (List.flatMap f L) → ∃ (x : α), x ∈ L ∧ t ∈ wTyRefs (f x)

A type reference of the items of a flattened list is one of the items of an element.

theorem Imperative.WP.tySpec_iteLaid {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iL : LawfulHasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} {κ : RE P} {d : Nat} {c : P.Expr} {tss ess : BigStep.PStmts P} (md : MetaData P) (hT : ∀ (κ' : RE P), TySpec K V Θ T0 (wpList κ' d true tss) tss) (hE : ∀ (κ' : RE P), TySpec K V Θ T0 (wpList κ' d true ess) ess) : TySpec K V Θ T0 (wpIteLaid κ d c tss ess) [Stmt.ite (ExprOrNondet.det c) tss ess md]

The walk of a laid-out ite has the type property when the walks of its arms (at the same depth, under every context, an obligation following them) have it.

theorem Imperative.WP.wpList_tySpec {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} [LawfulHasIdent P] (ss : BigStep.PStmts P) (κ : RE P) (d : Nat) (fEnd : Bool) : TySpec K V Θ T0 (wpList κ d fEnd ss) ss

Every statement-list walk has the type property.

theorem Imperative.WP.wpStmt_tySpec {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {K V : List P.Ident} {Θ : P.Ty → Prop} {T0 : Std.HashMap P.Ident P.Ty} [LawfulHasIdent P] (s : BigStep.PStmt P) (κ : RE P) (d : Nat) (f : Bool) : TySpec K V Θ T0 (wpStmt κ d f s) [s]

Every statement walk has the type property.

theorem Imperative.WP.wpEntry_initTypes {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iHS : HasSubstFvar P] [iHI : HasIdent P] [iL : LawfulHasIdent P] [iHa : Hashable P.Ident] [iHV : HasFvars P] [iW : WPOps P] {G : IdSet P} {tys : Tys P} {ss : BigStep.PStmts P} {w : WOut P} (h : wpEntry G tys ss = Except.ok w) {Lc S : List P.Ident} (hwf : Block.WellScoped Lc S ss) (hS : ∀ (x : P.Ident), x ∈ List.map (fun (x : P.Ident × P.Ty) => x.fst) tys → x ∈ S) (ty : P.Ty) : ty ∈ Block.initTypes w.lay → ty ∈ Block.initTypes ss ∨ ty = HasBool.boolTy ∨ ∃ (x : P.Ident), x ∈ Block.freeVars ss ∧ tys.get? x = some ty

The types the output of the WP phase declares. For a loop-free list ss well scoped (Block.WellScoped) from a scope S containing the variables of tys, every type an init of the output of wpEntry declares is a declared type of ss, the Boolean type, or the type in tys of a variable that ss reads or writes (Block.freeVars).