# Weir vision
Weir is the dataflow layer on top of Vyre.
Vyre provides the GPU execution stratum. Weir proves that stratum can express
compiler and security-analysis workloads that are traditionally CPU-only:
SSA, reaching definitions, IFDS, points-to, range analysis, slicing,
callgraph queries, and proof witness extraction.
## Product boundary
Weir is not a parser, scanner, or source-language frontend. It consumes graph,
AST, and fact buffers produced by frontends and emits Vyre `Program`s plus CPU
oracles for dataflow primitives.
Weir owns:
1. Dataflow primitive APIs.
2. Soundness tags for those primitives.
3. CPU reference implementations.
4. Vyre `Program` builders for GPU execution.
5. Bridges from GPU reachability output to proof objects.
Weir does not own:
1. C parsing.
2. Rule languages.
3. Raw CUDA, WGSL, or PTX kernels.
4. Security finding schemas.
## quality bar
Weir is depth when:
1. Every primitive has a CPU oracle and a GPU `Program`.
2. Every primitive declares soundness as `Exact`, `MayOver`, or `MustUnder`.
3. IFDS reaches GPU fixpoint and decodes into source-level proof witnesses.
4. Proof extraction is amortized over many findings, not rebuilt per finding.
5. A frontend can add a new source language without changing Weir internals.
6. Every public claim is backed by a test or executable example.
## Release thesis
The release thesis is simple: Weir makes GPU dataflow real enough to compose
with Vyre's condition engine.
For this release, Weir must demonstrate:
1. IFDS CPU reference correctness.
2. GPU step construction as Vyre IR.
3. Exploded reachability decoding into statement masks.
4. Witness extraction with sanitizer rejection and per-source masks.
5. Reusable prepared witness graphs for many findings over one CSR.
## Architecture rules
1. No raw shader source in Weir.
2. No fake implementations.
3. CPU references must be clear enough to act as correctness oracles.
4. GPU builders must return real Vyre `Program`s.
5. Soundness tags are part of the public contract.
6. Repeated proof extraction must reuse prepared graph state.
## Relationship to Vyre
Weir depends on Vyre the way a compiler backend depends on LLVM: it uses the
substrate without becoming the substrate. If Weir needs a lower-level primitive
used by multiple domains, that primitive belongs in `vyre-primitives`; otherwise
it stays in Weir.
## Release evidence
Release readiness for this document is proven through the Vyre/Weir evidence manifest and generated artifacts under `release/evidence/`. Claims here must map to concrete gate output, benchmark output, conformance output, parser corpus output, or documentation proof files before the release requirement can be closed.
Concrete evidence anchors:
- `release/evidence/weir/weir-analysis-api-matrix.json`
- `release/evidence/weir/weir-vyre-integration-tests.json`
- `release/evidence/optimization/weir-facts-pass-firing.json`
- `release/evidence/benchmarks/weir-dataflow-release.json`