class GaudisCrypt.ProgramSpec : Type (u + 1)

• state : Type u

def GaudisCrypt.State [spec : ProgramSpec] : Type u_1

Equations

• GaudisCrypt.State = GaudisCrypt.ProgramSpec.state

structure GaudisCrypt.ProcedureState [ProgramSpec] (l : Type) : Type u_1

The state a statement runs in: the global program state together with the local state l (procedure parameters + local variables). Replaces the former State × l product so that the two halves are named.

• global : State
• locals : l

def GaudisCrypt.ProcedureState.globalL [ProgramSpec] {l : Type} : Lens State (ProcedureState l)

Lens onto the global part of a ProcedureState.

Equations

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

def GaudisCrypt.ProcedureState.localL [ProgramSpec] {l : Type} : Lens l (ProcedureState l)

Lens onto the local part of a ProcedureState.

Equations

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

def GaudisCrypt.VariableName : Type

Equations

• GaudisCrypt.VariableName = String

structure GaudisCrypt.ProcedureSignature : Type 1

• params : List Type
• ret : Type

class GaudisCrypt.LocalState : Type 1

• params : List Type
• locals : List Type

def GaudisCrypt.paramListToTuple : List Type → Type

Equations

• GaudisCrypt.paramListToTuple [] = Unit
• GaudisCrypt.paramListToTuple [x_1] = x_1
• GaudisCrypt.paramListToTuple (x_1 :: xs) = (x_1 × GaudisCrypt.paramListToTuple xs)

structure GaudisCrypt.LocalVariableState (paramTypes : List Type) (locals : List ((t : Type) × Inhabited t)) : Type

The local state of a procedure: parameter values (params) and local-variable values (vars). Indexed by the parameter types and the local declarations only (not the return type), so it can be formed before the return type is known — this is what lets a proc with an omitted return type elaborate.

• params : paramListToTuple paramTypes
• vars : paramListToTuple (List.map (fun (x : (t : Type) × Inhabited t) => x.fst) locals)

@[reducible]

def GaudisCrypt.ProcedureSignature.LocalVariableState (sig : ProcedureSignature) (locals : List ((t : Type) × Inhabited t)) : Type

The local state for a full signature (delegates to LocalVariableState; reducible so sig.LocalVariableState locals is defeq to LocalVariableState sig.params locals).

Equations

• sig.LocalVariableState locals = GaudisCrypt.LocalVariableState sig.params locals

def GaudisCrypt.LocalVariableState.paramsL {paramTypes : List Type} {locals : List ((t : Type) × Inhabited t)} : Lens (paramListToTuple paramTypes) (LocalVariableState paramTypes locals)

Lens onto the parameter tuple of a LocalVariableState.

Equations

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

def GaudisCrypt.LocalVariableState.varsL {paramTypes : List Type} {locals : List ((t : Type) × Inhabited t)} : Lens (paramListToTuple (List.map (fun (x : (t : Type) × Inhabited t) => x.fst) locals)) (LocalVariableState paramTypes locals)

Lens onto the local-variable tuple of a LocalVariableState.

Equations

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

def GaudisCrypt.Lens.intoParams [ProgramSpec] {a : Type} {paramTypes : List Type} {locals : List ((t : Type) × Inhabited t)} (lens : Lens a (paramListToTuple paramTypes)) : Lens a (ProcedureState (LocalVariableState paramTypes locals))

Lift a lens into the parameter tuple to a lens into the full procedure state (localL ∘ paramsL). Analogous to Lens.ofst. (Defined in the Lens namespace via _root_ so dot notation lens.intoParams resolves.)

Equations

• lens.intoParams = GaudisCrypt.ProcedureState.localL.chain (GaudisCrypt.LocalVariableState.paramsL.chain lens)

def GaudisCrypt.Lens.intoVars [ProgramSpec] {a : Type} {paramTypes : List Type} {locals : List ((t : Type) × Inhabited t)} (lens : Lens a (paramListToTuple (List.map (fun (x : (t : Type) × Inhabited t) => x.fst) locals))) : Lens a (ProcedureState (LocalVariableState paramTypes locals))

Lift a lens into the local-variable tuple to a lens into the full procedure state (localL ∘ varsL). Analogous to Lens.ofst.

Equations

