Exact binary projection for the full-register auxiliary checks

def MIPRE.Introspection.AuxiliaryProgram.firstEmbedding {s Q : ℕ} (h : s ≤ Q) : Fin s ↪ Fin Q

Equations

• MIPRE.Introspection.AuxiliaryProgram.firstEmbedding h = { toFun := Fin.castLE h, inj' := ⋯ }

theorem MIPRE.Introspection.AuxiliaryProgram.ofBits_take_first {s Q : ℕ} (h : s ≤ Q) (z : Fin Q → CL.𝔽₂) : CL.ofBits s (List.take s (CL.toBits z)) = CL.pull (firstEmbedding h) z

theorem MIPRE.Introspection.AuxiliaryProgram.toBits_push_first {s Q : ℕ} (h : s ≤ Q) (x : Fin s → CL.𝔽₂) : CL.toBits (CL.push (firstEmbedding h) x) = CL.toBits x ++ List.replicate (Q - s) false

theorem MIPRE.Introspection.AuxiliaryProgram.source_bits_iff {s Q : ℕ} (h : s ≤ Q) (y : Fin Q → CL.𝔽₂) (x : Fin s → CL.𝔽₂) : SourceCompiler.InSource s (CL.toBits y) ∧ List.take s (CL.toBits y) = CL.toBits x ↔ y = CL.push (firstEmbedding h) x

A full-register output equals a zero-extended source output exactly when its suffix is zero and its retained prefix agrees.