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.