Flip fixtures exist

The check is flip_fixtures_exist. It is VERIFY-stage. Default severity is warning. It is disabled by default. Enable it with project.checks.flip_fixtures_exist.enabled: true, and list the component in project.verification.fixture_evidence.components. Then the hop asks whether FLIP scenario files exist. It does not measure independence. The instrument stays on MC/DC coverage for Go. The Z3-example hop stays on property fixtures exist.

Empty fixture_evidence.components is a pass: no components declare fixture-backed evidence -- FLIP fixtures not applicable. Opted-in components with no FLIP-eligible requirement (no FRETish, or not a guarantee) is also a pass: no declared fixture-evidence components have FLIP-eligible requirements -- FLIP fixtures not applicable. Those passes are silence, not a scenario set. Retired, superseded, and rejected requirements are not in the active set. A requirements load error, or a tests/ path that is not a directory, is fail: the hop cannot decide whether fixtures apply. Zero tc-*.json under an opted-in component with formalized guarantees is warning: N formalized reqs across M components, K components missing FLIP fixtures.

The expensive miss is a review that treats generated scenarios as part of the pack, then CI that never wrote them. The audit then reports that coverage was fine, because the instrument hop closed, or because this hop never ran. This hop is the gate that says the scenarios exist, or names the components that still have none.

This is not whether the Go decision was independently covered. That hop is MC/DC coverage for Go. A 100% MC/DC report can still have zero tc-*.json files. The help file teaches that first.

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

# tests/firewall/ is empty
# proof audit --check flip_fixtures_exist
# 1 formalized reqs across 1 components, 1 components missing
# FLIP fixtures
# missing: firewall (1 reqs)
# warning: the scenarios were never generated

The fix is to generate the scenarios, or to drop the component from the list if they were never a review artifact. Run proof testgen specs/system <component> --engine heuristic. Then re-run VERIFY. Do not copy a sample JSON by hand to silence the checker. A quiet hop after you ignore the warning is still not a fixture set. The default warning does not block advancement.

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

The teaching graph is still one guarantee whose Go report was green while tests/firewall/ stayed empty. Close it by generating the scenarios, or by removing the component from fixture_evidence.components if they were never a review artifact. Do not add another sample only to silence the checker. With no opted-in component the empty pass still prints, and the scenarios did not go anywhere. They just were never in scope.

# scenarios generated for the opted-in component
# proof testgen specs/system firewall --engine heuristic
# wrote tests/firewall/tc-001.json

# proof audit --check flip_fixtures_exist
# 1 FLIP fixtures across 1 components (1 formalized reqs)
#
# VERIFY is allowed to move on. a pass now sits on files

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

Warning when opted-in FLIP-eligible guarantees have no tc-*.json. Fail when requirements cannot be loaded, or when tests/ is not a directory, so the hop cannot decide whether fixtures apply. Empty fixture scope is a pass, not a fail: the hop does not invent scenarios. 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 scenario files, or that none were in scope. It does not say the fixtures still match the FRETish. That freshness hop is fixture_staleness_clean. 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 instrument hop stays on MC/DC coverage for Go. 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 flip fixtures exist? Same question. Same URL.

Is this MC/DC coverage? No. That hop is whether each condition independently affects the decision. This hop is whether opted-in scenario files exist. See MC/DC coverage for Go.

Is this property fixtures exist? No. That hop is Z3 examples as z3-*.json. This hop is FLIP scenarios as tc-*.json. See property fixtures exist.

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

Is this fixture staleness? No. Staleness is whether existing files still match the formalization. This hop is whether the files exist at all.

Does a quiet hop prove the Go matches the shall? No. The hop observes files. 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 a fixture set.

Does missing tc-*.json 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.