diff --git a/.github/workflows/anneal-release.yml b/.github/workflows/anneal-release.yml index 6581e15c41..6980ae941a 100644 --- a/.github/workflows/anneal-release.yml +++ b/.github/workflows/anneal-release.yml @@ -297,6 +297,7 @@ jobs: mkdir -p anneal/target anneal/v1/release-download-check anneal/v1/release-metadata nix build ./anneal#omnibus-archive-ci --system "$NIX_SYSTEM" --out-link "anneal/target/${ARCHIVE_NAME}" + nix build ./anneal#omnibus-archive-layout-check --system "$NIX_SYSTEM" --no-link cp -L "anneal/target/${ARCHIVE_NAME}" "anneal/v1/${ARCHIVE_NAME}" ARCHIVE_SIZE="$(python3 -c 'import os, sys; print(os.path.getsize(sys.argv[1]))' "anneal/v1/${ARCHIVE_NAME}")" printf 'Built %s (%s bytes)\n' "$ARCHIVE_NAME" "$ARCHIVE_SIZE" diff --git a/anneal/flake.lock b/anneal/flake.lock index 92ac56b0a7..72f427f115 100644 --- a/anneal/flake.lock +++ b/anneal/flake.lock @@ -1,9 +1,125 @@ { "nodes": { + "aeneas": { + "inputs": { + "charon": "charon", + "flake-utils": [ + "aeneas", + "charon", + "flake-utils" + ], + "fstar": "fstar", + "nixpkgs": "nixpkgs_2" + }, + "locked": { + "lastModified": 1790781188, + "narHash": "sha256-gDWeMrDawLfd7FZpLUQnz55zcvCjRZlJxW+6PsG8CTw=", + "owner": "AeneasVerif", + "repo": "aeneas", + "rev": "ca282ec2312a96f6a985a4d23a663690816d3f3e", + "type": "github" + }, + "original": { + "owner": "AeneasVerif", + "repo": "aeneas", + "rev": "ca282ec2312a96f6a985a4d23a663690816d3f3e", + "type": "github" + } + }, + "charon": { + "inputs": { + "crane": "crane", + "flake-compat": "flake-compat", + "flake-utils": "flake-utils", + "jail-nix": "jail-nix", + "nixpkgs": [ + "nixpkgs" + ], + "rust-overlay": "rust-overlay" + }, + "locked": { + "lastModified": 1790769003, + "narHash": "sha256-xcYfAoqgGENU8zDXW7wD8ApcgEI9QojriFCKWUSkOAQ=", + "owner": "aeneasverif", + "repo": "charon", + "rev": "cf02e3f228f97ee7be3a415be56989053063326d", + "type": "github" + }, + "original": { + "owner": "aeneasverif", + "repo": "charon", + "type": "github" + } + }, + "crane": { + "locked": { + "lastModified": 1743700120, + "narHash": "sha256-8BjG/P0xnuCyVOXlYRwdI1B8nVtyYLf3oDwPSimqREY=", + "owner": "ipetkov", + "repo": "crane", + "rev": "e316f19ee058e6db50075115783be57ac549c389", + "type": "github" + }, + "original": { + "owner": "ipetkov", + "repo": "crane", + "type": "github" + } + }, + "flake-compat": { + "locked": { + "lastModified": 1733328505, + "narHash": "sha256-NeCCThCEP3eCl2l/+27kNNK7QrwZB1IJCrXfrbv5oqU=", + "owner": "edolstra", + "repo": "flake-compat", + "rev": "ff81ac966bb2cae68946d5ed5fc4994f96d0ffec", + "type": "github" + }, + "original": { + "owner": "edolstra", + "repo": "flake-compat", + "type": "github" + } + }, "flake-utils": { "inputs": { "systems": "systems" }, + "locked": { + "lastModified": 1726560853, + "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_2": { + "inputs": { + "systems": "systems_2" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "id": "flake-utils", + "type": "indirect" + } + }, + "flake-utils_3": { + "inputs": { + "systems": "systems_3" + }, "locked": { "lastModified": 1731533236, "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", @@ -18,7 +134,72 @@ "type": "github" } }, + "fstar": { + "inputs": { + "flake-utils": "flake-utils_2", + "nixpkgs": "nixpkgs" + }, + "locked": { + "lastModified": 1773420322, + "narHash": "sha256-24p4oLISFCehrfYAXORuEm6WzvWgRMhoApYnwUjSfPM=", + "owner": "FStarLang", + "repo": "fstar", + "rev": "7c23ae87427d49f73626f3bd045d7980f00b2685", + "type": "github" + }, + "original": { + "owner": "FStarLang", + "repo": "fstar", + "type": "github" + } + }, + "jail-nix": { + "locked": { + "lastModified": 1776230864, + "narHash": "sha256-YsEjjdOsGEzTeD+iT7ONh071BqWAOQWpzYVei3okAXE=", + "owner": "~alexdavid", + "repo": "jail.nix", + "rev": "404e7da9da5ab9aa643666682b2ba1312fa5fbe8", + "type": "sourcehut" + }, + "original": { + "owner": "~alexdavid", + "repo": "jail.nix", + "type": "sourcehut" + } + }, "nixpkgs": { + "locked": { + "lastModified": 1759381078, + "narHash": "sha256-gTrEEp5gEspIcCOx9PD8kMaF1iEmfBcTbO0Jag2QhQs=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "7df7ff7d8e00218376575f0acdcc5d66741351ee", + "type": "github" + }, + "original": { + "id": "nixpkgs", + "ref": "nixos-unstable", + "type": "indirect" + } + }, + "nixpkgs_2": { + "locked": { + "lastModified": 1762111121, + "narHash": "sha256-4vhDuZ7OZaZmKKrnDpxLZZpGIJvAeMtK6FKLJYUtAdw=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "b3d51a0365f6695e7dd5cdf3e180604530ed33b4", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "b3d51a0365f6695e7dd5cdf3e180604530ed33b4", + "type": "github" + } + }, + "nixpkgs_3": { "locked": { "lastModified": 1777954456, "narHash": "sha256-hGdgeU2Nk87RAuZyYjyDjFL6LK7dAZN5RE9+hrDTkDU=", @@ -36,8 +217,32 @@ }, "root": { "inputs": { - "flake-utils": "flake-utils", - "nixpkgs": "nixpkgs" + "aeneas": "aeneas", + "flake-utils": "flake-utils_3", + "nixpkgs": "nixpkgs_3" + } + }, + "rust-overlay": { + "inputs": { + "nixpkgs": [ + "aeneas", + "charon", + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1789630063, + "narHash": "sha256-hulcXtNnQVDTPXiC8dQpTX3FPHxklIfX7Cx2kd2GDrM=", + "owner": "oxalica", + "repo": "rust-overlay", + "rev": "a1d497a9415999853809ba22a7959b1c36dc6554", + "type": "github" + }, + "original": { + "owner": "oxalica", + "repo": "rust-overlay", + "rev": "a1d497a9415999853809ba22a7959b1c36dc6554", + "type": "github" } }, "systems": { @@ -54,6 +259,36 @@ "repo": "default", "type": "github" } + }, + "systems_2": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "systems_3": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } } }, "root": "root", diff --git a/anneal/flake.nix b/anneal/flake.nix index 433fcf5c64..6c9f389b9a 100644 --- a/anneal/flake.nix +++ b/anneal/flake.nix @@ -4,9 +4,13 @@ inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-utils.url = "github:numtide/flake-utils"; + aeneas.url = "github:AeneasVerif/aeneas/ca282ec2312a96f6a985a4d23a663690816d3f3e"; + # Charon's upstream nixpkgs has dropped Intel Mac support. Reuse this + # flake's existing compatible lock for the source-built fallback. + aeneas.inputs.charon.inputs.nixpkgs.follows = "nixpkgs"; }; - outputs = { self, nixpkgs, flake-utils, ... }: + outputs = { self, nixpkgs, flake-utils, aeneas, ... }: flake-utils.lib.eachDefaultSystem (system: let pkgs = import nixpkgs { @@ -14,6 +18,54 @@ config.allowUnfree = true; }; + # The upstream source and its lock identify the complete translation + # chain. Release downloads and the source-built Intel Mac fallback use + # this same pin; consumers can read the package passthru below. + aeneasRevision = aeneas.rev; + aeneasReleaseTag = "nightly-2026.10.01-${builtins.substring 0 7 aeneasRevision}"; + charonRevision = aeneas.inputs.charon.rev; + charonSourcePin = pkgs.lib.last (builtins.filter + (line: line != "" && !(pkgs.lib.hasPrefix "#" line)) + (pkgs.lib.splitString "\n" (builtins.readFile "${aeneas}/charon-pin"))); + leanToolchainName = pkgs.lib.removeSuffix "\n" + (builtins.readFile "${aeneas}/backends/lean/lean-toolchain"); + rustToolchainName = + (builtins.fromTOML (builtins.readFile "${aeneas.inputs.charon}/rust-toolchain")).toolchain.channel; + # V1 embeds these values in its binary. They are compatibility mirrors + # of this flake's upstream pin, and must agree before an archive builds. + v1ToolchainMetadata = + (builtins.fromTOML (builtins.readFile ./v1/Cargo.toml)).package.metadata.build_rs; + toolchainMetadata = { + aeneas-release = aeneasReleaseTag; + aeneas-revision = aeneasRevision; + aeneas-source-nar-hash = aeneas.narHash; + charon-revision = charonRevision; + lean-toolchain = pkgs.lib.removePrefix "v" leanVersion; + rust-toolchain-date = rustDate; + rust-toolchain-version = rustToolchainName; + }; + toolchain = toolchainMetadata // { + aeneas-source = aeneas.outPath; + charon-source = aeneas.inputs.charon.outPath; + }; + + # Both the upstream Intel archive and a locally patched translator need + # the same portable Mach-O bundler. Preserve its upstream dependency; + # only remove signing flags that sigtool does not implement. + darwinBundlers = builtins.filter + (input: (input.pname or "") == "macdylibbundler") + aeneas.packages.${system}.aeneas-release.buildInputs; + darwinBundler = assert builtins.length darwinBundlers == 1; + (builtins.head darwinBundlers).overrideAttrs (old: { + postPatch = (old.postPatch or "") + '' + substituteInPlace src/Utils.cpp --replace-fail \ + 'codesign --force --deep --preserve-metadata=entitlements,requirements,flags,runtime' \ + 'codesign --force' + ''; + }); + portabilityInputs = pkgs.lib.optionals pkgs.stdenv.isDarwin + [ darwinBundler pkgs.darwin.sigtool ]; + # Upstream platform names. rustPlatform = if system == "x86_64-linux" then "x86_64-unknown-linux-gnu" else if system == "aarch64-linux" then "aarch64-unknown-linux-gnu" @@ -33,25 +85,25 @@ else if system == "aarch64-darwin" then "macos-aarch64" else throw "Unsupported system: ${system}"; - aeneasSha256 = if system == "x86_64-linux" then "sha256-APuO9CfU0G3KvZD1GWJm4HcxrfKnRmlkzm9PbR6MvBE=" - else if system == "aarch64-linux" then "sha256-JUAsTLy32i0zfLFoZjVCvJx1rpsQ0tJwj1KJ6MqdGQI=" - else if system == "x86_64-darwin" then "sha256-uiXuhXp2+o9MECL23/QHLJoBAHRT1nxhz7qhqhwD4xc=" - else if system == "aarch64-darwin" then "sha256-dveLZF4zjsfokynwrSJ5KZf0K9m16xRkOsMq3iJO62E=" + aeneasSha256 = if system == "x86_64-linux" then "sha256-Rz3y5bqwQ5v9GmhQOuAsf4io3kGC6Y5OKBWQKFqwHe4=" + else if system == "aarch64-linux" then "sha256-bRH8EBD386jLfDCaOxksohVJHwupQxGPKiLHokT2dOA=" + else if system == "x86_64-darwin" then null # Built from pinned source; no upstream archive. + else if system == "aarch64-darwin" then "sha256-+siAmenWh+syFJnkOu8UGKTQb3rnLsugtf19OM8BPd0=" else throw "Unsupported system: ${system}"; - rustDate = "2026-05-31"; - leanVersion = "v4.30.0-rc2"; + rustDate = pkgs.lib.removePrefix "nightly-" rustToolchainName; + leanVersion = pkgs.lib.removePrefix "leanprover/lean4:" leanToolchainName; - rustToolchainSha256 = if system == "x86_64-linux" then "sha256-MmvOgC3shIOVMWT1MTRajw8JuLwRk/P3LsmGVslNGKw=" - else if system == "aarch64-linux" then "sha256-gWFajI7TJyjslQLZm4VWBBsKA6nYe1lNQwrgUp2hwSA=" - else if system == "x86_64-darwin" then "sha256-dBLHRLo3omD7KRq0D8lzg6XiQfDKWOMD6YTrLQhEneo=" - else if system == "aarch64-darwin" then "sha256-X7ndqbjsmnjL6KZzNCxkVFJPzAsAjUqerD/wc1rxK5E=" + rustToolchainSha256 = if system == "x86_64-linux" then "sha256-t9elSNKukvVVsD+GcDRNQeGewoz44Optv5j2+nJNY+s=" + else if system == "aarch64-linux" then "sha256-l4v7ANDsaFgoyB/rXOsZMMd1mS6Wv2KsGuCIBMipc/w=" + else if system == "x86_64-darwin" then "sha256-p5RO89GIzFtV6osz9clheFTBPZ4tkQy3l+Odj5S2uLU=" + else if system == "aarch64-darwin" then "sha256-EZuO4uLKLDngPCqs9+MWzhYLVVqi/6SWvZ08L4n9+lw=" else throw "Unsupported system: ${system}"; - leanToolchainSha256 = if system == "x86_64-linux" then "sha256-o47cQjSLK5YL8YZ2raaj+mGAvvO+dIDfVeP2L+WoyMs=" - else if system == "aarch64-linux" then "sha256-IrEGcTEeI1q0/7tLtMiiKPcW05JvaU8kNY6y5eprYg4=" - else if system == "x86_64-darwin" then "sha256-DDPmVkXjSLDr21LXcdvNkmGjD2v+sbUyY+REr3uylwI=" - else if system == "aarch64-darwin" then "sha256-dpUCCLkhoGDKkDKPZxr7WrmkifxHi4MWLpD148z2vhg=" + leanToolchainSha256 = if system == "x86_64-linux" then "sha256-B5ZDv1AMKN6M6zVLSL6nhDJ64R7ZxupuJvxfAbTn5hw=" + else if system == "aarch64-linux" then "sha256-HNVY4B6PIaGzfk5wURbNYGm/v5t7ZLz+uzHExKnLM6A=" + else if system == "x86_64-darwin" then "sha256-ntsUnj7dQ0h+zSg0Ez48N91x8sCu/bu/uuN5VrVecX0=" + else if system == "aarch64-darwin" then "sha256-DqRuJqtagp5LLhGw0sD7fuDzqOB93cbIdJOK70GoXmE=" else throw "Unsupported system: ${system}"; leantarPlatform = if system == "x86_64-linux" then "x86_64-unknown-linux-musl" @@ -66,11 +118,7 @@ else if system == "aarch64-darwin" then "sha256-tbWQ0vhC4jWZPsdW09vWCKE8iP1U02p7K2WjY7LuXjU=" else throw "Unsupported system: ${system}"; - mathlibCacheDownloadSha256 = if system == "x86_64-linux" then "sha256-n67tKjzZm5LsDU1Dl9kaOFKrQw+8YE201F0toYu1C3s=" - else if system == "aarch64-linux" then "sha256-9Yj5BAv6V5BTLd/nOWzIuqTDJPKwqR28bg7m9+46K98=" - else if system == "x86_64-darwin" then "sha256-DBdUmPfheeLTVwaVUzkB541Y9CWSQN6gmxBnJ3oxL4c=" - else if system == "aarch64-darwin" then "sha256-wv2NZcKiyYaW6L/o7+oHWZdYZhVYLzZjyQczoaHRJnk=" - else throw "Unsupported system: ${system}"; + mathlibCacheDownloadSha256 = "sha256-pNTivfyKQAjjdrOdds+OBcfReVtMxR0JWHcW9MFQSUM="; linuxDynamicLinker = if system == "x86_64-linux" then "/lib64/ld-linux-x86-64.so.2" else if system == "aarch64-linux" then "/lib/ld-linux-aarch64.so.1" @@ -225,11 +273,30 @@ }; in { - packages.aeneas-download = fetchAeneas { - target = aeneasTarget; - releaseTag = "nightly-2026.06.03"; - sha256 = aeneasSha256; - }; + packages.aeneas-download = + assert charonRevision == charonSourcePin; + assert pkgs.lib.hasPrefix "nightly-" rustToolchainName; + assert v1ToolchainMetadata.aeneas_rev == aeneasRevision; + assert v1ToolchainMetadata.lean_toolchain == leanToolchainName; + if system == "x86_64-darwin" then + pkgs.runCommand "aeneas-${aeneasTarget}.tar.gz" { + nativeBuildInputs = with pkgs; [ gnutar gzip ]; + passthru = { inherit toolchain portabilityInputs; }; + upstreamRelease = aeneas.packages.${system}.aeneas-release.overrideAttrs (old: { + nativeBuildInputs = (old.nativeBuildInputs or []) ++ [ pkgs.darwin.sigtool ]; + buildInputs = map (input: + if (input.pname or "") == "macdylibbundler" then darwinBundler + else input) (old.buildInputs or []); + }); + } '' + cd "$upstreamRelease" + tar -czf "$out" * + '' + else (fetchAeneas { + target = aeneasTarget; + releaseTag = aeneasReleaseTag; + sha256 = aeneasSha256; + }).overrideAttrs (_: { passthru = { inherit toolchain portabilityInputs; }; }); # Extracts the toolchain metadata implied by the Aeneas archive. packages.aeneas-unpacked = pkgs.stdenv.mkDerivation { @@ -255,14 +322,12 @@ " echo \"ERROR: could not parse Lean toolchain from Aeneas archive: \$LEAN_RAW\" >&2" " exit 1" "fi" - "RUST_DATE=${rustDate}" - "RUST_VERSION=\"nightly-\$RUST_DATE\"" - "cat < $out/metadata.json" - "{" - " \"lean-toolchain\": \"\$LEAN_VERSION\"," - " \"rust-toolchain-date\": \"\$RUST_DATE\"," - " \"rust-toolchain-version\": \"\$RUST_VERSION\"" - "}" + "if [ \"\$LEAN_VERSION\" != '${toolchainMetadata.lean-toolchain}' ]; then" + " echo \"ERROR: Aeneas release/source Lean pins differ\" >&2" + " exit 1" + "fi" + "cat > $out/metadata.json <<'EOF'" + (builtins.toJSON toolchainMetadata) "EOF" ]; }; @@ -340,11 +405,10 @@ "mkdir -p $out/packages" "cp -r .lake/packages/* $out/packages/" "chmod -R +w $out/packages" - # Drop only traces that captured Nix store paths. - "find $out/packages -type f \\( -name \"*.trace\" -o -name \"*.hash\" \\) \\" - " -exec grep -q \"/nix/store\" {} \\; -delete" - # Mathlib's build cache is reconstructed from .ltar archives below. - "rm -rf $out/packages/mathlib/.lake" + # Keep this download fixed-output derivation independent of the + # build root. Lake generates package caches while building the cache + # downloader; the .ltar archives restore them in the unpack stage. + "find $out/packages -type d -name \".lake\" -prune -exec rm -rf {} +" # Git metadata is unnecessary for path dependencies. "find $out/packages -type d -name \".git\" -exec rm -rf {} +" ]; @@ -471,7 +535,7 @@ "EOF" "substituteInPlace $TMPDIR/aeneas-config-primer/lakefile.lean --replace-fail @AENEAS_ROOT@ \"$PWD\"" "(cd $TMPDIR/aeneas-config-primer && ${runLeanCommand "lake --old build Generated"})" - "test -f .lake/config/aeneas/lakefile.olean" + "test -n \"\$(find .lake/config -type f -name lakefile.olean -print)\"" "python3 ${./rewrite-lake-vendor.py} --root . --packages-dir ../../packages --rewrite-traces --trace-prefix \"$leanToolchain=lean\"" "TRACE_ABS_RE='(^|[\"[:space:]=:])/(nix/store|build|private/tmp/nix-build|ANNEAL_PLACEHOLDER_ROOT)'" "if find . ../../packages -type f -name \"*.trace\" -exec grep -EIl \"\$TRACE_ABS_RE\" {} + | tee /tmp/non-relocatable-traces | grep -q .; then" @@ -483,10 +547,13 @@ "python3 ${./prune-lake-cache.py} --project-root . --packages-root ../../packages" "cd ../.." "mkdir -p $out/backends $out/packages" + "cp $aeneasUnpacked/metadata.json $out/metadata.json" "cp -r backends/lean $out/backends/" "cp -r packages/* $out/packages/" "mkdir -p $out/bin" "cp \$(find $aeneasUnpacked -maxdepth 1 -type f -executable) $out/bin/" + # Darwin release binaries load bundled libraries relative to bin. + "if [ -d $aeneasUnpacked/libs ]; then cp -r $aeneasUnpacked/libs $out/bin/; fi" ]; }; @@ -609,13 +676,12 @@ fi for path in \ + aeneas/metadata.json \ aeneas/bin/aeneas \ aeneas/bin/charon \ aeneas/bin/charon-driver \ - aeneas/backends/lean/.lake/config/aeneas/lakefile.olean \ aeneas/backends/lean/lakefile.lean \ aeneas/packages/mathlib/lake-manifest.json \ - aeneas/packages/mathlib/.lake/config/mathlib/lakefile.olean \ lean/bin/lean \ rust/bin/cargo \ rust/bin/rustc; do @@ -625,6 +691,13 @@ 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 + if ! grep -Eq '^aeneas/packages/mathlib/\.lake/build/lib/lean/Mathlib/.+\.olean$' "$TMPDIR/archive/entries"; then echo "ERROR: archive is missing Mathlib .olean cache artifacts" >&2 exit 1 diff --git a/anneal/v1/Cargo.toml b/anneal/v1/Cargo.toml index 43314cb4d3..694a83deee 100644 --- a/anneal/v1/Cargo.toml +++ b/anneal/v1/Cargo.toml @@ -103,15 +103,13 @@ similar = "2.7.0" [package.metadata.build_rs] -# The commit hash of the Aeneas repository to use. -# -# FIXME: Add a CI step to verify that this commit exists and matches the -# toolchain version. -aeneas_rev = "42c0e90dacf486f7d3ed5b6cde3a9a81f04915a4" +# Values embedded in V1's binary. The archive builder checks these against the +# authoritative Aeneas source pin in ../flake.nix and ../flake.lock. +aeneas_rev = "ca282ec2312a96f6a985a4d23a663690816d3f3e" # The Lean toolchain version to use. This must match the version of Lean used # by Aeneas in the `lean-toolchain` file in the commit above. -lean_toolchain = "leanprover/lean4:v4.30.0-rc2" +lean_toolchain = "leanprover/lean4:v4.31.0" [[test]] name = "integration" harness = false diff --git a/anneal/v1/examples/anatomy.rs b/anneal/v1/examples/anatomy.rs index e77e257b20..8d0aef6bd5 100644 --- a/anneal/v1/examples/anatomy.rs +++ b/anneal/v1/examples/anatomy.rs @@ -118,12 +118,12 @@ pub unsafe fn fast_add(a: usize, b: usize) -> usize { /// -- `h_returns : get_unaligned_fast_pad ... = ok ret` hypothesis binding them! /// have h_fast_pad_result : ret.val.val = 1 := by /// unfold get_unaligned_fast_pad at h_returns -/// -- When unwrapping monadic execution chains (e.g. evaluating `x = Result.ok y`), -/// -- standard rewrites fail. Always apply `rw [..., Aeneas.Std.bind_tc_ok]`! -/// rw [h_aspec, Aeneas.Std.bind_tc_ok] at h_returns +/// -- Generated monadic chains use `Aeneas.Std.bind`. Reduce successful +/// -- binds with `Aeneas.Std.bind_ok` after rewriting each call result. +/// rw [h_aspec, Aeneas.Std.bind_ok] at h_returns /// have h_valid : Anneal.IsValid.isValid h_layout.layout.align.val := by /// simp_all [Anneal.IsValid.isValid] -/// rw [fast_add_zero _ h_valid, Aeneas.Std.bind_tc_ok] at h_returns +/// rw [fast_add_zero _ h_valid, Aeneas.Std.bind_ok] at h_returns /// cases ret; simp_all /// /// -- `h_ret_is_valid` is implicitly demanded by Anneal for all generated structures. @@ -175,8 +175,8 @@ pub unsafe fn fast_add(a: usize, b: usize) -> usize { /// rcases h_add with ⟨padded, h_add_eq⟩ /// /// -- 3. Conclude progress -/// -- Chain evaluated states seamlessly using `bind_tc_ok`. -/// rw [h_align_eq, Aeneas.Std.bind_tc_ok, h_add_eq, Aeneas.Std.bind_tc_ok] +/// -- Chain evaluated states seamlessly using `bind_ok`. +/// rw [h_align_eq, Aeneas.Std.bind_ok, h_add_eq, Aeneas.Std.bind_ok] /// exact ⟨_, rfl⟩ /// ``` pub unsafe fn get_unaligned_fast_pad() -> PositiveUsize { diff --git a/anneal/v1/examples/size_of_align_of.rs b/anneal/v1/examples/size_of_align_of.rs index a2b882ae8c..285ddc5e45 100644 --- a/anneal/v1/examples/size_of_align_of.rs +++ b/anneal/v1/examples/size_of_align_of.rs @@ -30,8 +30,8 @@ pub fn get_align_of_empty_tuple() -> usize { /// ```anneal /// requires: ∃ (_sz : Anneal.core.marker.Sized T) (tl : Anneal.HasStaticLayout T), True -/// ensures: match core.mem.size_of T with -/// | Result.ok size => ret.val = size.val +/// ensures: match (core.mem.size_of T).match with +/// | .ok size => ret.val = size.val /// | _ => False /// proof: /// rcases h_anon with ⟨_sz, tl, _⟩ diff --git a/anneal/v1/llms-full.txt b/anneal/v1/llms-full.txt index 638245c821..8f0681ff86 100644 --- a/anneal/v1/llms-full.txt +++ b/anneal/v1/llms-full.txt @@ -1064,8 +1064,6 @@ instance {T : Type} : TrailingSlice (Aeneas.Std.Slice T) -/ instance {T : Type} : ReprC (Aeneas.Std.Slice T) -def test_has_layout : HasLayout Aeneas.Std.U16 - instance {T : Type} {M : Aeneas.Std.Mutability} : core.marker.Sized (Aeneas.Std.RawPtr T M) /-- diff --git a/anneal/v1/src/Anneal.lean b/anneal/v1/src/Anneal.lean index 727199a546..0ccf026a52 100644 --- a/anneal/v1/src/Anneal.lean +++ b/anneal/v1/src/Anneal.lean @@ -28,14 +28,11 @@ namespace Anneal -- We use Aeneas.Result -- We use `@[simp]` directly on the `SpecificationHolds` definition. --- This unrolls the match logic for underlying results without forcing +-- This unfolds the total-success specification for underlying results without forcing -- users to manually type `unfold Anneal.SpecificationHolds` uniformly across all project proofs. @[simp] def SpecificationHolds {α : Type} (res : Result α) (post : α → Prop) : Prop := - match res with - | .ok v => post v - | .fail _ => False -- A function satisfying spec should not fail - | .div => False -- A function satisfying spec should not diverge + WP.spec res post -- 2. Struct Invariants @@ -63,7 +60,7 @@ theorem wp_prove_orthogonal {α} {m : Result α} {P : α → Prop} : (∃ y, m = .ok y) → (∀ y, m = .ok y → P y) → WP.spec m P := by intro ⟨y, hy⟩ hP rw [hy] - exact hP y hy + exact (WP.spec_ok y).mpr (hP y hy) /-- A macro that evaluates progress automatically, or falls back to sorry/fail if stuck. -/ macro "eval_progress" msg:str fnc:ident : tactic => @@ -589,7 +586,7 @@ opaque align_char : Alignment @[simp] axiom align_char_divides : align_char.val.val ∣ 4 primitive_multibyte_layout Char 4 align_char align_char_divides -def test_has_layout : HasLayout Aeneas.Std.U16 := inferInstance +@[reducible] def test_has_layout : HasLayout Aeneas.Std.U16 := inferInstance -- Architecture-Dependent Primitives -- For `usize` and `isize`, both the size and alignment are platform-dependent. diff --git a/anneal/v1/src/aeneas.rs b/anneal/v1/src/aeneas.rs index 9b4618a209..48db26c935 100644 --- a/anneal/v1/src/aeneas.rs +++ b/anneal/v1/src/aeneas.rs @@ -942,7 +942,7 @@ fn patch_funs(content: &str) -> String { let mut lines: Vec<&str> = content.split('\n').collect(); let mut insert_idx = 0; for (i, line) in lines.iter().enumerate() { - if line.starts_with("import ") { + if line.starts_with("import ") || line.starts_with("public import ") { insert_idx = i + 1; } } diff --git a/anneal/v1/tests/fixtures/cfg_blind_spot/expected.stderr b/anneal/v1/tests/fixtures/cfg_blind_spot/expected.stderr index bedc7cba44..538b4fe51a 100644 --- a/anneal/v1/tests/fixtures/cfg_blind_spot/expected.stderr +++ b/anneal/v1/tests/fixtures/cfg_blind_spot/expected.stderr @@ -1,13 +1,17 @@ Compiling cfg_blind_spot v0.1.0 ([PROJECT_ROOT]) warning: failed to resolve item path `crate::ghost::hidden`: path `crate::ghost` does not correspond to any item + --> src/lib.rs:6:3 + | +6 | } + | ^ -thread 'rustc' () panicked at src/errors.rs:261:13: +thread 'rustc' () panicked at src/errors.rs:278:13: failed to resolve item path `crate::ghost::hidden`: path `crate::ghost` does not correspond to any item note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace ERROR Compilation panicked error: could not compile `cfg_blind_spot` (lib) Caused by: - process didn't exit successfully: `[CACHE_ROOT]/charon-driver rustc --crate-name cfg_blind_spot --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/deps -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/debug/deps --remap-path-prefix=tests/fixtures/cfg_blind_spot=/dummy` (exit status: 101) + process didn't exit successfully: `[CACHE_ROOT]/charon-driver charon-dont-cache-this- rustc --crate-name cfg_blind_spot --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat,unused-externs-silent --crate-type lib --emit=dep-info,metadata,link -Z embed-metadata=no -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/build/cfg_blind_spot//out --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/debug/build/cfg_blind_spot//out --remap-path-prefix=tests/fixtures/cfg_blind_spot=/dummy --force-warn=unused_crate_dependencies` (exit status: 101) Error: Charon failed with status: exit status: 101 diff --git a/anneal/v1/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr b/anneal/v1/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr index 2005837595..f4cda4bcb6 100644 --- a/anneal/v1/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr +++ b/anneal/v1/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr @@ -1,13 +1,17 @@ Compiling test_7_1_phantom_fn v0.1.0 ([PROJECT_ROOT]) warning: failed to resolve item path `crate::windows_only`: path `crate::windows_only` does not correspond to any item + --> src/lib.rs:13:24 + | +13 | pub fn linux_only() {} + | ^ -thread 'rustc' () panicked at src/errors.rs:261:13: +thread 'rustc' () panicked at src/errors.rs:278:13: failed to resolve item path `crate::windows_only`: path `crate::windows_only` does not correspond to any item note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace ERROR Compilation panicked error: could not compile `test_7_1_phantom_fn` (lib) Caused by: - process didn't exit successfully: `[CACHE_ROOT]/charon-driver rustc --crate-name test_7_1_phantom_fn --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/deps -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/debug/deps --remap-path-prefix=tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn=/dummy` (exit status: 101) + process didn't exit successfully: `[CACHE_ROOT]/charon-driver charon-dont-cache-this- rustc --crate-name test_7_1_phantom_fn --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat,unused-externs-silent --crate-type lib --emit=dep-info,metadata,link -Z embed-metadata=no -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/build/test_7_1_phantom_fn//out --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/debug/build/test_7_1_phantom_fn//out --remap-path-prefix=tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn=/dummy --force-warn=unused_crate_dependencies` (exit status: 101) Error: Charon failed with status: exit status: 101 diff --git a/anneal/v1/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr b/anneal/v1/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr index c31f163856..580f0adac3 100644 --- a/anneal/v1/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr +++ b/anneal/v1/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr @@ -6,12 +6,12 @@ warning: failed to resolve item path `crate::windows_only`: path `crate::windows | ^ -thread 'rustc' () panicked at src/errors.rs:261:13: +thread 'rustc' () panicked at src/errors.rs:278:13: failed to resolve item path `crate::windows_only`: path `crate::windows_only` does not correspond to any item note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace ERROR Compilation panicked error: could not compile `test_7_3_ghost_spec` (lib) Caused by: - process didn't exit successfully: `[CACHE_ROOT]/charon-driver rustc --crate-name test_7_3_ghost_spec --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/deps -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/debug/deps --remap-path-prefix=tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec=/dummy` (exit status: 101) + process didn't exit successfully: `[CACHE_ROOT]/charon-driver charon-dont-cache-this- rustc --crate-name test_7_3_ghost_spec --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat,unused-externs-silent --crate-type lib --emit=dep-info,metadata,link -Z embed-metadata=no -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/build/test_7_3_ghost_spec//out --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/debug/build/test_7_3_ghost_spec//out --remap-path-prefix=tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec=/dummy --force-warn=unused_crate_dependencies` (exit status: 101) Error: Charon failed with status: exit status: 101 diff --git a/anneal/v1/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr b/anneal/v1/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr index 2a2b6ed630..dcd49d11a6 100644 --- a/anneal/v1/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr +++ b/anneal/v1/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr @@ -14,8 +14,8 @@ Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 Called from Aeneas__TypesAnalysis.analyze_type_declaration_group.analyze in file "llbc/TypesAnalysis.ml", lines 565-567, characters 6-23 Called from Aeneas__Interp.analyze_type_declarations.(fun) in file "interp/Interp.ml", line 31, characters 10-62 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 -Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 149, characters 19-66 -Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 313, characters 18-40 -Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2131, characters 31-71 -Called from Dune__exe__Main in file "Main.ml", lines 738-739, characters 8-37 +Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 157, characters 19-66 +Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 321, characters 18-40 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2199, characters 31-71 +Called from Dune__exe__Main in file "Main.ml", lines 765-766, characters 8-37 diff --git a/anneal/v1/tests/fixtures/expand_output/expected-aeneas.stdout b/anneal/v1/tests/fixtures/expand_output/expected-aeneas.stdout index db30a24a2e..61d6c12b39 100644 --- a/anneal/v1/tests/fixtures/expand_output/expected-aeneas.stdout +++ b/anneal/v1/tests/fixtures/expand_output/expected-aeneas.stdout @@ -2,11 +2,16 @@ --- Aeneas --- -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [expand_output]: type definitions -import Aeneas +module +public import Aeneas +@[expose] public section open Aeneas Aeneas.Std Result ControlFlow Error set_option linter.dupNamespace false set_option linter.hashCommand false set_option linter.unusedVariables false +set_option linter.style.whitespace false +set_option linter.style.setOption false +set_option linter.style.longLine false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 @@ -20,14 +25,19 @@ end expand_output -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [expand_output]: function definitions -import Aeneas -import ExpandOutputExpandOutput1d49e11e5683007f.Types +module +public import Aeneas +public import ExpandOutputExpandOutput1d49e11e5683007f.Types noncomputable section +@[expose] public section open Aeneas Aeneas.Std Result ControlFlow Error set_option linter.dupNamespace false set_option linter.hashCommand false set_option linter.unusedVariables false +set_option linter.style.whitespace false +set_option linter.style.setOption false +set_option linter.style.longLine false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 diff --git a/anneal/v1/tests/fixtures/expand_output/expected-all.stdout b/anneal/v1/tests/fixtures/expand_output/expected-all.stdout index b4934dc041..c619538ce5 100644 --- a/anneal/v1/tests/fixtures/expand_output/expected-all.stdout +++ b/anneal/v1/tests/fixtures/expand_output/expected-all.stdout @@ -2,11 +2,16 @@ --- Aeneas --- -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [expand_output]: type definitions -import Aeneas +module +public import Aeneas +@[expose] public section open Aeneas Aeneas.Std Result ControlFlow Error set_option linter.dupNamespace false set_option linter.hashCommand false set_option linter.unusedVariables false +set_option linter.style.whitespace false +set_option linter.style.setOption false +set_option linter.style.longLine false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 @@ -20,14 +25,19 @@ end expand_output -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [expand_output]: function definitions -import Aeneas -import ExpandOutputExpandOutput1d49e11e5683007f.Types +module +public import Aeneas +public import ExpandOutputExpandOutput1d49e11e5683007f.Types noncomputable section +@[expose] public section open Aeneas Aeneas.Std Result ControlFlow Error set_option linter.dupNamespace false set_option linter.hashCommand false set_option linter.unusedVariables false +set_option linter.style.whitespace false +set_option linter.style.setOption false +set_option linter.style.longLine false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 diff --git a/anneal/v1/tests/fixtures/extern_never_verified/out.txt b/anneal/v1/tests/fixtures/extern_never_verified/out.txt index 9cf7a9e663..db2cbc41e3 100644 --- a/anneal/v1/tests/fixtures/extern_never_verified/out.txt +++ b/anneal/v1/tests/fixtures/extern_never_verified/out.txt @@ -2,11 +2,16 @@ --- Aeneas --- -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [extern_never_verified]: type definitions -import Aeneas +module +public import Aeneas +@[expose] public section open Aeneas Aeneas.Std Result ControlFlow Error set_option linter.dupNamespace false set_option linter.hashCommand false set_option linter.unusedVariables false +set_option linter.style.whitespace false +set_option linter.style.setOption false +set_option linter.style.longLine false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 @@ -32,15 +37,20 @@ end extern_never_verified -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [extern_never_verified]: function definitions -import Aeneas -import ExternNeverVerifiedExternNeverVerified7818cfb81635275f.Types -import ExternNeverVerifiedExternNeverVerified7818cfb81635275f.FunsExternal +module +public import Aeneas +public import ExternNeverVerifiedExternNeverVerified7818cfb81635275f.Types +public import ExternNeverVerifiedExternNeverVerified7818cfb81635275f.FunsExternal noncomputable section +@[expose] public section open Aeneas Aeneas.Std Result ControlFlow Error set_option linter.dupNamespace false set_option linter.hashCommand false set_option linter.unusedVariables false +set_option linter.style.whitespace false +set_option linter.style.setOption false +set_option linter.style.longLine false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 @@ -88,12 +98,17 @@ end extern_never_verified -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [extern_never_verified]: external functions. -- This is a template file: rename it to "FunsExternal.lean" and fill the holes. -import Aeneas -import ExternNeverVerifiedExternNeverVerified7818cfb81635275f.Types +module +public import Aeneas +public import ExternNeverVerifiedExternNeverVerified7818cfb81635275f.Types +@[expose] public section open Aeneas Aeneas.Std Result ControlFlow Error set_option linter.dupNamespace false set_option linter.hashCommand false set_option linter.unusedVariables false +set_option linter.style.whitespace false +set_option linter.style.setOption false +set_option linter.style.longLine false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 diff --git a/anneal/v1/tests/fixtures/raw_ptr_dst_layout/expected.stderr b/anneal/v1/tests/fixtures/raw_ptr_dst_layout/expected.stderr index e94373076c..7bb1f562b7 100644 --- a/anneal/v1/tests/fixtures/raw_ptr_dst_layout/expected.stderr +++ b/anneal/v1/tests/fixtures/raw_ptr_dst_layout/expected.stderr @@ -9,7 +9,7 @@ 29 │ /// · exact {} ╰──── - × Goal is not a `spec m P` + × Exists is not a supported spec statement ╭─[[PROJECT_ROOT]/src/lib.rs:28:7] 27 │ /// unfold test_slice at * 28 │ /// progress with raw_ptr_dst_layout.size_of_val_raw.spec as ⟨ i, i_post ⟩ diff --git a/anneal/v1/tests/fixtures/split_artifact/expected.stderr b/anneal/v1/tests/fixtures/split_artifact/expected.stderr index eef1af957a..e6a5a5a39f 100644 --- a/anneal/v1/tests/fixtures/split_artifact/expected.stderr +++ b/anneal/v1/tests/fixtures/split_artifact/expected.stderr @@ -8,14 +8,18 @@ Compiling split v0.1.0 ([PROJECT_ROOT]) warning: failed to resolve item path `crate::main`: path `crate::main` does not correspond to any item + --> src/lib.rs:3:16 + | +3 | fn my_lib() {} + | ^ -thread 'rustc' () panicked at src/errors.rs:261:13: +thread 'rustc' () panicked at src/errors.rs:278:13: failed to resolve item path `crate::main`: path `crate::main` does not correspond to any item note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace ERROR Compilation panicked error: could not compile `split` (lib) Caused by: - process didn't exit successfully: `[CACHE_ROOT]/charon-driver rustc --crate-name split --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/deps -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/debug/deps --remap-path-prefix=tests/fixtures/split_artifact=/dummy` (exit status: 101) + process didn't exit successfully: `[CACHE_ROOT]/charon-driver charon-dont-cache-this- rustc --crate-name split --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat,unused-externs-silent --crate-type lib --emit=dep-info,metadata,link -Z embed-metadata=no -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/build/split//out --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/debug/build/split//out --remap-path-prefix=tests/fixtures/split_artifact=/dummy --force-warn=unused_crate_dependencies` (exit status: 101) Error: Charon failed with status: exit status: 101 diff --git a/anneal/v1/tests/fixtures/target_selection/expected.stderr b/anneal/v1/tests/fixtures/target_selection/expected.stderr index a39640c126..3495d8143a 100644 --- a/anneal/v1/tests/fixtures/target_selection/expected.stderr +++ b/anneal/v1/tests/fixtures/target_selection/expected.stderr @@ -1,13 +1,17 @@ Compiling selector v0.1.0 ([PROJECT_ROOT]) warning: failed to resolve item path `crate::_anneal_dummy`: path `crate::_anneal_dummy` does not correspond to any item + --> src/lib.rs:3:2 + | +3 | + | ^ -thread 'rustc' () panicked at src/errors.rs:261:13: +thread 'rustc' () panicked at src/errors.rs:278:13: failed to resolve item path `crate::_anneal_dummy`: path `crate::_anneal_dummy` does not correspond to any item note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace ERROR Compilation panicked error: could not compile `selector` (lib) Caused by: - process didn't exit successfully: `[CACHE_ROOT]/charon-driver rustc --crate-name selector --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/deps -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/debug/deps --remap-path-prefix=tests/fixtures/target_selection=/dummy` (exit status: 101) + process didn't exit successfully: `[CACHE_ROOT]/charon-driver charon-dont-cache-this- rustc --crate-name selector --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat,unused-externs-silent --crate-type lib --emit=dep-info,metadata,link -Z embed-metadata=no -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/build/selector//out --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/debug/build/selector//out --remap-path-prefix=tests/fixtures/target_selection=/dummy --force-warn=unused_crate_dependencies` (exit status: 101) Error: Charon failed with status: exit status: 101 diff --git a/anneal/v1/tests/fixtures/ui_silent_panic/expected.stderr b/anneal/v1/tests/fixtures/ui_silent_panic/expected.stderr index 2b6f04fe4f..60ad4b74ad 100644 --- a/anneal/v1/tests/fixtures/ui_silent_panic/expected.stderr +++ b/anneal/v1/tests/fixtures/ui_silent_panic/expected.stderr @@ -2,7 +2,7 @@ error: failed to run custom build command for `test_pkg v0.1.0 ([PROJECT_ROOT])` Caused by: - process didn't exit successfully: `[PROJECT_ROOT]/target/anneal/cargo_target/debug/build/test_pkg-/build-script-build` (exit status: 101) + process didn't exit successfully: `[PROJECT_ROOT]/target/anneal/cargo_target/debug/build/test_pkg//out/build_script_build` (exit status: 101) --- stderr thread 'main' () panicked at build.rs:1:13: diff --git a/anneal/v1/tests/fixtures/unions/expected.stderr b/anneal/v1/tests/fixtures/unions/expected.stderr index cd365777ec..a471e851da 100644 --- a/anneal/v1/tests/fixtures/unions/expected.stderr +++ b/anneal/v1/tests/fixtures/unions/expected.stderr @@ -14,8 +14,8 @@ Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 Called from Aeneas__TypesAnalysis.analyze_type_declaration_group.analyze in file "llbc/TypesAnalysis.ml", lines 565-567, characters 6-23 Called from Aeneas__Interp.analyze_type_declarations.(fun) in file "interp/Interp.ml", line 31, characters 10-62 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 -Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 149, characters 19-66 -Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 313, characters 18-40 -Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2131, characters 31-71 -Called from Dune__exe__Main in file "Main.ml", lines 738-739, characters 8-37 +Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 157, characters 19-66 +Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 321, characters 18-40 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2199, characters 31-71 +Called from Dune__exe__Main in file "Main.ml", lines 765-766, characters 8-37 diff --git a/anneal/v1/tests/fixtures/weird_functions/expected.stderr b/anneal/v1/tests/fixtures/weird_functions/expected.stderr index 4e22d5c3b6..85019cb234 100644 --- a/anneal/v1/tests/fixtures/weird_functions/expected.stderr +++ b/anneal/v1/tests/fixtures/weird_functions/expected.stderr @@ -6,7 +6,7 @@ warning: Coroutine types are not supported yet | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -thread 'rustc' () panicked at src/errors.rs:261:13: +thread 'rustc' () panicked at src/errors.rs:278:13: Coroutine types are not supported yet note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace warning: Thread panicked when extracting item `weird::async_foo`. @@ -16,11 +16,11 @@ warning: Thread panicked when extracting item `weird::async_foo`. | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -thread 'rustc' () panicked at src/errors.rs:261:13: +thread 'rustc' () panicked at src/errors.rs:278:13: Thread panicked when extracting item `weird::async_foo`. ERROR Compilation panicked error: could not compile `weird` (lib) Caused by: - process didn't exit successfully: `[CACHE_ROOT]/charon-driver rustc --crate-name weird --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/deps -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/debug/deps --remap-path-prefix=tests/fixtures/weird_functions=/dummy` (exit status: 101) + process didn't exit successfully: `[CACHE_ROOT]/charon-driver charon-dont-cache-this- rustc --crate-name weird --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat,unused-externs-silent --crate-type lib --emit=dep-info,metadata,link -Z embed-metadata=no -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/build/weird//out --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/anneal/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/anneal/cargo_target/debug/build/weird//out --remap-path-prefix=tests/fixtures/weird_functions=/dummy --force-warn=unused_crate_dependencies` (exit status: 101) Error: Charon failed with status: exit status: 101 diff --git a/anneal/v1/tests/integration.rs b/anneal/v1/tests/integration.rs index 8fc6f6b9b4..6a75e04175 100644 --- a/anneal/v1/tests/integration.rs +++ b/anneal/v1/tests/integration.rs @@ -317,7 +317,15 @@ fn assert_archive_lake_cache_reuse( fs::create_dir_all(workspace.join("generated"))?; fs::copy(aeneas_lean.join("lean-toolchain"), workspace.join("lean-toolchain"))?; - fs::write(workspace.join("generated/Generated.lean"), "import Aeneas\n")?; + // Compile the actual embedded prelude, then check its success predicate + // against the historical definition. This also tests that user proofs can + // import that prelude using the archive's read-only dependency caches. + fs::write(workspace.join("generated/Anneal.lean"), include_str!("../src/Anneal.lean"))?; + fs::write( + workspace.join("generated/SpecificationHolds.lean"), + include_str!("lean/SpecificationHolds.lean"), + )?; + fs::write(workspace.join("generated/Generated.lean"), "import SpecificationHolds\n")?; fs::write( workspace.join("lakefile.lean"), format!( @@ -331,7 +339,7 @@ package anneal_verification @[default_target] lean_lib Generated where srcDir := "generated" - roots := #[`Generated] + roots := #[`Generated, `Anneal, `SpecificationHolds] "#, lake_string(&aeneas_lean) ), @@ -1873,6 +1881,8 @@ fn sanitize_output(output: &str) -> String { let re_file_lock = regex::Regex::new(r"(?m)^.*Blocking waiting for file lock on.*$\n?").unwrap(); let re_cargo_hash = regex::Regex::new(r"([-=_])([a-f0-9]{5,16})\b").unwrap(); + let re_charon_nonce = regex::Regex::new(r"charon-dont-cache-this-[a-f0-9]+-\d+").unwrap(); + let re_cargo_build_hash = regex::Regex::new(r"(/debug/build/[^/]+/)[a-f0-9]{16}(/)").unwrap(); let re_timing = regex::Regex::new(r"took \d+(\.\d*)?(m?s)").unwrap(); let re_lake_timing = regex::Regex::new(r"\(\d+(\.\d*)?m?s\)").unwrap(); @@ -1893,6 +1903,8 @@ fn sanitize_output(output: &str) -> String { clean = re_thread_id.replace_all(&clean, "thread '$1' () panicked").into_owned(); clean = re_file_lock.replace_all(&clean, "").into_owned(); + clean = re_charon_nonce.replace_all(&clean, "charon-dont-cache-this-").into_owned(); + clean = re_cargo_build_hash.replace_all(&clean, "${1}${2}").into_owned(); clean = re_cargo_hash.replace_all(&clean, "${1}").into_owned(); clean = re_timing.replace_all(&clean, "took