Merge the proven-cicd history and record the 10 November fleet observation

.github/workflows/assurance-kernel.yml

@@ -8,12 +8,18 @@ on:
     paths:
       - "src/Assurance/**"
       - "assurance-kernel.ipkg"
+      - "assurance-github.ipkg"
+      - "scripts/assurance-github.*"
+      - "tests/assurance-github.sh"
+      - "tests/assurance-real-canaries.sh"
+      - "config/assurance-canaries/**"
       - "tests/assurance-kernel.sh"
       - ".github/workflows/assurance-kernel.yml"
   workflow_dispatch:
 
 permissions:
   contents: read
+  actions: read
 
 # PR updates supersede previous costly compiler boots; manual dispatches are unique.
 concurrency:
@@ -42,7 +48,14 @@ jobs:
         run: |
           set -euo pipefail
           sudo apt-get update
-          sudo DEBIAN_FRONTEND=noninteractive apt-get install -y --no-install-recommends chezscheme libgmp-dev git make gcc ca-certificates
+          sudo DEBIAN_FRONTEND=noninteractive apt-get install -y --no-install-recommends chezscheme libgmp-dev git make gcc ca-certificates jq gh
+      - name: Validate bridge shell and qualifier syntax
+        run: |
+          set -euo pipefail
+          for script in scripts/assurance-github.sh tests/assurance-github.sh tests/assurance-real-canaries.sh; do
+            bash -n "$script"
+          done
+          jq -n -L scripts 'include "assurance-github"; true' >/dev/null
       - name: Bootstrap pinned Idris2 0.7.0 source
         env:
           IDRIS2_SOURCE_SHA: 27780073c8631826d846499840b3857d9b9a4fd5
@@ -61,3 +74,20 @@ jobs:
           echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
       - name: Compile model and reject contradictory proof
         run: bash tests/assurance-kernel.sh
+      - name: Compile and exercise the new finite GitHub bridge
+        run: bash tests/assurance-github.sh
+      - name: Observe passing and defective real consumers
+        id: real_canaries
+        if: github.event_name == 'workflow_dispatch'
+        env:
+          GH_TOKEN: ${{ github.token }}
+          GH_PROMPT_DISABLED: "1"
+        run: bash tests/assurance-real-canaries.sh "$RUNNER_TEMP/assurance-real-consumers"
+      - name: Retain separate real consumer verdicts
+        if: ${{ always() && github.event_name == 'workflow_dispatch' && steps.real_canaries.outcome != 'skipped' }}
+        uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2
+        with:
+          name: assurance-real-consumers-${{ github.sha }}-${{ github.run_attempt }}
+          path: ${{ runner.temp }}/assurance-real-consumers/
+          if-no-files-found: error
+          retention-days: 14

.github/workflows/code-hygiene-self-test.yml

@@ -103,6 +103,11 @@
           # which installs none of their tools.
           run: "bash tests/pass-on-absence.sh",
         },
+        {
+          # Exercise both exact suite names, stale pins, missing history and
+          # nonempty populations before checking the real imported source.
+          run: "bash tests/lock-self-source-controls.sh",
+        },
         {
           run: "bash tests/lock-transitive-closure.sh",
         },

.github/workflows/language-gates-self-test.yml

@@ -21,6 +21,7 @@ on:
     branches: [main]
     paths:
       - "actions/rust-ci-check/**"
+      - "actions/verus-check/**"
       - "actions/creusot-check/**"
       - "actions/spark-check/**"
       - "actions/kanren-check/**"
@@ -30,6 +31,7 @@ on:
       - "tests/zig-ffi-scope.sh"
       - "tests/gate-action-owners.sh"
       - "tests/inspect-pr-ci.sh"
+      - "tests/rust-doc-package-scope.sh"
       - "tests/suite-source-compatibility.sh"
       - "scripts/inspect-pr-ci.sh"
       - ".github/workflows/rust-ci.yml"
@@ -41,6 +43,7 @@ on:
   pull_request:
     paths:
       - "actions/rust-ci-check/**"
+      - "actions/verus-check/**"
       - "actions/creusot-check/**"
       - "actions/spark-check/**"
       - "actions/kanren-check/**"
@@ -50,6 +53,7 @@ on:
       - "tests/zig-ffi-scope.sh"
       - "tests/gate-action-owners.sh"
       - "tests/inspect-pr-ci.sh"
+      - "tests/rust-doc-package-scope.sh"
       - "tests/suite-source-compatibility.sh"
       - "scripts/inspect-pr-ci.sh"
       - ".github/workflows/rust-ci.yml"
@@ -111,8 +115,12 @@ jobs:
         run: bash tests/zig-ffi-scope.sh
       - name: Rust gate
         run: bash actions/rust-ci-check/test.sh
+      - name: Scoped Rust documentation still rejects broken doctests
+        run: bash tests/rust-doc-package-scope.sh
       - name: Creusot gate
         run: bash actions/creusot-check/test.sh
+      - name: Verus execution gate controls
+        run: bash actions/verus-check/test.sh
       - name: SPARK gate
         run: bash actions/spark-check/test.sh
       - name: miniKanren gate

.github/workflows/rust-ci.yml

@@ -99,6 +99,11 @@ on:
         type: boolean
         required: false
         default: true
+      doc_packages:
+        description: Cargo package selection for docs and doctests; scope must match the declared consumer boundary
+        type: string
+        required: false
+        default: "--workspace"
       deny_warnings:
         description: Export RUSTFLAGS/RUSTDOCFLAGS "-D warnings" for every compile
         type: boolean
@@ -442,6 +447,7 @@ jobs:
           WORKING_DIRECTORY: ${{ inputs.working_directory }}
           TEST_ARGS: ${{ inputs.test_args }}
           DOCTESTS: ${{ inputs.doctests }}
+          DOC_PACKAGES: ${{ inputs.doc_packages }}
           DENY_WARNINGS: ${{ inputs.deny_warnings }}
         run: bash .cicd-suite/actions/rust-ci-check/check.sh
 
@@ -531,6 +537,7 @@ jobs:
         env:
           RUST_GATE_PHASE: doc
           WORKING_DIRECTORY: ${{ inputs.working_directory }}
+          DOC_PACKAGES: ${{ inputs.doc_packages }}
           DENY_WARNINGS: ${{ inputs.deny_warnings }}
         run: bash .cicd-suite/actions/rust-ci-check/check.sh
 

.github/workflows/secret-scanner-self-test.yml

@@ -30,6 +30,11 @@ jobs:
           bash tests/capability-catalogue.sh
           bash scripts/build-assurance-matrix.sh --check
           bash tests/assurance-matrix.sh
+      - name: Non-enforcing CI profile contract and proposed pilot controls
+        run: |
+          bash tests/ci-profiles.sh
+          bash tests/ci-pilot-manifest.sh
+          bash tests/docs-profile-subject.sh
       - name: Explicit workflow lock scope and omitted-key controls
         run: bash tests/workflow-lock-scope.sh
       - name: Governance pin representation regressions (not full lock verification)

.github/workflows/secret-scanner.yml

@@ -16,7 +16,7 @@ concurrency:
   cancel-in-progress: true
 jobs:
   scan:
-    uses: hyperpolymath/cicd-suite/.github/workflows/secret-scanner-reusable.yml@a12b2b4644db1a1250bc50b58fd24c99f89f564e
+    uses: hyperpolymath/proven-cicd/.github/workflows/secret-scanner-reusable.yml@a12b2b4644db1a1250bc50b58fd24c99f89f564e
     with:
       # Keep false until an initial full audit passes and the security owner
       # accepts introduced-commit PR coverage. All non-PR runs remain full.

README.adoc

@@ -3,6 +3,39 @@
 *An atlas of composable repository assurance: security, governance, build hygiene,
 contracts, language verification and ecosystem integration.*
 
+The link:docs/WORKFLOW-SCOPE.adoc[workflow scope proposal] keeps CI/CD and broader
+repository workflows together while preserving the current published coordinate.
+
+== Canonical repository and migration status
+
+[NOTE]
+====
+This section came from `hyperpolymath/proven-cicd` when its history was merged
+into this repository on 2026-11-10. It describes that repository as of
+2026-11-07. This repository is `hyperpolymath/proven-cicd-and-workflows`, the
+renamed `cicd-suite`. The owner has stated that the two repositories are to be
+one, under this name. The text below is kept as a dated record until the
+migration status is rewritten.
+====
+
+`hyperpolymath/proven-cicd` is the canonical destination for this suite.
+The GitHub import retained the existing Git history and both advertised branch
+heads, including the open Creusot execution-evidence work. The import checkpoint
+is recorded in link:docs/assurance/2026-11-04/CANONICAL-IMPORT.adoc[the canonical
+history and rollout record]. The legacy `hyperpolymath/cicd-suite` repository
+remains available for existing full-SHA callers and its review/run evidence.
+
+Migration is staged: repository protections, two real caller canaries and the
+remaining caller inventory must qualify before an estate-wide cutover. Existing
+full-SHA pins keep their source identity; this repository's scanner caller is a
+coordinate-only canary at the already published `a12b2b4` source. No release or
+gate is certified merely by the new repository name.
+
+The Idris2 verdict kernel is present. Its operational GitHub adapter remains
+unpromoted: review reproduced an invalid duplicate-field response becoming a
+false passed verdict, and the repair must complete its expanded controls before
+publication. See the checkpoint for the exact remaining boundary.
+
 == Discover the suite
 
 Start with the link:CATALOGUE.adoc[*CI/CD Capability Atlas*]: *32 composite actions
@@ -34,6 +67,10 @@ linked regression controls, explicit evidence gaps and consumer receipts, and
 the link:docs/assurance/SUITE-CLOSEOUT.adoc[suite-first completion ledger] for
 remaining shared work. These records do not certify every capability.
 
+The link:profiles/README.adoc[experimental CI profile contract] adds three
+proposed mother profiles, typed slots, validation controls and a bounded pilot
+manifest. It is non-enforcing and does not qualify consumer CI or add a workflow.
+
 == Estate-wide audit
 
 A subset of the suite is orchestrated by the reusable workflow
@@ -454,7 +491,20 @@ No logs, artifacts, secrets, policy edits, reruns or merges are requested.
 
 See link:docs/CI-TRIAGE-2026-10-30.adoc[the sampled estate diagnosis] and
 link:docs/SECRET-SCAN-PERFORMANCE.adoc[the secret-scan latency investigation
-and implementation handoff]. No replacement scanner has been deployed.
+and implementation handoff]. The bounded scanner is deployed to the suite and
+Echidna canaries. The earlier paired full-history receipts are retained in
+https://github.com/hyperpolymath/cicd-suite/pull/84[suite PR 84]. Canonical-name
+hosted canaries subsequently passed in
+https://github.com/hyperpolymath/proven-cicd/actions/runs/41910602874[Proven CI/CD run 41910602874]
+at subject `5f2fd18c3ec710db00486b9985d0cbb242803463` and
+https://github.com/hyperpolymath/echidna/actions/runs/41909747996[Echidna run 41909747996]
+at subject `b8dc7fa90f82ab124b6af18398999ef6a9724e32`.
+Both runs used scanner source `a12b2b4644db1a1250bc50b58fd24c99f89f564e`.
+These receipts qualify those historical heads only; later heads require their
+own hosted receipts before promotion. See
+link:docs/assurance/2026-11-04/CANONICAL-IMPORT.adoc[the canonical import checkpoint]
+for the retained evidence and remaining rollout conditions. An estate-wide
+replacement has not completed.
 
 === Bounded secret scanner (canary, not estate-deployed)
 
@@ -485,21 +535,19 @@ production rollout; see link:docs/SECRET-SCANNER-ROLLOUT.adoc[rollout status].
 
 ==== Post-merge startup repair and supplemental detector ports
 
-The follow-up described in
+The dated checkpoint in
 link:docs/SCANNER-STARTUP-AND-PARITY.adoc[Startup and supplemental coverage]
-repins this repository to the published #62 merge commit. The initial
-pre-merge pin failed resolution after merge; the canonical legacy dependency
-was then explicitly refused by the caller's Actions admission policy.
-Rather than broadening permissions, the suite now carries Rust/shell ports
-and 26 differential fixtures against frozen legacy run bodies, plus five
-hardening controls. The former legacy comparison workflow runs these local
-checks; it no longer invokes standards or repeats full-history Gitleaks.
-
-The new scanner source includes both ports in its composite verdict. Publish
-that implementation before advancing consumer pins: the currently deployed
-suite pin still selects the previously published scanner, while separate
-local supplement jobs preserve this repository's supplementary checking.
-No estate-wide rollout or whole-corpus equivalence is claimed by the fixtures.
+records the earlier pre-merge pin and admission failures. Its deployment status
+is historical. The integrated source was subsequently published and qualified
+with the suite and Echidna callers; the current full source pin is
+`a12b2b4644db1a1250bc50b58fd24c99f89f564e`.
+
+The reusable scanner now provides all three original contexts: Gitleaks, Rust
+secrets and shell secrets. Both canonical-name caller runs linked above executed
+that exact published source. The separate local supplemental workflow remains
+a regression control; it does not supply a missing port in the deployed source.
+The 26 differential fixtures and five hardening controls retain their finite
+coverage boundary. No estate-wide rollout or whole-corpus equivalence is claimed.
 
 == Strict scanner coverage and audit checkpoint
 
@@ -512,6 +560,6 @@ interpret an exit-zero partial scan as assurance. panic-attack assail findings
 remain report-only; strict coverage is not a security verdict.
 
 See link:docs/assurance/AUDIT-2026-11-04.adoc[the adversarial audit checkpoint]
-for executed controls, coverage gaps, proof boundaries and the pending
-`proven-cicd` rename. Reproduce bounded scanner controls with
+for executed controls, coverage gaps and proof boundaries. The canonical
+repository now exists; protection and consumer migration are still in progress. Reproduce bounded scanner controls with
 `bash tests/scanner-adversarial.sh /path/to/pons /path/to/panic-attack`.

actions/creusot-check/test.sh

@@ -41,13 +41,16 @@ fresh_fixture() {
     git -C "$FIX" init -q
     git -C "$FIX" config user.email t@example.invalid
     git -C "$FIX" config user.name t
+    # These temporary fixture commits are not published. A developer's locked
+    # signing key must not turn fixture creation into missing source evidence.
+    git -C "$FIX" config commit.gpgsign false
     printf '[package]\nname = "fx"\nversion = "0.1.0"\nedition = "2021"\n\n[dependencies]\n' > "$FIX/Cargo.toml"
     printf '//! fixture\npub fn id(x: u32) -> u32 { x }\n' > "$FIX/src/lib.rs"
     printf '= fx\n\nA small crate.\n' > "$FIX/README.adoc"
     printf '{"packages":["creusot"],"provers":["z3"]}\n' > "$FIX/why3find.json"
-    git -C "$FIX" add -A && git -C "$FIX" commit -qm fixture
+    git -C "$FIX" add -A && git -C "$FIX" commit -qm fixture || exit 2
 }
