pullback Framework for verified shallow embeddings and specification of proggramming language in Lean4