Variables

The memory model of programs and procedures:

• VariableName — a program variable's name together with its type (see below).
• VariableAssignment — a value for every VariableName, with VariableAssignment.init as the initial (unspecified) assignment, and varLens v onto the slot of v. Two varLens are disjoint by instance search when the names are literals that differ.
• ProgramState — the globals and the locals of the running procedure, both a VariableAssignment, with globalL/localL and Lens.intoGlobal/Lens.intoLocal.
• VariableAssignment.setParams — write an argument tuple into the parameter slots.
• VariableAssignment.embed/rename — view an assignment through an injective name map (types are kept, so no casts), used for flattening.
• global_var x : T — declares the global variable x, the slot of ⟨"N.x", T⟩ in the globals (N.x the full declaration name), disjoint from all other globals by instance search (Lens.IsGlobalVar).

Variable names

A VariableName is a program variable's name together with its type. Besides the name it carries a natural-number key, the name's encoding VariableName.encode name, stored as a literal. The key exists for instance search: two names with different literal keys are told apart by VariableName.NameNe in a single unification step, whatever their length, which is what lets disjointness of two variables be found automatically. (Instance search cannot compare strings in one step: a string literal is opened into a list of characters, and every character then costs a step and a level of recursion. Nat literals are the one kind of data the unifier has built-in arithmetic for.)

key and its correctness proof keyCorrect are filled in automatically: key is an implicit argument of the constructor, and the variable_name_key tactic behind keyCorrect evaluates encode name when name is a string literal and assigns key the resulting literal. So one writes ⟨"x", Int⟩ or { name := "x", type := Int } and gets @VariableName.mk "x" Int 121 ⋯.

Argument tuples

Defined here rather than in Programs.lean, which builds on this file.

@[reducible]

def GaudisCrypt.typeListToTuple : List Type → Type

Reducible on purpose: at a concrete parameter list the tuple type has to be visible to unification at reducible transparency, or everything stated about _ × _ gets stuck on it — typeclass resolution (OfNat (typeListToTuple [Nat]) 5 for a numeral argument of a call, Lens.Disjoint of two projection lenses) is where it shows.

Equations

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

Variable names

def GaudisCrypt.VariableName.encodeChars : List Char → ℕ

Bijective base-0x110000 numeration of a character list, least significant digit first: character c is the digit c.toNat + 1 (in 1 … 0x110000, since a code point is below 0x110000), and the empty list is 0. Reduces by rfl in the kernel on literals (the corresponding encoding of the UTF-8 bytes does not: String.toUTF8 gets stuck).

Equations

• GaudisCrypt.VariableName.encodeChars [] = 0
• GaudisCrypt.VariableName.encodeChars (c :: cs) = c.toNat + 1 + 1114112 * GaudisCrypt.VariableName.encodeChars cs

def GaudisCrypt.VariableName.encode (s : String) : ℕ

The key of a variable name: an injective, computable encoding of strings as naturals (encode_injective). Quadratic in the length of the string — each step multiplies the accumulated number, about 21 bits per character, by a constant — which is microseconds at any plausible name length. (An O(n log n) version is possible: with base 2 ^ 21, merge neighbouring blocks with a ||| (b <<< w) in log n passes, each pass recursing on the list and the passes on a counter. Both recursions are structural, so it still reduces by rfl, which variable_name_key relies on. Splitting at the midpoint instead would need well-founded recursion, which does not reduce.)

Equations

• GaudisCrypt.VariableName.encode s = GaudisCrypt.VariableName.encodeChars s.toList

theorem GaudisCrypt.VariableName.encodeChars_injective : Function.Injective encodeChars

theorem GaudisCrypt.VariableName.encode_injective : Function.Injective encode

def GaudisCrypt.tacticVariable_name_key : Lean.ParserDescr

Close ?key = VariableName.encode name. If name is a string literal, compute the encoding and assign ?key the resulting Nat literal, so that instance search can compare keys. Otherwise ?key becomes VariableName.encode name itself: the name is still a valid variable name, but VariableName.NameNe will not be found for it by instance search.

Equations

