structure GaudisCrypt.Getter (a : Type u) (b : Type v) : Type (max u v)

A read-only projection. Forgetting the setter of a Lens gives a Getter.

• get : b → a

theorem GaudisCrypt.Getter.ext_iff {a : Type u} {b : Type v} {x y : Getter a b} : x = y ↔ x.get = y.get

theorem GaudisCrypt.Getter.ext {a : Type u} {b : Type v} {x y : Getter a b} (get : x.get = y.get) : x = y

structure GaudisCrypt.Setter (a : Type u) (b : Type v) : Type (max u v)

A write-only updater (a lawful setter): the only law is overwrite-collapse (set_set). Forgetting the getter of a Lens gives a Setter. Unlike a Lens, a Setter need not be invertible — e.g. Setter.throwaway discards its writes.

• set : a → b → b
• set_set (s : b) (x y : a) : self.set y (self.set x s) = self.set y s

theorem GaudisCrypt.Setter.ext_iff {a : Type u} {b : Type v} {x y : Setter a b} : x = y ↔ x.set = y.set

theorem GaudisCrypt.Setter.ext {a : Type u} {b : Type v} {x y : Setter a b} (set : x.set = y.set) : x = y

structure GaudisCrypt.Lens (a : Type u) (b : Type v) extends GaudisCrypt.Getter a b, GaudisCrypt.Setter a b : Type (max u v)

• get : b → a
• set : a → b → b
• set_set (s : b) (x y : a) : self.set y (self.set x s) = self.set y s
• set_get (s : b) (x : a) : self.get (self.set x s) = x
• get_set (s : b) : self.set (self.get s) s = s

@[implicit_reducible]

instance GaudisCrypt.instCoeLensGetter {a : Type u_1} {b : Type u_2} : Coe (Lens a b) (Getter a b)

A Lens forgets to its Getter / Setter. (extends does not generate these coercions automatically, but code that passes a lens where a getter/setter is expected — e.g. ProgramDenotation.get/ProgramDenotation.set — relies on them.)

Equations

• GaudisCrypt.instCoeLensGetter = { coe := GaudisCrypt.Lens.toGetter }

@[implicit_reducible]

instance GaudisCrypt.instCoeLensSetter {a : Type u_1} {b : Type u_2} : Coe (Lens a b) (Setter a b)

Equations

• GaudisCrypt.instCoeLensSetter = { coe := GaudisCrypt.Lens.toSetter }

noncomputable def GaudisCrypt.Lens.get_from_set {a : Type u_1} {m : Type u_2} [ne : Nonempty a] (set : a → m → m) : m → a

Equations

• GaudisCrypt.Lens.get_from_set set mem = if h : ∃ (x : a), set x mem = mem then Classical.choose h else Classical.choice ne

def GaudisCrypt.Lens.get_from_set_correct {a : Type u_1} {m : Type u_2} [Nonempty a] (lens : Lens a m) : get_from_set lens.set = lens.get

Equations

• ⋯ = ⋯

theorem GaudisCrypt.Lens.ext {a : Type u_1} {m : Type u_2} (l r : Lens a m) (h : ∀ (x : a) (y : m), l.set x y = r.set x y) : l = r

theorem GaudisCrypt.Lens.ext_iff {a : Type u_1} {m : Type u_2} {l r : Lens a m} : l = r ↔ ∀ (x : a) (y : m), l.set x y = r.set x y

class GaudisCrypt.disjoint {a : Type u_1} {m : Type u_2} {b : Type u_3} (x : Lens a m) (y : Lens b m) : Prop

Lenses x and y are disjoint, i.e., refer to different parts of the memory

• commute (s : m) (v : a) (w : b) : x.set v (y.set w s) = y.set w (x.set v s)

theorem GaudisCrypt.disjoint.iff {a✝ : Type u_1} {b✝ : Type u_2} {x : Lens a✝ b✝} {a✝¹ : Type u_3} {y : Lens a✝¹ b✝} : disjoint x y ↔ ∀ (s : b✝) (v : a✝) (w : a✝¹), x.set v (y.set w s) = y.set w (x.set v s)

theorem GaudisCrypt.disjoint.symm {a b m : Type} {x : Lens a m} {y : Lens b m} (h : disjoint x y) : disjoint y x

Disjointness is symmetric. Not an instance (would loop).

