The univalence-free refusal guard

The crux of the Trocq port is to compute, per subterm, the minimal (m,n) relation level a goal needs, and — when that level is the equivalence top (level equiv, where an equivalence is used as an equality) — refuse and report rather than import univalence (UA), which would enlarge the TCB and is in any case false for the (non-surjective) byte encodings.

That full per-subterm level inference is a separate, larger engine (Coq-Elpi → Lean MetaM). This module provides the tractable, decidable guard it relies on. The primary form of the cap lives on the Trocq lattice: the guard refuses exactly the map4 universe witness (permittedMapClass / classifyMapClass — map0–map3 is the univalence-free fragment, wider than the 3-point view). The 3-point classification (permitted / classify) is the view of that lattice guard through RelLevel.toMapClass (permitted_toMapClass / classify_toMapClass), so refusing equiv is the derived form of refusing map4. This guard makes the discipline enforceable and distinguishes this cap from full Coq-Trocq.

The discipline

The permitted (m,n) slice on the lattice is map0–map3; in the 3-point view: map (transfers = forward), embedding (+ injective, transfers = both ways), and the refused equiv (image map4, needs UA). The crypto encodings (point/Fp¹²/word serializations) are embeddings, not bijections, so a goal that would need equiv is one this layer declines.

def Transfer.LevelRefusal.permittedMapClass : Param.MapClass → Bool

Primary. The univalence-free slice of the Trocq lattice: a MapClass is permitted iff it is not the map4 universe witness. map0–map3 are univalence-free (the fragment wider than the 3-point view — map2a, map2b and map3 are all permitted); only map4 needs UA.

Equations

• Transfer.LevelRefusal.permittedMapClass Transfer.Param.MapClass.map4 = false
• Transfer.LevelRefusal.permittedMapClass x✝ = true

def Transfer.LevelRefusal.permitted (lvl : RelLevel) : Bool

The univalence-free slice in the 3-point view: the lattice guard through toMapClass. map and embedding are univalence-free; equiv (image map4) needs UA.

Equations

• Transfer.LevelRefusal.permitted lvl = Transfer.LevelRefusal.permittedMapClass lvl.toMapClass

theorem Transfer.LevelRefusal.permitted_toMapClass (lvl : RelLevel) : permitted lvl = permittedMapClass lvl.toMapClass

The 3-point guard is the view of the lattice guard (definitional).

theorem Transfer.LevelRefusal.permitted_eq_old (lvl : RelLevel) : permitted lvl = match lvl with | RelLevel.equiv => false | x => true

Old = new: the derived guard agrees with the original 3-point table (refuse exactly equiv).

theorem Transfer.LevelRefusal.permittedMapClass_eq_false_iff (m : Param.MapClass) : permittedMapClass m = false ↔ m = Param.MapClass.map4

The lattice cap refuses exactly the map4 universe witness.

inductive Transfer.LevelRefusal.TransferOutcome : Type

The outcome of classifying the level a (sub)goal needs: either a permitted univalence-free transfer at lvl, or a refusal carrying a report of why (which subterm forced the equivalence level). The full engine feeds classify the level it infers per subterm; this module supplies classify and the report, not the inference.

• ok (lvl : RelLevel) : TransferOutcome

  Transfer permitted at this (univalence-free) level.

• refused (report : String) : TransferOutcome

  Transfer refused: the goal needs equiv (equivalence-as-equality).

def Transfer.LevelRefusal.instDecidableEqTransferOutcome.decEq (x✝ x✝¹ : TransferOutcome) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Transfer.LevelRefusal.instDecidableEqTransferOutcome.decEq (Transfer.LevelRefusal.TransferOutcome.ok lvl) (Transfer.LevelRefusal.TransferOutcome.refused report) = isFalse ⋯
• Transfer.LevelRefusal.instDecidableEqTransferOutcome.decEq (Transfer.LevelRefusal.TransferOutcome.refused report) (Transfer.LevelRefusal.TransferOutcome.ok lvl) = isFalse ⋯

