Structural enumeration correctness and verification claim accuracy

[metasmile]

Summary

A review of the CVA6 CV-X-IF verification report (docs/cva6.qmd) and a local reproduction of the benchmark numbers found one correctness bug in the structural enumeration pipeline and several claims in the report that do not hold as written.

Findings

1. StructuralEnum over-generates invalid combinations (correctness bug)

StructuralEnum::advance_indices in src/verify/compose.rs has a cross-constraint wrap bug. When a child field (e.g. funct7) wraps to its first allowed value while its parent (funct3) advances, the wrapped value is not revalidated against the new parent. Concretely, for tests/fixtures/cva6/xif_ref.xif.yaml, the funct3=2 band is emitted with funct7=0 (required: 96) for all 32,768 register combinations.

Measured on the committed fixtures (release build):

Fixture	struct_enum emitted	valid (full check set)	evaluate_all passed
cva6_full	262,144	229,376	229,376
cva6_r4	14,336	12,288	12,288

Because validate_into_space (src/verify/evaluate.rs) deliberately skips structural checks (build_runtime_checks keeps only eq/neq/lt/gt/le/ge/even), the 32,768 invalid combinations are placed into the CoordSpace as valid. The report claim "generates only structurally valid combinations" is therefore false in the current code. The existing equivalence test uses a cross mapping whose first allowed child value is valid for every parent, so it does not catch this.

2. Spike "cross-validation" is circular

The C program generated by src/synth/backends/spike.rs never executes the instruction words. main() runs check_encoding() (a C reimplementation of the same constraint model), assembles the word into a variable, and prints it. Spike runs that program under pk. There is no ISA-level validation, and the merge reason string "Spike: illegal instruction trap" is misleading. The report claims "actual RISC-V simulation" and "100% correctness", which overstate what is checked.

3. Valid count semantics

"229,376 valid encodings" counts field-value combinations. After enable_mask collapsing, distinct 32-bit words for the full fixture are about 164,865 (funct3=1: 32,768 combos collapse to 1 word; funct3=2: 32,768 combos collapse to 1,024 words). The report does not disclose this.

4. Benchmark reproducibility

benches/bench.rs has no benchmark for the full 33M fixture, so the 29.7 s / 31.3 ms figures are one-off measurements. Its own comment claims "cva6 evaluate = 14 s" while the report cites 1.23 s for the same R4 fixture.

5. Report typos and stale claims

"14.0Mx vs HashMap" is almost certainly a typo for ~14x. The limitations section still says NOP conditional field activation is unsupported even though enable_mask implements it, and says func2 is unavailable even though the R4 fixture has a func2 field.

Proposed work

• Fix StructuralEnum so every emitted combination satisfies the full constraint set, with an equivalence guarantee between struct_enum, validate_into_space, and evaluate_all.
• Add regression tests in /tests covering the wrap pattern and the CVA6 fixtures.
• Add full-space CVA6 benchmarks plus a structural validity guard to benches/bench.rs.
• Make the Spike path cross-check C-assembled instruction words against the Rust-computed reference words and correct the reason strings.
• Correct the report claims in docs/ (Spike wording, combination vs word counts, 14.0Mx typo, stale limitations) using re-measured numbers.

[metasmile]

Work in progress on branch 43-structural-enum-correctness (not pushed).

Completed:

• fix: structural enumeration emits only cross-valid combinations #43 (compose.rs: stable topological order, O(1) fix_suffix via precomputed first-valid indices, valid initial state; struct_enum full now 25.5 ms vs 28.1 ms before, emitting exactly 229,376 valid combos)
• test: structural enumeration equivalence and wrap regression #43 (tests/structural_enum.rs: wrap pattern, invalid initial state, CVA6 full/R4 counts, validate_into_space distinct-path semantics)
• bench: full-space CVA6 group with structural validity guard #43 (bench.rs: evaluate/struct_enum/validate/validity for the 33M fixture; validity guard is green)
• fix: spike backend cross-checks assembled words with honest reasons #43 (spike.rs: C program now compares its assembled word against the Rust reference; reasons corrected; doc comment states Spike never executes the custom opcodes)
• docs: sync cva6 and index reports with corrected claims #43 (229,376 combinations with 164,865 distinct words documented; 14.0Mx -> 14x; Spike wording; limitations updated; riscv-dv/OneSpin caveats)

All 92 tests pass; clippy and fmt clean.

Remaining (needs decisions): apply the same doc corrections to ssccs/docs/projects/ev/ (separate repo), and decide whether the HW_NOP any-funct7 and ADD_RS3_R rs2[4:2] model gaps should be closed in the fixtures (they would change the valid counts).

[metasmile]

Registered as a separate follow-up: #44 (Execute accepted CVA6 custom-3 encodings through the standard tandem simulation flow).