Flattening calls whose callee is spelled out

Flatten.flattenProcedureCalls rewrites every call of a statement whose callee is written out (a proc literal) into the callee's body, and proves the result denotationally equivalent to the input (StmtWithHoles.EquivInLens) along a lens that renames the locals. Flatten.flattenProcedure does the same to a procedure, with a proof that its procedureDenotation is unchanged. Flatten.unfoldProcedure and Flatten.inlineProcedure first evaluate a callee named through modules, so that it can be flattened.

One call is flattened by renaming the locals: the caller's keep their names (Flatten.trafo, renaming by Flatten.escape, the identity on every name not starting with @), the callee's frame moves to names the caller cannot have (Flatten.emb, renaming n to @.n by Flatten.tag), and the call becomes

reset_vars stringsStartingWith "@.";  -- the callee's frame back to its initial values
«@.z₁», …, «@.zₙ» <- (args);  -- the arguments, in the callee's parameter slots
‹callee body, renamed›
x <- ‹callee return value, renamed›;

The two renamings have disjoint images, which is what makes the callee's frame disjoint from the caller's without looking at either. Readable names come last, in a pass of their own (Flatten.renameNames): a permutation of names (Flatten.rename ren, «@.w» ↦ w0), which is sound for any choice of names.

What a reset puts back is given by a set of names, which every later round and the cleanup renaming map along with the rest. The cleaning keeps such a set in a normal form, {"z", "w0"} ∪ stringsStartingWith "@@." \ {"@@.z", "@@.w"} say (section Reset regions, and Flatten.cleanNameSet?, the only meta code that knows that form).

Names

In a flattening round the caller's names go through escape, the callee's through tag; the two have disjoint images (escape_ne_tag), and escape is the identity on every name that does not start with @. The readable names come from a separate permutation, swaps ren.

def GaudisCrypt.Flatten.escapeChars : List Char → List Char

escape on character lists: a leading @ is doubled.

Equations

• GaudisCrypt.Flatten.escapeChars [] = []
• GaudisCrypt.Flatten.escapeChars (c :: cs) = if c = '@' then '@' :: '@' :: cs else c :: cs

def GaudisCrypt.Flatten.escape (n : String) : String

The caller's names: @… ↦ @@…, every other name unchanged.

Equations

• GaudisCrypt.Flatten.escape n = String.ofList (GaudisCrypt.Flatten.escapeChars n.toList)

def GaudisCrypt.Flatten.tag (n : String) : String

The callee's names: n ↦ @.n.

Equations

• GaudisCrypt.Flatten.tag n = String.ofList ('@' :: '.' :: n.toList)

theorem GaudisCrypt.Flatten.escapeChars_injective : Function.Injective escapeChars

theorem GaudisCrypt.Flatten.escape_injective : Function.Injective escape

theorem GaudisCrypt.Flatten.tag_injective : Function.Injective tag

theorem GaudisCrypt.Flatten.escape_ne_tag (a b : String) : escape a ≠ tag b

No caller name is a callee name.

def GaudisCrypt.Flatten.swaps : List (String × String) → Equiv.Perm String

The cleanup renaming: for each (a, f), the names a and f swap places.

Equations

• GaudisCrypt.Flatten.swaps [] = 1
• GaudisCrypt.Flatten.swaps ((a, f) :: ren) = Equiv.swap a f * GaudisCrypt.Flatten.swaps ren

def GaudisCrypt.Flatten.renameName (ren : List (String × String)) (n : String) : String

The name n after the cleanup renaming ren.

Equations

• GaudisCrypt.Flatten.renameName ren n = (GaudisCrypt.Flatten.swaps ren) n

theorem GaudisCrypt.Flatten.renameName_injective (ren : List (String × String)) : Function.Injective (renameName ren)

Renaming the locals of a program state

theorem GaudisCrypt.VariableAssignment.embed_get_embed_set {ι₁ ι₂ : String → String} (h₁ : Function.Injective ι₁) (h₂ : Function.Injective ι₂) (hd : ∀ (a b : String), ι₁ a ≠ ι₂ b) (w m : VariableAssignment) : (embed ι₁ h₁).get ((embed ι₂ h₂).set w m) = (embed ι₁ h₁).get m

Writing through one embed is invisible through another whose image is disjoint.

Reset regions

The names a flattened call resets start out as all of the callee's (Set.univ, seen through emb), and every later round and the cleanup renaming map them along with the rest. The cleaning keeps such a set in the normal form nf p add rem, that is {add…} ∪ stringsStartingWith p \ {rem…}: the names that start with p, except those in rem, and those in add. The three name maps keep that form: tag and escape move the prefix (@., @@., …), and each swap of the cleanup renaming moves at most one name out of the set and one into it.

This section and cleanNameSet? (which computes the normal form, with these lemmas as proofs) are all there is to the form; another one replaces both.

def GaudisCrypt.stringsStartingWith (p : String) : Set String

The strings that start with p. (Lean has the predicate, String.IsPrefix, which unfolds to the same p.toList <+: n.toList, but not the set.)

Equations

• GaudisCrypt.stringsStartingWith p = {n : String | p.toList <+: n.toList}

def GaudisCrypt.Flatten.ofList (l : List String) : Set String

The names in l. Never printed: the cleaning writes it as a set literal (ofList_cons, ofList_singleton).

Equations

• GaudisCrypt.Flatten.ofList l = {n : String | n ∈ l}

theorem GaudisCrypt.Flatten.ofList_singleton (a : String) : ofList [a] = {a}

theorem GaudisCrypt.Flatten.ofList_cons (a b : String) (l : List String) : ofList (a :: b :: l) = insert a (ofList (b :: l))

def GaudisCrypt.Flatten.nf (p : String) (add rem : List String) : Set String

The normal form of a reset region: the names that start with p and are not in rem, and those in add. Never printed: the cleaning writes it out without its empty parts (nf_eq_pretty and the rest).

Equations

• GaudisCrypt.Flatten.nf p add rem = GaudisCrypt.Flatten.ofList add ∪ GaudisCrypt.stringsStartingWith p \ GaudisCrypt.Flatten.ofList rem

def GaudisCrypt.Flatten.memB (p : String) (add rem : List String) (n : String) : Bool

Membership in nf p add rem, as a computation.

Equations

• GaudisCrypt.Flatten.memB p add rem n = (add.contains n || p.toList.isPrefixOf n.toList && !rem.contains n)

theorem GaudisCrypt.Flatten.nf_eq_setOf (p : String) (add rem : List String) : nf p add rem = {n : String | n ∈ add ∨ p.toList <+: n.toList ∧ n ∉ rem}

theorem GaudisCrypt.Flatten.nf_eq_setOf_memB (p : String) (add rem : List String) : nf p add rem = {n : String | memB p add rem n = true}

nf p add rem written out, given the set literals A, R of add, rem.

theorem GaudisCrypt.Flatten.nf_nil_nil (p : String) : nf p [] [] = stringsStartingWith p

theorem GaudisCrypt.Flatten.nf_nil_eq (p : String) (add : List String) (A : Set String) (hA : ofList add = A) : nf p add [] = A ∪ stringsStartingWith p

theorem GaudisCrypt.Flatten.nf_nil_left_eq (p : String) (rem : List String) (R : Set String) (hR : ofList rem = R) : nf p [] rem = stringsStartingWith p \ R

theorem GaudisCrypt.Flatten.nf_eq_pretty (p : String) (add rem : List String) (A R : Set String) (hA : ofList add = A) (hR : ofList rem = R) : nf p add rem = A ∪ stringsStartingWith p \ R

theorem GaudisCrypt.Flatten.univ_eq_nf : Set.univ = nf "" [] []

theorem GaudisCrypt.Flatten.image_nf {ι : String → String} (hι : Function.Injective ι) {p p' : String} (h₁ : ∀ (n : String), p.toList <+: n.toList → p'.toList <+: (ι n).toList) (h₂ : ∀ (m : String), p'.toList <+: m.toList → ∃ (n : String), ι n = m ∧ p.toList <+: n.toList) (add rem : List String) : ι '' nf p add rem = nf p' (List.map ι add) (List.map ι rem)

The image of a normal form under an injective name map that maps the names with prefix p onto those with prefix p'.

theorem GaudisCrypt.Flatten.image_tag_nf (p : String) (add rem : List String) : tag '' nf p add rem = nf (tag p) (List.map tag add) (List.map tag rem)

theorem GaudisCrypt.Flatten.image_escape_nf (p : String) (hp : p ≠ "") (add rem : List String) : escape '' nf p add rem = nf (escape p) (List.map escape add) (List.map escape rem)

escape moves a nonempty prefix along (the empty one it would not: escape maps the names starting with @ to those starting with @@, not onto all).

def GaudisCrypt.Flatten.swapOK (p : String) (add rem add' rem' : List String) (a f : String) : Bool

nf p add' rem' is the image of nf p add rem under the swap of a and f: a and f trade membership, and the lists agree on every other name.

Equations

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

theorem GaudisCrypt.Flatten.contains_eq_of_all {l l' : List String} {a f : String} (h : ((l ++ l').all fun (x : String) => x == a || x == f || l.contains x == l'.contains x) = true) {m : String} (ha : m ≠ a) (hf : m ≠ f) : l.contains m = l'.contains m

theorem GaudisCrypt.Flatten.memB_swap {p : String} {add rem add' rem' : List String} {a f : String} (h : swapOK p add rem add' rem' a f = true) (m : String) : memB p add' rem' m = memB p add rem ((Equiv.swap a f) m)

The steps of cleanNameSet?: each takes the region in normal form and a check that the meta code proves by evaluation (rfl).

theorem GaudisCrypt.Flatten.image_tag_eq (S : Set String) (p : String) (add rem : List String) (p' : String) (add' rem' : List String) (hS : S = nf p add rem) (h : (tag p == p' && List.map tag add == add' && List.map tag rem == rem') = true) : tag '' S = nf p' add' rem'

theorem GaudisCrypt.Flatten.image_escape_eq (S : Set String) (p : String) (add rem : List String) (p' : String) (add' rem' : List String) (hS : S = nf p add rem) (h : (p != "" && escape p == p' && List.map escape add == add' && List.map escape rem == rem') = true) : escape '' S = nf p' add' rem'

theorem GaudisCrypt.Flatten.image_renameName_nil (S : Set String) (p : String) (add rem : List String) (hS : S = nf p add rem) : renameName [] '' S = nf p add rem

theorem GaudisCrypt.Flatten.image_renameName_cons (S : Set String) (a f : String) (ren : List (String × String)) (p : String) (add rem add' rem' : List String) (hS : renameName ren '' S = nf p add rem) (h : swapOK p add rem add' rem' a f = true) : renameName ((a, f) :: ren) '' S = nf p add' rem'

