Skip to content

backlog.md

Latest commit

 

History

History
317 lines (250 loc) · 15.5 KB

backlog.md

File metadata and controls

317 lines (250 loc) · 15.5 KB
Raw

ProvableWorldModel: Pivot Backlog

Implementation backlog and status ledger for the CommitLLM × LeWorldModel pivot. Companion to roadmap.md (plan) and specs.md (spec). Milestones M0-M7 have landed in the current tree; M8 records follow-up modes and post-V0 scope.

Conventions. Each issue: ID - Title · area label · size (S ≤ 0.5d, M ≈ 1–2d, L ≈ 3–5d) · deps: blocking issues. Area labels reuse the existing scheme: area:core, area:export, area:prover, area:verifier, area:testing, area:ci, area:docs, area:security, area:planner. Acceptance criteria are the merge gate. Keep files small and focused (no thousand‑line modules).

Legend for status of pre‑pivot work: [reuse] keep as‑is · [adapt] modify · [remove] delete · [new] create.

Milestone M0: Repository reset & scaffold

Initial goal: a clean, building, stable‑toolchain 5‑crate workspace with the STARK backend removed and the new corpus in place. No proofs yet.

  • P-001 - Branch & archive legacy STARK corpus · area:docs · S

    • git mv STARK‑specific RFCs (range‑check, tensor‑memory AIR, linear/matmul AIR, nonlinear AIR, predictor AIR, rollout AIR, planner AIR, CEM AIR, encoder AIR, recursion, vendoring) and the AIR sections of the spec docs to docs/legacy-stark/. Add a docs/legacy-stark/README.md explaining they are superseded by specs.md.
    • AC: nothing deleted (moved only); docs/legacy-stark/ builds in link‑check; top‑level docs reference the new corpus.
    • deps: none

  • P-002 - Remove AIR & circuits crates · area:core · S · [remove]

    • Delete crates/pwm-air, crates/pwm-circuits; drop from Cargo.toml members and [workspace.dependencies].
    • AC: workspace resolves without them; no first‑party crate references them.
    • deps: P-004

  • P-003 - Remove vendored Stwo & stwo‑circuits · area:core · S · [remove]

    • Delete third_party/stwo, third_party/stwo-circuits; remove stwo from [workspace.dependencies]; update third_party/INVENTORY.md/README.md.
    • AC: no stwo/stwo-circuits path or dep anywhere; cargo metadata clean.
    • deps: P-004, P-005

  • P-004 - Switch to stable toolchain · area:ci · S · [adapt]

    • Replace rust-toolchain.toml nightly pin with a stable channel pin; bump workspace.package.rust-version MSRV; remove nightly‑only flags.
    • AC: cargo +stable build succeeds for all remaining crates.
    • deps: P-002, P-003

  • P-005 - De‑Stwo pwm-core::field · area:core · M · [adapt]

    • Replace the M31/QM31 re‑export from Stwo with a native M31 implementation (centered encoding helpers unchanged) so pwm-core has zero proving deps. Add the audit field Fp61 (p = 2⁶¹−1, Mersenne) used by Freivalds.
    • AC: pwm-core cargo tree shows no stwo; no_std build passes; existing field/fixed_point tests pass against native M31.
    • deps: none

  • P-006 - Update workspace manifest & lints · area:ci · S · [adapt]

    • members = 5 crates; remove vendored exclude; keep lints/profiles; blake2 stays.
    • AC: cargo build/clippy/fmt green on the 5‑crate workspace.
    • deps: P-002, P-003

  • P-007 - Rewrite README & SPEC pointers · area:docs · S · [adapt]

    • Point README/SPEC to roadmap/specs/backlog; update the crate table and the "what it is" section to commit‑and‑audit.
    • AC: links resolve; no STARK/Stwo claims remain in top‑level docs.
    • deps: P-001

  • P-008 - Prune CI of AIR/Stwo gates · area:ci · S · [adapt]

    • Remove AIR/LogUp/Stwo‑specific CI steps; keep SPDX, changelog, links, fmt, clippy, deny. Add the new gates that M7 later fills in.
    • AC: CI passes on the scaffold.
    • deps: P-004, P-006

