ci: add build/test/proof gate; fix stale Hypatia & Scorecard reusable pins by hyperpolymath · Pull Request #52 · hyperpolymath/oblibeny

hyperpolymath · 2026-06-04T01:55:27Z

Summary

Root-cause fixes for the repo's red CI, diagnosed from the live workflow runs on main (the #51 merge commit d1deb29). Three workflows were red; here is each, with its true cause:

Workflow	Symptom	Root cause	Fix
Hypatia Security Scan	run fails, 0 jobs	reusable pinned at a stale SHA (`97df762`) that can't start	re-pin to `861b5e9`
Scorecards	`startup_failure` (pre-existing, also on `acfeec7`)	reusable pinned at a stale SHA (`e0caf11`)	re-pin to `861b5e9`
Instant Sync	`##[error]Bad credentials`	`FARM_DISPATCH_TOKEN` secret expired/invalid	⚠️ maintainer must rotate the secret — not fixable in-repo
(missing entirely)	broken proofs merged unnoticed	no build/test/proof CI existed	new `ci.yml`

The PR's own check runs were already all green (Governance, Secret-Scanner, Semgrep, CodeQL); these reds are the standalone wrappers + the absent build gate.

Changes

`ci.yml` (new) — the gate this repo never had

This is the root reason non-compiling Idris stubs, a false believe_me-masked theorem, and a type-safety hole all merged before: nothing ever built or tested the code. Two parallel jobs:

OCaml — dune build + the 24-case conformance suite.
Idris2 proofs — bootstrap Idris2 0.7.0 from source (Chez), idris2 --build src/abi/oblibeny-abi.ipkg (type-check = proof), then a soundness escape-hatch guard.

Self-contained (no external reusable dependency), checkout action SHA-pinned, minimal contents: read permissions. Verified locally end-to-end (./scripts/check-proofs.sh), including a clean Idris build with only bin on PATH (mirrors the CI step).

Re-pin stale reusables

hypatia-scan.yml and scorecard.yml re-pinned from their stale SHAs to 861b5e911d9e5dcfb3c0ab3dd2a9a3c8fd0a1613 — the same SHA the green governance workflow already uses. Confirmed both hypatia-scan-reusable.yml and scorecard-reusable.yml exist at that SHA with on: workflow_call. (Governance and Secret-Scanner, pinned to current SHAs, were already green — only these two had drifted.)

⚠️ Needs maintainer action (out of repo scope)

Instant Sync fails with Bad credentials dispatching to the private hyperpolymath/.git-private-farm: the FARM_DISPATCH_TOKEN secret is expired/invalid. No in-repo change can mint a valid credential — please rotate the secret. (I deliberately did not mask it with continue-on-error, since that would silently hide cross-forge mirroring being down.)

🤖 Draft — opened for review.

https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ

Generated by Claude Code

…bles Root-cause fixes for the repo's red CI (diagnosed from the live runs): - ci.yml (new): the build/test/proof gate this repo never had -- the reason non-compiling Idris stubs, a false `believe_me`-masked theorem, and a type-safety hole all merged unnoticed. Two parallel jobs: OCaml build + the 24-case conformance suite; and Idris2 0.7.0 (Chez bootstrap) type-check (= proof) of the ABI layer + a soundness escape-hatch guard. Self-contained; checkout action SHA-pinned; minimal read-only permissions. - hypatia-scan.yml, scorecard.yml: the standards reusables were pinned at stale SHAs (97df762 / e0caf11) that fail to start (0 jobs / startup_failure). Re-pin both to 861b5e9 -- the same confirmed-good SHA the green governance workflow already uses; both reusable files exist there with `on: workflow_call`. Not fixable from in-repo (flagged for the maintainer): Instant Sync fails with "Bad credentials" -- the FARM_DISPATCH_TOKEN secret is expired/invalid and must be rotated; no in-repo change can mint a valid credential. https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ

github-actions · 2026-06-04T01:56:19Z

🔍 Hypatia Security Scan

Findings: 90 issues detected

