Provenance

Every Deep node c-earchin emits records where it came from. The record lives in the .spans.json manifest written alongside the .dp file, and it lets any tool resolve a generated witness back to the exact requirement line that produced it.

The manifest

A span manifest names the source file, a hash of its exact bytes, and one entry per emitted requirement:

{
  "source": "references/finance_options/options_rules.ears",
  "source_hash": "sha256:...",
  "spans": [ ... ]
}

The hash binds the manifest to one specific revision of the source. If the EARS file changes, the hash changes, so a manifest cannot be silently paired with a different version of the requirements it describes.

A span entry

Each entry ties a Deep node to its requirement, and breaks the requirement down into clauses:

{
  "deep_node_id": "req_FIN_003",
  "deep_path": "module.def[2]",
  "ears_id": "FIN-003",
  "ears_file": "references/finance_options/options_rules.ears",
  "ears_text": "WHILE the exchange is open, the portfolio delta shall be at most the limit.",
  "ears": {
    "start_byte": 160, "end_byte": 244,
    "start_line": 3, "start_column": 1,
    "end_line": 3, "end_column": 84
  },
  "clauses": [
    { "kind": "state",    "ears_text": "the exchange is open", "deep_path": "module.def[2].state",    "ears": { ... } },
    { "kind": "system",   "ears_text": "portfolio delta",      "deep_path": "module.def[2].system",   "ears": { ... } },
    { "kind": "response", "ears_text": "be at most the limit", "deep_path": "module.def[2].response", "ears": { ... } }
  ]
}

The fields carry:

• deep_node_id and deep_path: the generated witness, by name and by position in the Deep module.
• ears_id, ears_file, ears_text: the requirement id, its source file, and its full text.
• ears: the source span, as byte offsets and as line and column positions, both start and end.
• clauses: the same provenance, one level finer, for each clause the classifier found. The clause kind is one of trigger, state, condition, feature, system, or response, each mapped to its own deep_path.

How the witness carries provenance too

The Deep file does not depend on the manifest to stay traceable. Each emitted witness also carries its requirement identity inline as metadata:

(def {c_earchin_ears_id: "FIN-003",
      c_earchin_ears_pattern: "state_driven",
      c_earchin_clause_spans: "state:the exchange is open|system:portfolio delta|response:be at most the limit",
      property_source_id: "FIN-003",
      property_source_kind: "bridge:c-earchin",
      span: "req:FIN-003"
      ...}
  req_FIN_003
  ...)

The property_source_id and property_source_kind are canonical Chelis property metadata, so chelis prove records which requirement each property came from. The c_earchin_* fields keep the EARS pattern and clause text attached to the witness itself.

Resolving a failure

When chelis prove reports a failing witness, it uses the manifest to print the requirement instead of the generated node:

property failure: req_FIN_003
  --> references/finance_options/options_rules.ears:3:1 FIN-003
  | WHILE the exchange is open, the portfolio delta shall be at most the limit.

The same resolution is available on its own through explain, which looks up a node id or Deep path and prints its origin:

c-earchin explain references/finance_options/options_rules.spans.json \
  --target req_FIN_003

req_FIN_003 -> references/finance_options/options_rules.ears:3:1 FIN-003
WHILE the exchange is open, the portfolio delta shall be at most the limit.

The line and column come straight from the span entry, so the location a stakeholder reads in the EARS file and the location an engineer reads in proof output are the same location.

The Surf emission format

When c-earchin emits Chelis Surf property source rather than Deep, every emitted file begins with a format marker that the consumer validates:

// c-earchin-surf-emission: v1

A consumer reads this comment to confirm it understands the file before parsing it. A mismatch is a clear error rather than a silent misread.