[kani] Upgrade verifier to 0.67.0

.github/workflows/ci.yml

@@ -740,10 +740,12 @@ jobs:
           # TODO(https://github.com/model-checking/kani-github-action/issues/56):
           # Go back to testing all features once the Kani GitHub Action supports
           # specifying a particular toolchain.
-          args: "--manifest-path zerocopy/Cargo.toml --package zerocopy --features __internal_use_only_features_that_work_on_stable --output-format=terse -Zfunction-contracts --randomize-layout --memory-safety-checks --overflow-checks --undefined-function-checks --unwinding-checks"
+          # Memory-safety, overflow, undefined-function, and unwinding checks
+          # are enabled by default. Kani 0.65 removed their positive flags.
+          args: "--manifest-path zerocopy/Cargo.toml --package zerocopy --features __internal_use_only_features_that_work_on_stable --output-format=terse -Zfunction-contracts --randomize-layout"
           # This version is automatically rolled by
           # `roll-pinned-toolchain-versions.yml`.
-          kani-version: 0.60.0
+          kani-version: 0.67.0
 
   # NEON intrinsics are currently broken on big-endian platforms. [1] This test ensures
   # that we don't accidentally attempt to compile these intrinsics on such platforms. We

.github/workflows/roll-pinned-toolchain-versions.yml

@@ -189,28 +189,48 @@ jobs:
           )"
           KANI_LATEST="$(
             sed -nE \
-              's/^kani-verifier = "([0-9]+\.[0-9]+\.[0-9]+)".*/\1/p' \
+              's/^kani-verifier = "((0|[1-9][0-9]*)\.(0|[1-9][0-9]*)\.(0|[1-9][0-9]*))".*/\1/p' \
               <<< "$KANI_SEARCH"
           )"
-          if ! [[ "$KANI_LATEST" =~ ^[0-9]+\.[0-9]+\.[0-9]+$ ]]; then
+          KANI_SEMVER_CORE='(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)'
+          KANI_VERSION_REGEX="^${KANI_SEMVER_CORE}$"
+          if ! [[ "$KANI_LATEST" =~ $KANI_VERSION_REGEX ]]; then
             echo "Could not parse a Kani version from: $KANI_SEARCH" >&2
             exit 1
           fi
           echo "ZC_KANI_LATEST=$KANI_LATEST" >> "$GITHUB_ENV"
 
