Skip to content

feat: Wave 1 — fix truth gaps, close rivet coverage, add Rocq CI#76

Merged
avrabe merged 1 commit intomainfrom
feat/wave1-truth-gaps-rivet-coverage
Apr 13, 2026
Merged

feat: Wave 1 — fix truth gaps, close rivet coverage, add Rocq CI#76
avrabe merged 1 commit intomainfrom
feat/wave1-truth-gaps-rivet-coverage

Conversation

@avrabe
Copy link
Copy Markdown
Contributor

@avrabe avrabe commented Apr 13, 2026

Summary

  • UCA YAML restructured (workaround rivet#129): flat ucas: format, all 25 UCAs now parsed (was 3), 33 broken links resolved. rivet validate goes from FAIL (55 errors) to PASS (0 errors).
  • Pipeline ordering docs (REQ-10): Updated REQ-10 and architecture.md to match actual CLI 10-phase order.
  • New rivet artifacts: FEAT-15/16/17 and DD-8/9/10/11/12 for code-verified capabilities.
  • Rocq CI (Add Rocq formal verification support using rules_rocq_rust #45): Added rocq-proofs job with Nix + Bazel (continue-on-error initially).

Rivet metrics

Metric Before After
Artifacts 144 174
Validation FAIL (55 errors) PASS (0 errors)
UCAs parsed 3/25 25/25
Broken links 33 0
Features 14 17
Design decisions 7 12
STPA chain coverage 8.3% (CC→UCA) 100%

Test plan

  • rivet validate — PASS (0 errors, 47 warnings)
  • rivet stats — 174 artifacts, 0 broken links
  • All pre-commit hooks pass
  • CI checks (Rocq job expected to be advisory)

🤖 Generated with Claude Code

UCA YAML restructured (workaround rivet#129):
- Flat ucas: section replaces grouped parser-ucas/isle-rewriter-ucas/etc
- All 25 UCAs now parsed (was 3), resolves 33 broken links
- rivet validate: PASS (0 errors, 47 warnings)

Pipeline ordering docs (REQ-10):
- Updated REQ-10 and docs/architecture.md to match CLI 10-phase order
- CLI is canonical: inline→precompute→constant-folding→cse→advanced→
  branches→dce→merge-blocks→vacuum→simplify-locals

New rivet artifacts:
- FEAT-15 (RSE), FEAT-16 (register allocation), FEAT-17 (precompute)
- DD-8 (HashMap policy), DD-9 (greedy coloring), DD-10 (stack validation),
  DD-11 (conservative LICM), DD-12 (two-tier verification)

Rocq CI integration (#45):
- Add rocq-proofs job with Nix + Bazel (continue-on-error: true)

Trace: REQ-10, REQ-9, REQ-14, REQ-13, REQ-5, REQ-1, REQ-7
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@avrabe avrabe merged commit a8837a8 into main Apr 13, 2026
22 of 23 checks passed
@avrabe avrabe deleted the feat/wave1-truth-gaps-rivet-coverage branch April 13, 2026 11:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant