Documentation

Transfer.Base.Core

The repr registry + repr_transfer tactic #

A relation-generic transfer driver over the ReprTransfer layer: a registry of realization lemmas (the repr simp set) and a tactic that composes them. Tag a realization lemma enc-side = byte-side (abstract op → emitted kernel) with @[repr]; then repr_transfer rewrites any composite of registered ops to its emitted-kernel form automatically — deriving what the per-protocol bridges (groth16_full_verifier_transfer, pedersen_commitment_transfer, the field- layer connections, …) otherwise derive by hand.

register_simp_attr must live in its own module (the attribute is only usable in importing files), so the tagged lemmas live in Transfer/Base/FieldRegistry.lean and similar modules.

source
def Parser.Attr.transfer :
Lean.ParserDescr

The Trocq realization registry: a simp set of abstract-op = emitted-kernel lemmas. Tag each realization (e.g. a * b = bbFieldMul a b) with @[transfer]. (Named transfer, not repr, to avoid clashing with the Repr.repr function.)

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Parser.Attr.transfer_proc :
    Lean.ParserDescr

    Simplification procedure

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def tacticRepr_transfer :
      Lean.ParserDescr

      Transfer tactic. Rewrites the goal's abstract operations into their registered emitted kernels (the compile-to-emitted-leaf direction), composing the registered realizations structurally.

      Equations
      Instances For
        source
        def tacticRepr_transfer! :
        Lean.ParserDescr

        Variant that also closes the resulting goal by reflexivity / hypotheses.

        Equations
        Instances For