Fix/idris2 totality and elaboration cures - #217
Merged
Merged
Conversation
Part of estate-wide standards#426 remediation - cleanup. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…e87a5923fdf329 Part of estate-wide standards#426 remediation - Batch 11 SHA update. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…e87a5923fdf329 Part of estate-wide standards#426 remediation - Batch 13 SHA update. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Add security-events: write and id-token: write to workflow-level permissions in scorecard.yml for scorecard-reusable.yml calls. Ensure contents: read at workflow-level for secret-scanner.yml. Part of hyperpolymath/standards#426 remediation - Batch 2. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Update reusable workflow SHA from d135b05 to f2f8e6791b09f1f498f01b798e4670a1ebc9c986 to pick up fixes for: - Bug A: Invalid timeout-minutes at workflow_call level and duplicates - Bug B: Permissions escalation in scorecard-reusable Part of hyperpolymath/standards#426 remediation. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Final SHA update for Bug A and Bug B fixes. Part of hyperpolymath/standards#426 remediation. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Before this branch, `idris2 --build proven.ipkg` was cancelled at CI's
45-minute timeout having produced no verdict at all: the build was VOID
(exit 2 semantics), not red and not green. It now answers RED in minutes
with named errors, and the module frontier has moved from 165/305 to
210/305.
Measured on Idris2 0.7.0. Source and CI target 0.8.0, so every frontier
figure here is a 0.7.0 reading, not a 0.8.0 one.
Seven files, each verified standalone with
`idris2 -p contrib --source-dir src --check <file>` returning rc=0:
SafeOTP.idr where-block ordering; recursion on a
non-inductive numeric type, restructured to
recurse structurally on a derived Nat bound
SafeRedirect.idr two where-local wrappers shadowing the Prelude
names they called; renamed the locals
SafeCSP.idr a where block attached to one clause of a
multi-clause function; hoisted to top level
SafeCrypto/Proofs.idr two proof bodies written in Lean 4 tactic
syntax; replaced with real Idris2 proofs
SafeEmail/Proofs.idr top-level forward reference; signature hoisted
SafeUrl/Proofs.idr Ord Nat's <= is not Data.Nat.lte -- the
hypothesis was restated over the relation the
stdlib lemma actually consumes
SafeRegex/Parser.idr see below
SafeRegex/Parser.idr carried five distinct defects and went from 39
reported errors to 0:
1. 25 sites wrote `Char c` where the constructor is `SingleChar`.
`Char` resolves to the builtin TYPE, so the compiler reports
"Mismatch between: Type and Char -> CharClass" and never
"Undefined name". `SingleChar` is used correctly in Types.idr,
Safety.idr, Proofs.idr and SafeArgs/Proofs.idr -- this file is the
only one the rename never reached.
2. An eta/arity bug: `map Match (parseCharClass st)` applied the
parser before passing it to the file's own local `map`.
3. `many` and `parseClassContents` recursed with no decreasing
measure. Both now derive a fuel bound from `length st.input`
internally, so their public signatures are unchanged.
4. The six-member mutual block recursed through a ParserState record
Idris2 cannot measure. A Nat budget is now threaded through the
group; the two public entry points seed it with
`16 * length (unpack pattern) + 16`, a strict over-approximation.
`parseSequence`'s where-block was hoisted to `parseSequenceGo`
because a where attaches to one clause only.
5. A let-bound record update could not infer its type. Idris2
resolves record-update field names from the EXPECTED type
downward; a bare `let` supplies none. Fixed with an annotation.
Discipline observed throughout:
- Zero new trusted-base markers. The four marker tokens were counted
in every touched file before and after each edit and every count is
unchanged; SafeRegex/Parser.idr was and remains 0/0/0/0.
- Five proof obligations genuinely discharged (modernIsSecure,
standardIsSecure, errorMakesInvalid, warningKeepsValid,
lteFrom65535Check), two of them in strictly stronger generalised
form. No obligation was discharged by assertion.
- No public signature changed. The entire SafeRegex mutual block is
private; only parseRegex, parseRegexWithFlags, parseSafe and
parseSafeStrict are public and none of their types moved.
IMPORTANT -- SafeRegex/Parser.idr was NOT in HEAD before this commit.
Commit f2833c2 ("feat: add ECHIDNA validation modules", 2026-01-29)
deleted 22 .idr files while claiming to add modules. Seventeen were
later restored and re-tracked. Five were restored to the working tree
but never re-added to git: SafeRegex/Matcher.idr,
SafeRegex/Parser.idr, SafeSQL/Builder.idr, SafeXML/Parser.idr and
SafeYAML/Parser.idr. This commit restores exactly one of them --
Parser.idr, the one it cures. The other four are left untouched and
filed as an issue.
Consequence, stated as a deduction and not yet measured: Parser.idr is
imported by Proven.FFI.SafeRegex, which IS listed in proven.ipkg, so a
clean checkout of the previous HEAD cannot have built that module. The
local frontier of 210/305 therefore depended on untracked files. This
should be confirmed by building a clean clone.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…files Preservation commit only — flushes the uncommitted postulate/totality cures to the branch before they can be lost to a checkout or sweep. Deliberately excludes the other ~169 working-tree changes: 72 .ts binding files are pure-deletion blanking damage (do NOT commit them; HEAD holds the real content) and the rest are of unaudited provenance. See hyperpolymath/standards#705. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The rescript/deno/typescript blanking sweep excised its search terms as bare
substrings, including from inside longer words. Nine lines across four files
are restored from the merge-base blob.
The severe case is src/Proven/SafeDNS.idr, where `PureScript` contains the
substring `reScript` and was truncated to `Pu`:
data PureScript : String -> Type where -> data Pu : String -> Type where
`PureScript` here is the Unicode sense - a string in a single script, guarding
`isMixedScript s = False` for homoglyph/IDN safety - and has nothing to do with
the language. The declaration, the constructor `MkPureScript` and the use site
in `MkIDNSafe` were all renamed consistently, so the code still compiled and no
gate could see it.
The other three files are doc comments comparing Idris2's type system to
ReScript's. They are restored verbatim rather than migrated to AffineScript:
they are statements about what ReScript cannot express, so rewriting the
language name would make them false.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
- Add Optimus-Branch.json for branch protection - Add Immutable-Tags.json for tag protection - Remove deprecated branches: from settings.yml - Keep labels and repository metadata Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Contributor
|
Caution Review failedThe pull request is closed. ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: 📒 Files selected for processing (86)
📝 SummarySummary by CodeRabbit
WalkthroughThis pull request adds GitHub tag and branch rulesets, updates Idris compatibility and totality, adds regex, SQL, XML, and YAML functionality, and changes many proof declarations from postulates to erased declarations or concrete definitions. ChangesRepository controls
Idris implementation and proofs
Estimated code review effort: 5 (Critical) | ~120 minutes Change: Feature Sequence Diagram(s)sequenceDiagram
participant Caller
participant RegexParser
participant SafeRegex
participant RegexMatcher
Caller->>RegexParser: parseSafe pattern
RegexParser->>SafeRegex: analyse parsed Regex
SafeRegex-->>Caller: SafeRegex or RegexError
Caller->>RegexMatcher: safeMatch input
RegexMatcher-->>Caller: MatchResult or safety error
✨ Finishing Touches 💡 1🛠️ Fix failing CI checks 💡
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. A rabbit reads each line, Comment |
hyperpolymath
enabled auto-merge (squash)
September 14, 2026 17:37
…nd-elaboration-cures # Conflicts: # .github/workflows/governance.yml # .github/workflows/hypatia-scan.yml # .github/workflows/mirror.yml # .github/workflows/scorecard.yml # .github/workflows/secret-scanner.yml # .github/workflows/spark-theatre-gate.yml # GOVERNANCE.adoc
…rseable YAML) The bulk permissions pass appended a mapping key under the read-all scalar shorthand in clusterfuzzlite.yml and e2e.yml. read-all already grants actions:read; the stray key made both files unparseable.
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @@ -0,0 +1,558 @@ | |||
| -- SPDX-License-Identifier: Palimpsest-MPL-1.0 | |||
| @@ -0,0 +1,481 @@ | |||
| -- SPDX-License-Identifier: Palimpsest-MPL-1.0 | |||
| @@ -0,0 +1,567 @@ | |||
| -- SPDX-License-Identifier: Palimpsest-MPL-1.0 | |||
|
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
3 participants
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
Closes #
Type of change
How has this been verified?
Checklist
git commit -S).SPDX-License-Identifier(code/configMPL-2.0,prose
CC-BY-SA-4.0); I did not relicense existing files.Notes for reviewers