Tagma decoder execution path verification: ev as an independent channel

[metasmile]

Goal

Verify the Tagma 3-axis decoder execution path with the ev constraint engine as an independent channel, complementing the syntagma hardware track (syntagma issue #48), which verifies the decoder through Verilator simulation, golden anchors from the Rust tagma_core reference, gate-level simulation, and formal equivalence. ev would add a fifth, structurally different channel: the decoder contract expressed as a VerificationSpec, exhaustively enumerated and evaluated by ev's own engine.

Background

The Tagma decoder (syntagma/hw/rtl/tagma_decoder.v) maps a 16-bit Hangul code point to three structural axes:

code in [0xAC00, 0xD7A3]  (11,172 valid syllables)
offset = code - 0xAC00
i = offset / 588           (initial, 0..18)
m = (offset % 588) / 28    (medial, 0..20)
f = offset % 28            (final, 0..27)

Whitepaper: https://doi.org/10.5281/zenodo.21302508. The hardware verification artifacts live in syntagma/hw/ (branch 48-hw-verification, PR #50).

Scope

1. Model the decoder contract as a VerificationSpec:
   • field code over all 2^16 values
   • constraint: valid range [0xAC00, 0xD7A3]
   • axis decomposition (i, m, f) as projections of the offset
2. Add the projector capability the contract needs. ev currently ships sum, identity, parity; the decoder requires integer division and modulo by constants (588, 28, 21, 7) or a dedicated decode projector. This is the main engine extension.
3. Exhaustively verify the execution path: all 11,172 valid code points produce the expected axes, and invalid inputs are rejected by the range constraint.
4. Cross-check the ev results against the syntagma golden anchors (syntagma/hw/rtl/golden_anchors.hex, generated by tagma_core), following the golden-anchor pattern of issues Cross-verification harness: ev as reference for SSCCS standard experiment golden anchors #25 and SSCCS standard workspace golden anchor CI integration #28.
5. Optional follow-up: raw RTL design input for ev synth (ev synth --design tagma_decoder.v --top tagma_decoder), so the decoder's generic synthesis report comes from ev's YosysBackend instead of the mirrored script in syntagma/hw/synth/yosys/synth_generic.ys. The RunSynthesis trait already accepts arbitrary RTL; only the CLI path (currently VerificationSpec::from_yaml required) needs a design-only mode.

Acceptance criteria

• ev verify on the Tagma spec passes all 11,172 valid code points and rejects the invalid domain.
• The axis projections match the golden anchors for every valid code point.
• (Optional) ev synth --design produces the same SynthesisMetrics as the syntagma generic flow (478 cells, 0 registers, ev-compatible stat -json schema).

References

• Tagma whitepaper: https://doi.org/10.5281/zenodo.21302508
• syntagma hardware track: hw: Tagma decoder RTL, FPGA verification, and standard cell synthesis report syntagma#48
• golden anchor pattern: ssccs/poc/baremetal_riscv/sv (_golden_anchors.svh + check_golden_anchors.py)
• ev synthesis channel: issue Synthesis channel abstraction and Yosys integration in ev #4 (closed), src/synth/backends/yosys.rs

[metasmile]

Milestone 2 delivered on branch 47-tagma-fixture-specs (commit b10eab7), per the plan in ev issue #47.

Implemented the dedicated decode projector (tagma_decode):

• ProjectorSpec::TagmaDecode { field, base } in src/spec/mod.rs, with base defaulting to 0xAC00.
• Evaluator in src/verify/registry.rs: packs the Hangul decomposition into the golden-anchor layout offset[28:15] i[14:10] m[9:5] f[4:0] (offset = code - base, i = offset / 588, m = (offset % 588) / 28, f = offset % 28); returns None outside the valid block.
• sv_projector arm in src/synth/mod.rs so generated SystemVerilog preserves the packed layout.
• The tagma_decoder.xif.yaml fixture now uses the projector.

Verification: the projection of code 0xAC00 + k equals line k of syntagma/hw/rtl/golden_anchors.hex (spot values 0x00000000, 0x00008001, 0x00010002 confirmed; full 11,172-domain loop in tests). Tests: 100 total (73 lib + 17 CLI + 5 tagma + 5 structural), all passing; coverage gate at 82.30% regions / 83.27% lines.

Remaining per this issue: Milestone 3 (line-by-line cross-check against the anchor file) is now a direct comparison since the projector emits the anchor layout; Milestone 4 (design-only ev synth mode) is optional.