[kani] Strengthen DST layout proofs

.github/workflows/ci.yml

@@ -730,6 +730,7 @@ jobs:
           persist-credentials: false
       - uses: model-checking/kani-github-action@f838096619a707b0f6b2118cf435eaccfa33e51f # v1.1
         with:
+          command: zerocopy/ci/run_kani.sh
           # Use `--features __internal_use_only_features_that_work_on_stable`
           # because the Kani GitHub Action uses its own pinned nightly
           # toolchain. Sometimes, we make changes to our nightly features for
@@ -742,7 +743,9 @@ jobs:
           # specifying a particular toolchain.
           # 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"
+          # The custom command enters the `zerocopy` crate directory before
+          # forwarding these arguments.
+          args: "--manifest-path 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.67.0

githooks/pre-push

@@ -19,6 +19,8 @@ echo "Running pre-push git hook: $0"
 ./ci/check_job_dependencies.sh      >/dev/null         & JOB_DEPS_PID=$!
 ./zerocopy/ci/check_all_toolchains_tested.sh >/dev/null & TOOLCHAINS_PID=$!
 ./zerocopy/ci/check_readme.sh                >/dev/null & README_PID=$!
+./zerocopy/ci/run_kani.sh --self-test-cover-parser >/dev/null &
+KANI_RUNNER_PID=$!
 ./zerocopy/ci/check_stale_stderr.sh          >/dev/null & STALE_STDERR_PID=$!
 ./zerocopy/ci/check_versions.sh              >/dev/null & VERSIONS_PID=$!
 ./zerocopy/ci/check_msrv_is_minimal.sh       >/dev/null & MSRV_PID=$!
@@ -34,6 +36,7 @@ wait $FMT_PID
 wait $TOOLCHAINS_PID
 wait $JOB_DEPS_PID
 wait $README_PID
+wait $KANI_RUNNER_PID
 wait $STALE_STDERR_PID
 wait $VERSIONS_PID
 wait $MSRV_PID

zerocopy/agent_docs/validation.md

@@ -92,6 +92,17 @@ usually sufficient.
           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.
+        - **Non-vacuity:** Use `kani::cover!` to check that important input and
+          result partitions are reachable. Every assumption must correspond to
+          a documented precondition or to the stated proof bound. Do not reject
+          inputs using an impossible assumption or a diverging loop. Kani 0.67
+          [treats cover properties as reporting-only][Kani cover renderer] and
+          has no
+          `--fail-on-cover` option: zero satisfied covers can accompany a
+          successful verification result. `ci/run_kani.sh` therefore checks
+          every emitted cover summary and fails unless all cover properties are
+          satisfied. Its parser is part of the pinned-version audit and must be
+          revalidated when Kani or its output format changes.
         - **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
@@ -114,8 +125,17 @@ usually sufficient.
           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
+      the proof toolchain. `ci/run_kani.sh` enters this crate and invokes Kani
+      through `cargo.sh +stable`. The `stable` label selects the repository
+      wrapper configuration; Kani still compiles the proof target with its own
+      bundled compiler. Kani supplies `cfg(kani)` to target crates and
+      `cfg(kani_host)` to host build targets. The wrapper additionally supplies
+      `cfg(zerocopy_unstable_linux)`,
+      `cfg(zerocopy_derive_union_into_bytes)`,
+      `cfg(__ZEROCOPY_INTERNAL_USE_ONLY_DEV_MODE)`,
+      `cfg(__ZEROCOPY_INTERNAL_USE_ONLY_TOOLCHAIN = "stable")`, and
+      `cfg(__ZEROCOPY_TOOLCHAIN = "stable")`. 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
@@ -151,33 +171,36 @@ usually sufficient.
       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
