Finalized random prims and added tests

example/rsa.disco

@@ -18,6 +18,30 @@ decrypt = encrypt
 
 -- takes two primes, returns a pair of pairs containing the RSA public/private keys
 -- prime -> prime -> (public key, private key)
+
+
+-- randKeys takes in a nat (number of digits in the random range) and a 
+-- generator (created using `seed`), and generates two random prime numbers 
+-- in the range and calls getKeys with them
+
+randKeys : N -> Gen -> (N * N) * (N * N)
+randKeys d g = 
+   let   p1 = genPrime (10^d,10^(d+1)) g,
+         p2 = genPrime (10^d,10^(d+1)) (snd p1)
+   in getKeys (fst p1) (fst p2) 
+
+genPrime : (N * N) -> Gen -> (N * Gen)
+genPrime r g = let p = random(r,g) in 
+   {? p                          if isPrime (fst p)
+   ,  genPrime r (snd p)         otherwise
+   ?}
+
+fst : (a * b) -> a 
+fst (a,_) = a 
+
+snd : (a * b) -> b 
+snd (_,b) = b 
+
 getKeys : N -> N -> (N * N) * (N * N)
 getKeys p1 p2 =
   let m = p1 * p2,

src/Disco/Interpret/CESK.hs

@@ -432,9 +432,9 @@ appConst k = \case
   --------------------------------------------------
   -- Randomness
 
