Factor out doc/note/bounds-checking.md
diff --git a/doc/note/bounds-checking.md b/doc/note/bounds-checking.md
new file mode 100644
index 0000000..2ef7507
--- /dev/null
+++ b/doc/note/bounds-checking.md
@@ -0,0 +1,32 @@
+# Bounds Checking
+
+For a slice or array `x`, an expression like `x[i .. j]` is invalid unless the
+compiler can prove that `((0 <= i) and (i <= j) and (j <= x.length()))`. For
+example, the expression `x[..]` is always valid because the implicit `i` and
+`j` values are `0` and `x.length()`, and a slice or array cannot have negative
+length.
+
+Similarly, an expression like `x[i]` is invalid unless there is a compile-time
+proof that `i` is in bounds: that `((0 <= i) and (i < x.length()))`. Proofs can
+involve natural bounds (e.g. if `i` has type `base.u8` then `(0 <= i)` is
+trivially true since a `base.u8` is unsigned),
+[refinements](/doc/glossary.md#refinement-type) (e.g. if `i`has type
+`base.u32[..= 100]` then 100 is an upper bound for `i`) and [interval
+arithmetic](/doc/note/interval-arithmetic.md) (e.g. for an expression like
+`x[m + n]`, the upper bound for `m + n` is the sum of the upper bounds of `m`
+and `n`).
+
+For example, if `a` is an `array[1024] base.u8`, and `expr` is some expression
+of type `base.u32`, then `a[expr & 1023]` is valid, because the bitwise-and
+means that the overall index expression is in the range `[0 ..= 1023]`,
+regardless of `expr`'s range.
+
+Proofs can also involve [facts](/doc/note/facts.md), dynamic constraints that
+are not confined to the type system. For example, when the if-true branch of an
+`if i < j { etc }` statement is taken, that `(i < j)` fact could combine with
+another `(j <= x.length())` fact to deduce that `(i < x.length())` when inside
+that if-true branch (but not necessarily outside of that if statement).
+
+Wuffs does not have dependent types. Dependent types are one way to enforce
+bounds checking, but they're not the only way, and there's more to programming
+languages than their type systems.
diff --git a/doc/note/slices-arrays-and-tables.md b/doc/note/slices-arrays-and-tables.md
index 5fc308c..0b5d92b 100644
--- a/doc/note/slices-arrays-and-tables.md
+++ b/doc/note/slices-arrays-and-tables.md
@@ -22,6 +22,9 @@
 implicitly equalling zero. `j` can be omitted, implicitly equalling the length.
 For example, `s[.. 5]` contains the first five elements of `s`.
 
+Sub-expressions, whether a single element like `s[i]` or a sub-slice of
+elements like `a[i .. j]`, are [bounds checked](/doc/note/bounds-checking.md).
+
 
 ## Tables
 
@@ -47,35 +50,3 @@
 
 Lengths, widths, heights and strides are all measured in number of elements,
 even when an element occupies multiple bytes.
-
-
-## Bounds Checking
-
-An expression like `x[i .. j]` is invalid unless the compiler can prove that
-`((0 <= i) and (i <= j) and (j <= x.length()))`. For example, the expression
-`x[..]` is always valid because the implicit `i` and `j` values are `0` and
-`x.length()`, and a slice or array cannot have negative length.
-
-Similarly, an expression like `x[i]` is invalid unless there is a compile-time
-proof that `i` is in bounds: that `((0 <= i) and (i < x.length()))`. Proofs can
-involve natural bounds (e.g. if `i` has type `base.u8` then `(0 <= i)` is
-trivially true since a `base.u8` is unsigned), refinements (e.g. if `i`has type
-`base.u32[..100]` then 100 is an upper bound for `i`) and [interval
-arithmetic](/doc/note/interval-arithmetic.md) (e.g. for an expression like
-`x[m + n]`, the upper bound for `m + n` is the sum of the upper bounds of `m`
-and `n`).
-
-For example, if `a` is an `array[1024] base.u8`, and `expr` is some expression
-of type `base.u32`, then `a[expr & 1023]` is valid, because the bitwise-and
-means that the overall index expression is in the range `[0..1023]`, regardless
-of `expr`'s range.
-
-Proofs can also involve [facts](/doc/note/facts.md), dynamic constraints that
-are not confined to the type system. For example, when the if-true branch of an
-`if i < j { etc }` statement is taken, that `(i < j)` fact could combine with
-another `(j <= x.length())` fact to deduce that `(i < x.length())` when inside
-that if-true branch (but not necessarily outside of that if statement).
-
-Wuffs does not have dependent types. Dependent types are one way to enforce
-bounds checking, but they're not the only way, and there's more to programming
-languages than their type systems.
diff --git a/doc/note/zero-initialization.md b/doc/note/zero-initialization.md
index fcf28f4..9dc0119 100644
--- a/doc/note/zero-initialization.md
+++ b/doc/note/zero-initialization.md
@@ -20,8 +20,7 @@
 With or without this flag bit set, the Wuffs compiler still enforces bounds and
 arithmetic overflow checks. It's just that for potentially-uninitialized struct
 fields, the compiler has weaker starting assumptions: their numeric types
-cannot be
-[refined](https://github.com/google/wuffs/blob/master/doc/glossary.md#refinement-type).
+cannot be [refined](/doc/glossary.md#refinement-type).
 
 Even with this flag bit set, the Wuffs standard library also considers reading
 from an uninitialized buffer to be a bug, and strives to never do so, but
@@ -36,8 +35,7 @@
 improvement on micro-benchmarks, mostly noticable (in relative terms) only when
 the actual work to do (the input) is also small. Look for
 `WUFFS_INITIALIZE__LEAVE_INTERNAL_BUFFERS_UNINITIALIZED` in the
-[benchmarks](https://github.com/google/wuffs/blob/master/doc/benchmarks.md) for
-performance numbers.
+[benchmarks](/doc/benchmarks.md) for performance numbers.
 
 In Wuffs code, a struct definition has two parts, although the second part's
 `()` parentheses may be omitted if empty: