Expose deterministic reply transformations

src/Commons.lean

@@ -22,6 +22,7 @@ public import Commons.Definitions.Nonce
 public import Commons.Definitions.NonceAEAD
 public import Commons.Definitions.MAC
 public import Commons.Definitions.MAC.Keyed
+public import Commons.Definitions.ReplyTransform
 public import Commons.Definitions.PRG
 public import Commons.Definitions.PublicKeyEncryption
 public import Commons.Definitions.PublicKeyEncryption.Keyed

src/Commons/Definitions/ReplyTransform.lean

@@ -0,0 +1,45 @@
+module
+
+public import Commons.Definitions.Ideal
+public import RandomSystems.Typed.QueryRouting
+
+/-!
+# Transforming evaluation replies
+
+`mapReplies f q` forwards an `eval(())` query once and returns `f x` on the inside reply `x`.
+The per-port allowance `q` is unchanged. `mapReplies_smul_memorylessSource` identifies
+the attached source with the source of the mapped probability law.
+
+```text
+caller ── eval(()) ──► [mapReplies f] ── eval(()) ──► source P
+       ◄──── f x ────              ◄────── x ─────
+```
+-/
+
+@[expose] public section
+
+namespace Commons.Evaluation
+
+open SystemAlgebra Probability.Distribution
+
+/-- Forward each `eval(())` once and return `f x`; keep no state between calls. -/
+noncomputable def mapReplies
+    -- `X`, `Y` are the inside and outside reply alphabets; `f` transforms one reply.
+    {X Y : Type} [Fintype X] [Fintype Y] (f : X → Y)
+    -- `q` permits the same number of evaluations at both interfaces.
+    (q : Evaluation.Port → ℕ) :
+    TypedConverter (Evaluation.perPort Unit Y q) (Evaluation.perPort Unit X q) :=
+  TypedConverter.mapReplies (Evaluation.perPort Unit X q) (fun _ => f)
+
+/-- Mapping fresh replies from `P` by `f` gives fresh replies from `P.map f`. -/
+lemma mapReplies_smul_memorylessSource
+    -- `f` transforms each inside reply from `X` into an outside reply in `Y`.
+    {X Y : Type} [Fintype X] [Fintype Y] (f : X → Y)
+    -- `P` is the fresh inside law; `q` is the shared query allowance.
+    (P : ProbDist X) (q : Evaluation.Port → ℕ) :
+    mapReplies f q • MemorylessSource.perPort X P (budget := q) =
+      MemorylessSource.perPort Y (P.map f) (budget := q) := by
+  rw [MemorylessSource.eq_ofMemoryless, MemorylessSource.eq_ofMemoryless]
+  exact TypedConverter.mapReplies_smul_ofMemoryless _ _ _
+
+end Commons.Evaluation

src/RandomSystems/Typed/Interface.lean

@@ -13,6 +13,7 @@ The carriers are indexed by finite interfaces, using the systems and converters
 [2, Definitions 2.2.1–2.2.2, pp. 16–18] and [3, Definitions 3.8–3.9, p. 62; Definition 3.17, p. 64].
 
 `Interface.queryBudget` and `Interface.portBudget` admit total and per-port query bounds.
+`Interface.withReplies` replaces reply alphabets while preserving ports, queries and domain.
 `Interface.queryBudget_domain_map` transfers one-query maps when `A.bound ≤ q`;
 `Interface.queryBudget_inputDomain_iff` reduces next-query admission to a length inequality.
 `TypedSystem.ofPDS` presents a sampled deterministic system; `TypedSystem.exists_ofPDS` gives
@@ -60,6 +61,12 @@ attribute [instance] Interface.instFintypeI Interface.instFintypeX Interface.ins
 
 namespace Interface
 
+/-- Replace `A.Y i` by `Y i`, retaining the queries, domain and bound of `A`. -/
+abbrev withReplies
+    -- `A` supplies the ports and admitted input histories; `Y i` is the new reply alphabet.
+    (A : Interface) (Y : A.I → Type) [∀ i, Fintype (Y i)] : Interface :=
+  { A with Y := Y, instFintypeY := inferInstance }
+
 /-- `D = {h | h ≠ [] ∧ h.length ≤ q}` admits at most `q` queries in total. -/
 abbrev queryBudget
     -- `I` indexes finite ports; `X i`, `Y i` carry their finite query and reply alphabets.

src/RandomSystems/Typed/QueryRouting.lean

