structure GaudisCrypt.ProcedureSignature : Type 1

• params : List Type
• ret : Type

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

Equations

• sig.ParamType = GaudisCrypt.typeListToTuple sig.params

inductive GaudisCrypt.HoleSigs : Type 1

A sequence of procedure signatures, describing the holes of a program.

A cons list, head first: .cons X (.cons Y .empty) is the context of a body that calls X and then Y. Everything indexed by it agrees on that order — HoleIndex.zero is the head, HoleSigs.Instantiation is the tuple with the head's procedure first, toList, toModuleTypeRepTuple and toModuleExpr all put the head first, and the uses (…) display lists it first. So "hole 0" means one thing throughout: the first hole the body declares.

• empty : HoleSigs
• cons : ProcedureSignature → HoleSigs → HoleSigs

def GaudisCrypt.HoleSigs.length : HoleSigs → ℕ

Equations

• GaudisCrypt.HoleSigs.empty.length = 0
• (GaudisCrypt.HoleSigs.cons a h).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 = []
• (GaudisCrypt.HoleSigs.cons a h).toList = a :: h.toList

inductive GaudisCrypt.HoleIndex : HoleSigs → ProcedureSignature → Type 1

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

@[implicit_reducible]

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

Equations

• GaudisCrypt.instDecidableEqHoleIndex = GaudisCrypt.instDecidableEqHoleIndex.decEq

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 ⋯

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 {holes : HoleSigs} {sig : ProcedureSignature} (i1 i2 : HoleIndex holes sig) : i1.toFin = i2.toFin → i1 = i2

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev GaudisCrypt.Var (a : Type u_1) : Type (max u_1 1)

Equations

• GaudisCrypt.Var a = GaudisCrypt.Lens a GaudisCrypt.VariableAssignment

@[reducible, inline]

abbrev GaudisCrypt.Expr (a : Type u_1) : Type (max u_1 1)

Equations

• GaudisCrypt.Expr a = GaudisCrypt.Getter a GaudisCrypt.VariableAssignment

inductive GaudisCrypt.StmtWithHoles : HoleSigs → Type 1

Syntactic program (with arbitrary Lean terms as expressions). Every statement runs on a ProgramState: the globals, and the locals of the running procedure (its parameters among them).

• skip {h : HoleSigs} : StmtWithHoles h
• sample {h : HoleSigs} {a : Type} : Setter a ProgramState → Getter (SubProbability a) ProgramState → StmtWithHoles h
• call' {h : HoleSigs} {sig : ProcedureSignature} : Setter sig.ret ProgramState → (parameterNames : List String) → parameterNames.length = sig.params.length → parameterNames.Nodup → StmtWithHoles HoleSigs.empty → Getter sig.ret ProgramState → Getter sig.ParamType ProgramState → StmtWithHoles h
• hole {h : HoleSigs} {sig : ProcedureSignature} (n : HoleIndex h sig) : Setter sig.ret ProgramState → Getter sig.ParamType ProgramState → StmtWithHoles h
• seq {h : HoleSigs} : StmtWithHoles h → StmtWithHoles h → StmtWithHoles h
• ifThenElse {h : HoleSigs} : Getter Bool ProgramState → StmtWithHoles h → StmtWithHoles h → StmtWithHoles h
• while {h : HoleSigs} : Getter Bool ProgramState → StmtWithHoles h → StmtWithHoles h

def GaudisCrypt.Stmt : Type 1

Equations

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

structure GaudisCrypt.ProcedureWithHoles (holeSigs : HoleSigs) (sig : ProcedureSignature) : Type 1

A procedure: its body and return value run on a ProgramState, and on a call the arguments are written into the local slots named parameterNames (with the types sig.params), see ProcedureWithHoles.initLocals.

• parameterNames : List String
• parameterNames_length : self.parameterNames.length = sig.params.length
• parameterNames_nodup : self.parameterNames.Nodup
• body : StmtWithHoles holeSigs
• return_val : Getter sig.ret ProgramState

def GaudisCrypt.Procedure (sig : ProcedureSignature) : Type 1

Equations

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

@[reducible, inline]

