Validation of top 50 HF models

.pmat-tickets/DEBT-COV-20260705104033.yaml

@@ -0,0 +1,22 @@
+# PMAT Legacy Debt Ticket
+# Auto-generated by `pmat comply upgrade`
+# DO NOT DELETE - Required for Popperian falsification override
+
+ticket_id: "DEBT-COV-20260705104033"
+category: "coverage"
+created_at: "2026-07-05T10:40:33.185722978+00:00"
+status: "open"
+
+description: |
+  Coverage 0.0% is below required 95.0%
+
+metrics:
+  current: 0.00
+  required: 95.00
+  gap: 95.00
+
+resolution:
+  # Update this section when addressing the debt
+  plan: "TBD"
+  target_date: null
+  completed_at: null

.pmat-tickets/DEBT-SIZE-20260705104033.yaml

@@ -0,0 +1,22 @@
+# PMAT Legacy Debt Ticket
+# Auto-generated by `pmat comply upgrade`
+# DO NOT DELETE - Required for Popperian falsification override
+
+ticket_id: "DEBT-SIZE-20260705104033"
+category: "file_size"
+created_at: "2026-07-05T10:40:33.185755177+00:00"
+status: "open"
+
+description: |
+  7727 file(s) exceed 500 line limit: crates/aprender-contracts-staging/lean/.lake/packages/mathlib/.lake/build/ir/Mathlib/CategoryTheory/SmallRepresentatives.c: 514 lines, crates/aprender-rand/src/tests.rs: 515 lines, crates/aprender-present-terminal/src/ptop/ui/panels/psi.rs: 574 lines, .claude/worktrees/agent-acfe67904858695b9/crates/aprender-orchestrate/src/bug_hunter/model_parity.rs: 532 lines, crates/aprender-contracts-staging/lean/.lake/packages/mathlib/.lake/build/ir/Mathlib/CategoryTheory/Limits/Bicones.c: 1087 lines, .claude/worktrees/agent-acfe67904858695b9/crates/aprender-orchestrate/src/comply/rules/ci_workflow.rs: 655 lines, crates/aprender-contracts-staging/lean/.lake/packages/aesop/.lake/build/ir/Aesop/Script/ScriptM.c: 741 lines, crates/aprender-contracts-staging/lean/.lake/packages/batteries/.lake/build/ir/Batteries/CodeAction/Misc.c: 12782 lines, crates/aprender-serve/tests/cuda_coverage.rs: 1783 lines, crates/aprender-contracts-staging/lean/.lake/packages/mathlib/.lake/build/ir/Mathlib/RingTheory/DedekindDomain/SelmerGroup.c: 665 lines
+
+metrics:
+  current: 7727.00
+  required: 0.00
+  gap: -7727.00
+
+resolution:
+  # Update this section when addressing the debt
+  plan: "TBD"
+  target_date: null
+  completed_at: null

.pmat-work.toml

@@ -0,0 +1,20 @@
+[contract]
+min_coverage_pct = 95.0
+max_tdg_regression = 0.0
+max_function_complexity = 20
+max_file_lines = 500
+min_spec_score = 95
+
+[contract.enforcement]
+manifest_integrity = "block"
+coverage_gaming = "block"
+differential_coverage = "block"
+absolute_coverage = "block"
+tdg_regression = "block"
+complexity_regression = "block"
+file_size_regression = "warn"
+spec_quality = "block"
+roadmap_update = "block"
+github_sync = "block"
+supply_chain = "block"
+meta_check = "block"

contracts/absolute-position-v1.yaml

@@ -18,7 +18,16 @@ equations:
     preconditions:
     - indices.iter().all(|&i| i < vocab_size)
     - indices.len() > 0
-    lean_theorem: Theorems.Absolute_Position_Add
+    lean_theorem: Theorems.AbsolutePosition.Core
+  sinusoidal_position:
+    formula: PE(pos, 2i) = sin(pos / 10000^(2i/d)); PE(pos, 2i+1) = cos(pos / 10000^(2i/d))
+    domain: pos in R, i in {0, ..., d/2 - 1}, d even
+    codomain: PE(pos, j) in [-1, 1]
+    invariants:
+    - -1 <= PE(pos, j) <= 1 for all pos, j (sin/cos range)
+    - PE(0, 2i) = 0 and PE(0, 2i+1) = 1 (known zero-position value)
+    - PE(pos+k) is a linear rotation of PE(pos) by angle k*omega(i) (angle addition)
+    lean_theorem: Theorems.AbsolutePosition.Core
 proof_obligations:
 - type: invariant
   property: Shape preservation