theorem GaudisCrypt.Lens.get_of_disjoint_set {a b m : Type} (L : Lens a m) (M : Lens b m) [hd : disjoint M L] (v : b) (s : m) : L.get (M.set v s) = L.get s

Setting through a disjoint lens leaves the other lens's get unchanged. Disjointness is recorded as disjoint M L (setter then reader).

def GaudisCrypt.Lens.pair {a : Type u_1} {m : Type u_2} {b : Type u_3} (x : Lens a m) (y : Lens b m) [disj : disjoint x y] : Lens (a × b) m

Equations

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

def GaudisCrypt.Lens.chain {a : Type u_1} {b : Type u_2} {c : Type u_3} (x : Lens b c) (y : Lens a b) : Lens a c

Equations

• x.chain y = { get := fun (s : c) => y.get (x.get s), set := fun (a_1 : a) (s : c) => x.set (y.set a_1 (x.get s)) s, set_set := ⋯, set_get := ⋯, get_set := ⋯ }

def GaudisCrypt.Lens.fst {a : Type u_1} {b : Type u_2} : Lens a (a × b)

Equations

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

def GaudisCrypt.Lens.snd {b : Type u_1} {a : Type u_2} : Lens b (a × b)

Equations

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

def GaudisCrypt.Lens.ofst {a : Type u_1} {m : Type u_2} {m' : Type u_3} (lens : Lens a m) : Lens a (m × m')

Equations

• lens.ofst = GaudisCrypt.Lens.fst.chain lens

def GaudisCrypt.Lens.osnd {a : Type u_1} {m : Type u_2} {m' : Type u_3} (lens : Lens a m) : Lens a (m' × m)

Equations

• lens.osnd = GaudisCrypt.Lens.snd.chain lens

def GaudisCrypt.Setter.ofst {a : Type u_1} {m : Type u_2} {m' : Type u_3} (s : Setter a m) : Setter a (m × m')

Lift a setter into the first component of a product (no get needed, unlike Lens.ofst, which is why a bare Setter can be lifted).

Equations

