Skip to content

Cross-attestation dependencies need first-class RDF, not narrative prose ('numerical adequacy depends on symbolic adequacy') #34

@mzargham

Description

@mzargham

Surfaced by

UAT walkthrough of the engineer skill against the ADCS arc, while
authoring the second of two AdequacyAttestations for REQ-001 (one per
behavioral model — symbolic + numerical). The numerical adequacy
claim contains a critical dependency:

"Critical complementarity note: this numerical adequacy claim
DEPENDS ON the symbolic adequacy claim — the simulator measures
settling time given convergence, but convergence is what the
symbolic analysis is supposed to establish. The two lines are NOT
redundant; they are complementary. If the symbolic adequacy is
deprecated, this numerical adequacy must be re-judged."

That dependency is load-bearing for the audit story — if the
symbolic adequacy is later deprecated (e.g., the linearization regime
turns out not to hold for the satellite's actual mass distribution),
the numerical adequacy MUST automatically fall too. But the
dependency is currently captured ONLY in prose rdfs:comment text.
SPARQL can't query "what attestations depend on this one?"; the
deprecation flow can't auto-propagate.

The class of dependency

Several kinds of cross-attestation dependency arise in real
engineering:

  1. Definitional dependency — A's claim makes no sense without B.
    ("The settling-time measurement makes no sense unless convergence
    is established.")
  2. Evidentiary dependency — A's reasoning relies on B's
    conclusion. ("The sufficiency claim cites the adequacy claim as
    premise.")
  3. Cumulative-reasoning dependency — A is downstream of B in a
    chain of derived attestations (e.g., a SatisfactionAttestation
    synthesizing Adequacy + Sufficiency).
  4. Temporal/PROV dependency — A was authored after B and
    informed by it. (This one is partly captured by
    prov:wasInformedBy in the transcript surface; not yet
    surfaced for attestations specifically.)

All four matter for audit propagation. Today none are queryable.

Why this matters

Specifically: the deprecation flow (which is the framework's
main correctness mechanism for evolving judgements) operates
attestation-by-attestation. When the engineer deprecates A, the
audit-side can detect "A is invalidated" via the
prov:wasInvalidatedBy triple — BUT the audit can't automatically
detect that B (which depended on A) is now in a structurally
suspect state.

Concrete failure mode: an adopter deprecates the symbolic adequacy
attestation. The audit reports "1 deprecated attestation." It does
NOT report "and 4 downstream attestations are now potentially
invalid because they depended on it." The auditor has to read every
attestation's prose to spot the dependency chain.

For complex requirement structures (a satellite cert might involve
50+ attestations across model + evidence + composition layers), this
is unmanageable.

Vocabulary candidates

A — rtm:dependsOn (attestation → attestation)

<urn:rtm:attest/numerical-adequacy>
    a rtm:AdequacyAttestation ;
    rtm:dependsOn <urn:rtm:attest/symbolic-adequacy> ;
    ... .

Pros: simple; queryable; SHACL profiles can demand "if A depends on
B and B has prov:wasInvalidatedBy, then A must also have
prov:wasInvalidatedBy OR a status of deferred."

Cons: doesn't distinguish the dependency KIND (definitional vs
evidentiary vs cumulative).

B — Multiple predicates by dependency kind

<urn:rtm:attest/numerical-adequacy>
    rtm:isDefinedAgainst <urn:rtm:attest/symbolic-adequacy> .

<urn:rtm:attest/sufficiency-req-001>
    rtm:premisedOn <urn:rtm:attest/numerical-adequacy>,
                   <urn:rtm:attest/symbolic-adequacy> .

<urn:rtm:attest/satisfaction-req-001>
    rtm:synthesizes <urn:rtm:attest/sufficiency-req-001>,
                    <urn:rtm:attest/adequacy-...> .

Pros: richer audit; per-kind propagation rules possible.

Cons: more vocabulary; need to draw the predicate lines carefully.

C — PROV-aligned via prov:wasInformedBy

PROV has prov:wasInformedBy for activity→activity chains. If
attestations are typed as prov:Activity (which they aren't in
v0.1, but could be via multi-typing), the existing transcript
infrastructure trivially extends.

Pros: zero new vocabulary; standards-aligned; the transcript's
chain-of-reasoning machinery already replays via prov:wasInformedBy.

Cons: prov:wasInformedBy doesn't distinguish dependency kind;
implicit semantic stretch (attestations as Activities is meaningful
but not the only modeling choice).

D — GSN promotion

GSN's gsn:supportedBy, gsn:inContextOf, gsn:hasJustification
are precisely the predicates for argument structure between
attestations. Adopting them would resolve #29-#33

Pros: standards-aligned; one consistent framework for ALL the
engineering-precondition + cross-attestation vocabulary work.

Cons: heaviest spec move; parsimony budget; adopters need to learn
GSN.

SHACL propagation rule (sketch)

Once vocabulary lands, the audit-side gets a SHACL closure rule
along the lines of:

rtm:DeprecationPropagationShape a sh:NodeShape ;
    sh:targetClass rtm:Attestation ;
    sh:rule [
        a sh:SPARQLRule ;
        sh:construct """
            CONSTRUCT { ?downstream rtm:hasPotentialDeprecation ?upstream }
            WHERE {
                ?upstream prov:wasInvalidatedBy ?activity .
                ?downstream rtm:dependsOn ?upstream .
                FILTER NOT EXISTS { ?downstream prov:wasInvalidatedBy ?any }
            }
        """ ;
    ] .

The audit then surfaces rtm:hasPotentialDeprecation as a finding
class — "these N attestations depend on M deprecated ones and may
themselves be invalid; the engineer must review and either re-judge
or deprecate."

Coupling

  • #29-#32 (precondition vocabulary + adequacy/sufficiency partition + temporal partition + model/evidence partition)
  • #33 (content-addressed reasons)
  • ADCS prototype future-work item What does sysml mean here #5 (multi-attestation aggregation
    policy as SHACL)

GSN promotion (option D) is the unifying direction across all of
these.

Impl-side follower

Once vocabulary lands:

  • Engineer skill's attest catechism gains a question: "Does this
    attestation depend on any prior attestation? If yes, name them."
  • Constructor CLI's attest gets a --depends-on <iri> flag
    (repeatable).
  • Auditor skill's read-only walk surfaces dependency chains and
    potentially-affected attestations as findings (per the SHACL
    closure rule sketch above).
  • Reconcile skill propagates: when a reconciliation decision
    invalidates an upstream attestation, the dependency chain
    surfaces for cascading deprecation decisions.

What the in-flight UAT is doing

Recording the dependency in rdfs:comment prose text (visible to a
human reader; not queryable). The walkthrough proceeds without
structural dependencies; if/when the symbolic adequacy is later
deprecated, the engineer skill will have to manually trigger
re-judgement of the numerical adequacy (a human catches what the
system should catch automatically).

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions