refactor(Crypto): replace projection chains across Pseudoentropy, Stretch, and DDH modules (#1764)

Complexity/Crypto/Computational/DiffieHellman/MultiDDH.lean

@@ -287,10 +287,10 @@ theorem advantage_multiDDH_le (d : F.Desc) (ι : Type*) [Fintype ι] [DecidableE
       ((PMF.uniformOfFintype (ZMod (F.order d))).bind fun α =>
         (F.multiDDHIdealTupleLaw d ι).bind (test (α • F.generator d))) ≤
     Game.advantage
-      ((F.ddhRealTupleLaw d).bind fun t =>
-        (F.multiDDHRerandomizeLaw d ι t.1 t.2.1 t.2.2).bind (test t.1))
-      ((F.ddhIdealTupleLaw d).bind fun t =>
-        (F.multiDDHRerandomizeLaw d ι t.1 t.2.1 t.2.2).bind (test t.1)) +
+      ((F.ddhRealTupleLaw d).bind fun (u, v, w) =>
+        (F.multiDDHRerandomizeLaw d ι u v w).bind (test u))
+      ((F.ddhIdealTupleLaw d).bind fun (u, v, w) =>
+        (F.multiDDHRerandomizeLaw d ι u v w).bind (test u)) +
       (F.order d : ℝ≥0)⁻¹ := by
   have hreal :
       ((F.ddhRealTupleLaw d).bind fun t =>

Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean

@@ -51,55 +51,75 @@ open Turing.MultiTapeTM
 
 namespace SchnorrGroup
 
+/-- The prime modulus `p` of a raw Schnorr-group description `(p, q, g)`. -/
+abbrev rawModulus (d : ℕ × ℕ × ℕ) : ℕ := d.1
+
+/-- The prime subgroup order `q` of a raw Schnorr-group description `(p, q, g)`. -/
+abbrev rawOrder (d : ℕ × ℕ × ℕ) : ℕ := d.2.1
+
+/-- The subgroup generator residue `g` of a raw Schnorr-group description `(p, q, g)`. -/
+abbrev rawGeneratorResidue (d : ℕ × ℕ × ℕ) : ℕ := d.2.2
+
 /-- A valid description `(p, q, g)` of a Schnorr group: `p` and `q` are prime, and the residue
 `g` satisfies `1 < g < p` and `g ^ q ≡ 1 (mod p)`. -/
 structure Valid (d : ℕ × ℕ × ℕ) : Prop where
   /-- The modulus is prime. -/
-  prime_modulus : d.1.Prime
+  prime_modulus : (rawModulus d).Prime
   /-- The group order is prime. -/
-  prime_order : d.2.1.Prime
+  prime_order : (rawOrder d).Prime
   /-- The generator is not `0` or `1`. -/
-  one_lt_generator : 1 < d.2.2
+  one_lt_generator : 1 < rawGeneratorResidue d
   /-- The generator is a reduced residue. -/
-  generator_lt : d.2.2 < d.1
+  generator_lt : rawGeneratorResidue d < rawModulus d
   /-- The generator has order dividing `q`. -/
-  generator_pow : d.2.2 ^ d.2.1 % d.1 = 1
+  generator_pow : rawGeneratorResidue d ^ rawOrder d % rawModulus d = 1
 
 /-- Valid Schnorr-group descriptions. -/
 abbrev Desc : Type := {d : ℕ × ℕ × ℕ // Valid d}
 
+/-- The prime modulus `p` of a valid Schnorr-group description `(p, q, g)`. -/
+abbrev Desc.modulus (d : Desc) : ℕ := rawModulus d.val
+
+/-- The prime subgroup order `q` of a valid Schnorr-group description `(p, q, g)`. -/
+abbrev Desc.order (d : Desc) : ℕ := rawOrder d.val
+
+/-- The subgroup generator residue `g` of a valid Schnorr-group description `(p, q, g)`. -/
+abbrev Desc.generatorResidue (d : Desc) : ℕ := rawGeneratorResidue d.val
+
 /-- The generator as a unit modulo `p`. -/
-def generatorUnit (d : Desc) : (ZMod d.1.1)ˣ :=
-  ZMod.unitOfCoprime d.1.2.2 ((Nat.coprime_comm.mp ((d.2.prime_modulus.coprime_iff_not_dvd).mpr
-    (Nat.not_dvd_of_pos_of_lt (by have := d.2.one_lt_generator; lia) d.2.generator_lt))))
+def generatorUnit (d : Desc) : (ZMod d.modulus)ˣ :=
+  ZMod.unitOfCoprime d.generatorResidue ((Nat.coprime_comm.mp
+    ((d.2.prime_modulus.coprime_iff_not_dvd).mpr
+      (Nat.not_dvd_of_pos_of_lt (by have := d.2.one_lt_generator; lia) d.2.generator_lt))))
 
 /-- The Schnorr group of a description, written additively. -/
 abbrev Carrier (d : Desc) : Type := Additive (Subgroup.zpowers (generatorUnit d))
 
-instance (d : Desc) : Fact d.1.2.1.Prime := ⟨d.2.prime_order⟩
+instance (d : Desc) : Fact d.order.Prime := ⟨d.2.prime_order⟩
 
 /-- The generator has order dividing `q`. -/
-theorem generatorUnit_pow_order (d : Desc) : generatorUnit d ^ d.1.2.1 = 1 := by
+theorem generatorUnit_pow_order (d : Desc) : generatorUnit d ^ d.order = 1 := by
   ext
   rw [Units.val_pow_eq_pow_val, generatorUnit, ZMod.coe_unitOfCoprime, Units.val_one,
     ← Nat.cast_pow, ← ZMod.natCast_mod, d.2.generator_pow, Nat.cast_one]
 
 /-- Every element of the Schnorr group has order dividing `q`. -/
-theorem pow_order (d : Desc) (x : Subgroup.zpowers (generatorUnit d)) : x ^ d.1.2.1 = 1 := by
+theorem pow_order (d : Desc) (x : Subgroup.zpowers (generatorUnit d)) :
+    x ^ d.order = 1 := by
   obtain ⟨k, hk⟩ := Subgroup.mem_zpowers_iff.mp x.2
   ext
   rw [Subgroup.coe_pow, ← hk, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast,
     generatorUnit_pow_order, one_zpow, Subgroup.coe_one]
 
-instance (d : Desc) : Module (ZMod d.1.2.1) (Carrier d) :=
+instance (d : Desc) : Module (ZMod d.order) (Carrier d) :=
   AddCommMonoid.zmodModule fun x => Additive.toMul.injective (by
     rw [toMul_nsmul, pow_order, toMul_zero])
 
-instance (d : Desc) : NeZero d.1.1 := ⟨d.2.prime_modulus.ne_zero⟩
+instance (d : Desc) : NeZero d.modulus := ⟨d.2.prime_modulus.ne_zero⟩
 
 /-- The generator is not the identity. -/
 theorem generatorUnit_ne_one (d : Desc) : generatorUnit d ≠ 1 := fun h => by
-  have hval := congrArg (fun u : (ZMod d.1.1)ˣ => (u : ZMod d.1.1).val) h
+  have hval := congrArg (fun u : (ZMod d.modulus)ˣ => (u : ZMod d.modulus).val) h
   simp only [generatorUnit, ZMod.coe_unitOfCoprime, ZMod.val_natCast,
     Nat.mod_eq_of_lt d.2.generator_lt, Units.val_one,
     ZMod.val_one_eq_one_mod, Nat.mod_eq_of_lt d.2.prime_modulus.one_lt] at hval
@@ -110,19 +130,19 @@ def generator (d : Desc) : Carrier d :=
   Additive.ofMul ⟨generatorUnit d, Subgroup.mem_zpowers _⟩
 
 /-- The Schnorr group has `q` elements. -/
-theorem card_carrier (d : Desc) : Nat.card (Carrier d) = d.1.2.1 := by
+theorem card_carrier (d : Desc) : Nat.card (Carrier d) = d.order := by
   change Nat.card (Subgroup.zpowers (generatorUnit d)) = d.1.2.1
   rw [Nat.card_zpowers, orderOf_eq_prime (generatorUnit_pow_order d) (generatorUnit_ne_one d)]
 
 /-- The generator is not the identity of the Schnorr group. -/
 theorem generator_ne_zero (d : Desc) : generator d ≠ 0 := fun h =>
   generatorUnit_ne_one d (congrArg (fun x : Carrier d => ((Additive.toMul x :
-    Subgroup.zpowers (generatorUnit d)) : (ZMod d.1.1)ˣ)) h)
+    Subgroup.zpowers (generatorUnit d)) : (ZMod d.modulus)ˣ)) h)
 
 /-- Elements are encoded by the binary digits of their residues modulo `p`. -/
 def encode (d : Desc) (x : Carrier d) : List Bool :=
