class GaudisCrypt.GranularProgramSpecextends GaudisCrypt.ProgramSpec : Type 1

• state : Type
• grains : Set (Footprint State)
• from_lenses (f : Footprint State) : f ∈ grains → f.FromLens
• disjoint (f : Footprint State) : f ∈ grains → ∀ g ∈ grains, f ≠ g → f ≤ gᶜ
• nonempty_grains (f : Footprint State) : f ∈ grains → f ≠ ⊥

def GaudisCrypt.GranularFootprint [spec : GranularProgramSpec] : Type

Equations

• GaudisCrypt.GranularFootprint = Finset ↑GaudisCrypt.GranularProgramSpec.grains

def GaudisCrypt.GranularFootprint.grains [spec : GranularProgramSpec] (F : GranularFootprint) : Set (Footprint State)

Equations

• F.grains = Subtype.val '' ↑(have this := F; this)

def GaudisCrypt.GranularFootprint.grainsFinset [spec : GranularProgramSpec] (F : GranularFootprint) : Finset (Footprint State)

Equations

• F.grainsFinset = Finset.map { toFun := Subtype.val, inj' := ⋯ } F

theorem GaudisCrypt.GranularFootprint.grains_finite [spec : GranularProgramSpec] (F : GranularFootprint) : F.grains.Finite

theorem GaudisCrypt.GranularFootprint.grains_subset [spec : GranularProgramSpec] (F : GranularFootprint) : F.grains ⊆ GranularProgramSpec.grains

def GaudisCrypt.GranularFootprint.footprint [spec : GranularProgramSpec] (F : GranularFootprint) : Footprint ProgramSpec.state

Equations

• F.footprint = sSup F.grains

def GaudisCrypt.Footprint.IsGranular [spec : GranularProgramSpec] (f : Footprint ProgramSpec.state) : Prop

Equations

• f.IsGranular = ∃ (F : GaudisCrypt.GranularFootprint), f = F.footprint

def GaudisCrypt.Footprint.IsSubGranular [spec : GranularProgramSpec] (f : Footprint ProgramSpec.state) : Prop

Equations

• f.IsSubGranular = ∃ (F : GaudisCrypt.GranularFootprint), f ≤ F.footprint

@[implicit_reducible]

instance GaudisCrypt.instPartialOrderGranularFootprint [spec : GranularProgramSpec] : PartialOrder GranularFootprint

Equations

• GaudisCrypt.instPartialOrderGranularFootprint = { le := fun (f g : GaudisCrypt.GranularFootprint) => f.grains ⊆ g.grains, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[implicit_reducible]

instance GaudisCrypt.instOrderBotGranularFootprint [spec : GranularProgramSpec] : OrderBot GranularFootprint

Equations

• GaudisCrypt.instOrderBotGranularFootprint = { bot := Finset.empty, bot_le := ⋯ }

def GaudisCrypt.GranularFootprint.toFinset [spec : GranularProgramSpec] (F : GranularFootprint) : Finset ↑GranularProgramSpec.grains

Equations

• F.toFinset = F

theorem GaudisCrypt.GranularFootprint.le_iff_subset [spec : GranularProgramSpec] {f g : GranularFootprint} : f ≤ g ↔ (have this := f; this) ⊆ have this := g; this

@[implicit_reducible]

noncomputable instance GaudisCrypt.instLatticeGranularFootprint [spec : GranularProgramSpec] : Lattice GranularFootprint

Equations

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

theorem GaudisCrypt.GranularFootprint.toFinset_injective [spec : GranularProgramSpec] : Function.Injective toFinset

@[implicit_reducible]

noncomputable instance GaudisCrypt.instSDiffGranularFootprint [spec : GranularProgramSpec] : SDiff GranularFootprint

Equations

• GaudisCrypt.instSDiffGranularFootprint = { sdiff := fun (f g : GaudisCrypt.GranularFootprint) => f.toFinset \ g.toFinset }

@[implicit_reducible]

noncomputable instance GaudisCrypt.instGeneralizedBooleanAlgebraGranularFootprint [spec : GranularProgramSpec] : GeneralizedBooleanAlgebra GranularFootprint

GranularFootprint is a generalized Boolean algebra (a distributive lattice with ⊥ and a relative complement \), inherited from Finset spec.grains via the identity injection toFinset. There is no ⊤/ᶜ in general: complementing a finite grain family need not stay finite when the granularity is infinite, so this does not extend to a BooleanAlgebra.

Equations

• GaudisCrypt.instGeneralizedBooleanAlgebraGranularFootprint = Function.Injective.generalizedBooleanAlgebra GaudisCrypt.GranularFootprint.toFinset ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

noncomputable instance GaudisCrypt.instInfSetGranularFootprint [spec : GranularProgramSpec] : InfSet GranularFootprint

Infimum of a family of grain-sets: the intersection (grains common to every member). Only meaningful when the family is nonempty; empty family reduces to ⊥ (junk, unconstrained by the conditional axioms).

Equations

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

@[implicit_reducible]

noncomputable instance GaudisCrypt.instSupSetGranularFootprint [spec : GranularProgramSpec] : SupSet GranularFootprint

Supremum of a family of grain-sets: the union (grains touched by some member), which stays finite exactly when the family is bounded above. Unbounded families reduce to ⊥ (junk); the empty family also gives ⊥, so sSup ∅ = ⊥.

Equations

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

@[implicit_reducible]

noncomputable instance GaudisCrypt.instConditionallyCompleteLatticeGranularFootprint [spec : GranularProgramSpec] : ConditionallyCompleteLattice GranularFootprint

GranularFootprint is a conditionally complete lattice: any nonempty family of grain-sets that is bounded below has a greatest lower bound (its intersection), and any nonempty family bounded above has a least upper bound (its union — finite because contained in the bound). It is not a CompleteLattice: there is no ⊤ when the granularity is infinite. Combined with the existing OrderBot, sSup ∅ = ⊥ holds by construction.

Equations

• GaudisCrypt.instConditionallyCompleteLatticeGranularFootprint = { toLattice := inferInstance, toSupSet := inferInstance, toInfSet := inferInstance, isLUB_csSup := ⋯, isGLB_csInf := ⋯ }

theorem GaudisCrypt.GranularFootprint.footprint_mono [spec : GranularProgramSpec] {F G : GranularFootprint} (h : F ≤ G) : F.footprint ≤ G.footprint

noncomputable def GaudisCrypt.Footprint.IsSubGranular.granularCover [spec : GranularProgramSpec] {footprint : Footprint State} (h : footprint.IsSubGranular) : GranularFootprint

A minimal granular cover of a sub-granular footprint: the sub-family of the grains of exactly the atoms footprint genuinely touches. It is the least granular footprint containing footprint — that every touched atom is needed is immediate, and that these atoms already cover footprint is the product-corner argument inlined into Footprint.IsSubGranular.granularCover_ge.

Equations

• h.granularCover = ⋯.toFinset

theorem GaudisCrypt.GranularFootprint.footprint_fromLens [spec : GranularProgramSpec] (F : GranularFootprint) : F.footprint.FromLens

A granular footprint is a join of finitely many pairwise-disjoint lens footprints, hence itself lens-derived.

theorem GaudisCrypt.IsGranularFootprint.fromLens [spec : GranularProgramSpec] {f : Footprint State} (h : f.IsGranular) : f.FromLens

noncomputable def GaudisCrypt.IsGranularFootprint.lens [spec : GranularProgramSpec] {f : Footprint State} (h : f.IsGranular) : Lens (Quotient fᶜ.orbit_setoid) State

Equations

• GaudisCrypt.IsGranularFootprint.lens h = ⋯.lens

theorem GaudisCrypt.isSubGranularFootprint_closed_sup [spec : GranularProgramSpec] {f g : Footprint State} (hf : f.IsSubGranular) (hg : g.IsSubGranular) : (f ⊔ g).IsSubGranular

theorem GaudisCrypt.Footprint.IsSubGranular.granularCover_footprint_eq_sSup [spec : GranularProgramSpec] (f : Footprint State) (h : f.IsSubGranular) : h.granularCover.footprint = sSup {g : Footprint State | g ∈ GranularProgramSpec.grains ∧ ¬f ≤ gᶜ}

The minimal granular cover's footprint is the join of exactly the grains that f touches.

theorem GaudisCrypt.lens_pair_isSubGranular {a b : Type} [GranularProgramSpec] {lens1 : Lens a State} {lens2 : Lens b State} [disjoint lens1 lens2] (h1 : lens1.footprint.IsSubGranular) (h2 : lens2.footprint.IsSubGranular) : (lens1.pair lens2).footprint.IsSubGranular

theorem GaudisCrypt.Granularity.lens_pair_isSubGranular_sup {a b : Type} [GranularProgramSpec] {lens1 : Lens a State} {lens2 : Lens b State} [disjoint lens1 lens2] (h1 : lens1.footprint.IsSubGranular) (h2 : lens2.footprint.IsSubGranular) : ⋯.granularCover.footprint = h1.granularCover.footprint ⊔ h2.granularCover.footprint

theorem GaudisCrypt.Footprint.IsSubGranular.granularCover_ge [spec : GranularProgramSpec] (footprint : Footprint State) (h : footprint.IsSubGranular) : footprint ≤ h.granularCover.footprint