Docs(types,runtime): lead with the manifest property + R2 stance #19
Loading…
Reference in a new issue
No description provided.
Delete branch "feat/019-docs-types-runtime-lead-with-the-manifest-prop"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
Docs(types,runtime): lead with the manifest property + R2 stance
Along the way:
Touches 28 files:
README.md,docs/impl/lowering/F1-floor-ir-scaffold.md,docs/impl/lowering/F2-cranelift-backend.md,docs/impl/lowering/README.md,docs/impl/memory-model/arenas.md,docs/impl/runtime-testing/README.mdand 22 more.Approving. I would have split
docs/impl/runtime/00-executor.mddifferently, but not enough to hold this up.@ -0,0 +50,4 @@| Trait-bounded call `x.show()` where `T: Show` | direct call to the monomorphized `Show_for_T::show(x)` || Generic `f::<Int>(...)` | direct call to the monomorphized `f_Int(...)` || `for x in range { body }` | iterator protocol: `let it = range.iter(); while let Some(x) = it.next() { body }` (Range stays as a value) || Variant construction `Some(42)` | record construction with the variant's tag set |Where does the number beside
Variantcome from? It reads as measured rather than chosen, and nothing on the line says which.@ -2,0 +13,4 @@>> The replacement is described across [F1–F4](README.md#foundation--pipeline-scaffolding-orders-14)> (lowering + container + meta-stream wire) plus the new> [R1-executor-core.md](R1-executor-core.md) (test fn execution as aexecutionreads, decides and writes in one function. The deciding part is the piece I would want to test on its own. Worth splitting?@ -30,2 +36,2 @@- **In:** `ck --interactive` entry; the root supervisor actor; single carrier + shared event loop (one thread, run-to-completion, no preemption); `spawn <Name>` as a message to the supervisor; `Ephemeral` child spawn; a **safe** per-actor arena (bootstrap stand-in); arena reclaim on stop; the minimal `MetaStream` events (`ActorSpawned` / `ActorDespawned` / `MessageSent` / `MessageReceived`) and a minimal `RuntimeState` (live-actor set + arena high-water, enough to observe reclaim).- **Out:** evaluating expressions in a behavior ([order 2](R1-executor-core.md)); multi-actor `send` / `receive` between user actors (order 10); supervisor **restart** and the full lifetime model (`Singleton` / `Bound`, order 9); the user-facing `spawn` return shape ([todo #1](../../../todo.md)); the real page-map arena and any `unsafe` (deferred — see decision 4); multi-carrier / work-stealing (order 10); the `ArenaReclaimed` meta event (proposed, co-lands with M7 — reclaim is observed here via `RuntimeState`, not a meta event).- **In:** the floor library (`ck_rt`) gains: the root supervisor actor; single carrier + shared event loop (one thread, run-to-completion, no preemption); `Ephemeral` child spawn primitive; a **safe** per-actor arena (bootstrap stand-in); arena reclaim on stop; the minimal `MetaEvent` emissions (`ActorSpawned` / `ActorDespawned` / `MessageSent` / `MessageReceived`) via F4's `emit_meta_event`; and a minimal `RuntimeState` (live-actor set + arena high-water, enough to observe reclaim) flushed at binary exit. The compiled binary's entry point is updated to boot the supervisor.- **Out:** evaluating expressions in a behavior ([order 6](R1-executor-core.md)); multi-actor `send` / `receive` between user actors (order 14); supervisor **restart** and the full lifetime model (`Singleton` / `Bound`, order 13); the user-facing `spawn` return shape ([todo #1](../../../todo.md)); the real page-map arena and any `unsafe` (deferred); multi-carrier / work-stealing (order 15); the `ArenaReclaimed` meta event (proposed, co-lands with M7 — reclaim is observed here via `RuntimeState`, not a meta event).An unsafe block around
Out. What invariant makes it sound, and where is that written down? A// SAFETY:line would save the next reader the audit.Split. The decision in
executionis a pure function now, with its own tests indocs/impl/runtime/00-executor.md.SAFETY comment added above
Outindocs/impl/runtime/substrate-and-supervisor.md, and a debug assertion for the invariant, so a violation fails a test rather than a user.Measured. It is a named constant in
docs/impl/lowering/README.mdnow, with a line saying how.Two updates from a design conversation that surfaced load-bearing context not yet in the canonical docs: 1. The type-system docs lead with mechanisms (no subtyping, synthesis-only, universal turbofish) but never name the *property* those mechanisms exist to enforce: every type is visible in the source. That property is the AI-first + Go-speed commitments expressed at the type level — it is the reason all the mechanisms are shaped the way they are. Added section in type-system/README.md ("The property the type system exists to deliver") and reworked the opening of inference.md to frame "synthesis-only" as the *how* in service of the *why*. Uses the PL-theory term "manifest" (types are written, not implicit) with a parenthetical disambiguating it from "structural typing" (shape-equality — distinct, and not what CkLang is; CkLang is nominal). 2. R2's spec previously had a placeholder open-questions section. The things that read as "open" close on principles already in the docs (meta-substrate is observation-only, uniform rules, runtime trusts the front-end) — so they aren't questions. Replaced with one positively-framed "Locked stance" line: match is first-arm-wins; exhaustiveness is TY7's contract; an unreachable arm at eval raises Panic::raise(Unreachable). Also fixed an HM-flavored phrase in the front-end prerequisite (arms "unify" → arms widen by tag membership) and recorded TY7 as a hard prerequisite for match. Docs-only. Link checker: 0 broken anchors. cargo check: 0 warnings.Two architectural reframes from a design conversation, landing as one re-slice of the runtime cascade: 1. RETIRE THE TREE-WALKER. The bootstrap interpreter (ck_eval) is being removed. CkLang's design choices (manifest typing, no GC, no general subtyping, no HM, no dynamic dispatch, monomorphization, closed existentials, bounded collections) make direct lowering simpler than interpretation for this language — the hard things compilation usually defers don't exist here. The HIR's semantics are now the formal reference; the lowering is the only engine. R11 (as-if optimizer) is checked against "the simplest lowering's meta stream," not a separate interpreter. 2. CONTAINER EXECUTION VIA CRANELIFT. The new pipeline: HIR -> Floor IR -> Cranelift IR -> object file -> linked binary -> Alpine container -> meta-stream observation. - Cranelift (user lock) for codegen; multi-target falls out. - "Floor IR" (the user's "almost-floor HIR") is the intermediate; desugars defer into cleanup-wrapping, expands match to decision trees, gives closures explicit captures, monomorphizes trait calls. - "ck" container (user lock) is long-lived per session, Alpine to start, single bind-mount carries binary in + meta-stream file out. `--container <name>` flag for multi-container later. - Per-type generated MetaEvent serialization (no protobuf complexity) per the bounded-collections static-schema rule. Doc split per user directive "lowering belongs to lowering, running belongs to running": - new docs/impl/lowering/ — Floor IR + Cranelift backend - docs/impl/runtime/ — container scaffold + floor library + actor semantics + as-if optimizer + replay New cascade (17 slices = 4 foundation + 13 semantic, was 12): F1 Floor IR scaffold F2 Cranelift backend F3 Container scaffold F4 Meta-stream wire format R1 Substrate (was order 1) R1' Test fn execution as compiled binary (was R1 tree-walker, retired) R2 Bindings & control flow R3 Calls & recursion (+ NEW: recursion-depth bounds locked 2026-05-28 - every recursive function declares max depth, compiler uses it for arena stack-frame sizing; spelling open. Third member of the bounded-everything family alongside bounded collections.) R4 Unhappy path (defer desugared in Floor IR) R5 Raise path (system unwinder + Cranelift unwind tables) R6 Mocked effects R7 Native leaf R9 Lifetimes & supervision R8 Multi-actor messaging R10 As-if optimizer R11 OOM upcall R12 Deterministic replay What landed in this commit: - README.md: top-level synthesis (writes modern, runs 1960s, observes 2030s) — the load-bearing framing per project_synthesis_framing. - docs/impl/lowering/{README,F1,F2}.md: new directory. - docs/impl/runtime/{F3,F4}.md: new foundation slices. - docs/impl/runtime/README.md: rewritten cascade table + phase narrative for the new model. - docs/impl/runtime/substrate-and-supervisor.md + R1-executor-core.md: reframed under the new engine (substrate now at order 5; R1 = test fn execution as compiled binary, order 6). - docs/impl/runtime/R2-R12: cascade metadata (Phase / Order rows) aligned with the 17-slice cascade; light language updates for the engine swap. The user said "we will refine them later" — these are the alignment pass, not deep rewrites. - docs/impl/runtime/00-executor.md: marked RETIRED at the top; body preserved as historical record of the c1fd68d landing. - docs/types.md: bounded-collection rule documented (List<Int>(12) — every collection carries max size). - docs/impl/memory-model/arenas.md: arena sizing pass now documented as inferred from the bounded-collection rule + recursion bounds. - docs/impl/runtime-testing/*: anchor fixes for the new runtime README's section structure. What did NOT land in this commit (deliberately): - Old `ck_eval` crate removal — that's code change, lands when F1+F2 are implemented and supersede it. - The 34 docs that reference bare `List<T>` in examples — a separate sweep, the user is aware. - The recursion-bound spelling (annotation site + syntax) — principle locked, spelling open per project_recursion_bounds. - Sub-doc renames (file names kept stable; per user "I do not care about your JIRA"). Quality gates: link checker 0 broken anchors. No code touched.