• s.ofst = { set := fun (v : a) (p : m × m') => (s.set v p.1, p.2), set_set := ⋯ }

def GaudisCrypt.Setter.osnd {a : Type u_1} {m : Type u_2} {m' : Type u_3} (s : Setter a m) : Setter a (m' × m)

Equations

• s.osnd = { set := fun (v : a) (p : m' × m) => (p.1, s.set v p.2), set_set := ⋯ }

def GaudisCrypt.Setter.throwaway {a : Type u_1} {m : Type u_2} : Setter a m

A setter that discards its writes.

Equations

• GaudisCrypt.Setter.throwaway = { set := fun (x : a) (s : m) => s, set_set := ⋯ }

theorem GaudisCrypt.pair_fst {a : Type u_1} {m : Type u_2} {b : Type u_3} (x : Lens a m) (y : Lens b m) [disj : disjoint x y] : (x.pair y).chain Lens.fst = x

theorem GaudisCrypt.pair_snd {a : Type u_1} {m : Type u_2} {b : Type u_3} (x : Lens a m) (y : Lens b m) [disj : disjoint x y] : (x.pair y).chain Lens.snd = y

instance GaudisCrypt.disjoint3 {a✝ : Type u_1} {b✝ : Type u_2} {x : Lens a✝ b✝} {a✝¹ : Type u_3} {y : Lens a✝¹ b✝} {a✝² : Type u_4} {z : Lens a✝² b✝} [xy : disjoint x y] [xz : disjoint x z] [yz : disjoint y z] : disjoint x (y.pair z)

instance GaudisCrypt.disjoint3' {a✝ : Type u_1} {b✝ : Type u_2} {x : Lens a✝ b✝} {a✝¹ : Type u_3} {y : Lens a✝¹ b✝} {a✝² : Type u_4} {z : Lens a✝² b✝} [xy : disjoint x y] [xz : disjoint x z] [yz : disjoint y z] : disjoint (x.pair y) z

instance GaudisCrypt.Lens.disjoint_ofst_osnd {a : Type u_1} {b : Type u_2} {m : Type u_3} {m' : Type u_4} (x : Lens a m) (y : Lens b m') : disjoint x.ofst y.osnd

instance GaudisCrypt.Lens.disjoint_osnd_ofst {a : Type u_1} {b : Type u_2} {m : Type u_3} {m' : Type u_4} (x : Lens a m') (y : Lens b m) : disjoint x.osnd y.ofst

instance GaudisCrypt.Lens.disjoint_chain {a₁ : Type u_1} {a₂ : Type u_2} {b : Type u_3} {c : Type u_4} (L : Lens b c) (x : Lens a₁ b) (y : Lens a₂ b) [d : disjoint x y] : disjoint (L.chain x) (L.chain y)

instance GaudisCrypt.Lens.disjoint_ofst_ofst {a : Type u_1} {b : Type u_2} {m : Type u_3} {m' : Type u_4} (x : Lens a m) (y : Lens b m) [disjoint x y] : disjoint x.ofst y.ofst

instance GaudisCrypt.Lens.disjoint_osnd_osnd {a : Type u_1} {b : Type u_2} {m : Type u_3} {m' : Type u_4} (x : Lens a m) (y : Lens b m) [disjoint x y] : disjoint x.osnd y.osnd

def GaudisCrypt.Lens.id {m : Type u_1} : Lens m m

Equations

• GaudisCrypt.Lens.id = { get := fun (m : m) => m, set := fun (a x : m) => a, set_set := ⋯, set_get := ⋯, get_set := ⋯ }

def GaudisCrypt.Lens.punit {s : Type u_1} {t : Type u_2} [Unique t] : Lens t s

The trivial lens onto a subsingleton-with-default content type: reads nothing, writes nothing. Its footprint is ⊥.

Equations

• GaudisCrypt.Lens.punit = { get := fun (x : s) => default, set := fun (x : t) (σ : s) => σ, set_set := ⋯, set_get := ⋯, get_set := ⋯ }

def GaudisCrypt.Lens.bijection {a : Type u_1} {b : Type u_2} (e : a ≃ b) : Lens a b

Equations

• GaudisCrypt.Lens.bijection e = { get := ⇑e.symm, set := fun (x : a) (x_1 : b) => e x, set_set := ⋯, set_get := ⋯, get_set := ⋯ }

theorem GaudisCrypt.Lens.bijection_chain {a b c : Type} (e : a ≃ b) (f : b ≃ c) : (bijection f).chain (bijection e) = bijection (e.trans f)

@[simp]

theorem GaudisCrypt.Lens.bijection_refl {a : Type} : bijection (Equiv.refl a) = id

structure GaudisCrypt.LensIn (m : Type u) : Type (max u (v + 1))

• content : Type v
• lens : Lens self.content m

def GaudisCrypt.LensIn.mk' {a : Type u_1} {m : Type u_2} (lens : Lens a m) : LensIn m

Equations

• GaudisCrypt.LensIn.mk' lens = { content := a, lens := lens }

def GaudisCrypt.IsoLens {a : Type u_1} {b : Type u_2} (lens : Lens a b) : Prop

Equations

• GaudisCrypt.IsoLens lens = Function.Bijective lens.get

@[implicit_reducible]

instance GaudisCrypt.instPreorderLensIn {m : Type u_1} : Preorder (LensIn m)

Equations

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

@[reducible, inline]

abbrev GaudisCrypt.bit : Type

Equations

• GaudisCrypt.bit = ZMod 2

def GaudisCrypt.Lens.liftFunction {a : Type u_1} {m : Type u_2} (lens : Lens a m) (f : Function.End a) : Function.End m

Equations

• lens.liftFunction f x = lens.set (f (lens.get x)) x

def GaudisCrypt.Lens.equal_outside {a : Type u_1} {m : Type u_2} (lens : Lens a m) (s s' : m) : Prop

s ~ s' iff they differ only in the part the lens controls: ∃ a, lens.set a s = s'.

Equations

• lens.equal_outside s s' = ∃ (x : a), lens.set x s = s'

def GaudisCrypt.Lens.equal_outside_setoid {a : Type u_1} {m : Type u_2} (lens : Lens a m) : Setoid m

The relation equal_outside is an equivalence.

• refl: set (get s) s = s (by get_set)
• symm: set x s = s' → set (get s) s' = set (get s) (set x s) = set (get s) s = s (first step by set_set, second by get_set)
• trans: set x s = s', set y s' = s'' → set y s = set y (set x s) = s'' (by set_set)

Equations

• lens.equal_outside_setoid = { r := lens.equal_outside, iseqv := ⋯ }

def GaudisCrypt.Lens.ComplContent {a : Type u_1} {m : Type u_2} (lens : Lens a m) : Type u_2

Equations

• lens.ComplContent = Quotient lens.equal_outside_setoid

def GaudisCrypt.Lens.compl {a : Type u_1} {m : Type u_2} (lens : Lens a m) : Lens lens.ComplContent m

Equations

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

noncomputable def GaudisCrypt.Lens.splitSpace {a : Type u_1} {b : Type u_2} (lens : Lens a b) : b ≃ a × lens.ComplContent

Equations

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

theorem GaudisCrypt.Lens.empty_eq {m : Type u_1} {a : Type u_2} [IsEmpty m] (lens1 lens2 : Lens a m) : lens1 = lens2

theorem GaudisCrypt.lens_leq_content_leq {m : Type u_1} [Nonempty m] (lens1 lens2 : LensIn m) (h : lens1 ≤ lens2) : Cardinal.mk lens1.content ≤ Cardinal.mk lens2.content

theorem GaudisCrypt.get_surjective {m : Type u_1} {a : Type u_2} [Nonempty m] (lens : Lens a m) : Function.Surjective lens.get

theorem GaudisCrypt.get_injective_iso_lens {m : Type u_1} {a : Type u_2} [Nonempty m] (lens : Lens a m) : Function.Injective lens.get → IsoLens lens

theorem GaudisCrypt.iso_lens_ge {a : Type u_1} {m : Type u_2} {b : Type u_1} {z : Lens a b} (lens1 : Lens a m) (lens2 : Lens b m) : IsoLens z → lens2.chain z = lens1 → LensIn.mk' lens1 ≥ LensIn.mk' lens2

theorem GaudisCrypt.lens_lt_content_lt {m : Type u_1} [Nonempty m] (lens1 lens2 : LensIn m) [Fintype lens1.content] [Fintype lens2.content] (lt : lens1 < lens2) : Fintype.card lens1.content < Fintype.card lens2.content

theorem GaudisCrypt.lens_content_div_mem {a : Type u_1} {m : Type u_2} [Fintype a] [Fintype m] (lens : Lens a m) : Fintype.card a ∣ Fintype.card m

theorem GaudisCrypt.lens_le_content_div {m : Type u_1} (lens1 lens2 : LensIn m) [Fintype lens1.content] [Fintype lens2.content] (hle : lens1 ≤ lens2) : Fintype.card lens1.content ∣ Fintype.card lens2.content

Navigating nested tuples

A TuplePath names a slot in an arbitrarily nested tuple of binary products (here/left/right); the ProjAt typeclass decomposes the (concrete) tuple type structurally, so Lens.insideTuple path deduces both the tuple type M and the component type A from the expected output type. Encoding the path as an inductive (rather than Nat arithmetic in instance indices) keeps typeclass resolution robust.

inductive GaudisCrypt.TuplePath : Type

A navigation path into an arbitrarily nested tuple of binary products. here stops at the current node; left/right descend into the first/second component of A × B and continue.

• here : TuplePath
• left : TuplePath → TuplePath
• right : TuplePath → TuplePath

class GaudisCrypt.ProjAt (p : TuplePath) (M : Type) (A : outParam Type) : Type

ProjAt p M A: following path p into tuple type M lands on component A, with projection lens proj. M is an input (taken from the expected type), A is deduced (outParam).

• proj : Lens A M

@[implicit_reducible]

instance GaudisCrypt.instProjAtHere {M : Type} : ProjAt TuplePath.here M M

Equations

• GaudisCrypt.instProjAtHere = { proj := GaudisCrypt.Lens.id }

@[implicit_reducible]

instance GaudisCrypt.instProjAtLeftProd {p : TuplePath} {A B Tgt : Type} [g : ProjAt p A Tgt] : ProjAt p.left (A × B) Tgt

Equations

• GaudisCrypt.instProjAtLeftProd = { proj := (GaudisCrypt.ProjAt.proj p).ofst }

@[implicit_reducible]

instance GaudisCrypt.instProjAtRightProd {p : TuplePath} {A B Tgt : Type} [g : ProjAt p B Tgt] : ProjAt p.right (A × B) Tgt

Equations

• GaudisCrypt.instProjAtRightProd = { proj := (GaudisCrypt.ProjAt.proj p).osnd }

def GaudisCrypt.Lens.insideTuple (p : TuplePath) {M A : Type} [g : ProjAt p M A] : Lens A M

The lens projecting the slot named by p out of a (possibly nested) tuple. The tuple type M and component type A are deduced from the expected output type.

Equations

• GaudisCrypt.Lens.insideTuple p = GaudisCrypt.ProjAt.proj p