abbrev GaudisCrypt.ProcedureWithHoles.signature {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

noncomputable def GaudisCrypt.ProcedureWithHoles.initLocals {holes : HoleSigs} {sig : ProcedureSignature} (p : ProcedureWithHoles holes sig) (args : sig.ParamType) : VariableAssignment

The locals a call of p with arguments args starts with: the arguments in the parameter slots, everything else at VariableAssignment.init.

Equations

• p.initLocals args = GaudisCrypt.VariableAssignment.setParams p.parameterNames sig.params ⋯ args GaudisCrypt.VariableAssignment.init

@[match_pattern]

def GaudisCrypt.StmtWithHoles.call {h : HoleSigs} {sig : ProcedureSignature} (x : Setter sig.ret ProgramState) (proc : Procedure sig) (params : Getter sig.ParamType ProgramState) : StmtWithHoles h

Equations

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

noncomputable def GaudisCrypt.StmtWithHoles.assign {a : Type} {h : HoleSigs} (x : Setter a ProgramState) (e : Getter a ProgramState) : StmtWithHoles h

Equations

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

noncomputable def GaudisCrypt.resetSetter (S : Set String) : Setter Unit ProgramState

The setter that puts the local variables with a name in S (of every type) back to VariableAssignment.init, the value every local has when a procedure starts, and leaves every other one alone; the value written, (), is ignored. The values put back form a VariableAssignment, which lives in Type 1, so they cannot themselves be the value of an assign; assign (resetSetter S) ⟨fun _ => ()⟩ is the reset, reset_vars S; in the surface syntax. Flattening (Logic/Inline.lean) emits it for the frame of the callee it inlines.

Equations

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

def GaudisCrypt.Stmt.call {sig : ProcedureSignature} (x : Setter sig.ret ProgramState) (proc : Procedure sig) (params : Getter sig.ParamType ProgramState) : Stmt

Equations

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

def GaudisCrypt.HoleSigs.Instantiation : HoleSigs → Type 1

The procedures filling the holes holes, as a tuple: right-nested, with HoleIndex.zero — the last-appended hole — as the first component, the same order as HoleSigs.Instantiation.toList and HoleSigs.Instantiation.toModuleExpr. No holes at all is PUnit, so what one writes is

p.instantiate (c₁, c₂, c₃)   -- three holes, in the order the body declares them
p.instantiate c              -- one hole: the tuple is its element

and nothing else is needed to build one: Prod.mk is the only constructor involved. Reading a hole out is HoleSigs.Instantiation.lookup.

A one-hole instantiation is the procedure itself rather than a pair with PUnit, which is what keeps the written form free of a trailing ⟨⟩. The cost is that knowing Instantiation (cons sig holes) is a pair takes two constructors, not one — so every function that recurses on holes and takes an instantiation apart splits on both levels, cons _ .empty beside cons _ (.cons ..). Do that split in the function itself; routing it through head/tail helpers instead makes them stuck at a variable holes, and then nothing about them is rfl any more.

It is a tuple rather than the function ∀ {sig}, HoleIndex holes sig → Procedure sig it used to be so that instantiations can be written and read as ordinary Lean tuples — the function form made every instantiation an implicit-lambda chain, in the source and in every goal that mentioned one. The price is that holes has to be concrete for the type to reduce: an instantiation at a symbolic holes can still be taken as a hypothesis and looked up (lookup recurses on the index, which refines holes), but not built or taken apart without recursing on holes in step.

The universe is written out only because PUnit would otherwise take one of its own: nothing in the .empty branch constrains its level, so Type _ gives the definition a universe parameter that no argument determines, and a use site inside an inductive (ModuleExpression.ReductionStep) then has nothing to infer it from.

Equations

• GaudisCrypt.HoleSigs.empty.Instantiation = PUnit.{2}
• (GaudisCrypt.HoleSigs.cons sig GaudisCrypt.HoleSigs.empty).Instantiation = GaudisCrypt.Procedure sig
• (GaudisCrypt.HoleSigs.cons sig holes).Instantiation = (GaudisCrypt.Procedure sig × holes.Instantiation)

def GaudisCrypt.HoleSigs.Instantiation.lookup {holes : HoleSigs} {sig : ProcedureSignature} : holes.Instantiation → HoleIndex holes sig → Procedure sig

The procedure filling hole idx. Recursion is on the index, which refines holes as it goes — which is what lets this work at a holes that is still a variable.

Equations

• inst.lookup GaudisCrypt.HoleIndex.zero = inst
• inst.lookup GaudisCrypt.HoleIndex.zero = inst.1
• inst.lookup j.succ = inst.2.lookup j

@[simp]

theorem GaudisCrypt.HoleSigs.Instantiation.lookup_zero_single {sig : ProcedureSignature} (inst : (cons sig empty).Instantiation) : inst.lookup HoleIndex.zero = inst

The only hole of a one-hole instantiation is the instantiation itself.

@[simp]

theorem GaudisCrypt.HoleSigs.Instantiation.lookup_zero_cons {holes : HoleSigs} {sig sig' : ProcedureSignature} (inst : (cons sig (cons sig' holes)).Instantiation) : inst.lookup HoleIndex.zero = inst.1

The first hole of a tuple of two or more: its first component.

@[simp]