-  ((((Additive.toMul x : Subgroup.zpowers (generatorUnit d)) : (ZMod d.1.1)ˣ) :
-    ZMod d.1.1).val).bits
+  ((((Additive.toMul x : Subgroup.zpowers (generatorUnit d)) : (ZMod d.modulus)ˣ) :
+    ZMod d.modulus).val).bits
 
 /-- Distinct elements have distinct encodings. -/
 theorem encode_injective (d : Desc) : Function.Injective (encode d) := fun _ _ h =>
@@ -134,7 +154,7 @@ private theorem ofBits_bits (n : ℕ) : ofBits n.bits = n := Nat.foldr_bit_bits
 
 /-- Multiplication modulo `p` of encoded residues. -/
 def add (input : Desc × List Bool × List Bool) : List Bool :=
-  (ofBits input.2.1 * ofBits input.2.2 % input.1.1.1).bits
+  (ofBits input.2.1 * ofBits input.2.2 % input.1.modulus).bits
 
 /-- `add` multiplies encoded group elements. -/
 theorem add_encode (d : Desc) (x y : Carrier d) :
@@ -143,17 +163,17 @@ theorem add_encode (d : Desc) (x y : Carrier d) :
 
 /-- Exponentiation modulo `p` of an encoded residue. -/
 def smul (input : Desc × ℕ × List Bool) : List Bool :=
