Evaluate generic checked unsigned subtraction in compiler-produced pure programs #730

Executable claim

The generic pure evaluator can execute a compiler-produced core.integer.subtract<U32/U64> expression with deterministic checked semantics and normal budget accounting. Jim remains an external conformance consumer; no editing nouns enter Echo production code.

Reproduced boundary

An isolated source copy of jedit PR #302 at 83ab52a3744babb63c8ce15cd94d917012e364a2 adds and returns deletedByteCount = input.endByte - input.startByte under its existing ordered-range constraint. Edict compiler #211 plus target-validation #212 now completes the public application build using the unchanged provider 49e9efb68001dfd78563d18bac9359a87671e431.

The resulting package and verified-host digest were supplied to the existing generic evaluator at 8c725d699241a7e3adee482029031ff6bade25fa through a COPY-based Docker copy of Jim's standalone conformance host. The non-vacuous test ran and returned EvaluationError::UnsupportedProgram at evaluation. The parser currently only accepts zero-argument, zero-type-argument helper calls.

Scope and acceptance

• Decode the exact compiler-produced subtraction form with U32/U64 width and exactly two operands; preserve existing helper calls and artifact compatibility.
• Interpret bounded unsigned values with checked subtraction, rejecting malformed/over-width/signed operands and underflow without wrap, saturation, or panic.
• Preserve the interpreter's step, allocation, depth, input, output, and package-identity limits.
• Prove literal results and deterministic resource accounting from the real external compiler artifact, including zero and nonzero differences, invalid input, and package substitution.
• Add adversarial operand/type/arity/underflow and budget tests with structured outcomes.
• Document that pure evaluation is not package admission, graph mutation, Tick settlement, receipt, WAL, or recovery.

Dependencies and safe intermediate state

Extend the generic pure-evaluation implementation from PR #726. The externally generated conformance fixture depends on flyingrobots/edict#210 and flyingrobots/edict#212. This is a child capability needed by #684, not completion of #684 or jedit's full rope operation. Existing Jim producer locks remain unchanged until a separate integration step verifies the new producer set.

No native Jim planner, caller-provided patch, rope algorithm, or application callback is in scope.