Share Rust mathematical models across Anneal frontends

.github/workflows/anneal-release.yml

@@ -287,6 +287,7 @@ jobs:
           mkdir -p anneal/target anneal/v1/release-download-check anneal/v1/release-metadata
 
           nix build ./anneal#omnibus-archive-ci --out-link "anneal/target/${ARCHIVE_NAME}"
+          nix build ./anneal#omnibus-archive-layout-check --no-link
           cp -L "anneal/target/${ARCHIVE_NAME}" "anneal/v1/${ARCHIVE_NAME}"
           ARCHIVE_SIZE="$(python3 -c 'import os, sys; print(os.path.getsize(sys.argv[1]))' "anneal/v1/${ARCHIVE_NAME}")"
           printf 'Built %s (%s bytes)\n' "$ARCHIVE_NAME" "$ARCHIVE_SIZE"

.github/workflows/anneal.yml

@@ -292,14 +292,14 @@ jobs:
       # remains the cross-job fan-out mechanism for the current run.
       #
       # Keep the key inputs in sync with the local files that influence
-      # `.#omnibus-archive-ci`. It intentionally excludes most Anneal source
-      # files so ordinary PRs can reuse the archive built from `main`.
+      # `.#omnibus-archive-ci`. The shared Lean package is built into that
+      # archive, so changes under anneal/lean must invalidate this cache.
       - name: Restore Anneal main Nix binary cache
         id: restore_anneal_main_nix_cache
         uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
         with:
           path: anneal/target/nix-cache-main
-          key: anneal-v2-main-nix-cache-v2-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('anneal/flake.nix', 'anneal/flake.lock', 'anneal/rewrite-lake-vendor.py', 'anneal/prune-lake-cache.py') }}
+          key: anneal-v2-main-nix-cache-v3-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('anneal/flake.nix', 'anneal/flake.lock', 'anneal/rewrite-lake-vendor.py', 'anneal/prune-lake-cache.py', 'anneal/lean/**') }}
 
       # Pull request caches are scoped by GitHub to the PR merge ref, so they
       # can speed up repeated pushes to the same PR without becoming visible to
@@ -319,7 +319,7 @@ jobs:
         uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
         with:
           path: anneal/target/nix-cache-pr
-          key: anneal-v2-pr-nix-cache-v1-${{ runner.os }}-${{ runner.arch }}-pr-${{ github.event.pull_request.number }}-${{ hashFiles('anneal/flake.nix', 'anneal/flake.lock', 'anneal/rewrite-lake-vendor.py', 'anneal/prune-lake-cache.py') }}
+          key: anneal-v2-pr-nix-cache-v2-${{ runner.os }}-${{ runner.arch }}-pr-${{ github.event.pull_request.number }}-${{ hashFiles('anneal/flake.nix', 'anneal/flake.lock', 'anneal/rewrite-lake-vendor.py', 'anneal/prune-lake-cache.py', 'anneal/lean/**') }}
 
       - name: Install Nix
         uses: DeterminateSystems/determinate-nix-action@4d65ea9cab522b6d9f29a170aed23ededc1b27af # v3.23.0

anneal/check-flake-eval.sh

@@ -35,6 +35,7 @@ packages=(
   omnibus-archive-layout-check
   omnibus-tar
   rust-toolchain
+  rust-model-compiled
 )
 
 for system in "${systems[@]}"; do

anneal/flake.nix

@@ -490,6 +490,64 @@
           ];
         };
 
