Support docstrings on DSL components

REUSE.md

@@ -5,8 +5,67 @@ law in a construction, identify its declaration, owner, parameters, domain and s
 Use the live declaration to check the fit. The map below supplies starting points, not a list
 of interchangeable objects.
 
-Ideal systems, schemes and constructions are in `Commons`; typed systems, converters and games
-are in `SystemAlgebra`. The probability operations below are in `Probability.Distribution`.
+Ideal systems and schemes are in `Commons`; specifications and constructions are in
+`ConstructiveCryptography`. Typed systems, converters and games belong to the `RandomSystems`
+library, namespace `SystemAlgebra`. The probability operations below are in
+`Probability.Distribution`.
+
+## Start from the type you need
+
+For a definition, choose a constructor by its return type. A `by` block is optional:
+`:= expression` and `:= by exact expression` supply the same object.
+
+**A law, `ProbDist Y`.** For `P : ProbDist X` and `f : X → Y`, `P.map f` is the normalized
+law of `f(x)`. `P.bind K` samples from `K x` after drawing `x`; `prodProbDist P Q` draws
+independently. `𝒰[X]` is already normalized. The raw operations `fTransform`, `bindK` and `prod`
+return `Distribution`, so their results do not directly fill a `ProbDist` goal.
+
+**A source, `TypedSystem A`.** The interface `A` determines which constructor fits.
+For a reply law `P : ProbDist Y`:
+
+- `TypedSystem.source P q` returns `TypedSystem (Interface.source Y q)`.
+  It uses the port `()` and a scalar allowance `q : ℕ`.
+- `MemorylessSource.perPort Y P (budget := b)` returns
+  `TypedSystem (Evaluation.perPort Unit Y b)`. It uses the port `.eval`;
+  `b : Evaluation.Port → ℕ` gives its allowance. `fun _ => q` assigns `q` to that sole port.
+
+Both draw afresh on each call. Their port types and domain presentations differ, so their
+return types must be matched explicitly. `TypedSystem.sample P R`, with
+`R : Y → TypedSystem A`, draws `y` once and behaves as `R y` throughout the interaction.
+
+**A converter, `TypedConverter A B`.** It exposes `A` and uses a system on `B`, so
+`α • R : TypedSystem A` when `R : TypedSystem B`. Reuse a stock converter with the required
+contract. For fresh evaluation replies, import `Commons.Definitions.ReplyTransform` and use:
+
+```lean
+-- f : X → Y; b : Evaluation.Port → ℕ
+Evaluation.mapReplies f b :
+  TypedConverter (Evaluation.perPort Unit Y b) (Evaluation.perPort Unit X b)
+-- P : ProbDist K; f : K → X → Y
+Evaluation.sampleReplies P f b :
+  TypedConverter (Evaluation.perPort Unit Y b) (Evaluation.perPort Unit X b)
+```
+
+Both make one inside call per outside call. `mapReplies` returns `f x`; `sampleReplies` draws
+`k ∼ P` afresh and returns `f k x`. Their contracts `mapReplies_smul_memorylessSource` and
+`sampleReplies_smul_memorylessSource` rewrite attachment to
+`MemorylessSource.perPort X Q (budget := b)` into sources of `Q.map f` and
+`(prodProbDist P Q).map (fun kx => f kx.1 kx.2)` respectively.
+Use `ProbDist.map_map`, `prodProbDist_map_left`, `prodProbDist_map_right` and
+`prodProbDist_uniform` for the remaining normalized-law equations.
+
+For a custom component, write a DSL `converter` declaration beside your definitions,
+then use its generated term. Put a short `/-- ... -/` input/output rule before it; the same
+documentation appears on the component and its `.perPort` and `.exact` forms, when generated.
+Declarations go outside `by`.
+The [declaration grammar](src/ConstructiveCryptography/DSL/GRAMMAR.md#grammar) and
+[budget forms](src/ConstructiveCryptography/DSL/GRAMMAR.md#interfaces-budgets-and-obligations)
+give the syntax and the types of `.perPort` and the other generated terms.
+
+Use `#check Name` or Go to Definition to inspect the full constructor signature, including its
+named `budget` argument. The object index below supplies owners for those declarations.
+
+## Object index
 
 | Needed object | Declaration and module |
 | --- | --- |
@@ -45,6 +104,9 @@ are in `SystemAlgebra`. The probability operations below are in `Probability.Dis
 | Nonce/AD encrypt-then-MAC | `nonceEncryptThenMAC` in [NonceEncryptThenMAC] |
 | Restricted interface | `TypedConverter.filter` in [Filter] |
 | Relabeled interface | `TypedConverter.rename` in [Relabel] |
+| Deterministic reply map | `Evaluation.mapReplies` in [ReplyTransform] |
+| Fresh randomized reply map | `Evaluation.sampleReplies` in [ReplyTransform] |
+| Reply map on an arbitrary input domain | `TypedConverter.mapReplies` in [QueryRouting] |
 | One-query input and reply translation | `TypedConverter.routing` in [QueryRouting] |
 | Shared access by tagged callers | `routing` in [QueryRouting], `smul_sample` in [Functional] |
 
@@ -216,3 +278,5 @@ component mathematics explicit. They do not choose the objects, their ownership
 Compile the focused probes, run the changed-file linters, then the full build and source/axiom
 checks in [AGENTS.md](AGENTS.md). These checks establish the Lean claims; reuse and modeling
 still require reading the definitions.
+
+[ReplyTransform]: src/Commons/Definitions/ReplyTransform.lean

src/ConstructiveCryptography/DSL/Elaborator.lean

@@ -23,7 +23,9 @@ first invocation. Named `outside` components `a : A`, `b : B`, `c : C` give the
 A converter gets its inferred per-call bound `C.bound` and an inside allowance
 of `C.bound` times its outside interface's bound, plus the exact arrow `C.exact` when its number of
 inside calls is a function of the input; a filter is the arrow from the restricted budget.
-System definitions take their budget from their outermost component. The compiler is a front end
+System definitions take their budget from their outermost component. Leading docstrings are
+attached to the public declaration and its generated per-port and exact forms.
+The compiler is a front end
 on the category of interfaces: systems are `TypedSystem`s, and converters, built from
 `TypedConverter.ofProgram` and its variants, are declared as arrows `A ⟶ B` of
 `Interface.category`, so that components assemble with `≫` and `⊗ₘ`.
@@ -989,13 +991,36 @@ def elabComponentEquations (name : Ident) (params : Array (TSyntax ``Term.bracke
         ($state : $stateTy) ($input : ($outer).X $label) :
         $step $args* $state $label $input using $step:ident))
 
+/-- Split a component command into its optional documentation and declaration body. -/
+def componentDocAndBody
+    -- `stx` is a system or converter command, with its optional docstring as the first field.
+    (stx : Syntax) : Option (TSyntax `Lean.Parser.Command.docComment) × Syntax :=
+  (if stx[0].isNone then none else some ⟨stx[0][0]⟩,
+    stx.modifyArgs (fun args => args.extract 1 args.size))
+
+/-- Document the component and its `.perPort` and `.exact` forms, when generated. -/
+def addComponentDocStrings
+    -- `name` identifies the component in the current namespace.
+    (name : Ident)
+    -- `params` supplies its binders to Lean's documentation elaborator; `doc` is the user's text.
+    (params : Array (TSyntax ``Term.bracketedBinder))
+    (doc : Option (TSyntax `Lean.Parser.Command.docComment)) : CommandElabM Unit := do
+  let some doc := doc | return
+  let owner := (← getCurrNamespace) ++ name.getId
+  for suffix in [Name.anonymous, `perPort, `exact] do
+    let decl := owner ++ suffix
+    if (← getEnv).contains decl then
+      liftTermElabM <| Lean.addDocString decl (mkNullNode (params.map (·.raw))) doc
+
 /-- A system or converter declaration. Its outside interface is the annotation, the ordered
 tensor of its named `outside` components, or its generated ports; an annotation and named
 components exclude each other. The private state of `initialize`, samples included, is shared
 by every procedure, whichever component it is on. -/
 @[command_elab systemComponentDecl, command_elab systemComponentTypedDecl,
   command_elab converterDecl, command_elab converterTypedDecl]
 def elabComponent : CommandElab := fun stx => do
+  -- Field indices below refer to the declaration body, after its optional docstring.
+  let (doc, stx) := componentDocAndBody stx
   let before ← getEnv
   let beforeErrors ← errorCount
   checkReserved stx
@@ -1113,6 +1138,7 @@ def elabComponent : CommandElab := fun stx => do
     if (← errorCount) == beforeErrors then
       elabComponentEquations name params σ oracles stateTy none
       registerComponentDefinitions name before
+      addComponentDocStrings name params doc
     return
   let (innerZero, _, calls) ← componentInside converting insides sites used (← `(0))
   let resultOf (resultType : TSyntax `term) : CommandElabM (TSyntax `term) :=
@@ -1133,6 +1159,7 @@ def elabComponent : CommandElab := fun stx => do
     elabExactDecls name params σ insides used oracles bodies calls input
   if (← errorCount) == beforeErrors then
     registerComponentDefinitions name before
+    addComponentDocStrings name params doc
 
 /-- A domain filter: forward the queries whose input history is admitted, and stop on the
 others. -/
@@ -1191,6 +1218,8 @@ partial def isConverterExpr (e : TSyntax `term) : Bool :=
 and `D` takes that family's budget, `BudgetOf D.outer`, so a tuple when the component has named
 outside components. -/
 @[command_elab systemDecl] def elabSystem : CommandElab := fun stx => do
+  -- Field indices below refer to the declaration body, after its optional docstring.
+  let (doc, stx) := componentDocAndBody stx
   let before ← getEnv
   let beforeErrors ← errorCount
   checkReserved stx
@@ -1219,5 +1248,6 @@ outside components. -/
     elabCommand (← `(noncomputable def $name:ident $params:bracketedBinder* := $rhs))
   if (← errorCount) == beforeErrors then
     registerComponentDefinitions name before
+    addComponentDocStrings name params doc
 
 end SystemAlgebra.DSL

src/ConstructiveCryptography/DSL/GRAMMAR.md

@@ -15,6 +15,22 @@ interfaces](../README.md#the-instances-on-interfaces),
 so that components assemble with `≫` and `⊗ₘ`. Citations refer to the numbered
 [references](../../../THEORY.md#references) of THEORY.md.
 
+System and converter declarations accept a leading `/-- ... -/` docstring. State the query,
+reply and sampling rule there. Lean exposes it on the component and its `.perPort` and `.exact`
+forms when those forms are generated. For example:
+
+```lean
+/-- Each eval(()) queries one inside bit b and returns its negation. -/
+converter Negate : Evaluation Unit Bool
+  inside oracle : Evaluation Unit Bool
+  on eval(_trigger : Unit) → Bool
+    b ← oracle.eval(())
+    return !b
+```
+
+Use the [constructor guide](../../../REUSE.md#start-from-the-type-you-need) for laws, sources
+and reusable reply transformations before defining a custom component.
+
 ## Grammar
 
 `block(P)` is a newline followed by one or more equally indented occurrences
@@ -23,18 +39,19 @@ denote optional syntax; quoted brackets are literal. `*` means repetition.
 
 ```text
 declaration ::= interface | system | converter | filter | system_definition | LeanDeclaration
+docstring   ::= "/--" Text "-/"
 parameters  ::= ("(" names ":" Type ")" | "[" Instance "]")*
 arguments   ::= [argument ("," argument)*]
 argument    ::= Name ":" Type
 
 interface ::= "interface" Name parameters block(port)
 port      ::= Name "(" arguments ")" "→" Type
 
-system ::= "system" Name parameters [":" InterfaceApplication]
+system ::= [docstring] "system" Name parameters [":" InterfaceApplication]
            block(system_member) ["by" Proof]
 system_member ::= requirement | domain | outside | initialization | reply
 
-converter ::= "converter" Name parameters [":" InterfaceApplication]
+converter ::= [docstring] "converter" Name parameters [":" InterfaceApplication]
               block(converter_member)
 converter_member ::= requirement | outside | inside | initialization | reply
 outside       ::= "outside" Name ":" InterfaceApplication
@@ -62,7 +79,7 @@ matching     ::= "match" Expression block(match_case)
 match_case   ::= "|" Pattern "→" block(statement)
 returning    ::= "return" Expression
 
-system_definition ::= "system" Name parameters "≔" SystemExpression
+system_definition ::= [docstring] "system" Name parameters "≔" SystemExpression
 SystemExpression ::= ComponentExpression | "(" SystemExpression ")"
                    | SystemExpression "∥" SystemExpression
                    | SystemExpression "≫" SystemExpression

src/RandomSystems/Typed/DSL/Syntax.lean

@@ -6,7 +6,8 @@ public import Lean
 # Surface syntax
 
 Indentation-based declarations of interfaces, systems, converters and filters, and their effect
-statements. Pure expressions, types and proofs use Lean's own parsers.
+statements. Systems and converters accept leading Lean docstrings.
+Pure expressions, types and proofs use Lean's own parsers.
 -/
 
 @[expose] public meta section
@@ -67,14 +68,19 @@ def cryptoPorts := leading_parser
   many1Indent (ppLine >> categoryParser `cryptoPort 0)
 
 syntax (name := interfaceDecl) "interface " ident cryptoParam* cryptoPorts : command
-syntax (name := systemComponentDecl) "system " ident cryptoParam* cryptoMembers
+syntax (name := systemComponentDecl) (Parser.Command.docComment)?
+  "system " ident cryptoParam* cryptoMembers
   ("by" tacticSeq)? : command
-syntax (name := systemComponentTypedDecl) "system " ident cryptoParam* " : " lineTerm cryptoMembers
+syntax (name := systemComponentTypedDecl) (Parser.Command.docComment)?
+  "system " ident cryptoParam* " : " lineTerm cryptoMembers
   ("by" tacticSeq)? : command
-syntax (name := converterDecl) "converter " ident cryptoParam* cryptoMembers : command
-syntax (name := converterTypedDecl) "converter " ident cryptoParam* " : " lineTerm cryptoMembers :
+syntax (name := converterDecl) (Parser.Command.docComment)?
+  "converter " ident cryptoParam* cryptoMembers : command
+syntax (name := converterTypedDecl) (Parser.Command.docComment)?
+  "converter " ident cryptoParam* " : " lineTerm cryptoMembers :
   command
-syntax (name := systemDecl) "system " ident cryptoParam* " ≔ " term : command
+syntax (name := systemDecl) (Parser.Command.docComment)?
+  "system " ident cryptoParam* " ≔ " term : command
 syntax (name := filterDecl) "filter " ident cryptoParam* " : " lineTerm
   "domain " ident " ↦ " lineTerm ("by" tacticSeq)? : command
 

src/Tests.lean

@@ -43,6 +43,7 @@ public import Tests.NaryParallelConverters
 public import Tests.CompositionalCosts
 public import Tests.DSL.Axioms
 public import Tests.DSL.Diagnostics
+public import Tests.DSL.Documentation
 public import Tests.DSL.Inlining
 public import Tests.DSL.ParallelOutside
 public import Tests.DSL.ProbabilityNotation

src/Tests/DSL/Documentation.lean

@@ -0,0 +1,69 @@
+module
+
+public import ConstructiveCryptography.DSL
+
+/-!
+# Documentation on component declarations
+
+Leading docstrings document the component and its `.perPort` and `.exact` forms, when generated.
+The examples cover typed and generated interfaces, deterministic and sampling systems, converters,
+and a named assembly. Metadata lookup checks the text a reader sees through Lean's documentation.
+-/
+
+@[expose] public section
+
+open SystemAlgebra SystemAlgebra.DSL Probability.Distribution
+
+namespace Tests.DSL.Documentation
+
+interface BitSource
+  draw() → Bool
+
+/-- Every `draw()` returns `false`. -/
+system Fixed : BitSource
+  on draw() → Bool
+    return false
+
+/-- Every `draw()` returns a fresh uniform bit. -/
+system Fresh
+  on draw() → Bool
+    b ←$ 𝒰[Bool]
+    return b
+
+/-- Every `draw()` forwards one inside draw and negates its reply. -/
+converter Negate : BitSource
+  inside source : BitSource
+  on draw() → Bool
+    b ← source.draw()
+    return !b
+
+/-- Every `get()` forwards one inside draw and returns its reply. -/
+converter Forward
+  inside source : BitSource
+  on get() → Bool
+    b ← source.draw()
+    return b
+
+/-- `Negate • Fixed`: every `draw()` returns `true`. -/
+system Combined ≔ Negate • Fixed
+
+-- Fully qualified metadata names also check components declared in a namespace.
+run_cmd do
+  let env ← Lean.getEnv
+  for (name, expected) in [
+      (``Fixed, "Every `draw()` returns `false`."),
+      (``Fixed.perPort, "Every `draw()` returns `false`."),
+      (``Fresh, "Every `draw()` returns a fresh uniform bit."),
+      (``Fresh.perPort, "Every `draw()` returns a fresh uniform bit."),
+      (``Negate, "Every `draw()` forwards one inside draw and negates its reply."),
+      (``Negate.perPort, "Every `draw()` forwards one inside draw and negates its reply."),
+      (``Negate.exact, "Every `draw()` forwards one inside draw and negates its reply."),
+      (``Forward, "Every `get()` forwards one inside draw and returns its reply."),
+      (``Forward.exact, "Every `get()` forwards one inside draw and returns its reply."),
+      (``Combined, "`Negate • Fixed`: every `draw()` returns `true`.")] do
+    let some actual ← Lean.findDocString? env name
+      | throwError "Missing documentation for {name}"
+    unless actual.trimAscii.toString == expected do
+      throwError "Unexpected documentation for {name}: {actual}"
+
+end Tests.DSL.Documentation