@@ -36,6 +45,18 @@ proof_obligations:
   property: Finite output
   formal: is_finite(token_embed[t]) and is_finite(pos_embed[t]) implies is_finite(output[t])
   applies_to: all
+- type: bound
+  property: Sinusoidal component bound
+  formal: -1 <= PE(pos, j) <= 1 for all pos, j (Real.sin/cos range)
+  applies_to: sinusoidal_position
+- type: invariant
+  property: Zero-position value
+  formal: PE(0, 2i) = 0 and PE(0, 2i+1) = 1
+  applies_to: sinusoidal_position
+- type: linearity
+  property: Relative-position rotation
+  formal: PE(pos+k) = R(k*omega(i)) . PE(pos) — linear rotation via angle addition (sin_add/cos_add)
+  applies_to: sinusoidal_position
 kernel_structure:
   phases:
   - name: lookup_position_embedding
@@ -83,6 +104,21 @@ falsification_tests:
   prediction: output is finite for all finite inputs
   test: proptest with random finite token_embed and pos_embed values
   if_fails: Float addition producing NaN or Inf from finite inputs
+- id: FALSIFY-AP-005
+  rule: Sinusoidal component bound
+  prediction: every PE(pos, j) component lies in [-1, 1]
+  test: proptest with random pos and dimension index, assert component in [-1, 1]
+  if_fails: Sinusoidal encoding produces a component outside sin/cos range
+- id: FALSIFY-AP-006
+  rule: Zero-position value
+  prediction: PE(0, 2i) = 0 and PE(0, 2i+1) = 1
+  test: proptest over dimension indices at pos = 0, assert even = 0 and odd = 1
+  if_fails: Zero-position encoding is not (0, 1) per even/odd component
+- id: FALSIFY-AP-007
+  rule: Relative-position rotation
+  prediction: PE(pos+k) equals the angle-addition rotation of PE(pos) by k*omega(i)
+  test: proptest with random pos, k, i; assert sin_add/cos_add rotation identity holds
+  if_fails: Shifted encoding is not a linear rotation of the base encoding
 kani_harnesses:
 - id: KANI-AP-001
   obligation: AP-INV-001
@@ -129,3 +165,23 @@ qa_gate:
   - finite_output
   pass_criteria: All 4 falsification tests pass + Kani harnesses verify
   falsification: Replace addition with multiplication to break additive identity
+verification_summary:
+  total_obligations: 7
+  l2_property_tested: 7
+  l3_kani_proved: 4
+  l4_lean_proved: 5
+  l4_sorry_count: 0
+  l4_not_applicable: 2
+# L4 leveling justification (strict per-obligation, proved + N/A == total):
+#   PROVED in Lean (ProvableContracts.Theorems.AbsolutePosition.Core, sorry-free,
+#   verified via `lake env lean` exit 0):
+#     1. Shape preservation      -> abs_add_shape   (elementwise, Fin n preserved)
+#     2. Additive identity       -> abs_add_identity (add_zero)
+#     3. Sinusoidal comp. bound  -> pe_even_bound / pe_odd_bound (Real.sin/cos in [-1,1])
+#     4. Zero-position value     -> pe_even_at_zero / pe_odd_at_zero (sin 0 = 0, cos 0 = 1)
+#     5. Relative-pos. rotation  -> pe_even_rotation / pe_odd_rotation (sin_add/cos_add)
+#   GENUINELY NOT APPLICABLE (runtime/IEEE — no analytic identity to prove):
+#     6. Max position bound  -> caller-supplied index precondition, enforced by a
+#        runtime `assert!(seq_len <= max_pos)`; constrains inputs, not an operation identity.
+#     7. Finite output       -> IEEE-754 f32 semantics (finite + finite may overflow to Inf);
+#        vacuous over Real (all reals finite), so no analytic theorem exists.

