From 1ed582696e43fa0d1e21d0d7c7f18d38e426733e Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Wed, 7 Oct 2026 16:37:37 -0400 Subject: [PATCH] Update Anneal to Aeneas ca282ec and Lean 4.31 Anneal's older extraction toolchain cannot share the newer backend used by zerocopy verification. Pin Aeneas ca282ec2312a96f6a985a4d23a663690816d3f3e and derive Charon, Rust and Lean versions from that upstream source and lock. Check V1's embedded version metadata against the archive builder. Retain all four release platforms, building and signing the missing Intel Mac archive from pinned source. Normalize downloaded Mathlib build inputs and rebuild relocatable caches for the updated toolchain. Keep V1's SpecificationHolds interface as an alias for Aeneas WP.spec. An exhaustive, kernel-checked comparison establishes equivalence to the previous success/failure/divergence predicate without using V1's Rust axioms. Compile the actual embedded prelude in the relocated archive test and refresh the extraction and diagnostic fixtures for the new versions. gherrit-pr-id: G7btlodhfbdy3pcw7qjdrj2okvowiex7l Agent-authored-by: AI agent acting on joshlf's behalf --- .github/workflows/anneal-release.yml | 1 + anneal/flake.lock | 239 +++++++++++++++++- anneal/flake.nix | 155 +++++++++--- anneal/v1/Cargo.toml | 10 +- anneal/v1/examples/anatomy.rs | 12 +- anneal/v1/examples/size_of_align_of.rs | 4 +- anneal/v1/llms-full.txt | 2 - anneal/v1/src/Anneal.lean | 11 +- anneal/v1/src/aeneas.rs | 2 +- .../fixtures/cfg_blind_spot/expected.stderr | 8 +- .../test_7_1_phantom_fn/expected.stderr | 8 +- .../test_7_3_ghost_spec/expected.stderr | 4 +- .../test_8_2_unions/expected.stderr | 8 +- .../expand_output/expected-aeneas.stdout | 16 +- .../expand_output/expected-all.stdout | 16 +- .../fixtures/extern_never_verified/out.txt | 27 +- .../raw_ptr_dst_layout/expected.stderr | 2 +- .../fixtures/split_artifact/expected.stderr | 8 +- .../fixtures/target_selection/expected.stderr | 8 +- .../fixtures/ui_silent_panic/expected.stderr | 2 +- .../v1/tests/fixtures/unions/expected.stderr | 8 +- .../fixtures/weird_functions/expected.stderr | 6 +- anneal/v1/tests/integration.rs | 16 +- anneal/v1/tests/lean/SpecificationHolds.lean | 88 +++++++ 24 files changed, 557 insertions(+), 104 deletions(-) create mode 100644 anneal/v1/tests/lean/SpecificationHolds.lean 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