Repository navigation
Recognize Agda infrastructure and resolve local prose references - #651
Conversation
Bounded draft proposal related to hyperpolymath/echo-types#361. Native/policy gaps remain explicit in the PR description.
|
Caution Review failedThe pull request is closed.
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. |
|
Codex Review Summary: ✅ CompletedThis 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. |
This draft preserves source-attested reusable-workflow closure and resolves the nine governance findings without policy waivers. Released gh-actions-lock v0.4.1 does not lock external job-level reusable workflows. A separate gate binds five active caller/job pairs to immutable repository/commit/path/blob identities, authenticates raw Git objects in an isolated bare cache, and compares observed direct edges with reviewed receipt unions. Fetched code is never executed. Missing evidence is nonzero NOT-RUN; contradictory identities and dropped edges are fatal. Two explicitly historical source paths preserve the original standards75bd union and cannot substitute for active callers. All 20 original ordinary lock records, 10 supplemental records, 13 original receipt rows and six newer governance receipt rows are preserved. Supplemental records are admitted only after complete source verification. The published governance caller stays pinned to standards ea2f4d8a886585ed442687ae63d4ad7493379ba4. Draft Fleet #651 and standards #1419 remain separate and unadopted. The source job remains an explicit E2E prerequisite with failure/skipped/cancelled/missing results rejected; no branch ruleset or baseline is changed. The governance follow-up removes the four prohibited Python auditor/test files and replaces them with an isolated Rust CLI plus Bash entrypoints. It preserves map and regeneration exit semantics, strict input validation, transitive closure comparison, source-scope limitations and all original regression controls. The parser is saphyr 0.3.3; the abandoned unsafe-libyaml dependency is absent. CI audits the exact crate lock with cargo-audit 0.22.2, verifies the release archive SHA256, and denies warnings without advisory exclusions. The four credential-bearing workflow jobs now run harden-runner at 46b06cea07f9e64621fdf066ba77ac6915163d43. Dispatch and SMTP jobs use explicit egress block rules; scheduled fleet scans use audit mode pending endpoint observations. Inbox write permissions are scoped to the existing auto-merge job, and its already-produced outputs are declared for downstream consumers. Existing triggers, guards, needs, steps and concurrency are preserved. No mail or dispatch was manually sent to test these rules. Official lock regeneration rewrites bare SHA uses to known tags. The final lock therefore preserves the reviewed records verbatim and imports only the officially generated hardener metadata under its authoritative SHA key, plus four workflow edges. Both official read-only --verify-local and authenticated --verify pass. The tag v2.22.3 resolves to that SHA, although the upstream commit message says v2.23.0; the SHA is authoritative. Local validation at signed head e911e68 (tree 8019b4d): - 55 source controls, 47 preserved closure controls and nine migration-preflight controls pass. - Five source roots verified; integrated audit fatal=0, review=0, not-run=0, accepted=3, source-attested-records=11. - 41 native Rust tests pass. Independent verification replays all 22 original map controls, eight regeneration methods/eight scenarios, 30 additional adversarial cases and two subprocess-failure controls. - Actual pinned Hypatia RE001/WH002 rules report no findings; four-workflow actionlint passes. - All 20 reviewed dependency records and original workflow edges remain unchanged apart from the one added hardener record/four edges. - Dependency audit --deny warnings is clean at RustSec 309392b18f6b17022f82c701f300433126901068. The final signed follow-up is a070e1e (reviewed tree 8eaf158). It passes 42 native Rust tests on Rust/Cargo 1.85.1, addresses Sonar’s control-flow, HTTPS-redirect and read-permission findings, and closes two independently reproduced parser fail-open batches. All 11 bare numeric/malformed-radix forms reject, and all 11 quoted counterparts remain accepted; the immutable regeneration controls pass again. Conservative additional rejections of ambiguous plain strings are documented rather than presented as exact acceptance parity. No dependency lock, source identity or receipt data changed in this follow-up. On this final head, all nine distinct required contexts pass. Hosted source closure records 55/47/9 passed controls with zero failures, and the integrated audit retains fatal=0, review=0, not-run=0, accepted=3 and source-attested-records=11. E2E, SonarCloud, governance baseline/language policy, action-lock verification, K9 and DEED pass. The report-back production job is still running at this snapshot; the Scorecard app alert below remains open. No all-CI-green claim is made. Scorecard’s app check flags contents:write on the existing opt-in auto-merge job. That permission is scoped to the guarded job and required by its existing merge API and merge-result git push; [GitHub’s merge endpoint documentation](https://docs.github.com/en/rest/pulls/pulls#fine-grained-access-tokens-for-merge-a-pull-request) confirms the contents-write requirement. The default-off guard and merge criteria remain unchanged. The alert remains open for owner review; no suppression, broader PAT or feature deletion was substituted. The distinct Actions Scorecard PR job passes on the final head. CodeRabbit skips automatic review while this PR is draft; no fresh CodeRabbit review is claimed. The scanner migration preflight still requires canary evidence and exits 2 without it. The native en_GB.UTF-8 report-back ordering fixture issue was reproduced on unchanged base and prior candidate and remains separate. Static egress review does not establish successful SMTP or dispatch runtime behavior. Scope and reproducible commands are documented in docs/migrations/pinned-source-closure.adoc and tools/workflow-lock-audit/README.adoc. This proves the stated direct-edge/receipt boundary, not arbitrary recursive runtime/container/downloaded-script provenance. No exemptions, credentials, rulesets, mirror activation or ordinal work are included. This PR remains draft; no merge or ready-for-review transition is requested.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4fa1a52378
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| && args.iter().any(|arg| { | ||
| let operand = arg.trim_matches(['\'', '"']); | ||
| !operand.starts_with('-') && operand.ends_with(".agda") |
There was a problem hiding this comment.
When an option's separate value happens to end in .agda, this reports a runner even though no source file was supplied—for example, agda -i vendor.agda, where vendor.agda is a directory, satisfies this predicate and suppresses TEST-AG-002. The Agda CLI documents -i {DIR} as consuming a directory argument, so the recognizer needs to skip values for options such as -i rather than treating every non-dash token as a source operand. See the Agda command-line documentation.
Useful? React with 👍 / 👎.
| let command = line.split('#').next().unwrap_or("").trim(); | ||
| let command = command.strip_prefix("- ").unwrap_or(command); | ||
| let command = command.strip_prefix("run:").unwrap_or(command).trim(); | ||
| is_direct_agda_source_check(command) |
There was a problem hiding this comment.
For a valid single-line workflow scalar such as run: "agda proofs/agda/Main.agda", stripping run: leaves the leading quote in place, so is_direct_agda_source_check sees "agda rather than agda and emits TEST-AG-002 even though the known workflow directly runs the source check. Unwrap the YAML scalar before tokenizing, or parse the workflow value structurally.
Useful? React with 👍 / 👎.
| entry.file_type().is_file() | ||
| && entry | ||
| .path() | ||
| .extension() | ||
| .is_some_and(|extension| extension == "agda") |
There was a problem hiding this comment.
An Agda repository whose proofs use supported literate source files is misclassified here: verification/proofs/Main.lagda.md does not make is_agda true, while the same file under proofs/agda subsequently causes the analyzer to report TEST-AG-001 because the source scan repeats this .agda-only check. Agda officially treats .lagda, .lagda.tex, .lagda.md, and .lagda.rst as source formats, so these layouts should be recognized rather than reported as unknown or empty. See the Agda literate-programming documentation.
Useful? React with 👍 / 👎.
| } else if kind.is_file() && entry.file_name() == name { | ||
| let candidate = local_file(&root, &entry.path())?; |
There was a problem hiding this comment.
When an unqualified prose reference names a tracked symlink to a source elsewhere in the repository, DirEntry::file_type() identifies the entry as a symlink, so this branch ignores it and emits CLM-006 even though the reference resolves to a valid local file. The direct-path branches already canonicalize and accept such links while rejecting targets outside the repository; the basename scan should apply the same local_file validation to symlink entries.
Useful? React with 👍 / 👎.
| "vendor", | ||
| "deps", | ||
| ]; |
There was a problem hiding this comment.
In repositories that retain generated bundles under the conventional dist/ directory, this exclusion list still traverses those artifacts. Consequently, a prose reference such as see app.js is accepted when only dist/app.js exists, or is reported as ambiguous when both the real source and its generated copy exist, contradicting the resolver's stated rule that generated basename fallbacks must not satisfy references. Add dist and equivalent configured output directories to the excluded traversal set.
Useful? React with 👍 / 👎.
Finishingbot treats an Agda proof repository as an unknown Rust/Deno project and resolves free-prose file references only from the repository root. This bounded proposal recognizes substantive Agda source layouts and conservative direct source-check commands, and resolves document-relative/repository-relative paths plus unique unqualified module basenames.
Missing qualified paths, ambiguous basenames, generated basename fallbacks, directories and paths escaping the repository remain unresolved. The command recognizer rejects informational version/help/print modes even with an apparent
.agdaoperand, comments, misleading suffixes and option-value substrings. It recognizes only direct single-line calls in known workflow/recipe locations; dynamic wrappers need separate review. No prover is executed and no proof result is certified. Mixed Rust/Deno/Agda projects retain independent checks.Validation on base
34908580b98cd354caa3bfc5a000bc7935957fce:cargo test --locked --manifest-path bots/finishingbot/Cargo.toml --no-default-featureswith existing Rust/cargo 1.99.1: 13 library unit tests, the same 13 binary executions, and 37 integration tests pass (50 distinct tests; 63 executions).rustfmt --checkon the four changed files andgit diff --checkpass. No dependencies, lockfiles or shared libraries are changed.c3407350844fe4d882fe2c63e9b97f5bbbf441b5using explicit dry-run/auto-fix-false configuration. Both exit 1. Total findings change 267→189: CLM-006 200→123 and TEST-001 1→0; all other rule counts remain unchanged. The target stays clean. Distinct compiler metadata prevents baseline/patched final executable cache collisions.This draft does not implement the shared native chora reader. Six obsolete SCM-file expectations remain in the actual audit. Rhodibot's vendored A2ML criteria/profile readers and Finishingbot/Glambot's metadata readers/auto-fixer require a coordinated follow-up with a pinned native parser/runtime distribution, consistent local/API tree handling and accepted owning clause semantics. No auto-fixer was used; remaining findings have not all been adjudicated.
Related: hyperpolymath/echo-types#361, which remains open. No fake SCM/A2ML files, empty proof directories or fabricated all-fleet success are introduced.