-          # Update the `kani-version:` argument in-place.
-          MATCH_COUNT="$(
-            grep -Ec '^ *kani-version: [0-9]+\.[0-9]+\.[0-9]+$' \
-              .github/workflows/ci.yml || true
-          )"
-          if [ "$MATCH_COUNT" -ne 1 ]; then
-            echo "Expected exactly one Kani version in ci.yml; found $MATCH_COUNT" >&2
+          # Update only the executable `kani-version:` argument in-place. Do
+          # not mechanically update the manual compiler/CBMC audit in
+          # `agent_docs/validation.md`: on branches which carry that audit,
+          # `ci/check_actions.sh` deliberately fails until a human replaces
+          # the audit and its version label after checking the new release.
+          mapfile -t KANI_PIN_LINES < <(
+            # Count every non-comment textual candidate before requiring the
+            # one canonical spelling below. This catches quoted YAML keys,
+            # whitespace before `:`, and malformed duplicates.
+            awk '
+              {
+                line = $0
+                sub(/^[[:space:]]*/, "", line)
+                if (line !~ /^#/ && line ~ /kani-version/) print
+              }
+            ' .github/workflows/ci.yml
+          )
+          if [ "${#KANI_PIN_LINES[@]}" -ne 1 ]; then
+            echo "Expected exactly one Kani pin candidate in ci.yml; found ${#KANI_PIN_LINES[@]}" >&2
+            exit 1
+          fi
+          KANI_PIN_LINE_REGEX="^([[:space:]]*)kani-version:[[:space:]]+${KANI_SEMVER_CORE}$"
+          if ! [[ "${KANI_PIN_LINES[0]}" =~ $KANI_PIN_LINE_REGEX ]]; then
+            echo "Malformed Kani pin in ci.yml: ${KANI_PIN_LINES[0]}" >&2
             exit 1
           fi
+          KANI_PIN_INDENT="${BASH_REMATCH[1]}"
           sed -i -E -e \
-            "s/^( *kani-version:)( [0-9]+\.[0-9]+\.[0-9]+)/\1 $KANI_LATEST/" \
+            "s/^([[:space:]]*)kani-version:[[:space:]]+${KANI_SEMVER_CORE}$/\1kani-version: $KANI_LATEST/" \
             .github/workflows/ci.yml
-          grep -E "^ *kani-version: $KANI_LATEST$" \
+          grep -F -x "${KANI_PIN_INDENT}kani-version: $KANI_LATEST" \
             .github/workflows/ci.yml >/dev/null
       - name: Submit PR
         id: submit-pr
@@ -220,6 +240,16 @@ jobs:
           author: Google PR Creation Bot <github-pull-request-creation-bot@google.com>
           committer: Google PR Creation Bot <github-pull-request-creation-bot@google.com>
           title: "[ci] Roll pinned Kani version"
+          body: |
+            This automation updates only the executable Kani pin; it does not
+            claim that the prior manual compiler/CBMC audit applies to the new
+            release.
+
+            On branches carrying that audit, `ci/check_actions.sh` will fail
+            closed until a human installs the new release, replaces the
+            compiler/target/CBMC record, rechecks every versioned Rust contract
+            and tool-option premise, updates the audited-version label, and
+            reruns the complete Kani suite.
           branch: roll-pinned-kani-to-${{ env.ZC_KANI_LATEST }}-for-${{ matrix.branch }}
           push-to-fork: google-pr-creation-bot/zerocopy
           token: ${{ secrets.GOOGLE_PR_CREATION_BOT_TOKEN }} # zizmor: ignore[secrets-outside-env]

ci/check_actions.sh

@@ -13,6 +13,70 @@ cd "$(dirname "$0")/.."
 
 script_name="ci/check_actions.sh"
 
+# The Kani toolchain audit is manual: it records the bundled compiler, target,
+# CBMC, option behavior, and the applicability of versioned Rust contracts.
+# Require its visible version label to match the executable workflow pin so an
+# automated pin-only roll cannot silently make that record stale.
+semver_core='(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)'
+kani_pin_line_regex="^[[:space:]]*kani-version:[[:space:]]+(${semver_core})$"
+kani_audit_line_regex="^[[:space:]]*-[[:space:]]+\*\*Recorded toolchain audit for \`kani-version: (${semver_core})\`:\*\*.*$"
+
+# Count every candidate before parsing. A valid line must not hide an
+# additional malformed or duplicate key/label.
+kani_pin_lines=()
+# Process substitution keeps this loop in the current shell, while `IFS=` and
+# `read -r` preserve every candidate verbatim. This spelling works in Bash 3,
+# which does not provide `mapfile`.
+while IFS= read -r line || [[ -n "$line" ]]; do
+    kani_pin_lines[${#kani_pin_lines[@]}]="$line"
+done < <(
+    # Deliberately conservative: catch quoted keys, whitespace before `:`, and
+    # other noncanonical YAML spellings. The strict parser below accepts only
+    # the one canonical line, so an equivalent duplicate cannot hide from the
+    # audit-version comparison.
+    awk '
+        {
+            line = $0
+            sub(/^[[:space:]]*/, "", line)
+            if (line !~ /^#/ && line ~ /kani-version/) print
+        }
+    ' .github/workflows/ci.yml
+)
+kani_audit_lines=()
+while IFS= read -r line || [[ -n "$line" ]]; do
+    kani_audit_lines[${#kani_audit_lines[@]}]="$line"
+done < <(
+    grep -F 'Recorded toolchain audit for' zerocopy/agent_docs/validation.md || true
+)
+
+if [[ ${#kani_pin_lines[@]} -ne 1 ]]; then
+    echo "$script_name: expected exactly one Kani workflow-pin candidate; found ${#kani_pin_lines[@]}" >&2
+    exit 1
+fi
+if [[ ${#kani_audit_lines[@]} -ne 1 ]]; then
+    echo "$script_name: expected exactly one recorded Kani audit-label candidate; found ${#kani_audit_lines[@]}" >&2
+    exit 1
+fi
+if [[ "${kani_pin_lines[0]}" =~ $kani_pin_line_regex ]]; then
+    kani_version="${BASH_REMATCH[1]}"
+else
+    echo "$script_name: malformed Kani workflow pin: '${kani_pin_lines[0]}'" >&2
+    exit 1
+fi
+if [[ "${kani_audit_lines[0]}" =~ $kani_audit_line_regex ]]; then
+    kani_audit_version="${BASH_REMATCH[1]}"
+else
+    echo "$script_name: malformed recorded Kani audit label: '${kani_audit_lines[0]}'" >&2
+    exit 1
+fi
+if [[ "$kani_version" != "$kani_audit_version" ]]; then
+    printf '%s\n' \
+        "$script_name: Kani $kani_version is pinned, but the manual toolchain audit covers Kani $kani_audit_version." \
+        "$script_name: replace the compiler/target/CBMC audit, recheck every versioned contract and tool-option premise, update its version label, and rerun the complete Kani suite." \
+        >&2
+    exit 1
+fi
+
 # Ensure action-validator is installed
 if [ ! -x "$HOME/.cargo/bin/action-validator" ]; then
     echo "$script_name: action-validator not found, installing..." >&2

tools/cargo-zerocopy/src/main.rs

@@ -329,6 +329,15 @@ fn get_toolchain_rustflags(name: &str) -> String {
     format!("--cfg __ZEROCOPY_TOOLCHAIN=\"{}\"", name)
 }
 
+fn join_flags(flags: &[&str]) -> String {
+    flags
+        .iter()
+        .map(|flag| flag.trim())
+        .filter(|flag| !flag.is_empty())
+        .collect::<Vec<_>>()
+        .join(" ")
+}
+
 fn rustup<'a>(args: impl IntoIterator<Item = &'a str>, env: Option<(&str, &str)>) -> Command {
     let mut cmd = Command::new("rustup");
     // It's important to set `RUSTUP_TOOLCHAIN` to override any value set while
@@ -414,13 +423,12 @@ fn delegate_cargo() -> Result<(), Error> {
                     .next()
                     .unwrap_or_default();
 
-                let rustflags = format!(
-                    "{} {} {}",
-                    get_rustflags(name),
-                    get_toolchain_rustflags(name),
-                    env_rustflags,
-                );
-                let rustdocflags = format!("{rustflags} {env_rustdocflags}");
+                let rustflags = join_flags(&[
+                    &get_rustflags(name),
+                    &get_toolchain_rustflags(name),
+                    &env_rustflags,
+                ]);
+                let rustdocflags = join_flags(&[&rustflags, &env_rustdocflags]);
 
                 // Rustdoc needs the wrapper's cfgs and the caller's RUSTFLAGS
                 // in addition to any rustdoc-specific flags supplied through
@@ -495,12 +503,20 @@ fn delegate_cargo() -> Result<(), Error> {
 mod tests {
     use std::{ffi::OsStr, process::Command};
 
-    use super::{capture_feature_selection_args, set_ui_test_feature_args};
+    use super::{capture_feature_selection_args, join_flags, set_ui_test_feature_args};
 
     fn strings(args: &[&str]) -> Vec<String> {
         args.iter().map(|arg| (*arg).to_string()).collect()
     }
 
+    #[test]
+    fn joins_nonempty_flags_without_outer_whitespace() {
+        assert_eq!(
+            join_flags(&["", "  --cfg foo ", " ", "-C opt-level=2"]),
+            "--cfg foo -C opt-level=2"
+        );
+    }
+
     #[test]
     fn captures_feature_selection_before_separator() {
         let args = strings(&[

zerocopy/agent_docs/validation.md

@@ -60,19 +60,123 @@ usually sufficient.
     - **Purpose:** Use the
       [Kani Rust Verifier](https://model-checking.github.io/kani/) to prove the
       soundness of `unsafe` code or code relied upon by `unsafe` blocks. Unlike
-      testing, which checks specific inputs, Kani proves properties for *all*
-      possible inputs.
+      testing, which checks selected executions, Kani exhaustively checks a
+      harness's modeled state space. That state space is limited by the
+      harness's bounds and assumptions, its target and feature configuration,
+      and Kani's model of Rust.
     - **How to Write Proofs:**
         - **Harnesses:** Mark proof functions with `#[kani::proof]`.
         - **Inputs:** Use `kani::any()` to generate arbitrary inputs.
         - **Assumptions:** Use `kani::assume(condition)` to constrain inputs to
           valid states (e.g., `align.is_power_of_two()`).
         - **Assertions:** Use `assert!(condition)` to verify the properties you
           want to prove.
-    - **CI:** Kani runs in CI using the `model-checking/kani-github-action` with
-      specific feature flags to ensure compatibility.
+        - **Oracles:** Every oracle must be independent of the implementation
+          under proof. Prefer a safe Rust language or standard-library
+          operation whose documented contract directly supplies the expected
+          behavior. Do not call the target, reuse its zerocopy helper or policy,
+          or manually reconstruct the same unchecked operation. For every
+          oracle, state its normative basis, why it is independent, and its
+          limitations. If no safe oracle exists, isolate the smallest manual
+          rule and cite its normative basis. If a predicate merely restates a
+          zerocopy acceptance policy, label it as a policy oracle rather than
+          evidence of Rust-level validity.
+        - **Factoring:** Share repeated case generation, oracle construction,
+          and postcondition checks within the proof module. Keep distinct
+          harnesses when they exercise different entry points or contracts.
+        - **Domain:** Document every scope dimension independently: the
+          symbolic input domain; concrete size, allocation, loop, and unwind
+          bounds; assumptions and excluded boundary cases; Kani and bundled
+          compiler selection; target and data model; enabled features and
+          verifier flags; randomized-layout count or seed; the established
+          properties; and explicit non-goals. Shared configuration may be
+          factored into a nearby family or module scope only when every covered
+          harness refers to it unambiguously.
+        - **Bit validity:** `kani::any::<T>()` produces only valid instances of
+          `T`. To verify a byte validator, generate arbitrary bytes and decide
+          expected acceptance using an independent oracle before consulting the
+          target. Never materialize `T` merely because the validator under
+          proof accepts: that validator may be the bug. Construct `T` only
+          through an independently safe checked operation. If no such operation
+          exists, exercise only a non-materializing decision path for invalid
+          candidates and document that limitation.
+        - **Soundness boundary:** State which obligations Kani does not prove.
+          In particular, Kani does not completely check reference aliasing,
+          pointer provenance, invalid values, or uninitialized memory. Kani's
+          official [Rust feature support] table marks breaking pointer aliasing
+          rules and producing invalid values as unsupported (where unsupported
+          analyses "should not be trusted"), and describes uninitialized-memory
+          checking as partial and experimental. Its [undefined-behaviour guide]
+          also explains the corresponding reference-lifetime and invalid-value
+          gaps. Treat conclusions that depend on those semantics as TOOL/TCB
+          premises rather than proof results.
+        - **Layout randomization:** `--randomize-layout` checks one randomized
+          layout per run; it does not prove behavior for every layout or target.
+    - **Kani CI configuration:** The exact Kani release is the single
+      `kani-version` pin in `.github/workflows/ci.yml`; its bundled compiler is
+      the proof toolchain. CI runs on `x86_64-unknown-linux-gnu` (64-bit,
+      little-endian) with
+      `__internal_use_only_features_that_work_on_stable` (`alloc`, `derive`,
+      `simd`, and `std`), `-Zfunction-contracts`, and one layout selected by
+      `--randomize-layout` per invocation. Source-level proof scopes should
+      refer to this common configuration and state any deviations.
+    - **Compiler and documentation compatibility:** After installing the
+      pinned Kani release, inspect the `kani-compiler` executable in that
+      release's installation directory (normally
+      `~/.kani/kani-<version>/bin/kani-compiler`) with `--version --verbose`,
+      and inspect its data model with `--print cfg`. Proof premises must cite
+      versioned Rust Reference or standard-library documentation. When changing
+      the Kani pin, manually recheck every such premise against the new compiler
+      snapshot; mechanically changing citation versions does not establish that
+      a guarantee still applies. This compatibility check is a manual TOOL/TCB
+      premise: a successful Kani run does not itself establish that the cited
+      documentation describes the bundled compiler snapshot.
+    - **Fail-closed audit synchronization:** `ci/check_actions.sh`, run by
+      pre-push and CI, requires the `kani-version` pin to equal the version named
+      by the recorded audit below. The scheduled Kani roller intentionally
+      changes only the executable pin, so its PR cannot pass this check until a
+      human completes the audit workflow. Do not mechanically update the audit
+      version label: first install the new release; replace the compiler,
+      target, CBMC, and option-behavior record; recheck every versioned Rust
+      contract against the new compiler snapshot; and rerun the complete Kani
+      suite. Only then update the label to the new pin.
+    - **Recorded toolchain audit for `kani-version: 0.67.0`:** On 2026-09-08,
+      `kani-compiler --version --verbose` reported `rustc 1.93.0-nightly`, commit
+      `53732d5e076329a62f71d3c6901886ce8a71e812` dated 2025-11-20, LLVM 21.1.5,
+      and host `x86_64-unknown-linux-gnu`; `kani-compiler --print cfg` reported
+      Linux/gnu, x86_64, little endian, 64-bit pointers, and panic unwinding.
+      The bundled `cbmc --version` reported CBMC 6.8.0, and its `--help`
+      reported `--no-malloc-may-fail  disable potential malloc failure` and
+      `--malloc-may-fail  allow malloc calls to return a null pointer`. The
+      admitted compatibility proposition is that the versioned Rust 1.93.0
+      contracts cited by the current proofs describe the corresponding
+      behavior of this nightly snapshot. This was checked manually, not proved
+      by Kani. Kani 0.67 [does not model stack unwinding][Kani panic strategies]
+      even though
+      its bundled compiler's target cfg reports `panic="unwind"`; proofs may
+      use reachable panics as failed properties but may not infer cleanup or
+      post-panic behavior.
+
+[Rust feature support]: https://model-checking.github.io/kani/rust-feature-support.html
+[undefined-behaviour guide]: https://model-checking.github.io/kani/undefined-behaviour.html
+[Kani panic strategies]: https://github.com/model-checking/kani/blob/kani-0.67.0/docs/src/rust-feature-support.md#panic-strategies
+
+Before running proofs locally, install the Kani version pinned in
+`.github/workflows/ci.yml`. Run Kani locally through the required repository
+wrapper with:
 
-<!-- FIXME: Describe how to ensure that a Kani proof is "total" (esp wrt function inputs). -->
+```bash
+./cargo.sh +stable kani \
+  --package zerocopy \
+  --features __internal_use_only_features_that_work_on_stable \
+  --output-format=terse \
+  -Zfunction-contracts \
+  --randomize-layout
+```
+
+At this intermediate commit, CI invokes `cargo-kani` directly while the
+wrapper injects project source-selection cfgs. Consequently, the local and CI
+source-selection configurations are not identical.
 
 ## Feature Gates