From eb799cb029462dc250f571b90a57f78f5082b779 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Wed, 7 Oct 2026 05:50:39 -0400 Subject: [PATCH] Share Rust mathematical models across Anneal frontends Move common layout and numerical memory geometry into an independent Lean package under anneal/lean. Add reusable integer byte-order models and prove length, bound, truncation and round-trip laws without frontend assumptions. Package sources and compiled artifacts in the existing omnibus dependency archive; import the installed package from Anneal V1 and test relocation from V2. Include these sources in archive cache inputs. Keep frontend axioms and annotation machinery in their existing consumers. Validation: independent Lean builds on 4.30.0-rc2 and 4.31.0; V1 Rust unit tests; native relocation check; formatting and workflow/script checks. Nix archive construction remains covered by the existing CI builder. Agent-authored-by: AI agent acting on joshlf's behalf gherrit-pr-id: Gluzscumtqii4zeryhevzpymev2ojqng --- .github/workflows/anneal-release.yml | 1 + .github/workflows/anneal.yml | 8 +- anneal/check-flake-eval.sh | 1 + anneal/flake.nix | 78 +++++++++++- anneal/lean/.gitignore | 1 + anneal/lean/README.md | 60 ++++++++++ anneal/lean/Rust.lean | 19 +++ anneal/lean/Rust/Bytes.lean | 172 +++++++++++++++++++++++++++ anneal/lean/Rust/Layout.lean | 111 +++++++++++++++++ anneal/lean/Rust/Memory.lean | 96 +++++++++++++++ anneal/lean/RustBytesTests.lean | 68 +++++++++++ anneal/lean/RustTests.lean | 86 ++++++++++++++ anneal/lean/lake-manifest.json | 6 + anneal/lean/lakefile.lean | 26 ++++ anneal/lean/lean-toolchain | 1 + anneal/src/main.rs | 76 ++++++++++++ anneal/src/setup.rs | 5 + anneal/v1/Cargo.lock | 140 +++++++++++++++++++++- anneal/v1/src/Anneal.lean | 99 +++++++-------- anneal/v1/src/aeneas.rs | 36 ++++-- anneal/v1/src/setup.rs | 6 + 21 files changed, 1030 insertions(+), 66 deletions(-) create mode 100644 anneal/lean/.gitignore create mode 100644 anneal/lean/README.md create mode 100644 anneal/lean/Rust.lean create mode 100644 anneal/lean/Rust/Bytes.lean create mode 100644 anneal/lean/Rust/Layout.lean create mode 100644 anneal/lean/Rust/Memory.lean create mode 100644 anneal/lean/RustBytesTests.lean create mode 100644 anneal/lean/RustTests.lean create mode 100644 anneal/lean/lake-manifest.json create mode 100644 anneal/lean/lakefile.lean create mode 100644 anneal/lean/lean-toolchain diff --git a/.github/workflows/anneal-release.yml b/.github/workflows/anneal-release.yml index 718f28e5b9..09802cd5d0 100644 --- a/.github/workflows/anneal-release.yml +++ b/.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" diff --git a/.github/workflows/anneal.yml b/.github/workflows/anneal.yml index 1754412432..e5f4e05ab0 100644 --- a/.github/workflows/anneal.yml +++ b/.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 diff --git a/anneal/check-flake-eval.sh b/anneal/check-flake-eval.sh index 5deef6e2ae..30fb8a8a47 100644 --- a/anneal/check-flake-eval.sh +++ b/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 diff --git a/anneal/flake.nix b/anneal/flake.nix index 433fcf5c64..7765a7b749 100644 --- a/anneal/flake.nix +++ b/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 diff --git a/anneal/lean/.gitignore b/anneal/lean/.gitignore new file mode 100644 index 0000000000..01f8cdb637 --- /dev/null +++ b/anneal/lean/.gitignore @@ -0,0 +1 @@ +.lake/ diff --git a/anneal/lean/README.md b/anneal/lean/README.md new file mode 100644 index 0000000000..9e3b2368ec --- /dev/null +++ b/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. diff --git a/anneal/lean/Rust.lean b/anneal/lean/Rust.lean new file mode 100644 index 0000000000..688ef4a946 --- /dev/null +++ b/anneal/lean/Rust.lean @@ -0,0 +1,19 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , 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. +-/ diff --git a/anneal/lean/Rust/Bytes.lean b/anneal/lean/Rust/Bytes.lean new file mode 100644 index 0000000000..e627cc3f94 --- /dev/null +++ b/anneal/lean/Rust/Bytes.lean @@ -0,0 +1,172 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Std.Tactic +@[expose] public section + +/-! +This module specifies integer byte order with base-256 arithmetic. A byte is an +unsigned eight-bit digit; a sequence is a `List`, whose order describes byte +positions rather than a particular memory allocation or host endianness. + +Encoding always produces the requested number of bytes. If the natural-number +input is too large, it keeps the low bits; if it is small, it supplies zero bytes +to fill the width. The two round-trip directions therefore have different +claims: decoding an encoding truncates the integer to that width, whereas +encoding a decoded sequence at its original length recovers every byte. + +These definitions and proofs do not depend on machine integer types or Aeneas. +A consumer must separately show that its Rust operations implement this byte +order, with the intended width and memory-access conditions. +-/ + +namespace Rust.Bytes + +/-- An unsigned eight-bit digit; `BitVec` already guarantees its value is below 256. -/ +abbrev Byte := BitVec 8 + +/-- +Reads little-endian digits: the head contributes units and the remainder is +multiplied by 256. For example, bytes `[0x34, 0x12]` represent `0x1234`. +-/ +def decodeLE : List Byte → Nat + | [] => 0 + | byte :: rest => byte.toNat + 256 * decodeLE rest + +/-- +Reads big-endian digits by reversing their positions before little-endian +decoding. Both byte orders can then share the same arithmetic proofs. +-/ +def decodeBE (bytes : List Byte) : Nat := decodeLE bytes.reverse + +/-- +Writes exactly `count` little-endian bytes, keeping the low `8 * count` bits of +`n`. Each step writes the current low byte and divides by 256 for the next step. +The output width, rather than the input value, controls when recursion stops. +-/ +def encodeLE : (count : Nat) → Nat → List Byte + | 0, _ => [] + | count + 1, n => BitVec.ofNat 8 n :: encodeLE count (n / 256) + +/-- Writes the same fixed-width digits as `encodeLE`, in big-endian order. -/ +def encodeBE (count n : Nat) : List Byte := (encodeLE count n).reverse + +-- Register the recursive equations as simplification rules. `rfl` checks that +-- each equation is exactly the corresponding definition; the later theorems +-- provide the length, bounds, and inverse laws consumers normally need. +@[simp] theorem decodeLE_nil : decodeLE [] = 0 := rfl + +@[simp] theorem decodeLE_cons (byte : Byte) (rest : List Byte) : + decodeLE (byte :: rest) = byte.toNat + 256 * decodeLE rest := rfl + +@[simp] theorem encodeLE_zero (n : Nat) : encodeLE 0 n = [] := rfl + +@[simp] theorem encodeLE_succ (count n : Nat) : + encodeLE (count + 1) n = BitVec.ofNat 8 n :: encodeLE count (n / 256) := rfl + +/-- Exposes the digit bound as natural-number arithmetic for the proofs below. -/ +theorem byte_lt_256 (byte : Byte) : byte.toNat < 256 := byte.isLt + +/-- The encoder preserves its requested width, including zero and leading zero bytes. -/ +@[simp] theorem length_encodeLE (count n : Nat) : (encodeLE count n).length = count := by + -- The recursive input is `n / 256`, so the induction hypothesis must work + -- for every input value, not just the original `n`. + induction count generalizing n with + | zero => rfl + | succ count ih => simp [ih] + +/-- Reversing the digits changes byte order without changing the encoded width. -/ +@[simp] theorem length_encodeBE (count n : Nat) : (encodeBE count n).length = count := by + simp [encodeBE] + +/-- +Converts the base-256 bound for `count` bytes to the bit-width bound used by +`BitVec`. This lets consumers connect these laws to fixed-width integer carriers. +-/ +theorem radix_pow_eq_two_pow (count : Nat) : 256 ^ count = 2 ^ (8 * count) := by + rw [Nat.pow_mul] + +/-- A sequence of `count` bytes always fits in an unsigned `8 * count`-bit integer. -/ +theorem decodeLE_lt (bytes : List Byte) : decodeLE bytes < 256 ^ bytes.length := by + induction bytes with + | nil => simp + | cons byte rest ih => + -- The low digit is below 256 and the remaining digits fit their shorter + -- width. After exposing one recursive step, `omega` combines these bounds. + have hb := byte_lt_256 byte + simp only [decodeLE_cons, List.length_cons, Nat.pow_succ] + omega + +/-- The representable bound depends on width, not on the order of the digits. -/ +theorem decodeBE_lt (bytes : List Byte) : decodeBE bytes < 256 ^ bytes.length := by + simpa [decodeBE] using decodeLE_lt bytes.reverse + +/-- +Writing and then reading keeps exactly the representable low bits. This law +holds even when `n` does not fit: overflow means truncation, not decoder failure. +-/ +@[simp] theorem decodeLE_encodeLE (count n : Nat) : + decodeLE (encodeLE count n) = n % 256 ^ count := by + induction count generalizing n with + | zero => simp [Nat.mod_one] + | succ count ih => + -- Split the integer into its low digit and quotient. The induction + -- hypothesis truncates the quotient; `Nat.mod_mul` combines the two pieces + -- into reduction modulo the capacity of the complete byte sequence. + simp only [encodeLE_succ, decodeLE_cons, BitVec.toNat_ofNat, ih] + change n % 256 + 256 * (n / 256 % 256 ^ count) = n % 256 ^ (count + 1) + rw [Nat.pow_succ, Nat.mul_comm (256 ^ count) 256, Nat.mod_mul] + +/-- Big-endian writing has the same truncation behavior as little-endian writing. -/ +@[simp] theorem decodeBE_encodeBE (count n : Nat) : + decodeBE (encodeBE count n) = n % 256 ^ count := by + simp [decodeBE, encodeBE] + +/-- +Writing a sequence's decoded value at its original length recovers every byte. +The width matters: it retains leading zeros that the numerical value alone +cannot distinguish. No input-size premise is needed, since each digit fits. +-/ +@[simp] theorem encodeLE_decodeLE (bytes : List Byte) : + encodeLE bytes.length (decodeLE bytes) = bytes := by + induction bytes with + | nil => rfl + | cons byte rest ih => + have hb := byte_lt_256 byte + -- Modulo 256 recovers the head byte; division by 256 recovers the decoded + -- tail. The digit bound rules out a carry from the head into that tail. + have low : BitVec.ofNat 8 (byte.toNat + 256 * decodeLE rest) = byte := by + apply BitVec.eq_of_toNat_eq + simp only [BitVec.toNat_ofNat] + change (byte.toNat + 256 * decodeLE rest) % 256 = byte.toNat + simp [Nat.mod_eq_of_lt hb] + have high : (byte.toNat + 256 * decodeLE rest) / 256 = decodeLE rest := by + rw [Nat.add_mul_div_left _ _ (by decide), Nat.div_eq_of_lt hb, Nat.zero_add] + simp only [List.length_cons, decodeLE_cons, encodeLE_succ, low, high, ih] + +/-- Reversing both sides transfers exact byte recovery to big-endian sequences. -/ +@[simp] theorem encodeBE_decodeBE (bytes : List Byte) : + encodeBE bytes.length (decodeBE bytes) = bytes := by + have h := encodeLE_decodeLE bytes.reverse + simpa [encodeBE, decodeBE] using congrArg List.reverse h + +/-- +An integer that already fits is recovered exactly. This is the specialization +used when a Rust input type guarantees the requested unsigned width. +-/ +theorem decodeLE_encodeLE_of_lt (count n : Nat) (h : n < 256 ^ count) : + decodeLE (encodeLE count n) = n := by + rw [decodeLE_encodeLE, Nat.mod_eq_of_lt h] + +/-- A representable input is also recovered exactly with big-endian encoding. -/ +theorem decodeBE_encodeBE_of_lt (count n : Nat) (h : n < 256 ^ count) : + decodeBE (encodeBE count n) = n := by + rw [decodeBE_encodeBE, Nat.mod_eq_of_lt h] + +end Rust.Bytes diff --git a/anneal/lean/Rust/Layout.lean b/anneal/lean/Rust/Layout.lean new file mode 100644 index 0000000000..a380c01ca7 --- /dev/null +++ b/anneal/lean/Rust/Layout.lean @@ -0,0 +1,111 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +import Std.Tactic + +/-! +This module describes object sizes and alignments using unbounded natural +numbers. Sharing the arithmetic lets frontends reuse the same proofs while +keeping their machine-word limits and Rust layout assumptions explicit. + +The proof fields below constrain mathematical values: for example, constructing +a `Layout` requires proving that its size is a multiple of its alignment. They +do not prove that these values describe a particular Rust type. A consumer must +establish that connection separately before using the geometry for that type. +-/ + +namespace Rust + +/-- +The numerical condition on a Rust alignment: positive and a power of two. +There is no upper bound here; a frontend supplies the limits of its target. +-/ +def IsAlignment (n : Nat) : Prop := + 0 < n ∧ ∃ (k : Nat), n = 2^k + +@[simp] theorem alignment_one : IsAlignment 1 := ⟨by decide, 0, by rfl⟩ + +/-- +The size and alignment of a complete object, including its final padding. +Requiring `align ∣ size` means placing another object immediately after this one +preserves alignment. Size zero is allowed, as it is for Rust's zero-sized types. +-/ +structure Layout where + size : Nat + align : Nat + isAlignment : IsAlignment align + sizeAligned : align ∣ size + +/-- +Rounds a byte count up to the nearest multiple of a positive alignment. + +The formula is total even for zero alignment: Lean's natural-number division by +zero returns zero, so this definition does too. That case is useful for testing +the formula's exact behavior, but is not a valid Rust alignment. The theorems +about rounding upward therefore require `0 < align` explicitly. +-/ +abbrev roundUpToAlign (val align : Nat) : Nat := + ((val + align - 1) / align) * align + +/-- Rounding to a positive alignment never makes an object smaller. -/ +theorem roundUpToAlign_ge (val align : Nat) (h : 0 < align) : + val ≤ roundUpToAlign val align := by + dsimp [roundUpToAlign] + -- Division with remainder expresses the rounded multiple in terms of the + -- original count. Since the remainder is less than `align`, the preceding + -- addition of `align - 1` prevents the multiple from falling below `val`. + have h1 : ((val + align - 1) / align) * align + (val + align - 1) % align = val + align - 1 := by + rw [Nat.mul_comm] + exact Nat.div_add_mod _ _ + have h2 : (val + align - 1) % align < align := Nat.mod_lt _ h + omega + +/-- A positive byte count rounds to at least one full alignment unit. -/ +theorem align_le_roundUpToAlign (val align : Nat) (h_val : 0 < val) (h_align : 0 < align) : + align ≤ roundUpToAlign val align := by + dsimp [roundUpToAlign] + -- Show that the quotient is at least one before multiplying by alignment. + have h_val_align : align ≤ val + align - 1 := by omega + have h_div_pos : 1 ≤ (val + align - 1) / align := Nat.div_pos h_val_align h_align + have h_mul : 1 * align ≤ ((val + align - 1) / align) * align := Nat.mul_le_mul_right align h_div_pos + omega + +/-- +The rounded size is a multiple of the supplied alignment. This algebraic fact +also holds at alignment zero, where the rounded size is zero; it does not make +zero a valid alignment. +-/ +theorem roundUpToAlign_aligned (val align : Nat) : align ∣ roundUpToAlign val align := + ⟨_, Nat.mul_comm _ _⟩ + +/-- +The static data needed to size an object ending in a dynamically sized slice. +`trailingOffset` is the start of the slice payload, `elementSize` is its stride, +and `align` is the alignment of the containing object. A zero stride is allowed. +The frontend must establish these values from the actual Rust layout. +-/ +structure SliceDstLayout where + trailingOffset : Nat + elementSize : Nat + align : Nat + isAlignment : IsAlignment align + +/-- +Adds the slice payload to its starting offset, then pads the complete object. +The count is unbounded and the calculation cannot overflow. A machine-level +sizing operation needs a separate proof of its checked or wrapping behavior. +-/ +abbrev reprCSliceDstSize (info : SliceDstLayout) (elemCount : Nat) : Nat := + roundUpToAlign (info.trailingOffset + elemCount * info.elementSize) info.align + +/-- Final padding gives an aligned complete size for every slice length. -/ +theorem reprCSliceDstSize_aligned (info : SliceDstLayout) (elemCount : Nat) : + info.align ∣ reprCSliceDstSize info elemCount := + roundUpToAlign_aligned _ _ + +end Rust diff --git a/anneal/lean/Rust/Memory.lean b/anneal/lean/Rust/Memory.lean new file mode 100644 index 0000000000..6f29babfd4 --- /dev/null +++ b/anneal/lean/Rust/Memory.lean @@ -0,0 +1,96 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +import Std.Tactic + +/-! +An allocation and a pointer's referent have different byte footprints. An +allocation bounds the available storage; a referent describes the bytes of the +object a pointer addresses. This module relates those footprints numerically. + +Addresses and sizes are unbounded `Nat` values. The structures do not establish +that storage exists, remains alive, is initialized, or may be accessed through a +particular pointer. Frontends retain those obligations, together with target +address limits and provenance. Here, an address set is a predicate `Nat → Prop`, +so the geometry needs neither a particular set representation nor a frontend. +-/ + +namespace Rust + +/-- +An allocation's base, byte size, and admitted byte addresses. Every member of +`addresses` must lie in the half-open interval `[base, base + size)`. The reverse +inclusion is not required: the predicate may describe only part of that range. +-/ +structure Allocation where + base : Nat + size : Nat + addresses : Nat → Prop + bounds : ∀ a, addresses a → base ≤ a ∧ a < base + size + +namespace Allocation + +/-- An admitted byte's offset is strictly inside the allocation's size. -/ +theorem offset_lt_size (alloc : Allocation) (a : Nat) (ha : alloc.addresses a) : + a - alloc.base < alloc.size := by + have := alloc.bounds a ha + omega + +/-- +An admitted address is not below the base. Natural-number subtraction truncates +at zero; this premise ensures subtracting the base really describes an offset. +-/ +theorem offset_non_negative (alloc : Allocation) (a : Nat) (ha : alloc.addresses a) : + alloc.base ≤ a := (alloc.bounds a ha).left + +/-- The allocation's end address is excluded from its admitted bytes. -/ +theorem address_lt_end (alloc : Allocation) (a : Nat) (ha : alloc.addresses a) : + a < alloc.base + alloc.size := (alloc.bounds a ha).right + +end Allocation + +/-- +The starting address, size, and byte footprint of an object addressed by a +pointer. Like `Allocation`, this bounds members of the footprint without +requiring every address in the range to be a member. A zero-sized referent has +no member addresses, but still has a starting address. +-/ +structure Referent where + address : Nat + size : Nat + addresses : Nat → Prop + bounds : ∀ a, addresses a → address ≤ a ∧ a < address + size + +/-- +Requires the referent's footprint to fill its entire half-open byte interval. +Together with `Referent.bounds`, this makes the predicate exactly that interval. +-/ +abbrev Referent.IsContiguous (r : Referent) : Prop := + ∀ a, r.address ≤ a ∧ a < r.address + r.size → r.addresses a + +/-- +Every referent byte belongs to the allocation, and the referent's endpoints fit +within the allocation's endpoints. These are separate requirements: inclusion +alone says nothing about the start of an empty footprint. The endpoint checks +allow a zero-sized referent at the allocation's end, without admitting a byte +there. This is a geometric condition, not permission to dereference a pointer. +-/ +abbrev FitsInAllocation (r : Referent) (a : Allocation) : Prop := + (∀ ⦃addr⦄, r.addresses addr → a.addresses addr) ∧ + a.base ≤ r.address ∧ r.address + r.size ≤ a.base + a.size + +/-- +Footprint inclusion transfers the allocation's upper bound to each referent +byte. Consumers can reuse this fact without unfolding the allocation record. +-/ +theorem FitsInAllocation.address_bounds_alloc (r : Referent) (a : Allocation) + (h : FitsInAllocation r a) (addr : Nat) (ha : r.addresses addr) : + addr < a.base + a.size := + a.address_lt_end addr (h.left ha) + +end Rust diff --git a/anneal/lean/RustBytesTests.lean b/anneal/lean/RustBytesTests.lean new file mode 100644 index 0000000000..95acffefee --- /dev/null +++ b/anneal/lean/RustBytesTests.lean @@ -0,0 +1,68 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +import Rust.Bytes + +open Rust.Bytes + +/-! +These examples pin down observable byte order, width, and truncation, then +exercise the universal laws as a consumer would. They do not extract a Rust +method or prove any memory access safe. Those connections belong to frontend +contracts; this package checks the mathematical byte operations alone. + +In these examples, `0x34#8` is an eight-bit `BitVec` literal. `by decide` asks +Lean to compute the concrete proposition and check a proof of the result. +-/ + +-- Zero-width encoding discards the input; empty sequences decode to zero. +example : encodeLE 0 65535 = [] := by decide +example : encodeBE 0 65535 = [] := by decide +example : decodeLE [] = 0 := by decide +example : decodeBE [] = 0 := by decide + +-- Distinct bytes make an accidental reversal visible. Both orders are checked +-- at the two widths used by the initial unsigned-integer consumers. +example : encodeLE 2 0x1234 = [0x34#8, 0x12#8] := by decide +example : encodeBE 2 0x1234 = [0x12#8, 0x34#8] := by decide +example : encodeLE 4 0x12345678 = [0x78#8, 0x56#8, 0x34#8, 0x12#8] := by decide +example : encodeBE 4 0x12345678 = [0x12#8, 0x34#8, 0x56#8, 0x78#8] := by decide +example : decodeLE [0x34#8, 0x12#8] = 0x1234 := by decide +example : decodeBE [0x12#8, 0x34#8] = 0x1234 := by decide + +-- Check the largest two-byte integer and the first values that overflow two +-- and four bytes. The value one checks that encoding retains the full width, +-- placing its zero bytes at the end appropriate to each byte order. +example : encodeLE 2 65535 = [255#8, 255#8] := by decide +example : encodeLE 2 65536 = [0#8, 0#8] := by decide +example : encodeBE 4 4294967296 = [0#8, 0#8, 0#8, 0#8] := by decide +example : encodeLE 4 1 = [1#8, 0#8, 0#8, 0#8] := by decide +example : encodeBE 4 1 = [0#8, 0#8, 0#8, 1#8] := by decide + +-- Use the general theorems directly, without unfolding or recomputing their +-- definitions. This checks their interfaces as well as the concrete examples. +example (count n : Nat) : decodeLE (encodeLE count n) = n % 256 ^ count := + decodeLE_encodeLE count n +example (count n : Nat) (h : n < 256 ^ count) : + decodeBE (encodeBE count n) = n := decodeBE_encodeBE_of_lt count n h +example (bytes : List Byte) : encodeBE bytes.length (decodeBE bytes) = bytes := + encodeBE_decodeBE bytes + +example (count : Nat) : 256 ^ count = 2 ^ (8 * count) := radix_pow_eq_two_pow count + +-- Expose representative proof dependencies for inspection. `RustTests` audits +-- every declaration owned by `Rust.Bytes`, so these printed names are not the +-- enforced coverage boundary. +#print axioms radix_pow_eq_two_pow +#print axioms byte_lt_256 +#print axioms decodeLE_lt +#print axioms decodeBE_lt +#print axioms decodeLE_encodeLE +#print axioms decodeBE_encodeBE +#print axioms encodeLE_decodeLE +#print axioms encodeBE_decodeBE diff --git a/anneal/lean/RustTests.lean b/anneal/lean/RustTests.lean new file mode 100644 index 0000000000..02b6f161bb --- /dev/null +++ b/anneal/lean/RustTests.lean @@ -0,0 +1,86 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +import Rust +import Lean.Util.CollectAxioms +import Lean.Elab.Command + +/-! +This module checks that the shared geometry is usable independently of a +frontend. Concrete examples exercise boundary behavior; parameterized examples +check that callers can use the universal lemmas without reproducing their proofs. +Lean checks each `example` as a theorem. `by decide` computes the small concrete +proposition and supplies a proof; it is not an unchecked runtime assertion. + +The final command audits the assumptions of every compiled library declaration. +An abstract mathematical library should not acquire a Rust correspondence axiom +merely because one frontend needs that premise for its own operations. +-/ + +-- Cover a valid minimal alignment, exact multiples, padding, and empty objects. +-- Alignment zero is deliberately tested as an input to the total formula, not +-- admitted as a Rust alignment. +example : Rust.IsAlignment 1 := Rust.alignment_one +example : Rust.IsAlignment 16 := ⟨by decide, 4, by decide⟩ +example : Rust.roundUpToAlign 0 8 = 0 := by decide +example : Rust.roundUpToAlign 9 8 = 16 := by decide +example : Rust.roundUpToAlign 16 8 = 16 := by decide +example : Rust.roundUpToAlign 9 0 = 0 := by decide +example (n a : Nat) (ha : 0 < a) : n ≤ Rust.roundUpToAlign n a := + Rust.roundUpToAlign_ge n a ha +example (a : Rust.Allocation) (addr : Nat) (h : a.addresses addr) : + addr - a.base < a.size := a.offset_lt_size addr h +example (r : Rust.Referent) (a : Rust.Allocation) (h : Rust.FitsInAllocation r a) + (addr : Nat) (ha : r.addresses addr) : addr < a.base + a.size := + Rust.FitsInAllocation.address_bounds_alloc r a h addr ha + +-- These commands make representative dependencies visible in build output. +-- The complete audit below enforces the policy, including for unused helpers. +#print axioms Rust.roundUpToAlign_ge +#print axioms Rust.Allocation.offset_lt_size +#print axioms Rust.FitsInAllocation.address_bounds_alloc + +-- Frontends can keep historical names as reducible aliases. Check that an +-- explicit unfolding through such a name still exposes the arithmetic; existing +-- proofs should not need to change their simplification lists after the move. +namespace Compatibility +abbrev roundUpToAlign := Rust.roundUpToAlign +example (v a : Nat) : roundUpToAlign v a = ((v + a - 1) / a) * a := by + simp only [roundUpToAlign] +end Compatibility + +-- `run_cmd` executes while Lean elaborates this file. Run it through +-- `lake env lean RustTests.lean` when the audit must run even if Lake could reuse +-- a previously compiled test module. +run_cmd do + let env ← Lean.getEnv + -- Select declarations by the module that defined them, not by namespace. + -- A helper outside `Rust` still belongs to this library. Keep this roster in + -- step with the library modules, and reject a missing import rather than + -- accidentally auditing only part of the package. + let libraryModules := #[`Rust, `Rust.Layout, `Rust.Memory, `Rust.Bytes] + let owners ← libraryModules.mapM fun moduleName => do + let some owner := env.getModuleIdx? moduleName + | throwError "Shared library module was not imported: {moduleName}" + pure owner + -- Permit Lean's standard logical axioms only. The transitive dependency + -- collection also catches an imported forbidden axiom used through a helper, + -- including the `sorryAx` assumption produced by an unfinished proof. + let allowed := #[`propext, `Classical.choice, `Quot.sound] + let mut audited := 0 + for (name, _) in env.constants.toList do + if let some owner := env.getModuleIdxFor? name then + if owners.contains owner then + for assumption in ← Lean.collectAxioms name do + unless allowed.contains assumption do + throwError "Shared library declaration {name} depends on forbidden axiom {assumption}" + audited := audited + 1 + -- An empty scan cannot establish that the compiled library was checked. + unless audited > 0 do + throwError "Shared library axiom audit found no declarations" + Lean.logInfo m!"Shared library axiom audit checked {audited} declarations" diff --git a/anneal/lean/lake-manifest.json b/anneal/lean/lake-manifest.json new file mode 100644 index 0000000000..a359ac4437 --- /dev/null +++ b/anneal/lean/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "rust_model", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/anneal/lean/lakefile.lean b/anneal/lean/lakefile.lean new file mode 100644 index 0000000000..f6a213b01e --- /dev/null +++ b/anneal/lean/lakefile.lean @@ -0,0 +1,26 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +import Lake +open Lake DSL + +package rust_model + +-- Normal consumers build the mathematical library. It needs only Lean's +-- standard library; frontend or Aeneas dependencies belong in the consumer. +@[default_target] +lean_lib Rust + +-- Tests are explicit targets, so importing `Rust` does not run test commands. +-- Package validation builds `Rust RustTests RustBytesTests` and reruns the +-- `RustTests.lean` axiom audit directly when cached test output might be reused. +lean_lib RustTests where + roots := #[`RustTests] + +lean_lib RustBytesTests where + roots := #[`RustBytesTests] diff --git a/anneal/lean/lean-toolchain b/anneal/lean/lean-toolchain new file mode 100644 index 0000000000..6c7e31fffe --- /dev/null +++ b/anneal/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.30.0-rc2 diff --git a/anneal/src/main.rs b/anneal/src/main.rs index b947700606..757a0a9c45 100644 --- a/anneal/src/main.rs +++ b/anneal/src/main.rs @@ -128,6 +128,17 @@ mod tests { .expect("archive Lake cache reuse test failed"); } + #[test] + fn test_archive_rust_model_dependency() { + let installation_dir = install_local_archive(); + let temp = tempfile::Builder::new() + .prefix("anneal-v2-rust-model-cache-reuse-") + .tempdir() + .expect("failed to create Rust model cache reuse tempdir"); + assert_archive_rust_model_dependency(&installation_dir, temp.path()) + .expect("archive Rust model dependency test failed"); + } + fn install_local_archive() -> PathBuf { // ASSUMPTION: The CI dependency builder downloads the Nix-built // archive artifact to this path before running v2 tests. @@ -190,6 +201,71 @@ lean_lib Generated where Ok(()) } + fn assert_archive_rust_model_dependency( + toolchain_root: &Path, + temp_root: &Path, + ) -> Result<(), Box> { + let rust_model = toolchain_root.join("rust-model"); + let lean_root = toolchain_root.join("lean"); + let workspace = temp_root.join("generated-workspace"); + + assert_no_write_bits(&rust_model)?; + fs::create_dir_all(workspace.join("generated"))?; + fs::copy(rust_model.join("lean-toolchain"), workspace.join("lean-toolchain"))?; + fs::write( + workspace.join("generated/Generated.lean"), + "import Rust.Layout\nimport Rust.Memory\nimport Rust.Bytes\n", + )?; + fs::write( + workspace.join("lakefile.lean"), + format!( + r#"import Lake +open Lake DSL + +require rust_model from "{}" + +package anneal_rust_model_test + +@[default_target] +lean_lib Generated where + srcDir := "generated" + roots := #[`Generated] +"#, + lake_string(&rust_model) + ), + )?; + let manifest = json!({ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [{ + "type": "path", + "name": "rust_model", + "dir": relative_manifest_string(&rust_model, &workspace)?, + "inherited": false, + }], + "name": "anneal_rust_model_test", + "lakeDir": ".lake", + "fixedToolchain": false, + }); + fs::write( + workspace.join("lake-manifest.json"), + format!("{}\n", serde_json::to_string_pretty(&manifest)?), + )?; + + run_lake_archive_command( + &workspace, + &lean_root, + &["--keep-toolchain", "--old", "build", "Generated"], + )?; + run_lake_archive_command( + &workspace, + &lean_root, + &["--keep-toolchain", "env", "lean", "--json", "generated/Generated.lean"], + )?; + + Ok(()) + } + fn assert_no_write_bits(root: &Path) -> Result<(), Box> { let metadata = fs::symlink_metadata(root)?; if metadata.file_type().is_symlink() { diff --git a/anneal/src/setup.rs b/anneal/src/setup.rs index 9e17911f4d..12bcbc52c7 100644 --- a/anneal/src/setup.rs +++ b/anneal/src/setup.rs @@ -54,6 +54,7 @@ impl Tool { const AENEAS_DIR: &str = "aeneas"; const RUST_SYSROOT: &str = "rust"; +const RUST_MODEL_DIR: &str = "rust-model"; const AENEAS_BIN_DIR: &str = "bin"; const RUST_BIN_DIR: &str = "bin"; const RUST_LIB_DIR: &str = "lib"; @@ -84,6 +85,10 @@ impl Toolchain { self.root.join(RUST_SYSROOT) } + pub fn rust_lean_dir(&self) -> std::path::PathBuf { + self.root.join(RUST_MODEL_DIR) + } + pub fn rust_bin(&self) -> std::path::PathBuf { self.rust_sysroot().join(RUST_BIN_DIR) } diff --git a/anneal/v1/Cargo.lock b/anneal/v1/Cargo.lock index 04bcfa1bdb..6b37bcca92 100644 --- a/anneal/v1/Cargo.lock +++ b/anneal/v1/Cargo.lock @@ -237,7 +237,7 @@ dependencies = [ "syn", "tempfile", "thiserror 2.0.18", - "toml", + "toml 0.8.23", "ui_test", "walkdir", ] @@ -621,6 +621,7 @@ dependencies = [ "sha2-const", "tar", "tempfile", + "toml_const", "ureq", "zstd", ] @@ -1087,6 +1088,49 @@ version = "2.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9b4f627cb1b25917193a259e49bdad08f671f8d9708acfd5fe0a8c1455d87220" +[[package]] +name = "phf" +version = "0.13.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c1562dc717473dbaa4c1f85a36410e03c047b2e7df7f45ee938fbef64ae7fadf" +dependencies = [ + "phf_macros", + "phf_shared", + "serde", +] + +[[package]] +name = "phf_generator" +version = "0.13.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "135ace3a761e564ec88c03a77317a7c6b80bb7f7135ef2544dbe054243b89737" +dependencies = [ + "fastrand", + "phf_shared", +] + +[[package]] +name = "phf_macros" +version = "0.13.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "812f032b54b1e759ccd5f8b6677695d5268c588701effba24601f6932f8269ef" +dependencies = [ + "phf_generator", + "phf_shared", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "phf_shared" +version = "0.13.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e57fef6bc5981e38c2ce2d63bfa546861309f875b8a75f092d1d54ae2d64f266" +dependencies = [ + "siphasher", +] + [[package]] name = "pin-project-lite" version = "0.2.17" @@ -1450,6 +1494,15 @@ dependencies = [ "serde", ] +[[package]] +name = "serde_spanned" +version = "1.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6662b5879511e06e8999a8a235d848113e942c9124f211511b16466ee2995f26" +dependencies = [ + "serde_core", +] + [[package]] name = "sha2" version = "0.10.9" @@ -1494,6 +1547,12 @@ version = "2.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bbbb5d9659141646ae647b42fe094daf6c6192d1620870b449d9557f748b2daa" +[[package]] +name = "siphasher" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "33f4fe9184a62d842c9ef383018f3306d8ba224fd9d836f56d7288308847c256" + [[package]] name = "smallvec" version = "1.15.1" @@ -1676,11 +1735,50 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "dc1beb996b9d83529a9e75c17a1686767d148d70663143c7854d8b4a09ced362" dependencies = [ "serde", - "serde_spanned", - "toml_datetime", + "serde_spanned 0.6.9", + "toml_datetime 0.6.11", "toml_edit", ] +[[package]] +name = "toml" +version = "0.9.12+spec-1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf92845e79fc2e2def6a5d828f0801e29a2f8acc037becc5ab08595c7d5e9863" +dependencies = [ + "indexmap", + "serde_core", + "serde_spanned 1.1.1", + "toml_datetime 0.7.5+spec-1.1.0", + "toml_parser", + "toml_writer", + "winnow 0.7.15", +] + +[[package]] +name = "toml_const" +version = "1.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "683e27d47b82029b5ae915b5dd80c05b2065c1c06046199900e8b2acdf531135" +dependencies = [ + "phf", + "toml 0.9.12+spec-1.1.0", + "toml_const_macros", +] + +[[package]] +name = "toml_const_macros" +version = "1.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4a0d196bfbd74f5f2a9e37f35632c7217e4c46dedaed0327a20dd1230fad9504" +dependencies = [ + "indexmap", + "proc-macro2", + "quote", + "syn", + "toml 0.9.12+spec-1.1.0", +] + [[package]] name = "toml_datetime" version = "0.6.11" @@ -1690,6 +1788,15 @@ dependencies = [ "serde", ] +[[package]] +name = "toml_datetime" +version = "0.7.5+spec-1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "92e1cfed4a3038bc5a127e35a2d360f145e1f4b971b551a2ba5fd7aedf7e1347" +dependencies = [ + "serde_core", +] + [[package]] name = "toml_edit" version = "0.22.27" @@ -1698,10 +1805,19 @@ checksum = "41fe8c660ae4257887cf66394862d21dbca4a6ddd26f04a3560410406a2f819a" dependencies = [ "indexmap", "serde", - "serde_spanned", - "toml_datetime", + "serde_spanned 0.6.9", + "toml_datetime 0.6.11", "toml_write", - "winnow", + "winnow 0.7.15", +] + +[[package]] +name = "toml_parser" +version = "1.1.3+spec-1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1d38ac1cf9b95face32296c0a3ede1fdc270627c9d9c02a7274dd6d960dc4d56" +dependencies = [ + "winnow 1.0.4", ] [[package]] @@ -1710,6 +1826,12 @@ version = "0.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5d99f8c9a7727884afe522e9bd5edbfc91a3312b36a77b5fb8926e4c31a41801" +[[package]] +name = "toml_writer" +version = "1.1.2+spec-1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7d56353a2a665ad0f41a421187180aab746c8c325620617ad883a99a1cbe66d2" + [[package]] name = "tracing" version = "0.1.44" @@ -2192,6 +2314,12 @@ dependencies = [ "memchr", ] +[[package]] +name = "winnow" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "23b97319f7b8343df12cc98938e5c3eb436064524c8d2b4e30a1d3a36eecdf81" + [[package]] name = "wit-bindgen" version = "0.51.0" diff --git a/anneal/v1/src/Anneal.lean b/anneal/v1/src/Anneal.lean index 727199a546..f5e29ce27b 100644 --- a/anneal/v1/src/Anneal.lean +++ b/anneal/v1/src/Anneal.lean @@ -1,3 +1,6 @@ +-- Shared definitions supply the unbounded mathematics. This frontend retains +-- its machine-word representations and premises about actual Rust operations. +import Rust import Aeneas.Std.Core import Aeneas.Std.WP import Aeneas.Tactic.Solver.ScalarTac @@ -155,8 +158,7 @@ macro "verify_empty_post" fnc:ident : tactic => do This reflects Rust's requirement that all layout alignments are non-zero powers of two. -/ -def IsAlignment (n : Nat) : Prop := - 0 < n ∧ ∃ (k : Nat), n = 2^k +abbrev IsAlignment := Rust.IsAlignment /-- A validated Rust alignment, bundling the value and its proof. -/ structure Alignment where @@ -168,7 +170,7 @@ structure Alignment where @[simp] theorem Alignment_isValid (a : Alignment) : IsAlignment a.val.val := a.isValid @[simp, grind .] -theorem alignment_one : IsAlignment 1 := ⟨by decide, 0, by rfl⟩ +theorem alignment_one : IsAlignment 1 := Rust.alignment_one instance : Inhabited Alignment := ⟨⟨sz 1, alignment_one⟩⟩ @@ -262,6 +264,14 @@ structure SpecLayout where align : Alignment sizeAligned : align.val.val ∣ size +/-- +Projects a specification layout into the shared unbounded geometry. The +alignment's numerical value and its proof are retained, so shared theorems apply +to the same layout. Machine bounds remain in the frontend representation. +-/ +abbrev SpecLayout.toGeometry (lay : SpecLayout) : Rust.Layout := + ⟨lay.size, lay.align.val.val, lay.align.isValid, lay.sizeAligned⟩ + /-- A valid physical memory layout for a value. @@ -416,6 +426,14 @@ structure SpecSliceDstLayout where elementSize : Nat align : Alignment +/-- +Projects the slice offset, stride, and outer alignment into shared geometry. +Sizing then uses the common natural-number formula, while this frontend keeps +the connection between a Rust type and its static layout. +-/ +abbrev SpecSliceDstLayout.toGeometry (info : SpecSliceDstLayout) : Rust.SliceDstLayout := + ⟨info.trailingOffset, info.elementSize, info.align.val.val, info.align.isValid⟩ + /-- Provides the static slice DST layout properties for a given type. @@ -431,35 +449,12 @@ class SpecSliceDstTypeLayout (α : Type) where class TrailingSlice (α : Type) where len : α → Nat -/-- Rounds `val` up to the nearest multiple of `align`. -/ -def roundUpToAlign (val align : Nat) : Nat := - ((val + align - 1) / align) * align - -/-- A theorem stating that rounding up always produces a value greater than or equal to the original value. -/ -theorem roundUpToAlign_ge (val align : Nat) (h : 0 < align) : - val ≤ roundUpToAlign val align := by - dsimp [roundUpToAlign] - have h1 : ((val + align - 1) / align) * align + (val + align - 1) % align = val + align - 1 := by - rw [Nat.mul_comm] - exact Nat.div_add_mod _ _ - have h2 : (val + align - 1) % align < align := Nat.mod_lt _ h - omega - -/-- A theorem stating that if the resulting padded value is non-zero, it must be at least the alignment. -/ -theorem align_le_roundUpToAlign (val align : Nat) (h_val : 0 < val) (h_align : 0 < align) : - align ≤ roundUpToAlign val align := by - dsimp [roundUpToAlign] - have h_val_align : align ≤ val + align - 1 := by omega - have h_div_pos : 1 ≤ (val + align - 1) / align := Nat.div_pos h_val_align h_align - have h_mul : 1 * align ≤ ((val + align - 1) / align) * align := Nat.mul_le_mul_right align h_div_pos - omega - - - - - - - +-- Keep the historical names available to specifications and unfolding proofs. +-- Reducible aliases reuse the shared definitions without adding equivalence +-- assumptions or asking callers to rewrite between two arithmetic models. +abbrev roundUpToAlign := Rust.roundUpToAlign +abbrev roundUpToAlign_ge := Rust.roundUpToAlign_ge +abbrev align_le_roundUpToAlign := Rust.align_le_roundUpToAlign /-- Computes the exact mathematical size of a `repr(C)` Slice DST instance. @@ -468,8 +463,7 @@ theorem align_le_roundUpToAlign (val align : Nat) (h_val : 0 < val) (h_align : 0 element count. It is not constrained by physical memory limits. -/ def reprCSliceDstSize (info : SpecSliceDstLayout) (elemCount : Nat) : Nat := - let unpaddedSize := info.trailingOffset + elemCount * info.elementSize - roundUpToAlign unpaddedSize info.align.val.val + Rust.reprCSliceDstSize info.toGeometry elemCount /-- A theorem stating that the unpadded size rounded up to the alignment is always @@ -477,8 +471,7 @@ def reprCSliceDstSize (info : SpecSliceDstLayout) (elemCount : Nat) : Nat := -/ theorem reprCSliceDstSize_aligned (info : SpecSliceDstLayout) (elemCount : Nat) : info.align.val.val ∣ reprCSliceDstSize info elemCount := by - dsimp [reprCSliceDstSize, roundUpToAlign] - exact ⟨_, Nat.mul_comm _ _⟩ + exact Rust.reprCSliceDstSize_aligned info.toGeometry elemCount /-- Marker trait for types that are explicitly `#[repr(C)]`. -/ class ReprC (α : Type) @@ -753,14 +746,20 @@ structure Allocation where -- For all addresses `a` in `addresses`, `a` is in the range `base .. (base + size)` bounds : ∀ a ∈ addresses, base.val ≤ a ∧ a < base.val + size.val +/-- +Projects the allocation's base, size, and address membership into unbounded +geometry. The bounds proof is retained. The frontend's signed-size and address +limits remain separate premises for the machine-level lemmas below. +-/ +abbrev Allocation.toGeometry (a : Allocation) : Rust.Allocation := + ⟨a.base.val, a.size.val, fun addr => addr ∈ a.addresses, a.bounds⟩ + namespace Allocation -- Consequence 1: `a - base` does not overflow `isize` theorem offset_le_isize_max (alloc : Allocation) (a : Nat) (ha : a ∈ alloc.addresses) : a - alloc.base.val ≤ Isize.max := by - have h_bound := alloc.bounds a ha - have h_lt : a < alloc.base.val + alloc.size.val := h_bound.right - have h_sub : a - alloc.base.val < alloc.size.val := by omega + have h_sub := Rust.Allocation.offset_lt_size alloc.toGeometry a ha have h_size : alloc.size.val ≤ Isize.max := alloc.size_le_isize_max omega @@ -769,14 +768,13 @@ theorem offset_le_isize_max (alloc : Allocation) (a : Nat) (ha : a ∈ alloc.add -- which we prove here to show the offset is well-defined mathematically). theorem offset_non_negative (alloc : Allocation) (a : Nat) (ha : a ∈ alloc.addresses) : alloc.base.val ≤ a := - (alloc.bounds a ha).left + Rust.Allocation.offset_non_negative alloc.toGeometry a ha -- Consequence 3: `base + o` will not wrap around the address space (overflow `usize`) -- `o = a - base`, so `base + o` is just `a` if `base <= a` (which we proved above). theorem address_le_usize_max (alloc : Allocation) (a : Nat) (ha : a ∈ alloc.addresses) : a ≤ Usize.max := by - have h_bound := alloc.bounds a ha - have h_lt : a < alloc.base.val + alloc.size.val := h_bound.right + have h_lt := Rust.Allocation.address_lt_end alloc.toGeometry a ha have h_max : alloc.base.val + alloc.size.val ≤ Usize.max := alloc.base_add_size_le_usize_max omega @@ -810,13 +808,21 @@ instance : Nonempty Referent := intro a h simp at h }⟩ +/-- +Projects the referent's numerical footprint into the shared geometry. This lets +containment proofs reuse the allocation model without changing this frontend's +pointer encoding or claiming new access, lifetime, or provenance guarantees. +-/ +abbrev Referent.toGeometry (r : Referent) : Rust.Referent := + ⟨r.address.val, r.size.val, fun addr => addr ∈ r.addresses, r.bounds⟩ + /-- A predicate indicating that a referent's set of addresses fills the contiguous range `[address, address + size)`. This means every address in that range belongs to the referent's addresses. -/ def Referent.IsContiguous (r : Referent) : Prop := - ∀ a, r.address.val ≤ a ∧ a < r.address.val + r.size.val → a ∈ r.addresses + Rust.Referent.IsContiguous r.toGeometry /-- A predicate indicating that a referent fits entirely within a given allocation. @@ -825,8 +831,7 @@ def Referent.IsContiguous (r : Referent) : Prop := a sub-range of the contiguous address range of the allocation. -/ def FitsInAllocation (r : Referent) (a : Allocation) : Prop := - r.addresses ⊆ a.addresses ∧ - a.base.val ≤ r.address.val ∧ r.address.val + r.size.val ≤ a.base.val + a.size.val + Rust.FitsInAllocation r.toGeometry a.toGeometry /-- A helper theorem proving that any address belonging to a referent that @@ -834,9 +839,7 @@ def FitsInAllocation (r : Referent) (a : Allocation) : Prop := -/ theorem FitsInAllocation.address_bounds_alloc (r : Referent) (a : Allocation) (h : FitsInAllocation r a) (addr : Nat) (ha : addr ∈ r.addresses) : addr < a.base.val + a.size.val := by - have h_subset := h.left - have h_addr_in_alloc := h_subset ha - exact (a.bounds _ h_addr_in_alloc).right + exact Rust.FitsInAllocation.address_bounds_alloc r.toGeometry a.toGeometry h addr ha /-- A class for types that act as pointers with a well-defined referent. diff --git a/anneal/v1/src/aeneas.rs b/anneal/v1/src/aeneas.rs index 9b4618a209..7d3fc7c0a2 100644 --- a/anneal/v1/src/aeneas.rs +++ b/anneal/v1/src/aeneas.rs @@ -281,6 +281,8 @@ require aeneas from "{}""#, path.display() ); + let rust_dep = format!(r#"require rust_model from "{}""#, toolchain.rust_lean_dir().display()); + let roots_str = lake_roots.iter().map(|r| format!("`{}", r)).collect::>().join(", "); let lakefile = format!( @@ -289,6 +291,7 @@ import Lake open Lake DSL {aeneas_dep} +{rust_dep} package anneal_verification @@ -385,7 +388,13 @@ fn generated_lake_manifest( ) })?; - let mut packages = Vec::with_capacity(aeneas_packages.len() + 1); + let rust_lean_dir = fs::canonicalize(toolchain.rust_lean_dir()).with_context(|| { + format!( + "Failed to resolve Rust Lake package directory {}", + toolchain.rust_lean_dir().display() + ) + })?; + let mut packages = Vec::with_capacity(aeneas_packages.len() + 2); let aeneas_lean_dir_manifest_path = path_to_manifest_string(&relative_manifest_path(&aeneas_lean_dir, workspace_root)?); packages.push(json!({ @@ -395,6 +404,13 @@ fn generated_lake_manifest( "inherited": false, })); + packages.push(json!({ + "type": "path", + "name": "rust_model", + "dir": path_to_manifest_string(&relative_manifest_path(&rust_lean_dir, workspace_root)?), + "inherited": false, + })); + for entry in aeneas_packages { let mut entry = entry .as_object() @@ -991,6 +1007,8 @@ mod tests { let workspace_root = temp.path().join("workspace/target/anneal/hash/lean"); let toolchain_root = temp.path().join("toolchain"); let aeneas_lean = toolchain_root.join("aeneas/backends/lean"); + let rust_lean = toolchain_root.join("rust-model"); + std::fs::create_dir_all(&rust_lean).unwrap(); let mathlib = toolchain_root.join("aeneas/packages/mathlib"); let qq = toolchain_root.join("aeneas/packages/Qq"); std::fs::create_dir_all(workspace_root.parent().unwrap()).unwrap(); @@ -1035,18 +1053,22 @@ mod tests { // is renamed into place. std::fs::create_dir_all(&workspace_root).unwrap(); - assert_eq!(packages.len(), 3); + assert_eq!(packages.len(), 4); assert_eq!(packages[0]["name"], "aeneas"); assert_manifest_dir_resolves(&workspace_root, &packages[0], &aeneas_lean); assert_eq!(packages[0]["inherited"], false); - assert_eq!(packages[1]["name"], "mathlib"); - assert_manifest_dir_resolves(&workspace_root, &packages[1], &mathlib); - assert_eq!(packages[1]["inherited"], true); + assert_eq!(packages[1]["name"], "rust_model"); + assert_manifest_dir_resolves(&workspace_root, &packages[1], &rust_lean); + assert_eq!(packages[1]["inherited"], false); - assert_eq!(packages[2]["name"], "Qq"); - assert_manifest_dir_resolves(&workspace_root, &packages[2], &qq); + assert_eq!(packages[2]["name"], "mathlib"); + assert_manifest_dir_resolves(&workspace_root, &packages[2], &mathlib); assert_eq!(packages[2]["inherited"], true); + + assert_eq!(packages[3]["name"], "Qq"); + assert_manifest_dir_resolves(&workspace_root, &packages[3], &qq); + assert_eq!(packages[3]["inherited"], true); } fn assert_manifest_dir_resolves(workspace_root: &Path, entry: &Value, expected: &Path) { diff --git a/anneal/v1/src/setup.rs b/anneal/v1/src/setup.rs index 32216cedf1..e79881d19c 100644 --- a/anneal/v1/src/setup.rs +++ b/anneal/v1/src/setup.rs @@ -44,6 +44,7 @@ const BIN_DIR: &str = "bin"; const LIB_DIR: &str = "lib"; const LEAN_SYSROOT: &str = "lean"; const RUST_SYSROOT: &str = "rust"; +const RUST_LEAN_DIR: &str = "rust-model"; pub struct Toolchain { pub root: PathBuf, @@ -77,6 +78,10 @@ impl Toolchain { self.aeneas_root().join(AENEAS_BACKENDS_DIR).join(AENEAS_LEAN_DIR) } + pub fn rust_lean_dir(&self) -> PathBuf { + self.root.join(RUST_LEAN_DIR) + } + pub fn rust_sysroot(&self) -> PathBuf { self.root.join(RUST_SYSROOT) } @@ -194,6 +199,7 @@ mod tests { fn tool_paths_use_omnibus_layout() { let toolchain = Toolchain { root: PathBuf::from("/tmp/toolchain") }; + assert_eq!(toolchain.rust_lean_dir(), PathBuf::from("/tmp/toolchain/rust-model")); assert_eq!(toolchain.bin_dir(), PathBuf::from("/tmp/toolchain/aeneas/bin")); assert_eq!( toolchain.aeneas_lean_dir(),