1 files changed, 55 insertions, 8 deletions
diff --git a/chapter-construction/README.md b/chapter-construction/README.md
index c61bd7b7..f0ea4222 100644
--- a/chapter-construction/README.md
+++ b/chapter-construction/README.md
@@ -75,7 +75,7 @@ including their existing integer range widening. For example:
 
 ```simple
 struct Counter {
-    int x;
+    val x = 0;
     new Counter = { int n -> while (x < n) x++; };
 };
 return new Counter(arg).x;
@@ -86,6 +86,17 @@ performs no field Store on each trip.  At the constructor exit, the compiler
 stores the final value into the new object.  This is the result scalar
 replacement would give us, built directly from the construction rules.
 
+Even final data fields can change during construction; they become final when
+the constructor finishes. `x = 1; x = 2;` leaves the local value 2 for the exit
+Store. In the loop above, `x++` updates a local Phi, not memory. No sequence of
+final field Stores needs cleaning up inside the loop.
+
+A constant default does not make a field shared by every instance: a later
+constructor may change it. Inferred field types therefore describe the value's
+family, not just its initial constant. Ordinary local `val` bindings remain
+final. Shared function declarations are also fixed; a constructor cannot replace
+one of those functions.
+
 Private memory is still useful at the helper boundaries. `NewNode` produces
 the pointer and its initial private memory. The hidden initializer computes
 defaults as local values and emits ordinary initializing Stores at exit.  The
@@ -109,18 +120,17 @@ initialized length are published before the array is returned.  Required
 non-null fields have no legal zero default.  Reading one before it is written
 is an error.
 
-
 ## Publish only after completion
 
 `EscapeNode` publishes one field.  It consumes control, public memory, private
 memory, and `self`; its result joins the field's value into the public alias.
 Publication has no machine instruction, but its memory edges keep initializing
-Stores before later Loads and Stores.  Every field is published independently, 
+Stores before later Loads and Stores.  Every field is published independently,
 and scheduling may well interleave the initializing writes from many unrelated
 allocations and public memory updates.
 
 Before publication, every required field must be initialized on every live
-path.  This is rejected when `arg` can be zero:
+path.  This constructor is rejected:
 
 ```simple
 struct Box {
@@ -130,10 +140,44 @@ struct Box {
 return new Box(arg);
 ```
 
-This is rejected because `int[] data` requires a non-null initial value, and if
-`arg` is null, `data` is never set not-null.  This check is based on the type
-of every field at the constructor exit; if type analysis (e.g. SCCP) determines
-the field is set, the code is good; if not then not.
+`int[] data` requires a non-null initial value. If `n` is zero, `data` is never
+set. The current parser follows explicit missing-initialization values through
+the constructor's merges and checks its exit. This happens before SCCP: even
+calling this constructor only with `new Box(1)` does not rescue it. Allowing
+later type analysis to prove completion would require deferring this check.
+
+
+## Helper calls and *final* fields during construction
+
+Constructor code may read the unfinished object, but never an uninitialized
+field. Ordinary code must not observe it before construction finishes.
+
+We would like to allow helper calls when optimization proves they do not expose
+the unfinished object. Inlining could turn a helper's field accesses into local
+values. After optimization reaches a fixed point, each final field would have
+a final Store: before that line, accesses use local values; after it, the field
+can be read but never written. Mutable fields can still be written later.
+
+This is a proposed relaxation, not implemented in this snapshot. The parser
+currently rejects passing `self` to an ordinary method before inlining can
+prove it safe. For example, we would like this constructor to work:
+
+```simple
+struct Vec {
+    int    _max;
+    u8[~] !_buf; // Not-null, must be set before reading
+
+    new Vec = { ->
+        _buf = new u8[1];
+        clear(); // Would be safe after inlining; currently rejected
+    };
+    val clear = { ->
+        // Keep at most 1K of storage in a cleared Vec
+        if( _buf# > 1024 ) _buf = new u8[1024];
+        _max=0;
+    };
+};
+```
 
 ## Build and check
 
@@ -153,3 +197,6 @@ make tests CHAPTERS=chapter-construction CTAGS=
 defaults, completion errors, forward fields and methods, private loops, native
 execution, and ARM/RISC-V execution. The inherited language, memory, lattice,
 and backend suites run alongside it.
+`FinalConstructionTest` checks repeated assignments and loops over final fields,
+reads through methods, rejection of later writes, and native execution. It also
+checks that the loop's field Stores are outside the loop.