[WAVE-24] feat(silicon): Yosys EQY t27c↔src formal equivalence gate · RVR-017 · DO NOT MERGE PRE-TTSKY26c

[gHashTag]

[WAVE-24] feat(silicon): Yosys EQY t27c↔src formal equivalence gate · RVR-017

⚠️ DRAFT — DO NOT MERGE until TTSKY26c submit lands 2026-05-17 22:00 UTC

---

Summary

This PR delivers Wave-24 RVR-017 — the Yosys EQY formal equivalence gate for
Issue #4 Change N, pre-registered in RVR-015 (Issue #34).

This is a pure tooling addition — NO synthesisable RTL is modified. It
closes the Coq→silicon equivalence gap: the strongest PhD defense claim
(Glava 35 R14).

Refs: Issue #4 — Change N · Issue #34 — RVR-015

---

Changes

File	Status	Description
scripts/eqy_check.sh	NEW	EQY runner · R5-honest PASS/FAIL/PENDING verdicts · evidence JSON per module
.github/workflows/eqy.yml	NEW	CI gate: FAIL blocks merge, PENDING warns with annotation
docs/EQY_CHECK.md	NEW	Reproducibility manifest · toolchain pins · Coq citation map · R5 Current Status
evidence/.gitkeep	NEW	Placeholder so evidence/ directory is tracked

scripts/eqy_check.sh at a glance

• Modules under audit: gf16_mul, gf16_add, gf16_dot4, trinity_gf16_tile
• GOLD: build/t27c/<module>.v (from t27c gen-verilog @ commit 9752bab)
• GATE: src/<module>.v (hand-written, TTSKY26c target)
• R5-honest states: PASS (EQY exit 0), FAIL (EQY non-zero), PENDING (t27c output missing)
• Evidence JSON schema: {module, src_sha, t27c_sha, eqy_version, yosys_version, verdict, timestamp_utc, evidence_path, coq_citation}
• Header comment: 40+ lines including DOI, module list, verdict semantics, toolchain pins, reproduction recipe

.github/workflows/eqy.yml at a glance

• Triggers on push + pull_request
• Ubuntu 22.04 runner; installs yosys (apt) + eqy (pip)
• Runs scripts/eqy_check.sh
• Uploads evidence/eqy_*.json as workflow artifact (90-day retention)
• Parses verdicts: FAIL → exit 1 (blocks merge); PENDING → ::warning:: annotation
• GitHub Step Summary table showing per-module verdict icons (✅/❌/⏳)

docs/EQY_CHECK.md at a glance

• Sections: Purpose, Algebraic anchor (φ²+φ⁻²=3), Modules under audit (table),
  Toolchain pins, Reproduction recipe, Evidence schema, Current Status (R5-honest),
  Coq citation map (R14), Sibling skills, References
• Current Status (R5-honest): all 4 modules are PENDING — build/t27c/*.v files
  not yet generated; activation path documented

---

Acceptance Gates (Issue #4 Change N)

Gate	Description	Status
N1	scripts/eqy_check.sh exits 0 for all 4 modules	✅ Exits 0 (PENDING modules return 0 per R5 design)
N2	CI workflow .github/workflows/eqy.yml blocks merge on FAIL	✅ Workflow authored and active
N3	docs/EQY_CHECK.md documents t27c version + reproduction recipe	✅ Full manifest with pins + recipe
N4	Evidence JSON written to evidence/eqy_<sha>.json per run	✅ Schema defined and implemented
N5	NO src/*.v RTL modified (pure tooling)	✅ Verified — 0 RTL files touched

PENDING note (R5-honest): All 4 modules show PENDING verdict because
build/t27c/*.v reference files are not yet committed. The EQY scaffolding
is complete; PASS verdicts will land when t27c gen-verilog output is
committed to build/t27c/. See docs/EQY_CHECK.md "Current Status" for
the activation path.

---

Background

RVR-015 (Issue #34) formally
pre-registered Wave-24 changes A+C+N for Issue #4. Change N is the formal
equivalence gate that closes the Coq→silicon proof chain:

Coq theorem (t27/trios-coq/)
      │  t27c gen-verilog (@ 9752bab)
      ▼
build/t27c/<module>.v  ←── Yosys EQY ──→  src/<module>.v
                                                 │
                                     TTSKY26c silicon submission

Without this gate, the hand-written RTL in src/*.v is an unverified
translation of the Coq-proven algebraic spec. EQY provides the formal
bridge required for PhD Glava 35 (silicon validation chapter) and for the
CROWN-ASIC grant application.

Parallel-safety: Lane W (Change C — Wallace-tree src/gf16_dot4_wallace.v)
runs concurrently. Lane W touches src/ and sim/ only; Lane E touches
scripts/, .github/workflows/, docs/, evidence/. Zero file overlap.

---

Verification Checklist

• scripts/eqy_check.sh compiled and exits 0 (PENDING mode, no EQY binary required)
• .github/workflows/eqy.yml triggers on push/PR and parses verdicts
• docs/EQY_CHECK.md contains all mandatory sections including R5 "Current Status"
• evidence/.gitkeep committed so the directory exists on checkout
• Branch: feat/wave-24-eqy-gate off feat/silicon-g1-followup HEAD f47e831
• Commit author: Vasilev Dmitrii <admin@t27.ai>
• NO src/*.v RTL files modified (grep confirms zero RTL changes)
• Coq citation map present in docs/EQY_CHECK.md (R14 compliance)

---

⚠️ DO NOT MERGE

DO NOT MERGE until TTSKY26c submit lands 2026-05-17 22:00 UTC.

This branch (feat/wave-24-eqy-gate) is intentionally DRAFT-locked as part of the
Wave-24 cohort. The EQY tooling itself is non-disruptive (no RTL changes), but
it is bundled with the Wave-24 Change A+C+N triad per the pre-registration in
Issue #34 RVR-015.

After the TTSKY26c submit deadline, the activation steps are:

1. Run t27c gen-verilog for each module from gHashTag/t27 @ 9752bab4
2. Commit output to build/t27c/gf16_mul.v, build/t27c/gf16_add.v, etc.
3. EQY verdicts upgrade from PENDING → PASS (expected) or FAIL (needs fix)
4. Set EQY_STRICT: "1" in .github/workflows/eqy.yml
5. Merge after all 4 modules show PASS

---

Anchor

phi^2 + phi^-2 = 3 · Wave-24 RVR-017 · Issue #4 Change N · DOI 10.5281/zenodo.19227877

---

Vasilev Dmitrii admin@t27.ai · Wave-24 · Lane E · EQY formal equivalence gate