docs: codify unsigned widening boundaries

Author: a19q3

CHANGELOG.md

@@ -25,6 +25,10 @@
 - Allow direct lifecycle operations to be authorized by kernel-effect
   equivalents: `transfer` accepts `replace + relock`, and `destroy` accepts
   `consume + burn`.
+- Define expression-local unsigned widening: primitive unsigned integers may
+  widen inside arithmetic and numeric comparison only; integer literals may be
+  context-typed, but non-literal values do not widen across assignment, return,
+  ABI, witness, layout, field initialization, or serialization boundaries.
 - Convert canonical bundled examples, language examples, README examples, wiki
   tutorials, and release gates to strict 0.15 kernel-effect capabilities.
 - Extend strict acceptance and syntax-combination gates so bundled examples

docs/CELLSCRIPT_CKB_LANGUAGE_AUDIT.md

@@ -40,6 +40,15 @@ literals, explicit `protected` / `witness` / `require` lock syntax, and
 fixed-width `lock_args` binding. It does not add implicit signer authority,
 hidden sighash defaults, or automatic signature verification.
 
+The 2026-05-18 coercion hardening keeps numeric convenience inside verifier
+expressions while preserving explicit boundaries. The rule is named
+expression-local unsigned widening: primitive unsigned integers may widen only
+inside arithmetic and numeric comparison. Assignment, return, ABI, witness,
+Molecule/layout, struct field initialization, and serialization boundaries
+remain exact-type boundaries unless the source contains an explicit cast.
+Integer literals may still be context-typed by an expected primitive integer
+type, but non-literal values do not pretend to have another width at a boundary.
+
 The 0.13 compiler also exposes CKB-specific evidence instead of hiding it behind
 a generic artifact:
 

docs/wiki/Tutorial-02-Language-Basics.md

@@ -94,6 +94,39 @@ Hash
 Use fixed-size byte arrays when a value must live in a predictable persistent
 schema or CKB data layout.
 
+### Expression-local Unsigned Widening
+
+CellScript supports expression-local primitive unsigned integer widening for
+arithmetic and numeric comparison:
+
+```cellscript
+let total: u64 = amount_u64 + fee_u16
+let under_limit: bool = fee_u16 < amount_u64
+```
+
+The chain is `u8 -> u16 -> u32 -> u64 -> u128`, but the widening is local to
+the expression being evaluated. It does not cross assignment, return, ABI,
+witness, `create` layout, struct field initialization, or serialization
+boundaries.
+
+Integer literals may be context-typed by an expected primitive integer type:
+
+```cellscript
+let byte: u8 = 1
+```
+
+Non-literal numeric values must keep their actual width at boundaries:
+
+```cellscript
+let amount64: u64 = amount16        // rejected
+let explicit: u64 = amount16 as u64 // accepted
+```
+
+Compound assignment is a write boundary. `target += rhs` is valid only when
+`rhs` is the same width as, or narrower than, `target`. Generic `u128`
+arithmetic and ordering remain unsupported except for explicitly implemented
+`u128` delta or equality paths.
+
 `Signature` is not a built-in scalar. If a contract needs to carry a signature,
 model it explicitly:
 

docs/wiki/Tutorial-11-Scoped-Invariants-and-ProofPlan.md

@@ -243,6 +243,25 @@ When some related action origins still lack matching evidence, ProofPlan reports
 `declared(unmatched_related_action_obligation_count:...)` so reviewers do not
 mistake one matching action for exhaustive action coverage.
 
+## Numeric Boundary Evidence
+
+ProofPlan and release review should treat integer width changes at verifier
+boundaries as explicit evidence. The language rule is expression-local unsigned
+widening: `u8`, `u16`, `u32`, `u64`, and `u128` values may widen inside
+arithmetic and numeric comparison, but not across assignment, return, ABI,
+witness, layout, struct field initialization, or serialization boundaries.
+
+For boundary values, the source should show intent:
+
+```cellscript
+receipt.amount = value as u64
+```
+
+Do not read acceptance of mixed-width arithmetic as acceptance of implicit
+numeric coercions throughout the language. Non-literal boundary conversions
+must stay explicit so reviewers can see which transaction fields, witness
+values, and serialized layouts changed width.
+
 ## JSON Output
 
 For tooling, use:

src/types/mod.rs

@@ -6553,6 +6553,116 @@ where
         assert!(err.message.contains("matching types") || err.message.contains("u128"), "u64==u128 rejected: {}", err.message);
     }
 
+    #[test]
+    fn expected_type_does_not_widen_non_literal_let_boundary() {
+        let err = check(&source_module(
+            r#"
+module types::expected_let_no_widen
+
+action bad(x: u16) -> u64
+where
+    let y: u64 = x
+    return y
+"#,
+        ))
+        .unwrap_err();
+        assert!(
+            err.message.contains("type mismatch") || err.message.contains("mismatch"),
+            "let expected type should not widen a non-literal u16 into u64: {}",
+            err.message
+        );
+    }
+
+    #[test]
+    fn expected_type_does_not_widen_non_literal_return_boundary() {
+        let err = check(&source_module(
+            r#"
+module types::expected_return_no_widen
+
+action bad(x: u16) -> u64
+where
+    return x
+"#,
+        ))
+        .unwrap_err();
+        assert!(
+            err.message.contains("return type") || err.message.contains("mismatch"),
+            "return expected type should not widen a non-literal u16 into u64: {}",
+            err.message
+        );
+    }
+
+    #[test]
+    fn expected_type_does_not_widen_non_literal_abi_arg_boundary() {
+        let err = check(&source_module(
+            r#"
+module types::expected_abi_no_widen
+
+fn takes_u64(x: u64) -> u64 {
+    return x
+}
+
+action bad(x: u16) -> u64
+where
+    return takes_u64(x)
+"#,
+        ))
+        .unwrap_err();
+        assert!(
+            err.message.contains("argument 1 type mismatch"),
+            "ABI argument expected type should not widen a non-literal u16 into u64: {}",
+            err.message
+        );
+    }
+
+    #[test]
+    fn expected_type_does_not_widen_non_literal_field_boundary() {
+        let err = check(&source_module(
+            r#"
+module types::expected_field_no_widen
+
+struct Holder {
+    value: u64,
+}
+
+action bad(x: u16) -> u64
+where
+    let holder = Holder { value: x }
+    return holder.value
+"#,
+        ))
+        .unwrap_err();
+        assert!(
+            err.message.contains("type mismatch"),
+            "field expected type should not widen a non-literal u16 into u64: {}",
+            err.message
+        );
+    }
+
+    #[test]
+    fn explicit_cast_can_cross_integer_width_boundary() {
+        check(&source_module(
+            r#"
+module types::explicit_cast_boundary
+
+struct Holder {
+    value: u64,
+}
+
+fn takes_u64(x: u64) -> u64 {
+    return x
+}
+
+action good(x: u16) -> u64
+where
+    let y: u64 = x as u64
+    let holder = Holder { value: x as u64 }
+    return takes_u64(y) + holder.value
+"#,
+        ))
+        .expect("explicit casts should be accepted across integer width boundaries");
+    }
+
     #[test]
     fn contextual_integer_literals_fit_declared_widths() {
         let module = source_module(