Apply typed contracts through named assemblies

src/ConstructiveCryptography/Instances/Substitution.lean

@@ -3,9 +3,10 @@ module
 public import RandomSystems.Typed.Context
 public import ConstructiveCryptography.Substitution.Relaxation
 public import ConstructiveCryptography.Instances.Algebra
+public import ConstructiveCryptography.Notation.Basic
 
 /-!
-# Substitution images and parallel composition
+# Typed substitution and parallel composition
 
 For interfaces, the fixed contexts `TypedConverter.rightContext` and `TypedConverter.leftContext`
 realize parallel composition with a fixed typed system. A single-substitution relaxation whose
@@ -25,11 +26,16 @@ So placing a fixed system beside a one-use image `ρ(X₀)` is the one-use image
 composite transformation `context ≫ ρ`, with the same fixed system beside `ρ(X₁)`. These are
 exact equalities of typed systems; no error is involved.
 
-## Main results
+`TypedConverter.substitutesWithin_attach` transports a selected-test bound through attachment,
+with the typed reduced test `d.absorb α`. `singleSubstitutionRelaxation_parallelCompatible`
+lifts one-use substitution images through both ordered parallel contexts.
 
-* `singleSubstitutionRelaxation_parallelCompatible`
+## References
 
-Source: Banfi 2023, §4.1.4; Jost, §2.2.2.
+1. F. Banfi. *A Composable Treatment of Anonymous Communication*. Doctoral thesis,
+   Diss. ETH No. 29663, ETH Zurich, 2023.
+2. D. Jost. *On Generalizations of Composable Security*. Doctoral thesis,
+   Diss. ETH No. 26723, ETH Zurich, 2020.
 -/
 
 @[expose] public section
@@ -45,29 +51,22 @@ open CategoryTheory CategoryTheory.MonoidalCategory
 open ConstructiveCryptography.CryptographicAlgebra
 
 
-/-- The literal one-use substitution relaxation preserves independent
-parallel composition under explicit closure of the admitted transformations in both
-ordered context positions.
-
-Banfi, Section 4.1.4 (printed p. 76), requires an "(efficient) transformation".
-These closure hypotheses do not assert that arbitrary converters are efficient.
-Jost's locality equation, Proposition 2.2.3 (printed p. 18), supplies
-"composition order independence"; its concrete RS realization is already
-proved by the two context-attachment equations.
-
-With `φ_A = singleSubstitutionRelaxation (transformations A) left right (diagonal A)`, for
-specifications `𝒮` on `A` and `𝒯` on `B`:
+/-- One-use substitution preserves independent parallel composition when admitted transformations
+are closed under both ordered contexts for every fixed system.
+Write `φ_A = singleSubstitutionRelaxation (transformations A) left right (diagonal A)`.
+For specifications `𝒮` on `A` and `𝒯` on `B`, with `X₀ = left`, `X₁ = right`:
 
 ```text
 φ_A(𝒮) ∥ 𝒯 ⊆ φ_{A⊗B}(𝒮 ∥ 𝒯)       ρ(X₀) ∥ T = (rightContext A T ≫ ρ)(X₀)
 𝒮 ∥ φ_B(𝒯) ⊆ φ_{A⊗B}(𝒮 ∥ 𝒯)       S ∥ ρ(X₀) = (leftContext S B ≫ ρ)(X₀)
 ```
 
-Here `S ∈ 𝒮`, `T ∈ 𝒯`, and `ρ` is the admitted transformation witnessing the relaxed
-component. Its `X₁`-side `ρ(X₁)` lies in `𝒮` (resp. `𝒯`), so `ρ(X₁) ∥ T` (resp.
-`S ∥ ρ(X₁)`) lies in `𝒮 ∥ 𝒯`.
-The two positions are handled by different contexts, so no symmetry of `∥` is used. The
-closure hypotheses quantify over every fixed system `context`. -/
+Here `S ∈ 𝒮`, `T ∈ 𝒯`, and `ρ` is the admitted witness at the replaced interface. The same
+context at `X₁` gives `ρ(X₁) ∥ T ∈ 𝒮 ∥ 𝒯` or `S ∥ ρ(X₁) ∈ 𝒮 ∥ 𝒯`, respectively.
+[1, §4.1.4, p. 76] requires an “(efficient) transformation”; `transformations` is an explicit
+admitted class whose efficiency is a property of the caller's model.
+[2, Proposition 2.2.3, p. 18] gives “composition order independence”, instantiated here by
+the two context-attachment equations. -/
 theorem singleSubstitutionRelaxation_parallelCompatible
     -- `D : Interface` is the interface of the assumption's two systems.
     {D : Interface}
@@ -139,3 +138,25 @@ theorem singleSubstitutionRelaxation_parallelCompatible
 end
 
 end SystemAlgebra.Substitution