-  (ofBits input.2.2 ^ input.2.1 % input.1.1.1).bits
+  (ofBits input.2.2 ^ input.2.1 % input.1.modulus).bits
 
 /-- `smul` raises encoded group elements to natural powers. -/
 theorem smul_encode (d : Desc) (a : ℕ) (x : Carrier d) :
-    smul (d, a, encode d x) = encode d ((a : ZMod d.1.2.1) • x) := by
+    smul (d, a, encode d x) = encode d ((a : ZMod d.order) • x) := by
   rw [Nat.cast_smul_eq_nsmul]
   simp only [smul, encode, ofBits_bits, toMul_nsmul, Subgroup.coe_pow, Units.val_pow_eq_pow_val]
   rw [← ZMod.val_natCast, Nat.cast_pow, ZMod.natCast_zmod_val]
 
 /-- The encoded generator is the binary digits of `g`. -/
-theorem encode_generator (d : Desc) : encode d (generator d) = d.1.2.2.bits := by
+theorem encode_generator (d : Desc) : encode d (generator d) = d.generatorResidue.bits := by
   change (((generatorUnit d : (ZMod d.1.1)ˣ) : ZMod d.1.1).val).bits = _
   rw [generatorUnit, ZMod.coe_unitOfCoprime, ZMod.val_natCast,
     Nat.mod_eq_of_lt d.2.generator_lt]
@@ -170,22 +190,23 @@ private theorem computableInPolyTime_val :
 
 /-- The group order is computable in polynomial time from the description. -/
 theorem computableInPolyTime_order :
-    ComputableInPolyTime (fun d : Desc => d.1.2.1) encDesc encNat := by
+    ComputableInPolyTime Desc.order encDesc encNat := by
   have := computableInPolyTime_val
+  unfold Desc.order rawOrder
   fun_prop
 
 /-- The encoded generator is computable in polynomial time from the description. -/
 theorem computableInPolyTime_generator :
     ComputableInPolyTime (fun d => encode d (generator d)) encDesc encBits := by
   have := computableInPolyTime_val
-  simp only [encode_generator]
+  simp only [encode_generator, Desc.generatorResidue, rawGeneratorResidue]
   fun_prop
 
 /-- Multiplication modulo `p` is computable in polynomial time. -/
 theorem computableInPolyTime_add :
     ComputableInPolyTime add (encPair encDesc (encPair encBits encBits)) encBits := by
   have := computableInPolyTime_val