Severity	Count
🔴 Critical	12
🟠 High	39
🟡 Medium	39

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Stray AI.a2ml in root -- use 0-AI-MANIFEST.a2ml only",
    "type": "banned",
    "file": "AI.a2ml",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "missing_timeout_minutes",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "missing_timeout_minutes",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "missing_timeout_minutes",
    "file": "instant-sync.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "missing_timeout_minutes",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "missing_timeout_minutes",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_timeout_minutes",
    "file": "secret-scanner.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

The re-pinned Hypatia scan now runs (advisory) and surfaced actionable hygiene. Fix the tractable, unambiguous ones: - timeout-minutes added to every *real* job (ci.yml x2, codeql, semgrep, instant-sync). The five reusable-caller wrappers (governance, hypatia-scan, mirror, scorecard, secret-scanner) cannot carry timeout-minutes on a `uses:` job — GitHub forbids it — so Hypatia's flag on those is a false positive and is intentionally left unchanged. - AI.a2ml -> 0-AI-MANIFEST.a2ml: oblibeny carried the legacy manifest name while the rest of the estate uses 0-AI-MANIFEST.a2ml. Hypatia flagged the stray name with action "delete", but 0-AI-MANIFEST.a2ml did not exist, so deleting would have removed the only manifest — the correct fix is a rename (content preserved; no in-repo references). Deferred (ambiguous / needs maintainer intent, surfaced separately): six submodule gitlinks (fs, obli-fs, transpiler, ssg, riscv-dev-kit, obli-riscv-dev-kit) are committed with no .gitmodules mapping at all. https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ

github-actions · 2026-06-04T02:03:27Z

🔍 Hypatia Security Scan

Findings: 90 issues detected

