harden(foundation P1): reproducible CI-via-flake exact pin (additive verifier)

flake.nix evolved to pin the toolchain reproducibly:
  * Agda via nixpkgs nixos-24.11 (2.7.0.1)
  * standard-library tag v2.3 as a flake input (was nixpkgs-bundled,
    a DIFFERENT version than CI/local verify against)
  * absolute-zero @3ff5cee as a flake input (was a local ~/dev
    checkout — not reproducible / not CI-usable)
plus a hermetic checks.suite (guardrail + 4 roots + N5 xfail) under
that pinned toolchain.

CI: additive  job runs . ADDITIVE and
continue-on-error: the apt  +  jobs remain the
gate, so the 2.7.0.1-vs-verified-2.8.0 delta (if any) is SURFACED,
not a regression. First green run is the P1 verification.

Honest constraints, flagged not hidden (triage, not a blind cutover):
  * no  in the dev env → flake authored designed-correct,
    verified BY CI, NOT locally claimed green; libraries file built
    via writeText+cp (no heredoc/indentation hazard) to de-risk the
    one fragile part by construction.
  * cross-stack: a devShell-only flake.nix also lives on the reframe
    stack (#47, commit 185eb74); THIS strictly supersedes it (adds
    pins+checks, no behavioural conflict) — take this at integration.
  * Agda 2.7.0.1 vs verified 2.8.0 is an explicit surfaced decision,
    not an assumption; reconcile via the logged CI delta.

docs/foundation.adoc P1 item moved tracked-followup -> implemented,
pending first-green CI verification; revision history appended.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/agda.yml

@@ -179,3 +179,28 @@ jobs:
           agda --ignore-interfaces -i proofs/agda proofs/agda/Smoke.agda
           agda --ignore-interfaces -i proofs/agda proofs/agda/characteristic/All.agda
           agda --ignore-interfaces -i proofs/agda proofs/agda/examples/All.agda
+
+  flake-check:
+    # Foundation P1: the reproducible, exactly-pinned toolchain.
+    # `nix flake check` runs flake.nix's hermetic `checks.suite`
+    # (flake-pinned Agda + PINNED stdlib v2.3 + PINNED absolute-zero
+    # @3ff5cee, guardrail + 4 roots + N5 xfail). ADDITIVE: the apt
+    # `check` and `cold-check` jobs remain the gate, so a version
+    # delta surfaced here (e.g. 2.7.0.1 vs verified 2.8.0) is
+    # informative, not a regression. Its first green run IS the P1
+    # verification (the dev env has no nix; CI is the verifier).
+    # Flip continue-on-error to false once it is first green.
+    runs-on: ubuntu-latest
+    continue-on-error: true
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+
+      - name: Install Nix (pinned action)
+        uses: cachix/install-nix-action@08dcb3a5e62fa31e2da3d490afc4176ef55ecd72  # v30
+        with:
+          extra_nix_config: |
+            experimental-features = nix-command flakes
+
+      - name: nix flake check (hermetic, reproducible)
+        run: nix flake check --print-build-logs

docs/foundation.adoc

@@ -89,12 +89,25 @@ hack: left explicit and failing, never forced green.
 
 == Known limitations (tracked, not silent)
 