-  unfold add
+  unfold add Desc.modulus rawModulus
   fun_prop
 
 /-- Exponentiation modulo `p` is computable in polynomial time, by square-and-multiply. -/
@@ -197,7 +218,7 @@ theorem computableInPolyTime_smul :
       (encPair encDesc (encPair encNat encBits)) encNat :=
     ComputableInPolyTime.binary_powMod (by fun_prop) (by fun_prop) (by fun_prop)
       fun input => input.1.2.prime_modulus.pos
-  unfold smul
+  unfold smul Desc.modulus rawModulus
   fun_prop
 
 end SchnorrGroup
@@ -208,7 +229,7 @@ of prime order with efficient operations. -/
 def schnorrGroups : PrimeOrderGroupFamily where
   Desc := SchnorrGroup.Desc
   encDesc := SchnorrGroup.encDesc
-  order d := d.1.2.1
+  order := Desc.order
   prime_order d := d.2.prime_order
   Carrier := Carrier
   generator := generator

Complexity/Crypto/Computational/GeneratorXor.lean

@@ -257,7 +257,7 @@ theorem indistinguishable {generator : ℕ → ℕ → List Bool → List Bool}
     (hchoose : ∀ᶠ n in Filter.atTop, choose n < count n)
     (hsecure : ∀ adversary : ℕ → ℕ → List Bool → ProbComp Bool,
       IsPPTOn (encPair (encPair encUnary encUnary) encBits)
-        encBool (fun input => adversary input.1.1 input.1.2 input.2) →
+        encBool (fun ((n, i), word) => adversary n i word) →
       Negligible (fun n => Game.advantage
         (((uniformList (seedBits n)).map (generator n (choose n))).bind
           (fun word => ProbComp.eval (adversary n (choose n) word)))

Complexity/Crypto/Computational/NaorReingold.lean

@@ -602,8 +602,9 @@ rerandomize it into a `BitString k`-indexed family via `multiDDHRerandomizeLaw`
 noncomputable def naorReingoldLevelDDHDistinguisher (d : F.Desc) {n : ℕ} (k : ℕ) (hk : k < n)
     (adv : OracleComp (fun _ : BitString n => F.Carrier d) Bool)
     (t : F.Carrier d × F.Carrier d × F.Carrier d) : PMF Bool :=
-  (F.multiDDHRerandomizeLaw d (BitString k) t.1 t.2.1 t.2.2).bind
-    (F.naorReingoldLevelTest d k hk adv t.1)
+  let (u, v, w) := t
+  (F.multiDDHRerandomizeLaw d (BitString k) u v w).bind
+    (F.naorReingoldLevelTest d k hk adv u)
 
 /-- Under `multiDDHRealTupleLaw`, `naorReingoldLevelTest` reproduces `naorReingoldHybridGame` at
 depth `k`. -/

Complexity/Crypto/Computational/NaorReingold/Security.lean

@@ -467,12 +467,13 @@ noncomputable def naorReingoldToDDHDistinguisher (inLen : ℕ → ℕ)
   let m := inLen n
   let k ← ProbComp.sampleDyadicIndex m
   if k < m then do
-    let αs ← OracleComp.replicate (m - (k + 1)) (F.sampleNaorReingoldExp n input.1)
+    let (d, u, v, w) := input
+    let αs ← OracleComp.replicate (m - (k + 1)) (F.sampleNaorReingoldExp n d)
     Prod.fst <$> (OracleComp.interpret
       (OracleComp.sumHandler (fun r => StateT.lift (ProbComp.unifFin r))
-        (fun request => F.naorReingoldFrontierOracle n m k input.1
-          input.2.1 input.2.2.1 input.2.2.2 αs request.2))
-      (adversary n (F.encDesc input.1))).run []
+        (fun request => F.naorReingoldFrontierOracle n m k d
+          u v w αs request.2))
+      (adversary n (F.encDesc d))).run []
   else pure false
 
 private theorem isPPTOn_sampleNaorReingoldPair (F : PrimeOrderGroupFamily)

Complexity/Crypto/Computational/OneWay/NP.lean

@@ -80,7 +80,13 @@ open Complexity Probability Turing.MultiTapeTM ComputableTidilyInPolyTime
 /-- **The preimage-prefix problem** of `f`: the instances `(n, y, u)` such that some input `x` of
 length `n` that starts with `u` satisfies `f x = y`. -/
 def preimagePrefix (f : List Bool → List Bool) : Set (ℕ × List Bool × List Bool) :=
