Vocabulary of the WP and SSA phases (language-generic)

The WP phase (WP/WP.lean) turns a loop-free program (structured, without loops or calls, with deterministic guards) into a guarded program, and the SSA phase (SSA/SSA.lean) turns a guarded program into an obligation program (init/assume/assert/cover commands combined by nondeterministic ites, as consumed by obligation extraction), generic over the expression language P (see WPOps, WPLang). This file holds what both phases, their composition and their correctness statements share:

• renamings (Ren) and source-variable types (Tys);
• reachability conditions (RE): top, a Boolean name, the negation of a guard name, or the conjunction of a Boolean name with the negation of a guard name;
• the flat output (Item: straight-line statements, side branches of obligations under one reachability, real branches) and its nesting into a statement list (nest, computed in one pass by nestFast);
• the choice record of the SSA phase (LogEntry, substObl): the substitution under which each loop-free obligation is emitted;
• fresh names b@n (freshName) outside a two-level hash set of avoided names (AvoidSet, freshIn); baseOf strips the counter of a fresh name; the initial state of both phases (FreshSt: counter, avoided names, free-variable types) and the names a phase avoids for its input (inputAvoid).

Key definitions: RE, Item, nest, LogEntry, substObl, freshName, AvoidSet, freshIn, FreshSt, inputAvoid.

Names, renamings, expressions

@[reducible, inline]

abbrev Imperative.WP.Ren (P : PureExpr) : Type

A renaming: source variable → current SSA name (first binding wins; unbound variables are their own current name).

Equations

• Imperative.WP.Ren P = List (P.Ident × P.Ident)

def Imperative.WP.Ren.get {P : PureExpr} [BEq P.Ident] (ρ : Ren P) (x : P.Ident) : P.Ident

The current name of x under ρ.

Equations

• ρ.get x = match List.find? (fun (p : P.Ident × P.Ident) => p.fst == x) ρ with | some p => p.snd | none => x

def Imperative.WP.Ren.set {P : PureExpr} (ρ : Ren P) (x y : P.Ident) : Ren P

Rename x to y, shadowing earlier bindings of x.

Equations

• ρ.set x y = (x, y) :: ρ

@[reducible, inline]

abbrev Imperative.WP.Tys (P : PureExpr) : Type

Source-variable types.

Equations

• Imperative.WP.Tys P = List (P.Ident × P.Ty)

def Imperative.WP.Tys.get? {P : PureExpr} [BEq P.Ident] (tys : Tys P) (x : P.Ident) : Option P.Ty

The type recorded for x, if any (first binding wins).

Equations

• tys.get? x = Option.map (fun (x : P.Ident × P.Ty) => x.snd) (List.find? (fun (p : P.Ident × P.Ty) => p.fst == x) tys)

def Imperative.WP.contFV {P : PureExpr} [BEq P.Ident] [LawfulBEq P.Ident] [Hashable P.Ident] [HasFvars P] (k : List (BigStep.PStmts P)) : List P.Ident

Free variables of a continuation (a stack of statement lists).

Equations

• Imperative.WP.contFV k = Strata.Util.OrderedSet.eraseDups (List.flatMap Imperative.Block.freeVars k)

def Imperative.WP.isLocal {P : PureExpr} (ss : BigStep.PStmts P) : Bool

A branch is local when it consists only of assert/cover commands: skipping it on the continuation's path skips no evaluation, no assumption and no assignment, so it can become a side branch of its own.

Equations

• Imperative.WP.isLocal ss = List.all ss Imperative.Stmt.isCheck

Reachability conditions and the flat output

inductive Imperative.WP.RE (P : PureExpr) : Type

A reachability condition: top (reached whenever the enclosing path is), a Boolean name, the negation ¬g of a guard name, or q ∧ ¬g for a Boolean name q and a guard name g. Literals and negations are kept inline.

• top {P : PureExpr} : RE P
• name {P : PureExpr} (r : P.Ident) : RE P
• neg {P : PureExpr} (g : P.Ident) : RE P
• andNeg {P : PureExpr} (q g : P.Ident) : RE P

@[instance_reducible]

instance Imperative.WP.instInhabitedRE {a✝ : PureExpr} : Inhabited (RE a✝)

Equations

• Imperative.WP.instInhabitedRE = { default := Imperative.WP.instInhabitedRE.default }

@[instance_reducible]