• GaudisCrypt.tacticVariable_name_key = Lean.ParserDescr.node `GaudisCrypt.tacticVariable_name_key 1024 (Lean.ParserDescr.nonReservedSymbol "variable_name_key" false)

def GaudisCrypt.VariableName.reduceEncode : Lean.Meta.Simp.DSimproc

VariableName.encode "x" ↦ the literal variable_name_key assigns for "x". A slot built from a name that is a variable (as in setParams) carries the key encode n, and once n is instantiated to "x" it is still encode "x", while the slot localVarLens "x" T written in a program carries the literal. The two are defeq but not syntactically equal, so without this simp treats them as different slots (Function.update_self does not fire). The rewrite is by rfl: encode reduces on literals. A dsimproc, not a simproc: the key is an argument other arguments depend on (keyCorrect, and the value written in a Function.update), and simp rewrites such positions only with definitional steps.

Equations

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

structure GaudisCrypt.VariableName : Type 1

A program variable's name and type. key is encode name as a literal and is filled in automatically, together with its proof (see the module docstring). Two VariableNames are equal iff their names and types are (nonempty is a proposition, and key/keyCorrect are determined by the name).

The type has to be nonempty, so that an assignment of values to all variable names exists at all (VariableAssignment.init). The instance is found by instance search.

• name : String
• type : Type
• nonempty : Nonempty self.type
• key : ℕ
• keyCorrect : self.key = encode self.name

def GaudisCrypt.VariableName.mkTerm (n : String) (T : Lean.Expr) (ne? : Option Lean.Expr := none) : Lean.MetaM Lean.Expr

The variable name n : T as a term, the way localVarLens "n" T elaborates it: the Nonempty T instance synthesized (unless given), the key the literal variable_name_key computes. For meta code that makes up variables (hoare_proc_to_stmt, flattening).

Equations

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

class GaudisCrypt.NatLt (a b : ℕ) : Prop

a < b, for natural-number literals, found by instance search in one step: unifying ?k + a + 1 =?= b is solved by the unifier's literal-offset rule as ?k := b - a - 1, at any size of the literals. (The unknown has to be the leftmost summand for that rule to apply.)

• lt : a < b

instance GaudisCrypt.instNatLtHAddNatOfNat (a k : ℕ) : NatLt a (k + a + 1)

class GaudisCrypt.NatNe (a b : ℕ) : Prop

a ≠ b, for natural-number literals, found by instance search via NatLt.

• ne : a ≠ b

instance GaudisCrypt.instNatNeOfNatLt (a b : ℕ) [h : NatLt a b] : NatNe a b

instance GaudisCrypt.instNatNeOfNatLt_1 (a b : ℕ) [h : NatLt b a] : NatNe a b

class GaudisCrypt.VariableName.NameNe (v w : VariableName) : Prop

Two variable names whose names differ. Found by instance search from the literal keys, for names given as constructor applications (as ⟨"x", Int⟩ elaborates); since encode is injective, it is found exactly when the names differ.

• ne : v.name ≠ w.name

instance GaudisCrypt.instNameNeMkOfNatNe (n₁ n₂ : String) (T₁ T₂ : Type) (i₁ : Nonempty T₁) (i₂ : Nonempty T₂) (k₁ k₂ : ℕ) (h₁ : k₁ = VariableName.encode n₁) (h₂ : k₂ = VariableName.encode n₂) [h : NatNe k₁ k₂] : { name := n₁, type := T₁, nonempty := i₁, key := k₁, keyCorrect := h₁ }.NameNe { name := n₂, type := T₂, nonempty := i₂, key := k₂, keyCorrect := h₂ }

theorem GaudisCrypt.VariableName.ne_of_nameNe {v w : VariableName} [h : v.NameNe w] : v ≠ w

theorem GaudisCrypt.VariableName.ext' {v w : VariableName} (hn : v.name = w.name) (ht : v.type = w.type) : v = w

A variable name is determined by its name and type.

def GaudisCrypt.VariableName.withName (v : VariableName) (n : String) : VariableName

The variable name n : v.type: v with its name replaced (and the key recomputed, as a non-literal encode n). (v.withName n).type is v.type by definition, which is what lets embed move values between slots without casts.

Equations

• v.withName n = { name := n, type := v.type, nonempty := ⋯, key := GaudisCrypt.VariableName.encode n, keyCorrect := ⋯ }

@[simp]

theorem GaudisCrypt.VariableName.withName_name (v : VariableName) (n : String) : (v.withName n).name = n

@[simp]

theorem GaudisCrypt.VariableName.withName_withName (v : VariableName) (a b : String) : (v.withName a).withName b = v.withName b

theorem GaudisCrypt.VariableName.withName_self (v : VariableName) : v.withName v.name = v

Variable assignments

@[reducible, inline]

abbrev GaudisCrypt.VariableAssignment : Type 1

A value for every variable name. Inhabited (init) because every VariableName has a nonempty type. Reducible, so that m v typechecks at every transparency (rewriting needs this).

Equations

• GaudisCrypt.VariableAssignment = ((v : GaudisCrypt.VariableName) → v.type)

noncomputable def GaudisCrypt.VariableAssignment.init : VariableAssignment

The initial assignment: an unspecified value in every slot.

Equations

• GaudisCrypt.VariableAssignment.init v = Classical.choice ⋯

@[implicit_reducible]

noncomputable instance GaudisCrypt.instInhabitedVariableAssignment : Inhabited VariableAssignment

Equations

• GaudisCrypt.instInhabitedVariableAssignment = { default := GaudisCrypt.VariableAssignment.init }

theorem GaudisCrypt.VariableAssignment.apply_withName (m : VariableAssignment) (v : VariableName) {n : String} (h : n = v.name) : m (v.withName n) = m v

Reading a slot under a renamed variable name, when the new name is the old one.

theorem GaudisCrypt.VariableAssignment.apply_withName_congr (m : VariableAssignment) (v : VariableName) {a b : String} (h : a = b) : m (v.withName a) = m (v.withName b)

noncomputable def GaudisCrypt.varLens (v : VariableName) : Lens v.type VariableAssignment

The lens onto the slot of variable v. Writing uses Function.update, with classical decidable equality of variable names (their types are arbitrary, so there is no other).

Equations

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

@[simp]

theorem GaudisCrypt.varLens_get (v : VariableName) (m : VariableAssignment) : (varLens v).get m = m v

theorem GaudisCrypt.varLens_set (v : VariableName) (x : v.type) (m : VariableAssignment) : (varLens v).set x m = Function.update m v x

theorem GaudisCrypt.varLens_disjoint {v w : VariableName} (h : v ≠ w) : (varLens v).Disjoint (varLens w)

Slots of different variable names are disjoint.

instance GaudisCrypt.varLens.instDisjoint (n₁ n₂ : String) (T₁ T₂ : Type) (i₁ : Nonempty T₁) (i₂ : Nonempty T₂) (k₁ k₂ : ℕ) (h₁ : k₁ = VariableName.encode n₁) (h₂ : k₂ = VariableName.encode n₂) [{ name := n₁, type := T₁, nonempty := i₁, key := k₁, keyCorrect := h₁ }.NameNe { name := n₂, type := T₂, nonempty := i₂, key := k₂, keyCorrect := h₂ }] : (varLens { name := n₁, type := T₁, nonempty := i₁, key := k₁, keyCorrect := h₁ }).Disjoint (varLens { name := n₂, type := T₂, nonempty := i₂, key := k₂, keyCorrect := h₂ })

Slots of differently named variables are disjoint, found by instance search when both names are literals (VariableName.NameNe). Stated for constructor applications: for a variable v, the slot type v.type is a projection the instance index cannot match against a concrete type, while (VariableName.mk n T).type reduces to T.

Writing arguments into parameter slots

noncomputable def GaudisCrypt.VariableAssignment.setParams (names : List String) (tys : List Type) : names.length = tys.length → typeListToTuple tys → VariableAssignment → VariableAssignment

Write an argument tuple typeListToTuple tys into the slots names.zip tys, first parameter first (so on a duplicate name the later parameter wins). The Nonempty instance each slot's VariableName needs comes from the argument itself. Lists of different lengths (excluded by the length hypothesis) leave the assignment unchanged.

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.VariableAssignment.setParams [] [] x_5 x_6 x✝ = x✝
• GaudisCrypt.VariableAssignment.setParams x✝⁴ x✝³ x✝² x✝¹ x✝ = x✝

theorem GaudisCrypt.VariableAssignment.setParams_apply_of_notMem (names : List String) (tys : List Type) (h : names.length = tys.length) (args : typeListToTuple tys) (m : VariableAssignment) (v : VariableName) : v.name ∉ names → setParams names tys h args m v = m v

setParams leaves every slot outside the parameter names alone.

Renaming

noncomputable def GaudisCrypt.VariableAssignment.embed (ι : String → String) (hι : Function.Injective ι) : Lens VariableAssignment VariableAssignment

View an assignment through an injective name map ι: slot n : T of the view is slot ι n : T of the assignment. Writing a view back overwrites exactly the slots in the range of ι. Types are kept, so no casts are needed.

Equations

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

theorem GaudisCrypt.VariableAssignment.embed_chain_varLens (ι : String → String) (hι : Function.Injective ι) (v : VariableName) : (embed ι hι).chain (varLens v) = varLens (v.withName (ι v.name))

Cleaning lemma: a slot seen through embed ι is the slot of the renamed variable.

noncomputable def GaudisCrypt.VariableAssignment.rename (π : Equiv.Perm String) : VariableAssignment ≃ VariableAssignment

Renaming along a permutation of names: an isomorphism of assignments, slot n : T of rename π m being slot π n : T of m.

Equations

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

theorem GaudisCrypt.VariableAssignment.embed_perm (π : Equiv.Perm String) : embed ⇑π ⋯ = Lens.bijection (rename π).symm

embed along a permutation is the isomorphism lens of rename.

Program states

structure GaudisCrypt.ProgramState : Type 1

The state a statement runs in: the program's globals and the running procedure's locals. Both are variable assignments, the globals named by full declaration names (see global_var).

• globals : VariableAssignment
• locals : VariableAssignment

def GaudisCrypt.ProgramState.globalL : Lens VariableAssignment ProgramState

Lens onto the globals of a ProgramState.

Equations

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

def GaudisCrypt.ProgramState.localL : Lens VariableAssignment ProgramState

Lens onto the locals of a ProgramState.

Equations

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

instance GaudisCrypt.ProgramState.disjoint_globalL_localL : globalL.Disjoint localL

instance GaudisCrypt.ProgramState.disjoint_localL_globalL : localL.Disjoint globalL

def GaudisCrypt.Lens.intoLocal {a : Type u_1} (x : Lens a VariableAssignment) : Lens a ProgramState

A lens into the locals, as a lens into the program state.

Equations

• x.intoLocal = GaudisCrypt.ProgramState.localL.chain x

def GaudisCrypt.Lens.intoGlobal {a : Type u_1} (x : Lens a VariableAssignment) : Lens a ProgramState

A lens into the globals, as a lens into the program state.

Equations

• x.intoGlobal = GaudisCrypt.ProgramState.globalL.chain x

@[reducible, inline]

noncomputable abbrev GaudisCrypt.localVarLens (n : String) (T : Type) [Nonempty T] {key : ℕ} (keyCorrect : key = VariableName.encode n := by variable_name_key) : Lens T ProgramState

The local variable n : T: its slot in the locals, as a lens into the program state. This is what a parameter or var of a proc stands for. The key of the variable name is filled in at the use site by variable_name_key, so for a literal n it is a literal, and two local variables with different literal names are found disjoint by instance search (through Lens.disjoint_intoLocal and varLens.instDisjoint; an abbrev, so that instance search sees the slot).

Equations

• GaudisCrypt.localVarLens n T keyCorrect = (GaudisCrypt.varLens { name := n, type := T, nonempty := inst✝, key := key, keyCorrect := keyCorrect }).intoLocal

instance GaudisCrypt.Lens.disjoint_intoLocal_intoGlobal {a : Type u_1} {b : Type u_2} (x : Lens a VariableAssignment) (y : Lens b VariableAssignment) : x.intoLocal.Disjoint y.intoGlobal

instance GaudisCrypt.Lens.disjoint_intoGlobal_intoLocal {a : Type u_1} {b : Type u_2} (x : Lens a VariableAssignment) (y : Lens b VariableAssignment) : x.intoGlobal.Disjoint y.intoLocal

instance GaudisCrypt.Lens.disjoint_intoLocal {a : Type u_1} {b : Type u_2} (x : Lens a VariableAssignment) (y : Lens b VariableAssignment) [x.Disjoint y] : x.intoLocal.Disjoint y.intoLocal

instance GaudisCrypt.Lens.disjoint_intoGlobal {a : Type u_1} {b : Type u_2} (x : Lens a VariableAssignment) (y : Lens b VariableAssignment) [x.Disjoint y] : x.intoGlobal.Disjoint y.intoGlobal

Global variables

global_var x : T declares the global variable x: the slot of the variable name ⟨"N.x", T⟩ in the globals, where N.x is the full name of the declaration, so two globals declared in different places never share a slot. It is a plain def (simp does not see through it), and Lens.IsGlobalVar records which slot it is, which is what instance search uses to find two globals disjoint (Lens.IsGlobalVar.instDisjoint).

class GaudisCrypt.Lens.IsGlobalVar {T : Type} (x : Lens T VariableAssignment) (v : outParam VariableName) : Prop

x is the slot of the variable name v (as the instance global_var emits says). v is an outParam, found from x.

• type_eq : v.type = T
• heq : x ≍ varLens v

theorem GaudisCrypt.Lens.IsGlobalVar.disjoint {T U : Type} {x : Lens T VariableAssignment} {y : Lens U VariableAssignment} {v w : VariableName} (hx : x.IsGlobalVar v) (hy : y.IsGlobalVar w) (h : v ≠ w) : x.Disjoint y

Two slots of differently named variables are disjoint.

instance GaudisCrypt.Lens.IsGlobalVar.instDisjoint {T U : Type} (x : Lens T VariableAssignment) (y : Lens U VariableAssignment) {v w : VariableName} [hx : x.IsGlobalVar v] [hy : y.IsGlobalVar w] [v.NameNe w] : x.Disjoint y

Globals with different (literal) names are disjoint.

def GaudisCrypt.«command_Global_var_:_» : Lean.ParserDescr

global_var x : T declares the global variable x : Lens T VariableAssignment, the slot of ⟨"N.x", T⟩ with N.x the full name of the declaration (T must be nonempty), together with its Lens.IsGlobalVar instance, so that globals are found disjoint by instance search.

Equations

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