Skip to content

Share Rust layout, storage and pointer models in anneal/lean #3823

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
joshlf wants to merge 1 commit into
base: Gkxoay4mfhudcnfy2cuk46iu6gnltvxg3
Choose a base branch
from
Open

Share Rust layout, storage and pointer models in anneal/lean #3823

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions .github/workflows/anneal.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
1 change: 1 addition & 0 deletions anneal/check-flake-eval.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ packages=(
omnibus-archive-layout-check
omnibus-tar
rust-toolchain
rust-model-compiled
)

for system in "${systems[@]}"; do
Expand Down
147 changes: 140 additions & 7 deletions anneal/flake.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand All @@ -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;

Expand All @@ -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...\""
Expand Down Expand Up @@ -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 *"
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
5 changes: 5 additions & 0 deletions anneal/lean/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Loading
Loading