Feature contract: nat-modulo — compile-time natural remainder#

One of the five compile-time natural arithmetic heads of Language & Testing Evolution L12k (PRD 08 N1: "naturalAdd/Multiply/… on two literals are primitive-evaluated"). Compact naturals are compile-time constants with bounded primitive operations; there is NO runtime arbitrary-precision natural.

1. Lexical and grammar rules, including precedence and termination#

(nat-modulo a b): a fixed binary head, both operands terms of type Nat. Draft edition alpha-2027 only; under alpha-2026 the form is ALPHA-EDITION-UNSUPPORTED-FORM.

2. Scope and binding rules, including generated names#

Binds nothing; no generated names.

3. Type and quantity requirements#

Nat -> Nat -> Nat. Both operands are checked against Nat (a Byte operand is ALPHA-TYPE-MISMATCH). Runtime usages are the union of the operands' usages.

4. Effects, totality, and evaluation-order rules#

Pure and total. (nat-modulo a b) is the remainder of the truncated division; (nat-modulo a 0) is a (so a = q*b + r holds with q = 0; stated). The result is a compact literal computed in O(digits) by integer arithmetic when BOTH operands normalize to closed naturals (compact literal or unary); otherwise the node is a stuck neutral term (no unfolding rule relates (nat-add x 1) to (succ x) — recorded, not implied).

5. Elaboration into existing core or a specifically versioned new core extension#

Elaborates to the trusted-core node RNatModulo (Alpha.Core naturalModulo), a new core extension serialized as alpha-checked-interface-v5 (tags 60–64; v4 readers do not accept v5 — every cached interface is recomputed once).

6. Representation and target support, where relevant#

Compile-time only. Erasure folds closed operands to the unary runtime literal (ALRI v4 unchanged) and REFUSES an operand that did not fold with the named error CompileTimeArithmeticAtRuntime — no lane executes the node; programs use the Std.Natural functions for runtime values. The direct lane never sees the node (closed operands fold before projection; an open one is refused at erasure first).

7. Error codes and primary/secondary origins#

ALPHA-TYPE-MISMATCH (operand not Nat, at the operand's span); ALPHA-EDITION-UNSUPPORTED-FORM (the head under alpha-2026, at the form's span); CompileTimeArithmeticAtRuntime (erasure of an unfolded node, reported by the build).

8. Formatting and migration rules#

Printed as the S-expression (nat-modulo a b) by the generic head renderer. No migration from alpha-2026 (the form did not exist); the Std.Natural eliminators remain the runtime owners and the specification the primitive must agree with.

9. Positive, negative, execution, and edge-case tests#

tests/language/NatArithmeticCompileTime.alpha (refl laws incl. 10^20·10^20, mixed unary/compact, saturation, x/0 = 0, x mod 0 = x, an open operand that checks) through debug/nat-arithmetic-check.py (work counters 10^3..10^20 under 2 s each, wrong-value control rejected, alpha-2026 rejection, erasure refusal by name, a folded program built and executed with the folded exit status, and evaluator-lane agreement with the Std.Natural eliminators on small operands with a discriminating control); bootstrap tests in alpha-core and alpha-surface.

10. Compatibility with the old edition, serialized forms, and cache keys#

alpha-2026 corpus unchanged (the head is not a form there). Serialized cores carry the v5 schema; the receipt identity moves with the compiler identity as for any kernel change.