Meta helpers for statement rewriting

Generic pieces of the statement-rewriting tactics: exposing a statement's head (openStmt), re-associating sequences (flattenSeq), and running a statement rewriter on the statement of a Hoare triple (hoareOnStmt). A rewriter returns its result together with a proof of StmtWithHoles.Equiv (Logic/StmtEquiv.lean). Users: Inline.lean and HoareSplit.lean.

Exposing statements

def GaudisCrypt.TacticMisc.stmtHeads : Array Lean.Name

The statement heads a traversal stops at. call is one: whnf would step through it to the call' it is defined as, which spreads the callee over several arguments and no longer prints as a call. applyLens and weaken are the inliner's (Inline.lean, which imports this file), and so are named unchecked.

Equations

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

def GaudisCrypt.TacticMisc.whnfNoZeta (e : Lean.Expr) : Lean.MetaM Lean.Expr

Head reduction that keeps lets: beta, iota and projections only.

Equations

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

partial def GaudisCrypt.TacticMisc.openStmt (e : Lean.Expr) : Lean.MetaM Lean.Expr

Expose a statement position: reduce until a statement head (or a let) is visible, without zeta-reducing and without stepping through assign or call.

def GaudisCrypt.TacticMisc.isSkip (e : Lean.Expr) : Bool

Is this skip?

Equations

• GaudisCrypt.TacticMisc.isSkip e = e.isAppOf `GaudisCrypt.StmtWithHoles.skip

def GaudisCrypt.TacticMisc.isThrowawayAssign (e : Lean.Expr) : Bool

Is this _ <- e, an assignment with no effect?

Equations

• GaudisCrypt.TacticMisc.isThrowawayAssign e = (e.isAppOfArity `GaudisCrypt.StmtWithHoles.assign 4 && (e.getArg! 2).isAppOf `GaudisCrypt.Setter.throwaway)

def GaudisCrypt.TacticMisc.mkEquivRefl (s : Lean.Expr) : Lean.MetaM Lean.Expr

a.Equiv a.

Equations

• GaudisCrypt.TacticMisc.mkEquivRefl s = Lean.Meta.mkAppM `GaudisCrypt.StmtWithHoles.Equiv.refl #[s]

flattenSeq

