Closed thoughtpolice closed 5 years ago
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.
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?
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!
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.
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
andArith.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 ofe * (bb + 121665 * e)
, so it's some variation)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:
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 HaskellPoint
simply be a triplet of these modular numbers that you operate over. The way it works in my older code uses thereflection
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, soreflection
made it easier to test this (for example, I could pretty easily reuse those routines with different choices of the Edwardsd
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:
That is, parameterize the modulus as a type variable, and instantiate it concretely to a particular prime value when necessary:
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 somenewtype
, 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?