fix(hazmat-kzg): build LeanHazmatKzg on macOS (etheorem#13)

* fix(macos-kzg-build): use Mach-O section name for embedded trusted setup on Apple

* fix(macos-kzg-build): use platform-specific KZG link and symbol names

* fix(macos-kzg-build): ignore local clang output

* fix(macos-kzg-build): describe the platform-specific blst link flag

* fix(macos-build): make EthCLLib/EthCLSpecs libcrypto link portable

EthCLLib and EthCLSpecs re-supply the system libcrypto flag that Lake
doesn't propagate across `require` (see SizzLean's lakefile note), but
they linked it as `-l:libcrypto.so.3`, an exact-SONAME form that only
resolves on Linux. Switch to `-lcrypto`, which resolves through the
unversioned symlink every platform's `-dev`/Homebrew OpenSSL package
provides, and add the Homebrew `opt` paths (Apple Silicon and Intel)
to the existing Linux `-L` candidate list. The linker already ignores
whichever `-L` paths are absent, so one flag list now covers all three
platforms.

Verified with `lake build EthCLSpecs` (clean, 365/365 jobs) and
`just ethcl-test`, whose native_decide self-tests (BLS sign/verify,
KZG cell-proof-batch round-trips through the FFI crypto backend)
exercise the linked shared libraries at runtime, not just at link time.

Append a dated addendum to hazmat-docs/PLAN.md's Stage 0 outcome note,
which recorded `-l:libcrypto.so.3` as the settled flag; the propagation
finding and the decision to re-supply independently are unchanged,
only the literal flag.

* docs(contributing): document macOS native deps in the Quick Start

The Quick Start only listed `apt-get install libssl-dev` and referenced
the Linux-only `libcrypto.so.3`, even though README.md's "Native
dependencies" section already documents the macOS Homebrew path. Add
the macOS line, add the missing `pkg-config` to the Linux line (already
present in README.md's fuller version), and point to README.md for the
per-platform details instead of naming one platform's library file.

Author: Mouzayan

.gitignore

@@ -58,3 +58,4 @@ packages/SizzLean/bench/*.tsv
 
 # macOS Finder cruft
 .DS_Store
+a.out

CONTRIBUTING.md

@@ -11,8 +11,11 @@ correctness on the verified core. Contributions are welcome.
 # 1. Install elan (one-time). https://elan.lean-lang.org/
 curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
 
-# 2. Install native deps. On Debian/Ubuntu:
-sudo apt-get install libssl-dev
+# 2. Install native deps.
+# Linux (Debian/Ubuntu):
+sudo apt-get install libssl-dev pkg-config
+# macOS:
+brew install openssl@3 pkg-config
 
 # 3. Clone and build.
 git clone https://github.com/etheorem/etheorem
@@ -22,7 +25,9 @@ lake build
 
 The pinned toolchain in `lean-toolchain` is picked up by elan
 automatically. First build pulls Lake deps + compiles the FFI
-SHA-256 shim against `libcrypto.so.3`.
+SHA-256 shim against the system OpenSSL `libcrypto` (see
+[`README.md`](README.md#native-dependencies) for the per-platform
+library names and discovery details).
 
 ## Running the test suites
 

hazmat-docs/PLAN.md

@@ -73,6 +73,13 @@ discovery, accepted, per the no-shared-lakefile-code decision
 > `-l:libcrypto.so.3`, and `LeanHazmatSha256` keeps its own for its
 > test lib. No package reverts to a TOML lakefile. This matches the
 > prior link-arg evidence and the no-shared-lakefile-code decision (§3.3).
+>
+> **Addendum (macOS portability).** `EthCLLib`/`EthCLSpecs`'s hardcoded
+> flag later changed from the Linux-only `-l:libcrypto.so.3` to the
+> portable `-lcrypto` plus Homebrew's `-L` paths, so the same
+> independent, hardcoded re-supply this stage decided on now resolves
+> on macOS too. The propagation finding and the decision to re-supply
+> independently are unchanged, only the literal flag each package hardcodes.
 
 ---
 

packages/EthCLLib/lakefile.toml

@@ -6,9 +6,12 @@ defaultTargets = ["EthCLLib"]
 # `libcrypto` flag its `native_decide` self-tests need transitively through
 # SizzLean's FFI SHA-256. The blst / c-kzg archives propagate automatically
 # as `extern_lib`s, only the system shared lib needs re-stating here.
-# Two `-L` paths cover the common Linux libdir layouts (Debian multiarch and
-# `/usr/lib64` on Gentoo / Fedora / RHEL); the linker ignores whichever is absent.
-moreLinkArgs = ["-L/usr/lib/x86_64-linux-gnu", "-L/usr/lib64", "-l:libcrypto.so.3"]
+# The `-L` paths cover the common libdir layouts across platforms (Debian
+# multiarch, `/usr/lib64` on Fedora/RHEL, and Homebrew's `opt` symlink on
+# both macOS architectures); the linker ignores whichever are absent.
+# `-lcrypto` (not `-l:libcrypto.so.3`) resolves via the unversioned symlink
+# every platform's `-dev`/Homebrew package provides, so it works on both.
+moreLinkArgs = ["-L/usr/lib/x86_64-linux-gnu", "-L/usr/lib64", "-L/opt/homebrew/opt/openssl@3/lib", "-L/usr/local/opt/openssl@3/lib", "-lcrypto"]
 moreLeancArgs = ["-march=native"]
 
 # SizzLean supplies the SSZ machinery (SSZRepr, Box, the cache, sszGet /

packages/EthCLSpecs/lakefile.toml

@@ -3,9 +3,12 @@ defaultTargets = ["EthCLSpecs"]
 
 # Re-supply the system libcrypto flag (does not propagate across `require`); the
 # blst / c-kzg archives propagate transitively from the LeanHazmat packages.
-# Two `-L` paths cover the common Linux libdir layouts (Debian multiarch and
-# `/usr/lib64` on Gentoo / Fedora / RHEL); the linker ignores whichever is absent.
-moreLinkArgs = ["-L/usr/lib/x86_64-linux-gnu", "-L/usr/lib64", "-l:libcrypto.so.3"]
+# The `-L` paths cover the common libdir layouts across platforms (Debian
+# multiarch, `/usr/lib64` on Fedora/RHEL, and Homebrew's `opt` symlink on
+# both macOS architectures); the linker ignores whichever are absent.
+# `-lcrypto` (not `-l:libcrypto.so.3`) resolves via the unversioned symlink
+# every platform's `-dev`/Homebrew package provides, so it works on both.
+moreLinkArgs = ["-L/usr/lib/x86_64-linux-gnu", "-L/usr/lib64", "-L/opt/homebrew/opt/openssl@3/lib", "-L/usr/local/opt/openssl@3/lib", "-lcrypto"]
 moreLeancArgs = ["-march=native"]
 
 # The framework. Pulls in SizzLean (SSZ), LeanHazmatBls / LeanHazmatKzg (crypto)

packages/LeanHazmatKzg/LeanHazmatKzg/Ffi.lean

@@ -1,10 +1,10 @@
 -- Build-ordering import (not for any Lean symbol): this package's
--- precompiled `.so` links Bls's shared lib (`moreLinkArgs`,
--- `-l:libleanhazmat_bls.so`) for the `blst_*` symbols c-kzg references.
+-- precompiled `.so` links Bls's shared lib (`moreLinkArgs`'s
+-- platform-specific `-l`) for the `blst_*` symbols c-kzg references.
 -- Importing the Bls module makes the Bls package, and so its shared
 -- lib, a build prerequisite of this module, ordering it before this
 -- package's link step (otherwise a clean parallel build can race and the
--- KZG `.so` link fails with "unable to find -l:libleanhazmat_bls.so").
+-- KZG `.so` link fails with "unable to find" the missing lib).
 import LeanHazmatBls
 
 /-!

packages/LeanHazmatKzg/csrc/trusted_setup_incbin.S

@@ -14,9 +14,29 @@
 // `just hazmat-kzg-vendor`). The C shim reads these bytes via `fmemopen` +
 // `load_trusted_setup_file` once at library load.
 
+    #ifdef __APPLE__
+    .section __DATA,__const
+    #else
     .section .rodata
+    #endif
+
+    // Mach-O's C ABI prefixes every C symbol with `_` at the linker level;
+    // the compiler adds it automatically when it compiles `kzg_shim.c`'s
+    // `extern const char lean_hazmat_kzg_ts_start[]`, but an `.S` file
+    // bypasses that mangling, so the label written here must carry the
+    // `_` itself on Apple to match what the linker looks for.
+    #ifdef __APPLE__
+    .global _lean_hazmat_kzg_ts_start
+_lean_hazmat_kzg_ts_start:
+    #else
     .global lean_hazmat_kzg_ts_start
 lean_hazmat_kzg_ts_start:
+    #endif
     .incbin TRUSTED_SETUP_PATH
+    #ifdef __APPLE__
+    .global _lean_hazmat_kzg_ts_end
+_lean_hazmat_kzg_ts_end:
+    #else
     .global lean_hazmat_kzg_ts_end
 lean_hazmat_kzg_ts_end:
+    #endif

packages/LeanHazmatKzg/docs/ARCHITECTURE.md

@@ -58,13 +58,15 @@ work without duplicating it:
   one blst copy and no duplicate symbols.
 * **Shared lib (precompiled module / `native_decide`).** The precompiled
   module's `.so` would otherwise have undefined `blst_*` at load. The
-  package's `moreLinkArgs` give it `-l:libleanhazmat_bls.so` +
-  `-L`/`-rpath` into Bls's build lib, so the loader pulls Bls's shared lib
-  and resolves `blst_*`, mirroring how `LeanHazmatSha256`'s `.so` gains
-  `NEEDED libcrypto.so.3`. That link reference is invisible to Lake's
-  scheduler, so the `extern_lib` folds Bls's shared-lib build into its own
-  dependency trace (`Job.zipWith` over `findExternLib? `libleanhazmat_bls`)
-  to keep clean parallel builds from racing ahead of Bls's `.so`.
+  package's `moreLinkArgs` give it `-L`/`-rpath` into Bls's build lib plus
+  a platform-appropriate `-l`: `-l:libleanhazmat_bls.so` (a `DT_NEEDED`
+  entry, ELF/Linux) or `-lleanhazmat_bls` (a Mach-O `LC_LOAD_DYLIB`,
+  Apple), so the loader pulls Bls's shared lib and resolves `blst_*`,
+  mirroring how `LeanHazmatSha256`'s `.so` gains `libcrypto` on each
+  platform. That link reference is invisible to Lake's scheduler, so the
+  `extern_lib` folds Bls's shared-lib build into its own dependency trace
+  (`Job.zipWith` over `findExternLib? `libleanhazmat_bls`) to keep clean
+  parallel builds from racing ahead of Bls's `.so`.
 
 ## Trust boundary
 

packages/LeanHazmatKzg/lakefile.lean

@@ -44,16 +44,21 @@ package LeanHazmatKzg where
   licenseFiles := #["../../LICENSE"]
   -- Make this package's *shared* lib depend on LeanHazmatBls's shared lib
   -- so the precompiled module `.so` resolves c-kzg's `blst_*` references
-  -- at load: `-l:libleanhazmat_bls.so` adds a `DT_NEEDED`, `-L` finds it
-  -- at link, and the `-rpath` finds it at `dlopen`. This mirrors exactly
-  -- how LeanHazmatSha256's `.so` gains `NEEDED libcrypto.so.3`. blst lives
-  -- in Bls's archive (not duplicated here), so the final exe link still
-  -- sees one blst copy via normal `extern_lib` propagation, no
+  -- at load: `-L` finds it at link, `-rpath` finds it at `dlopen`, and the
+  -- `-l` itself is platform-specific (`if Platform.isOSX` below; see
+  -- ARCHITECTURE.md "Sharing one blst" for the ELF/Mach-O rationale). This
+  -- mirrors exactly how LeanHazmatSha256's `.so` gains `libcrypto`. blst
+  -- lives in Bls's archive (not duplicated here), so the final exe link
+  -- still sees one blst copy via normal `extern_lib` propagation, no
   -- duplicate symbols. (Monorepo path; a standalone Kzg mirror resolves
   -- Bls through its git `require`.)
   moreLinkArgs := Id.run do
     let d := unsafe blsLibDir
-    #["-L" ++ d, "-l:libleanhazmat_bls.so", "-Wl,-rpath," ++ d]
+    if Platform.isOSX then
+      #["-L" ++ d, "-lleanhazmat_bls", "-Wl,-rpath," ++ d]
+    else
+      let lib := nameToSharedLib "leanhazmat_bls"
+      #["-L" ++ d, "-l:" ++ lib, "-Wl,-rpath," ++ d]
 
 -- Shares LeanHazmatBls's blst, the single blst owner for the family.
 require LeanHazmatBls from "../LeanHazmatBls"
@@ -126,9 +131,9 @@ extern_lib libleanhazmat_kzg pkg := do
   let staticJob ← buildStaticLib (pkg.staticLibDir / name) #[shimO, ckzgO, setupO]
   -- Order LeanHazmatBls's *shared* lib before this archive (and therefore
   -- before the `.so` derived from it). Our shared lib references it via
-  -- `moreLinkArgs` (`-l:libleanhazmat_bls.so`), but that path is invisible
-  -- to Lake's scheduler, so a clean parallel build can otherwise link this
-  -- `.so` before Bls's `.so` exists ("unable to find -l:libleanhazmat_bls.so").
+  -- `moreLinkArgs`'s platform-specific `-l`, but that path is invisible to
+  -- Lake's scheduler, so a clean parallel build can otherwise link this
+  -- `.so` before Bls's `.so` exists ("unable to find" the missing lib).
   -- `Job.zipWith` folds Bls's shared-lib build into this job's dependency
   -- trace (keeping this archive's path as the value), making the ordering
   -- explicit.
@@ -142,8 +147,8 @@ extern_lib libleanhazmat_kzg pkg := do
 lean_lib LeanHazmatKzg where
   -- Precompiled so `native_decide` (here and downstream) finds the KZG
   -- externs as loaded precompiled symbols. The module `.so` resolves
-  -- `blst_*` at load via the `DT_NEEDED` + `-rpath` on Bls's shared lib
-  -- that `moreLinkArgs` adds.
+  -- `blst_*` at load via the platform-specific `-l` + `-rpath` on Bls's
+  -- shared lib that `moreLinkArgs` adds.
   precompileModules := true
 
 -- KAT gate against the consensus-spec KZG vectors + self-contained