Three small spec corrections that surfaced during today's bug
burn-down audit:

- **#557** — `spec/03-slot-references.md` Example 9 (line 292)
  previously said the match-arm pattern binding "shadows the
  function parameter".  "Shadow" left undefined; two readings
  were equally consistent with the prose (replace vs push-on-top).
  The compiler implements push-on-top — the function parameter
  remains accessible at `@T.1` (`@T.2`, etc.) — which matches
  `let`'s rule but isn't derivable from the docs.  Replaced the
  one-liner with an explicit paragraph spelling out the
  push-on-binding semantics, the resulting De Bruijn ordering for
  multi-field constructors (leftmost = deepest = highest index,
  rightmost = shallowest), and the non-commutative-operations
  caveat that exposes the rule.

- **#561** — `spec/06-contracts.md` had two tier-accuracy bugs:
  - §6.3.1 (Tier 1 list) was missing "calls to pure functions
    that have their own contracts", and §6.3.2 (Tier 2 NYI list)
    incorrectly included it.  Pure-fn calls in `ensures` already
    verify at Tier 1 in v0.0.143 — the verifier inlines the
    callee's contract at the call site.  Same for `@T.result` and
    `if/then/else` in contracts, which similarly already work at
    Tier 1.  Moved all three from §6.3.2 to §6.3.1.
  - §6.3.3 said "Bounded quantification is decidable for finite
    bounds and is handled by Z3 via finite unrolling".  That
    reads as "Tier 1 decidable", but Tier 2 (the Z3-guided tier
    that would handle it) is [#427](NYI).  In practice every
    `forall`/`exists` in a contract falls to Tier 3 today.
    Clarified the prose to make this explicit, both for `forall`
    and `exists`.

- **#560** — the `invariant(...)` clause on `data` declarations
  is documented in `spec/02-types.md` §2.4.1, `spec/06-contracts.md`
  §6.2.3, and `SKILL.md`, but every documented form fails with
  `[E130] no <DataName> bindings in scope` at v0.0.143 (and at
  v0.0.127 when the issue was filed).  Added inline NYI markers
  at all three sites pointing at #560, with the working
  alternative (refinement types).  Added the limitation to
  spec/06-contracts.md's §6.9 Limitations table.

Allowlist line-number shifts auto-fixed via
`scripts/fix_allowlists.py --fix`, with one manual correction
to a duplicate-key collision the auto-fix introduced in
`scripts/check_skill_examples.py` (the known footgun: when the
fixer undercounts a multi-line edit, two adjacent entries can
collapse onto the same dict key — Python silently drops the
first).

Closes #557.
Closes #561.
Closes #560.

Co-Authored-By: Claude <noreply@anthropic.invalid>

PR #650's lint check (`check_changelog_updated.py`) was failing because
the original three-spec-fix commit didn't have a `[Unreleased]`
CHANGELOG entry — fixed here, and the scope is widened to bundle three
more aging small-docs issues that share the same shape.

Six closures now in one PR:

- **#557** (already in this PR): match-arm slot semantics "shadow" →
  "push-on-binding" in `spec/03-slot-references.md` Example 9.
- **#561** (already in this PR): Tier 1 vs Tier 2 vs Tier 3 accuracy
  in `spec/06-contracts.md` (pure-fn calls in ensures actually verify
  at Tier 1; quantifiers actually fall to Tier 3).
- **#560** (already in this PR): `invariant(...)` NYI markers in
  `spec/02 §2.4.1`, `spec/06 §6.2.3`, and `SKILL.md`.

New in this commit:

- **#607**: new `spec/02-types.md` §2.2.1 "`Int` and `Nat`
  compatibility" subsection covering the bidirectional subtyping
  (`Nat <: Int` always; `Int <: Nat` permitted with verifier-discharged
  obligation).  Plus a cross-reference paragraph in `SKILL.md`'s
  "Primitive types" listing telling agents not to insert `nat_to_int`
  defensively.
- **#608**: new `SKILL.md` "IO model: terminal vs browser" subsection
  under the Browser compilation section, explaining that programs
  using `IO.sleep` + ANSI escapes for terminal pacing/rendering
  compile cleanly to `--target browser` but render escapes as
  literal text and busy-wait the main thread.  Recommended pattern:
  "Vera pure simulation core + JS driver via `requestAnimationFrame`".
  `README.md`'s "write once, run anywhere" line qualified to
  acknowledge the IO seam.
- **#512**: all 31 Stage 11 rows in `HISTORY.md` (v0.0.112 → v0.0.138)
  trimmed to the canonical `**X** ([#N]).` template now embedded in
  long-term memory.  Detailed mechanism descriptions for each version
  stay in CHANGELOG under their respective `## [0.0.X]` section.

CHANGELOG: new `[Unreleased] / ### Documentation` section covering
all six closures with the rationale per fix.

Allowlist drift fixed via `scripts/fix_allowlists.py --fix` plus four
manual corrections for the known duplicate-key footgun
(`feedback_spec_allowlist.md`) — `scripts/check_skill_examples.py`
had four collapsed-key collisions after the auto-fix; lines 435
(Tuple), 1099 (HTML constructor match), 2092 (import aliasing),
2097 (import syntax) restored to their correct positions, plus line
1218 (Requires clause fragment) corrected from stale 1202.

All consistency checks green:
- `python scripts/check_doc_counts.py`
- `python scripts/check_spec_examples.py`
- `python scripts/check_skill_examples.py`
- `python scripts/check_limitations_sync.py`
- `python scripts/check_readme_examples.py`

Closes #557.
Closes #560.
Closes #561.
Closes #607.
Closes #608.
Closes #512.

Co-Authored-By: Claude <noreply@anthropic.invalid>

The lead sentence of the new `Int` and `Nat` compatibility subsection
used the word "implicitly", which set the wrong frame for Vera's
design principles.  "Implicit" suggests "silent and unchecked"; the
Int→Nat flow is actually "syntactically silent, semantically
verified" — the verifier emits a proof obligation and Z3 discharges
it (or it falls to a runtime check).

Reworded the lead to make the verifier's mediating role explicit:

  Vera's type checker accepts both flows without an explicit cast —
  but the narrowing direction (Int <: Nat) is not unchecked: the
  type checker emits a verification obligation that the contract
  verifier discharges via Z3, so the flow is syntactically silent
  but semantically verified.  This matches Vera's "verification is
  a first-class citizen" design point: subtyping that can be proved
  doesn't need to be spelled out at every call site.

Also changed "The conversion is implicit and either statically
verified or guarded at runtime" to "The conversion is syntactically
silent and either statically verified or guarded at runtime" for
the same reason.

Bullets and rest of subsection unchanged — they were already
accurate (explicitly named "verifier-discharged" and "Tier 1"/"Tier 3"
mechanics).

Co-Authored-By: Claude <noreply@anthropic.invalid>

The reword for #608 strengthened the parity claim to "for all
language constructs" — which is immediately contradicted by the
next sentence describing the IO seam.  CodeRabbit-flagged.

Tightened to "for the pure-language surface (arithmetic, ADTs,
pattern matching, closures, contracts, effects-as-host-imports,
etc.)" — accurate and naturally segues into the IO-exception
paragraph that follows.  Also reframed "The IO surface differs
between targets" to "The IO surface is the documented exception"
so the structural relationship between the two sentences is
explicit rather than implied.

