test: add executable safety verification envelope

[tarang-tj]

Part of #212.

Why

The risk scorer assigned diminishing weights by analyzer output order. The first revision exposed that equal-severity permutations could change the final score: CRITICAL confidence 0.01 followed by 1.0 scored 25, while the reverse order scored 50.

The verification envelope then found a stronger counterexample in the severity-first fix: a HIGH finding at confidence 0.1 scored 2, but adding a CRITICAL finding at confidence 0.01 lowered the score to 1 because the weaker finding took the full-weight slot.

Severity-first allocation and global evidence monotonicity cannot both hold when confidence varies and each rule has a fixed, capped sequence of diminishing weights. This draft orders occurrences by their unweighted score contribution (severity points x confidence x executable multiplier), so the largest contributions receive the largest weights. Severity remains represented in the base points.

What changed

• order same-rule findings by unweighted score contribution, making scoring permutation-invariant and monotone under additional non-negative evidence
• add an independent executable risk reference model that imports no production scoring constants or helpers
• use Hypothesis differential properties for score equivalence, bounds, floors, provenance, banding, permutation invariance, and arbitrary-evidence monotonicity
• use adversarial-oracle properties to ensure arbitrary valid LLM outcomes cannot remove or weaken deterministic findings
• include fixed regressions for both historical ordering failures
• document what S1/S2 verify—and explicitly what semantic LLM behavior they do not
• add a fast make verify target

The production change remains deliberately narrow: deterministic weight allocation inside a rule. The rest is executable specification and test scaffolding.

Verification

• uv run make verify: 7 passed (including 500 generated arbitrary-evidence monotonicity examples)
• focused scoring/verification suite: 106 passed
• uv run make test-unit: 3,167 passed, 14 skipped, 38 deselected, 4 xfailed
• uv run make lint
• uv run make format-check
• uv run mypy src/skillspector/nodes/report.py tests/verification
• git diff --check

This stays draft while maintainers decide whether the Phase 1 contract in #212 is the right boundary and whether the production scoring behavior ruling should remain in the same PR.

[tarang-tj]

Verification-envelope update: the generalized monotonicity property found a second scoring counterexample in my first fix. With same-rule evidence, HIGH@0.1 scored 2 alone, but adding CRITICAL@0.01 reduced it to 1 because severity-first ordering gave the weaker numeric contribution the full-weight slot.

Head 3d50958 now allocates the fixed diminishing weights by each finding’s unweighted contribution (severity points × confidence × executable multiplier). This preserves severity in the base score while making the result permutation-invariant and monotone under arbitrary additional non-negative evidence. I added both a fixed regression and a 500-example generalized property, updated the independent reference model and contract docs, and reran the full unit suite: 3,167 passed, with expected skips/xfails. The PR remains draft for the Phase 1 behavior ruling.