Li Master Implementation Plan (rev. 5)¶

For agentic workers: Execute phases in order. Python 3.14 typing parity is the typechecker north star — not a minimal v1 subset.

Human-only actions: If a task needs something you cannot do in code — create a GitHub repo, org/app settings (Renovate, branch protection, secrets), OAuth/PAT, DNS, billing, or clicking UI in github.com — stop and ask the human explicitly before proceeding. Do not assume gh login, org-wide access, or that settings already exist. List exact steps; wait for confirmation.

Repos: Before a new li-langverse/* repository, ask the human (see § Repository separation). Phases through 8d need only lic, lip, lit (already created).

Goal: Open-source language: (1) Lean provability (2) Nim syntax (3) LLVM speed — in that priority order.

Strict by default: Proof, security, and performance gates are always on at maximum; there is no optional provability (strict-by-default.md). Tracker items close implementation gaps — they do not add implicit opt-out.

Reliability target: Li is not a runtime-interpreted language. User logic is fully static: types, contracts, memory, parallelism, and (for release) bounds/shapes are resolved at lic build + Lean — not at process start with dynamic checks. Push failures left until runtime error rate for proved programs approaches zero (only the capped trusted IO / platform surface remains outside user proofs).

Honest status (docs): Provability gaps (today) — living register of what is not proved/wired yet (Lean gate, heuristic parallel policy, decorator parse-only, …). Update that file when closing a phase gate.

Architecture: C++ compiler → MIR → LLVM 22 (sole backend). Bootstrap to self-host later. No VM, no JIT for user code, no runtime decorator dispatch.

GitHub org (li-langverse) — three repos (locked):

This workspace is the compiler tree until fully migrated/pushed to lic. Replaces canonical li-langverse/li-language (archive or redirect when migration completes).

Design spec: docs/superpowers/specs/2026-05-14-li-language-design.md

Ecosystem (agents — read before cross-repo work): agent-coordination.md, engineering-standards.md, vision-and-roadmap.md.

Vision, roadmap, and agent discipline¶

Where to record vision¶

Agents must not treat package README as the only vision doc when the change affects multiple repos or pillars.

Non-negotiable engineering (all agents)¶

Strict-by-default: See strict-by-default.md. Agents must not treat proof, CVE suites, or benches as optional; explicit downgrades only.

Strict gates — no exceptions without human approval and a tracked PH-/issue:

1. Functionality — spec/REQ correct; tests green; no silent wrong behavior.
2. Security — engineering-standards § CVE; run_security / exploit harness / fuzz per repo; map to catalog.
3. Performance — measured; benchmark regressions investigated; no “fast” without data.

Agents have freedom on structure and naming; not on skipping these three.

Learn from other ecosystems (implementing Li features)¶

Before shipping ecosystem tooling (lip, lit, httpd, std split):

• Survey 2–4 mature systems (Cargo, nginx, npm, Envoy, …).
• Adopt algorithms and practices that fit Li: easy, AI-first, provable, blazingly fast.
• Document “Learned from” in the phase plan or ADR; do not port C/nginx verbatim.

Details: engineering-standards.md.

Repository separation — when to create repos¶

What lives where (locked)¶

Never create separate repos for: registry (stays in lip), or lit duplicated inside lip.

Sufficient today (phases 0–8d) — no new org repos¶

These three are enough until a row in Future org repos applies:

• lic — compiler + 8a, 8e-li, Pkg, phases 0–7, H prep in-tree
• lip — 8b–8d
• lit — 8e

8-repo exit gate: each repo pushed, origin set, CI green (or documented skip). Until then, note push pending in the tracker.

Future org repos — agent must remind human¶

Rule for agents — ask the human first: Any action that is not a local code/docs change in the workspace requires explicit human approval before the agent continues. Examples:

New org repo workflow (subset of above):

1. Check whether the repo already exists on GitHub.
2. If no, post “Action needed from you” with: repo name, purpose, phase ID, governance checklist.
3. Wait for confirmation before implementing or pushing.
4. Do not request “authorize all orgs” OAuth; human uses UI or fine-grained PAT scoped to li-langverse.

Stay in lic monorepo (packages/<name>/) when: experimental, single consumer, or blocked on 8a/8b — document promotion in CHANGELOG when splitting out.

Human checklist (after agent reminder): governance § Repo creation checklist; templates in scripts/templates/github-repo/.

Cross-repo dependency notifications (every official package)¶

When lic, lit, lip, or any li-std-* / li-* package releases, dependents must be notified so maintainers bump pins and CI. Required for every repo under li-langverse (and documented for third-party lip consumers in 8d).

Dependency layers (what can change):

GitHub setup (mandatory per repo — templates in Pkg / governance):

Phase 8-sync (ecosystem — after 8-repo, parallel with 8b):

Agent rule: When scaffolding or promoting an official package, enable notification templates and add the repo to lic li-downstream-repos.txt. Remind human if Renovate org app is not installed.

Human one-time (org): Install Renovate on li-langverse (scoped to org) or rely on repository_dispatch + manual bumps until Renovate lands.

Exit gate: Bump lic patch tag in a test repo → downstream receives dispatch/issue; Dependabot PR for an Action pin in lip.

Phase map (revised)¶

Old 2-week schedule is void. Type parity alone is ~6 months part-time.

Doc runs in parallel with compiler phases — not after “v1”. Every compiler PR that changes the proof surface must touch the gap register (see below).

Ecosystem — packages (lic, lip, lit, scaffold)¶

Three org repos + scaffold in lic. One li.toml schema (authoritative in lip plan § A3):

8-repo (lic + lip + lit on GitHub, push + CI)
  Pkg (scaffold in lic) ──► 8a (import/workspace in lic)
                                    ├──► 8e-li (coverage flag in lic)
                                    ├──► 8e (lit repo: lit CLI + 80% gate)
                                    └──► 8b (lip repo) ──► 8c ──► 8d
                              8-sync (notify on lic/lit/std releases) ──► all official repos

lip publish / registry install: lic build + lit test --coverage ≥ 80% + ed25519 (unsigned third-party rejected by default).

Policy: Do not advertise third-party lip install until 8a + 8c + 8e. Scaffold and path-only workspaces are fine earlier.

Docs: docs/ecosystem/* in lic; docs/lip.md + registry.md in lip; docs/lit.md in lit; threat model docs/verification/packages.md in lic.

Governance: 2026-05-16-li-ecosystem-governance.md — org li-langverse, compiler home lic (not li-language), SemVer/SPDX/Changelog, PKG/REQ traceability.

Also uses packages: li-httpd plan — li-new-package in lic; resolve with lip after 8b; promote to li-langverse/li-* per governance.

Compile-time reliability (no user runtime)¶

Li maximizes reliability by eliminating user-visible runtime failure modes wherever proofs allow.

Not in user code: Any, unsafe, sorry, runtime reflection on types, dynamic decorator registries, “try at runtime” bounds.

Minimal native layer (not “the language runtime”): li_rt.c + trusted.lean — bounded IO, debug hooks, OpenMP thread team. This is platform glue, not a place to hide user semantics. Release builds after successful lic build must not rely on catching user logic bugs via panic.

Debug-only (optional CI): TSan/fuzz find compiler bugs — not a user safety net.

Implication for 7d / 7e / 2i: decorators and math are static sugar only; performance and correctness are fixed at compile time.

The table above describes the target. Where lic has not established mathematical provability yet, see Provability gaps and compiler task → gap map below.

Phase 8p — Parallel compile & CI throughput¶

Problem: Full li-tests + scripts/local-ci.sh often take 5–15+ minutes on a devbox because almost every gate runs lic build sequentially, even when the machine has many idle cores. Only the C++ compiler build (./scripts/build.sh → Ninja -j) uses parallelism today.

Goal: Use all host cores for orchestration and compilation where proofs and determinism allow — so agents and humans do not wait “ages” on every green gate.

Not the same as runtime parallel for: Phase 8p speeds up building and verifying Li programs. User-code multi-core execution stays in phases 7 / 7d / 7e (--threads=N, OpenMP).

Layers (what can run in parallel)¶

Sub-phases & exit gates¶

Safety & determinism rules¶

1. Default parallelism = host cores; LI_TEST_JOBS=1 / LI_BUILD_JOBS=1 for bisect and golden logs.
2. No shared build/generated/AutoVC.lean across concurrent workers without isolation — race caused flaky Lean failures in parallel experiments.
3. Proof surface unchanged — parallel builds must not skip Lean or open-VC policy; only schedule work faster.
4. GHA quota: parallel local CI is the primary win when Actions minutes are exhausted; same gates, shorter wall clock.

Agent priority¶

Implement 8p-a before 8p-c (largest CI win for least compiler risk). Track in provability-gaps only if parallel scheduling changes what “green” means.

Learned from: Cargo build -j, Ninja, Bazel remote/local pools — adopt job pool + hermetic per-task target/, not distributed compilation in v1.

Deferred — GHCR release images (prebuilt lic)¶

Today: ghcr.io/li-langverse/lic-ci:* images are development/CI toolchain only (OS + LLVM 22 + cmake/ninja/python). They do not ship a built lic binary; ./scripts/local-ci.sh --docker mounts the repo and runs scripts/build.sh + ci.sh so the compiler always matches the branch under test.

Later (after compiler stabilizes): publish release container tags that include a pinned lic release (and optionally lit/lip smoke tools) for consumers who should not compile from source. Not started while lic still changes frequently (httpd, contracts, LLVM pins, manifest gates).

See local-ci-docker-images.md.

Documentation & provability honesty (cross-cutting)¶

Problem: Handbook and specs must not read as if Lean, full disjoint proofs, decorators, or math lowering already ship when they do not. Contributors need a single gap register and compiler-task linkage.

Canonical register: docs/verification/provability-gaps.md (G-* IDs).

Phase Doc — sub-phases¶

Doc is “done” for a release tag only when: open G-* rows match reality and handbook does not overclaim.

PR rule (binding for compiler work)¶

When a PR implements or partially implements a proof-related compiler feature:

1. Update provability-gaps.md — move G- row to Partial or Done* with one-line evidence (file, test suite, CLI flag).
2. Update affected handbook pages listed in the gap doc § Documentation that must stay aligned.
3. If the feature is still Partial, add an admonition on the handbook page (mkdocs !!! note "Provability status").
4. Mention G-* ID in the PR description.

Compiler tasks vs proof gaps¶

Maps master plan phases to gap IDs and what “mathematical provability established” means for lic (not aspirational spec text).

Not proof (document as limits): G-wrong-spec, G-hw, G-meta — stay in why-provable.

Documentation gaps to close (checklist)¶

Track in phase Doc until each is checked:

• Doc-a — gap register complete and linked site-wide (mkdocs nav; README audit ongoing)
• Doc-b — linear-algebra.md stub + decorators.md; fast-math guide audit partial
• Doc-b — language design spec banner: “implementation status → provability-gaps”
• Doc-c — phase plan files (02, 03, 07) link G-* in exit gates
• Doc-d — .cursor/skills/build-li-master-plan/SKILL.md includes gap-register update step
• Doc-e — check-doc-provability-claims.sh in scripts/ci.sh

Stack decision record¶

Sub-plan index¶

2g / 2h / 2i: After 2d, run 2g + 2h in parallel; then 2i (linalg surface). User-facing functions are def only; numerics read like math (C += A @ B, y[i] = alpha * x[i] + y[i]), not simd(...). Finish 2g–2i before widening 2e method VCs. simd[T,N] / __li_simd_* only in compiler appendix.

7 / 7d / 7e: Complete 7a–7c (SIMD MIR, parallel for, benchmarks) first. 7d = decorators (@parallel, @vectorized, @cpu, …). 7e = lower math expressions to that MIR (users never write simd(...) in docs/benches). Depends on 2i + 7b. Cross-lang perf: benchmarks plan Tier 1 (simd_dot, matmul_*), policy ≤1.2× C++. Specs: docs/superpowers/specs/2026-05-16-li-execution-decorators.md, docs/superpowers/specs/2026-05-16-li-math-linalg-surface.md.

Phase completion tracker¶

• Phase 0 — C++ / LLVM bootstrap
• Phase 1 — Lexer + Parser
• Phase 2a — Type core (typecheck + prove_reject + race policy gates; full mypy parity pending)
• Phase 2b — Generics + Protocol (PEP 695 params, TypeApp, Callable, Sized protocol)
• Phase 2c — Collections + TypedDict (list/dict/tuple, named tuple, enum)
• Phase 2d — Borrow + effects (lexical borrowck, raises IO/Alloc)
• Phase 2g — def, object + field private/public, minimal import (encapsulation suite green; import parse-only; not full OOP)
• Phase 2j — Full OOP surface — 2j-a…f done (#83+); Lean method/trait ensures sugar still G-oop open — OOP roadmap
• Phase 2h — Python-math operators %, //, ** (math_syntax suite); for i in start..<end (for_range_sum.li); Python range() deferred (G-math-syn)
• Phase 2i — Math / linalg surface — partial: 2i-a/c (#148); 2i-b norm, sum/dot, reductions/, same-length **, prelude axpy, scalar×array; length-1 broadcast (array[1]→array[N] element-wise); full NumPy rank broadcast still open; float @ Props closed (mat2_at2_eval)
• Phase 3 — MIR + LLVM codegen (lic build, minimal lower/emit; CFG/bounds IR deferred)
• Phase 4 — Runtime + stdlib
• Phase 4s — Stdlib seal (prelude/std/ names cannot be shadowed; stdlib_seal/ CI)
• Phase 5 — Tetris
• Phase 5b — Benchmarks & simulations (harness + X plots skeleton on dev)
• Phase 6 — Self-host (bootstrap seed: bootstrap/lic/main.li → build/lic-from-li)
• Phase 2e — Contracts + refinements — merged (PR #83): call-site requires (E0304), refinement types (E0305), if-guard VC discharge, import/extern; corpus proof-corpus-roadmap.md; float/nontrivial ensures still open
• Phase 2f — Lean 4 verify — partial (#83, #151, #155): default lake build AutoVC on lic build; P-linalg closed corpus + loop dot (dot4_int_loop_eval_spec); fib/recursive call-site + decreases/_par* VCs typecheck; intentional open: sqrt_open_bound; G-lean / G-vc still open — still open gaps
• Phase 7 — Native HPC — v1 gate: simd + parallel for + OpenMP + check-master-plan-gates.sh (tier 1/2 perf advisory)
• Phase 7d — Execution decorators — partial (#150 7d-c): @vectorized on for → ArraySimdScope; 7d-b lanes=4; def @parallel(disjoint=) inherits to nested parallel for (policy); open: full MIR proc tags, Lean G-par proofs
• Phase 7e — Math → SIMD/parallel lowering — partial (#148, #150, #155): loop matmul + FMA horner; tier-1 advisory ≤1.2× (matmul_naive, horner_pure_li); check-tier1-li-vs-cpp.sh strict optional; open: remaining tier-1 slices, full float Lean Props
• Phase H — li-httpd infra — lis harness, mitigations, CI, workspace stubs (implementation-status)
• Phase H — li-httpd M1 .li — partial: TOML match_route, validate/explain/flatten-config, overlap reject, Bearer auth (C), packages/li-log (#158); next: Li net.httpd lib build + M1 ship gate Lean (httpd-prerequisites)
• Phase Pkg — Package scaffold + governance stubs (scaffold, governance; li.toml = lip § A3)
• Phase 8-repo — lic, lip, lit on GitHub + CI
• Phase 8a — Modules + workspace lic build — std.* + workspace/local imports; li-tests/modules/; lic-workspace-build.sh on 3 packages
• Phase 8e-li — lic build --coverage-instrument (LLVM profile flags)
• Phase 8e — lit CLI + ≥80% publish gate — lit repo: scripts/lit, coverage gate; lic: check-stdlib-coverage.sh instrumented import harness (stdlib_coverage/); llvm-cov 100% on std/** in lit repo
• Phase 8b — lip path/git + li.lock — lip repo: path deps, install/build/lock, integration fixtures
• Phase 8c — ed25519 + proof_digest in lock — v1: lock fields + optional publisher.key signing
• Phase 8d — Registry + lip publish — v1: local registry/index.json + publish gate (lit + lic)
• Phase 8-sync — cross-repo workflows; optional PAT scope fix for repository_dispatch
• Phase 8p — Parallel compile + CI throughput — partial (8p-a/b/c/d): 8p-a parallel run_all + isolated LI_BUILD_DIR (#186, #200); 8p-c/d ResourceOptions + lic build --jobs reserved pass + CI test-job smokes (compiler/common/, scripts/ci.sh); open: 8p-b workspace pool, wall-time SLO (§ 8p)
• Phase Doc-a — Gap register current + site links (provability-gaps)
• Phase Doc-b — Handbook stubs (decorators, linear-algebra); audit partial
• Phase Doc-c — Phase 02 plan links G-* IDs (expand to 03/07 as those land)
• Phase Doc-d — Contributing / build skill requires gap-register updates
• Phase Doc-e — scripts/check-doc-provability-claims.sh in scripts/ci.sh (expand patterns over time)
• Vision-LLM — LLM-first + agent JSON diagnostics — partial: lic check --format=json, lic diagnose, diagnostic-v1 schema, handover docs, manifest stub (llm-first spec, agent-handover)

Dashboards (Cursor): canvases/li-master-plan-progress.canvas.tsx — phase tracker; canvases/li-fuzz-security-dashboard.canvas.tsx — updated by scripts/export-fuzz-status.sh after nightly fuzz.

Maintenance: When ecosystem or org layout changes (lic / lip / lit repos, phase gates, policies, future-repo table), update this file, 2026-05-16-li-package-manager-lip.md, and 2026-05-16-li-ecosystem-governance.md in the same PR. Agents: add a row to Future org repos when a plan introduces a new li-langverse/* home.

Maintenance (proof surface): When a compiler phase changes what lic build proves, update provability-gaps.md and the compiler task → gap map in the same PR — see Doc phase rules above.

v1 compiler milestone (honest scope)¶

Lic monorepo v1 — gate complete (scripts/check-master-plan-gates.sh)¶

Runnable on dev after ./scripts/build.sh:

• Phases 0–6, 2g, 2h, 7 (core), Pkg, Doc, 8-sync, 8e-li
• 180 li-tests manifest entries (run_all.sh --ci after gap-closure)
• 2e/2f partial: build/generated/AutoVC.lean every lic build; P-linalg closed VCs (#151)
• 7e partial: 1d/2d float @, element-wise SIMD, pure-Li tier-1 simd_dot / matmul_* (#148)
• 7d partial: @vectorized(lanes=4) + scoped for (#150); structured disjoint= still open

Full master plan — not complete (v2 backlog)¶

Open G-* register: every row in provability-gaps.md — none Done; Partial is the best current status.

“Master plan done” per original spec = all tracker rows plus proved lic build plus shipped lip/lit/httpd — not claimed. Use Lic monorepo v1 for what ships from this repository today.