Rocq and Lean recheck legs for N-1..3, N-7..9 (PWG-2ii)

.github/hooks/scan-secrets.sh

@@ -7,13 +7,15 @@
 # ── Why this is NOT duplicated work ─────────────────────────────────────────
 # The estate runs a TWO-TIER secret defence:
 #
-#   CI     gitleaks, via the standards `secret-scanner-reusable.yml`
-#          (gitleaks + rust-secrets + shell-secrets). Catches what reaches the
+#   CI     gitleaks, rust-secrets and shell-secrets, inline in
+#          `.github/workflows/secret-scanner.yml` (the same three scanner
+#          contracts the standards reusable publishes, kept inline so the three
+#          check names are this repository's own). Catches what reaches the
 #          remote, on every pull_request and push to main.
 #   LOCAL  TruffleHog — this script — before the push leaves the machine.
 #
-# Different detection engines at different checkpoints. The reusable's header
-# retires TruffleHog "as redundant with gitleaks"; that judgement is scoped to
+# Different detection engines at different checkpoints. The estate retired
+# TruffleHog "as redundant with gitleaks"; that judgement is scoped to
 # CI, where running both cost twice over one population. It is not a reason to
 # leave the local tier unguarded. DO NOT delete this script as duplication —
 # see .github/workflows/README.adoc, "Secret scanning is single-sourced".

.github/hooks/validate-deed.sh

@@ -9,34 +9,60 @@
 # live here were a second validator. This runs 1-formats/deed/tools/deed_lint.js
 # (Bun) from a standards checkout over the tracked .deed files, as the
 # deed-conformance lane does in CI (.github/workflows/dogfood-gate.yml). The
-# lane is the gate; this is the early warning. A tracked .a2ml file is an
-# error on sight: the format is retired estate-wide (D99, D312) and its facts
-# belong in the repo deed.
+# lane is the gate; this is the early warning.
+#
+# A2ML is retired estate-wide (D99, D312); its facts belong in the repo deed.
+# Without a ledger, any tracked A2ML file is an error on sight. A repository
+# that still carries legacy A2ML lists each file, by exact path, in the
+# shrink-only ledger .machine_readable/a2ml-legacy-allow.txt (owner decision
+# 2026-11-04), and the A2ML check is then the canonical gate,
+# scripts/check-a2ml-archived.sh from the same standards checkout: a file
+# outside the ledger and outside 9-archive/ fails, and so does an entry whose
+# file is gone. With A2ML_BASE set to a ref (CI sets the PR base), an entry
+# the base ledger did not list also fails, so the ledger can only shrink.
 #
 # Environment variables:
 #   INPUT_PATH     — Repository to check (default: .)
 #   STANDARDS_DIR  — A hyperpolymath/standards checkout
 #                    (default: ../standards beside the repository)
+#   A2ML_BASE      — Ref whose ledger this one may not grow beyond (optional)
 #
 # Exit codes:
-#   0 — Every tracked deed lints, or no linter is available (skipped with a
-#       notice: CI still runs the lane)
-#   1 — A deed failed, or a .a2ml file is tracked
+#   0 — Every tracked deed lints and the A2ML check passes, or no linter is
+#       available (skipped with a notice: CI still runs the lane)
+#   1 — A deed failed, or an A2ML file is not accounted for
 
 set -euo pipefail
 
 REPO="${INPUT_PATH:-.}"
 STANDARDS_DIR="${STANDARDS_DIR:-$(cd "$REPO/.." && pwd)/standards}"
+case "$STANDARDS_DIR" in
+    /*) ;;
+    *) STANDARDS_DIR="$PWD/$STANDARDS_DIR" ;;
+esac
 LINTER="$STANDARDS_DIR/1-formats/deed/tools/deed_lint.js"
+A2ML_GATE="$STANDARDS_DIR/scripts/check-a2ml-archived.sh"
+LEDGER=".machine_readable/a2ml-legacy-allow.txt"
 
 cd "$REPO"
 errors=0
 
-mapfile -t a2ml < <(git ls-files -- '*.a2ml')
-for f in "${a2ml[@]}"; do
-    echo "::error file=$f::.a2ml is retired; move its facts into the repo deed and delete it"
-    errors=$((errors + 1))
-done
+if [ -f "$LEDGER" ]; then
+    if [ -f "$A2ML_GATE" ]; then
+        echo "  A2ML: checking against the shrink-only ledger $LEDGER"
+        if ! bash "$A2ML_GATE" ${A2ML_BASE:+--base "$A2ML_BASE"} .; then
+            errors=$((errors + 1))
+        fi
+    else
+        echo "::notice::A2ML: $LEDGER is present but the canonical gate is not ($A2ML_GATE); the deed-conformance lane checks it in CI"
+    fi
+else
+    mapfile -t a2ml < <(git ls-files | grep -E '\.a2ml(\.in|\.template|\.v[0-9]+\.template)?$' | grep -v '^9-archive/' || true)
+    for f in "${a2ml[@]}"; do
+        echo "::error file=$f::.a2ml is retired; move its facts into the repo deed and delete it, or list it in $LEDGER"
+        errors=$((errors + 1))
+    done
+fi
 
 if [ ! -f "$LINTER" ] || ! command -v bun >/dev/null 2>&1; then
     echo "::notice::DEED: no deed linter here (needs Bun and a standards checkout at $STANDARDS_DIR; set STANDARDS_DIR); the deed-conformance lane lints in CI"

.github/hooks/validate-k9.sh

@@ -26,6 +26,10 @@ set -euo pipefail
 
 REPO="${INPUT_PATH:-.}"
 STANDARDS_DIR="${STANDARDS_DIR:-$(cd "$REPO/.." && pwd)/standards}"
+case "$STANDARDS_DIR" in
+    /*) ;;
+    *) STANDARDS_DIR="$PWD/$STANDARDS_DIR" ;;
+esac
 VALIDATOR="$STANDARDS_DIR/1-formats/k9/tools/k9-validate.sh"
 
 if [ ! -f "$VALIDATOR" ]; then

.github/rulesets/README.adoc

@@ -79,14 +79,36 @@ gh api "/repos/{owner}/{repo}/rulesets" --jq '.[] | "\(.id)\t\(.name)\t\(.enforc
 ----
 
 |===
-| Live ruleset | Enforcement | Target | Covers
+| Live ruleset | Enforcement | Target | Rules reported by the API
 
-| `Base` (`23218684`) | active | branch | deletion, required signatures, code scanning (CodeQL/Hypatia), Copilot review, non-fast-forward
-| `Require-Linear-History` (`24258228`) | active | branch | required linear history
-| `Secret-Scan-Floor` (`24309812`) | active | branch | required status checks (`scan / gitleaks`)
+| `Require-Linear-History` (`24258228`) | active | branch | `required_linear_history`
+| `Secret-Scan-Floor` (`24309812`) | active | branch | *none* — `rules: []`
 | `Immutable-Tags` (`22959911`) | active | tag | creation, deletion, non-fast-forward, update, required signatures
 |===
 
+[IMPORTANT]
+====
+Measured 2026-11-08. Two corrections against the previous version of this table:
+
+. `Base` (`23218684`) no longer exists. `GET /rulesets/23218684` returns
+*404 Not Found*, and the repository's ruleset list does not include it. Every
+claim in the drift notes below about what `Base` enforces — code scanning,
+Copilot review, `deletion`, `non_fast_forward` — describes a ruleset that is
+gone. `GET /rules/branches/main` now returns exactly one rule
+(`required_linear_history`, from `24258228`).
+. `Secret-Scan-Floor` (`24309812`) is `active` on `target: branch` with
+`conditions.ref_name.include: ["~DEFAULT_BRANCH"]`, but it carries **zero
+rules**. It therefore requires *no* status check. `scan / gitleaks` is
+*produced* by `.github/workflows/secret-scanner.yml`, not required by anything.
+
+So as of 2026-11-08 `main` is protected only by `required_linear_history`.
+This is a record of the live state, not an endorsement: a status-check floor
+that enforces nothing is not a floor. Restoring it is an owner action on the
+live ruleset and a deliberate decision about which contexts to require, not
+something these files can do on their own — `base.json` is upstream-sourced and
+its `required_status_checks` is deliberately empty.
+====
+
 === Known drift between these files and what is live
 
 The files below are *not* a transcript of the live rulesets. This is the
@@ -95,19 +117,28 @@ divergence as of 2026-10-25, recorded rather than silently reconciled because
 
 *Live rulesets that no synced file describes* ::
 
-`code_scanning` (with CodeQL and Hypatia tools) and `copilot_code_review` are
-enforced live in `Base` (`23218684`), and `Secret-Scan-Floor` (`24309812`)
-enforces `required_status_checks` for `scan / gitleaks` (`integration_id: 15368`),
-yet neither appears in `base.json` nor any upstream file synced into this
-directory. Upstream's nearest equivalent for code scanning,
+CORRECTED 2026-11-08: the previous text here stated that `code_scanning` (CodeQL
+and Hypatia) and `copilot_code_review` are "enforced live in `Base`
+(`23218684`)", and that `Secret-Scan-Floor` (`24309812`) "enforces
+`required_status_checks` for `scan / gitleaks`". Both statements are now false.
+`Base` returns 404 and is absent from the ruleset list; `Secret-Scan-Floor` is
+active but has `rules: []`. No live branch ruleset carries a `code_scanning`
+rule either, so CodeQL and Hypatia currently *report* results without gating
+merges. What remains true is the file-vs-live gap: upstream's nearest
+equivalent for code scanning,
 `config/rulesets/Optimus-Extras.json`, declares `code_scanning` with an *empty*
-`code_scanning_tools` list, so it does not describe what is live here either.
-Conversely, `branch-floor.json` is retained here as the irreducible recovery
-payload even though the separate `Branch-Floor` live ruleset is not currently
-mounted (`Base` covers both `deletion` and `non_fast_forward`).
+`code_scanning_tools` list, so it would not describe a populated live rule
+either. Conversely, `branch-floor.json` is retained here as the irreducible
+recovery payload even though `Branch-Floor` is not mounted as a live ruleset and
+nothing currently supplies its `deletion` / `non_fast_forward` coverage.
 
 *Removed from live `Base` on 2026-10-02 (owner decision)* ::
 
+NOTE (2026-11-08): the history below is retained, but `Base` was subsequently
+deleted outright — the ruleset returns 404 and is absent from the ruleset list.
+Every rule discussed here is now unenforced, including the `deletion` and
+`non_fast_forward` coverage noted further down.
+
 `Scorecard` was dropped from `code_scanning_tools`, and the `code_coverage` rule
 (minimum 80%, max drop 5) was deleted. Neither could ever be satisfied by a pull
 request. `scorecard.yml` runs only on `schedule` and `workflow_dispatch`, and
@@ -123,9 +154,9 @@ so they stay. Do not add either rule back without a producer that runs on
 
 `required_linear_history` is in `base.json` but not in live `Base`; it is
 enforced by the separate `Require-Linear-History` ruleset. `required_status_checks` (an empty list, so a no-op) and the
-`pull_request` rule are likewise absent from live `Base`. (`non_fast_forward` is
+`pull_request` rule are likewise absent from live `Base`. (`non_fast_forward` was
 live in `Base` as of 2026-10-02; `branch-floor.json` also specifies it as a
-retained recovery payload, though `Branch-Floor` is not mounted as a separate live ruleset.)
+retained recovery payload, though `Branch-Floor` is not mounted as a separate live ruleset. With `Base` deleted as of 2026-11-08, no live ruleset supplies `non_fast_forward` or `deletion` on branches.)
 
 *`Immutable-Tags.json` lags the live ruleset* ::
 

.github/workflows/README.adoc

@@ -11,18 +11,36 @@ not "tidied away" into a real coverage gap.
   Independent; this is the repo's own Hypatia coverage.
 * `static-analysis-gate.yml` -> `hypatia-scan` job — runs Hypatia as part of the
   **gate**, then the `deposit-findings` job hands the results to the
-  **gitbot-fleet learning** pipeline. This job is also a *required status check*.
+  **gitbot-fleet learning** pipeline. This job is *documented here as a
+  required status check*, but as of 2026-11-08 no live rule requires it:
+  `GET /rules/branches/main` returns only `required_linear_history`. It is a
+  gate in the sense that it reddens a run; it is not a merge blocker until a
+  ruleset says so.
 
 Same tool, two different consumers (security scan vs fleet learning). Removing
 either loses real function — keep both.
 
 == Secret scanning is single-sourced *in CI* — and two-tier overall
 
-`secret-scanner.yml` calls the standards reusable (gitleaks + a Rust-secrets
-check). An inline TruffleHog job was removed: the reusable deliberately retired
+`secret-scanner.yml` runs all three estate scanners inline: `scan / gitleaks`,
+`scan / rust-secrets` and `scan / shell-secrets`. An inline TruffleHog job was
+removed earlier: the standards reusable it was paired with deliberately retired
 TruffleHog as redundant with gitleaks, so re-adding it was duplicated work, not
 extra coverage.
 
+The three jobs are inline rather than one `uses:` of the standards
+`secret-scanner-reusable.yml`, and that is deliberate. A job-level reusable call
+reports `<caller job> / <called job>`, so the wrapper's three public check names
+would depend on job names inside a *remote* workflow: rename one there and three
+required contexts move in every generated repository. Inline jobs whose `name:`
+is the context make the names this repository's own, and the whole file stays
+inside `gh actions-lock`'s model — every `uses:` is a step-level action the
+official generator can lock, so regenerating never leaves a dangling edge. Do
+not "simplify" this back into a single wrapper call;
+
+`metadatastician/standards` does it as a wrapper because it *owns* the reusable
+and can keep `./`-local, so its own names cannot re-stale.
+
 **That retirement is scoped to CI.** The estate runs a deliberate *two-tier*
 secret defence, and the second tier is not in this directory:
 
@@ -32,7 +50,7 @@ secret defence, and the second tier is not in this directory:
 
 | CI
 | gitleaks (+ rust-secrets, shell-secrets)
-| `secret-scanner.yml` -> standards reusable. Runs on pull_request and on push
+| `secret-scanner.yml`, three inline jobs. Runs on pull_request and on push
   to main — i.e. on what has *already reached* the remote.
 
 | Local

.github/workflows/actions.lock

@@ -82,7 +82,7 @@ workflows:
     '.github/workflows/scorecard.yml':
         - 'metadatastician/standards@46ee18323305d5b36e2eef936e47dd54c39ea736'
     '.github/workflows/secret-scanner.yml':
-        - 'metadatastician/standards@46ee18323305d5b36e2eef936e47dd54c39ea736'
+        - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
     '.github/workflows/security-policy.yml':
         - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
     '.github/workflows/sonarqube.yml':

.github/workflows/dogfood-gate.yml

@@ -41,9 +41,11 @@ jobs:
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           repository: metadatastician/standards
-          ref: 8e48b1caade08a552646adeab66558ac43b4360d
+          ref: e064539116c2dcfdf282a4749dbd58c69961c7e6
           path: .standards-deed
-          sparse-checkout: 1-formats/deed
+          sparse-checkout: |
+            1-formats/deed
+            scripts
           sparse-checkout-cone-mode: true
           persist-credentials: false
       - name: Setup Bun runtime
@@ -55,6 +57,10 @@ jobs:
           set -euo pipefail
           rm -rf "$RUNNER_TEMP/standards-deed"
           mv "$PWD/.standards-deed" "$RUNNER_TEMP/standards-deed"
+          if [ -f .machine_readable/a2ml-legacy-allow.txt ] && [ ! -f "$RUNNER_TEMP/standards-deed/scripts/check-a2ml-archived.sh" ]; then
+            echo "::error::A2ML ledger present but scripts/check-a2ml-archived.sh is missing from the standards checkout"
+            exit 1
+          fi
           STANDARDS_DIR="$RUNNER_TEMP/standards-deed" bash .github/hooks/validate-deed.sh
 
   # ---------------------------------------------------------------------------
@@ -79,7 +85,7 @@ jobs:
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           repository: metadatastician/standards
-          ref: 8e48b1caade08a552646adeab66558ac43b4360d
+          ref: e064539116c2dcfdf282a4749dbd58c69961c7e6
           path: .standards-k9
           sparse-checkout: 1-formats/k9
           sparse-checkout-cone-mode: true
@@ -103,6 +109,14 @@ jobs:
           set -euo pipefail
           rm -rf "$RUNNER_TEMP/standards-k9"
           mv "$PWD/.standards-k9" "$RUNNER_TEMP/standards-k9"
+          if [ ! -f "$RUNNER_TEMP/standards-k9/1-formats/k9/tools/k9-validate.sh" ]; then
+            echo "::error::K9 validator is missing from the standards checkout"
+            exit 1
+          fi
+          if ! command -v nickel >/dev/null 2>&1; then
+            echo "::error::nickel is required for K9 layer L2 validation"
+            exit 1
+          fi
           STANDARDS_DIR="$RUNNER_TEMP/standards-k9" bash .github/hooks/validate-k9.sh
 
       # The state -> badge mapping lives in scripts/governance-badge.js and
@@ -567,7 +581,7 @@ jobs:
           else
             GROOVE_STATUS=":ballot_box_with_check:"
           fi
-          if grep -rl 'verisimdb\|VeriSimDB' --include='*.toml' --include='*.yaml' --include='*.yml' --include='*.json' --include='*.rs' --include='*.ex' . 2>/dev/null | head -1 | grep -q .; then
+          if grep -rl 'verisimdb\|VeriSimDB' --include='*.toml' --include='*.yaml' --include='*.yml' --include='*.kyaml' --include='*.json' --include='*.rs' --include='*.ex' . 2>/dev/null | head -1 | grep -q .; then
             SCORE=$((SCORE + 1)); VSDB_STATUS=":white_check_mark:"
           else
             VSDB_STATUS=":ballot_box_with_check:"
@@ -605,7 +619,7 @@ jobs:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           repository: metadatastician/standards
-          ref: 8e48b1caade08a552646adeab66558ac43b4360d
+          ref: e064539116c2dcfdf282a4749dbd58c69961c7e6
           path: _standards
           persist-credentials: false
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1

.github/workflows/dogfood-summary.yml

@@ -64,7 +64,7 @@ jobs:
           fi
 
           # VeriSimDB integration?
-          if grep -rl 'verisimdb\|VeriSimDB' --include='*.toml' --include='*.yaml' --include='*.yml' --include='*.json' --include='*.rs' --include='*.ex' . 2>/dev/null | head -1 | grep -q .; then
+          if grep -rl 'verisimdb\|VeriSimDB' --include='*.toml' --include='*.yaml' --include='*.yml' --include='*.kyaml' --include='*.json' --include='*.rs' --include='*.ex' . 2>/dev/null | head -1 | grep -q .; then
             SCORE=$((SCORE + 1))
             VSDB_STATUS=":white_check_mark:"
           else