sync: re-vendor absolute-zero/ subtree to upstream HEAD (trusted-base + 16-commit catch-up)#83
Merged
Conversation
Brings maa-framework's vendored absolute-zero/ tree from its previous snapshot (16+ commits behind) up to current upstream HEAD. The primary motivation is to pull in the standards#203 trusted-base reduction work that landed upstream today: - absolute-zero#52 — docs/proof-debt.md seed (standards#203 schema). - absolute-zero#58/#59 — Phase 1 per-axiom triage of 72 Coq Axioms (docs/proof-debt-triage.md). - absolute-zero#60 — Phase 2a Lambda cluster (Coq + Lean inline AXIOM: annotations). - absolute-zero#61 — Phase 2b CNOCategory.v hom_functor §(d) DEBT entry. - absolute-zero#62 — Phase 2c Filesystem cluster (26 inline annotations + 8 §(d) DEBT entries). Cumulative trusted-base state: 41/129 escape hatches now documented (35.7% covered). Remaining 88 belong to Quantum + Physics clusters (future Phase 2d/2e PRs upstream). Side effects of the full re-vendor (also pulled in): - Estate-policy / governance / hypatia / language-policy workflow updates (~15 .github/workflows files). - MPL-2.0 SPDX header migration from PMPL-1.0-or-later (~20 files). - .machine_readable A2ML updates. - ReScript interpreter removal (per estate language-policy ban). - Verification scripts moved to verification/ subdir. - Old session debris pruned (SONNET-HANDOFF.md, STACK_AUDIT.txt, ROADMAP-V1-TO-V12.adoc, ROADMAP-UPDATED.adoc, etc.). Preserved (maa-framework-specific Agda extensions, NOT in upstream): - proofs/agda/EchoBridgeCNO.agda - proofs/agda/EchoBridgeScaffold.agda - proofs/agda/README.adoc These were added in maa-framework directly (commits 0538283 and e80c5fb) and survive the re-vendor via rsync --filter='P ...'. Refs maa-framework own proof-debt rollout; absolute-zero#52, #58, #59, #60, #61, #62; standards#203. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
4 tasks
hyperpolymath
added a commit
to hyperpolymath/absolute-zero
that referenced
this pull request
May 27, 2026
…vendored copy (#65) ## Summary Upstreams 3 Agda files that exist only in maa-framework's vendored copy of absolute-zero, but self-identify as absolute-zero artefacts. - `proofs/agda/EchoBridgeScaffold.agda` — compile-safe interface (`Echo` Σ-shape, `CNOModel`), intentionally independent of `CNO.agda`. - `proofs/agda/EchoBridgeCNO.agda` — concrete instantiation from `CNO.Program` / `CNO.eval` into the scaffold. - `proofs/agda/README.adoc` — describes the directory. ## Why now Discovered during proof-debt classification triage for maa-framework (filed at hyperpolymath/maa-framework#82, with disposition analysis in hyperpolymath/maa-framework#84). The maa-framework re-vendor (hyperpolymath/maa-framework#83) currently uses `rsync --filter='P ...'` to *preserve* these files across each sync — once they're upstream, that filter becomes redundant. The README.adoc literally titles itself "Agda Proofs (absolute-zero)" and the scaffold header says "Echo/CNO Agda bridge scaffold", so the canonical home is here. ## Trusted-base impact The 3-file set has **zero postulates and zero axioms**. `EchoBridgeCNO.agda` imports `Axiom.Extensionality.Propositional` to obtain the `Extensionality` *type*, which is then accepted as an explicit *module parameter* by downstream functions — not postulated. Documented in `docs/proof-debt.md` under a new "False positives" section to satisfy `check-trusted-base.sh`'s path-enumeration clause. ## Test plan - [ ] `cd proofs/agda && agda EchoBridgeScaffold.agda` typechecks. - [ ] `cd proofs/agda && agda EchoBridgeCNO.agda` typechecks (may need `CNO.agda` build prerequisites). - [ ] `bash scripts/check-trusted-base.sh .` passes (path-enumeration covers the false positive). - [ ] CI green. ## Companion - hyperpolymath/maa-framework#82 — proof-debt schema PR (parallel). - hyperpolymath/maa-framework#83 — re-vendor PR (parallel; this PR removes its need for `rsync --filter='P ...'`). - hyperpolymath/maa-framework#84 — fork-vs-vendor disposition issue (open, owner-decision). - hyperpolymath/standards#203 — trusted-base reduction policy. - hyperpolymath/standards#211 — `check-trusted-base.sh`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> 🤖 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.
Summary
Re-syncs maa-framework's vendored
absolute-zero/tree from itsprevious snapshot (16+ commits behind) up to current upstream HEAD
(commit
ab35c07).Primary motivation: pull in standards#203 trusted-base work
docs/proof-debt.mdper standards#203 schemadocs/proof-debt-triage.md)AXIOM:annotationsCNOCategory.v:323hom_functor§(d) DEBT entryCumulative trusted-base state: 41 / 129 escape hatches documented
(35.7% covered). Remaining 88 belong to Quantum + Physics clusters
(future Phase 2d/2e PRs upstream).
Side effects of the full re-vendor
Because the vendored tree was 16+ commits behind, the sync also pulls
in unrelated upstream work:
updates (~15
.github/workflows/*files)..machine_readable/A2ML updates.interpreters/rescript/*deleted).verification/subdir.SONNET-HANDOFF.md,STACK_AUDIT.txt,ROADMAP-V1-TO-V12.adoc,ROADMAP-UPDATED.adoc, etc.).Preserved (maa-framework-specific, NOT in upstream)
Three Agda extensions were added in maa-framework directly (commits
0538283+e80c5fb) and survive the re-vendor via rsync filters:proofs/agda/EchoBridgeCNO.agdaproofs/agda/EchoBridgeScaffold.agdaproofs/agda/README.adocVerification
Matches upstream exactly. The 41 documented entries are Lambda (5) +
CNOCategory (1) + already-passing (1) + Filesystem (34).
Scope warning
This is a large PR (168 files changed) because of the catch-up. If
desired, I can re-do this as two PRs:
But that requires hand-curating the file list. The single-PR shape
matches the "full re-vendor" option from the planning question.
Refs absolute-zero#52, #58, #59, #60, #61, #62; standards#203.
🤖 Generated with Claude Code