extendMask

formal source

  29  funext i; simp [restrict, enc]
  30
  31/-- Extend a partial assignment on `M` to a full mask by defaulting to `false` off `M`. -/
  32def extendMask (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) : Fin n → Bool :=
  33  fun i => if h : i ∈ M then a ⟨i, h⟩ else false
  34
  35@[simp] lemma extendMask_in (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) {i : Fin n} (h : i ∈ M) :
  36  extendMask (n:=n) M a i = a ⟨i, h⟩ := by
  37  simp [extendMask, h]
  38
  39@[simp] lemma extendMask_notin (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) {i : Fin n} (h : i ∉ M) :
  40  extendMask (n:=n) M a i = false := by
  41  simp [extendMask, h]
  42
  43@[simp] lemma restrict_extendMask (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) :
  44  restrict (n:=n) (extendMask (n:=n) M a) M = a := by
  45  funext i
  46  simp [restrict, extendMask]
  47
  48/-- Any fixed-view decoder on a set `M` of queried indices can be fooled by a suitable `(b,R)`. -/
  49 theorem adversarial_failure (M : Finset (Fin n))
  50  (g : (({i // i ∈ M} → Bool)) → Bool) :
  51  ∃ (b : Bool) (R : Fin n → Bool),
  52    g (restrict (n:=n) (enc b R) M) ≠ b := by
  53  classical
  54  -- Pick an arbitrary local view `a` and force the decoder to predict `b' := g a`.
  55  let a : {i // i ∈ M} → Bool := fun _ => false
  56  let b' : Bool := g a
  57  -- Choose the true bit to be the opposite of the decoder's prediction.
  58  let b : Bool := ! b'
  59  -- Choose the mask so that the restricted encoding equals `a`.
  60  let R : Fin n → Bool :=
  61    if b then extendMask M (fun i => ! (a i)) else extendMask M a
  62  have hRestr : restrict (n:=n) (enc b R) M = a := by