Complete Logtalk to Elixir rule migration

.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]
 ----

.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]
 ----

.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]
 ----

.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]
 ----

.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]
 ----

.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]
 ----

.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]
 ----

.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

.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 @@
     - 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 @@
     - 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 @@
             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

.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/<dir>/`
+# 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

.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: <path> | <classification> | <removal condition>
+#
+# 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

.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 ===

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

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

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)

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]

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]

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