metadata:
  version: "1.0.0"
  created: "2026-03-19"
  author: "PAIML Engineering"
  description: "Sampling algorithms for LLM token generation"
  references:
    - "Holtzman et al. (2019) The Curious Case of Neural Text Degeneration"

equations:
  temperature_scaling:
    formula: "P_scaled(x)_i = softmax(x_i / T)"
    domain: "x ∈ ℝ^V, T > 0"
    invariants:
      - "T→0: argmax selection, T→∞: uniform"
      - "P_scaled sums to 1.0"
  top_p:
    formula: "V_p = min{V_sorted : Σ P(v) ≥ p}, renormalize over V_p"
    domain: "P ∈ (0,1)^V, p ∈ (0,1]"
    invariants:
      - "Σ P_filtered = 1.0 after renormalization"
      - "|V_p| ≤ |V|"

proof_obligations:
  - type: invariant
    property: "Temperature-scaled probabilities sum to 1"
    formal: "|Σ softmax(x/T) - 1.0| < eps"
    tolerance: 1.0e-6
    applies_to: all
  - type: bound
    property: "Top-p vocabulary size bounded"
    formal: "|V_p| ≥ 1 and |V_p| ≤ |V|"
    applies_to: all
  - type: invariant
    property: "Top-p renormalized"
    formal: "Σ P_filtered = 1.0 after top-p filtering"
    tolerance: 1.0e-6
    applies_to: all

falsification_tests:
  - id: FALSIFY-SAMP-001
    rule: "Temperature normalization"
    prediction: "Sum = 1.0 for T in {0.1, 0.5, 1.0, 2.0}"
    test: "Random logits, multiple temperatures"
    if_fails: "Division before softmax wrong"
  - id: FALSIFY-SAMP-002
    rule: "Top-p bounds"
    prediction: "At least 1 token, at most vocab_size"
    test: "p=0.01 and p=1.0 edge cases"
    if_fails: "Cumulative sum threshold bug"
  - id: FALSIFY-SAMP-003
    rule: "Top-p renormalization"
    prediction: "Filtered probs sum to 1.0"
    test: "Apply top-p, check sum"
    if_fails: "Renormalization denominator wrong"

kani_harnesses:
  - id: samp-kani-001
    obligation: "Temperature-scaled probabilities sum to 1"
    bound: 4
    strategy: stub_float
