An expression can name a derivation and resolve to an output path without settling reproducibility of the builder's result. Nix's functional evaluation gives us a way to reason about the expression. The external commands still need their own input account.
Consider a hypothetical build environment that permits an undeclared host-file read. The builder copies /opt/local/banner into its output. Between two builds, the declared inputs stay the same but that file changes. The output contents could then differ. This counterexample depends on that read being permitted.
I would want the builder definition, declared dependencies and evidence about which external inputs it can actually observe. If some changing host state is intentionally allowed, the reproducibility claim needs to say what is held fixed.
SLSA provenance can record the build definition, execution details and known resolved dependencies. That could help us inspect the claim, but it does not establish that every output-affecting input has been accounted for. What evidence would close that gap for this derivation?
