Documentation

LeanMlir.Proofs.Float.E4M3Fold

PoC: the E4M3 (fp8) quantized MNIST-linear render-tie (planning §3b) #

planning/archive/floatbridge_quantization.md §3b: the structural faithfulness of the low-precision scheme. Where §3c bounds the accuracy of E4M3-mixed inference, this file proves the correctness of the implementation: the emitted block-scaled-E4M3 matmul graph denotes the intended algorithm, with no accuracy claim.

The deployed fp8 kernel is block-scaled with fp32 accumulate: weights are quantized offline to an integer grid with a per-output-column scale sWⱼ, activations at runtime with a per-tensor scale sx; the integer codes are multiply-accumulated in fp32; a single per-output dequant sx·sWⱼ scales the result; the fp32 bias is added. The one fact that makes this equal to "dequantize each tensor, then do the exact matmul" is that the per-output dequant scale factors out of the accumulate — (sx·sWⱼ)·∑ᵢ q(xᵢ/sx)·q(Wᵢⱼ/sWⱼ) = ∑ᵢ (sx·q(xᵢ/sx))·(sWⱼ·q(Wᵢⱼ/sWⱼ)) — which is exactly what "fp32 accumulate" buys you (the scales are constant across the reduction).

No SHlo surgery. The emitted graph is built entirely from existing den-faithful ops: operand (the int activation code = the stored bytes), dotIn (the int weight code; its den is the exact ∑, i.e. the fp32 accumulate), layerScaleF (the per-output dequant block-scale, layerScaleF_faithful), addBcast (the fp32 bias). The quantizer q : ℝ → ℝ (E4M3 round-to-nearest on the 1-4-3 grid; see scripts/mnist_e4m3_demo.py) is left abstract — the scheme is faithful for any grid, E4M3 being one instance. Quantization-to-code is the offline/runtime byte preparation that produces the operands (exactly as real fp8 inference does), so the render-tie is the genuine "the bytes implement block-scaled-E4M3 matmul with fp32 accumulate" claim.

All theorems kernel-close under [propext, Classical.choice, Quot.sound] (tests/AuditAxioms.lean). (Namespace/name kept short for the audit's per-line #print axioms grep — cf. LinearFold.lean.)

source
noncomputable def Proofs.QuantPoC.actCode {m : ℕ} (q : ℝ → ℝ) (sx : ℝ) (x : Vec m) :
Vec m

The stored integer-grid activation code (per-tensor scale sx): q(xᵢ / sx). These are the int8-style bytes the runtime feeds the kernel.

Equations
Instances For
    source
    noncomputable def Proofs.QuantPoC.weightCode {m n : ℕ} (q : ℝ → ℝ) (sW : Vec n) (W : Mat m n) :
    Mat m n

    The stored integer-grid weight code (per-output-column scale sW j): q(Wᵢⱼ / sWⱼ). Quantized offline; the per-column scale is the "block scale".

    Equations
    Instances For
      source
      noncomputable def Proofs.QuantPoC.e4m3LinearGraph {m n : ℕ} (q : ℝ → ℝ) (sx : ℝ) (sW : Vec n) (W : Mat m n) (b : Vec n) (x : Vec m) :
      StableHLO.SHlo n

      The emitted block-scaled-E4M3 linear graph. Built only from den-faithful SHlo ops: operand (int activation code) → dotIn (int weight code; the den ∑ is the fp32 accumulate) → layerScaleF (per-output dequant sx·sWⱼ) → addBcast (fp32 bias). The "int matmul, fp32 accumulate, single dequant" kernel.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Proofs.QuantPoC.quantLinear {m n : ℕ} (q : ℝ → ℝ) (sx : ℝ) (sW : Vec n) (W : Mat m n) (b : Vec n) (x : Vec m) :
        Vec n

        The intended algorithm, dequant-first form. Dequantize each tensor — activation sx·q(xᵢ/sx), weight sWⱼ·q(Wᵢⱼ/sWⱼ) (i.e. dequant ∘ quant, the round-trip) — then the exact-ℝ linear map mnistLinear. This is the reference semantics the kernel must match.

        Equations
        Instances For
          source
          theorem Proofs.QuantPoC.dequant_factors {m n : ℕ} (q : ℝ → ℝ) (sx : ℝ) (sW : Vec n) (W : Mat m n) (x : Vec m) (j : Fin n) :
          sx * sW j * ∑ i : Fin m, q (x i / sx) * q (W i j / sW j) = ∑ i : Fin m, sx * q (x i / sx) * (sW j * q (W i j / sW j))

          The block-scale factors out of the fp32 accumulate — the arithmetic heart of §3b. "Int matmul then one per-output dequant" equals "dequantize each operand then matmul"; the per-output scale sx·sWⱼ is constant across the reduction, so it pulls through the ∑. (This is why fp32 accumulate is the faithful choice.)

          source
          theorem Proofs.QuantPoC.e4m3_render_faithful {m n : ℕ} (q : ℝ → ℝ) (sx : ℝ) (sW : Vec n) (W : Mat m n) (b : Vec n) (x : Vec m) :
          StableHLO.den (e4m3LinearGraph q sx sW W b x) = quantLinear q sx sW W b x

          E4M3 render-tie (structural faithfulness, planning §3b). The emitted block-scaled int-matmul graph denotes exactly the intended dequant-first algorithm, for any quantizer q and scales sx, sW. The proof is the dequant_factors identity composed with the den of each (verified-faithful) op. No accuracy claim — purely "the bytes implement block-scaled-E4M3 matmul with fp32 accumulate".