General stuff

@[reducible]

def GaudisCrypt.recursion {a : Type u_2} {b : a → Type u_1} [(x : a) → OmegaCompletePartialOrder (b x)] [(x : a) → OrderBot (b x)] (F : ((x : a) → b x) →𝒄 (x : a) → b x) (x : a) : b x

Equations

• GaudisCrypt.recursion F = F.lfp

Stateful programs

def GaudisCrypt.ProgramDenotation (state : Type u) (a : Type v) : Type (max u v)

A probabilistic program with state state and result a: from an initial state, a sub-distribution over results and final states.

This is StateT state SubProbability a unfolded, and deliberately not defined as that: StateT puts the state and the result in one universe, but a program's state lives in a higher universe than its results (variables are indexed by VariableName, which contains a Type, so VariableAssignment and ProgramState are in Type 1, while results are Unit, Bool, …). The Monad instance below and the instances after the monad laws are StateT's, written out. The state and the results have independent universes.

Equations

• GaudisCrypt.ProgramDenotation state a = (state → GaudisCrypt.SubProbability (a × state))

noncomputable def GaudisCrypt.SubProbability.toProgramDenotation {a : Type u_1} {s : Type u_2} (p : SubProbability a) : ProgramDenotation s a

Run a sub-probability as a program that leaves the state alone (StateT.lift). The bind is SubProbability.hbind since a and a × s may live in different universes.

Equations

• p.toProgramDenotation st = p.hbind fun (x : a) => pure (x, st)

noncomputable def GaudisCrypt.PMF.toProgramDenotation {st : Type u_1} {α : Type u_2} (p : PMF α) : ProgramDenotation st α

Equations

• GaudisCrypt.PMF.toProgramDenotation p = (GaudisCrypt.toSubProbability p).toProgramDenotation

noncomputable def GaudisCrypt.ProgramDenotation.uniform {α : Type u_1} {s : Type u_2} [h : Fintype α] : [Nonempty α] → ProgramDenotation s α

Equations

• GaudisCrypt.ProgramDenotation.uniform = GaudisCrypt.SubProbability.uniform.toProgramDenotation

noncomputable def GaudisCrypt.SubProbability.uniformOfFinset {α : Type u} (fs : Finset α) (hs : fs.Nonempty) : SubProbability α

Uniform subprobability over a nonempty finset.

Equations

• GaudisCrypt.SubProbability.uniformOfFinset fs hs = GaudisCrypt.toSubProbability (PMF.uniformOfFinset fs hs)

noncomputable def GaudisCrypt.ProgramDenotation.uniformOfFinset {s : Type u} {α : Type v} (fs : Finset α) (hs : fs.Nonempty) : ProgramDenotation s α

Uniform sampling over a nonempty finset (used e.g. for "sample without replacement" — uniform over the complement of the values seen so far).

Equations

• GaudisCrypt.ProgramDenotation.uniformOfFinset fs hs = (GaudisCrypt.SubProbability.uniformOfFinset fs hs).toProgramDenotation

def GaudisCrypt.ProgramDenotation.finalProb {s : Type u_1} {a : Type u_2} (prog : ProgramDenotation s a) (st : s) (X : Set a) : NNReal

Equations

• prog.finalProb st X = (prog st).ofEvent (X ×ˢ ⊤)

def GaudisCrypt.ProgramDenotation.finalProb1 {s : Type u_1} {a : Type u_2} (prog : ProgramDenotation s a) (st : s) (x : a) : NNReal

Equations

• prog.finalProb1 st x = prog.finalProb st {x}

@[implicit_reducible]

instance GaudisCrypt.instPartialOrderProgramDenotation {s : Type u_1} {a : Type u_2} : PartialOrder (ProgramDenotation s a)

Equations

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

@[implicit_reducible]

instance GaudisCrypt.instOrderBotProgramDenotation {s : Type u_1} {a : Type u_2} : OrderBot (ProgramDenotation s a)

Equations

• GaudisCrypt.instOrderBotProgramDenotation = { bot := fun (x : s) => ⟨0, ⋯⟩, bot_le := ⋯ }

@[implicit_reducible]

noncomputable instance GaudisCrypt.instOmegaCompletePartialOrderProgramDenotation {s : Type u_1} {a : Type u_2} : OmegaCompletePartialOrder (ProgramDenotation s a)

Equations

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

@[implicit_reducible]

noncomputable instance GaudisCrypt.instMonadProgramDenotation {s : Type u_1} : Monad (ProgramDenotation s)

