fix(governance): reconcile hypatia baseline with current scanner ruleset - #328
Conversation
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>
Code Review ✅ ApprovedReconciles the Hypatia governance baseline with current scanner rules by fixing 15 findings directly in code and baselining 70 remaining entries. No issues found.
OptionsAuto-apply is off → Gitar will not commit updates to this branch. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
Do not merge on a green board — every gate in this repo is dead
It is repo-wide and predates this branch
The commit correlation is misleading: What I ruled out
The remaining difference
The repo-level Actions policy is the only variable left, and the minimal probe proves it is not about any individual action reference ( I stopped here deliberately. Confirming it means toggling ConsequenceAll four PRs (#328–#331) report #328 itself is verified independently — the hypatia gate was reproduced offline against scanner 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. |
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.
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, WF017secret_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_apifrom 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:
timeout-minutesonserver-boot-gate,fly-deploy,s4-loop,push-email-notifyinstant-sync.yml: gate therepository-dispatchstep behind aFARM_DISPATCH_TOKENpresence check (WF017)codeql.yml: scan theactionslanguage alongsidejavascript-typescript.claude/CLAUDE.md: reword the.scm-deprecation paragraph so it stops tripping SD007 on its own migration examplesffi/zig/src/{typell,overlay,boj}.zig: makeerror_bufsentinel-terminated ([N:0]u8) and drop the@ptrCast— writers always NUL-terminate, so the coercion is sound70 findings baselined as 44 acknowledged entries (medium
deprecated_apipending the ReScript→AffineScript migration, FFI-boundaryunsafe_block/as_ptr/expect_in_hot_pathdebt, and two SD022 false positives that cite external-corpora paths).Verification
Reproduced the CI job offline against hypatia
3b04900using the exactgovernance-reusable.ymlinvocation (HYPATIA_FORMAT=json,BLOCKING_THRESHOLD=info, the same jq path relativisation, thenapply-baseline.sh … blocking):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.