spec/crypto/keccak/main.bend
bend-collections@1.0.0.0 · 83 lines · 17 definitions
1import Base
2import bend-collections@1.0.0.0/src/crypto/keccak/types.bend as T
3import bend-collections@1.0.0.0/spec/crypto/keccak/permutation.bend as F
4
5def initial() -> T.State:
6 T.S{T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0},T.W{0,0}}
7
8def low_tail(w: U32, n: Nat) -> U32:
9 match n:
10 case 0n: 1
11 case 1n: U32.or(U32.and(w,255),256)
12 case 2n: U32.or(U32.and(w,65535),65536)
13 case 3n: U32.or(U32.and(w,16777215),16777216)
14 case _: w
15
16def select_tail(c: Cmp, w: U32, n: Nat) -> U32:
17 match c:
18 case GT{}: 0
19 case EQ{}: 1
20 case LT{}: low_tail(w,n)
21
22def tail_word(w: U32, +pos: Nat, +remain: Nat) -> U32:
23 select_tail(Nat.cmp(pos,remain),w,Nat.sub(remain,pos))
24
25def last_bit(w: U32, last: Bool) -> U32:
26 match last:
27 case False{}: w
28 case True{}: U32.or(w,2147483648)
29
30def pad(ws: List<&2,U32>, +pos: Nat, +remain: Nat) -> List<&2,U32>:
31 match ws:
32 case Nil{}: Nil{}
33 case w <> rest:
34 last_bit(tail_word(w,pos,remain),Nat.is_eq(pos,132n)) <> pad(rest,Nat.add(pos,4n),remain)
35
36def prepare(padding: Bool, ws: List<&2,U32>, remain: Nat) -> List<&2,U32>:
37 match padding:
38 case False{}: ws
39 case True{}: pad(ws,0n,remain)
40
41def inject(s: T.State, ws: List<&2,U32>) -> T.State:
42 match s ws:
43 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} w0 <> w1 <> w2 <> w3 <> w4 <> w5 <> w6 <> w7 <> w8 <> w9 <> w10 <> w11 <> w12 <> w13 <> w14 <> w15 <> w16 <> w17 <> w18 <> w19 <> w20 <> w21 <> w22 <> w23 <> w24 <> w25 <> w26 <> w27 <> w28 <> w29 <> w30 <> w31 <> w32 <> w33 <> Nil{}:
44 T.S{F.xor(a0,T.W{w0,w1}),F.xor(a1,T.W{w2,w3}),F.xor(a2,T.W{w4,w5}),F.xor(a3,T.W{w6,w7}),F.xor(a4,T.W{w8,w9}),F.xor(a5,T.W{w10,w11}),F.xor(a6,T.W{w12,w13}),F.xor(a7,T.W{w14,w15}),F.xor(a8,T.W{w16,w17}),F.xor(a9,T.W{w18,w19}),F.xor(a10,T.W{w20,w21}),F.xor(a11,T.W{w22,w23}),F.xor(a12,T.W{w24,w25}),F.xor(a13,T.W{w26,w27}),F.xor(a14,T.W{w28,w29}),F.xor(a15,T.W{w30,w31}),F.xor(a16,T.W{w32,w33}),a17,a18,a19,a20,a21,a22,a23,a24}
45 case s _: s
46
47def gather(+round_count: Nat, n: Nat, +base: U32, +next: U32, +padding: Bool, +remain: Nat, s: T.State, acc: List<&2,U32>, pair: Array<U32> & U32) -> Array<U32> & T.State:
48 match n pair:
49 case 0n Tuple{a,w}:
50 (a,F.rounds(round_count,0n,inject(s,prepare(padding,List.reverse(&2,U32,w <> acc),remain))))
51 case 1n+p Tuple{a,w}:
52 gather(round_count,p,base,U32.inc(next),padding,remain,s,w <> acc,Array.get(U32,a,U32.add(base,next)))
53
54def absorb(+round_count: Nat, a: Array<U32>, +index: U32, s: T.State) -> Array<U32> & T.State:
55 gather(round_count,33n,index,1,False{},0n,s,Nil{},Array.get(U32,a,index))
56
57def finish(round_count: Nat, a: Array<U32>, +index: U32, remain: Nat, s: T.State) -> T.State:
58 Pair.snd(Array<U32>,T.State,gather(round_count,33n,index,1,True{},remain,s,Nil{},Array.get(U32,a,index)))
59
60def blocks(+round_count: Nat, n: Nat, +index: U32, remain: Nat, pair: Array<U32> & T.State) -> T.State:
61 match n pair:
62 case 0n Tuple{a,s}: finish(round_count,a,index,remain,s)
63 case 1n+p Tuple{a,s}: blocks(round_count,p,U32.add(index,34),remain,absorb(round_count,a,index,s))
64
65def unchecked(+round_count: Nat, a: Array<U32>, +length: Nat) -> T.State:
66 blocks(round_count,Nat.div(length,136n),0,Nat.mod(length,136n),(a,initial()))
67
68def digest(s: T.State) -> Array<U32>:
69 match s:
70 case T.S{T.W{l0,h0},T.W{l1,h1},T.W{l2,h2},T.W{l3,h3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}:
71 ANode{ANode{ANode{ALeaf{l0},ALeaf{h0}},ANode{ALeaf{l1},ALeaf{h1}}},ANode{ANode{ALeaf{l2},ALeaf{h2}},ANode{ALeaf{l3},ALeaf{h3}}}}
72
73def checked(round_count: Nat, valid: Bool, a: Array<U32>, length: Nat) -> Maybe<&1,Array<U32>>:
74 match valid:
75 case False{}: None{}
76 case True{}: Some{digest(unchecked(round_count,a,length))}
77
78def sized(round_count: Nat, +length: Nat, pair: Array<U32> & U32) -> Maybe<&1,Array<U32>>:
79 (a,capacity) = pair
80 checked(round_count,Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
81
82def keccak256_rounds(round_count: Nat, a: Array<U32>, length: Nat) -> Maybe<&1,Array<U32>>:
83 sized(round_count,length,Array.size(U32,a))