بنقرة واحدة
spec-adhere
Audit a Rust crate's adherence to its Stellar protocol spec (spec-driven, walks every normative claim)
التثبيت باستخدام Codex أو Claude انسخ هذا Prompt والصقه في Codex أو Claude أو مساعد آخر ليراجع صفحة Skill ويثبّتها لك.
القائمة
Audit a Rust crate's adherence to its Stellar protocol spec (spec-driven, walks every normative claim)
التثبيت باستخدام Codex أو Claude انسخ هذا Prompt والصقه في Codex أو Claude أو مساعد آخر ليراجع صفحة Skill ويثبّتها لك.
استنادا إلى تصنيف SOC المهني
| name | spec-adhere |
| description | Audit a Rust crate's adherence to its Stellar protocol spec (spec-driven, walks every normative claim) |
| argument-hint | [<SPEC> | <crate-path>] [--apply] |
Parse $ARGUMENTS:
{SCP_SPEC, OVERLAY_SPEC, HERDER_SPEC, LEDGER_SPEC, TX_SPEC, BUCKETLISTDB_SPEC, CATCHUP_SPEC} (case-insensitive, with or
without .md), set $TARGET to the spec name. The skill resolves
to the corresponding Rust crate via the mapping below.crates/scp,
crates/tx), set $TARGET to the crate. The skill resolves to
the corresponding spec.$TARGET = all: run every (spec, crate) pair in parallel.--apply is present, $MODE = apply. Otherwise $MODE = review.Walk every normative claim in a Stellar protocol spec under
stellar-specs/ and verify that the corresponding Rust
implementation in crates/<crate>/ enforces it. Spec-driven:
every MUST / SHALL / MUST NOT / SHALL NOT statement, every
INV-<X><N> invariant, every numbered validation rule, every
protocol-version branch, and every error-code mapping is checked.
This is the inverse of /spec-from-core and complements
/parity-check (which compares Rust against C++ headers, not
against the specs).
| Spec | Primary Rust crate | Notes |
|---|---|---|
SCP_SPEC | crates/scp | Driver/wiring also in crates/app (event loop owns SCP message dispatch & consensus trigger) |
OVERLAY_SPEC | crates/overlay | Dispatch/wiring also in crates/app (event loop: survey_impl.rs, tx_flooding.rs, peers.rs, lifecycle.rs) |
HERDER_SPEC | crates/herder | Integration/wiring also in crates/app (event-loop dispatch, consensus trigger) |
LEDGER_SPEC | crates/ledger | Some integration in crates/app |
TX_SPEC | crates/tx | Apply path also touches crates/app |
BUCKETLISTDB_SPEC | crates/bucket | |
CATCHUP_SPEC | crates/history | Also crates/historywork |
Cross-crate caveat (the #3158 blind spot).
crates/appowns the live overlay/herder/scp wiring — the event loop incrates/app/src/app/(lifecycle.rs,survey_impl.rs,tx_flooding.rs,peers.rs) is where message dispatch, survey processing, flood scheduling, and consensus triggers actually run. The spec-named library crate (crates/overlay,crates/herder,crates/scp) may contain dead / unwired code: a symbol can bepuband re-exported yet never instantiated outside#[cfg(test)](e.g.crates/overlay/src/survey.rs'sSurveyManager, exported atlib.rsbut only constructed in tests — the real survey logic lives incrates/app). Therefore: never declare an OVERLAY/HERDER/SCP feature "Absent" after searching only the named crate. Grepcrates/app(and the rest of thecrates/tree) for the wiring first. Conversely, do not treat an exported-but-never-instantiated library symbol as "the implementation" — confirm it is reachable from production code before classifying it Full.
Output file (apply mode):
/Users/tomer/dev/henyey/crates/<primary-crate>/SPEC_ADHERENCE.md
Read /Users/tomer/dev/henyey/stellar-specs/<SPEC>.md end-to-end.
Build a claim inventory:
INV-<X><N> ID and its body.@version(...) annotation.MANAGE_SELL_OFFER_MALFORMED) tied to a
specific check.Each claim gets a stable ID (use spec section + a sequence number,
e.g., SCP §4.2.3-1 for the first claim in §4.2.3).
For the primary crate (plus any secondary crates per the mapping
table), read all .rs files under src/. Skip tests/,
benches/, and #[cfg(test)] modules — adherence is about
production code.
Search ALL crates, not just the name-matched one (the #3158 fix).
Before classifying any claim, run a grep-first pass over the entire
crates/ tree for the spec-bound symbols (function names, constants,
result-code enum values, dispatch match-arms) — do not scope the
search to the primary crate alone. Henyey's event loop in crates/app
owns much overlay/herder/scp wiring (dispatch, survey processing,
flood scheduling, consensus trigger), so a symbol absent from the
name-matched crate is not absent from the codebase. Keep the
primary crate as the deep-read target; grep-target the rest of the
crates (especially crates/app) and read only the matching files.
Concrete command:
# Locate candidate implementations across ALL crates before reading.
grep -rni --include='*.rs' -e '<symbol>' -e '<CONST>' -e '<RESULT_CODE>' crates/
Build a lightweight index of:
SCREAMING_SNAKE_CASE or PascalCase per Rust convention)const fnprotocol_version_starts_from, protocol_version_is_before,
>= ProtocolVersion::, or equivalent helpers// Spec: anchors (already 16 across the workspace as
of v26.0.1 regenerate)For every claim from Step 1, attempt to locate the Rust enforcement:
// Spec: <SPEC> §N comment cites the
claim's section, follow it.grep -rn --include='*.rs' … crates/), not
only the name-matched crate.Reachability check (the #3158 fix) — run at every Full/Absent
decision point. Before recording a found symbol as Full, verify it
is actually instantiated / called in the production control path:
grep for a non-#[cfg(test)] caller or constructor.
# Is the candidate reachable from production code (not just tests)?
grep -rn --include='*.rs' '<symbol>' crates/ | grep -v -e '#\[cfg(test)\]' -e '/tests/'
If the only references are tests or re-exports — the
crates/overlay/src/survey.rs SurveyManager dead-scaffold case
(exported at lib.rs but constructed only under #[cfg(test)]) — treat
it as dead/unwired code and keep searching (the live implementation
is typically the event-loop wiring in crates/app) rather than reporting
it as "the implementation." Symmetrically, never record Absent without
an all-crates grep: confirm the symbol/result-code is missing from the
entire crates/ tree (especially crates/app), using two search
strategies across all crates, before classifying Absent.
Classify the finding:
Absent (SHOULD) and note.)For each finding, record:
path/to/file.rs:LINE) or not foundCross-check every // Spec: <SPEC> §N comment in
crates/*/src/*.rs against the regenerated spec sections. If a
cited section no longer exists or has been renumbered, list it as
a dangling anchor for fix-up.
adherence_pct = Full / (Full + Partial + Absent) * 100
Partial and Absent count against adherence; N/A is excluded. Drift items are surfaced separately and not counted (they require human decision).
$MODE = review (default)Report to chat in this structure:
# Spec Adherence: <SPEC> ↔ crates/<crate>
**Adherence:** X% (Full N | Partial M | Absent K | Drift D | N/A J)
## Summary table (top section, ≤ 15 rows)
| Section | Topic | Status | Implementation |
|---------|-------|--------|----------------|
| §4.2 | Quorum slice test | Full | scp/quorum.rs:142 |
| §8.5 step 7 | Upgrade stripping | Absent | not found |
| ... |
## Detailed findings (grouped by spec section)
### §4.2 — Quorum Slice Test
- **Claim SCP §4.2-1** (MUST): "A quorum slice U of node N MUST..."
- **Rust**: `crates/scp/src/quorum.rs:142` `fn is_quorum_slice(...)`
- **Status**: Full
- **Notes**: Includes the v-blocking edge case in spec.
(repeat per section that has findings; collapse Full-only sections
to a single line)
## Invariant coverage
| Invariant | Status | Enforcement |
|-----------|--------|-------------|
| INV-S1 (Phase monotonicity) | Full | scp/phase.rs:apply (asserts) |
| INV-S11 (Singleton qset for EXTERNALIZE) | Absent | grep returned nothing |
| ... |
## Dangling Spec anchors
- `crates/tx/src/validation.rs:553` → `TX_SPEC §4.2.3` — section
not found in current spec (renumbered to §5.2.3?).
## Drift items (require human review)
- §6.2 step 4: spec says `nC != 0 → nH != 0 AND ballot.counter >=
nH AND nH >= nC`. Rust implements `nH > nC` (strict). Likely
the Rust is wrong; verify against stellar-core.
## Recommendations
1. Add enforcement for INV-S11 (correctness-critical).
2. Fix dangling anchors.
3. Investigate drift items.
Do not write any files in review mode.
$MODE = applyWrite the report to
/Users/tomer/dev/henyey/crates/<primary-crate>/SPEC_ADHERENCE.md
using the same format. Bump (or set) a **Last Updated:** line.
If SPEC_ADHERENCE.md already exists, preserve any
Human-Verified annotations (a future convention — items the
reviewer marked as "verified Full", "verified Drift", or
"deliberately Absent"). Reformat everything else.
If the parity column in the main README.md Crate Overview also
tracks a "Spec Adherence" percentage in the future, update it.
(Today the column tracks /parity-check percentage; do not change
it.)
$TARGET = <SPEC name>: run the spec ↔ crate pair for that spec.$TARGET = <crate path>: resolve to the spec mapped to that crate.$TARGET = all: run all 7 spec ↔ crate pairs. Recommend
parallel subagents (one per pair) since each is independent..rs file in the primary crate; skim
secondary crates if mapped.tests/, #[cfg(test)]).grep to locate candidate
implementations before reading full files.// Spec: anchors are accelerators — start there
to seed the search.crates/. This skill audits, it
does not fix.crates/ tree, especially crates/app,
not just the name-matched crate) before marking Absent. This is the
#3158 cross-crate fix: overlay/herder/scp wiring lives in crates/app./spec-from-core — generates / updates specs from C++. Run when
stellar-core changes or canon evolves./parity-check — structural parity (Rust API vs C++ headers).
Use when you want a function-by-function inventory./spec-adhere — behavioral parity (Rust vs Spec). Use when you
want to verify implementation correctness against the contract.The three skills form a triangle: C++ ↔ Spec ↔ Rust ↔ C++. Each edge is checked by one skill.
One tick of a CI watchdog — check main-branch GHA status; spawn an agent to fix if failing and no investigation is in flight.
One tick of the henyey mainnet monitor — checks, metrics scan, deploy, status report
Continuous always-on orchestrator for the henyey project pipeline. Each pass queries the board, central-picks up to N actionable issues by priority, and fans out parallel foreground specialist sub-agents (triage/plan/do/review-pr) with the right Claude model per stage. Owns concurrency, conflict-avoidance, CI pipelining, sibling-nit consolidation, and a self-reflection pass that files pipeline-improvement issues. Replaces scripts/project-tick-loop.sh. Use when the operator asks to "run the loop", "process the board continuously", or "keep the pipeline going".
Single-pick dispatcher primitive for the henyey project pipeline. One tick = pick one actionable issue from the project board and dispatch the right specialist sub-agent for its current state. Used for manual single picks and `--issue=` recovery; the continuous orchestrator is `/project-loop`, which owns concurrency centrally. Use when the user asks to "run a tick", "pick up an issue", or "process one board item".
Run two parallel adversarial PR reviewers and combine their verdicts with external PR reviews (GH Copilot bot, humans, other bots) and CI state into a merge decision. Agent reviewers post structured comment verdicts (since the agent is the PR author and cannot self-approve via GH native review). External CHANGES_REQUESTED reviews block merge identically to agent CHANGES_REQUESTED. Operates on issues in `in-review`. Auto-merges with --admin on all-green (after filing follow-up issues for unaddressed inline review comments, so non-critical feedback is preserved as backlog instead of dropped); bounces to `ready-for-doing` on any request-changes or CI red; blocks after 3 bounce-backs on the same code state. At the lifetime cap (6 bounces since last `## Review: Reset`) the PR enters **force-converge mode**: if CI is green, the PR auto-merges and unresolved reviewer concerns become follow-up issues; only red/pending CI at the cap still blocks. Use when invoked by /project-tick with an issue in in-review, or manuall
Audit a Rust crate's adherence to its Stellar protocol spec (spec-driven, walks every normative claim)