foundation.adoc

Echo Types — Foundation and Trusted Base

Foundation

Echo f y := Σ (x : A) , (f x ≡ y) is the standard dependent fibre. The ordinary kernel uses Agda dependent pairs and propositional equality. EchoFiberTriangulation.agda compares this definition with standard-library surjection witnesses; it is calibration and orientation coherence, not an independent soundness metatheorem.

Audited baseline: 2026-11-06

The baseline is main commit cd85288dcce55191ad477c0fa7d1d2421514a0d3, tree 74db6f3b4f4907ca02fb45903a161e1546b9ff6e. Its recorded successful remote Agda run is 41687674126. This is evidence for that revision and workflow, not certification of subsequent local edits.

The baseline inventory is 382 tracked files and 147 Agda files. Excluding three residual ordinal files leaves 144 in scope. The union of the seven workflow-root import closures contains 127 in-scope files, leaving 17 outside: ten tutorial files plus EchoDecorationBridge, EchoExampleSignAnalysis, EchoFidelity, EchoImageFactorizationPropPostulated, MinimalCNO, SimpleTest, and WorkingCNO. These are dated baseline counts; adding local modules changes them.

Baseline workflow and profiles

At the audited baseline, the owning source was .github/workflows/agda.yml. Its seven roots were:

• All.agda

• Smoke.agda

• characteristic/All.agda

• examples/All.agda

• EchoImageFactorizationPropCubical.agda

• experimental/echo-additive/All.agda

• NarrowingSmoke.agda

The ordinary roots use --safe --without-K --cubical-compatible. The Cubical root is checked separately with --safe --cubical. The cold lane adds --ignore-interfaces; the warm lane uses interfaces. A green collection of roots is not a typecheck of every tracked Agda file.

characteristic/N5Falsifier.agda is imported by characteristic/All.agda; there is no current expected-failure gate. Earlier reports of a deliberately broken excluded N5 describe an earlier state.

tools/check-guardrails.sh scans beyond the root closures, but explicitly exempts EchoImageFactorizationPropPostulated, EchoImageFactorizationPropCubical, and EchoDecorationBridge. Thus “every module is safe and postulate-free” is false as a repository-wide claim. The exemptions do not all have the same reason: the Cubical file is safe in its own profile; the postulated and exploratory files carry different trust obligations.

The Cubical file constructs truncation in a separate, self-contained restatement. It does not import the ordinary Echo interface literally. Relating those presentations is a separate boundary obligation.

Baseline toolchain

The audited baseline CI installs Agda from apt on ubuntu-latest and only asserts a 2.x version. Agda and the runner were therefore not exactly pinned in that revision. The standard library checkout at tag v2.3 is verified against commit 8326c7475af1fa456ca04a0203c168d5d7ff842b; absolute-zero is checked out and verified at f486c29903434589117fa0662c6f29b0f17d1d5f.

The audited baseline contains no reproducible flake-style toolchain pin after the Nix-to-Guix removal (#275), and its workflow contains no corresponding check job. Its echo messages refer to absent facilities. Those were stale workflow prose, not evidence of a reproducible toolchain. Baseline library pins live in .github/workflows/agda.yml; its Agda executable is apt-selected. Earlier revision-history entries below record historical claims and do not establish the current files or checks.

Current local workflow changes (2026-11-06 source inspection)

The local replacement workflow uses ubuntu-24.04 and calls scripts/setup-agda.sh. That script declares Agda 2.7.0.1, verifies its Linux x86-64 release archive against SHA256 975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a, and verifies standard-library commit 8326c7475af1fa456ca04a0203c168d5d7ff842b and absolute-zero commit f486c29903434589117fa0662c6f29b0f17d1d5f. The executable and library pins now live in that setup script; workflow calls and profiles remain in .github/workflows/agda.yml. This is source inspection of the local configuration, not a new successful remote workflow receipt.

The draft workflow adds AuditSmoke.agda to the ordinary checks and separates experimental/narrowing/Cubical work into their own jobs. The baseline seven-root counts above and the completed local compiler receipts remain evidence about their stated checks, not evidence that the changed GitHub configuration has executed successfully.

Current static entrypoints include sh scripts/check-agda-invocations.sh and bun tools/audit-inventory.mjs. The latter replaces the historical Python inventory command; conversion equivalence is checked separately from proof typechecking. mise.toml lists Bun and just; Agda setup is handled by the dedicated script.

Reproducing and interpreting evidence

Register the pinned standard-library and absolute-zero libraries, then run the seven commands in the workflow using their respective profiles. Run scripts/kernel-guard.sh, tools/check-guardrails.sh, scripts/check-experimental-aggregate.sh, and scripts/check-agda-invocations.sh for the separate static checks. A source scan is not a typecheck; a successful remote baseline run is not a fresh local run. The local audit now passes all 15 direct/audit entrypoints and all seven existing roots under Agda 2.7.0.1, plus a fresh --ignore-interfaces AuditSmoke check with exit 0. Consult the evidence ledger for receipts, warnings, source identity, current inventory, and the limits of these checks. Ordinal mathematics is excluded from the audit; residual imports may still affect builds.

Revision history

• 2026-05-18 — created. Post foundation provenance audit. Records the closure-hole closure (examples.Transport), the disclosed N5 known-broken hole, the guardrail script, the absolute-zero pin, the cold-check job, and the open CI-Agda-pin / triangulation follow-ups. Append-only.

• 2026-05-18 — external-fibre triangulation delivered. EchoFiberTriangulation.agda (T1/T2/T3 against stdlib’s own Function.Definitions/Function.Bundles), wired into All.agda, pinned in Smoke.agda, full + smoke build green, guardrail OK (88 modules). The same-module self-reference of R-2026-05-18 finding 5 is removed; claimed strictly at calibration + one genuine coherence, not as a grounding metatheorem. Remaining foundational item: cross-assistant kernel check (P2). A docs/retractions.adoc 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.guix 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 guix (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".

• 2026-10-01 — absolute-zero pin moved to the first green Proofs revision. ABSZ_REF in .github/workflows/agda.yml moved from 3ff5cee7 (2026-05-18) to f486c29903434589117fa0662c6f29b0f17d1d5f (PR #334), the absolute-zero revision whose own Proofs workflow is green on Coq, Lean, Agda and Z3 (run 36864369380). The claims table and "Pinned inputs" above now read f486c299; the two 2026-05-18 entries keep 3ff5cee because they record what was pinned then. Verified by check + cold-check green on #334.

• 2026-11-06 — baseline re-audit. Corrected root coverage, N5 status, guard exemptions, exact dependency commits, and absent flake facilities. Historical entries above are retained as records of earlier assertions.

• 2026-11-06 — #335 historical-entry acceptance. The original 2026-05-18 history entries above remain unchanged, including their then-written flake.guix claim. Since #275 there is no reproducible flake-style pin in this checkout. The live absolute-zero and standard-library commit assertions are in .github/workflows/agda.yml, while Agda is installed through apt. The correction is appended rather than rewriting those historical entries.

• 2026-11-06 — current draft toolchain correction. The #335 acceptance entry immediately above records the audited baseline. The current local workflow instead calls scripts/setup-agda.sh, which owns the compiler checksum and library commit declarations. The baseline dated entries remain unchanged; the new draft has no remote success receipt in this document.