Skip to content

Commit 302e843

Browse files
committed
[anneal][v1] Preserve the Darwin native translation tool closure
Keep downloaded Darwin producer bytes intact until explicit private staging, retain the release GMP provider beside Aeneas, and relocate/sign the Rust and Aeneas native closure coherently. Correct the Darwin Rust archive hashes for the preserved producer bytes. Validation: the 68 publisher/native staging unit tests pass. The native helper and final downloader recipe preserve previously accepted RC2/macOS translation behavior. gherrit-pr-id: G246gdcbsz2wjddnwbpl2g567g3kxnlx2 Agent-authored-by: AI agent acting on joshlf's behalf
1 parent 5b12697 commit 302e843

4 files changed

Lines changed: 453 additions & 6 deletions

File tree

‎.github/workflows/anneal.yml‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,8 @@ jobs:
6565
anneal/v1/tools/update-exocrate-metadata.py \
6666
anneal/tests/test_prune_lake_cache.py \
6767
anneal/prune-lake-cache.py \
68+
anneal/prepare-native-tools.py \
69+
anneal/tests/test_prepare_native_tools.py \
6870
anneal/rewrite-lake-vendor.py
6971
python3 -m unittest discover -s anneal/v1/tools -p 'test_*.py'
7072
python3 -m unittest discover -s anneal/tests -p 'test_*.py'
@@ -289,7 +291,7 @@ jobs:
289291
uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
290292
with:
291293
path: anneal/target/nix-cache-main
292-
key: anneal-v2-main-nix-cache-v2-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('anneal/flake.nix', 'anneal/flake.lock', 'anneal/rewrite-lake-vendor.py', 'anneal/prune-lake-cache.py') }}
294+
key: anneal-v2-main-nix-cache-v2-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('anneal/flake.nix', 'anneal/flake.lock', 'anneal/rewrite-lake-vendor.py', 'anneal/prune-lake-cache.py', 'anneal/prepare-native-tools.py') }}
293295

294296
# Pull request caches are scoped by GitHub to the PR merge ref, so they
295297
# can speed up repeated pushes to the same PR without becoming visible to
@@ -309,7 +311,7 @@ jobs:
309311
uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
310312
with:
311313
path: anneal/target/nix-cache-pr
312-
key: anneal-v2-pr-nix-cache-v1-${{ runner.os }}-${{ runner.arch }}-pr-${{ github.event.pull_request.number }}-${{ hashFiles('anneal/flake.nix', 'anneal/flake.lock', 'anneal/rewrite-lake-vendor.py', 'anneal/prune-lake-cache.py') }}
314+
key: anneal-v2-pr-nix-cache-v1-${{ runner.os }}-${{ runner.arch }}-pr-${{ github.event.pull_request.number }}-${{ hashFiles('anneal/flake.nix', 'anneal/flake.lock', 'anneal/rewrite-lake-vendor.py', 'anneal/prune-lake-cache.py', 'anneal/prepare-native-tools.py') }}
313315

314316
- name: Install Nix
315317
uses: DeterminateSystems/determinate-nix-action@4d65ea9cab522b6d9f29a170aed23ededc1b27af # v3.23.0

‎anneal/flake.nix‎

Lines changed: 41 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -44,8 +44,8 @@
4444

4545
rustToolchainSha256 = if system == "x86_64-linux" then "sha256-MmvOgC3shIOVMWT1MTRajw8JuLwRk/P3LsmGVslNGKw="
4646
else if system == "aarch64-linux" then "sha256-gWFajI7TJyjslQLZm4VWBBsKA6nYe1lNQwrgUp2hwSA="
47-
else if system == "x86_64-darwin" then "sha256-dBLHRLo3omD7KRq0D8lzg6XiQfDKWOMD6YTrLQhEneo="
48-
else if system == "aarch64-darwin" then "sha256-X7ndqbjsmnjL6KZzNCxkVFJPzAsAjUqerD/wc1rxK5E="
47+
else if system == "x86_64-darwin" then "sha256-VRNaD18Q5TOUwgLETnF40xm5HsKIZ22eDaDD/uoaots="
48+
else if system == "aarch64-darwin" then "sha256-N6Ce8oiYRg/Twaz6X7VFGvgA2pXKOBjiAZCHxXYwMQk="
4949
else throw "Unsupported system: ${system}";
5050

5151
leanToolchainSha256 = if system == "x86_64-linux" then "sha256-o47cQjSLK5YL8YZ2raaj+mGAvvO+dIDfVeP2L+WoyMs="
@@ -104,12 +104,15 @@
104104

