Rewrite Core language reference and add transforms doc (#1084)

## Summary

- Rewrites `LangDefDoc.lean` as a proper 5-section language reference:
Introduction, Lambda (syntax + type system), Imperative (commands,
statements, KleeneStmt, metadata), Strata Core (expressions, built-in
types, built-in operators, type declarations, ADTs, functions, recursive
functions, axioms, commands, procedures, programs), and Semantics
(Lambda operational + denotational, command, statement, KleeneStmt).
- Adds `TransformsDoc.lean` documenting program transforms (`strata
transform` CLI), analysis modes, and the SMT analysis pipeline.
- Adds missing docstrings to `CmdExt`, `CallArg`, `Decl`, `Program`,
`LSort`, `StepKleene`, and `StepKleeneStar` in the source.
- Adds deprecation notes to `Datatypes.md`, `RecursiveFunctions.md`, and
`VerificationModes.md` pointing to the canonical Verso docs.
- Cross-document links point to rendered HTML output rather than GitHub
source files.

---------

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Mikael Mayer <mimayere@amazon.com>

Author: 3 people

Strata/DL/Imperative/KleeneStmtSemantics.lean

@@ -52,6 +52,7 @@ section
 
 variable {CmdT : Type} (P : PureExpr) [HasBool P] [HasNot P]
 
+/-- A single execution step for non-deterministic (Kleene) statements. -/
 inductive StepKleene
   (EvalCmd : EvalCmdParam P CmdT) :
   KleeneConfig P CmdT → KleeneConfig P CmdT → Prop where
@@ -113,6 +114,8 @@ end
 
 /-! ## Multi-step relation -/
 
+/-- Multi-step execution for non-deterministic statements: the reflexive,
+transitive closure of `StepKleene`. -/
 abbrev StepKleeneStar (P : PureExpr) [HasBool P] [HasNot P]
     (EvalCmd : EvalCmdParam P CmdT) :
     KleeneConfig P CmdT → KleeneConfig P CmdT → Prop :=

Strata/DL/Lambda/Denote/LExprDenote.lean

@@ -33,7 +33,9 @@ namespace Lambda
 variables. We use a separate type rather than `LMonoTy` to avoid carrying
 around proofs that a type has no type variables. -/
 public inductive LSort where
+  /-- A named type constructor applied to sort arguments. -/
   | tcons (name : String) (args : List LSort)
+  /-- A bit vector sort of the given size. -/
   | bitvec (size : Nat)
 
 def LSort_eqb (s1 s2: LSort) : Bool :=

Strata/Languages/Core/Program.lean

@@ -45,12 +45,17 @@ A Strata Core declaration.
 Note: constants are 0-ary functions.
  -/
 inductive Decl where
+  /-- A type declaration (abstract type, type synonym, or algebraic datatype). -/
   | type (t : TypeDecl) (md : MetaData Core.Expression)
+  /-- An axiom declaration. -/
   | ax   (a : Axiom) (md : MetaData Core.Expression)
-  -- The following is temporary, until we have lists and can encode `distinct` in Lambda.
+  /-- A `distinct` assertion: the given expressions are pairwise distinct. -/
   | distinct (name : Expression.Ident) (es : List Expression.Expr) (md : MetaData Core.Expression)
+  /-- A procedure declaration. -/
   | proc (d : Procedure) (md : MetaData Core.Expression)
+  /-- A function declaration. -/
   | func (f : Function) (md : MetaData Core.Expression)
+  /-- A mutually recursive function block. -/
   | recFuncBlock (fs : List Function) (md : MetaData Core.Expression)
   deriving Inhabited
 
@@ -159,8 +164,9 @@ def Decl.formatWithMetaData (decl : Decl) : Format :=
 
 @[expose] abbrev Decls := List Decl
 
-/-- A Core.Program -/
+/-- A Core.Program is an ordered list of declarations. -/
 structure Program where
+  /-- The declarations that make up this program. -/
   { decls : Decls }
 
 @[expose]

Strata/Languages/Core/Statement.lean

@@ -29,15 +29,20 @@ A call argument is either an input expression, an in-out variable, or an
 output variable.
 -/
 inductive CallArg (P : PureExpr) where
+  /-- An input argument: a by-value expression. -/
   | inArg (e : P.Expr)
+  /-- An input-output argument: a mutable variable passed by reference. -/
   | inoutArg (id : P.Ident)
+  /-- An output-only argument: a variable whose final value is returned to the caller. -/
   | outArg (id : P.Ident)
 
 /--
 Extend Imperative's commands by adding a procedure call.
 -/
 inductive CmdExt (P : PureExpr) where
+  /-- A standard imperative command. -/
   | cmd (c : Imperative.Cmd P)
+  /-- A procedure call with the given name and arguments. -/
   | call (procName : String) (args : List (CallArg P))
          (md : MetaData P)
 

docs/Datatypes.md

@@ -1,3 +1,7 @@
+> **Note:** The canonical reference for datatypes is now the
+> [Strata Core Language Definition](verso/LangDefDoc.lean) (Section 4, "Type Declarations").
+> This file is retained for additional detail not yet migrated. It may be removed in the future.
+
 # Datatypes in Strata
 
 This document describes the datatype system in Strata Core.

docs/RecursiveFunctions.md

@@ -1,3 +1,8 @@
+> **Note:** The canonical reference for recursive function syntax is now the
+> [Strata Core Language Definition](verso/LangDefDoc.lean) (Section 4, "Recursive Functions").
+> SMT encoding details are in [Transforms and Analysis](verso/TransformsDoc.lean).
+> This file is retained for additional detail not yet migrated. It may be removed in the future.
+
 # Recursive Functions in Strata
 
 This document describes the recursive function infrastructure in Strata Core.

docs/VerificationModes.md

@@ -1,3 +1,8 @@
+> **Note:** The canonical reference for verification modes is now
+> [Transforms and Analysis](verso/TransformsDoc.lean).
+> This file is retained for the detailed error classification table not yet migrated.
+> It may be removed in the future.
+
 # Verification Modes
 
 Strata supports three verification modes, selected via `--check-mode`: