TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.Routes

Structural routes for binary descriptor execution #

A structural route identifies the specialized kernel family entered by an operation's executable dispatcher. The route and its cost metadata are kept separate from certified candidate construction so configured-format planning can use them without importing tiny-table proofs.

source
inductive FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.StructuralRoute :
Type

The structural implementation entered by an operation's executable dispatcher.

This classifies the route that will actually run; it is not a second list of competing algorithms. Several routes share one dispatcher function, but retain distinct cost metadata because their specialized kernels have different performance.

Instances For
    source
    @[instance_reducible]
    instance FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.instDecidableEqStructuralRoute :
    DecidableEq StructuralRoute
    source
    def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.instReprStructuralRoute.repr :
    StructuralRoute → ℕ → Std.Format
    Instances For
      source
      @[instance_reducible]
      instance FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.instReprStructuralRoute :
      Repr StructuralRoute
      source
      def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.StructuralRoute.estimate (route : StructuralRoute) (format : FloatFormat) (operation : ExecFloat.Backend.Operation) :
      ExecFloat.Backend.Candidate

      Cost estimate associated with a structural route.

      Instances For
        source
        def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.isFixedFormat (format : FloatFormat) :
        Bool

        Whether the descriptor structurally satisfies a fixed-format kernel capability.

        Instances For
          source
          def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.pairKernelEligible (format : FloatFormat) :
          Bool

          Whether the descriptor structurally satisfies the two-word pair-kernel capability: an IEEE layout of at most 128 bits whose fraction is wider than one word.

          Instances For
            source
            def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.structuralRoute? (format : FloatFormat) :
            ExecFloat.Backend.Operation → Option StructuralRoute

            Select the single structural route entered by the executable dispatcher.

            The branch order mirrors the corresponding Model.*Backend implementation. Returning none means that the operation proceeds directly to its width-generic kernel.

            Instances For