• lens.intoVars = GaudisCrypt.ProcedureState.localL.chain (GaudisCrypt.LocalVariableState.varsL.chain lens)

instance GaudisCrypt.Programs.disjoint_intoVars [ProgramSpec] {a b : Type} {paramTypes : List Type} {locals : List ((t : Type) × Inhabited t)} {x : Lens a (paramListToTuple (List.map (fun (x : (t : Type) × Inhabited t) => x.fst) locals))} {y : Lens b (paramListToTuple (List.map (fun (x : (t : Type) × Inhabited t) => x.fst) locals))} [disjoint x y] : disjoint x.intoVars y.intoVars

Local program variables are Lens.intoVars of their slot projections; distinct slots are disjoint, and intoVars (two chain layers) preserves that.

def GaudisCrypt.ProcedureSignature.ParamType (sig : ProcedureSignature) : Type

Equations

• sig.ParamType = GaudisCrypt.paramListToTuple sig.params

def GaudisCrypt.ProcedureSignature.localVariableInit (sig : ProcedureSignature) (locals : List ((t : Type) × Inhabited t)) (params : paramListToTuple sig.params) : sig.LocalVariableState locals

Equations

• sig.localVariableInit locals params = { params := params, vars := GaudisCrypt.localDefaults✝ locals }

inductive GaudisCrypt.HoleSigs : Type 1

A sequences of procedure signatures, intended to be used to describe the type of holes in a program

• empty : HoleSigs
• append : HoleSigs → ProcedureSignature → HoleSigs

def GaudisCrypt.HoleSigs.length : HoleSigs → ℕ

Equations

• GaudisCrypt.HoleSigs.empty.length = 0
• (h.append a).length = h.length.succ

def GaudisCrypt.HoleSigs.NonEmpty : HoleSigs → Prop

Equations

• GaudisCrypt.HoleSigs.empty.NonEmpty = False
• x✝.NonEmpty = True

def GaudisCrypt.HoleSigs.toList : HoleSigs → List ProcedureSignature

Equations

• GaudisCrypt.HoleSigs.empty.toList = []
• (h.append a).toList = h.toList ++ [a]

inductive GaudisCrypt.HoleIndex : HoleSigs → ProcedureSignature → Type 1

• zero {a : ProcedureSignature} {Γ : HoleSigs} : HoleIndex (Γ.append a) a
• succ {Γ : HoleSigs} {a b : ProcedureSignature} : HoleIndex Γ a → HoleIndex (Γ.append b) a