theorem GaudisCrypt.HoleSigs.Instantiation.lookup_succ {holes : HoleSigs} {sig sig' sig'' : ProcedureSignature} (inst : (cons sig (cons sig' holes)).Instantiation) (i : HoleIndex (cons sig' holes) sig'') : inst.lookup i.succ = inst.2.lookup i

Any later hole: the rest of the tuple.

def GaudisCrypt.HoleSigs.Instantiation.toList {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 the tuple itself and as HoleSigs.Instantiation.toModuleExpr.

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

Equations

• x_2.toList = []
• inst.toList = [⟨sig, inst⟩]
• inst.toList = ⟨sig, inst.1⟩ :: inst.2.toList

def GaudisCrypt.StmtWithHoles.instantiate {holes : HoleSigs} (stmt : StmtWithHoles holes) (instantiation : holes.Instantiation) : Stmt

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

• GaudisCrypt.StmtWithHoles.skip.instantiate instantiation = GaudisCrypt.StmtWithHoles.skip
• (GaudisCrypt.StmtWithHoles.sample x e).instantiate instantiation = GaudisCrypt.StmtWithHoles.sample x e
• (GaudisCrypt.StmtWithHoles.call' x ns hl hn b r p).instantiate instantiation = GaudisCrypt.StmtWithHoles.call' x ns hl hn b r p
• (GaudisCrypt.StmtWithHoles.hole n x p).instantiate instantiation = GaudisCrypt.StmtWithHoles.call x (instantiation.lookup n) p
• (s1.seq s2).instantiate instantiation = GaudisCrypt.StmtWithHoles.seq (s1.instantiate instantiation) (s2.instantiate instantiation)
• (GaudisCrypt.StmtWithHoles.ifThenElse c t e).instantiate instantiation = GaudisCrypt.StmtWithHoles.ifThenElse c (t.instantiate instantiation) (e.instantiate instantiation)
• (GaudisCrypt.StmtWithHoles.while c t).instantiate instantiation = GaudisCrypt.StmtWithHoles.while c (t.instantiate instantiation)

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

Equations

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

def GaudisCrypt.StmtWithHoles.depth {h : HoleSigs} : StmtWithHoles h → ℕ

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 parameterNames a_1 a_2 body a_3 a_4).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 (inst : HoleSigs.empty.Instantiation) (s : Stmt) : instantiate s 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 {sig : ProcedureSignature} (p : ProcedureWithHoles HoleSigs.empty sig) (inst : HoleSigs.empty.Instantiation) : p.instantiate inst = p

Instantiating a procedure that has no holes leaves it alone.

@[irreducible]

noncomputable def GaudisCrypt.programDenotation : Stmt → ProgramDenotation ProgramState 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)

noncomputable def GaudisCrypt.procedureDenotation {sig : ProcedureSignature} (proc : Procedure sig) (args : sig.ParamType) : ProgramDenotation VariableAssignment sig.ret

Run proc on fresh locals (ProcedureWithHoles.initLocals); the callee's locals are discarded at the end, only the globals are kept. The state and the result live in different universes, hence hbind in place of do.

Not mutual with programDenotation, whose call' case repeats this body.

Equations

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

theorem GaudisCrypt.programDenotation_call' {sig : ProcedureSignature} (x : Setter sig.ret ProgramState) (names : List String) (hlen : names.length = sig.params.length) (hnodup : names.Nodup) (body : Stmt) (ret : Getter sig.ret ProgramState) (args : Getter sig.ParamType ProgramState) : programDenotation (StmtWithHoles.call' x names hlen hnodup body ret args) = do let argValues ← ProgramDenotation.get args let retVal ← ProgramDenotation.zoom ProgramState.globalL (procedureDenotation { parameterNames := names, parameterNames_length := hlen, parameterNames_nodup := hnodup, body := body, return_val := ret } argValues) ProgramDenotation.set x retVal

The call' case of programDenotation, with the callee run folded into procedureDenotation.

noncomputable def GaudisCrypt.procWrap {sig : ProcedureSignature} (rv : Getter sig.ret ProgramState) (initL : VariableAssignment) (B : ProgramDenotation ProgramState Unit) : ProgramDenotation VariableAssignment sig.ret

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

Equations

• GaudisCrypt.procWrap rv initL B st = (B { globals := st, locals := initL }).hbind fun (p : Unit × GaudisCrypt.ProgramState) => pure (rv.get p.2, p.2.globals)

theorem GaudisCrypt.procedureDenotation_eq_procWrap_gen {holes : HoleSigs} {sig : ProcedureSignature} (A : ProcedureWithHoles holes sig) (args : sig.ParamType) (inst : holes.Instantiation) : procedureDenotation (A.instantiate inst) args = procWrap A.return_val (A.initLocals args) (programDenotation (A.body.instantiate inst))

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