@[instance_reducible]

instance Transfer.LevelRefusal.instDecidableEqTransferOutcome : DecidableEq TransferOutcome

Equations

• Transfer.LevelRefusal.instDecidableEqTransferOutcome = Transfer.LevelRefusal.instDecidableEqTransferOutcome.decEq

def Transfer.LevelRefusal.instReprTransferOutcome.repr : TransferOutcome → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Transfer.LevelRefusal.instReprTransferOutcome : Repr TransferOutcome

Equations

• Transfer.LevelRefusal.instReprTransferOutcome = { reprPrec := Transfer.LevelRefusal.instReprTransferOutcome.repr }

def Transfer.LevelRefusal.classifyMapClass : Param.MapClass → TransferOutcome

Primary. Classify a needed lattice level: refuse exactly the map4 universe witness, reporting it; every univalence-free level is permitted at its 3-point view.

Equations

• One or more equations did not get rendered due to their size.
• Transfer.LevelRefusal.classifyMapClass x✝ = Transfer.LevelRefusal.TransferOutcome.ok x✝.view3

def Transfer.LevelRefusal.classify (lvl : RelLevel) : TransferOutcome

Classify a needed level: the lattice classifier through toMapClass — refuses exactly the equivalence top (image map4), reporting it.

Equations

• Transfer.LevelRefusal.classify lvl = Transfer.LevelRefusal.classifyMapClass lvl.toMapClass

theorem Transfer.LevelRefusal.classify_toMapClass (lvl : RelLevel) : classify lvl = classifyMapClass lvl.toMapClass

The 3-point classifier is the view of the lattice classifier (definitional).

theorem Transfer.LevelRefusal.classifyMapClass_refused_iff (m : Param.MapClass) : (∃ (r : String), classifyMapClass m = TransferOutcome.refused r) ↔ m = Param.MapClass.map4

The lattice classifier refuses exactly the map4 universe witness.

theorem Transfer.LevelRefusal.classifyMapClass_map3_ok : classifyMapClass Param.MapClass.map3 = TransferOutcome.ok RelLevel.embedding

The wider-than-3-point fragment is permitted at the lattice level: a two-sided graph relation (map3) classifies as an embedding-view transfer, not a refusal.

The guard is correct and decidable

theorem Transfer.LevelRefusal.classify_map : classify RelLevel.map = TransferOutcome.ok RelLevel.map

map is permitted (forward equation transfer needs no UA).

theorem Transfer.LevelRefusal.classify_embedding : classify RelLevel.embedding = TransferOutcome.ok RelLevel.embedding

embedding is permitted (both-ways equation transfer via injectivity — the level at which the crypto encodings, and the Num ↪ ℕ transfer, live).

theorem Transfer.LevelRefusal.classify_equiv_refused : ∃ (r : String), classify RelLevel.equiv = TransferOutcome.refused r

equiv is refused with a report — the univalence-free cap.

theorem Transfer.LevelRefusal.permitted_iff_not_refused (lvl : RelLevel) : permitted lvl = true ↔ ∀ (r : String), classify lvl ≠ TransferOutcome.refused r

classify permits a level iff permitted says so — the guard and the classifier agree, by cases on the three levels.

A minimal-level inferencer over a goal-shape model

The classifier above takes the needed level as given and only classifies it. This inferencer computes the level from a small, hand-rolled goal-shape AST and feeds the inferred level to classify, so classify is reached with equiv when the shape forces it rather than when a level is supplied.

This is a minimal model. It walks a GoalShape — a small model of the cases the level discipline turns on — not a real Expr. The full engine traverses a Lean Expr, threads RelatedAt annotations through binders, and is a larger MetaM port (no Lean precedent). The contribution here is the direction of dataflow: level ← shape, then refuse-or-permit.

