CoBOMs, context, and provenance

[deeglaze]

After context initialization, additional inputs are held back until appraisal processing has completed.
[...]
8.3.1.1 CoRIM Selection
All available CoRIMs are collected.

and

6. CoBOM
   If a Verifier Owner has a policy that does not require CoBOM, tags within a CoRIM received by a Verifier are activated immediately and treated valid for appraisal.

These two pieces are at odds with one another I think. At the very least this should be "valid for future appraisal sessions".
I don't know what it means for the Verifier Owner policy to require CoBOM. Does it need appraisal requests to provide CoBOM tags to guide tag selection? Is this only for ingesting tags prior to an appraisal? Why is that an interaction we are specifying?

After context initialization, additional inputs are held back until appraisal processing has completed.

I think this text still leaves a window for state mutation to muddle things. We ought to say that the input state to context construction is also fixed at the start of an appraisal session.

The primary goal of this phase is to ensure that all necessary information is available for subsequent processing.

Given that there are apparently different Verifier interactions that change the available information to construct the input context, we have a few entry points to the imagined Verifier. Perhaps we can simplify this to just the theory of appraisal of evidence and say the goal of context construction is to have a well-defined set of inputs for describing attestation appraisal as determined entirely by its inputs.

Wonk follows

Immediacy is not meaningful in distributed systems and leads to problems with tracking provenance. We haven't really described the difference between a Verifier receiving a CoRIM and performing an attestation appraisal. I don't think we want to draw the distinction and instead treat the initial state as an immutable input.

Right now we have the ECT and ACS internal representations, but not an abstract machine. Since evs can fail to match the ACS at one point in time and then succeed after a different triple has been processed, we ought to describe the semantics as a fixed-point computation.

I think we're not meant to be talking about interactions between services in this specification. Instead we are describing a document format and its meaning for attestation appraisal. Perhaps we can say there are internal representations of inputs,

• initial state available to construct an appraisal context [e.g., a versioned database]
• time used for validity-checking
• evidence submitted for appraisal

and an internal representation of an appraisal state that includes the ACS,

• appraisal context as constructed for a session

Each of the triple's internal representations correspond to a cm-type, so let's make a tagged union.

ctx-triple = {
  val: rv / es / evs / policy
  cmtype: cm-type
]
context = {
  todo: [ ctx-triple ]
  acs: ACS
  session: any
}

A context transition is therefore a selection of a triple to process, where a selection strategy already determined the order of processing, an ACS addition (if any), and a session state update (if any).

step({todo: [ triple, todo ... ], acs: ACS, session: session}) = {
  todo: [ todo ... ]
  acs: ACS-next
  session: session-next
}
where
ACS-next, session-next = process-triple(triple, session)
}

step({todo: [], acs: ACS, session: session}) = final-phases(ACS, session)

We've defined process-triple for all the internal triple types and described final-phases as optional.

Finally,

appraise(initial-state, evidence, time) = appraise-internal(ctx)
  where ctx = construct-context(initial-state, evidence, time)

construct-context(initial-state, evidence, time) = {
  todo: tag-selection(initial-state, evidence),
  acs: valid-evidence(initial-state, evidence, time)
  session: verifier-session-new()
} 
appraise-internal(context) = leastfixedpoint(step)(context)

The tag-selection MAY take evidence into account to narrow the active tags further from its initial state to tags hinted at from evidence.
The valid-evidence function is effectively phase 2.

[deeglaze]

I'd generally like for appraise to be able to provide a summary of its inputs in its results for provenance's sake, but we can leave that out of this spec.

[deeglaze]

Attempted to handle this a bit in PR#307.