Skip to content

fix(governance): reconcile hypatia baseline with current scanner ruleset - #328

Merged
hyperpolymath merged 1 commit into
mainfrom
fix/governance-hypatia-baseline
Jul 28, 2026
Merged

fix(governance): reconcile hypatia baseline with current scanner ruleset#328
hyperpolymath merged 1 commit into
mainfrom
fix/governance-hypatia-baseline

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Cures the only red check on main: governance / Validate Hypatia Baseline.

Root cause

The reusable governance workflow runs hypatia at main HEAD, unpinned. Since the baseline was written, hypatia gained rule types the 285-entry baseline predates (missing_timeout_minutes, WF017 secret_action_without_presence_gate, codeql_missing_actions_language, expect_in_hot_path, unsafe_block, as_ptr, zig_ptr_cast, SD007, SD022) and dropped Belt/Js.* deprecated_api from high to medium, which breaks exact-severity baseline matching for 36 findings. 85 findings were failing the gate.

What this does

15 findings fixed in code rather than baselined:

  • job-level timeout-minutes on server-boot-gate, fly-deploy, s4-loop, push-email-notify
  • instant-sync.yml: gate the repository-dispatch step behind a FARM_DISPATCH_TOKEN presence check (WF017)
  • codeql.yml: scan the actions language alongside javascript-typescript
  • .claude/CLAUDE.md: reword the .scm-deprecation paragraph so it stops tripping SD007 on its own migration examples
  • ffi/zig/src/{typell,overlay,boj}.zig: make error_buf sentinel-terminated ([N:0]u8) and drop the @ptrCast — writers always NUL-terminate, so the coercion is sound

70 findings baselined as 44 acknowledged entries (medium deprecated_api pending the ReScript→AffineScript migration, FFI-boundary unsafe_block/as_ptr/expect_in_hot_path debt, and two SD022 false positives that cite external-corpora paths).

Verification

Reproduced the CI job offline against hypatia 3b04900 using the exact governance-reusable.yml invocation (HYPATIA_FORMAT=json, BLOCKING_THRESHOLD=info, the same jq path relativisation, then apply-baseline.sh … blocking):

  • before: 151 findings → 85 kept → exit 1
  • after: 136 findings → 0 kept → exit 0

Zig changes pass semantic analysis on both the CI-pinned 0.14.0 and 0.16.0. All six modified workflows strict-parse as YAML.

Follow-up (not in this PR)

The scanner floats at hypatia main HEAD, so this gate can re-redden whenever hypatia adds rules — worth proposing a pinned scanner SHA upstream in standards.

The Validate Hypatia Baseline gate went red because hypatia main
(3b04900) added rule types the 285-entry baseline predates
(missing_timeout_minutes, WF017, codeql_missing_actions_language,
expect_in_hot_path, unsafe_block, as_ptr, zig_ptr_cast, SD007, SD022)
and dropped Belt/Js.* deprecated_api severities from high to medium,
breaking exact-severity baseline matching for 36 findings.

Fix 15 findings in code rather than baselining them:
- add job-level timeout-minutes to server-boot-gate, fly-deploy,
  s4-loop, push-email-notify
- instant-sync: gate the repository-dispatch step on a
  FARM_DISPATCH_TOKEN presence check (WF017)
- codeql: scan the actions language alongside javascript-typescript
- .claude/CLAUDE.md: reword the .scm-deprecation paragraph so it stops
  tripping SD007 on its own migration examples
- ffi/zig: make error_buf sentinel-terminated ([N:0]u8) and drop the
  @ptrCast — writers always NUL-terminate, so the coercion is sound
  (verified: semantic analysis clean on zig 0.14.0 and 0.16.0)

Baseline the remaining 70 findings as 44 acknowledged entries
(medium deprecated_api pending the ReScript migration, FFI-boundary
unsafe_block/as_ptr/expect_in_hot_path debt, two SD022 false
positives citing external-corpora paths).

Verified offline against hypatia 3b04900 with the exact
governance-reusable.yml invocation: 136 findings, 0 kept, gate exit 0.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@gitar-bot

gitar-bot Bot commented Jul 28, 2026

Copy link
Copy Markdown
Code Review ✅ Approved

Reconciles the Hypatia governance baseline with current scanner rules by fixing 15 findings directly in code and baselining 70 remaining entries. No issues found.

Auto-approved and auto-merge armed: No blocking issues found.
Please see Auto-approve Docs for details on setting custom approval criteria. — merges when pipeline and required approvals pass.

Options

Auto-apply is off → Gitar will not commit updates to this branch.
Display: compact → Showing less information.

Comment with these commands to change the behavior for this request:

Auto-apply Compact
gitar auto-apply:on         
gitar display:verbose         

Was this helpful? React with 👍 / 👎 | Gitar

@gitar-bot
gitar-bot Bot enabled auto-merge (squash) July 28, 2026 15:33

@gitar-bot gitar-bot Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Gitar has auto-approved this PR and enabled auto-merge (configure)

@gitar-bot gitar-bot Bot added the gitar-approved Added by Gitar label Jul 28, 2026
@hyperpolymath

Copy link
Copy Markdown
Owner Author

Do not merge on a green board — every gate in this repo is dead

gh pr checks on this PR shows a single passing check (Gitar). That is not a green board: all 16 workflow runs on this branch are startup_failure, and a workflow that fails at startup registers no check run at all, so it cannot appear as missing.

gh run list --branch fix/governance-hypatia-baseline
pull_request  completed/startup_failure  Governance
pull_request  completed/startup_failure  Rust CI
pull_request  completed/startup_failure  CodeQL Security Analysis
... 16/16

It is repo-wide and predates this branch

