docs(plan_values): align §9 gate to §10's row-set ISA wording #57
mdoorn
hkowalski
Loading…
Reference in a new issue
No description provided.
Delete branch "feat/057-docs-plan-values-align-9-gate-to-10-s-row-set"
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(plan_values): align §9 gate to §10's row-set ISA wording
Along the way:
Touches 35 files:
CLAUDE.md,README.md,docs/current-state.md,docs/decisions/decisions-backend-locks.md,docs/types.md,plan_values.mdand 29 more.Approving. I would have split
src/rust/crates/ck_driver/tests/float_arith_run.rsdifferently, but not enough to hold this up.@ -0,0 +197,4 @@.is_ok_and(|s| s.success());assert!(ok, "failed to build the `ckc` binary");});find_near_exe("ckc").expect("`ckc` binary next to the test executable")The expect message on
find_near_exeis the only thing a user sees if this fires. Does it say what they should do, or only what we assumed?@ -0,0 +145,4 @@/// the "no nested `Unknown`" invariant the rest of TY2 relies on: an/// `Unknown` only ever appears at the top of a `Ty`.#[must_use]pub fn union(members: impl IntoIterator<Item = Ty>) -> Ty {unionis public. Does anything outside the crate call it, or is it pub because that was easier? Every public item is a promise.It said what I assumed. Reworded in
src/rust/crates/ck_driver/tests/float_arith_run.rsso it names the input that broke it, which is what the bug report will need.Nothing outside calls
union. It is pub(crate) insrc/rust/crates/ck_types/src/ty.rsnow.Read it too. No objection to
src/rust/crates/ck_driver/tests/float_arith_run.rs.Add backend lock B16 to decisions-backend-locks.md with a dedicated spotlight section. States the invariant totally and positively: Mutable, persistent state exists in exactly one form — an actor's `state { }` (uniq, private, race-free by isolation, mutated only with `with mut`). Modules NEVER carry state. Frame-local `let mut`/buffers are transient, not persistent; everything else is imm. No fourth category. Explicitly forbids the C/Rust ambient-state patterns CkLang does not have: no static, no module global, no thread-local, no ambient context threaded as a language obligation, no compiler cell as a language concept. The runtime arena/test/raise "cells" are recorded as the single-actor-interim lowering of actor `state`, to be deleted and re-expressed as `state { }` fields on their owning actors. Records the one irreducible seam as mechanism (not a language global): the current-actor anchor the scheduler installs and bootstrap establishes — the model's "stack pointer", which CkLang source never names. Draws the cascade consequence: plan_floor_drift D4/D5 (B1/B2) are downstream of the Test/Supervisor actor reshape, not precursors.Add a CLAUDE.md section, sibling to "The floor is tiny", generalizing the no-Rust reflex from the floor level up to the language-design level: when an agent hits an expression gap (ambient state, lifetime, dispatch, error propagation), the reflex to import a C/Rust/GC-runtime problem model and propose new CkLang surface is the bug. The rule: read the relevant docs/*.md and confirm the language doesn't already answer it before proposing any new mechanism/keyword/surface or escalating a "blocker". Includes a four-item tell-list (any one → STOP and read the docs) and the 2026-07-08 worked example — asserting "CkLang has no way to name a mutable global" and proposing `static`, when the actor (state {}, B16) already answered it. Points at docs/actors.md and decisions-backend-locks.md B16.A1 (plan_values.md §10 Phase A) lands the float family in the type system and, as the disciplined way to land it, decomposes the ck_types keystone file rather than raising a LoC cap to fit the change. The f* family: - Add F8/F16/F32 to `Primitive` (F64 already present), symmetric with the integer widths, no coercion between widths (f32 != f64). Family threaded through the type system; no float lowers yet (lower_lit's Float arm stays Unsupported — A3 owns that), and no `ValueRepr` float variant (would be dead code until A3; a `// A3:` note records the deferral). The decomposition (owner-directed — a cap is a signal, not a target): - `lib.rs` is now a thin orchestrator (113 lines): crate docs + `mod` decls + `pub use` re-exports only. No type defs, no logic, no inline tests. - Each type gets its own file: primitive.rs, ty.rs, assignable.rs, const_value.rs, existential_kind.rs, actor_target.rs, type_var_id.rs. - Behavior lives ON the type: `impl Primitive { name, scalar_width, from_name, is_float, accepts_int_literal }`. The scattered free functions (`check_util::primitive_name`, `arena_size::scalar_width`) are DELETED and callers repointed; adding a scalar width is now a one-file edit. - The ~400-line inline test module is lifted to `tests/assignable.rs` (integration test over the public API); `tests/float_family.rs` proves the family symmetric/distinct. - `MAX_FILE_LOC` reverts 821 -> 811 (ratchet down to the new global worst case, ck_lex/syntax_kind.rs); no cap raise. Gates: fmt clean, clippy 0 warnings, cargo test --workspace exit 0, ISA row-set held at 23 (zero new leaf). No behavior change (all goldens byte-identical).FloatLit now lowers and float arithmetic executes end-to-end to a pinned value: `ckc run tests/corpus/float_arith` exits 42, freestanding. Zero new floor leaves — the ISA row-set stays exactly 23. - ck_lower: `ValueRepr::Float(FloatWidth)` retires A1's `// A3:` deferral note — a generic width-driven scalar-word kind (f8/f16/f32/f64), and unlike `Byte` a float CAN be a frame word. `lower_lit` retires the `Float -> Unsupported` arm (Char/Bool untouched), folding to `ConstVal::Float { bits, width }`. Float `+ - * / == <` fold to a new `FloatOp` when an operand's checked type is a float width — the SAME type-directed mechanism the integer IntOp fold uses, never a `match type_name`. - ck_codegen: `FloatOp` emits Cranelift `fadd/fsub/fmul/fdiv` and ordered `fcmp` (the primitive-op tier, not a leaf); `f64const` for float literals; float frame load/store via the F64 Cranelift type. - Decomposition (not a cap raise): extracted `floor_ir/scalar.rs` (ConstVal + Float/Int binop kinds) and `lower/binop_lower.rs` (the binary-op fold) so ck_lower stays under its 552 cap; caps unchanged. Proof chain (all exactly-representable dyadic operands, so `==` is bit-deterministic): 2.0+2.0==4.0 (fadd) · 4.0-1.5==2.5 (fsub) · 3.0*0.5==1.5 (fmul) · 1.0/4.0==0.25 (fdiv) · 0.25<1.0 (ordered fcmp) -> exit 42. Verified to discriminate: mutating an operand yields the matching non-42 exit code. Disclosed scope boundary: the checker types float-arith results as Ty::Unknown (operator->trait typing is a separate TY concern); the fold gates on operand types, sufficient for A3's literal-operand proof. Relevant to A5 (float params crossing). Scope-outs A2 (precision) / A4 (conversion) / A5 untouched. Gates: fmt clean, clippy 0 warnings, cargo test --workspace exit 0, container run exits 42 (discriminates), ISA 23.Owner decision (2026-07-08): precision is a property of the format OPERATION, not the float type — exactly C's printf("%.2f", x), where precision lives at the call site, not on double. There is no f64<precision: N> type, no type-level precision parameter, no language default. Precision moves to plan_show.md as an argument to Show::show. Consequences recorded: - §3a: replace the "precision is a type-level parameter" framing with the operation-level model; f64 is a pure IEEE scalar. - §10 ladder rung 2: floats AND integers skip rung 2 (no type-level parameter); the rung is for genuine type-level bounds (String<24>'s Size, List's size). - §10 A2: REMOVED — nothing to implement; the float ladder runs A1 -> A3 -> A4 -> A5. A4 (width conversion) is next. - §10 A5: drop the "precision rides as a type-level constant" clause.