spec/crypto/sha/packed.bend
bend-collections-laws-crypto@1.0.0.0 · 114 lines · 20 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha.bend as F
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as S
4
5
6
7
8def len_hi(+n: Nat) -> U32:
9 +d0 = Nat.div(n, 32n)
10 +d1 = Nat.div(d0, 256n)
11 +d2 = Nat.div(d1, 256n)
12 +d3 = Nat.div(d2, 256n)
13 +d4 = Nat.div(d3, 256n)
14 +d5 = Nat.div(d4, 256n)
15 +d6 = Nat.div(d5, 256n)
16 F.decode(U32.from_nat(Nat.mod(d6, 256n)), U32.from_nat(Nat.mod(d5, 256n)),
17 U32.from_nat(Nat.mod(d4, 256n)), U32.from_nat(Nat.mod(d3, 256n)))
18
19def len_lo(+n: Nat) -> U32:
20 +d0 = Nat.div(n, 32n)
21 +d1 = Nat.div(d0, 256n)
22 +d2 = Nat.div(d1, 256n)
23 F.decode(U32.from_nat(Nat.mod(d2, 256n)), U32.from_nat(Nat.mod(d1, 256n)),
24 U32.from_nat(Nat.mod(d0, 256n)), U32.shln(U32.from_nat(Nat.mod(n, 32n)), 3n))
25
26def partial(+w: U32, delta: Nat) -> U32:
27 match delta:
28 case 0n: 2147483648
29 case 1n: U32.or(U32.and(w,4278190080),8388608)
30 case 2n: U32.or(U32.and(w,4294901760),32768)
31 case 3n: U32.or(U32.and(w,4294967040),128)
32 case _: w
33
34def pad_choose(c: Cmp, w: U32, delta: Nat) -> U32:
35 match c:
36 case GT{}: 0
37 case EQ{}: 2147483648
38 case LT{}: partial(w,delta)
39
40def pad_word(w: U32, +pos: Nat, +remain: Nat) -> U32:
41 pad_choose(Nat.cmp(pos,remain),w,Nat.sub(remain,pos))
42
43def length_word(short: Bool, w: U32, length: U32) -> U32:
44 match short:
45 case True{}: length
46 case False{}: w
47
48
49def padded_word(+position: Nat, w: U32, +remain: Nat, total: Nat) -> U32:
50 match position:
51 case 56n: length_word(Nat.is_lt(remain,56n),pad_word(w,56n,remain),len_hi(total))
52 case 60n: length_word(Nat.is_lt(remain,56n),pad_word(w,60n,remain),len_lo(total))
53 case _: pad_word(w,position,remain)
54
55def padded_words(ws: List<&2,U32>, +position: Nat, +remain: Nat, +total: Nat) -> List<&2,U32>:
56 match ws:
57 case Nil{}: Nil{}
58 case w <> tail:
59 padded_word(position,w,remain,total) <> padded_words(tail,Nat.add(position,4n),remain,total)
60
61def prepare(padding: Bool, ws: List<&2,U32>, remain: Nat, total: Nat) -> List<&2,U32>:
62 match padding:
63 case False{}: ws
64 case True{}: padded_words(ws,0n,remain,total)
65
66def compress(ws: List<&2,U32>, extra: Nat, s: S.State) -> S.State:
67 F.compress(F.schedule(extra,ws),F.constants(),s)
68
69def gather(+extra: Nat,n: Nat, +index: U32, +padding: Bool, +remain: Nat, +total: Nat,
70 s: S.State, acc: List<&2,U32>, pair: Array<U32> & U32) -> Array<U32> & S.State:
71 match n pair:
72 case 0n Tuple{a,w}:
73 (a,compress(prepare(padding,List.reverse(&2,U32,w <> acc),remain,total),extra,s))
74 case 1n+p Tuple{a,w}:
75 gather(extra,p,U32.inc(index),padding,remain,total,s,w <> acc,Array.get(U32,a,U32.inc(index)))
76
77def final_extra(+extra: Nat,more: Bool, +total: Nat, pair: Array<U32> & S.State) -> Array<U32> & S.State:
78 match more pair:
79 case False{} Tuple{a,s}: (a,s)
80 case True{} Tuple{a,s}:
81 (a,compress([0,0,0,0,0,0,0,0,0,0,0,0,0,0,len_hi(total),len_lo(total)],extra,s))
82
83def blocks(+extra: Nat,n: Nat, +index: U32, +remain: Nat, +total: Nat, pair: Array<U32> & S.State) -> Array<U32> & S.State:
84 match n pair:
85 case 0n Tuple{a,s}:
86 final_extra(extra,Nat.is_ge(remain,56n),total,gather(extra,15n,index,True{},remain,total,s,Nil{},Array.get(U32,a,index)))
87 case 1n+p Tuple{a,s}:
88 blocks(extra,p,U32.add(index,16),remain,total,gather(extra,15n,index,False{},0n,0n,s,Nil{},Array.get(U32,a,index)))
89
90def take_state(pair: Array<U32> & S.State) -> S.State:
91 Pair.snd(Array<U32>,S.State,pair)
92
93def hash_unchecked(a: Array<U32>, +length: Nat) -> S.State:
94 take_state(blocks(48n,Nat.div(length,64n),0,Nat.mod(length,64n),length,(a,F.initial())))
95
96def checked(valid: Bool, a: Array<U32>, length: Nat) -> Maybe<&2,S.State>:
97 match valid:
98 case False{}: None{}
99 case True{}: Some{hash_unchecked(a,length)}
100
101def sized(+length: Nat, pair: Array<U32> & U32) -> Maybe<&2,S.State>:
102 (a,capacity) = pair
103 checked(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
104
105def hash(a: Array<U32>, length: Nat) -> Maybe<&2,S.State>:
106 sized(length,Array.size(U32,a))
107
108def digest_result(r: Maybe<&2,S.State>) -> Maybe<&2,List<&2,U32>>:
109 match r:
110 case None{}: None{}
111 case Some{s}: Some{F.digest(s)}
112
113def sha256(a: Array<U32>, length: Nat) -> Maybe<&2,List<&2,U32>>:
114 digest_result(hash(a,length))