-  {p | ∃ x : List Bool, x.length = p.1 ∧ p.2.2 <+: x ∧ f x = p.2.1}
+  {(n, y, u) : ℕ × List Bool × List Bool | ∃ x : List Bool, x.length = n ∧ u <+: x ∧ f x = y}
+
+/-- Membership in `preimagePrefix f`: `(n, y, u) ∈ preimagePrefix f` iff `y` has an `n`-bit
+preimage under `f` with prefix `u`. -/
+@[simp] theorem mem_preimagePrefix {f : List Bool → List Bool} {n : ℕ} {y u : List Bool} :
+    (n, y, u) ∈ preimagePrefix f ↔ ∃ x : List Bool, x.length = n ∧ u <+: x ∧ f x = y := by
+  simp [preimagePrefix]
 
 /-- The encoding of instances of the preimage-prefix problem: the length `n` in unary, then the
 image and the prefix. -/
@@ -95,7 +101,8 @@ variable {f : List Bool → List Bool}
 prefix. -/
 def preimagePrefixVerifier (f : List Bool → List Bool)
     (p : (ℕ × List Bool × List Bool) × List Bool) : Bool :=
-  decide (p.1.2.2.length ≤ p.1.1) && f (p.1.2.2 ++ p.2.take (p.1.1 - p.1.2.2.length)) == p.1.2.1
+  let ((n, y, u), rest) := p
+  decide (u.length ≤ n) && f (u ++ rest.take (n - u.length)) == y
 
 /-- The unary length is at most as long as the encoded instance. -/
 private theorem le_length_encPreimagePrefix (p : ℕ × List Bool × List Bool) :
@@ -107,14 +114,15 @@ private theorem le_length_encPreimagePrefix (p : ℕ × List Bool × List Bool)
 members. -/
 theorem isVerifier_preimagePrefixVerifier (f : List Bool → List Bool) :
     IsVerifier encPreimagePrefix Polynomial.X (preimagePrefixVerifier f) (preimagePrefix f) := by
-  refine IsVerifier.of_padding (fun ⟨n, y, u⟩ w hw h => ?_) fun ⟨n, y, u⟩ ⟨x, hx, hux, hfx⟩ => ?_
+  refine IsVerifier.of_padding (fun ⟨n, y, u⟩ w hw h => ?_) fun ⟨n, y, u⟩ hmem => ?_
   · rw [Polynomial.eval_X] at hw
     have hn := le_length_encPreimagePrefix (n, y, u)
     simp only [preimagePrefixVerifier, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq] at h
+    rw [mem_preimagePrefix]
     refine ⟨u ++ w.take (n - u.length), ?_, List.prefix_append _ _, h.2⟩
     simp only [List.length_append, List.length_take] at hw ⊢
     omega
-  · obtain ⟨v, rfl⟩ := hux
+  · obtain ⟨x, hx, ⟨v, rfl⟩, hfx⟩ := mem_preimagePrefix.mp hmem
     have hn := le_length_encPreimagePrefix (n, y, u)
     simp only [List.length_append] at hx
     refine ⟨v, ?_, fun k => ?_⟩
@@ -131,7 +139,11 @@ theorem computableInPolyTime_preimagePrefixVerifier
     (hf : ComputableInPolyTime f encBits encBits) :
     ComputableInPolyTime (preimagePrefixVerifier f) (encPair encPreimagePrefix encBits)
       encBool := by
-  unfold preimagePrefixVerifier
+  change ComputableInPolyTime
+    (fun p : (ℕ × List Bool × List Bool) × List Bool =>
+      decide (p.1.2.2.length ≤ p.1.1) &&
+        f (p.1.2.2 ++ p.2.take (p.1.1 - p.1.2.2.length)) == p.1.2.1)
+    (encPair encPreimagePrefix encBits) encBool
   fun_prop
 
 /-- **The preimage-prefix problem is in `NP`** for every function computable in polynomial
@@ -171,15 +183,15 @@ theorem preimageSearchStep_mem {D : ℕ × List Bool × List Bool → Bool}
     (n, y, preimageSearchStep D (n, y) u) ∈ preimagePrefix f := by
   rw [preimageSearchStep]
   cases hb : D (n, y, u ++ [false])