-  ORandom ->  arity3 $ \v1 v2 v3 -> 
-    let (a,g') = R.randomR (vint v2,vint v3) (vgen v1) 
-    in out $ VPair (intv a) (genv g')
+  ORandom -> arity2 (\t g -> arity2 (\v1 v2 -> 
+      let (a,g') = R.randomR (vint v1,vint v2) (vgen g)
+      in out $ VPair (intv a) (genv g')) t)
   OSeed -> out . VGen . (R.mkStdGen . fromIntegral . vint) 
   --------------------------------------------------
   -- Graph operations

src/Disco/Parser.hs

@@ -450,6 +450,7 @@ reservedWords =
   , "Set"
   , "Graph"
   , "Map"
+  , "Gen"
   , "N"
   , "Z"
   , "F"
@@ -1212,6 +1213,7 @@ parseAtomicType =
       <|> TyZ <$ (reserved "Integer" <|> reserved "Int" <|> reserved "Z" <|> reserved "ℤ")
       <|> TyF <$ (reserved "Fractional" <|> reserved "Frac" <|> reserved "F" <|> reserved "𝔽")
       <|> TyQ <$ (reserved "Rational" <|> reserved "Q" <|> reserved "ℚ")
+      <|> TyGen <$ reserved "Gen"
       <|> TyCon <$> parseCon <*> (fromMaybe [] <$> optional (parens (parseType `sepBy1` comma)))
       <|> TyVar <$> parseTyVar
       <|> parens parseType

src/Disco/Typecheck.hs

@@ -771,7 +771,7 @@ typecheck Infer (TPrim prim) = do
   ----------------------------------------
   -- Randomness
 
-  inferPrim PrimRandom = return $ TyGen :*: TyN :*: TyN :->: (TyN :*: TyGen)
+  inferPrim PrimRandom = return $ (TyN :*: TyN) :*: TyGen :->: (TyN :*: TyGen)
   inferPrim PrimSeed = return $ TyN :->: TyGen
   ----------------------------------------
   -- Arithmetic

test/prim-random/expected

@@ -0,0 +1,13 @@
+Loading prim-random.disco...
+Loading num.disco...
+Loaded.
+<Gen>
+(3503371672, <Gen>)
+(3503371672, <Gen>)
+(2618153580, <Gen>)
+[1, 8, 27, 64, 125, 216, 343, 512, 729]
+[1, 2, 3, 4, 5, 6, 7, 8, 9]
+[1, 2, 3, 4, 5, 6, 7, 8, 9]
+[1, 8, 27, 64, 125, 216, 343, 512, 729]
+[1, 2, 3, 4, 5, 6, 7, 8, 9]
+[1, 2, 3, 4, 5, 6, 7, 8, 9]

test/prim-random/input

@@ -0,0 +1,14 @@
+:load test/prim-random/prim-random.disco
+
+seed(1000)
+random((1,10000000000),seed(2134))
+random((10000000000,1),seed(2134))
+random((10000000000,1),seed(2135))
+
+encrypt (fst (getKeys 227 971)) [1,2,3,4,5,6,7,8,9]
+decrypt (snd (getKeys 227 971)) [1,8,27,64,125,216,343,512,729]
+decrypt (snd (getKeys 227 971)) (encrypt (fst (getKeys 227 971)) [1,2,3,4,5,6,7,8,9])
+
+encrypt (fst (randKeys 2 (seed 10000))) [1,2,3,4,5,6,7,8,9]
+decrypt (snd (randKeys 2 (seed 10000))) [1,8,27,64,125,216,343,512,729]
+decrypt (snd (randKeys 2 (seed 10000))) (encrypt (fst (randKeys 2 (seed 10000))) [1,2,3,4,5,6,7,8,9])

test/prim-random/prim-random.disco

@@ -0,0 +1,94 @@
+import num
+import list
+
+-- Implementation of RSA encryption algorithm.
+-- Reference: https://simple.wikipedia.org/wiki/RSA_(algorithm)
+
+-- To use, first call `getKeys` with two prime numbers, which returns
+-- two pairs. The first pair is the public key, the second is the
+-- private key. These keys, along with the `encrypt` and `decrypt`
+-- functions can be used to encrypt and decrypt lists of natural
+-- numbers.
+
+encrypt : N * N -> List(N) -> List(N)
+encrypt key xs = each (encrypt1 key, xs)
+
+decrypt : N * N -> List(N) -> List(N)
+decrypt = encrypt
+
+
+-- randKeys takes in a nat (number of digits in the random range) and a 
+-- generator (created using `seed`), and generates two random prime numbers 
+-- in the range and calls getKeys with them
+
+randKeys : N -> Gen -> (N * N) * (N * N)
+randKeys d g = 
+   let   p1 = genPrime (10^d,10^(d+1)) g,
+         p2 = genPrime (10^d,10^(d+1)) (snd p1)
+   in getKeys (fst p1) (fst p2) 
+
+genPrime : (N * N) -> Gen -> (N * Gen)
+genPrime r g = let p = random(r,g) in 
+   {? p                          if isPrime (fst p)
+   ,  genPrime r (snd p)         otherwise
+   ?}
+
+fst : (a * b) -> a 
+fst (a,_) = a 
+
+snd : (a * b) -> b 
+snd (_,b) = b 
+
+getKeys : N -> N -> (N * N) * (N * N)
+getKeys p1 p2 =
+  let m = p1 * p2,
+      totient = (p1 .- 1)*(p2 .- 1),
+      e = getPubExp 2 totient
+  in ((m, e), (m, getPrivExp e totient))
+
+-- guess -> totient -> e
+getPubExp : N -> N -> N
+getPubExp e totient =
+  {? e                          if gcd(e, totient) == 1
+   , getPubExp (e+1) totient    otherwise
+  ?}
+
+gcd : N*N -> N
+gcd (a, 0) = a
+gcd (a, b) = gcd (b, a mod b)
+
+getPrivExp : N -> N -> N
+getPrivExp e totient =
+  let t = inverse (0,1) (totient,e)
+  in {? abs t              if t>=0
+      , abs (t+totient)    otherwise
+     ?}
+
+
+-- Implemented using Extended Euclidean Algorithm (reference:
+-- https://en.wikipedia.org/wiki/Extended_Euclidean_algorithm#Computing_multiplicative_inverses_in_modular_structures)
+inverse : (Z * Z) -> (Z * Z) -> Z
+inverse (t,newt) (r,newr) =
+  {? t                                                                    if newr==0
+   , let q = r // newr in (inverse (newt, t-q*newt) (newr,r-q*newr))      otherwise
+  ?}
+
+-- encrypt1 : msg -> public key (mod,exp) -> encrypted msg
+-- encrypts one single number
+encrypt1 : Nat * Nat -> Nat -> Nat
+encrypt1 (m, e) msg = modPower msg e m
+
+-- decrypts one single number
+decrypt1 : Nat * Nat -> Nat -> Nat
+decrypt1 = encrypt1
+
+-- modPower : n -> power -> modulus -> nat
+-- Exponentiating by squaring algorithm reference:
+-- https://simple.wikipedia.org/wiki/Exponentiation_by_squaring
+modPower : Nat -> Nat -> Nat -> Nat
+modPower n p m =
+  {? 1                                     if p==0
+   , n % m                                 if p==1
+   , (modPower (n^2) (p//2) m) % m         if (even p)
+   , (n * (modPower (n^2) (p//2) m)) % m   if (p>2) && (odd p)
+  ?}