@@ -20,8 +20,13 @@ lets the reply alphabets `B.Y j` differ from `A.Y o` and from each other.
                 └───────────────────────┘            └────────────┘
 ```
 
+`mapReplies A f` forwards each query unchanged and returns `f i y` in a common output alphabet.
+It preserves `A.domain` exactly.
+
 ## Main results
 
+* `mapReplies_smul_ofFunction`, `mapReplies_smul_ofMemoryless` and `mapReplies_smul_source`:
+  contracts for reply mapping on deterministic systems, fresh laws and sources
 * `TypedConverter.routing`: one inside query and a translated reply, with an explicit domain map
 * `TypedConverter.routing_smul_ofFunction`: `α • ofFunction f = ofFunction g`
 * `TypedConverter.routing_smul_ofMemoryless`: fresh inside replies stay fresh; their laws are
@@ -143,4 +148,46 @@ lemma routing_smul_ofMemoryless
     B.nonempty_prefix A.nonempty_prefix () (routingProgram request answer)
     (routingProgram_bounded request answer) hp hκ rfl (TypedSystem.ofMemoryless B ν).2)
 
+/-- Forward query `(i,x)` once and return `f i y` on reply `y : A.Y i`.
+The outside interface retains `A.domain`; successive calls share no converter state. -/
+noncomputable def mapReplies
+    -- `A` is the inside interface, including any restrictions on its input histories.
+    (A : Interface)
+    -- `Y` is the common outside reply alphabet; `f i` transforms replies at port `i`.
+    {Y : Type} [Fintype Y] (f : ∀ i, A.Y i → Y) :
+    TypedConverter (A.withReplies (fun _ => Y)) A :=
+  routing id (fun _ r => f r.1 r.2)
+    (fun _ h => by simpa only [List.map_id] using h)
+
+/-- Transforming the fixed reply `g i x` returns `f i (g i x)` on the same domain. -/
+lemma mapReplies_smul_ofFunction
+    -- `A` fixes the admitted queries; `f i` maps their inside replies to `Y`.
+    (A : Interface) {Y : Type} [Fintype Y] (f : ∀ i, A.Y i → Y)
+    -- `g i x` is the deterministic inside reply to query `x` at port `i`.
+    (g : ∀ i, A.X i → A.Y i) :
+    mapReplies A f • TypedSystem.ofFunction g =
+      TypedSystem.ofFunction (A := A.withReplies (fun _ => Y)) (fun i x => f i (g i x)) :=
+  routing_smul_ofFunction _ _ _ _
+
+/-- Fresh replies with law `ν i x` become fresh replies with law `(ν i x).map (f i)`. -/
+lemma mapReplies_smul_ofMemoryless
+    -- `A` fixes the admitted queries; `f i` transforms inside replies into `Y`.
+    (A : Interface) {Y : Type} [Fintype Y] (f : ∀ i, A.Y i → Y)
+    -- `ν i x` is the fresh inside reply law at query `(i,x)`.
+    (ν : ∀ i, A.X i → ProbDist (A.Y i)) :
+    mapReplies A f • TypedSystem.ofMemoryless A ν =
+      TypedSystem.ofMemoryless (A.withReplies (fun _ => Y)) (fun i x => (ν i x).map (f i)) :=
+  routing_smul_ofMemoryless _ _ _ _
+
+/-- Mapping each source reply by `f` gives the source of `P.map f`, with the same allowance. -/
+lemma mapReplies_smul_source
+    -- `X`, `Y` are the inside and outside reply alphabets; `f` transforms one reply.
+    {X Y : Type} [Fintype X] [Fintype Y] (f : X → Y)
+    -- `P` supplies fresh inside replies, for at most `q` calls.
+    (P : ProbDist X) (q : ℕ) :
+    mapReplies (Interface.source X q) (fun _ => f) • TypedSystem.source P q =
+      TypedSystem.source (P.map f) q := by
+  rw [TypedSystem.source_eq_ofMemoryless, TypedSystem.source_eq_ofMemoryless]
+  exact mapReplies_smul_ofMemoryless _ _ _
+
 end SystemAlgebra.TypedConverter

src/Tests.lean

@@ -10,6 +10,7 @@ public import Tests.Problem
 public import Tests.GameConsumers
 public import Tests.Guessing
 public import Tests.ContractApplication
+public import Tests.ReplyTransform
 public import Tests.RecordingGuard
 public import Tests.AllDistinguishers
 public import Tests.MixtureObservation

src/Tests/ReplyTransform.lean

@@ -0,0 +1,45 @@
+module
+
+public import Commons.Definitions.ReplyTransform
+
+/-!
+# Reply transformation clients
+
+A client supplies an ordinary function and rewrites with its source contract.
+`TypedConverter.mapReplies`
+accepts arbitrary restricted input domains, including an empty source domain.
+-/
+
+@[expose] public section
+
+namespace Tests.ReplyTransform
+
+open Commons Commons.Evaluation SystemAlgebra Probability.Distribution
+
+-- `f` maps finite inside replies `X` to finite outside replies `Y`; `P` is the fresh inside law.
+variable {X Y : Type} [Fintype X] [Fintype Y] (f : X → Y) (P : ProbDist X)
+
+example (q : ℕ) :
+    mapReplies f (fun _ => q) • MemorylessSource.perPort X P (budget := fun _ => q) =
+      MemorylessSource.perPort Y (P.map f) (budget := fun _ => q) := by
+  rw [mapReplies_smul_memorylessSource]
+
+-- Zero permitted queries still give a well-typed converter and source contract.
+example :
+    TypedConverter.mapReplies (Interface.source X 0) (fun _ => f) • TypedSystem.source P 0 =
+      TypedSystem.source (P.map f) 0 := by
+  rw [TypedConverter.mapReplies_smul_source]
+
+-- `A` may restrict query values and their order; reply mapping leaves that domain intact.
+example (A : Interface) (g : ∀ i, A.Y i → Y) (ν : ∀ i, A.X i → ProbDist (A.Y i)) :
+    TypedConverter.mapReplies A g • TypedSystem.ofMemoryless A ν =
+      TypedSystem.ofMemoryless (A.withReplies (fun _ => Y)) (fun i x => (ν i x).map (g i)) := by
+  rw [TypedConverter.mapReplies_smul_ofMemoryless]
+
+example (A : Interface) :
+    (A.withReplies (fun _ => Y)).domain = A.domain := rfl
+
+#print axioms TypedConverter.mapReplies_smul_ofMemoryless
+#print axioms mapReplies_smul_memorylessSource
+
+end Tests.ReplyTransform