Open rokopt opened 1 year ago
+ : 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 mod
s were happening, which might not be so clear if the arithmetic interfaces used types of different sizes.
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
)?
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.
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.
The
substobj
andsubstmorph
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 naturaln
(not for zero, because arithmetic mod 0 isNat
itself, and circuits can only support fixed-size natural numbers).There will be the following new morphisms with the following signatures, where
bool
iscoprod so1 so1
, andfs <n>
means for every non-zero natural number<n>
:m
including zero and less thann
,const m
:so1 -> fs n
inj
:fs m -> fs n
(injects one bounded type into another -- may wrap around ifm > n
; equal toid
ifm == 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.