examples: Example 10 — abstract interpretation (Sign lattice)#82
Merged
Conversation
Adds `proofs/agda/EchoExampleAbsInt.agda` — Example 10 from the presentation-dependence cluster identified by PR #76 (abstract interpretation via a three-element Sign lattice over a hand-rolled five-element integer carrier). Headlines: - concretization-collapses, α-non-injective-on-pos - echo-pos-p1, echo-pos-p2, echo-zero-witness - distinct-echoes-same-sign - absint-classification Wired into `All.agda` (alphabetical) and `Smoke.agda` (per-lemma pins). EchoExamples.agda not modified (separate lanes also work on examples). Invariants: `--safe --without-K`; no postulates, no funext, no escape pragmas. Clean-worktree Agda build green (EchoExampleAbsInt.agda + All.agda + Smoke.agda all exit 0 on Agda 2.8.0 + stdlib). Refs #76 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The `3227b15` merge of `main` into `examples/absint-sign` silently dropped PR #83's additive changes (Example 9 parser residue, landed on main as commit `0f37f12`). This recovers them: * `proofs/agda/EchoExampleParser.agda` — restored from `main:proofs/agda/EchoExampleParser.agda` (227 lines, byte-identical to the file PR #83 added). * `proofs/agda/All.agda` — re-add `open import EchoExampleParser` alongside the AbsInt import. * `proofs/agda/Smoke.agda` — re-add the 23-line `using` block from #83 alongside this PR's AbsInt headline pins; both examples now pinned. Build invariant restored: `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K` with both Example 9 (parser) and Example 10 (AbsInt) wired in. No postulates, no escape pragmas. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Second wave of the same merge regression: the `3227b15` merge of `main` into `examples/absint-sign` also dropped PR #80's additive changes (Axis 8(4) witness-search machine, landed on main as commit `a1e9cbc`). This recovers them on top of the previous parser recovery commit `8950855`: * `proofs/agda/EchoSearch.agda` — restored from `main:proofs/agda/EchoSearch.agda` (156 lines, byte-identical to PR #80). * `proofs/agda/EchoSearchInstance.agda` — restored similarly (86 lines). * `proofs/agda/All.agda` — re-add `open import EchoSearch` + `EchoSearchInstance` (in the post-`EchoDecidable` slot per #80). * `proofs/agda/Smoke.agda` — re-add the 30-line headline-pin block for both modules, slotted between `EchoDecidable` and `EchoAccess`. Build invariant restored: `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K`. All four parallel-session additions (PRs #80 EchoSearch, #83 EchoExampleParser, plus this PR #82's EchoExampleAbsInt) are now wired in together. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Resolves the Smoke.agda conflict by keeping the Example 10 (EchoExampleAbsInt) headline-pin block alongside the parser, search, and approx pins already on main. All.agda is auto-merged with the import deduplicated (EchoExampleParser was listed twice after the naïve merge). Build invariant: `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Third wave of the same merge regression pattern that the prior fix-up commits (8950855 for #83 EchoExampleParser, 549f219 for #80 EchoSearch) already addressed: between the last main-merge and now, PR #81 landed on main, adding EchoExampleProvenance.agda and its imports/pins. Resolution: keep this PR's EchoExampleAbsInt additions and add the EchoExampleProvenance additions from main alongside them (additive on both sides — no semantic conflict, both examples coexist). * proofs/agda/All.agda — both `open import EchoExampleAbsInt` and `open import EchoExampleProvenance` retained; EchoExamples (which the conflict block had duplicated) appears once. * proofs/agda/Smoke.agda — both the Example 10 (AbsInt) pin block and the Example 5 (Provenance) pin block retained, in that order. * proofs/agda/EchoExampleProvenance.agda — restored from main (new file on this branch). Build invariant restored: `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K`. All examples added by parallel sessions (#80 EchoSearch, #81 EchoExampleProvenance, #83 EchoExampleParser, plus this PR #82 EchoExampleAbsInt) are wired in together. No postulates, no escape pragmas. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Owner
Author
|
Pushed a merge-resolution commit ( Cause — same pattern as the existing fix-up commits Resolution — additive merge keeping both EchoExampleAbsInt (this PR's contribution) and EchoExampleProvenance (from main). No semantic conflict — they are independent examples; All.agda and Smoke.agda now wire in both. Heads-up to the original author session: I pushed this from a parallel Claude session — if you have local in-progress work on this branch, 🤖 Posted by a parallel Claude Code session |
11 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 20, 2026
…landed (#89) Updates the `Current rung state (2026-05-20)` block to record Wave 3 of today's swarm and refresh the next-Claude plan. ## What this captures * 5 Wave-3 PRs (`#80` EchoSearch, `#81` provenance, `#82` absint, `#83` parser, `#85` EchoCost) and 2 parallel-session merges (`#84` Pillar E Evaluation, `#86` F1 gc-coassoc). * Axis 8 is now 4-of-4 (decidability + graded access + cost + search). * Next-Claude plan refreshed: ordinal-track unbudgeted WF is the named next bottleneck; EchoApprox examples 6/8 still open; EchoSearch sequential/product composition deferred. ## Two minor lessons memorialised * Per-lane Smoke `open import ... using ( ... )` blocks should be separate (with header comments), not shared paren-blocks — cuts swarm merge-conflict noise. * During swarm-merge sequences, re-fetch the branch before any force-push: parallel claude sessions may be concurrently rebasing the same PR (observed on `#82`). ## Invariants * Doc-only change; no Agda touched. * `--safe --without-K` invariant unchanged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
4 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 20, 2026
…luster landed (#92) ## Summary Three small accuracy passes through `docs/echo-types/` after the earn-back programme, the §"Theory work — no proof assistant needed" section, and the canonical examples cluster (5/9/10) all closed in this session. Pure prose; no Agda changes. ### 1. `roadmap.md` §"Theory work" — two stale items refreshed * **Axis 8** line said the *decidability-respecting* candidate had shipped but listed the other three as still candidate refinements. All four have now shipped: `EchoDecidable`, `EchoCost` (#85), `EchoAccess` (#68 / #75), `EchoSearch` (#80). Updated to credit all four. * **Negative / co-echoes** line was `[unblocked]`; now `[landed]` — `AntiEcho` (#69), tropical decomposition concrete + generic (#72 + #91), `antiecho-partition-dec` (#90). Names the `coecho.md` §5 obligation-5 / obligation-6 closures explicitly. After these edits, every item in §"Theory work — no proof assistant needed" is either `[landed]` or `[ruled out]`/`[refreshed]` — the section is genuinely closed. ### 2. `roadmap.md` §"Example work" — three items landed * ex. 5 (`EchoExampleProvenance`, #81) → `[landed]` * ex. 9 (`EchoExampleParser`, #83) → `[landed]` * ex. 10 (`EchoExampleAbsInt`, #82) → `[landed]` Only ex. 6 (approximate-echo numeric example) remains `[unblocked]`. ### 3. `earn-back-plan.adoc` — stale `roadmap-gates.adoc` claim corrected * Header note used to say "the gate discipline was historically attributed to a `roadmap-gates.adoc`; that file does not exist in-tree". The file **does** exist (created 2026-05-18; see its preamble). Header rewritten to list `roadmap-gates.adoc` alongside `retractions.adoc` / this plan / `next-questions.adoc` as the four canonical loci. * Ledger row D (the "doesn't exist" entry) marked **CLOSED 2026-05-20** with the cite reflecting current reality. ## Test plan * [x] Pure docs / `.adoc` / `.md` edits — no Agda touched * [x] `agda proofs/agda/All.agda` exit 0 (confirms docs match code) * [x] `agda proofs/agda/Smoke.agda` exit 0 * [x] No retracted-claim language moved; no earned-back claim overclaimed; `paper.adoc` / `types-abstract.adoc` / `conservativity.adoc` untouched ## Scope Disjoint from all currently-open PRs: * #88 (F3) — touches Agda + `retractions.adoc` (different sections) + `earn-back-plan.adoc` Status (different section from header / ledger-D) * #90 (partition-dec) — touches Agda only * #91 (generic-codomain) — touches Agda + preamble comments No retracted claim is moved. No earned-back claim is overclaimed. `paper.adoc` / `types-abstract.adoc` / `conservativity.adoc` are intentionally untouched (owner-gated, per the posture set by #86 / #88). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 20, 2026
…nstances (#88) ## Summary Gate **F3** of the earn-back plan (`docs/echo-types/earn-back-plan.adoc §F3`) now passes. Two non-isomorphic-grade-monoid instances of an abstract graded-comonad interface, with no `⊑-prop`-equivalent field in the interface itself, are mechanised: * **`nat-instance`** at the **commutative** monoid `(ℕ, +, 0)` — packages the F1 (#86) iterated-residue construction. * **`list-instance`** at the **non-commutative** free monoid `(List Tag, ++, [])` over a two-element `Tag` with per-element residue layers `R smol A = A × Bool`, `R big A = A × ℕ`. All three graded-comonad laws proved. The non-isomorphism is constructively witnessed by `tag-list-non-commutative` (one direction: only a non-commutative monoid satisfies it). The two earn-back gates F1 and F3 — both landed today — close the comonad-side earn-back programme as specified. ## Three new modules ### `EchoGradedComonadInterface.agda` — abstract record `GradedComonadStructure` fields: * Grade monoid: `G`, `1G`, `_·G_`, the three monoid laws. * Graded carrier: `D : G → Set → Set`, `mapD`, functor laws. * Counit `ε : D 1G A → A` at the unit grade. * **Nested** comultiplication `δ : D (g ·G h) A → D g (D h A)`. * The three graded-comonad laws stated against `subst` along the monoid's propositional identities. **No `⊑-prop`-equivalent field** — F3 guardrail honoured by construction. Inspect the field list at the top of the module. ### `EchoGradedComonadInstance1.agda` — F1 packaged `nat-instance : GradedComonadStructure` reuses `EchoGradedComonadF1.D / mapD / ε / δ / gc-counit-l / gc-counit-r / gc-coassoc` verbatim; stdlib's `+-identityˡ / +-identityʳ / +-assoc` supply the monoid laws. No adapter lemma needed — F1's signatures already use `subst` along the corresponding ℕ-equation proofs. ### `EchoGradedComonadInstance2.agda` — free-monoid instance `list-instance : GradedComonadStructure` at `(List Tag, ++, [])`. Construction parallels F1: * `D [] A = A`; `D (x ∷ xs) A = R x (D xs A)`. * `mapD-id`, `mapD-∘` by structural induction (per Tag). * `D-++` proves the type equality `D (xs ++ ys) A ≡ D xs (D ys A)` inductively; `δ = coe (D-++ xs ys A)`. * `gc-counit-r`: definitional (`++-identityˡ _ = refl` in stdlib). * `gc-counit-l` / `gc-coassoc`: structural induction on the grade list, cons step splitting on the head `Tag`. Same `δ`-naturality + `subst`-over-residue factoring as F1's `gc-coassoc`. * `D-nontrivial`: separating witness that `D (smol ∷ big ∷ []) Bool` is not collapsing to `⊤` / a prop. ## Build invariant * `agda proofs/agda/All.agda` exit 0 under `--safe --without-K` * `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K` * **zero postulates, no funext, no escape pragmas** anywhere in the three new modules * both instances wired into `All.agda`; record + both instances + non-isomorphism witness + non-triviality witness pinned in `Smoke.agda` ## Scope (please re-read with care) F3 earns back the two-models claim **for the graded-comonad witness introduced by F1** — there are two genuinely non-isomorphic grade-monoid models of the `GradedComonadStructure` interface, the laws hold at each, the interface itself is `⊑-prop`-free. That is exactly what the gate asked for. F3 does **NOT** earn back the older `EchoRelModel`/`GCLaws` two-models claim retracted at R-2026-05-18 finding 3. That retraction concerned `set-model` and `rel-model` (both at the same grade poset, with `⊑-prop` baked in as a field, `rel-model = set-model × ⊤`, agreement by `refl`). The `GradedLossModel` interface there still has `⊑-prop`; that situation is unchanged. F3 here is about a **different** abstract interface and a **different** pair of models. The two earn-backs are not interconvertible — do not cite one as evidence for the other. `paper.adoc`, `types-abstract.adoc`, and `conservativity.adoc` remain untouched. Their bodies are about `EchoGraded`'s thin-poset structure, which neither F1 nor F3 changes. The combined F1+F3 result strengthens the case for a bounded "new contribution" paragraph, but the title / thesis / reindexing-modality framing should not move on these gates alone — owner-gated, as for F1. ## Doc updates (gated, scoped) * `docs/echo-types/earn-back-plan.adoc` — ledger row A3 (Unstarted → PASSED), Sequencing entry added, Status entry with the strict scope qualifier above. * `docs/retractions.adoc` — follow-up **F-2026-05-20b** appended (append-only revision policy preserved); the scope qualifier pinned in prose. ## Dependencies * Builds on **#86** (F1 PASSED). Branch based on `f1-coassoc-earn-back`; will rebase cleanly onto `main` once #86 lands. * Disjoint from **#82** (AbsInt) and **#84** (paper Evaluation — already merged). ## Test plan * [x] Interface module typechecks * [x] Instance 1 (nat) typechecks * [x] Instance 2 (list) typechecks — all three comonad laws * [x] Full `All.agda` build green * [x] `Smoke.agda` build green * [x] No postulates, no escape pragmas, no funext in any new module * [x] No `⊑-prop`-equivalent field in the interface record * [x] Non-commutativity witness for the second grade monoid * [x] Non-triviality witness for the second carrier * [ ] (owner) inspect field list of `GradedComonadStructure` — flag anything `⊑-prop`-shaped if present * [ ] (owner) ratify the F-2026-05-20b scope language in `retractions.adoc` 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds
proofs/agda/EchoExampleAbsInt.agda— Example 10 from thepresentation-dependence cluster identified by PR #76.
What lands
{neg, zero, pos}(no ⊥/⊤ — the headline is "manyconcretes ↦ one abstract", which the three-element lattice
already exhibits; ⊥/⊤ is a Galois-closure refinement, separate
story)
{m2, m1, z, p1, p2}(avoids dragging
Data.Integerinto a small worked example)α : Carrier → Signcollapsing{m1, m2} ↦ neg,{z} ↦ zero,{p1, p2} ↦ posconcretization-collapses,α-non-injective-on-pos,echo-pos-p1,echo-pos-p2,echo-zero-witness,distinct-echoes-same-sign,absint-classificationAll.agda(alphabetical) +Smoke.agda(per-lemmapins matching the suite's
usingconvention)Cluster relationship
Abstract interpretation is the canonical compiler-analysis lens
on Echo: the abstraction is the structured loss, and Echo carries
the concretes that collapse to a given abstract value. The
widening / approximate-echo half of Example 10 (axis 2; ties
to Example 6) is not addressed here — it lives in the
EchoApproxtolerance-graded family. This PR is the exact-Galois-abstraction half only.
absint-classificationis the abstract-interpretation analogueof
EchoCharacteristic.collapse-classificationand the standard"preimage class is the partition cell" statement.
Invariants
--safe --without-K; no postulates, no funext, no escape pragmasagda --safe --without-K EchoExampleAbsInt.agda→ exit 0agda --safe --without-K All.agda→ exit 0agda --safe --without-K Smoke.agda→ exit 0(Agda 2.8.0 + stdlib v2; verified in
/tmp/echo-types-worktrees/ex10on origin/main
4015df6)EchoExamples.agdaNOT modified (other lanes also work on theexamples cluster — new file is cleaner)
Refs #76
🤖 Generated with Claude Code
Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com