Fixture staleness clean

The check is fixture_staleness_clean. It is VERIFY-stage. Default severity is warning. It is disabled by default. Enable it with project.checks.fixture_staleness_clean.enabled: true, and list the component in project.verification.fixture_evidence.components. Then the hop asks whether generated fixtures still match the formalization inputs that shaped them. It does not ask whether the files exist. That hop stays on flip fixtures exist for FLIP, and on property fixtures exist for Z3 examples. The instrument stays on MC/DC coverage for Go.

Empty fixture_evidence.components is a pass: no components declare fixture-backed evidence -- fixture staleness not applicable. No tests/ directory is also a pass: no tests/ directory -- fixture staleness not applicable. Those passes are silence, not a freshness proof. A requirements load error, a tests/ path the hop cannot read, or a freshness evaluation that cannot run, is fail: the hop cannot decide whether fixtures are current. When opted-in fixtures no longer match the stored source fingerprint, the hop warns: N requirements have stale fixtures (formalization inputs changed after fixture generation). Retired, superseded, and rejected requirements are not in the active set. Traceability, approval, review, and lifecycle metadata should not be the reason the fingerprint moved.

The expensive miss is a review that treats generated scenarios as part of the pack, then a FRETish edit that never regenerated them. Existence still closes, because the files are still there. The Go suite can still be green, because the samples still union. This hop is the gate that says the files still match the model, or names the requirements whose fixtures drifted.

Typical stale inputs are FRETish text, formalization strategy, component variable definitions, and solver-visible behavior. Hand-editing a generated JSON to silence the checker is not a refresh. Regenerating every component because one requirement moved is not the narrow fix.

# proof.yaml
project:
  checks:
    fixture_staleness_clean:
      enabled: true
  verification:
    fixture_evidence:
      components: [firewall]

# tests/firewall/tc-001.json still exists
# FRETish on SYS-REQ-firewall-quota changed after generation
# proof audit --check fixture_staleness_clean
# 1 requirements have stale fixtures (formalization inputs
# changed after fixture generation)
# warning: the files are older than the model

The fix is to regenerate the fixtures for that component, or to drop the component from the list if they were never a review artifact. For FLIP: proof testgen specs/system <component> --engine heuristic. For Z3 examples: proof proptest specs/system <component> --source z3 --output tests/<component>/. Then re-run VERIFY. Do not copy a sample JSON by hand. A quiet hop after you ignore the warning is still not freshness. The default warning does not block advancement.

proof audit --check fixture_staleness_clean --verbose
proof testgen specs/system firewall --engine heuristic
proof help fixture_staleness_clean

The teaching graph is still one guarantee whose scenario files still exist while the FRETish moved. Close it by regenerating the fixtures, or by removing the component from fixture_evidence.components if they were never a review artifact. Do not edit the JSON by hand to silence the checker. With no opted-in component the empty pass still prints, and the freshness question did not go anywhere. It just was never in scope.

# fixtures regenerated for the opted-in component
# proof testgen specs/system firewall --engine heuristic
# wrote tests/firewall/tc-001.json against the current FRETish

# proof audit --check fixture_staleness_clean
# all declared fixture-backed evidence is up-to-date with requirements
#
# VERIFY is allowed to move on. a pass now sits on a current fingerprint

The existence hop stays on flip fixtures exist. The Z3-example hop stays on property fixtures exist. The instrument hop stays on MC/DC coverage for Go. The rewrite hop stays on characterization testing and mirrors. Jama still authors. Proof vs Jama.

Warning when opted-in fixtures no longer match the formalization fingerprint. Fail when requirements cannot be loaded, when tests/ cannot be read, or when freshness cannot be evaluated, so the hop cannot decide. Empty fixture scope is a pass, not a fail: the hop does not invent freshness. No tests/ directory is a pass, not a fail. Disabled by default: if you never enable it, CI never asks. The hop does not write the JSON. It does not add a shall. It does not prove the Go. It does not run Kind2. It does not measure independence. A quiet hop is not a proof that the authored guarantee is the one you meant, only that every opted-in component has current fixtures, or that none were in scope. It does not say the files exist. That existence hop is flip fixtures exist. It does not say a FLIP row has a matching Verifies: test. That alignment hop is flip_test_alignment. The default warning does not block advancement. We have not scored this floor against a frozen Jama pack or a VectorCAST corpus. The loss is named, not scored.

The existence hop stays on flip fixtures exist. The Z3-example hop stays on property fixtures exist. The rewrite hop stays on characterization testing and mirrors. The engagement stays on software correctness audit. Jama still authors.

What is fixture staleness clean? Same question. Same URL.

Is this flip fixtures exist? No. That hop is whether opted-in tc-*.json files exist. This hop is whether existing files still match the formalization. See flip fixtures exist.

Is this property fixtures exist? No. That hop is whether opted-in Z3 examples exist. This hop is freshness for the files you already generated. See property fixtures exist.

Is this MC/DC coverage? No. That hop is whether each condition independently affects the decision. This hop is whether generated evidence is still current. See MC/DC coverage for Go.

Is this characterization testing? No. That page is rewrite-with-a-ledger. This hop is generated-fixture freshness for a listed component. See characterization testing and mirrors.

Is this flip test alignment? No. Alignment is whether a FLIP row has matching source-native Verifies: tests. This hop is whether the generated files still match the model.

Does a quiet hop prove the Go matches the shall? No. The hop observes fingerprints. It does not prove the Go.

Does empty fixture_evidence fail this hop? No. That is a pass. A pass with nothing in scope is not freshness.

Does no tests/ directory fail this hop? No. That is a pass: fixture staleness is not applicable. Existence is the hop that cares whether tests/ is a directory.

Does a stale fixture fail the merge? No. The check keeps warning severity unless you raise it in proof.yaml.

Is Proof an LDRA alternative for the instrument? No. LDRA still owns the avionics toolchain. Proof vs LDRA.

Is Proof a Jama alternative for the shall? No. Jama still authors. Proof vs Jama.