diff --git a/issues/0116-const-write-not-rejected.md b/issues/0116-const-write-not-rejected.md
index c9f9ed8..9024dc1 100644
--- a/issues/0116-const-write-not-rejected.md
+++ b/issues/0116-const-write-not-rejected.md
@@ -5,7 +5,8 @@
 > const-flagged global (array consts, #run consts) or a module value
 > const (struct consts incl.) — with `cannot assign through constant
 > 'X'`. A deref along the chain (`p.*`) breaks the root (pointer writes
-> stay the documented escape until the const-ness steps); a local
+> are permanently unchecked — the documented pointer contract, specs.md
+> §Pointer Types); a local
 > shadowing the const name stays writable. Regression test:
 > examples/1162-diagnostics-const-write-rejected.sx (struct field — the
 > crash repro, array element, compound, bare scalar).
diff --git a/readme.md b/readme.md
index cbae90c..d502eb0 100644
--- a/readme.md
+++ b/readme.md
@@ -126,6 +126,27 @@ int+float arithmetic promotes to the float in either operand order (`n + 0.5` an
 `0.5 + n` are both `f64`), so `C : s64 : M + 0.5` is rejected regardless of order
 while `F : f64 : M + 0.5` folds to `2.5`.
 
+**Aggregate constants.** Array- and struct-typed `::` constants are immutable
+globals — one storage, reads index into it directly, whole-value uses copy by
+value, and unused tables are dropped from the binary. `::` is the one and only
+const spelling (`const` is not a keyword):
+
+```sx
+K : [4]s64 : .[11, 22, 33, 44];   // typed array const
+A :: .[1, 2, 3];                  // untyped — infers [3]s64
+M :: .[1, 2.2, 3];                // numeric mix promotes — [3]f64
+LIT :: Color.{ r = 255, g = 0, b = 0 };   // struct const — also one global
+
+N :: K[0] + K[3];     // 55 — const element reads fold at compile time
+D : [K.len]u8 = ---;  // [4]u8 — .len and LIT.r fold in dimensions too
+K[0] = 5;             // error: cannot assign through constant 'K'
+```
+
+Writes through any constant's name — element, field, compound — are compile
+errors; a local copy (`k := K`) stays writable. A struct constant whose
+initializer calls a function (`CALL :: Color.{ r = bump(), … }`) is re-evaluated
+at each use (documented contract); use `NAME :: #run f();` for evaluate-once.
+
 **Float → integer narrowing (unified rule).** A float flowing into an
 integer-typed binding *without* a cast follows the same integral-fold rule an
 array dimension uses: an **integral** compile-time float folds to its integer, a
diff --git a/specs.md b/specs.md
index 4a6b8f1..95e8503 100644
--- a/specs.md
+++ b/specs.md
@@ -1029,6 +1029,18 @@ val := mp[2];             // 30
 - `T` → `*T` at call sites (implicit address-of)
 - `null` (`*void`) → any `*T`
 
