Repository navigation
proofs: make the repo's own modules pass the strict flag set - #355
Merged
Merged
Conversation
Fixes the repo-side sites the strict-flag survey found: - EchoExampleParser.parses-aux: the LP clause takes a variable depth but came after clauses that split on the depth, so --exact-split rejected it. Put it first, so the case tree splits on the token first. The function is unchanged. - EchoTropical._⊕_: the clause `m ⊕ zero = m` overlapped `zero ⊕ n`. It is now `suc m ⊕ zero = suc m`; the two agree at zero. - EchoBitNarrowingNumeric: stdlib's deprecated ≤-step, fatal under -W error, is replaced by m≤n⇒m≤1+n. Remaining strict failures, outside this repo: EchoCNOBridge and EchoThermodynamicsArbitrary import absolute-zero's CNO, which does not declare --cubical-compatible. That fix belongs in absolute-zero. Co-Authored-By: Claude Opus 5.5 <[email protected]> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
The strict re-sweep found one more site that the earlier parses-aux failure had masked: second-token's catch-all clause. List its two short-list cases explicitly. Behaviour is unchanged. Co-Authored-By: Claude Opus 5.5 <[email protected]> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
Contributor
|
Warning Review limit reachedYou'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 27 minutes. View limit details
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. Comment |
🔍 Hypatia Security ScanFindings: 38 issues detected
View findings[
{
"reason": "Required file missing",
"type": "missing",
"file": "0-AI-MANIFEST.a2ml",
"level": "epi",
"action": "create",
"rule_module": "root_hygiene",
"severity": "high",
"evidence": [
{
"span": {
"file": "0-AI-MANIFEST.a2ml",
"end_line": 0,
"start_line": 0
},
"rule": "root_hygiene/missing",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"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",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "triage",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"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",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "sync",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"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",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 39,
"start_line": 39
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 53,
"reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 53,
"start_line": 53
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 87,
"reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/hypatia-scan.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/hypatia-scan.yml",
"end_line": 87,
"start_line": 87
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"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",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/push-email-notify.yml",
"end_line": 46,
"start_line": 46
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 34,
"reason": "workflow .github/workflows/labels.yml:34 job `sync` has no `timeout-minutes:` — defaults to 360 min on hang",
"type": "WH006",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 34,
"start_line": 34
},
"rule": "workflow_hardening/WH006",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 48,
"reason": "workflow .github/workflows/label-triage.yml:48 job `triage` has no `timeout-minutes:` — defaults to 360 min on hang",
"type": "WH006",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 48,
"start_line": 48
},
"rule": "workflow_hardening/WH006",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": null,
"reason": "workflow .github/workflows/hypatia-scan.yml uploads SARIF to code scanning but masks the scanner's failure (`|| true` / `|| echo 0`) and never asserts the findings artefact is a non-empty array. When the scanner fails, this uploads a SARIF with zero results, and GitHub AUTO-CLOSES every previously-open alert for that category — silently, with the job green.",
"type": "WH014",
"file": ".github/workflows/hypatia-scan.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "high",
"evidence": [
{
"span": {
"file": ".github/workflows/hypatia-scan.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_hardening/WH014",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
marked this pull request as ready for review
October 26, 2026 22:26
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
hyperpolymath
enabled auto-merge (squash)
October 26, 2026 22:29
hyperpolymath
disabled auto-merge
October 27, 2026 00:08
Contributor
|
Add Carrot credits or activate Agent usage billing to use Autofix |
hyperpolymath
added a commit
that referenced
this pull request
Oct 27, 2026
…357) ## Summary #355 made the code compatible with the strict Agda flag set. This PR declares the flags in the files, which is what downstream repos need. `--cubical-compatible` is coinfective: a module that declares it may only import modules that also declare it. choreographic-types imports `experimental/echo-additive/Grade.agda`, and through it `EchoGraded`, `Echo`, `EchoCharacteristic` and `EchoResidue`. It cannot adopt the strict set until these modules declare the flag. - **141 modules:** the `OPTIONS` pragma gains `--cubical-compatible --exact-split --no-sized-types --no-guardedness`, keeping `--safe --without-K`. - **6 modules left unchanged:** | Module | Why | |---|---| | `EchoCNOBridge`, `EchoThermodynamicsArbitrary` | Import absolute-zero's `CNO`, which does not declare `--cubical-compatible` yet | | `All`, `Smoke` | Import those two | | `EchoImageFactorizationPropCubical` | The `--cubical` island | | `EchoImageFactorizationPropPostulated` | The quarantined postulate block | A module without the flag may still import modules that have it, so these all keep building. Once absolute-zero lands the flag, a follow-up adds it to the first four. - **`scripts/kernel-guard.sh`:** the safety-relaxing-flag check matched the substring `--cubical` inside `--cubical-compatible`, which strengthens safety rather than relaxing it. It now matches whole flags only. ## Verification (Agda 2.6.3, stdlib 2.3) - Every CI root compiles with `--ignore-interfaces`: - `All` - `Smoke` - `characteristic/All` - `examples/All` - `experimental/echo-additive/All` - `tutorial/All` compiles. - `scripts/kernel-guard.sh`: PASS. Negative controls: planting `--cubical`, `--sized-types` or `--guardedness` in `Echo.agda` still fails the guard. - `tools/check-guardrails.sh`: OK (137 modules). - A trial build of choreographic-types with these pragmas, plus strict pragmas on resource-algebra and epistemic-types, passes all of its gates: 17 modules, 5 rejections, and the minimal-laws certificate. Companion PR: epistemic-types (same change). --- _Generated by [Claude Code](https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV)_ Co-authored-by: Claude <[email protected]>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR fixes the four echo-types sites that failed the strict Agda flag set. No theorem statements change. These are clause splits plus one stdlib rename.
The strict set:
OPTIONSpragma:--safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness.--double-check -W error -W noUnsupportedIndexedMatch.EchoExampleParser.agda(parses-aux)--exact-splitLPclause first so the case tree splits on the token first.EchoExampleParser.agda(second-token)--exact-split[]and(_ ∷ [])clauses. This site was hidden behind theparses-auxfailure.EchoTropical.agda(_⊕_)--exact-splitm ⊕ zero = mbecomessuc m ⊕ zero = suc m.EchoBitNarrowingNumeric.agda-W error≤-stepwithm≤n⇒m≤1+n.Verification (Agda 2.6.3, stdlib 2.3)
agda proofs/agda/All.agdaandagda proofs/agda/Smoke.agdaboth exit 0 under the repo's current flags.scripts/kernel-guard.shPASS.tools/check-guardrails.shOK (137 modules).Strict sweep, every module compiled on its own with the strict set: 2 sites remain, both outside this repo:
EchoCNOBridge.agda:35EchoThermodynamicsArbitrary.agda:76Both import absolute-zero's
CNO, which does not declare--cubical-compatible. That flag is coinfective: a module using it can only import modules that also use it. So the fix belongs in absolute-zero, not here.This PR does not add the strict pragmas to the repo's files. It only makes the code compatible with them.
Generated by Claude Code