formal circuit language implement in Coq circom like syntax with polynomial lookup support refinement proof between circuit and coq functions.