Milestone M1: Core crypto & data model

Goal: the shared, no_std, float‑free primitives the prover and verifier both use.

  • C-101 - pwm-core::freivalds · area:core · M · [new]

    • precompute_v(r: &[Fp61], weight: &[i8], rows, cols) -> Vec<Fp61> and check(v, x, r, z) -> bool over Fp61; int8/int16 x, i32 z. Port from CommitLLM verilm-core::freivalds into our types. no_std.
    • AC: unit tests (identity, negative weights, wrong‑z reject) pass; property test: random W,x → check true iff z == Wx.
    • deps: P-005

  • C-102 - Freivalds challenge derivation · area:core · S · [new]

    • Derive r vectors (one per weight tensor_id) from the Fiat‑Shamir transcript after trace_root; deterministic, documented channel order.
    • AC: prover and verifier derive identical r; reorder → different r.
    • deps: C-101, [reuse] transcript

  • C-103 - pwm-core::trace data model · area:core · M · [new]

    • The OpRecord enum and tensor/accumulator reference types (§5), canonical encodings via CanonicalEncode. Pure data, no_std. Keep per‑variant structs in small submodules.
    • AC: round‑trip canonical bytes; golden encoding vectors stable.
    • deps: [reuse] serialize, tensor

  • C-104 - Trace Merkle commitment · area:core · S · [adapt]

    • trace_root over trace leaves reusing commit.rs Merkle (selective‑open friendly leaf layout). Merkle inclusion proof + verify.
    • AC: root stable; valid proof verifies; tampered leaf/proof rejected.
    • deps: C-103, [reuse] commit

  • C-105 - Extend commitments for the new artifact · area:core · S · [adapt]

    • Add trace_root to the binding/commitment set; keep ModelBinding/ QuantBinding/PlannerBinding as‑is.
    • AC: mutating any bound field changes the digest; commitment tests pass.
    • deps: C-104

  • C-106 - Limb accumulator review for Freivalds field · area:core · S · [adapt]

    • Ensure accumulator bounds and limb decomposition are consistent with Fp61 embedding (int32 accumulators fit; limb path documented).
    • AC: bound‑escape cases produce limb decomposition, not wraparound.
    • deps: P-005

Milestone M2: Export pipeline & data adapter

Goal: le‑wm checkpoint → committed quantized manifest + golden vectors; data tuples.

  • E-201 - le‑wm checkpoint ingest · area:export · M · [new]

    • Python: load JEPA object / weights.pt+config.json; extract the V0 subgraph (action_encoder, predictor ×6 blocks, pred_proj); record shapes/dims.
    • AC: ingest the reference checkpoint; assert dims (192/3/6/16/64/2048).
    • deps: P-004

  • E-202 - Quantization pass · area:export · L · [adapt]

    • int8 weights, int8/int16 activations (per‑tensor), int32 accumulators/biases, pow‑2 scales; per spec §3. Emit per‑op scale ids.
    • AC: quantized graph; MAC bounds respected; scales recorded.
    • deps: E-201

  • E-203 - BatchNorm folding · area:export · M · [new]

    • Fold pred_proj (and projector, deferred) BatchNorm1d frozen stats into the preceding Linear; record provenance.
    • AC: folded affine ≡ Linear∘BN on golden inputs (within quant); fold is byte‑deterministic.
    • deps: E-202

  • E-204 - Nonlinear lookup‑table generation · area:export · M · [new]

    • Emit committed integer tables: gelu_table_v1, silu_table_v1, softmax_table_v1 (exp), invsqrt_table_v1; bind under quantization_commitment.
    • AC: tables committed; table reads reproduce the quantized nonlinearity.
    • deps: E-202

  • E-205 - Manifest writer & commitments · area:export · M · [adapt]

    • Write canonical manifest (ops[], scales, tables, BatchNorm provenance); compute model_commitment/quantization_commitment; byte‑identical re‑export.
    • AC: re‑export byte‑identical; commitments stable (SC3).
    • deps: E-203, E-204

  • E-206 - Rust integer reference inference · area:export · L · [new]

    • Rust path over the exported graph reproducing the quantized ops exactly (pwm-core::fixed_point), emitting all activations/accumulators.
    • AC: Rust ref ≡ golden bit‑for‑bit on the V0 subgraph.
    • deps: E-205, [reuse] fixed_point

  • E-207 - Python↔Rust parity gate · area:export/testing · M · [new]

    • Differential: Python quantized ref ≡ Rust ref ≡ golden across seeded inputs.
    • AC: parity gate green; any divergence fails CI (SC4).
    • deps: E-206

  • E-208 - stable‑worldmodel data adapter · area:export · M · [new]

    • Thin Python: load_dataset(num_steps=2) → (obs, action, next_obs); encode obs→latent offline; export (z_history, action, z_next), goal latent, and a fixed candidate action set for P2.
    • AC: produces committed input bundles consumable by the prover.
    • deps: E-201

