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) : Type → Type

Equations

• GaudisCrypt.ProgramDenotation state = StateT state GaudisCrypt.SubProbability

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

Equations

• p.toProgramDenotation = StateT.lift p

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

Equations

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

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

Equations

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

noncomputable def GaudisCrypt.SubProbability.uniformOfFinset {α : Type} (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} (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 a : Type} (prog : ProgramDenotation s a) (st : s) (X : Set a) : NNReal

Equations

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

noncomputable instance GaudisCrypt.instOmegaCompletePartialOrderProgramDenotation {s a : Type} : 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} : Monad (ProgramDenotation s)

Equations

• GaudisCrypt.instMonadProgramDenotation = inferInstance

theorem GaudisCrypt.ProgramDenotation.bind_mono {i : Type u_1} {s a b : Type} [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 b c : Type} [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} (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} (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} (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} : ProgramDenotation s s

Equations

• GaudisCrypt.ProgramDenotation.get_state = StateT.get

class GaudisCrypt.AsGetter (T : Type) (a s : outParam Type) : Type

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) (a s : outParam Type) : Type

• toS : T → Setter a s

@[implicit_reducible]

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

Equations

• GaudisCrypt.instAsGetterGetter = { toG := id }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• GaudisCrypt.instAsSetterSetter = { toS := id }

@[implicit_reducible]

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

Equations

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

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

Equations

• GaudisCrypt.ProgramDenotation.set v x = do let st ← StateT.get have st' : s := (GaudisCrypt.AsSetter.toS v).set x st StateT.set st'

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

Equations

• GaudisCrypt.ProgramDenotation.get v = do let s_1 ← StateT.get pure ((GaudisCrypt.AsGetter.toG v).get s_1)

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

Equations

• GaudisCrypt.ProgramDenotation.skip = pure ()

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

Equations

• GaudisCrypt.ProgramDenotation.zoom lens p t_val = do let __discr ← p (lens.get t_val) match __discr with | (a_1, s') => pure (a_1, lens.set s' t_val)

Monad laws for ProgramDenotation s

theorem GaudisCrypt.ProgramDenotation.bind_assoc {s a b c : Type} (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 a b : Type} (x : a) (f : a → ProgramDenotation s b) : pure x >>= f = f x

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

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

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

zoom is a monad morphism

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

theorem GaudisCrypt.ProgramDenotation.zoom_bind {s t a b : Type} (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)