pRHL tactic layer (v1)

Lightweight sugar for the recurring proof moves observed in the validation clients:

• wp_peel — strip leading deterministic (set/get/pure) and uniform steps off a wp goal, turning them into state updates and uniform averages and stopping at the first non-atomic head (a loop, an adversary, …). This packages the "peel the synchronized prefix" pattern used by both clients: do-notation produces exactly the right-nested binds the peel lemmas match.
• rel_bind Mid — cut a relational goal at the leading bind with the given intermediate relation (EasyCrypt's seq tactic). The Mid annotation is mandatory by design: it is the specification of the cut, and implicit unification of it is non-Miller and unreliable.
• rel_step — try the structural/leaf relational rules in order (refl, pure, set, get, ite, uniform with the identity coupling, loop, while, one-sided sampling). Rules with side conditions leave them as goals.

Peel lemmas

theorem ProgramDenotation.wp_set_seq {s γ α : Type} (L : GaudisCrypt.Lens γ s) (v : γ) (P : GaudisCrypt.ProgramDenotation s α) (F : α × s → ENNReal) (σ : s) : (do GaudisCrypt.ProgramDenotation.set L v P).wp F σ = P.wp F (L.set v σ)

theorem ProgramDenotation.wp_get_seq {s γ α : Type} (L : GaudisCrypt.Lens γ s) (k : γ → GaudisCrypt.ProgramDenotation s α) (F : α × s → ENNReal) (σ : s) : (GaudisCrypt.ProgramDenotation.get L >>= k).wp F σ = (k (L.get σ)).wp F σ

theorem ProgramDenotation.wp_pure_seq {s α β : Type} (x : α) (k : α → GaudisCrypt.ProgramDenotation s β) (F : β × s → ENNReal) (σ : s) : (pure x >>= k).wp F σ = (k x).wp F σ

theorem ProgramDenotation.wp_uniform_seq {s α β : Type} [Fintype α] [Nonempty α] (k : α → GaudisCrypt.ProgramDenotation s β) (F : β × s → ENNReal) (σ : s) : (GaudisCrypt.ProgramDenotation.uniform >>= k).wp F σ = ∑ v : α, (k v).wp F σ / ↑(Fintype.card α)

Tactics

def tacticWp_peel : Lean.ParserDescr

Strip leading set/get/pure/uniform steps off wp goals.

Equations

• tacticWp_peel = Lean.ParserDescr.node `tacticWp_peel 1024 (Lean.ParserDescr.nonReservedSymbol "wp_peel" false)

def tacticRel_bind_ : Lean.ParserDescr

Cut a relE goal at the leading bind, with the given intermediate relation (EasyCrypt's seq). Produces the prefix judgment and the ∀-quantified continuation judgment as goals.

Equations

• tacticRel_bind_ = Lean.ParserDescr.node `tacticRel_bind_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "rel_bind" false) (Lean.ParserDescr.cat `term 0))

def tacticRel_bind_le_ : Lean.ParserDescr

Like rel_bind, for one-sided rel goals.

Equations

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

def tacticRel_step : Lean.ParserDescr

Try the structural/leaf relational rules; side conditions are left as goals. Runs at reducible transparency so failed candidates fail fast instead of unfolding program semantics.

Equations

• tacticRel_step = Lean.ParserDescr.node `tacticRel_step 1024 (Lean.ParserDescr.nonReservedSymbol "rel_step" false)

Smoke tests