-commit() { git -C "$FIX" add -A && git -C "$FIX" commit -qm change >/dev/null; }
+commit() { git -C "$FIX" add -A && git -C "$FIX" commit -qm change >/dev/null || exit 2; }
 run_phase() { # <phase> [env...]
     local phase="$1"; shift
     : > "$WORK/receipt"

actions/rust-ci-check/action.yml

@@ -30,6 +30,10 @@ inputs:
     description: 'Run cargo test --doc as well (true|false)'
     required: false
     default: 'true'
+  doc_packages:
+    description: 'Cargo package selection for docs and doctests; default covers the whole workspace'
+    required: false
+    default: '--workspace'
   deny_warnings:
     description: 'Export RUSTFLAGS/RUSTDOCFLAGS=-D warnings for every compile'
     required: false
@@ -50,6 +54,7 @@ runs:
         CLIPPY_ARGS: ${{ inputs.clippy_args }}
         TEST_ARGS: ${{ inputs.test_args }}
         DOCTESTS: ${{ inputs.doctests }}
+        DOC_PACKAGES: ${{ inputs.doc_packages }}
         DENY_WARNINGS: ${{ inputs.deny_warnings }}
         MSRV: ${{ inputs.msrv }}
       run: bash "$GITHUB_ACTION_PATH/check.sh"

actions/rust-ci-check/check.sh

@@ -43,6 +43,7 @@ check_args="${CHECK_ARGS:---all-targets}"
 clippy_args="${CLIPPY_ARGS:---all-targets -- -D warnings}"
 test_args="${TEST_ARGS:---all-targets}"
 doctests="${DOCTESTS:-true}"
+doc_packages="${DOC_PACKAGES:---workspace}"
 deny_warnings="${DENY_WARNINGS:-true}"
 
 fail=0
@@ -94,9 +95,10 @@ case "$phase" in
     # shellcheck disable=SC2086
     run "cargo test" cargo test --locked $test_args
     if [ "$doctests" = true ]; then
-      echo "::group::cargo doctests — cargo test --locked --doc --workspace"
+      echo "::group::cargo doctests — cargo test --locked --doc $doc_packages"
       out="$(mktemp)"
-      if cargo test --locked --doc --workspace 2>&1 | tee "$out"; then
+      # shellcheck disable=SC2086 # Cargo package selectors are deliberately word-split
+      if cargo test --locked --doc $doc_packages 2>&1 | tee "$out"; then
         echo "::endgroup::"
         echo "ok: cargo doctests"
       else
@@ -107,7 +109,7 @@ case "$phase" in
            && [ "$(grep -cE '^error' "$out" || true)" -eq 1 ]; then
           echo "::notice::rust-ci-check[test]: no library target in the workspace, so there are no doctests to run (cargo: 'no library targets found'). This is a fact about the crate, not a skipped check."
         else
-          err "cargo doctests failed: cargo test --locked --doc --workspace"
+          err "cargo doctests failed: cargo test --locked --doc $doc_packages"
         fi
       fi
       rm -f "$out"
@@ -116,7 +118,8 @@ case "$phase" in
     fi
     ;;
   doc)
-    run "cargo doc" cargo doc --locked --no-deps --document-private-items --workspace
+    # shellcheck disable=SC2086
+    run "cargo doc" cargo doc --locked --no-deps --document-private-items $doc_packages
     ;;
   msrv)
     msrv="${MSRV:-}"

actions/verus-check/check.sh

@@ -0,0 +1,36 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Run an installed Verus with planted controls; no source download here.
+set -euo pipefail
+verifier="${VERUS:-verus}"
+command -v "$verifier" >/dev/null || { echo "Verus unavailable: no proof performed" >&2; exit 2; }
+[[ $# -gt 0 ]] || { echo "Supply at least one Rust proof file" >&2; exit 2; }
+for source in "$@"; do
+  [[ -f "$source" && "$source" == *.rs && "$source" != -* ]] || { echo "Invalid proof source: $source" >&2; exit 2; }
+done
+work=$(mktemp -d)
+trap 'rm -rf "$work"' EXIT
+cat > "$work/positive.rs" <<'RS'
+use vstd::prelude::*;
+verus! { pub fn positive() -> (r: u32) ensures r == 2 { 2 } }
+RS
+cat > "$work/negative.rs" <<'RS'
+use vstd::prelude::*;
+verus! { pub fn negative() -> (r: u32) ensures r == 0 { 1 } }
+RS
+if "$verifier" --no-cheating --crate-type lib "$work/negative.rs" >"$work/negative.log" 2>&1; then
+  echo "False contract accepted: no caller proof credited" >&2; exit 2
+fi
+report() {
+  grep -qE '^verification results:: [1-9][0-9]* verified, 0 errors$' "$1"
+}
+if ! "$verifier" --no-cheating --crate-type lib "$work/positive.rs" >"$work/positive.log" 2>&1 || ! report "$work/positive.log"; then
+  cat "$work/positive.log" >&2
+  echo "Positive control unavailable: no caller proof credited" >&2; exit 2
+fi
+for source in "$@"; do
+  "$verifier" --no-cheating --crate-type lib "$source" >"$work/caller.log" 2>&1 || { cat "$work/caller.log" >&2; exit 1; }
+  report "$work/caller.log" || { echo "No nonzero proof report: $source" >&2; exit 2; }
+  printf 'verified source: %s\n' "$source"
+  cat "$work/caller.log"
+done