Equations

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

theorem GaudisCrypt.ProgramDenotation.pure_apply {s : Type u} {a : Type v} (x : a) (st : s) : pure x st = pure (x, st)

pure, applied to a state. (What StateT.pure unfolded to.)

theorem GaudisCrypt.ProgramDenotation.bind_apply {s : Type u} {a b : Type v} (p : ProgramDenotation s a) (f : a → ProgramDenotation s b) (st : s) : (p >>= f) st = do let r ← p st f r.1 r.2

bind, applied to a state. (What StateT.bind unfolded to.)

@[implicit_reducible]

noncomputable instance GaudisCrypt.instMonadLiftSubProbabilityProgramDenotation {s : Type u} : MonadLift SubProbability (ProgramDenotation s)

Running a sub-probability as a program that leaves the state alone (StateT.lift).

Equations

• GaudisCrypt.instMonadLiftSubProbabilityProgramDenotation = { monadLift := fun {α : Type ?u.1} => GaudisCrypt.SubProbability.toProgramDenotation }

theorem GaudisCrypt.ProgramDenotation.toProgramDenotation_apply {s : Type u} {a : Type v} (μ : SubProbability a) (st : s) : μ.toProgramDenotation st = μ.hbind fun (x : a) => pure (x, st)

toProgramDenotation, applied to a state. (In one universe, SubProbability.hbind_eq_bind turns the hbind into >>=.)

theorem GaudisCrypt.ProgramDenotation.bind_mono {i : Type u_1} {s : Type u_2} {a b : Type u_3} [Preorder i] (f : i → ProgramDenotation s a) (g : i → a → ProgramDenotation s b) (hf : Monotone f) (hg : Monotone g) : Monotone fun (x : i) => f x >>= g x

theorem GaudisCrypt.ProgramDenotation.bind_ωScottContinuous {a : Type u_1} {s : Type u_2} {b c : Type u_3} [OmegaCompletePartialOrder a] (f : a → ProgramDenotation s b) (g : a → b → ProgramDenotation s c) (hg : OmegaCompletePartialOrder.ωScottContinuous g) (hf : OmegaCompletePartialOrder.ωScottContinuous f) : OmegaCompletePartialOrder.ωScottContinuous fun (x : a) => f x >>= g x

noncomputable def GaudisCrypt.while_iteration {s : Type u_1} (cond : ProgramDenotation s Bool) (body : ProgramDenotation s Unit) : (Unit → ProgramDenotation s Unit) →𝒄 Unit → ProgramDenotation s Unit

Equations

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

noncomputable def GaudisCrypt.while_loop {s : Type u_1} (cond : ProgramDenotation s Bool) (body : ProgramDenotation s Unit) : ProgramDenotation s Unit

Equations

• GaudisCrypt.while_loop cond body = GaudisCrypt.recursion (GaudisCrypt.while_iteration cond body) ()

theorem GaudisCrypt.while_unroll {s : Type u_1} (cond : ProgramDenotation s Bool) (body : ProgramDenotation s Unit) : while_loop cond body = do let __do_lift ← cond if __do_lift = true then do body while_loop cond body else pure ()

noncomputable def GaudisCrypt.ProgramDenotation.get_state {s : Type u_1} : ProgramDenotation s s

Equations

• GaudisCrypt.ProgramDenotation.get_state st = pure (st, st)

noncomputable def GaudisCrypt.ProgramDenotation.set_state {s : Type u_1} (st' : s) : ProgramDenotation s Unit

Overwrite the whole state.

Equations

• GaudisCrypt.ProgramDenotation.set_state st' x✝ = pure ((), st')

class GaudisCrypt.AsGetter (T : Type w) (a : outParam (Type u)) (s : outParam (Type v)) : Type (max (max u v) w)

ProgramDenotation.get/ProgramDenotation.set accept anything that forgets to a Getter/Setter — a Getter/Setter itself, or a full Lens/Variable. The value/state types are outParams recovered from the argument, which sidesteps the Lean 4.30 coercion that no longer fires when the value type is a metavariable.

• toG : T → Getter a s

class GaudisCrypt.AsSetter (T : Type w) (a : outParam (Type u)) (s : outParam (Type v)) : Type (max (max u v) w)

• toS : T → Setter a s

@[implicit_reducible]

instance GaudisCrypt.instAsGetterGetter {a : Type u} {s : Type v} : AsGetter (Getter a s) a s

Equations