main flipped wholesale on 2026-07-27 22:45. The run immediately before (834ee82, the Dependabot actions bump) produced real results — a normal mix of success and failure. Every run since (0823afc onward) is startup_failure, across all 34 workflows.

The commit correlation is misleading: 834ee82..0823afc touches only dogfood-gate.yml plus two new vendored scripts, which cannot break unrelated workflows.

What I ruled out

Hypothesis Result
Invalid workflow YAML No — all 33 files strict-parse; a minimal probe workflow (one SHA-pinned actions/checkout + echo) also startup_failured
Dependabot wrote unresolvable SHAs No — every bumped SHA resolves; actions/checkout@3d3c42e5… is exactly the v7.0.1 tag
Billing / private-repo block No — repo is public, enabled: true, not archived
Ruleset injecting a broken required workflow No — no workflows rule in either ruleset
Account-wide outage Noechidnabot CI is healthy right now; standards is only partly affected

The remaining difference

repo allowed_actions sha_pinning_required state
echidna selected true 100% startup_failure
echidnabot all false healthy
standards selected true mixed

The repo-level Actions policy is the only variable left, and the minimal probe proves it is not about any individual action reference (github_owned_allowed is true, so actions/checkout is permitted).

I stopped here deliberately. Confirming it means toggling sha_pinning_required and re-running the probe, and I am not willing to weaken a security control on a public repo without the owner saying so — especially one that looks deliberately set to match estate SHA-pinning doctrine.

Consequence

All four PRs (#328#331) report MERGEABLE / BLOCKED: the Base ruleset requires status checks that can never arrive while startup fails. Merging any of them today means merging with zero gates actually run.

#328 itself is verified independently — the hypatia gate was reproduced offline against scanner 3b04900 with the exact governance-reusable.yml invocation (136 findings, 0 kept, exit 0) — but that verification is mine, not CI's.

Suggested order once Actions are alive: land #328 first (so the baseline is in place), then #329/#330/#331, re-running the gates on each.

@hyperpolymath
hyperpolymath disabled auto-merge July 28, 2026 16:27
@hyperpolymath
hyperpolymath merged commit ea5af2f into main Jul 28, 2026
1 check passed
@hyperpolymath
hyperpolymath deleted the fix/governance-hypatia-baseline branch July 28, 2026 16:28
hyperpolymath added a commit that referenced this pull request Jul 28, 2026
Turns the Pages output at **nesy-prover.dev** from a README dump into an
actual site: landing page, platform docs, an accurate API reference, and
a working in-browser Coq playground.

## Why the build changed

`pages.yml` built from `src/` — the *Rust source tree* — with a README
shim. That published five stray `src/**/README.html` pages to the live
site and set the Ddraig base URL to `hyperpolymath.github.io/echidna`,
so every canonical URL, sitemap entry and feed link pointed at the wrong
host. It now builds from a dedicated `site/` tree with the custom domain
as base, and copies the playground in with `cp` (Ddraig's `copyTree` is
text-only and corrupts binaries).

No `CNAME` file is needed: `build_type` is `workflow`, so the custom
domain lives in the Pages settings, where it is already verified.

## The API reference was wrong in every example

An adversarial review confirmed the pages inherited from
`docs-site/content` documented an API that does not exist:

- GraphQL documented at `/graphql` and `/playground` — both 404; the
service serves POST **and** the playground at `/`
- `suggestTactics` shown as a Query; it is a **Mutation** taking
`(prover, context, goalState)`. The query is `suggestTacticsByProofId`
- argument names wrong throughout (`proofState(sessionId:)` → `id`,
`submitProof(proverKind:)` → `prover`+`goal`, `applyTactic(sessionId:)`
→ `proofId`+`tactic`+required `args`)
- REST documented `timeout_ms`; the field is `timeout_seconds` (serde
silently drops the unknown key, so an operator's timeout vanishes — and
30000 s vs ms is a 1000× trap if they only fix the name). Tactic body is
`{name, args}`, not `{tactic}`
- gRPC showed a `SubmitProofResponse` and a `ProofUpdate` shape that are
not in the proto
- every quick-start `curl` used `https://` against services that bind
**plain HTTP** on loopback

All three interface references are rewritten from source, and a new
**core server reference** documents what is actually deployed at
`api.nesy-prover.dev`, taken from the route table and types in
`src/rust/server.rs`. The stale 30-row prover table claiming every
backend is tier "core" is gone; the canonical tier table is linked
instead.

## Playground

`echidna-playground/index.html` never loaded jsCoq at all — the init
block was commented out behind an `npm install` note. It now loads jsCoq
0.17.1 from jsdelivr as an ES module. The bundled demo was Mathematical
Components, which the CDN package does not ship, so the example is a
stdlib-only induction proof (`n + 0 = n`) that actually runs.

The load-failure banner uses a **dynamic** `import()` inside
`try`/`catch`: with a static import, a failed CDN fetch aborts module
instantiation, so the handler that reveals the banner would never run —
in exactly the case the banner exists for.

## Verification

- `ddraig build` locally: **6/6 pages `[a11y ok]`** (the SSG hard-fails
on multiple h1s, skipped heading levels, or missing alt text)
- every absolute internal link resolves in the assembled artifact,
including `/playground/`
- the playground references no asset beyond the `styles.css` shipped
alongside it
- `sitemap.xml` entries use `https://nesy-prover.dev`
- hypatia governance gate re-run on this branch **merged with #328**:
136 findings, 0 kept, exit 0 — this branch introduces no new findings

## Note on DNS (separate from this PR)

`nesy-prover.dev` currently resolves to Cloudflare proxy IPs and does
not answer (`curl` hangs), while `hyperpolymath.github.io/echidna` 301s
to it. The apex records need reconciling to GitHub Pages before this
site is reachable.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

gitar-approved Added by Gitar

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant