Repository navigation
Complete Logtalk to Elixir rule migration - #996
Conversation
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
Caution Review failedThe pull request is closed. Summary
Merge Risk:
 |
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
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. |
![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: 4018290eaa
ℹ️ 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".
| files = Map.get(evidence, :files, []) | ||
| contents = Map.get(evidence, :contents, %{}) | ||
| repo_tags = Map.get(evidence, :repo_tags, []) |
There was a problem hiding this comment.
When callers intentionally supply only a subset of evidence, these defaults turn absent evidence into negative evidence. For example, check_all(%{repo_tags: ["cryptography"], required_reviews: 2}) passes an empty file list to AP010 and incorrectly reports that fuzz targets are missing; similarly, supplying :files without :contents can make AP003 report that no workflow runs cargo audit. This contradicts the documented contract that missing evidence yields no finding and can produce high-severity false positives, so each check should run only when all of its required keys are present.
Useful? React with 👍 / 👎.
| '#'*) return 0 ;; | ||
| ';'*) return 0 ;; | ||
| '//'*) return 0 ;; | ||
| '--'*) return 0 ;; |
There was a problem hiding this comment.
In shell scripts and YAML run blocks, a continued command-line option commonly begins with --, but this branch treats every such line as a comment regardless of file type. Consequently, an active command such as reporter \\ followed by --format logtalk is matched and then discarded; check-no-active-logtalk.sh --all still exits successfully, allowing exactly the retired output setting this CI guard is intended to reject. Comment syntax should be selected by file type rather than globally treating -- as a comment prefix.
Useful? React with 👍 / 👎.
| # Guarded forms. | ||
| # --------------------------------------------------------------------------- | ||
| active_re='\[source,logtalk\]|:-[[:space:]]*(object|end_object|protocol|category)[[:space:]]*\(|logtalk_load[[:space:]]*\(|logtalk_(tester|doclet)|report-format[[:space:]]*=[[:space:]]*["'"'"']?logtalk|:report-format[[:space:]]+"logtalk"|(report[-_]?format|format)[[:space:]]*:[[:space:]]*["'"'"']?logtalk|--format([[:space:]]+|=)logtalk|^[[:space:]]*(loader|output_path|output|path|file|rules?)[[:space:]]*[:=].*\.lgt' | ||
| codegen_re='\.lgt(["'"'"'[:space:],)\]]|$)|security_rule[[:space:]]*\(' |
There was a problem hiding this comment.
The .lgt alternative only matches references at end of line because the intended delimiter character class is malformed and does not match even a following quote or space. As a result, an executable line such as logtalk engine/loader.lgt --quiet passes check-no-active-logtalk.sh --all, as do the quoted .lgt references already present in poc-scanner.sh, despite the guard's stated coverage of non-comment references in executable files. Correct the character class so references followed by whitespace, quotes, commas, or brackets are rejected.
Useful? React with 👍 / 👎.
| String.starts_with?(path, ".github/workflows/"), | ||
| do: content | ||
|
|
||
| audited? = Enum.any?(workflow_contents, fn content -> String.contains?(content, "cargo audit") end) |
There was a problem hiding this comment.
Any textual mention of cargo audit anywhere in a workflow is treated as proof that the audit runs. A Rust workflow containing only # TODO: add cargo audit, an explanatory step name, or an echo therefore suppresses AP003 even though CI never performs a vulnerability audit. Since this rule is specifically meant to require execution in CI, inspect active run commands rather than using an unrestricted substring search over the whole YAML document.
Useful? React with 👍 / 👎.
| ||| The repo/file/category/severity projection of a finding: the fields a | ||
| ||| canonical JSON finding (schema/findings.ncl) carries for every result. |
There was a problem hiding this comment.
The retargeted proof says schema/findings.ncl carries repo, file, category, and severity on every finding, but that schema's escript finding has no repo or category fields and its bash finding likewise has no repo or category. Moreover, toFact populates the purported category from Pattern.description. The unchanged equality proof therefore establishes preservation for an invented record rather than the canonical JSON contract it now claims to model, making the new verification statement misleading; the model should use the schema's real fields and mappings.
Useful? React with 👍 / 👎.
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
|
Final receipt note (the PR body above predates the last two commits):
|
Follow-up to #996 (merged at `4428672` before these post-merge check findings were addressed). - Refactor `scripts/check-no-active-logtalk.sh` to use Bash `[[ ... ]]` conditional expressions, assign positional parameters to locals, and give each `case` an explicit default branch (SonarCloud annotations on #996). - Force HTTPS (including redirects) for the pinned official Agda release download in `verify-proofs.yml`. - No semantic change to the guard: `bash -n`, `scripts/check-no-active-logtalk.sh --all` (1,100 files, 14 allowlisted, 0 violations), and `git diff --check` pass locally. This also supplies the standards exemption-ratchet declaration for the two SD022 entries added in #996: Ratchet-exception: .hypatia-ignore — two exact SD022 entries remove a foreign-tree false positive in sibling migration packets that quote epistemic-types' own src paths; delete each entry when its packet is removed after sibling landing. Known unrelated failure: Governance "Allowlist Preflight" rejects the pre-existing ClusterFuzzLite action refs because they are not covered by the standards allowlist at the pinned standards revision; that needs the standards allowlist/pin process and is not changed here.
Summary
Completes the Logtalk -> Elixir semantic migration for Hypatia's canonical rule system (
lib/rules/*.ex):security_learning.lgtalert semantics intoHypatia.Rules.SecurityErrors(alert_category/1, explicit catch-all severities,validate_alert/1, CWE-915, Logtalk banned -> Elixir).Hypatia.Rules.AuditPreventionor points each at its existing canonical checker.schemas/learned-security-rules.schema.json).integration/robot-repo-automaton,INTENT.contractile, hooks language policy, guides, generated catalogue).scripts/check-no-active-logtalk.sh+ exact-path shrink-only.logtalk-allowlist, wired into CI and proven by mutant locally (planted.lgt+report_format: logtalk-> red; removed -> green).epistemic-types_chora.deedwith:report-format "json"), and standards.Proof status (stated exactly)
verification/proofs/agda/LogtalkMigration.agda.AGDA-PENDINGinverification/PROOF-STATUS.adocuntil this PR's strict-profile Agda receipt exists. Theverify-proofsworkflow now installs the official pinned Agda 2.8.0.2 release and runsagda --safe --without-K --cubical-compatible LogtalkMigration.agdaas a hard failure (never a skip).VerisimdbConnector.idr: statement superseded from the retired Logtalk fact format toFindingFact(canonical JSON finding projection); proof term unchanged, no runtime-refinement claim.Local validation
Authoring sandbox has no BEAM/prover binaries and its egress blocks their installers, so local evidence is static only (guard, proof-status/trusted-base scripts, JSON/shell checks, Elixir syntax parse). This PR's CI runs are the compile/ExUnit/Idris/Agda receipts;
PROOF-STATUS.adocwill be updated from them before this leaves draft.Ledger:
docs/rules/logtalk-migration.adoc.