Denotational equivalence of statements

StmtWithHoles.EquivInLens a b l: b, running on wide states, does what a does on the narrow state l projects to. StmtWithHoles.Equiv is the case l = Lens.id, plain denotational equivalence. The relation is a congruence for the statement formers, and a Hoare triple can be moved along it (hoareStmt_iff_of_equivInLens).

The statement rewriters (TacticMisc.flattenSeq, HoareSplit.splitSeq, the inliner in Inline.lean) prove their results equivalent to their inputs with these lemmas.

Lens helpers

def GaudisCrypt.Lens.chainGetter {a : Type u} {s : Type v} {t : Type w} (l : Lens s t) (g : Getter a s) : Getter a t

Compose a getter with a lens between its containers.

Equations

• l.chainGetter g = { get := fun (τ : t) => g.get (l.get τ) }

def GaudisCrypt.Lens.chainSetter {a : Type u} {s : Type v} {t : Type w} (l : Lens s t) (x : Setter a s) : Setter a t

Compose a setter with a lens between its containers.

Equations

• l.chainSetter x = { set := fun (v : a) (τ : t) => l.set (x.set v (l.get τ)) τ, set_set := ⋯ }

@[simp]

theorem GaudisCrypt.Lens.id_chain {a : Type u} {m : Type v} (y : Lens a m) : id.chain y = y

@[simp]

theorem GaudisCrypt.Lens.chain_id {a : Type u} {m : Type v} (x : Lens a m) : x.chain id = x