+**Unchecked writes (the pointer contract)**: pointers carry no
+read-only qualifier — there is no `const` pointer type in sx (`const` is
+not a keyword). Taking the address of constant storage yields a plain
+pointer: `@K` on an array constant `K : [4]s64 : .[...]` is `*[4]s64`.
+Reads through it are fine; **writes through any pointer are unchecked**,
+and writing into constant storage through a pointer is undefined behavior
+(the storage is marked constant in the emitted binary). The compile-time
+guard on constants protects their *name* — every assignment whose target
+chain is rooted at a constant is rejected (see
+[Constant-Write Rejection](#constant-write-rejection)); a dereference in
+the chain leaves the checked zone.
+
 **Fat pointer layout**: `[:0]u8`, `string`, and `[]T` are `{ptr, i64}` structs. The raw pointer is always the first field at offset 0. This means `*[:0]u8` works as C's `char**` — a C function dereferences through the outer pointer and reads the raw `char*` from offset 0.
 
 ### Optional Types
@@ -1439,7 +1451,7 @@ isReady : ValueListenable(bool) = map(
 - `:=` bindings infer type from the right-hand side
 - Explicit annotation overrides inference: `NAME : f64 : 0.9;`
 - Integer literals default to `s64`
-- Float literals default to `f32`
+- Float literals default to `f64`
 - Enum literals (`.variant`) infer their enum type from context (expected type)
 
 ### Type Conversions
@@ -1517,15 +1529,19 @@ NAME :: value;
 NAME : type : value;
 ```
 
-The `::` operator creates an immutable binding. The value is evaluated at compile time when possible.
+The `::` operator creates an immutable binding. The value is evaluated at
+compile time when possible.
+
+`::` is the one and only constant spelling in sx. `const` is not a keyword
+and never will be — it is an ordinary identifier.
 
 Examples:
 ```sx
-SOME_INT    :: 0;           // s32
+SOME_INT    :: 0;           // s64
 SOME_STR    :: "Hello";     // string
-SOME_FLOAT  :: 0.3;         // f32
+SOME_FLOAT  :: 0.3;         // f64
 SOME_DOUBLE : f64 : 0.9;   // f64 (explicit)
-SOME_FUNC   :: () => 42;    // () -> s32
+SOME_FUNC   :: () => 42;    // () -> s64
 SOME_TYPE   :: f64;         // type alias
 ```
 
@@ -1541,6 +1557,110 @@ A constant expression's type is its promoted result type (see
 operand order: `C : s64 : M + 0.5` and `C : s64 : 0.5 + M` are both rejected, and
 `F : f64 : M + 0.5` is accepted and folds to `2.5`.
 
+#### Array Constants
+
+An array-typed `::` constant is an **immutable global**: one storage,
+registered once, marked constant in the emitted binary. Indexed reads GEP
+into that storage directly — no per-use copies. Unused array constants are
+dropped by dead-global elimination.
+
+```sx
+K : [4]s64 : .[11, 22, 33, 44];   // typed
+A :: .[1, 2, 3];                  // untyped — infers [3]s64
+M :: .[1, 2.2, 3];                // untyped — infers [3]f64
+
+x := K[i];      // GEP into the global — no copy
+y := K;         // by-value copy (normal array-value semantics);
+                // mutating y does not touch K
+f(K);           // by-value param — copy at the call
+p := @K;        // *[4]s64 — address of the const storage (reads)
+```
+
+Untyped inference unifies the element types: all ints → `s64`; any float
+present promotes the whole element type to `f64` (int elements convert
+exactly, mirroring "an integer fits any integer or float"); all floats →
+`f64`; `bool` / `string` elements must be homogeneous. Element shapes may
+nest (array-of-structs, array-of-arrays, struct-containing-array). The
+length comes from the element count.
+
+Diagnostics (each rejects the declaration):
+- A non-numeric element mix (string + int, bool + int):
+  `constant 'X' mixes incompatible element types — annotate the array type`.
+- A runtime element (a call, a variable read):
+  `constant 'X' must be initialized by compile-time constant elements`.
+- A typed declaration whose length disagrees with the initializer:
+  `constant 'X' declares [3] elements but its initializer has 2`.
+
+#### Struct Constants
+
+A struct-typed constant whose every field **serializes** — literals, enum
+literals, bools, strings, nested aggregates, named-const leaves, constant
+expressions (`K + 1`), another constant's field (`LIT.r`), a const array's
+element (`A[1]`) — becomes an immutable global exactly like an array
+constant: one storage, field reads GEP it, `@LIT` is addressable, copies
+are independent. The same constant-expression forms are accepted as
+elements of array constants.
+
+```sx
+Color :: struct { r, g, b: s64; }
+LIT  :: Color.{ r = 255, g = 0, b = 0 };        // one global; uses GEP it
+EXPR :: Color.{ r = K + 1, g = K * 2, b = 0 };  // folds, also one global
+W : Color : Color.{ r = 1, g = 2, b = 3 };      // typed form, same storage
+```
+
+A struct constant with a **non-serializable** initializer field (a call, a
+runtime-global read, `@x`, `context`) keeps **inline re-lowering**
+semantics: the initializer is evaluated **at each use**. This is the
+documented contract for this class — side effects run per use and the
+value may differ between reads:
+
+```sx
+counter : s64 = 0;
+bump :: () -> s64 { counter += 1; counter }
+CALL :: Color.{ r = bump(), g = 0, b = 0 };
+
+print("{} {}\n", CALL.r, CALL.r);   // prints '1 2'; counter is now 2
+```
+
+For evaluate-once semantics use `NAME :: #run f();` (see
+[Compile-time Evaluation](#8-compile-time-evaluation)).
+
+#### Constant Folding over Aggregates
+
+An array constant's `.len` and `K[<const idx>]` element reads, and a
+struct constant's field (`LIT.r`), are compile-time integer leaves —
+usable in array dimensions and in other constants' initializers,
+source-aware like every const fold:
+
+```sx
+N :: K[0] + K[3];    // 55 — folds
+L :: K.len;          // 4
+D : [K[1]]u8 = ---;  // [22]u8 — const-index read in a dimension
+E :: K[9];           // error: index 9 is out of bounds for constant 'K'
+                     //        (4 elements) — diagnosed at fold time
+```
+
+#### Constant-Write Rejection
+
+An assignment or compound assignment whose target chain is **rooted at a
+constant** is a compile error — scalar consts, array-const elements, and
+struct-const fields alike:
+
+```sx
+N = 9;          // error: cannot assign through constant 'N' —
+K[0] = 5;       //   constants are immutable (use a '=' global or a
+K[1] += 2;      //   local copy for mutable data)
+WHITE.r = 0;    // same — struct field
+```
+
+Two boundaries:
+- A **local that shadows** the constant's name is an ordinary variable and
+  stays writable.
+- A **dereference along the chain breaks the root**: `p.*` writes through a
+  pointer, and pointer writes are unchecked (see
+  [Pointer Types](#pointer-types) — writing into constant storage through
+  a pointer is undefined behavior).
+
 ### Variable Binding (mutable)
 
 ```sx