ARK RTL Review Witness - Evidence Memo v1.0

This memo states what ARK RTL Review Witness has and has not proven as of the v0.6.1 evaluation packet.

What The System Does

RTL Review Witness takes a suspicious RTL change, flags structural or semantic drift, isolates the affected cone-of-influence, escalates a localized review target into a SAT-backed miter check where available, and produces a manifest-linked evidence packet.

The differentiation is the review-compression workflow: drift detection, cone isolation, localized review targeting, packetization, replay posture, and provenance. The SAT backend itself is standard tooling; ARK's value is upstream and downstream of that solver.

Review Compression Metric

• Input scope: 403 measured RTL lines across 7 available Reserve Arbiter scenario files and 8 RTL Review Witness scenarios.
• Review target scope: 8 isolated root-signal targets, 6 cone files, 28 cone entries, and 1 localized SAT escalation case.
• Compression ratio: 50.375:1, measured as available RTL lines divided by isolated root-signal targets.
• Boundary: This is measured on current internal/public-corpus artifacts. It is review-compression evidence, not final verification closure, customer ROI, or a guarantee that excluded regions are safe.

Review Priority & Third-Party RTL Exercise

The Review Priority Analyzer ranks isolated RTL review targets by graph leverage, cone context, and feedback-cycle involvement (using PageRank centrality, Strongly Connected Components, and cycle multipliers). It helps engineers decide what to inspect first; it does not prove safety or replace formal verification.

• Third-Party RTL Exercise: The priority analyzer was run on public third-party Verilog modules (PicoRV32 and verilog-axi priority encoder).
• Boundary: This benchmark does not claim vulnerabilities in PicoRV32 or verilog-axi. It demonstrates that the analyzer can process public third-party RTL and produce bounded review-priority rankings.

What Is Proven

• Drift detection and semantic flagging on ARK's internal RTL corpus, including Reserve Arbiter variants and associated silicon evidence assets.
• Cone-of-influence isolation for evaluated suspicious RTL changes.
• Localized miter-based SAT escalation on the evaluated breaker-state operator-shift case.
• Yosys SAT backend integration with counterexample capture for the isolated miter.
• Manifest-linked packet generation with SHA-256 provenance through the v0.6.1 evaluation packet.
• Specific evaluated result: breaker_state / trip operator shift, reference < versus candidate <=, divergence confirmed.
• Concrete counterexample: liquidity_pool=0, threshold=0; reference 0 < 0 is false, candidate 0 <= 0 is true.
• Triage and cone isolation exercised on public third-party RTL corpora with ARK-introduced controlled mutations. Source repo, license, file, mutation, reference expression, candidate expression, SHA-256 provenance, and cone summary are documented per case.
• Replay posture: replayable on the evaluated internal corpus and packet artifacts.

What Is Not Proven

• RTL Review Witness has not yet been validated on external partner RTL.
• The triage methodology has not yet received independent third-party review.
• No completeness claim is made; RTL Review Witness reduces review scope and highlights suspicious regions, but does not replace human review, LEC, full formal verification, security signoff, or vendor EDA tools.
• No claim is made that cone isolation catches every malicious, accidental, sequential, timing-dependent, or stateful RTL change.
• The v0.6 localized miter is a checked-in harness for the evaluated breaker cone; broad automated miter generation for multi-cycle sequential cones remains a v0.7 roadmap item.
• Production hardening, external adapter packaging, and customer-owned RTL evaluation are not complete.

Current Maturity

Internal corpus validated; public third-party corpus exercised on PicoRV32 (YosysHQ, ISC) and verilog-axi (MIT) with four ARK-introduced controlled mutations: valid-signal inversion, one-hot output shift, ready-gate bypass, and reset-gate removal. All four were flagged REVIEW_CANDIDATE with cone isolation. The external corpus run also exposed and resolved three parser gaps in public Verilog-2001 handling: line-comment stripping, wire/reg declaration discovery, and unary ~ tokenization. Customer-owned RTL evaluation has not yet been performed.

What The Evaluator Gets On Day One

• Internal generation details are reserved for partner evaluation. Public materials show the resulting reports, ranked targets, evidence boundaries, and manifest lineage.
• Sample RTL artifacts with known suspicious changes.
• Expected evidence packet output for the evaluated breaker-state operator-shift case.
• Localized SAT miter artifact for the < versus <= divergence example.
• Manifest and SHA-256 provenance references.
• Replay and walkthrough instructions appropriate to the evaluation scope.
• This evidence memo.

What The Evaluator Does Not Get Automatically

Full source access, private internal corpus RTL, unrestricted redistribution rights, proprietary tuning internals, and unrelated ARK chip-IP assets are not included automatically. Deeper access is governed by paid evaluation terms, NDA scope, and field-of-use constraints.

Next Step

Paid evaluation: the evaluator supplies or nominates a sanitized RTL artifact; ARK runs RTL Review Witness, delivers an evidence packet and technical walkthrough, and reports whether the workflow narrows review scope usefully for that artifact.