From 96bff5c4a8e91eb90d6783b0d88d4a0f00bc114d Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 3 Oct 2017 13:40:53 -0700 Subject: [PATCH 1/2] Update keccak.cry example to work with Cryptol 2.x Fixes #458. --- examples/contrib/keccak.cry | 157 +++++++++++++++++------------------- 1 file changed, 75 insertions(+), 82 deletions(-) diff --git a/examples/contrib/keccak.cry b/examples/contrib/keccak.cry index 36fa8863..122029f2 100644 --- a/examples/contrib/keccak.cry +++ b/examples/contrib/keccak.cry @@ -23,109 +23,102 @@ // Specification of the Keccak (SHA-3) hash function // Author: David Lazar -SHA_3_224 M = take(224, Keccak `{r = 1152, c = 448} M); -SHA_3_256 M = take(256, Keccak `{r = 1088, c = 512} M); -SHA_3_384 M = take(384, Keccak `{r = 832, c = 768} M); -SHA_3_512 M = take(512, Keccak `{r = 576, c = 1024} M); +SHA_3_224 M = take`{224} (Keccak `{r = 1152, c = 448} M) +SHA_3_256 M = take`{256} (Keccak `{r = 1088, c = 512} M) +SHA_3_384 M = take`{384} (Keccak `{r = 832, c = 768} M) +SHA_3_512 M = take`{512} (Keccak `{r = 576, c = 1024} M) -Keccak : {r c m} - ( fin r, fin c, fin m - , r >= 0, c >= 0, m >= 0 - , fin ((r + m + 1) / r) - , (r + m + 1) / r >= 0 - , (r + m + 1) / r * r - m >= 2 +Keccak : {r, c, m, n} + ( fin r, fin c, fin m, fin n + , (r + c) % 25 == 0 , 64 >= (r + c) / 25 - , 25 * ((r + c) / 25) >= r - ) => [m] -> [inf]; + , r * n >= 2 + m + ) => [m] -> [inf] Keccak M = squeeze `{r = r} (absorb `{w = (r + c) / 25} Ps) - where Ps = pad `{r = r} M; + where Ps = pad `{r = r, n = n} M -squeeze : {r w} (fin r, fin w, 64 >= w, r >= 0, 25 * w >= r) => [5][5][w] -> [inf]; -squeeze A = take(`r, flatten A) # squeeze `{r = r} (Keccak_f A); +squeeze : {r, w} (fin r, fin w, 64 >= w, r >= 0, 25 * w >= r) => [5][5][w] -> [inf] +squeeze A = take`{r} (flatten A) # squeeze`{r = r} (Keccak_f A) -absorb : {r w n} (fin r, fin w, fin n, 64 >= w, 25 * w >= r) => [n][r] -> [5][5][w]; +absorb : {r, w, n} (fin r, fin w, fin n, 64 >= w, 25 * w >= r) => [n][r] -> [5][5][w] absorb Ps = as ! 0 - where { - as = [zero] # [| Keccak_f `{w = w} (s ^ (unflatten p)) || s <- as || p <- Ps |]; - }; + where + as = [zero] # [ Keccak_f `{w = w} (s ^ (unflatten p)) | s <- as | p <- Ps ] -pad : {r m n} +pad : {r, m, n} ( fin r, fin m, fin n - , n == (r + m + 1) / r - , r * n - m >= 2 - ) => [m] -> [n][r]; -pad M = split (M # [True] # zero # [True]); + , r * n >= 2 + m + ) => [m] -> [n][r] +pad M = split (M # [True] # (zero : [r*n-2-m]) # [True]) -Keccak_f : {b w} (fin w, b == 25 * w, 64 >= w) => [5][5][w] -> [5][5][w]; +Keccak_f : {w} (fin w, 64 >= w) => [5][5][w] -> [5][5][w] Keccak_f A = rounds ! 0 - where { - rounds = [A] # [| Round RC A || RC <- RCs `{w = w} || A <- rounds |]; - }; + where + rounds = [A] # [ Round RC A | RC <- RCs`{w = w} | A <- rounds ] -Round : {w} (fin w) => [5][5][w] -> [5][5][w] -> [5][5][w]; -Round RC A = ι RC (χ (π (ρ (θ A)))); +Round : {w} (fin w) => [5][5][w] -> [5][5][w] -> [5][5][w] +Round RC A = ι RC (χ (π (ρ (θ A)))) -θ : {w} (fin w) => [5][5][w] -> [5][5][w]; +θ : {w} (fin w) => [5][5][w] -> [5][5][w] θ A = A' - where { - C = [| xor a || a <- A |]; - D = [| C @ x ^ (C @ y <<< 1) - || x <- [0 .. 4] >>> 1 - || y <- [0 .. 4] <<< 1 - |]; - A' = [| [| a ^ (D @ x) || a <- A @ x |] || x <- [0 .. 4] |]; - }; + where + C = [ xor a | a <- A ] + D = [ C @ x ^ (C @ y <<< 1) + | x <- [0 .. 4] >>> 1 + | y <- [0 .. 4] <<< 1 + ] + A' = [ [ a ^ (D @ x) | a <- A @ x ] | x <- [0 .. 4] ] -ρ : {w} (fin w) => [5][5][w] -> [5][5][w]; -ρ A = groupBy(5, [| a <<< r || a <- join(A) || r <- R |]) - where R = [00 36 03 41 18 - 01 44 10 45 02 - 62 06 43 15 61 - 28 55 25 21 56 - 27 20 39 08 14]; +ρ : {w} (fin w) => [5][5][w] -> [5][5][w] +ρ A = groupBy`{5} [ a <<< r | a <- join A | r <- R ] + where R = [00, 36, 03, 41, 18, + 01, 44, 10, 45, 02, + 62, 06, 43, 15, 61, + 28, 55, 25, 21, 56, + 27, 20, 39, 08, 14] -π : {w} (fin w) => [5][5][w] -> [5][5][w]; -π A = groupBy(5, [| A @ ((x + (3:[8]) * y) % 5) @ x - || x <- [0..4], y <- [0..4] - |]); +π : {w} (fin w) => [5][5][w] -> [5][5][w] +π A = groupBy`{5} [ A @ ((x + (3:[8]) * y) % 5) @ x + | x <- [0..4], y <- [0..4] + ] -χ : {w} (fin w) => [5][5][w] -> [5][5][w]; -χ A = groupBy(5, [| (A @ x @ y) ^ (~ A @ ((x + 1) % 5) @ y - & A @ ((x + 2) % 5) @ y) - || x <- [0..4], y <- [0..4] - |]); +χ : {w} (fin w) => [5][5][w] -> [5][5][w] +χ A = groupBy`{5} [ (A @ x @ y) ^ (~ A @ ((x + 1) % 5) @ y + && A @ ((x + 2) % 5) @ y) + | x <- [0..4], y <- [0..4] + ] -ι : {w} (fin w) => [5][5][w] -> [5][5][w] -> [5][5][w]; -ι RC A = A ^ RC; +ι : {w} (fin w) => [5][5][w] -> [5][5][w] -> [5][5][w] +ι RC A = A ^ RC -RCs : {w n} (fin w, fin n, 24 >= n, n == 12 + 2 * (lg2 w)) => [n][5][5][w]; -RCs = [| [([(RC @@ [0 .. `(w - 1)])] # zero)] # zero - || RC <- RCs64 - || _ <- [1 .. `n] - |]; +RCs : {w, n} (fin w, fin n, 24 >= n, n == 12 + 2 * (lg2 w)) => [n][5][5][w] +RCs = [ [[take`{w} RC] # zero] # zero + | RC <- RCs64 + | _ <- zero:[n] + ] -RCs64 : [24][64]; +RCs64 : [24][64] RCs64 = join (transpose [ - [0x0000000000000001 0x000000008000808B] - [0x0000000000008082 0x800000000000008B] - [0x800000000000808A 0x8000000000008089] - [0x8000000080008000 0x8000000000008003] - [0x000000000000808B 0x8000000000008002] - [0x0000000080000001 0x8000000000000080] - [0x8000000080008081 0x000000000000800A] - [0x8000000000008009 0x800000008000000A] - [0x000000000000008A 0x8000000080008081] - [0x0000000000000088 0x8000000000008080] - [0x0000000080008009 0x0000000080000001] - [0x000000008000000A 0x8000000080008008] -]); + [0x0000000000000001, 0x000000008000808B], + [0x0000000000008082, 0x800000000000008B], + [0x800000000000808A, 0x8000000000008089], + [0x8000000080008000, 0x8000000000008003], + [0x000000000000808B, 0x8000000000008002], + [0x0000000080000001, 0x8000000000000080], + [0x8000000080008081, 0x000000000000800A], + [0x8000000000008009, 0x800000008000000A], + [0x000000000000008A, 0x8000000080008081], + [0x0000000000000088, 0x8000000000008080], + [0x0000000080008009, 0x0000000080000001], + [0x000000008000000A, 0x8000000080008008] +]) -unflatten : {r w} (fin r, 25*w >= r) => [r] -> [5][5][w]; -unflatten p = transpose(groupBy(5, groupBy(`w, p # zero))); +unflatten : {r, w} (fin w, 25*w >= r) => [r] -> [5][5][w] +unflatten p = transpose (groupBy`{5} (groupBy`{w} (p # zero))) -flatten : {r w} [5][5][w] -> [5 * 5 * w]; -flatten A = join (join (transpose A)); +flatten : {w} (fin w) => [5][5][w] -> [5 * 5 * w] +flatten A = join (join (transpose A)) -xor : {a b} (fin a) => [a][b] -> [b]; +xor : {a, b} (fin a) => [a][b] -> [b] xor xs = xors ! 0 - where xors = [0] # [| x ^ z || x <- xs || z <- xors |]; + where xors = [zero] # [ x ^ z | x <- xs | z <- xors ] From 866a1142da5bbb72415335f841c0fa004053c85a Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 3 Oct 2017 14:04:29 -0700 Subject: [PATCH 2/2] Try out a new logo. Stuff that matters :-) --- cryptol/REPL/Logo.hs | 31 ++++++++++++++++++++++--------- 1 file changed, 22 insertions(+), 9 deletions(-) diff --git a/cryptol/REPL/Logo.hs b/cryptol/REPL/Logo.hs index 6d2f7aee..2213c0ff 100644 --- a/cryptol/REPL/Logo.hs +++ b/cryptol/REPL/Logo.hs @@ -20,8 +20,8 @@ type Version = String type Logo = [String] -logo :: Bool -> Logo -logo useColor = +logo :: Bool -> (String -> [String]) -> Logo +logo useColor mk = [ sgr [SetColor Foreground Dull White] ++ l | l <- ws ] ++ [ sgr [SetColor Foreground Vivid Blue ] ++ l | l <- vs ] ++ [ sgr [SetColor Foreground Dull Blue ] ++ l | l <- ds ] @@ -35,7 +35,17 @@ logo useColor = ver = sgr [SetColor Foreground Dull White] ++ replicate (lineLen - 20 - length versionText) ' ' ++ versionText - ls = + ls = mk ver + slen = length ls `div` 3 + (ws,rest) = splitAt slen ls + (vs,ds) = splitAt slen rest + lineLen = length (head ls) + +displayLogo :: Bool -> REPL () +displayLogo useColor = unlessBatch (io (mapM_ putStrLn (logo useColor logo2))) + +logo1 :: String -> [String] +logo1 ver = [ " _ _" , " ___ _ __ _ _ _ __ | |_ ___ | |" , " / __| \'__| | | | \'_ \\| __/ _ \\| |" @@ -43,10 +53,13 @@ logo useColor = , " \\___|_| \\__, | .__/ \\__\\___/|_|" , " |___/|_| " ++ ver ] - slen = length ls `div` 3 - (ws,rest) = splitAt slen ls - (vs,ds) = splitAt slen rest - lineLen = length (head ls) -displayLogo :: Bool -> REPL () -displayLogo useColor = unlessBatch (io (mapM_ putStrLn (logo useColor))) +logo2 :: String -> [String] +logo2 ver = + [ "┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻ " + , "┃ ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃ " + , "┗━╸╹┗╸ ╹ ╹ ╹ ┗━┛┗━╸" + , ver + ] + +