Systems: probabilistic automata, attaching programs to them, memoryless systems

README.md

@@ -15,15 +15,15 @@ summarizes the theory layer by layer, with links to the Lean declarations.
 | Library | Content |
 |---|---|
 | `Probability` | finitely supported distributions, kernels, statistical distance, couplings, expectation, counting |
-| `RandomSystems` | systems and automata; deterministic converters and programs; distributions over deterministic systems; random systems given by their cumulative probabilities; probabilistic converters, attachment and parallel composition; transcript distance and distinguishers; games |
+| `RandomSystems` | systems and automata; deterministic converters and programs; distributions over deterministic systems; random systems given by their cumulative probabilities; probabilistic automata and memoryless systems; probabilistic converters, attachment and parallel composition; transcript distance and distinguishers; games |
 | `ConstructiveCryptography.Specification`, `.Construction` | specifications, constructions and relaxations over any carrier |
 | `ConstructiveCryptography.CryptographicAlgebra` | the classes of cryptographic algebras: resource theories, parallel composition, compatible pseudo-metrics and distinguisher classes, relaxations |
-| `ConstructiveCryptography` (top level) | interfaces, resources and converters on random systems, and their instances of the classes; filters, contexts, sources, automata, functional resources, games presented by discrete games; notation |
+| `ConstructiveCryptography` (top level) | interfaces, resources and converters on random systems, and their instances of the classes; filters, contexts, sources, automata, memoryless systems, functional resources, games presented by discrete games; notation |
 | `ConstructiveCryptography.Substitution` | the substitution calculus for constructions [6] |
 | `ConstructiveCryptography.DSL` | a compiler from component declarations to resources and converters |
 | `ConstructiveCryptography.Tactics` | proof commands, including the substitution calculations `cc_calc` |
-| `Commons` | common ideal systems (URF, URP and their strong and tweakable forms), the CDH assumption as a pair of systems, the security notions as pairs of systems [6]: symmetric encryption (real-or-random and left-or-right CPA) and authenticated encryption (ind-cca, int-ptxt, int-ctxt, ae), public-key encryption and KEMs (IND-CPA, IND-CCA), MACs and signatures (EUF-CMA, SUF-CMA), PRGs, universal hashing (UHF, DUF) and collision resistance, and the schemes SHA-256, SHA-3, SHAKE, Keccak-256, ML-KEM [9] and ML-DSA [10] (the last two adapted from VCVio [11]) with known-answer tests, in the order of [8] |
-| `Examples` | authenticated encryption, AES, AEAD, substitutions on interfaces, the proof commands |
+| `Commons` | common ideal systems (URF, URP and their strong and tweakable forms, memoryless sources), the CDH assumption as a pair of systems, the security notions as pairs of systems [6]: symmetric encryption (real-or-random and left-or-right CPA) and authenticated encryption (ind-cca, int-ptxt, int-ctxt, ae), public-key encryption and KEMs (IND-CPA, IND-CCA), MACs and signatures (EUF-CMA, SUF-CMA), PRGs, universal hashing (UHF, DUF) and collision resistance, and the schemes SHA-256, SHA-3, SHAKE, Keccak-256, ML-KEM [9] and ML-DSA [10] (the last two adapted from VCVio [11]) with known-answer tests, in the order of [8] |
+| `Examples` | authenticated encryption, AES, AEAD, PRG length extension, substitutions on interfaces, the proof commands |
 | `Tests` | axiom audits, counterexamples, DSL diagnostics and semantics, tests of the substitution calculus |
 
 Module docstrings cite the source of each definition and theorem, with the

THEORY.md

@@ -59,6 +59,33 @@ environment, and on a domain of input histories
 systems on one domain form [mixtures][RandomSystem.mix], and two random systems run
 [independently in parallel][RandomSystem.parallel] form one on the combined alphabets.
 
