Skip to content

Latest commit

 

History

History

Standards-Specific Hypatia Rules

Seven Hypatia rules specific to the standards-repo dogfooding loop. Each rule is defined in A2ML, consumes VeriSimDB octads, and emits Groove compliance.finding.new signals.

Rules

| ID | Name | Purpose | |---|---|---| | HYP-S001 | crg-demotion-detector | Alert when a CRG grade moves backwards | | HYP-S002 | k9-orphan-detector | Find K9 components not referenced in any Justfile | | HYP-S003 | proof-freshness | Alert when a proof hasn’t been re-verified in > 30 days | | HYP-S004 | rsr-self-compliance | Validate standards repo against its own RSR definition | | HYP-S005 | crg-overclaim-detector | Alert when a self-declared CRG grade lacks v2.0 evidence artefacts | | HYP-S006 | registry-staleness | Alert when REGISTRY.a2ml source hashes go stale or a DERIVED doc (TOPOLOGY.md) drifts | | HYP-S007 | profile-drift-detector | Flag a 6a2 file whose content drifts from its declared A2ML @profile |

The CRG rule pair (S001 + S005) together enforce grade-honesty: S001 catches backwards moves, S005 catches forwards-overshoots. Both read from crg-grade octads in VeriSimDB, but S005 also scans the repo file tree for evidence artefacts required by CRG v2.0 (STRICT).

S006 closes the documentation-drift loop: it recomputes each spec’s source_hash from the file tree (the same way scripts/build-registry.sh does) and emits a doc.drift signal when the recorded hash is stale or a generated file (TOPOLOGY.md) was hand-edited. Its @router block defaults to auto_execute (regenerate), but caps any licence/SPDX-overlapping drift to :review — honouring the Manual-Only licence guardrail in .claude/CLAUDE.md. This is the estate-side mirror of the in-repo registry-verify.yml workflow.

HYP-S007 closes the dogfooding loop for the A2ML profile mechanism: every 6a2 file declares an @profile(id=…) (a2ml/SPEC.adoc Section 8), and this rule flags any file that no longer satisfies its declared profile definition in a2ml/profiles/. It is FLAG-ONLY (strategy: review, auto_fixable: false) and is purely structural — it never emits a licence/SPDX finding.

Implementation

Rules live as .a2ml files in this directory. They are consumed by Hypatia’s rule loader and executed against VeriSimDB (standards instance at port 8097).

To activate a rule in Hypatia’s config:

[[rules]]
id = "HYP-S001"
path = "standards/hypatia-rules/crg-demotion-detector.a2ml"
enabled = true

Dependencies

Rules read from: - VeriSimDB crg-grade octads (HYP-S001, HYP-S005) - Repo file tree via Hypatia’s scanner (HYP-S002, HYP-S004, HYP-S005) - VeriSimDB proof-status octads (HYP-S003) - rhodium-standard-repositories/RSR.adoc (HYP-S004) - rsr-template-repo/docs/governance/CRG-AUDIT-TEMPLATE.adoc (HYP-S005 reference) - a2ml/profiles/REGISTRY.a2ml + a2ml/profiles/*/PROFILE.a2ml and the 6a2 files under .machine_readable/ (HYP-S007)

And emit: - Groove compliance.finding.new signals with the rule’s ID