Skip to content

zola, tamarin-prover: fix reproducibility (parallel codegen order; compile-time clock) - #525

Merged
bryan-minimal merged 3 commits into
mainfrom
bryan/zola-tamarin-repro
Aug 4, 2026
Merged

zola, tamarin-prover: fix reproducibility (parallel codegen order; compile-time clock)#525
bryan-minimal merged 3 commits into
mainfrom
bryan/zola-tamarin-repro

Conversation

@bryan-minimal

@bryan-minimal bryan-minimal commented Jul 26, 2026

Copy link
Copy Markdown
Member

Both packages were flagged unknown by a build-twice audit of the 87 packages added since the last fleet run (83/86 reproducible, 96.5%). They looked identical in the verdict table and turned out to be completely different problems.

zola — build-time entropy, not codegen order (corrected by build-twice)

The original analysis here blamed parallel-CGU emission order and proposed -C codegen-units=1 + -C symbol-mangling-version=v0. Build-twice verification falsified that: with both flags applied, 17.4% of bytes still differed (size-preserving, twin-windows). Two further controls sharpened it — ripgrep builds reproducibly with no ordering flags at all (so CGU output is assembled deterministically by rustc), and symbol forensics on unstripped pairs showed identical symbol sets AND order with churn inside generated hash-table code (first address divergence at minify_html_common's spec tables; size-flapping perfect-hash asso_values).

Mechanism: build-time entropy — HashMap-iteration randomness in build-time codegen, invisible to every rustc ordering flag. Fix (last commit): LD_PRELOAD a 12-line deterministic getrandom/getentropy interposer around cargo build only — the entropy analogue of SOURCE_DATE_EPOCH, exactly as minimal-repro's guide prescribes. The runtime binary is unaffected and the upstream profile (fat LTO, strip) stays untouched, so the fix costs zero runtime performance.

tamarin-prover — not GHC, and not the toolchain

Worth stating plainly, since the GHC determinism work is recent: that work is holding. tamarin's Haskell codegen is bit-identical across builds. What differs is 26 bytes out of a 135 MB binary:

Git revision: UNKNOWN, branch: UNKNOWN
Compiled at: 2026-07-25 03:47:54.541898723 UTC     <- build A
Compiled at: 2026-07-25 03:53:20.855637052 UTC     <- build B

tamarin's version banner embeds the wall-clock compile time through a TemplateHaskell splice that calls getCurrentTime while compiling. It asks the clock directly, so the sandbox's SOURCE_DATE_EPOCH never reaches it. (The git fields are already deterministic — there's no repo in the build tree, so both builds say UNKNOWN.)

This is the same family as perl's cf_time (#291): an application baking a timestamp, not a compiler being nondeterministic.

The patch rewrites the splice to a fixed instant derived from SOURCE_DATE_EPOCH, and locates the source file by content (grep -rl 'Compiled at') rather than by path, so an upstream file move fails loudly here instead of silently reverting to a wall clock. It follows the verify-grep style the recipe already uses for its other source patches.

Verification status — both halves verified

Forced-real build-twice via repro-lab on min 0.5.1-rc1 (each build's cache slot evicted first; runs abort unless the builder proves a real build; every build byte-compared against build 1):

  • zola: with the entropy shim — 4 real builds, all byte-identical, upstream profile untouched.
  • tamarin-prover: patch as shipped — 4 real builds, all byte-identical (the builder's warm dep store means only tamarin's own modules rebuild, which is precisely the region the patch touches).

Disclosed caveats: verification used an inert cmd-field spec perturbation to defeat artifact hydration (changed build scripts do not change the spec hash on the current scheme — see the SpecHash migration discussion); and these are target-determinism builds (identical deps by construction), not clean-room. Full methodology, lever matrix, and forensics trail: repro-lab docs/pr525-doublebuild-results.md.

Summary by CodeRabbit

  • Build Improvements
    • Improved reproducibility for Tamarin Prover builds by ensuring version metadata is derived consistently from the build environment.
    • Improved reproducibility for Zola builds with deterministic compilation settings and stable generated outputs.
    • Added safeguards to detect unexpected build-time timestamps or unsupported compilation conditions.

Both were flagged `unknown` by a build-twice audit of the 87 packages added
since the last fleet run. They turned out to be completely different problems.

zola — the reproducibility guide was applied halfway. The recipe already cites
minimal-repro's guide and strips build paths, but never pinned codegen. rustc's
default release build shards codegen across parallel units that finish in
thread-completion order, so functions are EMITTED in a different order each
build. Measured on 0.22.1: 16.89% of bytes differed while the total size stayed
identical, and 69% of differing windows had a byte-exact twin elsewhere in the
other build — a size-preserving permutation, i.e. ordering, not codegen
variance. Adds `-C codegen-units=1` (ordering) and
`-C symbol-mangling-version=v0` (legacy mangling embeds a per-session hash).
Same fix as nushell and difftastic.

tamarin-prover — not GHC, and not the toolchain. Its version banner embeds the
wall-clock compile time via a TemplateHaskell splice that calls getCurrentTime
while compiling; it asks the clock directly, so SOURCE_DATE_EPOCH never reaches
it. Exactly 26 bytes of a 135 MB binary differ, and the Haskell codegen is
otherwise bit-identical — the GHC determinism work is holding fine. Rewrites the
splice to a fixed instant derived from SOURCE_DATE_EPOCH, locating the source
file by content so an upstream file move fails loudly instead of silently
reverting to a wall clock.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@coderabbitai

coderabbitai Bot commented Jul 26, 2026

Copy link
Copy Markdown
Contributor

Review Change Stack

📝 Walkthrough

Walkthrough

The build scripts for Tamarin and Zola now apply deterministic timestamps, Rust compilation settings, and entropy sources to improve reproducibility.

Changes

Reproducible build configuration

Layer / File(s) Summary
Deterministic Tamarin version banner
packages/tamarin-prover/build.sh
The script derives a fixed timestamp from SOURCE_DATE_EPOCH, rewrites supported getCurrentTime splices, and fails when the banner source or rewrite is invalid.
Deterministic Zola compilation
packages/zola/build.sh
The script pins Rust codegen and symbol settings, compiles a deterministic entropy shim, and runs the release build with LD_PRELOAD.

Estimated code review effort: 3 (Moderate) | ~20 minutes

Possibly related PRs

  • gominimal/pkgs#449: Introduced the Tamarin package and its original build script, which this change modifies.
🚥 Pre-merge checks | ✅ 5
✅ Passed checks (5 passed)
Check name Status Explanation
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The title clearly identifies both packages and the reproducibility goal, although the zola cause is broader than the final entropy-based fix.
Docstring Coverage ✅ Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check ✅ Passed Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check ✅ Passed Check skipped because no linked issues were found for this pull request.
✨ Finishing Touches
📝 Generate docstrings
  • Create stacked PR
  • Commit on current branch
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch bryan/zola-tamarin-repro

Comment @coderabbitai help to get the list of available commands.

The reproducibility patch only matched a BARE call:

    s|runIO Data\.Time\.getCurrentTime|...|
    s|runIO getCurrentTime|...|

but upstream composes the action rather than naming it:

    $(stringE =<< runIO (show `fmap` Data.Time.getCurrentTime))

`runIO` is followed by `(show ` fmap ` ...`, so neither pattern matched,
getCurrentTime survived, and the guard correctly refused the build on both
arches rather than shipping a wall-clock binary:

    ERROR: tamarin compile-time-clock patch did not apply in src/Main/Console.hs

Add a pattern for the whole parenthesised argument; keep the two bare forms in
case upstream simplifies back to them. Verified by running the patched block
verbatim against the real line:

    compileTime = "Compiled at: " ++ $(stringE =<< pure ("1970-01-01 00:00:00 UTC"))

which type-checks (`pure :: String -> Q String` feeding `stringE`) and leaves no
getCurrentTime for the guard to catch.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Build-twice verification (repro-lab, min 0.5.1-rc1, forced-real builds)
falsified the codegen-ordering hypothesis: with cg-units=1 + v0 already
applied, 17.4% of bytes still differed. Symbol forensics on unstripped
pairs attributed the churn to build-time entropy in generated hash-table
code (first address divergence at minify_html_common's spec tables;
ripgrep control shows plain parallel builds reproduce fine, so CGU
completion order was never the mechanism).

Fix: LD_PRELOAD a 12-line deterministic getrandom/getentropy interposer
around cargo build only — the entropy analogue of SOURCE_DATE_EPOCH, as
prescribed (but never shipped) by minimal-repro's guide. Runtime binary
unaffected; upstream profile (lto=true, strip=true) untouched.

Verified: 4 forced-real builds, all byte-identical.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@bryan-minimal

Copy link
Copy Markdown
Member Author

Build-twice results, as promised before leaving draft — both halves verified on min 0.5.1-rc1 with forced-real builds (cache slot evicted before every build; the harness aborts unless the builder proves a real build happened; every build byte-compared against build 1):

  • zola: the original codegen-units=1 + v0 fix was falsified (17.4% still differed). Root cause is build-time entropy in generated hash-table code (symbol-forensics attribution in the updated description). With the deterministic-entropy shim (6ca9d7b): 4 real builds, all byte-identical, upstream profile untouched — zero runtime perf cost.
  • tamarin-prover: the splice patch works exactly as shipped: 4 real builds, all byte-identical.

The description's zola section has been rewritten to match the evidence (the ripgrep control disproves the CGU-completion-order explanation — worth knowing for the guide, which repro-lab will follow up on separately).

Caveats, disclosed: verification used an inert cmd-field spec perturbation to defeat artifact hydration (script-only changes don't move the spec hash on the current scheme), and these are target-determinism builds, not clean-room. Full lever matrix and forensics trail: repro-lab docs/pr525-doublebuild-results.md.

🤖 Generated with Claude Code

@bryan-minimal
bryan-minimal marked this pull request as ready for review August 4, 2026 19:24

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 1

🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@packages/zola/build.sh`:
- Line 19: Update the entropy-shim setup in build.sh to create a private
directory with mktemp -d, place detrand.c and detrand.so there instead of /tmp,
and register a trap to remove the directory on exit. Preserve -C codegen-units=1
and -C symbol-mangling-version=v0 in the RUSTFLAGS configuration.
🪄 Autofix

Fix all unresolved CodeRabbit comments on this PR:

  • Push a commit to this branch (recommended)
  • Create a new PR with the fixes

ℹ️ Review info
⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: CHILL

Plan: Pro

Run ID: 4bbb6556-6e76-4c46-a6e5-b78e8b718551

📥 Commits

Reviewing files that changed from the base of the PR and between defad31 and 6ca9d7b.

📒 Files selected for processing (2)
  • packages/tamarin-prover/build.sh
  • packages/zola/build.sh

Comment thread packages/zola/build.sh
#
# symbol-mangling-version=v0 removes the other half: the legacy mangling scheme
# embeds a compilation-session hash in symbol names, which varies run to run.
export RUSTFLAGS="-C linker=gcc --remap-path-prefix=$(pwd)=/builddir --remap-path-prefix=$HOME/.cargo=/cargo -C codegen-units=1 -C symbol-mangling-version=v0"

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🎯 Functional Correctness | 🟠 Major | ⚡ Quick win

🧩 Analysis chain

🏁 Script executed:

#!/bin/sh
set -eu

rg -n -C 4 'codegen.units|codegen-units|symbol.mangling|symbol-mangling|entropy|falsif' \
  repro-lab/docs/pr525-doublebuild-results.md packages/zola/build.sh

Repository: gominimal/pkgs

Length of output: 2791


🏁 Script executed:

#!/bin/sh
set -eu

printf '%s\n' '--- candidate files ---'
git ls-files | rg '(^|/)(build\.sh|.*repro.*|.*doublebuild.*|.*zola.*)$' | head -200

printf '%s\n' '--- zola build script ---'
cat -n packages/zola/build.sh

printf '%s\n' '--- references to the reported flags and entropy shim ---'
rg -n -C 3 'codegen-units|symbol-mangling-version|detrand|LD_PRELOAD|double.?build|nondetermin|reproduc' . \
  -g '!packages/zola/build.sh' -g '!vendor/**' | head -300

Repository: gominimal/pkgs

Length of output: 29554


🌐 Web query:

Rust rustc -C symbol-mangling-version=v0 compilation-session hash legacy mangling reproducible builds official documentation

💡 Result:

The v0 symbol mangling scheme is the current standard for symbol name encoding in the Rust compiler (rustc) [1][2]. It was developed to replace the legacy mangling scheme, which relied on C++-style mangling and compiler-internal structures [3][2]. Key aspects of the v0 scheme include: Consistency and Reproducibility: The v0 format is designed to be unambiguous and platform-independent, with a consistent definition that does not depend on compiler-internal states or pretty-printing [4][3]. By restricting symbols to a consistent character set (A-Z, a-z, 0-9, _), it improves compatibility across different toolchains and platforms [4][2]. Reproducible Builds: While v0 provides a more stable and decodable symbol format than the legacy scheme, reproducibility can still be affected by other compiler settings [5]. For example, the use of -Cmetadata in rustc can influence the disambiguators present in mangled symbols [5]. Discussions in the Rust community note that because v0 symbols may include hashes to distinguish crate versions or generic instantiations, changes in metadata can still lead to differences in the generated symbol names and, consequently, the order of symbols in an executable [5]. Compilation Control: The mangling version can be controlled using the compiler flag -Csymbol-mangling-version [1]. - v0: The current standard, which provides reversible encoding for generic parameters and is more efficient/standardized [4][6]. - legacy: The older scheme, which is available on some versions of the compiler (primarily for backward compatibility or as an escape hatch) but is generally deprecated [1][2][7]. Official documentation on the v0 format is maintained in The rustc book, which details the encoding, the motivation behind the change (RFC 2603), and how the scheme handles various Rust entities [4][3][1]. Tooling such as rustfilt or the rustc-demangle crate is recommended for decoding these symbols [1].

Citations:


🏁 Script executed:

#!/bin/sh
set -eu

python3 - <<'PY'
from pathlib import Path
import re

script = Path("packages/zola/build.sh").read_text()
policy = Path("AGENTS.md").read_text()

flags = re.search(r'^export RUSTFLAGS="([^"]+)"$', script, re.M)
assert flags, "RUSTFLAGS assignment not found"
rustflags = flags.group(1)

required = [
    "-C linker=gcc",
    "--remap-path-prefix=$(pwd)=/builddir",
    "--remap-path-prefix=$HOME/.cargo=/cargo",
]
conditional = "-C codegen-units=1"

print("RUSTFLAGS:", rustflags)
print("base Rust flags present:", all(x in rustflags for x in required))
print("codegen-units=1 present:", conditional in rustflags)
print("policy requires codegen fallback:", conditional in policy and ".text`/`.rodata" in policy)
print("script documents differing bytes:", "bytes differed" in script)
print("symbol mangling flag present:", "-C symbol-mangling-version=v0" in rustflags)
print("cited double-build report exists:", Path("repro-lab/docs/pr525-doublebuild-results.md").exists())
print("predictable temporary paths:", all(p in script for p in ("/tmp/detrand.c", "/tmp/detrand.so")))
PY

Repository: gominimal/pkgs

Length of output: 550


Create a private temporary directory for the entropy shim.

/tmp/detrand.c and /tmp/detrand.so use predictable shared paths. A local user can replace these files and cause LD_PRELOAD to load attacker-controlled code. Use a private mktemp -d directory and clean it with trap.

The cited double-build report is absent. Keep -C codegen-units=1; AGENTS.md requires it when .text or .rodata differs, and this script documents such differences. Do not remove symbol-mangling-version=v0 without a reproducibility comparison.

🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@packages/zola/build.sh` at line 19, Update the entropy-shim setup in build.sh
to create a private directory with mktemp -d, place detrand.c and detrand.so
there instead of /tmp, and register a trap to remove the directory on exit.
Preserve -C codegen-units=1 and -C symbol-mangling-version=v0 in the RUSTFLAGS
configuration.

@bryan-minimal
bryan-minimal added this pull request to the merge queue Aug 4, 2026
Merged via the queue into main with commit 31593f0 Aug 4, 2026
10 checks passed
@bryan-minimal
bryan-minimal deleted the bryan/zola-tamarin-repro branch August 4, 2026 20:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants