feat: add example from paper for FHE.

[bollu]

To make this example work, we need a definition of R.ofZ that is computable, and which is not agressively unfolded. This is ensured by our axiom trick.

Code peeled from pre-paper submission PR: #196.
Code stacked on: #234

---

Closes #196 (This PR fully integrates the features of #196 into main.)

[alexkeizer]

To clarify: the axiom trick is needed because of the reduction we do in the fhe_com elaborator?

[bollu]

@alexkeizer that's right.

[bollu]

@alexkeizer actually, on second thought, I think there are two places we agressively reduce: one is in simp_peephole/change_mlir_context, and one is at the fhe_com. I think it's the aggressiveness of simp_peephole / change_mlir_context that used to cause stuff to explode.

[bollu]

@alexkeizer My hope is that the example is self-contained enough for someone (nudge nudge @tobiasgrosser ) to investigate if it's possible to eliminate the need for the axiom.

[alexkeizer]

Good to know: we could (should) change change_mlir_context to only reduce to a sort of transitive whnf, where it is of the form _ :: _ :: ... :: [] (with the cons being made explicit), but the elements don't have to be reduced. That would solve your issue as well, then?

[bollu]

@alexkeizer that might, but I would not take my word for it. I'd have to play with the example again to remember precisely what caused me to need an axiom instead of just an implemented_by.

[alexkeizer]

I'd like to give it a try: reducing less aggressively seems like a win regardless of if it fixes this exact issue.

EDIT: I've attempted my suggestion in #238, but it does not seem to solve all of the problems here.
I suspect we do have to make the fhe_com less aggressively as well, which is a bit more involved.
I'll make a note of this in #232, but won't block the current PR any more on this

[alexkeizer]

I'd say this is fine to merge after you've addressed my (minor) comments