Codify what it means to be a "pure function" in Noir

[iamrecursion]

When proving properties of programs using Lampe we can make stronger statements if we know that a function is pure. That said, we cannot necessarily model Noir's notion of purity with pure functions in lean. To that end, we should state (and prove) a theorem about what it means to be a pure function in (extracted) Noir.