docs(design): bring models/0007 worked examples onto the shipped surface (refs #7)

The raw-buf milestone fieldtest (spec 0066) surfaced a spec_gap: the
kernel-extensions whitepaper teaches RawBuf surface syntax through its
§Series worked examples, but those examples were written before three
downstream surface decisions landed and never caught up — so an LLM
author who pattern-matches them writes programs that fail to parse.
Three drift classes, all verified against the HEAD parser:

- fn-type slots carried no mode. Post-#55 every value slot needs an
  explicit `(own …)` / `(borrow …)` (the bare_slot_reject contract).
- `(new RawBuf lookback)` omitted the element type. Post-#51 the form
  is `(new RawBuf (con T) <size>)`; the whitepaper's own spec line
  (§"allocates") already documents `(new RawBuf (con T) (size: Int))`.
- parametrised kernel types were spelled bare `(Series a)` /
  `(Series (con Float))`, contradicting the whitepaper's OWN prose
  (`(con Series (con Float))` at the §mechanisms section). Wrapped in
  `(con …)` to match the documented canonical form.
- `len` / `total_count` carried no `(type …)` at all; completed from
  the obvious neighbour signatures (`borrow (con Series a) → own Int`).

Scope is deliberately surface-syntax only. The §Series listing stays a
forward-looking sketch of the still-pending library-extension milestone
(STATUS header; "not in today's AILang" at the sma_demo block). Its
full cross-module compile-verification remains assigned to the Series
milestone per spec 0059 — these edits do not claim it compiles today
(it leans on kernel-tier polymorphism that is not yet authorable), only
that its surface syntax now matches what RawBuf authors must actually
write.

design/models/0007-kernel-extensions.md

@@ -58,8 +58,8 @@ moving average over a stream of float values, window size 3":
 
   (fn sum_window_step
     (type (fn-type
-      (params (borrow (Series (con Float))) (con Int) (con Int) (con Float))
-      (ret (con Float))))
+      (params (borrow (con Series (con Float))) (own (con Int)) (own (con Int)) (own (con Float)))
+      (ret (own (con Float)))))
     (params s n i acc)
     (body
       (if (app eq i n)
@@ -70,8 +70,8 @@ moving average over a stream of float values, window size 3":
 
   (fn emit_if_full
     (type (fn-type
-      (params (borrow (Series (con Float))) (con Int))
-      (ret (con Unit)) (effects IO)))
+      (params (borrow (con Series (con Float))) (own (con Int)))
+      (ret (own (con Unit))) (effects IO)))
     (params s n)
     (body
       (if (app >= (app Series.total_count s) n)
@@ -82,8 +82,8 @@ moving average over a stream of float values, window size 3":
 
   (fn run_stream
     (type (fn-type
-      (params (own (Series (con Float))) (con Int) (con FloatList))
-      (ret (con Unit)) (effects IO)))
+      (params (own (con Series (con Float))) (own (con Int)) (own (con FloatList)))
+      (ret (own (con Unit))) (effects IO)))
     (params s n input)
     (body
       (match input
@@ -94,7 +94,7 @@ moving average over a stream of float values, window size 3":
               (tail-app run_stream s_new n rest)))))))
 
   (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
     (params)
     (body
       (let s (new Series (con Float) 3)
@@ -117,7 +117,7 @@ maps onto one of the four mechanisms this whitepaper defines:
   construct*.
 - `(app Series.at s i)`, `(app Series.total_count s)`,
   `(app Series.push s v)` — *type-scoped namespacing*.
-- The `(own (Series ...))` mode on `run_stream` plus the linear
+- The `(own (con Series ...))` mode on `run_stream` plus the linear
   state-threading via `(let s_new ...)` is the *uniqueness mode*
   discipline that already exists in AILang. Series carries no
   separate algebraic effect; its mutation is mode-tracked, not
@@ -453,17 +453,17 @@ handles allocation, drop, and copy-on-share.
 
   (fn new
     (type (fn-type
-      (params (con Int))
-      (ret (own (Series a)))))
+      (params (own (con Int)))
+      (ret (own (con Series a)))))
     (params lookback)
     (body
       (term-ctor Series S
-        (new RawBuf lookback) lookback 0 0 0)))
+        (new RawBuf (con a) lookback) lookback 0 0 0)))
 
   (fn push
     (type (fn-type
-      (params (own (Series a)) (con a))
-      (ret (own (Series a)))))
+      (params (own (con Series a)) (own (con a)))
+      (ret (own (con Series a)))))
     (params s v)
     (body
       (match s
@@ -477,8 +477,8 @@ handles allocation, drop, and copy-on-share.
 
   (fn at
     (type (fn-type
-      (params (borrow (Series a)) (con Int))
-      (ret (con a))))
+      (params (borrow (con Series a)) (own (con Int)))
+      (ret (own (con a)))))
     (params s i)
     (body
       (match s
@@ -487,10 +487,16 @@ handles allocation, drop, and copy-on-share.
             (app % (app + (app - head 1) (app + (app * lookback 2) i)) lookback))))))
 
   (fn len
+    (type (fn-type
+      (params (borrow (con Series a)))
+      (ret (own (con Int)))))
     (params s)
     (body (match s (case (pat-ctor S buf lookback head count total) count))))
 
   (fn total_count
+    (type (fn-type
+      (params (borrow (con Series a)))
+      (ret (own (con Int)))))
     (params s)
     (body (match s (case (pat-ctor S buf lookback head count total) total)))))
 ```