spec(openxc7): restore executable counter and flip-flop checks

[dmitrii-f-t27]

Closes #5850. Refs #5810 and #5812.

The two openxc7 host models discarded 347 tokens, losing tuple sequence checks and invariants. The counter tests also expected LED bit 23 to toggle after one pulse; the flip-flop checks included a wrong edge expectation and a tautological LED assertion. Both files now carry executable checks for their original Verilog behavior.

The repair uses supported tuple member access through locals and brace bodies, initializes the counter state, and spells boolean negation as logical ! so the Rust backend can build. All 17 function signatures and state layouts remain unchanged. The counter checks bit-23 carry, full rollover and low-clock hold; the flip-flop checks rising edges, held-high/falling input and complementary LED output. Two dropped flip-flop sequence tests and two dropped invariants are restored. One NOW receipt covers this defect family; benchmark blocks carry no measured timing claims.

Validation with fresh t27c at master 6e33229:

• Both specs consume every token: zero discard/truncate; typecheck zero errors/warnings; coverage 9/9 and 8/8.
• Counter: 8 tests pass, 4 compile-time invariants. Flip-flop: 14 tests pass, 4 compile-time invariants.
• Six negative controls reject a wrong LED bit, stopped carry, unconditional increment, stuck toggle, inverted LED and a level-triggered second cycle. The last mutant initially survived; the repeated-high scenario now rejects it. test-report exits zero even for failed tests, so verdict text was inspected.
• Generated Rust libraries compile. That backend does not lower the tests/invariants; behavior was executed in Zig.
• Duplicate-body ratchet, NOW shape, ASCII/signature preservation and whitespace checks pass. Seal-currency scan reports no new stale generated hashes.
• Final full corpus suite: 96 primary failures against 95 ledger entries. Only specs/xilinx7/packets.t27 [parse] remains unexpected; both repaired files are absent from primary failures. Ledger and cap are unchanged. The independent type-name collision is addressed by PR specs/port: four ported types stop colliding with corpus types (types ratchet) #5812.

Generated C remains blocked by tuple declarations emitted before their struct definitions; reproduced on the original and repaired counter, and observed on the flip-flop. No generated files were edited. Neither source has a saved seal; multiple openxc7 modules share the same seal path, so no seal was minted. No synthesis, bitstream, board, radio or measured latency validation is claimed.

{
  "version": 1,
  "head_sha": "346ea8ada57a74317f5f25c54ea0c2b5d25cc442",
  "summary": "Restore executable counter and flip-flop checks in two openxc7 host models, removing 347 discarded tokens.",
  "changes": [
    "Restore brace-form assertions and supported tuple access; explicitly initialize the counter and use logical boolean negation.",
    "Preserve all 17 function signatures and state layouts; check carry, rollover, hold, rising edges and LED polarity.",
    "Keep one NOW receipt for the family; do not enlarge failure ledgers or edit generated output."
  ],
  "tests": [
    {
      "command": "t27c test-report <each repaired spec>",
      "status": "passed",
      "result": "22 tests pass and 8 compile-time invariants hold; six source mutants rejected.",
      "evidence": "docs/now/2026-10-03-slow-blink-tests-execute.md"
    },
    {
      "command": "t27c parse-complete / coverage / typecheck <repaired specs>",
      "status": "passed",
      "result": "2/2 consume all tokens; coverage 9/9 and 8/8; zero type errors/warnings.",
      "evidence": "Both specs and the NOW receipt."
    },
    {
      "command": "t27c suite --repo-root . --ratchet --corpus-only",
      "status": "failed",
      "result": "96 observed versus 95 expected; only xilinx7/packets.t27 [parse] remains unexpected. Both repaired specs removed from primary failures.",
      "evidence": "Reproducible at this HEAD; local restored-family-suite.json/log."
    },
    {
      "command": "rustc --crate-type lib <each t27c gen-rust output>",
      "status": "passed",
      "result": "Both generated libraries compile; the Rust backend does not lower their tests/invariants.",
      "evidence": "Outputs generated from both specs without manual changes."
    },
    {
      "command": "cc -std=c11 -c <each t27c gen-c output>",
      "status": "failed",
      "result": "Existing tuple declaration ordering uses struct types before definition; no C success claimed.",
      "evidence": "Unknown CounterState / FlipFlopState at generated tuple typedefs."
    },
    {
      "command": "python3 tools/dupe_scan.py; NOW shape; signature/ASCII audit; git diff --check",
      "status": "passed",
      "result": "No new duplicate body; one valid NOW receipt; signatures preserved and files ASCII; no whitespace errors.",
      "evidence": "590 of 4749 bodies in 169 groups; none grew."
    },
    {
      "command": "GitHub CI for updated HEAD",
      "status": "not_run",
      "result": "Awaiting checks on this pushed commit; old-head greens do not validate this HEAD.",
      "evidence": "PR #5851 check rollup."
    }
  ],
  "limitations": [
    "Host simulation only; no physical FPGA/radio, synthesis or timing measurement.",
    "C tuple ordering remains a compiler defect; Rust tests/invariants are not lowered.",
    "Packets parse and independent type conflicts still need their existing repair PRs; no failure was hidden in a ledger."
  ],
  "tags": [
    "Engineering",
    "Verification"
  ],
  "blog": {
    "title": "Executable assertions expose discarded hardware model tests",
    "summary": "Twenty-two host model tests and eight invariants distinguish six counter and flip-flop faults.",
    "outline": [
      "Unsupported tuple bindings and misspelled declarations silently discarded checks while old expectations contradicted the modeled signals.",
      "Brace-form assertions, valid tuple access and negative controls check the counter boundary and flip-flop edge behavior.",
      "C declaration ordering and physical FPGA validation remain beyond the verified result."
    ]
  }
}