Observable outcome
An authored len(value) on bounded Bytes lowers through Edict Core and independently validated Target IR to a generic byte-length operation returning U64. This implements the byte-count portion of EDICT-LANG-LEN-001 without confusing it with String Unicode-scalar length.
Reproduced consumer failure
A disposable copy of flyingrobots/jedit#302 adds and returns insertedByteCount: U64 = len(input.replacement) beside the already compiled unsigned deleted-byte difference. The public JSONL application build at 3d05b8b2a4b552bf4afd402c20dc2e198601e69d fails with ApplicationCompilationFailed / TypeCheck UnresolvedFunction: pure helper len has no compiler context fact. The operation needs the inserted byte count for its application-owned rope facts and result.
Scope
- Recognize the existing prelude spelling
len for structurally bounded Bytes, with exactly one argument and no authored type arguments.
- Produce a generic Core operation retaining the operand and its exact type coordinate; return U64.
- Independently check argument arity, byte shape, bounds/type coordinate, result width, and local authority at the Target boundary. Preserve result-projection and artifact identity semantics.
- Reject unsupported String/List/record/integer operands in this slice rather than silently using bytes as Unicode-scalar length.
- Preserve the existing imported helper path. No application vocabulary enters compiler or runtime core.
- Record the real consumer build advancement and adversarial Core mutation results; tests execute in copied-source Docker only.
Acceptance and exclusions
Source and target positive witnesses cover bounded/exact bytes, changed operands, and U64 output. Negative witnesses use structured failures for wrong arity/type arguments/operand types, mismatched target coordinates, dangling locals, and forged output width. The public consumer build must advance past its current UnresolvedFunction boundary.
String length, concatenation/slicing, full rope semantics, graph access, runtime execution, settlement, and release/consumer repinning are excluded. Target acceptance is not proof of Echo evaluator support; run the actual emitted package to identify that boundary separately.
This is a prerequisite for the authored operation in flyingrobots/jedit#296/#302. The consumer probe also uses #210/#212 subtraction. Preserve its existing checked-in producer pins and baseline proof; candidate experiments are isolated.
Observable outcome
An authored
len(value)on boundedByteslowers through Edict Core and independently validated Target IR to a generic byte-length operation returning U64. This implements the byte-count portion of EDICT-LANG-LEN-001 without confusing it with String Unicode-scalar length.Reproduced consumer failure
A disposable copy of flyingrobots/jedit#302 adds and returns
insertedByteCount: U64 = len(input.replacement)beside the already compiled unsigned deleted-byte difference. The public JSONL application build at3d05b8b2a4b552bf4afd402c20dc2e198601e69dfails withApplicationCompilationFailed/ TypeCheckUnresolvedFunction:pure helper len has no compiler context fact. The operation needs the inserted byte count for its application-owned rope facts and result.Scope
lenfor structurally bounded Bytes, with exactly one argument and no authored type arguments.Acceptance and exclusions
Source and target positive witnesses cover bounded/exact bytes, changed operands, and U64 output. Negative witnesses use structured failures for wrong arity/type arguments/operand types, mismatched target coordinates, dangling locals, and forged output width. The public consumer build must advance past its current
UnresolvedFunctionboundary.String length, concatenation/slicing, full rope semantics, graph access, runtime execution, settlement, and release/consumer repinning are excluded. Target acceptance is not proof of Echo evaluator support; run the actual emitted package to identify that boundary separately.
This is a prerequisite for the authored operation in flyingrobots/jedit#296/#302. The consumer probe also uses #210/#212 subtraction. Preserve its existing checked-in producer pins and baseline proof; candidate experiments are isolated.