1	import Base
2	import ../sha.bend as F
3	import ../../../src/crypto/sha/state.bend as S
4	
5	# Packed-format reference: logical input byte j is the big-endian byte j%4
6	# of array word floor(j/4). Only the declared prefix is part of the message.
7	# Block collection uses a generic list reader, not the optimized 16-read chain.
8	def 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	
19	def 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	
26	def 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	
34	def 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	
40	def pad_word(w: U32, +pos: Nat, +remain: Nat) -> U32:
41	  pad_choose(Nat.cmp(pos,remain),w,Nat.sub(remain,pos))
42	
43	def length_word(short: Bool, w: U32, length: U32) -> U32:
44	  match short:
45	    case True{}: length
46	    case False{}: w
47	
48	
49	def 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	
55	def 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	
61	def 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	
66	def compress(ws: List<&2,U32>, extra: Nat, s: S.State) -> S.State:
67	  F.compress(F.schedule(extra,ws),F.constants(),s)
68	
69	def 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	
77	def 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	
83	def 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	
90	def take_state(pair: Array<U32> & S.State) -> S.State:
91	  Pair.snd(Array<U32>,S.State,pair)
92	
93	def 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	
96	def 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	
101	def 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	
105	def hash(a: Array<U32>, length: Nat) -> Maybe<&2,S.State>:
106	  sized(length,Array.size(U32,a))
107	
108	def 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	
113	def sha256(a: Array<U32>, length: Nat) -> Maybe<&2,List<&2,U32>>:
114	  digest_result(hash(a,length))