-. *CI Agda version not exactly pinned.* CI installs Ubuntu's `agda`
-  (apt); local dev and the Nix flake differ (2.8.0 / flake-pinned).
-  The CI step *records and minimally asserts* the version (fails on a
-  wildly wrong major) so it is visible, not silently floating. Exact
-  parity via *CI-through-the-flake* is the tracked P1 follow-up — the
-  only honest way to pin Agda reproducibly.
+. *CI Agda exact pin* — *reproducible pin IMPLEMENTED 2026-05-18;
+  first-green verification delegated to CI.* `flake.nix` now pins, as
+  flake inputs: Agda via `nixpkgs nixos-24.11` (2.7.0.1), standard
+  library at tag `v2.3`, and `absolute-zero` at commit `3ff5cee…`
+  (previously nixpkgs-bundled stdlib + a local `absolute-zero`
+  checkout — neither reproducible). A hermetic `checks.suite`
+  (guardrail + four roots + N5 xfail) runs under that pinned
+  toolchain; an *additive* `flake-check` CI job (`nix flake check`)
+  exercises it. This is honest about its boundary: the dev
+  environment has no `nix`, so the flake was authored designed-correct
+  but its build is *first verified by CI*, not claimed green here. It
+  is `continue-on-error` until first green so a version delta
+  (2.7.0.1 vs the verified-green 2.8.0 / apt) is *surfaced*, not a
+  regression; the apt `check` + `cold-check` jobs remain the gate.
+  Open sub-item: on first green, flip `continue-on-error` to `false`
+  and retire the apt job; if red, the logged delta says which
+  nixpkgs/Agda to bump. (Cross-stack: a devShell-only `flake.nix`
+  also exists on the reframe stack PR #47; this one strictly
+  supersedes it.)
 . *External-fibre triangulation* — *DONE 2026-05-18*,
   `proofs/agda/EchoFiberTriangulation.agda` (wired into `All.agda`,
   pinned in `Smoke.agda`, `--safe --without-K`, zero postulates).
@@ -157,3 +170,12 @@ Pinned inputs: `standard-library` `v2.3`; `absolute-zero`
   follow-up entry is intentionally deferred to stack reconciliation
   (the append-only log evolves on the reframe/earn-back stack; adding
   a divergent entry on this `main`-based branch would fork it).
+* *2026-05-18 — CI-via-flake reproducible pin implemented.*
+  `flake.nix` evolved to pin Agda (nixpkgs nixos-24.11) + stdlib v2.3
+  + absolute-zero @3ff5cee as flake inputs, with a hermetic
+  `checks.suite`; additive `flake-check` CI job
+  (`continue-on-error`) added as the verifier. Authored without local
+  `nix` (none in dev env) — designed-correct, CI-verified, not
+  locally claimed green; flagged as such, gate unchanged. P1 item
+  status moved from "tracked follow-up" to "implemented, pending
+  first-green CI verification".

flake.nix