-  · obtain ⟨x, hx, ⟨v, rfl⟩, hfx⟩ := hu
+  · obtain ⟨x, hx, ⟨v, rfl⟩, hfx⟩ := mem_preimagePrefix.mp hu
     simp only [List.length_append] at hx
     obtain ⟨b, v, rfl⟩ : ∃ b v', v = b :: v' := List.exists_cons_of_length_pos (by omega)
     cases b
     · have hmem : (n, y, u ++ [false]) ∈ preimagePrefix f :=
-        ⟨u ++ false :: v, by simpa using hx, ⟨v, by simp⟩, hfx⟩
+        mem_preimagePrefix.mpr ⟨u ++ false :: v, by simpa using hx, ⟨v, by simp⟩, hfx⟩
       rw [hD, hb] at hmem
       exact absurd hmem Bool.false_ne_true
-    · exact ⟨u ++ true :: v, by simpa using hx, ⟨v, by simp⟩, hfx⟩
+    · exact mem_preimagePrefix.mpr ⟨u ++ true :: v, by simpa using hx, ⟨v, by simp⟩, hfx⟩
   · exact (hD _).2 hb
 
 /-- **Search to decision.** With a decision procedure for the preimage-prefix problem, the search
@@ -191,14 +203,13 @@ theorem apply_preimageSearch {D : ℕ × List Bool × List Bool → Bool}
       (x.length, f x, (preimageSearchStep D (x.length, f x))^[i] []) ∈ preimagePrefix f := by
     intro i hi
     induction i with
-    | zero => exact ⟨x, rfl, List.nil_prefix, rfl⟩
+    | zero => exact mem_preimagePrefix.mpr ⟨x, rfl, List.nil_prefix, rfl⟩
     | succ i ih =>
       rw [Function.iterate_succ_apply']
       exact preimageSearchStep_mem hD (ih (by omega))
         (by rw [length_iterate_preimageSearchStep]; omega)
-  obtain ⟨x', hx', hpre, hfx'⟩ := hmem x.length le_rfl
+  obtain ⟨x', hx', hpre, hfx'⟩ := mem_preimagePrefix.mp (hmem x.length le_rfl)
   have heq := hpre.eq_of_length (by rw [length_iterate_preimageSearchStep]; exact hx'.symm)
-  dsimp only at heq hfx'
   change f ((preimageSearchStep D (x.length, f x))^[x.length] []) = f x
   rw [heq]
   exact hfx'

Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean

@@ -63,7 +63,7 @@ theorem HasGap.eventually_exists_indexed_mask {pair : SamplablePair} {gap : ℕ
     (hpair : pair.HasGap gap) (test : ℕ → ℕ → List (List Bool × Bool) → ProbComp Bool)
     (htest : IsPPTOn (encPair (encPair encUnary encUnary)
       (encList (encPair encBits encBool))) encBool
-        (fun input => test input.1.1 input.1.2 input.2))
+        (fun ((n, i), samples) => test n i samples))
     {candidates count densityBound inverseGap : ℕ → ℕ} {numerator : ℕ → ℕ → ℕ}
     (hcandidates : ComputableInPolyTime candidates encUnary encUnary)
     (hcount : ComputableInPolyTime count encUnary encUnary)

Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean

@@ -154,9 +154,10 @@ theorem computableInPolyTime_wordObservation {α : Type} {encode : α ↪ List B
 /-- Encode a finite public observation using the chosen image representation. -/
 def encodeObservation {n count : ℕ} {Image : Type*} (encodeImage : Image → List Bool)
     (observation : Observation n count Image) : List Bool :=
-  wordObservation (encodeImage observation.2.2.1) observation.1.val
-    (List.ofFn observation.2.1.1) (List.ofFn observation.2.2.2)
-    (List.ofFn observation.2.1.2)
+  let ⟨pos, (matrix, query), image, digest⟩ := observation
+  wordObservation (encodeImage image) pos.val
+    (List.ofFn matrix) (List.ofFn digest)
+    (List.ofFn query)
 
 /-- Encoding loses none of the public information, even though the digest's width varies. -/
 theorem encodeObservation_injective {n count : ℕ} {Image : Type*}