Facts about WP walk results #
Facts relating the result of a WP walk (wpList, wpStmt, wpIteLaid, wpIteReal) to the
walk state and to the loop-free runs of the walked fragment:
- only a main-list
exitdrops the rest of its list (wpStmt_drop,wpList_drop); - a reachable failing obligation makes the result carry an obligation (
wpList_hit_hasObl,noObl_claim); - a statement walked with an obligation following it does not always exit when it has a normal
run (
wpStmt_ax_normal); - the registrations of a result (exit snapshots, carried copies) are fresh names drawn by its
walk (
wpStmt_regs,wpList_regs), not dead after it (wpList_regs_live) and registered for at most one label (wpList_regs_one_label); the snapshots of a block's label not dead after the walk of its body are registrations of the body (body_snaps_regs); snapshots and dead names only grow by drawn names (wpList_pending_new,pending_regs,wpStmt_dead); - carried merges are only put in front, with registered or dead copies, at the depths of
enclosing blocks (
wpStmt_carries,body_carries), and target names that are no registrations or context variables (body_carries_names).
A successful walk of a laid-out ite has the steps of LaidSteps (wpIteLaid_inv), stated as
an elimination principle so that each proof about such a walk starts from its steps.
The facts about runs and dead names need the names marked dead to have counters below the
state's counter (DeadBelow, defined with the walk facts), which every walk keeps
(wpList_deadBelow) and a state without dead names has (deadBelow_of_dead_empty).
Key theorems: wpStmt_drop, wpList_drop, wpList_hit_hasObl, noObl_claim,
wpStmt_ax_normal, wpList_regs, wpList_regs_live, body_snaps_regs, wpList_regs_one_label,
pending_regs, wpList_deadBelow, wpStmt_carries, body_carries, body_carries_names,
wpIteLaid_inv.
State changes of walks #
n is a fresh name drawn between the states s and s': not avoided, with a counter from
s.next on and below s'.next.
Equations
Instances For
A name drawn between two states is drawn between any wider pair of states.
Runs of the state primitives #
Closes the result goal of a pure step of a Good decomposition.
Equations
- Imperative.WP.tacticGclose = Lean.ParserDescr.node `Imperative.WP.tacticGclose 1024 (Lean.ParserDescr.nonReservedSymbol "gclose" false)
Instances For
A one-element rope is not empty.
The walk state a block's body is walked from is well formed when the block's is.
A name is in a hash set after inserting the first components of a list exactly when it was before or is the first component of an element.
An element of a filtering fold over a hash set is an element of the set.
A selector condition of the guarded program: built from variables, literals and conditionals.
Equations
Instances For
The variables of an expression of the guarded program built without loop-free expressions.
Equations
Instances For
A concatenation fold is empty exactly when its start and all its operands are.
An optionally drawn name: none leaves the state unchanged, some x is drawn by
wFreshBool b.
Equations
- Imperative.WP.OptDraw b s s' none = (s' = s)
- Imperative.WP.OptDraw b s s' (some x_1) = (StateT.run (Imperative.WP.wFreshBool b) s = Except.ok (x_1, s'))
Instances For
The variable of an optional guard name, false without one.
Equations
Instances For
The copy pairs of cps whose carried merges an arm registers when o is the largest target
depth of its exits: the pairs whose variable is live in st before the clock at which the
walk entered the block at that depth.
Equations
- Imperative.WP.carryOf st cps (some t) = List.filter (fun (p : P.Ident × P.Ident) => Imperative.WP.liveBefore st p.fst (st.stampAt.getD t 0)) cps
- Imperative.WP.carryOf st cps none = []
Instances For
The carried merges C after registering at the depth o (if any) the merges
(x, ite(e, xB, x), xB) of the copy pairs (x, xB) of cps.
Equations
- One or more equations did not get rendered due to their size.
- Imperative.WP.carryIns e cps C none = C
Instances For
The guard of the carried merges of the else arm of a laid-out ite under the context κ,
with the optional merge guard gm and the optional else-arm carry guards qm, rEm.
Equations
- Imperative.WP.elseGuard Imperative.WP.RE.top gm qm rEm = (Imperative.WP.optVar gm).not
- Imperative.WP.elseGuard (Imperative.WP.RE.name r) gm (some qm_2) rEm = (Imperative.WP.WExpr.var qm_2).and (Imperative.WP.optVar gm).not
- Imperative.WP.elseGuard κ gm qm (some rEm_2) = Imperative.WP.WExpr.var rEm_2
- Imperative.WP.elseGuard κ gm qm rEm = Imperative.WP.WExpr.lit false
Instances For
The context of the else arm of a laid-out ite under κ, with guard g, drawn from s3
to s4: neg g under top, andNeg q g under name q, otherwise name x for a reach x
drawn for it, recorded in rE.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The steps of a successful run of a laid-out ite from s to s' with result r, as an
elimination principle (every Q that follows from the steps holds): the renaming of the
condition, the draws of the guard g and of the then-arm reach rT, the else-arm context
κE (LaidElseCtx), the runs of the arms, the three save/restore steps, the optional draws of
the merge guard gm (drawn exactly when needGm holds) and of the else-arm carry guards qm
(drawn exactly under name q when the else arm carries merges) and rEm (drawn exactly when
the else arm has a reach rE and carries merges), the registrations of the carried merges, and
the result.
Instances For
Every successful run of a laid-out ite has the steps of LaidSteps.
The registered copy pairs are copy pairs.
The carried merges at depth k after carryIns e cps C o are new merges in front of those
of C, the merges (x, ite(e, xB, x), xB) of copy pairs (x, xB) of cps, when o is
some k.
A successful walk of s :: rest walks rest, then s with the obligation bit of the rest,
and returns the result of s alone (after a drop, or after marking the registrations of the
rest dead when s always exits) or the combination of both results.
Drops #
Only a main-list exit (under the reach context top) drops the rest of its list.
A list walk that drops the rest of an enclosing list is under the reach context top.
The walk facts #
DeadBelow holds after a change keeping the dead names and not decreasing the counter.
Runs: normal ends, exit snapshots and reachable failures #
An outcome projected to an exit is an exit to the same label.
A body outcome that a block labelled l' turns into an exit to l is an exit to l ≠ l'.
The facts as stated for the users #
A walk state with no dead name has DeadBelow.
A list walk keeps DeadBelow.
The registrations of a statement walk's result are fresh names drawn by the walk: not avoided, with counters from the input counter on and below the output counter.
The registrations of a list walk's result are fresh names drawn by the walk: not avoided, with counters from the input counter on and below the output counter.
An exit snapshot registered for a label after a list walk was registered before it or is a fresh name drawn by the walk.
After the walks of rest and then of s, a registration of rest registered for a label
was registered for it before the walk of s.
A statement walk keeps the names marked dead, and marks dead only fresh names it draws.
A statement walked with an obligation following it (from a state with DeadBelow) that has
a normal run does not always exit.
A statement walk (from a state with DeadBelow) of a statement with a reach of a failing
target has an obligation.
A list walk (from a state with DeadBelow) of a list with a reach of a failing target has
an obligation.
A list walk (from a state with DeadBelow) whose result has no obligation reaches no failing
target of the list.
Registrations, snapshots and dead names #
The registrations of a list walk's result (from a state with DeadBelow) are not dead after
the walk.
For the walk of a block's body under a variable context, from a state with no snapshot for the block's label: the snapshots for the label that are not dead after the walk are registrations of the body.
Snapshots under one label #
A registration of a list walk's result, from a state whose snapshots of fresh-name form have counters below its counter, is registered after the walk for at most one label.
Carried merges #
An exit of an arm walk under a variable context with an obligation following (from a state
with DeadBelow whose label depths are at most d) to a label of the region at depth t
gives the walk a largest exit target K at least t, the depth of a label of the walk's
input state.
A carried merge registered by a list walk (from a well-formed state with DeadBelow whose
label depths are at most d, with no label under top) lies at a depth at most the walk's
largest exit target.
After the walks of rest and then of s at depth d (from a well-formed state whose label
depths are at most d), at each block depth, the carried merges of the output state of s
are new merges, with copies registered by s or dead, followed by those of its input state,
or neither state has a carried merge registered by rest at that depth.
For the walk of a block's body at depth d + 1 under a variable context, from a state with
no carried merge at depth d + 1 and label depths at most d + 1: the carried merges at
depth d + 1 that are not dead after the walk have copies registered by the body; and, when
the carried copies of the input state have counters below its counter, a carried merge whose
copy is registered by the body is at a depth at most d + 1.
The carried merges after the walk of a real branch are those before it.
Assigned names, merge targets and selector variables #
For the walk of a block's body at depth d + 1 from a well-formed state with no carried
merge at depth d + 1, whose names of D (holding the body's identifiers) are avoided if
they have the form of a fresh name, and whose reach context's variables are fresh names drawn
before, not avoided and no renamings: the targets of the merges at depth d + 1 not dead
after the walk are no registrations of the body; a carried merge whose copy is registered by
the body has a selector built from variables, literals and conditionals, reading no such
target and no variable of the context, and targets no variable of the context.
A list walk at depth d, from a state whose label depths are at most d, adds no carried
merge at a depth below d.