contracts/activation-kernel-v1.yaml

@@ -108,6 +108,72 @@ proof_obligations:
     - le_max_left
     mathlib_imports: []
     notes: 'relu(x) = max 0 x ≥ 0 by le_max_left 0 x.'
+- type: invariant
+  property: ReLU idempotent
+  formal: ReLU(ReLU(x)) = ReLU(x)
+  applies_to: all
+  lean:
+    theorem: Elementwise.relu_idempotent
+    module: ProvableContracts.Elementwise
+    status: proved
+    depends_on:
+    - relu_nonneg
+    - relu_of_nonneg
+    mathlib_imports: []
+    notes: 'relu output is non-negative (relu_nonneg) and relu is the identity on
+      non-negative inputs (relu_of_nonneg), so relu(relu x) = relu x.'
+- type: invariant
+  property: Leaky-ReLU identity on non-negative inputs
+  formal: x ≥ 0 ⟹ LeakyReLU(α, x) = x
+  applies_to: all
+  lean:
+    theorem: Elementwise.leaky_relu_of_nonneg
+    module: ProvableContracts.Elementwise
+    status: proved
+    depends_on: []
+    mathlib_imports: []
+    notes: 'leaky_relu(α,x) = if x ≥ 0 then x else α·x; the non-negative branch is the
+      identity, closed by if_pos. Matches Rust nn::functional::leaky_relu (x>0 ⟹ x).'
+- type: invariant
+  property: Leaky-ReLU negative-slope branch
+  formal: x < 0 ⟹ LeakyReLU(α, x) = α · x
+  applies_to: all
+  lean:
+    theorem: Elementwise.leaky_relu_of_neg
+    module: ProvableContracts.Elementwise
+    status: proved
+    depends_on: []
+    mathlib_imports: []
+    notes: 'leaky_relu(α,x) = if x ≥ 0 then x else α·x; for x < 0 the else-branch gives
+      α·x, closed by if_neg (not_le.mpr hx).'
+- type: bound
+  property: GELU non-negative on non-negative inputs
+  formal: x ≥ 0 ⟹ GELU(x) ≥ 0
+  applies_to: all
+  lean:
+    theorem: Gelu.gelu_nonneg_of_nonneg
+    module: ProvableContracts.Gelu
+    status: proved
+    depends_on:
+    - Real.neg_one_lt_tanh
+    mathlib_imports:
+    - Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
+    notes: 'GELU(x) = 0.5·x·(1 + tanh a); for x ≥ 0 the factor 0.5·x ≥ 0 and 1 + tanh a
+      > 0 since tanh a > -1 (Real.neg_one_lt_tanh), so the product is ≥ 0.'
+- type: bound
+  property: GELU bounded by identity on non-negative inputs
+  formal: x ≥ 0 ⟹ GELU(x) ≤ x
+  applies_to: all
+  lean:
+    theorem: Gelu.gelu_le_self_of_nonneg
+    module: ProvableContracts.Gelu
+    status: proved
+    depends_on:
+    - Real.tanh_lt_one
+    mathlib_imports:
+    - Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
+    notes: 'GELU(x) = 0.5·x·(1 + tanh a); since tanh a < 1 (Real.tanh_lt_one) the factor
+      1 + tanh a ≤ 2, and 0.5·x·2 = x for x ≥ 0, so GELU(x) ≤ x.'
 - type: equivalence
   property: SIMD matches scalar
   tolerance: 4.0
@@ -143,6 +209,31 @@ falsification_tests:
   prediction: x1 <= x2 => ReLU(x1) <= ReLU(x2)
   test: proptest with random x1 <= x2 pairs
   if_fails: ReLU implementation not monotonic