theorem GaudisCrypt.Lens.chain_assoc {a : Type u} {b : Type v} {c : Type w} {d : Type w'} (x : Lens c d) (y : Lens b c) (z : Lens a b) : (x.chain y).chain z = x.chain (y.chain z)

Chaining is associative.

Denotational equivalence along a lens

noncomputable def GaudisCrypt.SubProbability.mapState {α : Type v} {s t : Type u} (f : t → s) (μ : SubProbability (α × t)) : SubProbability (α × s)

Push a state map through a denotation's result: (u, τ) ↦ (u, f τ).

Equations

• GaudisCrypt.SubProbability.mapState f μ = (fun (p : α × t) => (p.1, f p.2)) <$> μ

def GaudisCrypt.ProgramDenotation.EquivInLens {s t : Type u} {α : Type v} (a : ProgramDenotation s α) (b : ProgramDenotation t α) (l : Lens s t) : Prop

b, running on the wide state t, is denotationally equivalent to a, running on the narrow state s, in the lens l : Lens s t: from any wide state, running b and projecting the result with l.get gives the same subdistribution as running a from the projected state.

Nothing is assumed about the part of the wide state that l does not see — in particular the frame of a flattened callee, which the flattened code resets before it reads it.

Equations

• a.EquivInLens b l = ∀ (sa : s) (sb : t), sa = l.get sb → GaudisCrypt.SubProbability.mapState l.get (b sb) = a sa

def GaudisCrypt.StmtWithHoles.EquivInLens {hCtx : HoleSigs} (a b : StmtWithHoles hCtx) (l : Lens ProgramState ProgramState) : Prop

The statement-level relation. programDenotation needs a hole-free statement and the rewrites here leave hole indices untouched, so the instantiation is quantified — the same one on both sides.

Equations

• a.EquivInLens b l = ∀ (inst : hCtx.Instantiation), (GaudisCrypt.programDenotation (a.instantiate inst)).EquivInLens (GaudisCrypt.programDenotation (b.instantiate inst)) l

@[reducible, inline]

abbrev GaudisCrypt.StmtWithHoles.Equiv {hCtx : HoleSigs} (a b : StmtWithHoles hCtx) : Prop

Denotational equivalence without renaming — what flattenSeq proves.

Equations

• a.Equiv b = a.EquivInLens b GaudisCrypt.Lens.id

The primitives, applied at a state

theorem GaudisCrypt.ProgramDenotation.get_apply' {s : Type u} {a : Type v} (g : Getter a s) (st : s) : get g st = pure (g.get st, st)

ProgramDenotation.get applied at a state — the Getter version of ProgramDenotation.get_apply (which is stated for a Lens).

theorem GaudisCrypt.ProgramDenotation.set_apply' {s : Type u} {a : Type v} (x : Setter a s) (v : a) (st : s) : set x v st = pure ((), x.set v st)

ProgramDenotation.set applied at a state — the Setter version of ProgramDenotation.set_apply (which is stated for a Lens).

EquivInLens is a congruence

What the flattener needs along the path down to the call it is rewriting.

theorem GaudisCrypt.SubProbability.mapState_eq {α : Type v} {s t : Type u} (f : t → s) (μ : SubProbability (α × t)) : mapState f μ = do let q ← μ pure (q.1, f q.2)

mapState spelled out as a bind, for rewriting.

theorem GaudisCrypt.ProgramDenotation.EquivInLens.pure {s t : Type u} {α : Type v} {l : Lens s t} (a : α) : (Pure.pure a).EquivInLens (Pure.pure a) l

pure is equivalent to itself.

theorem GaudisCrypt.ProgramDenotation.EquivInLens.bot {s t : Type u} {α : Type v} {l : Lens s t} : ⊥.EquivInLens ⊥ l

Diverging is equivalent to diverging.

theorem GaudisCrypt.ProgramDenotation.EquivInLens.get {s t : Type u} {α : Type v} (l : Lens s t) (g : Getter α s) : (ProgramDenotation.get g).EquivInLens (ProgramDenotation.get (l.chainGetter g)) l

Reading through the composed getter is equivalent to reading through the original one.

theorem GaudisCrypt.ProgramDenotation.EquivInLens.set {s t : Type u} {α : Type v} (l : Lens s t) (x : Setter α s) (v : α) : (ProgramDenotation.set x v).EquivInLens (ProgramDenotation.set (l.chainSetter x) v) l

Writing through the composed setter is equivalent to writing through the original one.

theorem GaudisCrypt.ProgramDenotation.EquivInLens.lift {s t : Type u} {α : Type v} (l : Lens s t) (μ : SubProbability α) : μ.toProgramDenotation.EquivInLens μ.toProgramDenotation l

A state-blind draw is equivalent to itself.

theorem GaudisCrypt.ProgramDenotation.EquivInLens.bind {s t : Type u} {α β : Type v} {l : Lens s t} {p : ProgramDenotation s α} {q : ProgramDenotation t α} {p' : α → ProgramDenotation s β} {q' : α → ProgramDenotation t β} (h : p.EquivInLens q l) (h' : ∀ (a : α), (p' a).EquivInLens (q' a) l) : (p >>= p').EquivInLens (q >>= q') l

Bind congruence — the seq case, and the heart of the path congruences. Note the continuation hypothesis is over wide states, which is exactly what EquivInLens provides.

theorem GaudisCrypt.SubProbability.mapState_mapState {α : Type v} {s t u : Type w} (f : u → t) (g : t → s) (μ : SubProbability (α × u)) : mapState g (mapState f μ) = mapState (fun (x : u) => g (f x)) μ

Projecting twice is projecting along the composite.

theorem GaudisCrypt.ProgramDenotation.EquivInLens.trans {s t u : Type w} {α : Type v} {l : Lens s t} {m : Lens t u} {p : ProgramDenotation s α} {q : ProgramDenotation t α} {r : ProgramDenotation u α} (h : p.EquivInLens q l) (h' : q.EquivInLens r m) : p.EquivInLens r (m.chain l)

Equivalences compose: through l, then through m, is through m.chain l.

theorem GaudisCrypt.SubProbability.mapState_ωScottContinuous {α : Type v} {s t : Type u} (f : t → s) : OmegaCompletePartialOrder.ωScottContinuous fun (μ : SubProbability (α × t)) => mapState f μ

mapState is ω-continuous — what the loop congruence needs.

theorem GaudisCrypt.ProgramDenotation.EquivInLens.ωSup {s t : Type u} {α : Type v} {l : Lens s t} (chP : OmegaCompletePartialOrder.Chain (ProgramDenotation s α)) (chQ : OmegaCompletePartialOrder.Chain (ProgramDenotation t α)) (h : ∀ (n : ℕ), (chP n).EquivInLens (chQ n) l) : (OmegaCompletePartialOrder.ωSup chP).EquivInLens (OmegaCompletePartialOrder.ωSup chQ) l

Equivalence passes to ω-suprema of chains — the limit step of the loop congruence.

theorem GaudisCrypt.ProgramDenotation.EquivInLens.while_loop {s t : Type u} {l : Lens s t} {cond : ProgramDenotation s Bool} {cond' : ProgramDenotation t Bool} {body : ProgramDenotation s Unit} {body' : ProgramDenotation t Unit} (hc : cond.EquivInLens cond' l) (hb : body.EquivInLens body' l) : (GaudisCrypt.while_loop cond body).EquivInLens (GaudisCrypt.while_loop cond' body') l

Loop congruence (Kleene/ωSup argument again): equivalent conditions and equivalent bodies give equivalent loops.

theorem GaudisCrypt.ProgramDenotation.EquivInLens.refl {s : Type u} {α : Type v} (p : ProgramDenotation s α) : p.EquivInLens p Lens.id

Every program is equivalent to itself, in the identity lens.

The same, at statement level

theorem GaudisCrypt.StmtWithHoles.EquivInLens.seq {hCtx : HoleSigs} {l : Lens ProgramState ProgramState} {a b a' b' : StmtWithHoles hCtx} (ha : a.EquivInLens a' l) (hb : b.EquivInLens b' l) : (a.seq b).EquivInLens (a'.seq b') l

Sequencing.

theorem GaudisCrypt.StmtWithHoles.EquivInLens.ifThenElse {hCtx : HoleSigs} {l : Lens ProgramState ProgramState} (c : Getter Bool ProgramState) {a b a' b' : StmtWithHoles hCtx} (ha : a.EquivInLens a' l) (hb : b.EquivInLens b' l) : (StmtWithHoles.ifThenElse c a b).EquivInLens (StmtWithHoles.ifThenElse (l.chainGetter c) a' b') l

Branching; the condition is re-targeted by composing it with the lens.

theorem GaudisCrypt.StmtWithHoles.EquivInLens.while {hCtx : HoleSigs} {l : Lens ProgramState ProgramState} (c : Getter Bool ProgramState) {b b' : StmtWithHoles hCtx} (hb : b.EquivInLens b' l) : (StmtWithHoles.while c b).EquivInLens (StmtWithHoles.while (l.chainGetter c) b') l

Looping; the condition is re-targeted by composing it with the lens.

theorem GaudisCrypt.StmtWithHoles.EquivInLens.trans {hCtx : HoleSigs} {l m : Lens ProgramState ProgramState} {a b c : StmtWithHoles hCtx} (h : a.EquivInLens b l) (h' : b.EquivInLens c m) : a.EquivInLens c (m.chain l)

Statement equivalences compose — how the flattener's passes are stitched together.

theorem GaudisCrypt.StmtWithHoles.Equiv.refl {hCtx : HoleSigs} (a : StmtWithHoles hCtx) : a.Equiv a

Reflexivity of the renaming-free relation.

theorem GaudisCrypt.StmtWithHoles.Equiv.seq_assoc {hCtx : HoleSigs} (a b c : StmtWithHoles hCtx) : ((a.seq b).seq c).Equiv (a.seq (b.seq c))

Sequencing is associative, denotationally.

Deterministic statements

theorem GaudisCrypt.programDenotation_assign_apply {a : Type} (y : Setter a ProgramState) (e : Getter a ProgramState) (τ : ProgramState) : programDenotation (StmtWithHoles.assign y e) τ = pure ((), y.set (e.get τ) τ)

An assignment, run at a state: a deterministic write.

theorem GaudisCrypt.programDenotation_assign {a : Type} (y : Setter a ProgramState) (e : Getter a ProgramState) : programDenotation (StmtWithHoles.assign y e) = do let v ← ProgramDenotation.get e ProgramDenotation.set y v

An assignment is a read followed by a write.

theorem GaudisCrypt.programDenotation_skip_apply (τ : ProgramState) : programDenotation StmtWithHoles.skip τ = pure ((), τ)

skip is the identity state map.

theorem GaudisCrypt.programDenotation_seq (a b : Stmt) : programDenotation (StmtWithHoles.seq a b) = do programDenotation a programDenotation b

Sequencing is bind.

theorem GaudisCrypt.programDenotation_seq_apply_det {a b : Stmt} {fa fb : ProgramState → ProgramState} (ha : ∀ (τ : ProgramState), programDenotation a τ = pure ((), fa τ)) (hb : ∀ (τ : ProgramState), programDenotation b τ = pure ((), fb τ)) (τ : ProgramState) : programDenotation (StmtWithHoles.seq a b) τ = pure ((), fb (fa τ))

Two deterministic statements in sequence: their state maps compose.

At the identity lens

What flattenSeq rewrites with (and StmtWithHoles.Equiv.seq_assoc, above).

theorem GaudisCrypt.StmtWithHoles.Equiv.skip_seq {hCtx : HoleSigs} (a : StmtWithHoles hCtx) : (skip.seq a).Equiv a

A leading skip can be dropped.

theorem GaudisCrypt.StmtWithHoles.Equiv.seq_skip {hCtx : HoleSigs} (a : StmtWithHoles hCtx) : (a.seq skip).Equiv a

A trailing skip can be dropped.

theorem GaudisCrypt.programDenotation_assign_throwaway {a : Type} (e : Getter a ProgramState) : programDenotation (StmtWithHoles.assign Setter.throwaway e) = ProgramDenotation.skip

An assignment to _ does nothing.

theorem GaudisCrypt.StmtWithHoles.Equiv.throwaway_seq {hCtx : HoleSigs} {α : Type} (e : Getter α ProgramState) (a : StmtWithHoles hCtx) : ((assign Setter.throwaway e).seq a).Equiv a

A leading assignment to _ can be dropped (a call with no parameters writes its argument () to _).

theorem GaudisCrypt.StmtWithHoles.Equiv.seq_throwaway {hCtx : HoleSigs} {α : Type} (a : StmtWithHoles hCtx) (e : Getter α ProgramState) : (a.seq (assign Setter.throwaway e)).Equiv a

A trailing assignment to _ can be dropped (a call whose result is discarded stores it to _).

theorem GaudisCrypt.StmtWithHoles.Equiv.ifThenElse {hCtx : HoleSigs} (c : Getter Bool ProgramState) {a b a' b' : StmtWithHoles hCtx} (ha : a.Equiv a') (hb : b.Equiv b') : (StmtWithHoles.ifThenElse c a b).Equiv (StmtWithHoles.ifThenElse c a' b')

Branching, at the identity lens.

theorem GaudisCrypt.StmtWithHoles.Equiv.while {hCtx : HoleSigs} (c : Getter Bool ProgramState) {b b' : StmtWithHoles hCtx} (hb : b.Equiv b') : (StmtWithHoles.while c b).Equiv (StmtWithHoles.while c b')

Looping, at the identity lens.

theorem GaudisCrypt.StmtWithHoles.Equiv.trans {hCtx : HoleSigs} {a b c : StmtWithHoles hCtx} (h : a.Equiv b) (h' : b.Equiv c) : a.Equiv c

Transitivity, at the identity lens (Lens.id.chain Lens.id is Lens.id).

theorem GaudisCrypt.StmtWithHoles.Equiv.symm {hCtx : HoleSigs} {a b : StmtWithHoles hCtx} (h : a.Equiv b) : b.Equiv a

Symmetry, at the identity lens (the one lens at which the relation is symmetric).

Hoare triples

A statement triple is a triple about any statement equivalent to its own, with the conditions read through the lens of the equivalence: so it can be proved about a rewritten statement instead (hoare_inline, hoare_split).

theorem GaudisCrypt.SubProbability.ofEvent_mapState {α : Type v} {s t : Type u} (f : t → s) (μ : SubProbability (α × t)) (E : Set (α × s)) : (mapState f μ).ofEvent E = μ.ofEvent ((fun (p : α × t) => (p.1, f p.2)) ⁻¹' E)

The chance of an event under mapState f μ is that of its preimage under μ.

theorem GaudisCrypt.hoareStmt_iff_of_equivInLens {A B : ProgramState → Prop} {s s' : Stmt} {l : Lens ProgramState ProgramState} (h : StmtWithHoles.EquivInLens s s' l) : hoareStmt A s B ↔ hoareStmt (fun (τ : ProgramState) => A (l.get τ)) s' fun (τ : ProgramState) => B (l.get τ)

A triple about an equivalent statement: along s.EquivInLens s' l, the triple about s is the triple about s' with both conditions read through l.

theorem GaudisCrypt.hoareStmt_of_equivInLens {A B A' B' : ProgramState → Prop} {s s' : Stmt} {l : Lens ProgramState ProgramState} (h : StmtWithHoles.EquivInLens s s' l) (hA : (fun (τ : ProgramState) => A (l.get τ)) = A') (hB : (fun (τ : ProgramState) => B (l.get τ)) = B') (h' : hoareStmt A' s' B') : hoareStmt A s B

hoareStmt_iff_of_equivInLens, backwards, with the conditions given up to an equation: what hoare_inline applies, the equations being those of the cleaning pass.

theorem GaudisCrypt.hoareStmt_of_equiv {A B : ProgramState → Prop} {s s' : Stmt} (h : StmtWithHoles.Equiv s s') (h' : hoareStmt A s' B) : hoareStmt A s B

A triple about an equivalent statement, without renaming: the conditions stay as they are.