diff --git a/README.md b/README.md index 28ee142..ef0d60c 100644 --- a/README.md +++ b/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 diff --git a/THEORY.md b/THEORY.md index 448c9b1..03244f4 100644 --- a/THEORY.md +++ b/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 @@ -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 diff --git a/src/Commons/Definitions/Ideal.lean b/src/Commons/Definitions/Ideal.lean index a7ae0e1..b59c6ac 100644 --- a/src/Commons/Definitions/Ideal.lean +++ b/src/Commons/Definitions/Ideal.lean @@ -1,5 +1,6 @@ import ConstructiveCryptography.DSL import ConstructiveCryptography.Functional +import ConstructiveCryptography.Memoryless import Mathlib.Data.Fintype.Perm /-! @@ -10,7 +11,8 @@ 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 @@ -18,6 +20,11 @@ samples once and keeps its sample for the whole interaction. 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 diff --git a/src/ConstructiveCryptography.lean b/src/ConstructiveCryptography.lean index af012f5..e9bfc6b 100644 --- a/src/ConstructiveCryptography.lean +++ b/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). -/ diff --git a/src/ConstructiveCryptography/Memoryless.lean b/src/ConstructiveCryptography/Memoryless.lean new file mode 100644 index 0000000..af4b169 --- /dev/null +++ b/src/ConstructiveCryptography/Memoryless.lean @@ -0,0 +1,297 @@ +import ConstructiveCryptography.DSL.Converters +import ConstructiveCryptography.Context +import RandomSystems.System.Memoryless + +/-! +# Memoryless systems on interfaces + +A system on an interface whose random system is memoryless [1, Definition 3.1, §3.6.1] replies to +each query with a fresh sample of a law of that query. A source of independent samples is +memoryless, two memoryless systems side by side are memoryless, and the converter of a program maps +memoryless systems to memoryless systems, with the reply law of the program +(`PDCBehavior.attach_ofDDC_ofProgramOn_memoryless`), also when the converter has its own sources +beside its inside interface: + +``` + o(u) ┌───┐ ── j(q) ───► R, memoryless with ν + ────────────────►│ P │ + ◄────────────────┤ │ ── k(()) ──► T, memoryless with ν' (the converter's own randomness) + o ⇒ v └───┘ + (P ≫ rightContext B T) • R = mem(κ), κ = P's reply law against ν, ν' +``` + +Statements about typed systems are equalities of their random systems (`.1`). + +## Main results + +* `Interface.source_eq_memoryless`: a source of independent samples of `law` is memoryless +* `Interface.parallel_eq_memoryless`: memoryless systems side by side are memoryless +* `Interface.Converter.ofProgram_smul_memoryless`, + `Interface.Converter.ofPreservingProgram_smul_memoryless`, + `Interface.Converter.ofPreservingProgram_comp_rightContext_smul_memoryless`: the composition law + `P • mem(ν) = mem(κ)` for the converters of programs + +## References + +1. U. Maurer. *Cryptography Foundations*. Lecture notes, ETH Zurich, Spring 2018. +-/ + +namespace SystemAlgebra.Interface + +open Probability Probability.Distribution CategoryTheory RandomSystem + +/-- **A source of independent samples is memoryless** [1, Definition 3.1]: the source of `q` +samples of `law` replies to each trigger with a fresh sample of `law`. -/ +lemma source_eq_memoryless {Z : Type} [Fintype Z] (law : ProbDist Z) (q : ℕ) : + (Resource.source law q).1 = + memoryless (Interface.source Z q).inputDomain (portLaw fun _ _ => law) := by + -- Plan: + -- 1. The typed source's random system is presented by a table `t ← law^q` of independent + -- samples: a transcript `h` has the mass of the tables that give it (`hmass`). + -- 2. One more trigger reads entry `h.length` of the table (`hsnoc`). + -- 3. Whether a table gives `h` depends only on its entries before `h.length` (`hread`). + -- 4. The systems-level criterion `eq_memoryless_of_snoc` asks for the chain rule of `law`: + -- entry `h.length` is independent of the earlier ones, so each admitted trigger + -- multiplies the probability by `law z`. + -- + -- ┌─────────────────────────────┐ + -- () ──────▶ │ table t = (t 0, …, t (q-1)) │ entries independent, each ∼ law + -- ◀── t k ── │ trigger k ↦ entry t k │ (k = 0, 1, …; at most q triggers) + -- └─────────────────────────────┘ + -- + -- P[h · ((), z)] = law^q[t gives h ∧ t h.length = z] + -- = law^q[t gives h] · law z (entry h.length independent of the rest) + -- = P[h] · law z + classical + -- Step 1: the probability of a transcript is a mass of tables. + -- The source reads its `k`-th reply from the `k`-th entry of a table `t` of independent + -- samples. A transcript `h` has the probability of the tables from which it is read. + let event : List ((Σ _ : Unit, Unit) × (Σ _ : Unit, Z)) → (Fin q → Z) → Prop := fun h t => + Replies (filterDom (Interface.source Z q).domain (automatonSystem (sourceStep law) (t, 0))) + (h.map Prod.fst) (h.map Prod.snd) + have hmass : ∀ h, (Resource.source law q).1 h = (pi fun _ : Fin q => law.1).mass (event h) := by + intro h + -- The source is the automaton `sourceStep` started in `(t, 0)` (table `t`, counter `0`) + -- for `t ← law^q`: a transcript has the mass of the initial states, hence of the tables, + -- from which the automaton gives it. + rw [Resource.source, Resource.ofAutomaton_mass, mass_fTransform] + -- Step 2: one more trigger reads the next entry of the table. + -- One more exchange: the table also gives `h · ((), z)` when the domain admits one more query + -- and its entry `h.length` is `z`. + have hsnoc : ∀ h z (hlt : h.length < q), ((Interface.source Z q).domain + (h.map Prod.fst ++ [⟨(), ()⟩])) → ∀ t, event (h ++ [(⟨(), ()⟩, ⟨(), z⟩)]) t ↔ + event h t ∧ t ⟨h.length, hlt⟩ = z := by + intro h z hlt hd t + -- After `h` the automaton is in state `(t, h.length)` (`stateAfter_sourceStep`); the + -- domain admits the new trigger (`hd`), so the domain filter keeps its reply, the entry + -- `t h.length`. + simp only [event, List.map_append, List.map_cons, List.map_nil, replies_snoc, + SystemAlgebra.filterDom, automatonSystem_snoc, stateAfter_sourceStep, if_pos hd] + simp [sourceStep, hlt, Part.some_inj, eq_comm] + -- Step 3: tables agreeing on the entries that `h` reads give `h` alike. + -- The event of `h` reads only the entries before `h.length`. + have hread : ∀ h t t', (∀ j : Fin q, j.val < h.length → t j = t' j) → + (event h t ↔ event h t') := by + intro h + -- Induction on `h`, one exchange added at the end at a time. + induction h using List.reverseRecOn with + -- No exchange: every table gives the empty transcript. + | nil => intro t t' _; simp [event] + -- One more exchange `((), z)` after `h`, for tables `t`, `t'` agreeing below + -- `h.length + 1`. + | append_singleton h e ih => + intro t t' ht + obtain ⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, z⟩⟩ := e + -- the earlier entries agree + have hpre := ih t t' fun j hj => ht j (by simp; omega) + -- One step of the automaton after `h`, for both tables. + simp only [event, List.map_append, List.map_cons, List.map_nil, replies_snoc, + SystemAlgebra.filterDom, automatonSystem_snoc, stateAfter_sourceStep] at hpre ⊢ + -- The earlier exchanges are given by `t` iff by `t'`. + rw [hpre] + -- Split on whether the domain still admits a trigger after `h`. + by_cases hlt : h.length < q + -- `h.length < q`: the new reply is `t h.length = t' h.length`. + · simp [sourceStep, hlt, ht ⟨h.length, hlt⟩ (by simp)] + -- Past `q` triggers the domain admits no more trigger, under either table. + · simp [hlt] + -- Step 4: the chain rule, by the systems-level criterion `eq_memoryless_of_snoc`. + -- The chain rule of `law`: each admitted trigger multiplies the probability by `law z`. + refine eq_memoryless_of_snoc fun h x y hd => ?_ + -- The query is the trigger `()`, the reply some `z`. + obtain ⟨⟨⟩, ⟨⟩⟩ := x + obtain ⟨⟨⟩, z⟩ := y + -- The domain admits the trigger after `h`: at most `q` triggers, so `h.length < q`. + have hd' : (Interface.source Z q).domain (h.map Prod.fst ++ [⟨(), ()⟩]) := hd + have hlt : h.length < q := by + have := hd'.2 + simp only [List.length_append, List.length_map, List.length_singleton] at this + omega + -- Both sides as masses of tables (`hmass`); the tables giving `h · ((), z)` are those giving + -- `h` with `t h.length = z` (`hsnoc`). + rw [hmass, hmass, mass_congr _ (hsnoc h z hlt hd')] + -- Independent entries: the entry `h.length` is independent of the earlier ones. + rw [mass_pi_and_eq (fun _ : Fin q => law.1) (fun _ => law.2.2) ⟨h.length, hlt⟩ z (event h) + fun t a => hread h _ _ fun j hj => Function.update_of_ne (Fin.ne_of_val_ne hj.ne) _ _] + -- The reply law of the source at its port is `law`. + rw [portLaw_apply_mk] + +/-- **Memoryless systems side by side are memoryless**: a query at a left port has the reply +law of the left system, one at a right port the reply law of the right system. The typed parallel +composition is the systems-level one, `RandomSystem.parallel_memoryless`, with the ports of the +two interfaces relabelled as the ports of their tensor. -/ +lemma parallel_eq_memoryless {A B : Interface} {R : Resource A} {T : Resource B} + {ν₁ : ∀ i, A.X i → ProbDist (A.Y i)} {ν₂ : ∀ j, B.X j → ProbDist (B.Y j)} + (hR : R.1 = memoryless A.inputDomain (portLaw ν₁)) + (hT : T.1 = memoryless B.inputDomain (portLaw ν₂)) : + (parallel R T).1 = memoryless (tensor A B).inputDomain (portLaw (parallelLaw ν₁ ν₂)) := by + -- Plan: + -- 1. Systems level: `RandomSystem.parallel_memoryless` gives the parallel composition of the + -- two memoryless systems as the memoryless system of the side-by-side law `twoLaw`. + -- 2. The typed system `parallel R T` has as random system that systems-level composition, + -- read through the relabelling `e` of the tensor's ports `inl i`, `inr j` as left and + -- right ports. The systems-level criterion `eq_memoryless_of_snoc` asks for the chain + -- rule of `parallelLaw` at each admitted exchange. + -- 3. An impossible transcript stays impossible. For a possible one, the systems-level domain + -- admits the relabelled query, and the chain rule `memoryless_snoc` of `hsys` applies. + -- 4. Port by port, the law `twoLaw` of the relabelled reply is `parallelLaw`. + -- + -- ┌───┐ + -- inl i ─x─▶ │ R │ reply ∼ ν₁ i x + -- ├───┤ + -- inr j ─x─▶ │ T │ reply ∼ ν₂ j x + -- └───┘ + -- + -- Step 1: the systems-level statement. + -- At the systems level, the two memoryless systems side by side are the memoryless system of + -- their side-by-side laws. + have hsys := RandomSystem.parallel_memoryless A.inputDomain B.inputDomain (portLaw ν₁) + (portLaw ν₂) + -- Write the two memoryless systems of `hsys` as `R.1` and `T.1` (`hR`, `hT`). + rw [← hR, ← hT] at hsys + -- Step 2: reduce to the chain rule on relabelled transcripts. + -- The chain rule of the laws of the ports of the tensor, at each admitted exchange `(x, y)`. + refine eq_memoryless_of_snoc fun h x y hd => ?_ + -- The typed system is the systems-level one on the transcript with relabelled ports. + let eX := sumAlphabet (Sum.rec A.X B.X) + let e := eX.symm.prodCongr (sumAlphabet (Sum.rec A.Y B.Y)).symm + change RandomSystem.parallel R.1 T.1 ((h ++ [(x, y)]).map e) = + RandomSystem.parallel R.1 T.1 (h.map e) * (portLaw (parallelLaw ν₁ ν₂) x).1 y + rw [List.map_append, List.map_singleton] + -- Step 3: split on whether the relabelled transcript `h` has probability zero. + by_cases hz : RandomSystem.parallel R.1 T.1 (h.map e) = 0 + · -- An impossible transcript stays impossible. + rw [hz, zero_mul] + exact (RandomSystem.parallel R.1 T.1).mass_eq_zero_of_prefix (List.prefix_append _ _) hz + -- A possible transcript: the systems-level parallel domain admits the relabelled query, as the + -- domain of the tensor admits `x`. + have hadm := (parallel_admits_iff A B R T (h.map e) hz (eX.symm x)).mpr (by + -- Relabelling the queries of `h` to the systems level and back leaves them unchanged. + have hround : ((h.map e).map Prod.fst).map eX = h.map Prod.fst := by + simp only [List.map_map] + exact List.map_congr_left fun z _ => eX.apply_symm_apply _ + rw [hround, eX.apply_symm_apply] + exact hd) + -- The chain rule at the systems level; it remains to compare the two laws of the reply. + rw [hsys, show e (x, y) = (eX.symm x, (sumAlphabet (Sum.rec A.Y B.Y)).symm y) from rfl, + memoryless_snoc, if_pos hadm] + -- Cancel the common factor, the probability of `h`. + congr 1 + -- Step 4: the two reply laws agree. + -- The relabelled query goes to the system of its port, and its law there is the law of that + -- port; a reply at another port has probability zero on both sides. + -- Four cases: the query at a left or a right port, the reply at a left or a right port. + obtain ⟨(i | j), x⟩ := x <;> obtain ⟨(k | l), y⟩ := y + -- Left query `⟨inl i, x⟩`, left reply at `k`: `twoLaw` hands the query to `portLaw ν₁`. + · change (portLaw (twoLaw (portLaw ν₁) (portLaw ν₂)) ⟨none, ⟨i, x⟩⟩).1 ⟨none, ⟨k, y⟩⟩ = _ + rw [portLaw_apply_mk] + -- At `k = i` both laws are `ν₁ i x`; at `k ≠ i` both give the reply zero mass. + by_cases hk : k = i + · subst hk + simp only [twoLaw, parallelLaw, portLaw_apply_mk] + · simp only [twoLaw] + rw [portLaw_apply_of_ne _ (by simpa using hk), portLaw_apply_of_ne _ (by simpa using hk)] + -- Left query, right reply: zero on both sides. + · change (portLaw (twoLaw (portLaw ν₁) (portLaw ν₂)) ⟨none, ⟨i, x⟩⟩).1 ⟨some (), ⟨l, y⟩⟩ = _ + rw [portLaw_apply_of_ne _ (by simp), portLaw_apply_of_ne _ (by simp)] + -- Right query, left reply: zero on both sides. + · change (portLaw (twoLaw (portLaw ν₁) (portLaw ν₂)) ⟨some (), ⟨j, x⟩⟩).1 ⟨none, ⟨k, y⟩⟩ = _ + rw [portLaw_apply_of_ne _ (by simp), portLaw_apply_of_ne _ (by simp)] + -- Right query `⟨inr j, x⟩`, right reply at `l`: as the left case, with `portLaw ν₂`. + · change (portLaw (twoLaw (portLaw ν₁) (portLaw ν₂)) ⟨some (), ⟨j, x⟩⟩).1 ⟨some (), ⟨l, y⟩⟩ = _ + rw [portLaw_apply_mk] + by_cases hl : l = j + · subst hl + simp only [twoLaw, parallelLaw, portLaw_apply_mk] + · simp only [twoLaw] + rw [portLaw_apply_of_ne _ (by simpa using hl), portLaw_apply_of_ne _ (by simpa using hl)] + +namespace Converter + +variable {A B : Interface} {S : Type} + +/-- **The composition law** for the converter of a program: on a memoryless system with the +reply law `ν`, the converter of a program whose reply law against `ν` is `κ` in every state gives +the memoryless system with the reply law `κ`. -/ +lemma ofProgram_smul_memoryless (s : S) (P : Program S A.I B.I A.X A.Y B.X B.Y) {b : ℕ} + (hb : P.Bounded b) (hB : ∀ xs, xs ≠ [] → xs.length ≤ b * A.bound → B.domain xs) + {R : Resource B} {ν : ∀ j, B.X j → ProbDist (B.Y j)} {κ : ∀ o, A.X o → ProbDist (A.Y o)} + (hR : R.1 = memoryless B.inputDomain (portLaw ν)) + (hκ : ∀ s' o u, P.replyLaw ν s' o u b [] = (κ o u).1) : + (ofProgram s P hb hB • R).1 = memoryless A.inputDomain (portLaw κ) := + -- The typed attachment's random system is the systems-level attachment of the behavior of + -- the program's DDC (`DDC.ofProgramOn s P A.domain`) to `R.1`. The systems-level + -- composition law `PDCBehavior.attach_ofDDC_ofProgramOn_memoryless` gives it: both interface + -- domains exclude `[]` and are closed under nonempty prefixes (`nonempty_prefix`), and `R` + -- replies at the queried port (`R.2`): + -- + -- o(u) ──▶ ┌───┐ ── j(x) ──▶ ┌────────┐ + -- │ P │ │ mem(ν) │ y ∼ ν j x, fresh at each query + -- ◀── v ── └───┘ ◀── y ───── └────────┘ + -- + -- v ∼ κ o u: the law of P's reply when each inside query gets a fresh sample of ν. + PDCBehavior.attach_ofDDC_ofProgramOn_memoryless B.nonempty_prefix A.nonempty_prefix s P hb _ hκ hR + R.2 + +/-- **The composition law** for the converter of a port-preserving program. -/ +lemma ofPreservingProgram_smul_memoryless (s : S) (P : Program S A.I B.I A.X A.Y B.X B.Y) + {b : ℕ} (hb : P.Bounded b) (ι : A.I → Option B.I) (hι : P.PortPreserving ι) (q : A.I → ℕ) + (hA : ∀ xs, A.domain xs → ∀ o, (SystemAlgebra.restrict o xs).length ≤ q o) + (hB : ∀ ys, ys ≠ [] → ys.length ≤ b * A.bound → + (∀ o j, ι o = some j → (SystemAlgebra.restrict j ys).length ≤ q o) → B.domain ys) + {R : Resource B} {ν : ∀ j, B.X j → ProbDist (B.Y j)} {κ : ∀ o, A.X o → ProbDist (A.Y o)} + (hR : R.1 = memoryless B.inputDomain (portLaw ν)) + (hκ : ∀ s' o u, P.replyLaw ν s' o u b [] = (κ o u).1) : + (ofPreservingProgram s P hb ι hι q hA hB • R).1 = memoryless A.inputDomain (portLaw κ) := + -- As for `ofProgram_smul_memoryless`: this converter is again the converter of the DDC + -- `DDC.ofProgramOn s P A.domain`, and the same systems-level composition law applies. + PDCBehavior.attach_ofDDC_ofProgramOn_memoryless B.nonempty_prefix A.nonempty_prefix s P hb _ hκ hR + R.2 + +/-- **The composition law** for the converter of a port-preserving program with a memoryless +system `T` beside its inside interface (its own randomness, `≫ rightContext B T`): the program +is run against the side-by-side reply laws of `R` and `T`. -/ +lemma ofPreservingProgram_comp_rightContext_smul_memoryless {C : Interface} (s : S) + (P : Program S A.I (tensor B C).I A.X A.Y (tensor B C).X (tensor B C).Y) {b : ℕ} + (hb : P.Bounded b) (ι : A.I → Option (tensor B C).I) (hι : P.PortPreserving ι) + (q : A.I → ℕ) (hA : ∀ xs, A.domain xs → ∀ o, (SystemAlgebra.restrict o xs).length ≤ q o) + (hB : ∀ ys, ys ≠ [] → ys.length ≤ b * A.bound → + (∀ o j, ι o = some j → (SystemAlgebra.restrict j ys).length ≤ q o) → (tensor B C).domain ys) + {R : Resource B} {T : Resource C} {ν : ∀ j, B.X j → ProbDist (B.Y j)} + {ν' : ∀ k, C.X k → ProbDist (C.Y k)} {κ : ∀ o, A.X o → ProbDist (A.Y o)} + (hR : R.1 = memoryless B.inputDomain (portLaw ν)) + (hT : T.1 = memoryless C.inputDomain (portLaw ν')) + (hκ : ∀ s' o u, P.replyLaw (parallelLaw ν ν') s' o u b [] = (κ o u).1) : + ((ofPreservingProgram s P hb ι hι q hA hB ≫ rightContext B T) • R).1 = + memoryless A.inputDomain (portLaw κ) := by + -- Attaching `rightContext B T` places `T` beside `R` ... + -- (`Interface.comp_smul`: `(P ≫ K) • R = P • (K • R)`; `attach_rightContext`: + -- `rightContext B T • R = parallel R T`.) + rw [Interface.comp_smul, attach_rightContext] + -- ... a memoryless system with the side-by-side law, to which the program is attached. + -- `parallel_eq_memoryless`: `parallel R T` is the memoryless system of `parallelLaw ν ν'`. + exact ofPreservingProgram_smul_memoryless s P hb ι hι q hA hB (parallel_eq_memoryless hR hT) hκ + +end Converter + +end SystemAlgebra.Interface diff --git a/src/Examples.lean b/src/Examples.lean index dad9e27..b2ef0fc 100644 --- a/src/Examples.lean +++ b/src/Examples.lean @@ -4,10 +4,12 @@ import Examples.DSL.AEADTests import Examples.DSL.AES import Examples.DSL.Components import Examples.Games +import Examples.PRGLengthExtension import Examples.Substitution import Examples.Usability /-! Applications and examples: AES and components in the DSL, authenticated encryption with AES-CTR and PMAC, `(ind-cca, int-ptxt) → ae` (Banfi, Theorem 2.3.10(4), corrected), the proof -commands on interfaces, single substitutions, and games: reductions in any compatible solver -class and the collision step of authenticated encryption as a game. -/ +commands on interfaces, single substitutions, and games: reductions for the winners of any +`Games` instance and the collision step of authenticated encryption by conditional equivalence; +PRG length extension, whose hops are equalities of memoryless sources. -/ diff --git a/src/Examples/PRGLengthExtension.lean b/src/Examples/PRGLengthExtension.lean new file mode 100644 index 0000000..91d53b6 --- /dev/null +++ b/src/Examples/PRGLengthExtension.lean @@ -0,0 +1,286 @@ +import Commons.Definitions.Ideal +import ConstructiveCryptography.Tactics.Substitution + +/-! +# PRG length extension + +The 2-wise sequential composition of a length-doubling PRG `G : S → S × S` [1, §3.4.2, p. 59], + +``` + H(s) = (A, C, D) where (A, B) := G(s) and (C, D) := G(B), +``` + +is a secure PRG when `G` is, here with a fresh seed for every query: `prg-real^G` answers each +`eval(())` with `G(s)` for a fresh uniform seed `s`, and `prg-rand` is the beacon of uniform +samples [2, Example 3.2, p. 56], the memoryless source `MemorylessSource 𝒰[R]`. + +Every system of the proof is a memoryless source [2, Definition 3.1, p. 55], and the calling +programs `𝓡₁` and `𝓡₂` of the two swaps map memoryless sources to memoryless sources, with the +law of one invocation (the composition laws `Interface.Converter.*_smul_memoryless`). So each +hop is an equality of the laws of one reply: + +``` + system law of one reply to eval(()) (U = 𝒰[S]) + prg-real^H H_* U + = 𝓡₁ • prg-real^G (a, G b)_* (G_* U) H = (a, G b) ∘ G + ≃ 𝓡₁ • prg-rand (a, G b)_* U² + = 𝓡₂ • prg-real^G U ⊗ G_* U (a, b) ↦ (a, G b) is id × G + ≃ 𝓡₂ • prg-rand U ⊗ U² + = prg-rand U³ a product of uniform laws +``` + +## Main definitions + +* `H G`: the 2-wise sequential composition of `G` +* `PRGReal G`: `prg-real^G`, a fresh seed for every query +* `𝓡₁ G`, `𝓡₂ S`: the calling programs of the two swaps +* `PRGSamples G error`: PRG security with a fresh seed for every query + +## Main results + +* `prgReal_eq_source`: `prg-real^G` is the memoryless source of `G_* 𝒰[S]` +* `𝓡₁_smul_source`, `𝓡₂_smul_source`: `𝓡₁` and `𝓡₂` on memoryless sources +* `prgReal_H_eq`, `𝓡₁_smul_prgRand`, `𝓡₂_smul_prgRand`: the three hops +* `prg_length_extension`: `H` is a secure PRG within the losses of the two swaps + +## References + +1. D. Boneh and V. Shoup. *A Graduate Course in Applied Cryptography*. Version 0.6, 2023. +2. U. Maurer. *Cryptography Foundations*. Lecture notes, ETH Zurich, Spring 2018. +-/ + +namespace Examples.PRGLengthExtension + +open Commons Probability Probability.Distribution SystemAlgebra SystemAlgebra.DSL + SystemAlgebra.Interface RandomSystem +open scoped SystemAlgebra SystemAlgebra.DSL + +/-- **The 2-wise sequential composition** of `G` [1, §3.4.2]: `H(s) = (A, C, D)` for +`(A, B) := G(s)` and `(C, D) := G(B)`. -/ +def H {S : Type} (G : S → S × S) (seed : S) : S × S × S := + let (A, B) := G seed + let (C, D) := G B + (A, C, D) + +variable {S R : Type} [Fintype S] [Fintype R] + +-- `prg-real^G`: on `eval(())`, a fresh uniform seed `s`, and `G(s)`. +system PRGReal(G : S → R) [Nonempty S] : Evaluation Unit R + on eval(_input : Unit) → R + seed ←$ 𝒰[S] + return G seed + +-- `𝓡₁`: `(A, B) ← prg.eval(())`, and `(A, G(B))`. +converter 𝓡₁(G : S → S × S) : Evaluation Unit (S × S × S) + inside prg : Evaluation Unit (S × S) + on eval(_input : Unit) → S × S × S + (A, B) ← prg.eval(()) + return (A, G B) + +-- `𝓡₂`: a fresh uniform `A`, `(C, D) ← prg.eval(())`, and `(A, C, D)`. +converter 𝓡₂(S : Type) [Fintype S] [Nonempty S] : Evaluation Unit (S × S × S) + inside prg : Evaluation Unit (S × S) + on eval(_input : Unit) → S × S × S + A ←$ 𝒰[S] + CD ← prg.eval(()) + return (A, CD) + +noncomputable section + +variable {q : Evaluation.Port → ℕ} + +/-! ### The systems of the proof are memoryless sources -/ + +/-- **`prg-real^G` is the memoryless source of `G(s)` for a uniform seed `s`.** -/ +lemma prgReal_eq_source [Nonempty S] (G : S → R) : + PRGReal.perPort G (budget := q) = MemorylessSource.perPort R (ProbDist.map G 𝒰[S]) := by + -- Equal systems: compare their random systems. + apply Subtype.ext + -- `prg-real^G` is its program attached to its source of seeds: + -- + -- eval(()) ──► program ── randomness(()) ──► source, seeds s ← 𝒰[S] + -- ◄── eval ⇒ G s + -- + -- The source is memoryless, so by the composition law `prg-real^G` is memoryless with the law + -- of one invocation of the program. + have real : (PRGReal.perPort G (budget := q)).1 = + memoryless _ (portLaw fun _ _ => ProbDist.map G 𝒰[S]) := by + -- The composition law `Converter.ofProgram_smul_memoryless`, with the source of seeds + -- memoryless (`source_eq_memoryless`); the law of one invocation remains. + refine Converter.ofProgram_smul_memoryless none _ _ _ (source_eq_memoryless _ _) ?_ + -- One invocation: draw `s ← 𝒰[S]`, reply `G s`; the same in both initialization states. + -- The cases: initialization state `none` or `some ()`, the port `eval`, the input `()`. + rintro (_ | ⟨⟩) ⟨⟩ ⟨⟩ + · simp [Program.replyLaw, PRGReal.body, PRGReal.law1, callProg, returnProg, ProbDist.map, + bindK_single_comp] + · simp [Program.replyLaw, PRGReal.body, PRGReal.law1, callProg, returnProg, ProbDist.map, + bindK_single_comp] + -- The memoryless source of `G_* 𝒰[S]` is the same memoryless system. + rw [real, MemorylessSource.memoryless_eq] + +/-- **`𝓡₁` on the memoryless source** of `(A, B)` is the memoryless source of `(A, G(B))`. -/ +lemma 𝓡₁_smul_source (G : S → S × S) (ν : ProbDist (S × S)) : + 𝓡₁.perPort G (budget := q) • MemorylessSource.perPort (S × S) ν = + MemorylessSource.perPort (S × S × S) (ProbDist.map (fun AB => (AB.1, G AB.2)) ν) := by + -- Equal systems: compare their random systems. + apply Subtype.ext + -- One invocation of `𝓡₁` against the source of `ν`: + -- + -- eval(()) ──► 𝓡₁ ── prg.eval(()) ──► source of ν, prg.eval ⇒ (a, b) ← ν + -- ◄── eval ⇒ (a, G b) + have attached : (𝓡₁.perPort G (budget := q) • + MemorylessSource.perPort (S × S) ν (budget := 𝓡₁.insideBudget G q)).1 = + memoryless _ (portLaw fun _ _ => ProbDist.map (fun AB => (AB.1, G AB.2)) ν) := by + -- `𝓡₁.perPort` is the converter of a port-preserving program. + unfold 𝓡₁.perPort 𝓡₁.perPortProgram + -- The composition law for port-preserving programs, with the source of `ν` memoryless + -- (`MemorylessSource.memoryless_eq`); the law of one invocation remains. + refine Converter.ofPreservingProgram_smul_memoryless none _ _ _ _ _ _ _ + (MemorylessSource.memoryless_eq ν _) ?_ + -- The law of one invocation: one call, answered `(a, b) ← ν`, reply `(a, G b)`. + -- The cases: initialization state `none` or `some ()`, the port `eval`, the input `()`. + rintro (_ | ⟨⟩) ⟨⟩ ⟨⟩ + · simp [Program.replyLaw, 𝓡₁.body, callProg, returnProg, ProbDist.map, bindK_single_comp] + · simp [Program.replyLaw, 𝓡₁.body, callProg, returnProg, ProbDist.map, bindK_single_comp] + -- The memoryless source of `(a, G b)_* ν` is the same memoryless system. + rw [attached, MemorylessSource.memoryless_eq] + +/-- **`𝓡₂` on the memoryless source** of `(C, D)` is the memoryless source of `(A, C, D)` for a +uniform `A`. -/ +lemma 𝓡₂_smul_source [Nonempty S] (ν : ProbDist (S × S)) : + 𝓡₂.perPort S (budget := q) • MemorylessSource.perPort (S × S) ν = + MemorylessSource.perPort (S × S × S) (prodProbDist 𝒰[S] ν) := by + -- Equal systems: compare their random systems. + apply Subtype.ext + -- One invocation of `𝓡₂` against the source of `ν`, with its own source of `A`'s beside: + -- + -- eval(()) ──► 𝓡₂ ── randomness(()) ──► own source, randomness ⇒ a ← 𝒰[S] + -- ── prg.eval(()) ──► source of ν, prg.eval ⇒ (c, d) ← ν + -- ◄── eval ⇒ (a, c, d) + have attached : (𝓡₂.perPort S (budget := q) • + MemorylessSource.perPort (S × S) ν (budget := 𝓡₂.insideBudget S q)).1 = + memoryless _ (portLaw fun _ _ => prodProbDist 𝒰[S] ν) := by + -- `𝓡₂.perPort` is its program with its own source beside the inside interface. + unfold 𝓡₂.perPort 𝓡₂.perPortProgram 𝓡₂.randomness + -- The composition law with the converter's own source beside its inside interface: the + -- source of `ν` and the source of the `a`'s are memoryless (`MemorylessSource.memoryless_eq`, + -- `source_eq_memoryless`); the law of one invocation against their side-by-side laws + -- remains. + refine Converter.ofPreservingProgram_comp_rightContext_smul_memoryless none _ _ _ _ _ _ _ + (MemorylessSource.memoryless_eq ν _) (source_eq_memoryless _ _) ?_ + -- The law of one invocation: `a` from its own source, `(c, d)` from the source of `ν`, + -- reply `(a, c, d)`: the product of the two laws. + -- The cases: initialization state `none` or `some ()`, the port `eval`, the input `()`. + rintro (_ | ⟨⟩) ⟨⟩ ⟨⟩ + · simp [Program.replyLaw, 𝓡₂.body, 𝓡₂.law1, parallelLaw, callProg, returnProg, + prod_eq_bindK, bindK_single_comp] + · simp [Program.replyLaw, 𝓡₂.body, 𝓡₂.law1, parallelLaw, callProg, returnProg, + prod_eq_bindK, bindK_single_comp] + -- The memoryless source of `𝒰[S] ⊗ ν` is the same memoryless system. + rw [attached, MemorylessSource.memoryless_eq] + +/-! ### The hops -/ + +variable [Nonempty S] + +/-- `(A, G(B))` for a uniform `(A, B)` is a uniform `A` beside `G(s)` for a uniform `s`. -/ +lemma map_uniform_eq_prod (G : S → S × S) : + ProbDist.map (fun AB => (AB.1, G AB.2)) 𝒰[S × S] = + prodProbDist 𝒰[S] (ProbDist.map G 𝒰[S]) := by + -- Equal laws: compare their distributions. + apply Subtype.ext + -- `(a, b) ↦ (a, G b)` is the product map `id × G` ... + change fTransform (Prod.map id G) (Distribution.uniform (S × S)) = _ + -- ... 𝒰[S × S] is 𝒰[S] ⊗ 𝒰[S] ... + rw [← prod_uniform] + -- ... a product map acts factor by factor ... + rw [fTransform_prod] + -- ... and `id` leaves 𝒰[S] unchanged. + rw [fTransform_id] + rfl + +/-- **The first hop**, factoring out the first call of `G`: `prg-real^H` is `𝓡₁` on +`prg-real^G`. -/ +lemma prgReal_H_eq (G : S → S × S) (q : Evaluation.Port → ℕ) : + PRGReal.perPort (H G) (budget := q) = + 𝓡₁.perPort G • PRGReal.perPort G (budget := 𝓡₁.insideBudget G q) := by + -- Left: prg-real^H = source of H_* U + -- Right: 𝓡₁ • prg-real^G = 𝓡₁ • source of G_* U = source of (a, G b)_* (G_* U) + rw [prgReal_eq_source (H G), prgReal_eq_source G, 𝓡₁_smul_source] + -- Pushing forward twice is pushing forward along `(a, G b) ∘ G`, which is `H`. + rw [ProbDist.map_map] + rfl + +/-- **The middle hop**: `𝓡₁` on `prg-rand` is `𝓡₂` on `prg-real^G`, a uniform `A` beside `G(s)` +for a uniform `s` either way. -/ +lemma 𝓡₁_smul_prgRand (G : S → S × S) (q : Evaluation.Port → ℕ) : + 𝓡₁.perPort G (budget := q) • + MemorylessSource.perPort (S × S) 𝒰[S × S] (budget := 𝓡₁.insideBudget G q) = + 𝓡₂.perPort S • PRGReal.perPort G (budget := 𝓡₂.insideBudget S q) := by + -- Left: 𝓡₁ • prg-rand = source of (a, G b)_* 𝒰[S × S] + rw [𝓡₁_smul_source] + -- Right: 𝓡₂ • prg-real^G = 𝓡₂ • source of G_* 𝒰[S] = source of 𝒰[S] ⊗ G_* 𝒰[S] + rw [prgReal_eq_source, 𝓡₂_smul_source] + -- Equal laws: `(a, G b)` for a uniform pair is a uniform `a` beside `G` of a uniform seed. + rw [map_uniform_eq_prod] + +/-- **The last hop**: `𝓡₂` on `prg-rand` is `prg-rand` on `S × S × S`, a uniform `A` beside a +uniform `(C, D)`. -/ +lemma 𝓡₂_smul_prgRand (q : Evaluation.Port → ℕ) : + 𝓡₂.perPort S (budget := q) • + MemorylessSource.perPort (S × S) 𝒰[S × S] (budget := 𝓡₂.insideBudget S q) = + MemorylessSource.perPort (S × S × S) 𝒰[S × S × S] (budget := q) := by + -- Left: 𝓡₂ • prg-rand = source of 𝒰[S] ⊗ 𝒰[S × S] + rw [𝓡₂_smul_source] + -- Equal laws: a product of uniform laws is the uniform law on the product. + rw [show prodProbDist 𝒰[S] 𝒰[S × S] = 𝒰[S × S × S] from Subtype.ext prod_uniform] + +/-! ### Security -/ + +/-- **PRG security with a fresh seed for every query** within `error`: against the admitted +distinguishers, `prg-real^G` substitutes for `prg-rand`, the beacon of uniform samples. -/ +def PRGSamples [AdmissibleDistinguishers] [Nonempty R] (G : S → R) + {q : Evaluation.Port → ℕ} + (error : (Evaluation.perPort Unit R q).inputDomain.DistinguisherBehavior → ENNReal) : Prop := + PRGReal.perPort G (budget := q) ≃[error] MemorylessSource.perPort R 𝒰[R] (budget := q) + +/-- **PRG length extension**, as [1, Theorem 3.3] for `n = 2` with a fresh seed for every query: +if `G` is a secure PRG within `ε`, then `H` is a secure PRG within the losses of the two swaps. -/ +theorem prg_length_extension [AdmissibleDistinguishers] (G : S → S × S) + {q : Evaluation.Port → ℕ} + (ε : (Evaluation.perPort Unit (S × S) (𝓡₁.insideBudget G q)).inputDomain.DistinguisherBehavior + → ENNReal) + (secure : PRGSamples G ε) : + PRGSamples (H G) (q := q) fun D => + ε (absorb (𝓡₁.perPort G) D) + ε (absorb (𝓡₂.perPort S) D) := by + -- The hybrids, as systems (the distinguisher D on the left): + -- + -- D ─ prg-real^H start + -- D ─ 𝓡₁ ─ prg-real^G = factor out prgReal_H_eq + -- D ─ 𝓡₁ ─ prg-rand ≃[ε(D ∘ 𝓡₁)] swap: G is secure + -- D ─ 𝓡₂ ─ prg-real^G = middle hop 𝓡₁_smul_prgRand + -- D ─ 𝓡₂ ─ prg-rand ≃[ε(D ∘ 𝓡₂)] swap: G is secure + -- D ─ prg-rand = last hop 𝓡₂_smul_prgRand + -- + -- One chain: the equalities cost nothing, each swap costs `ε` at the distinguisher with the + -- calling converter absorbed, and the losses add up. + cc_calc quantitative (distinguisherAdvantage AdmissibleDistinguishers.admissible) + -- The first hop: factor out the first call of `G`. + PRGReal.perPort (H G) = 𝓡₁.perPort G • PRGReal.perPort G := prgReal_H_eq G q + -- The first swap: `prg-real^G` ≃ `prg-rand` (`secure`), attached through `𝓡₁`; its loss is + -- `ε` at `D` with `𝓡₁` absorbed (`substitutesWithin_attach`). + _ ≃[fun D => ε (absorb (𝓡₁.perPort G) D)] + 𝓡₁.perPort G • MemorylessSource.perPort (S × S) 𝒰[S × S] := + AdmissibleDistinguishers.substitutesWithin_attach _ secure + -- The middle hop: both are the memoryless source of `𝒰[S] ⊗ G_* 𝒰[S]`. + _ = 𝓡₂.perPort S • PRGReal.perPort G := 𝓡₁_smul_prgRand G q + -- The second swap, through `𝓡₂`; its loss is `ε` at `D` with `𝓡₂` absorbed. + _ ≃[fun D => ε (absorb (𝓡₂.perPort S) D)] + 𝓡₂.perPort S • MemorylessSource.perPort (S × S) 𝒰[S × S] := + AdmissibleDistinguishers.substitutesWithin_attach _ secure + -- The last hop: both are the memoryless source of `𝒰[S × S × S]`. + _ = MemorylessSource.perPort (S × S × S) 𝒰[S × S × S] := 𝓡₂_smul_prgRand q + +end + +end Examples.PRGLengthExtension diff --git a/src/RandomSystems.lean b/src/RandomSystems.lean index 64e17ec..828d014 100644 --- a/src/RandomSystems.lean +++ b/src/RandomSystems.lean @@ -9,6 +9,7 @@ import RandomSystems.Converter.PartialConverter import RandomSystems.Converter.PartialIdentity import RandomSystems.Converter.Program import RandomSystems.Converter.ProgramAttachment +import RandomSystems.Converter.ProbProgramAttachment import RandomSystems.Converter.ParallelPDS import RandomSystems.Converter.PDCBehavior import RandomSystems.Converter.ResourceAttachment @@ -49,10 +50,13 @@ import RandomSystems.PDS.PDS import RandomSystems.System.Basic import RandomSystems.System.DDE import RandomSystems.System.InterfaceSystem +import RandomSystems.System.Memoryless import RandomSystems.System.Observation +import RandomSystems.System.ProbAutomaton import RandomSystems.System.Replies /-! Random systems: raw systems and connection, deterministic converters, PDSs, cumulative random -systems, converters and attachment, parallel composition, distance and games. +systems, probabilistic automata and memoryless systems, converters and attachment, parallel +composition, distance and games. -/ diff --git a/src/RandomSystems/Converter/ProbProgramAttachment.lean b/src/RandomSystems/Converter/ProbProgramAttachment.lean new file mode 100644 index 0000000..4af207a --- /dev/null +++ b/src/RandomSystems/Converter/ProbProgramAttachment.lean @@ -0,0 +1,1174 @@ +import RandomSystems.Converter.ProgramAttachment +import RandomSystems.Converter.ConverterAttachment +import RandomSystems.System.ProbAutomaton + +/-! +# Attaching a program to a probabilistic automaton + +Run against a probabilistic automaton, a program answers each outside query by an invocation in +which the automaton answers the inside queries, from its state, with fresh steps. This is again a +probabilistic automaton, on pairs of states (`Program.probCombine`). The main theorem says that it +is the attachment of the program's converter to the automaton, as random systems: + +``` + u ┌─────┐ q ┌───────────┐ + ─────────────────►│ P ├───────────►│ automaton │ = ┌─────────────────────┐ + ◄─────────────────┤ (s) │◄───────────┤ (step, r) │ │ P run against step │ + v └─────┘ y └───────────┘ │ from (s, r) │ + └─────────────────────┘ +``` + +A system `C(·)` invoking an internal system `F` is the combined system `C(F)` [1, §3.3]; for a +deterministic automaton this is the inlining theorem `Program.inline_automatonSystem`. The +probabilistic case is reduced to it: a probabilistic automaton is a random automaton in the sense +of [1, Definition 2], a deterministic automaton whose internal randomness, a table of the draws of +every step from every reachable state, is sampled once with the initial state. Reading this table +in order is drawing afresh (a simulation, `simulatesAt_drawStep`), the program attached to each +deterministic automaton is the combined automaton, and the program respects simulations. + +## Main definitions + +* `Program.probInvoke`, `Program.probCombine`: an invocation against a probabilistic step, and + the program run against a probabilistic automaton, a probabilistic automaton on pairs of states +* `ProbStep.reachable`, `ProbStep.recording`, `ProbStep.drawStep`, `ProbStep.drawKernel`: the + states reachable from the initial law, the step recording its draws, the deterministic step + reading pre-sampled draws, and the law of the draws given the recorded ones + +## Main results + +* `Program.ofDeterministic_combine`: against a deterministic automaton, the program run against its + point steps is the combined automaton +* `Program.simulatesAt_probCombine`, `RandomSystem.ofProbAutomaton_probCombine_eq_of_simulation`: + a program respects simulations of the automaton it is run against +* `RandomSystem.ofProbAutomaton_eq_drawStep`: a probabilistic automaton is a deterministic + automaton reading pre-sampled draws +* `PDCBehavior.attach_ofDDC_ofProgramOn_ofDeterministic`: attaching a program to a deterministic + automaton with a random initial state +* `PDCBehavior.attach_ofDDC_ofProgramOn_ofProbAutomaton`: attaching a program to a probabilistic + automaton is the program run against it + +## References + +1. U. Maurer. Indistinguishability of Random Systems. In *Advances in Cryptology – EUROCRYPT + 2002*, LNCS 2332, Springer, 2002. +-/ + +namespace SystemAlgebra + +open Probability Probability.Distribution + +variable {S O J R : Type} {U V : O → Type} {X Y : J → Type} + +/-! ### Programs against probabilistic steps -/ + +namespace Program + +variable (P : Program S O J U V X Y) (stepR : ProbStep R J X Y) + +/-- **An invocation against a probabilistic step**: the body runs from the exchanges `h`, the +automaton in the state `r` answering its inside queries, with at most `n` more of them; the law +of the next states and of the reply. + +``` + body(h) = reply (s', v) ⟶ point law at ((s', r), v) + body(h) = query q ⟶ (r', y) ← step r q; continue from r' with h · (q, y) +``` +-/ +noncomputable def probInvoke (s : S) (o : O) (u : U o) : + ℕ → R → List ((Σ j, X j) × (Σ j, Y j)) → Distribution ((S × R) × V o) + -- One invocation: the outside query `u` enters the body, whose inside queries the automaton + -- answers with fresh steps from `r`, until the body replies `v`: + -- + -- u ──►┌──────┐── q₁, q₂, … ──►┌──────────┐ + -- │ P(s) │ │ stepR, r │ r ─► r₁ ─► r₂ ─► … (fresh draws) + -- v ◄──└──────┘◄── y₁, y₂, … ──└──────────┘ + -- + -- No query left: a reply is its point law, a further query gets no mass. + | 0, r, h => match P s o u h with + | .inl a => Finsupp.single ((a.1, r), a.2) 1 + | .inr _ => 0 + -- Queries left: a further query `q` is answered by a draw `(r', y)` of the step from `r`. + | n + 1, r, h => match P s o u h with + | .inl a => Finsupp.single ((a.1, r), a.2) 1 + | .inr q => bindK (stepR.outcome r q) fun p => probInvoke s o u n p.1 (h ++ [(q, p.2)]) + +variable {P stepR} + +/-- When the body replies, the invocation is the point law of its reply. -/ +lemma probInvoke_inl {s : S} {o : O} {u : U o} {h : List ((Σ j, X j) × (Σ j, Y j))} + {a : S × V o} (ha : P s o u h = .inl a) (n : ℕ) (r : R) : + P.probInvoke stepR s o u n r h = Finsupp.single ((a.1, r), a.2) 1 := by + -- Whatever the number of queries left, the first case of the definition. + cases n <;> simp [probInvoke, ha] + +/-- When the body asks with no query left, the invocation has no mass. -/ +lemma probInvoke_zero_inr {s : S} {o : O} {u : U o} {h : List ((Σ j, X j) × (Σ j, Y j))} + {q : Σ j, X j} (hq : P s o u h = .inr q) (r : R) : + P.probInvoke stepR s o u 0 r h = 0 := by + -- The second case of the definition with no query left. + simp [probInvoke, hq] + +/-- When the body asks `q`, the invocation draws a step and continues. -/ +lemma probInvoke_succ_inr {s : S} {o : O} {u : U o} {h : List ((Σ j, X j) × (Σ j, Y j))} + {q : Σ j, X j} (hq : P s o u h = .inr q) (n : ℕ) (r : R) : + P.probInvoke stepR s o u (n + 1) r h = + bindK (stepR.outcome r q) fun p => P.probInvoke stepR s o u n p.1 (h ++ [(q, p.2)]) := by + -- The second case of the definition with a query left. + simp [probInvoke, hq] + +/-- An invocation is a nonnegative law. -/ +lemma probInvoke_nonNeg (s : S) (o : O) (u : U o) : + ∀ n r h, (P.probInvoke stepR s o u n r h).NonNeg := by + -- Induction on the number of queries left: point laws, zero, or mixtures of nonnegative laws. + intro n + induction n with + | zero => + intro r h + cases hq : P s o u h with + -- the body replies: a point law + | inl a => rw [probInvoke_inl hq]; exact (isProbDist_single _).1 + -- the body asks with no query left: the zero law + | inr q => rw [probInvoke_zero_inr hq]; exact fun _ => le_rfl + | succ n ih => + intro r h + cases hq : P s o u h with + -- the body replies: a point law + | inl a => rw [probInvoke_inl hq]; exact (isProbDist_single _).1 + | inr q => + -- the body asks `q`: the step's draws, a nonnegative law, mixing nonnegative + -- continuations (induction) + rw [probInvoke_succ_inr hq] + exact bindK_nonNeg (stepR.outcome_nonNeg r q) fun _ => ih _ _ + +/-- **A bounded program completes each invocation** against a probabilistic step. -/ +lemma probInvoke_weight {b : ℕ} (hP : P.Bounded b) (s : S) (o : O) (u : U o) : + ∀ n r h, P.Consistent s o u h → b ≤ n + h.length → + (P.probInvoke stepR s o u n r h).weight = 1 := by + -- Plan: induction on the number `n` of inside queries left, keeping `b ≤ n + |h|`: the + -- queries left and the queries the body has made reach its bound `b`. + -- 1. No query left: a reply is a point law, of weight one; a query cannot happen, since + -- the body has made `|h| ≥ b` queries and a bounded body asks only after fewer than `b`. + -- 2. `n + 1` queries left: a reply as in 1; a query `q` is a draw of the step, a probability + -- law, followed from each possible draw by a continuation of weight one (induction). + intro n + induction n with + -- Step 1: no query left. + | zero => + intro r h hc hb + cases hq : P s o u h with + | inl a => + -- the body replies: a point law + rw [probInvoke_inl hq]; exact (isProbDist_single _).2 + | inr q => + -- a query with no query left: impossible, the body has made its `b` queries already + exact absurd (hP s o u h q hc hq) (by omega) + -- Step 2: `n + 1` queries left. + | succ n ih => + intro r h hc hb + cases hq : P s o u h with + | inl a => + -- the body replies: a point law + rw [probInvoke_inl hq]; exact (isProbDist_single _).2 + | inr q => + -- the body asks `q`: a draw of the step, then the rest of the invocation + rw [probInvoke_succ_inr hq] + -- every continuation completes (induction), so the mixture keeps the weight ... + rw [weight_bindK_of_weight fun p hp => ?_] + -- ... of the step, a probability law + · exact stepR.weight_outcome r q + -- a possible draw replies at `q`'s port, and the body's exchanges grow by one + obtain ⟨y, hy⟩ := stepR.mem_support_outcome hp + rw [hy] + exact ih _ _ (hc.snoc hq y) (by simp; omega) + +variable (P stepR) in +/-- **The program run against a probabilistic automaton**, a probabilistic automaton on pairs of +states: each outside query runs an invocation, the automaton answering its inside queries. -/ +noncomputable def probCombine {b : ℕ} (hP : P.Bounded b) : ProbStep (S × R) O U V := + -- From `(s, r)` at `⟨o, u⟩`: the invocation from no exchanges with the whole budget `b`, a + -- nonnegative law of weight one since the program is bounded. + fun sr o u => ⟨P.probInvoke stepR sr.1 o u b sr.2 [], + probInvoke_nonNeg sr.1 o u b sr.2 [], + probInvoke_weight hP sr.1 o u b sr.2 [] (consistent_nil P _ _ _) (by simp)⟩ + +/-- The law of a combined step is the invocation from the empty exchanges. -/ +lemma probCombine_val {b : ℕ} (hP : P.Bounded b) (sr : S × R) (o : O) (u : U o) : + (P.probCombine stepR hP sr o u).1 = P.probInvoke stepR sr.1 o u b sr.2 [] := rfl + +/-- Against a deterministic automaton, an invocation is the point law of its completion. -/ +lemma probInvoke_ofDeterministic (stepD : R → (j : J) → X j → R × Y j) (s : S) (o : O) + (u : U o) : ∀ n r h v, P.invoke stepD s o u n r h = some v → + P.probInvoke (ProbStep.ofDeterministic stepD) s o u n r h = Finsupp.single v 1 := by + -- Plan: induction on the number `n` of inside queries left, along the deterministic + -- invocation, which completes with `v`. + -- 1. No query left: the body replies and both invocations give its reply; a query would + -- leave the deterministic invocation incomplete. + -- 2. `n + 1` queries left: a reply as in 1; on a query `q` the point step has the single + -- outcome `stepD r q`, so the invocation is its continuation from it (induction). + intro n + induction n with + -- Step 1: no query left. + | zero => + intro r h v hv + cases hq : P s o u h with + | inl a => + -- the body replies: both are its reply + simp only [invoke, hq, Sum.elim_inl, Option.some.injEq] at hv + rw [probInvoke_inl hq, hv] + | inr q => + -- the body asks with no query left: the invocation does not complete + simp [invoke, hq] at hv + -- Step 2: `n + 1` queries left. + | succ n ih => + intro r h v hv + cases hq : P s o u h with + | inl a => + -- the body replies: both are its reply + simp only [invoke, hq, Option.some.injEq] at hv + rw [probInvoke_inl hq, ← hv] + | inr q => + -- the body asks `q`: the invocation draws a step ... + simp only [invoke, hq] at hv + rw [probInvoke_succ_inr hq] + -- ... a point step, whose single outcome is the automaton's answer ... + rw [ProbStep.outcome_ofDeterministic, bindK_single, one_smul] + -- ... and continues as the deterministic invocation (induction) + exact ih _ _ v hv + +/-- **A program against a deterministic automaton**: the program run against its point steps is +the point step of the combined automaton. -/ +lemma ofDeterministic_combine (stepD : R → (j : J) → X j → R × Y j) {b : ℕ} + (hP : P.Bounded b) : + ProbStep.ofDeterministic (P.combine stepD hP) = + P.probCombine (ProbStep.ofDeterministic stepD) hP := by + -- Compare the laws of each step, from each pair of states, at each query. + funext sr o u + apply Subtype.ext + -- The invocation against the automaton completes with the combined step ... + have hinvoke := invoke_eq_combine stepD hP sr o u + -- ... so the invocation against its point steps is the point law of the combined step. + exact (probInvoke_ofDeterministic stepD sr.1 o u b sr.2 [] _ hinvoke).symm + +/-! ### Programs along simulations -/ + +section Simulation + +variable {R₁ R₂ : Type} {stepR₁ : ProbStep R₁ J X Y} {stepR₂ : ProbStep R₂ J X Y} + {K : R₁ → Distribution.ProbDist R₂} {E : List (Σ j, X j) → Prop} + {invR : List (Σ j, X j) → R₁ → Prop} + +variable (P) in +/-- After the inside queries `τ`, every inside query of an invocation at `⟨o, u⟩` in the state `s` +is admitted by `E`. -/ +def AdmitsInvocation (E : List (Σ j, X j) → Prop) (s : S) (o : O) (u : U o) + (τ : List (Σ j, X j)) : Prop := + ∀ h q, P.Consistent s o u h → P s o u h = .inr q → E (τ ++ h.map Prod.fst ++ [q]) + +/-- **An invocation along simulation steps** of the inside automata: from the kernel image of `r`, +the invocation against `stepR₂` is the invocation against `stepR₁` followed by the kernel. -/ +lemma probInvoke_simulation + (hsim : ∀ τ r q, invR τ r → E (τ ++ [q]) → ProbStep.SimulatesAt stepR₁ stepR₂ K r q) + (hpres : ∀ τ r q, invR τ r → E (τ ++ [q]) → + ∀ p ∈ (stepR₁.outcome r q).support, invR (τ ++ [q]) p.1) + (s : S) (o : O) (u : U o) (τ : List (Σ j, X j)) (hgood : P.AdmitsInvocation E s o u τ) : + ∀ n r h, P.Consistent s o u h → invR (τ ++ h.map Prod.fst) r → + (bindK (K r).1 fun r₂ => P.probInvoke stepR₂ s o u n r₂ h) = + bindK (P.probInvoke stepR₁ s o u n r h) fun p => + fTransform (fun r₂ => ((p.1.1, r₂), p.2)) (K p.1.2).1 := by + -- The square to prove, for an invocation from the exchanges `h` with `n` queries left: + -- + -- r ──── P against stepR₁ ────► ((s', r'), v) + -- │ │ + -- K K on r' + -- ▼ ▼ + -- r₂ ─── P against stepR₂ ────► ((s', r₂'), v) + -- + -- Plan: induction on `n`. + -- 1. The body replies on `h`: no inside step; both sides are the kernel image of `r`, + -- paired with the body's state and reply, which depend on `h` only. + -- 2. The body asks with no query left: no mass on both sides. + -- 3. The body asks `q` with `n + 1` queries left: `q` is admitted and `invR` holds at `r`, + -- so one inside step is a simulation square; the next state keeps `invR`, so the rest of + -- the invocation is a square by induction. Glue the two squares: + -- + -- r ── stepR₁, q ──► (r', y) ── rest against stepR₁ ──► ((s', r''), v) + -- │ │ │ + -- K (simulation at r) K (induction hypothesis) K + -- ▼ ▼ ▼ + -- r₂ ── stepR₂, q ──► (r₂', y) ── rest against stepR₂ ──► ((s', r₂''), v) + -- + intro n + induction n with + | zero => + intro r h _ _ + cases hq : P s o u h with + -- Step 1, with no query left. + | inl a => + -- the body replies: the inside state is only moved by the kernel + simp only [probInvoke_inl hq, bindK_single, one_smul] + -- a point kernel along `r₂ ↦ ((s', r₂), v)` is the pushforward of `K r` along it + exact bindK_single_comp _ _ + -- Step 2. + | inr q => + -- the body asks with no query left: no mass on both sides + simp only [probInvoke_zero_inr hq, bindK_zero, bindK_zero_right] + | succ n ih => + intro r h hc hr + cases hq : P s o u h with + -- Step 1, with `n + 1` queries left. + | inl a => + -- the body replies: the inside state is only moved by the kernel + simp only [probInvoke_inl hq, bindK_single, one_smul] + exact bindK_single_comp _ _ + -- Step 3. + | inr q => + -- the body asks `q`, which is admitted, so the simulation step applies at `r` + have hE := hgood h q hc hq + have hs := hsim _ r q hr hE + unfold ProbStep.SimulatesAt at hs + -- on both sides the invocation draws an inside step on `q`, then continues + simp only [probInvoke_succ_inr hq] + -- Left square, then right square, along the chain: + -- K, then (stepR₂, then rest₂) + -- = (K, then stepR₂), then rest₂ (associativity) + -- = stepR₁, then (K, then rest₂) (simulation at `r`) + -- = stepR₁, then (rest₁, then K) (induction hypothesis) + -- = (stepR₁, then rest₁), then K (associativity) + calc (bindK (K r).1 fun r₂ => bindK (stepR₂.outcome r₂ q) fun p => + P.probInvoke stepR₂ s o u n p.1 (h ++ [(q, p.2)])) + -- regroup: first the step of `stepR₂` from the kernel image of `r` + = bindK (bindK (K r).1 fun r₂ => stepR₂.outcome r₂ q) fun p => + P.probInvoke stepR₂ s o u n p.1 (h ++ [(q, p.2)]) := (bindK_bindK _ _ _).symm + -- simulation step: a step of `stepR₁` from `r`, then the kernel + _ = bindK (stepR₁.outcome r q) fun p => bindK (K p.1).1 fun r₂ => + P.probInvoke stepR₂ s o u n r₂ (h ++ [(q, p.2)]) := by + -- the simulation step at `r` + rw [hs] + -- regroup: for each outcome `p` of `stepR₁`, the kernel image of its next state + rw [bindK_bindK] + refine bindK_congr fun p _ => ?_ + -- pairing the kernel image with the reply `p.2`, then continuing, is continuing + -- from the kernel image with `(q, p.2)` appended + rw [bindK_fTransform] + rfl + -- the rest of the invocation along the simulation (induction hypothesis) + _ = bindK (stepR₁.outcome r q) fun p => + bindK (P.probInvoke stepR₁ s o u n p.1 (h ++ [(q, p.2)])) fun p' => + fTransform (fun r₂ => ((p'.1.1, r₂), p'.2)) (K p'.1.2).1 := + bindK_congr fun p hp => by + -- a possible draw replies at `q`'s port: the body's exchanges grow by one ... + obtain ⟨y, hy⟩ := stepR₁.mem_support_outcome hp + refine ih _ _ (hy ▸ hc.snoc hq y) ?_ + -- ... and the next state keeps the invariant + have := hpres _ r q hr hE p hp + -- the inside queries of `h · (q, y)` are those of `h`, then `q` + simpa using this + -- regroup the two mixtures + _ = _ := (bindK_bindK _ _ _).symm + +/-- **The end of an invocation**: each outcome of an invocation is the reply of the body on its +own exchanges extending `h`, with the invariant on the inside queries made. -/ +lemma probInvoke_support + (hpres : ∀ τ r q, invR τ r → E (τ ++ [q]) → + ∀ p ∈ (stepR₁.outcome r q).support, invR (τ ++ [q]) p.1) + (s : S) (o : O) (u : U o) (τ : List (Σ j, X j)) (hgood : P.AdmitsInvocation E s o u τ) : + ∀ n r h, P.Consistent s o u h → invR (τ ++ h.map Prod.fst) r → + ∀ p ∈ (P.probInvoke stepR₁ s o u n r h).support, ∃ hf, P.Consistent s o u hf ∧ + h <+: hf ∧ P s o u hf = .inl (p.1.1, p.2) ∧ invR (τ ++ hf.map Prod.fst) p.1.2 := by + -- Plan: induction on the number `n` of inside queries left; the exchanges `hf` are those + -- on which the body replies. + -- 1. The body replies on `h`: the only outcome is its reply, with `hf = h`. + -- 2. The body asks with no query left: no outcome. + -- 3. The body asks `q` with `n + 1` queries left: an outcome comes from a possible draw + -- `(r', y)` of the step and an outcome of the rest of the invocation from `h · (q, y)`. + -- The query is admitted, so `r'` keeps the invariant (`hpres`); by induction the rest + -- ends on exchanges `hf` extending `h · (q, y)`, hence `h`. + intro n + induction n with + | zero => + intro r h hc hr p hp + cases hq : P s o u h with + -- Step 1, with no query left. + | inl a => + -- the body replies on `h` itself: the outcome is its reply + rw [probInvoke_inl hq, Finsupp.mem_support_single] at hp + rw [hp.1] + -- `hf = h`: the body's own exchanges, a prefix of themselves, with the invariant + exact ⟨h, hc, List.prefix_refl _, hq, hr⟩ + -- Step 2. + | inr q => + -- no query left: no outcome + rw [probInvoke_zero_inr hq] at hp; simp at hp + | succ n ih => + intro r h hc hr p hp + cases hq : P s o u h with + -- Step 1, with `n + 1` queries left. + | inl a => + -- the body replies on `h` itself: the outcome is its reply + rw [probInvoke_inl hq, Finsupp.mem_support_single] at hp + rw [hp.1] + exact ⟨h, hc, List.prefix_refl _, hq, hr⟩ + -- Step 3. + | inr q => + -- the outcome comes from a possible draw `p'` and the rest of the invocation + rw [probInvoke_succ_inr hq] at hp + obtain ⟨p', hp', hp⟩ := mem_support_bindK hp + -- the draw replies at `q`'s port: `p' = (r', ⟨q.1, y⟩)` + obtain ⟨y, hy⟩ := stepR₁.mem_support_outcome hp' + -- the draw keeps the invariant on the inside queries made + have hr' : invR (τ ++ (h ++ [(q, p'.2)]).map Prod.fst) p'.1 := by + simpa using hpres _ r q hr (hgood h q hc hq) p' hp' + -- the rest of the invocation ends on exchanges extending `h · (q, y)` (induction) + obtain ⟨hf, hcf, hpf, hf₁, hf₂⟩ := ih _ _ (hy ▸ hc.snoc hq y) hr' p hp + -- `h` is a prefix of `h · (q, y)`, hence of `hf` + exact ⟨hf, hcf, (List.prefix_append h _).trans hpf, hf₁, hf₂⟩ + +/-- The kernel on the inside state, the program state unchanged. -/ +noncomputable def insideKernel (K : R₁ → Distribution.ProbDist R₂) (sr : S × R₁) : + Distribution.ProbDist (S × R₂) := + (K sr.2).map fun r₂ => (sr.1, r₂) + +variable (P) in +/-- **A program respects simulations**: when the inside queries of an invocation are admitted +and simulated, the program run against `stepR₂` simulates the program run against `stepR₁` along +the kernel on the inside state. -/ +lemma simulatesAt_probCombine {b : ℕ} (hP : P.Bounded b) + (hsim : ∀ τ r q, invR τ r → E (τ ++ [q]) → ProbStep.SimulatesAt stepR₁ stepR₂ K r q) + (hpres : ∀ τ r q, invR τ r → E (τ ++ [q]) → + ∀ p ∈ (stepR₁.outcome r q).support, invR (τ ++ [q]) p.1) + {s : S} {r : R₁} {τ : List (Σ j, X j)} (hr : invR τ r) {x : Σ o, U o} + (hgood : P.AdmitsInvocation E s x.1 x.2 τ) : + ProbStep.SimulatesAt (P.probCombine stepR₁ hP) (P.probCombine stepR₂ hP) (insideKernel K) + (s, r) x := by + -- One step of the two combined automata at the outside query `⟨o, u⟩`, the kernel `K` + -- acting on the inside state only: + -- + -- (s, r) ── P against stepR₁, ⟨o, u⟩ ──► ((s', r'), v) + -- │ │ + -- K K + -- ▼ ▼ + -- (s, r₂) ── P against stepR₂, ⟨o, u⟩ ──► ((s', r₂'), v) + -- + -- It is the square of one invocation (`probInvoke_simulation`), the reply tagged by `o`. + obtain ⟨o, u⟩ := x + -- The invocations from the empty exchanges, along the simulation. + have hinv := probInvoke_simulation (P := P) hsim hpres s o u τ hgood b r [] + (consistent_nil P _ _ _) (by simpa using hr) + -- Unfold the outcomes of the combined steps into the invocations, tagged by the port. + unfold ProbStep.SimulatesAt + simp only [insideKernel, ProbDist.map_val, ProbStep.outcome, probCombine_val, bindK_fTransform, + Function.comp_def] + -- Tag after mixing: the left side is the tagged invocation from the kernel image of `r` ... + rw [← fTransform_bindK] + -- ... which is the invocation from `r` followed by the kernel (`hinv`) ... + rw [hinv] + -- ... tagged; compare outcome by outcome. + rw [fTransform_bindK] + refine bindK_congr fun p _ => ?_ + -- both sides push `K` of the final inside state along the same map + simp only [fTransform_fTransform, Function.comp_def] + rfl + +variable (P) in +/-- The outcomes of the program run against `stepR₁` come from the body's own exchanges, with the +invariant on the inside queries made. -/ +lemma probCombine_support {b : ℕ} (hP : P.Bounded b) + (hpres : ∀ τ r q, invR τ r → E (τ ++ [q]) → + ∀ p ∈ (stepR₁.outcome r q).support, invR (τ ++ [q]) p.1) + {s : S} {r : R₁} {τ : List (Σ j, X j)} (hr : invR τ r) {x : Σ o, U o} + (hgood : P.AdmitsInvocation E s x.1 x.2 τ) : + ∀ p ∈ ((P.probCombine stepR₁ hP).outcome (s, r) x).support, ∃ hf, + P.Consistent s x.1 x.2 hf ∧ invR (τ ++ hf.map Prod.fst) p.1.2 := by + intro p hp + -- An outcome is a tagged outcome `p'` of the invocation from the empty exchanges ... + obtain ⟨p', hp', rfl⟩ := mem_support_fTransform _ _ hp + -- ... which ends on the body's own exchanges `hf`, with the invariant. + obtain ⟨hf, hcf, -, -, hinv⟩ := probInvoke_support (P := P) hpres s x.1 x.2 τ hgood b r [] + (consistent_nil P _ _ _) (by simpa using hr) p' hp' + exact ⟨hf, hcf, hinv⟩ + +end Simulation + +end Program + +section + +variable [Fintype (Σ o, U o)] [Fintype (Σ o, V o)] + +/-- **A program respects simulations, as random systems**: if `stepR₂` simulates `stepR₁` along +`K` at the states satisfying an invariant of the inside queries so far, at every inside query +before the program's total budget `b * n`, then the program run against the two automata gives +the same random system on the outside domain `F`, of at most `n` queries. + +``` + P run against stepR₁ from (s, r) = P run against stepR₂ from (s, K r) +``` +-/ +lemma RandomSystem.ofProbAutomaton_probCombine_eq_of_simulation {F : List (Σ o, U o) → Prop} + {n : ℕ} {hF : ∀ h, F h → h.length ≤ n} (P : Program S O J U V X Y) {b : ℕ} + (hP : P.Bounded b) {R₁ R₂ : Type} (stepR₁ : ProbStep R₁ J X Y) (stepR₂ : ProbStep R₂ J X Y) + (K : R₁ → Distribution.ProbDist R₂) (invR : List (Σ j, X j) → R₁ → Prop) + (hpres : ∀ τ r q, invR τ r → τ.length < b * n → + ∀ p ∈ (stepR₁.outcome r q).support, invR (τ ++ [q]) p.1) + (hsim : ∀ τ r q, invR τ r → τ.length < b * n → ProbStep.SimulatesAt stepR₁ stepR₂ K r q) + (s : S) (init : Distribution.ProbDist R₁) (hinit : ∀ r ∈ init.1.support, invR [] r) : + RandomSystem.ofProbAutomaton (Domain.ofInputs F n hF) (P.probCombine stepR₁ hP) + (init.map fun r => (s, r)) = + RandomSystem.ofProbAutomaton (Domain.ofInputs F n hF) (P.probCombine stepR₂ hP) + ((init.bind K).map fun r => (s, r)) := by + -- Plan: the two combined automata are compared along the kernel on the inside state, by + -- `RandomSystem.ofProbAutomaton_eq_of_simulation` on the outside domain `F`. + -- 1. Admit the inside queries within the total budget `b * n`, and restate the hypotheses + -- for them. + -- 2. After `xs` outside queries and at most `b · |xs|` inside ones, an invocation at an + -- outside query that `F` admits stays within the budget. + -- 3. The outside invariant: an inside history `τ` of at most `b · |xs|` queries with + -- `invR τ` at the inside state; each outside step keeps it (`probCombine_support`). + -- 4. Each outside step from such a state is a simulation step (`simulatesAt_probCombine`), + -- and the initial states `(s, r)` satisfy the invariant with `τ = []`. + -- 5. Equal random systems along the outside simulation; the kernel image of the initial + -- law is the initial law of the right-hand side. + -- Step 1: the budget. + -- The inside queries admitted: those before the total budget, `τ ++ [q]` of length `≤ b * n`. + let E : List (Σ j, X j) → Prop := fun τ => τ.length ≤ b * n + -- The hypotheses, at the admitted inside queries. + -- (`τ ++ [q]` of length `≤ b * n` is `τ` of length `< b * n`) + have hsim' : ∀ τ r q, invR τ r → E (τ ++ [q]) → ProbStep.SimulatesAt stepR₁ stepR₂ K r q := + fun τ r q hr hq => hsim τ r q hr (by simp [E] at hq; omega) + have hpres' : ∀ τ r q, invR τ r → E (τ ++ [q]) → + ∀ p ∈ (stepR₁.outcome r q).support, invR (τ ++ [q]) p.1 := + fun τ r q hr hq => hpres τ r q hr (by simp [E] at hq; omega) + -- Step 2: invocations within the budget. + -- An invocation after `xs` outside queries, with at most `b` inside queries per earlier one, + -- keeps its inside queries within the budget when the outside domain admits one more. + have good : ∀ xs (sr : S × R₁) x τ, τ.length ≤ b * xs.length → F (xs ++ [x]) → + P.AdmitsInvocation E sr.1 x.1 x.2 τ := fun xs sr x τ hl hx h q hc hq => by + -- this invocation has made fewer than `b` queries, and there are at most `n` outside ones + have h1 := hP sr.1 x.1 x.2 h q hc hq + have h2 := hF _ hx + simp only [List.length_append, List.length_singleton] at h2 + simp only [E, List.length_append, List.length_map, List.length_singleton] + -- `|τ| + |h| + 1 ≤ b·|xs| + b = b·(|xs| + 1) ≤ b·n` + nlinarith + -- Step 3: the outside invariant. + -- The outside invariant: some inside history `τ`, at most `b` queries per outside query, + -- satisfies `invR` at the inside state. + let inv : List (Σ o, U o) → S × R₁ → Prop := + fun xs sr => ∃ τ, invR τ sr.2 ∧ τ.length ≤ b * xs.length + -- Each outside step keeps it: an invocation adds its own exchanges `hf`, at most `b`. + have hpres_out : ∀ xs sr x, inv xs sr → F (xs ++ [x]) → + ∀ p ∈ ((P.probCombine stepR₁ hP).outcome sr x).support, inv (xs ++ [x]) p.1 := by + rintro xs sr x ⟨τ, hτ, hl⟩ hx p hp + obtain ⟨hf, hcf, hinv⟩ := Program.probCombine_support P hP hpres' hτ + (good xs sr x τ hl hx) p hp + -- the new inside history: `τ`, then the inside queries of `hf` + refine ⟨τ ++ hf.map Prod.fst, hinv, ?_⟩ + -- `|hf| ≤ b`, the program being bounded + have := Program.Consistent.length_le hP hcf + simp only [List.length_append, List.length_map, List.length_singleton] + -- `|τ| + |hf| ≤ b·|xs| + b = b·(|xs| + 1)` + nlinarith + -- Step 4: the outside simulation. + -- Each outside step is a simulation step: the program respects the inside simulation. + have hsim_out : ∀ xs sr x, inv xs sr → F (xs ++ [x]) → + ProbStep.SimulatesAt (P.probCombine stepR₁ hP) (P.probCombine stepR₂ hP) + (Program.insideKernel K) sr x := by + rintro xs sr x ⟨τ, hτ, hl⟩ hx + -- the invocation is admitted (Step 2), and `invR τ` holds at the inside state + exact Program.simulatesAt_probCombine P hP hsim' hpres' hτ (good xs sr x τ hl hx) + -- Initially the inside history is empty. + have hinit_out : ∀ sr ∈ (init.map fun r => (s, r)).1.support, inv [] sr := by + intro sr hsr + -- an initial state is `(s, r)` for a possible `r` of `init`; take `τ = []` + obtain ⟨r, hr, rfl⟩ := mem_support_fTransform _ _ hsr + exact ⟨[], hinit r hr, le_refl _⟩ + -- Step 5: conclude. + -- Equal random systems along the outside simulation ... + rw [RandomSystem.ofProbAutomaton_eq_of_simulation (E := F) (bound := n) (hE := hF) + (P.probCombine stepR₁ hP) (P.probCombine stepR₂ hP) (Program.insideKernel K) inv hpres_out + hsim_out _ hinit_out] + -- ... from the kernel image of `(s, r)` for `r ← init`: `(s, r₂)` for `r₂ ← init.bind K`. + -- equal systems from equal initial laws + congr 1 + apply Subtype.ext + simp only [ProbDist.bind_val, ProbDist.map_val, Program.insideKernel, bindK_fTransform, + fTransform_bindK, Function.comp_def] + +end + +/-! ### Pre-sampled draws -/ + +namespace ProbStep + +variable (step : ProbStep R J X Y) + +/-- A record of one step: the state and the query, and the drawn next state and reply. -/ +abbrev Draw (R J : Type) (X Y : J → Type) := (R × Σ j, X j) × (R × Σ j, Y j) + +/-- **The step recording its draws**: it steps as `step` and appends the draw to its record. -/ +noncomputable def recording : ProbStep (R × List (Draw R J X Y)) J X Y := + fun rd j x => (step rd.1 j x).map fun o => + ((o.1, rd.2 ++ [((rd.1, ⟨j, x⟩), tagged ⟨j, x⟩ o)]), o.2) + +/-- The outcome of the recording step: a draw of `step`, appended to the record. -/ +lemma outcome_recording (rd : R × List (Draw R J X Y)) (x : Σ j, X j) : + step.recording.outcome rd x = + fTransform (fun o => ((o.1, rd.2 ++ [((rd.1, x), o)]), o.2)) (step.outcome rd.1 x) := by + -- Both are the step's law, pushed forward along the same map. + simp only [outcome, recording, ProbDist.map_val, fTransform_fTransform] + -- Recording the tagged draw then tagging the reply, or tagging first: the same map. + rfl + +/-- **Forgetting the record** is a simulation. -/ +lemma simulatesAt_forget (rd : R × List (Draw R J X Y)) (x : Σ j, X j) : + SimulatesAt step.recording step (fun rd => Distribution.ProbDist.single rd.1) rd x := by + -- The kernel maps each recorded state `(r, rec)` to the point mass at `r`: + -- + -- (r, rec) ── recording, x ──► ((r', rec · ((r, x), (r', y))), y) + -- │ │ + -- forget forget + -- ▼ ▼ + -- r ─────── step, x ───────► (r', y) + unfold SimulatesAt + -- From the recorded state, `step` steps as the recording step, forgetting the record. + simp only [Distribution.ProbDist.single, bindK_single, one_smul, outcome_recording, + bindK_fTransform, Function.comp_def, fTransform_single] + -- What is left: the step's law against its image under the point kernel, which is itself. + exact (bindK_single_one _).symm + +open scoped Classical in +/-- The reply at the queried port from a tagged draw, or the default `d`. -/ +noncomputable def untag (x : Σ j, X j) (o : R × Σ j, Y j) (d : R × Y x.1) : R × Y x.1 := + if h : o.2.1 = x.1 then (o.1, h ▸ o.2.2) else d + +@[simp] lemma untag_tagged (x : Σ j, X j) (o : R × Y x.1) (d : R × Y x.1) : + untag x (tagged x o) d = o := by + -- The tagged draw is at the queried port: `untag` takes its first case and gives back `o`. + simp [untag, tagged] + +/-- The initial law with an empty record, forgetting the record, is the initial law. -/ +lemma bind_forget (init : Distribution.ProbDist R) : + ((init.map fun r => (r, ([] : List (Draw R J X Y)))).bind + fun rd => Distribution.ProbDist.single rd.1) = init := by + -- Compare the underlying laws. + apply Subtype.ext + -- Pairing with the empty record and keeping the state is the point kernel. + simp only [ProbDist.bind_val, ProbDist.map_val, Distribution.ProbDist.single, + bindK_fTransform, Function.comp_def] + -- ... which leaves `init` unchanged. + exact bindK_single_one _ + +variable [Fintype (Σ j, X j)] (init : Distribution R) + +open scoped Classical in +/-- **The states reachable** from the initial law in at most `k` steps. -/ +noncomputable def reachable : ℕ → Finset R + | 0 => init.support + | k + 1 => reachable k ∪ (reachable k).biUnion fun r => + Finset.univ.biUnion fun x => (step.outcome r x).support.image Prod.fst + +/-- More steps reach more states. -/ +lemma reachable_mono {k k' : ℕ} (h : k ≤ k') : + step.reachable init k ⊆ step.reachable init k' := by + classical + -- Each step adds states to the reachable ones. + induction h with + -- `k' = k`: the same set + | refl => exact subset_refl _ + -- one step more: the states reachable before are the left part of the union + | step _ ih => exact ih.trans Finset.subset_union_left + +open scoped Classical in +/-- A possible next state from a state reachable in `k` steps is reachable in `k + 1`. -/ +lemma mem_reachable_succ {k : ℕ} {r : R} (hr : r ∈ step.reachable init k) {x : Σ j, X j} + {p : R × Σ j, Y j} (hp : p ∈ (step.outcome r x).support) : + p.1 ∈ step.reachable init (k + 1) := + -- `p.1` is a next state of a possible draw from `r` at `x`: one of the new states of step + -- `k + 1`, the right part of the union. + Finset.mem_union_right _ (Finset.mem_biUnion.mpr ⟨r, hr, Finset.mem_biUnion.mpr + ⟨x, Finset.mem_univ _, Finset.mem_image_of_mem _ hp⟩⟩) + +/-- **The record after `k` draws**: `k` draws, from a state reachable in `k` steps; one more draw +keeps this. -/ +lemma recording_reachable {k : ℕ} {rd : R × List (Draw R J X Y)} (hl : rd.2.length = k) + (hr : rd.1 ∈ step.reachable init k) (x : Σ j, X j) + {p : (R × List (Draw R J X Y)) × Σ j, Y j} (hp : p ∈ (step.recording.outcome rd x).support) : + p.1.2.length = k + 1 ∧ p.1.1 ∈ step.reachable init (k + 1) := by + -- The recording step draws `o` from `step` and appends it to the record. + rw [outcome_recording] at hp + obtain ⟨o, ho, rfl⟩ := mem_support_fTransform _ _ hp + -- One more draw in the record, and the next state of a possible draw. + exact ⟨by simp [hl], step.mem_reachable_succ init hr ho⟩ + +variable (L : ℕ) + +/-- A cell of the table of draws: a step number below `L`, a reachable state and a query. -/ +abbrev Cell := Fin L × {r // r ∈ step.reachable init L} × (Σ j, X j) + +open scoped Classical in +/-- **The deterministic step reading pre-sampled draws**: in the state `r` with `k` steps done +and the table `t`, the query `x` is answered by the draw in the cell `(k, r, x)`. + +``` + state (r, k, t) ──x──► (t(k, r, x) = (r', y)) ──► state (r', k + 1, t), reply y +``` +-/ +noncomputable def drawStep : + R × ℕ × (step.Cell init L → R × Σ j, Y j) → (j : J) → X j → + (R × ℕ × (step.Cell init L → R × Σ j, Y j)) × Y j := + fun rkt j x => + -- `d`: some next state and reply (the step's law has a sample), used as a default + let d := Classical.choice (step rkt.1 j x).nonempty + -- inside the table (fewer than `L` steps done, `r` reachable in `L` steps): read the cell + -- `(k, r, x)`, move to its next state and give its reply (`d` if it is at another port) + if h : rkt.2.1 < L ∧ rkt.1 ∈ step.reachable init L then + let o := untag ⟨j, x⟩ (rkt.2.2 (⟨rkt.2.1, h.1⟩, ⟨rkt.1, h.2⟩, ⟨j, x⟩)) d + ((o.1, rkt.2.1 + 1, rkt.2.2), o.2) + -- outside the table: stay in `r` and give the default reply + else ((rkt.1, rkt.2.1 + 1, rkt.2.2), d.2) + +open scoped Classical in +/-- The law of the draw in a cell, given the recorded draws: the recorded one if the cell was +read, a fresh step otherwise. -/ +noncomputable def drawLaw (rec : List (Draw R J X Y)) (c : step.Cell init L) : + Distribution (R × Σ j, Y j) := + -- a step already done: its recorded draw if it read this cell, a fresh step otherwise + if h : c.1.val < rec.length then + if rec[c.1.val].1 = (c.2.1.val, c.2.2) then Finsupp.single rec[c.1.val].2 1 + else step.outcome c.2.1.val c.2.2 + -- a step not yet done: a fresh step + else step.outcome c.2.1.val c.2.2 + +/-- The law of a cell is a probability law: a point mass or a step. -/ +lemma drawLaw_isProbDist (rec : List (Draw R J X Y)) (c : step.Cell init L) : + (step.drawLaw init L rec c).isProbDist := by + unfold drawLaw + split_ifs + -- the recorded draw: a point mass + · exact isProbDist_single _ + -- a fresh step: the tagged step's law, a probability law + · exact fTransform_isProbDist _ (step _ _ _).2 + · exact fTransform_isProbDist _ (step _ _ _).2 + +open scoped Classical in +/-- **The law of the table given the recorded draws**: the recorded cells fixed, the others +independent fresh steps; with the state and the number of steps done. -/ +noncomputable def drawKernel (rd : R × List (Draw R J X Y)) : + Distribution.ProbDist (R × ℕ × (step.Cell init L → R × Σ j, Y j)) := + ProbDist.map (fun t => (rd.1, rd.2.length, t)) + ⟨pi (step.drawLaw init L rd.2), pi_isProbDist fun c => step.drawLaw_isProbDist init L rd.2 c⟩ + +open scoped Classical in +/-- Recording a draw in a cell fixes that cell. -/ +lemma update_drawLaw (rec : List (Draw R J X Y)) (r : R) (x : Σ j, X j) (o : R × Σ j, Y j) + (hk : rec.length < L) (hr : r ∈ step.reachable init L) : + Function.update (step.drawLaw init L rec) (⟨rec.length, hk⟩, ⟨r, hr⟩, x) (Finsupp.single o 1) = + step.drawLaw init L (rec ++ [((r, x), o)]) := by + -- Plan: the law of the table given `rec` has one row per step `k < L`, one cell per + -- reachable state and query in each row: + -- + -- row k cell (k, r', x') law given rec + -- k < |rec| (r', x') the state and query read at k point mass at the recorded draw + -- any other (r', x') fresh step + -- k ≥ |rec| any (r', x') fresh step + -- + -- Appending the draw `((r, x), o)` turns the cell `(|rec|, r, x)` into the point mass at `o` + -- and leaves every other cell as it was. By the row of the cell: + -- 1. the updated cell itself: both sides are the point mass at `o`; + -- 2. a row `k < |rec|`: both records have the entry `rec[k]`; + -- 3. another cell of row `|rec|`: the new entry is at another state or query, fresh step; + -- 4. a row `k > |rec|`: no entry in either record, fresh step. + -- Compare cell by cell. + funext c + by_cases hc : c = (⟨rec.length, hk⟩, ⟨r, hr⟩, x) + -- Step 1: the updated cell. + · -- the new cell: the recorded draw `o` + subst hc + -- left: the update at its own cell; right: entry `|rec|` of the new record is the draw + -- `o`, read at this very state and query + simp [drawLaw] + -- Steps 2–4: on the left, any other cell keeps its law given `rec`. + · rw [Function.update_of_ne hc] + unfold drawLaw + by_cases hlt : c.1.val < rec.length + -- Step 2: a row already done. + · -- an earlier cell: the same record + -- (the entry `k < |rec|` of `rec ++ [_]` is `rec[k]`, so both case splits agree) + rw [dif_pos hlt, dif_pos (by simp; omega), List.getElem_append_left hlt] + · by_cases heq : c.1.val = rec.length + -- Step 3: the row read now, at another state or query. + · -- a cell of the current step at another state or query: still a fresh step + rw [dif_neg hlt, dif_pos (by simp; omega)] + -- entry `|rec|` of the new record is the new draw + have hget : (rec ++ [((r, x), o)])[c.1.val]'(by simp; omega) = ((r, x), o) := by + simp [heq] + rw [hget, if_neg] + -- the new record is at another state or query than `c` + intro h + obtain ⟨h₁, h₂⟩ := Prod.mk.inj h + apply hc + -- with that state and query, `c` (row `|rec|`) is the updated cell, against `hc` + -- (the bounds in the two triples are proofs, equal by proof irrelevance) + obtain ⟨⟨k, hk'⟩, ⟨r', hr'⟩, x'⟩ := c + simp only at heq h₁ h₂ + subst heq h₁ h₂ + rfl + -- Step 4: a row not yet reached. + · -- a later cell: a fresh step + rw [dif_neg hlt, dif_neg (by simp; omega)] + +/-- **Reading the next cell is drawing afresh**: while fewer than `L` steps are done from a +reachable state, the deterministic step on the table of draws simulates the recording step, +along the law of the table given the record. + +``` + (r, rec) ──── recording, x ────► ((r', rec · ((r, x), (r', y))), y) + │ │ + drawKernel drawKernel + ▼ ▼ + (r, k, t) ──── drawStep, x ────► ((r', k + 1, t), y) t(k, r, x) = (r', y) +``` +-/ +lemma simulatesAt_drawStep (rd : R × List (Draw R J X Y)) (hk : rd.2.length < L) + (hr : rd.1 ∈ step.reachable init L) (x : Σ j, X j) : + SimulatesAt step.recording (ofDeterministic (step.drawStep init L)) (step.drawKernel init L) + rd x := by + classical + -- Plan, with `c = (|rec|, r, x)` the cell read now (row `|rec|`, state `r`, query `x`): + -- 1. Under the kernel the table `t` is sampled given `rec`, and `drawStep` reads `t(c)`. + -- 2. Disintegrate the independent table at `c`: first `o = t(c)`, a fresh step from `r`, + -- then the other cells, i.e. the table given `rec · ((r, x), o)` (`update_drawLaw`). + -- 3. That is the recording step's draw `o`, then the kernel at the extended record. + -- + -- (t ← table given rec; read t(c)) + -- = (o ← step from r at x; t ← table given rec · ((r, x), o); read o) Step 2 + -- = (o ← recording from (r, rec) at x; kernel at the extended record) Step 3 + -- + -- Name the recorded state `(r, rec)` and the query `⟨j, x⟩`. + obtain ⟨r, rec⟩ := rd + obtain ⟨j, x⟩ := x + simp only at hk hr + -- The cell read now: step `rec.length`, state `r`, query `x`. + set c : step.Cell init L := (⟨rec.length, hk⟩, ⟨r, hr⟩, ⟨j, x⟩) + -- Its law given the record is a fresh step of `step` from `r`. + have hentry : step.drawLaw init L rec c = step.outcome r ⟨j, x⟩ := by + -- (no draw is recorded for row `|rec|` yet: the last case of `drawLaw`) + simp [drawLaw, c] + -- The deterministic step reads the cell `c` (fewer than `L` steps, reachable state). + have hread : ∀ t : step.Cell init L → R × Σ j, Y j, + step.drawStep init L (r, rec.length, t) j x = + (((untag ⟨j, x⟩ (t c) (Classical.choice (step r j x).nonempty)).1, rec.length + 1, t), + (untag ⟨j, x⟩ (t c) (Classical.choice (step r j x).nonempty)).2) := by + intro t + -- the guard of `drawStep` holds: `|rec| < L` and `r` is reachable in `L` steps + simp only [drawStep, dif_pos (And.intro hk hr), c] + -- The simulation equation: the kernel then `drawStep`, against `recording` then the kernel. + unfold SimulatesAt + calc bindK (step.drawKernel init L (r, rec)).1 + (fun st => (ofDeterministic (step.drawStep init L)).outcome st ⟨j, x⟩) + -- Step 1: read the table. + -- the table `t` is sampled, and the deterministic step reads `t c` + = fTransform (fun t => (((untag ⟨j, x⟩ (t c) (Classical.choice (step r j x).nonempty)).1, + rec.length + 1, t), (⟨j, (untag ⟨j, x⟩ (t c) + (Classical.choice (step r j x).nonempty)).2⟩ : Σ j, Y j))) + (pi (step.drawLaw init L rec)) := by + -- the kernel fixes `(r, |rec|)` and samples `t`; the point step at `(r, |rec|, t)` + -- reads `t c` (`hread`) + simp only [drawKernel, ProbDist.map_val, bindK_fTransform, Function.comp_def, + outcome_ofDeterministic, hread] + -- a point kernel along a map is the pushforward along it + exact bindK_single_comp _ _ + -- Step 2: disintegrate the table at the cell `c`. + -- sample the cell `c` first: a fresh step `o`, then the table with `c` fixed to `o` + _ = bindK (step.outcome r ⟨j, x⟩) fun o => + fTransform (fun t => (((untag ⟨j, x⟩ o (Classical.choice (step r j x).nonempty)).1, + rec.length + 1, t), (⟨j, (untag ⟨j, x⟩ o + (Classical.choice (step r j x).nonempty)).2⟩ : Σ j, Y j))) + (pi (step.drawLaw init L (rec ++ [((r, ⟨j, x⟩), o)]))) := by + -- the independent table, disintegrated at the cell `c`, whose law is a fresh step + rw [pi_eq_bindK_update _ c, fTransform_bindK, hentry] + refine bindK_congr fun o _ => ?_ + -- with `c` fixed to `o`, the table is the table given the record with `o` appended ... + rw [update_drawLaw step init L rec r ⟨j, x⟩ o hk hr] + -- ... and every possible such table has `o` in the cell `c` + refine fTransform_congr_support fun t ht => ?_ + -- `t` is a possible table with `c` fixed to `o`, so `t c = o` + rw [← update_drawLaw step init L rec r ⟨j, x⟩ o hk hr] at ht + rw [eq_of_mem_support_pi_update _ _ o ht] + -- Step 3: the recording step, then the kernel. + -- the fresh step is the recording step's draw, and the table with the record is the + -- kernel image of the recorded state + _ = _ := by + -- unfold the recording step's draw and the kernel at the record of length `|rec| + 1` + simp only [outcome_recording, drawKernel, ProbDist.map_val, bindK_fTransform, + Function.comp_def, fTransform_fTransform, List.length_append, List.length_singleton] + -- draw from the untagged step on both sides + rw [outcome, bindK_fTransform, bindK_fTransform] + refine bindK_congr fun o _ => ?_ + -- untagging a tagged draw gives it back + simp only [Function.comp_def, untag_tagged] + -- what is left: `tagged ⟨j, x⟩ o` is `(o.1, ⟨j, o.2⟩)`, by definition + rfl + +end ProbStep + +/-- The draws of the initial law: no step done, all cells fresh. -/ +noncomputable def ProbStep.drawInit [Fintype (Σ j, X j)] (step : ProbStep R J X Y) + (init : Distribution.ProbDist R) (L : ℕ) : + Distribution.ProbDist (R × ℕ × (step.Cell init.1 L → R × Σ j, Y j)) := + (init.map fun r => (r, [])).bind (step.drawKernel init.1 L) + +section + +variable [Fintype (Σ j, X j)] [Fintype (Σ j, Y j)] + +/-- **A probabilistic automaton is a random automaton** [1, Definition 2]: on any input domain +of at most `L` queries, it is the deterministic automaton reading a table of pre-sampled draws, +the table sampled once with the initial state. + +``` + (step, init) = (recording, (init, [])) = (drawStep, (r, 0, t) for r ← init, t ← draws) +``` +-/ +theorem RandomSystem.ofProbAutomaton_eq_drawStep {E : List (Σ j, X j) → Prop} {m : ℕ} + {hE : ∀ h, E h → h.length ≤ m} (step : ProbStep R J X Y) (init : Distribution.ProbDist R) + {L : ℕ} (hL : m ≤ L) : + RandomSystem.ofProbAutomaton (Domain.ofInputs E m hE) step init = + RandomSystem.ofProbAutomaton (Domain.ofInputs E m hE) + (ProbStep.ofDeterministic (step.drawStep init.1 L)) (step.drawInit init L) := by + -- Plan: the recording step sits between the two automata, linked by two simulations of it: + -- + -- (step, init) + -- = (recording, (init, [])) `step` simulates it, forgetting the record + -- = (drawStep, drawInit) `drawStep` simulates it, reading the table + -- + -- 1. The invariant of the recording step, kept by each step and true initially. + -- 2. Along the domain (at most `m ≤ L` queries), `drawStep` simulates the recording step. + -- 3. The chain above, by `RandomSystem.ofProbAutomaton_eq_of_simulation` twice. + -- + -- Step 1: the invariant. + -- The invariant of the recording step: one draw per query, from a reachable state. + let inv : List (Σ j, X j) → R × List (ProbStep.Draw R J X Y) → Prop := + fun xs rd => rd.2.length = xs.length ∧ rd.1 ∈ step.reachable init.1 xs.length + have hpres : ∀ xs rd x, inv xs rd → E (xs ++ [x]) → + ∀ p ∈ (step.recording.outcome rd x).support, inv (xs ++ [x]) p.1 := by + -- a recording step adds one draw and reaches one step further (`recording_reachable`) + rintro xs rd x ⟨hl, hr⟩ - p hp + obtain ⟨h₁, h₂⟩ := step.recording_reachable init.1 hl hr x hp + exact ⟨by simpa using h₁, by simpa using h₂⟩ + have hinit : ∀ rd ∈ (init.map fun r => (r, ([] : List (ProbStep.Draw R J X Y)))).1.support, + inv [] rd := by + -- initially: the empty record, and a state of `init`'s support, reachable in no step + intro rd hrd + obtain ⟨r, hr, rfl⟩ := mem_support_fTransform _ _ hrd + exact ⟨rfl, hr⟩ + -- Step 2: the simulation by the table of draws. + -- Along the domain, fewer than `L` steps are done, from states reachable in `L` steps: the + -- deterministic step on the table of draws simulates the recording step. + have hsim : ∀ xs rd x, inv xs rd → E (xs ++ [x]) → + ProbStep.SimulatesAt step.recording (ProbStep.ofDeterministic (step.drawStep init.1 L)) + (step.drawKernel init.1 L) rd x := by + rintro xs rd x ⟨hl, hr⟩ hx + -- the domain admits `xs · x`, so `|xs| + 1 ≤ m ≤ L`: fewer than `L` draws recorded ... + have hlen := hE _ hx + simp only [List.length_append, List.length_singleton] at hlen + -- ... and the state, reachable in `|xs|` steps, is reachable in `L` + exact step.simulatesAt_drawStep init.1 L rd (by omega) + (step.reachable_mono init.1 (by omega) hr) x + -- Step 3: the chain. + calc RandomSystem.ofProbAutomaton (Domain.ofInputs E m hE) step init + -- the initial law is the recorded initial law, the record forgotten ... + _ = RandomSystem.ofProbAutomaton (Domain.ofInputs E m hE) step + ((init.map fun r => (r, ([] : List (ProbStep.Draw R J X Y)))).bind + fun rd => Distribution.ProbDist.single rd.1) := by rw [ProbStep.bind_forget] + -- ... and forgetting the record is a simulation of the recording step + _ = RandomSystem.ofProbAutomaton (Domain.ofInputs E m hE) step.recording + (init.map fun r => (r, ([] : List (ProbStep.Draw R J X Y)))) := + (RandomSystem.ofProbAutomaton_eq_of_simulation step.recording step + (fun rd => Distribution.ProbDist.single rd.1) inv hpres + (fun xs rd x _ _ => step.simulatesAt_forget rd x) _ hinit).symm + -- the deterministic step on the table of draws simulates the recording step + -- (`drawInit` is by definition the kernel image of `(init, [])`) + _ = _ := RandomSystem.ofProbAutomaton_eq_of_simulation step.recording _ _ inv hpres hsim _ + hinit + +end + +/-! ### Attaching a program -/ + +namespace PDCBehavior + +variable [Fintype O] [Fintype J] [∀ o, Fintype (U o)] [∀ o, Fintype (V o)] [∀ j, Fintype (X j)] + [∀ j, Fintype (Y j)] {E : List (Σ j, X j) → Prop} {m : ℕ} {hE : ∀ h, E h → h.length ≤ m} + {F : List (Σ o, U o) → Prop} {n : ℕ} {hF : ∀ h, F h → h.length ≤ n} + (hE' : ¬ E [] ∧ ∀ {p h}, p <+: h → p ≠ [] → E h → E p) + (hF' : ¬ F [] ∧ ∀ {p h}, p <+: h → p ≠ [] → F h → F p) + +/-- **Attaching a program to a deterministic automaton** with a random initial state: the +combined automaton, its initial state paired with the program's. -/ +lemma attach_ofDDC_ofProgramOn_ofDeterministic (s : S) (P : Program S O J U V X Y) {b : ℕ} + (hb : P.Bounded b) (hα : IsDDCFrom E F b (DDC.ofProgramOn s P F)) + (stepR : R → (j : J) → X j → R × Y j) (init : Distribution.ProbDist R) : + attach hE' hF' (ofDDC (DDC.ofProgramOn s P F) hα) + (RandomSystem.ofProbAutomaton (Domain.ofInputs E m hE) + (ProbStep.ofDeterministic stepR) init) + (RandomSystem.ofProbAutomaton_repliesAtQueriedInterface _ _ _) = + RandomSystem.ofProbAutomaton (Domain.ofInputs F n hF) + (ProbStep.ofDeterministic (P.combine stepR hb)) (init.map fun r => (s, r)) := by + -- Plan: compare the probabilities of each outside transcript `t`. + -- 1. Present the automaton by the law of its deterministic systems `aut r`, `r ← init`. + -- 2. Present the converter by the point law at its DDC; the attachment of the presentations + -- gives `t` the mass, over `r ← init`, of "the DDC attached to `aut r` replies `t`". + -- 3. The combined automaton gives `t` the mass, over `r ← init`, of "the combined automaton + -- from `(s, r)` replies `t`". + -- 4. For each `r` the two systems are equal (`trim_apply_ofProgramOn_automaton`): + -- + -- ┌──────┐ ──q─▶ ┌──────────┐ + -- ──u──▶ │ P(s) │ │ stepR, r │ = combined automaton `P.combine stepR`, + -- ◀──v── └──────┘ ◀─y── └──────────┘ from `(s, r)` + -- + -- Step 1: the presentation of the automaton. + -- The automaton started in `r`, on the domain `E`, as a deterministic system with domain `E`. + let aut : R → {t : InterfaceSystem J X Y // + IsDDS t ∧ RepliesAtQueriedInterface t ∧ ∀ h, (t h).Dom ↔ E h} := fun r => + ⟨filterDom E (automatonSystem stepR r), + -- a DDS: the automaton system restricted to the prefix-closed domain `E` + (automatonSystem_isDDS stepR r).filterDom _ hE'.2, + -- it replies at the queried port, as the automaton does + fun h x y hy => automatonSystem_replies stepR r h x y ((filterDom_mem_iff _ _ _ _).mp hy).2, + -- its domain is `E`: the automaton answers every nonempty input list, and `E []` fails + fun h => by + rw [filterDom_dom, automatonSystem_dom] + exact ⟨fun hd => hd.1, fun hd => ⟨hd, fun he => hE'.1 (he ▸ hd)⟩⟩⟩ + -- Its random initial state presents the probabilistic automaton of its point steps. + have hQ : ∀ h, behaviorMass (init.map aut).1 (h.map Prod.fst) (h.map Prod.snd) = + RandomSystem.ofProbAutomaton (Domain.ofInputs E m hE) (ProbStep.ofDeterministic stepR) + init h := by + intro h + -- right side: the mass of the initial states whose automaton replies `h` ... + rw [RandomSystem.ofProbAutomaton_ofDeterministic_apply] + -- ... and the left side is the same mass, under the image law of `init` by `aut` + exact mass_fTransform _ _ _ + -- Compare the probabilities of each outside transcript `t`. + apply RandomSystem.ext + intro t + -- Step 2: the attachment of the presentations. + -- Present the converter by its DDC and the automaton by its deterministic systems. + -- (The point law at the DDC presents `ofDDC` by definition: `fun _ => rfl`.) + rw [attach_presents hE' hF' _ _ _ ⟨Finsupp.single ⟨_, hα⟩ 1, isProbDist_single _⟩ + (init.map aut) (fun _ => rfl) hQ] + -- The attachment of presentations: the program attached to the automaton from each initial + -- state `r`, with probability `init r`. + rw [behaviorMass_attachPDS, prod_single_left, mass_fTransform, ProbDist.map_val, + mass_fTransform] + -- Step 3: the combined automaton. + -- The other side: the combined automaton from each initial pair `(s, r)`. + rw [RandomSystem.ofProbAutomaton_ofDeterministic_apply, ProbDist.map_val, mass_fTransform] + -- Step 4: equal systems for each initial state. + -- Attached to each automaton, the program is the combined automaton. + refine mass_congr _ fun r => ?_ + -- the trimmed attachment of the DDC to `aut r` is the combined automaton from `(s, r)`, + -- restricted to the outside domain `F` + exact iff_of_eq (congrArg (fun z => Replies z (t.map Prod.fst) (t.map Prod.snd)) + (Program.trim_apply_ofProgramOn_automaton stepR hb s r hE' hF' hα)) + +/-- **Attaching a program to a probabilistic automaton is the program run against it**: on the +inside domain `E`, the converter of a bounded program on the outside domain `F`, attached to the +probabilistic automaton of `step` started from `init`, is the probabilistic automaton of the +program run against `step`, started from `s` and `init` [1, §3.3]. + +``` + P(s) attached to (step, init) = P run against step, from (s, r) for r ← init +``` + +The proof presents the automaton by pre-sampled draws and uses the deterministic case: + +``` + P • (step, init) + = P • (drawStep, draws) a random automaton ofProbAutomaton_eq_drawStep + = (P.combine drawStep, (s, draws)) deterministic case …_ofDeterministic + = (P run against drawStep, (s, draws)) point steps ofDeterministic_combine + = (P run against recording, (s, (init, []))) P respects the simulation + = (P run against step, (s, init)) P respects forgetting the record +``` +-/ +theorem attach_ofDDC_ofProgramOn_ofProbAutomaton (s : S) (P : Program S O J U V X Y) {b : ℕ} + (hb : P.Bounded b) (hα : IsDDCFrom E F b (DDC.ofProgramOn s P F)) + (step : ProbStep R J X Y) (init : Distribution.ProbDist R) : + attach hE' hF' (ofDDC (DDC.ofProgramOn s P F) hα) + (RandomSystem.ofProbAutomaton (Domain.ofInputs E m hE) step init) + (RandomSystem.ofProbAutomaton_repliesAtQueriedInterface _ _ _) = + RandomSystem.ofProbAutomaton (Domain.ofInputs F n hF) (P.probCombine step hb) + (init.map fun r => (s, r)) := by + -- Plan: the chain of the docstring, with tables of draws for `L = m + b * n` steps. + -- 1. The automaton is the deterministic automaton `drawStep` reading the table. + -- 2. Attached to it, the program is the combined automaton (the deterministic case). + -- 3. Its point steps are the program run against the point steps of `drawStep`. + -- 4. `drawStep` simulates the recording step, and the program respects this simulation ... + -- 5. ... and `step` simulates it too, forgetting the record: back to `step` from `init`. + -- + -- Pre-sampled draws for at most `L = m + b * n` steps: enough for the inside domain and for + -- the inside queries of `n` invocations. + let L := m + b * n + -- Attachment depends on the random system only. + have congr_attach : ∀ (α : PDCBehavior O J U V X Y E m hE F n hF) + (R₁ R₂ : RandomSystem (Σ j, X j) (Σ j, Y j) (Domain.ofInputs E m hE)) + (h₁ : R₁.RepliesAtQueriedInterface) (h₂ : R₂.RepliesAtQueriedInterface), R₁ = R₂ → + attach hE' hF' α R₁ h₁ = attach hE' hF' α R₂ h₂ := by + -- equal systems: the two proofs that it replies at the queried port are equal + rintro α R₁ _ _ _ rfl + rfl + -- Step 1: the automaton is the deterministic automaton reading pre-sampled draws. + -- (`m ≤ L`: the table covers the inside domain.) + rw [congr_attach _ _ _ _ (RandomSystem.ofProbAutomaton_repliesAtQueriedInterface _ _ _) + (RandomSystem.ofProbAutomaton_eq_drawStep step init (L := L) (by omega))] + -- Step 2: attached to a deterministic automaton, the program is the combined automaton ... + rw [attach_ofDDC_ofProgramOn_ofDeterministic hE' hF' s P hb hα] + -- Step 3: ... which is the program run against the point steps of the deterministic automaton. + rw [Program.ofDeterministic_combine] + -- Steps 4 and 5: the program respects the simulations of Step 1, from the recorded initial + -- law. The invariant: one draw per inside query, from a reachable state. + let inv : List (Σ j, X j) → R × List (ProbStep.Draw R J X Y) → Prop := + fun τ rd => rd.2.length = τ.length ∧ rd.1 ∈ step.reachable init.1 τ.length + have hpres : ∀ τ rd q, inv τ rd → τ.length < b * n → + ∀ p ∈ (step.recording.outcome rd q).support, inv (τ ++ [q]) p.1 := by + -- a recording step adds one draw and reaches one step further (`recording_reachable`) + rintro τ rd q ⟨hl, hr⟩ - p hp + obtain ⟨h₁, h₂⟩ := step.recording_reachable init.1 hl hr q hp + exact ⟨by simpa using h₁, by simpa using h₂⟩ + have hinit : ∀ rd ∈ (init.map fun r => (r, ([] : List (ProbStep.Draw R J X Y)))).1.support, + inv [] rd := by + -- initially: the empty record, and a state of `init`'s support, reachable in no step + intro rd hrd + obtain ⟨r, hr, rfl⟩ := mem_support_fTransform _ _ hrd + exact ⟨rfl, hr⟩ + -- Before the program's budget `b * n ≤ L`, the deterministic step on the table of draws + -- simulates the recording step. + have hsim : ∀ τ rd q, inv τ rd → τ.length < b * n → + ProbStep.SimulatesAt step.recording (ProbStep.ofDeterministic (step.drawStep init.1 L)) + (step.drawKernel init.1 L) rd q := by + rintro τ rd q ⟨hl, hr⟩ hτ + -- `|rec| = |τ| < b * n ≤ L` draws, and the state, reachable in `|τ|` steps, is reachable + -- in `L` + exact step.simulatesAt_drawStep init.1 L rd (by omega) + (step.reachable_mono init.1 (by omega) hr) q + -- Step 4: the program run against the recording step is the one against the table of draws. + -- (Its right side starts from `(s, drawInit)`: `drawInit` is the kernel image of `(init, [])`.) + have draw := RandomSystem.ofProbAutomaton_probCombine_eq_of_simulation (hF := hF) P hb + step.recording (ProbStep.ofDeterministic (step.drawStep init.1 L)) (step.drawKernel init.1 L) + inv hpres hsim s _ hinit + -- Step 5: it is also the one against `step`, forgetting the record ... + have forget := RandomSystem.ofProbAutomaton_probCombine_eq_of_simulation (hF := hF) P hb + step.recording step (fun rd => Distribution.ProbDist.single rd.1) inv hpres + (fun τ rd q _ _ => step.simulatesAt_forget rd q) s _ hinit + -- ... from the initial law `init` itself. + rw [ProbStep.bind_forget] at forget + -- The chain: + -- P against drawStep, from (s, drawInit) + -- = P against recording, from (s, (init, [])) (Step 4, `draw`) + -- = P against step, from (s, init) (Step 5, `forget`) + exact draw.symm.trans forget + +end PDCBehavior + +end SystemAlgebra diff --git a/src/RandomSystems/Converter/Program.lean b/src/RandomSystems/Converter/Program.lean index 89ebe28..85a87e6 100644 --- a/src/RandomSystems/Converter/Program.lean +++ b/src/RandomSystems/Converter/Program.lean @@ -84,6 +84,30 @@ theorem Consistent.snoc {P : Program S O J U V X Y} {s : S} {o : O} {u : U o} · rw [List.take_left' rfl, List.getElem_append_right (le_refl _)] simpa using hq +/-- **A bounded program's own exchanges** in one invocation number at most its bound. -/ +theorem Consistent.length_le {P : Program S O J U V X Y} {b : ℕ} (hP : P.Bounded b) {s : S} {o : O} + {u : U o} {h : List ((Σ j, X j) × (Σ j, Y j))} (hc : P.Consistent s o u h) : h.length ≤ b := by + -- Either `h` is empty, or it is earlier exchanges `h'` followed by a last exchange `z`. + rcases List.eq_nil_or_concat h with rfl | ⟨h', z, rfl⟩ + -- No exchange: `0 ≤ b`. + · exact Nat.zero_le _ + -- `h = h' · z`: + · rw [List.concat_eq_append] at hc ⊢ + -- The last exchange answers a query the body made after the exchanges `h'` ... + have hz := hc h'.length (by simp) + rw [List.take_left' rfl, List.getElem_append_right (le_refl _)] at hz + -- ... which are its own exchanges too ... + have hc' : P.Consistent s o u h' := fun i hi => by + have := hc i (by simp; omega) + rwa [List.take_append_of_le_length hi.le, List.getElem_append_left hi] at this + -- ... so `h'` is shorter than the bound, and `h' · z` is within it. + -- The body still queries after its own exchanges `h'` (`hz.1`), so the bound of `P` + -- gives `h'.length < b`. + have := hP s o u h' _ hc' (by simpa using hz.1) + -- Hence `(h' · z).length = h'.length + 1 ≤ b`. + simp only [List.length_append, List.length_singleton] + omega + /-- Each invocation on the outside query `⟨o, u⟩` makes exactly `cost ⟨o, u⟩` inside queries. -/ def Costs (cost : (Σ o, U o) → ℕ) (P : Program S O J U V X Y) : Prop := ∀ s o u, CallCost (cost ⟨o, u⟩) (P s o u) diff --git a/src/RandomSystems/System/Memoryless.lean b/src/RandomSystems/System/Memoryless.lean new file mode 100644 index 0000000..ca3761d --- /dev/null +++ b/src/RandomSystems/System/Memoryless.lean @@ -0,0 +1,459 @@ +import RandomSystems.Converter.ProbProgramAttachment + +/-! +# Memoryless systems + +A system is 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" [1, Definition 3.1, p. 55], and a single-input +system given by a conditional distribution `p_{Y|X}` is a "discrete memoryless channel" +[1, §3.6.1, p. 65]. As a random system, a memoryless system is given by its conditional reply +laws, which are those of the current query alone, as for the beacon, whose conditional law is +`1/|Y|` "for all choices of the arguments" [1, Example 3.8, p. 68]. + +A probabilistic automaton whose reply law does not depend on its state is memoryless, and a +program run against memoryless replies replies memorylessly when one invocation, fed with fresh +samples of the inside laws, has the same reply law `κ` from every program state. So attaching such +a program to a memoryless system gives the memoryless system of `κ`, whatever the number of the +program's inside queries: + +``` + o(u) ┌───┐ j(q) ┌──────────┐ + ──────────────────►│ P ├────────────►│ mem(ν) │ = mem(κ) + ◄──────────────────┤ │◄────────────┤ │ + o ⇒ v └───┘ j ⇒ y └──────────┘ κ = the reply law of P against ν +``` + +## Main definitions + +* `RandomSystem.memoryless D ν`: the memoryless system with the reply law `ν` on the domain `D` +* `RandomSystem.portLaw ν`: the reply law `ν i x` at the queried port `i` +* `RandomSystem.parallelLaw ν₁ ν₂`: the reply laws of two systems side by side +* `RandomSystem.twoLaw ν₁ ν₂`: the same, on the alphabets of their parallel composition +* `ProbStep.Memoryless step ν`: a probabilistic step replying with the law `ν` from every state +* `ProbStep.fresh ν`: fresh samples of `ν`, a step with no state +* `Program.replyLaw P ν`: the reply law of an invocation against inside replies of the laws `ν` + +## Main results + +* `RandomSystem.memoryless_snoc`, `RandomSystem.eq_memoryless_of_snoc`: the chain rule, and a + random system obeying it is the memoryless system +* `RandomSystem.parallel_memoryless`: memoryless systems side by side are memoryless +* `RandomSystem.ofProbAutomaton_eq_memoryless`: an automaton with a memoryless step is the + memoryless system of its reply law +* `Program.memoryless_probCombine`: a program run against a memoryless step, with the same reply + law from every program state, is memoryless +* `PDCBehavior.attach_ofDDC_ofProgramOn_memoryless`: the composition law: attaching a program to + the memoryless system of `ν` gives the memoryless system of its reply law against `ν` + +## References + +1. U. Maurer. *Cryptography Foundations*. Lecture notes, ETH Zurich, Spring 2018. +-/ + +namespace SystemAlgebra + +open Probability Probability.Distribution + +/-! ### Memoryless systems -/ + +namespace RandomSystem + +variable {A B : Type} [Fintype A] [Fintype B] + +/-- **The memoryless system** with the reply law `ν` [1, Definition 3.1, §3.6.1]: on the domain +`D`, the reply to the query `x` is a fresh sample of `ν x`, independent of the history. -/ +noncomputable def memoryless (D : Domain A B) (ν : A → ProbDist B) : RandomSystem A B D := + -- A random system is given by its conditional reply laws (`ofConditional`). Here the law at + -- the history `h` and the query `x` ignores `h`: it is `ν x`. + ofConditional fun _ x _ => ν x + +open scoped Classical in +/-- **The chain rule**: one more exchange multiplies the probability of a transcript by the +reply law, when the domain admits the query. -/ +lemma memoryless_snoc (D : Domain A B) (ν : A → ProbDist B) (h : List (A × B)) (x : A) + (y : B) : + memoryless D ν (h ++ [(x, y)]) = if D h x then memoryless D ν h * (ν x).1 y else 0 := by + -- `ofConditional_snoc` is the chain rule of any system given by conditional laws ... + have chain := ofConditional_snoc (D := D) (fun _ x _ => ν x) h x y + -- ... stated with a dependent `if`; ours does not use the proof that `D h x`. + rw [dite_eq_ite] at chain + exact chain + +/-- **A random system obeying the chain rule of `ν` is the memoryless system** of `ν`: when each +admitted exchange multiplies the probability by the reply law `ν`. -/ +lemma eq_memoryless_of_snoc {D : Domain A B} {ν : A → ProbDist B} {R : RandomSystem A B D} + (hR : ∀ h x y, D h x → R (h ++ [(x, y)]) = R h * (ν x).1 y) : R = memoryless D ν := by + -- Compare the probabilities of every transcript, by induction, one exchange at a time. + ext t + induction t using List.reverseRecOn with + | nil => + -- the empty transcript has probability one on both sides + rw [mass_nil, mass_nil] + | append_singleton t e ih => + obtain ⟨x, y⟩ := e + -- the chain rule of the memoryless system + rw [memoryless_snoc] + split_ifs with hd + · -- an admitted query: both multiply the probability of `t` by `ν x y` + rw [hR t x y hd, ih] + · -- a query outside the domain has no reply + exact R.mass_eq_zero_of_not_admitted hd y + +variable {I : Type} {X Y : I → Type} + +/-- **The reply law at the queried port**: for a query `x` at the port `i`, the law `ν i x` of +the reply, as a law on replies tagged with their port. -/ +noncomputable def portLaw (ν : ∀ i, X i → ProbDist (Y i)) (x : Σ i, X i) : + ProbDist (Σ i, Y i) := + ProbDist.map (Sigma.mk x.1) (ν x.1 x.2) + +/-- The reply law at the queried port, at a reply at that port. -/ +lemma portLaw_apply_mk (ν : ∀ i, X i → ProbDist (Y i)) (i : I) (x : X i) (y : Y i) : + (portLaw ν ⟨i, x⟩).1 ⟨i, y⟩ = (ν i x).1 y := + -- Tagging by the port is injective. + fTransform_injective_apply _ _ sigma_mk_injective y + +/-- The reply law at the queried port gives no mass to replies at another port. -/ +lemma portLaw_apply_of_ne (ν : ∀ i, X i → ProbDist (Y i)) {x : Σ i, X i} {y : Σ i, Y i} + (h : y.1 ≠ x.1) : (portLaw ν x).1 y = 0 := + -- Every tagged reply is at the port `x.1`. + fTransform_apply_of_forall_ne _ _ _ fun _ ha => h (ha ▸ rfl) + +variable {J : Type} {X₁ Y₁ : I → Type} {X₂ Y₂ : J → Type} + +/-- **The reply laws of two systems side by side**: a query at a left port has the left law, one +at a right port the right law. -/ +def parallelLaw (ν₁ : ∀ i, X₁ i → ProbDist (Y₁ i)) (ν₂ : ∀ j, X₂ j → ProbDist (Y₂ j)) : + ∀ l : I ⊕ J, Sum.rec (motive := fun _ => Type) X₁ X₂ l → + ProbDist (Sum.rec (motive := fun _ => Type) Y₁ Y₂ l) + | .inl i, x => ν₁ i x + | .inr j, x => ν₂ j x + +section Parallel + +variable {A B C E : Type} [Fintype A] [Fintype B] [Fintype C] [Fintype E] + +/-- **The reply laws of two systems side by side**, on the alphabets of their parallel +composition: a query to the left system has the law `ν₁`, one to the right system the law `ν₂`. -/ +def twoLaw (ν₁ : A → ProbDist B) (ν₂ : C → ProbDist E) : + ∀ o, optF A (fun _ : Unit => C) o → ProbDist (optF B (fun _ : Unit => E) o) + | none, x => ν₁ x + | some (), x => ν₂ x + +/-- **Memoryless systems side by side are memoryless**: in the parallel composition of the +memoryless systems of `ν₁` and `ν₂`, a query to the left system is answered by a fresh sample of +`ν₁`, and a query to the right system by a fresh sample of `ν₂`. -/ +lemma parallel_memoryless (D : Domain A B) (D' : Domain C E) (ν₁ : A → ProbDist B) + (ν₂ : C → ProbDist E) : + parallel (memoryless D ν₁) (memoryless D' ν₂) = + memoryless (D.parallel D') (portLaw (twoLaw ν₁ ν₂)) := by + -- Plan: + -- 1. Reduce to the chain rule of the side-by-side laws: each admitted exchange `(x, y)` + -- multiplies the probability of the transcript `h` by the law of `y` at the queried port. + -- 2. Write the parallel composition at `h` and at `h · (x, y)` as the product of the + -- probabilities of the left and the right transcripts. + -- 3. Case on the ports of the query and of the reply: the chain rule of the queried system + -- (same port), or no mass on both sides (different ports). + -- + -- ┌─────────┐ + -- ──x₁──▶ │ mem(ν₁) │ left port: y₁ ← ν₁ x₁, a fresh sample + -- ◀──y₁── │ │ + -- └─────────┘ + -- ┌─────────┐ + -- ──x₂──▶ │ mem(ν₂) │ right port: y₂ ← ν₂ x₂, a fresh sample + -- ◀──y₂── │ │ + -- └─────────┘ + -- + -- Step 1: reduce to the chain rule. + -- The chain rule of the side-by-side laws, at each admitted exchange `(x, y)`. + refine eq_memoryless_of_snoc fun h x y hd => ?_ + -- Step 2: split the transcript into its left and right transcripts. + -- The parallel domain admits a query only after a transcript whose every exchange is with one + -- of the two systems; such a transcript is a left and a right transcript side by side. + have hcons : parallelConsistent h := hd.1 + -- For such an `h`: `P(h) = mem(ν₁)(left h) · mem(ν₂)(right h)`, on both sides. + rw [parallel_mass, parallel_mass, if_pos hcons] + -- Step 3: case on the ports of the query and of the reply. + -- Case on the systems that receive the query and that give the reply. + obtain ⟨(_ | ⟨⟩), x⟩ := x <;> obtain ⟨(_ | ⟨⟩), y⟩ := y + · -- A query and a reply of the left system: the left transcript grows by `(x, y)`, the right + -- one stays, and the left system multiplies its probability by `ν₁ x y`. + -- + -- P(h · (x, y)) = mem(ν₁)(left h · (x, y)) · mem(ν₂)(right h) + -- = mem(ν₁)(left h) · ν₁ x y · mem(ν₂)(right h) (left chain rule) + -- = P(h) · ν₁ x y + have hleft : parallelLeft (h ++ [(⟨none, x⟩, ⟨none, y⟩)]) = parallelLeft h ++ [(x, y)] := by + simp [parallelLeft] + have hright : parallelRight (h ++ [(⟨none, x⟩, ⟨none, y⟩)]) = parallelRight h := by + simp [parallelRight] + -- `h · (x, y)` is still consistent; the left chain rule applies, since the left domain + -- admits `x` after the left transcript (part of `hd`); the port law at the left port is `ν₁`. + rw [if_pos (parallelConsistent_snoc.mpr ⟨hcons, rfl⟩), hleft, hright, memoryless_snoc, + if_pos hd.2.2, portLaw_apply_mk] + simp only [twoLaw] + -- reorder the product + ring + · -- A left query with a right reply: an exchange with no single system, impossible on both + -- sides. + -- Left: `h · (x, y)` is not consistent. Right: the port law gives no mass to a reply at + -- another port than the queried one. + rw [if_neg fun h' => absurd (parallelConsistent_snoc.mp h').2 (by simp), + portLaw_apply_of_ne _ (by simp), mul_zero] + · -- A right query with a left reply: impossible on both sides. + -- (The same two facts as in the previous case.) + rw [if_neg fun h' => absurd (parallelConsistent_snoc.mp h').2 (by simp), + portLaw_apply_of_ne _ (by simp), mul_zero] + · -- A query and a reply of the right system: the right transcript grows by `(x, y)`, and the + -- right system multiplies its probability by `ν₂ x y`. + -- + -- P(h · (x, y)) = mem(ν₁)(left h) · mem(ν₂)(right h · (x, y)) + -- = mem(ν₁)(left h) · mem(ν₂)(right h) · ν₂ x y (right chain rule) + -- = P(h) · ν₂ x y + have hleft : parallelLeft (h ++ [(⟨some (), x⟩, ⟨some (), y⟩)]) = parallelLeft h := by + simp [parallelLeft] + have hright : + parallelRight (h ++ [(⟨some (), x⟩, ⟨some (), y⟩)]) = parallelRight h ++ [(x, y)] := by + simp [parallelRight] + -- `h · (x, y)` is still consistent; the right chain rule applies, since the right domain + -- admits `x` after the right transcript (part of `hd`); the port law there is `ν₂`. + rw [if_pos (parallelConsistent_snoc.mpr ⟨hcons, rfl⟩), hleft, hright, memoryless_snoc, + if_pos hd.2.2, portLaw_apply_mk] + simp only [twoLaw] + -- reorder the product + ring + +end Parallel + +end RandomSystem + +/-! ### Memoryless steps -/ + +namespace ProbStep + +variable {S I : Type} {X Y : I → Type} + +/-- **A memoryless step** with the reply law `ν`: from every state, the reply to `x` at `i` has +the law `ν i x`. -/ +def Memoryless (step : ProbStep S I X Y) (ν : ∀ i, X i → ProbDist (Y i)) : Prop := + -- `step s i x` is a law on pairs (next state, reply); forgetting the next state leaves `ν i x` + ∀ s i x, fTransform Prod.snd (step s i x).1 = (ν i x).1 + +/-- From any state, a memoryless step replies `y` with the probability its reply law gives `y`. -/ +lemma Memoryless.mass_outcome {step : ProbStep S I X Y} {ν : ∀ i, X i → ProbDist (Y i)} + (hν : step.Memoryless ν) (s : S) (x : Σ i, X i) (y : Σ i, Y i) : + (step.outcome s x).mass (·.2 = y) = (RandomSystem.portLaw ν x).1 y := by + -- The probability that the reply is `y` is the pushforward to the reply, evaluated at `y`. + rw [← fTransform_apply_eq_mass] + -- `outcome` is the step at the port `x.1`, the reply tagged by the port. + rw [outcome, fTransform_fTransform] + -- Tagging and then keeping the reply is keeping the reply and then tagging it. + rw [show (Prod.snd ∘ tagged x) = Sigma.mk x.1 ∘ Prod.snd from rfl, ← fTransform_fTransform] + -- The step is memoryless: its reply law is `ν x.1 x.2`, whatever the state `s`. + rw [hν s x.1 x.2] + -- What remains is the definition of `portLaw`. + rfl + +/-- **Fresh samples** of `ν`: a step with no state, answering the query `x` at `i` with a new +sample of `ν i x`. -/ +noncomputable def fresh (ν : ∀ i, X i → ProbDist (Y i)) : ProbStep Unit I X Y := + fun _ i x => (ν i x).map fun y => ((), y) + +/-- **Fresh samples are memoryless.** -/ +lemma memoryless_fresh (ν : ∀ i, X i → ProbDist (Y i)) : (fresh ν).Memoryless ν := by + intro _ i x + -- The step pairs a sample of `ν i x` with the trivial state; keeping the reply undoes this. + simp only [fresh, ProbDist.map_val, fTransform_fTransform] + -- `Prod.snd ∘ (y ↦ ((), y))` is the identity, and pushing forward along it changes nothing. + exact fTransform_id _ + +end ProbStep + +/-- **A probabilistic automaton with a memoryless step is the memoryless system** of its reply +law. -/ +lemma RandomSystem.ofProbAutomaton_eq_memoryless {S I : Type} {X Y : I → Type} + [Fintype (Σ i, X i)] [Fintype (Σ i, Y i)] (D : Domain (Σ i, X i) (Σ i, Y i)) + {step : ProbStep S I X Y} {ν : ∀ i, X i → ProbDist (Y i)} (hν : step.Memoryless ν) + (init : ProbDist S) : + RandomSystem.ofProbAutomaton D step init = RandomSystem.memoryless D (portLaw ν) := by + -- It suffices to check the chain rule of `portLaw ν` at every admitted exchange `(x, y)`: + -- + -- P(t · (x, y)) = ∑ₛ belief_t(s) · Pr[step s x replies y] (state laws) + -- = (∑ₛ belief_t(s)) · ν x y (memoryless step) + -- = P(t) · ν x y + -- + -- where `belief_t` is the state law after the transcript `t`, of weight `P(t)`. + refine eq_memoryless_of_snoc fun t x y hd => ?_ + -- the probability of `t · (x, y)` is the weight of the state law after it + rw [ofProbAutomaton_apply, ProbStep.belief_snoc, if_pos hd] + -- the weight of the transition: the old state law, weighted by the reply probabilities + rw [ProbStep.weight_transition] + -- every state replies `y` with the same probability (the step is memoryless) ... + simp only [hν.mass_outcome] + -- ... which factors out of the sum, leaving the weight of the old state law + rw [ofProbAutomaton_apply, weight, Finsupp.sum_mul] + +/-! ### Programs against memoryless steps -/ + +namespace Program + +variable {S O J R : Type} {U V : O → Type} {X Y : J → Type} (P : Program S O J U V X Y) + +/-- **The reply law of an invocation** against inside replies of the laws `ν`: the body runs +from the exchanges `h`, with at most `n` more inside queries, and each inside query `q` is +answered by a fresh sample of `ν q`. -/ +noncomputable def replyLaw (ν : ∀ j, X j → ProbDist (Y j)) (s : S) (o : O) (u : U o) : + ℕ → List ((Σ j, X j) × (Σ j, Y j)) → Distribution (V o) + -- No inside query is left: the body must reply now (otherwise no mass). + | 0, h => match P s o u h with + | .inl a => Finsupp.single a.2 1 + | .inr _ => 0 + -- The body replies (a point law on its reply), or asks `q` and continues with `y ← ν q`. + | n + 1, h => match P s o u h with + | .inl a => Finsupp.single a.2 1 + | .inr q => bindK (ν q.1 q.2).1 fun y => replyLaw ν s o u n (h ++ [(q, ⟨q.1, y⟩)]) + +variable {P} + +/-- When the body replies, the reply law is the point law on its reply. -/ +lemma replyLaw_inl {ν : ∀ j, X j → ProbDist (Y j)} {s : S} {o : O} {u : U o} + {h : List ((Σ j, X j) × (Σ j, Y j))} {a : S × V o} (ha : P s o u h = .inl a) (n : ℕ) : + P.replyLaw ν s o u n h = Finsupp.single a.2 1 := by + -- Whatever the number of queries left, the first case of the definition. + cases n <;> simp [replyLaw, ha] + +/-- When the body asks `q`, the reply law samples the answer `y ← ν q` and continues. -/ +lemma replyLaw_succ_inr {ν : ∀ j, X j → ProbDist (Y j)} {s : S} {o : O} {u : U o} + {h : List ((Σ j, X j) × (Σ j, Y j))} {q : Σ j, X j} (hq : P s o u h = .inr q) (n : ℕ) : + P.replyLaw ν s o u (n + 1) h = + bindK (ν q.1 q.2).1 fun y => P.replyLaw ν s o u n (h ++ [(q, ⟨q.1, y⟩)]) := by + -- The second case of the definition with a query left. + simp [replyLaw, hq] + +/-- **An invocation against a memoryless step** replies with the reply law of the program, +whatever the state of the step. -/ +lemma fTransform_snd_probInvoke {stepR : ProbStep R J X Y} {ν : ∀ j, X j → ProbDist (Y j)} + (hν : stepR.Memoryless ν) (s : S) (o : O) (u : U o) : + ∀ n r h, fTransform Prod.snd (P.probInvoke stepR s o u n r h) = P.replyLaw ν s o u n h := by + -- Plan: induction on the number `n` of inside queries still allowed, for every state `r` of + -- the step and every list `h` of inside exchanges so far. + -- 1. `n = 0`: the body replies (a point law on both sides) or asks (no mass on both sides). + -- 2. `n + 1`: the body replies (a point law on both sides) or asks `q`; then the chain below, + -- where `snd₊` keeps only the reply of the invocation: + -- + -- snd₊ invoke_{n+1}(r, h) + -- = ∑_{(r', y) ← step r q} snd₊ invoke_n(r', h · (q, y)) (one inside query) + -- = ∑_{(r', y) ← step r q} replyLaw_n(h · (q, y)) (induction hypothesis) + -- = ∑_{y ← ν q} replyLaw_n(h · (q, y)) (memoryless: `r'` drops out) + -- = replyLaw_{n+1}(h) + -- + -- ┌───┐ ──q──▶ ┌────────────────┐ + -- o(u) ─▶│ P │ │ step, state r │ the step's reply y has the law ν q, + -- ◀── v ─│ │ ◀──y── │ │ whatever its state r + -- └───┘ └────────────────┘ + -- + -- `probInvoke` runs the body against the step, tracking (next states, reply). Looking only at + -- the reply, the state of the step drops out: each inside answer has the law `ν q`. + -- Induction on the number `n` of inside queries still allowed. + intro n + induction n with + -- Step 1: no inside query left. + | zero => + intro r h + cases hq : P s o u h with + | inl a => + -- the body replies `a.2`: a point law on both sides + simp [probInvoke_inl hq, replyLaw_inl hq, fTransform] + | inr q => + -- the body asks, but no query is left: no mass on both sides + simp [probInvoke_zero_inr hq, replyLaw, hq, fTransform] + -- Step 2: one more inside query allowed. + | succ n ih => + intro r h + cases hq : P s o u h with + | inl a => + -- the body replies `a.2`: a point law on both sides + simp [probInvoke_inl hq, replyLaw_inl hq, fTransform] + | inr q => + -- the body asks `q`: the invocation draws the step's (next state, answer) and continues + rw [probInvoke_succ_inr hq, replyLaw_succ_inr hq] + -- move the projection to the reply inside the draw + rw [fTransform_bindK] + -- the step's answer law, with the state forgotten, is `ν q` (memoryless) + rw [← hν r q.1 q.2, bindK_fTransform] + -- the continuation's reply law does not depend on the next state (induction hypothesis) + simp only [ih, ProbStep.outcome, bindK_fTransform] + -- both kernels read only the answer `y` of the draw `(r', y)`, tagged by the port of `q` + rfl + +/-- **A program run against a memoryless step is memoryless**, when its reply law against `ν` is +the same `κ` in every state of the program. -/ +lemma memoryless_probCombine {stepR : ProbStep R J X Y} {ν : ∀ j, X j → ProbDist (Y j)} + (hν : stepR.Memoryless ν) {b : ℕ} (hb : P.Bounded b) {κ : ∀ o, U o → ProbDist (V o)} + (hκ : ∀ s o u, P.replyLaw ν s o u b [] = (κ o u).1) : + (P.probCombine stepR hb).Memoryless κ := by + -- The combined step runs one invocation from the pair of states `(s, r)`. + intro sr o u + -- Its reply law is the program's reply law against `ν` from `s` (previous theorem) ... + have reply := fTransform_snd_probInvoke (P := P) hν sr.1 o u b sr.2 [] + -- ... which is `κ o u` by hypothesis. + exact reply.trans (hκ sr.1 o u) + +end Program + +/-! ### The composition law -/ + +namespace PDCBehavior + +variable {S O J : Type} {U V : O → Type} {X Y : J → Type} [Fintype O] [Fintype J] + [∀ o, Fintype (U o)] [∀ o, Fintype (V o)] [∀ j, Fintype (X j)] [∀ j, Fintype (Y j)] + {E : List (Σ j, X j) → Prop} {m : ℕ} {hE : ∀ h, E h → h.length ≤ m} + {F : List (Σ o, U o) → Prop} {n : ℕ} {hF : ∀ h, F h → h.length ≤ n} + +/-- **The composition law for memoryless systems**: attaching the converter of a bounded program, +whose reply law against `ν` is `κ` in every state, to the memoryless system of `ν` gives the +memoryless system of `κ`. + +``` + P • mem(ν) = mem(κ) κ o u = the law of P's reply to o(u) when every inside query + j(q) is answered by a fresh sample of ν j q +``` +-/ +theorem attach_ofDDC_ofProgramOn_memoryless + (hE' : ¬ E [] ∧ ∀ {p h}, p <+: h → p ≠ [] → E h → E p) + (hF' : ¬ F [] ∧ ∀ {p h}, p <+: h → p ≠ [] → F h → F p) (s : S) (P : Program S O J U V X Y) + {b : ℕ} (hb : P.Bounded b) (hα : IsDDCFrom E F b (DDC.ofProgramOn s P F)) + {ν : ∀ j, X j → ProbDist (Y j)} {κ : ∀ o, U o → ProbDist (V o)} + (hκ : ∀ s' o u, P.replyLaw ν s' o u b [] = (κ o u).1) + {R : RandomSystem (Σ j, X j) (Σ j, Y j) (Domain.ofInputs E m hE)} + (hR : R = RandomSystem.memoryless _ (RandomSystem.portLaw ν)) + (hRq : R.RepliesAtQueriedInterface) : + attach hE' hF' (ofDDC (DDC.ofProgramOn s P F) hα) R hRq = + RandomSystem.memoryless (Domain.ofInputs F n hF) (RandomSystem.portLaw κ) := by + -- The program `P`, started in the state `s`, attached to the memoryless system of `ν`: + -- + -- ┌───┐ ──j(q)──▶ ┌────────┐ + -- ─o(u)─▶ │ P │ │ mem(ν) │ = mem(κ) + -- ◀──v─── │ │ ◀───y──── │ │ + -- └───┘ └────────┘ + -- + -- P • mem(ν) = P • aut(fresh ν) (Step 1: fresh samples present mem(ν)) + -- = aut(P run against fresh ν) (Step 2: attachment to an automaton) + -- = mem(κ) (Step 3: a memoryless step of law κ) + -- + -- Step 1: the memoryless system of `ν` is the automaton of fresh samples of `ν`. + have hfresh : R = RandomSystem.ofProbAutomaton _ (ProbStep.fresh ν) + (Distribution.ProbDist.single ()) := + hR.trans (RandomSystem.ofProbAutomaton_eq_memoryless _ (ProbStep.memoryless_fresh ν) _).symm + -- Replace `R` by that automaton (with no state, started at `()`). + subst hfresh + -- Step 2: attached to an automaton, the program is the program run against its step ... + rw [attach_ofDDC_ofProgramOn_ofProbAutomaton hE' hF' s P hb hα] + -- Step 3: ... a memoryless step of law `κ`, so the memoryless system of `κ`. + -- (The combined step is memoryless of law `κ` because fresh samples are memoryless of law + -- `ν` and `P`'s reply law against `ν` is `κ` in every state, `hκ`.) + exact RandomSystem.ofProbAutomaton_eq_memoryless _ + (Program.memoryless_probCombine (ProbStep.memoryless_fresh ν) hb hκ) _ + +end PDCBehavior + +end SystemAlgebra diff --git a/src/RandomSystems/System/ProbAutomaton.lean b/src/RandomSystems/System/ProbAutomaton.lean new file mode 100644 index 0000000..636b20d --- /dev/null +++ b/src/RandomSystems/System/ProbAutomaton.lean @@ -0,0 +1,547 @@ +import RandomSystems.System.Automaton +import RandomSystems.Cumulative.Cumulative +import RandomSystems.PDS.Filter +import Probability.Kernel + +/-! +# Probabilistic automata + +A probabilistic automaton answers a query at a port from its state with a law on the next state +and the reply at that port (a probabilistic step). Its random system is given by its state laws +along a transcript: after a transcript `h`, the sub-law `belief h` of the states reached with the +replies of `h`, whose weight is the probability of `h`. One more exchange `port(x)`, `port ⇒ y` +moves this sub-law by one step and keeps the states that replied `y`: + +``` + belief (h · (x, y)) (s') = ∑ₛ belief h (s) · Pr[step s x = (s', y)] (if the domain admits x) + P(h) = ∑ₛ belief h (s) +``` + +On an input domain, two probabilistic automata have the same random system along a +**simulation**: a kernel from the states of the first to those of the second such that, from the +kernel image of a state, a step of the second is a step of the first followed by the kernel. A +deterministic automaton is the probabilistic automaton of its point steps: with its initial state +sampled, a transcript has the probability of the initial states from which the automaton gives +it, as for a random automaton whose only randomness is its initial state [1, Definition 2]. + +## Main definitions + +* `ProbStep S I X Y`: a probabilistic step +* `ProbStep.outcome`, `ProbStep.transition`: the law of the next state and the reply, and the + states reached with a given reply +* `ProbStep.belief D step init h`: the sub-law of the states after the transcript `h` +* `RandomSystem.ofProbAutomaton D step init`: the random system of a probabilistic automaton +* `ProbStep.SimulatesAt step₁ step₂ K s x`: a simulation step along the kernel `K` +* `ProbStep.ofDeterministic step`: the probabilistic step of a deterministic automaton + +## Main results + +* `RandomSystem.ofProbAutomaton_repliesAtQueriedInterface`: a probabilistic automaton replies at + the queried port +* `ProbStep.belief_simulation`, `RandomSystem.ofProbAutomaton_eq_of_simulation`: along a + simulation the state laws correspond, and on an input domain the random systems are equal +* `RandomSystem.ofProbAutomaton_ofDeterministic_apply`: a deterministic automaton with a random + initial state is the probabilistic automaton of its point steps + +## References + +1. U. Maurer. Indistinguishability of Random Systems. In *Advances in Cryptology – EUROCRYPT + 2002*, LNCS 2332, Springer, 2002. +-/ + +namespace SystemAlgebra + +open Probability Probability.Distribution + +/-- **A probabilistic step**: from a state and a query at the port `i`, a law on the next state +and the reply at `i`. -/ +abbrev ProbStep (S I : Type) (X Y : I → Type) := + S → (i : I) → X i → Distribution.ProbDist (S × Y i) + +namespace ProbStep + +variable {S I : Type} {X Y : I → Type} (step : ProbStep S I X Y) + +/-- The next state with the reply tagged by the queried port. -/ +def tagged (x : Σ i, X i) (sy : S × Y x.1) : S × Σ i, Y i := (sy.1, ⟨x.1, sy.2⟩) + +/-- **The outcome** of the query `x` in the state `s`: the law of the next state and the reply, +tagged by the queried port. -/ +noncomputable def outcome (s : S) (x : Σ i, X i) : Distribution (S × Σ i, Y i) := + fTransform (tagged x) (step s x.1 x.2).1 + +/-- An outcome is a nonnegative law: the tagged step. -/ +lemma outcome_nonNeg (s : S) (x : Σ i, X i) : (step.outcome s x).NonNeg := + (step s x.1 x.2).2.1.fTransform _ + +/-- An outcome has weight one: the step is a probability law. -/ +lemma weight_outcome (s : S) (x : Σ i, X i) : (step.outcome s x).weight = 1 := by + -- Tagging the reply moves mass without changing it, and the step is a probability law. + rw [outcome, weight_fTransform] + -- the weight-one field of the probability law `step s x.1 x.2` + exact (step s x.1 x.2).2.2 + +/-- The replies of an outcome are at the queried port. -/ +lemma mem_support_outcome {s : S} {x : Σ i, X i} {p : S × Σ i, Y i} + (hp : p ∈ (step.outcome s x).support) : ∃ y : Y x.1, p.2 = ⟨x.1, y⟩ := by + -- A possible outcome is the tag of a possible step `(s', y)`, whose reply is at `x.1`. + obtain ⟨a, -, rfl⟩ := mem_support_fTransform _ _ hp + exact ⟨a.2, rfl⟩ + +/-- **The transition** of a state law on a query and its reply: the states reached with that +reply. -/ +noncomputable def transition (β : Distribution S) (x : Σ i, X i) (y : Σ i, Y i) : + Distribution S := + bindK β fun s => fTransform Prod.fst ((step.outcome s x).restrict fun sy => sy.2 = y) + +/-- The law of the reply to the query `x` from the state law `β`. -/ +noncomputable def replyLaw (β : Distribution S) (x : Σ i, X i) : Distribution (Σ i, Y i) := + bindK β fun s => fTransform Prod.snd (step.outcome s x) + +/-- The weight of a transition: the probability, under the state law, of replying `y`. -/ +lemma weight_transition (β : Distribution S) (x : Σ i, X i) (y : Σ i, Y i) : + (step.transition β x y).weight = β.sum fun s w => w * (step.outcome s x).mass (·.2 = y) := by + -- The weight of a mixture weighs each law of the kernel; forgetting the reply keeps the + -- weight, and the weight of a restriction is the mass of its event. + rw [transition, weight_bindK] + simp only [weight_fTransform, weight_restrict] + +/-- The reply law at `y` is the weight of the transition with the reply `y`. -/ +lemma replyLaw_apply (β : Distribution S) (x : Σ i, X i) (y : Σ i, Y i) : + step.replyLaw β x y = (step.transition β x y).weight := by + -- Both sides are `∑ₛ β s · Pr[step s x replies y]`. + rw [weight_transition, replyLaw, bindK_apply] + -- The reply marginal of the outcome at `y` is the mass of the outcomes with reply `y`. + simp only [fTransform_apply_eq_mass] + +/-- The reply law has the weight of the state law. -/ +lemma weight_replyLaw (β : Distribution S) (x : Σ i, X i) : + (step.replyLaw β x).weight = β.weight := by + -- Each outcome is a probability law, so its reply law has weight one. + rw [replyLaw, weight_bindK_of_weight fun s _ => by rw [weight_fTransform, weight_outcome]] + +/-- A transition of a nonnegative state law is nonnegative. -/ +lemma transition_nonNeg {β : Distribution S} (hβ : β.NonNeg) (x : Σ i, X i) (y : Σ i, Y i) : + (step.transition β x y).NonNeg := + bindK_nonNeg hβ fun s => ((step.outcome_nonNeg s x).restrict _).fTransform _ + +/-- A reply at another port than the queried one is impossible. -/ +lemma transition_eq_zero {β : Distribution S} {x : Σ i, X i} {y : Σ i, Y i} (hy : y.1 ≠ x.1) : + step.transition β x y = 0 := by + -- No outcome of `x` has its reply at `y.1`, so every restriction to the reply `y` is empty. + have hr : ∀ s, (step.outcome s x).restrict (fun sy => sy.2 = y) = 0 := by + intro s + -- Pointwise at `sy = (s', y')`: the restriction is the outcome if `y' = y`, else zero. + ext sy + rw [restrict_apply] + split_ifs with h + · -- an outcome with reply `y` would be the tag of a step replying at `x.1` + rw [outcome, fTransform_apply_eq_mass] + -- (a step `a` tagged to `sy` with `sy.2 = y` would force `y.1 = x.1`, against `hy`) + exact mass_eq_zero_of_forall_not _ fun a ha => hy (by rw [← h, ← ha]; rfl) + -- a reply other than `y`: both sides are zero + · rfl + -- The kernel vanishes, so the mixture does. + rw [transition] + simp only [hr] + -- Each kernel law is the projection of zero, which is zero; a mixture of zeros is zero. + exact (bindK_congr fun _ _ => fTransform_zero _).trans (bindK_zero_right β) + +variable (D : Domain (Σ i, X i) (Σ i, Y i)) (init : Distribution S) + +open scoped Classical in +/-- The state laws along a reversed transcript. -/ +noncomputable def beliefRev : List ((Σ i, X i) × (Σ i, Y i)) → Distribution S + | [] => init + | e :: rh => if D rh.reverse e.1 then step.transition (beliefRev rh) e.1 e.2 else 0 + +/-- **The state law after the transcript `h`**: the sub-law of the states reached with the +replies of `h`, started from `init`; zero once a query is outside the domain. -/ +noncomputable def belief (h : List ((Σ i, X i) × (Σ i, Y i))) : Distribution S := + step.beliefRev D init h.reverse + +@[simp] lemma belief_nil : step.belief D init [] = init := rfl + +open scoped Classical in +/-- One more exchange: the transition of the state law, if the domain admits the query. -/ +lemma belief_snoc (h : List ((Σ i, X i) × (Σ i, Y i))) (x : Σ i, X i) (y : Σ i, Y i) : + step.belief D init (h ++ [(x, y)]) = + if D h x then step.transition (step.belief D init h) x y else 0 := by + -- Reversed, the exchange `(x, y)` comes first: one step of `beliefRev`. + -- + -- belief h ──(x, reply y)──▶ belief (h · (x, y)) if the domain admits `x` after `h` + -- = 0 otherwise + simp [belief, beliefRev, List.reverse_append] + +/-- The state laws of a nonnegative initial law are nonnegative. -/ +lemma belief_nonNeg (hinit : init.NonNeg) (h : List ((Σ i, X i) × (Σ i, Y i))) : + (step.belief D init h).NonNeg := by + -- Induction on the transcript: each exchange is a transition of a nonnegative law, or zero. + induction h using List.reverseRecOn with + | nil => exact hinit + | append_singleton h e ih => + rw [belief_snoc] + split_ifs + -- admitted query: a transition of the state law after `h`, nonnegative by induction + · exact step.transition_nonNeg ih _ _ + -- query outside the domain: the zero law + · exact fun _ => le_rfl + +end ProbStep + +variable {S I : Type} {X Y : I → Type} [Fintype (Σ i, X i)] [Fintype (Σ i, Y i)] + +open scoped Classical in +/-- **The random system of a probabilistic automaton** with its initial state sampled from +`init`: the probability of a transcript is the weight of the state law after it. -/ +noncomputable def RandomSystem.ofProbAutomaton (D : Domain (Σ i, X i) (Σ i, Y i)) + (step : ProbStep S I X Y) (init : Distribution.ProbDist S) : + RandomSystem (Σ i, X i) (Σ i, Y i) D := + -- The fields of a random system: the probability of `h` is the weight of the state law + -- after it; the empty transcript has the weight of `init`, which is one; probabilities are + -- nonnegative as the state laws are; and, at each `h` and `x`, a reply law below. + ⟨fun h => (step.belief D init.1 h).weight, init.2.2, + fun h => (step.belief_nonNeg D init.1 init.2.1 h).weight_nonneg, fun h x => + -- At an admitted query, the replies have the law of the reply from the current state law; + -- elsewhere no reply has mass. + ⟨if D h x then step.replyLaw (step.belief D init.1 h) x else 0, fun y => by + -- the reply `y` has the weight of the state law after `h · (x, y)` ... + change _ = (step.belief D init.1 (h ++ [(x, y)])).weight + rw [step.belief_snoc] + split_ifs + · -- ... which is the transition with the reply `y` + exact step.replyLaw_apply _ _ _ + · -- ... or zero, outside the domain + simp [weight], by + -- the reply law has the weight of the state law after `h`, or zero outside the domain + split_ifs + · exact step.weight_replyLaw _ _ + · simp [weight]⟩⟩ + +/-- The probability of a transcript is the weight of the state law after it. -/ +lemma RandomSystem.ofProbAutomaton_apply (D : Domain (Σ i, X i) (Σ i, Y i)) + (step : ProbStep S I X Y) (init : Distribution.ProbDist S) + (h : List ((Σ i, X i) × (Σ i, Y i))) : + RandomSystem.ofProbAutomaton D step init h = (step.belief D init.1 h).weight := rfl + +/-- **A probabilistic automaton replies at the queried port.** -/ +lemma RandomSystem.ofProbAutomaton_repliesAtQueriedInterface (D : Domain (Σ i, X i) (Σ i, Y i)) + (step : ProbStep S I X Y) (init : Distribution.ProbDist S) : + (RandomSystem.ofProbAutomaton D step init).RepliesAtQueriedInterface := by + -- A transcript `h`, a query `x`, and a reply `y` at a port `y.1 ≠ x.1`. + intro h x y hy + -- The probability of `h · (x, y)` is the weight of the state law after it ... + rw [ofProbAutomaton_apply, step.belief_snoc] + split_ifs + · -- ... which is the transition with a reply at another port: no state is reached. + rw [step.transition_eq_zero hy] + simp [weight] + · -- ... or zero, when the domain does not admit `x`. + simp [weight] + +/-! ### Simulations -/ + +namespace ProbStep + +variable {S₁ S₂ : Type} (step₁ : ProbStep S₁ I X Y) (step₂ : ProbStep S₂ I X Y) + +/-- **A simulation step** of `step₁` by `step₂` along the kernel `K`, at the state `s` and the +query `x`: from the kernel image of `s`, a step of `step₂` is a step of `step₁` from `s` followed +by the kernel, with the same reply. + +``` + s ──── step₁, x ────► (s₁', y) + │ │ + K K + ▼ ▼ + K(s) ─── step₂, x ────► (s₂', y) +``` +-/ +def SimulatesAt (K : S₁ → Distribution.ProbDist S₂) (s : S₁) (x : Σ i, X i) : Prop := + bindK (K s).1 (fun s₂ => step₂.outcome s₂ x) = + bindK (step₁.outcome s x) fun p => fTransform (fun s₂ => (s₂, p.2)) (K p.1).1 + +omit [Fintype (Σ i, X i)] [Fintype (Σ i, Y i)] in +open scoped Classical in +/-- The states of a pushforward into pairs `(a, c)` with second component `y`. -/ +lemma fTransform_fst_restrict_pair {A C : Type} (ν : Distribution A) (c y : C) : + fTransform Prod.fst ((fTransform (fun a => (a, c)) ν).restrict fun p => p.2 = y) = + if c = y then ν else 0 := by + -- Restricting the pairs to the second component `y` keeps everything if `c = y` and nothing + -- otherwise; then forgetting `c` gives back `ν`. + rw [restrict_fTransform, fTransform_fTransform] + split_ifs with h + -- `c = y`: every pair passes the event; restricting to `True` keeps `ν`, and `a ↦ (a, c).1` + -- is the identity. + · rw [restrict_congr ν (Q := fun _ => True) fun _ => by simp [h]] + rw [show (ν.restrict fun _ => True) = ν by ext; simp] + exact fTransform_id ν + -- `c ≠ y`: no pair passes; the restriction to `False` is zero, and so is its pushforward. + · rw [restrict_congr ν (Q := fun _ => False) fun _ => by simp [h], restrict_false] + exact fTransform_zero _ + +omit [Fintype (Σ i, X i)] [Fintype (Σ i, Y i)] in +/-- **Transitions along simulation steps**: the transition of the kernel image is the kernel +image of the transition. -/ +lemma transition_bindK {K : S₁ → Distribution.ProbDist S₂} {β : Distribution S₁} + {x : Σ i, X i} (hsim : ∀ s ∈ β.support, SimulatesAt step₁ step₂ K s x) (y : Σ i, Y i) : + step₂.transition (bindK β fun s => (K s).1) x y = + bindK (step₁.transition β x y) fun s => (K s).1 := by + -- Plan: at each state `s` of `β`, the claim is the simulation step at `s` restricted to the + -- reply `y`, with the reply then forgotten: + -- + -- (fst ∘ [reply = y]) (∑_{s₂ ~ K s} step₂ s₂ x) + -- = (fst ∘ [reply = y]) (∑_{(s₁', y') ~ step₁ s x} (K s₁', y')) (simulation step at s) + -- = ∑_{(s₁', y') ~ step₁ s x} [y' = y] · K s₁' + -- = ∑_{s₁' ~ fst ([reply = y] (step₁ s x))} K s₁' + -- + -- 1. Write both sides as mixtures over `β` and compare them state by state. + -- 2. Move the restriction to the reply `y` and the projection out of the mixture over `K s`. + -- 3. Replace that mixture by the step of `step₁` followed by `K` (`hsim` at `s`). + -- 4. Move the restriction and projection back over the outcomes of `step₁` and evaluate. + -- + -- Step 1. + -- Both sides are mixtures over `β`; compare them state by state. + rw [transition, transition, bindK_bindK, bindK_bindK] + refine bindK_congr fun s hs => ?_ + -- Step 2. + -- Left: from `K s`, the step of `step₂` restricted to the reply `y`, next states only. + -- Move the restriction and the projection outside the mixture over `K s`. + have hpush : (bindK (K s).1 fun s₂ => + fTransform Prod.fst ((step₂.outcome s₂ x).restrict fun sy => sy.2 = y)) = + fTransform Prod.fst ((bindK (K s).1 fun s₂ => step₂.outcome s₂ x).restrict + fun sy => sy.2 = y) := by + -- restriction and pushforward commute with mixtures + rw [restrict_bindK, fTransform_bindK] + rw [hpush] + -- Step 3. + -- The simulation step replaces the mixture by the step of `step₁` followed by `K`. + rw [hsim s hs] + -- Step 4. + -- Move the restriction and projection back inside, over the outcomes `p` of `step₁`. + rw [restrict_bindK, fTransform_bindK] + -- For each outcome `p = (s₁', y')`: `K s₁'` if `y' = y`, nothing otherwise. + simp only [fTransform_fst_restrict_pair] + -- Keeping the outcomes with reply `y` and their next states is the right-hand side. + rw [bindK_ite, bindK_fTransform] + -- both kernels are `p ↦ K p.1` + rfl + +omit [Fintype (Σ i, X i)] [Fintype (Σ i, Y i)] in +/-- **The state laws along a simulation**: if `step₂` simulates `step₁` along `K` at the states +satisfying an invariant of the inputs so far, at every query the domain admits, then after each +transcript the invariant holds on the states of `step₁`, and the state law of `step₂` is the +kernel image of that of `step₁`. -/ +lemma belief_simulation (E : List (Σ i, X i) → Prop) (bound : ℕ) + (hE : ∀ h, E h → h.length ≤ bound) (K : S₁ → Distribution.ProbDist S₂) + (inv : List (Σ i, X i) → S₁ → Prop) + (hpres : ∀ xs s x, inv xs s → E (xs ++ [x]) → + ∀ p ∈ (step₁.outcome s x).support, inv (xs ++ [x]) p.1) + (hsim : ∀ xs s x, inv xs s → E (xs ++ [x]) → SimulatesAt step₁ step₂ K s x) + (init : Distribution S₁) (hinit : ∀ s ∈ init.support, inv [] s) + (h : List ((Σ i, X i) × (Σ i, Y i))) : + (∀ s ∈ (step₁.belief (Domain.ofInputs E bound hE) init h).support, inv (h.map Prod.fst) s) ∧ + step₂.belief (Domain.ofInputs E bound hE) (bindK init fun s => (K s).1) h = + bindK (step₁.belief (Domain.ofInputs E bound hE) init h) fun s => (K s).1 := by + -- Plan: prove both claims together, by induction on the transcript. Writing `βᵢ` for the + -- state laws of `step₁`, the square below commutes at every exchange: + -- + -- init ───(x₁, y₁)───▶ β₁ ───(x₂, y₂)───▶ β₂ ⋯ state laws of step₁ + -- │ K │ K │ K + -- ▼ ▼ ▼ + -- K(init) ─(x₁, y₁)──▶ K(β₁) ─(x₂, y₂)──▶ K(β₂) ⋯ state laws of step₂ + -- + -- 1. Empty transcript: the invariant holds on `init` (`hinit`), and the initial law of + -- `step₂` is the kernel image of `init` by definition. + -- 2. One more exchange `(x, y)` that the domain admits: the invariant passes to the states + -- reached (`hpres`); the states after `h` satisfy the invariant, so `step₂` simulates + -- `step₁` there (`hsim`), and the transition commutes with `K` (`transition_bindK`). + -- 3. An exchange the domain does not admit: both state laws are zero. + -- + -- Induction on the transcript, one exchange `(x, y)` at a time. + induction h using List.reverseRecOn with + -- Step 1. + | nil => exact ⟨hinit, rfl⟩ + | append_singleton h e ih => + obtain ⟨x, y⟩ := e + -- After `h · (x, y)` each state law is the transition of the one after `h` if the domain + -- admits `x`, and zero otherwise; case on the domain. + rw [belief_snoc, belief_snoc] + split_ifs with hd + -- Step 2. + -- (admitting `x` after `h` means the inputs of `h` followed by `x` are in `E`) + · have hd' : E (h.map Prod.fst ++ [x]) := hd + refine ⟨fun s hs => ?_, ?_⟩ + · -- A state after `h · (x, y)` is reached by a step from a state after `h`, which + -- satisfies the invariant; the step preserves it. + -- `s` gets mass from some state `s₀` after `h` ... + obtain ⟨s₀, hs₀, hs⟩ := mem_support_bindK hs + -- ... as the next state of an outcome `p` of `step₁` from `s₀` with reply `y` ... + obtain ⟨p, hp, rfl⟩ := mem_support_fTransform _ _ hs + -- ... which is a possible outcome (restricting only removes mass); + have hp' : p ∈ (step₁.outcome s₀ x).support := support_restrict_subset _ _ hp + -- `hpres` at `s₀`; the inputs of `h · (x, y)` are those of `h` followed by `x`. + simpa using hpres _ _ x (ih.1 s₀ hs₀) hd' p hp' + · -- The state law of `step₂` after `h` is the kernel image (induction hypothesis), and + -- transitions commute with the kernel along simulation steps. + rw [ih.2] + exact transition_bindK step₁ step₂ (fun s hs => hsim _ s x (ih.1 s hs) hd') y + -- Step 3. + · -- The query is not admitted: both state laws are zero. + -- (the zero law has no states, and the kernel image of zero is zero) + exact ⟨fun s hs => absurd hs (by simp), by simp⟩ + +end ProbStep + +/-- **Equal random systems along a simulation**: if `step₂` simulates `step₁` along `K` at the +states satisfying an invariant of the inputs so far, at every query the domain admits, the +probabilistic automata are the same random system, `step₂` started from the kernel image of the +initial law of `step₁`. -/ +lemma RandomSystem.ofProbAutomaton_eq_of_simulation {E : List (Σ i, X i) → Prop} {bound : ℕ} + {hE : ∀ h, E h → h.length ≤ bound} {S₁ S₂ : Type} (step₁ : ProbStep S₁ I X Y) + (step₂ : ProbStep S₂ I X Y) (K : S₁ → Distribution.ProbDist S₂) + (inv : List (Σ i, X i) → S₁ → Prop) + (hpres : ∀ xs s x, inv xs s → E (xs ++ [x]) → + ∀ p ∈ (step₁.outcome s x).support, inv (xs ++ [x]) p.1) + (hsim : ∀ xs s x, inv xs s → E (xs ++ [x]) → ProbStep.SimulatesAt step₁ step₂ K s x) + (init : Distribution.ProbDist S₁) (hinit : ∀ s ∈ init.1.support, inv [] s) : + RandomSystem.ofProbAutomaton (Domain.ofInputs E bound hE) step₁ init = + RandomSystem.ofProbAutomaton (Domain.ofInputs E bound hE) step₂ (init.bind K) := by + -- Compare the probabilities of every transcript `h`. + -- Writing `β₁ h` for the state law of `step₁` after `h` and `β₂ h` for that of `step₂`: + -- + -- P₁(h) = weight (β₁ h) + -- = weight (K(β₁ h)) (each `K s` is a probability law) + -- = weight (β₂ h) (`belief_simulation`) + -- = P₂(h) + apply RandomSystem.ext + intro h + -- each probability is the weight of the state law after `h` + rw [ofProbAutomaton_apply, ofProbAutomaton_apply] + -- The state law of `step₂` after `h` is the kernel image of that of `step₁` ... + rw [ProbDist.bind_val, (ProbStep.belief_simulation step₁ step₂ E bound hE K inv hpres hsim + init.1 hinit h).2] + -- ... and a kernel of probability laws preserves the weight. + rw [weight_bindK_of_weight fun s _ => (K s).2.2] + +/-! ### Deterministic automata -/ + +namespace ProbStep + +/-- **The probabilistic step of a deterministic automaton**: the point law of its step. -/ +noncomputable def ofDeterministic (step : S → (i : I) → X i → S × Y i) : ProbStep S I X Y := + fun s i x => Distribution.ProbDist.single (step s i x) + +omit [Fintype (Σ i, X i)] [Fintype (Σ i, Y i)] in +/-- The outcome of a point step: the point mass at the step's next state and tagged reply. -/ +lemma outcome_ofDeterministic (step : S → (i : I) → X i → S × Y i) (s : S) (x : Σ i, X i) : + (ofDeterministic step).outcome s x = + Finsupp.single ((step s x.1 x.2).1, (⟨x.1, (step s x.1 x.2).2⟩ : Σ i, Y i)) 1 := by + -- The point law of the step, with its reply tagged by the port. + simp [outcome, ofDeterministic, Distribution.ProbDist.single, fTransform, tagged] + +omit [Fintype (Σ i, X i)] [Fintype (Σ i, Y i)] in +/-- The transition of a deterministic step moves the states that reply `y` to their next state. -/ +lemma transition_ofDeterministic (step : S → (i : I) → X i → S × Y i) (β : Distribution S) + (x : Σ i, X i) (y : Σ i, Y i) : + (ofDeterministic step).transition β x y = fTransform (fun s => (step s x.1 x.2).1) + (β.restrict fun s => (⟨x.1, (step s x.1 x.2).2⟩ : Σ i, Y i) = y) := by + -- Each state has one outcome; restricted to the reply `y` it is that outcome or nothing. + rw [transition] + simp only [outcome_ofDeterministic, single_restrict] + -- A kernel vanishing off an event is the kernel on the restriction, here a point kernel. + rw [← bindK_single_comp, ← bindK_ite] + -- Compare the kernels state by state. + refine bindK_congr fun s _ => ?_ + -- Reply `y`: the next-state projection of the point mass at `(s', y)` is the point mass at + -- `s'`. Another reply: both kernels give zero. + split_ifs <;> simp [fTransform] + +omit [Fintype (Σ i, X i)] [Fintype (Σ i, Y i)] in +/-- **The state law of a deterministic automaton** on an input domain: the initial states from +which the automaton gives the transcript, moved to the state they reach. -/ +lemma belief_ofDeterministic (step : S → (i : I) → X i → S × Y i) (E : List (Σ i, X i) → Prop) + (bound : ℕ) (hE : ∀ h, E h → h.length ≤ bound) (init : Distribution S) + (h : List ((Σ i, X i) × (Σ i, Y i))) : + (ofDeterministic step).belief (Domain.ofInputs E bound hE) init h = + fTransform (fun s => stateAfter step s (h.map Prod.fst)) (init.restrict fun s => + Replies (filterDom E (automatonSystem step s)) (h.map Prod.fst) (h.map Prod.snd)) := by + -- Plan: induction on the transcript. An initial state `s` is kept iff the automaton started + -- in `s` gives `h`; it then sits at the state its run reaches: + -- + -- s ──x₁ / y₁──▶ s₁ ──x₂ / y₂──▶ s₂ ⋯ ──xₙ / yₙ──▶ stateAfter step s (x₁ ⋯ xₙ) + -- + -- (each reply of the run is the `yᵢ` of `h`, and each prefix of inputs is in `E`). + -- 1. Empty transcript: every initial state gives it and stays where it is. + -- 2. One more exchange `(x, y)`: "gives `h · (x, y)`" unfolds into "gives `h`, `E` admits + -- `x`, and the reply from the state after `h` is `y`" (`hrep`). + -- 3. Admitted `x`: the deterministic transition keeps the states that reply `y` and moves + -- each one step; with the induction hypothesis this is the event of step 2, moved. + -- 4. Not admitted: the state law is zero, and no initial state gives the transcript. + induction h using List.reverseRecOn with + -- Step 1. + | nil => + -- No exchange: every initial state gives the empty transcript, and stays where it is. + simp only [belief_nil, List.map_nil, stateAfter_nil, replies_nil] + -- restricting to `True` keeps `init`, and moving along the identity keeps it too + rw [show (init.restrict fun _ => True) = init by ext; simp] + exact (fTransform_id init).symm + | append_singleton h e ih => + obtain ⟨x, y⟩ := e + -- Step 2. + -- The automaton from `s` gives `h · (x, y)` when it gives `h`, the domain admits `x`, and + -- its reply from the state after `h` is `y`. + have hrep : ∀ s, Replies (filterDom E (automatonSystem step s)) ((h ++ [(x, y)]).map Prod.fst) + ((h ++ [(x, y)]).map Prod.snd) ↔ + Replies (filterDom E (automatonSystem step s)) (h.map Prod.fst) (h.map Prod.snd) ∧ + E (h.map Prod.fst ++ [x]) ∧ + (⟨x.1, (step (stateAfter step s (h.map Prod.fst)) x.1 x.2).2⟩ : Σ i, Y i) = y := by + intro s + -- Giving `h · (x, y)` = giving `h`, and the system's answer to `x` after `h` is `y`; + -- the system filtered by `E` answers only when `E` admits the inputs `h · x`. + simp only [List.map_append, List.map_cons, List.map_nil, replies_snoc, + SystemAlgebra.filterDom, automatonSystem_snoc] + by_cases hx : E (h.map Prod.fst ++ [x]) + -- admitted: the answer is the automaton's reply, equal to `y` iff the replies agree + · simp [hx, Part.some_inj, eq_comm] + -- not admitted: no answer, so the transcript is not given + · simp [hx, Part.none_ne_some] + -- Unfold the state law after `h · (x, y)` and rewrite the event by `hrep`. + rw [belief_snoc, restrict_congr init hrep] + split_ifs with hd + -- Step 3. + · have hd' : E (h.map Prod.fst ++ [x]) := hd + -- The transition moves the states replying `y` (induction hypothesis for `h`) ... + rw [ih, transition_ofDeterministic, restrict_fTransform, fTransform_fTransform, + restrict_restrict] + -- ... to the state after `h · x`. + simp only [List.map_append, List.map_cons, List.map_nil, stateAfter_snoc] + -- Both sides move each state the same way; it remains to match the events, which + -- differ only by the conjunct `E (inputs of h · x)`, true here (`hd'`). + congr 1 + exact restrict_congr init fun s => by simp [hd'] + -- Step 4. + · -- The query is not admitted: no initial state gives the transcript. + have hd' : ¬ E (h.map Prod.fst ++ [x]) := hd + -- the event contains the false conjunct `E (inputs of h · x)`: the restriction is zero + rw [restrict_congr init (Q := fun _ => False) fun s => by simp [hd'], restrict_false] + exact (fTransform_zero _).symm + +end ProbStep + +/-- **A deterministic automaton is a probabilistic automaton** with point steps: with its initial +state sampled from `init`, a transcript has the probability of the initial states from which the +automaton gives it [1, Definition 2]. -/ +lemma RandomSystem.ofProbAutomaton_ofDeterministic_apply {E : List (Σ i, X i) → Prop} + {bound : ℕ} {hE : ∀ h, E h → h.length ≤ bound} (step : S → (i : I) → X i → S × Y i) + (init : Distribution.ProbDist S) (h : List ((Σ i, X i) × (Σ i, Y i))) : + RandomSystem.ofProbAutomaton (Domain.ofInputs E bound hE) (ProbStep.ofDeterministic step) + init h = + init.1.mass fun s => + Replies (filterDom E (automatonSystem step s)) (h.map Prod.fst) (h.map Prod.snd) := by + -- The probability is the weight of the state law: the initial states giving `h`, moved. + rw [ofProbAutomaton_apply, ProbStep.belief_ofDeterministic] + -- Moving keeps the weight, and the weight of a restriction is the mass of its event. + rw [weight_fTransform, weight_restrict] + +end SystemAlgebra diff --git a/src/Tests/Axioms/CC.lean b/src/Tests/Axioms/CC.lean index e68bcc1..a1cdd0a 100644 --- a/src/Tests/Axioms/CC.lean +++ b/src/Tests/Axioms/CC.lean @@ -91,6 +91,14 @@ classes, and the abstract results of those classes depend only on `propext`, #print axioms SystemAlgebra.Interface.parallel #print axioms SystemAlgebra.Interface.parallelConverter +-- ConstructiveCryptography.Memoryless +#print axioms SystemAlgebra.Interface.source_eq_memoryless +#print axioms SystemAlgebra.Interface.parallel_eq_memoryless +#print axioms SystemAlgebra.Interface.Converter.ofProgram_smul_memoryless +#print axioms SystemAlgebra.Interface.Converter.ofPreservingProgram_smul_memoryless +#print axioms + SystemAlgebra.Interface.Converter.ofPreservingProgram_comp_rightContext_smul_memoryless + -- ConstructiveCryptography.Notation #print axioms SystemAlgebra.Interface.distance_triangle #print axioms SystemAlgebra.Interface.tensor_smul diff --git a/src/Tests/Axioms/Commons.lean b/src/Tests/Axioms/Commons.lean index 8f12e45..91fbcbe 100644 --- a/src/Tests/Axioms/Commons.lean +++ b/src/Tests/Axioms/Commons.lean @@ -15,6 +15,7 @@ ML-DSA depend only on `propext`, `Classical.choice` and `Quot.sound`. #print axioms Commons.StrongURP #print axioms Commons.TweakableURP #print axioms Commons.TweakableStrongURP +#print axioms Commons.MemorylessSource.memoryless_eq -- Commons.Definitions.Cipher #print axioms Commons.BlockCipher.perm diff --git a/src/Tests/Axioms/Systems.lean b/src/Tests/Axioms/Systems.lean index 4c8e7bc..7ef5f56 100644 --- a/src/Tests/Axioms/Systems.lean +++ b/src/Tests/Axioms/Systems.lean @@ -4,10 +4,10 @@ import Tests.Counterexamples /-! # Axioms of the systems layer -The laws of random systems, deterministic and probabilistic converters, attachment, -parallel composition, distance and games, and the counterexamples, depend only on -`propext`, `Classical.choice` and `Quot.sound`. Comments name the laws of -`papers/SYSTEM_ALGEBRA_SPEC.md`. +The laws of random systems, deterministic and probabilistic converters, attachment, parallel +composition, probabilistic automata, memoryless systems, distance and games, and the +counterexamples, depend only on `propext`, `Classical.choice` and `Quot.sound`. Comments name the +laws of `papers/SYSTEM_ALGEBRA_SPEC.md`. -/ -- RandomSystems.Converter.ConverterAttachment @@ -47,6 +47,15 @@ parallel composition, distance and games, and the counterexamples, depend only o #print axioms SystemAlgebra.IsDDC.trim_serialM_id #print axioms SystemAlgebra.IsDDC.trim_id_serialM +-- RandomSystems.Converter.ProbProgramAttachment +#print axioms SystemAlgebra.Program.ofDeterministic_combine +#print axioms SystemAlgebra.Program.simulatesAt_probCombine +#print axioms SystemAlgebra.RandomSystem.ofProbAutomaton_probCombine_eq_of_simulation +#print axioms SystemAlgebra.ProbStep.simulatesAt_drawStep +#print axioms SystemAlgebra.RandomSystem.ofProbAutomaton_eq_drawStep +#print axioms SystemAlgebra.PDCBehavior.attach_ofDDC_ofProgramOn_ofDeterministic +#print axioms SystemAlgebra.PDCBehavior.attach_ofDDC_ofProgramOn_ofProbAutomaton + -- RandomSystems.Converter.ResourceAttachment #print axioms SystemAlgebra.MapsDomain.comp #print axioms SystemAlgebra.IsResponsiveDDC.mapsDomain_of_replies @@ -254,6 +263,13 @@ parallel composition, distance and games, and the counterexamples, depend only o #print axioms SystemAlgebra.close_pair -- E2, only `D` terminating #print axioms SystemAlgebra.partialClose_isDDD -- `S` arbitrary +-- RandomSystems.System.Memoryless +#print axioms SystemAlgebra.RandomSystem.memoryless +#print axioms SystemAlgebra.RandomSystem.eq_memoryless_of_snoc +#print axioms SystemAlgebra.RandomSystem.ofProbAutomaton_eq_memoryless +#print axioms SystemAlgebra.Program.memoryless_probCombine +#print axioms SystemAlgebra.PDCBehavior.attach_ofDDC_ofProgramOn_memoryless + -- RandomSystems.System.Observation #print axioms SystemAlgebra.close_decision #print axioms SystemAlgebra.close_dom_iff_compatible @@ -261,6 +277,13 @@ parallel composition, distance and games, and the counterexamples, depend only o #print axioms SystemAlgebra.behEq_iff_transcript_DDD #print axioms SystemAlgebra.dde_blind_beyond_resources +-- RandomSystems.System.ProbAutomaton +#print axioms SystemAlgebra.RandomSystem.ofProbAutomaton +#print axioms SystemAlgebra.RandomSystem.ofProbAutomaton_repliesAtQueriedInterface +#print axioms SystemAlgebra.ProbStep.belief_simulation +#print axioms SystemAlgebra.RandomSystem.ofProbAutomaton_eq_of_simulation +#print axioms SystemAlgebra.RandomSystem.ofProbAutomaton_ofDeterministic_apply + -- RandomSystems.System.Replies #print axioms SystemAlgebra.replies_trim_iff diff --git a/src/Tests/DSL/Axioms.lean b/src/Tests/DSL/Axioms.lean index 8ffb20f..0e08375 100644 --- a/src/Tests/DSL/Axioms.lean +++ b/src/Tests/DSL/Axioms.lean @@ -1,4 +1,5 @@ import Examples.DSL.AEADTests +import Examples.PRGLengthExtension import Tests.DSL.Diagnostics import Tests.DSL.Semantics @@ -78,6 +79,10 @@ checks depend only on `propext`, `Classical.choice` and `Quot.sound`. #print axioms DSLExamples.Cipher.cbc_nonexpanding #print axioms DSLExamples.Authenticated.AuthenticatedEncryption #print axioms DSLExamples.Authenticated.authenticatedEncryption_eq +#print axioms Examples.PRGLengthExtension.prgReal_H_eq +#print axioms Examples.PRGLengthExtension.𝓡₁_smul_prgRand +#print axioms Examples.PRGLengthExtension.𝓡₂_smul_prgRand +#print axioms Examples.PRGLengthExtension.prg_length_extension -- Checks. #print axioms DSLTests.Semantics.freshBits_independent