partial def GaudisCrypt.TacticMisc.concatSeq (a b : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Concatenate two already right-nested sequences, dropping skips and _ <- es: returns the result together with a proof of (a.seq b).Equiv result.

partial def GaudisCrypt.TacticMisc.flattenSeq (s₀ : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Re-associate seq to the right and drop skips and _ <- es, returning the result and a proof of ‹input›.Equiv result. Never fails; ifs are not otherwise touched.

Rewriting the statement of a triple

def GaudisCrypt.TacticMisc.hoareOnStmt (f : Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)) (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

On a goal hoareStmt A s B: rewrite the statement with f, which returns the new statement s' and a proof of s.Equiv s' (as flattenSeq and HoareSplit.splitSeq do), and continue with the triple about s'. The conditions are untouched — conv for the statement of a triple.

Equations

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

Weakest preconditions of straight-line statements

partial def GaudisCrypt.TacticMisc.hoareWpClose (g : Lean.MVarId) : Lean.MetaM Unit

Close a goal hoareStmt ?A s B, ?A a metavariable, by the wp rules: hoare_seq (the second statement first, which fixes the intermediate condition), hoare_assign_wp (resets included), hoare_sample_wp and hoare_skip_wp. ?A ends up assigned the weakest precondition. lets in the statement are zeta-reduced. Fails on anything else (call, if, while, holes).

def GaudisCrypt.TacticMisc.hoareWpFull (g : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

On a goal hoareStmt A s B with s straight-line code (assignments, resets, samplings, skip, in sequence): if A is a metavariable, close the goal and assign A the weakest precondition (hoareWpClose); otherwise reduce it, by hoare_pre, to the goal ∀ σ, A σ → wp σ, which is returned.

Equations

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

Reads of the state as plain values

What the Hoare rules leave is a goal ∀ σ, … x.get σ …: the state is only read, through lenses (local variables, globals, anything else). generalizeReads replaces each read by a universally quantified value, giving ∀ x, … x …; the same read, wherever it occurs, becomes the same value.

Only one direction is proved: the new goal implies the old one (a value for every read, not only the values some state has). So it is always sound, but the new goal can be strictly stronger: when σ is still used elsewhere (it then stays, ∀ σ x, …, with the link between x and σ cut), or when two of the lenses overlap (a variable and a pair containing it, say), since their values are then quantified independently. For distinct variables and no other use of σ, nothing is lost.

def GaudisCrypt.TacticMisc.readNameWrappers : List String

Wrappers a read is named through: the name comes from their last argument (the inner lens).

Equations

• GaudisCrypt.TacticMisc.readNameWrappers = ["chain", "chainGetter", "toGetter", "toG", "intoLocal", "intoGlobal", "liftLens"]

def GaudisCrypt.TacticMisc.readNameStoplist : List String

Generic combinators a read is not named after.

Equations

• GaudisCrypt.TacticMisc.readNameStoplist = ["mk", "pair", "fst", "snd", "id"]

def GaudisCrypt.TacticMisc.sanitizeName (s : String) : String

s as an identifier: only letters, digits, _ and ', not starting with a digit, and v if nothing is left (a made-up name like @.x becomes x).

Equations

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

partial def GaudisCrypt.TacticMisc.readBaseName (g : Lean.Expr) : Lean.MetaM String

A name for the value a read through the getter g yields: the variable's name for a local or global variable slot ((varLens ⟨n, …⟩).intoLocal / .intoGlobal, also spelled localVarLens n T); else, through the wrappers of readNameWrappers, the last component of the lens's head constant or the name of the local it is; else v.

def GaudisCrypt.TacticMisc.readBaseName.varName? (l : Lean.Expr) : Lean.MetaM (Option String)

Equations

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

def GaudisCrypt.TacticMisc.isStateOf (σ : Lean.FVarId) (s : Lean.Expr) : Bool

s is the state σ, or its globals or locals.

Equations

• GaudisCrypt.TacticMisc.isStateOf σ s = (s.isFVarOf σ || (s.isAppOfArity `GaudisCrypt.ProgramState.globals 1 || s.isAppOfArity `GaudisCrypt.ProgramState.locals 1) && s.appArg!.isFVarOf σ)

def GaudisCrypt.TacticMisc.readOfContainer (X x s : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

x.get s for x a lens or getter into ProgramState or VariableAssignment (its type X): a lens read through Lens.toGetter, and a read of the globals at s.globals. none for any other type.

Equations

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

partial def GaudisCrypt.TacticMisc.unfoldReadStep (σ : Lean.FVarId) (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

One step of unfoldReads at e, if a rule applies. Every rule is a definitional unfolding, and fires only on a read of the state σ itself:

• (Getter.mk f).get σ ↦ f σ, and a let of the CurrentState (as GaudiExpr[ ] binds it) is substituted;
• eval x in the current state ⟨σ⟩ ↦ x.get σ (or x.get σ.globals for a global);
• (AsGetter.toG x).get σ ↦ x.get σ;
• (x.pair y).get σ ↦ (x.get σ, y.get σ);
• (x.chain Lens.fst).get σ ↦ (x.get σ).1, and likewise for Lens.snd.

eval/CurrentState (Syntax/ExpressionSyntax.lean) are not imported here, so they are matched by name.

def GaudisCrypt.TacticMisc.unfoldReads (σ : Lean.FVarId) (e : Lean.Expr) : Lean.MetaM Lean.Expr

Unfold the reads of σ in e that are not reads of a lens or getter as it is, but of an expression built around them (unfoldReadStep), until none is left: what remains are reads x.get σ (or x.get σ.globals) of the lenses and getters themselves. A definitional rewrite.

Equations

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

partial def GaudisCrypt.TacticMisc.collectReadsOf (σ : Lean.FVarId) (e : Lean.Expr) (acc : Array Lean.Expr := #[]) : Array Lean.Expr

The reads Getter.get g s in e, s the state σ or its globals or locals, in order of appearance, without syntactic duplicates. Only closed ones (a read under a binder that mentions the bound variable cannot be generalized), and only through a getter that does not itself mention σ.

partial def GaudisCrypt.TacticMisc.binderNamesIn (e : Lean.Expr) (acc : Array String := #[]) : Array String

The binder names inside e, so that a new name does not shadow them.

def GaudisCrypt.TacticMisc.freshIn (used : Array String) (base : String) : String

base, or base1, base2, … if taken.

Equations

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

def GaudisCrypt.TacticMisc.generalizeReads (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

On a goal ∀ σ : ProgramState, P σ: first unfold the reads of σ through expressions, pairs and the like down to reads of lenses and getters (unfoldReads), then generalize every read g.get σ (or g.get σ.globals) to a universally quantified value (readBaseName, made unique against the context, the goal's binders and each other). Reads that agree up to reducible unfolding become one value. If σ is then unused it is dropped, giving ∀ m x …, P'; otherwise it stays in front, ∀ σ m x …, P'. With no read left, only the unfolding is done (and σ dropped if unused).

Equations

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