The modeling decisions

• A leaf is an equation whose carrier encoding has some RelLevel and a surjective : Bool flag. The flag distinguishes an embedding that is onto (so the backward direction is free) from a non-surjective encoding (the crypto case: a point/Fp¹²/word serialization that is injective but not onto, so the reverse needs UA).
• A forward ∀ (forallFwd) transfers in the map direction only: it adds no strength, so inferLevel (forallFwd d) = inferLevel d.
• A backward ∀ (forallBwd) needs the reverse direction over its domain.
  • Over a surjective domain the backward direction is available at the embedding strength, so inferLevel is max (inferLevel d) embedding.
  • Over a non-surjective domain at level embedding (the crypto encodings) the reverse needs a bijection, so inferLevel is equiv. This is the one place the inferencer produces equiv, exactly when a subterm lacks the backward direction — matching the classifier's discipline that equiv is refused.
  • A forallBwd whose domain already needs equiv stays at equiv.
• A composite (compose a b) supports only its weakest part, so inferLevel (compose a b) = RelLevel.meet (inferLevel a) (inferLevel b) (using meet from Levels.lean).

inductive Transfer.LevelRefusal.GoalShape : Type

A tiny goal-shape AST: the cases the minimal-level inferencer reasons about. A model of the level discipline rather than a real Expr (the full engine walks Expr; this drives the dataflow level ← shape).

• leafEq (carrierLevel : RelLevel) (surjective : Bool) : GoalShape

  An equation at a leaf whose carrier encoding has level carrierLevel; surjective records whether that encoding is onto (so the backward direction is free) — false is the crypto case (injective, not onto).

• forallFwd (dom : GoalShape) : GoalShape

  A ∀ transferred in the forward (map) direction: adds no strength.

• forallBwd (dom : GoalShape) : GoalShape

  A ∀ needing the backward direction over dom: needs at least embedding, and forces equiv when dom is a non-surjective leaf.

• compose (a b : GoalShape) : GoalShape

  A composite: level is the meet (weakest) of the parts.

def Transfer.LevelRefusal.instReprGoalShape.repr : GoalShape → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Transfer.LevelRefusal.instReprGoalShape : Repr GoalShape

Equations

• Transfer.LevelRefusal.instReprGoalShape = { reprPrec := Transfer.LevelRefusal.instReprGoalShape.repr }

def Transfer.LevelRefusal.maxLevel (l₁ l₂ : RelLevel) : RelLevel

The maximum (stronger) of two levels — dual to RelLevel.meet; a backward ∀ needs at least embedding, so it takes the max with embedding.

Equations

• Transfer.LevelRefusal.maxLevel l₁ l₂ = if l₁.toNat ≤ l₂.toNat then l₂ else l₁

def Transfer.LevelRefusal.needsEquivUnderBwd : GoalShape → Bool

Whether a shape's domain is a leaf that is an embedding but not surjective — the configuration whose reverse direction needs a bijection, hence forces equiv under a backward ∀.

Equations

• Transfer.LevelRefusal.needsEquivUnderBwd (Transfer.LevelRefusal.GoalShape.leafEq Transfer.RelLevel.embedding false) = true
• Transfer.LevelRefusal.needsEquivUnderBwd x✝ = false

def Transfer.LevelRefusal.inferLevel : GoalShape → RelLevel

Infer the minimal level a shape needs. The level is computed, then handed to classify. See the section docstring above for the modeling decisions behind each clause.

Equations

• One or more equations did not get rendered due to their size.
• Transfer.LevelRefusal.inferLevel (Transfer.LevelRefusal.GoalShape.leafEq l surjective) = l
• Transfer.LevelRefusal.inferLevel d.forallFwd = Transfer.LevelRefusal.inferLevel d
• Transfer.LevelRefusal.inferLevel (a.compose b) = (Transfer.LevelRefusal.inferLevel a).meet (Transfer.LevelRefusal.inferLevel b)

