Verification

Verification: Ensuring Invariants and Stability in Compitum Loops

Quick-Scan Infobox

Aspect	Details
Target User	Educators validating class tools, developers confirming extensions; pytest basics assumed.
Core Goal	Arm you with test suites, coverage gates, and CI flows to prove Compitum's bounded invariants—e.g., ΔE ≤0, feas true.
Time to First Run	2 mins: pytest -q → Green for core, flags for routerbench.
Key Analogy	Like a safety inspection: Markers as checklists (invariants pass?), coverage the full scan (100% no shadows), CI the automated patrol.
Gate Threshold	Fail <100% src cov; invariants must hold ∀ traces.

Core Principles Layer (Technical Backbone)

Verification in Compitum enforces mechanistic guarantees: Pytest suites assert invariants (e.g., ∀t, ΔE_t ≤0 ∧ slacks ≥0 via @pytest.mark.invariants), property-based tests (hypothesis lib) gen edge cases (e.g., infeas b with shadows>0), coverage via pytest-cov enforces 100% on src (pyproject.toml: fail_under = 100). Markers modularize: -m invariants for Lyapunov V descent, -m routerbench for optional benches (e.g., boundary flags <5% false pos). CI yaml orchestrates ruff (lint), mypy (types), pytest (tests)—runs on PRs, gates merges. Locally mirrors: Sequential checks ensure repro, tying to traces (e.g., assert cert['feasible'], unpack via Output-Format). Invariants formal: For quadratic space, ∀x feas, d_M(x,μ) ≤ r_t ∧ H(p) ≤ log k (no collapse).

• Test Structure: Unit: Mock router.route() → assert U <0; Prop: Rand prompts → 95% feas.
• Coverage Config: pyproject.toml [tool.coverage.run] source=src, omit=tests/*—fails builds under thresh.
• CI Flow: .github/workflows/ci.yml: Matrix Python 3.10-3.12, jobs: lint → type → test → cov report.

Why verify? Bounded proofs: Tests as observer queries on code space, coverage as constraint feas—emergent trust from local checks, no runtime gambles.

Code Dive: Invariant Test Snippet (Collapsible for Tinkerers)

Open on GitHub | Open in nbviewer | Launch in Binder

Snippet from Verification.md

# Adapted from tests/invariants/test_invariants_energy.py (real file, mocked deps)
import pytest
import numpy as np
from unittest.mock import MagicMock
from compitum.energy import SymbolicFreeEnergy
from compitum.predictors import CalibratedPredictor
from hypothesis import given, strategies as st

@pytest.mark.invariants
def test_utility_improves_with_quality():
    energy_func = SymbolicFreeEnergy(alpha=0.4, beta_t=0.2, beta_c=0.15, beta_d=0.15, beta_s=0.1)
    mock_metric = MagicMock()
    mock_metric.distance.return_value = (1.0, 0.1)  # (d, sigma)
    mock_coherence = MagicMock()
    mock_coherence.log_evidence.return_value = 0.0
    mock_model = MagicMock()
    mock_model.cost = 0.0
    mock_predictors = {
        "quality": MagicMock(spec=CalibratedPredictor),
        "latency": MagicMock(spec=CalibratedPredictor),
        "cost": MagicMock(spec=CalibratedPredictor),
    }
    for p in mock_predictors.values():
        p.predict.return_value = (np.array([0.5]), np.array([0.4]), np.array([0.6]))

    U_t, _, _ = energy_func.compute(np.zeros(1), mock_model, mock_predictors, mock_coherence, mock_metric)

    # Improve the quality predictor's forecast; utility should not decrease
    mock_predictors["quality"].predict.return_value = (np.array([0.9]), np.array([0.8]), np.array([1.0]))
    U_tp1, _, _ = energy_func.compute(np.zeros(1), mock_model, mock_predictors, mock_coherence, mock_metric)

    assert U_tp1 >= U_t, "Utility should not decrease when quality improves"

@given(st.lists(st.floats(min_value=0, max_value=1), min_size=2))
def test_feas_slack_nonneg(utilities):
    # Prop: Sorted utils -> gap >=0
    sorted_u = np.sort(utilities)[::-1]
    assert sorted_u[0] >= sorted_u[1], "Gap negative-infeas order"

Pro Tip: Run targeted: pytest -m invariants --cov=src/compitum --cov-report=term-missing—spots gaps.

Approachable Layer (Relatable Hooks for Educators)

Verification's the "pre-flight" for your lessons: Pytest as the walk-through ("Invariants green? No drift surprises"), coverage the full inventory ("All quadratic paths checked?"), CI the auto-grader keeping it fair. No gatekeeping—run local for quick "does this edu config hold feas?" checks, tying traces to "what if" probes. For classrooms, it's reliability ritual: Green suites mean safe sim deploys, markers as modular "unit quizzes"—teach kids to assert "ΔE descent" like self-correcting proofs, echoing Montessori's error controls without the red pen.

• Classroom Tie-In: @pytest.mark.routerbench for group evals—batch traces, assert <1% violations, discuss "shadow spikes" as constraint convos.
• Analogy Echo: Ruff/mypy as spell-check: Lint catches indents, types the "promise keepers."
• Common Hurdle: Cov <100%? --cov-branch for paths; focus src first.

Quick-Reference Toolkit (Commands & Markers)

Command	Purpose	Markers/Options	Expected	When
pytest -q	Unit/prop tests.	-m invariants (core); -m routerbench (benches).	Green dots, %pass.	Daily dev.
ruff check .	Lint code.	--fix auto.	No violations.	Pre-commit.
mypy src/compitum	Type check.	--strict.	No errors.	PR gate.
pytest --cov=src/compitum	Coverage report.	--fail-under=100 --cov-report=html.	100% src.	Release prep.
act	Local CI sim.	Mirrors .github/workflows/ci.yml.	Workflow pass.	Offline test.

Gotchas Table (Collapsible: Verify Snags)

Issue	Symptom	Fix	Analogy
Cov Drop	<100% on src.	Add tests for missed branches; --cov-append.	Patch hole—full seal.
Marker Miss	-m invariants skips.	@pytest.mark.invariants on defs.	Wrong label—retag.
CI Flake	Green local, red PR.	Seed rand: np.random.seed(42).	Windy test—anchor.
Type Ignore	Mypy warns on stubs.	Inline # type: ignore; fix upstream.	Temp scaffold—reinforce later.

Next Steps: Your Loop

• Run a Suite: pytest -m invariants—all green? Add a prop test.
• Cov Hunt: --cov-report=html → browser gaps, patch one.
• CI Local: act your branch—mimic the gate.

See also: Output-Format for trace asserts; Trace-Glossary for signal tests; Cookbook for pytest recipes; Roadmap for bench milestones.