Properties of the WP phase

The output of wpBody is a guarded program in which only obligations follow an assert (wpBody_shape), the output of wpEntry on a well-scoped list reads only variables the list reads (wpEntry_fv), and every arm of every ite of the output of wpEntry, at any depth, contains an assert or a cover (wpEntry_armsHaveObl).

The ites of the output come from the nesting of the flat items (nest): a side branch is the then arm of an ite whose else arm is the nesting of the rest of the list, and a real branch is an ite of the nestings of its arms. The proof of wpEntry_armsHaveObl shows that every run of obligations of the walk's output is nonempty, that every real branch has a run of obligations or a real branch in each arm, and that a walk result carrying an obligation has a run of obligations or a real branch in its output (ROK). It proves the facts about the walk along the computations of the WP monad: Post m Q says that every successful run of m returns a value with Q, and the tactic post_step decomposes such a goal along the binds, conditionals, matches and join points of a do block.

Key theorems: wpBody_shape, wpEntry_fv, wpEntry_armsHaveObl.

Shape of the output

theorem Imperative.WP.wpBody_shape {P : PureExpr} [iDE : DecidableEq P.Ident] [iB : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iBo : HasBool P] [iFv : HasFvar P] [iSu : HasSubstFvar P] [iId : HasIdent P] [iHa : Hashable P.Ident] [iFs : HasFvars P] [iW : WPLang P] {st : FreshSt P} {ss : BigStep.PStmts P} {w : WOut P} (h : wpBody st ss = Except.ok w) : Block.treeForm w.lay = true ∧ Block.onlyChecksAfterAssert w.lay = true

The output of the WP phase is a guarded program in which only obligations follow each assert in its list.

The names the output reads

theorem Imperative.WP.wpEntry_fv {P : PureExpr} [iDE : DecidableEq P.Ident] [iB : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iBo : HasBool P] [iFv : HasFvar P] [iSu : HasSubstFvar P] [iId : HasIdent P] [iLI : LawfulHasIdent P] [iHa : Hashable P.Ident] [iFs : HasFvars P] [iW : WPLang P] [LawfulHasVal P] [HasOps P] [LawfulHasFvar P] [LawfulHasFvars 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) (x : P.Ident) : x ∈ Block.freeVars w.lay → x ∈ Block.freeVars ss

The output of the WP phase of a well-scoped loop-free list reads only variables the list reads.

Obligations in every arm of the output

Flat items

Items before resolution

Successful runs of the WP monad

The walk

theorem Imperative.WP.wpEntry_armsHaveObl {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] {G : IdSet P} {tys : Tys P} {ss : BigStep.PStmts P} {w : WOut P} (h : wpEntry G tys ss = Except.ok w) : Block.armsHaveChecks w.lay = true

Every arm of every ite of the output of the WP phase, at any depth, contains an assert or a cover.