docs(pm2): B-0271 — PM-2 first research pass, 6 Zeta feature gaps predicted #3033
There are no files selected for viewing
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
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,62 @@ | ||
| --- | ||
| id: B-0444 | ||
| priority: P1 | ||
| status: open | ||
| title: "Getting-started guide for Zeta library consumers — quickstart doc + sample project" | ||
| type: friction-reducer | ||
| origin: PM-2 gap-prediction pass (B-0271) 2026-05-13 | ||
| created: 2026-05-13 | ||
| last_updated: 2026-05-13 | ||
| depends_on: [] | ||
| composes_with: [B-0154, B-0445] | ||
| tags: [consumer-ux, getting-started, quickstart, documentation, onboarding, csharp, samples] | ||
| --- | ||
|
|
||
| # B-0444 — Getting-started guide for library consumers | ||
|
|
||
| ## PM-2 signal | ||
|
|
||
| External .NET developers who land on the repo from NuGet or GitHub | ||
| encounter Budiu et al. VLDB'23 math in the second paragraph of the README. | ||
| No `docs/getting-started.md` exists. No "hello world" circuit example | ||
| appears before the operator catalogue. | ||
|
|
||
| ## What | ||
|
|
||
| 1. `docs/getting-started.md` — 5-step quickstart: | ||
| install → create circuit → map → step/tick → inspect output. | ||
| Target audience: C# developer unfamiliar with DBSP. | ||
| 2. `samples/QuickStart/` — minimal standalone project (single `.csproj`) | ||
| that mirrors the quickstart doc and builds with `dotnet run`. | ||
| 3. README badge / top-10-lines link pointing to the guide. | ||
|
|
||
| ## Why now | ||
|
|
||
| The library is production-ready (0 warnings, 470+ tests, 25-round | ||
| stability window on residuated lattices + FastCDC). The entry path is | ||
| research-paper difficulty. Every consumer who bounces in the first 5 | ||
| minutes is a permanent loss. | ||
|
|
||
| ## Non-goals | ||
|
|
||
| - Does not replace the operator catalogue. | ||
| - Does not add new operators. | ||
| - Does not touch the F# API surface. | ||
|
|
||
| ## Acceptance criteria | ||
|
|
||
| - [ ] `docs/getting-started.md` exists with a working 5-step C# example. | ||
| - [ ] `samples/QuickStart/` builds and runs: `dotnet run --project samples/QuickStart`. | ||
| - [ ] README links to the guide within the first 10 lines. | ||
| - [ ] `dotnet build -c Release` 0 warnings after changes. | ||
|
|
||
| ## Kill criteria | ||
|
|
||
| If the Aurora pitch / factory-demo consumer path (B-0437 or equivalent) | ||
| already produces a canonical "hello world" moment, subsume this row under | ||
| that and close here. | ||
|
|
||
| ## Composes with | ||
|
|
||
| - B-0154 (GitHub Pages SEO — the guide should be discoverable via Pages) | ||
| - B-0445 (C# fluent operator surface — quickstart uses the fluent API when it ships) | ||
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,65 @@ | ||
| --- | ||
| id: B-0445 | ||
| priority: P1 | ||
| status: open | ||
| title: "C# fluent operator surface — Map, Filter, Join, Distinct, Window via idiomatic CSharp API" | ||
| type: feature | ||
| origin: PM-2 gap-prediction pass (B-0271) 2026-05-13 | ||
| created: 2026-05-13 | ||
| last_updated: 2026-05-13 | ||
| depends_on: [] | ||
| composes_with: [B-0444] | ||
| tags: [csharp, api-surface, fluent, operator, consumer-ux, dotnet] | ||
| --- | ||
|
|
||
| # B-0445 — C# fluent operator surface | ||
|
|
||
| ## PM-2 signal | ||
|
|
||
| The README states "a surface that feels native to both F# and C#." | ||
| Current state: `src/Core.CSharp/` contains exactly one file (`Variance.cs`) | ||
| — declaration-site variance shims. All operators (`Map`, `Filter`, `Join`, | ||
| `Distinct`, `GroupBy`, `Window`) require F# discriminated-union idioms. | ||
| The C# sample in `samples/FactoryDemo.Api.CSharp/` calls the F# surface directly. | ||
|
|
||
| ## What | ||
|
|
||
| 1. `ZetaCircuitBuilder<T>` — C# fluent class wrapping `Circuit` and `Op<'T>` | ||
| so consumers can write: | ||
| ```csharp | ||
| var result = circuit | ||
| .From(source) | ||
| .Map(x => x.Name) | ||
| .Filter(name => name.Length > 0) | ||
| .Distinct(); | ||
| ``` | ||
| 2. Extension methods on `Op<ZSet<K>>` for common operators. | ||
| 3. XML doc comments on all new public C# symbols (IntelliSense parity). | ||
| 4. Rewrite `samples/FactoryDemo.Api.CSharp/` to use the new fluent API. | ||
|
|
||
| ## Why now | ||
|
|
||
| The existing CSharp sample builds but uses raw F# discriminated unions, | ||
| which is non-idiomatic C#. The fluent API is the minimum viable C# surface | ||
| that makes the "native to both F# and C#" README claim true. | ||
|
|
||
| ## Non-goals | ||
|
|
||
| - Does not change operator semantics. | ||
| - Does not rewrite the F# core. | ||
| - Does not need to cover every operator — the six core ones suffice for v1. | ||
|
|
||
| ## Acceptance criteria | ||
|
|
||
| - [ ] `src/Core.CSharp/` contains fluent builder covering: Map, Filter, Join, | ||
| GroupBy, Distinct, Window (sliding). | ||
| - [ ] `samples/FactoryDemo.Api.CSharp/` rewrites its circuit construction | ||
| to use the new fluent API, not raw F# types. | ||
| - [ ] All public C# types have `<summary>` XML docs. | ||
| - [ ] `dotnet build -c Release` 0 warnings. | ||
| - [ ] New `tests/Core.CSharp.Tests/` tests cover the fluent API round-trips. | ||
|
|
||
| ## Kill criteria | ||
|
|
||
| If Aurora / enterprise pitch explicitly targets F# only (no C# consumer), | ||
| defer to P2. |
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,63 @@ | ||
| --- | ||
| id: B-0446 | ||
| priority: P2 | ||
| status: open | ||
| title: "Lean 4 formal proof completion — DBSP chain rule + core stream-calculus identities" | ||
| type: feature | ||
| origin: PM-2 gap-prediction pass (B-0271) 2026-05-13 | ||
| created: 2026-05-13 | ||
| last_updated: 2026-05-13 | ||
| depends_on: [] | ||
| composes_with: [] | ||
| tags: [lean4, formal-verification, proof, dbsp, chain-rule, identities, correctness] | ||
| --- | ||
|
|
||
| # B-0446 — Lean 4 formal proof completion for DBSP core identities | ||
|
|
||
| ## PM-2 signal | ||
|
|
||
| Academic reviewers and enterprise adopters want to cite Zeta as a | ||
| verified DBSP implementation. `proofs/lean/ChainRule.lean` is a stub | ||
|
There was a problem hiding this comment.
This row’s signal is built on an invalid file location: Useful? React with 👍 / 👎. |
||
| (no proof body). The four core identities are tested as F# property | ||
| tests but carry no formal proof certificate. TECH-RADAR has Lean 4 | ||
| on "Assess" since Round 10 with no promotion. | ||
|
|
||
| ## What | ||
|
|
||
| 1. Complete `proofs/lean/ChainRule.lean`: | ||
| - `D ∘ I = id` (differentiation cancels integration) | ||
| - `I ∘ D = id` (integration cancels differentiation) | ||
| These are the bijection identities; they establish Z-sets form a | ||
| group under the stream calculus. | ||
| 2. Add `proofs/lean/LinearityRule.lean`: | ||
| - For linear Q: `Q^Δ = Q` (trivial incrementalization). | ||
| 3. Wire `lake build` in `proofs/lean/` as a CI check (new GitHub | ||
| Actions step, not blocking the main .NET build gate). | ||
| 4. Promote TECH-RADAR Lean 4 from Assess → Trial. | ||
| 5. README "formally verified" badge after CI check is green. | ||
|
|
||
| ## Why now | ||
|
|
||
| TECH-RADAR Lean 4 has been on "Assess" since Round 10 with no action. | ||
| The stub proof `ChainRule.lean` is a lying stub — it exists but proves | ||
| nothing. A complete proof of two identities is the minimum step to a | ||
| verified claim, independent of the heavier F* extraction track. | ||
|
|
||
| ## Non-goals | ||
|
|
||
| - Does not prove every operator. | ||
| - Does not require a full Mathlib port. | ||
| - Does not block the F* extraction path (TECH-RADAR "Assess" — runs | ||
| in parallel). | ||
|
|
||
| ## Acceptance criteria | ||
|
|
||
| - [ ] `proofs/lean/ChainRule.lean` contains a complete proof with no `sorry`. | ||
| - [ ] `proofs/lean/LinearityRule.lean` exists with a complete proof. | ||
| - [ ] CI runs `lake build` in `proofs/lean/` and the step is green. | ||
| - [ ] TECH-RADAR Lean 4 row updated: Assess → Trial. | ||
|
|
||
| ## Kill criteria | ||
|
|
||
| If the F* extraction path (TECH-RADAR entry) ships first and covers the | ||
| same identities, subsume this row under that PR and close here. | ||
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,72 @@ | ||
| --- | ||
| id: B-0447 | ||
| priority: P2 | ||
| status: open | ||
| title: "NuGet package metadata completeness — description, tags, SourceLink, semantic versioning" | ||
| type: friction-reducer | ||
| origin: PM-2 gap-prediction pass (B-0271) 2026-05-13 | ||
| created: 2026-05-13 | ||
| last_updated: 2026-05-13 | ||
| depends_on: [] | ||
| composes_with: [B-0154] | ||
| tags: [nuget, package-metadata, discoverability, sourcelink, versioning, dotnet] | ||
| --- | ||
|
|
||
| # B-0447 — NuGet package metadata completeness | ||
|
|
||
| ## PM-2 signal | ||
|
|
||
| `Directory.Build.props` has `<Authors>zeta contributors</Authors>` but | ||
| no `PackageDescription`, `PackageTags`, `RepositoryUrl`, | ||
| `PackageLicenseExpression`, or `PackageVersion`. `dotnet pack` currently | ||
| produces a `.nupkg` with a blank description, no tags, and version `1.0.0` | ||
| baked in. A developer searching NuGet for "incremental streaming F#" | ||
| would not find Zeta. | ||
|
|
||
| ## What | ||
|
|
||
| Add to `Directory.Build.props`: | ||
|
|
||
| ```xml | ||
| <PackageDescription> | ||
| Zeta — retraction-native incremental view maintenance for .NET. | ||
| An F# implementation of the DBSP algebra (Budiu et al., VLDB'23). | ||
| Streaming, reproducible, near-zero-allocation. | ||
| </PackageDescription> | ||
| <PackageTags>dbsp;incremental;streaming;retraction;fsharp;dotnet;ivm</PackageTags> | ||
| <RepositoryUrl>https://github.com/Lucent-Financial-Group/Zeta</RepositoryUrl> | ||
| <PackageProjectUrl>https://github.com/Lucent-Financial-Group/Zeta</PackageProjectUrl> | ||
| <PackageLicenseExpression>Apache-2.0</PackageLicenseExpression> | ||
| ``` | ||
|
|
||
| Semantic versioning: drive `Version` from a `VERSION` file checked into | ||
| git root (e.g., `1.0.0-alpha.1`) so every `dotnet pack` produces a | ||
| deterministic version tied to source. | ||
|
|
||
| SourceLink: add `Microsoft.SourceLink.GitHub` to `Directory.Packages.props` | ||
| and `<PublishRepositoryUrl>true</PublishRepositoryUrl>` in `Directory.Build.props` | ||
| so debugger source-navigation works for downstream consumers. | ||
|
|
||
| ## Why now | ||
|
|
||
| The Aurora pitch (PR #2924) and B-0154 (GitHub Pages SEO) are preparing | ||
| the external-consumption story. A NuGet package with no description and | ||
| a static version looks abandoned and is invisible to search. | ||
|
|
||
| ## Non-goals | ||
|
|
||
| - Does not require publishing to nuget.org yet. | ||
| - Does not change any F# or C# source code. | ||
|
|
||
| ## Acceptance criteria | ||
|
|
||
| - [ ] `dotnet pack` produces a `.nupkg` with Description, Tags, | ||
| RepositoryUrl, LicenseExpression populated. | ||
| - [ ] `Version` is driven from a `VERSION` file, not hard-coded. | ||
| - [ ] `dotnet pack --include-symbols` produces a `.snupkg` with SourceLink. | ||
| - [ ] `dotnet build -c Release` 0 warnings after the change. | ||
|
|
||
| ## Kill criteria | ||
|
|
||
| If NuGet publishing is explicitly WONT-DO before the Aurora pitch closes, | ||
| defer to P3 and note that decision in this row. |
Oops, something went wrong.
Oops, something went wrong.
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.
Uh oh!
There was an error while loading. Please reload this page.