105105
# Fixed-output downloader used for toolchain assets.
106106
fetchToolchainAsset = { pname, version, sha256, buildPhase }:
107-
pkgs.stdenv.mkDerivation {
107+
pkgs.stdenv.mkDerivation ({
108108
pname = "${pname}-${system}";
109109
inherit version sha256 buildPhase;
110110

111111
dontUnpack = true;
112112

113+
# Preserve upstream Darwin install names and signatures at the
114+
# first producer; relocation belongs to the private archive stage.
115+
dontFixup = pkgs.stdenv.isDarwin;
113116
# Keep downloaded toolchains byte-for-byte independent of the builder.
114117
dontPatchShebangs = true;
115118
dontPatchELF = true;
@@ -128,7 +131,21 @@
128131
];
129132

130133
SSL_CERT_FILE = "${pkgs.cacert}/etc/ssl/certs/ca-bundle.crt";
131-
};
134+
} // pkgs.lib.optionalAttrs pkgs.stdenv.isDarwin {
135+
# Run only the downloaded-tree recipe, without stdenv setup hooks.
136+
__structuredAttrs = false;
137+
realBuilder = "${pkgs.bash}/bin/bash";
138+
args = [ "-e" (pkgs.writeText "anneal-${pname}-${system}-raw-builder" ''
139+
set -euo pipefail
140+
shopt -s inherit_errexit
141+
umask 022
142+
export PATH="${pkgs.lib.makeBinPath (with pkgs; [ curl gnutar gzip zstd coreutils findutils ])}"
143+
build_toolchain() {
144+
${buildPhase}
145+
}
146+
build_toolchain
147+
'') ];
148+
});
132149

133150
# Merge the Rust components into one sysroot.
134151
fetchRustToolchain = { rustDate, sha256 }:
@@ -236,6 +253,10 @@
236253
pname = "aeneas-unpacked";
237254
version = "1.0.0";
238255

256+
# This is the first output containing the release Mach-O files.
257+
# Preserve their load commands and signatures until native staging.
258+
dontFixup = pkgs.stdenv.isDarwin;
259+
239260
src = self.packages.${system}.aeneas-download;
240261

241262
nativeBuildInputs = with pkgs; [
@@ -391,6 +412,10 @@
391412
pname = "aeneas-compiled";
392413
version = "0.1.0";
393414

415+
# Preserve upstream Darwin signatures and native producer bytes;
416+
# relocation/signing happens explicitly in fresh omnibus staging.
417+
dontFixup = pkgs.stdenv.isDarwin;
418+
394419
src = pkgs.runCommand "empty-src" {} "mkdir $out";
395420

396421
leanToolchain = self.packages.${system}.lean-toolchain;
@@ -487,6 +512,8 @@
487512
"cp -r packages/* $out/packages/"
488513
"mkdir -p $out/bin"
489514
"cp \$(find $aeneasUnpacked -maxdepth 1 -type f -executable) $out/bin/"
515+
# Aeneas resolves release libraries relative to its executable.
516+
"if [ -d $aeneasUnpacked/libs ]; then cp -a $aeneasUnpacked/libs $out/bin/libs; fi"
490517
];
491518
};
492519

@@ -499,6 +526,7 @@
499526