+        # Build the shared Rust semantics library independently of Aeneas.
+        # Its Lean-only sources can be checked with the archive's Lean version
+        # and reused by generated workspaces as a path dependency.
+        packages.rust-model-compiled = pkgs.stdenv.mkDerivation {
+          pname = "anneal-rust-model-compiled";
+          version = "0.1.0";
+
+          src = ./lean;
+          leanToolchain = self.packages.${system}.lean-toolchain;
+
+          nativeBuildInputs = with pkgs; [ python3 ];
+
+          buildPhase = builtins.concatStringsSep "\n" [
+            "export HOME=$TMPDIR"
+            "export PATH=\"$leanToolchain/bin:\$PATH\""
+            "export LEAN_SYSROOT=\"$leanToolchain\""
+            "export LD_LIBRARY_PATH=\"$leanToolchain/lib:$leanToolchain/lib/lean:\$LD_LIBRARY_PATH\""
+            # Keep the source package pin aligned with this archive's Lean.
+            "grep -Fxq 'leanprover/lean4:${leanVersion}' lean-toolchain"
+            (runLeanCommand "lake --old build Rust RustTests RustBytesTests")
+            (runLeanCommand "lake env lean -DwarningAsError=true RustTests.lean")
+            # A fresh verification workspace loads this package as a dependency.
+            # Prime that package configuration while its build tree is writable.
+            "mkdir -p $TMPDIR/rust-model-config-primer/generated"
+            "cp lean-toolchain $TMPDIR/rust-model-config-primer/lean-toolchain"
+            "printf 'import Rust\\n' > $TMPDIR/rust-model-config-primer/generated/Generated.lean"
+            "cat > $TMPDIR/rust-model-config-primer/lakefile.lean <<'EOF'"
+            "import Lake"
+            "open Lake DSL"
+            ""
+            "require rust_model from \"@RUST_MODEL_ROOT@\""
+            ""
+            "package anneal_rust_model_primer"
+            ""
+            "@[default_target]"
+            "lean_lib Generated where"
+            "  srcDir := \"generated\""
+            "  roots := #[`Generated]"
+            "EOF"
+            "substituteInPlace $TMPDIR/rust-model-config-primer/lakefile.lean --replace-fail @RUST_MODEL_ROOT@ \"$PWD\""
+            "(cd $TMPDIR/rust-model-config-primer && ${runLeanCommand "lake --old build Generated"})"
+            "test -n \"\$(find .lake/config -type f -name lakefile.olean -print)\""
+            "mkdir -p $TMPDIR/empty-packages"
+            "python3 ${./rewrite-lake-vendor.py} --root . --packages-dir $TMPDIR/empty-packages --rewrite-traces --trace-prefix \"$leanToolchain=lean\""
+            "TRACE_ABS_RE='(^|[\"[:space:]=:])/(nix/store|build|private/tmp/nix-build|ANNEAL_PLACEHOLDER_ROOT)'"
+            "if find . -type f -name \"*.trace\" -exec grep -EIl \"\$TRACE_ABS_RE\" {} + | grep -q .; then"
+            "  echo \"ERROR: non-relocatable Rust model trace paths remain\" >&2"
+            "  exit 1"
+            "fi"
+          ];
+
+          installPhase = builtins.concatStringsSep "\n" [
+            "mkdir -p $out"
+            "cp -r . $out/"
+            "find $out -type f \\( -name \"*.lean\" -o -name \"lakefile.lean\" -o -name \"lakefile.toml\" -o -name \"lake-manifest.json\" -o -name \"lean-toolchain\" \\) -exec touch -h -d \"1970-01-01 00:00:00\" {} +"
+          ];
+        };
+
         # Stages the relocatable toolchain bundle before compression.
         packages.omnibus-tar = pkgs.stdenv.mkDerivation {
           pname = "anneal-toolchain-omnibus-tar";
@@ -505,6 +563,7 @@
           ];
 
           aeneasBuild = self.packages.${system}.aeneas-compiled;
+          rustModelBuild = self.packages.${system}.rust-model-compiled;
           rustToolchain = self.packages.${system}.rust-toolchain;
           leanToolchain = self.packages.${system}.lean-toolchain;
 
@@ -520,6 +579,9 @@
             "mkdir -p $TMPDIR/dist_staging/aeneas"
             "cp -r $aeneasBuild/* $TMPDIR/dist_staging/aeneas/"
             "chmod -R +w $TMPDIR/dist_staging/aeneas"
+            "mkdir -p $TMPDIR/dist_staging/rust-model"
+            "cp -r $rustModelBuild/. $TMPDIR/dist_staging/rust-model/"
+            "chmod -R +w $TMPDIR/dist_staging/rust-model"
           ] ++ pkgs.lib.optionals pkgs.stdenv.isLinux [
             # Remove Nix dynamic-linker and RPATH references from ELF binaries.
             "echo \"Cleaning up Nix store references...\""
@@ -547,6 +609,7 @@
             # workspaces can use `lake --old` against the installed archive
             # without setup-time mtime repair.
             "find $TMPDIR/dist_staging/aeneas -type f \\( -name \"*.lean\" -o -name \"lakefile.lean\" -o -name \"lakefile.toml\" -o -name \"lake-manifest.json\" -o -name \"lean-toolchain\" \\) -exec touch -h -d \"1970-01-01 00:00:00\" {} +"
+            "find $TMPDIR/dist_staging/rust-model -type f \\( -name \"*.lean\" -o -name \"lakefile.lean\" -o -name \"lakefile.toml\" -o -name \"lake-manifest.json\" -o -name \"lean-toolchain\" \\) -exec touch -h -d \"1970-01-01 00:00:00\" {} +"
             "chmod -R a-w $TMPDIR/dist_staging"
             "cd $TMPDIR/dist_staging"
             "tar -cf $out *"
@@ -602,6 +665,7 @@
             aeneas
             lean
             rust
+            rust-model
             EOF
             if ! diff -u "$TMPDIR/archive/expected-top-level" "$TMPDIR/archive/top-level"; then
               echo "ERROR: unexpected top-level archive layout" >&2
@@ -618,13 +682,25 @@
               aeneas/packages/mathlib/.lake/config/mathlib/lakefile.olean \
               lean/bin/lean \
               rust/bin/cargo \
-              rust/bin/rustc; do
+              rust/bin/rustc \
+              rust-model/lakefile.lean \
+              rust-model/.lake/build/lib/lean/Rust.olean \
+              rust-model/.lake/build/lib/lean/Rust/Layout.olean \
+              rust-model/.lake/build/lib/lean/Rust/Memory.olean \
+              rust-model/.lake/build/lib/lean/Rust/Bytes.olean \
+              rust-model/.lake/build/lib/lean/RustTests.olean \
+              rust-model/.lake/build/lib/lean/RustBytesTests.olean; do
               if ! grep -Fxq "$path" "$TMPDIR/archive/entries"; then
                 echo "ERROR: expected archive entry missing: $path" >&2
                 exit 1
               fi
             done
 
+            if ! grep -Eq '^rust-model/\.lake/config/[^/]+/lakefile\.olean$' "$TMPDIR/archive/entries"; then
+              echo "ERROR: archive is missing Rust model Lake package configuration" >&2
+              exit 1
+            fi
+
             if ! grep -Eq '^aeneas/packages/mathlib/\.lake/build/lib/lean/Mathlib/.+\.olean$' "$TMPDIR/archive/entries"; then
               echo "ERROR: archive is missing Mathlib .olean cache artifacts" >&2
               exit 1

anneal/lean/.gitignore

@@ -0,0 +1 @@
+.lake/

anneal/lean/README.md

@@ -0,0 +1,60 @@
+# Shared Rust models for Lean
+
+This Lake package contains mathematical models used by Anneal and zerocopy's
+Aeneas verification. Its modules live in the `Rust` namespace. The package
+imports Lean's standard library and has no dependency on a Rust frontend or
+Aeneas, so consumers can check the same sources with their own compatible Lean
+pins.
+
+- `Rust.Layout` describes alignment, padding, and trailing-slice sizes using
+  unbounded natural numbers.
+- `Rust.Memory` describes numerical allocation and referent bounds. These
+  structures do not themselves establish pointer provenance, ownership, or
+  permission to access memory.
+- `Rust.Bytes` gives positional little- and big-endian integer encodings,
+  including exact-length, bound, truncation, and round-trip theorems.
+
+These are models, not a claim that every Rust operation obeys them. A consumer
+must connect an operation's actual extracted implementation to its intended
+model through a checked contract. Frontend annotations, machine word carriers,
+and external Rust correspondence premises stay in that consumer. This package
+introduces no axioms about the Rust compiler or its abstract machine.
+
+## Check the package
+
+From this directory, with the pinned Lean toolchain installed:
+
+```sh
+lake build Rust RustTests RustBytesTests
+lake env lean -DwarningAsError=true RustTests.lean
+```
+
+`RustTests` and `RustBytesTests` check concrete boundary cases and use the
+universal theorems independently of any frontend. `RustTests` also audits every
+compiled library declaration, including unused helpers, and rejects assumptions
+beyond Lean's standard logical axioms. The second command reruns that audit even
+when Lake can reuse its compiled test module.
+
+## Distribution and repository use
+
+Anneal's omnibus dependency archive contains the package at `rust-model/`,
+including source and precompiled artifacts built with the archive's Lean pin.
+`cargo anneal setup` installs that archive through exocrate. Generated Anneal
+workspaces require the installed package, rather than copying its definitions
+into each frontend. Archive tests import it from a relocated, read-only
+installation.
+
+Repository consumers can use a Lake path dependency on `anneal/lean`. A
+consumer with a different compatible Lean pin recompiles these sources; it must
+not reuse artifacts compiled by another Lean version. The archive's build and
+CI cache inputs include this source tree.
+
+Until a new release archive includes this package, unpublished source checkouts
+must install a locally built omnibus archive with
+`cargo run setup --local-archive /path/to/archive.tar.zst` from `anneal/v1`.
+Use a fresh `ANNEAL_TOOLCHAIN_DIR` when replacing a previously installed archive;
+setup reuses existing installations even when the local archive changes.
+The current remote metadata points to an older archive without `rust-model/`.
+For the next release, use the existing manually dispatched Anneal release
+workflow: it builds the platform archives and prepares the version/metadata PR
+with their actual URLs and hashes before crate publication.

anneal/lean/Rust.lean

@@ -0,0 +1,19 @@
+/- 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. -/
+
+import Rust.Layout
+import Rust.Memory
+import Rust.Bytes
+
+/-!
+The public entry point for the shared mathematical library. Consumers can import
+`Rust` for layout, byte-order, and memory-geometry definitions, or import the
+individual modules when they need fewer dependencies. These imports introduce
+no assumptions about the Rust compiler, pointer validity, or a frontend's
+translation. A consumer supplies those connections in its own verification.
+-/