diff --git a/.audittraining/security-errors/bunsenite.adoc b/.audittraining/security-errors/bunsenite.adoc index be17fa64..8af379e1 100644 --- a/.audittraining/security-errors/bunsenite.adoc +++ b/.audittraining/security-errors/bunsenite.adoc @@ -154,7 +154,9 @@ fuzz_target!(|data: &[u8]| { ''''' -=== Prevention Rules (Logtalk) +=== Prevention Rules (historical Logtalk — superseded) + +NOTE: Historical source of record only (2025-12-29), retained so the transcription can be audited. These are rules AP001–AP002; the canonical Elixir form is `Hypatia.Rules.AuditPrevention` plus the live checkers named in `docs/rules/logtalk-migration.adoc`. Do not treat the block below as an active rule source. [source,logtalk] ---- diff --git a/.audittraining/security-errors/czech-file-knife.adoc b/.audittraining/security-errors/czech-file-knife.adoc index 86c183ae..5c45405b 100644 --- a/.audittraining/security-errors/czech-file-knife.adoc +++ b/.audittraining/security-errors/czech-file-knife.adoc @@ -155,7 +155,9 @@ RUN cargo +nightly fuzz build ''''' -=== Prevention Rules (Logtalk) +=== Prevention Rules (historical Logtalk — superseded) + +NOTE: Historical source of record only (2025-12-29), retained so the transcription can be audited. These are rules AP003–AP004; the canonical Elixir form is `Hypatia.Rules.AuditPrevention` plus the live checkers named in `docs/rules/logtalk-migration.adoc`. Do not treat the block below as an active rule source. [source,logtalk] ---- diff --git a/.audittraining/security-errors/gitvisor.adoc b/.audittraining/security-errors/gitvisor.adoc index 26ec70fd..db4daeb2 100644 --- a/.audittraining/security-errors/gitvisor.adoc +++ b/.audittraining/security-errors/gitvisor.adoc @@ -178,7 +178,9 @@ For polyglot repos like gitvisor: ''''' -=== Prevention Rules (Logtalk) +=== Prevention Rules (historical Logtalk — superseded) + +NOTE: Historical source of record only (2025-12-29), retained so the transcription can be audited. These are rules AP005–AP006; the canonical Elixir form is `Hypatia.Rules.AuditPrevention` plus the live checkers named in `docs/rules/logtalk-migration.adoc`. Do not treat the block below as an active rule source. [source,logtalk] ---- diff --git a/.audittraining/security-errors/polyglot-i18n.adoc b/.audittraining/security-errors/polyglot-i18n.adoc index 6172745c..e4ad6516 100644 --- a/.audittraining/security-errors/polyglot-i18n.adoc +++ b/.audittraining/security-errors/polyglot-i18n.adoc @@ -151,7 +151,9 @@ bestpractices.coreinfrastructure.org ''''' -=== Prevention Rules (Logtalk) +=== Prevention Rules (historical Logtalk — superseded) + +NOTE: Historical source of record only (2025-12-29), retained so the transcription can be audited. These are rules AP007–AP008; the canonical Elixir form is `Hypatia.Rules.AuditPrevention` plus the live checkers named in `docs/rules/logtalk-migration.adoc`. Do not treat the block below as an active rule source. [source,logtalk] ---- diff --git a/.audittraining/security-errors/proof-of-work.adoc b/.audittraining/security-errors/proof-of-work.adoc index 4445dbfc..17105922 100644 --- a/.audittraining/security-errors/proof-of-work.adoc +++ b/.audittraining/security-errors/proof-of-work.adoc @@ -194,7 +194,9 @@ let key = keys.get(index).ok_or(CryptoError::InvalidIndex)?; ''''' -=== Prevention Rules (Logtalk) +=== Prevention Rules (historical Logtalk — superseded) + +NOTE: Historical source of record only (2025-12-29), retained so the transcription can be audited. These are rules AP009–AP011; the canonical Elixir form is `Hypatia.Rules.AuditPrevention` plus the live checkers named in `docs/rules/logtalk-migration.adoc`. Do not treat the block below as an active rule source. [source,logtalk] ---- diff --git a/.audittraining/security-errors/supernorma.adoc b/.audittraining/security-errors/supernorma.adoc index 51bd0921..49a7fbaa 100644 --- a/.audittraining/security-errors/supernorma.adoc +++ b/.audittraining/security-errors/supernorma.adoc @@ -104,7 +104,9 @@ runs: ''''' -=== Prevention Rules (Logtalk) +=== Prevention Rules (historical Logtalk — superseded) + +NOTE: Historical source of record only (2025-12-29), retained so the transcription can be audited. These are rules AP012–AP013; the canonical Elixir form is `Hypatia.Rules.AuditPrevention` plus the live checkers named in `docs/rules/logtalk-migration.adoc`. Do not treat the block below as an active rule source. [source,logtalk] ---- diff --git a/.audittraining/security-errors/ubicity.adoc b/.audittraining/security-errors/ubicity.adoc index 8700912b..d3a48dea 100644 --- a/.audittraining/security-errors/ubicity.adoc +++ b/.audittraining/security-errors/ubicity.adoc @@ -131,7 +131,9 @@ end ''''' -=== Prevention Rules (Logtalk) +=== Prevention Rules (historical Logtalk — superseded) + +NOTE: Historical source of record only (2025-12-29), retained so the transcription can be audited. These are rules AP014–AP015; the canonical Elixir form is `Hypatia.Rules.AuditPrevention` plus the live checkers named in `docs/rules/logtalk-migration.adoc`. Do not treat the block below as an active rule source. [source,logtalk] ---- diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 44f46d93..3184c6c1 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -354,9 +354,20 @@ jobs: test/rules/actions_lock_test.exs \ test/rules/actions_lock_closure_corpus_test.exs \ test/rules/rsr_conformance_test.exs \ + test/rules/audit_prevention_test.exs \ + test/security_errors_test.exs \ test/research_extensions_test.exs \ test/deed_test.exs + # ADR-001 retirement guard: Hypatia rules are pure Elixir + # (lib/rules/*.ex). This fails if an active .lgt/.logtalk source + # or a Logtalk output/loader setting re-enters the tree outside + # the exact-path, shrink-only .logtalk-allowlist. Proven by + # mutant (plant a .lgt + a report_format: logtalk setting -> red; + # revert -> green). See docs/rules/logtalk-migration.adoc. + - name: No active Logtalk (ADR-001 guard) + run: bash scripts/check-no-active-logtalk.sh + # The consumers' invocation, verbatim: the oracle is called with an # EXPLICIT --ssot. The default SSOT resolution is deliberately not # exercised here — it depends on the layout of the checkout that hosts diff --git a/.github/workflows/verify-proofs.yml b/.github/workflows/verify-proofs.yml index dfffb4ea..98fec031 100644 --- a/.github/workflows/verify-proofs.yml +++ b/.github/workflows/verify-proofs.yml @@ -3,7 +3,7 @@ # This workflow is managed by gh actions-lock. # Consolidated workflow (behaviour-preserving merge). # Merged from: verify-idris.yml, verify-lean.yml, verify-tlaplus.yml -name: Verify Proofs (Idris / Lean / TLA+) +name: Verify Proofs (Idris / Lean / TLA+ / Agda) on: push: @@ -14,6 +14,7 @@ on: - verification/proofs/idris2/** - verification/proofs/lean4/** - verification/proofs/tlaplus/** + - verification/proofs/agda/** - verification/PROOF-STATUS.adoc - scripts/check-proof-status.sh - scripts/check-trusted-base.sh @@ -38,6 +39,7 @@ on: - verification/proofs/idris2/** - verification/proofs/lean4/** - verification/proofs/tlaplus/** + - verification/proofs/agda/** - verification/PROOF-STATUS.adoc - scripts/check-proof-status.sh - scripts/check-trusted-base.sh @@ -285,6 +287,68 @@ jobs: done } >> "$GITHUB_STEP_SUMMARY" + # Estate PROOF-POLICY / Mathesis Grade 3 gate for the one Agda artefact: + # a missing or failing checker is a hard failure, never a skip. The file + # imports only Agda builtins, so no standard-library dependency is + # involved. A green run is the receipt material for the PROOF-STATUS + # Grade 3 / AGDA-VERIFIED row; it does not by itself claim Grade 2/1 + # reconciliation or runtime refinement. + agda-check: + name: agda strict-profile check + runs-on: ubuntu-latest + timeout-minutes: 20 + permissions: + contents: read + + env: + # Latest stable Agda release at implementation time, pinned so the + # Grade 3 receipt names an exact checker (estate PROOF-POLICY). + # Deliberately not the runner's APT package, whose version floats. + AGDA_VERSION: 2.8.0.2 + + steps: + - name: Checkout + uses: actions/checkout@v7.0.1 + + - name: Install Agda (official pinned release) + run: | + set -euo pipefail + asset="Agda-v${AGDA_VERSION}-linux.tar.xz" + curl -fL --retry 3 -o "/tmp/${asset}" \ + "https://github.com/agda/agda/releases/download/v${AGDA_VERSION}/${asset}" + install_root="$HOME/.local/opt/agda-${AGDA_VERSION}" + rm -rf "$install_root" + mkdir -p "$install_root" + tar -xJf "/tmp/${asset}" -C "$install_root" + # The official tarball is a flat archive containing ./agda + # (see agda/agda .github/workflows/deploy.yml), not bin/agda. + agda_bin="$(find "$install_root" -type f -name agda | head -1)" + [ -n "$agda_bin" ] + chmod +x "$agda_bin" + echo "$(dirname "$agda_bin")" >> "$GITHUB_PATH" + "$agda_bin" --version + + - name: Check LogtalkMigration.agda (strict profile) + working-directory: verification/proofs/agda + run: | + set -euo pipefail + agda --version + sha256sum LogtalkMigration.agda + agda --safe --without-K --cubical-compatible LogtalkMigration.agda + + - name: Summary + if: always() + run: | + { + echo "## Agda proof verification" + echo "" + echo "- Invocation: \`agda --safe --without-K --cubical-compatible LogtalkMigration.agda\`" + if command -v agda >/dev/null 2>&1; then + echo "- Checker: \`$(agda --version | head -1)\`" + fi + echo "- Source SHA-256: \`$(sha256sum verification/proofs/agda/LogtalkMigration.agda | cut -d' ' -f1)\`" + } >> "$GITHUB_STEP_SUMMARY" + tlc: name: TLC model-check runs-on: ubuntu-latest diff --git a/.hypatia-ignore b/.hypatia-ignore index 8d4aaae6..8b03daa1 100644 --- a/.hypatia-ignore +++ b/.hypatia-ignore @@ -124,3 +124,14 @@ cicd_rules/banned_language_file:resolve.py # "docker" string and flagging the policy itself; this is recursive # self-flagging. # code_safety/ncl_docker_not_podman:.machine_readable/self-validating/hypatia-metadata.k9.ncl + +# ─── 2026-11-01 Logtalk migration coordination packets ───────────────── +# +# These two packets quote epistemic-types' OWN `src/EpistemicTypes/` +# paths and Agda checker command verbatim, because the sibling issue is +# precisely about that repository's descriptor. SD022 (stale `src//` +# after a rename in THIS tree) cannot distinguish a quoted foreign tree +# from local rename drift. Exact files only; remove each entry when its +# packet is deleted after the sibling change lands. +structural_drift/SD022:docs/rules/migration/epistemic-types-neurosym-deed-issue.md +structural_drift/SD022:docs/rules/migration/standards-deed-mapping-issue.md diff --git a/.logtalk-allowlist b/.logtalk-allowlist new file mode 100644 index 00000000..419e9755 --- /dev/null +++ b/.logtalk-allowlist @@ -0,0 +1,38 @@ +# SPDX-License-Identifier: MPL-2.0 +# Exact-path exemptions for scripts/check-no-active-logtalk.sh. +# +# Rules for this file (following the .hypatia-ignore precedent): +# * exact repository-relative file paths only — no wildcards, no +# directory blankets, no globs of any kind; +# * every entry names a classification and a removal condition; +# * shrink-only: adding an entry is a policy change requiring the +# same review as adding a rule; removing one is always welcome; +# * the guard fails if an entry points at a missing file or a file +# that no longer contains any guarded form (stale exemption). +# +# Format: | | +# +# Historical audit-training originals (2025-12-29). The blocks are the +# source of record against which AuditPrevention was transcribed; they +# are headed "historical … superseded" in place. Remove an entry only +# together with deleting/rewriting that file's Logtalk block. +.audittraining/security-errors/bunsenite.adoc | historical source of record (AP001-AP002) | remove with the block +.audittraining/security-errors/czech-file-knife.adoc | historical source of record (AP003-AP004) | remove with the block +.audittraining/security-errors/gitvisor.adoc | historical source of record (AP005-AP006) | remove with the block +.audittraining/security-errors/polyglot-i18n.adoc | historical source of record (AP007-AP008) | remove with the block +.audittraining/security-errors/proof-of-work.adoc | historical source of record (AP009-AP011) | remove with the block +.audittraining/security-errors/supernorma.adoc | historical source of record (AP012-AP013) | remove with the block +.audittraining/security-errors/ubicity.adoc | historical source of record (AP014-AP015) | remove with the block +# The migration ledger and sibling-coordination packets must quote the +# retired forms to specify their replacements. +docs/rules/logtalk-migration.adoc | migration ledger of record | permanent while it is the ledger; remove only if superseded and rewritten without quoted forms +docs/rules/migration/echidna-security-learning-issue.md | sibling coordination packet | remove when the ECHIDNA change lands and the packet is deleted +docs/rules/migration/epistemic-types-neurosym-deed-issue.md | sibling coordination packet | remove when the epistemic-types change lands and the packet is deleted +docs/rules/migration/standards-deed-mapping-issue.md | sibling coordination packet | remove when the standards change lands and the packet is deleted +# Vendored standards conformance fixtures: byte-faithful copies whose +# retired report-format value is upstream-owned drift (see the +# standards packet above). Never edit these to diverge from standards. +test/fixtures/deed_egress/rsr-template-repo_chora.deed | vendored upstream fixture | remove when the standards fixture re-sync no longer carries the retired value +test/fixtures/deed_egress/template-main/rsr-template-repo_chora.deed | vendored upstream fixture | remove when the standards fixture re-sync no longer carries the retired value +# The guard itself contains the pattern definitions it enforces. +scripts/check-no-active-logtalk.sh | enforcement definition | remove only with the guard itself diff --git a/.machine_readable/INTENT.contractile b/.machine_readable/INTENT.contractile index 352e5213..5274ec3c 100644 --- a/.machine_readable/INTENT.contractile +++ b/.machine_readable/INTENT.contractile @@ -12,9 +12,9 @@ ecosystem. It coordinates the gitbot-fleet (rhodibot, echidnabot, sustainabot, glambot, seambot, finishbot) via a safety triangle pipeline (Eliminate > Substitute > Control). It uses 5 neural networks for intelligent dispatch, VQL queries over - verisimdb-data, Bayesian confidence updating, and Logtalk rules for pattern - detection. It is the brain that decides which automated actions to take across - all repositories." + verisimdb-data, Bayesian confidence updating, and pure-Elixir rules in + lib/rules/*.ex for pattern detection. It is the brain that decides which + automated actions to take across all repositories." ) ; === Anti-Purpose (what this repo is NOT — prevents scope creep) === @@ -34,7 +34,7 @@ "5 neural networks (Graph of Trust, MoE, LSM, ESN, RNN) in coordinator GenServer" "VQL as the query interface to verisimdb-data — no raw SQL or direct file reads" "JSONL dispatch manifests for fleet execution layer" - "Logtalk rule engine for error catalog and pattern detection" + "Pure-Elixir rule engine in lib/rules/*.ex for error catalog and pattern detection — no Logtalk/SWI-Prolog (ADR-001)" "Idris2 ABI for Types, GraphQL, gRPC, REST with dependent type proofs" "Zig FFI with 7 exported functions for C ABI bridge" ) @@ -46,7 +46,7 @@ "ffi/zig/ — C ABI boundary; changes affect all language consumers" "config/ — dispatch thresholds and neural network parameters" ".machine_readable/ — checkpoint files, format is specified" - "data/ — Logtalk rules and pattern registry; 954 canonical patterns" + "data/ — verisim pattern registry, learned-rule data and dispatch outcomes; 954 canonical patterns" ) ; === Ecosystem Position === diff --git a/cli/man/hyper.1 b/cli/man/hyper.1 index 33ff51a5..fbf60d0b 100644 --- a/cli/man/hyper.1 +++ b/cli/man/hyper.1 @@ -20,7 +20,7 @@ platform. It provides tools for scanning repositories, managing bot fleets, and interacting with the ruleset registry. .PP The platform combines neural learning for pattern recognition with symbolic -reasoning (Logtalk/Prolog) for fast, deterministic rule execution. +reasoning (Elixir rule modules) for fast, deterministic rule execution. .SH GLOBAL OPTIONS .TP .BR \-o ", " \-\-output =\fIFORMAT\fR diff --git a/docs/DEBT-REGISTER.adoc b/docs/DEBT-REGISTER.adoc index 1ac8376c..683da669 100644 --- a/docs/DEBT-REGISTER.adoc +++ b/docs/DEBT-REGISTER.adoc @@ -428,6 +428,21 @@ a Haskell registry that *does not exist*, Julia neural networks (*zero README says ArangoDB was ditched. trufflehog is still _executing_ in `+security-policy.yml+` despite #675 retiring it. +*Logtalk subset — closed 2026-11-01.* The remaining Logtalk *semantics* +(ECHIDNA `security_learning.lgt`; Hypatia's embedded audit-training +rules AP001–AP015) are transcribed to Elixir with a clause-by-clause +ledger (`docs/rules/logtalk-migration.adoc`); the Logtalk generator is +replaced by schema'd JSON; active-tense Logtalk documentation +(developer guide, EXPLAINME, FAQ/glossary, diagrams, quickstarts, man +page, security/testing/API docs, integration config, INTENT) is +corrected to the canonical `lib/rules/*.ex` locations or explicitly +classified historical; and `scripts/check-no-active-logtalk.sh` guards +against new active `.lgt` files/settings. The two vendored DEED +fixtures still carrying the retired Logtalk report-format value are upstream-owned +(standards) and tracked in the migration packet, so they remain until +standards re-sync. D-2 stays open for its non-Logtalk parts (Haskell +registry prose, Julia claims, ArangoDB/Dragonfly, trufflehog). + ==== D-3 · HIGH · No rule catalogue exists · UNTRACKED 33 rule modules emit families diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc index 45cdcaec..b384906c 100644 --- a/docs/EXPLAINME.adoc +++ b/docs/EXPLAINME.adoc @@ -17,7 +17,7 @@ ____ *Evidence:* The learning pipeline (CLAUDE.md line 77-101) demonstrates this cycle: 1. **Learning** — 5 neural networks (Graph of Trust, Mixture of Experts, Liquid State Machine, Echo State Network, Radial Neural Network) analyze verisim-data 2. **Distillation** — PatternRegistry deduplicates findings into 46 canonical recipes (PA001-PA046 + 20 OpenSSF Scorecard recipes) -3. **Symbolic** — Recipes execute as fast Logtalk rules (no ML at runtime) +3. **Symbolic** — Recipes and checks execute as pure-Elixir rules in `lib/rules/*.ex` (no ML needed for the deterministic checks) 4. **Verification** — Idris2 ABI proofs formally verify recipe correctness This is proven by the metrics: 1635 dispatched actions (600 auto-execute with 95%+ confidence, 667 review, 368 report), 16,671 outcomes recorded (99% success rate), 46 recipes zero-uncovered (every category has a recipe). @@ -34,7 +34,7 @@ ____ *Evidence:* The architecture (lines 49-100) shows all 6 layers implemented: - Verification (Haskell Liquid types, property testing, formal proofs) - Learning (neural subsystem with 5 networks) -- Symbolic (Logtalk rules + Prolog inference) +- Symbolic (Elixir rule modules in `lib/rules/*.ex`) - Data (ArangoDB graph, Dragonfly cache, Radicle P2P) - Action (robot-repo-automaton, hooks, diagnostics) - Forge adapters (6: GitHub, GitLab, Bitbucket, Codeberg, sr.ht, Gitea) @@ -57,7 +57,7 @@ This is operationalized in TriangleRouter, FleetDispatcher (confidence-gated), a | **Elixir 1.16+** | https://elixir-lang.org (8 core modules, OTP GenServers, concurrency) | **Rust** | https://www.rust-lang.org (adapters, CLI, data layer, fixer) | **Julia 1.10+** | https://julialang.org (5 neural networks, training pipeline) -| **Logtalk / Prolog** | Declarative rules (error catalog, pattern detection) +| **Elixir / OTP** | Rule modules (error catalog, pattern detection) | **Haskell** | Formal verification (Liquid types, property testing) | **Idris2 ABI** | https://www.idris-lang.org (type-safe GraphQL, gRPC, REST with proofs) | **Zig FFI** | https://ziglang.org (C ABI bridge for 7 exported functions) diff --git a/docs/api/cli-reference.adoc b/docs/api/cli-reference.adoc index 1f7ae48b..2c639f4f 100644 --- a/docs/api/cli-reference.adoc +++ b/docs/api/cli-reference.adoc @@ -914,6 +914,6 @@ color = true == See Also - xref:rust-api.adoc[Rust API Documentation] -- xref:logtalk-api.adoc[Logtalk Predicates] +- xref:../rules/catalogue.adoc[Rule Catalogue (Elixir rules)] - xref:haskell-api.adoc[Haskell Modules] - xref:http-api.adoc[HTTP API Reference] diff --git a/docs/api/rust-api.adoc b/docs/api/rust-api.adoc index d84c8b37..422bad50 100644 --- a/docs/api/rust-api.adoc +++ b/docs/api/rust-api.adoc @@ -566,5 +566,5 @@ Key dependencies used across the workspace: == See Also - xref:cli-reference.adoc[CLI Reference] -- xref:logtalk-api.adoc[Logtalk Predicates] +- xref:../rules/catalogue.adoc[Rule Catalogue (Elixir rules)] - xref:haskell-api.adoc[Haskell Modules] diff --git a/docs/architecture/system-integration.adoc b/docs/architecture/system-integration.adoc index ac5cba11..3f767e92 100644 --- a/docs/architecture/system-integration.adoc +++ b/docs/architecture/system-integration.adoc @@ -205,8 +205,9 @@ the Elixir equivalent lives in `+lib/rules/code_safety.ex+`. ____ *Note:* this document still contains residual `+.lgt+` filenames and "`learned-rules.lgt`"-style references from the earlier Logtalk-era -architecture. A full rewrite is tracked separately; the rules engine is -now 100% Elixir (`+lib/rules/*.ex+`). +architecture; they are provenance only. The rules engine is 100% Elixir +(`+lib/rules/*.ex+`); see `+docs/rules/logtalk-migration.adoc+` for the +semantic transcription and JSON replacement contracts. ____ === Current Rules Coverage diff --git a/docs/diagrams/architecture.adoc b/docs/diagrams/architecture.adoc index e6dc8a18..f2e2ea40 100644 --- a/docs/diagrams/architecture.adoc +++ b/docs/diagrams/architecture.adoc @@ -17,9 +17,9 @@ graph TB end subgraph "Core Engine" - Rules[Rule Engine
Logtalk] - Learning[Learning Module
Logtalk] - Distiller[Rule Distiller
Logtalk] + Rules[Rule Engine
Elixir — lib/rules] + Learning[Learning Module
Elixir] + Distiller[Rule Distiller
Elixir] end subgraph "Registry" @@ -106,9 +106,9 @@ graph TB [cols=",,",options="header",] |=== |Component |Language |Purpose -|Rule Engine |Logtalk |Declarative rule evaluation -|Learning Module |Logtalk |Pattern learning and confidence scoring -|Rule Distiller |Logtalk |Extract rules from training data +|Rule Engine |Elixir |Pattern-matching rule evaluation (`+lib/rules/*.ex+`) +|Learning Module |Elixir |Pattern learning and confidence scoring +|Rule Distiller |Elixir |Propose/promote rules from training data |=== ==== Registry @@ -153,13 +153,13 @@ graph LR subgraph "Languages" Rust[Rust] Haskell[Haskell] - Logtalk[Logtalk] + Elixir[Elixir] end subgraph "Frameworks" Clap[clap] Servant[Servant] - SWI[SWI-Prolog] + BEAM[BEAM/OTP] end subgraph "Databases" @@ -175,10 +175,10 @@ graph LR Rust --> Clap Haskell --> Servant - Logtalk --> SWI + Elixir --> BEAM Rust --> Dragon - Logtalk --> Arango + Elixir --> Arango Haskell --> Arango Rust --> GH @@ -203,8 +203,8 @@ graph TB end subgraph "Engine Tier" - Engine1[Logtalk Engine 1] - Engine2[Logtalk Engine 2] + Engine1[Elixir/BEAM Engine 1] + Engine2[Elixir/BEAM Engine 2] end end diff --git a/docs/guides/admin-guide.adoc b/docs/guides/admin-guide.adoc index c07c6d72..4235895c 100644 --- a/docs/guides/admin-guide.adoc +++ b/docs/guides/admin-guide.adoc @@ -320,8 +320,8 @@ source ~/.cargo/env # Install GHC (Haskell) curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh -# Install Elixir (rule engine; the Logtalk/SWI-Prolog engine is retired) -apt-get install -y swi-prolog +# Install Erlang/Elixir (the rule engine). Use the versions pinned in +# mise.toml / CI. SWI-Prolog/Logtalk are NOT dependencies. # See https://elixir-lang.org/install.html ---- diff --git a/docs/guides/cicd-guidebook.adoc b/docs/guides/cicd-guidebook.adoc index bfc42b62..fdaf3cd2 100644 --- a/docs/guides/cicd-guidebook.adoc +++ b/docs/guides/cicd-guidebook.adoc @@ -194,11 +194,11 @@ hypatia/ │ ├── catalog.rs # Error catalog (Rust port) │ └── sha_pins.rs # SHA pins reference (Rust port) │ -├── engine/ # (retired) Logtalk engine — logic now in lib/rules/*.ex -│ └── rules/ -│ ├── cicd_rules.lgt # Core rules (absorbed into lib/rules/cicd_rules.ex) -│ ├── forge_adapters.lgt # Multi-forge (absorbed into lib/rules/forge_adapters.ex) -│ └── rule_distiller.lgt # Rule extraction (absorbed into lib/rules/) +├── lib/ +│ └── rules/ # Canonical Elixir rule engine +│ ├── cicd_rules.ex # Core CI/CD rules +│ ├── forge_adapters.ex # Multi-forge operations +│ └── *.ex # See docs/rules/catalogue.adoc │ ├── adapters/ # Rust forge adapters │ └── src/ diff --git a/docs/guides/developer-guide.adoc b/docs/guides/developer-guide.adoc index bae3ca12..ee3a58fb 100644 --- a/docs/guides/developer-guide.adoc +++ b/docs/guides/developer-guide.adoc @@ -127,214 +127,80 @@ cabal test . *Learning Feedback*: Outcomes feed back to improve rules [[writing-rules]] -== Writing Rules (Logtalk) - -=== Logtalk Basics - -Logtalk extends Prolog with objects, protocols, and categories. Rules are defined as predicates within objects. - -=== Rule Object Structure - -[source,prolog] ----- -%% SPDX-License-Identifier: CC-BY-SA-4.0 -%% Custom rules for my-project - -:- object(my_project_rules). - - :- info([ - version is 1:'0':'0', - author is 'Your Name', - date is 2026-01-18, - comment is 'Custom CI/CD rules for my-project' - ]). - - %% Public predicates - :- public([ - repo_must_have/2, - block_commit_if/2, - auto_fix/2, - classify_severity/2, - suggest_fix/2 - ]). - - %% --- DECLARATIVE RULES --- - - %% All repos must have a README - repo_must_have(Repo, 'README.md') :- - repo_exists(Repo). - - %% Public repos must have a license - repo_must_have(Repo, 'LICENSE') :- - repo_is_public(Repo). - - %% --- PREVENTIVE RULES --- - - %% Block commits with large files - block_commit_if(Commit, large_file) :- - commit_adds_file(Commit, File), - file_size(File, Size), - Size > 10485760. % 10MB - - %% Block secrets in code - block_commit_if(Commit, secret_detected) :- - commit_content_matches(Commit, Pattern), - secret_pattern(Pattern). - - %% --- CURATIVE RULES --- - - %% Auto-fix missing .gitignore - auto_fix(Repo, missing_gitignore) :- - \+ repo_has_file(Repo, '.gitignore'), - inject_gitignore(Repo). - - %% --- SEVERITY CLASSIFICATION --- - - classify_severity(large_file, low). - classify_severity(secret_detected, critical). - classify_severity(missing_gitignore, low). - - %% --- FIX SUGGESTIONS --- - - suggest_fix(large_file, 'Use Git LFS for files >10MB'). - suggest_fix(secret_detected, 'Remove secrets and rotate credentials'). - suggest_fix(missing_gitignore, 'Add appropriate .gitignore for your language'). - -:- end_object. ----- - -=== Available Predicates - -These predicates are available from the core `cicd_rules` object: - -.Repository State Predicates -[cols="2,3"] -|=== -| Predicate | Description - -| `repo_exists(Repo)` -| True if repository exists - -| `repo_is_public(Repo)` -| True if repository is public - -| `repo_has_file(Repo, Path)` -| True if file exists in repo - -| `repo_uses_dependencies(Repo)` -| True if repo has dependency files - -| `repo_has_workflows(Repo)` -| True if repo has GitHub Actions - -| `repo_languages(Repo, Languages)` -| Unifies with list of languages - -| `repo_has_branch_protection(Repo)` -| True if branch protection enabled -|=== - -.Commit Predicates -[cols="2,3"] -|=== -| Predicate | Description - -| `commit_adds_file(Commit, File)` -| True if commit adds file - -| `commit_modifies_file(Commit, File)` -| True if commit modifies file - -| `commit_deletes_file(Commit, File)` -| True if commit deletes file - -| `commit_content_matches(Commit, Pattern)` -| True if content matches regex - -| `commit_modifies_workflow(Commit)` -| True if commit modifies workflows -|=== - -.Workflow Predicates -[cols="2,3"] -|=== -| Predicate | Description - -| `workflow_has_unpinned_action(Commit)` -| True if workflow has unpinned actions - -| `workflow_missing_permissions(Commit)` -| True if permissions not declared - -| `workflow_contains(Workflow, Pattern)` -| True if workflow contains pattern -|=== - -=== Pattern Matching - -Use Prolog pattern matching for flexible conditions: - -[source,prolog] ----- -%% Match any JavaScript/TypeScript file -js_file(File) :- - ( file_extension(File, '.js') - ; file_extension(File, '.ts') - ; file_extension(File, '.jsx') - ; file_extension(File, '.tsx') - ). - -%% Match test files -is_test_file(File) :- - ( atom_concat(_, '_test.go', File) - ; atom_concat('test_', _, File) - ; atom_concat(_, '.test.js', File) - ; atom_concat(_, '.spec.ts', File) - ). ----- - -=== Calling Learning Module - -Integrate with the learning system: - -[source,prolog] ----- -%% Use learned fix if confidence is high -smart_suggest_fix(Issue, Fix) :- - ( learning::get_confidence(Issue, Conf), - Conf >= 0.85, - learning::recommend_fix(Issue, Fix) - -> true - ; suggest_fix(Issue, Fix) % Fallback to static - ). - -%% Record outcome for learning -record_outcome(Issue, Fix, success) :- - learning::learn_from_fix(Issue, Fix, success). ----- - -=== Testing Rules - -Test rules with the Logtalk REPL: +== Writing Rules (Elixir) + +Rules are pure-Elixir modules under `+lib/rules/*.ex+` in the +`+Hypatia.Rules+` namespace. There is no Logtalk engine, loader, or +output format (ADR-001, 2026-04-14). The clause-by-clause transcription +of the retired Logtalk semantics — and the JSON contracts that replaced +Logtalk facts — is `+docs/rules/logtalk-migration.adoc+`. Do not add +`+.lgt+`/`+.logtalk+` files or Logtalk output settings: +`+scripts/check-no-active-logtalk.sh+` rejects them, and +`+Hypatia.Rules.SecurityErrors.language_replacement("logtalk")+` +answers `+"elixir"+` for scanned repositories. + +=== Shape of a rule module + +Follow the nearest existing module for the exact function shapes — the +estate deliberately does not impose one signature on every checker — +but keep to these invariants: + +* SPDX header and an `@moduledoc` whose first non-empty line summarises + the module (the generated catalogue extracts it). +* Checks are pure functions over explicit evidence (file lists, file + contents, alert/score/review facts) wherever possible, so they are + testable without a checkout or network. `+AuditPrevention+` is the + worked example for evidence-shaped checks. +* Findings are maps naming at least the rule, its severity, and a + human-readable description (match the neighbouring module's field + names; `+BuildSystemRules+` is a small example). +* Stable rule IDs. If the module emits prefixed IDs, keep them as + `+rule:+`/`+id:+` literals so the catalogue generator can see them. + +=== Where shared semantics live + +Do not fork shared tables into a new module: + +* Alert categories, severities, fixes, prevention workflows, SHA pins, + CWE mappings, and the language policy: `+Hypatia.Rules.SecurityErrors+` + (extend its tables and `+validate_alert/1+` rather than re-deriving + them; alert semantics changes belong there). +* Code-pattern detection: `+Hypatia.Rules.CodeSafety+`; workflow + checks: `+Hypatia.Rules.WorkflowAudit+` / + `+Hypatia.Rules.WorkflowHardening+`. +* Learned behaviour and confidence: `+Hypatia.Rules.Learning+`. + Observation counts inform confidence; they are never by themselves a + soundness claim. +* Standards-authored rule *data* (`.a2ml`) is loaded via + `+Hypatia.Rules.RuleLoader+` — data, never dynamically evaluated code. + +=== Registering and documenting a rule + +. Add `+lib/rules/.ex+` and, if it belongs to the facade's + documented surface, mention it in `+lib/rules/rules.ex+`. +. Regenerate the catalogue: `+./scripts/gen-rule-catalogue.sh+` + (updates `+docs/rules/catalogue.adoc+`; never hand-edit that file). +. Findings crossing a process boundary are JSON + (`+schema/findings.ncl+`); rulesets exchanged as data follow + `+schemas/ruleset.schema.json+`, learned-rule exports + `+schemas/learned-security-rules.schema.json+`. + +=== Testing rules [source,bash] ---- -# Start SWI-Prolog with Logtalk -swipl -g "['$LOGTALKUSER/adapters/swi.pl']" - -# Load the engine -?- logtalk_load(loader). - -# Test a predicate -?- cicd_rules::classify_severity(secret_detected, Severity). -Severity = critical. - -# Test with mock data -?- assertz(repo_has_file(test_repo, 'README.md')), - cicd_rules::repo_must_have(test_repo, File). -File = 'README.md'. +mix deps.get +mix compile --warnings-as-errors +mix test test/rules/_test.exs ---- +Tests live beside their families (`+test/rules/+` for rule modules, +`+test/security_errors_test.exs+` for the shared tables). Cover the +firing case, the nearest non-firing case, and any boundary the rule +states (for example `+< 8+` versus `+8+`). The CI rule-regression job +runs a targeted suite — add new rule tests to it when a module becomes +load-bearing. + == Creating Rulesets (Haskell) === Type-Safe Rule DSL @@ -818,13 +684,19 @@ fourmolu -i src/**/*.hs hlint src/ ---- -==== Logtalk +==== Elixir -Follow Logtalk coding guidelines: +Format and compile cleanly: + +[source,bash] +---- +mix format +mix compile --warnings-as-errors +---- -* Use snake_case for predicates -* Document all public predicates with `:- info/1` -* Keep objects focused and cohesive +Keep rule modules focused (one concern per module under `+lib/rules/+`), +document every public function, and prefer pure functions over explicit +evidence to hidden filesystem/network reads. === Testing Requirements @@ -893,7 +765,7 @@ make test # Run specific test suite cargo test -p hypatia-cli cabal test registry -logtalk_tester -d engine/ +mix test test/rules/ # Build release make build-release @@ -914,14 +786,15 @@ cargo doc --workspace --no-deps --open # Haskell docs cabal haddock --open -# Logtalk docs -cd engine && logtalk_doclet -f html +# Rule catalogue (generated from lib/rules/*.ex moduledocs) +./scripts/gen-rule-catalogue.sh ---- == Reference * <> * <> -* https://logtalk.org/documentation.html[Logtalk Documentation] +* https://elixir-lang.org/docs.html[Elixir Documentation] +* <<../rules/logtalk-migration.adoc#,Logtalk → Elixir Migration Ledger>> (historical semantics and replacement contracts) * https://www.haskell.org/documentation/[Haskell Documentation] * https://doc.rust-lang.org/book/[The Rust Book] diff --git a/docs/guides/faq.adoc b/docs/guides/faq.adoc index f0d055c2..8739c160 100644 --- a/docs/guides/faq.adoc +++ b/docs/guides/faq.adoc @@ -17,7 +17,7 @@ Frequently asked questions about hypatia, organized by topic. hypatia is a neurosymbolic CI/CD intelligence platform that combines: * *Neural learning* for pattern recognition across thousands of repositories -* *Symbolic reasoning* (Logtalk/Prolog) for fast, deterministic rule execution +* *Symbolic reasoning* (pure-Elixir rule modules) for fast, deterministic rule execution * *Formal verification* (Haskell/Liquid Haskell) for ruleset correctness proofs * *Multi-forge support* for GitHub, GitLab, Bitbucket, and more @@ -169,7 +169,7 @@ There are three effect types: Rules can be written in: -* *Logtalk* for symbolic rules (recommended for most cases) +* *Elixir* for symbolic rules — add a module under `lib/rules/*.ex` (the only rule language) * *Haskell* for type-safe rules with formal verification See <> for detailed instructions. diff --git a/docs/guides/glossary.adoc b/docs/guides/glossary.adoc index 48d5f7f2..19c2a725 100644 --- a/docs/guides/glossary.adoc +++ b/docs/guides/glossary.adoc @@ -62,7 +62,7 @@ The category of action a rule performs. There are three effect types: <>). + +There is no `engine/` tree, no Logtalk loader, and no tracked `.lgt` or +`.logtalk` source in this repository. This completes ADR-001 +(2026-04-14, "Hypatia is pure Elixir") at the level of rule semantics: +ADR-001 removed the runtime; the two residual Logtalk rule sources +(ECHIDNA's fact module and Hypatia's own audit-training blocks) are +transcribed below. + +== How fidelity is recorded + +Each transcribed item carries one disposition: + +[cols="1,3",options="header"] +|=== +|Disposition |Meaning + +|Exact +|Same inputs, same outputs, including failure/absence behaviour over +the stated domain. + +|Operationalised +|The Logtalk condition named an uninterpreted predicate +(`crate_type(parser)`, `nearby_pattern/1`, `pr_reviews < 2`, …). The +Elixir check states the concrete evidence test used in its place; the +interpretation is written down here and in the module, not hidden. + +|Extension +|The Elixir surface is a superset (more alert types, a total function +where Logtalk failed, an extra prevention mapping). Shared-domain +behaviour is unchanged. + +|Superseded +|The Logtalk value was wrong or unsafe under current estate policy and +was replaced on purpose. The old value is quoted here so the change is +auditable. + +|Dead code +|The Logtalk clause could never execute as written, or described a +runtime/dynamic-database mechanism replaced wholesale by an Elixir +subsystem. No clause-by-clause equivalent is pretended. +|=== + +== Consumer inventory and exact replacements + +[cols="2,2,3",options="header"] +|=== +|Consumer / stale claim |Was requesting |Replacement (this change) + +|`Mix.Tasks.Hypatia.BatchSecurityScan.generate_echidna_rules/1` +|Generated `learned_security_rules.lgt` / +`.audittraining/echidna-rules.lgt` containing +`security_rule(Type, Category, AutoFix, Count)` facts +|`generate_learned_rules/1` writes +`~/repos/echidna/rules/learned_security_rules.json` (when that +directory exists) or `.audittraining/echidna-rules.json`, conforming to +`schemas/learned-security-rules.schema.json`. See <>. + +|ECHIDNA `security_learning::export_rules/1`, +`cicd_integration::push_rules_to_cicd/0` +|Wrote `security_rule(Type, Category, Severity, AutoFix)` facts to +`~/repos/cicd-hyper-a/.audittraining/echidna-rules.lgt` +|Same JSON contract. The `.lgt` file itself is transcribed into +`Hypatia.Rules.SecurityErrors` (<>); ECHIDNA-side +removal/archival is coordinated in +`docs/rules/migration/echidna-security-learning-issue.md`. + +|ECHIDNA `docs/ECOSYSTEM-INTEGRATION.adoc`; +`echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml` +|"Auto-generates Logtalk rules after 5+ observations"; a live +(`scan-enabled = true`) descriptor with `report-format = "logtalk"` +|Same coordination packet: docs reworded to Elixir rule +modules / learned-rules JSON, and the descriptor value replaced with +exactly `report-format = "json"` (full DEED conversion may follow the +estate descriptile programme separately). + +|epistemic-types `.machine_readable/descriptiles/NEUROSYM.a2ml` +(at `5422cd5`, still on `main`) +|`report-format = "logtalk"` for a (disabled) Hypatia scan +|Status drift, not a dependency: Hypatia has had no such output since +ADR-001. The whole descriptor is re-expressed as a DEED +(`docs/rules/migration/epistemic-types_chora.deed`) with +`:report-format "json"`; landing instructions and issue text in +`docs/rules/migration/epistemic-types-neurosym-deed-issue.md`. + +|`integration/robot-repo-automaton/config.yml` +|`engine/loader.lgt`, `engine/rules/*.lgt`, distillation and export to +`learned_rules.lgt`, `format: logtalk`, Logtalk in `allowed_languages` +|Repointed to the Elixir application (`mix.exs`, `lib/rules/*.ex`, +`schema/findings.ncl`, `report_format: json`), to +`.audittraining/echidna-rules.json` + the learned-rules schema, and to +`logtalk` under `banned_languages` with `elixir` allowed. (The file's +long-dead Haskell-registry and ArangoDB sections are separate drift and +are not silently rewritten here.) + +|`.machine_readable/INTENT.contractile` +|Three active-tense Logtalk claims (pattern detection, "Logtalk rule +engine" invariant, Logtalk rules under `data/`) +|Corrected to the pure-Elixir engine in `lib/rules/*.ex`. Other stale +contents of that file are untouched by this change. + +|`Hypatia.Rules.SecurityErrors` language policy; `hooks/lib/common.sh` +|"logtalk" in the allowed-language set; hook library detected `.lgt` +files but never banned them +|Logtalk moves to banned with replacement `"elixir"` +(`language_replacement("logtalk") == "elixir"`); `is_banned_language` +now fires on `logtalk` and `get_language_alternative` answers +"Elixir (lib/rules/*.ex)". Detection of `.lgt` is retained precisely so +the ban can trigger. The standards language policies contain no +Logtalk/Prolog allowlist entry, so this aligns Hypatia with the estate +canon rather than inventing a new rule. + +|`verification/proofs/idris2/VerisimdbConnector.idr` +|`LogtalkFact`, "transit to Logtalk facts", a fictitious +`to_logtalk_facts` in a nonexistent `lib/verisimdb_connector.ex` +|Renamed to `FindingFact` (the canonical JSON finding projection), +pointed at the real `lib/verisim_connector.ex`, and recorded as a +*superseded statement* in `verification/PROOF-STATUS.adoc` — see +<>. The proof term is unchanged; its old target no longer +exists, which is exactly why the supersession is explicit. + +|standards DEED mapping/template; Hypatia deed test fixtures +|The standards `agentic-neurosym-playbook-to-repo-deed` mapping's own +template still emits `:report-format "logtalk"`, and two fixtures +vendored into `test/fixtures/deed_egress/` reproduce it +|Upstream-owned drift. The fixtures stay byte-faithful to standards +until standards lands the fix (deviating locally would falsify the +reader's conformance fixtures); they are exact-path exemptions in the +new guard, and the standards fix is coordinated in +`docs/rules/migration/standards-deed-mapping-issue.md`. + +|Active-tense documentation (developer guide, EXPLAINME, FAQ/glossary, +quickstarts, man page, API/security/testing docs, rules README, CLI and +schema docs) +|Described a live Logtalk engine under a nonexistent `engine/` +|Corrected to the canonical Elixir locations above. Genuinely +historical records — ADR-001, STATE/AGENTIC/MUST checkpoints, +roadmaps, dated audits, provenance/history narratives, and the arXiv +paper snapshot — are *not* rewritten; they are classified historical in +the guard allowlist and in `docs/DEBT-REGISTER.adoc` (D-2 closure note). +|=== + +No other live consumer of Logtalk output was found: the Hypatia CLI +accepts `json|text|github|sarif`; `Hypatia.CLI.Formatter`, panic-attack +integration, VCL, and the neural/dispatch pipeline are all JSON-shaped. + +[[learned-rules-json]] +== The learned-rules JSON contract + +There were *two* incompatible `security_rule/4` shapes, which is +itself sufficient reason the positional format had to die: + +* Hypatia's generator: `security_rule(Type, Category, AutoFix, Count)` +* ECHIDNA's exporter: `security_rule(Type, Category, Severity, AutoFix)` + +The replacement is one named-field JSON document, +`schemas/learned-security-rules.schema.json` ($id +`https://hyperpolymath.dev/schemas/hypatia/learned-security-rules`, +format version `1.0.0`), produced by +`Mix.Tasks.Hypatia.BatchSecurityScan`: + +[source,json] +---- +{ + "schema": "https://hyperpolymath.dev/schemas/hypatia/learned-security-rules", + "version": "1.0.0", + "generated_at": "2026-11-01T00:00:00Z", + "generator": "mix hypatia.batch_security_scan", + "source_alert_count": 1234, + "rules": [ + { + "alert_type": "TokenPermissionsID", + "category": "workflow_security", + "severity": "high", + "auto_fixable": true, + "observations": 87, + "fix": "Add granular workflow-level permissions ...", + "prevention_workflow": "workflow-linter.yml" + } + ] +} +---- + +Field provenance: + +[cols="1,2,2",options="header"] +|=== +|JSON field |Retired Logtalk source |Canonical Elixir source + +|`alert_type` |Field 1 of both shapes |GitHub/Scorecard alert id +|`category` |Field 2 of both shapes; `alert_category/2` +|`SecurityErrors.alert_category/1` (snake-case string; task-local +substring grouping only as fallback for ids outside the 18) +|`severity` |ECHIDNA field 3; `classify_severity/2` (absent from +Hypatia's generator) |`SecurityErrors.issue_severity/1` +|`auto_fixable` |Hypatia field 3 / ECHIDNA field 4; `is_auto_fixable/1` +|`SecurityErrors.auto_fixable?/1` +|`observations` |Hypatia field 4 (absent from ECHIDNA's export) +|Alert count in the producing scan. Evidence for belief formation +only — never a soundness claim (`src/Hypatia/ABI/Verdict.idr`). +|`fix` |`suggest_fix/2` |`SecurityErrors.fix_suggestion/1` (`null` when none) +|`prevention_workflow` |`get_prevention_workflow/2` +|`SecurityErrors.prevention_workflow/1` (`null` when none) +|=== + +All per-alert fields except `observations` are exactly +`Hypatia.Rules.SecurityErrors.validate_alert/1` rendered as JSON. + +[[echidna-ledger]] +== ECHIDNA `security_learning.lgt` — clause-by-clause ledger + +Source: `hyperpolymath/echidna:rules/security_learning.lgt` (only +`.lgt` file in that repository; added 2025-12-29; no loader or other +Logtalk consumer exists there). Target: +`Hypatia.Rules.SecurityErrors`, except where stated. + +=== `alert_category/2` — 18 facts → `@alert_categories` — *Exact* + +New canonical home: `SecurityErrors.alert_categories/0` / +`alert_category/1` (atoms, snake-case as in the Logtalk): + +* `workflow_security`: TokenPermissionsID, PinnedDependenciesID, + missing-workflow-permissions +* `code_security`: hard-coded-cryptographic-value, + remote-property-injection, sql-injection +* `code_quality`: unused-local-variable, syntax-error +* `dependency_vuln`: VulnerabilitiesID, unmaintained +* `process_hygiene`: SecurityPolicyID, MaintainedID, CodeReviewID, + BranchProtectionID, CIIBestPracticesID +* `missing_tests`: FuzzingID, SASTID, CITestsID + +Outside these 18, `alert_category/1` returns `nil`, mirroring the +absence of a fact. (The batch-scan task keeps a separate kebab-case +*display* grouping with substring fallback for unseen ids such as +`unused-import`; it is not a second semantic source and is commented +as such.) + +=== `classify_severity/2` → `issue_severity/1` — *Exact on the 18; one stated difference outside* + +* critical: hard-coded-cryptographic-value, sql-injection, + VulnerabilitiesID +* high: remote-property-injection, TokenPermissionsID, + missing-workflow-permissions +* medium: PinnedDependenciesID, SecurityPolicyID, BranchProtectionID, + CodeReviewID, syntax-error +* low (Logtalk catch-all `classify_severity(_, low)`): the remaining + seven — unused-local-variable, unmaintained, MaintainedID, + CIIBestPracticesID, FuzzingID, SASTID, CITestsID + +Before this change, SASTID, CITestsID, and unmaintained had no +explicit Elixir entry and fell through to `issue_severity/1`'s `:info` +default — a silent transcription bug against the Logtalk catch-all. +They are now explicit `:low` entries. For ids *neither* system has +seen, Elixir keeps its long-standing `:info` unknown-default rather +than the Logtalk catch-all's `low`; that is the single deliberate +difference, unreachable for any of the 18. + +=== `is_auto_fixable/1` — 6 facts → `@auto_fixable` — *Exact on the 18 (Elixir set is a superset overall)* + +TokenPermissionsID, PinnedDependenciesID, missing-workflow-permissions, +SecurityPolicyID, BranchProtectionID, unused-local-variable. The +Elixir set additionally contains later alert ids outside the Logtalk +domain; on the 18 the two agree exactly. + +=== `suggest_fix/2` — 13 facts → `@fix_suggestions` + +* *Exact (10), byte-identical strings:* SecurityPolicyID, + BranchProtectionID, CodeReviewID, CIIBestPracticesID, FuzzingID, + VulnerabilitiesID, hard-coded-cryptographic-value, + remote-property-injection, unused-local-variable, syntax-error. +* *Generalised (1):* PinnedDependenciesID — Logtalk + "Replace @v4 with @SHA # v4 format" → Elixir + "Replace @vN with @SHA # vN format" (same instruction, version + parameterised). +* *Superseded (2):* TokenPermissionsID and missing-workflow-permissions + — Logtalk prescribed `Add "permissions: read-all" at workflow level`. + Current OSSF guidance (and Hypatia's own + `scorecard_compliance/token_permissions` check) flags `read-all` + itself as high severity, so the canonical text prescribes granular + least-privilege permissions and explicitly warns against `read-all`. + Transcribing the old string would have made Hypatia recommend what + Hypatia flags. +* *No fix in either system (5 of the 18):* sql-injection, unmaintained, + MaintainedID, SASTID, CITestsID → `fix_suggestion/1` returns `nil`. + +=== `get_prevention_workflow/2` — 7 facts → `@prevention_workflows` + +Exact for six: TokenPermissionsID, PinnedDependenciesID, +missing-workflow-permissions → `workflow-linter.yml`; +hard-coded-cryptographic-value → `secret-scanner.yml`; +VulnerabilitiesID → `cargo-audit.yml`; SecurityPolicyID → +`scorecard-enforcer.yml`. + +* *Superseded (pre-existing, now ledgered):* BranchProtectionID — + Logtalk `branch-protection-enforcer.yml` → Elixir + `scorecard-enforcer.yml`. The Elixir value predates this change (it + groups BranchProtection with the other Scorecard process checks) and + every executable consumer has used it since; both workflow templates + still exist under `.audittraining/prevention/`. Changing it back is + a policy decision for a separate change, not a transcription fix. +* *Extension:* CodeReviewID → `scorecard-enforcer.yml` exists in + Elixir with no Logtalk counterpart. + +=== `cicd_integration::validate_alert/2` → `validate_alert/1` — *Total-function extension* + +Logtalk composed severity + fix + auto-fixability into +`alert_validation(Type, Severity, Fix, AutoFix)` and *failed* for any +alert without a `suggest_fix/2` clause. `SecurityErrors.validate_alert/1` +returns those fields plus the separately-looked-up `category` and +`prevention_workflow`, and is total: absent facts are `nil`/`false` +rather than query failure. Consumers that relied on Logtalk failure +as an "unknown alert" signal should test `category: nil` and +`fix: nil` in the returned map (or the JSON `null`s). + +=== Learning machinery — *Dead code / wholesale replacement* + +`load_training_data/1`, `read_training_examples/1`, +`process_training_term/1`, `learn_rules/0`, the `training_data/3` / +`learned_rule/4` / `fix_pattern/3` dynamic database, and +`sync_from_cicd/0` (hard-coded `~/repos/cicd-hyper-a` path, Prolog +`read/1` over a Guile Scheme module) never formed a runnable pipeline +and have no clause-level equivalents. Their *purpose* is served by: + +* `Hypatia.Rules.Learning` — outcome tracking, confidence, promotion + (the live learning subsystem); +* `Mix.Tasks.Hypatia.BatchSecurityScan` — fleet alert collection and + the learned-rules JSON above; +* `.audittraining/ERROR-CATALOG.scm` — retained as training-data + record (Scheme, not Logtalk). + +One latent ambiguity is worth recording because the JSON contract +dissolves it: `process_training_term/1` stored the catalog's second +field as `Type`, while `learn_rules/0` read the same position as +`Category`. Named JSON fields make that class of error impossible. + +=== Where `.audittraining/ERROR-CATALOG.scm` disagrees with the Logtalk + +The Logtalk header says its facts derive from `ERROR-CATALOG.scm`, but +the two disagree, and this transcription follows the *Logtalk* (the +values every executable consumer used), recording the Scheme variants +as open policy questions rather than smuggling them in: + +* Categories: the catalog splits fuzzing/SAST/CI-tests into + `missing-fuzzing` / `missing-sast` / `missing-tests`; Logtalk and + Elixir use one `missing_tests` group. +* Severities: catalog has VulnerabilitiesID high (Logtalk critical), + unmaintained medium (Logtalk low), FuzzingID/SASTID/CITestsID medium + (Logtalk low). +* Auto-fixability: catalog marks CodeReviewID, FuzzingID, SASTID, + CITestsID `#t`; Logtalk/Elixir say false. +* The catalog's extra entries (workflow-linter self-detection, + rust-toolchain input, duplicate workflows, …) were never in the + Logtalk; most already live in Elixir's extended severity/fix tables. + +Adopting the catalog's finer split or medium grading would change +live severities fleet-wide and needs its own decision. + +== Audit-training prevention rules AP001–AP015 + +Source: the `Prevention Rules (Logtalk)` blocks (2025-12-29) in seven +`.audittraining/security-errors/*.adoc` files — the last rule-bearing +Logtalk text inside Hypatia itself. Those blocks are retained in +place, now headed as historical, and are *not* executable sources. +Canonical target: `Hypatia.Rules.AuditPrevention`, whose `rules/0` +preserves every record verbatim as data (id, functor, name, effect, +description, conditions, action, origin, canonical equivalent). + +Common operationalisations: + +* The records had effects and actions but no severities. Finding + severity derives from the action (`block_merge_with_escalation` → + `:critical`; other `block_*` → `:high`; `warn_*`/`alert_*` → + `:medium`; `warn_and_log` → `:low`). Alert-id severities remain + `SecurityErrors`' business. +* Checks are pure functions over caller-supplied evidence (file lists, + file contents, tag/review/score facts). `check_all/1` runs every + implemented check whose evidence is present and is silent otherwise; + it never duplicates a check whose canonical home is another module. + +[cols="1,2,3,3",options="header"] +|=== +|ID |Logtalk rule |Canonical Elixir |Disposition / operationalisation + +|AP001 |`parser_rule(input_limits)` (bunsenite) +|`AuditPrevention.check_parser_input_limits/1` +|Implemented. `crate_type(parser)` is inferred from a Cargo description +naming a parser; the negated size-limit pattern is searched over the +supplied contents. + +|AP002 |`wasm_rule(memory_limits)` (bunsenite) +|`AuditPrevention.check_wasm_memory_limits/1` +|Implemented. `feature("wasm")` is inferred from Cargo wasm +features/dependencies; memory-limit markers searched likewise. + +|AP003 |`rust_rule(missing_audit)` (czech-file-knife) +|`AuditPrevention.check_missing_cargo_audit/2` +|Implemented exactly over evidence: `Cargo.toml` present and no +*workflow* content running `cargo audit` (a README mention is not CI). + +|AP004 |`rust_rule(workspace_vuln)` (czech-file-knife) +|`AuditPrevention.check_workspace_vuln/2` +|Implemented as the stated conjunction; `any_member_has_vuln` is +caller-supplied vulnerability evidence (this check does not itself +audit members — that is the scanner's/cargo-audit's job). + +|AP005 |`project_rule(missing_ci_tests)` (gitvisor) +|`AuditPrevention.check_missing_ci_tests/1` +|Implemented. The literal glob was `*test*.yml`; `.yaml` test +workflows are accepted as the same semantic object (recorded here +because the glob, read literally, would false-positive on them). +`has_source_code` uses the module's source-extension list. + +|AP006 |`project_rule(missing_sast)` (gitvisor) +|`AuditPrevention.check_missing_sast/2` +|Implemented; `codeql.yaml` accepted alongside the literal +`codeql.yml`, same reasoning as AP005. SecurityErrors' CodeQL language +matrix validation is the related pre-existing surface. + +|AP007 |`security_rule(property_injection)` (polyglot-i18n) +|`AuditPrevention.check_property_injection/1` +|Implemented. Both Logtalk access patterns are used verbatim; +`nearby_pattern(allowlist)` is operationalised as *same file*. CWE-915 +added to `SecurityErrors` for `remote-property-injection` / +`remote_property_injection` (previously unmapped). + +|AP008 |`code_quality_rule(unused_vars)` (polyglot-i18n) +|`SecurityErrors` metadata for `unused-local-variable` +|Metadata only, deliberately: the Logtalk condition is a compiler +diagnostic string ("is declared but its value is never read"), so the +detector of record stays the language compiler/linter. Severity +(`:low`), fix, category (`:code_quality`), and auto-fixability are +canonical in `SecurityErrors`. + +|AP009 |`crypto_rule(enhanced_review)` (proof-of-work) +|`AuditPrevention.check_crypto_enhanced_review/2` +|Implemented. `pr_reviews < 2` is read as the *required approving +review count* from branch protection; unknown (`nil`) never fires. + +|AP010 |`crypto_rule(require_fuzzing)` (proof-of-work) +|`AuditPrevention.check_crypto_require_fuzzing/2` +|Implemented: cryptography tag + no `fuzz/` path in the file list. + +|AP011 |`crypto_rule(no_panic)` (proof-of-work) +|`CodeSafety.scan_content/2` (`:panic_macro`, `:unwrap_without_check`, +`:expect_in_hot_path`) +|Already canonical — and a superset: the Elixir patterns fire in every +Rust repo, not only cryptography-tagged ones. Not duplicated. + +|AP012 |`meta_rule(rsr_self_compliance)` (supernorma) +|`RsrConformance` + `Dogfooding` +|Already canonical, generalised: the Logtalk hard-coded +`repo_name(supernorma)` becomes "any RSR-tooling repo, including +Hypatia itself" via the conformance oracle and dogfooding checks. + +|AP013 |`template_rule(exemplary_standards)` (supernorma) +|`AuditPrevention.check_exemplary_standards/2` +|Implemented exactly: tooling purpose + Scorecard score < 8; +boundary value 8 passes, mirroring `<`. + +|AP014 |`workflow_rule(missing_permissions)` (ubicity) +|`WorkflowAudit.check_permissions/1`, +`WorkflowHardening.wh002_excessive_permissions/1` +|Already canonical (and stricter: excessive grants are flagged, not +only absence). Not duplicated; `check_all/1` excludes it. + +|AP015 |`workflow_rule(unpinned_action)` (ubicity) +|`WorkflowHardening.wh004_unpinned_uses/1`, +`WorkflowAudit.check_unpinned_actions/1` +|Already canonical with one supersession: Logtalk excused a tag ref +with a trailing `# vN` comment; the Elixir checks require the +40-hex SHA form (comment or not). A comment beside a mutable tag is +not a pin. +|=== + +== epistemic-types `NEUROSYM.a2ml` → DEED + +Artifact: `docs/rules/migration/epistemic-types_chora.deed`, to land +at the epistemic-types repository root under that exact filename +(DEED v1.2.1 dispatches the `repo-deed` head by the +`_chora.deed` filename). If that repository has acquired a repo +deed in the meantime, the single `(neurosym …)` clause merges into it +instead — a repo has one deed, not two. + +Grammar authority: standards `1-formats/deed/spec/abnf/deed.abnf` +(v1.2.1); mapping authority: standards +`1-formats/deed/mappings/agentic-neurosym-playbook-to-repo-deed.adoc` +family 4. The transcription: + +* `[metadata]` → `(neurosym :project :version :status :last-updated + :author …)`, strings preserved. +* `[hypatia-config]` → `(hypatia :scan-enabled #f :scan-depth + standard :report-format "json" :scan-paths ("src/EpistemicTypes") + :file-globs ("*.agda"))`. Per the mapping: `scan-enabled` is a DEED + boolean (`#f`, never the word), `scan-depth` a symbol, paths/globs + lists of strings, DOIs would be strings (none here). +* `[neural-config] enabled=false` and `[ci] enabled=false` map + directly to `(neural-config :enabled #f)` / `(ci :enabled #f)`. +* The one intentional semantic change in the entire file: + `report-format` `"logtalk"` → `"json"`. + +*Proposed mapping extension (needs a standards row):* family 4 +currently fails closed on a populated `[symbolic-rules]` table. +epistemic-types has ten real rules, so the artifact transcribes them +as `(symbolic-rules (notes :checker-of-record … :safe-flags …) (rule +:name … :pattern … :severity … :note …) …)` — syntactically valid +under the ABNF (clauses are generic), semantically a row standards +should ratify; see the standards coordination issue. The same applies +to the extra `[metadata]` fields carried as `:status` / +`:last-updated` / `:author` strings. Pattern strings were converted +escape-for-escape so their parsed values are identical to the A2ML +(arbitrary-precision string escapes in DEED are only `\"`, `\\`, `\n`, +`\t`). The A2ML's prose comments survive as DEED comments/notes where +they carry meaning. + +Two deliberate non-changes: the repo's checker-of-record and +`--safe --without-K` flags are transcribed as-is — bringing that +repo's own proof profile to the estate's current strict invocation +(which adds `--cubical-compatible`) is a sibling proof-policy +reconciliation, not something to smuggle into a format migration; +and Hypatia's *own* `NEUROSYM.a2ml` is not deed-translated here, +because its populated neural configuration contains values DEED v1 +cannot yet express losslessly (the mapping's fail-closed gap). It +already declares JSON. + +Before landing in epistemic-types: run the standards gate — +`bun /path/to/standards/1-formats/deed/tools/deed_lint.js epistemic-types_chora.deed` +(expected exit 0) — and keep the receipt with the sibling PR. In this +change the artifact was validated against the ABNF subset it uses +(header, balanced single root form, exactly one string +`:schema-version`, boolean spelling, escape discipline, and +field-by-field equality with the `5422cd5` source) — that is authoring +evidence, not a standards-gate receipt. + +[[proofing]] +== Proofing: policy, grades, and exact statuses + +Proofing follows hyperpolymath/mathesis' +`estate-mathematical-architecture` (§§5–6) for grades and +metadatastician/standards `3-practice/PROOF-POLICY.adoc` for evidence +discipline; everything else follows the standards repo. In Mathesis' +ladder, *Grade 3* means the statement is formulated in Agda and +type-checks under the strict profile; Grade 2 additionally requires +translation into independent foundational system(s); Grade 1 +additionally requires those witnesses to compile in headless isolated +CI through verified checker APIs. Statuses are recorded exactly +(Open / Claimed / AGDA-PENDING / Grade 3 / …), never as a percentage, +and a checked model never silently becomes a runtime-refinement or +reconciliation claim. + +Applied here: + +[cols="2,2,2",options="header"] +|=== +|Claim |Artefact |Status at this change + +|Finite correspondence of the 18-alert category / severity / +auto-fixability / fix-presence tables, prevention agreement on the +six unchanged entries, and the two prevention non-equalities stated +exactly +|`verification/proofs/agda/LogtalkMigration.agda` +(`categoriesAgree`, `severitiesAgree`, `autoFixableAgrees`, +`fixPresenceAgrees`, `prevention*`, `catchAll*Low`) +|*Grade 3 — AGDA-VERIFIED.* Receipt recorded in +`verification/PROOF-STATUS.adoc`: official pinned Agda 2.8.0.2 Linux +release (builtins only, no stdlib), invocation `agda --safe +--without-K --cubical-compatible LogtalkMigration.agda`, success in +Verify Proofs run 41328302925, job 124912804344, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331; +source SHA-256 +bbd18e2747c84e2eda7ff5a778a2df7f8960a1ef47b1c253f316b9d97b9902a0. +The `agda strict-profile check` job fails hard (never skips) on every +relevant change. No Grade 2/1, Rocq/Lean reconciliation, or Elixir +runtime-refinement claim is made. + +|VeriSimDB connector field preservation +|`VerisimdbConnector.idr` (`factPreservesData` over `FindingFact`) +|Engineering (Idris2) evidence with a *superseded statement*: target +changed from the retired Logtalk fact format to the canonical JSON +finding record on 2026-11-01. Re-checked in Verify Proofs run +41328302925 (idris2 --check job 124912804086) at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331; the +model alone does not prove the Elixir connector refines it. + +|Elixir runtime behaviour of the transcription +|`test/security_errors_test.exs`, +`test/rules/audit_prevention_test.exs` +|TESTED in CI run 41328303014 (Elixir Compile job 124912999773: +`mix compile --warnings-as-errors`, targeted ExUnit including these +suites, and the no-Logtalk guard) at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331. Tests are +evidence about the Elixir code; they are not a substitute +for the Agda statement above, nor vice versa. + +|AP001–AP015 check semantics beyond table correspondence +|`AuditPrevention` + canonical checkers +|No formal claim. The regex/evidence semantics are specified in code ++ tests; formalising them is future theory work and would enter at +Open/Claimed, not by inheriting the alert-table status. +|=== + +== Guard: keeping Logtalk out + +`scripts/check-no-active-logtalk.sh` (wired into CI) enforces, over +tracked files: + +* no `*.lgt` / `*.logtalk` files outside the allowlist; +* no active configuration requesting Logtalk — loader paths, +`format: logtalk`, `report-format` set to `logtalk` in A2ML/DEED +form, or generated `.lgt` outputs — outside the allowlist. + +Exemptions live in `.logtalk-allowlist` as *exact paths only* +(following the `.hypatia-ignore` precedent: no wildcards, no directory +blankets), each with a classification and removal condition. The list +is shrink-only: adding an entry requires the same review as adding a +rule, and the script fails if an allowlisted path no longer exists +(the classic stale-exemption rot). Historical prose mentioning +Logtalk is not banned — the guard targets executable/config forms, +and this ledger, the migration packet, the proof model, and the +seven audit-training originals are its initially allowlisted records. +Estate rollout (other repos have their own trees) is proposed through +the standards coordination issue rather than pretend-enforced from +here. + +== Sibling coordination + +Prepared, ready-to-file packets (Hypatia cannot land changes in +sibling repositories from this branch): + +* `docs/rules/migration/echidna-security-learning-issue.md` — remove + `rules/security_learning.lgt` from ECHIDNA's active tree (preferred: + delete, pointing at this ledger as the transcription of record; + acceptable fallback: move under an explicit archive path), and fix + any ECHIDNA docs still presenting Logtalk generation as live. +* `docs/rules/migration/epistemic-types-neurosym-deed-issue.md` + + `epistemic-types_chora.deed` — land the deed, run `deed_lint`, + then delete `.machine_readable/descriptiles/NEUROSYM.a2ml`. +* `docs/rules/migration/standards-deed-mapping-issue.md` — fix the + `"logtalk"` literal in the standards DEED mapping/template (the + upstream source of Hypatia's two vendored fixtures), ratify the + populated-`[symbolic-rules]` mapping row proposed above, and + consider the no-active-Logtalk guard for estate-wide adoption. + +== Acceptance summary + +* Canonical active rules: `lib/rules/*.ex`, documented here and in + `lib/rules/README.adoc` / the generated catalogue. ✓ +* ECHIDNA Logtalk semantics faithfully in Elixir, divergences + itemised (3 superseded/generalised fix strings, 1 prevention + supersession + 1 extension, catch-all severity bug fixed, + total-function `validate_alert`). ✓ (CI receipt recorded above) +* Hypatia's embedded Logtalk rules AP001–AP015 transcribed to + `AuditPrevention` or pointed at their pre-existing canonical + checkers. ✓ (CI receipt recorded above) +* Logtalk-generating code replaced by a schema'd JSON contract. ✓ +* Every consumer that requested Logtalk has an exact replacement + above. ✓ +* epistemic-types descriptor re-expressed as an ABNF-conformant DEED + with `report-format "json"`. ✓ (landing + lint receipt: sibling) +* ECHIDNA `.lgt` removal/archival coordinated; standards drift + coordinated. ✓ (landing: siblings) +* Repository guard against new active `.lgt` files / Logtalk output + settings, exact-path shrink-only allowlist, wired into CI. ✓ +* Proofing graded honestly: finite correspondence at Mathesis + *Grade 3 / AGDA-VERIFIED* on the recorded strict-profile Agda + receipt; Idris statement supersession recorded and re-checked; no + claim inflated beyond its evidence. ✓ diff --git a/docs/rules/migration/echidna-security-learning-issue.md b/docs/rules/migration/echidna-security-learning-issue.md new file mode 100644 index 00000000..5454c7b1 --- /dev/null +++ b/docs/rules/migration/echidna-security-learning-issue.md @@ -0,0 +1,54 @@ + +# Issue packet for hyperpolymath/echidna + +**Suggested title:** Retire `rules/security_learning.lgt` — semantics now canonical in Hypatia Elixir + JSON + +**Prepared from:** Hypatia branch `arena/82ed8898-hypatia`, `docs/rules/logtalk-migration.adoc` (2026-11-01) + +--- + +## Summary + +`rules/security_learning.lgt` is dead, active-looking Logtalk. As of this audit it is the only `.lgt` path in ECHIDNA's recursive tree, there is no Logtalk loader/settings file or other in-tree consumer for it, and ECHIDNA's documented stack is Rust/Julia/Idris2/Zig/Chapel. Its security-alert semantics have now been transcribed clause-by-clause into Hypatia's canonical Elixir rule system, so the file can be removed (or explicitly archived) without losing meaning. + +## Where the semantics went + +All in `hyperpolymath/hypatia`, module `Hypatia.Rules.SecurityErrors` (`lib/rules/security_errors.ex`): + +| Logtalk | Elixir | +|---|---| +| `alert_category/2` (18 facts) | `alert_categories/0`, `alert_category/1` | +| `classify_severity/2` | `issue_severity/1` — including the `low` catch-all, now explicit for `SASTID`, `CITestsID`, `unmaintained` (previously drifting to `:info`) | +| `is_auto_fixable/1` (6 facts) | `auto_fixable?/1` | +| `suggest_fix/2` (13 facts) | `fix_suggestion/1` | +| `get_prevention_workflow/2` | `prevention_workflow/1` | +| `cicd_integration::validate_alert/2` | `validate_alert/1` (total-function extension: returns `nil` fields instead of failing; also folds in category + prevention) | +| `export_rules/1` / `push_rules_to_cicd/0` (`security_rule/4` `.lgt`) | `Mix.Tasks.Hypatia.BatchSecurityScan` now emits `learned_security_rules.json` per `schemas/learned-security-rules.schema.json` | +| dynamic learning predicates | superseded wholesale by `Hypatia.Rules.Learning`; no clause-level equivalent is claimed | + +Deliberate divergences, all ledgered in Hypatia `docs/rules/logtalk-migration.adoc`: + +- `TokenPermissionsID` / `missing-workflow-permissions` fix text no longer prescribes `permissions: read-all` (Hypatia flags `read-all` itself); granular least-privilege text is canonical. +- `PinnedDependenciesID` fix generalised `@v4` → `@vN`. +- `BranchProtectionID` prevention is `scorecard-enforcer.yml` (long-standing Elixir value), not the Logtalk `branch-protection-enforcer.yml`; `CodeReviewID` gained a prevention mapping with no Logtalk counterpart. +- Wholly unknown alert ids get severity `:info` in Elixir rather than the Logtalk catch-all `low`; all 18 known ids agree exactly. + +Proof status, stated exactly: the finite table correspondence is modelled in Hypatia `verification/proofs/agda/LogtalkMigration.agda` and is **Mathesis Grade 3 / AGDA-VERIFIED** on a strict-profile receipt (Agda 2.8.0.2, `agda --safe --without-K --cubical-compatible`, Hypatia Verify Proofs run 41328302925 at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331; full receipt in Hypatia `verification/PROOF-STATUS.adoc`). Elixir behaviour is pinned by ExUnit tests in the same PR's CI. The Agda model grades the finite table correspondence only — no runtime-refinement or Grade 2/1 claim is being sold here. + +## Requested changes in ECHIDNA + +1. **Delete `rules/security_learning.lgt`** (preferred). Git history plus the Hypatia ledger preserve it; no replacement `.lgt` should be created. If a local archival copy is required instead, move it to a non-executable archival name (e.g. `docs/archive/security_learning.logtalk.txt`) with a header stating it is superseded by Hypatia `lib/rules/security_errors.ex` and linking the ledger — do not leave an active-looking `.lgt` under `rules/`. +2. **Fix `docs/ECOSYSTEM-INTEGRATION.adoc`**, which currently says the learning engine "Auto-generates Logtalk rules after 5+ observations". Replacement wording: learned patterns are proposed as Hypatia Elixir rule modules (`lib/rules/*.ex`) and/or emitted as learned-security-rules JSON; observation counts are belief-forming evidence, never a soundness claim. +3. **Fix `echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml`**: it has `scan-enabled = true` with `report-format = "logtalk"`. Exact replacement value: `report-format = "json"` (Hypatia findings, `schema/findings.ncl`). A full DEED conversion can ride the estate descriptile programme separately; the format value should not wait for it. +4. Sweep the tree for any remaining `.lgt` paths, Logtalk loader/settings references, or `format.*logtalk` settings after the deletion. + +## Acceptance criteria + +- [ ] No `.lgt` / `.logtalk` file remains in an active path (`git ls-files '*.lgt' '*.logtalk'` empty, or only under an explicitly archival, non-executable name). +- [ ] No document in ECHIDNA describes Logtalk rule generation/output as current behaviour. +- [ ] `echidna-playground` NEUROSYM requests JSON. +- [ ] ECHIDNA docs (or the archival stub) point at Hypatia `docs/rules/logtalk-migration.adoc` as the transcription of record. + +## Non-goals + +No change to ECHIDNA's prover architecture, rule-learning research direction, or non-Logtalk subsystems. This is solely retirement of a dead format and its stale documentation. diff --git a/docs/rules/migration/epistemic-types-neurosym-deed-issue.md b/docs/rules/migration/epistemic-types-neurosym-deed-issue.md new file mode 100644 index 00000000..66a648e0 --- /dev/null +++ b/docs/rules/migration/epistemic-types-neurosym-deed-issue.md @@ -0,0 +1,56 @@ + +# Issue packet for hyperpolymath/epistemic-types + +**Suggested title:** Replace `NEUROSYM.a2ml` with a repo DEED — `report-format = "logtalk"` is retired + +**Prepared from:** Hypatia branch `arena/82ed8898-hypatia`; artifact `docs/rules/migration/epistemic-types_chora.deed`; ledger `docs/rules/logtalk-migration.adoc` +**Source pinned:** `.machine_readable/descriptiles/NEUROSYM.a2ml` at `5422cd5` (identical on `main` at audit time) + +--- + +## Summary + +This repo's `NEUROSYM.a2ml` declares `report-format = "logtalk"` for Hypatia. That is status drift, not a working dependency: Hypatia's rule engine has been pure Elixir (`lib/rules/*.ex`) since its ADR-001 (2026-04-14), its report formats are `json|text|github|sarif`, and the scan here is disabled (`scan-enabled = false`) in any case. + +The estate direction is that this descriptor information lives in the repository's DEED, in the `(neurosym …)` clause defined by standards (`1-formats/deed/spec/abnf/deed.abnf` v1.2.1; mapping `1-formats/deed/mappings/agentic-neurosym-playbook-to-repo-deed.adoc`, family 4). A complete, ready-to-land transcription is attached from Hypatia: `epistemic-types_chora.deed`. + +## The change + +1. Add **`epistemic-types_chora.deed`** at the repository root, with exactly the content of Hypatia `docs/rules/migration/epistemic-types_chora.deed`. + - Filename matters: DEED dispatches the `repo-deed` head by the `_chora.deed` name. + - If this repo has acquired a repo deed since the audit, do **not** add a second one — merge the single `(neurosym …)` clause from the artifact into the existing deed instead. +2. Delete **`.machine_readable/descriptiles/NEUROSYM.a2ml`** once the deed lints (step 3). +3. Validate with the standards gate and keep the receipt in the landing PR: + + ```bash + bun /path/to/standards/1-formats/deed/tools/deed_lint.js epistemic-types_chora.deed + # expected: exit 0 + ``` + +## Semantic diff (complete) + +Everything from the `5422cd5` descriptor is carried over: + +- `[metadata]` → `:project`, `:version`, `:status`, `:last-updated`, `:author` (strings verbatim). +- `[hypatia-config]` → `(hypatia :scan-enabled #f :scan-depth standard :report-format "json" :scan-paths ("src/EpistemicTypes") :file-globs ("*.agda"))`. Note DEED booleans are `#t/#f` and `scan-depth` is a symbol, per the mapping. +- All ten `[symbolic-rules]` entries → `(rule :name … :pattern … :severity … :note …)`, patterns converted escape-for-escape so the parsed strings are identical; `[symbolic-rules.notes]` → `(notes :checker-of-record … :safe-flags …)`. +- `[neural-config] enabled=false`, `[ci] enabled=false` → `:enabled #f` clauses. +- Meaningful A2ML comments are preserved as DEED comments. + +**The only intentional semantic change:** `:report-format "logtalk"` → `"json"`. + +Two non-changes, on purpose: + +- The checker-of-record (`agda --no-libraries -i src src/EpistemicTypes/All.agda`) and `--safe --without-K` flags are transcribed as-is. Whether this repo should also adopt the estate's current strict-profile addition `--cubical-compatible` is a *separate* proof-policy reconciliation — please don't bundle it silently into this format migration, and don't read this issue as a proof-grade claim about the Agda sources. +- No scan behaviour changes: the scan remains disabled. + +## One standards dependency to be aware of + +Family 4 of the standards mapping currently *fails closed* on a populated `[symbolic-rules]` table (it has no ratified row yet — this repo is the motivating case, with ten real rules). The `(symbolic-rules (notes …) (rule …))` shape in the artifact is valid DEED syntax under the ABNF, and a companion standards issue (Hypatia `docs/rules/migration/standards-deed-mapping-issue.md`) proposes ratifying exactly this row. Landing here does not depend on that ratification for syntactic validity, but the shape should be treated as "proposed standard" until the row lands. + +## Acceptance criteria + +- [ ] `deed_lint.js` exits 0 on the landed deed; receipt recorded in the PR. +- [ ] `grep -ri logtalk` over active (non-historical) files finds no report-format or rule-format claim. +- [ ] `NEUROSYM.a2ml` deleted; nothing references the old path. +- [ ] `just check` (Agda proof check) unaffected and still the soundness floor, as the original notes say. diff --git a/docs/rules/migration/epistemic-types_chora.deed b/docs/rules/migration/epistemic-types_chora.deed new file mode 100644 index 00000000..c42b56fc --- /dev/null +++ b/docs/rules/migration/epistemic-types_chora.deed @@ -0,0 +1,92 @@ +;; SPDX-License-Identifier: MPL-2.0 +; epistemic-types_chora.deed — proposed repo deed clause set for +; hyperpolymath/epistemic-types, prepared in Hypatia as the exact +; replacement for .machine_readable/descriptiles/NEUROSYM.a2ml at +; epistemic-types@5422cd5. Land at the sibling repository root; if a +; repo deed has been created there in the meantime, merge the single +; (neurosym ...) clause into it instead of adding a second deed. +; Sole intentional semantic change: :report-format "logtalk" -> +; "json" (Hypatia has had no Logtalk output since ADR-001, +; 2026-04-14; the value was status drift, not a dependency). +; Grammar: metadatastician/standards 1-formats/deed/spec/abnf/deed.abnf +; v1.2.1. Mapping: 1-formats/deed/mappings/ +; agentic-neurosym-playbook-to-repo-deed.adoc family 4, extended for +; the populated [symbolic-rules] table (see Hypatia +; docs/rules/logtalk-migration.adoc). +(repo-deed + :schema-version "1.0.0" + :canonical-name "epistemic-types" + (neurosym + :project "epistemic-types" + :version "0.1.0" + :status "prototype" + :last-updated "2026-06-15" + :author "Jonathan D.A. Jewell (hyperpolymath) " + (hypatia + :scan-enabled #f + :scan-depth standard + :report-format "json" + :scan-paths ("src/EpistemicTypes") + :file-globs ("*.agda")) + ; Custom symbolic rules for this repository. Agda has no + ; believe_me/unsafeCoerce; the honest analogues to flag are escape + ; hatches and library coupling that would weaken the constructive, + ; --safe --without-K, no-postulate, no-stdlib discipline here. + (symbolic-rules + (notes + :checker-of-record "agda --no-libraries -i src src/EpistemicTypes/All.agda" + :safe-flags "--safe --without-K") + (rule + :name "no-postulate" + :pattern "postulate" + :severity "critical" + :note "This repo postulates nothing. Any `postulate` is a silent axiom; laws must be fields or proofs.") + (rule + :name "no-terminating-pragma" + :pattern "\\{-# TERMINATING #-\\}" + :severity "critical" + :note "Bypasses the termination checker; breaks the constructive honesty guarantee.") + (rule + :name "no-non-terminating-pragma" + :pattern "\\{-# NON_TERMINATING #-\\}" + :severity "critical" + :note "Same escape hatch as TERMINATING; not used here and must not appear.") + (rule + :name "no-primTrustMe" + :pattern "primTrustMe" + :severity "critical" + :note "Unsound equality witness; equivalent in spirit to believe_me. Must never appear.") + (rule + :name "no-trustMe" + :pattern "trustMe" + :severity "critical" + :note "Library-level wrapper over primTrustMe; same prohibition.") + (rule + :name "no-no-positivity-check" + :pattern "\\{-# NO_POSITIVITY_CHECK #-\\}" + :severity "critical" + :note "Disables the positivity checker; would admit non-strictly-positive (unsound) data.") + (rule + :name "no-no-termination-check" + :pattern "\\{-# NO_TERMINATION_CHECK #-\\}" + :severity "critical" + :note "Legacy termination bypass; forbidden for the same reason as TERMINATING.") + (rule + :name "no-stdlib-import" + :pattern "open import (Data|Relation|Function|Algebra|Category|Codata|Effect|Foreign|IO|Reflection|Tactic|Agda\\.Builtin\\.Reflection)\\b" + :severity "high" + :note "Repo builds with `agda --no-libraries`; only `Agda.Builtin.*` and `Agda.Primitive` are permitted. A standard-library import would not type-check under `just check` and breaks the self-contained guarantee.") + (rule + :name "no-unsafe-options" + :pattern "\\{-# OPTIONS[^#]*--type-in-type" + :severity "critical" + :note "`--type-in-type` is inconsistent; the repo target is `--safe --without-K`.") + (rule + :name "echo-not-collapsed" + :pattern "Echo .* = .* E " + :severity "medium" + :note "Heuristic: Echo C y (certified residue and separately measured bounds) and E kappa A (epistemic availability) are distinct modalities. Their composition is meaningful; their identification is a modelling error. Manual review on hit.")) + (neural-config + :enabled #f) + (ci + :enabled #f))) diff --git a/docs/rules/migration/standards-deed-mapping-issue.md b/docs/rules/migration/standards-deed-mapping-issue.md new file mode 100644 index 00000000..5258d5f0 --- /dev/null +++ b/docs/rules/migration/standards-deed-mapping-issue.md @@ -0,0 +1,82 @@ + +# Issue packet for metadatastician/standards + +**Suggested title:** DEED neurosym mapping: retire the `"logtalk"` report-format example and ratify populated `[symbolic-rules]` + +**Prepared from:** Hypatia branch `arena/82ed8898-hypatia`; motivating case `hyperpolymath/epistemic-types` (`NEUROSYM.a2ml` @ `5422cd5`); ledger Hypatia `docs/rules/logtalk-migration.adoc` + +--- + +## 1. The `"logtalk"` literal is a retired format presented as the example + +`1-formats/deed/mappings/agentic-neurosym-playbook-to-repo-deed.adoc` (family 4) maps: + +``` +[hypatia-config] report-format → (neurosym (hypatia :report-format "logtalk")) — verbatim STRING +``` + +and the template/valid fixtures under `1-formats/deed/tools/fixtures/` reproduce `:report-format "logtalk"`. Two of those fixtures are vendored byte-for-byte into Hypatia's DEED-reader conformance tests (`test/fixtures/deed_egress/`), so the drift now has downstream copies that cannot be corrected locally without falsifying fixture provenance. + +Facts: + +- Hypatia — the system the `report-format` names — retired Logtalk in ADR-001 (2026-04-14). Its report formats are `json | text | github | sarif`; `json` is canonical (findings: `schema/findings.ncl`). There is no Logtalk output to request. +- Neither `0-canon/rsr/LANGUAGE-POLICY.adoc` nor `3-practice/LANGUAGE-POLICY.adoc` lists Logtalk (or Prolog) as approved. +- At audit, at least two live descriptors carry the value as if current: `epistemic-types/.machine_readable/descriptiles/NEUROSYM.a2ml` and `echidna/echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml` (the latter with `scan-enabled = true`). + +**Requested:** + +1. Change the mapping example to `:report-format "json"`, and add an explicit migration note: a source value of `"logtalk"` is a *retired format*, to be normalised to `"json"` during A2ML→DEED migration, **not** carried across verbatim. (This is the one place where "verbatim STRING" is the wrong rule: verbatim preservation of an unimplementable format is how the drift propagated.) +2. Consider closing the value set in the row (as `scan-depth` already is): `json text github sarif`, string-valued, with `json` canonical. +3. Regenerate/update the affected fixtures and template pair so vendored copies downstream (Hypatia's reader fixtures) can re-sync cleanly. +4. In the same pass, fix any converter behaviour in `1-formats/deed/tools/a2ml_to_deed.py` / `migrate_a2ml_to_deed.sh` that would emit `"logtalk"` from a legacy descriptor without complaint. + +## 2. Ratify the populated `[symbolic-rules]` row (currently fail-closed) + +Family 4 says populated `[symbolic-rules]` / `[neural-config]` fail closed pending table rows. epistemic-types is a real, minimal motivating case: ten rules, a notes sub-table, `neural-config` present but disabled, plus `[metadata]` fields (`status`, `last-updated`, `author`) and a `[ci]` section the current rows don't cover. + +Hypatia's proposed transcription (full artifact: `docs/rules/migration/epistemic-types_chora.deed` in the Hypatia repo) uses only generic DEED clause syntax from `deed.abnf` v1.2.1: + +```scheme +(repo-deed + :schema-version "1.0.0" + :canonical-name "epistemic-types" + (neurosym + :project "epistemic-types" + :version "0.1.0" + :status "prototype" + :last-updated "2026-06-15" + :author "Jonathan D.A. Jewell (hyperpolymath) " + (hypatia + :scan-enabled #f + :scan-depth standard + :report-format "json" + :scan-paths ("src/EpistemicTypes") + :file-globs ("*.agda")) + (symbolic-rules + (notes + :checker-of-record "agda --no-libraries -i src src/EpistemicTypes/All.agda" + :safe-flags "--safe --without-K") + (rule :name "no-postulate" :pattern "postulate" + :severity "critical" :note "…") + …) + (neural-config :enabled #f) + (ci :enabled #f))) +``` + +**Requested:** add family-4 rows for + +- `[symbolic-rules] rules[]` → `(symbolic-rules (rule :name S :pattern S :severity S :note S)…)`; +- `[symbolic-rules.notes]` → `(symbolic-rules (notes :checker-of-record S :safe-flags S))` (or a ruling on where notes belong); +- `[metadata] status/author` and `[ci] enabled` (currently only `version`/`last-updated` have rows); +- and state explicitly which A2ML values, if any, still fail closed after these rows (e.g. populated `[neural-config]` floats — Hypatia's own `NEUROSYM.a2ml` remains unconvertible for that reason and is intentionally left for that ruling). + +## 3. Optional estate guard + +Hypatia now carries `scripts/check-no-active-logtalk.sh` + an exact-path, shrink-only `.logtalk-allowlist` (no tracked `*.lgt/*.logtalk`; no active config requesting Logtalk loaders/formats). If standards wants this estate-wide, Hypatia's implementation is offered as the seed for a template/CI-snippet ruling rather than each repo inventing its own patterns. + +## Acceptance criteria + +- [ ] No standards mapping, template, or *valid* fixture presents `"logtalk"` as a current Hypatia report format. +- [ ] The A2ML→DEED tooling normalises or rejects a legacy `"logtalk"` value loudly (never emits it silently). +- [ ] Family-4 rows exist for populated `[symbolic-rules]`, its notes, `[ci]`, and the extra `[metadata]` fields — or an explicit ruling records a different canonical shape, in which case Hypatia's epistemic-types artifact will be regenerated to match. +- [ ] Downstream vendored fixtures (Hypatia `test/fixtures/deed_egress/`) can be re-synced from the corrected standards fixtures. diff --git a/docs/security/security-audit.adoc b/docs/security/security-audit.adoc index e87c126f..c186fa67 100644 --- a/docs/security/security-audit.adoc +++ b/docs/security/security-audit.adoc @@ -10,7 +10,7 @@ toc::[] == Overview -This document provides a comprehensive security audit checklist for the hypatia neurosymbolic CI/CD intelligence platform. It covers all layers of the system: Rust adapters, Haskell verification registry, Logtalk rule engine, data stores (ArangoDB, Dragonfly), container deployments, and API surfaces. +This document provides a comprehensive security audit checklist for the hypatia neurosymbolic CI/CD intelligence platform. It covers all layers of the system: Rust adapters, Haskell verification registry, Elixir rule engine (`lib/rules/*.ex`), data stores (ArangoDB, Dragonfly), container deployments, and API surfaces. === Audit Scope @@ -20,7 +20,7 @@ This document provides a comprehensive security audit checklist for the hypatia | Forge Adapters | Rust | High | Verification Registry | Haskell | Medium -| Rule Engine | Logtalk/SWI-Prolog | Medium +| Rule Engine | Elixir/BEAM (`lib/rules/*.ex`) | Medium | Graph Database | ArangoDB | High | Cache Layer | Dragonfly (Redis-compatible) | Medium | Container Runtime | Docker/Kubernetes | High @@ -81,7 +81,7 @@ This document provides a comprehensive security audit checklist for the hypatia === Ruleset Validation [%interactive] -* [ ] *INPUT-RULE-001*: Logtalk/Prolog rules are parsed in a sandboxed environment +* [ ] *INPUT-RULE-001*: Rules are compiled Elixir modules or validated rule *data* (`RuleLoader`); no untrusted rule code is dynamically evaluated * [ ] *INPUT-RULE-002*: Haskell rulesets pass type checking before acceptance * [ ] *INPUT-RULE-003*: Rules cannot execute arbitrary shell commands * [ ] *INPUT-RULE-004*: Rules cannot access network resources directly diff --git a/docs/security/threat-model.adoc b/docs/security/threat-model.adoc index 8d4147e8..ba47bc15 100644 --- a/docs/security/threat-model.adoc +++ b/docs/security/threat-model.adoc @@ -38,7 +38,7 @@ Due to its position in the software supply chain and its access to repository cr ┌──────────────────────────────────────┼──────────────────────────────────────┐ │ TRUST BOUNDARY │ │ ┌─────────────┐ ┌─────────────┐ ┌─────────────┐ ┌─────────────┐ │ -│ │ Haskell │ │ Logtalk │ │ Rust │ │ Rust │ │ +│ │ Haskell │ │ Elixir │ │ Rust │ │ Rust │ │ │ │ Registry │ │ Engine │ │ Adapters │ │ CLI │ │ │ └──────┬──────┘ └──────┬──────┘ └──────┬──────┘ └─────────────┘ │ │ │ │ │ │ diff --git a/docs/specs/ada-tui-audit-spec.adoc b/docs/specs/ada-tui-audit-spec.adoc index a90d18b3..e207657d 100644 --- a/docs/specs/ada-tui-audit-spec.adoc +++ b/docs/specs/ada-tui-audit-spec.adoc @@ -177,7 +177,7 @@ GitHub Actions workflow validation: == Integration Points === hypatia Integration -* Export audit results to Logtalk rule engine +* Export audit results to Hypatia as JSON findings (`schema/findings.ncl`) for evaluation by the Elixir rule modules * Feed error patterns to neurosymbolic learning * Trigger hook wave propagation on fixes diff --git a/docs/testing/audit.adoc b/docs/testing/audit.adoc index e4e6dbf9..83e62755 100644 --- a/docs/testing/audit.adoc +++ b/docs/testing/audit.adoc @@ -47,7 +47,7 @@ VerisimConnector → PatternRegistry → TriangleRouter → DispatchManifest pipeline |*BLD* (Build) |strong |`+ci.yml+` exercises -`+cargo check/clippy/test+`, Haskell registry, Logtalk engine +`+cargo check/clippy/test+`, Haskell registry, Elixir rule engine |*EXE* (Execution) |strong |`+zig_ffi_smoke_test.exs+` (248 LOC), `+vcl_client_test.exs+` (582 LOC), `+vcl_file_executor_test.exs+` (642 diff --git a/docs/wiki-pages/Rule-Catalogue.md b/docs/wiki-pages/Rule-Catalogue.md index 39ca846b..ebae6b9c 100644 --- a/docs/wiki-pages/Rule-Catalogue.md +++ b/docs/wiki-pages/Rule-Catalogue.md @@ -7,22 +7,29 @@ Every rule module Hypatia ships. **Generated** from `lib/rules/*.ex` — regener | Module | Rule IDs | Purpose | |---|---|---| +| `actions_lock` | — | Strict local validation for machine-generated `gh actions-lock` v0.0.2/v0.0.3 files. | | `admin_merge_eligibility` | DBA002 | Recognises PR shapes that are safe to admin-merge in bulk when the | +| `audit_prevention` | AP001 AP002 AP003 AP004 AP005 AP006 AP007 AP008 AP009 AP010 AP011 AP012 AP013 AP014 AP015 | Audit-training prevention rules AP001–AP015, transcribed from Logtalk. | | `baseline_health` | BH001 BH002 BH003 BH004 BH005 BH006 BH007 BH008 | Detects degraded `main`-branch baseline conditions that allow silent rot. | | `branch_protection` | BP001 BP002 BP003 BP004 BP005 BP006 BP007 BP008 BP009 | Branch-protection hygiene rules drawn from the CIS GitHub Benchmark, | | `build_system_rules` | — | Build-tool configuration anti-patterns that block estate CI but slip past | | `cicd_rules` | — | Primary Elixir CI/CD policy rules (migrated from legacy Logtalk engine). | | `code_safety` | — | Primary Elixir rules for code safety (migrated from legacy Logtalk engine). | -| `code_scanning_alerts` | CSA001 CSA002 CSA003 CSA004 | GitHub Code Scanning alert querying (CodeQL + third-party SARIF). | +| `code_scanning_alerts` | CSA001 CSA002 CSA003 CSA004 CSA005 CSA006 | GitHub Code Scanning alert querying (CodeQL + third-party SARIF). | | `dependabot_alerts` | DA001 DA002 DA003 DA004 | GitHub Dependabot alert querying and risk assessment. | | `disambiguation_rules` | DR001 | Cross-reference / language-disambiguation rules. | | `dogfooding` | HYP-DOG-001 HYP-DOG-003 HYP-DOG-004 HYP-DOG-005 HYP-DOG-006 HYP-DOG-007 HYP-DOG-008 HYP-DOG-009 HYP-DOG-010 | Dogfooding compliance rules -- HYP-DOG-001 through HYP-DOG-010. | | `forge_adapters` | — | Primary Elixir forge adapter rules (migrated from legacy Logtalk engine). | -| `git_state` | GS001 GS002 GS003 GS004 GS005 GS006 GS007 | Git repository synchronisation state checks. | +| `git_state` | GS001 GS002 GS003 GS004 GS005 GS006 GS007 GS008 | Git repository synchronisation state checks. | | `green_web` | — | Green Web Foundation certification checks for hyperpolymath repositories. | | `honest_completion` | — | Honest completion audit -- cross-references claimed completion percentages | -| `learning` | — | Learning engine rules absorbed from Logtalk engine/rules/learning.lgt | +| `implementation_inside_canon` | — | Executable evaluator for the standards-authored HYP-S009 rule. | +| `learning` | — | Learning engine rules absorbed from the retired Logtalk learning and | | `migration_rules` | — | Primary Elixir ReScript migration rules (migrated from legacy Logtalk engine). | +| `moved_repositories` | — | Versioned records of confirmed repository moves relevant to reusable workflows. | +| `pin_integrity` | — | Pin-level integrity rules for workflow and lockfile content. | +| `pin_sites` | — | Structural `uses:` pin sites on one line of workflow YAML. | +| `pr_automerge` | — | Decide whether a pull request is an unambiguous bump or chore that may be | | `proof_obligation` | — | ProofObligation recipe type for Hypatia. | | `proof_strategy_selection` | — | Prover-strategy selection from VeriSimDB historical outcomes. | | `research_extensions` | RE001 RE002 RE003 RE004 RE005 RE006 RE007 RE008 RE009 RE010 | Static detection of GitHub Actions workflow defects sourced from | @@ -35,17 +42,19 @@ Every rule module Hypatia ships. **Generated** from `lib/rules/*.ex` — regener | `secret_scanning_alerts` | SSA001 SSA002 SSA003 SSA004 | GitHub Secret Scanning alert querying. | | `security_errors` | — | Primary Elixir security error database (migrated from legacy Logtalk engine). | | `sha_bump_propagation` | — | Detection: an estate-wide reusable workflow has been bumped to a new SHA | +| `standards_repo` | — | The names of the estate standards repository. | | `strategy_drift` | — | N4: Detects strategy-shift events and flags previously-failed attempts | -| `structural_drift` | SD001 SD002 SD003 SD004 SD005 SD006 SD007 SD008 SD009 SD010 SD011 SD013 SD014 SD021 SD022 SD023 | Structural drift detection rules. | +| `structural_drift` | SD001 SD002 SD003 SD004 SD005 SD006 SD007 SD008 SD009 SD010 SD011 SD013 SD014 SD021 SD022 SD023 SD024 | Structural drift detection rules. | | `supply_chain` | SC001 SC002 SC003 SC004 SC005 SC006 SC007 SC008 SC009 SC010 SC011 SC012 SC013 | Supply-chain integrity rules drawn from OSSF Scorecard, SLSA, OWASP | -| `workflow_audit` | ERR-WF-013 ERR-WF-014 WF013 WF014 WF015 WF016 WF017 WF018 WF019 WF020 WF021 WF022 WF023 WF024 WF-025 WF025 | CI/CD workflow audit rules. | -| `workflow_hardening` | WH001 WH002 WH003 WH004 WH005 WH006 WH007 WH008 WH009 WH010 WH011 WH012 | Static detection of dangerous GitHub Actions workflow patterns. | +| `workflow_audit` | ERR-WF-013 ERR-WF-014 WF-025 WF013 WF014 WF015 WF016 WF017 WF018 WF019 WF020 WF021 WF022 WF023 WF024 WF025 WF026 WF027 WF028 | CI/CD workflow audit rules. | +| `workflow_hardening` | WH001 WH002 WH003 WH004 WH005 WH006 WH007 WH008 WH009 WH010 WH011 WH012 WH013 WH014 | Static detection of dangerous GitHub Actions workflow patterns. | ## ID families | Prefix | Family | |---|---| | `AM` | Admin-merge eligibility | +| `AP` | Audit-prevention rules transcribed from the historical Logtalk blocks | | `BH` | Baseline health (silent `main` rot) | | `BP` | Branch protection (CIS / Scorecard / NIST SSDF) | | `CSA` | Code-scanning alerts (CodeQL + third-party SARIF) | diff --git a/hooks/lib/common.sh b/hooks/lib/common.sh index d15d86ae..90b2133f 100755 --- a/hooks/lib/common.sh +++ b/hooks/lib/common.sh @@ -160,6 +160,8 @@ detect_languages() { echo "$_files" | grep -qE '\.json$' && _langs="$_langs json" echo "$_files" | grep -qE '\.scm$' && _langs="$_langs scheme" echo "$_files" | grep -qE '\.ncl$' && _langs="$_langs nickel" + # .lgt is still *detected* so the RSR ban below can fire on it; + # detection is not approval (Logtalk retired estate-wide, ADR-001). echo "$_files" | grep -qE '\.(lgt|logtalk)$' && _langs="$_langs logtalk" echo "$_files" | grep -qE '\.adoc$' && _langs="$_langs asciidoc" echo "$_files" | grep -qE '\.md$' && _langs="$_langs markdown" @@ -171,7 +173,7 @@ detect_languages() { # Usage: if is_banned_language "typescript"; then ... is_banned_language() { case "$1" in - typescript|go|python|java|kotlin) return 0 ;; + typescript|go|python|java|kotlin|logtalk) return 0 ;; *) return 1 ;; esac } @@ -185,6 +187,7 @@ get_language_alternative() { go) echo "Rust" ;; python) echo "Elixir or Rust" ;; java|kotlin) echo "Rust" ;; + logtalk) echo "Elixir (lib/rules/*.ex)" ;; *) echo "allowed languages" ;; esac } diff --git a/integration/robot-repo-automaton/config.yml b/integration/robot-repo-automaton/config.yml index 0672d9a5..bffbdf4e 100644 --- a/integration/robot-repo-automaton/config.yml +++ b/integration/robot-repo-automaton/config.yml @@ -9,13 +9,17 @@ integration: # Connection to hypatia engine engine: - # Logtalk rule engine - logtalk: - loader: engine/loader.lgt - rules: - - engine/rules/cicd_rules.lgt - - engine/rules/rule_distiller.lgt - - engine/rules/forge_adapters.lgt + # Canonical Elixir rule engine (ADR-001, 2026-04-14). Rules are + # compiled Elixir modules in lib/rules/*.ex — there is no loader + # file and no Logtalk/Prolog runtime. Migration ledger: + # docs/rules/logtalk-migration.adoc. + elixir: + application: hypatia + mix_project: mix.exs + rules_glob: lib/rules/*.ex + catalogue: docs/rules/catalogue.adoc + findings_schema: schema/findings.ncl + report_format: json # Haskell verification registry registry: @@ -113,15 +117,18 @@ learning: path: training-data/ format: scm # ERROR-CATALOG.scm format - # Distillation settings + # Distillation settings. Learned rules are Elixir modules in + # lib/rules/*.ex (see rules.a2ml lifecycle); the machine-readable + # export for cross-repo consumers is the learned-security-rules JSON. distillation: min_occurrences: 3 - output_path: engine/rules/learned_rules.lgt + output_path: .audittraining/echidna-rules.json - # Export formats + # Export formats (replaces the retired Logtalk security_rule/4 file) exports: - - format: logtalk - path: engine/rules/learned_rules.lgt + - format: json + path: .audittraining/echidna-rules.json + schema: schemas/learned-security-rules.schema.json - format: haskell path: registry/src/CicdHyperA/LearnedRules.hs @@ -179,6 +186,7 @@ rsr_policy: - java - kotlin - swift + - logtalk # retired 2026-04-14 (ADR-001); rules are Elixir # Allowed languages allowed_languages: @@ -186,7 +194,7 @@ rsr_policy: - rust - gleam - julia - - logtalk + - elixir - haskell - bash - nickel diff --git a/lib/mix/tasks/hypatia.batch_security_scan.ex b/lib/mix/tasks/hypatia.batch_security_scan.ex index 8a044877..ea66da19 100644 --- a/lib/mix/tasks/hypatia.batch_security_scan.ex +++ b/lib/mix/tasks/hypatia.batch_security_scan.ex @@ -13,11 +13,12 @@ defmodule Mix.Tasks.Hypatia.BatchSecurityScan do Outputs: * `.audittraining/security-errors/.md` — per-repo audit markdown * `.audittraining/security-errors/SUMMARY.md` — org-wide summary - * `~/repos/echidna/rules/learned_security_rules.lgt` (if that dir - exists) or `.audittraining/echidna-rules.lgt` — Logtalk-format - rules for echidnabot. NB: Hypatia retired its own Logtalk engine; - this output is purely for consumption by echidnabot in a separate - repo. + * `~/repos/echidna/rules/learned_security_rules.json` (if that dir + exists) or `.audittraining/echidna-rules.json` — learned security + rules for echidnabot in the JSON format defined by + `schemas/learned-security-rules.schema.json`. This replaces the + retired Logtalk `security_rule/4` export; see + `docs/rules/logtalk-migration.adoc` for the exact field mapping. """ use Mix.Task @@ -28,6 +29,14 @@ defmodule Mix.Tasks.Hypatia.BatchSecurityScan do @output_dir ".audittraining/security-errors" @echidna_rules_dir "~/repos/echidna/rules" + # Display grouping for the generated markdown (kebab-case headings). + # The canonical alert-type semantics live in + # `Hypatia.Rules.SecurityErrors.alert_categories/0` (exact match, + # snake-case atoms, transcribed from ECHIDNA's retired + # `security_learning.lgt`); this local table is kept only because its + # substring matching also buckets alert ids the canonical table has + # never seen (for example `unused-import`). The JSON learned-rules + # export below reads the canonical table via `validate_alert/1`. @alert_categories %{ "workflow-security" => ~w(TokenPermissionsID PinnedDependenciesID missing-workflow-permissions), @@ -86,7 +95,7 @@ defmodule Mix.Tasks.Hypatia.BatchSecurityScan do Mix.shell().info(" Total alerts: #{length(all_alerts)}") generate_summary(all_alerts, length(repos)) - generate_echidna_rules(all_alerts) + generate_learned_rules(all_alerts) Mix.shell().info("\n✅ Complete! Training data generated in #{@output_dir}") end @@ -244,55 +253,71 @@ defmodule Mix.Tasks.Hypatia.BatchSecurityScan do Mix.shell().info("Generated: #{filepath}") end - defp generate_echidna_rules(all_alerts) do + # Learned-rules export. This replaces two retired, mutually + # incompatible Logtalk `security_rule/4` shapes — Hypatia's generated + # `security_rule(Type, Category, AutoFix, Count)` and ECHIDNA's + # exported `security_rule(Type, Category, Severity, AutoFix)` — with + # one named-field JSON object carrying the union of their data plus + # the fix/prevention lookups: + # + # {"alert_type", "category", "severity", "auto_fixable", + # "observations", "fix", "prevention_workflow"} + # + # Schema: schemas/learned-security-rules.schema.json. Semantics come + # from the canonical `Hypatia.Rules.SecurityErrors.validate_alert/1`, + # not from this task's display grouping. + defp generate_learned_rules(all_alerts) do by_rule = Enum.reduce(all_alerts, %{}, fn a, acc -> Map.update(acc, a.rule_id, 1, &(&1 + 1)) end) now = DateTime.utc_now() |> DateTime.truncate(:second) |> DateTime.to_iso8601() - header = """ - %% SPDX-License-Identifier: MPL-2.0 - %% Auto-generated security rules from #{length(all_alerts)} alerts across hyperpolymath org - %% Generated: #{now} - - :- object(security_rules). - - :- public([ - check_workflow/2, - check_code/2, - check_dependencies/2 - ]). - - """ - - body = + rules = by_rule - |> Enum.sort_by(fn {_r, c} -> -c end) - |> Enum.map_join("\n", fn {rule_id, count} -> - category = categorize_alert(rule_id) - auto_fix = MapSet.member?(@auto_fixable, rule_id) - - """ - %% Rule: #{rule_id} (seen #{count} times) - %% Category: #{category} - %% Auto-fixable: #{auto_fix} - security_rule('#{rule_id}', #{category}, #{auto_fix}, #{count}). - """ + |> Enum.sort_by(fn {rule_id, count} -> {-count, rule_id} end) + |> Enum.map(fn {rule_id, count} -> + validation = Hypatia.Rules.SecurityErrors.validate_alert(rule_id) + + %{ + "alert_type" => rule_id, + "category" => category_string(validation.category, rule_id), + "severity" => Atom.to_string(validation.severity), + "auto_fixable" => validation.auto_fixable, + "observations" => count, + "fix" => validation.fix, + "prevention_workflow" => validation.prevention_workflow + } end) - footer = "\n:- end_object.\n" + payload = %{ + "schema" => "https://hyperpolymath.dev/schemas/hypatia/learned-security-rules", + "version" => "1.0.0", + "generated_at" => now, + "generator" => "mix hypatia.batch_security_scan", + "source_alert_count" => length(all_alerts), + "rules" => rules + } - rules = header <> body <> footer echidna_dir = Path.expand(@echidna_rules_dir) filepath = if File.dir?(echidna_dir) do - Path.join(echidna_dir, "learned_security_rules.lgt") + Path.join(echidna_dir, "learned_security_rules.json") else - Path.join(".audittraining", "echidna-rules.lgt") + Path.join(".audittraining", "echidna-rules.json") end - File.write!(filepath, rules) - Mix.shell().info("Generated echidna rules: #{filepath}") + File.write!(filepath, Jason.encode!(payload, pretty: true) <> "\n") + Mix.shell().info("Generated learned security rules: #{filepath}") + end + + defp category_string(category, _rule_id) when is_atom(category) do + Atom.to_string(category) + end + + defp category_string(nil, rule_id) do + rule_id + |> categorize_alert() + |> String.replace("-", "_") end end diff --git a/lib/rules/README.adoc b/lib/rules/README.adoc index 28fc2637..1514855b 100644 --- a/lib/rules/README.adoc +++ b/lib/rules/README.adoc @@ -1,32 +1,67 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -= lib/rules/ — Elixir Rules Engine += lib/rules/ — the canonical Hypatia rule system -Pattern detection rules applied during the analysis phase. -Each module provides a set of `check/2` or `generate_findings/2` functions -that take scan evidence and return typed finding structs. +This directory is Hypatia's active, canonical rule system: pure-Elixir +modules compiled into the `hypatia` Mix application. There is no +`engine/` tree, no Logtalk loader, and no Logtalk output format (ADR-001, +2026-04-14; semantic migration completed 2026-11-01 — see +`docs/rules/logtalk-migration.adoc`). -== Rule Modules +The inventory is intentionally *not* hand-listed here; it drifts. The +generated catalogue is the reference, and the modules themselves win in +any disagreement: + +[source,bash] +---- +./scripts/gen-rule-catalogue.sh # -> docs/rules/catalogue.adoc +---- + +== Entry points + +* `Hypatia.Rules` (`rules.ex`) — facade over the rule modules. +* `Hypatia.Rules.RuleLoader` + `Hypatia.Rules.RsrCriteria` + — standards-authored rule data (`.a2ml`) loaded as data, never as code. +* `Hypatia.Rules.Learning` — outcome tracking, confidence, and pattern + promotion (the live learning subsystem that replaced the old dynamic + Logtalk learning predicates). + +== Canonical semantic homes most often needed [cols="2,3"] |=== -|Module |Domain - -|`cicd_rules.ex` |CI/CD pipeline integrity checks -|`code_safety.ex` |Memory safety, unsafe blocks, banned patterns -|`dependabot_alerts.ex` |Dependency vulnerability detection -|`dogfooding.ex` |Ecosystem self-application compliance -|`forge_adapters.ex` |Cross-forge adapter validation -|`git_state.ex` |Git hygiene: branch protection, signed commits, stale branches -|`green_web.ex` |Green Web Foundation compliance -|`honest_completion.ex` |Detects inflated completion claims (believe_me, sorry, stub counts) -|`learning.ex` |Feedback loop quality and learning signal checks -|`migration_rules.ex` |Language migration progress tracking -|`proof_obligation.ex` |Formal verification coverage requirements -|`proof_strategy_selection.ex` |Selects appropriate proof strategy per finding type -|`root_hygiene.ex` |Root-level file hygiene (SPDX, licence, README) -|`scorecard_compliance.ex` |OpenSSF Scorecard check compliance -|`security_errors.ex` |Common security error patterns (MD5, HTTP, hardcoded secrets) -|`strategy_drift.ex` |Dispatch strategy drift detection over time -|`structural_drift.ex` |Repository structure drift from RSR template -|`workflow_audit.ex` |GitHub Actions workflow security and correctness +|Module |Owns + +|`security_errors.ex` +|Shared security knowledge: error categories, the canonical alert +category/severity/fix/prevention tables and `validate_alert/1` +(transcribed from ECHIDNA's retired `security_learning.lgt`), SHA pins +and pin exemptions, secret patterns, CodeQL language support, CWE +mappings, and the RSR language policy (Logtalk banned → Elixir). + +|`audit_prevention.ex` +|Audit-training prevention rules AP001–AP015, transcribed from the +historical Logtalk blocks in `.audittraining/security-errors/*.adoc`: +verbatim rule records (`rules/0`) plus the evidence-shaped checks that +had no other home. Rules whose checks already existed point at them +instead of duplicating them. + +|`code_safety.ex` / `workflow_audit.ex` / `workflow_hardening.ex` +|Content-level code and workflow checkers (including the canonical +homes of AP011, AP014, and AP015). + +|`rsr_conformance.ex` / `dogfooding.ex` +|RSR v2.0 conformance oracle and self-application checks (canonical +home of AP012). |=== + +== Output contracts + +Rules produce findings consumed as JSON (`schema/findings.ncl`), never +as Logtalk facts. Rulesets exchanged as data follow +`schemas/ruleset.schema.json`; learned security-rule exports follow +`schemas/learned-security-rules.schema.json` +(`Mix.Tasks.Hypatia.BatchSecurityScan`). + +New `.lgt`/`.logtalk` sources and Logtalk output settings are blocked +by `scripts/check-no-active-logtalk.sh` (exact-path exemptions, with +removal conditions, in `.logtalk-allowlist`). diff --git a/lib/rules/audit_prevention.ex b/lib/rules/audit_prevention.ex new file mode 100644 index 00000000..33e565cc --- /dev/null +++ b/lib/rules/audit_prevention.ex @@ -0,0 +1,563 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +defmodule Hypatia.Rules.AuditPrevention do + @moduledoc """ + Audit-training prevention rules AP001–AP015, transcribed from Logtalk. + + These fifteen rules were the last rule-bearing Logtalk text in this + repository: the `Prevention Rules (Logtalk)` blocks embedded in + `.audittraining/security-errors/*.adoc` (2025-12-29). They are recorded + here verbatim as data (`rules/0` — functor, name, effect, description, + conditions, action, origin file) so the transcription can be diffed + against the originals preserved in `docs/rules/logtalk-migration.adoc`. + + Every rule names its canonical Elixir equivalent. Where the estate + already had a live checker (workflow permissions, unpinned actions, + Rust panic patterns, RSR self-compliance), this module points at it and + does not duplicate it. Where no live checker existed, this module + implements the missing check as a pure function over caller-supplied + evidence (file lists, file contents, alert/tag/review/score facts). + Callers opt in with that evidence; `check_all/1` runs every check whose + evidence is present and stays silent on the rest. + + Two operationalisations are recorded here rather than hidden: + + * The Logtalk records carry an effect and an action but no severity. + Findings therefore derive severity from the action + (`block_merge_with_escalation` is `:critical`; other `block_*` + actions are `:high`; `warn_*`/`alert_*` are `:medium`; + `warn_and_log` is `:low`). `Hypatia.Rules.SecurityErrors` stays + canonical for alert-id severities. + * The property-injection rule's `nearby_pattern` condition is + operationalised as *same file*: both access patterns must occur in + one file with no allowlist marker anywhere in that file. + """ + + @rules [ + %{ + id: "AP001", + rule: "parser_input_limits", + logtalk_functor: "parser_rule", + logtalk_name: "input_limits", + effect: :preventive, + description: "Config parsers must have input size limits", + conditions: [ + "crate_type(parser)", + ~S{not(pattern("MAX.*SIZE|size.*limit"))} + ], + action: "warn_reviewer", + origin: ".audittraining/security-errors/bunsenite.adoc", + canonical: "Hypatia.Rules.AuditPrevention.check_parser_input_limits/1" + }, + %{ + id: "AP002", + rule: "wasm_memory_limits", + logtalk_functor: "wasm_rule", + logtalk_name: "memory_limits", + effect: :preventive, + description: "WASM crates must limit memory allocation", + conditions: [ + ~S{feature("wasm")}, + ~S{not(pattern("memory.*limit|max.*alloc"))} + ], + action: "warn_reviewer", + origin: ".audittraining/security-errors/bunsenite.adoc", + canonical: "Hypatia.Rules.AuditPrevention.check_wasm_memory_limits/1" + }, + %{ + id: "AP003", + rule: "rust_missing_audit", + logtalk_functor: "rust_rule", + logtalk_name: "missing_audit", + effect: :preventive, + description: "Rust repos must run cargo audit in CI", + conditions: [ + ~S{file_exists("Cargo.toml")}, + ~S{not(workflow_contains("cargo audit"))} + ], + action: "block_release", + origin: ".audittraining/security-errors/czech-file-knife.adoc", + canonical: "Hypatia.Rules.AuditPrevention.check_missing_cargo_audit/2" + }, + %{ + id: "AP004", + rule: "rust_workspace_vuln", + logtalk_functor: "rust_rule", + logtalk_name: "workspace_vuln", + effect: :curative, + description: "Check all workspace members for vulnerabilities", + conditions: [ + ~S{file_exists("Cargo.toml")}, + ~S{contains("[workspace]")}, + "any_member_has_vuln" + ], + action: "alert_maintainer", + origin: ".audittraining/security-errors/czech-file-knife.adoc", + canonical: "Hypatia.Rules.AuditPrevention.check_workspace_vuln/2" + }, + %{ + id: "AP005", + rule: "project_missing_ci_tests", + logtalk_functor: "project_rule", + logtalk_name: "missing_ci_tests", + effect: :preventive, + description: "Repos must have automated test workflow", + conditions: [ + ~S{not(file_exists(".github/workflows/*test*.yml"))}, + "has_source_code" + ], + action: "block_release", + origin: ".audittraining/security-errors/gitvisor.adoc", + canonical: "Hypatia.Rules.AuditPrevention.check_missing_ci_tests/1" + }, + %{ + id: "AP006", + rule: "project_missing_sast", + logtalk_functor: "project_rule", + logtalk_name: "missing_sast", + effect: :preventive, + description: "Multi-language repos must have SAST configured", + conditions: [ + "language_count > 1", + ~S{not(file_exists(".github/workflows/codeql.yml"))} + ], + action: "warn_maintainer", + origin: ".audittraining/security-errors/gitvisor.adoc", + canonical: "Hypatia.Rules.AuditPrevention.check_missing_sast/2" + }, + %{ + id: "AP007", + rule: "security_property_injection", + logtalk_functor: "security_rule", + logtalk_name: "property_injection", + effect: :preventive, + description: "Reject dynamic property access without validation", + conditions: [ + ~S{pattern("\[\s*\w+Input\s*\]")}, + ~S{pattern("\[\s*req\.(body|query|params)")}, + ~S{not(nearby_pattern("allowedProps|whitelist|ALLOWED"))} + ], + action: "block_commit", + origin: ".audittraining/security-errors/polyglot-i18n.adoc", + canonical: "Hypatia.Rules.AuditPrevention.check_property_injection/1" + }, + %{ + id: "AP008", + rule: "code_quality_unused_vars", + logtalk_functor: "code_quality_rule", + logtalk_name: "unused_vars", + effect: :curative, + description: "Flag files with unused variables for cleanup", + conditions: [ + ~S{pattern("is declared but its value is never read")} + ], + action: "warn_and_log", + origin: ".audittraining/security-errors/polyglot-i18n.adoc", + canonical: + "Hypatia.Rules.SecurityErrors metadata for \"unused-local-variable\"; the condition is a compiler-diagnostic string, so the language compiler/linter remains the detector" + }, + %{ + id: "AP009", + rule: "crypto_enhanced_review", + logtalk_functor: "crypto_rule", + logtalk_name: "enhanced_review", + effect: :preventive, + description: "Crypto repos require 2+ reviewers", + conditions: [ + "repo_tag(cryptography)", + "pr_reviews < 2" + ], + action: "block_merge", + origin: ".audittraining/security-errors/proof-of-work.adoc", + canonical: "Hypatia.Rules.AuditPrevention.check_crypto_enhanced_review/2" + }, + %{ + id: "AP010", + rule: "crypto_require_fuzzing", + logtalk_functor: "crypto_rule", + logtalk_name: "require_fuzzing", + effect: :preventive, + description: "Crypto repos must have fuzz targets", + conditions: [ + "repo_tag(cryptography)", + ~S{not(dir_exists("fuzz/"))} + ], + action: "block_release", + origin: ".audittraining/security-errors/proof-of-work.adoc", + canonical: "Hypatia.Rules.AuditPrevention.check_crypto_require_fuzzing/2" + }, + %{ + id: "AP011", + rule: "crypto_no_panic", + logtalk_functor: "crypto_rule", + logtalk_name: "no_panic", + effect: :preventive, + description: "Crypto code must not panic", + conditions: [ + "repo_tag(cryptography)", + ~S{pattern("panic!|unwrap\(\)|expect\(")} + ], + action: "warn_reviewer", + origin: ".audittraining/security-errors/proof-of-work.adoc", + canonical: + "Hypatia.Rules.CodeSafety.scan_content/2 Rust patterns :panic_macro, :unwrap_without_check and :expect_in_hot_path (a superset: they fire in every Rust repo, not only cryptography-tagged ones)" + }, + %{ + id: "AP012", + rule: "meta_rsr_self_compliance", + logtalk_functor: "meta_rule", + logtalk_name: "rsr_self_compliance", + effect: :preventive, + description: "RSR tooling repos must pass all RSR checks", + conditions: [ + "repo_name(supernorma)", + "has_rsr_violation" + ], + action: "block_merge_with_escalation", + origin: ".audittraining/security-errors/supernorma.adoc", + canonical: + "Hypatia.Rules.RsrConformance (the RSR v2.0 oracle) with Hypatia.Rules.Dogfooding self-application checks; generalised from the hard-coded repo_name(supernorma) to every RSR-tooling repo" + }, + %{ + id: "AP013", + rule: "template_exemplary_standards", + logtalk_functor: "template_rule", + logtalk_name: "exemplary_standards", + effect: :diagnostic, + description: "Template/tooling repos should exceed normal standards", + conditions: [ + "repo_purpose(tooling)", + "scorecard_score < 8" + ], + action: "alert_maintainer", + origin: ".audittraining/security-errors/supernorma.adoc", + canonical: "Hypatia.Rules.AuditPrevention.check_exemplary_standards/2" + }, + %{ + id: "AP014", + rule: "workflow_missing_permissions", + logtalk_functor: "workflow_rule", + logtalk_name: "missing_permissions", + effect: :preventive, + description: "Reject workflows without permissions declaration", + conditions: [ + ~S{file_type(".github/workflows/*.yml")}, + ~S{not(contains("permissions:"))} + ], + action: "block_merge", + origin: ".audittraining/security-errors/ubicity.adoc", + canonical: + "Hypatia.Rules.WorkflowAudit.check_permissions/1 and Hypatia.Rules.WorkflowHardening.wh002_excessive_permissions/1" + }, + %{ + id: "AP015", + rule: "workflow_unpinned_action", + logtalk_functor: "workflow_rule", + logtalk_name: "unpinned_action", + effect: :preventive, + description: "Reject workflows with unpinned actions", + conditions: [ + ~S{pattern("uses:.*@v[0-9]")}, + ~S{not(pattern("#.*v[0-9]"))} + ], + action: "block_merge", + origin: ".audittraining/security-errors/ubicity.adoc", + canonical: + "Hypatia.Rules.WorkflowHardening.wh004_unpinned_uses/1 and Hypatia.Rules.WorkflowAudit.check_unpinned_actions/1 (the Logtalk second condition is superseded: a trailing \"# vN\" comment beside a tag ref is not a pin; the Elixir checks require the 40-hex SHA form)" + } + ] + + @source_extensions ~w(.rs .ex .exs .erl .gleam .jl .ml .mli .hs .lhs .zig .idr .agda + .affine .res .resi .js .mjs .cjs .sh .py .go .java .kt .swift + .c .h .cpp .hpp .adb .ads .lean .v) + + @property_input_pattern ~r/\[\s*\w+Input\s*\]/ + @property_request_pattern ~r/\[\s*req\.(body|query|params)/ + @property_allowlist_pattern ~r/allowedProps|whitelist|ALLOWED/ + + @doc "The fifteen transcribed rule records, in ledger order (AP001–AP015)." + def rules, do: @rules + + @doc "One transcribed rule record by AP id or snake-case rule name, or `nil`." + def rule(id) when is_binary(id) do + Enum.find(@rules, fn record -> record.id == id or record.rule == id end) + end + + @doc """ + The canonical Elixir equivalent of a transcribed rule (AP id or + snake-case rule name), or `nil` for an unknown id. + """ + def canonical_equivalent(id) when is_binary(id) do + case rule(id) do + nil -> nil + record -> record.canonical + end + end + + @doc """ + AP001 — a parser crate whose sources state no input-size limit. + + `crate_type(parser)` is operationalised as a `Cargo.toml` that + describes the crate with parse/parser/parsing; the negative condition + keeps the Logtalk pattern verbatim (`MAX.*SIZE|size.*limit`, + case-insensitive) over every supplied file content. + """ + def check_parser_input_limits(contents) when is_map(contents) do + cargo = Map.get(contents, "Cargo.toml", "") + parser_crate? = Regex.match?(~r/pars(e|er|ing)/i, cargo) + + has_input_limit? = + contents + |> Map.values() + |> Enum.any?(fn content -> Regex.match?(~r/MAX.*SIZE|size.*limit/i, content) end) + + if cargo != "" and parser_crate? and not has_input_limit? do + [finding(rec("AP001"))] + else + [] + end + end + + @doc """ + AP002 — a WASM crate whose sources state no memory limit. + + `feature("wasm")` is operationalised as a `wasm` entry in the + `[features]` table, a `wasm-bindgen` dependency, or a `wasm32` + target mention in `Cargo.toml`; the negative condition keeps the + Logtalk pattern verbatim (`memory.*limit|max.*alloc`). + """ + def check_wasm_memory_limits(contents) when is_map(contents) do + cargo = Map.get(contents, "Cargo.toml", "") + + features = + case Regex.run(~r/\[features\](.*?)(\n\[|\z)/s, cargo) do + [_, body | _] -> body + _ -> "" + end + + wasm? = + Regex.match?(~r/\bwasm\b/, features) or + String.contains?(cargo, "wasm-bindgen") or + String.contains?(cargo, "wasm32") + + has_memory_limit? = + contents + |> Map.values() + |> Enum.any?(fn content -> Regex.match?(~r/memory.*limit|max.*alloc/i, content) end) + + if cargo != "" and wasm? and not has_memory_limit? do + [finding(rec("AP002"))] + else + [] + end + end + + @doc """ + AP003 — a Rust repo with no `cargo audit` in any supplied workflow. + `contents` is keyed by repo-relative path; only entries under + `.github/workflows/` count as workflow evidence. + """ + def check_missing_cargo_audit(files, contents) + when is_list(files) and is_map(contents) do + workflow_contents = + for {path, content} <- contents, + String.starts_with?(path, ".github/workflows/"), + do: content + + audited? = Enum.any?(workflow_contents, fn content -> String.contains?(content, "cargo audit") end) + + if "Cargo.toml" in files and not audited? do + [finding(rec("AP003"))] + else + [] + end + end + + @doc """ + AP004 — a Cargo workspace with a known-vulnerable member. + `any_member_has_vuln` is caller evidence (for example from + `Hypatia.Rules.DependabotAlerts`); this check contributes only the + `[workspace]` half of the conjunction. + """ + def check_workspace_vuln(cargo_toml, any_member_has_vuln) when is_binary(cargo_toml) do + if String.contains?(cargo_toml, "[workspace]") and any_member_has_vuln == true do + [finding(rec("AP004"))] + else + [] + end + end + + @doc """ + AP005 — source code with no test workflow. The Logtalk glob + (`.github/workflows/*test*.yml`) is transcribed semantically: the + `.yaml` spelling counts too. The ledger records the literal glob. + """ + def check_missing_ci_tests(files) when is_list(files) do + test_workflow? = + Enum.any?(files, fn path -> + Regex.match?(~r{\A\.github/workflows/[^/]*test[^/]*\.ya?ml\z}i, path) + end) + + has_source? = Enum.any?(files, fn path -> Path.extname(path) in @source_extensions end) + + if has_source? and not test_workflow? do + [finding(rec("AP005"))] + else + [] + end + end + + @doc """ + AP006 — a multi-language repo with no CodeQL workflow. The Logtalk + file test is transcribed semantically: `codeql.yaml` counts too. + """ + def check_missing_sast(files, language_count) when is_list(files) do + codeql? = + Enum.any?(files, fn path -> + path in [".github/workflows/codeql.yml", ".github/workflows/codeql.yaml"] + end) + + if is_integer(language_count) and language_count > 1 and not codeql? do + [finding(rec("AP006"))] + else + [] + end + end + + @doc """ + AP007 — dynamic property access from request input with no allowlist + nearby (same file). Both Logtalk access patterns must match and the + allowlist pattern (`allowedProps|whitelist|ALLOWED`) must not. + """ + def check_property_injection(content) when is_binary(content) do + if Regex.match?(@property_input_pattern, content) and + Regex.match?(@property_request_pattern, content) and + not Regex.match?(@property_allowlist_pattern, content) do + [Map.put(finding(rec("AP007")), :cwe, "CWE-915")] + else + [] + end + end + + @doc """ + AP009 — a cryptography-tagged repo whose required approving-review + count is below 2. `pr_reviews < 2` is operationalised as the branch + protection requirement, matching the audit prose ("Required reviews: + 2 (not 1)"); pair with `Hypatia.Rules.BranchProtection` BP003, which + enforces the general ≥1 floor. + """ + def check_crypto_enhanced_review(repo_tags, required_reviews) do + if cryptography_tagged?(repo_tags) and is_integer(required_reviews) and + required_reviews < 2 do + [finding(rec("AP009"))] + else + [] + end + end + + @doc "AP010 — a cryptography-tagged repo with no `fuzz/` tree." + def check_crypto_require_fuzzing(repo_tags, files) when is_list(files) do + fuzz? = Enum.any?(files, fn path -> String.starts_with?(path, "fuzz/") end) + + if cryptography_tagged?(repo_tags) and not fuzz? do + [finding(rec("AP010"))] + else + [] + end + end + + @doc "AP013 — a tooling-purpose repo scoring below 8 on Scorecard." + def check_exemplary_standards(repo_purpose, scorecard_score) do + if purpose_string(repo_purpose) == "tooling" and is_number(scorecard_score) and + scorecard_score < 8 do + [finding(rec("AP013"))] + else + [] + end + end + + @doc """ + Run every implemented check whose evidence the caller supplied. + + Recognised evidence keys: `:files` (repo-relative paths), `:contents` + (`%{path => content}`), `:repo_tags`, `:language_count`, + `:required_reviews`, `:any_member_has_vuln`, `:repo_purpose` and + `:scorecard_score`. Missing evidence yields no finding for the + dependent check — never an error, and never a fabricated pass claim: + findings are the only output. AP007 runs over supplied + `.js`/`.mjs`/`.cjs` contents. Rules whose canonical equivalent is a + live checker elsewhere (AP008, AP011, AP012, AP014, AP015) are not + re-run here. + """ + def check_all(evidence) when is_map(evidence) do + files = Map.get(evidence, :files, []) + contents = Map.get(evidence, :contents, %{}) + repo_tags = Map.get(evidence, :repo_tags, []) + + property_findings = + Enum.flat_map(contents, fn {path, content} -> + if javascript_file?(path) and is_binary(content) do + check_property_injection(content) + else + [] + end + end) + + check_parser_input_limits(contents) ++ + check_wasm_memory_limits(contents) ++ + check_missing_cargo_audit(files, contents) ++ + check_workspace_vuln( + Map.get(contents, "Cargo.toml", ""), + Map.get(evidence, :any_member_has_vuln, false) + ) ++ + check_missing_ci_tests(files) ++ + check_missing_sast(files, Map.get(evidence, :language_count, 0)) ++ + property_findings ++ + check_crypto_enhanced_review(repo_tags, Map.get(evidence, :required_reviews)) ++ + check_crypto_require_fuzzing(repo_tags, files) ++ + check_exemplary_standards( + Map.get(evidence, :repo_purpose), + Map.get(evidence, :scorecard_score) + ) + end + + defp rec(id), do: Enum.find(@rules, fn record -> record.id == id end) + + defp finding(record) do + %{ + rule: record.id, + type: record.rule, + effect: record.effect, + severity: action_severity(record.action), + action: record.action, + description: record.description, + source: record.origin + } + end + + defp action_severity("block_merge_with_escalation"), do: :critical + + defp action_severity(action) + when action in ["block_commit", "block_merge", "block_release"], + do: :high + + defp action_severity("warn_and_log"), do: :low + defp action_severity(_action), do: :medium + + defp cryptography_tagged?(tags) when is_list(tags) do + Enum.any?(tags, fn tag -> tag in [:cryptography, "cryptography"] end) + end + + defp cryptography_tagged?(_tags), do: false + + defp javascript_file?(path) when is_binary(path) do + Path.extname(path) in [".js", ".mjs", ".cjs"] + end + + defp javascript_file?(_path), do: false + + defp purpose_string(value) when is_binary(value), do: value + defp purpose_string(value) when is_atom(value), do: Atom.to_string(value) + defp purpose_string(_value), do: "" +end diff --git a/lib/rules/learning.ex b/lib/rules/learning.ex index 0ec759a9..bff5ee4a 100644 --- a/lib/rules/learning.ex +++ b/lib/rules/learning.ex @@ -2,8 +2,8 @@ defmodule Hypatia.Rules.Learning do @moduledoc """ - Learning engine rules absorbed from Logtalk engine/rules/learning.lgt - and engine/rules/rule_distiller.lgt. + Learning engine rules absorbed from the retired Logtalk learning and + rule-distiller modules (see docs/rules/logtalk-migration.adoc). Tracks fix outcomes, adjusts confidence, promotes patterns to rules, and manages cross-repo learning. diff --git a/lib/rules/rules.ex b/lib/rules/rules.ex index 66c793db..16576fec 100644 --- a/lib/rules/rules.ex +++ b/lib/rules/rules.ex @@ -6,14 +6,18 @@ defmodule Hypatia.Rules do This replaces the need for Logtalk rule evaluation by providing all policy rules, security checks, and learning operations directly - in Elixir. The Logtalk files in engine/ remain as documentation of - the original rule declarations. + in Elixir. The canonical active rule system is this directory + (`lib/rules/*.ex`); there is no `engine/` tree and no Logtalk output + format. The original Logtalk declarations are preserved — + clause-by-clause, with every divergence — in + `docs/rules/logtalk-migration.adoc`. ## Submodules - - `SecurityErrors` -- Error categories, SHA pins, secret detection, CodeQL, CWE mappings + - `SecurityErrors` -- Error categories, SHA pins, secret detection, CodeQL, CWE mappings, alert validation - `CicdRules` -- Repo requirements, commit blocking, waste detection, license validation - `CodeSafety` -- Language-specific dangerous pattern detection + - `AuditPrevention` -- AP001–AP015 audit-training prevention rules transcribed from Logtalk - `MigrationRules` -- ReScript v12→v13 migration, merge conflict resolution - `Learning` -- Fix outcome tracking, confidence, pattern promotion (GenServer) - `ForgeAdapters` -- Multi-forge operations with input validation diff --git a/lib/rules/security_errors.ex b/lib/rules/security_errors.ex index b522f35a..2b5ae751 100644 --- a/lib/rules/security_errors.ex +++ b/lib/rules/security_errors.ex @@ -87,6 +87,19 @@ defmodule Hypatia.Rules.SecurityErrors do # --------------------------------------------------------------------------- # Issue Severity Classification # --------------------------------------------------------------------------- + # + # Provenance: transcribed from ECHIDNA `rules/security_learning.lgt` + # `classify_severity/2` (explicit critical/high/medium membership lists + # plus a `low` catch-all), itself derived from + # `.audittraining/ERROR-CATALOG.scm`. The catch-all members are spelled + # out below as explicit `:low` entries (MaintainedID, FuzzingID, + # SASTID, CITestsID, CIIBestPracticesID, unmaintained, + # unused-local-variable) so they do not fall through to this module's + # `:info` unknown-id default; ERROR-CATALOG.scm grades + # fuzzing/sast/ci-tests `medium` instead — that upstream disagreement + # is recorded in docs/rules/logtalk-migration.adoc and deliberately + # not resolved here, because every executable consumer since the + # Logtalk module has used the `low` grading. @issue_severity %{ "hard-coded-cryptographic-value" => :critical, @@ -123,6 +136,9 @@ defmodule Hypatia.Rules.SecurityErrors do "unused-local-variable" => :low, "MaintainedID" => :low, "FuzzingID" => :low, + "SASTID" => :low, + "CITestsID" => :low, + "unmaintained" => :low, "CIIBestPracticesID" => :low, "deno-lint-include-pattern" => :low, "workflow-linter-self-detection" => :low, @@ -279,6 +295,122 @@ defmodule Hypatia.Rules.SecurityErrors do def prevention_workflow(issue_type), do: Map.get(@prevention_workflows, issue_type) + # --------------------------------------------------------------------------- + # Alert Categories + Alert Validation (ECHIDNA security_learning) + # --------------------------------------------------------------------------- + # + # Canonical alert-type -> category mapping and the composed + # `validate_alert/1` query. Faithfully transcribed 2026-11-01 from + # ECHIDNA `rules/security_learning.lgt`: + # + # * `alert_category/2` (18 facts) -> @alert_categories + # * `classify_severity/2` -> `issue_severity/1` (above) + # * `is_auto_fixable/1` (6 facts) -> @auto_fixable (above) + # * `suggest_fix/2` (13 facts) -> @fix_suggestions (above) + # * `get_prevention_workflow/2` -> @prevention_workflows (above) + # * `cicd_integration::validate_alert/2` -> `validate_alert/1` (below) + # + # The Logtalk module derived its facts from + # `.audittraining/ERROR-CATALOG.scm`; where the two disagree this + # module keeps the values every executable consumer has used since + # (the Logtalk facts / earlier Elixir transcription) and records the + # disagreement in the migration ledger rather than changing live + # behaviour as a side effect of transcription: + # + # * ERROR-CATALOG.scm splits the `:missing_tests` group into + # missing-fuzzing / missing-sast / missing-tests; the six-group + # form below is canonical because the Logtalk module and + # `Mix.Tasks.Hypatia.BatchSecurityScan` -- the two executable + # consumers -- both used it. + # * `BranchProtectionID` prevention was `branch-protection-enforcer.yml` + # in Logtalk; the Elixir mapping has used `scorecard-enforcer.yml` + # (jointly with SecurityPolicyID/CodeReviewID) since the first + # transcription and stays canonical. Both workflow templates + # still exist under `.audittraining/prevention/`. + # * `TokenPermissionsID` / `missing-workflow-permissions` fix text + # prescribed `permissions: read-all` in Logtalk. That advice is + # superseded ON PURPOSE: current OSSF guidance flags `read-all` + # itself, so the granular-permissions text in @fix_suggestions + # is canonical (see scorecard_compliance/token_permissions). + # + # Full clause-by-clause ledger: docs/rules/logtalk-migration.adoc. + + @alert_categories %{ + "TokenPermissionsID" => :workflow_security, + "PinnedDependenciesID" => :workflow_security, + "missing-workflow-permissions" => :workflow_security, + "hard-coded-cryptographic-value" => :code_security, + "remote-property-injection" => :code_security, + "sql-injection" => :code_security, + "unused-local-variable" => :code_quality, + "syntax-error" => :code_quality, + "VulnerabilitiesID" => :dependency_vuln, + "unmaintained" => :dependency_vuln, + "SecurityPolicyID" => :process_hygiene, + "MaintainedID" => :process_hygiene, + "CodeReviewID" => :process_hygiene, + "BranchProtectionID" => :process_hygiene, + "CIIBestPracticesID" => :process_hygiene, + "FuzzingID" => :missing_tests, + "SASTID" => :missing_tests, + "CITestsID" => :missing_tests + } + + @doc """ + All canonical alert-type -> category mappings (the transcribed + ECHIDNA `alert_category/2` facts). Categories are atoms in the + snake-case spelling the Logtalk module used; ERROR-CATALOG.scm's + kebab-case type names map to them by hyphen -> underscore. + """ + def alert_categories, do: @alert_categories + + @doc """ + Category for a GitHub code-scanning / Scorecard alert type, or `nil` + when the alert type has no transcribed `alert_category/2` fact. + """ + def alert_category(alert_type), do: Map.get(@alert_categories, alert_type) + + @doc """ + Validate an alert type against the learned security rules. + + Faithful transcription of ECHIDNA `cicd_integration::validate_alert/2`, + which composed `classify_severity/2`, `suggest_fix/2` and + `is_auto_fixable/1` into `alert_validation(Type, Severity, Fix, + AutoFix)`. The category and prevention-workflow lookups the Logtalk + caller performed separately are folded in, so this one map is the + complete replacement surface for `security_learning.lgt` consumers: + + %{ + alert_type: "TokenPermissionsID", + category: :workflow_security, + severity: :high, + fix: "Add granular workflow-level permissions ...", + auto_fixable: true, + prevention_workflow: "workflow-linter.yml" + } + + This is deliberately a total-function extension of the Logtalk query: + Logtalk `validate_alert/2` fails outright for an alert type with no + `suggest_fix/2` clause, whereas this returns the map with `fix: nil` + (and `category`/`prevention_workflow` `nil`, `auto_fixable` `false` + when those facts are absent too). One further documented difference: + the Logtalk severity catch-all returned `low` for wholly unknown + types, where `issue_severity/1`'s long-standing unknown-id default + is `:info`. Every alert type the Logtalk module knew is now an + explicit entry above, so the difference is reachable only for ids + neither system has seen. + """ + def validate_alert(alert_type) when is_binary(alert_type) do + %{ + alert_type: alert_type, + category: alert_category(alert_type), + severity: issue_severity(alert_type), + fix: fix_suggestion(alert_type), + auto_fixable: auto_fixable?(alert_type), + prevention_workflow: prevention_workflow(alert_type) + } + end + # --------------------------------------------------------------------------- # GitHub Action SHA Pins (canonical) # --------------------------------------------------------------------------- @@ -494,13 +626,20 @@ defmodule Hypatia.Rules.SecurityErrors do # estate policy refresh — migration target is AffineScript directly, # not through ReScript). affinescript ADDED. typescript replacement # corrected from "rescript" → "affinescript". + # + # Policy refresh 2026-11-01: logtalk REMOVED from allowed and added + # to banned (replacement: elixir). Logtalk appears nowhere in the + # estate LANGUAGE-POLICY allowlist; Hypatia's rule engine has been + # pure Elixir since ADR-001 (2026-04-14), and the estate carries no + # active `.lgt` sources. New Logtalk in a scanned repo is drift to + # migrate to `lib/rules/*.ex`-style Elixir, not an approved choice. + # See docs/rules/logtalk-migration.adoc. @allowed_languages MapSet.new([ "affinescript", "affine", "rust", "gleam", "julia", - "logtalk", "haskell", "bash", "nickel", @@ -520,7 +659,8 @@ defmodule Hypatia.Rules.SecurityErrors do "python" => "julia", "java" => "rust", "kotlin" => "rust", - "swift" => "tauri" + "swift" => "tauri", + "logtalk" => "elixir" } def language_allowed?(lang), do: MapSet.member?(@allowed_languages, String.downcase(lang)) @@ -545,6 +685,10 @@ defmodule Hypatia.Rules.SecurityErrors do "unwrap_without_check" => {"CWE-754", "Improper Check for Unusual Conditions"}, "getexn_on_external_data" => {"CWE-754", "Improper Check for Unusual Conditions"}, "sql_injection" => {"CWE-89", "SQL Injection"}, + "remote-property-injection" => + {"CWE-915", "Improperly Controlled Modification of Dynamically-Determined Object Attributes"}, + "remote_property_injection" => + {"CWE-915", "Improperly Controlled Modification of Dynamically-Determined Object Attributes"}, "stub_crypto" => {"CWE-327", "Use of Broken or Risky Cryptographic Algorithm"}, "js_eval" => {"CWE-94", "Improper Control of Code Generation"}, "elixir_code_eval" => {"CWE-94", "Improper Control of Code Generation"}, diff --git a/schemas/learned-security-rules.schema.json b/schemas/learned-security-rules.schema.json new file mode 100644 index 00000000..dc8fbd4b --- /dev/null +++ b/schemas/learned-security-rules.schema.json @@ -0,0 +1,81 @@ +{ + "$schema": "http://json-schema.org/draft-07/schema#", + "$id": "https://hyperpolymath.dev/schemas/hypatia/learned-security-rules", + "title": "Hypatia Learned Security Rules", + "description": "Named-field JSON replacement for two retired, mutually incompatible Logtalk security_rule/4 exports: Hypatia's generated (Type, Category, AutoFix, Count) and ECHIDNA's (Type, Category, Severity, AutoFix). Produced by `mix hypatia.batch_security_scan`; semantics are Hypatia.Rules.SecurityErrors.validate_alert/1 plus the observation count. See docs/rules/logtalk-migration.adoc for the field-by-field mapping.", + "type": "object", + "additionalProperties": false, + "required": ["schema", "version", "generated_at", "generator", "source_alert_count", "rules"], + "properties": { + "schema": { + "type": "string", + "const": "https://hyperpolymath.dev/schemas/hypatia/learned-security-rules", + "description": "Schema identifier for this document shape" + }, + "version": { + "type": "string", + "pattern": "^\\d+\\.\\d+\\.\\d+$", + "description": "Semantic version of the export format" + }, + "generated_at": { + "type": "string", + "format": "date-time", + "description": "UTC generation timestamp (second precision)" + }, + "generator": { + "type": "string", + "description": "Producing command" + }, + "source_alert_count": { + "type": "integer", + "minimum": 0, + "description": "Total code-scanning alerts the rules were learned from" + }, + "rules": { + "type": "array", + "items": { "$ref": "#/definitions/learnedRule" }, + "description": "One object per distinct alert type, sorted by observations descending then alert_type" + } + }, + "definitions": { + "learnedRule": { + "type": "object", + "additionalProperties": false, + "required": ["alert_type", "category", "severity", "auto_fixable", "observations", "fix", "prevention_workflow"], + "properties": { + "alert_type": { + "type": "string", + "minLength": 1, + "description": "GitHub code-scanning / Scorecard alert id (first positional field in both retired Logtalk exports)" + }, + "category": { + "type": "string", + "enum": ["workflow_security", "code_security", "code_quality", "dependency_vuln", "process_hygiene", "missing_tests", "unknown"], + "description": "Canonical alert category (second positional field in both retired exports; snake-case as in the retired ECHIDNA module). ERROR-CATALOG.scm kebab-case names map by hyphen to underscore." + }, + "severity": { + "type": "string", + "enum": ["critical", "high", "medium", "low", "info"], + "description": "Classified severity (ECHIDNA export field 3 / Logtalk classify_severity/2; absent from Hypatia's old generator. Canonical source SecurityErrors.issue_severity/1)" + }, + "auto_fixable": { + "type": "boolean", + "description": "Whether an automated fix exists (Hypatia generator field 3, ECHIDNA export field 4; Logtalk is_auto_fixable/1)" + }, + "observations": { + "type": "integer", + "minimum": 1, + "description": "Alerts of this type seen in the source scan (Hypatia generator field 4; absent from ECHIDNA's export). An observation count is belief-formation evidence, never a soundness claim: see schema/findings.ncl and src/Hypatia/ABI/Verdict.idr." + }, + "fix": { + "type": ["string", "null"], + "description": "Suggested fix text (Logtalk suggest_fix/2), or null when none is recorded" + }, + "prevention_workflow": { + "type": ["string", "null"], + "description": "Prevention workflow template name (Logtalk get_prevention_workflow/2), or null when none is recorded" + } + } + } + } +} diff --git a/scripts/check-no-active-logtalk.sh b/scripts/check-no-active-logtalk.sh new file mode 100755 index 00000000..7008a7fc --- /dev/null +++ b/scripts/check-no-active-logtalk.sh @@ -0,0 +1,190 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-no-active-logtalk.sh — keep Logtalk retired (ADR-001, 2026-04-14). +# +# Hypatia's canonical rule system is pure Elixir (lib/rules/*.ex); there +# is no Logtalk loader, rule format, or report format. This guard fails +# if an *active* Logtalk form re-enters the tracked tree: +# +# 1. a *.lgt / *.logtalk source file; +# 2. an embedded Logtalk source block or object directive, a +# logtalk_load/tester/doclet invocation; +# 3. a configuration setting requesting Logtalk (report-format / +# format / --format, A2ML or DEED spelling, loader/output paths +# ending in .lgt); +# 4. in executable/config files, a non-comment .lgt reference or a +# generated security_rule(...) fact. +# +# Historical *prose* about Logtalk is not banned; the ledger, dated +# audits, and provenance notes are records, not settings. Files that +# must quote an active-looking form to document its retirement are +# exempted by exact path in .logtalk-allowlist (shrink-only, each with +# a classification and removal condition). Comment-only lines are not +# settings and are ignored. +# +# Usage: scripts/check-no-active-logtalk.sh [--all] +# default: tracked files (git ls-files) +# --all: also untracked, non-ignored files (local pre-commit use) +# Exit: 0 clean; 1 = active Logtalk form or stale/malformed allowlist; +# 2 = usage / IO error. + +set -uo pipefail + +ROOT="$(git rev-parse --show-toplevel 2>/dev/null)" || { + echo "::error::check-no-active-logtalk: not inside a git repository" >&2 + exit 2 +} +cd "$ROOT" || exit 2 + +ALLOWLIST=".logtalk-allowlist" +SELF="scripts/check-no-active-logtalk.sh" + +mode="tracked" +case "${1:-}" in + "") ;; + --all) mode="all" ;; + *) echo "usage: $0 [--all]" >&2; exit 2 ;; +esac +if [ $# -gt 1 ]; then + echo "usage: $0 [--all]" >&2 + exit 2 +fi + +[ -f "$ALLOWLIST" ] || { + echo "::error::check-no-active-logtalk: $ALLOWLIST not found" >&2 + exit 2 +} + +# --------------------------------------------------------------------------- +# 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:]]*\(' + +is_comment_line() { + local trimmed + trimmed="$(printf '%s' "$1" | sed 's/^[[:space:]]*//')" + case "$trimmed" in + '#'*) return 0 ;; + ';'*) return 0 ;; + '//'*) return 0 ;; + '--'*) return 0 ;; + '%'*) return 0 ;; + esac + return 1 +} + +is_codegen_file() { + case "$1" in + *.ex|*.exs|*.sh|*.bash|*.yml|*.yaml|*.toml|*.json|*.ncl|*.a2ml|\ + *.deed|*.contractile|*.rs|*.py|*.js|*.ts|*.jl|*.hs|*.erl|*.gleam|\ + *.zig|*.idr|*.agda) return 0 ;; + esac + return 1 +} + +# has_candidate : raw (comment-inclusive) presence of a guarded +# form — used only to detect allowlist entries that have gone stale. +has_candidate() { + grep -IqiE -- "$active_re" "$1" 2>/dev/null && return 0 + if is_codegen_file "$1"; then + grep -IqiE -- "$codegen_re" "$1" 2>/dev/null && return 0 + fi + return 1 +} + +# --------------------------------------------------------------------------- +# Parse + validate the allowlist. +# --------------------------------------------------------------------------- +declare -A allowed=() +failures=0 +ln=0 +while IFS= read -r line || [ -n "$line" ]; do + ln=$((ln + 1)) + case "$line" in + ''|'#'*) continue ;; + esac + IFS='|' read -r path class removal extra <<<"$line" + path="$(printf '%s' "$path" | sed 's/^[[:space:]]*//;s/[[:space:]]*$//')" + class="$(printf '%s' "${class:-}" | sed 's/^[[:space:]]*//;s/[[:space:]]*$//')" + removal="$(printf '%s' "${removal:-}" | sed 's/^[[:space:]]*//;s/[[:space:]]*$//')" + if [ -n "${extra:-}" ] || [ -z "$path" ] || [ -z "$class" ] || [ -z "$removal" ]; then + echo "::error::$ALLOWLIST:$ln: expected ' | | '" + failures=$((failures + 1)); continue + fi + case "$path" in + *'*'*|*'?'*|*'['*|*']'*|'/'*|*'..'*|*'/') + echo "::error::$ALLOWLIST:$ln: '$path' is not an exact repository-relative file path (no wildcards, no directories)" + failures=$((failures + 1)); continue ;; + esac + if [ -n "${allowed[$path]:-}" ]; then + echo "::error::$ALLOWLIST:$ln: duplicate entry for '$path'" + failures=$((failures + 1)); continue + fi + allowed["$path"]=1 + if [ ! -f "$path" ]; then + echo "::error::$ALLOWLIST:$ln: allowlisted path no longer exists: $path (shrink the list)" + failures=$((failures + 1)); continue + fi + case "$path" in + *.lgt|*.logtalk) ;; + *) + if ! has_candidate "$path"; then + echo "::error::$ALLOWLIST:$ln: stale exemption — $path no longer contains a guarded form (shrink the list)" + failures=$((failures + 1)) + fi ;; + esac +done <"$ALLOWLIST" + +# --------------------------------------------------------------------------- +# Scan. +# --------------------------------------------------------------------------- +if [ "$mode" = "all" ]; then + mapfile -d '' files < <(git ls-files --cached --others --exclude-standard -z) +else + mapfile -d '' files < <(git ls-files -z) +fi + +checked=0 +for f in "${files[@]}"; do + [ -n "$f" ] || continue + [ -f "$f" ] || continue + checked=$((checked + 1)) + + lower="$(printf '%s' "$f" | tr '[:upper:]' '[:lower:]')" + case "$lower" in + *.lgt|*.logtalk) + if [ -z "${allowed[$f]:-}" ]; then + echo "::error::$f: active Logtalk source file (Hypatia rules are Elixir in lib/rules/*.ex; see docs/rules/logtalk-migration.adoc)" + failures=$((failures + 1)) + fi + continue ;; + esac + + [ "$f" = "$ALLOWLIST" ] && continue + [ -n "${allowed[$f]:-}" ] && continue + + patterns="$active_re" + if is_codegen_file "$f"; then + patterns="$active_re|$codegen_re" + fi + + while IFS= read -r hit; do + [ -n "$hit" ] || continue + lineno="${hit%%:*}" + text="${hit#*:}" + is_comment_line "$text" && continue + echo "::error::$f:$lineno: active Logtalk form (retired; canonical replacement is Elixir + JSON — see docs/rules/logtalk-migration.adoc)" + failures=$((failures + 1)) + done < <(grep -InE -- "$patterns" "$f" 2>/dev/null || true) +done + +echo "check-no-active-logtalk: files checked ${checked}, allowlisted ${#allowed[@]}, violations ${failures}" +if [ "$failures" -gt 0 ]; then + echo "check-no-active-logtalk: FAIL" + exit 1 +fi +echo "check-no-active-logtalk: OK — no active Logtalk forms outside the exact-path allowlist" +exit 0 diff --git a/test/rules/audit_prevention_test.exs b/test/rules/audit_prevention_test.exs new file mode 100644 index 00000000..594b0d9d --- /dev/null +++ b/test/rules/audit_prevention_test.exs @@ -0,0 +1,230 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +defmodule Hypatia.Rules.AuditPreventionTest do + use ExUnit.Case, async: true + + alias Hypatia.Rules.AuditPrevention + + describe "rules/0 — the transcription ledger as data" do + test "carries exactly AP001–AP015, in order, with origins" do + rules = AuditPrevention.rules() + ids = Enum.map(rules, & &1.id) + + assert ids == Enum.map(1..15, fn n -> "AP" <> String.pad_leading(Integer.to_string(n), 3, "0") end) + assert Enum.all?(rules, fn r -> String.starts_with?(r.origin, ".audittraining/security-errors/") end) + assert Enum.all?(rules, fn r -> r.description != "" and r.conditions != [] and r.canonical != "" end) + end + + test "rule/1 and canonical_equivalent/1 resolve by id and by name" do + assert AuditPrevention.rule("AP001").rule == "parser_input_limits" + assert AuditPrevention.rule("workflow_unpinned_action").id == "AP015" + assert AuditPrevention.rule("nope") == nil + assert AuditPrevention.canonical_equivalent("AP014") =~ "WorkflowAudit.check_permissions" + assert AuditPrevention.canonical_equivalent("nope") == nil + end + end + + describe "check_parser_input_limits/1 (AP001)" do + test "flags a parser crate with no stated input limit" do + contents = %{ + "Cargo.toml" => "[package]\nname = \"x\"\ndescription = \"A config file parser\"\n", + "src/lib.rs" => "pub fn parse(input: &str) {}\n" + } + + assert [finding] = AuditPrevention.check_parser_input_limits(contents) + assert finding.rule == "AP001" + assert finding.action == "warn_reviewer" + end + + test "does not flag a parser crate that states a limit" do + contents = %{ + "Cargo.toml" => "[package]\nname = \"x\"\ndescription = \"parser\"\n", + "src/lib.rs" => "const MAX_CONFIG_SIZE: usize = 1024;\n" + } + + assert AuditPrevention.check_parser_input_limits(contents) == [] + end + + test "does not flag a non-parser crate" do + contents = %{"Cargo.toml" => "[package]\nname = \"x\"\ndescription = \"A web server\"\n"} + assert AuditPrevention.check_parser_input_limits(contents) == [] + end + end + + describe "check_wasm_memory_limits/1 (AP002)" do + test "flags a wasm-featured crate with no memory limit" do + contents = %{ + "Cargo.toml" => "[package]\nname = \"x\"\n\n[features]\nwasm = []\n", + "src/lib.rs" => "pub fn run() {}\n" + } + + assert [finding] = AuditPrevention.check_wasm_memory_limits(contents) + assert finding.rule == "AP002" + end + + test "does not flag a wasm crate that states a memory limit" do + contents = %{ + "Cargo.toml" => "[dependencies]\nwasm-bindgen = \"0.2\"\n", + "src/lib.rs" => "// memory limit: 256 pages\n" + } + + assert AuditPrevention.check_wasm_memory_limits(contents) == [] + end + end + + describe "check_missing_cargo_audit/2 (AP003)" do + test "flags a Rust repo whose workflows never run cargo audit" do + files = ["Cargo.toml", ".github/workflows/ci.yml"] + contents = %{".github/workflows/ci.yml" => "run: cargo test\n"} + + assert [finding] = AuditPrevention.check_missing_cargo_audit(files, contents) + assert finding.rule == "AP003" + assert finding.severity == :high + end + + test "does not flag when a workflow runs cargo audit" do + files = ["Cargo.toml", ".github/workflows/audit.yml"] + contents = %{".github/workflows/audit.yml" => "run: cargo audit\n"} + + assert AuditPrevention.check_missing_cargo_audit(files, contents) == [] + end + + test "a cargo audit mention outside workflows is not CI evidence" do + files = ["Cargo.toml", "README.adoc"] + contents = %{"README.adoc" => "run cargo audit locally\n"} + + assert [%{rule: "AP003"}] = AuditPrevention.check_missing_cargo_audit(files, contents) + end + + test "does not flag non-Rust repos" do + assert AuditPrevention.check_missing_cargo_audit(["mix.exs"], %{}) == [] + end + end + + describe "check_workspace_vuln/2 (AP004)" do + test "flags a workspace with a vulnerable member" do + assert [%{rule: "AP004"}] = + AuditPrevention.check_workspace_vuln("[workspace]\nmembers = []\n", true) + end + + test "needs both halves of the conjunction" do + assert AuditPrevention.check_workspace_vuln("[workspace]\n", false) == [] + assert AuditPrevention.check_workspace_vuln("[package]\n", true) == [] + end + end + + describe "check_missing_ci_tests/1 (AP005)" do + test "flags source code with no test workflow" do + files = [".github/workflows/ci.yml", "src/main.rs"] + assert [%{rule: "AP005"}] = AuditPrevention.check_missing_ci_tests(files) + end + + test "accepts .yml and .yaml test workflows" do + assert AuditPrevention.check_missing_ci_tests([".github/workflows/test.yml", "src/main.rs"]) == [] + assert AuditPrevention.check_missing_ci_tests([".github/workflows/unit-tests.yaml", "lib/x.ex"]) == [] + end + + test "does not flag a repo with no source code" do + assert AuditPrevention.check_missing_ci_tests(["README.adoc", "docs/x.adoc"]) == [] + end + end + + describe "check_missing_sast/2 (AP006)" do + test "flags a multi-language repo with no CodeQL workflow" do + assert [%{rule: "AP006"}] = AuditPrevention.check_missing_sast(["src/main.rs"], 3) + end + + test "does not flag single-language repos or CodeQL carriers" do + assert AuditPrevention.check_missing_sast(["src/main.rs"], 1) == [] + + assert AuditPrevention.check_missing_sast( + [".github/workflows/codeql.yml", "src/main.rs"], + 3 + ) == [] + + assert AuditPrevention.check_missing_sast( + [".github/workflows/codeql.yaml", "src/main.rs"], + 3 + ) == [] + end + end + + describe "check_property_injection/1 (AP007)" do + test "flags request-driven dynamic access with no allowlist" do + content = "const v = obj[userInput]; const w = obj[req.body.key];\n" + assert [finding] = AuditPrevention.check_property_injection(content) + assert finding.rule == "AP007" + assert finding.cwe == "CWE-915" + assert finding.severity == :high + end + + test "an allowlist marker in the same file satisfies the negative condition" do + content = "const ALLOWED = new Set(['a']); const v = obj[userInput]; obj[req.query.k];\n" + assert AuditPrevention.check_property_injection(content) == [] + end + + test "one access pattern alone is not the conjunction" do + assert AuditPrevention.check_property_injection("const v = obj[userInput];\n") == [] + assert AuditPrevention.check_property_injection("const v = obj[req.params.id];\n") == [] + end + end + + describe "crypto checks (AP009, AP010)" do + test "flags fewer than two required reviewers on a cryptography repo" do + assert [%{rule: "AP009"}] = AuditPrevention.check_crypto_enhanced_review(["cryptography"], 1) + assert AuditPrevention.check_crypto_enhanced_review(["cryptography"], 2) == [] + assert AuditPrevention.check_crypto_enhanced_review(["web"], 1) == [] + assert AuditPrevention.check_crypto_enhanced_review(["cryptography"], nil) == [] + end + + test "flags a cryptography repo with no fuzz tree" do + assert [%{rule: "AP010"}] = + AuditPrevention.check_crypto_require_fuzzing([:cryptography], ["src/lib.rs"]) + + assert AuditPrevention.check_crypto_require_fuzzing( + ["cryptography"], + ["fuzz/fuzz_targets/x.rs"] + ) == [] + end + end + + describe "check_exemplary_standards/2 (AP013)" do + test "flags a tooling repo below the scorecard bar" do + assert [%{rule: "AP013"}] = AuditPrevention.check_exemplary_standards(:tooling, 7.5) + assert AuditPrevention.check_exemplary_standards("tooling", 8) == [] + assert AuditPrevention.check_exemplary_standards("library", 2) == [] + assert AuditPrevention.check_exemplary_standards(nil, nil) == [] + end + end + + describe "check_all/1" do + test "combines implemented checks and never duplicates canonical ones" do + evidence = %{ + files: ["Cargo.toml", "src/lib.rs"], + contents: %{ + "Cargo.toml" => "[package]\nname = \"proof-of-work\"\n", + "src/lib.rs" => "pub fn f() {}\n", + "web/app.js" => "obj[userInput]; obj[req.body.k];\n" + }, + repo_tags: ["cryptography"], + language_count: 1 + } + + ids = evidence |> AuditPrevention.check_all() |> Enum.map(& &1.rule) + + assert "AP003" in ids + assert "AP005" in ids + assert "AP007" in ids + assert "AP010" in ids + # AP014/AP015/AP011/AP012/AP008 live in their canonical modules. + refute "AP014" in ids + refute "AP015" in ids + refute "AP011" in ids + end + + test "empty evidence is silent, not an error" do + assert AuditPrevention.check_all(%{}) == [] + end + end +end diff --git a/test/security_errors_test.exs b/test/security_errors_test.exs index 9d8324d8..d829ef5d 100644 --- a/test/security_errors_test.exs +++ b/test/security_errors_test.exs @@ -105,4 +105,87 @@ defmodule Hypatia.Rules.SecurityErrorsTest do ) end end + + describe "ECHIDNA security_learning transcription" do + test "alert_categories/0 carries all 18 alert_category/2 facts" do + expected = %{ + "TokenPermissionsID" => :workflow_security, + "PinnedDependenciesID" => :workflow_security, + "missing-workflow-permissions" => :workflow_security, + "hard-coded-cryptographic-value" => :code_security, + "remote-property-injection" => :code_security, + "sql-injection" => :code_security, + "unused-local-variable" => :code_quality, + "syntax-error" => :code_quality, + "VulnerabilitiesID" => :dependency_vuln, + "unmaintained" => :dependency_vuln, + "SecurityPolicyID" => :process_hygiene, + "MaintainedID" => :process_hygiene, + "CodeReviewID" => :process_hygiene, + "BranchProtectionID" => :process_hygiene, + "CIIBestPracticesID" => :process_hygiene, + "FuzzingID" => :missing_tests, + "SASTID" => :missing_tests, + "CITestsID" => :missing_tests + } + + assert SecurityErrors.alert_categories() == expected + end + + test "alert_category/1 returns nil outside the transcribed facts" do + assert SecurityErrors.alert_category("TokenPermissionsID") == :workflow_security + assert SecurityErrors.alert_category("unused-import") == nil + end + + test "Logtalk severity catch-all members are explicit :low, not :info" do + for alert_type <- ["SASTID", "CITestsID", "unmaintained", "FuzzingID"] do + assert SecurityErrors.issue_severity(alert_type) == :low + end + end + + test "validate_alert/1 composes the transcribed predicates" do + validation = SecurityErrors.validate_alert("TokenPermissionsID") + + assert validation.alert_type == "TokenPermissionsID" + assert validation.category == :workflow_security + assert validation.severity == :high + assert validation.auto_fixable == true + assert validation.fix =~ "granular workflow-level permissions" + assert validation.prevention_workflow == "workflow-linter.yml" + end + + test "validate_alert/1 keeps the catch-all members complete" do + validation = SecurityErrors.validate_alert("SASTID") + + assert validation.category == :missing_tests + assert validation.severity == :low + assert validation.auto_fixable == false + assert validation.fix == nil + assert validation.prevention_workflow == nil + end + + test "validate_alert/1 on an unknown type mirrors the failure fields" do + validation = SecurityErrors.validate_alert("never-seen-alert") + + assert validation.category == nil + assert validation.severity == :info + assert validation.auto_fixable == false + assert validation.fix == nil + assert validation.prevention_workflow == nil + end + + test "remote property injection carries its exact CWE" do + assert {cwe, _title} = SecurityErrors.cwe_for("remote-property-injection") + assert cwe == "CWE-915" + end + end + + describe "language policy (2026-11-01 refresh)" do + test "logtalk is banned with Elixir as the replacement" do + refute SecurityErrors.language_allowed?("logtalk") + assert SecurityErrors.language_banned?("logtalk") + assert SecurityErrors.language_replacement("logtalk") == "elixir" + assert SecurityErrors.language_allowed?("elixir") + end + end end diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index 5eaeef37..ea95851c 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -27,12 +27,26 @@ neurosymbolic CI/CD platform. * Canonical estate policy: https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[Proof and Verification Policy]. This file is a proof inventory, not an independent alternative policy. - -NOTE: This repo currently verifies Idris2, Lean and TLA+ artefacts in CI. -It does not yet run an Agda + Rocq + Lean reconciliation pipeline. -The pre-existing Lean files below retain their documented scope; they -must not be represented as independently rechecking Agda proofs until -the checked Agda source and correspondence evidence actually exist. +* Proof *grades* follow hyperpolymath/mathesis, + `+estate-mathematical-architecture+` §§5–6: *Grade 3* is an Agda proof + formulated and type-checking under the strict profile; *Grade 2* + requires translation(s) into independent foundational system(s); + *Grade 1* additionally requires those translated witnesses to compile + in headless, isolated CI via verified checker APIs. A target grade is + not a status. This inventory records exact statuses (Open / Claimed / + `+AGDA-PENDING+` / `+AGDA-VERIFIED+` / Grade 3 …) and never flattens + them into a confidence percentage. +* A checked model proves its stated proposition only. In particular it + does not prove runtime refinement of Elixir/BEAM code; such claims + need their own correspondence evidence and tests. + +NOTE: This repo verifies Idris2, Lean and TLA+ artefacts in CI, and — +since 2026-11-01 — carries one narrowly scoped Agda artefact +(`+LogtalkMigration.agda+`, below) gated by the same workflow. It does +not yet run an Agda + Rocq + Lean reconciliation pipeline. The +pre-existing Lean files below retain their documented scope; they must +not be represented as independently rechecking Agda proofs until +checked Agda sources and correspondence evidence actually exist. === Proof Inventory @@ -92,11 +106,14 @@ annealing clamp bounds, nascent-never-auto, veteran-unrestricted |COMPLETE |`+verification/proofs/idris2/VerisimdbConnector.idr+` |Idris2 -|Completeness (mandatory fields), Soundness (no "`unknown`" fallbacks), -Preservation (transit to Logtalk facts — the retired engine's fact -format; the proof covers the connector's preservation property as -specified; status retained unchanged when the engine was retired -2026-03-06) |COMPLETE +|Completeness (mandatory fields), Soundness (missing fields rejected), +Preservation of repo/file/category/severity under projection to the +canonical JSON finding record (`+FindingFact+`). *Statement superseded +2026-11-01:* the 2026-04-04 target was the retired Logtalk fact format +(`+LogtalkFact+`); the equality proof term is unchanged, the target is +now `+FindingFact+`, and the corresponding module is +`+lib/verisim_connector.ex+`. Runtime refinement is not claimed. +|COMPLETE (superseded statement; re-checked 2026-11-01 in Verify Proofs run 41328302925, idris2 --check job 124912804086, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331) |`+verification/proofs/idris2/Quarantine.idr+` |Idris2 |State transitions (ok/soft/hard/permanent), Auto-quarantine triggers, Release @@ -148,6 +165,38 @@ downgraded to a runtime assertion in JSONL for violations. See commit history. |=== +==== Logtalk → Elixir migration correspondence (2026-11-01) + +Finite, implementation-independent table correspondence for the retired +ECHIDNA `+security_learning.lgt+` alert semantics versus +`+Hypatia.Rules.SecurityErrors+`. Per the estate verifier mapping this +is Agda territory; per Mathesis this is now *Grade 3* on the +strict-profile receipt recorded in the row below (checker version, +library discipline, exact invocation, result, source digest, and +verification commit). Fix *strings* and Elixir +runtime behaviour are outside the model and are pinned by the migration +ledger and ExUnit tests respectively. + +[width="100%",cols="28%,14%,42%,16%",options="header",] +|=== +|File |Language |Properties stated |Status +|`+verification/proofs/agda/LogtalkMigration.agda+` |Agda +|Exhaustive agreement over the 18 transcribed alert types: +`+categoriesAgree+`, `+severitiesAgree+`, `+autoFixableAgrees+`, +`+fixPresenceAgrees+`; prevention agreement on the six unchanged shared +entries; the two ledgered non-equalities stated exactly +(`+preventionBranchSource+`, `+preventionBranchTarget+`, +`+preventionCodeReviewSource+`, `+preventionCodeReviewTarget+`); the +former severity catch-all members explicit (`+catchAllSastLow+`, +`+catchAllCiTestsLow+`, `+catchAllUnmaintainedLow+`). Source SHA-256 +(at authoring): bbd18e2747c84e2eda7ff5a778a2df7f8960a1ef47b1c253f316b9d97b9902a0. +|Grade 3 — AGDA-VERIFIED. Receipt: official pinned Agda 2.8.0.2 Linux +release, builtins only/no stdlib; invocation `agda --safe --without-K +--cubical-compatible LogtalkMigration.agda`; success in Verify Proofs +run 41328302925, job 124912804344, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331. No Grade 2/1, +reconciliation, or runtime-refinement claim. +|=== + ==== Verdict support (2026-10-14, HYP-01) A gate verdict names its support: a pattern match, an observation count, or @@ -291,10 +340,11 @@ internal types * *P4.2* Soundness: ill-formed data (missing fields) is rejected as `+Nothing+` * *P4.3* Severity Parsing: total mapping for all valid severity levels -* *P4.4* Data Preservation: conversion to Logtalk facts preserves repo, -file, category, and severity (Logtalk fact format = the retired engine's; -proof status unchanged by the 2026-03-06 retirement — recorded here so the -claim is not silently rewritten) +* *P4.4* Data Preservation: projection to the canonical finding record +(`+FindingFact+`, via `+toFact+`) preserves repo, file, category, and +severity (`+factPreservesData+`). Superseded 2026-11-01 from the retired +Logtalk-fact target; the proof term is unchanged, the statement's target +is the JSON finding record, and no runtime-refinement claim is made. ==== 5. Quarantine Logic (`+Quarantine.idr+`) @@ -326,6 +376,28 @@ list) rejected * *P7.6* Count bounded after any sequence of accepts +==== 8. Logtalk Migration Correspondence (`+LogtalkMigration.agda+`) + +Status for all of P8: *Grade 3 — AGDA-VERIFIED* on the strict-profile +receipt in the inventory row above (Agda 2.8.0.2, Verify Proofs run +41328302925, job 124912804344, commit 4018290eaa3265b82209e2a45b6917a4bb0a0331). This grades the finite +model only. + +* *P8.1* Category correspondence: `+categoriesAgree+` +* *P8.2* Severity correspondence, including the former catch-all: + `+severitiesAgree+`, `+catchAllSastLow+`, `+catchAllCiTestsLow+`, + `+catchAllUnmaintainedLow+` +* *P8.3* Auto-fixability correspondence: `+autoFixableAgrees+` +* *P8.4* Fix-presence (domain) correspondence: `+fixPresenceAgrees+` +* *P8.5* Prevention agreement where the target did not deliberately + change it: `+preventionAgreesToken+`, `+preventionAgreesPinned+`, + `+preventionAgreesMissing+`, `+preventionAgreesHardCoded+`, + `+preventionAgreesVulnerabilities+`, + `+preventionAgreesSecurityPolicy+` +* *P8.6* The ledgered prevention non-equalities, exactly: + `+preventionBranchSource+`, `+preventionBranchTarget+`, + `+preventionCodeReviewSource+`, `+preventionCodeReviewTarget+` + === Dangerous Pattern Audit [cols=",,",options="header",] @@ -372,7 +444,12 @@ rejected |Batch rollback |`+BatchRollback.idr+` |Full -|VeriSimDB connector |`+VerisimdbConnector.idr+` |Full +|VeriSimDB connector |`+VerisimdbConnector.idr+` |Full (model; statement +superseded 2026-11-01) + +|Logtalk → Elixir alert-table correspondence +|`+LogtalkMigration.agda+` |Finite model only — Grade 3 / +AGDA-VERIFIED (receipt above); fix text and runtime refinement excluded |Neural ensemble aggregation |`+NeuralConsensus.idr+` |Full (bounds + min-lower-bound) @@ -396,7 +473,7 @@ that adding a proof does not require editing a third hand-maintained list. hypatia/ ├── src/Hypatia/ABI/ # Idris2 ABI definitions + proofs (normative wire contract) ├── verify/src/ # Pipeline state machine proofs -└── verification/proofs/ # Standalone property proofs (idris2/, lean4/, tlaplus/) +└── verification/proofs/ # Standalone property proofs (idris2/, lean4/, tlaplus/, agda/) .... === Retired proofs @@ -407,5 +484,8 @@ property — JSONL outcome log timestamps strictly increasing — is trivial enough that a runtime assertion does the job. It now lives in `+lib/outcome_tracker.ex+` (`+assert_h6_monotone/2+`) and echidnabot audits the logs for any violation. Removing Agda also removes a theorem -prover from the toolchain: Hypatia now uses Idris2 (compile-time types), -Lean 4 (universal invariants), and TLA+ (model-checked concurrency). +prover from the toolchain: at retirement Hypatia used Idris2 +(compile-time types), Lean 4 (universal invariants), and TLA+ +(model-checked concurrency). The 2026-11-01 migration correspondence +reintroduces exactly one narrowly scoped Agda artefact +(`+LogtalkMigration.agda+`); it does not revive this retired proof. diff --git a/verification/README.adoc b/verification/README.adoc index 4cfa6e66..6cb675c1 100644 --- a/verification/README.adoc +++ b/verification/README.adoc @@ -1,13 +1,16 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 = verification/ — Formal Proofs -Idris2, Lean 4 and TLA+ proof sources for Hypatia's type-level guarantees. +Idris2, Lean 4, TLA+ and Agda proof sources for Hypatia's type-level guarantees. == Contents * `proofs/idris2/` — Idris2 proof files (`.idr`) asserting invariants over the normative ABI in `src/Hypatia/ABI/` * `proofs/lean4/`, `proofs/tlaplus/` — Lean 4 and TLA+ proofs +* `proofs/agda/` — Agda correspondence model for the Logtalk → Elixir + rule migration (`LogtalkMigration.agda`; Mathesis Grade 3 receipt in + `PROOF-STATUS.adoc`) * `PROOF-STATUS.adoc` — Current proof completion status == Building Proofs @@ -21,6 +24,15 @@ cd verification/proofs/idris2 for f in *.idr; do idris2 --check "$f"; done ---- +The Agda artefact is checked under the estate strict profile (capital +K). A missing `agda` binary is an open proof obligation, never a skip: + +[source,bash] +---- +cd verification/proofs/agda +agda --safe --without-K --cubical-compatible LogtalkMigration.agda +---- + The Idris2 *packages* in the repository are built separately: [source,bash] diff --git a/verification/proofs/agda/LogtalkMigration.agda b/verification/proofs/agda/LogtalkMigration.agda new file mode 100644 index 00000000..e06f803f --- /dev/null +++ b/verification/proofs/agda/LogtalkMigration.agda @@ -0,0 +1,436 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Finite correspondence model for the Logtalk -> Elixir security-rule +-- migration (ECHIDNA rules/security_learning.lgt -> +-- Hypatia.Rules.SecurityErrors). +-- +-- Scope, deliberately narrow (estate PROOF-POLICY: a checked model is not +-- a runtime-refinement proof): +-- +-- * The source functions transcribe the 18 alert_category/2 facts, the +-- classify_severity/2 clauses (including the final low catch-all), +-- the six is_auto_fixable/1 facts, the domain of suggest_fix/2, and +-- get_prevention_workflow/2 from security_learning.lgt. +-- * The target functions transcribe the corresponding Elixir tables in +-- lib/rules/security_errors.ex over the same 18 alert types. +-- * The theorems check exhaustive agreement for category, severity, +-- auto-fixability, and fix presence. Prevention agrees on the six +-- shared, unchanged entries; the BranchProtectionID supersession and +-- the CodeReviewID extension are stated as separate lemmas rather +-- than hidden inside a false universal equality. +-- * Fix *text* is not modelled here: 10 of 13 strings are verbatim and +-- the other three are ledgered supersessions/generalisation in +-- docs/rules/logtalk-migration.adoc. Elixir runtime behaviour is +-- pinned by ExUnit tests, not by this file. +-- +-- Intended Mathesis grade: Grade 3 target. It becomes Grade 3 only when +-- the strict command in verification/PROOF-STATUS.adoc has a recorded +-- successful receipt; until then its status is AGDA-PENDING. +-- No postulates, no unsafe options, no standard-library dependency. + +module LogtalkMigration where + +open import Agda.Builtin.Bool +open import Agda.Builtin.Equality + +------------------------------------------------------------------------ +-- Finite domains +------------------------------------------------------------------------ + +data Alert : Set where + tokenPermissions : Alert + pinnedDependencies : Alert + missingWorkflowPerms : Alert + hardCodedCrypto : Alert + remotePropertyInjection : Alert + sqlInjection : Alert + unusedLocalVariable : Alert + syntaxError : Alert + vulnerabilities : Alert + unmaintained : Alert + securityPolicy : Alert + maintained : Alert + codeReview : Alert + branchProtection : Alert + ciiBestPractices : Alert + fuzzing : Alert + sast : Alert + ciTests : Alert + +data Category : Set where + workflowSecurity : Category + codeSecurity : Category + codeQuality : Category + dependencyVuln : Category + processHygiene : Category + missingTests : Category + +data Severity : Set where + critical : Severity + high : Severity + medium : Severity + low : Severity + +data Workflow : Set where + workflowLinter : Workflow + secretScanner : Workflow + cargoAudit : Workflow + scorecardEnforcer : Workflow + branchProtectionEnforcer : Workflow + +data Maybe (A : Set) : Set where + nothing : Maybe A + just : A -> Maybe A + +------------------------------------------------------------------------ +-- Source: ECHIDNA security_learning.lgt +------------------------------------------------------------------------ + +logtalkCategory : Alert -> Category +logtalkCategory tokenPermissions = workflowSecurity +logtalkCategory pinnedDependencies = workflowSecurity +logtalkCategory missingWorkflowPerms = workflowSecurity +logtalkCategory hardCodedCrypto = codeSecurity +logtalkCategory remotePropertyInjection = codeSecurity +logtalkCategory sqlInjection = codeSecurity +logtalkCategory unusedLocalVariable = codeQuality +logtalkCategory syntaxError = codeQuality +logtalkCategory vulnerabilities = dependencyVuln +logtalkCategory unmaintained = dependencyVuln +logtalkCategory securityPolicy = processHygiene +logtalkCategory maintained = processHygiene +logtalkCategory codeReview = processHygiene +logtalkCategory branchProtection = processHygiene +logtalkCategory ciiBestPractices = processHygiene +logtalkCategory fuzzing = missingTests +logtalkCategory sast = missingTests +logtalkCategory ciTests = missingTests + +-- The final Logtalk clause is classify_severity(_, low), so every alert +-- outside the critical/high/medium member lists is low here. +logtalkSeverity : Alert -> Severity +logtalkSeverity tokenPermissions = high +logtalkSeverity pinnedDependencies = medium +logtalkSeverity missingWorkflowPerms = high +logtalkSeverity hardCodedCrypto = critical +logtalkSeverity remotePropertyInjection = high +logtalkSeverity sqlInjection = critical +logtalkSeverity unusedLocalVariable = low +logtalkSeverity syntaxError = medium +logtalkSeverity vulnerabilities = critical +logtalkSeverity unmaintained = low +logtalkSeverity securityPolicy = medium +logtalkSeverity maintained = low +logtalkSeverity codeReview = medium +logtalkSeverity branchProtection = medium +logtalkSeverity ciiBestPractices = low +logtalkSeverity fuzzing = low +logtalkSeverity sast = low +logtalkSeverity ciTests = low + +logtalkAutoFixable : Alert -> Bool +logtalkAutoFixable tokenPermissions = true +logtalkAutoFixable pinnedDependencies = true +logtalkAutoFixable missingWorkflowPerms = true +logtalkAutoFixable hardCodedCrypto = false +logtalkAutoFixable remotePropertyInjection = false +logtalkAutoFixable sqlInjection = false +logtalkAutoFixable unusedLocalVariable = true +logtalkAutoFixable syntaxError = false +logtalkAutoFixable vulnerabilities = false +logtalkAutoFixable unmaintained = false +logtalkAutoFixable securityPolicy = true +logtalkAutoFixable maintained = false +logtalkAutoFixable codeReview = false +logtalkAutoFixable branchProtection = true +logtalkAutoFixable ciiBestPractices = false +logtalkAutoFixable fuzzing = false +logtalkAutoFixable sast = false +logtalkAutoFixable ciTests = false + +-- Domain of suggest_fix/2 only (13 facts); the strings themselves are +-- handled by the migration ledger and Elixir tests. +logtalkHasFix : Alert -> Bool +logtalkHasFix tokenPermissions = true +logtalkHasFix pinnedDependencies = true +logtalkHasFix missingWorkflowPerms = true +logtalkHasFix hardCodedCrypto = true +logtalkHasFix remotePropertyInjection = true +logtalkHasFix sqlInjection = false +logtalkHasFix unusedLocalVariable = true +logtalkHasFix syntaxError = true +logtalkHasFix vulnerabilities = true +logtalkHasFix unmaintained = false +logtalkHasFix securityPolicy = true +logtalkHasFix maintained = false +logtalkHasFix codeReview = true +logtalkHasFix branchProtection = true +logtalkHasFix ciiBestPractices = true +logtalkHasFix fuzzing = true +logtalkHasFix sast = false +logtalkHasFix ciTests = false + +logtalkPrevention : Alert -> Maybe Workflow +logtalkPrevention tokenPermissions = just workflowLinter +logtalkPrevention pinnedDependencies = just workflowLinter +logtalkPrevention missingWorkflowPerms = just workflowLinter +logtalkPrevention hardCodedCrypto = just secretScanner +logtalkPrevention remotePropertyInjection = nothing +logtalkPrevention sqlInjection = nothing +logtalkPrevention unusedLocalVariable = nothing +logtalkPrevention syntaxError = nothing +logtalkPrevention vulnerabilities = just cargoAudit +logtalkPrevention unmaintained = nothing +logtalkPrevention securityPolicy = just scorecardEnforcer +logtalkPrevention maintained = nothing +logtalkPrevention codeReview = nothing +logtalkPrevention branchProtection = just branchProtectionEnforcer +logtalkPrevention ciiBestPractices = nothing +logtalkPrevention fuzzing = nothing +logtalkPrevention sast = nothing +logtalkPrevention ciTests = nothing + +------------------------------------------------------------------------ +-- Target: Hypatia.Rules.SecurityErrors (same 18 alert types) +------------------------------------------------------------------------ + +elixirCategory : Alert -> Category +elixirCategory tokenPermissions = workflowSecurity +elixirCategory pinnedDependencies = workflowSecurity +elixirCategory missingWorkflowPerms = workflowSecurity +elixirCategory hardCodedCrypto = codeSecurity +elixirCategory remotePropertyInjection = codeSecurity +elixirCategory sqlInjection = codeSecurity +elixirCategory unusedLocalVariable = codeQuality +elixirCategory syntaxError = codeQuality +elixirCategory vulnerabilities = dependencyVuln +elixirCategory unmaintained = dependencyVuln +elixirCategory securityPolicy = processHygiene +elixirCategory maintained = processHygiene +elixirCategory codeReview = processHygiene +elixirCategory branchProtection = processHygiene +elixirCategory ciiBestPractices = processHygiene +elixirCategory fuzzing = missingTests +elixirCategory sast = missingTests +elixirCategory ciTests = missingTests + +elixirSeverity : Alert -> Severity +elixirSeverity tokenPermissions = high +elixirSeverity pinnedDependencies = medium +elixirSeverity missingWorkflowPerms = high +elixirSeverity hardCodedCrypto = critical +elixirSeverity remotePropertyInjection = high +elixirSeverity sqlInjection = critical +elixirSeverity unusedLocalVariable = low +elixirSeverity syntaxError = medium +elixirSeverity vulnerabilities = critical +elixirSeverity unmaintained = low +elixirSeverity securityPolicy = medium +elixirSeverity maintained = low +elixirSeverity codeReview = medium +elixirSeverity branchProtection = medium +elixirSeverity ciiBestPractices = low +elixirSeverity fuzzing = low +elixirSeverity sast = low +elixirSeverity ciTests = low + +elixirAutoFixable : Alert -> Bool +elixirAutoFixable tokenPermissions = true +elixirAutoFixable pinnedDependencies = true +elixirAutoFixable missingWorkflowPerms = true +elixirAutoFixable hardCodedCrypto = false +elixirAutoFixable remotePropertyInjection = false +elixirAutoFixable sqlInjection = false +elixirAutoFixable unusedLocalVariable = true +elixirAutoFixable syntaxError = false +elixirAutoFixable vulnerabilities = false +elixirAutoFixable unmaintained = false +elixirAutoFixable securityPolicy = true +elixirAutoFixable maintained = false +elixirAutoFixable codeReview = false +elixirAutoFixable branchProtection = true +elixirAutoFixable ciiBestPractices = false +elixirAutoFixable fuzzing = false +elixirAutoFixable sast = false +elixirAutoFixable ciTests = false + +elixirHasFix : Alert -> Bool +elixirHasFix tokenPermissions = true +elixirHasFix pinnedDependencies = true +elixirHasFix missingWorkflowPerms = true +elixirHasFix hardCodedCrypto = true +elixirHasFix remotePropertyInjection = true +elixirHasFix sqlInjection = false +elixirHasFix unusedLocalVariable = true +elixirHasFix syntaxError = true +elixirHasFix vulnerabilities = true +elixirHasFix unmaintained = false +elixirHasFix securityPolicy = true +elixirHasFix maintained = false +elixirHasFix codeReview = true +elixirHasFix branchProtection = true +elixirHasFix ciiBestPractices = true +elixirHasFix fuzzing = true +elixirHasFix sast = false +elixirHasFix ciTests = false + +elixirPrevention : Alert -> Maybe Workflow +elixirPrevention tokenPermissions = just workflowLinter +elixirPrevention pinnedDependencies = just workflowLinter +elixirPrevention missingWorkflowPerms = just workflowLinter +elixirPrevention hardCodedCrypto = just secretScanner +elixirPrevention remotePropertyInjection = nothing +elixirPrevention sqlInjection = nothing +elixirPrevention unusedLocalVariable = nothing +elixirPrevention syntaxError = nothing +elixirPrevention vulnerabilities = just cargoAudit +elixirPrevention unmaintained = nothing +elixirPrevention securityPolicy = just scorecardEnforcer +elixirPrevention maintained = nothing +elixirPrevention codeReview = just scorecardEnforcer +elixirPrevention branchProtection = just scorecardEnforcer +elixirPrevention ciiBestPractices = nothing +elixirPrevention fuzzing = nothing +elixirPrevention sast = nothing +elixirPrevention ciTests = nothing + +------------------------------------------------------------------------ +-- Correspondence theorems (exhaustive over the finite Alert type) +------------------------------------------------------------------------ + +categoriesAgree : (a : Alert) -> logtalkCategory a ≡ elixirCategory a +categoriesAgree tokenPermissions = refl +categoriesAgree pinnedDependencies = refl +categoriesAgree missingWorkflowPerms = refl +categoriesAgree hardCodedCrypto = refl +categoriesAgree remotePropertyInjection = refl +categoriesAgree sqlInjection = refl +categoriesAgree unusedLocalVariable = refl +categoriesAgree syntaxError = refl +categoriesAgree vulnerabilities = refl +categoriesAgree unmaintained = refl +categoriesAgree securityPolicy = refl +categoriesAgree maintained = refl +categoriesAgree codeReview = refl +categoriesAgree branchProtection = refl +categoriesAgree ciiBestPractices = refl +categoriesAgree fuzzing = refl +categoriesAgree sast = refl +categoriesAgree ciTests = refl + +severitiesAgree : (a : Alert) -> logtalkSeverity a ≡ elixirSeverity a +severitiesAgree tokenPermissions = refl +severitiesAgree pinnedDependencies = refl +severitiesAgree missingWorkflowPerms = refl +severitiesAgree hardCodedCrypto = refl +severitiesAgree remotePropertyInjection = refl +severitiesAgree sqlInjection = refl +severitiesAgree unusedLocalVariable = refl +severitiesAgree syntaxError = refl +severitiesAgree vulnerabilities = refl +severitiesAgree unmaintained = refl +severitiesAgree securityPolicy = refl +severitiesAgree maintained = refl +severitiesAgree codeReview = refl +severitiesAgree branchProtection = refl +severitiesAgree ciiBestPractices = refl +severitiesAgree fuzzing = refl +severitiesAgree sast = refl +severitiesAgree ciTests = refl + +autoFixableAgrees : (a : Alert) -> logtalkAutoFixable a ≡ elixirAutoFixable a +autoFixableAgrees tokenPermissions = refl +autoFixableAgrees pinnedDependencies = refl +autoFixableAgrees missingWorkflowPerms = refl +autoFixableAgrees hardCodedCrypto = refl +autoFixableAgrees remotePropertyInjection = refl +autoFixableAgrees sqlInjection = refl +autoFixableAgrees unusedLocalVariable = refl +autoFixableAgrees syntaxError = refl +autoFixableAgrees vulnerabilities = refl +autoFixableAgrees unmaintained = refl +autoFixableAgrees securityPolicy = refl +autoFixableAgrees maintained = refl +autoFixableAgrees codeReview = refl +autoFixableAgrees branchProtection = refl +autoFixableAgrees ciiBestPractices = refl +autoFixableAgrees fuzzing = refl +autoFixableAgrees sast = refl +autoFixableAgrees ciTests = refl + +fixPresenceAgrees : (a : Alert) -> logtalkHasFix a ≡ elixirHasFix a +fixPresenceAgrees tokenPermissions = refl +fixPresenceAgrees pinnedDependencies = refl +fixPresenceAgrees missingWorkflowPerms = refl +fixPresenceAgrees hardCodedCrypto = refl +fixPresenceAgrees remotePropertyInjection = refl +fixPresenceAgrees sqlInjection = refl +fixPresenceAgrees unusedLocalVariable = refl +fixPresenceAgrees syntaxError = refl +fixPresenceAgrees vulnerabilities = refl +fixPresenceAgrees unmaintained = refl +fixPresenceAgrees securityPolicy = refl +fixPresenceAgrees maintained = refl +fixPresenceAgrees codeReview = refl +fixPresenceAgrees branchProtection = refl +fixPresenceAgrees ciiBestPractices = refl +fixPresenceAgrees fuzzing = refl +fixPresenceAgrees sast = refl +fixPresenceAgrees ciTests = refl + +-- Prevention: agreement on the six unchanged shared entries. +preventionAgreesToken : + logtalkPrevention tokenPermissions ≡ elixirPrevention tokenPermissions +preventionAgreesToken = refl + +preventionAgreesPinned : + logtalkPrevention pinnedDependencies ≡ elixirPrevention pinnedDependencies +preventionAgreesPinned = refl + +preventionAgreesMissing : + logtalkPrevention missingWorkflowPerms ≡ elixirPrevention missingWorkflowPerms +preventionAgreesMissing = refl + +preventionAgreesHardCoded : + logtalkPrevention hardCodedCrypto ≡ elixirPrevention hardCodedCrypto +preventionAgreesHardCoded = refl + +preventionAgreesVulnerabilities : + logtalkPrevention vulnerabilities ≡ elixirPrevention vulnerabilities +preventionAgreesVulnerabilities = refl + +preventionAgreesSecurityPolicy : + logtalkPrevention securityPolicy ≡ elixirPrevention securityPolicy +preventionAgreesSecurityPolicy = refl + +-- Prevention: the two ledgered non-equalities, stated exactly. +preventionBranchSource : + logtalkPrevention branchProtection ≡ just branchProtectionEnforcer +preventionBranchSource = refl + +preventionBranchTarget : + elixirPrevention branchProtection ≡ just scorecardEnforcer +preventionBranchTarget = refl + +preventionCodeReviewSource : + logtalkPrevention codeReview ≡ nothing +preventionCodeReviewSource = refl + +preventionCodeReviewTarget : + elixirPrevention codeReview ≡ just scorecardEnforcer +preventionCodeReviewTarget = refl + +-- The three alerts that reached low only through the Logtalk catch-all +-- are explicit low entries in Elixir. (Also covered by +-- severitiesAgree; named here because this was the one place where a +-- fact-by-fact transcription would have changed behaviour to :info.) +catchAllSastLow : elixirSeverity sast ≡ low +catchAllSastLow = refl + +catchAllCiTestsLow : elixirSeverity ciTests ≡ low +catchAllCiTestsLow = refl + +catchAllUnmaintainedLow : elixirSeverity unmaintained ≡ low +catchAllUnmaintainedLow = refl diff --git a/verification/proofs/idris2/VerisimdbConnector.idr b/verification/proofs/idris2/VerisimdbConnector.idr index 1732dae5..a9c08fa0 100644 --- a/verification/proofs/idris2/VerisimdbConnector.idr +++ b/verification/proofs/idris2/VerisimdbConnector.idr @@ -6,9 +6,15 @@ -- Formal verification of the VeriSimDB connector data integrity: -- 1. Completeness: all mandatory fields in the DB map to the ABI types -- 2. Soundness: ill-formed data is rejected (no "unknown" fallbacks in the core) --- 3. Preservation: findings are not corrupted during transit to Logtalk facts +-- 3. Preservation: cleaned findings keep repo/file/category/severity when +-- projected to the canonical JSON finding record (schema/findings.ncl) -- --- Corresponds to: lib/verisimdb_connector.ex +-- Corresponds to: lib/verisim_connector.ex (cleaned-finding projection model). +-- Statement superseded 2026-11-01: the 2026-04-04 target was the retired +-- Logtalk fact format. The equality proof below is unchanged; its target is +-- now the JSON finding record. This model does not by itself prove runtime +-- refinement of the Elixir connector (estate PROOF-POLICY); see +-- docs/rules/logtalk-migration.adoc and verification/PROOF-STATUS.adoc. module VerisimdbConnector @@ -142,29 +148,30 @@ cleanFindingSoundness (MkRawFinding (Just _) (Just _) (Just _) (Just sevS) (Just Right (Right (Right (Right p))) => absurd p ------------------------------------------------------------------------ --- Section 3: Transit to Logtalk Facts +-- Section 3: Projection to the canonical finding record ------------------------------------------------------------------------ -||| Representation of a Logtalk fact. +||| The repo/file/category/severity projection of a finding: the fields a +||| canonical JSON finding (schema/findings.ncl) carries for every result. +||| (Named LogtalkFact until the 2026-11-01 supersession in the header.) public export -record LogtalkFact where +record FindingFact where constructor MkFact repo : String file : String category : String severity : Severity -||| Transform a clean Pattern into a Logtalk fact. -||| This models the logic in VerisimdbConnector.to_logtalk_facts. +||| Project a clean Pattern to its canonical finding record. public export -toFact : Pattern -> LogtalkFact +toFact : Pattern -> FindingFact toFact p = let r = case p.affectedRepos of [] => "unknown" (h :: _) => h in MkFact r p.file p.description p.severity -||| Proof: data preservation — fields in the Fact match the Pattern exactly. +||| Proof: data preservation — fields in the record match the Pattern exactly. public export factPreservesData : (p : Pattern) -> (r : String) -> p.affectedRepos = [r] -> ( (toFact p).repo = r