Add modular-arithmetic types to Geb external API

[rokopt]

The substobj and substmorph types in https://github.com/anoma/geb/blob/main/src/specs/geb.lisp should be extended with those required for built-in modular arithmetic.

Specifically, there will be a new object called something like fs n for each non-zero natural n (not for zero, because arithmetic mod 0 is Nat itself, and circuits can only support fixed-size natural numbers).

There will be the following new morphisms with the following signatures, where bool is coprod so1 so1, and fs <n> means for every non-zero natural number <n>:

• For each natural number m including zero and less than n, const m : so1 -> fs n
• inj : fs m -> fs n (injects one bounded type into another -- may wrap around if m > n; equal to id if m == n)
• + : prod (fs m) (fs n) -> fs p
• * : prod (fs m) (fs n) -> fs p
• - : prod (fs m) (fs n) -> fs p
• / : prod (fs m) (fs n) -> fs p
• % : prod (fs m) (fs n) -> fs p
• == : prod (fs m) (fs n) -> bool
• < : prod (fs m) (fs n) -> bool

Because the arithmetic is modular, overflows just cause wraparound. Division and modulus by zero will produce errors at witness generation time in VampIR. (Once we support dependent types in Geb, we will be able to allow users to include proof content demonstrating that they are not dividing by zero.)

VampIR higher-order functions might be helpful in integrating this with #60 ; see https://github.com/anoma/vamp-ir/blob/main/tests/funcs.pir for examples.

[rokopt]

+ : prod (fs m) (fs n) -> fs p

It occurs to me regarding these variable-type-size interfaces that they could be constructed from single-type-size interfaces such as + : prod (fs n) (fs n) -> fs n together with appropriate uses of inj, and given that that's possible I think that that is how we should do it, as it's usually best to construct more complex things out of simpler things when possible, inj shouldn't add any circuitry as it's just a cast, and that would make it very clear where any mods were happening, which might not be so clear if the arithmetic interfaces used types of different sizes.

[rokopt]

A question for @lukaszcz : does Juvix (currently, at least) use natural-number types that aren't of 2^n size, or for at least the initial implementations of these interfaces, would it suffice if the arithmetic operations all used types of natural numbers of 2^n size (precisely n bits for some n)?

[lukaszcz]

We currently use theoretically unbounded numbers, but having fixed 2^n sizes should be fine. We haven't completely decided yet what number types we should support, but if the size is fixed then it makes sense for it to be a power of two.

We might also want to have direct access to the actual fields elements with their corresponding operations (e.g. where division is actual field division not integer division). That would be a separate Field type.

[rokopt]

We might also want to have direct access to the actual fields elements with their corresponding operations (e.g. where division is actual field division not integer division). That would be a separate Field type.

Good point -- I filed #122 for this.