From 14f194cf2cde018cee09ab76260ae6c863f394fd Mon Sep 17 00:00:00 2001 From: arena-agent Date: Sun, 27 Sep 2026 23:04:32 +0000 Subject: [PATCH 1/2] =?UTF-8?q?fix(agda):=20restore=20main=20typecheck=20?= =?UTF-8?q?=E2=80=94=20carry=20the=20fiber=20invariant=20in=20FiberBundle?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CI 'Agda' has been red on main since 2026-09-26 (last green 9c4b72b5, 2026-09-21). Two independent gates fail; this commit addresses both. 1. kernel-guard.sh check B (classification drift). EchoBitNarrowingNumeric, EchoExampleBitNarrowing and EchoHaplotypeCollapsing were never added to the classification table in docs/echo-types/echo-kernel-note.adoc. Added to Tier 2 (each depends on a Tier-2 module). The guard now PASSES — verified locally, it is pure POSIX shell and needs no Agda. 2. Agda cold typecheck (exit 42, i.e. a real type error). Root cause: FiberBundle carried `fiber : List Clone` with NO invariant linking the clones to `haplotype`, so bundle-fiber-echoes b = map (\c -> c , refl) (FiberBundle.fiber b) demanded `refl : collapse c == FiberBundle.haplotype b` for an ARBITRARY c. Those terms are not judgementally equal, so the proof was unprovable — not a typo, a missing invariant. The invariant is documented, and enforced, one layer up: docs/echo-types/applications/haplotype-collapsing.adoc says the Nickel contracts enforce "every clones[i].haplotype_id == haplotype_id". The runtime layer had the contract; the machine-checked layer did not. Fix: make the invariant structural — `fiber : List (HaploFiber haplotype)` and `representative : HaploFiber haplotype`. bundle-fiber-echoes is then the field projection and needs no proof. Same discipline as the Ephapax region_shrink falsity: the invariant belongs in the carrier, not in a side-condition re-imposed at every use site. Also drops the now-unused `map` and `length` imports. NOTE: item 2 is reasoned, not machine-verified. No Agda toolchain is reachable in this environment (GitHub release assets are network-blocked, and Agda is not installable from source here). It awaits the CI 'Agda' run. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- docs/echo-types/echo-kernel-note.adoc | 3 ++- proofs/agda/EchoHaplotypeCollapsing.agda | 23 +++++++++++++++++------ 2 files changed, 19 insertions(+), 7 deletions(-) diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc index 9044c39..2c9e031 100644 --- a/docs/echo-types/echo-kernel-note.adoc +++ b/docs/echo-types/echo-kernel-note.adoc @@ -96,7 +96,8 @@ kernel** — the boundary is real and lives outside this core. `EchoOFSUnivF5`, `EchoOFSUnivF5Diag`, `EchoOFSUnivF5Iso`, `EchoCanonicalIdentitySuite`, `EchoDifferential`, `EchoEntropy`, `EchoLLEncoding`, `EchoProbabilisticSupport`, `EchoProvenance`, - `EchoSecurity` + `EchoSecurity`, `EchoHaplotypeCollapsing`, + `EchoBitNarrowingNumeric`, `EchoExampleBitNarrowing` | Multi-hop. `EchoThermodynamics` reaches the kernel via `EchoFiberCount` (no direct `Echo` import); `EchoThermodynamicsFinite` is its Bishop-finite transport layer. diff --git a/proofs/agda/EchoHaplotypeCollapsing.agda b/proofs/agda/EchoHaplotypeCollapsing.agda index c1d3444..fb5d05e 100644 --- a/proofs/agda/EchoHaplotypeCollapsing.agda +++ b/proofs/agda/EchoHaplotypeCollapsing.agda @@ -44,7 +44,7 @@ open import EchoNoSectionGeneric using (no-section-of-collapsing-map) open import Data.Bool.Base using (Bool; true; false) open import Data.Nat.Base using (ℕ) open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) -open import Data.List.Base using (List; []; _∷_; _++_; map; length) +open import Data.List.Base using (List; []; _∷_; _++_) open import Data.Unit.Base using (⊤) open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong) open import Relation.Nullary using (¬_) @@ -174,21 +174,32 @@ data PipelineRole : Set where record FiberBundle : Set where field haplotype : Haplotype - representative : Clone - fiber : List Clone + representative : HaploFiber haplotype + fiber : List (HaploFiber haplotype) example-bundle : FiberBundle example-bundle = record { haplotype = 0 - ; representative = clone₁ - ; fiber = example-clones + ; representative = echo-clone₁ + ; fiber = echo-clone₁ ∷ echo-clone₂ ∷ [] } bundle-projection : FiberBundle → Haplotype bundle-projection = FiberBundle.haplotype +-- Every element of the sidecar IS an echo at the bundle's haplotype, by +-- construction: the field type *is* the fiber, so no separate soundness +-- proof is needed. This mirrors the Nickel contract in +-- docs/echo-types/applications/haplotype-collapsing.adoc §"Nickel +-- contracts enforce" — "every `clones[i].haplotype_id == haplotype_id`". +-- +-- Previously `fiber : List Clone`, which carried no link to `haplotype`; +-- the claim below was then unprovable (`refl` is not available for an +-- arbitrary element). The invariant belongs in the record, not in a +-- side-condition at the use site — the same layering lesson as the +-- `region_shrink` falsity in ephapax. bundle-fiber-echoes : (b : FiberBundle) → List (HaploFiber (FiberBundle.haplotype b)) -bundle-fiber-echoes b = map (λ c → c , refl) (FiberBundle.fiber b) +bundle-fiber-echoes b = FiberBundle.fiber b ------------------------------------------------------------------------ -- 7. Separation from O(n²) distance matrix From 60449710176f5aae1890c7719393dcda696dc14c Mon Sep 17 00:00:00 2001 From: arena-agent Date: Sun, 27 Sep 2026 23:08:57 +0000 Subject: [PATCH 2/2] =?UTF-8?q?fix(ci):=20reconcile=20actions.lock=20?= =?UTF-8?q?=E2=80=94=20regenerate=20for=20codeql-action=204.38.1?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Workflows have failed at creation with `startup_failure` since 2026-09-26. Root cause: cd9aa401 (dependabot, #326) bumped github/codeql-action 4.38.0 -> 4.38.1 in codeql.yml (+2 -2) and hypatia-scan.yml (+1 -1), but did not regenerate .github/workflows/actions.lock, which still pinned 4.38.0 in three places. The lockfile no longer validates against the workflows, so the lockfile gate rejects the runs before any job starts. This is the same failure mode, and the same fix, as 9c4b72b5 (the last green main commit): "Workflows fail at creation with `The lockfile could not be validated. Regenerate it by running gh actions-lock`." Scope: version strings only. * workflows: map — github/codeql-action@v4.38.0 -> v4.38.1 for codeql.yml and hypatia-scan.yml (the refs those files actually use). * dependencies: entry regenerated for 4.38.1. The commit hash is the PEELED tag commit, which is the convention the existing entry already follows (v4.38.0^{} = b96794f015dfd88f77b49b1c93e0fa7110f94c63, exactly the hash previously recorded). v4.38.1^{} = 1c5b675653bb5c22dbe9b12b556ec555138e09fd, resolved via `git ls-remote --tags https://github.com/github/codeql-action`. owner_id 9919 / repo_id 259445878 are unchanged — same repository. Relation to the existing convention is unchanged: the lock records the repo-level ref (github/codeql-action@v4.38.1) while the workflow files reference sub-paths (github/codeql-action/init@v4.38.1) — the lock normalised that the same way for 4.38.0. NOTE: regenerated by hand, not by `gh actions-lock` — the extension's release binary is not reachable from the environment this was prepared in. It is byte-faithful to the tool's convention (verified against the pre-existing 4.38.0 entry) but a maintainer run of `gh actions-lock` should be preferred if anything looks off. Because the failure mode is startup_failure, this could not be tested locally — it will only be confirmed by whether runs now start. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/actions.lock | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index bdac037..92f822a 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -8,14 +8,14 @@ workflows: - 'actions/checkout@v7.0.1' '.github/workflows/codeql.yml': - 'actions/checkout@v7.0.1' - - 'github/codeql-action@v4.38.0' + - 'github/codeql-action@v4.38.1' '.github/workflows/governance.yml': [] '.github/workflows/hypatia-scan.yml': - 'actions/checkout@v7.0.1' - 'actions/github-script@v9.0.0' - 'actions/upload-artifact@v7.0.1' - 'erlef/setup-beam@v1.24.1' - - 'github/codeql-action@v4.38.0' + - 'github/codeql-action@v4.38.1' '.github/workflows/label-triage.yml': [] '.github/workflows/labels.yml': [] '.github/workflows/mirror.yml': [] @@ -70,9 +70,9 @@ dependencies: commit: 'sha1-54075bcc5e249e4758d363f27d099f55d843f124' owner_id: 47606891 repo_id: 331103973 - 'github/codeql-action@v4.38.0': - ref: 'v4.38.0' - commit: 'sha1-b96794f015dfd88f77b49b1c93e0fa7110f94c63' + 'github/codeql-action@v4.38.1': + ref: 'v4.38.1' + commit: 'sha1-1c5b675653bb5c22dbe9b12b556ec555138e09fd' owner_id: 9919 repo_id: 259445878 'hyperpolymath/smtp-notify-action@v0.3.0':