To determine the exact rules for dependency propagation, we start by assigning to each dependency a couple of ternary numbers (`-1` for `build`, `0` for `host`, and `1` for `target`) representing its [dependency type](#possible-dependency-types), which captures how its host and target platforms are each "offset" from the depending derivation’s host and target platforms. The following table summarize the different combinations that can be obtained:

| `host → target`     | attribute name      | offset   | typical purpose                               |
| ------------------- | ------------------- | -------- | --------------------------------------------- |
| `build --> build`   | `depsBuildBuild`    | `-1, -1` | compilers for build helpers                   |
| `build --> host`    | `nativeBuildInputs` | `-1, 0`  | build tools, compilers, setup hooks           |
| `build --> target`  | `depsBuildTarget`   | `-1, 1`  | compilers to build stdlibs to run on target   |
| `host --> host`     | `depsHostHost`      | `0, 0`   | compilers to build C code at runtime (rare)   |
| `host --> target`   | `buildInputs`       | `0, 1`   | libraries                                     |
| `target --> target` | `depsTargetTarget`  | `1, 1`   | stdlibs to run on target                      |

Algorithmically, we traverse propagated inputs, accumulating every propagated dependency’s propagated dependencies and adjusting them to account for the “shift in perspective” described by the current dependency’s platform offsets. This results in a sort of transitive closure of the dependency relation, with the offsets being approximately summed when two dependency links are combined. We also prune transitive dependencies whose combined offsets go out-of-bounds, which can be viewed as a filter over that transitive closure removing dependencies that are blatantly absurd.

We can define the process precisely with [Natural Deduction](https://en.wikipedia.org/wiki/Natural_deduction) using the inference rules below. This probably seems a bit obtuse, but so is the bash code that actually implements it! [^footnote-stdenv-find-inputs-location] They’re confusing in very different ways so… hopefully if something doesn’t make sense in one presentation, it will in the other!

**Definitions:**

`dep(h_offset, t_offset, X, Y)`
:    Package X has a direct dependency on Y in a position with host offset `h_offset` and target offset `t_offset`.

     For example, `nativeBuildInputs = [ Y ]` means `dep(-1, 0, X, Y)`.

`propagated-dep(h_offset, t_offset, X, Y)`
:    Package X has a propagated dependency on Y in a position with host offset `h_offset` and target offset `t_offset`.

     For example, `depsBuildTargetPropagated = [ Y ]` means `propagated-dep(-1, 1, X, Y)`.

`mapOffset(h, t, i) = offs`
:    In a package X with a dependency on Y in a position with host offset `h` and target offset `t`, Y's transitive dependency Z in a position with offset `i` is mapped to offset `offs` in X.


::: {.example}
# Truth table of `mapOffset(h, t, i)`

`x` means that the dependency was discarded because `h + i ∉ {-1, 0, 1}`.

<!-- This is written as an ascii art table because the CSS was introducing so much space it was unreadable and doesn't support double lines -->

```
  h |   t  || i=-1 |  i=0 |  i=1
----|------||------|------|-----
 -1 |  -1  ||   x  |  -1  |  -1
 -1 |   0  ||   x  |  -1  |   0
 -1 |   1  ||   x  |  -1  |   1
  0 |   0  ||  -1  |   0  |   0
  0 |   1  ||  -1  |   0  |   1
  1 |   1  ||   0  |   1  |   x
```

:::

```
let mapOffset(h, t, i) = i + (if i <= 0 then h else t - 1)

propagated-dep(h0, t0, A, B)
propagated-dep(h1, t1, B, C)
h0 + h1 in {-1, 0, 1}
h0 + t1 in {-1, 0, 1}
-------------------------------------- Transitive property
propagated-dep(mapOffset(h0, t0, h1),
               mapOffset(h0, t0, t1),
               A, C)
```

```
let mapOffset(h, t, i) = i + (if i <= 0 then h else t - 1)

dep(h0, t0, A, B)
propagated-dep(h1, t1, B, C)
h0 + h1 in {-1, 0, 1}
h0 + t1 in {-1, 0, 1}