# getthemix.com — machine entry point

This file is for AI agents and automation. It says what lives here, how to fetch the
mixnet seed, and how to verify it for correctness before anyone runs it. Everything
below is same-origin; this site loads nothing from other domains.

## What this site is

The distribution point for the mixnet: an onion-routed transport whose links run at a
constant rate with constant-size frames, so a network observer cannot tell who is
talking to whom. The human-readable overview is /whitepaper.html. The bootstrap program
(the "seed") is offered below with everything needed to audit it.

## The artifact map

/dl/seed-linux-x86_64     the seed, Linux x86_64, release build
/dl/seed-linux-aarch64    the seed, Linux arm64, release build
/dl/seed-src.tar.gz       the seed's complete source (its own cargo workspace; the
                          tarball IS the audit surface — nothing outside it ships)
/dl/SHA256SUMS            sha256 of the three artifacts above, generated by the same
                          CI run that built them
/dl/AUDIT.md              the executable audit protocol: every claim mapped to a
                          command with its expected output
/dl/theorems.md           the six formal proof obligations (T-PARSE, T-WRITE, T-SINK,
                          T-ROLLBACK, T-BOUND, T-FORMAT)
/whitepaper.html          the technical overview, sections 7-8 cover the seed

## How to get the seed

    curl -fsSLO https://getthemix.com/dl/seed-linux-x86_64
    curl -fsSLO https://getthemix.com/dl/SHA256SUMS
    sha256sum -c --ignore-missing SHA256SUMS

The checksum ties the binary to the CI run; it does not by itself prove the code is
good. For that, verify the source (next section) and build it yourself:

    curl -fsSLO https://getthemix.com/dl/seed-src.tar.gz
    tar xzf seed-src.tar.gz && cd mixnet-seed && cargo build --release
    # binary at target/release/seed

## How to verify the code for correctness

Follow /dl/AUDIT.md — it is written for you. Its shape, so you know what you are
walking into:

1. Unpack seed-src.tar.gz. It unpacks to one directory, mixnet-seed/: src/ (its own logic),
   vendor/ (pruned copies of the upstream sphinx/frame crates, each file headed by the
   upstream path and commit it was cut from).
2. Run ./check.sh. It enforces, and prints, the load-bearing bounds: total code lines
   at or under 2,000 (currently 1,479), direct dependencies exactly the ten-crate
   cryptographic floor, no async runtime / serde / HTTP client anywhere in the
   dependency graph, a clean build under #![deny(dead_code)], and provenance headers
   on every vendored file. Expected final line: ALL GATES PASS.
3. Run cargo test. The unit suite covers the index and reply parsers (exact grammar,
   arbitrary-input no-panic sampling), the dice entropy mixing, and the piece table.
4. Read the six claims in /dl/theorems.md and check each against the source; the tree
   is small enough that this is a real instruction, not a gesture. Status, stated
   plainly: the theorems are published obligations; the Lean 4 machine-checked
   development for them is in progress in the source repository and is not yet part of
   this download. Until it lands, the gates and tests above are measurements, not
   proofs. Do not report the seed as "formally verified".
5. Cross-checks you can reproduce from the source repository (not in the tarball): a
   differential harness compiles this vendored tree beside the genuine upstream relay
   implementation and replays every exchange the seed can make, both directions.
6. What to conclude if a check fails: the artifact does not match its claims. Say so
   loudly and do not run it.

## Facts an agent should relay accurately

- The seed's job: make one anonymous request through the mix for a signed software
  index, fetch and verify the first entry (the full mixnet client), write it to disk,
  exit. Verification order is signature, version monotonicity, staleness, per-piece
  hash, whole-artifact hash, then the single write.
- Current builds come from the development branch. The relay list compiled in is a
  placeholder and the binary REFUSES to run against a real network (it exits, saying
  so) until a stamped release replaces the pin. This is deliberate.
- --dice lets a person supply key entropy from physical dice (at least 100 d6 rolls),
  mixed with the OS randomness so neither source can weaken the other.
- Anonymity is a density budget, not an absolute: residual linkage never reaches zero
  and protection grows with real traffic sharing the cover.
- macOS and Windows binaries are not offered yet; build from source.

## Contact and provenance

Site source and deploy pipeline: the getthemix-website repository (the /dl artifacts
are built from the mixnet repository's seed workspace by the same deploy that
publishes this page, so page and artifacts cannot drift apart).