+
+namespace SystemAlgebra.TypedConverter
+
+open ConstructiveCryptography
+
+/-- A selected-test bound survives attachment through `α`, at the reduced test `d.absorb α`. -/
+lemma substitutesWithin_attach
+    -- The instance selects the admitted tests at every interface.
+    [AdmissibleDistinguishers Interface TypedDistinguisher]
+    -- `A` is the outside interface; `B` carries the compared inside systems.
+    {A B : Interface} (α : TypedConverter A B)
+    -- `closed` admits `d.absorb α` whenever the outside test `d` is admitted.
+    (closed : AdmissibleDistinguishers.ClosedUnder
+      (Phi := TypedSystem) (D := TypedDistinguisher) α)
+    -- `h` bounds the advantage between `R`, `S` by the inside-test-dependent error `ε`.
+    {R S : TypedSystem B} {ε : TypedDistinguisher B → ENNReal} (h : R ≃[ε] S) :
+    α • R ≃[fun d => ε (d.absorb α)] α • S := by
+  -- The interface instance interprets abstract absorption as typed converter absorption.
+  simpa only [DistinguisherAction.absorb] using
+    (AdmissibleDistinguishers.substitutesWithin_attach α closed h)
+
+end SystemAlgebra.TypedConverter

src/ConstructiveCryptography/Tactics/Substitution.lean

@@ -1,14 +1,16 @@
 module
 
 public import ConstructiveCryptography.Tactics.Basic
+public import ConstructiveCryptography.Instances.Substitution
 public import ConstructiveCryptography.Substitution.Quantitative
 public import ConstructiveCryptography.CryptographicAlgebra.DistinguisherAction
 
 /-!
 # Substitution proof commands
 
-Commands that apply the substitution laws to supplied terms (Banfi, Definition 2.3.1 and
-§2.3.1).
+Commands that apply named substitution laws to supplied terms. For typed systems,
+`TypedConverter.substitutesWithin_attach` gives the transported loss `fun d => ε (d.absorb α)`
+under explicit closure of the selected test class.
 
 * `cc_substitute relation through converter using premise` applies preservation.
 * `cc_substitution_chain relation using witness, premises` interprets a witness.
@@ -101,7 +103,7 @@ syntax ppIndent(colGe term:51 " ≃ " term " := " "← " term) : ccSubstitutionC
 
 syntax ccSubstitutionCalcSteps := ppLine withPosition(
   ccSubstitutionCalcStep (ppLine linebreak ccSubstitutionCalcStep)*)
-/-- A Banfi substitution calculation elaborated through Lean's existing `calc`. -/
+/-- A substitution calculation elaborated through Lean's existing `calc`. -/
 syntax (name := ccCalc) "cc_calc " term:max ccSubstitutionCalcSteps : tactic
 
 open Lean Elab Tactic in
@@ -255,8 +257,7 @@ partial def ccUsageRule? (witness : Expr) : MetaM (Option (Name × Expr)) := do
     return none
 
 open Lean Meta Elab Tactic in
-/-- Normalize use counts by constructor-directed structural laws, not by
-enumerating positions or trying unrelated count rules at default transparency. -/
+/-- Normalize use counts by constructor-directed structural laws. -/
 elab "cc_usage" : tactic => Lean.Elab.Tactic.withMainContext do
   let rec findUsage (expression : Expr) : MetaM (Option (Expr × Name × Expr)) := do
     if expression.isAppOf ``SubstitutionRelation.Implication.usageCount &&
@@ -322,7 +323,8 @@ open Lean Meta in
 /-- Read the selected substitution model from the goal, unfolding only its outer definition
 until `SubstitutesWithin` is exposed. This does not search for a security model. -/
 partial def ccSubstitutionModel (target : Expr) : MetaM Expr := do
-  let target ← instantiateMVars target
+  -- `have` can wrap the goal in `noImplicitLambda` metadata, hiding its head constant.
+  let target := (← instantiateMVars target).consumeMData
   if target.getAppFn.isConstOf
       ``ConstructiveCryptography.CryptographicAlgebra.DistinguisherAdvantage.SubstitutesWithin then
     return target.getAppArgs[3]!

src/Tests.lean

@@ -48,6 +48,7 @@ public import Tests.DSL.ParallelOutside
 public import Tests.DSL.ProbabilityNotation
 public import Tests.DSL.Semantics
 public import Tests.FreshReplyTransform
+public import Tests.NamedAssemblyContracts
 public import Tests.NormalizedProbability
 public import Tests.ProbabilityNotation
 public import Tests.ProbabilityTablePatterns

src/Tests/NamedAssemblyContracts.lean

@@ -0,0 +1,105 @@
+module
+
+public import Commons.Definitions.ReplyTransform
+public import ConstructiveCryptography.Tactics.Substitution
+
+/-!
+# Contracts through named assemblies
+
+Client definitions name a source and its reply transformation. Ordinary rewriting applies the
+public contracts after opening those definitions, including under an arbitrary outer attachment.
+Scalar allowances become constant per-port functions; incompatible allowances and domains fail.
+The selected-test transport uses `d.absorb α` directly and requires explicit admission closure.
+-/
+
+@[expose] public section
+
+namespace Tests.NamedAssemblyContracts
+
+open Commons Commons.Evaluation ConstructiveCryptography SystemAlgebra Probability.Distribution
+open scoped ENNReal
+
+-- `S` carries finite nonempty seeds; `X`, `Y` carry finite replies.
+variable {S X Y : Type} [Fintype S] [Nonempty S] [Fintype X] [Fintype Y]
+
+/-- The evaluation interface returning `X` on at most `q` triggers. -/
+abbrev samples (X : Type) [Fintype X] (q : ℕ) : Interface :=
+  Evaluation.perPort Unit X (fun _ => q)
+
+/-- Each trigger returns `F s` for an independent uniform seed `s : S`. -/
+noncomputable def generated (F : S → X) (q : ℕ) : TypedSystem (samples X q) :=
+  MemorylessSource.perPort X ((𝒰[S]).map F) (budget := fun _ => q)
+
+/-- Attach the reusable reply map `f` to the named fresh-seed source. -/
+noncomputable def mapped (f : X → Y) (F : S → X) (q : ℕ) : TypedSystem (samples Y q) :=
+  mapReplies f (fun _ => q) • generated F q
+
+/-- A named assembly rewrites under an arbitrary outer converter without interface casts. -/
+lemma mapped_in_context
+    -- `C` is the outer interface; `α` encloses the mapped source with allowance `q`.
+    {C : Interface} (q : ℕ) (α : TypedConverter C (samples Y q))
+    -- `F` computes a source reply and `f` transforms it.
+    (F : S → X) (f : X → Y) :
+    α • mapped f F q = α • generated (f ∘ F) q := by
+  unfold mapped generated
+  rw [mapReplies_smul_memorylessSource, ProbDist.map_map]
+
+/-- Each trigger draws `b` independently of the source seed `s`, then returns `g (f b (F s))`.
+The outer map `g` is deterministic. -/
+example (q : ℕ) (F : S → X) (f : Bool → X → Y) (g : Y → X) :
+    mapReplies g (fun _ => q) •
+        (sampleReplies 𝒰[Bool] f (fun _ => q) • generated F q) =
+      MemorylessSource.perPort X
+        (((prodProbDist 𝒰[Bool] ((𝒰[S]).map F)).map (fun bx => f bx.1 bx.2)).map g)
+        (budget := fun _ => q) := by
+  unfold generated
+  rw [sampleReplies_smul_memorylessSource, mapReplies_smul_memorylessSource]
+
+-- An extra outside call cannot be hidden by an interface alias.
+example (_q : ℕ) (_f : X → Y) : True := by
+  fail_if_success
+    have bad : TypedConverter (samples Y (_q + 1)) (samples X _q) :=
+      mapReplies _f (fun _ => _q)
+  trivial
+
+-- A resource restricted to no admitted histories cannot fill an unrestricted inside interface.
+example (q : ℕ) (_f : X → Y)
+    (_R : TypedSystem (Interface.restrict (samples X q) (fun _ => False)
+      (fun _ _ _ h => h))) : True := by
+  fail_if_success
+    have bad : TypedSystem (samples Y q) := mapReplies _f (fun _ => q) • _R
+  trivial
+
+/-- Typed test absorption is the public loss expression; admission closure remains explicit. -/
+example [AdmissibleDistinguishers Interface TypedDistinguisher]
+    -- `α` exposes `A` while using the systems on `B`.
+    {A B : Interface} (α : TypedConverter A B)
+    -- `closed` preserves the selected test class through this particular converter.
+    (closed : AdmissibleDistinguishers.ClosedUnder
+      (Phi := TypedSystem) (D := TypedDistinguisher) α)
+    -- `h` bounds the inside comparison by `ε`, evaluated at each admitted inside test.
+    {R T : TypedSystem B} {ε : TypedDistinguisher B → ℝ≥0∞} (h : R ≃[ε] T) :
+    α • R ≃[fun d => ε (d.absorb α)] α • T :=
+  TypedConverter.substitutesWithin_attach α closed h
+
+/-- `cc_calc quantitative` reads an annotated goal and chains sources with error `ε + δ`. -/
+example
+    [AdmissibleDistinguishers Interface TypedDistinguisher]
+    -- `F`, `G`, `H : S → X` are the maps; `generated F q` uses fresh seeds for `q` calls.
+    (F G H : S → X) (q : ℕ)
+    -- `ε`, `δ` give each comparison's error at a test of `samples X q`.
+    (ε δ : TypedDistinguisher (samples X q) → ℝ≥0∞)
+    -- `first`, `second` bound the adjacent comparisons by those errors.
+    (first : generated F q ≃[ε] generated G q)
+    (second : generated G q ≃[δ] generated H q) :
+    generated F q ≃[fun d => ε d + δ d] generated H q := by
+  -- `have` annotates the goal; `cc_calc` reads the model beneath that annotation.
+  have firstStep := first
+  cc_calc quantitative
+    generated F q ≃[ε] generated G q := firstStep
+    _ ≃[δ] generated H q := second
+
+#print axioms mapped_in_context
+#print axioms TypedConverter.substitutesWithin_attach
+
+end Tests.NamedAssemblyContracts