diff --git a/docs/design-pure-bootstrap-zero.md b/docs/design-pure-bootstrap-zero.md index 58b93a5dfe2..dcac7dec223 100644 --- a/docs/design-pure-bootstrap-zero.md +++ b/docs/design-pure-bootstrap-zero.md @@ -4,6 +4,8 @@ > **v4 supersession (2026-05-15).** The 0-floor target articulated in this doc now applies to **v4** ([`src/v4/`](../src/v4/)) as the operational instantiation. v2 binary serves as v4's stage minus one (per [`src/v4/STRUCTURE.md`](../src/v4/STRUCTURE.md) "Bootstrap chain"); v4's compiler emits its own Rust trampoline (`bin/main.dag`) to satisfy 0-floor without needing the runtime-resolution choices (shipped binary / runtime crate / rustc-macro) described below. v3 references throughout this doc describe the v2β†’v3 transition that v4 supersedes; v3 is frozen pending v4 ship. +**v4 workflow authorities (registry).** Load-bearing workflow models: [`src/v4/workflow/bootstrap.dag`](../src/v4/workflow/bootstrap.dag) (bootstrap orchestration as data) and [`src/v4/workflow/ci.dag`](../src/v4/workflow/ci.dag) (CI pipeline as data). This doc governs their Pure Bootstrap / N=0 discipline (A3, PROOF-1, and the STOP rail: only bootstrap-modeled authority in those surfaces). **C4** (committed `ci.yml` as checked projection from `.dag`) is ratified in [`src/v4/STRUCTURE.md`](../src/v4/STRUCTURE.md). + **Promotion evidence chain (cited in cascade promotion PR body):** - D1 audit: PRs #769 + #771 + #775 + #777 + #779 (audit doc with substrate-generation already proven; 23 generated files + 24 REGEN_OUTPUTS entries; 38-type substrate.dag coverage survey) - D2 PB-1 brief amendment: PR #770 (non-goals revised under 0-floor) diff --git a/src/v3/SELF_HOSTING.md b/src/v3/SELF_HOSTING.md index d9cfbb7edf9..be3a7274004 100644 --- a/src/v3/SELF_HOSTING.md +++ b/src/v3/SELF_HOSTING.md @@ -25,6 +25,8 @@ off the ground. **Historical note.** The legacy self-hosted compiler tree (retired under T-V2-Retirement) established the same pattern v3 follows: `.dag` pipeline plus a small Rust bootstrap. v3 proceeds under PB-Runtime / Pure-Bootstrap-Zero. +**v4 operational workflow authorities.** Load-bearing v4 models live at `src/v4/workflow/bootstrap.dag` and `src/v4/workflow/ci.dag`; their governing program + rails (Pure Bootstrap / N=0, **C4**) are named in `docs/design-pure-bootstrap-zero.md` and `src/v4/STRUCTURE.md` β€” top-down registry, not duplicated as upward pointers in those `.dag` headers (`docs/modeling-discipline.md`). + **What changes with self-hosting:** - **The compiler becomes a substrate fact.** The pipeline stages diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index d498f7ed128..28be361f516 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -1443,3 +1443,61 @@ git show 92cb26402eeb21471acb6ac47559cbae3b52afdb:src/v4/std/float.dag Merge-base `92cb26402` **may** mark a sum coproduct **πŸ”΄** in the Practice-4 header (stop-signal / fail-closed disposition). Live substrate one-liners use **`// πŸ”΄ coproduct dissolution β€” DECISIONS.md Part 6 Β· CP-3229-RED-PRACTICE4.`** β€” **not** `CP-3229-GREEN-TERMINAL` (that slug is **🟒 GREEN** bulk recovery only). Verbatim πŸ”΄ five-pattern ledgers recover from the merge-base object the same way as 🟒 carriers; this row exists so the tag map never mislabels red as β€œgreen terminal.” **Recovery:** `git show 92cb26402eeb21471acb6ac47559cbae3b52afdb:`*path* on the five allowlisted `.dag` files; search `Coproduct dissolution` + `πŸ”΄` in the recovered `//` text. + + +## Part 7 β€” Practice-4 coproduct classification ledger (PR #3213, still-hawk-102 Option-1) + +> Worker-authored provisional, operator-ratified on audit (still-hawk-102 +> Option-1, 2026-05-17). Scope: coproducts introduced by **PR #3213** in +> non-allowlisted **workflow** files β€” distinct from **Part 6 / #3229**, +> which relocates Practice-4 receipts for the five strict-de-prose +> substrate files (`SL-3229-*` / `CP-3229-*`). The coproduct carries the +> one-line in-file tag `// 🟑 coproduct dissolution β€” DECISIONS.md +> LB-P4-3213` (modeling-discipline.md Practice 4 / Practice 9 general form). + +| ID | Coproduct / classification / dissolution-patterns-tried / trigger | Home | +|---|---|---| +| **LB-P4-3213** | `CiCommand` (`LintCommand \| TestCommand \| IgnoredTestCommand{test_name} \| BootstrapStageCompile{produces:Symbol} \| ShellCommand{command:String}`) β€” faithful PORT of v3 `dsl/gunbc/ci.dag` `CICommand` (still-hawk-102 fork-2 directive; not imported). **Single-authority (P2/Practice 5) β€” RESOLVED in-PR (openai-pro #3213 13971):** the bootstrap seed action is NOT restated in `ci.dag`; the `v2_compile_src_v4` job uses `BootstrapStageCompile{produces: v4_stage0_binary}`, a typed machine-readable reference imported from `v4.workflow.bootstrap` β€” `BootstrapPlan.seed` is the sole authority for the seed stage. **Structurally ENFORCED (P2/P3/Practice 5/6), not prose (openai-pro #3213 14006; operator BLOCKING inline #3213 ci.dag:168):** `ci_pipeline_well_formed` consumes the bootstrap authority `bootstrap_stage_output(plan: Outcome, s)` (owned by `v4.workflow.bootstrap`), which pattern-matches the canonical `bootstrap_plan` Outcome itself: fail-closed (`Rejected β‡’ false` β€” if the canonical bootstrap plan is Rejected, NO `BootstrapStageCompile` can satisfy the CI gate, so CI cannot be `Produced` while bootstrap is `Rejected`, INVARIANTS P3) and validates `produces` against the *validated plan's actual stage outputs* (`bp.seed/self0/self1.produces`), not a static symbol set β€” the validated `bootstrap_plan` is the sole authority (P2). Any out-of-plan or plan-Rejected payload routes to `ci_bootstrap_authority_violation`; a dangling payload cannot reach `Produced`. `BootstrapStageCompile` is 🟒 (a real cross-module authority edge, boundary-enforced, not deferred command-shape). The remaining 🟑 below is ONLY the `ShellCommand{String}` raw-argv command-shape decomposition, which is orthogonal and CORE-deferred to the consumer lane. **🟑 YELLOW (scaffold) β€” valid plan-bound, NOT "no change needed" (anti-#3250).** **Gate kind = `consumer:`** β€” the gate is the **first meaning-consumer** of the typed-command shape (deferred ci.yml projection / `select_jobs` / T-22 eval), which is **currently deferred-by-brief**, so the consumer-gate remains **CLOSED** and the #3244 gate-openβ†’πŸ”΄ chain does **not** fire here. **Landed migration target:** `extdeps/process.dag::Command{program,args,env}` is **LANDED (#3209)** β€” it is the typed-command *feature/target*, NOT the meaning-consumer; the future consumer consumes typed `Command` **directly**, so **no parallel carrier is needed** and `#3213` does **NO migration** and **NO local `CiCommand` parse**. **Dissolution plan (complete #3244 plan-binding):** named consumer (ci.yml projection / `select_jobs` / T-22 eval) + landed target (`process.dag::Command`, #3209) + owning deferred lane β€” when that consumer lane is built it consumes `Command`, and `ShellCommand{command:String}`'s `String` dissolves there into typed `program/args/env`; the consumer owes the decomposition, not a local parse. **5 dissolution patterns tried:** (1) fact-placement FAILS (uniform command consumer, not scattered); (2) variant-is-data FAILS (heterogeneous payloads β€” `test_name` vs raw `command`; collapsing loses structural-intent-vs-raw-shell, the carrier's point); (3) algebraic N/A (not an algebra carrier); (4) dimensional FAILS (exactly-one-intent, not orthogonal axes); (5) parameterized-family FAILS (not `F` over a declared set). Terminal-as-coproduct but 🟑 (not 🟒) because the consumer-gate is closed and the landed richer source (`process.dag::Command` #3209 / v3-F12) is the named decomposition target. | `src/v4/workflow/ci.dag` (`type CiCommand`) | + +### LB-P10-3213 β€” Practice-10 hand-rolled `List` operation dissolution ledger + +> Operator-flagged merge gate (still-hawk-102 via Lane B, 2026-05-18): +> per-file hand-rolled `List` ops with duplicate-across-files are a +> Practice-10 tell and must not merge as silent debt. Dispositions use +> the **#3244 unified Dissolution dispositions** vocabulary (πŸ”΄ +> dissolve-now / 🟒 terminal / 🟑 gated `feature:`). Procedure result: +> `std/collection.dag` (T-3; `git ls-tree` HEAD = 18 lines, only +> `List`/`Set`/`Map` type aliases) declares **zero** derived `List` +> operations β‡’ **zero πŸ”΄** (nothing to dissolve into in-PR); every +> generic primitive is **🟑 gated `feature:`**, owner **T-3 +> `std/collection.dag`** (the FreeMonoid-derived List-op surface; +> `fold`/`map`/`count`/`concat` are language substrate primitives, used +> directly β€” not hand-rolled, out of scope). In-file tag: +> `// 🟑 List-op dissolution (Practice 10) β€” DECISIONS.md LB-P10-3213`. + +| ID | Helper(s) β€” *duplicate-across-files = Practice-10 tell* | Disposition | Missing `std/collection.dag` op (gate kind `feature:`, owner T-3) Β· dissolve-on-arrival obligation | +|---|---|---|---| +| **LB-P10-3213-MEMBER** | `bs_member` (bootstrap.dag) βˆ₯ `ci_member` (ci.dag) β€” **duplicate** | 🟑 gated `feature:` | `member(x: T, xs: List) -> Bool` (membership/contains). On arrival: replace both call-sites with the std op; **delete both hand-rolled helpers**. | +| **LB-P10-3213-ANY** | `ci_symbol_resolves`, `ci_blocked` (ci.dag) | 🟑 gated `feature:` | `any(p: fn(T) -> Bool, xs: List) -> Bool` (existential). On arrival: re-express as `any(...)`; delete the helpers. | +| **LB-P10-3213-ALL** | `ci_all_job_ids_unique`, `ci_all_gate_ids_unique`, `ci_all_needs_resolve`, `ci_all_gate_jobs_resolve` (ci.dag) | 🟑 gated `feature:` | `all(p: fn(T) -> Bool, xs: List) -> Bool` (universal). On arrival: the four predicates become `all(...)` compositions; delete the bespoke folds. | +| **LB-P10-3213-COUNTIF** | `ci_id_occurrences` βˆ₯ `ci_gate_id_occurrences` (ci.dag) β€” **duplicate** | 🟑 gated `feature:` | `count_if(p: fn(T) -> Bool, xs: List) -> Int` (predicate count). On arrival: both occurrence-folds collapse to one `count_if`; delete both. | +| **LB-P10-3213-SETEQ** | `bs_list_eq` (bootstrap.dag) | 🟑 gated `feature:` | `set_eq(a: List, b: List) -> Bool` (membership-symmetric / multiset equality). On arrival: replace with std `set_eq`; delete helper. | +| **LB-P10-3213-FILTER** | `ci_eliminate_pass` (ci.dag) | 🟑 gated `feature:` | `filter(p: fn(T) -> Bool, xs: List) -> List`. On arrival: the keep-blocked pass becomes `filter(...)`; delete helper. | +| **LB-P10-3213-FIND** | `ci_job_needs` (ci.dag) | 🟑 gated `feature:` | `find`/lookup-first β€” honest shape `find(p: fn(T) -> Bool, xs: List) -> Witness` (per TASKS.md:235 `Map`/`PartialFunction` honesty; gated also on `witness.dag`/Wave-A2). On arrival: replace lookup-fold; delete helper. | +| **LB-P10-3213-KAHN** | `ci_kahn_fixpoint`, `ci_acyclic` (ci.dag) | 🟒 **terminal** | **Not** a reusable collection primitive: Kahn topological-elimination cycle-detection over the job graph β€” domain well-formedness model content, a *peer* of `ci_pipeline_well_formed` / `bootstrap_plan_well_formed` (which the gate does not ask to dissolve). Consumer-independent; no `std/collection.dag` op to dissolve into. (`fold`-as-bounded-counter is the P4 decidability idiom.) Its generic sub-primitives (`ci_member`/`ci_job_needs`/`ci_eliminate_pass`/`ci_blocked`) dissolve via the rows above; the Kahn *composition* stays. | + +**Note (out of dissolution scope, recorded for completeness):** `bs_diagnostic` / `ci_diagnostic` are `Diagnostic` constructors, not `List` operations. No πŸ”΄ in this ledger β€” `std/collection.dag` currently has no derived-op surface to dissolve into; the gate opens when T-3 `std/collection.dag` lands the List-op surface, at which point every 🟑 row above is a dissolve-on-arrival merge obligation. + +### LB-T22-3213 β€” bootstrap-stage rejection-family negative-coverage plan-bound 🟑 + +> CORE ruling (still-hawk-102, 2026-05-18, horn (i)): the +> `BootstrapStageCompile` single-authority seam is **ADDRESSED-BY-CONSTRUCTION** β€” +> `ci_pipeline_well_formed` is a pure structural predicate over the modeled +> `CiPipeline`; an out-of-set `BootstrapStageCompile.produces` cannot satisfy +> the gate (deterministically routes to `Rejected{ci_bootstrap_authority_violation}`, +> a modeled `Outcome` variant β€” no imperative side-channel / stringly exception). +> Verified in code by `bold-hawk-201` @ `6353d695e`. Horn (ii) β€” in-PR +> executable negative harness β€” REJECTED (T-22-in-#3213 = brief violation; +> hand-rolled harness = parallel test mechanism, anti-pattern). + +**🟑 plan-bound (NOT "no change needed" β€” anti-#3250).** The enforcement is structural and fail-closed *now*; what is deferred is the executable *demonstration*. **Arrival:** T-22's executable `TestClaim` runner lands (`compiler/05_eval.dag`; brief defers the executable TestClaim lane to the T-22 named trigger). **Follow-up (dissolves this 🟑):** add negative `TestClaim`(s) for the CI bootstrap-stage rejection family β€” dangling `BootstrapStageCompile.produces` + siblings (duplicate job/gate id, dangling `needs`, dangling gate job, dependency cycle) β€” exercising `ci_pipeline_well_formed`'s `Rejected` branches. **Bilateral binding:** the same obligation is recorded in `src/v4/TASKS.md` T-22 scope text (neither side is a vague "T-22 will cover"). In-file tag: `// 🟑 negative-coverage plan-bound (T-22) β€” DECISIONS.md LB-T22-3213`. | `src/v4/workflow/ci.dag` (`ci_pipeline_well_formed` rejection family) | diff --git a/src/v4/TASKS.md b/src/v4/TASKS.md index 399b7662400..1f3e1c7d067 100644 --- a/src/v4/TASKS.md +++ b/src/v4/TASKS.md @@ -859,6 +859,8 @@ All 5 artifacts share ONE Node tree (per gate #28 omni_layers_share_one_node_tre **Incremental Re-Test requirement set β€” held (IRT-3; see T-21 for the full IRT-1..4 set + rationale).** - **IRT-3 (with T-19).** `eval` MUST evaluate ANY node subgraph bound into a TestClaim's `input: Node` β€” including a `program ∘ generated-input` composite β€” at arbitrary-node granularity; it must never silently restrict TestClaim evaluation to whole-function / whole-module units. Node-level evaluability is what lets the affected set (T-21) name re-runs at node precision. +**Bilateral binding β€” #3213 negative-coverage obligation (DECISIONS.md LB-T22-3213).** ci.dag's `ci_pipeline_well_formed` enforces bootstrap-stage single-authority fail-closed by construction (`ci_all_commands_authority_ok` / `bootstrap_stage_output`), but the rejection family has no executable demonstration (the TestClaim runner is this task). **Arrival = T-22's executable `TestClaim` runner lands. Follow-up obligation:** add negative `TestClaim`(s) for the CI bootstrap-stage rejection family β€” dangling `BootstrapStageCompile.produces` + siblings (duplicate job/gate id, dangling `needs`, dangling gate job, dependency cycle) β€” landing them dissolves the `LB-T22-3213` 🟑. This binding is bilateral with DECISIONS.md `LB-T22-3213` (neither side is vague "T-22 will cover"). + **Scope**: XL (extra-large β€” THE primary execution path; bootstrap + tests + dry-run all depend on it) **Reference**: THESIS:225 + concept-unification THESIS:188 + STRUCTURE.md Β§"Bootstrap chain" (v2's eval seeds; v4's eval takes over) diff --git a/src/v4/workflow/bootstrap.dag b/src/v4/workflow/bootstrap.dag index f32f7a3a3b7..416105955d4 100644 --- a/src/v4/workflow/bootstrap.dag +++ b/src/v4/workflow/bootstrap.dag @@ -1,84 +1,120 @@ // src/v4/workflow/bootstrap.dag -// -// Scope: bootstrap orchestration AS DATA β€” the seed-once β†’ self-host β†’ -// fixed-point chain expressed as a .dag workflow, NOT a build.rs -// or shell script. v2's interpreter (`v2-compiler run`) executes -// this workflow; every step is data, so the bootstrap orchestration -// carries zero editable Rust authority. -// Anchor: THESIS:223-226 (meta-process: "Bootstrap, CI, build orchestration -// ... modeled as .dag workflows") + docs/design-pure-bootstrap-zero.md -// Β§"N=0 runtime boundary" (seed is external-to-v4; here in-repo as -// frozen src/v2/, not in src/v4/) -// -// Owns: -// - BootstrapPlan: the ordered step sequence -// - Step seed: v2-compiler compile --source-root src/v4 β†’ emit Rust -// to build-dir β†’ rustc β†’ v4-stage0 binary (v2 = seed, -// touched EXACTLY ONCE; v2's Rust lives in src/v2/, -// outside src/v4/, and is frozen/CI-gated) -// - Step self0: v4-stage0 compile src/v4 β†’ emit Rust (v4's OWN -// emission style) β†’ rustc β†’ v4-stage1 -// - Step self1: v4-stage1 compile src/v4 β†’ emit Rust β†’ rustc β†’ v4-stage2 -// - Step fixpt: assert stage1-emitted == stage2-emitted (BitIdentical); -// fixed point is stage1==stage2 (NOT stage0==stage1 β€” -// stage0 is v2-emission-style, stage1+ is v4-style) -// - artifact pinning: v4-stage-final binary is content-addressed; its -// hash is the anti-regression anchor (T-15 BitIdentical TestClaim) -// -// A3 (operator-ratified 2026-05-15) β€” the retirement predicate, honestly: -// - `retired` is NOT a count of hand-Rust files (v3's gameable proxy β€” -// defeated by paper-shrink: template-relocation, module-relocation). -// It is a REPRODUCTION: rebuild from (.dag + frozen-pinned seed) ONLY -// reproduces the pinned hash AND the seed's own hash matches its pin. -// `HandResidual` = the Rust the .dag-rebuild cannot reproduce β€” -// empty BY REPRODUCTION, never BY COUNT. -// - This is NOT un-gameable (no structural mechanism is β€” Trusting-Trust; -// the pin/CI/seed are all editable by whoever commits). Its job is -// EARLY, LOUD SURFACING: run per-PR on the affected set (T-21/T-24) so -// a gaming attempt (un-pin/edit seed, relocate Rust authority, add a -// 7th connective) is un-missable and routes to operator ratification -// the same commit β€” not silent drift found months later. -// - Seed trust is a NAMED AXIOM (built in the open, pinned at a known- -// good point), not a proof β€” stated honestly per feedback_no_engine. -// Any edit to / growth of src/v2/ is the maximally-conspicuous signal -// = STOP (INVARIANTS:136 bounded seed), routed to the operator. -// - Actual enforcement = operator-ratification spine + STOP-and-escalate -// culture + no proxy ratchet to game. Structure makes defection -// conspicuous, not impossible. -// - A4 corollary: a 7th connective / 6th behavior is the SAME machine β€” -// it changes the reproduction β†’ conspicuous signal β†’ STOP β†’ human -// judgment. Not "the substrate refuses by construction." -// - PROOF-1 (operator-ratified 2026-05-15) β€” the EXTERNAL trust- -// discharge: gunbc's structural evidence (A2 descent, the algebra- -// homomorphism chain, cost, effects) is emitted as a machine- -// checkable proof term an external Lean/Coq KERNEL checks. Converts -// the seed-trust NAMED AXIOM above into an INTERSUBJECTIVE check -// against an anchor gunbc does not own β€” does NOT make it -// un-gameable (the external kernel + evidence-faithfulness are the -// new named axioms; trust MOVED, not eliminated). The lens exports -// witnesses already held; the prover only kernel-checks, never -// searches (no-engine + A2). Full framing: STRUCTURE.md Β§7 + -// DECISIONS.md PROOF-1. -// -// Discipline: -// - This file is the ONLY bootstrap authority. No build.rs, no bootstrap.sh. -// A worker reaching for shell/build.rs orchestration has reintroduced -// editable Rust authority = STOP signal (the v3 regression door). -// - v2 interprets this (`v2-compiler run workflow/bootstrap.dag`) β€” v2 is -// never compiled INTO v4; it is the external frozen seed. -// - Emitted Rust is transient (build-dir; option (a)); never committed, -// never editable authority. .dag is sole authority. -// -// Consumes: -// - extdeps/process.dag: spawn v2-compiler / rustc / v4-stage-N subprocesses -// - extdeps/file_system.dag: read src/v4/*.dag, write build-dir Rust -// - std/diagnostic.dag: fail-closed on any step -// - std/verification.dag: BitIdentical TestClaim for the fixed-point assert -// -// Status: scaffold β€” fill per TASKS.md T-20 (scaffold early; full self-host -// content lands incrementally as the pipeline matures; T-15 consumes this -// for fixed-point validation) -// Brief: see BRIEF_TEMPLATE.md. +// Scope: v4-owned bootstrap orchestration AS DATA β€” four stages (seedβ†’stage0β†’stage1β†’stage2, fixpt stage1==stage2). compiled_by = stage compiler-of-record: seed←v2 (seed used once), self0←stage0, self1←stage1; v2 is never in the loop again (STRUCTURE.md "Seed used once" :404-405, SELF_HOSTING.md Β§meta-circular). +// Owns: CompileStage, FixptStage1Stage2, BootstrapPlan, bootstrap_stage_output, bootstrap_plan_well_formed, bootstrap_plan +// Consumes: v4.std.node, v4.std.diagnostic +// Status: filled β€” compiler-of-record is the self-hosting structural fact; structural gate only. module v4.workflow.bootstrap +import v4.std.node { Symbol } +import v4.std.diagnostic { + Correction, + Diagnostic, + Extent, + Locus, + NoCorrectionReason, + Outcome +} + +data v4_dag_source: Symbol = v4_dag_source +data v4_stage0_binary: Symbol = v4_stage0_binary +data v4_stage1_binary: Symbol = v4_stage1_binary +data v4_stage2_binary: Symbol = v4_stage2_binary +data v2_pipeline: Symbol = v2_pipeline +data bit_identical_check: Symbol = bit_identical_check + +type CompileStage { + consumes: List + produces: Symbol + compiled_by: Symbol +} + +type FixptStage1Stage2 { + left: Symbol + right: Symbol + via: Symbol +} + +type BootstrapPlan { + seed: CompileStage + self0: CompileStage + self1: CompileStage + fixpt: FixptStage1Stage2 +} + +data bootstrap_mis_wired: Symbol = bootstrap_mis_wired +data bootstrap_workflow_file: Symbol = bootstrap_workflow_file + +fn bs_diagnostic(reason: Symbol) -> Diagnostic { + Diagnostic { + reason: reason, + at: Textual { file: bootstrap_workflow_file, extent: WholeFile }, + correction: Unavailable { reason: AmbiguousIntent } + } +} + +// 🟑 List-op dissolution (Practice 10) β€” DECISIONS.md LB-P10-3213 +fn bs_member(s: Symbol, xs: List) -> Bool { + fold(xs, init: false, f: fn(acc, x) { + acc || (x == s) + }) +} + +fn bs_list_eq(a: List, b: List) -> Bool { + (count(a) == count(b)) + && fold(a, init: true, f: fn(acc, x) { + acc && bs_member(s: x, xs: b) + }) + && fold(b, init: true, f: fn(acc, y) { + acc && bs_member(s: y, xs: a) + }) +} + +fn bootstrap_stage_output(plan: Outcome, s: Symbol) -> Bool { + match plan { + Produced { value: bp } => (s == bp.seed.produces) || (s == bp.self0.produces) || (s == bp.self1.produces) + Rejected { diagnostic: _ } => false + } +} + +fn bootstrap_plan_well_formed(p: BootstrapPlan) -> Outcome { + if bs_list_eq(a: p.seed.consumes, b: [v4_dag_source]) + && (p.seed.produces == v4_stage0_binary) + && (p.seed.compiled_by == v2_pipeline) + && bs_list_eq(a: p.self0.consumes, b: [v4_dag_source, v4_stage0_binary]) + && (p.self0.produces == v4_stage1_binary) + && (p.self0.compiled_by == v4_stage0_binary) + && bs_list_eq(a: p.self1.consumes, b: [v4_dag_source, v4_stage1_binary]) + && (p.self1.produces == v4_stage2_binary) + && (p.self1.compiled_by == v4_stage1_binary) + && (p.fixpt.left == v4_stage1_binary) + && (p.fixpt.right == v4_stage2_binary) + && (p.fixpt.via == bit_identical_check) { + Produced { value: p } + } else { + Rejected { diagnostic: bs_diagnostic(reason: bootstrap_mis_wired) } + } +} + +data bootstrap_plan: Outcome = bootstrap_plan_well_formed(p: BootstrapPlan { + seed: CompileStage { + consumes: [v4_dag_source], + produces: v4_stage0_binary, + compiled_by: v2_pipeline + }, + self0: CompileStage { + consumes: [v4_dag_source, v4_stage0_binary], + produces: v4_stage1_binary, + compiled_by: v4_stage0_binary + }, + self1: CompileStage { + consumes: [v4_dag_source, v4_stage1_binary], + produces: v4_stage2_binary, + compiled_by: v4_stage1_binary + }, + fixpt: FixptStage1Stage2 { + left: v4_stage1_binary, + right: v4_stage2_binary, + via: bit_identical_check + } +}) diff --git a/src/v4/workflow/ci.dag b/src/v4/workflow/ci.dag index 052d3781395..91b796af0a6 100644 --- a/src/v4/workflow/ci.dag +++ b/src/v4/workflow/ci.dag @@ -1,43 +1,205 @@ // src/v4/workflow/ci.dag -// -// Scope: CI pipeline AS DATA. .github/workflows/ci.yml becomes a DERIVED artifact emitted from this file. Adding a CI gate = editing this one .dag file (THESIS:226). v3's gate #98 ci_yml_hand_authority_dissolved was an open R3 gap precisely because CI YAML was hand-authored β€” v4 must NOT reproduce it. -// Anchor: THESIS:223-226 (meta-process modeling: "Bootstrap, CI ... modeled as .dag workflows") + v4-close-interrogation.md Β§3.2 (ci_workflow_modeled_as_dag) + v3 gate #98 (the gap v4 must not reproduce) -// -// Owns: -// - CiPipeline { jobs: List, gates: List } -// - affected-set-driven job selection: consumes lens/affected_set.dag -// (this is what replaces scripts/detect-affected-components.sh β€” the -// shell bridge dissolves once this + affected_set land) -// - emission target: .github/workflows/ci.yml as DERIVED artifact (Shape B -// user-program emission β€” .dag walks CiPipeline, emits YAML) -// - C4 (operator-ratified 2026-05-15): the committed `ci.yml` MUST exist -// on disk (GitHub reads it from the repo) yet is NOT editable -// authority. It is a committed == emit(CiPipeline) CHECKED PROJECTION, -// guarded by the SAME machine as A3: if committed ci.yml β‰  -// emit(CiPipeline), CI is red and the divergence is conspicuous + -// STOP-routed. This is how feedback_no_generated_code_on_disk is -// honored honestly β€” "no editable generated AUTHORITY", not "no -// generated bytes on disk". The `.dag` is authority; the file is a -// checked projection. -// - cache keys in the emitted `ci.yml` are STRUCTURAL: each cacheable -// job's `actions/cache` key is `content_hash` (B1) of that job's -// input subgraph, derived from the dependency graph via -// lens/affected_set.dag β€” not a hand-authored `hashFiles(...)` glob. -// GHA `actions/cache` is one emission target of that hash; a remote -// build cache is another. The interim hand-written `hashFiles(...)` -// keys in the committed `ci.yml` (e.g. the v2-compiler-binary cache) -// are manual approximations of those content-hashes; emitting -// `ci.yml` from this file replaces them with the real structural keys. -// -// Consumes: -// - lens/affected_set.dag: job selection -// - extdeps/process.dag: CI steps spawn subprocesses -// - workflow/bootstrap.dag: CI runs the bootstrap chain -// -// Status: scaffold β€” fill per TASKS.md T-24 -// Brief: see BRIEF_TEMPLATE.md; this file's I/O contract is the immutable -// contract for the worker. Splitting this file requires explicit operator -// ratification (substrate extension = stop signal). +// Scope: CI pipeline AS DATA; gunbc job/gate DAG + eager well-formedness; ci.yml projection deferred. +// Owns: CiCommand, CiJob, CiGate, CiPipeline, ci_pipeline_well_formed, ci_pipeline +// Consumes: v4.std.node, v4.std.diagnostic, v4.workflow.bootstrap +// Status: filled β€” declarative core + eager well-formedness; structural v2 gate only. module v4.workflow.ci + +import v4.std.node { Symbol } +import v4.std.diagnostic { + Correction, + Diagnostic, + Extent, + Locus, + NoCorrectionReason, + Outcome +} +import v4.workflow.bootstrap { v4_stage0_binary, bootstrap_plan, bootstrap_stage_output } + + +// 🟑 coproduct dissolution β€” DECISIONS.md LB-P4-3213 +type CiCommand + = LintCommand + | TestCommand + | IgnoredTestCommand { test_name: String } + | BootstrapStageCompile { produces: Symbol } + | ShellCommand { command: String } + +type CiJob { + id: Symbol + command: CiCommand + needs: List +} + +type CiGate { + id: Symbol + job: Symbol +} + +type CiPipeline { + jobs: List + gates: List +} + + +data v2_compile_src_v4: Symbol = v2_compile_src_v4 +data structural_v2_compile: Symbol = structural_v2_compile + +data ci_pipeline: Outcome = ci_pipeline_well_formed(p: CiPipeline { + jobs: [ + CiJob { + id: v2_compile_src_v4, + command: BootstrapStageCompile { produces: v4_stage0_binary }, + needs: [] + } + ], + gates: [ + CiGate { id: structural_v2_compile, job: v2_compile_src_v4 } + ] +}) + + +data ci_duplicate_job_id: Symbol = ci_duplicate_job_id +data ci_duplicate_gate_id: Symbol = ci_duplicate_gate_id +data ci_dangling_reference: Symbol = ci_dangling_reference +data ci_dependency_cycle: Symbol = ci_dependency_cycle +data ci_bootstrap_authority_violation: Symbol = ci_bootstrap_authority_violation +data ci_workflow_file: Symbol = ci_workflow_file + +fn ci_diagnostic(reason: Symbol) -> Diagnostic { + Diagnostic { + reason: reason, + at: Textual { file: ci_workflow_file, extent: WholeFile }, + correction: Unavailable { reason: AmbiguousIntent } + } +} + +// 🟑 List-op dissolution (Practice 10) β€” DECISIONS.md LB-P10-3213 +fn ci_id_occurrences(id: Symbol, jobs: List) -> Int { + fold(jobs, init: 0, f: fn(acc, j) { + if j.id == id { acc + 1 } else { acc } + }) +} + +fn ci_symbol_resolves(s: Symbol, jobs: List) -> Bool { + fold(jobs, init: false, f: fn(acc, j) { + acc || (j.id == s) + }) +} + +fn ci_member(s: Symbol, ids: List) -> Bool { + fold(ids, init: false, f: fn(acc, x) { + acc || (x == s) + }) +} + +fn ci_all_job_ids_unique(jobs: List) -> Bool { + fold(jobs, init: true, f: fn(acc, j) { + acc && (ci_id_occurrences(id: j.id, jobs: jobs) == 1) + }) +} + +fn ci_gate_id_occurrences(id: Symbol, gates: List) -> Int { + fold(gates, init: 0, f: fn(acc, g) { + if g.id == id { acc + 1 } else { acc } + }) +} + +fn ci_all_gate_ids_unique(gates: List) -> Bool { + fold(gates, init: true, f: fn(acc, g) { + acc && (ci_gate_id_occurrences(id: g.id, gates: gates) == 1) + }) +} + +fn ci_all_needs_resolve(jobs: List) -> Bool { + fold(jobs, init: true, f: fn(acc, j) { + acc && fold(j.needs, init: true, f: fn(acc2, n) { + acc2 && ci_symbol_resolves(s: n, jobs: jobs) + }) + }) +} + +fn ci_all_gate_jobs_resolve(gates: List, jobs: List) -> Bool { + fold(gates, init: true, f: fn(acc, g) { + acc && ci_symbol_resolves(s: g.job, jobs: jobs) + }) +} + +fn ci_job_needs(id: Symbol, jobs: List) -> List { + fold(jobs, init: [], f: fn(acc, j) { + if j.id == id { j.needs } else { acc } + }) +} + +fn ci_blocked(id: Symbol, remaining: List, jobs: List) -> Bool { + fold(ci_job_needs(id: id, jobs: jobs), init: false, f: fn(acc, n) { + acc || ci_member(s: n, ids: remaining) + }) +} + +fn ci_eliminate_pass(remaining: List, jobs: List) -> List { + fold(remaining, init: [], f: fn(acc, id) { + if ci_blocked(id: id, remaining: remaining, jobs: jobs) { + concat([id], acc) + } else { + acc + } + }) +} + +fn ci_kahn_fixpoint(jobs: List) -> List { + fold(jobs, init: map(jobs, fn(j) { j.id }), f: fn(remaining, job) { + ci_eliminate_pass(remaining: remaining, jobs: jobs) + }) +} + +fn ci_acyclic(jobs: List) -> Bool { + count(ci_kahn_fixpoint(jobs: jobs)) == 0 +} + +// 🟑 negative-coverage plan-bound (T-22) β€” DECISIONS.md LB-T22-3213 +fn ci_command_authority_ok(c: CiCommand) -> Bool { + match c { + LintCommand => true + TestCommand => true + IgnoredTestCommand { test_name: _ } => true + BootstrapStageCompile { produces: pr } => bootstrap_stage_output(plan: bootstrap_plan, s: pr) + ShellCommand { command: _ } => true + } +} + +fn ci_all_commands_authority_ok(jobs: List) -> Bool { + fold(jobs, init: true, f: fn(acc, j) { + acc && ci_command_authority_ok(c: j.command) + }) +} + +fn ci_pipeline_well_formed(p: CiPipeline) -> Outcome { + if ci_all_job_ids_unique(jobs: p.jobs) { + if ci_all_gate_ids_unique(gates: p.gates) { + if ci_all_needs_resolve(jobs: p.jobs) { + if ci_all_gate_jobs_resolve(gates: p.gates, jobs: p.jobs) { + if ci_acyclic(jobs: p.jobs) { + if ci_all_commands_authority_ok(jobs: p.jobs) { + Produced { value: p } + } else { + Rejected { diagnostic: ci_diagnostic(reason: ci_bootstrap_authority_violation) } + } + } else { + Rejected { diagnostic: ci_diagnostic(reason: ci_dependency_cycle) } + } + } else { + Rejected { diagnostic: ci_diagnostic(reason: ci_dangling_reference) } + } + } else { + Rejected { diagnostic: ci_diagnostic(reason: ci_dangling_reference) } + } + } else { + Rejected { diagnostic: ci_diagnostic(reason: ci_duplicate_gate_id) } + } + } else { + Rejected { diagnostic: ci_diagnostic(reason: ci_duplicate_job_id) } + } +}