fix(proofs): restore the proof gate (dedupe allTake, read idris2 pin, run on every PR) by hyperpolymath · Pull Request #350 · hyperpolymath/boj-server

hyperpolymath · 2026-10-07T07:15:37Z

Summary

Restores the Idris2 proof gate. Closes #343.

The core ABI did not typecheck, because SafetyLemmas.idr defined allTake twice.
proofs.yml asked asdf to install Idris2 version "".
The changes path-skip let the gate report green without checking anything.

📌 New pins

Head SHA: ec79cd6. No action, lockfile or container pins are added or changed. The Idris2 version is now read from the existing .mise.toml pin (idris2 = "0.8.0"); that pin itself is unchanged.

Changes

src/abi/Boj/SafetyLemmas.idr: delete the second allTake (formerly ~L235–243). The first, at :146, is kept and is equivalent.
.github/workflows/proofs.yml:
- Read the Idris2 pin from .mise.toml. .tool-versions was converted to .mise.toml in 4d1fe0c. A missing or malformed pin now fails the step with an ::error annotation instead of continuing.
- Remove the changes job and the needs/if path-skip on trusted-base and typecheck. Proofs Gate is not a required check (the effective rules require only scan / gitleaks), so always running it blocks no PR.
- Header comments updated to match.
README.adoc, README.md, site/index.html: drop the "core does not currently typecheck" caveat (added in docs: Proven/Witnessed/Trusted ladder; correct believe_me and annotation claims #344) and the stale "job is path-filtered" note. README.md was edited by hand to mirror README.adoc; README Derive's freshness check verifies it.

RSR Quality Checklist

Required

Tests pass: locally, idris2 --typecheck boj.ipkg in src/abi builds 17/17 modules with rc 0 (local Idris2 is 0.7.0; CI uses the 0.8.0 pin, and this PR's own Proofs Gate run is the evidence for that). bash scripts/check-trusted-base.sh reports OK: 4 sanctioned axioms.
Code is formatted: no formatter is configured for Idris2 or workflow YAML here. The YAML parses (js-yaml).
Linter is clean: no local linter applies. CI scanners report on this PR.
No banned language patterns: no new code beyond a deletion in Idris2 and shell inside a workflow step.
No unsafe blocks: there is no Rust or Zig in this change.
No banned functions: the change only deletes a duplicate lemma. The axiom count is unchanged at 4 (trusted-base audit).
SPDX headers: the modified files keep theirs. No new files.
No secrets.

As Applicable

.machine_readable/*: not updated, and A2ML is retired estate-wide.
Documentation updated: README.adoc, README.md and site/index.html.
TOPOLOGY.md: architecture is unchanged.
CHANGELOG: CI and proof-hygiene fix, not user-facing.
New dependencies: none.
ABI changes validated: the src/abi/ package typechecks. ffi/zig/ is untouched; the deleted definition was a duplicate.

Testing

cd src/abi && idris2 --typecheck boj.ipkg: 17/17 modules, rc 0.
bash scripts/check-trusted-base.sh: "OK: no undocumented unsound constructs; 4 sanctioned class-(J) axioms".
Pin step, run on its own: on this tree it prints idris2=0.8.0, rc 0. On a .mise.toml without an idris2 line it emits ::error with rc 1.
This PR's Proofs Gate run must show "Idris2 type-check (core + all cartridge ABIs)" executing under 0.8.0, not skipped.

🤖 Generated with Claude Code

https://claude.ai/code/session_019j8She9eTFx54r6aL6sCHP

… pin, run on every PR - SafetyLemmas.idr defined `allTake` twice; the core package failed `idris2 --typecheck boj.ipkg`. Keep the first definition (:146). - proofs.yml read the Idris2 version from .tool-versions, which was converted to .mise.toml (4d1fe0c), so asdf was asked to install "". Read the pin from .mise.toml and fail loudly on a missing pin. - Drop the `changes` path-skip: a skipped proof job reported success without checking anything. Proofs Gate is not a required check, so always running it blocks nothing. - Remove the "does not typecheck" caveat from README.adoc/README.md and site/index.html, and the stale "path-filtered" note. Closes #343 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019j8She9eTFx54r6aL6sCHP

coderabbitai · 2026-10-07T07:15:50Z

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 37 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Advanced
Run ID: d62dcbe3-6fb3-4a6e-88d3-efc4fda7ba4d

📥 Commits

Reviewing files that changed from the base of the PR and between 0e700c9 and 740b4b2.

📒 Files selected for processing (5)

.github/workflows/proofs.yml
README.adoc
README.md
site/index.html
src/abi/Boj/SafetyLemmas.idr

Autopilot · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

_{Comment @coderabbitai help to get the list of available commands.}

github-actions · 2026-10-07T07:16:33Z

🏁 path-claims bench

Commit ecf2870

Numbers

path-claims bench  (node v22.23.3)

  scenario                                              iters       ms        ns/op          ops/s
  --------------------------------------------------------------------------------------------------------------
  register: 10 active claims, 3 new paths               50000 iters    195 ms      3.91 µs/op    255.7k ops/s
  register: 100 active claims, 3 new paths              20000 iters    315 ms     15.77 µs/op     63.4k ops/s
  register: 1000 active claims, 3 new paths              5000 iters    943 ms    188.64 µs/op      5.3k ops/s
  register: 100 active claims, 20 new paths              5000 iters    365 ms     73.19 µs/op     13.7k ops/s

  pathsOverlap: deep diverge at segment 4             1000000 iters    162 ms     163.0 ns/op     6.14M ops/s
  pathsOverlap: short prefix match                    1000000 iters    134 ms     134.1 ns/op     7.46M ops/s

  refresh (existing claim)                             100000 iters     10 ms     109.9 ns/op     9.10M ops/s
  list (100 active claims)                              50000 iters    290 ms      5.80 µs/op    172.3k ops/s

  (Bench numbers depend on host; use deltas across commits, not absolute values.)

Host-dependent — compare deltas across commits, not absolute values.

github-actions · 2026-10-07T07:16:43Z

🔍 Hypatia Security Scan

Findings: 113 issues detected

Severity	Count
🔴 Critical	10
🟠 High	20
🟡 Medium	83

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Job `sonarqube` in build.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sonarqube"
  },
  {
    "reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/label-triage.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "triage"
  },
  {
    "reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/labels.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sync"
  },
  {
    "reason": "Job `deploy` in pages-deploy.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/pages-deploy.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "deploy"
  },
  {
    "reason": "Step uses `peter-evans/repository-dispatch` with `token: ${{ secrets.FARM_DISPATCH_TOKEN }}` but has no `if: secrets.FARM_DISPATCH_TOKEN != ''` gate. On repos where the secret hasn't been propagated the action fails on every push, red-maining the repo. Add the step-level gate (or env+if pattern) so the missing-secret path is a clean skip instead of a red.",
    "type": "secret_action_without_presence_gate",
    "file": ".github/workflows/instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high",
    "fix_recipe": "add_secret_presence_gate"
  },
  {
    "reason": "codeql.yml does not list `language: actions` in its matrix, but the repo has workflow files. CodeQL's `actions` language scans workflow YAML for injection and other CI/CD-specific weaknesses — every repo with workflows benefits. Add an entry to `matrix.include` with `language: actions` + `build-mode: none`.",
    "type": "codeql_missing_actions_language",
    "file": ".github/workflows/codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "fix_recipe": "add_codeql_actions_language"
  },
  {
    "line": 39,
    "reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/labels.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 46,
    "reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/push-email-notify.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 32,
    "reason": "job in .github/workflows/build.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/build.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 44,
    "reason": "job in .github/workflows/container-publish.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/container-publish.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

github-actions · 2026-10-07T07:17:48Z

🔍 Hypatia Security Scan

Findings: 113 issues detected

Severity	Count
🔴 Critical	10
🟠 High	20
🟡 Medium	83

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Job `sonarqube` in build.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sonarqube"
  },
  {
    "reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/label-triage.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "triage"
  },
  {
    "reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/labels.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sync"
  },
  {
    "reason": "Job `deploy` in pages-deploy.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/pages-deploy.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "deploy"
  },
  {
    "reason": "Step uses `peter-evans/repository-dispatch` with `token: ${{ secrets.FARM_DISPATCH_TOKEN }}` but has no `if: secrets.FARM_DISPATCH_TOKEN != ''` gate. On repos where the secret hasn't been propagated the action fails on every push, red-maining the repo. Add the step-level gate (or env+if pattern) so the missing-secret path is a clean skip instead of a red.",
    "type": "secret_action_without_presence_gate",
    "file": ".github/workflows/instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high",
    "fix_recipe": "add_secret_presence_gate"
  },
  {
    "reason": "codeql.yml does not list `language: actions` in its matrix, but the repo has workflow files. CodeQL's `actions` language scans workflow YAML for injection and other CI/CD-specific weaknesses — every repo with workflows benefits. Add an entry to `matrix.include` with `language: actions` + `build-mode: none`.",
    "type": "codeql_missing_actions_language",
    "file": ".github/workflows/codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "fix_recipe": "add_codeql_actions_language"
  },
  {
    "line": 39,
    "reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/labels.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 46,
    "reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/push-email-notify.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 32,
    "reason": "job in .github/workflows/build.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/build.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 44,
    "reason": "job in .github/workflows/container-publish.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/container-publish.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Merge branch 'main' into fix/proof-gate

740b4b2

hyperpolymath enabled auto-merge (squash) October 7, 2026 07:16

hyperpolymath disabled auto-merge October 7, 2026 07:17

hyperpolymath merged commit 14386f3 into main Oct 7, 2026
53 of 55 checks passed

hyperpolymath deleted the fix/proof-gate branch October 7, 2026 07:17

Navigation Menu

Repository navigation

fix(proofs): restore the proof gate (dedupe allTake, read idris2 pin, run on every PR) - #350

fix(proofs): restore the proof gate (dedupe allTake, read idris2 pin, run on every PR)#350
hyperpolymath merged 2 commits into
mainfrom
fix/proof-gate

hyperpolymath commented Oct 7, 2026

Uh oh!

coderabbitai Bot commented Oct 7, 2026 •

edited

Loading

Review limit reached

Uh oh!

github-actions Bot commented Oct 7, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented Oct 7, 2026

Summary

📌 New pins

Changes

RSR Quality Checklist

Required

As Applicable

Testing

Uh oh!

coderabbitai Bot commented Oct 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review limit reached

Uh oh!

github-actions Bot commented Oct 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🏁 path-claims bench

Uh oh!

github-actions Bot commented Oct 7, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

github-actions Bot commented Oct 7, 2026

🔍 Hypatia Security Scan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

coderabbitai Bot commented Oct 7, 2026 •

edited

Loading

github-actions Bot commented Oct 7, 2026 •

edited

Loading