-
Notifications
You must be signed in to change notification settings - Fork 1
Round 35: chain-rule proof + expert-skill wave + BP-24 consent gate + factory hygiene #28
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from all commits
79bb2c3
af11c6a
348ad0a
9f138eb
047858b
889fa65
4cff57c
d8c24e8
79b518a
83f7fdd
2de813f
9b28ae4
bbbdec5
35d5096
ee4998e
6f9c7de
d7e84a0
f32834d
daf83e8
823037d
161e82a
5507238
91de2fa
d7d2db3
16d2348
7dc10b5
7c89be5
564f2fb
f2d4aa1
634ce89
be50bd1
176bc2e
1955894
d34ca1c
ad472ee
e67038b
bffd30b
f69d7b6
c6224e4
0db46c4
0209f7c
e60ab6e
ed9bb99
d368d2b
9723d89
853ab31
1117fba
72e2d7e
eefddd4
3e4e989
6edfa79
53e66c3
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| @@ -1,113 +1,91 @@ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| # Current Round — 34 (open) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Round 33 closed — 15 PRs merged, `docs/VISION.md` went from | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| nothing to v11 across a cascade of Aaron edits. Round 34 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| opens with a rich vision to execute against. Track A | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| (LawRunner), Track B (security follow-through), and the | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| newly-surfaced round-33 factory + vision items are all | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| candidates for 34's anchor. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| # Current Round — 36 (open) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Round 35 closed — expert-skill spawn wave (batches #20-69, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ~50 skills), chain-rule proof fully closed at the Lean4 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| level (`T5/B1/B3/chain_rule` verified against Budiu et al. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| §4.4) plus the signed-delta semi-naive LFP TLA+ spec for | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| portfolio-of-two verification, BP-24 Elisabeth consent | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| gate + human-maintainer seat governance landing, the | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| no-empty-dirs CI gate, LiquidF# moved to Hold after the | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Day-0 build check failed. See `docs/ROUND-HISTORY.md` for | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| the full narrative. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ## Status | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - **Round number:** 34 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - **Opened:** 2026-04-18 (continuous from round-33 close) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - **Classification:** open — anchor chosen at round-open | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - **Round number:** 36 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - **Opened:** 2026-04-19 (continuous from round-35 close) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - **Classification:** open — anchor selection staged | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - **Branch topology note:** Round 35 commits land on the | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `round-34-upstream-sync` branch; the `round-36` branch | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| was staged from `main@5fdc72b` (pre-round-35 tip) for | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| clean-tree kickoff. Once the Round 35 PR merges, the | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `round-36` branch rebases onto the new `main` tip. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - **Reviewer budget:** `harsh-critic` + | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `maintainability-reviewer` floor per GOVERNANCE §20. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `security-researcher` + `threat-model-critic` on any | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| security / install-script / threat-model touch. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `spec-zealot` on any spec edit (GOVERNANCE §28). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `public-api-designer` on any public-API change. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ## Round-33 newly-surfaced P1s (ready to execute) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| From `docs/BACKLOG.md` P1 sections "SQL frontend / query | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| surface" and "Factory / static-analysis / tooling": | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 1. **`product-visionary` role spawn** — stewardship of | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `docs/VISION.md`; feeds the feature-selection loop; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| closes the "direct questions beat abstract | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| scaffolding" principle by making it a role rather | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| than an ad-hoc practice. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 2. **Pluggable wire-protocol design doc** — abstraction | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| first, then per-plugin (PostgreSQL, MySQL, Zeta- | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| native). `docs/research/pluggable-wire-protocol- | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| design.md`. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 3. **Shared query IR + LINQ integration design doc** — | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| SQLSharp's "SQL-text and integrated-query flows | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| converge on one logical planning pipeline" is the | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| pattern; Zeta needs the same convergence point. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 4. **EF Core provider scope doc** — 100% all features | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ambition needs a roadmap (query, save-changes, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| migrations, tracking, change-detection). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 5. **F# DSL design sequence** — HUGE multi-round | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| research; round 34 does step 1 (research what modern | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| SQL should look like; survey Rel/Tutorial D, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Datalog, LINQ, Kleppmann talks, relational-algebra | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| type theory). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 6. **`openspec-gap-finder` skill** (round-32 surface). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 7. **`static-analysis-gap-finder` skill** (round-33 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| surface). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 8. **documentation-agent cadence** — add to | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `factory-audit`'s every-10-rounds walk. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 9. **Upstream sync script** + **upstream-comparative- | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| analysis skill** + **upstream categorisation audit** | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| (multi-round). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 10. **Crank lint configurations to HIGH** across shellcheck, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| actionlint, markdownlint, cspell. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 11. **Declarative-manifest tiering** (match `../scratch` | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `min`/`runner`/`quality`/`all`). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ## Round-33 carry-forward (Tracks A + B re-deferred) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| **Track A — product (LawRunner):** | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - `LawRunner.checkBilinear` — join-shaped ops with a | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `BilinearOp` fixture. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - `LawRunner.checkSinkTerminal` — retraction-lossy sink | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| verification; re-run against `BayesianRateOp`. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - Config-record refactor (round-28 DEBT) before adding | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| a third law. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| **Track B — security follow-through:** | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - `packages.lock.json` adoption. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - Verifier-jar SHA-256 pinning. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - Safety-clause-diff lint on `.claude/skills/**/SKILL.md`. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - CodeQL workflow. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - Branch-protection required-check on `main` — round 33 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ran 15 green PRs, strong signal to flip. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ## Open asks to the maintainer | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Aaron decisions staged for round 34 (from VISION.md | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| "remaining gaps" + BACKLOG): | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - Wire protocol server: v1 or slip to early post-v1? | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - Admin UI tech stack (Fable/SAFE/Blazor/Avalonia)? | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - Emulate PostgreSQL vs translate on ingress/egress? | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - Which Track-A/B/factory item is round-34's anchor? | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| - Branch protection on `main` — flip now (15 green PRs | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| of evidence) or wait for round-34 green? | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `skill-tune-up` / `skill-improver` on any | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `.claude/skills/**/SKILL.md` edit. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ## Round-36 committed P0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| From `docs/BACKLOG.md` P0 "next round (committed)": | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 1. **`memory/role/persona/` restructure** — Aaron | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 2026-04-19 explicit ask: *"can we add a memory 2nd | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| level folder so it's memory/role/persona that makes | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| roles fist class defined of what we need too in the | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| memory definition"*. Scope: (a) define the role axis | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| (crosswalk `docs/EXPERT-REGISTRY.md` → role | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| directories), (b) move existing notebooks from | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `memory/persona/<name>/NOTEBOOK.md` to | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| `memory/<role>/<persona>/NOTEBOOK.md`, (c) update all | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| pointers (skill `reference patterns:` blocks, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| CLAUDE.md, AGENTS.md §18, BP-07/BP-08 rule text, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| every skill or agent with a `memory/persona/<name>` | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path). Owner: Kenji (Architect) integrates; Aarav | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| (skill-tune-up) audits post-rename for BP-drift. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Effort: M. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
Comment on lines
+36
to
+50
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 1. **`memory/role/persona/` restructure** — Aaron | |
| 2026-04-19 explicit ask: *"can we add a memory 2nd | |
| level folder so it's memory/role/persona that makes | |
| roles fist class defined of what we need too in the | |
| memory definition"*. Scope: (a) define the role axis | |
| (crosswalk `docs/EXPERT-REGISTRY.md` → role | |
| directories), (b) move existing notebooks from | |
| `memory/persona/<name>/NOTEBOOK.md` to | |
| `memory/<role>/<persona>/NOTEBOOK.md`, (c) update all | |
| pointers (skill `reference patterns:` blocks, | |
| CLAUDE.md, AGENTS.md §18, BP-07/BP-08 rule text, | |
| every skill or agent with a `memory/persona/<name>` | |
| path). Owner: Kenji (Architect) integrates; Aarav | |
| (skill-tune-up) audits post-rename for BP-drift. | |
| Effort: M. | |
| 1. **`memory/role/persona/` restructure** — human | |
| maintainer 2026-04-19 explicit ask: *"can we add a | |
| memory 2nd level folder so it's memory/role/persona | |
| that makes roles fist class defined of what we need | |
| too in the memory definition"*. Scope: (a) define | |
| the role axis (crosswalk `docs/EXPERT-REGISTRY.md` | |
| → role directories), (b) move existing notebooks | |
| from `memory/persona/<name>/NOTEBOOK.md` to | |
| `memory/<role>/<persona>/NOTEBOOK.md`, (c) update | |
| all pointers (skill `reference patterns:` blocks, | |
| CLAUDE.md, AGENTS.md §18, BP-07/BP-08 rule text, | |
| every skill or agent with a `memory/persona/<name>` | |
| path). Owner: Architect integrates; skill-tune-up | |
| audits post-rename for BP-drift. Effort: M. |
| Original file line number | Diff line number | Diff line change | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|
|
|
@@ -9,6 +9,174 @@ New rounds are appended at the top. | |||||||||
|
|
||||||||||
| --- | ||||||||||
|
|
||||||||||
| ## Round 35 — expert-skill spawn wave + chain-rule proof close + BP-24 consent gate | ||||||||||
|
|
||||||||||
| Anchor: **finish the chain-rule proof** carried from | ||||||||||
| round 34, and — once that landed — open the floor for | ||||||||||
| the **expert-skill spawn wave** Aaron had been signalling | ||||||||||
| across the preceding rounds. The round also absorbed a | ||||||||||
| sacred-tier governance landing (BP-24) and a CI-gate ship | ||||||||||
| (no-empty-dirs). | ||||||||||
|
|
||||||||||
| ### Arc 1 — chain-rule proof fully closed | ||||||||||
|
|
||||||||||
| The four-lemma chain (`T5: I_D_eq` telescoping induction, | ||||||||||
| `B1: linear_commute_I`, `B3: linear_commute_D`, and the | ||||||||||
| `chain_rule` calc block) closed in | ||||||||||
| `tools/lean4/Lean4/DbspChainRule.lean`, checked against | ||||||||||
| Budiu et al. §4.4 (task #17). `RecursiveSigned.fs` landed | ||||||||||
| as the skeleton for the retraction-safe semi-naive path | ||||||||||
| paired with a fresh TLA+ spec at | ||||||||||
| `tools/tla/specs/RecursiveSignedSemiNaive.tla`. The | ||||||||||
| Lean-level proof plus the TLA+ model gives two | ||||||||||
| independent witnesses of the same property — the | ||||||||||
| portfolio approach Soraya owns per | ||||||||||
| `docs/research/proof-tool-coverage.md`. | ||||||||||
|
Comment on lines
+33
to
+34
|
||||||||||
| portfolio approach Soraya owns per | |
| `docs/research/proof-tool-coverage.md`. | |
| portfolio approach owned by the formal-verification lane | |
| per `docs/research/proof-tool-coverage.md`. |
Copilot
AI
Apr 20, 2026
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
P1: This section attributes actions/disclosures to the human maintainer by name (“Aaron”). Per the repo’s comms-hygiene guidance, please replace with role-based phrasing (“human maintainer”) in this doc.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
P1: This section uses direct contributor names (e.g., the human maintainer) in a doc. Per
docs/AGENT-BEST-PRACTICES.md“No name attribution in code, docs, or skills”, please switch to role-based references (e.g., “human maintainer”) and keep personal names out of this file.