From a30eb5a2f8f85028c9ea9de7505e6842c8cd030e Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Wed, 14 Oct 2026 13:20:53 -0400 Subject: [PATCH] Share Rust layout, storage and pointer models in anneal/lean Anneal V1's embedded prelude mixes reusable Rust mathematics with frontend classes and trusted ABI and pointer premises. Move its layout, allocation and referent records into shared Lean packages, preserving the Anneal names through compatibility aliases. Keep unbounded alignment, layout, memory geometry and byte encodings in a Std-only Rust package. An Aeneas companion supplies bounded machine carriers, their proved conversions and byte-operation bridges using the consumer's existing backend. Frontend-specific classes and Rust premises remain in V1. Distribute both packages through the existing exocrate omnibus archive. Include sources, compiled artifacts and relative Lake manifests so V1 and V2 can import them after relocation from read-only installations. Add consumer tests and declaration audits that reject unapproved axioms. Model abstract bytes as initialized eight-bit values or uninitialized storage. Width- and endian-indexed integer decoders, validity filters, and array composition prove initialization of complete representations. Empty-storage decoding requires an explicit inhabitant: byte width zero cannot construct an uninhabited type or discharge a stateful library invariant. Rust correspondence remains a consumer premise. Metadata-indexed storage decoders retain explicit slice counts, including zero-sized elements, and check the returned metadata as well as byte width. Initialization remains independent of mathematical admission. Prove that source initialization and complete destination decoding admit an owned byte cast at equal widths, without asserting Rust operation correspondence. Keep pointer provenance as an opaque value independent of address and metadata. Prove preservation through value casts and metadata operations; non-nullness supplies no liveness or access permission. No pointer bytes or memory accesses are modeled. gherrit-pr-id: Ggis7hb6l6jmnmnk4fjfb3w2lulssgynz Agent-authored-by: AI agent acting on joshlf's behalf --- .github/workflows/anneal.yml | 8 +- anneal/check-flake-eval.sh | 1 + anneal/flake.nix | 147 ++++- anneal/lean/.gitignore | 5 + anneal/lean/README.md | 112 ++++ anneal/lean/Rust.lean | 22 + anneal/lean/Rust/Arithmetic.lean | 84 +++ anneal/lean/Rust/Bytes.lean | 205 +++++++ anneal/lean/Rust/Layout.lean | 111 ++++ anneal/lean/Rust/Memory.lean | 96 ++++ anneal/lean/Rust/Pointer.lean | 148 +++++ anneal/lean/Rust/Storage.lean | 601 +++++++++++++++++++++ anneal/lean/RustBytesTests.lean | 68 +++ anneal/lean/RustPointerTests.lean | 39 ++ anneal/lean/RustStorageTests.lean | 267 +++++++++ anneal/lean/RustTests.lean | 86 +++ anneal/lean/aeneas/RustAeneas.lean | 11 + anneal/lean/aeneas/RustAeneas/Bytes.lean | 75 +++ anneal/lean/aeneas/RustAeneas/Machine.lean | 194 +++++++ anneal/lean/aeneas/RustAeneas/Storage.lean | 54 ++ anneal/lean/aeneas/RustAeneasTests.lean | 41 ++ anneal/lean/aeneas/lakefile.lean | 20 + anneal/lean/lake-manifest.json | 6 + anneal/lean/lakefile.lean | 32 ++ anneal/lean/lean-toolchain | 1 + anneal/src/main.rs | 76 +++ anneal/src/setup.rs | 5 + anneal/v1/llms-full.txt | 161 +++--- anneal/v1/src/Anneal.lean | 282 +++------- anneal/v1/src/aeneas.rs | 53 +- anneal/v1/src/setup.rs | 6 + anneal/v1/tests/integration.rs | 21 +- 32 files changed, 2735 insertions(+), 303 deletions(-) create mode 100644 anneal/lean/.gitignore create mode 100644 anneal/lean/README.md create mode 100644 anneal/lean/Rust.lean create mode 100644 anneal/lean/Rust/Arithmetic.lean create mode 100644 anneal/lean/Rust/Bytes.lean create mode 100644 anneal/lean/Rust/Layout.lean create mode 100644 anneal/lean/Rust/Memory.lean create mode 100644 anneal/lean/Rust/Pointer.lean create mode 100644 anneal/lean/Rust/Storage.lean create mode 100644 anneal/lean/RustBytesTests.lean create mode 100644 anneal/lean/RustPointerTests.lean create mode 100644 anneal/lean/RustStorageTests.lean create mode 100644 anneal/lean/RustTests.lean create mode 100644 anneal/lean/aeneas/RustAeneas.lean create mode 100644 anneal/lean/aeneas/RustAeneas/Bytes.lean create mode 100644 anneal/lean/aeneas/RustAeneas/Machine.lean create mode 100644 anneal/lean/aeneas/RustAeneas/Storage.lean create mode 100644 anneal/lean/aeneas/RustAeneasTests.lean create mode 100644 anneal/lean/aeneas/lakefile.lean create mode 100644 anneal/lean/lake-manifest.json create mode 100644 anneal/lean/lakefile.lean create mode 100644 anneal/lean/lean-toolchain diff --git a/.github/workflows/anneal.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()