Representation transfer for realization bridges

A small proof-transfer layer for the following situation: a proof quantifies over an abstract (often noncomputable, classical) operation, a compiled artifact computes a concrete (for example byte-level) operation, and a chosen encoding relates the two. Examples are a byte-level realization of a group pairing and the byte-level realizations of lattice or hash-based primitives. This module provides the relation structure and the generic transfer theorem that such a realization instantiates.

Lineage

This layer follows Kaliszyk & O'Connor, Computing with Classical Real Numbers (JFR 2009, arXiv:0809.1644), who transfer theorems across an isomorphism between Coq's classical reals and CoRN's computational reals, and forms a hand-built, fixed-relation instance of Trocq (Cohen–Crance–Mahboubi, ESOP 2024 / TOPLAS 2025, arXiv:2310.14022), whose hierarchy of relation structures performs "a fine-grained analysis of the properties required for a given proof of relatedness." This file identifies the minimal level for transferring a decidable equation: the domains need only a map, and the codomain needs an embedding (an equality-reflecting, i.e. injective, encoding) — no equivalence, no univalence. The transfer mechanisms built into Lean and Mathlib (norm_cast, and the name-translation attributes @[to_additive] and @[to_dual]) each act along a fixed axis (casts, multiplicative↔additive, order duality); this layer takes an arbitrary user-supplied representation relation.

Main definitions

• ReprEmbedding C γ — an equality-reflecting encoding C → γ.
• BinOpRealization op bop — op : A → B → C realized by bop : α → β → γ along domain maps + a codomain embedding + a commuting square.
• BinOpRealization.eq_transfer — the transfer theorem: an abstract equation op a b = op a' b' holds iff bop agrees on the encoded operands.

Representation embedding (the codomain level)

structure ReprTransfer.ReprEmbedding (C γ : Type u) : Type u

A representation embedding: a map C → γ that reflects equality (injective). This is the minimal relatedness needed to transfer a decidable equation across the representation in both directions: forward needs only a map, backward needs injectivity.

• enc : C → γ

  The encoding of abstract values as computational ones.

• enc_inj : Function.Injective self.enc

  Distinct abstract values encode distinctly (equality reflection).

@[simp]

theorem ReprTransfer.ReprEmbedding.eq_iff {C γ : Type u} (e : ReprEmbedding C γ) (a a' : C) : e.enc a = e.enc a' ↔ a = a'

Equality reflects across the embedding.

Binary-operation realization

structure ReprTransfer.BinOpRealization {A B C α β γ : Type u} (op : A → B → C) (bop : α → β → γ) : Type u

A binary-operation realization: the abstract operation op : A → B → C is realized by the computational operation bop : α → β → γ along domain encodings encA/encB (plain maps) and a codomain embedding cod, via the commuting square cod.enc (op a b) = bop (encA a) (encB b).

The asymmetry — maps on the domains, an embedding on the codomain — is the structure that transfers a decidable equation between op applications (eq_transfer). It is the Trocq-hierarchy level for this goal: weaker than an equivalence, requiring neither surjectivity of the encodings nor univalence.

• encA : A → α

  Encoding of the first operand.

• encB : B → β

  Encoding of the second operand.

• cod : ReprEmbedding C γ

  Equality-reflecting encoding of the result.

• commutes (a : A) (b : B) : self.cod.enc (op a b) = bop (self.encA a) (self.encB b)

  The commuting square tying op to bop through the encodings.

theorem ReprTransfer.BinOpRealization.eq_transfer {A B C α β γ : Type u} {op : A → B → C} {bop : α → β → γ} (R : BinOpRealization op bop) (a a' : A) (b b' : B) : op a b = op a' b' ↔ bop (R.encA a) (R.encB b) = bop (R.encA a') (R.encB b')

The transfer theorem. An abstract equation between two applications of op holds iff the computational bop agrees on the encoded operands.

A verification predicate phrased as op a b = op a' b' (e.g. a pairing-check e(X,Y) = e(X',Y')) is decided, equivalently, by the byte-level comparison the compiled code computes.

theorem ReprTransfer.BinOpRealization.eq_transfer_forward {A B C α β γ : Type u} {op : A → B → C} {bop : α → β → γ} (R : BinOpRealization op bop) {a a' : A} {b b' : B} (h : op a b = op a' b') : bop (R.encA a) (R.encB b) = bop (R.encA a') (R.encB b')

The forward (soundness) direction: an abstract equality implies the byte comparison succeeds. Needs only the commuting square, not injectivity.

theorem ReprTransfer.BinOpRealization.eq_transfer_backward {A B C α β γ : Type u} {op : A → B → C} {bop : α → β → γ} (R : BinOpRealization op bop) {a a' : A} {b b' : B} (h : bop (R.encA a) (R.encB b) = bop (R.encA a') (R.encB b')) : op a b = op a' b'

The backward (completeness) direction: the byte comparison succeeding implies the abstract equality. Uses codomain injectivity.

The relation hierarchy (Trocq's "fine-grained analysis", made explicit)

Which transfer needs which structure:

• a plain map (enc : C → γ) transfers an op-application forward (a homomorphism) — BinOpHomOn;
• an embedding (+ enc_inj) additionally reflects equality, so it transfers a decidable equation in both directions — ReprEmbedding / BinOpRealization.eq_transfer;
• an equivalence (a bijection) is the top level the univalence / SIP route requires — which the crypto encodings (point/Fp¹² serialization is injective but not surjective: most byte strings aren't valid) do not reach, so this layer never requires it and never incurs univalence.

@[reducible, inline]

abbrev ReprTransfer.ReprEquiv (C γ : Type u) : Type u

Top of the hierarchy: a representation equivalence (bijection). Refines to an embedding. Recorded for completeness; the realization bridges do not use this level (their encodings are embeddings, not bijections), which is why they stay univalence-free.

Equations

• ReprTransfer.ReprEquiv C γ = (C ≃ γ)

def ReprTransfer.ReprEquiv.toReprEmbedding {C γ : Type u} (e : ReprEquiv C γ) : ReprEmbedding C γ

An equivalence forgets to an embedding (a bijection is injective).

Equations

• e.toReprEmbedding = { enc := e.toFun, enc_inj := ⋯ }

Domain-restricted operation homomorphism (the map-level transfer)

Realizations of field arithmetic by compiled kernels (Baby Bear or Fp arithmetic on machine words) are not codomain-embedding equality transfers; they are homomorphisms along a decoding map φ, valid on a canonical sub-domain (e.g. words < p). This is a strictly weaker hierarchy level than BinOpRealization — map-only, no injectivity — and packaging it here lets those bridges share the layer.

structure ReprTransfer.BinOpHomOn {α A : Type u} (φ : α → A) (dom : α → Prop) (src : α → α → α) (tgt : A → A → A) : Prop

A domain-restricted binary-operation homomorphism: along a map φ : α → A, the concrete src maps through φ to the abstract tgt, on a canonical sub-domain dom (the < p canonical-range condition the field kernels carry). Map-level: no injectivity required.

• app_eq (a b : α) : dom a → dom b → φ (src a b) = tgt (φ a) (φ b)

  The homomorphism square, on the canonical sub-domain.

theorem ReprTransfer.BinOpHomOn.realizes {α A : Type u} {φ : α → A} {dom : α → Prop} {src : α → α → α} {tgt : A → A → A} (H : BinOpHomOn φ dom src tgt) {a b : α} (ha : dom a) (hb : dom b) : φ (src a b) = tgt (φ a) (φ b)

The realization equation: on canonical inputs, decoding the concrete result equals the abstract operation on the decoded inputs.