metadata:
  version: "1.0.0"
  description: "Dot product kernel — inner product"
  references:
    - "Golub & Van Loan (2013) Matrix Computations"

equations:
  dot:
    formula: "y = Σ x_i · w_i"
    domain: "x ∈ ℝ^n, w ∈ ℝ^n"
    codomain: "y ∈ ℝ"
    invariants:
      - "dot(x, 0) = 0"
      - "dot(α·x, w) = α·dot(x, w)"

proof_obligations:
  - type: linearity
    property: "Scalar linearity"
    formal: "dot(α·x, w) = α·dot(x, w)"
    applies_to: all
  - type: invariant
    property: "Zero annihilation"
    formal: "dot(x, 0) = 0"
    applies_to: all
  - type: equivalence
    property: "SIMD matches scalar"
    tolerance: 4.0
    applies_to: simd

kernel_structure:
  phases:
    - name: multiply
      description: "Element-wise x_i * w_i"
      invariant: "prod_i = x_i * w_i"
    - name: reduce
      description: "Sum all products"
      invariant: "y = Σ prod_i"

simd_dispatch:
  dot:
    scalar: dot_scalar
    avx2: dot_avx2

falsification_tests:
  - id: FALSIFY-DOT-001
    rule: "Linearity"
    prediction: "dot(α·x, w) = α·dot(x, w) within tolerance"
    if_fails: "FMA ordering breaks associativity"

kani_harnesses:
  - id: KANI-DOT-001
    obligation: DOT-LIN-001
    property: "Linearity for small vectors"
    bound: 8
    strategy: stub_float

qa_gate:
  id: F-DOT-001
  name: "Dot Product Contract"
  checks:
    - "linearity"
  pass_criteria: "All 1 falsification tests pass"