+      by Kani. The audited terse output reports cover summaries as
+      `** N of M cover properties satisfied`, with canonical nonnegative `N`
+      and positive `M`. `ci/run_kani.sh` rejects malformed summary candidates,
+      requires `N == M` for every summary, and requires at least one recognized
+      summary. Pre-push exercises its parser against valid, unsatisfied,
+      absent, nonnumeric, zero-total, noncanonical, extra-token, numeric-
+      precision-edge, and mixed multiple-summary fixtures. 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 cover renderer]: https://github.com/model-checking/kani/blob/kani-0.67.0/kani-driver/src/cbmc_property_renderer.rs
 [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:
+`.github/workflows/ci.yml`. Run the same proof configuration as CI with:
 
 ```bash
-./cargo.sh +stable kani \
+ci/run_kani.sh \
+  --manifest-path Cargo.toml \
   --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
 
 When editing code gated by a feature, compile **with and without** that feature.

zerocopy/ci/run_kani.sh

@@ -0,0 +1,111 @@
+#!/usr/bin/env bash
+#
+# Copyright 2026 The Fuchsia Authors
+#
+# Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+# <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+# license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+# This file may not be copied, modified, or distributed except according to
+# those terms.
+
+set -eo pipefail
+
+ZEROCOPY_DIR="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." && pwd)"
+readonly ZEROCOPY_DIR
+KANI_OUTPUT="$(mktemp)"
+readonly KANI_OUTPUT
+trap 'rm -f "${KANI_OUTPUT}"' EXIT
+
+check_cover_summaries() {
+    awk '
+        /cover[[:space:]]+properties[[:space:]]+satisfied/ {
+            found_cover_candidate = 1
+            if (NF != 7 || $1 != "**" || $3 != "of" || $5 != "cover" ||
+                    $6 != "properties" || $7 != "satisfied" ||
+                    $2 !~ /^(0|[1-9][0-9]*)$/ || $4 !~ /^[1-9][0-9]*$/) {
+                print "Malformed Kani cover summary: " $0 > "/dev/stderr"
+                malformed_cover_summary = 1
+            } else {
+                found_cover_summary = 1
+                # Canonical decimal strings are numerically equal exactly when
+                # their strings are equal; this avoids AWK numeric precision
+                # limits for arbitrarily long counts.
+                if (("count:" $2) != ("count:" $4)) {
+                    print "Kani cover obligation failed: " $0 > "/dev/stderr"
+                    failed_cover = 1
+                }
+            }
+        }
+        END {
+            if (malformed_cover_summary) {
+                exit 2
+            }
+            if (!found_cover_candidate || !found_cover_summary) {
+                print "Kani emitted no recognized cover summary" > "/dev/stderr"
+                exit 2
+            }
+            if (failed_cover) {
+                exit 1
+            }
+        }
+    ' "$1"
+}
+
+expect_parser_result() {
+    local expected="$1"
+    local fixture="$2"
+    local actual
+    printf '%s\n' "${fixture}" > "${KANI_OUTPUT}"
+    if check_cover_summaries "${KANI_OUTPUT}" >/dev/null 2>&1; then
+        actual=success
+    else
+        actual=failure
+    fi
+    if [[ "${actual}" != "${expected}" ]]; then
+        echo "Kani cover parser self-test expected ${expected}: ${fixture}" >&2
+        exit 1
+    fi
+}
+
+if (( $# == 1 )) && [[ "$1" == "--self-test-cover-parser" ]]; then
+    readonly SELF_TEST_VALID_SUMMARY="** 1 of 1 cover properties satisfied"
+    expect_parser_result success "** 2 of 2 cover properties satisfied"
+    expect_parser_result failure "** 1 of 2 cover properties satisfied"
+    expect_parser_result failure "VERIFICATION:- SUCCESSFUL"
+    expect_parser_result failure "** x of x cover properties satisfied"
+    expect_parser_result failure "** 0 of 0 cover properties satisfied"
+    expect_parser_result failure "** 01 of 01 cover properties satisfied"
+    expect_parser_result failure "** 1 of 1 cover properties satisfied extra"
+    expect_parser_result success \
+        "** 9007199254740993 of 9007199254740993 cover properties satisfied"
+    expect_parser_result failure \
+        "** 9007199254740992 of 9007199254740993 cover properties satisfied"
+    expect_parser_result failure \
+        "${SELF_TEST_VALID_SUMMARY}"$'\n'"** 1 of 2 cover properties satisfied"
+    expect_parser_result failure \
+        "${SELF_TEST_VALID_SUMMARY}"$'\n'"* 1 of 1 cover properties satisfied"
+    exit 0
+fi
+
+cd "${ZEROCOPY_DIR}"
+
+set +e
+"${ZEROCOPY_DIR}/cargo.sh" +stable kani "$@" 2>&1 | tee "${KANI_OUTPUT}"
+PIPELINE_STATUS=("${PIPESTATUS[@]}")
+readonly KANI_STATUS="${PIPELINE_STATUS[0]}"
+readonly TEE_STATUS="${PIPELINE_STATUS[1]}"
+set -e
+
+if (( KANI_STATUS != 0 )); then
+    exit "${KANI_STATUS}"
+fi
+if (( TEE_STATUS != 0 )); then
+    exit "${TEE_STATUS}"
+fi
+
+# Kani 0.67 reports unsatisfied `kani::cover!` properties but still exits
+# successfully. Its CLI has no `--fail-on-cover` option. Parse the exact output
+# format audited in `agent_docs/validation.md` so every emitted non-vacuity
+# summary fails closed, and total absence also fails. Re-audit this parser
+# whenever the pinned Kani version changes.
+check_cover_summaries "${KANI_OUTPUT}"