Backwards wp steps on a Hoare triple

hoareWpStep k: split off the last k statements of a triple's statement (hoareSplit), close their triple by the wp rules (hoareWpFull), and simplify the reads in the resulting postcondition (simpReads). All three are meta-functions on goals, without tactic syntax.

theorem GaudisCrypt.intoLocal_varLens_get_resetSetter (n : String) (T : Type) (i : Nonempty T) (k : ℕ) (hk : k = VariableName.encode n) (S : Set String) (u : Unit) (σ : ProgramState) : (varLens { name := n, type := T, nonempty := i, key := k, keyCorrect := hk }).intoLocal.get ((resetSetter S).set u σ) = if n ∈ S then VariableAssignment.init { name := n, type := T, nonempty := i, key := k, keyCorrect := hk } else (varLens { name := n, type := T, nonempty := i, key := k, keyCorrect := hk }).intoLocal.get σ

A local variable read after a reset: its initial value if the reset covers its name, else what it was before. Unconditional, so that simp needs no discharger for it; the condition is decided afterwards, on the literal set the reset prints with. The slot is spelled with its fields and @Lens.intoLocal T, as a slot in a program is: stated for a variable v, the content type would be the projection v.type, which does not unify with T before v is known.

theorem GaudisCrypt.mem_stringsStartingWith_iff (p n : String) : n ∈ stringsStartingWith p ↔ p.toList <+: n.toList

Membership in a prefix region, as a statement about character lists that decide settles on literals. A rewrite of the membership only: unfolding stringsStartingWith itself would also change how the resets in the program print.

def GaudisCrypt.HoareWp.simpReadsDecls : List Lean.Name

The simp set of simpReads: theorems are rewritten with, definitions unfolded.

Equations

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

def GaudisCrypt.HoareWp.simpReads (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

Reads through writes, in the postcondition of a goal hoareStmt A s B (as hoare_assign_wp leaves it): liftLens of a program-state lens is the lens itself, Lens.pair splits a tuple write into one write per slot, eval_lens_full turns a read pinned at a written state into a get, a read of the written slot is the value (Lens.set_get), and a read of a disjoint slot ignores the write (Lens.get_of_disjoint_set; disjointness by instance search, so for slots with literal names), and a read after a reset is decided by whether the reset covers the name (intoLocal_varLens_get_resetSetter, then membership in the literal set the reset prints with, by decide). simp only with simpReadsDecls and the default simprocs.

Only the postcondition is rewritten: the same lemmas would also unfold the lenses of the statement itself (a tuple l-value into a raw Setter structure), which then no longer prints in the program syntax. Never fails; an unchanged goal is returned as is.

Equations

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

def GaudisCrypt.HoareWp.hoareWpStep (k : ℕ) (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

One backwards step on a goal hoareStmt A {x₁; …; xₙ} B: split off the last k statements (hoareSplit), close their triple by the wp rules, which fixes the intermediate condition (hoare_seq, hoareWpFull), and continue with the triple about x₁; …; xₙ₋ₖ, its postcondition simplified (simpReads). The last k statements must be straight-line code.

Equations

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

def GaudisCrypt.HoareWp.tacticHoare_wp_ : Lean.ParserDescr

hoare_wp k: hoareWpStep k on the main goal — split off the last k statements, close their triple by the wp rules, and simplify the reads in the new postcondition.

Equations

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

def GaudisCrypt.HoareWp.hoareSkip (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

The end of a backwards proof, on a goal hoareStmt A skip B (the statement possibly under its lets): the implication ∀ σ, A σ → B σ (hoare_skip_of_imp), with the reads of the state in it generalized to plain values (generalizeReads), if there are any.

Equations

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

def GaudisCrypt.HoareWp.tacticHoare_skip : Lean.ParserDescr

hoare_skip: hoareSkip on the main goal — from hoareStmt A skip B to ∀ x …, A → B with the reads of the state as plain values.

Equations

• GaudisCrypt.HoareWp.tacticHoare_skip = Lean.ParserDescr.node `GaudisCrypt.HoareWp.tacticHoare_skip 1024 (Lean.ParserDescr.nonReservedSymbol "hoare_skip" false)