Re: Deep vs Shallow trace: Removing the tradeoff?

[ilmu]

> > 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