diff --git a/.github/workflows/anneal.yml b/.github/workflows/anneal.yml index ce076ec5bf..7b6a72cf79 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@d0c908e6cbe9f89f36ed8205a3ab6f092636916a # v3.23.1 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 6c9f389b9a..efeed1846c 100644 --- a/anneal/flake.nix +++ b/anneal/flake.nix @@ -557,6 +557,106 @@ ]; }; + # Build the pure Rust semantics and its Aeneas companion against the + # archive's already-compiled backend and shared Mathlib dependencies. + packages.rust-model-compiled = pkgs.stdenv.mkDerivation { + pname = "anneal-rust-model-compiled"; + version = "0.1.0"; + + src = ./lean; + leanToolchain = self.packages.${system}.lean-toolchain; + compiledAeneas = self.packages.${system}.aeneas-compiled; + + 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\"" + "export MATHLIB_NO_CACHE_ON_UPDATE=1" + # Lake's --old mode requires compiled files to be newer than + # their sources. Nix normalizes both to the same timestamp, so a + # direct dependency on the store output would rebuild its caches. + # Stage a private copy with older inputs, as the final archive does, + # then freeze it. Never write to the authoritative backend output. + "mkdir -p $TMPDIR/bundle" + "cp -r $compiledAeneas $TMPDIR/bundle/aeneas" + "chmod -R +w $TMPDIR/bundle/aeneas" + "find $TMPDIR/bundle/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\" {} +" + "chmod -R a-w $TMPDIR/bundle/aeneas" + "cp -r . $TMPDIR/bundle/rust-model" + "cd $TMPDIR/bundle/rust-model" + # Keep the shared source package pin aligned with this archive's Lean. + "grep -Fxq 'leanprover/lean4:${leanVersion}' lean-toolchain" + (runLeanCommand "lake --old build Rust RustTests RustBytesTests RustStorageTests RustPointerTests") + (runLeanCommand "lake env lean -DwarningAsError=true RustTests.lean") + # Seed normal Lake path dependencies from the backend's manifest. + # os.path operations are lexical: resolving the bundle symlink + # would embed Nix store paths in the companion's manifest. + "python3 - <<'PY'" + "import json, os" + "backend = os.path.abspath('../aeneas/backends/lean')" + "companion = os.path.abspath('aeneas')" + "with open(os.path.join(backend, 'lake-manifest.json')) as source:" + " manifest = json.load(source)" + "manifest['name'] = 'rust_model_aeneas'" + "for dep in manifest['packages']:" + " assert dep['type'] == 'path', dep" + " dep['dir'] = os.path.relpath(os.path.join(backend, dep['dir']), companion)" + " dep['inherited'] = True" + "manifest['packages'] += [" + " dict(type='path', name='rust_model', dir='..', inherited=False)," + " dict(type='path', name='aeneas', dir='../../aeneas/backends/lean', inherited=False)," + "]" + "with open('aeneas/lake-manifest.json', 'w') as target:" + " json.dump(manifest, target, indent=2)" + " target.write('\\n')" + "PY" + "(cd aeneas && ${runLeanCommand "lake --old build RustAeneas RustAeneasTests"})" + "(cd aeneas && ${runLeanCommand "lake env lean -DwarningAsError=true RustAeneasTests.lean"})" + # A fresh verification workspace loads both packages as dependencies. + # 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 RustAeneas\\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@\"" + "require rust_model_aeneas from \"@RUST_MODEL_ROOT@/aeneas\"" + "require aeneas from \"@AENEAS_ROOT@/backends/lean\"" + "" + "package anneal_verification" + "" + "@[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\" --replace-fail @AENEAS_ROOT@ \"$TMPDIR/bundle/aeneas\"" + "(cd $TMPDIR/rust-model-config-primer && ${runLeanCommand "lake --old build Generated"})" + "test -n \"\$(find .lake/config -type f -name lakefile.olean -print)\"" + "test -n \"\$(find aeneas/.lake/config -type f -name lakefile.olean -print)\"" + "mkdir -p $TMPDIR/empty-packages" + # Restrict rewriting to our writable model tree. In particular, + # never walk compiledAeneas or its shared dependency packages. + "python3 ${./rewrite-lake-vendor.py} --root . --packages-dir $TMPDIR/empty-packages --rewrite-traces --trace-prefix \"$compiledAeneas=aeneas\" --trace-prefix \"$TMPDIR/bundle/aeneas=aeneas\" --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 $TMPDIR/bundle/rust-model/. $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"; @@ -572,6 +672,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; @@ -587,6 +688,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...\"" @@ -614,6 +718,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 *" @@ -669,6 +774,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 @@ -684,19 +790,46 @@ aeneas/packages/mathlib/lake-manifest.json \ lean/bin/lean \ rust/bin/cargo \ - rust/bin/rustc; do + rust/bin/rustc \ + rust-model/lakefile.lean \ + rust-model/lake-manifest.json \ + rust-model/aeneas/lakefile.lean \ + rust-model/aeneas/lake-manifest.json \ + rust-model/Rust/Arithmetic.lean \ + rust-model/Rust/Pointer.lean \ + rust-model/RustPointerTests.lean \ + rust-model/.lake/build/lib/lean/Rust/Arithmetic.olean \ + rust-model/aeneas/RustAeneas.lean \ + rust-model/aeneas/RustAeneas/Machine.lean \ + rust-model/aeneas/RustAeneas/Bytes.lean \ + rust-model/aeneas/.lake/build/lib/lean/RustAeneas.olean \ + rust-model/aeneas/.lake/build/lib/lean/RustAeneas/Machine.olean \ + rust-model/aeneas/.lake/build/lib/lean/RustAeneas/Bytes.olean \ + rust-model/aeneas/.lake/build/lib/lean/RustAeneasTests.olean \ + 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/Pointer.olean \ + rust-model/.lake/build/lib/lean/Rust/Bytes.olean \ + rust-model/.lake/build/lib/lean/Rust/Storage.olean \ + rust-model/.lake/build/lib/lean/RustTests.olean \ + rust-model/.lake/build/lib/lean/RustBytesTests.olean \ + rust-model/.lake/build/lib/lean/RustStorageTests.olean \ + rust-model/.lake/build/lib/lean/RustPointerTests.olean; do if ! grep -Fxq "$path" "$TMPDIR/archive/entries"; then echo "ERROR: expected archive entry missing: $path" >&2 exit 1 fi done - # Lean 4.31 stores dependency configurations under numbered - # directories at the workspace root. - if ! grep -Eq '^aeneas/backends/lean/\.lake/config/[^/]+/lakefile\.olean$' "$TMPDIR/archive/entries"; then - echo "ERROR: archive is missing the Aeneas Lake package configuration" >&2 - exit 1 - fi + # Lean 4.31 caches dependency configurations in the workspace + # root, rather than under each dependency package. + for package_root in aeneas/backends/lean rust-model rust-model/aeneas; do + if ! grep -Eq "^$package_root/\\.lake/config/[^/]+/lakefile\\.olean$" "$TMPDIR/archive/entries"; then + echo "ERROR: archive is missing Lake package configuration for $package_root" >&2 + exit 1 + fi + done 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 diff --git a/anneal/lean/.gitignore b/anneal/lean/.gitignore new file mode 100644 index 0000000000..6879ec19c1 --- /dev/null +++ b/anneal/lean/.gitignore @@ -0,0 +1,5 @@ +.lake/ +# Lake writes the companion's local dependency paths and inherits our Lean pin. +# The archive builder regenerates both files for the installed package. +aeneas/lake-manifest.json +aeneas/lean-toolchain diff --git a/anneal/lean/README.md b/anneal/lean/README.md new file mode 100644 index 0000000000..0fce80a921 --- /dev/null +++ b/anneal/lean/README.md @@ -0,0 +1,112 @@ +# 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.Pointer` describes raw pointer values with a numerical address, opaque + optional provenance, and unit or count metadata. Its casts preserve exact + provenance; non-nullness and provenance presence confer no access permission. + It has no pointer byte encoding or dereference operation. +- `Rust.Bytes` gives positional little- and big-endian integer encodings, + including exact-length, bound, truncation, and round-trip theorems. +- `Rust.Storage` distinguishes initialized bytes from uninitialized bytes and + composes fixed-width and metadata-indexed decoders. Its array theorem + transfers initialization from element representations to their concatenation, + including zero-sized elements. It does not model runtime storage or typed-copy + events. +- `Rust.Arithmetic` proves natural-number padding and round-down laws. + +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. + +The nested `aeneas/` Lake package adds `RustAeneas.Machine` for bounded +`Usize` layouts, allocations, and referents. It depends on this pure package +and on the same Aeneas backend used by the consumer. Its `Rust.Machine` +namespace contains proved conversions to the pure geometry. Its +`RustAeneas.Bytes` module proves that Aeneas bit-vector byte operations agree +with `Rust.Bytes`. Anneal V1 keeps +its historical `Anneal` names as compatibility aliases and retains frontend +classes, ABI premises, and raw-pointer premises in V1. The companion has its +own declaration-level axiom audit; it does not expand the pure package's +permitted assumptions. + +The storage constructors preserve the distinction between physical decoding and +library invariants. `integerDecoder` selects a width and byte order; `map` and +`filterMap` add value interpretation and language-level validity checks while +preserving initialization. `emptyDecoder` requires an explicit inhabitant. A +zero-byte layout alone cannot construct an uninhabited type, and physical +decoding of a stateful token cannot establish its library invariant. Consumers +must check that invariant separately when composing bytes-to-model decoding. +`RustAeneas.Storage` supplies the corresponding signed and unsigned machine +carriers without assuming that alignment equals byte width. + +`StorageDecoder` accepts metadata separately from the byte list. Its checked +`run` requires both the correct width and agreement with the decoded value's +metadata. This matters for zero-sized slices and padded layouts: several +metadata values can describe the same byte width. Fixed `BitDecoder` values +adapt through unit metadata without changing their accepted representations. + +Initialization and mathematical admission remain separate obligations. +`Initialized` covers every accepted physical representation. `CompleteWith` +requires every initialized representation of the requested width to admit both +a physical value and a value through the supplied mathematical decoder. +`cast_complete` composes those laws at equal widths for arbitrary represented +bytes. It does not establish that a particular Rust cast or transmutation uses +this interpretation; that connection remains the consumer's obligation. + +## Check the package + +From this directory, with the pinned Lean toolchain installed: + +```sh +lake build Rust RustTests RustBytesTests RustStorageTests RustPointerTests +lake env lean -DwarningAsError=true RustTests.lean +``` + +`RustTests`, `RustBytesTests`, `RustStorageTests`, and `RustPointerTests` 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. + +With the matching Aeneas backend installed, the nested package builds +`RustAeneas` and `RustAeneasTests`. Its Lake option `aeneasPath` selects that +existing backend for source builds. In the omnibus archive, its default +`../../aeneas/backends/lean` resolves to the bundled backend. No separate +Aeneas version is selected by the companion. + +## 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..8ad93c4955 --- /dev/null +++ b/anneal/lean/Rust.lean @@ -0,0 +1,22 @@ +/- 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.Pointer +import Rust.Bytes +import Rust.Storage +import Rust.Arithmetic + +/-! +The public entry point for the shared mathematical library. Consumers can import +`Rust` for layout, arithmetic, byte order, memory geometry, and raw pointer +values, or import 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/Arithmetic.lean b/anneal/lean/Rust/Arithmetic.lean new file mode 100644 index 0000000000..09a5be3e7f --- /dev/null +++ b/anneal/lean/Rust/Arithmetic.lean @@ -0,0 +1,84 @@ +/- 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 + +/-! +Natural-number alignment facts, independent of machine words and backends. +Bounded-word implementations can use these laws after separately proving their +numerical results. A positive alignment and exact padding or round-down result +are explicit hypotheses; these laws add no Rust or machine-layout assumptions. +-/ + +namespace Rust.Arithmetic + +/-- The unique bounded padding that makes the sum divisible by alignment. -/ +theorem padding_unique (len align p : Nat) (hpos : 0 < align) + (hlt : p < align) (haligned : (len + p) % align = 0) : + p = (align - len % align) % align := by + have hr := Nat.mod_lt len hpos + have hsum : (len % align + p) % align = 0 := by + rw [Nat.add_mod, Nat.mod_eq_of_lt hlt] at haligned + exact haligned + by_cases hzero : len % align = 0 + · simpa only [hzero, Nat.zero_add, Nat.mod_eq_of_lt hlt, + Nat.sub_zero, Nat.mod_self] using hsum + · have hge : align ≤ len % align + p := by + by_cases h : align ≤ len % align + p + · exact h + · rw [Nat.mod_eq_of_lt (by omega)] at hsum + omega + rw [Nat.mod_eq_sub_mod hge, Nat.mod_eq_of_lt (by omega)] at hsum + rw [Nat.mod_eq_of_lt (by omega)] + omega + +/-- Exact padding also gives minimality and the zero-padding criterion. -/ +theorem padding_properties (len align p : Nat) (hpos : 0 < align) + (hlt : p < align) (haligned : (len + p) % align = 0) : + p = (align - len % align) % align ∧ + (∀ q : Nat, (len + q) % align = 0 → p ≤ q) ∧ + (p = 0 ↔ len % align = 0) := by + refine ⟨padding_unique len align p hpos hlt haligned, ?_, ?_⟩ + · intro q hq + have hqm : (len + q % align) % align = 0 := by + rw [Nat.add_mod] at hq + rw [Nat.add_mod, Nat.mod_mod] + exact hq + have heq := padding_unique len align (q % align) hpos + (Nat.mod_lt q hpos) hqm + have hp := padding_unique len align p hpos hlt haligned + have := Nat.mod_le q align + omega + · constructor + · intro hp + simpa only [hp, Nat.add_zero] using haligned + · intro hl + have hp := padding_unique len align p hpos hlt haligned + simpa only [hl, Nat.sub_zero, Nat.mod_self] using hp + +/-- An exact round-down result is aligned and the greatest such lower bound. -/ +theorem round_down_properties (n align m : Nat) (hpos : 0 < align) + (hm : m = n - n % align) : + m ≤ n ∧ m % align = 0 ∧ n < m + align ∧ + (∀ q : Nat, q ≤ n → q % align = 0 → q ≤ m) := by + have hr := Nat.mod_lt n hpos + have hrle := Nat.mod_le n align + have hmul : m = (n / align) * align := by + rw [Nat.div_mul_self_eq_mod_sub_self, hm] + refine ⟨by omega, ?_, by omega, ?_⟩ + · rw [hmul, Nat.mul_mod_left] + · intro q hqn hqa + have hdiv := Nat.div_le_div_right (c := align) hqn + have hle := Nat.mul_le_mul_right align hdiv + rw [Nat.div_mul_self_eq_mod_sub_self, Nat.div_mul_self_eq_mod_sub_self, + hqa, Nat.sub_zero, ← hm] at hle + exact hle + +end Rust.Arithmetic diff --git a/anneal/lean/Rust/Bytes.lean b/anneal/lean/Rust/Bytes.lean new file mode 100644 index 0000000000..9c390cdf95 --- /dev/null +++ b/anneal/lean/Rust/Bytes.lean @@ -0,0 +1,205 @@ +/- 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 + +/-- Byte order is an explicit input, independent of the host running Lean. -/ +inductive Endian where + | little + | big + deriving DecidableEq, Repr + +/-- Read digits in the requested byte order. -/ +def decode (endian : Endian) (bytes : List Byte) : Nat := + match endian with + | .little => decodeLE bytes + | .big => decodeBE bytes + +/-- +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 + +/-- Both byte orders obey the same bound, determined by the number of bytes. -/ +theorem decode_lt (endian : Endian) (bytes : List Byte) : + decode endian bytes < 2 ^ (8 * bytes.length) := by + rw [← radix_pow_eq_two_pow] + cases endian with + | little => exact decodeLE_lt bytes + | big => exact decodeBE_lt bytes + +/-- Reading zero digits produces zero in either byte order and at every width. -/ +@[simp] theorem decode_replicate_zero (endian : Endian) (count : Nat) : + decode endian (List.replicate count 0) = 0 := by + have little : decodeLE (List.replicate count 0) = 0 := by + induction count with + | zero => rfl + | succ count ih => + rw [List.replicate_succ, decodeLE_cons, ih] + rfl + cases endian with + | little => exact little + | big => simpa only [decode, decodeBE, List.reverse_replicate] using little + +/-- +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/Rust/Pointer.lean b/anneal/lean/Rust/Pointer.lean new file mode 100644 index 0000000000..a85d6c187f --- /dev/null +++ b/anneal/lean/Rust/Pointer.lean @@ -0,0 +1,148 @@ +/- 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 + +/-! +Resource-free raw pointer values. Provenance is an opaque parameter, not an +address, permission, allocation witness, or encoding in physical bytes. Merely +having provenance says nothing about whether memory may be accessed. Addresses +and slice counts use unbounded naturals; consumers must establish their target +word bounds when relating these values to Rust. + +`cast` covers only raw pointer casts preserving both address and metadata (thin +casts, or compatible wide casts). `withMetadata` models slice-pointer assembly +from a thin data pointer and a count; it does not construct a reference. +`nonNull` checks just the nonzero address and provides no access permission. + +Rust correspondence remains a consumer obligation. Relevant documented +premises are the Rust Reference's pointer-to-pointer cast rules, `ptr::cast`, +`ptr::slice_from_raw_parts`, and `NonNull::new`: +https://doc.rust-lang.org/reference/expressions/operator-expr.html#pointer-to-pointer-cast +https://doc.rust-lang.org/std/primitive.pointer.html#method.cast +https://doc.rust-lang.org/std/ptr/fn.slice_from_raw_parts.html +https://doc.rust-lang.org/std/ptr/struct.NonNull.html#method.new +These links identify premises to check for the consumer's version and scope; +they introduce no axioms here. There is no byte encoder, dereference, allocation, +mutation, liveness, or borrow operation in this module. +-/ + +namespace Rust.Pointer + +/-- A raw pointer value, independent of the state of any referent. -/ +structure Value (Provenance : Type u) (Metadata : Type v) where + address : Nat + provenance : Option Provenance + metadata : Metadata + +abbrev Thin (Provenance : Type u) := Value Provenance Unit +abbrev Slice (Provenance : Type u) := Value Provenance Nat + +/-- An address-and-metadata-preserving cast changes only the Rust pointee type, +which is deliberately absent from this resource-free carrier. -/ +def cast (pointer : Value Provenance Metadata) : Value Provenance Metadata := pointer + +/-- Assemble metadata without acquiring permission or changing provenance. -/ +def withMetadata (data : Thin Provenance) (metadata : Metadata) : + Value Provenance Metadata := ⟨data.address, data.provenance, metadata⟩ + +/-- Extract the thin data pointer, discarding only metadata. -/ +def dataPointer (pointer : Value Provenance Metadata) : Thin Provenance := + ⟨pointer.address, pointer.provenance, ()⟩ + +/-- Extract metadata without examining provenance. -/ +def metadata (pointer : Value Provenance Metadata) : Metadata := pointer.metadata + +/-- Provenance presence is a value property, not an access permission. -/ +def hasProvenance (pointer : Value Provenance Metadata) : Prop := + pointer.provenance.isSome = true + +/-- Identify the opaque token without claiming what access it permits. -/ +def Carries (pointer : Value Provenance Metadata) (token : Provenance) : Prop := + pointer.provenance = some token + +/-- Preservation includes absence and retains the same token when present. +The operation may change metadata without changing provenance. -/ +def PreservesProvenance (before : Value Provenance BeforeMetadata) + (after : Value Provenance AfterMetadata) : Prop := + after.provenance = before.provenance + +/-- Raw pointer equality observes address and metadata, independently of the +opaque provenance. This is distinct from Lean equality of the entire carrier. -/ +def equal (left right : Value Provenance Metadata) : Prop := + left.address = right.address ∧ left.metadata = right.metadata + +instance [DecidableEq Metadata] (left right : Value Provenance Metadata) : + Decidable (equal left right) := by + unfold equal + infer_instance + +/-- Non-nullness alone does not imply alignment, validity, or dereferenceability. -/ +abbrev NonNull (Provenance : Type u) (Metadata : Type v) := + { pointer : Value Provenance Metadata // pointer.address ≠ 0 } + +def nonNull (pointer : Value Provenance Metadata) : Option (NonNull Provenance Metadata) := + if h : pointer.address = 0 then none else some ⟨pointer, h⟩ + +@[simp] theorem cast_eq (pointer : Value Provenance Metadata) : cast pointer = pointer := rfl + +theorem cast_preservesProvenance (pointer : Value Provenance Metadata) : + PreservesProvenance pointer (cast pointer) := rfl + +theorem withMetadata_preservesProvenance (data : Thin Provenance) (m : Metadata) : + PreservesProvenance data (withMetadata data m) := rfl + +theorem dataPointer_preservesProvenance (pointer : Value Provenance Metadata) : + PreservesProvenance pointer (dataPointer pointer) := rfl + +@[simp] theorem withMetadata_provenance (data : Thin Provenance) (m : Metadata) : + (withMetadata data m).provenance = data.provenance := rfl + +@[simp] theorem metadata_withMetadata (data : Thin Provenance) (m : Metadata) : + metadata (withMetadata data m) = m := rfl + +@[simp] theorem dataPointer_withMetadata (data : Thin Provenance) (m : Metadata) : + dataPointer (withMetadata data m) = data := by + cases data + rfl + +@[simp] theorem withMetadata_dataPointer (pointer : Value Provenance Metadata) : + withMetadata (dataPointer pointer) (metadata pointer) = pointer := by + cases pointer + rfl + +@[simp] theorem nonNull_eq_none_iff (pointer : Value Provenance Metadata) : + nonNull pointer = none ↔ pointer.address = 0 := by + simp [nonNull] + +/-- The successful guard returns the exact pointer, including opaque provenance. -/ +theorem nonNull_eq_some_iff (pointer : Value Provenance Metadata) + (result : NonNull Provenance Metadata) : + nonNull pointer = some result ↔ result.val = pointer := by + by_cases h : pointer.address = 0 + · simp [nonNull, h] + intro eq + exact result.property ((congrArg Value.address eq).trans h) + · simp only [nonNull, h, ↓reduceDIte, Option.some.injEq] + constructor + · intro eq + exact (congrArg Subtype.val eq).symm + · intro eq + exact Subtype.ext eq.symm + +@[simp] theorem equal_refl (pointer : Value Provenance Metadata) : equal pointer pointer := + ⟨rfl, rfl⟩ + +/-- Equal Rust pointer values may have different provenance. No equality test +or decision procedure for the opaque provenance parameter is required. -/ +theorem equal_ignores_provenance (address : Nat) (m : Metadata) + (left right : Option Provenance) : + equal (⟨address, left, m⟩ : Value Provenance Metadata) ⟨address, right, m⟩ := + ⟨rfl, rfl⟩ + +end Rust.Pointer diff --git a/anneal/lean/Rust/Storage.lean b/anneal/lean/Rust/Storage.lean new file mode 100644 index 0000000000..2994183b2e --- /dev/null +++ b/anneal/lean/Rust/Storage.lean @@ -0,0 +1,601 @@ +/- 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 Rust.Bytes +@[expose] public section + +/-! +This module describes numeric byte initialization and fixed-size or metadata-indexed +decoding as pure values. Numeric bytes do not encode pointer provenance. +A successful decoder run must have the specified width. Initialization is a +separate law: a decoder may accept uninitialized bytes, but then cannot satisfy +`BitDecoder.Initialized`. + +Array decoding applies the element decoder to consecutive, equal-size chunks. +Recursion counts elements, so zero-length arrays and zero-sized elements need no +special size arithmetic. For a Rust array interpretation, the consumer must +justify the Rust Reference layout bridge: array size is `n * size(T)`, alignment +is that of `T`, and element `k` starts at `k * size(T)`, with no inter-element +padding. Element padding is initialized only when the element's law proves it. +These mathematical laws alone do not prove a physical Rust implementation. +-/ + +namespace Rust.Storage + +/-- An abstract-machine byte may lack an initialized value. -/ +inductive AMByte where + | uninit + | init (byte : Rust.Bytes.Byte) + deriving DecidableEq, Repr + +/-- Every byte has an initialized value, including any element padding. -/ +def Initialized (bytes : List AMByte) : Prop := + ∀ byte ∈ bytes, ∃ value, byte = AMByte.init value + +@[simp] theorem initialized_nil : Initialized [] := by + simp [Initialized] + +@[simp] theorem initialized_cons (byte : AMByte) (bytes : List AMByte) : + Initialized (byte :: bytes) ↔ (∃ value, byte = AMByte.init value) ∧ Initialized bytes := by + simp [Initialized] + +@[simp] theorem initialized_append (left right : List AMByte) : + Initialized (left ++ right) ↔ Initialized left ∧ Initialized right := by + simp [Initialized, or_imp, forall_and] + +/-- Collect byte values, rejecting the entire representation if any byte is uninitialized. -/ +def collectInitialized : List AMByte → Option (List Rust.Bytes.Byte) + | [] => some [] + | AMByte.uninit :: _ => none + | AMByte.init byte :: rest => (collectInitialized rest).map (byte :: ·) + +/-- Collection loses neither positions nor byte values. -/ +theorem collectInitialized_eq_some_iff (bytes : List AMByte) (values : List Rust.Bytes.Byte) : + collectInitialized bytes = some values ↔ bytes = values.map AMByte.init := by + induction bytes generalizing values with + | nil => cases values <;> simp [collectInitialized] + | cons byte rest ih => + cases byte with + | uninit => cases values <;> simp [collectInitialized] + | init byte => + cases values with + | nil => simp [collectInitialized] + | cons value values => + cases h : collectInitialized rest with + | none => simp [collectInitialized, ← ih, h] + | some tail => simp [collectInitialized, ← ih, h] + +@[simp] theorem collectInitialized_map (values : List Rust.Bytes.Byte) : + collectInitialized (values.map AMByte.init) = some values := + (collectInitialized_eq_some_iff _ _).mpr rfl + +theorem collectInitialized_length (bytes : List AMByte) (values : List Rust.Bytes.Byte) + (h : collectInitialized bytes = some values) : values.length = bytes.length := by + rw [(collectInitialized_eq_some_iff _ _).mp h, List.length_map] + +/-- Exactly the fully initialized representations can be collected. -/ +theorem collectInitialized_complete (bytes : List AMByte) : + (∃ values, collectInitialized bytes = some values) ↔ Initialized bytes := by + induction bytes with + | nil => simp [collectInitialized] + | cons byte rest ih => + cases byte with + | uninit => simp [collectInitialized] + | init byte => + simp only [initialized_cons, AMByte.init.injEq, exists_eq', true_and] + constructor + · rintro ⟨values, h⟩ + cases tail : collectInitialized rest with + | none => simp [collectInitialized, tail] at h + | some values => exact ih.mp ⟨values, tail⟩ + · intro initialized + obtain ⟨values, h⟩ := ih.mpr initialized + exact ⟨byte :: values, by simp [collectInitialized, h]⟩ + +/-- Decoding behavior and its fixed representation width; validity laws are separate. -/ +structure BitDecoder (Raw : Type u) where + byteSize : Nat + decode : List AMByte → Option Raw + +namespace BitDecoder + +/-- Reject a width mismatch before invoking the decoder. -/ +def run (decoder : BitDecoder Raw) (bytes : List AMByte) : Option Raw := + if bytes.length = decoder.byteSize then decoder.decode bytes else none + +/-- Successful decoding requires every representation byte to be initialized. -/ +def Initialized (decoder : BitDecoder Raw) : Prop := + ∀ bytes raw, decoder.run bytes = some raw → Rust.Storage.Initialized bytes + +/-- Every successful run has the decoder's specified width. -/ +theorem run_length (decoder : BitDecoder Raw) (bytes : List AMByte) (raw : Raw) + (h : decoder.run bytes = some raw) : bytes.length = decoder.byteSize := by + by_cases width : bytes.length = decoder.byteSize + · exact width + · simp [run, width] at h + +/-- Width mismatches fail even if `decode` itself would accept them. -/ +theorem run_eq_none_of_length_ne (decoder : BitDecoder Raw) (bytes : List AMByte) + (h : bytes.length ≠ decoder.byteSize) : decoder.run bytes = none := by + simp [run, h] + +/-- Change decoded values while retaining the same accepted byte representations. -/ +def map (decoder : BitDecoder Raw) (f : Raw → Other) : BitDecoder Other where + byteSize := decoder.byteSize + decode bytes := (decoder.decode bytes).map f + +@[simp] theorem run_map (decoder : BitDecoder Raw) (f : Raw → Other) (bytes : List AMByte) : + (decoder.map f).run bytes = (decoder.run bytes).map f := by + simp only [map, run] + split <;> rfl + +/-- Mapping decoded values preserves the initialization law. -/ +theorem map_initialized (decoder : BitDecoder Raw) (f : Raw → Other) + (h : decoder.Initialized) : (decoder.map f).Initialized := by + intro bytes raw accepted + rw [run_map] at accepted + cases result : decoder.run bytes with + | none => simp [result] at accepted + | some value => exact h bytes value result + +/-- A validity check may reject a decoded value, while preserving outer decoding failures. -/ +def filterMap (decoder : BitDecoder Raw) (f : Raw → Option Other) : BitDecoder Other where + byteSize := decoder.byteSize + decode bytes := (decoder.decode bytes).bind f + +@[simp] theorem run_filterMap (decoder : BitDecoder Raw) (f : Raw → Option Other) + (bytes : List AMByte) : + (decoder.filterMap f).run bytes = (decoder.run bytes).bind f := by + simp only [filterMap, run] + split <;> rfl + +/-- Rejecting some values cannot introduce representations with uninitialized bytes. -/ +theorem filterMap_initialized (decoder : BitDecoder Raw) (f : Raw → Option Other) + (h : decoder.Initialized) : (decoder.filterMap f).Initialized := by + intro bytes raw accepted + rw [run_filterMap] at accepted + cases result : decoder.run bytes with + | none => simp [result] at accepted + | some value => exact h bytes value result + +end BitDecoder + +/-- Decode every fully initialized integer representation at an explicit width and byte order. +The carrier is unsigned bits; signed and restricted values use value adapters. Width and +endianness are mathematical inputs, whose correspondence to Rust needs separate evidence. -/ +def integerDecoder (byteSize : Nat) (endian : Rust.Bytes.Endian) : + BitDecoder (BitVec (8 * byteSize)) where + byteSize := byteSize + decode bytes := (collectInitialized bytes).map (fun values => + BitVec.ofNat (8 * byteSize) (Rust.Bytes.decode endian values)) + +theorem integerDecoder_initialized (byteSize : Nat) (endian : Rust.Bytes.Endian) : + (integerDecoder byteSize endian).Initialized := by + intro bytes word accepted + have width := BitDecoder.run_length _ _ _ accepted + simp only [BitDecoder.run, width, ↓reduceIte, integerDecoder] at accepted + cases collected : collectInitialized bytes with + | none => simp [collected] at accepted + | some values => exact (collectInitialized_complete bytes).mp ⟨values, collected⟩ + +/-- Every initialized representation of the specified width has an integer value. -/ +theorem integerDecoder_complete (byteSize : Nat) (endian : Rust.Bytes.Endian) + (bytes : List AMByte) (width : bytes.length = byteSize) (initialized : Initialized bytes) : + ∃ word, (integerDecoder byteSize endian).run bytes = some word := by + obtain ⟨values, collected⟩ := (collectInitialized_complete bytes).mpr initialized + exact ⟨BitVec.ofNat (8 * byteSize) (Rust.Bytes.decode endian values), + by simp [BitDecoder.run, integerDecoder, width, collected]⟩ + +/-- Once the width guard holds, integer decoding preserves the exact digit value. +The byte bound proves that the fixed-width carrier does not truncate that value. -/ +theorem integerDecoder_run_map (byteSize : Nat) (endian : Rust.Bytes.Endian) + (values : List Rust.Bytes.Byte) (width : values.length = byteSize) : + (integerDecoder byteSize endian).run (values.map AMByte.init) = + some (BitVec.ofNat (8 * byteSize) (Rust.Bytes.decode endian values)) := by + simp [BitDecoder.run, integerDecoder, width] + +theorem integerDecoder_value (byteSize : Nat) (endian : Rust.Bytes.Endian) + (values : List Rust.Bytes.Byte) (width : values.length = byteSize) : + (BitVec.ofNat (8 * byteSize) (Rust.Bytes.decode endian values)).toNat = + Rust.Bytes.decode endian values := by + have bound := Rust.Bytes.decode_lt endian values + rw [width] at bound + exact Nat.mod_eq_of_lt bound + +@[simp] theorem integerDecoder_run_zeros (byteSize : Nat) (endian : Rust.Bytes.Endian) : + (integerDecoder byteSize endian).run (List.replicate byteSize (AMByte.init 0)) = + some (0 : BitVec (8 * byteSize)) := by + have h := integerDecoder_run_map byteSize endian (List.replicate byteSize 0) (by simp) + rw [Rust.Bytes.decode_replicate_zero] at h + simpa only [List.map_replicate, BitVec.ofNat_eq_ofNat] using h + +/-- A zero-byte representation requires an explicit value. Size zero or an `Inhabited` +instance alone does not justify a Rust value or any state that its validity requires. -/ +def emptyDecoder (value : Raw) : BitDecoder Raw where + byteSize := 0 + decode + | [] => some value + | _ => none + +@[simp] theorem emptyDecoder_run_nil (value : Raw) : (emptyDecoder value).run [] = some value := rfl + +theorem emptyDecoder_initialized (value : Raw) : (emptyDecoder value).Initialized := by + intro bytes raw accepted + have width := BitDecoder.run_length _ _ _ accepted + have empty : bytes = [] := List.length_eq_zero_iff.mp width + simp [empty] + +/-- The supplied value makes empty storage complete; no representation bytes create it. -/ +theorem emptyDecoder_complete (value : Raw) (bytes : List AMByte) + (width : bytes.length = 0) : (emptyDecoder value).run bytes = some value := by + have empty := List.length_eq_zero_iff.mp width + simp [empty] + +/-- Rust booleans accept exactly the initialized bytes zero and one. -/ +def boolDecoder : BitDecoder Bool where + byteSize := 1 + decode + | [AMByte.init byte] => + if byte = 0 then some false else if byte = 1 then some true else none + | _ => none + +/-- Every initialized eight-bit value is a valid byte. -/ +def byteDecoder : BitDecoder Rust.Bytes.Byte where + byteSize := 1 + decode + | [AMByte.init byte] => some byte + | _ => none + +/-- Unit occupies no bytes. -/ +def unitDecoder : BitDecoder Unit := emptyDecoder () + +theorem boolDecoder_initialized : boolDecoder.Initialized := by + intro bytes raw h + have width := BitDecoder.run_length boolDecoder bytes raw h + cases bytes with + | nil => simp [boolDecoder] at width + | cons byte bytes => + cases bytes with + | cons _ _ => simp [boolDecoder] at width + | nil => + cases byte with + | uninit => simp [BitDecoder.run, boolDecoder] at h + | init value => simp [Initialized] + +theorem byteDecoder_initialized : byteDecoder.Initialized := by + intro bytes raw h + have width := BitDecoder.run_length byteDecoder bytes raw h + cases bytes with + | nil => simp [byteDecoder] at width + | cons byte bytes => + cases bytes with + | cons _ _ => simp [byteDecoder] at width + | nil => + cases byte with + | uninit => simp [BitDecoder.run, byteDecoder] at h + | init value => simp [Initialized] + +/-- Every initialized one-byte representation has a byte value. -/ +theorem byteDecoder_complete (bytes : List AMByte) (width : bytes.length = 1) + (initialized : Initialized bytes) : ∃ byte, byteDecoder.run bytes = some byte := by + cases bytes with + | nil => simp at width + | cons byte bytes => + cases bytes with + | cons _ _ => simp at width + | nil => + cases byte with + | uninit => simp [Initialized] at initialized + | init byte => exact ⟨byte, rfl⟩ + +theorem unitDecoder_initialized : unitDecoder.Initialized := by + intro bytes raw h + have width := BitDecoder.run_length unitDecoder bytes raw h + have empty : bytes = [] := List.length_eq_zero_iff.mp width + simp [empty] + +@[simp] theorem boolDecoder_run_zero : boolDecoder.run [AMByte.init 0] = some false := by + decide + +@[simp] theorem boolDecoder_run_one : boolDecoder.run [AMByte.init 1] = some true := by + decide + +@[simp] theorem boolDecoder_run_two : boolDecoder.run [AMByte.init 2] = none := by + decide + +@[simp] theorem boolDecoder_run_uninit : boolDecoder.run [AMByte.uninit] = none := by + decide + +@[simp] theorem byteDecoder_run_init (byte : Rust.Bytes.Byte) : + byteDecoder.run [AMByte.init byte] = some byte := by + simp [BitDecoder.run, byteDecoder] + +@[simp] theorem byteDecoder_run_uninit : byteDecoder.run [AMByte.uninit] = none := by + decide + +@[simp] theorem unitDecoder_run_nil : unitDecoder.run [] = some () := by + decide + +/-- Consume exactly `n` chunks, requiring the final remainder to be empty. -/ +def arrayDecode (element : BitDecoder Raw) : + (n : Nat) → List AMByte → Option { values : List Raw // values.length = n } + | 0, bytes => if bytes = [] then some ⟨[], rfl⟩ else none + | n + 1, bytes => do + let value ← element.run (bytes.take element.byteSize) + let values ← arrayDecode element n (bytes.drop element.byteSize) + return ⟨value :: values.val, by simp [values.property]⟩ + +/-- Decode an array from contiguous element representations. -/ +def arrayDecoder (element : BitDecoder Raw) (n : Nat) : + BitDecoder { values : List Raw // values.length = n } where + byteSize := n * element.byteSize + decode := arrayDecode element n + +theorem arrayDecode_initialized (element : BitDecoder Raw) + (he : element.Initialized) (n : Nat) (bytes : List AMByte) + (values : { values : List Raw // values.length = n }) + (h : arrayDecode element n bytes = some values) : Initialized bytes := by + induction n generalizing bytes with + | zero => + simp only [arrayDecode] at h + split at h + · rename_i empty + simp [empty] + · contradiction + | succ n ih => + simp only [arrayDecode] at h + cases first : element.run (bytes.take element.byteSize) with + | none => simp [first] at h + | some value => + cases rest : arrayDecode element n (bytes.drop element.byteSize) with + | none => simp [first, rest] at h + | some tail => + have head_initialized := he _ _ first + have tail_initialized := ih _ tail rest + have both : Initialized (bytes.take element.byteSize ++ bytes.drop element.byteSize) := + (initialized_append _ _).mpr ⟨head_initialized, tail_initialized⟩ + simpa using both + +/-- Arrays inherit initialization from the accepted element representations. -/ +theorem arrayDecoder_initialized (element : BitDecoder Raw) + (he : element.Initialized) (n : Nat) : (arrayDecoder element n).Initialized := by + intro bytes values h + have width := BitDecoder.run_length (arrayDecoder element n) bytes values h + simp only [BitDecoder.run, width, ↓reduceIte, arrayDecoder] at h + exact arrayDecode_initialized element he n bytes values h + +/-- A successful array run consumes exactly its total representation width. -/ +theorem arrayDecoder_run_length (element : BitDecoder Raw) (n : Nat) + (bytes : List AMByte) (values : { values : List Raw // values.length = n }) + (h : (arrayDecoder element n).run bytes = some values) : + bytes.length = n * element.byteSize := + BitDecoder.run_length (arrayDecoder element n) bytes values h + +/-- The decoder's output carries the required number of elements. -/ +theorem arrayDecoder_output_length (element : BitDecoder Raw) (n : Nat) + (bytes : List AMByte) (values : { values : List Raw // values.length = n }) + (_h : (arrayDecoder element n).run bytes = some values) : values.val.length = n := + values.property + +/-- Fixed array completeness follows from completeness of every element. +Only fully initialized inputs are covered; the proof never fills missing bytes. -/ +theorem arrayDecoder_complete (element : BitDecoder Raw) + (complete : ∀ bytes, bytes.length = element.byteSize → Initialized bytes → + ∃ raw, element.run bytes = some raw) + (n : Nat) (bytes : List AMByte) (width : bytes.length = n * element.byteSize) + (initialized : Initialized bytes) : ∃ values, (arrayDecoder element n).run bytes = some values := by + induction n generalizing bytes with + | zero => + have empty : bytes = [] := List.length_eq_zero_iff.mp (by simpa using width) + subst bytes + exact ⟨⟨[], rfl⟩, by simp [BitDecoder.run, arrayDecoder, arrayDecode]⟩ + | succ n ih => + have sizeBound : element.byteSize ≤ bytes.length := by + rw [Nat.succ_mul] at width + omega + have headWidth : (bytes.take element.byteSize).length = element.byteSize := by + simp [List.length_take, Nat.min_eq_left sizeBound] + have tailWidth : (bytes.drop element.byteSize).length = n * element.byteSize := by + simp only [List.length_drop] + rw [Nat.succ_mul] at width + omega + have both : Initialized (bytes.take element.byteSize ++ bytes.drop element.byteSize) := by + simpa using initialized + obtain ⟨head, acceptedHead⟩ := complete _ headWidth ((initialized_append _ _).mp both).1 + obtain ⟨tail, acceptedTail⟩ := ih _ tailWidth ((initialized_append _ _).mp both).2 + have tailDecode : arrayDecode element n (bytes.drop element.byteSize) = some tail := by + simpa [BitDecoder.run, arrayDecoder, tailWidth] using acceptedTail + exact ⟨⟨head :: tail.val, by simp [tail.property]⟩, + by + simp only [BitDecoder.run, arrayDecoder] + rw [if_pos width] + simp only [arrayDecode, acceptedHead, tailDecode] + rfl⟩ + +/-- A physical decoder at explicit metadata. `metadata` observes the decoded raw +value; `run` checks that observation against the requested metadata. Size need +not identify metadata: zero-sized slices and padded layouts may share a width. +These numeric bytes do not represent pointer provenance or pointer validity. -/ +structure StorageDecoder (Metadata : Type v) (Raw : Type u) where + byteSize : Metadata → Nat + metadata : Raw → Metadata + decode : Metadata → List AMByte → Option Raw + +namespace StorageDecoder + +/-- Width and returned metadata are checked before a decoded value is exposed. -/ +def run [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (metadata : Metadata) (bytes : List AMByte) : Option Raw := + if bytes.length = decoder.byteSize metadata then do + let raw ← decoder.decode metadata bytes + if decoder.metadata raw = metadata then some raw else none + else none + +/-- The complete successful-run contract, including the underlying decode. -/ +theorem run_eq_some_iff [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (metadata : Metadata) (bytes : List AMByte) (raw : Raw) : + decoder.run metadata bytes = some raw ↔ + bytes.length = decoder.byteSize metadata ∧ + decoder.decode metadata bytes = some raw ∧ decoder.metadata raw = metadata := by + by_cases width : bytes.length = decoder.byteSize metadata + · cases decoded : decoder.decode metadata bytes with + | none => simp [run, width, decoded] + | some value => + by_cases agrees : decoder.metadata value = metadata + · simp [run, width, decoded, agrees] + intro equality + subst raw + exact agrees + · simp [run, width, decoded, agrees] + intro equality + subst raw + exact agrees + · simp [run, width] + +/-- Accepted representations have exactly the requested layout size. -/ +theorem run_length [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (metadata : Metadata) (bytes : List AMByte) (raw : Raw) + (accepted : decoder.run metadata bytes = some raw) : + bytes.length = decoder.byteSize metadata := + ((decoder.run_eq_some_iff metadata bytes raw).mp accepted).1 + +/-- Returned metadata cannot disagree even when widths coincide. -/ +theorem run_metadata [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (metadata : Metadata) (bytes : List AMByte) (raw : Raw) + (accepted : decoder.run metadata bytes = some raw) : decoder.metadata raw = metadata := + ((decoder.run_eq_some_iff metadata bytes raw).mp accepted).2.2 + +/-- Every language-valid representation is initialized, independently of any +mathematical decoder. This is the representation obligation used by IntoBytes. -/ +def Initialized [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) : Prop := + ∀ metadata bytes raw, decoder.run metadata bytes = some raw → Rust.Storage.Initialized bytes + +/-- Compose language validity with a mathematical decoder, retaining both failures. -/ +def runWith [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (decodeModel : Raw → Option Model) (metadata : Metadata) (bytes : List AMByte) : Option Model := + (decoder.run metadata bytes).bind decodeModel + +theorem runWith_eq_some_iff [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (decodeModel : Raw → Option Model) (metadata : Metadata) (bytes : List AMByte) (value : Model) : + decoder.runWith decodeModel metadata bytes = some value ↔ + ∃ raw, decoder.run metadata bytes = some raw ∧ decodeModel raw = some value := by + cases decoded : decoder.run metadata bytes <;> simp [runWith, decoded] + +/-- Every initialized representation of the requested width admits both a +language value and a mathematical value. This is stronger than language-only +completeness; supplying it does not establish the other FromBytes clauses. -/ +def CompleteWith [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (decodeModel : Raw → Option Model) : Prop := + ∀ metadata bytes, bytes.length = decoder.byteSize metadata → Rust.Storage.Initialized bytes → + ∃ value, decoder.runWith decodeModel metadata bytes = some value + +theorem completeWith_iff [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (decodeModel : Raw → Option Model) : decoder.CompleteWith decodeModel ↔ + ∀ metadata bytes, bytes.length = decoder.byteSize metadata → Rust.Storage.Initialized bytes → + ∃ raw value, decoder.run metadata bytes = some raw ∧ decodeModel raw = some value := by + simp only [CompleteWith, runWith_eq_some_iff] + constructor + · intro h metadata bytes width initialized + obtain ⟨value, raw, language, model⟩ := h metadata bytes width initialized + exact ⟨raw, value, language, model⟩ + · intro h metadata bytes width initialized + obtain ⟨raw, value, language, model⟩ := h metadata bytes width initialized + exact ⟨value, raw, language, model⟩ + +/-- Owned byte-cast admission over an arbitrary represented byte list. Source +initialization and destination completeness compose at equal requested widths; +no source encoder or physical Rust transmute correspondence is assumed. -/ +theorem cast_complete [DecidableEq SourceMetadata] [DecidableEq Metadata] + (source : StorageDecoder SourceMetadata SourceRaw) (destination : StorageDecoder Metadata Raw) + (decodeModel : Raw → Option Model) (sourceInitialized : source.Initialized) + (destinationComplete : destination.CompleteWith decodeModel) + (sourceMetadata : SourceMetadata) (metadata : Metadata) (bytes : List AMByte) (raw : SourceRaw) + (accepted : source.run sourceMetadata bytes = some raw) + (sameWidth : source.byteSize sourceMetadata = destination.byteSize metadata) : + ∃ value, destination.runWith decodeModel metadata bytes = some value := + destinationComplete metadata bytes + ((source.run_length sourceMetadata bytes raw accepted).trans sameWidth) + (sourceInitialized sourceMetadata bytes raw accepted) + +/-- Adapt raw values while explicitly preserving their metadata observation. -/ +def map (decoder : StorageDecoder Metadata Raw) (f : Raw → Other) + (metadataOther : Other → Metadata) + (_preserves : ∀ raw, metadataOther (f raw) = decoder.metadata raw) : StorageDecoder Metadata Other where + byteSize := decoder.byteSize + metadata := metadataOther + decode metadata bytes := (decoder.decode metadata bytes).map f + +@[simp] theorem run_map [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (f : Raw → Other) (metadataOther : Other → Metadata) + (preserves : ∀ raw, metadataOther (f raw) = decoder.metadata raw) + (metadata : Metadata) (bytes : List AMByte) : + (decoder.map f metadataOther preserves).run metadata bytes = + (decoder.run metadata bytes).map f := by + unfold run map + split + · cases decoded : decoder.decode metadata bytes <;> simp [decoded, preserves] + · rfl + +theorem map_initialized [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (f : Raw → Other) (metadataOther : Other → Metadata) + (preserves : ∀ raw, metadataOther (f raw) = decoder.metadata raw) + (initialized : decoder.Initialized) : (decoder.map f metadataOther preserves).Initialized := by + intro metadata bytes value accepted + rw [run_map] at accepted + cases language : decoder.run metadata bytes with + | none => simp [language] at accepted + | some raw => exact initialized metadata bytes raw language + +end StorageDecoder + +/-- Fixed-width decoding is the Unit-metadata case, with no metadata inferred +from bytes. The compatibility API uses the same width guard and validity domain. -/ +def BitDecoder.asStorageDecoder (decoder : BitDecoder Raw) : StorageDecoder Unit Raw where + byteSize _ := decoder.byteSize + metadata _ := () + decode _ := decoder.decode + +@[simp] theorem BitDecoder.run_asStorageDecoder (decoder : BitDecoder Raw) (bytes : List AMByte) : + decoder.asStorageDecoder.run () bytes = decoder.run bytes := by + simp only [asStorageDecoder, StorageDecoder.run, run] + split + · cases decoder.decode bytes <;> rfl + · rfl + +theorem BitDecoder.asStorageDecoder_initialized (decoder : BitDecoder Raw) + (initialized : decoder.Initialized) : decoder.asStorageDecoder.Initialized := by + intro metadata bytes raw accepted + cases metadata + exact initialized bytes raw (by simpa using accepted) + +/-- A slice's element count is explicit metadata. Chunk decoding reuses array +recursion, including for zero-sized elements, and returns the same count. -/ +def sliceDecoder (element : BitDecoder Raw) : StorageDecoder Nat (List Raw) where + byteSize count := count * element.byteSize + metadata := List.length + decode count bytes := (arrayDecode element count bytes).map Subtype.val + +@[simp] theorem sliceDecoder_run (element : BitDecoder Raw) (count : Nat) (bytes : List AMByte) : + (sliceDecoder element).run count bytes = ((arrayDecoder element count).run bytes).map Subtype.val := by + simp only [StorageDecoder.run, sliceDecoder, BitDecoder.run, arrayDecoder] + split + · cases decoded : arrayDecode element count bytes with + | none => rfl + | some values => simp [values.property] + · rfl + +theorem sliceDecoder_initialized (element : BitDecoder Raw) (initialized : element.Initialized) : + (sliceDecoder element).Initialized := by + intro count bytes raw accepted + rw [sliceDecoder_run] at accepted + cases language : (arrayDecoder element count).run bytes with + | none => simp [language] at accepted + | some values => exact arrayDecoder_initialized element initialized count bytes values language + +end Rust.Storage 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/RustPointerTests.lean b/anneal/lean/RustPointerTests.lean new file mode 100644 index 0000000000..f3ae2ca6d9 --- /dev/null +++ b/anneal/lean/RustPointerTests.lean @@ -0,0 +1,39 @@ +/- 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.Pointer + +open Rust.Pointer + +-- The laws quantify over an opaque provenance type, with no equality instance. +example {P : Type} (p : Value P Nat) : (cast p).provenance = p.provenance := rfl +example {P : Type} (p : Thin P) (count : Nat) : + dataPointer (withMetadata p count) = p := dataPointer_withMetadata p count +example {P : Type} (p : Value P Nat) : + withMetadata (dataPointer p) (metadata p) = p := withMetadata_dataPointer p + +-- Count zero and unbounded mathematical counts are valid raw value inputs. +example : metadata (withMetadata (⟨0, none, ()⟩ : Thin Nat) 0) = 0 := rfl +example : metadata (withMetadata (⟨1, some 7, ()⟩ : Thin Nat) (2^128)) = 2^128 := rfl + +-- Provenance presence, non-nullness, and pointer equality are independent. +example : hasProvenance (⟨0, some 7, ()⟩ : Thin Nat) := rfl +example : nonNull (⟨0, some 7, ()⟩ : Thin Nat) = none := by + exact (nonNull_eq_none_iff _).mpr rfl +example : ∃ result, nonNull (⟨1, none, ()⟩ : Thin Nat) = some result := by + exact ⟨⟨⟨1, none, ()⟩, by decide⟩, rfl⟩ +example : equal (⟨42, some 1, 3⟩ : Slice Nat) ⟨42, some 2, 3⟩ := + equal_ignores_provenance _ _ _ _ +example : ¬ equal (⟨42, some 1, 3⟩ : Slice Nat) ⟨42, some 1, 4⟩ := by + decide +example : ¬ equal (⟨42, some 1, 3⟩ : Slice Nat) ⟨43, some 1, 3⟩ := by + decide + +example {P M : Type} (p : Value P M) (r : NonNull P M) + (success : nonNull p = some r) : r.val.provenance = p.provenance := by + rw [(nonNull_eq_some_iff p r).mp success] diff --git a/anneal/lean/RustStorageTests.lean b/anneal/lean/RustStorageTests.lean new file mode 100644 index 0000000000..43637a1c88 --- /dev/null +++ b/anneal/lean/RustStorageTests.lean @@ -0,0 +1,267 @@ +/- 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 +import Rust.Storage + +namespace Rust.Storage.Tests + +-- Nonempty arrays preserve element order and byte values. +example : (arrayDecoder boolDecoder 3).run + [AMByte.init 0, AMByte.init 1, AMByte.init 0] = + some ⟨[false, true, false], rfl⟩ := by decide + +example : (arrayDecoder byteDecoder 3).run + [AMByte.init 0, AMByte.init 2, AMByte.init 255] = + some ⟨[0, 2, 255], rfl⟩ := by decide + +-- Empty arrays accept no representation bytes, regardless of the element width. +example : (arrayDecoder boolDecoder 0).run [] = some ⟨[], rfl⟩ := by decide +example : (arrayDecoder byteDecoder 0).run [] = some ⟨[], rfl⟩ := by decide +example : (arrayDecoder unitDecoder 0).run [] = some ⟨[], rfl⟩ := by decide +example : (arrayDecoder boolDecoder 0).run [AMByte.init 0] = none := by decide + +-- Positive counts of zero-sized elements decode empty chunks repeatedly. +example : (arrayDecoder unitDecoder 3).run [] = some ⟨[(), (), ()], rfl⟩ := by decide +example : (arrayDecoder unitDecoder 3).run [AMByte.init 0] = none := by decide +example : (arrayDecoder unitDecoder 3).decode [AMByte.init 0] = none := by decide + +-- The outer width guard rejects both extra and short representations. +example : (arrayDecoder boolDecoder 2).run + [AMByte.init 0, AMByte.init 1, AMByte.init 0] = none := by decide +example : (arrayDecoder boolDecoder 2).run [AMByte.init 0] = none := by decide + +-- The recursive decoder also enforces the final remainder and each chunk's width. +example : (arrayDecoder boolDecoder 2).decode + [AMByte.init 0, AMByte.init 1, AMByte.init 0] = none := by decide +example : (arrayDecoder boolDecoder 2).decode [AMByte.init 0] = none := by decide + +-- A failure in a later element propagates despite earlier success. +example : (arrayDecoder boolDecoder 2).run [AMByte.init 0, AMByte.init 2] = none := by decide +example : (arrayDecoder boolDecoder 2).run [AMByte.init 1, AMByte.uninit] = none := by decide +example : (arrayDecoder byteDecoder 2).run [AMByte.init 255, AMByte.uninit] = none := by decide + +-- Initialization is inherited only when an element law is supplied. +example : (arrayDecoder boolDecoder 3).Initialized := + arrayDecoder_initialized boolDecoder boolDecoder_initialized 3 +example : (arrayDecoder byteDecoder 3).Initialized := + arrayDecoder_initialized byteDecoder byteDecoder_initialized 3 +example : (arrayDecoder unitDecoder 3).Initialized := + arrayDecoder_initialized unitDecoder unitDecoder_initialized 3 + +-- A decoder may accept an uninitialized byte, but cannot claim the law. +def badDecoder : BitDecoder Unit where + byteSize := 1 + decode _ := some () + +example : badDecoder.run [AMByte.uninit] = some () := by decide +example : ¬ badDecoder.Initialized := by + intro h + have impossible := h [AMByte.uninit] () (by decide) + simp [Initialized] at impossible + +-- The width guard remains effective for deliberately permissive decoders. +example : badDecoder.run [] = none := by decide +example : badDecoder.run [AMByte.uninit, AMByte.uninit] = none := by decide + +-- Mapping values retains byte width and initialization for an adapter. +example : (byteDecoder.map (fun byte => byte.toNat)).run [AMByte.init 255] = some 255 := by decide +example : (byteDecoder.map (fun byte => byte.toNat)).Initialized := + BitDecoder.map_initialized byteDecoder _ byteDecoder_initialized + +-- Integer width and byte order are explicit; the same decoder covers all widths. +example : (integerDecoder 2 .little).run [AMByte.init 0x34, AMByte.init 0x12] = + some 0x1234 := by decide +example : (integerDecoder 2 .big).run [AMByte.init 0x34, AMByte.init 0x12] = + some 0x3412 := by decide +example : (integerDecoder 16 .little).run (List.replicate 16 (AMByte.init 255)) = + some (BitVec.ofNat 128 (2 ^ 128 - 1)) := by decide +example : (integerDecoder 2 .little).run [AMByte.init 0] = none := by decide +example : (integerDecoder 2 .big).run [AMByte.init 0, AMByte.init 0, AMByte.init 0] = + none := by decide +example : (integerDecoder 2 .little).run [AMByte.init 0, AMByte.uninit] = none := by decide +example : (integerDecoder 2 .big).run [AMByte.uninit, AMByte.init 255] = none := by decide +example (count : Nat) (endian : Rust.Bytes.Endian) : + (integerDecoder count endian).Initialized := integerDecoder_initialized count endian +example (count : Nat) (endian : Rust.Bytes.Endian) : + (integerDecoder count endian).run (List.replicate count (AMByte.init 0)) = some 0 := + integerDecoder_run_zeros count endian +example (count : Nat) (endian : Rust.Bytes.Endian) (bytes : List AMByte) + (width : bytes.length = count) (initialized : Initialized bytes) : + ∃ word, (integerDecoder count endian).run bytes = some word := + integerDecoder_complete count endian bytes width initialized + +-- A restricted value uses partial mapping; zero remains rejected by that restriction. +def nonzeroWord (word : BitVec 16) : Option { value : BitVec 16 // value ≠ 0 } := + if zero : word = 0 then none else some ⟨word, zero⟩ + +example : ((integerDecoder 2 .little).filterMap nonzeroWord).run + [AMByte.init 0, AMByte.init 0] = none := by decide +example : ((integerDecoder 2 .little).filterMap nonzeroWord).run + [AMByte.init 1, AMByte.init 0] = some ⟨1, by decide⟩ := by decide +example : ((integerDecoder 2 .little).filterMap nonzeroWord).Initialized := + BitDecoder.filterMap_initialized _ _ (integerDecoder_initialized _ _) + +-- For optional nonzero values, zero is a successful decode of the inner `none`. +example : ((integerDecoder 2 .little).map nonzeroWord).run + [AMByte.init 0, AMByte.init 0] = some none := by decide +example : ((integerDecoder 2 .little).map nonzeroWord).run + [AMByte.init 1, AMByte.init 0] = some (some ⟨1, by decide⟩) := by decide +example : ((integerDecoder 2 .little).map nonzeroWord).run + [AMByte.init 0, AMByte.uninit] = none := by decide +example : ((integerDecoder 2 .little).map nonzeroWord).Initialized := + BitDecoder.map_initialized _ _ (integerDecoder_initialized _ _) + +-- A general decoder may accept uninitialized padding after a valid payload. +def paddedByteDecoder : BitDecoder Rust.Bytes.Byte where + byteSize := 2 + decode + | [AMByte.init value, _] => some value + | _ => none + +example : paddedByteDecoder.run [AMByte.init 42, AMByte.uninit] = some 42 := by decide +example : ¬ paddedByteDecoder.Initialized := by + intro initialized + have impossible := initialized _ _ (by decide : + paddedByteDecoder.run [AMByte.init 42, AMByte.uninit] = some 42) + simp [Initialized] at impossible + +-- Empty storage cannot produce a value of an uninhabited type. +inductive Void : Type + +def voidDecoder : BitDecoder Void where + byteSize := 0 + decode _ := none + +example (decoder : BitDecoder Void) (bytes : List AMByte) : decoder.run bytes = none := by + cases result : decoder.run bytes with + | none => rfl + | some value => cases value + +example : voidDecoder.run [] = none := rfl +example : (arrayDecoder voidDecoder 0).run [] = some ⟨[], rfl⟩ := rfl +example : (arrayDecoder voidDecoder 1).run [] = none := by decide + +-- A state-dependent zero-byte type needs evidence of its state even though Unit is inhabited. +def statefulZstDecoder (live : Bool) : BitDecoder { _value : Unit // live = true } where + byteSize := 0 + decode bytes := if valid : live = true then (emptyDecoder ⟨(), valid⟩).decode bytes else none + +example : (statefulZstDecoder true).run [] = some ⟨(), rfl⟩ := by decide +example : (statefulZstDecoder false).run [] = none := by decide +example : (arrayDecoder (statefulZstDecoder false) 0).run [] = some ⟨[], rfl⟩ := by decide +example : (arrayDecoder (statefulZstDecoder false) 1).run [] = none := by decide +example : (emptyDecoder false).run [] = some false := rfl +example : (emptyDecoder false).run [AMByte.uninit] = none := by decide + +#print axioms integerDecoder_initialized +#print axioms integerDecoder_complete +#print axioms integerDecoder_value +#print axioms integerDecoder_run_zeros +#print axioms BitDecoder.filterMap_initialized +#print axioms emptyDecoder_initialized + +#print axioms arrayDecoder_initialized +#print axioms arrayDecoder_run_length +#print axioms arrayDecoder_output_length + +-- Metadata is supplied independently of width, with agreement checked on output. +example : boolDecoder.asStorageDecoder.run () [AMByte.init 1] = some true := by decide +example : boolDecoder.asStorageDecoder.run () [AMByte.init 2] = none := by decide +example (bytes : List AMByte) : byteDecoder.asStorageDecoder.run () bytes = byteDecoder.run bytes := + BitDecoder.run_asStorageDecoder _ _ + +example : (sliceDecoder boolDecoder).run 2 [AMByte.init 1, AMByte.init 0] = some [true, false] := by decide +example : (sliceDecoder boolDecoder).run 1 [AMByte.init 1, AMByte.init 0] = none := by decide +example : (sliceDecoder boolDecoder).run 2 [AMByte.init 1, AMByte.init 2] = none := by decide +example : (sliceDecoder unitDecoder).run 0 [] = some [] := by decide +example : (sliceDecoder unitDecoder).run 3 [] = some [(), (), ()] := by decide +example : (sliceDecoder unitDecoder).run 3 [AMByte.init 0] = none := by decide +example : (sliceDecoder (statefulZstDecoder false)).run 1 [] = none := by decide +example : (sliceDecoder (statefulZstDecoder false)).run 0 [] = some [] := by decide +example : (sliceDecoder boolDecoder).Initialized := sliceDecoder_initialized _ boolDecoder_initialized + +-- These synthetic layouts share a padded width for multiple metadata values. +-- The example establishes no Rust representation or ABI for a particular type. +def plateauDecoder : StorageDecoder Nat Nat where + byteSize count := (count + 3) / 4 * 4 + metadata := id + decode count _ := some count + +example : plateauDecoder.byteSize 1 = plateauDecoder.byteSize 2 := by decide +example : plateauDecoder.run 1 (List.replicate 4 (AMByte.init 0)) = some 1 := by decide +example : plateauDecoder.run 2 (List.replicate 4 (AMByte.init 0)) = some 2 := by decide +example : plateauDecoder.run 2 (List.replicate 3 (AMByte.init 0)) = none := by decide + +def wrongMetadataDecoder : StorageDecoder Nat Nat where + byteSize _ := 0 + metadata := id + decode _ _ := some 0 + +example : wrongMetadataDecoder.decode 3 [] = some 0 := rfl +example : wrongMetadataDecoder.run 3 [] = none := by decide +example : wrongMetadataDecoder.run 0 [] = some 0 := by decide + +-- Mathematical rejection cannot reduce the independent initialization obligation. +example : ¬ badDecoder.asStorageDecoder.Initialized := by + intro initialized + have impossible := initialized () [AMByte.uninit] () (by decide) + simp [Initialized] at impossible +example : badDecoder.asStorageDecoder.runWith (fun _ => (none : Option Unit)) () [AMByte.uninit] = none := by decide + +-- Strong completeness demands a mathematical value as well as a language value. +example : unitDecoder.asStorageDecoder.CompleteWith (fun raw => some raw) := by + intro metadata bytes width initialized + cases metadata + have empty : bytes = [] := List.length_eq_zero_iff.mp width + subst bytes + exact ⟨(), rfl⟩ +example : ¬ unitDecoder.asStorageDecoder.CompleteWith (fun _ => (none : Option Unit)) := by + intro complete + obtain ⟨value, accepted⟩ := complete () [] rfl initialized_nil + simp [StorageDecoder.runWith] at accepted + +#print axioms StorageDecoder.run_eq_some_iff +#print axioms sliceDecoder_initialized +#print axioms StorageDecoder.completeWith_iff + +-- Every represented initialized 32-bit word admits a four-byte array model. +-- This tests the owned byte-cast law without introducing an encoder authority. +theorem fourBytes_complete : (arrayDecoder byteDecoder 4).asStorageDecoder.CompleteWith some := by + intro metadata bytes width initialized + cases metadata + obtain ⟨values, accepted⟩ := arrayDecoder_complete byteDecoder byteDecoder_complete 4 bytes width initialized + exact ⟨values, by simpa [StorageDecoder.runWith] using accepted⟩ + +example (bytes : List AMByte) (word : BitVec 32) + (accepted : (integerDecoder 4 .little).run bytes = some word) : + ∃ values, (arrayDecoder byteDecoder 4).asStorageDecoder.runWith some () bytes = some values := + StorageDecoder.cast_complete (integerDecoder 4 .little).asStorageDecoder + (arrayDecoder byteDecoder 4).asStorageDecoder some + (BitDecoder.asStorageDecoder_initialized _ (integerDecoder_initialized _ _)) + fourBytes_complete () () bytes word (by simpa using accepted) rfl + +example : (integerDecoder 4 .little).asStorageDecoder.run () + [AMByte.init 2, AMByte.init 0, AMByte.init 0, AMByte.init 0] = some 2 := by decide +example : (arrayDecoder byteDecoder 4).asStorageDecoder.runWith some () + [AMByte.init 2, AMByte.init 0, AMByte.init 0, AMByte.init 0] = some ⟨[2, 0, 0, 0], rfl⟩ := by decide + +-- Equal width and initialized source storage cannot replace destination completeness. +example : (integerDecoder 1 .little).asStorageDecoder.run () [AMByte.init 2] = some 2 := by decide +example : boolDecoder.asStorageDecoder.runWith some () [AMByte.init 2] = none := by decide +example : ¬ boolDecoder.asStorageDecoder.CompleteWith some := by + intro complete + obtain ⟨value, accepted⟩ := complete () [AMByte.init 2] rfl (by simp [Initialized]) + have invalid : boolDecoder.asStorageDecoder.runWith some () [AMByte.init 2] = none := by decide + rw [invalid] at accepted + contradiction + +#print axioms arrayDecoder_complete +#print axioms StorageDecoder.cast_complete + +end Rust.Storage.Tests diff --git a/anneal/lean/RustTests.lean b/anneal/lean/RustTests.lean new file mode 100644 index 0000000000..cf3ca1739e --- /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.Pointer, `Rust.Bytes, `Rust.Storage, `Rust.Arithmetic] + 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/aeneas/RustAeneas.lean b/anneal/lean/aeneas/RustAeneas.lean new file mode 100644 index 0000000000..561e115ab6 --- /dev/null +++ b/anneal/lean/aeneas/RustAeneas.lean @@ -0,0 +1,11 @@ +/- 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 RustAeneas.Machine +import RustAeneas.Bytes +import RustAeneas.Storage diff --git a/anneal/lean/aeneas/RustAeneas/Bytes.lean b/anneal/lean/aeneas/RustAeneas/Bytes.lean new file mode 100644 index 0000000000..5cf35d342c --- /dev/null +++ b/anneal/lean/aeneas/RustAeneas/Bytes.lean @@ -0,0 +1,75 @@ +/- 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 Aeneas.Data.BitVec +public import Rust.Bytes +@[expose] public section + +/-! +These adapters connect the shared numerical byte model to Aeneas's byte +primitives for every byte sequence and byte-aligned bit width. They prove +relations between Lean definitions; Rust/compiler correspondence is separate. +-/ + +namespace Rust.Bytes.AeneasAdapter + +theorem fromLEBytes_toNat (bytes : List Rust.Bytes.Byte) : + (BitVec.fromLEBytes bytes).toNat = Rust.Bytes.decodeLE bytes := by + induction bytes with + | nil => simp [BitVec.fromLEBytes, Rust.Bytes.decodeLE] + | cons byte rest ih => + have hwidth : 2 ^ (8 * (byte :: rest).length) = 256 * 256 ^ rest.length := by + rw [← Rust.Bytes.radix_pow_eq_two_pow] + simp [Nat.pow_succ, Nat.mul_comm] + have hb := Rust.Bytes.byte_lt_256 byte + have hr := Rust.Bytes.decodeLE_lt rest + have hp : 0 < 256 ^ rest.length := Nat.pow_pos (by decide) + simp only [BitVec.fromLEBytes, BitVec.toNat_or, BitVec.toNat_setWidth, + BitVec.toNat_shiftLeft, Nat.shiftLeft_eq, ih, hwidth] + rw [Nat.mod_eq_of_lt (by omega : byte.toNat < 256 * 256 ^ rest.length), + Nat.mod_eq_of_lt (by omega : Rust.Bytes.decodeLE rest < 256 * 256 ^ rest.length), + Nat.mod_eq_of_lt (by omega : Rust.Bytes.decodeLE rest * 2 ^ 8 < 256 * 256 ^ rest.length)] + rw [Nat.or_comm, Nat.mul_comm (Rust.Bytes.decodeLE rest) (2 ^ 8), + ← Nat.two_pow_add_eq_or_of_lt (show byte.toNat < 2 ^ 8 from hb)] + simp only [Rust.Bytes.decodeLE_cons, Nat.reducePow] + omega + +theorem fromBEBytes_toNat (bytes : List Rust.Bytes.Byte) : + (BitVec.fromBEBytes bytes).toNat = Rust.Bytes.decodeBE bytes := by + simp only [BitVec.fromBEBytes, BitVec.toNat_cast, fromLEBytes_toNat, + Rust.Bytes.decodeBE] + +/-- For a whole number of bytes, Aeneas's emitted bytes recover the value. -/ +theorem decodeLE_toLEBytes {width : Nat} (h : width % 8 = 0) (value : BitVec width) : + Rust.Bytes.decodeLE value.toLEBytes = value.toNat := by + have result := congrArg BitVec.toNat (BitVec.fromLEBytes_toLEBytes h value) + simpa only [fromLEBytes_toNat, BitVec.toNat_cast] using result + +theorem decodeBE_toBEBytes {width : Nat} (h : width % 8 = 0) (value : BitVec width) : + Rust.Bytes.decodeBE value.toBEBytes = value.toNat := by + simp only [BitVec.toBEBytes, Rust.Bytes.decodeBE, List.reverse_reverse] + exact decodeLE_toLEBytes h value + +/-- Aeneas and the shared model write the same bytes for every byte-aligned width. -/ +theorem toLEBytes_eq_encodeLE {width : Nat} (h : width % 8 = 0) (value : BitVec width) : + value.toLEBytes = Rust.Bytes.encodeLE (width / 8) value.toNat := by + have hlength : value.toLEBytes.length = width / 8 := by + rw [BitVec.toLEBytes_length] + omega + calc + value.toLEBytes = Rust.Bytes.encodeLE value.toLEBytes.length + (Rust.Bytes.decodeLE value.toLEBytes) := (Rust.Bytes.encodeLE_decodeLE _).symm + _ = Rust.Bytes.encodeLE (width / 8) value.toNat := by + rw [hlength, decodeLE_toLEBytes h] + +theorem toBEBytes_eq_encodeBE {width : Nat} (h : width % 8 = 0) (value : BitVec width) : + value.toBEBytes = Rust.Bytes.encodeBE (width / 8) value.toNat := by + rw [BitVec.toBEBytes, Rust.Bytes.encodeBE, toLEBytes_eq_encodeLE h] + +end Rust.Bytes.AeneasAdapter diff --git a/anneal/lean/aeneas/RustAeneas/Machine.lean b/anneal/lean/aeneas/RustAeneas/Machine.lean new file mode 100644 index 0000000000..1e1f839d29 --- /dev/null +++ b/anneal/lean/aeneas/RustAeneas/Machine.lean @@ -0,0 +1,194 @@ +/- 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 Aeneas.Std.Core +import Aeneas.Tactic.Solver.ScalarTac + +open Aeneas.Std +namespace Rust.Machine + +/-- An Aeneas `Usize` carrier validated as a Rust alignment. -/ +structure Alignment where + val : Usize + isValid : IsAlignment val.val + + +@[simp] theorem Alignment_val {val} {h} : (@Alignment.mk val h).val = val := rfl +@[simp] theorem Alignment_isValid (a : Alignment) : Rust.IsAlignment a.val.val := a.isValid +instance : Inhabited Alignment := ⟨⟨Usize.ofNatCore 1 (by scalar_tac), Rust.alignment_one⟩⟩ + +structure SpecLayout where + size : Nat + align : Alignment + sizeAligned : align.val.val ∣ size + +/-- Forget the frontend's machine-bounded alignment representation. -/ +abbrev SpecLayout.toGeometry (lay : SpecLayout) : Rust.Layout := + ⟨lay.size, lay.align.val.val, lay.align.isValid, lay.sizeAligned⟩ + +/-- + A numerical layout with machine-bounded size and alignment. + + Its size is represented by `Usize` and its alignment satisfies the Rust + alignment predicate. These bounds do not establish that an allocation exists, + is live, or has valid pointer provenance. +-/ +structure Layout where + size : Usize + align : Alignment + sizeAligned : align.val.val ∣ size.val + +/-- + A proof that a mathematical layout's size fits within `Usize.max`. + + This numerical bound permits a `Usize` representation; it does not establish + allocation existence, liveness, or pointer provenance. +-/ +class FitsInUsize (lay : SpecLayout) : Prop where + fits : lay.size ≤ Usize.max + +/-- + Converts a mathematical layout to a machine-bounded numerical layout. + + The required proof bounds the size by `Usize.max`. +-/ +@[simp] +def SpecLayout.toLayout (lay : SpecLayout) [FitsInUsize lay] : Layout := + { + size := Usize.ofNatCore lay.size (by + have := FitsInUsize.fits (lay := lay) + scalar_tac), + align := lay.align, + sizeAligned := lay.sizeAligned + } + +/-- + Converts a machine-bounded numerical layout to its mathematical layout. + + The `Usize` carrier supplies the bound needed to prove that the resulting + `SpecLayout` also fits in `Usize`. +-/ +@[simp] +def Layout.toSpecLayout (lay : Layout) : SpecLayout := + { size := lay.size.val, align := lay.align, sizeAligned := lay.sizeAligned } + +instance (lay : Layout) : FitsInUsize lay.toSpecLayout where + fits := by + dsimp [Layout.toSpecLayout] + scalar_tac + +structure SpecSliceDstLayout where + trailingOffset : Nat + elementSize : Nat + align : Alignment + +abbrev SpecSliceDstLayout.toGeometry (info : SpecSliceDstLayout) : Rust.SliceDstLayout := + ⟨info.trailingOffset, info.elementSize, info.align.val.val, info.align.isValid⟩ + +structure Allocation where + base : Usize + size : Usize + addresses : Set Nat + + -- `base` is not equal to null (address 0) + base_not_null : base.val ≠ 0 + + -- `size <= isize::MAX` + size_le_isize_max : size.val ≤ Isize.max + + -- `base + size <= usize::MAX` + base_add_size_le_usize_max : base.val + size.val ≤ Usize.max + + -- 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 + +/-- Forget the frontend's machine bounds, retaining the shared allocation geometry. -/ +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_sub := Rust.Allocation.offset_lt_size alloc.toGeometry a ha + change a - alloc.base.val < alloc.size.val at h_sub + have h_size : alloc.size.val ≤ Isize.max := alloc.size_le_isize_max + omega + +-- Consequence 2: `a - base` is non-negative +-- (This is trivially true in Lean for `Nat` subtraction when `alloc.base ≤ a`, +-- 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 := + 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_lt := Rust.Allocation.address_lt_end alloc.toGeometry a ha + change a < alloc.base.val + alloc.size.val at h_lt + have h_max : alloc.base.val + alloc.size.val ≤ Usize.max := alloc.base_add_size_le_usize_max + omega + +end Allocation + +structure Referent where + -- The start address of the referent + address : Usize + -- The size of the referent in bytes + size : Usize + -- The mathematical set of addresses that make up the referent + addresses : Set Nat + + bounds : ∀ a ∈ addresses, address.val ≤ a ∧ a < address.val + size.val + + addresses_are_usizes : ∀ a ∈ addresses, a ≤ Usize.max + +instance : Nonempty Referent := + ⟨{ address := Usize.ofNatCore 0 (by scalar_tac), size := Usize.ofNatCore 0 (by scalar_tac), addresses := ∅, + bounds := by + intro a h + simp at h, + addresses_are_usizes := by + intro a h + simp at h }⟩ + +/-- Forget the frontend's machine bounds, retaining the shared referent geometry. -/ +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 := + Rust.Referent.IsContiguous r.toGeometry + +/-- + A predicate indicating that a referent fits entirely within a given allocation. + This means that all logical addresses of the referent are addresses allocated + in the allocation, and the contiguous address range of the referent is + a sub-range of the contiguous address range of the allocation. +-/ +def FitsInAllocation (r : Referent) (a : Allocation) : Prop := + Rust.FitsInAllocation r.toGeometry a.toGeometry + +/-- + A helper theorem proving that any address belonging to a referent that + fits in an allocation is strictly less than the allocation's upper bound. +-/ +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 + exact Rust.FitsInAllocation.address_bounds_alloc r.toGeometry a.toGeometry h addr ha + + +end Rust.Machine diff --git a/anneal/lean/aeneas/RustAeneas/Storage.lean b/anneal/lean/aeneas/RustAeneas/Storage.lean new file mode 100644 index 0000000000..e7c9c76402 --- /dev/null +++ b/anneal/lean/aeneas/RustAeneas/Storage.lean @@ -0,0 +1,54 @@ +/- 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 Aeneas +public import Rust.Storage +@[expose] public section + +/-! +The shared integer decoder retains the complete bit pattern. Aeneas's unsigned +and signed scalar carriers store that same bit vector, so these adapters change +the carrier without testing or discarding any initialized pattern. Signed +interpretation is supplied by Aeneas's two's-complement scalar observation. + +The byte order remains an argument. Connecting it and the machine-word width +to a Rust extraction is the consumer's target-specific responsibility; these +definitions do not establish a Rust ABI merely by constructing a Lean value. +-/ + +open Aeneas.Std +namespace Rust.Storage.AeneasAdapter + +/-- Aeneas currently supports 32- and 64-bit machine words. Both have a whole +number of bytes, as do its fixed-width integer carriers. -/ +theorem unsigned_byte_width (ty : UScalarTy) : 8 * (ty.numBits / 8) = ty.numBits := by + cases ty <;> simp [UScalarTy.numBits] + cases System.Platform.numBits_eq <;> simp_all + +theorem signed_byte_width (ty : IScalarTy) : 8 * (ty.numBits / 8) = ty.numBits := by + cases ty <;> simp [IScalarTy.numBits] + cases System.Platform.numBits_eq <;> simp_all + +def unsignedDecoder (ty : UScalarTy) (endian : Rust.Bytes.Endian) : BitDecoder (UScalar ty) := + (integerDecoder (ty.numBits / 8) endian).map fun word => + ⟨word.cast (unsigned_byte_width ty)⟩ + +def signedDecoder (ty : IScalarTy) (endian : Rust.Bytes.Endian) : BitDecoder (IScalar ty) := + (integerDecoder (ty.numBits / 8) endian).map fun word => + ⟨word.cast (signed_byte_width ty)⟩ + +theorem unsignedDecoder_initialized (ty : UScalarTy) (endian : Rust.Bytes.Endian) : + (unsignedDecoder ty endian).Initialized := + BitDecoder.map_initialized _ _ (integerDecoder_initialized _ _) + +theorem signedDecoder_initialized (ty : IScalarTy) (endian : Rust.Bytes.Endian) : + (signedDecoder ty endian).Initialized := + BitDecoder.map_initialized _ _ (integerDecoder_initialized _ _) + +end Rust.Storage.AeneasAdapter diff --git a/anneal/lean/aeneas/RustAeneasTests.lean b/anneal/lean/aeneas/RustAeneasTests.lean new file mode 100644 index 0000000000..1214cbb89e --- /dev/null +++ b/anneal/lean/aeneas/RustAeneasTests.lean @@ -0,0 +1,41 @@ +/- 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 RustAeneas.Machine +import RustAeneas.Bytes +import Lean.Util.CollectAxioms +import Lean.Elab.Command + +example (lay : Rust.Machine.Layout) : + lay.toSpecLayout.size = lay.size.val := rfl + +example (lay : Rust.Machine.SpecLayout) [Rust.Machine.FitsInUsize lay] : + lay.toLayout.toSpecLayout.size = lay.size := by simp [Rust.Machine.SpecLayout.toLayout, + Rust.Machine.Layout.toSpecLayout] + +-- Keep the Aeneas-backed machine layer separate from the pure Rust audit. +-- Only standard logical axioms are permitted in this companion's declarations. +run_cmd do + let env ← Lean.getEnv + let modules := #[`RustAeneas.Machine, `RustAeneas.Bytes] + let owners ← modules.mapM fun moduleName => do + let some owner := env.getModuleIdx? moduleName + | throwError "Companion module was not imported: {moduleName}" + pure owner + 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 "Companion declaration {name} depends on forbidden axiom {assumption}" + audited := audited + 1 + unless audited > 0 do + throwError "Companion axiom audit found no declarations" + Lean.logInfo m!"Companion axiom audit checked {audited} declarations" diff --git a/anneal/lean/aeneas/lakefile.lean b/anneal/lean/aeneas/lakefile.lean new file mode 100644 index 0000000000..fd944f0562 --- /dev/null +++ b/anneal/lean/aeneas/lakefile.lean @@ -0,0 +1,20 @@ +/- 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 + +require rust_model from ".." +require aeneas from ((get_config? aeneasPath).getD "../../aeneas/backends/lean") + +package rust_model_aeneas + +@[default_target] +lean_lib RustAeneas + +lean_lib RustAeneasTests 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..5b8789f232 --- /dev/null +++ b/anneal/lean/lakefile.lean @@ -0,0 +1,32 @@ +/- 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 the library and all four test targets below, then +-- reruns the `RustTests.lean` axiom audit when cached output might be reused. +lean_lib RustTests where + roots := #[`RustTests] + +lean_lib RustBytesTests where + roots := #[`RustBytesTests] + +lean_lib RustStorageTests where + roots := #[`RustStorageTests] + +lean_lib RustPointerTests where + roots := #[`RustPointerTests] diff --git a/anneal/lean/lean-toolchain b/anneal/lean/lean-toolchain new file mode 100644 index 0000000000..18640c8b06 --- /dev/null +++ b/anneal/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.31.0 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/llms-full.txt b/anneal/v1/llms-full.txt index 8f0681ff86..ed1bf337e4 100644 --- a/anneal/v1/llms-full.txt +++ b/anneal/v1/llms-full.txt @@ -822,14 +822,16 @@ theorem wp_prove_orthogonal {α} {m : Result α} {P : α → Prop} : This reflects Rust's requirement that all layout alignments are non-zero powers of two. -/ -def IsAlignment (n : Nat) : Prop +abbrev IsAlignment /-- A validated Rust alignment, bundling the value and its proof. -/ -structure Alignment where - val : Usize - isValid : IsAlignment val.val +abbrev Alignment -instance : Inhabited Alignment +abbrev mk + +abbrev val (x : Alignment) + +abbrev isValid (x : Alignment) /-- A stub for the `Sized` trait. @@ -898,35 +900,29 @@ def deriveSizedCmd (declName : Name) : CommandElabM Unit to fit within `Usize`. It is used to reason about the layout of values whose sizes may exceed the maximum addressable memory. -/ -structure SpecLayout where - size : Nat - align : Alignment - sizeAligned : align.val.val ∣ size +abbrev SpecLayout -/-- - A valid physical memory layout for a value. +abbrev mk - This layout is defined by a size and an alignment. It is bounded by the - physical constraints of the machine, meaning that its size is guaranteed to - fit within the addressable memory bounds of `Usize`. It is used to represent - the layout of a value that actually exists in physical memory. --/ -structure Layout where - size : Usize - align : Alignment - sizeAligned : align.val.val ∣ size.val +abbrev size (x : SpecLayout) -/-- - A proof that a mathematical layout size is small enough to exist in physical - memory. +abbrev align (x : SpecLayout) - This proof establishes that the size of a mathematical layout fits within - `Usize.max`, meaning the layout can describe a physical value. --/ -class FitsInUsize (lay : SpecLayout) : Prop where - fits : lay.size ≤ Usize.max +abbrev sizeAligned (x : SpecLayout) -instance (lay : Layout) : FitsInUsize lay.toSpecLayout +abbrev toGeometry (x : SpecLayout) + +abbrev Layout + +abbrev mk + +abbrev sizeAligned (x : Layout) + +abbrev FitsInUsize + +abbrev mk {lay : SpecLayout} (fits : lay.size ≤ Usize.max) : FitsInUsize lay + +abbrev fits {lay : SpecLayout} [FitsInUsize lay] : lay.size ≤ Usize.max /-- The ability to compute a mathematically idealized layout for a runtime value. @@ -986,10 +982,17 @@ class HasStaticLayout (α : Type) [core.marker.Sized α] where The mathematical layout properties that are statically known for all instances of a slice-based dynamically-sized type (Slice DST). -/ -structure SpecSliceDstLayout where - trailingOffset : Nat - elementSize : Nat - align : Alignment +abbrev SpecSliceDstLayout + +abbrev mk + +abbrev trailingOffset (x : SpecSliceDstLayout) + +abbrev elementSize (x : SpecSliceDstLayout) + +abbrev align (x : SpecSliceDstLayout) + +abbrev toGeometry (x : SpecSliceDstLayout) /-- Provides the static slice DST layout properties for a given type. @@ -1006,16 +1009,11 @@ 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 +abbrev roundUpToAlign -/-- 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 +abbrev roundUpToAlign_ge -/-- 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 +abbrev align_le_roundUpToAlign /-- Computes the exact mathematical size of a `repr(C)` Slice DST instance. @@ -1086,71 +1084,58 @@ abbrev align_of_spec (align_of_fun : Type → Result Usize) : Prop Because there is no guarantee that an allocation is contiguous, `addresses` is modeled as an arbitrary `Set Nat` rather than a contiguous range. -/ -structure Allocation where - base : Usize - size : Usize - addresses : Set Nat +abbrev Allocation - -- `base` is not equal to null (address 0) - base_not_null : base.val ≠ 0 +abbrev mk - -- `size <= isize::MAX` - size_le_isize_max : size.val ≤ Isize.max +abbrev base (x : Allocation) - -- `base + size <= usize::MAX` - base_add_size_le_usize_max : base.val + size.val ≤ Usize.max +abbrev size (x : Allocation) - -- 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 +abbrev addresses (x : Allocation) + +abbrev base_not_null (x : Allocation) -theorem offset_le_isize_max (alloc : Allocation) (a : Nat) (ha : a ∈ alloc.addresses) : - a - alloc.base.val ≤ Isize.max +abbrev size_le_isize_max (x : Allocation) -theorem offset_non_negative (alloc : Allocation) (a : Nat) (ha : a ∈ alloc.addresses) : - alloc.base.val ≤ a +abbrev base_add_size_le_usize_max (x : Allocation) -theorem address_le_usize_max (alloc : Allocation) (a : Nat) (ha : a ∈ alloc.addresses) : - a ≤ Usize.max +abbrev bounds (x : Allocation) + +abbrev toGeometry (x : Allocation) + +abbrev offset_le_isize_max (x : Allocation) (addr : Nat) (ha : addr ∈ x.addresses) + +abbrev offset_non_negative (x : Allocation) (addr : Nat) (ha : addr ∈ x.addresses) + +abbrev address_le_usize_max (x : Allocation) (addr : Nat) (ha : addr ∈ x.addresses) /-- Retrieves the properties of a pointer's referent. The referent is the region of memory that the pointer addresses. -/ -structure Referent where - -- The start address of the referent - address : Usize - -- The size of the referent in bytes - size : Usize - -- The mathematical set of addresses that make up the referent - addresses : Set Nat +abbrev Referent - bounds : ∀ a ∈ addresses, address.val ≤ a ∧ a < address.val + size.val +abbrev mk - addresses_are_usizes : ∀ a ∈ addresses, a ≤ Usize.max +abbrev address (x : Referent) -instance : Nonempty Referent +abbrev size (x : Referent) -/-- - 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 +abbrev addresses (x : Referent) -/-- - A predicate indicating that a referent fits entirely within a given allocation. - This means that all logical addresses of the referent are addresses allocated - in the allocation, and the contiguous address range of the referent is - a sub-range of the contiguous address range of the allocation. --/ -def FitsInAllocation (r : Referent) (a : Allocation) : Prop +abbrev bounds (x : Referent) -/-- - A helper theorem proving that any address belonging to a referent that - fits in an allocation is strictly less than the allocation's upper bound. --/ -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 +abbrev addresses_are_usizes (x : Referent) + +abbrev toGeometry (x : Referent) + +abbrev IsContiguous (x : Referent) : Prop + +abbrev FitsInAllocation + +abbrev address_bounds_alloc (r : Referent) (a : Allocation) + (h : FitsInAllocation r a) (addr : Nat) (ha : addr ∈ r.addresses) /-- A class for types that act as pointers with a well-defined referent. diff --git a/anneal/v1/src/Anneal.lean b/anneal/v1/src/Anneal.lean index 0ccf026a52..6a3bbb02a8 100644 --- a/anneal/v1/src/Anneal.lean +++ b/anneal/v1/src/Anneal.lean @@ -1,3 +1,7 @@ +-- Shared definitions supply the unbounded mathematics and its machine-bounded +-- companion. This frontend retains its premises about actual Rust operations. +import Rust +import RustAeneas.Machine import Aeneas.Std.Core import Aeneas.Std.WP import Aeneas.Tactic.Solver.ScalarTac @@ -152,22 +156,24 @@ 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 - val : Usize - isValid : IsAlignment val.val +abbrev Alignment := Rust.Machine.Alignment +namespace Alignment +abbrev mk := Rust.Machine.Alignment.mk +abbrev val (x : Alignment) := Rust.Machine.Alignment.val x +abbrev isValid (x : Alignment) := Rust.Machine.Alignment.isValid x +end Alignment @[simp] theorem Usize_ofNatCore_val {n} {h} : (Usize.ofNatCore n h).val = n := rfl @[simp] theorem Alignment_val {val} {h} : (@Alignment.mk val h).val = val := rfl @[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⟩⟩ +-- The shared machine module supplies the `Inhabited Alignment` instance. @[simp, grind .] theorem one_divides (n : Nat) : 1 ∣ n := ⟨n, by omega⟩ @@ -254,65 +260,34 @@ end core to fit within `Usize`. It is used to reason about the layout of values whose sizes may exceed the maximum addressable memory. -/ -structure SpecLayout where - size : Nat - align : Alignment - sizeAligned : align.val.val ∣ size - -/-- - A valid physical memory layout for a value. - - This layout is defined by a size and an alignment. It is bounded by the - physical constraints of the machine, meaning that its size is guaranteed to - fit within the addressable memory bounds of `Usize`. It is used to represent - the layout of a value that actually exists in physical memory. --/ -structure Layout where - size : Usize - align : Alignment - sizeAligned : align.val.val ∣ size.val - -/-- - A proof that a mathematical layout size is small enough to exist in physical - memory. - - This proof establishes that the size of a mathematical layout fits within - `Usize.max`, meaning the layout can describe a physical value. --/ -class FitsInUsize (lay : SpecLayout) : Prop where - fits : lay.size ≤ Usize.max - -/-- - Converts a mathematical layout into a physical layout. - - This conversion requires a proof that the mathematical layout fits within - physical memory. --/ -@[simp] -def SpecLayout.toLayout (lay : SpecLayout) [FitsInUsize lay] : Layout := - { - size := Usize.ofNatCore lay.size (by - have := FitsInUsize.fits (lay := lay) - scalar_tac), - align := lay.align, - sizeAligned := lay.sizeAligned - } - -/-- - Converts a valid physical layout into its corresponding mathematical layout. - - Because physical memory guarantees a layout's size easily fits within the - address space, we can inherently prove that the resulting mathematical `SpecLayout` - also fits in `Usize`. --/ -@[simp] -def Layout.toSpecLayout (lay : Layout) : SpecLayout := - { size := lay.size.val, align := lay.align, sizeAligned := lay.sizeAligned } - -instance (lay : Layout) : FitsInUsize lay.toSpecLayout where - fits := by - dsimp [Layout.toSpecLayout] - scalar_tac +abbrev SpecLayout := Rust.Machine.SpecLayout +namespace SpecLayout +abbrev mk := Rust.Machine.SpecLayout.mk +abbrev size (x : SpecLayout) := Rust.Machine.SpecLayout.size x +abbrev align (x : SpecLayout) := Rust.Machine.SpecLayout.align x +abbrev sizeAligned (x : SpecLayout) := Rust.Machine.SpecLayout.sizeAligned x +abbrev toGeometry (x : SpecLayout) := Rust.Machine.SpecLayout.toGeometry x +@[simp] abbrev toLayout (x : SpecLayout) [Rust.Machine.FitsInUsize x] := Rust.Machine.SpecLayout.toLayout x +end SpecLayout + +abbrev Layout := Rust.Machine.Layout +namespace Layout +abbrev mk := Rust.Machine.Layout.mk +-- These names used to be structure projections. Expose the shared projections +-- to simp so existing size_of/align_of proofs still reduce concrete layouts. +@[simp] abbrev size (x : Layout) := Rust.Machine.Layout.size x +@[simp] abbrev align (x : Layout) := Rust.Machine.Layout.align x +abbrev sizeAligned (x : Layout) := Rust.Machine.Layout.sizeAligned x +@[simp] abbrev toSpecLayout (x : Layout) := Rust.Machine.Layout.toSpecLayout x +end Layout + +abbrev FitsInUsize := Rust.Machine.FitsInUsize +namespace FitsInUsize +abbrev mk {lay : SpecLayout} (fits : lay.size ≤ Usize.max) : FitsInUsize lay := + Rust.Machine.FitsInUsize.mk fits +abbrev fits {lay : SpecLayout} [FitsInUsize lay] : lay.size ≤ Usize.max := + Rust.Machine.FitsInUsize.fits (lay := lay) +end FitsInUsize /-- The ability to compute a mathematically idealized layout for a runtime value. @@ -408,10 +383,14 @@ instance {α : Type} [core.marker.Sized α] [tl : HasStaticSpecLayout α] : HasS The mathematical layout properties that are statically known for all instances of a slice-based dynamically-sized type (Slice DST). -/ -structure SpecSliceDstLayout where - trailingOffset : Nat - elementSize : Nat - align : Alignment +abbrev SpecSliceDstLayout := Rust.Machine.SpecSliceDstLayout +namespace SpecSliceDstLayout +abbrev mk := Rust.Machine.SpecSliceDstLayout.mk +abbrev trailingOffset (x : SpecSliceDstLayout) := Rust.Machine.SpecSliceDstLayout.trailingOffset x +abbrev elementSize (x : SpecSliceDstLayout) := Rust.Machine.SpecSliceDstLayout.elementSize x +abbrev align (x : SpecSliceDstLayout) := Rust.Machine.SpecSliceDstLayout.align x +abbrev toGeometry (x : SpecSliceDstLayout) := Rust.Machine.SpecSliceDstLayout.toGeometry x +end SpecSliceDstLayout /-- Provides the static slice DST layout properties for a given type. @@ -428,35 +407,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. @@ -465,8 +421,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 @@ -474,8 +429,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) @@ -733,50 +687,20 @@ elab "inject_builtins" : command => do Because there is no guarantee that an allocation is contiguous, `addresses` is modeled as an arbitrary `Set Nat` rather than a contiguous range. -/ -structure Allocation where - base : Usize - size : Usize - addresses : Set Nat - - -- `base` is not equal to null (address 0) - base_not_null : base.val ≠ 0 - - -- `size <= isize::MAX` - size_le_isize_max : size.val ≤ Isize.max - - -- `base + size <= usize::MAX` - base_add_size_le_usize_max : base.val + size.val ≤ Usize.max - - -- 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 - +abbrev Allocation := Rust.Machine.Allocation 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_size : alloc.size.val ≤ Isize.max := alloc.size_le_isize_max - omega - --- Consequence 2: `a - base` is non-negative --- (This is trivially true in Lean for `Nat` subtraction when `alloc.base ≤ a`, --- 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 - --- 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_max : alloc.base.val + alloc.size.val ≤ Usize.max := alloc.base_add_size_le_usize_max - omega - +abbrev mk := Rust.Machine.Allocation.mk +abbrev base (x : Allocation) := Rust.Machine.Allocation.base x +abbrev size (x : Allocation) := Rust.Machine.Allocation.size x +abbrev addresses (x : Allocation) := Rust.Machine.Allocation.addresses x +abbrev base_not_null (x : Allocation) := Rust.Machine.Allocation.base_not_null x +abbrev size_le_isize_max (x : Allocation) := Rust.Machine.Allocation.size_le_isize_max x +abbrev base_add_size_le_usize_max (x : Allocation) := Rust.Machine.Allocation.base_add_size_le_usize_max x +abbrev bounds (x : Allocation) := Rust.Machine.Allocation.bounds x +abbrev toGeometry (x : Allocation) := Rust.Machine.Allocation.toGeometry x +abbrev offset_le_isize_max (x : Allocation) (addr : Nat) (ha : addr ∈ x.addresses) := Rust.Machine.Allocation.offset_le_isize_max x addr ha +abbrev offset_non_negative (x : Allocation) (addr : Nat) (ha : addr ∈ x.addresses) := Rust.Machine.Allocation.offset_non_negative x addr ha +abbrev address_le_usize_max (x : Allocation) (addr : Nat) (ha : addr ∈ x.addresses) := Rust.Machine.Allocation.address_le_usize_max x addr ha end Allocation -- 7. Pointer Referents @@ -786,54 +710,24 @@ end Allocation Retrieves the properties of a pointer's referent. The referent is the region of memory that the pointer addresses. -/ -structure Referent where - -- The start address of the referent - address : Usize - -- The size of the referent in bytes - size : Usize - -- The mathematical set of addresses that make up the referent - addresses : Set Nat - - bounds : ∀ a ∈ addresses, address.val ≤ a ∧ a < address.val + size.val - - addresses_are_usizes : ∀ a ∈ addresses, a ≤ Usize.max - -instance : Nonempty Referent := - ⟨{ address := sz 0, size := sz 0, addresses := ∅, - bounds := by - intro a h - simp at h, - addresses_are_usizes := by - intro a h - simp at h }⟩ - -/-- - 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 - -/-- - A predicate indicating that a referent fits entirely within a given allocation. - This means that all logical addresses of the referent are addresses allocated - in the allocation, and the contiguous address range of the referent is - 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 - -/-- - A helper theorem proving that any address belonging to a referent that - fits in an allocation is strictly less than the allocation's upper bound. --/ -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 +abbrev Referent := Rust.Machine.Referent +namespace Referent +abbrev mk := Rust.Machine.Referent.mk +abbrev address (x : Referent) := Rust.Machine.Referent.address x +abbrev size (x : Referent) := Rust.Machine.Referent.size x +abbrev addresses (x : Referent) := Rust.Machine.Referent.addresses x +abbrev bounds (x : Referent) := Rust.Machine.Referent.bounds x +abbrev addresses_are_usizes (x : Referent) := Rust.Machine.Referent.addresses_are_usizes x +abbrev toGeometry (x : Referent) := Rust.Machine.Referent.toGeometry x +abbrev IsContiguous (x : Referent) : Prop := Rust.Machine.Referent.IsContiguous x +end Referent + +abbrev FitsInAllocation := Rust.Machine.FitsInAllocation +namespace FitsInAllocation +abbrev address_bounds_alloc (r : Referent) (a : Allocation) + (h : FitsInAllocation r a) (addr : Nat) (ha : addr ∈ r.addresses) := + Rust.Machine.FitsInAllocation.address_bounds_alloc r a h addr ha +end FitsInAllocation /-- 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 48db26c935..532b4f6625 100644 --- a/anneal/v1/src/aeneas.rs +++ b/anneal/v1/src/aeneas.rs @@ -281,6 +281,12 @@ require aeneas from "{}""#, path.display() ); + let rust_dep = format!(r#"require rust_model from "{}""#, toolchain.rust_lean_dir().display()); + let rust_aeneas_dep = format!( + r#"require rust_model_aeneas from "{}""#, + toolchain.rust_lean_dir().join("aeneas").display() + ); + let roots_str = lake_roots.iter().map(|r| format!("`{}", r)).collect::>().join(", "); let lakefile = format!( @@ -289,6 +295,8 @@ import Lake open Lake DSL {aeneas_dep} +{rust_dep} +{rust_aeneas_dep} package anneal_verification @@ -385,7 +393,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() + 3); let aeneas_lean_dir_manifest_path = path_to_manifest_string(&relative_manifest_path(&aeneas_lean_dir, workspace_root)?); packages.push(json!({ @@ -395,6 +409,19 @@ 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, + })); + packages.push(json!({ + "type": "path", + "name": "rust_model_aeneas", + "dir": path_to_manifest_string(&relative_manifest_path(&rust_lean_dir.join("aeneas"), workspace_root)?), + "inherited": false, + })); + for entry in aeneas_packages { let mut entry = entry .as_object() @@ -991,6 +1018,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.join("aeneas")).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 +1064,26 @@ mod tests { // is renamed into place. std::fs::create_dir_all(&workspace_root).unwrap(); - assert_eq!(packages.len(), 3); + assert_eq!(packages.len(), 5); 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"], "rust_model_aeneas"); + assert_manifest_dir_resolves(&workspace_root, &packages[2], &rust_lean.join("aeneas")); + assert_eq!(packages[2]["inherited"], false); + + assert_eq!(packages[3]["name"], "mathlib"); + assert_manifest_dir_resolves(&workspace_root, &packages[3], &mathlib); + assert_eq!(packages[3]["inherited"], true); - assert_eq!(packages[2]["name"], "Qq"); - assert_manifest_dir_resolves(&workspace_root, &packages[2], &qq); - assert_eq!(packages[2]["inherited"], true); + assert_eq!(packages[4]["name"], "Qq"); + assert_manifest_dir_resolves(&workspace_root, &packages[4], &qq); + assert_eq!(packages[4]["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(), diff --git a/anneal/v1/tests/integration.rs b/anneal/v1/tests/integration.rs index 6a75e04175..62338c8568 100644 --- a/anneal/v1/tests/integration.rs +++ b/anneal/v1/tests/integration.rs @@ -311,9 +311,11 @@ fn assert_archive_lake_cache_reuse( let aeneas_root = toolchain_root.join("aeneas"); let aeneas_lean = aeneas_root.join("backends/lean"); let lean_root = toolchain_root.join("lean"); + let rust_model = toolchain_root.join("rust-model"); let workspace = temp_root.join("generated-workspace"); assert_no_write_bits(&aeneas_root)?; + assert_no_write_bits(&rust_model)?; fs::create_dir_all(workspace.join("generated"))?; fs::copy(aeneas_lean.join("lean-toolchain"), workspace.join("lean-toolchain"))?; @@ -333,6 +335,8 @@ fn assert_archive_lake_cache_reuse( open Lake DSL require aeneas from "{}" +require rust_model from "{}" +require rust_model_aeneas from "{}" package anneal_verification @@ -341,10 +345,12 @@ lean_lib Generated where srcDir := "generated" roots := #[`Generated, `Anneal, `SpecificationHolds] "#, - lake_string(&aeneas_lean) + lake_string(&aeneas_lean), + lake_string(&rust_model), + lake_string(&rust_model.join("aeneas")), ), )?; - write_relative_archive_manifest(&workspace, &aeneas_lean)?; + write_relative_archive_manifest(&workspace, &aeneas_lean, &rust_model)?; // This mirrors v1's generated workspace contract with the Nix-built // archive: dependency paths are locked relative to the workspace, package @@ -382,6 +388,7 @@ fn assert_no_write_bits(root: &Path) -> Result<(), Box> { fn write_relative_archive_manifest( workspace: &Path, aeneas_lean: &Path, + rust_model: &Path, ) -> Result<(), Box> { let aeneas_lean = fs::canonicalize(aeneas_lean)?; let workspace = fs::canonicalize(workspace)?; @@ -402,6 +409,16 @@ fn write_relative_archive_manifest( "inherited": false, })]; + for (name, path) in + [("rust_model", rust_model.to_path_buf()), ("rust_model_aeneas", rust_model.join("aeneas"))] + { + let path = fs::canonicalize(path)?; + packages.push(json!({ + "type": "path", "name": name, + "dir": relative_manifest_string(&path, &workspace)?, "inherited": false, + })); + } + for entry in aeneas_packages { let mut entry = entry .as_object()