Milestone M3: Trace builder & prover

  • PR-301 - Reference→trace builder · area:prover · L · [new]

    • Consume the Rust reference activations/accumulators → ordered OpRecord trace; assert graph fidelity vs manifest ops[].
    • AC: trace matches manifest op set/order; GraphMismatch on mismatch.
    • deps: E-206, C-103

  • PR-302 - Prover commit & transcript · area:prover · M · [new]

    • Merkle‑commit the trace; absorb the canonical transcript; squeeze r + audit selection (full set for V0).
    • AC: trace_root + r reproducible; transcript order documented.
    • deps: PR-301, C-102, C-104

  • PR-303 - AuditArtifact assembly & (de)serialize · area:prover/core · M · [new]

    • Build AuditArtifact { commitments, public_input, openings, claimed_outputs }; canonical binary (de)serialization.
    • AC: round‑trip stable; artifact self‑contained.
    • deps: PR-302, C-105

  • PR-304 - Prover CLI · area:prover · S · [adapt]

    • prove_step|prove_rollout|prove_planning entry points + CLI; load manifest + weights + inputs, emit artifact.
    • AC: CLI produces a P0 artifact end‑to‑end.
    • deps: PR-303

Milestone M4: Verifier & P0 (predictor step)

  • V-401 - Verifier shell (no_std) · area:verifier · M · [new]

    • verify(&AuditArtifact): parse, check relation_id, recompute public‑input digest, check commitments + trace_root Merkle proofs, replay transcript → r. no_std, float‑free.
    • AC: structural checks pass on a valid artifact; tamper → typed error.
    • deps: PR-303, C-102

  • V-402 - Freivalds matmul checks · area:verifier · M · [new]

    • For each Linear record: v = rᵀW from committed weights, check(v,x,r,z).
    • AC: valid matmuls pass; a single wrong accumulator → FreivaldsCheckFailed.
    • deps: V-401, C-101

  • V-403 - Exact replay: requant/elementwise/layernorm · area:verifier · M · [new]

    • Recompute Requant, Elementwise (add/modulate/gate), LayerNorm exactly; range‑check every value.
    • AC: valid ops pass; mutated remainder/modulation/inv‑std → typed error.
    • deps: V-401, [reuse] fixed_point

  • V-404 - Exact replay: attention + nonlinear tables · area:verifier · L · [new]

    • Recompute AttnScore/AttnApply integer dot products; verify Softmax, Activation (GELU/SiLU) table reads against committed tables.
    • AC: attention + activations verified exactly; off‑trace prob/activation rejected (no fake‑a hole; security test).
    • deps: V-402, V-403, E-204

  • V-405 - P0 end‑to‑end accept/reject · area:verifier/testing · M · [new]

    • Wire V-402..404 into the P0 relation; accepting + the predictor reject set from the spec.
    • AC: P0 proves+verifies; every P0 negative test rejects with the right code.
    • deps: V-404, PR-304