+A [**probabilistic automaton**][RandomSystem.ofProbAutomaton] answers a query from its state with a
+law on the next state and the reply, a [probabilistic step][ProbStep]; its random system follows
+the [sub-law of the states][ProbStep.belief] reached with the replies of a transcript, whose weight
+is the probability of the transcript. On an input domain, two probabilistic automata
+[have the same random system][RandomSystem.ofProbAutomaton_eq_of_simulation] along a
+[simulation][ProbStep.SimulatesAt], a kernel between their states through which their steps
+commute. A deterministic automaton with a random initial state
+[is the probabilistic automaton of its point steps][RandomSystem.ofProbAutomaton_ofDeterministic_apply],
+and a probabilistic automaton
+[is a deterministic automaton reading pre-sampled draws][RandomSystem.ofProbAutomaton_eq_drawStep],
+sampled once with the initial state: a random automaton [4, Definition 2].
+
+A random system is [**memoryless**][RandomSystem.memoryless] when the law of its reply depends only
+on the current query, never on the history: a source "can be memoryless or have memory"
+[3, Definition 3.1], and a single-input system given by a conditional distribution is a "discrete
+memoryless channel" [3, §3.6.1]. With the reply law $`\nu`$, its probabilities obey the chain rule
+
+```math
+p\big(h \cdot (x, y)\big) = p(h)\, \nu_x(y) \qquad \text{for every query } x \text{ admitted after } h,
+```
+
+and [a random system obeying it is the memoryless system][RandomSystem.eq_memoryless_of_snoc].
+A probabilistic automaton whose step [replies from every state with the same
+law][ProbStep.Memoryless] $`\nu`$ [is the memoryless system of this law][RandomSystem.ofProbAutomaton_eq_memoryless].
+Two memoryless systems [side by side are memoryless][RandomSystem.parallel_memoryless]: a query
+to either system is answered with the reply law of that system.
+
 ### 1.3 Converters
 
 A [**DDC**][IsDDC] is a system on the converter alphabets (outside queries and inside replies in;
@@ -94,6 +121,22 @@ Attached to an automaton, a program is [inlined][Program.inline] [4, §3.3]: the
 [combined automaton][Program.combine] on pairs of states, also
 [on domains][Program.trim_apply_ofProgramOn_automaton].
 
+Run against a probabilistic automaton, a program is the probabilistic automaton
+[on pairs of states][Program.probCombine] whose step runs one invocation, the automaton answering
+the inside queries with fresh steps; it [respects simulations][RandomSystem.ofProbAutomaton_probCombine_eq_of_simulation].
+[**Attaching the program's converter to a probabilistic automaton is the program run against
+it**][PDCBehavior.attach_ofDDC_ofProgramOn_ofProbAutomaton], the combined system $`C(F)`$ of a
+system $`C(\cdot)`$ invoking $`F`$ [4, §3.3]; for point steps it is the
+[combined automaton][PDCBehavior.attach_ofDDC_ofProgramOn_ofDeterministic]. Against memoryless
+replies of the laws $`\nu`$, a program [replies memorylessly][Program.memoryless_probCombine] when
+its [reply law][Program.replyLaw] $`\kappa`$, the law of one invocation whose inside queries are
+answered by fresh samples of $`\nu`$, is the same from every program state. So [the composition law][PDCBehavior.attach_ofDDC_ofProgramOn_memoryless]
+holds, whatever the number of the program's inside queries:
+
+```math
+\alpha_P\, \mathrm{mem}(\nu) = \mathrm{mem}(\kappa).
+```
+
 ### 1.4 Distance and distinguishers
 
 The [**transcript distance**][RandomSystem.transcriptDistance] takes the supremum over environments
@@ -327,10 +370,17 @@ resource beside: [attaching][Interface.attach_rightContext] $`\mathrm{rightConte
 gives $`R \parallel S`$, and so does [attaching][Interface.attach_leftContext]
 $`\mathrm{leftContext}\ R\ B`$ to $`S`$.
 
-A [**source**][Interface.Resource.source] answers with fresh independent samples of a law
-[4, Definition 1]. An [**automaton**][Interface.Resource.ofAutomaton] is a transition function with
+A [**source**][Interface.Resource.source] answers with fresh independent samples of a law: a
+memoryless source [3, Definition 3.1] (the sources of [4, Definition 1] may have memory). An [**automaton**][Interface.Resource.ofAutomaton] is a transition function with
 a sampled initial state [4, Definition 2], and [parallel automata][Interface.parallel_ofAutomaton]
-are the automaton running both side by side. **Functional resources** are given by
+are the automaton running both side by side. A source [is memoryless][Interface.source_eq_memoryless],
+memoryless systems [side by side are memoryless][Interface.parallel_eq_memoryless], and the
+converter of a program [maps a memoryless system to the memoryless system of its reply
+law][Interface.Converter.ofProgram_smul_memoryless], also
+[for port-preserving programs][Interface.Converter.ofPreservingProgram_smul_memoryless] and
+[with its own sources beside its inside interface][Interface.Converter.ofPreservingProgram_comp_rightContext_smul_memoryless]:
+the composition law of §1.3 on their random systems.
+**Functional resources** are given by
 [reply functions][Interface.Resource.ofFunction], by
 [conditional reply laws][Interface.Resource.ofConditional], or by
 [sampling once][Interface.Resource.sample] and keeping the sample.
@@ -745,7 +795,11 @@ A [`filter F : I domain h ↦ P`][elabFilter] generates `F : (I q).restrict P 
 A compiled component is an automaton with a sampled initial state. Attaching a program to an
 automaton [gives the combined automaton][Interface.Converter.ofProgram_smul_ofAutomaton], also
 [for port-preserving programs][Interface.Converter.ofPreservingProgram_smul_ofAutomaton], so
-compiled systems are compared by [bisimulation][automatonSystem_eq_of_bisim].
+compiled systems are compared by [bisimulation][automatonSystem_eq_of_bisim]. The
+[memoryless source][MemorylessSource] `y ←$ ν; return y`
+[is the memoryless system of `ν`][MemorylessSource.memoryless_eq], so systems built from programs
+and memoryless sources are compared by the laws of one reply, through the composition laws of §2.2:
+each hop of [PRG length extension][ExPRG] is one rewrite.
 
 ---
 
@@ -895,6 +949,7 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X
 [ExAES]: src/Examples/DSL/AES.lean
 [ExAEAD]: src/Examples/DSL/AEAD.lean
 [ExUse]: src/Examples/Usability.lean
+[ExPRG]: src/Examples/PRGLengthExtension.lean
 
 <!-- Declarations: §1 -->
 
@@ -950,13 +1005,32 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X
 [PDCBehavior.tensor_id]: src/RandomSystems/Converter/ConverterTensor.lean#L705
 [Program]: src/RandomSystems/Converter/Program.lean#L45
 [Program.Bounded]: src/RandomSystems/Converter/Program.lean#L70
-[Program.Costs]: src/RandomSystems/Converter/Program.lean#L88
-[Program.PortPreserving]: src/RandomSystems/Converter/Program.lean#L99
-[DDC.insideQueries_restrict_length_le]: src/RandomSystems/Converter/Program.lean#L513
-[DDC.ofProgramOn_isDDCFrom]: src/RandomSystems/Converter/Program.lean#L610
+[Program.Costs]: src/RandomSystems/Converter/Program.lean#L112
+[Program.PortPreserving]: src/RandomSystems/Converter/Program.lean#L123
+[DDC.insideQueries_restrict_length_le]: src/RandomSystems/Converter/Program.lean#L537
+[DDC.ofProgramOn_isDDCFrom]: src/RandomSystems/Converter/Program.lean#L634
 [Program.inline]: src/RandomSystems/Converter/ProgramAttachment.lean#L258
 [Program.combine]: src/RandomSystems/Converter/ProgramAttachment.lean#L429
 [Program.trim_apply_ofProgramOn_automaton]: src/RandomSystems/Converter/ProgramAttachment.lean#L609
+[RandomSystem.ofProbAutomaton]: src/RandomSystems/System/ProbAutomaton.lean#L197
+[ProbStep]: src/RandomSystems/System/ProbAutomaton.lean#L58
+[ProbStep.belief]: src/RandomSystems/System/ProbAutomaton.lean#L160
+[ProbStep.SimulatesAt]: src/RandomSystems/System/ProbAutomaton.lean#L260
+[RandomSystem.ofProbAutomaton_eq_of_simulation]: src/RandomSystems/System/ProbAutomaton.lean#L400
+[RandomSystem.ofProbAutomaton_ofDeterministic_apply]: src/RandomSystems/System/ProbAutomaton.lean#L535
+[RandomSystem.ofProbAutomaton_eq_drawStep]: src/RandomSystems/Converter/ProbProgramAttachment.lean#L933
+[RandomSystem.memoryless]: src/RandomSystems/System/Memoryless.lean#L65
+[RandomSystem.eq_memoryless_of_snoc]: src/RandomSystems/System/Memoryless.lean#L84
+[RandomSystem.parallel_memoryless]: src/RandomSystems/System/Memoryless.lean#L146
+[ProbStep.Memoryless]: src/RandomSystems/System/Memoryless.lean#L237
+[RandomSystem.ofProbAutomaton_eq_memoryless]: src/RandomSystems/System/Memoryless.lean#L273
+[Program.probCombine]: src/RandomSystems/Converter/ProbProgramAttachment.lean#L187
+[RandomSystem.ofProbAutomaton_probCombine_eq_of_simulation]: src/RandomSystems/Converter/ProbProgramAttachment.lean#L507
+[PDCBehavior.attach_ofDDC_ofProgramOn_ofProbAutomaton]: src/RandomSystems/Converter/ProbProgramAttachment.lean#L1095
+[PDCBehavior.attach_ofDDC_ofProgramOn_ofDeterministic]: src/RandomSystems/Converter/ProbProgramAttachment.lean#L1009
+[Program.memoryless_probCombine]: src/RandomSystems/System/Memoryless.lean#L390
+[Program.replyLaw]: src/RandomSystems/System/Memoryless.lean#L304
+[PDCBehavior.attach_ofDDC_ofProgramOn_memoryless]: src/RandomSystems/System/Memoryless.lean#L421
 [RandomSystem.transcriptDistance]: src/RandomSystems/Distance/Decision.lean#L228
 [Domain.Compatible]: src/RandomSystems/Distance/Decision.lean#L165
 [Domain.DecisionCompatible]: src/RandomSystems/Distance/Decision.lean#L171
@@ -1055,6 +1129,11 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X
 [Interface.Resource.source]: src/ConstructiveCryptography/Source.lean#L49
 [Interface.Resource.ofAutomaton]: src/ConstructiveCryptography/Automaton.lean#L42
 [Interface.parallel_ofAutomaton]: src/ConstructiveCryptography/Automaton.lean#L57
+[Interface.source_eq_memoryless]: src/ConstructiveCryptography/Memoryless.lean#L45
+[Interface.parallel_eq_memoryless]: src/ConstructiveCryptography/Memoryless.lean#L143
+[Interface.Converter.ofProgram_smul_memoryless]: src/ConstructiveCryptography/Memoryless.lean#L236
+[Interface.Converter.ofPreservingProgram_smul_memoryless]: src/ConstructiveCryptography/Memoryless.lean#L257
+[Interface.Converter.ofPreservingProgram_comp_rightContext_smul_memoryless]: src/ConstructiveCryptography/Memoryless.lean#L274
 [Interface.Resource.ofFunction]: src/ConstructiveCryptography/Functional.lean#L56
 [Interface.Resource.ofConditional]: src/ConstructiveCryptography/Functional.lean#L38
 [Interface.Resource.sample]: src/ConstructiveCryptography/Functional.lean#L176
@@ -1223,6 +1302,8 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X
 [Interface.Converter.ofPreservingProgram]: src/ConstructiveCryptography/DSL/Converters.lean#L67
 [Interface.Converter.ofProgram_smul_ofAutomaton]: src/ConstructiveCryptography/DSL/Converters.lean#L142
 [Interface.Converter.ofPreservingProgram_smul_ofAutomaton]: src/ConstructiveCryptography/DSL/Converters.lean#L152
+[MemorylessSource]: src/Commons/Definitions/Ideal.lean#L95
+[MemorylessSource.memoryless_eq]: src/Commons/Definitions/Ideal.lean#L103
 [cc_normalize]: src/ConstructiveCryptography/Tactics/Basic.lean#L30
 [cc_nonexpand]: src/ConstructiveCryptography/Tactics/Categorical.lean#L166
 [cc_nonexpand-interfaces]: src/ConstructiveCryptography/Notation.lean#L105

src/Commons/Definitions/Ideal.lean

@@ -1,5 +1,6 @@
 import ConstructiveCryptography.DSL
 import ConstructiveCryptography.Functional
+import ConstructiveCryptography.Memoryless
 import Mathlib.Data.Fintype.Perm
 
 /-!
@@ -10,14 +11,20 @@ answers each input with the function's value; an `X`-random permutation is one o
 bijections of `X`. The uniform ones are the uniform random function (URF) and the uniform random
 permutation (URP) (CR18, Definition 3.15 and Example 3.5, printed p. 64). The strong URP also
 answers inverse queries, and a tweakable URP is an independent URP for each tweak. Each system
-samples once and keeps its sample for the whole interaction.
+samples once and keeps its sample for the whole interaction. A memoryless source samples afresh
+at each query (CR18, Definition 3.1, printed p. 55: "A source can be memoryless or have memory").
 
 ## Main definitions
 
 * `Evaluation X Y`, `Bidirectional X`, `TweakedEvaluation T X`, `TweakedBidirectional T X`: the
   interfaces of a function, of a permutation with its inverse, and of their tweaked versions
 * `URF A`, `URP A`: an independent URF, and an independent URP, at each label of `A`
 * `StrongURP X`, `TweakableURP T X`, `TweakableStrongURP T X`
+* `MemorylessSource Y ν`: the memoryless source of `ν`, answering each query with a fresh sample
+
+## Main results
+
+* `MemorylessSource.memoryless_eq`: the memoryless source of `ν` is the memoryless system of `ν`
 -/
 
 namespace Commons
@@ -79,4 +86,41 @@ def TweakableStrongURP : Interface.Resource (TweakedBidirectional T X q) :=
 
 end
 
+/-! ### Memoryless sources -/
+
+open SystemAlgebra.DSL
+
+-- **The memoryless source** of `ν` (CR18, Definition 3.1, printed p. 55): on `eval(())`, a fresh
+-- sample `y ← ν`, returned.
+system MemorylessSource(Y : Type) [Fintype Y] (ν : Distribution.ProbDist Y) : Evaluation Unit Y
+  on eval(_input : Unit) → Y
+    y ←$ ν
+    return y
+
+open Distribution in
+/-- **The memoryless source of `ν` is the memoryless system of `ν`**: each `eval(())` is answered
+by a fresh sample of `ν`, independent of the history. -/
+lemma MemorylessSource.memoryless_eq {Y : Type} [Fintype Y] (ν : ProbDist Y)
+    (q : Evaluation.Port → ℕ) :
+    (MemorylessSource.perPort Y ν (budget := q)).1 =
+      RandomSystem.memoryless _ (RandomSystem.portLaw fun _ _ => ν) := by
+  -- The source is its program attached to its source of samples of `ν`:
+  --
+  --   eval(()) ──► program ── randomness(()) ──► source, fresh samples y ← ν
+  --            ◄── eval ⇒ y
+  --
+  -- The source of samples is memoryless, so by the composition law the system is memoryless with
+  -- the reply law of one invocation of the program.
+  -- The composition law `Interface.Converter.ofProgram_smul_memoryless`, with the source of
+  -- samples memoryless (`Interface.source_eq_memoryless`); the law of one invocation remains.
+  refine Interface.Converter.ofProgram_smul_memoryless none _ _ _
+    (Interface.source_eq_memoryless _ _) ?_
+  -- One invocation: draw `y ← ν` and reply `y`. Its law is `ν`, in both initialization states
+  -- (`none` before the first call, `some ()` after).
+  rintro (_ | ⟨⟩) ⟨⟩ ⟨⟩
+  · simp [Program.replyLaw, MemorylessSource.body, MemorylessSource.law1, callProg, returnProg,
+      bindK_single_one]
+  · simp [Program.replyLaw, MemorylessSource.body, MemorylessSource.law1, callProg, returnProg,
+      bindK_single_one]
+
 end Commons

src/ConstructiveCryptography.lean

@@ -20,6 +20,7 @@ import ConstructiveCryptography.InterfaceMonoidal
 import ConstructiveCryptography.InterfaceParallel
 import ConstructiveCryptography.InterfaceRelabel
 import ConstructiveCryptography.InterfaceTensorRename
+import ConstructiveCryptography.Memoryless
 import ConstructiveCryptography.Notation
 import ConstructiveCryptography.PresentedGame
 import ConstructiveCryptography.DSL
@@ -64,7 +65,7 @@ import ConstructiveCryptography.Tactics.ProofAutomationAttributes
 
 /-!
 Constructive Cryptography: interfaces and domains, arrows, resources and the action, parallel
-composition, the resource distance, specifications of resources, filters, budgets, functional
-constructors, games presented by discrete games; the categorical packaging; and the extensions
-(substitution, the DSL).
+composition, the resource distance, memoryless systems, specifications of resources, filters,
+budgets, functional constructors, games presented by discrete games; the categorical packaging;
+and the extensions (substitution, the DSL).
 -/