Re: Deep vs Shallow trace: Removing the tradeoff?

[ilmu <ilmu@rishi.is>]

> > Early cutoff is a very desirable property that nix does not have (and I assume therefore that neither does guix).

> The “intensional model” that Julien mentioned, or what the Nix folks now
> refer to as “content-addressed derivations”, have this early cutoff
> property.  It’s one of the main motivations for this whole endeavors.

> This document shows how Nix folks are working on retrofitting
> “content-addressed derivations” into Nix:

>   https://github.com/tweag/rfcs/blob/cas-rfc/rfcs/0062-content-addressed-paths.md

This looks to me to be massively more complicated and also needing stronger assumptions about how reproducible the builds are. However I am not even sure I understand the proposals that well...

Thank you for bringing this to my attention though, does guix have any plans to do something like this?


> I have long been wondering if reproducibility is too exclusively focused
> on the source transformation chain and the tools implementing that.
>
> E.g., for programs that execute like side-effect-free functions,
> why not an early-cutoff based on a functionally well-tested upgrade
> written in a different language, with a totally different source?
>
> If you source the following in a subshell
>
> cat ./early-cutoff.txt
> --8<---------------cut here---------------start------------->8---
>
> export HELLO_TO=World
>
> strace -qqxs120 -e write \
> guile -c '(let* ((msg (string-append "Hello " (getenv "HELLO_TO") "\n"))) (display msg))' |& tr , $'\n'|grep '^ *"'
>
> strace -qqxs120 -e write \
> echo "Hello $HELLO_TO" |& tr , $'\n'|grep '^ *"'
>
> --8<---------------cut here---------------end--------------->8---
>
> Like,
>
> (. early-cutoff.txt)
> --8<---------------cut here---------------start------------->8---
> "Hello World\n"
> "Hello World\n"
> --8<---------------cut here---------------end--------------->8---
>
> It informally shows that in a particular context,
>
> --8<---------------cut here---------------start------------->8---
> guile -c '(let* ((msg (string-append "Hello " (getenv "HELLO_TO") "\n"))) (display msg))'
> --8<---------------cut here---------------end--------------->8---
>
> can substitute for
> --8<---------------cut here---------------start------------->8---
> echo "Hello $HELLO_TO"
> --8<---------------cut here---------------end--------------->8---
>
> So, what kinds of build sequences could be cut off early if you ignore how
> you produced the code (i.e. just compile whatever source you like with whatever
> tools you like) so long as the resultant code passed the functionality tests?

Yes! Precisely, we should be able to switch out the implementations so long as we can prove that the result is the same. At the limit we are essentially saying that extensionally equal things can be swapped for one another. However, extensional equality is pretty much impossible to calculate in the general case (you'd need to prove it constructively) and of course your example does not have intensional equality (which is the whole point of switching out the dependency, to improve the implementation, i.e. break intensional equality while keeping extensional equality).

The equality that we can keep using the succinct arguments of knowledge is extensional because in the special case of build systems we can use a dependency at build time and then if the resulting artefact is unchanged then we can do the early cut-off. So we depend on the property that an artefact can be used independently once built, so for example two versions of a compiler may give the same binary and then updating a compiler will allow you to only rebuild transitive closures of programs that depended on changed behaviors between versions.

To drive the point home: If the artefact has the same hash as it did before then clearly the underlying change did not affect it. Early cut-off is therefore not possible in the case where the program being depended on is supposed to be used at runtime.

This is at least how I am thinking about it, I think this would be a good incremental improvement on the state of the art but it would still have these limitations.

Kind regards,
- ilmu