@@ -0,0 +1,117 @@
+{
+  # SPDX-License-Identifier: PMPL-1.0-or-later
+  #
+  # Reproducible toolchain for echo-types — foundation P1 (CI-via-flake
+  # exact pin; docs/foundation.adoc §"Known limitations").
+  #
+  # CROSS-STACK NOTE. A simpler devShell-only flake.nix also exists on
+  # the reframe stack (commit 185eb74, PR #47). THIS file is a strict
+  # evolution of it (same devShell tools + PINNED Agda-library inputs +
+  # a hermetic `checks` output). At integration, this harden-stack
+  # version supersedes the reframe-stack one — no behavioural conflict,
+  # it only adds pins and checks.
+  #
+  # PINNING DECISION (explicit, surfaced — not assumed):
+  #   * Agda: nixpkgs `nixos-24.11` -> agda 2.7.0.1 (also ghc 9.6.6,
+  #     cabal 3.12.1.0, rustc 1.82.0, just 1.38.0 — .tool-versions
+  #     match). The verified-green local toolchain is agda 2.8.0; CI's
+  #     apt job runs yet another. The suite has so far proven robust
+  #     across apt-agda and 2.8.0; whether it also typechecks under
+  #     2.7.0.1 + stdlib v2.3 is VERIFIED BY the additive
+  #     `nix flake check` CI job, not assumed here. If that job is red
+  #     it surfaces the exact version delta to reconcile (bump the
+  #     nixpkgs input); the apt + cold-check jobs remain the gate
+  #     meanwhile, so nothing regresses.
+  #   * standard-library: PINNED to tag v2.3 as a flake input (was
+  #     nixpkgs-bundled — a different version than CI/local verify).
+  #   * absolute-zero: PINNED to commit 3ff5cee… as a flake input
+  #     (was a local ~/dev checkout — not reproducible / not CI-usable).
+  #
+  # NOTE: authored without a local `nix` (none in the dev env);
+  # flake.lock is generated and the build first verified BY CI.
+  # Designed-correct, CI-verified — not locally claimed green.
+  description = "echo-types reproducible toolchain (Agda + libs pinned)";
+
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.11";
+    agda-stdlib = {
+      url = "github:agda/agda-stdlib/v2.3";
+      flake = false;
+    };
+    absolute-zero = {
+      url = "github:hyperpolymath/absolute-zero/3ff5cee7f3fd002378089cd02f0c90a3747b45f0";
+      flake = false;
+    };
+  };
+
+  outputs = { self, nixpkgs, agda-stdlib, absolute-zero }:
+    let
+      systems = [ "x86_64-linux" "aarch64-linux" "x86_64-darwin" "aarch64-darwin" ];
+      forAllSystems = nixpkgs.lib.genAttrs systems;
+
+      # The Agda libraries file as an exact store file — no heredoc,
+      # no Nix-string indentation hazard. Agda resolves each
+      # `.agda-lib`'s `include:` relative to that file's own directory,
+      # so pointing at the pinned inputs' own `.agda-lib` paths is
+      # sufficient. (Nix `"..."` interprets `\n` as a real newline.)
+      mkLibs = pkgs: pkgs.writeText "agda-libraries"
+        "${agda-stdlib}/standard-library.agda-lib\n${absolute-zero}/absolute-zero.agda-lib\n";
+    in {
+      devShells = forAllSystems (system:
+        let
+          pkgs = import nixpkgs { inherit system; };
+          libs = mkLibs pkgs;
+        in {
+          default = pkgs.mkShell {
+            name = "echo-types";
+            packages = [
+              pkgs.agda pkgs.just pkgs.ghc pkgs.cabal-install
+              pkgs.rustc pkgs.cargo pkgs.rustfmt pkgs.clippy
+            ];
+            shellHook = ''
+              export AGDA_DIR="$PWD/.agda"
+              mkdir -p "$AGDA_DIR"
+              cp -f ${libs} "$AGDA_DIR/libraries"
+              chmod u+w "$AGDA_DIR/libraries"
+              echo "echo-types devShell (PINNED):"
+              command -v agda >/dev/null && echo "  agda  : $(agda --version 2>/dev/null | head -n1)"
+              echo "  stdlib: v2.3 (flake input, pinned)"
+              echo "  absz  : 3ff5cee (flake input, pinned)"
+            '';
+          };
+        });
+
+      # Hermetic, reproducible verification: the flake-pinned Agda over
+      # the pinned stdlib v2.3 + absolute-zero, running the same
+      # guardrail + four roots + N5 expected-failure gate that CI's
+      # apt job runs. `nix flake check` exercises this.
+      checks = forAllSystems (system:
+        let
+          pkgs = import nixpkgs { inherit system; };
+          libs = mkLibs pkgs;
+        in {
+          suite = pkgs.runCommand "echo-types-suite"
+            { nativeBuildInputs = [ pkgs.agda pkgs.bash ]; }
+            ''
+              export HOME="$TMPDIR"
+              mkdir -p "$HOME/.agda"
+              cp -f ${libs} "$HOME/.agda/libraries"
+              # Agda needs a writable source tree (.agdai outputs).
+              cp -r ${self} src
+              chmod -R u+w src
+              cd src
+              bash tools/check-guardrails.sh proofs/agda
+              agda -i proofs/agda proofs/agda/All.agda
+              agda -i proofs/agda proofs/agda/Smoke.agda
+              agda -i proofs/agda proofs/agda/characteristic/All.agda
+              agda -i proofs/agda proofs/agda/examples/All.agda
+              if agda -i proofs/agda proofs/agda/characteristic/N5Falsifier.agda \
+                   > /dev/null 2>&1; then
+                echo "N5Falsifier unexpectedly typechecks — see foundation.adoc"
+                exit 1
+              fi
+              touch "$out"
+            '';
+        });
+    };
+}