Repository navigation
fix(SafeFiniteField): reject irreducibles not of degree n before reduction - #229
Merged
Merged
Conversation
…ction A polynomial of the wrong degree never cancels the top bit, so polyModReduction looped forever (e.g. irr = 0, 0x80 * 0x02) before the range check could run. bfMulWithIrr now returns Nothing unless bitLength irr == n + 1. Addresses CodeRabbit review on #228. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HZc76cZKg5tUgduxXGLQkD
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 12 minutes. View limit detailsLimit details: You’ve used the included review currently available. Review configuration: ⚙️ Run configuration
📒 Files selected for processing (1)
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 |
|
5 tasks
Contributor
|
Add Carrot credits or activate Agent usage billing to use Autopilot |
6 of 13 tasks
hyperpolymath
added a commit
that referenced
this pull request
Oct 7, 2026
## Summary Adds `AFFIRMATION.adoc`, the third file of the README / EXPLAINME / AFFIRMATION trio. It is a dated snapshot, open to refutation, of what proven can honestly claim at `main` **53600326**. It also lists what proven does **not** claim. - **Affirmed:** - `proven.ipkg` builds 305/305 modules in CI; - `proof-check (0.8.0)` passes; - there is no `believe_me` or `idris_crash` in code; - the false postulates are gone (#228, #229); - gitleaks is clean (#231). - **Not claimed:** - the README's "Mathematically proven" (PROOF-NEEDS samples about 3%); - the bodyless declarations that act as postulates; - 22 escape hatches; - the stubbed hash FFI; - `tests.ipkg` (it does not build); - about 79 unbuilt modules; - the weak or empty theorems; - the red checks on #230; - a pinned CI image. Where the README says more than this file, this file wins. Refs #230 ## Type of change - [ ] 🐛 Bug fix: no - [ ] ✨ New feature: no - [ ] 💥 Breaking change: no - [ ] 🕳️ Soundness fix: no - [x] 📖 Documentation - [ ] 🧹 Refactor / tech debt: no - [ ] ⚡ Performance: no - [ ] 🔧 Build / CI / tooling: no ## 📌 New pins Head SHA: **c25c3b5e302b9d66e1ae945ad47c72053c7d7234** None. This PR changes no action `uses:`, `actions.lock`, lockfile or container digest. ## How has this been verified? Every claim cites its evidence in the file: - **The build:** CI job `verify-idris-build` (id 112464109461) at 5360032 ends with `305/305: Building Proven`. - **The test build:** `idris2-ci.yml` at a32c3b6 gave proof-check success and build failure. The failure comes from the `tests.ipkg` renames in bdb1863. - **The escape-hatch counts:** `grep -rnw --include=*.idr <word> src`, with comment and doc-comment lines removed: - `believe_me` 0 (the 48 raw matches are all comments); - `idris_crash` 0; - `assert_total` 20; - `assert_smaller` 2. - **The hash stubs:** `Hash.idr` has 9 `%foreign` lines, all commented out. - **The recon figures** (383 bodyless, 79 unbuilt, 52 warnings, 71 `()` theorems) are labelled as measured at 8542e84 and not re-counted here. - **The 3%** is quoted from `PROOF-NEEDS.adoc` (1 of 32 sampled modules). - **Placeholder check:** the file contains no `{{`, `TODO: update`, `<PROJECT` or `example.com`. It has 103 substantive lines. ## Checklist - [x] My commits are **signed** (`git log --format=%G?` → `G`). - [x] I ran the project's own checks: no Idris source changed, so there was nothing to rebuild. The evidence is CI's at the anchor. - [x] New files carry the correct `SPDX-License-Identifier`: `CC-BY-SA-4.0`, as for the repo's other `.adoc` docs, with the attribution line from `.claude/CLAUDE.md`. - [x] Docs: this *is* the docs change. Correcting the README overclaim is item C4 of the follow-up and is not done here. - [x] No soundness hole: no `.idr` file is touched. ## Notes for reviewers - The anchor is the **parent** of this commit. A squash merge changes the commit SHA but keeps 5360032 as the parent, so the anchor stays valid only if nothing else lands on `main` first. If something does, rebase this branch and re-check the anchor row. **Pre-existing red checks** (red on `main` too; this PR does not touch them): - `governance / Workflow security linter`: deferred to #230 (dead OCaml pin) - `governance / Trusted-base reduction policy`: deferred to #230 (undocumented escape hatches) - `governance / Validate Hypatia Baseline`: deferred to #230 (`--argjson` crash in standards) - `Enforce Trustfile Policies`: deferred to #230 (Palimpsest licence headers) - `Aspect — Safety Invariants`: deferred to #230 - **Emerged, not yet on #230:** `GitHub Pages / build` is blocked by the action allowlist on `actions/upload-artifact@v4`. The `mirror-*` ×3 jobs have an empty host variable. Both are recorded in `dev-notes/inbox/findings.md`. - There are no required checks on `main`, so automerge is deliberately **not** armed. This waits for a human squash merge. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01HZc76cZKg5tUgduxXGLQkD Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
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
1 participant
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 is a follow-up to #228. It fixes the CodeRabbit finding on that PR (#228 (comment)), which was merged before the fix could be pushed to it.
bfMulWithIrrcould hang ifirrdid not have degree exactlyn. A polynomial of the wrong degree never cancels the top bit of the product, sopolyModReductionlooped forever, and the range check added in #228 never ran. For example,irr = 0with0x80 • 0x02hangs. NowbfMulWithIrrreturnsNothingunlessbitLength irr == S n, and it checks this before reducing. When the degree is exactlyn, each reduction step clears the top bit, so the loop terminates.Type of change
bfMulWithIrrhangs on an invalid polynomialMaybeafter fix(soundness): remove false postulates in SafeFiniteField, SafePipe, SafeTerminal #228)📌 New pins
Head SHA: bb82eeb. No action, lockfile or container pins are added or changed; only
src/Proven/SafeFiniteField.idris touched.How has this been verified?
All runs used Idris2 0.8.0 locally, on the identical file content (originally commit 178a01d, cherry-picked here):
idris2 -p contrib --total --check src/Proven/FFI/SafeFiniteField.idr(which buildsSafeFiniteField): rc=0. The only warning is the pre-existingSIsNonZerodeprecation.--execharness withbfMulWithIrr {n=8}:aesIrreducible:0x57•0x83 = 193,0x57•0x13 = 254,0x02•0x80 = 27, all correct.irr = 0→Nothing, andirr = 0x1B(degree 4) →Nothing. Both previously hung.CI red checks: all pre-existing on
main, none caused by this diff, deferred to #230build (0.8.0): deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230.proven.ipkgbuilds 305/305; the job then fails intests.ipkgattests/properties/SafeMathProps.idr(undefinedsafeNegate,detectOverflow, …).Aspect — Safety Invariants: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230. The pre-existingassert_totaluses insrc/; this PR adds none.Enforce Trustfile Policies: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230. 5 pre-existing non-MPL/CC-BY-SA SPDX headers; this PR changes no header.scan / gitleaks: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230. Fails identically onmain@ 8542e84.governance / Workflow security linter: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230. Fails identically onmain@ 8542e84.governance / Trusted-base reduction policy: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230. Fails identically onmain@ 8542e84.governance / Validate Hypatia Baseline: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230. Fails identically onmain@ 8542e84.proof-check (0.8.0)andverify-idris-buildare green.Checklist
proven.ipkgbuild is left to CI, because the local build is memory-bound on this host.SPDX-License-Identifier: no new files.bfMulWithIrrand the newbitLengthdescribe the behaviour.bitLengthiscovering, like the existinghighestBit.Notes for reviewers
fix/remove-false-runtime-assumptions. CodeRabbit's coding agent then pushed an unrelated, unreviewed commit there (4f8d7fa: assert_total rewrites and SPDX edits). It is not in this PR. That branch is safe to delete, unless you want to review the bot's commit.🤖 Generated with Claude Code
https://claude.ai/code/session_01HZc76cZKg5tUgduxXGLQkD