Milestone M5: Rollout (P1)

  • R-501 - Rollout trace + recurrence check · area:prover/verifier · M · [new]

    • Emit RolloutStep records (le‑wm windowing, history_size=3); verifier checks each step as a P0 step + windowing wiring.
    • AC: P1 horizon‑5 proves+verifies; mutated intermediate latent rejected.
    • deps: V-405

  • R-502 - Trajectory commitment · area:core/prover · S · [adapt]

    • Commit the rollout trajectory under claimed_output_commitment.
    • AC: trajectory bound; tamper rejected.
    • deps: R-501

Milestone M6: Fixed‑candidate planning (P2 = V0)

  • PL-601 - Multi‑candidate rollout · area:planner/prover · M · [new]

    • Roll out all S committed candidates (Freivalds v reused across candidates).
    • AC: all candidates traced; reuse factor measured.
    • deps: R-502

  • PL-602 - MSE cost check · area:planner/verifier · M · [new]

    • cost_s = Σ(z_final,s − goal)² exact/Freivalds; accumulator range‑checked.
    • AC: costs verified; mutated cost rejected.
    • deps: PL-601

  • PL-603 - Argmin + tie‑break check · area:planner/verifier · M · [new]

    • selected_cost ≤ cost_s ∀s via difference witnesses; smallest‑index tie‑break; all S present (no winner‑only proof).
    • AC: selection verified; lower unselected candidate / wrong index / bad tie‑break each rejected.
    • deps: PL-602

  • PL-604 - P2 end‑to‑end (V0 headline) · area:planner · M · [new]

    • prove_planning → verify Ok; full negative suite (SC1, SC2).
    • AC: V0 statement holds end‑to‑end; soundness suite green.
    • deps: PL-603

Milestone M7: Hardening, CI, docs

  • T-701 - Golden vector corpus · area:testing · M · per‑op + e2e goldens (SC4). deps: E-207
  • T-702 - Mutation tests (no dead checks) · area:testing · M · each verifier check load‑bearing. deps: PL-604
  • T-703 - Freivalds soundness/fuzz · area:security/testing · M · wrong‑z fuzz; N/p bound documented; transcript determinism. deps: V-402
  • T-704 - no_std + float‑free verifier gate · area:ci · S · CI builds verifier no_std, lints out float. deps: V-401
  • T-705 - Dependency‑DAG + deny + SPDX gates · area:ci · S · enforce verifier/export layering. deps: P-006
  • T-706 - Reproducibility gate · area:ci · S · same inputs → same artifact bytes. deps: PR-303
  • T-707 - Spec/threat‑model docs finalize · area:docs/security · M · binding checklist, honesty boundary, the "no attention hole" argument. deps: PL-604

Milestone M8: Post-V0 and follow-up ledger

  • D-801 - Audit subsampling (sub‑linear verify) · area:verifier · L · landed: verify_sampled checks a deterministic subset and reports coverage. deps: PL-604
  • D-802 - Interactive verifier‑secret r mode · area:security · M · landed: verifier-supplied Freivalds challenges are supported. deps: V-402
  • D-803 - CEM planner proof (P3) · area:planner · L · deferred: seeded sampling, clipping, top‑k, distribution updates. deps: PL-604
  • D-804 - Pixel encoder proof (P4) · area:export/verifier · XL · deferred: ViT‑Tiny/14 encode inside the proof. deps: PL-604
  • D-805 - Lean formalization · area:security · L · landed: Freivalds probability bound and argmin uniqueness are proved with no sorry. deps: V-402, PL-603
  • D-806 - Batched/efficient P2 · area:prover · L · landed: batched planning verification reuses per-weight Freivalds precomputes. deps: PL-604

Critical path

P-005 ─► C-101 ─► V-402 ─┐
P-004 ─► E-201 ─► E-206 ─► PR-301 ─► PR-302 ─► V-401 ─► V-405 ─► R-501 ─► PL-601 ─► PL-604 (V0)
                 E-205 ──┘                          C-104 ┘

M0 unblocked the stable-toolchain workspace and native field. The export reference (E-206) and the Freivalds core (C-101) were the two long poles into the first P0 proof (V-405); the remaining layers compose upward to the V0 headline (PL-604).