Co-Authored-By: Claude <noreply@anthropic.invalid>

The implementation note on `Int <: Nat` referenced "Section 2.1"
as the home of the `Nat <: Int` rule.  When the #607 work created
the new §2.2.1 "`Int` and `Nat` compatibility" subsection, the
pointer became stale — §2.1 is just the high-level Overview, while
the formal subtyping rules now live in §2.2.1.

Updated the pointer to §2.2.1.

(CodeRabbit said "around line 28-37" in the finding text; the
actual reference is at line 277.  Verified by grep — no other
"Section 2.1" pointers exist in the file that mention the
Int/Nat relationship.)

Co-Authored-By: Claude <noreply@anthropic.invalid>

… tier

Filed during PR #650's review pass — an audit of the spec found
~10 sites where the documented language behaviour contradicts the
spec's own foundational principles in §0.2 (Explicitness) and §0.3
(no shorthand / no implicit conversions / no default arguments).

Examples: the implicit prelude (§9.1.2), `effects(pure)` default on
function types (§2.5), multiple `requires` clauses being equivalent
to a single `requires` with && (§5.4), `@Fn<A,B>.0` shorthand (§3.7),
ability auto-derivation, implicit `resume` binding inside handler
arms, IO operations available without a user-side `effect IO` block,
optional `module` statement.

Recommendation in the issue body: Option 1 — strengthen §0.3 to
enumerate the deliberate implicit surfaces as exceptions (one PR,
honest framing, no behaviour change), then file individual triage
PRs for items where the implicitness is unfixed legacy rather than
load-bearing design.

Stabilisation-tier rather than enhancement because LLMs reading the
spec take §0.2.2 literally — internal inconsistency is a real
confusion source, not cosmetic.

Co-Authored-By: Claude <noreply@anthropic.invalid>

…invariant claim (CodeRabbit valid)

Two findings, both valid:

**Finding 1 — §2.4.1 line 149 contradicts the NYI block above it.**

The line "The invariant is checked by the contract verifier at
every construction site." is in present tense and asserts as fact
something that's directly contradicted by the "Status: Not yet
implemented" callout earlier in the same subsection.  Reworded to
future tense ("When implemented, the invariant will be checked...")
and made the present-day fact explicit ("At present...no checking
occurs and refinement types (§2.6) are the working alternative").

**Finding 2 — §2.2.1 calls Int↔Nat "subtypes of each other" but
§2.8's formal subtyping relation only includes Nat <: Int.**

§2.8 already documents Int <: Nat correctly as an
"Implementation note" sitting alongside (not inside) the formal
relation rules 1–5, which explicitly say "no other subtyping" at
rule 5.  But §2.2.1 was phrased as if Int <: Nat is a peer
subtyping rule, creating cross-section inconsistency.

Reworded §2.2.1 to mirror §2.8's framing exactly:

- `Nat <: Int` is a **formal subtyping rule** — it follows from
  refinement subtyping (§2.6.2, §2.8 rule 3).  No proof obligation,
  no runtime check.
- `Int -> Nat` is **not a formal subtyping rule** (explicitly
  excluded by §2.8 rule 5).  Instead it's a **verifier-mediated
  relaxation**: type checker permits the flow + emits a
  verification obligation + Tier 1 verifier discharges via Z3 (or
  falls to Tier 3 runtime check).

Added cross-references in both directions (§2.2.1 → §2.8 rule 3
and §2.8 rule 5; §2.8's implementation note already references
§2.2.1 from a previous commit on this PR).  Added an explicit
note tying the distinction to §0.2.2 ("no implicit behaviour"):
the formal subtyping rule is a logical consequence of refinement
subtyping (not implicit), and the verifier-mediated relaxation is
syntactically silent but semantically verified (the verifier is
the explicit check, not the syntax).

Co-Authored-By: Claude <noreply@anthropic.invalid>