def Transfer.LevelRefusal.inferAndClassify : GoalShape → TransferOutcome

The end-to-end guard: infer the level the shape needs, then refuse or permit it. classify is called on a computed level.

Equations

• Transfer.LevelRefusal.inferAndClassify = Transfer.LevelRefusal.classify ∘ Transfer.LevelRefusal.inferLevel

The inferencer is exercised end-to-end

theorem Transfer.LevelRefusal.inferAndClassify_leaf_embedding : inferAndClassify (GoalShape.leafEq RelLevel.embedding true) = TransferOutcome.ok RelLevel.embedding

A plain embedding equation (e.g. a Num ↪ ℕ leaf) infers embedding and is permitted.

theorem Transfer.LevelRefusal.inferAndClassify_leaf_map : inferAndClassify (GoalShape.leafEq RelLevel.map true) = TransferOutcome.ok RelLevel.map

A leaf at map (forward-only) is permitted at map.

theorem Transfer.LevelRefusal.inferAndClassify_forallFwd_embedding : inferAndClassify (GoalShape.leafEq RelLevel.embedding true).forallFwd = TransferOutcome.ok RelLevel.embedding

A forward ∀ over an embedding leaf still infers embedding and is permitted — the forward direction adds no strength.

theorem Transfer.LevelRefusal.inferAndClassify_forallBwd_surjective : inferAndClassify (GoalShape.leafEq RelLevel.embedding true).forallBwd = TransferOutcome.ok RelLevel.embedding

A backward ∀ over a surjective embedding leaf is still permitted at embedding — the reverse direction is available because the leaf is onto.

theorem Transfer.LevelRefusal.inferAndClassify_forallBwd_nonsurjective_refused : ∃ (r : String), inferAndClassify (GoalShape.leafEq RelLevel.embedding false).forallBwd = TransferOutcome.refused r

The central refusal. A backward ∀ over a non-surjective embedding leaf (the crypto encoding case) infers equiv, so the end-to-end guard refuses — the engine declines exactly when a subterm forces the equivalence level.

theorem Transfer.LevelRefusal.inferLevel_forallBwd_nonsurjective : inferLevel (GoalShape.leafEq RelLevel.embedding false).forallBwd = RelLevel.equiv

The inferred level for that refused shape is exactly equiv — pinning down why it was refused.

theorem Transfer.LevelRefusal.inferAndClassify_compose_meet : inferAndClassify ((GoalShape.leafEq RelLevel.map true).compose (GoalShape.leafEq RelLevel.embedding true)) = TransferOutcome.ok RelLevel.map

A composite drops to the weaker level: composing a map leaf with an embedding leaf infers map (the meet), and is permitted at map.

theorem Transfer.LevelRefusal.inferAndClassify_compose_rescues : inferAndClassify ((GoalShape.leafEq RelLevel.map true).compose (GoalShape.leafEq RelLevel.embedding false).forallBwd) = TransferOutcome.ok RelLevel.map

A composite that contains a refusing part still composes down: meeting an equiv-forcing backward-∀ with a map leaf yields map — the composite is permitted because its weakest part carries no UA need. So meet can rescue a transfer, and refusal is level-driven (it occurs only when the inferred level — after all meets — is equiv).

What this module is not

The inferencer above is a minimal model over a hand-rolled GoalShape; the level it computes is faithful to the discipline (forward adds nothing; backward over a non-surjective embedding forces equiv; composites meet), but the full engine walks a real Expr, threads RelatedAt levels through actual binders, and infers the least level that makes the whole transfer go through. That level-annotated parametricity translation is the heart of the Trocq paper and a larger MetaM port (no Lean precedent). The RelatedAt kernel carries the level; the transfer tactic traverses binders; the minimal-level solver over Expr is not implemented here. The contribution here is the dataflow direction: the level is computed and fed to classify rather than supplied.