500527
nativeBuildInputs = with pkgs; [
501528
gnutar
529+
python3
502530
] ++ pkgs.lib.optionals stdenv.isLinux [
503531
patchelf
504532
file
@@ -533,6 +561,8 @@
533561
" strip \"\$file\" || true"
534562
" fi"
535563
"done"
564+
] ++ pkgs.lib.optionals pkgs.stdenv.isDarwin [
565+
"python3 ${./prepare-native-tools.py} --root $TMPDIR/dist_staging --platform ${system}"
536566
] ++ [
537567
"TRACE_ABS_RE='(^|[\"[:space:]=:])/(nix/store|build|private/tmp/nix-build|ANNEAL_PLACEHOLDER_ROOT)'"
538568
"if find $TMPDIR/dist_staging -type f -name \"*.trace\" -exec grep -EIl \"\$TRACE_ABS_RE\" {} + | tee /tmp/non-relocatable-staged-traces | grep -q .; then"
@@ -625,6 +655,13 @@
625655
fi
626656
done
627657
658+
${pkgs.lib.optionalString pkgs.stdenv.isDarwin ''
659+
if ! grep -Fxq 'aeneas/bin/libs/libgmp.10.dylib' "$TMPDIR/archive/entries"; then
660+
echo "ERROR: archive is missing Aeneas's upstream GMP provider" >&2
661+
exit 1
662+
fi
663+
''}
664+
628665
if ! grep -Eq '^aeneas/packages/mathlib/\.lake/build/lib/lean/Mathlib/.+\.olean$' "$TMPDIR/archive/entries"; then
629666
echo "ERROR: archive is missing Mathlib .olean cache artifacts" >&2
630667
exit 1

‎anneal/prepare-native-tools.py‎

Lines changed: 173 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,173 @@
1+
#!/usr/bin/env python3
2+
# Copyright 2026 The Fuchsia Authors
3+
#
4+
# Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
5+
# <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
6+
# license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
7+
# This file may not be copied, modified, or distributed except according to
8+
# those terms.
9+
"""Relocate and statically check Darwin translation tools in new archive staging.
10+
11+
Never invokes translated tools, compilers, or the Lean SDK publisher. This is
12+
separate from the Lean-consumed closure and its identity. System libraries are
13+
an explicit Darwin platform assumption; this is not dynamic ABI acceptance.
14+
"""
15+
import argparse
16+
from pathlib import Path
17+
import re
18+
import subprocess
19+
20+
21+
def tool(name, *args):
22+
return subprocess.run(['/usr/bin/' + name, *map(str, args)], check=True,
23+
capture_output=True, text=True, timeout=60,
24+
env={'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'LC_ALL': 'C'}).stdout
25+
26+
27+
def loads(text):
28+
result = {'needed': [], 'rpaths': [], 'identity': None, 'interpreter': None,
29+
'code_signature': False}
30+
command = None
31+
for line in text.splitlines():
32+
line = line.strip()
33+
if line.startswith('cmd '):
34+
command = line.split()[1]
35+
if command == 'LC_CODE_SIGNATURE':
36+
result['code_signature'] = True
37+
elif line.startswith('name ') and command:
38+
name = line[5:].rsplit(' (offset ', 1)[0]
39+
if command == 'LC_ID_DYLIB':
40+
result['identity'] = name
41+
elif command == 'LC_LOAD_DYLINKER':
42+
result['interpreter'] = name
43+
elif command in {'LC_LOAD_DYLIB', 'LC_LOAD_WEAK_DYLIB', 'LC_REEXPORT_DYLIB', 'LC_LOAD_UPWARD_DYLIB', 'LC_LAZY_LOAD_DYLIB'}:
44+
result['needed'].append(name)
45+
elif line.startswith('path ') and command == 'LC_RPATH':
46+
result['rpaths'].append(line[5:].rsplit(' (offset ', 1)[0])
47+
return result
48+
49+
50+
def changes(name, dependencies, symbols):
51+
result = {}
52+
for dependency in dependencies:
53+
replacement = None
54+
if name in {'charon', 'charon-driver'}:
55+
if re.fullmatch(r'/nix/store/[^/]+-libiconv-109/lib/libiconv\.2\.dylib', dependency):
56+
replacement = '/usr/lib/libiconv.2.dylib'
57+
elif name == 'charon-driver' and re.fullmatch(r'/nix/store/[^/]+-zlib-1\.3\.1/lib/libz\.dylib', dependency):
58+
replacement = '/usr/lib/libz.1.dylib'
59+
elif name == 'charon-driver' and re.fullmatch(r'@rpath/librustc_driver-[0-9a-f]+\.dylib', dependency):
60+
# System shell shims on macOS strip DYLD_LIBRARY_PATH. The
61+
# archive already fixes this provider beside the tools.
62+
result[dependency] = '@loader_path/../../rust/lib/' + dependency[len('@rpath/'):]
63+
continue
64+
if replacement:
65+
family = 'libiconv' if 'iconv' in replacement else 'libz'
66+
if re.search(r'\(from ' + family + r'[^)]*\)', symbols):
67+
raise ValueError('system substitution needs a new ABI review: ' + dependency)
68+
result[dependency] = replacement
69+
return result
70+
71+
72+
def system(reference):
73+
return '..' not in Path(reference).parts and reference.startswith(('/usr/lib/', '/System/Library/Frameworks/'))
74+
75+
76+
def owned(path, root):
77+
path = path.resolve(strict=True)
78+
if not path.is_file() or not any(path.is_relative_to(root / family) for family in ('aeneas/bin', 'rust/lib')):
79+
raise ValueError('native provider escapes owned archive payload: ' + str(path))
80+
return path
81+
82+
83+
def provider(reference, image, root, rpaths):
84+
if system(reference):
85+
return None
86+
def expand(value):
87+
value = value.replace('@loader_path', str(image.parent)).replace('@executable_path', str(root / 'aeneas/bin'))
88+
if '@' in value or '$' in value or not Path(value).is_absolute():
89+
raise ValueError('unsupported native path: ' + value)
90+
return Path(value)
91+
if reference.startswith(('@loader_path/', '@executable_path/')):
92+
return owned(expand(reference), root)
93+
if reference.startswith('@rpath/'):
94+
name = reference[len('@rpath/'):]
95+
if '/' in name:
96+
raise ValueError('unsupported nested rpath provider: ' + reference)
97+
# Physical presence alone does not make a dyld search path. In
98+
# particular a system shell can discard DYLD_LIBRARY_PATH.
99+
directories = [expand(path).resolve(strict=True) for path in rpaths]
100+
for directory in directories:
101+
if not directory.is_dir() or not any(directory.is_relative_to(root / family) for family in ('aeneas/bin', 'rust/lib')):
102+
raise ValueError('loader search directory escapes owned archive payload: ' + str(directory))
103+
candidates = {owned(directory / name, root) for directory in directories if (directory / name).exists()}
104+
if len(candidates) != 1:
105+
raise ValueError('missing or ambiguous native provider: ' + reference)
106+
return candidates.pop()
107+
raise ValueError('non-system or unrecognized native reference: ' + reference)
108+
109+
110+
def prepare(root, platform):
111+
root = root.resolve(strict=True)
112+
if (root / 'lean-sdk').exists():
113+
raise ValueError('translation relocation must precede SDK assembly')
114+
architecture = {'aarch64-darwin': 'arm64', 'x86_64-darwin': 'x86_64'}[platform]
115+
pending = [owned(root / 'aeneas/bin' / name, root) for name in ('aeneas', 'charon', 'charon-driver')]
116+
owned(root / 'aeneas/bin/libs/libgmp.10.dylib', root)
117+
plans = []
118+
for image in pending:
119+
if architecture not in tool('lipo', '-archs', image).split():
120+
raise ValueError('native provider lacks selected architecture: ' + str(image))
121+
information = loads(tool('otool', '-l', image))
122+
symbols = tool('nm', '-m', '-u', image) if image.name in {'charon', 'charon-driver'} else ''
123+
replacements = changes(image.name, information['needed'], symbols)
124+
for new in replacements.values():
125+
if new.startswith('@loader_path/'):
126+
provider(new, image, root, [])
127+
plans.append((image, replacements))
128+
for image, replacements in plans:
129+
for old, new in replacements.items():
130+
tool('install_name_tool', '-change', old, new, image)
131+
if replacements:
132+
tool('codesign', '--force', '--sign', '-', '--timestamp=none', image)
133+
visited = set()
134+
while pending:
135+
image = owned(pending.pop(), root)
136+
if image in visited:
137+
continue
138+
visited.add(image)
139+
if architecture not in tool('lipo', '-archs', image).split():
140+
raise ValueError('native provider lacks selected architecture: ' + str(image))
141+
information = loads(tool('otool', '-l', image))
142+
if information['interpreter'] not in (None, '/usr/lib/dyld'):
143+
raise ValueError('foreign native interpreter')
144+
identity = information['identity']
145+
if identity and identity.startswith('/') and not system(identity):
146+
raise ValueError('non-system absolute native install ID')
147+
for path in information['rpaths']:
148+
if system(path):
149+
continue
150+
expanded = path.replace('@loader_path', str(image.parent)).replace('@executable_path', str(root / 'aeneas/bin'))
151+
if '@' in expanded or '$' in expanded or not Path(expanded).is_absolute():
152+
raise ValueError('unsupported native rpath: ' + path)
153+
directory = Path(expanded).resolve(strict=True)
154+
if not directory.is_dir() or not any(directory.is_relative_to(root / family) for family in ('aeneas/bin', 'rust/lib')):
155+
raise ValueError('native rpath escapes owned payload: ' + path)
156+
for reference in information['needed']:
157+
dependency = provider(reference, image, root, information['rpaths'])
158+
if dependency:
159+
pending.append(dependency)
160+
# Intel permits unsigned Mach-O providers. Determine absence from the
161+
# inspected load commands, never from a failed codesign invocation.
162+
# Arm64 still requires verification, as does any signature-present
163+
# image (including a signed slice of a universal provider).
164+
if architecture == 'arm64' or information['code_signature']:
165+
tool('codesign', '--verify', '--strict', image)
166+
167+
168+
if __name__ == '__main__':
169+
parser = argparse.ArgumentParser(description=__doc__)
170+
parser.add_argument('--root', type=Path, required=True)
171+
parser.add_argument('--platform', choices=['aarch64-darwin', 'x86_64-darwin'], required=True)
172+
args = parser.parse_args()
173+
prepare(args.root, args.platform)

0 commit comments

Comments
 (0)