brick/docs/research/gap-remediation-scope.md

# Verified gap-remediation scope

Status: baseline contract for Workflow 2, revision 2
Snapshot date: 2026-09-01

This document corrects the supplied Brick review and fixes the scope of the
remediation workflow. It is not an implementation claim. Later phases must
replace these decisions only with cited source, fixtures, and a workflow
revision.

## Current baseline

Brick's current public boundary is schema-versioned JSON. The renderer and CLI
consume that model; they do not define analysis correctness.

Verified repository facts:

- `src/model.rs` defines seven node kinds and six edge kinds.
- `src/scan.rs::language_for` recognizes six grouped language families through
  several extensions and seven internal labels. It does not recognize `.p4`.
- `src/fold.rs` imports Fold native findings JSON and SARIF findings. It does
  not import Fold call graphs or fact IDs.
- `brick check` already gates score, cycle count, and unresolved dependencies.
  There is no separate `gate`, `diff`, policy-file, MCP, P4, or tree-sitter
  implementation.
- Tree-sitter remains roadmap work. The current extractor is regex-based.
- Each edge stores one `Evidence`, and lexical edge deduplication uses only
  `(source, target, kind)`. The current model therefore cannot retain parallel
  lexical and tree-sitter evidence for one relationship.
- Symbol identities currently include source line number. They are
  deterministic for one file snapshot but are not stable under unrelated line
  insertions, so they are not yet suitable for structural drift claims.
- Missing Fold backend values currently default to `source`; a `source` backend
  is then labeled `Symbolic`. Unknown confidence strings become `0.25`. These
  behaviors conflict with the repository rule that unknown wire values remain
  unknown or produce diagnostics.

Baseline commands and observed results:

| Command | Result |
| --- | --- |
| `./scripts/quality-gate.sh` | exit 0; formatting, Rust tests, Clippy, and benchmark self-test passed |
| `cargo test -- --list` | 10 Rust tests, 0 benchmarks |
| `python3 -m unittest tests.benchmarks.test_runner -v` | 3 tests passed |
| `python3 tests/benchmarks/runner.py self-test` | passed as part of the quality gate |

The supplied statement `cargo test: 16 passed` is false for this snapshot. The
statement that all ten Rust tests pass is supported by the recorded run.

## Corrected concern ledger

| Concern | Decision |
| --- | --- |
| P4 support | Valid gap. Split it into model/identity, syntax extraction, compiler/verifier adapters, and P4-specific metric semantics. |
| P4 concepts | Do not silently equate parser/control/table/header with class or state/action with function. The model phase must retain the exact P4 kind, nesting, and relation even if a coarse display kind is also supplied. |
| Formal verification | Do not treat compiler success, BMv2 JSON, GraphViz output, generated tests, or an imported warning as proof. Symbolic means proved within the named tool's bounded model. |
| Tree-sitter | Valid roadmap direction. It is another syntax backend, not a symbolic lane and not grounds to upgrade lexical confidence. Start with one disabled-by-default pilot. |
| Parallel evidence | Required before running lexical and tree-sitter together. Preserve both producers deterministically instead of first-writer-wins deduplication. |
| Stable drift | Required before `diff`. Remove volatile line numbers from canonical symbol identity and define schema/root/scope compatibility. |
| Policy | Valid roadmap direction. Extend `brick check`; do not create a second divergent gate command. Policy evaluates graph evidence but does not change extraction truth. |
| MCP | Valid roadmap direction. Build a reusable read-only query API first, then a thin stdio MCP adapter. MCP must not reimplement P4 metrics or depend on Cytoscape. |

## P4 scope and external-tool decisions

### Dialect

The first supported dialect is **P4_16**. P4_14 is a later compatibility phase,
not an alias for P4_16. P4C can translate some P4_14 programs to P4_16, but a
translation is imported tool evidence and must not be presented as native P4_14
coverage.

The initial P4_16 fixture set will use the v1model architecture because it is
covered by the reference compiler and provides concrete parser, control, table,
action, header, and state examples. Architecture-specific semantics must be
attributes/provenance, not universal P4 facts.

### Reference compiler

Pin integration fixtures to **p4c v1.2.5.16**. P4C documents that:

- `p4test` checks P4_16/P4_14 syntax and writes diagnostics to ordinary output;
- `p4c --target bmv2 --arch v1model` writes JSON expected by BMv2;
- `p4c-graphs` writes GraphViz `.dot` parser/control graphs; and
- P4Testgen symbolically explores programs to generate tests.

None of these artifacts is a generic formal-verification findings JSON format.
The first evidence bridge may capture versioned p4c diagnostics and exit status
in a Brick-owned envelope. These are `Imported`, not `Symbolic`. BMv2 JSON is a
target artifact and is out of scope as a finding feed. P4Testgen test cases may
later become runtime/test evidence, but test generation alone is not a proof
finding.

Sources:

- <https://github.com/p4lang/p4c/releases/tag/v1.2.5.16>
- <https://github.com/p4lang/p4c/blob/main/README.md>
- <https://github.com/p4lang/p4c/tree/main/backends/p4tools/modules/testgen>

### Tree-sitter grammar

The pilot candidate is **`duskmoon314/tree-sitter-p4`**, pinned to an exact
commit during the pilot. It has MIT licensing, Rust bindings, P4_16 scope, CI,
and a claimed 119/121 parse result on official Tofino examples. That claim is
not Brick evidence until Brick reproduces it and adds clean negatives.

`oxidecomputer/tree-sitter-p4` remains the comparison candidate. It is
MPL-2.0, describes itself as early-stage, and its current main commit is
`ec27f5123d4f80ced59302820bec3e212794132f`. Neither grammar is approved as a
default frontend at baseline. The selected grammar remains experimental and
disabled by default until the three-repeat pilot passes accuracy, determinism,
license, and performance gates.

Sources:

- <https://github.com/duskmoon314/tree-sitter-p4>
- <https://github.com/oxidecomputer/tree-sitter-p4>

### Formal verifier qualification

No maintained, machine-readable P4 verifier findings contract was verified for
P4V, `p4-symbolic`, bf4, or P4K during baseline research.

- bf4 is a V1Model-focused Z3 analysis backend whose documented interface is
  log text. Its repository was last pushed in 2022.
- P4K provides formal semantics and symbolic execution, but its public
  repository was last pushed in 2021 and does not provide the report contract
  assumed by the supplied review.
- P4Testgen is maintained with p4c, but generates tests rather than a findings
  report.

The verifier-adapter phase therefore has a qualification gate:

1. accept only a named tool version with a checked-in real output fixture and a
   documented result schema;
2. otherwise implement only the versioned Brick evidence envelope and p4c
   diagnostic bridge;
3. keep the unsupported symbolic adapter disabled and document the missing
   prerequisite;
4. never fabricate a P4V or `p4-symbolic` JSON schema.

Sources:

- <https://github.com/dragosdmtrsc/bf4>
- <https://github.com/kframework/p4-semantics>

## Producer, fact, lane, and confidence contract

This table is the baseline contract. The model phase may refine representation,
but may not weaken the evidence boundary.

| Producer and fact | Lane | Confidence rule | Required provenance |
| --- | --- | --- | --- |
| Filesystem containment | Syntactic | exact observation | scanner version and repository-relative path |
| Lexically recognized declaration shape | Syntactic | backend-specific category; not a universal probability | `brick-lexical`, path, line |
| Lexical call/import/inheritance candidate or name resolution | Heuristic | retain original producer category when a name resolves | `brick-lexical`, path, line, resolution mode |
| Tree-sitter declaration or syntax relationship | Syntactic | grammar/backend-specific category | grammar repository, pinned commit, query version, path/range |
| Tree-sitter/name-index target resolution | Heuristic unless a compiler proves it | no upgrade merely because exactly one name matched | syntax evidence plus resolver/version |
| p4c compile diagnostic | Imported | exact severity/category from p4c; no synthetic probability | p4c version, command mode, raw artifact, path/range |
| p4c-graphs structure | Imported | structural compiler artifact, not proof | p4c version, command, `.dot` artifact |
| External analyzer warning | Imported | producer category retained verbatim | tool/version/report/result identity |
| Bounded verifier proved result or concrete counterexample | Symbolic | producer result category, never universalized | tool/version, model bounds, property identity, raw report |
| Missing or unknown backend/lane/confidence | no evidence edge | emit a diagnostic; do not map to `source`, `Symbolic`, or `0.25` | raw record identity and report path |

