[SwayamInSync]

The 25 changes merged since 0.1.1 (#14 to #38) were documented in DESIGN.md and ARCHITECTURE.md, but on the website mostly by a sentence each, often only in the limitations page, and none in the release notes. This documents each one where a user looks for it, with a complete example and the output the verifier prints, and starts the 0.2.0 release notes.

Page	What it now shows
language/syntax.rst	One condition per clause: the error for a missing &&, and that 0.1.1 verified only the first condition
language/expressions.rst	Where quantifiers may appear, the error in executable code, and the loop to write instead
language/ghost-proofs.rst	A spec function rejected in a generic lambda; the exact values a spec reads, where 0.1.1 verified that 2147483647 + 1 read through a spec is negative
language/integers.rst	The C++17 and C++20 shift rules on one function; a new section on enumeration ranges (fixed and unfixed underlying types, conversions, specs)
language/pointers.rst	Out-parameters: what is Unresolved, what to write instead, and a read through a reference before any write; two null pointers differ by 0
language/dynamic-storage.rst	Arithmetic and spec calls on values read through pointers from new
language/functions-loops.rst	Loops that never repeat (do { } while (0) macros); what templates and member functions do today
language/limitations.rst	The error for an expression nested too deep
language/tooling.rst	Header inputs and compiler errors, Ctrl-C, the options that select a backend and the errors for unused ones, a source run beside its replay, encoding.failed, --jobs, cvc5 1.4, clang-format, and the constructs in Clang's own tools
book ch13, ch16, ch17	A call inside choose checked as recursion (0.1.1 verified a false claim with it); why a downgraded result is not [vacuous]; a pointer to the replay example
release-notes.rst	A 0.2.0 section: one entry per change, grouped into wrong results, failures that were not real, C++ that compiles now, running cpp-verify, and data formats

Every output on these pages is checked. check-doc-examples.py now also compares the errors and warnings a page shows after an example, apart from the location before each, and checks examples marked .. cppverify-example: rejects, which cpp-verify must report as an error. A #line 1 before each example makes a location inside a message count from the example's first line, as the reader sees it. Each of these makes the check fail: a shown error or warning with a changed word, an error example without rejects, and rejects on code that verifies. The existing pages all pass the stricter check.

Writing the pages also turned up one sentence that contradicted #18 (pointers.rst called null operands of a pointer difference "fail closed"); it now says which cases fail with a counterexample and which stop the file. The options section lists what is checked today: a Lean export still accepts the solver budgets it does not use, which a separate change fixes.

Testing: docs_examples.test checks 191 examples (43 against the output their pages show), 0 failed; docs_coverage.test passes; sphinx-build -W builds the site without warnings.