fix(operators): the five B2 repairs — the law enforced where Rust used to guess #74

tvidal · 2026-04-01T19:24:11+02:00

tvidal commented

2026-04-01 19:24:11 +02:00

fix(operators): the five B2 repairs — the law enforced where Rust used to guess

Along the way:

fix+test(operators/const-param): finishing pass — every gate green, ratchet 120 → 94
docs: twelfth-session handoff — owner ruled B; operators B2 + const-param (OQ#25) LANDED (e449d67→6479f6c), slice 7 COMPLETE; the ≤1-instruction coercion law recorded; B2's masked runtime regression found and repaired (35 tests, four roots — the law arriving where the blind path guessed); ratchet 120→94; stdlib-type-clean green first time since B2; debts #35/#49/#52 closed, #58-61 minted; cap 822→840 + E0748/E0749 await owner ratification
feat(prelude): the byte leaf joins the roster — u8-mirrored impls in both Preludes + byte_ops stone
test(operators): the §7 conformance matrix realized — operator→leaf goldens, negative resolution rows, the delete-the-declaration gate; debt #51 closed

Touches 63 files: Prelude.ck, handoff.md, plan.md, src/rust/crates/ck_codegen/src/arg.rs, src/rust/crates/ck_codegen/src/binding.rs, src/rust/crates/ck_codegen/src/call.rs and 57 more.

fix(operators): the five B2 repairs — the law enforced where Rust used to guess Along the way: - fix+test(operators/const-param): finishing pass — every gate green, ratchet 120 → 94 - docs: twelfth-session handoff — owner ruled B; operators B2 + const-param (OQ#25) LANDED (e449d67→6479f6c), slice 7 COMPLETE; the ≤1-instruction coercion law recorded; B2's masked runtime regression found and repaired (35 tests, four roots — the law arriving where the blind path guessed); ratchet 120→94; stdlib-type-clean green first time since B2; debts #35/#49/#52 closed, #58-61 minted; cap 822→840 + E0748/E0749 await owner ratification - feat(prelude): the byte leaf joins the roster — u8-mirrored impls in both Preludes + byte_ops stone - test(operators): the §7 conformance matrix realized — operator→leaf goldens, negative resolution rows, the delete-the-declaration gate; debt #51 closed Touches 63 files: `Prelude.ck`, `handoff.md`, `plan.md`, `src/rust/crates/ck_codegen/src/arg.rs`, `src/rust/crates/ck_codegen/src/binding.rs`, `src/rust/crates/ck_codegen/src/call.rs` and 57 more.

praghunathan approved these changes

2026-04-02 06:30:00 +02:00

praghunathan left a comment

A clear improvement. The change in src/rust/crates/ck_driver/src/compile/mock.rs is the part I would have argued for.

A clear improvement. The change in `src/rust/crates/ck_driver/src/compile/mock.rs` is the part I would have argued for.

src/rust/crates/ck_driver/src/compile/mock.rs

					
				@ -654,0 +710,4 @@

				/// seeds plus this op's own parameters (E5 — `fn info(msg: String)` seeds `msg`

				/// at `String`), each keyed by its name-token span. The two never collide (a

				/// param cannot re-use a sibling state field's name — E0305).

				fn op_body_seeds(

op_body_seeds reads, decides and writes in one function. The deciding part is the piece I would want to test on its own. Worth splitting?

`op_body_seeds` reads, decides and writes in one function. The deciding part is the piece I would want to test on its own. Worth splitting?

mdoorn approved these changes

2026-04-02 09:08:34 +02:00

mdoorn left a comment

Second read on src/rust/crates/ck_driver/src/compile/mock.rs. Nothing to add.

Second read on `src/rust/crates/ck_driver/src/compile/mock.rs`. Nothing to add.

tvidal commented

2026-04-02 09:30:00 +02:00

Split. The decision in op_body_seeds is a pure function now, with its own tests in src/rust/crates/ck_driver/src/compile/mock.rs.

Split. The decision in `op_body_seeds` is a pure function now, with its own tests in `src/rust/crates/ck_driver/src/compile/mock.rs`.

tvidal added 5 commits

2026-04-02 12:34:39 +02:00

fix(operators): the five B2 repairs — the law enforced where Rust used to guess 8f16479646

The killed coherence-blind BinOp path had been compiling unlawful code; each
repair is the law applied: (1) §3a mixed-sign sites in stdlib .ck spell their
coercions (Bytes/Clock/Scheduler/Test/Meta/Assert — usize-vs-Int, letter form);
(2) two-word String returns consumed generically at call sites (emit_call_words,
repr-keyed, no type-name test; str_abi_word flattens via the shared arg path);
(3) list-literal for-binder element typing in the per-body recheck (loops.rs,
mirrors the range arm); (4) f8/f16 pre-claimed float impls authored in both
Preludes (Add/Sub/Mul/Div/Neg/Equals/Ord — the plan_traits roster completed);
(5) freestanding_actor String bound crossing spelled (let s: String = …).
Also: the Concat body's (la + lb)::usize parse gap worked around via a let
(parser rejects value-turbofish after a parenthesized expr — debt minted).

Rust net +72; .ck net +50.

fix+test(operators/const-param): finishing pass — every gate green, ratchet 120 → 94 eb3f71d8cd

(1) mock-op bodies TYPED: the project Tables threaded into lower_mock_op —
mock ops now type-check (seeded binders) and lower through lower_body_full with
method_impls; the untyped sliver is gone. (2) receive-probe runs the FS3
cross-module fixpoint — operator-impl callees discovered like the main path.
(3) freestanding_test golden re-recorded (+1 span drift from + → ++, verified
byte-identical otherwise). (4) Concat-allocation ruling applied: os_acquire
stands (surface CkLang cannot name the interim arena cell — FS7a will own
dispatch-scoped allocation; debt minted); six arena-accounting assertions
re-blessed to the lawful truth with the debt citation. (5) arena_oom
re-expressed: bounded list-allocation loop exhausts the arena at RUNTIME
(exit 101, OutOfMemory::Exhausted) — its old String-doubling now correctly
E0748s at compile time. (6) the ~20 stdlib-less operator fixtures trapped and
blessed from real output; untrapped ratchet 120 → 94 (tighter than the 98
target: full-trap discipline swept 4 pre-existing diagnostics; forcing 98
would have required selective under-trapping). (7) Bytes.ck 'let state'
keyword collision renamed (scratch); five corpus trap.mds re-blessed (+1
column drift); stdlib-type-clean gate green for the FIRST time since B2 —
22 more §1a coercions spelled in Clock.ck/Mailbox.ck (the gate had been
silently disabled by the Bytes.ck parse error).

Rust net +98 (mock typed path, probe fixpoint); harness +29; fixtures +186.

docs: twelfth-session handoff — owner ruled B; operators B2 + const-param (OQ#25) LANDED (e449d67→6479f6c), slice 7 COMPLETE; the ≤1-instruction coercion law recorded; B2's masked runtime regression found and repaired (35 tests, four roots — the law arriving where the blind path guessed); ratchet 120→94; stdlib-type-clean green first time since B2; debts #35/#49/#52 closed, #58-61 minted; cap 822→840 + E0748/E0749 await owner ratification 3e55e53cc0

feat(prelude): the byte leaf joins the roster — u8-mirrored impls in both Preludes + byte_ops stone 7dfb5562a8

The `byte` scalar leaf ({size 8, unsigned int}, its own identity though it
shares u8's machine word) was declared in Floor.ck/Floor.ckh but inert: zero
trait impls, zero corpus usage, so no program could ever construct one
(primitives-slice audit finding). Mirror the full u8 coherence roster for
byte in both Preludes (repo-root Prelude.ck and its tests/corpus/stdlib twin,
kept identical): Add/Sub/Mul/Div/Rem/Neg/Equals/Ord/BitAnd/BitOr/BitXor/
BitNot/Shl/Shr, each a one-line body naming the same Floor leaf the u8 row
calls (iadd/isub/imul/udiv/urem/ineg/ieq+ine/ult+ule+ugt+uge/band/bor/bxor/
bnot/ishl/ushr) — 14 rows added per file, nothing invented beyond what u8
already has.

Verified empirically (built ckc, ran with absolute paths against the real
stdlib) that the generic Floor pipeline already treats byte exactly like u8
end to end — codegen derives the Cranelift type from the leaf's repr
{size,signed,float}, never the name — so no Rust change and no Floor.ck/
Floor.ckh edit was needed. Finding worth recording: Floor's `where T is A or
B or ...` union bounds are not currently enforced by the type checker at all
(the lift step drops any union bound, ck_types::predicate.rs) — byte's calls
type-check today because the bound is a no-op, not because byte and u8 are
considered equivalent. Out of scope here (no Rust changes requested), but
future union-bound enforcement will need byte added to Floor's where-lists
to keep compiling.

New corpus stone tests/corpus/byte_ops exercises every added row through
real operator syntax (+ - * / % unary- == != < <= > >= & | ^ unary~ << >>,
never a direct Floor:: call) on 12::byte/5::byte — chosen so every op has a
non-trivial, discriminating result. Eighteen checks chain to a distinct
failure code (1..18) or exit 42; confirmed freestanding (no NEEDED, no
undefined symbols, no libc/ck_rt, 6752 bytes). Runtime-gated by
ck_driver/tests/byte_ops_run.rs (modeled on int_convert_run.rs) and
registered in RUNTIME_TESTED (runtime_registry.rs) so the app cannot regress
to diagnostics-only.

Gates: cargo fmt --check clean; cargo clippy --all-targets -D warnings clean;
cargo build --workspace clean; cargo test -p ck_driver --test architecture
21/21; cargo test -p ck_driver --test stdlib_type_clean green; cargo test
--workspace --no-fail-fast: only the 3 expected soft-assert canaries FAILED
inside captured stdout (soft_asserts/freestanding_write/string_eq negative
fixtures), every real test-binary result ok.

test(operators): the §7 conformance matrix realized — operator→leaf goldens, negative resolution rows, the delete-the-declaration gate; debt #51 closed f113304b01

Positive proofs (through the glyphs, never a qualified call): a new
corpus stone `operator_leaves` computes ten signed/unsigned-discriminating
checks (i32/u32 `/` -> sdiv/udiv, `%` -> srem/urem, `<` -> slt/ult,
`>>` -> sshr/ushr, `^` -> bxor, and the heterogeneous `i8 + f32 -> fadd`
delegation through `+` itself) and exits 42 iff all hold; gated by
`ck_driver/tests/operator_leaves_run.rs` and registered in
`RUNTIME_TESTED`. This closes tracked debt #51 (handoff.md): `%`/`/` are
now exercised end-to-end through the operators with exit-code
verification.

Negative resolution goldens (tests/types, .cktest style, real diagnostics
discovered via CK_BLESS then hand-trapped): `"a" + "b"` (String has no
Add impl — E0728) and `3.0 % 2.0` (no Rem<f64,f64,?>, alongside a
same-file i64 `%` positive control — E0728). Both fully `# trap`-covered
so the untrapped-diagnostic ratchet stays at 94.

The delete-the-declaration property gate (item 3) was found ALREADY
LANDED — `ck_parser::tests::operator::deleting_the_plus_declaration_makes_1_plus_2_a_parse_error`
builds a doctored `OperatorTable::from_source` missing `+` and proves
`1 + 2` becomes a parse error; verified green, no new work needed.

FINDING, not fixed (test-only slice): the `u32 + i32` negative row could
NOT be landed. `ck_types::method_call::resolve_method_call` selects
candidate traits via `coherence.traits_for(recv_ty.id)` — any impl for
the RECEIVER's type — never checking the full operand-pair key at
candidate-selection time; with `Add<u32,u32,u32>` + `Add<i32,i32,i32>`
both declared (no cross-sign impl), `u32 + i32` still resolves with ZERO
diagnostics (the impl-selection miss fails soft to `Unknown`, and
`assignable(i32, Unknown)` is permissive). Reproduced against both a
`.cktest` fixture and the real `Prelude.ck`. Recorded as new tracked
debt #62 in handoff.md, citing `method_call.rs:528`; the row could not be
authored without encoding the bug as "expected".

Gates (this worktree, from src/rust): cargo fmt --check clean; cargo
clippy --all-targets -- -D warnings clean; cargo build --workspace
clean; cargo test --workspace --no-fail-fast → 1359 passed, 3 failed
(the expected soft-assert canaries, inside captured stdout); cargo test
-p ck_driver --test architecture → 21/21; cargo test -p ck_driver --test
conformance → untrapped ratchet unchanged at 94.

tvidal manually merged commit 918bddac85 into master

2026-04-02 12:34:39 +02:00

tvidal referenced this pull request from a commit

2026-04-02 12:34:39 +02:00

Merge pull request #74 from northgale/feat/074-fix-operators-the-five-b2-repairs-the-law-enfo

Sign in to join this conversation.

No reviewers

No labels

No milestone

No project

No assignees

3 participants

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

northgale/cklang-bootstrap!74

Rows
Columns