Containment/definition evidence and dependency evidence may use different lanes.
A syntactically recognized call expression can coexist with a heuristic target
resolution and a later symbolic/imported fact. The canonical JSON must retain
all of them.

## Observable behavior and expected deltas

| Workflow phase | Observable behavior | Expected public-model delta |
| --- | --- | --- |
| Model/import contracts | An unrelated line insertion does not change symbol IDs; two backends can support one relation without provenance loss. | Schema version changes if readers need parallel evidence, nested P4 identities, or new relation kinds; existing fixture relation counts remain stable. |
| P4 syntax | A positive P4_16 fixture exposes exact P4 entities and parser/apply relationships; clean negatives emit none. | P4 file and symbol nodes plus defines/imports/calls or approved P4 relation kinds; no findings. |
| P4 evidence bridge | A real p4c failure fixture attaches a diagnostic/finding to the narrowest resolvable entity. | Finding node and Flags evidence, or an unmatched diagnostic; no structural-score change. |
| P4 metrics | A cyclic parser-state fixture yields one defined P4 cycle while an accept/reject fixture remains clean. | Metric-component delta only for approved P4 relationships; unrelated language metrics unchanged. |
| Tree-sitter pilot | A multiline P4 construct missed by lexical extraction is found without discarding lexical provenance. | Canonical relation count remains deduplicated under the approved model while evidence cardinality increases. |
| Structural diff | Reordered input arrays are unchanged; a serialized node field change (including `line`) or relation/evidence change is reported once. | No mutation of either input graph; deterministic diff artifact reports complete added/removed facts and before/after records for changed node/edge IDs. Top-level metrics and diagnostics are intentionally outside diff schema 1. |
| Declarative policy | The same graph passes or fails only according to an explicit versioned policy JSON document. | Extraction evidence unchanged; deterministic policy result and gate diagnostics only. |
| MCP | An MCP query returns the same stable-ID-ordered facts as the library `Catalog` query. | No graph mutation; protocol response preserves schema versions and complete evidence. Pagination is deferred. |
| Release verification | Every concern maps to a file, test, command, and retained artifact. | No unexplained generated files or schema drift. |

## Sentrux comparison snapshot

The comparison is pinned to public Sentrux commit
`6f8ff3c14b0423e4b58f42d1813d4d5f7fdc1d11`, release `v0.5.7`.

Verified with qualifications:

- the public core is Rust and contains 52 tree-sitter plugin definitions; this
  does not prove equal accuracy for all languages;
- the public core registers nine MCP tools, while official releases can include
  a private `sentrux-pro` crate, so the complete binary surface is not publicly
  attestable;
- `.sentrux/rules.toml` and baseline gating exist, but the gate tolerates a
  quality-signal decline up to 0.02 (200 displayed points) and also checks
  selected count/threshold regressions;
- the public README's `max_coupling` example does not match the implemented
  `max_coupling_score` field, and documented layer direction conflicts with the
  checker condition;
- public graph edges do not show Brick-style backend, confidence, and provenance;
- no public-source P4 or machine-checked formal-verification support was found.

This comparison supports prioritizing feedback-loop features. It does not
justify copying undocumented policy semantics, collapsing evidence lanes, or
claiming parity with private code.

Sources:

- <https://github.com/sentrux/sentrux/tree/6f8ff3c14b0423e4b58f42d1813d4d5f7fdc1d11>
- <https://github.com/sentrux/sentrux/releases/tag/v0.5.7>

## Baseline completion gate

The baseline state is ready to transition when:

- this ledger remains consistent with repository source;
- the quality-gate output and exact test inventories are recorded;
- P4_16, p4c v1.2.5.16, and the experimental grammar candidates are explicit;
- unsupported symbolic-verifier formats are not invented;
- each later phase has an observable model delta; and
- implementation starts at the model/identity/evidence contract rather than at
  an extractor regex, MCP transport, or renderer.