trevon/brick
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
brick/docs/architecture/p4-evidence.md

4.7 KiB
Raw Permalink Blame History

P4 evidence adapter contract

Brick imports P4 compiler evidence through a tool-specific envelope. It does not parse an assumed generic verifier format and does not route P4 evidence through the Fold adapter.

Qualified adapter

The only enabled contract in schema version 1 is:

Field Required value
adapter p4c-diagnostics
tool.name p4c
tool.version 1.2.5.16
invocation.mode p4test-regression
evidence lane imported

This narrow mode represents a structured transcription of p4c's checked-in P4_16 regression diagnostics. It is compiler evidence, not a proof. A different p4c version or command mode requires a separately captured real artifact and a contract update before Brick will import it.

Use the adapter while building a graph:

cargo run -- build tests/fixtures/p4c \
  --p4c-report tests/fixtures/p4c/reports/p4c-1.2.5.16-duplicate-state.json \
  --json p4c.brick.json --html p4c.brick.html

Brick-owned envelope

The versioned JSON envelope records producer and raw-artifact identity rather than trying to infer fields from diagnostic prose:

{
  "schema_version": 1,
  "adapter": "p4c-diagnostics",
  "tool": { "name": "p4c", "version": "1.2.5.16" },
  "invocation": { "mode": "p4test-regression" },
  "artifact": {
    "identity": "git-blob:<upstream blob id>",
    "provenance": "https://raw.githubusercontent.com/...p4-stderr"
  },
  "exit_status": 1,
  "results": [
    {
      "raw_identity": "producer-local stable identity",
      "category": "error",
      "code": "duplicate",
      "message": "producer message",
      "path": "repository-relative source path",
      "line": 5,
      "column": 9,
      "symbol": { "kind": "state", "name": "start", "owner": "p" },
      "model_bounds": null,
      "confidence_category": null
    }
  ]
}

category is limited to the qualified error and warning values. p4c does not define verifier model bounds or a confidence category for this diagnostic contract, so both fields must be explicit null. A non-null value is rejected rather than upgraded to symbolic evidence.

Paths are normalized lexically across /, \\, ., and ... Absolute paths must remain under the model's scan root. Brick first resolves an exact path/kind/name/owner/line symbol and otherwise attaches a valid diagnostic to the matching file with a resolution diagnostic. Missing files, escaping paths, unknown categories or symbol kinds, malformed records, unsupported versions, and unsupported tools import no affected result. Exact duplicates merge evidence; records that reuse one raw identity with different payloads are all rejected, independent of report order. A hash collision with a finding owned by another adapter preserves the foreign finding and rejects the P4 record.

Accepted findings retain the tool version, command mode, result category, result code, exit status, raw identity, artifact identity/provenance, source column, explicit null bounds/confidence, and an Imported evidence record. The Flags edge uses domain = "p4" and p4.relation = "compiler-diagnostic". Findings do not alter structural-health components.

Real fixture provenance

The checked-in source and stderr fixture are byte-identical to p4c tag v1.2.5.16:

  • source: testdata/p4_16_errors/decl-parser-with-duplicate-state-names.p4, Git blob 301a00817456db2e26eec8952e6868c0b82960e0;
  • diagnostic: testdata/p4_16_errors_outputs/decl-parser-with-duplicate-state-names.p4-stderr, Git blob d3b4f87b035dbddba726b3c376da415dd9df5766;
  • version source: p4c Version.txt at tag v1.2.5.16 contains 1.2.5.16.

Upstream URLs:

Brick's fixture test also checks the structured attachment and imported evidence contract; the raw files can be independently checked with git hash-object.

Disabled symbolic adapters

p4v, p4-symbolic, bf4, and p4k remain disabled because no qualified, maintained, versioned machine-readable findings contract was verified. The public p4_evidence::adapter_status(tool, version, mode) interface reports that missing prerequisite and enables p4c only for the qualified tuple. It does not define placeholder JSON for those tools.

BMv2 JSON remains a target artifact, p4c-graphs remains imported compiler structure, and P4Testgen output remains generated test evidence. None is accepted as a symbolic finding by this adapter.