docs: README — the universal verified primitive basis (Stages 1-6) (#78)

The language grew from bounded slice algorithms to a composable verified basis,
each stage L3 end-to-end: (1) recursive ADTs (struct/enum/Box/match), (2) recursion
schemes (fold/map/for_all + the fold_bound prove-once multiplier), (3) effect-
primitive stdlib (sandboxed #[boundary] primitives + outcome-coverage), (4) bounded
Vec (no-OOB get + capacity-preserving push), (5) compositional reasoning (verify-
through + honest min-aggregation), (6) security-by-construction / IFC (Tainted/
Secret/Authorized + #[sealed] clean types -> SQLi/secret-leak/missing-authz
un-typeable; the careless path doesn't compile). Headline + a Stages-1-6 bullet +
the v1.1 deferral list (dataflow taint-propagation, Map, Vec element-invariants,
scheme fusion, the runnable foreign-syscall link).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: dollspace-gay

README.md

@@ -32,7 +32,7 @@ See [`thermite-design.md`](./thermite-design.md) for the full design (thesis, su
 
 ## Status
 
-**v0.1–v0.5 complete — the toolchain runs end-to-end.** A Thermite program goes from source to a verified, **runnable, contract-checked native binary**. Both corpus programs certify **L3 in real Verus** and **L2 in real Kani**; every soundness invariant has been adversarially verified by the ACToR critic loop, and the toolchain's soundness-critical core is **itself Verus-verified** (`thermite-verified`).
+**v0.1–v0.5 complete + the universal verified primitive basis (Stages 1–6) — the toolchain runs end-to-end.** A Thermite program goes from source to a verified, **runnable, contract-checked native binary**. The language now expresses **recursive data, folds, bounded collections, effects, composition, and security-by-construction** — every corpus program across the six basis stages certifies **L3 in real Verus** (L2 in real Kani). Every soundness invariant has been adversarially verified by the ACToR critic loop, and the toolchain's soundness-critical core is **itself Verus-verified** (`thermite-verified`).
 
 - ✅ **Frontend** (`thermite-syntax`) — lexer, recovering per-item parser, AST (literals keep verbatim text), stable semantic addressing
 - ✅ **SpecTherm** (`thermite-spec`) — the frozen bounded-combinator registry + the cage validator (no anonymous nested quantifiers; closure bodies are flat predicates)
@@ -42,7 +42,14 @@ See [`thermite-design.md`](./thermite-design.md) for the full design (thesis, su
 - ✅ **Boundaries** — crates.io FFI + `#[slag]` modules, L1-enforced and runtime-confined to their declared `fx`; the manifest distinguishes *verified-to-the-boundary* from *verified, period*; a caller verifies **through** a boundary's contract (composition)
 - ✅ **`THERMITE.skill.md`** — the whole language in ≤ 6,000 tokens, regenerated from the registry, CI-gated; concurrency-safe multi-agent sessions
 - ✅ **Self-verification** (`thermite-verified`) — the soundness-critical pure core is itself **Verus-verified** (`verus --no-cheating`, no `assume`/`external_body` on the core): effect subsumption, the degrade anti-cheat (a counterexample never degrades), the seccomp allowlist (pure → no I/O + monotonicity), the boundary honesty gate (a regular fn is never laundered to L3), project-level aggregation (no over-claim), and the mutation 0/0 floor. Each is anchored to its production consumer by exhaustive/observable equivalence. The toolchain shrinks its own TCB.
-- 🔭 Deferred (tracked, crosslink #21): direct MIR-level lowering (we transpile to Rust, which rustc takes to MIR) and the incremental goal-state REPL
+- ✅ **Universal verified primitive basis** (`.design/basis/`, Stages 1–6) — the surface grew from bounded slice algorithms to a *composable* basis, each stage certifying **L3 end-to-end** in real Verus:
+  1. **Recursive ADTs** — `struct` (with `inv` type-invariants), `enum`, recursive types via `Box<T>`, and exhaustive `match` (a missed variant is a compile-time reject — the "handled-or-loud" tooth).
+  2. **Recursion schemes** — `fold`/`map`/`for_all`/`exists` over the ADTs, with the `fold_bound` *prove-once* induction law: an instance proves its bound by citing the law, no fresh induction.
+  3. **Effect-primitive stdlib** — each effect atom (`read`/`write`/`net`/`time`/…) a contracted, seccomp-confined `#[boundary]` primitive; outcome-coverage forces every `Result` arm handled.
+  4. **Bounded collections** — `Vec<T>` over verified vstd, with a no-OOB `get` (`req i < len`) and a capacity-preserving `push`.
+  5. **Compositional reasoning** — a caller verifies *through* its callees' contracts (no re-proof); project assurance aggregates as the honest **min** over parts; the TCB is enumerable.
+  6. **Security-by-construction (IFC)** — `Tainted`/`Secret`/`Authorized` marked types + `#[sealed]` clean types whose **only** producer is their `#[boundary]` door (`parameterize`/`declassify`/`authorize`). SQL injection, secret leaks, and missing-authorization are **un-typeable — the careless path does not compile.**
+- 🔭 Deferred (tracked): direct MIR-level lowering + the incremental goal-state REPL (crosslink #21); and the basis v1.1 layer — full dataflow taint-propagation, `Map`, `Vec` element-invariants, scheme fusion, and the runnable foreign-syscall link.
 
 Roadmap (all shipped): v0.1 kernel → v0.2 Kani-backed L2 + degrade protocol → v0.3 mutation/vacuity battery → v0.4 crates.io FFI boundary → v0.5 background proof-repair + multi-agent sessions, plus `forge build` (runnable binaries) and the runtime seccomp sandbox. Progress is tracked in crosslink (milestones #1–#5 closed).