Feature request: overloading arithmetic

[thoughtpolice]

Hi,

I recently took a stab at implementing RFC 7748 (AKA Curve25519) in Cryptol. It ended up pretty well, but at the end of it all I needed modular arithmetic, so I stole a copy of it from here, based on the Minilock spec, using bv.cry and Arith.cry. With that I fixed up my montgomery ladder and I got it working nicely. (Hilariously it ended up looking very close to the literal-cryptol Minilock version, but is smaller and more direct).

However, I find the code relatively suboptimal, so I was wondering if a feature request to improve it would be considered.

Here's the code for the differential double-and-add ladder from the EFD used in RFC 7748, adapted for Cryptol (technically, this isn't exactly mladd-1987-m I think, due to the final expression, e * (aa + 121665 * e) instead of e * (bb + 121665 * e), so it's some variation)

// monty: core differential double-and-add montgomery ladder
// see 'mladd-1987-m' on the Elliptic Curve Formula Database
//   https://hyperelliptic.org/EFD/g1p/auto-montgom-xz.html
monty : Scalar
     -> Coord
     -> [256]
     -> (Coord, Coord, Coord, Coord)
     -> (Coord, Coord, Coord, Coord)
monty k x1 t (x2, x3, z2, z3) = (rx2, rx3, rz2, rz3)
  where
    // set up the input XZ coordinates for double-and-addition. the
    // montgomery ladder either computes (p + q, 2q) or (2p, q + p),
    // based on whether the bits of the scalar are set to 1 or 0.
    // the first thing we do is check if the bit is set and if so,
    // swap out the value to get the correct result.
    k_t        = (k >> t) && 1
    (x2',x3')  = cswap k_t x2 x3
    (z2',z3')  = cswap k_t z2 z3

    // mladd-1987-m: differential double-and-addition for montgomery
    // curves.
    a    = add prime x2' z2'
    aa   = square prime a
    b    = sub prime x2' z2'
    bb   = square prime b
    e    = sub prime aa bb
    c    = add prime x3' z3'
    d    = sub prime x3' z3'
    da   = mul prime d a
    cb   = mul prime c b
    x3'' = square prime (add prime da cb)
    z3'' = mul prime x1 (square prime (sub prime cb da))
    x2'' = mul prime aa bb
    z2'' = mul prime e (add prime aa (mul prime 121665 e))

    (rx2, rx3) = cswap k_t x2'' x3''
    (rz2, rz3) = cswap k_t z2'' z3''

Recently I took a stab at implementing Curve41417, but using Haskell, not Cryptol. While I was fiddling with the modular arithmetic implementation I ended up using a representation that yielded Twisted Edwards multipliers/adders that came out very elegantly like this:

-- | Strongly unified addition of Curve41417 points.
--
-- Addition algorithm: @add-2007-bl-3@.
(.+) :: Modulo s => Point s -> Point s -> Point s
Point x1 y1 z1 .+ Point x2 y2 z2
  = Point x3 y3 z3
  where
    sqr n = n * n

    a = z1 * z2
    b = sqr a
    c = x1 * x2
    d = y1 * y2
    e = 3617 * c * d
    bb = sqr b
    ee = sqr e
    h = sqr (a + b) - bb
    i = sqr (a + e) - ee

    x3 = (h - i) * ((x1 + y1) * (x2 + y2) - c - d)
    y3 = (h + i - 2*b) * (d - c)
    z3 = 2 * (bb - ee)

-- We also give (.+) a proper fixity level, for completeness.
infixl 6 .+

-- | Explicit doubling of Curve41417 points; note that the unified
-- addition formula may also be used to do doubling (e.g. @add(p,p)@)
--
-- Doubling algorithm: @dbl-2007-bl@.
pointDbl0 :: Modulo s => Point s -> Point s
pointDbl0 (Point x y z) = Point x3 y3 z3
  where
    sqr n = n * n

    b = sqr (x + y)
    c = sqr x
    d = sqr y
    e = c + d
    h = sqr z
    j = e - (2*h)

    x3 = (b - e) * j
    y3 = e * (c - d)
    z3 = e * j

This is actually much nicer, and is a literal direct copy/paste from the EFD into a Haskell file! I just renamed the variables, and it compiled fine.

I was able to do this by simply overloading Num on my own modular number values, and having a Haskell Point simply be a triplet of these modular numbers that you operate over. The way it works in my older code uses the reflection library under the hood (and actually I was using a bad modular arithmetic implementation to get started hilariously -- this just managed to encapsulate all that badness). It's based on the example from the classic "Implicit Configurations" paper.

I'm wondering if anyone has though of exploring this design space in Cryptol 2, since arithmetic is now overloaded on Arith. Essentially, I think there'd mostly need to be a newtype mechanism and a way to instantiate classes? Is that "all" that's missing?

