structure GaudisCrypt.InductiveFunction [ProgramSpec] (t : Sort u_2) : Sort (max (max 2 (u_1 + 1)) u_2)

• nothing : t
• join : t → t → t
• proc {holes : HoleSigs} {sig : ProcedureSignature} (p : ProcedureWithHoles holes sig) : t

class GaudisCrypt.Reducible [ProgramSpec] {t : Type u_2} (ind : InductiveFunction t) extends Preorder t, Std.Commutative ind.join, Std.Associative ind.join : Type u_2

• le : t → t → Prop
• lt : t → t → Prop
• le_refl (a : t) : a ≤ a
• le_trans (a b c : t) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : t) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• comm (a b : t) : ind.join a b = ind.join b a
• assoc (a b c : t) : ind.join (ind.join a b) c = ind.join a (ind.join b c)
• join_mono_left {a a' b : t} : a' ≤ a → ind.join a' b ≤ ind.join a b
• join_mono_right {a b b' : t} : b' ≤ b → ind.join a b' ≤ ind.join a b
• le_join_left (a b : t) : a ≤ ind.join a b
• le_join_right (a b : t) : b ≤ ind.join a b
• join_idem (x : t) : ind.join x x ≤ x
• delta_bound {holes : HoleSigs} {sig : ProcedureSignature} (proc : ProcedureWithHoles holes sig) (args : holes.Instantiation) : ind.proc (proc.instantiate fun {sig : ProcedureSignature} => args) ≤ List.foldr (fun (p : (sig : ProcedureSignature) × Procedure sig) (acc : t) => ind.join (ind.proc p.snd) acc) (ind.proc proc) args.toList

def GaudisCrypt.InductiveFunction.evalInstantiationFold [ProgramSpec] {t : Type u_2} (ind : InductiveFunction t) {holes : HoleSigs} (inst : holes.Instantiation) : t

Evaluate an instantiation (a dependent tuple of procedures) by folding over the list inst.toList.

This matches the evaluation of inst.toModuleTuple under evalMexpr (see evalMexpr_toModuleTuple).

Equations

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

def GaudisCrypt.InductiveFunction.evalMexpr [ProgramSpec] {t : Sort u_2} (ind : InductiveFunction t) (m : ModuleExpression) : t

Equations

• ind.evalMexpr (GaudisCrypt.ModuleExpression.proc p) = ind.proc p
• ind.evalMexpr (GaudisCrypt.ModuleExpression.procHoles a p) = ind.proc p
• ind.evalMexpr (GaudisCrypt.ModuleExpression.var a) = ind.nothing
• ind.evalMexpr (m_2.app n) = ind.join (ind.evalMexpr m_2) (ind.evalMexpr n)
• ind.evalMexpr m_2.fst = ind.evalMexpr m_2
• ind.evalMexpr m_2.snd = ind.evalMexpr m_2
• ind.evalMexpr m_2.abs = ind.evalMexpr m_2
• ind.evalMexpr (m_2.pair n) = ind.join (ind.evalMexpr m_2) (ind.evalMexpr n)
• ind.evalMexpr GaudisCrypt.ModuleExpression.unit = ind.nothing

theorem GaudisCrypt.InductiveFunction.evalMexpr_rename [ProgramSpec] {t : Type u_1} (ind : InductiveFunction t) (m : ModuleExpression) (ρ : ℕ → ℕ) : ind.evalMexpr (ModuleExpression.rename ρ m) = ind.evalMexpr m

theorem GaudisCrypt.InductiveFunction.join_join_right_join_of_idem [ProgramSpec] {t : Type u_1} (ind : InductiveFunction t) [Reducible ind] (join_idem : ∀ (x : t), ind.join x x ≤ x) (x y e : t) : ind.join (ind.join x e) (ind.join y e) ≤ ind.join (ind.join x y) e

theorem GaudisCrypt.InductiveFunction.evalMexpr_substituteSimultaneously_le [ProgramSpec] {t : Type u_1} (ind : InductiveFunction t) [Reducible ind] (m : ModuleExpression) (σ : ℕ → ModuleExpression) (extra : t) : (∀ (n : ℕ), ind.evalMexpr (σ n) ≤ ind.join ind.nothing extra) → ind.evalMexpr (ModuleExpression.substituteSimultaneously σ m) ≤ ind.join (ind.evalMexpr m) extra

theorem GaudisCrypt.InductiveFunction.evalMexpr_substitute_le [ProgramSpec] {t : Type u_1} (ind : InductiveFunction t) [Reducible ind] (body arg : ModuleExpression) : ind.evalMexpr (body.substitute arg) ≤ ind.join (ind.evalMexpr body) (ind.evalMexpr arg)

def GaudisCrypt.InductiveFunction.eval' [ProgramSpec] {t : Sort u_2} {mt : ModuleTypeRep} (ind : InductiveFunction t) (m : Module mt) : t

Equations

• ind.eval' m = ind.evalMexpr m.expression

def GaudisCrypt.InductiveFunction.eval [ProgramSpec] {M : Type (max 1 u_1)} {t : Sort u_2} (ind : InductiveFunction t) [i : IsModule M] (m : M) : t

Equations

• ind.eval m = ind.eval' (GaudisCrypt.Module.cast M m)

theorem GaudisCrypt.InductiveFunction.evalMexpr_toModuleTuple [ProgramSpec] {t : Type u_1} (ind : InductiveFunction t) {holes : HoleSigs} (inst : holes.Instantiation) : ind.evalMexpr (HoleSigs.Instantiation.toModuleExpr fun {sig : ProcedureSignature} => inst) = ind.evalInstantiationFold fun {sig : ProcedureSignature} => inst

theorem GaudisCrypt.eval_induction_step [ProgramSpec] {t : Type u_1} (ind : InductiveFunction t) [Reducible ind] {m m' : ModuleExpression} (h : m.ReductionStep m') : ind.evalMexpr m' ≤ ind.evalMexpr m

theorem GaudisCrypt.evalMexpr_reduce [ProgramSpec] {t : Type u_1} (ind : InductiveFunction t) [Reducible ind] (m : ModuleExpression) (h : m.Terminating) : ind.evalMexpr m.reduce ≤ ind.evalMexpr m

theorem GaudisCrypt.evalMexpr_upper_bound [ProgramSpec] {t : Type u_1} {mt : ModuleTypeRep} (ind : InductiveFunction t) [Reducible ind] {m : ModuleExpression} (h : m.HasType [] mt) : ind.eval (m.toModule h) ≤ ind.evalMexpr m

theorem GaudisCrypt.InductiveFunction.app_moduleExpression [ProgramSpec] {t : Sort u_1} (ind : InductiveFunction t) (a b : ModuleExpression) : ind.evalMexpr (a.app b) = ind.join (ind.evalMexpr a) (ind.evalMexpr b)

theorem GaudisCrypt.InductiveFunction.app' [ProgramSpec] {t : Type u_1} {A B : ModuleTypeRep} (ind : InductiveFunction t) [Reducible ind] (a : Module (A.arr B)) (b : Module A) : ind.eval' (a.app' b) ≤ ind.join (ind.eval a) (ind.eval b)

theorem GaudisCrypt.InductiveFunction.app [ProgramSpec] {t : Type u_1} {A B : Type (max 1 u_2)} (ind : InductiveFunction t) [Reducible ind] [IsModule A] [IsModule B] (a : Module.Arr A B) (b : A) : ind.eval (Module.app a b) ≤ ind.join (ind.eval a) (ind.eval b)

theorem GaudisCrypt.InductiveFunction.pair_moduleExpression [ProgramSpec] {t : Sort u_1} (ind : InductiveFunction t) (a b : ModuleExpression) : ind.evalMexpr (a.pair b) = ind.join (ind.evalMexpr a) (ind.evalMexpr b)

theorem GaudisCrypt.InductiveFunction.pair' [ProgramSpec] {t : Sort u_1} {A B : ModuleTypeRep} (ind : InductiveFunction t) (a : Module A) (b : Module B) : ind.eval' (a.pair' b) = ind.join (ind.eval' a) (ind.eval' b)

theorem GaudisCrypt.InductiveFunction.pair [ProgramSpec] {t : Sort u_1} {A B : Type (max 1 u_2)} (ind : InductiveFunction t) [IsModule A] [IsModule B] (a : A) (b : B) : ind.eval (Module.pair a b) = ind.join (ind.eval a) (ind.eval b)

@[simp]

theorem GaudisCrypt.InductiveFunction.fst_moduleExpression [ProgramSpec] {t : Sort u_1} (ind : InductiveFunction t) (a : ModuleExpression) : ind.evalMexpr a.fst = ind.evalMexpr a

theorem GaudisCrypt.InductiveFunction.fst' [ProgramSpec] {t : Type u_1} {A B : ModuleTypeRep} (ind : InductiveFunction t) [Reducible ind] (a : Module (A.prod B)) : ind.eval' a.fst' ≤ ind.eval a

theorem GaudisCrypt.InductiveFunction.fst [ProgramSpec] {t : Type u_1} {A B : Type (max 1 u_2)} (ind : InductiveFunction t) [Reducible ind] [IsModule A] [IsModule B] (a : Module.Prod A B) : ind.eval (Module.fst a) ≤ ind.eval a

@[simp]

theorem GaudisCrypt.InductiveFunction.snd_moduleExpression [ProgramSpec] {t : Sort u_1} (ind : InductiveFunction t) (a : ModuleExpression) : ind.evalMexpr a.snd = ind.evalMexpr a

theorem GaudisCrypt.InductiveFunction.snd' [ProgramSpec] {t : Type u_1} {A B : ModuleTypeRep} (ind : InductiveFunction t) [Reducible ind] (a : Module (A.prod B)) : ind.eval' a.snd' ≤ ind.eval a

theorem GaudisCrypt.InductiveFunction.snd [ProgramSpec] {t : Type u_1} {A B : Type (max 1 u_2)} (ind : InductiveFunction t) [Reducible ind] [IsModule A] [IsModule B] (a : Module.Prod A B) : ind.eval (Module.snd a) ≤ ind.eval a

@[simp]

theorem GaudisCrypt.InductiveFunction.unit_moduleExpression [ProgramSpec] {t : Sort u_1} (ind : InductiveFunction t) : ind.evalMexpr ModuleExpression.unit = ind.nothing

@[simp]

theorem GaudisCrypt.InductiveFunction.unit [ProgramSpec] {t : Sort u_1} (ind : InductiveFunction t) (m : Module ModuleTypeRep.unit) : ind.eval m = ind.nothing

structure GaudisCrypt.InductiveFunctionGettersSetters (T : Type → Type) : Type 1

• nothing {t : Type} : T t
• join {t : Type} : T t → T t → T t
• getter {a s : Type} : Getter a s → T s
• setter {a s : Type} : Setter a s → T s
• reduce {a b : Type} (lens : Lens a b) (x : T b) : T a
• extend {a b : Type} (lens : Lens a b) (x : T a) : T b

def GaudisCrypt.InductiveFunctionGettersSetters.transfer [ProgramSpec] {T : Type → Type} {s t : Type} (ind : InductiveFunctionGettersSetters T) (x : T (ProcedureState s)) : T (ProcedureState t)

Equations

• ind.transfer x = ind.extend GaudisCrypt.ProcedureState.globalL (ind.reduce GaudisCrypt.ProcedureState.globalL x)

def GaudisCrypt.InductiveFunctionGettersSetters.stmt [ProgramSpec] {T : Type → Type} (ind : InductiveFunctionGettersSetters T) {s : Type} {holes : HoleSigs} : StmtWithHoles holes s → T (ProcedureState s)

Equations

• ind.stmt GaudisCrypt.StmtWithHoles.skip = ind.nothing
• ind.stmt (GaudisCrypt.StmtWithHoles.sample x_1 e) = ind.join (ind.setter x_1) (ind.getter e)
• ind.stmt (GaudisCrypt.StmtWithHoles.call' x_1 locals b r p) = ind.join (ind.setter x_1) (ind.join (ind.transfer (ind.stmt b)) (ind.join (ind.transfer (ind.getter r)) (ind.getter p)))
• ind.stmt (GaudisCrypt.StmtWithHoles.hole n x_1 p) = ind.join (ind.setter x_1) (ind.getter p)
• ind.stmt (s1.seq s2) = ind.join (ind.stmt s1) (ind.stmt s2)
• ind.stmt (GaudisCrypt.StmtWithHoles.ifThenElse c t e) = ind.join (ind.getter c) (ind.join (ind.stmt t) (ind.stmt e))
• ind.stmt (GaudisCrypt.StmtWithHoles.while c t) = ind.join (ind.getter c) (ind.stmt t)

def GaudisCrypt.InductiveFunctionGettersSetters.proc [ProgramSpec] {T : Type → Type} (ind : InductiveFunctionGettersSetters T) {sig : ProcedureSignature} {holes : HoleSigs} (proc : ProcedureWithHoles holes sig) : T State

Equations

• ind.proc proc = ind.join (ind.reduce GaudisCrypt.ProcedureState.globalL (ind.stmt proc.body)) (ind.reduce GaudisCrypt.ProcedureState.globalL (ind.getter proc.return_val))

class GaudisCrypt.ReducibleGettersSetters {T : Type → Type} (ind : InductiveFunctionGettersSetters T) : Type 1

• preorder {t : Type} : Preorder (T t)
• comm {t : Type} : Std.Commutative ind.join
• assoc {t : Type} : Std.Associative ind.join
• reduce_join {a b : Type} {r₁ r₂ : T b} (lens : Lens a b) : ind.reduce lens (ind.join r₁ r₂) ≤ ind.join (ind.reduce lens r₁) (ind.reduce lens r₂)
• extend_join {a b : Type} {r₁ r₂ : T a} (lens : Lens a b) : ind.join (ind.extend lens r₁) (ind.extend lens r₂) ≤ ind.extend lens (ind.join r₁ r₂)
• extend_reduce {a b : Type} (lens : Lens a b) (r : T a) : ind.reduce lens (ind.extend lens r) ≤ r
• reduce_mono {a b : Type} {r₁ r₂ : T b} (lens : Lens a b) : r₁ ≤ r₂ → ind.reduce lens r₁ ≤ ind.reduce lens r₂

  Monotonicity of reduce. Under only a Preorder this is not derivable from reduce_join (the old derivation used antisymmetry to turn r₁ ≤ r₂ into join r₁ r₂ = r₂).

• extend_mono {a b : Type} {r₁ r₂ : T a} (lens : Lens a b) : r₁ ≤ r₂ → ind.extend lens r₁ ≤ ind.extend lens r₂

  Monotonicity of extend; see reduce_mono.

• join_mono_left {t : Type} {a a' b : T t} : a' ≤ a → ind.join a' b ≤ ind.join a b
• le_join_left {t : Type} (a b : T t) : a ≤ ind.join a b
• join_idem {t : Type} (x : T t) : ind.join x x ≤ x
• nothing_le {t : Type} (x : T t) : ind.nothing ≤ x

Abstract join helpers (replacements for the lattice lemmas le_sup_*, sup_le, …).

def GaudisCrypt.InductiveFunctionGettersSetters.inductiveFunction [ProgramSpec] {T : Type → Type} (ind : InductiveFunctionGettersSetters T) : InductiveFunction (T State)

Equations

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

def GaudisCrypt.InductiveFunctionGettersSetters.evalMexpr [ProgramSpec] {T : Type → Type} (ind : InductiveFunctionGettersSetters T) : ModuleExpression → T State

Equations

• ind.evalMexpr = ind.inductiveFunction.evalMexpr

def GaudisCrypt.InductiveFunctionGettersSetters.eval' [ProgramSpec] {T : Type → Type} {t : ModuleTypeRep} (ind : InductiveFunctionGettersSetters T) : Module t → T State

Equations

• ind.eval' = ind.inductiveFunction.eval'

def GaudisCrypt.InductiveFunctionGettersSetters.eval [ProgramSpec] {T : Type → Type} {M : Type 1} (ind : InductiveFunctionGettersSetters T) [IsModule M] : M → T State

Equations

• ind.eval = ind.inductiveFunction.eval

@[implicit_reducible]

instance GaudisCrypt.instReducibleStateInductiveFunctionOfReducibleGettersSetters [ProgramSpec] {T : Type → Type} {ind : InductiveFunctionGettersSetters T} [red : ReducibleGettersSetters ind] : Reducible ind.inductiveFunction

Equations

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