• GaudisCrypt.instAsGetterGetter = { toG := id }

@[implicit_reducible]

instance GaudisCrypt.instAsGetterLens {a : Type u} {s : Type v} : AsGetter (Lens a s) a s

Equations

• GaudisCrypt.instAsGetterLens = { toG := GaudisCrypt.Lens.toGetter }

@[implicit_reducible]

instance GaudisCrypt.instAsSetterSetter {a : Type u} {s : Type v} : AsSetter (Setter a s) a s

Equations

• GaudisCrypt.instAsSetterSetter = { toS := id }

@[implicit_reducible]

instance GaudisCrypt.instAsSetterLens {a : Type u} {s : Type v} : AsSetter (Lens a s) a s

Equations

• GaudisCrypt.instAsSetterLens = { toS := GaudisCrypt.Lens.toSetter }

noncomputable def GaudisCrypt.ProgramDenotation.set {T : Type w} {a : Type u} {s : Type v} [AsSetter T a s] (v : T) (x : a) : ProgramDenotation s Unit

Equations

• GaudisCrypt.ProgramDenotation.set v x st = pure ((), (GaudisCrypt.AsSetter.toS v).set x st)

noncomputable def GaudisCrypt.ProgramDenotation.get {T : Type w} {a : Type u} {s : Type v} [AsGetter T a s] (v : T) : ProgramDenotation s a

Equations

• GaudisCrypt.ProgramDenotation.get v st = pure ((GaudisCrypt.AsGetter.toG v).get st, st)

noncomputable def GaudisCrypt.ProgramDenotation.skip {s : Type u_1} : ProgramDenotation s Unit

Equations

• GaudisCrypt.ProgramDenotation.skip = pure ()

noncomputable def GaudisCrypt.ProgramDenotation.zoom {s : Type u_1} {t : Type u_2} {a : Type u_3} (lens : Lens s t) (p : ProgramDenotation s a) : ProgramDenotation t a

Run p on the part of the state that lens selects. (s and t may live in different universes, hence SubProbability.hbind.)

Equations

• GaudisCrypt.ProgramDenotation.zoom lens p t_val = (p (lens.get t_val)).hbind fun (as : a × s) => pure (as.1, lens.set as.2 t_val)

Monad laws for ProgramDenotation s

theorem GaudisCrypt.ProgramDenotation.bind_assoc {s : Type u} {a b c : Type v} (p : ProgramDenotation s a) (f : a → ProgramDenotation s b) (g : b → ProgramDenotation s c) : p >>= f >>= g = p >>= fun (x : a) => f x >>= g

theorem GaudisCrypt.ProgramDenotation.pure_bind {s : Type u} {a b : Type v} (x : a) (f : a → ProgramDenotation s b) : pure x >>= f = f x

theorem GaudisCrypt.ProgramDenotation.bind_pure {s : Type u} {a : Type v} (m : ProgramDenotation s a) : m >>= pure = m

theorem GaudisCrypt.ProgramDenotation.bot_bind {s : Type u} {a b : Type v} (f : a → ProgramDenotation s b) : ⊥ >>= f = ⊥

theorem GaudisCrypt.ProgramDenotation.bind_bot {s : Type u} {a b : Type v} (m : ProgramDenotation s a) : (do let _ ← m ⊥) = ⊥

The instances StateT used to provide

instance GaudisCrypt.instLawfulMonadProgramDenotation {s : Type u} : LawfulMonad (ProgramDenotation s)

The monad laws. StateT would only have given this from a LawfulMonad SubProbability, which does not exist; here it comes from the three laws proved above.

@[implicit_reducible]

noncomputable instance GaudisCrypt.instMonadStateOfProgramDenotation {s : Type u} : MonadStateOf s (ProgramDenotation s)

Reading and writing the whole state (get/set/modify in do notation). Lean's MonadStateOf puts the state and the results in one universe, so this instance only exists for results in the state's universe.

Equations

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

zoom is a monad morphism

theorem GaudisCrypt.ProgramDenotation.zoom_pure {s : Type u} {t : Type v} {a : Type w} (lens : Lens s t) (x : a) : zoom lens (pure x) = pure x

theorem GaudisCrypt.ProgramDenotation.zoom_bind {s : Type u} {t : Type v} {a b : Type w} (lens : Lens s t) (p : ProgramDenotation s a) (k : a → ProgramDenotation s b) : zoom lens (p >>= k) = do let a ← zoom lens p zoom lens (k a)