Severity	Count
🔴 Critical	12
🟠 High	38
🟡 Medium	40

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in governance.yml",
    "type": "missing_timeout_minutes",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "missing_timeout_minutes",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "missing_timeout_minutes",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "missing_timeout_minutes",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_timeout_minutes",
    "file": "secret-scanner.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "secret_action_without_presence_gate",
    "file": "instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Repository has 5 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD001 -- Hypatia structural_drift: SD001 -- 12 day(s) old [STALE]",
    "type": "CSA001",
    "file": ".machine_readable/PLAYBOOK.scm",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD001 -- Hypatia structural_drift: SD001 -- 12 day(s) old [STALE]",
    "type": "CSA001",
    "file": ".machine_readable/NEUROSYM.scm",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD001 -- Hypatia structural_drift: SD001 -- 12 day(s) old [STALE]",
    "type": "CSA001",
    "file": ".machine_readable/AGENTIC.scm",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…gate instant-sync (#53) ## Summary Follow-up to #52. After the reusable re-pins landed, I verified `main`'s post-merge CI and found **Hypatia is now green** (re-pin worked) but **Scorecards still `startup_failure`** — proving its cause was *not* the stale SHA. Root-caused and fixed here, plus the one genuinely-actionable Hypatia HIGH. ## Scorecard `startup_failure` — real root cause The `scorecard-reusable.yml` declares top-level `permissions: contents: read`. But this repo's wrapper sets **job-level** `permissions: { security-events: write, id-token: write }` (added in #47), and a job-level permissions block sets every unlisted permission to `none` — so `contents` became `none`. A reusable workflow that requests a permission its caller didn't grant **fails at startup** (0 jobs), which is exactly the symptom — and it persisted across the re-pin (unlike Hypatia, whose wrapper grants `contents: read` at workflow level). **Fix:** add `contents: read` to the `analysis` job's permissions (verified against the reusable's declared `permissions:` at `861b5e9`). ## instant-sync — presence gate Per Hypatia's `secret_action_without_presence_gate` (HIGH), the `repository-dispatch` step is now gated on token presence (job `env` + `if: ${{ env.FARM_DISPATCH_TOKEN != '' }}`), so absent-token contexts skip cleanly. ⚠️ This does **not** make Instant Sync green by itself: the configured `FARM_DISPATCH_TOKEN` returns `Bad credentials` and **must be rotated by the maintainer** — no in-repo change can mint a valid credential. ## Still needs a maintainer decision (surfaced, not touched — ambiguous/destructive) - **6 submodule gitlinks with no `.gitmodules`** (`fs`, `obli-fs`, `transpiler`, `ssg`, `riscv-dev-kit`, `obli-riscv-dev-kit`) — all empty, pointing at commits with no URL. Either restore a `.gitmodules` (if real submodules) or `git rm --cached` them (if accidental). Needs your intent. - **Stale remote branches** (`GS007`): e.g. `cicd/codeql-cron-monthly`, `claude/codeql-actions-scan`, `claude/proof-debt-ledger`. Branch deletion is destructive — your call. - **`CSA001` structural-drift** alerts on `.machine_readable/{PLAYBOOK,NEUROSYM,AGENTIC}.scm` (stale prior-run code-scanning alerts) — schema work, needs context. - The other Hypatia findings are advisory; the 5 remaining `missing_timeout_minutes` flags are **false positives** (reusable-caller jobs cannot carry `timeout-minutes`). 🤖 Draft — opened for review. https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ --- _Generated by [Claude Code](https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ)_ Co-authored-by: Claude <noreply@anthropic.com>

…ipline (#55) ## Summary Implements the **echo↔reversibility** language feature you approved (design: *overwrite/drop discipline*; scope: *echoes*). It type-enforces the symmetry the Idris bridge proved — **reversible ⟺ no residue; irreversible ⟺ an echo** — so a residue can no longer be silently thrown away. A non-copyable `echo` is now **linear (consumed exactly once)**: - the existing affine rule already forbade a *second* use; - this adds the other half — it must be consumed (projected via `echo_visible`/`echo_witness`) **at least once** before it is **reassigned** (overwrite) or **goes out of scope** (drop). Discarding a non-copyable residue without consuming it is now a type error: *"an irreversible step must account for an echo of what it loses."* ## What changed - **`lib/typecheck.ml`** — a `live_echoes` tracker beside `affine_used`: binding a non-copyable echo arms it; using/projecting consumes it; `SAssign` and function-exit raise if a still-live residue would be discarded; `SIf`/`SForRange` snapshot it like the affine set. - **Scope & boundary** (deliberately narrow, still "no rhino"): non-copyable echo bindings only. **Copyable** echoes (`echo[i64,i64]`) and the **reversible primitives** (`incr`/`decr`/`swap`/`^=`) are exempt — they lose nothing. Echo still does **not** participate in reversibility balancing; the connection is one-directional (loss ⇒ must-capture), not a new reversibility mechanism. Generalising to other non-copyable carriers (structs/arrays) is a possible follow-up. - **Tests** — +3 conformance cases: *drop without consume rejected*, *overwrite live value rejected*, *overwrite after consume ok*. Suite **24 → 27, all green**. Existing programs are unaffected (verified up front: nothing in the tests or examples reassigns or drops a non-copyable echo). - **`docs/echo-alignment.md`** — records the landed discipline + its boundary. ## Verify ``` dune build && dune runtest # 27 conformance tests ``` (Idris ABI proofs untouched; the `ci.yml` gate from #52 builds + type-checks them on this PR too.) 🤖 Draft — opened for review. https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ --- _Generated by [Claude Code](https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ)_ Co-authored-by: Claude <noreply@anthropic.com>

…kly→monthly The Zig FFI layer was never built by CI (the #52 gate builds OCaml + Idris only), so it had accumulated compile errors. Verified with Zig 0.13.0 (zig ast-check + zig build-obj): zig build now compiles all sources and reaches the link step, failing only on the absent liboqs system library. ffi/zig/build.zig: - Four b.path("/usr/local/{lib,include}") calls PANIC under Zig 0.13 (b.path asserts a build-root-relative path). Switched to the correct .{ .cwd_relative = ... } LazyPath idiom for absolute system paths. ffi/zig/src/obli-pkg.zig (5 compile-error sites): - L209: catch block missing the labeled `break :blk` + `;`, so it couldn't yield the reopened file. Now `catch blk: { …; break :blk try …; }`. - L157/158: inner buf/msg shadowed outer locals — renamed to errbuf/errmsg. - L425/426: `_ = allocator; _ = pkg_path;` discarded params already in use. - L377/392/407: undeclared `mock_message`. Defined as a clearly-commented placeholder (= pkg_content) with a TODO(security): this verify path is an explicit MVP stub (zeroed test signatures) and the canonical signed payload (package bytes excluding embedded signature blocks) still needs deriving. Tidy: removed dead obli-pkg.zig.old; gitignore .zig-cache/ + zig-out/. CI: codeql schedule weekly ('0 6 * * 1') → monthly ('0 6 1 * *'). https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ

## Summary Repo-hygiene branch carrying three related cleanups (single dev branch per the session's branch policy). Two commits: ### 1. Metadata migration (`ae1d91f`) `.machine_readable/*.scm` (Guile Scheme) → `.machine_readable/6a2/*.a2ml` (estate-standard A2ML), matching the sibling repos and resolving the `structural_drift` (SD001) on the `.scm` files. Faithful translations (every real value preserved, nothing invented; all six parse as well-formed TOML/A2ML), rewritten `0-AI-MANIFEST.a2ml`, `AUTHORITY_STACK` fixed, legacy `.scm` removed. No code references the metadata; build/tests unaffected. ### 2. Zig FFI compile-fixes (`af855f8`) The Zig FFI (`ffi/zig/`) was **never built by CI** (the #52 gate builds OCaml + Idris only), so it had silently accumulated compile errors. Installed **Zig 0.13.0** and verified (`zig ast-check` + `zig build-obj`): `zig build` now compiles every source and reaches the link step, failing **only** on the absent `liboqs` system library (an external dep, not a code defect). - **`build.zig`**: four `b.path("/usr/local/{lib,include}")` calls **panic** under Zig 0.13 (`b.path` asserts a build-root-*relative* path) → switched to the correct `.{ .cwd_relative = … }` LazyPath idiom. - **`obli-pkg.zig`** (5 sites): missing labeled `break :blk` in a `catch` block (L209); two shadowed locals (L157/158); two pointless discards of in-use params (L425/426); and undeclared `mock_message` (L377/392/407) — now a clearly-commented placeholder with a **`TODO(security)`** (this verify path is an explicit MVP stub with zeroed test signatures; the canonical signed payload still needs deriving). - Removed dead `obli-pkg.zig.old`; gitignored `.zig-cache/` + `zig-out/`. ### 3. CI `codeql` schedule weekly (`0 6 * * 1`) → monthly (`0 6 1 * *`). ## Still open (need you) - **`.claude/CLAUDE.md`** still references the old `.scm` paths; editing it is blocked by the self-modification guardrail (twice) and needs a maintainer edit or a permission rule. - **Recommended follow-up**: add a lightweight Zig step to CI (`zig ast-check` over `ffi/zig`) so this layer can't silently rot again — happy to add it. 🤖 Draft — opened for review. https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ --------- Co-authored-by: Claude <noreply@anthropic.com>

hyperpolymath marked this pull request as ready for review June 4, 2026 02:04

hyperpolymath merged commit de2468e into main Jun 4, 2026
21 checks passed

hyperpolymath deleted the claude/confident-shannon-xf0Td branch June 4, 2026 02:04

hyperpolymath mentioned this pull request Jun 4, 2026

ci: fix Scorecard startup_failure (missing contents:read) + presence-gate instant-sync #53

Merged

hyperpolymath mentioned this pull request Jun 4, 2026

feat(typecheck): non-copyable echoes are linear — overwrite/drop discipline #55

Merged

hyperpolymath mentioned this pull request Jun 4, 2026

chore: metadata → 6a2/*.a2ml + Zig FFI compile-fixes + codeql cron #56

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

ci: add build/test/proof gate; fix stale Hypatia & Scorecard reusable pins#52

ci: add build/test/proof gate; fix stale Hypatia & Scorecard reusable pins#52
hyperpolymath merged 2 commits into
mainfrom
claude/confident-shannon-xf0Td

hyperpolymath commented Jun 4, 2026

Uh oh!

github-actions Bot commented Jun 4, 2026

Uh oh!

github-actions Bot commented Jun 4, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

hyperpolymath commented Jun 4, 2026

Summary

Changes

ci.yml (new) — the gate this repo never had

Re-pin stale reusables

⚠️ Needs maintainer action (out of repo scope)

Uh oh!

github-actions Bot commented Jun 4, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 4, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

`ci.yml` (new) — the gate this repo never had