instance Imperative.WP.instDecidableEqRE {P : PureExpr} [DecidableEq P.Ident] : DecidableEq (RE P)

Equations

• Imperative.WP.instDecidableEqRE Imperative.WP.RE.top Imperative.WP.RE.top = isTrue ⋯
• Imperative.WP.instDecidableEqRE (Imperative.WP.RE.name r) (Imperative.WP.RE.name r') = if h : r = r' then isTrue ⋯ else isFalse ⋯
• Imperative.WP.instDecidableEqRE (Imperative.WP.RE.neg g) (Imperative.WP.RE.neg g') = if h : g = g' then isTrue ⋯ else isFalse ⋯
• Imperative.WP.instDecidableEqRE (Imperative.WP.RE.andNeg q g) (Imperative.WP.RE.andNeg q' g') = if h : q = q' ∧ g = g' then isTrue ⋯ else isFalse ⋯
• Imperative.WP.instDecidableEqRE Imperative.WP.RE.top (Imperative.WP.RE.name r) = isFalse ⋯
• Imperative.WP.instDecidableEqRE Imperative.WP.RE.top (Imperative.WP.RE.neg g) = isFalse ⋯
• Imperative.WP.instDecidableEqRE Imperative.WP.RE.top (Imperative.WP.RE.andNeg q g) = isFalse ⋯
• Imperative.WP.instDecidableEqRE (Imperative.WP.RE.name r) Imperative.WP.RE.top = isFalse ⋯
• Imperative.WP.instDecidableEqRE (Imperative.WP.RE.name r) (Imperative.WP.RE.neg g) = isFalse ⋯
• Imperative.WP.instDecidableEqRE (Imperative.WP.RE.name r) (Imperative.WP.RE.andNeg q g) = isFalse ⋯
• Imperative.WP.instDecidableEqRE (Imperative.WP.RE.neg g) Imperative.WP.RE.top = isFalse ⋯
• Imperative.WP.instDecidableEqRE (Imperative.WP.RE.neg g) (Imperative.WP.RE.name r) = isFalse ⋯
• Imperative.WP.instDecidableEqRE (Imperative.WP.RE.neg g) (Imperative.WP.RE.andNeg q g_1) = isFalse ⋯
• Imperative.WP.instDecidableEqRE (Imperative.WP.RE.andNeg q g) Imperative.WP.RE.top = isFalse ⋯
• Imperative.WP.instDecidableEqRE (Imperative.WP.RE.andNeg q g) (Imperative.WP.RE.name r) = isFalse ⋯
• Imperative.WP.instDecidableEqRE (Imperative.WP.RE.andNeg q g) (Imperative.WP.RE.neg g_1) = isFalse ⋯

def Imperative.WP.RE.expr {P : PureExpr} [HasBool P] [HasFvar P] [WPOps P] : RE P → P.Expr

The Boolean expression of a reachability condition.

Equations

• Imperative.WP.RE.top.expr = Imperative.WP.tt
• (Imperative.WP.RE.name r).expr = Imperative.HasFvar.mkBoolVar r
• (Imperative.WP.RE.neg g).expr = Imperative.WP.notE (Imperative.HasFvar.mkBoolVar g)
• (Imperative.WP.RE.andNeg q g).expr = Imperative.WP.andE (Imperative.HasFvar.mkBoolVar q) (Imperative.WP.notE (Imperative.HasFvar.mkBoolVar g))

def Imperative.WP.RE.ite {P : PureExpr} [HasBool P] [HasFvar P] [WPOps P] (r : RE P) (t e : P.Expr) : P.Expr

ite(r, t, e) with the condition folded: t for top, ite(g, e, t) for ¬g, ite(q, ite(g, e, t), e) for q ∧ ¬g.

Equations

• Imperative.WP.RE.top.ite t e = t
• (Imperative.WP.RE.name r_1).ite t e = Imperative.WP.WPOps.ite (Imperative.HasFvar.mkBoolVar r_1) t e
• (Imperative.WP.RE.neg g).ite t e = Imperative.WP.WPOps.ite (Imperative.HasFvar.mkBoolVar g) e t
• (Imperative.WP.RE.andNeg q g).ite t e = Imperative.WP.WPOps.ite (Imperative.HasFvar.mkBoolVar q) (Imperative.WP.WPOps.ite (Imperative.HasFvar.mkBoolVar g) e t) e

def Imperative.WP.reachLabel : String

The label of generated reachability assumptions.

Equations

• Imperative.WP.reachLabel = "wp$reach"

def Imperative.WP.reachPre {P : PureExpr} [HasBool P] [HasFvar P] [WPOps P] : Option (RE P) → BigStep.PStmts P

The reachability assumption opening a side branch: none when always reached.

Equations

• Imperative.WP.reachPre none = []
• Imperative.WP.reachPre (some Imperative.WP.RE.top) = []
• Imperative.WP.reachPre (some r) = [Imperative.Stmt.cmd (Imperative.CmdExt.cmd (Imperative.Cmd.assume Imperative.WP.reachLabel r.expr Imperative.MetaData.empty))]

inductive Imperative.WP.Item (P : PureExpr) : Type

One element of the flat translation.

• plain {P : PureExpr} (s : BigStep.PStmt P) : Item P

  A straight-line statement of the obligation program.

• obls {P : PureExpr} (reach : Option (RE P)) (cs : BigStep.PStmts P) : Item P

  A side branch: the consecutive obligations cs under the reachability reach.

• branch {P : PureExpr} (t e : List (Item P)) : Item P

  A real branch: the flat translations t and e of the two arms of an ite after which no obligation follows. It ends the main path.

@[instance_reducible]

instance Imperative.WP.instInhabitedItem {a✝ : PureExpr} : Inhabited (Item a✝)

Equations

• Imperative.WP.instInhabitedItem = { default := Imperative.WP.instInhabitedItem.default }

def Imperative.WP.Item.isBranching {P : PureExpr} : Item P → Bool

Does the item leave the main path (a side branch or a real branch)?

Equations

• (Imperative.WP.Item.plain s).isBranching = false
• (Imperative.WP.Item.obls reach cs).isBranching = true
• (Imperative.WP.Item.branch t e).isBranching = true

def Imperative.WP.nest {P : PureExpr} [HasBool P] [HasFvar P] [WPOps P] : List (Item P) → BigStep.PStmts P

Turn the flat translation into the obligation program.

Equations

• Imperative.WP.nest [] = []
• Imperative.WP.nest (it :: rest) = Imperative.WP.nestCons it rest (Imperative.WP.nest rest)

def Imperative.WP.nestCons {P : PureExpr} [HasBool P] [HasFvar P] [WPOps P] : Item P → List (Item P) → BigStep.PStmts P → BigStep.PStmts P

nest (it :: rest), given nr = nest rest: a straight-line statement is kept when a branching item follows; a side branch becomes the then branch of a nondeterministic ite whose else branch is nr, and is inline when no branching item follows; a real branch becomes a nondeterministic ite of its nested arms, or the one nested arm that is not empty, and ends the list.

Equations

• One or more equations did not get rendered due to their size.
• Imperative.WP.nestCons (Imperative.WP.Item.plain s) x✝¹ x✝ = if x✝¹.any Imperative.WP.Item.isBranching = true then s :: x✝ else []

def Imperative.WP.nestB {P : PureExpr} [HasBool P] [HasFvar P] [WPOps P] : List (Item P) → BigStep.PStmts P × Bool

nest of an item list, with whether one of its items leaves the main path (Item.isBranching), in one pass over the list.

Equations

• Imperative.WP.nestB [] = ([], false)
• Imperative.WP.nestB (it :: rest) = match Imperative.WP.nestB rest with | (nr, b) => (Imperative.WP.nestConsB it b nr, it.isBranching || b)

def Imperative.WP.nestConsB {P : PureExpr} [HasBool P] [HasFvar P] [WPOps P] : Item P → Bool → BigStep.PStmts P → BigStep.PStmts P

nestCons it rest nr, given b, whether an item of rest leaves the main path.

Equations

• One or more equations did not get rendered due to their size.
• Imperative.WP.nestConsB (Imperative.WP.Item.plain s) x✝¹ x✝ = if x✝¹ = true then s :: x✝ else []

def Imperative.WP.nestFast {P : PureExpr} [HasBool P] [HasFvar P] [WPOps P] (l : List (Item P)) : BigStep.PStmts P

nest computed in one pass over the list (nestB).

Equations

• Imperative.WP.nestFast l = (Imperative.WP.nestB l).fst

@[csimp]

theorem Imperative.WP.nest_eq_nestFast : @nest = @nestFast

The compiled code of nest is nestFast, linear in the number of items where nest rescans the rest of the list at each item.

The choice record

inductive Imperative.WP.LogEntry (P : PureExpr) : Type

An entry of the record of the obligations the SSA phase emits.

• obl {P : PureExpr} (label : String) (sub : List (P.Ident × P.Ident × Option P.Ty)) : LogEntry P

  An obligation with label label, emitted on the SSA names: sub maps each renamed free variable x of its loop-free condition to its current name y and the type annotation ty of the emitted variable, so the emitted condition is the loop-free one with each such x replaced by y : ty (substObl), and the loop-free condition is the emitted one with sub inverted.

@[instance_reducible]

instance Imperative.WP.instInhabitedLogEntry {a✝ : PureExpr} : Inhabited (LogEntry a✝)

Equations

• Imperative.WP.instInhabitedLogEntry = { default := Imperative.WP.instInhabitedLogEntry.default }

def Imperative.WP.substObl {P : PureExpr} [HasFvar P] [HasSubstFvar P] (sub : List (P.Ident × P.Ident × Option P.Ty)) (e : P.Expr) : P.Expr

The condition an obligation of the obligation program has, for the loop-free condition e and the substitution sub of its choice-record entry: each x with (x, y, ty) in sub replaced by the variable y annotated ty.

Equations

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

Fresh names

def Imperative.WP.freshName {P : PureExpr} [HasIdent P] (b : String) (n : Nat) : P.Ident

The name the pass introduces with base b and counter n: b@n.

Equations

• Imperative.WP.freshName b n = Imperative.HasIdent.ident (b ++ "@" ++ toString n)

def Imperative.WP.joinLabel : String

The label of generated join assumptions.

Equations

• Imperative.WP.joinLabel = "wp$join"

def Imperative.WP.mkInit {P : PureExpr} (x : P.Ident) (ty : P.Ty) (e : ExprOrNondet P) : BigStep.PStmt P

The statement init x : ty := e.

Equations

• Imperative.WP.mkInit x ty e = Imperative.Stmt.cmd (Imperative.CmdExt.cmd (Imperative.Cmd.init x ty e Imperative.MetaData.empty))

def Imperative.WP.mkAssume {P : PureExpr} (l : String) (e : P.Expr) : BigStep.PStmt P

The statement assume l : e.

Equations

• Imperative.WP.mkAssume l e = Imperative.Stmt.cmd (Imperative.CmdExt.cmd (Imperative.Cmd.assume l e Imperative.MetaData.empty))

@[irreducible]

def Imperative.WP.stmtsInits {P : PureExpr} : BigStep.PStmts P → List P.Ident

The names declared by the inits of a list, at any depth.

Equations

• Imperative.WP.stmtsInits [] = []
• Imperative.WP.stmtsInits (Imperative.Stmt.cmd (Imperative.CmdExt.cmd (Imperative.Cmd.init x_1 ty e md)) :: rest) = x_1 :: Imperative.WP.stmtsInits rest
• Imperative.WP.stmtsInits (Imperative.Stmt.ite cond t e md :: rest) = Imperative.WP.stmtsInits t ++ Imperative.WP.stmtsInits e ++ Imperative.WP.stmtsInits rest
• Imperative.WP.stmtsInits (Imperative.Stmt.block label b md :: rest) = Imperative.WP.stmtsInits b ++ Imperative.WP.stmtsInits rest
• Imperative.WP.stmtsInits (Imperative.Stmt.loop guard measure invariants b md :: rest) = Imperative.WP.stmtsInits b ++ Imperative.WP.stmtsInits rest
• Imperative.WP.stmtsInits (head :: rest) = Imperative.WP.stmtsInits rest

@[reducible, inline]

abbrev Imperative.WP.IdSet (P : PureExpr) [DecidableEq P.Ident] [BEq P.Ident] [LawfulBEq P.Ident] [HasBool P] [HasFvar P] [HasSubstFvar P] [HasIdent P] [Hashable P.Ident] [HasFvars P] : Type

A hash set of identifiers.

Equations

• Imperative.WP.IdSet P = Std.HashSet P.Ident

def Imperative.WP.IdSet.ofList {P : PureExpr} [DecidableEq P.Ident] [BEq P.Ident] [LawfulBEq P.Ident] [HasBool P] [HasFvar P] [HasSubstFvar P] [HasIdent P] [Hashable P.Ident] [HasFvars P] (l : List P.Ident) : IdSet P

The hash set of the identifiers of a list.

Equations

• Imperative.WP.IdSet.ofList l = Std.HashSet.ofList l

structure Imperative.WP.AvoidSet (P : PureExpr) [DecidableEq P.Ident] [BEq P.Ident] [LawfulBEq P.Ident] [HasBool P] [HasFvar P] [HasSubstFvar P] [HasIdent P] [Hashable P.Ident] [HasFvars P] : Type

The names fresh names avoid, in two levels: the global names glob (built once per program and shared by its procedures) and the identifiers loc of one procedure.

• glob : IdSet P
• loc : IdSet P

def Imperative.WP.AvoidSet.contains {P : PureExpr} [DecidableEq P.Ident] [BEq P.Ident] [LawfulBEq P.Ident] [HasBool P] [HasFvar P] [HasSubstFvar P] [HasIdent P] [Hashable P.Ident] [HasFvars P] (a : AvoidSet P) (x : P.Ident) : Bool

Is x avoided?

Equations

• a.contains x = (Std.HashSet.contains a.glob x || Std.HashSet.contains a.loc x)

def Imperative.WP.AvoidSet.toList {P : PureExpr} [DecidableEq P.Ident] [BEq P.Ident] [LawfulBEq P.Ident] [HasBool P] [HasFvar P] [HasSubstFvar P] [HasIdent P] [Hashable P.Ident] [HasFvars P] (a : AvoidSet P) : List P.Ident

The avoided names, as a list.

Equations

• a.toList = Std.HashSet.toList a.glob ++ Std.HashSet.toList a.loc

def Imperative.WP.freeCounterIn {P : PureExpr} [DecidableEq P.Ident] [BEq P.Ident] [LawfulBEq P.Ident] [HasBool P] [HasFvar P] [HasSubstFvar P] [HasIdent P] [Hashable P.Ident] [HasFvars P] (avoid : AvoidSet P) (b : String) : Nat → Nat → Nat

The first counter from n (within fuel tries) whose name with base b is not avoided.

Equations

• Imperative.WP.freeCounterIn avoid b 0 x✝ = x✝
• Imperative.WP.freeCounterIn avoid b fuel.succ x✝ = if avoid.contains (Imperative.WP.freshName b x✝) = true then Imperative.WP.freeCounterIn avoid b fuel (x✝ + 1) else x✝

def Imperative.WP.freshIn {P : PureExpr} [DecidableEq P.Ident] [BEq P.Ident] [LawfulBEq P.Ident] [HasBool P] [HasFvar P] [HasSubstFvar P] [HasIdent P] [Hashable P.Ident] [HasFvars P] (avoid : AvoidSet P) (b : String) (n : Nat) : P.Ident × Nat

A fresh name with base b from counter n: freshName b k for the least k ≥ n whose name is not avoided, and the counter advanced past it.

Equations

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

def Imperative.WP.baseOf {P : PureExpr} [WPOps P] (x : P.Ident) : String

The base of a name: the name without one trailing @digits (the counter of a fresh name).

Equations

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

structure Imperative.WP.FreshSt (P : PureExpr) [DecidableEq P.Ident] [BEq P.Ident] [LawfulBEq P.Ident] [HasBool P] [HasFvar P] [HasSubstFvar P] [HasIdent P] [Hashable P.Ident] [HasFvars P] : Type

The initial state of the WP and SSA phases: fresh-name counter, avoided names, types of the free variables.

• next : Nat
• avoid : AvoidSet P
• tys : Tys P

def Imperative.WP.inputAvoid {P : PureExpr} [DecidableEq P.Ident] [BEq P.Ident] [LawfulBEq P.Ident] [HasBool P] [HasFvar P] [HasSubstFvar P] [HasIdent P] [Hashable P.Ident] [HasFvars P] (G : IdSet P) (tys : Tys P) (ss : BigStep.PStmts P) : AvoidSet P

The names a phase avoids for its input ss with free-variable types tys: the names of G (the names of the enclosing program), the identifiers of ss and the free variables.

Equations

• Imperative.WP.inputAvoid G tys ss = { glob := G, loc := Imperative.WP.IdSet.ofList (Imperative.Block.idents ss ++ List.map (fun (x : P.Ident × P.Ty) => x.fst) tys) }