diff --git a/REUSE.md b/REUSE.md index 23a40ba..3fe710b 100644 --- a/REUSE.md +++ b/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 diff --git a/src/ConstructiveCryptography/DSL/Elaborator.lean b/src/ConstructiveCryptography/DSL/Elaborator.lean index f7325f4..44b9188 100644 --- a/src/ConstructiveCryptography/DSL/Elaborator.lean +++ b/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,6 +991,27 @@ 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 @@ -996,6 +1019,8 @@ 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 diff --git a/src/ConstructiveCryptography/DSL/GRAMMAR.md b/src/ConstructiveCryptography/DSL/GRAMMAR.md index 62d334b..73284b3 100644 --- a/src/ConstructiveCryptography/DSL/GRAMMAR.md +++ b/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,6 +39,7 @@ 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 @@ -30,11 +47,11 @@ 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 diff --git a/src/RandomSystems/Typed/DSL/Syntax.lean b/src/RandomSystems/Typed/DSL/Syntax.lean index 28b98cc..1bcb456 100644 --- a/src/RandomSystems/Typed/DSL/Syntax.lean +++ b/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 diff --git a/src/Tests.lean b/src/Tests.lean index 586c4cc..ff7a1ae 100644 --- a/src/Tests.lean +++ b/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 diff --git a/src/Tests/DSL/Documentation.lean b/src/Tests/DSL/Documentation.lean new file mode 100644 index 0000000..06f5543 --- /dev/null +++ b/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