This is the piece I said I would write in 0023. It turns two messages into a
table: Roel's two-field answer in 0020 and Kenne's hold on the cross-field
check
in 0021. Nothing here is mine except the pair table, one added column, and
the
problem in section 3, which comes from reading 0024 against 0020.

1. The five states

From Roel, 0020. Two verdict states and three non-verdict ones.

  pass                  the check ran and concluded in the affirmative
  fail                     the check ran and concluded in the negative
  not-exercised    the check never ran
  inconclusive      the check ran and reached no conclusion
  void                   the check ran and its evidence cannot be trusted

The state is what a consumer may conclude and the only field an aggregate
counts. Roel's wording, and the reason "unavailable" moved out of the 1
September text: unavailable is a cause, not a state.

2. The cause vocabulary

Start from CAP-1, draft-hillier-coverage-attestation-00, which defines eight
closed dispositions for a unit left out of the examined count:
not_applicable,
disabled_by_policy, unsupported_input, resource_exhausted, failed,
unavailable,
out_of_scope, withheld. It refuses free text in their place, and its reason
is
worth keeping as ours: "Free-text reasons MUST NOT be accepted in place of a
disposition, because free text does not aggregate."

Three changes to that list for this format.

Roel's gap, 0020: nothing in CAP-1 fits void. Every disposition describes a
unit
that was not examined or not disclosed. Void is a unit that was examined and
whose evidence does not hold up. CAP-1's failed means the unit errored,
which is
closer to inconclusive.

Kenne's seam, 0021, which he credits to Isaac: integrity-failure kept
separate
from availability-failure. A signature that will not verify is a corruption
signal. A key set that cannot be fetched is an operations signal. Collapsing
both into one unavailable-shaped cause loses the difference a reviewer acts
on.

And one this thread produced and no surveyed format has:
precondition-unsatisfiable. The check cannot run because the condition it
tests
cannot exist in any artifact the emitter is allowed to produce. R3 and R8
are
the worked case and the code is in main at 76de05f.

3. The problem 0024 creates, and it is the reason for this message

Roel's rule in 0020: the two verdict states carry evidence references
instead of
a cause. That was right for what the survey covered, which was checks that
did
not run.

Kenne's rule in 0024: a pass is only evidence if you also report whether the
check could have failed.

Both cannot hold. A saturated gate is a pass. Under 0020 a pass carries no
cause, so there is no cell to write the saturation in, and Evgenii's case is
unreportable in the schema we just agreed on. The two cases separate
cleanly:

  foreclosed   the pair (pass, precondition-unsatisfiable) is illegal, so
the
               emitter is forced to not-exercised. The pair table catches
it.
  saturated    state is pass and the pass is true. Nothing catches it.

So I propose the cause field is required on all five states, with two
disjoint
value sets. Verdict causes answer one question: could this check have
produced
the other verdict on some artifact the emitter was allowed to produce?

  counterexample-in-suite     a failing case for this check exists in the
suite
  counterexample-absent       a failing case is constructible, none is
present
  counterexample-impossible   no failing case can be constructed
  not-established             the emitter did not determine which

The referent is the artifact, not the run. That is a choice and it should be
argued: "could have failed" is ambiguous until you say could have failed at
what, and I picked the reading that makes foreclosure detectable.

not-established is the escape value, and it costs what Roel said an escape
should cost in 0020: its own count in the summary, and a run that carries
one
cannot be reported as complete. Not another free-text field. A field gets
filled. What changes behaviour is that the omission is counted where a
reader
sees it.

4. The pair table

Illegal pairs, rejected by the validator. This is the part Kenne said he
would
hold hardest and I agree, so it is written as rejections rather than as
guidance.

  pass  + precondition-unsatisfiable    a check that cannot run did not pass
  pass  + counterexample-impossible     same thing said the other way
  fail  + counterexample-impossible     a check that cannot fail did not
fail
  not-exercised + any verdict cause     a check that did not run has no
                                        counterexample question
  not-exercised + integrity-failure     evidence that was never examined
                                        cannot fail integrity
  void  + not_applicable                a unit that was never examined has
no
  void  + out_of_scope                  evidence that can fail to hold up
  void  + withheld
  non-verdict state with no cause       Roel's rule in 0020, as a rejection
  confinement control that failed while the check ran, with any state but
void
  declared exclusion, with any state but not-exercised

The last two are Roel's, verbatim in intent from 0020.

5. Three worked rows

  R3/R8, disensor, verified in main at 76de05f
    state not-exercised, cause precondition-unsatisfiable.
    Before two fields the tool reported it as covered, because a coverage
count
    sees a vector and stops. The pair table is what makes that report
illegal.

  Evgenii's suite, as reported in 0022
    state pass, cause counterexample-absent or counterexample-in-suite
    depending on the answer to the question in 0023. I am not asserting
which.
    That is the point of the cell: the format makes the emitter answer.

  Guigui's checker, verified by running it, reported in 0011
    a check whose companion file is missing disappears from the count. 40/40
    with the file, 38/38 without, both pass. Under two fields the check is
    not-exercised with a cause, and the denominator stays 40.

6. What this does not settle

The names. I care about the shape, not the words, and counterexample-* is a
placeholder someone should improve.

Whether not-established belongs in the vocabulary at all. It exists because
an
emitter that cannot determine the answer will otherwise pick a wrong value,
and
a wrong value is worse than a declared unknown. If the group thinks a format
should refuse to report rather than report an unknown, that is a defensible
position and it deletes four lines.

XCCDF's Default Model, which Roel read and I have not: he reports it drops
four
values from the count and treats error and unknown like a fail. If that is
right, it is prior art for making a state affect the denominator, and it
should
be a row.

When this stops being right: if an emitter can satisfy the pair table by
always
writing not-established, the table has become decoration. The check is
whether
the count of not-established in published artifacts goes up while the count
of
runs marked complete stays flat. If that happens, the escape needs a harder
cost, not a better name.

I can write the schema fragment and a vector pair per illegal row next, in
the
same shape as the MUST-FAIL vectors already in the thread, so the table is
testable rather than prose.

Nicolás
