Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 40 additions & 11 deletions dag/gunbc/char_at_scaling_probe_support.dag
Original file line number Diff line number Diff line change
@@ -1,24 +1,53 @@
module gunbc.char_at_scaling_probe_support

import std.types { NonEmptyStr }
import std.disposition { Disposition, Terminal }
import std.disposition { Disposition, Scaffold, SingleAuthority }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import std.dissolution { DissolutionCondition, unbound_dissolution }

// Per DESIGN §4b: this probe IS the discriminating evidence for CHARAT-0's O(1)
// char_at claim, so it stays enrolled rather than dissolving — the disposition is
// Terminal, not Scaffold. §5's same-unit rule is why this carries its own
// independent trigger rather than sharing json_parse_scaling_probe.rs's: the two
// probes measure different primitives (char_at cost in isolation vs. end-to-end
// parse) and could have independently different lifetimes.
data char_at_scaling_probe_disposition: Disposition = Terminal {
reason: "the entry point `src/v1/stage0/src/bin/char_at_scaling_probe.rs` resolves against — a single `char_at` call, isolated from every other primitive, so per-access cost can be fit against position and against string length without the JSON parser's independent list-materialization cost. NOT floor-enrolled; the acceptance evidence for CHARAT-0's O(1) claim."
// DISPOSITION: Scaffold, NOT Terminal. The base of this branch carried a
// three-way contradiction -- a `Terminal` disposition, a `DissolutionCondition`
// beside it, and a `.rs` header reading SCAFFOLD -- and an earlier revision of
// this PR resolved it toward Terminal. That was the wrong side, per review 53457.
//
// The deciding fact is that NOTHING EXECUTES THIS BIN: it is hand-run, it is not
// floor-enrolled, and no cadence, workflow or witness invokes it (checked
// corpus-wide -- the only references are its own Cargo.toml row and this module).
// DESIGN §4b keeps a class's discriminating RED and positive control "enrolled as
// the executing evidence"; enrolled means executing. Evidence no consumer runs is
// a measurement transport, which is a legitimate thing for a probe to be and is
// precisely the Scaffold shape -- an instrument whose lifetime ends when the
// property it measures is floor-enrolled. Calling it Terminal is the §4b rung
// inflation case: a carrier named for the top rung while occupying the bottom,
// and an inflated class never ranks for climbing. It would also convert bounded
// hand-Rust in the seed into permanent unowned hand-Rust, against §7's shrink.
//
// This restores a dissolution obligation that the base already carried; it is
// NOT net-new debt requiring an operator verdict under §5 -- the §5 disposition
// is AcknowledgePreexistingDebt, which exists so that recording debt already
// present never reads as creating it.
//
// The `Scaffold` row and the `DissolutionCondition` row are complementary, not a
// §3 dual representation: §5 rules lifecycle and admission two separate questions,
// and `std.disposition` `Scaffold` carries a construction mechanism and a binding
// "and nothing else" -- WHAT it dissolves to. WHEN it dissolves is the
// `DissolutionCondition`'s fact, and neither row can state the other's.
data char_at_scaling_probe_disposition: Disposition = Scaffold {
dissolves_to: SingleAuthority,
bind: DeclarationRef {
module_path: "gunbc.char_at_scaling_probe_support",
decl_name: "char_at_probe",
field: WholeDeclaration
}
}

// §3: cite the symbol, not a position or another file's marker. The bin's own
// grep receipt is `CHAR_AT_SCALING_PROBE_SCAFFOLD_MARKER` in
// `char_at_scaling_probe.rs` — a real, distinct const from
// `char_at_scaling_probe.rs` -- a real, distinct const from
// `json_parse_scaling_probe.rs`'s `JSON_PARSE_SCALING_PROBE_SCAFFOLD_MARKER`,
// which this probe's disposition no longer cites or depends on.
// which this probe's disposition no longer cites or depends on. The SCAFFOLD
// spelling is correct again now that the disposition is Scaffold; the rename to
// IDENTITY_MARKER was downstream of the Terminal reading and is reverted with it.
data char_at_scaling_probe_dissolution: DissolutionCondition = unbound_dissolution(
description: "delete `src/v1/stage0/src/bin/char_at_scaling_probe.rs` (grep receipt: `CHAR_AT_SCALING_PROBE_SCAFFOLD_MARKER`) when char_at's O(1) property is floor-enrolled with a modeled witness, or when a fresh run of this probe's own printed TSV (mean_call_us per string_len/position, per its CHECKABLE RECEIPT doc comment) shows mean_call_us growing with string_len across the CHAR_AT_PROBE_LENGTHS range instead of staying flat" as NonEmptyStr
)
Expand Down
60 changes: 60 additions & 0 deletions dag/test/claim/string_length_char_count_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
module test.claim.string_length_char_count_witness

// CONTRACT: `.length()` and `.count()` on a String report the CHARACTER
// (codepoint) count, never the UTF-8 BYTE count. The discriminating risk is a
// fast-path arm that reads a byte length: a naive `Value::Str(s) => Some(s.len())`
// (Rust byte length) would answer 3 for the single-codepoint CJK string below,
// not 1. Any future O(1) fast path -- an ASCII-flag read included -- must keep
// answering the character count on multibyte input, and these cases go red if
// it does not.
//
// WHY `.size()` IS NOT COVERED HERE, measured rather than assumed. `size` is a
// registered-but-UNREACHABLE spelling: the interpreter admits it at runtime
// (`method_call.length { "length" | "count" | "size" }` in `v1_interpreter.rs`)
// and `gunbc.v1_interpreter_primitive_surface` declares it as a third authored
// spelling, but the typechecker's method-existence authority
// (`v1_compiler_infer_method.rs` `builtin_function_registry`) seeds `count` and
// inserts `length` and never inserts `size`. So `"x".size()` refuses at compile
// time -- `method 'size' not found on receiver type 'Primitive(String)'` -- and
// no `.dag` source can reach the runtime arm through it. Adding a `.size()` case
// here does not extend coverage; it reds the build, which is how this was found
// (CI on this PR, not by reading the surface).
//
// That fork is a real defect and is NOT this witness's to fix: three names for
// one concept is nicknaming (DESIGN §2/§3), so the likely correct repair is to
// DELETE `size` from the interpreter arm and the primitive surface rather than
// to widen the typechecker to admit it. Either direction changes a load-bearing
// file and needs its own change. Until one lands, this witness covers exactly
// the two spellings that are reachable.

test fn ascii_string_length_is_char_count() -> Bool {
"hello".length() == 5
}

// "\u{ef}" (lowercase i with diaeresis) encodes as 2 bytes in UTF-8.
// Byte length would be 2; character length must be 1.
test fn multibyte_two_byte_codepoint_length_is_one() -> Bool {
"\u{ef}".length() == 1
}

// "\u{4e2d}" (CJK character) encodes as 3 bytes in UTF-8.
// Byte length would be 3; character length must be 1.
test fn multibyte_three_byte_codepoint_length_is_one() -> Bool {
"\u{4e2d}".length() == 1
}

// "\u{1f600}" (an emoji) encodes as 4 bytes in UTF-8.
// Byte length would be 4; character length must be 1.
test fn multibyte_four_byte_codepoint_length_is_one() -> Bool {
"\u{1f600}".length() == 1
}

// "na\u{ef}ve" is 5 characters but 6 UTF-8 bytes (the \u{ef} costs 2 bytes).
// Byte length would be 6; character length must be 5.
test fn mixed_ascii_and_multibyte_length_counts_chars_not_bytes() -> Bool {
"na\u{ef}ve".length() == 5
}

test fn multibyte_string_count_matches_length() -> Bool {
"\u{4e2d}\u{6587}".count() == 2
}
6 changes: 5 additions & 1 deletion src/v1/stage0/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,11 @@ path = "src/bin/json_parse_scaling_probe.rs"

# Isolated char_at scaling receipt: position x string-length, uncontaminated by the
# JSON parser's independent list-accumulation cost (eager-koi-458 scope correction,
# 2026-08-17). DISSOLUTION: delete alongside json_parse_scaling_probe.rs.
# 2026-08-17). SCAFFOLD -- disposition authority is
# `char_at_scaling_probe_disposition` in dag/gunbc/char_at_scaling_probe_support.dag.
# DISSOLUTION: its OWN trigger (`char_at_scaling_probe_dissolution`), NOT alongside
# json_parse_scaling_probe.rs -- the two probes measure different primitives and can
# have independently different lifetimes (DESIGN section 5, same-unit rule).
[[bin]]
name = "char_at_scaling_probe"
path = "src/bin/char_at_scaling_probe.rs"
Expand Down
Loading