This particular Haskell example is very fancy but only because reflection allows me to propagate the modulus at runtime. This was because I was exploring efficient, reusable ECC components, so reflection made it easier to test this (for example, I could pretty easily reuse those routines with different choices of the Edwards d constant and different prime values for other twisted edwards curves too.)

If I picked the modulus statically at compile time, I could write a much simpler Num instance once and be done with it. For the vast majority of Cryptol code, I'd expect this to be more the case.

You could also do some of this propagation with type variables too, I think. In the event you wanted to parameterize something over a chosen prime:

f : {m, a} (fin a, a >= width m) => [a] -> [a]
f x = x % `(m)

That is, parameterize the modulus as a type variable, and instantiate it concretely to a particular prime value when necessary:

f`{m=(2^^255)-19} reallyBigNum

But this doesn't really fix the overloading part, so much. There's probably some interplay between these two, to fully get what I got out of the Haskell code. e.g. I want a Arith implementation that has a modular implementation for some newtype, but I want to be able to parameterize that choice over the given prime, as well.

Maybe I'm missing something more cleanly doable. Thoughts?

[yav]

Hi Austin,

Cryptol almost has what you are asking for. In particular, there are newtype declarations, although they are a bit secret, mostly because we are not sure if they are a good idea and as a result have fallen a bit in disrepair. For an overview of how they are supposed to work have a look at bug #369.

Cryptol also has support fix infix operators, so you could certainly make you definition look prettier and almost as in the spec by using them. For example you could something like this:

newtype Bellow (m : #) = { value : [64] }

// This could be the implementation of addition modulo `m`.
// Currently, I just return the 3 arguments.
(++) : {m} (fin m, 64 >= width m) => Bellow m -> Bellow m -> ([64],[64],[64])
x ++ y = (x.value, y.value, `m)

As you know, we already have a built-in class for arithmetic too. The main thing that's missing is support for user-defined instances. I doubt that this would be very hard to do, but I am not sure if it is a good idea from a language design perspective. In particular, I think that one can go a long way by just using names and controlling what's in scope where, rather than resorting to using types to resolve overloading, and it's nice if there is one less concept to learn before you can use the language.

So, technically, I think we are quite close, it would just be nice to see what design choices we want to make.

By the way, my example was for situation where you know the modulo statically. If it is going to be a computed run-time value you could simply define the operators you want to use locally:

f m x y = x1 +++ x2
  where
  x1 = x +++ y
  x2 = (y +++ x) *** x
  // etc.

  (+++) = addMod m
  (***) = mulMod m

I had to use the weird operator names due to bug #368, but you should be able to just shadow (+) locally.

[brianhuffman]

Cryptol now has a built-in type of integers mod n (see #510). Does that suffice for this problem, or is there still a need for user-defined Arith instances?

[thoughtpolice]

I'll have to dig up some of my code and build a recent copy of Cryptol -- if this works, it'll be a wonderful addition!

[thoughtpolice]

Just as an update (after a long hiatus), I did actually test this, and it works very nicely -- I can now copy/paste the EFD formulas pretty much directly! The following is a valid program (for some chosen edwards curve parameters a and d):

// curve: twisted edwards -- ax^2 + y^2 = 1 + dx^2y^2
// coordinates: extended homogeneous
//    x  = X / Z
//    y  = Y / Z
//    xy = T / Z

type P = ... // prime P
type Point  = ( Z P, Z P, Z P, Z P )

// point addition
add : Point -> Point -> Point
add (X1, Y1, Z1, T1) (X2, Y2, Z2, T2) = (X3, Y3, Z3, T3)
  where
    // add-2008-hwcd, strongly unified
    // cost: 9M + 1*a + 1*d + 7add -- 9M + 1*a + 6add, dependent upon the first point
    A = X1*X2
    B = Y1*Y2
    C = T1*d*T2
    D = Z1*Z2
    E = (X1+Y1)*(X2+Y2)-A-B
    F = D-C
    G = D+C
    H = B-a*A
    X3 = E*F
    Y3 = G*H
    T3 = E*H
    Z3 = F*G

// (explicit) point doubling
dbl : Point -> Point
dbl (X1, Y1, Z1, T1) = (X3, Y3, Z3, T3)
  where
    // dbl-2008-hwcd
    // cost: 4M + 4S + 1*a + 6add + 1*2
    sqr x = x * x
    A = sqr X1
    B = sqr Y1
    C = 2 * sqr Z1
    D = a * A
    E = (sqr (X1+Y1))-A-B
    G = D+B
    F = G-C
    H = D-B
    X3 = E*F
    Y3 = G*H
    T3 = E*H
    Z3 = F*G

So I think this can reasonably be closed for my use case, actually.