Reduce the use of the fix function in the Cryptol->SAWCore translation

[RyanGlScott]

Currently, all recursive Cryptol functions are translated to SAWCore definitions involving the fix primitive. This poses several issues, including:

1. In general, fix is unsound (see Make summarize_verification report whether definitions depend on unsafe primitives or axioms (e.g., fix) #2088). We should try to minimize uses of fix so that we can reduce the trusted code base.
2. The fix function cannot be translated to Coq, so the less we use fix in the Cryptol->SAWCore translation, the more Cryptol definitions we can port to Coq.

In order to accomplish this, we will need to identify which recursive Cryptol definitions are guaranteed to terminate after a certain number of iterations and translate them to well-founded recursion primitives in SAWCore. For example, one common pattern is the "take a finite number of elements from an infinite stream pattern", e.g.,

foo = take`{5} [0 ...]

While [0 ...] is an infinite sequence (and will never terminate on its own), the overall expression take`{5} [0 ...] does terminate. We should identify this pattern and translate it to a SAWCore term that computes a finite prefix of [0 ...].

[RyanGlScott]

As an intermediate step towards fixing this issue, it would be worth translating each recursive Cryptol definition into its own, bespoke SAWCore fixpoint axiom. For example, we could translate the following Cryptol function:

xs = [True] # xs

Into the SAWCore that looks like the following:

primitive xs : Stream Bool

-- xs == [True] # xs
axiom xs_unfold = Eq (Stream Bool)
                     xs
                     (ecCat (TCNum 1) TCInf Bool True xs)

Where xs_unfold corresponds to the unfold_fix_once proof tactic, but specialized for the definition of xs. This approach would have a couple of advantages:

1. These axioms would become parameters to an exported Coq theory. Because they are specialized to particular definitions, it would be easier to prove their consistency in Coq at that point.
2. When examining whether a proof depends on unsafe parameters or axioms (see Make summarize_verification report whether definitions depend on unsafe primitives or axioms (e.g., fix) #2088), it would be easier to tell at a glance where these axioms arise from as opposed to a general-purpose fix function (which could come from any number of different places).