def GaudisCrypt.instDecidableEqHoleIndex.decEq {a✝ : HoleSigs} {a✝¹ : ProcedureSignature} (x✝ x✝¹ : HoleIndex a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

• GaudisCrypt.instDecidableEqHoleIndex.decEq GaudisCrypt.HoleIndex.zero GaudisCrypt.HoleIndex.zero = isTrue ⋯
• GaudisCrypt.instDecidableEqHoleIndex.decEq GaudisCrypt.HoleIndex.zero a_3.succ = isFalse ⋯
• GaudisCrypt.instDecidableEqHoleIndex.decEq a_3.succ GaudisCrypt.HoleIndex.zero = isFalse ⋯
• GaudisCrypt.instDecidableEqHoleIndex.decEq a_5.succ b.succ = if h : a_5 = b then h ▸ have inst := GaudisCrypt.instDecidableEqHoleIndex.decEq a_5 a_5; isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance GaudisCrypt.instDecidableEqHoleIndex {a✝ : HoleSigs} {a✝¹ : ProcedureSignature} : DecidableEq (HoleIndex a✝ a✝¹)

Equations

• GaudisCrypt.instDecidableEqHoleIndex = GaudisCrypt.instDecidableEqHoleIndex.decEq

def GaudisCrypt.HoleIndex.toFin {holes : HoleSigs} {sig : ProcedureSignature} : HoleIndex holes sig → Fin holes.length

Equations

• GaudisCrypt.HoleIndex.zero.toFin = ⟨0, ⋯⟩
• i.succ.toFin = ⟨(↑i.toFin).succ, ⋯⟩

theorem GaudisCrypt.HoleIndex.toFin_inj [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (i1 i2 : HoleIndex holes sig) : i1.toFin = i2.toFin → i1 = i2

@[implicit_reducible]

noncomputable instance GaudisCrypt.instFintypeHoleIndex [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} : Fintype (HoleIndex holes sig)

Equations

• GaudisCrypt.instFintypeHoleIndex = Fintype.ofInjective GaudisCrypt.HoleIndex.toFin ⋯

@[reducible, inline]

abbrev GaudisCrypt.Var [ProgramSpec] (a : Type u_2) : Type (max u_2 u_1)

Equations

• GaudisCrypt.Var a = GaudisCrypt.Lens a GaudisCrypt.State

@[reducible, inline]

abbrev GaudisCrypt.Expr [ProgramSpec] (a : Type u_2) : Type (max u_2 u_1)

Equations

• GaudisCrypt.Expr a = GaudisCrypt.Getter a GaudisCrypt.State

inductive GaudisCrypt.StmtWithHoles [ProgramSpec] : HoleSigs → Type → Type (max 1 u_1)

Syntactic program (with arbitrary Lean terms as expressions)

• skip [ProgramSpec] {h : HoleSigs} {l : Type} : StmtWithHoles h l
• sample [ProgramSpec] {l : Type} {h : HoleSigs} {a : Type} : Setter a (ProcedureState l) → Getter (SubProbability a) (ProcedureState l) → StmtWithHoles h l
• call' [ProgramSpec] {l : Type} {h : HoleSigs} {sig : ProcedureSignature} : Setter sig.ret (ProcedureState l) → (locals : List ((t : Type) × Inhabited t)) → StmtWithHoles HoleSigs.empty (sig.LocalVariableState locals) → Getter sig.ret (ProcedureState (sig.LocalVariableState locals)) → Getter sig.ParamType (ProcedureState l) → StmtWithHoles h l
• hole [ProgramSpec] {h : HoleSigs} {l : Type} {sig : ProcedureSignature} (n : HoleIndex h sig) : Setter sig.ret (ProcedureState l) → Getter sig.ParamType (ProcedureState l) → StmtWithHoles h l
• seq [ProgramSpec] {h : HoleSigs} {l : Type} : StmtWithHoles h l → StmtWithHoles h l → StmtWithHoles h l
• ifThenElse [ProgramSpec] {l : Type} {h : HoleSigs} : Getter Bool (ProcedureState l) → StmtWithHoles h l → StmtWithHoles h l → StmtWithHoles h l
• while [ProgramSpec] {l : Type} {h : HoleSigs} : Getter Bool (ProcedureState l) → StmtWithHoles h l → StmtWithHoles h l

def GaudisCrypt.Stmt [ProgramSpec] : Type → Type (max 1 u_1)

Equations

• GaudisCrypt.Stmt = GaudisCrypt.StmtWithHoles GaudisCrypt.HoleSigs.empty

structure GaudisCrypt.ProcedureWithHoles [ProgramSpec] (holeSigs : HoleSigs) (sig : ProcedureSignature) : Type (max 1 u_1)

• locals : List ((t : Type) × Inhabited t)
• body : StmtWithHoles holeSigs (sig.LocalVariableState self.locals)
• return_val : Getter sig.ret (ProcedureState (sig.LocalVariableState self.locals))

def GaudisCrypt.Procedure [ProgramSpec] (sig : ProcedureSignature) : Type (max 1 u_1)

Equations

• GaudisCrypt.Procedure sig = GaudisCrypt.ProcedureWithHoles GaudisCrypt.HoleSigs.empty sig

@[reducible, inline]

abbrev GaudisCrypt.ProcedureWithHoles.signature [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (_p : ProcedureWithHoles holes sig) : ProcedureSignature

The signature of a procedure-with-holes as a term — sig is otherwise only reachable as an implicit argument of the type, which makes it awkward to name in generated code.

Equations

• _p.signature = sig

@[match_pattern]

def GaudisCrypt.StmtWithHoles.call {l : Type} {h : HoleSigs} [ProgramSpec] {sig : ProcedureSignature} (x : Setter sig.ret (ProcedureState l)) (proc : Procedure sig) (params : Getter sig.ParamType (ProcedureState l)) : StmtWithHoles h l

Equations

• GaudisCrypt.StmtWithHoles.call x proc params = GaudisCrypt.StmtWithHoles.call' x proc.locals proc.body proc.return_val params

noncomputable def GaudisCrypt.StmtWithHoles.assign {a l : Type} {h : HoleSigs} [ProgramSpec] (x : Setter a (ProcedureState l)) (e : Getter a (ProcedureState l)) : StmtWithHoles h l

Equations

• GaudisCrypt.StmtWithHoles.assign x e = GaudisCrypt.StmtWithHoles.sample x { get := fun (st : GaudisCrypt.ProcedureState l) => pure (e.get st) }

def GaudisCrypt.Stmt.call {l : Type} [ProgramSpec] {sig : ProcedureSignature} (x : Setter sig.ret (ProcedureState l)) (proc : Procedure sig) (params : Getter sig.ParamType (ProcedureState l)) : Stmt l

Equations

• GaudisCrypt.Stmt.call x proc params = GaudisCrypt.StmtWithHoles.call x proc params

def GaudisCrypt.HoleSigs.Instantiation [ProgramSpec] (holes : HoleSigs) : Type (max 1 u_1)

Equations

• holes.Instantiation = ({sig : GaudisCrypt.ProcedureSignature} → GaudisCrypt.HoleIndex holes sig → GaudisCrypt.Procedure sig)

def GaudisCrypt.HoleSigs.Instantiation.nil [ProgramSpec] : empty.Instantiation

The only instantiation of no holes at all.

def GaudisCrypt.HoleSigs.Instantiation.push [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (inst : holes.Instantiation) (p : Procedure sig) : (holes.append sig).Instantiation

Extend an instantiation by one more procedure, for one more (last-appended) hole. Written in the order the holes were appended, nil.push p₀ |>.push p₁ …, this is how an instantiation is built up from concrete procedures — note HoleIndex.zero is the last one pushed.

Equations

• inst.push p GaudisCrypt.HoleIndex.zero = p
• inst.push p i.succ = inst i

@[simp]

theorem GaudisCrypt.HoleSigs.Instantiation.push_zero [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (inst : holes.Instantiation) (p : Procedure sig) : push (fun {sig : ProcedureSignature} => inst) p HoleIndex.zero = p

Looking up the hole a push was made for.

@[simp]

theorem GaudisCrypt.HoleSigs.Instantiation.push_succ [ProgramSpec] {holes : HoleSigs} {sig sig' : ProcedureSignature} (inst : holes.Instantiation) (p : Procedure sig) (i : HoleIndex holes sig') : push (fun {sig : ProcedureSignature} => inst) p i.succ = inst i

Looking up any other hole of a push falls through to the instantiation it extends.

def GaudisCrypt.HoleSigs.Instantiation.toList [ProgramSpec] {holes : HoleSigs} : holes.Instantiation → List ((sig : ProcedureSignature) × Procedure sig)

Convert an instantiation into a plain list of procedures (tagged by their signature), in the same right-nested order as HoleSigs.Instantiation.toModuleTuple.

The head of the list corresponds to the most-recently appended hole signature.

Equations

• One or more equations did not get rendered due to their size.
• x_2.toList = []

def GaudisCrypt.StmtWithHoles.instantiate [ProgramSpec] {holes : HoleSigs} {l : Type} (stmt : StmtWithHoles holes l) (instantiation : holes.Instantiation) : Stmt l

Instantiate all holes in a statement using resolve, turning each .hole into a .call' of the resolved procedure. Hole-free constructors are simply re-typed.

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.StmtWithHoles.skip.instantiate instantiation = GaudisCrypt.StmtWithHoles.skip
• (GaudisCrypt.StmtWithHoles.sample x e).instantiate instantiation = GaudisCrypt.StmtWithHoles.sample x e
• (GaudisCrypt.StmtWithHoles.call' x ls b r p).instantiate instantiation = GaudisCrypt.StmtWithHoles.call' x ls b r p
• (GaudisCrypt.StmtWithHoles.hole n x p).instantiate instantiation = GaudisCrypt.StmtWithHoles.call x (instantiation n) p
• (GaudisCrypt.StmtWithHoles.while c t).instantiate instantiation = GaudisCrypt.StmtWithHoles.while c (t.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => instantiation)

def GaudisCrypt.ProcedureWithHoles.instantiate [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (proc : ProcedureWithHoles holes sig) (instantiation : holes.Instantiation) : Procedure sig

Equations

• proc.instantiate instantiation = { locals := proc.locals, body := proc.body.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => instantiation, return_val := proc.return_val }

def GaudisCrypt.StmtWithHoles.depth [ProgramSpec] {h : HoleSigs} {l : Type} : StmtWithHoles h l → ℕ

A structural size measure used to justify termination of programDenotation. The auto-generated sizeOf for StmtWithHoles is trivially 0 (the inductive lives in a higher universe because its constructors quantify over a : Type), so we define our own.

Equations

• GaudisCrypt.StmtWithHoles.skip.depth = 0
• (GaudisCrypt.StmtWithHoles.sample a_1 a_2).depth = 0
• (GaudisCrypt.StmtWithHoles.hole n a a_1).depth = 0
• (GaudisCrypt.StmtWithHoles.call' a locals body a_1 a_2).depth = body.depth + 1
• (p.seq q).depth = max p.depth q.depth + 1
• (GaudisCrypt.StmtWithHoles.ifThenElse a p q).depth = max p.depth q.depth + 1
• (GaudisCrypt.StmtWithHoles.while a p).depth = p.depth + 1

theorem GaudisCrypt.StmtWithHoles.instantiate_empty [ProgramSpec] {l : Type} (inst : HoleSigs.empty.Instantiation) (s : Stmt l) : (instantiate s fun {sig : ProcedureSignature} => inst) = s

A hole-free statement has nothing to instantiate: every constructor is re-typed as itself, and the .hole case cannot occur (HoleIndex .empty _ is empty). Recursion is on depth — the statement's own index HoleSigs.empty is not a variable, so the equation compiler cannot recurse on it structurally.

@[simp]

theorem GaudisCrypt.ProcedureWithHoles.instantiate_empty [ProgramSpec] {sig : ProcedureSignature} (p : ProcedureWithHoles HoleSigs.empty sig) (inst : HoleSigs.empty.Instantiation) : (p.instantiate fun {sig : ProcedureSignature} => inst) = p

Instantiating a procedure that has no holes leaves it alone.

@[irreducible]

noncomputable def GaudisCrypt.programDenotation [ProgramSpec] {l : Type} : Stmt l → ProgramDenotation (ProcedureState l) Unit

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.programDenotation GaudisCrypt.StmtWithHoles.skip = GaudisCrypt.ProgramDenotation.skip
• GaudisCrypt.programDenotation (GaudisCrypt.StmtWithHoles.sample x_1 e) = do let μ ← GaudisCrypt.ProgramDenotation.get e let v ← μ.toProgramDenotation GaudisCrypt.ProgramDenotation.set x_1 v
• GaudisCrypt.programDenotation (p.seq q) = do let __discr ← GaudisCrypt.programDenotation p have x : Unit := __discr GaudisCrypt.programDenotation q
• GaudisCrypt.programDenotation (GaudisCrypt.StmtWithHoles.while c p) = GaudisCrypt.while_loop (GaudisCrypt.ProgramDenotation.get c) (GaudisCrypt.programDenotation p)

@[irreducible]

noncomputable def GaudisCrypt.procedureDenotation [ProgramSpec] {sig : ProcedureSignature} (proc : Procedure sig) (args : sig.ParamType) : ProgramDenotation State sig.ret

Equations

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

noncomputable def GaudisCrypt.procWrap [ProgramSpec] {sig : ProcedureSignature} {L : Type} (rv : Getter sig.ret (ProcedureState L)) (initL : L) (B : ProgramDenotation (ProcedureState L) Unit) : ProgramDenotation State sig.ret

The procedure denotation as an explicit wrapper: initialise locals, run the body, extract (return_val, global).

Equations

• GaudisCrypt.procWrap rv initL B st = do let p ← B { global := st, locals := initL } pure (rv.get p.2, p.2.global)

theorem GaudisCrypt.procedureDenotation_eq_procWrap_gen [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (A : ProcedureWithHoles holes sig) (args : sig.ParamType) (inst : holes.Instantiation) : procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => inst) args = procWrap A.return_val (sig.localVariableInit A.locals args) (programDenotation (A.body.instantiate fun {sig : ProcedureSignature} => inst))

procedureDenotation of an instantiated procedure is procWrap of its body (generic over the holes and their instantiation).