+- id: FALSIFY-ACT-007
+  rule: ReLU idempotent
+  prediction: ReLU(ReLU(x)) == ReLU(x) for all x
+  test: proptest with random x
+  if_fails: ReLU not idempotent (double application changes output)
+- id: FALSIFY-ACT-008
+  rule: Leaky-ReLU non-negative branch
+  prediction: x >= 0 => LeakyReLU(alpha, x) == x
+  test: proptest with random x >= 0 and random alpha
+  if_fails: Leaky-ReLU alters non-negative inputs
+- id: FALSIFY-ACT-009
+  rule: Leaky-ReLU negative branch
+  prediction: x < 0 => LeakyReLU(alpha, x) == alpha * x
+  test: proptest with random x < 0 and random alpha
+  if_fails: Leaky-ReLU negative slope not applied
+- id: FALSIFY-ACT-010
+  rule: GELU non-negative on non-negative inputs
+  prediction: x >= 0 => GELU(x) >= 0
+  test: proptest with random x >= 0
+  if_fails: GELU dips below zero for a non-negative input
+- id: FALSIFY-ACT-011
+  rule: GELU bounded by identity on non-negative inputs
+  prediction: x >= 0 => GELU(x) <= x
+  test: proptest with random x >= 0
+  if_fails: GELU exceeds the identity envelope for a non-negative input
 kani_harnesses:
 - id: KANI-ACT-001
   obligation: ACT-INV-001
@@ -196,18 +287,23 @@ qa_gate:
   pass_criteria: All 6 falsification tests pass + Kani verifies ReLU
   falsification: Replace max(0,x) with x to break ReLU non-negativity
 verification_summary:
-  total_obligations: 6
+  total_obligations: 11
   l2_property_tested: 6
   l3_kani_proved: 2
-  l4_lean_proved: 4
+  l4_lean_proved: 9
   l4_sorry_count: 0
   l4_not_applicable: 1
   notes: |
     Analytic obligations proved in verified Lean (0 sorry):
-      - GELU at zero     -> Gelu.gelu_zero       (0.5·0·(1+tanh …) = 0)
-      - SiLU at zero     -> Sigmoid.silu_zero     (0·σ(0) = 0)
-      - ReLU monotonic   -> Elementwise.relu_monotone (max_le_max)
-      - ReLU non-negative-> Elementwise.relu_nonneg    (le_max_left)
+      - GELU at zero                 -> Gelu.gelu_zero                (0.5·0·(1+tanh …) = 0)
+      - SiLU at zero                 -> Sigmoid.silu_zero             (0·σ(0) = 0)
+      - ReLU monotonic               -> Elementwise.relu_monotone     (max_le_max)
+      - ReLU non-negative            -> Elementwise.relu_nonneg       (le_max_left)
+      - ReLU idempotent (relu∘relu)  -> Elementwise.relu_idempotent   (relu_of_nonneg ∘ relu_nonneg)
+      - Leaky-ReLU nonneg branch     -> Elementwise.leaky_relu_of_nonneg (if_pos)
+      - Leaky-ReLU negative branch   -> Elementwise.leaky_relu_of_neg    (if_neg)
+      - GELU ≥ 0 for x ≥ 0           -> Gelu.gelu_nonneg_of_nonneg    (tanh a > -1)
+      - GELU ≤ x for x ≥ 0           -> Gelu.gelu_le_self_of_nonneg   (tanh a < 1)
     Not applicable (runtime/empirical, no algebraic statement):
       - SIMD matches scalar (avx2 vs scalar within 4 ULP) -> fast-math ULP
         equivalence is a hardware/rounding property, not an algebraic identity.
@@ -216,8 +312,13 @@ verification_summary:
         This is a genuine numerical bound between the tanh approximation and the
         exact erf-based GELU; closing it in Lean requires interval/erf bounds we
         have not discharged. Honestly left UNPROVEN rather than marked N/A.
-    Strict leveling: l4_lean_proved(4) + l4_not_applicable(1) = 5 != 6, so this
-    contract is HONESTLY L3 (not L4) until the GELU approximation bound is proven.
+    Strict leveling: l4_lean_proved(9) + l4_not_applicable(1) = 10 != 11, so this
+    contract is HONESTLY L3 (not L4). The sole blocker is the GELU approximation
+    error bound (hard transcendental / interval reasoning). Every other analytic
+    obligation — including the wave-3 additions relu∘relu idempotency, both
+    Leaky-ReLU branches, and the GELU 0 ≤ GELU(x) ≤ x envelope on x ≥ 0 — is
+    machine-checked in Lean with 0 sorry. A truthful L3 with a hardened analytic
+    core, not a faked L4.
 simd_dispatch:
   activation:
     scalar: activation_scalar