theorem GaudisCrypt.varLens_rename {n n' : String} {T : Type} (i : Nonempty T) (k : ℕ) (hk : k = VariableName.encode n) (k' : ℕ) (hk' : k' = VariableName.encode n') (h : n = n') : varLens { name := n, type := T, nonempty := i, key := k, keyCorrect := hk } = varLens { name := n', type := T, nonempty := i, key := k', keyCorrect := hk' }

The slot of a variable whose name is given as another term for the same string.

def GaudisCrypt.ProgramState.mapLocal (m : Lens VariableAssignment VariableAssignment) : Lens ProgramState ProgramState

A lens on the locals, as a lens on the program state that keeps the globals.

Equations

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

theorem GaudisCrypt.ProgramState.mapLocal_chain_globalL (m : Lens VariableAssignment VariableAssignment) : (mapLocal m).chain globalL = globalL

@[simp]

theorem GaudisCrypt.ProgramState.mapLocal_chain_intoLocal {A : Type u} (m : Lens VariableAssignment VariableAssignment) (L : Lens A VariableAssignment) : (mapLocal m).chain L.intoLocal = (m.chain L).intoLocal

@[simp]

theorem GaudisCrypt.ProgramState.mapLocal_chain_intoGlobal {A : Type u} (m : Lens VariableAssignment VariableAssignment) (g : Lens A VariableAssignment) : (mapLocal m).chain g.intoGlobal = g.intoGlobal

theorem GaudisCrypt.ProgramState.mapLocal_embed_chain_varLens (ι : String → String) (hι : Function.Injective ι) (n : String) (T : Type) (i : Nonempty T) (k : ℕ) (hk : k = VariableName.encode n) : (mapLocal (VariableAssignment.embed ι hι)).chain (varLens { name := n, type := T, nonempty := i, key := k, keyCorrect := hk }).intoLocal = (varLens { name := ι n, type := T, nonempty := i, key := VariableName.encode (ι n), keyCorrect := ⋯ }).intoLocal

Cleaning: a local variable seen through a renaming of the locals is the renamed variable. (The content type is spelled T rather than (VariableName.mk n T …).type: simp reduces the latter in the term before it looks for lemmas, so a lemma indexed by it would never be found.)

theorem GaudisCrypt.ProgramState.mapLocal_embed_get_entry (ι : String → String) (hι : Function.Injective ι) (names : List String) (tys : List Type) (hlen : names.length = tys.length) (hfix : ∀ n ∈ names, ι n = n) (args : typeListToTuple tys) (st : VariableAssignment) : (mapLocal (VariableAssignment.embed ι hι)).get { globals := st, locals := VariableAssignment.setParams names tys hlen args VariableAssignment.init } = { globals := st, locals := VariableAssignment.setParams names tys hlen args VariableAssignment.init }

A renaming of the locals leaves the entry state of a procedure alone when it keeps the names of the parameters: the parameters are where they were, and every other slot is init, whatever it is called.

theorem GaudisCrypt.ProgramState.mapLocal_embed_chainSetter_resetSetter (ι : String → String) (hι : Function.Injective ι) (S : Set String) : (mapLocal (VariableAssignment.embed ι hι)).chainSetter (resetSetter S) = resetSetter (ι '' S)

Cleaning: a reset seen through a renaming of the locals resets the renamed names.

theorem GaudisCrypt.resetSetter_univ_set (x : Unit) (σ : ProgramState) : (resetSetter Set.univ).set x σ = { globals := σ.globals, locals := VariableAssignment.init }

Resetting every variable.

noncomputable def GaudisCrypt.Flatten.trafo : Lens ProgramState ProgramState

The caller's side of a flattening round: its locals, renamed by escape (which keeps every name that does not start with @).

Equations

• GaudisCrypt.Flatten.trafo = GaudisCrypt.ProgramState.mapLocal (GaudisCrypt.VariableAssignment.embed GaudisCrypt.Flatten.escape GaudisCrypt.Flatten.escape_injective)

noncomputable def GaudisCrypt.Flatten.emb : Lens ProgramState ProgramState

The callee's frame inside the caller's locals, renamed by tag (n ↦ @.n).

Equations

• GaudisCrypt.Flatten.emb = GaudisCrypt.ProgramState.mapLocal (GaudisCrypt.VariableAssignment.embed GaudisCrypt.Flatten.tag GaudisCrypt.Flatten.tag_injective)

noncomputable def GaudisCrypt.Flatten.rename (ren : List (String × String)) : Lens ProgramState ProgramState

The cleanup renaming ren, on the locals: a permutation of the names, hence an isomorphism.

Equations

• GaudisCrypt.Flatten.rename ren = GaudisCrypt.ProgramState.mapLocal (GaudisCrypt.VariableAssignment.embed (GaudisCrypt.Flatten.renameName ren) ⋯)

theorem GaudisCrypt.Flatten.trafo_chain_globalL : trafo.chain ProgramState.globalL = ProgramState.globalL

theorem GaudisCrypt.Flatten.emb_chain_globalL : emb.chain ProgramState.globalL = ProgramState.globalL

theorem GaudisCrypt.Flatten.rename_chain_globalL (ren : List (String × String)) : (rename ren).chain ProgramState.globalL = ProgramState.globalL

theorem GaudisCrypt.Flatten.trafo_get_emb_set (v τ : ProgramState) : trafo.get (emb.set v τ) = ProgramState.globalL.set v.globals (trafo.get τ)

Writing the callee's frame is invisible to the caller, except for the globals.

theorem GaudisCrypt.Flatten.emb_chainSetter_resetSetter_univ_set (τ : ProgramState) : (emb.chainSetter (resetSetter Set.univ)).set () τ = emb.set { globals := τ.globals, locals := VariableAssignment.init } τ

The reset a flattened call starts with: every variable of the callee, seen through emb, which is the callee's frame.

@[simp]

theorem GaudisCrypt.Flatten.trafo_chain_varLens (n : String) (T : Type) (i : Nonempty T) (k : ℕ) (hk : k = VariableName.encode n) : trafo.chain (varLens { name := n, type := T, nonempty := i, key := k, keyCorrect := hk }).intoLocal = (varLens { name := escape n, type := T, nonempty := i, key := VariableName.encode (escape n), keyCorrect := ⋯ }).intoLocal

Cleaning: a caller's local variable, seen through trafo, is the escaped variable.

@[simp]

theorem GaudisCrypt.Flatten.emb_chain_varLens (n : String) (T : Type) (i : Nonempty T) (k : ℕ) (hk : k = VariableName.encode n) : emb.chain (varLens { name := n, type := T, nonempty := i, key := k, keyCorrect := hk }).intoLocal = (varLens { name := tag n, type := T, nonempty := i, key := VariableName.encode (tag n), keyCorrect := ⋯ }).intoLocal

Cleaning: a callee's local variable, seen through emb, is the tagged variable.

@[simp]

theorem GaudisCrypt.Flatten.rename_chain_varLens (ren : List (String × String)) (n : String) (T : Type) (i : Nonempty T) (k : ℕ) (hk : k = VariableName.encode n) : (rename ren).chain (varLens { name := n, type := T, nonempty := i, key := k, keyCorrect := hk }).intoLocal = (varLens { name := renameName ren n, type := T, nonempty := i, key := VariableName.encode (renameName ren n), keyCorrect := ⋯ }).intoLocal

Cleaning: a local variable, seen through the cleanup renaming, is the renamed variable.

The composite lenses stepAllCalls and withRenaming build (rename ren or trafo in front of the earlier rounds), reassociated so the variable lemmas above meet one renaming at a time. Stated per head rather than as Lens.chain_assoc, so that cleaning reassociates the inliner's own lenses only.

theorem GaudisCrypt.Flatten.rename_chain_chain {A : Type} (ren : List (String × String)) (l : Lens ProgramState ProgramState) (x : Lens A ProgramState) : ((rename ren).chain l).chain x = (rename ren).chain (l.chain x)

theorem GaudisCrypt.Flatten.trafo_chain_chain {A : Type} (l : Lens ProgramState ProgramState) (x : Lens A ProgramState) : (trafo.chain l).chain x = trafo.chain (l.chain x)

theorem GaudisCrypt.Flatten.emb_chain_chain {A : Type} (l : Lens ProgramState ProgramState) (x : Lens A ProgramState) : (emb.chain l).chain x = emb.chain (l.chain x)

A read at a state seen through one of the renamings, as a read through the composite: the plain-get counterparts of eval_chain_lens, for conditions whose reads were already turned into gets (hoareInline).

theorem GaudisCrypt.Flatten.get_rename {A : Type} (ren : List (String × String)) (τ : ProgramState) (x : Lens A ProgramState) : x.get ((rename ren).get τ) = ((rename ren).chain x).get τ

theorem GaudisCrypt.Flatten.get_trafo {A : Type} (τ : ProgramState) (x : Lens A ProgramState) : x.get (trafo.get τ) = (trafo.chain x).get τ

theorem GaudisCrypt.Flatten.get_emb {A : Type} (τ : ProgramState) (x : Lens A ProgramState) : x.get (emb.get τ) = (emb.chain x).get τ

theorem GaudisCrypt.Flatten.get_rename_chain {A : Type} (ren : List (String × String)) (l : Lens ProgramState ProgramState) (τ : ProgramState) (x : Lens A ProgramState) : x.get (((rename ren).chain l).get τ) = ((rename ren).chain (l.chain x)).get τ

theorem GaudisCrypt.Flatten.get_trafo_chain {A : Type} (l : Lens ProgramState ProgramState) (τ : ProgramState) (x : Lens A ProgramState) : x.get ((trafo.chain l).get τ) = (trafo.chain (l.chain x)).get τ

theorem GaudisCrypt.Flatten.get_emb_chain {A : Type} (l : Lens ProgramState ProgramState) (τ : ProgramState) (x : Lens A ProgramState) : x.get ((emb.chain l).get τ) = (emb.chain (l.chain x)).get τ

theorem GaudisCrypt.Flatten.emb_chain_varLens_eq (n : String) (T : Type) (i : Nonempty T) (k : ℕ) (hk : k = VariableName.encode n) (f : String) (k' : ℕ) (hk' : k' = VariableName.encode f) (h : tag n = f) : emb.chain (varLens { name := n, type := T, nonempty := i, key := k, keyCorrect := hk }).intoLocal = (varLens { name := f, type := T, nonempty := i, key := k', keyCorrect := hk' }).intoLocal

emb_chain_varLens, with the new name given: what the meta code instantiates, proving the name by evaluation.

theorem GaudisCrypt.Lens.chain_pair_eq {a b : Type u} {s : Type v} {t : Type w} (l : Lens s t) (x : Lens a s) (y : Lens b s) [x.Disjoint y] (x' : Lens a t) (y' : Lens b t) [x'.Disjoint y'] (hx : l.chain x = x') (hy : l.chain y = y') : l.chain (x.pair y) = x'.pair y'

A lens composed with a pair is the pair of the composites — stated with the composites given up to an equation (and any Disjoint instance for them), so that the cleaning pass can rewrite the components and re-synthesize the instance (Flatten.reduceChainPair).

Re-targeting a statement along a lens

def GaudisCrypt.StmtWithHoles.applyLens {h : HoleSigs} (l : Lens ProgramState ProgramState) : StmtWithHoles h → StmtWithHoles h

Re-target a statement along a lens between program states. The call' case does not recurse into the callee: its body and return value run in the callee's own frame, which the lens does not touch.

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.StmtWithHoles.applyLens l (GaudiProg[ skip; ]) = GaudiProg[ skip; ]
• GaudisCrypt.StmtWithHoles.applyLens l (GaudiProg[ x_1 <$ §e; ]) = GaudiProg[ (l.chainSetter x_1) <$ §(l.chainGetter e); ]
• GaudisCrypt.StmtWithHoles.applyLens l (GaudisCrypt.StmtWithHoles.call' x_1 ns hl hn b r p) = GaudisCrypt.StmtWithHoles.call' (l.chainSetter x_1) ns hl hn b r (l.chainGetter p)
• GaudisCrypt.StmtWithHoles.applyLens l (GaudiProg[ x_1 <- holecall n (§p); ]) = GaudiProg[ (l.chainSetter x_1) <- holecall n (§(l.chainGetter p)); ]
• GaudisCrypt.StmtWithHoles.applyLens l (s₁.seq s₂) = (GaudisCrypt.StmtWithHoles.applyLens l s₁).seq (GaudisCrypt.StmtWithHoles.applyLens l s₂)
• GaudisCrypt.StmtWithHoles.applyLens l (GaudisCrypt.StmtWithHoles.while c b) = GaudisCrypt.StmtWithHoles.while (l.chainGetter c) (GaudisCrypt.StmtWithHoles.applyLens l b)

theorem GaudisCrypt.StmtWithHoles.applyLens_instantiate {h : HoleSigs} (l : Lens ProgramState ProgramState) (inst : h.Instantiation) (s : StmtWithHoles h) : (applyLens l s).instantiate inst = applyLens l (s.instantiate inst)

applyLens commutes with hole instantiation: it never touches a hole's index, and the hole ↦ call step only re-tags the same setter and getter.

zoom against the primitives

(The equivalence StmtWithHoles.EquivInLens it is used for is in Logic/StmtEquiv.lean.)

theorem GaudisCrypt.ProgramDenotation.zoom_chain {s : Type u₁} {t : Type u₂} {u : Type u₃} {a : Type v} (x : Lens t u) (y : Lens s t) (p : ProgramDenotation s a) : zoom (x.chain y) p = zoom x (zoom y p)

Zooming twice is zooming along the chained lens.

theorem GaudisCrypt.ProgramDenotation.zoom_get {s t : Type u} {a : Type v} (l : Lens s t) (g : Getter a s) : zoom l (get g) = get (l.chainGetter g)

Reading through a zoomed lens is reading through the composed getter.

theorem GaudisCrypt.ProgramDenotation.zoom_set {s t : Type u} {a : Type v} (l : Lens s t) (x : Setter a s) (v : a) : zoom l (set x v) = set (l.chainSetter x) v

Writing through a zoomed lens is writing through the composed setter.

theorem GaudisCrypt.ProgramDenotation.zoom_lift {s t : Type u} {a : Type v} (l : Lens s t) (μ : SubProbability a) : zoom l μ.toProgramDenotation = μ.toProgramDenotation

A state-blind draw is unaffected by zooming.

theorem GaudisCrypt.ProgramDenotation.zoom_bot {s t : Type u} {a : Type v} (l : Lens s t) : zoom l ⊥ = ⊥

Zooming the everywhere-diverging program diverges.

theorem GaudisCrypt.ProgramDenotation.zoom_ωScottContinuous {s t : Type u} {a : Type v} (l : Lens s t) : OmegaCompletePartialOrder.ωScottContinuous fun (m : ProgramDenotation s a) => zoom l m

zoom is ω-continuous in its program argument — what the loop case needs.

theorem GaudisCrypt.ProgramDenotation.zoom_while {s t : Type u} (l : Lens s t) (cond : ProgramDenotation s Bool) (body : ProgramDenotation s Unit) : zoom l (while_loop cond body) = while_loop (zoom l cond) (zoom l body)

zoom commutes with while_loop (Kleene/ωSup argument): running the whole loop in the sublens and writing back once is the same as writing back after every iteration.

The transport theorem

applyLens l s runs s in the sublens l — which is exactly zoom l. The only assumption is that l leaves the globals alone, which is what a call needs (the callee runs on the globals, and must see the same ones before and after re-targeting).

This holds for an arbitrary statement s, which is why the flattener may wrap whole subprograms in applyLens without looking at them.

theorem GaudisCrypt.programDenotation_applyLens (l : Lens ProgramState ProgramState) (hglob : l.chain ProgramState.globalL = ProgramState.globalL) (s : Stmt) : programDenotation (StmtWithHoles.applyLens l s) = ProgramDenotation.zoom l (programDenotation s)

theorem GaudisCrypt.ProgramDenotation.equivInLens_zoom {s t : Type u} {α : Type v} (l : Lens s t) (p : ProgramDenotation s α) : p.EquivInLens (zoom l p) l

Zooming is always a correct replacement: projecting the result of the zoomed program back gives the original program's result.

theorem GaudisCrypt.StmtWithHoles.equivInLens_applyLens {hCtx : HoleSigs} (l : Lens ProgramState ProgramState) (hglob : l.chain ProgramState.globalL = ProgramState.globalL) (s : StmtWithHoles hCtx) : s.EquivInLens (applyLens l s) l

applyLens is always the right replacement: whatever the statement, re-targeting it along a globals-preserving lens is denotationally equivalent in that lens.

Placing a hole-free statement into a hole context

A flattened callee body is hole-free, but the statement it is spliced into need not be.

@[irreducible]

def GaudisCrypt.StmtWithHoles.weaken {h : HoleSigs} : Stmt → StmtWithHoles h

Re-type a hole-free statement in any hole context. (hole cannot occur: HoleIndex .empty is uninhabited.)

Equations

• GaudisCrypt.StmtWithHoles.weaken (GaudiProg[ skip; ]) = GaudiProg[ skip; ]
• GaudisCrypt.StmtWithHoles.weaken (GaudiProg[ x_1 <$ §e; ]) = GaudiProg[ x_1 <$ §e; ]
• GaudisCrypt.StmtWithHoles.weaken (GaudisCrypt.StmtWithHoles.call' x_1 ns hl hn b r p) = GaudisCrypt.StmtWithHoles.call' x_1 ns hl hn b r p
• GaudisCrypt.StmtWithHoles.weaken (s₁.seq s₂) = (GaudisCrypt.StmtWithHoles.weaken s₁).seq (GaudisCrypt.StmtWithHoles.weaken s₂)
• GaudisCrypt.StmtWithHoles.weaken (GaudisCrypt.StmtWithHoles.ifThenElse c t e) = GaudisCrypt.StmtWithHoles.ifThenElse c (GaudisCrypt.StmtWithHoles.weaken t) (GaudisCrypt.StmtWithHoles.weaken e)
• GaudisCrypt.StmtWithHoles.weaken (GaudisCrypt.StmtWithHoles.while c b) = GaudisCrypt.StmtWithHoles.while c (GaudisCrypt.StmtWithHoles.weaken b)

theorem GaudisCrypt.StmtWithHoles.weaken_instantiate {h : HoleSigs} (inst : h.Instantiation) (s : Stmt) : (weaken s).instantiate inst = s

Weakening is undone by instantiation: a hole-free statement has nothing to fill in.

Flattening one call

The one step with real content. Everything else above is congruence and transport.

theorem GaudisCrypt.programDenotation_call'_apply {sig : ProcedureSignature} (x : Setter sig.ret ProgramState) (names : List String) (hlen : names.length = sig.params.length) (hnodup : names.Nodup) (b : Stmt) (r : Getter sig.ret ProgramState) (args : Getter sig.ParamType ProgramState) (s : ProgramState) : programDenotation (StmtWithHoles.call' x names hlen hnodup b r args) s = do let z ← programDenotation b { globals := s.globals, locals := VariableAssignment.setParams names sig.params hlen (args.get s) VariableAssignment.init } pure ((), x.set (r.get z.2) (ProgramState.globalL.set z.2.globals s))

A call statement, run at a state: run the callee's body on fresh locals holding the arguments, then store its return value.

theorem GaudisCrypt.flattenedCall_apply {sig : ProcedureSignature} (trafo emb : Lens ProgramState ProgramState) (heg : emb.chain ProgramState.globalL = ProgramState.globalL) (x : Setter sig.ret ProgramState) (b : Stmt) (r : Getter sig.ret ProgramState) (f : ProgramState → ProgramState) (τ : ProgramState) : ((fun (σ : ProgramState) => pure ((), f σ)) >>= fun (x_1 : Unit) => do programDenotation (StmtWithHoles.applyLens emb b) let v ← ProgramDenotation.get (emb.chainGetter r) ProgramDenotation.set (trafo.chainSetter x) v) τ = do let w ← programDenotation b (emb.get (f τ)) pure ((), trafo.set (x.set (r.get w.2) (trafo.get (emb.set w.2 (f τ)))) (emb.set w.2 (f τ)))

The expansion of a call, run at a state: after the prelude f, the callee's body runs in emb, and its return value is stored through the caller's setter.

theorem GaudisCrypt.equivInLens_flattenCall {sig : ProcedureSignature} (trafo emb : Lens ProgramState ProgramState) (htg : trafo.chain ProgramState.globalL = ProgramState.globalL) (heg : emb.chain ProgramState.globalL = ProgramState.globalL) (hdisj : ∀ (v τ : ProgramState), trafo.get (emb.set v τ) = ProgramState.globalL.set v.globals (trafo.get τ)) (x : Setter sig.ret ProgramState) (names : List String) (hlen : names.length = sig.params.length) (hnodup : names.Nodup) (args : Getter sig.ParamType ProgramState) (b : Stmt) (r : Getter sig.ret ProgramState) (f : ProgramState → ProgramState) (hpre_get : ∀ (τ : ProgramState), emb.get (f τ) = { globals := τ.globals, locals := VariableAssignment.setParams names sig.params hlen (args.get (trafo.get τ)) VariableAssignment.init }) (hpre_vis : ∀ (τ : ProgramState), trafo.get (f τ) = trafo.get τ) : (programDenotation (StmtWithHoles.call' x names hlen hnodup b r args)).EquivInLens (do fun (σ : ProgramState) => pure ((), f σ) programDenotation (StmtWithHoles.applyLens emb b) let v ← ProgramDenotation.get (emb.chainGetter r) ProgramDenotation.set (trafo.chainSetter x) v) trafo

Flattening a call is sound. A call is denotationally equivalent, along trafo, to

• a prelude f that puts the callee's entry locals into the callee's frame of the wide state (hpre_get) without disturbing anything visible through trafo (hpre_vis);
• the callee's body, re-targeted with applyLens emb;
• a store of the callee's return value through the caller's setter.

The two lenses must preserve the globals (htg, heg), and writing the callee's frame must be invisible through trafo except for the globals (hdisj).

theorem GaudisCrypt.StmtWithHoles.equivInLens_flattenCall {hCtx : HoleSigs} {sig : ProcedureSignature} (trafo emb : Lens ProgramState ProgramState) (htg : trafo.chain ProgramState.globalL = ProgramState.globalL) (heg : emb.chain ProgramState.globalL = ProgramState.globalL) (hdisj : ∀ (v τ : ProgramState), trafo.get (emb.set v τ) = ProgramState.globalL.set v.globals (trafo.get τ)) (x : Setter sig.ret ProgramState) (names : List String) (hlen : names.length = sig.params.length) (hnodup : names.Nodup) (args : Getter sig.ParamType ProgramState) (b : Stmt) (r : Getter sig.ret ProgramState) (pre : StmtWithHoles hCtx) (f : ProgramState → ProgramState) (hpre : ∀ (inst : hCtx.Instantiation) (τ : ProgramState), programDenotation (pre.instantiate inst) τ = pure ((), f τ)) (hpre_get : ∀ (τ : ProgramState), emb.get (f τ) = { globals := τ.globals, locals := VariableAssignment.setParams names sig.params hlen (args.get (trafo.get τ)) VariableAssignment.init }) (hpre_vis : ∀ (τ : ProgramState), trafo.get (f τ) = trafo.get τ) : (call' x names hlen hnodup b r args).EquivInLens (pre.seq ((weaken (applyLens emb b)).seq (GaudiProg[ (trafo.chainSetter x) <- §(emb.chainGetter r); ]))) trafo

The statement-level form, for any prelude pre that is the deterministic state map f.

def GaudisCrypt.Flatten.IsParamWriter (emb : Lens ProgramState ProgramState) (names : List String) (tys : List Type) (hlen : names.length = tys.length) (P : Setter (typeListToTuple tys) ProgramState) : Prop

P writes an argument tuple into the parameter slots names of the callee's frame emb: the wide-state form of VariableAssignment.setParams. The meta code builds P as the tuple of the parameters' renamed variables, which is how it prints.

Equations

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

theorem GaudisCrypt.Flatten.isParamWriter_nil (emb : Lens ProgramState ProgramState) (hlen : [].length = [].length) : IsParamWriter emb [] [] hlen Setter.throwaway

No parameters: nothing to write.

theorem GaudisCrypt.Flatten.isParamWriter_single (emb : Lens ProgramState ProgramState) (n : String) (T : Type) (i : Nonempty T) (k : ℕ) (hk : k = VariableName.encode n) (hlen : [n].length = [T].length) (L : Lens T ProgramState) (hL : emb.chain (varLens { name := n, type := T, nonempty := i, key := k, keyCorrect := hk }).intoLocal = L) : IsParamWriter emb [n] [T] hlen L.toSetter

One parameter: its variable, seen through emb.

theorem GaudisCrypt.Flatten.isParamWriter_cons (emb : Lens ProgramState ProgramState) (n n' : String) (ns : List String) (T T' : Type) (Ts : List Type) (i : Nonempty T) (k : ℕ) (hk : k = VariableName.encode n) (hlen : (n :: n' :: ns).length = (T :: T' :: Ts).length) (hlen' : (n' :: ns).length = (T' :: Ts).length) (L₁ : Lens T ProgramState) (L₂ : Lens (typeListToTuple (T' :: Ts)) ProgramState) (hL₁ : emb.chain (varLens { name := n, type := T, nonempty := i, key := k, keyCorrect := hk }).intoLocal = L₁) [hd : L₁.Disjoint L₂] (hrest : IsParamWriter emb (n' :: ns) (T' :: Ts) hlen' L₂.toSetter) : IsParamWriter emb (n :: n' :: ns) (T :: T' :: Ts) hlen (L₁.pair L₂).toSetter

Two or more parameters: the first one's variable, paired with the rest.

theorem GaudisCrypt.Flatten.equivInLens_call {hCtx : HoleSigs} {sig : ProcedureSignature} (x : Setter sig.ret ProgramState) (names : List String) (hlen : names.length = sig.params.length) (hnodup : names.Nodup) (b : Stmt) (r : Getter sig.ret ProgramState) (args : Getter sig.ParamType ProgramState) (P : Setter (typeListToTuple sig.params) ProgramState) (hP : IsParamWriter emb names sig.params hlen P) : (StmtWithHoles.call' x names hlen hnodup b r args).EquivInLens (GaudiProg[ (emb.chainSetter (resetSetter Set.univ)) <- (); ].seq (GaudiProg[ P <- §(trafo.chainGetter args); ].seq ((StmtWithHoles.weaken (StmtWithHoles.applyLens emb b)).seq (GaudiProg[ (trafo.chainSetter x) <- §(emb.chainGetter r); ])))) trafo

Flattening a call, as the meta code instantiates it: the call is equivalent, along trafo, to resetting the callee's frame, writing the arguments with P, the callee's body in emb, and the store of its return value. Every side condition of the general StmtWithHoles.equivInLens_flattenCall is discharged here, once.

P's content type is spelled typeListToTuple sig.params, not sig.ParamType: the two are equal by definition, but only the former reduces at the transparency simp matches at, and the cleaning lemmas have to see the parameters' types inside P when a later round renames them.

The procedure level

What turns the statement-level result into a fact about procedureDenotation, and therefore into something usable where the procedure is called.

def GaudisCrypt.Flatten.FixesEntry (names : List String) (tys : List Type) (hlen : names.length = tys.length) (l : Lens ProgramState ProgramState) : Prop

l leaves the entry state of a procedure with parameters names : tys alone: the arguments in their slots, init everywhere else.

Equations

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

theorem GaudisCrypt.Flatten.fixesEntry_trafo (names : List String) (tys : List Type) (hlen : names.length = tys.length) (hfix : ∀ n ∈ names, escape n = n) : FixesEntry names tys hlen trafo

theorem GaudisCrypt.Flatten.fixesEntry_rename (ren : List (String × String)) (names : List String) (tys : List Type) (hlen : names.length = tys.length) (hfix : ∀ n ∈ names, renameName ren n = n) : FixesEntry names tys hlen (rename ren)

theorem GaudisCrypt.Flatten.chain_chain_globalL {l m : Lens ProgramState ProgramState} (hl : l.chain ProgramState.globalL = ProgramState.globalL) (hm : m.chain ProgramState.globalL = ProgramState.globalL) : (m.chain l).chain ProgramState.globalL = ProgramState.globalL

Two renamings that keep the globals compose to one that keeps them.

theorem GaudisCrypt.Flatten.FixesEntry.chain {names : List String} {tys : List Type} {hlen : names.length = tys.length} {l m : Lens ProgramState ProgramState} (hl : FixesEntry names tys hlen l) (hm : FixesEntry names tys hlen m) : FixesEntry names tys hlen (m.chain l)

theorem GaudisCrypt.Flatten.procedureDenotation_congr {sig : ProcedureSignature} (names : List String) (hlen : names.length = sig.params.length) (hnodup : names.Nodup) (l : Lens ProgramState ProgramState) (b b' : Stmt) (r : Getter sig.ret ProgramState) (hb : StmtWithHoles.EquivInLens b b' l) (hinit : FixesEntry names sig.params hlen l) (hglobL : l.chain ProgramState.globalL = ProgramState.globalL) : procedureDenotation { parameterNames := names, parameterNames_length := hlen, parameterNames_nodup := hnodup, body := b', return_val := l.chainGetter r } = procedureDenotation { parameterNames := names, parameterNames_length := hlen, parameterNames_nodup := hnodup, body := b, return_val := r }

The procedure-level statement: flattening the body of a procedure does not change what it computes, given that the renaming leaves the entry state and the globals alone.

The lemmas cleanStmt rewrites with

The closed set. Flatten.cleanLemmas lists exactly these names and nothing else; the cleaning pass runs simp only with that list, the name evaluation of Flatten.reduceNames and VariableName.reduceEncode, no default simp set and zeta := false, so statement lets survive.

Three groups: through the statement wrappers (applyLens, weaken), into l-values, and into expressions. Everything that does not match keeps its wrapper — that costs prettiness, never correctness.

Through the statement wrappers

@[simp]

theorem GaudisCrypt.StmtWithHoles.applyLens_skip {h : HoleSigs} (l : Lens ProgramState ProgramState) : applyLens l (GaudiProg[ skip; ]) = GaudiProg[ skip; ]

@[simp]

theorem GaudisCrypt.StmtWithHoles.applyLens_sample {h : HoleSigs} {A : Type} (l : Lens ProgramState ProgramState) (x : Setter A ProgramState) (e : Getter (SubProbability A) ProgramState) : applyLens l (GaudiProg[ x <$ §e; ]) = GaudiProg[ (l.chainSetter x) <$ §(l.chainGetter e); ]

@[simp]

theorem GaudisCrypt.StmtWithHoles.applyLens_assign {h : HoleSigs} {A : Type} (l : Lens ProgramState ProgramState) (x : Setter A ProgramState) (e : Getter A ProgramState) : applyLens l (GaudiProg[ x <- §e; ]) = GaudiProg[ (l.chainSetter x) <- §(l.chainGetter e); ]

@[simp]

theorem GaudisCrypt.StmtWithHoles.applyLens_call' {h : HoleSigs} {sig : ProcedureSignature} (l : Lens ProgramState ProgramState) (x : Setter sig.ret ProgramState) (ns : List String) (hl : ns.length = sig.params.length) (hn : ns.Nodup) (b : Stmt) (r : Getter sig.ret ProgramState) (p : Getter sig.ParamType ProgramState) : applyLens l (call' x ns hl hn b r p) = call' (l.chainSetter x) ns hl hn b r (l.chainGetter p)

@[simp]

theorem GaudisCrypt.StmtWithHoles.applyLens_call {h : HoleSigs} {sig : ProcedureSignature} (l : Lens ProgramState ProgramState) (x : Setter sig.ret ProgramState) (p : Procedure sig) (args : Getter sig.ParamType ProgramState) : applyLens l (GaudiProg[ x <- call p (§args); ]) = GaudiProg[ (l.chainSetter x) <- call p (§(l.chainGetter args)); ]

@[simp]

theorem GaudisCrypt.StmtWithHoles.applyLens_hole {h : HoleSigs} {sig : ProcedureSignature} (l : Lens ProgramState ProgramState) (n : HoleIndex h sig) (x : Setter sig.ret ProgramState) (p : Getter sig.ParamType ProgramState) : applyLens l (GaudiProg[ x <- holecall n (§p); ]) = GaudiProg[ (l.chainSetter x) <- holecall n (§(l.chainGetter p)); ]

@[simp]

theorem GaudisCrypt.StmtWithHoles.applyLens_seq {h : HoleSigs} (l : Lens ProgramState ProgramState) (s₁ s₂ : StmtWithHoles h) : applyLens l (s₁.seq s₂) = (applyLens l s₁).seq (applyLens l s₂)

@[simp]

theorem GaudisCrypt.StmtWithHoles.applyLens_ifThenElse {h : HoleSigs} (l : Lens ProgramState ProgramState) (c : Getter Bool ProgramState) (t e : StmtWithHoles h) : applyLens l (ifThenElse c t e) = ifThenElse (l.chainGetter c) (applyLens l t) (applyLens l e)

@[simp]

theorem GaudisCrypt.StmtWithHoles.applyLens_while {h : HoleSigs} (l : Lens ProgramState ProgramState) (c : Getter Bool ProgramState) (b : StmtWithHoles h) : applyLens l («while» c b) = «while» (l.chainGetter c) (applyLens l b)

@[simp]

theorem GaudisCrypt.StmtWithHoles.applyLens_applyLens {h : HoleSigs} (l m : Lens ProgramState ProgramState) (s : StmtWithHoles h) : applyLens m (applyLens l s) = applyLens (m.chain l) s

Two nested re-targetings collapse into one — what a second flattening round leaves behind.

@[simp]

theorem GaudisCrypt.StmtWithHoles.weaken_skip {h : HoleSigs} : weaken (GaudiProg[ skip; ]) = GaudiProg[ skip; ]

@[simp]

theorem GaudisCrypt.StmtWithHoles.weaken_sample {h : HoleSigs} {A : Type} (x : Setter A ProgramState) (e : Getter (SubProbability A) ProgramState) : weaken (GaudiProg[ x <$ §e; ]) = GaudiProg[ x <$ §e; ]

@[simp]

theorem GaudisCrypt.StmtWithHoles.weaken_assign {h : HoleSigs} {A : Type} (x : Setter A ProgramState) (e : Getter A ProgramState) : weaken (GaudiProg[ x <- §e; ]) = GaudiProg[ x <- §e; ]

@[simp]

theorem GaudisCrypt.StmtWithHoles.weaken_call' {h : HoleSigs} {sig : ProcedureSignature} (x : Setter sig.ret ProgramState) (ns : List String) (hl : ns.length = sig.params.length) (hn : ns.Nodup) (b : Stmt) (r : Getter sig.ret ProgramState) (p : Getter sig.ParamType ProgramState) : weaken (call' x ns hl hn b r p) = call' x ns hl hn b r p

@[simp]

theorem GaudisCrypt.StmtWithHoles.weaken_call {h : HoleSigs} {sig : ProcedureSignature} (x : Setter sig.ret ProgramState) (p : Procedure sig) (args : Getter sig.ParamType ProgramState) : weaken (GaudiProg[ x <- call p (§args); ]) = GaudiProg[ x <- call p (§args); ]

@[simp]

theorem GaudisCrypt.StmtWithHoles.weaken_seq {h : HoleSigs} (s₁ s₂ : Stmt) : weaken (seq s₁ s₂) = (weaken s₁).seq (weaken s₂)

@[simp]

theorem GaudisCrypt.StmtWithHoles.weaken_ifThenElse {h : HoleSigs} (c : Getter Bool ProgramState) (t e : Stmt) : weaken (ifThenElse c t e) = ifThenElse c (weaken t) (weaken e)

@[simp]

theorem GaudisCrypt.StmtWithHoles.weaken_while {h : HoleSigs} (c : Getter Bool ProgramState) (b : Stmt) : weaken («while» c b) = «while» c (weaken b)

@[simp]

theorem GaudisCrypt.StmtWithHoles.weaken_applyLens {h : HoleSigs} (l : Lens ProgramState ProgramState) (s : Stmt) : weaken (applyLens l s) = applyLens l (weaken s)

Weakening and re-targeting commute, so the two wrappers can be pushed inwards together.

Into l-values

@[simp]

theorem GaudisCrypt.Lens.chainSetter_liftLens {A : Type} (l : Lens ProgramState ProgramState) (x : Lens A ProgramState) : l.chainSetter (liftLens x) = liftLens (l.chain x)

A variable used as an l-value travels along the lens.

@[simp]

theorem GaudisCrypt.Lens.chainSetter_liftLens_global {A : Type} (m : Lens VariableAssignment VariableAssignment) (g : Lens A VariableAssignment) : (ProgramState.mapLocal m).chainSetter (liftLens g) = liftLens g

A global l-value is unaffected by a renaming of the locals.

@[simp]

theorem GaudisCrypt.Lens.chainSetter_throwaway {A : Type} {s t : Type u} (l : Lens s t) : l.chainSetter Setter.throwaway = Setter.throwaway

A discarded result stays discarded, so a void call does not acquire an l-value.

@[simp]

theorem GaudisCrypt.Lens.chainSetter_toSetter {a : Type u} {s : Type v} {t : Type w} (l : Lens s t) (x : Lens a s) : l.chainSetter x.toSetter = (l.chain x).toSetter

A lens used as an l-value composes as a lens.

@[simp]

theorem GaudisCrypt.Lens.chainSetter_chainSetter {a : Type u} {s t u' : Type v} (m : Lens t u') (l : Lens s t) (x : Setter a s) : m.chainSetter (l.chainSetter x) = (m.chain l).chainSetter x

@[simp]

theorem GaudisCrypt.Lens.chainGetter_chainGetter {a : Type u} {s t u' : Type v} (m : Lens t u') (l : Lens s t) (g : Getter a s) : m.chainGetter (l.chainGetter g) = (m.chain l).chainGetter g

@[simp]

theorem GaudisCrypt.Lens.chainGetter_toGetter {a : Type u} {s : Type v} {t : Type w} (l : Lens s t) (x : Lens a s) : l.chainGetter x.toGetter = (l.chain x).toGetter

A lens read as an expression composes as a lens.

Into expressions

A GaudiExpr getter is Getter.mk (fun st => body) with every variable read spelled eval x at the current state ⟨st⟩. Composing it with a lens beta-reduces to the same body at l.get st, and these lemmas move the lens from the state to the variable — after which the variable lemmas rename it, and the read prints as §x again.

@[simp]

theorem GaudisCrypt.eval_chain_lens {A : Type} (l : Lens ProgramState ProgramState) (τ : ProgramState) (x : Lens A ProgramState) : §x = §(l.chain x)

@[simp]

theorem GaudisCrypt.eval_chain_getter {A : Type} (l : Lens ProgramState ProgramState) (τ : ProgramState) (x : Getter A ProgramState) : §x = §(l.chainGetter x)

@[simp]

theorem GaudisCrypt.eval_mapLocal_global_lens {A : Type} (m : Lens VariableAssignment VariableAssignment) (τ : ProgramState) (g : Lens A VariableAssignment) : §g = §g

@[simp]

theorem GaudisCrypt.eval_mapLocal_global_getter {A : Type} (m : Lens VariableAssignment VariableAssignment) (τ : ProgramState) (g : Getter A VariableAssignment) : §g = §g

The three renamings, unfolded where the lemmas above need mapLocal

trafo, emb and rename ren are definitions (so that they print by name), and simp does not see the mapLocal inside; each gets the global-variable lemmas restated.

@[simp]

theorem GaudisCrypt.Flatten.trafo_chainSetter_liftLens_global {A : Type} (g : Lens A VariableAssignment) : trafo.chainSetter (liftLens g) = liftLens g

@[simp]

theorem GaudisCrypt.Flatten.emb_chainSetter_liftLens_global {A : Type} (g : Lens A VariableAssignment) : emb.chainSetter (liftLens g) = liftLens g

@[simp]

theorem GaudisCrypt.Flatten.rename_chainSetter_liftLens_global {A : Type} (ren : List (String × String)) (g : Lens A VariableAssignment) : (rename ren).chainSetter (liftLens g) = liftLens g

@[simp]

theorem GaudisCrypt.Flatten.trafo_chain_intoGlobal {A : Type} (g : Lens A VariableAssignment) : trafo.chain g.intoGlobal = g.intoGlobal

@[simp]

theorem GaudisCrypt.Flatten.emb_chain_intoGlobal {A : Type} (g : Lens A VariableAssignment) : emb.chain g.intoGlobal = g.intoGlobal

@[simp]

theorem GaudisCrypt.Flatten.rename_chain_intoGlobal {A : Type} (ren : List (String × String)) (g : Lens A VariableAssignment) : (rename ren).chain g.intoGlobal = g.intoGlobal

@[simp]

theorem GaudisCrypt.Flatten.eval_trafo_global_lens {A : Type} (τ : ProgramState) (g : Lens A VariableAssignment) : §g = §g

@[simp]

theorem GaudisCrypt.Flatten.eval_emb_global_lens {A : Type} (τ : ProgramState) (g : Lens A VariableAssignment) : §g = §g

@[simp]

theorem GaudisCrypt.Flatten.eval_rename_global_lens {A : Type} (ren : List (String × String)) (τ : ProgramState) (g : Lens A VariableAssignment) : §g = §g

@[simp]

theorem GaudisCrypt.Flatten.eval_trafo_global_getter {A : Type} (τ : ProgramState) (g : Getter A VariableAssignment) : §g = §g

@[simp]

theorem GaudisCrypt.Flatten.eval_emb_global_getter {A : Type} (τ : ProgramState) (g : Getter A VariableAssignment) : §g = §g

@[simp]

theorem GaudisCrypt.Flatten.eval_rename_global_getter {A : Type} (ren : List (String × String)) (τ : ProgramState) (g : Getter A VariableAssignment) : §g = §g

Resets

A renaming around a reset resets the renamed region; cleanNameSet? then puts the region back in normal form.

@[simp]

theorem GaudisCrypt.Flatten.trafo_chainSetter_resetSetter (S : Set String) : trafo.chainSetter (resetSetter S) = resetSetter (escape '' S)

@[simp]

theorem GaudisCrypt.Flatten.emb_chainSetter_resetSetter (S : Set String) : emb.chainSetter (resetSetter S) = resetSetter (tag '' S)

@[simp]

theorem GaudisCrypt.Flatten.rename_chainSetter_resetSetter (ren : List (String × String)) (S : Set String) : (rename ren).chainSetter (resetSetter S) = resetSetter (renameName ren '' S)

The meta code

The passes, of which only the first can fail:

• flattenCall n — flatten call site n, leaving deliberately ugly terms behind: everything off the path to the call is wrapped in applyLens trafo without being looked at;
• cleanStmt — push those wrappers inwards with the closed lemma set of Clean;
• flattenSeq — re-associate seq to the right and drop skip and _ <- e;
• flattenCallCleaned n — the three in a row, proofs composed. The callee's variables now have made-up names («@.w»);
• renameNames — the cleanup: give the made-up names readable ones (w, or w0 on a clash), by one renaming of the whole statement;
• flattenProcedureCalls — repeat flattenCallCleaned until no call can be flattened, then renameNames.

flattenProcedure does it to a procedure, and Inlining (unfoldProcedure, inlineProcedure) evaluates a callee that is named through modules first.

@[reducible, inline]

abbrev GaudisCrypt.Flatten.Expr : Type

Lean.Expr, under a name that GaudisCrypt.Expr (the program-expression abbreviation) does not shadow.

Equations

• GaudisCrypt.Flatten.Expr = Lean.Expr

Evaluating renamed names

partial def GaudisCrypt.Flatten.renOfExpr? (e : Expr) : Option (List (String × String))

A literal List (String × String), read back.

def GaudisCrypt.Flatten.evalName? (e : Expr) : Option String

escape n, tag n or renameName ren n, with ren and n literals, evaluated.

Equations

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

def GaudisCrypt.Flatten.reduceVarName : Lean.Meta.Simp.Simproc

varLens ⟨escape "x", T, …⟩ (or tag, renameName ren) ↦ varLens ⟨"y", T, …⟩, the name evaluated and the key with it, by varLens_rename.

A proof, not a definitional step: the two are equal by definition too, but checking that means evaluating VariableName.encode of a computed string, which decodes it character by character in the unifier (tens of seconds for a short name). With the proof, the name is compared once, and the key is the literal's.

Equations

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

Reset regions in normal form

Everything the meta code knows about the normal form of a reset region (section Reset regions above) is in this section; cleanNameSet? is its entry point.

def GaudisCrypt.Flatten.nfExpr (p : String) (add rem : List String) : Expr

nf p add rem, as a term.

Equations

• GaudisCrypt.Flatten.nfExpr p add rem = Lean.mkAppN (Lean.mkConst `GaudisCrypt.Flatten.nf) #[Lean.mkStrLit p, Lean.toExpr add, Lean.toExpr rem]

partial def GaudisCrypt.Flatten.ofListToLit (l : List String) : Lean.MetaM (Expr × Expr)

A nonempty ofList l as a set literal {a, b, …}, with a proof of ofList l = ‹it›.

partial def GaudisCrypt.Flatten.litToList? (e : Expr) : Option (List String)

A set literal {a, b, …} of strings, read back.

def GaudisCrypt.Flatten.nfToPretty (p : String) (add rem : List String) : Lean.MetaM (Expr × Expr)

nf p add rem, written out without its empty parts, with a proof of nf p add rem = ‹it›.

Equations

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

def GaudisCrypt.Flatten.nfOfExpr? (S : Expr) : Lean.MetaM (Option (String × List String × List String × Expr))

A reset region as nfToPretty writes it (or Set.univ), read back as nf p add rem, with a proof of S = nf p add rem.

Equations

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

def GaudisCrypt.Flatten.swapNF (p : String) (add rem : List String) (a f : String) : List String × List String

The image of nf p add rem under the swap of a and f, in normal form: a name leaving the set goes out of add and, if it has the prefix, into rem; a name entering it goes out of rem if it has the prefix, and into add otherwise. New names go to the front, so that after a whole renaming (whose last pair is swapped first) add and rem are in the order of the renaming.

Equations

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

def GaudisCrypt.Flatten.applyCheck (lem : Expr) : Lean.MetaM Expr

Apply the lemma lem (partially applied) to a proof, by evaluation, of its next hypothesis, a Bool check … = true.

Equations

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

partial def GaudisCrypt.Flatten.renameNF (S : Expr) (p : String) (add rem : List String) (hS renE : Expr) : Lean.MetaM (Option (List String × List String × Expr))

renameName ren '' S in normal form, given S in normal form: the swaps of ren one at a time, the last pair first (image_renameName_nil/_cons).

def GaudisCrypt.Flatten.cleanNameSet? (e : Expr) : Lean.MetaM (Option Lean.Meta.Simp.Result)

The set cleaning: ι '' S, for S in normal form (or Set.univ) and ι one of tag, escape, renameName ren (with ren a literal), in normal form again, written out (nfToPretty). none when the term is not of that shape.

def GaudisCrypt.Flatten.reduceNameSet : Lean.Meta.Simp.Simproc

See cleanNameSet?.

Equations

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

def GaudisCrypt.Flatten.reduceChainPair : Lean.Meta.Simp.Simproc

l.chain (Lens.pair x y) ↦ Lens.pair x' y', where x', y' are l.chain x, l.chain y cleaned (renamed, typically) and the Disjoint instance is synthesized for them anew. Not a plain lemma: the instance argument of Lens.pair depends on the components, so simp cannot rewrite them in place.

Equations

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

Statements

structure GaudisCrypt.Flatten.FlattenStep : Type

What one flattening step produces: the rewritten statement, the renaming lens, and a proof of ‹input›.EquivInLens stmt trafo.

• stmt : Expr

  The rewritten statement.

• trafo : Expr

  The renaming lens: the caller's locals, renamed.

• proof : Expr

  A proof of ‹input›.EquivInLens stmt trafo.

• hCtx : Expr

  The hole context.

def GaudisCrypt.Flatten.unfoldStmt (e : Expr) : Lean.MetaM Expr

Expose the statement hiding behind projections and definitions (someProc.body), without zeta-reducing the lets of the statement — those are the user's own binders.

Equations

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

partial def GaudisCrypt.Flatten.listLitElems (e : Expr) : Lean.MetaM (List Expr)

The elements of a literal List expression. Reducible transparency only: a callee named by a definition stays stuck here, which is what makes "literal callees only" bite.

def GaudisCrypt.Flatten.stringListLit (e : Expr) : Lean.MetaM (List String)

The strings of a literal List String.

Equations

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

def GaudisCrypt.Flatten.isCallSite (e : Expr) : Bool

Is this application a call site — one of the two call forms, or a hole?

A hole is a call whose callee is not known yet, so it is one of the things a user counts when numbering the call sites of a statement, even though neither flattening nor inlining can do anything with it. Numbering it along with the rest is what keeps the call-site numbers of a statement independent of which sites happen to be flattenable.

Equations

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

partial def GaudisCrypt.Flatten.countCallSites (e₀ : Expr) : Lean.MetaM ℕ

How many call sites the statement contains, in the pre-order they are numbered by. A callee's own body is not searched: its calls belong to a later round.

structure GaudisCrypt.Flatten.CallData : Type

The pieces of a call: its signature, result l-value, the callee's parameter names (with their two proofs), body and return value, and the argument expression.

• sig : Expr

  The callee's signature.

• lvalue : Expr

  Where the result is stored.

• names : Expr

  The callee's parameter names.

• hlen : Expr

  names.length = sig.params.length.

• hnodup : Expr

  names.Nodup.

• body : Expr

  The callee's body.

• retVal : Expr

  The callee's return value.

• args : Expr

  The argument expression.

def GaudisCrypt.Flatten.reduceField (e : Expr) : Lean.MetaM Expr

A field of a structure literal, read off: (ProcedureWithHoles.mk … b …).body ↦ b. Anything else is returned unchanged; nothing is unfolded but the projection.

Equations

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

def GaudisCrypt.Flatten.callData? (e : Expr) : Lean.MetaM (Option CallData)

Read a call's pieces off the application. Both call forms are accepted; a call needs a callee that is a procedure written out.

Equations

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

def GaudisCrypt.Flatten.inStep {α : Type} (what : String) (k : Lean.MetaM α) : Lean.MetaM α

Annotate whatever goes wrong inside k with the step that was being built.

Equations

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

Names in use

The cleanup renaming gives the made-up names the names of the frame that are free. Which names are taken is read off the term, the literal variable names it mentions; a frame a statement reads opaquely (through a getter that is not a variable) is not seen, but the renaming is sound regardless, only the printed names could then be confusing.

partial def GaudisCrypt.Flatten.namesIn (e : Expr) (acc : Array String := #[]) : Array String

Every literal variable name of the frame e runs in (as VariableName.mk "x" … or localVarLens "x" …), and every let binder name, in first-occurrence order. The callees of calls run in frames of their own and are skipped.

def GaudisCrypt.Flatten.freshName (used : Array String) (base : String) : String

base, or base0, base1, … — the first one not in used.

Equations

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

def GaudisCrypt.Flatten.isMadeUp (n : String) : Bool

A name the flattening rounds made up: @.w for a callee's w, @@.w once a later round has escaped it, and so on. (Or a name a user wrote with a leading @, which the cleanup renames just as well.)

Equations

• GaudisCrypt.Flatten.isMadeUp n = n.startsWith "@"

def GaudisCrypt.Flatten.baseName (n : String) : String

The readable name a made-up name stands for: without its leading @s and .s.

Equations

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

Flattening one call

partial def GaudisCrypt.Flatten.mkParamWriter (emb : Expr) : List String → List Expr → Lean.MetaM (Expr × Expr)

The parameters' new variables as one l-value — Setter.throwaway for none, the variable for one, the Lens.pair tuple for more — with the proof that it writes the callee's parameter slots (IsParamWriter).

def GaudisCrypt.Flatten.mkParamWriter.lenProof (ns : List String) (ts : List Expr) : Lean.MetaM Expr

names.length = tys.length, for literal lists of the same length.

Equations

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

def GaudisCrypt.Flatten.mkParamWriter.slot (z : String) (T : Expr) : Lean.MetaM (Expr × Array Expr × Expr)

Parameter z : T after renaming, (varLens ⟨@.z, T⟩).intoLocal, together with the instance, key and key proof of the callee's own ⟨z, T⟩ and the proof that emb takes the one to the other.

Equations

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

partial def GaudisCrypt.Flatten.mkParamWriter.lensOf (emb : Expr) (zs : List String) (Ts : List Expr) : Lean.MetaM (Expr × Expr)

Two or more parameters as a lens (for the Lens.pair of the next level up).

structure GaudisCrypt.Flatten.CallPlan : Type

The replacement for one call, with its proof.

• trafo : Expr

  trafo.

• htg : Expr

  trafo.chain globalL = globalL.

• stmt : Expr

  The statement replacing the call.

• proof : Expr

  (call …).EquivInLens stmt trafo.

def GaudisCrypt.Flatten.planCall (hCtx : Expr) (cd : CallData) : Lean.MetaM CallPlan

Build the expansion and its correctness proof for one call site.

Equations

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

structure GaudisCrypt.Flatten.PathResult : Type

What the traversal returns: the rewritten statement, its proof, and the plan the call site produced (the lenses are only known once the call has been reached).

• stmt : Expr

  The rewritten statement.

• proof : Expr

  Its correctness proof.

• plan : CallPlan

  The plan built at the call site.

partial def GaudisCrypt.Flatten.rebuildPath (hCtx : Expr) (idx : ℕ) (stmt₀ : Expr) : Lean.MetaM PathResult

Rebuild the statement along the path to call idx, planning the call where it is found — inside whatever let binders enclose it, since the call may mention them. Everything off the path is re-targeted wholesale with applyLens, without being inspected.

def GaudisCrypt.Flatten.stmtType (stmt : Expr) : Lean.MetaM Expr

The statement's hole context, read off its type.

Equations

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

def GaudisCrypt.Flatten.mkEquivInLens (hCtx a b l : Expr) : Lean.MetaM Expr

a.EquivInLens b l.

Equations

• GaudisCrypt.Flatten.mkEquivInLens hCtx a b l = Lean.Meta.mkAppOptM `GaudisCrypt.StmtWithHoles.EquivInLens #[some hCtx, some a, some b, some l]

def GaudisCrypt.Flatten.flattenCall (n : ℕ) (stmt : Expr) : Lean.MetaM FlattenStep

Flatten call site n (pre-order), leaving the result deliberately uncleaned.

Equations

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

Cleaning

simp only with cleanLemmas, the name evaluation of cleanSimprocs and nothing else: no default simp set, and zeta := false / zetaDelta := false, so the user's lets survive. The only declaration unfolded is Lens.chainGetter, which has to go away for the eval lemmas to see the state they are composed with.

def GaudisCrypt.Flatten.cleanLemmas : List Lean.Name

The closed lemma list of the cleaning pass. Nothing outside this list ever rewrites the statement.

Equations

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

def GaudisCrypt.Flatten.cleanPreLemmas : List Lean.Name

The lemmas of the cleaning pass that have to apply before Lens.chainGetter is unfolded.

Equations

• GaudisCrypt.Flatten.cleanPreLemmas = [`GaudisCrypt.Lens.chainGetter_toGetter]

def GaudisCrypt.Flatten.cleanUnfold : List Lean.Name

The definitions the cleaning pass unfolds: Lens.chainGetter, and typeListToTuple, which the content type of the parameter writer is spelled with (Flatten.equivInLens_call) — a variable renamed in a later round would otherwise take that spelling for its type.

Equations

• GaudisCrypt.Flatten.cleanUnfold = [`GaudisCrypt.Lens.chainGetter, `GaudisCrypt.typeListToTuple]

def GaudisCrypt.Flatten.cleanSimprocs : List Lean.Name

The simprocs of the cleaning pass: evaluating the new names, renaming inside a tuple, and the reset regions.

Equations

• GaudisCrypt.Flatten.cleanSimprocs = [`GaudisCrypt.Flatten.reduceVarName, `GaudisCrypt.Flatten.reduceChainPair, `GaudisCrypt.Flatten.reduceNameSet]

def GaudisCrypt.Flatten.cleanContext : Lean.MetaM (Lean.Meta.Simp.Context × Lean.Meta.Simp.SimprocsArray)

The simp context and simprocs of the cleaning pass, and nothing else.

Equations

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

partial def GaudisCrypt.Flatten.cleanStmt (stmt : Expr) : Lean.MetaM Lean.Meta.Simp.Result

Push applyLens / weaken / chain* inwards as far as the terms allow, and evaluate the new variable names. Never fails; whatever does not match keeps its wrapper, which costs prettiness, never correctness.

The lets around the statement (a procedure's holes, the user's binders) are kept, and the statement under them is cleaned: simp with zeta := false would not go under them.

Composition and the fixed point

(flattenSeq, the sequence pass, is in Logic/TacticMisc.lean.)

def GaudisCrypt.Flatten.transportClean (input : Expr) (step : FlattenStep) : Lean.MetaM (Expr × Expr)

Clean step.stmt, and carry step.proof (about input) along: the cleaned statement, and the proof of input.EquivInLens ‹cleaned› step.trafo.

Equations

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

def GaudisCrypt.Flatten.flattenCallCleaned (n : ℕ) (stmt : Expr) : Lean.MetaM FlattenStep

flattenCall, then cleanStmt, then flattenSeq, with the proofs composed. The only step that can fail is the first.

Equations

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

structure GaudisCrypt.Flatten.FlatteningResultextends GaudisCrypt.Flatten.FlattenStep : Type

The result of the whole pass.

• stmt : Expr
• trafo : Expr
• proof : Expr
• hCtx : Expr
• count : ℕ

  How many calls were flattened; nonzero, or we threw.

def GaudisCrypt.Flatten.stepSomeCall (step : ℕ → Expr → Lean.MetaM FlattenStep) (stmt : Expr) : Lean.MetaM (Option FlattenStep × Lean.MessageData)

Run step on the first call site it succeeds on, or report why there is none.

Equations

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

def GaudisCrypt.Flatten.stepAllCalls (step : ℕ → Expr → Lean.MetaM FlattenStep) (stmt : Expr) (fuel : ℕ := 256) : Lean.MetaM FlatteningResult

Run step on call sites until it succeeds on none, composing the proofs and the lenses. Throws if it succeeds on nothing at all, or after fuel rounds.

Equations

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

The cleanup renaming

def GaudisCrypt.Flatten.renameNames (stmt : Expr) (avoid : Array String := #[]) : Lean.MetaM (Option FlattenStep)

Give the made-up names of stmt (isMadeUp) readable ones: baseName, or with 0, 1, … appended on a clash with a name the statement uses or one in avoid. One renaming of the whole statement, applyLens (rename ren), cleaned; sound for any choice of names, since rename ren is a permutation of the names. none if there is nothing to rename.

Equations

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

partial def GaudisCrypt.Flatten.renameNames.applyLensUnderLets (l htg stmt : Expr) : Lean.MetaM (Expr × Expr)

applyLens l under the lets a statement starts with (a procedure's holes, the user's binders), with its proof equivInLens_applyLens: cleaning does not go under an applyLens into a let.

def GaudisCrypt.Flatten.withRenaming (avoid : Array String) (step : FlattenStep) : Lean.MetaM FlattenStep

step, followed by the cleanup renaming (renameNames), proofs and lenses composed.

Equations

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

def GaudisCrypt.Flatten.flattenProcedureCalls (stmt : Expr) (avoid : Array String := #[]) : Lean.MetaM FlatteningResult

Flatten calls until none is left, then give the made-up names readable ones (avoiding avoid too). Throws if there was nothing to flatten at all; each round removes one call node, so the loop terminates.

Equations

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

The procedure wrapper

Run a pass on the body, give the made-up names readable ones (never the parameters' names), then re-target return_val along the composite lens, and prove with procedureDenotation_congr that the procedure computes the same: every renaming involved keeps the parameters' names, so the procedure's entry state is unchanged.

def GaudisCrypt.Flatten.fixesNamesProof (names f : Expr) : Lean.MetaM Expr

∀ n ∈ names, f n = n, by decide.

Equations

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

partial def GaudisCrypt.Flatten.fixesEntryProof (names tys hlen l : Expr) : Lean.MetaM Expr

FixesEntry names tys hlen l for a composite of trafo and rename ren: each keeps the parameters' names (checked by decide).

partial def GaudisCrypt.Flatten.keepsGlobalsProof (l : Expr) : Lean.MetaM Expr

l.chain globalL = globalL for a composite of trafo and rename ren, piece by piece. (Not by rfl: the unifier would compare the renamed locals on the way, and get lost evaluating the names of a variable it does not know.)

def GaudisCrypt.Flatten.inProcedure {α : Type} (p : Expr) (pass : Expr → Array String → Lean.MetaM (FlattenStep × α)) : Lean.MetaM (Expr × Expr × α)

Run a pass on the body of a hole-free procedure and put the procedure back together: the return_val re-targeted along the pass's lens and cleaned, and procedureDenotation_congr for the proof. Whatever else the pass reports (α) is passed on.

Equations

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

def GaudisCrypt.Flatten.flattenProcedure (p : Expr) : Lean.MetaM (Expr × Expr × ℕ)

Flatten the calls of a hole-free procedure. Returns the new procedure, a proof that it has the same procedureDenotation, and the number of calls flattened.

Equations

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

Inlining: unfolding a module expression to a procedure

A call site may name its callee through modules: call (Module.Proc.procedure (T.f (Module.app M A))) …. Flattening cannot handle that — it wants the callee spelled out at the call site — so this section provides the step before it: evaluate such a term to the procedure it denotes.

What it evaluates, and how far

The term is built from Module.app, the constants the module and moduletype commands emit, Module.pair/Module.fst/Module.snd, Module.proc and Module.Proc.procedure. Two shapes matter (ModuleSyntax.lean documents what each command declares):

• T.f stuff for a moduletype accessor T.f — the argument is evaluated only as far as the accessor needs: to a record, i.e. a T.mk or a Module.pair, and no further. What comes out is the field, which is then evaluated in turn;
• M.f stuff for a module-declared procedure M.f, which for a module with no module parameters is a straight substitution of the definition.

The steps are the generated lemmas, each applied at the head of the term and nowhere else: M.apply_simp (applying a module to its parameters, giving the record of its procedures), T.f.mk_simp (reading a field off that record), Module.fst_pair/snd_pair (the same for the anonymous record a module without a module type builds), M.f.apply_simp (applying a procedure of a module to the parameters it uses, giving Module.proc (M.f.procedure.instantiate ‹callees›)) and finally M.f.procedure.apply_simp (the body as written, with the hole calls turned back into calls of those callees). Nothing is rewritten inside the body: the callees it calls are left exactly as the module wrote them.

Everything is head-position, so there is no simp set here and no risk of a lemma firing somewhere unintended; what the pass cannot step is an error, not a silent stop. In particular, a module that is not concrete — T.f (Module.app M A) for a M that is a variable or an axiom — has no body to find, and unfoldProcedure fails.

And back into a statement

inlineProcedureRaw n rewrites call site n of a statement with unfoldProcedure, so that its callee becomes literal; inlineProcedure n does that and then flattens the site with flattenCallCleaned n — which is what "inlining" means here. Call sites are numbered by countCallSites, which counts call, call' and hole nodes: all three are calls as far as someone reading the statement is concerned, and numbering them together makes the numbers independent of which sites happen to be flattenable. A hole has no callee, so both functions fail on one.

def GaudisCrypt.Flatten.rewriteHead? (lem : Lean.Name) (e : Expr) : Lean.MetaM (Option (Expr × Expr))

One rewrite with a named equation, at the head of e and nowhere else: instantiate the lemma's binders with metavariables, unify its left-hand side with e, and hand back the instantiated right-hand side together with the instantiated lemma as its proof.

none if the lemma does not exist (the callers name lemmas that a module/moduletype declaration may have emitted), if it does not match, or if matching leaves anything open — whatever comes back is a closed term.

Equations

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

def GaudisCrypt.Flatten.setArg (e : Expr) (i : ℕ) (x : Expr) : Expr

Replace argument i of an application.

Equations

• GaudisCrypt.Flatten.setArg e i x = Lean.mkAppN (Lean.Expr.getAppFn e) ((Lean.Expr.getAppArgs e).set! i x)

def GaudisCrypt.Flatten.congrArgAt (e : Expr) (i : ℕ) (h : Expr) : Lean.MetaM Expr

congrArg at argument i of an application: from h : ‹arg i› = x to e = e[arg i := x].

Equations

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

def GaudisCrypt.Flatten.liftResultAt (e : Expr) (i : ℕ) (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Meta.Simp.Result

Lift a rewrite of argument i to the whole application.

Equations

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

partial def GaudisCrypt.Flatten.procCore (e : Expr) : Lean.MetaM Expr

Peel the let telescope off a procedure and look at what is underneath.

def GaudisCrypt.Flatten.isProcLiteral (e : Expr) : Lean.MetaM Bool

Is this a procedure written out — a ProcedureWithHoles.mk, possibly under the let telescope that binds its holes?

Equations

• GaudisCrypt.Flatten.isProcLiteral e = do let __do_lift ← GaudisCrypt.Flatten.procCore e pure (Lean.Expr.isAppOfArity __do_lift `GaudisCrypt.ProcedureWithHoles.mk 7)

def GaudisCrypt.Flatten.lookupComponent? (e : Expr) : Option Expr

‹literal tuple›.lookup ‹literal index›, computed. This is what the three HoleSigs.Instantiation.lookup_* lemmas say, and each of them is rfl, so the result is definitionally the term it replaces — no proof is needed for the step, only a re-typing of the proof that mentions it.

Equations

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

partial def GaudisCrypt.Flatten.lookupComponent?.go (tuple idx : Expr) : Option Expr

Walk the index, taking the tuple apart as it goes. A one-hole instantiation is its procedure rather than a pair, which is the tuple that is not a Prod.mk.

def GaudisCrypt.Flatten.reduceLookups (e : Expr) : Expr

Compute away every lookup of a literal instantiation.

Equations

• GaudisCrypt.Flatten.reduceLookups e = Lean.Expr.replace GaudisCrypt.Flatten.lookupComponent? e

def GaudisCrypt.Flatten.reduceStructProj (e : Expr) : Lean.MetaM Expr

Reduce a projection function applied to a record — the shape a mk_simp leaves behind (T.Structure.f {f := …, …}). Anything else is returned unchanged.

Equations

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

partial def GaudisCrypt.Flatten.spellOutProcedure (e : Expr) (fuel : ℕ := 32) : Lean.MetaM Lean.Meta.Simp.Result

Spell a procedure out: M.f.procedure.instantiate ‹callees› becomes the body as it was written — with each hole call turned back into a call of the callee it was made from — by the M.f.procedure.apply_simp lemma the module command emits; a procedure named by a constant is unfolded, its definition being the body. Fails when no body can be reached.

def GaudisCrypt.Flatten.moduleAppFn? (e : Expr) : Option ℕ

The function argument of a Module.app — the last argument is what it is applied to.

Equations

• GaudisCrypt.Flatten.moduleAppFn? e = if (Lean.Expr.isAppOf e `GaudisCrypt.Module.app && decide (Lean.Expr.getAppNumArgs e ≥ 2)) = true then some (Lean.Expr.getAppNumArgs e - 2) else none

partial def GaudisCrypt.Flatten.moduleAppHead (e : Expr) : Expr

The head of a Module.app spine: Module.app (… (Module.app h x₁) …) xₖ ↦ h.

def GaudisCrypt.Flatten.pairLemma? : Lean.Name → Option Lean.Name

The lemma that reads a projection off a Module.pair — the anonymous record a module without a module type builds.

Equations

• GaudisCrypt.Flatten.pairLemma? `GaudisCrypt.Module.fst = some `GaudisCrypt.Module.fst_pair
• GaudisCrypt.Flatten.pairLemma? `GaudisCrypt.Module.snd = some `GaudisCrypt.Module.snd_pair
• GaudisCrypt.Flatten.pairLemma? `GaudisCrypt.Module.fst' = some `GaudisCrypt.Module.fst_pair'
• GaudisCrypt.Flatten.pairLemma? `GaudisCrypt.Module.snd' = some `GaudisCrypt.Module.snd_pair'
• GaudisCrypt.Flatten.pairLemma? x✝ = none

def GaudisCrypt.Flatten.isAccessor (c : Lean.Name) : Lean.MetaM Bool

Is this constant an accessor of a moduletype declaration? It is exactly when the command emitted the mk_simp lemma that reads the field back off a built module.

Equations

• GaudisCrypt.Flatten.isAccessor c = do let __do_lift ← Lean.getEnv pure (__do_lift.contains (c ++ `mk_simp))

partial def GaudisCrypt.Flatten.moduleStep? (e : Expr) : Lean.MetaM (Option Lean.Meta.Simp.Result)

One step of head evaluation of a module expression: applying a module or one of its procedures to its parameters, reading a field off a record, or — when none of those applies yet — the same one step in the position that has to be evaluated first (the function of a Module.app, the module a projection is taken of).

partial def GaudisCrypt.Flatten.unfoldModuleExpr (e : Expr) (fuel : ℕ := 64) : Lean.MetaM Lean.Meta.Simp.Result

Evaluate a module expression until its head is Module.proc, then spell that procedure out. Fails as soon as no step applies — which is exactly the case where the term has no concrete procedure body.

def GaudisCrypt.Flatten.unfoldProcedureCore (e : Expr) : Lean.MetaM Lean.Meta.Simp.Result

Unfold a term built from modules that evaluates to a procedure, and hand back the result with a proof that it equals the term.

Accepts both levels: a module term of type Module.Proc sig, whose result is Module.proc ‹procedure›, and a procedure term — Module.Proc.procedure ‹module›, the shape a call site carries — whose result is the procedure itself. Fails if no concrete body can be found.

This is the pass itself; unfoldProcedure wraps it.

Equations

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

def GaudisCrypt.Flatten.unfoldProcedure (e : Expr) : Lean.MetaM Lean.Meta.Simp.Result

unfoldProcedureCore, with the proof re-typed to say what it proves.

A step that unfolds a definition carries no proof of its own — none is rfl — so what the composed proof states can end at a term that is only definitionally the result. Both are correct; this is the one a caller (and a #check) would rather read.

Equations

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

partial def GaudisCrypt.Flatten.rewriteCalleeAt (idx : ℕ) (e₀ : Expr) : Lean.MetaM Lean.Meta.Simp.Result

Rewrite call site idx of a statement by unfolding its callee, and prove that the result equals the statement. The traversal is the one that numbers the call sites, with the single difference that it stops at a StmtWithHoles.call (openStmt): whnf would step through it to the call' it is defined as, which spreads the callee over several arguments instead of one.

def GaudisCrypt.Flatten.inlineProcedureRaw (n : ℕ) (stmt : Expr) : Lean.MetaM Lean.Meta.Simp.Result

Unfold the callee of call site n, leaving the call itself alone. The proof is an equation: the statement is rewritten, not re-targeted.

Equations

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

def GaudisCrypt.Flatten.inlineCall (n : ℕ) (stmt : Expr) : Lean.MetaM FlattenStep

Inline call site n, leaving the callee's variables with made-up names: unfold its callee (inlineProcedureRaw), then flatten the call (flattenCallCleaned). The two proofs compose: the first is an equation, which transports the second's EquivInLens back to the statement it started from.

Equations

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

def GaudisCrypt.Flatten.inlineProcedure (n : ℕ) (stmt : Expr) (avoid : Array String := #[]) : Lean.MetaM FlattenStep

Inline call site n (inlineCall), then give the made-up names readable ones (avoiding avoid too).

Equations

• GaudisCrypt.Flatten.inlineProcedure n stmt avoid = do let __do_lift ← GaudisCrypt.Flatten.inlineCall n stmt GaudisCrypt.Flatten.withRenaming avoid __do_lift

def GaudisCrypt.Flatten.inlineInProcedure (n : ℕ) (p : Expr) : Lean.MetaM (Expr × Expr)

inlineProcedure at the procedure level: inline call site n of the body of a hole-free procedure that is spelled out, and hand back the new procedure together with a proof that it has the same procedureDenotation.

proc (…) { xxx; call bla; yyy } becomes proc (…) { xxx; ‹the body of bla›; yyy }, with the callee's variables added to the procedure's own (renamed where they collide) and its result stored where the call stored it.

Equations

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

Hoare triples

A triple can be proved about the flattened statement instead, along hoareStmt_of_equivInLens (Logic/StmtEquiv.lean).

def GaudisCrypt.Flatten.cleanCondition (C l : Expr) : Lean.MetaM (Expr × Expr)

fun τ => C (l.get τ), cleaned like a statement, with the equation.

Equations

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

def GaudisCrypt.Flatten.hoareInline (n : ℕ) (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

On a goal hoareStmt A s B: inline call site n of s (inlineProcedure) and continue with the triple about the result, its conditions read through the renaming and cleaned. The names the conditions use count as taken.

Equations

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

def GaudisCrypt.Flatten.tacticHoare_inline_ : Lean.ParserDescr

hoare_inline n: on a goal hoareStmt A s B, inline call site n of s (numbered in pre-order, holes included; the callee spelled out, named by a definition or through modules), and continue with the triple about the result. The callee's own calls stay calls.

Equations

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