# VEX Integration with Reachability

## Module
Attestor

## Status
VERIFIED

## Description
VEX candidates emitted from SmartDiff are bridged to reachability gates, VEX proof gate in policy engine, and VEX proof integrator in attestation for evidence-backed VEX statements.

## Implementation Details
- **VEX Proof Integrator**: `src/Attestor/__Libraries/StellaOps.Attestor.ProofChain/Generators/VexProofIntegrator.cs` (with `.Helpers`, `.Metadata`) -- integrates reachability evidence into VEX verdicts as proof references (proof_method, proof_confidence).
- **VEX Verdict Proof Payload**: `Generators/VexVerdictProofPayload.cs` -- payload binding VEX verdicts to reachability evidence.
- **VEX Attestation Predicate**: `Predicates/VexAttestationPredicate.cs` -- predicate containing VEX verdicts with reachability-backed proof.
- **Micro Witness Verdicts**: `Predicates/MicroWitnessVerdicts.cs` -- reachability verdicts from micro-witness evidence (function-level call path analysis).
- **Micro Witness Function Evidence**: `Predicates/MicroWitnessFunctionEvidence.cs` -- function-level evidence linking CVE to call path presence/absence.
- **Micro Witness Binary Ref**: `Predicates/MicroWitnessBinaryRef.cs` -- binary reference for the analyzed artifact.
- **Micro Witness CVE Ref**: `Predicates/MicroWitnessCveRef.cs` -- CVE reference within micro-witness evidence.
- **Micro Witness SBOM Ref**: `Predicates/MicroWitnessSbomRef.cs` -- SBOM reference linking reachability to component identity.
- **Micro Witness Tooling**: `Predicates/MicroWitnessTooling.cs` -- information about the reachability analysis tool.
- **Reachability Witness Payload**: `Statements/ReachabilityWitnessPayload.cs` (with `.Path`) -- witness payload containing reachability call paths.
- **Witness Call Path Node**: `Statements/WitnessCallPathNode.cs` -- node in the reachability call path.
- **Witness Path Node**: `Statements/WitnessPathNode.cs` -- path node in the reachability graph.
- **Witness Gate Info**: `Statements/WitnessGateInfo.cs` -- gate information for reachability policy evaluation.
- **Witness Evidence Metadata**: `Statements/WitnessEvidenceMetadata.cs` -- metadata about the reachability evidence source.
- **Tests**: `__Tests/StellaOps.Attestor.ProofChain.Tests/`

## E2E Test Plan
- [ ] Create reachability evidence via `MicroWitnessFunctionEvidence` showing a CVE's vulnerable function is NOT reachable; integrate into VEX as not_affected
- [ ] Create reachability evidence showing a CVE's vulnerable function IS reachable; verify VEX status is affected with proof_method="reachability_witness"
- [ ] Build a `ReachabilityWitnessPayload` with a call path (3 nodes) and verify the path nodes are correctly ordered
- [ ] Integrate reachability proof via `VexProofIntegrator` and verify the VEX verdict contains proof_ref pointing to the witness payload
- [ ] Verify micro-witness linking: create evidence with `MicroWitnessSbomRef` and verify the SBOM component is correctly linked to the reachability result
- [ ] Create a `WitnessGateInfo` for a reachability gate and verify it captures the gate policy (e.g., "block if reachable")
- [ ] Build a VEX attestation predicate with reachability evidence and verify it is a valid in-toto statement
- [ ] Test the boundary: create reachability evidence with unknown reachability status and verify VEX status is under_investigation

## Verification

| Check | Result |
|-------|--------|
| Tier 0 - Source Verification | PASS |
| Tier 1 - Build + Code Review | PASS |
| Tier 2 - Behavioral Verification | PASS |
| Verified Date | 2026-02-13 |
| Run ID | run-001 |